diff --git a/hol4/.HOLCOMMIT b/hol4/.HOLCOMMIT
index faf9210f32ee9982d06b581a71db2bad5580814d..0777dc3aed055adb9ef7ef067ce271eee25e5055 100644
--- a/hol4/.HOLCOMMIT
+++ b/hol4/.HOLCOMMIT
@@ -1 +1 @@
-89e07c5a43c0637bc614b4396e6a8b3cb902cedb
+52ffdc8f01c5cf044427bf6f3a12e8300e91765a
diff --git a/hol4/ErrorBoundsScript.sml b/hol4/ErrorBoundsScript.sml
index 3f87939a93e880c62f6d90459bf85e0ddfe9cf47..18aa186b267261be16af2ec19155eef6de07482a 100644
--- a/hol4/ErrorBoundsScript.sml
+++ b/hol4/ErrorBoundsScript.sml
@@ -447,16 +447,13 @@ Proof
QED
Theorem err_prop_inversion_pos:
- !(nF:real) (nR:real) (err:real) (elo:real) (ehi:real).
- 0 < elo - err /\ 0 < elo /\
- abs (nR - nF) <= err /\
- elo <= nR /\
- nR <= ehi /\
- elo - err <= nF /\
- nF <= ehi + err /\
- 0 <=
- err ==>
- abs (inv nR - inv nF) <= err * inv ((elo - err) * (elo - err))
+ ∀ (nF:real) (nR:real) (err:real) (elo:real) (ehi:real).
+ 0 < elo - err ∧ 0 < elo ∧
+ abs (nR - nF) <= err ∧
+ elo <= nR ∧ nR <= ehi ∧
+ elo - err <= nF ∧ nF <= ehi + err ∧
+ 0 <= err ⇒
+ abs (inv nR - inv nF) <= err * inv ((elo - err) * (elo - err))
Proof
rpt strip_tac
\\ `! (x:real). ((abs x = x) /\ 0 < x) \/ ((abs x = - x) /\ x <= 0)`
@@ -481,26 +478,25 @@ Proof
>- (match_mp_tac REAL_LE_LADD_IMP
\\ ‘0 < nR - err ∧ nR - err ≤ nF’ by REAL_ASM_ARITH_TAC
\\ simp[])
- >- (`- nR <> 0 /\ nR - err <> 0` by REAL_ASM_ARITH_TAC
- \\ ‘(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 * (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))
+ \\ `- nR <> 0 /\ nR - err <> 0` by REAL_ASM_ARITH_TAC
+ \\ ‘(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
+ \\ `nR * (nR - err) <> 0` by fs[REAL_ENTIRE]
+ \\ ‘err * inv (nR * (nR − err)) ≤ err * inv ((elo + -err) pow 2)’
+ by (
+ 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)
+ \\ fs[REAL_INV_MUL'] \\ pop_assum mp_tac \\ fs[])
>- (fs[]
\\ `nR <= nF` by REAL_ASM_ARITH_TAC
\\ `0 < nF` by REAL_ASM_ARITH_TAC
@@ -617,61 +613,61 @@ Proof
>- (`- (nR * (nR - err)) <= - ((ehi + err) * (nR - err))`
by (once_rewrite_tac [REAL_NEG_RMUL] \\ match_mp_tac REAL_LE_RMUL_IMP \\ REAL_ASM_ARITH_TAC)
\\ REAL_ASM_ARITH_TAC)))
- >- (fs []
- \\ `nR <= nF` by REAL_ASM_ARITH_TAC
- \\ `0 < -nF /\ nF <> 0` by REAL_ASM_ARITH_TAC
- \\ `0 < -nR /\ nR <> 0` by REAL_ASM_ARITH_TAC
- \\ `inv (- nR) <= inv (- nF)`
- by (match_mp_tac REAL_INV_LE_ANTIMONO_IMPR \\ conj_tac
- \\ REAL_ASM_ARITH_TAC)
- \\ `inv (- nR) - inv (- nF) <= 0` by REAL_ASM_ARITH_TAC
- \\ `0 <= - (inv (- nR) - inv (-nR)) ` 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]
- \\ `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_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] \\ 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 [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
- \\ ‘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
- \\ 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)
- \\ 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[])
- \\ `0 < (ehi + err) * (ehi + err)` by REAL_ASM_ARITH_TAC
- \\ `0 < - nR * - (nR + err)` by (match_mp_tac REAL_LT_MUL \\ REAL_ASM_ARITH_TAC)
- \\ `0 < nR * (nR + err)` by REAL_ASM_ARITH_TAC
- \\ asm_rewrite_tac[GSYM REAL_NEG_RMUL]
- \\ once_rewrite_tac [REAL_MUL_COMM]
- \\ asm_rewrite_tac[REAL_NEG_INV, REAL_NEGNEG]
- \\ match_mp_tac REAL_INV_LE_ANTIMONO_IMPR \\ conj_tac
- \\ once_rewrite_tac [POW_2] \\ TRY (REAL_ASM_ARITH_TAC)
- \\ conj_tac \\ TRY(REAL_ASM_ARITH_TAC)
- \\ qspec_then `(nR + err) * (ehi + err)` match_mp_tac real_le_trans2
- \\ conj_tac
- >- (once_rewrite_tac [REAL_MUL_COMM]
- \\ match_mp_tac REAL_MUL_LE_COMPAT_NEG_L \\ conj_tac \\ REAL_ASM_ARITH_TAC)
- >- (`- (nR * (nR + err)) <= - ((ehi + err) * (nR + err))`
- by (once_rewrite_tac [REAL_NEG_RMUL] \\ match_mp_tac REAL_LE_RMUL_IMP \\ REAL_ASM_ARITH_TAC)
- \\ REAL_ASM_ARITH_TAC)))
+ \\ fs []
+ \\ `nR <= nF` by REAL_ASM_ARITH_TAC
+ \\ `0 < -nF /\ nF <> 0` by REAL_ASM_ARITH_TAC
+ \\ `0 < -nR /\ nR <> 0` by REAL_ASM_ARITH_TAC
+ \\ `inv (- nR) <= inv (- nF)`
+ by (match_mp_tac REAL_INV_LE_ANTIMONO_IMPR \\ conj_tac
+ \\ REAL_ASM_ARITH_TAC)
+ \\ `inv (- nR) - inv (- nF) <= 0` by REAL_ASM_ARITH_TAC
+ \\ `0 <= - (inv (- nR) - inv (-nR)) ` 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]
+ \\ `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_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] \\ 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 [REAL_LE_NEG, REAL_INV_LE_ANTIMONO, REAL_MUL_LNEG])
+ >- (`- nR <> 0 /\ nR - err <> 0` by REAL_ASM_ARITH_TAC
+ \\ `- (nR + err) <> 0` by REAL_ASM_ARITH_TAC
+ \\ ‘1 / - (nR + err) + 1 / nR = (1 * nR + - (nR + err) * 1) / (- (nR + err) * nR)’
+ by (fs[REAL_ADD_RAT])
+ \\ pop_assum (rewrite_tac o single)
+ \\ rewrite_tac [REAL_MUL_RID, REAL_MUL_LID, real_div, GSYM REAL_NEG_RMUL, GSYM REAL_NEG_LMUL]
+ \\ `nR + - (nR + err) = - err` by REAL_ASM_ARITH_TAC
+ \\ 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)
+ \\ 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[])
+ \\ `0 < (ehi + err) * (ehi + err)` by REAL_ASM_ARITH_TAC
+ \\ `0 < - nR * - (nR + err)` by (match_mp_tac REAL_LT_MUL \\ REAL_ASM_ARITH_TAC)
+ \\ `0 < nR * (nR + err)` by REAL_ASM_ARITH_TAC
+ \\ asm_rewrite_tac[GSYM REAL_NEG_RMUL]
+ \\ once_rewrite_tac [REAL_MUL_COMM]
+ \\ asm_rewrite_tac[REAL_NEG_INV, REAL_NEGNEG, GSYM REAL_INV_1OVER]
+ \\ match_mp_tac REAL_INV_LE_ANTIMONO_IMPR \\ conj_tac
+ \\ once_rewrite_tac [POW_2] \\ TRY (REAL_ASM_ARITH_TAC)
+ \\ conj_tac \\ TRY(REAL_ASM_ARITH_TAC)
+ \\ qspec_then `(nR + err) * (ehi + err)` match_mp_tac real_le_trans2
+ \\ conj_tac
+ >- (once_rewrite_tac [REAL_MUL_COMM]
+ \\ match_mp_tac REAL_MUL_LE_COMPAT_NEG_L \\ conj_tac \\ REAL_ASM_ARITH_TAC)
+ \\ `- (nR * (nR + err)) <= - ((ehi + err) * (nR + err))`
+ by (once_rewrite_tac [REAL_NEG_RMUL] \\ match_mp_tac REAL_LE_RMUL_IMP \\ REAL_ASM_ARITH_TAC)
+ \\ REAL_ASM_ARITH_TAC)
QED
val _ = export_theory();
diff --git a/hol4/ErrorValidationScript.sml b/hol4/ErrorValidationScript.sml
index 9006a7bab503f1977f72cd1eda1d8df36169cd4c..5ad5d16b06967e07fc462ac387dbbba9773135fe 100644
--- a/hol4/ErrorValidationScript.sml
+++ b/hol4/ErrorValidationScript.sml
@@ -366,7 +366,7 @@ QED
local
val trivial_up_tac =
- fs[REAL_LE_ADD] (* remove lhs of addition *)
+ irule REAL_LE_LADD_IMP (* remove lhs of addition *)
(* Try first proving by transitivity only *)
\\ TRY (
irule REAL_LE_RMUL_IMP \\ fs[] \\ NO_TAC)
@@ -470,7 +470,8 @@ Proof
(* 0 ≤ -(nR2 + err2) *)
\\ irule REAL_LE_TRANS
\\ qexists_tac `nR1 * nR2 + (nR1 + err1) * - (nR2 + err2)` \\ conj_tac
- >- trivial_up_tac
+ >- (irule REAL_LE_LADD_IMP
+ \\ irule REAL_LE_RMUL_IMP \\ fs[])
\\ real_rewrite
`nR1 * nR2 + (nR1 + err1) * - (nR2 + err2) = - nR1 * err2 + - nR2 * err1 + - err1 * err2`
\\ simp[] \\ irule REAL_LE_ADD2 \\ conj_tac \\ TRY(simp[GSYM REAL_NEG_LMUL])
@@ -479,7 +480,9 @@ Proof
>- (
irule REAL_LE_TRANS
\\ qexists_tac `nR1 * nR2 + nF1 * - (nR2 - err2)` \\ conj_tac
- >- trivial_up_tac
+ >- (irule REAL_LE_LADD_IMP \\ once_rewrite_tac [REAL_NEG_RMUL]
+ \\ irule REAL_LE_LMUL_IMP \\ fs[real_sub]
+ \\ qpat_x_assum ‘∀ x. _’ kall_tac \\ REAL_ASM_ARITH_TAC)
\\ qspecl_then [`- (nR2 - err2)`, `0`] DISJ_CASES_TAC REAL_LTE_TOTAL
(* -(nR2 - err2) < 0 *)
>- (irule REAL_LE_TRANS
@@ -494,7 +497,7 @@ Proof
>- (
irule REAL_LE_TRANS
\\ qexists_tac `nR1 * nR2 + (nR1 + err1) * - (nR2 - err2)` \\ conj_tac
- >- trivial_up_tac
+ >- (irule REAL_LE_LADD_IMP \\ irule REAL_LE_RMUL_IMP \\ fs[])
\\ real_rewrite
`nR1 * nR2 + (nR1 + err1) * - (nR2 - err2) = nR1 * err2 + - nR2 * err1 + err1 * err2`
\\ simp[] \\ irule REAL_LE_ADD2 \\ conj_tac \\ simp[GSYM REAL_NEG_LMUL])))
diff --git a/hol4/TypeValidatorScript.sml b/hol4/TypeValidatorScript.sml
index 3705382981c0d5f583c5199bd5b820d0c9085d41..4e6676a30108e16321bd4a434f8045f9f076faa5 100644
--- a/hol4/TypeValidatorScript.sml
+++ b/hol4/TypeValidatorScript.sml
@@ -219,6 +219,8 @@ val by_monotonicity =
\\ fs[FloverMapTree_mem_def]
\\ EVERY_CASE_TAC \\ fs[];
+val _ = temp_delsimps ["lift_disj_eq", "lift_imp_disj"]
+
Theorem getValidMap_mono:
∀ e Gamma akk res.
getValidMap Gamma e akk = Succes res ⇒