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