diff options
Diffstat (limited to '')
| -rw-r--r-- | backends/hol4/divDefLib.sig | 5 | ||||
| -rw-r--r-- | backends/hol4/divDefLib.sml | 23 | ||||
| -rw-r--r-- | backends/hol4/divDefScript.sml | 52 | ||||
| -rw-r--r-- | backends/hol4/divDefTheory.sig | 22 | ||||
| -rw-r--r-- | backends/hol4/primitivesBaseTacLib.sml | 1 |
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 |