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

Fix all proofs up to multiplication, except for variables in ErrroValidationScript.sml

parent 48976b98
......@@ -8,7 +8,7 @@
**)
open preamble
open simpLib realTheory realLib RealArith
open AbbrevsTheory ExpressionsTheory RealSimpsTheory
open AbbrevsTheory ExpressionsTheory RealSimpsTheory DaisyTactics
open ExpressionAbbrevsTheory ErrorBoundsTheory IntervalArithTheory
open IntervalValidationTheory EnvironmentsTheory CommandsTheory ssaPrgsTheory
......@@ -60,8 +60,8 @@ val validErrorboundCmd_def = Define `
validErrorbound e env dVars`;
val err_always_positive = store_thm ("err_always_positive",
``!(e:real exp) (absenv:analysisResult) (iv:interval) (err:real).
(validErrorbound (e:real exp) (absenv:analysisResult)) /\
``!(e:real exp) (absenv:analysisResult) (iv:interval) (err:real) dVars.
(validErrorbound (e:real exp) (absenv:analysisResult) dVars) /\
((iv,err) = absenv e) ==>
0 <= err``,
once_rewrite_tac [validErrorbound_def] \\ rpt strip_tac \\
......@@ -70,11 +70,11 @@ val err_always_positive = store_thm ("err_always_positive",
Cases_on `absenv e0` \\ Cases_on `absenv e'` \\ fs[]);
val validErrorboundCorrectVariable = store_thm ("validErrorboundCorrectVariable",
``!(ParamEnv:env) (v:num)
(nR nF err nlo nhi:real) (P:precond) 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 /\
``!(E1 E2:env) absenv (v:num)
(nR nF err nlo nhi:real) (P:precond) VarEnv1 absenv E2.
approxEnv VarEnv1 absenv E2 /\
eval_exp 0 VarEnv1P (Var v) nR /\
eval_exp machineEpsilon E2 (Var v) nF /\
validErrorbound (Var v) absenv /\
(absenv (Var v) = ((nlo, nhi),err)) ==>
abs (nR - nF) <= err``,
......@@ -96,73 +96,42 @@ val validErrorboundCorrectVariable = store_thm ("validErrorboundCorrectVariable"
conj_tac \\ metis_tac [eval_exp_rules]));
val validErrorboundCorrectConstant = store_thm ("validErrorboundCorrectConstant",
``!(VarEnv1 VarEnv2 ParamEnv:env) (absenv:analysisResult) (n nR nF e nlo nhi:real) (P:precond).
approxEnv VarEnv1 absenv VarEnv2 /\
eval_exp 0 VarEnv1 ParamEnv P (Const n) nR /\
eval_exp machineEpsilon VarEnv2 ParamEnv P (Const n) nF /\
validErrorbound (Const n) absenv /\
``!(E1 E2:env) (absenv:analysisResult) (n nR nF e nlo nhi:real) dVars.
eval_exp 0 E1 (Const n) nR /\
eval_exp machineEpsilon E2 (Const n) nF /\
validErrorbound (Const n) absenv dVars /\
FST (FST (absenv (Const n))) <= nR /\
nR <= SND (FST (absenv (Const n))) /\
(absenv (Const n) = ((nlo,nhi),e)) ==>
(abs (nR - nF)) <= e``,
once_rewrite_tac [validErrorbound_def] \\
rpt strip_tac \\ fs[] \\
inversion `eval_exp 0 _ _ P (Const n) nR` eval_exp_cases \\ rveq \\
simp [delta_0_deterministic] \\
inversion `eval_exp machineEpsilon _ _ _ _ _` eval_exp_cases \\ rveq \\
simp[perturb_def] \\
rename1 `abs deltaF <= machineEpsilon` \\
simp [Rabs_err_simpl, ABS_MUL] \\
match_mp_tac REAL_LE_TRANS \\
qexists_tac `maxAbsFun (nlo, nhi) * machineEpsilon` \\ conj_tac \\ TRY (simp[]) \\
match_mp_tac REAL_LE_MUL2 \\ rpt (conj_tac) \\ TRY (simp[ABS_POS]) \\
simp[maxAbsFun_def] \\
match_mp_tac maxAbs \\
qspecl_then [`delta`, `n`] (fn thm => fs [thm]) delta_0_deterministic \\
qpat_x_assum `absenv _ = _` (fn thm => rule_assum_tac (fn thm2 => REWRITE_RULE [thm] thm2)) \\
simp[]);
val validErrorboundCorrectParam = store_thm ("validErrorboundCorrectParam",
``!(VarEnv1 VarEnv2 ParamEnv:env) (absenv:analysisResult) (v:num) (nR nF e nlo nhi:real) (P:precond).
approxEnv VarEnv1 absenv VarEnv2 /\
eval_exp 0 VarEnv1 ParamEnv P (Param v) nR /\
eval_exp machineEpsilon VarEnv2 ParamEnv P (Param v) nF /\
validErrorbound (Param v) absenv /\
FST (FST (absenv (Param v))) <= nR /\
nR <= SND (FST (absenv (Param v))) /\
(!(v1:num).
MEM v1 (freeVars ((Param v):real exp)) ==>
isSupersetInterval (P v1) (FST (absenv (Param v1)))) /\
(absenv (Param v) = ((nlo,nhi),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 \\
simp [delta_0_deterministic] \\
inversion `eval_exp _ _ _ _ _ _` eval_exp_cases \\ rveq \\
simp [perturb_def] \\
rename1 `abs deltaF <= machineEpsilon` \\
simp [Rabs_err_simpl, ABS_MUL] \\
match_mp_tac REAL_LE_TRANS \\
qexists_tac `maxAbsFun (nlo, nhi) * machineEpsilon` \\
conj_tac \\ TRY (simp []) \\
match_mp_tac REAL_LE_MUL2 \\ rpt (conj_tac) \\ TRY (simp [ABS_POS]) \\
simp[maxAbsFun_def] \\
match_mp_tac maxAbs \\
qspecl_then [`delta`, `n`] (fn thm => fs [thm]) delta_0_deterministic);
once_rewrite_tac [validErrorbound_def]
\\ rpt strip_tac \\ fs[]
\\ inversion `eval_exp 0 _ (Const n) nR` eval_exp_cases \\ rveq
\\ simp [delta_0_deterministic]
\\ inversion `eval_exp machineEpsilon _ _ _` eval_exp_cases \\ rveq
\\ simp[perturb_def]
\\ rename1 `abs deltaF <= machineEpsilon`
\\ simp [Rabs_err_simpl, ABS_MUL]
\\ match_mp_tac REAL_LE_TRANS
\\ qexists_tac `maxAbs (nlo, nhi) * machineEpsilon` \\ conj_tac \\ TRY (simp[])
\\ match_mp_tac REAL_LE_MUL2 \\ rpt (conj_tac) \\ TRY (simp[ABS_POS])
\\ simp[maxAbs_def]
\\ match_mp_tac maxAbs
\\ qspecl_then [`delta`, `n`] (fn thm => fs [thm]) delta_0_deterministic
\\ qpat_x_assum `absenv _ = _` (fn thm => rule_assum_tac (fn thm2 => REWRITE_RULE [thm] thm2))
\\ simp[]);
val validErrorboundCorrectAddition = store_thm ("validErrorboundCorrectAddition",
``!(VarEnv1 VarEnv2 ParamEnv: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 VarEnv1 ParamEnv P e1 nR1 /\
eval_exp 0 VarEnv1 ParamEnv P e2 nR2 /\
eval_exp 0 VarEnv1 ParamEnv P (Binop Plus e1 e2) nR /\
eval_exp machineEpsilon VarEnv2 ParamEnv P e1 nF1 /\
eval_exp machineEpsilon VarEnv2 ParamEnv P e2 nF2 /\
``!(E1 E2: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) dVars.
eval_exp 0 E1 e1 nR1 /\
eval_exp 0 E1 e2 nR2 /\
eval_exp 0 E1 (Binop Plus e1 e2) nR /\
eval_exp machineEpsilon E2 e1 nF1 /\
eval_exp machineEpsilon E2 e2 nF2 /\
eval_exp machineEpsilon
(updEnv 2 nF2 (updEnv 1 nF1 VarEnv2)) ParamEnv P (Binop Plus (Var 1) (Var 2)) nF /\
validErrorbound (Binop Plus e1 e2) absenv /\
(updEnv 2 nF2 (updEnv 1 nF1 emptyEnv)) (Binop Plus (Var 1) (Var 2)) nF /\
validErrorbound (Binop Plus e1 e2) absenv dVars /\
FST (FST (absenv e1)) <= nR1 /\
nR1 <= SND (FST (absenv e1)) /\
FST (FST (absenv e2)) <= nR2 /\
......@@ -173,49 +142,50 @@ val validErrorboundCorrectAddition = store_thm ("validErrorboundCorrectAddition"
abs (nR1 - nF1) <= err1 /\
abs (nR2 - nF2) <= err2 ==>
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) \\ 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 [] \\
match_mp_tac REAL_LE_TRANS \\
qexists_tac `err1 + err2 + (abs (nF1 + nF2) * machineEpsilon)` \\
conj_tac
>- (match_mp_tac add_abs_err_bounded \\
qexistsl_tac [`e1`, `nR1`, `e2`, `nR2`, `VarEnv1`, `VarEnv2`, `ParamEnv`, `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[]));
once_rewrite_tac [validErrorbound_def]
\\ rpt strip_tac \\ fs[]
\\ rw_asm `absenv _ = _`
\\ rw_asm `absenv e1 = _`
\\ match_mp_tac REAL_LE_TRANS
\\ qexists_tac `err1 + err2 + (abs (nF1 + nF2) * machineEpsilon)`
\\ conj_tac
>- (match_mp_tac add_abs_err_bounded
\\ qexistsl_tac [`e1`, `nR1`, `e2`, `nR2`, `E1`, `E2`]
\\ rpt (conj_tac) \\ simp[])
>- (match_mp_tac REAL_LE_TRANS
\\ qexists_tac
`err1 + err2 + maxAbs (
addInterval (widenInterval (e1lo,e1hi) err1)
(widenInterval (e2lo,e2hi) err2)) * machineEpsilon`
\\ conj_tac \\ simp[maxAbs_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 validErrorboundCorrectSubtraction = store_thm ("validErrorboundCorrectSubtraction",
``!(VarEnv1 VarEnv2 ParamEnv: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 VarEnv1 ParamEnv P e1 nR1 /\
eval_exp 0 VarEnv1 ParamEnv P e2 nR2 /\
eval_exp 0 VarEnv1 ParamEnv P (Binop Sub e1 e2) nR /\
eval_exp machineEpsilon VarEnv2 ParamEnv P e1 nF1 /\
eval_exp machineEpsilon VarEnv2 ParamEnv P e2 nF2 /\
``!(E1 E2: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) dVars.
eval_exp 0 E1 e1 nR1 /\
eval_exp 0 E1 e2 nR2 /\
eval_exp 0 E1 (Binop Sub e1 e2) nR /\
eval_exp machineEpsilon E2 e1 nF1 /\
eval_exp machineEpsilon E2 e2 nF2 /\
eval_exp machineEpsilon
(updEnv 2 nF2 (updEnv 1 nF1 VarEnv2)) ParamEnv P (Binop Sub (Var 1) (Var 2)) nF /\
validErrorbound (Binop Sub e1 e2) absenv /\
(updEnv 2 nF2 (updEnv 1 nF1 emptyEnv)) (Binop Sub (Var 1) (Var 2)) nF /\
validErrorbound (Binop Sub e1 e2) absenv dVars /\
FST (FST (absenv e1)) <= nR1 /\
nR1 <= SND (FST (absenv e1)) /\
FST (FST (absenv e2)) <= nR2 /\
......@@ -226,49 +196,49 @@ val validErrorboundCorrectSubtraction = store_thm ("validErrorboundCorrectSubtra
abs (nR1 - nF1) <= err1 /\
abs (nR2 - nF2) <= err2 ==>
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) \\ 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 [] \\
match_mp_tac REAL_LE_TRANS \\
qexists_tac `err1 + err2 + (abs (nF1 - nF2) * machineEpsilon)` \\
conj_tac
>- (match_mp_tac subtract_abs_err_bounded \\
qexistsl_tac [`e1`, `nR1`, `e2`, `nR2`, `VarEnv1`, `VarEnv2`, `ParamEnv`, `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[]));
once_rewrite_tac [validErrorbound_def]
\\ rpt strip_tac \\ fs[]
\\ rpt (rw_asm `absenv _ = _`)
\\ match_mp_tac REAL_LE_TRANS
\\ qexists_tac `err1 + err2 + (abs (nF1 - nF2) * machineEpsilon)`
\\ conj_tac
>- (match_mp_tac subtract_abs_err_bounded
\\ qexistsl_tac [`e1`, `nR1`, `e2`, `nR2`, `E1`, `E2`]
\\ rpt (conj_tac) \\ simp[])
>- (match_mp_tac REAL_LE_TRANS
\\ qexists_tac
`err1 + err2 + maxAbs (
subtractInterval (widenInterval (e1lo,e1hi) err1)
(widenInterval (e2lo,e2hi) err2)) * machineEpsilon`
\\ conj_tac \\ simp[maxAbs_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 validErrorboundCorrectMult = store_thm ("validErrorboundCorrectMult",
``!(VarEnv1 VarEnv2 ParamEnv: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 VarEnv1 ParamEnv P e1 nR1 /\
eval_exp 0 VarEnv1 ParamEnv P e2 nR2 /\
eval_exp 0 VarEnv1 ParamEnv P (Binop Mult e1 e2) nR /\
eval_exp machineEpsilon VarEnv2 ParamEnv P e1 nF1 /\
eval_exp machineEpsilon VarEnv2 ParamEnv P e2 nF2 /\
``!(E1 E2: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) dVars.
eval_exp 0 E1 e1 nR1 /\
eval_exp 0 E1 e2 nR2 /\
eval_exp 0 E1 (Binop Mult e1 e2) nR /\
eval_exp machineEpsilon E2 e1 nF1 /\
eval_exp machineEpsilon E2 e2 nF2 /\
eval_exp machineEpsilon
(updEnv 2 nF2 (updEnv 1 nF1 VarEnv2)) ParamEnv P (Binop Mult (Var 1) (Var 2)) nF /\
validErrorbound (Binop Mult e1 e2) absenv /\
(updEnv 2 nF2 (updEnv 1 nF1 emptyEnv)) (Binop Mult (Var 1) (Var 2)) nF /\
validErrorbound (Binop Mult e1 e2) absenv dVars /\
FST (FST (absenv e1)) <= nR1 /\
nR1 <= SND (FST (absenv e1)) /\
FST (FST (absenv e2)) <= nR2 /\
......@@ -279,55 +249,53 @@ val validErrorboundCorrectMult = store_thm ("validErrorboundCorrectMult",
abs (nR1 - nF1) <= err1 /\
abs (nR2 - nF2) <= err2 ==>
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) \\ 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 [] \\
`0 <= err1`
by (match_mp_tac err_always_positive \\
qexists_tac `e1` \\ qexists_tac `absenv` \\ qexists_tac `(e1lo,e1hi)` \\ fs[]) \\
`0 <= err2`
by (match_mp_tac err_always_positive \\
qexists_tac `e2` \\ qexists_tac `absenv` \\ qexists_tac `(e2lo,e2hi)` \\ fs[]) \\
match_mp_tac REAL_LE_TRANS \\
qexists_tac `abs (nR1 * nR2 - nF1 * nF2) + abs (nF1 * nF2) * machineEpsilon` \\
conj_tac
>- (match_mp_tac mult_abs_err_bounded \\
qexistsl_tac [`e1`, `e2`, `err1`, `err2`, `VarEnv1`, `VarEnv2`, `ParamEnv`, `P`] \\
fs [])
>- (match_mp_tac REAL_LE_TRANS \\
qexists_tac `maxAbsFun (e1lo,e1hi) * err2 + maxAbsFun (e2lo,e2hi) * err1 +
once_rewrite_tac [validErrorbound_def]
\\ rpt strip_tac \\ fs[]
\\ qpat_x_assum `absenv (Binop _ _ _) = _` (fn thm => fs [thm] \\ ASSUME_TAC thm)
\\ qpat_x_assum `absenv e1 = _` (fn thm => fs [thm] \\ ASSUME_TAC thm)
\\ qpat_x_assum `absenv e2 = _` (fn thm => fs [thm] \\ ASSUME_TAC thm)
\\ `0 <= err1`
by (match_mp_tac err_always_positive
\\ qexistsl_tac [`e1`, `absenv`, `(e1lo,e1hi)`, `dVars`] \\ fs[])
\\ `0 <= err2`
by (match_mp_tac err_always_positive
\\ qexistsl_tac [`e2`, `absenv`, `(e2lo,e2hi)`, `dVars`] \\ fs[])
\\ match_mp_tac REAL_LE_TRANS
\\ qexists_tac `abs (nR1 * nR2 - nF1 * nF2) + abs (nF1 * nF2) * machineEpsilon`
\\ conj_tac
>- (match_mp_tac mult_abs_err_bounded
\\ qexistsl_tac [`e1`, `e2`, `err1`, `err2`, `E1`, `E2`]
\\ fs [])
>- (match_mp_tac REAL_LE_TRANS
\\ qexists_tac `maxAbs (e1lo,e1hi) * err2 + maxAbs (e2lo,e2hi) * err1 +
err1 * err2 +
maxAbsFun (multInterval (widenInterval (e1lo,e1hi) err1)
(widenInterval (e2lo,e2hi) err2)) * machineEpsilon` \\
conj_tac \\ TRY(simp[]) \\
match_mp_tac REAL_LE_ADD2 \\ conj_tac
>- (`nR1 <= maxAbsFun (e1lo, e1hi)`
maxAbs (multInterval (widenInterval (e1lo,e1hi) err1)
(widenInterval (e2lo,e2hi) err2)) * machineEpsilon`
\\ conj_tac \\ TRY(simp[]) \\
\\ match_mp_tac REAL_LE_ADD2 \\ conj_tac
>- (`nR1 <= maxAbs (e1lo, e1hi)`
by (match_mp_tac contained_leq_maxAbs_val \\ fs[contained_def, IVlo_def, IVhi_def]) \\
`nR2 <= maxAbsFun (e2lo, e2hi)`
`nR2 <= maxAbs (e2lo, e2hi)`
by (match_mp_tac contained_leq_maxAbs_val \\ fs[contained_def, IVlo_def, IVhi_def]) \\
`-nR1 <= maxAbsFun (e1lo, e1hi)`
`-nR1 <= maxAbs (e1lo, e1hi)`
by (match_mp_tac contained_leq_maxAbs_neg_val \\ fs[contained_def, IVlo_def, IVhi_def]) \\
`-nR2 <= maxAbsFun (e2lo, e2hi)`
`-nR2 <= maxAbs (e2lo, e2hi)`
by (match_mp_tac contained_leq_maxAbs_neg_val \\ fs[contained_def, IVlo_def, IVhi_def]) \\
`nR1 * err2 <= maxAbsFun (e1lo, e1hi) * err2`
`nR1 * err2 <= maxAbs (e1lo, e1hi) * err2`
by (match_mp_tac REAL_LE_RMUL_IMP \\ fs[]) \\
`-nR1 * err2 <= maxAbsFun (e1lo, e1hi) * err2`
`-nR1 * err2 <= maxAbs (e1lo, e1hi) * err2`
by (match_mp_tac REAL_LE_RMUL_IMP \\ fs[]) \\
`nR2 * err1 <= maxAbsFun (e2lo, e2hi) * err1`
`nR2 * err1 <= maxAbs (e2lo, e2hi) * err1`
by (match_mp_tac REAL_LE_RMUL_IMP \\ fs[]) \\
`-nR2 * err1 <= maxAbsFun (e2lo, e2hi) * err1`
`-nR2 * err1 <= maxAbs (e2lo, e2hi) * err1`
by (match_mp_tac REAL_LE_RMUL_IMP \\ fs[]) \\
`- (err1 * err2) <= err1 * err2`
by (fs[REAL_NEG_LMUL] \\ match_mp_tac REAL_LE_RMUL_IMP \\ REAL_ASM_ARITH_TAC) \\
`0 <= maxAbsFun (e1lo, e1hi) * err2` by REAL_ASM_ARITH_TAC \\
`maxAbsFun (e1lo, e1hi) * err2 <= maxAbsFun (e1lo, e1hi) * err2 + maxAbsFun (e2lo, e2hi) * err1`
`0 <= maxAbs (e1lo, e1hi) * err2` by REAL_ASM_ARITH_TAC \\
`maxAbs (e1lo, e1hi) * err2 <= maxAbs (e1lo, e1hi) * err2 + maxAbs (e2lo, e2hi) * err1`
by REAL_ASM_ARITH_TAC \\
`maxAbsFun (e1lo, e1hi) * err2 + maxAbsFun (e2lo, e2hi) * err1 <=
maxAbsFun (e1lo, e1hi) * err2 + maxAbsFun (e2lo, e2hi) * err1 + err1 * err2`
`maxAbs (e1lo, e1hi) * err2 + maxAbs (e2lo, e2hi) * err1 <=
maxAbs (e1lo, e1hi) * err2 + maxAbs (e2lo, e2hi) * err1 + err1 * err2`
by REAL_ASM_ARITH_TAC \\
rpt (qpat_x_assum `eval_exp _ _ _ _ _` kall_tac) \\
rpt (qpat_x_assum `validErrorbound _ _` kall_tac) \\
......@@ -491,9 +459,9 @@ val validErrorboundCorrectMult = store_thm ("validErrorboundCorrectMult",
fs [GSYM REAL_SUB_LNEG, real_sub, REAL_LDISTRIB, REAL_NEG_MUL2, REAL_ADD_ASSOC] \\
fs [GSYM real_sub, REAL_SUB_REFL, GSYM REAL_NEG_RMUL, REAL_MUL_COMM]) \\
simp[] \\ match_mp_tac REAL_LE_TRANS \\
qexists_tac `maxAbsFun (e2lo,e2hi) * err1` \\ conj_tac \\ simp[] \\
qexists_tac `maxAbs (e2lo,e2hi) * err1` \\ conj_tac \\ simp[] \\
match_mp_tac REAL_LE_TRANS \\
qexists_tac `maxAbsFun (e1lo, e1hi) * err2 + maxAbsFun (e2lo, e2hi) * err1` \\
qexists_tac `maxAbs (e1lo, e1hi) * err2 + maxAbs (e2lo, e2hi) * err1` \\
conj_tac \\ simp[] \\
once_rewrite_tac [REAL_ADD_COMM] \\
simp [REAL_LE_ADDR]))
......@@ -505,9 +473,9 @@ val validErrorboundCorrectMult = store_thm ("validErrorboundCorrectMult",
fs [GSYM REAL_SUB_LNEG, real_sub, REAL_LDISTRIB, REAL_NEG_MUL2, REAL_ADD_ASSOC] \\
fs [GSYM real_sub, REAL_SUB_REFL, GSYM REAL_NEG_RMUL, REAL_MUL_COMM]) \\
simp[] \\ match_mp_tac REAL_LE_TRANS \\
qexists_tac `maxAbsFun (e2lo,e2hi) * err1` \\ conj_tac \\ simp[] \\
qexists_tac `maxAbs (e2lo,e2hi) * err1` \\ conj_tac \\ simp[] \\
match_mp_tac REAL_LE_TRANS \\
qexists_tac `maxAbsFun (e1lo, e1hi) * err2 + maxAbsFun (e2lo, e2hi) * err1` \\
qexists_tac `maxAbs (e1lo, e1hi) * err2 + maxAbs (e2lo, e2hi) * err1` \\
conj_tac \\ simp[] \\
once_rewrite_tac [REAL_ADD_COMM] \\
simp [REAL_LE_ADDR])))))
......@@ -531,9 +499,9 @@ val validErrorboundCorrectMult = store_thm ("validErrorboundCorrectMult",
fs [GSYM REAL_SUB_LNEG, real_sub, REAL_LDISTRIB, REAL_NEG_MUL2, REAL_ADD_ASSOC] \\
fs [GSYM real_sub, REAL_SUB_REFL, GSYM REAL_NEG_RMUL, REAL_MUL_COMM]) \\
simp[] \\ match_mp_tac REAL_LE_TRANS \\
qexists_tac `maxAbsFun (e2lo,e2hi) * err1` \\ conj_tac \\ simp[] \\
qexists_tac `maxAbs (e2lo,e2hi) * err1` \\ conj_tac \\ simp[] \\
match_mp_tac REAL_LE_TRANS \\
qexists_tac `maxAbsFun (e1lo, e1hi) * err2 + maxAbsFun (e2lo, e2hi) * err1` \\
qexists_tac `maxAbs (e1lo, e1hi) * err2 + maxAbs (e2lo, e2hi) * err1` \\
conj_tac \\ simp[] \\
once_rewrite_tac [REAL_ADD_COMM] \\
simp [REAL_LE_ADDR]))
......@@ -545,9 +513,9 @@ val validErrorboundCorrectMult = store_thm ("validErrorboundCorrectMult",
fs [GSYM REAL_SUB_LNEG, real_sub, REAL_LDISTRIB, REAL_NEG_MUL2, REAL_ADD_ASSOC] \\
fs [GSYM real_sub, REAL_SUB_REFL, GSYM REAL_NEG_RMUL, REAL_MUL_COMM]) \\
simp[] \\ match_mp_tac REAL_LE_TRANS \\
qexists_tac `maxAbsFun (e2lo,e2hi) * err1` \\ conj_tac \\ simp[] \\
qexists_tac `maxAbs (e2lo,e2hi) * err1` \\ conj_tac \\ simp[] \\
match_mp_tac REAL_LE_TRANS \\
qexists_tac `maxAbsFun (e1lo, e1hi) * err2 + maxAbsFun (e2lo, e2hi) * err1` \\
qexists_tac `maxAbs (e1lo, e1hi) * err2 + maxAbs (e2lo, e2hi) * err1` \\
conj_tac \\ simp[] \\
once_rewrite_tac [REAL_ADD_COMM] \\
simp [REAL_LE_ADDR]))))
......@@ -599,9 +567,9 @@ val validErrorboundCorrectMult = store_thm ("validErrorboundCorrectMult",
fs [GSYM REAL_SUB_LNEG, real_sub, REAL_LDISTRIB, REAL_NEG_MUL2, REAL_ADD_ASSOC] \\
fs [GSYM real_sub, REAL_SUB_REFL, GSYM REAL_NEG_RMUL, REAL_MUL_COMM]) \\
simp[] \\ match_mp_tac REAL_LE_TRANS \\
qexists_tac `maxAbsFun (e1lo, e1hi) * err2` \\ conj_tac \\ simp[] \\
qexists_tac `maxAbs (e1lo, e1hi) * err2` \\ conj_tac \\ simp[] \\
match_mp_tac REAL_LE_TRANS \\
qexists_tac `maxAbsFun (e1lo, e1hi) * err2 + maxAbsFun (e2lo, e2hi) * err1` \\
qexists_tac `maxAbs (e1lo, e1hi) * err2 + maxAbs (e2lo, e2hi) * err1` \\
conj_tac \\ simp[]))
>- (match_mp_tac REAL_LE_TRANS \\ qexists_tac `nR1 * nR2 + (nR1 + err1) * - (nR2 + err2)` \\ conj_tac
>- (fs [REAL_NEG_RMUL] \\ once_rewrite_tac [REAL_MUL_COMM] \\
......@@ -628,9 +596,9 @@ val validErrorboundCorrectMult = store_thm ("validErrorboundCorrectMult",
fs [GSYM REAL_SUB_LNEG, real_sub, REAL_LDISTRIB, REAL_NEG_MUL2, REAL_ADD_ASSOC] \\
fs [GSYM real_sub, REAL_SUB_REFL, GSYM REAL_NEG_RMUL, REAL_MUL_COMM]) \\
simp[] \\ match_mp_tac REAL_LE_TRANS \\
qexists_tac `maxAbsFun (e1lo, e1hi) * err2` \\ conj_tac \\ simp[] \\
qexists_tac `maxAbs (e1lo, e1hi) * err2` \\ conj_tac \\ simp[] \\
match_mp_tac REAL_LE_TRANS \\
qexists_tac `maxAbsFun (e1lo, e1hi) * err2 + maxAbsFun (e2lo, e2hi) * err1` \\
qexists_tac `maxAbs (e1lo, e1hi) * err2 + maxAbs (e2lo, e2hi) * err1` \\
conj_tac \\ simp[]))
>- (match_mp_tac REAL_LE_TRANS \\ qexists_tac `nR1 * nR2 + (nR1 + err1) * - (nR2 - err2)` \\ conj_tac
>- (fs [REAL_NEG_RMUL] \\ once_rewrite_tac [REAL_MUL_COMM] \\
......@@ -660,9 +628,9 @@ val validErrorboundCorrectMult = store_thm ("validErrorboundCorrectMult",
fs [GSYM REAL_SUB_LNEG, real_sub, REAL_LDISTRIB, REAL_NEG_MUL2, REAL_ADD_ASSOC] \\
fs [GSYM real_sub, REAL_SUB_REFL, GSYM REAL_NEG_RMUL, REAL_MUL_COMM]) \\
simp[] \\ match_mp_tac REAL_LE_TRANS \\
qexists_tac `maxAbsFun (e1lo, e1hi) * err2` \\ conj_tac \\ simp[] \\
qexists_tac `maxAbs (e1lo, e1hi) * err2` \\ conj_tac \\ simp[] \\
match_mp_tac REAL_LE_TRANS \\
qexists_tac `maxAbsFun (e1lo, e1hi) * err2 + maxAbsFun (e2lo, e2hi) * err1` \\
qexists_tac `maxAbs (e1lo, e1hi) * err2 + maxAbs (e2lo, e2hi) * err1` \\
conj_tac \\ simp[]))
>- (match_mp_tac REAL_LE_TRANS \\ qexists_tac `-(nR1 * nR2) + (nR1 + err1) * (nR2 - err2)` \\ conj_tac
>- (fs [REAL_NEG_RMUL] \\ once_rewrite_tac [REAL_MUL_COMM] \\
......@@ -688,9 +656,9 @@ val validErrorboundCorrectMult = store_thm ("validErrorboundCorrectMult",
fs [GSYM REAL_SUB_LNEG, real_sub, REAL_LDISTRIB, REAL_NEG_MUL2, REAL_ADD_ASSOC] \\
fs [GSYM real_sub, REAL_SUB_REFL, GSYM REAL_NEG_RMUL, REAL_MUL_COMM]) \\
simp[] \\ match_mp_tac REAL_LE_TRANS \\
qexists_tac `maxAbsFun (e1lo, e1hi) * err2` \\ conj_tac \\ simp[] \\
qexists_tac `maxAbs (e1lo, e1hi) * err2` \\ conj_tac \\ simp[] \\
match_mp_tac REAL_LE_TRANS \\
qexists_tac `maxAbsFun (e1lo, e1hi) * err2 + maxAbsFun (e2lo, e2hi) * err1` \\
qexists_tac `maxAbs (e1lo, e1hi) * err2 + maxAbs (e2lo, e2hi) * err1` \\
conj_tac \\ simp[]))
>- (match_mp_tac REAL_LE_TRANS \\ qexists_tac `-(nR1 * nR2) + (nR1 + err1) * (nR2 + err2)` \\ conj_tac
>- (fs [REAL_NEG_RMUL] \\ once_rewrite_tac [REAL_MUL_COMM] \\
......@@ -736,9 +704,9 @@ val validErrorboundCorrectMult = store_thm ("validErrorboundCorrectMult",
fs [GSYM REAL_SUB_LNEG, real_sub, REAL_LDISTRIB, REAL_NEG_MUL2, REAL_ADD_ASSOC] \\
fs [GSYM real_sub, REAL_SUB_REFL, GSYM REAL_NEG_RMUL, REAL_MUL_COMM]) \\
simp[] \\ match_mp_tac REAL_LE_TRANS \\
qexists_tac `maxAbsFun (e1lo, e1hi) * err2` \\ conj_tac \\ simp[] \\
qexists_tac `maxAbs (e1lo, e1hi) * err2` \\ conj_tac \\ simp[] \\
match_mp_tac REAL_LE_TRANS \\
qexists_tac `maxAbsFun (e1lo, e1hi) * err2 + maxAbsFun (e2lo, e2hi) * err1` \\
qexists_tac `maxAbs (e1lo, e1hi) * err2 + maxAbs (e2lo, e2hi) * err1` \\
conj_tac \\ simp[]))
>- (match_mp_tac REAL_LE_TRANS \\ qexists_tac `nR1 * nR2 + (nR1 + err1) * - (nR2 + err2)` \\ conj_tac
>- (fs [REAL_NEG_RMUL] \\ once_rewrite_tac [REAL_MUL_COMM] \\
......@@ -763,9 +731,9 @@ val validErrorboundCorrectMult = store_thm ("validErrorboundCorrectMult",
fs [GSYM REAL_SUB_LNEG, real_sub, REAL_LDISTRIB, REAL_NEG_MUL2, REAL_ADD_ASSOC] \\
fs [GSYM real_sub, REAL_SUB_REFL, GSYM REAL_NEG_RMUL, REAL_MUL_COMM]) \\
simp[] \\ match_mp_tac REAL_LE_TRANS \\
qexists_tac `maxAbsFun (e1lo, e1hi) * err2` \\ conj_tac \\ simp[] \\
qexists_tac `maxAbs (e1lo, e1hi) * err2` \\ conj_tac \\ simp[] \\
match_mp_tac REAL_LE_TRANS \\
qexists_tac `maxAbsFun (e1lo, e1hi) * err2 + maxAbsFun (e2lo, e2hi) * err1` \\
qexists_tac `maxAbs (e1lo, e1hi) * err2 + maxAbs (e2lo, e2hi) * err1` \\
conj_tac \\ simp[]))
>- (match_mp_tac REAL_LE_TRANS \\ qexists_tac `nR1 * nR2 + (nR1 + err1) * - nR2` \\ conj_tac
>- (fs [REAL_NEG_RMUL] \\ once_rewrite_tac [REAL_MUL_COMM] \\
......@@ -775,9 +743,9 @@ val validErrorboundCorrectMult = store_thm ("validErrorboundCorrectMult",
fs [GSYM REAL_SUB_LNEG, real_sub, REAL_LDISTRIB, REAL_NEG_MUL2, REAL_ADD_ASSOC] \\
fs [GSYM real_sub, REAL_SUB_REFL, GSYM REAL_NEG_RMUL, REAL_MUL_COMM]) \\
simp[] \\ match_mp_tac REAL_LE_TRANS \\
qexists_tac `maxAbsFun (e2lo, e2hi) * err1` \\ conj_tac \\ simp[] \\
qexists_tac `maxAbs (e2lo, e2hi) * err1` \\ conj_tac \\ simp[] \\
match_mp_tac REAL_LE_TRANS \\
qexists_tac `maxAbsFun (e1lo, e1hi) * err2 + maxAbsFun (e2lo, e2hi) * err1` \\
qexists_tac `maxAbs (e1lo, e1hi) * err2 + maxAbs (e2lo, e2hi) * err1` \\
conj_tac \\ simp[] \\
once_rewrite_tac [REAL_ADD_COMM] \\
simp[REAL_LE_ADDR])))))
......@@ -799,9 +767,9 @@ val validErrorboundCorrectMult = store_thm ("validErrorboundCorrectMult",
fs [GSYM REAL_SUB_LNEG, real_sub, REAL_LDISTRIB, REAL_NEG_MUL2, REAL_ADD_ASSOC] \\
fs [GSYM real_sub, REAL_SUB_REFL, GSYM REAL_NEG_RMUL, REAL_MUL_COMM]) \\
simp[] \\ match_mp_tac REAL_LE_TRANS \\
qexists_tac `maxAbsFun (e1lo, e1hi) * err2` \\ conj_tac \\ simp[] \\
qexists_tac `maxAbs (e1lo, e1hi) * err2` \\ conj_tac \\ simp[] \\