summaryrefslogtreecommitdiff
path: root/backends/hol4
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--backends/hol4/divDefLib.sig5
-rw-r--r--backends/hol4/divDefLib.sml23
-rw-r--r--backends/hol4/divDefScript.sml52
-rw-r--r--backends/hol4/divDefTheory.sig22
-rw-r--r--backends/hol4/primitivesBaseTacLib.sml1
5 files changed, 90 insertions, 13 deletions
diff --git a/backends/hol4/divDefLib.sig b/backends/hol4/divDefLib.sig
index df879b4b..0de88db5 100644
--- a/backends/hol4/divDefLib.sig
+++ b/backends/hol4/divDefLib.sig
@@ -34,7 +34,10 @@
Remark: "Partial recursive functions in higher-order logic", Alexander Krauss,
introduces an interesting approach by means of an inductive. It could be
- interesting to try and compare.
+ interesting to try and compare. One advantage of the current approach, though,
+ is that it is compatible with an "execution" through [EVAL]. But if we manage
+ to make [EVAL] use arbitrary rewriting theorems, then it doesn't make a
+ difference.
*)
signature divDefLib =
diff --git a/backends/hol4/divDefLib.sml b/backends/hol4/divDefLib.sml
index f53ef6f8..78e664e6 100644
--- a/backends/hol4/divDefLib.sml
+++ b/backends/hol4/divDefLib.sml
@@ -24,7 +24,12 @@ val fail_tm = “Fail : error -> 'a result”
val fail_failure_tm = “Fail Failure : 'a result”
val diverge_tm = “Diverge : 'a result”
+(* Switch to use ‘fix_exec’ (leading to executable definitions) and ‘fix’ (non
+ executable) *)
+val use_fix_exec = ref true
+
val fix_tm = “fix”
+val fix_exec_tm = “fix_exec”
val is_valid_fp_body_tm = “is_valid_fp_body”
fun mk_result (ty : hol_type) : hol_type = Type.type_subst [ alpha_ty |-> ty ] result_ty
@@ -744,8 +749,8 @@ fun mk_raw_defs (in_out_tys : (hol_type * hol_type) list)
(* Retrieve the body *)
val body = (List.last o snd o strip_comb o concl) body_is_valid
- (* Create the term ‘fix body’ *)
- val fixed_body = mk_icomb (fix_tm, body)
+ (* Create the term ‘fix_exec body’ *)
+ val fixed_body = mk_icomb (if !use_fix_exec then fix_exec_tm else fix_tm, body)
(* For every function in the group, generate the equation that we will
use as definition. In particular:
@@ -814,12 +819,13 @@ fun prove_def_eq_tac
(body_def : thm option) : tactic =
let
val body_def_thm = case body_def of SOME th => [th] | NONE => []
+ val fix_eq = if !use_fix_exec then fix_exec_fixed_eq else fix_fixed_eq
in
rpt gen_tac >>
(* Expand the definition *)
pure_once_rewrite_tac [current_raw_def] >>
(* Use the fixed-point equality *)
- pure_once_rewrite_left_tac [HO_MATCH_MP fix_fixed_eq is_valid] >>
+ pure_once_rewrite_left_tac [HO_MATCH_MP fix_eq is_valid] >>
(* Expand the body definition *)
pure_rewrite_tac body_def_thm >>
(* Expand all the definitions from the group *)
@@ -896,13 +902,12 @@ fun DefineDiv (def_qt : term quotation) =
(* Prove the final equations *)
val def_eqs = prove_def_eqs body_is_valid def_tms raw_defs
- (* Save the final equations as definitions.
-
- Note that because we use the same names, doing this overrides the "raw"
- definitions, which are then forgotten, which means we don't need to
- manually delete them.
- *)
+ (* Save the final equations as definitions. *)
val thm_names = map (fn x => x ^ "_def") fnames
+ (* Because [store_definition] overrides existing names, it seems that in
+ practice we don't really need to delete the previous definitions
+ (we still do it: it doesn't cost much). *)
+ val _ = map delete_binding thm_names
val _ = map store_definition (zip thm_names def_eqs)
in
def_eqs
diff --git a/backends/hol4/divDefScript.sml b/backends/hol4/divDefScript.sml
index b80aa2bf..cc745e5d 100644
--- a/backends/hol4/divDefScript.sml
+++ b/backends/hol4/divDefScript.sml
@@ -36,6 +36,22 @@ Definition fix_def:
if (∃ n. fix_fuel_P f x n) then fix_fuel ($LEAST (fix_fuel_P f x)) f x else Diverge
End
+(* An "executable" fixed point operator - useful for unit tests: we first test
+ if ‘fix_fuel_P f x’ is true for a high quantity of fuel, otherwise we use
+ ‘fix’ (which is not executable).
+
+ We prove later that, under some constraints: ‘∀n. fix_nexec n f = fix f’
+ *)
+Definition fix_nexec_def:
+ fix_nexec (n : num) (f : ('a -> 'b result) -> 'a -> 'b result) (x : 'a) : 'b result =
+ if (fix_fuel_P f x n) then fix_fuel n f x else fix f x
+End
+
+(* We fix a quantity of fuel for ’fix_nexec *)
+Definition fix_exec_def:
+ fix_exec = fix_nexec 1000000
+End
+
(* A validity condition.
If a function body ‘f’ satisfies this condition, then we have the fixed point
@@ -50,9 +66,9 @@ Definition is_valid_fp_body_def:
∀g. f g x = do z <- g y; h g z od))
End
-(*======================
- * Lemmas
- *======================*)
+(*=====================================*
+ * Lemmas about ‘fix_fuel’ and ‘fix’
+ *=====================================*)
(* Auxiliary lemma.
We generalize the goal of [fix_fuel_mono] in the case the fuel is non-empty
(this allows us to unfold definitions like ‘fix_fuel’ once, and reveal
@@ -323,6 +339,36 @@ Proof
QED
(*===============================
+ * Lemmas about ‘fix_exec’
+ *===============================*)
+
+(* Prove that ‘fix_nexec’ is equivalent to ‘fix’ *)
+Theorem fix_nexec_eq_fix:
+ ∀ N f n. is_valid_fp_body N f ⇒ fix_nexec n f = fix f
+Proof
+ rw [] >>
+ rpt (irule EQ_EXT >> gen_tac) >>
+ fs [fix_nexec_def, fix_def] >>
+ top_case_tac >>
+ case_tac >> fs [] >>
+ (* Use the properties of the least upper bound *)
+ qspec_assume ‘fix_fuel_P f x’ whileTheory.LEAST_EXISTS_IMP >>
+ pop_assum sg_premise_tac >- metis_tac [] >> fs [] >>
+ (* Use the monotonicity property *)
+ irule fix_fuel_mono_least >> metis_tac []
+QED
+
+(* Prove the fixed point property for ‘fix_exec’ *)
+Theorem fix_exec_fixed_eq:
+ ∀N f. is_valid_fp_body N f ⇒ ∀x. fix_exec f x = f (fix_exec f) x
+Proof
+ rw [fix_exec_def] >>
+ imp_res_tac fix_nexec_eq_fix >> fs [] >>
+ irule fix_fixed_eq >> fs [] >> metis_tac []
+QED
+
+
+(*===============================
* Utilities for the automation
*===============================*)
diff --git a/backends/hol4/divDefTheory.sig b/backends/hol4/divDefTheory.sig
index 15592052..ec69c44f 100644
--- a/backends/hol4/divDefTheory.sig
+++ b/backends/hol4/divDefTheory.sig
@@ -4,12 +4,15 @@ sig
(* Definitions *)
val fix_def : thm
+ val fix_exec_def : thm
val fix_fuel_P_def : thm
val fix_fuel_def : thm
+ val fix_nexec_def : thm
val is_valid_fp_body_def : thm
(* Theorems *)
val case_result_switch_eq : thm
+ val fix_exec_fixed_eq : thm
val fix_fixed_diverges : thm
val fix_fixed_eq : thm
val fix_fixed_terminates : thm
@@ -21,6 +24,7 @@ sig
val fix_fuel_mono_least : thm
val fix_fuel_not_diverge_eq_fix : thm
val fix_fuel_not_diverge_eq_fix_aux : thm
+ val fix_nexec_eq_fix : thm
val fix_not_diverge_implies_fix_fuel : thm
val fix_not_diverge_implies_fix_fuel_aux : thm
val is_valid_fp_body_compute : thm
@@ -37,6 +41,10 @@ sig
fix_fuel ($LEAST (fix_fuel_P f x)) f x
else Diverge
+ [fix_exec_def] Definition
+
+ ⊢ fix_exec = fix_nexec 1000000
+
[fix_fuel_P_def] Definition
⊢ ∀f x n. fix_fuel_P f x n ⇔ ¬is_diverge (fix_fuel n f x)
@@ -46,6 +54,12 @@ sig
⊢ (∀f x. fix_fuel 0 f x = Diverge) ∧
∀n f x. fix_fuel (SUC n) f x = f (fix_fuel n f) x
+ [fix_nexec_def] Definition
+
+ ⊢ ∀n f x.
+ fix_nexec n f x =
+ if fix_fuel_P f x n then fix_fuel n f x else fix f x
+
[is_valid_fp_body_def] Definition
⊢ (∀f. is_valid_fp_body 0 f ⇔ F) ∧
@@ -75,6 +89,10 @@ sig
| Fail e => Fail e
| Diverge => Diverge
+ [fix_exec_fixed_eq] Theorem
+
+ ⊢ ∀N f. is_valid_fp_body N f ⇒ ∀x. fix_exec f x = f (fix_exec f) x
+
[fix_fixed_diverges] Theorem
⊢ ∀N f.
@@ -151,6 +169,10 @@ sig
∀n x.
g (fix_fuel n f) x ≠ Diverge ⇒ g (fix f) x = g (fix_fuel n f) x
+ [fix_nexec_eq_fix] Theorem
+
+ ⊢ ∀N f n. is_valid_fp_body N f ⇒ fix_nexec n f = fix f
+
[fix_not_diverge_implies_fix_fuel] Theorem
⊢ ∀N f.
diff --git a/backends/hol4/primitivesBaseTacLib.sml b/backends/hol4/primitivesBaseTacLib.sml
index 78822abe..133f6a99 100644
--- a/backends/hol4/primitivesBaseTacLib.sml
+++ b/backends/hol4/primitivesBaseTacLib.sml
@@ -25,6 +25,7 @@ val exfalso : tactic =
SUBGOAL_THEN “F” (fn th => ASSUME_TAC th >> fs[])
val case_tac = CASE_TAC
+val top_case_tac = BasicProvers.TOP_CASE_TAC
val try_tac = TRY
val first_tac = FIRST
val map_first_tac = MAP_FIRST