1.1 --- a/src/HOL/IsaMakefile Tue Jun 07 11:10:42 2011 +0200
1.2 +++ b/src/HOL/IsaMakefile Tue Jun 07 11:10:57 2011 +0200
1.3 @@ -1047,7 +1047,7 @@
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/Birthday_Paradoxon.thy \
1.8 + ex/BinEx.thy ex/Binary.thy ex/Birthday_Paradox.thy \
1.9 ex/CASC_Setup.thy ex/CTL.thy ex/Case_Product.thy \
1.10 ex/Chinese.thy ex/Classical.thy ex/CodegenSML_Test.thy \
1.11 ex/Coercion_Examples.thy ex/Coherent.thy ex/Dedekind_Real.thy \
2.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
2.2 +++ b/src/HOL/ex/Birthday_Paradox.thy Tue Jun 07 11:10:57 2011 +0200
2.3 @@ -0,0 +1,101 @@
2.4 +(* Title: HOL/ex/Birthday_Paradox.thy
2.5 + Author: Lukas Bulwahn, TU Muenchen, 2007
2.6 +*)
2.7 +
2.8 +header {* A Formulation of the Birthday Paradox *}
2.9 +
2.10 +theory Birthday_Paradox
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 paradox *}
2.92 +
2.93 +lemma birthday_paradox:
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/Birthday_Paradoxon.thy Tue Jun 07 11:10:42 2011 +0200
3.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
3.3 @@ -1,101 +0,0 @@
3.4 -(* Title: HOL/ex/Birthday_Paradoxon.thy
3.5 - Author: Lukas Bulwahn, TU Muenchen, 2007
3.6 -*)
3.7 -
3.8 -header {* A Formulation of the Birthday Paradoxon *}
3.9 -
3.10 -theory Birthday_Paradoxon
3.11 -imports Main "~~/src/HOL/Fact" "~~/src/HOL/Library/FuncSet"
3.12 -begin
3.13 -
3.14 -section {* Cardinality *}
3.15 -
3.16 -lemma card_product_dependent:
3.17 - assumes "finite S"
3.18 - assumes "\<forall>x \<in> S. finite (T x)"
3.19 - shows "card {(x, y). x \<in> S \<and> y \<in> T x} = (\<Sum>x \<in> S. card (T x))"
3.20 -proof -
3.21 - note `finite S`
3.22 - moreover
3.23 - have "{(x, y). x \<in> S \<and> y \<in> T x} = (UN x : S. Pair x ` T x)" by auto
3.24 - moreover
3.25 - from `\<forall>x \<in> S. finite (T x)` have "ALL x:S. finite (Pair x ` T x)" by auto
3.26 - moreover
3.27 - have " ALL i:S. ALL j:S. i ~= j --> Pair i ` T i Int Pair j ` T j = {}" by auto
3.28 - moreover
3.29 - ultimately have "card {(x, y). x \<in> S \<and> y \<in> T x} = (SUM i:S. card (Pair i ` T i))"
3.30 - by (auto, subst card_UN_disjoint) auto
3.31 - also have "... = (SUM x:S. card (T x))"
3.32 - by (subst card_image) (auto intro: inj_onI)
3.33 - finally show ?thesis by auto
3.34 -qed
3.35 -
3.36 -lemma card_extensional_funcset_inj_on:
3.37 - assumes "finite S" "finite T" "card S \<le> card T"
3.38 - shows "card {f \<in> extensional_funcset S T. inj_on f S} = fact (card T) div (fact (card T - card S))"
3.39 -using assms
3.40 -proof (induct S arbitrary: T rule: finite_induct)
3.41 - case empty
3.42 - from this show ?case by (simp add: Collect_conv_if extensional_funcset_empty_domain)
3.43 -next
3.44 - case (insert x S)
3.45 - { fix x
3.46 - from `finite T` have "finite (T - {x})" by auto
3.47 - from `finite S` this have "finite (extensional_funcset S (T - {x}))"
3.48 - by (rule finite_extensional_funcset)
3.49 - moreover
3.50 - have "{f : extensional_funcset S (T - {x}). inj_on f S} \<subseteq> (extensional_funcset S (T - {x}))" by auto
3.51 - ultimately have "finite {f : extensional_funcset S (T - {x}). inj_on f S}"
3.52 - by (auto intro: finite_subset)
3.53 - } note finite_delete = this
3.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
3.55 - from extensional_funcset_extend_domain_inj_on_eq[OF `x \<notin> S`]
3.56 - have "card {f. f : extensional_funcset (insert x S) T & inj_on f (insert x S)} =
3.57 - card ((%(y, g). g(x := y)) ` {(y, g). y : T & g : extensional_funcset S (T - {y}) & inj_on g S})"
3.58 - by metis
3.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}"
3.60 - by (simp add: card_image)
3.61 - also have "card {(y, g). y \<in> T \<and> g \<in> extensional_funcset S (T - {y}) \<and> inj_on g S} =
3.62 - card {(y, g). y \<in> T \<and> g \<in> {f \<in> extensional_funcset S (T - {y}). inj_on f S}}" by auto
3.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})"
3.64 - by (subst card_product_dependent) auto
3.65 - also from hyps have "... = (card T) * ?k"
3.66 - by auto
3.67 - also have "... = card T * fact (card T - 1) div fact (card T - card (insert x S))"
3.68 - using insert unfolding div_mult1_eq[of "card T" "fact (card T - 1)"]
3.69 - by (simp add: fact_mod)
3.70 - also have "... = fact (card T) div fact (card T - card (insert x S))"
3.71 - using insert by (simp add: fact_reduce_nat[of "card T"])
3.72 - finally show ?case .
3.73 -qed
3.74 -
3.75 -lemma card_extensional_funcset_not_inj_on:
3.76 - assumes "finite S" "finite T" "card S \<le> card T"
3.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))"
3.78 -proof -
3.79 - have subset: "{f : extensional_funcset S T. inj_on f S} <= extensional_funcset S T" by auto
3.80 - from finite_subset[OF subset] assms have finite: "finite {f : extensional_funcset S T. inj_on f S}"
3.81 - by (auto intro!: finite_extensional_funcset)
3.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
3.83 - from assms this finite subset show ?thesis
3.84 - by (simp add: card_Diff_subset card_extensional_funcset card_extensional_funcset_inj_on)
3.85 -qed
3.86 -
3.87 -lemma setprod_upto_nat_unfold:
3.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)}))"
3.89 - by auto (auto simp add: gr0_conv_Suc atLeastAtMostSuc_conv)
3.90 -
3.91 -section {* Birthday paradoxon *}
3.92 -
3.93 -lemma birthday_paradoxon:
3.94 - assumes "card S = 23" "card T = 365"
3.95 - shows "2 * card {f \<in> extensional_funcset S T. \<not> inj_on f S} \<ge> card (extensional_funcset S T)"
3.96 -proof -
3.97 - from `card S = 23` `card T = 365` have "finite S" "finite T" "card S <= card T" by (auto intro: card_ge_0_finite)
3.98 - from assms show ?thesis
3.99 - using card_extensional_funcset[OF `finite S`, of T]
3.100 - card_extensional_funcset_not_inj_on[OF `finite S` `finite T` `card S <= card T`]
3.101 - by (simp add: fact_div_fact setprod_upto_nat_unfold)
3.102 -qed
3.103 -
3.104 -end
4.1 --- a/src/HOL/ex/ROOT.ML Tue Jun 07 11:10:42 2011 +0200
4.2 +++ b/src/HOL/ex/ROOT.ML Tue Jun 07 11:10:57 2011 +0200
4.3 @@ -73,7 +73,7 @@
4.4 "Gauge_Integration",
4.5 "Dedekind_Real",
4.6 "Quicksort",
4.7 - "Birthday_Paradoxon",
4.8 + "Birthday_Paradox",
4.9 "List_to_Set_Comprehension_Examples",
4.10 "Set_Algebras"
4.11 ];