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