author hoelzl Mon May 04 18:49:51 2015 +0200 (2015-05-04) changeset 60174 70d8f7abde8f parent 60173 6a61bb577d5b child 60175 831ddb69db9b
strengthened lfp_ordinal_induct; added dual gfp variant
 src/HOL/Inductive.thy file | annotate | diff | revisions
```     1.1 --- a/src/HOL/Inductive.thy	Mon May 04 18:04:01 2015 +0200
1.2 +++ b/src/HOL/Inductive.thy	Mon May 04 18:49:51 2015 +0200
1.3 @@ -56,32 +56,10 @@
1.4
1.5  subsection {* General induction rules for least fixed points *}
1.6
1.7 -theorem lfp_induct:
1.8 -  assumes mono: "mono f" and ind: "f (inf (lfp f) P) <= P"
1.9 -  shows "lfp f <= P"
1.10 -proof -
1.11 -  have "inf (lfp f) P <= lfp f" by (rule inf_le1)
1.12 -  with mono have "f (inf (lfp f) P) <= f (lfp f)" ..
1.13 -  also from mono have "f (lfp f) = lfp f" by (rule lfp_unfold [symmetric])
1.14 -  finally have "f (inf (lfp f) P) <= lfp f" .
1.15 -  from this and ind have "f (inf (lfp f) P) <= inf (lfp f) P" by (rule le_infI)
1.16 -  hence "lfp f <= inf (lfp f) P" by (rule lfp_lowerbound)
1.17 -  also have "inf (lfp f) P <= P" by (rule inf_le2)
1.18 -  finally show ?thesis .
1.19 -qed
1.20 -
1.21 -lemma lfp_induct_set:
1.22 -  assumes lfp: "a: lfp(f)"
1.23 -      and mono: "mono(f)"
1.24 -      and indhyp: "!!x. [| x: f(lfp(f) Int {x. P(x)}) |] ==> P(x)"
1.25 -  shows "P(a)"
1.26 -  by (rule lfp_induct [THEN subsetD, THEN CollectD, OF mono _ lfp])
1.27 -    (auto simp: intro: indhyp)
1.28 -
1.29 -lemma lfp_ordinal_induct:
1.30 +lemma lfp_ordinal_induct[case_names mono step union]:
1.31    fixes f :: "'a\<Colon>complete_lattice \<Rightarrow> 'a"
1.32    assumes mono: "mono f"
1.33 -  and P_f: "\<And>S. P S \<Longrightarrow> P (f S)"
1.34 +  and P_f: "\<And>S. P S \<Longrightarrow> S \<le> lfp f \<Longrightarrow> P (f S)"
1.35    and P_Union: "\<And>M. \<forall>S\<in>M. P S \<Longrightarrow> P (Sup M)"
1.36    shows "P (lfp f)"
1.37  proof -
1.38 @@ -92,13 +70,29 @@
1.39      show "Sup ?M \<le> lfp f" by (blast intro: Sup_least)
1.40      hence "f (Sup ?M) \<le> f (lfp f)" by (rule mono [THEN monoD])
1.41      hence "f (Sup ?M) \<le> lfp f" using mono [THEN lfp_unfold] by simp
1.42 -    hence "f (Sup ?M) \<in> ?M" using P_f P_Union by simp
1.43 +    hence "f (Sup ?M) \<in> ?M" using P_Union by simp (intro P_f Sup_least, auto)
1.44      hence "f (Sup ?M) \<le> Sup ?M" by (rule Sup_upper)
1.45      thus "lfp f \<le> Sup ?M" by (rule lfp_lowerbound)
1.46    qed
1.47    finally show ?thesis .
1.48  qed
1.49
1.50 +theorem lfp_induct:
1.51 +  assumes mono: "mono f" and ind: "f (inf (lfp f) P) \<le> P"
1.52 +  shows "lfp f \<le> P"
1.53 +proof (induction rule: lfp_ordinal_induct)
1.54 +  case (step S) then show ?case
1.55 +    by (intro order_trans[OF _ ind] monoD[OF mono]) auto
1.56 +qed (auto intro: mono Sup_least)
1.57 +
1.58 +lemma lfp_induct_set:
1.59 +  assumes lfp: "a: lfp(f)"
1.60 +      and mono: "mono(f)"
1.61 +      and indhyp: "!!x. [| x: f(lfp(f) Int {x. P(x)}) |] ==> P(x)"
1.62 +  shows "P(a)"
1.63 +  by (rule lfp_induct [THEN subsetD, THEN CollectD, OF mono _ lfp])
1.64 +     (auto simp: intro: indhyp)
1.65 +
1.66  lemma lfp_ordinal_induct_set:
1.67    assumes mono: "mono f"
1.68    and P_f: "!!S. P S ==> P(f S)"
1.69 @@ -179,17 +173,35 @@
1.70  lemma coinduct_set: "[| mono(f);  a: X;  X \<subseteq> f(X Un gfp(f)) |] ==> a : gfp(f)"
1.71    by (rule weak_coinduct[rotated], rule coinduct_lemma) blast+
1.72
1.73 -lemma coinduct: "[| mono(f); X \<le> f (sup X (gfp f)) |] ==> X \<le> gfp(f)"
1.74 -  apply (rule order_trans)
1.75 -  apply (rule sup_ge1)
1.76 -  apply (rule gfp_upperbound)
1.77 -  apply (erule coinduct_lemma)
1.78 -  apply assumption
1.79 -  done
1.80 -
1.81  lemma gfp_fun_UnI2: "[| mono(f);  a: gfp(f) |] ==> a: f(X Un gfp(f))"
1.82    by (blast dest: gfp_lemma2 mono_Un)
1.83
1.84 +lemma gfp_ordinal_induct[case_names mono step union]:
1.85 +  fixes f :: "'a\<Colon>complete_lattice \<Rightarrow> 'a"
1.86 +  assumes mono: "mono f"
1.87 +  and P_f: "\<And>S. P S \<Longrightarrow> gfp f \<le> S \<Longrightarrow> P (f S)"
1.88 +  and P_Union: "\<And>M. \<forall>S\<in>M. P S \<Longrightarrow> P (Inf M)"
1.89 +  shows "P (gfp f)"
1.90 +proof -
1.91 +  let ?M = "{S. gfp f \<le> S \<and> P S}"
1.92 +  have "P (Inf ?M)" using P_Union by simp
1.93 +  also have "Inf ?M = gfp f"
1.94 +  proof (rule antisym)
1.95 +    show "gfp f \<le> Inf ?M" by (blast intro: Inf_greatest)
1.96 +    hence "f (gfp f) \<le> f (Inf ?M)" by (rule mono [THEN monoD])
1.97 +    hence "gfp f \<le> f (Inf ?M)" using mono [THEN gfp_unfold] by simp
1.98 +    hence "f (Inf ?M) \<in> ?M" using P_Union by simp (intro P_f Inf_greatest, auto)
1.99 +    hence "Inf ?M \<le> f (Inf ?M)" by (rule Inf_lower)
1.100 +    thus "Inf ?M \<le> gfp f" by (rule gfp_upperbound)
1.101 +  qed
1.102 +  finally show ?thesis .
1.103 +qed
1.104 +
1.105 +lemma coinduct: assumes mono: "mono f" and ind: "X \<le> f (sup X (gfp f))" shows "X \<le> gfp f"
1.106 +proof (induction rule: gfp_ordinal_induct)
1.107 +  case (step S) then show ?case
1.108 +    by (intro order_trans[OF ind _] monoD[OF mono]) auto
1.109 +qed (auto intro: mono Inf_greatest)
1.110
1.111  subsection {* Even Stronger Coinduction Rule, by Martin Coen *}
1.112
```