From 1b06f7879582527a2534f6267e4166841646d56d Mon Sep 17 00:00:00 2001
From: Heiko Becker <hbecker@mpi-sws.org>
Date: Mon, 18 Jan 2021 16:02:44 +0100
Subject: [PATCH] Update FloVer to work with latest HOL4 develop
---
hol4/EnvironmentsScript.sml | 6 +-
hol4/ErrorBoundsScript.sml | 132 +++++---
hol4/FPRangeValidatorScript.sml | 229 +++++++-------
hol4/IEEE_connectionScript.sml | 485 ++++++++++++++++--------------
hol4/Infra/MachineTypeScript.sml | 86 +++---
hol4/IntervalValidationScript.sml | 5 +
hol4/TypeValidatorScript.sml | 326 +++++++++++++-------
7 files changed, 740 insertions(+), 529 deletions(-)
diff --git a/hol4/EnvironmentsScript.sml b/hol4/EnvironmentsScript.sml
index 86b25426..d70808ae 100644
--- a/hol4/EnvironmentsScript.sml
+++ b/hol4/EnvironmentsScript.sml
@@ -125,7 +125,7 @@ Proof
QED
Theorem approxEnv_dVar_bounded:
- !E1 Gamma A fVars dVars E2 x v v2 m iv e.
+ !E1 (Gamma:real expr -> mType option) (A:analysisResult) fVars dVars E2 x v v2 m iv e.
approxEnv E1 Gamma A fVars dVars E2 /\
E1 x = SOME v /\
E2 x = SOME v2 /\
@@ -151,8 +151,8 @@ Theorem approxEnv_refl:
approxEnv E1 Gamma A fVars dVars E1
Proof
rw[approxEnv_def] \\ res_tac \\ fsrw_tac [SATISFY_ss] []
- \\ Cases_on ‘m’ \\ fs[computeError_def, mTypeToR_pos]
- \\ irule REAL_LE_MUL \\ fs[mTypeToR_pos]
+ \\ Cases_on ‘m’ \\ fs[mTypeToR_pos]
+ \\ irule computeError_pos
QED
val _ = export_theory ();;
diff --git a/hol4/ErrorBoundsScript.sml b/hol4/ErrorBoundsScript.sml
index 4d8597d9..5817a258 100644
--- a/hol4/ErrorBoundsScript.sml
+++ b/hol4/ErrorBoundsScript.sml
@@ -14,7 +14,7 @@ val _ = Parse.hide "delta"; (* so that it can be used as a variable *)
val _ = temp_overload_on("abs",``real$abs``);
val triangle_tac =
- irule triangle_trans \\ fs[REAL_ABS_TRIANGLE];
+ irule triangle_trans \\ rpt conj_tac \\ TRY (fs[REAL_ABS_TRIANGLE] \\ NO_TAC);
Theorem const_abs_err_bounded:
!(n:real) (nR:real) (nF:real) (E1 E2:env) (m:mType) Gamma.
@@ -109,14 +109,14 @@ val float_sub_tac =
\\ `e1R + (-e2R + -((1 + deltaF) * (e1F + -e2F))) =
(e1R + - e1F) + ((- e2R + e2F) + - (e1F + - e2F) * deltaF)`
by REAL_ASM_ARITH_TAC
- \\ simp []
+ \\ pop_assum (once_rewrite_tac o single)
\\ triangle_tac
\\ irule REAL_LE_ADD2 \\ conj_tac
>- fs[GSYM real_sub]
\\ triangle_tac
\\ irule REAL_LE_ADD2 \\ conj_tac
>- REAL_ASM_ARITH_TAC
- \\ once_rewrite_tac [REAL_ABS_MUL, ABS_NEG]
+ \\ rewrite_tac [REAL_ABS_MUL, ABS_NEG]
\\ metis_tac [REAL_ABS_POS, REAL_LE_LMUL_IMP, REAL_MUL_COMM];
Theorem subtract_abs_err_bounded:
@@ -181,12 +181,11 @@ val float_mul_tac =
`e1R * e2R + -(e1F * e2F * (1 + deltaF)) =
(e1R * e2R + - (e1F * e2F)) + - (e1F * e2F * deltaF)`
by REAL_ASM_ARITH_TAC
- \\ simp[]
+ \\ pop_assum (once_rewrite_tac o single)
\\ triangle_tac
- \\ rewrite_tac[GSYM REAL_MUL_ASSOC]
- \\ once_rewrite_tac [REAL_ABS_MUL]
+ \\ rewrite_tac [ABS_NEG, REAL_ABS_MUL] \\ rename1 ‘abs errF ≤ mTypeToR _’
\\ simp[computeError_def]
- \\ metis_tac [REAL_LE_LMUL_IMP, REAL_MUL_COMM, REAL_ABS_POS];
+ \\ metis_tac [REAL_LE_LMUL_IMP, REAL_ABS_MUL, REAL_ABS_POS];
Theorem mult_abs_err_bounded:
! (e1:real expr) (e1R:real) (e1F:real) (e2:real expr) (e2R:real) (e2F:real)
@@ -235,15 +234,23 @@ Proof
\\ fs[ABS_NEG, computeError_def]
QED
+Theorem REAL_LE_MUL_SWAP:
+ ∀ (a b c:real).
+ a * b ≤ a * c ⇒ b * a ≤ a * c
+Proof
+ rpt strip_tac \\ fs[]
+QED
+
val float_div_tac =
`e1R / e2R + -(e1F / e2F * (1 + deltaF)) =
(e1R / e2R + - (e1F / e2F)) + - (e1F / e2F * deltaF)`
by REAL_ASM_ARITH_TAC
- \\ simp[]
+ \\ once_rewrite_tac [GSYM real_div]
+ \\ pop_assum (fn thm => once_rewrite_tac [thm])
\\ triangle_tac
- \\ once_rewrite_tac [REAL_ABS_MUL]
- \\ simp[computeError_def]
- \\ metis_tac [REAL_LE_LMUL_IMP, REAL_MUL_COMM, REAL_ABS_POS];
+ \\ once_rewrite_tac [ABS_NEG]
+ \\ simp[computeError_def, REAL_ABS_MUL]
+ \\ metis_tac [REAL_LE_LMUL_IMP, REAL_ABS_POS, REAL_LE_MUL_SWAP];
Theorem div_abs_err_bounded:
!(e1:real expr) (e1R:real) (e1F:real) (e2:real expr) (e2R:real) (e2F:real)
@@ -300,8 +307,8 @@ val float_fma_tac =
\\ triangle_tac
\\ irule REAL_LE_ADD2 \\ conj_tac
\\ TRY (REAL_ASM_ARITH_TAC)
- \\ once_rewrite_tac[REAL_ABS_MUL]
- \\ metis_tac [REAL_LE_LMUL_IMP, REAL_MUL_COMM, REAL_ABS_POS];
+ \\ rewrite_tac[REAL_ABS_MUL, ABS_NEG]
+ \\ metis_tac [REAL_LE_LMUL_IMP, REAL_MUL_COMM, REAL_ABS_POS, REAL_LE_MUL_SWAP];
Theorem fma_abs_err_bounded:
!(e1:real expr) (e1R:real) (e1F:real) (e2:real expr) (e2R:real) (e2F:real)
@@ -389,7 +396,7 @@ Proof
\\ Cases_on `m1` \\ fs[perturb_def, computeError_def]
\\ once_rewrite_tac [REAL_LDISTRIB]
\\ simp[real_sub, REAL_NEG_ADD, REAL_ADD_ASSOC, ABS_NEG, ABS_MUL]
- \\ metis_tac [REAL_LE_LMUL_IMP, ABS_POS, REAL_MUL_COMM]
+ \\ metis_tac [REAL_LE_LMUL_IMP, ABS_POS, REAL_MUL_COMM, REAL_LE_MUL_SWAP]
QED
Theorem nonzerop_EQ1_I'[simp]:
@@ -424,34 +431,35 @@ Proof
\\ `0 <= - (inv nR - inv nF) ` by REAL_ASM_ARITH_TAC
\\ `abs (- (inv nR - inv nF)) = - (inv nR - inv nF)` by fs [ABS_REFL]
\\ `abs (inv nR - inv nF) = - (inv nR - inv nF)` by metis_tac[ABS_NEG]
- \\ simp[REAL_INV_1OVER, real_sub, REAL_NEG_ADD]
+ \\ simp[real_sub, REAL_NEG_ADD]
\\ rpt (qpat_x_assum `abs v = v'` kall_tac)
- \\ `- (1 / nR) = 1 / - nR`
+ \\ `- (inv nR) = inv (- nR)`
by (fs [real_div] \\ irule REAL_NEG_INV \\ REAL_ASM_ARITH_TAC)
\\ simp[]
- \\ qspec_then `1 / -nR + 1 / (nR - err)` match_mp_tac real_le_trans2 \\ conj_tac
+ \\ qspec_then `inv (-nR) + inv (nR - err)` match_mp_tac real_le_trans2 \\ conj_tac
>- (match_mp_tac REAL_LE_LADD_IMP
\\ ‘0 < nR - err ∧ nR - err ≤ nF’ by REAL_ASM_ARITH_TAC
- \\ simp[GSYM REAL_INV_1OVER])
+ \\ simp[])
>- (`- nR <> 0 /\ nR - err <> 0` by REAL_ASM_ARITH_TAC
- \\ fs [REAL_ADD_RAT] (* Goal: (nR − err + -nR) / (-nR * (nR − err)) ≤ err * (1 / (elo + -err) pow 2) *)
+ \\ ‘(nR - err + -nR) / (-nR * (nR - err)) ≤ err * (1 / (elo + -err) pow 2)’
+ suffices_by (rewrite_tac[REAL_INV_1OVER] \\ fs[REAL_ADD_RAT])
\\ `nR - err + - nR = - err` by REAL_ASM_ARITH_TAC
\\ pop_assum (rewrite_tac o single)
\\ qspec_then `nR` (fn thm => fs [real_div, GSYM thm]) REAL_NEG_LMUL
- (* Goal: -(err * inv (-(nR * (nR − err)))) ≤ err * inv ((elo + -err)pow 2) *)
- \\ `nR <> 0` by REAL_ASM_ARITH_TAC
+ (* Goal: -(err * inv (-(nR * (nR − err)))) ≤ err * inv ((elo + -err) pow 2) *)
\\ `nR * (nR - err) <> 0` by fs[REAL_ENTIRE]
\\ fs [GSYM REAL_NEG_INV, GSYM REAL_NEG_LMUL, GSYM REAL_NEG_RMUL]
(* Goal: err * inv (nR * (nR − err)) ≤ err * inv ((elo + -err) pow 2) *)
+ \\ rewrite_tac [REAL_POW_INV]
\\ match_mp_tac REAL_LE_LMUL_IMP \\ conj_tac \\ simp[]
\\ rpt (qpat_x_assum `T` kall_tac)
\\ `0 < elo + - err` by REAL_ASM_ARITH_TAC
\\ `0 < (elo + - err) * (elo + - err)` by fs[REAL_LT_MUL]
\\ match_mp_tac REAL_INV_LE_ANTIMONO_IMPR \\ conj_tac
>- (match_mp_tac REAL_LT_MUL \\ REAL_ASM_ARITH_TAC)
- >- (conj_tac
- >- (fs[POW_2])
- >- (once_rewrite_tac [POW_2] \\ irule REAL_LE_MUL2 \\ REAL_ASM_ARITH_TAC))))
+ \\ conj_tac
+ >- (fs[POW_2])
+ \\ once_rewrite_tac [POW_2] \\ irule REAL_LE_MUL2 \\ REAL_ASM_ARITH_TAC))
>- (fs[]
\\ `nR <= nF` by REAL_ASM_ARITH_TAC
\\ `0 < nF` by REAL_ASM_ARITH_TAC
@@ -459,28 +467,38 @@ Proof
\\ `inv nF <= inv nR` by fs [REAL_INV_LE_ANTIMONO]
\\ `0 <= inv nR - inv nF` by REAL_ASM_ARITH_TAC \\ qpat_x_assum `inv nF <= inv nR` kall_tac
\\ `abs (inv nR - inv nF) = inv nR - inv nF` by fs[ABS_REFL] \\ qpat_x_assum `0 <= inv a - b` kall_tac
- \\ simp [REAL_INV_1OVER, real_sub, REAL_NEG_ADD]
+ \\ simp [real_sub, REAL_NEG_ADD]
\\ rpt (qpat_x_assum `abs x = y` kall_tac)
- \\ qspec_then `1 / nR + - (1 / (nR + err))` match_mp_tac real_le_trans2 \\ conj_tac
+ \\ qspec_then `inv nR + - (inv (nR + err))` match_mp_tac real_le_trans2 \\ conj_tac
>- (match_mp_tac REAL_LE_LADD_IMP
\\ `0 < nR + err /\ nF <= nR + err` by REAL_ASM_ARITH_TAC
\\ fs[GSYM REAL_INV_1OVER, REAL_INV_LE_ANTIMONO])
- >- (` - nR <> 0 /\ nR - err <> 0` by REAL_ASM_ARITH_TAC
- \\ `- (1 / (nR + err)) = 1 / - (nR + err)` by (fs [real_div] \\ match_mp_tac REAL_NEG_INV \\ REAL_ASM_ARITH_TAC)
+ >- (`- nR <> 0 /\ nR - err <> 0` by REAL_ASM_ARITH_TAC
+ \\ `- (inv (nR + err)) = inv (- (nR + err))`
+ by (fs [real_div] \\ match_mp_tac REAL_NEG_INV \\ REAL_ASM_ARITH_TAC)
+ \\ pop_assum (rewrite_tac o single)
\\ `- (nR + err) <> 0` by REAL_ASM_ARITH_TAC
\\ `nR <> 0` by REAL_ASM_ARITH_TAC
- \\ fs [REAL_ADD_RAT] (* Goal: (-(nR + err) + nR) / (nR * -(nR + err)) ≤ err * (1 / (elo + -err) pow 2) *)
+ \\ rewrite_tac[REAL_INV_1OVER]
+ \\ ‘1 / - (nR + err) = -1 / (nR + err)’ by (fs[neg_rat])
+ \\ pop_assum (rewrite_tac o single)
+ \\ ‘1 / nR + -1 / (nR + err) = (-(nR + err) + nR) / (nR * -(nR + err))’
+ by (fs[REAL_ADD_RAT, real_div, REAL_MUL_LNEG, REAL_MUL_RNEG]
+ \\ rewrite_tac[GSYM REAL_MUL_RNEG, REAL_NEG_ADD, REAL_NEG_NEG])
+ \\ pop_assum (rewrite_tac o single)
+ (* Goal: (-(nR + err) + nR) / (nR * -(nR + err)) ≤ err * (1 / (elo + -err) pow 2) *)
\\ `- (nR + err) + nR = - err` by REAL_ASM_ARITH_TAC
- \\ qspec_then `nR` (fn thm => fs [real_div, GSYM thm]) REAL_NEG_LMUL
- \\ simp [REAL_NEG_RMUL, REAL_NEG_INV]
- (* Goal: err * inv (nR * (nR + err)) ≤ err * inv ((elo + -err) pow 2) *)
+ \\ pop_assum (rewrite_tac o single)
+ \\ rewrite_tac[real_div, GSYM REAL_NEG_LMUL, REAL_NEG_RMUL]
\\ match_mp_tac REAL_LE_LMUL_IMP \\ conj_tac \\ simp[]
+ \\ fs [REAL_NEG_INV, REAL_NEG_RMUL, REAL_NEG_NEG]
+ (* Goal: inv (nR * (nR + err)) ≤ inv ((elo + -err) pow 2)) *)
\\ match_mp_tac REAL_INV_LE_ANTIMONO_IMPR \\ conj_tac
- >- (match_mp_tac REAL_LT_MUL \\ REAL_ASM_ARITH_TAC)
- >- (conj_tac \\ once_rewrite_tac [POW_2]
- >- (match_mp_tac REAL_LT_MUL
- \\ REAL_ASM_ARITH_TAC)
- >- (match_mp_tac REAL_LE_MUL2 \\ REAL_ASM_ARITH_TAC))))
+ >- (match_mp_tac REAL_LT_MUL \\ REAL_ASM_ARITH_TAC)
+ \\ conj_tac \\ once_rewrite_tac [POW_2]
+ >- (match_mp_tac REAL_LT_MUL
+ \\ REAL_ASM_ARITH_TAC)
+ \\ match_mp_tac REAL_LE_MUL2 \\ REAL_ASM_ARITH_TAC))
QED
Theorem err_prop_inversion_neg:
@@ -508,14 +526,18 @@ Proof
\\ `0 <= - (inv (- nF) - inv (-nR)) ` by REAL_ASM_ARITH_TAC
\\ `abs (- (inv (- nF) - inv (- nR))) = - (inv (- nF) - inv (- nR))` by fs [ABS_REFL]
\\ `abs (inv (- nF) - inv (- nR)) = - (inv (- nF) - inv (- nR))` by metis_tac[ABS_NEG]
- \\ `inv (- nF) - inv (- nR) = inv nR - inv nF` by (fs[GSYM REAL_NEG_INV, real_sub] \\ REAL_ASM_ARITH_TAC)
+ \\ `inv (- nF) - inv (- nR) = inv nR - inv nF`
+ by (fs[GSYM REAL_NEG_INV, real_sub] \\ REAL_ASM_ARITH_TAC)
\\ `abs (inv nR - inv nF) = - (inv nR - inv nF)` by fs[]
- \\ simp[REAL_INV_1OVER, real_sub, REAL_NEG_ADD]
+ \\ simp[real_sub, REAL_NEG_ADD]
\\ rpt (qpat_x_assum `abs v = v'` kall_tac)
- \\ `- (1 / nR) = 1 / - nR` by (fs [real_div] \\ match_mp_tac REAL_NEG_INV \\ REAL_ASM_ARITH_TAC)
+ \\ `- (1 / nR) = 1 / - nR`
+ by (fs [real_div] \\ match_mp_tac REAL_NEG_INV \\ REAL_ASM_ARITH_TAC)
\\ simp[]
\\ qspec_then `1 / -nR + 1 / (nR - err)` match_mp_tac real_le_trans2 \\ conj_tac
- >- (match_mp_tac REAL_LE_LADD_IMP
+ >- (once_rewrite_tac [REAL_INV_1OVER]
+ \\ pop_assum (rewrite_tac o single)
+ \\ match_mp_tac REAL_LE_LADD_IMP
\\ simp[GSYM REAL_INV_1OVER]
\\ `nR - err <= nF` by REAL_ASM_ARITH_TAC
\\ `- nF <= - (nR - err)` by REAL_ASM_ARITH_TAC
@@ -528,9 +550,14 @@ Proof
\\ qpat_x_assum `-(inv nRerr) = v` (fn thm => once_rewrite_tac [thm])
\\ qpat_x_assum `-(inv nF) = v` (fn thm => once_rewrite_tac [thm])
\\ simp[])
- >- (`- nR <> 0 /\ nR - err <> 0` by REAL_ASM_ARITH_TAC \\ fs [REAL_ADD_RAT]
+ >- (`- nR <> 0 /\ nR - err <> 0` by REAL_ASM_ARITH_TAC
+ \\ ‘1 / -nR + 1 / (nR - err) = (1 * (nR - err) + -nR * 1) / (-nR * (nR - err))’
+ by (fs [REAL_ADD_RAT])
+ \\ pop_assum (rewrite_tac o single)
+ \\ rewrite_tac [REAL_MUL_LID, REAL_MUL_RID]
\\ `nR - err + - nR = - err` by REAL_ASM_ARITH_TAC
- \\ qspec_then `nR` (fn thm => fs [real_div, GSYM thm]) REAL_NEG_LMUL
+ \\ pop_assum (rewrite_tac o single)
+ \\ rewrite_tac [GSYM REAL_NEG_LMUL, real_div]
\\ `nR <> 0` by REAL_ASM_ARITH_TAC
\\ `nR * (nR - err) <> 0` by fs[REAL_ENTIRE]
\\ fs [GSYM REAL_NEG_INV, GSYM REAL_NEG_LMUL, GSYM REAL_NEG_RMUL]
@@ -563,23 +590,28 @@ Proof
\\ `inv (- nR) - inv (- nF) = inv nF - inv nR` by (fs[GSYM REAL_NEG_INV, real_sub] \\ REAL_ASM_ARITH_TAC)
\\ `abs (inv nF - inv nR) = - (inv (- nR) - inv (- nF))` by fs[]
\\ `abs (inv nR - inv nF) = - (inv (- nR) - inv (- nF))` by fs[ABS_SUB]
- \\ simp[REAL_INV_1OVER, real_sub, REAL_NEG_ADD]
+ \\ simp[real_sub, REAL_NEG_ADD]
\\ rpt (qpat_x_assum `abs v = v'` kall_tac)
\\ `- (1 / nF) = 1 / - nF` by (fs [real_div] \\ match_mp_tac REAL_NEG_INV \\ REAL_ASM_ARITH_TAC)
\\ simp[]
\\ qspec_then `1 / -(nR + err) + 1 / nR` match_mp_tac real_le_trans2 \\ conj_tac
- >- (once_rewrite_tac [REAL_ADD_COMM] \\ match_mp_tac REAL_LE_LADD_IMP
+ >- (once_rewrite_tac [REAL_ADD_COMM] \\ rewrite_tac [REAL_INV_1OVER]
+ \\ pop_assum (rewrite_tac o single)
+ \\ match_mp_tac REAL_LE_LADD_IMP
\\ `0 < - (nR + err) /\ nF <= nR + err` by REAL_ASM_ARITH_TAC
- \\ simp [GSYM REAL_INV_1OVER, REAL_LE_NEG, REAL_INV_LE_ANTIMONO])
+ \\ simp [REAL_LE_NEG, REAL_INV_LE_ANTIMONO])
>- (`- nR <> 0 /\ nR - err <> 0` by REAL_ASM_ARITH_TAC
\\ `- (nR + err) <> 0` by REAL_ASM_ARITH_TAC
- \\ fs [REAL_ADD_RAT]
+ \\ ‘1 / - (nR + err) + 1 / nR = (1 * nR + - (nR + err) * 1) / (- (nR + err) * nR)’
+ by (fs[REAL_ADD_RAT])
+ \\ pop_assum (rewrite_tac o single)
\\ `nR + - (nR + err) = - err` by REAL_ASM_ARITH_TAC
- \\ fs [real_div, GSYM REAL_NEG_RMUL]
- \\ simp [GSYM REAL_NEG_RMUL, GSYM REAL_NEG_LMUL]
+ \\ rewrite_tac [REAL_MUL_RID, REAL_MUL_LID, real_div, GSYM REAL_NEG_RMUL, GSYM REAL_NEG_LMUL]
+ \\ pop_assum (rewrite_tac o single)
\\ `inv (- ((nR + err) * nR)) = - (inv ((nR + err) * nR))`
by (match_mp_tac (GSYM REAL_NEG_INV) \\ fs[] \\ REAL_ASM_ARITH_TAC)
- \\ simp[REAL_NEG_RMUL]
+ \\ pop_assum (rewrite_tac o single)
+ \\ simp[GSYM REAL_NEG_RMUL, GSYM REAL_NEG_LMUL, REAL_NEG_NEG]
\\ match_mp_tac REAL_LE_LMUL_IMP \\ conj_tac \\ simp[]
\\ `0 < - (ehi + err)` by REAL_ASM_ARITH_TAC
\\ `0 < - (ehi + err) * -(ehi + err)` by (match_mp_tac REAL_LT_MUL \\ fs[])
diff --git a/hol4/FPRangeValidatorScript.sml b/hol4/FPRangeValidatorScript.sml
index ba69e2d4..5d3ae902 100644
--- a/hol4/FPRangeValidatorScript.sml
+++ b/hol4/FPRangeValidatorScript.sml
@@ -128,20 +128,22 @@ val solve_tac =
by (fs[widenInterval_def, IVlo_def, IVhi_def] \\ RealArith.REAL_ASM_ARITH_TAC)
\\ TRY (every_case_tac \\ RealArith.REAL_ASM_ARITH_TAC);
-val FPRangeValidator_sound = store_thm (
- "FPRangeValidator_sound",
- ``!e E1 E2 Gamma v m A fVars (dVars:num_set).
- approxEnv E1 (toRExpMap Gamma) A fVars dVars E2 /\
- eval_expr E2 (toRExpMap Gamma) e v m /\
- validTypes e Gamma /\
- validRanges e A E1 (toRTMap (toRExpMap Gamma)) /\
- validErrorbound e Gamma A dVars /\
- FPRangeValidator e A Gamma dVars /\
- domain (usedVars e) DIFF (domain dVars) SUBSET (domain fVars) /\
- (!(v:num). v IN domain dVars ==>
- (?vF m. E2 v = SOME vF /\ FloverMapTree_find (Var v) Gamma = SOME m
- /\ validFloatValue vF m)) ==>
- validFloatValue v m``,
+Theorem FPRangeValidator_sound:
+ ∀ e E1 E2 Gamma v m A fVars (dVars:num_set).
+ approxEnv E1 (toRExpMap Gamma) A fVars dVars E2 ∧
+ eval_expr E2 (toRExpMap Gamma) e v m ∧
+ validTypes e Gamma ∧
+ validRanges e A E1 (toRTMap (toRExpMap Gamma)) ∧
+ validErrorbound e Gamma A dVars ∧
+ FPRangeValidator e A Gamma dVars ∧
+ domain (usedVars e) DIFF (domain dVars) SUBSET (domain fVars) ∧
+ (∀(v:num).
+ v IN domain dVars ==>
+ (?vF m.
+ E2 v = SOME vF ∧ FloverMapTree_find (Var v) Gamma = SOME m ∧
+ validFloatValue vF m)) ==>
+ validFloatValue v m
+Proof
rpt strip_tac
\\ IMP_RES_TAC validTypes_single
\\ `m = mG`
@@ -165,10 +167,11 @@ val FPRangeValidator_sound = store_thm (
\\ fs[] \\ rveq \\ fs[]
\\ rpt (inversion `eval_expr E2 _ _ _ _` eval_expr_cases)
\\ fs[] \\ rveq \\ fs[])
- \\ solve_tac);
+ \\ solve_tac
+QED
Theorem FPRangeValidatorCmd_sound:
- !f E1 E2 Gamma v vR m A fVars dVars outVars.
+ ∀ f E1 E2 Gamma v vR m A fVars dVars outVars.
approxEnv E1 (toRExpMap Gamma) A fVars dVars E2 ∧
ssa f (union fVars dVars) outVars /\
bstep (toREvalCmd f) E1 (toRTMap (toRExpMap Gamma)) vR m /\
@@ -187,99 +190,107 @@ Proof
\\ simp[Once toREvalCmd_def, Once FPRangeValidatorCmd_def,
Once freeVars_def]
\\ rpt strip_tac
- >- (Flover_compute ``validErrorboundCmd``
- \\ rveq \\ fs[]
- \\ rpt (inversion `bstep (Let _ _ _ _) _ _ _ _` bstep_cases)
- \\ rveq
- \\ rename1 `bstep (toREvalCmd f) (updEnv n vR_e E1) _ _ mR`
- \\ rename1 `bstep f (updEnv n vF E2) _ _ mF`
- \\ fs[Once validTypesCmd_def]
- \\ IMP_RES_TAC validTypes_single
- \\ `m = mG`
- by (first_x_assum irule
- \\ qexistsl_tac [`E2`, `Gamma`, `vF`] \\ fs[])
- \\ rveq
- \\ inversion `ssa _ _ _` ssa_cases
- \\ drule validErrorbound_sound
- \\ disch_then drule
- \\ disch_then
- (qspecl_then [`vR_e`, `err_e`, `FST iv_e`, `SND iv_e`]
- impl_subgoal_tac)
- >- (fs[Once validRangesCmd_def]
- \\ fs[DIFF_DEF, SUBSET_DEF] \\ rpt strip_tac \\ first_x_assum irule
- \\ fs[domain_union]
- \\ CCONTR_TAC \\ fs[] \\ rveq
- \\ first_x_assum (qspec_then `n` assume_tac)
- \\ `n IN domain fVars \/ n IN domain dVars`
- suffices_by (fs[])
- \\ fs[])
- \\ fs[Once validRangesCmd_def]
- \\ IMP_RES_TAC validRanges_single
- \\ IMP_RES_TAC meps_0_deterministic \\ rveq \\ fs[]
- \\ rename1 `vR_e <= SND _`
- \\ first_x_assum
- (qspecl_then [`updEnv n vR_e E1`, `updEnv n vF E2`,
- `Gamma`, `v`, `vR`, `mF`, `A`,
- `fVars`, `insert n () dVars`, `outVars`]
- impl_subgoal_tac)
- >- (fs[] \\ rpt conj_tac
- >- (irule approxEnvUpdBound \\ fs[lookup_NONE_domain]
- \\ first_x_assum (qspecl_then [`vF`, `m`] irule)
- \\ qexists_tac `m` \\ fs[])
- >- (irule ssa_equal_set
- \\ qexists_tac `insert n () (union fVars dVars)`
- \\ conj_tac \\ TRY (fs[] \\ FAIL_TAC "")
- \\ rewrite_tac [domain_union, domain_insert]
- \\ rewrite_tac [UNION_DEF, INSERT_DEF]
- \\ fs[EXTENSION]
- \\ rpt strip_tac
- \\ metis_tac[])
- >- (fs[Once validTypesCmd_def])
- >- (IMP_RES_TAC validTypesCmd_single
- \\ find_exists_tac \\ fs[]
- \\ first_x_assum MATCH_ACCEPT_TAC)
- >- (fs[Once validRangesCmd_def])
- >- (`validRangesCmd f A (updEnv n vR_e E1) (toRTMap (toRExpMap Gamma))`
- by (first_x_assum irule \\ fs[])
- \\ IMP_RES_TAC validRangesCmd_single
- \\ rpt (find_exists_tac \\ fs[]))
- >- (fs[DIFF_DEF, domain_insert, SUBSET_DEF]
- \\ rpt strip_tac \\ first_x_assum irule
- \\ simp[Once freeVars_def]
- \\ once_rewrite_tac [domain_union]
- \\ fs[]
- \\ rw_thm_asm `x IN domain (freeVars f)` freeVars_def
- \\ fs[])
- \\ rpt strip_tac
- \\ fs[updEnv_def] \\ rveq \\ fs[]
- >- (qpat_x_assum `eval_expr E2 _ e nF _` kall_tac
- \\ drule FPRangeValidator_sound
- \\ rpt (disch_then drule)
- \\ disch_then irule \\ fs[]
- \\ fs[DIFF_DEF, domain_insert, SUBSET_DEF]
- \\ rpt strip_tac \\ first_x_assum irule
- \\ simp[Once freeVars_def]
- \\ once_rewrite_tac [domain_union]
- \\ fs[]
- \\ CCONTR_TAC \\ fs[] \\ rveq
- \\ first_x_assum (qspec_then `n` assume_tac)
- \\ res_tac)
- \\ TOP_CASE_TAC \\ fs[]
- \\ qpat_x_assum `eval_expr E2 _ e nF _` kall_tac
- \\ drule FPRangeValidator_sound
- \\ rpt (disch_then drule)
- \\ disch_then irule \\ fs[]
- \\ fs[DIFF_DEF, domain_insert, SUBSET_DEF]
- \\ rpt strip_tac \\ first_x_assum irule
- \\ simp[Once freeVars_def]
- \\ once_rewrite_tac [domain_union]
- \\ fs[]
- \\ CCONTR_TAC \\ fs[] \\ rveq
- \\ first_x_assum (qspec_then `n` assume_tac)
- \\ res_tac)
- \\ fs[])
- \\ Flover_compute ``validErrorboundCmd``
- \\ rveq \\ fs[]
+ >- (
+ qpat_x_assum ‘validErrorboundCmd _ _ _ _’
+ (mp_tac o SIMP_RULE std_ss [Once validErrorboundCmd_def]) \\ fs[]
+ \\ ntac 4 (TOP_CASE_TAC \\ fs[]) \\ strip_tac \\ rveq
+ \\ rpt (inversion `bstep (Let _ _ _ _) _ _ _ _` bstep_cases) \\ rveq
+ \\ rename1 `bstep (toREvalCmd f) (updEnv n vR_e E1) _ _ mR`
+ \\ rename1 `bstep f (updEnv n vF E2) _ _ mF`
+ \\ rename1 ‘FloverMapTree_find e A = SOME (iv_e, err_e)’
+ \\ fs[Once validTypesCmd_def]
+ \\ imp_res_tac validTypes_single
+ \\ `m = mG`
+ by (first_x_assum irule
+ \\ qexistsl_tac [`E2`, `Gamma`, `vF`] \\ fs[])
+ \\ rveq
+ \\ inversion `ssa _ _ _` ssa_cases
+ \\ drule validErrorbound_sound
+ \\ disch_then drule
+ \\ disch_then
+ (qspecl_then [`vR_e`, `err_e`, `FST iv_e`, `SND iv_e`]
+ impl_subgoal_tac)
+ >- (
+ fs[Once validRangesCmd_def]
+ \\ fs[DIFF_DEF, SUBSET_DEF] \\ rpt strip_tac \\ first_x_assum irule
+ \\ fs[domain_union]
+ \\ CCONTR_TAC \\ fs[] \\ rveq
+ \\ first_x_assum (qspec_then `n` assume_tac)
+ \\ `n IN domain fVars \/ n IN domain dVars`
+ suffices_by (fs[])
+ \\ fs[])
+ \\ fs[Once validRangesCmd_def]
+ \\ imp_res_tac validRanges_single
+ \\ imp_res_tac meps_0_deterministic \\ rveq \\ fs[]
+ \\ rename1 `vR_e <= SND _`
+ \\ first_x_assum
+ (qspecl_then [`updEnv n vR_e E1`, `updEnv n vF E2`, `Gamma`, `v`, `vR`,
+ `mF`, `A`, `fVars`, `insert n () dVars`, `outVars`]
+ impl_subgoal_tac)
+ >- (
+ fs[] \\ rpt conj_tac
+ >- (
+ irule approxEnvUpdBound \\ fs[lookup_NONE_domain]
+ \\ first_x_assum (qspecl_then [`vF`, `m`] irule)
+ \\ qexists_tac `m` \\ fs[])
+ >- (
+ irule ssa_equal_set
+ \\ qexists_tac `insert n () (union fVars dVars)`
+ \\ conj_tac \\ TRY (fs[] \\ FAIL_TAC "")
+ \\ rewrite_tac [domain_union, domain_insert]
+ \\ rewrite_tac [UNION_DEF, INSERT_DEF]
+ \\ fs[EXTENSION]
+ \\ rpt strip_tac
+ \\ metis_tac[])
+ >- fs[Once validTypesCmd_def]
+ >- (
+ imp_res_tac validTypesCmd_single
+ \\ find_exists_tac \\ fs[]
+ \\ first_x_assum MATCH_ACCEPT_TAC)
+ >- (fs[Once validRangesCmd_def])
+ >- (
+ `validRangesCmd f A (updEnv n vR_e E1) (toRTMap (toRExpMap Gamma))`
+ by (first_x_assum irule \\ fs[])
+ \\ imp_res_tac validRangesCmd_single
+ \\ rpt (find_exists_tac \\ fs[]))
+ >- (
+ fs[DIFF_DEF, domain_insert, SUBSET_DEF]
+ \\ rpt strip_tac \\ first_x_assum irule
+ \\ simp[Once freeVars_def]
+ \\ once_rewrite_tac [domain_union]
+ \\ fs[]
+ \\ rw_thm_asm `x IN domain (freeVars f)` freeVars_def
+ \\ fs[])
+ \\ rpt strip_tac
+ \\ fs[updEnv_def] \\ rveq \\ fs[]
+ >- (qpat_x_assum `eval_expr E2 _ e nF _` kall_tac
+ \\ drule FPRangeValidator_sound
+ \\ rpt (disch_then drule)
+ \\ disch_then irule \\ fs[]
+ \\ fs[DIFF_DEF, domain_insert, SUBSET_DEF]
+ \\ rpt strip_tac \\ first_x_assum irule
+ \\ simp[Once freeVars_def]
+ \\ once_rewrite_tac [domain_union]
+ \\ fs[]
+ \\ CCONTR_TAC \\ fs[] \\ rveq
+ \\ first_x_assum (qspec_then `n` assume_tac)
+ \\ res_tac)
+ \\ TOP_CASE_TAC \\ fs[]
+ \\ qpat_x_assum `eval_expr E2 _ e nF _` kall_tac
+ \\ drule FPRangeValidator_sound
+ \\ rpt (disch_then drule)
+ \\ disch_then irule \\ fs[]
+ \\ fs[DIFF_DEF, domain_insert, SUBSET_DEF]
+ \\ rpt strip_tac \\ first_x_assum irule
+ \\ simp[Once freeVars_def]
+ \\ once_rewrite_tac [domain_union]
+ \\ fs[]
+ \\ CCONTR_TAC \\ fs[] \\ rveq
+ \\ first_x_assum (qspec_then `n` assume_tac)
+ \\ res_tac)
+ \\ fs[])
+ \\ qpat_x_assum ‘validErrorboundCmd _ _ _ _’
+ (assume_tac o SIMP_RULE std_ss [Once validErrorboundCmd_def]) \\ fs[]
\\ rpt (inversion `bstep (Ret _) _ _ _ _` bstep_cases)
\\ drule FPRangeValidator_sound
\\ rpt (disch_then drule)
diff --git a/hol4/IEEE_connectionScript.sml b/hol4/IEEE_connectionScript.sml
index e36395ae..a8f86f10 100644
--- a/hol4/IEEE_connectionScript.sml
+++ b/hol4/IEEE_connectionScript.sml
@@ -223,17 +223,18 @@ val denormalValue_implies_finiteness = store_thm ("normalValue_implies_finitenes
\\ irule REAL_LE_TRANS \\ qexists_tac `1`
\\ fs[maxValue_def, maxExponent_def]);
-val normal_value_is_float_value = store_thm (
- "normal_value_is_float_value",
- ``!ff.
- normal (float_to_real ((ff):(52,11) float)) M64 ==>
- float_value ff = Float (float_to_real ff)``,
+Theorem normal_value_is_float_value:
+ ∀ ff.
+ normal (float_to_real ((ff):(52,11) float)) M64 ⇒
+ float_value ff = Float (float_to_real ff)
+Proof
rpt strip_tac
\\ rewrite_tac[float_value_def]
\\ rw_thm_asm `normal _ _` normal_def
\\ fs[float_to_real_def]
\\ every_case_tac
- \\ fs [maxValue_def, maxExponent_def, minValue_pos_def, minExponentPos_def, GSYM REAL_OF_NUM_POW, pow_simp1, REAL_DIV_LZERO]
+ \\ fs [maxValue_def, maxExponent_def, minValue_pos_def, minExponentPos_def,
+ GSYM REAL_OF_NUM_POW, pow_simp1, REAL_DIV_LZERO]
>-(Cases_on `ff.Sign` \\ fs[]
\\ Cases_on `n` \\ fs[pow]
>- (fs[GSYM POW_ABS, abs, REAL_OF_NUM_POW])
@@ -263,19 +264,18 @@ val normal_value_is_float_value = store_thm (
\\ Cases_on `ff.Significand` \\ fs[]
\\ Cases_on `n` \\ fs[pow]
\\ `abs (cst1 * cst2) = -(cst1 * cst2)`
- by (once_rewrite_tac[abs]
- \\ `~ (0 <= cst1 * cst2)` suffices_by (fs[] )
- \\ unabbrev_all_tac
- \\ once_rewrite_tac [REAL_MUL_LNEG] \\ fs[]
- \\ CCONTR_TAC \\ fs[REAL_LDISTRIB]
- \\ `0 <= - (2 pow 1024)`
- by (irule REAL_LE_TRANS \\ find_exists_tac \\ fs[GSYM REAL_NEG_LMUL, GSYM REAL_NEG_ADD]
- \\ qabbrev_tac `res = 2 pow 1024 + 2 pow 1024 * (&SUC n' / 2 pow 52)`
- \\ qspec_then `2 pow 1024` (fn thm => once_rewrite_tac [GSYM thm]) REAL_ADD_RID
- \\ unabbrev_all_tac
- \\ irule REAL_LE_LADD_IMP
- \\ irule REAL_LE_MUL \\ fs[])
- \\ fs[REAL_OF_NUM_POW])
+ by (
+ fs[abs]
+ \\ ‘~ (0 ≤ cst1 * cst2)’ suffices_by (fs[])
+ \\ unabbrev_all_tac
+ \\ once_rewrite_tac [REAL_NOT_LE]
+ \\ simp [GSYM REAL_NEG_LT0]
+ \\ rewrite_tac [GSYM REAL_MUL_ASSOC, GSYM REAL_NEG_MINUS1]
+ \\ fs[REAL_NEG_LT0]
+ \\ once_rewrite_tac [REAL_MUL_LNEG] \\ fs[REAL_NEG_LT0]
+ \\ irule REAL_LT_MUL \\ fs[]
+ \\ irule REAL_LT_ADD \\ fs[]
+ \\ irule REAL_LT_DIV \\ fs[])
\\ rw_asm_star `abs _ = _`
\\ `- cst1 <= cst3`
suffices_by (unabbrev_all_tac \\ fs[REAL_NEG_LMUL, REAL_NEGNEG, REAL_OF_NUM_POW])
@@ -286,19 +286,18 @@ val normal_value_is_float_value = store_thm (
\\ irule REAL_LE_LMUL_IMP
\\ unabbrev_all_tac \\ fs[]
\\ once_rewrite_tac [REAL_LE_ADDR]
- \\ conj_tac
- >- (once_rewrite_tac [real_div]
- \\ irule REAL_LE_MUL \\ fs[]
- \\ once_rewrite_tac[ REAL_INV_1OVER] \\ fs[])
- \\ fs[GSYM REAL_NEG_MINUS1]);
+ \\ rewrite_tac [GSYM REAL_NEG_MINUS1]
+ \\ fs[REAL_NEG_LT0]
+QED
-val denormal_value_is_float_value = store_thm ("denormal_value_is_float_value",
- ``!ff:(52,11) float.
+Theorem denormal_value_is_float_value:
+ ∀ ff:(52,11) float.
denormal (float_to_real ff) M64 ==>
- float_value ff = Float (float_to_real ff)``,
+ float_value ff = Float (float_to_real ff)
+Proof
rpt strip_tac
- \\rewrite_tac[float_value_def]
- \\rw_thm_asm `denormal _ _` denormal_def
+ \\ rewrite_tac[float_value_def]
+ \\ rw_thm_asm `denormal _ _` denormal_def
\\ TOP_CASE_TAC \\ fs[]
\\ rw_thm_asm `abs _ < _` float_to_real_def
\\ fs[]
@@ -316,23 +315,17 @@ val denormal_value_is_float_value = store_thm ("denormal_value_is_float_value",
\\ fs[REAL_INV1])
\\ Cases_on `c1` \\ fs[]
\\ `1 < abs (1 + &n / 4503599627370496)`
- by (fs[abs]
- \\ `0:real <= 1 + &n / 4503599627370496`
- by (irule REAL_LE_TRANS
- \\ qexists_tac `1` \\ fs[]
- \\ once_rewrite_tac [GSYM REAL_ADD_RID]
- \\ once_rewrite_tac [GSYM REAL_ADD_ASSOC]
- \\ irule REAL_LE_LADD_IMP
- \\ fs[REAL_ADD_RID, real_div]
- \\ irule REAL_LE_MUL \\ fs[]
- \\ irule REAL_LE_INV \\ fs[])
- \\ fs[]
- \\ once_rewrite_tac [GSYM REAL_ADD_RID]
- \\ once_rewrite_tac [GSYM REAL_ADD_ASSOC]
- \\ irule REAL_LT_IADD
- \\ fs[REAL_ADD_RID, real_div]
- \\ irule REAL_LT_MUL \\ fs[]
- \\ irule REAL_INV_POS \\ fs[])
+ by (
+ fs[abs]
+ \\ `0:real <= 1 + &n / 4503599627370496`
+ by (irule REAL_LE_TRANS
+ \\ qexists_tac `1` \\ fs[]
+ \\ irule REAL_LE_DIV \\ fs[])
+ \\ fs[]
+ \\ once_rewrite_tac [GSYM REAL_ADD_RID]
+ \\ once_rewrite_tac [GSYM REAL_ADD_ASSOC]
+ \\ fs[]
+ \\ irule REAL_LT_DIV \\ fs[])
\\ `44942328371557897693232629769725618340449424473557664318357520289433168951375240783177119330601884005280028469967848339414697442203604155623211857659868531094441973356216371319075554900311523529863270738021251442209537670585615720368478277635206809290837627671146574559986811484619929076208839082406056034304â»Â¹ <= inv 1`
by (irule REAL_INV_LE_ANTIMONO_IMPR \\ fs[])
\\ fs[pow_simp1, REAL_DIV_LZERO, ABS_1, REAL_OF_NUM_POW, abs]
@@ -351,7 +344,8 @@ val denormal_value_is_float_value = store_thm ("denormal_value_is_float_value",
\\ once_rewrite_tac [GSYM REAL_MUL_ASSOC] \\ irule REAL_LT_LMUL_IMP
\\ fs[]
\\ unabbrev_all_tac \\ fs[])
- \\ fs[REAL_INV1]);
+ \\ fs[REAL_INV1]
+QED
val validValue_gives_float_value = store_thm ("validValue_gives_float_value",
``!ff:(52,11) float.
@@ -573,139 +567,160 @@ Proof
\\ qexists_tac `0:real`
\\ fs[mTypeToR_pos, perturb_def, fp64_to_float_float_to_fp64,
zero_to_real])
- >- (fs[eval_expr_float_def, optionLift_def, toRExpMap_def, Once validTypes_def]
- \\ rveq \\ IMP_RES_TAC validTypes_single
- \\ `mG = M64`
- by (fs[is64BitEnv_def] \\ first_x_assum irule \\ fs[]
- \\ rveq \\ find_exists_tac \\ fs[])
- \\ rveq
- \\ `m' = M64`
+ >- (fs[Once validTypes_def]
+ \\ ‘M64 = mG’
by (first_x_assum irule
- \\ qexistsl_tac [`toREnv E2`, `Gamma`, `v1`] \\ fs[toRExpMap_def])
- \\ rveq
+ \\ qexistsl_tac [‘toREnv E2’, ‘Gamma’, ‘vR’] \\ rveq \\ fs[eval_expr_cases]
+ \\ qexistsl_tac [‘m'’, ‘v1’] \\ fs[])
+ \\ ‘m' = M64’ by (Cases_on ‘m'’ \\ fs[isCompat_def])
+ \\ ‘me = M64’ by (Cases_on ‘me’ \\ fs[isCompat_def])
+ \\ rveq \\ fs[isCompat_def] \\ rpt (qpat_x_assum ‘T’ kall_tac)
+ \\ fs[eval_expr_float_def]
\\ first_x_assum
(qspecl_then
[`E1`, `E2`, `E2_real`, `Gamma`, `v1`, `A`, `fVars`, `dVars`]
destruct)
- >- (fs[]
- \\ rpt conj_tac
- >- (fs[Once validTypes_def])
- >- (rveq \\ rpt strip_tac \\ first_x_assum irule
- \\ find_exists_tac \\ fs[]
- \\ qexistsl_tac [`E`, `v`] \\ fs[toRExpMap_def])
- >- (fs[Once validRanges_def])
- >- (Flover_compute ``validErrorbound``)
- >- (rw_thm_asm `FPRangeValidator _ _ _ _` FPRangeValidator_def
- \\ fs[]
- \\ Cases_on `FloverMapTree_find (Unop Neg (toRExp e)) A` \\ fs[]
- \\ PairCases_on `x` \\ fs[]
- \\ rw_asm_star `FloverMapTree_find (Unop _ _) Gamma = _`)
- >- (rw_thm_asm `domain (usedVars _) DIFF _ SUBSET _` usedVars_def
- \\ fs[])
- \\ rw_thm_asm `is64BitEval _` is64BitEval_def
- \\ fs[])
+ >- (
+ fs[] \\ rpt conj_tac
+ >- (fs[Once validTypes_def])
+ >- (rveq \\ rpt strip_tac
+ \\ drule validTypes_single \\ strip_tac \\ rfs[] \\ rveq
+ \\ first_x_assum irule
+ \\ find_exists_tac \\ fs[]
+ \\ asm_exists_tac \\ fs[])
+ >- (fs[Once validRanges_def])
+ >- (
+ qpat_x_assum ‘validErrorbound _ _ _ _’
+ (fn thm => assume_tac (ONCE_REWRITE_RULE [validErrorbound_def] thm))
+ \\ fs[option_case_eq]
+ \\ pop_assum mp_tac \\ rpt (TOP_CASE_TAC \\ fs[]))
+ >- (
+ rw_thm_asm `FPRangeValidator _ _ _ _` FPRangeValidator_def
+ \\ fs[]
+ \\ Cases_on `FloverMapTree_find (Unop Neg (toRExp e)) A` \\ fs[]
+ \\ PairCases_on `x` \\ fs[]
+ \\ rw_asm_star `FloverMapTree_find (Unop _ _) Gamma = _`)
+ >- (rw_thm_asm `domain (usedVars _) DIFF _ SUBSET _` usedVars_def \\ fs[])
+ \\ rw_thm_asm `is64BitEval _` is64BitEval_def
+ \\ fs[])
\\ fs[fp64_negate_def, fp64_to_float_float_to_fp64]
\\ once_rewrite_tac [float_to_real_negate]
\\ once_rewrite_tac [eval_expr_cases]
\\ fs[] \\ once_rewrite_tac [CONJ_COMM]
- \\ rveq \\ asm_exists_tac
- \\ fs[evalUnop_def]
- \\ find_exists_tac \\ fs[] )
- >- (Flover_compute ``validErrorbound``
- \\ rveq \\ fs[])
- >- (rename1 `Binop b (toRExp e1) (toRExp e2)` \\ rveq
- \\ IMP_RES_TAC validRanges_single
- \\ rw_thm_asm `validTypes _ _` validTypes_def
- \\ rw_thm_asm `validRanges _ _ _ _` validRanges_def
- \\ fs[eval_expr_float_def, optionLift_def]
- \\ IMP_RES_TAC validTypes_exec
- \\ `m1 = m1'`
- by (first_x_assum irule \\ qexistsl_tac [`toREnv E2`, `v1`]
- \\ rewrite_tac [toRExpMap_def]
- \\ first_x_assum MATCH_ACCEPT_TAC)
- \\ `m2 = m2'`
- by (first_x_assum irule \\ qexistsl_tac [`toREnv E2`, `v2`]
- \\ rewrite_tac [toRExpMap_def]
- \\ first_x_assum MATCH_ACCEPT_TAC)
- \\ rveq \\ first_x_assum kall_tac
- \\ `m1 = M64 /\ m2 = M64`
- by (fs[is64BitEnv_def]
- \\ conj_tac \\ first_x_assum irule \\ find_exists_tac \\ fs[])
- \\ rveq
- \\ rw_thm_asm `is64BitEval _` is64BitEval_def \\ fs[]
- \\ ntac 2
- (first_x_assum
- (qspecl_then [`E1`, `E2`,`E2_real`, `Gamma`] assume_tac))
- \\ first_x_assum (qspecl_then [`v1`, `A`, `fVars`, `dVars`] destruct)
- >- (rpt conj_tac \\ fs[]
- >- (Flover_compute ``validErrorbound``)
- >- (rw_thm_asm `FPRangeValidator _ _ _ _` FPRangeValidator_def
- \\ fs[] \\ rveq
- \\ rw_asm_star `FloverMapTree_find (Binop _ _ _) A = _`
- \\ rw_asm_star `FloverMapTree_find (Binop _ _ _) Gamma = _`)
- \\ rw_thm_asm `domain (usedVars _) DIFF _ SUBSET _` usedVars_def
- \\ fs[domain_union, DIFF_DEF, SUBSET_DEF, Once usedVars_def]
- \\ rpt strip_tac \\ first_x_assum irule \\ simp[Once usedVars_def])
- \\ first_x_assum (qspecl_then [`v2`, `A`, `fVars`, `dVars`] destruct)
- >- (rpt conj_tac \\ fs[]
- >- (Flover_compute ``validErrorbound``)
- >- (rw_thm_asm `FPRangeValidator _ _ _ _` FPRangeValidator_def
- \\ fs[] \\ rveq
- \\ rw_asm_star `FloverMapTree_find (Binop _ _ _) A = _`
- \\ rw_asm_star `FloverMapTree_find (Binop _ _ _) Gamma = _`)
- \\ rw_thm_asm `domain (usedVars _) DIFF _ SUBSET _` usedVars_def
- \\ fs[domain_union, DIFF_DEF, SUBSET_DEF])
- \\ fs[]
- \\ rename1 `eval_expr_float e1 _ = SOME vF1`
- \\ rename1 `eval_expr_float e2 _ = SOME vF2`
- \\ IMP_RES_TAC validRanges_single
- \\ rename1 `FloverMapTree_find (toRExp e2) A = SOME (iv2, err2)`
- \\ rename1 `FloverMapTree_find (toRExp e1) A = SOME (iv1, err1)`
- \\ rename1 `eval_expr E1 _ (toREval (toRExp e2)) nR2 REAL`
- \\ rename1 `eval_expr E1 _ (toREval (toRExp e1)) nR1 REAL`
- (* Obtain evaluation for E2_real*)
- \\ `!vF2 m2. eval_expr E2_real (toRExpMap Gamma) (toRExp e2) vF2 m2 ==>
- abs (nR2 - vF2) <= err2`
- by (qspecl_then [`toRExp e2`, `E1`, `E2_real`, `A`,`nR2`,
- `err2`, `FST iv2`, `SND iv2`, `fVars`,
- `dVars`,`Gamma`] destruct validErrorbound_sound
- \\ rpt conj_tac \\ fs[]
- >- (fs [DIFF_DEF, SUBSET_DEF]
- \\ rpt strip_tac \\ first_x_assum irule
- \\ once_rewrite_tac [usedVars_def] \\ fs[domain_union])
- \\ Flover_compute ``validErrorbound``)
+ \\ qexists_tac ‘M64’ \\ fs[isCompat_def]
+ \\ asm_exists_tac \\ fs[evalUnop_def])
+ >- (
+ qpat_x_assum ‘validErrorbound _ _ _ _’
+ (fn thm => mp_tac (ONCE_REWRITE_RULE [validErrorbound_def] thm))
+ \\ fs[option_case_eq] \\ rpt (TOP_CASE_TAC \\ fs[]))
+ >- (
+ rename1 `Binop b (toRExp e1) (toRExp e2)` \\ rveq
+ \\ IMP_RES_TAC validRanges_single
+ \\ rw_thm_asm `validTypes _ _` validTypes_def
+ \\ rw_thm_asm `validRanges _ _ _ _` validRanges_def
+ \\ fs[eval_expr_float_def, optionLift_def]
+ \\ IMP_RES_TAC validTypes_exec
+ (* \\ `m1 = m1'`
+ by (first_x_assum irule \\ qexistsl_tac [`toREnv E2`, `v1`]
+ \\ rewrite_tac [toRExpMap_def]
+ \\ first_x_assum MATCH_ACCEPT_TAC)
+ \\ `m2 = m2'`
+ by (first_x_assum irule \\ qexistsl_tac [`toREnv E2`, `v2`]
+ \\ rewrite_tac [toRExpMap_def]
+ \\ first_x_assum MATCH_ACCEPT_TAC) *)
+ \\ rveq
+ \\ `m1 = M64 /\ m2 = M64`
+ by (fs[is64BitEnv_def]
+ \\ conj_tac \\ first_x_assum irule \\ find_exists_tac \\ fs[])
+ \\ rveq
+ \\ rw_thm_asm `is64BitEval _` is64BitEval_def \\ fs[]
+ \\ ntac 2
+ (first_x_assum
+ (qspecl_then [`E1`, `E2`,`E2_real`, `Gamma`] assume_tac))
+ \\ first_x_assum (qspecl_then [`v1`, `A`, `fVars`, `dVars`] destruct)
+ >- (
+ rpt conj_tac \\ fs[]
+ >- (
+ qpat_x_assum ‘validErrorbound _ _ _ _’
+ (fn thm => mp_tac (ONCE_REWRITE_RULE [validErrorbound_def] thm))
+ \\ fs[option_case_eq] \\ rpt (TOP_CASE_TAC \\ fs[]))
+ >- (
+ rw_thm_asm `FPRangeValidator _ _ _ _` FPRangeValidator_def
+ \\ fs[] \\ rveq
+ \\ rw_asm_star `FloverMapTree_find (Binop _ _ _) A = _`
+ \\ rw_asm_star `FloverMapTree_find (Binop _ _ _) Gamma = _`)
+ \\ rw_thm_asm `domain (usedVars _) DIFF _ SUBSET _` usedVars_def
+ \\ fs[domain_union, DIFF_DEF, SUBSET_DEF, Once usedVars_def]
+ \\ rpt strip_tac \\ first_x_assum irule \\ simp[Once usedVars_def])
+ \\ first_x_assum (qspecl_then [`v2`, `A`, `fVars`, `dVars`] destruct)
+ >- (
+ rpt conj_tac \\ fs[]
+ >- (
+ qpat_x_assum ‘validErrorbound _ _ _ _’
+ (fn thm => mp_tac (ONCE_REWRITE_RULE [validErrorbound_def] thm))
+ \\ fs[option_case_eq] \\ rpt (TOP_CASE_TAC \\ fs[]))
+ >- (
+ rw_thm_asm `FPRangeValidator _ _ _ _` FPRangeValidator_def
+ \\ fs[] \\ rveq
+ \\ rw_asm_star `FloverMapTree_find (Binop _ _ _) A = _`
+ \\ rw_asm_star `FloverMapTree_find (Binop _ _ _) Gamma = _`)
+ \\ rw_thm_asm `domain (usedVars _) DIFF _ SUBSET _` usedVars_def
+ \\ fs[domain_union, DIFF_DEF, SUBSET_DEF])
+ \\ fs[]
+ \\ rename1 `eval_expr_float e1 _ = SOME vF1`
+ \\ rename1 `eval_expr_float e2 _ = SOME vF2`
+ \\ IMP_RES_TAC validRanges_single
+ \\ rename1 `FloverMapTree_find (toRExp e2) A = SOME (iv2, err2)`
+ \\ rename1 `FloverMapTree_find (toRExp e1) A = SOME (iv1, err1)`
+ \\ rename1 `eval_expr E1 _ (toREval (toRExp e2)) nR2 REAL`
+ \\ rename1 `eval_expr E1 _ (toREval (toRExp e1)) nR1 REAL`
+ (* Obtain evaluation for E2_real*)
+ \\ ‘!vF2 m2. eval_expr E2_real (toRExpMap Gamma) (toRExp e2) vF2 m2 ==>
+ abs (nR2 - vF2) <= err2’
+ by (qspecl_then [`toRExp e2`, `E1`, `E2_real`, `A`,`nR2`,
+ `err2`, `FST iv2`, `SND iv2`, `fVars`,
+ `dVars`,`Gamma`] destruct validErrorbound_sound
+ \\ rpt conj_tac \\ fs[]
+ >- (fs [DIFF_DEF, SUBSET_DEF]
+ \\ rpt strip_tac \\ first_x_assum irule
+ \\ once_rewrite_tac [usedVars_def] \\ fs[domain_union])
+ \\ qpat_x_assum ‘validErrorbound _ _ _ _’
+ (fn thm => mp_tac (ONCE_REWRITE_RULE [validErrorbound_def] thm))
+ \\ fs[option_case_eq] \\ rpt (TOP_CASE_TAC \\ fs[]))
\\ `contained (float_to_real (fp64_to_float vF2))
- (widenInterval (FST iv2, SND iv2) err2)`
- by (irule distance_gives_iv
- \\ qexists_tac `nR2` \\ fs [contained_def]
- \\ first_x_assum irule
- \\ qexists_tac `M64`
- \\ drule eval_eq_env
- \\ rpt (disch_then drule) \\ fs[])
- \\ `b = Div ==> float_to_real (fp64_to_float vF2) <> 0`
- by (strip_tac \\ rveq
- \\ Flover_compute ``validErrorbound``
- \\ fs[widenInterval_def, contained_def, noDivzero_def]
- >- (CCONTR_TAC \\ fs[] \\ rveq
- \\ `0 < 0:real`
- by (irule REAL_LET_TRANS
- \\ qexists_tac `SND iv2 + err2` \\ fs[])
- \\ fs[])
- >- (CCONTR_TAC \\ fs[] \\ rveq
- \\ `0 < 0:real`
- by (irule REAL_LTE_TRANS
- \\ qexists_tac `FST iv2 - err2` \\ fs[])
- \\ fs[])
- >- (CCONTR_TAC \\ fs[] \\ rveq
- \\ `0 < 0:real`
- by (irule REAL_LET_TRANS
- \\ qexists_tac `SND iv2 + err2` \\ fs[])
- \\ fs[])
- \\ CCONTR_TAC \\ fs[] \\ rveq
- \\ `0 < 0:real`
- by (irule REAL_LTE_TRANS
- \\ qexists_tac `FST iv2 - err2` \\ fs[])
- \\ fs[])
+ (widenInterval (FST iv2, SND iv2) err2)`
+ by (irule distance_gives_iv
+ \\ qexists_tac `nR2` \\ fs [contained_def]
+ \\ first_x_assum irule
+ \\ qexists_tac `M64`
+ \\ drule eval_eq_env
+ \\ rpt (disch_then drule) \\ fs[])
+ \\ `b = Div ==> float_to_real (fp64_to_float vF2) <> 0`
+ by (strip_tac \\ rveq
+ \\ qpat_x_assum ‘validErrorbound _ _ _ _’
+ (fn thm => mp_tac (ONCE_REWRITE_RULE [validErrorbound_def] thm))
+ \\ fs[widenInterval_def, contained_def, noDivzero_def]
+ \\ rpt strip_tac
+ >- (CCONTR_TAC \\ fs[] \\ rveq
+ \\ `0 < 0:real`
+ by (irule REAL_LET_TRANS
+ \\ qexists_tac `SND iv2 + err2` \\ fs[])
+ \\ fs[])
+ >- (CCONTR_TAC \\ fs[] \\ rveq
+ \\ `0 < 0:real`
+ by (irule REAL_LTE_TRANS
+ \\ qexists_tac `FST iv2 - err2` \\ fs[])
+ \\ fs[])
+ >- (CCONTR_TAC \\ fs[] \\ rveq
+ \\ `0 < 0:real`
+ by (irule REAL_LET_TRANS
+ \\ qexists_tac `SND iv2 + err2` \\ fs[])
+ \\ fs[])
+ \\ CCONTR_TAC \\ fs[] \\ rveq
+ \\ `0 < 0:real`
+ by (irule REAL_LTE_TRANS
+ \\ qexists_tac `FST iv2 - err2` \\ fs[])
+ \\ fs[])
\\ `validFloatValue
(evalBinop b (float_to_real (fp64_to_float vF1))
(float_to_real (fp64_to_float vF2))) M64`
@@ -720,14 +735,15 @@ Proof
\\ qexistsl_tac [`e1`, `e2`] \\ fs[]
\\ rpt conj_tac
>- (simp[Once validTypes_def] \\ first_x_assum MATCH_ACCEPT_TAC)
- >- (simp[Once validRanges_def] \\ find_exists_tac \\ fs[]
+ >- (simp[Once validRanges_def] \\ asm_exists_tac \\ fs[]
\\ fs[] \\ rveq \\ fs[])
\\ irule eval_eq_env
- \\ find_exists_tac \\ fs[eval_expr_cases]
- \\ qexistsl_tac [`M64`, `M64`, `float_to_real (fp64_to_float vF1)`,
- `float_to_real (fp64_to_float vF2)`, `0:real`]
- \\ Cases_on `b`
- \\ fs[perturb_def, evalBinop_def, mTypeToR_pos])
+ \\ qexists_tac ‘toREnv E2’ \\ rpt conj_tac >- fs[]
+ \\ irule Binop_dist'
+ \\ qexistsl_tac [‘0’, `M64`, `M64`, ‘M64’, `float_to_real (fp64_to_float vF1)`,
+ `float_to_real (fp64_to_float vF2)`]
+ \\ Cases_on `b`
+ \\ fs[perturb_def, evalBinop_def, mTypeToR_pos])
\\ `validFloatValue (float_to_real (fp64_to_float vF1)) M64`
by (drule FPRangeValidator_sound
\\ disch_then
@@ -743,7 +759,10 @@ Proof
\\ fs[] \\ rveq
\\ rw_asm_star `FloverMapTree_find (Binop _ _ _) A = _`
\\ rw_asm_star `FloverMapTree_find (Binop _ _ _) Gamma = _`)
- >- (Flover_compute ``validErrorbound``)
+ >- (
+ qpat_x_assum ‘validErrorbound _ _ _ _’
+ (fn thm => mp_tac (ONCE_REWRITE_RULE [validErrorbound_def] thm))
+ \\ fs[option_case_eq] \\ rpt (TOP_CASE_TAC \\ fs[]))
\\ irule eval_eq_env
\\ find_exists_tac \\ fs[])
\\ `validFloatValue (float_to_real (fp64_to_float vF2)) M64`
@@ -761,12 +780,16 @@ Proof
\\ fs[] \\ rveq
\\ rw_asm_star `FloverMapTree_find (Binop _ _ _) A = _`
\\ rw_asm_star `FloverMapTree_find (Binop _ _ _) Gamma = _`)
- >- (Flover_compute ``validErrorbound``)
+ >- (
+ qpat_x_assum ‘validErrorbound _ _ _ _’
+ (fn thm => mp_tac (ONCE_REWRITE_RULE [validErrorbound_def] thm))
+ \\ fs[option_case_eq] \\ rpt (TOP_CASE_TAC \\ fs[]))
\\ irule eval_eq_env
\\ find_exists_tac \\ fs[])
- \\ simp[eval_expr_cases]
+ (* \\ simp[eval_expr_cases] *)
(** Case distinction for operator **)
\\ Cases_on `b` \\ fs[optionLift_def, PULL_EXISTS, normal_or_zero_def]
+ \\ simp[Once eval_expr_cases]
(* Addition, result normal *)
>- (fs[fp64_add_def, fp64_to_float_float_to_fp64, evalBinop_def]
\\ `normal (evalBinop Plus (float_to_real (fp64_to_float vF1))
@@ -1035,7 +1058,11 @@ Proof
(qspecl_then [`E1`, `E2`,`E2_real`, `Gamma`] assume_tac))
\\ first_x_assum (qspecl_then [`v1`, `A`, `fVars`, `dVars`] destruct)
>- (rpt conj_tac \\ fs[]
- >- (Flover_compute ``validErrorbound``)
+ >- (
+ qpat_x_assum ‘validErrorbound _ _ _ _’
+ (fn thm => assume_tac (ONCE_REWRITE_RULE [validErrorbound_def] thm))
+ \\ fs[option_case_eq]
+ \\ pop_assum mp_tac \\ rpt (TOP_CASE_TAC \\ fs[]))
>- (rw_thm_asm `FPRangeValidator _ _ _ _` FPRangeValidator_def
\\ fs[] \\ rveq
\\ rw_asm_star `FloverMapTree_find (Fma _ _ _) A = _`
@@ -1045,7 +1072,11 @@ Proof
\\ rpt strip_tac \\ first_x_assum irule \\ simp[Once usedVars_def])
\\ first_x_assum (qspecl_then [`v2`, `A`, `fVars`, `dVars`] destruct)
>- (rpt conj_tac \\ fs[]
- >- (Flover_compute ``validErrorbound``)
+ >- (
+ qpat_x_assum ‘validErrorbound _ _ _ _’
+ (fn thm => assume_tac (ONCE_REWRITE_RULE [validErrorbound_def] thm))
+ \\ fs[option_case_eq]
+ \\ pop_assum mp_tac \\ rpt (TOP_CASE_TAC \\ fs[]))
>- (rw_thm_asm `FPRangeValidator _ _ _ _` FPRangeValidator_def
\\ fs[] \\ rveq
\\ rw_asm_star `FloverMapTree_find (Fma _ _ _) A = _`
@@ -1054,7 +1085,11 @@ Proof
\\ fs[domain_union, DIFF_DEF, SUBSET_DEF])
\\ first_x_assum (qspecl_then [`v3`, `A`, `fVars`, `dVars`] destruct)
>- (rpt conj_tac \\ fs[]
- >- (Flover_compute ``validErrorbound``)
+ >- (
+ qpat_x_assum ‘validErrorbound _ _ _ _’
+ (fn thm => assume_tac (ONCE_REWRITE_RULE [validErrorbound_def] thm))
+ \\ fs[option_case_eq]
+ \\ pop_assum mp_tac \\ rpt (TOP_CASE_TAC \\ fs[]))
>- (rw_thm_asm `FPRangeValidator _ _ _ _` FPRangeValidator_def
\\ fs[] \\ rveq
\\ rw_asm_star `FloverMapTree_find (Fma _ _ _) A = _`
@@ -1103,7 +1138,11 @@ Proof
\\ fs[] \\ rveq
\\ rw_asm_star `FloverMapTree_find (Fma _ _ _) A = _`
\\ rw_asm_star `FloverMapTree_find (Fma _ _ _) Gamma = _`)
- >- (Flover_compute ``validErrorbound``)
+ >- (
+ qpat_x_assum ‘validErrorbound _ _ _ _’
+ (fn thm => assume_tac (ONCE_REWRITE_RULE [validErrorbound_def] thm))
+ \\ fs[option_case_eq]
+ \\ pop_assum mp_tac \\ rpt (TOP_CASE_TAC \\ fs[]))
\\ irule eval_eq_env
\\ find_exists_tac \\ fs[])
\\ `validFloatValue (float_to_real (fp64_to_float vF2)) M64`
@@ -1121,7 +1160,11 @@ Proof
\\ fs[] \\ rveq
\\ rw_asm_star `FloverMapTree_find (Fma _ _ _) A = _`
\\ rw_asm_star `FloverMapTree_find (Fma _ _ _) Gamma = _`)
- >- (Flover_compute ``validErrorbound``)
+ >- (
+ qpat_x_assum ‘validErrorbound _ _ _ _’
+ (fn thm => assume_tac (ONCE_REWRITE_RULE [validErrorbound_def] thm))
+ \\ fs[option_case_eq]
+ \\ pop_assum mp_tac \\ rpt (TOP_CASE_TAC \\ fs[]))
\\ irule eval_eq_env
\\ find_exists_tac \\ fs[])
\\ `validFloatValue (float_to_real (fp64_to_float vF3)) M64`
@@ -1139,7 +1182,11 @@ Proof
\\ fs[] \\ rveq
\\ rw_asm_star `FloverMapTree_find (Fma _ _ _) A = _`
\\ rw_asm_star `FloverMapTree_find (Fma _ _ _) Gamma = _`)
- >- (Flover_compute ``validErrorbound``)
+ >- (
+ qpat_x_assum ‘validErrorbound _ _ _ _’
+ (fn thm => assume_tac (ONCE_REWRITE_RULE [validErrorbound_def] thm))
+ \\ fs[option_case_eq]
+ \\ pop_assum mp_tac \\ rpt (TOP_CASE_TAC \\ fs[]))
\\ irule eval_eq_env
\\ find_exists_tac \\ fs[])
\\ fs[optionLift_def, normal_or_zero_def]
@@ -1231,9 +1278,12 @@ Proof
\\ inversion `ssa _ _ _` ssa_cases
\\ once_rewrite_tac [bstep_float_def]
\\ fs[bstep_valid_def, noDowncast_def]
- \\ Flover_compute ``validErrorboundCmd``
- \\ fs[] \\ rveq \\ fs[]
- >- (`?v_e. eval_expr_float e E2 = SOME v_e /\
+ \\ qpat_x_assum ‘validErrorboundCmd _ _ _ _’
+ (fn thm => mp_tac (ONCE_REWRITE_RULE[validErrorboundCmd_def] thm))
+ \\ fs[option_case_eq]
+ >- (rpt (TOP_CASE_TAC \\ fs[])
+ \\ rpt strip_tac \\ rveq \\ fs[]
+ \\ `?v_e. eval_expr_float e E2 = SOME v_e /\
eval_expr (toREnv E2) (toRExpMap Gamma) (toRExp e)
(float_to_real (fp64_to_float v_e)) M64`
by (irule eval_expr_gives_IEEE \\ rpt conj_tac \\ fs[]
@@ -1241,7 +1291,6 @@ Proof
>- (find_exists_tac \\ fs[])
\\ qexistsl_tac [`A`, `E1`, `E2_real`, `dVars`, `fVars`]
\\ rpt conj_tac \\ fs[]
- \\ Flover_compute ``validErrorboundCmd``
>- (fs[Once freeVars_def, domain_union, DIFF_DEF, SUBSET_DEF]
\\ rpt strip_tac
\\ `x IN domain fVars \/ x IN domain dVars`
@@ -1254,8 +1303,8 @@ Proof
\\ fs[Once validTypesCmd_def]
(* prove validity of errorbound for floating-point value *)
\\ qspecl_then
- [`toRExp e`, `E1`, `E2_real`, `A`, `v'`, `err_e`,
- `FST iv_e`, `SND iv_e`, `fVars`, `dVars`, `Gamma`]
+ [`toRExp e`, `E1`, `E2_real`, `A`, `v'`, `r`,
+ `FST iv`, `SND iv`, `fVars`, `dVars`, `Gamma`]
impl_subgoal_tac
validErrorbound_sound
>- (fs[DIFF_DEF, SUBSET_DEF]
@@ -1263,10 +1312,13 @@ Proof
\\ fs[Once freeVars_def, domain_union]
\\ CCONTR_TAC \\ fs[] \\ rveq \\ fs[]
\\ `n IN domain fVars \/ n IN domain dVars`
- by (first_x_assum irule \\ fs[]))
+ by (first_x_assum irule \\ fs[]))
\\ fs[]
\\ IMP_RES_TAC meps_0_deterministic \\ rveq
- \\ rename1 `FST iv <= vR_e` \\ rename1 `FST iv_e <= vR_e`
+ \\ rename1 `FST iv <= vR_e`
+ \\ rename1 ‘FloverMapTree_find (getRetExp (Let M64 n (toRExp e) (toRCmd f))) A =
+ SOME (ivR,errR)’
+ \\ rename1 `FST iv_e <= vR_e`
\\ rename1 `abs (vR_e - nF) <= err_e`
\\ `abs (vR_e - (float_to_real (fp64_to_float v_e))) <= err_e`
by (first_x_assum irule \\ fs[]
@@ -1299,20 +1351,6 @@ Proof
\\ fs[Once freeVars_def]
\\ simp[Once freeVars_def, domain_union]))
\\ fs[optionLift_def]
- (* \\ `FloverMapTree_find (getRetExp (toRCmd f)) Gamma = SOME M64` *)
- (* by (irule typingSoundnessCmd *)
- (* \\ qexistsl_tac [`updEnv n v (toREnv E2)`, *)
- (* `updDefVars n M64 Gamma`, `fBits`, `vF`] *)
- (* \\ fs[] *)
- (* \\ rw_thm_asm `typeCheckCmd _ _ _` typeCheckCmd_def *)
- (* \\ EVERY_CASE_TAC \\ fs[]\\ rveq \\ fs[]) *)
- (* \\ `m' = M64` *)
- (* by (irule typing_agrees_cmd *)
- (* \\ rewrite_tac [CONJ_ASSOC] \\ once_rewrite_tac[CONJ_COMM] *)
- (* \\ rpt (asm_exists_tac \\ fs[]) *)
- (* \\ rw_thm_asm `typeCheckCmd _ _ _` typeCheckCmd_def *)
- (* \\ EVERY_CASE_TAC \\ fs[] \\ rveq \\ fs[]) *)
- (* \\ rveq \\ fs[bstep_cases, PULL_EXISTS] *)
(* Instantiate IH with newly obtained evaluation, to get the conclusion *)
\\ first_x_assum
(qspecl_then [`updEnv n vR_e E1`, `updFlEnv n v_e E2`,
@@ -1386,7 +1424,7 @@ Proof
\\ find_exists_tac \\ fs[]
\\ strip_tac \\ fs[toREnv_def, updEnv_def, updFlEnv_def]
\\ IF_CASES_TAC \\ fs[])
- >- (fs[bstep_cases] \\ drule eval_expr_gives_IEEE
+ >- (strip_tac \\ fs[bstep_cases] \\ drule eval_expr_gives_IEEE
\\ disch_then irule \\ rpt conj_tac
\\ fs[Once validTypesCmd_def]
>- (find_exists_tac \\ fs[])
@@ -1398,14 +1436,14 @@ QED
val found_tac = TRY (last_x_assum irule \\ find_exists_tac \\ fs[] \\ FAIL_TAC "")
\\ first_x_assum irule \\ find_exists_tac \\ fs[];
-val getValidMap_preserving = store_thm (
- "getValidMap_preserving",
- ``! e defVars akk res.
- (! e m. FloverMapTree_find e akk = SOME m ==> m = M64) /\
- is64BitEval e /\
- getValidMap defVars e akk = Succes res /\
- (! e m. FloverMapTree_find e defVars = SOME m ==> m = M64) ==>
- ! e m. FloverMapTree_find e res = SOME m ==> m = M64``,
+Theorem getValidMap_preserving:
+ ∀ e defVars akk res.
+ (∀ e m. FloverMapTree_find e akk = SOME m ==> m = M64) /\
+ is64BitEval e /\
+ getValidMap defVars e akk = Succes res /\
+ (∀ e m. FloverMapTree_find e defVars = SOME m ==> m = M64) ==>
+ ∀ e m. FloverMapTree_find e res = SOME m ==> m = M64
+Proof
Induct_on `e` \\ once_rewrite_tac[getValidMap_def] \\ rpt strip_tac
>- (fs[] \\ Cases_on `FloverMapTree_mem (Var n) akk` \\ fs[]
>- (rveq \\ found_tac)
@@ -1468,8 +1506,11 @@ val getValidMap_preserving = store_thm (
\\ Cases_on `e'' = Binop b e1 e2` \\ fs[]
>- (rveq \\ metis_tac[])
\\ metis_tac[])
+ \\ TOP_CASE_TAC \\ fs[]
+ >- (TOP_CASE_TAC \\ fs[] \\ res_tac \\ fs[])
+ >- (TOP_CASE_TAC \\ fs[] \\ res_tac \\ fs[])
\\ rpt strip_tac \\ qpat_x_assum `_ = Succes res` mp_tac
- \\ TOP_CASE_TAC \\ fs[addMono_def, option_case_eq]
+ \\ ntac 2 (TOP_CASE_TAC \\ fs[addMono_def, option_case_eq])
\\ rpt strip_tac \\ rveq \\ fs[map_find_add]
\\ Cases_on `e'' = Binop b e1 e2` \\ fs[]
>- (rveq
@@ -1505,8 +1546,11 @@ val getValidMap_preserving = store_thm (
\\ Cases_on `e''' = Fma e1 e2 e3` \\ fs[]
>- (rveq \\ metis_tac[])
\\ metis_tac[])
- \\ rpt strip_tac \\ qpat_x_assum `_ = Succes res` mp_tac
- \\ TOP_CASE_TAC \\ fs[addMono_def, option_case_eq]
+ \\ TOP_CASE_TAC \\ fs[]
+ >- (TOP_CASE_TAC \\ fs[] \\ res_tac \\ fs[])
+ >- (TOP_CASE_TAC \\ fs[] \\ res_tac \\ fs[])
+ >- (TOP_CASE_TAC \\ fs[] \\ res_tac \\ fs[])
+ \\ ntac 2 (TOP_CASE_TAC \\ fs[option_case_eq, addMono_def])
\\ rpt strip_tac \\ rveq \\ fs[map_find_add]
\\ Cases_on `e''' = Fma e1 e2 e3` \\ fs[]
>- (rveq
@@ -1530,7 +1574,8 @@ val getValidMap_preserving = store_thm (
\\ TOP_CASE_TAC \\ fs[addMono_def, option_case_eq]
\\ strip_tac \\ rveq \\ fs[map_find_add]
\\ Cases_on `e' = Downcast M64 e` \\ fs[] \\ rveq
- \\ res_tac);
+ \\ res_tac
+QED
val getValidMapCmd_preserving = store_thm (
"getValidMapCmd_preserving",
diff --git a/hol4/Infra/MachineTypeScript.sml b/hol4/Infra/MachineTypeScript.sml
index 1e1399a7..03eb5d92 100644
--- a/hol4/Infra/MachineTypeScript.sml
+++ b/hol4/Infra/MachineTypeScript.sml
@@ -33,6 +33,45 @@ Definition mTypeToR_def:
| F w f => 1 / (2 pow f)
End
+Definition maxExponent_def:
+ (maxExponent (REAL) = 0n) /\
+ (maxExponent (M16) = 15) /\
+ (maxExponent (M32) = 127) /\
+ (maxExponent (M64) = 1023) /\
+ (maxExponent (F w f) = f)
+End
+
+Definition minExponentPos_def:
+ (minExponentPos (REAL) = 0n) /\
+ (minExponentPos (M16) = 14) /\
+ (minExponentPos (M32) = 126) /\
+ (minExponentPos (M64) = 1022) /\
+ (minExponentPos (F w f) = f)
+End
+
+(**
+Goldberg - Handbook of Floating-Point Arithmetic: (p.183)
+(𛃠- ð›ƒ^(1 - p)) * ð›ƒ^(e_max)
+which simplifies to 2^(e_max) for base 2
+**)
+
+Definition maxValue_def:
+ maxValue (m:mType) =
+ case m of
+ | F w f => &((2n ** (w-1)) - 1) * inv &(2n ** (maxExponent m))
+ | _ => (&(2n ** (maxExponent m))):real
+End
+
+(** Using the sign bit, the very same number is representable as a negative number,
+ thus just apply negation here **)
+Definition minValue_pos_def:
+ minValue_pos (m:mType) =
+ case m of
+ | F w f => 0
+ | _ => inv (&(2n ** (minExponentPos m)))
+End
+
+
Definition computeError_def:
computeError v m =
case m of
@@ -61,6 +100,15 @@ Proof
\\ fs[ABS_LE]
QED
+Theorem computeError_pos:
+ 0 ≤ computeError v m
+Proof
+ fs[computeError_def]
+ \\ Cases_on ‘m’ \\ fs[mTypeToR_def]
+ \\ irule REAL_LE_ADD \\ fs[maxAbs_def, max_def]
+ \\ TOP_CASE_TAC \\ fs[minValue_pos_def]
+QED
+
(**
Check if machine precision m1 is more precise than machine precision m2.
REAL is real-valued evaluation, hence the most precise.
@@ -187,44 +235,6 @@ Definition isJoin3_def:
|SOME mNew => mNew = mj)
End
-Definition maxExponent_def:
- (maxExponent (REAL) = 0n) /\
- (maxExponent (M16) = 15) /\
- (maxExponent (M32) = 127) /\
- (maxExponent (M64) = 1023) /\
- (maxExponent (F w f) = f)
-End
-
-Definition minExponentPos_def:
- (minExponentPos (REAL) = 0n) /\
- (minExponentPos (M16) = 14) /\
- (minExponentPos (M32) = 126) /\
- (minExponentPos (M64) = 1022) /\
- (minExponentPos (F w f) = f)
-End
-
-(**
-Goldberg - Handbook of Floating-Point Arithmetic: (p.183)
-(𛃠- ð›ƒ^(1 - p)) * ð›ƒ^(e_max)
-which simplifies to 2^(e_max) for base 2
-**)
-
-Definition maxValue_def:
- maxValue (m:mType) =
- case m of
- | F w f => &((2n ** (w-1)) - 1) * inv &(2n ** (maxExponent m))
- | _ => (&(2n ** (maxExponent m))):real
-End
-
-(** Using the sign bit, the very same number is representable as a negative number,
- thus just apply negation here **)
-Definition minValue_pos_def:
- minValue_pos (m:mType) =
- case m of
- | F w f => 0
- | _ => inv (&(2n ** (minExponentPos m)))
-End
-
(** Goldberg - Handbook of Floating-Point Arithmetic: (p.183)
ð›ƒ^(e_min -p + 1) = ð›ƒ^(e_min -1) for base 2
**)
diff --git a/hol4/IntervalValidationScript.sml b/hol4/IntervalValidationScript.sml
index 0ec743fd..1dc849bd 100644
--- a/hol4/IntervalValidationScript.sml
+++ b/hol4/IntervalValidationScript.sml
@@ -122,6 +122,11 @@ val real_prove =
\\ rpt (qpat_x_assum `_ ==> ! x. _` kall_tac)
\\ REAL_ASM_ARITH_TAC;
+val _ = add_unevaluated_function “addIntervalâ€
+val _ = add_unevaluated_function “subtractIntervalâ€
+val _ = add_unevaluated_function “multIntervalâ€
+val _ = add_unevaluated_function “divideIntervalâ€
+
Theorem validIntervalbounds_sound:
!(f:real expr) (A:analysisResult) (P:precond) (fVars:num_set)
(dVars:num_set) E Gamma.
diff --git a/hol4/TypeValidatorScript.sml b/hol4/TypeValidatorScript.sml
index a42f5903..4ac6f681 100644
--- a/hol4/TypeValidatorScript.sml
+++ b/hol4/TypeValidatorScript.sml
@@ -6,54 +6,56 @@ open preambleFloVer;
val _ = new_theory "TypeValidator";
-val validTypes_def = Define `
+Definition validTypes_def:
validTypes e Gamma =
- ? mG. FloverMapTree_find e Gamma = SOME mG /\
+ ∃ mG. FloverMapTree_find e Gamma = SOME mG ∧
(case e of
| Var x => T
| Const m v => m = mG
| Unop u e1 =>
- validTypes e1 Gamma /\
- (? me. FloverMapTree_find e1 Gamma = SOME me /\ isCompat me mG)
+ validTypes e1 Gamma ∧
+ (? me. FloverMapTree_find e1 Gamma = SOME me ∧ isCompat me mG)
| Binop b e1 e2 =>
- validTypes e1 Gamma /\
- validTypes e2 Gamma /\
- (?m1 m2. FloverMapTree_find e1 Gamma = SOME m1 /\
- FloverMapTree_find e2 Gamma = SOME m2 /\
+ validTypes e1 Gamma ∧
+ validTypes e2 Gamma ∧
+ (?m1 m2. FloverMapTree_find e1 Gamma = SOME m1 ∧
+ FloverMapTree_find e2 Gamma = SOME m2 ∧
isJoin m1 m2 mG)
| Fma e1 e2 e3 =>
- validTypes e1 Gamma /\
- validTypes e2 Gamma /\
- validTypes e3 Gamma /\
- (?m1 m2 m3. FloverMapTree_find e1 Gamma = SOME m1 /\
- FloverMapTree_find e2 Gamma = SOME m2 /\
- FloverMapTree_find e3 Gamma = SOME m3 /\
+ validTypes e1 Gamma ∧
+ validTypes e2 Gamma ∧
+ validTypes e3 Gamma ∧
+ (?m1 m2 m3. FloverMapTree_find e1 Gamma = SOME m1 ∧
+ FloverMapTree_find e2 Gamma = SOME m2 ∧
+ FloverMapTree_find e3 Gamma = SOME m3 ∧
isJoin3 m1 m2 m3 mG)
| Downcast m e1 =>
- validTypes e1 Gamma /\
- m = mG /\
- (? m1. FloverMapTree_find e1 Gamma = SOME m1 /\
- isMorePrecise m1 mG)) /\
+ validTypes e1 Gamma ∧
+ m = mG ∧
+ (? m1. FloverMapTree_find e1 Gamma = SOME m1 ∧
+ isMorePrecise m1 mG)) ∧
(! E Gamma2 v m.
(! e m. FloverMapTree_find e Gamma = SOME m ==>
- FloverMapTree_find e Gamma2 = SOME m) /\
+ FloverMapTree_find e Gamma2 = SOME m) ∧
eval_expr E (toRExpMap Gamma2) e v m ==>
- m = mG)`;
+ m = mG)
+End
-val validTypes_single = store_thm (
- "validTypes_single",
- ``!e Gamma.
- validTypes e Gamma ==>
- ?mG.
- FloverMapTree_find e Gamma = SOME mG /\
- (!E v m Gamma2.
- (! e m. FloverMapTree_find e Gamma = SOME m ==>
- FloverMapTree_find e Gamma2 = SOME m) /\
- eval_expr E (toRExpMap Gamma2) e v m ==>
- m = mG)``,
+Theorem validTypes_single:
+ ∀ e Gamma.
+ validTypes e Gamma ==>
+ ∃ mG.
+ FloverMapTree_find e Gamma = SOME mG /\
+ (!E v m Gamma2.
+ (! e m. FloverMapTree_find e Gamma = SOME m ==>
+ FloverMapTree_find e Gamma2 = SOME m) /\
+ eval_expr E (toRExpMap Gamma2) e v m ==>
+ m = mG)
+Proof
Cases_on `e` \\ rpt strip_tac \\ fs[Once validTypes_def] \\ rpt strip_tac
\\ first_x_assum irule \\ fs[]
- \\ rpt (asm_exists_tac \\ fs[]));
+ \\ rpt (asm_exists_tac \\ fs[])
+QED
val validTypes_exec = store_thm (
"validTypes_exec",
@@ -82,7 +84,7 @@ val addMono_def = Define `
val _ = Parse.temp_overload_on ("insert", Term`FloverMapTree_insert`);
-val getValidMap_def = Define `
+Definition getValidMap_def:
getValidMap Gamma e akk =
if (FloverMapTree_mem e akk)
then Succes akk
@@ -133,6 +135,13 @@ val getValidMap_def = Define `
then addMono e mj akk2_map
else Fail "Incorrect fixed-point type"
else
+ if (t1 = REAL ∨ t2 = REAL)
+ then if (t1 = REAL ∧ t2 = REAL)
+ then if (isMonotone mOldO REAL)
+ then addMono e REAL akk2_map
+ else Fail "Wrong type annotation for binary operator"
+ else Fail "Both arguments must be REAL if one is REAL"
+ else
(case join_fl t1 t2 of
| NONE => Fail "Could not compute join for arguments"
| SOME m =>
@@ -159,7 +168,13 @@ val getValidMap_def = Define `
if (morePrecise t1 mj /\ morePrecise t2 mj /\ morePrecise t3 mj)
then addMono e mj akk3_map
else Fail "Incorrect fixed-point type"
- else
+ else if (t1 = REAL ∨ t2 = REAL ∨ t3 = REAL)
+ then if (t1 = REAL ∧ t2 = REAL ∧ t3 = REAL)
+ then if (isMonotone mOldO REAL)
+ then addMono e REAL akk3_map
+ else Fail "Wrong type annotation for binary operator"
+ else Fail "Both arguments must be REAL if one is REAL"
+ else
(case join_fl3 t1 t2 t3 of
| NONE => Fail "Could not compute join for arguments"
| SOME m =>
@@ -186,7 +201,8 @@ val getValidMap_def = Define `
if (morePrecise t1 m /\ isMonotone mOldO m)
then addMono e m akk_new
else Fail "Cannot cast down to lower precision"
- od`;
+ od
+End
add_unevaluated_function ``getValidMap``;
@@ -205,12 +221,12 @@ val by_monotonicity =
\\ fs[FloverMapTree_mem_def]
\\ EVERY_CASE_TAC \\ fs[];
-val getValidMap_mono = store_thm (
- "getValidMap_mono",
- ``! e Gamma akk res.
- getValidMap Gamma e akk = Succes res ==>
- ! e m. FloverMapTree_find e akk = SOME m ==>
- FloverMapTree_find e res = SOME m``,
+Theorem getValidMap_mono:
+ ∀ e Gamma akk res.
+ getValidMap Gamma e akk = Succes res ⇒
+ ∀ e m. FloverMapTree_find e akk = SOME m ⇒
+ FloverMapTree_find e res = SOME m
+Proof
Induct_on `e`
\\ once_rewrite_tac [getValidMap_def] \\ fs[]
\\ rpt strip_tac
@@ -242,8 +258,14 @@ val getValidMap_mono = store_thm (
\\ fs[addMono_def, option_case_eq]
\\ rveq \\ res_tac
\\ by_monotonicity)
- \\ rename1 `join_fl t1 t2 = SOME mj`
- \\ Cases_on `isMonotone (FloverMapTree_find (Binop b e1 e2) Gamma) mj`
+ \\ Cases_on ‘t1 = REAL ∨ t2 = REAL’ \\ fs[]
+ \\ TRY (rename1 ‘t1 = REAL ∧ t2 = REAL’ \\ Cases_on ‘t1 = REAL ∧ t2 = REAL’ \\ fs[] \\ fs[])
+ \\ TRY (fs[option_case_eq] \\ rename1 `join_fl t1 t2 = SOME mj`
+ \\ Cases_on `isMonotone (FloverMapTree_find (Binop b e1 e2) Gamma) mj`
+ \\ fs[addMono_def, option_case_eq] \\ rveq \\ res_tac
+ \\ by_monotonicity)
+ \\ rveq \\ fs[]
+ \\ Cases_on `isMonotone (FloverMapTree_find (Binop b e1 e2) Gamma) REAL`
\\ fs[addMono_def, option_case_eq] \\ rveq \\ res_tac
\\ by_monotonicity)
>- (rename1 `Fma e1 e2 e3` \\ Cases_on `FloverMapTree_mem (Fma e1 e2 e3) akk`
@@ -261,8 +283,16 @@ val getValidMap_mono = store_thm (
\\ fs[addMono_def, option_case_eq]
\\ rveq \\ res_tac
\\ by_monotonicity)
- \\ rename1 `join_fl3 t1 t2 t3 = SOME mj`
- \\ Cases_on `isMonotone (FloverMapTree_find (Fma e1 e2 e3) Gamma) mj`
+ \\ Cases_on ‘t1 = REAL ∨ t2 = REAL ∨ t3 = REAL’ \\ fs[]
+ \\ TRY (rename1 ‘t1 = REAL ∧ t2 = REAL ∧ t3 = REAL’
+ \\ Cases_on ‘t1 = REAL ∧ t2 = REAL ∧ t3 = REAL’ \\ fs[] \\ fs[])
+ \\ TRY (fs[option_case_eq]
+ \\ rename1 `join_fl3 t1 t2 t3 = SOME mj`
+ \\ Cases_on `isMonotone (FloverMapTree_find (Fma e1 e2 e3) Gamma) mj`
+ \\ fs[addMono_def, option_case_eq] \\ rveq \\ res_tac
+ \\ by_monotonicity)
+ \\ rveq \\ fs[]
+ \\ Cases_on `isMonotone (FloverMapTree_find (Fma e1 e2 e3) Gamma) REAL`
\\ fs[addMono_def, option_case_eq] \\ rveq \\ res_tac
\\ by_monotonicity)
\\ Cases_on `FloverMapTree_mem (Downcast m e) akk`
@@ -277,7 +307,8 @@ val getValidMap_mono = store_thm (
\\ Cases_on `isMonotone (FloverMapTree_find (Downcast m e) Gamma) m`
\\ fs[addMono_def, option_case_eq] \\ rveq
\\ res_tac
- \\ by_monotonicity);
+ \\ by_monotonicity
+QED
val validTypes_mono = store_thm (
"validTypes_mono",
@@ -338,15 +369,16 @@ val map_find_mono = store_thm (
rpt strip_tac \\ fs[map_find_add]
\\ Cases_on `e1 = e2` \\ fs[FloverMapTree_mem_def]);
-val getValidMap_correct = store_thm (
- "getValidMap_correct",
- ``! e Gamma akk res.
- (! e.
- FloverMapTree_mem e akk ==>
- validTypes e akk) /\
- getValidMap Gamma e akk = Succes res ==>
- ! e. FloverMapTree_mem e res ==>
- validTypes e res``,
+Theorem getValidMap_correct:
+ ∀ e Gamma akk res.
+ (∀ e.
+ FloverMapTree_mem e akk ⇒
+ validTypes e akk) ∧
+ getValidMap Gamma e akk = Succes res ⇒
+ ∀ e.
+ FloverMapTree_mem e res ⇒
+ validTypes e res
+Proof
Induct_on `e` \\ simp[Once getValidMap_def] \\ rpt strip_tac
>- (Cases_on `FloverMapTree_mem (Var n) akk`
\\ fs[] \\ rveq \\ fs[option_case_eq]
@@ -436,14 +468,14 @@ val getValidMap_correct = store_thm (
\\ rename1 `getValidMap Gamma e2 a = Succes map2`
\\ Cases_on `FloverMapTree_find e1 map2` \\ fs[]
\\ Cases_on `FloverMapTree_find e2 map2` \\ fs[]
- \\ `! e. FloverMapTree_mem e a ==> validTypes e a`
+ \\ ‘∀ e. FloverMapTree_mem e a ⇒ validTypes e a’
by (rpt strip_tac \\ last_x_assum irule \\ fs[]
\\ qexistsl_tac [`Gamma`, `akk`] \\ fs[])
- \\ `! e. FloverMapTree_mem e map2 ==> validTypes e map2`
+ \\ ‘∀ e. FloverMapTree_mem e map2 ⇒ validTypes e map2’
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 x mj` \\ Cases_on `morePrecise x' mj`
+ \\ Cases_on ‘isFixedPoint x ∧ isFixedPoint 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[]
@@ -462,21 +494,30 @@ val getValidMap_correct = store_thm (
\\ qexists_tac `map2` \\ fs[]
\\ rpt strip_tac \\ fs[map_find_add]
\\ COND_CASES_TAC \\ fs[])
- >- (fs[no_cycle_binop_left, no_cycle_binop_right, isJoin_def])
+ >- (fs[no_cycle_binop_left, no_cycle_binop_right, isJoin_def]
+ \\ Cases_on ‘x’ \\ Cases_on ‘x'’ \\ fs[isFixedPoint_def]
+ \\ fs[join_fl_def]
+ \\ Cases_on ‘mj’ \\ fs[morePrecise_def])
\\ rpt strip_tac
\\ first_x_assum (qspecl_then [`Binop b e1 e2`, `mj`] assume_tac)
\\ fs[eval_expr_cases, toRExpMap_def] \\ rveq \\ fs[])
- \\ fs[option_case_eq]
- \\ Cases_on `isMonotone (FloverMapTree_find (Binop b e1 e2) Gamma) m`
+ \\ pop_assum (fn thm => fs[thm, option_case_eq])
+ \\ rename1 ‘m1 = REAL ∨ m2 = REAL’
+ \\ Cases_on ‘m1 = REAL ∨ m2 = REAL’ \\ fs[] \\ fs[]
+ \\ TRY (rename1 ‘(if m2 = REAL then _ else _) = _’ \\ Cases_on ‘m2 = REAL’ \\ fs[]
+ \\ Cases_on `isMonotone (FloverMapTree_find (Binop b e1 e2) Gamma) REAL`)
+ ORELSE (TRY (rename1 ‘(if m1 = REAL then _ else _) = _’ \\ Cases_on ‘m1 = REAL’ \\ fs[]
+ \\ Cases_on `isMonotone (FloverMapTree_find (Binop b e1 e2) Gamma) REAL`))
+ ORELSE (Cases_on `isMonotone (FloverMapTree_find (Binop b e1 e2) Gamma) m`)
\\ fs[addMono_def, option_case_eq]
\\ rveq \\ fs[FloverMapTree_mem_def, map_find_add]
\\ reverse (Cases_on `e'' = Binop b e1 e2`) \\ fs[]
- >- (irule validTypes_mono
+ \\ TRY (irule validTypes_mono
\\ qexists_tac `map2` \\ fs[]
\\ rpt strip_tac \\ fs[map_find_add]
- \\ COND_CASES_TAC \\ fs[])
+ \\ COND_CASES_TAC \\ fs[] \\ FAIL_TAC "NOT FINISHED")
>- (rveq \\ once_rewrite_tac[validTypes_def]
- \\ qexists_tac `m` \\ fs[map_find_add]
+ \\ qexists_tac `REAL` \\ fs[map_find_add]
\\ rpt conj_tac
>- (irule validTypes_mono
\\ qexists_tac `map2` \\ fs[]
@@ -486,17 +527,44 @@ val getValidMap_correct = store_thm (
\\ qexists_tac `map2` \\ fs[]
\\ rpt strip_tac \\ fs[map_find_add]
\\ COND_CASES_TAC \\ fs[])
- >- (fs[no_cycle_binop_left, no_cycle_binop_right, isJoin_def])
- \\ rpt strip_tac
- \\ first_x_assum (qspecl_then [`Binop b e1 e2`, `m`] assume_tac)
- \\ fs[eval_expr_cases, toRExpMap_def] \\ rveq \\ fs[])
- >- (irule validTypes_mono
- \\ qexists_tac `map2` \\ fs[]
+ >- fs[isJoin_def, isFixedPoint_def, join_fl_def]
+ \\ rpt strip_tac \\ fs[eval_expr_cases, toRExpMap_def]
+ \\ first_x_assum (qspecl_then [‘Binop b e1 e2’, ‘REAL’] assume_tac) \\ fs[])
+ >- (Cases_on ‘FloverMapTree_find (Binop b e1 e2) akk’ \\ fs[]
+ \\ Cases_on ‘m1 = REAL’ \\ fs[]
+ \\ Cases_on ‘isMonotone (FloverMapTree_find (Binop b e1 e2) Gamma) REAL’
+ \\ fs[option_case_eq] \\ rveq
+ \\ irule validTypes_mono \\ qexists_tac ‘map2’ \\ fs[]
\\ rpt strip_tac \\ fs[map_find_add]
- \\ COND_CASES_TAC \\ fs[])
+ \\ TOP_CASE_TAC \\ fs[])
+ >- (rveq
+ \\ Cases_on ‘FloverMapTree_find (Binop b e1 e2) akk’ \\ fs[]
+ \\ Cases_on ‘m1 = REAL’ \\ fs[]
+ \\ Cases_on ‘isMonotone (FloverMapTree_find (Binop b e1 e2) Gamma) REAL’
+ \\ fs[option_case_eq] \\ rveq
+ \\ once_rewrite_tac[validTypes_def]
+ \\ qexists_tac `REAL` \\ fs[map_find_add]
+ \\ rpt conj_tac
+ >- (irule validTypes_mono
+ \\ qexists_tac `map2` \\ fs[]
+ \\ rpt strip_tac \\ fs[map_find_add]
+ \\ COND_CASES_TAC \\ fs[])
+ >- (irule validTypes_mono
+ \\ qexists_tac `map2` \\ fs[]
+ \\ rpt strip_tac \\ fs[map_find_add]
+ \\ COND_CASES_TAC \\ fs[])
+ >- fs[isJoin_def, isFixedPoint_def, join_fl_def]
+ \\ rpt strip_tac \\ fs[eval_expr_cases, toRExpMap_def]
+ \\ first_x_assum (qspecl_then [‘Binop b e1 e2’, ‘REAL’] assume_tac) \\ fs[])
+ >- (Cases_on ‘isMonotone (FloverMapTree_find (Binop b e1 e2) Gamma) m’
+ \\ fs[option_case_eq] \\ rveq
+ \\ irule validTypes_mono \\ qexists_tac ‘map2’ \\ fs[map_find_add]
+ \\ rpt strip_tac \\ TOP_CASE_TAC \\ fs[])
+ \\ rveq \\ fs[]
+ \\ Cases_on ‘isMonotone (FloverMapTree_find (Binop b e1 e2) Gamma) m’
+ \\ fs[option_case_eq] \\ rveq
\\ rveq \\ once_rewrite_tac[validTypes_def]
- \\ qexists_tac `m` \\ fs[map_find_add]
- \\ rpt conj_tac
+ \\ qexists_tac ‘m’ \\ fs[] \\ rpt conj_tac \\ fs[map_find_add]
>- (irule validTypes_mono
\\ qexists_tac `map2` \\ fs[]
\\ rpt strip_tac \\ fs[map_find_add]
@@ -505,7 +573,9 @@ val getValidMap_correct = store_thm (
\\ qexists_tac `map2` \\ fs[]
\\ rpt strip_tac \\ fs[map_find_add]
\\ COND_CASES_TAC \\ fs[])
- >- (fs[no_cycle_binop_left, no_cycle_binop_right, isJoin_def])
+ >- (fs[no_cycle_binop_left, no_cycle_binop_right, isJoin_def]
+ \\ Cases_on ‘m1’ \\ Cases_on ‘m2’ \\ fs[join_fl_def, morePrecise_def]
+ \\ rveq \\ EVAL_TAC)
\\ rpt strip_tac
\\ first_x_assum (qspecl_then [`Binop b e1 e2`, `m`] assume_tac)
\\ fs[eval_expr_cases, toRExpMap_def] \\ rveq \\ fs[])
@@ -533,8 +603,8 @@ val getValidMap_correct = store_thm (
by (rpt strip_tac \\ first_x_assum irule \\ fs[]
\\ qexistsl_tac [`Gamma`, `map2`] \\ fs[])
\\ Cases_on `isFixedPoint x /\ isFixedPoint x' /\ isFixedPoint x''`
- \\ fs[option_case_eq]
- >- (Cases_on `morePrecise x mj` \\ Cases_on `morePrecise x' mj`
+ >- (fs[option_case_eq]
+ \\ 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]
@@ -560,12 +630,25 @@ val getValidMap_correct = store_thm (
\\ rpt strip_tac \\ fs[map_find_add]
\\ COND_CASES_TAC \\ fs[])
>- (fs[no_cycle_fma_left, no_cycle_fma_center, no_cycle_fma_right,
- isJoin3_def])
+ isJoin3_def]
+ \\ Cases_on ‘x’ \\ Cases_on ‘x'’ \\ Cases_on ‘x''’ \\ fs[isFixedPoint_def]
+ \\ Cases_on ‘mj’ \\ fs[morePrecise_def])
\\ rpt strip_tac
\\ first_x_assum (qspecl_then [`Fma e1 e2 e3`, `mj`] assume_tac)
\\ fs[eval_expr_cases, toRExpMap_def] \\ rveq \\ fs[])
- \\ fs[option_case_eq]
- \\ Cases_on `isMonotone (FloverMapTree_find (Fma e1 e2 e3) Gamma) m`
+ \\ pop_assum (fn thm => fs[thm, option_case_eq])
+ \\ rename1 ‘m1 = REAL ∨ m2 = REAL ∨ m3 = REAL’
+ \\ Cases_on ‘m1 = REAL ∨ m2 = REAL ∨ m3 = REAL’ \\ fs[] \\ fs[]
+ \\ ((rename1 ‘(if m2 = REAL ∧ m3 = REAL then _ else _) = _’
+ \\ Cases_on ‘m2 = REAL ∧ m3 = REAL’ \\ fs[]
+ \\ Cases_on `isMonotone (FloverMapTree_find (Fma e1 e2 e3) Gamma) REAL`)
+ ORELSE (rename1 ‘(if m1 = REAL ∧ m3 = REAL then _ else _) = _’
+ \\ Cases_on ‘m1 = REAL ∧ m3 = REAL’ \\ fs[]
+ \\ Cases_on `isMonotone (FloverMapTree_find (Fma e1 e2 e3) Gamma) REAL`)
+ ORELSE (rename1 ‘(if m1 = REAL ∧ m2 = REAL then _ else _) = _’
+ \\ Cases_on ‘m1 = REAL ∧ m2 = REAL’ \\ fs[]
+ \\ Cases_on `isMonotone (FloverMapTree_find (Fma e1 e2 e3) Gamma) REAL`)
+ ORELSE (fs[option_case_eq] \\ Cases_on `isMonotone (FloverMapTree_find (Fma e1 e2 e3) Gamma) m`))
\\ fs[addMono_def, option_case_eq]
\\ rveq \\ fs[FloverMapTree_mem_def, map_find_add]
\\ rename1 `eNew = Fma e1 e2 e3`
@@ -575,7 +658,7 @@ val getValidMap_correct = store_thm (
\\ rpt strip_tac \\ fs[map_find_add]
\\ COND_CASES_TAC \\ fs[])
>- (rveq \\ once_rewrite_tac[validTypes_def]
- \\ qexists_tac `m` \\ fs[map_find_add]
+ \\ qexists_tac `REAL` \\ fs[map_find_add]
\\ rpt conj_tac
>- (irule validTypes_mono
\\ qexists_tac `map3` \\ fs[]
@@ -589,17 +672,16 @@ val getValidMap_correct = store_thm (
\\ qexists_tac `map3` \\ fs[]
\\ rpt strip_tac \\ fs[map_find_add]
\\ COND_CASES_TAC \\ fs[])
- >- (fs[no_cycle_fma_left, no_cycle_fma_center, no_cycle_fma_right,
- isJoin3_def])
+ >- EVAL_TAC
\\ rpt strip_tac
- \\ first_x_assum (qspecl_then [`Fma e1 e2 e3`, `m`] assume_tac)
+ \\ first_x_assum (qspecl_then [`Fma e1 e2 e3`, `REAL`] assume_tac)
\\ fs[eval_expr_cases, toRExpMap_def] \\ rveq \\ fs[])
>- (irule validTypes_mono
\\ qexists_tac `map3` \\ fs[]
\\ rpt strip_tac \\ fs[map_find_add]
\\ COND_CASES_TAC \\ fs[])
>- (rveq \\ once_rewrite_tac[validTypes_def]
- \\ qexists_tac `m` \\ fs[map_find_add]
+ \\ qexists_tac `REAL` \\ fs[map_find_add]
\\ rpt conj_tac
>- (irule validTypes_mono
\\ qexists_tac `map3` \\ fs[]
@@ -613,35 +695,60 @@ val getValidMap_correct = store_thm (
\\ qexists_tac `map3` \\ fs[]
\\ rpt strip_tac \\ fs[map_find_add]
\\ COND_CASES_TAC \\ fs[])
- >- (fs[no_cycle_fma_left, no_cycle_fma_center, no_cycle_fma_right,
- isJoin3_def])
+ >- EVAL_TAC
\\ rpt strip_tac
- \\ first_x_assum (qspecl_then [`Fma e1 e2 e3`, `m`] assume_tac)
+ \\ first_x_assum (qspecl_then [`Fma e1 e2 e3`, `REAL`] assume_tac)
\\ fs[eval_expr_cases, toRExpMap_def] \\ rveq \\ fs[])
>- (irule validTypes_mono
\\ qexists_tac `map3` \\ fs[]
\\ rpt strip_tac \\ fs[map_find_add]
\\ COND_CASES_TAC \\ fs[])
- \\ rveq \\ once_rewrite_tac[validTypes_def]
- \\ qexists_tac `m` \\ fs[map_find_add]
- \\ rpt conj_tac
- >- (irule validTypes_mono
- \\ qexists_tac `map3` \\ fs[]
- \\ rpt strip_tac \\ fs[map_find_add]
- \\ COND_CASES_TAC \\ fs[])
- >- (irule validTypes_mono
- \\ qexists_tac `map3` \\ fs[]
- \\ rpt strip_tac \\ fs[map_find_add]
- \\ COND_CASES_TAC \\ fs[])
- >- (irule validTypes_mono
- \\ qexists_tac `map3` \\ fs[]
- \\ rpt strip_tac \\ fs[map_find_add]
- \\ COND_CASES_TAC \\ fs[])
- >- (fs[no_cycle_fma_left, no_cycle_fma_center, no_cycle_fma_right,
- isJoin3_def])
- \\ rpt strip_tac
- \\ first_x_assum (qspecl_then [`Fma e1 e2 e3`, `m`] assume_tac)
- \\ fs[eval_expr_cases, toRExpMap_def] \\ rveq \\ fs[])
+ >- (rveq \\ once_rewrite_tac[validTypes_def]
+ \\ qexists_tac `REAL` \\ fs[map_find_add]
+ \\ rpt conj_tac
+ >- (irule validTypes_mono
+ \\ qexists_tac `map3` \\ fs[]
+ \\ rpt strip_tac \\ fs[map_find_add]
+ \\ COND_CASES_TAC \\ fs[])
+ >- (irule validTypes_mono
+ \\ qexists_tac `map3` \\ fs[]
+ \\ rpt strip_tac \\ fs[map_find_add]
+ \\ COND_CASES_TAC \\ fs[])
+ >- (irule validTypes_mono
+ \\ qexists_tac `map3` \\ fs[]
+ \\ rpt strip_tac \\ fs[map_find_add]
+ \\ COND_CASES_TAC \\ fs[])
+ >- EVAL_TAC
+ \\ rpt strip_tac
+ \\ first_x_assum (qspecl_then [`Fma e1 e2 e3`, `REAL`] assume_tac)
+ \\ fs[eval_expr_cases, toRExpMap_def] \\ rveq \\ fs[])
+ >- (irule validTypes_mono
+ \\ qexists_tac `map3` \\ fs[]
+ \\ rpt strip_tac \\ fs[map_find_add]
+ \\ COND_CASES_TAC \\ fs[])
+ >- (rveq \\ once_rewrite_tac[validTypes_def]
+ \\ qexists_tac `m` \\ fs[map_find_add]
+ \\ rpt conj_tac
+ >- (irule validTypes_mono
+ \\ qexists_tac `map3` \\ fs[]
+ \\ rpt strip_tac \\ fs[map_find_add]
+ \\ COND_CASES_TAC \\ fs[])
+ >- (irule validTypes_mono
+ \\ qexists_tac `map3` \\ fs[]
+ \\ rpt strip_tac \\ fs[map_find_add]
+ \\ COND_CASES_TAC \\ fs[])
+ >- (irule validTypes_mono
+ \\ qexists_tac `map3` \\ fs[]
+ \\ rpt strip_tac \\ fs[map_find_add]
+ \\ COND_CASES_TAC \\ fs[])
+ >- (fs[no_cycle_fma_left, no_cycle_fma_center, no_cycle_fma_right,
+ isJoin3_def]
+ \\ Cases_on ‘m1’ \\ Cases_on ‘m2’ \\ Cases_on ‘m3’
+ \\ fs[join_fl3_def, join_fl_def, morePrecise_def, isFixedPoint_def]
+ \\ rveq \\ fs[])
+ \\ rpt strip_tac
+ \\ first_x_assum (qspecl_then [`Fma e1 e2 e3`, `m`] assume_tac)
+ \\ fs[eval_expr_cases, toRExpMap_def] \\ rveq \\ fs[]))
\\ qpat_x_assum `getValidMap _ _ _ = _`
(fn thm => assume_tac (ONCE_REWRITE_RULE [getValidMap_def] thm))
\\ Cases_on `FloverMapTree_mem (Downcast m e) akk` \\ fs[]
@@ -689,7 +796,8 @@ val getValidMap_correct = store_thm (
>- (fs[no_cycle_cast, isMorePrecise_morePrecise])
\\ rpt strip_tac
\\ first_x_assum (qspecl_then [`Downcast m e`, `m`] assume_tac)
- \\ fs[eval_expr_cases, toRExpMap_def] \\ rveq \\ fs[]);
+ \\ fs[eval_expr_cases, toRExpMap_def] \\ rveq \\ fs[]
+QED
val getValidMap_top_contained = store_thm (
"getValidMap_top_contained",
--
GitLab