src/HOLCF/Discrete.thy
author wenzelm
Sun Oct 21 14:21:48 2007 +0200 (2007-10-21)
changeset 25131 2c8caac48ade
parent 19105 3aabd46340e0
child 25782 2d8b845dc298
permissions -rw-r--r--
modernized specifications ('definition', 'abbreviation', 'notation');
     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 instance discr :: (type) sq_ord ..
    19 
    20 defs (overloaded)
    21 less_discr_def: "((op <<)::('a::type)discr=>'a discr=>bool)  ==  op ="
    22 
    23 lemma discr_less_eq [iff]: "((x::('a::type)discr) << y) = (x = y)"
    24 by (unfold less_discr_def) (rule refl)
    25 
    26 instance discr :: (type) po
    27 proof
    28   fix x y z :: "'a discr"
    29   show "x << x" by simp
    30   { assume "x << y" and "y << x" thus "x = y" by simp }
    31   { assume "x << y" and "y << z" thus "x << z" by simp }
    32 qed
    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 lemma discr_cpo: 
    51  "!!S. chain S ==> ? x::('a::type)discr. range(S) <<| x"
    52 by (unfold is_lub_def is_ub_def) simp
    53 
    54 instance discr :: (type) cpo
    55 by intro_classes (rule discr_cpo)
    56 
    57 subsection {* @{term undiscr} *}
    58 
    59 definition
    60   undiscr :: "('a::type)discr => 'a" where
    61   "undiscr x = (case x of Discr y => y)"
    62 
    63 lemma undiscr_Discr [simp]: "undiscr(Discr x) = x"
    64 by (simp add: undiscr_def)
    65 
    66 lemma discr_chain_f_range0:
    67  "!!S::nat=>('a::type)discr. chain(S) ==> range(%i. f(S i)) = {f(S 0)}"
    68 by (fast dest: discr_chain0 elim: arg_cong)
    69 
    70 lemma cont_discr [iff]: "cont(%x::('a::type)discr. f x)"
    71 apply (unfold cont_def is_lub_def is_ub_def)
    72 apply (simp add: discr_chain_f_range0)
    73 done
    74 
    75 end