From 235966b1ef3350fbdbf3427851115491479827ff Mon Sep 17 00:00:00 2001
From: Heiko Becker <hbecker@mpi-sws.org>
Date: Thu, 21 Jan 2021 17:47:56 +0100
Subject: [PATCH] Rework infrastructure a bit
---
hol4/ErrorValidationScript.sml | 292 +++++++++---------
hol4/FloverTactics.sml | 147 +++++++++
hol4/Holmakefile | 2 +-
hol4/Infra/FloverTactics.sml | 233 --------------
hol4/Infra/RealSimpsScript.sml | 3 +-
hol4/IntervalArithScript.sml | 16 +-
hol4/IntervalValidationScript.sml | 54 ++--
hol4/TypeValidatorScript.sml | 2 -
hol4/{ => semantics}/AbbrevsScript.sml | 0
hol4/{ => semantics}/CommandsScript.sml | 0
.../ExpressionAbbrevsScript.sml | 1 +
.../ExpressionSemanticsScript.sml | 5 +-
hol4/{ => semantics}/ExpressionsScript.sml | 2 +-
hol4/{ => semantics}/FloverMapScript.sml | 2 +-
hol4/semantics/Holmakefile | 2 +
{hol4 => scripts}/configure_hol.sh | 0
{hol4 => scripts}/find_cheats.sh | 0
17 files changed, 337 insertions(+), 424 deletions(-)
create mode 100644 hol4/FloverTactics.sml
delete mode 100644 hol4/Infra/FloverTactics.sml
rename hol4/{ => semantics}/AbbrevsScript.sml (100%)
rename hol4/{ => semantics}/CommandsScript.sml (100%)
rename hol4/{ => semantics}/ExpressionAbbrevsScript.sml (99%)
rename hol4/{ => semantics}/ExpressionSemanticsScript.sml (98%)
rename hol4/{ => semantics}/ExpressionsScript.sml (98%)
rename hol4/{ => semantics}/FloverMapScript.sml (99%)
create mode 100644 hol4/semantics/Holmakefile
rename {hol4 => scripts}/configure_hol.sh (100%)
rename {hol4 => scripts}/find_cheats.sh (100%)
diff --git a/hol4/ErrorValidationScript.sml b/hol4/ErrorValidationScript.sml
index 88b79df7..9006a7ba 100644
--- a/hol4/ErrorValidationScript.sml
+++ b/hol4/ErrorValidationScript.sml
@@ -117,9 +117,8 @@ Definition validErrorbound_def:
else F)
End
-add_unevaluated_function ``validErrorbound``;
-add_unevaluated_function ``minAbsFun``;
-add_unevaluated_function ``noDivzero``;
+Theorem validErrorbound_eq =
+ SIMP_CONV flover_ss [Once validErrorbound_def] (Parse.Term ‘validErrorbound e Gamma A dVars’)
Definition validErrorboundCmd_def:
validErrorboundCmd (f:real cmd) (typeMap: (real expr # mType) binTree)
@@ -136,7 +135,8 @@ Definition validErrorboundCmd_def:
validErrorbound e typeMap A dVars
End
-add_unevaluated_function ``validErrorboundCmd``;
+Theorem validErrorboundCmd_eq =
+ SIMP_CONV flover_ss [Once validErrorboundCmd_def] (Parse.Term ‘validErrorboundCmd f Gamma A dVars’)
Definition eval_Real_def:
eval_Real E1 Gamma e nR =
@@ -186,10 +186,6 @@ Proof
\\ fs[eval_expr_cases, toRExpMap_def, toRTMap_def, option_case_eq]
QED
-add_unevaluated_function ``computeError``;
-add_unevaluated_function ``maxAbs``;
-add_unevaluated_function “normalâ€;
-
Theorem validErrorboundCorrectVariable:
∀ (E1 E2:env) A fVars dVars (v:num) (nR nF err nlo nhi:real) (P:precond) m
Gamma.
@@ -209,12 +205,13 @@ Proof
\\ fs[toREval_def]
\\ rpt (inversion `eval_expr _ _ _ _ _` eval_expr_cases)
\\ qpat_x_assum `validErrorbound _ _ _ _` mp_tac
- \\ simp[validErrorbound_def] \\ TOP_CASE_TAC \\ fs[]
+ \\ simp[Once validErrorbound_eq]
\\ rpt strip_tac \\ fs[]
>- (drule approxEnv_dVar_bounded
- \\ rpt (disch_then drule)
- \\ disch_then (qspecl_then [`m`, `(nlo,nhi)`, `e`] irule)
+ \\ rpt (disch_then drule) \\ rveq
+ \\ disch_then (qspecl_then [`m`, `(nlo,nhi)`, `err`] irule)
\\ fs[domain_lookup])
+ \\ rveq
\\ fs[usedVars_def,domain_lookup]
\\ irule REAL_LE_TRANS \\ find_exists_tac \\ fs[]
\\ drule approxEnv_fVar_bounded
@@ -250,8 +247,7 @@ Theorem validErrorboundCorrectConstant:
FloverMapTree_find (Const m n) A = SOME ((nlo,nhi),e) ==>
(abs (nR - nF)) <= e
Proof
- rpt strip_tac \\ fs[toREval_def]
- \\ Flover_compute ``validErrorbound``
+ rpt strip_tac \\ fs[Once validErrorbound_eq, toREval_def]
\\ rveq \\ fs[validTypes_def] \\ rveq
\\ irule REAL_LE_TRANS
\\ find_exists_tac \\ fs[]
@@ -294,7 +290,7 @@ Theorem validErrorboundCorrectAddition:
abs (nR - nF) <= e
Proof
rpt strip_tac \\ simp[Once toREval_def]
- \\ Flover_compute ``validErrorbound`` \\ rveq
+ \\ fs[Once validErrorbound_eq] \\ rveq
\\ fs[toRExpMap_def]
\\ irule REAL_LE_TRANS
\\ qexists_tac `err1 + err2 + (computeError (nF1 + nF2) m)`
@@ -319,31 +315,32 @@ Proof
\\ fs[contained_def, widenInterval_def]
QED
-val validErrorboundCorrectSubtraction = store_thm ("validErrorboundCorrectSubtraction",
- ``!(E1 E2:env) (A:analysisResult) (e1:real expr) (e2:real expr)
- (nR nR1 nR2 nF nF1 nF2:real) (e err1 err2:real)
- (alo ahi e1lo e1hi e2lo e2hi:real) dVars m m1 m2 Gamma.
- eval_Real E1 Gamma e1 nR1 /\
- eval_Real E1 Gamma e2 nR2 /\
- eval_Real E1 Gamma (Binop Sub e1 e2) nR /\
- eval_Fin E2 Gamma e1 nF1 m1 /\
- eval_Fin E2 Gamma e2 nF2 m2 /\
- eval_expr (updEnv 2 nF2 (updEnv 1 nF1 emptyEnv))
- (updDefVars (Binop Sub (Var 1) (Var 2)) m
- (updDefVars (Var 2) m2 (updDefVars (Var 1) m1 (toRExpMap Gamma))))
- (Binop Sub (Var 1) (Var 2)) nF m /\
- validErrorbound (Binop Sub e1 e2) Gamma A dVars /\
- (e1lo <= nR1 /\ nR1 <= e1hi) /\
- (e2lo <= nR2 /\ nR2 <= e2hi) /\
- FloverMapTree_find e1 A = SOME ((e1lo, e1hi), err1) /\
- FloverMapTree_find e2 A = SOME ((e2lo, e2hi), err2) /\
- FloverMapTree_find (Binop Sub e1 e2) A = SOME ((alo, ahi), e) /\
- FloverMapTree_find (Binop Sub e1 e2) Gamma = SOME m /\
- abs (nR1 - nF1) <= err1 /\
- abs (nR2 - nF2) <= err2 ==>
- abs (nR - nF) <= e``,
+Theorem validErrorboundCorrectSubtraction:
+ !(E1 E2:env) (A:analysisResult) (e1:real expr) (e2:real expr)
+ (nR nR1 nR2 nF nF1 nF2:real) (e err1 err2:real)
+ (alo ahi e1lo e1hi e2lo e2hi:real) dVars m m1 m2 Gamma.
+ eval_Real E1 Gamma e1 nR1 /\
+ eval_Real E1 Gamma e2 nR2 /\
+ eval_Real E1 Gamma (Binop Sub e1 e2) nR /\
+ eval_Fin E2 Gamma e1 nF1 m1 /\
+ eval_Fin E2 Gamma e2 nF2 m2 /\
+ eval_expr (updEnv 2 nF2 (updEnv 1 nF1 emptyEnv))
+ (updDefVars (Binop Sub (Var 1) (Var 2)) m
+ (updDefVars (Var 2) m2 (updDefVars (Var 1) m1 (toRExpMap Gamma))))
+ (Binop Sub (Var 1) (Var 2)) nF m /\
+ validErrorbound (Binop Sub e1 e2) Gamma A dVars /\
+ (e1lo <= nR1 /\ nR1 <= e1hi) /\
+ (e2lo <= nR2 /\ nR2 <= e2hi) /\
+ FloverMapTree_find e1 A = SOME ((e1lo, e1hi), err1) /\
+ FloverMapTree_find e2 A = SOME ((e2lo, e2hi), err2) /\
+ FloverMapTree_find (Binop Sub e1 e2) A = SOME ((alo, ahi), e) /\
+ FloverMapTree_find (Binop Sub e1 e2) Gamma = SOME m /\
+ abs (nR1 - nF1) <= err1 /\
+ abs (nR2 - nF2) <= err2 ==>
+ abs (nR - nF) <= e
+Proof
rpt strip_tac \\ simp[Once toREval_def]
- \\ Flover_compute ``validErrorbound`` \\ rveq
+ \\ fs[Once validErrorbound_eq] \\ rveq
\\ irule REAL_LE_TRANS
\\ qexists_tac `err1 + err2 + computeError (nF1 - nF2) m`
\\ conj_tac
@@ -364,7 +361,8 @@ val validErrorboundCorrectSubtraction = store_thm ("validErrorboundCorrectSubtra
\\ qexists_tac `nR2` \\ conj_tac
\\ simp[contained_def])
\\ assume_tac (REWRITE_RULE [validIntervalSub_def, contained_def] interval_subtraction_valid)
- \\ fs[contained_def, widenInterval_def]);
+ \\ fs[contained_def, widenInterval_def]
+QED
local
val trivial_up_tac =
@@ -932,31 +930,32 @@ Proof
QED
end
-val validErrorboundCorrectMult = store_thm ("validErrorboundCorrectMult",
- ``!(E1 E2:env) (A:analysisResult) (e1:real expr) (e2:real expr)
- (nR nR1 nR2 nF nF1 nF2:real) (e err1 err2:real)
- (alo ahi e1lo e1hi e2lo e2hi :real) dVars m m1 m2 Gamma.
- eval_Real E1 Gamma e1 nR1 /\
- eval_Real E1 Gamma e2 nR2 /\
- eval_Real E1 Gamma (Binop Mult e1 e2) nR /\
- eval_Fin E2 Gamma e1 nF1 m1 /\
- eval_Fin E2 Gamma e2 nF2 m2 /\
- eval_expr (updEnv 2 nF2 (updEnv 1 nF1 emptyEnv))
- (updDefVars (Binop Mult (Var 1) (Var 2)) m
- (updDefVars (Var 2) m2 (updDefVars (Var 1) m1 (toRExpMap Gamma))))
- (Binop Mult (Var 1) (Var 2)) nF m /\
- validErrorbound (Binop Mult e1 e2) Gamma A dVars /\
- (e1lo <= nR1 /\ nR1 <= e1hi) /\
- (e2lo <= nR2 /\ nR2 <= e2hi) /\
- FloverMapTree_find e1 A = SOME ((e1lo, e1hi), err1) /\
- FloverMapTree_find e2 A = SOME ((e2lo, e2hi), err2) /\
- FloverMapTree_find (Binop Mult e1 e2) A = SOME ((alo, ahi), e) /\
- FloverMapTree_find (Binop Mult e1 e2) Gamma = SOME m /\
- abs (nR1 - nF1) <= err1 /\
- abs (nR2 - nF2) <= err2 ==>
- abs (nR - nF) <= e``,
+Theorem validErrorboundCorrectMult:
+ !(E1 E2:env) (A:analysisResult) (e1:real expr) (e2:real expr)
+ (nR nR1 nR2 nF nF1 nF2:real) (e err1 err2:real)
+ (alo ahi e1lo e1hi e2lo e2hi :real) dVars m m1 m2 Gamma.
+ eval_Real E1 Gamma e1 nR1 /\
+ eval_Real E1 Gamma e2 nR2 /\
+ eval_Real E1 Gamma (Binop Mult e1 e2) nR /\
+ eval_Fin E2 Gamma e1 nF1 m1 /\
+ eval_Fin E2 Gamma e2 nF2 m2 /\
+ eval_expr (updEnv 2 nF2 (updEnv 1 nF1 emptyEnv))
+ (updDefVars (Binop Mult (Var 1) (Var 2)) m
+ (updDefVars (Var 2) m2 (updDefVars (Var 1) m1 (toRExpMap Gamma))))
+ (Binop Mult (Var 1) (Var 2)) nF m /\
+ validErrorbound (Binop Mult e1 e2) Gamma A dVars /\
+ (e1lo <= nR1 /\ nR1 <= e1hi) /\
+ (e2lo <= nR2 /\ nR2 <= e2hi) /\
+ FloverMapTree_find e1 A = SOME ((e1lo, e1hi), err1) /\
+ FloverMapTree_find e2 A = SOME ((e2lo, e2hi), err2) /\
+ FloverMapTree_find (Binop Mult e1 e2) A = SOME ((alo, ahi), e) /\
+ FloverMapTree_find (Binop Mult e1 e2) Gamma = SOME m /\
+ abs (nR1 - nF1) <= err1 /\
+ abs (nR2 - nF2) <= err2 ==>
+ abs (nR - nF) <= e
+Proof
rpt strip_tac \\ simp[Once toREval_def]
- \\ Flover_compute ``validErrorbound`` \\ rveq
+ \\ fs[Once validErrorbound_eq] \\ rveq
\\ `0 <= err1`
by (irule err_always_positive
\\ qexistsl_tac [`A`, `dVars`, `e1`, `(e1lo,e1hi)`, `Gamma`]
@@ -990,7 +989,8 @@ val validErrorboundCorrectMult = store_thm ("validErrorboundCorrectMult",
\\ qexists_tac `nR2` \\ conj_tac
\\ simp[contained_def])
\\ assume_tac (REWRITE_RULE [contained_def] interval_multiplication_valid)
- \\ fs[contained_def, widenInterval_def]);
+ \\ fs[contained_def, widenInterval_def]
+QED
val _ = diminish_srw_ss ["RMULCANON_ss","RMULRELNORM_ss"]
@@ -2052,32 +2052,33 @@ Proof
conj_tac \\ REAL_ASM_ARITH_TAC)))))))
QED
-val validErrorboundCorrectDiv = store_thm ("validErrorboundCorrectDiv",
- ``!(E1 E2:env) (A:analysisResult) (e1:real expr) (e2:real expr)
- (nR nR1 nR2 nF nF1 nF2:real) (e err1 err2:real)
- (alo ahi e1lo e1hi e2lo e2hi :real) dVars m m1 m2 Gamma.
- eval_Real E1 Gamma e1 nR1 /\
- eval_Real E1 Gamma e2 nR2 /\
- eval_Real E1 Gamma (Binop Div e1 e2) nR /\
- eval_Fin E2 Gamma e1 nF1 m1 /\
- eval_Fin E2 Gamma e2 nF2 m2 /\
- eval_expr (updEnv 2 nF2 (updEnv 1 nF1 emptyEnv))
- (updDefVars (Binop Div (Var 1) (Var 2)) m
- (updDefVars (Var 2) m2 (updDefVars (Var 1) m1 (toRExpMap Gamma))))
- (Binop Div (Var 1) (Var 2)) nF m /\
- validErrorbound (Binop Div e1 e2) Gamma A dVars /\
- (e1lo <= nR1 /\ nR1 <= e1hi) /\
- (e2lo <= nR2 /\ nR2 <= e2hi) /\
- noDivzero e2hi e2lo /\
- FloverMapTree_find e1 A = SOME ((e1lo, e1hi), err1) /\
- FloverMapTree_find e2 A = SOME ((e2lo, e2hi), err2) /\
- FloverMapTree_find (Binop Div e1 e2) A = SOME ((alo, ahi), e) /\
- FloverMapTree_find (Binop Div e1 e2) Gamma = SOME m /\
- abs (nR1 - nF1) <= err1 /\
- abs (nR2 - nF2) <= err2 ==>
- abs (nR - nF) <= e``,
+Theorem validErrorboundCorrectDiv:
+ !(E1 E2:env) (A:analysisResult) (e1:real expr) (e2:real expr)
+ (nR nR1 nR2 nF nF1 nF2:real) (e err1 err2:real)
+ (alo ahi e1lo e1hi e2lo e2hi :real) dVars m m1 m2 Gamma.
+ eval_Real E1 Gamma e1 nR1 /\
+ eval_Real E1 Gamma e2 nR2 /\
+ eval_Real E1 Gamma (Binop Div e1 e2) nR /\
+ eval_Fin E2 Gamma e1 nF1 m1 /\
+ eval_Fin E2 Gamma e2 nF2 m2 /\
+ eval_expr (updEnv 2 nF2 (updEnv 1 nF1 emptyEnv))
+ (updDefVars (Binop Div (Var 1) (Var 2)) m
+ (updDefVars (Var 2) m2 (updDefVars (Var 1) m1 (toRExpMap Gamma))))
+ (Binop Div (Var 1) (Var 2)) nF m /\
+ validErrorbound (Binop Div e1 e2) Gamma A dVars /\
+ (e1lo <= nR1 /\ nR1 <= e1hi) /\
+ (e2lo <= nR2 /\ nR2 <= e2hi) /\
+ noDivzero e2hi e2lo /\
+ FloverMapTree_find e1 A = SOME ((e1lo, e1hi), err1) /\
+ FloverMapTree_find e2 A = SOME ((e2lo, e2hi), err2) /\
+ FloverMapTree_find (Binop Div e1 e2) A = SOME ((alo, ahi), e) /\
+ FloverMapTree_find (Binop Div e1 e2) Gamma = SOME m /\
+ abs (nR1 - nF1) <= err1 /\
+ abs (nR2 - nF2) <= err2 ==>
+ abs (nR - nF) <= e
+Proof
rpt strip_tac \\ simp[Once toREval_def]
- \\ Flover_compute ``validErrorbound`` \\ rveq
+ \\ fs[Once validErrorbound_def] \\ rveq
\\ `0 <= err1`
by (irule err_always_positive
\\ qexistsl_tac [`A`, `dVars`, `e1`, `(e1lo,e1hi)`, `Gamma`]
@@ -2102,14 +2103,15 @@ val validErrorboundCorrectDiv = store_thm ("validErrorboundCorrectDiv",
\\ qexists_tac `nR2` \\ conj_tac
\\ simp[contained_def])
\\ irule REAL_LE_ADD2 \\ conj_tac
- >- (irule (REWRITE_RULE [IVlo_def, IVhi_def, widenInterval_def, invertInterval_def] divisionErrorBounded)
+ >- (irule divisionErrorBounded
\\ fs[widenInterval_def])
\\ qmatch_abbrev_tac `_ <= computeError (maxAbs iv) _`
\\ PairCases_on `iv` \\ irule computeError_up
\\ unabbrev_all_tac \\ fs[maxAbs_def]
\\ irule maxAbs
\\ assume_tac (REWRITE_RULE [contained_def] interval_division_valid)
- \\ fs[contained_def, widenInterval_def, noDivzero_def]);
+ \\ fs[contained_def, widenInterval_def, noDivzero_def]
+QED
Theorem validErrorboundCorrectFma:
!(E1 E2:env) (A:analysisResult) (e1:real expr) (e2:real expr) (e3: real expr)
@@ -2143,7 +2145,7 @@ Theorem validErrorboundCorrectFma:
Proof
fs [toREval_def]
\\ rpt strip_tac \\ simp[Once toREval_def]
- \\ Flover_compute ``validErrorbound`` \\ fs [] \\ rveq
+ \\ fs[Once validErrorbound_eq] \\ rveq
\\ `0 <= err1`
by (irule err_always_positive
\\ rpt (asm_exists_tac \\ fs[]))
@@ -2191,24 +2193,25 @@ Proof
\\ fs[contained_def, widenInterval_def, IVlo_def, IVhi_def, noDivzero_def]
QED
-val validErrorboundCorrectRounding = store_thm ("validErrorboundCorrectRounding",
- ``!(E1 E2:env) (A:analysisResult) (e:real expr)
- (nR nF nF1:real) (err err1:real) (alo ahi elo ehi:real) dVars m mEps Gamma.
- eval_Real E1 Gamma e nR /\
- eval_Fin E2 Gamma e nF1 m /\
- eval_expr (updEnv 1 nF1 emptyEnv)
- (updDefVars (Downcast mEps (Var 1)) mEps
- (updDefVars (Var 1) m (toRExpMap Gamma)))
- (Downcast mEps (Var 1)) nF mEps /\
- validErrorbound (Downcast mEps e) Gamma A dVars /\
- elo <= nR /\ nR <= ehi /\
- FloverMapTree_find e A = SOME ((elo, ehi), err1) /\
- FloverMapTree_find (Downcast mEps e) A = SOME ((alo, ahi), err) /\
- FloverMapTree_find (Downcast mEps e) Gamma = SOME mEps /\
- abs (nR - nF1) <= err1 ==>
- abs (nR - nF) <= err``,
+Theorem validErrorboundCorrectRounding:
+ !(E1 E2:env) (A:analysisResult) (e:real expr)
+ (nR nF nF1:real) (err err1:real) (alo ahi elo ehi:real) dVars m mEps Gamma.
+ eval_Real E1 Gamma e nR /\
+ eval_Fin E2 Gamma e nF1 m /\
+ eval_expr (updEnv 1 nF1 emptyEnv)
+ (updDefVars (Downcast mEps (Var 1)) mEps
+ (updDefVars (Var 1) m (toRExpMap Gamma)))
+ (Downcast mEps (Var 1)) nF mEps /\
+ validErrorbound (Downcast mEps e) Gamma A dVars /\
+ elo <= nR /\ nR <= ehi /\
+ FloverMapTree_find e A = SOME ((elo, ehi), err1) /\
+ FloverMapTree_find (Downcast mEps e) A = SOME ((alo, ahi), err) /\
+ FloverMapTree_find (Downcast mEps e) Gamma = SOME mEps /\
+ abs (nR - nF1) <= err1 ==>
+ abs (nR - nF) <= err
+Proof
fs [toREval_def] \\ rpt strip_tac
- \\ Flover_compute ``validErrorbound`` \\ rveq \\ fs[]
+ \\ fs[Once validErrorbound_eq] \\ rveq
\\ irule REAL_LE_TRANS
\\ qexists_tac `err1 + computeError nF1 mEps` \\ fs []
\\ conj_tac
@@ -2223,7 +2226,8 @@ val validErrorboundCorrectRounding = store_thm ("validErrorboundCorrectRounding"
\\ fs[widenInterval_def]
\\ res_tac
\\ ntac 2 (first_x_assum (qspec_then `(elo, ehi)` assume_tac))
- \\ rpt (first_x_assum (destruct) \\ fs[]));
+ \\ rpt (first_x_assum (destruct) \\ fs[])
+QED
(**
Soundness theorem for the error bound validator.
@@ -2266,13 +2270,14 @@ Proof
\\ `vR = nR` by (metis_tac [meps_0_deterministic])
\\ rveq \\ fs[]
\\ rpt (find_exists_tac \\ fs[]))
- >- (fs[] \\ Flover_compute ``validErrorbound``
+ >- (fs[] \\ rveq
+ \\ qpat_x_assum `validErrorbound _ _ _ _` mp_tac
+ \\ simp[Once validErrorbound_eq] \\ strip_tac
\\ Cases_on `u` \\ fs[toREval_def] \\ rveq
\\ rw_thm_asm `(domain _) DIFF _ SUBSET _` usedVars_def
\\ inversion `eval_expr E1 _ _ _ _` eval_expr_cases \\ fs[]
\\ `m' = REAL` by (irule toRTMap_eval_REAL \\ find_exists_tac \\ fs[])
- \\ Cases_on `FloverMapTree_find e A` \\ fs[] \\ rveq
- \\ PairCases_on `x` \\ fs[] \\ rveq
+ \\ PairCases_on `v4` \\ fs[] \\ rveq
\\ rename1 `FloverMapTree_find e A = SOME ((e_lo, e_hi) , err)`
\\ once_rewrite_tac [eval_expr_cases] \\ fs[]
\\ first_x_assum
@@ -2281,10 +2286,9 @@ Proof
`dVars`, `Gamma`]
destruct)
>- (fs[Once validTypes_def, Once validRanges_def])
- \\ conj_tac \\ rpt strip_tac
- >- (fs[Once validTypes_def, toRExpMap_def]
- \\ qexistsl_tac [`me`, `nF`] \\ fs[]
- \\ `m = me`
+ \\ fs[Once validTypes_def, toRExpMap_def] \\ conj_tac \\ rpt strip_tac
+ >- (qexistsl_tac [`me`, `nF`] \\ fs[]
+ \\ `m' = me`
by (irule validTypes_exec
\\ rpt (find_exists_tac \\ fs[toRExpMap_def]))
\\ rveq \\ fs[])
@@ -2296,8 +2300,9 @@ Proof
\\ disch_then assume_tac \\ fs[]
\\ first_x_assum irule \\ asm_exists_tac \\ fs[])
>- (rename1 `Binop op e1 e2` \\ fs[]
- \\ Flover_compute ``validErrorbound`` \\ rveq
- \\ fs[toREval_def]
+ \\ qpat_x_assum `validErrorbound _ _ _ _` mp_tac
+ \\ simp[Once validErrorbound_eq] \\ strip_tac
+ \\ fs[toREval_def] \\ rveq
\\ inversion `eval_expr E1 _ _ _ _` eval_expr_cases \\ fs[]
\\ `m1 = REAL /\ m2 = REAL`
by (conj_tac \\ irule toRTMap_eval_REAL \\ find_exists_tac \\ fs[])
@@ -2351,11 +2356,11 @@ Proof
\\ fs[] \\ FAIL_TAC "")
\\ irule REAL_LTE_TRANS \\ qexists_tac `FST iv2 - err2` \\ fs[])
\\ conj_tac \\ rpt strip_tac
- >- (qexistsl_tac [`perturb (evalBinop op nF1 nF2) x' 0`, `x'`]
+ >- (qexistsl_tac [`perturb (evalBinop op nF1 nF2) m 0`, `m`]
\\ irule Binop_dist'
- \\ qexistsl_tac [`0`, `x'`, `m1`, `m2`, `nF1`, `nF2`]
+ \\ qexistsl_tac [`0`, `m`, `m1`, `m2`, `nF1`, `nF2`]
\\ fs[ABS_0, mTypeToR_pos, toRExpMap_def])
- \\ `m = x'`
+ \\ ‘m' = m’
by (first_x_assum irule \\ simp[Once validTypes_def]
\\ conj_tac
>- (rpt strip_tac \\ first_x_assum irule
@@ -2397,9 +2402,10 @@ Proof
\\ TRY (irule Binop_dist'
\\ qexistsl_tac [`0`, `REAL`, `REAL`, `REAL`, `v1`, `v2`]
\\ fs[perturb_def, mTypeToR_pos])
- \\ simp[Once validErrorbound_def, widenInterval_def, invertInterval_def])
+ \\ simp[Once validErrorbound_eq])
>- (rename1 `Fma e1 e2 e3` \\ fs[]
- \\ Flover_compute ``validErrorbound``
+ \\ qpat_x_assum ‘validErrorbound _ _ _ _’ mp_tac \\ simp[Once validErrorbound_eq]
+ \\ strip_tac
\\ rveq \\ fs[toREval_def]
\\ inversion `eval_expr E1 _ _ _ _` eval_expr_cases
\\ `m1 = REAL /\ m2 = REAL /\ m3 = REAL`
@@ -2462,9 +2468,9 @@ Proof
\\ first_x_assum irule
\\ qexists_tac `m3` \\ fs[])
\\ conj_tac
- >- (qexistsl_tac [`perturb (evalFma nF1 nF2 nF3) x' 0`, `x'`]
+ >- (qexistsl_tac [`perturb (evalFma nF1 nF2 nF3) m 0`, `m`]
\\ irule Fma_dist'
- \\ qexistsl_tac [`0`, `x'`, `m1`, `m2`, `m3`, `nF1`, `nF2`, `nF3`]
+ \\ qexistsl_tac [`0`, `m`, `m1`, `m2`, `m3`, `nF1`, `nF2`, `nF3`]
\\ fs[mTypeToR_pos,toRExpMap_def])
\\ rpt strip_tac
\\ `perturb (evalFma nR1 nR2 nR3) REAL delta = evalFma nR1 nR2 nR3`
@@ -2483,7 +2489,7 @@ Proof
\\ qexistsl_tac [`E2`, `Gamma`, `e3`, `v3`] \\ fs[])
\\ rveq
\\ rename1 `abs delta2 <= mTypeToR mF _`
- \\ `mF = x'`
+ \\ `mF = m`
by (irule validTypes_exec
\\ qexistsl_tac [`E2`, `Gamma`, `Fma e1 e2 e3`,
`perturb (evalFma v1 v2 v3) mF delta2`]
@@ -2491,10 +2497,10 @@ Proof
\\ first_x_assum MATCH_ACCEPT_TAC)
\\ rveq
\\ `eval_expr (updEnv 3 v3 (updEnv 2 v2 (updEnv 1 v1 emptyEnv)))
- (updDefVars (Fma (Var 1) (Var 2) (Var 3)) mF
+ (updDefVars (Fma (Var 1) (Var 2) (Var 3)) m
(updDefVars (Var 3) m3
(updDefVars (Var 2) m2 (updDefVars (Var 1) m1 (toRExpMap Gamma)))))
- (Fma (Var 1) (Var 2) (Var 3)) (perturb (evalFma v1 v2 v3) mF delta2) mF`
+ (Fma (Var 1) (Var 2) (Var 3)) (perturb (evalFma v1 v2 v3) m delta2) m`
by (irule fma_unfolding \\ conj_tac \\ fs[]
\\ rpt (find_exists_tac \\ fs[]))
\\ irule validErrorboundCorrectFma
@@ -2511,7 +2517,8 @@ Proof
\\ fs[perturb_def, mTypeToR_pos])
\\ once_rewrite_tac [validErrorbound_def] \\ fs[widenInterval_def])
>- (rename1 `Downcast m1 e1` \\ fs[]
- \\ Flover_compute ``validErrorbound``
+ \\ qpat_x_assum ‘validErrorbound _ _ _ _’ mp_tac \\ simp[Once validErrorbound_eq]
+ \\ strip_tac
\\ rveq \\ fs[toREval_def]
\\ inversion `eval_expr E1 _ _ _ _` eval_expr_cases \\ fs[]
\\ first_x_assum
@@ -2534,11 +2541,11 @@ Proof
by (irule distance_gives_iv
\\ qexists_tac `nR1` \\ fs[contained_def]
\\ first_x_assum irule
- \\ qexists_tac `m` \\ fs[])
+ \\ qexists_tac `m'` \\ fs[])
\\ conj_tac \\ rpt strip_tac
- >- (qexistsl_tac [`perturb nF m1 0`, `m1`]
+ >- (qexistsl_tac [`perturb nF m 0`, `m`]
\\ irule Downcast_dist' \\ fs[toRExpMap_def]
- \\ qexistsl_tac [`0`, `m`, `nF`]
+ \\ qexistsl_tac [`0`, `m'`, `nF`]
\\ fs[mTypeToR_pos, isMorePrecise_morePrecise])
\\ inversion `eval_expr E2 _ (Downcast m1 e1) _ _` eval_expr_cases
\\ rveq
@@ -2573,9 +2580,9 @@ Theorem validErrorboundCmd_gives_eval:
?vF m.
bstep f E2 (toRExpMap Gamma) vF m
Proof
- Induct_on `f` \\ rpt strip_tac
- \\ Flover_compute ``validErrorboundCmd``
- \\ rveq \\ fs[Once toREvalCmd_def]
+ Induct_on `f`
+ \\ simp[Once validErrorboundCmd_eq, Once toREvalCmd_def]
+ \\ rpt strip_tac
>- (inversion `bstep _ _ _ _ _` bstep_cases
\\ inversion `ssa _ _ _` ssa_cases
\\ fs[Once validTypesCmd_def, Once validRangesCmd_def, getRetExp_def]
@@ -2584,7 +2591,7 @@ Proof
\\ IMP_RES_TAC validRangesCmd_single
\\ fs[] \\ rveq \\ fs[]
\\ qspecl_then
- [`e`, `E1`, `E2`, `A`, `v`, `err_e`, `FST iv_e`, `SND iv_e`, `fVars`,
+ [`e`, `E1`, `E2`, `A`, `v`, `err_x`, `FST iv_e`, `SND iv_e`, `fVars`,
`dVars`, `Gamma`] destruct validErrorbound_sound
\\ fs[]
>- (rw_thm_asm `domain (freeVars _) DIFF _ SUBSET _` freeVars_def
@@ -2592,7 +2599,8 @@ Proof
\\ fs[SUBSET_DEF, domain_union]
\\ rpt strip_tac \\ first_x_assum irule \\ fs[]
\\ CCONTR_TAC \\ fs[] \\ rveq
- \\ `n IN domain fVars \/ n IN domain dVars` by (first_x_assum irule \\ fs[]))
+ \\ `n IN domain fVars \/ n IN domain dVars` by (first_x_assum irule \\ fs[])
+ )
\\ rename1 `eval_expr E2 (toRExpMap Gamma) e vF mF`
\\ `approxEnv (updEnv n v E1) (toRExpMap Gamma) A fVars
(insert n () dVars) (updEnv n vF E2)`
@@ -2660,9 +2668,8 @@ Theorem validErrorboundCmd_sound:
FloverMapTree_find (getRetExp f) A = SOME ((elo,ehi),err) ==>
abs (vR - vF) <= err
Proof
- Induct_on `f` \\ rpt strip_tac
- \\ Flover_compute ``validErrorboundCmd``
- \\ rveq \\ fs[Once toREvalCmd_def]
+ Induct_on `f`
+ \\ simp[Once validErrorboundCmd_eq, Once toREvalCmd_def] \\ rpt strip_tac
>- (inversion `bstep _ _ _ _ REAL` bstep_cases \\ rveq
\\ inversion `bstep _ _ _ _ m'` bstep_cases \\ rveq
\\ inversion `ssa _ _ _` ssa_cases \\ rveq
@@ -2682,12 +2689,11 @@ Proof
\\ qexists_tac `insert n () (union fVars dVars)` \\ fs [ domain_union]
\\ once_rewrite_tac [UNION_COMM]
\\ fs [INSERT_UNION_EQ])
- >- (fs[Once toREvalCmd_def])
>- (irule approxEnvUpdBound \\ rpt conj_tac
\\ fs[]
>- (Cases_on `lookup n (union fVars dVars)` \\ fs [domain_lookup])
\\ qspecl_then
- [`e`, `E1`, `E2`, `A`, `vr`, `err_e`, `FST (iv_e)`,
+ [`e`, `E1`, `E2`, `A`, `vr`, `err_x`, `FST (iv_e)`,
`SND (iv_e)`, `fVars`, `dVars`, `Gamma`]
destruct validErrorbound_sound
\\ fs [Once freeVars_def, domain_union, SUBSET_DEF]
diff --git a/hol4/FloverTactics.sml b/hol4/FloverTactics.sml
new file mode 100644
index 00000000..2601dfc8
--- /dev/null
+++ b/hol4/FloverTactics.sml
@@ -0,0 +1,147 @@
+(*
+ Some tactics which ease proving goals
+*)
+
+structure FloverTactics =
+struct
+
+local open intLib wordsLib in end;
+open set_relationTheory;
+open BasicProvers Defn HolKernel Parse Tactic monadsyntax
+ alistTheory arithmeticTheory bagTheory boolLib boolSimps bossLib
+ combinTheory dep_rewrite finite_mapTheory indexedListsTheory
+ listTheory llistTheory markerLib
+ optionTheory pairLib pairTheory pred_setTheory
+ quantHeuristicsLib relationTheory res_quanTheory rich_listTheory
+ sortingTheory sptreeTheory stringTheory sumTheory wordsTheory simpLib;
+open ExpressionsTheory CommandsTheory;
+
+fun elim_conj thm =
+ let val (hypl, concl) = dest_thm thm in
+ if is_conj concl
+ then
+ let val (thm1, thm2) = CONJ_PAIR thm in
+ elim_conj thm1 \\ elim_conj thm2
+ end
+ else
+ ASSUME_TAC thm
+ end;
+
+fun elim_exist1 thm =
+ let val (hypl, concl) = dest_thm thm in
+ if is_exists concl
+ then CHOOSE_THEN elim_exist thm
+ else elim_conj thm
+ end
+and elim_exist thm =
+ let val (hypl, concl) = dest_thm thm in
+ if is_exists concl
+ then CHOOSE_THEN elim_exist1 thm
+ else elim_conj thm
+ end;
+
+fun inversion pattern cases_thm =
+ qpat_x_assum pattern
+ (fn thm => elim_exist (ONCE_REWRITE_RULE [cases_thm] thm));
+
+fun qexistsl_tac termlist =
+ case termlist of
+ [] => ALL_TAC
+ | t::tel => qexists_tac t \\ qexistsl_tac tel;
+
+fun specialize pat_hyp pat_thm =
+ qpat_x_assum pat_hyp
+ (fn hyp =>
+ (qspec_then pat_thm ASSUME_TAC hyp) ORELSE
+ (qpat_assum pat_thm
+ (fn asm => ASSUME_TAC (MP hyp asm))));
+
+fun rw_asm pat_asm =
+ qpat_x_assum pat_asm
+ (fn asm =>
+ (once_rewrite_tac [asm] \\ ASSUME_TAC asm));
+
+fun rw_asm_star pat_asm =
+ qpat_x_assum pat_asm
+ (fn asm =>
+ fs [Once asm] \\ ASSUME_TAC asm);
+
+fun rw_sym_asm pat_asm =
+ qpat_x_assum pat_asm
+ (fn asm =>
+ (once_rewrite_tac [GSYM asm] \\ ASSUME_TAC asm));
+
+fun rw_thm_asm pat_asm thm =
+ qpat_x_assum pat_asm
+ (fn asm =>
+ (ASSUME_TAC (ONCE_REWRITE_RULE[thm] asm)));
+
+
+(* Destruct like tactic, by Michael Norrish, see HOL-info **)
+(* Given theorem
+ P x y z ==> ?w. Q w
+ introduce P x y z as a subgoal and Q w for some w as hypothesis *)
+fun destruct th =
+ let
+ val hyp_to_prove = lhand (concl th)
+ in
+ SUBGOAL_THEN hyp_to_prove (fn thm => STRIP_ASSUME_TAC (MP th thm))
+ end
+
+fun impl_subgoal_tac th =
+ let
+ val hyp_to_prove = lhand (concl th)
+ in
+ SUBGOAL_THEN hyp_to_prove (fn thm => assume_tac (MP th thm))
+ end
+
+val flover_eval_tac :tactic=
+ let val _ = computeLib.del_funs([sptreeTheory.lookup_def])
+ val _ = computeLib.add_funs([sptreeTheory.lookup_compute]) in
+ computeLib.EVAL_TAC
+ \\ fs[sptreeTheory.lookup_def]
+ \\ rpt strip_tac
+ \\ fs[sptreeTheory.lookup_def]
+ \\ EVAL_TAC
+end;
+
+fun iter_exists_tac ind n =
+ fn tm =>
+ if ind < n
+ then
+ (part_match_exists_tac
+ (fn concl => List.nth (strip_conj concl, ind)) tm)
+ ORELSE (iter_exists_tac (ind+1) n tm)
+ else
+ FAIL_TAC (concat ["No matching clause found for ", term_to_string tm]) ;
+
+val try_all:term -> tactic =
+ fn tm =>
+ fn (asl, g) =>
+ let
+ val len = length (strip_conj (snd (dest_exists g))) in
+ iter_exists_tac 0 len tm (asl, g)
+ end;
+
+val find_exists_tac =
+ first_assum (try_all o concl);
+
+val bool_simps = Q.prove (
+ ‘(∀ P. (P ∧ F) = F) ∧
+ (∀ P. (F ∨ P) = P) ∧
+ (∀ P Q. (if P then Q else F) = (P ∧ Q))’, fs[]);
+
+val cond_simp = Q.prove (
+‘(if P then Q else R) = (P /\ Q \/ ~P /\ R)’,
+ TOP_CASE_TAC);
+
+val flover_ss =
+ (mk_simpset ([DatatypeSimps.case_cong_ss [“:real exprâ€, “:real cmdâ€]]
+ @ ssfrags_of bool_ss))
+ && [option_case_eq |> GEN “v:'b†|> Q.ISPEC ‘T’ |> SIMP_RULE bool_ss [],
+ pair_case_eq |> GEN “v:'a†|> Q.ISPEC ‘T’ |> SIMP_RULE bool_ss [],
+ expr_case_eq |> GEN “v:'a†|> Q.ISPEC ‘T’ |> SIMP_RULE bool_ss [],
+ cmd_case_eq |> GEN “v:'a†|> Q.ISPEC ‘T’ |> SIMP_RULE bool_ss [],
+ bool_simps, cond_simp, PULL_EXISTS];
+
+end
diff --git a/hol4/Holmakefile b/hol4/Holmakefile
index cc3cb62a..151e8303 100644
--- a/hol4/Holmakefile
+++ b/hol4/Holmakefile
@@ -1,2 +1,2 @@
-INCLUDES = Infra
+INCLUDES = Infra semantics
OPTIONS = QUIT_ON_FAILURE
diff --git a/hol4/Infra/FloverTactics.sml b/hol4/Infra/FloverTactics.sml
deleted file mode 100644
index 3ec2e79d..00000000
--- a/hol4/Infra/FloverTactics.sml
+++ /dev/null
@@ -1,233 +0,0 @@
-(*
- Some tactics which ease proving goals
-*)
-
-structure FloverTactics =
-struct
-
-local open intLib wordsLib in end;
-open set_relationTheory;
-open BasicProvers Defn HolKernel Parse Tactic monadsyntax
- alistTheory arithmeticTheory bagTheory boolLib boolSimps bossLib
- combinTheory dep_rewrite finite_mapTheory indexedListsTheory
- listTheory llistTheory markerLib
- optionTheory pairLib pairTheory pred_setTheory
- quantHeuristicsLib relationTheory res_quanTheory rich_listTheory
- sortingTheory sptreeTheory stringTheory sumTheory wordsTheory;
-
-fun elim_conj thm =
- let val (hypl, concl) = dest_thm thm in
- if is_conj concl
- then
- let val (thm1, thm2) = CONJ_PAIR thm in
- elim_conj thm1 \\ elim_conj thm2
- end
- else
- ASSUME_TAC thm
- end;
-
-fun elim_exist1 thm =
- let val (hypl, concl) = dest_thm thm in
- if is_exists concl
- then
- CHOOSE_THEN elim_exist thm
- else
- elim_conj thm
- end
-and elim_exist thm =
- let val (hypl, concl) = dest_thm thm in
- if is_exists concl
- then
- CHOOSE_THEN elim_exist1 thm
- else
- elim_conj thm
- end;
-
-fun inversion pattern cases_thm =
- qpat_x_assum pattern
- (fn thm => elim_exist (ONCE_REWRITE_RULE [cases_thm] thm));
-
-fun qexistsl_tac termlist =
- case termlist of
- [] => ALL_TAC
- | t::tel => qexists_tac t \\ qexistsl_tac tel;
-
-fun specialize pat_hyp pat_thm =
- qpat_x_assum pat_hyp
- (fn hyp =>
- (qspec_then pat_thm ASSUME_TAC hyp) ORELSE
- (qpat_assum pat_thm
- (fn asm => ASSUME_TAC (MP hyp asm))));
-
-fun rw_asm pat_asm =
- qpat_x_assum pat_asm
- (fn asm =>
- (once_rewrite_tac [asm] \\ ASSUME_TAC asm));
-
-fun rw_asm_star pat_asm =
- qpat_x_assum pat_asm
- (fn asm =>
- fs [Once asm] \\ ASSUME_TAC asm);
-
-fun rw_sym_asm pat_asm =
- qpat_x_assum pat_asm
- (fn asm =>
- (once_rewrite_tac [GSYM asm] \\ ASSUME_TAC asm));
-
-fun rw_thm_asm pat_asm thm =
- qpat_x_assum pat_asm
- (fn asm =>
- (ASSUME_TAC (ONCE_REWRITE_RULE[thm] asm)));
-
-
-(* Destruct like tactic, by Michael Norrish, see HOL-info **)
-
-(* Given theorem
-
- P x y z ==> ?w. Q w
-
- introduce P x y z as a subgoal and Q w for some w as hypothesis *)
-
-fun destruct th =
- let
- val hyp_to_prove = lhand (concl th)
- in
- SUBGOAL_THEN hyp_to_prove (fn thm => STRIP_ASSUME_TAC (MP th thm))
- end
-
-fun impl_subgoal_tac th =
- let
- val hyp_to_prove = lhand (concl th)
- in
- SUBGOAL_THEN hyp_to_prove (fn thm => assume_tac (MP th thm))
- end
-
-val flover_eval_tac :tactic=
- let val _ = computeLib.del_funs([sptreeTheory.lookup_def])
- val _ = computeLib.add_funs([sptreeTheory.lookup_compute]) in
- computeLib.EVAL_TAC
- \\ fs[sptreeTheory.lookup_def]
- \\ rpt strip_tac
- \\ fs[sptreeTheory.lookup_def]
- \\ EVAL_TAC
-end;
-
-(* Flover Compute Tactic as in Coq dev to simplify goals involving computations *)
-fun iter n s f =
- if n = 0 then s
- else iter (n - 1) (f s) f;
-
-fun getArgTypeList t num lst =
-let val (name, list) = dest_type t in
- case name of
- "fun" =>
- let
- val (hdty, tylist) = (hd list, tl list) in
- getArgTypeList (hd tylist) (num + 1) (hdty :: lst)
- end
- | _ => (num, rev lst)
-end
-
-exception ERR of string;
-
-fun getPatTerm t =
- let
- val decl_list = decls (term_to_string t);
- val argTypes_list = map (fn t => getArgTypeList (#Ty (dest_thy_const t)) 0 []) decl_list in
- if length decl_list = 1
- then
- let
- val (cnt, tyList) = hd argTypes_list
- in
- iter cnt (hd decl_list, tyList)
- (fn (t,tyList) =>
- let
- val var = mk_var ("_",hd tyList) in
- (* val _ = print_term var; *)
- (* val _ = print_term t in *)
- (mk_comb (t, var), tl tyList)
- end)
- end
- else raise ERR "Too many constants"
-end;
-
-(* This variable is supposed to hold all defined functions *)
-val eval_funs:term list ref = ref [];
-
-(* open TextIO; *)
-(* val t = TextIO.openIn("/home/hbecker/Downloads/test.txt"); *)
-(* inputLine(t); *)
-(* closeIn(t); *)
-(* val t2 = openIn("./test.txt"); *)
-(* inputLine(t2); *)
-(* output(t2, "ABC\n"); *)
-(* closeOut(t2); *)
-
-fun add_unevaluated_function (t:term) :unit =
- let
- val add_t = "val _ = FloverTactics.eval_funs :=``" ^ term_to_string t ^ "`` :: (!FloverTactics.eval_funs);"
- val _ = adjoin_to_theory
- { sig_ps = NONE,
- struct_ps =
- SOME (fn _ => PP.add_string add_t)};
- in
- eval_funs := t :: (!eval_funs)
- end;
-
-fun Flover_compute t =
- let
- val eval_thm = fst (snd (hd (DB.find ((term_to_string t)^"_def"))));
- val (pat,_) = getPatTerm t in
- TRY (
- Tactical.PAT_X_ASSUM
- pat
- (fn thm =>
- let
- val rwthm = ONCE_REWRITE_RULE [eval_thm] thm;
- val compute_thm = computeLib.RESTR_EVAL_RULE (!eval_funs) rwthm in
- assume_tac compute_thm end)
- \\ fs[]
- \\ TRY (
- REPEAT (
- ((qpat_assum `option_CASE _ _ _`
- (fn thm =>
- let
- val (t,t2,_) = optionSyntax.dest_option_case (concl thm) in
- Cases_on `^t2` \\ fs[] end))
- ORELSE
- (split_pair_case_tac)) \\ fs[])))
- end;
-
-fun iter_exists_tac ind n =
- fn tm =>
- if ind < n
- then
- (part_match_exists_tac
- (fn concl => List.nth (strip_conj concl, ind)) tm)
- ORELSE (iter_exists_tac (ind+1) n tm)
- else
- FAIL_TAC (concat ["No matching clause found for ", term_to_string tm]) ;
-
-val try_all:term -> tactic =
- fn tm =>
- fn (asl, g) =>
- let
- val len = length (strip_conj (snd (dest_exists g))) in
- iter_exists_tac 0 len tm (asl, g)
- end;
-
-val find_exists_tac =
- first_assum (try_all o concl);
-
-(* val Flover_compute:tactic = *)
-(* fn (g:goal) => *)
-(* let *)
-(* val terms_to_eval = !eval_funs in *)
-(* if (length terms_to_eval = 0) *)
-(* then let val _ = print "Nothing to evaluate" in ALL_TAC g end *)
-(* else *)
-(* Flover_compute_steps terms_to_eval g *)
-(* end; *)
-
-
-end
diff --git a/hol4/Infra/RealSimpsScript.sml b/hol4/Infra/RealSimpsScript.sml
index 7b8e2535..8fe579a7 100644
--- a/hol4/Infra/RealSimpsScript.sml
+++ b/hol4/Infra/RealSimpsScript.sml
@@ -1,6 +1,5 @@
open RealArith;
open realTheory realLib;
-open FloverTactics;
open preambleFloVer;
(*
val _ = ParseExtras.temp_tight_equality() *)
@@ -99,7 +98,7 @@ Theorem REAL_LE_ABS_TRANS:
a <= b
Proof
rpt strip_tac \\ irule REAL_LE_TRANS
- \\ find_exists_tac \\ fs[ABS_LE]
+ \\ fsrw_tac [SATISFY_ss] [ABS_LE]
QED
Theorem REAL_POW_1OVER_POS[simp]:
diff --git a/hol4/IntervalArithScript.sml b/hol4/IntervalArithScript.sml
index 2bdc189a..9757d1ad 100644
--- a/hol4/IntervalArithScript.sml
+++ b/hol4/IntervalArithScript.sml
@@ -96,26 +96,18 @@ Definition addInterval_def:
addInterval (iv1:interval) (iv2:interval) = absIntvUpd (+) iv1 iv2
End
-add_unevaluated_function ``addInterval``;
-
Definition subtractInterval_def:
subtractInterval (iv1:interval) (iv2:interval) = addInterval iv1 (negateInterval iv2)
End
-add_unevaluated_function ``subtractInterval``;
-
Definition multInterval_def:
multInterval (iv1:interval) (iv2:interval) = absIntvUpd ( * ) iv1 iv2
End
-add_unevaluated_function ``multInterval``;
-
Definition divideInterval_def:
divideInterval iv1 iv2 = multInterval iv1 (invertInterval iv2)
End
-add_unevaluated_function ``divideInterval``;
-
Definition minAbsFun_def:
minAbsFun iv = min (abs (FST iv)) (abs (SND iv))
End
@@ -490,8 +482,8 @@ val distance_gives_iv = store_thm ("distance_gives_iv",
val minAbs_positive_iv_is_lo = store_thm ("minAbs_positive_iv_is_lo",
``!(a b:real).
(0 < a) /\
- (a <= b) ==>
- (minAbsFun (a,b) = a)``,
+ (a <= b) ==>
+ (minAbsFun (a,b) = a)``,
rpt (strip_tac) \\
fs[minAbsFun_def] \\
`abs a = a` by (fs[ABS_REFL] \\ REAL_ASM_ARITH_TAC) \\
@@ -501,8 +493,8 @@ val minAbs_positive_iv_is_lo = store_thm ("minAbs_positive_iv_is_lo",
val minAbs_negative_iv_is_hi = store_thm ("minAbs_negative_iv_is_hi",
``!(a b:real).
(b < 0) /\
- (a <= b) ==>
- (minAbsFun (a,b) = - b)``,
+ (a <= b) ==>
+ (minAbsFun (a,b) = - b)``,
rpt (strip_tac) \\
fs[minAbsFun_def] \\
`abs a = - a` by REAL_ASM_ARITH_TAC \\
diff --git a/hol4/IntervalValidationScript.sml b/hol4/IntervalValidationScript.sml
index 1dc849bd..8b42fa98 100644
--- a/hol4/IntervalValidationScript.sml
+++ b/hol4/IntervalValidationScript.sml
@@ -22,7 +22,7 @@ val _ = temp_overload_on("abs",``real$abs``);
val _ = temp_overload_on("max",``real$max``);
val _ = temp_overload_on("min",``real$min``);
-val validIntervalbounds_def = Define `
+Definition validIntervalbounds_def:
validIntervalbounds f (absenv:analysisResult) (P:precond) (validVars:num_set) =
case (FloverMapTree_find f absenv) of
| SOME (intv, _) =>
@@ -93,11 +93,13 @@ val validIntervalbounds_def = Define `
isSupersetInterval new_iv intv
| _, _, _ => F
else F))
- | _ => F`;
+ | _ => F
+End
-add_unevaluated_function ``validIntervalbounds``;
+Theorem validIntervalbounds_eq =
+ SIMP_CONV flover_ss [Once validIntervalbounds_def] (Parse.Term ‘validIntervalbounds e A P v’)
-val validIntervalboundsCmd_def = Define `
+Definition validIntervalboundsCmd_def:
validIntervalboundsCmd (f:real cmd) (absenv:analysisResult) (P:precond) (validVars:num_set) =
case f of
| Let m x e g =>
@@ -108,25 +110,23 @@ val validIntervalboundsCmd_def = Define `
else F
|_,_ => F)
| Ret e =>
- (validIntervalbounds e absenv P validVars)`;
+ (validIntervalbounds e absenv P validVars)
+End
-add_unevaluated_function ``validIntervalboundsCmd``;
+Theorem validIntervalboundsCmd_eq =
+ SIMP_CONV flover_ss [Once validIntervalboundsCmd_def] (Parse.Term ‘validIntervalboundsCmd f A P v’)
-val cond_simpl = store_thm (
- "cond_simpl[simp]",
- ``!a b. (if a then T else b) <=> (a \/ (~ a /\ b))``,
- rpt strip_tac \\ metis_tac[]);
+Theorem cond_simpl:
+ ∀ a b. (if a then T else b) <=> (a \/ (~ a /\ b))
+Proof
+ rpt strip_tac \\ metis_tac[]
+QED
val real_prove =
rpt (qpat_x_assum `!x. _` kall_tac)
\\ rpt (qpat_x_assum `_ ==> ! x. _` kall_tac)
\\ REAL_ASM_ARITH_TAC;
-val _ = add_unevaluated_function “addIntervalâ€
-val _ = add_unevaluated_function “subtractIntervalâ€
-val _ = add_unevaluated_function “multIntervalâ€
-val _ = add_unevaluated_function “divideIntervalâ€
-
Theorem validIntervalbounds_sound:
!(f:real expr) (A:analysisResult) (P:precond) (fVars:num_set)
(dVars:num_set) E Gamma.
@@ -138,9 +138,12 @@ Theorem validIntervalbounds_sound:
validTypes f Gamma ==>
validRanges f A E (toRTMap (toRExpMap Gamma))
Proof
- Induct_on `f`
- \\ once_rewrite_tac [usedVars_def, toREval_def] \\ rpt strip_tac \\ rveq
- \\ Flover_compute ``validIntervalbounds`` \\ rveq
+ Induct_on `f` \\ rpt strip_tac
+ \\ qpat_x_assum ‘domain (usedVars _) DIFF _ SUBSET _’
+ (assume_tac o (SIMP_RULE flover_ss [Once usedVars_def]))
+ \\ qpat_x_assum ‘validIntervalbounds _ _ _ _’
+ (assume_tac o (ONCE_REWRITE_RULE [validIntervalbounds_eq]))
+ \\ fs[]
(* Defined variable case *)
>- (rw_thm_asm `dVars_range_valid _ _ _` dVars_range_valid_def
\\ specialize `!v. v IN domain dVars ==> _` `n`
@@ -165,7 +168,7 @@ Proof
\\ irule REAL_LE_TRANS \\ asm_exists_tac \\ fs[] \\ rveq \\ fs[])
(* Const case *)
>- (simp[validRanges_def]
- \\ qexists_tac `v` \\ fs[toREval_def]
+ \\ qexists_tac `v` \\ fs[toREval_def, isSupersetInterval_def]
\\ irule Const_dist' \\ fs[perturb_def, mTypeToR_def])
(* Unary operator case *)
>- (rw_thm_asm `validTypes _ _` validTypes_def
@@ -349,10 +352,9 @@ Theorem validIntervalboundsCmd_sound:
validTypesCmd f Gamma ==>
validRangesCmd f A E (toRTMap (toRExpMap Gamma))
Proof
- Induct_on `f`
+ Induct_on `f` \\ simp[Once validIntervalboundsCmd_eq]
\\ once_rewrite_tac [toREvalCmd_def, getRetExp_def, validTypesCmd_def]
\\ rpt strip_tac
- \\ Flover_compute ``validIntervalboundsCmd``
>- (
inversion `ssa _ _ _` ssa_cases \\ rveq
\\ drule validIntervalbounds_sound
@@ -424,9 +426,8 @@ Theorem validIntervalbounds_validates_iv:
FloverMapTree_find f A = SOME (iv, err) /\
valid iv
Proof
- Induct_on `f`
+ Induct_on `f` \\ simp[Once validIntervalbounds_eq]
\\ rpt strip_tac
- \\ Flover_compute ``validIntervalbounds``
>- (first_x_assum (qspecl_then [`n`] destruct)
\\ fs[domain_lookup, valid_def, isSupersetInterval_def, validIntervalbounds_def]
\\ rveq \\ fs[])
@@ -434,7 +435,7 @@ Proof
\\ irule REAL_LE_TRANS
\\ asm_exists_tac \\ conj_tac \\ fs[IVlo_def, IVhi_def]
\\ irule REAL_LE_TRANS \\ asm_exists_tac \\ fs[])
- >- (fs[valid_def, IVlo_def, IVhi_def]
+ >- (fs[isSupersetInterval_def, valid_def, IVlo_def, IVhi_def]
\\ irule REAL_LE_TRANS \\ asm_exists_tac \\ fs[])
>- (first_x_assum (qspecl_then [`A`, `P`, `dVars`] destruct)
\\ fs[]
@@ -512,7 +513,8 @@ Proof
\\ rveq
\\ `FST iv = FST intv` by (metis_tac[REAL_LE_ANTISYM])
\\ `SND iv = SND intv` by (metis_tac[REAL_LE_ANTISYM])
- \\ fs[valid_def, IVlo_def, IVhi_def]));
+ \\ 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).
@@ -520,7 +522,7 @@ val validIntervalbounds_noDivzero_real = store_thm("validIntervalbounds_noDivzer
?iv err.
FloverMapTree_find f2 A = SOME (iv,err) /\
noDivzero (SND iv) (FST iv)``,
- rpt strip_tac \\ Flover_compute ``validIntervalbounds``
+ rpt strip_tac \\ fs[Once validIntervalbounds_eq]
\\ fs[noDivzero_def, IVhi_def, IVlo_def]);
val validRanges_validates_iv = store_thm (
diff --git a/hol4/TypeValidatorScript.sml b/hol4/TypeValidatorScript.sml
index 4ac6f681..37053829 100644
--- a/hol4/TypeValidatorScript.sml
+++ b/hol4/TypeValidatorScript.sml
@@ -204,8 +204,6 @@ Definition getValidMap_def:
od
End
-add_unevaluated_function ``getValidMap``;
-
val tMap_def = FloverMapTree_correct;
val toRExpMap_char = store_thm (
diff --git a/hol4/AbbrevsScript.sml b/hol4/semantics/AbbrevsScript.sml
similarity index 100%
rename from hol4/AbbrevsScript.sml
rename to hol4/semantics/AbbrevsScript.sml
diff --git a/hol4/CommandsScript.sml b/hol4/semantics/CommandsScript.sml
similarity index 100%
rename from hol4/CommandsScript.sml
rename to hol4/semantics/CommandsScript.sml
diff --git a/hol4/ExpressionAbbrevsScript.sml b/hol4/semantics/ExpressionAbbrevsScript.sml
similarity index 99%
rename from hol4/ExpressionAbbrevsScript.sml
rename to hol4/semantics/ExpressionAbbrevsScript.sml
index fe37175a..32ab3bb1 100644
--- a/hol4/ExpressionAbbrevsScript.sml
+++ b/hol4/semantics/ExpressionAbbrevsScript.sml
@@ -33,6 +33,7 @@ val toRTMap_def = Define `
|_ => NONE) /\
toRTMap tMap e = SOME REAL`;
+
val no_cycle_unop = store_thm (
"no_cycle_unop",
``!e u. e <> Unop u e``,
diff --git a/hol4/ExpressionSemanticsScript.sml b/hol4/semantics/ExpressionSemanticsScript.sml
similarity index 98%
rename from hol4/ExpressionSemanticsScript.sml
rename to hol4/semantics/ExpressionSemanticsScript.sml
index 738f39ec..c88abbdc 100644
--- a/hol4/ExpressionSemanticsScript.sml
+++ b/hol4/semantics/ExpressionSemanticsScript.sml
@@ -2,7 +2,7 @@
Formalization of the base expression language for the flover framework
**)
open realTheory realLib sptreeTheory;
-open AbbrevsTheory MachineTypeTheory FloverTactics ExpressionsTheory;
+open AbbrevsTheory MachineTypeTheory ExpressionsTheory;
open ExpressionAbbrevsTheory;
open preambleFloVer;
@@ -206,8 +206,7 @@ Theorem toRTMap_eval_REAL:
∀ e v E Gamma m.
eval_expr E (toRTMap Gamma) (toREval e) v m ==> m = REAL
Proof
- Induct_on `e` \\ rpt strip_tac \\ fs[toREval_def]
- \\ inversion `eval_expr _ _ _ _ _` eval_expr_cases
+ Induct_on `e` \\ rpt strip_tac \\ fs[toREval_def, Once eval_expr_cases]
\\ fs[toRTMap_def, option_case_eq]
\\ res_tac \\ fs[]
QED
diff --git a/hol4/ExpressionsScript.sml b/hol4/semantics/ExpressionsScript.sml
similarity index 98%
rename from hol4/ExpressionsScript.sml
rename to hol4/semantics/ExpressionsScript.sml
index 549eeeb5..6bda9801 100644
--- a/hol4/ExpressionsScript.sml
+++ b/hol4/semantics/ExpressionsScript.sml
@@ -2,7 +2,7 @@
Formalization of the base expression language for the flover framework
**)
open realTheory realLib sptreeTheory
-open AbbrevsTheory MachineTypeTheory FloverTactics
+open AbbrevsTheory MachineTypeTheory
open preambleFloVer;
val _ = new_theory "Expressions";
diff --git a/hol4/FloverMapScript.sml b/hol4/semantics/FloverMapScript.sml
similarity index 99%
rename from hol4/FloverMapScript.sml
rename to hol4/semantics/FloverMapScript.sml
index 46409303..11eb1e74 100644
--- a/hol4/FloverMapScript.sml
+++ b/hol4/semantics/FloverMapScript.sml
@@ -1,4 +1,4 @@
-open MachineTypeTheory ExpressionsTheory FloverTactics
+open MachineTypeTheory ExpressionsTheory;
open preambleFloVer;
val _ = new_theory "FloverMap";
diff --git a/hol4/semantics/Holmakefile b/hol4/semantics/Holmakefile
new file mode 100644
index 00000000..6d33bcc5
--- /dev/null
+++ b/hol4/semantics/Holmakefile
@@ -0,0 +1,2 @@
+INCLUDES = ../Infra
+OPTIONS = QUIT_ON_FAILURE
diff --git a/hol4/configure_hol.sh b/scripts/configure_hol.sh
similarity index 100%
rename from hol4/configure_hol.sh
rename to scripts/configure_hol.sh
diff --git a/hol4/find_cheats.sh b/scripts/find_cheats.sh
similarity index 100%
rename from hol4/find_cheats.sh
rename to scripts/find_cheats.sh
--
GitLab