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.5  
     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.9  
    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.28  
    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
    1.42      by (simp add: cclfp_def)