src/HOL/Library/Order_Continuity.thy
 changeset 62374 cb27a55d868a parent 62373 ea7a442e9a56 child 63540 f8652d0534fa
1.1 --- a/src/HOL/Library/Order_Continuity.thy	Thu Feb 18 13:54:44 2016 +0100
1.2 +++ b/src/HOL/Library/Order_Continuity.thy	Fri Feb 19 12:25:57 2016 +0100
1.3 @@ -393,12 +393,12 @@
1.4  subsubsection \<open>Least fixed points in countable complete lattices\<close>
1.6  definition (in countable_complete_lattice) cclfp :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a"
1.7 -  where "cclfp f = (\<Squnion>i. (f ^^ i) \<bottom>)"
1.8 +  where "cclfp f = (SUP i. (f ^^ i) bot)"
1.10  lemma cclfp_unfold:
1.11    assumes "sup_continuous F" shows "cclfp F = F (cclfp F)"
1.12  proof -
1.13 -  have "cclfp F = (\<Squnion>i. F ((F ^^ i) \<bottom>))"
1.14 +  have "cclfp F = (SUP i. F ((F ^^ i) bot))"
1.15      unfolding cclfp_def by (subst UNIV_nat_eq) auto
1.16    also have "\<dots> = F (cclfp F)"
1.17      unfolding cclfp_def
1.18 @@ -409,7 +409,7 @@
1.19  lemma cclfp_lowerbound: assumes f: "mono f" and A: "f A \<le> A" shows "cclfp f \<le> A"
1.20    unfolding cclfp_def
1.21  proof (intro ccSUP_least)
1.22 -  fix i show "(f ^^ i) \<bottom> \<le> A"
1.23 +  fix i show "(f ^^ i) bot \<le> A"
1.24    proof (induction i)
1.25      case (Suc i) from monoD[OF f this] A show ?case
1.26        by auto
1.27 @@ -418,12 +418,12 @@
1.29  lemma cclfp_transfer:
1.30    assumes "sup_continuous \<alpha>" "mono f"
1.31 -  assumes "\<alpha> \<bottom> = \<bottom>" "\<And>x. \<alpha> (f x) = g (\<alpha> x)"
1.32 +  assumes "\<alpha> bot = bot" "\<And>x. \<alpha> (f x) = g (\<alpha> x)"
1.33    shows "\<alpha> (cclfp f) = cclfp g"
1.34  proof -
1.35 -  have "\<alpha> (cclfp f) = (\<Squnion>i. \<alpha> ((f ^^ i) \<bottom>))"
1.36 +  have "\<alpha> (cclfp f) = (SUP i. \<alpha> ((f ^^ i) bot))"
1.37      unfolding cclfp_def by (intro sup_continuousD assms mono_funpow sup_continuous_mono)
1.38 -  moreover have "\<alpha> ((f ^^ i) \<bottom>) = (g ^^ i) \<bottom>" for i
1.39 +  moreover have "\<alpha> ((f ^^ i) bot) = (g ^^ i) bot" for i
1.40      by (induction i) (simp_all add: assms)
1.41    ultimately show ?thesis