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
nipkow@2841
     1
(*  Title:      HOLCF/Discrete.thy
nipkow@2841
     2
    ID:         $Id$
nipkow@2841
     3
    Author:     Tobias Nipkow
nipkow@2841
     4
wenzelm@12030
     5
Discrete CPOs.
nipkow@2841
     6
*)
nipkow@2841
     7
huffman@15578
     8
header {* Discrete cpo types *}
huffman@15578
     9
huffman@15555
    10
theory Discrete
huffman@19105
    11
imports Cont
huffman@15555
    12
begin
huffman@15555
    13
huffman@15555
    14
datatype 'a discr = Discr "'a :: type"
huffman@15555
    15
huffman@15590
    16
subsection {* Type @{typ "'a discr"} is a partial order *}
huffman@15590
    17
huffman@25902
    18
instantiation discr :: (type) po
huffman@25902
    19
begin
huffman@15555
    20
huffman@25902
    21
definition
huffman@25902
    22
  less_discr_def [simp]:
huffman@25902
    23
    "(op \<sqsubseteq> :: 'a discr \<Rightarrow> 'a discr \<Rightarrow> bool) = (op =)"
huffman@15555
    24
huffman@25902
    25
instance
huffman@15555
    26
proof
huffman@15555
    27
  fix x y z :: "'a discr"
huffman@15555
    28
  show "x << x" by simp
huffman@15555
    29
  { assume "x << y" and "y << x" thus "x = y" by simp }
huffman@15555
    30
  { assume "x << y" and "y << z" thus "x << z" by simp }
huffman@15555
    31
qed
nipkow@2841
    32
huffman@25902
    33
end
huffman@25902
    34
huffman@25902
    35
lemma discr_less_eq [iff]: "((x::('a::type)discr) << y) = (x = y)"
huffman@25902
    36
by simp
huffman@25902
    37
huffman@15590
    38
subsection {* Type @{typ "'a discr"} is a cpo *}
huffman@15590
    39
huffman@15555
    40
lemma discr_chain0: 
huffman@15555
    41
 "!!S::nat=>('a::type)discr. chain S ==> S i = S 0"
huffman@15555
    42
apply (unfold chain_def)
huffman@15555
    43
apply (induct_tac "i")
huffman@15555
    44
apply (rule refl)
huffman@15555
    45
apply (erule subst)
huffman@15555
    46
apply (rule sym)
huffman@15555
    47
apply fast
huffman@15555
    48
done
huffman@15555
    49
huffman@15639
    50
lemma discr_chain_range0 [simp]: 
huffman@15555
    51
 "!!S::nat=>('a::type)discr. chain(S) ==> range(S) = {S 0}"
huffman@15639
    52
by (fast elim: discr_chain0)
huffman@15555
    53
huffman@25827
    54
instance discr :: (finite) finite_po
huffman@25827
    55
proof
huffman@25827
    56
  have "finite (Discr ` (UNIV :: 'a set))"
huffman@25827
    57
    by (rule finite_imageI [OF finite])
huffman@25827
    58
  also have "(Discr ` (UNIV :: 'a set)) = UNIV"
huffman@25827
    59
    by (auto, case_tac x, auto)
huffman@25827
    60
  finally show "finite (UNIV :: 'a discr set)" .
huffman@25827
    61
qed
huffman@25827
    62
huffman@25827
    63
instance discr :: (type) chfin
huffman@25827
    64
apply (intro_classes, clarify)
huffman@25827
    65
apply (rule_tac x=0 in exI)
huffman@25827
    66
apply (unfold max_in_chain_def)
huffman@25827
    67
apply (clarify, erule discr_chain0 [symmetric])
huffman@25827
    68
done
huffman@25827
    69
huffman@15590
    70
subsection {* @{term undiscr} *}
nipkow@2841
    71
wenzelm@25131
    72
definition
wenzelm@25131
    73
  undiscr :: "('a::type)discr => 'a" where
wenzelm@25131
    74
  "undiscr x = (case x of Discr y => y)"
nipkow@2841
    75
huffman@15555
    76
lemma undiscr_Discr [simp]: "undiscr(Discr x) = x"
huffman@15590
    77
by (simp add: undiscr_def)
huffman@15555
    78
huffman@15555
    79
lemma discr_chain_f_range0:
huffman@15555
    80
 "!!S::nat=>('a::type)discr. chain(S) ==> range(%i. f(S i)) = {f(S 0)}"
huffman@15590
    81
by (fast dest: discr_chain0 elim: arg_cong)
huffman@15555
    82
huffman@25827
    83
lemma cont_discr [iff]: "cont (%x::('a::type)discr. f x)"
huffman@25827
    84
apply (rule chfindom_monofun2cont)
huffman@25827
    85
apply (rule monofunI, simp)
huffman@15555
    86
done
huffman@15555
    87
nipkow@2841
    88
end