1(* Title: HOL/HOLCF/Discrete.thy 2 Author: Tobias Nipkow 3*) 4 5section \<open>Discrete cpo types\<close> 6 7theory Discrete 8 imports Cont 9begin 10 11datatype 'a discr = Discr "'a :: type" 12 13subsection \<open>Discrete cpo class instance\<close> 14 15instantiation discr :: (type) discrete_cpo 16begin 17 18definition "((\<sqsubseteq>) :: 'a discr \<Rightarrow> 'a discr \<Rightarrow> bool) = (=)" 19 20instance 21 by standard (simp add: below_discr_def) 22 23end 24 25 26subsection \<open>\emph{undiscr}\<close> 27 28definition undiscr :: "('a::type)discr \<Rightarrow> 'a" 29 where "undiscr x = (case x of Discr y \<Rightarrow> y)" 30 31lemma undiscr_Discr [simp]: "undiscr (Discr x) = x" 32 by (simp add: undiscr_def) 33 34lemma Discr_undiscr [simp]: "Discr (undiscr y) = y" 35 by (induct y) simp 36 37end 38