--- a/Nominal/Nominal2_Abs.thy	Thu Feb 03 02:51:57 2011 +0000
+++ b/Nominal/Nominal2_Abs.thy	Thu Feb 03 02:57:04 2011 +0000
@@ -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,31 @@
   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_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'"
@@ -483,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"