diff options
Diffstat (limited to 'backends/hol4/divDefScript.sml')
-rw-r--r-- | backends/hol4/divDefScript.sml | 52 |
1 files changed, 49 insertions, 3 deletions
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 *===============================*) |