src/HOL/HOLCF/Discrete.thy
author huffman
Sat, 27 Nov 2010 16:08:10 -0800
changeset 40774 0437dbc127b3
parent 40434 src/HOLCF/Discrete.thy@f775e6e0dc99
child 42151 4da4fc77664b
permissions -rw-r--r--
moved directory src/HOLCF to src/HOL/HOLCF; added HOLCF theories to src/HOL/IsaMakefile;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
2841
c2508f4ab739 Added "discrete" CPOs and modified IMP to use those rather than "lift"
nipkow
parents:
diff changeset
     1
(*  Title:      HOLCF/Discrete.thy
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
15578
d364491ba718 add header
huffman
parents: 15555
diff changeset
     5
header {* Discrete cpo types *}
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
9d4dbd18ff2d converted to new-style theory
huffman
parents: 14981
diff changeset
    11
datatype 'a discr = Discr "'a :: type"
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