Commit 72d872f3 authored by Heiko Becker's avatar Heiko Becker

And subtraction is also done

parent bc0f13ea
......@@ -169,4 +169,62 @@ val validErrorboundCorrectAddition = store_thm ("validErrorboundCorrectAddition"
rule_assum_tac (fn thm => REWRITE_RULE [contained_def, IVlo_def, IVhi_def] thm) \\
simp[] ));
val validErrorboundCorrectSubtraction = store_thm ("validErrorboundCorrectSubtraction",
``!(cenv:env) (absenv:analysisResult) (e1:real exp) (e2:real exp)
(nR nR1 nR2 nF nF1 nF2:real) (e err1 err2:real) (alo ahi e1lo e1hi e2lo e2hi :real) (P:precond).
eval_exp 0 cenv P e1 nR1 /\
eval_exp 0 cenv P e2 nR2 /\
eval_exp 0 cenv P (Binop Sub e1 e2) nR /\
eval_exp machineEpsilon cenv P e1 nF1 /\
eval_exp machineEpsilon cenv P e2 nF2 /\
eval_exp machineEpsilon
(updEnv 2 nF2 (updEnv 1 nF1 cenv)) P (Binop Sub (Var 1) (Var 2)) nF /\
validErrorbound (Binop Sub e1 e2) absenv /\
validIntervalbounds (Binop Sub e1 e2) absenv P /\
(absenv e1 = ((e1lo,e1hi),err1)) /\
(absenv e2 = ((e2lo, e2hi),err2)) /\
(absenv (Binop Sub e1 e2) = ((alo,ahi),e)) /\
abs (nR1 - nF1) <= err1 /\
abs (nR2 - nF2) <= err2 ==>
abs (nR - nF) <= e``,
once_rewrite_tac [validErrorbound_def] \\
rpt strip_tac \\ fs[] \\
qpat_x_assum `validIntervalbounds _ _ _` (fn thm => ASSUME_TAC (ONCE_REWRITE_RULE [validIntervalbounds_def] thm)) \\
qpat_x_assum `absenv _ = _` (fn thm => rule_assum_tac (fn thm2 => REWRITE_RULE [thm] thm2) \\ ASSUME_TAC thm) \\
fs [] \\
qpat_x_assum `absenv e1 = _` (fn thm => rule_assum_tac (fn thm2 => REWRITE_RULE [thm] thm2) \\ ASSUME_TAC thm) \\
qpat_x_assum `absenv e2 = _` (fn thm => rule_assum_tac (fn thm2 => REWRITE_RULE [thm] thm2) \\ ASSUME_TAC thm) \\
fs [] \\
`FST (FST (absenv e1 )) <= nR1 /\ nR1 <= SND (FST (absenv e1))`
by (match_mp_tac validIntervalbounds_sound \\ qexists_tac `P` \\ qexists_tac `cenv` \\ simp[]) \\
`FST (FST (absenv e2)) <= nR2 /\ nR2 <= SND (FST (absenv e2))`
by (match_mp_tac validIntervalbounds_sound \\ qexists_tac `P` \\ qexists_tac `cenv` \\ simp[]) \\
qpat_x_assum `absenv e1 = _` (fn thm => rule_assum_tac (fn thm2 => REWRITE_RULE [thm] thm2) \\ ASSUME_TAC thm) \\
qpat_x_assum `absenv e2 = _` (fn thm => rule_assum_tac (fn thm2 => REWRITE_RULE [thm] thm2) \\ ASSUME_TAC thm) \\
match_mp_tac REAL_LE_TRANS \\
qexists_tac `err1 + err2 + (abs (nF1 - nF2) * machineEpsilon)` \\
conj_tac
>- (match_mp_tac subtract_abs_err_bounded \\
qexists_tac `e1` \\ qexists_tac `nR1` \\ qexists_tac `e2` \\ qexists_tac `nR2` \\
qexists_tac `cenv` \\ qexists_tac `P` \\
rpt (conj_tac) \\ simp[])
>- (match_mp_tac REAL_LE_TRANS \\
qexists_tac
`err1 + err2 + maxAbsFun (subtractInterval (widenInterval (e1lo,e1hi) err1) (widenInterval (e2lo,e2hi) err2)) * machineEpsilon` \\
conj_tac \\ simp[maxAbsFun_def] \\
once_rewrite_tac [REAL_MUL_COMM] \\ match_mp_tac REAL_LE_LMUL_IMP \\
conj_tac \\ simp[mEps_geq_zero] \\
match_mp_tac maxAbs \\
`contained nF1 (widenInterval (e1lo,e1hi) err1)`
by (match_mp_tac distance_gives_iv \\
qexists_tac `nR1` \\ conj_tac \\ simp[contained_def, IVlo_def, IVhi_def]) \\
`contained nF2 (widenInterval (e2lo,e2hi) err2)`
by (match_mp_tac distance_gives_iv \\
qexists_tac `nR2` \\ conj_tac \\ simp[contained_def, IVlo_def, IVhi_def]) \\
`contained (nF1 - nF2) (subtractInterval (widenInterval (e1lo, e1hi) err1) (widenInterval (e2lo, e2hi) err2))`
by (match_mp_tac (ONCE_REWRITE_RULE [validIntervalSub_def] interval_subtraction_valid) \\
conj_tac \\ simp[]) \\
rule_assum_tac (fn thm => REWRITE_RULE [contained_def, IVlo_def, IVhi_def] thm) \\
simp[] ));
val _ = export_theory();
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