1(* Title: HOL/ex/Birthday_Paradox.thy 2 Author: Lukas Bulwahn, TU Muenchen, 2007 3*) 4 5section \<open>A Formulation of the Birthday Paradox\<close> 6 7theory Birthday_Paradox 8imports Main "HOL-Library.FuncSet" 9begin 10 11section \<open>Cardinality\<close> 12 13lemma 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 using card_SigmaI[OF assms, symmetric] by (auto intro!: arg_cong[where f=card] simp add: Sigma_def) 18 19lemma card_extensional_funcset_inj_on: 20 assumes "finite S" "finite T" "card S \<le> card T" 21 shows "card {f \<in> extensional_funcset S T. inj_on f S} = fact (card T) div (fact (card T - card S))" 22using assms 23proof (induct S arbitrary: T rule: finite_induct) 24 case empty 25 from this show ?case by (simp add: Collect_conv_if PiE_empty_domain) 26next 27 case (insert x S) 28 { fix x 29 from \<open>finite T\<close> have "finite (T - {x})" by auto 30 from \<open>finite S\<close> this have "finite (extensional_funcset S (T - {x}))" 31 by (rule finite_PiE) 32 moreover 33 have "{f : extensional_funcset S (T - {x}). inj_on f S} \<subseteq> (extensional_funcset S (T - {x}))" by auto 34 ultimately have "finite {f : extensional_funcset S (T - {x}). inj_on f S}" 35 by (auto intro: finite_subset) 36 } note finite_delete = this 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 38 from extensional_funcset_extend_domain_inj_on_eq[OF \<open>x \<notin> S\<close>] 39 have "card {f. f \<in> extensional_funcset (insert x S) T \<and> inj_on f (insert x S)} = 40 card ((\<lambda>(y, g). g(x := y)) ` {(y, g). y \<in> T \<and> g \<in> extensional_funcset S (T - {y}) \<and> inj_on g S})" 41 by metis 42 also from extensional_funcset_extend_domain_inj_onI[OF \<open>x \<notin> S\<close>, of T] have "\<dots> = card {(y, g). y \<in> T \<and> g \<in> extensional_funcset S (T - {y}) \<and> inj_on g S}" 43 by (simp add: card_image) 44 also have "card {(y, g). y \<in> T \<and> g \<in> extensional_funcset S (T - {y}) \<and> inj_on g S} = 45 card {(y, g). y \<in> T \<and> g \<in> {f \<in> extensional_funcset S (T - {y}). inj_on f S}}" by auto 46 also from \<open>finite T\<close> finite_delete have "... = (\<Sum>y \<in> T. card {g. g \<in> extensional_funcset S (T - {y}) \<and> inj_on g S})" 47 by (subst card_product_dependent) auto 48 also from hyps have "... = (card T) * ?k" 49 by auto 50 also have "... = card T * fact (card T - 1) div fact (card T - card (insert x S))" 51 using insert unfolding div_mult1_eq[of "card T" "fact (card T - 1)"] 52 by (simp add: fact_mod) 53 also have "... = fact (card T) div fact (card T - card (insert x S))" 54 using insert by (simp add: fact_reduce[of "card T"]) 55 finally show ?case . 56qed 57 58lemma card_extensional_funcset_not_inj_on: 59 assumes "finite S" "finite T" "card S \<le> card T" 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))" 61proof - 62 have subset: "{f : extensional_funcset S T. inj_on f S} <= extensional_funcset S T" by auto 63 from finite_subset[OF subset] assms have finite: "finite {f : extensional_funcset S T. inj_on f S}" 64 by (auto intro!: finite_PiE) 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 66 from assms this finite subset show ?thesis 67 by (simp add: card_Diff_subset card_PiE card_extensional_funcset_inj_on prod_constant) 68qed 69 70lemma prod_upto_nat_unfold: 71 "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)}))" 72 by auto (auto simp add: gr0_conv_Suc atLeastAtMostSuc_conv) 73 74section \<open>Birthday paradox\<close> 75 76lemma birthday_paradox: 77 assumes "card S = 23" "card T = 365" 78 shows "2 * card {f \<in> extensional_funcset S T. \<not> inj_on f S} \<ge> card (extensional_funcset S T)" 79proof - 80 from \<open>card S = 23\<close> \<open>card T = 365\<close> have "finite S" "finite T" "card S <= card T" by (auto intro: card_ge_0_finite) 81 from assms show ?thesis 82 using card_PiE[OF \<open>finite S\<close>, of "\<lambda>i. T"] \<open>finite S\<close> 83 card_extensional_funcset_not_inj_on[OF \<open>finite S\<close> \<open>finite T\<close> \<open>card S <= card T\<close>] 84 by (simp add: fact_div_fact prod_upto_nat_unfold prod_constant) 85qed 86 87end 88