Commit bd83c45a authored by Heiko Becker's avatar Heiko Becker

Same simplification in HOL4

parent 95dac28a
......@@ -38,7 +38,7 @@ Qed.
Lemma add_abs_err_bounded (e1:exp Q) (e1R:R) (e1F:R) (e2:exp Q) (e2R:R) (e2F:R)
(vR:R) (vF:R) (VarEnv1 VarEnv2 ParamEnv:env) (P:precond)
(err1 err2 :Q) (absenv:analysisResult):
(err1 err2 :Q):
eval_exp 0%R VarEnv1 ParamEnv P (toRExp e1) e1R ->
eval_exp (Q2R machineEpsilon) VarEnv2 ParamEnv P (toRExp e1) e1F ->
eval_exp 0%R VarEnv1 ParamEnv P (toRExp e2) e2R ->
......
......@@ -36,7 +36,7 @@ val param_abs_err_bounded = store_thm ("param_abs_err_bounded",
val add_abs_err_bounded = store_thm ("add_abs_err_bounded",
``!(e1:real exp) (e1R:real) (e1F:real) (e2:real exp) (e2R:real) (e2F:real) (err1:real) (err2:real)
(vR:real) (vF:real) (VarEnv1 VarEnv2 ParamEnv:env) (P:precond) (absenv:analysisResult).
(vR:real) (vF:real) (VarEnv1 VarEnv2 ParamEnv:env) (P:precond).
eval_exp 0 VarEnv1 ParamEnv P e1 e1R /\
eval_exp machineEpsilon VarEnv2 ParamEnv P e1 e1F /\
eval_exp 0 VarEnv1 ParamEnv P e2 e2R /\
......
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