--- a/Nominal/Nominal2_Base.thy	Wed Jan 19 18:07:29 2011 +0100
+++ b/Nominal/Nominal2_Base.thy	Wed Jan 19 18:56:28 2011 +0100
@@ -844,14 +844,25 @@
   by (simp add: fresh_permute_iff)
 
 lemma supp_eqvt:
-  fixes  p  :: "perm"
-  and    x   :: "'a::pt"
   shows "p \<bullet> (supp x) = supp (p \<bullet> x)"
   unfolding supp_conv_fresh
   unfolding Collect_def
   unfolding permute_fun_def
   by (simp add: Not_eqvt fresh_eqvt)
 
+lemma fresh_permute_left:
+  shows "a \<sharp> p \<bullet> x \<longleftrightarrow> - p \<bullet> a \<sharp> x"
+proof
+  assume "a \<sharp> p \<bullet> x"
+  then have "- p \<bullet> a \<sharp> - p \<bullet> p \<bullet> x" by (simp only: fresh_permute_iff)
+  then show "- p \<bullet> a \<sharp> x" by simp
+next
+  assume "- p \<bullet> a \<sharp> x"
+  then have "p \<bullet> - p \<bullet> a \<sharp> p \<bullet> x" by (simp only: fresh_permute_iff)
+  then show "a \<sharp> p \<bullet> x" by simp
+qed
+
+
 subsection {* supports *}
 
 definition
@@ -2236,11 +2247,15 @@
   apply(simp)
   done
 
+lemma fresh_at_base_permute_iff[simp]:
+  fixes a::"'a::at_base"
+  shows "atom (p \<bullet> a) \<sharp> p \<bullet> x \<longleftrightarrow> atom a \<sharp> x"
+  unfolding atom_eqvt[symmetric]
+  by (simp add: fresh_permute_iff)
+
 
 section {* Infrastructure for concrete atom types *}
 
-section {* A swapping operation for concrete atoms *}
-  
 definition
   flip :: "'a::at_base \<Rightarrow> 'a \<Rightarrow> perm" ("'(_ \<leftrightarrow> _')")
 where
@@ -2305,6 +2320,8 @@
 using assms
 by (simp add: flip_def swap_fresh_fresh)
 
+
+
 subsection {* Syntax for coercing at-elements to the atom-type *}
 
 syntax
@@ -2502,7 +2519,7 @@
   apply (subst fresh_fun_apply', assumption+)
   apply (drule fresh_permute_iff [where p=p, THEN iffD2])
   apply (drule fresh_permute_iff [where p=p, THEN iffD2])
-  apply (simp add: atom_eqvt permute_fun_app_eq [where f=h])
+  apply (simp only: atom_eqvt permute_fun_app_eq [where f=h])
   apply (erule (1) fresh_fun_apply' [symmetric])
   done