author hoelzl Thu Jan 31 11:31:27 2013 +0100 (2013-01-31) changeset 50999 3de230ed0547 parent 50123 69b35a75caf3 child 58889 5b7a9633cfa8 permissions -rw-r--r--
introduce order topology
1 (*  Title: HOL/ex/Birthday_Paradox.thy
2     Author: Lukas Bulwahn, TU Muenchen, 2007
3 *)
5 header {* A Formulation of the Birthday Paradox *}
8 imports Main "~~/src/HOL/Fact" "~~/src/HOL/Library/FuncSet"
9 begin
11 section {* Cardinality *}
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   using card_SigmaI[OF assms, symmetric] by (auto intro!: arg_cong[where f=card] simp add: Sigma_def)
19 lemma 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))"
22 using assms
23 proof (induct S arbitrary: T rule: finite_induct)
24   case empty
25   from this show ?case by (simp add: Collect_conv_if PiE_empty_domain)
26 next
27   case (insert x S)
28   { fix x
29     from `finite T` have "finite (T - {x})" by auto
30     from `finite S` 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 `x \<notin> S`]
39   have "card {f. f : extensional_funcset (insert x S) T & inj_on f (insert x S)} =
40     card ((%(y, g). g(x := y)) ` {(y, g). y : T & g : extensional_funcset S (T - {y}) & inj_on g S})"
41     by metis
42   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}"
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 `finite T` 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_nat[of "card T"])
55   finally show ?case .
56 qed
58 lemma 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))"
61 proof -
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 setprod_constant)
68 qed
70 lemma setprod_upto_nat_unfold:
71   "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)}))"
72   by auto (auto simp add: gr0_conv_Suc atLeastAtMostSuc_conv)
74 section {* Birthday paradox *}