--- 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)"

--- a/Nominal/Manual/Term5.thy	Fri Mar 26 17:22:17 2010 +0100
+++ b/Nominal/Manual/Term5.thy	Fri Mar 26 22:22:41 2010 +0100
@@ -1,5 +1,5 @@
 theory Term5
-imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "Abs" "Perm" "Fv" "Rsp" "../Attic/Prove"
+imports "../Nominal2_Atoms" "../Nominal2_Eqvt" "../Nominal2_Supp" "../Abs" "../Perm" "../Fv" "../Rsp"
 begin
 
 atom_decl name
@@ -23,7 +23,7 @@
 print_theorems
 
 local_setup {* snd o define_fv_alpha (Datatype.the_info @{theory} "Term5.rtrm5")
-  [[[], [], [(SOME (@{term rbv5}, true), 0, 1)]], [[], []]] [(@{term rbv5}, 1, [[], [0, 2]])] *}
+  [[[], [], [(SOME (@{term rbv5}, true), 0, 1)]], [[], []]] [(@{term rbv5}, 1, [[], [(0,NONE), (2,SOME @{term rbv5})]])] *}
 print_theorems
 
 notation
@@ -31,7 +31,7 @@
   alpha_rlts ("_ \<approx>l _" [100, 100] 100)
 thm alpha_rtrm5_alpha_rlts_alpha_rbv5.intros
 
-local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha5_inj}, []), (build_alpha_inj @{thms alpha_rtrm5_alpha_rlts_alpha_rbv5.intros} @{thms rtrm5.distinct rtrm5.inject rlts.distinct rlts.inject} @{thms alpha_rtrm5.cases alpha_rlts.cases alpha_rbv5.cases} ctxt)) ctxt)) *}
+local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha5_inj}, []), (build_rel_inj @{thms alpha_rtrm5_alpha_rlts_alpha_rbv5.intros} @{thms rtrm5.distinct rtrm5.inject rlts.distinct rlts.inject} @{thms alpha_rtrm5.cases alpha_rlts.cases alpha_rbv5.cases} ctxt)) ctxt)) *}
 thm alpha5_inj
 
 lemma rbv5_eqvt[eqvt]:
@@ -71,7 +71,17 @@
 "(a \<approx>5 b \<longrightarrow> b \<approx>5 a) \<and>
 (x \<approx>l y \<longrightarrow> y \<approx>l x) \<and>
 (alpha_rbv5 x y \<longrightarrow> alpha_rbv5 y x)"
-apply (tactic {* symp_tac @{thm alpha_rtrm5_alpha_rlts_alpha_rbv5.induct} @{thms alpha5_inj} @{thms alpha5_eqvt} @{context} 1 *})
+apply (rule alpha_rtrm5_alpha_rlts_alpha_rbv5.induct)
+apply (simp_all add: alpha5_inj)
+apply (erule exE)
+apply (rule_tac x="-pi" in exI)
+apply (rule alpha_gen_sym)
+apply (simp_all add: alphas)
+apply (case_tac x)
+apply (case_tac y)
+apply (simp add: alpha5_eqvt)
+apply clarify
+apply simp
 done
 
 lemma alpha5_symp1:

--- a/Nominal/Manual/Term5n.thy	Fri Mar 26 17:22:17 2010 +0100
+++ b/Nominal/Manual/Term5n.thy	Fri Mar 26 22:22:41 2010 +0100
@@ -1,5 +1,5 @@
 theory Term5
-imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "Abs" "Perm" "Fv" "Rsp" "../Attic/Prove"
+imports "../Nominal2_Atoms" "../Nominal2_Eqvt" "../Nominal2_Supp" "../Abs" "../Perm" "../Fv" "../Rsp"
 begin
 
 atom_decl name
@@ -23,7 +23,7 @@
 print_theorems
 
 local_setup {* snd o define_fv_alpha (Datatype.the_info @{theory} "Term5.rtrm5")
-  [[[], [], [(SOME (@{term rbv5}, false), 0, 1)]], [[], []]] [(@{term rbv5}, 1, [[], [0, 2]])] *}
+  [[[], [], [(SOME (@{term rbv5}, false), 0, 1)]], [[], []]] [(@{term rbv5}, 1, [[], [(0,NONE), (2,SOME @{term rbv5})]])] *}
 print_theorems
 
 notation
@@ -31,7 +31,7 @@
   alpha_rlts ("_ \<approx>l _" [100, 100] 100)
 thm alpha_rtrm5_alpha_rlts_alpha_rbv5.intros
 
-local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha5_inj}, []), (build_alpha_inj @{thms alpha_rtrm5_alpha_rlts_alpha_rbv5.intros} @{thms rtrm5.distinct rtrm5.inject rlts.distinct rlts.inject} @{thms alpha_rtrm5.cases alpha_rlts.cases alpha_rbv5.cases} ctxt)) ctxt)) *}
+local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha5_inj}, []), (build_rel_inj @{thms alpha_rtrm5_alpha_rlts_alpha_rbv5.intros} @{thms rtrm5.distinct rtrm5.inject rlts.distinct rlts.inject} @{thms alpha_rtrm5.cases alpha_rlts.cases alpha_rbv5.cases} ctxt)) ctxt)) *}
 thm alpha5_inj
 
 lemma rbv5_eqvt[eqvt]:
@@ -65,13 +65,45 @@
 "(a \<approx>5 b \<longrightarrow> b \<approx>5 a) \<and>
 (x \<approx>l y \<longrightarrow> y \<approx>l x) \<and>
 (alpha_rbv5 x y \<longrightarrow> alpha_rbv5 y x)"
-sorry
+apply (rule alpha_rtrm5_alpha_rlts_alpha_rbv5.induct)
+apply (simp_all add: alpha5_inj)
+apply (erule conjE)+
+apply (erule exE)
+apply (rule_tac x="-pi" in exI)
+apply (rule alpha_gen_sym)
+apply (simp add: alphas)
+apply (simp add: alpha5_eqvt)
+apply (simp add: alphas)
+apply clarify
+apply simp
+done
 
 lemma alpha5_transp:
 "(a \<approx>5 b \<longrightarrow> (\<forall>c. b \<approx>5 c \<longrightarrow> a \<approx>5 c)) \<and>
 (x \<approx>l y \<longrightarrow> (\<forall>z. y \<approx>l z \<longrightarrow> x \<approx>l z)) \<and>
 (alpha_rbv5 k l \<longrightarrow> (\<forall>m. alpha_rbv5 l m \<longrightarrow> alpha_rbv5 k m))"
-sorry
+apply (rule alpha_rtrm5_alpha_rlts_alpha_rbv5.induct)
+apply (rule_tac [!] allI)
+apply (simp_all add: alpha5_inj)
+apply (tactic {* (imp_elim_tac @{thms alpha_rtrm5.cases alpha_rlts.cases alpha_rbv5.cases} @{context}) 1 *})
+apply (simp_all add: alpha5_inj)
+defer
+apply (tactic {* (imp_elim_tac @{thms alpha_rtrm5.cases alpha_rlts.cases alpha_rbv5.cases} @{context}) 1 *})
+apply (simp_all add: alpha5_inj)
+apply (tactic {* (imp_elim_tac @{thms alpha_rtrm5.cases alpha_rlts.cases alpha_rbv5.cases} @{context}) 1 *})
+apply (simp_all add: alpha5_inj)
+apply (tactic {* (imp_elim_tac @{thms alpha_rtrm5.cases alpha_rlts.cases alpha_rbv5.cases} @{context}) 1 *})
+apply (simp_all add: alpha5_inj)
+apply (erule conjE)+
+apply (erule exE)+
+apply (rule_tac x="pi + pia" in exI)
+apply (rule alpha_gen_trans)
+prefer 6
+apply assumption
+apply (simp_all add: alphas alpha5_eqvt)
+apply (clarify)
+apply simp
+done
 
 lemma alpha5_equivp:
   "equivp alpha_rtrm5"