diff --git a/hol4/CertificateCheckerScript.sml b/hol4/CertificateCheckerScript.sml
index 96783cbe44f72d15e1b3637d8d6d3c51e4eb4003..bb2936dd7c7c79c43f28c341c4f28f94ddf8ae32 100644
--- a/hol4/CertificateCheckerScript.sml
+++ b/hol4/CertificateCheckerScript.sml
@@ -13,7 +13,8 @@ open AbbrevsTheory ExpressionsTheory FloverTactics ExpressionAbbrevsTheory
open preambleFloVer;
val _ = new_theory "CertificateChecker";
-val _ = temp_overload_on("abs",``real$abs``);
+
+Overload abs[local] = “real$absâ€;
(** Certificate checking function **)
Definition CertificateChecker_def:
diff --git a/hol4/CertificateGeneratorScript.sml b/hol4/CertificateGeneratorScript.sml
index af731bc5e7831dc87f1f5bf5eb7b8e974a59caa8..912e62bcf32584ab1b0e6ff7cb5923a227b50b7c 100644
--- a/hol4/CertificateGeneratorScript.sml
+++ b/hol4/CertificateGeneratorScript.sml
@@ -1,3 +1,8 @@
+(**
+ A simple, unverified generator for certificates.
+ To be used in conjunction with the certificate checker to first analyze
+ a kernel and then validate the analysis result
+**)
open RealIntervalInferenceTheory ErrorIntervalInferenceTheory ExpressionsTheory
FloverMapTheory TypeValidatorTheory CommandsTheory AbbrevsTheory
ExpressionAbbrevsTheory;
@@ -5,7 +10,7 @@ open preambleFloVer;
val _ = new_theory "CertificateGenerator";
-val CertificateGeneratorExp_def = Define `
+Definition CertificateGeneratorExp_def:
CertificateGeneratorExp (f:real expr) (P:precond) (Gamma:typeMap)
:(real expr # precond # typeMap # analysisResult) option =
let
@@ -17,15 +22,18 @@ val CertificateGeneratorExp_def = Define `
(case inferErrorbound f tMap ivMap FloverMapTree_empty of
| SOME errMap => SOME (f,P,Gamma,errMap)
| NONE => NONE)
- | _, _ => NONE`;
+ | _, _ => NONE
+End
-val getExp_def = Define `
- getExp (f, P, Gamma, errMap) = f`;
+Definition getExp_def:
+ getExp (f, P, Gamma, errMap) = f
+End
-val getError_def = Define `
- getError (f, P, Gamma, errMap) = FloverMapTree_find f errMap`;
+Definition getError_def:
+ getError (f, P, Gamma, errMap) = FloverMapTree_find f errMap
+End
-val CertificateGeneratorCmd_def = Define `
+Definition CertificateGeneratorCmd_def:
CertificateGeneratorCmd (f:real cmd) (P:precond) (Gamma:typeMap)
:(real cmd # precond # typeMap # analysisResult) option =
let
@@ -37,12 +45,15 @@ val CertificateGeneratorCmd_def = Define `
(case inferErrorboundCmd f tMap ivMap FloverMapTree_empty of
| SOME errMap => SOME (f,P,Gamma,errMap)
| NONE => NONE)
- | _, _ => NONE`;
+ | _, _ => NONE
+End
-val getCmd_def = Define `
- getCmd (f, P, Gamma, errMap) = f`;
+Definition getCmd_def:
+ getCmd (f, P, Gamma, errMap) = f
+End
-val getError_def = Define `
- getError (f, P, Gamma, errMap) = FloverMapTree_find (getRetExp f) errMap`;
+Definition getError_def:
+ getError (f, P, Gamma, errMap) = FloverMapTree_find (getRetExp f) errMap
+End
val _ = export_theory ();
diff --git a/hol4/EnvironmentsScript.sml b/hol4/EnvironmentsScript.sml
index d70808ae24432cdd87d1725938ef30e097389bc5..4c9afa6bcaa9ab3e212aef5b76584e285f876a3d 100644
--- a/hol4/EnvironmentsScript.sml
+++ b/hol4/EnvironmentsScript.sml
@@ -1,3 +1,8 @@
+(**
+ An inductive relation relating real-numbered environments with
+ an environment with "errors", i.e. where variables are bound to
+ finite-precision values
+**)
open simpLib realTheory realLib RealArith sptreeTheory;
open AbbrevsTheory ExpressionAbbrevsTheory RealSimpsTheory CommandsTheory
FloverTactics FloverMapTheory MachineTypeTheory;
@@ -5,7 +10,7 @@ open preambleFloVer;
val _ = new_theory "Environments";
-val _ = temp_overload_on("abs",``real$abs``);
+Overload abs[local] = “real$absâ€
Definition approxEnv_def:
approxEnv E1 Gamma absEnv (fVars:num_set) (dVars:num_set) E2 =
@@ -98,8 +103,7 @@ Proof
\\ fs[]
QED
-val approxEnv_rules = LIST_CONJ [approxEnvRefl, approxEnvUpdFree, approxEnvUpdBound]
-val _ = save_thm ("approxEnv_rules", approxEnv_rules);
+Theorem approxEnv_rules = LIST_CONJ [approxEnvRefl, approxEnvUpdFree, approxEnvUpdBound]
Theorem approxEnv_gives_value:
!E1 E2 x v (fVars:num_set) (dVars:num_set) absenv Gamma.
diff --git a/hol4/ErrorBoundsScript.sml b/hol4/ErrorBoundsScript.sml
index de5066aff8284f56497f1d83fabaabf983a454d3..28f75c3b528e7d968299252ff11efb4904a36500 100644
--- a/hol4/ErrorBoundsScript.sml
+++ b/hol4/ErrorBoundsScript.sml
@@ -11,7 +11,8 @@ open preambleFloVer;
val _ = new_theory "ErrorBounds";
val _ = Parse.hide "delta"; (* so that it can be used as a variable *)
-val _ = temp_overload_on("abs",``real$abs``);
+
+Overload abs[local] = “real$absâ€
val triangle_tac =
irule triangle_trans \\ rpt conj_tac \\ TRY (fs[REAL_ABS_TRIANGLE] \\ NO_TAC);
diff --git a/hol4/ErrorIntervalInferenceScript.sml b/hol4/ErrorIntervalInferenceScript.sml
index e7e460944bfd65e86277ab0dba7950632dfc8407..f764a730ab7154099c0c4ba7f1cdda4f9c79b962 100644
--- a/hol4/ErrorIntervalInferenceScript.sml
+++ b/hol4/ErrorIntervalInferenceScript.sml
@@ -1,4 +1,4 @@
- (**
+(**
This file contains the HOL4 implementation of the error bound validator as well
as its soundness proof. The function validErrorbound is the Error bound
validator from the certificate checking process. Under the assumption that a
diff --git a/hol4/ErrorValidationScript.sml b/hol4/ErrorValidationScript.sml
index 49dc781630440f36a47cc1af21743693b9b4aad1..cf7df26f5fba39e6da4def0816302a96ba063584 100644
--- a/hol4/ErrorValidationScript.sml
+++ b/hol4/ErrorValidationScript.sml
@@ -17,11 +17,10 @@ open preambleFloVer;
val _ = new_theory "ErrorValidation";
val _ = Parse.hide "delta"; (* so that it can be used as a variable *)
-val _ = temp_overload_on("abs",``real$abs``);
-val _ = temp_overload_on("+",``realax$real_add``);
-val _ = temp_overload_on("-",``real$real_sub``);
-val _ = temp_overload_on("*",``realax$real_mul``);
-val _ = temp_overload_on("/",``real$/``);
+
+Overload abs[local] = “real$absâ€
+
+val _ = realLib.prefer_real();
val triangle_tac =
irule triangle_trans \\ fs[REAL_ABS_TRIANGLE];
diff --git a/hol4/FPRangeValidatorScript.sml b/hol4/FPRangeValidatorScript.sml
index 5d3ae902fddcfd2b7688b222bbca8d152aa38859..87b1530c66bfe3551f2dab77ed1774d110852cfe 100644
--- a/hol4/FPRangeValidatorScript.sml
+++ b/hol4/FPRangeValidatorScript.sml
@@ -18,9 +18,9 @@ open preambleFloVer;
val _ = new_theory "FPRangeValidator";
-val _ = temp_overload_on("abs",``real$abs``);
+Overload abs[local] = “real$absâ€
-val FPRangeValidator_def = Define `
+Definition FPRangeValidator_def:
FPRangeValidator (e:real expr) A typeMap dVars =
case FloverMapTree_find e A, FloverMapTree_find e typeMap of
| SOME (iv_e, err_e), SOME m =>
@@ -58,28 +58,31 @@ val FPRangeValidator_def = Define `
then normal_or_zero /\ recRes
else
F)
- | _, _ => F`;
+ | _, _ => F
+End
-val normalOrZero_def = Define `
+Definition normalOrZero_def:
normalOrZero iv_e_float m =
((normal (IVlo iv_e_float) m \/ (IVlo iv_e_float) = 0) /\
- (normal (IVhi iv_e_float) m \/ (IVhi iv_e_float) = 0))`;
+ (normal (IVhi iv_e_float) m \/ (IVhi iv_e_float) = 0))
+End
-val FPRangeValidatorCmd_def = Define `
+Definition FPRangeValidatorCmd_def:
(FPRangeValidatorCmd ((Let m x e g):real cmd) A typeMap dVars =
if FPRangeValidator e A typeMap dVars
then FPRangeValidatorCmd g A typeMap (insert x () dVars)
else F) /\
(FPRangeValidatorCmd (Ret e) A typeMap dVars =
- FPRangeValidator e A typeMap dVars)`;
+ FPRangeValidator e A typeMap dVars)
+End
-val enclosure_to_abs = store_thm (
- "enclosure_to_abs",
- ``!a b c.
+Theorem enclosure_to_abs:
+ !a b c.
a <= b /\ b <= c /\
(0 < a \/ c < 0 ) ==>
(abs a <= abs b /\ abs b <= abs c) \/
- (abs c <= abs b /\ abs b <= abs a)``,
+ (abs c <= abs b /\ abs b <= abs a)
+Proof
rpt strip_tac \\ fs[]
>- (`0 < b` by REAL_ASM_ARITH_TAC
\\ `0 <= a /\ 0 <= b` by REAL_ASM_ARITH_TAC
@@ -91,21 +94,22 @@ val enclosure_to_abs = store_thm (
>- (`~ (0 <= b)` by REAL_ASM_ARITH_TAC
\\ `~ (0 <= a)` by REAL_ASM_ARITH_TAC
\\ `~ (0 <= c)` by REAL_ASM_ARITH_TAC
- \\ fs[realTheory.abs]));
+ \\ fs[realTheory.abs])
+QED
fun assume_all l =
case l of
t :: ls => assume_tac t \\ assume_all ls
| NIL => ALL_TAC;
-val normal_enclosing = store_thm (
- "normal_enclosing",
- ``!v m vHi vLo.
+Theorem normal_enclosing:
+ !v m vHi vLo.
(0 < vLo \/ vHi < 0) /\
normal vLo m /\
normal vHi m /\
vLo <= v /\ v <= vHi ==>
- normal v m``,
+ normal v m
+Proof
rpt gen_tac
\\ disch_then (fn thm => assume_all (CONJ_LIST 4 thm))
\\ `(abs vLo <= abs v /\ abs v <= abs vHi) \/ (abs vHi <= abs v /\ abs v <= abs vLo)`
@@ -114,7 +118,8 @@ val normal_enclosing = store_thm (
\\ fs[normal_def]
\\ rveq
\\ fs[]
- \\ RealArith.REAL_ASM_ARITH_TAC);
+ \\ RealArith.REAL_ASM_ARITH_TAC
+QED
val solve_tac =
rpt (qpat_x_assum `!x. _` kall_tac)
diff --git a/hol4/IEEE_connectionScript.sml b/hol4/IEEE_connectionScript.sml
index e966341aa18ff56c552a0029f118e7ef5048cfaa..0128b2dbdaa0f0e9f45dd7d048139e605d5e3c00 100644
--- a/hol4/IEEE_connectionScript.sml
+++ b/hol4/IEEE_connectionScript.sml
@@ -1,3 +1,7 @@
+(**
+ Connect FloVer's idealized machine semantics to 64-bit
+ IEEE-754 floating-point semantics
+**)
open machine_ieeeTheory binary_ieeeTheory lift_ieeeTheory realTheory RealArith;
open MachineTypeTheory ExpressionsTheory RealSimpsTheory FloverTactics
CertificateCheckerTheory FPRangeValidatorTheory IntervalValidationTheory
@@ -9,7 +13,8 @@ open preambleFloVer;
val _ = new_theory "IEEE_connection";
-val _ = temp_overload_on("abs",``real$abs``);
+Overload abs[local] = “real$absâ€
+
val _ = diminish_srw_ss ["RMULCANON_ss","RMULRELNORM_ss"]
(** FloVer assumes rounding with ties to even, thus we exprlicitly define
@@ -295,30 +300,41 @@ Proof
\\ `w2n c0 = 2047` by fs[] \\ fs[]
\\ TOP_CASE_TAC \\ fs[minValue_pos_def, minExponentPos_def]
\\ fs[REAL_ABS_MUL, POW_M1]
- >- (`44942328371557897693232629769725618340449424473557664318357520289433168951375240783177119330601884005280028469967848339414697442203604155623211857659868531094441973356216371319075554900311523529863270738021251442209537670585615720368478277635206809290837627671146574559986811484619929076208839082406056034304â»Â¹ <= inv 1`
- by (irule REAL_INV_LE_ANTIMONO_IMPR \\ fs[])
- \\ fs[pow_simp1, REAL_DIV_LZERO, ABS_1, REAL_OF_NUM_POW, abs]
- \\ `179769313486231590772930519078902473361797697894230657273430081157732675805500963132708477322407536021120113879871393357658789768814416622492847430639474124377767893424865485276302219601246094119453082952085005768838150682342462881473913110540827237163350510684586298239947245938479716304835356329624224137216 < inv 1`
- by (irule REAL_LTE_TRANS \\ asm_exists_tac \\ fs[])
- \\ fs[REAL_INV1])
+ >- (
+ qpat_x_assum ‘_ < inv _’ mp_tac
+ \\ qmatch_goalsub_abbrev_tac ‘_ < inv cst1 ⇒ _’
+ \\ strip_tac
+ \\ `inv cst1 <= inv 1`
+ by (unabbrev_all_tac \\ irule REAL_INV_LE_ANTIMONO_IMPR \\ fs[])
+ \\ fs[pow_simp1, REAL_DIV_LZERO, ABS_1, REAL_OF_NUM_POW, abs]
+ \\ qpat_x_assum ‘_ < inv cst1’ mp_tac
+ \\ qmatch_goalsub_abbrev_tac ‘cst2 < inv cst1’ \\ strip_tac
+ \\ `cst2 < inv 1`
+ by (unabbrev_all_tac \\ irule REAL_LTE_TRANS \\ asm_exists_tac \\ fs[])
+ \\ unabbrev_all_tac \\ 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[]
- \\ 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[])
+ 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[])
+ \\ qpat_x_assum ‘_ < inv _’ mp_tac
+ \\ qmatch_goalsub_abbrev_tac ‘_ < inv cst1 ⇒ _’
+ \\ `inv cst1 <= inv 1`
+ by (unabbrev_all_tac \\ irule REAL_INV_LE_ANTIMONO_IMPR \\ fs[])
+ \\ strip_tac
\\ fs[pow_simp1, REAL_DIV_LZERO, ABS_1, REAL_OF_NUM_POW, abs]
- \\ `179769313486231590772930519078902473361797697894230657273430081157732675805500963132708477322407536021120113879871393357658789768814416622492847430639474124377767893424865485276302219601246094119453082952085005768838150682342462881473913110540827237163350510684586298239947245938479716304835356329624224137216 < inv 1`
- by (irule REAL_LTE_TRANS \\ once_rewrite_tac[CONJ_COMM]
+ \\ qpat_x_assum ‘_ < inv cst1’ mp_tac
+ \\ qmatch_goalsub_abbrev_tac ‘(cst2 * _) < inv cst1’
+ \\ strip_tac
+ \\ `cst2 < inv 1`
+ by (unabbrev_all_tac \\ irule REAL_LTE_TRANS \\ once_rewrite_tac[CONJ_COMM]
\\ rewrite_tac[REAL_INV1] \\ asm_exists_tac \\ fs[]
\\ qmatch_goalsub_abbrev_tac `cst1 < cst2`
\\ `0 <= (1:real) + &n / 4503599627370496`
@@ -332,7 +348,7 @@ Proof
\\ once_rewrite_tac [GSYM REAL_MUL_ASSOC] \\ irule REAL_LT_LMUL_IMP
\\ fs[]
\\ unabbrev_all_tac \\ fs[])
- \\ fs[REAL_INV1]
+ \\ unabbrev_all_tac \\ fs[REAL_INV1]
QED
Theorem validValue_gives_float_value:
@@ -760,6 +776,7 @@ Proof
denormalTranslatedValue_implies_finiteness,
normalValue_implies_normalization,
GSYM float_is_zero_to_real, float_is_finite, evalUnop_def,
+ sqrtable_def,
normalizes_def])
\\ fs[dmode_def] \\ simp[Once eval_expr_cases]
\\ qexistsl_tac [`M64`, `float_to_real (fp64_to_float v)`, ‘e'’]
@@ -777,11 +794,7 @@ Proof
denormalTranslatedValue_implies_finiteness,
normalValue_implies_normalization, float_is_finite,
GSYM float_is_zero_to_real, evalUnop_def]
- >- fs[validFloatValue_def,
- normalTranslatedValue_implies_finiteness,
- denormalTranslatedValue_implies_finiteness,
- normalValue_implies_normalization, float_is_finite,
- GSYM float_is_zero_to_real, evalUnop_def]
+ >- fs[sqrtable_def]
>- (
fs[normalTranslatedValue_implies_finiteness,
denormalTranslatedValue_implies_finiteness,
diff --git a/hol4/Infra/MachineTypeScript.sml b/hol4/Infra/MachineTypeScript.sml
index 5b3abec2fd3d6798edab0ac0dc280549fe5d0ed1..9c343ddd663fc93e7ee0cfb61beb5b603922d35f 100644
--- a/hol4/Infra/MachineTypeScript.sml
+++ b/hol4/Infra/MachineTypeScript.sml
@@ -10,11 +10,11 @@ open preambleFloVer;
val _ = new_theory "MachineType";
-val _ = temp_overload_on("abs",``real$abs``);
+Overload abs[local] = “real$absâ€
+
val _ = monadsyntax.enable_monadsyntax();
val _ = List.app monadsyntax.enable_monad ["option"];
-
Datatype:
mType = REAL | M16 | M32 | M64 | F num num bool (* first num is word length, second is fractional bits, bool is for sign of fractional bits *)
End
diff --git a/hol4/Infra/RealSimpsScript.sml b/hol4/Infra/RealSimpsScript.sml
index 8fe579a7033e0d354c58fa813d8ed634a1af6658..7efdcad7fe1953deccfff75cb8727928f6eca062 100644
--- a/hol4/Infra/RealSimpsScript.sml
+++ b/hol4/Infra/RealSimpsScript.sml
@@ -1,44 +1,53 @@
+(**
+ Real-number simplification theorems
+**)
open RealArith;
open realTheory realLib;
open preambleFloVer;
- (*
-val _ = ParseExtras.temp_tight_equality() *)
val _ = new_theory "RealSimps";
-val _ = temp_overload_on("abs",``real$abs``);
-val _ = temp_overload_on("max",``real$max``);
+Overload abs[local] = “real$absâ€
+Overload max[local] = “real$maxâ€
-val abs_leq_zero = store_thm (
- "abs_leq_zero[simp]",
- ``!v. abs v <= 0 <=> v = 0``,
- rw[realTheory.abs] \\ RealArith.REAL_ASM_ARITH_TAC);
+Theorem abs_leq_zero[simp]:
+ !v. abs v <= 0 <=> v = 0
+Proof
+ rw[realTheory.abs] \\ RealArith.REAL_ASM_ARITH_TAC
+QED
-val REAL_INV_LE_ANTIMONO = store_thm ("REAL_INV_LE_ANTIMONO",
- ``! x y. 0 < x /\ 0 < y ==> (inv x <= inv y <=> y <= x)``,
+Theorem REAL_INV_LE_ANTIMONO:
+ ! x y. 0 < x /\ 0 < y ==> (inv x <= inv y <=> y <= x)
+Proof
rpt strip_tac
\\ `inv x < inv y <=> y < x`
by (MATCH_MP_TAC REAL_INV_LT_ANTIMONO \\ fs [])
\\ EQ_TAC
\\ fs [REAL_LE_LT]
\\ STRIP_TAC
- \\ fs [REAL_INV_INJ]);
+ \\ fs [REAL_INV_INJ]
+QED
-val REAL_INV_LE_ANTIMONO_IMPR = store_thm ("REAL_INV_LE_ANTIMONO_IMPR",
- ``! x y. 0 < x /\ 0 < y /\ y <= x ==> inv x <= inv y``,
- rpt strip_tac \\ fs[REAL_INV_LE_ANTIMONO]);
+Theorem REAL_INV_LE_ANTIMONO_IMPR:
+ ! x y. 0 < x /\ 0 < y /\ y <= x ==> inv x <= inv y
+Proof
+ rpt strip_tac \\ fs[REAL_INV_LE_ANTIMONO]
+QED
-val REAL_INV_LE_ANTIMONO_IMPL = store_thm ("REAL_INV_LE_ANTIMONO_IMPL",
- ``! x y. x <0 /\ y < 0 /\ y <= x ==> inv x <= inv y``,
+Theorem REAL_INV_LE_ANTIMONO_IMPL:
+ ! x y. x <0 /\ y < 0 /\ y <= x ==> inv x <= inv y
+Proof
rpt strip_tac
\\ once_rewrite_tac [GSYM REAL_LE_NEG]
\\ `- inv y = inv (- y)` by (irule REAL_NEG_INV \\ REAL_ASM_ARITH_TAC)
\\ `- inv x = inv (- x)` by (irule REAL_NEG_INV \\ REAL_ASM_ARITH_TAC)
\\ ntac 2(FIRST_X_ASSUM (fn thm => once_rewrite_tac [ thm]))
- \\ irule REAL_INV_LE_ANTIMONO_IMPR \\ fs[]);
+ \\ irule REAL_INV_LE_ANTIMONO_IMPR \\ fs[]
+QED
-val REAL_MUL_LE_COMPAT_NEG_L = store_thm( "REAL_MUL_LE_COMPAT_NEG_L",
-``!(a:real) b c. a <= &0 /\ b <= c ==> a * c <= a * b``,
+Theorem REAL_MUL_LE_COMPAT_NEG_L:
+ !(a:real) b c. a <= &0 /\ b <= c ==> a * c <= a * b
+Proof
rpt strip_tac
\\ once_rewrite_tac [SYM (SPEC ``a:real`` REAL_NEG_NEG)]
\\ once_rewrite_tac [SYM (SPECL [``a:real``, ``c:real``] REAL_MUL_LNEG)]
@@ -46,51 +55,70 @@ val REAL_MUL_LE_COMPAT_NEG_L = store_thm( "REAL_MUL_LE_COMPAT_NEG_L",
\\ `0 <= - (a:real)`
by (once_rewrite_tac [SYM (SPEC ``-(a:real)`` REAL_NEG_LE0)]
\\ fs [REAL_NEG_NEG])
- \\ match_mp_tac REAL_LE_LMUL_IMP \\ fs[]);
+ \\ match_mp_tac REAL_LE_LMUL_IMP \\ fs[]
+QED
-val maxAbs = store_thm ("maxAbs",
- ``!p q (r:real). (p <= q) /\ (q <= r) ==> (abs q <= max (abs p) (abs r))``,
+Theorem maxAbs:
+ !p q (r:real). (p <= q) /\ (q <= r) ==> (abs q <= max (abs p) (abs r))
+Proof
rpt strip_tac
\\ simp [REAL_LE_MAX]
- \\ REAL_ASM_ARITH_TAC);
+ \\ REAL_ASM_ARITH_TAC
+QED
-val maxAbs_def = Define `
- maxAbs iv = max (abs (FST iv)) (abs (SND iv))`;
+Definition maxAbs_def:
+ maxAbs iv = max (abs (FST iv)) (abs (SND iv))
+End
-val Rabs_err_simpl = store_thm("Rabs_err_simpl",
- ``!(a:real) (b:real). abs (a - (a * (1 + b))) = abs (a * b)``,
- rpt strip_tac \\ REAL_ASM_ARITH_TAC);
+Theorem Rabs_err_simpl:
+ !(a:real) (b:real). abs (a - (a * (1 + b))) = abs (a * b)
+Proof
+ rpt strip_tac \\ REAL_ASM_ARITH_TAC
+QED
-val machineEpsilon_def = Define `machineEpsilon = 1/ (2 pow 53)`;
+Definition machineEpsilon_def:
+ machineEpsilon = 1/ (2 pow 53)
+End
-val real_le_trans2 = store_thm ("real_le_trans2",
-``!(y:real) x z. x <= y /\ y <= z ==> x <= z``, metis_tac[REAL_LE_TRANS]);
+Theorem real_le_trans2:
+ !(y:real) x z. x <= y /\ y <= z ==> x <= z
+Proof
+ metis_tac[REAL_LE_TRANS]
+QED
-val mEps_geq_zero = store_thm ("mEps_geq_zero",
-``0 <= machineEpsilon``, once_rewrite_tac[machineEpsilon_def] \\ EVAL_TAC);
+Theorem mEps_geq_zero:
+ 0 <= machineEpsilon
+Proof
+ once_rewrite_tac[machineEpsilon_def] \\ EVAL_TAC
+QED
-val err_up = store_thm ("err_up",
- ``!a b (c:real).
+Theorem err_up:
+ !a b (c:real).
0 <= c /\
a - b <= c /\
0 < a - b ==>
- b <= a + c``,
- REAL_ASM_ARITH_TAC);
-
-val REAL_LE_ADD_FLIP = store_thm ("REAL_LE_ADD_FLIP",
- ``!a b (c:real).
- a - b <= c ==>
- a - c <= b``,
- REAL_ASM_ARITH_TAC);
-
-val triangle_trans = store_thm (
- "triangle_trans",
- ``!a b c.
+ b <= a + c
+Proof
+ REAL_ASM_ARITH_TAC
+QED
+
+Theorem REAL_LE_ADD_FLIP:
+ !a b (c:real).
+ a - b <= c ==>
+ a - c <= b
+Proof
+ REAL_ASM_ARITH_TAC
+QED
+
+Theorem triangle_trans:
+ !a b c.
abs (a + b) <= abs a + abs b /\
abs a + abs b <= c ==>
- abs (a + b) <= c``,
+ abs (a + b) <= c
+Proof
rpt strip_tac
- \\ REAL_ASM_ARITH_TAC);
+ \\ REAL_ASM_ARITH_TAC
+QED
Theorem REAL_LE_ABS_TRANS:
! a b.
diff --git a/hol4/Infra/ResultsScript.sml b/hol4/Infra/ResultsScript.sml
index 5c995ab12bcdebccfa91eed72daa4a3d10c04c80..4354a28621da05fde397255299058f193f9d12c2 100644
--- a/hol4/Infra/ResultsScript.sml
+++ b/hol4/Infra/ResultsScript.sml
@@ -1,25 +1,33 @@
+(**
+ A simple Result datatype to ease some implementations
+**)
open stringTheory;
open preambleFloVer;
val _ = new_theory "Results";
-val _ = Datatype `
- result = Succes 'a | Fail string | FailDet string 'a`;
+Datatype:
+ result = Succes 'a | Fail string | FailDet string 'a
+End
-val injectResult_def = Define `
+Definition injectResult_def:
injectResult (Succes _) = T /\
- injectResult _ = F`;
+ injectResult _ = F
+End
-val result_bind_def = Define `
+Definition result_bind_def:
result_bind (Fail s) f = Fail s /\
result_bind (FailDet s x) f = FailDet s x /\
- result_bind (Succes x) f = f x`;
+ result_bind (Succes x) f = f x
+End
-val result_ignore_bind_def = Define `
- result_ignore_bind m1 m2 = result_bind m1 (K m2) `;
+Definition result_ignore_bind_def:
+ result_ignore_bind m1 m2 = result_bind m1 (K m2)
+End
-val result_return_def = Define `
- result_return x = Succes x`;
+Definition result_return_def:
+ result_return x = Succes x
+End
val _ = export_rewrites ["result_return_def", "result_bind_def", "result_ignore_bind_def"]
diff --git a/hol4/IntervalArithScript.sml b/hol4/IntervalArithScript.sml
index 7dd1cce457e15c1e262db48c1119a88f16cad1da..35e5e72683aa793b60dfc34af01c5b70d8c2445f 100644
--- a/hol4/IntervalArithScript.sml
+++ b/hol4/IntervalArithScript.sml
@@ -10,9 +10,10 @@ val _ = temp_delsimps ["NORMEQ_CONV"]
val _ = new_theory "IntervalArith";
-val _ = temp_overload_on("abs",``real$abs``);
-val _ = temp_overload_on("max",``real$max``);
-val _ = temp_overload_on("min",``real$min``);
+Overload abs[local] = “real$absâ€
+Overload max[local] = “real$maxâ€
+Overload min[local] = “real$minâ€
+
(**
Define validity of an interval, requiring that the lower bound is less than or equal to the upper bound.
Containement is defined such that if x is contained in the interval, it must lie between the lower and upper bound.
@@ -136,20 +137,24 @@ Proof
metis_tac (iv_ss @ [REAL_LE_TRANS])
QED
-val contained_implies_subset = store_thm ("contained_implies_subset",
-``!(a:real) (iv:interval).
- contained a iv ==> isSupersetInterval (pointInterval a) iv``,
-fs iv_ss);
+Theorem contained_implies_subset:
+ !(a:real) (iv:interval).
+ contained a iv ==> isSupersetInterval (pointInterval a) iv
+Proof
+ fs iv_ss
+QED
-val validPointInterval = store_thm("validPointInterval",
-``!(a:real).
- contained a (pointInterval a)``,
-fs iv_ss);
+Theorem validPointInterval:
+ !(a:real). contained a (pointInterval a)
+Proof
+ fs iv_ss
+QED
-val min4_correct = store_thm ("min4_correct",
-``!a b c d.
- let m = min4 a b c d in
- m <= a /\ m <= b /\ m <= c /\ m <= d``,
+Theorem min4_correct:
+ !a b c d.
+ let m = min4 a b c d in
+ m <= a /\ m <= b /\ m <= c /\ m <= d
+Proof
rpt strip_tac \\fs [min4_def] \\ conj_tac \\
try (fs [REAL_MIN_LE1]) \\ conj_tac
>- (`min b (min c d) <= b` by fs[REAL_MIN_LE1] \\
@@ -172,12 +177,14 @@ try (fs [REAL_MIN_LE1]) \\ conj_tac
match_mp_tac REAL_LE_TRANS \\
`min b (min c d) <= min c d` by fs[REAL_MIN_LE2] \\
HINT_EXISTS_TAC \\
- fs [REAL_MIN_LE2])));
+ fs [REAL_MIN_LE2]))
+QED
-val max4_correct = store_thm ("max4_correct",
-``!a b c d.
+Theorem max4_correct:
+ !a b c d.
let m = max4 a b c d in
- a <= m /\ b <= m /\ c <= m /\ d <= m``,
+ a <= m /\ b <= m /\ c <= m /\ d <= m
+Proof
rpt strip_tac \\fs [max4_def] \\ conj_tac \\
try (fs [REAL_LE_MAX1]) \\ conj_tac
>-(`b <= max b (max c d)` by fs[REAL_LE_MAX1] \\
@@ -200,22 +207,27 @@ fs [REAL_LE_MAX2])
match_mp_tac REAL_LE_TRANS \\
`max c d <= max b (max c d)` by fs[REAL_LE_MAX2] \\
HINT_EXISTS_TAC \\
- fs [REAL_LE_MAX2] )));
+ fs [REAL_LE_MAX2] ))
+QED
-val interval_negation_valid = store_thm ("interval_negation_valid",
-``!iv a.
- contained a iv ==> contained (- a) (negateInterval iv)``,
-fs iv_ss);
+Theorem interval_negation_valid:
+ !iv a. contained a iv ==> contained (- a) (negateInterval iv)
+Proof
+ fs iv_ss
+QED
-val iv_neg_preserves_valid = store_thm ("iv_neg_preserves_valid",
- ``!iv.
- valid iv ==> valid (negateInterval iv)``,
- fs [valid_def, negateInterval_def, IVlo_def, IVhi_def]);
+Theorem iv_neg_preserves_valid:
+ !iv.
+ valid iv ==> valid (negateInterval iv)
+Proof
+ fs [valid_def, negateInterval_def, IVlo_def, IVhi_def]
+QED
-val interval_inversion_valid = store_thm ("interval_inversion_valid",
- ``!iv a.
+Theorem interval_inversion_valid:
+ !iv a.
(IVhi iv < 0 \/ 0 < IVlo iv) /\ contained a iv ==>
- contained (inv a) (invertInterval iv)``,
+ contained (inv a) (invertInterval iv)
+Proof
fs iv_ss \\ rpt strip_tac \\ once_rewrite_tac [GSYM REAL_INV_1OVER]
(* First subgoal *)
>- (once_rewrite_tac [GSYM REAL_LE_NEG]
@@ -250,7 +262,8 @@ val interval_inversion_valid = store_thm ("interval_inversion_valid",
>- (rewrite_tac [GSYM REAL_INV_1OVER]
\\ `inv a <= inv (FST iv) <=> FST iv <= a`
by (match_mp_tac REAL_INV_LE_ANTIMONO \\ REAL_ASM_ARITH_TAC)
- \\ REAL_ASM_ARITH_TAC));
+ \\ REAL_ASM_ARITH_TAC)
+QED
Theorem iv_inv_preserves_valid:
∀ iv.
@@ -283,8 +296,9 @@ Proof
\\ irule SQRT_MONO_LE \\ gs[]
QED
-val interval_addition_valid = store_thm ("interval_addition_valid",
-``!iv1 iv2. validIntervalAdd iv1 iv2 (addInterval iv1 iv2)``,
+Theorem interval_addition_valid:
+ !iv1 iv2. validIntervalAdd iv1 iv2 (addInterval iv1 iv2)
+Proof
fs iv_ss \\ rpt strip_tac
(* First subgoal, lower bound *)
>- (`FST iv1 + FST iv2 <= a + b`
@@ -295,37 +309,43 @@ fs iv_ss \\ rpt strip_tac
>- (`a + b <= SND iv1 + SND iv2`
by (match_mp_tac REAL_LE_ADD2 \\ fs []) \\
match_mp_tac REAL_LE_TRANS \\
- HINT_EXISTS_TAC \\ strip_tac \\ fs [REAL_LE_MAX]));
+ HINT_EXISTS_TAC \\ strip_tac \\ fs [REAL_LE_MAX])
+QED
-val iv_add_preserves_valid = store_thm ("iv_add_preserves_valid",
- ``!iv1 iv2.
+Theorem iv_add_preserves_valid:
+ !iv1 iv2.
valid iv1 /\ valid iv2 ==>
- valid (addInterval iv1 iv2)``,
+ valid (addInterval iv1 iv2)
+Proof
fs [valid_def, addInterval_def, IVlo_def, IVhi_def, absIntvUpd_def, min4_def, max4_def]
\\ rpt strip_tac
\\ match_mp_tac REAL_LE_TRANS
\\ qexists_tac `FST iv1 + FST iv2` \\ fs [REAL_MIN_LE1]
\\ match_mp_tac REAL_LE_TRANS
- \\ qexists_tac `FST iv1 + FST iv2` \\ fs [REAL_LE_MAX1]);
+ \\ qexists_tac `FST iv1 + FST iv2` \\ fs [REAL_LE_MAX1]
+QED
-val interval_subtraction_valid = store_thm ("interval_subtraction_valid",
-``!iv1 iv2.
- validIntervalSub iv1 iv2 (subtractInterval iv1 iv2)``,
+Theorem interval_subtraction_valid:
+ !iv1 iv2. validIntervalSub iv1 iv2 (subtractInterval iv1 iv2)
+Proof
rpt gen_tac \\ Cases_on `iv2` \\ rewrite_tac (iv_ss @ [real_sub]) \\
rpt gen_tac \\ strip_tac \\
(** TODO: FIXME, use qspecl_then or sth else **)
match_mp_tac (REWRITE_RULE (iv_ss @ [FST,SND]) (SPECL [``iv1:interval``,``(-r,-q):interval``] interval_addition_valid)) \\
-fs []);
+fs []
+QED
-val iv_sub_preserves_valid = store_thm ("iv_sub_preserves_valid",
- ``!iv1 iv2.
+Theorem iv_sub_preserves_valid:
+ !iv1 iv2.
valid iv1 /\ valid iv2 ==>
- valid (subtractInterval iv1 iv2)``,
+ valid (subtractInterval iv1 iv2)
+Proof
once_rewrite_tac [subtractInterval_def]
\\ rpt strip_tac
\\ match_mp_tac iv_add_preserves_valid
\\ conj_tac \\ fs []
- \\ match_mp_tac iv_neg_preserves_valid \\ fs []);
+ \\ match_mp_tac iv_neg_preserves_valid \\ fs []
+QED
Theorem interval_multiplication_valid:
!iv1 iv2 a b.
@@ -456,63 +476,77 @@ rpt gen_tac \\ Cases_on `iv2` \\ rewrite_tac (iv_ss @ [real_div, REAL_MUL_LID])
(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",
- ``!iv1 iv2.
- valid iv1 /\ valid iv2 /\ (IVhi iv2 < 0 \/ 0 < IVlo iv2) ==>
- valid (divideInterval iv1 iv2)``,
+Theorem iv_div_preserves_valid:
+ !iv1 iv2.
+ valid iv1 /\ valid iv2 /\ (IVhi iv2 < 0 \/ 0 < IVlo iv2) ==>
+ valid (divideInterval iv1 iv2)
+Proof
once_rewrite_tac [divideInterval_def]
\\ rpt strip_tac
\\ match_mp_tac iv_mult_preserves_valid
\\ fs []
\\ match_mp_tac iv_inv_preserves_valid
- \\ fs []);
+ \\ fs []
+QED
(** Properties of the maxAbs function **)
-val contained_leq_maxAbs = store_thm ("contained_leq_maxAbs",
- ``!a iv. contained a iv ==> abs a <= maxAbs iv``,
- rpt strip_tac\\ fs iv_ss \\ match_mp_tac maxAbs \\ fs []);
+Theorem contained_leq_maxAbs:
+ !a iv. contained a iv ==> abs a <= maxAbs iv
+Proof
+ rpt strip_tac\\ fs iv_ss \\ match_mp_tac maxAbs \\ fs []
+QED
-val contained_leq_maxAbs_val = store_thm ("contained_leq_maxAbs_val",
- ``!a iv. contained a iv ==> a <= maxAbs iv``,
+Theorem contained_leq_maxAbs_val:
+ !a iv. contained a iv ==> a <= maxAbs iv
+Proof
rpt strip_tac \\ fs iv_ss \\
`abs a <= max (abs (FST iv)) (abs (SND iv))`
by (match_mp_tac (REWRITE_RULE iv_ss contained_leq_maxAbs) \\ fs []) \\
- REAL_ASM_ARITH_TAC);
+ REAL_ASM_ARITH_TAC
+QED
-val contained_leq_maxAbs_neg_val = store_thm ("contained_leq_maxAbs_neg_val",
- ``!a iv. contained a iv ==> - a <= maxAbs iv``,
+Theorem contained_leq_maxAbs_neg_val:
+ !a iv. contained a iv ==> - a <= maxAbs iv
+Proof
rpt strip_tac\\ fs iv_ss \\
`abs a <= max (abs (FST iv)) (abs (SND iv))` by (match_mp_tac (REWRITE_RULE iv_ss contained_leq_maxAbs) \\ fs []) \\
- REAL_ASM_ARITH_TAC);
+ REAL_ASM_ARITH_TAC
+QED
-val distance_gives_iv = store_thm ("distance_gives_iv",
- ``!a b e iv. contained a iv /\ abs (a - b) <= e ==> contained b (widenInterval iv e)``,
+Theorem distance_gives_iv:
+ !a b e iv. contained a iv /\ abs (a - b) <= e ==> contained b (widenInterval iv e)
+Proof
fs iv_ss \\ rpt strip_tac \\
`(b:real) - e <= a /\ a <= b + e` by REAL_ASM_ARITH_TAC \\
- REAL_ASM_ARITH_TAC);
+ REAL_ASM_ARITH_TAC
+QED
-val minAbs_positive_iv_is_lo = store_thm ("minAbs_positive_iv_is_lo",
- ``!(a b:real).
+Theorem minAbs_positive_iv_is_lo:
+ !(a b:real).
(0 < a) /\
- (a <= b) ==>
- (minAbsFun (a,b) = a)``,
+ (a <= b) ==>
+ (minAbsFun (a,b) = a)
+Proof
rpt (strip_tac) \\
fs[minAbsFun_def] \\
`abs a = a` by (fs[ABS_REFL] \\ REAL_ASM_ARITH_TAC) \\
`abs b = b` by (fs[ABS_REFL] \\ REAL_ASM_ARITH_TAC) \\
- metis_tac[REAL_MIN_ALT]);
+ metis_tac[REAL_MIN_ALT]
+QED
-val minAbs_negative_iv_is_hi = store_thm ("minAbs_negative_iv_is_hi",
- ``!(a b:real).
+Theorem minAbs_negative_iv_is_hi:
+ !(a b:real).
(b < 0) /\
(a <= b) ==>
- (minAbsFun (a,b) = - b)``,
+ (minAbsFun (a,b) = - b)
+Proof
rpt (strip_tac) \\
fs[minAbsFun_def] \\
`abs a = - a` by REAL_ASM_ARITH_TAC \\
`abs b = - b` by REAL_ASM_ARITH_TAC \\
ntac 2 (pop_assum (fn thm => rewrite_tac [thm])) \\
`-b <= -a` by fs[] \\
- metis_tac[REAL_MIN_ALT]);
+ metis_tac[REAL_MIN_ALT]
+QED
val _ = export_theory();
diff --git a/hol4/IntervalValidationScript.sml b/hol4/IntervalValidationScript.sml
index 74652b5653adfbb5759d857a6aad3661cb5651fc..59b0e6f711ae32b966076a6fa050cb4ba7d63623 100644
--- a/hol4/IntervalValidationScript.sml
+++ b/hol4/IntervalValidationScript.sml
@@ -18,9 +18,10 @@ 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``);
-val _ = temp_overload_on("min",``real$min``);
+
+Overload abs[local] = “real$absâ€
+Overload max[local] = “real$maxâ€
+Overload min[local] = “real$minâ€
(** Define a global iteration count for square roots **)
Definition ITERCOUNT_def:
@@ -618,24 +619,27 @@ Proof
\\ fs[valid_def, IVlo_def, IVhi_def])
QED
-val validIntervalbounds_noDivzero_real = store_thm("validIntervalbounds_noDivzero_real",
- ``!(f1 f2:real expr) A (P:precond) (dVars:num_set).
+Theorem validIntervalbounds_noDivzero_real:
+ !(f1 f2:real expr) A (P:precond) (dVars:num_set).
validIntervalbounds (Binop Div f1 f2) A P dVars ==>
?iv err.
FloverMapTree_find f2 A = SOME (iv,err) /\
- noDivzero (SND iv) (FST iv)``,
+ noDivzero (SND iv) (FST iv)
+Proof
rpt strip_tac \\ fs[Once validIntervalbounds_eq]
- \\ fs[noDivzero_def, IVhi_def, IVlo_def]);
+ \\ fs[noDivzero_def, IVhi_def, IVlo_def]
+QED
-val validRanges_validates_iv = store_thm (
- "validRanges_validates_iv",
- ``! e Gamma E A.
- validRanges e A E Gamma ==>
+Theorem validRanges_validates_iv:
+ ! e Gamma E A.
+ validRanges e A E Gamma ==>
? iv err.
FloverMapTree_find e A = SOME (iv, err) /\
- valid iv``,
+ valid iv
+Proof
Induct_on `e` \\ simp[Once validRanges_def]
\\ rpt strip_tac
- \\ fs[valid_def] \\ real_prove);
+ \\ fs[valid_def] \\ real_prove
+QED
val _ = export_theory();
diff --git a/hol4/RealIntervalInferenceScript.sml b/hol4/RealIntervalInferenceScript.sml
index ae49afea261295f055dfd8ef6c3409fbb7814d30..a310cfe24ecc26d7489ede1a3e1c4fd6152fb034 100644
--- a/hol4/RealIntervalInferenceScript.sml
+++ b/hol4/RealIntervalInferenceScript.sml
@@ -13,7 +13,8 @@ val _ = new_theory "RealIntervalInference";
val _ = monadsyntax.enable_monadsyntax();
val _ = List.app monadsyntax.enable_monad ["option"];
-val _ = type_abbrev ("ivMap", ``:(real # real) fMap``);
+
+Type ivMap = “:(real#real) fMapâ€;
Definition ITERCOUNT_def:
ITERCOUNT = 4:num
diff --git a/hol4/RealRangeArithScript.sml b/hol4/RealRangeArithScript.sml
index 0c68021cd384ad965b86151630acb9f068f68915..c1315e6bc755181391183de31ae8f421c5e68d06 100644
--- a/hol4/RealRangeArithScript.sml
+++ b/hol4/RealRangeArithScript.sml
@@ -1,25 +1,31 @@
+(**
+ Recursive correctness predicate for a range analysis with some supporting
+ theorems
+**)
open FloverTactics AbbrevsTheory RealSimpsTheory TypeValidatorTheory
ExpressionSemanticsTheory ssaPrgsTheory IntervalArithTheory CommandsTheory;
open preambleFloVer;
val _ = new_theory "RealRangeArith";
-val dVars_range_valid_def = Define `
+Definition dVars_range_valid_def:
dVars_range_valid (dVars:num_set) (E:num -> real option) (A:analysisResult) =
!(v:num). v IN domain dVars ==>
?vR iv err.
E v = SOME vR /\
(FloverMapTree_find ((Var v):real expr) A = SOME (iv, err)) /\
- (FST iv) <= vR /\ vR <= (SND iv)`;
+ (FST iv) <= vR /\ vR <= (SND iv)
+End
-val fVars_P_sound_def = Define `
+Definition fVars_P_sound_def:
fVars_P_sound (fVars:num_set) (E:env) (P:precond) =
!(v:num).
v IN domain fVars ==>
?vR. E v = SOME vR /\
- FST (P v) <= vR /\ vR <= SND (P v)`;
+ FST (P v) <= vR /\ vR <= SND (P v)
+End
-val validRanges_def = Define `
+Definition validRanges_def:
validRanges e A E Gamma =
((case e of
| Var x => T
@@ -45,30 +51,33 @@ val validRanges_def = Define `
(? iv err vR.
FloverMapTree_find e A = SOME (iv, err) /\
eval_expr E Gamma (toREval e) vR REAL /\
- (IVlo iv <= vR /\ vR <= IVhi iv)))`;
+ (IVlo iv <= vR /\ vR <= IVhi iv)))
+End
-val validRanges_single = store_thm (
- "validRanges_single",
- ``! e A E Gamma.
- validRanges e A E Gamma ==>
- ? iv err vR.
- FloverMapTree_find e A = SOME (iv, err) /\
- eval_expr E Gamma (toREval e) vR REAL /\
- (IVlo iv <= vR /\ vR <= IVhi iv)``,
+Theorem validRanges_single:
+ ! e A E Gamma.
+ validRanges e A E Gamma ==>
+ ? iv err vR.
+ FloverMapTree_find e A = SOME (iv, err) /\
+ eval_expr E Gamma (toREval e) vR REAL /\
+ (IVlo iv <= vR /\ vR <= IVhi iv)
+Proof
rpt strip_tac \\ Cases_on `e` \\ fs[Once validRanges_def]
- \\ find_exists_tac \\ fs[]);
+ \\ find_exists_tac \\ fs[]
+QED
-val validRanges_swap = store_thm (
- "validRanges_swap",
- ``! Gamma1 Gamma2 e A E.
+Theorem validRanges_swap:
+ ! Gamma1 Gamma2 e A E.
(! n. Gamma1 n = Gamma2 n) /\
validRanges e A E Gamma1 ==>
- validRanges e A E Gamma2``,
+ validRanges e A E Gamma2
+Proof
Induct_on `e` \\ simp[Once validRanges_def] \\ rpt strip_tac
\\ simp[Once validRanges_def]
- \\ rpt conj_tac \\ metis_tac []);
+ \\ rpt conj_tac \\ metis_tac []
+QED
-val validRangesCmd_def = Define `
+Definition validRangesCmd_def:
validRangesCmd f A E Gamma =
((case f of
| Let m x e g =>
@@ -79,25 +88,28 @@ val validRangesCmd_def = Define `
? iv_e err_e vR.
FloverMapTree_find (getRetExp f) A = SOME (iv_e, err_e) /\
bstep (toREvalCmd f) E Gamma vR REAL /\
- (IVlo iv_e <= vR /\ vR <= IVhi iv_e))`;
+ (IVlo iv_e <= vR /\ vR <= IVhi iv_e))
+End
-val validRangesCmd_single = store_thm (
- "validRangesCmd_single",
- ``! f A E Gamma.
+Theorem validRangesCmd_single:
+ ! f A E Gamma.
validRangesCmd f A E Gamma ==>
? iv_e err_e vR.
FloverMapTree_find (getRetExp f) A = SOME (iv_e, err_e) /\
bstep (toREvalCmd f) E Gamma vR REAL /\
- (IVlo iv_e <= vR /\ vR <= IVhi iv_e)``,
- Cases_on `f` \\ simp[Once validRangesCmd_def] \\ metis_tac[]);
+ (IVlo iv_e <= vR /\ vR <= IVhi iv_e)
+Proof
+ Cases_on `f` \\ simp[Once validRangesCmd_def] \\ metis_tac[]
+QED
-val validRangesCmd_swap = store_thm (
- "validRangesCmd_swap",
- ``! f A E Gamma1 Gamma2.
+Theorem validRangesCmd_swap:
+ ! f A E Gamma1 Gamma2.
(! n. Gamma1 n = Gamma2 n) /\
validRangesCmd f A E Gamma1 ==>
- validRangesCmd f A E Gamma2``,
+ validRangesCmd f A E Gamma2
+Proof
Induct_on `f` \\ simp[Once validRangesCmd_def] \\ rpt strip_tac
- \\ simp[Once validRangesCmd_def] \\ rpt conj_tac \\ metis_tac[]);
+ \\ simp[Once validRangesCmd_def] \\ rpt conj_tac \\ metis_tac[]
+QED
val _ = export_theory();
diff --git a/hol4/TypeValidatorScript.sml b/hol4/TypeValidatorScript.sml
index 4e6676a30108e16321bd4a434f8045f9f076faa5..d067079b480ec5f6ccd210062e8890fac5794a7b 100644
--- a/hol4/TypeValidatorScript.sml
+++ b/hol4/TypeValidatorScript.sml
@@ -1,3 +1,7 @@
+(**
+ Simple Type Inference algorithm with correctness proof to infer machine type
+ assignments for FloVer's input expressions
+**)
open realTheory realLib sptreeTheory;
open ExpressionsTheory MachineTypeTheory FloverTactics ExpressionAbbrevsTheory
ExpressionSemanticsTheory CommandsTheory FloverMapTheory ResultsTheory;
@@ -57,32 +61,35 @@ Proof
\\ rpt (asm_exists_tac \\ fs[])
QED
-val validTypes_exec = store_thm (
- "validTypes_exec",
- ``! e Gamma m.
+Theorem validTypes_exec:
+ ! e Gamma m.
validTypes e Gamma /\
FloverMapTree_find e Gamma = SOME m ==>
! E v mG.
eval_expr E (toRExpMap Gamma) e v mG ==>
- mG = m``,
+ mG = m
+Proof
rpt strip_tac \\ IMP_RES_TAC validTypes_single
\\ rename1 `FloverMapTree_find e Gamma = SOME mG2`
\\ `m = mG2` by (fs[])
\\ rveq
\\ first_x_assum irule
- \\ qexistsl_tac [`E`, `Gamma`, `v`] \\ fs[]);
+ \\ qexistsl_tac [`E`, `Gamma`, `v`] \\ fs[]
+QED
-val isMonotone_def = Define `
+Definition isMonotone_def:
isMonotone NONE mNew = T /\
- isMonotone (SOME mOld) mNew = (mOld = mNew)`;
+ isMonotone (SOME mOld) mNew = (mOld = mNew)
+End
-val addMono_def = Define `
+Definition addMono_def:
addMono e m map =
case FloverMapTree_find e map of
| SOME mOld => Fail "Nonmonotonic map update"
- | NONE => Succes (FloverMapTree_insert e m map)`;
+ | NONE => Succes (FloverMapTree_insert e m map)
+End
-val _ = Parse.temp_overload_on ("insert", Term`FloverMapTree_insert`);
+Overload insert[local] = “FloverMapTree_insertâ€
Definition getValidMap_def:
getValidMap Gamma e akk =
@@ -206,11 +213,11 @@ End
val tMap_def = FloverMapTree_correct;
-val toRExpMap_char = store_thm (
- "toRExpMap_char",
- ``!e m akk.
- toRExpMap (FloverMapTree_insert e m akk) e = SOME m``,
- fs[toRExpMap_def, tMap_def]);
+Theorem toRExpMap_char:
+ !e m akk. toRExpMap (FloverMapTree_insert e m akk) e = SOME m
+Proof
+ fs[toRExpMap_def, tMap_def]
+QED
val by_monotonicity =
once_rewrite_tac [map_find_add]
@@ -310,13 +317,13 @@ Proof
\\ by_monotonicity
QED
-val validTypes_mono = store_thm (
- "validTypes_mono",
- ``! e map1 map2.
+Theorem validTypes_mono:
+ ! e map1 map2.
(! e m. FloverMapTree_find e map1 = SOME m ==>
FloverMapTree_find e map2 = SOME m) /\
validTypes e map1 ==>
- validTypes e map2``,
+ validTypes e map2
+Proof
Induct_on `e` \\ fs[Once validTypes_def]
\\ rpt strip_tac
\\ simp [Once validTypes_def]
@@ -358,16 +365,18 @@ val validTypes_mono = store_thm (
\\ qexists_tac `map1` \\ simp[GSYM validTypes_def])
>- (qexists_tac `m1` \\ fs[])
\\ rpt strip_tac \\ first_x_assum irule
- \\ qexistsl_tac [`E`, `Gamma2`, `v`] \\ fs[]);
+ \\ qexistsl_tac [`E`, `Gamma2`, `v`] \\ fs[]
+QED
-val map_find_mono = store_thm (
- "map_find_mono",
- ``! e1 e2 m1 m2 Gamma.
- FloverMapTree_mem e2 Gamma = F /\
- FloverMapTree_find e1 Gamma = SOME m1 ==>
- FloverMapTree_find e1 (FloverMapTree_insert e2 m2 Gamma) = SOME m1``,
+Theorem map_find_mono:
+ ! e1 e2 m1 m2 Gamma.
+ FloverMapTree_mem e2 Gamma = F /\
+ FloverMapTree_find e1 Gamma = SOME m1 ==>
+ FloverMapTree_find e1 (FloverMapTree_insert e2 m2 Gamma) = SOME m1
+Proof
rpt strip_tac \\ fs[map_find_add]
- \\ Cases_on `e1 = e2` \\ fs[FloverMapTree_mem_def]);
+ \\ Cases_on `e1 = e2` \\ fs[FloverMapTree_mem_def]
+QED
Theorem getValidMap_correct:
∀ e Gamma akk res.
@@ -799,11 +808,11 @@ Proof
\\ fs[eval_expr_cases, toRExpMap_def] \\ rveq \\ fs[]
QED
-val getValidMap_top_contained = store_thm (
- "getValidMap_top_contained",
- ``! e akk Gamma res.
+Theorem getValidMap_top_contained:
+ ! e akk Gamma res.
getValidMap Gamma e akk = Succes res ==>
- FloverMapTree_mem e res``,
+ FloverMapTree_mem e res
+Proof
Induct_on `e` \\ simp[Once getValidMap_def] \\ rpt strip_tac
>- (EVERY_CASE_TAC \\ rveq \\ fs[FloverMapTree_mem_def, map_find_add])
>- (EVERY_CASE_TAC \\ rveq \\ fs[FloverMapTree_mem_def, map_find_add])
@@ -826,17 +835,19 @@ val getValidMap_top_contained = store_thm (
\\ Cases_on `getValidMap Gamma e akk` \\ fs[]
\\ res_tac
\\ fs[addMono_def]
- \\ EVERY_CASE_TAC \\ rveq \\ fs[FloverMapTree_mem_def, map_find_add]);
+ \\ EVERY_CASE_TAC \\ rveq \\ fs[FloverMapTree_mem_def, map_find_add]
+QED
-val getValidMap_top_correct = store_thm (
- "getValidMap_top_correct",
- ``! e akk Gamma res.
+Theorem getValidMap_top_correct:
+ ! e akk Gamma res.
(! e. FloverMapTree_mem e akk ==> validTypes e akk) /\
getValidMap Gamma e akk = Succes res ==>
- validTypes e res``,
- metis_tac[getValidMap_correct, getValidMap_top_contained]);
+ validTypes e res
+Proof
+ metis_tac[getValidMap_correct, getValidMap_top_contained]
+QED
-val validTypesCmd_def = Define `
+Definition validTypesCmd_def:
validTypesCmd f Gamma =
((case f of
| Let m x e g =>
@@ -853,11 +864,11 @@ val validTypesCmd_def = Define `
(! e m. FloverMapTree_find e Gamma = SOME m ==>
FloverMapTree_find e Gamma2 = SOME m) /\
bstep f E (toRExpMap Gamma2) v m ==>
- m = mT))`;
+ m = mT))
+End
-val validTypesCmd_single = store_thm (
- "validTypesCmd_single",
- ``! f Gamma.
+Theorem validTypesCmd_single:
+ ! f Gamma.
validTypesCmd f Gamma ==>
? mT.
FloverMapTree_find (getRetExp f) Gamma = SOME mT /\
@@ -865,10 +876,12 @@ val validTypesCmd_single = store_thm (
(! e m. FloverMapTree_find e Gamma = SOME m ==>
FloverMapTree_find e Gamma2 = SOME m) /\
bstep f E (toRExpMap Gamma2) v m ==>
- m = mT``,
- Cases_on `f` \\ simp[Once validTypesCmd_def] \\ rpt strip_tac \\ metis_tac[]);
+ m = mT
+Proof
+ Cases_on `f` \\ simp[Once validTypesCmd_def] \\ rpt strip_tac \\ metis_tac[]
+QED
-val getValidMapCmd_def = Define `
+Definition getValidMapCmd_def:
getValidMapCmd Gamma (Let m x e g) akk =
do
res_e <- getValidMap Gamma e akk;
@@ -883,14 +896,15 @@ val getValidMapCmd_def = Define `
od
else Fail "Incorrect type for let-bound variable"
od /\
- getValidMapCmd Gamma (Ret e) akk = getValidMap Gamma e akk`;
+ getValidMapCmd Gamma (Ret e) akk = getValidMap Gamma e akk
+End
-val getValidMapCmd_mono = store_thm (
- "getValidMapCmd_mono",
- ``! f Gamma akk res.
+Theorem getValidMapCmd_mono:
+ ! f Gamma akk res.
getValidMapCmd Gamma f akk = Succes res ==>
! e m. FloverMapTree_find e akk = SOME m ==>
- FloverMapTree_find e res = SOME m``,
+ FloverMapTree_find e res = SOME m
+Proof
Induct_on `f` \\ simp[Once getValidMapCmd_def]
THENL [ ALL_TAC , MATCH_ACCEPT_TAC getValidMap_mono]
\\ rpt strip_tac
@@ -907,17 +921,18 @@ val getValidMapCmd_mono = store_thm (
by (irule getValidMap_mono \\ qexistsl_tac [`Gamma`, `akk`, `e`]
\\ fs[])
\\ fs[])
- \\ irule getValidMap_mono \\ ntac 2 (find_exists_tac \\ fs[]));
+ \\ irule getValidMap_mono \\ ntac 2 (find_exists_tac \\ fs[])
+QED
-val getValidMapCmd_correct = store_thm (
- "getValidMapCmd_correct",
- ``! f Gamma akk res.
+Theorem getValidMapCmd_correct:
+ ! f Gamma akk res.
(! e. FloverMapTree_mem e akk ==>
validTypes e akk) /\
getValidMapCmd Gamma f akk = Succes res ==>
validTypesCmd f res /\
(! e. FloverMapTree_mem e res ==>
- validTypes e res)``,
+ validTypes e res)
+Proof
Induct_on `f` \\ simp[getValidMapCmd_def]
\\ rpt gen_tac \\ rpt (disch_then assume_tac) \\ fs[]
>- (Cases_on `getValidMap Gamma e akk` \\ fs[option_case_eq]
@@ -966,7 +981,8 @@ val getValidMapCmd_correct = store_thm (
\\ IMP_RES_TAC validTypes_single
\\ qexists_tac `mG` \\ fs[getRetExp_def]
\\ rpt strip_tac \\ fs[bstep_cases]
- \\ first_x_assum irule \\ ntac 2 (find_exists_tac \\ fs[]));
+ \\ first_x_assum irule \\ ntac 2 (find_exists_tac \\ fs[])
+QED
Theorem validTypes_defined_usedVars:
∀ e Gamma.
diff --git a/hol4/binary/checkerBinaryScript.sml b/hol4/binary/checkerBinaryScript.sml
index bdbff08ce73130e33f796878a2f3875385719227..1fdfa7c30fa7857da17a482576031099bd3a288e 100644
--- a/hol4/binary/checkerBinaryScript.sml
+++ b/hol4/binary/checkerBinaryScript.sml
@@ -2,9 +2,11 @@ open preambleFloVer compilationLib transTheory
val _ = new_theory "checkerBinary"
+ (*
val checker_compiled = save_thm("checker_compiled",
compile_x64
"checker"
main_prog_def);
+*)
val _ = export_theory ();
diff --git a/hol4/binary/transScript.sml b/hol4/binary/transScript.sml
index a8a278464798d38102d69e1d333a9c813916da25..51a5026c250f01bb9dff17241b061f5299038dae 100644
--- a/hol4/binary/transScript.sml
+++ b/hol4/binary/transScript.sml
@@ -11,6 +11,7 @@ val _ = new_theory "trans";
val _ = translation_extends "basisProg";
+(*
val _ = temp_overload_on("abs",``real$abs``);
val _ = temp_overload_on("max",``real$max``);
val _ = temp_overload_on("min",``real$min``);
@@ -509,5 +510,6 @@ val main_semantics =
|> DISCH_ALL |> Q.GENL[`cl`,`contents`]
|> SIMP_RULE(srw_ss())[AND_IMP_INTRO,GSYM CONJ_ASSOC]
|> curry save_thm "main_semantics";
+*)
val _ = export_theory();
diff --git a/hol4/divisionRework.sml b/hol4/divisionRework.sml
new file mode 100644
index 0000000000000000000000000000000000000000..b76e4b9cb41a20f5002e2de62655f3e25c8cb1fb
--- /dev/null
+++ b/hol4/divisionRework.sml
@@ -0,0 +1,1034 @@
+Theorem divisionErrorBounded:
+ !(e1lo e1hi nR1 e2lo e2hi nR2 nF1 nF2 err1 err2:real).
+ (e1lo <= nR1) /\ (nR1 <= e1hi) /\
+ (e2lo <= nR2) /\ (nR2 <= e2hi) /\
+ abs (nR1 − nF1) <= err1 /\
+ abs (nR2 − nF2) <= err2 /\
+ 0 <= err1 /\
+ 0 <= err2 /\
+ contained nF1 (widenInterval (e1lo,e1hi) err1) /\
+ contained nF2 (widenInterval (e2lo,e2hi) err2) /\
+ noDivzero e2hi e2lo /\
+ noDivzero (SND (widenInterval (e2lo,e2hi) err2))
+ (FST (widenInterval (e2lo,e2hi) err2)) ==>
+ abs (nR1 / nR2 − nF1 / nF2) ≤
+ maxAbs (e1lo,e1hi) *
+ (1 /
+ (minAbsFun (widenInterval (e2lo,e2hi) err2) *
+ minAbsFun (widenInterval (e2lo,e2hi) err2)) * err2) +
+ maxAbs (invertInterval (e2lo,e2hi)) * err1 +
+ err1 *
+ (1 /
+ (minAbsFun (widenInterval (e2lo,e2hi) err2) *
+ minAbsFun (widenInterval (e2lo,e2hi) err2)) * err2)
+Proof
+ rpt strip_tac
+ \\ `contained (inv nR2) (invertInterval (e2lo, e2hi))`
+ by (irule interval_inversion_valid \\ conj_tac
+ \\ fs[contained_def, IVlo_def, IVhi_def, noDivzero_def])
+ \\ `contained (inv nF2) (invertInterval (widenInterval (e2lo, e2hi) err2))`
+ by (irule interval_inversion_valid \\ conj_tac
+ \\ fs[contained_def, IVlo_def, IVhi_def, noDivzero_def])
+ \\ `nR1 <= maxAbs (e1lo, e1hi)`
+ by (irule contained_leq_maxAbs_val
+ \\ fs[contained_def, IVlo_def, IVhi_def])
+ \\ `inv nR2 <= maxAbs (invertInterval(e2lo, e2hi))`
+ by (irule contained_leq_maxAbs_val
+ \\ fs[contained_def, IVlo_def, IVhi_def])
+ \\ `-nR1 <= maxAbs (e1lo, e1hi)`
+ by (irule contained_leq_maxAbs_neg_val
+ \\ fs[contained_def, IVlo_def, IVhi_def])
+ \\ `- inv nR2 <= maxAbs (invertInterval (e2lo, e2hi))`
+ by (irule contained_leq_maxAbs_neg_val
+ \\ fs[contained_def, IVlo_def, IVhi_def])
+ \\ `nR1 * err2 <= maxAbs (e1lo, e1hi) * err2`
+ by (irule REAL_LE_RMUL_IMP \\ fs[])
+ \\ `-nR1 * err2 <= maxAbs (e1lo, e1hi) * err2`
+ by (irule REAL_LE_RMUL_IMP \\ fs[])
+ \\ `inv nR2 * err1 <= maxAbs (invertInterval(e2lo, e2hi)) * err1`
+ by (irule REAL_LE_RMUL_IMP \\ fs[])
+ \\ `- inv nR2 * err1 <= maxAbs (invertInterval(e2lo, e2hi)) * err1`
+ by (irule REAL_LE_RMUL_IMP \\ fs[])
+ \\ `- (err1 * err2) <= err1 * err2`
+ by (rewrite_tac[REAL_NEG_LMUL] \\ irule REAL_LE_RMUL_IMP
+ \\ REAL_ASM_ARITH_TAC)
+ \\ `0 <= maxAbs (e1lo, e1hi) * err2` by REAL_ASM_ARITH_TAC
+ \\ `0 <= maxAbs (invertInterval (e2lo, e2hi)) * err1` by REAL_ASM_ARITH_TAC
+ \\ `maxAbs (e1lo, e1hi) * err2 <=
+ maxAbs (e1lo, e1hi) * err2 + maxAbs (invertInterval (e2lo, e2hi)) * err1`
+ by (REAL_ASM_ARITH_TAC)
+ \\ `maxAbs (e1lo, e1hi) * err2 + maxAbs (invertInterval(e2lo, e2hi)) * err1 <=
+ maxAbs (e1lo, e1hi) * err2 + maxAbs (invertInterval (e2lo, e2hi)) * err1 + err1 * err2`
+ by REAL_ASM_ARITH_TAC
+ \\ ntac 2 (first_x_assum (fn thm1 => (mp_then Any assume_tac REAL_LE_ABS_TRANS thm1 \\ mp_tac thm1)))
+ \\ rpt strip_tac
+ (* Case distinction for divisor range
+ positive or negative in float and real valued execution *)
+ \\ fs [IVlo_def, IVhi_def, widenInterval_def, contained_def, noDivzero_def]
+ (* Solve trivial, bogus cases *)
+ \\ TRY (`e2hi < e2lo` by REAL_ASM_ARITH_TAC \\ REAL_ASM_ARITH_TAC)
+ (* e2hi + err2 < 0, e2hi < 0;
+ The range of the divisor lies in the range from -infinity until 0 *)
+ >- (
+ `abs (inv nR2 - inv nF2) <= err2 * inv ((e2hi + err2) * (e2hi + err2))`
+ by (irule err_prop_inversion_neg \\ fs[] \\ qexists_tac `e2lo` \\ simp[])
+ \\ fs [widenInterval_def, IVlo_def, IVhi_def]
+ \\ `minAbsFun (e2lo - err2, e2hi + err2) = - (e2hi + err2)`
+ by (irule minAbs_negative_iv_is_hi \\ REAL_ASM_ARITH_TAC)
+ \\ simp[]
+ \\ qpat_x_assum `minAbsFun _ = _ ` kall_tac
+ \\ `nF1 <= nR1 + err1` by REAL_ASM_ARITH_TAC
+ \\ `nR1 - err1 <= nF1` by REAL_ASM_ARITH_TAC
+ \\ `(0 < nR2 - nF2 /\ nR2 - nF2 <= err2) \/ (nR2 - nF2 <= 0 /\ - (nR2 - nF2) <= err2)`
+ by REAL_ASM_ARITH_TAC
+ (* 0 < nR2 - nF2; nR2 - nF2 ≤ err2 *)
+ >- (
+ `nF2 < nR2` by REAL_ASM_ARITH_TAC
+ \\ qpat_x_assum `nF2 < nR2` (fn thm => assume_tac (ONCE_REWRITE_RULE [GSYM REAL_LT_NEG] thm))
+ \\ `inv (- nF2) < inv (- nR2)` by (irule REAL_LT_INV \\ REAL_ASM_ARITH_TAC)
+ \\ `inv (- nF2) = - (inv nF2)` by (irule (GSYM REAL_NEG_INV) \\ REAL_ASM_ARITH_TAC)
+ \\ `inv (- nR2) = - (inv nR2)` by (irule (GSYM REAL_NEG_INV) \\ REAL_ASM_ARITH_TAC)
+ \\ rpt (qpat_x_assum `inv (- _) = - (inv _)`
+ (fn thm => rule_assum_tac (fn hyp => REWRITE_RULE [thm] hyp)))
+ \\ `inv nR2 < inv nF2` by REAL_ASM_ARITH_TAC
+ \\ qpat_x_assum `- _ < - _` kall_tac
+ \\ `inv nR2 - inv nF2 < 0` by REAL_ASM_ARITH_TAC
+ \\ `- (nR2â»Â¹ − nF2â»Â¹) ≤ err2 * ((e2hi + err2) * (e2hi + err2))â»Â¹`
+ by (fs[] \\ REAL_ASM_ARITH_TAC)
+ \\ `inv nF2 <= inv nR2 + err2 * inv ((e2hi + err2) * (e2hi + err2))`
+ by REAL_ASM_ARITH_TAC
+ \\ `inv nR2 - err2 * inv ((e2hi + err2) * (e2hi + err2)) <= inv nF2`
+ by REAL_ASM_ARITH_TAC
+ (* Next do a case distinction for the absolute value *)
+ \\ `! (x:real). ((abs x = x) /\ 0 <= x) \/ ((abs x = - x) /\ x < 0)` by REAL_ASM_ARITH_TAC
+ \\ qpat_x_assum `!x. A /\ B \/ C`
+ (qspec_then `(nR1:real / nR2:real) - (nF1:real / nF2:real)`
+ DISJ_CASES_TAC)
+ \\ fs[realTheory.abs]
+ (* 0 ≤ nR1 / nR2 - nF1 / nF2 *)
+ >- (
+ fs[real_sub, real_div]
+ \\ qspecl_then [`nF1`, `0`] DISJ_CASES_TAC REAL_LTE_TOTAL
+ (* nF1 < 0 *)
+ >- (
+ irule REAL_LE_TRANS
+ \\ qexists_tac `nR1 * inv nR2 + - nF1 * (inv nR2 + err2 * inv ((e2hi + err2) pow 2))`
+ \\ conj_tac
+ >- (
+ fs[REAL_LE_LADD] \\ rewrite_tac [REAL_NEG_LMUL]
+ \\ irule REAL_LE_LMUL_IMP \\ conj_tac \\ REAL_ASM_ARITH_TAC)
+ \\ qabbrev_tac `err_inv = err2 * inv ((e2hi + err2) pow 2)`
+ \\ qspecl_then [`inv nR2 + err_inv`, `0`] DISJ_CASES_TAC REAL_LTE_TOTAL
+ (* inv nR2 + err_inv < 0 *)
+ >- (irule REAL_LE_TRANS
+ \\ qexists_tac `nR1 * inv nR2 + - (nR1 + err1) * (inv nR2 + err_inv)`
+ \\ conj_tac
+ >- (fs [REAL_LE_ADD])
+ \\ real_rewrite `nR1 * inv nR2 + - (nR1 + err1) * (inv nR2 + err_inv) =
+ - nR1 * err_inv + - (inv nR2) * err1 - err1 * err_inv`
+ \\ rewrite_tac [real_sub, GSYM REAL_ADD_ASSOC]
+ \\ irule REAL_LE_ADD2 \\ conj_tac
+ >- (unabbrev_all_tac
+ \\ fs[REAL_POW_INV]
+ \\ once_rewrite_tac [REAL_NEG_LMUL]
+ \\ once_rewrite_tac [REAL_NEG_RMUL]
+ \\ rewrite_tac [GSYM REAL_MUL_ASSOC]
+ \\ irule REAL_LE_LMUL_IMP
+ \\ conj_tac \\ fs[]
+ \\ irule REAL_LE_RMUL_IMP \\ fs[])
+ \\ irule REAL_LE_ADD2 \\ conj_tac
+ >- (once_rewrite_tac [REAL_NEG_RMUL]
+ \\ real_rewrite `- (inv nR2) * err1 = err1 * - (inv nR2)`
+ \\ irule REAL_LE_LMUL_IMP
+ \\ conj_tac \\ fs[])
+ \\ unabbrev_all_tac
+ \\ fs[REAL_POW_INV]
+ \\ irule REAL_LE_TRANS \\ qexists_tac `0`
+ \\ conj_tac \\ fs[REAL_NEG_LE0, REAL_LE_MUL])
+ (* 0 ≤ inv nR2 + err_inv *)
+ \\ irule REAL_LE_TRANS
+ \\ qexists_tac `nR1 * inv nR2 + - (nR1 + - err1) * (inv nR2 + err_inv)`
+ \\ conj_tac
+ >- (fs [REAL_LE_ADD]
+ \\ irule REAL_LE_RMUL_IMP
+ \\ conj_tac \\ REAL_ASM_ARITH_TAC)
+ \\ real_rewrite `nR1 * inv nR2 + - (nR1 + - err1) * (inv nR2 + err_inv) =
+ - nR1 * err_inv + inv nR2 * err1 + err1 * err_inv`
+ \\ unabbrev_all_tac
+ \\ rewrite_tac [real_sub, GSYM REAL_ADD_ASSOC]
+ \\ irule REAL_LE_ADD2 \\ conj_tac
+ >- (rewrite_tac [GSYM REAL_MUL_ASSOC]
+ \\ real_rewrite `-nR1 * (err2 * (inv ((e2hi + err2) pow 2))) =
+ err2 * (-nR1 * (inv ((e2hi + err2) pow 2)))`
+ \\ irule REAL_LE_LMUL_IMP
+ \\ conj_tac \\ fs[REAL_POW_INV]
+ \\ irule REAL_LE_RMUL_IMP \\ fs[])
+ \\ irule REAL_LE_ADD2 \\ conj_tac
+ >- (real_rewrite `inv nR2 * err1 = err1 * inv nR2`
+ \\ irule REAL_LE_LMUL_IMP
+ \\ conj_tac \\ fs[])
+ \\ fs[REAL_POW_INV])
+ (* 0 ≤ nF1 *)
+ \\ irule REAL_LE_TRANS
+ \\ qexists_tac `nR1 * inv nR2 + - nF1 * (inv nR2 - err2 * inv ((e2hi + err2) pow 2))`
+ \\ conj_tac
+ >- (fs[REAL_LE_LADD]
+ \\ once_rewrite_tac [REAL_NEG_LMUL]
+ \\ irule REAL_MUL_LE_COMPAT_NEG_L
+ \\ conj_tac \\ REAL_ASM_ARITH_TAC)
+ \\ qabbrev_tac `err_inv = (err2 * inv ((e2hi + err2) pow 2))`
+ \\ qspecl_then [`inv nR2 - err_inv`, `0`] DISJ_CASES_TAC REAL_LTE_TOTAL
+ (* inv nR2 - err_inv < 0 *)
+ >- (irule REAL_LE_TRANS
+ \\ qexists_tac `nR1 * inv nR2 + - (nR1 + err1) * (inv nR2 - err_inv)`
+ \\ conj_tac
+ >- (fs [REAL_LE_ADD]
+ \\ once_rewrite_tac [REAL_MUL_COMM]
+ \\ irule REAL_MUL_LE_COMPAT_NEG_L
+ \\ conj_tac \\ TRY REAL_ASM_ARITH_TAC
+ \\ fs [REAL_LE_NEG])
+ \\ real_rewrite `nR1 * inv nR2 + - (nR1 + err1) * (inv nR2 - err_inv) =
+ nR1 * err_inv + - (inv nR2) * err1 + err1 * err_inv`
+ \\ qunabbrev_tac `err_inv`
+ \\ irule REAL_LE_ADD2
+ \\ conj_tac \\ TRY REAL_ASM_ARITH_TAC
+ \\ irule REAL_LE_ADD2
+ \\ conj_tac \\ TRY REAL_ASM_ARITH_TAC
+ \\ real_rewrite `err2 * maxAbs (e1lo, e1hi) = maxAbs (e1lo, e1hi) * err2`
+ \\ rewrite_tac [GSYM REAL_MUL_ASSOC]
+ \\ irule REAL_LE_RMUL_IMP
+ \\ fs[REAL_LE_POW2, REAL_LE_MUL])
+ (* 0 ≤ inv nR2 - err_inv *)
+ \\ irule REAL_LE_TRANS
+ \\ qexists_tac `nR1 * inv nR2 + - (nR1 - err1) * (inv nR2 - err_inv)`
+ \\ conj_tac
+ >- (fs [REAL_LE_ADD]
+ \\ irule REAL_LE_RMUL_IMP
+ \\ conj_tac \\ REAL_ASM_ARITH_TAC)
+ \\ real_rewrite `nR1 * inv nR2 + - (nR1 - err1) * (inv nR2 - err_inv) =
+ nR1 * err_inv + inv nR2 * err1 + - err1 * err_inv`
+ \\ qunabbrev_tac `err_inv`
+ \\ irule REAL_LE_ADD2 \\ conj_tac
+ >- (
+ irule REAL_LE_ADD2 \\ conj_tac \\ TRY REAL_ASM_ARITH_TAC
+ \\ real_rewrite `err2 * maxAbs (e1lo, e1hi) = maxAbs (e1lo, e1hi) * err2`
+ \\ rewrite_tac [GSYM REAL_MUL_ASSOC]
+ \\ irule REAL_LE_RMUL_IMP
+ \\ fs[REAL_LE_POW2, REAL_LE_MUL])
+ \\ irule REAL_LE_TRANS \\ qexists_tac `0`
+ \\ fs[REAL_LE_POW2, REAL_LE_MUL])
+ (* nR1 / nR2 - nF1 / nF2 < 0; Absolute value negative *)
+ \\ fs[real_sub, real_div]
+ \\ qspecl_then [`nF1`, `0`] DISJ_CASES_TAC REAL_LTE_TOTAL
+ (* nF1 < 0 *)
+ >- (
+ irule REAL_LE_TRANS
+ \\ qexists_tac `- nR1 * inv nR2 + nF1 * (inv nR2 - err2 * inv ((e2hi + err2) pow 2))`
+ \\ conj_tac
+ >- (once_rewrite_tac [REAL_NEG_ADD, GSYM REAL_NEG_LMUL]
+ \\ fs[REAL_LE_LADD, real_sub])
+ \\ qabbrev_tac `err_inv = err2 * inv ((e2hi + err2) pow 2)`
+ \\ qspecl_then [`inv nR2 - err_inv`, `0`] DISJ_CASES_TAC REAL_LTE_TOTAL
+ (* inv nR2 - err_inv < 0 *)
+ >- (irule REAL_LE_TRANS
+ \\ qexists_tac `- nR1 * inv nR2 + (nR1 - err1) * (inv nR2 - err_inv)`
+ \\ conj_tac
+ >- (fs [REAL_LE_ADD, real_sub])
+ \\ real_rewrite `- nR1 * inv nR2 + (nR1 - err1) * (inv nR2 - err_inv) =
+ - nR1 * err_inv + - (inv nR2) * err1 + err1 * err_inv`
+ \\ qunabbrev_tac `err_inv`
+ \\ irule REAL_LE_ADD2
+ \\ conj_tac \\ TRY REAL_ASM_ARITH_TAC
+ \\ irule REAL_LE_ADD2
+ \\ conj_tac \\ TRY REAL_ASM_ARITH_TAC
+ \\ real_rewrite `err2 * maxAbs (e1lo, e1hi) = maxAbs (e1lo, e1hi) * err2`
+ \\ rewrite_tac [GSYM REAL_MUL_ASSOC]
+ \\ irule REAL_LE_RMUL_IMP
+ \\ fs[REAL_LE_POW2, REAL_LE_MUL])
+ (* 0 ≤ inv nR2 - err_inv *)
+ \\ irule REAL_LE_TRANS
+ \\ qexists_tac `- nR1 * inv nR2 + (nR1 + err1) * (inv nR2 - err_inv)`
+ \\ conj_tac
+ >- (fs [REAL_LE_ADD]
+ \\ irule REAL_LE_RMUL_IMP
+ \\ conj_tac \\ REAL_ASM_ARITH_TAC)
+ \\ real_rewrite `- nR1 * inv nR2 + (nR1 + err1) * (inv nR2 - err_inv) =
+ - nR1 * err_inv + inv nR2 * err1 - err1 * err_inv`
+ \\ qunabbrev_tac `err_inv` \\ rewrite_tac [real_sub]
+ \\ irule REAL_LE_ADD2 \\ conj_tac
+ >- (irule REAL_LE_ADD2
+ \\ conj_tac \\ TRY REAL_ASM_ARITH_TAC
+ \\ fs [GSYM REAL_NEG_ADD, REAL_NEG_MUL2, REAL_POW_INV]
+ \\ once_rewrite_tac [REAL_NEG_LMUL]
+ \\ once_rewrite_tac [REAL_NEG_RMUL]
+ \\ rewrite_tac [GSYM REAL_MUL_ASSOC]
+ \\ irule REAL_LE_LMUL_IMP
+ \\ conj_tac \\ TRY REAL_ASM_ARITH_TAC
+ \\ irule REAL_LE_RMUL_IMP
+ \\ fs[REAL_LE_POW2, REAL_LE_MUL])
+ \\ irule REAL_LE_TRANS \\ qexists_tac `0`
+ \\ fs[REAL_LE_POW2, REAL_LE_MUL])
+ (* 0 <= nF1 *)
+ \\ irule REAL_LE_TRANS
+ \\ qexists_tac `- nR1 * inv nR2 + nF1 * (inv nR2 + err2 * inv ((e2hi + err2) pow 2))`
+ \\ conj_tac
+ >- (fs[REAL_LE_LADD, REAL_NEG_ADD]
+ \\ irule REAL_LE_LMUL_IMP \\ REAL_ASM_ARITH_TAC)
+ \\ qabbrev_tac `err_inv = (err2 * inv ((e2hi + err2) pow 2))`
+ \\ qspecl_then [`inv nR2 + err_inv`, `0`] DISJ_CASES_TAC REAL_LTE_TOTAL
+ (* inv nR2 + err_inv < 0 *)
+ >- (irule REAL_LE_TRANS
+ \\ qexists_tac `-nR1 * inv nR2 + (nR1 - err1) * (inv nR2 + err_inv)`
+ \\ conj_tac
+ >- (fs [REAL_LE_ADD, real_sub])
+ \\ real_rewrite `- nR1 * inv nR2 + (nR1 - err1) * (inv nR2 + err_inv) =
+ nR1 * err_inv + - (inv nR2) * err1 - err1 * err_inv`
+ \\ qunabbrev_tac `err_inv`
+ \\ simp[real_sub]
+ \\ irule REAL_LE_ADD2 \\ conj_tac
+ >- (irule REAL_LE_ADD2
+ \\ conj_tac \\ TRY REAL_ASM_ARITH_TAC
+ \\ rewrite_tac [GSYM REAL_MUL_ASSOC]
+ \\ irule REAL_LE_LMUL_IMP \\ fs[REAL_POW_INV]
+ \\ irule REAL_LE_RMUL_IMP
+ \\ fs[REAL_LE_POW2, REAL_LE_MUL])
+ \\ irule REAL_LE_TRANS \\ qexists_tac `0`
+ \\ fs[REAL_LE_POW2, REAL_LE_MUL])
+ (* 0 ≤ inv nR2 + err_inv *)
+ \\ irule REAL_LE_TRANS
+ \\ qexists_tac `- nR1 * inv nR2 + (nR1 + err1) * (inv nR2 + err_inv)`
+ \\ conj_tac
+ >- (fs [REAL_LE_ADD]
+ \\ irule REAL_LE_RMUL_IMP
+ \\ conj_tac \\ REAL_ASM_ARITH_TAC)
+ \\ real_rewrite `- nR1 * inv nR2 + (nR1 + err1) * (inv nR2 + err_inv) =
+ nR1 * err_inv + inv nR2 * err1 + err1 * err_inv`
+ \\ qunabbrev_tac `err_inv`
+ \\ irule REAL_LE_ADD2
+ \\ conj_tac \\ TRY REAL_ASM_ARITH_TAC
+ \\ irule REAL_LE_ADD2
+ \\ conj_tac \\ TRY REAL_ASM_ARITH_TAC
+ \\ real_rewrite `err2 * maxAbs (e1lo, e1hi) = maxAbs (e1lo, e1hi) * err2`
+ \\ rewrite_tac [GSYM REAL_MUL_ASSOC]
+ \\ irule REAL_LE_RMUL_IMP
+ \\ fs[REAL_LE_POW2, REAL_LE_MUL])
+ (* - (nR2 - nF2) ≤ err2; nR2 - nF2 < 0;
+ Absolute value negative *)
+ \\ fs [GSYM REAL_NEG_ADD, REAL_NEG_MUL2]
+ \\ `nR2 <= nF2` by REAL_ASM_ARITH_TAC
+ \\ qpat_x_assum `nR2 <= nF2` (fn thm => assume_tac (ONCE_REWRITE_RULE [GSYM REAL_LE_NEG] thm))
+ \\ `inv (- nR2) <= inv (- nF2)` by (irule REAL_INV_LE_ANTIMONO_IMPR \\ REAL_ASM_ARITH_TAC)
+ \\ `inv (- nR2) = - (inv nR2)` by (irule (GSYM REAL_NEG_INV) \\ REAL_ASM_ARITH_TAC)
+ \\ `inv (- nF2) = - (inv nF2)` by (irule (GSYM REAL_NEG_INV) \\ REAL_ASM_ARITH_TAC)
+ \\ rpt (
+ qpat_x_assum `inv (- _) = - (inv _)`
+ (fn thm => rule_assum_tac (fn hyp => REWRITE_RULE [thm] hyp)))
+ \\ `inv nF2 <= inv nR2` by REAL_ASM_ARITH_TAC
+ \\ qpat_x_assum `- _ <= - _` kall_tac
+ \\ `0 <= inv nR2 - inv nF2` by REAL_ASM_ARITH_TAC
+ \\ `(inv nR2 − inv nF2) ≤ err2 * inv ((e2hi + err2) pow 2)` by REAL_ASM_ARITH_TAC
+ \\ `inv nF2 <= inv nR2 + err2 * inv ((e2hi + err2) pow 2)` by REAL_ASM_ARITH_TAC
+ \\ `inv nR2 - err2 * inv ((e2hi + err2) pow 2) <= inv nF2` by REAL_ASM_ARITH_TAC
+ (* Next do a case distinction for the absolute value *)
+ \\ `! (x:real). ((abs x = x) /\ 0 <= x) \/ ((abs x = - x) /\ x < 0)` by REAL_ASM_ARITH_TAC
+ \\ qpat_x_assum `!x. A /\ B \/ C`
+ (qspec_then `(nR1:real / nR2:real) - (nF1:real / nF2:real)` DISJ_CASES_TAC)
+ \\ fs[real_sub, real_div, REAL_NEG_ADD, realTheory.abs]
+ (* Combine with a case split for nF1 *)
+ \\ qspecl_then [`nF1`, `0`] DISJ_CASES_TAC REAL_LTE_TOTAL
+ (* 0 ≤ nR1 * inv nR2 + - (nF1 * inv nF2); nF1 < 0*)
+ >- (
+ \\ irule REAL_LE_TRANS
+ \\ qexists_tac `nR1 * inv nR2 + - nF1 * (inv nR2 + err2 * inv ((e2hi + err2) * (e2hi + err2)))`
+ \\ conj_tac
+ >- (fs[REAL_LE_LADD] \\ once_rewrite_tac [REAL_NEG_LMUL]
+ \\ irule REAL_LE_LMUL_IMP
+ \\ conj_tac \\ REAL_ASM_ARITH_TAC)
+ \\ qabbrev_tac `err_inv = (err2 * inv ((e2hi + err2) pow 2))`
+ \\ qspecl_then [`inv nR2 + err_inv`, `0`] DISJ_CASES_TAC REAL_LTE_TOTAL
+ (* inv nR2 + err_inv < 0 *)
+ >- (
+ irule REAL_LE_TRANS
+ \\ qexists_tac `nR1 * inv nR2 + - (nR1 + err1) * (inv nR2 + err_inv)`
+ \\ conj_tac
+ >- (fs [REAL_LE_ADD])
+ \\ real_rewrite `nR1 * inv nR2 + - (nR1 + err1) * (inv nR2 + err_inv) =
+ - nR1 * err_inv + - (inv nR2) * err1 - err1 * err_inv`
+ \\ qunabbrev_tac `err_inv`
+ \\ rewrite_tac[real_sub]
+ \\ irule REAL_LE_ADD2
+ \\ conj_tac
+ >- (irule REAL_LE_ADD2
+ \\ conj_tac \\ TRY REAL_ASM_ARITH_TAC
+ \\ real_rewrite `err2 * maxAbs (e1lo, e1hi) = maxAbs (e1lo, e1hi) * err2`
+ \\ rewrite_tac [GSYM REAL_MUL_ASSOC]
+ \\ irule REAL_LE_RMUL_IMP
+ \\ fs[REAL_LE_POW2, REAL_LE_MUL])
+ \\ irule REAL_LE_TRANS \\ qexists_tac `0`
+ \\ fs[REAL_LE_POW2, REAL_LE_MUL])
+ (* 0 ≤ inv nR2 + err_inv *)
+ \\ irule REAL_LE_TRANS
+ \\ qexists_tac `nR1 * inv nR2 + - (nR1 + - err1) * (inv nR2 + err_inv)`
+ \\ conj_tac
+ >- (fs [REAL_LE_ADD]
+ \\ irule REAL_LE_RMUL_IMP
+ \\ conj_tac \\ REAL_ASM_ARITH_TAC)
+ \\ real_rewrite `nR1 * inv nR2 + - (nR1 + - err1) * (inv nR2 + err_inv) =
+ - nR1 * err_inv + inv nR2 * err1 + err1 * err_inv`
+ \\ qunabbrev_tac `err_inv`
+ \\ irule REAL_LE_ADD2
+ \\ conj_tac \\ TRY REAL_ASM_ARITH_TAC
+ \\ irule REAL_LE_ADD2
+ \\ conj_tac \\ TRY REAL_ASM_ARITH_TAC
+ \\ real_rewrite `err2 * maxAbs (e1lo, e1hi) = maxAbs (e1lo, e1hi) * err2`
+ \\ rewrite_tac [GSYM REAL_MUL_ASSOC]
+ \\ irule REAL_LE_RMUL_IMP
+ \\ fs[REAL_LE_POW2, REAL_LE_MUL])
+ (* 0 ≤ nR1 * inv nR2 + - (nF1 * inv nF2); 0 ≤ nF1 *)
+ >- (
+ irule REAL_LE_TRANS
+ \\ qexists_tac `nR1 * inv nR2 + - nF1 * (inv nR2 - err2 * inv ((e2hi + err2) pow 2))`
+ \\ conj_tac
+ >- (fs[REAL_LE_LADD] \\ once_rewrite_tac [REAL_NEG_LMUL]
+ \\ irule REAL_MUL_LE_COMPAT_NEG_L
+ \\ conj_tac \\ REAL_ASM_ARITH_TAC)
+ \\ qabbrev_tac `err_inv = (err2 * inv ((e2hi + err2) pow 2))` \\
+ \\ qspecl_then [`inv nR2 - err_inv`, `0`] DISJ_CASES_TAC REAL_LTE_TOTAL
+ (* inv nR2 - err_inv < 0 *)
+ >- (irule REAL_LE_TRANS
+ \\ qexists_tac `nR1 * inv nR2 + - (nR1 + err1) * (inv nR2 - err_inv)`
+ \\ conj_tac
+ >- (fs [REAL_LE_ADD])
+ \\ real_rewrite `nR1 * inv nR2 + - (nR1 + err1) * (inv nR2 - err_inv) =
+ nR1 * err_inv + - (inv nR2) * err1 + err1 * err_inv`
+ \\ qunabbrev_tac `err_inv`
+ \\ irule REAL_LE_ADD2
+ \\ conj_tac \\ TRY REAL_ASM_ARITH_TAC
+ \\ irule REAL_LE_ADD2
+ \\ conj_tac \\ TRY REAL_ASM_ARITH_TAC
+ \\ real_rewrite `err2 * maxAbs (e1lo, e1hi) = maxAbs (e1lo, e1hi) * err2`
+ \\ rewrite_tac [GSYM REAL_MUL_ASSOC]
+ \\ irule REAL_LE_RMUL_IMP
+ \\ fs[REAL_LE_POW2, REAL_LE_MUL])
+ (* 0 <= inv nR2 - err_inv *)
+ \\ irule REAL_LE_TRANS
+ \\ qexists_tac `nR1 * inv nR2 + - (nR1 + - err1) * (inv nR2 - err_inv)`
+ \\ conj_tac
+ >- (fs [REAL_LE_ADD]
+ \\ irule REAL_LE_RMUL_IMP
+ \\ conj_tac \\ REAL_ASM_ARITH_TAC)
+ \\ real_rewrite `nR1 * inv nR2 + - (nR1 + - err1) * (inv nR2 - err_inv) =
+ nR1 * err_inv + inv nR2 * err1 - err1 * err_inv`
+ \\ qunabbrev_tac `err_inv` \\ rewrite_tac[real_sub]
+ \\ irule REAL_LE_ADD2 \\ conj_tac
+ >- (irule REAL_LE_ADD2
+ \\ conj_tac \\ TRY REAL_ASM_ARITH_TAC
+ \\ real_rewrite `err2 * maxAbs (e1lo, e1hi) = maxAbs (e1lo, e1hi) * err2`
+ \\ rewrite_tac [GSYM REAL_MUL_ASSOC]
+ \\ irule REAL_LE_RMUL_IMP
+ \\ fs[REAL_LE_POW2, REAL_LE_MUL])
+ \\ rewrite_tac [REAL_NEG_LMUL]
+ \\ irule REAL_LE_TRANS \\ qexists_tac `0`
+ \\ fs[REAL_LE_POW2, REAL_LE_MUL])
+ (* nR1 * inv nR2 + - (nF1 * inv nF2) < 0; nF1 < 0 *)
+ >- (
+ )
+ \\
+ )
+ (* 0 < e2lo, 0 < e2lo - err2;
+ The range of the divisor is positive *)
+ \\
+
+ (* Case 2: Absolute value negative; nF1 < 0 *)
+ >- (irule REAL_LE_TRANS \\
+ qexists_tac `- nR1 * inv nR2 + nF1 * (inv nR2 - err2 * inv ((e2hi + err2) * (e2hi + err2)))` \\
+ conj_tac
+ >- (fs[REAL_LE_LADD] \\
+ irule REAL_MUL_LE_COMPAT_NEG_L \\
+ conj_tac \\ REAL_ASM_ARITH_TAC)
+ >- (qabbrev_tac `err_inv = (err2 * ((e2hi + err2) * (e2hi + err2))â»Â¹)` \\
+ qspecl_then [`inv nR2 - err_inv`, `0`] DISJ_CASES_TAC REAL_LTE_TOTAL
+ >- (irule REAL_LE_TRANS \\
+ qexists_tac `- nR1 * inv nR2 + (nR1 - err1) * (inv nR2 - err_inv)` \\
+ conj_tac
+ >- (fs [REAL_LE_ADD] \\
+ once_rewrite_tac [REAL_MUL_COMM] \\
+ irule REAL_MUL_LE_COMPAT_NEG_L\\
+ conj_tac \\ TRY REAL_ASM_ARITH_TAC \\
+ fs [REAL_LE_NEG])
+ >- (`- nR1 * inv nR2 + (nR1 - err1) * (inv nR2 - err_inv) =
+ - nR1 * err_inv + - (inv nR2) * err1 + err1 * err_inv`
+ by REAL_ASM_ARITH_TAC \\
+ simp[REAL_NEG_MUL2] \\
+ qspecl_then [`inv ((e2hi + err2) * (e2hi + err2))`,`err2`]
+ (fn thm => once_rewrite_tac [thm]) REAL_MUL_COMM \\
+ qunabbrev_tac `err_inv` \\
+ irule REAL_LE_ADD2 \\
+ conj_tac \\ TRY REAL_ASM_ARITH_TAC \\
+ irule REAL_LE_ADD2 \\
+ conj_tac \\ TRY REAL_ASM_ARITH_TAC \\
+ irule REAL_LE_RMUL_IMP \\
+ conj_tac \\ REAL_ASM_ARITH_TAC))
+ >- (irule REAL_LE_TRANS \\
+ qexists_tac `- nR1 * inv nR2 + (nR1 + err1) * (inv nR2 - err_inv)` \\
+ conj_tac
+ >- (fs [REAL_LE_ADD] \\
+ irule REAL_LE_RMUL_IMP \\
+ conj_tac \\ REAL_ASM_ARITH_TAC)
+ >- (`- nR1 * inv nR2 + (nR1 + err1) * (inv nR2 - err_inv) =
+ - nR1 * err_inv + inv nR2 * err1 - err1 * err_inv`
+ by REAL_ASM_ARITH_TAC \\
+ simp[REAL_NEG_MUL2] \\
+ qspecl_then [`inv ((e2hi + err2) * (e2hi + err2))`,`err2`]
+ (fn thm => once_rewrite_tac [thm]) REAL_MUL_COMM \\
+ qunabbrev_tac `err_inv` \\
+ simp [real_sub] \\
+ irule REAL_LE_ADD2 \\
+ conj_tac
+ >- (irule REAL_LE_ADD2 \\
+ conj_tac \\ TRY REAL_ASM_ARITH_TAC \\
+ irule REAL_LE_RMUL_IMP \\
+ conj_tac \\ REAL_ASM_ARITH_TAC)
+ >- (fs [GSYM REAL_NEG_ADD, REAL_NEG_MUL2, REAL_NEG_LMUL] \\
+ irule REAL_LE_RMUL_IMP \\
+ conj_tac \\ REAL_ASM_ARITH_TAC)))))
+ (* 0 <= - nF1 *)
+ >- (irule REAL_LE_TRANS \\
+ qexists_tac `- nR1 * inv nR2 + nF1 * (inv nR2 + err2 * inv ((e2hi + err2) * (e2hi + err2)))` \\
+ conj_tac
+ >- (fs[REAL_LE_LADD] \\
+ irule REAL_LE_LMUL_IMP \\
+ conj_tac \\ REAL_ASM_ARITH_TAC)
+ >- (qabbrev_tac `err_inv = (err2 * ((e2hi + err2) * (e2hi + err2))â»Â¹)` \\
+ qspecl_then [`inv nR2 + err_inv`, `0`] DISJ_CASES_TAC REAL_LTE_TOTAL
+ >- (irule REAL_LE_TRANS \\
+ qexists_tac `-nR1 * inv nR2 + (nR1 - err1) * (inv nR2 + err_inv)` \\
+ conj_tac
+ >- (fs [REAL_LE_ADD] \\
+ once_rewrite_tac [REAL_MUL_COMM] \\
+ irule REAL_MUL_LE_COMPAT_NEG_L\\
+ conj_tac \\ TRY REAL_ASM_ARITH_TAC \\
+ fs [REAL_LE_NEG])
+ >- (`- nR1 * inv nR2 + (nR1 - err1) * (inv nR2 + err_inv) =
+ nR1 * err_inv + - (inv nR2) * err1 - err1 * err_inv`
+ by REAL_ASM_ARITH_TAC \\
+ simp[REAL_NEG_MUL2] \\
+ qspecl_then [`inv ((e2hi + err2) * (e2hi + err2))`,`err2`]
+ (fn thm => once_rewrite_tac [thm]) REAL_MUL_COMM \\
+ qunabbrev_tac `err_inv` \\
+ simp[real_sub] \\
+ irule REAL_LE_ADD2 \\
+ conj_tac
+ >- (irule REAL_LE_ADD2 \\
+ conj_tac \\ TRY REAL_ASM_ARITH_TAC \\
+ irule REAL_LE_RMUL_IMP \\
+ conj_tac \\ REAL_ASM_ARITH_TAC)
+ >- (fs [REAL_NEG_LMUL] \\
+ irule REAL_LE_RMUL_IMP \\
+ conj_tac \\ REAL_ASM_ARITH_TAC)))
+ >- (irule REAL_LE_TRANS \\
+ qexists_tac `- nR1 * inv nR2 + (nR1 + err1) * (inv nR2 + err_inv)` \\
+ conj_tac
+ >- (fs [REAL_LE_ADD] \\
+ irule REAL_LE_RMUL_IMP \\
+ conj_tac \\ REAL_ASM_ARITH_TAC)
+ >- (`- nR1 * inv nR2 + (nR1 + err1) * (inv nR2 + err_inv) =
+ nR1 * err_inv + inv nR2 * err1 + err1 * err_inv`
+ by REAL_ASM_ARITH_TAC \\
+ simp[REAL_NEG_MUL2] \\
+ qspecl_then [`inv ((e2hi + err2) * (e2hi + err2))`,`err2`]
+ (fn thm => once_rewrite_tac [thm]) REAL_MUL_COMM \\
+ qunabbrev_tac `err_inv` \\
+ irule REAL_LE_ADD2 \\
+ conj_tac \\ TRY REAL_ASM_ARITH_TAC \\
+ irule REAL_LE_ADD2 \\
+ conj_tac \\ TRY REAL_ASM_ARITH_TAC \\
+ irule REAL_LE_RMUL_IMP \\
+ conj_tac \\ REAL_ASM_ARITH_TAC)))))
+
+(* The range of the divisor lies in the range from 0 to infinity *)
+ >- (rule_assum_tac
+ (fn thm =>
+ REWRITE_RULE[IVlo_def, IVhi_def, widenInterval_def, contained_def, invertInterval_def] thm) \\
+ `abs (inv nR2 - inv nF2) <= err2 * (inv ((e2lo - err2) * (e2lo -err2)))`
+ by (irule err_prop_inversion_pos \\
+ qexists_tac `e2hi` \\ rpt(conj_tac) \\
+ fs[contained_def, IVlo_def, IVhi_def]) \\
+ fs [widenInterval_def, IVlo_def, IVhi_def, invertInterval_def] \\
+ `minAbsFun (e2lo - err2, e2hi + err2) = (e2lo - err2)`
+ by (irule minAbs_positive_iv_is_lo \\ REAL_ASM_ARITH_TAC) \\
+ simp[] \\
+ qpat_x_assum `minAbsFun _ = _ ` kall_tac \\
+ `nF1 <= err1 + nR1` by REAL_ASM_ARITH_TAC \\
+ `nR1 - err1 <= nF1` by REAL_ASM_ARITH_TAC \\
+ `(nR2 - nF2 > 0 /\ nR2 - nF2 <= err2) \/ (nR2 - nF2 <= 0 /\ - (nR2 - nF2) <= err2)`
+ by REAL_ASM_ARITH_TAC
+ (* Positive case for abs (nR2 - nF2) <= err2 *)
+ >- (`nF2 < nR2` by REAL_ASM_ARITH_TAC \\
+ `inv nR2 < inv nF2` by (irule REAL_LT_INV \\ TRY REAL_ASM_ARITH_TAC) \\
+ `inv nR2 - inv nF2 < 0` by REAL_ASM_ARITH_TAC \\
+ `nR2â»Â¹ − nF2â»Â¹ ≤ err2 * ((e2lo - err2) * (e2lo - err2))â»Â¹` by REAL_ASM_ARITH_TAC \\
+ `inv nF2 <= inv nR2 + err2 * inv ((e2lo - err2) * (e2lo - err2))` by REAL_ASM_ARITH_TAC \\
+ `inv nR2 - err2 * inv ((e2lo - err2) * (e2lo - err2)) <= inv nF2` by REAL_ASM_ARITH_TAC \\
+ (* Next do a case distinction for the absolute value *)
+ `! (x:real). ((abs x = x) /\ 0 <= x) \/ ((abs x = - x) /\ x < 0)` by REAL_ASM_ARITH_TAC \\
+ qpat_x_assum `!x. A /\ B \/ C`
+ (fn thm => qspec_then `(nR1:real / nR2:real) - (nF1:real / nF2:real)` DISJ_CASES_TAC thm)
+ \\ fs[realTheory.abs]
+ (* Case 1: Absolute value positive *)
+ >- (fs[real_sub, real_div, REAL_NEG_LMUL] \\
+ qspecl_then [`-nF1`, `0`] DISJ_CASES_TAC REAL_LTE_TOTAL
+ (* -nF1 < 0 *)
+ >- (irule REAL_LE_TRANS \\
+ qexists_tac `nR1 * inv nR2 + - nF1 * (inv nR2 - err2 * inv ((e2lo - err2) * (e2lo - err2)))` \\
+ conj_tac
+ >- (fs[REAL_LE_LADD] \\
+ irule REAL_MUL_LE_COMPAT_NEG_L \\
+ conj_tac \\ REAL_ASM_ARITH_TAC)
+ >- (qabbrev_tac `err_inv = (err2 * ((e2lo - err2) * (e2lo - err2))â»Â¹)` \\
+ qspecl_then [`inv nR2 - err_inv`, `0`] DISJ_CASES_TAC REAL_LTE_TOTAL
+ >- (irule REAL_LE_TRANS \\
+ qexists_tac `nR1 * inv nR2 + - (nR1 + err1) * (inv nR2 - err_inv)` \\
+ conj_tac
+ >- (fs [REAL_LE_ADD] \\
+ once_rewrite_tac [REAL_MUL_COMM] \\
+ irule REAL_MUL_LE_COMPAT_NEG_L\\
+ conj_tac \\ TRY REAL_ASM_ARITH_TAC \\
+ fs [REAL_LE_NEG])
+ >- (`nR1 * inv nR2 + - (nR1 + err1) * (inv nR2 - err_inv) =
+ nR1 * err_inv + - (inv nR2) * err1 + err1 * err_inv`
+ by REAL_ASM_ARITH_TAC \\
+ simp[REAL_NEG_MUL2] \\
+ qspecl_then [`inv ((e2lo + - err2) * (e2lo + - err2))`,`err2`]
+ (fn thm => once_rewrite_tac [thm]) REAL_MUL_COMM \\
+ qunabbrev_tac `err_inv` \\
+ irule REAL_LE_ADD2 \\
+ conj_tac \\ TRY REAL_ASM_ARITH_TAC \\
+ irule REAL_LE_ADD2 \\
+ conj_tac \\ TRY REAL_ASM_ARITH_TAC \\
+ simp[GSYM real_sub] \\
+ irule REAL_LE_RMUL_IMP \\
+ conj_tac \\ REAL_ASM_ARITH_TAC))
+ >- (irule REAL_LE_TRANS \\
+ qexists_tac `nR1 * inv nR2 + - (nR1 + - err1) * (inv nR2 - err_inv)` \\
+ conj_tac
+ >- (fs [REAL_LE_ADD] \\
+ irule REAL_LE_RMUL_IMP \\
+ conj_tac \\ REAL_ASM_ARITH_TAC)
+ >- (`nR1 * inv nR2 + - (nR1 + - err1) * (inv nR2 - err_inv) =
+ nR1 * err_inv + inv nR2 * err1 - err1 * err_inv`
+ by REAL_ASM_ARITH_TAC \\
+ simp[REAL_NEG_MUL2] \\
+ qspecl_then [`inv ((e2lo + -err2) * (e2lo + -err2))`,`err2`]
+ (fn thm => once_rewrite_tac [thm]) REAL_MUL_COMM \\
+ qunabbrev_tac `err_inv` \\
+ simp [real_sub] \\
+ irule REAL_LE_ADD2 \\
+ conj_tac
+ >- (irule REAL_LE_ADD2 \\
+ conj_tac \\ TRY REAL_ASM_ARITH_TAC \\
+ irule REAL_LE_RMUL_IMP \\
+ conj_tac \\ REAL_ASM_ARITH_TAC)
+ >- (simp [REAL_NEG_LMUL] \\
+ irule REAL_LE_RMUL_IMP \\
+ conj_tac \\ REAL_ASM_ARITH_TAC)))))
+ (* 0 <= - nF1 *)
+ >- (irule REAL_LE_TRANS \\
+ qexists_tac `nR1 * inv nR2 + - nF1 * (inv nR2 + err2 * inv ((e2lo - err2) * (e2lo - err2)))` \\
+ conj_tac
+ >- (fs[REAL_LE_LADD] \\
+ irule REAL_LE_LMUL_IMP \\
+ conj_tac \\ REAL_ASM_ARITH_TAC)
+ >- (qabbrev_tac `err_inv = (err2 * ((e2lo - err2) * (e2lo - err2))â»Â¹)` \\
+ qspecl_then [`inv nR2 + err_inv`, `0`] DISJ_CASES_TAC REAL_LTE_TOTAL
+ >- (irule REAL_LE_TRANS \\
+ qexists_tac `nR1 * inv nR2 + - (nR1 + err1) * (inv nR2 + err_inv)` \\
+ conj_tac
+ >- (fs [REAL_LE_ADD] \\
+ once_rewrite_tac [REAL_MUL_COMM] \\
+ irule REAL_MUL_LE_COMPAT_NEG_L\\
+ conj_tac \\ TRY REAL_ASM_ARITH_TAC \\
+ fs [REAL_LE_NEG])
+ >- (`nR1 * inv nR2 + - (nR1 + err1) * (inv nR2 + err_inv) =
+ - nR1 * err_inv + - (inv nR2) * err1 - err1 * err_inv`
+ by REAL_ASM_ARITH_TAC \\
+ simp[REAL_NEG_MUL2] \\
+ qspecl_then [`inv ((e2lo + -err2) * (e2lo + -err2))`,`err2`]
+ (fn thm => once_rewrite_tac [thm]) REAL_MUL_COMM \\
+ qunabbrev_tac `err_inv` \\
+ simp[real_sub] \\
+ irule REAL_LE_ADD2 \\
+ conj_tac
+ >- (irule REAL_LE_ADD2 \\
+ conj_tac \\ TRY REAL_ASM_ARITH_TAC \\
+ irule REAL_LE_RMUL_IMP \\
+ conj_tac \\ REAL_ASM_ARITH_TAC)
+ >- (simp [REAL_NEG_LMUL] \\
+ irule REAL_LE_RMUL_IMP \\
+ conj_tac \\ REAL_ASM_ARITH_TAC)))
+ >- (irule REAL_LE_TRANS \\
+ qexists_tac `nR1 * inv nR2 + - (nR1 + - err1) * (inv nR2 + err_inv)` \\
+ conj_tac
+ >- (fs [REAL_LE_ADD] \\
+ irule REAL_LE_RMUL_IMP \\
+ conj_tac \\ REAL_ASM_ARITH_TAC)
+ >- (`nR1 * inv nR2 + - (nR1 + - err1) * (inv nR2 + err_inv) =
+ - nR1 * err_inv + inv nR2 * err1 + err1 * err_inv`
+ by REAL_ASM_ARITH_TAC \\
+ simp[REAL_NEG_MUL2] \\
+ qspecl_then [`inv ((e2lo + -err2) * (e2lo + -err2))`,`err2`]
+ (fn thm => once_rewrite_tac [thm]) REAL_MUL_COMM \\
+ qunabbrev_tac `err_inv` \\
+ irule REAL_LE_ADD2 \\
+ conj_tac \\ TRY REAL_ASM_ARITH_TAC \\
+ irule REAL_LE_ADD2 \\
+ conj_tac \\ TRY REAL_ASM_ARITH_TAC \\
+ simp [GSYM real_sub] \\
+ irule REAL_LE_RMUL_IMP \\
+ conj_tac \\ REAL_ASM_ARITH_TAC)))))
+ (* Case 2: Absolute value negative *)
+ >- (fs[real_sub, real_div, REAL_NEG_LMUL, REAL_NEG_ADD] \\
+ qspecl_then [`nF1`, `0`] DISJ_CASES_TAC REAL_LTE_TOTAL
+ (* nF1 < 0 *)
+ >- (irule REAL_LE_TRANS \\
+ qexists_tac `- nR1 * inv nR2 + nF1 * (inv nR2 - err2 * inv ((e2lo - err2) * (e2lo - err2)))` \\
+ conj_tac
+ >- (fs[REAL_LE_LADD] \\
+ irule REAL_MUL_LE_COMPAT_NEG_L \\
+ conj_tac \\ REAL_ASM_ARITH_TAC)
+ >- (qabbrev_tac `err_inv = (err2 * ((e2lo - err2) * (e2lo - err2))â»Â¹)` \\
+ qspecl_then [`inv nR2 - err_inv`, `0`] DISJ_CASES_TAC REAL_LTE_TOTAL
+ >- (irule REAL_LE_TRANS \\
+ qexists_tac `- nR1 * inv nR2 + (nR1 - err1) * (inv nR2 - err_inv)` \\
+ conj_tac
+ >- (fs [REAL_LE_ADD] \\
+ once_rewrite_tac [REAL_MUL_COMM] \\
+ irule REAL_MUL_LE_COMPAT_NEG_L\\
+ conj_tac \\ TRY REAL_ASM_ARITH_TAC \\
+ fs [REAL_LE_NEG])
+ >- (`- nR1 * inv nR2 + (nR1 - err1) * (inv nR2 - err_inv) =
+ - nR1 * err_inv + - (inv nR2) * err1 + err1 * err_inv`
+ by REAL_ASM_ARITH_TAC \\
+ simp[REAL_NEG_MUL2] \\
+ qspecl_then [`inv ((e2lo + -err2) * (e2lo + -err2))`,`err2`]
+ (fn thm => once_rewrite_tac [thm]) REAL_MUL_COMM \\
+ qunabbrev_tac `err_inv` \\
+ irule REAL_LE_ADD2 \\
+ conj_tac \\ TRY REAL_ASM_ARITH_TAC \\
+ irule REAL_LE_ADD2 \\
+ conj_tac \\ TRY REAL_ASM_ARITH_TAC \\
+ simp [GSYM real_sub] \\
+ irule REAL_LE_RMUL_IMP \\
+ conj_tac \\ REAL_ASM_ARITH_TAC))
+ >- (irule REAL_LE_TRANS \\
+ qexists_tac `- nR1 * inv nR2 + (nR1 + err1) * (inv nR2 - err_inv)` \\
+ conj_tac
+ >- (fs [REAL_LE_ADD] \\
+ irule REAL_LE_RMUL_IMP \\
+ conj_tac \\ REAL_ASM_ARITH_TAC)
+ >- (`- nR1 * inv nR2 + (nR1 + err1) * (inv nR2 - err_inv) =
+ - nR1 * err_inv + inv nR2 * err1 - err1 * err_inv`
+ by REAL_ASM_ARITH_TAC \\
+ simp[REAL_NEG_MUL2] \\
+ qspecl_then [`inv ((e2lo + -err2) * (e2lo + -err2))`,`err2`]
+ (fn thm => once_rewrite_tac [thm]) REAL_MUL_COMM \\
+ qunabbrev_tac `err_inv` \\
+ simp [real_sub] \\
+ irule REAL_LE_ADD2 \\
+ conj_tac
+ >- (irule REAL_LE_ADD2 \\
+ conj_tac \\ TRY REAL_ASM_ARITH_TAC \\
+ fs [GSYM REAL_NEG_ADD, REAL_NEG_MUL2] \\
+ irule REAL_LE_RMUL_IMP \\
+ conj_tac \\ REAL_ASM_ARITH_TAC)
+ >- (fs [GSYM REAL_NEG_ADD, REAL_NEG_MUL2, REAL_NEG_LMUL] \\
+ irule REAL_LE_RMUL_IMP \\
+ conj_tac \\ REAL_ASM_ARITH_TAC)))))
+ (* 0 <= - nF1 *)
+ >- (irule REAL_LE_TRANS \\
+ qexists_tac `- nR1 * inv nR2 + nF1 * (inv nR2 + err2 * inv ((e2lo - err2) * (e2lo - err2)))` \\
+ conj_tac
+ >- (fs[REAL_LE_LADD] \\
+ irule REAL_LE_LMUL_IMP \\
+ conj_tac \\ REAL_ASM_ARITH_TAC)
+ >- (qabbrev_tac `err_inv = (err2 * ((e2lo - err2) * (e2lo - err2))â»Â¹)` \\
+ qspecl_then [`inv nR2 + err_inv`, `0`] DISJ_CASES_TAC REAL_LTE_TOTAL
+ >- (irule REAL_LE_TRANS \\
+ qexists_tac `-nR1 * inv nR2 + (nR1 - err1) * (inv nR2 + err_inv)` \\
+ conj_tac
+ >- (fs [REAL_LE_ADD] \\
+ once_rewrite_tac [REAL_MUL_COMM] \\
+ irule REAL_MUL_LE_COMPAT_NEG_L\\
+ conj_tac \\ TRY REAL_ASM_ARITH_TAC \\
+ fs [REAL_LE_NEG])
+ >- (`- nR1 * inv nR2 + (nR1 - err1) * (inv nR2 + err_inv) =
+ nR1 * err_inv + - (inv nR2) * err1 - err1 * err_inv`
+ by REAL_ASM_ARITH_TAC \\
+ simp[REAL_NEG_MUL2] \\
+ qspecl_then [`inv ((e2lo + -err2) * (e2lo + -err2))`,`err2`]
+ (fn thm => once_rewrite_tac [thm]) REAL_MUL_COMM \\
+ qunabbrev_tac `err_inv` \\
+ simp[real_sub] \\
+ irule REAL_LE_ADD2 \\
+ conj_tac
+ >- (irule REAL_LE_ADD2 \\
+ conj_tac \\ TRY REAL_ASM_ARITH_TAC \\
+ irule REAL_LE_RMUL_IMP \\
+ conj_tac \\ REAL_ASM_ARITH_TAC)
+ >- (fs [REAL_NEG_LMUL] \\
+ irule REAL_LE_RMUL_IMP \\
+ conj_tac \\ REAL_ASM_ARITH_TAC)))
+ >- (irule REAL_LE_TRANS \\
+ qexists_tac `- nR1 * inv nR2 + (nR1 + err1) * (inv nR2 + err_inv)` \\
+ conj_tac
+ >- (fs [REAL_LE_ADD] \\
+ irule REAL_LE_RMUL_IMP \\
+ conj_tac \\ REAL_ASM_ARITH_TAC)
+ >- (`- nR1 * inv nR2 + (nR1 + err1) * (inv nR2 + err_inv) =
+ nR1 * err_inv + inv nR2 * err1 + err1 * err_inv`
+ by REAL_ASM_ARITH_TAC \\
+ simp[REAL_NEG_MUL2] \\
+ qspecl_then [`inv ((e2lo + -err2) * (e2lo + -err2))`,`err2`]
+ (fn thm => once_rewrite_tac [thm]) REAL_MUL_COMM \\
+ qunabbrev_tac `err_inv` \\
+ irule REAL_LE_ADD2 \\
+ conj_tac \\ TRY REAL_ASM_ARITH_TAC \\
+ irule REAL_LE_ADD2 \\
+ conj_tac \\ TRY REAL_ASM_ARITH_TAC \\
+ simp [GSYM real_sub] \\
+ irule REAL_LE_RMUL_IMP \\
+ conj_tac \\ REAL_ASM_ARITH_TAC))))))
+ (* Negative case for abs (nR2 - nF2) <= err2 *)
+ >- (fs [GSYM REAL_NEG_ADD, REAL_NEG_MUL2, REAL_NEG_LMUL] \\
+ `nR2 <= nF2` by REAL_ASM_ARITH_TAC \\
+ `inv nF2 <= inv nR2` by (irule REAL_INV_LE_ANTIMONO_IMPR \\ REAL_ASM_ARITH_TAC) \\
+ `0 <= inv nR2 - inv nF2` by REAL_ASM_ARITH_TAC \\
+ `(nR2â»Â¹ − nF2â»Â¹) ≤ err2 * ((e2lo - err2) * (e2lo - err2))â»Â¹` by REAL_ASM_ARITH_TAC \\
+ `inv nF2 <= inv nR2 + err2 * inv ((e2lo - err2) * (e2lo - err2))` by REAL_ASM_ARITH_TAC \\
+ `inv nR2 - err2 * inv ((e2lo - err2) * (e2lo - err2)) <= inv nF2` by REAL_ASM_ARITH_TAC \\
+ (* Next do a case distinction for the absolute value *)
+ `! (x:real). ((abs x = x) /\ 0 <= x) \/ ((abs x = - x) /\ x < 0)` by REAL_ASM_ARITH_TAC \\
+ qpat_x_assum `!x. A /\ B \/ C`
+ (fn thm => qspec_then `(nR1:real / nR2:real) - (nF1:real / nF2:real)` DISJ_CASES_TAC thm) \\
+ fs[real_sub, real_div, REAL_NEG_LMUL, REAL_NEG_ADD, realTheory.abs]
+ (* Case 1: Absolute value positive *)
+ >- (qspecl_then [`-nF1`, `0`] DISJ_CASES_TAC REAL_LTE_TOTAL
+ (* -nF1 < 0 *)
+ >- (irule REAL_LE_TRANS \\
+ qexists_tac `nR1 * inv nR2 + - nF1 * (inv nR2 - err2 * inv ((e2lo - err2) * (e2lo - err2)))` \\
+ conj_tac
+ >- (fs[REAL_LE_LADD] \\
+ irule REAL_MUL_LE_COMPAT_NEG_L \\
+ conj_tac \\ REAL_ASM_ARITH_TAC)
+ >- (qabbrev_tac `err_inv = (err2 * ((e2lo - err2) * (e2lo - err2))â»Â¹)` \\
+ qspecl_then [`inv nR2 - err_inv`, `0`] DISJ_CASES_TAC REAL_LTE_TOTAL
+ >- (irule REAL_LE_TRANS \\
+ qexists_tac `nR1 * inv nR2 + - (nR1 + err1) * (inv nR2 - err_inv)` \\
+ conj_tac
+ >- (fs [REAL_LE_ADD] \\
+ once_rewrite_tac [REAL_MUL_COMM] \\
+ irule REAL_MUL_LE_COMPAT_NEG_L\\
+ conj_tac \\ TRY REAL_ASM_ARITH_TAC \\
+ fs [REAL_LE_NEG])
+ >- (`nR1 * inv nR2 + - (nR1 + err1) * (inv nR2 - err_inv) =
+ nR1 * err_inv + - (inv nR2) * err1 + err1 * err_inv`
+ by REAL_ASM_ARITH_TAC \\
+ simp[REAL_NEG_MUL2] \\
+ qspecl_then [`inv ((e2lo + -err2) * (e2lo + -err2))`,`err2`]
+ (fn thm => once_rewrite_tac [thm]) REAL_MUL_COMM \\
+ qunabbrev_tac `err_inv` \\
+ irule REAL_LE_ADD2 \\
+ conj_tac \\ TRY REAL_ASM_ARITH_TAC \\
+ irule REAL_LE_ADD2 \\
+ conj_tac \\ TRY REAL_ASM_ARITH_TAC \\
+ simp [GSYM real_sub] \\
+ irule REAL_LE_RMUL_IMP \\
+ conj_tac \\ REAL_ASM_ARITH_TAC))
+ >- (irule REAL_LE_TRANS \\
+ qexists_tac `nR1 * inv nR2 + - (nR1 + - err1) * (inv nR2 - err_inv)` \\
+ conj_tac
+ >- (fs [REAL_LE_ADD] \\
+ irule REAL_LE_RMUL_IMP \\
+ conj_tac \\ REAL_ASM_ARITH_TAC)
+ >- (`nR1 * inv nR2 + - (nR1 + - err1) * (inv nR2 - err_inv) =
+ nR1 * err_inv + inv nR2 * err1 - err1 * err_inv`
+ by REAL_ASM_ARITH_TAC \\
+ simp[REAL_NEG_MUL2] \\
+ qspecl_then [`inv ((e2lo + -err2) * (e2lo + -err2))`,`err2`]
+ (fn thm => once_rewrite_tac [thm]) REAL_MUL_COMM \\
+ qunabbrev_tac `err_inv` \\
+ simp [real_sub] \\
+ irule REAL_LE_ADD2 \\
+ conj_tac
+ >- (irule REAL_LE_ADD2 \\
+ conj_tac \\ TRY REAL_ASM_ARITH_TAC \\
+ irule REAL_LE_RMUL_IMP \\
+ conj_tac \\ REAL_ASM_ARITH_TAC)
+ >- (simp [REAL_NEG_LMUL] \\
+ irule REAL_LE_RMUL_IMP \\
+ conj_tac \\ REAL_ASM_ARITH_TAC)))))
+ (* 0 <= - nF1 *)
+ >- (irule REAL_LE_TRANS \\
+ qexists_tac `nR1 * inv nR2 + - nF1 * (inv nR2 + err2 * inv ((e2lo - err2) * (e2lo - err2)))` \\
+ conj_tac
+ >- (fs[REAL_LE_LADD] \\
+ irule REAL_LE_LMUL_IMP \\
+ conj_tac \\ REAL_ASM_ARITH_TAC)
+ >- (qabbrev_tac `err_inv = (err2 * ((e2lo - err2) * (e2lo - err2))â»Â¹)` \\
+ qspecl_then [`inv nR2 + err_inv`, `0`] DISJ_CASES_TAC REAL_LTE_TOTAL
+ >- (irule REAL_LE_TRANS \\
+ qexists_tac `nR1 * inv nR2 + - (nR1 + err1) * (inv nR2 + err_inv)` \\
+ conj_tac
+ >- (fs [REAL_LE_ADD] \\
+ once_rewrite_tac [REAL_MUL_COMM] \\
+ irule REAL_MUL_LE_COMPAT_NEG_L\\
+ conj_tac \\ TRY REAL_ASM_ARITH_TAC \\
+ fs [REAL_LE_NEG])
+ >- (`nR1 * inv nR2 + - (nR1 + err1) * (inv nR2 + err_inv) =
+ - nR1 * err_inv + - (inv nR2) * err1 - err1 * err_inv`
+ by REAL_ASM_ARITH_TAC \\
+ simp[REAL_NEG_MUL2] \\
+ qspecl_then [`inv ((e2lo + -err2) * (e2lo + -err2))`,`err2`]
+ (fn thm => once_rewrite_tac [thm]) REAL_MUL_COMM \\
+ qunabbrev_tac `err_inv` \\
+ simp[real_sub] \\
+ irule REAL_LE_ADD2 \\
+ conj_tac
+ >- (irule REAL_LE_ADD2 \\
+ conj_tac \\ TRY REAL_ASM_ARITH_TAC \\
+ irule REAL_LE_RMUL_IMP \\
+ conj_tac \\ REAL_ASM_ARITH_TAC)
+ >- (simp [REAL_NEG_LMUL] \\
+ irule REAL_LE_RMUL_IMP \\
+ conj_tac \\ REAL_ASM_ARITH_TAC)))
+ >- (irule REAL_LE_TRANS \\
+ qexists_tac `nR1 * inv nR2 + - (nR1 + - err1) * (inv nR2 + err_inv)` \\
+ conj_tac
+ >- (fs [REAL_LE_ADD] \\
+ irule REAL_LE_RMUL_IMP \\
+ conj_tac \\ REAL_ASM_ARITH_TAC)
+ >- (`nR1 * inv nR2 + - (nR1 + - err1) * (inv nR2 + err_inv) =
+ - nR1 * err_inv + inv nR2 * err1 + err1 * err_inv`
+ by REAL_ASM_ARITH_TAC \\
+ simp[REAL_NEG_MUL2] \\
+ qspecl_then [`inv ((e2lo + -err2) * (e2lo + -err2))`,`err2`]
+ (fn thm => once_rewrite_tac [thm]) REAL_MUL_COMM \\
+ qunabbrev_tac `err_inv` \\
+ irule REAL_LE_ADD2 \\
+ conj_tac \\ TRY REAL_ASM_ARITH_TAC \\
+ irule REAL_LE_ADD2 \\
+ conj_tac \\ TRY REAL_ASM_ARITH_TAC \\
+ simp [GSYM real_sub] \\
+ irule REAL_LE_RMUL_IMP \\
+ conj_tac \\ REAL_ASM_ARITH_TAC)))))
+ (* Case 2: Absolute value negative *)
+ >- (qspecl_then [`nF1`, `0`] DISJ_CASES_TAC REAL_LTE_TOTAL
+ (* nF1 < 0 *)
+ >- (irule REAL_LE_TRANS \\
+ qexists_tac `- nR1 * inv nR2 + nF1 * (inv nR2 - err2 * inv ((e2lo - err2) * (e2lo - err2)))` \\
+ conj_tac
+ >- (fs[REAL_LE_LADD] \\
+ irule REAL_MUL_LE_COMPAT_NEG_L \\
+ conj_tac \\ REAL_ASM_ARITH_TAC)
+ >- (qabbrev_tac `err_inv = (err2 * ((e2lo - err2) * (e2lo - err2))â»Â¹)` \\
+ qspecl_then [`inv nR2 - err_inv`, `0`] DISJ_CASES_TAC REAL_LTE_TOTAL
+ >- (irule REAL_LE_TRANS \\
+ qexists_tac `- nR1 * inv nR2 + (nR1 - err1) * (inv nR2 - err_inv)` \\
+ conj_tac
+ >- (fs [REAL_LE_ADD] \\
+ once_rewrite_tac [REAL_MUL_COMM] \\
+ irule REAL_MUL_LE_COMPAT_NEG_L\\
+ conj_tac \\ TRY REAL_ASM_ARITH_TAC \\
+ fs [REAL_LE_NEG])
+ >- (`- nR1 * inv nR2 + (nR1 - err1) * (inv nR2 - err_inv) =
+ - nR1 * err_inv + - (inv nR2) * err1 + err1 * err_inv`
+ by REAL_ASM_ARITH_TAC \\
+ simp[REAL_NEG_MUL2] \\
+ qspecl_then [`inv ((e2lo + -err2) * (e2lo + -err2))`,`err2`]
+ (fn thm => once_rewrite_tac [thm]) REAL_MUL_COMM \\
+ qunabbrev_tac `err_inv` \\
+ irule REAL_LE_ADD2 \\
+ conj_tac \\ TRY REAL_ASM_ARITH_TAC \\
+ irule REAL_LE_ADD2 \\
+ conj_tac \\ TRY REAL_ASM_ARITH_TAC \\
+ simp [GSYM real_sub] \\
+ irule REAL_LE_RMUL_IMP \\
+ conj_tac \\ REAL_ASM_ARITH_TAC))
+ >- (irule REAL_LE_TRANS \\
+ qexists_tac `- nR1 * inv nR2 + (nR1 + err1) * (inv nR2 - err_inv)` \\
+ conj_tac
+ >- (fs [REAL_LE_ADD] \\
+ irule REAL_LE_RMUL_IMP \\
+ conj_tac \\ REAL_ASM_ARITH_TAC)
+ >- (`- nR1 * inv nR2 + (nR1 + err1) * (inv nR2 - err_inv) =
+ - nR1 * err_inv + inv nR2 * err1 - err1 * err_inv`
+ by REAL_ASM_ARITH_TAC \\
+ simp[REAL_NEG_MUL2] \\
+ qspecl_then [`inv ((e2lo + -err2) * (e2lo + -err2))`,`err2`]
+ (fn thm => once_rewrite_tac [thm]) REAL_MUL_COMM \\
+ qunabbrev_tac `err_inv` \\
+ simp [real_sub] \\
+ irule REAL_LE_ADD2 \\
+ conj_tac
+ >- (irule REAL_LE_ADD2 \\
+ conj_tac \\ TRY REAL_ASM_ARITH_TAC \\
+ irule REAL_LE_RMUL_IMP \\
+ conj_tac \\ REAL_ASM_ARITH_TAC)
+ >- (fs [GSYM REAL_NEG_ADD, REAL_NEG_MUL2, REAL_NEG_LMUL] \\
+ irule REAL_LE_RMUL_IMP \\
+ conj_tac \\ REAL_ASM_ARITH_TAC)))))
+ (* 0 <= - nF1 *)
+ >- (irule REAL_LE_TRANS \\
+ qexists_tac `- nR1 * inv nR2 + nF1 * (inv nR2 + err2 * inv ((e2lo - err2) * (e2lo - err2)))` \\
+ conj_tac
+ >- (fs[REAL_LE_LADD] \\
+ irule REAL_LE_LMUL_IMP \\
+ conj_tac \\ REAL_ASM_ARITH_TAC)
+ >- (qabbrev_tac `err_inv = (err2 * ((e2lo - err2) * (e2lo - err2))â»Â¹)` \\
+ qspecl_then [`inv nR2 + err_inv`, `0`] DISJ_CASES_TAC REAL_LTE_TOTAL
+ >- (irule REAL_LE_TRANS \\
+ qexists_tac `-nR1 * inv nR2 + (nR1 - err1) * (inv nR2 + err_inv)` \\
+ conj_tac
+ >- (fs [REAL_LE_ADD] \\
+ once_rewrite_tac [REAL_MUL_COMM] \\
+ irule REAL_MUL_LE_COMPAT_NEG_L\\
+ conj_tac \\ TRY REAL_ASM_ARITH_TAC \\
+ fs [REAL_LE_NEG])
+ >- (`- nR1 * inv nR2 + (nR1 - err1) * (inv nR2 + err_inv) =
+ nR1 * err_inv + - (inv nR2) * err1 - err1 * err_inv`
+ by REAL_ASM_ARITH_TAC \\
+ simp[REAL_NEG_MUL2] \\
+ qspecl_then [`inv ((e2lo + -err2) * (e2lo + -err2))`,`err2`]
+ (fn thm => once_rewrite_tac [thm]) REAL_MUL_COMM \\
+ qunabbrev_tac `err_inv` \\
+ simp[real_sub] \\
+ irule REAL_LE_ADD2 \\
+ conj_tac
+ >- (irule REAL_LE_ADD2 \\
+ conj_tac \\ TRY REAL_ASM_ARITH_TAC \\
+ irule REAL_LE_RMUL_IMP \\
+ conj_tac \\ REAL_ASM_ARITH_TAC)
+ >- (fs [REAL_NEG_LMUL] \\
+ irule REAL_LE_RMUL_IMP \\
+ conj_tac \\ REAL_ASM_ARITH_TAC)))
+ >- (irule REAL_LE_TRANS \\
+ qexists_tac `- nR1 * inv nR2 + (nR1 + err1) * (inv nR2 + err_inv)` \\
+ conj_tac
+ >- (fs [REAL_LE_ADD] \\
+ irule REAL_LE_RMUL_IMP \\
+ conj_tac \\ REAL_ASM_ARITH_TAC)
+ >- (`- nR1 * inv nR2 + (nR1 + err1) * (inv nR2 + err_inv) =
+ nR1 * err_inv + inv nR2 * err1 + err1 * err_inv`
+ by REAL_ASM_ARITH_TAC \\
+ simp[REAL_NEG_MUL2] \\
+ qspecl_then [`inv ((e2lo + -err2) * (e2lo + -err2))`,`err2`]
+ (fn thm => once_rewrite_tac [thm]) REAL_MUL_COMM \\
+ qunabbrev_tac `err_inv` \\
+ irule REAL_LE_ADD2 \\
+ conj_tac \\ TRY REAL_ASM_ARITH_TAC \\
+ irule REAL_LE_ADD2 \\
+ conj_tac \\ TRY REAL_ASM_ARITH_TAC \\
+ simp [GSYM real_sub] \\
+ irule REAL_LE_RMUL_IMP \\
+ conj_tac \\ REAL_ASM_ARITH_TAC)))))))
+QED
diff --git a/hol4/floverParserScript.sml b/hol4/floverParserScript.sml
index 5b141fcbaf4c622209ec305f601268497911ec9f..23516d23ca652872faa58df07f3e3f41d5634989 100644
--- a/hol4/floverParserScript.sml
+++ b/hol4/floverParserScript.sml
@@ -4,6 +4,7 @@ open preambleFloVer;
val _ = new_theory "floverParser";
+ (*
val _ = Datatype `
Token =
| DLET
@@ -481,5 +482,6 @@ val dParse_def = Define `
|NONE => NONE
|SOME (A, residual) =>
SOME ((dCmd, P, A, Gamma), residual))))`;
+ *)
val _ = export_theory();
diff --git a/hol4/semantics/AbbrevsScript.sml b/hol4/semantics/AbbrevsScript.sml
index e8dd78dd3072ba3944be1eec23061bc88bdfba02..b300f8c74750b47c2e5519c5d778a50ac84fb66e 100644
--- a/hol4/semantics/AbbrevsScript.sml
+++ b/hol4/semantics/AbbrevsScript.sml
@@ -10,35 +10,45 @@ val _ = new_theory "Abbrevs";
For the moment we need only one interval type in HOL, since we do not have the
problem of computability as we have it in Coq
**)
-val _ = type_abbrev("interval", ``:real#real``);
-val IVlo_def = Define `IVlo (iv:interval) = FST iv`;
-val IVhi_def = Define `IVhi (iv:interval) = SND iv`;
+Type interval = “:real#realâ€
+
+Definition IVlo_def:
+ IVlo (iv:interval) = FST iv
+End
+
+Definition IVhi_def:
+ IVhi (iv:interval) = SND iv
+End
(**
Later we will argue about program preconditions.
Define a precondition to be a function mapping numbers (resp. variables) to intervals.
**)
-val _ = type_abbrev ("precond", ``:num->interval``);
+Type precond = “:num->intervalâ€
(**
Abbreviation for the type of a variable environment, which should be a partial function
**)
-val _ = type_abbrev("env",``:num->real option``);
+Type env = “:num -> real optionâ€
(**
The empty environment must return NONE for every variable
**)
-val emptyEnv_def = Define `
- emptyEnv (x:num) = NONE`;
+Definition emptyEnv_def:
+ emptyEnv (x:num) = NONE
+End
(**
Define environment update function as abbreviation, for variable environments
**)
-val updEnv_def = Define `
+Definition updEnv_def:
updEnv (x:num) (v:real) (E:env) (y:num) :real option =
- if y = x then SOME v else E y`;
+ if y = x then SOME v else E y
+End
-val noDivzero_def = Define `noDivzero (a:real) (b:real) = (a < &0 \/ &0 < b)`;
+Definition noDivzero_def:
+ noDivzero (a:real) (b:real) = (a < &0 \/ &0 < b)
+End
val _ = export_rewrites ["IVlo_def", "IVhi_def",
"emptyEnv_def", "updEnv_def"]
diff --git a/hol4/semantics/CommandsScript.sml b/hol4/semantics/CommandsScript.sml
index b1c23388109163e3768198d9ecb488cfa75f09a3..1d27dc31b8b8873c6c3d8e705a6dfc87fd08cd7b 100644
--- a/hol4/semantics/CommandsScript.sml
+++ b/hol4/semantics/CommandsScript.sml
@@ -1,5 +1,6 @@
(**
- Formalization of the Abstract Syntax Tree of a subset used in the Flover framework
+ Formalization of the Abstract Syntax Tree of a subset used in the Flover
+ framework
**)
open simpLib realTheory realLib RealArith;
open AbbrevsTheory ExpressionsTheory ExpressionAbbrevsTheory
@@ -13,21 +14,23 @@ val _ = new_theory "Commands";
Currently no loops, or conditionals.
Only assignments and return statement
**)
-val _ = Datatype `
+Datatype:
cmd = Let mType num ('v expr) cmd
- | Ret ('v expr)`;
+ | Ret ('v expr)
+End
-val toREvalCmd_def = Define `
+Definition toREvalCmd_def:
toREvalCmd (f:real cmd) : real cmd =
- case f of
- | Let m x e g => Let REAL x (toREval e) (toREvalCmd g)
- | Ret e => Ret (toREval e)`;
+ case f of
+ | Let m x e g => Let REAL x (toREval e) (toREvalCmd g)
+ | Ret e => Ret (toREval e)
+End
(**
Define big step semantics for the Flover language, terminating on a "returned"
result value
**)
-val (bstep_rules, bstep_ind, bstep_cases) = Hol_reln `
+Inductive bstep:
(!m m' x e s E v res Gamma.
eval_expr E Gamma e v m /\
Gamma (Var x) = SOME m ∧
@@ -35,73 +38,79 @@ val (bstep_rules, bstep_ind, bstep_cases) = Hol_reln `
bstep (Let m x e s) E Gamma res m') /\
(!m e E v Gamma.
eval_expr E Gamma e v m ==>
- bstep (Ret e) E Gamma v m)`;
+ bstep (Ret e) E Gamma v m)
+End
(**
Generate a better case lemma
**)
-val bstep_cases =
+Theorem bstep_cases =
map (GEN_ALL o SIMP_CONV (srw_ss()) [Once bstep_cases])
[``bstep (Let m x e s) E defVars vR m'``,
- ``bstep (Ret e) E defVars vR m``]
- |> LIST_CONJ |> curry save_thm "bstep_cases";
+ ``bstep (Ret e) E defVars vR m``] |> LIST_CONJ
val [let_b, ret_b] = CONJ_LIST 2 bstep_rules;
-save_thm ("let_b", let_b);
-save_thm ("ret_b", ret_b);
+Theorem let_b = let_b
+Theorem ret_b = ret_b
(**
The free variables of a command are all used variables of exprressions
without the let bound variables
**)
-val freeVars_def = Define `
+Definition freeVars_def:
freeVars (f: 'a cmd) :num_set =
case f of
|Let m x e g => delete x (union (usedVars e) (freeVars g))
- |Ret e => usedVars e`;
+ |Ret e => usedVars e
+End
(**
The defined variables of a command are all let bound variables
**)
-val definedVars_def = Define `
+Definition definedVars_def:
definedVars (f:'a cmd) :num_set =
case f of
|Let m (x:num) e g => insert x () (definedVars g)
- |Ret e => LN`;
+ |Ret e => LN
+End
-val bstep_eq_env = store_thm (
- "bstep_eq_env",
- ``!f E1 E2 Gamma v m.
+Theorem bstep_eq_env:
+ !f E1 E2 Gamma v m.
(!x. E1 x = E2 x) /\
bstep f E1 Gamma v m ==>
- bstep f E2 Gamma v m``,
+ bstep f E2 Gamma v m
+Proof
Induct \\ rpt strip_tac \\ fs[bstep_cases]
>- (qexists_tac `v'` \\ conj_tac
\\ TRY (drule eval_eq_env \\ disch_then drule \\ fs[] \\ FAIL_TAC"")
\\ first_x_assum irule \\ qexists_tac `updEnv n v' E1` \\ fs[]
\\ rpt strip_tac \\ fs[updEnv_def])
- \\ irule eval_eq_env \\ asm_exists_tac \\ fs[]);
+ \\ irule eval_eq_env \\ asm_exists_tac \\ fs[]
+QED
-val swap_Gamma_bstep = store_thm (
- "swap_Gamma_bstep",
- ``!f E vR m Gamma1 Gamma2.
+Theorem swap_Gamma_bstep:
+ !f E vR m Gamma1 Gamma2.
(! e. Gamma1 e = Gamma2 e) /\
bstep f E Gamma1 vR m ==>
- bstep f E Gamma2 vR m``,
+ bstep f E Gamma2 vR m
+Proof
Induct_on `f` \\ rpt strip_tac \\ fs[bstep_cases]
- \\ metis_tac [swap_Gamma_eval_expr]);
+ \\ metis_tac [swap_Gamma_eval_expr]
+QED
-val bstep_Gamma_det = store_thm (
- "bstep_Gamma_det",
- ``!f E1 E2 Gamma v1 v2 m1 m2.
+Theorem bstep_Gamma_det:
+ !f E1 E2 Gamma v1 v2 m1 m2.
bstep f E1 Gamma v1 m1 /\
bstep f E2 Gamma v2 m2 ==>
- m1 = m2``,
+ m1 = m2
+Proof
Induct_on `f` \\ rpt strip_tac \\ fs[bstep_cases]
- \\ metis_tac[Gamma_det]);
+ \\ metis_tac[Gamma_det]
+QED
-val getRetExp_def = Define `
+Definition getRetExp_def:
(getRetExp (Let m x e g) = getRetExp g) /\
-(getRetExp (Ret e) = e)`;
+(getRetExp (Ret e) = e)
+End
val _ = export_theory ();
diff --git a/hol4/semantics/ExpressionAbbrevsScript.sml b/hol4/semantics/ExpressionAbbrevsScript.sml
index 32ab3bb1ca7851c296ebf3b5e487f38467baf9b7..49bfd1cf5f9b3a2d5cf79bc832d7f14320f38beb 100644
--- a/hol4/semantics/ExpressionAbbrevsScript.sml
+++ b/hol4/semantics/ExpressionAbbrevsScript.sml
@@ -13,60 +13,69 @@ We treat a function mapping an exprression arguing on fractions as value type
to pairs of intervals on rationals and rational errors as the analysis result
**)
-val _ = type_abbrev ("fMap", ``:(real expr # 'a) binTree``);
-val _ = type_abbrev ("typeMap", ``:mType fMap``);
-val _ = type_abbrev ("analysisResult", ``:((real # real) # real) fMap``);
+Type fMap = ``:(real expr # 'a) binTree``
+Type typeMap = ``:mType fMap``
+Type analysisResult = ``:((real # real) # real) fMap``
-val updDefVars_def = Define `
+Definition updDefVars_def:
updDefVars (x:real expr) (m:mType) (defVars:real expr -> mType option)
(y:real expr) :mType option =
- if y = x then SOME m else defVars y`;
+ if y = x then SOME m else defVars y
+End
-val toRExpMap_def = Define `
+Definition toRExpMap_def:
toRExpMap (tMap:typeMap) =
- \e. FloverMapTree_find e tMap`;
+ \e. FloverMapTree_find e tMap
+End
-val toRTMap_def = Define `
+Definition toRTMap_def:
toRTMap (Gamma: real expr -> mType option) (Var v) =
(case Gamma (Var v) of
|SOME m => SOME REAL
|_ => NONE) /\
- toRTMap tMap e = SOME REAL`;
+ toRTMap tMap e = SOME REAL
+End
+Theorem no_cycle_unop:
+ !e u. e <> Unop u e
+Proof
+ Induct_on `e` \\ fs[expr_distinct]
+QED
-val no_cycle_unop = store_thm (
- "no_cycle_unop",
- ``!e u. e <> Unop u e``,
- Induct_on `e` \\ fs[expr_distinct]);
+Theorem no_cycle_cast:
+ !e m. e <> Downcast m e
+Proof
+ Induct_on `e` \\ fs[expr_distinct]
+QED
-val no_cycle_cast = store_thm (
- "no_cycle_cast",
- ``!e m. e <> Downcast m e``,
- Induct_on `e` \\ fs[expr_distinct])
+Theorem no_cycle_binop_left:
+ !e1 e2 b. e1 <> Binop b e1 e2
+Proof
+ Induct_on `e1` \\ fs[expr_distinct]
+QED
-val no_cycle_binop_left = store_thm (
- "no_cycle_binop_left",
- ``!e1 e2 b. e1 <> Binop b e1 e2``,
- Induct_on `e1` \\ fs[expr_distinct]);
+Theorem no_cycle_binop_right:
+ !e1 e2 b. e2 <> Binop b e1 e2
+Proof
+ Induct_on `e2` \\ fs[expr_distinct]
+QED
-val no_cycle_binop_right = store_thm (
- "no_cycle_binop_right",
- ``!e1 e2 b. e2 <> Binop b e1 e2``,
- Induct_on `e2` \\ fs[expr_distinct]);
+Theorem no_cycle_fma_left:
+ !e1 e2 e3. e1 <> Fma e1 e2 e3
+Proof
+ Induct_on `e1` \\ fs[expr_distinct]
+QED
-val no_cycle_fma_left = store_thm (
- "no_cycle_fma_left",
- ``!e1 e2 e3. e1 <> Fma e1 e2 e3``,
- Induct_on `e1` \\ fs[expr_distinct]);
+Theorem no_cycle_fma_center:
+ !e1 e2 e3. e2 <> Fma e1 e2 e3
+Proof
+ Induct_on `e2` \\ fs[expr_distinct]
+QED
-val no_cycle_fma_center = store_thm (
- "no_cycle_fma_center",
- ``!e1 e2 e3. e2 <> Fma e1 e2 e3``,
- Induct_on `e2` \\ fs[expr_distinct]);
-
-val no_cycle_fma_right = store_thm (
- "no_cycle_fma_right",
- ``!e1 e2 e3. e3 <> Fma e1 e2 e3``,
- Induct_on `e3` \\ fs[expr_distinct]);
+Theorem no_cycle_fma_right:
+ !e1 e2 e3. e3 <> Fma e1 e2 e3
+Proof
+ Induct_on `e3` \\ fs[expr_distinct]
+QED
val _ = export_theory()
diff --git a/hol4/semantics/ExpressionSemanticsScript.sml b/hol4/semantics/ExpressionSemanticsScript.sml
index 2df3c51bea3b53bb3fe7adb572bb99ce2eb4dfbb..04695592c5ff56faa303fe82d551e3816db5c38a 100644
--- a/hol4/semantics/ExpressionSemanticsScript.sml
+++ b/hol4/semantics/ExpressionSemanticsScript.sml
@@ -8,7 +8,8 @@ open preambleFloVer;
val _ = new_theory "ExpressionSemantics";
-val _ = temp_overload_on("abs",``real$abs``);
+Overload abs = “real$absâ€
+
(**
Define a perturbation function to ease writing of basic definitions
**)
@@ -94,8 +95,7 @@ Theorem eval_expr_cases =
``eval_expr E Gamma (Unop u e) res m``,
``eval_expr E Gamma (Binop n e1 e2) res m``,
``eval_expr E Gamma (Fma e1 e2 e3) res m``,
- ``eval_expr E Gamma (Downcast m1 e1) res m2``]
- |> LIST_CONJ |> curry save_thm "eval_expr_cases";
+ ``eval_expr E Gamma (Downcast m1 e1) res m2``] |> LIST_CONJ
val [Var_load, Const_dist, Unop_neg, Unop_inv, Unop_sqrt, Downcast_dist, Binop_dist, Fma_dist] =
CONJ_LIST 8 eval_expr_rules;
diff --git a/hol4/semantics/ExpressionsScript.sml b/hol4/semantics/ExpressionsScript.sml
index 0283cdbedfe9e217bc23ed2c60140098a8a92a53..c414409381fcf5d54cfd9e500e9a6b6613ac430b 100644
--- a/hol4/semantics/ExpressionsScript.sml
+++ b/hol4/semantics/ExpressionsScript.sml
@@ -7,30 +7,34 @@ open preambleFloVer;
val _ = new_theory "Expressions";
-val _ = temp_overload_on("abs",``real$abs``);
+Overload abs = “real$absâ€
+
(**
- EXPRESSIONS WILL use binary operators.
+ expressions will use binary operators.
Define them first
**)
-val _ = Datatype `
- binop = Plus | Sub | Mult | Div`;
+Datatype:
+ binop = Plus | Sub | Mult | Div
+End
(**
Next define an evaluation function for binary operators.
Errors are added on the exprression evaluation level later
*)
-val evalBinop_def = Define `
+Definition evalBinop_def:
evalBinop Plus v1 v2 = v1 + v2 /\
evalBinop Sub v1 v2 = v1 - v2 /\
evalBinop Mult v1 v2 = v1 * v2 /\
- evalBinop Div v1 v2 = v1 / (v2:real)`;
+ evalBinop Div v1 v2 = v1 / (v2:real)
+End
(**
Expressions will use unary operators.
Define them first
**)
-val _ = Datatype `
- unop = Neg | Inv | Sqrt`
+Datatype:
+ unop = Neg | Inv | Sqrt
+End
(**
Define evaluation for unary operators on reals.
@@ -94,48 +98,4 @@ Definition usedVars_def:
| _ => LN
End
-(* (** *)
-(* Analogous lemma for unary exprressions *)
-(* **) *)
-(* val unary_unfolding = store_thm("unary_unfolding", *)
-(* ``!(u:unop) (e1:(real)expr) (m:mType) E defVars (v:real). *)
-(* (eval_expr E defVars (Unop Inv e1) v m <=> *)
-(* (?(v1:real). *)
-(* eval_expr E defVars e1 v1 m /\ *)
-(* eval_expr (updEnv 1 v1 emptyEnv) (updDefVars 1 m defVars) (Unop Inv (Var 1)) v m))``, *)
-(* fs [updEnv_def, updDefVars_def, eval_expr_cases,APPLY_UPDATE_THM,PULL_EXISTS] *)
-(* \\ metis_tac []); *)
-
-(*
- Using the parametric Expressions, define boolean Expressions for conditionals
-*)
-(* val _ = Datatype ` *)
-(* bexpr = Leq ('v expr) ('v expr) *)
-(* | Less ('v expr) ('v expr)` *)
-
-(*
- Define evaluation of boolean exprressions
-*)
-(* val (bval_expr_rules, bval_expr_ind, bval_expr_cases) = Hol_reln ` *)
-(* (!E defVars e1 e2 v1 v2 m. *)
-(* eval_expr E defVars e1 v1 m /\ *)
-(* eval_expr E defVars e2 v2 m ==> *)
-(* bval E defVars m (Leq e1 e2) (v1 <= v2))/\ *)
-(* (!E defVars e1 e2 v1 v2 m. *)
-(* eval_expr E defVars e1 v1 m /\ *)
-(* eval_expr E defVars e2 v2 m ==> *)
-(* bval E defVars m (Less e1 e2) (v1 < v2))`; *)
-
-(* val bval_expr_cases = *)
-(* map (GEN_ALL o SIMP_CONV (srw_ss()) [Once bval_expr_cases]) *)
-(* [``bval E defVars m (Leq e1 e2) res``, *)
-(* ``bval E defVars m (Less e1 e2) res``] *)
-(* |> LIST_CONJ |> curry save_thm "bval_expr_cases"; *)
-
-(* (** *)
-(* Simplify arithmetic later by making > >= only abbreviations *)
-(* **) *)
-(* val _ = overload_on("Gr",``\(e1:('v)expr). \(e2:('v)expr). Less e2 e1``); *)
-(* val _ = overload_on("Greq",``\(e1:('v)expr). \(e2:('v)expr). Leq e2 e1``); *)
-
val _ = export_theory();
diff --git a/hol4/semantics/FloverMapScript.sml b/hol4/semantics/FloverMapScript.sml
index 11eb1e741d3d94068793461f6ff7df73e6cff790..cb39352458c5278ac52c59e88c84f579d106b742 100644
--- a/hol4/semantics/FloverMapScript.sml
+++ b/hol4/semantics/FloverMapScript.sml
@@ -1,12 +1,17 @@
+(**
+ A simple Map datatype for FloVer, implement a version based on lists and one
+ based on trees
+**)
open MachineTypeTheory ExpressionsTheory;
open preambleFloVer;
val _ = new_theory "FloverMap";
-val _ = Datatype `
- cmp = Lt | Eq | Gt`;
+Datatype:
+ cmp = Lt | Eq | Gt
+End
-val exprCompare_def = Define `
+Definition exprCompare_def:
exprCompare (e1:real expr) e2 =
case e1, e2 of
|(Var (n1:num)), (Var n2) =>
@@ -71,30 +76,36 @@ val exprCompare_def = Define `
| Gt => Gt)
| _ , Fma e1 e2 e3 => Lt
| Fma e1 e2 e3, _ => Gt
- |_ , _ => Gt`;
+ |_ , _ => Gt
+End
-val exprCompare_refl = store_thm (
- "exprCompare_refl",
- ``!e. exprCompare e e = Eq``,
+Theorem exprCompare_refl:
+ !e. exprCompare e e = Eq
+Proof
Induct \\ rpt strip_tac \\ simp[ Once exprCompare_def]
- \\ Cases_on `b` \\ fs[] );
+ \\ Cases_on `b` \\ fs[]
+QED
-val FloverMapList_insert_def = Define `
+Definition FloverMapList_insert_def:
(FloverMapList_insert e k NIL = [(e,k)]) /\
(FloverMapList_insert e k ((e1,l1) :: el) =
case exprCompare e e1 of
| Lt => (e,k)::(e1,l1)::el
| Eq => (e1,l1) :: el
- | Gt => (e1,l1):: FloverMapList_insert e k el)`;
+ | Gt => (e1,l1):: FloverMapList_insert e k el)
+End
-val FloverMapList_find_def = Define `
+Definition FloverMapList_find_def:
(FloverMapList_find e NIL = NONE) /\
- (FloverMapList_find e ((e1,k)::el) = if exprCompare e e1 = Eq then SOME k else FloverMapList_find e el)`;
+ (FloverMapList_find e ((e1,k)::el) = if exprCompare e e1 = Eq then SOME k
+ else FloverMapList_find e el)
+End
-val _ = Datatype `
- binTree = Node 'a binTree binTree | Leaf 'a | LeafN`;
+Datatype:
+ binTree = Node 'a binTree binTree | Leaf 'a | LeafN
+End
-val FloverMapTree_insert_def = Define `
+Definition FloverMapTree_insert_def:
(FloverMapTree_insert e k LeafN = Leaf (e,k)) /\
(FloverMapTree_insert e k (Leaf (e1,k1)) =
case (exprCompare e e1) of
@@ -105,9 +116,10 @@ val FloverMapTree_insert_def = Define `
case (exprCompare e e1) of
| Lt => Node (e1,k1) (FloverMapTree_insert e k tl) tr
| Eq => (Node (e1, k) tl tr)
- | Gt => Node (e1,k1) tl (FloverMapTree_insert e k tr))`;
+ | Gt => Node (e1,k1) tl (FloverMapTree_insert e k tr))
+End
-val FloverMapTree_find_def = Define `
+Definition FloverMapTree_find_def:
(FloverMapTree_find e (LeafN) = NONE) /\
(FloverMapTree_find e (Leaf (e1,k1)) =
if exprCompare e e1 = Eq then SOME k1 else NONE) /\
@@ -115,30 +127,34 @@ val FloverMapTree_find_def = Define `
case (exprCompare e e1) of
| Lt => FloverMapTree_find e tl
| Eq => SOME k1
- | Gt => FloverMapTree_find e tr)`;
+ | Gt => FloverMapTree_find e tr)
+End
-val FloverMapTree_mem_def = Define `
+Definition FloverMapTree_mem_def:
FloverMapTree_mem e tMap =
case (FloverMapTree_find e tMap) of
| SOME _ => T
- | _ => F`;
+ | _ => F
+End
-val FloverMapTree_empty_def = Define `
- FloverMapTree_empty = LeafN `;
+Definition FloverMapTree_empty_def:
+ FloverMapTree_empty = LeafN
+End
-val FloverMapTree_find_injective = store_thm (
- "FloverMapTree_find_injective",
- ``!e a b Tree.
+Theorem FloverMapTree_find_injective:
+ !e a b Tree.
FloverMapTree_find e Tree = SOME a /\
FloverMapTree_find e Tree = SOME b ==>
- a = b``,
+ a = b
+Proof
rpt strip_tac
- \\ Cases_on `Tree` \\ fs[FloverMapTree_find_def]);
+ \\ Cases_on `Tree` \\ fs[FloverMapTree_find_def]
+QED
-val FloverMapTree_correct = store_thm (
- "FloverMapTree_correct",
- ``!Tree k v.
- FloverMapTree_find k (FloverMapTree_insert k v Tree) = SOME v``,
+Theorem FloverMapTree_correct:
+ !Tree k v.
+ FloverMapTree_find k (FloverMapTree_insert k v Tree) = SOME v
+Proof
Induct_on `Tree`
\\ fs[FloverMapTree_find_def, FloverMapTree_insert_def]
\\ rpt strip_tac \\ fs[exprCompare_refl]
@@ -146,11 +162,12 @@ val FloverMapTree_correct = store_thm (
\\ Cases_on `exprCompare k q` \\ fs[FloverMapTree_find_def]
\\ first_x_assum irule \\ fs[])
\\ Cases_on `a` \\ fs[FloverMapTree_insert_def]
- \\ Cases_on `exprCompare k q` \\ fs[FloverMapTree_find_def, exprCompare_refl]);
+ \\ Cases_on `exprCompare k q` \\ fs[FloverMapTree_find_def, exprCompare_refl]
+QED
-val exprCompare_eq = store_thm (
- "exprCompare_eq",
- ``!e1 e2. exprCompare e1 e2 = Eq <=> e1 = e2``,
+Theorem exprCompare_eq:
+ !e1 e2. exprCompare e1 e2 = Eq <=> e1 = e2
+Proof
Induct_on `e1` \\ Cases_on `e2` \\ simp[Once exprCompare_def] \\ rpt strip_tac
>- (EVERY_CASE_TAC \\ fs[])
>- (EVERY_CASE_TAC \\ fs[])
@@ -165,11 +182,12 @@ val exprCompare_eq = store_thm (
\\ first_x_assum (qspec_then `e` assume_tac)
\\ EVERY_CASE_TAC \\ fs[])
\\ first_x_assum (qspec_then `e` assume_tac)
- \\ every_case_tac \\ fs[]);
+ \\ every_case_tac \\ fs[]
+QED
-val exprCompare_neq = store_thm (
- "exprCompare_neq",
- ``!e1 e2. exprCompare e1 e2 <> Eq <=> e1 <> e2``,
+Theorem exprCompare_neq:
+ !e1 e2. exprCompare e1 e2 <> Eq <=> e1 <> e2
+Proof
Induct_on `e1` \\ Cases_on `e2` \\ simp[Once exprCompare_def] \\ rpt strip_tac
>- (EVERY_CASE_TAC \\ fs[])
>- (EVERY_CASE_TAC \\ fs[])
@@ -184,15 +202,16 @@ val exprCompare_neq = store_thm (
\\ first_x_assum (qspec_then `e` assume_tac)
\\ EVERY_CASE_TAC \\ fs[])
\\ first_x_assum (qspec_then `e` assume_tac)
- \\ every_case_tac \\ fs[]);
+ \\ every_case_tac \\ fs[]
+QED
-val map_find_add = store_thm (
- "map_find_add",
- ``! e1 e2 m map1.
+Theorem map_find_add:
+ ! e1 e2 m map1.
FloverMapTree_find e1 (FloverMapTree_insert e2 m map1) =
if (e1 = e2)
then SOME m
- else FloverMapTree_find e1 map1``,
+ else FloverMapTree_find e1 map1
+Proof
Induct_on `map1` \\ rpt strip_tac
\\ fs[FloverMapTree_insert_def, FloverMapTree_find_def, exprCompare_eq]
>- (Cases_on `a` \\ fs[FloverMapTree_insert_def]
@@ -228,14 +247,16 @@ val map_find_add = store_thm (
>- (Cases_on `e1 = e2` \\ fs[])
\\ `e2 <> e1`
by (Cases_on `exprCompare e2 e1 = Eq` \\ fs[exprCompare_neq])
- \\ fs[]);
+ \\ fs[]
+QED
-val map_mem_add = store_thm (
- "map_mem_add",
- ``!e1 e2 m map1.
+Theorem map_mem_add:
+ !e1 e2 m map1.
FloverMapTree_mem e1 (FloverMapTree_insert e2 m map1) =
- (e1 = e2 \/ FloverMapTree_mem e1 map1)``,
+ (e1 = e2 \/ FloverMapTree_mem e1 map1)
+Proof
fs[FloverMapTree_mem_def, map_find_add]
- \\ rpt strip_tac \\ Cases_on `e1 = e2` \\ fs[]);
+ \\ rpt strip_tac \\ Cases_on `e1 = e2` \\ fs[]
+QED
val _ = export_theory();
diff --git a/hol4/sqrtApproxScript.sml b/hol4/sqrtApproxScript.sml
index d15f2768d4ecd9f7f4449e52ff38ebfc44bc69a4..c43e1813fa266bac6134a452b1313b2730535994 100644
--- a/hol4/sqrtApproxScript.sml
+++ b/hol4/sqrtApproxScript.sml
@@ -1,3 +1,9 @@
+(**
+ Simple approximation of sqrt as it is not computable in HOL4 using
+ newton iterations.
+ As the iteration may fail, the process "self-validates", checkign that
+ the result is an over/under-approximation of the real sqrt
+**)
open transcTheory realTheory realLib RealArith bossLib limTheory;
open preambleFloVer;
diff --git a/hol4/ssaPrgsScript.sml b/hol4/ssaPrgsScript.sml
index 447e43146ee6c6f3d64fcba664959f004232b12d..a1677d98ea90bb4e85cc0da4cf10f789c5a03edc 100644
--- a/hol4/ssaPrgsScript.sml
+++ b/hol4/ssaPrgsScript.sml
@@ -1,9 +1,10 @@
(**
We define a pseudo SSA predicate.
- The formalization is similar to the renamedApart property in the LVC framework by Schneider, Smolka and Hack
- http://dblp.org/rec/conf/itp/SchneiderSH15
- Our predicate is not as fully fledged as theirs, but we especially borrow the idea of annotating
- the program with the predicate with the set of free and defined variables
+ The formalization is similar to the renamedApart property in the LVC framework
+ by Schneider, Smolka and Hack (http://dblp.org/rec/conf/itp/SchneiderSH15)
+ Our predicate is not as fully fledged as theirs, but we especially borrow the
+ idea of annotating the program with the predicate with the set of free and
+ defined variables
**)
open pred_setSyntax pred_setTheory;
open AbbrevsTheory ExpressionsTheory ExpressionAbbrevsTheory FloverTactics
@@ -12,11 +13,13 @@ open preambleFloVer;
val _ = new_theory "ssaPrgs";
-val validVars_add = store_thm("validVars_add",
-``!(e:'a expr) Vs n.
+Theorem validVars_add:
+ !(e:'a expr) Vs n.
domain (usedVars e) ⊆ domain Vs ==>
- domain (usedVars e) ⊆ domain (insert n () Vs)``,
-fs [domain_insert, SUBSET_DEF]);
+ domain (usedVars e) ⊆ domain (insert n () Vs)
+Proof
+ fs [domain_insert, SUBSET_DEF]
+QED
(**
Inductive ssa predicate, following the definitions from the LVC framework,
@@ -24,7 +27,7 @@ fs [domain_insert, SUBSET_DEF]);
We maintain as an invariant that if we have
ssa f
**)
-val (ssa_rules, ssa_ind, ssa_cases) = Hol_reln `
+Inductive ssa:
(!m x e s inVars (Vterm:num_set).
(domain (usedVars e)) SUBSET (domain inVars) /\
(~ (x IN (domain inVars))) /\
@@ -33,25 +36,27 @@ val (ssa_rules, ssa_ind, ssa_cases) = Hol_reln `
(!e inVars Vterm.
(domain (usedVars e)) SUBSET (domain inVars) /\
(domain inVars = domain Vterm) ==>
- ssa (Ret e) inVars Vterm)`;
+ ssa (Ret e) inVars Vterm)
+End
(*
As usual
*)
-val ssa_cases =
+Theorem ssa_cases =
map (GEN_ALL o SIMP_CONV (srw_ss()) [Once ssa_cases])
[``ssa (Let m x e s) inVars Vterm``,
- ``ssa (Ret e) inVars Vterm``]
- |> LIST_CONJ |> curry save_thm "ssa_cases";
+ ``ssa (Ret e) inVars Vterm``] |> LIST_CONJ;
val [ssaLet, ssaRet] = CONJ_LIST 2 ssa_rules;
-save_thm ("ssaLet",ssaLet);
-save_thm ("ssaRet",ssaRet);
-val ssa_subset_freeVars = store_thm ("ssa_subset_freeVars",
- ``!(f:'a cmd) inVars outVars.
+Theorem ssaLet = ssaLet
+Theorem ssaRet = ssaRet
+
+Theorem ssa_subset_freeVars:
+ !(f:'a cmd) inVars outVars.
ssa f inVars outVars ==>
- (domain (freeVars f)) SUBSET (domain inVars)``,
+ (domain (freeVars f)) SUBSET (domain inVars)
+Proof
ho_match_mp_tac ssa_ind \\ rw []
>- (once_rewrite_tac [freeVars_def, domain_insert] \\ simp []
\\ once_rewrite_tac [domain_union]
@@ -62,14 +67,16 @@ val ssa_subset_freeVars = store_thm ("ssa_subset_freeVars",
>- (fs [ domain_insert]
\\ metis_tac[]))
>- (once_rewrite_tac[freeVars_def]
- \\ fs []));
+ \\ fs [])
+QED
-val ssa_equal_set_ind = prove(
- ``!(f:'a cmd) inVars outVars.
+Theorem ssa_equal_set_ind:
+ !(f:'a cmd) inVars outVars.
ssa f inVars outVars ==>
(!inVars'.
(domain inVars' = domain inVars) ==>
- ssa f inVars' outVars)``,
+ ssa f inVars' outVars)
+Proof
qspec_then `\f inVars outVars.
!inVars'. (domain inVars' = domain inVars) ==> ssa f inVars' outVars`
(fn thm => assume_tac (SIMP_RULE std_ss [] thm)) ssa_ind
@@ -78,20 +85,23 @@ val ssa_equal_set_ind = prove(
>- (match_mp_tac ssaLet \\ fs[]
\\ first_x_assum match_mp_tac
\\ simp[ domain_insert])
- >- (match_mp_tac ssaRet \\ fs[]));
+ >- (match_mp_tac ssaRet \\ fs[])
+QED
-val ssa_equal_set = store_thm ("ssa_equal_set",
- ``!(f:'a cmd) inVars outVars inVars'.
+Theorem ssa_equal_set:
+ !(f:'a cmd) inVars outVars inVars'.
(domain inVars' = domain inVars) /\
ssa f inVars outVars ==>
- ssa f inVars' outVars``,
+ ssa f inVars' outVars
+Proof
rpt strip_tac
\\ qspecl_then [`f`, `inVars`, `outVars`] assume_tac ssa_equal_set_ind
\\ specialize `ssa _ _ _ ==> _` `ssa f inVars outVars`
\\ specialize `!inVars'. A ==> B` `inVars'`
- \\ first_x_assum match_mp_tac \\ fs[]);
+ \\ first_x_assum match_mp_tac \\ fs[]
+QED
-val validSSA_def = Define `
+Definition validSSA_def:
validSSA (f:real cmd) (inVars:num_set) =
case f of
|Let m x e g =>
@@ -99,13 +109,15 @@ val validSSA_def = Define `
(subspt (usedVars e) inVars) /\
(validSSA g (insert x () inVars)))
|Ret e =>
- (subspt (usedVars e) inVars)`;
+ (subspt (usedVars e) inVars)
+End
-val validSSA_sound = store_thm ("validSSA_sound",
- ``!(f:real cmd) (inVars:num_set).
+Theorem validSSA_sound:
+ !(f:real cmd) (inVars:num_set).
(validSSA f inVars) ==>
?outVars.
- ssa f inVars outVars``,
+ ssa f inVars outVars
+Proof
Induct \\ once_rewrite_tac [validSSA_def] \\ rw[]
>- (specialize `!inVars. _ ==> _` `insert n () inVars`
\\ `?outVars. ssa f (insert n () inVars) outVars` by (first_x_assum match_mp_tac \\ simp[])
@@ -114,21 +126,22 @@ val validSSA_sound = store_thm ("validSSA_sound",
\\ fs [subspt_def, SUBSET_DEF, lookup_NONE_domain])
>- (exists_tac ``inVars:num_set``
\\ match_mp_tac ssaRet
- \\ fs[subspt_def, SUBSET_DEF]));
+ \\ fs[subspt_def, SUBSET_DEF])
+QED
-val ssa_shadowing_free = store_thm ("ssa_shadowing_free",
- ``!m x y v v' e f inVars outVars E Gamma.
+Theorem ssa_shadowing_free:
+ !m x y v v' e f inVars outVars E Gamma.
ssa (Let m x (toREval e) (toREvalCmd f)) inVars outVars /\
(y IN (domain inVars)) /\
eval_expr E Gamma (toREval e) v REAL ==>
- !E n. updEnv x v (updEnv y v' E) n = updEnv y v' (updEnv x v E) n``,
+ !E n. updEnv x v (updEnv y v' E) n = updEnv y v' (updEnv x v E) n
+Proof
rpt strip_tac
\\ inversion `ssa (Let m x (toREval e) (toREvalCmd f)) _ _` ssa_cases
\\ fs[updEnv_def]
- \\ Cases_on `n = x` \\ rveq
- >- (simp[]
- \\ Cases_on `n = y` \\ rveq \\ rw[]
- \\ metis_tac[])
- >- (simp[]));
+ \\ Cases_on `n = x` \\ rveq \\ simp[]
+ \\ Cases_on `n = y` \\ rveq \\ rw[]
+ \\ metis_tac[]
+QED
val _ = export_theory ();