src/HOL/BNF_Wellorder_Constructions.thy
 author wenzelm Sun Sep 18 20:33:48 2016 +0200 (2016-09-18) changeset 63915 bab633745c7f parent 63561 fba08009ff3e child 67091 1393c2340eec permissions -rw-r--r--
tuned proofs;
     1 (*  Title:      HOL/BNF_Wellorder_Constructions.thy

     2     Author:     Andrei Popescu, TU Muenchen

     3     Copyright   2012

     4

     5 Constructions on wellorders as needed by bounded natural functors.

     6 *)

     7

     8 section \<open>Constructions on Wellorders as Needed by Bounded Natural Functors\<close>

     9

    10 theory BNF_Wellorder_Constructions

    11 imports BNF_Wellorder_Embedding

    12 begin

    13

    14 text \<open>In this section, we study basic constructions on well-orders, such as restriction to

    15 a set/order filter, copy via direct images, ordinal-like sum of disjoint well-orders,

    16 and bounded square.  We also define between well-orders

    17 the relations \<open>ordLeq\<close>, of being embedded (abbreviated \<open>\<le>o\<close>),

    18 \<open>ordLess\<close>, of being strictly embedded (abbreviated \<open><o\<close>), and

    19 \<open>ordIso\<close>, of being isomorphic (abbreviated \<open>=o\<close>).  We study the

    20 connections between these relations, order filters, and the aforementioned constructions.

    21 A main result of this section is that \<open><o\<close> is well-founded.\<close>

    22

    23

    24 subsection \<open>Restriction to a set\<close>

    25

    26 abbreviation Restr :: "'a rel \<Rightarrow> 'a set \<Rightarrow> 'a rel"

    27 where "Restr r A \<equiv> r Int (A \<times> A)"

    28

    29 lemma Restr_subset:

    30 "A \<le> B \<Longrightarrow> Restr (Restr r B) A = Restr r A"

    31 by blast

    32

    33 lemma Restr_Field: "Restr r (Field r) = r"

    34 unfolding Field_def by auto

    35

    36 lemma Refl_Restr: "Refl r \<Longrightarrow> Refl(Restr r A)"

    37 unfolding refl_on_def Field_def by auto

    38

    39 lemma linear_order_on_Restr:

    40   "linear_order_on A r \<Longrightarrow> linear_order_on (A \<inter> above r x) (Restr r (above r x))"

    41 by(simp add: order_on_defs refl_on_def trans_def antisym_def total_on_def)(safe; blast)

    42

    43 lemma antisym_Restr:

    44 "antisym r \<Longrightarrow> antisym(Restr r A)"

    45 unfolding antisym_def Field_def by auto

    46

    47 lemma Total_Restr:

    48 "Total r \<Longrightarrow> Total(Restr r A)"

    49 unfolding total_on_def Field_def by auto

    50

    51 lemma trans_Restr:

    52 "trans r \<Longrightarrow> trans(Restr r A)"

    53 unfolding trans_def Field_def by blast

    54

    55 lemma Preorder_Restr:

    56 "Preorder r \<Longrightarrow> Preorder(Restr r A)"

    57 unfolding preorder_on_def by (simp add: Refl_Restr trans_Restr)

    58

    59 lemma Partial_order_Restr:

    60 "Partial_order r \<Longrightarrow> Partial_order(Restr r A)"

    61 unfolding partial_order_on_def by (simp add: Preorder_Restr antisym_Restr)

    62

    63 lemma Linear_order_Restr:

    64 "Linear_order r \<Longrightarrow> Linear_order(Restr r A)"

    65 unfolding linear_order_on_def by (simp add: Partial_order_Restr Total_Restr)

    66

    67 lemma Well_order_Restr:

    68 assumes "Well_order r"

    69 shows "Well_order(Restr r A)"

    70 proof-

    71   have "Restr r A - Id \<le> r - Id" using Restr_subset by blast

    72   hence "wf(Restr r A - Id)" using assms

    73   using well_order_on_def wf_subset by blast

    74   thus ?thesis using assms unfolding well_order_on_def

    75   by (simp add: Linear_order_Restr)

    76 qed

    77

    78 lemma Field_Restr_subset: "Field(Restr r A) \<le> A"

    79 by (auto simp add: Field_def)

    80

    81 lemma Refl_Field_Restr:

    82 "Refl r \<Longrightarrow> Field(Restr r A) = (Field r) Int A"

    83 unfolding refl_on_def Field_def by blast

    84

    85 lemma Refl_Field_Restr2:

    86 "\<lbrakk>Refl r; A \<le> Field r\<rbrakk> \<Longrightarrow> Field(Restr r A) = A"

    87 by (auto simp add: Refl_Field_Restr)

    88

    89 lemma well_order_on_Restr:

    90 assumes WELL: "Well_order r" and SUB: "A \<le> Field r"

    91 shows "well_order_on A (Restr r A)"

    92 using assms

    93 using Well_order_Restr[of r A] Refl_Field_Restr2[of r A]

    94      order_on_defs[of "Field r" r] by auto

    95

    96

    97 subsection \<open>Order filters versus restrictions and embeddings\<close>

    98

    99 lemma Field_Restr_ofilter:

   100 "\<lbrakk>Well_order r; wo_rel.ofilter r A\<rbrakk> \<Longrightarrow> Field(Restr r A) = A"

   101 by (auto simp add: wo_rel_def wo_rel.ofilter_def wo_rel.REFL Refl_Field_Restr2)

   102

   103 lemma ofilter_Restr_under:

   104 assumes WELL: "Well_order r" and OF: "wo_rel.ofilter r A" and IN: "a \<in> A"

   105 shows "under (Restr r A) a = under r a"

   106 using assms wo_rel_def

   107 proof(auto simp add: wo_rel.ofilter_def under_def)

   108   fix b assume *: "a \<in> A" and "(b,a) \<in> r"

   109   hence "b \<in> under r a \<and> a \<in> Field r"

   110   unfolding under_def using Field_def by fastforce

   111   thus "b \<in> A" using * assms by (auto simp add: wo_rel_def wo_rel.ofilter_def)

   112 qed

   113

   114 lemma ofilter_embed:

   115 assumes "Well_order r"

   116 shows "wo_rel.ofilter r A = (A \<le> Field r \<and> embed (Restr r A) r id)"

   117 proof

   118   assume *: "wo_rel.ofilter r A"

   119   show "A \<le> Field r \<and> embed (Restr r A) r id"

   120   proof(unfold embed_def, auto)

   121     fix a assume "a \<in> A" thus "a \<in> Field r" using assms *

   122     by (auto simp add: wo_rel_def wo_rel.ofilter_def)

   123   next

   124     fix a assume "a \<in> Field (Restr r A)"

   125     thus "bij_betw id (under (Restr r A) a) (under r a)" using assms *

   126     by (simp add: ofilter_Restr_under Field_Restr_ofilter)

   127   qed

   128 next

   129   assume *: "A \<le> Field r \<and> embed (Restr r A) r id"

   130   hence "Field(Restr r A) \<le> Field r"

   131   using assms  embed_Field[of "Restr r A" r id] id_def

   132         Well_order_Restr[of r] by auto

   133   {fix a assume "a \<in> A"

   134    hence "a \<in> Field(Restr r A)" using * assms

   135    by (simp add: order_on_defs Refl_Field_Restr2)

   136    hence "bij_betw id (under (Restr r A) a) (under r a)"

   137    using * unfolding embed_def by auto

   138    hence "under r a \<le> under (Restr r A) a"

   139    unfolding bij_betw_def by auto

   140    also have "\<dots> \<le> Field(Restr r A)" by (simp add: under_Field)

   141    also have "\<dots> \<le> A" by (simp add: Field_Restr_subset)

   142    finally have "under r a \<le> A" .

   143   }

   144   thus "wo_rel.ofilter r A" using assms * by (simp add: wo_rel_def wo_rel.ofilter_def)

   145 qed

   146

   147 lemma ofilter_Restr_Int:

   148 assumes WELL: "Well_order r" and OFA: "wo_rel.ofilter r A"

   149 shows "wo_rel.ofilter (Restr r B) (A Int B)"

   150 proof-

   151   let ?rB = "Restr r B"

   152   have Well: "wo_rel r" unfolding wo_rel_def using WELL .

   153   hence Refl: "Refl r" by (simp add: wo_rel.REFL)

   154   hence Field: "Field ?rB = Field r Int B"

   155   using Refl_Field_Restr by blast

   156   have WellB: "wo_rel ?rB \<and> Well_order ?rB" using WELL

   157   by (simp add: Well_order_Restr wo_rel_def)

   158   (* Main proof *)

   159   show ?thesis using WellB assms

   160   proof(auto simp add: wo_rel.ofilter_def under_def)

   161     fix a assume "a \<in> A" and *: "a \<in> B"

   162     hence "a \<in> Field r" using OFA Well by (auto simp add: wo_rel.ofilter_def)

   163     with * show "a \<in> Field ?rB" using Field by auto

   164   next

   165     fix a b assume "a \<in> A" and "(b,a) \<in> r"

   166     thus "b \<in> A" using Well OFA by (auto simp add: wo_rel.ofilter_def under_def)

   167   qed

   168 qed

   169

   170 lemma ofilter_Restr_subset:

   171 assumes WELL: "Well_order r" and OFA: "wo_rel.ofilter r A" and SUB: "A \<le> B"

   172 shows "wo_rel.ofilter (Restr r B) A"

   173 proof-

   174   have "A Int B = A" using SUB by blast

   175   thus ?thesis using assms ofilter_Restr_Int[of r A B] by auto

   176 qed

   177

   178 lemma ofilter_subset_embed:

   179 assumes WELL: "Well_order r" and

   180         OFA: "wo_rel.ofilter r A" and OFB: "wo_rel.ofilter r B"

   181 shows "(A \<le> B) = (embed (Restr r A) (Restr r B) id)"

   182 proof-

   183   let ?rA = "Restr r A"  let ?rB = "Restr r B"

   184   have Well: "wo_rel r" unfolding wo_rel_def using WELL .

   185   hence Refl: "Refl r" by (simp add: wo_rel.REFL)

   186   hence FieldA: "Field ?rA = Field r Int A"

   187   using Refl_Field_Restr by blast

   188   have FieldB: "Field ?rB = Field r Int B"

   189   using Refl Refl_Field_Restr by blast

   190   have WellA: "wo_rel ?rA \<and> Well_order ?rA" using WELL

   191   by (simp add: Well_order_Restr wo_rel_def)

   192   have WellB: "wo_rel ?rB \<and> Well_order ?rB" using WELL

   193   by (simp add: Well_order_Restr wo_rel_def)

   194   (* Main proof *)

   195   show ?thesis

   196   proof

   197     assume *: "A \<le> B"

   198     hence "wo_rel.ofilter (Restr r B) A" using assms

   199     by (simp add: ofilter_Restr_subset)

   200     hence "embed (Restr ?rB A) (Restr r B) id"

   201     using WellB ofilter_embed[of "?rB" A] by auto

   202     thus "embed (Restr r A) (Restr r B) id"

   203     using * by (simp add: Restr_subset)

   204   next

   205     assume *: "embed (Restr r A) (Restr r B) id"

   206     {fix a assume **: "a \<in> A"

   207      hence "a \<in> Field r" using Well OFA by (auto simp add: wo_rel.ofilter_def)

   208      with ** FieldA have "a \<in> Field ?rA" by auto

   209      hence "a \<in> Field ?rB" using * WellA embed_Field[of ?rA ?rB id] by auto

   210      hence "a \<in> B" using FieldB by auto

   211     }

   212     thus "A \<le> B" by blast

   213   qed

   214 qed

   215

   216 lemma ofilter_subset_embedS_iso:

   217 assumes WELL: "Well_order r" and

   218         OFA: "wo_rel.ofilter r A" and OFB: "wo_rel.ofilter r B"

   219 shows "((A < B) = (embedS (Restr r A) (Restr r B) id)) \<and>

   220        ((A = B) = (iso (Restr r A) (Restr r B) id))"

   221 proof-

   222   let ?rA = "Restr r A"  let ?rB = "Restr r B"

   223   have Well: "wo_rel r" unfolding wo_rel_def using WELL .

   224   hence Refl: "Refl r" by (simp add: wo_rel.REFL)

   225   hence "Field ?rA = Field r Int A"

   226   using Refl_Field_Restr by blast

   227   hence FieldA: "Field ?rA = A" using OFA Well

   228   by (auto simp add: wo_rel.ofilter_def)

   229   have "Field ?rB = Field r Int B"

   230   using Refl Refl_Field_Restr by blast

   231   hence FieldB: "Field ?rB = B" using OFB Well

   232   by (auto simp add: wo_rel.ofilter_def)

   233   (* Main proof *)

   234   show ?thesis unfolding embedS_def iso_def

   235   using assms ofilter_subset_embed[of r A B]

   236         FieldA FieldB bij_betw_id_iff[of A B] by auto

   237 qed

   238

   239 lemma ofilter_subset_embedS:

   240 assumes WELL: "Well_order r" and

   241         OFA: "wo_rel.ofilter r A" and OFB: "wo_rel.ofilter r B"

   242 shows "(A < B) = embedS (Restr r A) (Restr r B) id"

   243 using assms by (simp add: ofilter_subset_embedS_iso)

   244

   245 lemma embed_implies_iso_Restr:

   246 assumes WELL: "Well_order r" and WELL': "Well_order r'" and

   247         EMB: "embed r' r f"

   248 shows "iso r' (Restr r (f  (Field r'))) f"

   249 proof-

   250   let ?A' = "Field r'"

   251   let ?r'' = "Restr r (f  ?A')"

   252   have 0: "Well_order ?r''" using WELL Well_order_Restr by blast

   253   have 1: "wo_rel.ofilter r (f  ?A')" using assms embed_Field_ofilter  by blast

   254   hence "Field ?r'' = f  (Field r')" using WELL Field_Restr_ofilter by blast

   255   hence "bij_betw f ?A' (Field ?r'')"

   256   using EMB embed_inj_on WELL' unfolding bij_betw_def by blast

   257   moreover

   258   {have "\<forall>a b. (a,b) \<in> r' \<longrightarrow> a \<in> Field r' \<and> b \<in> Field r'"

   259    unfolding Field_def by auto

   260    hence "compat r' ?r'' f"

   261    using assms embed_iff_compat_inj_on_ofilter

   262    unfolding compat_def by blast

   263   }

   264   ultimately show ?thesis using WELL' 0 iso_iff3 by blast

   265 qed

   266

   267

   268 subsection \<open>The strict inclusion on proper ofilters is well-founded\<close>

   269

   270 definition ofilterIncl :: "'a rel \<Rightarrow> 'a set rel"

   271 where

   272 "ofilterIncl r \<equiv> {(A,B). wo_rel.ofilter r A \<and> A \<noteq> Field r \<and>

   273                          wo_rel.ofilter r B \<and> B \<noteq> Field r \<and> A < B}"

   274

   275 lemma wf_ofilterIncl:

   276 assumes WELL: "Well_order r"

   277 shows "wf(ofilterIncl r)"

   278 proof-

   279   have Well: "wo_rel r" using WELL by (simp add: wo_rel_def)

   280   hence Lo: "Linear_order r" by (simp add: wo_rel.LIN)

   281   let ?h = "(\<lambda> A. wo_rel.suc r A)"

   282   let ?rS = "r - Id"

   283   have "wf ?rS" using WELL by (simp add: order_on_defs)

   284   moreover

   285   have "compat (ofilterIncl r) ?rS ?h"

   286   proof(unfold compat_def ofilterIncl_def,

   287         intro allI impI, simp, elim conjE)

   288     fix A B

   289     assume *: "wo_rel.ofilter r A" "A \<noteq> Field r" and

   290            **: "wo_rel.ofilter r B" "B \<noteq> Field r" and ***: "A < B"

   291     then obtain a and b where 0: "a \<in> Field r \<and> b \<in> Field r" and

   292                          1: "A = underS r a \<and> B = underS r b"

   293     using Well by (auto simp add: wo_rel.ofilter_underS_Field)

   294     hence "a \<noteq> b" using *** by auto

   295     moreover

   296     have "(a,b) \<in> r" using 0 1 Lo ***

   297     by (auto simp add: underS_incl_iff)

   298     moreover

   299     have "a = wo_rel.suc r A \<and> b = wo_rel.suc r B"

   300     using Well 0 1 by (simp add: wo_rel.suc_underS)

   301     ultimately

   302     show "(wo_rel.suc r A, wo_rel.suc r B) \<in> r \<and> wo_rel.suc r A \<noteq> wo_rel.suc r B"

   303     by simp

   304   qed

   305   ultimately show "wf (ofilterIncl r)" by (simp add: compat_wf)

   306 qed

   307

   308

   309 subsection \<open>Ordering the well-orders by existence of embeddings\<close>

   310

   311 text \<open>We define three relations between well-orders:

   312 \begin{itemize}

   313 \item \<open>ordLeq\<close>, of being embedded (abbreviated \<open>\<le>o\<close>);

   314 \item \<open>ordLess\<close>, of being strictly embedded (abbreviated \<open><o\<close>);

   315 \item \<open>ordIso\<close>, of being isomorphic (abbreviated \<open>=o\<close>).

   316 \end{itemize}

   317 %

   318 The prefix "ord" and the index "o" in these names stand for "ordinal-like".

   319 These relations shall be proved to be inter-connected in a similar fashion as the trio

   320 \<open>\<le>\<close>, \<open><\<close>, \<open>=\<close> associated to a total order on a set.

   321 \<close>

   322

   323 definition ordLeq :: "('a rel * 'a' rel) set"

   324 where

   325 "ordLeq = {(r,r'). Well_order r \<and> Well_order r' \<and> (\<exists>f. embed r r' f)}"

   326

   327 abbreviation ordLeq2 :: "'a rel \<Rightarrow> 'a' rel \<Rightarrow> bool" (infix "<=o" 50)

   328 where "r <=o r' \<equiv> (r,r') \<in> ordLeq"

   329

   330 abbreviation ordLeq3 :: "'a rel \<Rightarrow> 'a' rel \<Rightarrow> bool" (infix "\<le>o" 50)

   331 where "r \<le>o r' \<equiv> r <=o r'"

   332

   333 definition ordLess :: "('a rel * 'a' rel) set"

   334 where

   335 "ordLess = {(r,r'). Well_order r \<and> Well_order r' \<and> (\<exists>f. embedS r r' f)}"

   336

   337 abbreviation ordLess2 :: "'a rel \<Rightarrow> 'a' rel \<Rightarrow> bool" (infix "<o" 50)

   338 where "r <o r' \<equiv> (r,r') \<in> ordLess"

   339

   340 definition ordIso :: "('a rel * 'a' rel) set"

   341 where

   342 "ordIso = {(r,r'). Well_order r \<and> Well_order r' \<and> (\<exists>f. iso r r' f)}"

   343

   344 abbreviation ordIso2 :: "'a rel \<Rightarrow> 'a' rel \<Rightarrow> bool" (infix "=o" 50)

   345 where "r =o r' \<equiv> (r,r') \<in> ordIso"

   346

   347 lemmas ordRels_def = ordLeq_def ordLess_def ordIso_def

   348

   349 lemma ordLeq_Well_order_simp:

   350 assumes "r \<le>o r'"

   351 shows "Well_order r \<and> Well_order r'"

   352 using assms unfolding ordLeq_def by simp

   353

   354 text\<open>Notice that the relations \<open>\<le>o\<close>, \<open><o\<close>, \<open>=o\<close> connect well-orders

   355 on potentially {\em distinct} types. However, some of the lemmas below, including the next one,

   356 restrict implicitly the type of these relations to \<open>(('a rel) * ('a rel)) set\<close> , i.e.,

   357 to \<open>'a rel rel\<close>.\<close>

   358

   359 lemma ordLeq_reflexive:

   360 "Well_order r \<Longrightarrow> r \<le>o r"

   361 unfolding ordLeq_def using id_embed[of r] by blast

   362

   363 lemma ordLeq_transitive[trans]:

   364 assumes *: "r \<le>o r'" and **: "r' \<le>o r''"

   365 shows "r \<le>o r''"

   366 proof-

   367   obtain f and f'

   368   where 1: "Well_order r \<and> Well_order r' \<and> Well_order r''" and

   369         "embed r r' f" and "embed r' r'' f'"

   370   using * ** unfolding ordLeq_def by blast

   371   hence "embed r r'' (f' o f)"

   372   using comp_embed[of r r' f r'' f'] by auto

   373   thus "r \<le>o r''" unfolding ordLeq_def using 1 by auto

   374 qed

   375

   376 lemma ordLeq_total:

   377 "\<lbrakk>Well_order r; Well_order r'\<rbrakk> \<Longrightarrow> r \<le>o r' \<or> r' \<le>o r"

   378 unfolding ordLeq_def using wellorders_totally_ordered by blast

   379

   380 lemma ordIso_reflexive:

   381 "Well_order r \<Longrightarrow> r =o r"

   382 unfolding ordIso_def using id_iso[of r] by blast

   383

   384 lemma ordIso_transitive[trans]:

   385 assumes *: "r =o r'" and **: "r' =o r''"

   386 shows "r =o r''"

   387 proof-

   388   obtain f and f'

   389   where 1: "Well_order r \<and> Well_order r' \<and> Well_order r''" and

   390         "iso r r' f" and 3: "iso r' r'' f'"

   391   using * ** unfolding ordIso_def by auto

   392   hence "iso r r'' (f' o f)"

   393   using comp_iso[of r r' f r'' f'] by auto

   394   thus "r =o r''" unfolding ordIso_def using 1 by auto

   395 qed

   396

   397 lemma ordIso_symmetric:

   398 assumes *: "r =o r'"

   399 shows "r' =o r"

   400 proof-

   401   obtain f where 1: "Well_order r \<and> Well_order r'" and

   402                  2: "embed r r' f \<and> bij_betw f (Field r) (Field r')"

   403   using * by (auto simp add: ordIso_def iso_def)

   404   let ?f' = "inv_into (Field r) f"

   405   have "embed r' r ?f' \<and> bij_betw ?f' (Field r') (Field r)"

   406   using 1 2 by (simp add: bij_betw_inv_into inv_into_Field_embed_bij_betw)

   407   thus "r' =o r" unfolding ordIso_def using 1 by (auto simp add: iso_def)

   408 qed

   409

   410 lemma ordLeq_ordLess_trans[trans]:

   411 assumes "r \<le>o r'" and " r' <o r''"

   412 shows "r <o r''"

   413 proof-

   414   have "Well_order r \<and> Well_order r''"

   415   using assms unfolding ordLeq_def ordLess_def by auto

   416   thus ?thesis using assms unfolding ordLeq_def ordLess_def

   417   using embed_comp_embedS by blast

   418 qed

   419

   420 lemma ordLess_ordLeq_trans[trans]:

   421 assumes "r <o r'" and " r' \<le>o r''"

   422 shows "r <o r''"

   423 proof-

   424   have "Well_order r \<and> Well_order r''"

   425   using assms unfolding ordLeq_def ordLess_def by auto

   426   thus ?thesis using assms unfolding ordLeq_def ordLess_def

   427   using embedS_comp_embed by blast

   428 qed

   429

   430 lemma ordLeq_ordIso_trans[trans]:

   431 assumes "r \<le>o r'" and " r' =o r''"

   432 shows "r \<le>o r''"

   433 proof-

   434   have "Well_order r \<and> Well_order r''"

   435   using assms unfolding ordLeq_def ordIso_def by auto

   436   thus ?thesis using assms unfolding ordLeq_def ordIso_def

   437   using embed_comp_iso by blast

   438 qed

   439

   440 lemma ordIso_ordLeq_trans[trans]:

   441 assumes "r =o r'" and " r' \<le>o r''"

   442 shows "r \<le>o r''"

   443 proof-

   444   have "Well_order r \<and> Well_order r''"

   445   using assms unfolding ordLeq_def ordIso_def by auto

   446   thus ?thesis using assms unfolding ordLeq_def ordIso_def

   447   using iso_comp_embed by blast

   448 qed

   449

   450 lemma ordLess_ordIso_trans[trans]:

   451 assumes "r <o r'" and " r' =o r''"

   452 shows "r <o r''"

   453 proof-

   454   have "Well_order r \<and> Well_order r''"

   455   using assms unfolding ordLess_def ordIso_def by auto

   456   thus ?thesis using assms unfolding ordLess_def ordIso_def

   457   using embedS_comp_iso by blast

   458 qed

   459

   460 lemma ordIso_ordLess_trans[trans]:

   461 assumes "r =o r'" and " r' <o r''"

   462 shows "r <o r''"

   463 proof-

   464   have "Well_order r \<and> Well_order r''"

   465   using assms unfolding ordLess_def ordIso_def by auto

   466   thus ?thesis using assms unfolding ordLess_def ordIso_def

   467   using iso_comp_embedS by blast

   468 qed

   469

   470 lemma ordLess_not_embed:

   471 assumes "r <o r'"

   472 shows "\<not>(\<exists>f'. embed r' r f')"

   473 proof-

   474   obtain f where 1: "Well_order r \<and> Well_order r'" and 2: "embed r r' f" and

   475                  3: " \<not> bij_betw f (Field r) (Field r')"

   476   using assms unfolding ordLess_def by (auto simp add: embedS_def)

   477   {fix f' assume *: "embed r' r f'"

   478    hence "bij_betw f (Field r) (Field r')" using 1 2

   479    by (simp add: embed_bothWays_Field_bij_betw)

   480    with 3 have False by contradiction

   481   }

   482   thus ?thesis by blast

   483 qed

   484

   485 lemma ordLess_Field:

   486 assumes OL: "r1 <o r2" and EMB: "embed r1 r2 f"

   487 shows "\<not> (f(Field r1) = Field r2)"

   488 proof-

   489   let ?A1 = "Field r1"  let ?A2 = "Field r2"

   490   obtain g where

   491   0: "Well_order r1 \<and> Well_order r2" and

   492   1: "embed r1 r2 g \<and> \<not>(bij_betw g ?A1 ?A2)"

   493   using OL unfolding ordLess_def by (auto simp add: embedS_def)

   494   hence "\<forall>a \<in> ?A1. f a = g a"

   495   using 0 EMB embed_unique[of r1] by auto

   496   hence "\<not>(bij_betw f ?A1 ?A2)"

   497   using 1 bij_betw_cong[of ?A1] by blast

   498   moreover

   499   have "inj_on f ?A1" using EMB 0 by (simp add: embed_inj_on)

   500   ultimately show ?thesis by (simp add: bij_betw_def)

   501 qed

   502

   503 lemma ordLess_iff:

   504 "r <o r' = (Well_order r \<and> Well_order r' \<and> \<not>(\<exists>f'. embed r' r f'))"

   505 proof

   506   assume *: "r <o r'"

   507   hence "\<not>(\<exists>f'. embed r' r f')" using ordLess_not_embed[of r r'] by simp

   508   with * show "Well_order r \<and> Well_order r' \<and> \<not> (\<exists>f'. embed r' r f')"

   509   unfolding ordLess_def by auto

   510 next

   511   assume *: "Well_order r \<and> Well_order r' \<and> \<not> (\<exists>f'. embed r' r f')"

   512   then obtain f where 1: "embed r r' f"

   513   using wellorders_totally_ordered[of r r'] by blast

   514   moreover

   515   {assume "bij_betw f (Field r) (Field r')"

   516    with * 1 have "embed r' r (inv_into (Field r) f) "

   517    using inv_into_Field_embed_bij_betw[of r r' f] by auto

   518    with * have False by blast

   519   }

   520   ultimately show "(r,r') \<in> ordLess"

   521   unfolding ordLess_def using * by (fastforce simp add: embedS_def)

   522 qed

   523

   524 lemma ordLess_irreflexive: "\<not> r <o r"

   525 proof

   526   assume "r <o r"

   527   hence "Well_order r \<and>  \<not>(\<exists>f. embed r r f)"

   528   unfolding ordLess_iff ..

   529   moreover have "embed r r id" using id_embed[of r] .

   530   ultimately show False by blast

   531 qed

   532

   533 lemma ordLeq_iff_ordLess_or_ordIso:

   534 "r \<le>o r' = (r <o r' \<or> r =o r')"

   535 unfolding ordRels_def embedS_defs iso_defs by blast

   536

   537 lemma ordIso_iff_ordLeq:

   538 "(r =o r') = (r \<le>o r' \<and> r' \<le>o r)"

   539 proof

   540   assume "r =o r'"

   541   then obtain f where 1: "Well_order r \<and> Well_order r' \<and>

   542                      embed r r' f \<and> bij_betw f (Field r) (Field r')"

   543   unfolding ordIso_def iso_defs by auto

   544   hence "embed r r' f \<and> embed r' r (inv_into (Field r) f)"

   545   by (simp add: inv_into_Field_embed_bij_betw)

   546   thus  "r \<le>o r' \<and> r' \<le>o r"

   547   unfolding ordLeq_def using 1 by auto

   548 next

   549   assume "r \<le>o r' \<and> r' \<le>o r"

   550   then obtain f and g where 1: "Well_order r \<and> Well_order r' \<and>

   551                            embed r r' f \<and> embed r' r g"

   552   unfolding ordLeq_def by auto

   553   hence "iso r r' f" by (auto simp add: embed_bothWays_iso)

   554   thus "r =o r'" unfolding ordIso_def using 1 by auto

   555 qed

   556

   557 lemma not_ordLess_ordLeq:

   558 "r <o r' \<Longrightarrow> \<not> r' \<le>o r"

   559 using ordLess_ordLeq_trans ordLess_irreflexive by blast

   560

   561 lemma ordLess_or_ordLeq:

   562 assumes WELL: "Well_order r" and WELL': "Well_order r'"

   563 shows "r <o r' \<or> r' \<le>o r"

   564 proof-

   565   have "r \<le>o r' \<or> r' \<le>o r"

   566   using assms by (simp add: ordLeq_total)

   567   moreover

   568   {assume "\<not> r <o r' \<and> r \<le>o r'"

   569    hence "r =o r'" using ordLeq_iff_ordLess_or_ordIso by blast

   570    hence "r' \<le>o r" using ordIso_symmetric ordIso_iff_ordLeq by blast

   571   }

   572   ultimately show ?thesis by blast

   573 qed

   574

   575 lemma not_ordLess_ordIso:

   576 "r <o r' \<Longrightarrow> \<not> r =o r'"

   577 using ordLess_ordIso_trans ordIso_symmetric ordLess_irreflexive by blast

   578

   579 lemma not_ordLeq_iff_ordLess:

   580 assumes WELL: "Well_order r" and WELL': "Well_order r'"

   581 shows "(\<not> r' \<le>o r) = (r <o r')"

   582 using assms not_ordLess_ordLeq ordLess_or_ordLeq by blast

   583

   584 lemma not_ordLess_iff_ordLeq:

   585 assumes WELL: "Well_order r" and WELL': "Well_order r'"

   586 shows "(\<not> r' <o r) = (r \<le>o r')"

   587 using assms not_ordLess_ordLeq ordLess_or_ordLeq by blast

   588

   589 lemma ordLess_transitive[trans]:

   590 "\<lbrakk>r <o r'; r' <o r''\<rbrakk> \<Longrightarrow> r <o r''"

   591 using ordLess_ordLeq_trans ordLeq_iff_ordLess_or_ordIso by blast

   592

   593 corollary ordLess_trans: "trans ordLess"

   594 unfolding trans_def using ordLess_transitive by blast

   595

   596 lemmas ordIso_equivalence = ordIso_transitive ordIso_reflexive ordIso_symmetric

   597

   598 lemma ordIso_imp_ordLeq:

   599 "r =o r' \<Longrightarrow> r \<le>o r'"

   600 using ordIso_iff_ordLeq by blast

   601

   602 lemma ordLess_imp_ordLeq:

   603 "r <o r' \<Longrightarrow> r \<le>o r'"

   604 using ordLeq_iff_ordLess_or_ordIso by blast

   605

   606 lemma ofilter_subset_ordLeq:

   607 assumes WELL: "Well_order r" and

   608         OFA: "wo_rel.ofilter r A" and OFB: "wo_rel.ofilter r B"

   609 shows "(A \<le> B) = (Restr r A \<le>o Restr r B)"

   610 proof

   611   assume "A \<le> B"

   612   thus "Restr r A \<le>o Restr r B"

   613   unfolding ordLeq_def using assms

   614   Well_order_Restr Well_order_Restr ofilter_subset_embed by blast

   615 next

   616   assume *: "Restr r A \<le>o Restr r B"

   617   then obtain f where "embed (Restr r A) (Restr r B) f"

   618   unfolding ordLeq_def by blast

   619   {assume "B < A"

   620    hence "Restr r B <o Restr r A"

   621    unfolding ordLess_def using assms

   622    Well_order_Restr Well_order_Restr ofilter_subset_embedS by blast

   623    hence False using * not_ordLess_ordLeq by blast

   624   }

   625   thus "A \<le> B" using OFA OFB WELL

   626   wo_rel_def[of r] wo_rel.ofilter_linord[of r A B] by blast

   627 qed

   628

   629 lemma ofilter_subset_ordLess:

   630 assumes WELL: "Well_order r" and

   631         OFA: "wo_rel.ofilter r A" and OFB: "wo_rel.ofilter r B"

   632 shows "(A < B) = (Restr r A <o Restr r B)"

   633 proof-

   634   let ?rA = "Restr r A" let ?rB = "Restr r B"

   635   have 1: "Well_order ?rA \<and> Well_order ?rB"

   636   using WELL Well_order_Restr by blast

   637   have "(A < B) = (\<not> B \<le> A)" using assms

   638   wo_rel_def wo_rel.ofilter_linord[of r A B] by blast

   639   also have "\<dots> = (\<not> Restr r B \<le>o Restr r A)"

   640   using assms ofilter_subset_ordLeq by blast

   641   also have "\<dots> = (Restr r A <o Restr r B)"

   642   using 1 not_ordLeq_iff_ordLess by blast

   643   finally show ?thesis .

   644 qed

   645

   646 lemma ofilter_ordLess:

   647 "\<lbrakk>Well_order r; wo_rel.ofilter r A\<rbrakk> \<Longrightarrow> (A < Field r) = (Restr r A <o r)"

   648 by (simp add: ofilter_subset_ordLess wo_rel.Field_ofilter

   649     wo_rel_def Restr_Field)

   650

   651 corollary underS_Restr_ordLess:

   652 assumes "Well_order r" and "Field r \<noteq> {}"

   653 shows "Restr r (underS r a) <o r"

   654 proof-

   655   have "underS r a < Field r" using assms

   656   by (simp add: underS_Field3)

   657   thus ?thesis using assms

   658   by (simp add: ofilter_ordLess wo_rel.underS_ofilter wo_rel_def)

   659 qed

   660

   661 lemma embed_ordLess_ofilterIncl:

   662 assumes

   663   OL12: "r1 <o r2" and OL23: "r2 <o r3" and

   664   EMB13: "embed r1 r3 f13" and EMB23: "embed r2 r3 f23"

   665 shows "(f13(Field r1), f23(Field r2)) \<in> (ofilterIncl r3)"

   666 proof-

   667   have OL13: "r1 <o r3"

   668   using OL12 OL23 using ordLess_transitive by auto

   669   let ?A1 = "Field r1"  let ?A2 ="Field r2" let ?A3 ="Field r3"

   670   obtain f12 g23 where

   671   0: "Well_order r1 \<and> Well_order r2 \<and> Well_order r3" and

   672   1: "embed r1 r2 f12 \<and> \<not>(bij_betw f12 ?A1 ?A2)" and

   673   2: "embed r2 r3 g23 \<and> \<not>(bij_betw g23 ?A2 ?A3)"

   674   using OL12 OL23 by (auto simp add: ordLess_def embedS_def)

   675   hence "\<forall>a \<in> ?A2. f23 a = g23 a"

   676   using EMB23 embed_unique[of r2 r3] by blast

   677   hence 3: "\<not>(bij_betw f23 ?A2 ?A3)"

   678   using 2 bij_betw_cong[of ?A2 f23 g23] by blast

   679   (*  *)

   680   have 4: "wo_rel.ofilter r2 (f12  ?A1) \<and> f12  ?A1 \<noteq> ?A2"

   681   using 0 1 OL12 by (simp add: embed_Field_ofilter ordLess_Field)

   682   have 5: "wo_rel.ofilter r3 (f23  ?A2) \<and> f23  ?A2 \<noteq> ?A3"

   683   using 0 EMB23 OL23 by (simp add: embed_Field_ofilter ordLess_Field)

   684   have 6: "wo_rel.ofilter r3 (f13  ?A1)  \<and> f13  ?A1 \<noteq> ?A3"

   685   using 0 EMB13 OL13 by (simp add: embed_Field_ofilter ordLess_Field)

   686   (*  *)

   687   have "f12  ?A1 < ?A2"

   688   using 0 4 by (auto simp add: wo_rel_def wo_rel.ofilter_def)

   689   moreover have "inj_on f23 ?A2"

   690   using EMB23 0 by (simp add: wo_rel_def embed_inj_on)

   691   ultimately

   692   have "f23  (f12  ?A1) < f23  ?A2" by (simp add: inj_on_strict_subset)

   693   moreover

   694   {have "embed r1 r3 (f23 o f12)"

   695    using 1 EMB23 0 by (auto simp add: comp_embed)

   696    hence "\<forall>a \<in> ?A1. f23(f12 a) = f13 a"

   697    using EMB13 0 embed_unique[of r1 r3 "f23 o f12" f13] by auto

   698    hence "f23  (f12  ?A1) = f13  ?A1" by force

   699   }

   700   ultimately

   701   have "f13  ?A1 < f23  ?A2" by simp

   702   (*  *)

   703   with 5 6 show ?thesis

   704   unfolding ofilterIncl_def by auto

   705 qed

   706

   707 lemma ordLess_iff_ordIso_Restr:

   708 assumes WELL: "Well_order r" and WELL': "Well_order r'"

   709 shows "(r' <o r) = (\<exists>a \<in> Field r. r' =o Restr r (underS r a))"

   710 proof(auto)

   711   fix a assume *: "a \<in> Field r" and **: "r' =o Restr r (underS r a)"

   712   hence "Restr r (underS r a) <o r" using WELL underS_Restr_ordLess[of r] by blast

   713   thus "r' <o r" using ** ordIso_ordLess_trans by blast

   714 next

   715   assume "r' <o r"

   716   then obtain f where 1: "Well_order r \<and> Well_order r'" and

   717                       2: "embed r' r f \<and> f  (Field r') \<noteq> Field r"

   718   unfolding ordLess_def embedS_def[abs_def] bij_betw_def using embed_inj_on by blast

   719   hence "wo_rel.ofilter r (f  (Field r'))" using embed_Field_ofilter by blast

   720   then obtain a where 3: "a \<in> Field r" and 4: "underS r a = f  (Field r')"

   721   using 1 2 by (auto simp add: wo_rel.ofilter_underS_Field wo_rel_def)

   722   have "iso r' (Restr r (f  (Field r'))) f"

   723   using embed_implies_iso_Restr 2 assms by blast

   724   moreover have "Well_order (Restr r (f  (Field r')))"

   725   using WELL Well_order_Restr by blast

   726   ultimately have "r' =o Restr r (f  (Field r'))"

   727   using WELL' unfolding ordIso_def by auto

   728   hence "r' =o Restr r (underS r a)" using 4 by auto

   729   thus "\<exists>a \<in> Field r. r' =o Restr r (underS r a)" using 3 by auto

   730 qed

   731

   732 lemma internalize_ordLess:

   733 "(r' <o r) = (\<exists>p. Field p < Field r \<and> r' =o p \<and> p <o r)"

   734 proof

   735   assume *: "r' <o r"

   736   hence 0: "Well_order r \<and> Well_order r'" unfolding ordLess_def by auto

   737   with * obtain a where 1: "a \<in> Field r" and 2: "r' =o Restr r (underS r a)"

   738   using ordLess_iff_ordIso_Restr by blast

   739   let ?p = "Restr r (underS r a)"

   740   have "wo_rel.ofilter r (underS r a)" using 0

   741   by (simp add: wo_rel_def wo_rel.underS_ofilter)

   742   hence "Field ?p = underS r a" using 0 Field_Restr_ofilter by blast

   743   hence "Field ?p < Field r" using underS_Field2 1 by fast

   744   moreover have "?p <o r" using underS_Restr_ordLess[of r a] 0 1 by blast

   745   ultimately

   746   show "\<exists>p. Field p < Field r \<and> r' =o p \<and> p <o r" using 2 by blast

   747 next

   748   assume "\<exists>p. Field p < Field r \<and> r' =o p \<and> p <o r"

   749   thus "r' <o r" using ordIso_ordLess_trans by blast

   750 qed

   751

   752 lemma internalize_ordLeq:

   753 "(r' \<le>o r) = (\<exists>p. Field p \<le> Field r \<and> r' =o p \<and> p \<le>o r)"

   754 proof

   755   assume *: "r' \<le>o r"

   756   moreover

   757   {assume "r' <o r"

   758    then obtain p where "Field p < Field r \<and> r' =o p \<and> p <o r"

   759    using internalize_ordLess[of r' r] by blast

   760    hence "\<exists>p. Field p \<le> Field r \<and> r' =o p \<and> p \<le>o r"

   761    using ordLeq_iff_ordLess_or_ordIso by blast

   762   }

   763   moreover

   764   have "r \<le>o r" using * ordLeq_def ordLeq_reflexive by blast

   765   ultimately show "\<exists>p. Field p \<le> Field r \<and> r' =o p \<and> p \<le>o r"

   766   using ordLeq_iff_ordLess_or_ordIso by blast

   767 next

   768   assume "\<exists>p. Field p \<le> Field r \<and> r' =o p \<and> p \<le>o r"

   769   thus "r' \<le>o r" using ordIso_ordLeq_trans by blast

   770 qed

   771

   772 lemma ordLeq_iff_ordLess_Restr:

   773 assumes WELL: "Well_order r" and WELL': "Well_order r'"

   774 shows "(r \<le>o r') = (\<forall>a \<in> Field r. Restr r (underS r a) <o r')"

   775 proof(auto)

   776   assume *: "r \<le>o r'"

   777   fix a assume "a \<in> Field r"

   778   hence "Restr r (underS r a) <o r"

   779   using WELL underS_Restr_ordLess[of r] by blast

   780   thus "Restr r (underS r a) <o r'"

   781   using * ordLess_ordLeq_trans by blast

   782 next

   783   assume *: "\<forall>a \<in> Field r. Restr r (underS r a) <o r'"

   784   {assume "r' <o r"

   785    then obtain a where "a \<in> Field r \<and> r' =o Restr r (underS r a)"

   786    using assms ordLess_iff_ordIso_Restr by blast

   787    hence False using * not_ordLess_ordIso ordIso_symmetric by blast

   788   }

   789   thus "r \<le>o r'" using ordLess_or_ordLeq assms by blast

   790 qed

   791

   792 lemma finite_ordLess_infinite:

   793 assumes WELL: "Well_order r" and WELL': "Well_order r'" and

   794         FIN: "finite(Field r)" and INF: "\<not>finite(Field r')"

   795 shows "r <o r'"

   796 proof-

   797   {assume "r' \<le>o r"

   798    then obtain h where "inj_on h (Field r') \<and> h  (Field r') \<le> Field r"

   799    unfolding ordLeq_def using assms embed_inj_on embed_Field by blast

   800    hence False using finite_imageD finite_subset FIN INF by blast

   801   }

   802   thus ?thesis using WELL WELL' ordLess_or_ordLeq by blast

   803 qed

   804

   805 lemma finite_well_order_on_ordIso:

   806 assumes FIN: "finite A" and

   807         WELL: "well_order_on A r" and WELL': "well_order_on A r'"

   808 shows "r =o r'"

   809 proof-

   810   have 0: "Well_order r \<and> Well_order r' \<and> Field r = A \<and> Field r' = A"

   811   using assms well_order_on_Well_order by blast

   812   moreover

   813   have "\<forall>r r'. well_order_on A r \<and> well_order_on A r' \<and> r \<le>o r'

   814                   \<longrightarrow> r =o r'"

   815   proof(clarify)

   816     fix r r' assume *: "well_order_on A r" and **: "well_order_on A r'"

   817     have 2: "Well_order r \<and> Well_order r' \<and> Field r = A \<and> Field r' = A"

   818     using * ** well_order_on_Well_order by blast

   819     assume "r \<le>o r'"

   820     then obtain f where 1: "embed r r' f" and

   821                         "inj_on f A \<and> f  A \<le> A"

   822     unfolding ordLeq_def using 2 embed_inj_on embed_Field by blast

   823     hence "bij_betw f A A" unfolding bij_betw_def using FIN endo_inj_surj by blast

   824     thus "r =o r'" unfolding ordIso_def iso_def[abs_def] using 1 2 by auto

   825   qed

   826   ultimately show ?thesis using assms ordLeq_total ordIso_symmetric by blast

   827 qed

   828

   829 subsection\<open>\<open><o\<close> is well-founded\<close>

   830

   831 text \<open>Of course, it only makes sense to state that the \<open><o\<close> is well-founded

   832 on the restricted type \<open>'a rel rel\<close>.  We prove this by first showing that, for any set

   833 of well-orders all embedded in a fixed well-order, the function mapping each well-order

   834 in the set to an order filter of the fixed well-order is compatible w.r.t. to \<open><o\<close> versus

   835 {\em strict inclusion}; and we already know that strict inclusion of order filters is well-founded.\<close>

   836

   837 definition ord_to_filter :: "'a rel \<Rightarrow> 'a rel \<Rightarrow> 'a set"

   838 where "ord_to_filter r0 r \<equiv> (SOME f. embed r r0 f)  (Field r)"

   839

   840 lemma ord_to_filter_compat:

   841 "compat (ordLess Int (ordLess^-1{r0} \<times> ordLess^-1{r0}))

   842         (ofilterIncl r0)

   843         (ord_to_filter r0)"

   844 proof(unfold compat_def ord_to_filter_def, clarify)

   845   fix r1::"'a rel" and r2::"'a rel"

   846   let ?A1 = "Field r1"  let ?A2 ="Field r2" let ?A0 ="Field r0"

   847   let ?phi10 = "\<lambda> f10. embed r1 r0 f10" let ?f10 = "SOME f. ?phi10 f"

   848   let ?phi20 = "\<lambda> f20. embed r2 r0 f20" let ?f20 = "SOME f. ?phi20 f"

   849   assume *: "r1 <o r0" "r2 <o r0" and **: "r1 <o r2"

   850   hence "(\<exists>f. ?phi10 f) \<and> (\<exists>f. ?phi20 f)"

   851   by (auto simp add: ordLess_def embedS_def)

   852   hence "?phi10 ?f10 \<and> ?phi20 ?f20" by (auto simp add: someI_ex)

   853   thus "(?f10  ?A1, ?f20  ?A2) \<in> ofilterIncl r0"

   854   using * ** by (simp add: embed_ordLess_ofilterIncl)

   855 qed

   856

   857 theorem wf_ordLess: "wf ordLess"

   858 proof-

   859   {fix r0 :: "('a \<times> 'a) set"

   860    (* need to annotate here!*)

   861    let ?ordLess = "ordLess::('d rel * 'd rel) set"

   862    let ?R = "?ordLess Int (?ordLess^-1{r0} \<times> ?ordLess^-1{r0})"

   863    {assume Case1: "Well_order r0"

   864     hence "wf ?R"

   865     using wf_ofilterIncl[of r0]

   866           compat_wf[of ?R "ofilterIncl r0" "ord_to_filter r0"]

   867           ord_to_filter_compat[of r0] by auto

   868    }

   869    moreover

   870    {assume Case2: "\<not> Well_order r0"

   871     hence "?R = {}" unfolding ordLess_def by auto

   872     hence "wf ?R" using wf_empty by simp

   873    }

   874    ultimately have "wf ?R" by blast

   875   }

   876   thus ?thesis by (simp add: trans_wf_iff ordLess_trans)

   877 qed

   878

   879 corollary exists_minim_Well_order:

   880 assumes NE: "R \<noteq> {}" and WELL: "\<forall>r \<in> R. Well_order r"

   881 shows "\<exists>r \<in> R. \<forall>r' \<in> R. r \<le>o r'"

   882 proof-

   883   obtain r where "r \<in> R \<and> (\<forall>r' \<in> R. \<not> r' <o r)"

   884   using NE spec[OF spec[OF subst[OF wf_eq_minimal, of "%x. x", OF wf_ordLess]], of _ R]

   885     equals0I[of R] by blast

   886   with not_ordLeq_iff_ordLess WELL show ?thesis by blast

   887 qed

   888

   889

   890 subsection \<open>Copy via direct images\<close>

   891

   892 text\<open>The direct image operator is the dual of the inverse image operator \<open>inv_image\<close>

   893 from \<open>Relation.thy\<close>.  It is useful for transporting a well-order between

   894 different types.\<close>

   895

   896 definition dir_image :: "'a rel \<Rightarrow> ('a \<Rightarrow> 'a') \<Rightarrow> 'a' rel"

   897 where

   898 "dir_image r f = {(f a, f b)| a b. (a,b) \<in> r}"

   899

   900 lemma dir_image_Field:

   901 "Field(dir_image r f) = f  (Field r)"

   902 unfolding dir_image_def Field_def Range_def Domain_def by fast

   903

   904 lemma dir_image_minus_Id:

   905 "inj_on f (Field r) \<Longrightarrow> (dir_image r f) - Id = dir_image (r - Id) f"

   906 unfolding inj_on_def Field_def dir_image_def by auto

   907

   908 lemma Refl_dir_image:

   909 assumes "Refl r"

   910 shows "Refl(dir_image r f)"

   911 proof-

   912   {fix a' b'

   913    assume "(a',b') \<in> dir_image r f"

   914    then obtain a b where 1: "a' = f a \<and> b' = f b \<and> (a,b) \<in> r"

   915    unfolding dir_image_def by blast

   916    hence "a \<in> Field r \<and> b \<in> Field r" using Field_def by fastforce

   917    hence "(a,a) \<in> r \<and> (b,b) \<in> r" using assms by (simp add: refl_on_def)

   918    with 1 have "(a',a') \<in> dir_image r f \<and> (b',b') \<in> dir_image r f"

   919    unfolding dir_image_def by auto

   920   }

   921   thus ?thesis

   922   by(unfold refl_on_def Field_def Domain_def Range_def, auto)

   923 qed

   924

   925 lemma trans_dir_image:

   926 assumes TRANS: "trans r" and INJ: "inj_on f (Field r)"

   927 shows "trans(dir_image r f)"

   928 proof(unfold trans_def, auto)

   929   fix a' b' c'

   930   assume "(a',b') \<in> dir_image r f" "(b',c') \<in> dir_image r f"

   931   then obtain a b1 b2 c where 1: "a' = f a \<and> b' = f b1 \<and> b' = f b2 \<and> c' = f c" and

   932                          2: "(a,b1) \<in> r \<and> (b2,c) \<in> r"

   933   unfolding dir_image_def by blast

   934   hence "b1 \<in> Field r \<and> b2 \<in> Field r"

   935   unfolding Field_def by auto

   936   hence "b1 = b2" using 1 INJ unfolding inj_on_def by auto

   937   hence "(a,c): r" using 2 TRANS unfolding trans_def by blast

   938   thus "(a',c') \<in> dir_image r f"

   939   unfolding dir_image_def using 1 by auto

   940 qed

   941

   942 lemma Preorder_dir_image:

   943 "\<lbrakk>Preorder r; inj_on f (Field r)\<rbrakk> \<Longrightarrow> Preorder (dir_image r f)"

   944 by (simp add: preorder_on_def Refl_dir_image trans_dir_image)

   945

   946 lemma antisym_dir_image:

   947 assumes AN: "antisym r" and INJ: "inj_on f (Field r)"

   948 shows "antisym(dir_image r f)"

   949 proof(unfold antisym_def, auto)

   950   fix a' b'

   951   assume "(a',b') \<in> dir_image r f" "(b',a') \<in> dir_image r f"

   952   then obtain a1 b1 a2 b2 where 1: "a' = f a1 \<and> a' = f a2 \<and> b' = f b1 \<and> b' = f b2" and

   953                            2: "(a1,b1) \<in> r \<and> (b2,a2) \<in> r " and

   954                            3: "{a1,a2,b1,b2} \<le> Field r"

   955   unfolding dir_image_def Field_def by blast

   956   hence "a1 = a2 \<and> b1 = b2" using INJ unfolding inj_on_def by auto

   957   hence "a1 = b2" using 2 AN unfolding antisym_def by auto

   958   thus "a' = b'" using 1 by auto

   959 qed

   960

   961 lemma Partial_order_dir_image:

   962 "\<lbrakk>Partial_order r; inj_on f (Field r)\<rbrakk> \<Longrightarrow> Partial_order (dir_image r f)"

   963 by (simp add: partial_order_on_def Preorder_dir_image antisym_dir_image)

   964

   965 lemma Total_dir_image:

   966 assumes TOT: "Total r" and INJ: "inj_on f (Field r)"

   967 shows "Total(dir_image r f)"

   968 proof(unfold total_on_def, intro ballI impI)

   969   fix a' b'

   970   assume "a' \<in> Field (dir_image r f)" "b' \<in> Field (dir_image r f)"

   971   then obtain a and b where 1: "a \<in> Field r \<and> b \<in> Field r \<and> f a = a' \<and> f b = b'"

   972     unfolding dir_image_Field[of r f] by blast

   973   moreover assume "a' \<noteq> b'"

   974   ultimately have "a \<noteq> b" using INJ unfolding inj_on_def by auto

   975   hence "(a,b) \<in> r \<or> (b,a) \<in> r" using 1 TOT unfolding total_on_def by auto

   976   thus "(a',b') \<in> dir_image r f \<or> (b',a') \<in> dir_image r f"

   977   using 1 unfolding dir_image_def by auto

   978 qed

   979

   980 lemma Linear_order_dir_image:

   981 "\<lbrakk>Linear_order r; inj_on f (Field r)\<rbrakk> \<Longrightarrow> Linear_order (dir_image r f)"

   982 by (simp add: linear_order_on_def Partial_order_dir_image Total_dir_image)

   983

   984 lemma wf_dir_image:

   985 assumes WF: "wf r" and INJ: "inj_on f (Field r)"

   986 shows "wf(dir_image r f)"

   987 proof(unfold wf_eq_minimal2, intro allI impI, elim conjE)

   988   fix A'::"'b set"

   989   assume SUB: "A' \<le> Field(dir_image r f)" and NE: "A' \<noteq> {}"

   990   obtain A where A_def: "A = {a \<in> Field r. f a \<in> A'}" by blast

   991   have "A \<noteq> {} \<and> A \<le> Field r" using A_def SUB NE by (auto simp: dir_image_Field)

   992   then obtain a where 1: "a \<in> A \<and> (\<forall>b \<in> A. (b,a) \<notin> r)"

   993   using spec[OF WF[unfolded wf_eq_minimal2], of A] by blast

   994   have "\<forall>b' \<in> A'. (b',f a) \<notin> dir_image r f"

   995   proof(clarify)

   996     fix b' assume *: "b' \<in> A'" and **: "(b',f a) \<in> dir_image r f"

   997     obtain b1 a1 where 2: "b' = f b1 \<and> f a = f a1" and

   998                        3: "(b1,a1) \<in> r \<and> {a1,b1} \<le> Field r"

   999     using ** unfolding dir_image_def Field_def by blast

  1000     hence "a = a1" using 1 A_def INJ unfolding inj_on_def by auto

  1001     hence "b1 \<in> A \<and> (b1,a) \<in> r" using 2 3 A_def * by auto

  1002     with 1 show False by auto

  1003   qed

  1004   thus "\<exists>a'\<in>A'. \<forall>b'\<in>A'. (b', a') \<notin> dir_image r f"

  1005   using A_def 1 by blast

  1006 qed

  1007

  1008 lemma Well_order_dir_image:

  1009 "\<lbrakk>Well_order r; inj_on f (Field r)\<rbrakk> \<Longrightarrow> Well_order (dir_image r f)"

  1010 unfolding well_order_on_def

  1011 using Linear_order_dir_image[of r f] wf_dir_image[of "r - Id" f]

  1012   dir_image_minus_Id[of f r]

  1013   subset_inj_on[of f "Field r" "Field(r - Id)"]

  1014   mono_Field[of "r - Id" r] by auto

  1015

  1016 lemma dir_image_bij_betw:

  1017 "\<lbrakk>inj_on f (Field r)\<rbrakk> \<Longrightarrow> bij_betw f (Field r) (Field (dir_image r f))"

  1018 unfolding bij_betw_def by (simp add: dir_image_Field order_on_defs)

  1019

  1020 lemma dir_image_compat:

  1021 "compat r (dir_image r f) f"

  1022 unfolding compat_def dir_image_def by auto

  1023

  1024 lemma dir_image_iso:

  1025 "\<lbrakk>Well_order r; inj_on f (Field r)\<rbrakk>  \<Longrightarrow> iso r (dir_image r f) f"

  1026 using iso_iff3 dir_image_compat dir_image_bij_betw Well_order_dir_image by blast

  1027

  1028 lemma dir_image_ordIso:

  1029 "\<lbrakk>Well_order r; inj_on f (Field r)\<rbrakk>  \<Longrightarrow> r =o dir_image r f"

  1030 unfolding ordIso_def using dir_image_iso Well_order_dir_image by blast

  1031

  1032 lemma Well_order_iso_copy:

  1033 assumes WELL: "well_order_on A r" and BIJ: "bij_betw f A A'"

  1034 shows "\<exists>r'. well_order_on A' r' \<and> r =o r'"

  1035 proof-

  1036    let ?r' = "dir_image r f"

  1037    have 1: "A = Field r \<and> Well_order r"

  1038    using WELL well_order_on_Well_order by blast

  1039    hence 2: "iso r ?r' f"

  1040    using dir_image_iso using BIJ unfolding bij_betw_def by auto

  1041    hence "f  (Field r) = Field ?r'" using 1 iso_iff[of r ?r'] by blast

  1042    hence "Field ?r' = A'"

  1043    using 1 BIJ unfolding bij_betw_def by auto

  1044    moreover have "Well_order ?r'"

  1045    using 1 Well_order_dir_image BIJ unfolding bij_betw_def by blast

  1046    ultimately show ?thesis unfolding ordIso_def using 1 2 by blast

  1047 qed

  1048

  1049

  1050 subsection \<open>Bounded square\<close>

  1051

  1052 text\<open>This construction essentially defines, for an order relation \<open>r\<close>, a lexicographic

  1053 order \<open>bsqr r\<close> on \<open>(Field r) \<times> (Field r)\<close>, applying the

  1054 following criteria (in this order):

  1055 \begin{itemize}

  1056 \item compare the maximums;

  1057 \item compare the first components;

  1058 \item compare the second components.

  1059 \end{itemize}

  1060 %

  1061 The only application of this construction that we are aware of is

  1062 at proving that the square of an infinite set has the same cardinal

  1063 as that set. The essential property required there (and which is ensured by this

  1064 construction) is that any proper order filter of the product order is included in a rectangle, i.e.,

  1065 in a product of proper filters on the original relation (assumed to be a well-order).\<close>

  1066

  1067 definition bsqr :: "'a rel => ('a * 'a)rel"

  1068 where

  1069 "bsqr r = {((a1,a2),(b1,b2)).

  1070            {a1,a2,b1,b2} \<le> Field r \<and>

  1071            (a1 = b1 \<and> a2 = b2 \<or>

  1072             (wo_rel.max2 r a1 a2, wo_rel.max2 r b1 b2) \<in> r - Id \<or>

  1073             wo_rel.max2 r a1 a2 = wo_rel.max2 r b1 b2 \<and> (a1,b1) \<in> r - Id \<or>

  1074             wo_rel.max2 r a1 a2 = wo_rel.max2 r b1 b2 \<and> a1 = b1  \<and> (a2,b2) \<in> r - Id

  1075            )}"

  1076

  1077 lemma Field_bsqr:

  1078 "Field (bsqr r) = Field r \<times> Field r"

  1079 proof

  1080   show "Field (bsqr r) \<le> Field r \<times> Field r"

  1081   proof-

  1082     {fix a1 a2 assume "(a1,a2) \<in> Field (bsqr r)"

  1083      moreover

  1084      have "\<And> b1 b2. ((a1,a2),(b1,b2)) \<in> bsqr r \<or> ((b1,b2),(a1,a2)) \<in> bsqr r \<Longrightarrow>

  1085                       a1 \<in> Field r \<and> a2 \<in> Field r" unfolding bsqr_def by auto

  1086      ultimately have "a1 \<in> Field r \<and> a2 \<in> Field r" unfolding Field_def by auto

  1087     }

  1088     thus ?thesis unfolding Field_def by force

  1089   qed

  1090 next

  1091   show "Field r \<times> Field r \<le> Field (bsqr r)"

  1092   proof(auto)

  1093     fix a1 a2 assume "a1 \<in> Field r" and "a2 \<in> Field r"

  1094     hence "((a1,a2),(a1,a2)) \<in> bsqr r" unfolding bsqr_def by blast

  1095     thus "(a1,a2) \<in> Field (bsqr r)" unfolding Field_def by auto

  1096   qed

  1097 qed

  1098

  1099 lemma bsqr_Refl: "Refl(bsqr r)"

  1100 by(unfold refl_on_def Field_bsqr, auto simp add: bsqr_def)

  1101

  1102 lemma bsqr_Trans:

  1103 assumes "Well_order r"

  1104 shows "trans (bsqr r)"

  1105 proof(unfold trans_def, auto)

  1106   (* Preliminary facts *)

  1107   have Well: "wo_rel r" using assms wo_rel_def by auto

  1108   hence Trans: "trans r" using wo_rel.TRANS by auto

  1109   have Anti: "antisym r" using wo_rel.ANTISYM Well by auto

  1110   hence TransS: "trans(r - Id)" using Trans by (simp add: trans_diff_Id)

  1111   (* Main proof *)

  1112   fix a1 a2 b1 b2 c1 c2

  1113   assume *: "((a1,a2),(b1,b2)) \<in> bsqr r" and **: "((b1,b2),(c1,c2)) \<in> bsqr r"

  1114   hence 0: "{a1,a2,b1,b2,c1,c2} \<le> Field r" unfolding bsqr_def by auto

  1115   have 1: "a1 = b1 \<and> a2 = b2 \<or> (wo_rel.max2 r a1 a2, wo_rel.max2 r b1 b2) \<in> r - Id \<or>

  1116            wo_rel.max2 r a1 a2 = wo_rel.max2 r b1 b2 \<and> (a1,b1) \<in> r - Id \<or>

  1117            wo_rel.max2 r a1 a2 = wo_rel.max2 r b1 b2 \<and> a1 = b1 \<and> (a2,b2) \<in> r - Id"

  1118   using * unfolding bsqr_def by auto

  1119   have 2: "b1 = c1 \<and> b2 = c2 \<or> (wo_rel.max2 r b1 b2, wo_rel.max2 r c1 c2) \<in> r - Id \<or>

  1120            wo_rel.max2 r b1 b2 = wo_rel.max2 r c1 c2 \<and> (b1,c1) \<in> r - Id \<or>

  1121            wo_rel.max2 r b1 b2 = wo_rel.max2 r c1 c2 \<and> b1 = c1 \<and> (b2,c2) \<in> r - Id"

  1122   using ** unfolding bsqr_def by auto

  1123   show "((a1,a2),(c1,c2)) \<in> bsqr r"

  1124   proof-

  1125     {assume Case1: "a1 = b1 \<and> a2 = b2"

  1126      hence ?thesis using ** by simp

  1127     }

  1128     moreover

  1129     {assume Case2: "(wo_rel.max2 r a1 a2, wo_rel.max2 r b1 b2) \<in> r - Id"

  1130      {assume Case21: "b1 = c1 \<and> b2 = c2"

  1131       hence ?thesis using * by simp

  1132      }

  1133      moreover

  1134      {assume Case22: "(wo_rel.max2 r b1 b2, wo_rel.max2 r c1 c2) \<in> r - Id"

  1135       hence "(wo_rel.max2 r a1 a2, wo_rel.max2 r c1 c2) \<in> r - Id"

  1136       using Case2 TransS trans_def[of "r - Id"] by blast

  1137       hence ?thesis using 0 unfolding bsqr_def by auto

  1138      }

  1139      moreover

  1140      {assume Case23_4: "wo_rel.max2 r b1 b2 = wo_rel.max2 r c1 c2"

  1141       hence ?thesis using Case2 0 unfolding bsqr_def by auto

  1142      }

  1143      ultimately have ?thesis using 0 2 by auto

  1144     }

  1145     moreover

  1146     {assume Case3: "wo_rel.max2 r a1 a2 = wo_rel.max2 r b1 b2 \<and> (a1,b1) \<in> r - Id"

  1147      {assume Case31: "b1 = c1 \<and> b2 = c2"

  1148       hence ?thesis using * by simp

  1149      }

  1150      moreover

  1151      {assume Case32: "(wo_rel.max2 r b1 b2, wo_rel.max2 r c1 c2) \<in> r - Id"

  1152       hence ?thesis using Case3 0 unfolding bsqr_def by auto

  1153      }

  1154      moreover

  1155      {assume Case33: "wo_rel.max2 r b1 b2 = wo_rel.max2 r c1 c2 \<and> (b1,c1) \<in> r - Id"

  1156       hence "(a1,c1) \<in> r - Id"

  1157       using Case3 TransS trans_def[of "r - Id"] by blast

  1158       hence ?thesis using Case3 Case33 0 unfolding bsqr_def by auto

  1159      }

  1160      moreover

  1161      {assume Case33: "wo_rel.max2 r b1 b2 = wo_rel.max2 r c1 c2 \<and> b1 = c1"

  1162       hence ?thesis using Case3 0 unfolding bsqr_def by auto

  1163      }

  1164      ultimately have ?thesis using 0 2 by auto

  1165     }

  1166     moreover

  1167     {assume Case4: "wo_rel.max2 r a1 a2 = wo_rel.max2 r b1 b2 \<and> a1 = b1 \<and> (a2,b2) \<in> r - Id"

  1168      {assume Case41: "b1 = c1 \<and> b2 = c2"

  1169       hence ?thesis using * by simp

  1170      }

  1171      moreover

  1172      {assume Case42: "(wo_rel.max2 r b1 b2, wo_rel.max2 r c1 c2) \<in> r - Id"

  1173       hence ?thesis using Case4 0 unfolding bsqr_def by force

  1174      }

  1175      moreover

  1176      {assume Case43: "wo_rel.max2 r b1 b2 = wo_rel.max2 r c1 c2 \<and> (b1,c1) \<in> r - Id"

  1177       hence ?thesis using Case4 0 unfolding bsqr_def by auto

  1178      }

  1179      moreover

  1180      {assume Case44: "wo_rel.max2 r b1 b2 = wo_rel.max2 r c1 c2 \<and> b1 = c1 \<and> (b2,c2) \<in> r - Id"

  1181       hence "(a2,c2) \<in> r - Id"

  1182       using Case4 TransS trans_def[of "r - Id"] by blast

  1183       hence ?thesis using Case4 Case44 0 unfolding bsqr_def by auto

  1184      }

  1185      ultimately have ?thesis using 0 2 by auto

  1186     }

  1187     ultimately show ?thesis using 0 1 by auto

  1188   qed

  1189 qed

  1190

  1191 lemma bsqr_antisym:

  1192 assumes "Well_order r"

  1193 shows "antisym (bsqr r)"

  1194 proof(unfold antisym_def, clarify)

  1195   (* Preliminary facts *)

  1196   have Well: "wo_rel r" using assms wo_rel_def by auto

  1197   hence Trans: "trans r" using wo_rel.TRANS by auto

  1198   have Anti: "antisym r" using wo_rel.ANTISYM Well by auto

  1199   hence TransS: "trans(r - Id)" using Trans by (simp add: trans_diff_Id)

  1200   hence IrrS: "\<forall>a b. \<not>((a,b) \<in> r - Id \<and> (b,a) \<in> r - Id)"

  1201   using Anti trans_def[of "r - Id"] antisym_def[of "r - Id"] by blast

  1202   (* Main proof *)

  1203   fix a1 a2 b1 b2

  1204   assume *: "((a1,a2),(b1,b2)) \<in> bsqr r" and **: "((b1,b2),(a1,a2)) \<in> bsqr r"

  1205   hence 0: "{a1,a2,b1,b2} \<le> Field r" unfolding bsqr_def by auto

  1206   have 1: "a1 = b1 \<and> a2 = b2 \<or> (wo_rel.max2 r a1 a2, wo_rel.max2 r b1 b2) \<in> r - Id \<or>

  1207            wo_rel.max2 r a1 a2 = wo_rel.max2 r b1 b2 \<and> (a1,b1) \<in> r - Id \<or>

  1208            wo_rel.max2 r a1 a2 = wo_rel.max2 r b1 b2 \<and> a1 = b1 \<and> (a2,b2) \<in> r - Id"

  1209   using * unfolding bsqr_def by auto

  1210   have 2: "b1 = a1 \<and> b2 = a2 \<or> (wo_rel.max2 r b1 b2, wo_rel.max2 r a1 a2) \<in> r - Id \<or>

  1211            wo_rel.max2 r b1 b2 = wo_rel.max2 r a1 a2 \<and> (b1,a1) \<in> r - Id \<or>

  1212            wo_rel.max2 r b1 b2 = wo_rel.max2 r a1 a2 \<and> b1 = a1 \<and> (b2,a2) \<in> r - Id"

  1213   using ** unfolding bsqr_def by auto

  1214   show "a1 = b1 \<and> a2 = b2"

  1215   proof-

  1216     {assume Case1: "(wo_rel.max2 r a1 a2, wo_rel.max2 r b1 b2) \<in> r - Id"

  1217      {assume Case11: "(wo_rel.max2 r b1 b2, wo_rel.max2 r a1 a2) \<in> r - Id"

  1218       hence False using Case1 IrrS by blast

  1219      }

  1220      moreover

  1221      {assume Case12_3: "wo_rel.max2 r b1 b2 = wo_rel.max2 r a1 a2"

  1222       hence False using Case1 by auto

  1223      }

  1224      ultimately have ?thesis using 0 2 by auto

  1225     }

  1226     moreover

  1227     {assume Case2: "wo_rel.max2 r a1 a2 = wo_rel.max2 r b1 b2 \<and> (a1,b1) \<in> r - Id"

  1228      {assume Case21: "(wo_rel.max2 r b1 b2, wo_rel.max2 r a1 a2) \<in> r - Id"

  1229        hence False using Case2 by auto

  1230      }

  1231      moreover

  1232      {assume Case22: "(b1,a1) \<in> r - Id"

  1233       hence False using Case2 IrrS by blast

  1234      }

  1235      moreover

  1236      {assume Case23: "b1 = a1"

  1237       hence False using Case2 by auto

  1238      }

  1239      ultimately have ?thesis using 0 2 by auto

  1240     }

  1241     moreover

  1242     {assume Case3: "wo_rel.max2 r a1 a2 = wo_rel.max2 r b1 b2 \<and> a1 = b1 \<and> (a2,b2) \<in> r - Id"

  1243      moreover

  1244      {assume Case31: "(wo_rel.max2 r b1 b2, wo_rel.max2 r a1 a2) \<in> r - Id"

  1245       hence False using Case3 by auto

  1246      }

  1247      moreover

  1248      {assume Case32: "(b1,a1) \<in> r - Id"

  1249       hence False using Case3 by auto

  1250      }

  1251      moreover

  1252      {assume Case33: "(b2,a2) \<in> r - Id"

  1253       hence False using Case3 IrrS by blast

  1254      }

  1255      ultimately have ?thesis using 0 2 by auto

  1256     }

  1257     ultimately show ?thesis using 0 1 by blast

  1258   qed

  1259 qed

  1260

  1261 lemma bsqr_Total:

  1262 assumes "Well_order r"

  1263 shows "Total(bsqr r)"

  1264 proof-

  1265   (* Preliminary facts *)

  1266   have Well: "wo_rel r" using assms wo_rel_def by auto

  1267   hence Total: "\<forall>a \<in> Field r. \<forall>b \<in> Field r. (a,b) \<in> r \<or> (b,a) \<in> r"

  1268   using wo_rel.TOTALS by auto

  1269   (* Main proof *)

  1270   {fix a1 a2 b1 b2 assume "{(a1,a2), (b1,b2)} \<le> Field(bsqr r)"

  1271    hence 0: "a1 \<in> Field r \<and> a2 \<in> Field r \<and> b1 \<in> Field r \<and> b2 \<in> Field r"

  1272    using Field_bsqr by blast

  1273    have "((a1,a2) = (b1,b2) \<or> ((a1,a2),(b1,b2)) \<in> bsqr r \<or> ((b1,b2),(a1,a2)) \<in> bsqr r)"

  1274    proof(rule wo_rel.cases_Total[of r a1 a2], clarsimp simp add: Well, simp add: 0)

  1275        (* Why didn't clarsimp simp add: Well 0 do the same job? *)

  1276      assume Case1: "(a1,a2) \<in> r"

  1277      hence 1: "wo_rel.max2 r a1 a2 = a2"

  1278      using Well 0 by (simp add: wo_rel.max2_equals2)

  1279      show ?thesis

  1280      proof(rule wo_rel.cases_Total[of r b1 b2], clarsimp simp add: Well, simp add: 0)

  1281        assume Case11: "(b1,b2) \<in> r"

  1282        hence 2: "wo_rel.max2 r b1 b2 = b2"

  1283        using Well 0 by (simp add: wo_rel.max2_equals2)

  1284        show ?thesis

  1285        proof(rule wo_rel.cases_Total3[of r a2 b2], clarsimp simp add: Well, simp add: 0)

  1286          assume Case111: "(a2,b2) \<in> r - Id \<or> (b2,a2) \<in> r - Id"

  1287          thus ?thesis using 0 1 2 unfolding bsqr_def by auto

  1288        next

  1289          assume Case112: "a2 = b2"

  1290          show ?thesis

  1291          proof(rule wo_rel.cases_Total3[of r a1 b1], clarsimp simp add: Well, simp add: 0)

  1292            assume Case1121: "(a1,b1) \<in> r - Id \<or> (b1,a1) \<in> r - Id"

  1293            thus ?thesis using 0 1 2 Case112 unfolding bsqr_def by auto

  1294          next

  1295            assume Case1122: "a1 = b1"

  1296            thus ?thesis using Case112 by auto

  1297          qed

  1298        qed

  1299      next

  1300        assume Case12: "(b2,b1) \<in> r"

  1301        hence 3: "wo_rel.max2 r b1 b2 = b1" using Well 0 by (simp add: wo_rel.max2_equals1)

  1302        show ?thesis

  1303        proof(rule wo_rel.cases_Total3[of r a2 b1], clarsimp simp add: Well, simp add: 0)

  1304          assume Case121: "(a2,b1) \<in> r - Id \<or> (b1,a2) \<in> r - Id"

  1305          thus ?thesis using 0 1 3 unfolding bsqr_def by auto

  1306        next

  1307          assume Case122: "a2 = b1"

  1308          show ?thesis

  1309          proof(rule wo_rel.cases_Total3[of r a1 b1], clarsimp simp add: Well, simp add: 0)

  1310            assume Case1221: "(a1,b1) \<in> r - Id \<or> (b1,a1) \<in> r - Id"

  1311            thus ?thesis using 0 1 3 Case122 unfolding bsqr_def by auto

  1312          next

  1313            assume Case1222: "a1 = b1"

  1314            show ?thesis

  1315            proof(rule wo_rel.cases_Total3[of r a2 b2], clarsimp simp add: Well, simp add: 0)

  1316              assume Case12221: "(a2,b2) \<in> r - Id \<or> (b2,a2) \<in> r - Id"

  1317              thus ?thesis using 0 1 3 Case122 Case1222 unfolding bsqr_def by auto

  1318            next

  1319              assume Case12222: "a2 = b2"

  1320              thus ?thesis using Case122 Case1222 by auto

  1321            qed

  1322          qed

  1323        qed

  1324      qed

  1325    next

  1326      assume Case2: "(a2,a1) \<in> r"

  1327      hence 1: "wo_rel.max2 r a1 a2 = a1" using Well 0 by (simp add: wo_rel.max2_equals1)

  1328      show ?thesis

  1329      proof(rule wo_rel.cases_Total[of r b1 b2], clarsimp simp add: Well, simp add: 0)

  1330        assume Case21: "(b1,b2) \<in> r"

  1331        hence 2: "wo_rel.max2 r b1 b2 = b2" using Well 0 by (simp add: wo_rel.max2_equals2)

  1332        show ?thesis

  1333        proof(rule wo_rel.cases_Total3[of r a1 b2], clarsimp simp add: Well, simp add: 0)

  1334          assume Case211: "(a1,b2) \<in> r - Id \<or> (b2,a1) \<in> r - Id"

  1335          thus ?thesis using 0 1 2 unfolding bsqr_def by auto

  1336        next

  1337          assume Case212: "a1 = b2"

  1338          show ?thesis

  1339          proof(rule wo_rel.cases_Total3[of r a1 b1], clarsimp simp add: Well, simp add: 0)

  1340            assume Case2121: "(a1,b1) \<in> r - Id \<or> (b1,a1) \<in> r - Id"

  1341            thus ?thesis using 0 1 2 Case212 unfolding bsqr_def by auto

  1342          next

  1343            assume Case2122: "a1 = b1"

  1344            show ?thesis

  1345            proof(rule wo_rel.cases_Total3[of r a2 b2], clarsimp simp add: Well, simp add: 0)

  1346              assume Case21221: "(a2,b2) \<in> r - Id \<or> (b2,a2) \<in> r - Id"

  1347              thus ?thesis using 0 1 2 Case212 Case2122 unfolding bsqr_def by auto

  1348            next

  1349              assume Case21222: "a2 = b2"

  1350              thus ?thesis using Case2122 Case212 by auto

  1351            qed

  1352          qed

  1353        qed

  1354      next

  1355        assume Case22: "(b2,b1) \<in> r"

  1356        hence 3: "wo_rel.max2 r b1 b2 = b1"  using Well 0 by (simp add: wo_rel.max2_equals1)

  1357        show ?thesis

  1358        proof(rule wo_rel.cases_Total3[of r a1 b1], clarsimp simp add: Well, simp add: 0)

  1359          assume Case221: "(a1,b1) \<in> r - Id \<or> (b1,a1) \<in> r - Id"

  1360          thus ?thesis using 0 1 3 unfolding bsqr_def by auto

  1361        next

  1362          assume Case222: "a1 = b1"

  1363          show ?thesis

  1364          proof(rule wo_rel.cases_Total3[of r a2 b2], clarsimp simp add: Well, simp add: 0)

  1365            assume Case2221: "(a2,b2) \<in> r - Id \<or> (b2,a2) \<in> r - Id"

  1366            thus ?thesis using 0 1 3 Case222 unfolding bsqr_def by auto

  1367          next

  1368            assume Case2222: "a2 = b2"

  1369            thus ?thesis using Case222 by auto

  1370          qed

  1371        qed

  1372      qed

  1373    qed

  1374   }

  1375   thus ?thesis unfolding total_on_def by fast

  1376 qed

  1377

  1378 lemma bsqr_Linear_order:

  1379 assumes "Well_order r"

  1380 shows "Linear_order(bsqr r)"

  1381 unfolding order_on_defs

  1382 using assms bsqr_Refl bsqr_Trans bsqr_antisym bsqr_Total by blast

  1383

  1384 lemma bsqr_Well_order:

  1385 assumes "Well_order r"

  1386 shows "Well_order(bsqr r)"

  1387 using assms

  1388 proof(simp add: bsqr_Linear_order Linear_order_Well_order_iff, intro allI impI)

  1389   have 0: "\<forall>A \<le> Field r. A \<noteq> {} \<longrightarrow> (\<exists>a \<in> A. \<forall>a' \<in> A. (a,a') \<in> r)"

  1390   using assms well_order_on_def Linear_order_Well_order_iff by blast

  1391   fix D assume *: "D \<le> Field (bsqr r)" and **: "D \<noteq> {}"

  1392   hence 1: "D \<le> Field r \<times> Field r" unfolding Field_bsqr by simp

  1393   (*  *)

  1394   obtain M where M_def: "M = {wo_rel.max2 r a1 a2| a1 a2. (a1,a2) \<in> D}" by blast

  1395   have "M \<noteq> {}" using 1 M_def ** by auto

  1396   moreover

  1397   have "M \<le> Field r" unfolding M_def

  1398   using 1 assms wo_rel_def[of r] wo_rel.max2_among[of r] by fastforce

  1399   ultimately obtain m where m_min: "m \<in> M \<and> (\<forall>a \<in> M. (m,a) \<in> r)"

  1400   using 0 by blast

  1401   (*  *)

  1402   obtain A1 where A1_def: "A1 = {a1. \<exists>a2. (a1,a2) \<in> D \<and> wo_rel.max2 r a1 a2 = m}" by blast

  1403   have "A1 \<le> Field r" unfolding A1_def using 1 by auto

  1404   moreover have "A1 \<noteq> {}" unfolding A1_def using m_min unfolding M_def by blast

  1405   ultimately obtain a1 where a1_min: "a1 \<in> A1 \<and> (\<forall>a \<in> A1. (a1,a) \<in> r)"

  1406   using 0 by blast

  1407   (*  *)

  1408   obtain A2 where A2_def: "A2 = {a2. (a1,a2) \<in> D \<and> wo_rel.max2 r a1 a2 = m}" by blast

  1409   have "A2 \<le> Field r" unfolding A2_def using 1 by auto

  1410   moreover have "A2 \<noteq> {}" unfolding A2_def

  1411   using m_min a1_min unfolding A1_def M_def by blast

  1412   ultimately obtain a2 where a2_min: "a2 \<in> A2 \<and> (\<forall>a \<in> A2. (a2,a) \<in> r)"

  1413   using 0 by blast

  1414   (*   *)

  1415   have 2: "wo_rel.max2 r a1 a2 = m"

  1416   using a1_min a2_min unfolding A1_def A2_def by auto

  1417   have 3: "(a1,a2) \<in> D" using a2_min unfolding A2_def by auto

  1418   (*  *)

  1419   moreover

  1420   {fix b1 b2 assume ***: "(b1,b2) \<in> D"

  1421    hence 4: "{a1,a2,b1,b2} \<le> Field r" using 1 3 by blast

  1422    have 5: "(wo_rel.max2 r a1 a2, wo_rel.max2 r b1 b2) \<in> r"

  1423    using *** a1_min a2_min m_min unfolding A1_def A2_def M_def by auto

  1424    have "((a1,a2),(b1,b2)) \<in> bsqr r"

  1425    proof(cases "wo_rel.max2 r a1 a2 = wo_rel.max2 r b1 b2")

  1426      assume Case1: "wo_rel.max2 r a1 a2 \<noteq> wo_rel.max2 r b1 b2"

  1427      thus ?thesis unfolding bsqr_def using 4 5 by auto

  1428    next

  1429      assume Case2: "wo_rel.max2 r a1 a2 = wo_rel.max2 r b1 b2"

  1430      hence "b1 \<in> A1" unfolding A1_def using 2 *** by auto

  1431      hence 6: "(a1,b1) \<in> r" using a1_min by auto

  1432      show ?thesis

  1433      proof(cases "a1 = b1")

  1434        assume Case21: "a1 \<noteq> b1"

  1435        thus ?thesis unfolding bsqr_def using 4 Case2 6 by auto

  1436      next

  1437        assume Case22: "a1 = b1"

  1438        hence "b2 \<in> A2" unfolding A2_def using 2 *** Case2 by auto

  1439        hence 7: "(a2,b2) \<in> r" using a2_min by auto

  1440        thus ?thesis unfolding bsqr_def using 4 7 Case2 Case22 by auto

  1441      qed

  1442    qed

  1443   }

  1444   (*  *)

  1445   ultimately show "\<exists>d \<in> D. \<forall>d' \<in> D. (d,d') \<in> bsqr r" by fastforce

  1446 qed

  1447

  1448 lemma bsqr_max2:

  1449 assumes WELL: "Well_order r" and LEQ: "((a1,a2),(b1,b2)) \<in> bsqr r"

  1450 shows "(wo_rel.max2 r a1 a2, wo_rel.max2 r b1 b2) \<in> r"

  1451 proof-

  1452   have "{(a1,a2),(b1,b2)} \<le> Field(bsqr r)"

  1453   using LEQ unfolding Field_def by auto

  1454   hence "{a1,a2,b1,b2} \<le> Field r" unfolding Field_bsqr by auto

  1455   hence "{wo_rel.max2 r a1 a2, wo_rel.max2 r b1 b2} \<le> Field r"

  1456   using WELL wo_rel_def[of r] wo_rel.max2_among[of r] by fastforce

  1457   moreover have "(wo_rel.max2 r a1 a2, wo_rel.max2 r b1 b2) \<in> r \<or> wo_rel.max2 r a1 a2 = wo_rel.max2 r b1 b2"

  1458   using LEQ unfolding bsqr_def by auto

  1459   ultimately show ?thesis using WELL unfolding order_on_defs refl_on_def by auto

  1460 qed

  1461

  1462 lemma bsqr_ofilter:

  1463 assumes WELL: "Well_order r" and

  1464         OF: "wo_rel.ofilter (bsqr r) D" and SUB: "D < Field r \<times> Field r" and

  1465         NE: "\<not> (\<exists>a. Field r = under r a)"

  1466 shows "\<exists>A. wo_rel.ofilter r A \<and> A < Field r \<and> D \<le> A \<times> A"

  1467 proof-

  1468   let ?r' = "bsqr r"

  1469   have Well: "wo_rel r" using WELL wo_rel_def by blast

  1470   hence Trans: "trans r" using wo_rel.TRANS by blast

  1471   have Well': "Well_order ?r' \<and> wo_rel ?r'"

  1472   using WELL bsqr_Well_order wo_rel_def by blast

  1473   (*  *)

  1474   have "D < Field ?r'" unfolding Field_bsqr using SUB .

  1475   with OF obtain a1 and a2 where

  1476   "(a1,a2) \<in> Field ?r'" and 1: "D = underS ?r' (a1,a2)"

  1477   using Well' wo_rel.ofilter_underS_Field[of ?r' D] by auto

  1478   hence 2: "{a1,a2} \<le> Field r" unfolding Field_bsqr by auto

  1479   let ?m = "wo_rel.max2 r a1 a2"

  1480   have "D \<le> (under r ?m) \<times> (under r ?m)"

  1481   proof(unfold 1)

  1482     {fix b1 b2

  1483      let ?n = "wo_rel.max2 r b1 b2"

  1484      assume "(b1,b2) \<in> underS ?r' (a1,a2)"

  1485      hence 3: "((b1,b2),(a1,a2)) \<in> ?r'"

  1486      unfolding underS_def by blast

  1487      hence "(?n,?m) \<in> r" using WELL by (simp add: bsqr_max2)

  1488      moreover

  1489      {have "(b1,b2) \<in> Field ?r'" using 3 unfolding Field_def by auto

  1490       hence "{b1,b2} \<le> Field r" unfolding Field_bsqr by auto

  1491       hence "(b1,?n) \<in> r \<and> (b2,?n) \<in> r"

  1492       using Well by (simp add: wo_rel.max2_greater)

  1493      }

  1494      ultimately have "(b1,?m) \<in> r \<and> (b2,?m) \<in> r"

  1495      using Trans trans_def[of r] by blast

  1496      hence "(b1,b2) \<in> (under r ?m) \<times> (under r ?m)" unfolding under_def by simp}

  1497      thus "underS ?r' (a1,a2) \<le> (under r ?m) \<times> (under r ?m)" by auto

  1498   qed

  1499   moreover have "wo_rel.ofilter r (under r ?m)"

  1500   using Well by (simp add: wo_rel.under_ofilter)

  1501   moreover have "under r ?m < Field r"

  1502   using NE under_Field[of r ?m] by blast

  1503   ultimately show ?thesis by blast

  1504 qed

  1505

  1506 definition Func where

  1507 "Func A B = {f . (\<forall> a \<in> A. f a \<in> B) \<and> (\<forall> a. a \<notin> A \<longrightarrow> f a = undefined)}"

  1508

  1509 lemma Func_empty:

  1510 "Func {} B = {\<lambda>x. undefined}"

  1511 unfolding Func_def by auto

  1512

  1513 lemma Func_elim:

  1514 assumes "g \<in> Func A B" and "a \<in> A"

  1515 shows "\<exists> b. b \<in> B \<and> g a = b"

  1516 using assms unfolding Func_def by (cases "g a = undefined") auto

  1517

  1518 definition curr where

  1519 "curr A f \<equiv> \<lambda> a. if a \<in> A then \<lambda>b. f (a,b) else undefined"

  1520

  1521 lemma curr_in:

  1522 assumes f: "f \<in> Func (A \<times> B) C"

  1523 shows "curr A f \<in> Func A (Func B C)"

  1524 using assms unfolding curr_def Func_def by auto

  1525

  1526 lemma curr_inj:

  1527 assumes "f1 \<in> Func (A \<times> B) C" and "f2 \<in> Func (A \<times> B) C"

  1528 shows "curr A f1 = curr A f2 \<longleftrightarrow> f1 = f2"

  1529 proof safe

  1530   assume c: "curr A f1 = curr A f2"

  1531   show "f1 = f2"

  1532   proof (rule ext, clarify)

  1533     fix a b show "f1 (a, b) = f2 (a, b)"

  1534     proof (cases "(a,b) \<in> A \<times> B")

  1535       case False

  1536       thus ?thesis using assms unfolding Func_def by auto

  1537     next

  1538       case True hence a: "a \<in> A" and b: "b \<in> B" by auto

  1539       thus ?thesis

  1540       using c unfolding curr_def fun_eq_iff by(elim allE[of _ a]) simp

  1541     qed

  1542   qed

  1543 qed

  1544

  1545 lemma curr_surj:

  1546 assumes "g \<in> Func A (Func B C)"

  1547 shows "\<exists> f \<in> Func (A \<times> B) C. curr A f = g"

  1548 proof

  1549   let ?f = "\<lambda> ab. if fst ab \<in> A \<and> snd ab \<in> B then g (fst ab) (snd ab) else undefined"

  1550   show "curr A ?f = g"

  1551   proof (rule ext)

  1552     fix a show "curr A ?f a = g a"

  1553     proof (cases "a \<in> A")

  1554       case False

  1555       hence "g a = undefined" using assms unfolding Func_def by auto

  1556       thus ?thesis unfolding curr_def using False by simp

  1557     next

  1558       case True

  1559       obtain g1 where "g1 \<in> Func B C" and "g a = g1"

  1560       using assms using Func_elim[OF assms True] by blast

  1561       thus ?thesis using True unfolding Func_def curr_def by auto

  1562     qed

  1563   qed

  1564   show "?f \<in> Func (A \<times> B) C" using assms unfolding Func_def mem_Collect_eq by auto

  1565 qed

  1566

  1567 lemma bij_betw_curr:

  1568 "bij_betw (curr A) (Func (A \<times> B) C) (Func A (Func B C))"

  1569 unfolding bij_betw_def inj_on_def image_def

  1570 apply (intro impI conjI ballI)

  1571 apply (erule curr_inj[THEN iffD1], assumption+)

  1572 apply auto

  1573 apply (erule curr_in)

  1574 using curr_surj by blast

  1575

  1576 definition Func_map where

  1577 "Func_map B2 f1 f2 g b2 \<equiv> if b2 \<in> B2 then f1 (g (f2 b2)) else undefined"

  1578

  1579 lemma Func_map:

  1580 assumes g: "g \<in> Func A2 A1" and f1: "f1  A1 \<subseteq> B1" and f2: "f2  B2 \<subseteq> A2"

  1581 shows "Func_map B2 f1 f2 g \<in> Func B2 B1"

  1582 using assms unfolding Func_def Func_map_def mem_Collect_eq by auto

  1583

  1584 lemma Func_non_emp:

  1585 assumes "B \<noteq> {}"

  1586 shows "Func A B \<noteq> {}"

  1587 proof-

  1588   obtain b where b: "b \<in> B" using assms by auto

  1589   hence "(\<lambda> a. if a \<in> A then b else undefined) \<in> Func A B" unfolding Func_def by auto

  1590   thus ?thesis by blast

  1591 qed

  1592

  1593 lemma Func_is_emp:

  1594 "Func A B = {} \<longleftrightarrow> A \<noteq> {} \<and> B = {}" (is "?L \<longleftrightarrow> ?R")

  1595 proof

  1596   assume L: ?L

  1597   moreover {assume "A = {}" hence False using L Func_empty by auto}

  1598   moreover {assume "B \<noteq> {}" hence False using L Func_non_emp[of B A] by simp }

  1599   ultimately show ?R by blast

  1600 next

  1601   assume R: ?R

  1602   moreover

  1603   {fix f assume "f \<in> Func A B"

  1604    moreover obtain a where "a \<in> A" using R by blast

  1605    ultimately obtain b where "b \<in> B" unfolding Func_def by blast

  1606    with R have False by blast

  1607   }

  1608   thus ?L by blast

  1609 qed

  1610

  1611 lemma Func_map_surj:

  1612 assumes B1: "f1  A1 = B1" and A2: "inj_on f2 B2" "f2  B2 \<subseteq> A2"

  1613 and B2A2: "B2 = {} \<Longrightarrow> A2 = {}"

  1614 shows "Func B2 B1 = Func_map B2 f1 f2  Func A2 A1"

  1615 proof(cases "B2 = {}")

  1616   case True

  1617   thus ?thesis using B2A2 by (auto simp: Func_empty Func_map_def)

  1618 next

  1619   case False note B2 = False

  1620   show ?thesis

  1621   proof safe

  1622     fix h assume h: "h \<in> Func B2 B1"

  1623     define j1 where "j1 = inv_into A1 f1"

  1624     have "\<forall> a2 \<in> f2  B2. \<exists> b2. b2 \<in> B2 \<and> f2 b2 = a2" by blast

  1625     then obtain k where k: "\<forall> a2 \<in> f2  B2. k a2 \<in> B2 \<and> f2 (k a2) = a2"

  1626       by atomize_elim (rule bchoice)

  1627     {fix b2 assume b2: "b2 \<in> B2"

  1628      hence "f2 (k (f2 b2)) = f2 b2" using k A2(2) by auto

  1629      moreover have "k (f2 b2) \<in> B2" using b2 A2(2) k by auto

  1630      ultimately have "k (f2 b2) = b2" using b2 A2(1) unfolding inj_on_def by blast

  1631     } note kk = this

  1632     obtain b22 where b22: "b22 \<in> B2" using B2 by auto

  1633     define j2 where [abs_def]: "j2 a2 = (if a2 \<in> f2  B2 then k a2 else b22)" for a2

  1634     have j2A2: "j2  A2 \<subseteq> B2" unfolding j2_def using k b22 by auto

  1635     have j2: "\<And> b2. b2 \<in> B2 \<Longrightarrow> j2 (f2 b2) = b2"

  1636     using kk unfolding j2_def by auto

  1637     define g where "g = Func_map A2 j1 j2 h"

  1638     have "Func_map B2 f1 f2 g = h"

  1639     proof (rule ext)

  1640       fix b2 show "Func_map B2 f1 f2 g b2 = h b2"

  1641       proof(cases "b2 \<in> B2")

  1642         case True

  1643         show ?thesis

  1644         proof (cases "h b2 = undefined")

  1645           case True

  1646           hence b1: "h b2 \<in> f1  A1" using h \<open>b2 \<in> B2\<close> unfolding B1 Func_def by auto

  1647           show ?thesis using A2 f_inv_into_f[OF b1]

  1648             unfolding True g_def Func_map_def j1_def j2[OF \<open>b2 \<in> B2\<close>] by auto

  1649         qed(insert A2 True j2[OF True] h B1, unfold j1_def g_def Func_def Func_map_def,

  1650           auto intro: f_inv_into_f)

  1651       qed(insert h, unfold Func_def Func_map_def, auto)

  1652     qed

  1653     moreover have "g \<in> Func A2 A1" unfolding g_def apply(rule Func_map[OF h])

  1654     using j2A2 B1 A2 unfolding j1_def by (fast intro: inv_into_into)+

  1655     ultimately show "h \<in> Func_map B2 f1 f2  Func A2 A1"

  1656     unfolding Func_map_def[abs_def] by auto

  1657   qed(insert B1 Func_map[OF _ _ A2(2)], auto)

  1658 qed

  1659

  1660 end