--- a/Quot/Nominal/Fv.thy	Mon Feb 22 18:09:44 2010 +0100
+++ b/Quot/Nominal/Fv.thy	Tue Feb 23 09:31:59 2010 +0100
@@ -295,10 +295,32 @@
 *}
 
 ML {*
-fun transp_tac induct alpha_inj term_inj distinct cases eqvt =
-  ((rtac @{thm impI} THEN' etac induct) ORELSE' rtac induct) THEN_ALL_NEW
-  (rtac allI THEN' rtac impI THEN' rotate_tac (~1) THEN'
-  eresolve_tac cases) THEN_ALL_NEW
+fun imp_elim_tac case_rules =
+  Subgoal.FOCUS (fn {concl, context, ...} =>
+    case term_of concl of
+      _ $ (_ $ asm $ _) =>
+        let
+          fun filter_fn case_rule = (
+            case Logic.strip_assums_hyp (prop_of case_rule) of
+              ((_ $ asmc) :: _) =>
+                let
+                  val thy = ProofContext.theory_of context
+                in
+                  Pattern.matches thy (asmc, asm)
+                end
+            | _ => false)
+          val matching_rules = filter filter_fn case_rules
+        in
+         (rtac impI THEN' rotate_tac (~1) THEN' eresolve_tac matching_rules) 1
+        end
+    | _ => no_tac
+  )
+*}
+
+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 @{thm conjI}) THEN_ALL_NEW
@@ -328,7 +350,7 @@
   val (reflg, (symg, transg)) = build_alpha_refl_gl alphas (x, y, z)
   fun reflp_tac' _ = reflp_tac term_induct alpha_inj 1;
   fun symp_tac' _ = symp_tac alpha_induct alpha_inj eqvt 1;
-  fun transp_tac' _ = transp_tac alpha_induct alpha_inj term_inj distinct cases eqvt 1;
+  fun transp_tac' _ = transp_tac ctxt alpha_induct alpha_inj term_inj distinct cases eqvt 1;
   val reflt = Goal.prove ctxt' [] [] reflg reflp_tac';
   val symt = Goal.prove ctxt' [] [] symg symp_tac';
   val transt = Goal.prove ctxt' [] [] transg transp_tac';
@@ -349,4 +371,29 @@
 end
 *}
 
+(*
+Tests:
+prove alpha1_reflp_aux: {* fst (build_alpha_refl_gl [@{term alpha_rtrm1}, @{term alpha_bp}] ("x","y","z")) *}
+by (tactic {* reflp_tac @{thm rtrm1_bp.induct} @{thms alpha1_inj} 1 *})
+
+prove alpha1_symp_aux: {* (fst o snd) (build_alpha_refl_gl [@{term alpha_rtrm1}, @{term alpha_bp}] ("x","y","z")) *}
+by (tactic {* symp_tac @{thm alpha_rtrm1_alpha_bp.induct} @{thms alpha1_inj} @{thms alpha1_eqvt} 1 *})
+
+prove alpha1_transp_aux: {* (snd o snd) (build_alpha_refl_gl [@{term alpha_rtrm1}, @{term alpha_bp}] ("x","y","z")) *}
+by (tactic {* transp_tac @{context} @{thm alpha_rtrm1_alpha_bp.induct} @{thms alpha1_inj} @{thms rtrm1.inject bp.inject} @{thms rtrm1.distinct bp.distinct} @{thms alpha_rtrm1.cases alpha_bp.cases} @{thms alpha1_eqvt} 1 *})
+
+lemma alpha1_equivp:
+  "equivp alpha_rtrm1"
+  "equivp alpha_bp"
+apply (tactic {*
+  (simp_tac (HOL_ss addsimps @{thms equivp_reflp_symp_transp reflp_def symp_def})
+  THEN' rtac @{thm conjI} THEN' rtac @{thm allI} THEN'
+  resolve_tac (HOLogic.conj_elims @{thm alpha1_reflp_aux})
+  THEN' rtac @{thm conjI} THEN' rtac @{thm allI} THEN' rtac @{thm allI} THEN'
+  resolve_tac (HOLogic.conj_elims @{thm alpha1_symp_aux}) THEN' rtac @{thm transp_aux}
+  THEN' resolve_tac (HOLogic.conj_elims @{thm alpha1_transp_aux})
+)
+1 *})
+done*)
+
 end