strengthened lfp_ordinal_induct; added dual gfp variant
authorhoelzl
Mon May 04 18:49:51 2015 +0200 (2015-05-04)
changeset 6017470d8f7abde8f
parent 60173 6a61bb577d5b
child 60175 831ddb69db9b
strengthened lfp_ordinal_induct; added dual gfp variant
src/HOL/Inductive.thy
     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