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