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