src/HOLCF/Discrete.thy
author huffman
Mon May 11 08:28:09 2009 -0700 (2009-05-11)
changeset 31095 b79d140f6d0b
parent 31076 99fe356cbbc2
child 35900 aa5dfb03eb1e
permissions -rw-r--r--
simplify fixrec proofs for mutually-recursive definitions; generate better fixpoint induction rules
     1 (*  Title:      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 {* Type @{typ "'a discr"} is a discrete cpo *}
    14 
    15 instantiation discr :: (type) below
    16 begin
    17 
    18 definition
    19   below_discr_def:
    20     "(op \<sqsubseteq> :: 'a discr \<Rightarrow> 'a discr \<Rightarrow> bool) = (op =)"
    21 
    22 instance ..
    23 end
    24 
    25 instance discr :: (type) discrete_cpo
    26 by intro_classes (simp add: below_discr_def)
    27 
    28 lemma discr_below_eq [iff]: "((x::('a::type)discr) << y) = (x = y)"
    29 by simp (* FIXME: same discrete_cpo - remove? is [iff] important? *)
    30 
    31 subsection {* Type @{typ "'a discr"} is a cpo *}
    32 
    33 lemma discr_chain0: 
    34  "!!S::nat=>('a::type)discr. chain S ==> S i = S 0"
    35 apply (unfold chain_def)
    36 apply (induct_tac "i")
    37 apply (rule refl)
    38 apply (erule subst)
    39 apply (rule sym)
    40 apply fast
    41 done
    42 
    43 lemma discr_chain_range0 [simp]: 
    44  "!!S::nat=>('a::type)discr. chain(S) ==> range(S) = {S 0}"
    45 by (fast elim: discr_chain0)
    46 
    47 instance discr :: (finite) finite_po
    48 proof
    49   have "finite (Discr ` (UNIV :: 'a set))"
    50     by (rule finite_imageI [OF finite])
    51   also have "(Discr ` (UNIV :: 'a set)) = UNIV"
    52     by (auto, case_tac x, auto)
    53   finally show "finite (UNIV :: 'a discr set)" .
    54 qed
    55 
    56 instance discr :: (type) chfin
    57 apply intro_classes
    58 apply (rule_tac x=0 in exI)
    59 apply (unfold max_in_chain_def)
    60 apply (clarify, erule discr_chain0 [symmetric])
    61 done
    62 
    63 subsection {* @{term undiscr} *}
    64 
    65 definition
    66   undiscr :: "('a::type)discr => 'a" where
    67   "undiscr x = (case x of Discr y => y)"
    68 
    69 lemma undiscr_Discr [simp]: "undiscr (Discr x) = x"
    70 by (simp add: undiscr_def)
    71 
    72 lemma Discr_undiscr [simp]: "Discr (undiscr y) = y"
    73 by (induct y) simp
    74 
    75 lemma discr_chain_f_range0:
    76  "!!S::nat=>('a::type)discr. chain(S) ==> range(%i. f(S i)) = {f(S 0)}"
    77 by (fast dest: discr_chain0 elim: arg_cong)
    78 
    79 lemma cont_discr [iff]: "cont (%x::('a::type)discr. f x)"
    80 by (rule cont_discrete_cpo)
    81 
    82 end