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))"