|
1 (* Title: HOL/BNF_Constructions_on_Wellorders.thy |
|
2 Author: Andrei Popescu, TU Muenchen |
|
3 Copyright 2012 |
|
4 |
|
5 Constructions on wellorders (BNF). |
|
6 *) |
|
7 |
|
8 header {* Constructions on Wellorders (BNF) *} |
|
9 |
|
10 theory BNF_Constructions_on_Wellorders |
|
11 imports BNF_Wellorder_Embedding |
|
12 begin |
|
13 |
|
14 |
|
15 text {* In this section, we study basic constructions on well-orders, such as restriction to |
|
16 a set/order filter, copy via direct images, ordinal-like sum of disjoint well-orders, |
|
17 and bounded square. We also define between well-orders |
|
18 the relations @{text "ordLeq"}, of being embedded (abbreviated @{text "\<le>o"}), |
|
19 @{text "ordLess"}, of being strictly embedded (abbreviated @{text "<o"}), and |
|
20 @{text "ordIso"}, of being isomorphic (abbreviated @{text "=o"}). We study the |
|
21 connections between these relations, order filters, and the aforementioned constructions. |
|
22 A main result of this section is that @{text "<o"} is well-founded. *} |
|
23 |
|
24 |
|
25 subsection {* Restriction to a set *} |
|
26 |
|
27 |
|
28 abbreviation Restr :: "'a rel \<Rightarrow> 'a set \<Rightarrow> 'a rel" |
|
29 where "Restr r A \<equiv> r Int (A \<times> A)" |
|
30 |
|
31 |
|
32 lemma Restr_subset: |
|
33 "A \<le> B \<Longrightarrow> Restr (Restr r B) A = Restr r A" |
|
34 by blast |
|
35 |
|
36 |
|
37 lemma Restr_Field: "Restr r (Field r) = r" |
|
38 unfolding Field_def by auto |
|
39 |
|
40 |
|
41 lemma Refl_Restr: "Refl r \<Longrightarrow> Refl(Restr r A)" |
|
42 unfolding refl_on_def Field_def by auto |
|
43 |
|
44 |
|
45 lemma antisym_Restr: |
|
46 "antisym r \<Longrightarrow> antisym(Restr r A)" |
|
47 unfolding antisym_def Field_def by auto |
|
48 |
|
49 |
|
50 lemma Total_Restr: |
|
51 "Total r \<Longrightarrow> Total(Restr r A)" |
|
52 unfolding total_on_def Field_def by auto |
|
53 |
|
54 |
|
55 lemma trans_Restr: |
|
56 "trans r \<Longrightarrow> trans(Restr r A)" |
|
57 unfolding trans_def Field_def by blast |
|
58 |
|
59 |
|
60 lemma Preorder_Restr: |
|
61 "Preorder r \<Longrightarrow> Preorder(Restr r A)" |
|
62 unfolding preorder_on_def by (simp add: Refl_Restr trans_Restr) |
|
63 |
|
64 |
|
65 lemma Partial_order_Restr: |
|
66 "Partial_order r \<Longrightarrow> Partial_order(Restr r A)" |
|
67 unfolding partial_order_on_def by (simp add: Preorder_Restr antisym_Restr) |
|
68 |
|
69 |
|
70 lemma Linear_order_Restr: |
|
71 "Linear_order r \<Longrightarrow> Linear_order(Restr r A)" |
|
72 unfolding linear_order_on_def by (simp add: Partial_order_Restr Total_Restr) |
|
73 |
|
74 |
|
75 lemma Well_order_Restr: |
|
76 assumes "Well_order r" |
|
77 shows "Well_order(Restr r A)" |
|
78 proof- |
|
79 have "Restr r A - Id \<le> r - Id" using Restr_subset by blast |
|
80 hence "wf(Restr r A - Id)" using assms |
|
81 using well_order_on_def wf_subset by blast |
|
82 thus ?thesis using assms unfolding well_order_on_def |
|
83 by (simp add: Linear_order_Restr) |
|
84 qed |
|
85 |
|
86 |
|
87 lemma Field_Restr_subset: "Field(Restr r A) \<le> A" |
|
88 by (auto simp add: Field_def) |
|
89 |
|
90 |
|
91 lemma Refl_Field_Restr: |
|
92 "Refl r \<Longrightarrow> Field(Restr r A) = (Field r) Int A" |
|
93 unfolding refl_on_def Field_def by blast |
|
94 |
|
95 |
|
96 lemma Refl_Field_Restr2: |
|
97 "\<lbrakk>Refl r; A \<le> Field r\<rbrakk> \<Longrightarrow> Field(Restr r A) = A" |
|
98 by (auto simp add: Refl_Field_Restr) |
|
99 |
|
100 |
|
101 lemma well_order_on_Restr: |
|
102 assumes WELL: "Well_order r" and SUB: "A \<le> Field r" |
|
103 shows "well_order_on A (Restr r A)" |
|
104 using assms |
|
105 using Well_order_Restr[of r A] Refl_Field_Restr2[of r A] |
|
106 order_on_defs[of "Field r" r] by auto |
|
107 |
|
108 |
|
109 subsection {* Order filters versus restrictions and embeddings *} |
|
110 |
|
111 |
|
112 lemma Field_Restr_ofilter: |
|
113 "\<lbrakk>Well_order r; wo_rel.ofilter r A\<rbrakk> \<Longrightarrow> Field(Restr r A) = A" |
|
114 by (auto simp add: wo_rel_def wo_rel.ofilter_def wo_rel.REFL Refl_Field_Restr2) |
|
115 |
|
116 |
|
117 lemma ofilter_Restr_under: |
|
118 assumes WELL: "Well_order r" and OF: "wo_rel.ofilter r A" and IN: "a \<in> A" |
|
119 shows "under (Restr r A) a = under r a" |
|
120 using assms wo_rel_def |
|
121 proof(auto simp add: wo_rel.ofilter_def under_def) |
|
122 fix b assume *: "a \<in> A" and "(b,a) \<in> r" |
|
123 hence "b \<in> under r a \<and> a \<in> Field r" |
|
124 unfolding under_def using Field_def by fastforce |
|
125 thus "b \<in> A" using * assms by (auto simp add: wo_rel_def wo_rel.ofilter_def) |
|
126 qed |
|
127 |
|
128 |
|
129 lemma ofilter_embed: |
|
130 assumes "Well_order r" |
|
131 shows "wo_rel.ofilter r A = (A \<le> Field r \<and> embed (Restr r A) r id)" |
|
132 proof |
|
133 assume *: "wo_rel.ofilter r A" |
|
134 show "A \<le> Field r \<and> embed (Restr r A) r id" |
|
135 proof(unfold embed_def, auto) |
|
136 fix a assume "a \<in> A" thus "a \<in> Field r" using assms * |
|
137 by (auto simp add: wo_rel_def wo_rel.ofilter_def) |
|
138 next |
|
139 fix a assume "a \<in> Field (Restr r A)" |
|
140 thus "bij_betw id (under (Restr r A) a) (under r a)" using assms * |
|
141 by (simp add: ofilter_Restr_under Field_Restr_ofilter) |
|
142 qed |
|
143 next |
|
144 assume *: "A \<le> Field r \<and> embed (Restr r A) r id" |
|
145 hence "Field(Restr r A) \<le> Field r" |
|
146 using assms embed_Field[of "Restr r A" r id] id_def |
|
147 Well_order_Restr[of r] by auto |
|
148 {fix a assume "a \<in> A" |
|
149 hence "a \<in> Field(Restr r A)" using * assms |
|
150 by (simp add: order_on_defs Refl_Field_Restr2) |
|
151 hence "bij_betw id (under (Restr r A) a) (under r a)" |
|
152 using * unfolding embed_def by auto |
|
153 hence "under r a \<le> under (Restr r A) a" |
|
154 unfolding bij_betw_def by auto |
|
155 also have "\<dots> \<le> Field(Restr r A)" by (simp add: under_Field) |
|
156 also have "\<dots> \<le> A" by (simp add: Field_Restr_subset) |
|
157 finally have "under r a \<le> A" . |
|
158 } |
|
159 thus "wo_rel.ofilter r A" using assms * by (simp add: wo_rel_def wo_rel.ofilter_def) |
|
160 qed |
|
161 |
|
162 |
|
163 lemma ofilter_Restr_Int: |
|
164 assumes WELL: "Well_order r" and OFA: "wo_rel.ofilter r A" |
|
165 shows "wo_rel.ofilter (Restr r B) (A Int B)" |
|
166 proof- |
|
167 let ?rB = "Restr r B" |
|
168 have Well: "wo_rel r" unfolding wo_rel_def using WELL . |
|
169 hence Refl: "Refl r" by (simp add: wo_rel.REFL) |
|
170 hence Field: "Field ?rB = Field r Int B" |
|
171 using Refl_Field_Restr by blast |
|
172 have WellB: "wo_rel ?rB \<and> Well_order ?rB" using WELL |
|
173 by (simp add: Well_order_Restr wo_rel_def) |
|
174 (* Main proof *) |
|
175 show ?thesis using WellB assms |
|
176 proof(auto simp add: wo_rel.ofilter_def under_def) |
|
177 fix a assume "a \<in> A" and *: "a \<in> B" |
|
178 hence "a \<in> Field r" using OFA Well by (auto simp add: wo_rel.ofilter_def) |
|
179 with * show "a \<in> Field ?rB" using Field by auto |
|
180 next |
|
181 fix a b assume "a \<in> A" and "(b,a) \<in> r" |
|
182 thus "b \<in> A" using Well OFA by (auto simp add: wo_rel.ofilter_def under_def) |
|
183 qed |
|
184 qed |
|
185 |
|
186 |
|
187 lemma ofilter_Restr_subset: |
|
188 assumes WELL: "Well_order r" and OFA: "wo_rel.ofilter r A" and SUB: "A \<le> B" |
|
189 shows "wo_rel.ofilter (Restr r B) A" |
|
190 proof- |
|
191 have "A Int B = A" using SUB by blast |
|
192 thus ?thesis using assms ofilter_Restr_Int[of r A B] by auto |
|
193 qed |
|
194 |
|
195 |
|
196 lemma ofilter_subset_embed: |
|
197 assumes WELL: "Well_order r" and |
|
198 OFA: "wo_rel.ofilter r A" and OFB: "wo_rel.ofilter r B" |
|
199 shows "(A \<le> B) = (embed (Restr r A) (Restr r B) id)" |
|
200 proof- |
|
201 let ?rA = "Restr r A" let ?rB = "Restr r B" |
|
202 have Well: "wo_rel r" unfolding wo_rel_def using WELL . |
|
203 hence Refl: "Refl r" by (simp add: wo_rel.REFL) |
|
204 hence FieldA: "Field ?rA = Field r Int A" |
|
205 using Refl_Field_Restr by blast |
|
206 have FieldB: "Field ?rB = Field r Int B" |
|
207 using Refl Refl_Field_Restr by blast |
|
208 have WellA: "wo_rel ?rA \<and> Well_order ?rA" using WELL |
|
209 by (simp add: Well_order_Restr wo_rel_def) |
|
210 have WellB: "wo_rel ?rB \<and> Well_order ?rB" using WELL |
|
211 by (simp add: Well_order_Restr wo_rel_def) |
|
212 (* Main proof *) |
|
213 show ?thesis |
|
214 proof |
|
215 assume *: "A \<le> B" |
|
216 hence "wo_rel.ofilter (Restr r B) A" using assms |
|
217 by (simp add: ofilter_Restr_subset) |
|
218 hence "embed (Restr ?rB A) (Restr r B) id" |
|
219 using WellB ofilter_embed[of "?rB" A] by auto |
|
220 thus "embed (Restr r A) (Restr r B) id" |
|
221 using * by (simp add: Restr_subset) |
|
222 next |
|
223 assume *: "embed (Restr r A) (Restr r B) id" |
|
224 {fix a assume **: "a \<in> A" |
|
225 hence "a \<in> Field r" using Well OFA by (auto simp add: wo_rel.ofilter_def) |
|
226 with ** FieldA have "a \<in> Field ?rA" by auto |
|
227 hence "a \<in> Field ?rB" using * WellA embed_Field[of ?rA ?rB id] by auto |
|
228 hence "a \<in> B" using FieldB by auto |
|
229 } |
|
230 thus "A \<le> B" by blast |
|
231 qed |
|
232 qed |
|
233 |
|
234 |
|
235 lemma ofilter_subset_embedS_iso: |
|
236 assumes WELL: "Well_order r" and |
|
237 OFA: "wo_rel.ofilter r A" and OFB: "wo_rel.ofilter r B" |
|
238 shows "((A < B) = (embedS (Restr r A) (Restr r B) id)) \<and> |
|
239 ((A = B) = (iso (Restr r A) (Restr r B) id))" |
|
240 proof- |
|
241 let ?rA = "Restr r A" let ?rB = "Restr r B" |
|
242 have Well: "wo_rel r" unfolding wo_rel_def using WELL . |
|
243 hence Refl: "Refl r" by (simp add: wo_rel.REFL) |
|
244 hence "Field ?rA = Field r Int A" |
|
245 using Refl_Field_Restr by blast |
|
246 hence FieldA: "Field ?rA = A" using OFA Well |
|
247 by (auto simp add: wo_rel.ofilter_def) |
|
248 have "Field ?rB = Field r Int B" |
|
249 using Refl Refl_Field_Restr by blast |
|
250 hence FieldB: "Field ?rB = B" using OFB Well |
|
251 by (auto simp add: wo_rel.ofilter_def) |
|
252 (* Main proof *) |
|
253 show ?thesis unfolding embedS_def iso_def |
|
254 using assms ofilter_subset_embed[of r A B] |
|
255 FieldA FieldB bij_betw_id_iff[of A B] by auto |
|
256 qed |
|
257 |
|
258 |
|
259 lemma ofilter_subset_embedS: |
|
260 assumes WELL: "Well_order r" and |
|
261 OFA: "wo_rel.ofilter r A" and OFB: "wo_rel.ofilter r B" |
|
262 shows "(A < B) = embedS (Restr r A) (Restr r B) id" |
|
263 using assms by (simp add: ofilter_subset_embedS_iso) |
|
264 |
|
265 |
|
266 lemma embed_implies_iso_Restr: |
|
267 assumes WELL: "Well_order r" and WELL': "Well_order r'" and |
|
268 EMB: "embed r' r f" |
|
269 shows "iso r' (Restr r (f ` (Field r'))) f" |
|
270 proof- |
|
271 let ?A' = "Field r'" |
|
272 let ?r'' = "Restr r (f ` ?A')" |
|
273 have 0: "Well_order ?r''" using WELL Well_order_Restr by blast |
|
274 have 1: "wo_rel.ofilter r (f ` ?A')" using assms embed_Field_ofilter by blast |
|
275 hence "Field ?r'' = f ` (Field r')" using WELL Field_Restr_ofilter by blast |
|
276 hence "bij_betw f ?A' (Field ?r'')" |
|
277 using EMB embed_inj_on WELL' unfolding bij_betw_def by blast |
|
278 moreover |
|
279 {have "\<forall>a b. (a,b) \<in> r' \<longrightarrow> a \<in> Field r' \<and> b \<in> Field r'" |
|
280 unfolding Field_def by auto |
|
281 hence "compat r' ?r'' f" |
|
282 using assms embed_iff_compat_inj_on_ofilter |
|
283 unfolding compat_def by blast |
|
284 } |
|
285 ultimately show ?thesis using WELL' 0 iso_iff3 by blast |
|
286 qed |
|
287 |
|
288 |
|
289 subsection {* The strict inclusion on proper ofilters is well-founded *} |
|
290 |
|
291 |
|
292 definition ofilterIncl :: "'a rel \<Rightarrow> 'a set rel" |
|
293 where |
|
294 "ofilterIncl r \<equiv> {(A,B). wo_rel.ofilter r A \<and> A \<noteq> Field r \<and> |
|
295 wo_rel.ofilter r B \<and> B \<noteq> Field r \<and> A < B}" |
|
296 |
|
297 |
|
298 lemma wf_ofilterIncl: |
|
299 assumes WELL: "Well_order r" |
|
300 shows "wf(ofilterIncl r)" |
|
301 proof- |
|
302 have Well: "wo_rel r" using WELL by (simp add: wo_rel_def) |
|
303 hence Lo: "Linear_order r" by (simp add: wo_rel.LIN) |
|
304 let ?h = "(\<lambda> A. wo_rel.suc r A)" |
|
305 let ?rS = "r - Id" |
|
306 have "wf ?rS" using WELL by (simp add: order_on_defs) |
|
307 moreover |
|
308 have "compat (ofilterIncl r) ?rS ?h" |
|
309 proof(unfold compat_def ofilterIncl_def, |
|
310 intro allI impI, simp, elim conjE) |
|
311 fix A B |
|
312 assume *: "wo_rel.ofilter r A" "A \<noteq> Field r" and |
|
313 **: "wo_rel.ofilter r B" "B \<noteq> Field r" and ***: "A < B" |
|
314 then obtain a and b where 0: "a \<in> Field r \<and> b \<in> Field r" and |
|
315 1: "A = underS r a \<and> B = underS r b" |
|
316 using Well by (auto simp add: wo_rel.ofilter_underS_Field) |
|
317 hence "a \<noteq> b" using *** by auto |
|
318 moreover |
|
319 have "(a,b) \<in> r" using 0 1 Lo *** |
|
320 by (auto simp add: underS_incl_iff) |
|
321 moreover |
|
322 have "a = wo_rel.suc r A \<and> b = wo_rel.suc r B" |
|
323 using Well 0 1 by (simp add: wo_rel.suc_underS) |
|
324 ultimately |
|
325 show "(wo_rel.suc r A, wo_rel.suc r B) \<in> r \<and> wo_rel.suc r A \<noteq> wo_rel.suc r B" |
|
326 by simp |
|
327 qed |
|
328 ultimately show "wf (ofilterIncl r)" by (simp add: compat_wf) |
|
329 qed |
|
330 |
|
331 |
|
332 |
|
333 subsection {* Ordering the well-orders by existence of embeddings *} |
|
334 |
|
335 |
|
336 text {* We define three relations between well-orders: |
|
337 \begin{itemize} |
|
338 \item @{text "ordLeq"}, of being embedded (abbreviated @{text "\<le>o"}); |
|
339 \item @{text "ordLess"}, of being strictly embedded (abbreviated @{text "<o"}); |
|
340 \item @{text "ordIso"}, of being isomorphic (abbreviated @{text "=o"}). |
|
341 \end{itemize} |
|
342 % |
|
343 The prefix "ord" and the index "o" in these names stand for "ordinal-like". |
|
344 These relations shall be proved to be inter-connected in a similar fashion as the trio |
|
345 @{text "\<le>"}, @{text "<"}, @{text "="} associated to a total order on a set. |
|
346 *} |
|
347 |
|
348 |
|
349 definition ordLeq :: "('a rel * 'a' rel) set" |
|
350 where |
|
351 "ordLeq = {(r,r'). Well_order r \<and> Well_order r' \<and> (\<exists>f. embed r r' f)}" |
|
352 |
|
353 |
|
354 abbreviation ordLeq2 :: "'a rel \<Rightarrow> 'a' rel \<Rightarrow> bool" (infix "<=o" 50) |
|
355 where "r <=o r' \<equiv> (r,r') \<in> ordLeq" |
|
356 |
|
357 |
|
358 abbreviation ordLeq3 :: "'a rel \<Rightarrow> 'a' rel \<Rightarrow> bool" (infix "\<le>o" 50) |
|
359 where "r \<le>o r' \<equiv> r <=o r'" |
|
360 |
|
361 |
|
362 definition ordLess :: "('a rel * 'a' rel) set" |
|
363 where |
|
364 "ordLess = {(r,r'). Well_order r \<and> Well_order r' \<and> (\<exists>f. embedS r r' f)}" |
|
365 |
|
366 abbreviation ordLess2 :: "'a rel \<Rightarrow> 'a' rel \<Rightarrow> bool" (infix "<o" 50) |
|
367 where "r <o r' \<equiv> (r,r') \<in> ordLess" |
|
368 |
|
369 |
|
370 definition ordIso :: "('a rel * 'a' rel) set" |
|
371 where |
|
372 "ordIso = {(r,r'). Well_order r \<and> Well_order r' \<and> (\<exists>f. iso r r' f)}" |
|
373 |
|
374 abbreviation ordIso2 :: "'a rel \<Rightarrow> 'a' rel \<Rightarrow> bool" (infix "=o" 50) |
|
375 where "r =o r' \<equiv> (r,r') \<in> ordIso" |
|
376 |
|
377 |
|
378 lemmas ordRels_def = ordLeq_def ordLess_def ordIso_def |
|
379 |
|
380 lemma ordLeq_Well_order_simp: |
|
381 assumes "r \<le>o r'" |
|
382 shows "Well_order r \<and> Well_order r'" |
|
383 using assms unfolding ordLeq_def by simp |
|
384 |
|
385 |
|
386 text{* Notice that the relations @{text "\<le>o"}, @{text "<o"}, @{text "=o"} connect well-orders |
|
387 on potentially {\em distinct} types. However, some of the lemmas below, including the next one, |
|
388 restrict implicitly the type of these relations to @{text "(('a rel) * ('a rel)) set"} , i.e., |
|
389 to @{text "'a rel rel"}. *} |
|
390 |
|
391 |
|
392 lemma ordLeq_reflexive: |
|
393 "Well_order r \<Longrightarrow> r \<le>o r" |
|
394 unfolding ordLeq_def using id_embed[of r] by blast |
|
395 |
|
396 |
|
397 lemma ordLeq_transitive[trans]: |
|
398 assumes *: "r \<le>o r'" and **: "r' \<le>o r''" |
|
399 shows "r \<le>o r''" |
|
400 proof- |
|
401 obtain f and f' |
|
402 where 1: "Well_order r \<and> Well_order r' \<and> Well_order r''" and |
|
403 "embed r r' f" and "embed r' r'' f'" |
|
404 using * ** unfolding ordLeq_def by blast |
|
405 hence "embed r r'' (f' o f)" |
|
406 using comp_embed[of r r' f r'' f'] by auto |
|
407 thus "r \<le>o r''" unfolding ordLeq_def using 1 by auto |
|
408 qed |
|
409 |
|
410 |
|
411 lemma ordLeq_total: |
|
412 "\<lbrakk>Well_order r; Well_order r'\<rbrakk> \<Longrightarrow> r \<le>o r' \<or> r' \<le>o r" |
|
413 unfolding ordLeq_def using wellorders_totally_ordered by blast |
|
414 |
|
415 |
|
416 lemma ordIso_reflexive: |
|
417 "Well_order r \<Longrightarrow> r =o r" |
|
418 unfolding ordIso_def using id_iso[of r] by blast |
|
419 |
|
420 |
|
421 lemma ordIso_transitive[trans]: |
|
422 assumes *: "r =o r'" and **: "r' =o r''" |
|
423 shows "r =o r''" |
|
424 proof- |
|
425 obtain f and f' |
|
426 where 1: "Well_order r \<and> Well_order r' \<and> Well_order r''" and |
|
427 "iso r r' f" and 3: "iso r' r'' f'" |
|
428 using * ** unfolding ordIso_def by auto |
|
429 hence "iso r r'' (f' o f)" |
|
430 using comp_iso[of r r' f r'' f'] by auto |
|
431 thus "r =o r''" unfolding ordIso_def using 1 by auto |
|
432 qed |
|
433 |
|
434 |
|
435 lemma ordIso_symmetric: |
|
436 assumes *: "r =o r'" |
|
437 shows "r' =o r" |
|
438 proof- |
|
439 obtain f where 1: "Well_order r \<and> Well_order r'" and |
|
440 2: "embed r r' f \<and> bij_betw f (Field r) (Field r')" |
|
441 using * by (auto simp add: ordIso_def iso_def) |
|
442 let ?f' = "inv_into (Field r) f" |
|
443 have "embed r' r ?f' \<and> bij_betw ?f' (Field r') (Field r)" |
|
444 using 1 2 by (simp add: bij_betw_inv_into inv_into_Field_embed_bij_betw) |
|
445 thus "r' =o r" unfolding ordIso_def using 1 by (auto simp add: iso_def) |
|
446 qed |
|
447 |
|
448 |
|
449 lemma ordLeq_ordLess_trans[trans]: |
|
450 assumes "r \<le>o r'" and " r' <o r''" |
|
451 shows "r <o r''" |
|
452 proof- |
|
453 have "Well_order r \<and> Well_order r''" |
|
454 using assms unfolding ordLeq_def ordLess_def by auto |
|
455 thus ?thesis using assms unfolding ordLeq_def ordLess_def |
|
456 using embed_comp_embedS by blast |
|
457 qed |
|
458 |
|
459 |
|
460 lemma ordLess_ordLeq_trans[trans]: |
|
461 assumes "r <o r'" and " r' \<le>o r''" |
|
462 shows "r <o r''" |
|
463 proof- |
|
464 have "Well_order r \<and> Well_order r''" |
|
465 using assms unfolding ordLeq_def ordLess_def by auto |
|
466 thus ?thesis using assms unfolding ordLeq_def ordLess_def |
|
467 using embedS_comp_embed by blast |
|
468 qed |
|
469 |
|
470 |
|
471 lemma ordLeq_ordIso_trans[trans]: |
|
472 assumes "r \<le>o r'" and " r' =o r''" |
|
473 shows "r \<le>o r''" |
|
474 proof- |
|
475 have "Well_order r \<and> Well_order r''" |
|
476 using assms unfolding ordLeq_def ordIso_def by auto |
|
477 thus ?thesis using assms unfolding ordLeq_def ordIso_def |
|
478 using embed_comp_iso by blast |
|
479 qed |
|
480 |
|
481 |
|
482 lemma ordIso_ordLeq_trans[trans]: |
|
483 assumes "r =o r'" and " r' \<le>o r''" |
|
484 shows "r \<le>o r''" |
|
485 proof- |
|
486 have "Well_order r \<and> Well_order r''" |
|
487 using assms unfolding ordLeq_def ordIso_def by auto |
|
488 thus ?thesis using assms unfolding ordLeq_def ordIso_def |
|
489 using iso_comp_embed by blast |
|
490 qed |
|
491 |
|
492 |
|
493 lemma ordLess_ordIso_trans[trans]: |
|
494 assumes "r <o r'" and " r' =o r''" |
|
495 shows "r <o r''" |
|
496 proof- |
|
497 have "Well_order r \<and> Well_order r''" |
|
498 using assms unfolding ordLess_def ordIso_def by auto |
|
499 thus ?thesis using assms unfolding ordLess_def ordIso_def |
|
500 using embedS_comp_iso by blast |
|
501 qed |
|
502 |
|
503 |
|
504 lemma ordIso_ordLess_trans[trans]: |
|
505 assumes "r =o r'" and " r' <o r''" |
|
506 shows "r <o r''" |
|
507 proof- |
|
508 have "Well_order r \<and> Well_order r''" |
|
509 using assms unfolding ordLess_def ordIso_def by auto |
|
510 thus ?thesis using assms unfolding ordLess_def ordIso_def |
|
511 using iso_comp_embedS by blast |
|
512 qed |
|
513 |
|
514 |
|
515 lemma ordLess_not_embed: |
|
516 assumes "r <o r'" |
|
517 shows "\<not>(\<exists>f'. embed r' r f')" |
|
518 proof- |
|
519 obtain f where 1: "Well_order r \<and> Well_order r'" and 2: "embed r r' f" and |
|
520 3: " \<not> bij_betw f (Field r) (Field r')" |
|
521 using assms unfolding ordLess_def by (auto simp add: embedS_def) |
|
522 {fix f' assume *: "embed r' r f'" |
|
523 hence "bij_betw f (Field r) (Field r')" using 1 2 |
|
524 by (simp add: embed_bothWays_Field_bij_betw) |
|
525 with 3 have False by contradiction |
|
526 } |
|
527 thus ?thesis by blast |
|
528 qed |
|
529 |
|
530 |
|
531 lemma ordLess_Field: |
|
532 assumes OL: "r1 <o r2" and EMB: "embed r1 r2 f" |
|
533 shows "\<not> (f`(Field r1) = Field r2)" |
|
534 proof- |
|
535 let ?A1 = "Field r1" let ?A2 = "Field r2" |
|
536 obtain g where |
|
537 0: "Well_order r1 \<and> Well_order r2" and |
|
538 1: "embed r1 r2 g \<and> \<not>(bij_betw g ?A1 ?A2)" |
|
539 using OL unfolding ordLess_def by (auto simp add: embedS_def) |
|
540 hence "\<forall>a \<in> ?A1. f a = g a" |
|
541 using 0 EMB embed_unique[of r1] by auto |
|
542 hence "\<not>(bij_betw f ?A1 ?A2)" |
|
543 using 1 bij_betw_cong[of ?A1] by blast |
|
544 moreover |
|
545 have "inj_on f ?A1" using EMB 0 by (simp add: embed_inj_on) |
|
546 ultimately show ?thesis by (simp add: bij_betw_def) |
|
547 qed |
|
548 |
|
549 |
|
550 lemma ordLess_iff: |
|
551 "r <o r' = (Well_order r \<and> Well_order r' \<and> \<not>(\<exists>f'. embed r' r f'))" |
|
552 proof |
|
553 assume *: "r <o r'" |
|
554 hence "\<not>(\<exists>f'. embed r' r f')" using ordLess_not_embed[of r r'] by simp |
|
555 with * show "Well_order r \<and> Well_order r' \<and> \<not> (\<exists>f'. embed r' r f')" |
|
556 unfolding ordLess_def by auto |
|
557 next |
|
558 assume *: "Well_order r \<and> Well_order r' \<and> \<not> (\<exists>f'. embed r' r f')" |
|
559 then obtain f where 1: "embed r r' f" |
|
560 using wellorders_totally_ordered[of r r'] by blast |
|
561 moreover |
|
562 {assume "bij_betw f (Field r) (Field r')" |
|
563 with * 1 have "embed r' r (inv_into (Field r) f) " |
|
564 using inv_into_Field_embed_bij_betw[of r r' f] by auto |
|
565 with * have False by blast |
|
566 } |
|
567 ultimately show "(r,r') \<in> ordLess" |
|
568 unfolding ordLess_def using * by (fastforce simp add: embedS_def) |
|
569 qed |
|
570 |
|
571 |
|
572 lemma ordLess_irreflexive: "\<not> r <o r" |
|
573 proof |
|
574 assume "r <o r" |
|
575 hence "Well_order r \<and> \<not>(\<exists>f. embed r r f)" |
|
576 unfolding ordLess_iff .. |
|
577 moreover have "embed r r id" using id_embed[of r] . |
|
578 ultimately show False by blast |
|
579 qed |
|
580 |
|
581 |
|
582 lemma ordLeq_iff_ordLess_or_ordIso: |
|
583 "r \<le>o r' = (r <o r' \<or> r =o r')" |
|
584 unfolding ordRels_def embedS_defs iso_defs by blast |
|
585 |
|
586 |
|
587 lemma ordIso_iff_ordLeq: |
|
588 "(r =o r') = (r \<le>o r' \<and> r' \<le>o r)" |
|
589 proof |
|
590 assume "r =o r'" |
|
591 then obtain f where 1: "Well_order r \<and> Well_order r' \<and> |
|
592 embed r r' f \<and> bij_betw f (Field r) (Field r')" |
|
593 unfolding ordIso_def iso_defs by auto |
|
594 hence "embed r r' f \<and> embed r' r (inv_into (Field r) f)" |
|
595 by (simp add: inv_into_Field_embed_bij_betw) |
|
596 thus "r \<le>o r' \<and> r' \<le>o r" |
|
597 unfolding ordLeq_def using 1 by auto |
|
598 next |
|
599 assume "r \<le>o r' \<and> r' \<le>o r" |
|
600 then obtain f and g where 1: "Well_order r \<and> Well_order r' \<and> |
|
601 embed r r' f \<and> embed r' r g" |
|
602 unfolding ordLeq_def by auto |
|
603 hence "iso r r' f" by (auto simp add: embed_bothWays_iso) |
|
604 thus "r =o r'" unfolding ordIso_def using 1 by auto |
|
605 qed |
|
606 |
|
607 |
|
608 lemma not_ordLess_ordLeq: |
|
609 "r <o r' \<Longrightarrow> \<not> r' \<le>o r" |
|
610 using ordLess_ordLeq_trans ordLess_irreflexive by blast |
|
611 |
|
612 |
|
613 lemma ordLess_or_ordLeq: |
|
614 assumes WELL: "Well_order r" and WELL': "Well_order r'" |
|
615 shows "r <o r' \<or> r' \<le>o r" |
|
616 proof- |
|
617 have "r \<le>o r' \<or> r' \<le>o r" |
|
618 using assms by (simp add: ordLeq_total) |
|
619 moreover |
|
620 {assume "\<not> r <o r' \<and> r \<le>o r'" |
|
621 hence "r =o r'" using ordLeq_iff_ordLess_or_ordIso by blast |
|
622 hence "r' \<le>o r" using ordIso_symmetric ordIso_iff_ordLeq by blast |
|
623 } |
|
624 ultimately show ?thesis by blast |
|
625 qed |
|
626 |
|
627 |
|
628 lemma not_ordLess_ordIso: |
|
629 "r <o r' \<Longrightarrow> \<not> r =o r'" |
|
630 using assms ordLess_ordIso_trans ordIso_symmetric ordLess_irreflexive by blast |
|
631 |
|
632 |
|
633 lemma not_ordLeq_iff_ordLess: |
|
634 assumes WELL: "Well_order r" and WELL': "Well_order r'" |
|
635 shows "(\<not> r' \<le>o r) = (r <o r')" |
|
636 using assms not_ordLess_ordLeq ordLess_or_ordLeq by blast |
|
637 |
|
638 |
|
639 lemma not_ordLess_iff_ordLeq: |
|
640 assumes WELL: "Well_order r" and WELL': "Well_order r'" |
|
641 shows "(\<not> r' <o r) = (r \<le>o r')" |
|
642 using assms not_ordLess_ordLeq ordLess_or_ordLeq by blast |
|
643 |
|
644 |
|
645 lemma ordLess_transitive[trans]: |
|
646 "\<lbrakk>r <o r'; r' <o r''\<rbrakk> \<Longrightarrow> r <o r''" |
|
647 using assms ordLess_ordLeq_trans ordLeq_iff_ordLess_or_ordIso by blast |
|
648 |
|
649 |
|
650 corollary ordLess_trans: "trans ordLess" |
|
651 unfolding trans_def using ordLess_transitive by blast |
|
652 |
|
653 |
|
654 lemmas ordIso_equivalence = ordIso_transitive ordIso_reflexive ordIso_symmetric |
|
655 |
|
656 |
|
657 lemma ordIso_imp_ordLeq: |
|
658 "r =o r' \<Longrightarrow> r \<le>o r'" |
|
659 using ordIso_iff_ordLeq by blast |
|
660 |
|
661 |
|
662 lemma ordLess_imp_ordLeq: |
|
663 "r <o r' \<Longrightarrow> r \<le>o r'" |
|
664 using ordLeq_iff_ordLess_or_ordIso by blast |
|
665 |
|
666 |
|
667 lemma ofilter_subset_ordLeq: |
|
668 assumes WELL: "Well_order r" and |
|
669 OFA: "wo_rel.ofilter r A" and OFB: "wo_rel.ofilter r B" |
|
670 shows "(A \<le> B) = (Restr r A \<le>o Restr r B)" |
|
671 proof |
|
672 assume "A \<le> B" |
|
673 thus "Restr r A \<le>o Restr r B" |
|
674 unfolding ordLeq_def using assms |
|
675 Well_order_Restr Well_order_Restr ofilter_subset_embed by blast |
|
676 next |
|
677 assume *: "Restr r A \<le>o Restr r B" |
|
678 then obtain f where "embed (Restr r A) (Restr r B) f" |
|
679 unfolding ordLeq_def by blast |
|
680 {assume "B < A" |
|
681 hence "Restr r B <o Restr r A" |
|
682 unfolding ordLess_def using assms |
|
683 Well_order_Restr Well_order_Restr ofilter_subset_embedS by blast |
|
684 hence False using * not_ordLess_ordLeq by blast |
|
685 } |
|
686 thus "A \<le> B" using OFA OFB WELL |
|
687 wo_rel_def[of r] wo_rel.ofilter_linord[of r A B] by blast |
|
688 qed |
|
689 |
|
690 |
|
691 lemma ofilter_subset_ordLess: |
|
692 assumes WELL: "Well_order r" and |
|
693 OFA: "wo_rel.ofilter r A" and OFB: "wo_rel.ofilter r B" |
|
694 shows "(A < B) = (Restr r A <o Restr r B)" |
|
695 proof- |
|
696 let ?rA = "Restr r A" let ?rB = "Restr r B" |
|
697 have 1: "Well_order ?rA \<and> Well_order ?rB" |
|
698 using WELL Well_order_Restr by blast |
|
699 have "(A < B) = (\<not> B \<le> A)" using assms |
|
700 wo_rel_def wo_rel.ofilter_linord[of r A B] by blast |
|
701 also have "\<dots> = (\<not> Restr r B \<le>o Restr r A)" |
|
702 using assms ofilter_subset_ordLeq by blast |
|
703 also have "\<dots> = (Restr r A <o Restr r B)" |
|
704 using 1 not_ordLeq_iff_ordLess by blast |
|
705 finally show ?thesis . |
|
706 qed |
|
707 |
|
708 |
|
709 lemma ofilter_ordLess: |
|
710 "\<lbrakk>Well_order r; wo_rel.ofilter r A\<rbrakk> \<Longrightarrow> (A < Field r) = (Restr r A <o r)" |
|
711 by (simp add: ofilter_subset_ordLess wo_rel.Field_ofilter |
|
712 wo_rel_def Restr_Field) |
|
713 |
|
714 |
|
715 corollary underS_Restr_ordLess: |
|
716 assumes "Well_order r" and "Field r \<noteq> {}" |
|
717 shows "Restr r (underS r a) <o r" |
|
718 proof- |
|
719 have "underS r a < Field r" using assms |
|
720 by (simp add: underS_Field3) |
|
721 thus ?thesis using assms |
|
722 by (simp add: ofilter_ordLess wo_rel.underS_ofilter wo_rel_def) |
|
723 qed |
|
724 |
|
725 |
|
726 lemma embed_ordLess_ofilterIncl: |
|
727 assumes |
|
728 OL12: "r1 <o r2" and OL23: "r2 <o r3" and |
|
729 EMB13: "embed r1 r3 f13" and EMB23: "embed r2 r3 f23" |
|
730 shows "(f13`(Field r1), f23`(Field r2)) \<in> (ofilterIncl r3)" |
|
731 proof- |
|
732 have OL13: "r1 <o r3" |
|
733 using OL12 OL23 using ordLess_transitive by auto |
|
734 let ?A1 = "Field r1" let ?A2 ="Field r2" let ?A3 ="Field r3" |
|
735 obtain f12 g23 where |
|
736 0: "Well_order r1 \<and> Well_order r2 \<and> Well_order r3" and |
|
737 1: "embed r1 r2 f12 \<and> \<not>(bij_betw f12 ?A1 ?A2)" and |
|
738 2: "embed r2 r3 g23 \<and> \<not>(bij_betw g23 ?A2 ?A3)" |
|
739 using OL12 OL23 by (auto simp add: ordLess_def embedS_def) |
|
740 hence "\<forall>a \<in> ?A2. f23 a = g23 a" |
|
741 using EMB23 embed_unique[of r2 r3] by blast |
|
742 hence 3: "\<not>(bij_betw f23 ?A2 ?A3)" |
|
743 using 2 bij_betw_cong[of ?A2 f23 g23] by blast |
|
744 (* *) |
|
745 have 4: "wo_rel.ofilter r2 (f12 ` ?A1) \<and> f12 ` ?A1 \<noteq> ?A2" |
|
746 using 0 1 OL12 by (simp add: embed_Field_ofilter ordLess_Field) |
|
747 have 5: "wo_rel.ofilter r3 (f23 ` ?A2) \<and> f23 ` ?A2 \<noteq> ?A3" |
|
748 using 0 EMB23 OL23 by (simp add: embed_Field_ofilter ordLess_Field) |
|
749 have 6: "wo_rel.ofilter r3 (f13 ` ?A1) \<and> f13 ` ?A1 \<noteq> ?A3" |
|
750 using 0 EMB13 OL13 by (simp add: embed_Field_ofilter ordLess_Field) |
|
751 (* *) |
|
752 have "f12 ` ?A1 < ?A2" |
|
753 using 0 4 by (auto simp add: wo_rel_def wo_rel.ofilter_def) |
|
754 moreover have "inj_on f23 ?A2" |
|
755 using EMB23 0 by (simp add: wo_rel_def embed_inj_on) |
|
756 ultimately |
|
757 have "f23 ` (f12 ` ?A1) < f23 ` ?A2" by (simp add: inj_on_strict_subset) |
|
758 moreover |
|
759 {have "embed r1 r3 (f23 o f12)" |
|
760 using 1 EMB23 0 by (auto simp add: comp_embed) |
|
761 hence "\<forall>a \<in> ?A1. f23(f12 a) = f13 a" |
|
762 using EMB13 0 embed_unique[of r1 r3 "f23 o f12" f13] by auto |
|
763 hence "f23 ` (f12 ` ?A1) = f13 ` ?A1" by force |
|
764 } |
|
765 ultimately |
|
766 have "f13 ` ?A1 < f23 ` ?A2" by simp |
|
767 (* *) |
|
768 with 5 6 show ?thesis |
|
769 unfolding ofilterIncl_def by auto |
|
770 qed |
|
771 |
|
772 |
|
773 lemma ordLess_iff_ordIso_Restr: |
|
774 assumes WELL: "Well_order r" and WELL': "Well_order r'" |
|
775 shows "(r' <o r) = (\<exists>a \<in> Field r. r' =o Restr r (underS r a))" |
|
776 proof(auto) |
|
777 fix a assume *: "a \<in> Field r" and **: "r' =o Restr r (underS r a)" |
|
778 hence "Restr r (underS r a) <o r" using WELL underS_Restr_ordLess[of r] by blast |
|
779 thus "r' <o r" using ** ordIso_ordLess_trans by blast |
|
780 next |
|
781 assume "r' <o r" |
|
782 then obtain f where 1: "Well_order r \<and> Well_order r'" and |
|
783 2: "embed r' r f \<and> f ` (Field r') \<noteq> Field r" |
|
784 unfolding ordLess_def embedS_def[abs_def] bij_betw_def using embed_inj_on by blast |
|
785 hence "wo_rel.ofilter r (f ` (Field r'))" using embed_Field_ofilter by blast |
|
786 then obtain a where 3: "a \<in> Field r" and 4: "underS r a = f ` (Field r')" |
|
787 using 1 2 by (auto simp add: wo_rel.ofilter_underS_Field wo_rel_def) |
|
788 have "iso r' (Restr r (f ` (Field r'))) f" |
|
789 using embed_implies_iso_Restr 2 assms by blast |
|
790 moreover have "Well_order (Restr r (f ` (Field r')))" |
|
791 using WELL Well_order_Restr by blast |
|
792 ultimately have "r' =o Restr r (f ` (Field r'))" |
|
793 using WELL' unfolding ordIso_def by auto |
|
794 hence "r' =o Restr r (underS r a)" using 4 by auto |
|
795 thus "\<exists>a \<in> Field r. r' =o Restr r (underS r a)" using 3 by auto |
|
796 qed |
|
797 |
|
798 |
|
799 lemma internalize_ordLess: |
|
800 "(r' <o r) = (\<exists>p. Field p < Field r \<and> r' =o p \<and> p <o r)" |
|
801 proof |
|
802 assume *: "r' <o r" |
|
803 hence 0: "Well_order r \<and> Well_order r'" unfolding ordLess_def by auto |
|
804 with * obtain a where 1: "a \<in> Field r" and 2: "r' =o Restr r (underS r a)" |
|
805 using ordLess_iff_ordIso_Restr by blast |
|
806 let ?p = "Restr r (underS r a)" |
|
807 have "wo_rel.ofilter r (underS r a)" using 0 |
|
808 by (simp add: wo_rel_def wo_rel.underS_ofilter) |
|
809 hence "Field ?p = underS r a" using 0 Field_Restr_ofilter by blast |
|
810 hence "Field ?p < Field r" using underS_Field2 1 by fast |
|
811 moreover have "?p <o r" using underS_Restr_ordLess[of r a] 0 1 by blast |
|
812 ultimately |
|
813 show "\<exists>p. Field p < Field r \<and> r' =o p \<and> p <o r" using 2 by blast |
|
814 next |
|
815 assume "\<exists>p. Field p < Field r \<and> r' =o p \<and> p <o r" |
|
816 thus "r' <o r" using ordIso_ordLess_trans by blast |
|
817 qed |
|
818 |
|
819 |
|
820 lemma internalize_ordLeq: |
|
821 "(r' \<le>o r) = (\<exists>p. Field p \<le> Field r \<and> r' =o p \<and> p \<le>o r)" |
|
822 proof |
|
823 assume *: "r' \<le>o r" |
|
824 moreover |
|
825 {assume "r' <o r" |
|
826 then obtain p where "Field p < Field r \<and> r' =o p \<and> p <o r" |
|
827 using internalize_ordLess[of r' r] by blast |
|
828 hence "\<exists>p. Field p \<le> Field r \<and> r' =o p \<and> p \<le>o r" |
|
829 using ordLeq_iff_ordLess_or_ordIso by blast |
|
830 } |
|
831 moreover |
|
832 have "r \<le>o r" using * ordLeq_def ordLeq_reflexive by blast |
|
833 ultimately show "\<exists>p. Field p \<le> Field r \<and> r' =o p \<and> p \<le>o r" |
|
834 using ordLeq_iff_ordLess_or_ordIso by blast |
|
835 next |
|
836 assume "\<exists>p. Field p \<le> Field r \<and> r' =o p \<and> p \<le>o r" |
|
837 thus "r' \<le>o r" using ordIso_ordLeq_trans by blast |
|
838 qed |
|
839 |
|
840 |
|
841 lemma ordLeq_iff_ordLess_Restr: |
|
842 assumes WELL: "Well_order r" and WELL': "Well_order r'" |
|
843 shows "(r \<le>o r') = (\<forall>a \<in> Field r. Restr r (underS r a) <o r')" |
|
844 proof(auto) |
|
845 assume *: "r \<le>o r'" |
|
846 fix a assume "a \<in> Field r" |
|
847 hence "Restr r (underS r a) <o r" |
|
848 using WELL underS_Restr_ordLess[of r] by blast |
|
849 thus "Restr r (underS r a) <o r'" |
|
850 using * ordLess_ordLeq_trans by blast |
|
851 next |
|
852 assume *: "\<forall>a \<in> Field r. Restr r (underS r a) <o r'" |
|
853 {assume "r' <o r" |
|
854 then obtain a where "a \<in> Field r \<and> r' =o Restr r (underS r a)" |
|
855 using assms ordLess_iff_ordIso_Restr by blast |
|
856 hence False using * not_ordLess_ordIso ordIso_symmetric by blast |
|
857 } |
|
858 thus "r \<le>o r'" using ordLess_or_ordLeq assms by blast |
|
859 qed |
|
860 |
|
861 |
|
862 lemma finite_ordLess_infinite: |
|
863 assumes WELL: "Well_order r" and WELL': "Well_order r'" and |
|
864 FIN: "finite(Field r)" and INF: "\<not>finite(Field r')" |
|
865 shows "r <o r'" |
|
866 proof- |
|
867 {assume "r' \<le>o r" |
|
868 then obtain h where "inj_on h (Field r') \<and> h ` (Field r') \<le> Field r" |
|
869 unfolding ordLeq_def using assms embed_inj_on embed_Field by blast |
|
870 hence False using finite_imageD finite_subset FIN INF by metis |
|
871 } |
|
872 thus ?thesis using WELL WELL' ordLess_or_ordLeq by blast |
|
873 qed |
|
874 |
|
875 |
|
876 lemma finite_well_order_on_ordIso: |
|
877 assumes FIN: "finite A" and |
|
878 WELL: "well_order_on A r" and WELL': "well_order_on A r'" |
|
879 shows "r =o r'" |
|
880 proof- |
|
881 have 0: "Well_order r \<and> Well_order r' \<and> Field r = A \<and> Field r' = A" |
|
882 using assms well_order_on_Well_order by blast |
|
883 moreover |
|
884 have "\<forall>r r'. well_order_on A r \<and> well_order_on A r' \<and> r \<le>o r' |
|
885 \<longrightarrow> r =o r'" |
|
886 proof(clarify) |
|
887 fix r r' assume *: "well_order_on A r" and **: "well_order_on A r'" |
|
888 have 2: "Well_order r \<and> Well_order r' \<and> Field r = A \<and> Field r' = A" |
|
889 using * ** well_order_on_Well_order by blast |
|
890 assume "r \<le>o r'" |
|
891 then obtain f where 1: "embed r r' f" and |
|
892 "inj_on f A \<and> f ` A \<le> A" |
|
893 unfolding ordLeq_def using 2 embed_inj_on embed_Field by blast |
|
894 hence "bij_betw f A A" unfolding bij_betw_def using FIN endo_inj_surj by blast |
|
895 thus "r =o r'" unfolding ordIso_def iso_def[abs_def] using 1 2 by auto |
|
896 qed |
|
897 ultimately show ?thesis using assms ordLeq_total ordIso_symmetric by metis |
|
898 qed |
|
899 |
|
900 |
|
901 subsection{* @{text "<o"} is well-founded *} |
|
902 |
|
903 |
|
904 text {* Of course, it only makes sense to state that the @{text "<o"} is well-founded |
|
905 on the restricted type @{text "'a rel rel"}. We prove this by first showing that, for any set |
|
906 of well-orders all embedded in a fixed well-order, the function mapping each well-order |
|
907 in the set to an order filter of the fixed well-order is compatible w.r.t. to @{text "<o"} versus |
|
908 {\em strict inclusion}; and we already know that strict inclusion of order filters is well-founded. *} |
|
909 |
|
910 |
|
911 definition ord_to_filter :: "'a rel \<Rightarrow> 'a rel \<Rightarrow> 'a set" |
|
912 where "ord_to_filter r0 r \<equiv> (SOME f. embed r r0 f) ` (Field r)" |
|
913 |
|
914 |
|
915 lemma ord_to_filter_compat: |
|
916 "compat (ordLess Int (ordLess^-1``{r0} \<times> ordLess^-1``{r0})) |
|
917 (ofilterIncl r0) |
|
918 (ord_to_filter r0)" |
|
919 proof(unfold compat_def ord_to_filter_def, clarify) |
|
920 fix r1::"'a rel" and r2::"'a rel" |
|
921 let ?A1 = "Field r1" let ?A2 ="Field r2" let ?A0 ="Field r0" |
|
922 let ?phi10 = "\<lambda> f10. embed r1 r0 f10" let ?f10 = "SOME f. ?phi10 f" |
|
923 let ?phi20 = "\<lambda> f20. embed r2 r0 f20" let ?f20 = "SOME f. ?phi20 f" |
|
924 assume *: "r1 <o r0" "r2 <o r0" and **: "r1 <o r2" |
|
925 hence "(\<exists>f. ?phi10 f) \<and> (\<exists>f. ?phi20 f)" |
|
926 by (auto simp add: ordLess_def embedS_def) |
|
927 hence "?phi10 ?f10 \<and> ?phi20 ?f20" by (auto simp add: someI_ex) |
|
928 thus "(?f10 ` ?A1, ?f20 ` ?A2) \<in> ofilterIncl r0" |
|
929 using * ** by (simp add: embed_ordLess_ofilterIncl) |
|
930 qed |
|
931 |
|
932 |
|
933 theorem wf_ordLess: "wf ordLess" |
|
934 proof- |
|
935 {fix r0 :: "('a \<times> 'a) set" |
|
936 (* need to annotate here!*) |
|
937 let ?ordLess = "ordLess::('d rel * 'd rel) set" |
|
938 let ?R = "?ordLess Int (?ordLess^-1``{r0} \<times> ?ordLess^-1``{r0})" |
|
939 {assume Case1: "Well_order r0" |
|
940 hence "wf ?R" |
|
941 using wf_ofilterIncl[of r0] |
|
942 compat_wf[of ?R "ofilterIncl r0" "ord_to_filter r0"] |
|
943 ord_to_filter_compat[of r0] by auto |
|
944 } |
|
945 moreover |
|
946 {assume Case2: "\<not> Well_order r0" |
|
947 hence "?R = {}" unfolding ordLess_def by auto |
|
948 hence "wf ?R" using wf_empty by simp |
|
949 } |
|
950 ultimately have "wf ?R" by blast |
|
951 } |
|
952 thus ?thesis by (simp add: trans_wf_iff ordLess_trans) |
|
953 qed |
|
954 |
|
955 corollary exists_minim_Well_order: |
|
956 assumes NE: "R \<noteq> {}" and WELL: "\<forall>r \<in> R. Well_order r" |
|
957 shows "\<exists>r \<in> R. \<forall>r' \<in> R. r \<le>o r'" |
|
958 proof- |
|
959 obtain r where "r \<in> R \<and> (\<forall>r' \<in> R. \<not> r' <o r)" |
|
960 using NE spec[OF spec[OF subst[OF wf_eq_minimal, of "%x. x", OF wf_ordLess]], of _ R] |
|
961 equals0I[of R] by blast |
|
962 with not_ordLeq_iff_ordLess WELL show ?thesis by blast |
|
963 qed |
|
964 |
|
965 |
|
966 |
|
967 subsection {* Copy via direct images *} |
|
968 |
|
969 |
|
970 text{* The direct image operator is the dual of the inverse image operator @{text "inv_image"} |
|
971 from @{text "Relation.thy"}. It is useful for transporting a well-order between |
|
972 different types. *} |
|
973 |
|
974 |
|
975 definition dir_image :: "'a rel \<Rightarrow> ('a \<Rightarrow> 'a') \<Rightarrow> 'a' rel" |
|
976 where |
|
977 "dir_image r f = {(f a, f b)| a b. (a,b) \<in> r}" |
|
978 |
|
979 |
|
980 lemma dir_image_Field: |
|
981 "Field(dir_image r f) \<le> f ` (Field r)" |
|
982 unfolding dir_image_def Field_def by auto |
|
983 |
|
984 |
|
985 lemma dir_image_minus_Id: |
|
986 "inj_on f (Field r) \<Longrightarrow> (dir_image r f) - Id = dir_image (r - Id) f" |
|
987 unfolding inj_on_def Field_def dir_image_def by auto |
|
988 |
|
989 |
|
990 lemma Refl_dir_image: |
|
991 assumes "Refl r" |
|
992 shows "Refl(dir_image r f)" |
|
993 proof- |
|
994 {fix a' b' |
|
995 assume "(a',b') \<in> dir_image r f" |
|
996 then obtain a b where 1: "a' = f a \<and> b' = f b \<and> (a,b) \<in> r" |
|
997 unfolding dir_image_def by blast |
|
998 hence "a \<in> Field r \<and> b \<in> Field r" using Field_def by fastforce |
|
999 hence "(a,a) \<in> r \<and> (b,b) \<in> r" using assms by (simp add: refl_on_def) |
|
1000 with 1 have "(a',a') \<in> dir_image r f \<and> (b',b') \<in> dir_image r f" |
|
1001 unfolding dir_image_def by auto |
|
1002 } |
|
1003 thus ?thesis |
|
1004 by(unfold refl_on_def Field_def Domain_def Range_def, auto) |
|
1005 qed |
|
1006 |
|
1007 |
|
1008 lemma trans_dir_image: |
|
1009 assumes TRANS: "trans r" and INJ: "inj_on f (Field r)" |
|
1010 shows "trans(dir_image r f)" |
|
1011 proof(unfold trans_def, auto) |
|
1012 fix a' b' c' |
|
1013 assume "(a',b') \<in> dir_image r f" "(b',c') \<in> dir_image r f" |
|
1014 then obtain a b1 b2 c where 1: "a' = f a \<and> b' = f b1 \<and> b' = f b2 \<and> c' = f c" and |
|
1015 2: "(a,b1) \<in> r \<and> (b2,c) \<in> r" |
|
1016 unfolding dir_image_def by blast |
|
1017 hence "b1 \<in> Field r \<and> b2 \<in> Field r" |
|
1018 unfolding Field_def by auto |
|
1019 hence "b1 = b2" using 1 INJ unfolding inj_on_def by auto |
|
1020 hence "(a,c): r" using 2 TRANS unfolding trans_def by blast |
|
1021 thus "(a',c') \<in> dir_image r f" |
|
1022 unfolding dir_image_def using 1 by auto |
|
1023 qed |
|
1024 |
|
1025 |
|
1026 lemma Preorder_dir_image: |
|
1027 "\<lbrakk>Preorder r; inj_on f (Field r)\<rbrakk> \<Longrightarrow> Preorder (dir_image r f)" |
|
1028 by (simp add: preorder_on_def Refl_dir_image trans_dir_image) |
|
1029 |
|
1030 |
|
1031 lemma antisym_dir_image: |
|
1032 assumes AN: "antisym r" and INJ: "inj_on f (Field r)" |
|
1033 shows "antisym(dir_image r f)" |
|
1034 proof(unfold antisym_def, auto) |
|
1035 fix a' b' |
|
1036 assume "(a',b') \<in> dir_image r f" "(b',a') \<in> dir_image r f" |
|
1037 then obtain a1 b1 a2 b2 where 1: "a' = f a1 \<and> a' = f a2 \<and> b' = f b1 \<and> b' = f b2" and |
|
1038 2: "(a1,b1) \<in> r \<and> (b2,a2) \<in> r " and |
|
1039 3: "{a1,a2,b1,b2} \<le> Field r" |
|
1040 unfolding dir_image_def Field_def by blast |
|
1041 hence "a1 = a2 \<and> b1 = b2" using INJ unfolding inj_on_def by auto |
|
1042 hence "a1 = b2" using 2 AN unfolding antisym_def by auto |
|
1043 thus "a' = b'" using 1 by auto |
|
1044 qed |
|
1045 |
|
1046 |
|
1047 lemma Partial_order_dir_image: |
|
1048 "\<lbrakk>Partial_order r; inj_on f (Field r)\<rbrakk> \<Longrightarrow> Partial_order (dir_image r f)" |
|
1049 by (simp add: partial_order_on_def Preorder_dir_image antisym_dir_image) |
|
1050 |
|
1051 |
|
1052 lemma Total_dir_image: |
|
1053 assumes TOT: "Total r" and INJ: "inj_on f (Field r)" |
|
1054 shows "Total(dir_image r f)" |
|
1055 proof(unfold total_on_def, intro ballI impI) |
|
1056 fix a' b' |
|
1057 assume "a' \<in> Field (dir_image r f)" "b' \<in> Field (dir_image r f)" |
|
1058 then obtain a and b where 1: "a \<in> Field r \<and> b \<in> Field r \<and> f a = a' \<and> f b = b'" |
|
1059 using dir_image_Field[of r f] by blast |
|
1060 moreover assume "a' \<noteq> b'" |
|
1061 ultimately have "a \<noteq> b" using INJ unfolding inj_on_def by auto |
|
1062 hence "(a,b) \<in> r \<or> (b,a) \<in> r" using 1 TOT unfolding total_on_def by auto |
|
1063 thus "(a',b') \<in> dir_image r f \<or> (b',a') \<in> dir_image r f" |
|
1064 using 1 unfolding dir_image_def by auto |
|
1065 qed |
|
1066 |
|
1067 |
|
1068 lemma Linear_order_dir_image: |
|
1069 "\<lbrakk>Linear_order r; inj_on f (Field r)\<rbrakk> \<Longrightarrow> Linear_order (dir_image r f)" |
|
1070 by (simp add: linear_order_on_def Partial_order_dir_image Total_dir_image) |
|
1071 |
|
1072 |
|
1073 lemma wf_dir_image: |
|
1074 assumes WF: "wf r" and INJ: "inj_on f (Field r)" |
|
1075 shows "wf(dir_image r f)" |
|
1076 proof(unfold wf_eq_minimal2, intro allI impI, elim conjE) |
|
1077 fix A'::"'b set" |
|
1078 assume SUB: "A' \<le> Field(dir_image r f)" and NE: "A' \<noteq> {}" |
|
1079 obtain A where A_def: "A = {a \<in> Field r. f a \<in> A'}" by blast |
|
1080 have "A \<noteq> {} \<and> A \<le> Field r" |
|
1081 using A_def dir_image_Field[of r f] SUB NE by blast |
|
1082 then obtain a where 1: "a \<in> A \<and> (\<forall>b \<in> A. (b,a) \<notin> r)" |
|
1083 using WF unfolding wf_eq_minimal2 by metis |
|
1084 have "\<forall>b' \<in> A'. (b',f a) \<notin> dir_image r f" |
|
1085 proof(clarify) |
|
1086 fix b' assume *: "b' \<in> A'" and **: "(b',f a) \<in> dir_image r f" |
|
1087 obtain b1 a1 where 2: "b' = f b1 \<and> f a = f a1" and |
|
1088 3: "(b1,a1) \<in> r \<and> {a1,b1} \<le> Field r" |
|
1089 using ** unfolding dir_image_def Field_def by blast |
|
1090 hence "a = a1" using 1 A_def INJ unfolding inj_on_def by auto |
|
1091 hence "b1 \<in> A \<and> (b1,a) \<in> r" using 2 3 A_def * by auto |
|
1092 with 1 show False by auto |
|
1093 qed |
|
1094 thus "\<exists>a'\<in>A'. \<forall>b'\<in>A'. (b', a') \<notin> dir_image r f" |
|
1095 using A_def 1 by blast |
|
1096 qed |
|
1097 |
|
1098 |
|
1099 lemma Well_order_dir_image: |
|
1100 "\<lbrakk>Well_order r; inj_on f (Field r)\<rbrakk> \<Longrightarrow> Well_order (dir_image r f)" |
|
1101 using assms unfolding well_order_on_def |
|
1102 using Linear_order_dir_image[of r f] wf_dir_image[of "r - Id" f] |
|
1103 dir_image_minus_Id[of f r] |
|
1104 subset_inj_on[of f "Field r" "Field(r - Id)"] |
|
1105 mono_Field[of "r - Id" r] by auto |
|
1106 |
|
1107 |
|
1108 lemma dir_image_Field2: |
|
1109 "Refl r \<Longrightarrow> Field(dir_image r f) = f ` (Field r)" |
|
1110 unfolding Field_def dir_image_def refl_on_def Domain_def Range_def by blast |
|
1111 |
|
1112 |
|
1113 lemma dir_image_bij_betw: |
|
1114 "\<lbrakk>Well_order r; inj_on f (Field r)\<rbrakk> \<Longrightarrow> bij_betw f (Field r) (Field (dir_image r f))" |
|
1115 unfolding bij_betw_def |
|
1116 by (simp add: dir_image_Field2 order_on_defs) |
|
1117 |
|
1118 |
|
1119 lemma dir_image_compat: |
|
1120 "compat r (dir_image r f) f" |
|
1121 unfolding compat_def dir_image_def by auto |
|
1122 |
|
1123 |
|
1124 lemma dir_image_iso: |
|
1125 "\<lbrakk>Well_order r; inj_on f (Field r)\<rbrakk> \<Longrightarrow> iso r (dir_image r f) f" |
|
1126 using iso_iff3 dir_image_compat dir_image_bij_betw Well_order_dir_image by blast |
|
1127 |
|
1128 |
|
1129 lemma dir_image_ordIso: |
|
1130 "\<lbrakk>Well_order r; inj_on f (Field r)\<rbrakk> \<Longrightarrow> r =o dir_image r f" |
|
1131 unfolding ordIso_def using dir_image_iso Well_order_dir_image by blast |
|
1132 |
|
1133 |
|
1134 lemma Well_order_iso_copy: |
|
1135 assumes WELL: "well_order_on A r" and BIJ: "bij_betw f A A'" |
|
1136 shows "\<exists>r'. well_order_on A' r' \<and> r =o r'" |
|
1137 proof- |
|
1138 let ?r' = "dir_image r f" |
|
1139 have 1: "A = Field r \<and> Well_order r" |
|
1140 using WELL well_order_on_Well_order by blast |
|
1141 hence 2: "iso r ?r' f" |
|
1142 using dir_image_iso using BIJ unfolding bij_betw_def by auto |
|
1143 hence "f ` (Field r) = Field ?r'" using 1 iso_iff[of r ?r'] by blast |
|
1144 hence "Field ?r' = A'" |
|
1145 using 1 BIJ unfolding bij_betw_def by auto |
|
1146 moreover have "Well_order ?r'" |
|
1147 using 1 Well_order_dir_image BIJ unfolding bij_betw_def by blast |
|
1148 ultimately show ?thesis unfolding ordIso_def using 1 2 by blast |
|
1149 qed |
|
1150 |
|
1151 |
|
1152 |
|
1153 subsection {* Bounded square *} |
|
1154 |
|
1155 |
|
1156 text{* This construction essentially defines, for an order relation @{text "r"}, a lexicographic |
|
1157 order @{text "bsqr r"} on @{text "(Field r) \<times> (Field r)"}, applying the |
|
1158 following criteria (in this order): |
|
1159 \begin{itemize} |
|
1160 \item compare the maximums; |
|
1161 \item compare the first components; |
|
1162 \item compare the second components. |
|
1163 \end{itemize} |
|
1164 % |
|
1165 The only application of this construction that we are aware of is |
|
1166 at proving that the square of an infinite set has the same cardinal |
|
1167 as that set. The essential property required there (and which is ensured by this |
|
1168 construction) is that any proper order filter of the product order is included in a rectangle, i.e., |
|
1169 in a product of proper filters on the original relation (assumed to be a well-order). *} |
|
1170 |
|
1171 |
|
1172 definition bsqr :: "'a rel => ('a * 'a)rel" |
|
1173 where |
|
1174 "bsqr r = {((a1,a2),(b1,b2)). |
|
1175 {a1,a2,b1,b2} \<le> Field r \<and> |
|
1176 (a1 = b1 \<and> a2 = b2 \<or> |
|
1177 (wo_rel.max2 r a1 a2, wo_rel.max2 r b1 b2) \<in> r - Id \<or> |
|
1178 wo_rel.max2 r a1 a2 = wo_rel.max2 r b1 b2 \<and> (a1,b1) \<in> r - Id \<or> |
|
1179 wo_rel.max2 r a1 a2 = wo_rel.max2 r b1 b2 \<and> a1 = b1 \<and> (a2,b2) \<in> r - Id |
|
1180 )}" |
|
1181 |
|
1182 |
|
1183 lemma Field_bsqr: |
|
1184 "Field (bsqr r) = Field r \<times> Field r" |
|
1185 proof |
|
1186 show "Field (bsqr r) \<le> Field r \<times> Field r" |
|
1187 proof- |
|
1188 {fix a1 a2 assume "(a1,a2) \<in> Field (bsqr r)" |
|
1189 moreover |
|
1190 have "\<And> b1 b2. ((a1,a2),(b1,b2)) \<in> bsqr r \<or> ((b1,b2),(a1,a2)) \<in> bsqr r \<Longrightarrow> |
|
1191 a1 \<in> Field r \<and> a2 \<in> Field r" unfolding bsqr_def by auto |
|
1192 ultimately have "a1 \<in> Field r \<and> a2 \<in> Field r" unfolding Field_def by auto |
|
1193 } |
|
1194 thus ?thesis unfolding Field_def by force |
|
1195 qed |
|
1196 next |
|
1197 show "Field r \<times> Field r \<le> Field (bsqr r)" |
|
1198 proof(auto) |
|
1199 fix a1 a2 assume "a1 \<in> Field r" and "a2 \<in> Field r" |
|
1200 hence "((a1,a2),(a1,a2)) \<in> bsqr r" unfolding bsqr_def by blast |
|
1201 thus "(a1,a2) \<in> Field (bsqr r)" unfolding Field_def by auto |
|
1202 qed |
|
1203 qed |
|
1204 |
|
1205 |
|
1206 lemma bsqr_Refl: "Refl(bsqr r)" |
|
1207 by(unfold refl_on_def Field_bsqr, auto simp add: bsqr_def) |
|
1208 |
|
1209 |
|
1210 lemma bsqr_Trans: |
|
1211 assumes "Well_order r" |
|
1212 shows "trans (bsqr r)" |
|
1213 proof(unfold trans_def, auto) |
|
1214 (* Preliminary facts *) |
|
1215 have Well: "wo_rel r" using assms wo_rel_def by auto |
|
1216 hence Trans: "trans r" using wo_rel.TRANS by auto |
|
1217 have Anti: "antisym r" using wo_rel.ANTISYM Well by auto |
|
1218 hence TransS: "trans(r - Id)" using Trans by (simp add: trans_diff_Id) |
|
1219 (* Main proof *) |
|
1220 fix a1 a2 b1 b2 c1 c2 |
|
1221 assume *: "((a1,a2),(b1,b2)) \<in> bsqr r" and **: "((b1,b2),(c1,c2)) \<in> bsqr r" |
|
1222 hence 0: "{a1,a2,b1,b2,c1,c2} \<le> Field r" unfolding bsqr_def by auto |
|
1223 have 1: "a1 = b1 \<and> a2 = b2 \<or> (wo_rel.max2 r a1 a2, wo_rel.max2 r b1 b2) \<in> r - Id \<or> |
|
1224 wo_rel.max2 r a1 a2 = wo_rel.max2 r b1 b2 \<and> (a1,b1) \<in> r - Id \<or> |
|
1225 wo_rel.max2 r a1 a2 = wo_rel.max2 r b1 b2 \<and> a1 = b1 \<and> (a2,b2) \<in> r - Id" |
|
1226 using * unfolding bsqr_def by auto |
|
1227 have 2: "b1 = c1 \<and> b2 = c2 \<or> (wo_rel.max2 r b1 b2, wo_rel.max2 r c1 c2) \<in> r - Id \<or> |
|
1228 wo_rel.max2 r b1 b2 = wo_rel.max2 r c1 c2 \<and> (b1,c1) \<in> r - Id \<or> |
|
1229 wo_rel.max2 r b1 b2 = wo_rel.max2 r c1 c2 \<and> b1 = c1 \<and> (b2,c2) \<in> r - Id" |
|
1230 using ** unfolding bsqr_def by auto |
|
1231 show "((a1,a2),(c1,c2)) \<in> bsqr r" |
|
1232 proof- |
|
1233 {assume Case1: "a1 = b1 \<and> a2 = b2" |
|
1234 hence ?thesis using ** by simp |
|
1235 } |
|
1236 moreover |
|
1237 {assume Case2: "(wo_rel.max2 r a1 a2, wo_rel.max2 r b1 b2) \<in> r - Id" |
|
1238 {assume Case21: "b1 = c1 \<and> b2 = c2" |
|
1239 hence ?thesis using * by simp |
|
1240 } |
|
1241 moreover |
|
1242 {assume Case22: "(wo_rel.max2 r b1 b2, wo_rel.max2 r c1 c2) \<in> r - Id" |
|
1243 hence "(wo_rel.max2 r a1 a2, wo_rel.max2 r c1 c2) \<in> r - Id" |
|
1244 using Case2 TransS trans_def[of "r - Id"] by blast |
|
1245 hence ?thesis using 0 unfolding bsqr_def by auto |
|
1246 } |
|
1247 moreover |
|
1248 {assume Case23_4: "wo_rel.max2 r b1 b2 = wo_rel.max2 r c1 c2" |
|
1249 hence ?thesis using Case2 0 unfolding bsqr_def by auto |
|
1250 } |
|
1251 ultimately have ?thesis using 0 2 by auto |
|
1252 } |
|
1253 moreover |
|
1254 {assume Case3: "wo_rel.max2 r a1 a2 = wo_rel.max2 r b1 b2 \<and> (a1,b1) \<in> r - Id" |
|
1255 {assume Case31: "b1 = c1 \<and> b2 = c2" |
|
1256 hence ?thesis using * by simp |
|
1257 } |
|
1258 moreover |
|
1259 {assume Case32: "(wo_rel.max2 r b1 b2, wo_rel.max2 r c1 c2) \<in> r - Id" |
|
1260 hence ?thesis using Case3 0 unfolding bsqr_def by auto |
|
1261 } |
|
1262 moreover |
|
1263 {assume Case33: "wo_rel.max2 r b1 b2 = wo_rel.max2 r c1 c2 \<and> (b1,c1) \<in> r - Id" |
|
1264 hence "(a1,c1) \<in> r - Id" |
|
1265 using Case3 TransS trans_def[of "r - Id"] by blast |
|
1266 hence ?thesis using Case3 Case33 0 unfolding bsqr_def by auto |
|
1267 } |
|
1268 moreover |
|
1269 {assume Case33: "wo_rel.max2 r b1 b2 = wo_rel.max2 r c1 c2 \<and> b1 = c1" |
|
1270 hence ?thesis using Case3 0 unfolding bsqr_def by auto |
|
1271 } |
|
1272 ultimately have ?thesis using 0 2 by auto |
|
1273 } |
|
1274 moreover |
|
1275 {assume Case4: "wo_rel.max2 r a1 a2 = wo_rel.max2 r b1 b2 \<and> a1 = b1 \<and> (a2,b2) \<in> r - Id" |
|
1276 {assume Case41: "b1 = c1 \<and> b2 = c2" |
|
1277 hence ?thesis using * by simp |
|
1278 } |
|
1279 moreover |
|
1280 {assume Case42: "(wo_rel.max2 r b1 b2, wo_rel.max2 r c1 c2) \<in> r - Id" |
|
1281 hence ?thesis using Case4 0 unfolding bsqr_def by force |
|
1282 } |
|
1283 moreover |
|
1284 {assume Case43: "wo_rel.max2 r b1 b2 = wo_rel.max2 r c1 c2 \<and> (b1,c1) \<in> r - Id" |
|
1285 hence ?thesis using Case4 0 unfolding bsqr_def by auto |
|
1286 } |
|
1287 moreover |
|
1288 {assume Case44: "wo_rel.max2 r b1 b2 = wo_rel.max2 r c1 c2 \<and> b1 = c1 \<and> (b2,c2) \<in> r - Id" |
|
1289 hence "(a2,c2) \<in> r - Id" |
|
1290 using Case4 TransS trans_def[of "r - Id"] by blast |
|
1291 hence ?thesis using Case4 Case44 0 unfolding bsqr_def by auto |
|
1292 } |
|
1293 ultimately have ?thesis using 0 2 by auto |
|
1294 } |
|
1295 ultimately show ?thesis using 0 1 by auto |
|
1296 qed |
|
1297 qed |
|
1298 |
|
1299 |
|
1300 lemma bsqr_antisym: |
|
1301 assumes "Well_order r" |
|
1302 shows "antisym (bsqr r)" |
|
1303 proof(unfold antisym_def, clarify) |
|
1304 (* Preliminary facts *) |
|
1305 have Well: "wo_rel r" using assms wo_rel_def by auto |
|
1306 hence Trans: "trans r" using wo_rel.TRANS by auto |
|
1307 have Anti: "antisym r" using wo_rel.ANTISYM Well by auto |
|
1308 hence TransS: "trans(r - Id)" using Trans by (simp add: trans_diff_Id) |
|
1309 hence IrrS: "\<forall>a b. \<not>((a,b) \<in> r - Id \<and> (b,a) \<in> r - Id)" |
|
1310 using Anti trans_def[of "r - Id"] antisym_def[of "r - Id"] by blast |
|
1311 (* Main proof *) |
|
1312 fix a1 a2 b1 b2 |
|
1313 assume *: "((a1,a2),(b1,b2)) \<in> bsqr r" and **: "((b1,b2),(a1,a2)) \<in> bsqr r" |
|
1314 hence 0: "{a1,a2,b1,b2} \<le> Field r" unfolding bsqr_def by auto |
|
1315 have 1: "a1 = b1 \<and> a2 = b2 \<or> (wo_rel.max2 r a1 a2, wo_rel.max2 r b1 b2) \<in> r - Id \<or> |
|
1316 wo_rel.max2 r a1 a2 = wo_rel.max2 r b1 b2 \<and> (a1,b1) \<in> r - Id \<or> |
|
1317 wo_rel.max2 r a1 a2 = wo_rel.max2 r b1 b2 \<and> a1 = b1 \<and> (a2,b2) \<in> r - Id" |
|
1318 using * unfolding bsqr_def by auto |
|
1319 have 2: "b1 = a1 \<and> b2 = a2 \<or> (wo_rel.max2 r b1 b2, wo_rel.max2 r a1 a2) \<in> r - Id \<or> |
|
1320 wo_rel.max2 r b1 b2 = wo_rel.max2 r a1 a2 \<and> (b1,a1) \<in> r - Id \<or> |
|
1321 wo_rel.max2 r b1 b2 = wo_rel.max2 r a1 a2 \<and> b1 = a1 \<and> (b2,a2) \<in> r - Id" |
|
1322 using ** unfolding bsqr_def by auto |
|
1323 show "a1 = b1 \<and> a2 = b2" |
|
1324 proof- |
|
1325 {assume Case1: "(wo_rel.max2 r a1 a2, wo_rel.max2 r b1 b2) \<in> r - Id" |
|
1326 {assume Case11: "(wo_rel.max2 r b1 b2, wo_rel.max2 r a1 a2) \<in> r - Id" |
|
1327 hence False using Case1 IrrS by blast |
|
1328 } |
|
1329 moreover |
|
1330 {assume Case12_3: "wo_rel.max2 r b1 b2 = wo_rel.max2 r a1 a2" |
|
1331 hence False using Case1 by auto |
|
1332 } |
|
1333 ultimately have ?thesis using 0 2 by auto |
|
1334 } |
|
1335 moreover |
|
1336 {assume Case2: "wo_rel.max2 r a1 a2 = wo_rel.max2 r b1 b2 \<and> (a1,b1) \<in> r - Id" |
|
1337 {assume Case21: "(wo_rel.max2 r b1 b2, wo_rel.max2 r a1 a2) \<in> r - Id" |
|
1338 hence False using Case2 by auto |
|
1339 } |
|
1340 moreover |
|
1341 {assume Case22: "(b1,a1) \<in> r - Id" |
|
1342 hence False using Case2 IrrS by blast |
|
1343 } |
|
1344 moreover |
|
1345 {assume Case23: "b1 = a1" |
|
1346 hence False using Case2 by auto |
|
1347 } |
|
1348 ultimately have ?thesis using 0 2 by auto |
|
1349 } |
|
1350 moreover |
|
1351 {assume Case3: "wo_rel.max2 r a1 a2 = wo_rel.max2 r b1 b2 \<and> a1 = b1 \<and> (a2,b2) \<in> r - Id" |
|
1352 moreover |
|
1353 {assume Case31: "(wo_rel.max2 r b1 b2, wo_rel.max2 r a1 a2) \<in> r - Id" |
|
1354 hence False using Case3 by auto |
|
1355 } |
|
1356 moreover |
|
1357 {assume Case32: "(b1,a1) \<in> r - Id" |
|
1358 hence False using Case3 by auto |
|
1359 } |
|
1360 moreover |
|
1361 {assume Case33: "(b2,a2) \<in> r - Id" |
|
1362 hence False using Case3 IrrS by blast |
|
1363 } |
|
1364 ultimately have ?thesis using 0 2 by auto |
|
1365 } |
|
1366 ultimately show ?thesis using 0 1 by blast |
|
1367 qed |
|
1368 qed |
|
1369 |
|
1370 |
|
1371 lemma bsqr_Total: |
|
1372 assumes "Well_order r" |
|
1373 shows "Total(bsqr r)" |
|
1374 proof- |
|
1375 (* Preliminary facts *) |
|
1376 have Well: "wo_rel r" using assms wo_rel_def by auto |
|
1377 hence Total: "\<forall>a \<in> Field r. \<forall>b \<in> Field r. (a,b) \<in> r \<or> (b,a) \<in> r" |
|
1378 using wo_rel.TOTALS by auto |
|
1379 (* Main proof *) |
|
1380 {fix a1 a2 b1 b2 assume "{(a1,a2), (b1,b2)} \<le> Field(bsqr r)" |
|
1381 hence 0: "a1 \<in> Field r \<and> a2 \<in> Field r \<and> b1 \<in> Field r \<and> b2 \<in> Field r" |
|
1382 using Field_bsqr by blast |
|
1383 have "((a1,a2) = (b1,b2) \<or> ((a1,a2),(b1,b2)) \<in> bsqr r \<or> ((b1,b2),(a1,a2)) \<in> bsqr r)" |
|
1384 proof(rule wo_rel.cases_Total[of r a1 a2], clarsimp simp add: Well, simp add: 0) |
|
1385 (* Why didn't clarsimp simp add: Well 0 do the same job? *) |
|
1386 assume Case1: "(a1,a2) \<in> r" |
|
1387 hence 1: "wo_rel.max2 r a1 a2 = a2" |
|
1388 using Well 0 by (simp add: wo_rel.max2_equals2) |
|
1389 show ?thesis |
|
1390 proof(rule wo_rel.cases_Total[of r b1 b2], clarsimp simp add: Well, simp add: 0) |
|
1391 assume Case11: "(b1,b2) \<in> r" |
|
1392 hence 2: "wo_rel.max2 r b1 b2 = b2" |
|
1393 using Well 0 by (simp add: wo_rel.max2_equals2) |
|
1394 show ?thesis |
|
1395 proof(rule wo_rel.cases_Total3[of r a2 b2], clarsimp simp add: Well, simp add: 0) |
|
1396 assume Case111: "(a2,b2) \<in> r - Id \<or> (b2,a2) \<in> r - Id" |
|
1397 thus ?thesis using 0 1 2 unfolding bsqr_def by auto |
|
1398 next |
|
1399 assume Case112: "a2 = b2" |
|
1400 show ?thesis |
|
1401 proof(rule wo_rel.cases_Total3[of r a1 b1], clarsimp simp add: Well, simp add: 0) |
|
1402 assume Case1121: "(a1,b1) \<in> r - Id \<or> (b1,a1) \<in> r - Id" |
|
1403 thus ?thesis using 0 1 2 Case112 unfolding bsqr_def by auto |
|
1404 next |
|
1405 assume Case1122: "a1 = b1" |
|
1406 thus ?thesis using Case112 by auto |
|
1407 qed |
|
1408 qed |
|
1409 next |
|
1410 assume Case12: "(b2,b1) \<in> r" |
|
1411 hence 3: "wo_rel.max2 r b1 b2 = b1" using Well 0 by (simp add: wo_rel.max2_equals1) |
|
1412 show ?thesis |
|
1413 proof(rule wo_rel.cases_Total3[of r a2 b1], clarsimp simp add: Well, simp add: 0) |
|
1414 assume Case121: "(a2,b1) \<in> r - Id \<or> (b1,a2) \<in> r - Id" |
|
1415 thus ?thesis using 0 1 3 unfolding bsqr_def by auto |
|
1416 next |
|
1417 assume Case122: "a2 = b1" |
|
1418 show ?thesis |
|
1419 proof(rule wo_rel.cases_Total3[of r a1 b1], clarsimp simp add: Well, simp add: 0) |
|
1420 assume Case1221: "(a1,b1) \<in> r - Id \<or> (b1,a1) \<in> r - Id" |
|
1421 thus ?thesis using 0 1 3 Case122 unfolding bsqr_def by auto |
|
1422 next |
|
1423 assume Case1222: "a1 = b1" |
|
1424 show ?thesis |
|
1425 proof(rule wo_rel.cases_Total3[of r a2 b2], clarsimp simp add: Well, simp add: 0) |
|
1426 assume Case12221: "(a2,b2) \<in> r - Id \<or> (b2,a2) \<in> r - Id" |
|
1427 thus ?thesis using 0 1 3 Case122 Case1222 unfolding bsqr_def by auto |
|
1428 next |
|
1429 assume Case12222: "a2 = b2" |
|
1430 thus ?thesis using Case122 Case1222 by auto |
|
1431 qed |
|
1432 qed |
|
1433 qed |
|
1434 qed |
|
1435 next |
|
1436 assume Case2: "(a2,a1) \<in> r" |
|
1437 hence 1: "wo_rel.max2 r a1 a2 = a1" using Well 0 by (simp add: wo_rel.max2_equals1) |
|
1438 show ?thesis |
|
1439 proof(rule wo_rel.cases_Total[of r b1 b2], clarsimp simp add: Well, simp add: 0) |
|
1440 assume Case21: "(b1,b2) \<in> r" |
|
1441 hence 2: "wo_rel.max2 r b1 b2 = b2" using Well 0 by (simp add: wo_rel.max2_equals2) |
|
1442 show ?thesis |
|
1443 proof(rule wo_rel.cases_Total3[of r a1 b2], clarsimp simp add: Well, simp add: 0) |
|
1444 assume Case211: "(a1,b2) \<in> r - Id \<or> (b2,a1) \<in> r - Id" |
|
1445 thus ?thesis using 0 1 2 unfolding bsqr_def by auto |
|
1446 next |
|
1447 assume Case212: "a1 = b2" |
|
1448 show ?thesis |
|
1449 proof(rule wo_rel.cases_Total3[of r a1 b1], clarsimp simp add: Well, simp add: 0) |
|
1450 assume Case2121: "(a1,b1) \<in> r - Id \<or> (b1,a1) \<in> r - Id" |
|
1451 thus ?thesis using 0 1 2 Case212 unfolding bsqr_def by auto |
|
1452 next |
|
1453 assume Case2122: "a1 = b1" |
|
1454 show ?thesis |
|
1455 proof(rule wo_rel.cases_Total3[of r a2 b2], clarsimp simp add: Well, simp add: 0) |
|
1456 assume Case21221: "(a2,b2) \<in> r - Id \<or> (b2,a2) \<in> r - Id" |
|
1457 thus ?thesis using 0 1 2 Case212 Case2122 unfolding bsqr_def by auto |
|
1458 next |
|
1459 assume Case21222: "a2 = b2" |
|
1460 thus ?thesis using Case2122 Case212 by auto |
|
1461 qed |
|
1462 qed |
|
1463 qed |
|
1464 next |
|
1465 assume Case22: "(b2,b1) \<in> r" |
|
1466 hence 3: "wo_rel.max2 r b1 b2 = b1" using Well 0 by (simp add: wo_rel.max2_equals1) |
|
1467 show ?thesis |
|
1468 proof(rule wo_rel.cases_Total3[of r a1 b1], clarsimp simp add: Well, simp add: 0) |
|
1469 assume Case221: "(a1,b1) \<in> r - Id \<or> (b1,a1) \<in> r - Id" |
|
1470 thus ?thesis using 0 1 3 unfolding bsqr_def by auto |
|
1471 next |
|
1472 assume Case222: "a1 = b1" |
|
1473 show ?thesis |
|
1474 proof(rule wo_rel.cases_Total3[of r a2 b2], clarsimp simp add: Well, simp add: 0) |
|
1475 assume Case2221: "(a2,b2) \<in> r - Id \<or> (b2,a2) \<in> r - Id" |
|
1476 thus ?thesis using 0 1 3 Case222 unfolding bsqr_def by auto |
|
1477 next |
|
1478 assume Case2222: "a2 = b2" |
|
1479 thus ?thesis using Case222 by auto |
|
1480 qed |
|
1481 qed |
|
1482 qed |
|
1483 qed |
|
1484 } |
|
1485 thus ?thesis unfolding total_on_def by fast |
|
1486 qed |
|
1487 |
|
1488 |
|
1489 lemma bsqr_Linear_order: |
|
1490 assumes "Well_order r" |
|
1491 shows "Linear_order(bsqr r)" |
|
1492 unfolding order_on_defs |
|
1493 using assms bsqr_Refl bsqr_Trans bsqr_antisym bsqr_Total by blast |
|
1494 |
|
1495 |
|
1496 lemma bsqr_Well_order: |
|
1497 assumes "Well_order r" |
|
1498 shows "Well_order(bsqr r)" |
|
1499 using assms |
|
1500 proof(simp add: bsqr_Linear_order Linear_order_Well_order_iff, intro allI impI) |
|
1501 have 0: "\<forall>A \<le> Field r. A \<noteq> {} \<longrightarrow> (\<exists>a \<in> A. \<forall>a' \<in> A. (a,a') \<in> r)" |
|
1502 using assms well_order_on_def Linear_order_Well_order_iff by blast |
|
1503 fix D assume *: "D \<le> Field (bsqr r)" and **: "D \<noteq> {}" |
|
1504 hence 1: "D \<le> Field r \<times> Field r" unfolding Field_bsqr by simp |
|
1505 (* *) |
|
1506 obtain M where M_def: "M = {wo_rel.max2 r a1 a2| a1 a2. (a1,a2) \<in> D}" by blast |
|
1507 have "M \<noteq> {}" using 1 M_def ** by auto |
|
1508 moreover |
|
1509 have "M \<le> Field r" unfolding M_def |
|
1510 using 1 assms wo_rel_def[of r] wo_rel.max2_among[of r] by fastforce |
|
1511 ultimately obtain m where m_min: "m \<in> M \<and> (\<forall>a \<in> M. (m,a) \<in> r)" |
|
1512 using 0 by blast |
|
1513 (* *) |
|
1514 obtain A1 where A1_def: "A1 = {a1. \<exists>a2. (a1,a2) \<in> D \<and> wo_rel.max2 r a1 a2 = m}" by blast |
|
1515 have "A1 \<le> Field r" unfolding A1_def using 1 by auto |
|
1516 moreover have "A1 \<noteq> {}" unfolding A1_def using m_min unfolding M_def by blast |
|
1517 ultimately obtain a1 where a1_min: "a1 \<in> A1 \<and> (\<forall>a \<in> A1. (a1,a) \<in> r)" |
|
1518 using 0 by blast |
|
1519 (* *) |
|
1520 obtain A2 where A2_def: "A2 = {a2. (a1,a2) \<in> D \<and> wo_rel.max2 r a1 a2 = m}" by blast |
|
1521 have "A2 \<le> Field r" unfolding A2_def using 1 by auto |
|
1522 moreover have "A2 \<noteq> {}" unfolding A2_def |
|
1523 using m_min a1_min unfolding A1_def M_def by blast |
|
1524 ultimately obtain a2 where a2_min: "a2 \<in> A2 \<and> (\<forall>a \<in> A2. (a2,a) \<in> r)" |
|
1525 using 0 by blast |
|
1526 (* *) |
|
1527 have 2: "wo_rel.max2 r a1 a2 = m" |
|
1528 using a1_min a2_min unfolding A1_def A2_def by auto |
|
1529 have 3: "(a1,a2) \<in> D" using a2_min unfolding A2_def by auto |
|
1530 (* *) |
|
1531 moreover |
|
1532 {fix b1 b2 assume ***: "(b1,b2) \<in> D" |
|
1533 hence 4: "{a1,a2,b1,b2} \<le> Field r" using 1 3 by blast |
|
1534 have 5: "(wo_rel.max2 r a1 a2, wo_rel.max2 r b1 b2) \<in> r" |
|
1535 using *** a1_min a2_min m_min unfolding A1_def A2_def M_def by auto |
|
1536 have "((a1,a2),(b1,b2)) \<in> bsqr r" |
|
1537 proof(cases "wo_rel.max2 r a1 a2 = wo_rel.max2 r b1 b2") |
|
1538 assume Case1: "wo_rel.max2 r a1 a2 \<noteq> wo_rel.max2 r b1 b2" |
|
1539 thus ?thesis unfolding bsqr_def using 4 5 by auto |
|
1540 next |
|
1541 assume Case2: "wo_rel.max2 r a1 a2 = wo_rel.max2 r b1 b2" |
|
1542 hence "b1 \<in> A1" unfolding A1_def using 2 *** by auto |
|
1543 hence 6: "(a1,b1) \<in> r" using a1_min by auto |
|
1544 show ?thesis |
|
1545 proof(cases "a1 = b1") |
|
1546 assume Case21: "a1 \<noteq> b1" |
|
1547 thus ?thesis unfolding bsqr_def using 4 Case2 6 by auto |
|
1548 next |
|
1549 assume Case22: "a1 = b1" |
|
1550 hence "b2 \<in> A2" unfolding A2_def using 2 *** Case2 by auto |
|
1551 hence 7: "(a2,b2) \<in> r" using a2_min by auto |
|
1552 thus ?thesis unfolding bsqr_def using 4 7 Case2 Case22 by auto |
|
1553 qed |
|
1554 qed |
|
1555 } |
|
1556 (* *) |
|
1557 ultimately show "\<exists>d \<in> D. \<forall>d' \<in> D. (d,d') \<in> bsqr r" by fastforce |
|
1558 qed |
|
1559 |
|
1560 |
|
1561 lemma bsqr_max2: |
|
1562 assumes WELL: "Well_order r" and LEQ: "((a1,a2),(b1,b2)) \<in> bsqr r" |
|
1563 shows "(wo_rel.max2 r a1 a2, wo_rel.max2 r b1 b2) \<in> r" |
|
1564 proof- |
|
1565 have "{(a1,a2),(b1,b2)} \<le> Field(bsqr r)" |
|
1566 using LEQ unfolding Field_def by auto |
|
1567 hence "{a1,a2,b1,b2} \<le> Field r" unfolding Field_bsqr by auto |
|
1568 hence "{wo_rel.max2 r a1 a2, wo_rel.max2 r b1 b2} \<le> Field r" |
|
1569 using WELL wo_rel_def[of r] wo_rel.max2_among[of r] by fastforce |
|
1570 moreover have "(wo_rel.max2 r a1 a2, wo_rel.max2 r b1 b2) \<in> r \<or> wo_rel.max2 r a1 a2 = wo_rel.max2 r b1 b2" |
|
1571 using LEQ unfolding bsqr_def by auto |
|
1572 ultimately show ?thesis using WELL unfolding order_on_defs refl_on_def by auto |
|
1573 qed |
|
1574 |
|
1575 |
|
1576 lemma bsqr_ofilter: |
|
1577 assumes WELL: "Well_order r" and |
|
1578 OF: "wo_rel.ofilter (bsqr r) D" and SUB: "D < Field r \<times> Field r" and |
|
1579 NE: "\<not> (\<exists>a. Field r = under r a)" |
|
1580 shows "\<exists>A. wo_rel.ofilter r A \<and> A < Field r \<and> D \<le> A \<times> A" |
|
1581 proof- |
|
1582 let ?r' = "bsqr r" |
|
1583 have Well: "wo_rel r" using WELL wo_rel_def by blast |
|
1584 hence Trans: "trans r" using wo_rel.TRANS by blast |
|
1585 have Well': "Well_order ?r' \<and> wo_rel ?r'" |
|
1586 using WELL bsqr_Well_order wo_rel_def by blast |
|
1587 (* *) |
|
1588 have "D < Field ?r'" unfolding Field_bsqr using SUB . |
|
1589 with OF obtain a1 and a2 where |
|
1590 "(a1,a2) \<in> Field ?r'" and 1: "D = underS ?r' (a1,a2)" |
|
1591 using Well' wo_rel.ofilter_underS_Field[of ?r' D] by auto |
|
1592 hence 2: "{a1,a2} \<le> Field r" unfolding Field_bsqr by auto |
|
1593 let ?m = "wo_rel.max2 r a1 a2" |
|
1594 have "D \<le> (under r ?m) \<times> (under r ?m)" |
|
1595 proof(unfold 1) |
|
1596 {fix b1 b2 |
|
1597 let ?n = "wo_rel.max2 r b1 b2" |
|
1598 assume "(b1,b2) \<in> underS ?r' (a1,a2)" |
|
1599 hence 3: "((b1,b2),(a1,a2)) \<in> ?r'" |
|
1600 unfolding underS_def by blast |
|
1601 hence "(?n,?m) \<in> r" using WELL by (simp add: bsqr_max2) |
|
1602 moreover |
|
1603 {have "(b1,b2) \<in> Field ?r'" using 3 unfolding Field_def by auto |
|
1604 hence "{b1,b2} \<le> Field r" unfolding Field_bsqr by auto |
|
1605 hence "(b1,?n) \<in> r \<and> (b2,?n) \<in> r" |
|
1606 using Well by (simp add: wo_rel.max2_greater) |
|
1607 } |
|
1608 ultimately have "(b1,?m) \<in> r \<and> (b2,?m) \<in> r" |
|
1609 using Trans trans_def[of r] by blast |
|
1610 hence "(b1,b2) \<in> (under r ?m) \<times> (under r ?m)" unfolding under_def by simp} |
|
1611 thus "underS ?r' (a1,a2) \<le> (under r ?m) \<times> (under r ?m)" by auto |
|
1612 qed |
|
1613 moreover have "wo_rel.ofilter r (under r ?m)" |
|
1614 using Well by (simp add: wo_rel.under_ofilter) |
|
1615 moreover have "under r ?m < Field r" |
|
1616 using NE under_Field[of r ?m] by blast |
|
1617 ultimately show ?thesis by blast |
|
1618 qed |
|
1619 |
|
1620 definition Func where |
|
1621 "Func A B = {f . (\<forall> a \<in> A. f a \<in> B) \<and> (\<forall> a. a \<notin> A \<longrightarrow> f a = undefined)}" |
|
1622 |
|
1623 lemma Func_empty: |
|
1624 "Func {} B = {\<lambda>x. undefined}" |
|
1625 unfolding Func_def by auto |
|
1626 |
|
1627 lemma Func_elim: |
|
1628 assumes "g \<in> Func A B" and "a \<in> A" |
|
1629 shows "\<exists> b. b \<in> B \<and> g a = b" |
|
1630 using assms unfolding Func_def by (cases "g a = undefined") auto |
|
1631 |
|
1632 definition curr where |
|
1633 "curr A f \<equiv> \<lambda> a. if a \<in> A then \<lambda>b. f (a,b) else undefined" |
|
1634 |
|
1635 lemma curr_in: |
|
1636 assumes f: "f \<in> Func (A <*> B) C" |
|
1637 shows "curr A f \<in> Func A (Func B C)" |
|
1638 using assms unfolding curr_def Func_def by auto |
|
1639 |
|
1640 lemma curr_inj: |
|
1641 assumes "f1 \<in> Func (A <*> B) C" and "f2 \<in> Func (A <*> B) C" |
|
1642 shows "curr A f1 = curr A f2 \<longleftrightarrow> f1 = f2" |
|
1643 proof safe |
|
1644 assume c: "curr A f1 = curr A f2" |
|
1645 show "f1 = f2" |
|
1646 proof (rule ext, clarify) |
|
1647 fix a b show "f1 (a, b) = f2 (a, b)" |
|
1648 proof (cases "(a,b) \<in> A <*> B") |
|
1649 case False |
|
1650 thus ?thesis using assms unfolding Func_def by auto |
|
1651 next |
|
1652 case True hence a: "a \<in> A" and b: "b \<in> B" by auto |
|
1653 thus ?thesis |
|
1654 using c unfolding curr_def fun_eq_iff by(elim allE[of _ a]) simp |
|
1655 qed |
|
1656 qed |
|
1657 qed |
|
1658 |
|
1659 lemma curr_surj: |
|
1660 assumes "g \<in> Func A (Func B C)" |
|
1661 shows "\<exists> f \<in> Func (A <*> B) C. curr A f = g" |
|
1662 proof |
|
1663 let ?f = "\<lambda> ab. if fst ab \<in> A \<and> snd ab \<in> B then g (fst ab) (snd ab) else undefined" |
|
1664 show "curr A ?f = g" |
|
1665 proof (rule ext) |
|
1666 fix a show "curr A ?f a = g a" |
|
1667 proof (cases "a \<in> A") |
|
1668 case False |
|
1669 hence "g a = undefined" using assms unfolding Func_def by auto |
|
1670 thus ?thesis unfolding curr_def using False by simp |
|
1671 next |
|
1672 case True |
|
1673 obtain g1 where "g1 \<in> Func B C" and "g a = g1" |
|
1674 using assms using Func_elim[OF assms True] by blast |
|
1675 thus ?thesis using True unfolding Func_def curr_def by auto |
|
1676 qed |
|
1677 qed |
|
1678 show "?f \<in> Func (A <*> B) C" using assms unfolding Func_def mem_Collect_eq by auto |
|
1679 qed |
|
1680 |
|
1681 lemma bij_betw_curr: |
|
1682 "bij_betw (curr A) (Func (A <*> B) C) (Func A (Func B C))" |
|
1683 unfolding bij_betw_def inj_on_def image_def |
|
1684 apply (intro impI conjI ballI) |
|
1685 apply (erule curr_inj[THEN iffD1], assumption+) |
|
1686 apply auto |
|
1687 apply (erule curr_in) |
|
1688 using curr_surj by blast |
|
1689 |
|
1690 definition Func_map where |
|
1691 "Func_map B2 f1 f2 g b2 \<equiv> if b2 \<in> B2 then f1 (g (f2 b2)) else undefined" |
|
1692 |
|
1693 lemma Func_map: |
|
1694 assumes g: "g \<in> Func A2 A1" and f1: "f1 ` A1 \<subseteq> B1" and f2: "f2 ` B2 \<subseteq> A2" |
|
1695 shows "Func_map B2 f1 f2 g \<in> Func B2 B1" |
|
1696 using assms unfolding Func_def Func_map_def mem_Collect_eq by auto |
|
1697 |
|
1698 lemma Func_non_emp: |
|
1699 assumes "B \<noteq> {}" |
|
1700 shows "Func A B \<noteq> {}" |
|
1701 proof- |
|
1702 obtain b where b: "b \<in> B" using assms by auto |
|
1703 hence "(\<lambda> a. if a \<in> A then b else undefined) \<in> Func A B" unfolding Func_def by auto |
|
1704 thus ?thesis by blast |
|
1705 qed |
|
1706 |
|
1707 lemma Func_is_emp: |
|
1708 "Func A B = {} \<longleftrightarrow> A \<noteq> {} \<and> B = {}" (is "?L \<longleftrightarrow> ?R") |
|
1709 proof |
|
1710 assume L: ?L |
|
1711 moreover {assume "A = {}" hence False using L Func_empty by auto} |
|
1712 moreover {assume "B \<noteq> {}" hence False using L Func_non_emp by metis} |
|
1713 ultimately show ?R by blast |
|
1714 next |
|
1715 assume R: ?R |
|
1716 moreover |
|
1717 {fix f assume "f \<in> Func A B" |
|
1718 moreover obtain a where "a \<in> A" using R by blast |
|
1719 ultimately obtain b where "b \<in> B" unfolding Func_def by blast |
|
1720 with R have False by blast |
|
1721 } |
|
1722 thus ?L by blast |
|
1723 qed |
|
1724 |
|
1725 lemma Func_map_surj: |
|
1726 assumes B1: "f1 ` A1 = B1" and A2: "inj_on f2 B2" "f2 ` B2 \<subseteq> A2" |
|
1727 and B2A2: "B2 = {} \<Longrightarrow> A2 = {}" |
|
1728 shows "Func B2 B1 = Func_map B2 f1 f2 ` Func A2 A1" |
|
1729 proof(cases "B2 = {}") |
|
1730 case True |
|
1731 thus ?thesis using B2A2 by (auto simp: Func_empty Func_map_def) |
|
1732 next |
|
1733 case False note B2 = False |
|
1734 show ?thesis |
|
1735 proof safe |
|
1736 fix h assume h: "h \<in> Func B2 B1" |
|
1737 def j1 \<equiv> "inv_into A1 f1" |
|
1738 have "\<forall> a2 \<in> f2 ` B2. \<exists> b2. b2 \<in> B2 \<and> f2 b2 = a2" by blast |
|
1739 then obtain k where k: "\<forall> a2 \<in> f2 ` B2. k a2 \<in> B2 \<and> f2 (k a2) = a2" by metis |
|
1740 {fix b2 assume b2: "b2 \<in> B2" |
|
1741 hence "f2 (k (f2 b2)) = f2 b2" using k A2(2) by auto |
|
1742 moreover have "k (f2 b2) \<in> B2" using b2 A2(2) k by auto |
|
1743 ultimately have "k (f2 b2) = b2" using b2 A2(1) unfolding inj_on_def by blast |
|
1744 } note kk = this |
|
1745 obtain b22 where b22: "b22 \<in> B2" using B2 by auto |
|
1746 def j2 \<equiv> "\<lambda> a2. if a2 \<in> f2 ` B2 then k a2 else b22" |
|
1747 have j2A2: "j2 ` A2 \<subseteq> B2" unfolding j2_def using k b22 by auto |
|
1748 have j2: "\<And> b2. b2 \<in> B2 \<Longrightarrow> j2 (f2 b2) = b2" |
|
1749 using kk unfolding j2_def by auto |
|
1750 def g \<equiv> "Func_map A2 j1 j2 h" |
|
1751 have "Func_map B2 f1 f2 g = h" |
|
1752 proof (rule ext) |
|
1753 fix b2 show "Func_map B2 f1 f2 g b2 = h b2" |
|
1754 proof(cases "b2 \<in> B2") |
|
1755 case True |
|
1756 show ?thesis |
|
1757 proof (cases "h b2 = undefined") |
|
1758 case True |
|
1759 hence b1: "h b2 \<in> f1 ` A1" using h `b2 \<in> B2` unfolding B1 Func_def by auto |
|
1760 show ?thesis using A2 f_inv_into_f[OF b1] |
|
1761 unfolding True g_def Func_map_def j1_def j2[OF `b2 \<in> B2`] by auto |
|
1762 qed(insert A2 True j2[OF True] h B1, unfold j1_def g_def Func_def Func_map_def, |
|
1763 auto intro: f_inv_into_f) |
|
1764 qed(insert h, unfold Func_def Func_map_def, auto) |
|
1765 qed |
|
1766 moreover have "g \<in> Func A2 A1" unfolding g_def apply(rule Func_map[OF h]) |
|
1767 using inv_into_into j2A2 B1 A2 inv_into_into |
|
1768 unfolding j1_def image_def by fast+ |
|
1769 ultimately show "h \<in> Func_map B2 f1 f2 ` Func A2 A1" |
|
1770 unfolding Func_map_def[abs_def] unfolding image_def by auto |
|
1771 qed(insert B1 Func_map[OF _ _ A2(2)], auto) |
|
1772 qed |
|
1773 |
|
1774 end |