new lemmas about lub
authorhuffman
Mon Oct 04 06:58:37 2010 -0700 (2010-10-04)
changeset 399690b8e19f588a4
parent 39968 d841744718fe
child 39970 9023b897e67a
new lemmas about lub
src/HOLCF/Adm.thy
src/HOLCF/Pcpo.thy
src/HOLCF/Porder.thy
     1.1 --- a/src/HOLCF/Adm.thy	Mon Oct 04 06:45:57 2010 -0700
     1.2 +++ b/src/HOLCF/Adm.thy	Mon Oct 04 06:58:37 2010 -0700
     1.3 @@ -171,6 +171,10 @@
     1.4    "\<lbrakk>compact x; chain Y; x \<sqsubseteq> (\<Squnion>i. Y i)\<rbrakk> \<Longrightarrow> \<exists>i. x \<sqsubseteq> Y i"
     1.5  unfolding compact_def adm_def by fast
     1.6  
     1.7 +lemma compact_below_lub_iff:
     1.8 +  "\<lbrakk>compact x; chain Y\<rbrakk> \<Longrightarrow> x \<sqsubseteq> (\<Squnion>i. Y i) \<longleftrightarrow> (\<exists>i. x \<sqsubseteq> Y i)"
     1.9 +by (fast intro: compactD2 elim: below_trans is_ub_thelub)
    1.10 +
    1.11  lemma compact_chfin [simp]: "compact (x::'a::chfin)"
    1.12  by (rule compactI [OF adm_chfin])
    1.13  
     2.1 --- a/src/HOLCF/Pcpo.thy	Mon Oct 04 06:45:57 2010 -0700
     2.2 +++ b/src/HOLCF/Pcpo.thy	Mon Oct 04 06:58:37 2010 -0700
     2.3 @@ -33,6 +33,9 @@
     2.4    "\<lbrakk>chain S; range S <| x\<rbrakk> \<Longrightarrow> (\<Squnion>i. S i) \<sqsubseteq> x"
     2.5    by (blast dest: cpo intro: lubI [THEN is_lub_lub])
     2.6  
     2.7 +lemma lub_below_iff: "chain S \<Longrightarrow> (\<Squnion>i. S i) \<sqsubseteq> x \<longleftrightarrow> (\<forall>i. S i \<sqsubseteq> x)"
     2.8 +  by (simp add: is_lub_below_iff [OF cpo_lubI] is_ub_def)
     2.9 +
    2.10  lemma lub_range_mono:
    2.11    "\<lbrakk>range X \<subseteq> range Y; chain Y; chain X\<rbrakk>
    2.12      \<Longrightarrow> (\<Squnion>i. X i) \<sqsubseteq> (\<Squnion>i. Y i)"
     3.1 --- a/src/HOLCF/Porder.thy	Mon Oct 04 06:45:57 2010 -0700
     3.2 +++ b/src/HOLCF/Porder.thy	Mon Oct 04 06:58:37 2010 -0700
     3.3 @@ -139,6 +139,9 @@
     3.4  lemma is_lubI: "\<lbrakk>S <| x; \<And>u. S <| u \<Longrightarrow> x \<sqsubseteq> u\<rbrakk> \<Longrightarrow> S <<| x"
     3.5    unfolding is_lub_def by fast
     3.6  
     3.7 +lemma is_lub_below_iff: "S <<| x \<Longrightarrow> x \<sqsubseteq> u \<longleftrightarrow> S <| u"
     3.8 +  unfolding is_lub_def is_ub_def by (metis below_trans)
     3.9 +
    3.10  text {* lubs are unique *}
    3.11  
    3.12  lemma unique_lub: "\<lbrakk>S <<| x; S <<| y\<rbrakk> \<Longrightarrow> x = y"