src/HOL/ex/Birthday_Paradox.thy
author bulwahn
Fri Oct 21 11:17:14 2011 +0200 (2011-10-21)
changeset 45231 d85a2fdc586c
parent 43238 04c886a1d1a5
child 50123 69b35a75caf3
permissions -rw-r--r--
replacing code_inline by code_unfold, removing obsolete code_unfold, code_inline del now that the ancient code generator is removed
     1 (*  Title: HOL/ex/Birthday_Paradox.thy
     2     Author: Lukas Bulwahn, TU Muenchen, 2007
     3 *)
     4 
     5 header {* A Formulation of the Birthday Paradox *}
     6 
     7 theory Birthday_Paradox
     8 imports Main "~~/src/HOL/Fact" "~~/src/HOL/Library/FuncSet"
     9 begin
    10 
    11 section {* Cardinality *}
    12 
    13 lemma card_product_dependent:
    14   assumes "finite S"
    15   assumes "\<forall>x \<in> S. finite (T x)" 
    16   shows "card {(x, y). x \<in> S \<and> y \<in> T x} = (\<Sum>x \<in> S. card (T x))"
    17 proof -
    18   note `finite S`
    19   moreover
    20   have "{(x, y). x \<in> S \<and> y \<in> T x} = (UN x : S. Pair x ` T x)" by auto
    21   moreover
    22   from `\<forall>x \<in> S. finite (T x)` have "ALL x:S. finite (Pair x ` T x)" by auto
    23   moreover
    24   have " ALL i:S. ALL j:S. i ~= j --> Pair i ` T i Int Pair j ` T j = {}" by auto
    25   moreover  
    26   ultimately have "card {(x, y). x \<in> S \<and> y \<in> T x} = (SUM i:S. card (Pair i ` T i))"
    27     by (auto, subst card_UN_disjoint) auto
    28   also have "... = (SUM x:S. card (T x))"
    29     by (subst card_image) (auto intro: inj_onI)
    30   finally show ?thesis by auto
    31 qed
    32 
    33 lemma card_extensional_funcset_inj_on:
    34   assumes "finite S" "finite T" "card S \<le> card T"
    35   shows "card {f \<in> extensional_funcset S T. inj_on f S} = fact (card T) div (fact (card T - card S))"
    36 using assms
    37 proof (induct S arbitrary: T rule: finite_induct)
    38   case empty
    39   from this show ?case by (simp add: Collect_conv_if extensional_funcset_empty_domain)
    40 next
    41   case (insert x S)
    42   { fix x
    43     from `finite T` have "finite (T - {x})" by auto
    44     from `finite S` this have "finite (extensional_funcset S (T - {x}))"
    45       by (rule finite_extensional_funcset)
    46     moreover
    47     have "{f : extensional_funcset S (T - {x}). inj_on f S} \<subseteq> (extensional_funcset S (T - {x}))" by auto    
    48     ultimately have "finite {f : extensional_funcset S (T - {x}). inj_on f S}"
    49       by (auto intro: finite_subset)
    50   } note finite_delete = this
    51   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
    52   from extensional_funcset_extend_domain_inj_on_eq[OF `x \<notin> S`]
    53   have "card {f. f : extensional_funcset (insert x S) T & inj_on f (insert x S)} =
    54     card ((%(y, g). g(x := y)) ` {(y, g). y : T & g : extensional_funcset S (T - {y}) & inj_on g S})"
    55     by metis
    56   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}"
    57     by (simp add: card_image)
    58   also have "card {(y, g). y \<in> T \<and> g \<in> extensional_funcset S (T - {y}) \<and> inj_on g S} =
    59     card {(y, g). y \<in> T \<and> g \<in> {f \<in> extensional_funcset S (T - {y}). inj_on f S}}" by auto
    60   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})"
    61     by (subst card_product_dependent) auto
    62   also from hyps have "... = (card T) * ?k"
    63     by auto
    64   also have "... = card T * fact (card T - 1) div fact (card T - card (insert x S))"
    65     using insert unfolding div_mult1_eq[of "card T" "fact (card T - 1)"]
    66     by (simp add: fact_mod)
    67   also have "... = fact (card T) div fact (card T - card (insert x S))"
    68     using insert by (simp add: fact_reduce_nat[of "card T"])
    69   finally show ?case .
    70 qed
    71 
    72 lemma card_extensional_funcset_not_inj_on:
    73   assumes "finite S" "finite T" "card S \<le> card T"
    74   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))"
    75 proof -
    76   have subset: "{f : extensional_funcset S T. inj_on f S} <= extensional_funcset S T" by auto
    77   from finite_subset[OF subset] assms have finite: "finite {f : extensional_funcset S T. inj_on f S}"
    78     by (auto intro!: finite_extensional_funcset)
    79   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 
    80   from assms this finite subset show ?thesis
    81     by (simp add: card_Diff_subset card_extensional_funcset card_extensional_funcset_inj_on)
    82 qed
    83 
    84 lemma setprod_upto_nat_unfold:
    85   "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)}))"
    86   by auto (auto simp add: gr0_conv_Suc atLeastAtMostSuc_conv)
    87 
    88 section {* Birthday paradox *}
    89 
    90 lemma birthday_paradox:
    91   assumes "card S = 23" "card T = 365"
    92   shows "2 * card {f \<in> extensional_funcset S T. \<not> inj_on f S} \<ge> card (extensional_funcset S T)"
    93 proof -
    94   from `card S = 23` `card T = 365` have "finite S" "finite T" "card S <= card T" by (auto intro: card_ge_0_finite)
    95   from assms show ?thesis
    96     using card_extensional_funcset[OF `finite S`, of T]
    97       card_extensional_funcset_not_inj_on[OF `finite S` `finite T` `card S <= card T`]
    98     by (simp add: fact_div_fact setprod_upto_nat_unfold)
    99 qed
   100 
   101 end