src/HOL/BNF_Wellorder_Constructions.thy
 author haftmann Fri Oct 10 19:55:32 2014 +0200 (2014-10-10) changeset 58646 cd63a4b12a33 parent 58127 b7cab82f488e child 58889 5b7a9633cfa8 permissions -rw-r--r--
specialized specification: avoid trivial instances
     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 header {* Constructions on Wellorders as Needed by Bounded Natural Functors *}

     9

    10 theory BNF_Wellorder_Constructions

    11 imports BNF_Wellorder_Embedding

    12 begin

    13

    14 text {* 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 @{text "ordLeq"}, of being embedded (abbreviated @{text "\<le>o"}),

    18 @{text "ordLess"}, of being strictly embedded (abbreviated @{text "<o"}), and

    19 @{text "ordIso"}, of being isomorphic (abbreviated @{text "=o"}).  We study the

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

    21 A main result of this section is that @{text "<o"} is well-founded. *}

    22

    23

    24 subsection {* Restriction to a set *}

    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 antisym_Restr:

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

    41 unfolding antisym_def Field_def by auto

    42

    43 lemma Total_Restr:

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

    45 unfolding total_on_def Field_def by auto

    46

    47 lemma trans_Restr:

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

    49 unfolding trans_def Field_def by blast

    50

    51 lemma Preorder_Restr:

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

    53 unfolding preorder_on_def by (simp add: Refl_Restr trans_Restr)

    54

    55 lemma Partial_order_Restr:

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

    57 unfolding partial_order_on_def by (simp add: Preorder_Restr antisym_Restr)

    58

    59 lemma Linear_order_Restr:

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

    61 unfolding linear_order_on_def by (simp add: Partial_order_Restr Total_Restr)

    62

    63 lemma Well_order_Restr:

    64 assumes "Well_order r"

    65 shows "Well_order(Restr r A)"

    66 proof-

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

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

    69   using well_order_on_def wf_subset by blast

    70   thus ?thesis using assms unfolding well_order_on_def

    71   by (simp add: Linear_order_Restr)

    72 qed

    73

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

    75 by (auto simp add: Field_def)

    76

    77 lemma Refl_Field_Restr:

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

    79 unfolding refl_on_def Field_def by blast

    80

    81 lemma Refl_Field_Restr2:

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

    83 by (auto simp add: Refl_Field_Restr)

    84

    85 lemma well_order_on_Restr:

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

    87 shows "well_order_on A (Restr r A)"

    88 using assms

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

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

    91

    92

    93 subsection {* Order filters versus restrictions and embeddings *}

    94

    95 lemma Field_Restr_ofilter:

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

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

    98

    99 lemma ofilter_Restr_under:

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

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

   102 using assms wo_rel_def

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

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

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

   106   unfolding under_def using Field_def by fastforce

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

   108 qed

   109

   110 lemma ofilter_embed:

   111 assumes "Well_order r"

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

   113 proof

   114   assume *: "wo_rel.ofilter r A"

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

   116   proof(unfold embed_def, auto)

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

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

   119   next

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

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

   122     by (simp add: ofilter_Restr_under Field_Restr_ofilter)

   123   qed

   124 next

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

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

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

   128         Well_order_Restr[of r] by auto

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

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

   131    by (simp add: order_on_defs Refl_Field_Restr2)

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

   133    using * unfolding embed_def by auto

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

   135    unfolding bij_betw_def by auto

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

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

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

   139   }

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

   141 qed

   142

   143 lemma ofilter_Restr_Int:

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

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

   146 proof-

   147   let ?rB = "Restr r B"

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

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

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

   151   using Refl_Field_Restr by blast

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

   153   by (simp add: Well_order_Restr wo_rel_def)

   154   (* Main proof *)

   155   show ?thesis using WellB assms

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

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

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

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

   160   next

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

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

   163   qed

   164 qed

   165

   166 lemma ofilter_Restr_subset:

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

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

   169 proof-

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

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

   172 qed

   173

   174 lemma ofilter_subset_embed:

   175 assumes WELL: "Well_order r" and

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

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

   178 proof-

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

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

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

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

   183   using Refl_Field_Restr by blast

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

   185   using Refl Refl_Field_Restr by blast

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

   187   by (simp add: Well_order_Restr wo_rel_def)

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

   189   by (simp add: Well_order_Restr wo_rel_def)

   190   (* Main proof *)

   191   show ?thesis

   192   proof

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

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

   195     by (simp add: ofilter_Restr_subset)

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

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

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

   199     using * by (simp add: Restr_subset)

   200   next

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

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

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

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

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

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

   207     }

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

   209   qed

   210 qed

   211

   212 lemma ofilter_subset_embedS_iso:

   213 assumes WELL: "Well_order r" and

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

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

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

   217 proof-

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

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

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

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

   222   using Refl_Field_Restr by blast

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

   224   by (auto simp add: wo_rel.ofilter_def)

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

   226   using Refl Refl_Field_Restr by blast

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

   228   by (auto simp add: wo_rel.ofilter_def)

   229   (* Main proof *)

   230   show ?thesis unfolding embedS_def iso_def

   231   using assms ofilter_subset_embed[of r A B]

   232         FieldA FieldB bij_betw_id_iff[of A B] by auto

   233 qed

   234

   235 lemma ofilter_subset_embedS:

   236 assumes WELL: "Well_order r" and

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

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

   239 using assms by (simp add: ofilter_subset_embedS_iso)

   240

   241 lemma embed_implies_iso_Restr:

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

   243         EMB: "embed r' r f"

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

   245 proof-

   246   let ?A' = "Field r'"

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

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

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

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

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

   252   using EMB embed_inj_on WELL' unfolding bij_betw_def by blast

   253   moreover

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

   255    unfolding Field_def by auto

   256    hence "compat r' ?r'' f"

   257    using assms embed_iff_compat_inj_on_ofilter

   258    unfolding compat_def by blast

   259   }

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

   261 qed

   262

   263

   264 subsection {* The strict inclusion on proper ofilters is well-founded *}

   265

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

   267 where

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

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

   270

   271 lemma wf_ofilterIncl:

   272 assumes WELL: "Well_order r"

   273 shows "wf(ofilterIncl r)"

   274 proof-

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

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

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

   278   let ?rS = "r - Id"

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

   280   moreover

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

   282   proof(unfold compat_def ofilterIncl_def,

   283         intro allI impI, simp, elim conjE)

   284     fix A B

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

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

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

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

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

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

   291     moreover

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

   293     by (auto simp add: underS_incl_iff)

   294     moreover

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

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

   297     ultimately

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

   299     by simp

   300   qed

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

   302 qed

   303

   304

   305 subsection {* Ordering the well-orders by existence of embeddings *}

   306

   307 text {* We define three relations between well-orders:

   308 \begin{itemize}

   309 \item @{text "ordLeq"}, of being embedded (abbreviated @{text "\<le>o"});

   310 \item @{text "ordLess"}, of being strictly embedded (abbreviated @{text "<o"});

   311 \item @{text "ordIso"}, of being isomorphic (abbreviated @{text "=o"}).

   312 \end{itemize}

   313 %

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

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

   316 @{text "\<le>"}, @{text "<"}, @{text "="} associated to a total order on a set.

   317 *}

   318

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

   320 where

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

   322

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

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

   325

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

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

   328

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

   330 where

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

   332

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

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

   335

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

   337 where

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

   339

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

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

   342

   343 lemmas ordRels_def = ordLeq_def ordLess_def ordIso_def

   344

   345 lemma ordLeq_Well_order_simp:

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

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

   348 using assms unfolding ordLeq_def by simp

   349

   350 text{* Notice that the relations @{text "\<le>o"}, @{text "<o"}, @{text "=o"} connect well-orders

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

   352 restrict implicitly the type of these relations to @{text "(('a rel) * ('a rel)) set"} , i.e.,

   353 to @{text "'a rel rel"}. *}

   354

   355 lemma ordLeq_reflexive:

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

   357 unfolding ordLeq_def using id_embed[of r] by blast

   358

   359 lemma ordLeq_transitive[trans]:

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

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

   362 proof-

   363   obtain f and f'

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

   365         "embed r r' f" and "embed r' r'' f'"

   366   using * ** unfolding ordLeq_def by blast

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

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

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

   370 qed

   371

   372 lemma ordLeq_total:

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

   374 unfolding ordLeq_def using wellorders_totally_ordered by blast

   375

   376 lemma ordIso_reflexive:

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

   378 unfolding ordIso_def using id_iso[of r] by blast

   379

   380 lemma ordIso_transitive[trans]:

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

   382 shows "r =o r''"

   383 proof-

   384   obtain f and f'

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

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

   387   using * ** unfolding ordIso_def by auto

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

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

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

   391 qed

   392

   393 lemma ordIso_symmetric:

   394 assumes *: "r =o r'"

   395 shows "r' =o r"

   396 proof-

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

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

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

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

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

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

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

   404 qed

   405

   406 lemma ordLeq_ordLess_trans[trans]:

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

   408 shows "r <o r''"

   409 proof-

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

   411   using assms unfolding ordLeq_def ordLess_def by auto

   412   thus ?thesis using assms unfolding ordLeq_def ordLess_def

   413   using embed_comp_embedS by blast

   414 qed

   415

   416 lemma ordLess_ordLeq_trans[trans]:

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

   418 shows "r <o r''"

   419 proof-

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

   421   using assms unfolding ordLeq_def ordLess_def by auto

   422   thus ?thesis using assms unfolding ordLeq_def ordLess_def

   423   using embedS_comp_embed by blast

   424 qed

   425

   426 lemma ordLeq_ordIso_trans[trans]:

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

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

   429 proof-

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

   431   using assms unfolding ordLeq_def ordIso_def by auto

   432   thus ?thesis using assms unfolding ordLeq_def ordIso_def

   433   using embed_comp_iso by blast

   434 qed

   435

   436 lemma ordIso_ordLeq_trans[trans]:

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

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

   439 proof-

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

   441   using assms unfolding ordLeq_def ordIso_def by auto

   442   thus ?thesis using assms unfolding ordLeq_def ordIso_def

   443   using iso_comp_embed by blast

   444 qed

   445

   446 lemma ordLess_ordIso_trans[trans]:

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

   448 shows "r <o r''"

   449 proof-

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

   451   using assms unfolding ordLess_def ordIso_def by auto

   452   thus ?thesis using assms unfolding ordLess_def ordIso_def

   453   using embedS_comp_iso by blast

   454 qed

   455

   456 lemma ordIso_ordLess_trans[trans]:

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

   458 shows "r <o r''"

   459 proof-

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

   461   using assms unfolding ordLess_def ordIso_def by auto

   462   thus ?thesis using assms unfolding ordLess_def ordIso_def

   463   using iso_comp_embedS by blast

   464 qed

   465

   466 lemma ordLess_not_embed:

   467 assumes "r <o r'"

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

   469 proof-

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

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

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

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

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

   475    by (simp add: embed_bothWays_Field_bij_betw)

   476    with 3 have False by contradiction

   477   }

   478   thus ?thesis by blast

   479 qed

   480

   481 lemma ordLess_Field:

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

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

   484 proof-

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

   486   obtain g where

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

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

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

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

   491   using 0 EMB embed_unique[of r1] by auto

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

   493   using 1 bij_betw_cong[of ?A1] by blast

   494   moreover

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

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

   497 qed

   498

   499 lemma ordLess_iff:

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

   501 proof

   502   assume *: "r <o r'"

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

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

   505   unfolding ordLess_def by auto

   506 next

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

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

   509   using wellorders_totally_ordered[of r r'] by blast

   510   moreover

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

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

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

   514    with * have False by blast

   515   }

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

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

   518 qed

   519

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

   521 proof

   522   assume "r <o r"

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

   524   unfolding ordLess_iff ..

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

   526   ultimately show False by blast

   527 qed

   528

   529 lemma ordLeq_iff_ordLess_or_ordIso:

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

   531 unfolding ordRels_def embedS_defs iso_defs by blast

   532

   533 lemma ordIso_iff_ordLeq:

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

   535 proof

   536   assume "r =o r'"

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

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

   539   unfolding ordIso_def iso_defs by auto

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

   541   by (simp add: inv_into_Field_embed_bij_betw)

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

   543   unfolding ordLeq_def using 1 by auto

   544 next

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

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

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

   548   unfolding ordLeq_def by auto

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

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

   551 qed

   552

   553 lemma not_ordLess_ordLeq:

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

   555 using ordLess_ordLeq_trans ordLess_irreflexive by blast

   556

   557 lemma ordLess_or_ordLeq:

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

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

   560 proof-

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

   562   using assms by (simp add: ordLeq_total)

   563   moreover

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

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

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

   567   }

   568   ultimately show ?thesis by blast

   569 qed

   570

   571 lemma not_ordLess_ordIso:

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

   573 using assms ordLess_ordIso_trans ordIso_symmetric ordLess_irreflexive by blast

   574

   575 lemma not_ordLeq_iff_ordLess:

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

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

   578 using assms not_ordLess_ordLeq ordLess_or_ordLeq by blast

   579

   580 lemma not_ordLess_iff_ordLeq:

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

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

   583 using assms not_ordLess_ordLeq ordLess_or_ordLeq by blast

   584

   585 lemma ordLess_transitive[trans]:

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

   587 using assms ordLess_ordLeq_trans ordLeq_iff_ordLess_or_ordIso by blast

   588

   589 corollary ordLess_trans: "trans ordLess"

   590 unfolding trans_def using ordLess_transitive by blast

   591

   592 lemmas ordIso_equivalence = ordIso_transitive ordIso_reflexive ordIso_symmetric

   593

   594 lemma ordIso_imp_ordLeq:

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

   596 using ordIso_iff_ordLeq by blast

   597

   598 lemma ordLess_imp_ordLeq:

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

   600 using ordLeq_iff_ordLess_or_ordIso by blast

   601

   602 lemma ofilter_subset_ordLeq:

   603 assumes WELL: "Well_order r" and

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

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

   606 proof

   607   assume "A \<le> B"

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

   609   unfolding ordLeq_def using assms

   610   Well_order_Restr Well_order_Restr ofilter_subset_embed by blast

   611 next

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

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

   614   unfolding ordLeq_def by blast

   615   {assume "B < A"

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

   617    unfolding ordLess_def using assms

   618    Well_order_Restr Well_order_Restr ofilter_subset_embedS by blast

   619    hence False using * not_ordLess_ordLeq by blast

   620   }

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

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

   623 qed

   624

   625 lemma ofilter_subset_ordLess:

   626 assumes WELL: "Well_order r" and

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

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

   629 proof-

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

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

   632   using WELL Well_order_Restr by blast

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

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

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

   636   using assms ofilter_subset_ordLeq by blast

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

   638   using 1 not_ordLeq_iff_ordLess by blast

   639   finally show ?thesis .

   640 qed

   641

   642 lemma ofilter_ordLess:

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

   644 by (simp add: ofilter_subset_ordLess wo_rel.Field_ofilter

   645     wo_rel_def Restr_Field)

   646

   647 corollary underS_Restr_ordLess:

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

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

   650 proof-

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

   652   by (simp add: underS_Field3)

   653   thus ?thesis using assms

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

   655 qed

   656

   657 lemma embed_ordLess_ofilterIncl:

   658 assumes

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

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

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

   662 proof-

   663   have OL13: "r1 <o r3"

   664   using OL12 OL23 using ordLess_transitive by auto

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

   666   obtain f12 g23 where

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

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

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

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

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

   672   using EMB23 embed_unique[of r2 r3] by blast

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

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

   675   (*  *)

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

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

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

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

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

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

   682   (*  *)

   683   have "f12  ?A1 < ?A2"

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

   685   moreover have "inj_on f23 ?A2"

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

   687   ultimately

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

   689   moreover

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

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

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

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

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

   695   }

   696   ultimately

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

   698   (*  *)

   699   with 5 6 show ?thesis

   700   unfolding ofilterIncl_def by auto

   701 qed

   702

   703 lemma ordLess_iff_ordIso_Restr:

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

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

   706 proof(auto)

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

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

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

   710 next

   711   assume "r' <o r"

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

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

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

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

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

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

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

   719   using embed_implies_iso_Restr 2 assms by blast

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

   721   using WELL Well_order_Restr by blast

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

   723   using WELL' unfolding ordIso_def by auto

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

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

   726 qed

   727

   728 lemma internalize_ordLess:

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

   730 proof

   731   assume *: "r' <o r"

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

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

   734   using ordLess_iff_ordIso_Restr by blast

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

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

   737   by (simp add: wo_rel_def wo_rel.underS_ofilter)

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

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

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

   741   ultimately

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

   743 next

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

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

   746 qed

   747

   748 lemma internalize_ordLeq:

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

   750 proof

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

   752   moreover

   753   {assume "r' <o r"

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

   755    using internalize_ordLess[of r' r] by blast

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

   757    using ordLeq_iff_ordLess_or_ordIso by blast

   758   }

   759   moreover

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

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

   762   using ordLeq_iff_ordLess_or_ordIso by blast

   763 next

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

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

   766 qed

   767

   768 lemma ordLeq_iff_ordLess_Restr:

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

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

   771 proof(auto)

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

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

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

   775   using WELL underS_Restr_ordLess[of r] by blast

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

   777   using * ordLess_ordLeq_trans by blast

   778 next

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

   780   {assume "r' <o r"

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

   782    using assms ordLess_iff_ordIso_Restr by blast

   783    hence False using * not_ordLess_ordIso ordIso_symmetric by blast

   784   }

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

   786 qed

   787

   788 lemma finite_ordLess_infinite:

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

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

   791 shows "r <o r'"

   792 proof-

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

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

   795    unfolding ordLeq_def using assms embed_inj_on embed_Field by blast

   796    hence False using finite_imageD finite_subset FIN INF by blast

   797   }

   798   thus ?thesis using WELL WELL' ordLess_or_ordLeq by blast

   799 qed

   800

   801 lemma finite_well_order_on_ordIso:

   802 assumes FIN: "finite A" and

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

   804 shows "r =o r'"

   805 proof-

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

   807   using assms well_order_on_Well_order by blast

   808   moreover

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

   810                   \<longrightarrow> r =o r'"

   811   proof(clarify)

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

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

   814     using * ** well_order_on_Well_order by blast

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

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

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

   818     unfolding ordLeq_def using 2 embed_inj_on embed_Field by blast

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

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

   821   qed

   822   ultimately show ?thesis using assms ordLeq_total ordIso_symmetric by blast

   823 qed

   824

   825 subsection{* @{text "<o"} is well-founded *}

   826

   827 text {* Of course, it only makes sense to state that the @{text "<o"} is well-founded

   828 on the restricted type @{text "'a rel rel"}.  We prove this by first showing that, for any set

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

   830 in the set to an order filter of the fixed well-order is compatible w.r.t. to @{text "<o"} versus

   831 {\em strict inclusion}; and we already know that strict inclusion of order filters is well-founded. *}

   832

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

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

   835

   836 lemma ord_to_filter_compat:

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

   838         (ofilterIncl r0)

   839         (ord_to_filter r0)"

   840 proof(unfold compat_def ord_to_filter_def, clarify)

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

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

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

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

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

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

   847   by (auto simp add: ordLess_def embedS_def)

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

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

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

   851 qed

   852

   853 theorem wf_ordLess: "wf ordLess"

   854 proof-

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

   856    (* need to annotate here!*)

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

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

   859    {assume Case1: "Well_order r0"

   860     hence "wf ?R"

   861     using wf_ofilterIncl[of r0]

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

   863           ord_to_filter_compat[of r0] by auto

   864    }

   865    moreover

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

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

   868     hence "wf ?R" using wf_empty by simp

   869    }

   870    ultimately have "wf ?R" by blast

   871   }

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

   873 qed

   874

   875 corollary exists_minim_Well_order:

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

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

   878 proof-

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

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

   881     equals0I[of R] by blast

   882   with not_ordLeq_iff_ordLess WELL show ?thesis by blast

   883 qed

   884

   885

   886 subsection {* Copy via direct images *}

   887

   888 text{* The direct image operator is the dual of the inverse image operator @{text "inv_image"}

   889 from @{text "Relation.thy"}.  It is useful for transporting a well-order between

   890 different types. *}

   891

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

   893 where

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

   895

   896 lemma dir_image_Field:

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

   898 unfolding dir_image_def Field_def Range_def Domain_def by fast

   899

   900 lemma dir_image_minus_Id:

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

   902 unfolding inj_on_def Field_def dir_image_def by auto

   903

   904 lemma Refl_dir_image:

   905 assumes "Refl r"

   906 shows "Refl(dir_image r f)"

   907 proof-

   908   {fix a' b'

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

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

   911    unfolding dir_image_def by blast

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

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

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

   915    unfolding dir_image_def by auto

   916   }

   917   thus ?thesis

   918   by(unfold refl_on_def Field_def Domain_def Range_def, auto)

   919 qed

   920

   921 lemma trans_dir_image:

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

   923 shows "trans(dir_image r f)"

   924 proof(unfold trans_def, auto)

   925   fix a' b' c'

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

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

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

   929   unfolding dir_image_def by blast

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

   931   unfolding Field_def by auto

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

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

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

   935   unfolding dir_image_def using 1 by auto

   936 qed

   937

   938 lemma Preorder_dir_image:

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

   940 by (simp add: preorder_on_def Refl_dir_image trans_dir_image)

   941

   942 lemma antisym_dir_image:

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

   944 shows "antisym(dir_image r f)"

   945 proof(unfold antisym_def, auto)

   946   fix a' b'

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

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

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

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

   951   unfolding dir_image_def Field_def by blast

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

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

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

   955 qed

   956

   957 lemma Partial_order_dir_image:

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

   959 by (simp add: partial_order_on_def Preorder_dir_image antisym_dir_image)

   960

   961 lemma Total_dir_image:

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

   963 shows "Total(dir_image r f)"

   964 proof(unfold total_on_def, intro ballI impI)

   965   fix a' b'

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

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

   968     unfolding dir_image_Field[of r f] by blast

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

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

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

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

   973   using 1 unfolding dir_image_def by auto

   974 qed

   975

   976 lemma Linear_order_dir_image:

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

   978 by (simp add: linear_order_on_def Partial_order_dir_image Total_dir_image)

   979

   980 lemma wf_dir_image:

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

   982 shows "wf(dir_image r f)"

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

   984   fix A'::"'b set"

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

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

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

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

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

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

   991   proof(clarify)

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

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

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

   995     using ** unfolding dir_image_def Field_def by blast

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

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

   998     with 1 show False by auto

   999   qed

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

  1001   using A_def 1 by blast

  1002 qed

  1003

  1004 lemma Well_order_dir_image:

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

  1006 using assms unfolding well_order_on_def

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

  1008   dir_image_minus_Id[of f r]

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

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

  1011

  1012 lemma dir_image_bij_betw:

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

  1014 unfolding bij_betw_def by (simp add: dir_image_Field order_on_defs)

  1015

  1016 lemma dir_image_compat:

  1017 "compat r (dir_image r f) f"

  1018 unfolding compat_def dir_image_def by auto

  1019

  1020 lemma dir_image_iso:

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

  1022 using iso_iff3 dir_image_compat dir_image_bij_betw Well_order_dir_image by blast

  1023

  1024 lemma dir_image_ordIso:

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

  1026 unfolding ordIso_def using dir_image_iso Well_order_dir_image by blast

  1027

  1028 lemma Well_order_iso_copy:

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

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

  1031 proof-

  1032    let ?r' = "dir_image r f"

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

  1034    using WELL well_order_on_Well_order by blast

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

  1036    using dir_image_iso using BIJ unfolding bij_betw_def by auto

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

  1038    hence "Field ?r' = A'"

  1039    using 1 BIJ unfolding bij_betw_def by auto

  1040    moreover have "Well_order ?r'"

  1041    using 1 Well_order_dir_image BIJ unfolding bij_betw_def by blast

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

  1043 qed

  1044

  1045

  1046 subsection {* Bounded square *}

  1047

  1048 text{* This construction essentially defines, for an order relation @{text "r"}, a lexicographic

  1049 order @{text "bsqr r"} on @{text "(Field r) \<times> (Field r)"}, applying the

  1050 following criteria (in this order):

  1051 \begin{itemize}

  1052 \item compare the maximums;

  1053 \item compare the first components;

  1054 \item compare the second components.

  1055 \end{itemize}

  1056 %

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

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

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

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

  1061 in a product of proper filters on the original relation (assumed to be a well-order). *}

  1062

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

  1064 where

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

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

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

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

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

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

  1071            )}"

  1072

  1073 lemma Field_bsqr:

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

  1075 proof

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

  1077   proof-

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

  1079      moreover

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

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

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

  1083     }

  1084     thus ?thesis unfolding Field_def by force

  1085   qed

  1086 next

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

  1088   proof(auto)

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

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

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

  1092   qed

  1093 qed

  1094

  1095 lemma bsqr_Refl: "Refl(bsqr r)"

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

  1097

  1098 lemma bsqr_Trans:

  1099 assumes "Well_order r"

  1100 shows "trans (bsqr r)"

  1101 proof(unfold trans_def, auto)

  1102   (* Preliminary facts *)

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

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

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

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

  1107   (* Main proof *)

  1108   fix a1 a2 b1 b2 c1 c2

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

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

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

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

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

  1114   using * unfolding bsqr_def by auto

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

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

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

  1118   using ** unfolding bsqr_def by auto

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

  1120   proof-

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

  1122      hence ?thesis using ** by simp

  1123     }

  1124     moreover

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

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

  1127       hence ?thesis using * by simp

  1128      }

  1129      moreover

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

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

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

  1133       hence ?thesis using 0 unfolding bsqr_def by auto

  1134      }

  1135      moreover

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

  1137       hence ?thesis using Case2 0 unfolding bsqr_def by auto

  1138      }

  1139      ultimately have ?thesis using 0 2 by auto

  1140     }

  1141     moreover

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

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

  1144       hence ?thesis using * by simp

  1145      }

  1146      moreover

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

  1148       hence ?thesis using Case3 0 unfolding bsqr_def by auto

  1149      }

  1150      moreover

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

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

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

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

  1155      }

  1156      moreover

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

  1158       hence ?thesis using Case3 0 unfolding bsqr_def by auto

  1159      }

  1160      ultimately have ?thesis using 0 2 by auto

  1161     }

  1162     moreover

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

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

  1165       hence ?thesis using * by simp

  1166      }

  1167      moreover

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

  1169       hence ?thesis using Case4 0 unfolding bsqr_def by force

  1170      }

  1171      moreover

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

  1173       hence ?thesis using Case4 0 unfolding bsqr_def by auto

  1174      }

  1175      moreover

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

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

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

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

  1180      }

  1181      ultimately have ?thesis using 0 2 by auto

  1182     }

  1183     ultimately show ?thesis using 0 1 by auto

  1184   qed

  1185 qed

  1186

  1187 lemma bsqr_antisym:

  1188 assumes "Well_order r"

  1189 shows "antisym (bsqr r)"

  1190 proof(unfold antisym_def, clarify)

  1191   (* Preliminary facts *)

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

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

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

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

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

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

  1198   (* Main proof *)

  1199   fix a1 a2 b1 b2

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

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

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

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

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

  1205   using * unfolding bsqr_def by auto

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

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

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

  1209   using ** unfolding bsqr_def by auto

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

  1211   proof-

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

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

  1214       hence False using Case1 IrrS by blast

  1215      }

  1216      moreover

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

  1218       hence False using Case1 by auto

  1219      }

  1220      ultimately have ?thesis using 0 2 by auto

  1221     }

  1222     moreover

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

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

  1225        hence False using Case2 by auto

  1226      }

  1227      moreover

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

  1229       hence False using Case2 IrrS by blast

  1230      }

  1231      moreover

  1232      {assume Case23: "b1 = a1"

  1233       hence False using Case2 by auto

  1234      }

  1235      ultimately have ?thesis using 0 2 by auto

  1236     }

  1237     moreover

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

  1239      moreover

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

  1241       hence False using Case3 by auto

  1242      }

  1243      moreover

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

  1245       hence False using Case3 by auto

  1246      }

  1247      moreover

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

  1249       hence False using Case3 IrrS by blast

  1250      }

  1251      ultimately have ?thesis using 0 2 by auto

  1252     }

  1253     ultimately show ?thesis using 0 1 by blast

  1254   qed

  1255 qed

  1256

  1257 lemma bsqr_Total:

  1258 assumes "Well_order r"

  1259 shows "Total(bsqr r)"

  1260 proof-

  1261   (* Preliminary facts *)

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

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

  1264   using wo_rel.TOTALS by auto

  1265   (* Main proof *)

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

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

  1268    using Field_bsqr by blast

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

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

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

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

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

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

  1275      show ?thesis

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

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

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

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

  1280        show ?thesis

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

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

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

  1284        next

  1285          assume Case112: "a2 = b2"

  1286          show ?thesis

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

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

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

  1290          next

  1291            assume Case1122: "a1 = b1"

  1292            thus ?thesis using Case112 by auto

  1293          qed

  1294        qed

  1295      next

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

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

  1298        show ?thesis

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

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

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

  1302        next

  1303          assume Case122: "a2 = b1"

  1304          show ?thesis

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

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

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

  1308          next

  1309            assume Case1222: "a1 = b1"

  1310            show ?thesis

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

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

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

  1314            next

  1315              assume Case12222: "a2 = b2"

  1316              thus ?thesis using Case122 Case1222 by auto

  1317            qed

  1318          qed

  1319        qed

  1320      qed

  1321    next

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

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

  1324      show ?thesis

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

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

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

  1328        show ?thesis

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

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

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

  1332        next

  1333          assume Case212: "a1 = b2"

  1334          show ?thesis

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

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

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

  1338          next

  1339            assume Case2122: "a1 = b1"

  1340            show ?thesis

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

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

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

  1344            next

  1345              assume Case21222: "a2 = b2"

  1346              thus ?thesis using Case2122 Case212 by auto

  1347            qed

  1348          qed

  1349        qed

  1350      next

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

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

  1353        show ?thesis

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

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

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

  1357        next

  1358          assume Case222: "a1 = b1"

  1359          show ?thesis

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

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

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

  1363          next

  1364            assume Case2222: "a2 = b2"

  1365            thus ?thesis using Case222 by auto

  1366          qed

  1367        qed

  1368      qed

  1369    qed

  1370   }

  1371   thus ?thesis unfolding total_on_def by fast

  1372 qed

  1373

  1374 lemma bsqr_Linear_order:

  1375 assumes "Well_order r"

  1376 shows "Linear_order(bsqr r)"

  1377 unfolding order_on_defs

  1378 using assms bsqr_Refl bsqr_Trans bsqr_antisym bsqr_Total by blast

  1379

  1380 lemma bsqr_Well_order:

  1381 assumes "Well_order r"

  1382 shows "Well_order(bsqr r)"

  1383 using assms

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

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

  1386   using assms well_order_on_def Linear_order_Well_order_iff by blast

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

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

  1389   (*  *)

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

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

  1392   moreover

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

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

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

  1396   using 0 by blast

  1397   (*  *)

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

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

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

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

  1402   using 0 by blast

  1403   (*  *)

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

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

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

  1407   using m_min a1_min unfolding A1_def M_def by blast

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

  1409   using 0 by blast

  1410   (*   *)

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

  1412   using a1_min a2_min unfolding A1_def A2_def by auto

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

  1414   (*  *)

  1415   moreover

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

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

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

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

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

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

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

  1423      thus ?thesis unfolding bsqr_def using 4 5 by auto

  1424    next

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

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

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

  1428      show ?thesis

  1429      proof(cases "a1 = b1")

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

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

  1432      next

  1433        assume Case22: "a1 = b1"

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

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

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

  1437      qed

  1438    qed

  1439   }

  1440   (*  *)

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

  1442 qed

  1443

  1444 lemma bsqr_max2:

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

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

  1447 proof-

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

  1449   using LEQ unfolding Field_def by auto

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

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

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

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

  1454   using LEQ unfolding bsqr_def by auto

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

  1456 qed

  1457

  1458 lemma bsqr_ofilter:

  1459 assumes WELL: "Well_order r" and

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

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

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

  1463 proof-

  1464   let ?r' = "bsqr r"

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

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

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

  1468   using WELL bsqr_Well_order wo_rel_def by blast

  1469   (*  *)

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

  1471   with OF obtain a1 and a2 where

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

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

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

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

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

  1477   proof(unfold 1)

  1478     {fix b1 b2

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

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

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

  1482      unfolding underS_def by blast

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

  1484      moreover

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

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

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

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

  1489      }

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

  1491      using Trans trans_def[of r] by blast

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

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

  1494   qed

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

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

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

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

  1499   ultimately show ?thesis by blast

  1500 qed

  1501

  1502 definition Func where

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

  1504

  1505 lemma Func_empty:

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

  1507 unfolding Func_def by auto

  1508

  1509 lemma Func_elim:

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

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

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

  1513

  1514 definition curr where

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

  1516

  1517 lemma curr_in:

  1518 assumes f: "f \<in> Func (A <*> B) C"

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

  1520 using assms unfolding curr_def Func_def by auto

  1521

  1522 lemma curr_inj:

  1523 assumes "f1 \<in> Func (A <*> B) C" and "f2 \<in> Func (A <*> B) C"

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

  1525 proof safe

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

  1527   show "f1 = f2"

  1528   proof (rule ext, clarify)

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

  1530     proof (cases "(a,b) \<in> A <*> B")

  1531       case False

  1532       thus ?thesis using assms unfolding Func_def by auto

  1533     next

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

  1535       thus ?thesis

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

  1537     qed

  1538   qed

  1539 qed

  1540

  1541 lemma curr_surj:

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

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

  1544 proof

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

  1546   show "curr A ?f = g"

  1547   proof (rule ext)

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

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

  1550       case False

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

  1552       thus ?thesis unfolding curr_def using False by simp

  1553     next

  1554       case True

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

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

  1557       thus ?thesis using True unfolding Func_def curr_def by auto

  1558     qed

  1559   qed

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

  1561 qed

  1562

  1563 lemma bij_betw_curr:

  1564 "bij_betw (curr A) (Func (A <*> B) C) (Func A (Func B C))"

  1565 unfolding bij_betw_def inj_on_def image_def

  1566 apply (intro impI conjI ballI)

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

  1568 apply auto

  1569 apply (erule curr_in)

  1570 using curr_surj by blast

  1571

  1572 definition Func_map where

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

  1574

  1575 lemma Func_map:

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

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

  1578 using assms unfolding Func_def Func_map_def mem_Collect_eq by auto

  1579

  1580 lemma Func_non_emp:

  1581 assumes "B \<noteq> {}"

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

  1583 proof-

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

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

  1586   thus ?thesis by blast

  1587 qed

  1588

  1589 lemma Func_is_emp:

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

  1591 proof

  1592   assume L: ?L

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

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

  1595   ultimately show ?R by blast

  1596 next

  1597   assume R: ?R

  1598   moreover

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

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

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

  1602    with R have False by blast

  1603   }

  1604   thus ?L by blast

  1605 qed

  1606

  1607 lemma Func_map_surj:

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

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

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

  1611 proof(cases "B2 = {}")

  1612   case True

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

  1614 next

  1615   case False note B2 = False

  1616   show ?thesis

  1617   proof safe

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

  1619     def j1 \<equiv> "inv_into A1 f1"

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

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

  1622       by atomize_elim (rule bchoice)

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

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

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

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

  1627     } note kk = this

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

  1629     def j2 \<equiv> "\<lambda> a2. if a2 \<in> f2  B2 then k a2 else b22"

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

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

  1632     using kk unfolding j2_def by auto

  1633     def g \<equiv> "Func_map A2 j1 j2 h"

  1634     have "Func_map B2 f1 f2 g = h"

  1635     proof (rule ext)

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

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

  1638         case True

  1639         show ?thesis

  1640         proof (cases "h b2 = undefined")

  1641           case True

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

  1643           show ?thesis using A2 f_inv_into_f[OF b1]

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

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

  1646           auto intro: f_inv_into_f)

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

  1648     qed

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

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

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

  1652     unfolding Func_map_def[abs_def] by auto

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

  1654 qed

  1655

  1656 end