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

Show soundness of error validator

parent 61d70ff1
......@@ -1944,4 +1944,204 @@ val validErrorboundCorrectDiv = store_thm ("validErrorboundCorrectDiv",
simp[]))
>- (fs[])));
val validErrorbound_sound = store_thm ("validErrorbound_sound",
``!(e:real exp) (cenv:env) (absenv:analysisResult) (nR nF err:real) (P:precond) (elo ehi:real).
eval_exp 0 cenv P e nR /\
eval_exp machineEpsilon cenv P e nF /\
validErrorbound e absenv /\
validIntervalbounds e absenv P /\
(absenv e = ((elo,ehi),err)) ==>
abs (nR - nF) <= err``,
Induct_on `e` \\ rpt strip_tac \\ fs[]
>- (qpat_x_assum `validErrorbound _ _` (fn thm => ASSUME_TAC (ONCE_REWRITE_RULE [validErrorbound_def] thm)) \\
qpat_x_assum `absenv _ = _` (fn thm => fs[thm]))
>- (match_mp_tac validErrorboundCorrectParam \\
qexists_tac `cenv` \\ qexists_tac `absenv` \\
qexists_tac `n` \\ qexists_tac `elo` \\ qexists_tac `ehi` \\
qexists_tac `P` \\ fs[])
>- (match_mp_tac validErrorboundCorrectConstant \\
qexists_tac `cenv` \\ qexists_tac `absenv` \\
qexists_tac `v` \\ qexists_tac `elo` \\
qexists_tac `ehi` \\ qexists_tac `P` \\ fs[])
>- (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`
>- (match_mp_tac validErrorboundCorrectAddition \\
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 cenv P e1 nR1` \\
rename1 `eval_exp 0 cenv 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 cenv P e1 nF1` \\
rename1 `eval_exp machineEpsilon cenv P e2 nF2` \\
qexistsl_tac
[`cenv`, `absenv`, `e1`, `e2`, `nR1`, `nR2`, `nF1`, `nF2`,
`err1`, `err2`, `elo`, `ehi`, `e1lo`, `e1hi`, `e2lo`, `e2hi`,
`P`] \\
`abs (nR2 - nF2) <= err2`
by (qpat_x_assum `cenv absenv nR nF err P elo ehi.
eval_exp 0 cenv P e2 nR eval_exp machineEpsilon cenv P e2 nF
validErrorbound e2 absenv validIntervalbounds e2 absenv P
(absenv e2 = ((elo,ehi),err))
abs (nR nF) err`
match_mp_tac \\
qexistsl_tac [`cenv`, `absenv`, `P`, `e2lo`, `e2hi`] \\
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 `cenv absenv nR nF err P elo ehi.
eval_exp 0 cenv P e1 nR eval_exp machineEpsilon cenv P e1 nF
validErrorbound e1 absenv validIntervalbounds e1 absenv P
(absenv e1 = ((elo,ehi),err))
abs (nR nF) err`
match_mp_tac \\
qexistsl_tac [`cenv`, `absenv`, `P`, `e1lo`, `e1hi`] \\
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[]) \\
fs[])
>- (match_mp_tac validErrorboundCorrectSubtraction \\
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 cenv P e1 nR1` \\
rename1 `eval_exp 0 cenv P e2 nR2` \\
qpat_x_assum `eval_exp machineEpsilon _ _ (Binop Sub e1 e2) _`
(fn thm => elim_exist (ONCE_REWRITE_RULE [binary_unfolding] thm)) \\
rename1 `eval_exp machineEpsilon cenv P e1 nF1` \\
rename1 `eval_exp machineEpsilon cenv P e2 nF2` \\
qexistsl_tac
[`cenv`, `absenv`, `e1`, `e2`, `nR1`, `nR2`, `nF1`, `nF2`,
`err1`, `err2`, `elo`, `ehi`, `e1lo`, `e1hi`, `e2lo`, `e2hi`,
`P`] \\
`abs (nR2 - nF2) <= err2`
by (qpat_x_assum `cenv absenv nR nF err P elo ehi.
eval_exp 0 cenv P e2 nR eval_exp machineEpsilon cenv P e2 nF
validErrorbound e2 absenv validIntervalbounds e2 absenv P
(absenv e2 = ((elo,ehi),err))
abs (nR nF) err`
match_mp_tac \\
qexistsl_tac [`cenv`, `absenv`, `P`, `e2lo`, `e2hi`] \\
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 `cenv absenv nR nF err P elo ehi.
eval_exp 0 cenv P e1 nR eval_exp machineEpsilon cenv P e1 nF
validErrorbound e1 absenv validIntervalbounds e1 absenv P
(absenv e1 = ((elo,ehi),err))
abs (nR nF) err`
match_mp_tac \\
qexistsl_tac [`cenv`, `absenv`, `P`, `e1lo`, `e1hi`] \\
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[]) \\
fs[])
>- (match_mp_tac validErrorboundCorrectMult \\
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 cenv P e1 nR1` \\
rename1 `eval_exp 0 cenv P e2 nR2` \\
qpat_x_assum `eval_exp machineEpsilon _ _ (Binop Mult e1 e2) _`
(fn thm => elim_exist (ONCE_REWRITE_RULE [binary_unfolding] thm)) \\
rename1 `eval_exp machineEpsilon cenv P e1 nF1` \\
rename1 `eval_exp machineEpsilon cenv P e2 nF2` \\
qexistsl_tac
[`cenv`, `absenv`, `e1`, `e2`, `nR1`, `nR2`, `nF1`, `nF2`,
`err1`, `err2`, `elo`, `ehi`, `e1lo`, `e1hi`, `e2lo`, `e2hi`,
`P`] \\
`abs (nR2 - nF2) <= err2`
by (qpat_x_assum `cenv absenv nR nF err P elo ehi.
eval_exp 0 cenv P e2 nR eval_exp machineEpsilon cenv P e2 nF
validErrorbound e2 absenv validIntervalbounds e2 absenv P
(absenv e2 = ((elo,ehi),err))
abs (nR nF) err`
match_mp_tac \\
qexistsl_tac [`cenv`, `absenv`, `P`, `e2lo`, `e2hi`] \\
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 ` cenv absenv nR nF err P elo ehi.
eval_exp 0 cenv P e1 nR eval_exp machineEpsilon cenv P e1 nF
validErrorbound e1 absenv validIntervalbounds e1 absenv P
(absenv e1 = ((elo,ehi),err))
abs (nR nF) err`
match_mp_tac \\
qexistsl_tac [`cenv`, `absenv`, `P`, `e1lo`, `e1hi`] \\
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[]) \\
fs[])
>- (match_mp_tac validErrorboundCorrectDiv \\
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 cenv P e1 nR1` \\
rename1 `eval_exp 0 cenv P e2 nR2` \\
qpat_x_assum `eval_exp machineEpsilon _ _ (Binop Div e1 e2) _`
(fn thm => elim_exist (ONCE_REWRITE_RULE [binary_unfolding] thm)) \\
rename1 `eval_exp machineEpsilon cenv P e1 nF1` \\
rename1 `eval_exp machineEpsilon cenv P e2 nF2` \\
qexistsl_tac
[`cenv`, `absenv`, `e1`, `e2`, `nR1`, `nR2`, `nF1`, `nF2`,
`err1`, `err2`, `elo`, `ehi`, `e1lo`, `e1hi`, `e2lo`, `e2hi`,
`P`] \\
`abs (nR2 - nF2) <= err2`
by (qpat_x_assum `cenv absenv nR nF err P elo ehi.
eval_exp 0 cenv P e2 nR eval_exp machineEpsilon cenv P e2 nF
validErrorbound e2 absenv validIntervalbounds e2 absenv P
(absenv e2 = ((elo,ehi),err))
abs (nR nF) err`
match_mp_tac \\
qexistsl_tac [`cenv`, `absenv`, `P`, `e2lo`, `e2hi`] \\
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 ` cenv absenv nR nF err P elo ehi.
eval_exp 0 cenv P e1 nR eval_exp machineEpsilon cenv P e1 nF
validErrorbound e1 absenv validIntervalbounds e1 absenv P
(absenv e1 = ((elo,ehi),err))
abs (nR nF) err`
match_mp_tac \\
qexistsl_tac [`cenv`, `absenv`, `P`, `e1lo`, `e1hi`] \\
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[]) \\
fs[])));
val _ = export_theory();
......@@ -445,6 +445,6 @@ val minAbs_negative_iv_is_hi = store_thm ("minAbs_negative_iv_is_hi",
fs[minAbsFun_def] \\
`abs a = - a` by REAL_ASM_ARITH_TAC \\
`abs b = - b` by REAL_ASM_ARITH_TAC \\
fs[REAL_MIN_ALT] );
fs[REAL_MIN_ALT]);
val _ = export_theory();
......@@ -55,6 +55,11 @@ and elim_exist thm =
fun inversion pattern cases_thm =
qpat_x_assum pattern
(fn thm => elim_exist (ONCE_REWRITE_RULE [cases_thm] thm));
fun qexistsl_tac termlist =
case termlist of
[] => ALL_TAC
| t::tel => qexists_tac t \\ qexistsl_tac tel;
(* -- *)
val _ = set_trace"Goalstack.print_goal_at_top"0 handle HOL_ERR _ => set_trace"goalstack print goal at top"0
......
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