--- a/src/HOLCF/Adm.thy Mon Oct 04 06:45:57 2010 -0700
+++ b/src/HOLCF/Adm.thy Mon Oct 04 06:58:37 2010 -0700
@@ -171,6 +171,10 @@
"\<lbrakk>compact x; chain Y; x \<sqsubseteq> (\<Squnion>i. Y i)\<rbrakk> \<Longrightarrow> \<exists>i. x \<sqsubseteq> Y i"
unfolding compact_def adm_def by fast
+lemma compact_below_lub_iff:
+ "\<lbrakk>compact x; chain Y\<rbrakk> \<Longrightarrow> x \<sqsubseteq> (\<Squnion>i. Y i) \<longleftrightarrow> (\<exists>i. x \<sqsubseteq> Y i)"
+by (fast intro: compactD2 elim: below_trans is_ub_thelub)
+
lemma compact_chfin [simp]: "compact (x::'a::chfin)"
by (rule compactI [OF adm_chfin])
--- a/src/HOLCF/Pcpo.thy Mon Oct 04 06:45:57 2010 -0700
+++ b/src/HOLCF/Pcpo.thy Mon Oct 04 06:58:37 2010 -0700
@@ -33,6 +33,9 @@
"\<lbrakk>chain S; range S <| x\<rbrakk> \<Longrightarrow> (\<Squnion>i. S i) \<sqsubseteq> x"
by (blast dest: cpo intro: lubI [THEN is_lub_lub])
+lemma lub_below_iff: "chain S \<Longrightarrow> (\<Squnion>i. S i) \<sqsubseteq> x \<longleftrightarrow> (\<forall>i. S i \<sqsubseteq> x)"
+ by (simp add: is_lub_below_iff [OF cpo_lubI] is_ub_def)
+
lemma lub_range_mono:
"\<lbrakk>range X \<subseteq> range Y; chain Y; chain X\<rbrakk>
\<Longrightarrow> (\<Squnion>i. X i) \<sqsubseteq> (\<Squnion>i. Y i)"
--- a/src/HOLCF/Porder.thy Mon Oct 04 06:45:57 2010 -0700
+++ b/src/HOLCF/Porder.thy Mon Oct 04 06:58:37 2010 -0700
@@ -139,6 +139,9 @@
lemma is_lubI: "\<lbrakk>S <| x; \<And>u. S <| u \<Longrightarrow> x \<sqsubseteq> u\<rbrakk> \<Longrightarrow> S <<| x"
unfolding is_lub_def by fast
+lemma is_lub_below_iff: "S <<| x \<Longrightarrow> x \<sqsubseteq> u \<longleftrightarrow> S <| u"
+ unfolding is_lub_def is_ub_def by (metis below_trans)
+
text {* lubs are unique *}
lemma unique_lub: "\<lbrakk>S <<| x; S <<| y\<rbrakk> \<Longrightarrow> x = y"