--- a/Nominal/Nominal2_Abs.thy	Sun Jan 30 09:57:37 2011 +0900
+++ b/Nominal/Nominal2_Abs.thy	Sun Jan 30 12:09:23 2011 +0900
@@ -285,7 +285,7 @@
   then have "(supp x' - as') \<inter> (p \<bullet> (supp x \<inter> as)) = {}" using a by (simp add: alphas)
   ultimately show "p \<bullet> (supp x \<inter> as) = supp x' \<inter> as'"
     by (auto dest: disjoint_right_eq)
-qed 
+qed
 
 lemma alpha_abs_res_stronger1_aux:
   assumes asm: "(as, x) \<approx>res (op =) supp p' (as', x')"
@@ -320,6 +320,26 @@
   show "\<exists>p. (as, x) \<approx>res (op =) supp p (as', x') \<and> supp p \<subseteq> (supp x \<inter> as) \<union> (supp x' \<inter> as')" by blast
 qed
 
+lemma alpha_abs_res_minimal:
+  assumes asm: "(as, x) \<approx>res (op =) supp p (as', x')"
+  shows "(as \<inter> supp x, x) \<approx>res (op =) supp p (as' \<inter> supp x', x')"
+  using asm unfolding alpha_res by (auto simp add: Diff_Int)
+
+lemma alpha_abs_res_abs_set:
+  assumes asm: "(as, x) \<approx>res (op =) supp p (as', x')"
+  shows "(as \<inter> supp x, x) \<approx>set (op =) supp p (as' \<inter> supp x', x')"
+proof -
+  have c: "p \<bullet> x = x'"
+    using alpha_abs_res_minimal[OF asm] unfolding alpha_res by clarify
+  then have a: "supp x - as \<inter> supp x = supp (p \<bullet> x) - as' \<inter> supp (p \<bullet> x)"
+    using alpha_abs_res_minimal[OF asm] by (simp add: alpha_res)
+  have b: "(supp x - as \<inter> supp x) \<sharp>* p"
+    using alpha_abs_res_minimal[OF asm] unfolding alpha_res by clarify
+  have "p \<bullet> (as \<inter> supp x) = as' \<inter> supp (p \<bullet> x)"
+    by (metis Int_commute asm c supp_property_res)
+  then show ?thesis using a b c unfolding alpha_set by simp
+qed
+
 lemma alpha_abs_res_stronger1:
   assumes asm: "(as, x) \<approx>res (op =) supp p' (as', x')"
   shows "\<exists>p. (as, x) \<approx>res (op =) supp p (as', x') \<and> supp p \<subseteq> as \<union> as'"