--- a/Nominal/Nominal2_Abs.thy	Tue Dec 07 14:27:39 2010 +0000
+++ b/Nominal/Nominal2_Abs.thy	Tue Dec 07 19:16:09 2010 +0000
@@ -540,6 +540,77 @@
   by(auto simp add: Abs_fresh_iff)
 
 
+subsection {* Renaming of bodies of abstractions *}
+
+
+lemma Abs_rename_set:
+  fixes x::"'a::fs"
+  assumes a: "(p \<bullet> bs) \<sharp>* (bs, x)" 
+  and     b: "finite bs"
+  shows "\<exists>y. [bs]set. x = [p \<bullet> bs]set. y"
+proof -
+  from a b have "p \<bullet> bs \<inter> bs = {}" using at_fresh_star_inter by (auto simp add: fresh_star_Pair)   
+  with set_renaming_perm 
+  obtain q where *: "q \<bullet> bs = p \<bullet> bs" and **: "supp q \<subseteq> bs \<union> (p \<bullet> bs)" using b by metis
+  have "[bs]set. x =  q \<bullet> ([bs]set. x)"
+    apply(rule perm_supp_eq[symmetric])
+    using a **
+    unfolding fresh_star_Pair
+    unfolding Abs_fresh_star_iff
+    unfolding fresh_star_def
+    by auto
+  also have "\<dots> = [q \<bullet> bs]set. (q \<bullet> x)" by simp
+  also have "\<dots> = [p \<bullet> bs]set. (q \<bullet> x)" using * by simp
+  finally have "[bs]set. x = [p \<bullet> bs]set. (q \<bullet> x)" .
+  then show "\<exists>y. [bs]set. x = [p \<bullet> bs]set. y" by blast
+qed
+
+lemma Abs_rename_res:
+  fixes x::"'a::fs"
+  assumes a: "(p \<bullet> bs) \<sharp>* (bs, x)" 
+  and     b: "finite bs"
+  shows "\<exists>y. [bs]res. x = [p \<bullet> bs]res. y"
+proof -
+  from a b have "p \<bullet> bs \<inter> bs = {}" using at_fresh_star_inter by (simp add: fresh_star_Pair) 
+  with set_renaming_perm 
+  obtain q where *: "q \<bullet> bs = p \<bullet> bs" and **: "supp q \<subseteq> bs \<union> (p \<bullet> bs)" using b by metis
+  have "[bs]res. x =  q \<bullet> ([bs]res. x)"
+    apply(rule perm_supp_eq[symmetric])
+    using a **
+    unfolding fresh_star_Pair
+    unfolding Abs_fresh_star_iff
+    unfolding fresh_star_def
+    by auto
+  also have "\<dots> = [q \<bullet> bs]res. (q \<bullet> x)" by simp
+  also have "\<dots> = [p \<bullet> bs]res. (q \<bullet> x)" using * by simp
+  finally have "[bs]res. x = [p \<bullet> bs]res. (q \<bullet> x)" .
+  then show "\<exists>y. [bs]res. x = [p \<bullet> bs]res. y" by blast
+qed
+
+lemma Abs_rename_list:
+  fixes x::"'a::fs"
+  assumes a: "(p \<bullet> (set bs)) \<sharp>* (bs, x)" 
+  shows "\<exists>y. [bs]lst. x = [p \<bullet> bs]lst. y"
+proof -
+  from a have "p \<bullet> (set bs) \<inter> (set bs) = {}" using at_fresh_star_inter 
+    by (simp add: fresh_star_Pair fresh_star_set)
+  with list_renaming_perm 
+  obtain q where *: "q \<bullet> bs = p \<bullet> bs" and **: "supp q \<subseteq> set bs \<union> (p \<bullet> set bs)" by metis 
+  have "[bs]lst. x =  q \<bullet> ([bs]lst. x)"
+    apply(rule perm_supp_eq[symmetric])
+    using a **
+    unfolding fresh_star_Pair
+    unfolding Abs_fresh_star_iff
+    unfolding fresh_star_def
+    by auto
+  also have "\<dots> = [q \<bullet> bs]lst. (q \<bullet> x)" by simp
+  also have "\<dots> = [p \<bullet> bs]lst. (q \<bullet> x)" using * by simp
+  finally have "[bs]lst. x = [p \<bullet> bs]lst. (q \<bullet> x)" .
+  then show "\<exists>y. [bs]lst. x = [p \<bullet> bs]lst. y" by blast
+qed
+
+
+
 section {* Infrastructure for building tuples of relations and functions *}
 
 fun