Skip to content

Instantly share code, notes, and snippets.



Last active Aug 16, 2019
What would you like to do?
Solving a puzzle using the Isabelle proof assistant
sectionA Simple Graph Problem
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
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
subsectionThe number of friends someone has
definition nfriends::"'a⇒nat" where
"nfriends x = card (frnd `` {x})"
subsectionThe range of the @{term "frnd"} relationship.
lemma no_x:"∀ x. frnd `` {x} ⊆ people - {x}"
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
subsectionThe main theorem.
text‹ @{term "nfriends"} is not a injective function on @{term "people"}
theorem "¬ inj_on nfriends people"
proof (-)
textWe 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
text ‹Two possibilities for a stricter bound.›
have rng_cases:"?n-1 ∈ ?frnds_rng ⟶ 0 ∉ ?frnds_rng"
assume popular_guy:"?n-1 ∈ ?frnds_rng"
then show " 0 ∉ ?frnds_rng"
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
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
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
text ‹Finally we can apply the pigeonhole principle›
thus ?thesis using pigeonhole by auto
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment