src/HOLCF/Discrete.thy
author huffman
Thu Jan 31 21:23:14 2008 +0100 (2008-01-31)
changeset 26025 ca6876116bb4
parent 25921 0ca392ab7f37
child 29138 661a8db7e647
permissions -rw-r--r--
instances for class discrete_cpo
     1 (*  Title:      HOLCF/Discrete.thy
     2     ID:         $Id$
     3     Author:     Tobias Nipkow
     4 
     5 Discrete CPOs.
     6 *)
     7 
     8 header {* Discrete cpo types *}
     9 
    10 theory Discrete
    11 imports Cont
    12 begin
    13 
    14 datatype 'a discr = Discr "'a :: type"
    15 
    16 subsection {* Type @{typ "'a discr"} is a discrete cpo *}
    17 
    18 instantiation discr :: (type) sq_ord
    19 begin
    20 
    21 definition
    22   less_discr_def:
    23     "(op \<sqsubseteq> :: 'a discr \<Rightarrow> 'a discr \<Rightarrow> bool) = (op =)"
    24 
    25 instance ..
    26 end
    27 
    28 instance discr :: (type) discrete_cpo
    29 by intro_classes (simp add: less_discr_def)
    30 
    31 lemma discr_less_eq [iff]: "((x::('a::type)discr) << y) = (x = y)"
    32 by simp
    33 
    34 subsection {* Type @{typ "'a discr"} is a cpo *}
    35 
    36 lemma discr_chain0: 
    37  "!!S::nat=>('a::type)discr. chain S ==> S i = S 0"
    38 apply (unfold chain_def)
    39 apply (induct_tac "i")
    40 apply (rule refl)
    41 apply (erule subst)
    42 apply (rule sym)
    43 apply fast
    44 done
    45 
    46 lemma discr_chain_range0 [simp]: 
    47  "!!S::nat=>('a::type)discr. chain(S) ==> range(S) = {S 0}"
    48 by (fast elim: discr_chain0)
    49 
    50 instance discr :: (finite) finite_po
    51 proof
    52   have "finite (Discr ` (UNIV :: 'a set))"
    53     by (rule finite_imageI [OF finite])
    54   also have "(Discr ` (UNIV :: 'a set)) = UNIV"
    55     by (auto, case_tac x, auto)
    56   finally show "finite (UNIV :: 'a discr set)" .
    57 qed
    58 
    59 instance discr :: (type) chfin
    60 apply intro_classes
    61 apply (rule_tac x=0 in exI)
    62 apply (unfold max_in_chain_def)
    63 apply (clarify, erule discr_chain0 [symmetric])
    64 done
    65 
    66 subsection {* @{term undiscr} *}
    67 
    68 definition
    69   undiscr :: "('a::type)discr => 'a" where
    70   "undiscr x = (case x of Discr y => y)"
    71 
    72 lemma undiscr_Discr [simp]: "undiscr (Discr x) = x"
    73 by (simp add: undiscr_def)
    74 
    75 lemma Discr_undiscr [simp]: "Discr (undiscr y) = y"
    76 by (induct y) simp
    77 
    78 lemma discr_chain_f_range0:
    79  "!!S::nat=>('a::type)discr. chain(S) ==> range(%i. f(S i)) = {f(S 0)}"
    80 by (fast dest: discr_chain0 elim: arg_cong)
    81 
    82 lemma cont_discr [iff]: "cont (%x::('a::type)discr. f x)"
    83 by (rule cont_discrete_cpo)
    84 
    85 end