src/HOLCF/Discrete.thy
author huffman
Mon Mar 22 12:52:51 2010 -0700 (2010-03-22)
changeset 35900 aa5dfb03eb1e
parent 31076 99fe356cbbc2
child 40089 8adc57fb8454
permissions -rw-r--r--
remove LaTeX hyperref warnings by avoiding antiquotations within section headings
nipkow@2841
     1
(*  Title:      HOLCF/Discrete.thy
nipkow@2841
     2
    Author:     Tobias Nipkow
nipkow@2841
     3
*)
nipkow@2841
     4
huffman@15578
     5
header {* Discrete cpo types *}
huffman@15578
     6
huffman@15555
     7
theory Discrete
huffman@19105
     8
imports Cont
huffman@15555
     9
begin
huffman@15555
    10
huffman@15555
    11
datatype 'a discr = Discr "'a :: type"
huffman@15555
    12
huffman@35900
    13
subsection {* Discrete ordering *}
huffman@15590
    14
huffman@31076
    15
instantiation discr :: (type) below
huffman@25902
    16
begin
huffman@15555
    17
huffman@25902
    18
definition
huffman@31076
    19
  below_discr_def:
huffman@25902
    20
    "(op \<sqsubseteq> :: 'a discr \<Rightarrow> 'a discr \<Rightarrow> bool) = (op =)"
huffman@15555
    21
huffman@26025
    22
instance ..
huffman@26025
    23
end
nipkow@2841
    24
huffman@35900
    25
subsection {* Discrete cpo class instance *}
huffman@35900
    26
huffman@26025
    27
instance discr :: (type) discrete_cpo
huffman@31076
    28
by intro_classes (simp add: below_discr_def)
huffman@25902
    29
huffman@31076
    30
lemma discr_below_eq [iff]: "((x::('a::type)discr) << y) = (x = y)"
huffman@31076
    31
by simp (* FIXME: same discrete_cpo - remove? is [iff] important? *)
huffman@25902
    32
huffman@15555
    33
lemma discr_chain0: 
huffman@15555
    34
 "!!S::nat=>('a::type)discr. chain S ==> S i = S 0"
huffman@15555
    35
apply (unfold chain_def)
huffman@15555
    36
apply (induct_tac "i")
huffman@15555
    37
apply (rule refl)
huffman@15555
    38
apply (erule subst)
huffman@15555
    39
apply (rule sym)
huffman@15555
    40
apply fast
huffman@15555
    41
done
huffman@15555
    42
huffman@15639
    43
lemma discr_chain_range0 [simp]: 
huffman@15555
    44
 "!!S::nat=>('a::type)discr. chain(S) ==> range(S) = {S 0}"
huffman@15639
    45
by (fast elim: discr_chain0)
huffman@15555
    46
huffman@25827
    47
instance discr :: (finite) finite_po
huffman@25827
    48
proof
huffman@25827
    49
  have "finite (Discr ` (UNIV :: 'a set))"
huffman@25827
    50
    by (rule finite_imageI [OF finite])
huffman@25827
    51
  also have "(Discr ` (UNIV :: 'a set)) = UNIV"
huffman@25827
    52
    by (auto, case_tac x, auto)
huffman@25827
    53
  finally show "finite (UNIV :: 'a discr set)" .
huffman@25827
    54
qed
huffman@25827
    55
huffman@25827
    56
instance discr :: (type) chfin
huffman@25921
    57
apply intro_classes
huffman@25827
    58
apply (rule_tac x=0 in exI)
huffman@25827
    59
apply (unfold max_in_chain_def)
huffman@25827
    60
apply (clarify, erule discr_chain0 [symmetric])
huffman@25827
    61
done
huffman@25827
    62
huffman@35900
    63
subsection {* \emph{undiscr} *}
nipkow@2841
    64
wenzelm@25131
    65
definition
wenzelm@25131
    66
  undiscr :: "('a::type)discr => 'a" where
wenzelm@25131
    67
  "undiscr x = (case x of Discr y => y)"
nipkow@2841
    68
huffman@26025
    69
lemma undiscr_Discr [simp]: "undiscr (Discr x) = x"
huffman@15590
    70
by (simp add: undiscr_def)
huffman@15555
    71
huffman@26025
    72
lemma Discr_undiscr [simp]: "Discr (undiscr y) = y"
huffman@26025
    73
by (induct y) simp
huffman@26025
    74
huffman@15555
    75
lemma discr_chain_f_range0:
huffman@15555
    76
 "!!S::nat=>('a::type)discr. chain(S) ==> range(%i. f(S i)) = {f(S 0)}"
huffman@15590
    77
by (fast dest: discr_chain0 elim: arg_cong)
huffman@15555
    78
huffman@25827
    79
lemma cont_discr [iff]: "cont (%x::('a::type)discr. f x)"
huffman@26025
    80
by (rule cont_discrete_cpo)
huffman@15555
    81
nipkow@2841
    82
end