author | wenzelm |
Mon, 19 Jan 2015 20:39:01 +0100 | |
changeset 59409 | b7cfe12acf2e |
parent 58880 | 0baae4311a9f |
child 61169 | 4de9ff3ea29a |
permissions | -rw-r--r-- |
42151 | 1 |
(* Title: HOL/HOLCF/Discrete.thy |
2841
c2508f4ab739
Added "discrete" CPOs and modified IMP to use those rather than "lift"
nipkow
parents:
diff
changeset
|
2 |
Author: Tobias Nipkow |
c2508f4ab739
Added "discrete" CPOs and modified IMP to use those rather than "lift"
nipkow
parents:
diff
changeset
|
3 |
*) |
c2508f4ab739
Added "discrete" CPOs and modified IMP to use those rather than "lift"
nipkow
parents:
diff
changeset
|
4 |
|
58880 | 5 |
section {* Discrete cpo types *} |
15578 | 6 |
|
15555 | 7 |
theory Discrete |
19105 | 8 |
imports Cont |
15555 | 9 |
begin |
10 |
||
58310 | 11 |
datatype 'a discr = Discr "'a :: type" |
15555 | 12 |
|
40434 | 13 |
subsection {* Discrete cpo class instance *} |
15590
17f4f5afcd5f
added subsection headings, cleaned up some proofs
huffman
parents:
15578
diff
changeset
|
14 |
|
40434 | 15 |
instantiation discr :: (type) discrete_cpo |
25902 | 16 |
begin |
15555 | 17 |
|
25902 | 18 |
definition |
40434 | 19 |
"(op \<sqsubseteq> :: 'a discr \<Rightarrow> 'a discr \<Rightarrow> bool) = (op =)" |
25902 | 20 |
|
40434 | 21 |
instance |
22 |
by default (simp add: below_discr_def) |
|
15555 | 23 |
|
40434 | 24 |
end |
15555 | 25 |
|
35900
aa5dfb03eb1e
remove LaTeX hyperref warnings by avoiding antiquotations within section headings
huffman
parents:
31076
diff
changeset
|
26 |
subsection {* \emph{undiscr} *} |
2841
c2508f4ab739
Added "discrete" CPOs and modified IMP to use those rather than "lift"
nipkow
parents:
diff
changeset
|
27 |
|
25131
2c8caac48ade
modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents:
19105
diff
changeset
|
28 |
definition |
2c8caac48ade
modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents:
19105
diff
changeset
|
29 |
undiscr :: "('a::type)discr => 'a" where |
2c8caac48ade
modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents:
19105
diff
changeset
|
30 |
"undiscr x = (case x of Discr y => y)" |
2841
c2508f4ab739
Added "discrete" CPOs and modified IMP to use those rather than "lift"
nipkow
parents:
diff
changeset
|
31 |
|
26025 | 32 |
lemma undiscr_Discr [simp]: "undiscr (Discr x) = x" |
15590
17f4f5afcd5f
added subsection headings, cleaned up some proofs
huffman
parents:
15578
diff
changeset
|
33 |
by (simp add: undiscr_def) |
15555 | 34 |
|
26025 | 35 |
lemma Discr_undiscr [simp]: "Discr (undiscr y) = y" |
36 |
by (induct y) simp |
|
37 |
||
2841
c2508f4ab739
Added "discrete" CPOs and modified IMP to use those rather than "lift"
nipkow
parents:
diff
changeset
|
38 |
end |