diff -r b4472ebd7fad -r 619ecb57db38 Nominal/Nominal2_Base.thy
--- a/Nominal/Nominal2_Base.thy	Thu Jan 13 12:12:47 2011 +0000
+++ b/Nominal/Nominal2_Base.thy	Fri Jan 14 14:22:25 2011 +0000
@@ -1668,6 +1668,21 @@
 by (rule supp_perm_eq)
    (simp add: fresh_star_supp_conv a)
 
+lemma supp_perm_perm_eq:
+  assumes a: "\<forall>a \<in> supp x. p \<bullet> a = q \<bullet> a"
+  shows "p \<bullet> x = q \<bullet> x"
+proof -
+  from a have "\<forall>a \<in> supp x. (-q + p) \<bullet> a = a" by simp
+  then have "\<forall>a \<in> supp x. a \<notin> supp (-q + p)" 
+    unfolding supp_perm by simp
+  then have "supp x \<sharp>* (-q + p)"
+    unfolding fresh_star_def fresh_def by simp
+  then have "(-q + p) \<bullet> x = x" by (simp only: supp_perm_eq)
+  then show "p \<bullet> x = q \<bullet> x"
+    by (metis permute_minus_cancel permute_plus)
+qed
+    
+
 
 section {* Avoiding of atom sets *}
 
@@ -1793,10 +1808,9 @@
 section {* Renaming permutations *}
 
 lemma set_renaming_perm:
-  assumes a: "p \<bullet> bs \<inter> bs = {}" 
-  and     b: "finite bs"
+  assumes b: "finite bs"
   shows "\<exists>q. q \<bullet> bs = p \<bullet> bs \<and> supp q \<subseteq> bs \<union> (p \<bullet> bs)"
-using b a
+using b
 proof (induct)
   case empty
   have "0 \<bullet> {} = p \<bullet> {} \<and> supp (0::perm) \<subseteq> {} \<union> p \<bullet> {}"
@@ -1827,8 +1841,14 @@
     }
     moreover 
     { have "{q \<bullet> a, p \<bullet> a} \<subseteq> insert a bs \<union> p \<bullet> insert a bs"
-	using ** `a \<notin> bs` `p \<bullet> insert a bs \<inter> insert a bs = {}`
-	by (auto simp add: supp_perm insert_eqvt)
+	using ** 
+	apply (auto simp add: supp_perm insert_eqvt)
+	apply (subgoal_tac "q \<bullet> a \<in> bs \<union> p \<bullet> bs")
+	apply(auto)[1]
+	apply(subgoal_tac "q \<bullet> a \<in> {a. q \<bullet> a \<noteq> a}")
+	apply(blast)
+	apply(simp)
+	done
       then have "supp (q \<bullet> a \<rightleftharpoons> p \<bullet> a) \<subseteq> insert a bs \<union> p \<bullet> insert a bs" by (simp add: supp_swap)
       moreover
       have "supp q \<subseteq> insert a bs \<union> p \<bullet> insert a bs" 
@@ -1844,12 +1864,9 @@
     by blast
 qed
 
-
 lemma list_renaming_perm:
   fixes bs::"atom list"
-  assumes a: "(p \<bullet> (set bs)) \<inter> (set bs) = {}"
   shows "\<exists>q. q \<bullet> bs = p \<bullet> bs \<and> supp q \<subseteq> (set bs) \<union> (p \<bullet> (set bs))"
-using a
 proof (induct bs)
   case Nil
   have "0 \<bullet> [] = p \<bullet> [] \<and> supp (0::perm) \<subseteq> set [] \<union> p \<bullet> set []"
@@ -1882,8 +1899,14 @@
     }
     moreover 
     { have "{q \<bullet> a, p \<bullet> a} \<subseteq> set (a # bs) \<union> p \<bullet> (set (a # bs))"
-	using ** `a \<notin> set bs` `p \<bullet> (set (a # bs)) \<inter> set (a # bs) = {}`
-	by (auto simp add: supp_perm insert_eqvt)
+	using **
+	apply (auto simp add: supp_perm insert_eqvt)
+	apply (subgoal_tac "q \<bullet> a \<in> set bs \<union> p \<bullet> set bs")
+	apply(auto)[1]
+	apply(subgoal_tac "q \<bullet> a \<in> {a. q \<bullet> a \<noteq> a}")
+	apply(blast)
+	apply(simp)
+	done
       then have "supp (q \<bullet> a \<rightleftharpoons> p \<bullet> a) \<subseteq> set (a # bs) \<union> p \<bullet> set (a # bs)" by (simp add: supp_swap)
       moreover
       have "supp q \<subseteq> set (a # bs) \<union> p \<bullet> (set (a # bs))"