# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1271678881 -7200
# Node ID 7abd8c1d9f4b6d1810febe1257b08d546d4456ba
# Parent  b8cf69f0fe2f5c25c5ee9ab02a1e9850fe7ad70e
Some new lemmas

diff -r b8cf69f0fe2f -r 7abd8c1d9f4b Nominal/FSet.thy
--- a/Nominal/FSet.thy	Mon Apr 19 13:58:10 2010 +0200
+++ b/Nominal/FSet.thy	Mon Apr 19 14:08:01 2010 +0200
@@ -531,7 +531,7 @@
   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)
+  by (lifting memb_card_not_0)
 
 text {* funion *}
 
@@ -540,6 +540,10 @@
   and   "finsert x S |\<union>| T = finsert x (S |\<union>| T)"
   by (lifting append.simps)
 
+lemma funion_empty[simp]:
+  shows "S |\<union>| {||} = S"
+  by (lifting append_Nil2)
+
 lemma funion_sym:
   shows "S |\<union>| T = T |\<union>| S"
   by (lifting funion_sym_pre)
@@ -548,6 +552,14 @@
   shows "S |\<union>| T |\<union>| U = S |\<union>| (T |\<union>| U)"
   by (lifting append_assoc)
 
+lemma singleton_union_left:
+  "{|a|} |\<union>| S = finsert a S"
+  by simp
+
+lemma singleton_union_right:
+  "S |\<union>| {|a|} = finsert a S"
+  by (subst funion_sym) simp
+
 section {* Induction and Cases rules for finite sets *}
 
 lemma fset_strong_cases: