diff -r eef49daac6c8 -r 7e7662890477 Nominal/Nominal2_Base.thy
--- a/Nominal/Nominal2_Base.thy	Tue Jan 18 22:11:49 2011 +0900
+++ b/Nominal/Nominal2_Base.thy	Tue Jan 18 17:19:50 2011 +0100
@@ -549,6 +549,21 @@
   shows "p \<bullet> (insert x A) = insert (p \<bullet> x) (p \<bullet> A)"
   unfolding permute_set_eq_image image_insert ..
 
+lemma Collect_eqvt:
+  shows "p \<bullet> {x. P x} = {x. (p \<bullet> P) x}"
+  unfolding Collect_def permute_fun_def ..
+
+lemma inter_eqvt:
+  shows "p \<bullet> (A \<inter> B) = (p \<bullet> A) \<inter> (p \<bullet> B)"
+  unfolding Int_def
+  apply(simp add: Collect_eqvt)
+  apply(simp add: permute_fun_def)
+  apply(simp add: conj_eqvt)
+  apply(simp add: mem_eqvt)
+  apply(simp add: permute_fun_def)
+  done
+
+
 
 subsection {* Permutations for units *}
 
@@ -1997,7 +2012,29 @@
     by blast
 qed
 
-
+lemma set_renaming_perm2:
+  shows "\<exists>q. (\<forall>b \<in> bs. q \<bullet> b = p \<bullet> b) \<and> supp q \<subseteq> bs \<union> (p \<bullet> bs)"
+proof -
+  have "finite (bs \<inter> supp p)" by (simp add: finite_supp)
+  then obtain q 
+    where *: "\<forall>b \<in> bs \<inter> supp p. q \<bullet> b = p \<bullet> b" and **: "supp q \<subseteq> (bs \<inter> supp p) \<union> (p \<bullet> (bs \<inter> supp p))"
+    using set_renaming_perm by blast
+  from ** have "supp q \<subseteq> bs \<union> (p \<bullet> bs)" by (auto simp add: inter_eqvt)
+  moreover
+  have "\<forall>b \<in> bs - supp p. q \<bullet> b = p \<bullet> b" 
+    apply(auto)
+    apply(subgoal_tac "b \<notin> supp q")
+    apply(simp add: fresh_def[symmetric])
+    apply(simp add: fresh_perm)
+    apply(clarify)
+    apply(rotate_tac 2)
+    apply(drule subsetD[OF **])
+    apply(simp add: inter_eqvt supp_eqvt permute_self)
+    done
+  ultimately have "(\<forall>b \<in> bs. q \<bullet> b = p \<bullet> b) \<and> supp q \<subseteq> bs \<union> (p \<bullet> bs)" using * by auto
+  then show "\<exists>q. (\<forall>b \<in> bs. q \<bullet> b = p \<bullet> b) \<and> supp q \<subseteq> bs \<union> (p \<bullet> bs)" by blast
+qed
+    
 lemma list_renaming_perm:
   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)