--- a/Nominal/Ex/Foo2.thy	Tue Dec 07 14:27:39 2010 +0000
+++ b/Nominal/Ex/Foo2.thy	Tue Dec 07 19:16:09 2010 +0000
@@ -49,179 +49,9 @@
   tests by cu
 *}
 
-lemma set_renaming_perm:
-  assumes a: "p \<bullet> bs \<inter> bs = {}" 
-  and     b: "finite bs"
-  shows "\<exists>q. q \<bullet> bs = p \<bullet> bs \<and> supp q \<subseteq> bs \<union> (p \<bullet> bs)"
-using b a
-proof (induct)
-  case empty
-  have "0 \<bullet> {} = p \<bullet> {} \<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
-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 (perm_simp) (auto)
-  then obtain q where *: "q \<bullet> bs = p \<bullet> bs" and **: "supp q \<subseteq> bs \<union> p \<bullet> bs" by blast 
-  { 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)
-    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
-  }
-  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) 
-    }
-    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)
-      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" 
-	using ** by (auto simp add: insert_eqvt)
-      ultimately 
-      have "supp q' \<subseteq> insert a bs \<union> p \<bullet> insert a bs" 
-        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
-  }
-  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"
-    by blast
-qed
-
-
-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
+text {* *}
 
-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 []"
-    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
-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 (perm_simp) (auto)
-  then obtain q where *: "q \<bullet> bs = p \<bullet> bs" 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 
-    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
-  }
-  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) 
-    }
-    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)
-      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))" 
-	using ** by (auto simp add: insert_eqvt)
-      ultimately 
-      have "supp q' \<subseteq> set (a # bs) \<union> p \<bullet> (set (a # bs))" 
-        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
-  }
-  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))"
-    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
 
 (*
 thm at_set_avoiding1[THEN exE]

--- 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

--- a/Nominal/Nominal2_Base.thy	Tue Dec 07 14:27:39 2010 +0000
+++ b/Nominal/Nominal2_Base.thy	Tue Dec 07 19:16:09 2010 +0000
@@ -1699,6 +1699,117 @@
   then show "\<exists>p. (p \<bullet> a) \<sharp> c \<and> supp x \<sharp>* p" by blast
 qed
 
+section {* Renaming permutations *}
+
+
+lemma set_renaming_perm:
+  assumes a: "p \<bullet> bs \<inter> bs = {}" 
+  and     b: "finite bs"
+  shows "\<exists>q. q \<bullet> bs = p \<bullet> bs \<and> supp q \<subseteq> bs \<union> (p \<bullet> bs)"
+using b a
+proof (induct)
+  case empty
+  have "0 \<bullet> {} = p \<bullet> {} \<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
+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 
+  { 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)
+    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
+  }
+  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) 
+    }
+    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)
+      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" 
+	using ** by (auto simp add: insert_eqvt)
+      ultimately 
+      have "supp q' \<subseteq> insert a bs \<union> p \<bullet> insert a bs" 
+        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
+  }
+  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"
+    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 []"
+    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
+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 
+  { 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 
+    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
+  }
+  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) 
+    }
+    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)
+      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))" 
+	using ** by (auto simp add: insert_eqvt)
+      ultimately 
+      have "supp q' \<subseteq> set (a # bs) \<union> p \<bullet> (set (a # bs))" 
+        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
+  }
+  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))"
+    by blast
+qed
+
+
 
 section {* Concrete Atoms Types *}