Commit b8a5ce0c authored by Heiko Becker's avatar Heiko Becker
Browse files

Fix some stuff as explained by Magnus

parent 7106b819
......@@ -71,12 +71,13 @@ val err_always_positive = store_thm ("err_always_positive",
val validErrorboundCorrectVariable = store_thm ("validErrorboundCorrectVariable",
``!(ParamEnv:env) (v:num)
(nR nF err nlo nhi:real) (P:precond) VarEnv1 absenv VarEnv2.
approxEnv VarEnv1 absenv VarEnv2 ==>
approxEnv VarEnv1 absenv VarEnv2 /\
eval_exp 0 VarEnv1 ParamEnv P (Var v) nR /\
eval_exp machineEpsilon VarEnv2 ParamEnv P (Var v) nF /\
validErrorbound (Var v) absenv /\
(absenv (Var v) = ((nlo, nhi),err)) ==>
abs (nR - nF) <= err``,
once_rewrite_tac [GSYM AND_IMP_INTRO] \\
gen_tac \\ gen_tac \\ gen_tac \\ gen_tac \\ gen_tac \\ gen_tac \\
gen_tac \\ gen_tac \\
ho_match_mp_tac approxEnv_ind \\
......@@ -132,11 +133,11 @@ val validErrorboundCorrectParam = store_thm ("validErrorboundCorrectParam",
MEM v1 (freeVars ((Param v):real exp)) ==>
isSupersetInterval (P v1) (FST (absenv (Param v1)))) /\
(absenv (Param v) = ((nlo,nhi),e)) ==>
(abs (nR - nF)) <= e``
(abs (nR - nF)) <= e``,
once_rewrite_tac [validErrorbound_def] \\
rpt strip_tac \\ fs[] \\
qpat_x_assum `absenv _ = _` (fn thm => rule_assum_tac (fn thm2 => REWRITE_RULE [thm] thm2)) \\
inversion `eval_exp 0 _ _ _ _ _` eval_exp_cases \\ rveq \\
inversion `eval_exp 0 _ _ _ _ _ ` eval_exp_cases \\ rveq \\
simp [delta_0_deterministic] \\
inversion `eval_exp _ _ _ _ _ _` eval_exp_cases \\ rveq \\
simp [perturb_def] \\
......
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