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