From 297e12b9c48206dcfbdb26569c43e51d38a6378d Mon Sep 17 00:00:00 2001
From: Heiko Becker <hbecker@mpi-sws.org>
Date: Thu, 23 Jul 2020 12:15:08 +0200
Subject: [PATCH] Minor changes to proofs
---
hol4/ErrorBoundsScript.sml | 18 +++++++++++-------
1 file changed, 11 insertions(+), 7 deletions(-)
diff --git a/hol4/ErrorBoundsScript.sml b/hol4/ErrorBoundsScript.sml
index 6569247e..f488aa05 100644
--- a/hol4/ErrorBoundsScript.sml
+++ b/hol4/ErrorBoundsScript.sml
@@ -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
--
GitLab