Commit 4ef8e1a3 authored by Heiko Becker's avatar Heiko Becker
Browse files

Prove IEEE connection with function suggested by Magnus

parent dfa6afde
......@@ -9,37 +9,60 @@ val _ = new_theory "IEEE_connection";
val _ = temp_overload_on("abs",``real$abs``);
(** FloVer assumes rounding with ties to even, thus we explicitly define
a rounding mode here **)
val dmode_def = Define `dmode = roundTiesToEven`;
val flush_def = Define `
flush real_val float_val =
if (abs real_val < minValue M64)
then SOME (float_to_fp64 (float_plus_zero (:52#11)))
else SOME float_val`;
val optionFlush_def = Define `
(optionFlush (NONE) = NONE) /\
(optionFlush (SOME v) = flush (float_to_real (fp64_to_float v)) v)`;
val eval_exp_float_def = Define `
(eval_exp_float (Var n) E = optionFlush (E n)) /\
(eval_exp_float (Const m v) E = flush (float_to_real (fp64_to_float v)) v) /\
(eval_exp_float (Var n) E = E n) /\
(eval_exp_float (Const m v) E = SOME v) /\
(eval_exp_float (Unop Neg e) E =
case eval_exp_float e E of
| SOME v => flush (- (float_to_real (fp64_to_float v))) (fp64_negate v)
| SOME v => SOME (fp64_negate v)
| _ => NONE) /\
(eval_exp_float (Unop Inv e) E = NONE) /\
(eval_exp_float (Binop b e1 e2) E =
(case (eval_exp_float e1 E), (eval_exp_float e2 E) of
| SOME v1, SOME v2 =>
let real_val = evalBinop b (float_to_real (fp64_to_float v1)) (float_to_real (fp64_to_float v2)) in
(case b of
| Plus => flush real_val (fp64_add dmode v1 v2)
| Sub => flush real_val (fp64_sub dmode v1 v2)
| Mult => flush real_val (fp64_mul dmode v1 v2)
| Div => flush real_val (fp64_div dmode v1 v2))
| _, _ => NONE) /\
(eval_exp_float (Downcast m e) E = NONE))`;
| Plus => SOME (fp64_add dmode v1 v2)
| Sub => SOME (fp64_sub dmode v1 v2)
| Mult => SOME (fp64_mul dmode v1 v2)
| Div => SOME (fp64_div dmode v1 v2))
| _, _ => NONE)) /\
(eval_exp_float (Downcast m e) E = NONE)`;
val optionLift_def = Define `
(optionLift (SOME v) some_cont none_cont = some_cont v) /\
(optionLift (NONE) some_cont none_cont = none_cont)`;
val normal_or_zero_def = Define `
normal_or_zero (v:real) =
(minValue 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_exp_valid_def = Define `
(eval_exp_valid (Var n) E = T (*isValid (eval_exp_float (Var n) E)*)) /\
(eval_exp_valid (Const m v) E = T (*isValid (eval_exp_float (Const m v) E)*)) /\
(eval_exp_valid (Unop u e) E = eval_exp_valid e E) /\
(*if eval_exp_valid e E
then isValid (eval_exp_float (Unop u e) E)
else F *)
(eval_exp_valid (Binop b e1 e2) E =
if (eval_exp_valid e1 E /\ eval_exp_valid e2 E)
then
let e1_res = eval_exp_float e1 E in
let e2_res = eval_exp_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)) F) F
else F)`;
val toRExp_def = Define `
(toRExp ((Var v):word64 exp) = Var v) /\
......@@ -390,12 +413,12 @@ val noDowncast_def = Define `
(noDowncast (Binop b e1 e2) = (noDowncast e1 /\ noDowncast e2)) /\
(noDowncast (Downcast _ _) = F)`;
val noDenormalCst_def = Define `
(noDenormalCst (Const m v) = ~ denormal (float_to_real (fp64_to_float v)) m) /\
(noDenormalCst (Var v) = T) /\
(noDenormalCst (Unop _ e) = noDenormalCst e) /\
(noDenormalCst (Binop _ e1 e2) = (noDenormalCst e1 /\ noDenormalCst e2)) /\
(noDenormalCst (Downcast _ e) = noDenormalCst e)`;
(* val noDenormalCst_def = Define ` *)
(* (noDenormalCst (Const m v) = ~ denormal (float_to_real (fp64_to_float v)) m) /\ *)
(* (noDenormalCst (Var v) = T) /\ *)
(* (noDenormalCst (Unop _ e) = noDenormalCst e) /\ *)
(* (noDenormalCst (Binop _ e1 e2) = (noDenormalCst e1 /\ noDenormalCst e2)) /\ *)
(* (noDenormalCst (Downcast _ e) = noDenormalCst e)`; *)
val is64BitEval_def = Define `
(is64BitEval ((Const m c):real exp) = (m = M64)) /\
......@@ -484,30 +507,30 @@ val typing_agrees = store_thm (
\\ qpat_x_assum `tMap (Downcast m e) = SOME _` (fn thm => fs[thm])
\\ Cases_on `tMap e` \\ fs[]));
val asFpOp_def = Define `
(asFpOp (Plus) = fp64_add dmode) /\
(asFpOp (Sub) = fp64_sub dmode) /\
(asFpOp (Mult) = fp64_mul dmode) /\
(asFpOp (Div) = fp64_div dmode)`;
val bin_eval_flushes_to_zero_def = Define `
bin_eval_flushes_to_zero =
!b e1 e2 E Gamma v1 v2 m1 m2.
eval_exp E Gamma e1 (float_to_real (fp64_to_float v1)) m1 /\
eval_exp E Gamma e2 (float_to_real (fp64_to_float v2)) m2 /\
(abs (evalBinop b (float_to_real (fp64_to_float v1)) (float_to_real (fp64_to_float v2)))) < minValue (join m1 m2)==>
eval_exp E Gamma (Binop b e1 e2) 0 (join m1 m2)`;
val neg_eval_flushes_to_zero_def = Define `
neg_eval_flushes_to_zero =
!e E Gamma v.
eval_exp E Gamma e v M64 /\
denormal v M64 ==>
eval_exp E Gamma (Unop Neg e) 0 M64`;
val no_denormal_binds_def = Define `
no_denormal_binds E =
!n v. E n = SOME v ==> ~ (denormal (float_to_real (fp64_to_float v)) M64)`;
(* val asFpOp_def = Define ` *)
(* (asFpOp (Plus) = fp64_add dmode) /\ *)
(* (asFpOp (Sub) = fp64_sub dmode) /\ *)
(* (asFpOp (Mult) = fp64_mul dmode) /\ *)
(* (asFpOp (Div) = fp64_div dmode)`; *)
(* val bin_eval_flushes_to_zero_def = Define ` *)
(* bin_eval_flushes_to_zero = *)
(* !b e1 e2 E Gamma v1 v2 m1 m2. *)
(* eval_exp E Gamma e1 (float_to_real (fp64_to_float v1)) m1 /\ *)
(* eval_exp E Gamma e2 (float_to_real (fp64_to_float v2)) m2 /\ *)
(* (abs (evalBinop b (float_to_real (fp64_to_float v1)) (float_to_real (fp64_to_float v2)))) < minValue (join m1 m2)==> *)
(* eval_exp E Gamma (Binop b e1 e2) 0 (join m1 m2)`; *)
(* val neg_eval_flushes_to_zero_def = Define ` *)
(* neg_eval_flushes_to_zero = *)
(* !e E Gamma v. *)
(* eval_exp E Gamma e v M64 /\ *)
(* denormal v M64 ==> *)
(* eval_exp E Gamma (Unop Neg e) 0 M64`; *)
(* val no_denormal_binds_def = Define ` *)
(* no_denormal_binds E = *)
(* !n v. E n = SOME v ==> ~ (denormal (float_to_real (fp64_to_float v)) M64)`; *)
val bstep_gives_IEEE = store_thm ("bstep_gives_IEEE2",
``!(e:word64 exp) E1 E2 Gamma tMap vR A P fVars dVars .
......@@ -515,15 +538,12 @@ val bstep_gives_IEEE = store_thm ("bstep_gives_IEEE2",
approxEnv E1 Gamma A fVars dVars (toREnv E2) /\
validIntervalbounds (toRExp e) A P dVars /\
validErrorbound (toRExp e) tMap A dVars /\
FPRangeValidator (toRExp e) A tMap /\
FPRangeValidator (toRExp e) A tMap dVars /\
eval_exp (toREnv E2) Gamma (toRExp e) vR M64 /\
domain (usedVars (toRExp e)) DIFF domain dVars domain fVars
is64BitEval (toRExp e) /\
noDowncast (toRExp e) /\
noDenormalCst e /\
bin_eval_flushes_to_zero /\
neg_eval_flushes_to_zero /\
no_denormal_binds E2 /\
eval_exp_valid e E2 /\
(v.
v domain fVars
vR. E1 v = SOME vR FST (P v) vR vR SND (P v))
......@@ -533,6 +553,11 @@ val bstep_gives_IEEE = store_thm ("bstep_gives_IEEE2",
vR.
E1 v = SOME vR FST (FST (A (Var v))) vR
vR SND (FST (A (Var v)))) /\
(v.
v domain dVars
vF m.
(toREnv E2 v = SOME vF tMap (Var v) = SOME m
validFloatValue vF m)) /\
(!v. v IN domain (usedVars (toRExp e)) ==> Gamma v = SOME M64) ==>
?v.
eval_exp_float e E2 = SOME v /\
......@@ -540,55 +565,48 @@ val bstep_gives_IEEE = store_thm ("bstep_gives_IEEE2",
Induct_on `e` \\ rewrite_tac[toRExp_def] \\ rpt strip_tac
\\ inversion `eval_exp _ _ _ _ _` eval_exp_cases
\\ once_rewrite_tac [eval_exp_float_def]
\\ fs[eval_exp_valid_def, isValid_def, noDowncast_def]
>- (once_rewrite_tac [toREnv_def]
\\ fs[validFloatValue_def]
\\ rveq
\\ fs[eval_exp_cases, fp64_to_float_float_to_fp64, dmode_def,
float_to_real_real_to_float_zero_id]
\\ fs[toREnv_def]
\\ Cases_on `E2 n` \\ fs[optionFlush_def, flush_def, no_denormal_binds_def]
\\ qpat_x_assum `float_to_real (fp64_to_float _) = _`
(fn thm => once_rewrite_tac[GSYM thm] \\ assume_tac (GSYM thm))
\\ first_x_assum (qspecl_then [`n`, `x`] impl_subgoal_tac)
\\ fs[denormal_def, minValue_def, minExponentPos_def, REAL_LT_INV_EQ,
fp64_to_float_float_to_fp64, zero_to_real])
\\ fs[eval_exp_float_def, optionLift_def]
\\ Cases_on `E2 n` \\ fs[optionLift_def, normal_or_zero_def])
(* \\ qpat_x_assum `float_to_real (fp64_to_float _) = _` *)
(* (fn thm => once_rewrite_tac[GSYM thm] \\ assume_tac (GSYM thm)) *)
(* \\ first_x_assum (qspecl_then [`n`, `x`] impl_subgoal_tac) *)
(* \\ fs[denormal_def, minValue_def, minExponentPos_def, REAL_LT_INV_EQ, *)
(* fp64_to_float_float_to_fp64, zero_to_real]) *)
>- (rveq \\ fs[eval_exp_cases]
\\ fs[flush_def, noDenormalCst_def, denormal_def, minValue_def,
\\ fs[optionLift_def, normal_or_zero_def, minValue_def,
minExponentPos_def, REAL_LT_INV_EQ]
\\ qexists_tac `0:real`
\\ fs[mTypeToQ_pos, perturb_def, fp64_to_float_float_to_fp64,
zero_to_real])
>- (simp [eval_exp_float_def]
\\ Cases_on `u`
\\ rveq
\\ TRY (rw_thm_asm `validErrorbound _ _ _ _` validErrorbound_def \\ fs[]
\\ Cases_on `tMap (Unop Inv (toRExp e))`
\\ Cases_on `A (Unop Inv (toRExp e))` \\ fs[] \\ FAIL_TAC "")
\\ fs[eval_exp_float_def, flush_def]
>- (fs[eval_exp_float_def, optionLift_def]
\\ first_x_assum (qspecl_then [`E1`, `E2`, `Gamma`, `tMap`, `v1`, `A`, `P`, `fVars`, `dVars`] destruct)
>- (rw_thm_asm `typeCheck _ _ _` typeCheck_def
\\ rw_thm_asm `validErrorbound _ _ _ _` validErrorbound_def
\\ rw_thm_asm `validIntervalbounds _ _ _ _` validIntervalbounds_def
\\ rw_thm_asm `FPRangeValidator _ _ _` FPRangeValidator_def
\\ rw_thm_asm `is64BitEval _` is64BitEval_def
\\ rw_thm_asm `noDenormalCst _` noDenormalCst_def
\\ rw_thm_asm `FPRangeValidator _ _ _ _` FPRangeValidator_def
\\ rw_thm_asm `domain (usedVars _) DIFF _ SUBSET _` usedVars_def
\\ rw_thm_asm `noDowncast _` noDowncast_def
\\ rw_thm_asm `is64BitEval _` is64BitEval_def
\\ fs[]
\\ Cases_on `A (Unop Neg (toRExp e))` \\ Cases_on ` A (toRExp e)` \\ fs[]
\\ Cases_on `tMap (Unop Neg (toRExp e))` \\ Cases_on `tMap (toRExp e)` \\fs[]
\\ rpt conj_tac \\ TRY (first_x_assum MATCH_ACCEPT_TAC)
\\ rpt strip_tac \\ first_x_assum irule \\ simp[Once usedVars_def])
\\ fs[fp64_negate_def, fp64_to_float_float_to_fp64]
\\ TOP_CASE_TAC \\ fs[neg_eval_flushes_to_zero_def, fp64_to_float_float_to_fp64, zero_to_real]
>- (Cases_on `float_to_real (fp64_to_float v) = 0`
>- (fs [eval_exp_cases]
\\ qexists_tac `0`
\\ fs[fp64_to_float_float_to_fp64, zero_to_real, evalUnop_def])
\\ first_x_assum drule
\\ disch_then irule \\ fs[denormal_def, float_to_real_negate, ABS_NEG])
\\ fs[eval_exp_cases] \\ qexists_tac `float_to_real (fp64_to_float v)`
\\ fs[evalUnop_def, fp64_to_float_float_to_fp64, float_to_real_negate])
\\ once_rewrite_tac [float_to_real_negate]
\\ once_rewrite_tac [eval_exp_cases]
\\ fs[] \\ once_rewrite_tac [CONJ_COMM] \\ asm_exists_tac
\\ fs[evalUnop_def])
>- (rw_thm_asm `validErrorbound _ _ _ _` validErrorbound_def \\ fs[]
\\ rveq
\\ Cases_on `tMap (Unop Inv (toRExp e))`
\\ Cases_on `A (Unop Inv (toRExp e))` \\ fs[])
>- (rename1 `Binop b (toRExp e1) (toRExp e2)`
\\ qpat_x_assum `M64 = _` (fn thm => fs [GSYM thm])
\\ `tMap (toRExp e1) = SOME M64 /\ tMap(toRExp e2) = SOME M64 /\ tMap (Binop b (toRExp e1) (toRExp e2)) = SOME M64`
......@@ -614,11 +632,10 @@ val bstep_gives_IEEE = store_thm ("bstep_gives_IEEE2",
\\ ntac 2 (first_x_assum (qspecl_then [`E1`, `E2`, `Gamma`, `tMap`] assume_tac))
\\ first_x_assum (qspecl_then [`v1`, `A`, `P`, `fVars`, `dVars`] destruct)
>- (rw_thm_asm `validErrorbound _ _ _ _` validErrorbound_def
\\ rw_thm_asm `FPRangeValidator _ _ _` FPRangeValidator_def
\\ rw_thm_asm `FPRangeValidator _ _ _ _` FPRangeValidator_def
\\ rw_thm_asm `validIntervalbounds _ _ _ _` validIntervalbounds_def
\\ rw_thm_asm `typeCheck _ _ _` typeCheck_def
\\ rw_thm_asm `is64BitEval _` is64BitEval_def
\\ rw_thm_asm `noDenormalCst _` noDenormalCst_def
\\ rw_thm_asm `domain (usedVars _) DIFF _ SUBSET _` usedVars_def
\\ rw_thm_asm `noDowncast _` noDowncast_def
\\ Cases_on `A (Binop b (toRExp e1) (toRExp e2))` \\ Cases_on `A (toRExp e1)`
......@@ -630,11 +647,10 @@ val bstep_gives_IEEE = store_thm ("bstep_gives_IEEE2",
\\ rpt strip_tac \\ first_x_assum irule \\ simp[Once usedVars_def, domain_union])
\\ first_x_assum (qspecl_then [`v2`, `A`, `P`, `fVars`, `dVars`] destruct)
>- (rw_thm_asm `validErrorbound _ _ _ _` validErrorbound_def
\\ rw_thm_asm `FPRangeValidator _ _ _` FPRangeValidator_def
\\ rw_thm_asm `FPRangeValidator _ _ _ _` FPRangeValidator_def
\\ rw_thm_asm `validIntervalbounds _ _ _ _` validIntervalbounds_def
\\ rw_thm_asm `typeCheck _ _ _` typeCheck_def
\\ rw_thm_asm `is64BitEval _` is64BitEval_def
\\ rw_thm_asm `noDenormalCst _` noDenormalCst_def
\\ rw_thm_asm `domain (usedVars _) DIFF _ SUBSET _` usedVars_def
\\ rw_thm_asm `noDowncast _` noDowncast_def
\\ Cases_on `A (Binop b (toRExp e1) (toRExp e2))` \\ Cases_on `A (toRExp e1)`
......@@ -676,7 +692,10 @@ val bstep_gives_IEEE = store_thm ("bstep_gives_IEEE2",
\\ fs [DIFF_DEF, SUBSET_DEF]
\\ rpt strip_tac \\ first_x_assum irule
\\ once_rewrite_tac [usedVars_def] \\ fs[domain_union])
\\ `contained (float_to_real (fp64_to_float vF2)) (widenInterval (FST (FST (A (toRExp e2))), SND (FST (A (toRExp e2)))) (SND(A (toRExp e2))))`
\\ `contained (float_to_real (fp64_to_float vF2))
(widenInterval
(FST (FST (A (toRExp e2))), SND (FST (A (toRExp e2))))
(SND(A (toRExp e2))))`
by (irule distance_gives_iv
\\ qexists_tac `nR2` \\ fs [contained_def, IVlo_def, IVhi_def]
\\ first_x_assum irule
......@@ -711,13 +730,12 @@ val bstep_gives_IEEE = store_thm ("bstep_gives_IEEE2",
(float_to_real (fp64_to_float vF2))`,
`M64`, `tMap`, `P`] irule)
\\ fs[]
\\ qexistsl_tac [`P`, `e1`, `e2`]
\\ qexistsl_tac [`P`, `e1`, `e2`, `tMap`]
\\ fs[]
\\ qexists_tac `tMap`
\\ simp[typeCheck_def, eval_exp_cases]
\\ rewrite_tac [CONJ_ASSOC]
\\ rpt (once_rewrite_tac [CONJ_COMM] \\ asm_exists_tac \\ fs[])
\\ qexists_tac `0:real`
\\ qexists_tac ` 0:real`
\\ Cases_on `b` \\ fs[perturb_def, evalBinop_def, mTypeToQ_pos, join_def])
\\ `validFloatValue (float_to_real (fp64_to_float vF1)) M64`
by (drule FPRangeValidator_sound
......@@ -727,11 +745,10 @@ val bstep_gives_IEEE = store_thm ("bstep_gives_IEEE2",
`float_to_real (fp64_to_float vF1)`,
`M64`, `tMap`, `P`] irule)
\\ fs[]
\\ qexistsl_tac [`P`, `e1`] \\ fs[]
\\ qexists_tac `tMap`
\\ qexistsl_tac [`P`, `e1`, `tMap`] \\ fs[]
\\ rw_thm_asm `typeCheck _ _ _` typeCheck_def
\\ rw_thm_asm `validErrorbound _ _ _ _` validErrorbound_def
\\ rw_thm_asm `FPRangeValidator _ _ _` FPRangeValidator_def
\\ rw_thm_asm `FPRangeValidator _ _ _ _` FPRangeValidator_def
\\ rw_thm_asm `validIntervalbounds _ _ _ _` validIntervalbounds_def
\\ rw_asm_star `tMap (Binop b (toRExp e1) (toRExp e2)) = SOME _`
\\ rw_asm_star `tMap (toRExp e1) = _`
......@@ -753,7 +770,7 @@ val bstep_gives_IEEE = store_thm ("bstep_gives_IEEE2",
\\ qexists_tac `tMap`
\\ rw_thm_asm `typeCheck _ _ _` typeCheck_def
\\ rw_thm_asm `validErrorbound _ _ _ _` validErrorbound_def
\\ rw_thm_asm `FPRangeValidator _ _ _` FPRangeValidator_def
\\ rw_thm_asm `FPRangeValidator _ _ _ _` FPRangeValidator_def
\\ rw_thm_asm `validIntervalbounds _ _ _ _` validIntervalbounds_def
\\ rw_asm_star `tMap (Binop b (toRExp e1) (toRExp e2)) = SOME _`
\\ rw_asm_star `tMap (toRExp e1) = _`
......@@ -766,47 +783,42 @@ val bstep_gives_IEEE = store_thm ("bstep_gives_IEEE2",
\\ simp[eval_exp_cases]
(** Case distinction for operator **)
\\ Cases_on `b` \\ fs[flush_def, PULL_EXISTS]
\\ fs[]
(* Addition *)
>- (TOP_CASE_TAC (* Case distinction whether denormal or not *)
>- (fs[fp64_to_float_float_to_fp64, zero_to_real]
\\ `eval_exp (toREnv E2) Gamma (Binop Plus (toRExp e1) (toRExp e2)) 0 M64`
by (fs[bin_eval_flushes_to_zero_def]
\\ first_x_assum
(qspecl_then [`Plus`, `toRExp e1`, `toRExp e2`,
`toREnv E2`, `Gamma`, `vF1`, `vF2`,
`M64`, `M64`]
impl_subgoal_tac)
\\ fs[asFpOp_def, join_def])
\\ inversion `eval_exp _ _ (Binop _ _ _) 0 _` eval_exp_cases
\\ qexistsl_tac [`m1`, `m2`, `v1'`, `v2'`, `delta'':real`]
\\ fs[join_def, mTypeToQ_pos, perturb_def, evalBinop_def])
\\ rw_thm_asm `validFloatValue (evalBinop _ _ _) _` validFloatValue_def
\\ fs[denormal_def]
(* normal value --> apply theorem, done ! *)
>- (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])
\\ fs[dmode_def]
\\ rename1 `abs err <= _`
\\ qexistsl_tac [`M64`, `M64`, `float_to_real (fp64_to_float vF1)`,
`float_to_real (fp64_to_float vF2)`, `err`]
\\ fs[perturb_def, evalBinop_def]
\\ fs[mTypeToQ_def, join_def])
(* denormal case -> show that we can make the value normal again *)
>- (fs[])
\\ fs[REAL_LNEG_UNIQ, evalBinop_def]
\\ fs[fp64_add_def, dmode_def, fp64_to_float_float_to_fp64]
\\ fs[float_add_def]
\\ Cases_on `b` \\ fs[optionLift_def, PULL_EXISTS, normal_or_zero_def]
(* 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]
\\ rename1 `abs err <= _`
\\ qexistsl_tac [`M64`, `M64`, `float_to_real (fp64_to_float vF1)`,
`float_to_real (fp64_to_float vF2)`, `err`]
\\ fs[perturb_def, evalBinop_def]
\\ fs[mTypeToQ_def, join_def])
(* result = 0 *)
>- (fs[REAL_LNEG_UNIQ, evalBinop_def]
\\ fs[fp64_add_def, dmode_def, fp64_to_float_float_to_fp64]
\\ fs[float_add_def]
\\ fs[join_def]
\\ qexistsl_tac [`M64`, `M64`, `float_to_real (fp64_to_float vF1)`, `float_to_real (fp64_to_float vF2)`, `0:real`]
\\ fs[perturb_def, mTypeToQ_pos, evalBinop_def]
......@@ -814,25 +826,23 @@ val bstep_gives_IEEE = store_thm ("bstep_gives_IEEE2",
\\ `2 * abs (0:real) <= ulp (:52 #11)`
by (fs[ulp_def, ULP_def])
\\ fs[ float_to_real_round_zero_is_zero])
(* Subtraction *)
>- (TOP_CASE_TAC (* Case distinction whether denormal or not *)
>- (fs[fp64_to_float_float_to_fp64, zero_to_real]
\\ `eval_exp (toREnv E2) Gamma (Binop Sub (toRExp e1) (toRExp e2)) 0 M64`
by (fs[bin_eval_flushes_to_zero_def]
\\ first_x_assum
(qspecl_then [`Sub`, `toRExp e1`, `toRExp e2`,
`toREnv E2`, `Gamma`, `vF1`, `vF2`,
`M64`, `M64`]
impl_subgoal_tac)
\\ fs[asFpOp_def, join_def])
\\ inversion `eval_exp _ _ (Binop _ _ _) 0 _` eval_exp_cases
\\ qexistsl_tac [`m1`, `m2`, `v1'`, `v2'`, `delta'':real`]
\\ fs[join_def, mTypeToQ_pos, perturb_def, evalBinop_def])
\\ rw_thm_asm `validFloatValue (evalBinop _ _ _) _` validFloatValue_def
\\ fs[denormal_def]
(* normal value --> apply theorem, done ! *)
>- (fs[fp64_sub_def, fp64_to_float_float_to_fp64, evalBinop_def]
\\ Q.ISPECL_THEN [`(fp64_to_float vF1):(52,11) float`,
(* 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
......@@ -841,16 +851,15 @@ val bstep_gives_IEEE = store_thm ("bstep_gives_IEEE2",
normalTranslatedValue_implies_finiteness,
denormalTranslatedValue_implies_finiteness,
normalValue_implies_normalization,
GSYM float_is_zero_to_real, float_is_finite])
GSYM float_is_zero_to_real, float_is_finite, evalBinop_def])
\\ fs[dmode_def]
\\ rename1 `abs err <= _`
\\ qexistsl_tac [`M64`, `M64`, `float_to_real (fp64_to_float vF1)`,
`float_to_real (fp64_to_float vF2)`, `err`]
\\ fs[perturb_def, evalBinop_def]
\\ fs[mTypeToQ_def, join_def])
(* denormal case -> show that we can make the value normal again *)
>- (fs[])
\\ pop_assum MP_TAC
>- (fs[evalBinop_def]
\\ qpat_x_assum `float_to_real (fp64_to_float _) = _` MP_TAC
\\ simp[real_sub, REAL_LNEG_UNIQ, evalBinop_def]
\\ fs[fp64_sub_def, dmode_def, fp64_to_float_float_to_fp64]
\\ fs[float_sub_def]
......@@ -865,42 +874,41 @@ val bstep_gives_IEEE = store_thm ("bstep_gives_IEEE2",
by (fs[ulp_def, ULP_def])
\\ fs[ float_to_real_round_zero_is_zero])
(* Multiplication *)
>- (TOP_CASE_TAC (* Case distinction whether denormal or not *)
>- (fs[fp64_to_float_float_to_fp64, zero_to_real]
\\ `eval_exp (toREnv E2) Gamma (Binop Mult (toRExp e1) (toRExp e2)) 0 M64`
by (fs[bin_eval_flushes_to_zero_def]
\\ first_x_assum
(qspecl_then [`Mult`, `toRExp e1`, `toRExp e2`,
`toREnv E2`, `Gamma`, `vF1`, `vF2`,
`M64`, `M64`]
impl_subgoal_tac)
\\ fs[asFpOp_def, join_def])
\\ inversion `eval_exp _ _ (Binop _ _ _) 0 _` eval_exp_cases
\\ qexistsl_tac [`m1`, `m2`, `v1'`, `v2'`, `delta'':real`]
\\ fs[join_def, mTypeToQ_pos, perturb_def, evalBinop_def])
\\ rw_thm_asm `validFloatValue (evalBinop _ _ _) _` validFloatValue_def
\\ fs[denormal_def]
(* normal value --> apply theorem, done ! *)
>- (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
>- (rpt conj_tac
\\ fs[validFloatValue_def,
>- (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
float_mul_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])
GSYM float_is_zero_to_real, float_is_finite, evalBinop_def])
\\ fs[dmode_def]
\\ rename1 `abs err <= _`
\\ qexistsl_tac [`M64`, `M64`, `float_to_real (fp64_to_float vF1)`,
`float_to_real (fp64_to_float vF2)`, `err`]
\\ fs[perturb_def, evalBinop_def]
\\ fs[mTypeToQ_def, join_def])
(* denormal case -> show that we can make the value normal again *)
>- (fs[])
\\ fs[evalBinop_def, REAL_ENTIRE, fp64_mul_def, float_mul_def,
>- (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)`,
Cases_on `float_value (fp64_to_float vF2)`]
......@@ -917,23 +925,20 @@ val bstep_gives_IEEE = store_thm ("bstep_gives_IEEE2",
\\ rveq
\\ fs[GSYM float_is_zero_to_real, float_is_zero_def, join_def, mTypeToQ_pos])
(* Division *)
>- (TOP_CASE_TAC (* Case distinction whether denormal or not *)
>- (fs[fp64_to_float_float_to_fp64, zero_to_real]
\\ `eval_exp (toREnv E2) Gamma (Binop Div (toRExp e1) (toRExp e2)) 0 M64`
by (fs[bin_eval_flushes_to_zero_def]
\\ first_x_assum
(qspecl_then [`Div`, `toRExp e1`, `toRExp e2`,
`toREnv E2`, `Gamma`, `vF1`, `vF2`,
`M64`, `M64`]
impl_subgoal_tac)
\\ fs[asFpOp_def, join_def])
\\ inversion `eval_exp _ _ (Binop _ _ _) 0 _` eval_exp_cases
\\ qexistsl_tac [`m1`, `m2`, `v1'`, `v2'`, `delta'':real`]
\\ fs[join_def, mTypeToQ_pos, perturb_def, evalBinop_def])
\\ rw_thm_asm `validFloatValue (evalBinop _ _ _) _` validFloatValue_def
\\ fs[denormal_def]
(* normal value --> apply theorem, done ! *)
>- (fs[fp64_div_def, fp64_to_float_float_to_fp64, evalBinop_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`,
`(fp64_to_float vF2):(52,11