src/HOLCF/Discrete.thy
 author huffman Mon Jan 14 20:28:59 2008 +0100 (2008-01-14) changeset 25906 2179c6661218 parent 25902 c00823ce7288 child 25921 0ca392ab7f37 permissions -rw-r--r--
class bifinite supersedes class dcpo; remove unnecessary dcpo stuff
```     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, clarify)
```
```    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
```