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