diff options
Diffstat (limited to '')
-rw-r--r-- | backends/hol4/divDefScript.sml | 17 |
1 files changed, 9 insertions, 8 deletions
diff --git a/backends/hol4/divDefScript.sml b/backends/hol4/divDefScript.sml index c742fb1f..b80aa2bf 100644 --- a/backends/hol4/divDefScript.sml +++ b/backends/hol4/divDefScript.sml @@ -20,35 +20,36 @@ val _ = new_theory "divDef" *======================*) (* An auxiliary operator which uses some fuel *) -val fix_fuel_def = Define ‘ +Definition fix_fuel_def: (fix_fuel (0 : num) (f : ('a -> 'b result) -> 'a -> 'b result) (x : 'a) : 'b result = Diverge) ∧ (fix_fuel (SUC n) (f : ('a -> 'b result) -> 'a -> 'b result) (x : 'a) : 'b result = f (fix_fuel n f) x) -’ +End (* An auxiliary predicate *) -val fix_fuel_P_def = Define ‘ +Definition fix_fuel_P_def: fix_fuel_P f x n = ~(is_diverge (fix_fuel n f x)) -’ +End (* The fixed point operator *) -val fix_def = Define ‘ +Definition fix_def: fix (f : ('a -> 'b result) -> 'a -> 'b result) (x : 'a) : 'b result = if (∃ n. fix_fuel_P f x n) then fix_fuel ($LEAST (fix_fuel_P f x)) f x else Diverge -’ +End (* A validity condition. If a function body ‘f’ satisfies this condition, then we have the fixed point equation ‘fix f = f (fix f)’ (see [fix_fixed_eq]). *) -val is_valid_fp_body_def = Define ‘ +Definition is_valid_fp_body_def: (is_valid_fp_body (0 : num) (f : ('a -> 'a result) -> 'a -> 'a result) = F) ∧ (is_valid_fp_body (SUC n) (f : ('a -> 'a result) -> 'a -> 'a result) = ∀x. (∀g h. f g x = f h x) ∨ (∃ h y. is_valid_fp_body n h ∧ ∀g. f g x = do z <- g y; h g z od)) -’ +End + (*====================== * Lemmas *======================*) |