1.1 --- a/src/HOL/Partial_Function.thy	Tue May 31 11:11:17 2011 +0200
     1.2 +++ b/src/HOL/Partial_Function.thy	Tue May 31 11:16:34 2011 +0200
     1.3 @@ -165,6 +165,25 @@
     1.4    finally show "f = F f" .
     1.5  qed
     1.6  
     1.7 +text {* Fixpoint induction rule *}
     1.8 +
     1.9 +lemma fixp_induct_uc:
    1.10 +  fixes F :: "'c \<Rightarrow> 'c" and
    1.11 +    U :: "'c \<Rightarrow> 'b \<Rightarrow> 'a" and
    1.12 +    C :: "('b \<Rightarrow> 'a) \<Rightarrow> 'c" and
    1.13 +    P :: "('b \<Rightarrow> 'a) \<Rightarrow> bool"
    1.14 +  assumes mono: "\<And>x. mono_body (\<lambda>f. U (F (C f)) x)"
    1.15 +  assumes eq: "f \<equiv> C (fixp_fun (\<lambda>f. U (F (C f))))"
    1.16 +  assumes inverse: "\<And>f. U (C f) = f"
    1.17 +  assumes adm: "ccpo.admissible le_fun lub_fun P"
    1.18 +  assumes step: "\<And>f. P (U f) \<Longrightarrow> P (U (F f))"
    1.19 +  shows "P (U f)"
    1.20 +unfolding eq inverse
    1.21 +apply (rule ccpo.fixp_induct[OF ccpo adm])
    1.22 +apply (insert mono, auto simp: monotone_def fun_ord_def)[1]
    1.23 +by (rule_tac f="C x" in step, simp add: inverse)
    1.24 +
    1.25 +
    1.26  text {* Rules for @{term mono_body}: *}
    1.27  
    1.28  lemma const_mono[partial_function_mono]: "monotone ord leq (\<lambda>f. c)"
    1.29 @@ -224,12 +243,6 @@
    1.30    partial_function_definitions "flat_ord None" "flat_lub None"
    1.31  by (rule flat_interpretation)
    1.32  
    1.33 -declaration {* Partial_Function.init "tailrec" @{term tailrec.fixp_fun}
    1.34 -  @{term tailrec.mono_body} @{thm tailrec.fixp_rule_uc} NONE *}
    1.35 -
    1.36 -declaration {* Partial_Function.init "option" @{term option.fixp_fun}
    1.37 -  @{term option.mono_body} @{thm option.fixp_rule_uc} NONE *}
    1.38 -
    1.39  
    1.40  abbreviation "option_ord \<equiv> flat_ord None"
    1.41  abbreviation "mono_option \<equiv> monotone (fun_ord option_ord) option_ord"
    1.42 @@ -288,6 +301,27 @@
    1.43    qed
    1.44  qed
    1.45  
    1.46 +lemma fixp_induct_option:
    1.47 +  fixes F :: "'c \<Rightarrow> 'c" and
    1.48 +    U :: "'c \<Rightarrow> 'b \<Rightarrow> 'a option" and
    1.49 +    C :: "('b \<Rightarrow> 'a option) \<Rightarrow> 'c" and
    1.50 +    P :: "'b \<Rightarrow> 'a \<Rightarrow> bool"
    1.51 +  assumes mono: "\<And>x. mono_option (\<lambda>f. U (F (C f)) x)"
    1.52 +  assumes eq: "f \<equiv> C (ccpo.fixp (fun_ord option_ord) (fun_lub (flat_lub None)) (\<lambda>f. U (F (C f))))"
    1.53 +  assumes inverse2: "\<And>f. U (C f) = f"
    1.54 +  assumes step: "\<And>f x y. (\<And>x y. U f x = Some y \<Longrightarrow> P x y) \<Longrightarrow> U (F f) x = Some y \<Longrightarrow> P x y"
    1.55 +  assumes defined: "U f x = Some y"
    1.56 +  shows "P x y"
    1.57 +  using step defined option.fixp_induct_uc[of U F C, OF mono eq inverse2 option_admissible]
    1.58 +  by blast
    1.59 +
    1.60 +declaration {* Partial_Function.init "tailrec" @{term tailrec.fixp_fun}
    1.61 +  @{term tailrec.mono_body} @{thm tailrec.fixp_rule_uc} NONE *}
    1.62 +
    1.63 +declaration {* Partial_Function.init "option" @{term option.fixp_fun}
    1.64 +  @{term option.mono_body} @{thm option.fixp_rule_uc} 
    1.65 +  (SOME @{thm fixp_induct_option}) *}
    1.66 +
    1.67  
    1.68  hide_const (open) chain
    1.69