(* Title: FriendshipTheory.thy Author:Wenda Li *) theory FriendshipTheory imports MoreGraph "HOL-Number_Theory.Number_Theory" begin (*Proofs in this section are the common steps for both combinatorial and algebraic proofs for the Friendship Theorem*) section‹Common steps› definition (in valid_unSimpGraph) non_adj :: "'v ⇒ 'v ⇒ bool" where "non_adj v v' ≡ v∈V ∧ v'∈V ∧ v≠v' ∧ ¬adjacent v v'" lemma (in valid_unSimpGraph) no_quad: assumes "⋀v u. v∈V ⟹ u∈V ⟹ v≠u ⟹ ∃! n. adjacent v n ∧ adjacent u n" shows "¬ (∃v1 v2 v3 v4. v2≠v4 ∧ v1≠v3 ∧ adjacent v1 v2 ∧ adjacent v2 v3 ∧ adjacent v3 v4 ∧ adjacent v4 v1)" proof assume "∃v1 v2 v3 v4. v2≠v4 ∧ v1≠v3 ∧ adjacent v1 v2 ∧ adjacent v2 v3 ∧ adjacent v3 v4 ∧ adjacent v4 v1" then obtain v1 v2 v3 v4 where "v2≠v4" "v1≠v3" "adjacent v1 v2" "adjacent v2 v3" "adjacent v3 v4" "adjacent v4 v1" by auto hence "∃!n. adjacent v1 n ∧ adjacent v3 n" using assms[of v1 v3] by auto thus False by (metis ‹adjacent v1 v2› ‹adjacent v2 v3› ‹adjacent v3 v4› ‹adjacent v4 v1› ‹v2 ≠ v4› adjacent_sym) qed lemma even_card_set: assumes "finite A" and "∀x∈A. f x∈A ∧ f x≠ x ∧ f (f x)=x" shows "even(card A)" using assms proof (induct "card A" arbitrary:A rule:less_induct) case less have "A={}⟹?case" by auto moreover have "A≠{}⟹?case" proof - assume "A≠{}" then obtain x where "x∈A" by auto hence "f x∈A" and "f x≠x" by (metis less.prems(2))+ obtain B where B:"B=A-{x,f x}" by auto hence "finite B" using ‹finite A› by auto moreover have "card B<card A" using B ‹finite A› by (metis Diff_insert ‹f x ∈ A› ‹x ∈ A› card_Diff2_less) moreover have "∀x∈B. f x ∈ B ∧ f x ≠ x ∧ f (f x) = x" proof fix y assume "y∈B" hence "y∈A" using B by auto hence "f y≠y" and "f (f y)=y" by (metis less.prems(2))+ moreover have "f y∈B" proof (rule ccontr) assume "f y∉B" have "f y∈A" by (metis ‹y ∈ A› less.prems(2)) hence "f y∈{x, f x}" by (metis B DiffI ‹f y ∉ B›) moreover have "f y=x ⟹ False" by (metis B Diff_iff Diff_insert2 ‹f (f y) = y› ‹y ∈ B› singleton_iff) moreover have "f y= f x⟹ False" by (metis B Diff_iff ‹x ∈ A› ‹y ∈ B› insertCI less.prems(2)) ultimately show False by auto qed ultimately show "f y ∈ B ∧ f y ≠ y ∧ f (f y) = y" by auto qed ultimately have "even (card B)" by (metis (full_types) less.hyps) moreover have "{x,f x}⊆A" using ‹f x∈A› ‹x∈A› by auto moreover have "card {x, f x} = 2" using ‹f x≠x› by auto ultimately show ?case using B ‹finite A› card_mono [of A "{x, f x}"] by (simp add: card_Diff_subset) qed ultimately show ?case by metis qed lemma (in valid_unSimpGraph) even_degree: assumes friend_assm:"⋀v u. v∈V ⟹ u∈V ⟹ v≠u ⟹ ∃! n. adjacent v n ∧ adjacent u n" and "finite E" shows "∀v∈V. even(degree v G)" proof fix v assume "v∈V" obtain f where f:"f = (λn. (SOME v'. n∈V ⟶n≠v⟶adjacent n v' ∧ adjacent v v'))" by auto have "⋀n. n∈V ⟶ n≠v ⟶ (∃v'. adjacent n v' ∧ adjacent v v')" proof (rule,rule) fix n assume "n ∈ V" "n ≠ v" hence "∃!v'. adjacent n v' ∧ adjacent v v'" using friend_assm[of n v] ‹v∈V› unfolding non_adj_def by auto thus "∃v'. adjacent n v' ∧ adjacent v v'" by auto qed hence f_ex:"⋀n. (∃v'. n∈V ⟶ n≠v ⟶ adjacent n v' ∧ adjacent v v')" by auto have "∀x∈{n. adjacent v n}. f x∈{n. adjacent v n} ∧ f x≠ x ∧ f (f x)=x" proof fix x assume "x ∈ {n. adjacent v n}" hence "adjacent v x" by auto have "f x∈{n. adjacent v n}" using someI_ex[OF f_ex,of x] by (metis ‹adjacent v x› adjacent_V(2) adjacent_no_loop f mem_Collect_eq) moreover have "f x≠x" using someI_ex[OF f_ex,of x] by (metis ‹adjacent v x› adjacent_V(2) adjacent_no_loop f) moreover have "f (f x)=x" proof (rule ccontr) assume "f (f x)≠x" have "adjacent (f x) (f (f x))" using someI_ex[OF f_ex,of "f x"] by (metis (full_types) adjacent_V(2) adjacent_no_loop calculation(1) f mem_Collect_eq) moreover have "adjacent (f (f x)) v" using someI_ex[OF f_ex,of "f x"] by (metis adjacent_V(1) adjacent_sym calculation f) moreover have "adjacent x (f x)" using someI_ex[OF f_ex,of x] by (metis ‹adjacent v x› adjacent_V(2) adjacent_no_loop f) moreover have "v≠f x" by (metis ‹f x ∈ {n. adjacent v n}› adjacent_no_loop mem_Collect_eq) ultimately show False using no_quad[OF friend_assm] using ‹adjacent v x› ‹f (f x)≠x› by metis qed ultimately show "f x ∈ {n. adjacent v n} ∧ f x ≠ x ∧ f (f x) = x" by auto qed moreover have "finite {n. adjacent v n}" by (metis adjacent_finite assms(2)) ultimately have "even (card {n. adjacent v n})" using even_card_set[of "{n. adjacent v n}" f] by auto thus "even(degree v G)" by (metis assms(2) degree_adjacent) qed lemma (in valid_unSimpGraph) degree_two_windmill: assumes friend_assm:"⋀v u. v∈V ⟹ u∈V ⟹ v≠u ⟹ ∃! n. adjacent v n ∧ adjacent u n" and "finite E" and "card V≥2" shows "(∃v∈V. degree v G = 2) ⟷(∃v. ∀n∈V. n≠v ⟶ adjacent v n)" proof assume "∃v∈V. degree v G = 2 " then obtain v where "degree v G=2" by auto hence "card {n. adjacent v n}=2" using degree_adjacent[OF ‹finite E›,of v] by auto then obtain v1 v2 where v1v2:"{n. adjacent v n}={v1,v2}" and "v1≠v2" proof - obtain v1 S where "{n. adjacent v n} = insert v1 S" and "v1 ∉ S" and "card S = 1" using ‹card {n. adjacent v n}=2› card_Suc_eq[of "{n. adjacent v n}" 1] by auto then obtain v2 where "S=insert v2 {}" using card_Suc_eq[of S 0] by auto hence "{n. adjacent v n}={v1,v2}" and "v1≠v2" using ‹{n. adjacent v n} = insert v1 S› ‹v1 ∉ S› by auto thus ?thesis using that[of v1 v2] by auto qed have "adjacent v1 v2" proof - obtain n where "adjacent v n" "adjacent v1 n" using friend_assm[of v v1] by (metis (full_types) adjacent_V(2) adjacent_sym insertI1 mem_Collect_eq v1v2) hence "n∈{n. adjacent v n}" by auto moreover have "n≠v1" by (metis ‹adjacent v1 n› adjacent_no_loop) ultimately have "n=v2" using v1v2 by auto thus ?thesis by (metis ‹adjacent v1 n›) qed have v1v2_adj:"∀x∈V. x∈{n. adjacent v1 n} ∪ {n. adjacent v2 n}" proof fix x assume "x∈V" have "x=v ⟹ x ∈ {n. adjacent v1 n} ∪ {n. adjacent v2 n}" by (metis Un_iff adjacent_sym insertI1 mem_Collect_eq v1v2) moreover have "x≠v ⟹ x ∈ {n. adjacent v1 n} ∪ {n. adjacent v2 n}" proof - assume "x≠v" then obtain y where "adjacent v y" "adjacent x y" using friend_assm[of v x] by (metis Collect_empty_eq ‹x ∈ V› adjacent_V(1) all_not_in_conv insertCI v1v2) hence "y=v1 ∨ y=v2" using v1v2 by auto thus "x ∈ {n. adjacent v1 n} ∪ {n. adjacent v2 n}" using ‹adjacent x y› by (metis UnI1 UnI2 adjacent_sym mem_Collect_eq) qed ultimately show "x ∈ {n. adjacent v1 n} ∪ {n. adjacent v2 n}" by auto qed have "{n. adjacent v1 n}-{v2,v}={} ⟹ ∃v. ∀n∈V. n ≠ v ⟶ adjacent v n" proof (rule exI[of _ v2],rule,rule) fix n assume v1_adj:"{n. adjacent v1 n} - {v2, v} = {}" and "n ∈ V" and "n ≠ v2" have "n∈{n. adjacent v2 n}" proof (cases "n=v") case True show ?thesis by (metis True adjacent_sym insertI1 insert_commute mem_Collect_eq v1v2) next case False have "n∉{n. adjacent v1 n}" by (metis DiffI False ‹n ≠ v2› empty_iff insert_iff v1_adj) thus ?thesis by (metis Un_iff ‹n ∈ V› v1v2_adj) qed thus "adjacent v2 n" by auto qed moreover have "{n. adjacent v2 n}-{v1,v}={} ⟹ ∃v. ∀n∈V. n ≠ v ⟶ adjacent v n" proof (rule exI[of _ v1],rule,rule) fix n assume v2_adj:"{n. adjacent v2 n} - {v1, v} = {}" and "n ∈ V" and "n ≠ v1" have "n∈{n. adjacent v1 n}" proof (cases "n=v") case True show ?thesis by (metis True adjacent_sym insertI1 mem_Collect_eq v1v2) next case False have "n∉{n. adjacent v2 n}" by (metis DiffI False ‹n ≠ v1› empty_iff insert_iff v2_adj) thus ?thesis by (metis Un_iff ‹n ∈ V› v1v2_adj) qed thus "adjacent v1 n" by auto qed moreover have "{n. adjacent v1 n}-{v2,v}≠{} ⟹ {n. adjacent v2 n}-{v1,v}≠{} ⟹False" proof - assume "{n. adjacent v1 n} - {v2, v} ≠ {}" "{n. adjacent v2 n} - {v1, v} ≠ {}" then obtain a b where a:"a∈{n. adjacent v1 n} - {v2, v}" and b:"b∈{n. adjacent v2 n} - {v1, v}" by auto have "a=b ⟹ False" proof - assume "a=b" have "adjacent v1 a" using a by auto moreover have "adjacent a v2" using b ‹a=b› adjacent_sym by auto moreover have "a≠v" by (metis DiffD2 ‹a = b› b doubleton_eq_iff insertI1) moreover have "adjacent v2 v" by (metis (full_types) adjacent_sym inf_sup_aci(5) insertI1 insert_is_Un mem_Collect_eq v1v2) moreover have "adjacent v v1" by (metis (full_types) insertI1 mem_Collect_eq v1v2) ultimately show False using no_quad[OF friend_assm] using ‹v1≠v2› by auto qed moreover have "a≠b⟹False" proof - assume "a≠b" moreover have "a∈V" using a by (metis DiffD1 adjacent_V(2) mem_Collect_eq) moreover have "b∈V" using b by (metis DiffD1 adjacent_V(2) mem_Collect_eq) ultimately obtain c where "adjacent a c" "adjacent b c" using friend_assm[of a b] by auto hence "c∈{n. adjacent v1 n} ∪ {n. adjacent v2 n}" by (metis (full_types) adjacent_V(2) v1v2_adj) moreover have "c∈{n. adjacent v1 n} ⟹ False" proof - assume "c∈{n. adjacent v1 n}" hence "adjacent v1 c" by auto moreover have "adjacent c b" by (metis ‹adjacent b c› adjacent_sym) moreover have "adjacent b v2" by (metis (full_types) Diff_iff adjacent_sym b mem_Collect_eq) moreover have "adjacent v2 v1" by (metis ‹adjacent v1 v2› adjacent_sym) moreover have "c≠v2" proof (rule ccontr) assume "¬ c ≠ v2" hence "c=v2" by auto hence "adjacent v2 a" by (metis ‹adjacent a c› adjacent_sym) moreover have "adjacent v2 v" by (metis adjacent_sym insert_iff mem_Collect_eq v1v2) moreover have "adjacent v1 v" using adjacent_sym v1v2 by auto moreover have "adjacent v1 a" by (metis (full_types) Diff_iff a mem_Collect_eq) ultimately have "a=v" using friend_assm[of v1 v2] by (metis ‹v1 ≠ v2› adjacent_V(1)) thus False using a by auto qed moreover have "b≠v1" by (metis DiffD2 b insertI1) ultimately show False using no_quad[OF friend_assm] by auto qed moreover have "c∈{n. adjacent v2 n} ⟹ False" proof - assume "c∈{n. adjacent v2 n}" hence "adjacent c v2" by (metis adjacent_sym mem_Collect_eq) moreover have "adjacent a c" using ‹adjacent a c› . moreover have "adjacent v1 a" by (metis (full_types) Diff_iff a mem_Collect_eq) moreover have "adjacent v2 v1" by (metis ‹adjacent v1 v2› adjacent_sym) moreover have "c≠v1" proof (rule ccontr) assume "¬ c ≠ v1" hence "c=v1" by auto hence "adjacent v1 b" by (metis ‹adjacent b c› adjacent_sym) moreover have "adjacent v2 v" by (metis adjacent_sym insert_iff mem_Collect_eq v1v2) moreover have "adjacent v1 v" using adjacent_sym v1v2 by auto moreover have "adjacent v2 b" by (metis Diff_iff b mem_Collect_eq) ultimately have "b=v" using friend_assm[of v1 v2] by (metis ‹v1 ≠ v2› adjacent_V(1)) thus False using b by auto qed moreover have "a≠v2" by (metis DiffD2 a insertI1) ultimately show False using no_quad[OF friend_assm] by auto qed ultimately show False by auto qed ultimately show False by auto qed ultimately show "∃v. ∀n∈V. n ≠ v ⟶ adjacent v n" by auto next assume "∃v. ∀n∈V. n ≠ v ⟶ adjacent v n" then obtain v where v:"∀n∈V. n ≠ v ⟶ adjacent v n" by auto obtain v1 where "v1∈V" "v1≠v" proof (cases "v∈V") case False have "V≠{}" using ‹2≤card V› by auto then obtain v1 where "v1∈V" by auto thus ?thesis using False that[of v1] by auto next case True then obtain S where "V = insert v S" "v ∉ S" using mk_disjoint_insert[OF True] by auto moreover have "finite V" using ‹2≤card V› by (metis add_leE card.infinite not_one_le_zero numeral_Bit0 numeral_One) ultimately have "1≤card S" using ‹2≤card V› card.insert[of S v] finite_insert[of v S] by auto hence "S≠{}" by auto then obtain v1 where "v1∈S" by auto hence "v1≠v" using ‹v∉S› by auto thus thesis using that[of v1] ‹v1∈S› ‹V=insert v S› by auto qed hence "v∈V" using v by (metis adjacent_V(1)) then obtain v2 where "adjacent v1 v2" "adjacent v v2" using friend_assm[of v v1] by (metis ‹v1 ∈ V› ‹v1 ≠ v›) have "degree v1 G≠2 ⟹ False" proof - assume "degree v1 G≠2" hence "card {n. adjacent v1 n}≠2" by (metis assms(2) degree_adjacent) have "{v,v2} ⊆ {n. adjacent v1 n}" by (metis ‹ adjacent v1 v2 › ‹ v1 ∈ V › ‹ v1 ≠ v › adjacent_sym bot_least insert_subset mem_Collect_eq v) moreover have "v≠v2" using ‹adjacent v v2› adjacent_no_loop by auto hence "card {v,v2} = 2" by auto ultimately have "card {n. adjacent v1 n} ≥2" using adjacent_finite[OF ‹finite E›, of v1] by (metis card_mono) hence "card {n. adjacent v1 n} ≥3" using ‹card {n. adjacent v1 n}≠2› by auto then obtain v3 where "v3∈{n. adjacent v1 n}" and "v3∉{v,v2}" using ‹{v,v2} ⊆ {n. adjacent v1 n}› ‹card {v, v2} = 2› by (metis ‹card {n. adjacent v1 n} ≠ 2› subsetI subset_antisym) hence "adjacent v1 v3" by auto moreover have "adjacent v3 v" using v by (metis ‹v3 ∉ {v, v2}› adjacent_V(2) adjacent_sym calculation insertCI) moreover have "adjacent v v2" using ‹adjacent v v2› . moreover have "adjacent v2 v1" using ‹adjacent v1 v2› adjacent_sym by auto moreover have "v1≠v" using ‹v1 ≠ v› . moreover have "v3≠v2" by (metis ‹v3 ∉ {v, v2}› insert_subset subset_insertI) ultimately show False using no_quad[OF friend_assm] by auto qed thus "∃v∈V. degree v G = 2" using ‹v1∈V› by auto qed lemma (in valid_unSimpGraph) regular: assumes friend_assm:"⋀v u. v∈V ⟹ u∈V ⟹ v≠u ⟹ ∃! n. adjacent v n ∧ adjacent u n" and "finite E" and "finite V" and "¬(∃v∈V. degree v G = 2)" shows "∃k. ∀v∈V. degree v G = k" proof - { fix v u assume "non_adj v u" obtain v_adj where v_adj:"v_adj={n. adjacent v n}" by auto obtain u_adj where u_adj:"u_adj={n. adjacent u n}" by auto obtain f where f:"f = (λn. (SOME v'. n∈V ⟶n≠u⟶adjacent n v' ∧ adjacent u v'))" by auto have "⋀n. n∈V ⟶ n≠u ⟶ (∃v'. adjacent n v' ∧ adjacent u v')" proof (rule,rule) fix n assume "n ∈ V" "n ≠ u" hence "∃!v'. adjacent n v' ∧ adjacent u v'" using friend_assm[of n u] ‹non_adj v u› unfolding non_adj_def by auto thus "∃v'. adjacent n v' ∧ adjacent u v'" by auto qed hence f_ex:"⋀n. (∃v'. n∈V ⟶ n≠u ⟶ adjacent n v' ∧ adjacent u v')" by auto obtain v_adj_u where v_adj_u:"v_adj_u= f ` v_adj" by auto have "finite u_adj" using u_adj adjacent_finite[OF ‹finite E›] by auto have "finite v_adj" using v_adj adjacent_finite[OF ‹finite E›] by auto hence "finite v_adj_u" using v_adj_u adjacent_finite[OF ‹finite E›] by auto have "inj_on f v_adj" unfolding inj_on_def proof (rule ccontr) assume "¬ (∀x∈v_adj. ∀y∈v_adj. f x = f y ⟶ x = y)" then obtain x y where "x∈v_adj" "y∈v_adj" "f x=f y" "x≠y" by auto have "x∈V" by (metis ‹x ∈ v_adj› adjacent_V(2) mem_Collect_eq v_adj) moreover have "x≠u" by (metis ‹non_adj v u› ‹x ∈ v_adj› mem_Collect_eq non_adj_def v_adj) ultimately have "adjacent (f x) u" and "adjacent x (f x)" using someI_ex[OF f_ex[of x]] adjacent_sym by (metis f)+ hence "f x ≠ v" by (metis ‹non_adj v u› non_adj_def) have "y∈V" by (metis ‹y ∈ v_adj› adjacent_V(2) mem_Collect_eq v_adj) moreover have "y≠u" by (metis ‹non_adj v u› ‹y ∈ v_adj› mem_Collect_eq non_adj_def v_adj) ultimately have "adjacent y (f y)" using someI_ex[OF f_ex[of y]] by (metis f) hence " x ≠ y ∧ v ≠ f x ∧ adjacent v x ∧ adjacent x (f x) ∧ adjacent (f x) y ∧ adjacent y v" using ‹x∈v_adj› ‹y∈v_adj› ‹f x=f y› ‹x≠y› ‹adjacent x (f x)› v_adj adjacent_sym ‹f x ≠ v› by auto thus False using no_quad[OF friend_assm] by auto qed then have "card v_adj =card v_adj_u" by (metis card_image v_adj_u) moreover have "v_adj_u ⊆ u_adj" proof fix x assume "x∈v_adj_u" then obtain y where "y∈v_adj" and "x = (SOME v'. y ∈ V ⟶ y ≠ u ⟶ adjacent y v' ∧ adjacent u v')" using f image_def v_adj_u by auto hence "y ∈ V ⟶ y ≠ u ⟶ adjacent y x ∧ adjacent u x" using someI_ex[OF f_ex[of y]] by auto moreover have "y∈V" by (metis ‹y ∈ v_adj› adjacent_V(2) mem_Collect_eq v_adj) moreover have "y≠u" by (metis ‹non_adj v u› ‹y ∈ v_adj› mem_Collect_eq non_adj_def v_adj) ultimately have "adjacent u x" by auto thus "x∈u_adj" unfolding u_adj by auto qed moreover have "card v_adj=degree v G" using degree_adjacent[OF ‹finite E›, of v] v_adj by auto moreover have "card u_adj=degree u G" using degree_adjacent[OF ‹finite E›, of u] u_adj by auto ultimately have "degree v G ≤ degree u G" using ‹finite u_adj› by (metis ‹inj_on f v_adj› card_inj_on_le v_adj_u) } hence non_adj_degree:"⋀v u. non_adj v u ⟹ degree v G = degree u G" by (metis adjacent_sym antisym non_adj_def) have "card V=3 ⟹ ?thesis" proof assume "card V=3" then obtain v1 v2 v3 where "V={v1,v2,v3}" "v1≠v2" "v2≠v3" "v1≠v3" proof - obtain v1 S1 where VS1:"V = insert v1 S1" and "v1 ∉ S1" and "card S1 = 2" using card_Suc_eq[of V 2] ‹card V=3› by auto then obtain v2 S2 where S1S2:"S1 = insert v2 S2" and "v2 ∉ S2" and "card S2 = 1" using card_Suc_eq[of S1 1] by auto then obtain v3 where "S2={v3}" using card_Suc_eq[of S2 0] by auto hence "V={v1,v2,v3}" using VS1 S1S2 by auto moreover have "v1≠v2" "v2≠v3" "v1≠v3"using VS1 S1S2 ‹v1∉S1› ‹v2∉S2› ‹S2={v3}› by auto ultimately show ?thesis using that by auto qed obtain n where "adjacent v1 n" "adjacent v2 n" using friend_assm[of v1 v2] by (metis ‹V = {v1, v2, v3}› ‹v1 ≠ v2› insertI1 insertI2) moreover hence "n=v3" using ‹V = {v1, v2, v3}› adjacent_V(2) adjacent_no_loop by (metis (mono_tags) empty_iff insertE) moreover obtain n' where "adjacent v2 n'" "adjacent v3 n'" using friend_assm[of v2 v3] by (metis ‹V = {v1, v2, v3}› ‹v2 ≠ v3› insertI1 insertI2) moreover hence "n'=v1" using ‹V = {v1, v2, v3}› adjacent_V(2) adjacent_no_loop by (metis (mono_tags) empty_iff insertE) ultimately have "adjacent v1 v2" and "adjacent v2 v3" and "adjacent v3 v1" using adjacent_sym by auto have "degree v1 G=2" proof - have "v2∈{n. adjacent v1 n}" and "v3∈{n. adjacent v1 n}" and "v1∉{n. adjacent v1 n}" using ‹adjacent v1 v2› ‹adjacent v3 v1› adjacent_sym by (auto,metis adjacent_no_loop) hence "{n. adjacent v1 n}={v2,v3}" using ‹V={v1,v2,v3}› by auto thus ?thesis using degree_adjacent[OF ‹finite E›,of v1] ‹v2≠v3› by auto qed moreover have "degree v2 G=2" proof - have "v1∈{n. adjacent v2 n}" and "v3∈{n. adjacent v2 n}" and "v2∉{n. adjacent v2 n}" using ‹adjacent v1 v2› ‹adjacent v2 v3› adjacent_sym by (auto,metis adjacent_no_loop) hence "{n. adjacent v2 n}={v1,v3}" using ‹V={v1,v2,v3}› by force thus ?thesis using degree_adjacent[OF ‹finite E›,of v2] ‹v1≠v3› by auto qed moreover have "degree v3 G=2" proof - have "v1∈{n. adjacent v3 n}" and "v2∈{n. adjacent v3 n}" and "v3∉{n. adjacent v3 n}" using ‹adjacent v3 v1› ‹adjacent v2 v3› adjacent_sym by (auto,metis adjacent_no_loop) hence "{n. adjacent v3 n}={v1,v2}" using ‹V={v1,v2,v3}› by force thus ?thesis using degree_adjacent[OF ‹finite E›,of v3] ‹v1≠v2› by auto qed ultimately show "∀v∈V. degree v G = 2" using ‹V={v1,v2,v3}› by auto qed moreover have "card V=2 ⟹ False" proof - assume "card V=2" obtain v1 v2 where "V={v1,v2}" "v1≠v2" proof - obtain v1 S1 where VS1:"V = insert v1 S1" and "v1 ∉ S1" and "card S1 = 1" using card_Suc_eq[of V 1] ‹card V=2› by auto then obtain v2 where "S1={v2}" using card_Suc_eq[of S1 0] by auto hence "V={v1,v2}" using VS1 by auto moreover have "v1≠v2" using ‹v1∉S1› ‹S1={v2}› by auto ultimately show ?thesis using that by auto qed then obtain v3 where "adjacent v1 v3" "adjacent v2 v3" using friend_assm[of v1 v2] by auto hence "v3≠v2" and "v3≠v1" by (metis adjacent_no_loop)+ hence "v3∉V" using ‹V={v1,v2}› by auto thus False using ‹adjacent v1 v3› by (metis (full_types) adjacent_V(2)) qed moreover have "card V=1 ⟹ ?thesis" proof assume "card V=1" then obtain v1 where "V={v1}" using card_eq_SucD[of V 0] by auto have "E={}" proof (rule ccontr) assume "E≠{}" then obtain x1 x2 x3 where x:"(x1,x2,x3)∈E" by auto hence "x1=v1" and "x3=v1" using ‹V={v1}› E_validD by auto thus False using no_id x by auto qed hence "degree v1 G=0" unfolding degree_def by auto thus "∀v∈V. degree v G =0" using ‹V={v1}›by auto qed moreover have "card V=0 ⟹ ?thesis" proof - assume "card V=0" hence "V={}" using ‹finite V› by auto thus ?thesis by auto qed moreover have "card V ≥4 ⟹ ¬(∃v u. non_adj v u) ⟹ False" proof - assume "¬(∃v u. non_adj v u)" "card V≥4" hence non_non_adj:"⋀v u. v∉V ∨ u∉V ∨ v=u ∨ adjacent v u" unfolding non_adj_def by auto obtain v1 v2 v3 v4 where "v1∈V" "v2∈V" "v3∈V" "v4∈V" "v1≠v2" "v1≠v3" "v1≠v4" "v2≠v3" "v2≠v4" "v3≠v4" proof - obtain v1 B1 where "V = insert v1 B1" "v1 ∉ B1" "card B1 ≥3" using ‹card V≥4› card_le_Suc_iff[of 3 V] by auto then obtain v2 B2 where "B1 = insert v2 B2" "v2 ∉ B2" "card B2 ≥2" using card_le_Suc_iff[of 2 B1] by auto then obtain v3 B3 where "B2= insert v3 B3" "v3∉B3" "card B3≥1" using card_le_Suc_iff[of 1 B2] by auto then obtain v4 B4 where "B3=insert v4 B4" "v4∉B4" using card_le_Suc_iff[of 0 B3] by auto have "v1∈V" by (metis ‹V = insert v1 B1› insert_subset order_refl) moreover have "v2∈V" by (metis ‹B1 = insert v2 B2› ‹V = insert v1 B1› insert_subset subset_insertI) moreover have "v3∈V" by (metis ‹B1 = insert v2 B2› ‹B2 = insert v3 B3› ‹V = insert v1 B1› insert_iff) moreover have "v4∈V" by (metis ‹B1 = insert v2 B2› ‹B2 = insert v3 B3› ‹B3 = insert v4 B4› ‹V = insert v1 B1› insert_iff) moreover have "v1≠v2" by (metis (full_types) ‹B1 = insert v2 B2› ‹v1 ∉ B1› insertI1) moreover have "v1≠v3" by (metis ‹B1 = insert v2 B2› ‹B2 = insert v3 B3› ‹v1 ∉ B1› insert_iff) moreover have "v1≠v4" by (metis ‹B1 = insert v2 B2› ‹B2 = insert v3 B3› ‹B3 = insert v4 B4› ‹v1 ∉ B1› insert_iff) moreover have "v2≠v3" by (metis (full_types) ‹B2 = insert v3 B3› ‹v2 ∉ B2› insertI1) moreover have "v2≠v4" by (metis ‹B2 = insert v3 B3› ‹B3 = insert v4 B4› ‹v2 ∉ B2› insert_iff) moreover have "v3≠v4" by (metis (full_types) ‹B3 = insert v4 B4› ‹v3 ∉ B3› insertI1) ultimately show ?thesis using that by auto qed hence "adjacent v1 v2" using non_non_adj by auto moreover have "adjacent v2 v3" using non_non_adj by (metis ‹v2 ∈ V› ‹v2 ≠ v3› ‹v3 ∈ V›) moreover have "adjacent v3 v4" using non_non_adj by (metis ‹v3 ∈ V› ‹v3 ≠ v4› ‹v4 ∈ V›) moreover have "adjacent v4 v1" using non_non_adj by (metis ‹v1 ∈ V› ‹v1 ≠ v4› ‹v4 ∈ V›) ultimately show False using no_quad[OF friend_assm] by (metis ‹v1 ≠ v3› ‹v2 ≠ v4›) qed moreover have "card V≥4 ⟹ (∃v u. non_adj v u) ⟹ ?thesis" proof - assume "(∃v u. non_adj v u)" "card V≥4" then obtain v u where "non_adj v u" by auto then obtain w where "adjacent v w" and "adjacent u w" and unique:"∀n. adjacent v n ∧ adjacent u n ⟶ n=w" using friend_assm[of v u] unfolding non_adj_def by auto have "∀n∈V. degree n G = degree v G" proof fix n assume "n∈V" moreover have "n=v ⟹ degree n G = degree v G" by auto moreover have "n=u ⟹ degree n G = degree v G" using non_adj_degree ‹non_adj v u› by auto moreover have "n≠v ⟹ n≠u ⟹ n≠w ⟹ degree n G = degree v G" proof - assume "n≠v" "n≠u" "n≠w" have "non_adj v n ⟹ degree n G = degree v G" by (metis non_adj_degree) moreover have "non_adj u n ⟹ degree n G = degree v G" by (metis ‹non_adj v u› non_adj_degree) moreover have "¬non_adj u n ⟹ ¬non_adj v n ⟹ degree n G = degree v G" by (metis ‹n ∈ V› ‹n ≠ w› ‹non_adj v u› non_adj_def unique) ultimately show "degree n G = degree v G" by auto qed moreover have "n=w ⟹ degree n G = degree v G" proof - assume "n=w" moreover have "¬(∃v. ∀n∈V. n≠v ⟶ adjacent v n)" using ‹card V≥4› degree_two_windmill assms(2) assms(4) friend_assm by auto ultimately obtain w1 where "w1∈V" "w1≠w" "non_adj w w1" by (metis ‹n∈V› non_adj_def) have "w1=v ⟹ degree n G = degree v G" by (metis ‹n = w› ‹non_adj w w1› non_adj_degree) moreover have "w1=u ⟹ degree n G = degree v G" by (metis ‹adjacent u w› ‹non_adj w w1› adjacent_sym non_adj_def) moreover have "w1≠u ⟹ w1≠v ⟹ degree n G = degree v G" by (metis ‹n = w› ‹non_adj v u› ‹non_adj w w1› non_adj_def non_adj_degree unique) ultimately show "degree n G = degree v G" by auto qed ultimately show "degree n G = degree v G" by auto qed thus ?thesis by auto qed ultimately show ?thesis by force qed (*In this section, combinatorial proofs for the Friendship Theorem differ from the algebraic ones. The main difference between these two approaches is that combinatorial proofs show Lemma exist_degree_two by counting the number of paths while algebraic proofs show it by computing the eigenvalue of adjacency matrices.*) section‹Exclusive steps for combinatorial proofs› fun (in valid_unSimpGraph) adj_path:: "'v ⇒ 'v list ⇒bool" where "adj_path v [] = (v∈V)" | "adj_path v (u#us)= (adjacent v u ∧ adj_path u us)" lemma (in valid_unSimpGraph) adj_path_butlast: "adj_path v ps ⟹ adj_path v (butlast ps)" by (induct ps arbitrary:v,auto) lemma (in valid_unSimpGraph) adj_path_V: "adj_path v ps ⟹ set ps ⊆ V" by (induct ps arbitrary:v, auto) lemma (in valid_unSimpGraph) adj_path_V': "adj_path v ps ⟹ v∈ V" by (induct ps arbitrary:v, auto) lemma (in valid_unSimpGraph) adj_path_app: "adj_path v ps ⟹ ps≠[] ⟹ adjacent (last ps) u ⟹ adj_path v (ps@[u])" proof (induct ps arbitrary:v) case Nil thus ?case by auto next case (Cons x xs) thus ?case by (cases xs,auto) qed lemma (in valid_unSimpGraph) adj_path_app': "adj_path v (ps @ [q] ) ⟹ ps ≠ [] ⟹ adjacent (last ps) q" proof (induct ps arbitrary:v) case Nil thus ?case by auto next case (Cons x xs) thus ?case by (cases xs,auto) qed lemma card_partition': assumes "∀v∈A. card {n. R v n} = k" "k>0" "finite A" "∀v1 v2. v1≠v2 ⟶ {n. R v1 n} ∩ {n. R v2 n}={}" shows "card (⋃v∈A. {n. R v n}) = k * card A" proof - have "⋀C. C ∈ (λx. {n. R x n}) ` A ⟹ card C = k" proof - fix C assume "C ∈ (λx. {n. R x n}) ` A" show "card C=k" by (metis (mono_tags) ‹C ∈ (λx. {n. R x n}) ` A› assms(1) imageE) qed moreover have "⋀C1 C2. C1 ∈(λx. {n. R x n}) ` A ⟹ C2 ∈ (λx. {n. R x n}) ` A ⟹ C1 ≠ C2 ⟹ C1 ∩ C2 = {}" proof - fix C1 C2 assume "C1 ∈ (λx. {n. R x n}) ` A" "C2 ∈ (λx. {n. R x n}) ` A" "C1 ≠ C2" obtain v1 where "v1∈A" "C1={n. R v1 n}" by (metis ‹C1 ∈ (λx. {n. R x n}) ` A› imageE) obtain v2 where "v2∈A" "C2={n. R v2 n}" by (metis ‹C2 ∈ (λx. {n. R x n}) ` A› imageE) have "v1≠v2" by (metis ‹C1 = {n. R v1 n}› ‹C1 ≠ C2› ‹C2 = {n. R v2 n}›) thus "C1 ∩ C2 ={}" by (metis ‹C1 = {n. R v1 n}› ‹C2 = {n. R v2 n}› assms(4)) qed moreover have "⋃((λx. {n. R x n}) ` A) = (⋃x∈A. {n. R x n})" by auto moreover have "finite ((λx. {n. R x n}) ` A )" by (metis assms(3) finite_imageI) moreover have "finite (⋃((λx. {n. R x n}) ` A))" by (metis (full_types) assms(1) assms(2) assms(3) card_eq_0_iff finite_UN_I less_nat_zero_code) moreover have " card A = card ((λx. {n. R x n}) ` A)" proof - have "inj_on (λx. {n. R x n}) A" unfolding inj_on_def using ‹∀v1 v2. v1≠v2 ⟶ {n. R v1 n} ∩ {n. R v2 n}={}› by (metis assms(1) assms(2) card.empty inf.idem less_le) thus ?thesis by (metis card_image) qed ultimately show ?thesis using card_partition[of "(λx. {n. R x n}) ` A"] by auto qed lemma (in valid_unSimpGraph) path_count: assumes k_adj:"⋀v. v∈V ⟹ card {n. adjacent v n} = k" and "v∈V" and "finite V" and "k>0" shows "card {ps. length ps=l ∧ adj_path v ps}=k^l" proof (induct l rule:nat.induct) case zero have "{ps. length ps=0 ∧ adj_path v ps}={[]}" using ‹v∈V› by auto thus ?case by auto next case (Suc n) obtain ext where ext: "ext=(λps ps'. ps'≠[] ∧ (butlast ps'=ps) ∧ adj_path v ps')" by auto have "∀ps∈{ps. length ps = n ∧ adj_path v ps}. card {ps'. ext ps ps'} = k" proof fix ps assume "ps∈{ps. length ps = n ∧ adj_path v ps}" hence "adj_path v ps" and "length ps = n" by auto obtain qs where qs:"qs = {n. if ps=[] then adjacent v n else adjacent (last ps) n}" by auto hence "card qs = k" proof (cases "ps=[]") case True thus ?thesis using qs k_adj[OF ‹v∈V›] by auto next case False have "last ps ∈ V" using adj_path_V by (metis False ‹adj_path v ps› last_in_set subsetD) thus ?thesis using k_adj[of "last ps"] False qs by auto qed obtain app where app:"app=(λq. ps@[q])" by auto have "app ` qs = {ps'. ext ps ps'}" proof - have "⋀xs. xs∈ app ` qs ⟹ xs ∈ {ps'. ext ps ps'}" proof (rule,cases "ps=[]") case True fix xs assume "xs∈ app ` qs" then obtain q where "q∈ qs" "app q=xs" by (metis imageE) hence "adjacent v q" and "xs=ps@[q]" using qs app True by auto hence "adj_path v xs" by (metis True adj_path.simps(1) adj_path.simps(2) adjacent_V(2) append_Nil) moreover have "butlast xs = ps" using ‹xs=ps@[q]› by auto ultimately show "ext ps xs" using ext ‹xs=ps@[q]› by auto next case False fix xs assume "xs∈ app ` qs" then obtain q where "q∈ qs" "app q=xs" by (metis imageE) hence "adjacent (last ps) q" using qs app False by auto hence "adj_path v (ps@[q])" using ‹adj_path v ps› False adj_path_app by auto hence "adj_path v xs" by (metis ‹app q = xs› app) moreover have "butlast xs=ps" by (metis ‹app q = xs› app butlast_snoc) ultimately show "ext ps xs" by (metis False butlast.simps(1) ext) qed moreover have "⋀xs. xs∈{ps'. ext ps ps'} ⟹ xs∈ app ` qs" proof (cases "ps=[]") case True hence "qs = {n. adjacent v n }" using qs by auto fix xs assume "xs ∈ {ps'. ext ps ps'}" hence "xs≠[]" and "(butlast xs=ps)" and "adj_path v xs" using ext by auto thus "xs ∈ app ` qs" using True app ‹qs = {n. adjacent v n}› by (metis adj_path.simps(2) append_butlast_last_id append_self_conv2 image_iff mem_Collect_eq) next case False fix xs assume "xs ∈ {ps'. ext ps ps'}" hence "xs≠[]" and "(butlast xs=ps)" and "adj_path v xs" using ext by auto then obtain q where "xs=ps@[q]" by (metis append_butlast_last_id) hence "adjacent (last ps) q" using ‹adj_path v xs› False adj_path_app' by auto thus "xs ∈ app ` qs" using qs by (metis (lifting, full_types) False ‹xs = ps @ [q]› app imageI mem_Collect_eq) qed ultimately show ?thesis by auto qed moreover have "inj_on app qs" using app unfolding inj_on_def by auto ultimately show "card {ps'. ext ps ps'}=k" by (metis ‹card qs = k› card_image) qed moreover have "∀ps1 ps2. ps1≠ps2 ⟶ {n. ext ps1 n} ∩ {n. ext ps2 n}={}" using ext by auto moreover have "finite {ps. length ps = n ∧ adj_path v ps}" using Suc.hyps assms by (auto intro: card_ge_0_finite) ultimately have "card (⋃v∈{ps. length ps = n ∧ adj_path v ps}. {n. ext v n}) = k * card {ps. length ps = n ∧ adj_path v ps}" using card_partition'[of "{ps. length ps = n ∧ adj_path v ps}" ext k] ‹k>0› by auto moreover have "{ps. length ps = n+1 ∧ adj_path v ps} =(⋃ps∈{ps. length ps = n ∧ adj_path v ps}. {ps'. ext ps ps'})" proof - have "⋀xs. xs ∈ {ps. length ps = n + 1 ∧ adj_path v ps} ⟹ xs ∈ (⋃ps∈{ps. length ps = n ∧ adj_path v ps}. {ps'. ext ps ps'})" proof - fix xs assume "xs ∈ {ps. length ps = n + 1 ∧ adj_path v ps}" hence "length xs = n +1" and "adj_path v xs" by auto hence "butlast xs ∈{ps. length ps = n ∧ adj_path v ps}" using adj_path_butlast length_butlast mem_Collect_eq by auto thus "xs ∈ (⋃ps∈{ps. length ps = n ∧ adj_path v ps}. {ps'. ext ps ps'})" using ‹adj_path v xs› ‹length xs = n + 1› UN_iff ext length_greater_0_conv mem_Collect_eq by auto qed moreover have "⋀xs . xs∈(⋃ps∈{ps. length ps = n ∧ adj_path v ps}. {ps'. ext ps ps'}) ⟹ xs ∈ {ps. length ps = n + 1 ∧ adj_path v ps}" proof - fix xs assume "xs∈(⋃ps∈{ps. length ps = n ∧ adj_path v ps}. {ps'. ext ps ps'})" then obtain ys where "length ys=n" "adj_path v ys" "ext ys xs" by auto hence "length xs=n+1" using ext by auto thus "xs∈{ps. length ps = n + 1 ∧ adj_path v ps}" by (metis (lifting, full_types) ‹ext ys xs› ext mem_Collect_eq) qed ultimately show ?thesis by fast qed ultimately show "card {ps. length ps = (Suc n) ∧ adj_path v ps} = k ^ (Suc n)" using Suc.hyps by auto qed lemma (in valid_unSimpGraph) total_v_num: assumes friend_assm:"⋀v u. v∈V ⟹ u∈V ⟹ v≠u ⟹ ∃! n. adjacent v n ∧ adjacent u n" and "finite E" and "finite V" and "V≠{}" and " ∀v∈V. degree v G = k" and "k>0" shows "card V= k*k - k +1" proof - have k_adj:"⋀v. v∈V⟹card ({n. adjacent v n})=k" by (metis assms(2) assms(5) degree_adjacent) obtain v where "v∈V" using ‹V≠{}› by auto obtain l2_eq_v where l2_eq_v: "l2_eq_v={ps. length ps=2 ∧ adj_path v ps ∧ last ps=v}" by auto have "card l2_eq_v=k" proof - obtain hds where hds:"hds= hd` l2_eq_v" by auto moreover have "hds={n. adjacent v n}" proof - have "⋀x. x∈hds ⟹ x∈ {n. adjacent v n}" proof fix x assume "x∈hds" then obtain ps where "hd ps=x" "length ps=2" "adj_path v ps" "last ps=v" using hds l2_eq_v by auto thus "adjacent v x" by (metis (full_types) adj_path.simps(2) list.sel(1) length_0_conv neq_Nil_conv zero_neq_numeral) qed moreover have "⋀x. x∈{n. adjacent v n} ⟹ x∈hds" proof - fix x assume "x∈{n. adjacent v n}" obtain ps where "ps=[x,v]" by auto hence "hd ps=x" and "length ps=2" and "adj_path v ps" and "last ps=v" using ‹x∈{n. adjacent v n}› adjacent_sym by auto thus "x∈hds" by (metis (lifting, mono_tags) hds image_eqI l2_eq_v mem_Collect_eq) qed ultimately show "hds={n. adjacent v n}" by auto qed moreover have "inj_on hd l2_eq_v" unfolding inj_on_def proof (rule+) fix x y assume "x ∈ l2_eq_v" "y ∈ l2_eq_v" "hd x = hd y" hence "length x=2" and "last x=last y" and "length y=2" using l2_eq_v by auto hence "x!1=y!1" using last_conv_nth[of x] last_conv_nth[of y] by force moreover have "x!0=y!0" using ‹hd x=hd y› ‹length x=2› ‹length y=2› by(metis hd_conv_nth length_greater_0_conv) ultimately show "x=y" using ‹length x=2› ‹length y=2› using nth_equalityI[of x y] by (metis One_nat_def less_2_cases) qed ultimately show "card l2_eq_v=k" using k_adj[OF ‹v∈V›] by (metis card_image) qed obtain l2_neq_v where l2_neq_v:"l2_neq_v={ps. length ps=2 ∧ adj_path v ps ∧ last ps≠v}" by auto have "card l2_neq_v = k*k-k" proof - obtain l2_v where l2_v:"l2_v={ps. length ps=2∧ adj_path v ps}" by auto hence "card l2_v=k*k" using path_count[OF k_adj,of v 2] ‹0<k› ‹finite V› ‹v∈V› by (simp add: power2_eq_square) hence "finite l2_v" using ‹k>0› by (metis card.infinite mult_is_0 neq0_conv) moreover have "l2_v=l2_neq_v ∪ l2_eq_v" using l2_v l2_neq_v l2_eq_v by auto moreover have "l2_neq_v ∩ l2_eq_v ={}" using l2_neq_v l2_eq_v by auto ultimately have "card l2_neq_v = card l2_v - card l2_eq_v" by (metis Int_commute Nat.add_0_right Un_commute card_Diff_subset_Int card_Un_Int card_gt_0_iff diff_add_inverse finite_Diff finite_Un inf_sup_absorb less_nat_zero_code) thus "card l2_neq_v = k*k-k" using ‹card l2_eq_v=k› using ‹card l2_v=k*k› by auto qed moreover have "bij_betw last l2_neq_v {n. n∈V ∧ n≠v}" proof - have "last ` l2_neq_v = {n. n∈V ∧ n≠v}" proof - have "⋀x. x∈ last` l2_neq_v ⟹ x∈{n. n∈V ∧ n≠v}" proof fix x assume "x∈last` l2_neq_v" then obtain ps where "length ps = 2" "adj_path v ps" "last ps=x" "last ps≠v" using l2_neq_v by auto hence "(last ps)∈V" by (metis (full_types) adj_path_V last_in_set length_0_conv rev_subsetD zero_neq_numeral) thus " x ∈ V ∧ x ≠ v" using ‹last ps=x› ‹last ps≠v› by auto qed moreover have "⋀x. x∈{n. n∈V ∧ n≠v} ⟹ x∈ last` l2_neq_v" proof - fix x assume x:"x ∈ {n ∈ V. n ≠ v}" then obtain y where "adjacent v y" "adjacent x y" using friend_assm[of v x] ‹v∈V› by auto hence "adj_path v [y,x]" using adjacent_sym[of x y]by auto hence "[y,x]∈l2_neq_v" using l2_neq_v x by auto thus "x∈ last` l2_neq_v" by (metis imageI last.simps not_Cons_self2) qed ultimately show ?thesis by fast qed moreover have "inj_on last l2_neq_v" unfolding inj_on_def proof (rule,rule,rule) fix x y assume "x ∈ l2_neq_v" "y ∈ l2_neq_v" "last x = last y" hence "length x=2" and "adj_path v x" and "last x≠v" and "length y=2" and "adj_path v y" and "last y≠v" using l2_neq_v by auto obtain x1 x2 y1 y2 where x:"x=[x1,x2]" and y:"y=[y1,y2]" proof - { fix l assume "length l=2" obtain h1 t where "l=h1#t" and "length t=1" using ‹length l=2› Suc_length_conv[of 1 l] by auto then obtain h2 where "t=[h2]" using Suc_length_conv[of 0 t] by auto have "∃h1 h2. l=[h1,h2]" using ‹l=h1#t› ‹t=[h2]› by auto } thus ?thesis using that ‹length x=2› ‹length y=2› by metis qed hence "x2≠v" and "y2≠v" using ‹last x≠v› ‹last y≠v› by auto moreover have "adjacent v x1" and "adjacent x2 x1" and "x2∈V" using ‹adj_path v x› x adjacent_sym by auto moreover have "adjacent v y1" and "adjacent y2 y1" and "y2∈V" using ‹adj_path v y› y adjacent_sym by auto ultimately have "x1=y1" using friend_assm ‹v∈V› by (metis ‹last x = last y› last_ConsL last_ConsR not_Cons_self2 x y) thus "x=y" using x y ‹last x = last y› by auto qed ultimately show ?thesis unfolding bij_betw_def by auto qed hence "card l2_neq_v = card {n. n∈V ∧ n≠v}" by (metis bij_betw_same_card) ultimately have "card {n. n∈V ∧ n≠v}=k*k-k" by auto moreover have "card V = card {n. n∈V∧n≠v} + card {v}" proof - have "V={n. n∈V ∧ n≠v} ∪ {v}" using ‹v∈V› by auto moreover have "{n. n∈V ∧ n≠v} ∩ {v}={}" by auto ultimately show ?thesis using ‹finite V› card_Un_disjoint[of "{n ∈ V. n ≠ v}" "{v}"] finite_Un by auto qed ultimately show "card V = k*k-k+1" by auto qed lemma rotate_eq:"rotate1 xs=rotate1 ys ⟹ xs=ys" proof (induct xs arbitrary:ys) case Nil thus ?case by (metis rotate1_is_Nil_conv) next case (Cons n ns) hence "ys≠[]" by (metis list.distinct(1) rotate1_is_Nil_conv) thus "?case" using Cons by (metis butlast_snoc last_snoc list.exhaust rotate1.simps(2)) qed lemma rotate_diff:"rotate m xs=rotate n xs ⟹rotate (m-n) xs = xs" proof (induct m arbitrary:n) case 0 thus ?case by auto next case (Suc m') hence "n=0 ⟹ ?case" by auto moreover have "n≠0 ⟹?case" proof - assume "n≠0" then obtain n' where n': "n = Suc n'" by (metis nat.exhaust) hence "rotate m' xs = rotate n' xs" using ‹rotate (Suc m') xs = rotate n xs› rotate_eq rotate_Suc by auto hence "rotate (m' - n') xs = xs" by (metis Suc.hyps) moreover have "Suc m' - n = m'-n'" by (metis n' diff_Suc_Suc) ultimately show ?case by auto qed ultimately show ?case by fast qed lemma (in valid_unSimpGraph) exist_degree_two: assumes friend_assm:"⋀v u. v∈V ⟹ u∈V ⟹ v≠u ⟹ ∃! n. adjacent v n ∧ adjacent u n" and "finite E" and "finite V" and "card V≥2" shows "∃v∈V. degree v G = 2" proof (rule ccontr) assume "¬ (∃v∈V. degree v G = 2)" hence "⋀v. v∈V ⟹ degree v G≠2" by auto obtain k where k_adj: "⋀v. v∈V⟹ card {n. adjacent v n}=k" using regular[OF friend_assm] by (metis ‹¬ (∃v∈V. degree v G = 2)› assms(2) assms(3) degree_adjacent) have "k≥4" proof - obtain v1 v2 where "v1∈V" "v2∈V" "v1≠v2" using ‹card V≥2› by (metis ‹¬(∃v∈V. degree v G = 2)› assms(2) degree_two_windmill) have "k≠0" proof assume "k=0" obtain v3 where "adjacent v1 v3" using friend_assm[OF ‹v1∈V› ‹v2∈V› ‹v1≠v2›] by auto hence "card {n. adjacent v1 n} ≠ 0" using adjacent_finite[OF ‹finite E›] by auto moreover have "card {n. adjacent v1 n} = 0" using k_adj[OF ‹v1∈V›] by (metis ‹k = 0›) ultimately show False by simp qed moreover have "even k" using even_degree[OF friend_assm] by (metis ‹v1 ∈ V› assms(2) degree_adjacent k_adj) hence "k≠1" and "k≠3" by auto moreover have "k≠2" using ‹⋀v. v∈V ⟹ degree v G≠2› degree_adjacent k_adj by (metis ‹v1 ∈ V› assms(2)) ultimately show ?thesis by auto qed obtain T where T:"T=(λl::nat. {ps. length ps = l+1 ∧ adj_path (hd ps) (tl ps)})" by auto have T_count:"⋀l::nat. card (T l) = (k*k-k+1)*k^l" using card_partition' proof - fix l::nat obtain ext where ext:"ext=(λv ps. adj_path v (tl ps) ∧ hd ps=v ∧ length ps=l+1)" by auto have "∀v∈V. card {ps. ext v ps} = k^l" proof fix v assume "v ∈ V" have "⋀ps. ps∈tl ` {ps. ext v ps} ⟹ ps∈{ps. length ps=l ∧ adj_path v ps}" proof - fix ps assume "ps ∈ tl ` {ps. ext v ps}" then obtain ps' where "adj_path v (tl ps')" "hd ps'=v" "length ps'=l+1" "ps=tl ps'" using ext by auto hence "adj_path v ps" and "length ps=l" by auto thus "ps∈{ps. length ps=l ∧ adj_path v ps}" by auto qed moreover have "⋀ps. ps∈{ps. length ps=l ∧ adj_path v ps} ⟹ ps∈ tl ` {ps. ext v ps}" proof - fix ps assume "ps ∈ {ps. length ps = l ∧ adj_path v ps}" hence "length ps=l" and "adj_path v ps" by auto moreover obtain ps' where "ps'=v#ps" by auto ultimately have "adj_path v (tl ps')" and "hd ps'=v" and "length ps'=l+1" by auto thus "ps ∈ tl ` {ps. ext v ps}" by (metis ‹ps' = v # ps› ext imageI mem_Collect_eq list.sel(3)) qed ultimately have "tl ` {ps. ext v ps} = {ps. length ps=l ∧ adj_path v ps}" by fast moreover have "inj_on tl {ps. ext v ps}" unfolding inj_on_def proof (rule,rule,rule) fix x y assume "x ∈ Collect (ext v)" "y ∈ Collect (ext v)" "tl x = tl y" hence "hd x=hd y" and "x≠[]" and "y≠[]"using ext by auto thus "x=y" using ‹tl x= tl y› by (metis list.sel(1,3) list.exhaust) qed moreover have "card {ps. length ps=l ∧ adj_path v ps} = k^l" using path_count[OF k_adj,of v l] ‹4 ≤ k› ‹v ∈ V› assms(3) by auto ultimately show " card {ps. ext v ps} = k ^ l" by (metis card_image) qed moreover have "∀v1 v2. v1 ≠ v2 ⟶ {n. ext v1 n} ∩ {n. ext v2 n} = {}" using ext by auto moreover have "(⋃v∈V. {n. ext v n})=T l" proof - have "⋀ps. ps∈(⋃v∈V. {n. ext v n}) ⟹ ps∈T l" using T proof - fix ps assume "ps∈(⋃v∈V. {n. ext v n})" then obtain v where "v∈V" "adj_path v (tl ps)" "hd ps = v" "length ps = l + 1" using ext by auto hence "length ps = l + 1" and "adj_path (hd ps) (tl ps)" by auto thus "ps∈T l" using T by auto qed moreover have "⋀ps. ps∈T l ⟹ ps∈(⋃v∈V. {n. ext v n})" proof - fix ps assume "ps∈T l" hence "length ps = l + 1" and "adj_path (hd ps) (tl ps)" using T by auto moreover then obtain v where "v=hd ps" "v∈V" by (metis adj_path.simps(1) adj_path.simps(2) adjacent_V(1) list.exhaust) ultimately show "ps∈(⋃v∈V. {n. ext v n})" using ext by auto qed ultimately show ?thesis by auto qed ultimately have "card (T l) = card V * k^l" using card_partition'[of V ext "k^l"] ‹ 4 ≤ k › assms(3) mult.commute nat_one_le_power by auto moreover have "card V=(k * k - k + 1)" using total_v_num[OF friend_assm,of k] k_adj degree_adjacent ‹finite E› ‹finite V› ‹card V≥2› ‹4 ≤ k› card_gt_0_iff by force ultimately show "card (T l) = (k * k - k + 1) * k ^ l" by auto qed obtain C where C:"C=(λl::nat. {ps. length ps = l+1 ∧ adj_path (hd ps) (tl ps) ∧ adjacent (last ps) (hd ps)})" by auto obtain C_star where C_star:"C_star=(λl::nat. {ps. length ps = l+1 ∧ adj_path (hd ps) (tl ps) ∧ (last ps) = (hd ps)})" by auto have "⋀l::nat. card (C (l+1)) = k* card (C_star l) + card (T l - C_star l)" proof - fix l::nat have "C (l+1) = {ps. length ps = l+2 ∧ adj_path (hd ps) (tl ps) ∧ adjacent (last ps) (hd ps) ∧ last (butlast ps)=hd ps} ∪ {ps. length ps = l+2 ∧ adj_path (hd ps) (tl ps) ∧ adjacent (last ps) (hd ps) ∧ last (butlast ps)≠hd ps}" using C by auto moreover have " {ps. length ps = l+2 ∧ adj_path (hd ps) (tl ps) ∧ adjacent (last ps) (hd ps) ∧ last (butlast ps)=hd ps} ∩ {ps. length ps = l+2 ∧ adj_path (hd ps) (tl ps) ∧ adjacent (last ps) (hd ps) ∧ last (butlast ps)≠hd ps} ={}" by auto moreover have "finite (C (l+1))" proof - have "C (l+1) ⊆ T (l+1)" using C T by auto moreover have "(k * k - k + 1) * k ^ (l + 1)≠0" using ‹k≥4› by auto hence "finite (T (l+1))" using T_count[of "l+1"] by (metis card.infinite) ultimately show ?thesis by (metis finite_subset) qed ultimately have "card (C (l+1)) = card {ps. length ps = l+2 ∧ adj_path (hd ps) (tl ps) ∧ adjacent (last ps) (hd ps) ∧ last (butlast ps)=hd ps} + card {ps. length ps = l+2 ∧ adj_path (hd ps) (tl ps) ∧ adjacent (last ps) (hd ps) ∧ last (butlast ps)≠hd ps}" using card_Un_disjoint[of "{ps. length ps = l + 2 ∧ adj_path (hd ps) (tl ps) ∧ adjacent (last ps) (hd ps) ∧ last (butlast ps) = hd ps}" "{ps. length ps = l + 2 ∧ adj_path (hd ps) (tl ps) ∧ adjacent (last ps) (hd ps) ∧ last (butlast ps) ≠ hd ps}"] finite_Un by auto moreover have "card {ps. length ps = l+2 ∧ adj_path (hd ps) (tl ps) ∧ adjacent (last ps) (hd ps) ∧ last (butlast ps)=hd ps}=k * card (C_star l)" proof - obtain ext where ext: "ext=(λps ps'. ps'≠[] ∧ (butlast ps'=ps) ∧ adj_path (hd ps') (tl ps'))" by auto have "∀ps∈(C_star l). card {ps'. ext ps ps'} = k" proof fix ps assume "ps∈C_star l" hence "length ps = l + 1" and "adj_path (hd ps) (tl ps)" and "last ps = hd ps" using C_star by auto obtain qs where qs:"qs={v. adjacent (last ps) v}" by auto obtain app where app:"app=(λv. ps@[v])" by auto have "app ` qs = {ps'. ext ps ps'}" proof - have "⋀x. x∈app`qs ⟹ x∈{ps'. ext ps ps'}" proof fix x assume "x ∈ app ` qs" then obtain y where "adjacent (last ps) y" "x=ps@[y]" using qs app by auto moreover hence "adj_path (hd x) (tl x)" by (cases "tl ps = []", metis adj_path.simps(1) adj_path.simps(2) adjacent_V(2) append_Nil list.sel(1,3) hd_append snoc_eq_iff_butlast tl_append2, metis ‹adj_path (hd ps) (tl ps)› adj_path_app hd_append last_tl list.sel(2) tl_append2) ultimately show "ext ps x" using ext by (metis snoc_eq_iff_butlast) qed moreover have "⋀x. x∈{ps'. ext ps ps'}⟹ x∈ app`qs" proof - fix x assume "x ∈ {ps'. ext ps ps'}" hence "x≠[]" and "butlast x=ps" and "adj_path (hd x) (tl x)" using ext by auto have "adjacent (last ps) (last x)" proof (cases "length ps=1") case True hence "length x=2" using ‹butlast x=ps› by auto then obtain x1 t1 where "x=x1#t1" and "length t1=1" using Suc_length_conv[of 1 x] by auto then obtain x2 where "t1=[x2]" using Suc_length_conv[of 0 t1] by auto have "x=[x1,x2]" using ‹x=x1#t1› ‹t1=[x2]› by auto thus "adjacent (last ps) (last x)" using ‹adj_path (hd x) (tl x)› ‹butlast x=ps› by auto next case False hence "tl ps≠[]" by (metis ‹length ps = l + 1› add_0_iff add_diff_cancel_left' length_0_conv length_tl add.commute) moreover have "adj_path (hd x) (tl ps @ [last x])" using ‹adj_path (hd x) (tl x)› ‹butlast x=ps› ‹x ≠ []› by (metis append_butlast_last_id calculation list.sel(2) tl_append2) ultimately have "adjacent (last (tl ps)) (last x)" using adj_path_app'[of "hd x" "tl ps" "last x"] by auto thus "adjacent (last ps) (last x)" by (metis ‹tl ps ≠ []› last_tl) qed thus "x ∈ app ` qs" using app qs by (metis ‹butlast x = ps› ‹x ≠ []› append_butlast_last_id mem_Collect_eq rev_image_eqI) qed ultimately show ?thesis by auto qed moreover have "inj_on app qs" using app unfolding inj_on_def by auto moreover have "last ps∈V" using ‹length ps = l + 1› ‹adj_path (hd ps) (tl ps)› adj_path_V by (metis ‹last ps = hd ps› adj_path.simps(1) last_in_set last_tl subset_code(1)) hence "card qs=k" using qs k_adj by auto ultimately show "card {ps'. ext ps ps'} = k" by (metis card_image) qed moreover have "finite (C_star l)" proof - have "C_star l ⊆ T l" using C_star T by auto moreover have "(k * k - k + 1) * k ^ l≠0" using ‹k≥4› by auto hence "finite (T l)" using T_count[of "l"] by (metis card.infinite) ultimately show ?thesis by (metis finite_subset) qed moreover have "∀ps1 ps2. ps1 ≠ ps2 ⟶ {ps'. ext ps1 ps'} ∩ {ps'. ext ps2 ps'} = {}" using ext by auto moreover have "(⋃ps∈(C_star l). {ps'. ext ps ps'}) = {ps. length ps = l+2 ∧ adj_path (hd ps) (tl ps) ∧ adjacent (last ps) (hd ps) ∧ last