Skip to content

Instantly share code, notes, and snippets.

Last active January 29, 2019 02:51
Show Gist options
  • Save jmoy/27bcc72fb5a3f871b72c31e81bccb55f to your computer and use it in GitHub Desktop.
Save jmoy/27bcc72fb5a3f871b72c31e81bccb55f to your computer and use it in GitHub Desktop.
Solving a puzzle using Isabelle: 2nd attempt
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
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›
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)"
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)
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
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment