src/HOLCF/Discrete.thy
author huffman
Tue Mar 08 00:15:01 2005 +0100 (2005-03-08)
changeset 15590 17f4f5afcd5f
parent 15578 d364491ba718
child 15639 99ed5113783b
permissions -rw-r--r--
added subsection headings, cleaned up some proofs
     1 (*  Title:      HOLCF/Discrete.thy
     2     ID:         $Id$
     3     Author:     Tobias Nipkow
     4     License:    GPL (GNU GENERAL PUBLIC LICENSE)
     5 
     6 Discrete CPOs.
     7 *)
     8 
     9 header {* Discrete cpo types *}
    10 
    11 theory Discrete
    12 imports Cont Datatype
    13 begin
    14 
    15 datatype 'a discr = Discr "'a :: type"
    16 
    17 subsection {* Type @{typ "'a discr"} is a partial order *}
    18 
    19 instance discr :: (type) sq_ord ..
    20 
    21 defs (overloaded)
    22 less_discr_def: "((op <<)::('a::type)discr=>'a discr=>bool)  ==  op ="
    23 
    24 lemma discr_less_eq [iff]: "((x::('a::type)discr) << y) = (x = y)"
    25 apply (unfold less_discr_def)
    26 apply (rule refl)
    27 done
    28 
    29 instance discr :: (type) po
    30 proof
    31   fix x y z :: "'a discr"
    32   show "x << x" by simp
    33   { assume "x << y" and "y << x" thus "x = y" by simp }
    34   { assume "x << y" and "y << z" thus "x << z" by simp }
    35 qed
    36 
    37 subsection {* Type @{typ "'a discr"} is a cpo *}
    38 
    39 lemma discr_chain0: 
    40  "!!S::nat=>('a::type)discr. chain S ==> S i = S 0"
    41 apply (unfold chain_def)
    42 apply (induct_tac "i")
    43 apply (rule refl)
    44 apply (erule subst)
    45 apply (rule sym)
    46 apply fast
    47 done
    48 
    49 lemma discr_chain_range0: 
    50  "!!S::nat=>('a::type)discr. chain(S) ==> range(S) = {S 0}"
    51 apply (fast elim: discr_chain0)
    52 done
    53 declare discr_chain_range0 [simp]
    54 
    55 lemma discr_cpo: 
    56  "!!S. chain S ==> ? x::('a::type)discr. range(S) <<| x"
    57 apply (unfold is_lub_def is_ub_def)
    58 apply (simp (no_asm_simp))
    59 done
    60 
    61 instance discr :: (type) cpo
    62 by intro_classes (rule discr_cpo)
    63 
    64 subsection {* @{term undiscr} *}
    65 
    66 constdefs
    67    undiscr :: "('a::type)discr => 'a"
    68   "undiscr x == (case x of Discr y => y)"
    69 
    70 lemma undiscr_Discr [simp]: "undiscr(Discr x) = x"
    71 by (simp add: undiscr_def)
    72 
    73 lemma discr_chain_f_range0:
    74  "!!S::nat=>('a::type)discr. chain(S) ==> range(%i. f(S i)) = {f(S 0)}"
    75 by (fast dest: discr_chain0 elim: arg_cong)
    76 
    77 lemma cont_discr [iff]: "cont(%x::('a::type)discr. f x)"
    78 apply (unfold cont is_lub_def is_ub_def)
    79 apply (simp add: discr_chain_f_range0)
    80 done
    81 
    82 end