1.1 --- a/src/HOL/Finite_Set.thy Fri Jun 18 20:22:06 2010 +0200
1.2 +++ b/src/HOL/Finite_Set.thy Fri Jun 18 22:40:58 2010 +0200
1.3 @@ -2180,6 +2180,55 @@
1.4 by (auto intro: le_antisym card_inj_on_le)
1.5
1.6
1.7 +subsubsection {* Pigeonhole Principles *}
1.8 +
1.9 +lemma pigeonhole: "finite(A) \<Longrightarrow> card A > card(f ` A) \<Longrightarrow> ~ inj_on f A "
1.10 +by (auto dest: card_image less_irrefl_nat)
1.11 +
1.12 +lemma pigeonhole_infinite:
1.13 +assumes "~ finite A" and "finite(f`A)"
1.14 +shows "EX a0:A. ~finite{a:A. f a = f a0}"
1.15 +proof -
1.16 + have "finite(f`A) \<Longrightarrow> ~ finite A \<Longrightarrow> EX a0:A. ~finite{a:A. f a = f a0}"
1.17 + proof(induct "f`A" arbitrary: A rule: finite_induct)
1.18 + case empty thus ?case by simp
1.19 + next
1.20 + case (insert b F)
1.21 + show ?case
1.22 + proof cases
1.23 + assume "finite{a:A. f a = b}"
1.24 + hence "~ finite(A - {a:A. f a = b})" using `\<not> finite A` by simp
1.25 + also have "A - {a:A. f a = b} = {a:A. f a \<noteq> b}" by blast
1.26 + finally have "~ finite({a:A. f a \<noteq> b})" .
1.27 + from insert(3)[OF _ this]
1.28 + show ?thesis using insert(2,4) by simp (blast intro: rev_finite_subset)
1.29 + next
1.30 + assume 1: "~finite{a:A. f a = b}"
1.31 + hence "{a \<in> A. f a = b} \<noteq> {}" by force
1.32 + thus ?thesis using 1 by blast
1.33 + qed
1.34 + qed
1.35 + from this[OF assms(2,1)] show ?thesis .
1.36 +qed
1.37 +
1.38 +lemma pigeonhole_infinite_rel:
1.39 +assumes "~finite A" and "finite B" and "ALL a:A. EX b:B. R a b"
1.40 +shows "EX b:B. ~finite{a:A. R a b}"
1.41 +proof -
1.42 + let ?F = "%a. {b:B. R a b}"
1.43 + from finite_Pow_iff[THEN iffD2, OF `finite B`]
1.44 + have "finite(?F ` A)" by(blast intro: rev_finite_subset)
1.45 + from pigeonhole_infinite[where f = ?F, OF assms(1) this]
1.46 + obtain a0 where "a0\<in>A" and 1: "\<not> finite {a\<in>A. ?F a = ?F a0}" ..
1.47 + obtain b0 where "b0 : B" and "R a0 b0" using `a0:A` assms(3) by blast
1.48 + { assume "finite{a:A. R a b0}"
1.49 + then have "finite {a\<in>A. ?F a = ?F a0}"
1.50 + using `b0 : B` `R a0 b0` by(blast intro: rev_finite_subset)
1.51 + }
1.52 + with 1 `b0 : B` show ?thesis by blast
1.53 +qed
1.54 +
1.55 +
1.56 subsubsection {* Cardinality of sums *}
1.57
1.58 lemma card_Plus:
1.59 @@ -2210,7 +2259,7 @@
1.60 apply (blast elim!: equalityE)
1.61 done
1.62
1.63 -text {* Relates to equivalence classes. Based on a theorem of F. Kammüller. *}
1.64 +text {* Relates to equivalence classes. Based on a theorem of F. Kammüller. *}
1.65
1.66 lemma dvd_partition:
1.67 "finite (Union C) ==>