src/HOL/HOLCF/Discrete.thy
author wenzelm
Mon Jan 01 23:07:24 2018 +0100 (19 months ago)
changeset 67312 0d25e02759b7
parent 62175 8ffc4d0e652d
child 67399 eab6ce8368fa
permissions -rw-r--r--
misc tuning and modernization;
     1 (*  Title:      HOL/HOLCF/Discrete.thy
     2     Author:     Tobias Nipkow
     3 *)
     4 
     5 section \<open>Discrete cpo types\<close>
     6 
     7 theory Discrete
     8   imports Cont
     9 begin
    10 
    11 datatype 'a discr = Discr "'a :: type"
    12 
    13 subsection \<open>Discrete cpo class instance\<close>
    14 
    15 instantiation discr :: (type) discrete_cpo
    16 begin
    17 
    18 definition "(op \<sqsubseteq> :: 'a discr \<Rightarrow> 'a discr \<Rightarrow> bool) = (op =)"
    19 
    20 instance
    21   by standard (simp add: below_discr_def)
    22 
    23 end
    24 
    25 
    26 subsection \<open>\emph{undiscr}\<close>
    27 
    28 definition undiscr :: "('a::type)discr \<Rightarrow> 'a"
    29   where "undiscr x = (case x of Discr y \<Rightarrow> y)"
    30 
    31 lemma undiscr_Discr [simp]: "undiscr (Discr x) = x"
    32   by (simp add: undiscr_def)
    33 
    34 lemma Discr_undiscr [simp]: "Discr (undiscr y) = y"
    35   by (induct y) simp
    36 
    37 end