1 (* Title: HOLCF/Library/Defl_Bifinite.thy |
|
2 Author: Brian Huffman |
|
3 *) |
|
4 |
|
5 header {* Algebraic deflations are a bifinite domain *} |
|
6 |
|
7 theory Defl_Bifinite |
|
8 imports HOLCF Infinite_Set |
|
9 begin |
|
10 |
|
11 subsection {* Lemmas about MOST *} |
|
12 |
|
13 default_sort type |
|
14 |
|
15 lemma MOST_INFM: |
|
16 assumes inf: "infinite (UNIV::'a set)" |
|
17 shows "MOST x::'a. P x \<Longrightarrow> INFM x::'a. P x" |
|
18 unfolding Alm_all_def Inf_many_def |
|
19 apply (auto simp add: Collect_neg_eq) |
|
20 apply (drule (1) finite_UnI) |
|
21 apply (simp add: Compl_partition2 inf) |
|
22 done |
|
23 |
|
24 lemma MOST_SucI: "MOST n. P n \<Longrightarrow> MOST n. P (Suc n)" |
|
25 by (rule MOST_inj [OF _ inj_Suc]) |
|
26 |
|
27 lemma MOST_SucD: "MOST n. P (Suc n) \<Longrightarrow> MOST n. P n" |
|
28 unfolding MOST_nat |
|
29 apply (clarify, rule_tac x="Suc m" in exI, clarify) |
|
30 apply (erule Suc_lessE, simp) |
|
31 done |
|
32 |
|
33 lemma MOST_Suc_iff: "(MOST n. P (Suc n)) \<longleftrightarrow> (MOST n. P n)" |
|
34 by (rule iffI [OF MOST_SucD MOST_SucI]) |
|
35 |
|
36 lemma INFM_finite_Bex_distrib: |
|
37 "finite A \<Longrightarrow> (INFM y. \<exists>x\<in>A. P x y) \<longleftrightarrow> (\<exists>x\<in>A. INFM y. P x y)" |
|
38 by (induct set: finite, simp, simp add: INFM_disj_distrib) |
|
39 |
|
40 lemma MOST_finite_Ball_distrib: |
|
41 "finite A \<Longrightarrow> (MOST y. \<forall>x\<in>A. P x y) \<longleftrightarrow> (\<forall>x\<in>A. MOST y. P x y)" |
|
42 by (induct set: finite, simp, simp add: MOST_conj_distrib) |
|
43 |
|
44 lemma MOST_ge_nat: "MOST n::nat. m \<le> n" |
|
45 unfolding MOST_nat_le by fast |
|
46 |
|
47 subsection {* Eventually constant sequences *} |
|
48 |
|
49 definition |
|
50 eventually_constant :: "(nat \<Rightarrow> 'a) \<Rightarrow> bool" |
|
51 where |
|
52 "eventually_constant S = (\<exists>x. MOST i. S i = x)" |
|
53 |
|
54 lemma eventually_constant_MOST_MOST: |
|
55 "eventually_constant S \<longleftrightarrow> (MOST m. MOST n. S n = S m)" |
|
56 unfolding eventually_constant_def MOST_nat |
|
57 apply safe |
|
58 apply (rule_tac x=m in exI, clarify) |
|
59 apply (rule_tac x=m in exI, clarify) |
|
60 apply simp |
|
61 apply fast |
|
62 done |
|
63 |
|
64 lemma eventually_constantI: "MOST i. S i = x \<Longrightarrow> eventually_constant S" |
|
65 unfolding eventually_constant_def by fast |
|
66 |
|
67 lemma eventually_constant_comp: |
|
68 "eventually_constant (\<lambda>i. S i) \<Longrightarrow> eventually_constant (\<lambda>i. f (S i))" |
|
69 unfolding eventually_constant_def |
|
70 apply (erule exE, rule_tac x="f x" in exI) |
|
71 apply (erule MOST_mono, simp) |
|
72 done |
|
73 |
|
74 lemma eventually_constant_Suc_iff: |
|
75 "eventually_constant (\<lambda>i. S (Suc i)) \<longleftrightarrow> eventually_constant (\<lambda>i. S i)" |
|
76 unfolding eventually_constant_def |
|
77 by (subst MOST_Suc_iff, rule refl) |
|
78 |
|
79 lemma eventually_constant_SucD: |
|
80 "eventually_constant (\<lambda>i. S (Suc i)) \<Longrightarrow> eventually_constant (\<lambda>i. S i)" |
|
81 by (rule eventually_constant_Suc_iff [THEN iffD1]) |
|
82 |
|
83 subsection {* Limits of eventually constant sequences *} |
|
84 |
|
85 definition |
|
86 eventual :: "(nat \<Rightarrow> 'a) \<Rightarrow> 'a" where |
|
87 "eventual S = (THE x. MOST i. S i = x)" |
|
88 |
|
89 lemma eventual_eqI: "MOST i. S i = x \<Longrightarrow> eventual S = x" |
|
90 unfolding eventual_def |
|
91 apply (rule the_equality, assumption) |
|
92 apply (rename_tac y) |
|
93 apply (subgoal_tac "MOST i::nat. y = x", simp) |
|
94 apply (erule MOST_rev_mp) |
|
95 apply (erule MOST_rev_mp) |
|
96 apply simp |
|
97 done |
|
98 |
|
99 lemma MOST_eq_eventual: |
|
100 "eventually_constant S \<Longrightarrow> MOST i. S i = eventual S" |
|
101 unfolding eventually_constant_def |
|
102 by (erule exE, simp add: eventual_eqI) |
|
103 |
|
104 lemma eventual_mem_range: |
|
105 "eventually_constant S \<Longrightarrow> eventual S \<in> range S" |
|
106 apply (drule MOST_eq_eventual) |
|
107 apply (simp only: MOST_nat_le, clarify) |
|
108 apply (drule spec, drule mp, rule order_refl) |
|
109 apply (erule range_eqI [OF sym]) |
|
110 done |
|
111 |
|
112 lemma eventually_constant_MOST_iff: |
|
113 assumes S: "eventually_constant S" |
|
114 shows "(MOST n. P (S n)) \<longleftrightarrow> P (eventual S)" |
|
115 apply (subgoal_tac "(MOST n. P (S n)) \<longleftrightarrow> (MOST n::nat. P (eventual S))") |
|
116 apply simp |
|
117 apply (rule iffI) |
|
118 apply (rule MOST_rev_mp [OF MOST_eq_eventual [OF S]]) |
|
119 apply (erule MOST_mono, force) |
|
120 apply (rule MOST_rev_mp [OF MOST_eq_eventual [OF S]]) |
|
121 apply (erule MOST_mono, simp) |
|
122 done |
|
123 |
|
124 lemma MOST_eventual: |
|
125 "\<lbrakk>eventually_constant S; MOST n. P (S n)\<rbrakk> \<Longrightarrow> P (eventual S)" |
|
126 proof - |
|
127 assume "eventually_constant S" |
|
128 hence "MOST n. S n = eventual S" |
|
129 by (rule MOST_eq_eventual) |
|
130 moreover assume "MOST n. P (S n)" |
|
131 ultimately have "MOST n. S n = eventual S \<and> P (S n)" |
|
132 by (rule MOST_conj_distrib [THEN iffD2, OF conjI]) |
|
133 hence "MOST n::nat. P (eventual S)" |
|
134 by (rule MOST_mono) auto |
|
135 thus ?thesis by simp |
|
136 qed |
|
137 |
|
138 lemma eventually_constant_MOST_Suc_eq: |
|
139 "eventually_constant S \<Longrightarrow> MOST n. S (Suc n) = S n" |
|
140 apply (drule MOST_eq_eventual) |
|
141 apply (frule MOST_Suc_iff [THEN iffD2]) |
|
142 apply (erule MOST_rev_mp) |
|
143 apply (erule MOST_rev_mp) |
|
144 apply simp |
|
145 done |
|
146 |
|
147 lemma eventual_comp: |
|
148 "eventually_constant S \<Longrightarrow> eventual (\<lambda>i. f (S i)) = f (eventual (\<lambda>i. S i))" |
|
149 apply (rule eventual_eqI) |
|
150 apply (rule MOST_mono) |
|
151 apply (erule MOST_eq_eventual) |
|
152 apply simp |
|
153 done |
|
154 |
|
155 subsection {* Constructing finite deflations by iteration *} |
|
156 |
|
157 default_sort cpo |
|
158 |
|
159 lemma le_Suc_induct: |
|
160 assumes le: "i \<le> j" |
|
161 assumes step: "\<And>i. P i (Suc i)" |
|
162 assumes refl: "\<And>i. P i i" |
|
163 assumes trans: "\<And>i j k. \<lbrakk>P i j; P j k\<rbrakk> \<Longrightarrow> P i k" |
|
164 shows "P i j" |
|
165 proof (cases "i = j") |
|
166 assume "i = j" |
|
167 thus "P i j" by (simp add: refl) |
|
168 next |
|
169 assume "i \<noteq> j" |
|
170 with le have "i < j" by simp |
|
171 thus "P i j" using step trans by (rule less_Suc_induct) |
|
172 qed |
|
173 |
|
174 definition |
|
175 eventual_iterate :: "('a \<rightarrow> 'a::cpo) \<Rightarrow> ('a \<rightarrow> 'a)" |
|
176 where |
|
177 "eventual_iterate f = eventual (\<lambda>n. iterate n\<cdot>f)" |
|
178 |
|
179 text {* A pre-deflation is like a deflation, but not idempotent. *} |
|
180 |
|
181 locale pre_deflation = |
|
182 fixes f :: "'a \<rightarrow> 'a::cpo" |
|
183 assumes below: "\<And>x. f\<cdot>x \<sqsubseteq> x" |
|
184 assumes finite_range: "finite (range (\<lambda>x. f\<cdot>x))" |
|
185 begin |
|
186 |
|
187 lemma iterate_below: "iterate i\<cdot>f\<cdot>x \<sqsubseteq> x" |
|
188 by (induct i, simp_all add: below_trans [OF below]) |
|
189 |
|
190 lemma iterate_fixed: "f\<cdot>x = x \<Longrightarrow> iterate i\<cdot>f\<cdot>x = x" |
|
191 by (induct i, simp_all) |
|
192 |
|
193 lemma antichain_iterate_app: "i \<le> j \<Longrightarrow> iterate j\<cdot>f\<cdot>x \<sqsubseteq> iterate i\<cdot>f\<cdot>x" |
|
194 apply (erule le_Suc_induct) |
|
195 apply (simp add: below) |
|
196 apply (rule below_refl) |
|
197 apply (erule (1) below_trans) |
|
198 done |
|
199 |
|
200 lemma finite_range_iterate_app: "finite (range (\<lambda>i. iterate i\<cdot>f\<cdot>x))" |
|
201 proof (rule finite_subset) |
|
202 show "range (\<lambda>i. iterate i\<cdot>f\<cdot>x) \<subseteq> insert x (range (\<lambda>x. f\<cdot>x))" |
|
203 by (clarify, case_tac i, simp_all) |
|
204 show "finite (insert x (range (\<lambda>x. f\<cdot>x)))" |
|
205 by (simp add: finite_range) |
|
206 qed |
|
207 |
|
208 lemma eventually_constant_iterate_app: |
|
209 "eventually_constant (\<lambda>i. iterate i\<cdot>f\<cdot>x)" |
|
210 unfolding eventually_constant_def MOST_nat_le |
|
211 proof - |
|
212 let ?Y = "\<lambda>i. iterate i\<cdot>f\<cdot>x" |
|
213 have "\<exists>j. \<forall>k. ?Y j \<sqsubseteq> ?Y k" |
|
214 apply (rule finite_range_has_max) |
|
215 apply (erule antichain_iterate_app) |
|
216 apply (rule finite_range_iterate_app) |
|
217 done |
|
218 then obtain j where j: "\<And>k. ?Y j \<sqsubseteq> ?Y k" by fast |
|
219 show "\<exists>z m. \<forall>n\<ge>m. ?Y n = z" |
|
220 proof (intro exI allI impI) |
|
221 fix k |
|
222 assume "j \<le> k" |
|
223 hence "?Y k \<sqsubseteq> ?Y j" by (rule antichain_iterate_app) |
|
224 also have "?Y j \<sqsubseteq> ?Y k" by (rule j) |
|
225 finally show "?Y k = ?Y j" . |
|
226 qed |
|
227 qed |
|
228 |
|
229 lemma eventually_constant_iterate: |
|
230 "eventually_constant (\<lambda>n. iterate n\<cdot>f)" |
|
231 proof - |
|
232 have "\<forall>y\<in>range (\<lambda>x. f\<cdot>x). eventually_constant (\<lambda>i. iterate i\<cdot>f\<cdot>y)" |
|
233 by (simp add: eventually_constant_iterate_app) |
|
234 hence "\<forall>y\<in>range (\<lambda>x. f\<cdot>x). MOST i. MOST j. iterate j\<cdot>f\<cdot>y = iterate i\<cdot>f\<cdot>y" |
|
235 unfolding eventually_constant_MOST_MOST . |
|
236 hence "MOST i. MOST j. \<forall>y\<in>range (\<lambda>x. f\<cdot>x). iterate j\<cdot>f\<cdot>y = iterate i\<cdot>f\<cdot>y" |
|
237 by (simp only: MOST_finite_Ball_distrib [OF finite_range]) |
|
238 hence "MOST i. MOST j. \<forall>x. iterate j\<cdot>f\<cdot>(f\<cdot>x) = iterate i\<cdot>f\<cdot>(f\<cdot>x)" |
|
239 by simp |
|
240 hence "MOST i. MOST j. \<forall>x. iterate (Suc j)\<cdot>f\<cdot>x = iterate (Suc i)\<cdot>f\<cdot>x" |
|
241 by (simp only: iterate_Suc2) |
|
242 hence "MOST i. MOST j. iterate (Suc j)\<cdot>f = iterate (Suc i)\<cdot>f" |
|
243 by (simp only: cfun_eq_iff) |
|
244 hence "eventually_constant (\<lambda>i. iterate (Suc i)\<cdot>f)" |
|
245 unfolding eventually_constant_MOST_MOST . |
|
246 thus "eventually_constant (\<lambda>i. iterate i\<cdot>f)" |
|
247 by (rule eventually_constant_SucD) |
|
248 qed |
|
249 |
|
250 abbreviation |
|
251 d :: "'a \<rightarrow> 'a" |
|
252 where |
|
253 "d \<equiv> eventual_iterate f" |
|
254 |
|
255 lemma MOST_d: "MOST n. P (iterate n\<cdot>f) \<Longrightarrow> P d" |
|
256 unfolding eventual_iterate_def |
|
257 using eventually_constant_iterate by (rule MOST_eventual) |
|
258 |
|
259 lemma f_d: "f\<cdot>(d\<cdot>x) = d\<cdot>x" |
|
260 apply (rule MOST_d) |
|
261 apply (subst iterate_Suc [symmetric]) |
|
262 apply (rule eventually_constant_MOST_Suc_eq) |
|
263 apply (rule eventually_constant_iterate_app) |
|
264 done |
|
265 |
|
266 lemma d_fixed_iff: "d\<cdot>x = x \<longleftrightarrow> f\<cdot>x = x" |
|
267 proof |
|
268 assume "d\<cdot>x = x" |
|
269 with f_d [where x=x] |
|
270 show "f\<cdot>x = x" by simp |
|
271 next |
|
272 assume f: "f\<cdot>x = x" |
|
273 have "\<forall>n. iterate n\<cdot>f\<cdot>x = x" |
|
274 by (rule allI, rule nat.induct, simp, simp add: f) |
|
275 hence "MOST n. iterate n\<cdot>f\<cdot>x = x" |
|
276 by (rule ALL_MOST) |
|
277 thus "d\<cdot>x = x" |
|
278 by (rule MOST_d) |
|
279 qed |
|
280 |
|
281 lemma finite_deflation_d: "finite_deflation d" |
|
282 proof |
|
283 fix x :: 'a |
|
284 have "d \<in> range (\<lambda>n. iterate n\<cdot>f)" |
|
285 unfolding eventual_iterate_def |
|
286 using eventually_constant_iterate |
|
287 by (rule eventual_mem_range) |
|
288 then obtain n where n: "d = iterate n\<cdot>f" .. |
|
289 have "iterate n\<cdot>f\<cdot>(d\<cdot>x) = d\<cdot>x" |
|
290 using f_d by (rule iterate_fixed) |
|
291 thus "d\<cdot>(d\<cdot>x) = d\<cdot>x" |
|
292 by (simp add: n) |
|
293 next |
|
294 fix x :: 'a |
|
295 show "d\<cdot>x \<sqsubseteq> x" |
|
296 by (rule MOST_d, simp add: iterate_below) |
|
297 next |
|
298 from finite_range |
|
299 have "finite {x. f\<cdot>x = x}" |
|
300 by (rule finite_range_imp_finite_fixes) |
|
301 thus "finite {x. d\<cdot>x = x}" |
|
302 by (simp add: d_fixed_iff) |
|
303 qed |
|
304 |
|
305 lemma deflation_d: "deflation d" |
|
306 using finite_deflation_d |
|
307 by (rule finite_deflation_imp_deflation) |
|
308 |
|
309 end |
|
310 |
|
311 lemma finite_deflation_eventual_iterate: |
|
312 "pre_deflation d \<Longrightarrow> finite_deflation (eventual_iterate d)" |
|
313 by (rule pre_deflation.finite_deflation_d) |
|
314 |
|
315 lemma pre_deflation_oo: |
|
316 assumes "finite_deflation d" |
|
317 assumes f: "\<And>x. f\<cdot>x \<sqsubseteq> x" |
|
318 shows "pre_deflation (d oo f)" |
|
319 proof |
|
320 interpret d: finite_deflation d by fact |
|
321 fix x |
|
322 show "\<And>x. (d oo f)\<cdot>x \<sqsubseteq> x" |
|
323 by (simp, rule below_trans [OF d.below f]) |
|
324 show "finite (range (\<lambda>x. (d oo f)\<cdot>x))" |
|
325 by (rule finite_subset [OF _ d.finite_range], auto) |
|
326 qed |
|
327 |
|
328 lemma eventual_iterate_oo_fixed_iff: |
|
329 assumes "finite_deflation d" |
|
330 assumes f: "\<And>x. f\<cdot>x \<sqsubseteq> x" |
|
331 shows "eventual_iterate (d oo f)\<cdot>x = x \<longleftrightarrow> d\<cdot>x = x \<and> f\<cdot>x = x" |
|
332 proof - |
|
333 interpret d: finite_deflation d by fact |
|
334 let ?e = "d oo f" |
|
335 interpret e: pre_deflation "d oo f" |
|
336 using `finite_deflation d` f |
|
337 by (rule pre_deflation_oo) |
|
338 let ?g = "eventual (\<lambda>n. iterate n\<cdot>?e)" |
|
339 show ?thesis |
|
340 apply (subst e.d_fixed_iff) |
|
341 apply simp |
|
342 apply safe |
|
343 apply (erule subst) |
|
344 apply (rule d.idem) |
|
345 apply (rule below_antisym) |
|
346 apply (rule f) |
|
347 apply (erule subst, rule d.below) |
|
348 apply simp |
|
349 done |
|
350 qed |
|
351 |
|
352 lemma eventual_mono: |
|
353 assumes A: "eventually_constant A" |
|
354 assumes B: "eventually_constant B" |
|
355 assumes below: "\<And>n. A n \<sqsubseteq> B n" |
|
356 shows "eventual A \<sqsubseteq> eventual B" |
|
357 proof - |
|
358 from A have "MOST n. A n = eventual A" |
|
359 by (rule MOST_eq_eventual) |
|
360 then have "MOST n. eventual A \<sqsubseteq> B n" |
|
361 by (rule MOST_mono) (erule subst, rule below) |
|
362 with B show "eventual A \<sqsubseteq> eventual B" |
|
363 by (rule MOST_eventual) |
|
364 qed |
|
365 |
|
366 lemma eventual_iterate_mono: |
|
367 assumes f: "pre_deflation f" and g: "pre_deflation g" and "f \<sqsubseteq> g" |
|
368 shows "eventual_iterate f \<sqsubseteq> eventual_iterate g" |
|
369 unfolding eventual_iterate_def |
|
370 apply (rule eventual_mono) |
|
371 apply (rule pre_deflation.eventually_constant_iterate [OF f]) |
|
372 apply (rule pre_deflation.eventually_constant_iterate [OF g]) |
|
373 apply (rule monofun_cfun_arg [OF `f \<sqsubseteq> g`]) |
|
374 done |
|
375 |
|
376 lemma cont2cont_eventual_iterate_oo: |
|
377 assumes d: "finite_deflation d" |
|
378 assumes cont: "cont f" and below: "\<And>x y. f x\<cdot>y \<sqsubseteq> y" |
|
379 shows "cont (\<lambda>x. eventual_iterate (d oo f x))" |
|
380 (is "cont ?e") |
|
381 proof (rule contI2) |
|
382 show "monofun ?e" |
|
383 apply (rule monofunI) |
|
384 apply (rule eventual_iterate_mono) |
|
385 apply (rule pre_deflation_oo [OF d below]) |
|
386 apply (rule pre_deflation_oo [OF d below]) |
|
387 apply (rule monofun_cfun_arg) |
|
388 apply (erule cont2monofunE [OF cont]) |
|
389 done |
|
390 next |
|
391 fix Y :: "nat \<Rightarrow> 'b" |
|
392 assume Y: "chain Y" |
|
393 with cont have fY: "chain (\<lambda>i. f (Y i))" |
|
394 by (rule ch2ch_cont) |
|
395 assume eY: "chain (\<lambda>i. ?e (Y i))" |
|
396 have lub_below: "\<And>x. f (\<Squnion>i. Y i)\<cdot>x \<sqsubseteq> x" |
|
397 by (rule admD [OF _ Y], simp add: cont, rule below) |
|
398 have "deflation (?e (\<Squnion>i. Y i))" |
|
399 apply (rule pre_deflation.deflation_d) |
|
400 apply (rule pre_deflation_oo [OF d lub_below]) |
|
401 done |
|
402 then show "?e (\<Squnion>i. Y i) \<sqsubseteq> (\<Squnion>i. ?e (Y i))" |
|
403 proof (rule deflation.belowI) |
|
404 fix x :: 'a |
|
405 assume "?e (\<Squnion>i. Y i)\<cdot>x = x" |
|
406 hence "d\<cdot>x = x" and "f (\<Squnion>i. Y i)\<cdot>x = x" |
|
407 by (simp_all add: eventual_iterate_oo_fixed_iff [OF d lub_below]) |
|
408 hence "(\<Squnion>i. f (Y i)\<cdot>x) = x" |
|
409 apply (simp only: cont2contlubE [OF cont Y]) |
|
410 apply (simp only: contlub_cfun_fun [OF fY]) |
|
411 done |
|
412 have "compact (d\<cdot>x)" |
|
413 using d by (rule finite_deflation.compact) |
|
414 then have "compact x" |
|
415 using `d\<cdot>x = x` by simp |
|
416 then have "compact (\<Squnion>i. f (Y i)\<cdot>x)" |
|
417 using `(\<Squnion>i. f (Y i)\<cdot>x) = x` by simp |
|
418 then have "\<exists>n. max_in_chain n (\<lambda>i. f (Y i)\<cdot>x)" |
|
419 by - (rule compact_imp_max_in_chain, simp add: fY, assumption) |
|
420 then obtain n where n: "max_in_chain n (\<lambda>i. f (Y i)\<cdot>x)" .. |
|
421 then have "f (Y n)\<cdot>x = x" |
|
422 using `(\<Squnion>i. f (Y i)\<cdot>x) = x` fY by (simp add: maxinch_is_thelub) |
|
423 with `d\<cdot>x = x` have "?e (Y n)\<cdot>x = x" |
|
424 by (simp add: eventual_iterate_oo_fixed_iff [OF d below]) |
|
425 moreover have "?e (Y n)\<cdot>x \<sqsubseteq> (\<Squnion>i. ?e (Y i)\<cdot>x)" |
|
426 by (rule is_ub_thelub, simp add: eY) |
|
427 ultimately have "x \<sqsubseteq> (\<Squnion>i. ?e (Y i))\<cdot>x" |
|
428 by (simp add: contlub_cfun_fun eY) |
|
429 also have "(\<Squnion>i. ?e (Y i))\<cdot>x \<sqsubseteq> x" |
|
430 apply (rule deflation.below) |
|
431 apply (rule admD [OF adm_deflation eY]) |
|
432 apply (rule pre_deflation.deflation_d) |
|
433 apply (rule pre_deflation_oo [OF d below]) |
|
434 done |
|
435 finally show "(\<Squnion>i. ?e (Y i))\<cdot>x = x" .. |
|
436 qed |
|
437 qed |
|
438 |
|
439 subsection {* Take function for finite deflations *} |
|
440 |
|
441 definition |
|
442 defl_take :: "nat \<Rightarrow> (udom \<rightarrow> udom) \<Rightarrow> (udom \<rightarrow> udom)" |
|
443 where |
|
444 "defl_take i d = eventual_iterate (udom_approx i oo d)" |
|
445 |
|
446 lemma finite_deflation_defl_take: |
|
447 "deflation d \<Longrightarrow> finite_deflation (defl_take i d)" |
|
448 unfolding defl_take_def |
|
449 apply (rule pre_deflation.finite_deflation_d) |
|
450 apply (rule pre_deflation_oo) |
|
451 apply (rule finite_deflation_udom_approx) |
|
452 apply (erule deflation.below) |
|
453 done |
|
454 |
|
455 lemma deflation_defl_take: |
|
456 "deflation d \<Longrightarrow> deflation (defl_take i d)" |
|
457 apply (rule finite_deflation_imp_deflation) |
|
458 apply (erule finite_deflation_defl_take) |
|
459 done |
|
460 |
|
461 lemma defl_take_fixed_iff: |
|
462 "deflation d \<Longrightarrow> defl_take i d\<cdot>x = x \<longleftrightarrow> udom_approx i\<cdot>x = x \<and> d\<cdot>x = x" |
|
463 unfolding defl_take_def |
|
464 apply (rule eventual_iterate_oo_fixed_iff) |
|
465 apply (rule finite_deflation_udom_approx) |
|
466 apply (erule deflation.below) |
|
467 done |
|
468 |
|
469 lemma defl_take_below: |
|
470 "\<lbrakk>a \<sqsubseteq> b; deflation a; deflation b\<rbrakk> \<Longrightarrow> defl_take i a \<sqsubseteq> defl_take i b" |
|
471 apply (rule deflation.belowI) |
|
472 apply (erule deflation_defl_take) |
|
473 apply (simp add: defl_take_fixed_iff) |
|
474 apply (erule (1) deflation.belowD) |
|
475 apply (erule conjunct2) |
|
476 done |
|
477 |
|
478 lemma cont2cont_defl_take: |
|
479 assumes cont: "cont f" and below: "\<And>x y. f x\<cdot>y \<sqsubseteq> y" |
|
480 shows "cont (\<lambda>x. defl_take i (f x))" |
|
481 unfolding defl_take_def |
|
482 using finite_deflation_udom_approx assms |
|
483 by (rule cont2cont_eventual_iterate_oo) |
|
484 |
|
485 definition |
|
486 fd_take :: "nat \<Rightarrow> fin_defl \<Rightarrow> fin_defl" |
|
487 where |
|
488 "fd_take i d = Abs_fin_defl (defl_take i (Rep_fin_defl d))" |
|
489 |
|
490 lemma Rep_fin_defl_fd_take: |
|
491 "Rep_fin_defl (fd_take i d) = defl_take i (Rep_fin_defl d)" |
|
492 unfolding fd_take_def |
|
493 apply (rule Abs_fin_defl_inverse [unfolded mem_Collect_eq]) |
|
494 apply (rule finite_deflation_defl_take) |
|
495 apply (rule deflation_Rep_fin_defl) |
|
496 done |
|
497 |
|
498 lemma fd_take_fixed_iff: |
|
499 "Rep_fin_defl (fd_take i d)\<cdot>x = x \<longleftrightarrow> |
|
500 udom_approx i\<cdot>x = x \<and> Rep_fin_defl d\<cdot>x = x" |
|
501 unfolding Rep_fin_defl_fd_take |
|
502 apply (rule defl_take_fixed_iff) |
|
503 apply (rule deflation_Rep_fin_defl) |
|
504 done |
|
505 |
|
506 lemma fd_take_below: "fd_take n d \<sqsubseteq> d" |
|
507 apply (rule fin_defl_belowI) |
|
508 apply (simp add: fd_take_fixed_iff) |
|
509 done |
|
510 |
|
511 lemma fd_take_idem: "fd_take n (fd_take n d) = fd_take n d" |
|
512 apply (rule fin_defl_eqI) |
|
513 apply (simp add: fd_take_fixed_iff) |
|
514 done |
|
515 |
|
516 lemma fd_take_mono: "a \<sqsubseteq> b \<Longrightarrow> fd_take n a \<sqsubseteq> fd_take n b" |
|
517 apply (rule fin_defl_belowI) |
|
518 apply (simp add: fd_take_fixed_iff) |
|
519 apply (simp add: fin_defl_belowD) |
|
520 done |
|
521 |
|
522 lemma approx_fixed_le_lemma: "\<lbrakk>i \<le> j; udom_approx i\<cdot>x = x\<rbrakk> \<Longrightarrow> udom_approx j\<cdot>x = x" |
|
523 apply (rule deflation.belowD) |
|
524 apply (rule finite_deflation_imp_deflation) |
|
525 apply (rule finite_deflation_udom_approx) |
|
526 apply (erule chain_mono [OF chain_udom_approx]) |
|
527 apply assumption |
|
528 done |
|
529 |
|
530 lemma fd_take_chain: "m \<le> n \<Longrightarrow> fd_take m a \<sqsubseteq> fd_take n a" |
|
531 apply (rule fin_defl_belowI) |
|
532 apply (simp add: fd_take_fixed_iff) |
|
533 apply (simp add: approx_fixed_le_lemma) |
|
534 done |
|
535 |
|
536 lemma finite_range_fd_take: "finite (range (fd_take n))" |
|
537 apply (rule finite_imageD [where f="\<lambda>a. {x. Rep_fin_defl a\<cdot>x = x}"]) |
|
538 apply (rule finite_subset [where B="Pow {x. udom_approx n\<cdot>x = x}"]) |
|
539 apply (clarify, simp add: fd_take_fixed_iff) |
|
540 apply (simp add: finite_deflation.finite_fixes [OF finite_deflation_udom_approx]) |
|
541 apply (rule inj_onI, clarify) |
|
542 apply (simp add: set_eq_iff fin_defl_eqI) |
|
543 done |
|
544 |
|
545 lemma fd_take_covers: "\<exists>n. fd_take n a = a" |
|
546 apply (rule_tac x= |
|
547 "Max ((\<lambda>x. LEAST n. udom_approx n\<cdot>x = x) ` {x. Rep_fin_defl a\<cdot>x = x})" in exI) |
|
548 apply (rule below_antisym) |
|
549 apply (rule fd_take_below) |
|
550 apply (rule fin_defl_belowI) |
|
551 apply (simp add: fd_take_fixed_iff) |
|
552 apply (rule approx_fixed_le_lemma) |
|
553 apply (rule Max_ge) |
|
554 apply (rule finite_imageI) |
|
555 apply (rule Rep_fin_defl.finite_fixes) |
|
556 apply (rule imageI) |
|
557 apply (erule CollectI) |
|
558 apply (rule LeastI_ex) |
|
559 apply (rule approx_chain.compact_eq_approx [OF udom_approx]) |
|
560 apply (erule subst) |
|
561 apply (rule Rep_fin_defl.compact) |
|
562 done |
|
563 |
|
564 subsection {* Chain of approx functions on algebraic deflations *} |
|
565 |
|
566 definition |
|
567 defl_approx :: "nat \<Rightarrow> defl \<rightarrow> defl" |
|
568 where |
|
569 "defl_approx = (\<lambda>i. defl.basis_fun (\<lambda>d. defl_principal (fd_take i d)))" |
|
570 |
|
571 lemma defl_approx_principal: |
|
572 "defl_approx i\<cdot>(defl_principal d) = defl_principal (fd_take i d)" |
|
573 unfolding defl_approx_def |
|
574 by (simp add: defl.basis_fun_principal fd_take_mono) |
|
575 |
|
576 lemma defl_approx: "approx_chain defl_approx" |
|
577 proof |
|
578 show chain: "chain defl_approx" |
|
579 unfolding defl_approx_def |
|
580 by (simp add: chainI defl.basis_fun_mono fd_take_mono fd_take_chain) |
|
581 show idem: "\<And>i x. defl_approx i\<cdot>(defl_approx i\<cdot>x) = defl_approx i\<cdot>x" |
|
582 apply (induct_tac x rule: defl.principal_induct, simp) |
|
583 apply (simp add: defl_approx_principal fd_take_idem) |
|
584 done |
|
585 show below: "\<And>i x. defl_approx i\<cdot>x \<sqsubseteq> x" |
|
586 apply (induct_tac x rule: defl.principal_induct, simp) |
|
587 apply (simp add: defl_approx_principal fd_take_below) |
|
588 done |
|
589 show lub: "(\<Squnion>i. defl_approx i) = ID" |
|
590 apply (rule cfun_eqI, rule below_antisym) |
|
591 apply (simp add: contlub_cfun_fun chain lub_below_iff chain below) |
|
592 apply (induct_tac x rule: defl.principal_induct, simp) |
|
593 apply (simp add: contlub_cfun_fun chain) |
|
594 apply (simp add: compact_below_lub_iff defl.compact_principal chain) |
|
595 apply (simp add: defl_approx_principal) |
|
596 apply (subgoal_tac "\<exists>i. fd_take i a = a", metis below_refl) |
|
597 apply (rule fd_take_covers) |
|
598 done |
|
599 show "\<And>i. finite {x. defl_approx i\<cdot>x = x}" |
|
600 apply (rule finite_range_imp_finite_fixes) |
|
601 apply (rule_tac B="defl_principal ` range (fd_take i)" in rev_finite_subset) |
|
602 apply (simp add: finite_range_fd_take) |
|
603 apply (clarsimp, rename_tac x) |
|
604 apply (induct_tac x rule: defl.principal_induct) |
|
605 apply (simp add: adm_mem_finite finite_range_fd_take) |
|
606 apply (simp add: defl_approx_principal) |
|
607 done |
|
608 qed |
|
609 |
|
610 subsection {* Algebraic deflations are a bifinite domain *} |
|
611 |
|
612 instantiation defl :: liftdomain |
|
613 begin |
|
614 |
|
615 definition |
|
616 "emb = udom_emb defl_approx" |
|
617 |
|
618 definition |
|
619 "prj = udom_prj defl_approx" |
|
620 |
|
621 definition |
|
622 "defl (t::defl itself) = |
|
623 (\<Squnion>i. defl_principal (Abs_fin_defl (emb oo defl_approx i oo prj)))" |
|
624 |
|
625 definition |
|
626 "(liftemb :: defl u \<rightarrow> udom) = udom_emb u_approx oo u_map\<cdot>emb" |
|
627 |
|
628 definition |
|
629 "(liftprj :: udom \<rightarrow> defl u) = u_map\<cdot>prj oo udom_prj u_approx" |
|
630 |
|
631 definition |
|
632 "liftdefl (t::defl itself) = u_defl\<cdot>DEFL(defl)" |
|
633 |
|
634 instance |
|
635 using liftemb_defl_def liftprj_defl_def liftdefl_defl_def |
|
636 proof (rule liftdomain_class_intro) |
|
637 show ep: "ep_pair emb (prj :: udom \<rightarrow> defl)" |
|
638 unfolding emb_defl_def prj_defl_def |
|
639 by (rule ep_pair_udom [OF defl_approx]) |
|
640 show "cast\<cdot>DEFL(defl) = emb oo (prj :: udom \<rightarrow> defl)" |
|
641 unfolding defl_defl_def |
|
642 apply (subst contlub_cfun_arg) |
|
643 apply (rule chainI) |
|
644 apply (rule defl.principal_mono) |
|
645 apply (simp add: below_fin_defl_def) |
|
646 apply (simp add: Abs_fin_defl_inverse approx_chain.finite_deflation_approx [OF defl_approx] |
|
647 ep_pair.finite_deflation_e_d_p [OF ep]) |
|
648 apply (intro monofun_cfun below_refl) |
|
649 apply (rule chainE) |
|
650 apply (rule approx_chain.chain_approx [OF defl_approx]) |
|
651 apply (subst cast_defl_principal) |
|
652 apply (simp add: Abs_fin_defl_inverse approx_chain.finite_deflation_approx [OF defl_approx] |
|
653 ep_pair.finite_deflation_e_d_p [OF ep]) |
|
654 apply (simp add: lub_distribs approx_chain.chain_approx [OF defl_approx] |
|
655 approx_chain.lub_approx [OF defl_approx]) |
|
656 done |
|
657 qed |
|
658 |
|
659 end |
|
660 |
|
661 end |
|