1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/HOLCF/Discrete.thy	Sat Nov 27 16:08:10 2010 -0800
     1.3 @@ -0,0 +1,38 @@
     1.4 +(*  Title:      HOLCF/Discrete.thy
     1.5 +    Author:     Tobias Nipkow
     1.6 +*)
     1.7 +
     1.8 +header {* Discrete cpo types *}
     1.9 +
    1.10 +theory Discrete
    1.11 +imports Cont
    1.12 +begin
    1.13 +
    1.14 +datatype 'a discr = Discr "'a :: type"
    1.15 +
    1.16 +subsection {* Discrete cpo class instance *}
    1.17 +
    1.18 +instantiation discr :: (type) discrete_cpo
    1.19 +begin
    1.20 +
    1.21 +definition
    1.22 +  "(op \<sqsubseteq> :: 'a discr \<Rightarrow> 'a discr \<Rightarrow> bool) = (op =)"
    1.23 +
    1.24 +instance
    1.25 +by default (simp add: below_discr_def)
    1.26 +
    1.27 +end
    1.28 +
    1.29 +subsection {* \emph{undiscr} *}
    1.30 +
    1.31 +definition
    1.32 +  undiscr :: "('a::type)discr => 'a" where
    1.33 +  "undiscr x = (case x of Discr y => y)"
    1.34 +
    1.35 +lemma undiscr_Discr [simp]: "undiscr (Discr x) = x"
    1.36 +by (simp add: undiscr_def)
    1.37 +
    1.38 +lemma Discr_undiscr [simp]: "Discr (undiscr y) = y"
    1.39 +by (induct y) simp
    1.40 +
    1.41 +end