Instantly share code, notes, and snippets.

@jmoy /Friends2.thy
Last active Jul 8, 2018

Embed
What would you like to do?
Solving a puzzle using Isabelle: 2nd attempt
sectionA 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
subsectionSetup
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
subsectionThe number of friends someone has
definition nfriends::"'a⇒nat" where
"nfriends x = card (frnd `` {x})"
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 ‹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
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment