Commit f5e323af authored by Heiko Becker's avatar Heiko Becker

Add no division by zero assumption to HOL4 evaluation model too

parent 1869fcc2
......@@ -80,7 +80,8 @@ val (eval_exp_rules, eval_exp_ind, eval_exp_cases) = Hol_reln `
(!eps E b f1 f2 v1 v2 delta.
abs delta <= eps /\
eval_exp eps E f1 v1 /\
eval_exp eps E f2 v2 ==>
eval_exp eps E f2 v2 /\
((b = Div) ==> (~ v2 = 0)) ==>
eval_exp eps E (Binop b f1 f2) (perturb (evalBinop b v1 v2) delta))`;
(**
......
......@@ -17,6 +17,7 @@ val validVars_add = store_thm("validVars_add",
domain (usedVars e) domain (insert n () Vs)``,
fs [domain_insert, SUBSET_DEF]);
(*
val validVars_non_stuck = store_thm ("validVars_non_stuck",
``!(e:real exp) inVars E.
domain (usedVars e) ⊆ inVars /\
......@@ -52,6 +53,7 @@ val validVars_non_stuck = store_thm ("validVars_non_stuck",
\\ Cases_on `b` \\ fs[eval_exp_cases]
\\ qexistsl_tac [`vR1`, `vR2`, `0`]
\\ fs[perturb_def]));
*)
(**
Inductive ssa predicate, following the definitions from the LVC framework,
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment