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