src/HOLCF/Discrete.thy
author huffman
Tue Mar 08 00:15:01 2005 +0100 (2005-03-08)
changeset 15590 17f4f5afcd5f
parent 15578 d364491ba718
child 15639 99ed5113783b
permissions -rw-r--r--
added subsection headings, cleaned up some proofs
nipkow@2841
     1
(*  Title:      HOLCF/Discrete.thy
nipkow@2841
     2
    ID:         $Id$
nipkow@2841
     3
    Author:     Tobias Nipkow
huffman@15555
     4
    License:    GPL (GNU GENERAL PUBLIC LICENSE)
nipkow@2841
     5
wenzelm@12030
     6
Discrete CPOs.
nipkow@2841
     7
*)
nipkow@2841
     8
huffman@15578
     9
header {* Discrete cpo types *}
huffman@15578
    10
huffman@15555
    11
theory Discrete
huffman@15555
    12
imports Cont Datatype
huffman@15555
    13
begin
huffman@15555
    14
huffman@15555
    15
datatype 'a discr = Discr "'a :: type"
huffman@15555
    16
huffman@15590
    17
subsection {* Type @{typ "'a discr"} is a partial order *}
huffman@15590
    18
huffman@15555
    19
instance discr :: (type) sq_ord ..
huffman@15555
    20
huffman@15555
    21
defs (overloaded)
huffman@15555
    22
less_discr_def: "((op <<)::('a::type)discr=>'a discr=>bool)  ==  op ="
huffman@15555
    23
huffman@15555
    24
lemma discr_less_eq [iff]: "((x::('a::type)discr) << y) = (x = y)"
huffman@15555
    25
apply (unfold less_discr_def)
huffman@15555
    26
apply (rule refl)
huffman@15555
    27
done
huffman@15555
    28
huffman@15555
    29
instance discr :: (type) po
huffman@15555
    30
proof
huffman@15555
    31
  fix x y z :: "'a discr"
huffman@15555
    32
  show "x << x" by simp
huffman@15555
    33
  { assume "x << y" and "y << x" thus "x = y" by simp }
huffman@15555
    34
  { assume "x << y" and "y << z" thus "x << z" by simp }
huffman@15555
    35
qed
nipkow@2841
    36
huffman@15590
    37
subsection {* Type @{typ "'a discr"} is a cpo *}
huffman@15590
    38
huffman@15555
    39
lemma discr_chain0: 
huffman@15555
    40
 "!!S::nat=>('a::type)discr. chain S ==> S i = S 0"
huffman@15555
    41
apply (unfold chain_def)
huffman@15555
    42
apply (induct_tac "i")
huffman@15555
    43
apply (rule refl)
huffman@15555
    44
apply (erule subst)
huffman@15555
    45
apply (rule sym)
huffman@15555
    46
apply fast
huffman@15555
    47
done
huffman@15555
    48
huffman@15555
    49
lemma discr_chain_range0: 
huffman@15555
    50
 "!!S::nat=>('a::type)discr. chain(S) ==> range(S) = {S 0}"
huffman@15555
    51
apply (fast elim: discr_chain0)
huffman@15555
    52
done
huffman@15555
    53
declare discr_chain_range0 [simp]
huffman@15555
    54
huffman@15555
    55
lemma discr_cpo: 
huffman@15555
    56
 "!!S. chain S ==> ? x::('a::type)discr. range(S) <<| x"
huffman@15555
    57
apply (unfold is_lub_def is_ub_def)
huffman@15555
    58
apply (simp (no_asm_simp))
huffman@15555
    59
done
huffman@15555
    60
huffman@15590
    61
instance discr :: (type) cpo
huffman@15590
    62
by intro_classes (rule discr_cpo)
huffman@15590
    63
huffman@15590
    64
subsection {* @{term undiscr} *}
nipkow@2841
    65
nipkow@2841
    66
constdefs
huffman@15555
    67
   undiscr :: "('a::type)discr => 'a"
nipkow@2841
    68
  "undiscr x == (case x of Discr y => y)"
nipkow@2841
    69
huffman@15555
    70
lemma undiscr_Discr [simp]: "undiscr(Discr x) = x"
huffman@15590
    71
by (simp add: undiscr_def)
huffman@15555
    72
huffman@15555
    73
lemma discr_chain_f_range0:
huffman@15555
    74
 "!!S::nat=>('a::type)discr. chain(S) ==> range(%i. f(S i)) = {f(S 0)}"
huffman@15590
    75
by (fast dest: discr_chain0 elim: arg_cong)
huffman@15555
    76
huffman@15555
    77
lemma cont_discr [iff]: "cont(%x::('a::type)discr. f x)"
huffman@15555
    78
apply (unfold cont is_lub_def is_ub_def)
huffman@15590
    79
apply (simp add: discr_chain_f_range0)
huffman@15555
    80
done
huffman@15555
    81
nipkow@2841
    82
end