author | huffman |
Thu, 17 Jan 2008 00:51:20 +0100 | |
changeset 25921 | 0ca392ab7f37 |
parent 25906 | 2179c6661218 |
child 26025 | ca6876116bb4 |
permissions | -rw-r--r-- |
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 | 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 | 8 |
header {* Discrete cpo types *} |
9 |
||
15555 | 10 |
theory Discrete |
19105 | 11 |
imports Cont |
15555 | 12 |
begin |
13 |
||
14 |
datatype 'a discr = Discr "'a :: type" |
|
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 |
|
25902 | 18 |
instantiation discr :: (type) po |
19 |
begin |
|
15555 | 20 |
|
25902 | 21 |
definition |
22 |
less_discr_def [simp]: |
|
23 |
"(op \<sqsubseteq> :: 'a discr \<Rightarrow> 'a discr \<Rightarrow> bool) = (op =)" |
|
15555 | 24 |
|
25902 | 25 |
instance |
15555 | 26 |
proof |
27 |
fix x y z :: "'a discr" |
|
28 |
show "x << x" by simp |
|
29 |
{ assume "x << y" and "y << x" thus "x = y" by simp } |
|
30 |
{ assume "x << y" and "y << z" thus "x << z" by simp } |
|
31 |
qed |
|
2841
c2508f4ab739
Added "discrete" CPOs and modified IMP to use those rather than "lift"
nipkow
parents:
diff
changeset
|
32 |
|
25902 | 33 |
end |
34 |
||
35 |
lemma discr_less_eq [iff]: "((x::('a::type)discr) << y) = (x = y)" |
|
36 |
by simp |
|
37 |
||
15590
17f4f5afcd5f
added subsection headings, cleaned up some proofs
huffman
parents:
15578
diff
changeset
|
38 |
subsection {* Type @{typ "'a discr"} is a cpo *} |
17f4f5afcd5f
added subsection headings, cleaned up some proofs
huffman
parents:
15578
diff
changeset
|
39 |
|
15555 | 40 |
lemma discr_chain0: |
41 |
"!!S::nat=>('a::type)discr. chain S ==> S i = S 0" |
|
42 |
apply (unfold chain_def) |
|
43 |
apply (induct_tac "i") |
|
44 |
apply (rule refl) |
|
45 |
apply (erule subst) |
|
46 |
apply (rule sym) |
|
47 |
apply fast |
|
48 |
done |
|
49 |
||
15639 | 50 |
lemma discr_chain_range0 [simp]: |
15555 | 51 |
"!!S::nat=>('a::type)discr. chain(S) ==> range(S) = {S 0}" |
15639 | 52 |
by (fast elim: discr_chain0) |
15555 | 53 |
|
25827
c2adeb1bae5c
new instance proofs for classes finite_po, chfin, flat
huffman
parents:
25782
diff
changeset
|
54 |
instance discr :: (finite) finite_po |
c2adeb1bae5c
new instance proofs for classes finite_po, chfin, flat
huffman
parents:
25782
diff
changeset
|
55 |
proof |
c2adeb1bae5c
new instance proofs for classes finite_po, chfin, flat
huffman
parents:
25782
diff
changeset
|
56 |
have "finite (Discr ` (UNIV :: 'a set))" |
c2adeb1bae5c
new instance proofs for classes finite_po, chfin, flat
huffman
parents:
25782
diff
changeset
|
57 |
by (rule finite_imageI [OF finite]) |
c2adeb1bae5c
new instance proofs for classes finite_po, chfin, flat
huffman
parents:
25782
diff
changeset
|
58 |
also have "(Discr ` (UNIV :: 'a set)) = UNIV" |
c2adeb1bae5c
new instance proofs for classes finite_po, chfin, flat
huffman
parents:
25782
diff
changeset
|
59 |
by (auto, case_tac x, auto) |
c2adeb1bae5c
new instance proofs for classes finite_po, chfin, flat
huffman
parents:
25782
diff
changeset
|
60 |
finally show "finite (UNIV :: 'a discr set)" . |
c2adeb1bae5c
new instance proofs for classes finite_po, chfin, flat
huffman
parents:
25782
diff
changeset
|
61 |
qed |
c2adeb1bae5c
new instance proofs for classes finite_po, chfin, flat
huffman
parents:
25782
diff
changeset
|
62 |
|
c2adeb1bae5c
new instance proofs for classes finite_po, chfin, flat
huffman
parents:
25782
diff
changeset
|
63 |
instance discr :: (type) chfin |
25921 | 64 |
apply intro_classes |
25827
c2adeb1bae5c
new instance proofs for classes finite_po, chfin, flat
huffman
parents:
25782
diff
changeset
|
65 |
apply (rule_tac x=0 in exI) |
c2adeb1bae5c
new instance proofs for classes finite_po, chfin, flat
huffman
parents:
25782
diff
changeset
|
66 |
apply (unfold max_in_chain_def) |
c2adeb1bae5c
new instance proofs for classes finite_po, chfin, flat
huffman
parents:
25782
diff
changeset
|
67 |
apply (clarify, erule discr_chain0 [symmetric]) |
c2adeb1bae5c
new instance proofs for classes finite_po, chfin, flat
huffman
parents:
25782
diff
changeset
|
68 |
done |
c2adeb1bae5c
new instance proofs for classes finite_po, chfin, flat
huffman
parents:
25782
diff
changeset
|
69 |
|
15590
17f4f5afcd5f
added subsection headings, cleaned up some proofs
huffman
parents:
15578
diff
changeset
|
70 |
subsection {* @{term undiscr} *} |
2841
c2508f4ab739
Added "discrete" CPOs and modified IMP to use those rather than "lift"
nipkow
parents:
diff
changeset
|
71 |
|
25131
2c8caac48ade
modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents:
19105
diff
changeset
|
72 |
definition |
2c8caac48ade
modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents:
19105
diff
changeset
|
73 |
undiscr :: "('a::type)discr => 'a" where |
2c8caac48ade
modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents:
19105
diff
changeset
|
74 |
"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
|
75 |
|
15555 | 76 |
lemma undiscr_Discr [simp]: "undiscr(Discr x) = x" |
15590
17f4f5afcd5f
added subsection headings, cleaned up some proofs
huffman
parents:
15578
diff
changeset
|
77 |
by (simp add: undiscr_def) |
15555 | 78 |
|
79 |
lemma discr_chain_f_range0: |
|
80 |
"!!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
|
81 |
by (fast dest: discr_chain0 elim: arg_cong) |
15555 | 82 |
|
25827
c2adeb1bae5c
new instance proofs for classes finite_po, chfin, flat
huffman
parents:
25782
diff
changeset
|
83 |
lemma cont_discr [iff]: "cont (%x::('a::type)discr. f x)" |
c2adeb1bae5c
new instance proofs for classes finite_po, chfin, flat
huffman
parents:
25782
diff
changeset
|
84 |
apply (rule chfindom_monofun2cont) |
c2adeb1bae5c
new instance proofs for classes finite_po, chfin, flat
huffman
parents:
25782
diff
changeset
|
85 |
apply (rule monofunI, simp) |
15555 | 86 |
done |
87 |
||
2841
c2508f4ab739
Added "discrete" CPOs and modified IMP to use those rather than "lift"
nipkow
parents:
diff
changeset
|
88 |
end |