diff --git a/hol4/.HOLCOMMIT b/hol4/.HOLCOMMIT
index b85ced1d61d6b2e8cfe2219153f36f11a35db688..ead220a1d5bd848889199f5f40bba1f77d0d1722 100644
--- a/hol4/.HOLCOMMIT
+++ b/hol4/.HOLCOMMIT
@@ -1 +1 @@
-9eb85f2893da888359e9bff54ed3bca6467523d1
+6f28c73ae9284a3419a94804032a979c36154808
diff --git a/hol4/ErrorBoundsScript.sml b/hol4/ErrorBoundsScript.sml
index e129830afd73143455cca78d63860ba0f2f5ff9f..6569247e877070672fdb37b239f21f8747d1df8e 100644
--- a/hol4/ErrorBoundsScript.sml
+++ b/hol4/ErrorBoundsScript.sml
@@ -8,6 +8,8 @@ open AbbrevsTheory ExpressionsTheory ExpressionSemanticsTheory RealSimpsTheory
FloverTactics MachineTypeTheory ExpressionAbbrevsTheory EnvironmentsTheory;
open preambleFloVer;
+val _ = temp_delsimps ["NORMEQ_CONV"]
+
val _ = new_theory "ErrorBounds";
val _ = Parse.hide "delta"; (* so that it can be used as a variable *)
@@ -424,10 +426,9 @@ Proof
\\ simp[]
\\ qspec_then `1 / -nR + 1 / (nR - err)` match_mp_tac real_le_trans2 \\ conj_tac
>- (match_mp_tac REAL_LE_LADD_IMP
- \\ simp[GSYM REAL_INV_1OVER]
- \\ `0 < nR - err /\ nR - err <= nF` by REAL_ASM_ARITH_TAC
- \\ qpat_abbrev_tac `nRerr = nR - err`
- \\ fs [REAL_INV_LE_ANTIMONO])
+ \\ rewrite_tac [GSYM REAL_INV_1OVER]
+ \\ ‘0 < nR - err ∧ nR - err ≤ nF’ suffices_by (fs [REAL_INV_LE_ANTIMONO])
+ \\ REAL_ASM_ARITH_TAC)
>- (` - nR <> 0 /\ nR - err <> 0` by REAL_ASM_ARITH_TAC
\\ fs [REAL_ADD_RAT]
\\ `nR - err + - nR = - err` by REAL_ASM_ARITH_TAC
@@ -455,10 +456,8 @@ Proof
\\ rpt (qpat_x_assum `abs x = y` kall_tac)
\\ qspec_then `1 / nR + - (1 / (nR + err))` match_mp_tac real_le_trans2 \\ conj_tac
>- (match_mp_tac REAL_LE_LADD_IMP
- \\ simp [GSYM REAL_INV_1OVER, GSYM REAL_NEG_INV, REAL_LE_NEG]
\\ `0 < nR + err /\ nF <= nR + err` by REAL_ASM_ARITH_TAC
- \\ match_mp_tac REAL_INV_LE_ANTIMONO_IMPR
- \\ conj_tac \\ 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 + err) <> 0` by REAL_ASM_ARITH_TAC
@@ -562,10 +561,8 @@ Proof
\\ 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
- \\ simp [GSYM REAL_INV_1OVER, REAL_LE_NEG]
\\ `0 < - (nR + err) /\ nF <= nR + err` by REAL_ASM_ARITH_TAC
- \\ match_mp_tac REAL_INV_LE_ANTIMONO_IMPR
- \\ conj_tac \\ REAL_ASM_ARITH_TAC)
+ \\ simp [GSYM REAL_INV_1OVER, 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]
@@ -581,7 +578,9 @@ Proof
\\ `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
- \\ simp[GSYM REAL_NEG_RMUL, REAL_NEG_INV, REAL_NEGNEG]
+ \\ 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)
diff --git a/hol4/ErrorIntervalInferenceScript.sml b/hol4/ErrorIntervalInferenceScript.sml
index 69821ef040e8c1a182b53364ba09658c73672bb1..32574f07357013014aac692274efc589ae62245d 100644
--- a/hol4/ErrorIntervalInferenceScript.sml
+++ b/hol4/ErrorIntervalInferenceScript.sml
@@ -86,10 +86,10 @@ Definition inferErrorbound_def:
upperBoundE1 = maxAbs ive1;
upperBoundE2 = maxAbs ive2;
upperBoundE3 = maxAbs ive3;
- errIntv_prod = multInterval errIve2 errIve3;
- mult_error_bound = (upperBoundE2 * err3 + upperBoundE3 * err2 + err2 * err3);
- mAbs = maxAbs (addInterval errIve1 errIntv_prod);
- eNew = err1 + mult_error_bound + computeError mAbs m
+ errIntv_prod = multInterval errIve1 errIve2;
+ mult_error_bound = (upperBoundE1 * err2 + upperBoundE2 * err1 + err1 * err2);
+ mAbs = maxAbs (addInterval errIntv_prod errIve3);
+ eNew = mult_error_bound + err3 + computeError mAbs m
in
SOME (FloverMapTree_insert e (iv_f, eNew) recRes3);
od
diff --git a/hol4/Infra/FloverTactics.sml b/hol4/Infra/FloverTactics.sml
index 9d4e3bdbb64c1f7a235a43d173baa981df1a3994..3ec2e79dc1b75b9454933c93f36a22b1baaba202 100644
--- a/hol4/Infra/FloverTactics.sml
+++ b/hol4/Infra/FloverTactics.sml
@@ -9,7 +9,7 @@ local open intLib wordsLib in end;
open set_relationTheory;
open BasicProvers Defn HolKernel Parse Tactic monadsyntax
alistTheory arithmeticTheory bagTheory boolLib boolSimps bossLib
- combinTheory dep_rewrite finite_mapTheory indexedListsTheory lcsymtacs
+ combinTheory dep_rewrite finite_mapTheory indexedListsTheory
listTheory llistTheory markerLib
optionTheory pairLib pairTheory pred_setTheory
quantHeuristicsLib relationTheory res_quanTheory rich_listTheory
diff --git a/hol4/Infra/preambleFloVer.sml b/hol4/Infra/preambleFloVer.sml
index 9bcfe43bfa5410dea9aeb6c67312d699865ad802..645dd137e950205a1a25088745995495560d8769 100644
--- a/hol4/Infra/preambleFloVer.sml
+++ b/hol4/Infra/preambleFloVer.sml
@@ -8,7 +8,7 @@ open set_relationTheory; (* comes first so relationTheory takes precedence *)
open ASCIInumbersTheory BasicProvers Defn HolKernel Parse SatisfySimps Tactic
monadsyntax alistTheory alignmentTheory arithmeticTheory bagTheory boolLib
boolSimps bossLib containerTheory combinTheory dep_rewrite
- finite_mapTheory indexedListsTheory lcsymtacs listTheory llistTheory
+ finite_mapTheory indexedListsTheory listTheory llistTheory
markerLib mp_then optionTheory pairLib pairTheory pred_setTheory
quantHeuristicsLib relationTheory res_quanTheory
rich_listTheory sortingTheory sptreeTheory stringTheory sumTheory
diff --git a/hol4/IntervalArithScript.sml b/hol4/IntervalArithScript.sml
index 47ac55070e71f27f2de11c1d868e20f403d36970..2bdc189a41ab2317764075eb03cf49a0db560654 100644
--- a/hol4/IntervalArithScript.sml
+++ b/hol4/IntervalArithScript.sml
@@ -6,6 +6,8 @@ open realTheory realLib RealArith
open AbbrevsTheory ExpressionsTheory RealSimpsTheory FloverTactics;
open preambleFloVer;
+val _ = temp_delsimps ["NORMEQ_CONV"]
+
val _ = new_theory "IntervalArith";
val _ = temp_overload_on("abs",``real$abs``);
@@ -254,10 +256,10 @@ val interval_inversion_valid = store_thm ("interval_inversion_valid",
by (match_mp_tac REAL_INV_LE_ANTIMONO \\ REAL_ASM_ARITH_TAC)
\\ REAL_ASM_ARITH_TAC));
-val iv_inv_preserves_valid = store_thm ("iv_inv_preserves_valid",
- ``!iv.
- (IVhi iv < 0 \/ 0 < IVlo iv) /\
- valid iv ==> valid (invertInterval iv)``,
+Theorem iv_inv_preserves_valid:
+ ∀ iv.
+ (IVhi iv < 0 ∨ 0 < IVlo iv) ∧ valid iv ⇒ valid (invertInterval iv)
+Proof
fs [valid_def, invertInterval_def, IVlo_def, IVhi_def]
\\ rpt strip_tac
>- (fs [GSYM REAL_INV_1OVER]
@@ -270,11 +272,12 @@ val iv_inv_preserves_valid = store_thm ("iv_inv_preserves_valid",
\\ rpt CONJ_TAC \\ fs []
\\ match_mp_tac REAL_LET_TRANS
\\ asm_exists_tac \\ fs [])
- >- (fs[GSYM REAL_INV_1OVER]
- \\ match_mp_tac REAL_INV_LE_ANTIMONO_IMPR
- \\ rpt CONJ_TAC \\ fs []
- \\ match_mp_tac REAL_LTE_TRANS
- \\ asm_exists_tac \\ fs []));
+ \\ rewrite_tac [GSYM REAL_INV_1OVER]
+ \\ match_mp_tac REAL_INV_LE_ANTIMONO_IMPR
+ \\ rpt CONJ_TAC \\ fs []
+ \\ match_mp_tac REAL_LTE_TRANS
+ \\ asm_exists_tac \\ fs []
+QED
val interval_addition_valid = store_thm ("interval_addition_valid",
``!iv1 iv2. validIntervalAdd iv1 iv2 (addInterval iv1 iv2)``,
@@ -431,23 +434,22 @@ Proof
QED
Theorem interval_division_valid:
- !(iv1:interval) (iv2:interval) (a:real) (b:real).
- (IVhi iv2 < 0 \/ 0 < IVlo iv2) /\
- contained a iv1 /\
- contained b iv2 ==>
+ ∀ (iv1:interval) (iv2:interval) (a:real) (b:real).
+ (IVhi iv2 < 0 ∨ 0 < IVlo iv2) ∧
+ contained a iv1 ∧
+ contained b iv2 ⇒
contained (a / b) (divideInterval iv1 iv2)
Proof
-rpt gen_tac \\ Cases_on `iv2` \\ rewrite_tac (iv_ss @ [real_div, REAL_MUL_LID]) \\
-rpt gen_tac \\ strip_tac \\
+rpt gen_tac \\ Cases_on `iv2` \\ rewrite_tac (iv_ss @ [real_div, REAL_MUL_LID])
+\\ rpt gen_tac \\ strip_tac
(** TODO: FIXME use qspecl_then **)
-match_mp_tac
+\\ match_mp_tac
(REWRITE_RULE (iv_ss @ [FST,SND])
- (SPECL [``iv1:interval``, ``(inv r, inv q):interval``] interval_multiplication_valid)) \\
-fs [] \\
-match_mp_tac
+ (SPECL [``iv1:interval``, ``(inv r, inv q):interval``] interval_multiplication_valid))
+\\ rpt conj_tac \\ TRY (fs[] \\ NO_TAC)
+\\ imp_res_tac
(REWRITE_RULE
- (iv_ss @ [FST, SND, real_div, REAL_MUL_LID]) (SPECL [``(q,r):interval``, ``b:real``] interval_inversion_valid)) \\
-fs[]
+ (iv_ss @ [FST, SND, real_div, REAL_MUL_LID]) (SPECL [``(q,r):interval``, ``b:real``] interval_inversion_valid))
QED
val iv_div_preserves_valid = store_thm ("iv_div_preserves_valid",
diff --git a/hol4/IntervalValidationScript.sml b/hol4/IntervalValidationScript.sml
index f718ca035be8fb2e482913a13adeb543487b8c75..0ec743fdc526fb4d013ce7bc567513b594add2fd 100644
--- a/hol4/IntervalValidationScript.sml
+++ b/hol4/IntervalValidationScript.sml
@@ -15,6 +15,8 @@ open preambleFloVer;
val _ = new_theory "IntervalValidation";
+val _ = temp_delsimps ["RMUL_LEQNORM"]
+
val _ = Parse.hide "delta"; (* so that it can be used as a variable *)
val _ = temp_overload_on("abs",``real$abs``);
val _ = temp_overload_on("max",``real$max``);