# HG changeset patch
# User paulson
# Date 1149606447 -7200
# Node ID 14fdd2a3d117413fd576d834ba6f855b72df8b36
# Parent  e8e3da6d3ff7e3e10f2d8af92d00b3ce6913d19e
new lemmas concerning finite cardinalities

diff -r e8e3da6d3ff7 -r 14fdd2a3d117 src/HOL/Finite_Set.thy
--- 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)