src/HOL/Partial_Function.thy
 changeset 42949 618adb3584e5 parent 40288 520199d8b66e child 43080 73a1d6a7ef1d
```     1.1 --- a/src/HOL/Partial_Function.thy	Sun May 22 22:22:25 2011 +0200
1.2 +++ b/src/HOL/Partial_Function.thy	Mon May 23 10:58:21 2011 +0200
1.3 @@ -16,7 +16,7 @@
1.4  subsection {* Axiomatic setup *}
1.5
1.6  text {* This techical locale constains the requirements for function
1.7 -  definitions with ccpo fixed points.  *}
1.8 +  definitions with ccpo fixed points. *}
1.9
1.10  definition "fun_ord ord f g \<longleftrightarrow> (\<forall>x. ord (f x) (g x))"
1.11  definition "fun_lub L A = (\<lambda>x. L {y. \<exists>f\<in>A. y = f x})"
1.12 @@ -169,9 +169,6 @@
1.13  lemma const_mono[partial_function_mono]: "monotone ord leq (\<lambda>f. c)"
1.14  by (rule monotoneI) (rule leq_refl)
1.15
1.16 -declaration {* Partial_Function.init @{term fixp_fun}
1.17 -  @{term mono_body} @{thm fixp_rule_uc} *}
1.18 -
1.19  end
1.20
1.21
1.22 @@ -226,6 +223,13 @@
1.23    partial_function_definitions "flat_ord None" "flat_lub None"
1.24  by (rule flat_interpretation)
1.25
1.26 +declaration {* Partial_Function.init "tailrec" @{term tailrec.fixp_fun}
1.27 +  @{term tailrec.mono_body} @{thm tailrec.fixp_rule_uc} *}
1.28 +
1.29 +declaration {* Partial_Function.init "option" @{term option.fixp_fun}
1.30 +  @{term option.mono_body} @{thm option.fixp_rule_uc} *}
1.31 +
1.32 +
1.33  abbreviation "option_ord \<equiv> flat_ord None"
1.34  abbreviation "mono_option \<equiv> monotone (fun_ord option_ord) option_ord"
1.35
```