diff -r 7b8f570b2450 -r 6b1eea8dcdc0 Nominal/Abs.thy
--- a/Nominal/Abs.thy	Mon Mar 22 17:21:27 2010 +0100
+++ b/Nominal/Abs.thy	Mon Mar 22 18:29:29 2010 +0100
@@ -642,7 +642,7 @@
   and a: "\<And>pi t s. (R t s \<Longrightarrow> R (pi \<bullet> t) (pi \<bullet> s))"
   shows "(aa, t) \<approx>gen R f (pia + pi) (ac, sa)"
   using b c apply -
-  apply(simp add: alpha_gen.simps)
+  apply(simp add: alpha_gen)
   apply(erule conjE)+
   apply(simp add: fresh_star_plus)
   apply(drule_tac x="- pia \<bullet> sa" in spec)
@@ -655,6 +655,40 @@
   apply(simp)
   done
 
+lemma alpha_gen_compose_trans2:
+  fixes pi pia
+  assumes b: "(aa, (t1, t2)) \<approx>gen
+    (\<lambda>(b, a) (d, c). R1 b d \<and> (\<forall>z. R1 d z \<longrightarrow> R1 b z) \<and> R2 a c \<and> (\<forall>z. R2 c z \<longrightarrow> R2 a z))
+    (\<lambda>(b, a). fv_a b \<union> fv_b a) pi (ab, (ta1, ta2))"
+  and c: "(ab, (ta1, ta2)) \<approx>gen (\<lambda>(b, a) (d, c). R1 b d \<and> R2 a c) (\<lambda>(b, a). fv_a b \<union> fv_b a)
+    pia (ac, (sa1, sa2))"
+  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 "(aa, (t1, t2)) \<approx>gen (\<lambda>(b, a) (d, c). R1 b d \<and> R2 a c) (\<lambda>(b, a). fv_a b \<union> fv_b a)
+    (pia + pi) (ac, (sa1, sa2))"
+  using b c apply -
+  apply(simp add: alpha_gen2)
+  apply(simp add: alpha_gen)
+  apply(erule conjE)+
+  apply(simp add: fresh_star_plus)
+  apply(drule_tac x="- pia \<bullet> sa1" in spec)
+  apply(drule mp)
+  apply(rotate_tac 5)
+  apply(drule_tac pi="- pia" in r1)
+  apply(simp)
+  apply(rotate_tac -1)
+  apply(drule_tac pi="pia" in r1)
+  apply(simp)
+  apply(drule_tac x="- pia \<bullet> sa2" in spec)
+  apply(drule mp)
+  apply(rotate_tac 6)
+  apply(drule_tac pi="- pia" in r2)
+  apply(simp)
+  apply(rotate_tac -1)
+  apply(drule_tac pi="pia" in r2)
+  apply(simp)
+  done
+
 lemma alpha_gen_compose_eqvt:
   fixes  pia
   assumes b: "(g d, t) \<approx>gen (\<lambda>x1 x2. R x1 x2 \<and> R (pi \<bullet> x1) (pi \<bullet> x2)) f pia (g e, s)"