src/HOL/HOLCF/Discrete.thy
author wenzelm
Sat Nov 04 15:24:40 2017 +0100 (20 months ago)
changeset 67003 49850a679c2c
parent 62175 8ffc4d0e652d
child 67312 0d25e02759b7
permissions -rw-r--r--
more robust sorted_entries;
wenzelm@42151
     1
(*  Title:      HOL/HOLCF/Discrete.thy
nipkow@2841
     2
    Author:     Tobias Nipkow
nipkow@2841
     3
*)
nipkow@2841
     4
wenzelm@62175
     5
section \<open>Discrete cpo types\<close>
huffman@15578
     6
huffman@15555
     7
theory Discrete
huffman@19105
     8
imports Cont
huffman@15555
     9
begin
huffman@15555
    10
blanchet@58310
    11
datatype 'a discr = Discr "'a :: type"
huffman@15555
    12
wenzelm@62175
    13
subsection \<open>Discrete cpo class instance\<close>
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
wenzelm@61169
    22
  by standard (simp add: below_discr_def)
huffman@15555
    23
huffman@40434
    24
end
huffman@15555
    25
wenzelm@62175
    26
subsection \<open>\emph{undiscr}\<close>
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