diff -r e3f8673085b1 -r 92c001d93225 Nominal/Nominal2_Base.thy
--- a/Nominal/Nominal2_Base.thy	Mon Jan 17 17:20:21 2011 +0100
+++ b/Nominal/Nominal2_Base.thy	Tue Jan 18 06:55:18 2011 +0100
@@ -1785,7 +1785,22 @@
     by (metis permute_minus_cancel permute_plus)
 qed
     
-
+lemma atom_set_perm_eq:
+  assumes a: "as \<sharp>* p"
+  shows "p \<bullet> as = as"
+proof -
+  from a have "supp p \<subseteq> {a. a \<notin> as}"
+    unfolding supp_perm fresh_star_def fresh_def by auto
+  then show "p \<bullet> as = as"
+  proof (induct p rule: perm_struct_induct)
+    case zero
+    show "0 \<bullet> as = as" by simp
+  next
+    case (swap p a b)
+    then have "a \<notin> as" "b \<notin> as" "p \<bullet> as = as" by simp_all
+    then show "((a \<rightleftharpoons> b) + p) \<bullet> as = as" by (simp add: swap_set_not_in)
+  qed
+qed
 
 section {* Avoiding of atom sets *}
 
@@ -1910,38 +1925,34 @@
 
 section {* Renaming permutations *}
 
+
 lemma set_renaming_perm:
   assumes b: "finite bs"
-  shows "\<exists>q. q \<bullet> bs = p \<bullet> bs \<and> supp q \<subseteq> bs \<union> (p \<bullet> bs)"
+  shows "\<exists>q. (\<forall>b \<in> bs. q \<bullet> b = p \<bullet> b) \<and> supp q \<subseteq> bs \<union> (p \<bullet> bs)"
 using b
 proof (induct)
   case empty
-  have "0 \<bullet> {} = p \<bullet> {} \<and> supp (0::perm) \<subseteq> {} \<union> p \<bullet> {}"
+  have "(\<forall>b \<in> {}. 0 \<bullet> b = p \<bullet> b) \<and> supp (0::perm) \<subseteq> {} \<union> p \<bullet> {}"
     by (simp add: permute_set_eq supp_perm)
-  then show "\<exists>q. q \<bullet> {} = p \<bullet> {} \<and> supp q \<subseteq> {} \<union> p \<bullet> {}" by blast
+  then show "\<exists>q. (\<forall>b \<in> {}. q \<bullet> b = p \<bullet> b) \<and> supp q \<subseteq> {} \<union> p \<bullet> {}" by blast
 next
   case (insert a bs)
-  then have " \<exists>q. q \<bullet> bs = p \<bullet> bs \<and> supp q \<subseteq> bs \<union> p \<bullet> bs" 
-    by (simp add: insert_eqvt) 
-  then obtain q where *: "q \<bullet> bs = p \<bullet> bs" and **: "supp q \<subseteq> bs \<union> p \<bullet> bs" by blast 
+  then have " \<exists>q. (\<forall>b \<in> bs. q \<bullet> b = p \<bullet> b) \<and> supp q \<subseteq> bs \<union> p \<bullet> bs" by simp 
+  then obtain q where *: "\<forall>b \<in> bs. q \<bullet> b = p \<bullet> b" and **: "supp q \<subseteq> bs \<union> p \<bullet> bs"
+    by (metis empty_subsetI insert(3) supp_swap) 
   { assume 1: "q \<bullet> a = p \<bullet> a"
-    have "q \<bullet> insert a bs = p \<bullet> insert a bs" using 1 * by (simp add: insert_eqvt)
+    have "\<forall>b \<in> (insert a bs). q \<bullet> b = p \<bullet> b" using 1 * by simp
     moreover 
     have "supp q \<subseteq> insert a bs \<union> p \<bullet> insert a bs" 
       using ** by (auto simp add: insert_eqvt)
     ultimately 
-    have "\<exists>q. q \<bullet> insert a bs = p \<bullet> insert a bs \<and> supp q \<subseteq> insert a bs \<union> p \<bullet> insert a bs" by blast
+    have "\<exists>q. (\<forall>b \<in> insert a bs. q \<bullet> b = p \<bullet> b) \<and> supp q \<subseteq> insert a bs \<union> p \<bullet> insert a bs" by blast
   }
   moreover
   { assume 2: "q \<bullet> a \<noteq> p \<bullet> a"
     def q' \<equiv> "((q \<bullet> a) \<rightleftharpoons> (p \<bullet> a)) + q"
-    { have "(q \<bullet> a) \<notin> (p \<bullet> bs)" using `a \<notin> bs` *[symmetric] by (simp add: mem_permute_iff)
-      moreover 
-      have "(p \<bullet> a) \<notin> (p \<bullet> bs)" using `a \<notin> bs` by (simp add: mem_permute_iff)
-      ultimately 
-      have "q' \<bullet> insert a bs = p \<bullet> insert a bs" using 2 * unfolding q'_def 
-        by (simp add: insert_eqvt  swap_set_not_in) 
-    }
+    have "\<forall>b \<in> insert a bs. q' \<bullet> b = p \<bullet> b" using 2 * `a \<notin> bs` unfolding q'_def
+      by (auto simp add: swap_atom)
     moreover 
     { have "{q \<bullet> a, p \<bullet> a} \<subseteq> insert a bs \<union> p \<bullet> insert a bs"
 	using ** 
@@ -1961,45 +1972,38 @@
         unfolding q'_def using supp_plus_perm by blast
     }
     ultimately 
-    have "\<exists>q. q \<bullet> insert a bs = p \<bullet> insert a bs \<and> supp q \<subseteq> insert a bs \<union> p \<bullet> insert a bs" by blast
+    have "\<exists>q. (\<forall>b \<in> insert a bs. q \<bullet> b = p \<bullet> b) \<and> supp q \<subseteq> insert a bs \<union> p \<bullet> insert a bs" by blast
   }
-  ultimately show "\<exists>q. q \<bullet> insert a bs = p \<bullet> insert a bs \<and> supp q \<subseteq> insert a bs \<union> p \<bullet> insert a bs"
+  ultimately show "\<exists>q. (\<forall>b \<in> insert a bs. q \<bullet> b = p \<bullet> b) \<and> supp q \<subseteq> insert a bs \<union> p \<bullet> insert a bs"
     by blast
 qed
 
+
 lemma list_renaming_perm:
-  fixes bs::"atom list"
-  shows "\<exists>q. q \<bullet> bs = p \<bullet> bs \<and> supp q \<subseteq> (set bs) \<union> (p \<bullet> (set bs))"
+  shows "\<exists>q. (\<forall>b \<in> set bs. q \<bullet> b = p \<bullet> b) \<and> supp q \<subseteq> set bs \<union> (p \<bullet> set bs)"
 proof (induct bs)
   case Nil
-  have "0 \<bullet> [] = p \<bullet> [] \<and> supp (0::perm) \<subseteq> set [] \<union> p \<bullet> set []"
-    by (simp add: permute_set_eq supp_perm)
-  then show "\<exists>q. q \<bullet> [] = p \<bullet> [] \<and> supp q \<subseteq> set [] \<union> p \<bullet> (set [])" by blast
+  have "(\<forall>b \<in> set []. 0 \<bullet> b = p \<bullet> b) \<and> supp (0::perm) \<subseteq> set [] \<union> p \<bullet> set []" 
+    by (simp add: supp_zero_perm)
+  then show "\<exists>q. (\<forall>b \<in> set []. q \<bullet> b = p \<bullet> b) \<and> supp q \<subseteq> set [] \<union> p \<bullet> (set [])" by blast
 next
   case (Cons a bs)
-  then have " \<exists>q. q \<bullet> bs = p \<bullet> bs \<and> supp q \<subseteq> set bs \<union> p \<bullet> (set bs)" 
-    by (simp add: insert_eqvt) 
-  then obtain q where *: "q \<bullet> bs = p \<bullet> bs" and **: "supp q \<subseteq> set bs \<union> p \<bullet> (set bs)" by blast 
+  then have " \<exists>q. (\<forall>b \<in> set bs. q \<bullet> b = p \<bullet> b) \<and> supp q \<subseteq> set bs \<union> p \<bullet> (set bs)"  by simp
+  then obtain q where *: "\<forall>b \<in> set bs. q \<bullet> b = p \<bullet> b" and **: "supp q \<subseteq> set bs \<union> p \<bullet> (set bs)"
+    by (blast)
   { assume 1: "a \<in> set bs"
     have "q \<bullet> a = p \<bullet> a" using * 1 by (induct bs) (auto)
-    then have "q \<bullet> (a # bs) = p \<bullet> (a # bs)" using * by simp 
+    then have "\<forall>b \<in> set (a # bs). q \<bullet> b = p \<bullet> b" using * by simp 
     moreover 
     have "supp q \<subseteq> set (a # bs) \<union> p \<bullet> (set (a # bs))" using ** by (auto simp add: insert_eqvt)
     ultimately 
-    have "\<exists>q. q \<bullet> (a # bs) = p \<bullet> (a # bs) \<and> supp q \<subseteq> set (a # bs) \<union> p \<bullet> (set (a # bs))" by blast
+    have "\<exists>q. (\<forall>b \<in> set (a # bs). q \<bullet> b = p \<bullet> b) \<and> supp q \<subseteq> set (a # bs) \<union> p \<bullet> (set (a # bs))" by blast
   }
   moreover
   { assume 2: "a \<notin> set bs"
     def q' \<equiv> "((q \<bullet> a) \<rightleftharpoons> (p \<bullet> a)) + q"
-    { have "(q \<bullet> a) \<sharp> (p \<bullet> bs)" using `a \<notin> set bs` *[symmetric] 
-	by (simp add: fresh_permute_iff) (simp add: fresh_def supp_of_atom_list)
-      moreover 
-      have "(p \<bullet> a) \<sharp> (p \<bullet> bs)" using `a \<notin> set bs` 
-	by (simp add: fresh_permute_iff) (simp add: fresh_def supp_of_atom_list)
-      ultimately 
-      have "q' \<bullet> (a # bs) = p \<bullet> (a # bs)" using 2 * unfolding q'_def 
-        by (simp add: swap_fresh_fresh) 
-    }
+    have "\<forall>b \<in> set (a # bs). q' \<bullet> b = p \<bullet> b" 
+      unfolding q'_def using 2 * `a \<notin> set bs` by (auto simp add: swap_atom)
     moreover 
     { have "{q \<bullet> a, p \<bullet> a} \<subseteq> set (a # bs) \<union> p \<bullet> (set (a # bs))"
 	using **
@@ -2019,14 +2023,13 @@
         unfolding q'_def using supp_plus_perm by blast
     }
     ultimately 
-    have "\<exists>q. q \<bullet> (a # bs) = p \<bullet> (a # bs) \<and> supp q \<subseteq> set (a # bs) \<union> p \<bullet> (set (a # bs))" by blast
+    have "\<exists>q. (\<forall>b \<in> set (a # bs).  q \<bullet> b = p \<bullet> b) \<and> supp q \<subseteq> set (a # bs) \<union> p \<bullet> (set (a # bs))" by blast
   }
-  ultimately show "\<exists>q. q \<bullet> (a # bs) = p \<bullet> (a # bs) \<and> supp q \<subseteq> set (a # bs) \<union> p \<bullet> (set (a # bs))"
+  ultimately show "\<exists>q. (\<forall>b \<in> set (a # bs). q \<bullet> b = p \<bullet> b) \<and> supp q \<subseteq> set (a # bs) \<union> p \<bullet> (set (a # bs))"
     by blast
 qed
 
 
-
 section {* Concrete Atoms Types *}
 
 text {*