Commit 065ad7bf authored by Heiko Becker's avatar Heiko Becker
Browse files

Proof Style improved for multiplication proof

parent bfc37fb7
......@@ -271,48 +271,53 @@ val validErrorboundCorrectMult = store_thm ("validErrorboundCorrectMult",
err1 * err2 +
maxAbs (multInterval (widenInterval (e1lo,e1hi) err1)
(widenInterval (e2lo,e2hi) err2)) * machineEpsilon`
\\ conj_tac \\ TRY(simp[]) \\
\\ 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 <= maxAbs (e2lo, e2hi)`
by (match_mp_tac contained_leq_maxAbs_val \\ fs[contained_def, IVlo_def, IVhi_def]) \\
`-nR1 <= maxAbs (e1lo, e1hi)`
by (match_mp_tac contained_leq_maxAbs_neg_val \\ fs[contained_def, IVlo_def, IVhi_def]) \\
`-nR2 <= maxAbs (e2lo, e2hi)`
by (match_mp_tac contained_leq_maxAbs_neg_val \\ fs[contained_def, IVlo_def, IVhi_def]) \\
`nR1 * err2 <= maxAbs (e1lo, e1hi) * err2`
by (match_mp_tac REAL_LE_RMUL_IMP \\ fs[]) \\
`-nR1 * err2 <= maxAbs (e1lo, e1hi) * err2`
by (match_mp_tac REAL_LE_RMUL_IMP \\ fs[]) \\
`nR2 * err1 <= maxAbs (e2lo, e2hi) * err1`
by (match_mp_tac REAL_LE_RMUL_IMP \\ fs[]) \\
`-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 <= 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 \\
`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) \\
`! (x:real). ((abs x = x) /\ 0 < x) \/ ((abs x = - x) /\ x <= 0)` by REAL_ASM_ARITH_TAC \\
by (match_mp_tac contained_leq_maxAbs_val
\\ fs[contained_def, IVlo_def, IVhi_def])
\\ `nR2 <= maxAbs (e2lo, e2hi)`
by (match_mp_tac contained_leq_maxAbs_val
\\ fs[contained_def, IVlo_def, IVhi_def])
\\`-nR1 <= maxAbs (e1lo, e1hi)`
by (match_mp_tac contained_leq_maxAbs_neg_val
\\ fs[contained_def, IVlo_def, IVhi_def])
\\ `-nR2 <= maxAbs (e2lo, e2hi)`
by (match_mp_tac contained_leq_maxAbs_neg_val
\\ fs[contained_def, IVlo_def, IVhi_def])
\\ `nR1 * err2 <= maxAbs (e1lo, e1hi) * err2`
by (match_mp_tac REAL_LE_RMUL_IMP \\ fs[])
\\ `-nR1 * err2 <= maxAbs (e1lo, e1hi) * err2`
by (match_mp_tac REAL_LE_RMUL_IMP \\ fs[])
\\ `nR2 * err1 <= maxAbs (e2lo, e2hi) * err1`
by (match_mp_tac REAL_LE_RMUL_IMP \\ fs[])
\\ `-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 <= 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
\\ `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)
\\ `! (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)))
\\ 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 *)
>- (`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
......@@ -455,30 +460,30 @@ val validErrorboundCorrectMult = store_thm ("validErrorboundCorrectMult",
>- (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 `maxAbs (e2lo,e2hi) * err1` \\ conj_tac \\ simp[] \\
match_mp_tac REAL_LE_TRANS \\
qexists_tac `maxAbs (e1lo, e1hi) * err2 + maxAbs (e2lo, e2hi) * err1` \\
conj_tac \\ simp[] \\
once_rewrite_tac [REAL_ADD_COMM] \\
simp [REAL_LE_ADDR]))
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 `maxAbs (e2lo,e2hi) * err1` \\ conj_tac \\ simp[]
\\ match_mp_tac REAL_LE_TRANS
\\ qexists_tac `maxAbs (e1lo, e1hi) * err2 + maxAbs (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 `maxAbs (e2lo,e2hi) * err1` \\ conj_tac \\ simp[] \\
match_mp_tac REAL_LE_TRANS \\
qexists_tac `maxAbs (e1lo, e1hi) * err2 + maxAbs (e2lo, e2hi) * err1` \\
conj_tac \\ simp[] \\
once_rewrite_tac [REAL_ADD_COMM] \\
simp [REAL_LE_ADDR])))))
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 `maxAbs (e2lo,e2hi) * err1` \\ conj_tac \\ simp[]
\\ match_mp_tac REAL_LE_TRANS
\\ qexists_tac `maxAbs (e1lo, e1hi) * err2 + maxAbs (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
......@@ -486,8 +491,10 @@ val validErrorboundCorrectMult = store_thm ("validErrorboundCorrectMult",
>- (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[]))
(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] \\
......@@ -495,30 +502,30 @@ val validErrorboundCorrectMult = store_thm ("validErrorboundCorrectMult",
>- (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 `maxAbs (e2lo,e2hi) * err1` \\ conj_tac \\ simp[] \\
match_mp_tac REAL_LE_TRANS \\
qexists_tac `maxAbs (e1lo, e1hi) * err2 + maxAbs (e2lo, e2hi) * err1` \\
conj_tac \\ simp[] \\
once_rewrite_tac [REAL_ADD_COMM] \\
simp [REAL_LE_ADDR]))
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 `maxAbs (e2lo,e2hi) * err1` \\ conj_tac \\ simp[]
\\ match_mp_tac REAL_LE_TRANS
\\ qexists_tac `maxAbs (e1lo, e1hi) * err2 + maxAbs (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 `maxAbs (e2lo,e2hi) * err1` \\ conj_tac \\ simp[] \\
match_mp_tac REAL_LE_TRANS \\
qexists_tac `maxAbs (e1lo, e1hi) * err2 + maxAbs (e2lo, e2hi) * err1` \\
conj_tac \\ simp[] \\
once_rewrite_tac [REAL_ADD_COMM] \\
simp [REAL_LE_ADDR]))))
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 `maxAbs (e2lo,e2hi) * err1` \\ conj_tac \\ simp[]
\\ match_mp_tac REAL_LE_TRANS
\\ qexists_tac `maxAbs (e1lo, e1hi) * err2 + maxAbs (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
......@@ -563,23 +570,23 @@ val validErrorboundCorrectMult = store_thm ("validErrorboundCorrectMult",
(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 `maxAbs (e1lo, e1hi) * err2` \\ conj_tac \\ simp[] \\
match_mp_tac REAL_LE_TRANS \\
qexists_tac `maxAbs (e1lo, e1hi) * err2 + maxAbs (e2lo, e2hi) * err1` \\
conj_tac \\ simp[]))
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 `maxAbs (e1lo, e1hi) * err2` \\ conj_tac \\ simp[]
\\ match_mp_tac REAL_LE_TRANS
\\ 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] \\
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]))))
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])
......@@ -589,25 +596,27 @@ val validErrorboundCorrectMult = store_thm ("validErrorboundCorrectMult",
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[]))
(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 `maxAbs (e1lo, e1hi) * err2` \\ conj_tac \\ simp[] \\
match_mp_tac REAL_LE_TRANS \\
qexists_tac `maxAbs (e1lo, e1hi) * err2 + maxAbs (e2lo, e2hi) * err1` \\
conj_tac \\ simp[]))
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 `maxAbs (e1lo, e1hi) * err2` \\ conj_tac \\ simp[]
\\ match_mp_tac REAL_LE_TRANS
\\ 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] \\
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] )))))
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
......@@ -621,26 +630,29 @@ val validErrorboundCorrectMult = store_thm ("validErrorboundCorrectMult",
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[]))
(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 `maxAbs (e1lo, e1hi) * err2` \\ conj_tac \\ simp[] \\
match_mp_tac REAL_LE_TRANS \\
qexists_tac `maxAbs (e1lo, e1hi) * err2 + maxAbs (e2lo, e2hi) * err1` \\
conj_tac \\ simp[]))
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 `maxAbs (e1lo, e1hi) * err2` \\ conj_tac \\ simp[]
\\ match_mp_tac REAL_LE_TRANS
\\ 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] \\
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]))))
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
......@@ -649,17 +661,19 @@ val validErrorboundCorrectMult = store_thm ("validErrorboundCorrectMult",
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[]))
(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 `maxAbs (e1lo, e1hi) * err2` \\ conj_tac \\ simp[] \\
match_mp_tac REAL_LE_TRANS \\
qexists_tac `maxAbs (e1lo, e1hi) * err2 + maxAbs (e2lo, e2hi) * err1` \\
conj_tac \\ simp[]))
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 `maxAbs (e1lo, e1hi) * err2` \\ conj_tac \\ simp[]
\\ match_mp_tac REAL_LE_TRANS
\\ 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] \\
match_mp_tac REAL_LE_LMUL_IMP \\ conj_tac \\ fs[])
......@@ -670,22 +684,28 @@ val validErrorboundCorrectMult = store_thm ("validErrorboundCorrectMult",
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 *)
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
......@@ -697,26 +717,35 @@ val validErrorboundCorrectMult = store_thm ("validErrorboundCorrectMult",
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[]))
(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 `maxAbs (e1lo, e1hi) * err2` \\ conj_tac \\ simp[] \\
match_mp_tac REAL_LE_TRANS \\
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] \\
match_mp_tac REAL_LE_LMUL_IMP \\ conj_tac \\ fs[])
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 `maxAbs (e1lo, e1hi) * err2`
\\ conj_tac \\ simp[]
\\ match_mp_tac REAL_LE_TRANS
\\ 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]
\\ 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]))))
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])
......@@ -727,28 +756,29 @@ val validErrorboundCorrectMult = store_thm ("validErrorboundCorrectMult",
>- (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 `maxAbs (e1lo, e1hi) * err2` \\ conj_tac \\ simp[] \\
match_mp_tac REAL_LE_TRANS \\
qexists_tac `maxAbs (e1lo, e1hi) * err2 + maxAbs (e2lo, e2hi) * err1` \\
conj_tac \\ simp[]))
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 `maxAbs (e1lo, e1hi) * err2`
\\ conj_tac \\ simp[]
\\ match_mp_tac REAL_LE_TRANS
\\ 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] \\
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 `maxAbs (e2lo, e2hi) * err1` \\ conj_tac \\ simp[] \\
match_mp_tac REAL_LE_TRANS \\
qexists_tac `maxAbs (e1lo, e1hi) * err2 + maxAbs (e2lo, e2hi) * err1` \\
conj_tac \\ simp[] \\
once_rewrite_tac [REAL_ADD_COMM] \\
simp[REAL_LE_ADDR])))))
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 `maxAbs (e2lo, e2hi) * err1` \\ conj_tac \\ simp[]
\\ match_mp_tac REAL_LE_TRANS
\\ qexists_tac `maxAbs (e1lo, e1hi) * err2 + maxAbs (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
......@@ -763,28 +793,29 @@ val validErrorboundCorrectMult = store_thm ("validErrorboundCorrectMult",
>- (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 `maxAbs (e1lo, e1hi) * err2` \\ conj_tac \\ simp[] \\
match_mp_tac REAL_LE_TRANS \\
qexists_tac `maxAbs (e1lo, e1hi) * err2 + maxAbs (e2lo, e2hi) * err1` \\
conj_tac \\ simp[]))
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 `maxAbs (e1lo, e1hi) * err2` \\ conj_tac \\ simp[]
\\ match_mp_tac REAL_LE_TRANS
\\ 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] \\
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 `maxAbs (e2lo, e2hi) * err1` \\ conj_tac \\ simp[] \\
match_mp_tac REAL_LE_TRANS \\
qexists_tac `maxAbs (e1lo, e1hi) * err2 + maxAbs (e2lo, e2hi) * err1` \\
conj_tac \\ simp[] \\
once_rewrite_tac [REAL_ADD_COMM] \\
simp[REAL_LE_ADDR]))))
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 `maxAbs (e2lo, e2hi) * err1`
\\ conj_tac \\ simp[]
\\ match_mp_tac REAL_LE_TRANS
\\ qexists_tac `maxAbs (e1lo, e1hi) * err2 + maxAbs (e2lo, e2hi) * err1`