# HG changeset patch
# User huffman
# Date 1199301829 -3600
# Node ID c0506ac5b6b482c999eede6b45a23087558f5608
# Parent  30cbe076459902b9d9da32f15478086907b9470b
add dcpo instance proof

diff -r 30cbe0764599 -r c0506ac5b6b4 src/HOLCF/Up.thy
--- a/src/HOLCF/Up.thy	Wed Jan 02 19:51:29 2008 +0100
+++ b/src/HOLCF/Up.thy	Wed Jan 02 20:23:49 2008 +0100
@@ -86,6 +86,22 @@
 apply simp
 done
 
+lemma is_lub_Iup': "\<lbrakk>directed S; S <<| x\<rbrakk> \<Longrightarrow> (Iup ` S) <<| Iup x"
+apply (rule is_lubI)
+apply (rule ub_imageI)
+apply (subst Iup_less)
+apply (erule (1) is_ubD [OF is_lubD1])
+apply (case_tac u)
+apply (drule directedD1, erule exE)
+apply (drule (1) ub_imageD)
+apply simp
+apply simp
+apply (erule is_lub_lub)
+apply (rule is_ubI)
+apply (drule (1) ub_imageD)
+apply simp
+done
+
 text {* Now some lemmas about chains of @{typ "'a u"} elements *}
 
 lemma up_lemma1: "z \<noteq> Ibottom \<Longrightarrow> Iup (THE a. Iup a = z) = z"
@@ -154,6 +170,55 @@
 instance u :: (cpo) cpo
 by intro_classes (rule cpo_up)
 
+lemma up_directed_lemma:
+  "directed (S::'a::dcpo u set) \<Longrightarrow>
+    (directed (Iup -` S) \<and> S <<| Iup (lub (Iup -` S))) \<or>
+    S = {Ibottom}"
+apply (case_tac "\<exists>x. Iup x \<in> S")
+apply (rule disjI1)
+apply (subgoal_tac "directed (Iup -` S)")
+apply (rule conjI, assumption)
+apply (rule is_lubI)
+apply (rule is_ubI)
+apply (case_tac x, simp, simp)
+apply (erule is_ub_thelub', simp)
+apply (case_tac u)
+apply (erule exE)
+apply (drule (1) is_ubD)
+apply simp
+apply simp
+apply (erule is_lub_thelub')
+apply (rule is_ubI, simp)
+apply (drule (1) is_ubD, simp)
+apply (rule directedI)
+apply (erule exE)
+apply (rule exI)
+apply (erule vimageI2)
+apply simp
+apply (drule_tac x="Iup x" and y="Iup y" in directedD2, assumption+)
+apply (erule bexE, rename_tac z)
+apply (case_tac z)
+apply simp
+apply (rule_tac x=a in bexI)
+apply simp
+apply simp
+apply (rule disjI2)
+apply (simp, safe)
+apply (case_tac x, simp, simp)
+apply (drule directedD1)
+apply (clarify, rename_tac x)
+apply (case_tac x, simp, simp)
+done
+
+lemma dcpo_up: "directed (S::'a::dcpo u set) \<Longrightarrow> \<exists>x. S <<| x"
+apply (frule up_directed_lemma, safe)
+apply (erule exI)
+apply (rule exI, rule is_lub_singleton)
+done
+
+instance u :: (dcpo) dcpo
+by intro_classes (rule dcpo_up)
+
 subsection {* Lifted cpo is pointed *}
 
 lemma least_up: "\<exists>x::'a u. \<forall>y. x \<sqsubseteq> y"