Commit 945abf48 authored by Heiko Becker's avatar Heiko Becker
Browse files

Prove multiplication sound in HOL4

parent d09f63e5
......@@ -227,4 +227,681 @@ val validErrorboundCorrectSubtraction = store_thm ("validErrorboundCorrectSubtra
rule_assum_tac (fn thm => REWRITE_RULE [contained_def, IVlo_def, IVhi_def] thm) \\
simp[] ));
val validErrorboundCorrectMult = store_thm ("validErrorboundCorrectMult",
``!(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 Mult 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 Mult (Var 1) (Var 2)) nF /\
validErrorbound (Binop Mult e1 e2) absenv /\
validIntervalbounds (Binop Mult e1 e2) absenv P /\
(absenv e1 = ((e1lo,e1hi),err1)) /\
(absenv e2 = ((e2lo, e2hi),err2)) /\
(absenv (Binop Mult 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) \\
`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 \\
qexists_tac `e1` \\ qexists_tac `e2` \\ qexists_tac `cenv` \\ qexists_tac `P` \\
qexists_tac `err1` \\ qexists_tac `err2` \\
fs [])
>- (match_mp_tac REAL_LE_TRANS \\
qexists_tac `maxAbsFun (e1lo,e1hi) * err2 + maxAbsFun (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)`
by (match_mp_tac contained_leq_maxAbs_val \\ fs[contained_def, IVlo_def, IVhi_def]) \\
`nR2 <= maxAbsFun (e2lo, e2hi)`
by (match_mp_tac contained_leq_maxAbs_val \\ fs[contained_def, IVlo_def, IVhi_def]) \\
`-nR1 <= maxAbsFun (e1lo, e1hi)`
by (match_mp_tac contained_leq_maxAbs_neg_val \\ fs[contained_def, IVlo_def, IVhi_def]) \\
`-nR2 <= maxAbsFun (e2lo, e2hi)`
by (match_mp_tac contained_leq_maxAbs_neg_val \\ fs[contained_def, IVlo_def, IVhi_def]) \\
`nR1 * err2 <= maxAbsFun (e1lo, e1hi) * err2`
by (match_mp_tac REAL_LE_RMUL_IMP \\ fs[]) \\
`-nR1 * err2 <= maxAbsFun (e1lo, e1hi) * err2`
by (match_mp_tac REAL_LE_RMUL_IMP \\ fs[]) \\
`nR2 * err1 <= maxAbsFun (e2lo, e2hi) * err1`
by (match_mp_tac REAL_LE_RMUL_IMP \\ fs[]) \\
`-nR2 * err1 <= maxAbsFun (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`
by REAL_ASM_ARITH_TAC \\
`maxAbsFun (e1lo, e1hi) * err2 + maxAbsFun (e2lo, e2hi) * err1 <=
maxAbsFun (e1lo, e1hi) * err2 + maxAbsFun (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) \\
rpt (qpat_x_assum `validIntervalbounds _ _ _` kall_tac) \\
`! (x:real). ((abs x = x) /\ 0 < x) \/ ((abs x = - x) /\ x <= 0)` by REAL_ASM_ARITH_TAC \\
(* Large case distinction for
a) different cases of the value of Rabs (...) and
b) wether arguments of multiplication in (nf1 * nF2) are < or >= 0 *)
qpat_assum `!x. (A /\ B) \/ C` (fn thm => qspecl_then [`nR1 - nF1` ] DISJ_CASES_TAC thm) \\
qpat_assum `!x. (A /\ B) \/ C` (fn thm => qspecl_then [`nR2 - nF2` ] DISJ_CASES_TAC thm) \\
fs[] \\
rpt (qpat_x_assum `abs _ = _` (fn thm => RULE_ASSUM_TAC (fn thm2 => ONCE_REWRITE_RULE [thm] thm2)))
(* All positive *)
>- (`nF1 <= nR1 + err1` by (match_mp_tac err_up \\ simp[]) \\
`nF2 <= nR2 + err2` by (match_mp_tac err_up \\ simp[]) \\
qpat_assum `!x. (A /\ B) \/ C` (fn thm => qspecl_then [`nR1 * nR2 - nF1 * nF2` ] DISJ_CASES_TAC thm) \\
fs[real_sub]
(* Absolute value positive *)
>-(qspecl_then [`nF1`, `0`] DISJ_CASES_TAC REAL_LTE_TOTAL
>- (match_mp_tac REAL_LE_TRANS \\ qexists_tac `nR1 * nR2 + nF1 * (- (nR2 + err2))` \\ conj_tac
>- (fs [REAL_NEG_RMUL] \\ match_mp_tac REAL_MUL_LE_COMPAT_NEG_L \\ conj_tac
>- (match_mp_tac REAL_LT_IMP_LE \\ simp[])
>- (simp[REAL_LE_NEG]))
>- (qspecl_then [`- (nR2 + err2)`, `0`] DISJ_CASES_TAC REAL_LTE_TOTAL
>- (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] \\
match_mp_tac REAL_MUL_LE_COMPAT_NEG_L \\ conj_tac
>- (fs[] \\ match_mp_tac REAL_LT_IMP_LE \\ simp[])
>- (match_mp_tac REAL_LE_ADD_FLIP \\ simp[real_sub]))
>- (`nR1 * nR2 + (nR1 - err1) * - (nR2 + err2) = - nR1 * err2 + nR2 * err1 + err1 * err2`
by (fs[real_sub,REAL_RDISTRIB] \\
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_ADD2 \\ 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] \\
match_mp_tac REAL_LE_LMUL_IMP \\ conj_tac \\ fs[])
>- (`nR1 * nR2 + (nR1 + err1) * - (nR2 + err2) = - nR1 * err2 + - nR2 * err1 + - err1 * err2`
by (fs[real_sub,REAL_RDISTRIB] \\
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_ADD2 \\ conj_tac \\ TRY(simp[GSYM REAL_NEG_LMUL]) \\
match_mp_tac REAL_LE_ADD2 \\ conj_tac \\ simp[REAL_NEG_LMUL]))))
>- (match_mp_tac REAL_LE_TRANS \\ qexists_tac `nR1 * nR2 + nF1 * - (nR2 - err2)` \\ conj_tac
>- (fs [REAL_NEG_RMUL] \\ match_mp_tac REAL_LE_LMUL_IMP \\ conj_tac \\ simp[REAL_LE_NEG] \\
match_mp_tac REAL_LE_ADD_FLIP \\ simp[real_sub])
>- (qspecl_then [`- (nR2 - err2)`, `0`] DISJ_CASES_TAC REAL_LTE_TOTAL
>- (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] \\
match_mp_tac REAL_MUL_LE_COMPAT_NEG_L \\ conj_tac
>- (fs[] \\ match_mp_tac REAL_LT_IMP_LE \\ simp[])
>- (match_mp_tac REAL_LE_ADD_FLIP \\ simp[real_sub]))
>- (`nR1 * nR2 + (nR1 - err1) * - (nR2 - err2) = nR1 * err2 + nR2 * err1 + - err1 * err2`
by (fs[real_sub,REAL_RDISTRIB] \\
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_ADD2 \\ conj_tac \\ simp[GSYM REAL_NEG_LMUL] \\
match_mp_tac REAL_LE_ADD2 \\ conj_tac \\ simp[REAL_NEG_LMUL]))
>- (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] \\
match_mp_tac REAL_LE_LMUL_IMP \\ conj_tac \\ fs[])
>- (`nR1 * nR2 + (nR1 + err1) * - (nR2 - err2) = nR1 * err2 + - nR2 * err1 + err1 * err2`
by (fs[real_sub,REAL_RDISTRIB] \\
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_ADD2 \\ conj_tac \\ simp[GSYM REAL_NEG_LMUL] )))))
(* Absolute value negative *)
>- (simp[REAL_NEG_ADD] \\
qspecl_then [`nF1`, `0`] DISJ_CASES_TAC REAL_LTE_TOTAL
>- (match_mp_tac REAL_LE_TRANS \\ qexists_tac `-(nR1 * nR2) + nF1 * (nR2 - err2)` \\ conj_tac
>- (fs [REAL_NEG_RMUL] \\ match_mp_tac REAL_MUL_LE_COMPAT_NEG_L \\ conj_tac
>- (match_mp_tac REAL_LT_IMP_LE \\ simp[])
>- (match_mp_tac REAL_LE_ADD_FLIP \\ simp[real_sub]))
>- (qspecl_then [`nR2 - err2`, `0`] DISJ_CASES_TAC REAL_LTE_TOTAL
>- (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] \\
match_mp_tac REAL_MUL_LE_COMPAT_NEG_L \\ conj_tac
>- (fs[] \\ match_mp_tac REAL_LT_IMP_LE \\ simp[])
>- (match_mp_tac REAL_LE_ADD_FLIP \\ simp[real_sub]))
>- (`-(nR1 * nR2) + (nR1 - err1) * (nR2 - err2) = - nR1 * err2 + - nR2 * err1 + err1 * err2`
by (fs[real_sub,REAL_RDISTRIB] \\
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_ADD2 \\ 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] \\
match_mp_tac REAL_LE_LMUL_IMP \\ conj_tac \\ fs[])
>- (`-(nR1 * nR2) + (nR1 + err1) * (nR2 - err2) = - nR1 * err2 + nR2 * err1 + - err1 * err2`
by (fs[real_sub,REAL_RDISTRIB] \\
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_ADD2 \\ conj_tac \\ TRY(simp[GSYM REAL_NEG_LMUL]) \\
match_mp_tac REAL_LE_ADD2 \\ conj_tac \\ simp[REAL_NEG_LMUL]))))
>- (match_mp_tac REAL_LE_TRANS \\ qexists_tac `-(nR1 * nR2) + nF1 * (nR2 + err2)` \\ conj_tac
>- (fs [REAL_NEG_RMUL] \\ match_mp_tac REAL_LE_LMUL_IMP \\ conj_tac \\ simp[REAL_LE_NEG])
>- (qspecl_then [`nR2 + err2`, `0`] DISJ_CASES_TAC REAL_LTE_TOTAL
>- (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] \\
match_mp_tac REAL_MUL_LE_COMPAT_NEG_L \\ conj_tac
>- (fs[] \\ match_mp_tac REAL_LT_IMP_LE \\ simp[])
>- (match_mp_tac REAL_LE_ADD_FLIP \\ simp[real_sub]))
>- (`-(nR1 * nR2) + (nR1 - err1) * (nR2 + err2) = nR1 * err2 + - nR2 * err1 + - err1 * err2`
by (fs[real_sub,REAL_RDISTRIB] \\
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_ADD2 \\ conj_tac \\ simp[GSYM REAL_NEG_LMUL] \\
match_mp_tac REAL_LE_ADD2 \\ conj_tac \\ simp[REAL_NEG_LMUL]))
>- (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] \\
match_mp_tac REAL_LE_LMUL_IMP \\ conj_tac \\ fs[])
>- (`-(nR1 * nR2) + (nR1 + err1) * (nR2 + err2) = nR1 * err2 + nR2 * err1 + err1 * err2`
by (fs[real_sub,REAL_RDISTRIB] \\
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_ADD2 \\ conj_tac \\ simp[GSYM REAL_NEG_LMUL]))))))
(* First positive, second negative *)
>- (`nF1 <= nR1 + err1` by (match_mp_tac err_up \\ simp[]) \\
`nF2 <= nR2 + err2`
by (once_rewrite_tac[REAL_ADD_COMM] \\ simp [GSYM REAL_LE_SUB_RADD] \\
once_rewrite_tac [REAL_ADD_COMM, GSYM REAL_NEG_SUB] \\ simp[] ) \\
qpat_assum `!x. (A /\ B) \/ C` (fn thm => qspecl_then [`nR1 * nR2 - nF1 * nF2` ] DISJ_CASES_TAC thm) \\
fs[real_sub]
(* Absolute value positive *)
>-(qspecl_then [`nF1`, `0`] DISJ_CASES_TAC REAL_LTE_TOTAL
>- (match_mp_tac REAL_LE_TRANS \\ qexists_tac `nR1 * nR2 + nF1 * (- (nR2 + err2))` \\ conj_tac
>- (fs [REAL_NEG_RMUL] \\ match_mp_tac REAL_MUL_LE_COMPAT_NEG_L \\ conj_tac
>- (match_mp_tac REAL_LT_IMP_LE \\ simp[])
>- (simp[REAL_LE_NEG]))
>- (qspecl_then [`- (nR2 + err2)`, `0`] DISJ_CASES_TAC REAL_LTE_TOTAL
>- (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] \\
match_mp_tac REAL_MUL_LE_COMPAT_NEG_L \\ conj_tac
>- (fs[] \\ match_mp_tac REAL_LT_IMP_LE \\ simp[])
>- (match_mp_tac REAL_LE_ADD_FLIP \\ simp[real_sub]))
>- (`nR1 * nR2 + (nR1 - err1) * - (nR2 + err2) = - nR1 * err2 + nR2 * err1 + err1 * err2`
by (fs[real_sub,REAL_RDISTRIB] \\
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_ADD2 \\ 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] \\
match_mp_tac REAL_LE_LMUL_IMP \\ conj_tac \\ fs[])
>- (`nR1 * nR2 + (nR1 + err1) * - (nR2 + err2) = - nR1 * err2 + - nR2 * err1 + - err1 * err2`
by (fs[real_sub,REAL_RDISTRIB] \\
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_ADD2 \\ conj_tac \\ TRY(simp[GSYM REAL_NEG_LMUL]) \\
match_mp_tac REAL_LE_ADD2 \\ conj_tac \\ simp[REAL_NEG_LMUL]))))
>- (match_mp_tac REAL_LE_TRANS \\ qexists_tac `nR1 * nR2 + nF1 * -nR2` \\ conj_tac
>- (fs [REAL_NEG_RMUL] \\ match_mp_tac REAL_LE_LMUL_IMP \\ conj_tac \\ simp[REAL_LE_NEG] \\
qpat_x_assum `nR2 + - nF2 <= _ `
(fn thm => ASSUME_TAC (SIMP_RULE bool_ss [GSYM real_sub, REAL_LE_SUB_RADD, REAL_ADD_LID] thm))\\
simp[])
>- (qspecl_then [`- nR2`, `0`] DISJ_CASES_TAC REAL_LTE_TOTAL
>- (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] \\
match_mp_tac REAL_MUL_LE_COMPAT_NEG_L \\ conj_tac
>- (fs[] \\ match_mp_tac REAL_LT_IMP_LE \\ simp[])
>- (match_mp_tac REAL_LE_ADD_FLIP \\ simp[real_sub]))
>- (`nR1 * nR2 + (nR1 - err1) * - nR2 = nR2 * err1`
by (fs[real_sub,REAL_RDISTRIB] \\
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[] \\
match_mp_tac REAL_LE_TRANS \\
qexists_tac `maxAbsFun (e1lo, e1hi) * err2 + maxAbsFun (e2lo, e2hi) * err1` \\
conj_tac \\ simp[] \\
once_rewrite_tac [REAL_ADD_COMM] \\
simp [REAL_LE_ADDR]))
>- (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] \\
match_mp_tac REAL_LE_LMUL_IMP \\ conj_tac \\ fs[])
>- (`nR1 * nR2 + (nR1 + err1) * - nR2 = - nR2 * err1`
by (fs[real_sub,REAL_RDISTRIB] \\
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[] \\
match_mp_tac REAL_LE_TRANS \\
qexists_tac `maxAbsFun (e1lo, e1hi) * err2 + maxAbsFun (e2lo, e2hi) * err1` \\
conj_tac \\ simp[] \\
once_rewrite_tac [REAL_ADD_COMM] \\
simp [REAL_LE_ADDR])))))
(* Absolute value negative *)
>- (simp[REAL_NEG_ADD] \\
qspecl_then [`nF1`, `0`] DISJ_CASES_TAC REAL_LTE_TOTAL
>- (match_mp_tac REAL_LE_TRANS \\ qexists_tac `-(nR1 * nR2) + nF1 * nR2` \\ conj_tac
>- (fs [REAL_NEG_RMUL] \\ match_mp_tac REAL_MUL_LE_COMPAT_NEG_L \\ conj_tac
>- (match_mp_tac REAL_LT_IMP_LE \\ simp[])
>- (qpat_x_assum `nR2 + - nF2 <= _ `
(fn thm => ASSUME_TAC (SIMP_RULE bool_ss [GSYM real_sub, REAL_LE_SUB_RADD, REAL_ADD_LID] thm))\\
simp[]))
>- (qspecl_then [`nR2`, `0`] DISJ_CASES_TAC REAL_LTE_TOTAL
>- (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] \\
match_mp_tac REAL_MUL_LE_COMPAT_NEG_L \\ conj_tac
>- (fs[] \\ match_mp_tac REAL_LT_IMP_LE \\ simp[])
>- (match_mp_tac REAL_LE_ADD_FLIP \\ simp[real_sub]))
>- (`-(nR1 * nR2) + (nR1 - err1) * nR2 = - nR2 * err1`
by (fs[real_sub,REAL_RDISTRIB] \\
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[] \\
match_mp_tac REAL_LE_TRANS \\
qexists_tac `maxAbsFun (e1lo, e1hi) * err2 + maxAbsFun (e2lo, e2hi) * err1` \\
conj_tac \\ simp[] \\
once_rewrite_tac [REAL_ADD_COMM] \\
simp [REAL_LE_ADDR]))
>- (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] \\
match_mp_tac REAL_LE_LMUL_IMP \\ conj_tac \\ fs[])
>- (`-(nR1 * nR2) + (nR1 + err1) * nR2 = nR2 * err1`
by (fs[real_sub,REAL_RDISTRIB] \\
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[] \\
match_mp_tac REAL_LE_TRANS \\
qexists_tac `maxAbsFun (e1lo, e1hi) * err2 + maxAbsFun (e2lo, e2hi) * err1` \\
conj_tac \\ simp[] \\
once_rewrite_tac [REAL_ADD_COMM] \\
simp [REAL_LE_ADDR]))))
>- (match_mp_tac REAL_LE_TRANS \\ qexists_tac `-(nR1 * nR2) + nF1 * (nR2 + err2)` \\ conj_tac
>- (fs [REAL_NEG_RMUL] \\ match_mp_tac REAL_LE_LMUL_IMP \\ conj_tac \\ simp[REAL_LE_NEG])
>- (qspecl_then [`nR2 + err2`, `0`] DISJ_CASES_TAC REAL_LTE_TOTAL
>- (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] \\
match_mp_tac REAL_MUL_LE_COMPAT_NEG_L \\ conj_tac
>- (fs[] \\ match_mp_tac REAL_LT_IMP_LE \\ simp[])
>- (match_mp_tac REAL_LE_ADD_FLIP \\ simp[real_sub]))
>- (`-(nR1 * nR2) + (nR1 - err1) * (nR2 + err2) = nR1 * err2 + - nR2 * err1 + - err1 * err2`
by (fs[real_sub,REAL_RDISTRIB] \\
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_ADD2 \\ conj_tac \\ simp[GSYM REAL_NEG_LMUL] \\
match_mp_tac REAL_LE_ADD2 \\ conj_tac \\ simp[REAL_NEG_LMUL]))
>- (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] \\
match_mp_tac REAL_LE_LMUL_IMP \\ conj_tac \\ fs[])
>- (`-(nR1 * nR2) + (nR1 + err1) * (nR2 + err2) = nR1 * err2 + nR2 * err1 + err1 * err2`
by (fs[real_sub,REAL_RDISTRIB] \\
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_ADD2 \\ conj_tac \\ simp[GSYM REAL_NEG_LMUL]))))))
(* First negative, second positive *)
>- (`nF2 <= nR2 + err2` by (match_mp_tac err_up \\ simp[]) \\
`nF1 <= nR1 + err1`
by (once_rewrite_tac[REAL_ADD_COMM] \\ simp [GSYM REAL_LE_SUB_RADD] \\
once_rewrite_tac [REAL_ADD_COMM, GSYM REAL_NEG_SUB] \\ simp[]) \\
qpat_assum `!x. (A /\ B) \/ C` (fn thm => qspecl_then [`nR1 * nR2 - nF1 * nF2` ] DISJ_CASES_TAC thm) \\
fs[real_sub]
(* Absolute value positive *)
>-(qspecl_then [`nF1`, `0`] DISJ_CASES_TAC REAL_LTE_TOTAL
>- (match_mp_tac REAL_LE_TRANS \\ qexists_tac `nR1 * nR2 + nF1 * - (nR2 + err2)` \\ conj_tac
>- (fs [REAL_NEG_RMUL] \\ match_mp_tac REAL_MUL_LE_COMPAT_NEG_L \\ conj_tac
>- (match_mp_tac REAL_LT_IMP_LE \\ simp[])
>- (simp[REAL_LE_NEG]))
>- (qspecl_then [`- (nR2 + err2)`, `0`] DISJ_CASES_TAC REAL_LTE_TOTAL
>- (match_mp_tac REAL_LE_TRANS \\ qexists_tac `nR1 * nR2 + nR1 * - (nR2 + err2)` \\ conj_tac
>- (fs [REAL_NEG_RMUL] \\ once_rewrite_tac [REAL_MUL_COMM] \\
match_mp_tac REAL_MUL_LE_COMPAT_NEG_L \\ conj_tac
>- (fs[] \\ match_mp_tac REAL_LT_IMP_LE \\ simp[])
>- (qpat_x_assum `nR1 + - nF1 <= _ `
(fn thm => ASSUME_TAC (SIMP_RULE bool_ss [GSYM real_sub, REAL_LE_SUB_RADD, REAL_ADD_LID] thm))\\
simp[]))
>- (`nR1 * nR2 + nR1 * - (nR2 + err2) = - nR1 * err2`
by (fs[real_sub,REAL_RDISTRIB] \\
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[] \\
match_mp_tac REAL_LE_TRANS \\
qexists_tac `maxAbsFun (e1lo, e1hi) * err2 + maxAbsFun (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] \\
match_mp_tac REAL_LE_LMUL_IMP \\ conj_tac \\ fs[])
>- (`nR1 * nR2 + (nR1 + err1) * - (nR2 + err2) = - nR1 * err2 + - nR2 * err1 + - err1 * err2`
by (fs[real_sub,REAL_RDISTRIB] \\
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_ADD2 \\ conj_tac \\ TRY(simp[GSYM REAL_NEG_LMUL]) \\
match_mp_tac REAL_LE_ADD2 \\ conj_tac \\ simp[REAL_NEG_LMUL]))))
>- (match_mp_tac REAL_LE_TRANS \\ qexists_tac `nR1 * nR2 + nF1 * - (nR2 - err2)` \\ conj_tac
>- (fs [REAL_NEG_RMUL] \\ match_mp_tac REAL_LE_LMUL_IMP \\ conj_tac \\ simp[REAL_LE_NEG] \\
match_mp_tac REAL_LE_ADD_FLIP \\ simp[real_sub])
>- (qspecl_then [`- (nR2 - err2)`, `0`] DISJ_CASES_TAC REAL_LTE_TOTAL
>- (match_mp_tac REAL_LE_TRANS \\ qexists_tac `nR1 * nR2 + nR1 * - (nR2 - err2)` \\ conj_tac
>- (fs [REAL_NEG_RMUL] \\ once_rewrite_tac [REAL_MUL_COMM] \\
match_mp_tac REAL_MUL_LE_COMPAT_NEG_L \\ conj_tac
>- (fs[] \\ match_mp_tac REAL_LT_IMP_LE \\ simp[])
>- (qpat_x_assum `nR1 + - nF1 <= _ `
(fn thm => ASSUME_TAC (SIMP_RULE bool_ss [GSYM real_sub, REAL_LE_SUB_RADD, REAL_ADD_LID] thm))\\
simp[]))
>- (`nR1 * nR2 + nR1 * - (nR2 - err2) = nR1 * err2`
by (fs[real_sub,REAL_RDISTRIB] \\
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[] \\
match_mp_tac REAL_LE_TRANS \\
qexists_tac `maxAbsFun (e1lo, e1hi) * err2 + maxAbsFun (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] \\
match_mp_tac REAL_LE_LMUL_IMP \\ conj_tac \\ fs[])
>- (`nR1 * nR2 + (nR1 + err1) * - (nR2 - err2) = nR1 * err2 + - nR2 * err1 + err1 * err2`
by (fs[real_sub,REAL_RDISTRIB] \\
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_ADD2 \\ conj_tac \\ simp[GSYM REAL_NEG_LMUL] )))))
(* Absolute value negative *)
>- (simp[REAL_NEG_ADD] \\
qspecl_then [`nF1`, `0`] DISJ_CASES_TAC REAL_LTE_TOTAL
>- (match_mp_tac REAL_LE_TRANS \\ qexists_tac `-(nR1 * nR2) + nF1 * (nR2 - err2)` \\ conj_tac
>- (fs [REAL_NEG_RMUL] \\ match_mp_tac REAL_MUL_LE_COMPAT_NEG_L \\ conj_tac
>- (match_mp_tac REAL_LT_IMP_LE \\ simp[])
>- (match_mp_tac REAL_LE_ADD_FLIP \\ simp[real_sub]))
>- (qspecl_then [`nR2 - err2`, `0`] DISJ_CASES_TAC REAL_LTE_TOTAL
>- (match_mp_tac REAL_LE_TRANS \\ qexists_tac `-(nR1 * nR2) + nR1 * (nR2 - err2)` \\ conj_tac
>- (fs [REAL_NEG_RMUL] \\ once_rewrite_tac [REAL_MUL_COMM] \\
match_mp_tac REAL_MUL_LE_COMPAT_NEG_L \\ conj_tac
>- (fs[] \\ match_mp_tac REAL_LT_IMP_LE \\ simp[])
>- (qpat_x_assum `nR1 + - nF1 <= _ `
(fn thm => ASSUME_TAC (SIMP_RULE bool_ss [GSYM real_sub, REAL_LE_SUB_RADD, REAL_ADD_LID] thm))\\
simp[]))
>- (`-(nR1 * nR2) + nR1 * (nR2 - err2) = - nR1 * err2`
by (fs[real_sub,REAL_RDISTRIB] \\
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[] \\
match_mp_tac REAL_LE_TRANS \\
qexists_tac `maxAbsFun (e1lo, e1hi) * err2 + maxAbsFun (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] \\
match_mp_tac REAL_LE_LMUL_IMP \\ conj_tac \\ fs[])
>- (`-(nR1 * nR2) + (nR1 + err1) * (nR2 - err2) = - nR1 * err2 + nR2 * err1 + - err1 * err2`
by (fs[real_sub,REAL_RDISTRIB] \\
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_ADD2 \\ conj_tac \\ TRY(simp[GSYM REAL_NEG_LMUL]) \\
match_mp_tac REAL_LE_ADD2 \\ conj_tac \\ simp[REAL_NEG_LMUL]))))
>- (match_mp_tac REAL_LE_TRANS \\ qexists_tac `-(nR1 * nR2) + nF1 * (nR2 + err2)` \\ conj_tac
>- (fs [REAL_NEG_RMUL] \\ match_mp_tac REAL_LE_LMUL_IMP \\ conj_tac \\ simp[REAL_LE_NEG])
>- (qspecl_then [`nR2 + err2`, `0`] DISJ_CASES_TAC REAL_LTE_TOTAL
>- (match_mp_tac REAL_LE_TRANS \\ qexists_tac `-(nR1 * nR2) + nR1 * (nR2 + err2)` \\ conj_tac
>- (fs [REAL_NEG_RMUL] \\ once_rewrite_tac [REAL_MUL_COMM] \\
match_mp_tac REAL_MUL_LE_COMPAT_NEG_L \\ conj_tac
>- (fs[] \\ match_mp_tac REAL_LT_IMP_LE \\ simp[])
>- (qpat_x_assum `nR1 + - nF1 <= _ `
(fn thm => ASSUME_TAC (SIMP_RULE bool_ss [GSYM real_sub, REAL_LE_SUB_RADD, REAL_ADD_LID] thm))\\
simp[]))
>- (`-(nR1 * nR2) + nR1 * (nR2 + err2) = nR1 * err2`
by (fs[real_sub,REAL_RDISTRIB] \\
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[] \\
match_mp_tac REAL_LE_TRANS \\
qexists_tac `maxAbsFun (e1lo, e1hi) * err2 + maxAbsFun (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] \\
match_mp_tac REAL_LE_LMUL_IMP \\ conj_tac \\ fs[])
>- (`-(nR1 * nR2) + (nR1 + err1) * (nR2 + err2) = nR1 * err2 + nR2 * err1 + err1 * err2`
by (fs[real_sub,REAL_RDISTRIB] \\
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_ADD2 \\ conj_tac \\ simp[GSYM REAL_NEG_LMUL]))))))
(* Both negative *)
>- (`nF1 <= nR1 + err1`
by (once_rewrite_tac[REAL_ADD_COMM] \\ simp [GSYM REAL_LE_SUB_RADD] \\
once_rewrite_tac [REAL_ADD_COMM, GSYM REAL_NEG_SUB] \\ simp[]) \\
`nF2 <= nR2 + err2`
by (once_rewrite_tac[REAL_ADD_COMM] \\ simp [GSYM REAL_LE_SUB_RADD] \\
once_rewrite_tac [REAL_ADD_COMM, GSYM REAL_NEG_SUB] \\ simp[]) \\
`nR1 <= nF1`
by (qpat_x_assum `nR1 - nF1 <= _ `
(fn thm => ASSUME_TAC (SIMP_RULE bool_ss [GSYM real_sub, REAL_LE_SUB_RADD, REAL_ADD_LID] thm))\\
simp[]) \\
`nR2 <= nF2`
by (qpat_x_assum `nR2 - nF2 <= _ `
(fn thm => ASSUME_TAC (SIMP_RULE bool_ss [GSYM real_sub, REAL_LE_SUB_RADD, REAL_ADD_LID] thm))\\
simp[]) \\
qpat_assum `!x. (A /\ B) \/ C` (fn thm => qspecl_then [`nR1 * nR2 - nF1 * nF2` ] DISJ_CASES_TAC thm) \\
fs[real_sub]
(* Absolute value positive *)
>-(qspecl_then [`nF1`, `0`] DISJ_CASES_TAC REAL_LTE_TOTAL
>- (match_mp_tac REAL_LE_TRANS \\ qexists_tac `nR1 * nR2 + nF1 * - (nR2 + err2)` \\ conj_tac
>- (fs [REAL_NEG_RMUL] \\ match_mp_tac REAL_MUL_LE_COMPAT_NEG_L \\ conj_tac
>- (match_mp_tac REAL_LT_IMP_LE \\ simp[])
>- (simp[REAL_LE_NEG]))
>- (qspecl_then [`- (nR2 + err2)`, `0`] DISJ_CASES_TAC REAL_LTE_TOTAL
>- (match_mp_tac REAL_LE_TRANS \\ qexists_tac `nR1 * nR2 + nR1 * - (nR2 + err2)` \\ conj_tac
>- (fs [REAL_NEG_RMUL] \\ once_rewrite_tac [REAL_MUL_COMM] \\
match_mp_tac REAL_MUL_LE_COMPAT_NEG_L \\ conj_tac
>- (fs[] \\ match_mp_tac REAL_LT_IMP_LE \\ simp[])
>- (qpat_x_assum `nR1 + - nF1 <= _ `
(fn thm => ASSUME_TAC (SIMP_RULE bool_ss [GSYM real_sub, REAL_LE_SUB_RADD, REAL_ADD_LID] thm))\\
simp[]))
>- (`nR1 * nR2 + nR1 * - (nR2 + err2) = - nR1 * err2`
by (fs[real_sub,REAL_RDISTRIB] \\
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[] \\
match_mp_tac REAL_LE_TRANS \\
qexists_tac `maxAbsFun (e1lo, e1hi) * err2 + maxAbsFun (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] \\
match_mp_tac REAL_LE_LMUL_IMP \\ conj_tac \\ fs[])
>- (`nR1 * nR2 + (nR1 + err1) * - (nR2 + err2) = - nR1 * err2 + - nR2 * err1 + - err1 * err2`
by (fs[real_sub,REAL_RDISTRIB] \\
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_ADD2 \\ conj_tac \\ TRY(simp[GSYM REAL_NEG_LMUL]) \\
match_mp_tac REAL_LE_ADD2 \\ conj_tac \\ simp[REAL_NEG_LMUL]))))
>- (match_mp_tac REAL_LE_TRANS \\ qexists_tac `nR1 * nR2 + nF1 * - nR2` \\ conj_tac
>- (fs [REAL_NEG_RMUL] \\ match_mp_tac REAL_LE_LMUL_IMP \\ conj_tac \\ simp[REAL_LE_NEG] \\
match_mp_tac REAL_LE_ADD_FLIP \\ simp[real_sub])
>- (qspecl_then [`- nR2`, `0`] DISJ_CASES_TAC REAL_LTE_TOTAL
>- (match_mp_tac REAL_LE_TRANS \\ qexists_tac `nR1 * nR2 + nR1 * - nR2` \\ conj_tac
>- (fs [REAL_NEG_RMUL] \\ once_rewrite_tac [REAL_MUL_COMM] \\
match_mp_tac REAL_MUL_LE_COMPAT_NEG_L \\ conj_tac
>- (fs[] \\ match_mp_tac REAL_LT_IMP_LE \\ simp[])
>- (simp[]))
>- (`nR1 * nR2 + nR1 * - nR2 = 0`
by (fs[real_sub,REAL_RDISTRIB] \\
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[] \\
match_mp_tac REAL_LE_TRANS \\
qexists_tac `maxAbsFun (e1lo, e1hi) * err2 + maxAbsFun (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] \\
match_mp_tac REAL_LE_LMUL_IMP \\ conj_tac \\ fs[])
>- (`nR1 * nR2 + (nR1 + err1) * - nR2 = - nR2 * err1`
by (fs[real_sub,REAL_RDISTRIB] \\
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[] \\
match_mp_tac REAL_LE_TRANS \\
qexists_tac `maxAbsFun (e1lo, e1hi) * err2 + maxAbsFun (e2lo, e2hi) * err1` \\
conj_tac \\ simp[] \\
once_rewrite_tac [REAL_ADD_COMM] \\
simp[REAL_LE_ADDR])))))