--- a/Nominal/Abs.thy	Tue Mar 02 11:04:49 2010 +0100
+++ b/Nominal/Abs.thy	Tue Mar 02 12:28:07 2010 +0100
@@ -75,12 +75,11 @@
   done
 
 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)"
+  fixes pi
+  assumes b: "(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)"
+  shows "(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)
   apply(erule conjE)+
   apply(rule conjI)
@@ -92,16 +91,14 @@
   done
 
 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)"
+  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)"
+  and c: "(ab, ta) \<approx>gen R f pia (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)"
+  shows "(aa, t) \<approx>gen R f (pia + pi) (ac, sa)"
   using b c apply -
   apply(simp add: alpha_gen.simps)
   apply(erule conjE)+
-  apply(erule exE)+
-  apply(erule conjE)+
-  apply(rule_tac x="pia + pi" in exI)
   apply(simp add: fresh_star_plus)
   apply(drule_tac x="- pia \<bullet> sa" in spec)
   apply(drule mp)

--- a/Nominal/Fv.thy	Tue Mar 02 11:04:49 2010 +0100
+++ b/Nominal/Fv.thy	Tue Mar 02 12:28:07 2010 +0100
@@ -303,18 +303,26 @@
 fun reflp_tac induct inj =
   rtac induct THEN_ALL_NEW
   asm_full_simp_tac (HOL_ss addsimps inj) THEN_ALL_NEW
-  TRY o REPEAT_ALL_NEW (CHANGED o rtac conjI) THEN_ALL_NEW
+(*  TRY o REPEAT_ALL_NEW (CHANGED o rtac conjI) THEN_ALL_NEW*)
   (rtac @{thm exI[of _ "0 :: perm"]} THEN'
    asm_full_simp_tac (HOL_ss addsimps
      @{thms alpha_gen fresh_star_def fresh_zero_perm permute_zero ball_triv}))
 *}
 
+lemma exi_neg: "\<exists>(pi :: perm). P pi \<Longrightarrow> (\<And>(p :: perm). P p \<Longrightarrow> Q (- p)) \<Longrightarrow> \<exists>pi. Q pi"
+apply (erule exE)
+apply (rule_tac x="-pi" in exI)
+by auto
+
 ML {*
 fun symp_tac induct inj eqvt =
-  ((rtac @{thm impI} THEN' etac induct) ORELSE' rtac induct) THEN_ALL_NEW
+  (((rtac impI THEN' etac induct) ORELSE' rtac induct) THEN_ALL_NEW
   asm_full_simp_tac (HOL_ss addsimps inj) THEN_ALL_NEW
-  TRY o REPEAT_ALL_NEW (CHANGED o rtac conjI) THEN_ALL_NEW
-  (etac @{thm alpha_gen_compose_sym} THEN' eresolve_tac eqvt)
+  (etac @{thm exi_neg} THEN' REPEAT o etac conjE THEN'
+  (TRY o REPEAT_ALL_NEW (CHANGED o rtac conjI))) THEN_ALL_NEW
+  (asm_full_simp_tac HOL_ss) THEN_ALL_NEW
+  (etac @{thm alpha_gen_compose_sym} THEN' 
+    (asm_full_simp_tac (HOL_ss addsimps (@{thm atom_eqvt} :: eqvt)))))
 *}
 
 ML {*
@@ -340,14 +348,23 @@
   )
 *}
 
+
+lemma exi_sum: "\<exists>(pi :: perm). P pi \<Longrightarrow> \<exists>(pi :: perm). Q pi \<Longrightarrow> (\<And>(p :: perm) (pi :: perm). P p \<Longrightarrow> Q pi \<Longrightarrow> R (pi + p)) \<Longrightarrow> \<exists>pi. R pi"
+apply (erule exE)+
+apply (rule_tac x="pia + pi" in exI)
+by auto
+
 ML {*
 fun transp_tac ctxt induct alpha_inj term_inj distinct cases eqvt =
   ((rtac impI THEN' etac induct) ORELSE' rtac induct) THEN_ALL_NEW
   (TRY o rtac allI THEN' imp_elim_tac cases ctxt) THEN_ALL_NEW
   (
-    asm_full_simp_tac (HOL_ss addsimps alpha_inj @ term_inj @ distinct) THEN'
-    TRY o REPEAT_ALL_NEW (CHANGED o rtac conjI) THEN_ALL_NEW
-    (etac @{thm alpha_gen_compose_trans} THEN' RANGE [atac, eresolve_tac eqvt])
+    asm_full_simp_tac (HOL_ss addsimps alpha_inj @ term_inj @ distinct)
+    THEN_ALL_NEW (etac @{thm exi_sum} THEN' RANGE [atac]) THEN_ALL_NEW
+    (REPEAT o etac conjE THEN' (TRY o REPEAT_ALL_NEW (CHANGED o rtac conjI)))
+    THEN_ALL_NEW (asm_full_simp_tac HOL_ss) THEN_ALL_NEW
+    (etac @{thm alpha_gen_compose_trans} THEN' RANGE[atac]) THEN_ALL_NEW
+    (asm_full_simp_tac (HOL_ss addsimps (@{thm atom_eqvt} :: eqvt)))
   )
 *}