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