src/HOL/BNF_Wellorder_Constructions.thy

prefer symbols for "abs";

(*  Title:      HOL/BNF_Wellorder_Constructions.thy
    Author:     Andrei Popescu, TU Muenchen
    Copyright   2012

Constructions on wellorders as needed by bounded natural functors.
*)

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

theory BNF_Wellorder_Constructions
imports BNF_Wellorder_Embedding
begin

text \<open>In this section, we study basic constructions on well-orders, such as restriction to
a set/order filter, copy via direct images, ordinal-like sum of disjoint well-orders,
and bounded square.  We also define between well-orders
the relations \<open>ordLeq\<close>, of being embedded (abbreviated \<open>\<le>o\<close>),
\<open>ordLess\<close>, of being strictly embedded (abbreviated \<open><o\<close>), and
\<open>ordIso\<close>, of being isomorphic (abbreviated \<open>=o\<close>).  We study the
connections between these relations, order filters, and the aforementioned constructions.
A main result of this section is that \<open><o\<close> is well-founded.\<close>


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

abbreviation Restr :: "'a rel \<Rightarrow> 'a set \<Rightarrow> 'a rel"
where "Restr r A \<equiv> r Int (A \<times> A)"

lemma Restr_subset:
"A \<le> B \<Longrightarrow> Restr (Restr r B) A = Restr r A"
by blast

lemma Restr_Field: "Restr r (Field r) = r"
unfolding Field_def by auto

lemma Refl_Restr: "Refl r \<Longrightarrow> Refl(Restr r A)"
unfolding refl_on_def Field_def by auto

lemma antisym_Restr:
"antisym r \<Longrightarrow> antisym(Restr r A)"
unfolding antisym_def Field_def by auto

lemma Total_Restr:
"Total r \<Longrightarrow> Total(Restr r A)"
unfolding total_on_def Field_def by auto

lemma trans_Restr:
"trans r \<Longrightarrow> trans(Restr r A)"
unfolding trans_def Field_def by blast

lemma Preorder_Restr:
"Preorder r \<Longrightarrow> Preorder(Restr r A)"
unfolding preorder_on_def by (simp add: Refl_Restr trans_Restr)

lemma Partial_order_Restr:
"Partial_order r \<Longrightarrow> Partial_order(Restr r A)"
unfolding partial_order_on_def by (simp add: Preorder_Restr antisym_Restr)

lemma Linear_order_Restr:
"Linear_order r \<Longrightarrow> Linear_order(Restr r A)"
unfolding linear_order_on_def by (simp add: Partial_order_Restr Total_Restr)

lemma Well_order_Restr:
assumes "Well_order r"
shows "Well_order(Restr r A)"
proof-
  have "Restr r A - Id \<le> r - Id" using Restr_subset by blast
  hence "wf(Restr r A - Id)" using assms
  using well_order_on_def wf_subset by blast
  thus ?thesis using assms unfolding well_order_on_def
  by (simp add: Linear_order_Restr)
qed

lemma Field_Restr_subset: "Field(Restr r A) \<le> A"
by (auto simp add: Field_def)

lemma Refl_Field_Restr:
"Refl r \<Longrightarrow> Field(Restr r A) = (Field r) Int A"
unfolding refl_on_def Field_def by blast

lemma Refl_Field_Restr2:
"\<lbrakk>Refl r; A \<le> Field r\<rbrakk> \<Longrightarrow> Field(Restr r A) = A"
by (auto simp add: Refl_Field_Restr)

lemma well_order_on_Restr:
assumes WELL: "Well_order r" and SUB: "A \<le> Field r"
shows "well_order_on A (Restr r A)"
using assms
using Well_order_Restr[of r A] Refl_Field_Restr2[of r A]
     order_on_defs[of "Field r" r] by auto


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

lemma Field_Restr_ofilter:
"\<lbrakk>Well_order r; wo_rel.ofilter r A\<rbrakk> \<Longrightarrow> Field(Restr r A) = A"
by (auto simp add: wo_rel_def wo_rel.ofilter_def wo_rel.REFL Refl_Field_Restr2)

lemma ofilter_Restr_under:
assumes WELL: "Well_order r" and OF: "wo_rel.ofilter r A" and IN: "a \<in> A"
shows "under (Restr r A) a = under r a"
using assms wo_rel_def
proof(auto simp add: wo_rel.ofilter_def under_def)
  fix b assume *: "a \<in> A" and "(b,a) \<in> r"
  hence "b \<in> under r a \<and> a \<in> Field r"
  unfolding under_def using Field_def by fastforce
  thus "b \<in> A" using * assms by (auto simp add: wo_rel_def wo_rel.ofilter_def)
qed

lemma ofilter_embed:
assumes "Well_order r"
shows "wo_rel.ofilter r A = (A \<le> Field r \<and> embed (Restr r A) r id)"
proof
  assume *: "wo_rel.ofilter r A"
  show "A \<le> Field r \<and> embed (Restr r A) r id"
  proof(unfold embed_def, auto)
    fix a assume "a \<in> A" thus "a \<in> Field r" using assms *
    by (auto simp add: wo_rel_def wo_rel.ofilter_def)
  next
    fix a assume "a \<in> Field (Restr r A)"
    thus "bij_betw id (under (Restr r A) a) (under r a)" using assms *
    by (simp add: ofilter_Restr_under Field_Restr_ofilter)
  qed
next
  assume *: "A \<le> Field r \<and> embed (Restr r A) r id"
  hence "Field(Restr r A) \<le> Field r"
  using assms  embed_Field[of "Restr r A" r id] id_def
        Well_order_Restr[of r] by auto
  {fix a assume "a \<in> A"
   hence "a \<in> Field(Restr r A)" using * assms
   by (simp add: order_on_defs Refl_Field_Restr2)
   hence "bij_betw id (under (Restr r A) a) (under r a)"
   using * unfolding embed_def by auto
   hence "under r a \<le> under (Restr r A) a"
   unfolding bij_betw_def by auto
   also have "\<dots> \<le> Field(Restr r A)" by (simp add: under_Field)
   also have "\<dots> \<le> A" by (simp add: Field_Restr_subset)
   finally have "under r a \<le> A" .
  }
  thus "wo_rel.ofilter r A" using assms * by (simp add: wo_rel_def wo_rel.ofilter_def)
qed

lemma ofilter_Restr_Int:
assumes WELL: "Well_order r" and OFA: "wo_rel.ofilter r A"
shows "wo_rel.ofilter (Restr r B) (A Int B)"
proof-
  let ?rB = "Restr r B"
  have Well: "wo_rel r" unfolding wo_rel_def using WELL .
  hence Refl: "Refl r" by (simp add: wo_rel.REFL)
  hence Field: "Field ?rB = Field r Int B"
  using Refl_Field_Restr by blast
  have WellB: "wo_rel ?rB \<and> Well_order ?rB" using WELL
  by (simp add: Well_order_Restr wo_rel_def)
  (* Main proof *)
  show ?thesis using WellB assms
  proof(auto simp add: wo_rel.ofilter_def under_def)
    fix a assume "a \<in> A" and *: "a \<in> B"
    hence "a \<in> Field r" using OFA Well by (auto simp add: wo_rel.ofilter_def)
    with * show "a \<in> Field ?rB" using Field by auto
  next
    fix a b assume "a \<in> A" and "(b,a) \<in> r"
    thus "b \<in> A" using Well OFA by (auto simp add: wo_rel.ofilter_def under_def)
  qed
qed

lemma ofilter_Restr_subset:
assumes WELL: "Well_order r" and OFA: "wo_rel.ofilter r A" and SUB: "A \<le> B"
shows "wo_rel.ofilter (Restr r B) A"
proof-
  have "A Int B = A" using SUB by blast
  thus ?thesis using assms ofilter_Restr_Int[of r A B] by auto
qed

lemma ofilter_subset_embed:
assumes WELL: "Well_order r" and
        OFA: "wo_rel.ofilter r A" and OFB: "wo_rel.ofilter r B"
shows "(A \<le> B) = (embed (Restr r A) (Restr r B) id)"
proof-
  let ?rA = "Restr r A"  let ?rB = "Restr r B"
  have Well: "wo_rel r" unfolding wo_rel_def using WELL .
  hence Refl: "Refl r" by (simp add: wo_rel.REFL)
  hence FieldA: "Field ?rA = Field r Int A"
  using Refl_Field_Restr by blast
  have FieldB: "Field ?rB = Field r Int B"
  using Refl Refl_Field_Restr by blast
  have WellA: "wo_rel ?rA \<and> Well_order ?rA" using WELL
  by (simp add: Well_order_Restr wo_rel_def)
  have WellB: "wo_rel ?rB \<and> Well_order ?rB" using WELL
  by (simp add: Well_order_Restr wo_rel_def)
  (* Main proof *)
  show ?thesis
  proof
    assume *: "A \<le> B"
    hence "wo_rel.ofilter (Restr r B) A" using assms
    by (simp add: ofilter_Restr_subset)
    hence "embed (Restr ?rB A) (Restr r B) id"
    using WellB ofilter_embed[of "?rB" A] by auto
    thus "embed (Restr r A) (Restr r B) id"
    using * by (simp add: Restr_subset)
  next
    assume *: "embed (Restr r A) (Restr r B) id"
    {fix a assume **: "a \<in> A"
     hence "a \<in> Field r" using Well OFA by (auto simp add: wo_rel.ofilter_def)
     with ** FieldA have "a \<in> Field ?rA" by auto
     hence "a \<in> Field ?rB" using * WellA embed_Field[of ?rA ?rB id] by auto
     hence "a \<in> B" using FieldB by auto
    }
    thus "A \<le> B" by blast
  qed
qed

lemma ofilter_subset_embedS_iso:
assumes WELL: "Well_order r" and
        OFA: "wo_rel.ofilter r A" and OFB: "wo_rel.ofilter r B"
shows "((A < B) = (embedS (Restr r A) (Restr r B) id)) \<and>
       ((A = B) = (iso (Restr r A) (Restr r B) id))"
proof-
  let ?rA = "Restr r A"  let ?rB = "Restr r B"
  have Well: "wo_rel r" unfolding wo_rel_def using WELL .
  hence Refl: "Refl r" by (simp add: wo_rel.REFL)
  hence "Field ?rA = Field r Int A"
  using Refl_Field_Restr by blast
  hence FieldA: "Field ?rA = A" using OFA Well
  by (auto simp add: wo_rel.ofilter_def)
  have "Field ?rB = Field r Int B"
  using Refl Refl_Field_Restr by blast
  hence FieldB: "Field ?rB = B" using OFB Well
  by (auto simp add: wo_rel.ofilter_def)
  (* Main proof *)
  show ?thesis unfolding embedS_def iso_def
  using assms ofilter_subset_embed[of r A B]
        FieldA FieldB bij_betw_id_iff[of A B] by auto
qed

lemma ofilter_subset_embedS:
assumes WELL: "Well_order r" and
        OFA: "wo_rel.ofilter r A" and OFB: "wo_rel.ofilter r B"
shows "(A < B) = embedS (Restr r A) (Restr r B) id"
using assms by (simp add: ofilter_subset_embedS_iso)

lemma embed_implies_iso_Restr:
assumes WELL: "Well_order r" and WELL': "Well_order r'" and
        EMB: "embed r' r f"
shows "iso r' (Restr r (f ` (Field r'))) f"
proof-
  let ?A' = "Field r'"
  let ?r'' = "Restr r (f ` ?A')"
  have 0: "Well_order ?r''" using WELL Well_order_Restr by blast
  have 1: "wo_rel.ofilter r (f ` ?A')" using assms embed_Field_ofilter  by blast
  hence "Field ?r'' = f ` (Field r')" using WELL Field_Restr_ofilter by blast
  hence "bij_betw f ?A' (Field ?r'')"
  using EMB embed_inj_on WELL' unfolding bij_betw_def by blast
  moreover
  {have "\<forall>a b. (a,b) \<in> r' \<longrightarrow> a \<in> Field r' \<and> b \<in> Field r'"
   unfolding Field_def by auto
   hence "compat r' ?r'' f"
   using assms embed_iff_compat_inj_on_ofilter
   unfolding compat_def by blast
  }
  ultimately show ?thesis using WELL' 0 iso_iff3 by blast
qed


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

definition ofilterIncl :: "'a rel \<Rightarrow> 'a set rel"
where
"ofilterIncl r \<equiv> {(A,B). wo_rel.ofilter r A \<and> A \<noteq> Field r \<and>
                         wo_rel.ofilter r B \<and> B \<noteq> Field r \<and> A < B}"

lemma wf_ofilterIncl:
assumes WELL: "Well_order r"
shows "wf(ofilterIncl r)"
proof-
  have Well: "wo_rel r" using WELL by (simp add: wo_rel_def)
  hence Lo: "Linear_order r" by (simp add: wo_rel.LIN)
  let ?h = "(\<lambda> A. wo_rel.suc r A)"
  let ?rS = "r - Id"
  have "wf ?rS" using WELL by (simp add: order_on_defs)
  moreover
  have "compat (ofilterIncl r) ?rS ?h"
  proof(unfold compat_def ofilterIncl_def,
        intro allI impI, simp, elim conjE)
    fix A B
    assume *: "wo_rel.ofilter r A" "A \<noteq> Field r" and
           **: "wo_rel.ofilter r B" "B \<noteq> Field r" and ***: "A < B"
    then obtain a and b where 0: "a \<in> Field r \<and> b \<in> Field r" and
                         1: "A = underS r a \<and> B = underS r b"
    using Well by (auto simp add: wo_rel.ofilter_underS_Field)
    hence "a \<noteq> b" using *** by auto
    moreover
    have "(a,b) \<in> r" using 0 1 Lo ***
    by (auto simp add: underS_incl_iff)
    moreover
    have "a = wo_rel.suc r A \<and> b = wo_rel.suc r B"
    using Well 0 1 by (simp add: wo_rel.suc_underS)
    ultimately
    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"
    by simp
  qed
  ultimately show "wf (ofilterIncl r)" by (simp add: compat_wf)
qed


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

text \<open>We define three relations between well-orders:
\begin{itemize}
\item \<open>ordLeq\<close>, of being embedded (abbreviated \<open>\<le>o\<close>);
\item \<open>ordLess\<close>, of being strictly embedded (abbreviated \<open><o\<close>);
\item \<open>ordIso\<close>, of being isomorphic (abbreviated \<open>=o\<close>).
\end{itemize}
%
The prefix "ord" and the index "o" in these names stand for "ordinal-like".
These relations shall be proved to be inter-connected in a similar fashion as the trio
\<open>\<le>\<close>, \<open><\<close>, \<open>=\<close> associated to a total order on a set.
\<close>

definition ordLeq :: "('a rel * 'a' rel) set"
where
"ordLeq = {(r,r'). Well_order r \<and> Well_order r' \<and> (\<exists>f. embed r r' f)}"

abbreviation ordLeq2 :: "'a rel \<Rightarrow> 'a' rel \<Rightarrow> bool" (infix "<=o" 50)
where "r <=o r' \<equiv> (r,r') \<in> ordLeq"

abbreviation ordLeq3 :: "'a rel \<Rightarrow> 'a' rel \<Rightarrow> bool" (infix "\<le>o" 50)
where "r \<le>o r' \<equiv> r <=o r'"

definition ordLess :: "('a rel * 'a' rel) set"
where
"ordLess = {(r,r'). Well_order r \<and> Well_order r' \<and> (\<exists>f. embedS r r' f)}"

abbreviation ordLess2 :: "'a rel \<Rightarrow> 'a' rel \<Rightarrow> bool" (infix "<o" 50)
where "r <o r' \<equiv> (r,r') \<in> ordLess"

definition ordIso :: "('a rel * 'a' rel) set"
where
"ordIso = {(r,r'). Well_order r \<and> Well_order r' \<and> (\<exists>f. iso r r' f)}"

abbreviation ordIso2 :: "'a rel \<Rightarrow> 'a' rel \<Rightarrow> bool" (infix "=o" 50)
where "r =o r' \<equiv> (r,r') \<in> ordIso"

lemmas ordRels_def = ordLeq_def ordLess_def ordIso_def

lemma ordLeq_Well_order_simp:
assumes "r \<le>o r'"
shows "Well_order r \<and> Well_order r'"
using assms unfolding ordLeq_def by simp

text\<open>Notice that the relations \<open>\<le>o\<close>, \<open><o\<close>, \<open>=o\<close> connect well-orders
on potentially {\em distinct} types. However, some of the lemmas below, including the next one,
restrict implicitly the type of these relations to \<open>(('a rel) * ('a rel)) set\<close> , i.e.,
to \<open>'a rel rel\<close>.\<close>

lemma ordLeq_reflexive:
"Well_order r \<Longrightarrow> r \<le>o r"
unfolding ordLeq_def using id_embed[of r] by blast

lemma ordLeq_transitive[trans]:
assumes *: "r \<le>o r'" and **: "r' \<le>o r''"
shows "r \<le>o r''"
proof-
  obtain f and f'
  where 1: "Well_order r \<and> Well_order r' \<and> Well_order r''" and
        "embed r r' f" and "embed r' r'' f'"
  using * ** unfolding ordLeq_def by blast
  hence "embed r r'' (f' o f)"
  using comp_embed[of r r' f r'' f'] by auto
  thus "r \<le>o r''" unfolding ordLeq_def using 1 by auto
qed

lemma ordLeq_total:
"\<lbrakk>Well_order r; Well_order r'\<rbrakk> \<Longrightarrow> r \<le>o r' \<or> r' \<le>o r"
unfolding ordLeq_def using wellorders_totally_ordered by blast

lemma ordIso_reflexive:
"Well_order r \<Longrightarrow> r =o r"
unfolding ordIso_def using id_iso[of r] by blast

lemma ordIso_transitive[trans]:
assumes *: "r =o r'" and **: "r' =o r''"
shows "r =o r''"
proof-
  obtain f and f'
  where 1: "Well_order r \<and> Well_order r' \<and> Well_order r''" and
        "iso r r' f" and 3: "iso r' r'' f'"
  using * ** unfolding ordIso_def by auto
  hence "iso r r'' (f' o f)"
  using comp_iso[of r r' f r'' f'] by auto
  thus "r =o r''" unfolding ordIso_def using 1 by auto
qed

lemma ordIso_symmetric:
assumes *: "r =o r'"
shows "r' =o r"
proof-
  obtain f where 1: "Well_order r \<and> Well_order r'" and
                 2: "embed r r' f \<and> bij_betw f (Field r) (Field r')"
  using * by (auto simp add: ordIso_def iso_def)
  let ?f' = "inv_into (Field r) f"
  have "embed r' r ?f' \<and> bij_betw ?f' (Field r') (Field r)"
  using 1 2 by (simp add: bij_betw_inv_into inv_into_Field_embed_bij_betw)
  thus "r' =o r" unfolding ordIso_def using 1 by (auto simp add: iso_def)
qed

lemma ordLeq_ordLess_trans[trans]:
assumes "r \<le>o r'" and " r' <o r''"
shows "r <o r''"
proof-
  have "Well_order r \<and> Well_order r''"
  using assms unfolding ordLeq_def ordLess_def by auto
  thus ?thesis using assms unfolding ordLeq_def ordLess_def
  using embed_comp_embedS by blast
qed

lemma ordLess_ordLeq_trans[trans]:
assumes "r <o r'" and " r' \<le>o r''"
shows "r <o r''"
proof-
  have "Well_order r \<and> Well_order r''"
  using assms unfolding ordLeq_def ordLess_def by auto
  thus ?thesis using assms unfolding ordLeq_def ordLess_def
  using embedS_comp_embed by blast
qed

lemma ordLeq_ordIso_trans[trans]:
assumes "r \<le>o r'" and " r' =o r''"
shows "r \<le>o r''"
proof-
  have "Well_order r \<and> Well_order r''"
  using assms unfolding ordLeq_def ordIso_def by auto
  thus ?thesis using assms unfolding ordLeq_def ordIso_def
  using embed_comp_iso by blast
qed

lemma ordIso_ordLeq_trans[trans]:
assumes "r =o r'" and " r' \<le>o r''"
shows "r \<le>o r''"
proof-
  have "Well_order r \<and> Well_order r''"
  using assms unfolding ordLeq_def ordIso_def by auto
  thus ?thesis using assms unfolding ordLeq_def ordIso_def
  using iso_comp_embed by blast
qed

lemma ordLess_ordIso_trans[trans]:
assumes "r <o r'" and " r' =o r''"
shows "r <o r''"
proof-
  have "Well_order r \<and> Well_order r''"
  using assms unfolding ordLess_def ordIso_def by auto
  thus ?thesis using assms unfolding ordLess_def ordIso_def
  using embedS_comp_iso by blast
qed

lemma ordIso_ordLess_trans[trans]:
assumes "r =o r'" and " r' <o r''"
shows "r <o r''"
proof-
  have "Well_order r \<and> Well_order r''"
  using assms unfolding ordLess_def ordIso_def by auto
  thus ?thesis using assms unfolding ordLess_def ordIso_def
  using iso_comp_embedS by blast
qed

lemma ordLess_not_embed:
assumes "r <o r'"
shows "\<not>(\<exists>f'. embed r' r f')"
proof-
  obtain f where 1: "Well_order r \<and> Well_order r'" and 2: "embed r r' f" and
                 3: " \<not> bij_betw f (Field r) (Field r')"
  using assms unfolding ordLess_def by (auto simp add: embedS_def)
  {fix f' assume *: "embed r' r f'"
   hence "bij_betw f (Field r) (Field r')" using 1 2
   by (simp add: embed_bothWays_Field_bij_betw)
   with 3 have False by contradiction
  }
  thus ?thesis by blast
qed

lemma ordLess_Field:
assumes OL: "r1 <o r2" and EMB: "embed r1 r2 f"
shows "\<not> (f`(Field r1) = Field r2)"
proof-
  let ?A1 = "Field r1"  let ?A2 = "Field r2"
  obtain g where
  0: "Well_order r1 \<and> Well_order r2" and
  1: "embed r1 r2 g \<and> \<not>(bij_betw g ?A1 ?A2)"
  using OL unfolding ordLess_def by (auto simp add: embedS_def)
  hence "\<forall>a \<in> ?A1. f a = g a"
  using 0 EMB embed_unique[of r1] by auto
  hence "\<not>(bij_betw f ?A1 ?A2)"
  using 1 bij_betw_cong[of ?A1] by blast
  moreover
  have "inj_on f ?A1" using EMB 0 by (simp add: embed_inj_on)
  ultimately show ?thesis by (simp add: bij_betw_def)
qed

lemma ordLess_iff:
"r <o r' = (Well_order r \<and> Well_order r' \<and> \<not>(\<exists>f'. embed r' r f'))"
proof
  assume *: "r <o r'"
  hence "\<not>(\<exists>f'. embed r' r f')" using ordLess_not_embed[of r r'] by simp
  with * show "Well_order r \<and> Well_order r' \<and> \<not> (\<exists>f'. embed r' r f')"
  unfolding ordLess_def by auto
next
  assume *: "Well_order r \<and> Well_order r' \<and> \<not> (\<exists>f'. embed r' r f')"
  then obtain f where 1: "embed r r' f"
  using wellorders_totally_ordered[of r r'] by blast
  moreover
  {assume "bij_betw f (Field r) (Field r')"
   with * 1 have "embed r' r (inv_into (Field r) f) "
   using inv_into_Field_embed_bij_betw[of r r' f] by auto
   with * have False by blast
  }
  ultimately show "(r,r') \<in> ordLess"
  unfolding ordLess_def using * by (fastforce simp add: embedS_def)
qed

lemma ordLess_irreflexive: "\<not> r <o r"
proof
  assume "r <o r"
  hence "Well_order r \<and>  \<not>(\<exists>f. embed r r f)"
  unfolding ordLess_iff ..
  moreover have "embed r r id" using id_embed[of r] .
  ultimately show False by blast
qed

lemma ordLeq_iff_ordLess_or_ordIso:
"r \<le>o r' = (r <o r' \<or> r =o r')"
unfolding ordRels_def embedS_defs iso_defs by blast

lemma ordIso_iff_ordLeq:
"(r =o r') = (r \<le>o r' \<and> r' \<le>o r)"
proof
  assume "r =o r'"
  then obtain f where 1: "Well_order r \<and> Well_order r' \<and>
                     embed r r' f \<and> bij_betw f (Field r) (Field r')"
  unfolding ordIso_def iso_defs by auto
  hence "embed r r' f \<and> embed r' r (inv_into (Field r) f)"
  by (simp add: inv_into_Field_embed_bij_betw)
  thus  "r \<le>o r' \<and> r' \<le>o r"
  unfolding ordLeq_def using 1 by auto
next
  assume "r \<le>o r' \<and> r' \<le>o r"
  then obtain f and g where 1: "Well_order r \<and> Well_order r' \<and>
                           embed r r' f \<and> embed r' r g"
  unfolding ordLeq_def by auto
  hence "iso r r' f" by (auto simp add: embed_bothWays_iso)
  thus "r =o r'" unfolding ordIso_def using 1 by auto
qed

lemma not_ordLess_ordLeq:
"r <o r' \<Longrightarrow> \<not> r' \<le>o r"
using ordLess_ordLeq_trans ordLess_irreflexive by blast

lemma ordLess_or_ordLeq:
assumes WELL: "Well_order r" and WELL': "Well_order r'"
shows "r <o r' \<or> r' \<le>o r"
proof-
  have "r \<le>o r' \<or> r' \<le>o r"
  using assms by (simp add: ordLeq_total)
  moreover
  {assume "\<not> r <o r' \<and> r \<le>o r'"
   hence "r =o r'" using ordLeq_iff_ordLess_or_ordIso by blast
   hence "r' \<le>o r" using ordIso_symmetric ordIso_iff_ordLeq by blast
  }
  ultimately show ?thesis by blast
qed

lemma not_ordLess_ordIso:
"r <o r' \<Longrightarrow> \<not> r =o r'"
using assms ordLess_ordIso_trans ordIso_symmetric ordLess_irreflexive by blast

lemma not_ordLeq_iff_ordLess:
assumes WELL: "Well_order r" and WELL': "Well_order r'"
shows "(\<not> r' \<le>o r) = (r <o r')"
using assms not_ordLess_ordLeq ordLess_or_ordLeq by blast

lemma not_ordLess_iff_ordLeq:
assumes WELL: "Well_order r" and WELL': "Well_order r'"
shows "(\<not> r' <o r) = (r \<le>o r')"
using assms not_ordLess_ordLeq ordLess_or_ordLeq by blast

lemma ordLess_transitive[trans]:
"\<lbrakk>r <o r'; r' <o r''\<rbrakk> \<Longrightarrow> r <o r''"
using assms ordLess_ordLeq_trans ordLeq_iff_ordLess_or_ordIso by blast

corollary ordLess_trans: "trans ordLess"
unfolding trans_def using ordLess_transitive by blast

lemmas ordIso_equivalence = ordIso_transitive ordIso_reflexive ordIso_symmetric

lemma ordIso_imp_ordLeq:
"r =o r' \<Longrightarrow> r \<le>o r'"
using ordIso_iff_ordLeq by blast

lemma ordLess_imp_ordLeq:
"r <o r' \<Longrightarrow> r \<le>o r'"
using ordLeq_iff_ordLess_or_ordIso by blast

lemma ofilter_subset_ordLeq:
assumes WELL: "Well_order r" and
        OFA: "wo_rel.ofilter r A" and OFB: "wo_rel.ofilter r B"
shows "(A \<le> B) = (Restr r A \<le>o Restr r B)"
proof
  assume "A \<le> B"
  thus "Restr r A \<le>o Restr r B"
  unfolding ordLeq_def using assms
  Well_order_Restr Well_order_Restr ofilter_subset_embed by blast
next
  assume *: "Restr r A \<le>o Restr r B"
  then obtain f where "embed (Restr r A) (Restr r B) f"
  unfolding ordLeq_def by blast
  {assume "B < A"
   hence "Restr r B <o Restr r A"
   unfolding ordLess_def using assms
   Well_order_Restr Well_order_Restr ofilter_subset_embedS by blast
   hence False using * not_ordLess_ordLeq by blast
  }
  thus "A \<le> B" using OFA OFB WELL
  wo_rel_def[of r] wo_rel.ofilter_linord[of r A B] by blast
qed

lemma ofilter_subset_ordLess:
assumes WELL: "Well_order r" and
        OFA: "wo_rel.ofilter r A" and OFB: "wo_rel.ofilter r B"
shows "(A < B) = (Restr r A <o Restr r B)"
proof-
  let ?rA = "Restr r A" let ?rB = "Restr r B"
  have 1: "Well_order ?rA \<and> Well_order ?rB"
  using WELL Well_order_Restr by blast
  have "(A < B) = (\<not> B \<le> A)" using assms
  wo_rel_def wo_rel.ofilter_linord[of r A B] by blast
  also have "\<dots> = (\<not> Restr r B \<le>o Restr r A)"
  using assms ofilter_subset_ordLeq by blast
  also have "\<dots> = (Restr r A <o Restr r B)"
  using 1 not_ordLeq_iff_ordLess by blast
  finally show ?thesis .
qed

lemma ofilter_ordLess:
"\<lbrakk>Well_order r; wo_rel.ofilter r A\<rbrakk> \<Longrightarrow> (A < Field r) = (Restr r A <o r)"
by (simp add: ofilter_subset_ordLess wo_rel.Field_ofilter
    wo_rel_def Restr_Field)

corollary underS_Restr_ordLess:
assumes "Well_order r" and "Field r \<noteq> {}"
shows "Restr r (underS r a) <o r"
proof-
  have "underS r a < Field r" using assms
  by (simp add: underS_Field3)
  thus ?thesis using assms
  by (simp add: ofilter_ordLess wo_rel.underS_ofilter wo_rel_def)
qed

lemma embed_ordLess_ofilterIncl:
assumes
  OL12: "r1 <o r2" and OL23: "r2 <o r3" and
  EMB13: "embed r1 r3 f13" and EMB23: "embed r2 r3 f23"
shows "(f13`(Field r1), f23`(Field r2)) \<in> (ofilterIncl r3)"
proof-
  have OL13: "r1 <o r3"
  using OL12 OL23 using ordLess_transitive by auto
  let ?A1 = "Field r1"  let ?A2 ="Field r2" let ?A3 ="Field r3"
  obtain f12 g23 where
  0: "Well_order r1 \<and> Well_order r2 \<and> Well_order r3" and
  1: "embed r1 r2 f12 \<and> \<not>(bij_betw f12 ?A1 ?A2)" and
  2: "embed r2 r3 g23 \<and> \<not>(bij_betw g23 ?A2 ?A3)"
  using OL12 OL23 by (auto simp add: ordLess_def embedS_def)
  hence "\<forall>a \<in> ?A2. f23 a = g23 a"
  using EMB23 embed_unique[of r2 r3] by blast
  hence 3: "\<not>(bij_betw f23 ?A2 ?A3)"
  using 2 bij_betw_cong[of ?A2 f23 g23] by blast
  (*  *)
  have 4: "wo_rel.ofilter r2 (f12 ` ?A1) \<and> f12 ` ?A1 \<noteq> ?A2"
  using 0 1 OL12 by (simp add: embed_Field_ofilter ordLess_Field)
  have 5: "wo_rel.ofilter r3 (f23 ` ?A2) \<and> f23 ` ?A2 \<noteq> ?A3"
  using 0 EMB23 OL23 by (simp add: embed_Field_ofilter ordLess_Field)
  have 6: "wo_rel.ofilter r3 (f13 ` ?A1)  \<and> f13 ` ?A1 \<noteq> ?A3"
  using 0 EMB13 OL13 by (simp add: embed_Field_ofilter ordLess_Field)
  (*  *)
  have "f12 ` ?A1 < ?A2"
  using 0 4 by (auto simp add: wo_rel_def wo_rel.ofilter_def)
  moreover have "inj_on f23 ?A2"
  using EMB23 0 by (simp add: wo_rel_def embed_inj_on)
  ultimately
  have "f23 ` (f12 ` ?A1) < f23 ` ?A2" by (simp add: inj_on_strict_subset)
  moreover
  {have "embed r1 r3 (f23 o f12)"
   using 1 EMB23 0 by (auto simp add: comp_embed)
   hence "\<forall>a \<in> ?A1. f23(f12 a) = f13 a"
   using EMB13 0 embed_unique[of r1 r3 "f23 o f12" f13] by auto
   hence "f23 ` (f12 ` ?A1) = f13 ` ?A1" by force
  }
  ultimately
  have "f13 ` ?A1 < f23 ` ?A2" by simp
  (*  *)
  with 5 6 show ?thesis
  unfolding ofilterIncl_def by auto
qed

lemma ordLess_iff_ordIso_Restr:
assumes WELL: "Well_order r" and WELL': "Well_order r'"
shows "(r' <o r) = (\<exists>a \<in> Field r. r' =o Restr r (underS r a))"
proof(auto)
  fix a assume *: "a \<in> Field r" and **: "r' =o Restr r (underS r a)"
  hence "Restr r (underS r a) <o r" using WELL underS_Restr_ordLess[of r] by blast
  thus "r' <o r" using ** ordIso_ordLess_trans by blast
next
  assume "r' <o r"
  then obtain f where 1: "Well_order r \<and> Well_order r'" and
                      2: "embed r' r f \<and> f ` (Field r') \<noteq> Field r"
  unfolding ordLess_def embedS_def[abs_def] bij_betw_def using embed_inj_on by blast
  hence "wo_rel.ofilter r (f ` (Field r'))" using embed_Field_ofilter by blast
  then obtain a where 3: "a \<in> Field r" and 4: "underS r a = f ` (Field r')"
  using 1 2 by (auto simp add: wo_rel.ofilter_underS_Field wo_rel_def)
  have "iso r' (Restr r (f ` (Field r'))) f"
  using embed_implies_iso_Restr 2 assms by blast
  moreover have "Well_order (Restr r (f ` (Field r')))"
  using WELL Well_order_Restr by blast
  ultimately have "r' =o Restr r (f ` (Field r'))"
  using WELL' unfolding ordIso_def by auto
  hence "r' =o Restr r (underS r a)" using 4 by auto
  thus "\<exists>a \<in> Field r. r' =o Restr r (underS r a)" using 3 by auto
qed

lemma internalize_ordLess:
"(r' <o r) = (\<exists>p. Field p < Field r \<and> r' =o p \<and> p <o r)"
proof
  assume *: "r' <o r"
  hence 0: "Well_order r \<and> Well_order r'" unfolding ordLess_def by auto
  with * obtain a where 1: "a \<in> Field r" and 2: "r' =o Restr r (underS r a)"
  using ordLess_iff_ordIso_Restr by blast
  let ?p = "Restr r (underS r a)"
  have "wo_rel.ofilter r (underS r a)" using 0
  by (simp add: wo_rel_def wo_rel.underS_ofilter)
  hence "Field ?p = underS r a" using 0 Field_Restr_ofilter by blast
  hence "Field ?p < Field r" using underS_Field2 1 by fast
  moreover have "?p <o r" using underS_Restr_ordLess[of r a] 0 1 by blast
  ultimately
  show "\<exists>p. Field p < Field r \<and> r' =o p \<and> p <o r" using 2 by blast
next
  assume "\<exists>p. Field p < Field r \<and> r' =o p \<and> p <o r"
  thus "r' <o r" using ordIso_ordLess_trans by blast
qed

lemma internalize_ordLeq:
"(r' \<le>o r) = (\<exists>p. Field p \<le> Field r \<and> r' =o p \<and> p \<le>o r)"
proof
  assume *: "r' \<le>o r"
  moreover
  {assume "r' <o r"
   then obtain p where "Field p < Field r \<and> r' =o p \<and> p <o r"
   using internalize_ordLess[of r' r] by blast
   hence "\<exists>p. Field p \<le> Field r \<and> r' =o p \<and> p \<le>o r"
   using ordLeq_iff_ordLess_or_ordIso by blast
  }
  moreover
  have "r \<le>o r" using * ordLeq_def ordLeq_reflexive by blast
  ultimately show "\<exists>p. Field p \<le> Field r \<and> r' =o p \<and> p \<le>o r"
  using ordLeq_iff_ordLess_or_ordIso by blast
next
  assume "\<exists>p. Field p \<le> Field r \<and> r' =o p \<and> p \<le>o r"
  thus "r' \<le>o r" using ordIso_ordLeq_trans by blast
qed

lemma ordLeq_iff_ordLess_Restr:
assumes WELL: "Well_order r" and WELL': "Well_order r'"
shows "(r \<le>o r') = (\<forall>a \<in> Field r. Restr r (underS r a) <o r')"
proof(auto)
  assume *: "r \<le>o r'"
  fix a assume "a \<in> Field r"
  hence "Restr r (underS r a) <o r"
  using WELL underS_Restr_ordLess[of r] by blast
  thus "Restr r (underS r a) <o r'"
  using * ordLess_ordLeq_trans by blast
next
  assume *: "\<forall>a \<in> Field r. Restr r (underS r a) <o r'"
  {assume "r' <o r"
   then obtain a where "a \<in> Field r \<and> r' =o Restr r (underS r a)"
   using assms ordLess_iff_ordIso_Restr by blast
   hence False using * not_ordLess_ordIso ordIso_symmetric by blast
  }
  thus "r \<le>o r'" using ordLess_or_ordLeq assms by blast
qed

lemma finite_ordLess_infinite:
assumes WELL: "Well_order r" and WELL': "Well_order r'" and
        FIN: "finite(Field r)" and INF: "\<not>finite(Field r')"
shows "r <o r'"
proof-
  {assume "r' \<le>o r"
   then obtain h where "inj_on h (Field r') \<and> h ` (Field r') \<le> Field r"
   unfolding ordLeq_def using assms embed_inj_on embed_Field by blast
   hence False using finite_imageD finite_subset FIN INF by blast
  }
  thus ?thesis using WELL WELL' ordLess_or_ordLeq by blast
qed

lemma finite_well_order_on_ordIso:
assumes FIN: "finite A" and
        WELL: "well_order_on A r" and WELL': "well_order_on A r'"
shows "r =o r'"
proof-
  have 0: "Well_order r \<and> Well_order r' \<and> Field r = A \<and> Field r' = A"
  using assms well_order_on_Well_order by blast
  moreover
  have "\<forall>r r'. well_order_on A r \<and> well_order_on A r' \<and> r \<le>o r'
                  \<longrightarrow> r =o r'"
  proof(clarify)
    fix r r' assume *: "well_order_on A r" and **: "well_order_on A r'"
    have 2: "Well_order r \<and> Well_order r' \<and> Field r = A \<and> Field r' = A"
    using * ** well_order_on_Well_order by blast
    assume "r \<le>o r'"
    then obtain f where 1: "embed r r' f" and
                        "inj_on f A \<and> f ` A \<le> A"
    unfolding ordLeq_def using 2 embed_inj_on embed_Field by blast
    hence "bij_betw f A A" unfolding bij_betw_def using FIN endo_inj_surj by blast
    thus "r =o r'" unfolding ordIso_def iso_def[abs_def] using 1 2 by auto
  qed
  ultimately show ?thesis using assms ordLeq_total ordIso_symmetric by blast
qed

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

text \<open>Of course, it only makes sense to state that the \<open><o\<close> is well-founded
on the restricted type \<open>'a rel rel\<close>.  We prove this by first showing that, for any set
of well-orders all embedded in a fixed well-order, the function mapping each well-order
in the set to an order filter of the fixed well-order is compatible w.r.t. to \<open><o\<close> versus
{\em strict inclusion}; and we already know that strict inclusion of order filters is well-founded.\<close>

definition ord_to_filter :: "'a rel \<Rightarrow> 'a rel \<Rightarrow> 'a set"
where "ord_to_filter r0 r \<equiv> (SOME f. embed r r0 f) ` (Field r)"

lemma ord_to_filter_compat:
"compat (ordLess Int (ordLess^-1``{r0} \<times> ordLess^-1``{r0}))
        (ofilterIncl r0)
        (ord_to_filter r0)"
proof(unfold compat_def ord_to_filter_def, clarify)
  fix r1::"'a rel" and r2::"'a rel"
  let ?A1 = "Field r1"  let ?A2 ="Field r2" let ?A0 ="Field r0"
  let ?phi10 = "\<lambda> f10. embed r1 r0 f10" let ?f10 = "SOME f. ?phi10 f"
  let ?phi20 = "\<lambda> f20. embed r2 r0 f20" let ?f20 = "SOME f. ?phi20 f"
  assume *: "r1 <o r0" "r2 <o r0" and **: "r1 <o r2"
  hence "(\<exists>f. ?phi10 f) \<and> (\<exists>f. ?phi20 f)"
  by (auto simp add: ordLess_def embedS_def)
  hence "?phi10 ?f10 \<and> ?phi20 ?f20" by (auto simp add: someI_ex)
  thus "(?f10 ` ?A1, ?f20 ` ?A2) \<in> ofilterIncl r0"
  using * ** by (simp add: embed_ordLess_ofilterIncl)
qed

theorem wf_ordLess: "wf ordLess"
proof-
  {fix r0 :: "('a \<times> 'a) set"
   (* need to annotate here!*)
   let ?ordLess = "ordLess::('d rel * 'd rel) set"
   let ?R = "?ordLess Int (?ordLess^-1``{r0} \<times> ?ordLess^-1``{r0})"
   {assume Case1: "Well_order r0"
    hence "wf ?R"
    using wf_ofilterIncl[of r0]
          compat_wf[of ?R "ofilterIncl r0" "ord_to_filter r0"]
          ord_to_filter_compat[of r0] by auto
   }
   moreover
   {assume Case2: "\<not> Well_order r0"
    hence "?R = {}" unfolding ordLess_def by auto
    hence "wf ?R" using wf_empty by simp
   }
   ultimately have "wf ?R" by blast
  }
  thus ?thesis by (simp add: trans_wf_iff ordLess_trans)
qed

corollary exists_minim_Well_order:
assumes NE: "R \<noteq> {}" and WELL: "\<forall>r \<in> R. Well_order r"
shows "\<exists>r \<in> R. \<forall>r' \<in> R. r \<le>o r'"
proof-
  obtain r where "r \<in> R \<and> (\<forall>r' \<in> R. \<not> r' <o r)"
  using NE spec[OF spec[OF subst[OF wf_eq_minimal, of "%x. x", OF wf_ordLess]], of _ R]
    equals0I[of R] by blast
  with not_ordLeq_iff_ordLess WELL show ?thesis by blast
qed


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

text\<open>The direct image operator is the dual of the inverse image operator \<open>inv_image\<close>
from \<open>Relation.thy\<close>.  It is useful for transporting a well-order between
different types.\<close>

definition dir_image :: "'a rel \<Rightarrow> ('a \<Rightarrow> 'a') \<Rightarrow> 'a' rel"
where
"dir_image r f = {(f a, f b)| a b. (a,b) \<in> r}"

lemma dir_image_Field:
"Field(dir_image r f) = f ` (Field r)"
unfolding dir_image_def Field_def Range_def Domain_def by fast

lemma dir_image_minus_Id:
"inj_on f (Field r) \<Longrightarrow> (dir_image r f) - Id = dir_image (r - Id) f"
unfolding inj_on_def Field_def dir_image_def by auto

lemma Refl_dir_image:
assumes "Refl r"
shows "Refl(dir_image r f)"
proof-
  {fix a' b'
   assume "(a',b') \<in> dir_image r f"
   then obtain a b where 1: "a' = f a \<and> b' = f b \<and> (a,b) \<in> r"
   unfolding dir_image_def by blast
   hence "a \<in> Field r \<and> b \<in> Field r" using Field_def by fastforce
   hence "(a,a) \<in> r \<and> (b,b) \<in> r" using assms by (simp add: refl_on_def)
   with 1 have "(a',a') \<in> dir_image r f \<and> (b',b') \<in> dir_image r f"
   unfolding dir_image_def by auto
  }
  thus ?thesis
  by(unfold refl_on_def Field_def Domain_def Range_def, auto)
qed

lemma trans_dir_image:
assumes TRANS: "trans r" and INJ: "inj_on f (Field r)"
shows "trans(dir_image r f)"
proof(unfold trans_def, auto)
  fix a' b' c'
  assume "(a',b') \<in> dir_image r f" "(b',c') \<in> dir_image r f"
  then obtain a b1 b2 c where 1: "a' = f a \<and> b' = f b1 \<and> b' = f b2 \<and> c' = f c" and
                         2: "(a,b1) \<in> r \<and> (b2,c) \<in> r"
  unfolding dir_image_def by blast
  hence "b1 \<in> Field r \<and> b2 \<in> Field r"
  unfolding Field_def by auto
  hence "b1 = b2" using 1 INJ unfolding inj_on_def by auto
  hence "(a,c): r" using 2 TRANS unfolding trans_def by blast
  thus "(a',c') \<in> dir_image r f"
  unfolding dir_image_def using 1 by auto
qed

lemma Preorder_dir_image:
"\<lbrakk>Preorder r; inj_on f (Field r)\<rbrakk> \<Longrightarrow> Preorder (dir_image r f)"
by (simp add: preorder_on_def Refl_dir_image trans_dir_image)

lemma antisym_dir_image:
assumes AN: "antisym r" and INJ: "inj_on f (Field r)"
shows "antisym(dir_image r f)"
proof(unfold antisym_def, auto)
  fix a' b'
  assume "(a',b') \<in> dir_image r f" "(b',a') \<in> dir_image r f"
  then obtain a1 b1 a2 b2 where 1: "a' = f a1 \<and> a' = f a2 \<and> b' = f b1 \<and> b' = f b2" and
                           2: "(a1,b1) \<in> r \<and> (b2,a2) \<in> r " and
                           3: "{a1,a2,b1,b2} \<le> Field r"
  unfolding dir_image_def Field_def by blast
  hence "a1 = a2 \<and> b1 = b2" using INJ unfolding inj_on_def by auto
  hence "a1 = b2" using 2 AN unfolding antisym_def by auto
  thus "a' = b'" using 1 by auto
qed

lemma Partial_order_dir_image:
"\<lbrakk>Partial_order r; inj_on f (Field r)\<rbrakk> \<Longrightarrow> Partial_order (dir_image r f)"
by (simp add: partial_order_on_def Preorder_dir_image antisym_dir_image)

lemma Total_dir_image:
assumes TOT: "Total r" and INJ: "inj_on f (Field r)"
shows "Total(dir_image r f)"
proof(unfold total_on_def, intro ballI impI)
  fix a' b'
  assume "a' \<in> Field (dir_image r f)" "b' \<in> Field (dir_image r f)"
  then obtain a and b where 1: "a \<in> Field r \<and> b \<in> Field r \<and> f a = a' \<and> f b = b'"
    unfolding dir_image_Field[of r f] by blast
  moreover assume "a' \<noteq> b'"
  ultimately have "a \<noteq> b" using INJ unfolding inj_on_def by auto
  hence "(a,b) \<in> r \<or> (b,a) \<in> r" using 1 TOT unfolding total_on_def by auto
  thus "(a',b') \<in> dir_image r f \<or> (b',a') \<in> dir_image r f"
  using 1 unfolding dir_image_def by auto
qed

lemma Linear_order_dir_image:
"\<lbrakk>Linear_order r; inj_on f (Field r)\<rbrakk> \<Longrightarrow> Linear_order (dir_image r f)"
by (simp add: linear_order_on_def Partial_order_dir_image Total_dir_image)

lemma wf_dir_image:
assumes WF: "wf r" and INJ: "inj_on f (Field r)"
shows "wf(dir_image r f)"
proof(unfold wf_eq_minimal2, intro allI impI, elim conjE)
  fix A'::"'b set"
  assume SUB: "A' \<le> Field(dir_image r f)" and NE: "A' \<noteq> {}"
  obtain A where A_def: "A = {a \<in> Field r. f a \<in> A'}" by blast
  have "A \<noteq> {} \<and> A \<le> Field r" using A_def SUB NE by (auto simp: dir_image_Field)
  then obtain a where 1: "a \<in> A \<and> (\<forall>b \<in> A. (b,a) \<notin> r)"
  using spec[OF WF[unfolded wf_eq_minimal2], of A] by blast
  have "\<forall>b' \<in> A'. (b',f a) \<notin> dir_image r f"
  proof(clarify)
    fix b' assume *: "b' \<in> A'" and **: "(b',f a) \<in> dir_image r f"
    obtain b1 a1 where 2: "b' = f b1 \<and> f a = f a1" and
                       3: "(b1,a1) \<in> r \<and> {a1,b1} \<le> Field r"
    using ** unfolding dir_image_def Field_def by blast
    hence "a = a1" using 1 A_def INJ unfolding inj_on_def by auto
    hence "b1 \<in> A \<and> (b1,a) \<in> r" using 2 3 A_def * by auto
    with 1 show False by auto
  qed
  thus "\<exists>a'\<in>A'. \<forall>b'\<in>A'. (b', a') \<notin> dir_image r f"
  using A_def 1 by blast
qed

lemma Well_order_dir_image:
"\<lbrakk>Well_order r; inj_on f (Field r)\<rbrakk> \<Longrightarrow> Well_order (dir_image r f)"
using assms unfolding well_order_on_def
using Linear_order_dir_image[of r f] wf_dir_image[of "r - Id" f]
  dir_image_minus_Id[of f r]
  subset_inj_on[of f "Field r" "Field(r - Id)"]
  mono_Field[of "r - Id" r] by auto

lemma dir_image_bij_betw:
"\<lbrakk>inj_on f (Field r)\<rbrakk> \<Longrightarrow> bij_betw f (Field r) (Field (dir_image r f))"
unfolding bij_betw_def by (simp add: dir_image_Field order_on_defs)

lemma dir_image_compat:
"compat r (dir_image r f) f"
unfolding compat_def dir_image_def by auto

lemma dir_image_iso:
"\<lbrakk>Well_order r; inj_on f (Field r)\<rbrakk>  \<Longrightarrow> iso r (dir_image r f) f"
using iso_iff3 dir_image_compat dir_image_bij_betw Well_order_dir_image by blast

lemma dir_image_ordIso:
"\<lbrakk>Well_order r; inj_on f (Field r)\<rbrakk>  \<Longrightarrow> r =o dir_image r f"
unfolding ordIso_def using dir_image_iso Well_order_dir_image by blast

lemma Well_order_iso_copy:
assumes WELL: "well_order_on A r" and BIJ: "bij_betw f A A'"
shows "\<exists>r'. well_order_on A' r' \<and> r =o r'"
proof-
   let ?r' = "dir_image r f"
   have 1: "A = Field r \<and> Well_order r"
   using WELL well_order_on_Well_order by blast
   hence 2: "iso r ?r' f"
   using dir_image_iso using BIJ unfolding bij_betw_def by auto
   hence "f ` (Field r) = Field ?r'" using 1 iso_iff[of r ?r'] by blast
   hence "Field ?r' = A'"
   using 1 BIJ unfolding bij_betw_def by auto
   moreover have "Well_order ?r'"
   using 1 Well_order_dir_image BIJ unfolding bij_betw_def by blast
   ultimately show ?thesis unfolding ordIso_def using 1 2 by blast
qed


subsection \<open>Bounded square\<close>

text\<open>This construction essentially defines, for an order relation \<open>r\<close>, a lexicographic
order \<open>bsqr r\<close> on \<open>(Field r) \<times> (Field r)\<close>, applying the
following criteria (in this order):
\begin{itemize}
\item compare the maximums;
\item compare the first components;
\item compare the second components.
\end{itemize}
%
The only application of this construction that we are aware of is
at proving that the square of an infinite set has the same cardinal
as that set. The essential property required there (and which is ensured by this
construction) is that any proper order filter of the product order is included in a rectangle, i.e.,
in a product of proper filters on the original relation (assumed to be a well-order).\<close>

definition bsqr :: "'a rel => ('a * 'a)rel"
where
"bsqr r = {((a1,a2),(b1,b2)).
           {a1,a2,b1,b2} \<le> Field r \<and>
           (a1 = b1 \<and> a2 = b2 \<or>
            (wo_rel.max2 r a1 a2, wo_rel.max2 r b1 b2) \<in> r - Id \<or>
            wo_rel.max2 r a1 a2 = wo_rel.max2 r b1 b2 \<and> (a1,b1) \<in> r - Id \<or>
            wo_rel.max2 r a1 a2 = wo_rel.max2 r b1 b2 \<and> a1 = b1  \<and> (a2,b2) \<in> r - Id
           )}"

lemma Field_bsqr:
"Field (bsqr r) = Field r \<times> Field r"
proof
  show "Field (bsqr r) \<le> Field r \<times> Field r"
  proof-
    {fix a1 a2 assume "(a1,a2) \<in> Field (bsqr r)"
     moreover
     have "\<And> b1 b2. ((a1,a2),(b1,b2)) \<in> bsqr r \<or> ((b1,b2),(a1,a2)) \<in> bsqr r \<Longrightarrow>
                      a1 \<in> Field r \<and> a2 \<in> Field r" unfolding bsqr_def by auto
     ultimately have "a1 \<in> Field r \<and> a2 \<in> Field r" unfolding Field_def by auto
    }
    thus ?thesis unfolding Field_def by force
  qed
next
  show "Field r \<times> Field r \<le> Field (bsqr r)"
  proof(auto)
    fix a1 a2 assume "a1 \<in> Field r" and "a2 \<in> Field r"
    hence "((a1,a2),(a1,a2)) \<in> bsqr r" unfolding bsqr_def by blast
    thus "(a1,a2) \<in> Field (bsqr r)" unfolding Field_def by auto
  qed
qed

lemma bsqr_Refl: "Refl(bsqr r)"
by(unfold refl_on_def Field_bsqr, auto simp add: bsqr_def)

lemma bsqr_Trans:
assumes "Well_order r"
shows "trans (bsqr r)"
proof(unfold trans_def, auto)
  (* Preliminary facts *)
  have Well: "wo_rel r" using assms wo_rel_def by auto
  hence Trans: "trans r" using wo_rel.TRANS by auto
  have Anti: "antisym r" using wo_rel.ANTISYM Well by auto
  hence TransS: "trans(r - Id)" using Trans by (simp add: trans_diff_Id)
  (* Main proof *)
  fix a1 a2 b1 b2 c1 c2
  assume *: "((a1,a2),(b1,b2)) \<in> bsqr r" and **: "((b1,b2),(c1,c2)) \<in> bsqr r"
  hence 0: "{a1,a2,b1,b2,c1,c2} \<le> Field r" unfolding bsqr_def by auto
  have 1: "a1 = b1 \<and> a2 = b2 \<or> (wo_rel.max2 r a1 a2, wo_rel.max2 r b1 b2) \<in> r - Id \<or>
           wo_rel.max2 r a1 a2 = wo_rel.max2 r b1 b2 \<and> (a1,b1) \<in> r - Id \<or>
           wo_rel.max2 r a1 a2 = wo_rel.max2 r b1 b2 \<and> a1 = b1 \<and> (a2,b2) \<in> r - Id"
  using * unfolding bsqr_def by auto
  have 2: "b1 = c1 \<and> b2 = c2 \<or> (wo_rel.max2 r b1 b2, wo_rel.max2 r c1 c2) \<in> r - Id \<or>
           wo_rel.max2 r b1 b2 = wo_rel.max2 r c1 c2 \<and> (b1,c1) \<in> r - Id \<or>
           wo_rel.max2 r b1 b2 = wo_rel.max2 r c1 c2 \<and> b1 = c1 \<and> (b2,c2) \<in> r - Id"
  using ** unfolding bsqr_def by auto
  show "((a1,a2),(c1,c2)) \<in> bsqr r"
  proof-
    {assume Case1: "a1 = b1 \<and> a2 = b2"
     hence ?thesis using ** by simp
    }
    moreover
    {assume Case2: "(wo_rel.max2 r a1 a2, wo_rel.max2 r b1 b2) \<in> r - Id"
     {assume Case21: "b1 = c1 \<and> b2 = c2"
      hence ?thesis using * by simp
     }
     moreover
     {assume Case22: "(wo_rel.max2 r b1 b2, wo_rel.max2 r c1 c2) \<in> r - Id"
      hence "(wo_rel.max2 r a1 a2, wo_rel.max2 r c1 c2) \<in> r - Id"
      using Case2 TransS trans_def[of "r - Id"] by blast
      hence ?thesis using 0 unfolding bsqr_def by auto
     }
     moreover
     {assume Case23_4: "wo_rel.max2 r b1 b2 = wo_rel.max2 r c1 c2"
      hence ?thesis using Case2 0 unfolding bsqr_def by auto
     }
     ultimately have ?thesis using 0 2 by auto
    }
    moreover
    {assume Case3: "wo_rel.max2 r a1 a2 = wo_rel.max2 r b1 b2 \<and> (a1,b1) \<in> r - Id"
     {assume Case31: "b1 = c1 \<and> b2 = c2"
      hence ?thesis using * by simp
     }
     moreover
     {assume Case32: "(wo_rel.max2 r b1 b2, wo_rel.max2 r c1 c2) \<in> r - Id"
      hence ?thesis using Case3 0 unfolding bsqr_def by auto
     }
     moreover
     {assume Case33: "wo_rel.max2 r b1 b2 = wo_rel.max2 r c1 c2 \<and> (b1,c1) \<in> r - Id"
      hence "(a1,c1) \<in> r - Id"
      using Case3 TransS trans_def[of "r - Id"] by blast
      hence ?thesis using Case3 Case33 0 unfolding bsqr_def by auto
     }
     moreover
     {assume Case33: "wo_rel.max2 r b1 b2 = wo_rel.max2 r c1 c2 \<and> b1 = c1"
      hence ?thesis using Case3 0 unfolding bsqr_def by auto
     }
     ultimately have ?thesis using 0 2 by auto
    }
    moreover
    {assume Case4: "wo_rel.max2 r a1 a2 = wo_rel.max2 r b1 b2 \<and> a1 = b1 \<and> (a2,b2) \<in> r - Id"
     {assume Case41: "b1 = c1 \<and> b2 = c2"
      hence ?thesis using * by simp
     }
     moreover
     {assume Case42: "(wo_rel.max2 r b1 b2, wo_rel.max2 r c1 c2) \<in> r - Id"
      hence ?thesis using Case4 0 unfolding bsqr_def by force
     }
     moreover
     {assume Case43: "wo_rel.max2 r b1 b2 = wo_rel.max2 r c1 c2 \<and> (b1,c1) \<in> r - Id"
      hence ?thesis using Case4 0 unfolding bsqr_def by auto
     }
     moreover
     {assume Case44: "wo_rel.max2 r b1 b2 = wo_rel.max2 r c1 c2 \<and> b1 = c1 \<and> (b2,c2) \<in> r - Id"
      hence "(a2,c2) \<in> r - Id"
      using Case4 TransS trans_def[of "r - Id"] by blast
      hence ?thesis using Case4 Case44 0 unfolding bsqr_def by auto
     }
     ultimately have ?thesis using 0 2 by auto
    }
    ultimately show ?thesis using 0 1 by auto
  qed
qed

lemma bsqr_antisym:
assumes "Well_order r"
shows "antisym (bsqr r)"
proof(unfold antisym_def, clarify)
  (* Preliminary facts *)
  have Well: "wo_rel r" using assms wo_rel_def by auto
  hence Trans: "trans r" using wo_rel.TRANS by auto
  have Anti: "antisym r" using wo_rel.ANTISYM Well by auto
  hence TransS: "trans(r - Id)" using Trans by (simp add: trans_diff_Id)
  hence IrrS: "\<forall>a b. \<not>((a,b) \<in> r - Id \<and> (b,a) \<in> r - Id)"
  using Anti trans_def[of "r - Id"] antisym_def[of "r - Id"] by blast
  (* Main proof *)
  fix a1 a2 b1 b2
  assume *: "((a1,a2),(b1,b2)) \<in> bsqr r" and **: "((b1,b2),(a1,a2)) \<in> bsqr r"
  hence 0: "{a1,a2,b1,b2} \<le> Field r" unfolding bsqr_def by auto
  have 1: "a1 = b1 \<and> a2 = b2 \<or> (wo_rel.max2 r a1 a2, wo_rel.max2 r b1 b2) \<in> r - Id \<or>
           wo_rel.max2 r a1 a2 = wo_rel.max2 r b1 b2 \<and> (a1,b1) \<in> r - Id \<or>
           wo_rel.max2 r a1 a2 = wo_rel.max2 r b1 b2 \<and> a1 = b1 \<and> (a2,b2) \<in> r - Id"
  using * unfolding bsqr_def by auto
  have 2: "b1 = a1 \<and> b2 = a2 \<or> (wo_rel.max2 r b1 b2, wo_rel.max2 r a1 a2) \<in> r - Id \<or>
           wo_rel.max2 r b1 b2 = wo_rel.max2 r a1 a2 \<and> (b1,a1) \<in> r - Id \<or>
           wo_rel.max2 r b1 b2 = wo_rel.max2 r a1 a2 \<and> b1 = a1 \<and> (b2,a2) \<in> r - Id"
  using ** unfolding bsqr_def by auto
  show "a1 = b1 \<and> a2 = b2"
  proof-
    {assume Case1: "(wo_rel.max2 r a1 a2, wo_rel.max2 r b1 b2) \<in> r - Id"
     {assume Case11: "(wo_rel.max2 r b1 b2, wo_rel.max2 r a1 a2) \<in> r - Id"
      hence False using Case1 IrrS by blast
     }
     moreover
     {assume Case12_3: "wo_rel.max2 r b1 b2 = wo_rel.max2 r a1 a2"
      hence False using Case1 by auto
     }
     ultimately have ?thesis using 0 2 by auto
    }
    moreover
    {assume Case2: "wo_rel.max2 r a1 a2 = wo_rel.max2 r b1 b2 \<and> (a1,b1) \<in> r - Id"
     {assume Case21: "(wo_rel.max2 r b1 b2, wo_rel.max2 r a1 a2) \<in> r - Id"
       hence False using Case2 by auto
     }
     moreover
     {assume Case22: "(b1,a1) \<in> r - Id"
      hence False using Case2 IrrS by blast
     }
     moreover
     {assume Case23: "b1 = a1"
      hence False using Case2 by auto
     }
     ultimately have ?thesis using 0 2 by auto
    }
    moreover
    {assume Case3: "wo_rel.max2 r a1 a2 = wo_rel.max2 r b1 b2 \<and> a1 = b1 \<and> (a2,b2) \<in> r - Id"
     moreover
     {assume Case31: "(wo_rel.max2 r b1 b2, wo_rel.max2 r a1 a2) \<in> r - Id"
      hence False using Case3 by auto
     }
     moreover
     {assume Case32: "(b1,a1) \<in> r - Id"
      hence False using Case3 by auto
     }
     moreover
     {assume Case33: "(b2,a2) \<in> r - Id"
      hence False using Case3 IrrS by blast
     }
     ultimately have ?thesis using 0 2 by auto
    }
    ultimately show ?thesis using 0 1 by blast
  qed
qed

lemma bsqr_Total:
assumes "Well_order r"
shows "Total(bsqr r)"
proof-
  (* Preliminary facts *)
  have Well: "wo_rel r" using assms wo_rel_def by auto
  hence Total: "\<forall>a \<in> Field r. \<forall>b \<in> Field r. (a,b) \<in> r \<or> (b,a) \<in> r"
  using wo_rel.TOTALS by auto
  (* Main proof *)
  {fix a1 a2 b1 b2 assume "{(a1,a2), (b1,b2)} \<le> Field(bsqr r)"
   hence 0: "a1 \<in> Field r \<and> a2 \<in> Field r \<and> b1 \<in> Field r \<and> b2 \<in> Field r"
   using Field_bsqr by blast
   have "((a1,a2) = (b1,b2) \<or> ((a1,a2),(b1,b2)) \<in> bsqr r \<or> ((b1,b2),(a1,a2)) \<in> bsqr r)"
   proof(rule wo_rel.cases_Total[of r a1 a2], clarsimp simp add: Well, simp add: 0)
       (* Why didn't clarsimp simp add: Well 0 do the same job? *)
     assume Case1: "(a1,a2) \<in> r"
     hence 1: "wo_rel.max2 r a1 a2 = a2"
     using Well 0 by (simp add: wo_rel.max2_equals2)
     show ?thesis
     proof(rule wo_rel.cases_Total[of r b1 b2], clarsimp simp add: Well, simp add: 0)
       assume Case11: "(b1,b2) \<in> r"
       hence 2: "wo_rel.max2 r b1 b2 = b2"
       using Well 0 by (simp add: wo_rel.max2_equals2)
       show ?thesis
       proof(rule wo_rel.cases_Total3[of r a2 b2], clarsimp simp add: Well, simp add: 0)
         assume Case111: "(a2,b2) \<in> r - Id \<or> (b2,a2) \<in> r - Id"
         thus ?thesis using 0 1 2 unfolding bsqr_def by auto
       next
         assume Case112: "a2 = b2"
         show ?thesis
         proof(rule wo_rel.cases_Total3[of r a1 b1], clarsimp simp add: Well, simp add: 0)
           assume Case1121: "(a1,b1) \<in> r - Id \<or> (b1,a1) \<in> r - Id"
           thus ?thesis using 0 1 2 Case112 unfolding bsqr_def by auto
         next
           assume Case1122: "a1 = b1"
           thus ?thesis using Case112 by auto
         qed
       qed
     next
       assume Case12: "(b2,b1) \<in> r"
       hence 3: "wo_rel.max2 r b1 b2 = b1" using Well 0 by (simp add: wo_rel.max2_equals1)
       show ?thesis
       proof(rule wo_rel.cases_Total3[of r a2 b1], clarsimp simp add: Well, simp add: 0)
         assume Case121: "(a2,b1) \<in> r - Id \<or> (b1,a2) \<in> r - Id"
         thus ?thesis using 0 1 3 unfolding bsqr_def by auto
       next
         assume Case122: "a2 = b1"
         show ?thesis
         proof(rule wo_rel.cases_Total3[of r a1 b1], clarsimp simp add: Well, simp add: 0)
           assume Case1221: "(a1,b1) \<in> r - Id \<or> (b1,a1) \<in> r - Id"
           thus ?thesis using 0 1 3 Case122 unfolding bsqr_def by auto
         next
           assume Case1222: "a1 = b1"
           show ?thesis
           proof(rule wo_rel.cases_Total3[of r a2 b2], clarsimp simp add: Well, simp add: 0)
             assume Case12221: "(a2,b2) \<in> r - Id \<or> (b2,a2) \<in> r - Id"
             thus ?thesis using 0 1 3 Case122 Case1222 unfolding bsqr_def by auto
           next
             assume Case12222: "a2 = b2"
             thus ?thesis using Case122 Case1222 by auto
           qed
         qed
       qed
     qed
   next
     assume Case2: "(a2,a1) \<in> r"
     hence 1: "wo_rel.max2 r a1 a2 = a1" using Well 0 by (simp add: wo_rel.max2_equals1)
     show ?thesis
     proof(rule wo_rel.cases_Total[of r b1 b2], clarsimp simp add: Well, simp add: 0)
       assume Case21: "(b1,b2) \<in> r"
       hence 2: "wo_rel.max2 r b1 b2 = b2" using Well 0 by (simp add: wo_rel.max2_equals2)
       show ?thesis
       proof(rule wo_rel.cases_Total3[of r a1 b2], clarsimp simp add: Well, simp add: 0)
         assume Case211: "(a1,b2) \<in> r - Id \<or> (b2,a1) \<in> r - Id"
         thus ?thesis using 0 1 2 unfolding bsqr_def by auto
       next
         assume Case212: "a1 = b2"
         show ?thesis
         proof(rule wo_rel.cases_Total3[of r a1 b1], clarsimp simp add: Well, simp add: 0)
           assume Case2121: "(a1,b1) \<in> r - Id \<or> (b1,a1) \<in> r - Id"
           thus ?thesis using 0 1 2 Case212 unfolding bsqr_def by auto
         next
           assume Case2122: "a1 = b1"
           show ?thesis
           proof(rule wo_rel.cases_Total3[of r a2 b2], clarsimp simp add: Well, simp add: 0)
             assume Case21221: "(a2,b2) \<in> r - Id \<or> (b2,a2) \<in> r - Id"
             thus ?thesis using 0 1 2 Case212 Case2122 unfolding bsqr_def by auto
           next
             assume Case21222: "a2 = b2"
             thus ?thesis using Case2122 Case212 by auto
           qed
         qed
       qed
     next
       assume Case22: "(b2,b1) \<in> r"
       hence 3: "wo_rel.max2 r b1 b2 = b1"  using Well 0 by (simp add: wo_rel.max2_equals1)
       show ?thesis
       proof(rule wo_rel.cases_Total3[of r a1 b1], clarsimp simp add: Well, simp add: 0)
         assume Case221: "(a1,b1) \<in> r - Id \<or> (b1,a1) \<in> r - Id"
         thus ?thesis using 0 1 3 unfolding bsqr_def by auto
       next
         assume Case222: "a1 = b1"
         show ?thesis
         proof(rule wo_rel.cases_Total3[of r a2 b2], clarsimp simp add: Well, simp add: 0)
           assume Case2221: "(a2,b2) \<in> r - Id \<or> (b2,a2) \<in> r - Id"
           thus ?thesis using 0 1 3 Case222 unfolding bsqr_def by auto
         next
           assume Case2222: "a2 = b2"
           thus ?thesis using Case222 by auto
         qed
       qed
     qed
   qed
  }
  thus ?thesis unfolding total_on_def by fast
qed

lemma bsqr_Linear_order:
assumes "Well_order r"
shows "Linear_order(bsqr r)"
unfolding order_on_defs
using assms bsqr_Refl bsqr_Trans bsqr_antisym bsqr_Total by blast

lemma bsqr_Well_order:
assumes "Well_order r"
shows "Well_order(bsqr r)"
using assms
proof(simp add: bsqr_Linear_order Linear_order_Well_order_iff, intro allI impI)
  have 0: "\<forall>A \<le> Field r. A \<noteq> {} \<longrightarrow> (\<exists>a \<in> A. \<forall>a' \<in> A. (a,a') \<in> r)"
  using assms well_order_on_def Linear_order_Well_order_iff by blast
  fix D assume *: "D \<le> Field (bsqr r)" and **: "D \<noteq> {}"
  hence 1: "D \<le> Field r \<times> Field r" unfolding Field_bsqr by simp
  (*  *)
  obtain M where M_def: "M = {wo_rel.max2 r a1 a2| a1 a2. (a1,a2) \<in> D}" by blast
  have "M \<noteq> {}" using 1 M_def ** by auto
  moreover
  have "M \<le> Field r" unfolding M_def
  using 1 assms wo_rel_def[of r] wo_rel.max2_among[of r] by fastforce
  ultimately obtain m where m_min: "m \<in> M \<and> (\<forall>a \<in> M. (m,a) \<in> r)"
  using 0 by blast
  (*  *)
  obtain A1 where A1_def: "A1 = {a1. \<exists>a2. (a1,a2) \<in> D \<and> wo_rel.max2 r a1 a2 = m}" by blast
  have "A1 \<le> Field r" unfolding A1_def using 1 by auto
  moreover have "A1 \<noteq> {}" unfolding A1_def using m_min unfolding M_def by blast
  ultimately obtain a1 where a1_min: "a1 \<in> A1 \<and> (\<forall>a \<in> A1. (a1,a) \<in> r)"
  using 0 by blast
  (*  *)
  obtain A2 where A2_def: "A2 = {a2. (a1,a2) \<in> D \<and> wo_rel.max2 r a1 a2 = m}" by blast
  have "A2 \<le> Field r" unfolding A2_def using 1 by auto
  moreover have "A2 \<noteq> {}" unfolding A2_def
  using m_min a1_min unfolding A1_def M_def by blast
  ultimately obtain a2 where a2_min: "a2 \<in> A2 \<and> (\<forall>a \<in> A2. (a2,a) \<in> r)"
  using 0 by blast
  (*   *)
  have 2: "wo_rel.max2 r a1 a2 = m"
  using a1_min a2_min unfolding A1_def A2_def by auto
  have 3: "(a1,a2) \<in> D" using a2_min unfolding A2_def by auto
  (*  *)
  moreover
  {fix b1 b2 assume ***: "(b1,b2) \<in> D"
   hence 4: "{a1,a2,b1,b2} \<le> Field r" using 1 3 by blast
   have 5: "(wo_rel.max2 r a1 a2, wo_rel.max2 r b1 b2) \<in> r"
   using *** a1_min a2_min m_min unfolding A1_def A2_def M_def by auto
   have "((a1,a2),(b1,b2)) \<in> bsqr r"
   proof(cases "wo_rel.max2 r a1 a2 = wo_rel.max2 r b1 b2")
     assume Case1: "wo_rel.max2 r a1 a2 \<noteq> wo_rel.max2 r b1 b2"
     thus ?thesis unfolding bsqr_def using 4 5 by auto
   next
     assume Case2: "wo_rel.max2 r a1 a2 = wo_rel.max2 r b1 b2"
     hence "b1 \<in> A1" unfolding A1_def using 2 *** by auto
     hence 6: "(a1,b1) \<in> r" using a1_min by auto
     show ?thesis
     proof(cases "a1 = b1")
       assume Case21: "a1 \<noteq> b1"
       thus ?thesis unfolding bsqr_def using 4 Case2 6 by auto
     next
       assume Case22: "a1 = b1"
       hence "b2 \<in> A2" unfolding A2_def using 2 *** Case2 by auto
       hence 7: "(a2,b2) \<in> r" using a2_min by auto
       thus ?thesis unfolding bsqr_def using 4 7 Case2 Case22 by auto
     qed
   qed
  }
  (*  *)
  ultimately show "\<exists>d \<in> D. \<forall>d' \<in> D. (d,d') \<in> bsqr r" by fastforce
qed

lemma bsqr_max2:
assumes WELL: "Well_order r" and LEQ: "((a1,a2),(b1,b2)) \<in> bsqr r"
shows "(wo_rel.max2 r a1 a2, wo_rel.max2 r b1 b2) \<in> r"
proof-
  have "{(a1,a2),(b1,b2)} \<le> Field(bsqr r)"
  using LEQ unfolding Field_def by auto
  hence "{a1,a2,b1,b2} \<le> Field r" unfolding Field_bsqr by auto
  hence "{wo_rel.max2 r a1 a2, wo_rel.max2 r b1 b2} \<le> Field r"
  using WELL wo_rel_def[of r] wo_rel.max2_among[of r] by fastforce
  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"
  using LEQ unfolding bsqr_def by auto
  ultimately show ?thesis using WELL unfolding order_on_defs refl_on_def by auto
qed

lemma bsqr_ofilter:
assumes WELL: "Well_order r" and
        OF: "wo_rel.ofilter (bsqr r) D" and SUB: "D < Field r \<times> Field r" and
        NE: "\<not> (\<exists>a. Field r = under r a)"
shows "\<exists>A. wo_rel.ofilter r A \<and> A < Field r \<and> D \<le> A \<times> A"
proof-
  let ?r' = "bsqr r"
  have Well: "wo_rel r" using WELL wo_rel_def by blast
  hence Trans: "trans r" using wo_rel.TRANS by blast
  have Well': "Well_order ?r' \<and> wo_rel ?r'"
  using WELL bsqr_Well_order wo_rel_def by blast
  (*  *)
  have "D < Field ?r'" unfolding Field_bsqr using SUB .
  with OF obtain a1 and a2 where
  "(a1,a2) \<in> Field ?r'" and 1: "D = underS ?r' (a1,a2)"
  using Well' wo_rel.ofilter_underS_Field[of ?r' D] by auto
  hence 2: "{a1,a2} \<le> Field r" unfolding Field_bsqr by auto
  let ?m = "wo_rel.max2 r a1 a2"
  have "D \<le> (under r ?m) \<times> (under r ?m)"
  proof(unfold 1)
    {fix b1 b2
     let ?n = "wo_rel.max2 r b1 b2"
     assume "(b1,b2) \<in> underS ?r' (a1,a2)"
     hence 3: "((b1,b2),(a1,a2)) \<in> ?r'"
     unfolding underS_def by blast
     hence "(?n,?m) \<in> r" using WELL by (simp add: bsqr_max2)
     moreover
     {have "(b1,b2) \<in> Field ?r'" using 3 unfolding Field_def by auto
      hence "{b1,b2} \<le> Field r" unfolding Field_bsqr by auto
      hence "(b1,?n) \<in> r \<and> (b2,?n) \<in> r"
      using Well by (simp add: wo_rel.max2_greater)
     }
     ultimately have "(b1,?m) \<in> r \<and> (b2,?m) \<in> r"
     using Trans trans_def[of r] by blast
     hence "(b1,b2) \<in> (under r ?m) \<times> (under r ?m)" unfolding under_def by simp}
     thus "underS ?r' (a1,a2) \<le> (under r ?m) \<times> (under r ?m)" by auto
  qed
  moreover have "wo_rel.ofilter r (under r ?m)"
  using Well by (simp add: wo_rel.under_ofilter)
  moreover have "under r ?m < Field r"
  using NE under_Field[of r ?m] by blast
  ultimately show ?thesis by blast
qed

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

lemma Func_empty:
"Func {} B = {\<lambda>x. undefined}"
unfolding Func_def by auto

lemma Func_elim:
assumes "g \<in> Func A B" and "a \<in> A"
shows "\<exists> b. b \<in> B \<and> g a = b"
using assms unfolding Func_def by (cases "g a = undefined") auto

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

lemma curr_in:
assumes f: "f \<in> Func (A \<times> B) C"
shows "curr A f \<in> Func A (Func B C)"
using assms unfolding curr_def Func_def by auto

lemma curr_inj:
assumes "f1 \<in> Func (A \<times> B) C" and "f2 \<in> Func (A \<times> B) C"
shows "curr A f1 = curr A f2 \<longleftrightarrow> f1 = f2"
proof safe
  assume c: "curr A f1 = curr A f2"
  show "f1 = f2"
  proof (rule ext, clarify)
    fix a b show "f1 (a, b) = f2 (a, b)"
    proof (cases "(a,b) \<in> A \<times> B")
      case False
      thus ?thesis using assms unfolding Func_def by auto
    next
      case True hence a: "a \<in> A" and b: "b \<in> B" by auto
      thus ?thesis
      using c unfolding curr_def fun_eq_iff by(elim allE[of _ a]) simp
    qed
  qed
qed

lemma curr_surj:
assumes "g \<in> Func A (Func B C)"
shows "\<exists> f \<in> Func (A \<times> B) C. curr A f = g"
proof
  let ?f = "\<lambda> ab. if fst ab \<in> A \<and> snd ab \<in> B then g (fst ab) (snd ab) else undefined"
  show "curr A ?f = g"
  proof (rule ext)
    fix a show "curr A ?f a = g a"
    proof (cases "a \<in> A")
      case False
      hence "g a = undefined" using assms unfolding Func_def by auto
      thus ?thesis unfolding curr_def using False by simp
    next
      case True
      obtain g1 where "g1 \<in> Func B C" and "g a = g1"
      using assms using Func_elim[OF assms True] by blast
      thus ?thesis using True unfolding Func_def curr_def by auto
    qed
  qed
  show "?f \<in> Func (A \<times> B) C" using assms unfolding Func_def mem_Collect_eq by auto
qed

lemma bij_betw_curr:
"bij_betw (curr A) (Func (A \<times> B) C) (Func A (Func B C))"
unfolding bij_betw_def inj_on_def image_def
apply (intro impI conjI ballI)
apply (erule curr_inj[THEN iffD1], assumption+)
apply auto
apply (erule curr_in)
using curr_surj by blast

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

lemma Func_map:
assumes g: "g \<in> Func A2 A1" and f1: "f1 ` A1 \<subseteq> B1" and f2: "f2 ` B2 \<subseteq> A2"
shows "Func_map B2 f1 f2 g \<in> Func B2 B1"
using assms unfolding Func_def Func_map_def mem_Collect_eq by auto

lemma Func_non_emp:
assumes "B \<noteq> {}"
shows "Func A B \<noteq> {}"
proof-
  obtain b where b: "b \<in> B" using assms by auto
  hence "(\<lambda> a. if a \<in> A then b else undefined) \<in> Func A B" unfolding Func_def by auto
  thus ?thesis by blast
qed

lemma Func_is_emp:
"Func A B = {} \<longleftrightarrow> A \<noteq> {} \<and> B = {}" (is "?L \<longleftrightarrow> ?R")
proof
  assume L: ?L
  moreover {assume "A = {}" hence False using L Func_empty by auto}
  moreover {assume "B \<noteq> {}" hence False using L Func_non_emp[of B A] by simp }
  ultimately show ?R by blast
next
  assume R: ?R
  moreover
  {fix f assume "f \<in> Func A B"
   moreover obtain a where "a \<in> A" using R by blast
   ultimately obtain b where "b \<in> B" unfolding Func_def by blast
   with R have False by blast
  }
  thus ?L by blast
qed

lemma Func_map_surj:
assumes B1: "f1 ` A1 = B1" and A2: "inj_on f2 B2" "f2 ` B2 \<subseteq> A2"
and B2A2: "B2 = {} \<Longrightarrow> A2 = {}"
shows "Func B2 B1 = Func_map B2 f1 f2 ` Func A2 A1"
proof(cases "B2 = {}")
  case True
  thus ?thesis using B2A2 by (auto simp: Func_empty Func_map_def)
next
  case False note B2 = False
  show ?thesis
  proof safe
    fix h assume h: "h \<in> Func B2 B1"
    def j1 \<equiv> "inv_into A1 f1"
    have "\<forall> a2 \<in> f2 ` B2. \<exists> b2. b2 \<in> B2 \<and> f2 b2 = a2" by blast
    then obtain k where k: "\<forall> a2 \<in> f2 ` B2. k a2 \<in> B2 \<and> f2 (k a2) = a2"
      by atomize_elim (rule bchoice)
    {fix b2 assume b2: "b2 \<in> B2"
     hence "f2 (k (f2 b2)) = f2 b2" using k A2(2) by auto
     moreover have "k (f2 b2) \<in> B2" using b2 A2(2) k by auto
     ultimately have "k (f2 b2) = b2" using b2 A2(1) unfolding inj_on_def by blast
    } note kk = this
    obtain b22 where b22: "b22 \<in> B2" using B2 by auto
    def j2 \<equiv> "\<lambda> a2. if a2 \<in> f2 ` B2 then k a2 else b22"
    have j2A2: "j2 ` A2 \<subseteq> B2" unfolding j2_def using k b22 by auto
    have j2: "\<And> b2. b2 \<in> B2 \<Longrightarrow> j2 (f2 b2) = b2"
    using kk unfolding j2_def by auto
    def g \<equiv> "Func_map A2 j1 j2 h"
    have "Func_map B2 f1 f2 g = h"
    proof (rule ext)
      fix b2 show "Func_map B2 f1 f2 g b2 = h b2"
      proof(cases "b2 \<in> B2")
        case True
        show ?thesis
        proof (cases "h b2 = undefined")
          case True
          hence b1: "h b2 \<in> f1 ` A1" using h \<open>b2 \<in> B2\<close> unfolding B1 Func_def by auto
          show ?thesis using A2 f_inv_into_f[OF b1]
            unfolding True g_def Func_map_def j1_def j2[OF \<open>b2 \<in> B2\<close>] by auto
        qed(insert A2 True j2[OF True] h B1, unfold j1_def g_def Func_def Func_map_def,
          auto intro: f_inv_into_f)
      qed(insert h, unfold Func_def Func_map_def, auto)
    qed
    moreover have "g \<in> Func A2 A1" unfolding g_def apply(rule Func_map[OF h])
    using j2A2 B1 A2 unfolding j1_def by (fast intro: inv_into_into)+
    ultimately show "h \<in> Func_map B2 f1 f2 ` Func A2 A1"
    unfolding Func_map_def[abs_def] by auto
  qed(insert B1 Func_map[OF _ _ A2(2)], auto)
qed

end