src/HOL/Finite_Set.thy
 changeset 14889 d7711d6b9014 parent 14748 001323d6d75b child 14944 efbaecbdc05c
```--- a/src/HOL/Finite_Set.thy	Tue Jun 08 19:25:27 2004 +0200
+++ b/src/HOL/Finite_Set.thy	Wed Jun 09 11:18:51 2004 +0200
@@ -496,6 +496,23 @@
lemma card_psubset: "finite B ==> A \<subseteq> B ==> card A < card B ==> A < B"
by (erule psubsetI, blast)

+lemma insert_partition:
+     "[| x \<notin> F; \<forall>c1\<in>insert x F. \<forall>c2 \<in> insert x F. c1 \<noteq> c2 --> c1 \<inter> c2 = {}|]
+      ==> x \<inter> \<Union> F = {}"
+by auto
+
+(* main cardinality theorem *)
+lemma card_partition [rule_format]:
+     "finite C ==>
+        finite (\<Union> C) -->
+        (\<forall>c\<in>C. card c = k) -->
+        (\<forall>c1 \<in> C. \<forall>c2 \<in> C. c1 \<noteq> c2 --> c1 \<inter> c2 = {}) -->
+        k * card(C) = card (\<Union> C)"
+apply (erule finite_induct, simp)
+apply (simp add: card_insert_disjoint card_Un_disjoint insert_partition
+       finite_subset [of _ "\<Union> (insert x F)"])
+done
+

subsubsection {* Cardinality of image *}
```