Commit 2863bff7 authored by Heiko Becker's avatar Heiko Becker
Browse files

Port soundness proof to new setting for let Bindings in HOL4

parent 1db30802
......@@ -11,8 +11,7 @@ open ExpressionAbbrevsTheory EnvironmentsTheory
val _ = new_theory "ErrorBounds";
val const_abs_err_bounded = store_thm ("const_abs_err_bounded",
``!(P:precond) (n:real) (nR:real) (nF:real) (VarEnv1 VarEnv2 ParamEnv:env) (absenv:analysisResult).
approxEnv VarEnv1 absenv VarEnv2 /\
``!(P:precond) (n:real) (nR:real) (nF:real) (VarEnv1 VarEnv2 ParamEnv:env).
eval_exp 0 VarEnv1 ParamEnv P (Const n) nR /\
eval_exp machineEpsilon VarEnv2 ParamEnv P (Const n) nF ==>
abs (nR - nF) <= abs n * machineEpsilon``,
......@@ -24,8 +23,7 @@ val const_abs_err_bounded = store_thm ("const_abs_err_bounded",
match_mp_tac REAL_LE_LMUL_IMP \\ REAL_ASM_ARITH_TAC);
val param_abs_err_bounded = store_thm ("param_abs_err_bounded",
``!(P:precond) (n:num) (nR:real) (nF:real) (VarEnv1 VarEnv2 ParamEnv:env) (absenv:analysisResult).
approxEnv VarEnv1 absenv VarEnv2 /\
``!(P:precond) (n:num) (nR:real) (nF:real) (VarEnv1 VarEnv2 ParamEnv:env).
eval_exp 0 VarEnv1 ParamEnv P (Param n) nR /\
eval_exp machineEpsilon VarEnv2 ParamEnv P (Param n) nF ==>
abs (nR - nF) <= abs (ParamEnv n) * machineEpsilon``,
......@@ -39,7 +37,6 @@ 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).
approxEnv VarEnv1 absenv VarEnv2 /\
eval_exp 0 VarEnv1 ParamEnv P e1 e1R /\
eval_exp machineEpsilon VarEnv2 ParamEnv P e1 e1F /\
eval_exp 0 VarEnv1 ParamEnv P e2 e2R /\
......@@ -80,7 +77,6 @@ val add_abs_err_bounded = store_thm ("add_abs_err_bounded",
val subtract_abs_err_bounded = store_thm ("subtract_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).
approxEnv VarEnv1 absenv VarEnv2 /\
eval_exp 0 VarEnv1 ParamEnv P e1 e1R /\
eval_exp machineEpsilon VarEnv2 ParamEnv P e1 e1F /\
eval_exp 0 VarEnv1 ParamEnv P e2 e2R /\
......@@ -123,8 +119,7 @@ val subtract_abs_err_bounded = store_thm ("subtract_abs_err_bounded",
val mult_abs_err_bounded = store_thm ("mult_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).
approxEnv VarEnv1 absenv VarEnv2 /\
(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 /\
......@@ -162,7 +157,6 @@ val mult_abs_err_bounded = store_thm ("mult_abs_err_bounded",
val div_abs_err_bounded = store_thm ("div_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).
approxEnv VarEnv1 absenv VarEnv2 /\
eval_exp 0 VarEnv1 ParamEnv P e1 e1R /\
eval_exp machineEpsilon VarEnv2 ParamEnv P e1 e1F /\
eval_exp 0 VarEnv1 ParamEnv P e2 e2R /\
......
This diff is collapsed.
......@@ -298,7 +298,7 @@ val validIntervalbounds_sound = store_thm ("validIntervalbounds_sound",
(FST iv_f * (inv (FST iv_f'))) (SND iv_f * (inv (SND iv_f'))) (SND iv_f * (inv (FST iv_f')))` \\
metis_tac []))));
val validIntervalboundsCmd_sound = store_thm ("validIntervalbounds_sound",
val validIntervalboundsCmd_sound = store_thm ("validIntervalboundsCmd_sound",
``!f absenv VarEnv ParamEnv envR inVars outVars elo ehi err P.
ssaPrg f inVars outVars /\
bstep f VarEnv ParamEnv P 0 Nop envR /\
......
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