diff -r 7b1a3df239cd -r 10a0e3578507 Quot/Nominal/Abs.thy
--- a/Quot/Nominal/Abs.thy	Mon Feb 22 14:50:53 2010 +0100
+++ b/Quot/Nominal/Abs.thy	Mon Feb 22 15:03:48 2010 +0100
@@ -74,11 +74,11 @@
   apply(clarsimp)
   done
 
-(* introduced for examples *)
-lemma alpha_gen_atom_sym:
-  assumes a: "\<And>pi t s. (R t s \<Longrightarrow> R (pi \<bullet> t) (pi \<bullet> s))"
-  shows "\<exists>pi. ({atom a}, t) \<approx>gen (\<lambda>x1 x2. R x1 x2 \<and> R x2 x1) f pi ({atom b}, s) \<Longrightarrow>
-        \<exists>pi. ({atom b}, s) \<approx>gen R f pi ({atom a}, t)"
+lemma alpha_gen_compose_sym:
+  assumes b: "\<exists>pi. (aa, t) \<approx>gen (\<lambda>x1 x2. R x1 x2 \<and> R x2 x1) f pi (ab, s)"
+  and a: "\<And>pi t s. (R t s \<Longrightarrow> R (pi \<bullet> t) (pi \<bullet> s))"
+  shows "\<exists>pi. (ab, s) \<approx>gen R f pi (aa, t)"
+  using b apply -
   apply(erule exE)
   apply(rule_tac x="- pi" in exI)
   apply(simp add: alpha_gen.simps)
@@ -91,11 +91,12 @@
   apply assumption
   done
 
-lemma alpha_gen_atom_trans:
-  assumes a: "\<And>pi t s. (R t s \<Longrightarrow> R (pi \<bullet> t) (pi \<bullet> s))"
-  shows "\<lbrakk>\<exists>pi\<Colon>perm. ({atom a}, t) \<approx>gen (\<lambda>x1 x2. R x1 x2 \<and> (\<forall>x. R x2 x \<longrightarrow> R x1 x)) f pi ({atom aa}, ta);
-        \<exists>pi\<Colon>perm. ({atom aa}, ta) \<approx>gen R f pi ({atom ba}, sa)\<rbrakk>
-    \<Longrightarrow> \<exists>pi\<Colon>perm. ({atom a}, t) \<approx>gen R f pi ({atom ba}, sa)"
+lemma alpha_gen_compose_trans:
+  assumes b: "\<exists>pi\<Colon>perm. (aa, t) \<approx>gen (\<lambda>x1 x2. R x1 x2 \<and> (\<forall>x. R x2 x \<longrightarrow> R x1 x)) f pi (ab, ta)"
+  and c: "\<exists>pi\<Colon>perm. (ab, ta) \<approx>gen R f pi (ac, sa)"
+  and a: "\<And>pi t s. (R t s \<Longrightarrow> R (pi \<bullet> t) (pi \<bullet> s))"
+  shows "\<exists>pi\<Colon>perm. (aa, t) \<approx>gen R f pi (ac, sa)"
+  using b c apply -
   apply(simp add: alpha_gen.simps)
   apply(erule conjE)+
   apply(erule exE)+