author | wenzelm |
Wed, 13 Jan 2016 23:07:06 +0100 | |
changeset 62175 | 8ffc4d0e652d |
parent 61169 | 4de9ff3ea29a |
child 67312 | 0d25e02759b7 |
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 |
|
62175 | 5 |
section \<open>Discrete cpo types\<close> |
15578 | 6 |
|
15555 | 7 |
theory Discrete |
19105 | 8 |
imports Cont |
15555 | 9 |
begin |
10 |
||
58310 | 11 |
datatype 'a discr = Discr "'a :: type" |
15555 | 12 |
|
62175 | 13 |
subsection \<open>Discrete cpo class instance\<close> |
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 |
61169 | 22 |
by standard (simp add: below_discr_def) |
15555 | 23 |
|
40434 | 24 |
end |
15555 | 25 |
|
62175 | 26 |
subsection \<open>\emph{undiscr}\<close> |
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 |