From 1dc9cf42af4cc325ad5c8bb94abd6ad71b5179ff Mon Sep 17 00:00:00 2001
From: Heiko Becker <hbecker@mpi-sws.org>
Date: Tue, 4 Jan 2022 07:47:05 +0100
Subject: [PATCH] Fixes to make FloVer compile with latest HOL
---
hol4/ErrorValidationScript.sml | 9 ++++++---
hol4/IEEE_connectionScript.sml | 2 +-
hol4/IntervalArithScript.sml | 2 +-
hol4/IntervalValidationScript.sml | 6 +++---
hol4/sqrtApproxScript.sml | 16 ----------------
5 files changed, 11 insertions(+), 24 deletions(-)
diff --git a/hol4/ErrorValidationScript.sml b/hol4/ErrorValidationScript.sml
index 7bd665a8..49dc7816 100644
--- a/hol4/ErrorValidationScript.sml
+++ b/hol4/ErrorValidationScript.sml
@@ -2323,9 +2323,9 @@ Proof
\\ irule computeError_up
\\ irule contained_leq_maxAbs
\\ gs[contained_def] \\ conj_tac \\ irule REAL_LE_TRANS
- >- (asm_exists_tac \\ gs[] \\ irule transcTheory.SQRT_MONO_LE \\ real_prove)
+ >- (asm_exists_tac \\ gs[] \\ irule SQRT_MONO_LE \\ real_prove)
\\ once_rewrite_tac[CONJ_COMM] \\ asm_exists_tac \\ gs[]
- \\ irule transcTheory.SQRT_MONO_LE \\ gs[] \\ REAL_ASM_ARITH_TAC
+ \\ irule SQRT_MONO_LE \\ gs[] \\ REAL_ASM_ARITH_TAC
QED
(**
@@ -2440,7 +2440,10 @@ Proof
by (
inversion `eval_expr E1 _ (Unop Sqrt _) _ _` eval_expr_cases \\ fs[]
\\ Cases_on ‘m1'’ \\ gs[isCompat_def, perturb_def]
- \\ imp_res_tac meps_0_deterministic \\ gs[])
+ \\ ‘v1'' = v1’ suffices_by gs[]
+ \\ irule meps_0_deterministic
+ \\ qexistsl_tac [‘E1’, ‘λ e. FloverMapTree_find e Gamma’, ‘e’]
+ \\ gs[])
\\ rveq \\ gs[])
>- simp[Once validErrorbound_def]
\\ irule Unop_sqrt' \\ fsrw_tac [SATISFY_ss] [updDefVars_def]
diff --git a/hol4/IEEE_connectionScript.sml b/hol4/IEEE_connectionScript.sml
index 8428a2cf..e966341a 100644
--- a/hol4/IEEE_connectionScript.sml
+++ b/hol4/IEEE_connectionScript.sml
@@ -808,7 +808,7 @@ Proof
\\ fs[perturb_def, evalUnop_def]
\\ fs[REAL_INV_1OVER, mTypeToR_def, isCompat_def, minExponentPos_def])
(* sqrt 0 *)
- \\ ‘0 < sqrt (float_to_real (fp64_to_float v))’ by (irule transcTheory.SQRT_POS_LT \\ gs[])
+ \\ ‘0 < sqrt (float_to_real (fp64_to_float v))’ by (irule SQRT_POS_LT \\ gs[])
\\ gs[evalUnop_def])
>- (
rename1 `Binop b (toRExp e1) (toRExp e2)` \\ rveq
diff --git a/hol4/IntervalArithScript.sml b/hol4/IntervalArithScript.sml
index 3419d12a..7dd1cce4 100644
--- a/hol4/IntervalArithScript.sml
+++ b/hol4/IntervalArithScript.sml
@@ -280,7 +280,7 @@ Theorem iv_sqrt_preserves_valid:
0 ≤ IVlo iv ∧ valid iv ⇒ valid (sqrtInterval iv)
Proof
gs[valid_def, sqrtInterval_def] \\ rpt strip_tac
- \\ irule transcTheory.SQRT_MONO_LE \\ gs[]
+ \\ irule SQRT_MONO_LE \\ gs[]
QED
val interval_addition_valid = store_thm ("interval_addition_valid",
diff --git a/hol4/IntervalValidationScript.sml b/hol4/IntervalValidationScript.sml
index 62c34267..74652b56 100644
--- a/hol4/IntervalValidationScript.sml
+++ b/hol4/IntervalValidationScript.sml
@@ -282,10 +282,10 @@ Proof
>- (
irule REAL_LE_TRANS \\ asm_exists_tac \\ gs[]
\\ irule REAL_LE_TRANS \\ asm_exists_tac \\ gs[]
- \\ irule transcTheory.SQRT_MONO_LE \\ real_prove)
+ \\ irule SQRT_MONO_LE \\ real_prove)
\\ irule REAL_LE_TRANS \\ qexists_tac ‘sqrt (SND iv)’ \\ conj_tac
>- (
- irule transcTheory.SQRT_MONO_LE \\ gs[]
+ irule SQRT_MONO_LE \\ gs[]
\\ irule REAL_LE_TRANS \\ qexists_tac ‘FST iv’ \\ real_prove)
\\ irule REAL_LE_TRANS \\ asm_exists_tac \\ gs[])
(* Binary operator case *)
@@ -559,7 +559,7 @@ Proof
\\ strip_tac
\\ irule REAL_LE_TRANS \\ asm_exists_tac \\ gs[]
\\ irule REAL_LE_TRANS \\ qexists_tac ‘sqrt(SND iv)’\\ gs[]
- \\ irule transcTheory.SQRT_MONO_LE \\ real_prove)
+ \\ irule SQRT_MONO_LE \\ real_prove)
>- (rename1 `Binop b f1 f2`
\\ rpt (first_x_assum (qspecl_then [`A`, `P`, `dVars`] destruct) \\ fs[])
\\ rveq \\ fs[]
diff --git a/hol4/sqrtApproxScript.sml b/hol4/sqrtApproxScript.sml
index cec97a19..d15f2768 100644
--- a/hol4/sqrtApproxScript.sml
+++ b/hol4/sqrtApproxScript.sml
@@ -3,22 +3,6 @@ open preambleFloVer;
val _ = new_theory "sqrtApprox";
-(*
-Definition newton_helper_def:
- newton_helper 0 n (x:real) = x ∧
- newton_helper (SUC n) (init:real) x = newton_helper n init ((x + (init / x)) / 2)
-End
-
-Definition newton_def:
- newton (n:num) (x:real) = newton_helper n x x
-End
-
-Definition newton_def:
- newton 0 n (x:real) = x ∧
- newton (SUC n) m x = newton n m ((x + (&m / x)) / 2)
-End
-*)
-
Definition newton_def:
newton 0 n (x:real) = x ∧
newton (SUC n) (m:real) x = newton n m ((x + (m / x)) / 2)
--
GitLab