--- a/Nominal/Abs.thy	Tue Apr 20 11:29:00 2010 +0200
+++ b/Nominal/Abs.thy	Tue Apr 20 18:24:50 2010 +0200
@@ -423,15 +423,50 @@
 apply(simp)
 done
 
-
+lemma 
+  fixes t1 s1::"'a::fs"
+  and   t2 s2::"'b::fs"
+  shows "Abs as (t1, t2) = Abs bs (s1, s2) \<longrightarrow> (Abs as t1 = Abs bs s1 \<and>  Abs as t2 = Abs bs s2)"
+apply(subst abs_eq_iff)
+apply(subst alphas_abs)
+apply(subst alphas)
+apply(rule impI)
+apply(erule exE)
+apply(simp add: supp_Pair)
+apply(simp add: Un_Diff)
+apply(simp add: fresh_star_union)
+apply(erule conjE)+
+apply(rule conjI)
+apply(rule trans)
+apply(rule sym)
+apply(rule_tac p="p" in supp_perm_eq)
+apply(simp add: supp_abs)
+apply(simp)
+apply(rule trans)
+apply(rule sym)
+apply(rule_tac p="p" in supp_perm_eq)
+apply(simp add: supp_abs)
+apply(simp)
+done
 
-(* support of concrete atom sets *)
+lemma fresh_star_eq:
+  assumes a: "as \<sharp>* p"
+  shows "\<forall>a \<in> as. p \<bullet> a = a"
+using a by (simp add: fresh_star_def fresh_def supp_perm)
+
+lemma fresh_star_set_eq:
+  assumes a: "as \<sharp>* p"
+  shows "p \<bullet> as = as"
+using a 
+apply(simp add: fresh_star_def fresh_def supp_perm permute_set_eq)
+apply(auto)
+by (metis permute_atom_def)
 
 lemma 
   fixes t1 s1::"'a::fs"
   and   t2 s2::"'b::fs"
   assumes asm: "finite as"
-  shows "(Abs as t1 = Abs as s1 \<and>  Abs as t2 = Abs as s2) \<longrightarrow> Abs as (t1, t2) = Abs as (s1, s2)"
+  shows "(Abs as t1 = Abs bs s1 \<and>  Abs as t2 = Abs bs s2) \<longrightarrow> Abs as (t1, t2) = Abs bs (s1, s2)"
 apply(subst abs_eq_iff)
 apply(subst abs_eq_iff)
 apply(subst alphas_abs)