1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/HOL/ex/Birthday_Paradoxon.thy Mon Nov 22 10:41:52 2010 +0100
1.3 @@ -0,0 +1,101 @@
1.4 +(* Title: HOL/ex/Birthday_Paradoxon.thy
1.5 + Author: Lukas Bulwahn, TU Muenchen, 2007
1.6 +*)
1.7 +
1.8 +header {* A Formulation of the Birthday Paradoxon *}
1.9 +
1.10 +theory Birthday_Paradoxon
1.11 +imports Main "~~/src/HOL/Fact" "~~/src/HOL/Library/FuncSet"
1.12 +begin
1.13 +
1.14 +section {* Cardinality *}
1.15 +
1.16 +lemma card_product_dependent:
1.17 + assumes "finite S"
1.18 + assumes "\<forall>x \<in> S. finite (T x)"
1.19 + shows "card {(x, y). x \<in> S \<and> y \<in> T x} = (\<Sum>x \<in> S. card (T x))"
1.20 +proof -
1.21 + note `finite S`
1.22 + moreover
1.23 + have "{(x, y). x \<in> S \<and> y \<in> T x} = (UN x : S. Pair x ` T x)" by auto
1.24 + moreover
1.25 + from `\<forall>x \<in> S. finite (T x)` have "ALL x:S. finite (Pair x ` T x)" by auto
1.26 + moreover
1.27 + have " ALL i:S. ALL j:S. i ~= j --> Pair i ` T i Int Pair j ` T j = {}" by auto
1.28 + moreover
1.29 + ultimately have "card {(x, y). x \<in> S \<and> y \<in> T x} = (SUM i:S. card (Pair i ` T i))"
1.30 + by (auto, subst card_UN_disjoint) auto
1.31 + also have "... = (SUM x:S. card (T x))"
1.32 + by (subst card_image) (auto intro: inj_onI)
1.33 + finally show ?thesis by auto
1.34 +qed
1.35 +
1.36 +lemma card_extensional_funcset_inj_on:
1.37 + assumes "finite S" "finite T" "card S \<le> card T"
1.38 + shows "card {f \<in> extensional_funcset S T. inj_on f S} = fact (card T) div (fact (card T - card S))"
1.39 +using assms
1.40 +proof (induct S arbitrary: T rule: finite_induct)
1.41 + case empty
1.42 + from this show ?case by (simp add: Collect_conv_if extensional_funcset_empty_domain)
1.43 +next
1.44 + case (insert x S)
1.45 + { fix x
1.46 + from `finite T` have "finite (T - {x})" by auto
1.47 + from `finite S` this have "finite (extensional_funcset S (T - {x}))"
1.48 + by (rule finite_extensional_funcset)
1.49 + moreover
1.50 + have "{f : extensional_funcset S (T - {x}). inj_on f S} \<subseteq> (extensional_funcset S (T - {x}))" by auto
1.51 + ultimately have "finite {f : extensional_funcset S (T - {x}). inj_on f S}"
1.52 + by (auto intro: finite_subset)
1.53 + } note finite_delete = this
1.54 + 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
1.55 + from extensional_funcset_extend_domain_inj_on_eq[OF `x \<notin> S`]
1.56 + have "card {f. f : extensional_funcset (insert x S) T & inj_on f (insert x S)} =
1.57 + card ((%(y, g). g(x := y)) ` {(y, g). y : T & g : extensional_funcset S (T - {y}) & inj_on g S})"
1.58 + by metis
1.59 + 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}"
1.60 + by (simp add: card_image)
1.61 + also have "card {(y, g). y \<in> T \<and> g \<in> extensional_funcset S (T - {y}) \<and> inj_on g S} =
1.62 + card {(y, g). y \<in> T \<and> g \<in> {f \<in> extensional_funcset S (T - {y}). inj_on f S}}" by auto
1.63 + 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})"
1.64 + by (subst card_product_dependent) auto
1.65 + also from hyps have "... = (card T) * ?k"
1.66 + by auto
1.67 + also have "... = card T * fact (card T - 1) div fact (card T - card (insert x S))"
1.68 + using insert unfolding div_mult1_eq[of "card T" "fact (card T - 1)"]
1.69 + by (simp add: fact_mod)
1.70 + also have "... = fact (card T) div fact (card T - card (insert x S))"
1.71 + using insert by (simp add: fact_reduce_nat[of "card T"])
1.72 + finally show ?case .
1.73 +qed
1.74 +
1.75 +lemma card_extensional_funcset_not_inj_on:
1.76 + assumes "finite S" "finite T" "card S \<le> card T"
1.77 + 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))"
1.78 +proof -
1.79 + have subset: "{f : extensional_funcset S T. inj_on f S} <= extensional_funcset S T" by auto
1.80 + from finite_subset[OF subset] assms have finite: "finite {f : extensional_funcset S T. inj_on f S}"
1.81 + by (auto intro!: finite_extensional_funcset)
1.82 + 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
1.83 + from assms this finite subset show ?thesis
1.84 + by (simp add: card_Diff_subset card_extensional_funcset card_extensional_funcset_inj_on)
1.85 +qed
1.86 +
1.87 +lemma setprod_upto_nat_unfold:
1.88 + "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)}))"
1.89 + by auto (auto simp add: gr0_conv_Suc atLeastAtMostSuc_conv)
1.90 +
1.91 +section {* Birthday paradoxon *}
1.92 +
1.93 +lemma birthday_paradoxon:
1.94 + assumes "card S = 23" "card T = 365"
1.95 + shows "2 * card {f \<in> extensional_funcset S T. \<not> inj_on f S} \<ge> card (extensional_funcset S T)"
1.96 +proof -
1.97 + from `card S = 23` `card T = 365` have "finite S" "finite T" "card S <= card T" by (auto intro: card_ge_0_finite)
1.98 + from assms show ?thesis
1.99 + using card_extensional_funcset[OF `finite S`, of T]
1.100 + card_extensional_funcset_not_inj_on[OF `finite S` `finite T` `card S <= card T`]
1.101 + by (simp add: fact_div_fact setprod_upto_nat_unfold)
1.102 +qed
1.103 +
1.104 +end