# HG changeset patch
# User huffman
# Date 1199294827 -3600
# Node ID 2d8b845dc298761709140c060a6c1894e0cfa944
# Parent  9182d8bc7742623a5fcbc544112c8d018da26794
added dcpo instance proofs

diff -r 9182d8bc7742 -r 2d8b845dc298 src/HOLCF/Discrete.thy
--- a/src/HOLCF/Discrete.thy	Wed Jan 02 18:26:01 2008 +0100
+++ b/src/HOLCF/Discrete.thy	Wed Jan 02 18:27:07 2008 +0100
@@ -47,12 +47,30 @@
  "!!S::nat=>('a::type)discr. chain(S) ==> range(S) = {S 0}"
 by (fast elim: discr_chain0)
 
-lemma discr_cpo: 
- "!!S. chain S ==> ? x::('a::type)discr. range(S) <<| x"
-by (unfold is_lub_def is_ub_def) simp
+lemma discr_directed_lemma:
+  fixes S :: "'a::type discr set"
+  assumes S: "directed S"
+  shows "\<exists>x. S = {x}"
+proof -
+  obtain x where x: "x \<in> S"
+    using S by (rule directedE1)
+  hence "S = {x}"
+  proof (safe)
+    fix y assume y: "y \<in> S"
+    obtain z where "x \<sqsubseteq> z" "y \<sqsubseteq> z"
+      using S x y by (rule directedE2)
+    thus "y = x" by simp
+  qed
+  thus "\<exists>x. S = {x}" ..
+qed
 
-instance discr :: (type) cpo
-by intro_classes (rule discr_cpo)
+instance discr :: (type) dcpo
+proof
+  fix S :: "'a discr set"
+  assume "directed S"
+  hence "\<exists>x. S = {x}" by (rule discr_directed_lemma)
+  thus "\<exists>x. S <<| x" by (fast intro: is_lub_singleton)
+qed
 
 subsection {* @{term undiscr} *}