Commit 2e3a7e7e authored by Heiko Becker's avatar Heiko Becker

Implement and prove correct new type inferencer in HOL4

parent 4ccb040c
......@@ -40,12 +40,7 @@ val updEnv_def = Define `
val noDivzero_def = Define `noDivzero (a:real) (b:real) = (a < &0 \/ &0 < b)`;
val updDefVars_def = Define `
updDefVars (x:num) (m:mType) (defVars:num -> mType option) (y:num) :mType option =
if y = x then SOME m else defVars y`;
val _ = export_rewrites ["IVlo_def", "IVhi_def",
"emptyEnv_def", "updEnv_def",
"updDefVars_def"]
"emptyEnv_def", "updEnv_def"]
val _ = export_theory();
......@@ -2,7 +2,8 @@
Formalization of the Abstract Syntax Tree of a subset used in the Flover framework
**)
open simpLib realTheory realLib RealArith
open AbbrevsTheory ExpressionsTheory ExpressionAbbrevsTheory MachineTypeTheory
open AbbrevsTheory ExpressionsTheory ExpressionAbbrevsTheory
ExpressionSemanticsTheory MachineTypeTheory;
open preamble
val _ = new_theory "Commands";
......@@ -27,21 +28,21 @@ val toREvalCmd_def = Define `
result value
**)
val (bstep_rules, bstep_ind, bstep_cases) = Hol_reln `
(!m m' x e s E v res Gamma fBits.
eval_expr E Gamma fBits e v m /\
bstep s (updEnv x v E) (updDefVars x m Gamma) fBits res m' ==>
bstep (Let m x e s) E Gamma fBits res m') /\
(!m e E v Gamma fBits.
eval_expr E Gamma fBits e v m ==>
bstep (Ret e) E Gamma fBits v m)`;
(!m m' x e s E v res Gamma.
eval_expr E Gamma e v m /\
bstep s (updEnv x v E) Gamma res m' ==>
bstep (Let m x e s) E Gamma res m') /\
(!m e E v Gamma.
eval_expr E Gamma e v m ==>
bstep (Ret e) E Gamma v m)`;
(**
Generate a better case lemma again
Generate a better case lemma
**)
val bstep_cases =
map (GEN_ALL o SIMP_CONV (srw_ss()) [Once bstep_cases])
[``bstep (Let m x e s) E defVars fBits vR m'``,
``bstep (Ret e) E defVars fBits vR m``]
[``bstep (Let m x e s) E defVars vR m'``,
``bstep (Ret e) E defVars vR m``]
|> LIST_CONJ |> curry save_thm "bstep_cases";
val [let_b, ret_b] = CONJ_LIST 2 bstep_rules;
......@@ -69,10 +70,10 @@ val definedVars_def = Define `
val bstep_eq_env = store_thm (
"bstep_eq_env",
``!f E1 E2 Gamma v m fBits.
``!f E1 E2 Gamma v m.
(!x. E1 x = E2 x) /\
bstep f E1 Gamma fBits v m ==>
bstep f E2 Gamma fBits v m``,
bstep f E1 Gamma v m ==>
bstep f E2 Gamma v m``,
Induct \\ rpt strip_tac \\ fs[bstep_cases]
>- (qexists_tac `v'` \\ conj_tac
\\ TRY (drule eval_eq_env \\ disch_then drule \\ fs[] \\ FAIL_TAC"")
......@@ -80,4 +81,26 @@ val bstep_eq_env = store_thm (
\\ rpt strip_tac \\ fs[updEnv_def])
\\ irule eval_eq_env \\ asm_exists_tac \\ fs[]);
val swap_Gamma_bstep = store_thm (
"swap_Gamma_bstep",
``!f E vR m Gamma1 Gamma2.
(! e. Gamma1 e = Gamma2 e) /\
bstep f E Gamma1 vR m ==>
bstep f E Gamma2 vR m``,
Induct_on `f` \\ rpt strip_tac \\ fs[bstep_cases]
\\ metis_tac [swap_Gamma_eval_expr]);
val bstep_Gamma_det = store_thm (
"bstep_Gamma_det",
``!f E1 E2 Gamma v1 v2 m1 m2.
bstep f E1 Gamma v1 m1 /\
bstep f E2 Gamma v2 m2 ==>
m1 = m2``,
Induct_on `f` \\ rpt strip_tac \\ fs[bstep_cases]
\\ metis_tac[Gamma_det]);
val getRetExp_def = Define `
(getRetExp (Let m x e g) = getRetExp g) /\
(getRetExp (Ret e) = e)`;
val _ = export_theory ();
open simpLib realTheory realLib RealArith sptreeTheory
open AbbrevsTheory ExpressionAbbrevsTheory RealSimpsTheory CommandsTheory FloverTactics FloverMapTheory
open preamble
open simpLib realTheory realLib RealArith sptreeTheory;
open AbbrevsTheory ExpressionAbbrevsTheory RealSimpsTheory CommandsTheory
FloverTactics FloverMapTheory;
open preamble;
val _ = new_theory "Environments";
val _ = temp_overload_on("abs",``real$abs``);
val (approxEnv_rules, approxEnv_ind, approxEnv_cases) = Hol_reln `
(!(defVars: num -> mType option) (A:analysisResult).
approxEnv emptyEnv defVars A LN LN emptyEnv) /\
(!(E1:env) (E2:env) (defVars: num -> mType option) (A:analysisResult) (fVars:num_set) (dVars:num_set) v1 v2 x.
approxEnv E1 defVars A fVars dVars E2 /\
(defVars x = SOME m) /\
(!(Gamma: real expr -> mType option) (A:analysisResult).
approxEnv emptyEnv Gamma A LN LN emptyEnv) /\
(!(E1:env) (E2:env) (Gamma: real expr -> mType option) (A:analysisResult)
(fVars:num_set) (dVars:num_set) v1 v2 x.
approxEnv E1 Gamma A fVars dVars E2 /\
(Gamma (Var x) = SOME m) /\
(abs (v1 - v2) <= computeError v1 m) /\
(lookup x (union fVars dVars) = NONE) ==>
approxEnv (updEnv x v1 E1) (updDefVars x m defVars) A (insert x () fVars) dVars (updEnv x v2 E2)) /\
(!(E1:env) (E2:env) (defVars: num -> mType option) (A:analysisResult)
approxEnv (updEnv x v1 E1)
Gamma A (insert x () fVars) dVars
(updEnv x v2 E2)) /\
(!(E1:env) (E2:env) (Gamma: real expr -> mType option) (A:analysisResult)
(fVars:num_set) (dVars:num_set) v1 v2 x iv err.
approxEnv E1 defVars A fVars dVars E2 /\
FloverMapTree_find (Var x) A = SOME (iv, err) /\
approxEnv E1 Gamma A fVars dVars E2 /\
Gamma (Var x) = SOME m /\
FloverMapTree_find (Var x) A = SOME (iv,err) /\
abs (v1 - v2) <= err /\
(lookup x (union fVars dVars) = NONE) ==>
approxEnv (updEnv x v1 E1) (updDefVars x m defVars) A fVars (insert x () dVars) (updEnv x v2 E2))`;
approxEnv (updEnv x v1 E1)
Gamma A fVars (insert x () dVars)
(updEnv x v2 E2))`;
val [approxRefl, approxUpdFree, approxUpdBound] = CONJ_LIST 3 approxEnv_rules;
save_thm ("approxRefl", approxRefl);
......@@ -57,7 +64,7 @@ val approxEnv_fVar_bounded = store_thm (
E1 x = SOME v /\
E2 x = SOME v2 /\
x IN (domain fVars) /\
Gamma x = SOME m ==>
Gamma (Var x) = SOME m ==>
abs (v - v2) <= computeError v m``,
rpt strip_tac
\\ qspec_then
......@@ -66,7 +73,7 @@ val approxEnv_fVar_bounded = store_thm (
E1 x = SOME v /\
E2 x = SOME v2 /\
x IN (domain fVars) /\
Gamma x = SOME m ==>
Gamma (Var x) = SOME m ==>
abs (v - v2) <= computeError v m`
(fn thm => irule (SIMP_RULE std_ss [] thm))
approxEnv_ind
......@@ -74,16 +81,12 @@ val approxEnv_fVar_bounded = store_thm (
>- (fs [])
>- (fs []
\\ EVERY_CASE_TAC \\ rveq \\ fs[lookup_union, domain_lookup]
\\ first_x_assum irule \\ fs[]
\\ rename1 `defVars x2 = SOME m2`
\\ qexists_tac `x2` \\ fs[updDefVars_def])
\\ first_x_assum drule \\ fs[])
>- (fs []
\\ rveq \\ fs[]
\\ EVERY_CASE_TAC
\\ rveq \\ fs[]
\\ first_x_assum irule \\ fs[]
\\ rename1 `defVars x1 = SOME m1` \\ qexists_tac `x1`
\\ fs[])
\\ first_x_assum drule \\ fs[])
\\ qexistsl_tac [`E1`, `Gamma`, `absenv`, `fVars`, `dVars`, `E2`, `x`]
\\ fs[]);
......@@ -93,7 +96,7 @@ val approxEnv_dVar_bounded = store_thm ("approxEnv_dVar_bounded",
E1 x = SOME v /\
E2 x = SOME v2 /\
x IN (domain dVars) /\
Gamma x = SOME m /\
Gamma (Var x) = SOME m /\
FloverMapTree_find (Var x) A = SOME (iv, e) ==>
abs (v - v2) <= e``,
rpt strip_tac
......@@ -103,7 +106,7 @@ val approxEnv_dVar_bounded = store_thm ("approxEnv_dVar_bounded",
E1 x = SOME v /\
E2 x = SOME v2 /\
x IN (domain dVars) /\
Gamma x = SOME m /\
Gamma (Var x) = SOME m /\
FloverMapTree_find (Var x) A = SOME (iv, e) ==>
abs (v - v2) <= e`
(fn thm => destruct (SIMP_RULE std_ss [] thm))
......@@ -113,14 +116,10 @@ val approxEnv_dVar_bounded = store_thm ("approxEnv_dVar_bounded",
>- (rpt strip_tac \\ fs [updEnv_def]
\\ EVERY_CASE_TAC \\ rveq \\ fs[lookup_union, domain_lookup]
>- (EVERY_CASE_TAC \\ fs[])
\\ first_x_assum irule \\ fs[updDefVars_def]
\\ rename1 `defVars x2 = SOME m2` \\ qexistsl_tac [`m2`, `x2`]
\\ fs[])
\\ first_x_assum drule \\ fs[])
>- (rpt strip_tac \\ fs [updEnv_def, updDefVars_def] \\ rveq \\ fs[]
\\ EVERY_CASE_TAC \\ rveq \\ fs[]
\\ first_x_assum irule \\ fs[]
\\ rename1 `defVars x1 = SOME m1` \\ qexistsl_tac [`m1`,`x1`]
\\ fs[]))
\\ first_x_assum drule \\ fs[]))
\\ first_x_assum drule
\\ rpt (disch_then drule)
\\ disch_then MATCH_ACCEPT_TAC);
......
(**
Some abbreviations that require having defined exprressions beforehand
If we would put them in the Abbrevs file, this would create a circular dependency which HOL4 cannot resolve.
Some abbreviations that require having defined expressions beforehand
If we would put them in the Abbrevs file, this would create a circular
dependency
**)
open FloverMapTheory
open preamble
open FloverMapTheory ExpressionsTheory;
open preamble;
val _ = new_theory "ExpressionAbbrevs";
......@@ -12,12 +13,58 @@ We treat a function mapping an exprression arguing on fractions as value type
to pairs of intervals on rationals and rational errors as the analysis result
**)
val _ = type_abbrev ("typeMap", ``:(real expr # mType) binTree``);
val _ = type_abbrev ("bitMap", ``:(real expr # num) binTree``);
val _ = type_abbrev ("analysisResult", ``:(real expr # ((real # real) # real)) binTree``);
val _ = type_abbrev ("fMap", ``:(real expr # 'a) binTree``);
val _ = type_abbrev ("typeMap", ``:mType fMap``);
val _ = type_abbrev ("analysisResult", ``:((real # real) # real) fMap``);
val toRBMap_def = Define `
toRBMap (fBits:bitMap) =
\e. FloverMapTree_find e fBits`;
val updDefVars_def = Define `
updDefVars (x:real expr) (m:mType) (defVars:real expr -> mType option) (y:real expr) :mType option =
if y = x then SOME m else defVars y`;
val toRExpMap_def = Define `
toRExpMap (tMap:typeMap) =
\e. FloverMapTree_find e tMap`;
val toRTMap_def = Define `
toRTMap Gamma (Var v) =
(case Gamma (Var v) of
|SOME m => SOME REAL
|_ => NONE) /\
toRTMap tMap e = SOME REAL`;
val no_cycle_unop = store_thm (
"no_cycle_unop",
``!e u. e <> Unop u e``,
Induct_on `e` \\ fs[expr_distinct]);
val no_cycle_cast = store_thm (
"no_cycle_cast",
``!e m. e <> Downcast m e``,
Induct_on `e` \\ fs[expr_distinct])
val no_cycle_binop_left = store_thm (
"no_cycle_binop_left",
``!e1 e2 b. e1 <> Binop b e1 e2``,
Induct_on `e1` \\ fs[expr_distinct]);
val no_cycle_binop_right = store_thm (
"no_cycle_binop_right",
``!e1 e2 b. e2 <> Binop b e1 e2``,
Induct_on `e2` \\ fs[expr_distinct]);
val no_cycle_fma_left = store_thm (
"no_cycle_fma_left",
``!e1 e2 e3. e1 <> Fma e1 e2 e3``,
Induct_on `e1` \\ fs[expr_distinct]);
val no_cycle_fma_center = store_thm (
"no_cycle_fma_center",
``!e1 e2 e3. e2 <> Fma e1 e2 e3``,
Induct_on `e2` \\ fs[expr_distinct]);
val no_cycle_fma_right = store_thm (
"no_cycle_fma_right",
``!e1 e2 e3. e3 <> Fma e1 e2 e3``,
Induct_on `e3` \\ fs[expr_distinct]);
val _ = export_theory()
(**
Formalization of the base expression language for the flover framework
**)
open miscTheory realTheory realLib sptreeTheory
open AbbrevsTheory MachineTypeTheory FloverTactics ExpressionsTheory
open ExpressionAbbrevsTheory
open preamble
val _ = new_theory "ExpressionSemantics";
val _ = temp_overload_on("abs",``real$abs``);
(**
Define a perturbation function to ease writing of basic definitions
**)
val perturb_def = Define `
(* The Real-type has no error *)
perturb (rVal:real) (REAL) (delta:real) = rVal /\
(* Fixed-point numbers have an absolute error *)
perturb rVal (F w f) delta = rVal + delta /\
(* Floating-point numbers have a relative error *)
perturb rVal _ delta = rVal * (1 + delta)`;
(**
Define exprression evaluation relation parametric by an "error" epsilon.
The result value exprresses float computations according to the IEEE standard,
using a perturbation of the real valued computation by (1 + delta), where
|delta| <= machine epsilon.
**)
val (eval_expr_rules, eval_expr_ind, eval_expr_cases) = Hol_reln `
(!E Gamma m x v.
Gamma (Var x) = SOME m /\
E x = SOME v ==>
eval_expr E Gamma (Var x) v m) /\
(!E Gamma m n delta.
abs delta <= (mTypeToR m) ==>
eval_expr E Gamma (Const m n) (perturb n m delta) m) /\
(!E Gamma m mN f1 v1.
Gamma (Unop Neg f1) = SOME mN /\
isCompat m mN /\
eval_expr E Gamma f1 v1 m ==>
eval_expr E Gamma (Unop Neg f1) (evalUnop Neg v1) mN) /\
(!E Gamma m mN f1 v1 delta.
Gamma (Unop Inv f1) = SOME mN /\
isCompat m mN /\
abs delta <= (mTypeToR m) /\
eval_expr E Gamma f1 v1 m /\
(v1 <> 0) ==>
eval_expr E Gamma (Unop Inv f1) (perturb (evalUnop Inv v1) m delta) mN) /\
(!E Gamma m m1 f1 v1 delta.
Gamma (Downcast m f1) = SOME m /\
isMorePrecise m1 m /\
abs delta <= (mTypeToR m) /\
eval_expr E Gamma f1 v1 m1 ==>
eval_expr E Gamma (Downcast m f1) (perturb v1 m delta) m) /\
(!E Gamma m1 m2 m op f1 f2 v1 v2 delta.
Gamma (Binop op f1 f2) = SOME m /\
isJoin m1 m2 m /\
abs delta <= (mTypeToR m) /\
eval_expr E Gamma f1 v1 m1 /\
eval_expr E Gamma f2 v2 m2 /\
((op = Div) ==> (v2 <> 0)) ==>
eval_expr E Gamma (Binop op f1 f2) (perturb (evalBinop op v1 v2) m delta) m) /\
(!E Gamma m1 m2 m3 m f1 f2 f3 v1 v2 v3 delta.
Gamma (Fma f1 f2 f3) = SOME m /\
isJoin3 m1 m2 m3 m /\
abs delta <= (mTypeToR m) /\
eval_expr E Gamma f1 v1 m1 /\
eval_expr E Gamma f2 v2 m2 /\
eval_expr E Gamma f3 v3 m3 ==>
eval_expr E Gamma (Fma f1 f2 f3) (perturb (evalFma v1 v2 v3) m delta) m)`;
val eval_expr_cases_old = save_thm ("eval_expr_cases_old", eval_expr_cases);
(**
Generate a better case lemma
**)
val eval_expr_cases =
map (GEN_ALL o SIMP_CONV (srw_ss()) [Once eval_expr_cases])
[``eval_expr E Gamma (Var v) res m``,
``eval_expr E Gamma (Const m1 n) res m2``,
``eval_expr E Gamma (Unop u e) res m``,
``eval_expr E Gamma (Binop n e1 e2) res m``,
``eval_expr E Gamma (Fma e1 e2 e3) res m``,
``eval_expr E Gamma (Downcast m1 e1) res m2``]
|> LIST_CONJ |> curry save_thm "eval_expr_cases";
val [Var_load, Const_dist, Unop_neg, Unop_inv, Downcast_dist, Binop_dist, Fma_dist] =
CONJ_LIST 7 eval_expr_rules;
save_thm ("Var_load", Var_load);
save_thm ("Const_dist", Const_dist);
save_thm ("Unop_neg", Unop_neg);
save_thm ("Unop_inv", Unop_inv);
save_thm ("Binop_dist", Binop_dist);
save_thm ("Fma_dist", Fma_dist);
save_thm ("Downcast_dist", Downcast_dist);
(**
Show some simpler (more general) rule lemmata
**)
val Const_dist' = store_thm (
"Const_dist'",
``!m n delta v m' E Gamma.
(abs delta) <= (mTypeToR m) /\
v = perturb n m delta /\
m' = m ==>
eval_expr E Gamma (Const m n) v m'``,
fs [Const_dist]);
val Unop_neg' = store_thm (
"Unop_neg'",
``!m f1 v1 v m' mN E Gamma.
eval_expr E Gamma f1 v1 m /\
v = evalUnop Neg v1 /\
Gamma (Unop Neg f1) = SOME mN /\
isCompat m mN /\
m' = mN ==>
eval_expr E Gamma (Unop Neg f1) v m'``,
rpt strip_tac \\ rveq \\ irule Unop_neg \\ fs[]
\\ asm_exists_tac \\ fs[]);
val Unop_inv' = store_thm (
"Unop_inv'",
``!m f1 v1 delta v m' mN E Gamma fBits.
(abs delta) <= (mTypeToR m) /\
eval_expr E Gamma f1 v1 m /\
(v1 <> 0) /\
v = perturb (evalUnop Inv v1) m delta /\
Gamma (Unop Inv f1) = SOME mN /\
isCompat m mN /\
m' = mN ==>
eval_expr E Gamma (Unop Inv f1) v m'``,
rpt strip_tac \\ rveq \\ irule Unop_inv \\ fs[]);
val Downcast_dist' = store_thm ("Downcast_dist'",
``!m m1 f1 v1 delta v m' E Gamma fBits.
isMorePrecise m1 m /\
(abs delta) <= (mTypeToR m) /\
eval_expr E Gamma f1 v1 m1 /\
v = perturb v1 m delta /\
Gamma (Downcast m f1) = SOME m /\
m' = m ==>
eval_expr E Gamma (Downcast m f1) v m'``,
rpt strip_tac
\\ rw []
\\ irule Downcast_dist
\\ fs[] \\ qexists_tac `m1` \\ fs[]);
val Binop_dist' = store_thm ("Binop_dist'",
``!m1 m2 op f1 f2 v1 v2 delta v m m' E Gamma fBit.
(abs delta) <= (mTypeToR m') /\
eval_expr E Gamma f1 v1 m1 /\
eval_expr E Gamma f2 v2 m2 /\
((op = Div) ==> (v2 <> 0)) /\
v = perturb (evalBinop op v1 v2) m' delta /\
Gamma (Binop op f1 f2) = SOME m /\
isJoin m1 m2 m /\
m = m' ==>
eval_expr E Gamma (Binop op f1 f2) v m'``,
rpt strip_tac \\ rveq
\\ irule Binop_dist \\ fs[]
\\ asm_exists_tac \\ fs[]);
val Fma_dist' = store_thm ("Fma_dist'",
``!m1 m2 m3 f1 f2 f3 v1 v2 v3 delta v m m' E Gamma fBit.
(abs delta) <= (mTypeToR m') /\
eval_expr E Gamma f1 v1 m1 /\
eval_expr E Gamma f2 v2 m2 /\
eval_expr E Gamma f3 v3 m3 /\
v = perturb (evalFma v1 v2 v3) m' delta /\
Gamma (Fma f1 f2 f3) = SOME m /\
isJoin3 m1 m2 m3 m /\
m' = m ==>
eval_expr E Gamma (Fma f1 f2 f3) v m'``,
rpt strip_tac \\ rveq
\\ irule Fma_dist \\ fs[]
\\ asm_exists_tac \\ fs[]);
val Gamma_det = store_thm (
"Gamma_det",
``!e1 e2 E1 E2 Gamma v1 v2 m1 m2.
eval_expr E1 Gamma e1 v1 m1 /\
e1 = e2 /\
eval_expr E2 Gamma e2 v2 m2 ==>
m1 = m2``,
Induct_on `e1` \\ rpt strip_tac \\ fs[eval_expr_cases]
\\ rveq \\ fs[eval_expr_cases]
\\ fs[]);
val toRTMap_eval_REAL = store_thm (
"toRTMap_eval_REAL",
``!e v E Gamma m.
eval_expr E (toRTMap Gamma) (toREval e) v m ==> m = REAL``,
Induct_on `e` \\ rpt strip_tac \\ fs[toREval_def]
\\ inversion `eval_expr _ _ _ _ _` eval_expr_cases
\\ fs[toRTMap_def, option_case_eq]
\\ res_tac \\ fs[]);
(**
If |delta| <= 0 then perturb v delta is exactly v.
**)
val delta_0_deterministic = store_thm(
"delta_0_deterministic",
``!(v:real) (m:mType) (delta:real).
abs delta <= 0 ==> perturb v m delta = v``,
Cases_on `m` \\
fs [perturb_def,ABS_BOUNDS,REAL_LE_ANTISYM]);
val delta_REAL_deterministic = store_thm(
"delta_REAL_deterministic",
``!(v:real) (m:mType) (delta:real).
abs delta <= mTypeToR REAL ==> perturb v m delta = v``,
Cases_on `m` \\ fs[mTypeToR_def, delta_0_deterministic]);
(**
Evaluation with 0 as machine epsilon is deterministic
**)
val meps_0_deterministic = store_thm("meps_0_deterministic",
``!(f: real expr) v1:real v2:real E defVars fBits.
eval_expr E (toRTMap defVars) (toREval f) v1 REAL /\
eval_expr E (toRTMap defVars) (toREval f) v2 REAL ==>
v1 = v2``,
Induct_on `f` \\ fs[toREval_def] \\ rpt strip_tac \\ fs[eval_expr_cases]
\\ rveq \\ fs[delta_REAL_deterministic]
>- (IMP_RES_TAC toRTMap_eval_REAL \\ rveq \\ res_tac \\ fs[])
>- (IMP_RES_TAC toRTMap_eval_REAL \\ rveq \\ res_tac
\\ fs[delta_REAL_deterministic])
>- (IMP_RES_TAC toRTMap_eval_REAL \\ rveq \\ res_tac
\\ fs[delta_REAL_deterministic])
>- (IMP_RES_TAC toRTMap_eval_REAL \\ rveq \\ res_tac
\\ fs[delta_REAL_deterministic])
\\ IMP_RES_TAC toRTMap_eval_REAL \\ rveq \\ res_tac
\\ fs[delta_REAL_deterministic]);
(**
Helping lemmas. Needed in soundness proof.
For each evaluation of using an arbitrary epsilon, we can replace it by
evaluating the subExpressions and then binding the result values to different
variables in the Environment.
**)
val binary_unfolding = store_thm("binary_unfolding",
``!(b:binop) (f1:(real)expr) (f2:(real)expr) E Gamma v1 v2 m1 m2 delta m.
(b = Div ==> (v2 <> 0)) /\
(abs delta) <= (mTypeToR m) /\
eval_expr E Gamma f1 v1 m1 /\
eval_expr E Gamma f2 v2 m2 /\
eval_expr E Gamma (Binop b f1 f2) (perturb (evalBinop b v1 v2) m delta) m ==>
eval_expr (updEnv 2 v2 (updEnv 1 v1 emptyEnv))
(updDefVars (Binop b (Var 1) (Var 2)) m (updDefVars (Var 2) m2 (updDefVars (Var 1) m1 Gamma)))
(Binop b (Var 1) (Var 2)) (perturb (evalBinop b v1 v2) m delta) m``,
fs [updEnv_def,updDefVars_def,join_fl_def,eval_expr_cases,APPLY_UPDATE_THM,PULL_EXISTS]
\\ rpt strip_tac
\\ qexists_tac `delta'` \\ fs[]
\\ IMP_RES_TAC Gamma_det \\ fs[]);
val fma_unfolding = store_thm("fma_unfolding",
``!(f1:(real)expr) (f2:(real)expr) (f3:(real)expr) E Gamma (v:real) v1 v2 v3
m1 m2 m3 delta fBit m.
(abs delta) <= (mTypeToR m) /\
eval_expr E Gamma f1 v1 m1 /\
eval_expr E Gamma f2 v2 m2 /\
eval_expr E Gamma f3 v3 m3 /\
eval_expr E Gamma (Fma f1 f2 f3) (perturb (evalFma v1 v2 v3) m delta) m ==>
eval_expr (updEnv 3 v3 (updEnv 2 v2 (updEnv 1 v1 emptyEnv)))
(updDefVars (Fma (Var 1) (Var 2) (Var 3)) m
(updDefVars (Var 3) m3 (updDefVars (Var 2) m2 (updDefVars (Var 1) m1 Gamma))))
(Fma (Var 1) (Var 2) (Var 3)) (perturb (evalFma v1 v2 v3) m delta) m``,
fs [updEnv_def,updDefVars_def,join_fl3_def,join_fl_def,eval_expr_cases,APPLY_UPDATE_THM,PULL_EXISTS]
\\ rpt strip_tac
\\ qexists_tac `delta'` \\ fs[]
\\ IMP_RES_TAC Gamma_det \\ fs[]);
val eval_eq_env = store_thm (
"eval_eq_env",
``!e E1 E2 Gamma v m.
(!x. E1 x = E2 x) /\
eval_expr E1 Gamma e v m ==>
eval_expr E2 Gamma e v m``,
Induct \\ rpt strip_tac \\ fs[eval_expr_cases]
>- (`E1 n = E2 n` by (first_x_assum irule)
\\ fs[])
>- (qexists_tac `delta'` \\ fs[])
>- (rveq \\ qexistsl_tac [`m'`, `v1`] \\ fs[]
\\ first_x_assum drule \\ disch_then irule \\ fs[])
>- (rveq \\ qexistsl_tac [`m'`, `v1`] \\ fs[]
\\ qexists_tac `delta'` \\ fs[]
\\ first_x_assum drule \\ disch_then irule \\ fs[])
>- (rveq \\ qexistsl_tac [`m1`, `m2`, `v1`, `v2`, `delta'`]
\\ fs[] \\ conj_tac \\ first_x_assum irule \\ asm_exists_tac \\ fs[])
>- (rveq \\ qexistsl_tac [`m1`, `m2`, `m3`, `v1`, `v2`, `v3`, `delta'`]
\\ fs[] \\ prove_tac [])
>- (rveq \\ qexistsl_tac [`m1'`, `v1`, `delta'`] \\ fs[]