# Theory Preliminaries

```section ‹Preliminaries›

(*<*)
theory Preliminaries
imports "List-Index.List_Index"
begin
(*>*)

subsection ‹Iterated Function Update›

abbreviation fun_upds ("_[_ :=⇧* _]" [90, 0, 0] 91) where
"f[xs :=⇧* ys] ≡ fold (λ(x, y) f. f(x := y)) (zip xs ys) f"

fun restrict where
"restrict A (x # xs) (y # ys) = (if x ∈ A then y # restrict (A - {x}) xs ys else restrict A xs ys)"
| "restrict A _ _ = []"

fun extend :: "nat set ⇒ nat list ⇒ 'a list ⇒ 'a list set" where
"extend A (x # xs) ys = (if x ∈ A
then (⋃zs ∈ extend (A - {x}) xs (tl ys). {hd ys # zs})
else (⋃z ∈ UNIV. ⋃zs ∈ extend A xs ys. {z # zs}))"
| "extend A _ _ = {[]}"

fun lookup where
"lookup (x # xs) (y # ys) z = (if x = z then y else lookup xs ys z)"
| "lookup _ _ _ = undefined"

lemma extend_nonempty: "extend A xs ys ≠ {}"
by (induct xs arbitrary: A ys) auto

lemma length_extend: "zs ∈ extend A xs ys ⟹ length zs = length xs"
by (induct xs arbitrary: A ys zs) (auto split: if_splits)

lemma ex_lookup_extend: "x ∉ A ⟹ x ∈ set xs ⟹ ∃zs ∈ extend A xs ys. lookup xs zs x = d"
proof (induct xs arbitrary: A ys)
case (Cons a xs)
from Cons(1)[of "A - {a}" "tl ys"] Cons(1)[of A ys] Cons(2-) show ?case
by (auto simp: ex_in_conv extend_nonempty)
qed simp

lemma restrict_extend: "A ⊆ set xs ⟹ length ys = card A ⟹ zs ∈ extend A xs ys ⟹ restrict A xs zs = ys"
proof (induct xs arbitrary: A ys zs)
case (Cons a xs)
then have "finite A"
by (elim finite_subset) auto
with Cons(1)[of "A - {a}" "tl ys" "tl zs"] Cons(1)[of A ys "tl zs"] Cons(2-) show ?case
by (cases ys) (auto simp: subset_insert_iff split: if_splits)
qed simp

lemma fun_upds_notin[simp]: "length xs = length ys ⟹ x ∉ set xs ⟹ (σ[xs :=⇧* ys]) x = σ x"
by (induct xs ys arbitrary: σ rule: list_induct2) auto

lemma fun_upds_twist: "length xs = length ys ⟹ a ∉ set xs ⟹ σ(a := x)[xs :=⇧* ys] = (σ[xs :=⇧* ys])(a := x)"
by (induct xs ys arbitrary: σ rule: list_induct2) (auto simp: fun_upd_twist)

lemma fun_upds_twist_apply: "length xs = length ys ⟹ a ∉ set xs ⟹ a ≠ b ⟹ (σ(a := x)[xs :=⇧* ys]) b = (σ[xs :=⇧* ys]) b"
by (induct xs ys arbitrary: σ rule: list_induct2) (auto simp: fun_upd_twist)

lemma fun_upds_extend:
"x ∈ A ⟹ A ⊆ set xs ⟹ distinct xs ⟹ sorted xs ⟹ length ys = card A ⟹ zs ∈ extend A xs ys ⟹
(σ[xs :=⇧* zs]) x = (σ[sorted_list_of_set A :=⇧* ys]) x"
proof (induct xs arbitrary: A ys zs σ)
case (Cons a xs)
then have fin[simp]: "finite A"
by (elim finite_subset) auto
from Cons(2-) have "a ∈ A ⟹ Min A = a" if "a ∈ A"
by (intro Min_eqI) auto
with Cons(2) fin have *: "a ∈ A ⟹ sorted_list_of_set A = a # sorted_list_of_set (A - {a})"
by (subst sorted_list_of_set_nonempty) auto
show ?case
using Cons(1)[of "A - {a}" "tl ys"] Cons(1)[of A ys] Cons(2-)
by (cases ys; cases "x = a")
(auto simp add: subset_insert_iff * fun_upds_twist_apply length_extend simp del: fun_upd_apply split: if_splits)
qed simp

lemma fun_upds_map_self: "σ[xs :=⇧* map σ xs] = σ"
by (induct xs arbitrary: σ) auto

lemma fun_upds_single: "distinct xs ⟹ σ[xs :=⇧* map (σ(y := d)) xs] = (if y ∈ set xs then σ(y := d) else σ)"
by (induct xs arbitrary: σ) (auto simp: fun_upds_twist)

subsection ‹Lists and Sets›

lemma find_index_less_size: "∃x ∈ set xs. P x ⟹ find_index P xs < size xs"
by (induct xs) auto

lemma index_less_size: "x ∈ set xs ⟹ index xs x < size xs"

lemma fun_upds_in: "length xs = length ys ⟹ distinct xs ⟹ x ∈ set xs ⟹ (σ[xs :=⇧* ys]) x = ys ! index xs x"
by (induct xs ys arbitrary: σ rule: list_induct2) auto

lemma remove_nth_index: "remove_nth (index ys y) ys = remove1 y ys"
by (induct ys) auto

lemma index_remove_nth: "distinct xs ⟹ x ∈ set xs ⟹ index (remove_nth i xs) x = (if index xs x < i then index xs x else if i = index xs x then length xs - 1 else index xs x - 1)"
by (induct i xs rule: remove_nth.induct) (auto simp: not_less intro!: Suc_pred split: if_splits)

lemma insert_nth_nth_index:
"y ≠ z ⟹ y ∈ set ys ⟹ z ∈ set ys ⟹ length ys = Suc (length xs) ⟹ distinct ys ⟹
insert_nth (index ys y) x xs ! index ys z =
xs ! index (remove1 y ys) z"
by (subst nth_insert_nth;
auto simp: remove_nth_index[symmetric] index_remove_nth dest: index_less_size intro!: arg_cong[of _ _ "nth xs"] index_eqI)

lemma index_lt_index_remove: "index xs x < index xs y ⟹ index xs x = index (remove1 y xs) x"
by (induct xs) auto

lemma index_gt_index_remove: "index xs x > index xs y ⟹ index xs x = Suc (index (remove1 y xs) x)"
proof (induct xs)
case (Cons z xs)
then show ?case
by (cases "z = x") auto
qed simp

lemma lookup_map[simp]: "x ∈ set xs ⟹ lookup xs (map f xs) x = f x"
by (induct xs) auto

lemma in_set_remove_cases: "P z ⟹ (∀x ∈ set (remove1 z xs). P x) ⟹ x ∈ set xs ⟹ P x"
by (cases "x = z") auto

lemma insert_remove_id: "x ∈ X ⟹ X = insert x (X - {x})"
by auto

lemma infinite_surj: "infinite A ⟹ A ⊆ f ` B ⟹ infinite B"
by (elim contrapos_nn finite_surj)

class infinite =
fixes to_nat :: "'a ⇒ nat"
assumes surj_to_nat: "surj to_nat"
begin

lemma infinite_UNIV: "infinite (UNIV :: 'a set)"
using surj_to_nat by (intro infinite_surj[of UNIV to_nat]) auto

end

instantiation nat :: infinite begin
definition to_nat_nat :: "nat ⇒ nat" where "to_nat_nat = id"
instance by standard (auto simp: to_nat_nat_def)
end

instantiation list :: (type) infinite begin
definition to_nat_list :: "'a list ⇒ nat" where "to_nat_list = length"
instance by standard (auto simp: image_iff to_nat_list_def intro!: exI[of _ "replicate _ _"])
end

subsection ‹Equivalence Closure and Classes›

definition symcl where
"symcl r = {(x, y). (x, y) ∈ r ∨ (y, x) ∈ r}"

definition transymcl where
"transymcl r = trancl (symcl r)"

lemma symclp_symcl_eq[pred_set_conv]: "symclp (λx y. (x, y) ∈ r) = (λx y. (x, y) ∈ symcl r)"
by (auto simp: symclp_def symcl_def fun_eq_iff)

definition "classes Qeq = quotient (Field Qeq) (transymcl Qeq)"

lemma Field_symcl[simp]: "Field (symcl r) = Field r"
unfolding symcl_def Field_def by auto

lemma Domain_symcl[simp]: "Domain (symcl r) = Field r"
unfolding symcl_def Field_def by auto

lemma Field_trancl[simp]: "Field (trancl r) = Field r"
unfolding Field_def by auto

lemma Field_transymcl[simp]: "Field (transymcl r) = Field r"
unfolding transymcl_def by auto

lemma eqclass_empty_iff[simp]: "r `` {x} = {} ⟷ x ∉ Domain r"
by auto

lemma sym_symcl[simp]: "sym (symcl r)"
unfolding symcl_def sym_def by auto

lemma in_symclI:
"(a,b) ∈ r ⟹ (a,b) ∈ symcl r"
"(a,b) ∈ r ⟹ (b,a) ∈ symcl r"
by (auto simp: symcl_def)

lemma sym_transymcl: "sym (transymcl r)"

lemma symcl_insert:
"symcl (insert (x, y) Qeq) = insert (y, x) (insert (x, y) (symcl Qeq))"
by (auto simp: symcl_def)

lemma equiv_transymcl: "Equiv_Relations.equiv (Field Qeq) (transymcl Qeq)"
by (auto simp: Equiv_Relations.equiv_def sym_trancl refl_on_def transymcl_def
dest: FieldI1 FieldI2 Field_def[THEN equalityD1, THEN set_mp]
intro: r_r_into_trancl[of x _ _ x for x]  elim!: in_symclI)

lemma equiv_quotient_no_empty_class: "Equiv_Relations.equiv A r ⟹ {} ∉ A // r"
by (auto simp: quotient_def refl_on_def sym_def Equiv_Relations.equiv_def)

lemma classes_cover: "⋃(classes Qeq) = Field Qeq"
by (simp add: Union_quotient classes_def equiv_transymcl)

lemma classes_disjoint: "X ∈ classes Qeq ⟹ Y ∈ classes Qeq ⟹ X = Y ∨ X ∩ Y = {}"
using quotient_disj[OF equiv_transymcl]
by (auto simp: classes_def)

lemma classes_nonempty: "{} ∉ classes Qeq"
using equiv_quotient_no_empty_class[OF equiv_transymcl]
by (auto simp: classes_def)

definition "class x Qeq = (if ∃X ∈ classes Qeq. x ∈ X then Some (THE X. X ∈ classes Qeq ∧ x ∈ X) else None)"

lemma class_Some_eq: "class x Qeq = Some X ⟷ X ∈ classes Qeq ∧ x ∈ X"
unfolding class_def
by (auto 0 3 dest: classes_disjoint del: conjI intro!: the_equality[of _ X]
conjI[of "(∃X∈classes Qeq. x ∈ X)"] intro: theI[where P="λX. X ∈ classes Qeq ∧ x ∈ X"])

lemma class_None_eq: "class x Qeq = None ⟷ x ∉ Field Qeq"
by (simp add: class_def classes_cover[symmetric] split: if_splits)

lemma insert_Image_triv: "x ∉ r ⟹ insert (x, y) Qeq `` r = Qeq `` r"
by auto

lemma Un1_Image_triv: "Domain B ∩ r = {} ⟹ (A ∪ B) `` r = A `` r"
by auto

lemma Un2_Image_triv: "Domain A ∩ r = {} ⟹ (A ∪ B) `` r = B `` r"
by auto

lemma classes_empty: "classes {} = {}"
unfolding classes_def by auto

lemma ex_class: "x ∈ Field Qeq ⟹ ∃X. class x Qeq = Some X ∧ x ∈ X"
by (metis Union_iff class_Some_eq classes_cover)

lemma equivD:
"Equiv_Relations.equiv A r ⟹ refl_on A r"
"Equiv_Relations.equiv A r ⟹ sym r"
"Equiv_Relations.equiv A r ⟹ trans r"
by (blast elim: Equiv_Relations.equivE)+

lemma transymcl_into:
"(x, y) ∈ r ⟹ (x, y) ∈ transymcl r"
"(x, y) ∈ r ⟹ (y, x) ∈ transymcl r"
unfolding transymcl_def by (blast intro: in_symclI r_into_trancl')+

lemma transymcl_self:
"(x, y) ∈ r ⟹ (x, x) ∈ transymcl r"
"(x, y) ∈ r ⟹ (y, y) ∈ transymcl r"
unfolding transymcl_def by (blast intro: in_symclI(1) in_symclI(2) r_r_into_trancl)+

lemma transymcl_trans: "(x, y) ∈ transymcl r ⟹ (y, z) ∈ transymcl r ⟹ (x, z) ∈ transymcl r"
using equiv_transymcl[THEN equivD(3), THEN transD] .

lemma transymcl_sym: "(x, y) ∈ transymcl r ⟹ (y, x) ∈ transymcl r"
using equiv_transymcl[THEN equivD(2), THEN symD] .

lemma edge_same_class: "X ∈ classes Qeq ⟹ (a, b) ∈ Qeq ⟹ a ∈ X ⟷ b ∈ X"
unfolding classes_def by (elim quotientE) (auto elim!: transymcl_trans transymcl_into)

lemma Field_transymcl_self: "a ∈ Field Qeq ⟹ (a, a) ∈ transymcl Qeq"
by (auto simp: Field_def transymcl_def[symmetric] transymcl_self)

lemma transymcl_insert: "transymcl (insert (a, b) Qeq) = transymcl Qeq ∪ {(a,a),(b,b)} ∪
((transymcl Qeq ∪ {(a, a), (b, b)}) O {(a, b), (b, a)} O (transymcl Qeq ∪ {(a, a), (b, b)}) - transymcl Qeq)"
by (auto simp: relcomp_def relcompp_apply transymcl_def symcl_insert trancl_insert2 dest: trancl_trans)

lemma transymcl_insert_both_new: "a ∉ Field Qeq ⟹ b ∉ Field Qeq ⟹
transymcl (insert (a, b) Qeq) = transymcl Qeq ∪ {(a,a),(b,b),(a,b),(b,a)}"
unfolding transymcl_insert
by (auto dest: FieldI1 FieldI2)

lemma transymcl_insert_same_class: "(x, y) ∈ transymcl Qeq ⟹ transymcl (insert (x, y) Qeq) = transymcl Qeq"
by (auto 0 3 simp: transymcl_insert intro: transymcl_sym transymcl_trans)

lemma classes_insert: "classes (insert (x, y) Qeq) =
(case (class x Qeq, class y Qeq) of
(Some X, Some Y) ⇒ if X = Y then classes Qeq else classes Qeq - {X, Y} ∪ {X ∪ Y}
| (Some X, None) ⇒ classes Qeq - {X} ∪ {insert y X}
| (None, Some Y) ⇒ classes Qeq - {Y} ∪ {insert x Y}
| (None, None) ⇒ classes Qeq ∪ {{x,y}})"
proof ((cases "class x Qeq"; cases "class y Qeq"), goal_cases NN NS SN SS)
case NN
then have "classes (insert (x, y) Qeq) = classes Qeq ∪ {{x, y}}"
by (fastforce simp: class_None_eq classes_def transymcl_insert_both_new insert_Image_triv quotientI
elim!: quotientE dest: FieldI1  intro: quotient_def[THEN Set.equalityD2, THEN set_mp] intro!: disjI1)
with NN show ?case
by auto
next
case (NS Y)
then have "insert x Y = transymcl (insert (x, y) Qeq) `` {x}"
unfolding transymcl_insert using FieldI1[of x _ "transymcl Qeq"]
relcompI[OF insertI1 relcompI[OF insertI1 insertI2[OF insertI2[OF transymcl_trans[OF transymcl_sym]]]],
of _ y Qeq _ x x "insert (y,y) (transymcl Qeq)" "{(y,x)}" "(x, x)" "(y, y)"]
by (auto simp: class_None_eq class_Some_eq classes_def
dest: FieldI1 FieldI2 elim!: quotientE intro: transymcl_sym transymcl_trans)
then have *: "insert x Y ∈ classes (insert (x, y) Qeq)"
by (auto simp: class_None_eq class_Some_eq classes_def  intro!: quotientI)
moreover from * NS have "Y ∉ classes (insert (x, y) Qeq)"
using classes_disjoint[of Y "insert (x, y) Qeq" "insert x Y"] classes_cover[of Qeq]
by (auto simp: class_None_eq class_Some_eq)
moreover {
fix Z
assume Z: "Z ≠ Y" "Z ∈ classes Qeq"
then obtain z where z: "z ∈ Field Qeq" "Z = transymcl Qeq `` {z}"
by (auto elim!: quotientE simp: classes_def)
with NS Z have "z ∈ Z" "z ≠ x" "z ≠ y" "(z, x) ∉ transymcl Qeq" "(z, y) ∉ transymcl Qeq"
using classes_disjoint[of Z "Qeq" Y] classes_nonempty[of Qeq]
by (auto simp: class_None_eq class_Some_eq disjoint_iff Field_transymcl_self
dest: FieldI2 intro: transymcl_trans)
with NS Z * have "transymcl Qeq `` {z} = transymcl (insert (x, y) Qeq) `` {z}"
unfolding transymcl_insert
by (intro trans[OF _ Un1_Image_triv[symmetric]]) (auto simp: class_None_eq class_Some_eq)
with z have "Z ∈ classes (insert (x, y) Qeq)"
by (auto simp: classes_def intro!: quotientI)
}
moreover {
fix Z
assume Z: "Z ≠ insert x Y" "Z ∈ classes (insert (x, y) Qeq)"
then obtain z where z: "z ∈ Field (insert (x, y) Qeq)" "Z = transymcl (insert (x, y) Qeq) `` {z}"
by (auto elim!: quotientE simp: classes_def)
with NS Z * have "z ∈ Z" "z ≠ x" "z ≠ y" "(z, x) ∉ transymcl (insert (x, y) Qeq)" "(z, y) ∉ transymcl (insert (x, y) Qeq)"
using classes_disjoint[of Z "insert (x, y) Qeq" "insert x Y"] classes_nonempty[of "insert (x, y) Qeq"]
by (auto simp: class_None_eq class_Some_eq Field_transymcl_self transymcl_into(2)
intro: transymcl_trans)
with NS Z * have "transymcl (insert (x, y) Qeq) `` {z} = transymcl Qeq `` {z}"
unfolding transymcl_insert
by (intro trans[OF Un1_Image_triv]) (auto simp: class_None_eq class_Some_eq)
with z ‹z ≠ x› ‹z ≠ y› have "Z ∈ classes Qeq"
by (auto simp: classes_def intro!: quotientI)
}
ultimately have "classes (insert (x, y) Qeq) = classes Qeq - {Y} ∪ {insert x Y}"
by blast
with NS show ?case
by auto
next
case (SN X)
then have "insert y X = transymcl (insert (x, y) Qeq) `` {x}"
unfolding transymcl_insert using FieldI1[of x _ "transymcl Qeq"]
by (auto simp: class_None_eq class_Some_eq classes_def
dest: FieldI1 FieldI2 elim!: quotientE intro: transymcl_sym transymcl_trans)
then have *: "insert y X ∈ classes (insert (x, y) Qeq)"
by (auto simp: class_None_eq class_Some_eq classes_def  intro!: quotientI)
moreover from * SN have "X ∉ classes (insert (x, y) Qeq)"
using classes_disjoint[of X "insert (x, y) Qeq" "insert y X"] classes_cover[of Qeq]
by (auto simp: class_None_eq class_Some_eq)
moreover {
fix Z
assume Z: "Z ≠ X" "Z ∈ classes Qeq"
then obtain z where z: "z ∈ Field Qeq" "Z = transymcl Qeq `` {z}"
by (auto elim!: quotientE simp: classes_def)
with SN Z have "z ∈ Z" "z ≠ x" "z ≠ y" "(z, x) ∉ transymcl Qeq" "(z, y) ∉ transymcl Qeq"
using classes_disjoint[of Z "Qeq" X] classes_nonempty[of Qeq]
by (auto simp: class_None_eq class_Some_eq disjoint_iff Field_transymcl_self
dest: FieldI2 intro: transymcl_trans)
with SN Z * have "transymcl Qeq `` {z} = transymcl (insert (x, y) Qeq) `` {z}"
unfolding transymcl_insert
by (intro trans[OF _ Un1_Image_triv[symmetric]]) (auto simp: class_None_eq class_Some_eq)
with z have "Z ∈ classes (insert (x, y) Qeq)"
by (auto simp: classes_def intro!: quotientI)
}
moreover {
fix Z
assume Z: "Z ≠ insert y X" "Z ∈ classes (insert (x, y) Qeq)"
then obtain z where z: "z ∈ Field (insert (x, y) Qeq)" "Z = transymcl (insert (x, y) Qeq) `` {z}"
by (auto elim!: quotientE simp: classes_def)
with SN Z * have "z ∈ Z" "z ≠ x" "z ≠ y" "(z, x) ∉ transymcl (insert (x, y) Qeq)" "(z, y) ∉ transymcl (insert (x, y) Qeq)"
using classes_disjoint[of Z "insert (x, y) Qeq" "insert y X"] classes_nonempty[of "insert (x, y) Qeq"]
by (auto simp: class_None_eq class_Some_eq Field_transymcl_self transymcl_into(2)
intro: transymcl_trans)
with SN Z * have "transymcl (insert (x, y) Qeq) `` {z} = transymcl Qeq `` {z}"
unfolding transymcl_insert
by (intro trans[OF Un1_Image_triv]) (auto simp: class_None_eq class_Some_eq)
with z ‹z ≠ x› ‹z ≠ y› have "Z ∈ classes Qeq"
by (auto simp: classes_def intro!: quotientI)
}
ultimately have "classes (insert (x, y) Qeq) = classes Qeq - {X} ∪ {insert y X}"
by blast
with SN show ?case
by auto
next
case (SS X Y)
moreover from SS have XY: "X ∈ classes Qeq" "Y ∈ classes Qeq" "x ∈ X" "y ∈ Y" "x ∈ Field Qeq" "y ∈ Field Qeq"
using class_None_eq[of x Qeq] class_None_eq[of y Qeq] class_Some_eq[of x Qeq X] class_Some_eq[of y Qeq Y]
by auto
moreover from XY have "X = Y ⟹ classes (insert (x, y) Qeq) = classes Qeq"
unfolding classes_def
by (subst transymcl_insert_same_class)
(auto simp: classes_def insert_absorb elim!: quotientE intro: transymcl_sym transymcl_trans)
moreover
{
assume neq: "X ≠ Y"
from XY have "X = transymcl Qeq `` {x}" "Y = transymcl Qeq `` {y}"
by (auto simp: classes_def elim!: quotientE intro: transymcl_sym transymcl_trans)
with XY have XY_eq:
"X ∪ Y = transymcl (insert (x, y) Qeq) `` {x}"
"X ∪ Y = transymcl (insert (x, y) Qeq) `` {y}"
unfolding transymcl_insert by auto
then have *: "X ∪ Y ∈ classes (insert (x, y) Qeq)"
by (auto simp: classes_def quotientI)
moreover
from * XY neq have **: "X ∉ classes (insert (x, y) Qeq)" "Y ∉ classes (insert (x, y) Qeq)"
using classes_disjoint[OF *, of X] classes_disjoint[OF *, of Y] classes_disjoint[of X Qeq Y]
by auto
moreover {
fix Z
assume Z: "Z ≠ X" "Z ≠ Y" "Z ∈ classes Qeq"
then obtain z where z: "z ∈ Field Qeq" "Z = transymcl Qeq `` {z}"
by (auto elim!: quotientE simp: classes_def)
with XY Z have "z ∈ Z" "z ≠ x" "z ≠ y" "(z, x) ∉ transymcl Qeq" "(z, y) ∉ transymcl Qeq"
using classes_disjoint[of Z Qeq X] classes_disjoint[of Z Qeq Y] classes_nonempty[of Qeq]
by (auto simp: disjoint_iff Field_transymcl_self dest: FieldI2 intro: transymcl_trans)
with XY Z * have "transymcl Qeq `` {z} = transymcl (insert (x, y) Qeq) `` {z}"
unfolding transymcl_insert
by (intro trans[OF _ Un1_Image_triv[symmetric]]) (auto simp: class_None_eq class_Some_eq)
with z have "Z ∈ classes (insert (x, y) Qeq)"
by (auto simp: classes_def intro!: quotientI)
}
moreover {
fix Z
assume Z: "Z ≠ X ∪ Y" "Z ∈ classes (insert (x, y) Qeq)"
then obtain z where z: "z ∈ Field (insert (x, y) Qeq)" "Z = transymcl (insert (x, y) Qeq) `` {z}"
by (auto elim!: quotientE simp: classes_def)
with XY Z neq XY_eq have "z ∈ Z" "z ≠ x" "z ≠ y" "(z, x) ∉ transymcl (insert (x, y) Qeq)" "(z, y) ∉ transymcl (insert (x, y) Qeq)"
using classes_disjoint[OF *, of Z] classes_disjoint[of X Qeq Y]
by (auto simp: Field_transymcl_self)
with XY Z * have "transymcl (insert (x, y) Qeq) `` {z} = transymcl Qeq `` {z}"
unfolding transymcl_insert
by (intro trans[OF Un1_Image_triv]) (auto simp: class_None_eq class_Some_eq)
with z ‹z ≠ x› ‹z ≠ y› have "Z ∈ classes Qeq"
by (auto simp: classes_def intro!: quotientI)
}
ultimately have "classes (insert (x, y) Qeq) = classes Qeq - {X, Y} ∪ {X ∪ Y}"
by blast
}
ultimately show ?case
by auto
qed

lemma classes_intersect_find_not_None:
assumes "∀V∈classes (set xys). V ∩ A ≠ {}" "xys ≠ []"
shows "find (λ(x, y). x ∈ A ∨ y ∈ A) xys ≠ None"
proof -
from assms(2) obtain x y where "(x, y) ∈ set xys" by (cases xys) auto
with assms(1) obtain X where x: "class x (set xys) = Some X" "X ∩ A ≠ {}"
using ex_class[of "x" "set xys"]
by (auto simp: class_Some_eq Field_def)
then obtain a where "a ∈ A" "a ∈ X"
by blast
with x have "(a, x) ∈ transymcl (set xys)"
using equiv_class_eq[OF equiv_transymcl, of _ _ "set xys"]
by (fastforce simp: class_Some_eq classes_def elim!: quotientE)
then obtain b where "(a, b) ∈ symcl (set xys)"
by (auto simp: transymcl_def elim: converse_tranclE)
with ‹a ∈ A› show ?thesis
by (auto simp: find_None_iff symcl_def)
qed

(*<*)
end
(*>*)```