src/HOL/BNF_Wellorder_Constructions.thy
author blanchet
Mon Sep 01 16:34:39 2014 +0200 (2014-09-01)
changeset 58127 b7cab82f488e
parent 56191 src/HOL/BNF_Constructions_on_Wellorders.thy@159b0c88b4a4
child 58889 5b7a9633cfa8
permissions -rw-r--r--
renamed '(BNF_)Constructions_on_Wellorders' to '(BNF_)Wellorder_Constructions'
     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