--- a/Nominal/Nominal2_Abs.thy	Sun Dec 19 07:50:37 2010 +0000
+++ b/Nominal/Nominal2_Abs.thy	Tue Dec 21 10:28:08 2010 +0000
@@ -547,7 +547,7 @@
   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"
+  shows "\<exists>q. [bs]set. x = [p \<bullet> bs]set. (q \<bullet> x) \<and> q \<bullet> bs = p \<bullet> bs"
 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 
@@ -560,16 +560,15 @@
     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
+  finally have "[bs]set. x = [p \<bullet> bs]set. (q \<bullet> x)" by (simp add: *)
+  then show "\<exists>q. [bs]set. x = [p \<bullet> bs]set. (q \<bullet> x) \<and> q \<bullet> bs = p \<bullet> bs" using * by metis
 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"
+  shows "\<exists>q. [bs]res. x = [p \<bullet> bs]res. (q \<bullet> x) \<and> q \<bullet> bs = p \<bullet> bs"
 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 
@@ -582,15 +581,14 @@
     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
+  finally have "[bs]res. x = [p \<bullet> bs]res. (q \<bullet> x)" by (simp add: *)
+  then show "\<exists>q. [bs]res. x = [p \<bullet> bs]res. (q \<bullet> x) \<and> q \<bullet> bs = p \<bullet> bs" using * by metis
 qed
 
 lemma Abs_rename_lst:
   fixes x::"'a::fs"
   assumes a: "(p \<bullet> (set bs)) \<sharp>* (bs, x)" 
-  shows "\<exists>y. [bs]lst. x = [p \<bullet> bs]lst. y"
+  shows "\<exists>q. [bs]lst. x = [p \<bullet> bs]lst. (q \<bullet> x) \<and> q \<bullet> bs = p \<bullet> bs"
 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)
@@ -604,12 +602,32 @@
     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
+  finally have "[bs]lst. x = [p \<bullet> bs]lst. (q \<bullet> x)" by (simp add: *)
+  then show "\<exists>q. [bs]lst. x = [p \<bullet> bs]lst. (q \<bullet> x) \<and> q \<bullet> bs = p \<bullet> bs" using * by metis
 qed
 
 
+text {* for deep recursive binders *}
+
+lemma Abs_rename_set':
+  fixes x::"'a::fs"
+  assumes a: "(p \<bullet> bs) \<sharp>* (bs, x)" 
+  and     b: "finite bs"
+  shows "\<exists>q. [bs]set. x = [q \<bullet> bs]set. (q \<bullet> x) \<and> q \<bullet> bs = p \<bullet> bs"
+using Abs_rename_set[OF a b] by metis
+
+lemma Abs_rename_res':
+  fixes x::"'a::fs"
+  assumes a: "(p \<bullet> bs) \<sharp>* (bs, x)" 
+  and     b: "finite bs"
+  shows "\<exists>q. [bs]res. x = [q \<bullet> bs]res. (q \<bullet> x) \<and> q \<bullet> bs = p \<bullet> bs"
+using Abs_rename_res[OF a b] by metis
+
+lemma Abs_rename_lst':
+  fixes x::"'a::fs"
+  assumes a: "(p \<bullet> (set bs)) \<sharp>* (bs, x)" 
+  shows "\<exists>q. [bs]lst. x = [q \<bullet> bs]lst. (q \<bullet> x) \<and> q \<bullet> bs = p \<bullet> bs"
+using Abs_rename_lst[OF a] by metis
 
 section {* Infrastructure for building tuples of relations and functions *}