1.1 --- a/src/HOL/Finite_Set.thy	Fri Jun 18 21:22:05 2010 +0200
     1.2 +++ b/src/HOL/Finite_Set.thy	Fri Jun 18 22:41:16 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) ==>