src/HOLCF/Discrete.thy
author huffman
Wed, 02 Jan 2008 18:27:07 +0100
changeset 25782 2d8b845dc298
parent 25131 2c8caac48ade
child 25827 c2adeb1bae5c
permissions -rw-r--r--
added dcpo instance proofs
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
19105
3aabd46340e0 use minimal imports
huffman
parents: 16213
diff changeset
    11
imports Cont
15555
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
25782
2d8b845dc298 added dcpo instance proofs
huffman
parents: 25131
diff changeset
    50
lemma discr_directed_lemma:
2d8b845dc298 added dcpo instance proofs
huffman
parents: 25131
diff changeset
    51
  fixes S :: "'a::type discr set"
2d8b845dc298 added dcpo instance proofs
huffman
parents: 25131
diff changeset
    52
  assumes S: "directed S"
2d8b845dc298 added dcpo instance proofs
huffman
parents: 25131
diff changeset
    53
  shows "\<exists>x. S = {x}"
2d8b845dc298 added dcpo instance proofs
huffman
parents: 25131
diff changeset
    54
proof -
2d8b845dc298 added dcpo instance proofs
huffman
parents: 25131
diff changeset
    55
  obtain x where x: "x \<in> S"
2d8b845dc298 added dcpo instance proofs
huffman
parents: 25131
diff changeset
    56
    using S by (rule directedE1)
2d8b845dc298 added dcpo instance proofs
huffman
parents: 25131
diff changeset
    57
  hence "S = {x}"
2d8b845dc298 added dcpo instance proofs
huffman
parents: 25131
diff changeset
    58
  proof (safe)
2d8b845dc298 added dcpo instance proofs
huffman
parents: 25131
diff changeset
    59
    fix y assume y: "y \<in> S"
2d8b845dc298 added dcpo instance proofs
huffman
parents: 25131
diff changeset
    60
    obtain z where "x \<sqsubseteq> z" "y \<sqsubseteq> z"
2d8b845dc298 added dcpo instance proofs
huffman
parents: 25131
diff changeset
    61
      using S x y by (rule directedE2)
2d8b845dc298 added dcpo instance proofs
huffman
parents: 25131
diff changeset
    62
    thus "y = x" by simp
2d8b845dc298 added dcpo instance proofs
huffman
parents: 25131
diff changeset
    63
  qed
2d8b845dc298 added dcpo instance proofs
huffman
parents: 25131
diff changeset
    64
  thus "\<exists>x. S = {x}" ..
2d8b845dc298 added dcpo instance proofs
huffman
parents: 25131
diff changeset
    65
qed
15555
9d4dbd18ff2d converted to new-style theory
huffman
parents: 14981
diff changeset
    66
25782
2d8b845dc298 added dcpo instance proofs
huffman
parents: 25131
diff changeset
    67
instance discr :: (type) dcpo
2d8b845dc298 added dcpo instance proofs
huffman
parents: 25131
diff changeset
    68
proof
2d8b845dc298 added dcpo instance proofs
huffman
parents: 25131
diff changeset
    69
  fix S :: "'a discr set"
2d8b845dc298 added dcpo instance proofs
huffman
parents: 25131
diff changeset
    70
  assume "directed S"
2d8b845dc298 added dcpo instance proofs
huffman
parents: 25131
diff changeset
    71
  hence "\<exists>x. S = {x}" by (rule discr_directed_lemma)
2d8b845dc298 added dcpo instance proofs
huffman
parents: 25131
diff changeset
    72
  thus "\<exists>x. S <<| x" by (fast intro: is_lub_singleton)
2d8b845dc298 added dcpo instance proofs
huffman
parents: 25131
diff changeset
    73
qed
15590
17f4f5afcd5f added subsection headings, cleaned up some proofs
huffman
parents: 15578
diff changeset
    74
17f4f5afcd5f added subsection headings, cleaned up some proofs
huffman
parents: 15578
diff changeset
    75
subsection {* @{term undiscr} *}
2841
c2508f4ab739 Added "discrete" CPOs and modified IMP to use those rather than "lift"
nipkow
parents:
diff changeset
    76
25131
2c8caac48ade modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents: 19105
diff changeset
    77
definition
2c8caac48ade modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents: 19105
diff changeset
    78
  undiscr :: "('a::type)discr => 'a" where
2c8caac48ade modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents: 19105
diff changeset
    79
  "undiscr x = (case x of Discr y => y)"
2841
c2508f4ab739 Added "discrete" CPOs and modified IMP to use those rather than "lift"
nipkow
parents:
diff changeset
    80
15555
9d4dbd18ff2d converted to new-style theory
huffman
parents: 14981
diff changeset
    81
lemma undiscr_Discr [simp]: "undiscr(Discr x) = x"
15590
17f4f5afcd5f added subsection headings, cleaned up some proofs
huffman
parents: 15578
diff changeset
    82
by (simp add: undiscr_def)
15555
9d4dbd18ff2d converted to new-style theory
huffman
parents: 14981
diff changeset
    83
9d4dbd18ff2d converted to new-style theory
huffman
parents: 14981
diff changeset
    84
lemma discr_chain_f_range0:
9d4dbd18ff2d converted to new-style theory
huffman
parents: 14981
diff changeset
    85
 "!!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
    86
by (fast dest: discr_chain0 elim: arg_cong)
15555
9d4dbd18ff2d converted to new-style theory
huffman
parents: 14981
diff changeset
    87
9d4dbd18ff2d converted to new-style theory
huffman
parents: 14981
diff changeset
    88
lemma cont_discr [iff]: "cont(%x::('a::type)discr. f x)"
16213
88ddef269510 replaced cont with cont_def
huffman
parents: 16070
diff changeset
    89
apply (unfold cont_def is_lub_def is_ub_def)
15590
17f4f5afcd5f added subsection headings, cleaned up some proofs
huffman
parents: 15578
diff changeset
    90
apply (simp add: discr_chain_f_range0)
15555
9d4dbd18ff2d converted to new-style theory
huffman
parents: 14981
diff changeset
    91
done
9d4dbd18ff2d converted to new-style theory
huffman
parents: 14981
diff changeset
    92
2841
c2508f4ab739 Added "discrete" CPOs and modified IMP to use those rather than "lift"
nipkow
parents:
diff changeset
    93
end