--- a/Nominal/Abs.thy	Fri Mar 26 17:22:17 2010 +0100
+++ b/Nominal/Abs.thy	Fri Mar 26 22:22:41 2010 +0100
@@ -587,24 +587,36 @@
   by (simp_all add: fresh_zero_perm)
 
 lemma alpha_gen_sym:
-  assumes a: "R (p \<bullet> x) y \<Longrightarrow> R (- p \<bullet> y) x"
+  assumes a: "R (p \<bullet> x) y \<Longrightarrow> R y (p \<bullet> x)"
+  and     b: "\<And>x y p. R x y \<Longrightarrow> R (p \<bullet> x) (p \<bullet> y)"
   shows "(bs, x) \<approx>gen R f p (cs, y) \<Longrightarrow> (cs, y) \<approx>gen R f (- p) (bs, x)"
   and   "(bs, x) \<approx>res R f p (cs, y) \<Longrightarrow> (cs, y) \<approx>res R f (- p) (bs, x)"
   and   "(ds, x) \<approx>lst R f p (es, y) \<Longrightarrow> (es, y) \<approx>lst R f (- p) (ds, x)"
+  unfolding alphas fresh_star_def
+  apply (erule_tac [1] conjE)+
+  apply (erule_tac [2] conjE)+
+  apply (erule_tac [3] conjE)+
   using a
-  unfolding alphas
-  unfolding fresh_star_def
-  by (auto simp add:  fresh_minus_perm)
-
+  apply (simp_all add: fresh_minus_perm)
+  apply (rotate_tac [!] -1)
+  apply (drule_tac [!] p="-p" in b)
+  apply (simp_all)
+  apply (metis permute_minus_cancel(2))
+  apply (metis permute_minus_cancel(2))
+  done
 lemma alpha_gen_trans:
-  assumes a: "\<lbrakk>R (p \<bullet> x) y; R (q \<bullet> y) z\<rbrakk> \<Longrightarrow> R ((q + p) \<bullet> x) z"
+  assumes a: "(\<forall>c. R y c \<longrightarrow> R (p \<bullet> x) c)"
+  and b: "R (p \<bullet> x) y"
+  and c: "R (q \<bullet> y) z"
+  and d: "\<And>x y p. R x y \<Longrightarrow> R (p \<bullet> x) (p \<bullet> y)"
   shows "\<lbrakk>(bs, x) \<approx>gen R f p (cs, y); (cs, y) \<approx>gen R f q (ds, z)\<rbrakk> \<Longrightarrow> (bs, x) \<approx>gen R f (q + p) (ds, z)"
   and   "\<lbrakk>(bs, x) \<approx>res R f p (cs, y); (cs, y) \<approx>res R f q (ds, z)\<rbrakk> \<Longrightarrow> (bs, x) \<approx>res R f (q + p) (ds, z)"
   and   "\<lbrakk>(es, x) \<approx>lst R f p (gs, y); (gs, y) \<approx>lst R f q (hs, z)\<rbrakk> \<Longrightarrow> (es, x) \<approx>lst R f (q + p) (hs, z)"
-  using a 
   unfolding alphas
   unfolding fresh_star_def
-  by (simp_all add: fresh_plus_perm)
+  apply (simp_all add: fresh_plus_perm)
+  apply (metis a c d permute_minus_cancel(2))+
+  done
 
 lemma alpha_gen_eqvt:
   assumes a: "R (q \<bullet> x) y \<Longrightarrow> R (p \<bullet> (q \<bullet> x)) (p \<bullet> y)"