1.1 --- a/src/HOL/IsaMakefile	Mon Nov 22 10:41:51 2010 +0100
     1.2 +++ b/src/HOL/IsaMakefile	Mon Nov 22 10:41:52 2010 +0100
     1.3 @@ -1016,7 +1016,8 @@
     1.4  $(LOG)/HOL-ex.gz: $(OUT)/HOL Decision_Procs/Commutative_Ring.thy	\
     1.5    Number_Theory/Primes.thy ex/Abstract_NAT.thy ex/Antiquote.thy		\
     1.6    ex/Arith_Examples.thy ex/Arithmetic_Series_Complex.thy ex/BT.thy	\
     1.7 -  ex/BinEx.thy ex/Binary.thy ex/CTL.thy ex/Chinese.thy			\
     1.8 +  ex/BinEx.thy ex/Binary.thy ex/Birthday_Paradoxon.thy ex/CTL.thy   \
     1.9 +  ex/Chinese.thy \
    1.10    ex/Classical.thy ex/CodegenSML_Test.thy ex/Coercion_Examples.thy	\
    1.11    ex/Coherent.thy ex/Dedekind_Real.thy ex/Efficient_Nat_examples.thy	\
    1.12    ex/Eval_Examples.thy ex/Fundefs.thy ex/Gauge_Integration.thy		\

     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/HOL/ex/Birthday_Paradoxon.thy	Mon Nov 22 10:41:52 2010 +0100
     2.3 @@ -0,0 +1,101 @@
     2.4 +(*  Title: HOL/ex/Birthday_Paradoxon.thy
     2.5 +    Author: Lukas Bulwahn, TU Muenchen, 2007
     2.6 +*)
     2.7 +
     2.8 +header {* A Formulation of the Birthday Paradoxon *}
     2.9 +
    2.10 +theory Birthday_Paradoxon
    2.11 +imports Main "~~/src/HOL/Fact" "~~/src/HOL/Library/FuncSet"
    2.12 +begin
    2.13 +
    2.14 +section {* Cardinality *}
    2.15 +
    2.16 +lemma card_product_dependent:
    2.17 +  assumes "finite S"
    2.18 +  assumes "\<forall>x \<in> S. finite (T x)" 
    2.19 +  shows "card {(x, y). x \<in> S \<and> y \<in> T x} = (\<Sum>x \<in> S. card (T x))"
    2.20 +proof -
    2.21 +  note `finite S`
    2.22 +  moreover
    2.23 +  have "{(x, y). x \<in> S \<and> y \<in> T x} = (UN x : S. Pair x ` T x)" by auto
    2.24 +  moreover
    2.25 +  from `\<forall>x \<in> S. finite (T x)` have "ALL x:S. finite (Pair x ` T x)" by auto
    2.26 +  moreover
    2.27 +  have " ALL i:S. ALL j:S. i ~= j --> Pair i ` T i Int Pair j ` T j = {}" by auto
    2.28 +  moreover  
    2.29 +  ultimately have "card {(x, y). x \<in> S \<and> y \<in> T x} = (SUM i:S. card (Pair i ` T i))"
    2.30 +    by (auto, subst card_UN_disjoint) auto
    2.31 +  also have "... = (SUM x:S. card (T x))"
    2.32 +    by (subst card_image) (auto intro: inj_onI)
    2.33 +  finally show ?thesis by auto
    2.34 +qed
    2.35 +
    2.36 +lemma card_extensional_funcset_inj_on:
    2.37 +  assumes "finite S" "finite T" "card S \<le> card T"
    2.38 +  shows "card {f \<in> extensional_funcset S T. inj_on f S} = fact (card T) div (fact (card T - card S))"
    2.39 +using assms
    2.40 +proof (induct S arbitrary: T rule: finite_induct)
    2.41 +  case empty
    2.42 +  from this show ?case by (simp add: Collect_conv_if extensional_funcset_empty_domain)
    2.43 +next
    2.44 +  case (insert x S)
    2.45 +  { fix x
    2.46 +    from `finite T` have "finite (T - {x})" by auto
    2.47 +    from `finite S` this have "finite (extensional_funcset S (T - {x}))"
    2.48 +      by (rule finite_extensional_funcset)
    2.49 +    moreover
    2.50 +    have "{f : extensional_funcset S (T - {x}). inj_on f S} \<subseteq> (extensional_funcset S (T - {x}))" by auto    
    2.51 +    ultimately have "finite {f : extensional_funcset S (T - {x}). inj_on f S}"
    2.52 +      by (auto intro: finite_subset)
    2.53 +  } note finite_delete = this
    2.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
    2.55 +  from extensional_funcset_extend_domain_inj_on_eq[OF `x \<notin> S`]
    2.56 +  have "card {f. f : extensional_funcset (insert x S) T & inj_on f (insert x S)} =
    2.57 +    card ((%(y, g). g(x := y)) ` {(y, g). y : T & g : extensional_funcset S (T - {y}) & inj_on g S})"
    2.58 +    by metis
    2.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}"
    2.60 +    by (simp add: card_image)
    2.61 +  also have "card {(y, g). y \<in> T \<and> g \<in> extensional_funcset S (T - {y}) \<and> inj_on g S} =
    2.62 +    card {(y, g). y \<in> T \<and> g \<in> {f \<in> extensional_funcset S (T - {y}). inj_on f S}}" by auto
    2.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})"
    2.64 +    by (subst card_product_dependent) auto
    2.65 +  also from hyps have "... = (card T) * ?k"
    2.66 +    by auto
    2.67 +  also have "... = card T * fact (card T - 1) div fact (card T - card (insert x S))"
    2.68 +    using insert unfolding div_mult1_eq[of "card T" "fact (card T - 1)"]
    2.69 +    by (simp add: fact_mod)
    2.70 +  also have "... = fact (card T) div fact (card T - card (insert x S))"
    2.71 +    using insert by (simp add: fact_reduce_nat[of "card T"])
    2.72 +  finally show ?case .
    2.73 +qed
    2.74 +
    2.75 +lemma card_extensional_funcset_not_inj_on:
    2.76 +  assumes "finite S" "finite T" "card S \<le> card T"
    2.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))"
    2.78 +proof -
    2.79 +  have subset: "{f : extensional_funcset S T. inj_on f S} <= extensional_funcset S T" by auto
    2.80 +  from finite_subset[OF subset] assms have finite: "finite {f : extensional_funcset S T. inj_on f S}"
    2.81 +    by (auto intro!: finite_extensional_funcset)
    2.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 
    2.83 +  from assms this finite subset show ?thesis
    2.84 +    by (simp add: card_Diff_subset card_extensional_funcset card_extensional_funcset_inj_on)
    2.85 +qed
    2.86 +
    2.87 +lemma setprod_upto_nat_unfold:
    2.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)}))"
    2.89 +  by auto (auto simp add: gr0_conv_Suc atLeastAtMostSuc_conv)
    2.90 +
    2.91 +section {* Birthday paradoxon *}
    2.92 +
    2.93 +lemma birthday_paradoxon:
    2.94 +  assumes "card S = 23" "card T = 365"
    2.95 +  shows "2 * card {f \<in> extensional_funcset S T. \<not> inj_on f S} \<ge> card (extensional_funcset S T)"
    2.96 +proof -
    2.97 +  from `card S = 23` `card T = 365` have "finite S" "finite T" "card S <= card T" by (auto intro: card_ge_0_finite)
    2.98 +  from assms show ?thesis
    2.99 +    using card_extensional_funcset[OF `finite S`, of T]
   2.100 +      card_extensional_funcset_not_inj_on[OF `finite S` `finite T` `card S <= card T`]
   2.101 +    by (simp add: fact_div_fact setprod_upto_nat_unfold)
   2.102 +qed
   2.103 +
   2.104 +end

     3.1 --- a/src/HOL/ex/ROOT.ML	Mon Nov 22 10:41:51 2010 +0100
     3.2 +++ b/src/HOL/ex/ROOT.ML	Mon Nov 22 10:41:52 2010 +0100
     3.3 @@ -67,7 +67,8 @@
     3.4    "Summation",
     3.5    "Gauge_Integration",
     3.6    "Dedekind_Real",
     3.7 -  "Quicksort"
     3.8 +  "Quicksort",
     3.9 +  "Birthday_Paradoxon"
    3.10  ];
    3.11  
    3.12  HTML.with_charset "utf-8" (no_document use_thys)