diff --git a/hol4/IEEE_connectionScript.sml b/hol4/IEEE_connectionScript.sml
index a8f86f105b64058541183f49e8f1faf155ae256b..376f9791b94728827851e1141d10ec78f6f8af94 100644
--- a/hol4/IEEE_connectionScript.sml
+++ b/hol4/IEEE_connectionScript.sml
@@ -14,16 +14,20 @@ val _ = diminish_srw_ss ["RMULCANON_ss","RMULRELNORM_ss"]
(** FloVer assumes rounding with ties to even, thus we exprlicitly define
a rounding mode here **)
-val dmode_def = Define `dmode = roundTiesToEven`;
+Definition dmode_def :
+ dmode = roundTiesToEven
+End
-val optionLift_def = Define `
+Definition optionLift_def:
(optionLift (SOME v) some_cont none_cont = some_cont v) /\
- (optionLift (NONE) some_cont none_cont = none_cont)`;
+ (optionLift (NONE) some_cont none_cont = none_cont)
+End
-val updFlEnv_def = Define `
- updFlEnv x v E = \ y. if y = x then SOME v else E y`;
+Definition updFlEnv_def:
+ updFlEnv x v E = \ y. if y = x then SOME v else E y
+End
-val eval_expr_float_def = Define `
+Definition eval_expr_float_def:
(eval_expr_float (Var n) E = E n) /\
(eval_expr_float (Const m v) E = SOME v) /\
(eval_expr_float (Unop Neg e) E =
@@ -44,100 +48,52 @@ val eval_expr_float_def = Define `
(case (eval_expr_float e1 E), (eval_expr_float e2 E), (eval_expr_float e3 E) of
| SOME v1, SOME v2, SOME v3 => SOME (fp64_mul_add roundTiesToEven v1 v2 v3)
| _, _, _ => NONE)) /\
- (eval_expr_float (Downcast m e) E = NONE)`;
+ (eval_expr_float (Downcast m e) E = NONE)
+End
-val bstep_float_def = Define `
+Definition bstep_float_def:
(bstep_float (Let m x e g) E :word64 option=
optionLift (eval_expr_float e E)
(\ v. bstep_float g (updFlEnv x v E))
NONE) /\
- (bstep_float (Ret e) E = eval_expr_float e E)`;
+ (bstep_float (Ret e) E = eval_expr_float e E)
+End
-val normal_or_zero_def = Define `
- normal_or_zero (v:real) =
- (minValue_pos M64 <= abs v \/ v = 0)`;
-
-val isValid_def = Define `
- isValid e =
- let trans_e = optionLift e (\ v. SOME (float_to_real (fp64_to_float v))) NONE in
- optionLift trans_e normal_or_zero F`;
-
-val eval_expr_valid_def = Define `
- (eval_expr_valid (Var n) E = T) /\
- (eval_expr_valid (Const m v) E = T) /\
- (eval_expr_valid (Unop u e) E = eval_expr_valid e E) /\
- (eval_expr_valid (Binop b e1 e2) E =
- (eval_expr_valid e1 E /\ eval_expr_valid e2 E /\
- let e1_res = eval_expr_float e1 E in
- let e2_res = eval_expr_float e2 E in
- optionLift (e1_res)
- (\ v1. let v1_real = float_to_real (fp64_to_float v1)
- in
- optionLift e2_res
- (\ v2.
- let v2_real = float_to_real (fp64_to_float v2)
- in
- normal_or_zero (evalBinop b v1_real v2_real))
- T)
- T)) /\
- (eval_expr_valid (Fma e1 e2 e3) E =
- (eval_expr_valid e1 E /\ eval_expr_valid e2 E /\ eval_expr_valid e3 E /\
- let e1_res = eval_expr_float e1 E in
- let e2_res = eval_expr_float e2 E in
- let e3_res = eval_expr_float e3 E in
- optionLift (e1_res)
- (\ v1. let v1_real = float_to_real (fp64_to_float v1)
- in
- optionLift e2_res
- (\ v2.
- let v2_real = float_to_real (fp64_to_float v2)
- in
- optionLift e3_res
- (\ v3. let v3_real = float_to_real (fp64_to_float v3) in
- normal_or_zero (evalFma v1_real v2_real v3_real))
- T)
- T)
- T)) /\
- (eval_expr_valid (Downcast m e) E = eval_expr_valid e E)`;
-
-val bstep_valid_def = Define `
- (bstep_valid (Let m x e g) E =
- (eval_expr_valid e E /\
- optionLift (eval_expr_float e E)
- (\v_e. bstep_valid g (updFlEnv x v_e E))
- T)) /\
- (bstep_valid (Ret e) E = eval_expr_valid e E)`;
-
-val toRExp_def = Define `
+Definition toRExp_def:
(toRExp ((Var v):word64 expr) = Var v) /\
(toRExp (Const m c) = Const m (float_to_real (fp64_to_float c))) /\
(toRExp (Unop u e1) = Unop u (toRExp e1)) /\
(toRExp (Binop b e1 e2) = Binop b (toRExp e1) (toRExp e2)) /\
(toRExp (Fma e1 e2 e3) = Fma (toRExp e1) (toRExp e2) (toRExp e3)) /\
- (toRExp (Downcast m e1) = Downcast m (toRExp e1))`;
+ (toRExp (Downcast m e1) = Downcast m (toRExp e1))
+End
-val toRCmd_def = Define `
+Definition toRCmd_def:
(toRCmd (Let m x e g) = Let m x (toRExp e) (toRCmd g)) /\
- (toRCmd (Ret e) = Ret (toRExp e))`;
+ (toRCmd (Ret e) = Ret (toRExp e))
+End
-val toREnv_def = Define `
+Definition toREnv_def:
toREnv (E:num -> word64 option) (x:num):real option =
case E x of
| NONE => NONE
- | SOME v => SOME (float_to_real (fp64_to_float v))`;
+ | SOME v => SOME (float_to_real (fp64_to_float v))
+End
-val toWordEnv_def = Define `
+Definition toWordEnv_def:
toWordEnv E = \x. case E x of
- | SOME v => SOME (float_to_fp64 (real_to_float dmode v))
- | NONE => NONE`;
+ | SOME v => SOME (float_to_fp64 (real_to_float dmode v))
+ | NONE => NONE
+End
-val Binop_to_Rop_def = Define `
+Definition Binop_to_Rop_def:
Binop_to_Rop (b:binop) :real->real->real =
case b of
| Plus => $+
| Sub => $-
| Mult => $*
- | Div => $/ `;
+ | Div => $/
+End
Theorem real_div_pow:
! a n m. a <> 0 /\ n >= m ==> a pow n / a pow m = a pow (n - m)
@@ -159,14 +115,15 @@ Proof
\\ fs[REAL_MUL_RINV]
QED
-val pow_simp1 = Q.prove (`2 pow 2047 / 2 pow 1023 = 2 pow 1024`,
+Theorem pow_simp1[local] = Q.prove (`2 pow 2047 / 2 pow 1023 = 2 pow 1024`,
qspecl_then [`2`, `2047`,`1023`] destruct real_div_pow \\ fs[]);
-val pow_simp2 = Q.prove (`2 pow 2046 / 2 pow 1023 = 2 pow 1023`,
+Theorem pow_simp2[local] = Q.prove (`2 pow 2046 / 2 pow 1023 = 2 pow 1023`,
qspecl_then [`2`, `2046`,`1023`] destruct real_div_pow \\ fs[]);
-val threshold_64_bit_lt_maxValue = store_thm ("threshold_64_bit_lt_maxValue",
- ``maxValue M64 < threshold (:52 # 11)``,
+Theorem threshold_64_bit_lt_maxValue:
+ maxValue M64 < threshold (:52 # 11)
+Proof
rewrite_tac[threshold_def, maxValue_def, maxExponent_def, GSYM REAL_OF_NUM_POW]
\\ simp[pow_simp2]
\\ once_rewrite_tac [GSYM REAL_MUL_RID]
@@ -181,34 +138,40 @@ val threshold_64_bit_lt_maxValue = store_thm ("threshold_64_bit_lt_maxValue",
\\ irule REAL_LT_INV \\ fs[]
\\ `1 = 2 pow 0` by (fs[pow])
\\ pop_assum (fn thm => once_rewrite_tac [thm])
- \\ irule REAL_POW_MONO_LT \\ fs[]);
+ \\ irule REAL_POW_MONO_LT \\ fs[]
+QED
-val normalValue_implies_normalization = store_thm ("validFloatValue_implies_normalization",
- ``!v.
- normal v M64 ==>
- normalizes (:52 #11) v``,
+Theorem normalValue_implies_normalization:
+ !v.
+ normal v M64 ==>
+ normalizes (:52 #11) v
+Proof
rewrite_tac[normal_def, minValue_pos_def, maxValue_def, GSYM REAL_OF_NUM_POW]
\\ rpt strip_tac
\\ fs[normalizes_def, wordsTheory.INT_MAX_def, minExponentPos_def,
wordsTheory.INT_MIN_def, wordsTheory.dimindex_11,
wordsTheory.UINT_MAX_def, wordsTheory.dimword_11]
\\ irule REAL_LET_TRANS
- \\ qexists_tac `maxValue M64` \\ fs[threshold_64_bit_lt_maxValue, GSYM REAL_OF_NUM_POW, maxValue_def]);
+ \\ qexists_tac `maxValue M64` \\ fs[threshold_64_bit_lt_maxValue, GSYM REAL_OF_NUM_POW, maxValue_def]
+QED
-val normalValue_implies_finiteness = store_thm ("normalValue_implies_finiteness",
- ``!v.
- normal v M64 ==>
- float_is_finite ((real_to_float dmode v):(52 , 11) float)``,
+Theorem normalValue_implies_finiteness:
+ !v.
+ normal v M64 ==>
+ float_is_finite ((real_to_float dmode v):(52 , 11) float)
+Proof
rpt strip_tac
\\ fs [real_to_float_def, normal_def, dmode_def]
\\ irule float_round_finite
\\ irule REAL_LET_TRANS
- \\ qexists_tac `maxValue M64` \\ fs[threshold_64_bit_lt_maxValue]);
+ \\ qexists_tac `maxValue M64` \\ fs[threshold_64_bit_lt_maxValue]
+QED
-val denormalValue_implies_finiteness = store_thm ("normalValue_implies_finiteness",
- ``!v.
- denormal v M64 ==>
- float_is_finite ((real_to_float dmode v):(52 , 11) float)``,
+Theorem denormalValue_implies_finiteness:
+ !v.
+ denormal v M64 ==>
+ float_is_finite ((real_to_float dmode v):(52 , 11) float)
+Proof
rpt strip_tac
\\ fs [real_to_float_def, denormal_def, dmode_def]
\\ irule float_round_finite
@@ -221,7 +184,8 @@ val denormalValue_implies_finiteness = store_thm ("normalValue_implies_finitenes
\\ irule REAL_INV_LE_ANTIMONO_IMPR \\ fs[])
\\ fs[threshold_64_bit_lt_maxValue]
\\ irule REAL_LE_TRANS \\ qexists_tac `1`
- \\ fs[maxValue_def, maxExponent_def]);
+ \\ fs[maxValue_def, maxExponent_def]
+QED
Theorem normal_value_is_float_value:
∀ ff.
@@ -347,60 +311,69 @@ Proof
\\ fs[REAL_INV1]
QED
-val validValue_gives_float_value = store_thm ("validValue_gives_float_value",
- ``!ff:(52,11) float.
+Theorem validValue_gives_float_value:
+ !ff:(52,11) float.
validFloatValue (float_to_real ff) M64 ==>
- float_value ff = Float (float_to_real ff)``,
+ float_value ff = Float (float_to_real ff)
+Proof
rpt strip_tac \\ fs[validFloatValue_def]
>- (irule normal_value_is_float_value \\ fs[])
>- (irule denormal_value_is_float_value \\ fs[])
\\ fs[GSYM float_is_zero_to_real, float_is_zero_def]
- \\ every_case_tac \\ fs[]);
+ \\ every_case_tac \\ fs[]
+QED
-val normalTranslatedValue_implies_finiteness = store_thm ("normalTranslatedValue_implies_finiteness",
- ``!ff:double.
+Theorem normalTranslatedValue_implies_finiteness:
+ !ff:double.
normal (float_to_real ff) M64 ==>
- float_is_finite ff``,
+ float_is_finite ff
+Proof
rpt strip_tac
\\ fs[float_is_finite_def]
\\ qspec_then `ff` impl_subgoal_tac normal_value_is_float_value
- \\ fs[]);
+ \\ fs[]
+QED
-val denormalTranslatedValue_implies_finiteness = store_thm (
- "denormalTranslatedValue_implies_finiteness",
- ``!ff:double.
- denormal (float_to_real ff) M64 ==>
- float_is_finite ff``,
+Theorem denormalTranslatedValue_implies_finiteness:
+ !ff:double.
+ denormal (float_to_real ff) M64 ==>
+ float_is_finite ff
+Proof
rpt strip_tac
\\ fs[float_is_finite_def]
\\ qspec_then `ff` impl_subgoal_tac denormal_value_is_float_value
- \\ fs[]);
+ \\ fs[]
+QED
-val zero_value_implies_finiteness = store_thm ("zero_value_implies_finiteness",
- ``!v. v= 0 ==> float_is_finite ((real_to_float dmode v))``,
+Theorem zero_value_implies_finiteness:
+ !v. v= 0 ==> float_is_finite ((real_to_float dmode v))
+Proof
rpt strip_tac \\ rveq
\\ fs[real_to_float_def, dmode_def]
\\ irule float_round_finite
\\ fs[threshold_is_positive]
-);
+QED
-val finite_float_implies_threshold = Q.prove (
- `!f:(α , β) float.
- float_is_finite f ==>
- ~(float_to_real f ≤ -threshold (:α # β)) /\
- ~(float_to_real f ≥ threshold (:α # β)) `,
+Theorem finite_float_implies_threshold:
+ !f:(α , β) float.
+ float_is_finite f ==>
+ ~(float_to_real f ≤ -threshold (:α # β)) /\
+ ~(float_to_real f ≥ threshold (:α # β))
+Proof
rpt strip_tac
\\ drule lift_ieeeTheory.float_to_real_threshold
\\ simp[realTheory.abs]
\\ every_case_tac
- \\ strip_tac \\ RealArith.REAL_ASM_ARITH_TAC);
+ \\ strip_tac \\ RealArith.REAL_ASM_ARITH_TAC
+QED
-val round_float_to_real_id = Q.prove(
- `!f.
- float_is_finite f /\
- float_is_normal f /\
- ~ float_is_zero f ==>
- round roundTiesToEven (float_to_real f) = f`,
+Theorem round_float_to_real_id:
+ !f.
+ float_is_finite f /\
+ float_is_normal f /\
+ ~ float_is_zero f ==>
+ round roundTiesToEven (float_to_real f) = f
+Proof
rw[]
\\ qpat_assum `float_is_finite _` mp_tac
\\ qpat_assum `float_is_normal _` mp_tac
@@ -428,102 +401,120 @@ val round_float_to_real_id = Q.prove(
\\ fs[realTheory.REAL_SUB_REFL]
\\ rpt strip_tac
\\ fs[float_to_real_eq]
- \\ rfs[]);
+ \\ rfs[]
+QED
-val real_to_float_id = Q.store_thm ("real_to_float_id",
- `!f.
+Theorem real_to_float_id:
+ !f.
float_is_finite f /\
float_is_normal f /\
~ float_is_zero f ==>
- real_to_float dmode (float_to_real f) = f`,
-rpt strip_tac
-\\ fs[dmode_def, real_to_float_def, float_round_def, round_float_to_real_id]);
+ real_to_float dmode (float_to_real f) = f
+Proof
+ rpt strip_tac
+ \\ fs[dmode_def, real_to_float_def, float_round_def, round_float_to_real_id]
+QED
-val real_to_float_float_id = Q.prove (
- `!f.
- fp64_isFinite f /\
- fp64_isNormal f /\
- ~ fp64_isZero f ==>
- float_to_fp64 (real_to_float dmode (float_to_real (fp64_to_float f))) = f`,
-rpt strip_tac
-\\ fs[fp64_isFinite_def, fp64_isZero_def, fp64_isNormal_def]
-\\ fs[real_to_float_id]
-\\ fs[float_to_fp64_fp64_to_float]);
+Theorem real_to_float_float_id:
+ !f.
+ fp64_isFinite f /\
+ fp64_isNormal f /\
+ ~ fp64_isZero f ==>
+ float_to_fp64 (real_to_float dmode (float_to_real (fp64_to_float f))) = f
+Proof
+ rpt strip_tac
+ \\ fs[fp64_isFinite_def, fp64_isZero_def, fp64_isNormal_def]
+ \\ fs[real_to_float_id]
+ \\ fs[float_to_fp64_fp64_to_float]
+QED
-val float_to_real_real_to_float_zero_id = store_thm ("float_to_real_real_to_float_zero_id",
- ``float_to_real (real_to_float roundTiesToEven 0) = 0``,
+Theorem float_to_real_real_to_float_zero_id:
+ float_to_real (real_to_float roundTiesToEven 0) = 0
+Proof
once_rewrite_tac[real_to_float_def]
\\ `float_round roundTiesToEven F 0 = (float_plus_zero(:α#β))`
by (irule round_roundTiesToEven_is_plus_zero
\\ fs[ulp_def, ULP_def, real_div]
\\ irule REAL_LE_MUL \\ fs[pow]
\\ irule REAL_LE_INV \\ irule POW_POS \\ fs[])
- \\ fs[float_to_real_def, float_plus_zero_def]);
+ \\ fs[float_to_real_def, float_plus_zero_def]
+QED
-val div_eq0_general = store_thm ("div_eq0_general",
- ``!a b:real. b <> 0 ==> (a / b = 0 <=> a = 0)``,
+Theorem div_eq0_general:
+ !a b:real. b <> 0 ==> (a / b = 0 <=> a = 0)
+Proof
rpt strip_tac \\ Cases_on `0 < b` \\ fs[div_eq0]
\\ `0 < -b` by RealArith.REAL_ASM_ARITH_TAC
\\ `a/ -b = 0 <=> a = 0` by fs[div_eq0]
\\ fs[real_div]
\\ Cases_on `a = 0` \\ fs[]
- \\ Cases_on `inv b = 0` \\ fs[REAL_INV_NZ]);
+ \\ Cases_on `inv b = 0` \\ fs[REAL_INV_NZ]
+QED
-val float_to_real_round_zero_is_zero = store_thm (
- "float_to_real_round_zero_is_zero",
- ``!ff P.
- 2 * abs ff <= ulp ((:α#β) :(α#β) itself) ==>
- float_to_real ((float_round roundTiesToEven P ff):(α, β) float) = 0``,
+Theorem float_to_real_round_zero_is_zero:
+ !ff P.
+ 2 * abs ff <= ulp ((:α#β) :(α#β) itself) ==>
+ float_to_real ((float_round roundTiesToEven P ff):(α, β) float) = 0
+Proof
rpt strip_tac \\ Cases_on `P`
\\ fs [round_roundTiesToEven_is_plus_zero,
- round_roundTiesToEven_is_minus_zero, zero_to_real]);
+ round_roundTiesToEven_is_minus_zero, zero_to_real]
+QED
-val noDowncast_def = Define `
+Definition noDowncast_def:
(noDowncast (Var v) = T) /\
(noDowncast (Const _ _) = T) /\
(noDowncast (Unop _ e) = noDowncast e) /\
(noDowncast (Binop b e1 e2) = (noDowncast e1 /\ noDowncast e2)) /\
(noDowncast (Fma e1 e2 e3) = (noDowncast e1 /\ noDowncast e2 /\ noDowncast e3)) /\
- (noDowncast (Downcast _ _) = F)`;
+ (noDowncast (Downcast _ _) = F)
+End
-val noDowncastFun_def = Define `
+Definition noDowncastFun_def:
(noDowncastFun (Let m x e g) = (noDowncast e /\ noDowncastFun g)) /\
- (noDowncastFun (Ret e) = noDowncast e)`;
+ (noDowncastFun (Ret e) = noDowncast e)
+End
-val is64BitEval_def = Define `
+Definition is64BitEval_def:
(is64BitEval ((Const m c):real expr) = (m = M64)) /\
(is64BitEval (Unop _ e) = is64BitEval e) /\
(is64BitEval (Binop b e1 e2) = (is64BitEval e1 /\ is64BitEval e2)) /\
(is64BitEval (Fma e1 e2 e3) = (is64BitEval e1 /\ is64BitEval e2 /\ is64BitEval e3)) /\
(is64BitEval (Downcast m e) = ((m = M64) /\ is64BitEval e)) /\
- (is64BitEval ((Var v):real expr) = T)`;
+ (is64BitEval ((Var v):real expr) = T)
+End
-val is64BitBstep_def = Define `
+Definition is64BitBstep_def:
(is64BitBstep (Let m x e g) = ((m = M64) /\ is64BitEval e /\ is64BitBstep g)) /\
- (is64BitBstep (Ret e) = is64BitEval e)`;
+ (is64BitBstep (Ret e) = is64BitEval e)
+End
-val is64BitEnv_def = Define `
+Definition is64BitEnv_def:
is64BitEnv Gamma =
- ! e m. FloverMapTree_find e Gamma = SOME m ==> m = M64`;
+ ! e m. FloverMapTree_find e Gamma = SOME m ==> m = M64
+End
-val typing_expr_64bit = store_thm("typing_expr_64bit",
- ``!e Gamma.
- is64BitEnv Gamma /\
- validTypes e Gamma ==>
- FloverMapTree_find e Gamma = SOME M64``,
+Theorem typing_expr_64bit:
+ !e Gamma.
+ is64BitEnv Gamma /\
+ validTypes e Gamma ==>
+ FloverMapTree_find e Gamma = SOME M64
+Proof
Cases_on `e` \\ fs[Once validTypes_def, is64BitEnv_def]
\\ rpt strip_tac \\ fs[]
- \\ res_tac);
+ \\ res_tac
+QED
-val typing_cmd_64bit = store_thm (
- "typing_cmd_64bit",
- ``!f Gamma.
- is64BitEnv Gamma /\
- validTypesCmd f Gamma ==>
- FloverMapTree_find (getRetExp f) Gamma = SOME M64``,
+Theorem typing_cmd_64bit:
+ !f Gamma.
+ is64BitEnv Gamma /\
+ validTypesCmd f Gamma ==>
+ FloverMapTree_find (getRetExp f) Gamma = SOME M64
+Proof
Cases_on `f` \\ fs[Once validTypes_def, Once validTypesCmd_def, is64BitEnv_def]
\\ rpt strip_tac \\ fs[]
- \\ res_tac);
+ \\ res_tac
+QED
Theorem eval_expr_gives_IEEE:
!(e:word64 expr) E1 E2 E2_real Gamma vR A fVars dVars.
@@ -538,7 +529,7 @@ Theorem eval_expr_gives_IEEE:
is64BitEval (toRExp e) /\
is64BitEnv Gamma /\
noDowncast (toRExp e) /\
- eval_expr_valid e E2 /\
+ (* eval_expr_valid e E2 /\ *)
(∀v.
v ∈ domain dVars ⇒
∃vF m.
@@ -552,7 +543,7 @@ Proof
Induct_on `e` \\ rewrite_tac[toRExp_def] \\ rpt strip_tac
\\ inversion `eval_expr _ _ _ _ _` eval_expr_cases
\\ once_rewrite_tac [eval_expr_float_def]
- \\ fs[eval_expr_valid_def, isValid_def, noDowncast_def]
+ \\ fs[noDowncast_def]
>- (once_rewrite_tac [toREnv_def]
\\ fs[validFloatValue_def]
\\ rveq
@@ -560,9 +551,9 @@ Proof
float_to_real_real_to_float_zero_id]
\\ fs[toREnv_def]
\\ fs[eval_expr_float_def, optionLift_def]
- \\ Cases_on `E2 n` \\ fs[optionLift_def, normal_or_zero_def])
+ \\ Cases_on `E2 n` \\ fs[optionLift_def])
>- (rveq \\ fs[eval_expr_cases]
- \\ fs[optionLift_def, normal_or_zero_def, minValue_pos_def,
+ \\ fs[optionLift_def, minValue_pos_def,
minExponentPos_def, REAL_LT_INV_EQ]
\\ qexists_tac `0:real`
\\ fs[mTypeToR_pos, perturb_def, fp64_to_float_float_to_fp64,
@@ -619,15 +610,7 @@ Proof
\\ rw_thm_asm `validTypes _ _` validTypes_def
\\ rw_thm_asm `validRanges _ _ _ _` validRanges_def
\\ fs[eval_expr_float_def, optionLift_def]
- \\ IMP_RES_TAC validTypes_exec
- (* \\ `m1 = m1'`
- by (first_x_assum irule \\ qexistsl_tac [`toREnv E2`, `v1`]
- \\ rewrite_tac [toRExpMap_def]
- \\ first_x_assum MATCH_ACCEPT_TAC)
- \\ `m2 = m2'`
- by (first_x_assum irule \\ qexistsl_tac [`toREnv E2`, `v2`]
- \\ rewrite_tac [toRExpMap_def]
- \\ first_x_assum MATCH_ACCEPT_TAC) *)
+ \\ imp_res_tac validTypes_exec
\\ rveq
\\ `m1 = M64 /\ m2 = M64`
by (fs[is64BitEnv_def]
@@ -669,7 +652,7 @@ Proof
\\ fs[]
\\ rename1 `eval_expr_float e1 _ = SOME vF1`
\\ rename1 `eval_expr_float e2 _ = SOME vF2`
- \\ IMP_RES_TAC validRanges_single
+ \\ imp_res_tac validRanges_single
\\ rename1 `FloverMapTree_find (toRExp e2) A = SOME (iv2, err2)`
\\ rename1 `FloverMapTree_find (toRExp e1) A = SOME (iv1, err1)`
\\ rename1 `eval_expr E1 _ (toREval (toRExp e2)) nR2 REAL`
@@ -786,40 +769,71 @@ Proof
\\ fs[option_case_eq] \\ rpt (TOP_CASE_TAC \\ fs[]))
\\ irule eval_eq_env
\\ find_exists_tac \\ fs[])
- (* \\ simp[eval_expr_cases] *)
- (** Case distinction for operator **)
- \\ Cases_on `b` \\ fs[optionLift_def, PULL_EXISTS, normal_or_zero_def]
- \\ simp[Once eval_expr_cases]
- (* Addition, result normal *)
- >- (fs[fp64_add_def, fp64_to_float_float_to_fp64, evalBinop_def]
- \\ `normal (evalBinop Plus (float_to_real (fp64_to_float vF1))
- (float_to_real (fp64_to_float vF2))) M64`
- by (rw_thm_asm `validFloatValue (_ + _) _` validFloatValue_def
- \\ fs[normal_def, denormal_def, evalBinop_def]
- >- (`abs (float_to_real (fp64_to_float vF1) +
- float_to_real (fp64_to_float vF2)) <
- abs (float_to_real (fp64_to_float vF1) +
- float_to_real (fp64_to_float vF2))`
- suffices_by (fs[])
- \\ irule REAL_LTE_TRANS
- \\ asm_exists_tac \\ fs[])
- \\ qpat_x_assum `_ + _ = 0` (fn thm => fs[thm])
- \\ fs[maxValue_def, maxExponent_def])
- \\ Q.ISPECL_THEN [`(fp64_to_float vF1):(52,11) float`,
- `(fp64_to_float vF2):(52,11) float`]
- impl_subgoal_tac
- float_add_relative
- >- (rpt conj_tac
- \\ fs[validFloatValue_def,
- normalTranslatedValue_implies_finiteness,
- denormalTranslatedValue_implies_finiteness,
- normalValue_implies_normalization,
- GSYM float_is_zero_to_real, float_is_finite, evalBinop_def])
- \\ fs[dmode_def]
- \\ qexistsl_tac [`M64`, `M64`, `float_to_real (fp64_to_float vF1)`,
- `float_to_real (fp64_to_float vF2)`, `e`]
- \\ fs[perturb_def, evalBinop_def]
- \\ fs[mTypeToR_def])
+ \\ qpat_x_assum `validFloatValue (evalBinop _ _ _) M64` (assume_tac o SIMP_RULE std_ss [validFloatValue_def])
+ (** Case distinction for operator **)
+ \\ Cases_on `b` \\ fs[optionLift_def, PULL_EXISTS]
+ \\ simp[Once eval_expr_cases]
+ (* Addition, result normal *)
+ >- (fs[fp64_add_def, fp64_to_float_float_to_fp64, evalBinop_def]
+ \\ Q.ISPECL_THEN [`(fp64_to_float vF1):(52,11) float`,
+ `(fp64_to_float vF2):(52,11) float`]
+ impl_subgoal_tac
+ float_add_relative
+ >- (rpt conj_tac
+ \\ fs[validFloatValue_def,
+ normalTranslatedValue_implies_finiteness,
+ denormalTranslatedValue_implies_finiteness,
+ normalValue_implies_normalization,
+ GSYM float_is_zero_to_real, float_is_finite, evalBinop_def])
+ \\ fs[dmode_def]
+ \\ qexistsl_tac [`M64`, `M64`, `float_to_real (fp64_to_float vF1)`,
+ `float_to_real (fp64_to_float vF2)`, `e`]
+ \\ fs[perturb_def, evalBinop_def]
+ \\ imp_res_tac normal_not_denormal
+ \\ fs[REAL_INV_1OVER, mTypeToR_def])
+ (* addition, result denormal *)
+ >- (fs[fp64_add_def, fp64_to_float_float_to_fp64, evalBinop_def]
+ \\ Q.ISPECL_THEN [`(fp64_to_float vF1):(52,11) float`,
+ `(fp64_to_float vF2):(52,11) float`]
+ impl_subgoal_tac
+ float_add_relative_denorm
+ >- (rpt conj_tac
+ >- fs[validFloatValue_def,
+ normalTranslatedValue_implies_finiteness,
+ denormalTranslatedValue_implies_finiteness,
+ normalValue_implies_normalization, float_is_finite,
+ GSYM float_is_zero_to_real, evalBinop_def]
+ >- fs[validFloatValue_def,
+ normalTranslatedValue_implies_finiteness,
+ denormalTranslatedValue_implies_finiteness,
+ normalValue_implies_normalization, float_is_finite,
+ GSYM float_is_zero_to_real, evalBinop_def]
+ >- (
+ fs[normalTranslatedValue_implies_finiteness,
+ denormalTranslatedValue_implies_finiteness,
+ normalValue_implies_normalization, float_is_finite,
+ GSYM float_is_zero_to_real, evalBinop_def, denormal_def, minValue_pos_def]
+ \\ rewrite_tac [INT_MAX_def, INT_MIN_def, dimindex_11, EVAL “2 ** (11 - 1) - 1 - 1â€]
+ \\ irule REAL_LT_TRANS
+ \\ asm_exists_tac \\ fs[GSYM REAL_OF_NUM_POW, minExponentPos_def]
+ \\ irule REAL_LET_TRANS \\ qexists_tac ‘1 * inv (2 pow 1022)’
+ \\ conj_tac
+ >- (rewrite_tac[real_div] \\ irule REAL_LT_RMUL_IMP \\ fs[])
+ \\ fs[])
+ >- (irule REAL_LT_TRANS \\ qexists_tac ‘maxValue M64’
+ \\ fs[threshold_64_bit_lt_maxValue, denormal_def]
+ \\ irule REAL_LTE_TRANS \\ qexists_tac ‘minValue_pos M64’
+ \\ fs[minValue_pos_def, maxValue_def, GSYM REAL_OF_NUM_POW]
+ \\ irule REAL_LE_TRANS \\ qexists_tac ‘1’ \\ conj_tac
+ >- (once_rewrite_tac[GSYM REAL_INV1] \\ irule REAL_INV_LE_ANTIMONO_IMPR
+ \\ fs[POW_2_LE1])
+ \\ fs[POW_2_LE1])
+ \\ fs[INT_MAX_def, INT_MIN_def, dimindex_11])
+ \\ fs[dmode_def]
+ \\ qexistsl_tac [`M64`, `M64`, `float_to_real (fp64_to_float vF1)`,
+ `float_to_real (fp64_to_float vF2)`, `e`]
+ \\ fs[perturb_def, evalBinop_def]
+ \\ fs[mTypeToR_def, minExponentPos_def, REAL_INV_1OVER])
(* result = 0 *)
>- (IMP_RES_TAC validValue_gives_float_value
\\ fs[REAL_LNEG_UNIQ, evalBinop_def]
@@ -836,35 +850,66 @@ Proof
\\ fs[float_to_real_round_zero_is_zero])
(* Subtraction, normal value *)
>- (fs[fp64_sub_def, fp64_to_float_float_to_fp64, evalBinop_def]
- \\ `normal (evalBinop Sub (float_to_real (fp64_to_float vF1))
- (float_to_real (fp64_to_float vF2))) M64`
- by (rw_thm_asm `validFloatValue (_ - _) _` validFloatValue_def
- \\ fs[normal_def, denormal_def, evalBinop_def]
- >- (`abs (float_to_real (fp64_to_float vF1) -
- float_to_real (fp64_to_float vF2)) <
- abs (float_to_real (fp64_to_float vF1) -
- float_to_real (fp64_to_float vF2))`
- suffices_by (fs[])
- \\ irule REAL_LTE_TRANS
- \\ asm_exists_tac \\ fs[])
- \\ qpat_x_assum `float_to_real (fp64_to_float _) = _`
- (fn thm => fs[thm])
- \\ fs[maxValue_def, maxExponent_def])
\\ Q.ISPECL_THEN [`(fp64_to_float vF1):(52,11) float`,
`(fp64_to_float vF2):(52,11) float`]
impl_subgoal_tac
float_sub_relative
- >- (rpt conj_tac
- \\ fs[validFloatValue_def,
- normalTranslatedValue_implies_finiteness,
- denormalTranslatedValue_implies_finiteness,
- normalValue_implies_normalization,
- GSYM float_is_zero_to_real, float_is_finite, evalBinop_def])
- \\ fs[dmode_def]
- \\ qexistsl_tac [`M64`, `M64`, `float_to_real (fp64_to_float vF1)`,
- `float_to_real (fp64_to_float vF2)`, `e`]
- \\ fs[perturb_def, evalBinop_def]
- \\ fs[mTypeToR_def])
+ >- (rpt conj_tac
+ \\ fs[validFloatValue_def,
+ normalTranslatedValue_implies_finiteness,
+ denormalTranslatedValue_implies_finiteness,
+ normalValue_implies_normalization,
+ GSYM float_is_zero_to_real, float_is_finite, evalBinop_def])
+ \\ fs[dmode_def]
+ \\ qexistsl_tac [`M64`, `M64`, `float_to_real (fp64_to_float vF1)`,
+ `float_to_real (fp64_to_float vF2)`, `e`]
+ \\ fs[perturb_def, evalBinop_def]
+ \\ imp_res_tac normal_not_denormal
+ \\ fs[mTypeToR_def, REAL_INV_1OVER])
+ (* Subtraction, denormal value *)
+ >- (fs[fp64_sub_def, fp64_to_float_float_to_fp64, evalBinop_def]
+ \\ Q.ISPECL_THEN [`(fp64_to_float vF1):(52,11) float`,
+ `(fp64_to_float vF2):(52,11) float`]
+ impl_subgoal_tac
+ float_sub_relative_denorm
+ >- (rpt conj_tac
+ >- fs[validFloatValue_def,
+ normalTranslatedValue_implies_finiteness,
+ denormalTranslatedValue_implies_finiteness,
+ normalValue_implies_normalization, float_is_finite,
+ GSYM float_is_zero_to_real, evalBinop_def]
+ >- fs[validFloatValue_def,
+ normalTranslatedValue_implies_finiteness,
+ denormalTranslatedValue_implies_finiteness,
+ normalValue_implies_normalization, float_is_finite,
+ GSYM float_is_zero_to_real, evalBinop_def]
+ >- (
+ fs[normalTranslatedValue_implies_finiteness,
+ denormalTranslatedValue_implies_finiteness,
+ normalValue_implies_normalization, float_is_finite,
+ GSYM float_is_zero_to_real, evalBinop_def, denormal_def, minValue_pos_def]
+ \\ rewrite_tac [INT_MAX_def, INT_MIN_def, dimindex_11, EVAL “2 ** (11 - 1) - 1 - 1â€]
+ \\ irule REAL_LT_TRANS
+ \\ asm_exists_tac \\ fs[GSYM REAL_OF_NUM_POW, minExponentPos_def]
+ \\ irule REAL_LET_TRANS \\ qexists_tac ‘1 * inv (2 pow 1022)’
+ \\ conj_tac
+ >- (rewrite_tac[real_div] \\ irule REAL_LT_RMUL_IMP \\ fs[])
+ \\ fs[])
+ >- (irule REAL_LT_TRANS \\ qexists_tac ‘maxValue M64’
+ \\ fs[threshold_64_bit_lt_maxValue, denormal_def]
+ \\ irule REAL_LTE_TRANS \\ qexists_tac ‘minValue_pos M64’
+ \\ fs[minValue_pos_def, maxValue_def, GSYM REAL_OF_NUM_POW]
+ \\ irule REAL_LE_TRANS \\ qexists_tac ‘1’ \\ conj_tac
+ >- (once_rewrite_tac[GSYM REAL_INV1] \\ irule REAL_INV_LE_ANTIMONO_IMPR
+ \\ fs[POW_2_LE1])
+ \\ fs[POW_2_LE1])
+ \\ fs[INT_MAX_def, INT_MIN_def, dimindex_11])
+ \\ fs[dmode_def]
+ \\ qexistsl_tac [`M64`, `M64`, `float_to_real (fp64_to_float vF1)`,
+ `float_to_real (fp64_to_float vF2)`, `e`]
+ \\ fs[perturb_def, evalBinop_def]
+ \\ fs[mTypeToR_def, minExponentPos_def, REAL_INV_1OVER])
+ (* subtraction, result = 0 *)
>- (fs[evalBinop_def]
\\ qpat_x_assum `float_to_real (fp64_to_float _) = _` MP_TAC
\\ simp[real_sub, REAL_LNEG_UNIQ, evalBinop_def]
@@ -882,25 +927,8 @@ Proof
\\ irule REAL_LE_MUL \\ fs[]
\\ irule REAL_LE_INV \\ fs[])
\\ fs[ float_to_real_round_zero_is_zero])
- (* Multiplication *)
+ (* Multiplication, normal result *)
>- (fs[fp64_mul_def, fp64_to_float_float_to_fp64, evalBinop_def]
- \\ `normal (evalBinop Mult (float_to_real (fp64_to_float vF1))
- (float_to_real (fp64_to_float vF2))) M64`
- by (rw_thm_asm `validFloatValue (_ * _) _` validFloatValue_def
- \\ fs[normal_def, denormal_def, evalBinop_def]
- >- (`abs (float_to_real (fp64_to_float vF1) *
- float_to_real (fp64_to_float vF2)) <
- abs (float_to_real (fp64_to_float vF1) *
- float_to_real (fp64_to_float vF2))`
- suffices_by (fs[])
- \\ irule REAL_LTE_TRANS
- \\ asm_exists_tac \\ fs[])
- >- (qpat_x_assum `float_to_real (fp64_to_float _) = _`
- (fn thm => fs[thm])
- \\ fs[maxValue_def, maxExponent_def])
- \\ qpat_x_assum `float_to_real (fp64_to_float _) = _`
- (fn thm => fs[thm])
- \\ fs[maxValue_def, maxExponent_def])
\\ Q.ISPECL_THEN [`(fp64_to_float vF1):(52,11) float`,
`(fp64_to_float vF2):(52,11) float`]
impl_subgoal_tac
@@ -915,7 +943,52 @@ Proof
\\ qexistsl_tac [`M64`, `M64`, `float_to_real (fp64_to_float vF1)`,
`float_to_real (fp64_to_float vF2)`, `e`]
\\ fs[perturb_def, evalBinop_def]
- \\ fs[mTypeToR_def])
+ \\ imp_res_tac normal_not_denormal
+ \\ fs[mTypeToR_def, REAL_INV_1OVER])
+ (* Multiplication, denormal result *)
+ >- (fs[fp64_mul_def, fp64_to_float_float_to_fp64, evalBinop_def]
+ \\ Q.ISPECL_THEN [`(fp64_to_float vF1):(52,11) float`,
+ `(fp64_to_float vF2):(52,11) float`]
+ impl_subgoal_tac
+ float_mul_relative_denorm
+ >- (rpt conj_tac
+ >- fs[validFloatValue_def,
+ normalTranslatedValue_implies_finiteness,
+ denormalTranslatedValue_implies_finiteness,
+ normalValue_implies_normalization, float_is_finite,
+ GSYM float_is_zero_to_real, evalBinop_def]
+ >- fs[validFloatValue_def,
+ normalTranslatedValue_implies_finiteness,
+ denormalTranslatedValue_implies_finiteness,
+ normalValue_implies_normalization, float_is_finite,
+ GSYM float_is_zero_to_real, evalBinop_def]
+ >- (
+ fs[normalTranslatedValue_implies_finiteness,
+ denormalTranslatedValue_implies_finiteness,
+ normalValue_implies_normalization, float_is_finite,
+ GSYM float_is_zero_to_real, evalBinop_def, denormal_def, minValue_pos_def]
+ \\ rewrite_tac [INT_MAX_def, INT_MIN_def, dimindex_11, EVAL “2 ** (11 - 1) - 1 - 1â€]
+ \\ irule REAL_LT_TRANS
+ \\ asm_exists_tac \\ fs[GSYM REAL_OF_NUM_POW, minExponentPos_def]
+ \\ irule REAL_LET_TRANS \\ qexists_tac ‘1 * inv (2 pow 1022)’
+ \\ conj_tac
+ >- (rewrite_tac[real_div] \\ irule REAL_LT_RMUL_IMP \\ fs[])
+ \\ fs[])
+ >- (irule REAL_LT_TRANS \\ qexists_tac ‘maxValue M64’
+ \\ fs[threshold_64_bit_lt_maxValue, denormal_def]
+ \\ irule REAL_LTE_TRANS \\ qexists_tac ‘minValue_pos M64’
+ \\ fs[minValue_pos_def, maxValue_def, GSYM REAL_OF_NUM_POW]
+ \\ irule REAL_LE_TRANS \\ qexists_tac ‘1’ \\ conj_tac
+ >- (once_rewrite_tac[GSYM REAL_INV1] \\ irule REAL_INV_LE_ANTIMONO_IMPR
+ \\ fs[POW_2_LE1])
+ \\ fs[POW_2_LE1])
+ \\ fs[INT_MAX_def, INT_MIN_def, dimindex_11])
+ \\ fs[dmode_def]
+ \\ qexistsl_tac [`M64`, `M64`, `float_to_real (fp64_to_float vF1)`,
+ `float_to_real (fp64_to_float vF2)`, `e`]
+ \\ fs[perturb_def, evalBinop_def]
+ \\ fs[mTypeToR_def, minExponentPos_def, REAL_INV_1OVER])
+ (* multiplication, result = 0 *)
>- (fs[evalBinop_def, REAL_ENTIRE, fp64_mul_def, float_mul_def,
GSYM float_is_zero_to_real, float_is_zero_def]
THENL [ Cases_on `float_value (fp64_to_float vF1)`,
@@ -936,51 +1009,9 @@ Proof
\\ rveq
\\ fs[GSYM float_is_zero_to_real, float_is_zero_def,
mTypeToR_pos, perturb_def])
- (* Division *)
+ (* Division, normal result *)
>- (fs[fp64_div_def, fp64_to_float_float_to_fp64, evalBinop_def]
- \\ `normal (evalBinop Div (float_to_real (fp64_to_float vF1))
- (float_to_real (fp64_to_float vF2))) M64`
- by (rw_thm_asm `validFloatValue (_ / _) _` validFloatValue_def
- \\ fs[normal_def, denormal_def, evalBinop_def]
- >- (`abs (float_to_real (fp64_to_float vF1) /
- float_to_real (fp64_to_float vF2)) <
- abs (float_to_real (fp64_to_float vF1) /
- float_to_real (fp64_to_float vF2))`
- suffices_by (fs[])
- \\ irule REAL_LTE_TRANS
- \\ asm_exists_tac \\ fs[])
- \\ qpat_x_assum `_ = 0` (fn thm => fs[thm])
- \\ fs[maxValue_def, maxExponent_def])
- \\ Q.ISPECL_THEN [`(fp64_to_float vF1):(52,11) float`,
- `(fp64_to_float vF2):(52,11) float`]
- impl_subgoal_tac
- float_div_relative
- >- (rpt conj_tac
- \\ fs[validFloatValue_def,
- normalTranslatedValue_implies_finiteness,
- denormalTranslatedValue_implies_finiteness,
- normalValue_implies_normalization,
- GSYM float_is_zero_to_real, float_is_finite, evalBinop_def])
- \\ fs[dmode_def]
- \\ qexistsl_tac [`M64`, `M64`, `float_to_real (fp64_to_float vF1)`,
- `float_to_real (fp64_to_float vF2)`, `e`]
- \\ fs[perturb_def, evalBinop_def]
- \\ fs[mTypeToR_def])
- >- (fs[fp64_div_def, fp64_to_float_float_to_fp64, evalBinop_def]
- \\ `normal (evalBinop Div (float_to_real (fp64_to_float vF1))
- (float_to_real (fp64_to_float vF2))) M64`
- by (rw_thm_asm `validFloatValue (_ / _) _` validFloatValue_def
- \\ fs[normal_def, denormal_def, evalBinop_def]
- >- (`abs (float_to_real (fp64_to_float vF1) /
- float_to_real (fp64_to_float vF2)) <
- abs (float_to_real (fp64_to_float vF1) /
- float_to_real (fp64_to_float vF2))`
- suffices_by (fs[])
- \\ irule REAL_LTE_TRANS
- \\ asm_exists_tac \\ fs[])
- \\ qpat_x_assum `_ = 0` (fn thm => fs[thm])
- \\ fs[maxValue_def, maxExponent_def])
- \\ Q.ISPECL_THEN [`(fp64_to_float vF1):(52,11) float`,
+ \\ Q.ISPECL_THEN [`(fp64_to_float vF1):(52,11) float`,
`(fp64_to_float vF2):(52,11) float`]
impl_subgoal_tac
float_div_relative
@@ -994,11 +1025,61 @@ Proof
\\ qexistsl_tac [`M64`, `M64`, `float_to_real (fp64_to_float vF1)`,
`float_to_real (fp64_to_float vF2)`, `e`]
\\ fs[perturb_def, evalBinop_def]
- \\ fs[mTypeToR_def])
+ \\ imp_res_tac normal_not_denormal
+ \\ fs[mTypeToR_def, REAL_INV_1OVER])
+ (* Division, denormal result *)
+ >- (fs[fp64_div_def, fp64_to_float_float_to_fp64, evalBinop_def]
+ \\ Q.ISPECL_THEN [`(fp64_to_float vF1):(52,11) float`,
+ `(fp64_to_float vF2):(52,11) float`]
+ impl_subgoal_tac
+ float_div_relative_denorm
+ >- (rpt conj_tac
+ >- fs[validFloatValue_def,
+ normalTranslatedValue_implies_finiteness,
+ denormalTranslatedValue_implies_finiteness,
+ normalValue_implies_normalization, float_is_finite,
+ GSYM float_is_zero_to_real, evalBinop_def]
+ >- fs[validFloatValue_def,
+ normalTranslatedValue_implies_finiteness,
+ denormalTranslatedValue_implies_finiteness,
+ normalValue_implies_normalization, float_is_finite,
+ GSYM float_is_zero_to_real, evalBinop_def]
+ >- fs[validFloatValue_def,
+ normalTranslatedValue_implies_finiteness,
+ denormalTranslatedValue_implies_finiteness,
+ normalValue_implies_normalization, float_is_finite,
+ GSYM float_is_zero_to_real, evalBinop_def]
+ >- (
+ fs[normalTranslatedValue_implies_finiteness,
+ denormalTranslatedValue_implies_finiteness,
+ normalValue_implies_normalization, float_is_finite,
+ GSYM float_is_zero_to_real, evalBinop_def, denormal_def, minValue_pos_def]
+ \\ rewrite_tac [INT_MAX_def, INT_MIN_def, dimindex_11, EVAL “2 ** (11 - 1) - 1 - 1â€]
+ \\ irule REAL_LT_TRANS
+ \\ asm_exists_tac \\ fs[GSYM REAL_OF_NUM_POW, minExponentPos_def]
+ \\ irule REAL_LET_TRANS \\ qexists_tac ‘1 * inv (2 pow 1022)’
+ \\ conj_tac
+ >- (rewrite_tac[real_div] \\ irule REAL_LT_RMUL_IMP \\ fs[])
+ \\ fs[])
+ >- (irule REAL_LT_TRANS \\ qexists_tac ‘maxValue M64’
+ \\ fs[threshold_64_bit_lt_maxValue, denormal_def]
+ \\ irule REAL_LTE_TRANS \\ qexists_tac ‘minValue_pos M64’
+ \\ fs[minValue_pos_def, maxValue_def, GSYM REAL_OF_NUM_POW]
+ \\ irule REAL_LE_TRANS \\ qexists_tac ‘1’ \\ conj_tac
+ >- (once_rewrite_tac[GSYM REAL_INV1] \\ irule REAL_INV_LE_ANTIMONO_IMPR
+ \\ fs[POW_2_LE1])
+ \\ fs[POW_2_LE1])
+ \\ fs[INT_MAX_def, INT_MIN_def, dimindex_11])
+ \\ fs[dmode_def]
+ \\ qexistsl_tac [`M64`, `M64`, `float_to_real (fp64_to_float vF1)`,
+ `float_to_real (fp64_to_float vF2)`, `e`]
+ \\ fs[perturb_def, evalBinop_def]
+ \\ fs[mTypeToR_def, minExponentPos_def, REAL_INV_1OVER])
+ (* division, result = 0 *)
>- (fs[fp64_div_def, dmode_def, fp64_to_float_float_to_fp64,
float_div_def, evalBinop_def]
\\ `float_to_real (fp64_to_float vF1) = 0`
- by (fs[div_eq0_general])
+ by (imp_res_tac div_eq0_general)
\\ rw_thm_asm `float_to_real (fp64_to_float vF1) = 0` (GSYM float_is_zero_to_real)
\\ fs[float_is_zero_def]
\\ Cases_on `float_value (fp64_to_float vF1)`
@@ -1018,10 +1099,77 @@ Proof
\\ qexistsl_tac [`M64`, `M64`, `float_to_real (fp64_to_float vF1)`,
`float_to_real (fp64_to_float vF2)`, `0:real`]
\\ fs[perturb_def, mTypeToR_pos, float_to_real_round_zero_is_zero])
+ (* division, result normal *)
+ >- (fs[fp64_div_def, fp64_to_float_float_to_fp64, evalBinop_def]
+ \\ Q.ISPECL_THEN [`(fp64_to_float vF1):(52,11) float`,
+ `(fp64_to_float vF2):(52,11) float`]
+ impl_subgoal_tac
+ float_div_relative
+ >- (rpt conj_tac
+ \\ fs[validFloatValue_def,
+ normalTranslatedValue_implies_finiteness,
+ denormalTranslatedValue_implies_finiteness,
+ normalValue_implies_normalization,
+ GSYM float_is_zero_to_real, float_is_finite, evalBinop_def])
+ \\ fs[dmode_def]
+ \\ qexistsl_tac [`M64`, `M64`, `float_to_real (fp64_to_float vF1)`,
+ `float_to_real (fp64_to_float vF2)`, `e`]
+ \\ fs[perturb_def, evalBinop_def]
+ \\ imp_res_tac normal_not_denormal
+ \\ fs[mTypeToR_def, REAL_INV_1OVER])
+ (* division, result denormal *)
+ >- (fs[fp64_div_def, fp64_to_float_float_to_fp64, evalBinop_def]
+ \\ Q.ISPECL_THEN [`(fp64_to_float vF1):(52,11) float`,
+ `(fp64_to_float vF2):(52,11) float`]
+ impl_subgoal_tac
+ float_div_relative_denorm
+ >- (rpt conj_tac
+ >- fs[validFloatValue_def,
+ normalTranslatedValue_implies_finiteness,
+ denormalTranslatedValue_implies_finiteness,
+ normalValue_implies_normalization, float_is_finite,
+ GSYM float_is_zero_to_real, evalBinop_def]
+ >- fs[validFloatValue_def,
+ normalTranslatedValue_implies_finiteness,
+ denormalTranslatedValue_implies_finiteness,
+ normalValue_implies_normalization, float_is_finite,
+ GSYM float_is_zero_to_real, evalBinop_def]
+ >- fs[validFloatValue_def,
+ normalTranslatedValue_implies_finiteness,
+ denormalTranslatedValue_implies_finiteness,
+ normalValue_implies_normalization, float_is_finite,
+ GSYM float_is_zero_to_real, evalBinop_def]
+ >- (
+ fs[normalTranslatedValue_implies_finiteness,
+ denormalTranslatedValue_implies_finiteness,
+ normalValue_implies_normalization, float_is_finite,
+ GSYM float_is_zero_to_real, evalBinop_def, denormal_def, minValue_pos_def]
+ \\ rewrite_tac [INT_MAX_def, INT_MIN_def, dimindex_11, EVAL “2 ** (11 - 1) - 1 - 1â€]
+ \\ irule REAL_LT_TRANS
+ \\ asm_exists_tac \\ fs[GSYM REAL_OF_NUM_POW, minExponentPos_def]
+ \\ irule REAL_LET_TRANS \\ qexists_tac ‘1 * inv (2 pow 1022)’
+ \\ conj_tac
+ >- (rewrite_tac[real_div] \\ irule REAL_LT_RMUL_IMP \\ fs[])
+ \\ fs[])
+ >- (irule REAL_LT_TRANS \\ qexists_tac ‘maxValue M64’
+ \\ fs[threshold_64_bit_lt_maxValue, denormal_def]
+ \\ irule REAL_LTE_TRANS \\ qexists_tac ‘minValue_pos M64’
+ \\ fs[minValue_pos_def, maxValue_def, GSYM REAL_OF_NUM_POW]
+ \\ irule REAL_LE_TRANS \\ qexists_tac ‘1’ \\ conj_tac
+ >- (once_rewrite_tac[GSYM REAL_INV1] \\ irule REAL_INV_LE_ANTIMONO_IMPR
+ \\ fs[POW_2_LE1])
+ \\ fs[POW_2_LE1])
+ \\ fs[INT_MAX_def, INT_MIN_def, dimindex_11])
+ \\ fs[dmode_def]
+ \\ qexistsl_tac [`M64`, `M64`, `float_to_real (fp64_to_float vF1)`,
+ `float_to_real (fp64_to_float vF2)`, `e`]
+ \\ fs[perturb_def, evalBinop_def]
+ \\ fs[mTypeToR_def, minExponentPos_def, REAL_INV_1OVER])
+ (* division, result = 0 *)
>- (fs[fp64_div_def, dmode_def, fp64_to_float_float_to_fp64,
float_div_def, evalBinop_def]
\\ `float_to_real (fp64_to_float vF1) = 0`
- by (fs[div_eq0_general])
+ by (imp_res_tac div_eq0_general)
\\ rw_thm_asm `float_to_real (fp64_to_float vF1) = 0` (GSYM float_is_zero_to_real)
\\ fs[float_is_zero_def]
\\ Cases_on `float_value (fp64_to_float vF1)`
@@ -1117,8 +1265,9 @@ Proof
>- (simp[Once validTypes_def] \\ first_x_assum MATCH_ACCEPT_TAC)
>- (simp[Once validRanges_def] \\ find_exists_tac \\ fs[]
\\ fs[] \\ rveq \\ fs[])
- \\ irule eval_eq_env
- \\ find_exists_tac \\ fs[eval_expr_cases]
+ \\ irule eval_eq_env \\ asm_exists_tac
+ \\ conj_tac >- fs[]
+ \\ simp[Once eval_expr_cases]
\\ qexistsl_tac [`M64`, `M64`, ‘M64’, `float_to_real (fp64_to_float vF1)`,
`float_to_real (fp64_to_float vF2)`,
`float_to_real (fp64_to_float vF3)`, `0:real`]
@@ -1143,8 +1292,7 @@ Proof
(fn thm => assume_tac (ONCE_REWRITE_RULE [validErrorbound_def] thm))
\\ fs[option_case_eq]
\\ pop_assum mp_tac \\ rpt (TOP_CASE_TAC \\ fs[]))
- \\ irule eval_eq_env
- \\ find_exists_tac \\ fs[])
+ \\ irule eval_eq_env \\ asm_exists_tac \\ fs[])
\\ `validFloatValue (float_to_real (fp64_to_float vF2)) M64`
by (drule FPRangeValidator_sound
\\ disch_then
@@ -1165,8 +1313,7 @@ Proof
(fn thm => assume_tac (ONCE_REWRITE_RULE [validErrorbound_def] thm))
\\ fs[option_case_eq]
\\ pop_assum mp_tac \\ rpt (TOP_CASE_TAC \\ fs[]))
- \\ irule eval_eq_env
- \\ find_exists_tac \\ fs[])
+ \\ irule eval_eq_env \\ asm_exists_tac \\ fs[])
\\ `validFloatValue (float_to_real (fp64_to_float vF3)) M64`
by (drule FPRangeValidator_sound
\\ disch_then
@@ -1187,31 +1334,16 @@ Proof
(fn thm => assume_tac (ONCE_REWRITE_RULE [validErrorbound_def] thm))
\\ fs[option_case_eq]
\\ pop_assum mp_tac \\ rpt (TOP_CASE_TAC \\ fs[]))
- \\ irule eval_eq_env
- \\ find_exists_tac \\ fs[])
- \\ fs[optionLift_def, normal_or_zero_def]
+ \\ irule eval_eq_env \\ asm_exists_tac \\ fs[])
+ \\ qpat_x_assum ‘validFloatValue (evalFma _ _ _) _’
+ (assume_tac o SIMP_RULE std_ss [validFloatValue_def])
+ \\ fs[optionLift_def]
\\ simp[Once eval_expr_cases, PULL_EXISTS]
\\ rewrite_tac [CONJ_ASSOC]
\\ ntac 3 (once_rewrite_tac [CONJ_COMM] \\ asm_exists_tac \\ fs[])
\\ fs[evalFma_def, evalBinop_def, fp64_mul_add_def, fp64_to_float_float_to_fp64]
>- (
- `normal (evalFma (float_to_real (fp64_to_float vF1))
- (float_to_real (fp64_to_float vF2))
- (float_to_real (fp64_to_float vF3))) M64`
- by (
- rw_thm_asm `validFloatValue (_ + _) _` validFloatValue_def
- \\ fs[normal_def, denormal_def, evalFma_def, evalBinop_def]
- >- (
- `abs (float_to_real (fp64_to_float vF1) *
- float_to_real (fp64_to_float vF2) + float_to_real (fp64_to_float vF3)) <
- abs (float_to_real (fp64_to_float vF1) *
- float_to_real (fp64_to_float vF2) + float_to_real (fp64_to_float vF3))`
- suffices_by (fs[])
- \\ irule REAL_LTE_TRANS
- \\ asm_exists_tac \\ fs[])
- \\ qpat_x_assum `_ + _ = 0` (fn thm => fs[thm])
- \\ fs[maxValue_def, maxExponent_def])
- \\ Q.ISPECL_THEN [`(fp64_to_float vF1):(52,11) float`,
+ Q.ISPECL_THEN [`(fp64_to_float vF1):(52,11) float`,
`(fp64_to_float vF2):(52,11) float`,
`(fp64_to_float vF3):(52,11) float`]
impl_subgoal_tac
@@ -1227,7 +1359,55 @@ Proof
\\ qexistsl_tac [`e`]
\\ pop_assum (rewrite_tac o single)
\\ fs[perturb_def, evalBinop_def]
- \\ fs[mTypeToR_def])
+ \\ imp_res_tac normal_not_denormal
+ \\ fs[mTypeToR_def, REAL_INV_1OVER])
+ (* result denormal MARKER *)
+ >- (fs[fp64_mul_add_def, fp64_to_float_float_to_fp64, evalFma_def]
+ \\ Q.ISPECL_THEN [`(fp64_to_float vF1):(52,11) float`,
+ `(fp64_to_float vF2):(52,11) float`,
+ `(fp64_to_float vF3):(52,11) float`]
+ impl_subgoal_tac
+ float_mul_add_relative_denorm
+ >- (rpt conj_tac
+ >- fs[validFloatValue_def,
+ normalTranslatedValue_implies_finiteness,
+ denormalTranslatedValue_implies_finiteness,
+ normalValue_implies_normalization, float_is_finite,
+ GSYM float_is_zero_to_real, evalBinop_def]
+ >- fs[validFloatValue_def,
+ normalTranslatedValue_implies_finiteness,
+ denormalTranslatedValue_implies_finiteness,
+ normalValue_implies_normalization, float_is_finite,
+ GSYM float_is_zero_to_real, evalBinop_def]
+ >- fs[validFloatValue_def,
+ normalTranslatedValue_implies_finiteness,
+ denormalTranslatedValue_implies_finiteness,
+ normalValue_implies_normalization, float_is_finite,
+ GSYM float_is_zero_to_real, evalBinop_def]
+ >- (
+ fs[normalTranslatedValue_implies_finiteness,
+ denormalTranslatedValue_implies_finiteness,
+ normalValue_implies_normalization, float_is_finite,
+ GSYM float_is_zero_to_real, evalBinop_def, denormal_def, minValue_pos_def]
+ \\ rewrite_tac [INT_MAX_def, INT_MIN_def, dimindex_11, EVAL “2 ** (11 - 1) - 1 - 1â€]
+ \\ irule REAL_LT_TRANS
+ \\ asm_exists_tac \\ fs[GSYM REAL_OF_NUM_POW, minExponentPos_def]
+ \\ irule REAL_LET_TRANS \\ qexists_tac ‘1 * inv (2 pow 1022)’
+ \\ conj_tac
+ >- (rewrite_tac[real_div] \\ irule REAL_LT_RMUL_IMP \\ fs[])
+ \\ fs[])
+ >- (irule REAL_LT_TRANS \\ qexists_tac ‘maxValue M64’
+ \\ fs[threshold_64_bit_lt_maxValue, denormal_def]
+ \\ irule REAL_LTE_TRANS \\ qexists_tac ‘minValue_pos M64’
+ \\ fs[minValue_pos_def, maxValue_def, GSYM REAL_OF_NUM_POW]
+ \\ irule REAL_LE_TRANS \\ qexists_tac ‘1’ \\ conj_tac
+ >- (once_rewrite_tac[GSYM REAL_INV1] \\ irule REAL_INV_LE_ANTIMONO_IMPR
+ \\ fs[POW_2_LE1])
+ \\ fs[POW_2_LE1])
+ \\ fs[INT_MAX_def, INT_MIN_def, dimindex_11])
+ \\ fs[dmode_def] \\ qexists_tac ‘e’
+ \\ fs[perturb_def, evalFma_def]
+ \\ fs[mTypeToR_def, minExponentPos_def, REAL_INV_1OVER])
(* result = 0 *)
>- (IMP_RES_TAC validValue_gives_float_value
\\ fs[REAL_LNEG_UNIQ, evalFma_def, evalBinop_def]
@@ -1259,7 +1439,6 @@ Theorem bstep_gives_IEEE:
is64BitBstep (toRCmd f) /\
is64BitEnv Gamma /\
noDowncastFun (toRCmd f) /\
- bstep_valid f E2 /\
(∀v.
v ∈ domain dVars ⇒
∃vF m.
@@ -1272,12 +1451,12 @@ Theorem bstep_gives_IEEE:
Proof
Induct_on `f`
\\ simp [toRCmd_def, Once toREvalCmd_def, is64BitBstep_def,
- noDowncastFun_def, bstep_valid_def]
+ noDowncastFun_def]
\\ rpt strip_tac
\\ rpt (inversion `bstep (Let _ _ _ _) _ _ _ _` bstep_cases)
\\ inversion `ssa _ _ _` ssa_cases
\\ once_rewrite_tac [bstep_float_def]
- \\ fs[bstep_valid_def, noDowncast_def]
+ \\ fs[noDowncast_def]
\\ qpat_x_assum ‘validErrorboundCmd _ _ _ _’
(fn thm => mp_tac (ONCE_REWRITE_RULE[validErrorboundCmd_def] thm))
\\ fs[option_case_eq]
@@ -1577,14 +1756,14 @@ Proof
\\ res_tac
QED
-val getValidMapCmd_preserving = store_thm (
- "getValidMapCmd_preserving",
- ``! f defVars akk res.
- (! e m. FloverMapTree_find e akk = SOME m ==> m = M64) /\
- is64BitBstep f /\
- getValidMapCmd defVars f akk = Succes res /\
- (! e m. FloverMapTree_find e defVars = SOME m ==> m = M64) ==>
- ! e m. FloverMapTree_find e res = SOME m ==> m = M64``,
+Theorem getValidMapCmd_preserving:
+ ! f defVars akk res.
+ (! e m. FloverMapTree_find e akk = SOME m ==> m = M64) /\
+ is64BitBstep f /\
+ getValidMapCmd defVars f akk = Succes res /\
+ (! e m. FloverMapTree_find e defVars = SOME m ==> m = M64) ==>
+ ! e m. FloverMapTree_find e res = SOME m ==> m = M64
+Proof
Induct_on `f` \\ once_rewrite_tac [getValidMapCmd_def]
\\ rpt strip_tac \\ fs[]
>- (Cases_on `getValidMap defVars e akk` \\ fs[option_case_eq]
@@ -1604,7 +1783,8 @@ val getValidMapCmd_preserving = store_thm (
\\ find_exists_tac \\ fs[])
\\ irule getValidMap_preserving
\\ qexistsl_tac [`akk`, `defVars`, `e`, `e'`, `res`]
- \\ rpt conj_tac \\ fs[is64BitBstep_def]);
+ \\ rpt conj_tac \\ fs[is64BitBstep_def]
+QED
val IEEE_connection_expr = store_thm (
"IEEE_connection_expr",
@@ -1612,7 +1792,6 @@ val IEEE_connection_expr = store_thm (
is64BitEval (toRExp e) /\
is64BitEnv defVars /\
noDowncast (toRExp e) /\
- eval_expr_valid e E2 /\
fVars_P_sound fVars E1 P /\
(domain (usedVars (toRExp e))) SUBSET (domain fVars) /\
CertificateChecker (toRExp e) A P defVars = SOME Gamma /\
@@ -1667,7 +1846,6 @@ val IEEE_connection_cmds = store_thm (
is64BitBstep (toRCmd f) /\
is64BitEnv defVars /\
noDowncastFun (toRCmd f) /\
- bstep_valid f E2 /\
fVars_P_sound fVars E1 P /\
(domain (freeVars (toRCmd f))) SUBSET (domain fVars) /\
CertificateCheckerCmd (toRCmd f) A P defVars = SOME Gamma /\
@@ -1732,4 +1910,61 @@ val IEEE_connection_cmds = store_thm (
[`outVars`, `vR`, `vF2`, `FST iv_e`, `SND iv_e`, `err_e`, `m2`] destruct)
\\ fs[]);
+(** UNUSED:
+val normal_or_zero_def = Define `
+ normal_or_zero (v:real) =
+ (minValue_pos M64 <= abs v \/ v = 0)`;
+
+val isValid_def = Define `
+ isValid e =
+ let trans_e = optionLift e (\ v. SOME (float_to_real (fp64_to_float v))) NONE in
+ optionLift trans_e normal_or_zero F`;
+
+val eval_expr_valid_def = Define `
+ (eval_expr_valid (Var n) E = T) /\
+ (eval_expr_valid (Const m v) E = T) /\
+ (eval_expr_valid (Unop u e) E = eval_expr_valid e E) /\
+ (eval_expr_valid (Binop b e1 e2) E =
+ (eval_expr_valid e1 E /\ eval_expr_valid e2 E /\
+ let e1_res = eval_expr_float e1 E in
+ let e2_res = eval_expr_float e2 E in
+ optionLift (e1_res)
+ (\ v1. let v1_real = float_to_real (fp64_to_float v1)
+ in
+ optionLift e2_res
+ (\ v2.
+ let v2_real = float_to_real (fp64_to_float v2)
+ in
+ normal_or_zero (evalBinop b v1_real v2_real))
+ T)
+ T)) /\
+ (eval_expr_valid (Fma e1 e2 e3) E =
+ (eval_expr_valid e1 E /\ eval_expr_valid e2 E /\ eval_expr_valid e3 E /\
+ let e1_res = eval_expr_float e1 E in
+ let e2_res = eval_expr_float e2 E in
+ let e3_res = eval_expr_float e3 E in
+ optionLift (e1_res)
+ (\ v1. let v1_real = float_to_real (fp64_to_float v1)
+ in
+ optionLift e2_res
+ (\ v2.
+ let v2_real = float_to_real (fp64_to_float v2)
+ in
+ optionLift e3_res
+ (\ v3. let v3_real = float_to_real (fp64_to_float v3) in
+ normal_or_zero (evalFma v1_real v2_real v3_real))
+ T)
+ T)
+ T)) /\
+ (eval_expr_valid (Downcast m e) E = eval_expr_valid e E)`;
+
+val bstep_valid_def = Define `
+ (bstep_valid (Let m x e g) E =
+ (eval_expr_valid e E /\
+ optionLift (eval_expr_float e E)
+ (\v_e. bstep_valid g (updFlEnv x v_e E))
+ T)) /\
+ (bstep_valid (Ret e) E = eval_expr_valid e E)`;
+*)
+
val _ = export_theory ();