author wenzelm Sat Nov 04 19:17:19 2017 +0100 (19 months ago) changeset 67006 b1278ed3cd46 parent 66453 cc19f7ca2ed6 child 67613 ce654b0e6d69 permissions -rw-r--r--
prefer main entry points of HOL;
```     1 (*  Title: HOL/ex/Birthday_Paradox.thy
```
```     2     Author: Lukas Bulwahn, TU Muenchen, 2007
```
```     3 *)
```
```     4
```
```     5 section \<open>A Formulation of the Birthday Paradox\<close>
```
```     6
```
```     7 theory Birthday_Paradox
```
```     8 imports Main "HOL-Library.FuncSet"
```
```     9 begin
```
```    10
```
```    11 section \<open>Cardinality\<close>
```
```    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   using card_SigmaI[OF assms, symmetric] by (auto intro!: arg_cong[where f=card] simp add: Sigma_def)
```
```    18
```
```    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 \<open>finite T\<close> have "finite (T - {x})" by auto
```
```    30     from \<open>finite S\<close> 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 \<open>x \<notin> S\<close>]
```
```    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 \<open>x \<notin> S\<close>, 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 \<open>finite T\<close> 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[of "card T"])
```
```    55   finally show ?case .
```
```    56 qed
```
```    57
```
```    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 prod_constant)
```
```    68 qed
```
```    69
```
```    70 lemma prod_upto_nat_unfold:
```
```    71   "prod f {m..(n::nat)} = (if n < m then 1 else (if n = 0 then f 0 else f n * prod f {m..(n - 1)}))"
```
```    72   by auto (auto simp add: gr0_conv_Suc atLeastAtMostSuc_conv)
```
```    73
```
```    74 section \<open>Birthday paradox\<close>
```
```    75
```
```    76 lemma birthday_paradox:
```
```    77   assumes "card S = 23" "card T = 365"
```
```    78   shows "2 * card {f \<in> extensional_funcset S T. \<not> inj_on f S} \<ge> card (extensional_funcset S T)"
```
```    79 proof -
```
```    80   from \<open>card S = 23\<close> \<open>card T = 365\<close> have "finite S" "finite T" "card S <= card T" by (auto intro: card_ge_0_finite)
```
```    81   from assms show ?thesis
```
```    82     using card_PiE[OF \<open>finite S\<close>, of "\<lambda>i. T"] \<open>finite S\<close>
```
```    83       card_extensional_funcset_not_inj_on[OF \<open>finite S\<close> \<open>finite T\<close> \<open>card S <= card T\<close>]
```
```    84     by (simp add: fact_div_fact prod_upto_nat_unfold prod_constant)
```
```    85 qed
```
```    86
```
```    87 end
```