# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1294320484 0
# Node ID 592d17e26e09b29d1ccaad400663ecd650e23486
# Parent  75d353e8e60eff6d6b8a77ec45bd4c74494b23a0
some further lemmas for fsets

diff -r 75d353e8e60e -r 592d17e26e09 Nominal/Nominal2_Base.thy
--- a/Nominal/Nominal2_Base.thy	Thu Jan 06 11:00:16 2011 +0000
+++ b/Nominal/Nominal2_Base.thy	Thu Jan 06 13:28:04 2011 +0000
@@ -1389,6 +1389,11 @@
   unfolding supp_def
   by simp
 
+lemma fresh_empty_fset:
+  shows "a \<sharp> {||}"
+unfolding fresh_def
+by (simp)
+
 lemma supp_insert_fset [simp]:
   fixes x::"'a::fs"
   and   S::"'a fset"
@@ -1397,6 +1402,13 @@
   apply(simp add: supp_of_finite_insert)
   done
 
+lemma fresh_insert_fset:
+  fixes x::"'a::fs"
+  and   S::"'a fset"
+  shows "a \<sharp> insert_fset x S \<longleftrightarrow> a \<sharp> x \<and> a \<sharp> S"
+  unfolding fresh_def
+  by (simp)
+
 lemma fset_finite_supp:
   fixes S::"('a::fs) fset"
   shows "finite (supp S)"