# Theory FriendshipTheory

```(*
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›
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]
moreover have "f x≠x"
using someI_ex[OF f_ex,of x]
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}"
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 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
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)
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
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"
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}"
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}"
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}"
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"
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"
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"
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"
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'
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 ```