src/HOLCF/Discrete.thy
author huffman
Sat, 04 Jun 2005 00:22:08 +0200
changeset 16221 879400e029bf
parent 16213 88ddef269510
child 19105 3aabd46340e0
permissions -rw-r--r--
New theory with lemmas for the fixrec package
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
2841
c2508f4ab739 Added "discrete" CPOs and modified IMP to use those rather than "lift"
nipkow
parents:
diff changeset
     1
(*  Title:      HOLCF/Discrete.thy
c2508f4ab739 Added "discrete" CPOs and modified IMP to use those rather than "lift"
nipkow
parents:
diff changeset
     2
    ID:         $Id$
c2508f4ab739 Added "discrete" CPOs and modified IMP to use those rather than "lift"
nipkow
parents:
diff changeset
     3
    Author:     Tobias Nipkow
c2508f4ab739 Added "discrete" CPOs and modified IMP to use those rather than "lift"
nipkow
parents:
diff changeset
     4
12030
wenzelm
parents: 2841
diff changeset
     5
Discrete CPOs.
2841
c2508f4ab739 Added "discrete" CPOs and modified IMP to use those rather than "lift"
nipkow
parents:
diff changeset
     6
*)
c2508f4ab739 Added "discrete" CPOs and modified IMP to use those rather than "lift"
nipkow
parents:
diff changeset
     7
15578
d364491ba718 add header
huffman
parents: 15555
diff changeset
     8
header {* Discrete cpo types *}
d364491ba718 add header
huffman
parents: 15555
diff changeset
     9
15555
9d4dbd18ff2d converted to new-style theory
huffman
parents: 14981
diff changeset
    10
theory Discrete
9d4dbd18ff2d converted to new-style theory
huffman
parents: 14981
diff changeset
    11
imports Cont Datatype
9d4dbd18ff2d converted to new-style theory
huffman
parents: 14981
diff changeset
    12
begin
9d4dbd18ff2d converted to new-style theory
huffman
parents: 14981
diff changeset
    13
9d4dbd18ff2d converted to new-style theory
huffman
parents: 14981
diff changeset
    14
datatype 'a discr = Discr "'a :: type"
9d4dbd18ff2d converted to new-style theory
huffman
parents: 14981
diff changeset
    15
15590
17f4f5afcd5f added subsection headings, cleaned up some proofs
huffman
parents: 15578
diff changeset
    16
subsection {* Type @{typ "'a discr"} is a partial order *}
17f4f5afcd5f added subsection headings, cleaned up some proofs
huffman
parents: 15578
diff changeset
    17
15555
9d4dbd18ff2d converted to new-style theory
huffman
parents: 14981
diff changeset
    18
instance discr :: (type) sq_ord ..
9d4dbd18ff2d converted to new-style theory
huffman
parents: 14981
diff changeset
    19
9d4dbd18ff2d converted to new-style theory
huffman
parents: 14981
diff changeset
    20
defs (overloaded)
9d4dbd18ff2d converted to new-style theory
huffman
parents: 14981
diff changeset
    21
less_discr_def: "((op <<)::('a::type)discr=>'a discr=>bool)  ==  op ="
9d4dbd18ff2d converted to new-style theory
huffman
parents: 14981
diff changeset
    22
9d4dbd18ff2d converted to new-style theory
huffman
parents: 14981
diff changeset
    23
lemma discr_less_eq [iff]: "((x::('a::type)discr) << y) = (x = y)"
15639
99ed5113783b cleaned up some proofs
huffman
parents: 15590
diff changeset
    24
by (unfold less_discr_def) (rule refl)
15555
9d4dbd18ff2d converted to new-style theory
huffman
parents: 14981
diff changeset
    25
9d4dbd18ff2d converted to new-style theory
huffman
parents: 14981
diff changeset
    26
instance discr :: (type) po
9d4dbd18ff2d converted to new-style theory
huffman
parents: 14981
diff changeset
    27
proof
9d4dbd18ff2d converted to new-style theory
huffman
parents: 14981
diff changeset
    28
  fix x y z :: "'a discr"
9d4dbd18ff2d converted to new-style theory
huffman
parents: 14981
diff changeset
    29
  show "x << x" by simp
9d4dbd18ff2d converted to new-style theory
huffman
parents: 14981
diff changeset
    30
  { assume "x << y" and "y << x" thus "x = y" by simp }
9d4dbd18ff2d converted to new-style theory
huffman
parents: 14981
diff changeset
    31
  { assume "x << y" and "y << z" thus "x << z" by simp }
9d4dbd18ff2d converted to new-style theory
huffman
parents: 14981
diff changeset
    32
qed
2841
c2508f4ab739 Added "discrete" CPOs and modified IMP to use those rather than "lift"
nipkow
parents:
diff changeset
    33
15590
17f4f5afcd5f added subsection headings, cleaned up some proofs
huffman
parents: 15578
diff changeset
    34
subsection {* Type @{typ "'a discr"} is a cpo *}
17f4f5afcd5f added subsection headings, cleaned up some proofs
huffman
parents: 15578
diff changeset
    35
15555
9d4dbd18ff2d converted to new-style theory
huffman
parents: 14981
diff changeset
    36
lemma discr_chain0: 
9d4dbd18ff2d converted to new-style theory
huffman
parents: 14981
diff changeset
    37
 "!!S::nat=>('a::type)discr. chain S ==> S i = S 0"
9d4dbd18ff2d converted to new-style theory
huffman
parents: 14981
diff changeset
    38
apply (unfold chain_def)
9d4dbd18ff2d converted to new-style theory
huffman
parents: 14981
diff changeset
    39
apply (induct_tac "i")
9d4dbd18ff2d converted to new-style theory
huffman
parents: 14981
diff changeset
    40
apply (rule refl)
9d4dbd18ff2d converted to new-style theory
huffman
parents: 14981
diff changeset
    41
apply (erule subst)
9d4dbd18ff2d converted to new-style theory
huffman
parents: 14981
diff changeset
    42
apply (rule sym)
9d4dbd18ff2d converted to new-style theory
huffman
parents: 14981
diff changeset
    43
apply fast
9d4dbd18ff2d converted to new-style theory
huffman
parents: 14981
diff changeset
    44
done
9d4dbd18ff2d converted to new-style theory
huffman
parents: 14981
diff changeset
    45
15639
99ed5113783b cleaned up some proofs
huffman
parents: 15590
diff changeset
    46
lemma discr_chain_range0 [simp]: 
15555
9d4dbd18ff2d converted to new-style theory
huffman
parents: 14981
diff changeset
    47
 "!!S::nat=>('a::type)discr. chain(S) ==> range(S) = {S 0}"
15639
99ed5113783b cleaned up some proofs
huffman
parents: 15590
diff changeset
    48
by (fast elim: discr_chain0)
15555
9d4dbd18ff2d converted to new-style theory
huffman
parents: 14981
diff changeset
    49
9d4dbd18ff2d converted to new-style theory
huffman
parents: 14981
diff changeset
    50
lemma discr_cpo: 
9d4dbd18ff2d converted to new-style theory
huffman
parents: 14981
diff changeset
    51
 "!!S. chain S ==> ? x::('a::type)discr. range(S) <<| x"
15639
99ed5113783b cleaned up some proofs
huffman
parents: 15590
diff changeset
    52
by (unfold is_lub_def is_ub_def) simp
15555
9d4dbd18ff2d converted to new-style theory
huffman
parents: 14981
diff changeset
    53
15590
17f4f5afcd5f added subsection headings, cleaned up some proofs
huffman
parents: 15578
diff changeset
    54
instance discr :: (type) cpo
17f4f5afcd5f added subsection headings, cleaned up some proofs
huffman
parents: 15578
diff changeset
    55
by intro_classes (rule discr_cpo)
17f4f5afcd5f added subsection headings, cleaned up some proofs
huffman
parents: 15578
diff changeset
    56
17f4f5afcd5f added subsection headings, cleaned up some proofs
huffman
parents: 15578
diff changeset
    57
subsection {* @{term undiscr} *}
2841
c2508f4ab739 Added "discrete" CPOs and modified IMP to use those rather than "lift"
nipkow
parents:
diff changeset
    58
c2508f4ab739 Added "discrete" CPOs and modified IMP to use those rather than "lift"
nipkow
parents:
diff changeset
    59
constdefs
15555
9d4dbd18ff2d converted to new-style theory
huffman
parents: 14981
diff changeset
    60
   undiscr :: "('a::type)discr => 'a"
2841
c2508f4ab739 Added "discrete" CPOs and modified IMP to use those rather than "lift"
nipkow
parents:
diff changeset
    61
  "undiscr x == (case x of Discr y => y)"
c2508f4ab739 Added "discrete" CPOs and modified IMP to use those rather than "lift"
nipkow
parents:
diff changeset
    62
15555
9d4dbd18ff2d converted to new-style theory
huffman
parents: 14981
diff changeset
    63
lemma undiscr_Discr [simp]: "undiscr(Discr x) = x"
15590
17f4f5afcd5f added subsection headings, cleaned up some proofs
huffman
parents: 15578
diff changeset
    64
by (simp add: undiscr_def)
15555
9d4dbd18ff2d converted to new-style theory
huffman
parents: 14981
diff changeset
    65
9d4dbd18ff2d converted to new-style theory
huffman
parents: 14981
diff changeset
    66
lemma discr_chain_f_range0:
9d4dbd18ff2d converted to new-style theory
huffman
parents: 14981
diff changeset
    67
 "!!S::nat=>('a::type)discr. chain(S) ==> range(%i. f(S i)) = {f(S 0)}"
15590
17f4f5afcd5f added subsection headings, cleaned up some proofs
huffman
parents: 15578
diff changeset
    68
by (fast dest: discr_chain0 elim: arg_cong)
15555
9d4dbd18ff2d converted to new-style theory
huffman
parents: 14981
diff changeset
    69
9d4dbd18ff2d converted to new-style theory
huffman
parents: 14981
diff changeset
    70
lemma cont_discr [iff]: "cont(%x::('a::type)discr. f x)"
16213
88ddef269510 replaced cont with cont_def
huffman
parents: 16070
diff changeset
    71
apply (unfold cont_def is_lub_def is_ub_def)
15590
17f4f5afcd5f added subsection headings, cleaned up some proofs
huffman
parents: 15578
diff changeset
    72
apply (simp add: discr_chain_f_range0)
15555
9d4dbd18ff2d converted to new-style theory
huffman
parents: 14981
diff changeset
    73
done
9d4dbd18ff2d converted to new-style theory
huffman
parents: 14981
diff changeset
    74
2841
c2508f4ab739 Added "discrete" CPOs and modified IMP to use those rather than "lift"
nipkow
parents:
diff changeset
    75
end