src/HOL/BNF_Wellorder_Constructions.thy
author haftmann
Mon Jun 05 15:59:41 2017 +0200 (2017-06-05)
changeset 66010 2f7d39285a1a
parent 63561 fba08009ff3e
child 67091 1393c2340eec
permissions -rw-r--r--
executable domain membership checks
     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