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