src/HOLCF/Discrete.thy
author huffman
Fri Jan 04 00:01:02 2008 +0100 (2008-01-04)
changeset 25827 c2adeb1bae5c
parent 25782 2d8b845dc298
child 25902 c00823ce7288
permissions -rw-r--r--
new instance proofs for classes finite_po, chfin, flat
     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_directed_lemma:
    51   fixes S :: "'a::type discr set"
    52   assumes S: "directed S"
    53   shows "\<exists>x. S = {x}"
    54 proof -
    55   obtain x where x: "x \<in> S"
    56     using S by (rule directedE1)
    57   hence "S = {x}"
    58   proof (safe)
    59     fix y assume y: "y \<in> S"
    60     obtain z where "x \<sqsubseteq> z" "y \<sqsubseteq> z"
    61       using S x y by (rule directedE2)
    62     thus "y = x" by simp
    63   qed
    64   thus "\<exists>x. S = {x}" ..
    65 qed
    66 
    67 instance discr :: (type) dcpo
    68 proof
    69   fix S :: "'a discr set"
    70   assume "directed S"
    71   hence "\<exists>x. S = {x}" by (rule discr_directed_lemma)
    72   thus "\<exists>x. S <<| x" by (fast intro: is_lub_singleton)
    73 qed
    74 
    75 instance discr :: (finite) finite_po
    76 proof
    77   have "finite (Discr ` (UNIV :: 'a set))"
    78     by (rule finite_imageI [OF finite])
    79   also have "(Discr ` (UNIV :: 'a set)) = UNIV"
    80     by (auto, case_tac x, auto)
    81   finally show "finite (UNIV :: 'a discr set)" .
    82 qed
    83 
    84 instance discr :: (type) chfin
    85 apply (intro_classes, clarify)
    86 apply (rule_tac x=0 in exI)
    87 apply (unfold max_in_chain_def)
    88 apply (clarify, erule discr_chain0 [symmetric])
    89 done
    90 
    91 subsection {* @{term undiscr} *}
    92 
    93 definition
    94   undiscr :: "('a::type)discr => 'a" where
    95   "undiscr x = (case x of Discr y => y)"
    96 
    97 lemma undiscr_Discr [simp]: "undiscr(Discr x) = x"
    98 by (simp add: undiscr_def)
    99 
   100 lemma discr_chain_f_range0:
   101  "!!S::nat=>('a::type)discr. chain(S) ==> range(%i. f(S i)) = {f(S 0)}"
   102 by (fast dest: discr_chain0 elim: arg_cong)
   103 
   104 lemma cont_discr [iff]: "cont (%x::('a::type)discr. f x)"
   105 apply (rule chfindom_monofun2cont)
   106 apply (rule monofunI, simp)
   107 done
   108 
   109 end