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 "\x \ S. finite (T x)" ``` bulwahn@40632 ` 16` ``` shows "card {(x, y). x \ S \ y \ T x} = (\x \ S. card (T x))" ``` bulwahn@40632 ` 17` ```proof - ``` bulwahn@40632 ` 18` ``` note `finite S` ``` bulwahn@40632 ` 19` ``` moreover ``` bulwahn@40632 ` 20` ``` have "{(x, y). x \ S \ y \ T x} = (UN x : S. Pair x ` T x)" by auto ``` bulwahn@40632 ` 21` ``` moreover ``` bulwahn@40632 ` 22` ``` from `\x \ S. finite (T x)` have "ALL x:S. finite (Pair x ` T x)" by auto ``` bulwahn@40632 ` 23` ``` moreover ``` bulwahn@40632 ` 24` ``` have " ALL i:S. ALL j:S. i ~= j --> Pair i ` T i Int Pair j ` T j = {}" by auto ``` bulwahn@40632 ` 25` ``` moreover ``` bulwahn@40632 ` 26` ``` ultimately have "card {(x, y). x \ S \ y \ T x} = (SUM i:S. card (Pair i ` T i))" ``` bulwahn@40632 ` 27` ``` by (auto, subst card_UN_disjoint) auto ``` bulwahn@40632 ` 28` ``` also have "... = (SUM x:S. card (T x))" ``` bulwahn@40632 ` 29` ``` by (subst card_image) (auto intro: inj_onI) ``` bulwahn@40632 ` 30` ``` finally show ?thesis by auto ``` bulwahn@40632 ` 31` ```qed ``` bulwahn@40632 ` 32` bulwahn@40632 ` 33` ```lemma card_extensional_funcset_inj_on: ``` bulwahn@40632 ` 34` ``` assumes "finite S" "finite T" "card S \ card T" ``` bulwahn@40632 ` 35` ``` shows "card {f \ extensional_funcset S T. inj_on f S} = fact (card T) div (fact (card T - card S))" ``` bulwahn@40632 ` 36` ```using assms ``` bulwahn@40632 ` 37` ```proof (induct S arbitrary: T rule: finite_induct) ``` bulwahn@40632 ` 38` ``` case empty ``` bulwahn@40632 ` 39` ``` from this show ?case by (simp add: Collect_conv_if extensional_funcset_empty_domain) ``` bulwahn@40632 ` 40` ```next ``` bulwahn@40632 ` 41` ``` case (insert x S) ``` bulwahn@40632 ` 42` ``` { fix x ``` bulwahn@40632 ` 43` ``` from `finite T` have "finite (T - {x})" by auto ``` bulwahn@40632 ` 44` ``` from `finite S` this have "finite (extensional_funcset S (T - {x}))" ``` bulwahn@40632 ` 45` ``` by (rule finite_extensional_funcset) ``` bulwahn@40632 ` 46` ``` moreover ``` bulwahn@40632 ` 47` ``` have "{f : extensional_funcset S (T - {x}). inj_on f S} \ (extensional_funcset S (T - {x}))" by auto ``` bulwahn@40632 ` 48` ``` ultimately have "finite {f : extensional_funcset S (T - {x}). inj_on f S}" ``` bulwahn@40632 ` 49` ``` by (auto intro: finite_subset) ``` bulwahn@40632 ` 50` ``` } note finite_delete = this ``` bulwahn@40632 ` 51` ``` 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 ``` bulwahn@40632 ` 52` ``` from extensional_funcset_extend_domain_inj_on_eq[OF `x \ S`] ``` bulwahn@40632 ` 53` ``` have "card {f. f : extensional_funcset (insert x S) T & inj_on f (insert x S)} = ``` bulwahn@40632 ` 54` ``` card ((%(y, g). g(x := y)) ` {(y, g). y : T & g : extensional_funcset S (T - {y}) & inj_on g S})" ``` bulwahn@40632 ` 55` ``` by metis ``` bulwahn@40632 ` 56` ``` 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}" ``` bulwahn@40632 ` 57` ``` by (simp add: card_image) ``` bulwahn@40632 ` 58` ``` also have "card {(y, g). y \ T \ g \ extensional_funcset S (T - {y}) \ inj_on g S} = ``` bulwahn@40632 ` 59` ``` card {(y, g). y \ T \ g \ {f \ extensional_funcset S (T - {y}). inj_on f S}}" by auto ``` bulwahn@40632 ` 60` ``` also from `finite T` finite_delete have "... = (\y \ T. card {g. g \ extensional_funcset S (T - {y}) \ inj_on g S})" ``` bulwahn@40632 ` 61` ``` by (subst card_product_dependent) auto ``` bulwahn@40632 ` 62` ``` also from hyps have "... = (card T) * ?k" ``` bulwahn@40632 ` 63` ``` by auto ``` bulwahn@40632 ` 64` ``` also have "... = card T * fact (card T - 1) div fact (card T - card (insert x S))" ``` bulwahn@40632 ` 65` ``` using insert unfolding div_mult1_eq[of "card T" "fact (card T - 1)"] ``` bulwahn@40632 ` 66` ``` by (simp add: fact_mod) ``` bulwahn@40632 ` 67` ``` also have "... = fact (card T) div fact (card T - card (insert x S))" ``` bulwahn@40632 ` 68` ``` using insert by (simp add: fact_reduce_nat[of "card T"]) ``` bulwahn@40632 ` 69` ``` finally show ?case . ``` bulwahn@40632 ` 70` ```qed ``` bulwahn@40632 ` 71` bulwahn@40632 ` 72` ```lemma card_extensional_funcset_not_inj_on: ``` bulwahn@40632 ` 73` ``` assumes "finite S" "finite T" "card S \ card T" ``` bulwahn@40632 ` 74` ``` shows "card {f \ extensional_funcset S T. \ inj_on f S} = (card T) ^ (card S) - (fact (card T)) div (fact (card T - card S))" ``` bulwahn@40632 ` 75` ```proof - ``` bulwahn@40632 ` 76` ``` have subset: "{f : extensional_funcset S T. inj_on f S} <= extensional_funcset S T" by auto ``` bulwahn@40632 ` 77` ``` from finite_subset[OF subset] assms have finite: "finite {f : extensional_funcset S T. inj_on f S}" ``` bulwahn@40632 ` 78` ``` by (auto intro!: finite_extensional_funcset) ``` bulwahn@40632 ` 79` ``` 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 ``` bulwahn@40632 ` 80` ``` from assms this finite subset show ?thesis ``` bulwahn@40632 ` 81` ``` by (simp add: card_Diff_subset card_extensional_funcset card_extensional_funcset_inj_on) ``` bulwahn@40632 ` 82` ```qed ``` bulwahn@40632 ` 83` bulwahn@40632 ` 84` ```lemma setprod_upto_nat_unfold: ``` bulwahn@40632 ` 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)}))" ``` bulwahn@40632 ` 86` ``` by auto (auto simp add: gr0_conv_Suc atLeastAtMostSuc_conv) ``` bulwahn@40632 ` 87` bulwahn@43238 ` 88` ```section {* Birthday paradox *} ``` bulwahn@40632 ` 89` bulwahn@43238 ` 90` ```lemma birthday_paradox: ``` bulwahn@40632 ` 91` ``` assumes "card S = 23" "card T = 365" ``` bulwahn@40632 ` 92` ``` shows "2 * card {f \ extensional_funcset S T. \ inj_on f S} \ card (extensional_funcset S T)" ``` bulwahn@40632 ` 93` ```proof - ``` bulwahn@40632 ` 94` ``` 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 ` 95` ``` from assms show ?thesis ``` bulwahn@40632 ` 96` ``` using card_extensional_funcset[OF `finite S`, of T] ``` bulwahn@40632 ` 97` ``` card_extensional_funcset_not_inj_on[OF `finite S` `finite T` `card S <= card T`] ``` bulwahn@40632 ` 98` ``` by (simp add: fact_div_fact setprod_upto_nat_unfold) ``` bulwahn@40632 ` 99` ```qed ``` bulwahn@40632 ` 100` bulwahn@40632 ` 101` ```end ```