src/HOL/ex/Birthday_Paradox.thy
author haftmann
Fri Oct 10 19:55:32 2014 +0200 (2014-10-10)
changeset 58646 cd63a4b12a33
parent 50123 69b35a75caf3
child 58889 5b7a9633cfa8
permissions -rw-r--r--
specialized specification: avoid trivial instances
bulwahn@43238
     1
(*  Title: HOL/ex/Birthday_Paradox.thy
bulwahn@40632
     2
    Author: Lukas Bulwahn, TU Muenchen, 2007
bulwahn@40632
     3
*)
bulwahn@40632
     4
bulwahn@43238
     5
header {* A Formulation of the Birthday Paradox *}
bulwahn@40632
     6
bulwahn@43238
     7
theory Birthday_Paradox
bulwahn@40632
     8
imports Main "~~/src/HOL/Fact" "~~/src/HOL/Library/FuncSet"
bulwahn@40632
     9
begin
bulwahn@40632
    10
bulwahn@40632
    11
section {* Cardinality *}
bulwahn@40632
    12
bulwahn@40632
    13
lemma card_product_dependent:
bulwahn@40632
    14
  assumes "finite S"
bulwahn@40632
    15
  assumes "\<forall>x \<in> S. finite (T x)" 
bulwahn@40632
    16
  shows "card {(x, y). x \<in> S \<and> y \<in> T x} = (\<Sum>x \<in> S. card (T x))"
hoelzl@50123
    17
  using card_SigmaI[OF assms, symmetric] by (auto intro!: arg_cong[where f=card] simp add: Sigma_def)
bulwahn@40632
    18
bulwahn@40632
    19
lemma card_extensional_funcset_inj_on:
bulwahn@40632
    20
  assumes "finite S" "finite T" "card S \<le> card T"
bulwahn@40632
    21
  shows "card {f \<in> extensional_funcset S T. inj_on f S} = fact (card T) div (fact (card T - card S))"
bulwahn@40632
    22
using assms
bulwahn@40632
    23
proof (induct S arbitrary: T rule: finite_induct)
bulwahn@40632
    24
  case empty
hoelzl@50123
    25
  from this show ?case by (simp add: Collect_conv_if PiE_empty_domain)
bulwahn@40632
    26
next
bulwahn@40632
    27
  case (insert x S)
bulwahn@40632
    28
  { fix x
bulwahn@40632
    29
    from `finite T` have "finite (T - {x})" by auto
bulwahn@40632
    30
    from `finite S` this have "finite (extensional_funcset S (T - {x}))"
hoelzl@50123
    31
      by (rule finite_PiE)
bulwahn@40632
    32
    moreover
bulwahn@40632
    33
    have "{f : extensional_funcset S (T - {x}). inj_on f S} \<subseteq> (extensional_funcset S (T - {x}))" by auto    
bulwahn@40632
    34
    ultimately have "finite {f : extensional_funcset S (T - {x}). inj_on f S}"
bulwahn@40632
    35
      by (auto intro: finite_subset)
bulwahn@40632
    36
  } note finite_delete = this
bulwahn@40632
    37
  from insert have hyps: "\<forall>y \<in> T. card ({g. g \<in> extensional_funcset S (T - {y}) \<and> inj_on g S}) = fact (card T - 1) div fact ((card T - 1) - card S)"(is "\<forall> _ \<in> T. _ = ?k") by auto
bulwahn@40632
    38
  from extensional_funcset_extend_domain_inj_on_eq[OF `x \<notin> S`]
bulwahn@40632
    39
  have "card {f. f : extensional_funcset (insert x S) T & inj_on f (insert x S)} =
bulwahn@40632
    40
    card ((%(y, g). g(x := y)) ` {(y, g). y : T & g : extensional_funcset S (T - {y}) & inj_on g S})"
bulwahn@40632
    41
    by metis
bulwahn@40632
    42
  also from extensional_funcset_extend_domain_inj_onI[OF `x \<notin> S`, of T] have "... =  card {(y, g). y : T & g : extensional_funcset S (T - {y}) & inj_on g S}"
bulwahn@40632
    43
    by (simp add: card_image)
bulwahn@40632
    44
  also have "card {(y, g). y \<in> T \<and> g \<in> extensional_funcset S (T - {y}) \<and> inj_on g S} =
bulwahn@40632
    45
    card {(y, g). y \<in> T \<and> g \<in> {f \<in> extensional_funcset S (T - {y}). inj_on f S}}" by auto
bulwahn@40632
    46
  also from `finite T` finite_delete have "... = (\<Sum>y \<in> T. card {g. g \<in> extensional_funcset S (T - {y}) \<and>  inj_on g S})"
bulwahn@40632
    47
    by (subst card_product_dependent) auto
bulwahn@40632
    48
  also from hyps have "... = (card T) * ?k"
bulwahn@40632
    49
    by auto
bulwahn@40632
    50
  also have "... = card T * fact (card T - 1) div fact (card T - card (insert x S))"
bulwahn@40632
    51
    using insert unfolding div_mult1_eq[of "card T" "fact (card T - 1)"]
bulwahn@40632
    52
    by (simp add: fact_mod)
bulwahn@40632
    53
  also have "... = fact (card T) div fact (card T - card (insert x S))"
bulwahn@40632
    54
    using insert by (simp add: fact_reduce_nat[of "card T"])
bulwahn@40632
    55
  finally show ?case .
bulwahn@40632
    56
qed
bulwahn@40632
    57
bulwahn@40632
    58
lemma card_extensional_funcset_not_inj_on:
bulwahn@40632
    59
  assumes "finite S" "finite T" "card S \<le> card T"
bulwahn@40632
    60
  shows "card {f \<in> extensional_funcset S T. \<not> inj_on f S} = (card T) ^ (card S) - (fact (card T)) div (fact (card T - card S))"
bulwahn@40632
    61
proof -
bulwahn@40632
    62
  have subset: "{f : extensional_funcset S T. inj_on f S} <= extensional_funcset S T" by auto
bulwahn@40632
    63
  from finite_subset[OF subset] assms have finite: "finite {f : extensional_funcset S T. inj_on f S}"
hoelzl@50123
    64
    by (auto intro!: finite_PiE)
bulwahn@40632
    65
  have "{f \<in> extensional_funcset S T. \<not> inj_on f S} = extensional_funcset S T - {f \<in> extensional_funcset S T. inj_on f S}" by auto 
bulwahn@40632
    66
  from assms this finite subset show ?thesis
hoelzl@50123
    67
    by (simp add: card_Diff_subset card_PiE card_extensional_funcset_inj_on setprod_constant)
bulwahn@40632
    68
qed
bulwahn@40632
    69
bulwahn@40632
    70
lemma setprod_upto_nat_unfold:
bulwahn@40632
    71
  "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)}))"
bulwahn@40632
    72
  by auto (auto simp add: gr0_conv_Suc atLeastAtMostSuc_conv)
bulwahn@40632
    73
bulwahn@43238
    74
section {* Birthday paradox *}
bulwahn@40632
    75
bulwahn@43238
    76
lemma birthday_paradox:
bulwahn@40632
    77
  assumes "card S = 23" "card T = 365"
bulwahn@40632
    78
  shows "2 * card {f \<in> extensional_funcset S T. \<not> inj_on f S} \<ge> card (extensional_funcset S T)"
bulwahn@40632
    79
proof -
bulwahn@40632
    80
  from `card S = 23` `card T = 365` have "finite S" "finite T" "card S <= card T" by (auto intro: card_ge_0_finite)
bulwahn@40632
    81
  from assms show ?thesis
hoelzl@50123
    82
    using card_PiE[OF `finite S`, of "\<lambda>i. T"] `finite S`
bulwahn@40632
    83
      card_extensional_funcset_not_inj_on[OF `finite S` `finite T` `card S <= card T`]
hoelzl@50123
    84
    by (simp add: fact_div_fact setprod_upto_nat_unfold setprod_constant)
bulwahn@40632
    85
qed
bulwahn@40632
    86
bulwahn@40632
    87
end