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>
```