--- a/Nominal/Nominal2_Abs.thy	Sun Jan 30 12:09:23 2011 +0900
+++ b/Nominal/Nominal2_Abs.thy	Tue Feb 01 08:48:14 2011 +0900
@@ -340,6 +340,11 @@
   then show ?thesis using a b c unfolding alpha_set by simp
 qed
 
+lemma alpha_abs_set_abs_res:
+  assumes asm: "(as \<inter> supp x, x) \<approx>set (op =) supp p (as' \<inter> supp x', x')"
+  shows "(as, x) \<approx>res (op =) supp p (as', x')"
+  using asm unfolding alphas by (auto simp add: Diff_Int)
+
 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'"
@@ -503,6 +508,25 @@
     (\<exists>p. (bsl, x) \<approx>lst (op =) supp p (csl, y) \<and> supp p \<subseteq> set bsl \<union> set csl)"
   by (lifting alphas_abs_stronger)
 
+lemma Abs_eq_res_set:
+  "(([bs]res. x) = ([cs]res. y)) = (([(bs \<inter> supp x)]set. x) = ([(cs \<inter> supp y)]set. y))"
+  unfolding Abs_eq_iff
+  using alpha_abs_set_abs_res alpha_abs_res_abs_set
+  apply auto
+  apply (rule_tac x="p" in exI)
+  apply assumption
+  apply (rule_tac x="p" in exI)
+  apply assumption
+  done
+
+lemma Abs_eq_res_supp:
+  assumes asm: "supp x \<subseteq> bs"
+  shows "([as]res. x) = ([as \<inter> bs]res. x)"
+  unfolding Abs_eq_iff alphas
+  apply (rule_tac x="0::perm" in exI)
+  apply (simp add: fresh_star_zero)
+  using asm by blast
+
 lemma Abs_exhausts:
   shows "(\<And>as (x::'a::pt). y1 = Abs_set as x \<Longrightarrow> P1) \<Longrightarrow> P1"
   and   "(\<And>as (x::'a::pt). y2 = Abs_res as x \<Longrightarrow> P2) \<Longrightarrow> P2"