--- a/NEWS Tue Jan 04 15:03:27 2011 -0800
+++ b/NEWS Tue Jan 04 15:32:56 2011 -0800
@@ -599,6 +599,10 @@
thelub_cprod ~> lub_prod
minimal_cprod ~> minimal_prod
inst_cprod_pcpo ~> inst_prod_pcpo
+ UU_I ~> bottomI
+ compact_UU ~> compact_bottom
+ deflation_UU ~> deflation_bottom
+ finite_deflation_UU ~> finite_deflation_bottom
* Many legacy theorem names have been discontinued. INCOMPATIBILITY.
sq_ord_less_eq_trans ~> below_eq_trans
--- a/src/HOL/HOLCF/Adm.thy Tue Jan 04 15:03:27 2011 -0800
+++ b/src/HOL/HOLCF/Adm.thy Tue Jan 04 15:32:56 2011 -0800
@@ -175,7 +175,7 @@
"\<lbrakk>compact k; cont (\<lambda>x. t x)\<rbrakk> \<Longrightarrow> adm (\<lambda>x. k \<noteq> t x)"
by (simp add: po_eq_conv)
-lemma compact_UU [simp, intro]: "compact \<bottom>"
+lemma compact_bottom [simp, intro]: "compact \<bottom>"
by (rule compactI, simp)
text {* Any upward-closed predicate is admissible. *}
--- a/src/HOL/HOLCF/Algebraic.thy Tue Jan 04 15:03:27 2011 -0800
+++ b/src/HOL/HOLCF/Algebraic.thy Tue Jan 04 15:32:56 2011 -0800
@@ -13,7 +13,7 @@
subsection {* Type constructor for finite deflations *}
typedef (open) 'a fin_defl = "{d::'a \<rightarrow> 'a. finite_deflation d}"
-by (fast intro: finite_deflation_UU)
+by (fast intro: finite_deflation_bottom)
instantiation fin_defl :: (bifinite) below
begin
@@ -138,14 +138,14 @@
apply (induct x rule: defl.principal_induct, simp)
apply (rule defl.principal_mono)
apply (simp add: below_fin_defl_def)
-apply (simp add: Abs_fin_defl_inverse finite_deflation_UU)
+apply (simp add: Abs_fin_defl_inverse finite_deflation_bottom)
done
instance defl :: (bifinite) pcpo
by intro_classes (fast intro: defl_minimal)
lemma inst_defl_pcpo: "\<bottom> = defl_principal (Abs_fin_defl \<bottom>)"
-by (rule defl_minimal [THEN UU_I, symmetric])
+by (rule defl_minimal [THEN bottomI, symmetric])
subsection {* Applying algebraic deflations *}
@@ -209,11 +209,11 @@
apply (subst inst_defl_pcpo)
apply (subst cast_defl_principal)
apply (rule Abs_fin_defl_inverse)
-apply (simp add: finite_deflation_UU)
+apply (simp add: finite_deflation_bottom)
done
lemma cast_strict2 [simp]: "cast\<cdot>A\<cdot>\<bottom> = \<bottom>"
-by (rule cast.below [THEN UU_I])
+by (rule cast.below [THEN bottomI])
subsection {* Deflation combinators *}
--- a/src/HOL/HOLCF/Bifinite.thy Tue Jan 04 15:03:27 2011 -0800
+++ b/src/HOL/HOLCF/Bifinite.thy Tue Jan 04 15:32:56 2011 -0800
@@ -253,7 +253,7 @@
qed
lemma approx_chain_unit: "approx_chain (\<bottom> :: nat \<Rightarrow> unit \<rightarrow> unit)"
-by (simp add: approx_chain_def cfun_eq_iff finite_deflation_UU)
+by (simp add: approx_chain_def cfun_eq_iff finite_deflation_bottom)
instance unit :: bifinite
by default (fast intro!: approx_chain_unit)
--- a/src/HOL/HOLCF/Cfun.thy Tue Jan 04 15:03:27 2011 -0800
+++ b/src/HOL/HOLCF/Cfun.thy Tue Jan 04 15:32:56 2011 -0800
@@ -92,20 +92,20 @@
subsection {* Continuous function space is pointed *}
-lemma UU_cfun: "\<bottom> \<in> cfun"
+lemma bottom_cfun: "\<bottom> \<in> cfun"
by (simp add: cfun_def inst_fun_pcpo)
instance cfun :: (cpo, discrete_cpo) discrete_cpo
by intro_classes (simp add: below_cfun_def Rep_cfun_inject)
instance cfun :: (cpo, pcpo) pcpo
-by (rule typedef_pcpo [OF type_definition_cfun below_cfun_def UU_cfun])
+by (rule typedef_pcpo [OF type_definition_cfun below_cfun_def bottom_cfun])
lemmas Rep_cfun_strict =
- typedef_Rep_strict [OF type_definition_cfun below_cfun_def UU_cfun]
+ typedef_Rep_strict [OF type_definition_cfun below_cfun_def bottom_cfun]
lemmas Abs_cfun_strict =
- typedef_Abs_strict [OF type_definition_cfun below_cfun_def UU_cfun]
+ typedef_Abs_strict [OF type_definition_cfun below_cfun_def bottom_cfun]
text {* function application is strict in its first argument *}
@@ -261,7 +261,7 @@
text {* strictness *}
lemma strictI: "f\<cdot>x = \<bottom> \<Longrightarrow> f\<cdot>\<bottom> = \<bottom>"
-apply (rule UU_I)
+apply (rule bottomI)
apply (erule subst)
apply (rule minimal [THEN monofun_cfun_arg])
done
@@ -364,7 +364,7 @@
lemma retraction_strict:
"\<forall>x. f\<cdot>(g\<cdot>x) = x \<Longrightarrow> f\<cdot>\<bottom> = \<bottom>"
-apply (rule UU_I)
+apply (rule bottomI)
apply (drule_tac x="\<bottom>" in spec)
apply (erule subst)
apply (rule monofun_cfun_arg)
@@ -406,7 +406,7 @@
"f\<cdot>x = (c::'b::flat) \<Longrightarrow> f\<cdot>\<bottom> = \<bottom> \<or> (\<forall>z. f\<cdot>z = c)"
apply (case_tac "f\<cdot>x = \<bottom>")
apply (rule disjI1)
-apply (rule UU_I)
+apply (rule bottomI)
apply (erule_tac t="\<bottom>" in subst)
apply (rule minimal [THEN monofun_cfun_arg])
apply clarify
--- a/src/HOL/HOLCF/ConvexPD.thy Tue Jan 04 15:03:27 2011 -0800
+++ b/src/HOL/HOLCF/ConvexPD.thy Tue Jan 04 15:32:56 2011 -0800
@@ -161,7 +161,7 @@
by intro_classes (fast intro: convex_pd_minimal)
lemma inst_convex_pd_pcpo: "\<bottom> = convex_principal (PDUnit compact_bot)"
-by (rule convex_pd_minimal [THEN UU_I, symmetric])
+by (rule convex_pd_minimal [THEN bottomI, symmetric])
subsection {* Monadic unit and plus *}
--- a/src/HOL/HOLCF/Cpodef.thy Tue Jan 04 15:03:27 2011 -0800
+++ b/src/HOL/HOLCF/Cpodef.thy Tue Jan 04 15:32:56 2011 -0800
@@ -203,9 +203,9 @@
fixes Abs :: "'a::pcpo \<Rightarrow> 'b::cpo"
assumes type: "type_definition Rep Abs A"
and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
- and UU_in_A: "\<bottom> \<in> A"
+ and bottom_in_A: "\<bottom> \<in> A"
shows "OFCLASS('b, pcpo_class)"
-by (rule typedef_pcpo_generic [OF type below UU_in_A], rule minimal)
+by (rule typedef_pcpo_generic [OF type below bottom_in_A], rule minimal)
subsubsection {* Strictness of \emph{Rep} and \emph{Abs} *}
@@ -217,36 +217,36 @@
theorem typedef_Abs_strict:
assumes type: "type_definition Rep Abs A"
and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
- and UU_in_A: "\<bottom> \<in> A"
+ and bottom_in_A: "\<bottom> \<in> A"
shows "Abs \<bottom> = \<bottom>"
- apply (rule UU_I, unfold below)
- apply (simp add: type_definition.Abs_inverse [OF type UU_in_A])
+ apply (rule bottomI, unfold below)
+ apply (simp add: type_definition.Abs_inverse [OF type bottom_in_A])
done
theorem typedef_Rep_strict:
assumes type: "type_definition Rep Abs A"
and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
- and UU_in_A: "\<bottom> \<in> A"
+ and bottom_in_A: "\<bottom> \<in> A"
shows "Rep \<bottom> = \<bottom>"
- apply (rule typedef_Abs_strict [OF type below UU_in_A, THEN subst])
- apply (rule type_definition.Abs_inverse [OF type UU_in_A])
+ apply (rule typedef_Abs_strict [OF type below bottom_in_A, THEN subst])
+ apply (rule type_definition.Abs_inverse [OF type bottom_in_A])
done
theorem typedef_Abs_bottom_iff:
assumes type: "type_definition Rep Abs A"
and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
- and UU_in_A: "\<bottom> \<in> A"
+ and bottom_in_A: "\<bottom> \<in> A"
shows "x \<in> A \<Longrightarrow> (Abs x = \<bottom>) = (x = \<bottom>)"
- apply (rule typedef_Abs_strict [OF type below UU_in_A, THEN subst])
- apply (simp add: type_definition.Abs_inject [OF type] UU_in_A)
+ apply (rule typedef_Abs_strict [OF type below bottom_in_A, THEN subst])
+ apply (simp add: type_definition.Abs_inject [OF type] bottom_in_A)
done
theorem typedef_Rep_bottom_iff:
assumes type: "type_definition Rep Abs A"
and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
- and UU_in_A: "\<bottom> \<in> A"
+ and bottom_in_A: "\<bottom> \<in> A"
shows "(Rep x = \<bottom>) = (x = \<bottom>)"
- apply (rule typedef_Rep_strict [OF type below UU_in_A, THEN subst])
+ apply (rule typedef_Rep_strict [OF type below bottom_in_A, THEN subst])
apply (simp add: type_definition.Rep_inject [OF type])
done
@@ -256,12 +256,12 @@
fixes Abs :: "'a::flat \<Rightarrow> 'b::pcpo"
assumes type: "type_definition Rep Abs A"
and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
- and UU_in_A: "\<bottom> \<in> A"
+ and bottom_in_A: "\<bottom> \<in> A"
shows "OFCLASS('b, flat_class)"
apply (intro_classes)
apply (unfold below)
apply (simp add: type_definition.Rep_inject [OF type, symmetric])
- apply (simp add: typedef_Rep_strict [OF type below UU_in_A])
+ apply (simp add: typedef_Rep_strict [OF type below bottom_in_A])
apply (simp add: ax_flat)
done
--- a/src/HOL/HOLCF/Deflation.thy Tue Jan 04 15:03:27 2011 -0800
+++ b/src/HOL/HOLCF/Deflation.thy Tue Jan 04 15:32:56 2011 -0800
@@ -56,7 +56,7 @@
end
lemma deflation_strict: "deflation d \<Longrightarrow> d\<cdot>\<bottom> = \<bottom>"
-by (rule deflation.below [THEN UU_I])
+by (rule deflation.below [THEN bottomI])
lemma adm_deflation: "adm (\<lambda>d. deflation d)"
by (simp add: deflation_def)
@@ -64,7 +64,7 @@
lemma deflation_ID: "deflation ID"
by (simp add: deflation.intro)
-lemma deflation_UU: "deflation \<bottom>"
+lemma deflation_bottom: "deflation \<bottom>"
by (simp add: deflation.intro)
lemma deflation_below_iff:
@@ -160,7 +160,7 @@
"finite_deflation d \<Longrightarrow> deflation d"
unfolding finite_deflation_def by simp
-lemma finite_deflation_UU: "finite_deflation \<bottom>"
+lemma finite_deflation_bottom: "finite_deflation \<bottom>"
by default simp_all
--- a/src/HOL/HOLCF/Domain_Aux.thy Tue Jan 04 15:03:27 2011 -0800
+++ b/src/HOL/HOLCF/Domain_Aux.thy Tue Jan 04 15:32:56 2011 -0800
@@ -52,7 +52,7 @@
have "\<bottom> \<sqsubseteq> rep\<cdot>\<bottom>" ..
then have "abs\<cdot>\<bottom> \<sqsubseteq> abs\<cdot>(rep\<cdot>\<bottom>)" by (rule monofun_cfun_arg)
then have "abs\<cdot>\<bottom> \<sqsubseteq> \<bottom>" by simp
- then show ?thesis by (rule UU_I)
+ then show ?thesis by (rule bottomI)
qed
lemma rep_strict: "rep\<cdot>\<bottom> = \<bottom>"
--- a/src/HOL/HOLCF/Fix.thy Tue Jan 04 15:03:27 2011 -0800
+++ b/src/HOL/HOLCF/Fix.thy Tue Jan 04 15:32:56 2011 -0800
@@ -122,7 +122,7 @@
apply (rule iffI)
apply (erule subst)
apply (rule fix_eq [symmetric])
-apply (erule fix_least [THEN UU_I])
+apply (erule fix_least [THEN bottomI])
done
lemma fix_strict: "F\<cdot>\<bottom> = \<bottom> \<Longrightarrow> fix\<cdot>F = \<bottom>"
--- a/src/HOL/HOLCF/Fun_Cpo.thy Tue Jan 04 15:03:27 2011 -0800
+++ b/src/HOL/HOLCF/Fun_Cpo.thy Tue Jan 04 15:32:56 2011 -0800
@@ -96,13 +96,13 @@
by default (fast intro: minimal_fun)
lemma inst_fun_pcpo: "\<bottom> = (\<lambda>x. \<bottom>)"
-by (rule minimal_fun [THEN UU_I, symmetric])
+by (rule minimal_fun [THEN bottomI, symmetric])
lemma app_strict [simp]: "\<bottom> x = \<bottom>"
by (simp add: inst_fun_pcpo)
lemma lambda_strict: "(\<lambda>x. \<bottom>) = \<bottom>"
-by (rule UU_I, rule minimal_fun)
+by (rule bottomI, rule minimal_fun)
subsection {* Propagation of monotonicity and continuity *}
--- a/src/HOL/HOLCF/HOLCF.thy Tue Jan 04 15:03:27 2011 -0800
+++ b/src/HOL/HOLCF/HOLCF.thy Tue Jan 04 15:32:56 2011 -0800
@@ -35,5 +35,12 @@
lemmas contlub_cfun = lub_APP [symmetric]
lemmas contlub_LAM = lub_LAM [symmetric]
lemmas thelubI = lub_eqI
+lemmas UU_I = bottomI
+lemmas lift_distinct1 = lift.distinct(1)
+lemmas lift_distinct2 = lift.distinct(2)
+lemmas Def_not_UU = lift.distinct(2)
+lemmas Def_inject = lift.inject
+lemmas below_UU_iff = below_bottom_iff
+lemmas eq_UU_iff = eq_bottom_iff
end
--- a/src/HOL/HOLCF/Lift.thy Tue Jan 04 15:03:27 2011 -0800
+++ b/src/HOL/HOLCF/Lift.thy Tue Jan 04 15:32:56 2011 -0800
@@ -32,13 +32,7 @@
rep_datatype "\<bottom>\<Colon>'a lift" Def
by (erule lift_induct) (simp_all add: Def_def Abs_lift_inject inst_lift_pcpo)
-lemmas lift_distinct1 = lift.distinct(1)
-lemmas lift_distinct2 = lift.distinct(2)
-lemmas Def_not_UU = lift.distinct(2)
-lemmas Def_inject = lift.inject
-
-
-text {* @{term UU} and @{term Def} *}
+text {* @{term bottom} and @{term Def} *}
lemma not_Undef_is_Def: "(x \<noteq> \<bottom>) = (\<exists>y. x = Def y)"
by (cases x) simp_all
@@ -47,7 +41,7 @@
by (cases x) simp_all
text {*
- For @{term "x ~= UU"} in assumptions @{text defined} replaces @{text
+ For @{term "x ~= \<bottom>"} in assumptions @{text defined} replaces @{text
x} by @{text "Def a"} in conclusion. *}
method_setup defined = {*
--- a/src/HOL/HOLCF/LowerPD.thy Tue Jan 04 15:03:27 2011 -0800
+++ b/src/HOL/HOLCF/LowerPD.thy Tue Jan 04 15:32:56 2011 -0800
@@ -116,7 +116,7 @@
by intro_classes (fast intro: lower_pd_minimal)
lemma inst_lower_pd_pcpo: "\<bottom> = lower_principal (PDUnit compact_bot)"
-by (rule lower_pd_minimal [THEN UU_I, symmetric])
+by (rule lower_pd_minimal [THEN bottomI, symmetric])
subsection {* Monadic unit and plus *}
@@ -240,8 +240,8 @@
lemma lower_plus_bottom_iff [simp]:
"xs \<union>\<flat> ys = \<bottom> \<longleftrightarrow> xs = \<bottom> \<and> ys = \<bottom>"
apply safe
-apply (rule UU_I, erule subst, rule lower_plus_below1)
-apply (rule UU_I, erule subst, rule lower_plus_below2)
+apply (rule bottomI, erule subst, rule lower_plus_below1)
+apply (rule bottomI, erule subst, rule lower_plus_below2)
apply (rule lower_plus_absorb)
done
--- a/src/HOL/HOLCF/Pcpo.thy Tue Jan 04 15:03:27 2011 -0800
+++ b/src/HOL/HOLCF/Pcpo.thy Tue Jan 04 15:32:56 2011 -0800
@@ -180,17 +180,17 @@
text {* useful lemmas about @{term \<bottom>} *}
-lemma below_UU_iff [simp]: "(x \<sqsubseteq> \<bottom>) = (x = \<bottom>)"
+lemma below_bottom_iff [simp]: "(x \<sqsubseteq> \<bottom>) = (x = \<bottom>)"
by (simp add: po_eq_conv)
-lemma eq_UU_iff: "(x = \<bottom>) = (x \<sqsubseteq> \<bottom>)"
+lemma eq_bottom_iff: "(x = \<bottom>) = (x \<sqsubseteq> \<bottom>)"
by simp
-lemma UU_I: "x \<sqsubseteq> \<bottom> \<Longrightarrow> x = \<bottom>"
-by (subst eq_UU_iff)
+lemma bottomI: "x \<sqsubseteq> \<bottom> \<Longrightarrow> x = \<bottom>"
+by (subst eq_bottom_iff)
lemma lub_eq_bottom_iff: "chain Y \<Longrightarrow> (\<Squnion>i. Y i) = \<bottom> \<longleftrightarrow> (\<forall>i. Y i = \<bottom>)"
-by (simp only: eq_UU_iff lub_below_iff)
+by (simp only: eq_bottom_iff lub_below_iff)
lemma chain_UU_I: "\<lbrakk>chain Y; (\<Squnion>i. Y i) = \<bottom>\<rbrakk> \<Longrightarrow> \<forall>i. Y i = \<bottom>"
by (simp add: lub_eq_bottom_iff)
@@ -202,7 +202,7 @@
by (blast intro: chain_UU_I_inverse)
lemma notUU_I: "\<lbrakk>x \<sqsubseteq> y; x \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> y \<noteq> \<bottom>"
- by (blast intro: UU_I)
+ by (blast intro: bottomI)
end
--- a/src/HOL/HOLCF/Product_Cpo.thy Tue Jan 04 15:03:27 2011 -0800
+++ b/src/HOL/HOLCF/Product_Cpo.thy Tue Jan 04 15:32:56 2011 -0800
@@ -155,7 +155,7 @@
by intro_classes (fast intro: minimal_prod)
lemma inst_prod_pcpo: "\<bottom> = (\<bottom>, \<bottom>)"
-by (rule minimal_prod [THEN UU_I, symmetric])
+by (rule minimal_prod [THEN bottomI, symmetric])
lemma Pair_bottom_iff [simp]: "(x, y) = \<bottom> \<longleftrightarrow> x = \<bottom> \<and> y = \<bottom>"
unfolding inst_prod_pcpo by simp
--- a/src/HOL/HOLCF/Sprod.thy Tue Jan 04 15:03:27 2011 -0800
+++ b/src/HOL/HOLCF/Sprod.thy Tue Jan 04 15:32:56 2011 -0800
@@ -117,7 +117,7 @@
"\<lbrakk>x \<noteq> \<bottom>; y \<noteq> \<bottom>; (:x, y:) = (:a, b:)\<rbrakk> \<Longrightarrow> x = a \<and> y = b"
by (rule spair_eq [THEN iffD1])
-lemma inst_sprod_pcpo2: "UU = (:UU,UU:)"
+lemma inst_sprod_pcpo2: "\<bottom> = (:\<bottom>, \<bottom>:)"
by simp
lemma sprodE2: "(\<And>x y. p = (:x, y:) \<Longrightarrow> Q) \<Longrightarrow> Q"
--- a/src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML Tue Jan 04 15:03:27 2011 -0800
+++ b/src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML Tue Jan 04 15:32:56 2011 -0800
@@ -325,7 +325,7 @@
@{thms adm_conj adm_subst [OF _ adm_deflation]
cont2cont_fst cont2cont_snd cont_id}
val bottom_rules =
- @{thms fst_strict snd_strict deflation_UU simp_thms}
+ @{thms fst_strict snd_strict deflation_bottom simp_thms}
val tuple_rules =
@{thms split_def fst_conv snd_conv}
val deflation_rules =
--- a/src/HOL/HOLCF/Tools/Domain/domain_take_proofs.ML Tue Jan 04 15:03:27 2011 -0800
+++ b/src/HOL/HOLCF/Tools/Domain/domain_take_proofs.ML Tue Jan 04 15:32:56 2011 -0800
@@ -330,7 +330,7 @@
@{thms adm_conj adm_subst [OF _ adm_deflation]
cont2cont_fst cont2cont_snd cont_id}
val bottom_rules =
- take_0_thms @ @{thms deflation_UU simp_thms}
+ take_0_thms @ @{thms deflation_bottom simp_thms}
val deflation_rules =
@{thms conjI deflation_ID}
@ deflation_abs_rep_thms
--- a/src/HOL/HOLCF/Universal.thy Tue Jan 04 15:03:27 2011 -0800
+++ b/src/HOL/HOLCF/Universal.thy Tue Jan 04 15:32:56 2011 -0800
@@ -242,7 +242,7 @@
by intro_classes (fast intro: udom_minimal)
lemma inst_udom_pcpo: "\<bottom> = udom_principal 0"
-by (rule udom_minimal [THEN UU_I, symmetric])
+by (rule udom_minimal [THEN bottomI, symmetric])
subsection {* Compact bases of domains *}
--- a/src/HOL/HOLCF/Up.thy Tue Jan 04 15:03:27 2011 -0800
+++ b/src/HOL/HOLCF/Up.thy Tue Jan 04 15:32:56 2011 -0800
@@ -127,7 +127,7 @@
text {* for compatibility with old HOLCF-Version *}
lemma inst_up_pcpo: "\<bottom> = Ibottom"
-by (rule minimal_up [THEN UU_I, symmetric])
+by (rule minimal_up [THEN bottomI, symmetric])
subsection {* Continuity of \emph{Iup} and \emph{Ifup} *}
--- a/src/HOL/HOLCF/UpperPD.thy Tue Jan 04 15:03:27 2011 -0800
+++ b/src/HOL/HOLCF/UpperPD.thy Tue Jan 04 15:32:56 2011 -0800
@@ -114,7 +114,7 @@
by intro_classes (fast intro: upper_pd_minimal)
lemma inst_upper_pd_pcpo: "\<bottom> = upper_principal (PDUnit compact_bot)"
-by (rule upper_pd_minimal [THEN UU_I, symmetric])
+by (rule upper_pd_minimal [THEN bottomI, symmetric])
subsection {* Monadic unit and plus *}
@@ -233,10 +233,10 @@
by (simp add: inst_upper_pd_pcpo)
lemma upper_plus_strict1 [simp]: "\<bottom> \<union>\<sharp> ys = \<bottom>"
-by (rule UU_I, rule upper_plus_below1)
+by (rule bottomI, rule upper_plus_below1)
lemma upper_plus_strict2 [simp]: "xs \<union>\<sharp> \<bottom> = \<bottom>"
-by (rule UU_I, rule upper_plus_below2)
+by (rule bottomI, rule upper_plus_below2)
lemma upper_unit_bottom_iff [simp]: "{x}\<sharp> = \<bottom> \<longleftrightarrow> x = \<bottom>"
unfolding upper_unit_strict [symmetric] by (rule upper_unit_eq_iff)