Commit bc0f13ea authored by Heiko Becker's avatar Heiko Becker

Show soundness of addition

parent 5e305543
......@@ -63,8 +63,8 @@ val validErrorboundCorrectConstant = store_thm ("validErrorboundCorrectConstant"
validIntervalbounds (Const n) absenv P /\
(absenv (Const n) = ((nlo,nhi),e)) ==>
(abs (nR - nF)) <= e``,
once_rewrite_tac [validErrorbound_def] \\ rpt strip_tac \\
fs[] \\
once_rewrite_tac [validErrorbound_def] \\
rpt strip_tac \\ fs[] \\
`FST (FST (absenv (Const n))) <= nR /\ nR <= SND (FST (absenv (Const n)))`
by (match_mp_tac validIntervalbounds_sound \\ qexists_tac `P` \\ qexists_tac `cenv` \\ simp[]) \\
inversion `eval_exp 0 cenv P (Const n) nR` eval_exp_cases \\ rveq \\
......@@ -90,8 +90,8 @@ val validErrorboundCorrectParam = store_thm ("validErrorboundCorrectParam",
validIntervalbounds (Param v) absenv P /\
(absenv (Param v) = ((nlo,nhi),e)) ==>
(abs (nR - nF)) <= e``,
once_rewrite_tac [validErrorbound_def] \\ rpt strip_tac \\
fs[] \\
once_rewrite_tac [validErrorbound_def] \\
rpt strip_tac \\ fs[] \\
`!(v1:num). MEM v1 (freeVars ((Param v):real exp)) ==> isSupersetInterval (P v1) (FST (absenv (Param v1)))`
by (drule ivbounds_approximatesPrecond_sound \\ rpt strip_tac \\ first_x_assum (match_mp_tac) \\ simp[]) \\
`FST (FST (absenv (Param v))) <= nR /\ nR <= SND (FST (absenv (Param v)))`
......@@ -111,4 +111,62 @@ val validErrorboundCorrectParam = store_thm ("validErrorboundCorrectParam",
match_mp_tac maxAbs \\
qspecl_then [`delta`, `n`] (fn thm => fs [thm]) delta_0_deterministic);
val validErrorboundCorrectAddition = store_thm ("validErrorboundCorrectAddition",
``!(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 Plus 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 Plus (Var 1) (Var 2)) nF /\
validErrorbound (Binop Plus e1 e2) absenv /\
validIntervalbounds (Binop Plus e1 e2) absenv P /\
(absenv e1 = ((e1lo,e1hi),err1)) /\
(absenv e2 = ((e2lo, e2hi),err2)) /\
(absenv (Binop Plus 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 add_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 (addInterval (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) (addInterval (widenInterval (e1lo, e1hi) err1) (widenInterval (e2lo, e2hi) err2))`
by (match_mp_tac (ONCE_REWRITE_RULE [validIntervalAdd_def] interval_addition_valid) \\
conj_tac \\ simp[]) \\
rule_assum_tac (fn thm => REWRITE_RULE [contained_def, IVlo_def, IVhi_def] thm) \\
simp[] ));
val _ = export_theory();
......@@ -40,4 +40,7 @@ val machineEpsilon_def = Define `machineEpsilon = 1/ (2 pow 53)`;
val real_le_trans2 = store_thm ("real_le_trans2",
``!(y:real) x z. x <= y /\ y <= z ==> x <= z``, metis_tac[REAL_LE_TRANS]);
val mEps_geq_zero = store_thm ("mEps_geq_zero",
``0 <= machineEpsilon``, once_rewrite_tac[machineEpsilon_def] \\ EVAL_TAC);
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