From dfdd8e026a43924d99527f9ce5e1f35898166faa Mon Sep 17 00:00:00 2001
From: Heiko Becker <hbecker@mpi-sws.org>
Date: Tue, 12 Jul 2022 12:21:15 +0200
Subject: [PATCH] Fix FloVer for latest HOL4 master changes
---
hol4/CertificateCheckerScript.sml | 2 +-
hol4/EnvironmentsScript.sml | 2 +-
hol4/ErrorBoundsScript.sml | 2 +-
hol4/ErrorValidationScript.sml | 462 +++++++++----------
hol4/FPRangeValidatorScript.sml | 2 +-
hol4/IEEE_connectionScript.sml | 2 +-
hol4/IEEE_reverseScript.sml | 74 +--
hol4/Infra/FloverCompLib.sml | 3 +
hol4/Infra/Holmakefile | 2 -
hol4/Infra/MachineTypeScript.sml | 43 +-
hol4/Infra/RealSimpsScript.sml | 4 +-
hol4/Infra/ResultsLib.sml | 3 +
hol4/IntervalArithScript.sml | 6 +-
hol4/IntervalValidationScript.sml | 6 +-
hol4/TypeValidatorScript.sml | 18 +-
hol4/semantics/ExpressionSemanticsScript.sml | 23 +-
hol4/semantics/ExpressionsScript.sml | 14 +-
hol4/semantics/expressionsLib.sml | 85 ++++
18 files changed, 438 insertions(+), 315 deletions(-)
create mode 100644 hol4/semantics/expressionsLib.sml
diff --git a/hol4/CertificateCheckerScript.sml b/hol4/CertificateCheckerScript.sml
index bb2936dd..dd227771 100644
--- a/hol4/CertificateCheckerScript.sml
+++ b/hol4/CertificateCheckerScript.sml
@@ -14,7 +14,7 @@ open preambleFloVer;
val _ = new_theory "CertificateChecker";
-Overload abs[local] = “real$absâ€;
+Overload abs[local] = “realax$absâ€;
(** Certificate checking function **)
Definition CertificateChecker_def:
diff --git a/hol4/EnvironmentsScript.sml b/hol4/EnvironmentsScript.sml
index 4c9afa6b..257d1314 100644
--- a/hol4/EnvironmentsScript.sml
+++ b/hol4/EnvironmentsScript.sml
@@ -10,7 +10,7 @@ open preambleFloVer;
val _ = new_theory "Environments";
-Overload abs[local] = “real$absâ€
+Overload abs[local] = “realax$absâ€
Definition approxEnv_def:
approxEnv E1 Gamma absEnv (fVars:num_set) (dVars:num_set) E2 =
diff --git a/hol4/ErrorBoundsScript.sml b/hol4/ErrorBoundsScript.sml
index 28f75c3b..36c39c35 100644
--- a/hol4/ErrorBoundsScript.sml
+++ b/hol4/ErrorBoundsScript.sml
@@ -12,7 +12,7 @@ val _ = new_theory "ErrorBounds";
val _ = Parse.hide "delta"; (* so that it can be used as a variable *)
-Overload abs[local] = “real$absâ€
+Overload abs[local] = “realax$absâ€
val triangle_tac =
irule triangle_trans \\ rpt conj_tac \\ TRY (fs[REAL_ABS_TRIANGLE] \\ NO_TAC);
diff --git a/hol4/ErrorValidationScript.sml b/hol4/ErrorValidationScript.sml
index cf7df26f..3f4f4fc2 100644
--- a/hol4/ErrorValidationScript.sml
+++ b/hol4/ErrorValidationScript.sml
@@ -18,7 +18,7 @@ val _ = new_theory "ErrorValidation";
val _ = Parse.hide "delta"; (* so that it can be used as a variable *)
-Overload abs[local] = “real$absâ€
+Overload abs[local] = “realax$absâ€
val _ = realLib.prefer_real();
@@ -1074,15 +1074,15 @@ Proof
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
- \\ `0 <= maxAbs (invertInterval (e2lo, e2hi)) * err1` by REAL_ASM_ARITH_TAC
+ \\ OLD_REAL_ASM_ARITH_TAC)
+ \\ `0 <= maxAbs (e1lo, e1hi) * err2` by OLD_REAL_ASM_ARITH_TAC
+ \\ `0 <= maxAbs (invertInterval (e2lo, e2hi)) * err1` by OLD_REAL_ASM_ARITH_TAC
\\ `maxAbs (e1lo, e1hi) * err2 <=
maxAbs (e1lo, e1hi) * err2 + maxAbs (invertInterval (e2lo, e2hi)) * err1`
- by (REAL_ASM_ARITH_TAC)
+ by (OLD_REAL_ASM_ARITH_TAC)
\\ `maxAbs (e1lo, e1hi) * err2 + maxAbs (invertInterval(e2lo, e2hi)) * err1 <=
maxAbs (e1lo, e1hi) * err2 + maxAbs (invertInterval (e2lo, e2hi)) * err1 + err1 * err2`
- by REAL_ASM_ARITH_TAC
+ by OLD_REAL_ASM_ARITH_TAC
(* Case distinction for divisor range
positive or negative in float and real valued execution *)
\\ fs [IVlo_def, IVhi_def, widenInterval_def, contained_def, noDivzero_def]
@@ -1091,32 +1091,32 @@ Proof
by (match_mp_tac err_prop_inversion_neg \\ qexists_tac `e2lo` \\simp[])
\\ fs [widenInterval_def, IVlo_def, IVhi_def]
\\ `minAbsFun (e2lo - err2, e2hi + err2) = - (e2hi + err2)`
- by (match_mp_tac minAbs_negative_iv_is_hi \\ REAL_ASM_ARITH_TAC)
+ by (match_mp_tac minAbs_negative_iv_is_hi \\ OLD_REAL_ASM_ARITH_TAC)
\\ simp[]
\\ qpat_x_assum `minAbsFun _ = _ ` kall_tac
- \\ `nF1 <= err1 + nR1` by REAL_ASM_ARITH_TAC
- \\ `nR1 - err1 <= nF1` by REAL_ASM_ARITH_TAC
+ \\ `nF1 <= err1 + nR1` by OLD_REAL_ASM_ARITH_TAC
+ \\ `nR1 - err1 <= nF1` by OLD_REAL_ASM_ARITH_TAC
\\ `(nR2 - nF2 > 0 /\ nR2 - nF2 <= err2) \/ (nR2 - nF2 <= 0 /\ - (nR2 - nF2) <= err2)`
- by REAL_ASM_ARITH_TAC
+ by OLD_REAL_ASM_ARITH_TAC
(* Positive case for abs (nR2 - nF2) <= err2 *)
- >- (`nF2 < nR2` by REAL_ASM_ARITH_TAC
+ >- (`nF2 < nR2` by OLD_REAL_ASM_ARITH_TAC
\\ qpat_x_assum `nF2 < nR2` (fn thm => assume_tac (ONCE_REWRITE_RULE [GSYM REAL_LT_NEG] thm))
- \\ `inv (- nF2) < inv (- nR2)` by (match_mp_tac REAL_LT_INV \\ REAL_ASM_ARITH_TAC)
- \\ `inv (- nF2) = - (inv nF2)` by (match_mp_tac (GSYM REAL_NEG_INV) \\ REAL_ASM_ARITH_TAC)
- \\ `inv (- nR2) = - (inv nR2)` by (match_mp_tac (GSYM REAL_NEG_INV) \\ REAL_ASM_ARITH_TAC)
+ \\ `inv (- nF2) < inv (- nR2)` by (match_mp_tac REAL_LT_INV \\ OLD_REAL_ASM_ARITH_TAC)
+ \\ `inv (- nF2) = - (inv nF2)` by (match_mp_tac (GSYM REAL_NEG_INV) \\ OLD_REAL_ASM_ARITH_TAC)
+ \\ `inv (- nR2) = - (inv nR2)` by (match_mp_tac (GSYM REAL_NEG_INV) \\ OLD_REAL_ASM_ARITH_TAC)
\\ rpt (qpat_x_assum `inv (- _) = - (inv _)`
(fn thm => rule_assum_tac (fn hyp => REWRITE_RULE [thm] hyp)))
- \\ `inv nR2 < inv nF2` by REAL_ASM_ARITH_TAC
+ \\ `inv nR2 < inv nF2` by OLD_REAL_ASM_ARITH_TAC
\\ qpat_x_assum `- _ < - _` kall_tac
- \\ `inv nR2 - inv nF2 < 0` by REAL_ASM_ARITH_TAC
+ \\ `inv nR2 - inv nF2 < 0` by OLD_REAL_ASM_ARITH_TAC
\\ `- (nR2â»Â¹ − nF2â»Â¹) ≤ err2 * ((e2hi + err2) * (e2hi + err2))â»Â¹`
- by REAL_ASM_ARITH_TAC
+ by OLD_REAL_ASM_ARITH_TAC
\\ `inv nF2 <= inv nR2 + err2 * inv ((e2hi + err2) * (e2hi + err2))`
- by REAL_ASM_ARITH_TAC
+ by OLD_REAL_ASM_ARITH_TAC
\\ `inv nR2 - err2 * inv ((e2hi + err2) * (e2hi + err2)) <= inv nF2`
- by REAL_ASM_ARITH_TAC
+ by OLD_REAL_ASM_ARITH_TAC
(* Next do a case distinction for the absolute value *)
- \\ `! (x:real). ((abs x = x) /\ 0 <= x) \/ ((abs x = - x) /\ x < 0)` by REAL_ASM_ARITH_TAC
+ \\ `! (x:real). ((abs x = x) /\ 0 <= x) \/ ((abs x = - x) /\ x < 0)` by OLD_REAL_ASM_ARITH_TAC
\\ qpat_x_assum `!x. A /\ B \/ C`
(fn thm =>
qspec_then `(nR1:real / nR2:real) - (nF1:real / nF2:real)`
@@ -1131,7 +1131,7 @@ Proof
\\ conj_tac
>- (fs[REAL_LE_LADD]
\\ match_mp_tac REAL_MUL_LE_COMPAT_NEG_L
- \\ conj_tac \\ REAL_ASM_ARITH_TAC)
+ \\ conj_tac \\ OLD_REAL_ASM_ARITH_TAC)
>- (qabbrev_tac `err_inv = (err2 * ((e2hi + err2) * (e2hi + err2))â»Â¹)`
\\ qspecl_then [`inv nR2 - err_inv`, `0`] DISJ_CASES_TAC REAL_LTE_TOTAL
>- (match_mp_tac REAL_LE_TRANS
@@ -1140,30 +1140,30 @@ Proof
>- (fs [REAL_LE_ADD]
\\ once_rewrite_tac [REAL_MUL_COMM]
\\ match_mp_tac REAL_MUL_LE_COMPAT_NEG_L
- \\ conj_tac \\ TRY REAL_ASM_ARITH_TAC
+ \\ conj_tac \\ TRY OLD_REAL_ASM_ARITH_TAC
\\ fs [REAL_LE_NEG])
>- (`nR1 * inv nR2 + - (nR1 + err1) * (inv nR2 - err_inv) =
nR1 * err_inv + - (inv nR2) * err1 + err1 * err_inv`
- by REAL_ASM_ARITH_TAC
+ by OLD_REAL_ASM_ARITH_TAC
\\ simp[REAL_NEG_MUL2]
\\ qspecl_then [`inv ((e2hi + err2) * (e2hi + err2))`,`err2`]
(fn thm => once_rewrite_tac [thm]) REAL_MUL_COMM
\\ qunabbrev_tac `err_inv`
\\ match_mp_tac REAL_LE_ADD2
- \\ conj_tac \\ TRY REAL_ASM_ARITH_TAC
+ \\ conj_tac \\ TRY OLD_REAL_ASM_ARITH_TAC
\\ match_mp_tac REAL_LE_ADD2
- \\ conj_tac \\ TRY REAL_ASM_ARITH_TAC
+ \\ conj_tac \\ TRY OLD_REAL_ASM_ARITH_TAC
\\ match_mp_tac REAL_LE_RMUL_IMP
- \\ conj_tac \\ REAL_ASM_ARITH_TAC))
+ \\ conj_tac \\ OLD_REAL_ASM_ARITH_TAC))
>- (match_mp_tac REAL_LE_TRANS
\\ qexists_tac `nR1 * inv nR2 + - (nR1 + - err1) * (inv nR2 - err_inv)`
\\ conj_tac
>- (fs [REAL_LE_ADD]
\\ match_mp_tac REAL_LE_RMUL_IMP
- \\ conj_tac \\ REAL_ASM_ARITH_TAC)
+ \\ conj_tac \\ OLD_REAL_ASM_ARITH_TAC)
>- (`nR1 * inv nR2 + - (nR1 + - err1) * (inv nR2 - err_inv) =
nR1 * err_inv + inv nR2 * err1 - err1 * err_inv`
- by REAL_ASM_ARITH_TAC
+ by OLD_REAL_ASM_ARITH_TAC
\\ simp[REAL_NEG_MUL2]
\\ qspecl_then [`inv ((e2hi + err2) * (e2hi + err2))`,`err2`]
(fn thm => once_rewrite_tac [thm]) REAL_MUL_COMM
@@ -1172,19 +1172,19 @@ Proof
\\ match_mp_tac REAL_LE_ADD2
\\ conj_tac
>- (match_mp_tac REAL_LE_ADD2
- \\ conj_tac \\ TRY REAL_ASM_ARITH_TAC
+ \\ conj_tac \\ TRY OLD_REAL_ASM_ARITH_TAC
\\ match_mp_tac REAL_LE_RMUL_IMP
- \\ conj_tac \\ REAL_ASM_ARITH_TAC)
+ \\ conj_tac \\ OLD_REAL_ASM_ARITH_TAC)
>- (simp [REAL_NEG_LMUL]
\\ match_mp_tac REAL_LE_RMUL_IMP
- \\ conj_tac \\ REAL_ASM_ARITH_TAC)))))
+ \\ conj_tac \\ OLD_REAL_ASM_ARITH_TAC)))))
(* 0 <= - nF1 *)
>- (match_mp_tac REAL_LE_TRANS
\\ qexists_tac `nR1 * inv nR2 + - nF1 * (inv nR2 + err2 * inv ((e2hi + err2) * (e2hi + err2)))`
\\ conj_tac
>- (fs[REAL_LE_LADD]
\\ match_mp_tac REAL_LE_LMUL_IMP
- \\ conj_tac \\ REAL_ASM_ARITH_TAC)
+ \\ conj_tac \\ OLD_REAL_ASM_ARITH_TAC)
>- (qabbrev_tac `err_inv = (err2 * ((e2hi + err2) * (e2hi + err2))â»Â¹)`
\\ qspecl_then [`inv nR2 + err_inv`, `0`] DISJ_CASES_TAC REAL_LTE_TOTAL
>- (match_mp_tac REAL_LE_TRANS
@@ -1193,11 +1193,11 @@ Proof
>- (fs [REAL_LE_ADD] \\
once_rewrite_tac [REAL_MUL_COMM] \\
match_mp_tac REAL_MUL_LE_COMPAT_NEG_L\\
- conj_tac \\ TRY REAL_ASM_ARITH_TAC \\
+ conj_tac \\ TRY OLD_REAL_ASM_ARITH_TAC \\
fs [REAL_LE_NEG])
>- (`nR1 * inv nR2 + - (nR1 + err1) * (inv nR2 + err_inv) =
- nR1 * err_inv + - (inv nR2) * err1 - err1 * err_inv`
- by REAL_ASM_ARITH_TAC \\
+ by OLD_REAL_ASM_ARITH_TAC \\
simp[REAL_NEG_MUL2] \\
qspecl_then [`inv ((e2hi + err2) * (e2hi + err2))`,`err2`]
(fn thm => once_rewrite_tac [thm]) REAL_MUL_COMM \\
@@ -1206,31 +1206,31 @@ Proof
match_mp_tac REAL_LE_ADD2 \\
conj_tac
>- (match_mp_tac REAL_LE_ADD2 \\
- conj_tac \\ TRY REAL_ASM_ARITH_TAC \\
+ conj_tac \\ TRY OLD_REAL_ASM_ARITH_TAC \\
match_mp_tac REAL_LE_RMUL_IMP \\
- conj_tac \\ REAL_ASM_ARITH_TAC)
+ conj_tac \\ OLD_REAL_ASM_ARITH_TAC)
>- (simp [REAL_NEG_LMUL] \\
match_mp_tac REAL_LE_RMUL_IMP \\
- conj_tac \\ REAL_ASM_ARITH_TAC)))
+ conj_tac \\ OLD_REAL_ASM_ARITH_TAC)))
>- (match_mp_tac REAL_LE_TRANS \\
qexists_tac `nR1 * inv nR2 + - (nR1 + - err1) * (inv nR2 + err_inv)` \\
conj_tac
>- (fs [REAL_LE_ADD] \\
match_mp_tac REAL_LE_RMUL_IMP \\
- conj_tac \\ REAL_ASM_ARITH_TAC)
+ conj_tac \\ OLD_REAL_ASM_ARITH_TAC)
>- (`nR1 * inv nR2 + - (nR1 + - err1) * (inv nR2 + err_inv) =
- nR1 * err_inv + inv nR2 * err1 + err1 * err_inv`
- by REAL_ASM_ARITH_TAC \\
+ by OLD_REAL_ASM_ARITH_TAC \\
simp[REAL_NEG_MUL2] \\
qspecl_then [`inv ((e2hi + err2) * (e2hi + err2))`,`err2`]
(fn thm => once_rewrite_tac [thm]) REAL_MUL_COMM \\
qunabbrev_tac `err_inv` \\
match_mp_tac REAL_LE_ADD2 \\
- conj_tac \\ TRY REAL_ASM_ARITH_TAC \\
+ conj_tac \\ TRY OLD_REAL_ASM_ARITH_TAC \\
match_mp_tac REAL_LE_ADD2 \\
- conj_tac \\ TRY REAL_ASM_ARITH_TAC \\
+ conj_tac \\ TRY OLD_REAL_ASM_ARITH_TAC \\
match_mp_tac REAL_LE_RMUL_IMP \\
- conj_tac \\ REAL_ASM_ARITH_TAC)))))
+ conj_tac \\ OLD_REAL_ASM_ARITH_TAC)))))
(* Case 2: Absolute value negative *)
>- (fs[real_sub, real_div, REAL_NEG_LMUL, REAL_NEG_ADD] \\
qspecl_then [`nF1`, `0`] DISJ_CASES_TAC REAL_LTE_TOTAL
@@ -1240,7 +1240,7 @@ Proof
conj_tac
>- (fs[REAL_LE_LADD] \\
match_mp_tac REAL_MUL_LE_COMPAT_NEG_L \\
- conj_tac \\ REAL_ASM_ARITH_TAC)
+ conj_tac \\ OLD_REAL_ASM_ARITH_TAC)
>- (qabbrev_tac `err_inv = (err2 * ((e2hi + err2) * (e2hi + err2))â»Â¹)` \\
qspecl_then [`inv nR2 - err_inv`, `0`] DISJ_CASES_TAC REAL_LTE_TOTAL
>- (match_mp_tac REAL_LE_TRANS \\
@@ -1249,31 +1249,31 @@ Proof
>- (fs [REAL_LE_ADD] \\
once_rewrite_tac [REAL_MUL_COMM] \\
match_mp_tac REAL_MUL_LE_COMPAT_NEG_L\\
- conj_tac \\ TRY REAL_ASM_ARITH_TAC \\
+ conj_tac \\ TRY OLD_REAL_ASM_ARITH_TAC \\
fs [REAL_LE_NEG])
>- (`- nR1 * inv nR2 + (nR1 - err1) * (inv nR2 - err_inv) =
- nR1 * err_inv + - (inv nR2) * err1 + err1 * err_inv`
- by REAL_ASM_ARITH_TAC \\
+ by OLD_REAL_ASM_ARITH_TAC \\
simp[REAL_NEG_MUL2] \\
qspecl_then [`inv ((-e2hi + -err2) * (-e2hi + -err2))`,`err2`]
(fn thm => once_rewrite_tac [thm]) REAL_MUL_COMM \\
qunabbrev_tac `err_inv` \\
match_mp_tac REAL_LE_ADD2 \\
- conj_tac \\ TRY REAL_ASM_ARITH_TAC \\
+ conj_tac \\ TRY OLD_REAL_ASM_ARITH_TAC \\
match_mp_tac REAL_LE_ADD2 \\
- conj_tac \\ TRY REAL_ASM_ARITH_TAC \\
+ conj_tac \\ TRY OLD_REAL_ASM_ARITH_TAC \\
fs [GSYM REAL_NEG_ADD, REAL_NEG_MUL2] \\
match_mp_tac REAL_LE_RMUL_IMP \\
- conj_tac \\ REAL_ASM_ARITH_TAC))
+ conj_tac \\ OLD_REAL_ASM_ARITH_TAC))
>- (match_mp_tac REAL_LE_TRANS \\
qexists_tac `- nR1 * inv nR2 + (nR1 + err1) * (inv nR2 - err_inv)` \\
conj_tac
>- (fs [REAL_LE_ADD] \\
match_mp_tac REAL_LE_RMUL_IMP \\
- conj_tac \\ REAL_ASM_ARITH_TAC)
+ conj_tac \\ OLD_REAL_ASM_ARITH_TAC)
>- (`- nR1 * inv nR2 + (nR1 + err1) * (inv nR2 - err_inv) =
- nR1 * err_inv + inv nR2 * err1 - err1 * err_inv`
- by REAL_ASM_ARITH_TAC \\
+ by OLD_REAL_ASM_ARITH_TAC \\
simp[REAL_NEG_MUL2] \\
qspecl_then [`inv ((-e2hi + -err2) * (-e2hi + -err2))`,`err2`]
(fn thm => once_rewrite_tac [thm]) REAL_MUL_COMM \\
@@ -1282,20 +1282,20 @@ Proof
match_mp_tac REAL_LE_ADD2 \\
conj_tac
>- (match_mp_tac REAL_LE_ADD2 \\
- conj_tac \\ TRY REAL_ASM_ARITH_TAC \\
+ conj_tac \\ TRY OLD_REAL_ASM_ARITH_TAC \\
fs [GSYM REAL_NEG_ADD, REAL_NEG_MUL2] \\
match_mp_tac REAL_LE_RMUL_IMP \\
- conj_tac \\ REAL_ASM_ARITH_TAC)
+ conj_tac \\ OLD_REAL_ASM_ARITH_TAC)
>- (fs [GSYM REAL_NEG_ADD, REAL_NEG_MUL2, REAL_NEG_LMUL] \\
match_mp_tac REAL_LE_RMUL_IMP \\
- conj_tac \\ REAL_ASM_ARITH_TAC)))))
+ conj_tac \\ OLD_REAL_ASM_ARITH_TAC)))))
(* 0 <= - nF1 *)
>- (match_mp_tac REAL_LE_TRANS \\
qexists_tac `- nR1 * inv nR2 + nF1 * (inv nR2 + err2 * inv ((e2hi + err2) * (e2hi + err2)))` \\
conj_tac
>- (fs[REAL_LE_LADD] \\
match_mp_tac REAL_LE_LMUL_IMP \\
- conj_tac \\ REAL_ASM_ARITH_TAC)
+ conj_tac \\ OLD_REAL_ASM_ARITH_TAC)
>- (qabbrev_tac `err_inv = (err2 * ((e2hi + err2) * (e2hi + err2))â»Â¹)` \\
qspecl_then [`inv nR2 + err_inv`, `0`] DISJ_CASES_TAC REAL_LTE_TOTAL
>- (match_mp_tac REAL_LE_TRANS \\
@@ -1304,11 +1304,11 @@ Proof
>- (fs [REAL_LE_ADD] \\
once_rewrite_tac [REAL_MUL_COMM] \\
match_mp_tac REAL_MUL_LE_COMPAT_NEG_L\\
- conj_tac \\ TRY REAL_ASM_ARITH_TAC \\
+ conj_tac \\ TRY OLD_REAL_ASM_ARITH_TAC \\
fs [REAL_LE_NEG])
>- (`- nR1 * inv nR2 + (nR1 - err1) * (inv nR2 + err_inv) =
nR1 * err_inv + - (inv nR2) * err1 - err1 * err_inv`
- by REAL_ASM_ARITH_TAC \\
+ by OLD_REAL_ASM_ARITH_TAC \\
simp[REAL_NEG_MUL2] \\
qspecl_then [`inv ((-e2hi + -err2) * (-e2hi + -err2))`,`err2`]
(fn thm => once_rewrite_tac [thm]) REAL_MUL_COMM \\
@@ -1317,51 +1317,51 @@ Proof
match_mp_tac REAL_LE_ADD2 \\
conj_tac
>- (match_mp_tac REAL_LE_ADD2 \\
- conj_tac \\ TRY REAL_ASM_ARITH_TAC \\
+ conj_tac \\ TRY OLD_REAL_ASM_ARITH_TAC \\
fs [GSYM REAL_NEG_ADD, REAL_NEG_MUL2, REAL_NEG_LMUL] \\
match_mp_tac REAL_LE_RMUL_IMP \\
- conj_tac \\ REAL_ASM_ARITH_TAC)
+ conj_tac \\ OLD_REAL_ASM_ARITH_TAC)
>- (fs [GSYM REAL_NEG_ADD, REAL_NEG_MUL2, REAL_NEG_LMUL, REAL_NEG_LMUL] \\
match_mp_tac REAL_LE_RMUL_IMP \\
- conj_tac \\ REAL_ASM_ARITH_TAC)))
+ conj_tac \\ OLD_REAL_ASM_ARITH_TAC)))
>- (match_mp_tac REAL_LE_TRANS \\
qexists_tac `- nR1 * inv nR2 + (nR1 + err1) * (inv nR2 + err_inv)` \\
conj_tac
>- (fs [REAL_LE_ADD] \\
match_mp_tac REAL_LE_RMUL_IMP \\
- conj_tac \\ REAL_ASM_ARITH_TAC)
+ conj_tac \\ OLD_REAL_ASM_ARITH_TAC)
>- (`- nR1 * inv nR2 + (nR1 + err1) * (inv nR2 + err_inv) =
nR1 * err_inv + inv nR2 * err1 + err1 * err_inv`
- by REAL_ASM_ARITH_TAC \\
+ by OLD_REAL_ASM_ARITH_TAC \\
simp[REAL_NEG_MUL2] \\
qspecl_then [`inv ((-e2hi + -err2) * (-e2hi + -err2))`,`err2`]
(fn thm => once_rewrite_tac [thm]) REAL_MUL_COMM \\
qunabbrev_tac `err_inv` \\
match_mp_tac REAL_LE_ADD2 \\
- conj_tac \\ TRY REAL_ASM_ARITH_TAC \\
+ conj_tac \\ TRY OLD_REAL_ASM_ARITH_TAC \\
match_mp_tac REAL_LE_ADD2 \\
- conj_tac \\ TRY REAL_ASM_ARITH_TAC \\
+ conj_tac \\ TRY OLD_REAL_ASM_ARITH_TAC \\
fs [GSYM REAL_NEG_ADD, REAL_NEG_MUL2, REAL_NEG_LMUL] \\
match_mp_tac REAL_LE_RMUL_IMP \\
- conj_tac \\ REAL_ASM_ARITH_TAC))))))
+ conj_tac \\ OLD_REAL_ASM_ARITH_TAC))))))
(* Negative case for abs (nR2 - nF2) <= err2 *)
>- (fs [GSYM REAL_NEG_ADD, REAL_NEG_MUL2, REAL_NEG_LMUL] \\
- `nR2 <= nF2` by REAL_ASM_ARITH_TAC \\
+ `nR2 <= nF2` by OLD_REAL_ASM_ARITH_TAC \\
qpat_x_assum `nR2 <= nF2` (fn thm => assume_tac (ONCE_REWRITE_RULE [GSYM REAL_LE_NEG] thm)) \\
- `inv (- nR2) <= inv (- nF2)` by (match_mp_tac REAL_INV_LE_ANTIMONO_IMPR \\ REAL_ASM_ARITH_TAC) \\
- `inv (- nR2) = - (inv nR2)` by (match_mp_tac (GSYM REAL_NEG_INV) \\ REAL_ASM_ARITH_TAC) \\
- `inv (- nF2) = - (inv nF2)` by (match_mp_tac (GSYM REAL_NEG_INV) \\ REAL_ASM_ARITH_TAC) \\
+ `inv (- nR2) <= inv (- nF2)` by (match_mp_tac REAL_INV_LE_ANTIMONO_IMPR \\ OLD_REAL_ASM_ARITH_TAC) \\
+ `inv (- nR2) = - (inv nR2)` by (match_mp_tac (GSYM REAL_NEG_INV) \\ OLD_REAL_ASM_ARITH_TAC) \\
+ `inv (- nF2) = - (inv nF2)` by (match_mp_tac (GSYM REAL_NEG_INV) \\ OLD_REAL_ASM_ARITH_TAC) \\
rpt (
qpat_x_assum `inv (- _) = - (inv _)`
(fn thm => rule_assum_tac (fn hyp => REWRITE_RULE [thm] hyp))) \\
- `inv nF2 <= inv nR2` by REAL_ASM_ARITH_TAC \\
+ `inv nF2 <= inv nR2` by OLD_REAL_ASM_ARITH_TAC \\
qpat_x_assum `- _ <= - _` kall_tac \\
- `0 <= inv nR2 - inv nF2` by REAL_ASM_ARITH_TAC \\
- `(nR2â»Â¹ − nF2â»Â¹) ≤ err2 * ((e2hi + err2) * (e2hi + err2))â»Â¹` by REAL_ASM_ARITH_TAC \\
- `inv nF2 <= inv nR2 + err2 * inv ((e2hi + err2) * (e2hi + err2))` by REAL_ASM_ARITH_TAC \\
- `inv nR2 - err2 * inv ((e2hi + err2) * (e2hi + err2)) <= inv nF2` by REAL_ASM_ARITH_TAC \\
+ `0 <= inv nR2 - inv nF2` by OLD_REAL_ASM_ARITH_TAC \\
+ `(nR2â»Â¹ − nF2â»Â¹) ≤ err2 * ((e2hi + err2) * (e2hi + err2))â»Â¹` by OLD_REAL_ASM_ARITH_TAC \\
+ `inv nF2 <= inv nR2 + err2 * inv ((e2hi + err2) * (e2hi + err2))` by OLD_REAL_ASM_ARITH_TAC \\
+ `inv nR2 - err2 * inv ((e2hi + err2) * (e2hi + err2)) <= inv nF2` by OLD_REAL_ASM_ARITH_TAC \\
(* Next do a case distinction for the absolute value *)
- `! (x:real). ((abs x = x) /\ 0 <= x) \/ ((abs x = - x) /\ x < 0)` by REAL_ASM_ARITH_TAC \\
+ `! (x:real). ((abs x = x) /\ 0 <= x) \/ ((abs x = - x) /\ x < 0)` by OLD_REAL_ASM_ARITH_TAC \\
qpat_x_assum `!x. A /\ B \/ C`
(fn thm => qspec_then `(nR1:real / nR2:real) - (nF1:real / nF2:real)` DISJ_CASES_TAC thm) \\
fs[real_sub, real_div, REAL_NEG_LMUL, REAL_NEG_ADD, realTheory.abs]
@@ -1373,7 +1373,7 @@ Proof
conj_tac
>- (fs[REAL_LE_LADD] \\
match_mp_tac REAL_MUL_LE_COMPAT_NEG_L \\
- conj_tac \\ REAL_ASM_ARITH_TAC)
+ conj_tac \\ OLD_REAL_ASM_ARITH_TAC)
>- (qabbrev_tac `err_inv = (err2 * ((e2hi + err2) * (e2hi + err2))â»Â¹)` \\
qspecl_then [`inv nR2 - err_inv`, `0`] DISJ_CASES_TAC REAL_LTE_TOTAL
>- (match_mp_tac REAL_LE_TRANS \\
@@ -1382,30 +1382,30 @@ Proof
>- (fs [REAL_LE_ADD] \\
once_rewrite_tac [REAL_MUL_COMM] \\
match_mp_tac REAL_MUL_LE_COMPAT_NEG_L\\
- conj_tac \\ TRY REAL_ASM_ARITH_TAC \\
+ conj_tac \\ TRY OLD_REAL_ASM_ARITH_TAC \\
fs [REAL_LE_NEG])
>- (`nR1 * inv nR2 + - (nR1 + err1) * (inv nR2 - err_inv) =
nR1 * err_inv + - (inv nR2) * err1 + err1 * err_inv`
- by REAL_ASM_ARITH_TAC \\
+ by OLD_REAL_ASM_ARITH_TAC \\
simp[REAL_NEG_MUL2] \\
qspecl_then [`inv ((e2hi + err2) * (e2hi + err2))`,`err2`]
(fn thm => once_rewrite_tac [thm]) REAL_MUL_COMM \\
qunabbrev_tac `err_inv` \\
match_mp_tac REAL_LE_ADD2 \\
- conj_tac \\ TRY REAL_ASM_ARITH_TAC \\
+ conj_tac \\ TRY OLD_REAL_ASM_ARITH_TAC \\
match_mp_tac REAL_LE_ADD2 \\
- conj_tac \\ TRY REAL_ASM_ARITH_TAC \\
+ conj_tac \\ TRY OLD_REAL_ASM_ARITH_TAC \\
match_mp_tac REAL_LE_RMUL_IMP \\
- conj_tac \\ REAL_ASM_ARITH_TAC))
+ conj_tac \\ OLD_REAL_ASM_ARITH_TAC))
>- (match_mp_tac REAL_LE_TRANS \\
qexists_tac `nR1 * inv nR2 + - (nR1 + - err1) * (inv nR2 - err_inv)` \\
conj_tac
>- (fs [REAL_LE_ADD] \\
match_mp_tac REAL_LE_RMUL_IMP \\
- conj_tac \\ REAL_ASM_ARITH_TAC)
+ conj_tac \\ OLD_REAL_ASM_ARITH_TAC)
>- (`nR1 * inv nR2 + - (nR1 + - err1) * (inv nR2 - err_inv) =
nR1 * err_inv + inv nR2 * err1 - err1 * err_inv`
- by REAL_ASM_ARITH_TAC \\
+ by OLD_REAL_ASM_ARITH_TAC \\
simp[REAL_NEG_MUL2] \\
qspecl_then [`inv ((e2hi + err2) * (e2hi + err2))`,`err2`]
(fn thm => once_rewrite_tac [thm]) REAL_MUL_COMM \\
@@ -1414,19 +1414,19 @@ Proof
match_mp_tac REAL_LE_ADD2 \\
conj_tac
>- (match_mp_tac REAL_LE_ADD2 \\
- conj_tac \\ TRY REAL_ASM_ARITH_TAC \\
+ conj_tac \\ TRY OLD_REAL_ASM_ARITH_TAC \\
match_mp_tac REAL_LE_RMUL_IMP \\
- conj_tac \\ REAL_ASM_ARITH_TAC)
+ conj_tac \\ OLD_REAL_ASM_ARITH_TAC)
>- (simp [REAL_NEG_LMUL] \\
match_mp_tac REAL_LE_RMUL_IMP \\
- conj_tac \\ REAL_ASM_ARITH_TAC)))))
+ conj_tac \\ OLD_REAL_ASM_ARITH_TAC)))))
(* 0 <= - nF1 *)
>- (match_mp_tac REAL_LE_TRANS \\
qexists_tac `nR1 * inv nR2 + - nF1 * (inv nR2 + err2 * inv ((e2hi + err2) * (e2hi + err2)))` \\
conj_tac
>- (fs[REAL_LE_LADD] \\
match_mp_tac REAL_LE_LMUL_IMP \\
- conj_tac \\ REAL_ASM_ARITH_TAC)
+ conj_tac \\ OLD_REAL_ASM_ARITH_TAC)
>- (qabbrev_tac `err_inv = (err2 * ((e2hi + err2) * (e2hi + err2))â»Â¹)` \\
qspecl_then [`inv nR2 + err_inv`, `0`] DISJ_CASES_TAC REAL_LTE_TOTAL
>- (match_mp_tac REAL_LE_TRANS \\
@@ -1435,11 +1435,11 @@ Proof
>- (fs [REAL_LE_ADD] \\
once_rewrite_tac [REAL_MUL_COMM] \\
match_mp_tac REAL_MUL_LE_COMPAT_NEG_L\\
- conj_tac \\ TRY REAL_ASM_ARITH_TAC \\
+ conj_tac \\ TRY OLD_REAL_ASM_ARITH_TAC \\
fs [REAL_LE_NEG])
>- (`nR1 * inv nR2 + - (nR1 + err1) * (inv nR2 + err_inv) =
- nR1 * err_inv + - (inv nR2) * err1 - err1 * err_inv`
- by REAL_ASM_ARITH_TAC \\
+ by OLD_REAL_ASM_ARITH_TAC \\
simp[REAL_NEG_MUL2] \\
qspecl_then [`inv ((e2hi + err2) * (e2hi + err2))`,`err2`]
(fn thm => once_rewrite_tac [thm]) REAL_MUL_COMM \\
@@ -1448,31 +1448,31 @@ Proof
match_mp_tac REAL_LE_ADD2 \\
conj_tac
>- (match_mp_tac REAL_LE_ADD2 \\
- conj_tac \\ TRY REAL_ASM_ARITH_TAC \\
+ conj_tac \\ TRY OLD_REAL_ASM_ARITH_TAC \\
match_mp_tac REAL_LE_RMUL_IMP \\
- conj_tac \\ REAL_ASM_ARITH_TAC)
+ conj_tac \\ OLD_REAL_ASM_ARITH_TAC)
>- (simp [REAL_NEG_LMUL] \\
match_mp_tac REAL_LE_RMUL_IMP \\
- conj_tac \\ REAL_ASM_ARITH_TAC)))
+ conj_tac \\ OLD_REAL_ASM_ARITH_TAC)))
>- (match_mp_tac REAL_LE_TRANS \\
qexists_tac `nR1 * inv nR2 + - (nR1 + - err1) * (inv nR2 + err_inv)` \\
conj_tac
>- (fs [REAL_LE_ADD] \\
match_mp_tac REAL_LE_RMUL_IMP \\
- conj_tac \\ REAL_ASM_ARITH_TAC)
+ conj_tac \\ OLD_REAL_ASM_ARITH_TAC)
>- (`nR1 * inv nR2 + - (nR1 + - err1) * (inv nR2 + err_inv) =
- nR1 * err_inv + inv nR2 * err1 + err1 * err_inv`
- by REAL_ASM_ARITH_TAC \\
+ by OLD_REAL_ASM_ARITH_TAC \\
simp[REAL_NEG_MUL2] \\
qspecl_then [`inv ((e2hi + err2) * (e2hi + err2))`,`err2`]
(fn thm => once_rewrite_tac [thm]) REAL_MUL_COMM \\
qunabbrev_tac `err_inv` \\
match_mp_tac REAL_LE_ADD2 \\
- conj_tac \\ TRY REAL_ASM_ARITH_TAC \\
+ conj_tac \\ TRY OLD_REAL_ASM_ARITH_TAC \\
match_mp_tac REAL_LE_ADD2 \\
- conj_tac \\ TRY REAL_ASM_ARITH_TAC \\
+ conj_tac \\ TRY OLD_REAL_ASM_ARITH_TAC \\
match_mp_tac REAL_LE_RMUL_IMP \\
- conj_tac \\ REAL_ASM_ARITH_TAC)))))
+ conj_tac \\ OLD_REAL_ASM_ARITH_TAC)))))
(* Case 2: Absolute value negative *)
>- (qspecl_then [`nF1`, `0`] DISJ_CASES_TAC REAL_LTE_TOTAL
(* nF1 < 0 *)
@@ -1481,7 +1481,7 @@ Proof
conj_tac
>- (fs[REAL_LE_LADD] \\
match_mp_tac REAL_MUL_LE_COMPAT_NEG_L \\
- conj_tac \\ REAL_ASM_ARITH_TAC)
+ conj_tac \\ OLD_REAL_ASM_ARITH_TAC)
>- (qabbrev_tac `err_inv = (err2 * ((e2hi + err2) * (e2hi + err2))â»Â¹)` \\
qspecl_then [`inv nR2 - err_inv`, `0`] DISJ_CASES_TAC REAL_LTE_TOTAL
>- (match_mp_tac REAL_LE_TRANS \\
@@ -1490,30 +1490,30 @@ Proof
>- (fs [REAL_LE_ADD] \\
once_rewrite_tac [REAL_MUL_COMM] \\
match_mp_tac REAL_MUL_LE_COMPAT_NEG_L\\
- conj_tac \\ TRY REAL_ASM_ARITH_TAC \\
+ conj_tac \\ TRY OLD_REAL_ASM_ARITH_TAC \\
fs [REAL_LE_NEG])
>- (`- nR1 * inv nR2 + (nR1 - err1) * (inv nR2 - err_inv) =
- nR1 * err_inv + - (inv nR2) * err1 + err1 * err_inv`
- by REAL_ASM_ARITH_TAC \\
+ by OLD_REAL_ASM_ARITH_TAC \\
simp[REAL_NEG_MUL2] \\
qspecl_then [`inv ((e2hi + err2) * (e2hi + err2))`,`err2`]
(fn thm => once_rewrite_tac [thm]) REAL_MUL_COMM \\
qunabbrev_tac `err_inv` \\
match_mp_tac REAL_LE_ADD2 \\
- conj_tac \\ TRY REAL_ASM_ARITH_TAC \\
+ conj_tac \\ TRY OLD_REAL_ASM_ARITH_TAC \\
match_mp_tac REAL_LE_ADD2 \\
- conj_tac \\ TRY REAL_ASM_ARITH_TAC \\
+ conj_tac \\ TRY OLD_REAL_ASM_ARITH_TAC \\
match_mp_tac REAL_LE_RMUL_IMP \\
- conj_tac \\ REAL_ASM_ARITH_TAC))
+ conj_tac \\ OLD_REAL_ASM_ARITH_TAC))
>- (match_mp_tac REAL_LE_TRANS \\
qexists_tac `- nR1 * inv nR2 + (nR1 + err1) * (inv nR2 - err_inv)` \\
conj_tac
>- (fs [REAL_LE_ADD] \\
match_mp_tac REAL_LE_RMUL_IMP \\
- conj_tac \\ REAL_ASM_ARITH_TAC)
+ conj_tac \\ OLD_REAL_ASM_ARITH_TAC)
>- (`- nR1 * inv nR2 + (nR1 + err1) * (inv nR2 - err_inv) =
- nR1 * err_inv + inv nR2 * err1 - err1 * err_inv`
- by REAL_ASM_ARITH_TAC \\
+ by OLD_REAL_ASM_ARITH_TAC \\
simp[REAL_NEG_MUL2] \\
qspecl_then [`inv ((e2hi + err2) * (e2hi + err2))`,`err2`]
(fn thm => once_rewrite_tac [thm]) REAL_MUL_COMM \\
@@ -1522,19 +1522,19 @@ Proof
match_mp_tac REAL_LE_ADD2 \\
conj_tac
>- (match_mp_tac REAL_LE_ADD2 \\
- conj_tac \\ TRY REAL_ASM_ARITH_TAC \\
+ conj_tac \\ TRY OLD_REAL_ASM_ARITH_TAC \\
match_mp_tac REAL_LE_RMUL_IMP \\
- conj_tac \\ REAL_ASM_ARITH_TAC)
+ conj_tac \\ OLD_REAL_ASM_ARITH_TAC)
>- (fs [GSYM REAL_NEG_ADD, REAL_NEG_MUL2, REAL_NEG_LMUL] \\
match_mp_tac REAL_LE_RMUL_IMP \\
- conj_tac \\ REAL_ASM_ARITH_TAC)))))
+ conj_tac \\ OLD_REAL_ASM_ARITH_TAC)))))
(* 0 <= - nF1 *)
>- (match_mp_tac REAL_LE_TRANS \\
qexists_tac `- nR1 * inv nR2 + nF1 * (inv nR2 + err2 * inv ((e2hi + err2) * (e2hi + err2)))` \\
conj_tac
>- (fs[REAL_LE_LADD] \\
match_mp_tac REAL_LE_LMUL_IMP \\
- conj_tac \\ REAL_ASM_ARITH_TAC)
+ conj_tac \\ OLD_REAL_ASM_ARITH_TAC)
>- (qabbrev_tac `err_inv = (err2 * ((e2hi + err2) * (e2hi + err2))â»Â¹)` \\
qspecl_then [`inv nR2 + err_inv`, `0`] DISJ_CASES_TAC REAL_LTE_TOTAL
>- (match_mp_tac REAL_LE_TRANS \\
@@ -1543,11 +1543,11 @@ Proof
>- (fs [REAL_LE_ADD] \\
once_rewrite_tac [REAL_MUL_COMM] \\
match_mp_tac REAL_MUL_LE_COMPAT_NEG_L\\
- conj_tac \\ TRY REAL_ASM_ARITH_TAC \\
+ conj_tac \\ TRY OLD_REAL_ASM_ARITH_TAC \\
fs [REAL_LE_NEG])
>- (`- nR1 * inv nR2 + (nR1 - err1) * (inv nR2 + err_inv) =
nR1 * err_inv + - (inv nR2) * err1 - err1 * err_inv`
- by REAL_ASM_ARITH_TAC \\
+ by OLD_REAL_ASM_ARITH_TAC \\
simp[REAL_NEG_MUL2] \\
qspecl_then [`inv ((e2hi + err2) * (e2hi + err2))`,`err2`]
(fn thm => once_rewrite_tac [thm]) REAL_MUL_COMM \\
@@ -1556,42 +1556,42 @@ Proof
match_mp_tac REAL_LE_ADD2 \\
conj_tac
>- (match_mp_tac REAL_LE_ADD2 \\
- conj_tac \\ TRY REAL_ASM_ARITH_TAC \\
+ conj_tac \\ TRY OLD_REAL_ASM_ARITH_TAC \\
match_mp_tac REAL_LE_RMUL_IMP \\
- conj_tac \\ REAL_ASM_ARITH_TAC)
+ conj_tac \\ OLD_REAL_ASM_ARITH_TAC)
>- (fs [REAL_NEG_LMUL] \\
match_mp_tac REAL_LE_RMUL_IMP \\
- conj_tac \\ REAL_ASM_ARITH_TAC)))
+ conj_tac \\ OLD_REAL_ASM_ARITH_TAC)))
>- (match_mp_tac REAL_LE_TRANS \\
qexists_tac `- nR1 * inv nR2 + (nR1 + err1) * (inv nR2 + err_inv)` \\
conj_tac
>- (fs [REAL_LE_ADD] \\
match_mp_tac REAL_LE_RMUL_IMP \\
- conj_tac \\ REAL_ASM_ARITH_TAC)
+ conj_tac \\ OLD_REAL_ASM_ARITH_TAC)
>- (`- nR1 * inv nR2 + (nR1 + err1) * (inv nR2 + err_inv) =
nR1 * err_inv + inv nR2 * err1 + err1 * err_inv`
- by REAL_ASM_ARITH_TAC \\
+ by OLD_REAL_ASM_ARITH_TAC \\
simp[REAL_NEG_MUL2] \\
qspecl_then [`inv ((e2hi + err2) * (e2hi + err2))`,`err2`]
(fn thm => once_rewrite_tac [thm]) REAL_MUL_COMM \\
qunabbrev_tac `err_inv` \\
match_mp_tac REAL_LE_ADD2 \\
- conj_tac \\ TRY REAL_ASM_ARITH_TAC \\
+ conj_tac \\ TRY OLD_REAL_ASM_ARITH_TAC \\
match_mp_tac REAL_LE_ADD2 \\
- conj_tac \\ TRY REAL_ASM_ARITH_TAC \\
+ conj_tac \\ TRY OLD_REAL_ASM_ARITH_TAC \\
match_mp_tac REAL_LE_RMUL_IMP \\
- conj_tac \\ REAL_ASM_ARITH_TAC)))))))
+ conj_tac \\ OLD_REAL_ASM_ARITH_TAC)))))))
>- (CCONTR_TAC \\
rule_assum_tac (fn thm => REWRITE_RULE[IVlo_def, IVhi_def, widenInterval_def] thm) \\
- `e2lo <= e2hi` by REAL_ASM_ARITH_TAC \\
- `e2lo <= e2hi + err2` by REAL_ASM_ARITH_TAC \\
- `e2lo <= e2hi + err2` by REAL_ASM_ARITH_TAC \\
- REAL_ASM_ARITH_TAC)
+ `e2lo <= e2hi` by OLD_REAL_ASM_ARITH_TAC \\
+ `e2lo <= e2hi + err2` by OLD_REAL_ASM_ARITH_TAC \\
+ `e2lo <= e2hi + err2` by OLD_REAL_ASM_ARITH_TAC \\
+ OLD_REAL_ASM_ARITH_TAC)
>- (CCONTR_TAC \\
rule_assum_tac (fn thm => REWRITE_RULE[IVlo_def, IVhi_def, widenInterval_def] thm) \\
- `e2lo <= e2hi` by REAL_ASM_ARITH_TAC \\
- `e2lo - err2 <= e2hi` by REAL_ASM_ARITH_TAC \\
- REAL_ASM_ARITH_TAC)
+ `e2lo <= e2hi` by OLD_REAL_ASM_ARITH_TAC \\
+ `e2lo - err2 <= e2hi` by OLD_REAL_ASM_ARITH_TAC \\
+ OLD_REAL_ASM_ARITH_TAC)
(* The range of the divisor lies in the range from 0 to infinity *)
>- (rule_assum_tac
(fn thm =>
@@ -1602,22 +1602,22 @@ Proof
fs[contained_def, IVlo_def, IVhi_def]) \\
fs [widenInterval_def, IVlo_def, IVhi_def, invertInterval_def] \\
`minAbsFun (e2lo - err2, e2hi + err2) = (e2lo - err2)`
- by (match_mp_tac minAbs_positive_iv_is_lo \\ REAL_ASM_ARITH_TAC) \\
+ by (match_mp_tac minAbs_positive_iv_is_lo \\ OLD_REAL_ASM_ARITH_TAC) \\
simp[] \\
qpat_x_assum `minAbsFun _ = _ ` kall_tac \\
- `nF1 <= err1 + nR1` by REAL_ASM_ARITH_TAC \\
- `nR1 - err1 <= nF1` by REAL_ASM_ARITH_TAC \\
+ `nF1 <= err1 + nR1` by OLD_REAL_ASM_ARITH_TAC \\
+ `nR1 - err1 <= nF1` by OLD_REAL_ASM_ARITH_TAC \\
`(nR2 - nF2 > 0 /\ nR2 - nF2 <= err2) \/ (nR2 - nF2 <= 0 /\ - (nR2 - nF2) <= err2)`
- by REAL_ASM_ARITH_TAC
+ by OLD_REAL_ASM_ARITH_TAC
(* Positive case for abs (nR2 - nF2) <= err2 *)
- >- (`nF2 < nR2` by REAL_ASM_ARITH_TAC \\
- `inv nR2 < inv nF2` by (match_mp_tac REAL_LT_INV \\ TRY REAL_ASM_ARITH_TAC) \\
- `inv nR2 - inv nF2 < 0` by REAL_ASM_ARITH_TAC \\
- `nR2â»Â¹ − nF2â»Â¹ ≤ err2 * ((e2lo - err2) * (e2lo - err2))â»Â¹` by REAL_ASM_ARITH_TAC \\
- `inv nF2 <= inv nR2 + err2 * inv ((e2lo - err2) * (e2lo - err2))` by REAL_ASM_ARITH_TAC \\
- `inv nR2 - err2 * inv ((e2lo - err2) * (e2lo - err2)) <= inv nF2` by REAL_ASM_ARITH_TAC \\
+ >- (`nF2 < nR2` by OLD_REAL_ASM_ARITH_TAC \\
+ `inv nR2 < inv nF2` by (match_mp_tac REAL_LT_INV \\ TRY OLD_REAL_ASM_ARITH_TAC) \\
+ `inv nR2 - inv nF2 < 0` by OLD_REAL_ASM_ARITH_TAC \\
+ `nR2â»Â¹ − nF2â»Â¹ ≤ err2 * ((e2lo - err2) * (e2lo - err2))â»Â¹` by OLD_REAL_ASM_ARITH_TAC \\
+ `inv nF2 <= inv nR2 + err2 * inv ((e2lo - err2) * (e2lo - err2))` by OLD_REAL_ASM_ARITH_TAC \\
+ `inv nR2 - err2 * inv ((e2lo - err2) * (e2lo - err2)) <= inv nF2` by OLD_REAL_ASM_ARITH_TAC \\
(* Next do a case distinction for the absolute value *)
- `! (x:real). ((abs x = x) /\ 0 <= x) \/ ((abs x = - x) /\ x < 0)` by REAL_ASM_ARITH_TAC \\
+ `! (x:real). ((abs x = x) /\ 0 <= x) \/ ((abs x = - x) /\ x < 0)` by OLD_REAL_ASM_ARITH_TAC \\
qpat_x_assum `!x. A /\ B \/ C`
(fn thm => qspec_then `(nR1:real / nR2:real) - (nF1:real / nF2:real)` DISJ_CASES_TAC thm)
\\ fs[realTheory.abs]
@@ -1630,7 +1630,7 @@ Proof
conj_tac
>- (fs[REAL_LE_LADD] \\
match_mp_tac REAL_MUL_LE_COMPAT_NEG_L \\
- conj_tac \\ REAL_ASM_ARITH_TAC)
+ conj_tac \\ OLD_REAL_ASM_ARITH_TAC)
>- (qabbrev_tac `err_inv = (err2 * ((e2lo - err2) * (e2lo - err2))â»Â¹)` \\
qspecl_then [`inv nR2 - err_inv`, `0`] DISJ_CASES_TAC REAL_LTE_TOTAL
>- (match_mp_tac REAL_LE_TRANS \\
@@ -1639,31 +1639,31 @@ Proof
>- (fs [REAL_LE_ADD] \\
once_rewrite_tac [REAL_MUL_COMM] \\
match_mp_tac REAL_MUL_LE_COMPAT_NEG_L\\
- conj_tac \\ TRY REAL_ASM_ARITH_TAC \\
+ conj_tac \\ TRY OLD_REAL_ASM_ARITH_TAC \\
fs [REAL_LE_NEG])
>- (`nR1 * inv nR2 + - (nR1 + err1) * (inv nR2 - err_inv) =
nR1 * err_inv + - (inv nR2) * err1 + err1 * err_inv`
- by REAL_ASM_ARITH_TAC \\
+ by OLD_REAL_ASM_ARITH_TAC \\
simp[REAL_NEG_MUL2] \\
qspecl_then [`inv ((e2lo + - err2) * (e2lo + - err2))`,`err2`]
(fn thm => once_rewrite_tac [thm]) REAL_MUL_COMM \\
qunabbrev_tac `err_inv` \\
match_mp_tac REAL_LE_ADD2 \\
- conj_tac \\ TRY REAL_ASM_ARITH_TAC \\
+ conj_tac \\ TRY OLD_REAL_ASM_ARITH_TAC \\
match_mp_tac REAL_LE_ADD2 \\
- conj_tac \\ TRY REAL_ASM_ARITH_TAC \\
+ conj_tac \\ TRY OLD_REAL_ASM_ARITH_TAC \\
simp[GSYM real_sub] \\
match_mp_tac REAL_LE_RMUL_IMP \\
- conj_tac \\ REAL_ASM_ARITH_TAC))
+ conj_tac \\ OLD_REAL_ASM_ARITH_TAC))
>- (match_mp_tac REAL_LE_TRANS \\
qexists_tac `nR1 * inv nR2 + - (nR1 + - err1) * (inv nR2 - err_inv)` \\
conj_tac
>- (fs [REAL_LE_ADD] \\
match_mp_tac REAL_LE_RMUL_IMP \\
- conj_tac \\ REAL_ASM_ARITH_TAC)
+ conj_tac \\ OLD_REAL_ASM_ARITH_TAC)
>- (`nR1 * inv nR2 + - (nR1 + - err1) * (inv nR2 - err_inv) =
nR1 * err_inv + inv nR2 * err1 - err1 * err_inv`
- by REAL_ASM_ARITH_TAC \\
+ by OLD_REAL_ASM_ARITH_TAC \\
simp[REAL_NEG_MUL2] \\
qspecl_then [`inv ((e2lo + -err2) * (e2lo + -err2))`,`err2`]
(fn thm => once_rewrite_tac [thm]) REAL_MUL_COMM \\
@@ -1672,19 +1672,19 @@ Proof
match_mp_tac REAL_LE_ADD2 \\
conj_tac
>- (match_mp_tac REAL_LE_ADD2 \\
- conj_tac \\ TRY REAL_ASM_ARITH_TAC \\
+ conj_tac \\ TRY OLD_REAL_ASM_ARITH_TAC \\
match_mp_tac REAL_LE_RMUL_IMP \\
- conj_tac \\ REAL_ASM_ARITH_TAC)
+ conj_tac \\ OLD_REAL_ASM_ARITH_TAC)
>- (simp [REAL_NEG_LMUL] \\
match_mp_tac REAL_LE_RMUL_IMP \\
- conj_tac \\ REAL_ASM_ARITH_TAC)))))
+ conj_tac \\ OLD_REAL_ASM_ARITH_TAC)))))
(* 0 <= - nF1 *)
>- (match_mp_tac REAL_LE_TRANS \\
qexists_tac `nR1 * inv nR2 + - nF1 * (inv nR2 + err2 * inv ((e2lo - err2) * (e2lo - err2)))` \\
conj_tac
>- (fs[REAL_LE_LADD] \\
match_mp_tac REAL_LE_LMUL_IMP \\
- conj_tac \\ REAL_ASM_ARITH_TAC)
+ conj_tac \\ OLD_REAL_ASM_ARITH_TAC)
>- (qabbrev_tac `err_inv = (err2 * ((e2lo - err2) * (e2lo - err2))â»Â¹)` \\
qspecl_then [`inv nR2 + err_inv`, `0`] DISJ_CASES_TAC REAL_LTE_TOTAL
>- (match_mp_tac REAL_LE_TRANS \\
@@ -1693,11 +1693,11 @@ Proof
>- (fs [REAL_LE_ADD] \\
once_rewrite_tac [REAL_MUL_COMM] \\
match_mp_tac REAL_MUL_LE_COMPAT_NEG_L\\
- conj_tac \\ TRY REAL_ASM_ARITH_TAC \\
+ conj_tac \\ TRY OLD_REAL_ASM_ARITH_TAC \\
fs [REAL_LE_NEG])
>- (`nR1 * inv nR2 + - (nR1 + err1) * (inv nR2 + err_inv) =
- nR1 * err_inv + - (inv nR2) * err1 - err1 * err_inv`
- by REAL_ASM_ARITH_TAC \\
+ by OLD_REAL_ASM_ARITH_TAC \\
simp[REAL_NEG_MUL2] \\
qspecl_then [`inv ((e2lo + -err2) * (e2lo + -err2))`,`err2`]
(fn thm => once_rewrite_tac [thm]) REAL_MUL_COMM \\
@@ -1706,32 +1706,32 @@ Proof
match_mp_tac REAL_LE_ADD2 \\
conj_tac
>- (match_mp_tac REAL_LE_ADD2 \\
- conj_tac \\ TRY REAL_ASM_ARITH_TAC \\
+ conj_tac \\ TRY OLD_REAL_ASM_ARITH_TAC \\
match_mp_tac REAL_LE_RMUL_IMP \\
- conj_tac \\ REAL_ASM_ARITH_TAC)
+ conj_tac \\ OLD_REAL_ASM_ARITH_TAC)
>- (simp [REAL_NEG_LMUL] \\
match_mp_tac REAL_LE_RMUL_IMP \\
- conj_tac \\ REAL_ASM_ARITH_TAC)))
+ conj_tac \\ OLD_REAL_ASM_ARITH_TAC)))
>- (match_mp_tac REAL_LE_TRANS \\
qexists_tac `nR1 * inv nR2 + - (nR1 + - err1) * (inv nR2 + err_inv)` \\
conj_tac
>- (fs [REAL_LE_ADD] \\
match_mp_tac REAL_LE_RMUL_IMP \\
- conj_tac \\ REAL_ASM_ARITH_TAC)
+ conj_tac \\ OLD_REAL_ASM_ARITH_TAC)
>- (`nR1 * inv nR2 + - (nR1 + - err1) * (inv nR2 + err_inv) =
- nR1 * err_inv + inv nR2 * err1 + err1 * err_inv`
- by REAL_ASM_ARITH_TAC \\
+ by OLD_REAL_ASM_ARITH_TAC \\
simp[REAL_NEG_MUL2] \\
qspecl_then [`inv ((e2lo + -err2) * (e2lo + -err2))`,`err2`]
(fn thm => once_rewrite_tac [thm]) REAL_MUL_COMM \\
qunabbrev_tac `err_inv` \\
match_mp_tac REAL_LE_ADD2 \\
- conj_tac \\ TRY REAL_ASM_ARITH_TAC \\
+ conj_tac \\ TRY OLD_REAL_ASM_ARITH_TAC \\
match_mp_tac REAL_LE_ADD2 \\
- conj_tac \\ TRY REAL_ASM_ARITH_TAC \\
+ conj_tac \\ TRY OLD_REAL_ASM_ARITH_TAC \\
simp [GSYM real_sub] \\
match_mp_tac REAL_LE_RMUL_IMP \\
- conj_tac \\ REAL_ASM_ARITH_TAC)))))
+ conj_tac \\ OLD_REAL_ASM_ARITH_TAC)))))
(* Case 2: Absolute value negative *)
>- (fs[real_sub, real_div, REAL_NEG_LMUL, REAL_NEG_ADD] \\
qspecl_then [`nF1`, `0`] DISJ_CASES_TAC REAL_LTE_TOTAL
@@ -1741,7 +1741,7 @@ Proof
conj_tac
>- (fs[REAL_LE_LADD] \\
match_mp_tac REAL_MUL_LE_COMPAT_NEG_L \\
- conj_tac \\ REAL_ASM_ARITH_TAC)
+ conj_tac \\ OLD_REAL_ASM_ARITH_TAC)
>- (qabbrev_tac `err_inv = (err2 * ((e2lo - err2) * (e2lo - err2))â»Â¹)` \\
qspecl_then [`inv nR2 - err_inv`, `0`] DISJ_CASES_TAC REAL_LTE_TOTAL
>- (match_mp_tac REAL_LE_TRANS \\
@@ -1750,31 +1750,31 @@ Proof
>- (fs [REAL_LE_ADD] \\
once_rewrite_tac [REAL_MUL_COMM] \\
match_mp_tac REAL_MUL_LE_COMPAT_NEG_L\\
- conj_tac \\ TRY REAL_ASM_ARITH_TAC \\
+ conj_tac \\ TRY OLD_REAL_ASM_ARITH_TAC \\
fs [REAL_LE_NEG])
>- (`- nR1 * inv nR2 + (nR1 - err1) * (inv nR2 - err_inv) =
- nR1 * err_inv + - (inv nR2) * err1 + err1 * err_inv`
- by REAL_ASM_ARITH_TAC \\
+ by OLD_REAL_ASM_ARITH_TAC \\
simp[REAL_NEG_MUL2] \\
qspecl_then [`inv ((e2lo + -err2) * (e2lo + -err2))`,`err2`]
(fn thm => once_rewrite_tac [thm]) REAL_MUL_COMM \\
qunabbrev_tac `err_inv` \\
match_mp_tac REAL_LE_ADD2 \\
- conj_tac \\ TRY REAL_ASM_ARITH_TAC \\
+ conj_tac \\ TRY OLD_REAL_ASM_ARITH_TAC \\
match_mp_tac REAL_LE_ADD2 \\
- conj_tac \\ TRY REAL_ASM_ARITH_TAC \\
+ conj_tac \\ TRY OLD_REAL_ASM_ARITH_TAC \\
simp [GSYM real_sub] \\
match_mp_tac REAL_LE_RMUL_IMP \\
- conj_tac \\ REAL_ASM_ARITH_TAC))
+ conj_tac \\ OLD_REAL_ASM_ARITH_TAC))
>- (match_mp_tac REAL_LE_TRANS \\
qexists_tac `- nR1 * inv nR2 + (nR1 + err1) * (inv nR2 - err_inv)` \\
conj_tac
>- (fs [REAL_LE_ADD] \\
match_mp_tac REAL_LE_RMUL_IMP \\
- conj_tac \\ REAL_ASM_ARITH_TAC)
+ conj_tac \\ OLD_REAL_ASM_ARITH_TAC)
>- (`- nR1 * inv nR2 + (nR1 + err1) * (inv nR2 - err_inv) =
- nR1 * err_inv + inv nR2 * err1 - err1 * err_inv`
- by REAL_ASM_ARITH_TAC \\
+ by OLD_REAL_ASM_ARITH_TAC \\
simp[REAL_NEG_MUL2] \\
qspecl_then [`inv ((e2lo + -err2) * (e2lo + -err2))`,`err2`]
(fn thm => once_rewrite_tac [thm]) REAL_MUL_COMM \\
@@ -1783,20 +1783,20 @@ Proof
match_mp_tac REAL_LE_ADD2 \\
conj_tac
>- (match_mp_tac REAL_LE_ADD2 \\
- conj_tac \\ TRY REAL_ASM_ARITH_TAC \\
+ conj_tac \\ TRY OLD_REAL_ASM_ARITH_TAC \\
fs [GSYM REAL_NEG_ADD, REAL_NEG_MUL2] \\
match_mp_tac REAL_LE_RMUL_IMP \\
- conj_tac \\ REAL_ASM_ARITH_TAC)
+ conj_tac \\ OLD_REAL_ASM_ARITH_TAC)
>- (fs [GSYM REAL_NEG_ADD, REAL_NEG_MUL2, REAL_NEG_LMUL] \\
match_mp_tac REAL_LE_RMUL_IMP \\
- conj_tac \\ REAL_ASM_ARITH_TAC)))))
+ conj_tac \\ OLD_REAL_ASM_ARITH_TAC)))))
(* 0 <= - nF1 *)
>- (match_mp_tac REAL_LE_TRANS \\
qexists_tac `- nR1 * inv nR2 + nF1 * (inv nR2 + err2 * inv ((e2lo - err2) * (e2lo - err2)))` \\
conj_tac
>- (fs[REAL_LE_LADD] \\
match_mp_tac REAL_LE_LMUL_IMP \\
- conj_tac \\ REAL_ASM_ARITH_TAC)
+ conj_tac \\ OLD_REAL_ASM_ARITH_TAC)
>- (qabbrev_tac `err_inv = (err2 * ((e2lo - err2) * (e2lo - err2))â»Â¹)` \\
qspecl_then [`inv nR2 + err_inv`, `0`] DISJ_CASES_TAC REAL_LTE_TOTAL
>- (match_mp_tac REAL_LE_TRANS \\
@@ -1805,11 +1805,11 @@ Proof
>- (fs [REAL_LE_ADD] \\
once_rewrite_tac [REAL_MUL_COMM] \\
match_mp_tac REAL_MUL_LE_COMPAT_NEG_L\\
- conj_tac \\ TRY REAL_ASM_ARITH_TAC \\
+ conj_tac \\ TRY OLD_REAL_ASM_ARITH_TAC \\
fs [REAL_LE_NEG])
>- (`- nR1 * inv nR2 + (nR1 - err1) * (inv nR2 + err_inv) =
nR1 * err_inv + - (inv nR2) * err1 - err1 * err_inv`
- by REAL_ASM_ARITH_TAC \\
+ by OLD_REAL_ASM_ARITH_TAC \\
simp[REAL_NEG_MUL2] \\
qspecl_then [`inv ((e2lo + -err2) * (e2lo + -err2))`,`err2`]
(fn thm => once_rewrite_tac [thm]) REAL_MUL_COMM \\
@@ -1818,42 +1818,42 @@ Proof
match_mp_tac REAL_LE_ADD2 \\
conj_tac
>- (match_mp_tac REAL_LE_ADD2 \\
- conj_tac \\ TRY REAL_ASM_ARITH_TAC \\
+ conj_tac \\ TRY OLD_REAL_ASM_ARITH_TAC \\
match_mp_tac REAL_LE_RMUL_IMP \\
- conj_tac \\ REAL_ASM_ARITH_TAC)
+ conj_tac \\ OLD_REAL_ASM_ARITH_TAC)
>- (fs [REAL_NEG_LMUL] \\
match_mp_tac REAL_LE_RMUL_IMP \\
- conj_tac \\ REAL_ASM_ARITH_TAC)))
+ conj_tac \\ OLD_REAL_ASM_ARITH_TAC)))
>- (match_mp_tac REAL_LE_TRANS \\
qexists_tac `- nR1 * inv nR2 + (nR1 + err1) * (inv nR2 + err_inv)` \\
conj_tac
>- (fs [REAL_LE_ADD] \\
match_mp_tac REAL_LE_RMUL_IMP \\
- conj_tac \\ REAL_ASM_ARITH_TAC)
+ conj_tac \\ OLD_REAL_ASM_ARITH_TAC)
>- (`- nR1 * inv nR2 + (nR1 + err1) * (inv nR2 + err_inv) =
nR1 * err_inv + inv nR2 * err1 + err1 * err_inv`
- by REAL_ASM_ARITH_TAC \\
+ by OLD_REAL_ASM_ARITH_TAC \\
simp[REAL_NEG_MUL2] \\
qspecl_then [`inv ((e2lo + -err2) * (e2lo + -err2))`,`err2`]
(fn thm => once_rewrite_tac [thm]) REAL_MUL_COMM \\
qunabbrev_tac `err_inv` \\
match_mp_tac REAL_LE_ADD2 \\
- conj_tac \\ TRY REAL_ASM_ARITH_TAC \\
+ conj_tac \\ TRY OLD_REAL_ASM_ARITH_TAC \\
match_mp_tac REAL_LE_ADD2 \\
- conj_tac \\ TRY REAL_ASM_ARITH_TAC \\
+ conj_tac \\ TRY OLD_REAL_ASM_ARITH_TAC \\
simp [GSYM real_sub] \\
match_mp_tac REAL_LE_RMUL_IMP \\
- conj_tac \\ REAL_ASM_ARITH_TAC))))))
+ conj_tac \\ OLD_REAL_ASM_ARITH_TAC))))))
(* Negative case for abs (nR2 - nF2) <= err2 *)
>- (fs [GSYM REAL_NEG_ADD, REAL_NEG_MUL2, REAL_NEG_LMUL] \\
- `nR2 <= nF2` by REAL_ASM_ARITH_TAC \\
- `inv nF2 <= inv nR2` by (match_mp_tac REAL_INV_LE_ANTIMONO_IMPR \\ REAL_ASM_ARITH_TAC) \\
- `0 <= inv nR2 - inv nF2` by REAL_ASM_ARITH_TAC \\
- `(nR2â»Â¹ − nF2â»Â¹) ≤ err2 * ((e2lo - err2) * (e2lo - err2))â»Â¹` by REAL_ASM_ARITH_TAC \\
- `inv nF2 <= inv nR2 + err2 * inv ((e2lo - err2) * (e2lo - err2))` by REAL_ASM_ARITH_TAC \\
- `inv nR2 - err2 * inv ((e2lo - err2) * (e2lo - err2)) <= inv nF2` by REAL_ASM_ARITH_TAC \\
+ `nR2 <= nF2` by OLD_REAL_ASM_ARITH_TAC \\
+ `inv nF2 <= inv nR2` by (match_mp_tac REAL_INV_LE_ANTIMONO_IMPR \\ OLD_REAL_ASM_ARITH_TAC) \\
+ `0 <= inv nR2 - inv nF2` by OLD_REAL_ASM_ARITH_TAC \\
+ `(nR2â»Â¹ − nF2â»Â¹) ≤ err2 * ((e2lo - err2) * (e2lo - err2))â»Â¹` by OLD_REAL_ASM_ARITH_TAC \\
+ `inv nF2 <= inv nR2 + err2 * inv ((e2lo - err2) * (e2lo - err2))` by OLD_REAL_ASM_ARITH_TAC \\
+ `inv nR2 - err2 * inv ((e2lo - err2) * (e2lo - err2)) <= inv nF2` by OLD_REAL_ASM_ARITH_TAC \\
(* Next do a case distinction for the absolute value *)
- `! (x:real). ((abs x = x) /\ 0 <= x) \/ ((abs x = - x) /\ x < 0)` by REAL_ASM_ARITH_TAC \\
+ `! (x:real). ((abs x = x) /\ 0 <= x) \/ ((abs x = - x) /\ x < 0)` by OLD_REAL_ASM_ARITH_TAC \\
qpat_x_assum `!x. A /\ B \/ C`
(fn thm => qspec_then `(nR1:real / nR2:real) - (nF1:real / nF2:real)` DISJ_CASES_TAC thm) \\
fs[real_sub, real_div, REAL_NEG_LMUL, REAL_NEG_ADD, realTheory.abs]
@@ -1865,7 +1865,7 @@ Proof
conj_tac
>- (fs[REAL_LE_LADD] \\
match_mp_tac REAL_MUL_LE_COMPAT_NEG_L \\
- conj_tac \\ REAL_ASM_ARITH_TAC)
+ conj_tac \\ OLD_REAL_ASM_ARITH_TAC)
>- (qabbrev_tac `err_inv = (err2 * ((e2lo - err2) * (e2lo - err2))â»Â¹)` \\
qspecl_then [`inv nR2 - err_inv`, `0`] DISJ_CASES_TAC REAL_LTE_TOTAL
>- (match_mp_tac REAL_LE_TRANS \\
@@ -1874,31 +1874,31 @@ Proof
>- (fs [REAL_LE_ADD] \\
once_rewrite_tac [REAL_MUL_COMM] \\
match_mp_tac REAL_MUL_LE_COMPAT_NEG_L\\
- conj_tac \\ TRY REAL_ASM_ARITH_TAC \\
+ conj_tac \\ TRY OLD_REAL_ASM_ARITH_TAC \\
fs [REAL_LE_NEG])
>- (`nR1 * inv nR2 + - (nR1 + err1) * (inv nR2 - err_inv) =
nR1 * err_inv + - (inv nR2) * err1 + err1 * err_inv`
- by REAL_ASM_ARITH_TAC \\
+ by OLD_REAL_ASM_ARITH_TAC \\
simp[REAL_NEG_MUL2] \\
qspecl_then [`inv ((e2lo + -err2) * (e2lo + -err2))`,`err2`]
(fn thm => once_rewrite_tac [thm]) REAL_MUL_COMM \\
qunabbrev_tac `err_inv` \\
match_mp_tac REAL_LE_ADD2 \\
- conj_tac \\ TRY REAL_ASM_ARITH_TAC \\
+ conj_tac \\ TRY OLD_REAL_ASM_ARITH_TAC \\
match_mp_tac REAL_LE_ADD2 \\
- conj_tac \\ TRY REAL_ASM_ARITH_TAC \\
+ conj_tac \\ TRY OLD_REAL_ASM_ARITH_TAC \\
simp [GSYM real_sub] \\
match_mp_tac REAL_LE_RMUL_IMP \\
- conj_tac \\ REAL_ASM_ARITH_TAC))
+ conj_tac \\ OLD_REAL_ASM_ARITH_TAC))
>- (match_mp_tac REAL_LE_TRANS \\
qexists_tac `nR1 * inv nR2 + - (nR1 + - err1) * (inv nR2 - err_inv)` \\
conj_tac
>- (fs [REAL_LE_ADD] \\
match_mp_tac REAL_LE_RMUL_IMP \\
- conj_tac \\ REAL_ASM_ARITH_TAC)
+ conj_tac \\ OLD_REAL_ASM_ARITH_TAC)
>- (`nR1 * inv nR2 + - (nR1 + - err1) * (inv nR2 - err_inv) =
nR1 * err_inv + inv nR2 * err1 - err1 * err_inv`
- by REAL_ASM_ARITH_TAC \\
+ by OLD_REAL_ASM_ARITH_TAC \\
simp[REAL_NEG_MUL2] \\
qspecl_then [`inv ((e2lo + -err2) * (e2lo + -err2))`,`err2`]
(fn thm => once_rewrite_tac [thm]) REAL_MUL_COMM \\
@@ -1907,19 +1907,19 @@ Proof
match_mp_tac REAL_LE_ADD2 \\
conj_tac
>- (match_mp_tac REAL_LE_ADD2 \\
- conj_tac \\ TRY REAL_ASM_ARITH_TAC \\
+ conj_tac \\ TRY OLD_REAL_ASM_ARITH_TAC \\
match_mp_tac REAL_LE_RMUL_IMP \\
- conj_tac \\ REAL_ASM_ARITH_TAC)
+ conj_tac \\ OLD_REAL_ASM_ARITH_TAC)
>- (simp [REAL_NEG_LMUL] \\
match_mp_tac REAL_LE_RMUL_IMP \\
- conj_tac \\ REAL_ASM_ARITH_TAC)))))
+ conj_tac \\ OLD_REAL_ASM_ARITH_TAC)))))
(* 0 <= - nF1 *)
>- (match_mp_tac REAL_LE_TRANS \\
qexists_tac `nR1 * inv nR2 + - nF1 * (inv nR2 + err2 * inv ((e2lo - err2) * (e2lo - err2)))` \\
conj_tac
>- (fs[REAL_LE_LADD] \\
match_mp_tac REAL_LE_LMUL_IMP \\
- conj_tac \\ REAL_ASM_ARITH_TAC)
+ conj_tac \\ OLD_REAL_ASM_ARITH_TAC)
>- (qabbrev_tac `err_inv = (err2 * ((e2lo - err2) * (e2lo - err2))â»Â¹)` \\
qspecl_then [`inv nR2 + err_inv`, `0`] DISJ_CASES_TAC REAL_LTE_TOTAL
>- (match_mp_tac REAL_LE_TRANS \\
@@ -1928,11 +1928,11 @@ Proof
>- (fs [REAL_LE_ADD] \\
once_rewrite_tac [REAL_MUL_COMM] \\
match_mp_tac REAL_MUL_LE_COMPAT_NEG_L\\
- conj_tac \\ TRY REAL_ASM_ARITH_TAC \\
+ conj_tac \\ TRY OLD_REAL_ASM_ARITH_TAC \\
fs [REAL_LE_NEG])
>- (`nR1 * inv nR2 + - (nR1 + err1) * (inv nR2 + err_inv) =
- nR1 * err_inv + - (inv nR2) * err1 - err1 * err_inv`
- by REAL_ASM_ARITH_TAC \\
+ by OLD_REAL_ASM_ARITH_TAC \\
simp[REAL_NEG_MUL2] \\
qspecl_then [`inv ((e2lo + -err2) * (e2lo + -err2))`,`err2`]
(fn thm => once_rewrite_tac [thm]) REAL_MUL_COMM \\
@@ -1941,32 +1941,32 @@ Proof
match_mp_tac REAL_LE_ADD2 \\
conj_tac
>- (match_mp_tac REAL_LE_ADD2 \\
- conj_tac \\ TRY REAL_ASM_ARITH_TAC \\
+ conj_tac \\ TRY OLD_REAL_ASM_ARITH_TAC \\
match_mp_tac REAL_LE_RMUL_IMP \\
- conj_tac \\ REAL_ASM_ARITH_TAC)
+ conj_tac \\ OLD_REAL_ASM_ARITH_TAC)
>- (simp [REAL_NEG_LMUL] \\
match_mp_tac REAL_LE_RMUL_IMP \\
- conj_tac \\ REAL_ASM_ARITH_TAC)))
+ conj_tac \\ OLD_REAL_ASM_ARITH_TAC)))
>- (match_mp_tac REAL_LE_TRANS \\
qexists_tac `nR1 * inv nR2 + - (nR1 + - err1) * (inv nR2 + err_inv)` \\
conj_tac
>- (fs [REAL_LE_ADD] \\
match_mp_tac REAL_LE_RMUL_IMP \\
- conj_tac \\ REAL_ASM_ARITH_TAC)
+ conj_tac \\ OLD_REAL_ASM_ARITH_TAC)
>- (`nR1 * inv nR2 + - (nR1 + - err1) * (inv nR2 + err_inv) =
- nR1 * err_inv + inv nR2 * err1 + err1 * err_inv`
- by REAL_ASM_ARITH_TAC \\
+ by OLD_REAL_ASM_ARITH_TAC \\
simp[REAL_NEG_MUL2] \\
qspecl_then [`inv ((e2lo + -err2) * (e2lo + -err2))`,`err2`]
(fn thm => once_rewrite_tac [thm]) REAL_MUL_COMM \\
qunabbrev_tac `err_inv` \\
match_mp_tac REAL_LE_ADD2 \\
- conj_tac \\ TRY REAL_ASM_ARITH_TAC \\
+ conj_tac \\ TRY OLD_REAL_ASM_ARITH_TAC \\
match_mp_tac REAL_LE_ADD2 \\
- conj_tac \\ TRY REAL_ASM_ARITH_TAC \\
+ conj_tac \\ TRY OLD_REAL_ASM_ARITH_TAC \\
simp [GSYM real_sub] \\
match_mp_tac REAL_LE_RMUL_IMP \\
- conj_tac \\ REAL_ASM_ARITH_TAC)))))
+ conj_tac \\ OLD_REAL_ASM_ARITH_TAC)))))
(* Case 2: Absolute value negative *)
>- (qspecl_then [`nF1`, `0`] DISJ_CASES_TAC REAL_LTE_TOTAL
(* nF1 < 0 *)
@@ -1975,7 +1975,7 @@ Proof
conj_tac
>- (fs[REAL_LE_LADD] \\
match_mp_tac REAL_MUL_LE_COMPAT_NEG_L \\
- conj_tac \\ REAL_ASM_ARITH_TAC)
+ conj_tac \\ OLD_REAL_ASM_ARITH_TAC)
>- (qabbrev_tac `err_inv = (err2 * ((e2lo - err2) * (e2lo - err2))â»Â¹)` \\
qspecl_then [`inv nR2 - err_inv`, `0`] DISJ_CASES_TAC REAL_LTE_TOTAL
>- (match_mp_tac REAL_LE_TRANS \\
@@ -1984,31 +1984,31 @@ Proof
>- (fs [REAL_LE_ADD] \\
once_rewrite_tac [REAL_MUL_COMM] \\
match_mp_tac REAL_MUL_LE_COMPAT_NEG_L\\
- conj_tac \\ TRY REAL_ASM_ARITH_TAC \\
+ conj_tac \\ TRY OLD_REAL_ASM_ARITH_TAC \\
fs [REAL_LE_NEG])
>- (`- nR1 * inv nR2 + (nR1 - err1) * (inv nR2 - err_inv) =
- nR1 * err_inv + - (inv nR2) * err1 + err1 * err_inv`
- by REAL_ASM_ARITH_TAC \\
+ by OLD_REAL_ASM_ARITH_TAC \\
simp[REAL_NEG_MUL2] \\
qspecl_then [`inv ((e2lo + -err2) * (e2lo + -err2))`,`err2`]
(fn thm => once_rewrite_tac [thm]) REAL_MUL_COMM \\
qunabbrev_tac `err_inv` \\
match_mp_tac REAL_LE_ADD2 \\
- conj_tac \\ TRY REAL_ASM_ARITH_TAC \\
+ conj_tac \\ TRY OLD_REAL_ASM_ARITH_TAC \\
match_mp_tac REAL_LE_ADD2 \\
- conj_tac \\ TRY REAL_ASM_ARITH_TAC \\
+ conj_tac \\ TRY OLD_REAL_ASM_ARITH_TAC \\
simp [GSYM real_sub] \\
match_mp_tac REAL_LE_RMUL_IMP \\
- conj_tac \\ REAL_ASM_ARITH_TAC))
+ conj_tac \\ OLD_REAL_ASM_ARITH_TAC))
>- (match_mp_tac REAL_LE_TRANS \\
qexists_tac `- nR1 * inv nR2 + (nR1 + err1) * (inv nR2 - err_inv)` \\
conj_tac
>- (fs [REAL_LE_ADD] \\
match_mp_tac REAL_LE_RMUL_IMP \\
- conj_tac \\ REAL_ASM_ARITH_TAC)
+ conj_tac \\ OLD_REAL_ASM_ARITH_TAC)
>- (`- nR1 * inv nR2 + (nR1 + err1) * (inv nR2 - err_inv) =
- nR1 * err_inv + inv nR2 * err1 - err1 * err_inv`
- by REAL_ASM_ARITH_TAC \\
+ by OLD_REAL_ASM_ARITH_TAC \\
simp[REAL_NEG_MUL2] \\
qspecl_then [`inv ((e2lo + -err2) * (e2lo + -err2))`,`err2`]
(fn thm => once_rewrite_tac [thm]) REAL_MUL_COMM \\
@@ -2017,19 +2017,19 @@ Proof
match_mp_tac REAL_LE_ADD2 \\
conj_tac
>- (match_mp_tac REAL_LE_ADD2 \\
- conj_tac \\ TRY REAL_ASM_ARITH_TAC \\
+ conj_tac \\ TRY OLD_REAL_ASM_ARITH_TAC \\
match_mp_tac REAL_LE_RMUL_IMP \\
- conj_tac \\ REAL_ASM_ARITH_TAC)
+ conj_tac \\ OLD_REAL_ASM_ARITH_TAC)
>- (fs [GSYM REAL_NEG_ADD, REAL_NEG_MUL2, REAL_NEG_LMUL] \\
match_mp_tac REAL_LE_RMUL_IMP \\
- conj_tac \\ REAL_ASM_ARITH_TAC)))))
+ conj_tac \\ OLD_REAL_ASM_ARITH_TAC)))))
(* 0 <= - nF1 *)
>- (match_mp_tac REAL_LE_TRANS \\
qexists_tac `- nR1 * inv nR2 + nF1 * (inv nR2 + err2 * inv ((e2lo - err2) * (e2lo - err2)))` \\
conj_tac
>- (fs[REAL_LE_LADD] \\
match_mp_tac REAL_LE_LMUL_IMP \\
- conj_tac \\ REAL_ASM_ARITH_TAC)
+ conj_tac \\ OLD_REAL_ASM_ARITH_TAC)
>- (qabbrev_tac `err_inv = (err2 * ((e2lo - err2) * (e2lo - err2))â»Â¹)` \\
qspecl_then [`inv nR2 + err_inv`, `0`] DISJ_CASES_TAC REAL_LTE_TOTAL
>- (match_mp_tac REAL_LE_TRANS \\
@@ -2038,11 +2038,11 @@ Proof
>- (fs [REAL_LE_ADD] \\
once_rewrite_tac [REAL_MUL_COMM] \\
match_mp_tac REAL_MUL_LE_COMPAT_NEG_L\\
- conj_tac \\ TRY REAL_ASM_ARITH_TAC \\
+ conj_tac \\ TRY OLD_REAL_ASM_ARITH_TAC \\
fs [REAL_LE_NEG])
>- (`- nR1 * inv nR2 + (nR1 - err1) * (inv nR2 + err_inv) =
nR1 * err_inv + - (inv nR2) * err1 - err1 * err_inv`
- by REAL_ASM_ARITH_TAC \\
+ by OLD_REAL_ASM_ARITH_TAC \\
simp[REAL_NEG_MUL2] \\
qspecl_then [`inv ((e2lo + -err2) * (e2lo + -err2))`,`err2`]
(fn thm => once_rewrite_tac [thm]) REAL_MUL_COMM \\
@@ -2051,32 +2051,32 @@ Proof
match_mp_tac REAL_LE_ADD2 \\
conj_tac
>- (match_mp_tac REAL_LE_ADD2 \\
- conj_tac \\ TRY REAL_ASM_ARITH_TAC \\
+ conj_tac \\ TRY OLD_REAL_ASM_ARITH_TAC \\
match_mp_tac REAL_LE_RMUL_IMP \\
- conj_tac \\ REAL_ASM_ARITH_TAC)
+ conj_tac \\ OLD_REAL_ASM_ARITH_TAC)
>- (fs [REAL_NEG_LMUL] \\
match_mp_tac REAL_LE_RMUL_IMP \\
- conj_tac \\ REAL_ASM_ARITH_TAC)))
+ conj_tac \\ OLD_REAL_ASM_ARITH_TAC)))
>- (match_mp_tac REAL_LE_TRANS \\
qexists_tac `- nR1 * inv nR2 + (nR1 + err1) * (inv nR2 + err_inv)` \\
conj_tac
>- (fs [REAL_LE_ADD] \\
match_mp_tac REAL_LE_RMUL_IMP \\
- conj_tac \\ REAL_ASM_ARITH_TAC)
+ conj_tac \\ OLD_REAL_ASM_ARITH_TAC)
>- (`- nR1 * inv nR2 + (nR1 + err1) * (inv nR2 + err_inv) =
nR1 * err_inv + inv nR2 * err1 + err1 * err_inv`
- by REAL_ASM_ARITH_TAC \\
+ by OLD_REAL_ASM_ARITH_TAC \\
simp[REAL_NEG_MUL2] \\
qspecl_then [`inv ((e2lo + -err2) * (e2lo + -err2))`,`err2`]
(fn thm => once_rewrite_tac [thm]) REAL_MUL_COMM \\
qunabbrev_tac `err_inv` \\
match_mp_tac REAL_LE_ADD2 \\
- conj_tac \\ TRY REAL_ASM_ARITH_TAC \\
+ conj_tac \\ TRY OLD_REAL_ASM_ARITH_TAC \\
match_mp_tac REAL_LE_ADD2 \\
- conj_tac \\ TRY REAL_ASM_ARITH_TAC \\
+ conj_tac \\ TRY OLD_REAL_ASM_ARITH_TAC \\
simp [GSYM real_sub] \\
match_mp_tac REAL_LE_RMUL_IMP \\
- conj_tac \\ REAL_ASM_ARITH_TAC)))))))
+ conj_tac \\ OLD_REAL_ASM_ARITH_TAC)))))))
QED
Theorem validErrorboundCorrectDiv:
diff --git a/hol4/FPRangeValidatorScript.sml b/hol4/FPRangeValidatorScript.sml
index 87b1530c..bd81e50b 100644
--- a/hol4/FPRangeValidatorScript.sml
+++ b/hol4/FPRangeValidatorScript.sml
@@ -18,7 +18,7 @@ open preambleFloVer;
val _ = new_theory "FPRangeValidator";
-Overload abs[local] = “real$absâ€
+Overload abs[local] = “realax$absâ€
Definition FPRangeValidator_def:
FPRangeValidator (e:real expr) A typeMap dVars =
diff --git a/hol4/IEEE_connectionScript.sml b/hol4/IEEE_connectionScript.sml
index 0128b2db..8152f1d3 100644
--- a/hol4/IEEE_connectionScript.sml
+++ b/hol4/IEEE_connectionScript.sml
@@ -13,7 +13,7 @@ open preambleFloVer;
val _ = new_theory "IEEE_connection";
-Overload abs[local] = “real$absâ€
+Overload abs[local] = “realax$absâ€
val _ = diminish_srw_ss ["RMULCANON_ss","RMULRELNORM_ss"]
diff --git a/hol4/IEEE_reverseScript.sml b/hol4/IEEE_reverseScript.sml
index 48b2edba..168a7d42 100644
--- a/hol4/IEEE_reverseScript.sml
+++ b/hol4/IEEE_reverseScript.sml
@@ -14,7 +14,7 @@ open preambleFloVer;
val _ = new_theory "IEEE_reverse";
-Overload abs[local] = “real$absâ€
+Overload abs[local] = “realax$absâ€
Definition toFlExp_def:
toFlExp ((Var v):real expr) = Var v ∧
@@ -56,49 +56,40 @@ Proof
\\ TOP_CASE_TAC \\ gs[]
QED
-(** Some eval test
-EVAL “float_to_real ((real_to_float roundTiesToEven (float_to_real <|Sign := 1w; Exponent := 0w:word11; Significand := 0w:52 word |>)):(52,11) floatâ€
-|> CONV_RULE (RHS_CONV $ RAND_CONV $ binary_ieeeLib.float_round_CONV)
-**)
-
Theorem eval_expr_gives_IEEE_reverse:
!(e:real expr) E1 E2 Gamma vR A fVars dVars.
validTypes e Gamma /\
- approxEnv E1 (toRExpMap Gamma) A fVars dVars E2 /\
+ approxEnv E1 (toRExpMap Gamma) A fVars dVars (toREnv E2) /\
validRanges e A E1 (toRTMap (toRExpMap Gamma)) /\
validErrorbound e Gamma A dVars /\
FPRangeValidator e A Gamma dVars /\
- eval_expr E2 (toRExpMap Gamma) e vR M64 /\
+ eval_expr (toREnv E2) (toRExpMap Gamma) e vR M64 /\
domain (usedVars e) DIFF domain dVars ⊆ domain fVars ∧
is64BitEval e /\
is64BitEnv Gamma /\
noDowncast e /\
- (∀ x v. E2 x = SOME v ⇒ float_to_real ((real_to_float dmode v):(52,11) float) = v) ∧
(∀v.
v ∈ domain dVars ⇒
∃vF m.
- (E2 v = SOME vF ∧ FloverMapTree_find (Var v) Gamma = SOME m ∧
+ ((toREnv E2) v = SOME vF ∧ FloverMapTree_find (Var v) Gamma = SOME m ∧
validFloatValue vF m)) ==>
?v.
- eval_expr_float (toFlExp e) (toFlEnv E2) = SOME v /\
- eval_expr E2 (toRExpMap Gamma) e (fp64_to_real v) M64
+ eval_expr_float (toFlExp e) E2 = SOME v /\
+ eval_expr (toREnv E2) (toRExpMap Gamma) e (fp64_to_real v) M64
Proof
Induct_on `e` \\ rw[toFlExp_def]
\\ inversion `eval_expr _ _ _ _ _` eval_expr_cases
\\ once_rewrite_tac [eval_expr_float_def]
\\ fs[noDowncast_def]
- >- (
- simp [toFlEnv_def, eval_expr_cases, fp64_to_real_def,
- real_to_fp64_def, fp64_to_float_float_to_fp64]
- \\ gs[usedVars_def]
- \\ first_x_assum $ qspecl_then [‘n’, ‘vR’] assume_tac
- \\ gs[])
+ >- gs [toREnv_def, eval_expr_cases, fp64_to_real_def,
+ real_to_fp64_def, fp64_to_float_float_to_fp64,
+ CaseEq"option"]
>- (
simp[eval_expr_cases, fp64_to_real_def, real_to_fp64_def,
fp64_to_float_float_to_fp64, real_to_float_def, dmode_def,
float_round_def, float_is_zero_to_real]
\\ gs[perturb_def]
- \\ ‘eval_expr E2 (toRExpMap Gamma) (Const M64 v) v M64’
+ \\ ‘eval_expr (toREnv E2) (toRExpMap Gamma) (Const M64 v) v M64’
by (gs[eval_expr_cases]
\\ qexists_tac ‘0’ \\ gs[perturb_def, mTypeToR_pos])
\\ ‘validFloatValue v M64’
@@ -145,15 +136,26 @@ Proof
\\ irule REAL_LT_TRANS
\\ first_assum $ irule_at Any
\\ fs[minExponentPos_def])
- \\ rpt conj_tac >- gs[]
+ \\ rpt conj_tac
>~ [‘1 < INT_MAX (:11)’] >- gs[]
- \\ irule REAL_LET_TRANS \\ qexists_tac ‘2 / 2 pow (INT_MAX (:11) - 1)’
- \\ reverse conj_tac
- >- (pop_assum $ mp_tac \\ REAL_ARITH_TAC)
- \\ gs[threshold_def]
- \\ rewrite_tac [REAL_INV_1OVER] \\ EVAL_TAC)
- \\ rpt strip_tac \\ qexists_tac ‘e’ \\ gs[]
- \\ TOP_CASE_TAC \\ gs[minExponentPos_def])
+ >- (
+ irule REAL_LTE_TRANS
+ \\ first_assum $ irule_at Any
+ \\ simp[threshold_def]
+ \\ rewrite_tac[REAL_INV_1OVER]
+ \\ EVAL_TAC)
+ \\ irule REAL_LTE_TRANS \\ qexists_tac ‘2 / 2 pow (INT_MAX (:11) - 1)’
+ \\ reverse conj_tac >- gs[]
+ \\ pop_assum $ mp_tac \\ REAL_ARITH_TAC)
+ \\ rpt strip_tac \\ TOP_CASE_TAC \\ gs[minExponentPos_def]
+ >- (
+ qexists_tac ‘-v’ \\ gs[]
+ \\ irule REAL_LE_TRANS \\ first_x_assum $ irule_at Any
+ \\ gs[])
+ \\ qexists_tac ‘float_to_real ((round roundTiesToEven v):(52,11) float) - v’ \\ gs[]
+ \\ conj_tac >- REAL_ARITH_TAC
+ \\ irule REAL_LE_TRANS \\ first_x_assum $ irule_at Any
+ \\ gs[])
>- (gvs[denormal_def] \\ qexists_tac ‘0’ \\ gs[mTypeToR_pos])
)
>- (
@@ -358,9 +360,9 @@ Proof
\\ rename1 `eval_expr E1 _ (toREval e2) nR2 REAL`
\\ rename1 `eval_expr E1 _ (toREval e1) nR1 REAL`
(* Obtain evaluation for E2 *)
- \\ ‘!vF2 m2. eval_expr E2 (toRExpMap Gamma) e2 vF2 m2 ==>
+ \\ ‘!vF2 m2. eval_expr (toREnv E2) (toRExpMap Gamma) e2 vF2 m2 ==>
abs (nR2 - vF2) <= err2’
- by (qspecl_then [`e2`, `E1`, `E2`, `A`,`nR2`,
+ by (qspecl_then [`e2`, `E1`, `toREnv E2`, `A`,`nR2`,
`err2`, `FST iv2`, `SND iv2`, `fVars`,
`dVars`,`Gamma`] destruct validErrorbound_sound
\\ rpt conj_tac \\ fs[]
@@ -865,9 +867,9 @@ Proof
\\ rw_asm_star `FloverMapTree_find (Fma _ _ _) Gamma = _`)
\\ rw_thm_asm `domain (usedVars _) DIFF _ SUBSET _` usedVars_def
\\ fs[domain_union, DIFF_DEF, SUBSET_DEF])
- \\ rename1 ‘eval_expr_float (toFlExp e1) (toFlEnv E2) = SOME vF1’
- \\ rename1 ‘eval_expr_float (toFlExp e2) (toFlEnv E2) = SOME vF2’
- \\ rename1 ‘eval_expr_float (toFlExp e3) (toFlEnv E2) = SOME vF3’
+ \\ rename1 ‘eval_expr_float (toFlExp e1) E2 = SOME vF1’
+ \\ rename1 ‘eval_expr_float (toFlExp e2) E2 = SOME vF2’
+ \\ rename1 ‘eval_expr_float (toFlExp e3) E2 = SOME vF3’
\\ `validFloatValue
(evalFma (float_to_real (fp64_to_float vF1))
(float_to_real (fp64_to_float vF2))
@@ -1255,14 +1257,12 @@ Theorem IEEE_connection_expr:
fVars_P_sound fVars E1 P /\
(domain (usedVars e)) SUBSET (domain fVars) /\
CertificateChecker e A P defVars = SOME Gamma /\
- (∀ x v. E2 x = SOME v ⇒
- float_to_real ((real_to_float dmode v):(52,11) float) = v) ∧
- approxEnv E1 (toRExpMap Gamma) A fVars LN E2 ⇒
+ approxEnv E1 (toRExpMap Gamma) A fVars LN (toREnv E2) ⇒
?iv err vR vF. (* m, currently = M64 *)
FloverMapTree_find e A = SOME (iv, err) /\
eval_expr E1 (toRTMap (toRExpMap Gamma)) (toREval e) vR REAL /\
- eval_expr_float (toFlExp e) (toFlEnv E2) = SOME vF /\
- eval_expr E2 (toRExpMap Gamma) e (fp64_to_real vF) M64 /\
+ eval_expr_float (toFlExp e) E2 = SOME vF /\
+ eval_expr (toREnv E2) (toRExpMap Gamma) e (fp64_to_real vF) M64 /\
abs (vR - (fp64_to_real vF)) <= err
Proof
simp [CertificateChecker_def]
diff --git a/hol4/Infra/FloverCompLib.sml b/hol4/Infra/FloverCompLib.sml
index 0e0dd4f8..09fd7850 100644
--- a/hol4/Infra/FloverCompLib.sml
+++ b/hol4/Infra/FloverCompLib.sml
@@ -1,3 +1,6 @@
+(**
+ Small changes to computeLib for FloVer
+**)
structure FloverCompLib =
struct
open computeLib;
diff --git a/hol4/Infra/Holmakefile b/hol4/Infra/Holmakefile
index 38c73a13..e64c77e7 100644
--- a/hol4/Infra/Holmakefile
+++ b/hol4/Infra/Holmakefile
@@ -1,3 +1 @@
-INCLUDES = $(HOLDIR)/examples/machine-code/hoare-triple $(HOLDIR)/examples/fun-op-sem/lprefix_lub
-
OPTIONS = QUIT_ON_FAILURE
diff --git a/hol4/Infra/MachineTypeScript.sml b/hol4/Infra/MachineTypeScript.sml
index b42d184a..39e8a999 100644
--- a/hol4/Infra/MachineTypeScript.sml
+++ b/hol4/Infra/MachineTypeScript.sml
@@ -4,27 +4,19 @@
@author: Raphael Monat
@maintainer: Heiko Becker
**)
-open realTheory realLib integerTheory;
+open realTheory realLib;
open RealSimpsTheory;
open preambleFloVer;
val _ = new_theory "MachineType";
-Overload abs[local] = “real$absâ€
+Overload abs[local] = “realax$absâ€
val _ = monadsyntax.enable_monadsyntax();
val _ = List.app monadsyntax.enable_monad ["option"];
Datatype:
- mType = REAL
- (* Floating point formats *)
- | M16 | M32 | M64
- (* Fixed point formats:
- * first num is word length,
- * second is fractional bits,
- * bool is for sign of fractional bits, inverse of the exponent sign with T <=> positive
- *)
- | F num num bool
+ mType = REAL | M16 | M32 | M64 | F num num bool (* first num is word length, second is fractional bits, bool is for sign of fractional bits *)
End
Definition isFixedPoint_def :
@@ -189,8 +181,9 @@ QED
REAL is real-valued evaluation, hence the most precise.
All floating-point types are compared by
mTypeToQ m1 <= mTypeToQ m2
- All fixed-point types are compared by comparing the positions of the
- least and most significant bits. It is equivalent to a subset check.
+ All fixed-point types are compared by comparing only the word size
+ We consider a 32 bit fixed-point number to be more precise than a 16 bit
+ fixed-point number, no matter what the fractional bits may be.
For the moment, fixed-point and floating-point formats are incomparable.
**)
Definition isMorePrecise_def:
@@ -198,8 +191,13 @@ Definition isMorePrecise_def:
case m1, m2 of
| REAL, _ => T
| F w1 f1 s1, F w2 f2 s2 =>
- let exp1: int = if s1 then &f1 else -&f1 ; exp2 = if s2 then &f2 else -&f2 in
- &w2 + exp2 <= &w1 + exp1 /\ exp1 <= exp2
+ if s1 then
+ if s2 then
+ (w2 ≤ w1 ∧ f2 ≤ f1)
+ else
+ (w2 ≤ w1)
+ else if s2 then F
+ else (w2 ≤ w1 ∧ f2 ≤ f1)
| F w f s, _ => F
| _, F w f s=> F
| M16, M16 => T
@@ -217,8 +215,13 @@ End
Definition morePrecise_def:
(morePrecise REAL _ = T) /\
(morePrecise (F w1 f1 s1) (F w2 f2 s2) =
- let exp1: int = if s1 then &f1 else -&f1 ; exp2 = if s2 then &f2 else -&f2 in
- &w2 + exp2 <= &w1 + exp1 /\ exp1 <= exp2) /\
+ (if s1 then
+ if s2 then
+ (w2 ≤ w1 ∧ f2 ≤ f1)
+ else
+ (w2 ≤ w1)
+ else if s2 then F
+ else (w2 ≤ w1 ∧ f2 ≤ f1))) ∧
(morePrecise (F w f s) _ = F) /\
(morePrecise _ (F w f s) = F) /\
(morePrecise M16 M16 = T) /\
@@ -238,7 +241,7 @@ Proof
rpt strip_tac
\\ Cases_on `m1` \\ Cases_on `m2` \\ Cases_on `m3`
\\ fs[morePrecise_def]
- \\ ntac 2 $ dxrule_all INT_LE_TRANS \\ simp[]
+ \\ every_case_tac \\ gs[]
QED
Theorem isMorePrecise_morePrecise:
@@ -302,7 +305,7 @@ End
Definition isJoin_def:
isJoin m1 m2 mj =
if (isFixedPoint m1 /\ isFixedPoint m2)
- then morePrecise mj m1 /\ morePrecise mj m2
+ then morePrecise m1 mj /\ morePrecise m2 mj
else
(case join_fl m1 m2 of
|NONE => F
@@ -312,7 +315,7 @@ End
Definition isJoin3_def:
isJoin3 m1 m2 m3 mj =
if (isFixedPoint m1 /\ isFixedPoint m2 /\ isFixedPoint m3)
- then morePrecise mj m1 /\ morePrecise mj m2 /\ morePrecise mj m3
+ then morePrecise m1 mj /\ morePrecise m2 mj /\ morePrecise m3 mj
else
(case join_fl3 m1 m2 m3 of
|NONE => F
diff --git a/hol4/Infra/RealSimpsScript.sml b/hol4/Infra/RealSimpsScript.sml
index 7efdcad7..4889a634 100644
--- a/hol4/Infra/RealSimpsScript.sml
+++ b/hol4/Infra/RealSimpsScript.sml
@@ -7,8 +7,8 @@ open preambleFloVer;
val _ = new_theory "RealSimps";
-Overload abs[local] = “real$absâ€
-Overload max[local] = “real$maxâ€
+Overload abs[local] = “realax$absâ€
+Overload max[local] = “realax$maxâ€
Theorem abs_leq_zero[simp]:
!v. abs v <= 0 <=> v = 0
diff --git a/hol4/Infra/ResultsLib.sml b/hol4/Infra/ResultsLib.sml
index 43ea08a2..6318af10 100644
--- a/hol4/Infra/ResultsLib.sml
+++ b/hol4/Infra/ResultsLib.sml
@@ -1,3 +1,6 @@
+(**
+ A monad for results used by FlOVer
+**)
structure ResultsLib =
struct
diff --git a/hol4/IntervalArithScript.sml b/hol4/IntervalArithScript.sml
index 35e5e726..b3aeeb09 100644
--- a/hol4/IntervalArithScript.sml
+++ b/hol4/IntervalArithScript.sml
@@ -10,9 +10,9 @@ val _ = temp_delsimps ["NORMEQ_CONV"]
val _ = new_theory "IntervalArith";
-Overload abs[local] = “real$absâ€
-Overload max[local] = “real$maxâ€
-Overload min[local] = “real$minâ€
+Overload abs[local] = “realax$absâ€
+Overload max[local] = “realax$maxâ€
+Overload min[local] = “realax$minâ€
(**
Define validity of an interval, requiring that the lower bound is less than or equal to the upper bound.
diff --git a/hol4/IntervalValidationScript.sml b/hol4/IntervalValidationScript.sml
index 59b0e6f7..ce147989 100644
--- a/hol4/IntervalValidationScript.sml
+++ b/hol4/IntervalValidationScript.sml
@@ -19,9 +19,9 @@ val _ = temp_delsimps ["RMUL_LEQNORM"]
val _ = Parse.hide "delta"; (* so that it can be used as a variable *)
-Overload abs[local] = “real$absâ€
-Overload max[local] = “real$maxâ€
-Overload min[local] = “real$minâ€
+Overload abs[local] = “realax$absâ€
+Overload max[local] = “realax$maxâ€
+Overload min[local] = “realax$minâ€
(** Define a global iteration count for square roots **)
Definition ITERCOUNT_def:
diff --git a/hol4/TypeValidatorScript.sml b/hol4/TypeValidatorScript.sml
index 1ecb6fe9..d067079b 100644
--- a/hol4/TypeValidatorScript.sml
+++ b/hol4/TypeValidatorScript.sml
@@ -138,7 +138,7 @@ Definition getValidMap_def:
case mOldO of
| NONE => Fail "Undefined fixed-point type"
| SOME mj =>
- if (morePrecise mj t1 /\ morePrecise mj t2)
+ if (morePrecise t1 mj /\ morePrecise t2 mj)
then addMono e mj akk2_map
else Fail "Incorrect fixed-point type"
else
@@ -172,7 +172,7 @@ Definition getValidMap_def:
case mOldO of
| NONE => Fail "Undefined fixed-point type"
| SOME mj =>
- if (morePrecise mj t1 /\ morePrecise mj t2 /\ morePrecise mj t3)
+ if (morePrecise t1 mj /\ morePrecise t2 mj /\ morePrecise t3 mj)
then addMono e mj akk3_map
else Fail "Incorrect fixed-point type"
else if (t1 = REAL ∨ t2 = REAL ∨ t3 = REAL)
@@ -261,7 +261,7 @@ Proof
\\ Cases_on `getValidMap Gamma e1 akk` \\ fs[result_bind_def]
\\ Cases_on `getValidMap Gamma e2 a` \\ fs[option_case_eq]
\\ Cases_on `isFixedPoint t1` \\ Cases_on `isFixedPoint t2` \\ fs[option_case_eq]
- >- (Cases_on `morePrecise mj t1` \\ Cases_on `morePrecise mj t2`
+ >- (Cases_on `morePrecise t1 mj` \\ Cases_on `morePrecise t2 mj`
\\ fs[addMono_def, option_case_eq]
\\ rveq \\ res_tac
\\ by_monotonicity)
@@ -284,9 +284,9 @@ Proof
\\ Cases_on `isFixedPoint t2`
\\ Cases_on `isFixedPoint t3`
\\ fs[option_case_eq]
- >- (Cases_on `morePrecise mj t1`
- \\ Cases_on `morePrecise mj t2`
- \\ Cases_on `morePrecise mj t3`
+ >- (Cases_on `morePrecise t1 mj`
+ \\ Cases_on `morePrecise t2 mj`
+ \\ Cases_on `morePrecise t3 mj`
\\ fs[addMono_def, option_case_eq]
\\ rveq \\ res_tac
\\ by_monotonicity)
@@ -484,7 +484,7 @@ Proof
by (rpt strip_tac \\ first_x_assum irule \\ fs[]
\\ qexistsl_tac [`Gamma`, `a`] \\ fs[])
\\ Cases_on ‘isFixedPoint x ∧ isFixedPoint x'’
- >- (fs[option_case_eq] \\ Cases_on `morePrecise mj x` \\ Cases_on `morePrecise mj x'`
+ >- (fs[option_case_eq] \\ Cases_on `morePrecise x mj` \\ Cases_on `morePrecise x' mj`
\\ fs[addMono_def, option_case_eq]
\\ rveq \\ fs[FloverMapTree_mem_def, map_find_add]
\\ reverse (Cases_on `e'' = Binop b e1 e2`) \\ fs[]
@@ -613,8 +613,8 @@ Proof
\\ qexistsl_tac [`Gamma`, `map2`] \\ fs[])
\\ Cases_on `isFixedPoint x /\ isFixedPoint x' /\ isFixedPoint x''`
>- (fs[option_case_eq]
- \\ Cases_on `morePrecise mj x` \\ Cases_on `morePrecise mj x'`
- \\ Cases_on `morePrecise mj x''`
+ \\ Cases_on `morePrecise x mj` \\ Cases_on `morePrecise x' mj`
+ \\ Cases_on `morePrecise x'' mj`
\\ fs[addMono_def, option_case_eq]
\\ rveq \\ fs[FloverMapTree_mem_def, map_find_add]
\\ rename1 `if eNew = Fma e1 e2 e3 then SOME mj else _`
diff --git a/hol4/semantics/ExpressionSemanticsScript.sml b/hol4/semantics/ExpressionSemanticsScript.sml
index 04695592..8f43dbab 100644
--- a/hol4/semantics/ExpressionSemanticsScript.sml
+++ b/hol4/semantics/ExpressionSemanticsScript.sml
@@ -8,7 +8,7 @@ open preambleFloVer;
val _ = new_theory "ExpressionSemantics";
-Overload abs = “real$absâ€
+Overload abs = “realax$absâ€
(**
Define a perturbation function to ease writing of basic definitions
@@ -355,4 +355,25 @@ Proof
\\ metis_tac[]
QED
+Theorem swap_gamma_eval_weak:
+ ∀ e E vR m Gamma1 Gamma2.
+ (∀ e m. Gamma1 e = SOME m ⇒ Gamma2 e = SOME m) ∧
+ eval_expr E Gamma1 e vR m ⇒
+ eval_expr E Gamma2 e vR m
+Proof
+ Induct_on `e` \\ fs[eval_expr_cases] \\ rpt strip_tac
+ >- metis_tac[]
+ >- metis_tac[]
+ >- metis_tac[]
+ >- (
+ res_tac
+ >> rpt $ first_x_assum $ irule_at Any
+ >> gs[])
+ >- (
+ res_tac
+ >> rpt $ first_x_assum $ irule_at Any
+ >> gs[])
+ >- metis_tac[]
+QED
+
val _ = export_theory();
diff --git a/hol4/semantics/ExpressionsScript.sml b/hol4/semantics/ExpressionsScript.sml
index c4144093..bee53e85 100644
--- a/hol4/semantics/ExpressionsScript.sml
+++ b/hol4/semantics/ExpressionsScript.sml
@@ -1,13 +1,13 @@
(**
Formalization of the base expression language for the flover framework
**)
-open realTheory realLib sptreeTheory
+open realTheory realLib RealArith sptreeTheory intrealTheory;
open AbbrevsTheory MachineTypeTheory
open preambleFloVer;
val _ = new_theory "Expressions";
-Overload abs = “real$absâ€
+Overload abs = “realax$absâ€
(**
expressions will use binary operators.
@@ -98,4 +98,14 @@ Definition usedVars_def:
| _ => LN
End
+Definition ratExp2realExp_def:
+ ratExp2realExp ((Const m (c,d)):(int#int) expr):real expr =
+ Const m ((real_of_int c) / (real_of_int d)) ∧
+ ratExp2realExp (Var x) = Var x ∧
+ ratExp2realExp (Unop u e1) = Unop u (ratExp2realExp e1) ∧
+ ratExp2realExp (Binop b e1 e2) = Binop b (ratExp2realExp e1) (ratExp2realExp e2) ∧
+ ratExp2realExp (Fma e1 e2 e3) = Fma (ratExp2realExp e1) (ratExp2realExp e2) (ratExp2realExp e3) ∧
+ ratExp2realExp (Downcast m e1) = Downcast m (ratExp2realExp e1)
+End
+
val _ = export_theory();
diff --git a/hol4/semantics/expressionsLib.sml b/hol4/semantics/expressionsLib.sml
new file mode 100644
index 00000000..8829fc7f
--- /dev/null
+++ b/hol4/semantics/expressionsLib.sml
@@ -0,0 +1,85 @@
+structure expressionsLib = struct
+
+ open HolKernel Parse Abbrev ExpressionsTheory;
+ open RealArith realTheory realLib integerTheory intLib bossLib;
+
+ exception FloVerException of string;
+
+ val fvar_tm = “Expressions$Varâ€
+ val fconst_tm = “Expressions$Constâ€
+ val unop_tm = “Expressions$Unopâ€
+ val bop_tm = “Expressions$Binopâ€
+ val fma_tm = “Expressions$Fmaâ€
+ val downcast_tm = “Expressions$Downcastâ€
+
+ local fun err s = FloVerException ("Not a FloVer " ^ s) in
+ val dest_fvar = HolKernel.dest_monop fvar_tm $ err "var"
+ val dest_fconst = HolKernel.dest_binop fconst_tm $ err "const"
+ val dest_unop = HolKernel.dest_binop unop_tm $ err "unop"
+ val dest_bop = HolKernel.dest_triop bop_tm $ err "bop"
+ val dest_fma = HolKernel.dest_triop fma_tm $ err "fma"
+ val dest_downcast = HolKernel.dest_binop downcast_tm $ err "downcast"
+ end;
+
+ local fun getArgTy t = type_of t |> dest_type |> snd |> hd in
+ fun mk_fvar ty n = mk_comb (fvar_tm, n) |> inst [alpha |-> ty]
+ fun mk_fconst m c = list_mk_comb (inst [alpha |-> type_of c] fconst_tm, [m, c])
+ fun mk_unop u e =
+ list_mk_comb (inst [alpha |-> getArgTy e] unop_tm, [u, e])
+ fun mk_bop b e1 e2 =
+ list_mk_comb (inst [alpha |-> getArgTy e1] bop_tm, [b, e1, e2])
+ fun mk_fma e1 e2 e3 =
+ list_mk_comb (inst [alpha |-> getArgTy e1] fma_tm, [e1, e2, e3])
+ fun mk_downcast m e =
+ list_mk_comb (inst [alpha |-> getArgTy e] downcast_tm, [m, e])
+ end;
+
+ val is_fvar = can dest_fvar
+ val is_fconst = can dest_fconst
+ val is_unop = can dest_unop
+ val is_bop = can dest_bop
+ val is_fma = can dest_fma
+ val is_downcast = can dest_downcast
+
+ fun realExp2ratExp (t:term) :term =
+ if type_of t = “:real expr†then
+ if is_fvar t then let
+ val var = dest_fvar t in
+ mk_fvar “:(int # int)†var end
+ else if is_fconst t then let
+ val (m,cst) = dest_fconst t
+ val (n,d) =
+ if realSyntax.is_div cst then
+ realSyntax.dest_div cst
+ else raise FloVerException ("Not a rational number" ^ (term_to_string cst))
+ val ni =
+ if realSyntax.is_real_literal n then
+ intSyntax.term_of_int $ realSyntax.int_of_term n
+ else raise FloVerException "Nominator not constant"
+ val di =
+ if realSyntax.is_real_literal d then
+ intSyntax.term_of_int $ realSyntax.int_of_term d
+ else raise FloVerException "Denominator not constant"
+ in
+ mk_fconst m (Parse.Term ‘(^ni, ^di)’) end
+ else if is_unop t then let
+ val (uop, e) = dest_unop t in
+ mk_unop uop (realExp2ratExp e) end
+ else if is_bop t then let
+ val (bop, e1, e2) = dest_bop t in
+ mk_bop bop (realExp2ratExp e1) (realExp2ratExp e2) end
+ else if is_fma t then let
+ val (e1, e2, e3) = dest_fma t in
+ mk_fma (realExp2ratExp e1) (realExp2ratExp e2) (realExp2ratExp e3) end
+ else if is_downcast t then let
+ val (m, e) = dest_downcast t in
+ mk_downcast m (realExp2ratExp e) end
+ else raise FloVerException ("Unsupported expression constructor in" ^ (term_to_string t))
+ else raise FloVerException "Not a real-valued expression";
+
+ fun realExp2ratExpConv t =
+ let val t_rat = realExp2ratExp t in
+ EVAL “^t = ratExp2realExp ^t_rat†|> Rewrite.REWRITE_RULE [boolTheory.EQ_CLAUSES]
+ end;
+
+end;
--
GitLab