src/HOL/Partial_Function.thy
 changeset 43082 8d0c44de9773 parent 43081 1a39c9898ae6 child 45297 3c9f17d017bf
```     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
```