author | wenzelm |
Thu, 07 Aug 2008 22:32:03 +0200 | |
changeset 27786 | 4525c6f5d753 |
parent 27406 | 3897988917a3 |
child 28611 | 983c1855a7af |
permissions | -rw-r--r-- |
25904 | 1 |
(* Title: HOLCF/CompactBasis.thy |
2 |
ID: $Id$ |
|
3 |
Author: Brian Huffman |
|
4 |
*) |
|
5 |
||
6 |
header {* Compact bases of domains *} |
|
7 |
||
8 |
theory CompactBasis |
|
27404 | 9 |
imports Completion |
25904 | 10 |
begin |
11 |
||
12 |
subsection {* Compact bases of bifinite domains *} |
|
13 |
||
26407
562a1d615336
rename class bifinite_cpo to profinite; generalize powerdomains from bifinite to profinite
huffman
parents:
26041
diff
changeset
|
14 |
defaultsort profinite |
25904 | 15 |
|
26407
562a1d615336
rename class bifinite_cpo to profinite; generalize powerdomains from bifinite to profinite
huffman
parents:
26041
diff
changeset
|
16 |
typedef (open) 'a compact_basis = "{x::'a::profinite. compact x}" |
25904 | 17 |
by (fast intro: compact_approx) |
18 |
||
27289 | 19 |
lemma compact_Rep_compact_basis: "compact (Rep_compact_basis a)" |
26927 | 20 |
by (rule Rep_compact_basis [unfolded mem_Collect_eq]) |
25904 | 21 |
|
26420
57a626f64875
make preorder locale into a superclass of class po
huffman
parents:
26407
diff
changeset
|
22 |
instantiation compact_basis :: (profinite) sq_ord |
57a626f64875
make preorder locale into a superclass of class po
huffman
parents:
26407
diff
changeset
|
23 |
begin |
57a626f64875
make preorder locale into a superclass of class po
huffman
parents:
26407
diff
changeset
|
24 |
|
57a626f64875
make preorder locale into a superclass of class po
huffman
parents:
26407
diff
changeset
|
25 |
definition |
57a626f64875
make preorder locale into a superclass of class po
huffman
parents:
26407
diff
changeset
|
26 |
compact_le_def: |
57a626f64875
make preorder locale into a superclass of class po
huffman
parents:
26407
diff
changeset
|
27 |
"(op \<sqsubseteq>) \<equiv> (\<lambda>x y. Rep_compact_basis x \<sqsubseteq> Rep_compact_basis y)" |
57a626f64875
make preorder locale into a superclass of class po
huffman
parents:
26407
diff
changeset
|
28 |
|
57a626f64875
make preorder locale into a superclass of class po
huffman
parents:
26407
diff
changeset
|
29 |
instance .. |
57a626f64875
make preorder locale into a superclass of class po
huffman
parents:
26407
diff
changeset
|
30 |
|
57a626f64875
make preorder locale into a superclass of class po
huffman
parents:
26407
diff
changeset
|
31 |
end |
57a626f64875
make preorder locale into a superclass of class po
huffman
parents:
26407
diff
changeset
|
32 |
|
57a626f64875
make preorder locale into a superclass of class po
huffman
parents:
26407
diff
changeset
|
33 |
instance compact_basis :: (profinite) po |
57a626f64875
make preorder locale into a superclass of class po
huffman
parents:
26407
diff
changeset
|
34 |
by (rule typedef_po |
57a626f64875
make preorder locale into a superclass of class po
huffman
parents:
26407
diff
changeset
|
35 |
[OF type_definition_compact_basis compact_le_def]) |
25904 | 36 |
|
27289 | 37 |
text {* Take function for compact basis *} |
25904 | 38 |
|
39 |
definition |
|
27406 | 40 |
compact_take :: "nat \<Rightarrow> 'a compact_basis \<Rightarrow> 'a compact_basis" where |
41 |
"compact_take = (\<lambda>n a. Abs_compact_basis (approx n\<cdot>(Rep_compact_basis a)))" |
|
25904 | 42 |
|
27406 | 43 |
lemma Rep_compact_take: |
44 |
"Rep_compact_basis (compact_take n a) = approx n\<cdot>(Rep_compact_basis a)" |
|
45 |
unfolding compact_take_def |
|
25904 | 46 |
by (simp add: Abs_compact_basis_inverse) |
47 |
||
27406 | 48 |
lemmas approx_Rep_compact_basis = Rep_compact_take [symmetric] |
25904 | 49 |
|
27289 | 50 |
interpretation compact_basis: |
27406 | 51 |
basis_take [sq_le compact_take] |
27289 | 52 |
proof |
53 |
fix n :: nat and a :: "'a compact_basis" |
|
27406 | 54 |
show "compact_take n a \<sqsubseteq> a" |
27289 | 55 |
unfolding compact_le_def |
27406 | 56 |
by (simp add: Rep_compact_take approx_less) |
27289 | 57 |
next |
58 |
fix n :: nat and a :: "'a compact_basis" |
|
27406 | 59 |
show "compact_take n (compact_take n a) = compact_take n a" |
60 |
by (simp add: Rep_compact_basis_inject [symmetric] Rep_compact_take) |
|
27289 | 61 |
next |
62 |
fix n :: nat and a b :: "'a compact_basis" |
|
27406 | 63 |
assume "a \<sqsubseteq> b" thus "compact_take n a \<sqsubseteq> compact_take n b" |
64 |
unfolding compact_le_def Rep_compact_take |
|
27289 | 65 |
by (rule monofun_cfun_arg) |
66 |
next |
|
67 |
fix n :: nat and a :: "'a compact_basis" |
|
27406 | 68 |
show "\<And>n a. compact_take n a \<sqsubseteq> compact_take (Suc n) a" |
69 |
unfolding compact_le_def Rep_compact_take |
|
27289 | 70 |
by (rule chainE, simp) |
71 |
next |
|
72 |
fix n :: nat |
|
27406 | 73 |
show "finite (range (compact_take n))" |
27289 | 74 |
apply (rule finite_imageD [where f="Rep_compact_basis"]) |
75 |
apply (rule finite_subset [where B="range (\<lambda>x. approx n\<cdot>x)"]) |
|
27406 | 76 |
apply (clarsimp simp add: Rep_compact_take) |
27289 | 77 |
apply (rule finite_range_approx) |
78 |
apply (rule inj_onI, simp add: Rep_compact_basis_inject) |
|
79 |
done |
|
80 |
next |
|
81 |
fix a :: "'a compact_basis" |
|
27406 | 82 |
show "\<exists>n. compact_take n a = a" |
27289 | 83 |
apply (simp add: Rep_compact_basis_inject [symmetric]) |
27406 | 84 |
apply (simp add: Rep_compact_take) |
27309 | 85 |
apply (rule profinite_compact_eq_approx) |
27289 | 86 |
apply (rule compact_Rep_compact_basis) |
87 |
done |
|
88 |
qed |
|
25904 | 89 |
|
27289 | 90 |
text {* Ideal completion *} |
25904 | 91 |
|
27289 | 92 |
definition |
93 |
compacts :: "'a \<Rightarrow> 'a compact_basis set" where |
|
94 |
"compacts = (\<lambda>x. {a. Rep_compact_basis a \<sqsubseteq> x})" |
|
25904 | 95 |
|
96 |
interpretation compact_basis: |
|
27406 | 97 |
ideal_completion [sq_le compact_take Rep_compact_basis compacts] |
27289 | 98 |
proof |
99 |
fix w :: 'a |
|
100 |
show "preorder.ideal sq_le (compacts w)" |
|
101 |
proof (rule sq_le.idealI) |
|
102 |
show "\<exists>x. x \<in> compacts w" |
|
103 |
unfolding compacts_def |
|
104 |
apply (rule_tac x="Abs_compact_basis (approx 0\<cdot>w)" in exI) |
|
105 |
apply (simp add: Abs_compact_basis_inverse approx_less) |
|
106 |
done |
|
107 |
next |
|
108 |
fix x y :: "'a compact_basis" |
|
109 |
assume "x \<in> compacts w" "y \<in> compacts w" |
|
110 |
thus "\<exists>z \<in> compacts w. x \<sqsubseteq> z \<and> y \<sqsubseteq> z" |
|
111 |
unfolding compacts_def |
|
112 |
apply simp |
|
113 |
apply (cut_tac a=x in compact_Rep_compact_basis) |
|
114 |
apply (cut_tac a=y in compact_Rep_compact_basis) |
|
27309 | 115 |
apply (drule profinite_compact_eq_approx) |
116 |
apply (drule profinite_compact_eq_approx) |
|
27289 | 117 |
apply (clarify, rename_tac i j) |
118 |
apply (rule_tac x="Abs_compact_basis (approx (max i j)\<cdot>w)" in exI) |
|
119 |
apply (simp add: compact_le_def) |
|
120 |
apply (simp add: Abs_compact_basis_inverse approx_less) |
|
121 |
apply (erule subst, erule subst) |
|
122 |
apply (simp add: monofun_cfun chain_mono [OF chain_approx]) |
|
123 |
done |
|
124 |
next |
|
125 |
fix x y :: "'a compact_basis" |
|
126 |
assume "x \<sqsubseteq> y" "y \<in> compacts w" thus "x \<in> compacts w" |
|
127 |
unfolding compacts_def |
|
128 |
apply simp |
|
129 |
apply (simp add: compact_le_def) |
|
130 |
apply (erule (1) trans_less) |
|
131 |
done |
|
132 |
qed |
|
133 |
next |
|
27297
2c42b1505f25
removed SetPcpo.thy and cpo instance for type bool;
huffman
parents:
27289
diff
changeset
|
134 |
fix Y :: "nat \<Rightarrow> 'a" |
2c42b1505f25
removed SetPcpo.thy and cpo instance for type bool;
huffman
parents:
27289
diff
changeset
|
135 |
assume Y: "chain Y" |
2c42b1505f25
removed SetPcpo.thy and cpo instance for type bool;
huffman
parents:
27289
diff
changeset
|
136 |
show "compacts (\<Squnion>i. Y i) = (\<Union>i. compacts (Y i))" |
27289 | 137 |
unfolding compacts_def |
27297
2c42b1505f25
removed SetPcpo.thy and cpo instance for type bool;
huffman
parents:
27289
diff
changeset
|
138 |
apply safe |
2c42b1505f25
removed SetPcpo.thy and cpo instance for type bool;
huffman
parents:
27289
diff
changeset
|
139 |
apply (simp add: compactD2 [OF compact_Rep_compact_basis Y]) |
2c42b1505f25
removed SetPcpo.thy and cpo instance for type bool;
huffman
parents:
27289
diff
changeset
|
140 |
apply (erule trans_less, rule is_ub_thelub [OF Y]) |
27289 | 141 |
done |
26420
57a626f64875
make preorder locale into a superclass of class po
huffman
parents:
26407
diff
changeset
|
142 |
next |
27289 | 143 |
fix a :: "'a compact_basis" |
144 |
show "compacts (Rep_compact_basis a) = {b. b \<sqsubseteq> a}" |
|
145 |
unfolding compacts_def compact_le_def .. |
|
26420
57a626f64875
make preorder locale into a superclass of class po
huffman
parents:
26407
diff
changeset
|
146 |
next |
57a626f64875
make preorder locale into a superclass of class po
huffman
parents:
26407
diff
changeset
|
147 |
fix x y :: "'a" |
57a626f64875
make preorder locale into a superclass of class po
huffman
parents:
26407
diff
changeset
|
148 |
assume "compacts x \<subseteq> compacts y" thus "x \<sqsubseteq> y" |
27289 | 149 |
apply (subgoal_tac "(\<Squnion>i. approx i\<cdot>x) \<sqsubseteq> y", simp) |
150 |
apply (rule admD, simp, simp) |
|
151 |
apply (drule_tac c="Abs_compact_basis (approx i\<cdot>x)" in subsetD) |
|
152 |
apply (simp add: compacts_def Abs_compact_basis_inverse approx_less) |
|
153 |
apply (simp add: compacts_def Abs_compact_basis_inverse) |
|
154 |
done |
|
26420
57a626f64875
make preorder locale into a superclass of class po
huffman
parents:
26407
diff
changeset
|
155 |
qed |
25904 | 156 |
|
27289 | 157 |
text {* minimal compact element *} |
158 |
||
159 |
definition |
|
160 |
compact_bot :: "'a::bifinite compact_basis" where |
|
161 |
"compact_bot = Abs_compact_basis \<bottom>" |
|
162 |
||
163 |
lemma Rep_compact_bot: "Rep_compact_basis compact_bot = \<bottom>" |
|
164 |
unfolding compact_bot_def by (simp add: Abs_compact_basis_inverse) |
|
165 |
||
166 |
lemma compact_minimal [simp]: "compact_bot \<sqsubseteq> a" |
|
167 |
unfolding compact_le_def Rep_compact_bot by simp |
|
168 |
||
25904 | 169 |
|
170 |
subsection {* A compact basis for powerdomains *} |
|
171 |
||
172 |
typedef 'a pd_basis = |
|
26407
562a1d615336
rename class bifinite_cpo to profinite; generalize powerdomains from bifinite to profinite
huffman
parents:
26041
diff
changeset
|
173 |
"{S::'a::profinite compact_basis set. finite S \<and> S \<noteq> {}}" |
25904 | 174 |
by (rule_tac x="{arbitrary}" in exI, simp) |
175 |
||
176 |
lemma finite_Rep_pd_basis [simp]: "finite (Rep_pd_basis u)" |
|
177 |
by (insert Rep_pd_basis [of u, unfolded pd_basis_def]) simp |
|
178 |
||
179 |
lemma Rep_pd_basis_nonempty [simp]: "Rep_pd_basis u \<noteq> {}" |
|
180 |
by (insert Rep_pd_basis [of u, unfolded pd_basis_def]) simp |
|
181 |
||
182 |
text {* unit and plus *} |
|
183 |
||
184 |
definition |
|
185 |
PDUnit :: "'a compact_basis \<Rightarrow> 'a pd_basis" where |
|
186 |
"PDUnit = (\<lambda>x. Abs_pd_basis {x})" |
|
187 |
||
188 |
definition |
|
189 |
PDPlus :: "'a pd_basis \<Rightarrow> 'a pd_basis \<Rightarrow> 'a pd_basis" where |
|
190 |
"PDPlus t u = Abs_pd_basis (Rep_pd_basis t \<union> Rep_pd_basis u)" |
|
191 |
||
192 |
lemma Rep_PDUnit: |
|
193 |
"Rep_pd_basis (PDUnit x) = {x}" |
|
194 |
unfolding PDUnit_def by (rule Abs_pd_basis_inverse) (simp add: pd_basis_def) |
|
195 |
||
196 |
lemma Rep_PDPlus: |
|
197 |
"Rep_pd_basis (PDPlus u v) = Rep_pd_basis u \<union> Rep_pd_basis v" |
|
198 |
unfolding PDPlus_def by (rule Abs_pd_basis_inverse) (simp add: pd_basis_def) |
|
199 |
||
200 |
lemma PDUnit_inject [simp]: "(PDUnit a = PDUnit b) = (a = b)" |
|
201 |
unfolding Rep_pd_basis_inject [symmetric] Rep_PDUnit by simp |
|
202 |
||
203 |
lemma PDPlus_assoc: "PDPlus (PDPlus t u) v = PDPlus t (PDPlus u v)" |
|
204 |
unfolding Rep_pd_basis_inject [symmetric] Rep_PDPlus by (rule Un_assoc) |
|
205 |
||
206 |
lemma PDPlus_commute: "PDPlus t u = PDPlus u t" |
|
207 |
unfolding Rep_pd_basis_inject [symmetric] Rep_PDPlus by (rule Un_commute) |
|
208 |
||
209 |
lemma PDPlus_absorb: "PDPlus t t = t" |
|
210 |
unfolding Rep_pd_basis_inject [symmetric] Rep_PDPlus by (rule Un_absorb) |
|
211 |
||
212 |
lemma pd_basis_induct1: |
|
213 |
assumes PDUnit: "\<And>a. P (PDUnit a)" |
|
214 |
assumes PDPlus: "\<And>a t. P t \<Longrightarrow> P (PDPlus (PDUnit a) t)" |
|
215 |
shows "P x" |
|
216 |
apply (induct x, unfold pd_basis_def, clarify) |
|
217 |
apply (erule (1) finite_ne_induct) |
|
218 |
apply (cut_tac a=x in PDUnit) |
|
219 |
apply (simp add: PDUnit_def) |
|
220 |
apply (drule_tac a=x in PDPlus) |
|
221 |
apply (simp add: PDUnit_def PDPlus_def Abs_pd_basis_inverse [unfolded pd_basis_def]) |
|
222 |
done |
|
223 |
||
224 |
lemma pd_basis_induct: |
|
225 |
assumes PDUnit: "\<And>a. P (PDUnit a)" |
|
226 |
assumes PDPlus: "\<And>t u. \<lbrakk>P t; P u\<rbrakk> \<Longrightarrow> P (PDPlus t u)" |
|
227 |
shows "P x" |
|
228 |
apply (induct x rule: pd_basis_induct1) |
|
229 |
apply (rule PDUnit, erule PDPlus [OF PDUnit]) |
|
230 |
done |
|
231 |
||
232 |
text {* fold-pd *} |
|
233 |
||
234 |
definition |
|
235 |
fold_pd :: |
|
236 |
"('a compact_basis \<Rightarrow> 'b::type) \<Rightarrow> ('b \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a pd_basis \<Rightarrow> 'b" |
|
237 |
where "fold_pd g f t = fold1 f (g ` Rep_pd_basis t)" |
|
238 |
||
26927 | 239 |
lemma fold_pd_PDUnit: |
240 |
includes ab_semigroup_idem_mult f |
|
241 |
shows "fold_pd g f (PDUnit x) = g x" |
|
25904 | 242 |
unfolding fold_pd_def Rep_PDUnit by simp |
243 |
||
26927 | 244 |
lemma fold_pd_PDPlus: |
245 |
includes ab_semigroup_idem_mult f |
|
246 |
shows "fold_pd g f (PDPlus t u) = f (fold_pd g f t) (fold_pd g f u)" |
|
25904 | 247 |
unfolding fold_pd_def Rep_PDPlus by (simp add: image_Un fold1_Un2) |
248 |
||
27405 | 249 |
text {* Take function for powerdomain basis *} |
25904 | 250 |
|
251 |
definition |
|
27405 | 252 |
pd_take :: "nat \<Rightarrow> 'a pd_basis \<Rightarrow> 'a pd_basis" where |
27406 | 253 |
"pd_take n = (\<lambda>t. Abs_pd_basis (compact_take n ` Rep_pd_basis t))" |
25904 | 254 |
|
27405 | 255 |
lemma Rep_pd_take: |
27406 | 256 |
"Rep_pd_basis (pd_take n t) = compact_take n ` Rep_pd_basis t" |
27405 | 257 |
unfolding pd_take_def |
25904 | 258 |
apply (rule Abs_pd_basis_inverse) |
259 |
apply (simp add: pd_basis_def) |
|
260 |
done |
|
261 |
||
27405 | 262 |
lemma pd_take_simps [simp]: |
27406 | 263 |
"pd_take n (PDUnit a) = PDUnit (compact_take n a)" |
27405 | 264 |
"pd_take n (PDPlus t u) = PDPlus (pd_take n t) (pd_take n u)" |
25904 | 265 |
apply (simp_all add: Rep_pd_basis_inject [symmetric]) |
27405 | 266 |
apply (simp_all add: Rep_pd_take Rep_PDUnit Rep_PDPlus image_Un) |
25904 | 267 |
done |
268 |
||
27405 | 269 |
lemma pd_take_idem: "pd_take n (pd_take n t) = pd_take n t" |
25904 | 270 |
apply (induct t rule: pd_basis_induct) |
27289 | 271 |
apply (simp add: compact_basis.take_take) |
25904 | 272 |
apply simp |
273 |
done |
|
274 |
||
27405 | 275 |
lemma finite_range_pd_take: "finite (range (pd_take n))" |
27289 | 276 |
apply (rule finite_imageD [where f="Rep_pd_basis"]) |
27406 | 277 |
apply (rule finite_subset [where B="Pow (range (compact_take n))"]) |
27405 | 278 |
apply (clarsimp simp add: Rep_pd_take) |
27289 | 279 |
apply (simp add: compact_basis.finite_range_take) |
25904 | 280 |
apply (rule inj_onI, simp add: Rep_pd_basis_inject) |
281 |
done |
|
282 |
||
27405 | 283 |
lemma pd_take_covers: "\<exists>n. pd_take n t = t" |
284 |
apply (subgoal_tac "\<exists>n. \<forall>m\<ge>n. pd_take m t = t", fast) |
|
25904 | 285 |
apply (induct t rule: pd_basis_induct) |
27289 | 286 |
apply (cut_tac a=a in compact_basis.take_covers) |
25904 | 287 |
apply (clarify, rule_tac x=n in exI) |
288 |
apply (clarify, simp) |
|
26420
57a626f64875
make preorder locale into a superclass of class po
huffman
parents:
26407
diff
changeset
|
289 |
apply (rule antisym_less) |
27289 | 290 |
apply (rule compact_basis.take_less) |
291 |
apply (drule_tac a=a in compact_basis.take_chain_le) |
|
25904 | 292 |
apply simp |
293 |
apply (clarify, rename_tac i j) |
|
294 |
apply (rule_tac x="max i j" in exI, simp) |
|
295 |
done |
|
296 |
||
297 |
end |