author paulson Tue, 06 Jun 2006 17:07:27 +0200 changeset 19793 14fdd2a3d117 parent 19792 e8e3da6d3ff7 child 19794 100ba10eee64
new lemmas concerning finite cardinalities
 src/HOL/Finite_Set.thy file | annotate | diff | comparison | revisions
```--- a/src/HOL/Finite_Set.thy	Tue Jun 06 16:07:10 2006 +0200
+++ b/src/HOL/Finite_Set.thy	Tue Jun 06 17:07:27 2006 +0200
@@ -1595,7 +1595,7 @@
\<Longrightarrow> x \<inter> \<Union> F = {}"
by auto

-(* main cardinality theorem *)
+text{* main cardinality theorem *}
lemma card_partition [rule_format]:
"finite C ==>
finite (\<Union> C) -->
@@ -1608,6 +1608,37 @@
done

+text{*The form of a finite set of given cardinality*}
+
+lemma card_eq_SucD:
+  assumes cardeq: "card A = Suc k" and fin: "finite A"
+  shows "\<exists>b B. A = insert b B & b \<notin> B & card B = k"
+proof -
+  have "card A \<noteq> 0" using cardeq by auto
+  then obtain b where b: "b \<in> A" using fin by auto
+  show ?thesis
+  proof (intro exI conjI)
+    show "A = insert b (A-{b})" using b by blast
+    show "b \<notin> A - {b}" by blast
+    show "card (A - {b}) = k" by (simp add: fin cardeq b card_Diff_singleton)
+  qed
+qed
+
+
+lemma card_Suc_eq:
+  "finite A ==>
+   (card A = Suc k) = (\<exists>b B. A = insert b B & b \<notin> B & card B = k)"
+by (auto dest!: card_eq_SucD)
+
+lemma card_1_eq:
+  "finite A ==> (card A = Suc 0) = (\<exists>x. A = {x})"
+by (auto dest!: card_eq_SucD)
+
+lemma card_2_eq:
+  "finite A ==> (card A = Suc(Suc 0)) = (\<exists>x y. x\<noteq>y & A = {x,y})"
+by (auto dest!: card_eq_SucD, blast)
+
+
lemma setsum_constant [simp]: "(\<Sum>x \<in> A. y) = of_nat(card A) * y"
apply (cases "finite A")
apply (erule finite_induct)```