Theory Birthday_Paradox

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

section ‹A Formulation of the Birthday Paradox›

theory Birthday_Paradox
imports Main "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[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 prod_constant)
qed

lemma prod_upto_nat_unfold:
  "prod f {m..(n::nat)} = (if n < m then 1 else (if n = 0 then f 0 else f n * prod 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 prod_upto_nat_unfold prod_constant)
qed

end