--- 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} *}