src/HOL/HOLCF/Discrete.thy
author wenzelm
Mon, 19 Jan 2015 20:39:01 +0100
changeset 59409 b7cfe12acf2e
parent 58880 0baae4311a9f
child 61169 4de9ff3ea29a
permissions -rw-r--r--
tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
42151
4da4fc77664b tuned headers;
wenzelm
parents: 40774
diff changeset
     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
0baae4311a9f modernized header;
wenzelm
parents: 58310
diff changeset
     5
section {* Discrete cpo types *}
15578
d364491ba718 add header
huffman
parents: 15555
diff changeset
     6
15555
9d4dbd18ff2d converted to new-style theory
huffman
parents: 14981
diff changeset
     7
theory Discrete
19105
3aabd46340e0 use minimal imports
huffman
parents: 16213
diff changeset
     8
imports Cont
15555
9d4dbd18ff2d converted to new-style theory
huffman
parents: 14981
diff changeset
     9
begin
9d4dbd18ff2d converted to new-style theory
huffman
parents: 14981
diff changeset
    10
58310
91ea607a34d8 updated news
blanchet
parents: 58249
diff changeset
    11
datatype 'a discr = Discr "'a :: type"
15555
9d4dbd18ff2d converted to new-style theory
huffman
parents: 14981
diff changeset
    12
40434
f775e6e0dc99 remove unnecessary stuff from Discrete.thy
huffman
parents: 40091
diff changeset
    13
subsection {* Discrete cpo class instance *}
15590
17f4f5afcd5f added subsection headings, cleaned up some proofs
huffman
parents: 15578
diff changeset
    14
40434
f775e6e0dc99 remove unnecessary stuff from Discrete.thy
huffman
parents: 40091
diff changeset
    15
instantiation discr :: (type) discrete_cpo
25902
c00823ce7288 new-style class instantiation
huffman
parents: 25827
diff changeset
    16
begin
15555
9d4dbd18ff2d converted to new-style theory
huffman
parents: 14981
diff changeset
    17
25902
c00823ce7288 new-style class instantiation
huffman
parents: 25827
diff changeset
    18
definition
40434
f775e6e0dc99 remove unnecessary stuff from Discrete.thy
huffman
parents: 40091
diff changeset
    19
  "(op \<sqsubseteq> :: 'a discr \<Rightarrow> 'a discr \<Rightarrow> bool) = (op =)"
25902
c00823ce7288 new-style class instantiation
huffman
parents: 25827
diff changeset
    20
40434
f775e6e0dc99 remove unnecessary stuff from Discrete.thy
huffman
parents: 40091
diff changeset
    21
instance
f775e6e0dc99 remove unnecessary stuff from Discrete.thy
huffman
parents: 40091
diff changeset
    22
by default (simp add: below_discr_def)
15555
9d4dbd18ff2d converted to new-style theory
huffman
parents: 14981
diff changeset
    23
40434
f775e6e0dc99 remove unnecessary stuff from Discrete.thy
huffman
parents: 40091
diff changeset
    24
end
15555
9d4dbd18ff2d converted to new-style theory
huffman
parents: 14981
diff changeset
    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
ca6876116bb4 instances for class discrete_cpo
huffman
parents: 25921
diff changeset
    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
9d4dbd18ff2d converted to new-style theory
huffman
parents: 14981
diff changeset
    34
26025
ca6876116bb4 instances for class discrete_cpo
huffman
parents: 25921
diff changeset
    35
lemma Discr_undiscr [simp]: "Discr (undiscr y) = y"
ca6876116bb4 instances for class discrete_cpo
huffman
parents: 25921
diff changeset
    36
by (induct y) simp
ca6876116bb4 instances for class discrete_cpo
huffman
parents: 25921
diff changeset
    37
2841
c2508f4ab739 Added "discrete" CPOs and modified IMP to use those rather than "lift"
nipkow
parents:
diff changeset
    38
end