added dcpo instance proofs
authorhuffman
Wed Jan 02 18:27:07 2008 +0100 (2008-01-02)
changeset 257822d8b845dc298
parent 25781 9182d8bc7742
child 25783 b2874ee9081a
added dcpo instance proofs
src/HOLCF/Discrete.thy
     1.1 --- a/src/HOLCF/Discrete.thy	Wed Jan 02 18:26:01 2008 +0100
     1.2 +++ b/src/HOLCF/Discrete.thy	Wed Jan 02 18:27:07 2008 +0100
     1.3 @@ -47,12 +47,30 @@
     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_cpo: 
     1.8 - "!!S. chain S ==> ? x::('a::type)discr. range(S) <<| x"
     1.9 -by (unfold is_lub_def is_ub_def) simp
    1.10 +lemma discr_directed_lemma:
    1.11 +  fixes S :: "'a::type discr set"
    1.12 +  assumes S: "directed S"
    1.13 +  shows "\<exists>x. S = {x}"
    1.14 +proof -
    1.15 +  obtain x where x: "x \<in> S"
    1.16 +    using S by (rule directedE1)
    1.17 +  hence "S = {x}"
    1.18 +  proof (safe)
    1.19 +    fix y assume y: "y \<in> S"
    1.20 +    obtain z where "x \<sqsubseteq> z" "y \<sqsubseteq> z"
    1.21 +      using S x y by (rule directedE2)
    1.22 +    thus "y = x" by simp
    1.23 +  qed
    1.24 +  thus "\<exists>x. S = {x}" ..
    1.25 +qed
    1.26  
    1.27 -instance discr :: (type) cpo
    1.28 -by intro_classes (rule discr_cpo)
    1.29 +instance discr :: (type) dcpo
    1.30 +proof
    1.31 +  fix S :: "'a discr set"
    1.32 +  assume "directed S"
    1.33 +  hence "\<exists>x. S = {x}" by (rule discr_directed_lemma)
    1.34 +  thus "\<exists>x. S <<| x" by (fast intro: is_lub_singleton)
    1.35 +qed
    1.36  
    1.37  subsection {* @{term undiscr} *}
    1.38