diff -r 869d1183e082 -r d360a26fa790 Nominal/FSet.thy
--- a/Nominal/FSet.thy	Mon Apr 19 09:25:31 2010 +0200
+++ b/Nominal/FSet.thy	Mon Apr 19 09:27:53 2010 +0200
@@ -80,6 +80,14 @@
   shows "\<not> memb x []"
   by (simp add: memb_def)
 
+lemma no_memb_nil:
+  "(\<forall>x. \<not> memb x xs) = (xs = [])"
+  by (simp add: memb_def)
+
+lemma none_memb_nil:
+  "(\<forall>x. \<not> memb x xs) = (xs \<approx> [])"
+  by (simp add: memb_def)
+
 lemma memb_cons_iff:
   shows "memb x (y # xs) = (x = y \<or> memb x xs)"
   by (induct xs) (auto simp add: memb_def)
@@ -162,6 +170,21 @@
   shows "fcard_raw ([x \<leftarrow> xs. x \<noteq> y]) = (if memb y xs then fcard_raw xs - 1 else fcard_raw xs)"
   by (induct xs) (auto dest: fcard_raw_gt_0 simp add: memb_def)
 
+lemma fcard_raw_suc_memb:
+  assumes a: "fcard_raw A = Suc n"
+  shows "\<exists>a. memb a A"
+  using a
+  apply (induct A)
+  apply simp
+  apply (rule_tac x="a" in exI)
+  apply (simp add: memb_def)
+  done
+
+lemma mem_card_not_0:
+  assumes a: "memb a A"
+  shows "\<not>(fcard_raw A = 0)"
+  by (metis a fcard_raw_0 none_memb_nil)
+
 lemma fcard_raw_rsp_aux:
   assumes a: "xs \<approx> ys"
   shows "fcard_raw xs = fcard_raw ys"
@@ -208,10 +231,6 @@
   "x # x # xs \<approx> x # xs"
   by auto
 
-lemma none_memb_nil:
-  "(\<forall>x. \<not> memb x xs) = (xs \<approx> [])"
-  by (simp add: memb_def)
-
 lemma fset_raw_strong_cases:
   "(xs = []) \<or> (\<exists>x ys. ((\<not> memb x ys) \<and> (xs \<approx> x # ys)))"
   apply (induct xs)
@@ -492,6 +511,12 @@
   "fcard (fdelete S y) = (if y |\<in>| S then fcard S - 1 else fcard S)"
   by (lifting fcard_raw_delete)
 
+lemma fcard_suc_memb: "fcard A = Suc n \<Longrightarrow> \<exists>a. a |\<in>| A"
+  by (lifting fcard_raw_suc_memb)
+
+lemma fin_fcard_not_0: "a |\<in>| A \<Longrightarrow> fcard A \<noteq> 0"
+  by (lifting mem_card_not_0)
+
 text {* funion *}
 
 lemma funion_simps[simp]: