Theory Birthday_Paradox

theory Birthday_Paradox
imports Fact FuncSet
(*  Title: HOL/ex/Birthday_Paradox.thy
Author: Lukas Bulwahn, TU Muenchen, 2007
*)


header {* A Formulation of the Birthday Paradox *}

theory Birthday_Paradox
imports Main "~~/src/HOL/Fact" "~~/src/HOL/Library/FuncSet"
begin

section {* Cardinality *}

lemma card_product_dependent:
assumes "finite S"
assumes "∀x ∈ S. finite (T x)"
shows "card {(x, y). x ∈ S ∧ y ∈ T x} = (∑x ∈ S. card (T x))"
using card_SigmaI[OF assms, symmetric] by (auto intro!: arg_cong[where f=card] simp add: Sigma_def)

lemma card_extensional_funcset_inj_on:
assumes "finite S" "finite T" "card S ≤ card T"
shows "card {f ∈ extensional_funcset S T. inj_on f S} = fact (card T) div (fact (card T - card S))"
using assms
proof (induct S arbitrary: T rule: finite_induct)
case empty
from this show ?case by (simp add: Collect_conv_if PiE_empty_domain)
next
case (insert x S)
{ fix x
from `finite T` have "finite (T - {x})" by auto
from `finite S` this have "finite (extensional_funcset S (T - {x}))"
by (rule finite_PiE)
moreover
have "{f : extensional_funcset S (T - {x}). inj_on f S} ⊆ (extensional_funcset S (T - {x}))" by auto
ultimately have "finite {f : extensional_funcset S (T - {x}). inj_on f S}"
by (auto intro: finite_subset)
} note finite_delete = this
from insert have hyps: "∀y ∈ T. card ({g. g ∈ extensional_funcset S (T - {y}) ∧ inj_on g S}) = fact (card T - 1) div fact ((card T - 1) - card S)"(is "∀ _ ∈ T. _ = ?k") by auto
from extensional_funcset_extend_domain_inj_on_eq[OF `x ∉ S`]
have "card {f. f : extensional_funcset (insert x S) T & inj_on f (insert x S)} =
card ((%(y, g). g(x := y)) ` {(y, g). y : T & g : extensional_funcset S (T - {y}) & inj_on g S})"

by metis
also from extensional_funcset_extend_domain_inj_onI[OF `x ∉ S`, of T] have "... = card {(y, g). y : T & g : extensional_funcset S (T - {y}) & inj_on g S}"
by (simp add: card_image)
also have "card {(y, g). y ∈ T ∧ g ∈ extensional_funcset S (T - {y}) ∧ inj_on g S} =
card {(y, g). y ∈ T ∧ g ∈ {f ∈ extensional_funcset S (T - {y}). inj_on f S}}"
by auto
also from `finite T` finite_delete have "... = (∑y ∈ T. card {g. g ∈ extensional_funcset S (T - {y}) ∧ inj_on g S})"
by (subst card_product_dependent) auto
also from hyps have "... = (card T) * ?k"
by auto
also have "... = card T * fact (card T - 1) div fact (card T - card (insert x S))"
using insert unfolding div_mult1_eq[of "card T" "fact (card T - 1)"]
by (simp add: fact_mod)
also have "... = fact (card T) div fact (card T - card (insert x S))"
using insert by (simp add: fact_reduce_nat[of "card T"])
finally show ?case .
qed

lemma card_extensional_funcset_not_inj_on:
assumes "finite S" "finite T" "card S ≤ card T"
shows "card {f ∈ extensional_funcset S T. ¬ inj_on f S} = (card T) ^ (card S) - (fact (card T)) div (fact (card T - card S))"
proof -
have subset: "{f : extensional_funcset S T. inj_on f S} <= extensional_funcset S T" by auto
from finite_subset[OF subset] assms have finite: "finite {f : extensional_funcset S T. inj_on f S}"
by (auto intro!: finite_PiE)
have "{f ∈ extensional_funcset S T. ¬ inj_on f S} = extensional_funcset S T - {f ∈ extensional_funcset S T. inj_on f S}" by auto
from assms this finite subset show ?thesis
by (simp add: card_Diff_subset card_PiE card_extensional_funcset_inj_on setprod_constant)
qed

lemma setprod_upto_nat_unfold:
"setprod f {m..(n::nat)} = (if n < m then 1 else (if n = 0 then f 0 else f n * setprod f {m..(n - 1)}))"
by auto (auto simp add: gr0_conv_Suc atLeastAtMostSuc_conv)

section {* Birthday paradox *}

lemma birthday_paradox:
assumes "card S = 23" "card T = 365"
shows "2 * card {f ∈ extensional_funcset S T. ¬ inj_on f S} ≥ card (extensional_funcset S T)"
proof -
from `card S = 23` `card T = 365` have "finite S" "finite T" "card S <= card T" by (auto intro: card_ge_0_finite)
from assms show ?thesis
using card_PiE[OF `finite S`, of "λi. T"] `finite S`
card_extensional_funcset_not_inj_on[OF `finite S` `finite T` `card S <= card T`]
by (simp add: fact_div_fact setprod_upto_nat_unfold setprod_constant)
qed

end