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'  vV  v'V  vv'  ¬adjacent v v'" 

lemma (in valid_unSimpGraph) no_quad:
  assumes "v u. vV  uV  vu  ∃! n. adjacent v n  adjacent u n"
  shows "¬ (v1 v2 v3 v4. v2v4  v1v3  adjacent v1 v2  adjacent v2 v3  adjacent v3 v4 
       adjacent v4 v1)"
proof
  assume "v1 v2 v3 v4. v2v4   v1v3  adjacent v1 v2  adjacent v2 v3  adjacent v3 v4  adjacent v4 v1"
  then obtain v1 v2 v3 v4 where 
    "v2v4" "v1v3" "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 "xA. f xA  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 "xA" by auto
      hence "f xA" and "f xx" 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 "xB. f x  B  f x  x  f (f x) = x" 
        proof 
          fix y assume "yB"
          hence "yA" using B by auto
          hence "f yy" and "f (f y)=y" by (metis less.prems(2))+
          moreover have "f yB" 
            proof (rule ccontr)
              assume "f yB"
              have "f yA" 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 xA xA by auto
      moreover have "card {x, f x} = 2" using f xx 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. vV  uV  vu  ∃! n. adjacent v n  adjacent u n" 
      and "finite E"
  shows "vV. even(degree v G)"
proof 
  fix v assume "vV"
  obtain f where f:"f = (λn. (SOME v'. nV nvadjacent n v'  adjacent v v'))" by auto
  have "n.  nV  nv  (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] vV  unfolding non_adj_def by auto
      thus "v'. adjacent n v'  adjacent v v'"  by auto
    qed
  hence f_ex:"n.  (v'. nV  nv   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 xx" 
        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 "vf 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. vV  uV  vu  ∃! n. adjacent v n  adjacent u n"
      and "finite E" and "card V2"
  shows "(vV. degree v G = 2) (v. nV. nv  adjacent v n)"
proof 
  assume "vV. 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 "v1v2"
    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 "v1v2" 
        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 "nv1" 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:"xV. x{n. adjacent v1 n}  {n. adjacent v2 n}"
    proof 
      fix x assume "xV"
      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 "xv  x  {n. adjacent v1 n}  {n. adjacent v2 n}" 
        proof -
          assume "xv"
          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. nV. 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. nV. 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 "av" 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 v1v2 by auto
        qed
      moreover have "abFalse"
        proof -
          assume "ab"
          moreover have "aV" using a by (metis DiffD1 adjacent_V(2) mem_Collect_eq)
          moreover have "bV" 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 "cv2" 
                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 "bv1" 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 "cv1" 
                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 "av2" 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. nV. n  v  adjacent v n" by auto
next
  assume "v. nV. n  v  adjacent v n"
  then obtain v where v:"nV. n  v  adjacent v n" by auto
  obtain v1 where "v1V" "v1v" 
    proof (cases "vV") 
      case False
      have "V{}" using 2card V by auto 
      then obtain v1 where "v1V" 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 2card V 
        by (metis add_leE card.infinite not_one_le_zero numeral_Bit0 numeral_One)
      ultimately have "1card S" 
        using 2card V  card.insert[of S v]  finite_insert[of v S] by auto
      hence "S{}" by auto
      then obtain v1 where "v1S" by auto
      hence "v1v" using vS by auto
      thus thesis using that[of v1] v1S V=insert v S by auto
    qed
  hence "vV" 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 G2  False" 
    proof -
      assume "degree v1 G2"
      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 "vv2" 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 "v1v" using v1  v .
      moreover have "v3v2" by (metis v3  {v, v2} insert_subset subset_insertI)
      ultimately show False using no_quad[OF friend_assm] by auto
    qed
  thus "vV. degree v G = 2" using v1V by auto
qed

lemma (in valid_unSimpGraph) regular:
  assumes friend_assm:"v u. vV  uV  vu  ∃! n. adjacent v n  adjacent u n" 
      and "finite E" and "finite V" and "¬(vV. degree v G = 2)"
  shows "k. vV. 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'. nV nuadjacent n v'  adjacent u v'))" by auto
    have "n.  nV  nu  (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'. nV  nu   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 "¬ (xv_adj. yv_adj. f x = f y  x = y)"
        then obtain x y where "xv_adj" "yv_adj" "f x=f y" "xy" by auto
        have "xV" by (metis x  v_adj adjacent_V(2) mem_Collect_eq v_adj)
        moreover have "xu" 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 "yV" by (metis y  v_adj adjacent_V(2) mem_Collect_eq v_adj) 
        moreover have "yu" 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 xv_adj yv_adj f x=f y xy 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 "xv_adj_u"
        then obtain y where "yv_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 "yV" by (metis y  v_adj adjacent_V(2) mem_Collect_eq v_adj) 
        moreover have "yu" 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 "xu_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}" "v1v2" "v2v3" "v1v3"
        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 "v1v2" "v2v3" "v1v3"using VS1 S1S2 v1S1 v2S2 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] v2v3 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] v1v3 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] v1v2 by auto
        qed
      ultimately show "vV. 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}" "v1v2"
        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 "v1v2" using v1S1 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 "v3v2" and "v3v1" by (metis adjacent_no_loop)+
      hence "v3V" 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  "vV. 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 V4"
      hence non_non_adj:"v u. vV  uV  v=u  adjacent v u" unfolding non_adj_def by auto
      obtain v1 v2 v3 v4 where "v1V" "v2V" "v3V" "v4V" "v1v2" "v1v3" "v1v4"
              "v2v3" "v2v4" "v3v4" 
        proof -
          obtain v1 B1 where "V = insert v1 B1"  "v1  B1"  "card B1 3"
            using card V4 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" "v3B3" "card B31"
            using card_le_Suc_iff[of 1 B2] by auto
          then obtain v4 B4 where "B3=insert v4 B4" "v4B4" 
            using card_le_Suc_iff[of 0 B3] by auto
          have "v1V" by (metis V = insert v1 B1 insert_subset order_refl)
          moreover have "v2V" 
            by (metis B1 = insert v2 B2 V = insert v1 B1 insert_subset subset_insertI)
          moreover have "v3V" 
            by (metis B1 = insert v2 B2 B2 = insert v3 B3 V = insert v1 B1 insert_iff)
          moreover have "v4V" 
            by (metis B1 = insert v2 B2 B2 = insert v3 B3 B3 = insert v4 B4 
              V = insert v1 B1 insert_iff)
          moreover have "v1v2" 
            by (metis (full_types) B1 = insert v2 B2 v1  B1 insertI1)
          moreover have "v1v3" 
            by (metis B1 = insert v2 B2 B2 = insert v3 B3 v1  B1 insert_iff)
          moreover have "v1v4" 
            by (metis B1 = insert v2 B2 B2 = insert v3 B3 B3 = insert v4 B4 v1  B1 
              insert_iff)
          moreover have "v2v3" 
            by (metis (full_types) B2 = insert v3 B3 v2  B2 insertI1)
          moreover have "v2v4" 
            by (metis B2 = insert v3 B3 B3 = insert v4 B4 v2  B2 insert_iff)
          moreover have "v3v4" 
            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 V4  (v u. non_adj v u)  ?thesis" 
    proof - 
      assume "(v u. non_adj v u)" "card V4"
      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 "nV. degree n G = degree v G" 
        proof 
          fix n assume "nV"
          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 "nv  nu  nw  degree n G = degree v G" 
            proof -
              assume "nv" "nu" "nw"
              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. nV. nv  adjacent v n)" 
                using card V4 degree_two_windmill assms(2) assms(4) friend_assm
                by auto
              ultimately obtain w1 where "w1V" "w1w" "non_adj w w1"
                by (metis nV 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 "w1u  w1v  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 [] =  (vV)" 
  | "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 "vA. card {n. R v n} = k" "k>0" "finite A" 
      "v1 v2. v1v2  {n. R v1 n}  {n. R v2 n}={}"
  shows "card (vA. {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 "v1A" "C1={n. R v1 n}" by (metis C1  (λx. {n. R x n}) ` A imageE)
      obtain v2 where "v2A" "C2={n. R v2 n}" by (metis C2  (λx. {n. R x n}) ` A imageE)
      have "v1v2" 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) = (xA. {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. v1v2  {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. vV  card {n. adjacent v n} = k" and  "vV" 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 vV 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 vV] 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. ps1ps2  {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. vV  uV  vu  ∃! n. adjacent v n  adjacent u n" 
      and "finite E" and "finite V" and "V{}" and " vV. degree v G = k" and "k>0"
  shows "card V= k*k - k +1"
proof -
  have k_adj:"v. vVcard ({n. adjacent v n})=k" by (metis assms(2) assms(5) degree_adjacent) 
  obtain v where "vV" 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. xhds  x {n. adjacent v n}" 
            proof 
              fix x assume "xhds"
              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}  xhds" 
            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 "xhds" 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 vV] 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 psv}" 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 vV
        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. nV  nv}" 
    proof -
      have "last ` l2_neq_v = {n. nV  nv}" 
        proof -
          have "x. x last` l2_neq_v  x{n. nV  nv}" 
            proof 
              fix x assume "xlast` l2_neq_v"
              then obtain ps where "length ps = 2"  "adj_path v ps" "last ps=x" "last psv"
                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 psv by auto
            qed
          moreover have "x. x{n. nV  nv}  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] vV 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 xv" and "length y=2" and "adj_path v y"
              and "last yv"
            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 "x2v" and "y2v" using last xv last yv by auto
          moreover have "adjacent v x1" and "adjacent x2 x1" and "x2V"
            using adj_path v x x adjacent_sym by auto
          moreover have "adjacent v y1" and "adjacent y2 y1" and "y2V"
            using adj_path v y y adjacent_sym by auto
          ultimately have "x1=y1" using friend_assm vV 
            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. nV  nv}" by (metis bij_betw_same_card)
  ultimately have "card {n. nV  nv}=k*k-k" by auto
  moreover have "card V = card {n. nVnv} + card {v}"
    proof -
      have "V={n. nV  nv}  {v}" using vV by auto
      moreover have "{n. nV  nv}  {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 "n0 ?case" 
    proof -
      assume "n0" 
      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. vV  uV  vu  ∃! n. adjacent v n  adjacent u n"
      and "finite E" and "finite V" and "card V2" 
  shows "vV. degree v G = 2"
proof (rule ccontr)
  assume "¬ (vV. degree v G = 2)"
  hence "v. vV  degree v G2" by auto
  obtain k where k_adj: "v. vV card {n. adjacent v n}=k" using regular[OF friend_assm] 
    by (metis ¬ (vV. degree v G = 2) assms(2) assms(3) degree_adjacent)
  have "k4"
    proof -
      obtain v1 v2 where "v1V" "v2V" "v1v2"
        using card V2 by (metis ¬(vV. degree v G = 2) assms(2) degree_two_windmill)
      have "k0"
        proof 
          assume "k=0"
          obtain v3 where "adjacent v1 v3" using friend_assm[OF v1V v2V v1v2] 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 v1V] 
            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 "k1" and "k3" by auto
      moreover have "k2" using v. vV  degree v G2 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 "vV. card {ps. ext v ps} = k^l" 
        proof 
          fix v assume "v  V" 
          have "ps. pstl ` {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 "(vV. {n. ext v n})=T l" 
        proof -
          have "ps. ps(vV. {n. ext v n})  psT l" using T
            proof -
              fix ps assume "ps(vV. {n. ext v n})"
              then obtain v where "vV" "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 "psT l" using T by auto
            qed
          moreover have "ps. psT l  ps(vV. {n. ext v n})" 
            proof -
              fix ps assume "psT 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" "vV" 
                by (metis adj_path.simps(1) adj_path.simps(2) adjacent_V(1) list.exhaust)
              ultimately show "ps(vV. {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 V2 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 k4 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 "psC_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. xapp`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 psV" 
                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 ^ l0" using k4 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