src/HOLCF/Discrete.thy
 changeset 25906 2179c6661218 parent 25902 c00823ce7288 child 25921 0ca392ab7f37
```     1.1 --- a/src/HOLCF/Discrete.thy	Mon Jan 14 20:04:40 2008 +0100
1.2 +++ b/src/HOLCF/Discrete.thy	Mon Jan 14 20:28:59 2008 +0100
1.3 @@ -51,31 +51,6 @@
1.4   "!!S::nat=>('a::type)discr. chain(S) ==> range(S) = {S 0}"
1.5  by (fast elim: discr_chain0)
1.6
1.7 -lemma discr_directed_lemma:
1.8 -  fixes S :: "'a::type discr set"
1.9 -  assumes S: "directed S"
1.10 -  shows "\<exists>x. S = {x}"
1.11 -proof -
1.12 -  obtain x where x: "x \<in> S"
1.13 -    using S by (rule directedE1)
1.14 -  hence "S = {x}"
1.15 -  proof (safe)
1.16 -    fix y assume y: "y \<in> S"
1.17 -    obtain z where "x \<sqsubseteq> z" "y \<sqsubseteq> z"
1.18 -      using S x y by (rule directedE2)
1.19 -    thus "y = x" by simp
1.20 -  qed
1.21 -  thus "\<exists>x. S = {x}" ..
1.22 -qed
1.23 -
1.24 -instance discr :: (type) dcpo
1.25 -proof
1.26 -  fix S :: "'a discr set"
1.27 -  assume "directed S"
1.28 -  hence "\<exists>x. S = {x}" by (rule discr_directed_lemma)
1.29 -  thus "\<exists>x. S <<| x" by (fast intro: is_lub_singleton)
1.30 -qed
1.31 -
1.32  instance discr :: (finite) finite_po
1.33  proof
1.34    have "finite (Discr ` (UNIV :: 'a set))"
```