--- a/Nominal/Nominal2_Base.thy	Wed Jul 06 01:04:09 2011 +0200
+++ b/Nominal/Nominal2_Base.thy	Wed Jul 06 15:59:11 2011 +0200
@@ -1238,6 +1238,18 @@
   then show "(a \<rightleftharpoons> b) \<bullet> x = x" by (simp add: swap_fresh_fresh)
 qed
 
+lemma supports_fresh:
+  fixes x :: "'a::pt"
+  assumes a1: "S supports x"
+  and     a2: "finite S"
+  and     a3: "a \<notin> S"
+  shows "a \<sharp> x"
+unfolding fresh_def
+proof -
+  have "(supp x) \<subseteq> S" using a1 a2 by (rule supp_is_subset)
+  then show "a \<notin> (supp x)" using a3 by auto
+qed
+
 lemma supp_is_least_supports:
   fixes S :: "atom set"
   and   x :: "'a::pt"
@@ -1252,6 +1264,7 @@
   with fin a3 show "S \<subseteq> supp x" by blast
 qed
 
+
 lemma subsetCI: 
   shows "(\<And>x. x \<in> A \<Longrightarrow> x \<notin> B \<Longrightarrow> False) \<Longrightarrow> A \<subseteq> B"
   by auto
@@ -1642,6 +1655,21 @@
 unfolding eqvt_def
 by simp
 
+lemma eqvt_at_perm:
+  assumes "eqvt_at f x"
+  shows "eqvt_at f (q \<bullet> x)"
+proof -
+  { fix p::"perm"
+    have "p \<bullet> (f (q \<bullet> x)) = p \<bullet> q \<bullet> (f x)"
+      using assms by (simp add: eqvt_at_def)
+    also have "\<dots> = (p + q) \<bullet> (f x)" by simp
+    also have "\<dots> = f ((p + q) \<bullet> x)"
+      using assms by (simp add: eqvt_at_def)
+    finally have "p \<bullet> (f (q \<bullet> x)) = f (p \<bullet> q \<bullet> x)" by simp } 
+  then show "eqvt_at f (q \<bullet> x)" unfolding eqvt_at_def
+    by simp
+qed
+
 lemma supp_fun_eqvt:
   assumes a: "eqvt f"
   shows "supp f = {}"