author | desharna |
Sat, 18 Dec 2021 23:11:49 +0100 | |
changeset 74953 | aade20a03edb |
parent 67399 | eab6ce8368fa |
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 |
67312 | 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 |
|
67399 | 18 |
definition "((\<sqsubseteq>) :: 'a discr \<Rightarrow> 'a discr \<Rightarrow> bool) = (=)" |
25902 | 19 |
|
40434 | 20 |
instance |
61169 | 21 |
by standard (simp add: below_discr_def) |
15555 | 22 |
|
40434 | 23 |
end |
15555 | 24 |
|
67312 | 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 |
|
67312 | 28 |
definition undiscr :: "('a::type)discr \<Rightarrow> 'a" |
29 |
where "undiscr x = (case x of Discr y \<Rightarrow> y)" |
|
2841
c2508f4ab739
Added "discrete" CPOs and modified IMP to use those rather than "lift"
nipkow
parents:
diff
changeset
|
30 |
|
26025 | 31 |
lemma undiscr_Discr [simp]: "undiscr (Discr x) = x" |
67312 | 32 |
by (simp add: undiscr_def) |
15555 | 33 |
|
26025 | 34 |
lemma Discr_undiscr [simp]: "Discr (undiscr y) = y" |
67312 | 35 |
by (induct y) simp |
26025 | 36 |
|
2841
c2508f4ab739
Added "discrete" CPOs and modified IMP to use those rather than "lift"
nipkow
parents:
diff
changeset
|
37 |
end |