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