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"
  by (simp add: index_def find_index_less_size)

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)"
  by (simp add: sym_trancl transymcl_def)

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
(*>*)