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