Commit 297e12b9 authored by Heiko Becker's avatar Heiko Becker
Browse files

Minor changes to proofs

parent d6aa770d
......@@ -8,8 +8,6 @@ open AbbrevsTheory ExpressionsTheory ExpressionSemanticsTheory RealSimpsTheory
FloverTactics MachineTypeTheory ExpressionAbbrevsTheory EnvironmentsTheory;
open preambleFloVer;
val _ = temp_delsimps ["NORMEQ_CONV"]
val _ = new_theory "ErrorBounds";
val _ = Parse.hide "delta"; (* so that it can be used as a variable *)
......@@ -394,6 +392,12 @@ Proof
\\ metis_tac [REAL_LE_LMUL_IMP, ABS_POS, REAL_MUL_COMM]
QED
Theorem nonzerop_EQ1_I'[simp]:
0 < r ==> (nonzerop r = 1)
Proof
rw[nonzerop_def]
QED
Theorem err_prop_inversion_pos:
!(nF:real) (nR:real) (err:real) (elo:real) (ehi:real).
0 < elo - err /\ 0 < elo /\
......@@ -402,7 +406,8 @@ Theorem err_prop_inversion_pos:
nR <= ehi /\
elo - err <= nF /\
nF <= ehi + err /\
0 <= err ==>
0 <=
err ==>
abs (inv nR - inv nF) <= err * inv ((elo - err) * (elo - err))
Proof
rpt strip_tac
......@@ -426,10 +431,9 @@ Proof
\\ simp[]
\\ qspec_then `1 / -nR + 1 / (nR - err)` match_mp_tac real_le_trans2 \\ conj_tac
>- (match_mp_tac REAL_LE_LADD_IMP
\\ rewrite_tac [GSYM REAL_INV_1OVER]
\\ 0 < nR - err nR - err nF suffices_by (fs [REAL_INV_LE_ANTIMONO])
\\ REAL_ASM_ARITH_TAC)
>- (` - nR <> 0 /\ nR - err <> 0` by REAL_ASM_ARITH_TAC
\\ 0 < nR - err nR - err nF by REAL_ASM_ARITH_TAC
\\ simp[GSYM REAL_INV_1OVER])
>- (`- nR <> 0 /\ nR - err <> 0` by REAL_ASM_ARITH_TAC
\\ fs [REAL_ADD_RAT]
\\ `nR - err + - nR = - err` by REAL_ASM_ARITH_TAC
\\ qspec_then `nR` (fn thm => fs [real_div, GSYM thm]) REAL_NEG_LMUL
......
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