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

Work on addition soundness

parent 6cf28652
......@@ -2130,71 +2130,60 @@ val validErrorbound_sound = store_thm ("validErrorbound_sound",
\\ fs [usedVars_def, SUBSET_DEF])
>- (qpat_x_assum `validErrorbound _ _ _` (fn thm => ASSUME_TAC (ONCE_REWRITE_RULE [validErrorbound_def] thm)) \\
qpat_x_assum `absenv _ = _` (fn thm => fs[thm]))
>- (rename1 `Binop op e1 e2` \\
Cases_on `op`
>- (Cases_on `absenv e1` \\ rename1 `absenv e1 = (iv, err1)` \\
Cases_on `iv` \\ rename1 `absenv e1 = ((e1lo, e1hi),err1)` \\
Cases_on `absenv e2` \\ rename1 `absenv e2 = (iv, err2)` \\
Cases_on `iv` \\ rename1 `absenv e2 = ((e2lo, e2hi), err2)` \\
qpat_assum `eval_exp 0 _ _ _ _ _`
(fn thm => elim_exist (ONCE_REWRITE_RULE [eval_exp_cases] thm)) \\
rename1 `eval_exp 0 _ _ P e1 nR1` \\
rename1 `eval_exp 0 _ _ P e2 nR2` \\
qpat_x_assum `eval_exp machineEpsilon _ _ _ (Binop Plus e1 e2) _`
(fn thm => elim_exist (ONCE_REWRITE_RULE [binary_unfolding] thm)) \\
rename1 `eval_exp machineEpsilon _ _ P e1 nF1` \\
rename1 `eval_exp machineEpsilon _ _ P e2 nF2` \\
`abs (nR2 - nF2) <= err2`
by (qpat_x_assum
`E1 E2absenv nR nF err P elo ehi fVars.
approxEnv E1 absenv E2
eval_exp 0 E1 e2 nR
eval_exp machineEpsilon E2 e2 nF
validErrorbound e2 absenv
validIntervalbounds e2 absenv P fVars
(v.
v fVars
FST (FST (absenv (Var v))) E1 v
E1 v SND (FST (absenv (Var v))))
(absenv e2 = ((elo,ehi),err))
abs (nR nF) err`
match_mp_tac \\
qexistsl_tac [`E1`, `E2`, `ParamEnv`, `absenv`, `P`, `e2lo`, `e2hi`, `fVars`] \\
qpat_x_assum `validErrorbound _ _` (fn thm => ASSUME_TAC (ONCE_REWRITE_RULE [validErrorbound_def] thm)) \\
qpat_x_assum `validIntervalbounds _ _ _ _` (fn thm => ASSUME_TAC (ONCE_REWRITE_RULE [validIntervalbounds_def] thm)) \\
fs[] \\
rpt (qpat_x_assum `absenv _ = _ ` (fn thm => rule_assum_tac (fn asm => REWRITE_RULE [thm] asm))) \\
fs[]) \\
`abs (nR1 - nF1) <= err1`
by (qpat_x_assum
`E1 E2absenv nR nF err P elo ehi fVars.
approxEnv E1 absenv E2
eval_exp 0 E1 e1 nR
eval_exp machineEpsilon E2 e1 nF
validErrorbound e1 absenv
validIntervalbounds e1 absenv P fVars
(v.
v fVars
FST (FST (absenv (Var v))) E1 v
E1 v SND (FST (absenv (Var v))))
(absenv e1 = ((elo,ehi),err))
abs (nR nF) err`
match_mp_tac \\
qexistsl_tac [`E1`, `E2`, `ParamEnv`, `absenv`, `P`, `e1lo`, `e1hi`, `fVars`] \\
qpat_x_assum `validErrorbound _ _` (fn thm => ASSUME_TAC (ONCE_REWRITE_RULE [validErrorbound_def] thm)) \\
qpat_x_assum `validIntervalbounds _ _ _ _` (fn thm => ASSUME_TAC (ONCE_REWRITE_RULE [validIntervalbounds_def] thm)) \\
fs[] \\
rpt (qpat_x_assum `absenv _ = _ ` (fn thm => rule_assum_tac (fn asm => REWRITE_RULE [thm] asm))) \\
fs[]) \\
match_mp_tac validErrorboundCorrectAddition \\
qexistsl_tac [`E1`, `E2`, `ParamEnv`, `absenv`, `e1`, `e2`,
`nR1`, `nR2`, `nF1`, `nF2`, `err1`, `err2`, `elo`, `ehi`,
`e1lo`, `e1hi`, `e2lo`, `e2hi`, `P`] \\
`FST (FST (absenv e1)) <= nR1 /\ nR1 <= SND (FST (absenv e1))`
by (match_mp_tac validIntervalbounds_sound \\
qexistsl_tac [`P`, `fVars`, `E1`, `ParamEnv`] \\
qpat_x_assum `validIntervalbounds _ _ _ _` (fn thm => ASSUME_TAC (ONCE_REWRITE_RULE [validIntervalbounds_def] thm)) \\
rpt (qpat_x_assum `absenv _ = _ ` (fn thm => fs [thm]))) \\
>- (rename1 `Binop op e1 e2`
\\ Cases_on `op`
>- (Cases_on `absenv e1` \\ rename1 `absenv e1 = (iv, err1)`
\\ Cases_on `iv` \\ rename1 `absenv e1 = ((e1lo, e1hi),err1)`
\\ Cases_on `absenv e2` \\ rename1 `absenv e2 = (iv, err2)`
\\ Cases_on `iv` \\ rename1 `absenv e2 = ((e2lo, e2hi), err2)`
\\ qpat_assum `eval_exp 0 _ _ _`
(fn thm => elim_exist (ONCE_REWRITE_RULE [eval_exp_cases] thm))
\\ rename1 `eval_exp 0 _ e1 nR1`
\\ rename1 `eval_exp 0 _ e2 nR2`
\\ qpat_x_assum `eval_exp machineEpsilon _ (Binop Plus e1 e2) _`
(fn thm => elim_exist (ONCE_REWRITE_RULE [binary_unfolding] thm))
\\ rename1 `eval_exp machineEpsilon _ e1 nF1`
\\ rename1 `eval_exp machineEpsilon _ e2 nF2`
\\ `abs (nR2 - nF2) <= err2`
by (qpat_x_assum
`E1 E2 absenv nR nF err P elo ehi fVars dVars.
_ /\
eval_exp 0 E1 e2 nR
eval_exp machineEpsilon E2 e2 nF
_
abs (nR nF) err`
match_mp_tac
\\ qexistsl_tac [`E1`, `E2`, `absenv`, `P`, `e2lo`, `e2hi`, `fVars`, `dVars`]
\\ qpat_x_assum `validErrorbound _ _ _` (fn thm => ASSUME_TAC (ONCE_REWRITE_RULE [validErrorbound_def] thm))
\\ qpat_x_assum `validIntervalbounds _ _ _ _` (fn thm => ASSUME_TAC (ONCE_REWRITE_RULE [validIntervalbounds_def] thm))
\\ fs[]
\\ rpt (qpat_x_assum `absenv _ = _ ` (fn thm => rule_assum_tac (fn asm => REWRITE_RULE [thm] asm)))
\\ fs[])
\\ `abs (nR1 - nF1) <= err1`
by (qpat_x_assum
`E1 E2 absenv nR nF err P elo ehi fVars dVars.
_
eval_exp 0 E1 e1 nR
eval_exp machineEpsilon E2 e1 nF
_
abs (nR nF) err`
match_mp_tac
\\ qexistsl_tac [`E1`, `E2`, `absenv`, `P`, `e1lo`, `e1hi`, `fVars`, `dVars`]
\\ qpat_x_assum `validErrorbound _ _ _` (fn thm => ASSUME_TAC (ONCE_REWRITE_RULE [validErrorbound_def] thm))
\\ qpat_x_assum `validIntervalbounds _ _ _ _` (fn thm => ASSUME_TAC (ONCE_REWRITE_RULE [validIntervalbounds_def] thm))
\\ fs[]
\\ rpt (qpat_x_assum `absenv _ = _ ` (fn thm => rule_assum_tac (fn asm => REWRITE_RULE [thm] asm)))
\\ fs[])
\\ match_mp_tac validErrorboundCorrectAddition
\\ qexistsl_tac [`E1`, `E2`, `absenv`, `e1`, `e2`, `nR1`, `nR2`,
`nF1`, `nF2`, `err1`, `err2`, `elo`, `ehi`, `e1lo`, `e1hi`,
`e2lo`, `e2hi`, `dVars`]
\\ `FST (FST (absenv e1)) <= nR1 /\ nR1 <= SND (FST (absenv e1))`
by (match_mp_tac validIntervalbounds_sound
\\ qexistsl_tac [`P`, `fVars`, `dVars`, `E1`]
\\ qpat_x_assum `validIntervalbounds _ _ _ _` (fn thm => ASSUME_TAC (ONCE_REWRITE_RULE [validIntervalbounds_def] thm))
\\ rpt (qpat_x_assum `absenv _ = _ ` (fn thm => fs [thm]))
(* CONTINUE HERE *))
`FST (FST (absenv e2)) <= nR2 /\ nR2 <= SND (FST (absenv e2))`
by (match_mp_tac validIntervalbounds_sound \\
qexistsl_tac [`P`, `fVars`, `E1`, `ParamEnv`] \\
......
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