src/HOLCF/Discrete.thy
author huffman
Wed Jan 02 18:27:07 2008 +0100 (2008-01-02)
changeset 25782 2d8b845dc298
parent 25131 2c8caac48ade
child 25827 c2adeb1bae5c
permissions -rw-r--r--
added dcpo instance proofs
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@15555
    18
instance discr :: (type) sq_ord ..
huffman@15555
    19
huffman@15555
    20
defs (overloaded)
huffman@15555
    21
less_discr_def: "((op <<)::('a::type)discr=>'a discr=>bool)  ==  op ="
huffman@15555
    22
huffman@15555
    23
lemma discr_less_eq [iff]: "((x::('a::type)discr) << y) = (x = y)"
huffman@15639
    24
by (unfold less_discr_def) (rule refl)
huffman@15555
    25
huffman@15555
    26
instance discr :: (type) po
huffman@15555
    27
proof
huffman@15555
    28
  fix x y z :: "'a discr"
huffman@15555
    29
  show "x << x" by simp
huffman@15555
    30
  { assume "x << y" and "y << x" thus "x = y" by simp }
huffman@15555
    31
  { assume "x << y" and "y << z" thus "x << z" by simp }
huffman@15555
    32
qed
nipkow@2841
    33
huffman@15590
    34
subsection {* Type @{typ "'a discr"} is a cpo *}
huffman@15590
    35
huffman@15555
    36
lemma discr_chain0: 
huffman@15555
    37
 "!!S::nat=>('a::type)discr. chain S ==> S i = S 0"
huffman@15555
    38
apply (unfold chain_def)
huffman@15555
    39
apply (induct_tac "i")
huffman@15555
    40
apply (rule refl)
huffman@15555
    41
apply (erule subst)
huffman@15555
    42
apply (rule sym)
huffman@15555
    43
apply fast
huffman@15555
    44
done
huffman@15555
    45
huffman@15639
    46
lemma discr_chain_range0 [simp]: 
huffman@15555
    47
 "!!S::nat=>('a::type)discr. chain(S) ==> range(S) = {S 0}"
huffman@15639
    48
by (fast elim: discr_chain0)
huffman@15555
    49
huffman@25782
    50
lemma discr_directed_lemma:
huffman@25782
    51
  fixes S :: "'a::type discr set"
huffman@25782
    52
  assumes S: "directed S"
huffman@25782
    53
  shows "\<exists>x. S = {x}"
huffman@25782
    54
proof -
huffman@25782
    55
  obtain x where x: "x \<in> S"
huffman@25782
    56
    using S by (rule directedE1)
huffman@25782
    57
  hence "S = {x}"
huffman@25782
    58
  proof (safe)
huffman@25782
    59
    fix y assume y: "y \<in> S"
huffman@25782
    60
    obtain z where "x \<sqsubseteq> z" "y \<sqsubseteq> z"
huffman@25782
    61
      using S x y by (rule directedE2)
huffman@25782
    62
    thus "y = x" by simp
huffman@25782
    63
  qed
huffman@25782
    64
  thus "\<exists>x. S = {x}" ..
huffman@25782
    65
qed
huffman@15555
    66
huffman@25782
    67
instance discr :: (type) dcpo
huffman@25782
    68
proof
huffman@25782
    69
  fix S :: "'a discr set"
huffman@25782
    70
  assume "directed S"
huffman@25782
    71
  hence "\<exists>x. S = {x}" by (rule discr_directed_lemma)
huffman@25782
    72
  thus "\<exists>x. S <<| x" by (fast intro: is_lub_singleton)
huffman@25782
    73
qed
huffman@15590
    74
huffman@15590
    75
subsection {* @{term undiscr} *}
nipkow@2841
    76
wenzelm@25131
    77
definition
wenzelm@25131
    78
  undiscr :: "('a::type)discr => 'a" where
wenzelm@25131
    79
  "undiscr x = (case x of Discr y => y)"
nipkow@2841
    80
huffman@15555
    81
lemma undiscr_Discr [simp]: "undiscr(Discr x) = x"
huffman@15590
    82
by (simp add: undiscr_def)
huffman@15555
    83
huffman@15555
    84
lemma discr_chain_f_range0:
huffman@15555
    85
 "!!S::nat=>('a::type)discr. chain(S) ==> range(%i. f(S i)) = {f(S 0)}"
huffman@15590
    86
by (fast dest: discr_chain0 elim: arg_cong)
huffman@15555
    87
huffman@15555
    88
lemma cont_discr [iff]: "cont(%x::('a::type)discr. f x)"
huffman@16213
    89
apply (unfold cont_def is_lub_def is_ub_def)
huffman@15590
    90
apply (simp add: discr_chain_f_range0)
huffman@15555
    91
done
huffman@15555
    92
nipkow@2841
    93
end