# HG changeset patch
# User huffman
# Date 1294184798 28800
# Node ID 138f414f14cb69c0bf82170e2c9327a448cc9108
# Parent  1aa23e9f2c872acd2cf801db3adb326119271116
remove various lemmas redundant with lub_eq_bottom_iff

diff -r 1aa23e9f2c87 -r 138f414f14cb src/HOL/HOLCF/FOCUS/Fstreams.thy
--- 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)
diff -r 1aa23e9f2c87 -r 138f414f14cb src/HOL/HOLCF/Pcpo.thy
--- 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 *}