src/HOLCF/Discrete.thy
author huffman
Thu Jan 17 00:51:20 2008 +0100 (2008-01-17)
changeset 25921 0ca392ab7f37
parent 25906 2179c6661218
child 26025 ca6876116bb4
permissions -rw-r--r--
change class axiom chfin to rule_format
     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 partial order *}
    17 
    18 instantiation discr :: (type) po
    19 begin
    20 
    21 definition
    22   less_discr_def [simp]:
    23     "(op \<sqsubseteq> :: 'a discr \<Rightarrow> 'a discr \<Rightarrow> bool) = (op =)"
    24 
    25 instance
    26 proof
    27   fix x y z :: "'a discr"
    28   show "x << x" by simp
    29   { assume "x << y" and "y << x" thus "x = y" by simp }
    30   { assume "x << y" and "y << z" thus "x << z" by simp }
    31 qed
    32 
    33 end
    34 
    35 lemma discr_less_eq [iff]: "((x::('a::type)discr) << y) = (x = y)"
    36 by simp
    37 
    38 subsection {* Type @{typ "'a discr"} is a cpo *}
    39 
    40 lemma discr_chain0: 
    41  "!!S::nat=>('a::type)discr. chain S ==> S i = S 0"
    42 apply (unfold chain_def)
    43 apply (induct_tac "i")
    44 apply (rule refl)
    45 apply (erule subst)
    46 apply (rule sym)
    47 apply fast
    48 done
    49 
    50 lemma discr_chain_range0 [simp]: 
    51  "!!S::nat=>('a::type)discr. chain(S) ==> range(S) = {S 0}"
    52 by (fast elim: discr_chain0)
    53 
    54 instance discr :: (finite) finite_po
    55 proof
    56   have "finite (Discr ` (UNIV :: 'a set))"
    57     by (rule finite_imageI [OF finite])
    58   also have "(Discr ` (UNIV :: 'a set)) = UNIV"
    59     by (auto, case_tac x, auto)
    60   finally show "finite (UNIV :: 'a discr set)" .
    61 qed
    62 
    63 instance discr :: (type) chfin
    64 apply intro_classes
    65 apply (rule_tac x=0 in exI)
    66 apply (unfold max_in_chain_def)
    67 apply (clarify, erule discr_chain0 [symmetric])
    68 done
    69 
    70 subsection {* @{term undiscr} *}
    71 
    72 definition
    73   undiscr :: "('a::type)discr => 'a" where
    74   "undiscr x = (case x of Discr y => y)"
    75 
    76 lemma undiscr_Discr [simp]: "undiscr(Discr x) = x"
    77 by (simp add: undiscr_def)
    78 
    79 lemma discr_chain_f_range0:
    80  "!!S::nat=>('a::type)discr. chain(S) ==> range(%i. f(S i)) = {f(S 0)}"
    81 by (fast dest: discr_chain0 elim: arg_cong)
    82 
    83 lemma cont_discr [iff]: "cont (%x::('a::type)discr. f x)"
    84 apply (rule chfindom_monofun2cont)
    85 apply (rule monofunI, simp)
    86 done
    87 
    88 end