# Theory BNF_Wellorder_Constructions

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

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

section ‹Constructions on Wellorders as Needed by Bounded Natural Functors›

theory BNF_Wellorder_Constructions
imports BNF_Wellorder_Embedding
begin

text ‹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 ‹ordLeq›, of being embedded (abbreviated ‹≤o›),
‹ordLess›, of being strictly embedded (abbreviated ‹<o›), and
‹ordIso›, of being isomorphic (abbreviated ‹=o›).  We study the
connections between these relations, order filters, and the aforementioned constructions.
A main result of this section is that ‹<o› is well-founded.›

subsection ‹Restriction to a set›

abbreviation Restr :: "'a rel ⇒ 'a set ⇒ 'a rel"
where "Restr r A ≡ r Int (A × A)"

lemma Restr_subset:
"A ≤ B ⟹ 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 ⟹ Refl(Restr r A)"
unfolding refl_on_def Field_def by auto

lemma linear_order_on_Restr:
"linear_order_on A r ⟹ linear_order_on (A ∩ above r x) (Restr r (above r x))"
by(simp add: order_on_defs refl_on_def trans_def antisym_def total_on_def)(safe; blast)

lemma antisym_Restr:
"antisym r ⟹ antisym(Restr r A)"
unfolding antisym_def Field_def by auto

lemma Total_Restr:
"Total r ⟹ Total(Restr r A)"
unfolding total_on_def Field_def by auto

lemma total_on_imp_Total_Restr: "total_on A r ⟹ Total (Restr r A)"
by (auto simp: Field_def total_on_def)

lemma trans_Restr:
"trans r ⟹ trans(Restr r A)"
unfolding trans_def Field_def by blast

lemma Preorder_Restr:
"Preorder r ⟹ Preorder(Restr r A)"
unfolding preorder_on_def by (simp add: Refl_Restr trans_Restr)

lemma Partial_order_Restr:
"Partial_order r ⟹ Partial_order(Restr r A)"
unfolding partial_order_on_def by (simp add: Preorder_Restr antisym_Restr)

lemma Linear_order_Restr:
"Linear_order r ⟹ 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)"
using assms
by (auto simp: well_order_on_def Linear_order_Restr elim: wf_subset)

lemma Field_Restr_subset: "Field(Restr r A) ≤ A"
by (auto simp add: Field_def)

lemma Refl_Field_Restr:
"Refl r ⟹ Field(Restr r A) = (Field r) Int A"
unfolding refl_on_def Field_def by blast

lemma Refl_Field_Restr2:
"⟦Refl r; A ≤ Field r⟧ ⟹ 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 ≤ 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 ‹Order filters versus restrictions and embeddings›

lemma Field_Restr_ofilter:
"⟦Well_order r; wo_rel.ofilter r A⟧ ⟹ 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 ∈ A"
shows "under (Restr r A) a = under r a"
unfolding wo_rel.ofilter_def under_def
proof
show "{b. (b, a) ∈ Restr r A} ⊆ {b. (b, a) ∈ r}"
by auto
next
have "under r a ⊆ A"
proof
fix x
assume *: "x ∈ under r a"
then have "a ∈ Field r"
unfolding under_def using Field_def by fastforce
then show "x ∈ A" using IN assms *
by (auto simp add: wo_rel_def wo_rel.ofilter_def)
qed
then show "{b. (b, a) ∈ r} ⊆ {b. (b, a) ∈ Restr r A}"
unfolding under_def using assms by auto
qed

lemma ofilter_embed:
assumes "Well_order r"
shows "wo_rel.ofilter r A = (A ≤ Field r ∧ embed (Restr r A) r id)"
proof
assume *: "wo_rel.ofilter r A"
show "A ≤ Field r ∧ embed (Restr r A) r id"
unfolding embed_def
proof safe
fix a assume "a ∈ A" thus "a ∈ Field r" using assms *
by (auto simp add: wo_rel_def wo_rel.ofilter_def)
next
fix a assume "a ∈ Field (Restr r A)"
thus "bij_betw id (under (Restr r A) a) (under r (id a))" using assms *
by (simp add: ofilter_Restr_under Field_Restr_ofilter)
qed
next
assume *: "A ≤ Field r ∧ embed (Restr r A) r id"
hence "Field(Restr r A) ≤ 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 ∈ A"
hence "a ∈ 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 ≤ under (Restr r A) a"
unfolding bij_betw_def by auto
also have "… ≤ Field(Restr r A)" by (simp add: under_Field)
also have "… ≤ A" by (simp add: Field_Restr_subset)
finally have "under r a ≤ 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 ∧ Well_order ?rB" using WELL
by (simp add: Well_order_Restr wo_rel_def)
(* Main proof *)
show ?thesis using WellB assms
unfolding wo_rel.ofilter_def under_def ofilter_def
proof safe
fix a assume "a ∈ A" and *: "a ∈ B"
hence "a ∈ Field r" using OFA Well by (auto simp add: wo_rel.ofilter_def)
with * show "a ∈ Field ?rB" using Field by auto
next
fix a b assume "a ∈ A" and "(b,a) ∈ r"
thus "b ∈ 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 ≤ 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 ≤ 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 ∧ Well_order ?rA" using WELL
by (simp add: Well_order_Restr wo_rel_def)
have WellB: "wo_rel ?rB ∧ Well_order ?rB" using WELL
by (simp add: Well_order_Restr wo_rel_def)
(* Main proof *)
show ?thesis
proof
assume *: "A ≤ 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 ∈ A"
hence "a ∈ Field r" using Well OFA by (auto simp add: wo_rel.ofilter_def)
with ** FieldA have "a ∈ Field ?rA" by auto
hence "a ∈ Field ?rB" using * WellA embed_Field[of ?rA ?rB id] by auto
hence "a ∈ B" using FieldB by auto
}
thus "A ≤ 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)) ∧
((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 "∀a b. (a,b) ∈ r' ⟶ a ∈ Field r' ∧ b ∈ 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 ‹The strict inclusion on proper ofilters is well-founded›

definition ofilterIncl :: "'a rel ⇒ 'a set rel"
where
"ofilterIncl r ≡ {(A,B). wo_rel.ofilter r A ∧ A ≠ Field r ∧
wo_rel.ofilter r B ∧ B ≠ Field r ∧ 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 = "(λ 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 ≠ Field r" and
**: "wo_rel.ofilter r B" "B ≠ Field r" and ***: "A < B"
then obtain a and b where 0: "a ∈ Field r ∧ b ∈ Field r" and
1: "A = underS r a ∧ B = underS r b"
using Well by (auto simp add: wo_rel.ofilter_underS_Field)
hence "a ≠ b" using *** by auto
moreover
have "(a,b) ∈ r" using 0 1 Lo ***
by (auto simp add: underS_incl_iff)
moreover
have "a = wo_rel.suc r A ∧ 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) ∈ r ∧ wo_rel.suc r A ≠ wo_rel.suc r B"
by simp
qed
ultimately show "wf (ofilterIncl r)" by (simp add: compat_wf)
qed

subsection ‹Ordering the well-orders by existence of embeddings›

text ‹We define three relations between well-orders:
\begin{itemize}
\item ‹ordLeq›, of being embedded (abbreviated ‹≤o›);
\item ‹ordLess›, of being strictly embedded (abbreviated ‹<o›);
\item ‹ordIso›, of being isomorphic (abbreviated ‹=o›).
\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
‹≤›, ‹<›, ‹=› associated to a total order on a set.
›

definition ordLeq :: "('a rel * 'a' rel) set"
where
"ordLeq = {(r,r'). Well_order r ∧ Well_order r' ∧ (∃f. embed r r' f)}"

abbreviation ordLeq2 :: "'a rel ⇒ 'a' rel ⇒ bool" (infix "<=o" 50)
where "r <=o r' ≡ (r,r') ∈ ordLeq"

abbreviation ordLeq3 :: "'a rel ⇒ 'a' rel ⇒ bool" (infix "≤o" 50)
where "r ≤o r' ≡ r <=o r'"

definition ordLess :: "('a rel * 'a' rel) set"
where
"ordLess = {(r,r'). Well_order r ∧ Well_order r' ∧ (∃f. embedS r r' f)}"

abbreviation ordLess2 :: "'a rel ⇒ 'a' rel ⇒ bool" (infix "<o" 50)
where "r <o r' ≡ (r,r') ∈ ordLess"

definition ordIso :: "('a rel * 'a' rel) set"
where
"ordIso = {(r,r'). Well_order r ∧ Well_order r' ∧ (∃f. iso r r' f)}"

abbreviation ordIso2 :: "'a rel ⇒ 'a' rel ⇒ bool" (infix "=o" 50)
where "r =o r' ≡ (r,r') ∈ ordIso"

lemmas ordRels_def = ordLeq_def ordLess_def ordIso_def

lemma ordLeq_Well_order_simp:
assumes "r ≤o r'"
shows "Well_order r ∧ Well_order r'"
using assms unfolding ordLeq_def by simp

text‹Notice that the relations ‹≤o›, ‹<o›, ‹=o› 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 ‹(('a rel) * ('a rel)) set› , i.e.,
to ‹'a rel rel›.›

lemma ordLeq_reflexive:
"Well_order r ⟹ r ≤o r"
unfolding ordLeq_def using id_embed[of r] by blast

lemma ordLeq_transitive[trans]:
assumes "r ≤o r'" and "r' ≤o r''"
shows "r ≤o r''"
using assms by (auto simp: ordLeq_def intro: comp_embed)

lemma ordLeq_total:
"⟦Well_order r; Well_order r'⟧ ⟹ r ≤o r' ∨ r' ≤o r"
unfolding ordLeq_def using wellorders_totally_ordered by blast

lemma ordIso_reflexive:
"Well_order r ⟹ 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''"
using assms by (auto simp: ordIso_def intro: comp_iso)

lemma ordIso_symmetric:
assumes *: "r =o r'"
shows "r' =o r"
proof-
obtain f where 1: "Well_order r ∧ Well_order r'" and
2: "embed r r' f ∧ 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' ∧ 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 ≤o r'" and " r' <o r''"
shows "r <o r''"
proof-
have "Well_order r ∧ 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' ≤o r''"
shows "r <o r''"
using embedS_comp_embed assms by (force simp: ordLeq_def ordLess_def)

lemma ordLeq_ordIso_trans[trans]:
assumes "r ≤o r'" and " r' =o r''"
shows "r ≤o r''"
using embed_comp_iso assms by (force simp: ordLeq_def ordIso_def)

lemma ordIso_ordLeq_trans[trans]:
assumes "r =o r'" and " r' ≤o r''"
shows "r ≤o r''"
using iso_comp_embed assms by (force simp: ordLeq_def ordIso_def)

lemma ordLess_ordIso_trans[trans]:
assumes "r <o r'" and " r' =o r''"
shows "r <o r''"
using embedS_comp_iso assms by (force simp: ordLess_def ordIso_def)

lemma ordIso_ordLess_trans[trans]:
assumes "r =o r'" and " r' <o r''"
shows "r <o r''"
using iso_comp_embedS assms by (force simp: ordLess_def ordIso_def)

lemma ordLess_not_embed:
assumes "r <o r'"
shows "¬(∃f'. embed r' r f')"
proof-
obtain f where 1: "Well_order r ∧ Well_order r'" and 2: "embed r r' f" and
3: " ¬ 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 "¬ (f(Field r1) = Field r2)"
proof-
let ?A1 = "Field r1"  let ?A2 = "Field r2"
obtain g where
0: "Well_order r1 ∧ Well_order r2" and
1: "embed r1 r2 g ∧ ¬(bij_betw g ?A1 ?A2)"
using OL unfolding ordLess_def by (auto simp add: embedS_def)
hence "∀a ∈ ?A1. f a = g a"
using 0 EMB embed_unique[of r1] by auto
hence "¬(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 ∧ Well_order r' ∧ ¬(∃f'. embed r' r f'))"
proof
assume *: "r <o r'"
hence "¬(∃f'. embed r' r f')" using ordLess_not_embed[of r r'] by simp
with * show "Well_order r ∧ Well_order r' ∧ ¬ (∃f'. embed r' r f')"
unfolding ordLess_def by auto
next
assume *: "Well_order r ∧ Well_order r' ∧ ¬ (∃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') ∈ ordLess"
unfolding ordLess_def using * by (fastforce simp add: embedS_def)
qed

lemma ordLess_irreflexive: "¬ r <o r"
using id_embed[of r] by (auto simp: ordLess_iff)

lemma ordLeq_iff_ordLess_or_ordIso:
"r ≤o r' = (r <o r' ∨ r =o r')"
unfolding ordRels_def embedS_defs iso_defs by blast

lemma ordIso_iff_ordLeq:
"(r =o r') = (r ≤o r' ∧ r' ≤o r)"
proof
assume "r =o r'"
then obtain f where 1: "Well_order r ∧ Well_order r' ∧
embed r r' f ∧ bij_betw f (Field r) (Field r')"
unfolding ordIso_def iso_defs by auto
hence "embed r r' f ∧ embed r' r (inv_into (Field r) f)"
by (simp add: inv_into_Field_embed_bij_betw)
thus  "r ≤o r' ∧ r' ≤o r"
unfolding ordLeq_def using 1 by auto
next
assume "r ≤o r' ∧ r' ≤o r"
then obtain f and g where 1: "Well_order r ∧ Well_order r' ∧
embed r r' f ∧ 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' ⟹ ¬ r' ≤o r"
using ordLess_ordLeq_trans ordLess_irreflexive by blast

lemma not_ordLeq_ordLess:
"r ≤o r' ⟹ ¬ r' <o r"
using not_ordLess_ordLeq by blast

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

lemma not_ordLess_ordIso:
"r <o r' ⟹ ¬ r =o r'"
using 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 "(¬ r' ≤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 "(¬ r' <o r) = (r ≤o r')"
using assms not_ordLess_ordLeq ordLess_or_ordLeq by blast

lemma ordLess_transitive[trans]:
"⟦r <o r'; r' <o r''⟧ ⟹ r <o r''"
using 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' ⟹ r ≤o r'"
using ordIso_iff_ordLeq by blast

lemma ordLess_imp_ordLeq:
"r <o r' ⟹ r ≤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 ≤ B) = (Restr r A ≤o Restr r B)"
proof
assume "A ≤ B"
thus "Restr r A ≤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 ≤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 ≤ 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 ∧ Well_order ?rB"
using WELL Well_order_Restr by blast
have "(A < B) = (¬ B ≤ A)" using assms
wo_rel_def wo_rel.ofilter_linord[of r A B] by blast
also have "… = (¬ Restr r B ≤o Restr r A)"
using assms ofilter_subset_ordLeq by blast
also have "… = (Restr r A <o Restr r B)"
using 1 not_ordLeq_iff_ordLess by blast
finally show ?thesis .
qed

lemma ofilter_ordLess:
"⟦Well_order r; wo_rel.ofilter r A⟧ ⟹ (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 ≠ {}"
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)) ∈ (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 ∧ Well_order r2 ∧ Well_order r3" and
1: "embed r1 r2 f12 ∧ ¬(bij_betw f12 ?A1 ?A2)" and
2: "embed r2 r3 g23 ∧ ¬(bij_betw g23 ?A2 ?A3)"
using OL12 OL23 by (auto simp add: ordLess_def embedS_def)
hence "∀a ∈ ?A2. f23 a = g23 a"
using EMB23 embed_unique[of r2 r3] by blast
hence 3: "¬(bij_betw f23 ?A2 ?A3)"
using 2 bij_betw_cong[of ?A2 f23 g23] by blast
(*  *)
have 4: "wo_rel.ofilter r2 (f12  ?A1) ∧ f12  ?A1 ≠ ?A2"
using 0 1 OL12 by (simp add: embed_Field_ofilter ordLess_Field)
have 5: "wo_rel.ofilter r3 (f23  ?A2) ∧ f23  ?A2 ≠ ?A3"
using 0 EMB23 OL23 by (simp add: embed_Field_ofilter ordLess_Field)
have 6: "wo_rel.ofilter r3 (f13  ?A1)  ∧ f13  ?A1 ≠ ?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: image_strict_mono)
moreover
{have "embed r1 r3 (f23 ∘ f12)"
using 1 EMB23 0 by (auto simp add: comp_embed)
hence "∀a ∈ ?A1. f23(f12 a) = f13 a"
using EMB13 0 embed_unique[of r1 r3 "f23 ∘ 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) = (∃a ∈ Field r. r' =o Restr r (underS r a))"
proof safe
fix a assume *: "a ∈ 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 ∧ Well_order r'" and
2: "embed r' r f ∧ f  (Field r') ≠ 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 ∈ 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 "∃a ∈ Field r. r' =o Restr r (underS r a)" using 3 by auto
qed

lemma internalize_ordLess:
"(r' <o r) = (∃p. Field p < Field r ∧ r' =o p ∧ p <o r)"
proof
assume *: "r' <o r"
hence 0: "Well_order r ∧ Well_order r'" unfolding ordLess_def by auto
with * obtain a where 1: "a ∈ 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 "∃p. Field p < Field r ∧ r' =o p ∧ p <o r" using 2 by blast
next
assume "∃p. Field p < Field r ∧ r' =o p ∧ p <o r"
thus "r' <o r" using ordIso_ordLess_trans by blast
qed

lemma internalize_ordLeq:
"(r' ≤o r) = (∃p. Field p ≤ Field r ∧ r' =o p ∧ p ≤o r)"
proof
assume *: "r' ≤o r"
moreover
have "r' <o r ⟹ ∃p. Field p ≤ Field r ∧ r' =o p ∧ p ≤o r"
using ordLeq_iff_ordLess_or_ordIso internalize_ordLess[of r' r] by blast
moreover
have "r ≤o r" using * ordLeq_def ordLeq_reflexive by blast
ultimately show "∃p. Field p ≤ Field r ∧ r' =o p ∧ p ≤o r"
using ordLeq_iff_ordLess_or_ordIso by blast
next
assume "∃p. Field p ≤ Field r ∧ r' =o p ∧ p ≤o r"
thus "r' ≤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 ≤o r') = (∀a ∈ Field r. Restr r (underS r a) <o r')"
proof safe
assume *: "r ≤o r'"
fix a assume "a ∈ 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 *: "∀a ∈ Field r. Restr r (underS r a) <o r'"
{assume "r' <o r"
then obtain a where "a ∈ Field r ∧ 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 ≤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: "¬finite(Field r')"
shows "r <o r'"
proof-
{assume "r' ≤o r"
then obtain h where "inj_on h (Field r') ∧ h  (Field r') ≤ 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 ∧ Well_order r' ∧ Field r = A ∧ Field r' = A"
using assms well_order_on_Well_order by blast
moreover
have "∀r r'. well_order_on A r ∧ well_order_on A r' ∧ r ≤o r'
⟶ 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 ∧ Well_order r' ∧ Field r = A ∧ Field r' = A"
using * ** well_order_on_Well_order by blast
assume "r ≤o r'"
then obtain f where 1: "embed r r' f" and
"inj_on f A ∧ f  A ≤ 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‹‹<o› is well-founded›

text ‹Of course, it only makes sense to state that the ‹<o› is well-founded
on the restricted type ‹'a rel rel›.  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 ‹<o› versus
{\em strict inclusion}; and we already know that strict inclusion of order filters is well-founded.›

definition ord_to_filter :: "'a rel ⇒ 'a rel ⇒ 'a set"
where "ord_to_filter r0 r ≡ (SOME f. embed r r0 f)  (Field r)"

lemma ord_to_filter_compat:
"compat (ordLess Int (ordLess¯{r0} × ordLess¯{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 = "λ f10. embed r1 r0 f10" let ?f10 = "SOME f. ?phi10 f"
let ?phi20 = "λ f20. embed r2 r0 f20" let ?f20 = "SOME f. ?phi20 f"
assume *: "r1 <o r0" "r2 <o r0" and **: "r1 <o r2"
hence "(∃f. ?phi10 f) ∧ (∃f. ?phi20 f)"
by (auto simp add: ordLess_def embedS_def)
hence "?phi10 ?f10 ∧ ?phi20 ?f20" by (auto simp add: someI_ex)
thus "(?f10  ?A1, ?f20  ?A2) ∈ ofilterIncl r0"
using * ** by (simp add: embed_ordLess_ofilterIncl)
qed

theorem wf_ordLess: "wf ordLess"
proof-
{fix r0 :: "('a × 'a) set"
(* need to annotate here!*)
let ?ordLess = "ordLess::('d rel * 'd rel) set"
let ?R = "?ordLess Int (?ordLess¯{r0} × ?ordLess¯{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: "¬ 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 ≠ {}" and WELL: "∀r ∈ R. Well_order r"
shows "∃r ∈ R. ∀r' ∈ R. r ≤o r'"
proof-
obtain r where "r ∈ R ∧ (∀r' ∈ R. ¬ 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 ‹Copy via direct images›

text‹The direct image operator is the dual of the inverse image operator ‹inv_image›
from ‹Relation.thy›.  It is useful for transporting a well-order between
different types.›

definition dir_image :: "'a rel ⇒ ('a ⇒ 'a') ⇒ 'a' rel"
where
"dir_image r f = {(f a, f b)| a b. (a,b) ∈ 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) ⟹ (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') ∈ dir_image r f"
then obtain a b where 1: "a' = f a ∧ b' = f b ∧ (a,b) ∈ r"
unfolding dir_image_def by blast
hence "a ∈ Field r ∧ b ∈ Field r" using Field_def by fastforce
hence "(a,a) ∈ r ∧ (b,b) ∈ r" using assms by (simp add: refl_on_def)
with 1 have "(a',a') ∈ dir_image r f ∧ (b',b') ∈ 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)"
unfolding trans_def
proof safe
fix a' b' c'
assume "(a',b') ∈ dir_image r f" "(b',c') ∈ dir_image r f"
then obtain a b1 b2 c where 1: "a' = f a ∧ b' = f b1 ∧ b' = f b2 ∧ c' = f c" and
2: "(a,b1) ∈ r ∧ (b2,c) ∈ r"
unfolding dir_image_def by blast
hence "b1 ∈ Field r ∧ b2 ∈ 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') ∈ dir_image r f"
unfolding dir_image_def using 1 by auto
qed

lemma Preorder_dir_image:
"⟦Preorder r; inj_on f (Field r)⟧ ⟹ 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)"
unfolding antisym_def
proof safe
fix a' b'
assume "(a',b') ∈ dir_image r f" "(b',a') ∈ dir_image r f"
then obtain a1 b1 a2 b2 where 1: "a' = f a1 ∧ a' = f a2 ∧ b' = f b1 ∧ b' = f b2" and
2: "(a1,b1) ∈ r ∧ (b2,a2) ∈ r " and
3: "{a1,a2,b1,b2} ≤ Field r"
unfolding dir_image_def Field_def by blast
hence "a1 = a2 ∧ 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:
"⟦Partial_order r; inj_on f (Field r)⟧ ⟹ 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' ∈ Field (dir_image r f)" "b' ∈ Field (dir_image r f)"
then obtain a and b where 1: "a ∈ Field r ∧ b ∈ Field r ∧ f a = a' ∧ f b = b'"
unfolding dir_image_Field[of r f] by blast
moreover assume "a' ≠ b'"
ultimately have "a ≠ b" using INJ unfolding inj_on_def by auto
hence "(a,b) ∈ r ∨ (b,a) ∈ r" using 1 TOT unfolding total_on_def by auto
thus "(a',b') ∈ dir_image r f ∨ (b',a') ∈ dir_image r f"
using 1 unfolding dir_image_def by auto
qed

lemma Linear_order_dir_image:
"⟦Linear_order r; inj_on f (Field r)⟧ ⟹ 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' ≤ Field(dir_image r f)" and NE: "A' ≠ {}"
obtain A where A_def: "A = {a ∈ Field r. f a ∈ A'}" by blast
have "A ≠ {} ∧ A ≤ Field r" using A_def SUB NE by (auto simp: dir_image_Field)
then obtain a where 1: "a ∈ A ∧ (∀b ∈ A. (b,a) ∉ r)"
using spec[OF WF[unfolded wf_eq_minimal2], of A] by blast
have "∀b' ∈ A'. (b',f a) ∉ dir_image r f"
proof(clarify)
fix b' assume *: "b' ∈ A'" and **: "(b',f a) ∈ dir_image r f"
obtain b1 a1 where 2: "b' = f b1 ∧ f a = f a1" and
3: "(b1,a1) ∈ r ∧ {a1,b1} ≤ 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 ∈ A ∧ (b1,a) ∈ r" using 2 3 A_def * by auto
with 1 show False by auto
qed
thus "∃a'∈A'. ∀b'∈A'. (b', a') ∉ dir_image r f"
using A_def 1 by blast
qed

lemma Well_order_dir_image:
"⟦Well_order r; inj_on f (Field r)⟧ ⟹ Well_order (dir_image r f)"
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:
"⟦inj_on f (Field r)⟧ ⟹ 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:
"⟦Well_order r; inj_on f (Field r)⟧  ⟹ 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:
"⟦Well_order r; inj_on f (Field r)⟧  ⟹ 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 "∃r'. well_order_on A' r' ∧ r =o r'"
proof-
let ?r' = "dir_image r f"
have 1: "A = Field r ∧ 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 ‹Bounded square›

text‹This construction essentially defines, for an order relation ‹r›, a lexicographic
order ‹bsqr r› on ‹(Field r) × (Field r)›, 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).›

definition bsqr :: "'a rel => ('a * 'a)rel"
where
"bsqr r = {((a1,a2),(b1,b2)).
{a1,a2,b1,b2} ≤ Field r ∧
(a1 = b1 ∧ a2 = b2 ∨
(wo_rel.max2 r a1 a2, wo_rel.max2 r b1 b2) ∈ r - Id ∨
wo_rel.max2 r a1 a2 = wo_rel.max2 r b1 b2 ∧ (a1,b1) ∈ r - Id ∨
wo_rel.max2 r a1 a2 = wo_rel.max2 r b1 b2 ∧ a1 = b1  ∧ (a2,b2) ∈ r - Id
)}"

lemma Field_bsqr:
"Field (bsqr r) = Field r × Field r"
proof
show "Field (bsqr r) ≤ Field r × Field r"
proof-
{fix a1 a2 assume "(a1,a2) ∈ Field (bsqr r)"
moreover
have "⋀ b1 b2. ((a1,a2),(b1,b2)) ∈ bsqr r ∨ ((b1,b2),(a1,a2)) ∈ bsqr r ⟹
a1 ∈ Field r ∧ a2 ∈ Field r" unfolding bsqr_def by auto
ultimately have "a1 ∈ Field r ∧ a2 ∈ Field r" unfolding Field_def by auto
}
thus ?thesis unfolding Field_def by force
qed
next
show "Field r × Field r ≤ Field (bsqr r)"
proof safe
fix a1 a2 assume "a1 ∈ Field r" and "a2 ∈ Field r"
hence "((a1,a2),(a1,a2)) ∈ bsqr r" unfolding bsqr_def by blast
thus "(a1,a2) ∈ 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)"
unfolding trans_def
proof safe
(* 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)) ∈ bsqr r" and **: "((b1,b2),(c1,c2)) ∈ bsqr r"
hence 0: "{a1,a2,b1,b2,c1,c2} ≤ Field r" unfolding bsqr_def by auto
have 1: "a1 = b1 ∧ a2 = b2 ∨ (wo_rel.max2 r a1 a2, wo_rel.max2 r b1 b2) ∈ r - Id ∨
wo_rel.max2 r a1 a2 = wo_rel.max2 r b1 b2 ∧ (a1,b1) ∈ r - Id ∨
wo_rel.max2 r a1 a2 = wo_rel.max2 r b1 b2 ∧ a1 = b1 ∧ (a2,b2) ∈ r - Id"
using * unfolding bsqr_def by auto
have 2: "b1 = c1 ∧ b2 = c2 ∨ (wo_rel.max2 r b1 b2, wo_rel.max2 r c1 c2) ∈ r - Id ∨
wo_rel.max2 r b1 b2 = wo_rel.max2 r c1 c2 ∧ (b1,c1) ∈ r - Id ∨
wo_rel.max2 r b1 b2 = wo_rel.max2 r c1 c2 ∧ b1 = c1 ∧ (b2,c2) ∈ r - Id"
using ** unfolding bsqr_def by auto
show "((a1,a2),(c1,c2)) ∈ bsqr r"
proof-
{assume Case1: "a1 = b1 ∧ a2 = b2"
hence ?thesis using ** by simp
}
moreover
{assume Case2: "(wo_rel.max2 r a1 a2, wo_rel.max2 r b1 b2) ∈ r - Id"
{assume Case21: "b1 = c1 ∧ b2 = c2"
hence ?thesis using * by simp
}
moreover
{assume Case22: "(wo_rel.max2 r b1 b2, wo_rel.max2 r c1 c2) ∈ r - Id"
hence "(wo_rel.max2 r a1 a2, wo_rel.max2 r c1 c2) ∈ 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 ∧ (a1,b1) ∈ r - Id"
{assume Case31: "b1 = c1 ∧ b2 = c2"
hence ?thesis using * by simp
}
moreover
{assume Case32: "(wo_rel.max2 r b1 b2, wo_rel.max2 r c1 c2) ∈ 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 ∧ (b1,c1) ∈ r - Id"
hence "(a1,c1) ∈ 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 ∧ 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 ∧ a1 = b1 ∧ (a2,b2) ∈ r - Id"
{assume Case41: "b1 = c1 ∧ b2 = c2"
hence ?thesis using * by simp
}
moreover
{assume Case42: "(wo_rel.max2 r b1 b2, wo_rel.max2 r c1 c2) ∈ 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 ∧ (b1,c1) ∈ 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 ∧ b1 = c1 ∧ (b2,c2) ∈ r - Id"
hence "(a2,c2) ∈ 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: "∀a b. ¬((a,b) ∈ r - Id ∧ (b,a) ∈ 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)) ∈ bsqr r" and **: "((b1,b2),(a1,a2)) ∈ bsqr r"
hence "{a1,a2,b1,b2} ≤ Field r" unfolding bsqr_def by auto
moreover
have "a1 = b1 ∧ a2 = b2 ∨ (wo_rel.max2 r a1 a2, wo_rel.max2 r b1 b2) ∈ r - Id ∨
wo_rel.max2 r a1 a2 = wo_rel.max2 r b1 b2 ∧ (a1,b1) ∈ r - Id ∨
wo_rel.max2 r a1 a2 = wo_rel.max2 r b1 b2 ∧ a1 = b1 ∧ (a2,b2) ∈ r - Id"
using * unfolding bsqr_def by auto
moreover
have "b1 = a1 ∧ b2 = a2 ∨ (wo_rel.max2 r b1 b2, wo_rel.max2 r a1 a2) ∈ r - Id ∨
wo_rel.max2 r b1 b2 = wo_rel.max2 r a1 a2 ∧ (b1,a1) ∈ r - Id ∨
wo_rel.max2 r b1 b2 = wo_rel.max2 r a1 a2 ∧ b1 = a1 ∧ (b2,a2) ∈ r - Id"
using ** unfolding bsqr_def by auto
ultimately show "a1 = b1 ∧ a2 = b2"
using IrrS by auto
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: "∀a ∈ Field r. ∀b ∈ Field r. (a,b) ∈ r ∨ (b,a) ∈ r"
using wo_rel.TOTALS by auto
(* Main proof *)
{fix a1 a2 b1 b2 assume "{(a1,a2), (b1,b2)} ≤ Field(bsqr r)"
hence 0: "a1 ∈ Field r ∧ a2 ∈ Field r ∧ b1 ∈ Field r ∧ b2 ∈ Field r"
using Field_bsqr by blast
have "((a1,a2) = (b1,b2) ∨ ((a1,a2),(b1,b2)) ∈ bsqr r ∨ ((b1,b2),(a1,a2)) ∈ 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) ∈ 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) ∈ 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) ∈ r - Id ∨ (b2,a2) ∈ 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) ∈ r - Id ∨ (b1,a1) ∈ 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) ∈ 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) ∈ r - Id ∨ (b1,a2) ∈ 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) ∈ r - Id ∨ (b1,a1) ∈ 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) ∈ r - Id ∨ (b2,a2) ∈ 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) ∈ 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) ∈ 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) ∈ r - Id ∨ (b2,a1) ∈ 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) ∈ r - Id ∨ (b1,a1) ∈ 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) ∈ r - Id ∨ (b2,a2) ∈ 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) ∈ 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) ∈ r - Id ∨ (b1,a1) ∈ 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) ∈ r - Id ∨ (b2,a2) ∈ 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: "∀A ≤ Field r. A ≠ {} ⟶ (∃a ∈ A. ∀a' ∈ A. (a,a') ∈ r)"
using assms well_order_on_def Linear_order_Well_order_iff by blast
fix D assume *: "D ≤ Field (bsqr r)" and **: "D ≠ {}"
hence 1: "D ≤ Field r × Field r" unfolding Field_bsqr by simp
(*  *)
obtain M where M_def: "M = {wo_rel.max2 r a1 a2| a1 a2. (a1,a2) ∈ D}" by blast
have "M ≠ {}" using 1 M_def ** by auto
moreover
have "M ≤ 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 ∈ M ∧ (∀a ∈ M. (m,a) ∈ r)"
using 0 by blast
(*  *)
obtain A1 where A1_def: "A1 = {a1. ∃a2. (a1,a2) ∈ D ∧ wo_rel.max2 r a1 a2 = m}" by blast
have "A1 ≤ Field r" unfolding A1_def using 1 by auto
moreover have "A1 ≠ {}" unfolding A1_def using m_min unfolding M_def by blast
ultimately obtain a1 where a1_min: "a1 ∈ A1 ∧ (∀a ∈ A1. (a1,a) ∈ r)"
using 0 by blast
(*  *)
obtain A2 where A2_def: "A2 = {a2. (a1,a2) ∈ D ∧ wo_rel.max2 r a1 a2 = m}" by blast
have "A2 ≤ Field r" unfolding A2_def using 1 by auto
moreover have "A2 ≠ {}" unfolding A2_def
using m_min a1_min unfolding A1_def M_def by blast
ultimately obtain a2 where a2_min: "a2 ∈ A2 ∧ (∀a ∈ A2. (a2,a) ∈ 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) ∈ D" using a2_min unfolding A2_def by auto
(*  *)
moreover
{fix b1 b2 assume ***: "(b1,b2) ∈ D"
hence 4: "{a1,a2,b1,b2} ≤ Field r" using 1 3 by blast
have 5: "(wo_rel.max2 r a1 a2, wo_rel.max2 r b1 b2) ∈ r"
using *** a1_min a2_min m_min unfolding A1_def A2_def M_def by auto
have "((a1,a2),(b1,b2)) ∈ bsqr r"
proof(cases "wo_rel.max2 r a1 a2 = wo_rel.max2 r b1 b2")
assume Case1: "wo_rel.max2 r a1 a2 ≠ 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 ∈ A1" unfolding A1_def using 2 *** by auto
hence 6: "(a1,b1) ∈ r" using a1_min by auto
show ?thesis
proof(cases "a1 = b1")
assume Case21: "a1 ≠ b1"
thus ?thesis unfolding bsqr_def using 4 Case2 6 by auto
next
assume Case22: "a1 = b1"
hence "b2 ∈ A2" unfolding A2_def using 2 *** Case2 by auto
hence 7: "(a2,b2) ∈ r" using a2_min by auto
thus ?thesis unfolding bsqr_def using 4 7 Case2 Case22 by auto
qed
qed
}
(*  *)
ultimately show "∃d ∈ D. ∀d' ∈ D. (d,d') ∈ bsqr r" by fastforce
qed

lemma bsqr_max2:
assumes WELL: "Well_order r" and LEQ: "((a1,a2),(b1,b2)) ∈ bsqr r"
shows "(wo_rel.max2 r a1 a2, wo_rel.max2 r b1 b2) ∈ r"
proof-
have "{(a1,a2),(b1,b2)} ≤ Field(bsqr r)"
using LEQ unfolding Field_def by auto
hence "{a1,a2,b1,b2} ≤ Field r" unfolding Field_bsqr by auto
hence "{wo_rel.max2 r a1 a2, wo_rel.max2 r b1 b2} ≤ 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) ∈ r ∨ 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 × Field r" and
NE: "¬ (∃a. Field r = under r a)"
shows "∃A. wo_rel.ofilter r A ∧ A < Field r ∧ D ≤ A × 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' ∧ 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) ∈ 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} ≤ Field r" unfolding Field_bsqr by auto
let ?m = "wo_rel.max2 r a1 a2"
have "D ≤ (under r ?m) × (under r ?m)"
proof(unfold 1)
{fix b1 b2
let ?n = "wo_rel.max2 r b1 b2"
assume "(b1,b2) ∈ underS ?r' (a1,a2)"
hence 3: "((b1,b2),(a1,a2)) ∈ ?r'"
unfolding underS_def by blast
hence "(?n,?m) ∈ r" using WELL by (simp add: bsqr_max2)
moreover
{have "(b1,b2) ∈ Field ?r'" using 3 unfolding Field_def by auto
hence "{b1,b2} ≤ Field r" unfolding Field_bsqr by auto
hence "(b1,?n) ∈ r ∧ (b2,?n) ∈ r"
using Well by (simp add: wo_rel.max2_greater)
}
ultimately have "(b1,?m) ∈ r ∧ (b2,?m) ∈ r"
using Trans trans_def[of r] by blast
hence "(b1,b2) ∈ (under r ?m) × (under r ?m)" unfolding under_def by simp}
thus "underS ?r' (a1,a2) ≤ (under r ?m) × (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 . (∀ a ∈ A. f a ∈ B) ∧ (∀ a. a ∉ A ⟶ f a = undefined)}"

lemma Func_empty:
"Func {} B = {λx. undefined}"
unfolding Func_def by auto

lemma Func_elim:
assumes "g ∈ Func A B" and "a ∈ A"
shows "∃ b. b ∈ B ∧ g a = b"
using assms unfolding Func_def by (cases "g a = undefined") auto

definition curr where
"curr A f ≡ λ a. if a ∈ A then λb. f (a,b) else undefined"

lemma curr_in:
assumes f: "f ∈ Func (A × B) C"
shows "curr A f ∈ Func A (Func B C)"
using assms unfolding curr_def Func_def by auto

lemma curr_inj:
assumes "f1 ∈ Func (A × B) C" and "f2 ∈ Func (A × B) C"
shows "curr A f1 = curr A f2 ⟷ 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) ∈ A × B")
case False
thus ?thesis using assms unfolding Func_def by auto
next
case True hence a: "a ∈ A" and b: "b ∈ 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 ∈ Func A (Func B C)"
shows "∃ f ∈ Func (A × B) C. curr A f = g"
proof
let ?f = "λ ab. if fst ab ∈ A ∧ snd ab ∈ 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 ∈ 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 ∈ 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 ∈ Func (A × B) C" using assms unfolding Func_def mem_Collect_eq by auto
qed

lemma bij_betw_curr:
"bij_betw (curr A) (Func (A × B) C) (Func A (Func B C))"
unfolding bij_betw_def inj_on_def
using curr_surj curr_in curr_inj by blast

definition Func_map where
"Func_map B2 f1 f2 g b2 ≡ if b2 ∈ B2 then f1 (g (f2 b2)) else undefined"

lemma Func_map:
assumes g: "g ∈ Func A2 A1" and f1: "f1  A1 ⊆ B1" and f2: "f2  B2 ⊆ A2"
shows "Func_map B2 f1 f2 g ∈ Func B2 B1"
using assms unfolding Func_def Func_map_def mem_Collect_eq by auto

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

lemma Func_is_emp:
"Func A B = {} ⟷ A ≠ {} ∧ B = {}" (is "?L ⟷ ?R")
proof
assume ?L
then show ?R
using Func_empty Func_non_emp[of B A] by blast
next
assume ?R
then show ?L
using Func_empty Func_non_emp[of B A] by (auto simp: Func_def)
qed

lemma Func_map_surj:
assumes B1: "f1  A1 = B1" and A2: "inj_on f2 B2" "f2  B2 ⊆ A2"
and B2A2: "B2 = {} ⟹ A2 = {}"
shows "Func B2 B1 = Func_map B2 f1 f2  Func A2 A1"
proof(cases "B2 = {}")