40632
|
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
|