src/HOLCF/Discrete.thy
author huffman
Wed Mar 02 00:54:06 2005 +0100 (2005-03-02)
changeset 15555 9d4dbd18ff2d
parent 14981 e73f8140af78
child 15578 d364491ba718
permissions -rw-r--r--
converted to new-style theory
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@15555
     9
theory Discrete
huffman@15555
    10
imports Cont Datatype
huffman@15555
    11
begin
huffman@15555
    12
huffman@15555
    13
datatype 'a discr = Discr "'a :: type"
huffman@15555
    14
huffman@15555
    15
instance discr :: (type) sq_ord ..
huffman@15555
    16
huffman@15555
    17
defs (overloaded)
huffman@15555
    18
less_discr_def: "((op <<)::('a::type)discr=>'a discr=>bool)  ==  op ="
huffman@15555
    19
huffman@15555
    20
lemma discr_less_eq [iff]: "((x::('a::type)discr) << y) = (x = y)"
huffman@15555
    21
apply (unfold less_discr_def)
huffman@15555
    22
apply (rule refl)
huffman@15555
    23
done
huffman@15555
    24
huffman@15555
    25
instance discr :: (type) po
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@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@15555
    43
lemma discr_chain_range0: 
huffman@15555
    44
 "!!S::nat=>('a::type)discr. chain(S) ==> range(S) = {S 0}"
huffman@15555
    45
apply (fast elim: discr_chain0)
huffman@15555
    46
done
huffman@15555
    47
declare discr_chain_range0 [simp]
huffman@15555
    48
huffman@15555
    49
lemma discr_cpo: 
huffman@15555
    50
 "!!S. chain S ==> ? x::('a::type)discr. range(S) <<| x"
huffman@15555
    51
apply (unfold is_lub_def is_ub_def)
huffman@15555
    52
apply (simp (no_asm_simp))
huffman@15555
    53
done
huffman@15555
    54
huffman@15555
    55
instance discr :: (type)cpo
huffman@15555
    56
by (intro_classes, rule discr_cpo)
nipkow@2841
    57
nipkow@2841
    58
constdefs
huffman@15555
    59
   undiscr :: "('a::type)discr => 'a"
nipkow@2841
    60
  "undiscr x == (case x of Discr y => y)"
nipkow@2841
    61
huffman@15555
    62
lemma undiscr_Discr [simp]: "undiscr(Discr x) = x"
huffman@15555
    63
apply (unfold undiscr_def)
huffman@15555
    64
apply (simp (no_asm))
huffman@15555
    65
done
huffman@15555
    66
huffman@15555
    67
lemma discr_chain_f_range0:
huffman@15555
    68
 "!!S::nat=>('a::type)discr. chain(S) ==> range(%i. f(S i)) = {f(S 0)}"
huffman@15555
    69
apply (fast dest: discr_chain0 elim: arg_cong)
huffman@15555
    70
done
huffman@15555
    71
huffman@15555
    72
lemma cont_discr [iff]: "cont(%x::('a::type)discr. f x)"
huffman@15555
    73
apply (unfold cont is_lub_def is_ub_def)
huffman@15555
    74
apply (simp (no_asm) add: discr_chain_f_range0)
huffman@15555
    75
done
huffman@15555
    76
nipkow@2841
    77
end