src/HOLCF/Discrete.thy
author huffman
Wed Nov 10 17:56:08 2010 -0800 (2010-11-10)
changeset 40502 8e92772bc0e8
parent 40434 f775e6e0dc99
permissions -rw-r--r--
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
nipkow@2841
     1
(*  Title:      HOLCF/Discrete.thy
nipkow@2841
     2
    Author:     Tobias Nipkow
nipkow@2841
     3
*)
nipkow@2841
     4
huffman@15578
     5
header {* Discrete cpo types *}
huffman@15578
     6
huffman@15555
     7
theory Discrete
huffman@19105
     8
imports Cont
huffman@15555
     9
begin
huffman@15555
    10
huffman@15555
    11
datatype 'a discr = Discr "'a :: type"
huffman@15555
    12
huffman@40434
    13
subsection {* Discrete cpo class instance *}
huffman@15590
    14
huffman@40434
    15
instantiation discr :: (type) discrete_cpo
huffman@25902
    16
begin
huffman@15555
    17
huffman@25902
    18
definition
huffman@40434
    19
  "(op \<sqsubseteq> :: 'a discr \<Rightarrow> 'a discr \<Rightarrow> bool) = (op =)"
huffman@25902
    20
huffman@40434
    21
instance
huffman@40434
    22
by default (simp add: below_discr_def)
huffman@15555
    23
huffman@40434
    24
end
huffman@15555
    25
huffman@35900
    26
subsection {* \emph{undiscr} *}
nipkow@2841
    27
wenzelm@25131
    28
definition
wenzelm@25131
    29
  undiscr :: "('a::type)discr => 'a" where
wenzelm@25131
    30
  "undiscr x = (case x of Discr y => y)"
nipkow@2841
    31
huffman@26025
    32
lemma undiscr_Discr [simp]: "undiscr (Discr x) = x"
huffman@15590
    33
by (simp add: undiscr_def)
huffman@15555
    34
huffman@26025
    35
lemma Discr_undiscr [simp]: "Discr (undiscr y) = y"
huffman@26025
    36
by (induct y) simp
huffman@26025
    37
nipkow@2841
    38
end