Solving a puzzle using Isabelle: 2nd attempt

Friends2.thy

section ‹A Simple Graph Problem: Second Attempt›

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 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 ‹The range of the @{term "frnd"} relationship.›
    
    have no_x: "∀ x. frnd `` {x} ⊆ people - {x}" 
      using ass_irr ass_dom
      by (metis Diff_empty Image_singleton_iff Image_subset irrefl_def subset_Diff_insert)

    text ‹A rough bound on the range of @{term "nfriends"}›

    have rng_rough:  "?frnds_rng ⊆ {0..?n-1}" 
      using ass_findom no_x
      by (metis atLeast0AtMost atMost_iff card_Diff_singleton card_mono finite_Diff 
            image_subsetI nfriends_def)

    text ‹n-1 and 0 cannot both be in the range.›
    
    have rng_cases:"¬ (?n-1 ∈ ?frnds_rng ∧ 0 ∈ ?frnds_rng)" 
    proof 
      assume oppo:"?n-1 ∈ ?frnds_rng ∧ 0 ∈ ?frnds_rng"
 
      then obtain x where thex:"x ∈ people ∧ frnd `` {x}  = people - {x}" using no_x
        using ass_findom
        by (metis card_Diff_singleton card_subset_eq finite_Diff imageE nfriends_def)
 
      obtain z where thez:"z ∈ people ∧ frnd `` {z} = {}"
        using oppo ass_findom no_x 
        by (metis card_0_eq finite_Diff imageE finite_subset nfriends_def)

      show False
      proof (contradiction)
        have "x ≠ z" using thex thez ass_findom ass_two
            by (metis One_nat_def card_Suc_Diff1 card_empty less_le)
        thus "(x,z) ∈ frnd" using thex thez by blast
        show "(x,z) ∉ frnd" using thex thez ass_sym
          by (metis Image_singleton_iff empty_iff symE)
      qed
    qed

    have "card ?frnds_rng < ?n" 
        using rng_rough rng_cases ass_two
        by (metis Suc_diff_1 atLeast0AtMost atMost_iff 
                  card_atMost card_eq_0_iff card_image_le card_subset_eq 
                  gr_implies_not0 le0 le_eq_less_or_eq)

    text ‹Finally we can apply the pigeonhole principle›

    thus ?thesis using pigeonhole by auto
  qed
end
end