--- a/src/HOLCF/Pcpo.thy Wed Jan 02 18:23:45 2008 +0100
+++ b/src/HOLCF/Pcpo.thy Wed Jan 02 18:26:01 2008 +0100
@@ -17,20 +17,40 @@
-- {* class axiom: *}
cpo: "chain S \<Longrightarrow> \<exists>x. range S <<| x"
+axclass dcpo < po
+ dcpo: "directed S \<Longrightarrow> \<exists>x. S <<| x"
+
+instance dcpo < cpo
+by (intro_classes, rule dcpo [OF directed_chain])
+
text {* in cpo's everthing equal to THE lub has lub properties for every chain *}
lemma thelubE: "\<lbrakk>chain S; (\<Squnion>i. S i) = (l::'a::cpo)\<rbrakk> \<Longrightarrow> range S <<| l"
by (blast dest: cpo intro: lubI)
+lemma thelubE': "\<lbrakk>directed S; lub S = (l::'a::dcpo)\<rbrakk> \<Longrightarrow> S <<| l"
+by (blast dest: dcpo intro: lubI)
+
text {* Properties of the lub *}
lemma is_ub_thelub: "chain (S::nat \<Rightarrow> 'a::cpo) \<Longrightarrow> S x \<sqsubseteq> (\<Squnion>i. S i)"
by (blast dest: cpo intro: lubI [THEN is_ub_lub])
+lemma is_ub_thelub': "\<lbrakk>directed S; (x::'a::dcpo) \<in> S\<rbrakk> \<Longrightarrow> x \<sqsubseteq> lub S"
+apply (drule thelubE' [OF _ refl])
+apply (drule is_lubD1)
+apply (erule (1) is_ubD)
+done
+
lemma is_lub_thelub:
"\<lbrakk>chain (S::nat \<Rightarrow> 'a::cpo); range S <| x\<rbrakk> \<Longrightarrow> (\<Squnion>i. S i) \<sqsubseteq> x"
by (blast dest: cpo intro: lubI [THEN is_lub_lub])
+lemma is_lub_thelub': "\<lbrakk>directed S; S <| x\<rbrakk> \<Longrightarrow> lub S \<sqsubseteq> (x::'a::dcpo)"
+apply (drule dcpo, clarify, drule lubI)
+apply (erule is_lub_lub, assumption)
+done
+
lemma lub_range_mono:
"\<lbrakk>range X \<subseteq> range Y; chain Y; chain (X::nat \<Rightarrow> 'a::cpo)\<rbrakk>
\<Longrightarrow> (\<Squnion>i. X i) \<sqsubseteq> (\<Squnion>i. Y i)"