# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1271339798 -7200
# Node ID d744b157dd2ac0615d2bcbb33eb5254410a8cce6
# Parent  591cc76da570dc733dc8961a53b4fafde017098a# Parent  c8e406f64db081ed302ed85022309568c43a54cd
merged

diff -r c8e406f64db0 -r d744b157dd2a Nominal/Abs.thy
--- a/Nominal/Abs.thy	Thu Apr 15 15:31:36 2010 +0200
+++ b/Nominal/Abs.thy	Thu Apr 15 15:56:38 2010 +0200
@@ -397,6 +397,58 @@
 
 section {* BELOW is stuff that may or may not be needed *}
 
+lemma 
+  fixes t1 s1::"'a::fs"
+  and   t2 s2::"'b::fs"
+  shows "Abs as (t1, t2) = Abs as (s1, s2) \<longrightarrow> (Abs as t1 = Abs as s1 \<and>  Abs as t2 = Abs as 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 
+  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)"
+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(simp add: abs_eq_iff)
+apply(simp add: alphas_abs)
+apply(simp add: alphas)
+apply(rule conjI)
+apply(simp add: supp_Pair Un_Diff)
+oops
+
+
+
 (* support of concrete atom sets *)
 
 lemma supp_atom_image: