Commit d6aa770d authored by Heiko Becker's avatar Heiko Becker
Browse files

Make FloVer work with latest HOL master

parent 06ad54de
9eb85f2893da888359e9bff54ed3bca6467523d1
6f28c73ae9284a3419a94804032a979c36154808
......@@ -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)
......
......@@ -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
......
......@@ -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
......
......@@ -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
......
......@@ -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",
......
......@@ -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``);
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment