--- a/Nominal/Abs.thy	Wed Mar 17 12:23:04 2010 +0100
+++ b/Nominal/Abs.thy	Wed Mar 17 17:09:01 2010 +0100
@@ -74,7 +74,7 @@
   and a: "\<And>pi t s. (R t s \<Longrightarrow> R (pi \<bullet> t) (pi \<bullet> s))"
   shows "(ab, s) \<approx>gen R f (- pi) (aa, t)"
   using b apply -
-  apply(simp add: alpha_gen.simps)
+  apply(simp add: alpha_gen)
   apply(erule conjE)+
   apply(rule conjI)
   apply(simp add: fresh_star_def fresh_minus_perm)
@@ -86,6 +86,35 @@
   apply assumption
   done
 
+lemma alpha_gen_compose_sym2:
+  assumes a: "(aa, (t1, t2)) \<approx>gen (\<lambda>(x11, x12) (x21, x22). R1 x11 x21 \<and> R1 x21 x11 \<and> R2 x12 x22 \<and> R2 x22 x12)
+  (\<lambda>(b, a). fb b \<union> fa a) pi (ab, (s1, s2))"
+  and r1: "\<And>pi t s. R1 t s \<Longrightarrow> R1 (pi \<bullet> t) (pi \<bullet> s)"
+  and r2: "\<And>pi t s. R2 t s \<Longrightarrow> R2 (pi \<bullet> t) (pi \<bullet> s)"
+  shows "(ab, (s1, s2)) \<approx>gen
+ (\<lambda>x1 x2. (\<lambda>(a, b) (d, c). R1 a d \<and> R2 b c) x1 x2 \<and> (\<lambda>(a, b) (d, c). R1 a d \<and> R2 b c) x2 x1)
+ (\<lambda>(b, a). fb b \<union> fa a) (- pi) (aa, (t1, t2))"
+ using a
+apply(simp add: alpha_gen)
+apply clarify
+apply (rule conjI)
+  apply(simp add: fresh_star_def fresh_minus_perm)
+apply (rule conjI)
+apply (rotate_tac 3)
+apply (drule_tac pi="- pi" in r1)
+apply simp
+apply (rule conjI)
+apply (rotate_tac -1)
+apply (drule_tac pi="- pi" in r2)
+apply simp
+apply (rule conjI)
+apply (drule_tac pi="- pi" in r1)
+apply simp
+apply (rule conjI)
+apply (drule_tac pi="- pi" in r2)
+apply simp_all
+done
+
 lemma alpha_gen_compose_trans:
   fixes pi pia
   assumes b: "(aa, t) \<approx>gen (\<lambda>x1 x2. R x1 x2 \<and> (\<forall>x. R x2 x \<longrightarrow> R x1 x)) f pi (ab, ta)"