--- a/Nominal/Abs.thy	Wed Apr 21 12:37:19 2010 +0200
+++ b/Nominal/Abs.thy	Wed Apr 21 12:37:44 2010 +0200
@@ -465,7 +465,30 @@
 lemma 
   fixes t1 s1::"'a::fs"
   and   t2 s2::"'b::fs"
-  assumes asm: "finite as"
+  shows "Abs as t1 = Abs bs s1 \<longrightarrow> Abs (as \<union> cs) t1 = Abs (bs \<union> cs) s1"
+apply(subst abs_eq_iff)
+apply(subst abs_eq_iff)
+apply(subst alphas_abs)
+apply(subst alphas_abs)
+apply(subst alphas)
+apply(subst alphas)
+apply(rule impI)
+apply(erule exE | erule conjE)+
+apply(rule_tac x="p" in exI)
+apply(simp)
+apply(rule conjI)
+apply(auto)[1]
+apply(rule conjI)
+apply(auto)[1]
+apply(simp add: fresh_star_def)
+apply(auto)[1]
+apply(simp add: union_eqvt)
+oops
+
+
+lemma 
+  fixes t1 s1::"'a::fs"
+  and   t2 s2::"'b::fs"
   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)
@@ -486,6 +509,39 @@
 
 (* support of concrete atom sets *)
 
+lemma
+  shows "Abs as t = Abs (supp t \<inter> as) t"
+apply(simp add: abs_eq_iff)
+apply(simp add: alphas_abs)
+apply(rule_tac x="0" in exI)
+apply(simp add: alphas)
+apply(auto)
+oops
+
+lemma
+  assumes "finite S"
+  shows "\<exists>q. supp q \<subseteq> S \<union> p \<bullet> S \<and> (\<forall>a \<in> S. q \<bullet> a = p \<bullet> a)"
+using assms
+apply(induct)
+apply(rule_tac x="0" in exI)
+apply(simp add: supp_zero_perm)
+apply(auto)
+apply(simp add: insert_eqvt)
+apply(rule_tac x="((p \<bullet> x) \<rightleftharpoons> x) + q" in exI)
+apply(rule conjI)
+apply(rule subset_trans)
+apply(rule supp_plus_perm)
+apply(simp add: supp_swap)
+apply(auto)[1]
+apply(simp)
+apply(rule conjI)
+apply(case_tac "q \<bullet> x = x")
+apply(simp)
+apply(simp add: supp_perm)
+apply(case_tac "x \<in> p \<bullet> F")
+sorry
+
+
 lemma supp_atom_image:
   fixes as::"'a::at_base set"
   shows "supp (atom ` as) = supp as"