change some lemma names containing 'UU' to 'bottom'
authorhuffman
Tue Jan 04 15:32:56 2011 -0800 (2011-01-04)
changeset 414301aa23e9f2c87
parent 41429 cf5f025bc3c7
child 41431 138f414f14cb
change some lemma names containing 'UU' to 'bottom'
NEWS
src/HOL/HOLCF/Adm.thy
src/HOL/HOLCF/Algebraic.thy
src/HOL/HOLCF/Bifinite.thy
src/HOL/HOLCF/Cfun.thy
src/HOL/HOLCF/ConvexPD.thy
src/HOL/HOLCF/Cpodef.thy
src/HOL/HOLCF/Deflation.thy
src/HOL/HOLCF/Domain_Aux.thy
src/HOL/HOLCF/Fix.thy
src/HOL/HOLCF/Fun_Cpo.thy
src/HOL/HOLCF/HOLCF.thy
src/HOL/HOLCF/Lift.thy
src/HOL/HOLCF/LowerPD.thy
src/HOL/HOLCF/Pcpo.thy
src/HOL/HOLCF/Product_Cpo.thy
src/HOL/HOLCF/Sprod.thy
src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML
src/HOL/HOLCF/Tools/Domain/domain_take_proofs.ML
src/HOL/HOLCF/Universal.thy
src/HOL/HOLCF/Up.thy
src/HOL/HOLCF/UpperPD.thy
     1.1 --- a/NEWS	Tue Jan 04 15:03:27 2011 -0800
     1.2 +++ b/NEWS	Tue Jan 04 15:32:56 2011 -0800
     1.3 @@ -599,6 +599,10 @@
     1.4    thelub_cprod    ~> lub_prod
     1.5    minimal_cprod   ~> minimal_prod
     1.6    inst_cprod_pcpo ~> inst_prod_pcpo
     1.7 +  UU_I            ~> bottomI
     1.8 +  compact_UU      ~> compact_bottom
     1.9 +  deflation_UU    ~> deflation_bottom
    1.10 +  finite_deflation_UU ~> finite_deflation_bottom
    1.11  
    1.12  * Many legacy theorem names have been discontinued. INCOMPATIBILITY.
    1.13    sq_ord_less_eq_trans ~> below_eq_trans
     2.1 --- a/src/HOL/HOLCF/Adm.thy	Tue Jan 04 15:03:27 2011 -0800
     2.2 +++ b/src/HOL/HOLCF/Adm.thy	Tue Jan 04 15:32:56 2011 -0800
     2.3 @@ -175,7 +175,7 @@
     2.4    "\<lbrakk>compact k; cont (\<lambda>x. t x)\<rbrakk> \<Longrightarrow> adm (\<lambda>x. k \<noteq> t x)"
     2.5  by (simp add: po_eq_conv)
     2.6  
     2.7 -lemma compact_UU [simp, intro]: "compact \<bottom>"
     2.8 +lemma compact_bottom [simp, intro]: "compact \<bottom>"
     2.9  by (rule compactI, simp)
    2.10  
    2.11  text {* Any upward-closed predicate is admissible. *}
     3.1 --- a/src/HOL/HOLCF/Algebraic.thy	Tue Jan 04 15:03:27 2011 -0800
     3.2 +++ b/src/HOL/HOLCF/Algebraic.thy	Tue Jan 04 15:32:56 2011 -0800
     3.3 @@ -13,7 +13,7 @@
     3.4  subsection {* Type constructor for finite deflations *}
     3.5  
     3.6  typedef (open) 'a fin_defl = "{d::'a \<rightarrow> 'a. finite_deflation d}"
     3.7 -by (fast intro: finite_deflation_UU)
     3.8 +by (fast intro: finite_deflation_bottom)
     3.9  
    3.10  instantiation fin_defl :: (bifinite) below
    3.11  begin
    3.12 @@ -138,14 +138,14 @@
    3.13  apply (induct x rule: defl.principal_induct, simp)
    3.14  apply (rule defl.principal_mono)
    3.15  apply (simp add: below_fin_defl_def)
    3.16 -apply (simp add: Abs_fin_defl_inverse finite_deflation_UU)
    3.17 +apply (simp add: Abs_fin_defl_inverse finite_deflation_bottom)
    3.18  done
    3.19  
    3.20  instance defl :: (bifinite) pcpo
    3.21  by intro_classes (fast intro: defl_minimal)
    3.22  
    3.23  lemma inst_defl_pcpo: "\<bottom> = defl_principal (Abs_fin_defl \<bottom>)"
    3.24 -by (rule defl_minimal [THEN UU_I, symmetric])
    3.25 +by (rule defl_minimal [THEN bottomI, symmetric])
    3.26  
    3.27  subsection {* Applying algebraic deflations *}
    3.28  
    3.29 @@ -209,11 +209,11 @@
    3.30  apply (subst inst_defl_pcpo)
    3.31  apply (subst cast_defl_principal)
    3.32  apply (rule Abs_fin_defl_inverse)
    3.33 -apply (simp add: finite_deflation_UU)
    3.34 +apply (simp add: finite_deflation_bottom)
    3.35  done
    3.36  
    3.37  lemma cast_strict2 [simp]: "cast\<cdot>A\<cdot>\<bottom> = \<bottom>"
    3.38 -by (rule cast.below [THEN UU_I])
    3.39 +by (rule cast.below [THEN bottomI])
    3.40  
    3.41  subsection {* Deflation combinators *}
    3.42  
     4.1 --- a/src/HOL/HOLCF/Bifinite.thy	Tue Jan 04 15:03:27 2011 -0800
     4.2 +++ b/src/HOL/HOLCF/Bifinite.thy	Tue Jan 04 15:32:56 2011 -0800
     4.3 @@ -253,7 +253,7 @@
     4.4  qed
     4.5  
     4.6  lemma approx_chain_unit: "approx_chain (\<bottom> :: nat \<Rightarrow> unit \<rightarrow> unit)"
     4.7 -by (simp add: approx_chain_def cfun_eq_iff finite_deflation_UU)
     4.8 +by (simp add: approx_chain_def cfun_eq_iff finite_deflation_bottom)
     4.9  
    4.10  instance unit :: bifinite
    4.11    by default (fast intro!: approx_chain_unit)
     5.1 --- a/src/HOL/HOLCF/Cfun.thy	Tue Jan 04 15:03:27 2011 -0800
     5.2 +++ b/src/HOL/HOLCF/Cfun.thy	Tue Jan 04 15:32:56 2011 -0800
     5.3 @@ -92,20 +92,20 @@
     5.4  
     5.5  subsection {* Continuous function space is pointed *}
     5.6  
     5.7 -lemma UU_cfun: "\<bottom> \<in> cfun"
     5.8 +lemma bottom_cfun: "\<bottom> \<in> cfun"
     5.9  by (simp add: cfun_def inst_fun_pcpo)
    5.10  
    5.11  instance cfun :: (cpo, discrete_cpo) discrete_cpo
    5.12  by intro_classes (simp add: below_cfun_def Rep_cfun_inject)
    5.13  
    5.14  instance cfun :: (cpo, pcpo) pcpo
    5.15 -by (rule typedef_pcpo [OF type_definition_cfun below_cfun_def UU_cfun])
    5.16 +by (rule typedef_pcpo [OF type_definition_cfun below_cfun_def bottom_cfun])
    5.17  
    5.18  lemmas Rep_cfun_strict =
    5.19 -  typedef_Rep_strict [OF type_definition_cfun below_cfun_def UU_cfun]
    5.20 +  typedef_Rep_strict [OF type_definition_cfun below_cfun_def bottom_cfun]
    5.21  
    5.22  lemmas Abs_cfun_strict =
    5.23 -  typedef_Abs_strict [OF type_definition_cfun below_cfun_def UU_cfun]
    5.24 +  typedef_Abs_strict [OF type_definition_cfun below_cfun_def bottom_cfun]
    5.25  
    5.26  text {* function application is strict in its first argument *}
    5.27  
    5.28 @@ -261,7 +261,7 @@
    5.29  text {* strictness *}
    5.30  
    5.31  lemma strictI: "f\<cdot>x = \<bottom> \<Longrightarrow> f\<cdot>\<bottom> = \<bottom>"
    5.32 -apply (rule UU_I)
    5.33 +apply (rule bottomI)
    5.34  apply (erule subst)
    5.35  apply (rule minimal [THEN monofun_cfun_arg])
    5.36  done
    5.37 @@ -364,7 +364,7 @@
    5.38  
    5.39  lemma retraction_strict:
    5.40    "\<forall>x. f\<cdot>(g\<cdot>x) = x \<Longrightarrow> f\<cdot>\<bottom> = \<bottom>"
    5.41 -apply (rule UU_I)
    5.42 +apply (rule bottomI)
    5.43  apply (drule_tac x="\<bottom>" in spec)
    5.44  apply (erule subst)
    5.45  apply (rule monofun_cfun_arg)
    5.46 @@ -406,7 +406,7 @@
    5.47    "f\<cdot>x = (c::'b::flat) \<Longrightarrow> f\<cdot>\<bottom> = \<bottom> \<or> (\<forall>z. f\<cdot>z = c)"
    5.48  apply (case_tac "f\<cdot>x = \<bottom>")
    5.49  apply (rule disjI1)
    5.50 -apply (rule UU_I)
    5.51 +apply (rule bottomI)
    5.52  apply (erule_tac t="\<bottom>" in subst)
    5.53  apply (rule minimal [THEN monofun_cfun_arg])
    5.54  apply clarify
     6.1 --- a/src/HOL/HOLCF/ConvexPD.thy	Tue Jan 04 15:03:27 2011 -0800
     6.2 +++ b/src/HOL/HOLCF/ConvexPD.thy	Tue Jan 04 15:32:56 2011 -0800
     6.3 @@ -161,7 +161,7 @@
     6.4  by intro_classes (fast intro: convex_pd_minimal)
     6.5  
     6.6  lemma inst_convex_pd_pcpo: "\<bottom> = convex_principal (PDUnit compact_bot)"
     6.7 -by (rule convex_pd_minimal [THEN UU_I, symmetric])
     6.8 +by (rule convex_pd_minimal [THEN bottomI, symmetric])
     6.9  
    6.10  
    6.11  subsection {* Monadic unit and plus *}
     7.1 --- a/src/HOL/HOLCF/Cpodef.thy	Tue Jan 04 15:03:27 2011 -0800
     7.2 +++ b/src/HOL/HOLCF/Cpodef.thy	Tue Jan 04 15:32:56 2011 -0800
     7.3 @@ -203,9 +203,9 @@
     7.4    fixes Abs :: "'a::pcpo \<Rightarrow> 'b::cpo"
     7.5    assumes type: "type_definition Rep Abs A"
     7.6      and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
     7.7 -    and UU_in_A: "\<bottom> \<in> A"
     7.8 +    and bottom_in_A: "\<bottom> \<in> A"
     7.9    shows "OFCLASS('b, pcpo_class)"
    7.10 -by (rule typedef_pcpo_generic [OF type below UU_in_A], rule minimal)
    7.11 +by (rule typedef_pcpo_generic [OF type below bottom_in_A], rule minimal)
    7.12  
    7.13  subsubsection {* Strictness of \emph{Rep} and \emph{Abs} *}
    7.14  
    7.15 @@ -217,36 +217,36 @@
    7.16  theorem typedef_Abs_strict:
    7.17    assumes type: "type_definition Rep Abs A"
    7.18      and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
    7.19 -    and UU_in_A: "\<bottom> \<in> A"
    7.20 +    and bottom_in_A: "\<bottom> \<in> A"
    7.21    shows "Abs \<bottom> = \<bottom>"
    7.22 - apply (rule UU_I, unfold below)
    7.23 - apply (simp add: type_definition.Abs_inverse [OF type UU_in_A])
    7.24 + apply (rule bottomI, unfold below)
    7.25 + apply (simp add: type_definition.Abs_inverse [OF type bottom_in_A])
    7.26  done
    7.27  
    7.28  theorem typedef_Rep_strict:
    7.29    assumes type: "type_definition Rep Abs A"
    7.30      and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
    7.31 -    and UU_in_A: "\<bottom> \<in> A"
    7.32 +    and bottom_in_A: "\<bottom> \<in> A"
    7.33    shows "Rep \<bottom> = \<bottom>"
    7.34 - apply (rule typedef_Abs_strict [OF type below UU_in_A, THEN subst])
    7.35 - apply (rule type_definition.Abs_inverse [OF type UU_in_A])
    7.36 + apply (rule typedef_Abs_strict [OF type below bottom_in_A, THEN subst])
    7.37 + apply (rule type_definition.Abs_inverse [OF type bottom_in_A])
    7.38  done
    7.39  
    7.40  theorem typedef_Abs_bottom_iff:
    7.41    assumes type: "type_definition Rep Abs A"
    7.42      and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
    7.43 -    and UU_in_A: "\<bottom> \<in> A"
    7.44 +    and bottom_in_A: "\<bottom> \<in> A"
    7.45    shows "x \<in> A \<Longrightarrow> (Abs x = \<bottom>) = (x = \<bottom>)"
    7.46 - apply (rule typedef_Abs_strict [OF type below UU_in_A, THEN subst])
    7.47 - apply (simp add: type_definition.Abs_inject [OF type] UU_in_A)
    7.48 + apply (rule typedef_Abs_strict [OF type below bottom_in_A, THEN subst])
    7.49 + apply (simp add: type_definition.Abs_inject [OF type] bottom_in_A)
    7.50  done
    7.51  
    7.52  theorem typedef_Rep_bottom_iff:
    7.53    assumes type: "type_definition Rep Abs A"
    7.54      and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
    7.55 -    and UU_in_A: "\<bottom> \<in> A"
    7.56 +    and bottom_in_A: "\<bottom> \<in> A"
    7.57    shows "(Rep x = \<bottom>) = (x = \<bottom>)"
    7.58 - apply (rule typedef_Rep_strict [OF type below UU_in_A, THEN subst])
    7.59 + apply (rule typedef_Rep_strict [OF type below bottom_in_A, THEN subst])
    7.60   apply (simp add: type_definition.Rep_inject [OF type])
    7.61  done
    7.62  
    7.63 @@ -256,12 +256,12 @@
    7.64    fixes Abs :: "'a::flat \<Rightarrow> 'b::pcpo"
    7.65    assumes type: "type_definition Rep Abs A"
    7.66      and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
    7.67 -    and UU_in_A: "\<bottom> \<in> A"
    7.68 +    and bottom_in_A: "\<bottom> \<in> A"
    7.69    shows "OFCLASS('b, flat_class)"
    7.70   apply (intro_classes)
    7.71   apply (unfold below)
    7.72   apply (simp add: type_definition.Rep_inject [OF type, symmetric])
    7.73 - apply (simp add: typedef_Rep_strict [OF type below UU_in_A])
    7.74 + apply (simp add: typedef_Rep_strict [OF type below bottom_in_A])
    7.75   apply (simp add: ax_flat)
    7.76  done
    7.77  
     8.1 --- a/src/HOL/HOLCF/Deflation.thy	Tue Jan 04 15:03:27 2011 -0800
     8.2 +++ b/src/HOL/HOLCF/Deflation.thy	Tue Jan 04 15:32:56 2011 -0800
     8.3 @@ -56,7 +56,7 @@
     8.4  end
     8.5  
     8.6  lemma deflation_strict: "deflation d \<Longrightarrow> d\<cdot>\<bottom> = \<bottom>"
     8.7 -by (rule deflation.below [THEN UU_I])
     8.8 +by (rule deflation.below [THEN bottomI])
     8.9  
    8.10  lemma adm_deflation: "adm (\<lambda>d. deflation d)"
    8.11  by (simp add: deflation_def)
    8.12 @@ -64,7 +64,7 @@
    8.13  lemma deflation_ID: "deflation ID"
    8.14  by (simp add: deflation.intro)
    8.15  
    8.16 -lemma deflation_UU: "deflation \<bottom>"
    8.17 +lemma deflation_bottom: "deflation \<bottom>"
    8.18  by (simp add: deflation.intro)
    8.19  
    8.20  lemma deflation_below_iff:
    8.21 @@ -160,7 +160,7 @@
    8.22    "finite_deflation d \<Longrightarrow> deflation d"
    8.23  unfolding finite_deflation_def by simp
    8.24  
    8.25 -lemma finite_deflation_UU: "finite_deflation \<bottom>"
    8.26 +lemma finite_deflation_bottom: "finite_deflation \<bottom>"
    8.27  by default simp_all
    8.28  
    8.29  
     9.1 --- a/src/HOL/HOLCF/Domain_Aux.thy	Tue Jan 04 15:03:27 2011 -0800
     9.2 +++ b/src/HOL/HOLCF/Domain_Aux.thy	Tue Jan 04 15:32:56 2011 -0800
     9.3 @@ -52,7 +52,7 @@
     9.4    have "\<bottom> \<sqsubseteq> rep\<cdot>\<bottom>" ..
     9.5    then have "abs\<cdot>\<bottom> \<sqsubseteq> abs\<cdot>(rep\<cdot>\<bottom>)" by (rule monofun_cfun_arg)
     9.6    then have "abs\<cdot>\<bottom> \<sqsubseteq> \<bottom>" by simp
     9.7 -  then show ?thesis by (rule UU_I)
     9.8 +  then show ?thesis by (rule bottomI)
     9.9  qed
    9.10  
    9.11  lemma rep_strict: "rep\<cdot>\<bottom> = \<bottom>"
    10.1 --- a/src/HOL/HOLCF/Fix.thy	Tue Jan 04 15:03:27 2011 -0800
    10.2 +++ b/src/HOL/HOLCF/Fix.thy	Tue Jan 04 15:32:56 2011 -0800
    10.3 @@ -122,7 +122,7 @@
    10.4  apply (rule iffI)
    10.5  apply (erule subst)
    10.6  apply (rule fix_eq [symmetric])
    10.7 -apply (erule fix_least [THEN UU_I])
    10.8 +apply (erule fix_least [THEN bottomI])
    10.9  done
   10.10  
   10.11  lemma fix_strict: "F\<cdot>\<bottom> = \<bottom> \<Longrightarrow> fix\<cdot>F = \<bottom>"
    11.1 --- a/src/HOL/HOLCF/Fun_Cpo.thy	Tue Jan 04 15:03:27 2011 -0800
    11.2 +++ b/src/HOL/HOLCF/Fun_Cpo.thy	Tue Jan 04 15:32:56 2011 -0800
    11.3 @@ -96,13 +96,13 @@
    11.4  by default (fast intro: minimal_fun)
    11.5  
    11.6  lemma inst_fun_pcpo: "\<bottom> = (\<lambda>x. \<bottom>)"
    11.7 -by (rule minimal_fun [THEN UU_I, symmetric])
    11.8 +by (rule minimal_fun [THEN bottomI, symmetric])
    11.9  
   11.10  lemma app_strict [simp]: "\<bottom> x = \<bottom>"
   11.11  by (simp add: inst_fun_pcpo)
   11.12  
   11.13  lemma lambda_strict: "(\<lambda>x. \<bottom>) = \<bottom>"
   11.14 -by (rule UU_I, rule minimal_fun)
   11.15 +by (rule bottomI, rule minimal_fun)
   11.16  
   11.17  subsection {* Propagation of monotonicity and continuity *}
   11.18  
    12.1 --- a/src/HOL/HOLCF/HOLCF.thy	Tue Jan 04 15:03:27 2011 -0800
    12.2 +++ b/src/HOL/HOLCF/HOLCF.thy	Tue Jan 04 15:32:56 2011 -0800
    12.3 @@ -35,5 +35,12 @@
    12.4  lemmas contlub_cfun = lub_APP [symmetric]
    12.5  lemmas contlub_LAM = lub_LAM [symmetric]
    12.6  lemmas thelubI = lub_eqI
    12.7 +lemmas UU_I = bottomI
    12.8 +lemmas lift_distinct1 = lift.distinct(1)
    12.9 +lemmas lift_distinct2 = lift.distinct(2)
   12.10 +lemmas Def_not_UU = lift.distinct(2)
   12.11 +lemmas Def_inject = lift.inject
   12.12 +lemmas below_UU_iff = below_bottom_iff
   12.13 +lemmas eq_UU_iff = eq_bottom_iff
   12.14  
   12.15  end
    13.1 --- a/src/HOL/HOLCF/Lift.thy	Tue Jan 04 15:03:27 2011 -0800
    13.2 +++ b/src/HOL/HOLCF/Lift.thy	Tue Jan 04 15:32:56 2011 -0800
    13.3 @@ -32,13 +32,7 @@
    13.4  rep_datatype "\<bottom>\<Colon>'a lift" Def
    13.5    by (erule lift_induct) (simp_all add: Def_def Abs_lift_inject inst_lift_pcpo)
    13.6  
    13.7 -lemmas lift_distinct1 = lift.distinct(1)
    13.8 -lemmas lift_distinct2 = lift.distinct(2)
    13.9 -lemmas Def_not_UU = lift.distinct(2)
   13.10 -lemmas Def_inject = lift.inject
   13.11 -
   13.12 -
   13.13 -text {* @{term UU} and @{term Def} *}
   13.14 +text {* @{term bottom} and @{term Def} *}
   13.15  
   13.16  lemma not_Undef_is_Def: "(x \<noteq> \<bottom>) = (\<exists>y. x = Def y)"
   13.17    by (cases x) simp_all
   13.18 @@ -47,7 +41,7 @@
   13.19    by (cases x) simp_all
   13.20  
   13.21  text {*
   13.22 -  For @{term "x ~= UU"} in assumptions @{text defined} replaces @{text
   13.23 +  For @{term "x ~= \<bottom>"} in assumptions @{text defined} replaces @{text
   13.24    x} by @{text "Def a"} in conclusion. *}
   13.25  
   13.26  method_setup defined = {*
    14.1 --- a/src/HOL/HOLCF/LowerPD.thy	Tue Jan 04 15:03:27 2011 -0800
    14.2 +++ b/src/HOL/HOLCF/LowerPD.thy	Tue Jan 04 15:32:56 2011 -0800
    14.3 @@ -116,7 +116,7 @@
    14.4  by intro_classes (fast intro: lower_pd_minimal)
    14.5  
    14.6  lemma inst_lower_pd_pcpo: "\<bottom> = lower_principal (PDUnit compact_bot)"
    14.7 -by (rule lower_pd_minimal [THEN UU_I, symmetric])
    14.8 +by (rule lower_pd_minimal [THEN bottomI, symmetric])
    14.9  
   14.10  
   14.11  subsection {* Monadic unit and plus *}
   14.12 @@ -240,8 +240,8 @@
   14.13  lemma lower_plus_bottom_iff [simp]:
   14.14    "xs \<union>\<flat> ys = \<bottom> \<longleftrightarrow> xs = \<bottom> \<and> ys = \<bottom>"
   14.15  apply safe
   14.16 -apply (rule UU_I, erule subst, rule lower_plus_below1)
   14.17 -apply (rule UU_I, erule subst, rule lower_plus_below2)
   14.18 +apply (rule bottomI, erule subst, rule lower_plus_below1)
   14.19 +apply (rule bottomI, erule subst, rule lower_plus_below2)
   14.20  apply (rule lower_plus_absorb)
   14.21  done
   14.22  
    15.1 --- a/src/HOL/HOLCF/Pcpo.thy	Tue Jan 04 15:03:27 2011 -0800
    15.2 +++ b/src/HOL/HOLCF/Pcpo.thy	Tue Jan 04 15:32:56 2011 -0800
    15.3 @@ -180,17 +180,17 @@
    15.4  
    15.5  text {* useful lemmas about @{term \<bottom>} *}
    15.6  
    15.7 -lemma below_UU_iff [simp]: "(x \<sqsubseteq> \<bottom>) = (x = \<bottom>)"
    15.8 +lemma below_bottom_iff [simp]: "(x \<sqsubseteq> \<bottom>) = (x = \<bottom>)"
    15.9  by (simp add: po_eq_conv)
   15.10  
   15.11 -lemma eq_UU_iff: "(x = \<bottom>) = (x \<sqsubseteq> \<bottom>)"
   15.12 +lemma eq_bottom_iff: "(x = \<bottom>) = (x \<sqsubseteq> \<bottom>)"
   15.13  by simp
   15.14  
   15.15 -lemma UU_I: "x \<sqsubseteq> \<bottom> \<Longrightarrow> x = \<bottom>"
   15.16 -by (subst eq_UU_iff)
   15.17 +lemma bottomI: "x \<sqsubseteq> \<bottom> \<Longrightarrow> x = \<bottom>"
   15.18 +by (subst eq_bottom_iff)
   15.19  
   15.20  lemma lub_eq_bottom_iff: "chain Y \<Longrightarrow> (\<Squnion>i. Y i) = \<bottom> \<longleftrightarrow> (\<forall>i. Y i = \<bottom>)"
   15.21 -by (simp only: eq_UU_iff lub_below_iff)
   15.22 +by (simp only: eq_bottom_iff lub_below_iff)
   15.23  
   15.24  lemma chain_UU_I: "\<lbrakk>chain Y; (\<Squnion>i. Y i) = \<bottom>\<rbrakk> \<Longrightarrow> \<forall>i. Y i = \<bottom>"
   15.25  by (simp add: lub_eq_bottom_iff)
   15.26 @@ -202,7 +202,7 @@
   15.27    by (blast intro: chain_UU_I_inverse)
   15.28  
   15.29  lemma notUU_I: "\<lbrakk>x \<sqsubseteq> y; x \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> y \<noteq> \<bottom>"
   15.30 -  by (blast intro: UU_I)
   15.31 +  by (blast intro: bottomI)
   15.32  
   15.33  end
   15.34  
    16.1 --- a/src/HOL/HOLCF/Product_Cpo.thy	Tue Jan 04 15:03:27 2011 -0800
    16.2 +++ b/src/HOL/HOLCF/Product_Cpo.thy	Tue Jan 04 15:32:56 2011 -0800
    16.3 @@ -155,7 +155,7 @@
    16.4  by intro_classes (fast intro: minimal_prod)
    16.5  
    16.6  lemma inst_prod_pcpo: "\<bottom> = (\<bottom>, \<bottom>)"
    16.7 -by (rule minimal_prod [THEN UU_I, symmetric])
    16.8 +by (rule minimal_prod [THEN bottomI, symmetric])
    16.9  
   16.10  lemma Pair_bottom_iff [simp]: "(x, y) = \<bottom> \<longleftrightarrow> x = \<bottom> \<and> y = \<bottom>"
   16.11  unfolding inst_prod_pcpo by simp
    17.1 --- a/src/HOL/HOLCF/Sprod.thy	Tue Jan 04 15:03:27 2011 -0800
    17.2 +++ b/src/HOL/HOLCF/Sprod.thy	Tue Jan 04 15:32:56 2011 -0800
    17.3 @@ -117,7 +117,7 @@
    17.4    "\<lbrakk>x \<noteq> \<bottom>; y \<noteq> \<bottom>; (:x, y:) = (:a, b:)\<rbrakk> \<Longrightarrow> x = a \<and> y = b"
    17.5  by (rule spair_eq [THEN iffD1])
    17.6  
    17.7 -lemma inst_sprod_pcpo2: "UU = (:UU,UU:)"
    17.8 +lemma inst_sprod_pcpo2: "\<bottom> = (:\<bottom>, \<bottom>:)"
    17.9  by simp
   17.10  
   17.11  lemma sprodE2: "(\<And>x y. p = (:x, y:) \<Longrightarrow> Q) \<Longrightarrow> Q"
    18.1 --- a/src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML	Tue Jan 04 15:03:27 2011 -0800
    18.2 +++ b/src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML	Tue Jan 04 15:32:56 2011 -0800
    18.3 @@ -325,7 +325,7 @@
    18.4            @{thms adm_conj adm_subst [OF _ adm_deflation]
    18.5                   cont2cont_fst cont2cont_snd cont_id}
    18.6          val bottom_rules =
    18.7 -          @{thms fst_strict snd_strict deflation_UU simp_thms}
    18.8 +          @{thms fst_strict snd_strict deflation_bottom simp_thms}
    18.9          val tuple_rules =
   18.10            @{thms split_def fst_conv snd_conv}
   18.11          val deflation_rules =
    19.1 --- a/src/HOL/HOLCF/Tools/Domain/domain_take_proofs.ML	Tue Jan 04 15:03:27 2011 -0800
    19.2 +++ b/src/HOL/HOLCF/Tools/Domain/domain_take_proofs.ML	Tue Jan 04 15:32:56 2011 -0800
    19.3 @@ -330,7 +330,7 @@
    19.4            @{thms adm_conj adm_subst [OF _ adm_deflation]
    19.5                   cont2cont_fst cont2cont_snd cont_id}
    19.6          val bottom_rules =
    19.7 -          take_0_thms @ @{thms deflation_UU simp_thms}
    19.8 +          take_0_thms @ @{thms deflation_bottom simp_thms}
    19.9          val deflation_rules =
   19.10            @{thms conjI deflation_ID}
   19.11            @ deflation_abs_rep_thms
    20.1 --- a/src/HOL/HOLCF/Universal.thy	Tue Jan 04 15:03:27 2011 -0800
    20.2 +++ b/src/HOL/HOLCF/Universal.thy	Tue Jan 04 15:32:56 2011 -0800
    20.3 @@ -242,7 +242,7 @@
    20.4  by intro_classes (fast intro: udom_minimal)
    20.5  
    20.6  lemma inst_udom_pcpo: "\<bottom> = udom_principal 0"
    20.7 -by (rule udom_minimal [THEN UU_I, symmetric])
    20.8 +by (rule udom_minimal [THEN bottomI, symmetric])
    20.9  
   20.10  
   20.11  subsection {* Compact bases of domains *}
    21.1 --- a/src/HOL/HOLCF/Up.thy	Tue Jan 04 15:03:27 2011 -0800
    21.2 +++ b/src/HOL/HOLCF/Up.thy	Tue Jan 04 15:32:56 2011 -0800
    21.3 @@ -127,7 +127,7 @@
    21.4  
    21.5  text {* for compatibility with old HOLCF-Version *}
    21.6  lemma inst_up_pcpo: "\<bottom> = Ibottom"
    21.7 -by (rule minimal_up [THEN UU_I, symmetric])
    21.8 +by (rule minimal_up [THEN bottomI, symmetric])
    21.9  
   21.10  subsection {* Continuity of \emph{Iup} and \emph{Ifup} *}
   21.11  
    22.1 --- a/src/HOL/HOLCF/UpperPD.thy	Tue Jan 04 15:03:27 2011 -0800
    22.2 +++ b/src/HOL/HOLCF/UpperPD.thy	Tue Jan 04 15:32:56 2011 -0800
    22.3 @@ -114,7 +114,7 @@
    22.4  by intro_classes (fast intro: upper_pd_minimal)
    22.5  
    22.6  lemma inst_upper_pd_pcpo: "\<bottom> = upper_principal (PDUnit compact_bot)"
    22.7 -by (rule upper_pd_minimal [THEN UU_I, symmetric])
    22.8 +by (rule upper_pd_minimal [THEN bottomI, symmetric])
    22.9  
   22.10  
   22.11  subsection {* Monadic unit and plus *}
   22.12 @@ -233,10 +233,10 @@
   22.13  by (simp add: inst_upper_pd_pcpo)
   22.14  
   22.15  lemma upper_plus_strict1 [simp]: "\<bottom> \<union>\<sharp> ys = \<bottom>"
   22.16 -by (rule UU_I, rule upper_plus_below1)
   22.17 +by (rule bottomI, rule upper_plus_below1)
   22.18  
   22.19  lemma upper_plus_strict2 [simp]: "xs \<union>\<sharp> \<bottom> = \<bottom>"
   22.20 -by (rule UU_I, rule upper_plus_below2)
   22.21 +by (rule bottomI, rule upper_plus_below2)
   22.22  
   22.23  lemma upper_unit_bottom_iff [simp]: "{x}\<sharp> = \<bottom> \<longleftrightarrow> x = \<bottom>"
   22.24  unfolding upper_unit_strict [symmetric] by (rule upper_unit_eq_iff)