author Andreas Lochbihler Fri Sep 27 12:26:23 2013 +0200 (2013-09-27) changeset 53949 021a8ef97f5f parent 53947 54b08afc03c7 child 53950 ea38710e731c
generalise lemma
```     1.1 --- a/src/HOL/Partial_Function.thy	Fri Sep 27 10:40:02 2013 +0200
1.2 +++ b/src/HOL/Partial_Function.thy	Fri Sep 27 12:26:23 2013 +0200
1.3 @@ -248,21 +248,21 @@
1.4  abbreviation "mono_tailrec \<equiv> monotone (fun_ord tailrec_ord) tailrec_ord"
1.5
1.7 -  "ccpo.admissible (fun_lub (flat_lub undefined)) (fun_ord tailrec_ord)
1.8 -     (\<lambda>a. \<forall>x. a x \<noteq> undefined \<longrightarrow> P x (a x))"
1.9 +  "ccpo.admissible (fun_lub (flat_lub c)) (fun_ord (flat_ord c))
1.10 +     (\<lambda>a. \<forall>x. a x \<noteq> c \<longrightarrow> P x (a x))"
1.12    fix A x
1.13 -  assume chain: "Complete_Partial_Order.chain (fun_ord tailrec_ord) A"
1.14 -    and P [rule_format]: "\<forall>f\<in>A. \<forall>x. f x \<noteq> undefined \<longrightarrow> P x (f x)"
1.15 -    and defined: "fun_lub (flat_lub undefined) A x \<noteq> undefined"
1.16 -  from defined obtain f where f: "f \<in> A" "f x \<noteq> undefined"
1.17 +  assume chain: "Complete_Partial_Order.chain (fun_ord (flat_ord c)) A"
1.18 +    and P [rule_format]: "\<forall>f\<in>A. \<forall>x. f x \<noteq> c \<longrightarrow> P x (f x)"
1.19 +    and defined: "fun_lub (flat_lub c) A x \<noteq> c"
1.20 +  from defined obtain f where f: "f \<in> A" "f x \<noteq> c"
1.21      by(auto simp add: fun_lub_def flat_lub_def split: split_if_asm)
1.22    hence "P x (f x)" by(rule P)
1.23 -  moreover from chain f have "\<forall>f' \<in> A. f' x = undefined \<or> f' x = f x"
1.24 +  moreover from chain f have "\<forall>f' \<in> A. f' x = c \<or> f' x = f x"
1.25      by(auto 4 4 simp add: Complete_Partial_Order.chain_def flat_ord_def fun_ord_def)
1.26 -  hence "fun_lub (flat_lub undefined) A x = f x"
1.27 +  hence "fun_lub (flat_lub c) A x = f x"
1.28      using f by(auto simp add: fun_lub_def flat_lub_def)
1.29 -  ultimately show "P x (fun_lub (flat_lub undefined) A x)" by simp
1.30 +  ultimately show "P x (fun_lub (flat_lub c) A x)" by simp
1.31  qed
1.32
1.33  lemma fixp_induct_tailrec:
1.34 @@ -271,16 +271,17 @@
1.35      C :: "('b \<Rightarrow> 'a) \<Rightarrow> 'c" and
1.36      P :: "'b \<Rightarrow> 'a \<Rightarrow> bool" and
1.37      x :: "'b"
1.38 -  assumes mono: "\<And>x. mono_tailrec (\<lambda>f. U (F (C f)) x)"
1.39 -  assumes eq: "f \<equiv> C (ccpo.fixp (fun_lub (flat_lub undefined)) (fun_ord tailrec_ord) (\<lambda>f. U (F (C f))))"
1.40 +  assumes mono: "\<And>x. monotone (fun_ord (flat_ord c)) (flat_ord c) (\<lambda>f. U (F (C f)) x)"
1.41 +  assumes eq: "f \<equiv> C (ccpo.fixp (fun_lub (flat_lub c)) (fun_ord (flat_ord c)) (\<lambda>f. U (F (C f))))"
1.42    assumes inverse2: "\<And>f. U (C f) = f"
1.43 -  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.44 +  assumes step: "\<And>f x y. (\<And>x y. U f x = y \<Longrightarrow> y \<noteq> c \<Longrightarrow> P x y) \<Longrightarrow> U (F f) x = y \<Longrightarrow> y \<noteq> c \<Longrightarrow> P x y"
1.45    assumes result: "U f x = y"
1.46 -  assumes defined: "y \<noteq> undefined"
1.47 +  assumes defined: "y \<noteq> c"
1.48    shows "P x y"
1.49  proof -
1.50 -  have "\<forall>x y. U f x = y \<longrightarrow> y \<noteq> undefined \<longrightarrow> P x y"
1.51 -    by(rule tailrec.fixp_induct_uc[of U F C, OF mono eq inverse2])(auto intro: step tailrec_admissible)
1.52 +  have "\<forall>x y. U f x = y \<longrightarrow> y \<noteq> c \<longrightarrow> P x y"
1.53 +    by(rule partial_function_definitions.fixp_induct_uc[OF flat_interpretation, of _ U F C, OF mono eq inverse2])
1.54 +      (auto intro: step tailrec_admissible)
1.55    thus ?thesis using result defined by blast
1.56  qed
1.57
1.58 @@ -391,7 +392,7 @@
1.59
1.60  declaration {* Partial_Function.init "tailrec" @{term tailrec.fixp_fun}
1.61    @{term tailrec.mono_body} @{thm tailrec.fixp_rule_uc} @{thm tailrec.fixp_induct_uc}
1.62 -  (SOME @{thm fixp_induct_tailrec}) *}
1.63 +  (SOME @{thm fixp_induct_tailrec[where c=undefined]}) *}
1.64
1.65  declaration {* Partial_Function.init "option" @{term option.fixp_fun}
1.66    @{term option.mono_body} @{thm option.fixp_rule_uc} @{thm option.fixp_induct_uc}
```