--- a/src/HOL/HOLCF/FOCUS/Fstreams.thy Tue Jan 04 15:32:56 2011 -0800
+++ b/src/HOL/HOLCF/FOCUS/Fstreams.thy Tue Jan 04 15:46:38 2011 -0800
@@ -233,7 +233,7 @@
lemma fstreams_lub_lemma1: "[| chain Y; (LUB i. Y i) = <a> ooo s |] ==> EX j t. Y j = <a> ooo t"
apply (subgoal_tac "(LUB i. Y i) ~= UU")
-apply (drule chain_UU_I_inverse2, auto)
+apply (frule lub_eq_bottom_iff, auto)
apply (drule_tac x="i" in is_ub_thelub, auto)
by (drule fstreams_prefix' [THEN iffD1], auto)
@@ -267,7 +267,7 @@
"[| chain Y; (LUB i. Y i) = ((a::'a::flat), b); a ~= UU; b ~= UU |]
==> EX j c d. Y j = (c, d) & c ~= UU & d ~= UU"
apply (frule lub_prod, clarsimp)
-apply (drule chain_UU_I_inverse2, clarsimp)
+apply (clarsimp simp add: lub_eq_bottom_iff [where Y="\<lambda>i. fst (Y i)"])
apply (case_tac "Y i", clarsimp)
apply (case_tac "max_in_chain i Y")
apply (drule maxinch_is_thelub, auto)
--- a/src/HOL/HOLCF/Pcpo.thy Tue Jan 04 15:32:56 2011 -0800
+++ b/src/HOL/HOLCF/Pcpo.thy Tue Jan 04 15:46:38 2011 -0800
@@ -175,9 +175,6 @@
simproc_setup reorient_bottom ("\<bottom> = x") = Reorient_Proc.proc
-context pcpo
-begin
-
text {* useful lemmas about @{term \<bottom>} *}
lemma below_bottom_iff [simp]: "(x \<sqsubseteq> \<bottom>) = (x = \<bottom>)"
@@ -192,20 +189,6 @@
lemma lub_eq_bottom_iff: "chain Y \<Longrightarrow> (\<Squnion>i. Y i) = \<bottom> \<longleftrightarrow> (\<forall>i. Y i = \<bottom>)"
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)
-
-lemma chain_UU_I_inverse: "\<forall>i::nat. Y i = \<bottom> \<Longrightarrow> (\<Squnion>i. Y i) = \<bottom>"
-by simp
-
-lemma chain_UU_I_inverse2: "(\<Squnion>i. Y i) \<noteq> \<bottom> \<Longrightarrow> \<exists>i::nat. Y i \<noteq> \<bottom>"
- 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: bottomI)
-
-end
-
subsection {* Chain-finite and flat cpos *}
text {* further useful classes for HOLCF domains *}