1 (* Title: HOL/ex/Birthday_Paradoxon.thy |
|
2 Author: Lukas Bulwahn, TU Muenchen, 2007 |
|
3 *) |
|
4 |
|
5 header {* A Formulation of the Birthday Paradoxon *} |
|
6 |
|
7 theory Birthday_Paradoxon |
|
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 paradoxon *} |
|
89 |
|
90 lemma birthday_paradoxon: |
|
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 |
|