src/HOL/Inductive.thy
changeset 63400 249fa34faba2
parent 61955 e96292f32c3c
child 63540 f8652d0534fa
     1.1 --- a/src/HOL/Inductive.thy	Tue Jul 05 22:47:48 2016 +0200
     1.2 +++ b/src/HOL/Inductive.thy	Tue Jul 05 23:39:49 2016 +0200
     1.3 @@ -19,48 +19,45 @@
     1.4  context complete_lattice
     1.5  begin
     1.6  
     1.7 -definition
     1.8 -  lfp :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a" where
     1.9 -  "lfp f = Inf {u. f u \<le> u}"    \<comment>\<open>least fixed point\<close>
    1.10 +definition lfp :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a"  \<comment> \<open>least fixed point\<close>
    1.11 +  where "lfp f = Inf {u. f u \<le> u}"
    1.12  
    1.13 -definition
    1.14 -  gfp :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a" where
    1.15 -  "gfp f = Sup {u. u \<le> f u}"    \<comment>\<open>greatest fixed point\<close>
    1.16 +definition gfp :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a"  \<comment> \<open>greatest fixed point\<close>
    1.17 +  where "gfp f = Sup {u. u \<le> f u}"
    1.18  
    1.19  
    1.20 -subsection\<open>Proof of Knaster-Tarski Theorem using @{term lfp}\<close>
    1.21 +subsection \<open>Proof of Knaster-Tarski Theorem using @{term lfp}\<close>
    1.22  
    1.23 -text\<open>@{term "lfp f"} is the least upper bound of
    1.24 -      the set @{term "{u. f(u) \<le> u}"}\<close>
    1.25 +text \<open>@{term "lfp f"} is the least upper bound of the set @{term "{u. f u \<le> u}"}\<close>
    1.26  
    1.27 -lemma lfp_lowerbound: "f A \<le> A ==> lfp f \<le> A"
    1.28 +lemma lfp_lowerbound: "f A \<le> A \<Longrightarrow> lfp f \<le> A"
    1.29    by (auto simp add: lfp_def intro: Inf_lower)
    1.30  
    1.31 -lemma lfp_greatest: "(!!u. f u \<le> u ==> A \<le> u) ==> A \<le> lfp f"
    1.32 +lemma lfp_greatest: "(\<And>u. f u \<le> u \<Longrightarrow> A \<le> u) \<Longrightarrow> A \<le> lfp f"
    1.33    by (auto simp add: lfp_def intro: Inf_greatest)
    1.34  
    1.35  end
    1.36  
    1.37 -lemma lfp_lemma2: "mono f ==> f (lfp f) \<le> lfp f"
    1.38 +lemma lfp_lemma2: "mono f \<Longrightarrow> f (lfp f) \<le> lfp f"
    1.39    by (iprover intro: lfp_greatest order_trans monoD lfp_lowerbound)
    1.40  
    1.41 -lemma lfp_lemma3: "mono f ==> lfp f \<le> f (lfp f)"
    1.42 +lemma lfp_lemma3: "mono f \<Longrightarrow> lfp f \<le> f (lfp f)"
    1.43    by (iprover intro: lfp_lemma2 monoD lfp_lowerbound)
    1.44  
    1.45 -lemma lfp_unfold: "mono f ==> lfp f = f (lfp f)"
    1.46 +lemma lfp_unfold: "mono f \<Longrightarrow> lfp f = f (lfp f)"
    1.47    by (iprover intro: order_antisym lfp_lemma2 lfp_lemma3)
    1.48  
    1.49  lemma lfp_const: "lfp (\<lambda>x. t) = t"
    1.50 -  by (rule lfp_unfold) (simp add:mono_def)
    1.51 +  by (rule lfp_unfold) (simp add: mono_def)
    1.52  
    1.53  
    1.54  subsection \<open>General induction rules for least fixed points\<close>
    1.55  
    1.56 -lemma lfp_ordinal_induct[case_names mono step union]:
    1.57 +lemma lfp_ordinal_induct [case_names mono step union]:
    1.58    fixes f :: "'a::complete_lattice \<Rightarrow> 'a"
    1.59    assumes mono: "mono f"
    1.60 -  and P_f: "\<And>S. P S \<Longrightarrow> S \<le> lfp f \<Longrightarrow> P (f S)"
    1.61 -  and P_Union: "\<And>M. \<forall>S\<in>M. P S \<Longrightarrow> P (Sup M)"
    1.62 +    and P_f: "\<And>S. P S \<Longrightarrow> S \<le> lfp f \<Longrightarrow> P (f S)"
    1.63 +    and P_Union: "\<And>M. \<forall>S\<in>M. P S \<Longrightarrow> P (Sup M)"
    1.64    shows "P (lfp f)"
    1.65  proof -
    1.66    let ?M = "{S. S \<le> lfp f \<and> P S}"
    1.67 @@ -68,96 +65,94 @@
    1.68    also have "Sup ?M = lfp f"
    1.69    proof (rule antisym)
    1.70      show "Sup ?M \<le> lfp f" by (blast intro: Sup_least)
    1.71 -    hence "f (Sup ?M) \<le> f (lfp f)" by (rule mono [THEN monoD])
    1.72 -    hence "f (Sup ?M) \<le> lfp f" using mono [THEN lfp_unfold] by simp
    1.73 -    hence "f (Sup ?M) \<in> ?M" using P_Union by simp (intro P_f Sup_least, auto)
    1.74 -    hence "f (Sup ?M) \<le> Sup ?M" by (rule Sup_upper)
    1.75 -    thus "lfp f \<le> Sup ?M" by (rule lfp_lowerbound)
    1.76 +    then have "f (Sup ?M) \<le> f (lfp f)"
    1.77 +      by (rule mono [THEN monoD])
    1.78 +    then have "f (Sup ?M) \<le> lfp f"
    1.79 +      using mono [THEN lfp_unfold] by simp
    1.80 +    then have "f (Sup ?M) \<in> ?M"
    1.81 +      using P_Union by simp (intro P_f Sup_least, auto)
    1.82 +    then have "f (Sup ?M) \<le> Sup ?M"
    1.83 +      by (rule Sup_upper)
    1.84 +    then show "lfp f \<le> Sup ?M"
    1.85 +      by (rule lfp_lowerbound)
    1.86    qed
    1.87    finally show ?thesis .
    1.88 -qed 
    1.89 +qed
    1.90  
    1.91  theorem lfp_induct:
    1.92 -  assumes mono: "mono f" and ind: "f (inf (lfp f) P) \<le> P"
    1.93 +  assumes mono: "mono f"
    1.94 +    and ind: "f (inf (lfp f) P) \<le> P"
    1.95    shows "lfp f \<le> P"
    1.96  proof (induction rule: lfp_ordinal_induct)
    1.97 -  case (step S) then show ?case
    1.98 +  case (step S)
    1.99 +  then show ?case
   1.100      by (intro order_trans[OF _ ind] monoD[OF mono]) auto
   1.101  qed (auto intro: mono Sup_least)
   1.102  
   1.103  lemma lfp_induct_set:
   1.104 -  assumes lfp: "a: lfp(f)"
   1.105 -    and mono: "mono(f)"
   1.106 -    and indhyp: "!!x. [| x: f(lfp(f) Int {x. P(x)}) |] ==> P(x)"
   1.107 -  shows "P(a)"
   1.108 -  by (rule lfp_induct [THEN subsetD, THEN CollectD, OF mono _ lfp])
   1.109 -     (auto simp: intro: indhyp)
   1.110 +  assumes lfp: "a \<in> lfp f"
   1.111 +    and mono: "mono f"
   1.112 +    and hyp: "\<And>x. x \<in> f (lfp f \<inter> {x. P x}) \<Longrightarrow> P x"
   1.113 +  shows "P a"
   1.114 +  by (rule lfp_induct [THEN subsetD, THEN CollectD, OF mono _ lfp]) (auto intro: hyp)
   1.115  
   1.116 -lemma lfp_ordinal_induct_set: 
   1.117 +lemma lfp_ordinal_induct_set:
   1.118    assumes mono: "mono f"
   1.119 -    and P_f: "!!S. P S ==> P(f S)"
   1.120 -    and P_Union: "!!M. !S:M. P S ==> P (\<Union>M)"
   1.121 -  shows "P(lfp f)"
   1.122 +    and P_f: "\<And>S. P S \<Longrightarrow> P (f S)"
   1.123 +    and P_Union: "\<And>M. \<forall>S\<in>M. P S \<Longrightarrow> P (\<Union>M)"
   1.124 +  shows "P (lfp f)"
   1.125    using assms by (rule lfp_ordinal_induct)
   1.126  
   1.127  
   1.128 -text\<open>Definition forms of \<open>lfp_unfold\<close> and \<open>lfp_induct\<close>, 
   1.129 -    to control unfolding\<close>
   1.130 +text \<open>Definition forms of \<open>lfp_unfold\<close> and \<open>lfp_induct\<close>, to control unfolding.\<close>
   1.131  
   1.132 -lemma def_lfp_unfold: "[| h==lfp(f);  mono(f) |] ==> h = f(h)"
   1.133 +lemma def_lfp_unfold: "h \<equiv> lfp f \<Longrightarrow> mono f \<Longrightarrow> h = f h"
   1.134    by (auto intro!: lfp_unfold)
   1.135  
   1.136 -lemma def_lfp_induct: 
   1.137 -    "[| A == lfp(f); mono(f);
   1.138 -        f (inf A P) \<le> P
   1.139 -     |] ==> A \<le> P"
   1.140 +lemma def_lfp_induct: "A \<equiv> lfp f \<Longrightarrow> mono f \<Longrightarrow> f (inf A P) \<le> P \<Longrightarrow> A \<le> P"
   1.141    by (blast intro: lfp_induct)
   1.142  
   1.143 -lemma def_lfp_induct_set: 
   1.144 -    "[| A == lfp(f);  mono(f);   a:A;                    
   1.145 -        !!x. [| x: f(A Int {x. P(x)}) |] ==> P(x)         
   1.146 -     |] ==> P(a)"
   1.147 +lemma def_lfp_induct_set:
   1.148 +  "A \<equiv> lfp f \<Longrightarrow> mono f \<Longrightarrow> a \<in> A \<Longrightarrow> (\<And>x. x \<in> f (A \<inter> {x. P x}) \<Longrightarrow> P x) \<Longrightarrow> P a"
   1.149    by (blast intro: lfp_induct_set)
   1.150  
   1.151 -(*Monotonicity of lfp!*)
   1.152 -lemma lfp_mono: "(!!Z. f Z \<le> g Z) ==> lfp f \<le> lfp g"
   1.153 -  by (rule lfp_lowerbound [THEN lfp_greatest], blast intro: order_trans)
   1.154 +text \<open>Monotonicity of \<open>lfp\<close>!\<close>
   1.155 +lemma lfp_mono: "(\<And>Z. f Z \<le> g Z) \<Longrightarrow> lfp f \<le> lfp g"
   1.156 +  by (rule lfp_lowerbound [THEN lfp_greatest]) (blast intro: order_trans)
   1.157  
   1.158  
   1.159 -subsection \<open>Proof of Knaster-Tarski Theorem using @{term gfp}\<close>
   1.160 +subsection \<open>Proof of Knaster-Tarski Theorem using \<open>gfp\<close>\<close>
   1.161  
   1.162 -text\<open>@{term "gfp f"} is the greatest lower bound of 
   1.163 -      the set @{term "{u. u \<le> f(u)}"}\<close>
   1.164 +text \<open>@{term "gfp f"} is the greatest lower bound of the set @{term "{u. u \<le> f u}"}\<close>
   1.165  
   1.166 -lemma gfp_upperbound: "X \<le> f X ==> X \<le> gfp f"
   1.167 +lemma gfp_upperbound: "X \<le> f X \<Longrightarrow> X \<le> gfp f"
   1.168    by (auto simp add: gfp_def intro: Sup_upper)
   1.169  
   1.170 -lemma gfp_least: "(!!u. u \<le> f u ==> u \<le> X) ==> gfp f \<le> X"
   1.171 +lemma gfp_least: "(\<And>u. u \<le> f u \<Longrightarrow> u \<le> X) \<Longrightarrow> gfp f \<le> X"
   1.172    by (auto simp add: gfp_def intro: Sup_least)
   1.173  
   1.174 -lemma gfp_lemma2: "mono f ==> gfp f \<le> f (gfp f)"
   1.175 +lemma gfp_lemma2: "mono f \<Longrightarrow> gfp f \<le> f (gfp f)"
   1.176    by (iprover intro: gfp_least order_trans monoD gfp_upperbound)
   1.177  
   1.178 -lemma gfp_lemma3: "mono f ==> f (gfp f) \<le> gfp f"
   1.179 +lemma gfp_lemma3: "mono f \<Longrightarrow> f (gfp f) \<le> gfp f"
   1.180    by (iprover intro: gfp_lemma2 monoD gfp_upperbound)
   1.181  
   1.182 -lemma gfp_unfold: "mono f ==> gfp f = f (gfp f)"
   1.183 +lemma gfp_unfold: "mono f \<Longrightarrow> gfp f = f (gfp f)"
   1.184    by (iprover intro: order_antisym gfp_lemma2 gfp_lemma3)
   1.185  
   1.186  
   1.187  subsection \<open>Coinduction rules for greatest fixed points\<close>
   1.188  
   1.189 -text\<open>weak version\<close>
   1.190 -lemma weak_coinduct: "[| a: X;  X \<subseteq> f(X) |] ==> a : gfp(f)"
   1.191 +text \<open>Weak version.\<close>
   1.192 +lemma weak_coinduct: "a \<in> X \<Longrightarrow> X \<subseteq> f X \<Longrightarrow> a \<in> gfp f"
   1.193    by (rule gfp_upperbound [THEN subsetD]) auto
   1.194  
   1.195 -lemma weak_coinduct_image: "!!X. [| a : X; g`X \<subseteq> f (g`X) |] ==> g a : gfp f"
   1.196 +lemma weak_coinduct_image: "a \<in> X \<Longrightarrow> g`X \<subseteq> f (g`X) \<Longrightarrow> g a \<in> gfp f"
   1.197    apply (erule gfp_upperbound [THEN subsetD])
   1.198    apply (erule imageI)
   1.199    done
   1.200  
   1.201 -lemma coinduct_lemma:
   1.202 -     "[| X \<le> f (sup X (gfp f));  mono f |] ==> sup X (gfp f) \<le> f (sup X (gfp f))"
   1.203 +lemma coinduct_lemma: "X \<le> f (sup X (gfp f)) \<Longrightarrow> mono f \<Longrightarrow> sup X (gfp f) \<le> f (sup X (gfp f))"
   1.204    apply (frule gfp_lemma2)
   1.205    apply (drule mono_sup)
   1.206    apply (rule le_supI)
   1.207 @@ -169,112 +164,113 @@
   1.208    apply assumption
   1.209    done
   1.210  
   1.211 -text\<open>strong version, thanks to Coen and Frost\<close>
   1.212 -lemma coinduct_set: "[| mono(f);  a: X;  X \<subseteq> f(X Un gfp(f)) |] ==> a : gfp(f)"
   1.213 +text \<open>Strong version, thanks to Coen and Frost.\<close>
   1.214 +lemma coinduct_set: "mono f \<Longrightarrow> a \<in> X \<Longrightarrow> X \<subseteq> f (X \<union> gfp f) \<Longrightarrow> a \<in> gfp f"
   1.215    by (rule weak_coinduct[rotated], rule coinduct_lemma) blast+
   1.216  
   1.217 -lemma gfp_fun_UnI2: "[| mono(f);  a: gfp(f) |] ==> a: f(X Un gfp(f))"
   1.218 +lemma gfp_fun_UnI2: "mono f \<Longrightarrow> a \<in> gfp f \<Longrightarrow> a \<in> f (X \<union> gfp f)"
   1.219    by (blast dest: gfp_lemma2 mono_Un)
   1.220  
   1.221  lemma gfp_ordinal_induct[case_names mono step union]:
   1.222    fixes f :: "'a::complete_lattice \<Rightarrow> 'a"
   1.223    assumes mono: "mono f"
   1.224 -  and P_f: "\<And>S. P S \<Longrightarrow> gfp f \<le> S \<Longrightarrow> P (f S)"
   1.225 -  and P_Union: "\<And>M. \<forall>S\<in>M. P S \<Longrightarrow> P (Inf M)"
   1.226 +    and P_f: "\<And>S. P S \<Longrightarrow> gfp f \<le> S \<Longrightarrow> P (f S)"
   1.227 +    and P_Union: "\<And>M. \<forall>S\<in>M. P S \<Longrightarrow> P (Inf M)"
   1.228    shows "P (gfp f)"
   1.229  proof -
   1.230    let ?M = "{S. gfp f \<le> S \<and> P S}"
   1.231    have "P (Inf ?M)" using P_Union by simp
   1.232    also have "Inf ?M = gfp f"
   1.233    proof (rule antisym)
   1.234 -    show "gfp f \<le> Inf ?M" by (blast intro: Inf_greatest)
   1.235 -    hence "f (gfp f) \<le> f (Inf ?M)" by (rule mono [THEN monoD])
   1.236 -    hence "gfp f \<le> f (Inf ?M)" using mono [THEN gfp_unfold] by simp
   1.237 -    hence "f (Inf ?M) \<in> ?M" using P_Union by simp (intro P_f Inf_greatest, auto)
   1.238 -    hence "Inf ?M \<le> f (Inf ?M)" by (rule Inf_lower)
   1.239 -    thus "Inf ?M \<le> gfp f" by (rule gfp_upperbound)
   1.240 +    show "gfp f \<le> Inf ?M"
   1.241 +      by (blast intro: Inf_greatest)
   1.242 +    then have "f (gfp f) \<le> f (Inf ?M)"
   1.243 +      by (rule mono [THEN monoD])
   1.244 +    then have "gfp f \<le> f (Inf ?M)"
   1.245 +      using mono [THEN gfp_unfold] by simp
   1.246 +    then have "f (Inf ?M) \<in> ?M"
   1.247 +      using P_Union by simp (intro P_f Inf_greatest, auto)
   1.248 +    then have "Inf ?M \<le> f (Inf ?M)"
   1.249 +      by (rule Inf_lower)
   1.250 +    then show "Inf ?M \<le> gfp f"
   1.251 +      by (rule gfp_upperbound)
   1.252    qed
   1.253    finally show ?thesis .
   1.254 -qed 
   1.255 +qed
   1.256  
   1.257 -lemma coinduct: assumes mono: "mono f" and ind: "X \<le> f (sup X (gfp f))" shows "X \<le> gfp f"
   1.258 +lemma coinduct:
   1.259 +  assumes mono: "mono f"
   1.260 +    and ind: "X \<le> f (sup X (gfp f))"
   1.261 +  shows "X \<le> gfp f"
   1.262  proof (induction rule: gfp_ordinal_induct)
   1.263    case (step S) then show ?case
   1.264      by (intro order_trans[OF ind _] monoD[OF mono]) auto
   1.265  qed (auto intro: mono Inf_greatest)
   1.266  
   1.267 +
   1.268  subsection \<open>Even Stronger Coinduction Rule, by Martin Coen\<close>
   1.269  
   1.270 -text\<open>Weakens the condition @{term "X \<subseteq> f(X)"} to one expressed using both
   1.271 +text \<open>Weakens the condition @{term "X \<subseteq> f X"} to one expressed using both
   1.272    @{term lfp} and @{term gfp}\<close>
   1.273 -
   1.274 -lemma coinduct3_mono_lemma: "mono(f) ==> mono(%x. f(x) Un X Un B)"
   1.275 -by (iprover intro: subset_refl monoI Un_mono monoD)
   1.276 +lemma coinduct3_mono_lemma: "mono f \<Longrightarrow> mono (\<lambda>x. f x \<union> X \<union> B)"
   1.277 +  by (iprover intro: subset_refl monoI Un_mono monoD)
   1.278  
   1.279  lemma coinduct3_lemma:
   1.280 -     "[| X \<subseteq> f(lfp(%x. f(x) Un X Un gfp(f)));  mono(f) |]
   1.281 -      ==> lfp(%x. f(x) Un X Un gfp(f)) \<subseteq> f(lfp(%x. f(x) Un X Un gfp(f)))"
   1.282 -apply (rule subset_trans)
   1.283 -apply (erule coinduct3_mono_lemma [THEN lfp_lemma3])
   1.284 -apply (rule Un_least [THEN Un_least])
   1.285 -apply (rule subset_refl, assumption)
   1.286 -apply (rule gfp_unfold [THEN equalityD1, THEN subset_trans], assumption)
   1.287 -apply (rule monoD, assumption)
   1.288 -apply (subst coinduct3_mono_lemma [THEN lfp_unfold], auto)
   1.289 -done
   1.290 +  "X \<subseteq> f (lfp (\<lambda>x. f x \<union> X \<union> gfp f)) \<Longrightarrow> mono f \<Longrightarrow>
   1.291 +    lfp (\<lambda>x. f x \<union> X \<union> gfp f) \<subseteq> f (lfp (\<lambda>x. f x \<union> X \<union> gfp f))"
   1.292 +  apply (rule subset_trans)
   1.293 +  apply (erule coinduct3_mono_lemma [THEN lfp_lemma3])
   1.294 +  apply (rule Un_least [THEN Un_least])
   1.295 +  apply (rule subset_refl, assumption)
   1.296 +  apply (rule gfp_unfold [THEN equalityD1, THEN subset_trans], assumption)
   1.297 +  apply (rule monoD, assumption)
   1.298 +  apply (subst coinduct3_mono_lemma [THEN lfp_unfold], auto)
   1.299 +  done
   1.300  
   1.301 -lemma coinduct3: 
   1.302 -  "[| mono(f);  a:X;  X \<subseteq> f(lfp(%x. f(x) Un X Un gfp(f))) |] ==> a : gfp(f)"
   1.303 -apply (rule coinduct3_lemma [THEN [2] weak_coinduct])
   1.304 -apply (rule coinduct3_mono_lemma [THEN lfp_unfold, THEN ssubst])
   1.305 -apply (simp_all)
   1.306 -done
   1.307 +lemma coinduct3: "mono f \<Longrightarrow> a \<in> X \<Longrightarrow> X \<subseteq> f (lfp (\<lambda>x. f x \<union> X \<union> gfp f)) \<Longrightarrow> a \<in> gfp f"
   1.308 +  apply (rule coinduct3_lemma [THEN [2] weak_coinduct])
   1.309 +  apply (rule coinduct3_mono_lemma [THEN lfp_unfold, THEN ssubst])
   1.310 +  apply simp_all
   1.311 +  done
   1.312  
   1.313 -text\<open>Definition forms of \<open>gfp_unfold\<close> and \<open>coinduct\<close>, 
   1.314 -    to control unfolding\<close>
   1.315 +text  \<open>Definition forms of \<open>gfp_unfold\<close> and \<open>coinduct\<close>, to control unfolding.\<close>
   1.316  
   1.317 -lemma def_gfp_unfold: "[| A==gfp(f);  mono(f) |] ==> A = f(A)"
   1.318 +lemma def_gfp_unfold: "A \<equiv> gfp f \<Longrightarrow> mono f \<Longrightarrow> A = f A"
   1.319    by (auto intro!: gfp_unfold)
   1.320  
   1.321 -lemma def_coinduct:
   1.322 -     "[| A==gfp(f);  mono(f);  X \<le> f(sup X A) |] ==> X \<le> A"
   1.323 +lemma def_coinduct: "A \<equiv> gfp f \<Longrightarrow> mono f \<Longrightarrow> X \<le> f (sup X A) \<Longrightarrow> X \<le> A"
   1.324    by (iprover intro!: coinduct)
   1.325  
   1.326 -lemma def_coinduct_set:
   1.327 -     "[| A==gfp(f);  mono(f);  a:X;  X \<subseteq> f(X Un A) |] ==> a: A"
   1.328 +lemma def_coinduct_set: "A \<equiv> gfp f \<Longrightarrow> mono f \<Longrightarrow> a \<in> X \<Longrightarrow> X \<subseteq> f (X \<union> A) \<Longrightarrow> a \<in> A"
   1.329    by (auto intro!: coinduct_set)
   1.330  
   1.331 -(*The version used in the induction/coinduction package*)
   1.332  lemma def_Collect_coinduct:
   1.333 -    "[| A == gfp(%w. Collect(P(w)));  mono(%w. Collect(P(w)));   
   1.334 -        a: X;  !!z. z: X ==> P (X Un A) z |] ==>  
   1.335 -     a : A"
   1.336 +  "A \<equiv> gfp (\<lambda>w. Collect (P w)) \<Longrightarrow> mono (\<lambda>w. Collect (P w)) \<Longrightarrow> a \<in> X \<Longrightarrow>
   1.337 +    (\<And>z. z \<in> X \<Longrightarrow> P (X \<union> A) z) \<Longrightarrow> a \<in> A"
   1.338    by (erule def_coinduct_set) auto
   1.339  
   1.340 -lemma def_coinduct3:
   1.341 -    "[| A==gfp(f); mono(f);  a:X;  X \<subseteq> f(lfp(%x. f(x) Un X Un A)) |] ==> a: A"
   1.342 +lemma def_coinduct3: "A \<equiv> gfp f \<Longrightarrow> mono f \<Longrightarrow> a \<in> X \<Longrightarrow> X \<subseteq> f (lfp (\<lambda>x. f x \<union> X \<union> A)) \<Longrightarrow> a \<in> A"
   1.343    by (auto intro!: coinduct3)
   1.344  
   1.345 -text\<open>Monotonicity of @{term gfp}!\<close>
   1.346 -lemma gfp_mono: "(!!Z. f Z \<le> g Z) ==> gfp f \<le> gfp g"
   1.347 -  by (rule gfp_upperbound [THEN gfp_least], blast intro: order_trans)
   1.348 +text \<open>Monotonicity of @{term gfp}!\<close>
   1.349 +lemma gfp_mono: "(\<And>Z. f Z \<le> g Z) \<Longrightarrow> gfp f \<le> gfp g"
   1.350 +  by (rule gfp_upperbound [THEN gfp_least]) (blast intro: order_trans)
   1.351 +
   1.352  
   1.353  subsection \<open>Rules for fixed point calculus\<close>
   1.354  
   1.355 -
   1.356  lemma lfp_rolling:
   1.357    assumes "mono g" "mono f"
   1.358    shows "g (lfp (\<lambda>x. f (g x))) = lfp (\<lambda>x. g (f x))"
   1.359  proof (rule antisym)
   1.360    have *: "mono (\<lambda>x. f (g x))"
   1.361      using assms by (auto simp: mono_def)
   1.362 -
   1.363    show "lfp (\<lambda>x. g (f x)) \<le> g (lfp (\<lambda>x. f (g x)))"
   1.364      by (rule lfp_lowerbound) (simp add: lfp_unfold[OF *, symmetric])
   1.365 -
   1.366    show "g (lfp (\<lambda>x. f (g x))) \<le> lfp (\<lambda>x. g (f x))"
   1.367    proof (rule lfp_greatest)
   1.368 -    fix u assume "g (f u) \<le> u"
   1.369 +    fix u
   1.370 +    assume "g (f u) \<le> u"
   1.371      moreover then have "g (lfp (\<lambda>x. f (g x))) \<le> g (f u)"
   1.372        by (intro assms[THEN monoD] lfp_lowerbound)
   1.373      ultimately show "g (lfp (\<lambda>x. f (g x))) \<le> u"
   1.374 @@ -309,7 +305,6 @@
   1.375      using assms by (auto simp: mono_def)
   1.376    show "g (gfp (\<lambda>x. f (g x))) \<le> gfp (\<lambda>x. g (f x))"
   1.377      by (rule gfp_upperbound) (simp add: gfp_unfold[OF *, symmetric])
   1.378 -
   1.379    show "gfp (\<lambda>x. g (f x)) \<le> g (gfp (\<lambda>x. f (g x)))"
   1.380    proof (rule gfp_least)
   1.381      fix u assume "u \<le> g (f u)"
   1.382 @@ -339,6 +334,7 @@
   1.383    qed
   1.384  qed
   1.385  
   1.386 +
   1.387  subsection \<open>Inductive predicates and sets\<close>
   1.388  
   1.389  text \<open>Package setup.\<close>