src/HOL/HOLCF/Discrete.thy
author haftmann
Sun Jun 23 21:16:07 2013 +0200 (2013-06-23)
changeset 52435 6646bb548c6b
parent 42151 4da4fc77664b
child 58249 180f1b3508ed
permissions -rw-r--r--
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
     1 (*  Title:      HOL/HOLCF/Discrete.thy
     2     Author:     Tobias Nipkow
     3 *)
     4 
     5 header {* Discrete cpo types *}
     6 
     7 theory Discrete
     8 imports Cont
     9 begin
    10 
    11 datatype 'a discr = Discr "'a :: type"
    12 
    13 subsection {* Discrete cpo class instance *}
    14 
    15 instantiation discr :: (type) discrete_cpo
    16 begin
    17 
    18 definition
    19   "(op \<sqsubseteq> :: 'a discr \<Rightarrow> 'a discr \<Rightarrow> bool) = (op =)"
    20 
    21 instance
    22 by default (simp add: below_discr_def)
    23 
    24 end
    25 
    26 subsection {* \emph{undiscr} *}
    27 
    28 definition
    29   undiscr :: "('a::type)discr => 'a" where
    30   "undiscr x = (case x of Discr y => y)"
    31 
    32 lemma undiscr_Discr [simp]: "undiscr (Discr x) = x"
    33 by (simp add: undiscr_def)
    34 
    35 lemma Discr_undiscr [simp]: "Discr (undiscr y) = y"
    36 by (induct y) simp
    37 
    38 end