Solving a puzzle using the Isabelle proof assistant

Friends.thy

section ‹A Simple Graph Problem›

text ‹
We shall prove the following: "In a finite group of people, some of whom are friends with some
of the others there must be at least two people who have the same number of friends."
›

theory Friends
  imports   Main 
            Finite_Set 
            Relation
begin

subsection ‹Setup›

locale Friends =
  fixes people::"'a set"                          -- ‹The set of individuals›
    and frnd::"'a rel"                            -- ‹The friendship relation›
  assumes ass_findom: "finite people"             -- ‹Finite number of individuals›
    and ass_two:      "card people > 1"           -- ‹At least two individual›
    and ass_dom:      "frnd ⊆ people × people"   -- ‹The domain of the friendship relation›
    and ass_irr:      "irrefl frnd"               -- ‹Friendship is irreflexive›
    and ass_sym:      "sym frnd"                  -- ‹Friendship is symmetric›
begin

subsection ‹The number of friends someone has›

definition nfriends::"'a⇒nat" where
  "nfriends x = card (frnd `` {x})"

subsection ‹The range of the @{term "frnd"} relationship.›

lemma no_x:"∀ x. frnd `` {x} ⊆ people - {x}"
proof
 fix x
 show "frnd `` {x} ⊆ people - {x}"
 proof (-)
   have s1: "frnd `` {x} ⊆ people" using ass_dom by blast
   have "x ∉ frnd `` {x}" using ass_irr by (simp add:irrefl_def)
   thus ?thesis using s1 by blast
 qed
qed

subsection ‹The main theorem.›

text‹ @{term "nfriends"} is not a injective function on @{term "people"}›

theorem "¬ inj_on nfriends people"
proof (-)
  text ‹We do a proof by using the pigeon hole principle. 
        @{term "nfriends"} takes on values between $0$ and $n-1$
        where $n$ is the number of individuals (the value $n$ being ruled out by irreflexibility. 
        These are exactly $n$ values. However @{term "nfriends} cannot take on both the values
        $n-1$ and $0$ since if it takes on the value $n-1$ then there is someone who has
        everyone else as their friend and so no one can have $0$ friends. Thus
        @{term "nfriends"} can take on at most $n-1$ values, so it must take on at
        least one value twice› 

    let ?n = "card people"                -- ‹Number of people›
    let ?frnds_rng = "nfriends ` people"  -- ‹The range of the nfriends function›

    text ‹A rough bound on the range of @{term "nfriends"}›
    
    have rng_rough:  "?frnds_rng ⊆ {0..?n-1}"
    proof (-)
      have "∀x ∈ people. nfriends x ≤ ?n-1" using no_x ass_findom
            by (metis card_Diff_singleton card_mono finite_Diff nfriends_def)
      thus ?thesis using atLeastAtMost_iff by blast
    qed

    text ‹Two possibilities for a stricter bound.›

    have rng_cases:"?n-1 ∈ ?frnds_rng ⟶ 0 ∉ ?frnds_rng"
    proof
      assume popular_guy:"?n-1 ∈ ?frnds_rng"
      then show " 0 ∉ ?frnds_rng"
      proof
        obtain x where thex:"x∈people ∧ nfriends x = ?n-1" using popular_guy by auto
        hence "frnd `` {x} = people-{x}" using no_x 
          by (simp add: ass_findom card_subset_eq nfriends_def)
        hence  "∀ z∈people. z ≠ x ⟶ (x,z) ∈ frnd" by blast
        hence "∀ z ∈ people. z ≠ x ⟶ frnd `` {z} ≠ {}" using ass_sym
          by (metis Image_singleton_iff empty_iff symE)
        hence "∀ z ∈ people. z ≠ x ⟶ nfriends z ≠ 0"
          by (metis ass_findom card_0_eq finite_Diff nfriends_def no_x rev_finite_subset)
        hence "∀ z ∈ people. nfriends z ≠ 0" using ass_two thex by auto
        hence "0 ∉ ?frnds_rng" using rng_rough by auto
        thus ?thesis by blast
      qed
    qed

    text ‹The cardinality result we need to apply the pigeonhole principle holds in either case›

    have "card ?frnds_rng < ?n" 
    proof (cases "?n-1 ∈ ?frnds_rng")
      case True
      hence "0 ∉ ?frnds_rng" using rng_cases by simp
      hence "?frnds_rng ⊆ {0..?n-1}-{0}" using rng_rough by auto
      hence st:"card ?frnds_rng ≤ card ({0..?n-1}-{0})"
        by (meson card_mono finite_Diff finite_atLeastAtMost)
      have ct:"card ({0..?n-1}-{0})<?n" 
          using ass_two by auto
      show ?thesis using st ct
          using le_less_trans by blast
    next
      case False
      hence "?frnds_rng ⊆ {0..?n-1}-{?n-1}" using rng_rough by blast
      hence sf:"card ?frnds_rng ≤ card ({0..?n-1}-{?n-1})"
          by (meson card_mono finite_Diff finite_atLeastAtMost)
      have cf:"card ({0..?n-1}-{?n-1})<?n"
          using ass_two by auto
      show ?thesis using sf cf
          using le_less_trans by blast
    qed

    text ‹Finally we can apply the pigeonhole principle›

    thus ?thesis using pigeonhole by auto
  qed
end
end