--- a/Nominal/Nominal2_Base.thy	Sat Nov 27 23:00:16 2010 +0000
+++ b/Nominal/Nominal2_Base.thy	Sun Nov 28 16:37:34 2010 +0000
@@ -414,7 +414,6 @@
   shows "p \<bullet> (f x) = (p \<bullet> f) (p \<bullet> x)"
   unfolding permute_fun_def by simp
 
-
 subsection {* Permutations for booleans *}
 
 instantiation bool :: pt
@@ -483,6 +482,18 @@
   unfolding permute_fun_def permute_bool_def
   unfolding vimage_def Collect_def mem_def ..
 
+lemma permute_finite [simp]:
+  shows "finite (p \<bullet> X) = finite X"
+apply(simp add: permute_set_eq_image)
+apply(rule iffI)
+apply(drule finite_imageD)
+using inj_permute[where p="p"]
+apply(simp add: inj_on_def)
+apply(assumption)
+apply(rule finite_imageI)
+apply(assumption)
+done
+
 lemma swap_set_not_in:
   assumes a: "a \<notin> S" "b \<notin> S"
   shows "(a \<rightleftharpoons> b) \<bullet> S = S"
@@ -1162,6 +1173,12 @@
 apply (simp_all add: supp_Nil supp_Cons finite_supp)
 done
 
+lemma supp_of_atom_list:
+  fixes as::"atom list"
+  shows "supp as = set as"
+by (induct as)
+   (simp_all add: supp_Nil supp_Cons supp_atom)
+
 
 section {* Support and Freshness for Applications *}
 
@@ -1288,6 +1305,13 @@
   using fin
   by (simp add: supp_of_finite_sets)
 
+lemma fresh_finite_insert:
+  fixes S::"('a::fs) set"
+  assumes fin:  "finite S"
+  shows "a \<sharp> (insert x S) \<longleftrightarrow> a \<sharp> x \<and> a \<sharp> S"
+  using fin unfolding fresh_def
+  by (simp add: supp_of_finite_insert)
+
 
 subsection {* Type @{typ "'a fset"} is finitely supported *}