author Andreas Lochbihler Tue Mar 19 13:19:21 2013 +0100 (2013-03-19) changeset 51459 bc3651180a09 parent 51458 67542078fa21 child 51460 a5af7c2baf2b
add induction rule for partial_function (tailrec)
```     1.1 --- a/src/HOL/Partial_Function.thy	Mon Mar 18 20:02:37 2013 +0100
1.2 +++ b/src/HOL/Partial_Function.thy	Tue Mar 19 13:19:21 2013 +0100
1.3 @@ -244,6 +244,47 @@
1.4  by (rule flat_interpretation)
1.5
1.6
1.7 +abbreviation "tailrec_ord \<equiv> flat_ord undefined"
1.8 +abbreviation "mono_tailrec \<equiv> monotone (fun_ord tailrec_ord) tailrec_ord"
1.9 +
1.10 +lemma tailrec_admissible:
1.11 +  "ccpo.admissible (fun_lub (flat_lub undefined)) (fun_ord tailrec_ord)
1.12 +     (\<lambda>a. \<forall>x. a x \<noteq> undefined \<longrightarrow> P x (a x))"
1.13 +proof(intro ccpo.admissibleI[OF tailrec.ccpo] strip)
1.14 +  fix A x
1.15 +  assume chain: "Complete_Partial_Order.chain (fun_ord tailrec_ord) A"
1.16 +    and P [rule_format]: "\<forall>f\<in>A. \<forall>x. f x \<noteq> undefined \<longrightarrow> P x (f x)"
1.17 +    and defined: "fun_lub (flat_lub undefined) A x \<noteq> undefined"
1.18 +  from defined obtain f where f: "f \<in> A" "f x \<noteq> undefined"
1.19 +    by(auto simp add: fun_lub_def flat_lub_def split: split_if_asm)
1.20 +  hence "P x (f x)" by(rule P)
1.21 +  moreover from chain f have "\<forall>f' \<in> A. f' x = undefined \<or> f' x = f x"
1.22 +    by(auto 4 4 simp add: Complete_Partial_Order.chain_def flat_ord_def fun_ord_def)
1.23 +  hence "fun_lub (flat_lub undefined) A x = f x"
1.24 +    using f by(auto simp add: fun_lub_def flat_lub_def)
1.25 +  ultimately show "P x (fun_lub (flat_lub undefined) A x)" by simp
1.26 +qed
1.27 +
1.28 +lemma fixp_induct_tailrec:
1.29 +  fixes F :: "'c \<Rightarrow> 'c" and
1.30 +    U :: "'c \<Rightarrow> 'b \<Rightarrow> 'a" and
1.31 +    C :: "('b \<Rightarrow> 'a) \<Rightarrow> 'c" and
1.32 +    P :: "'b \<Rightarrow> 'a \<Rightarrow> bool" and
1.33 +    x :: "'b"
1.34 +  assumes mono: "\<And>x. mono_tailrec (\<lambda>f. U (F (C f)) x)"
1.35 +  assumes eq: "f \<equiv> C (ccpo.fixp (fun_lub (flat_lub undefined)) (fun_ord tailrec_ord) (\<lambda>f. U (F (C f))))"
1.36 +  assumes inverse2: "\<And>f. U (C f) = f"
1.37 +  assumes step: "\<And>f x y. (\<And>x y. U f x = y \<Longrightarrow> y \<noteq> undefined \<Longrightarrow> P x y) \<Longrightarrow> U (F f) x = y \<Longrightarrow> y \<noteq> undefined \<Longrightarrow> P x y"
1.38 +  assumes result: "U f x = y"
1.39 +  assumes defined: "y \<noteq> undefined"
1.40 +  shows "P x y"
1.41 +proof -
1.42 +  have "\<forall>x y. U f x = y \<longrightarrow> y \<noteq> undefined \<longrightarrow> P x y"
1.43 +    by(rule tailrec.fixp_induct_uc[of U F C, OF mono eq inverse2])(auto intro: step tailrec_admissible)
1.44 +  thus ?thesis using result defined by blast
1.45 +qed
1.46 +
1.47 +
1.48  abbreviation "option_ord \<equiv> flat_ord None"
1.49  abbreviation "mono_option \<equiv> monotone (fun_ord option_ord) option_ord"
1.50
1.51 @@ -316,13 +357,13 @@
1.52    by blast
1.53
1.54  declaration {* Partial_Function.init "tailrec" @{term tailrec.fixp_fun}
1.55 -  @{term tailrec.mono_body} @{thm tailrec.fixp_rule_uc} NONE *}
1.56 +  @{term tailrec.mono_body} @{thm tailrec.fixp_rule_uc}
1.57 +  (SOME @{thm fixp_induct_tailrec}) *}
1.58
1.59  declaration {* Partial_Function.init "option" @{term option.fixp_fun}
1.60    @{term option.mono_body} @{thm option.fixp_rule_uc}
1.61    (SOME @{thm fixp_induct_option}) *}
1.62
1.63 -
1.64  hide_const (open) chain
1.65
1.66  end
```