# HG changeset patch
# User huffman
# Date 1286200717 25200
# Node ID 0b8e19f588a472701183a1322b95286ecb55874a
# Parent  d841744718fec1775f7f582a9077a3376ebfb0e0
new lemmas about lub

diff -r d841744718fe -r 0b8e19f588a4 src/HOLCF/Adm.thy
--- 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])
 
diff -r d841744718fe -r 0b8e19f588a4 src/HOLCF/Pcpo.thy
--- 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)"
diff -r d841744718fe -r 0b8e19f588a4 src/HOLCF/Porder.thy
--- 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"