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

--- a/Quot/Nominal/Terms.thy	Mon Feb 22 18:09:44 2010 +0100
+++ b/Quot/Nominal/Terms.thy	Tue Feb 23 09:31:59 2010 +0100
@@ -120,29 +120,6 @@
   (build_equivps [@{term alpha_rtrm1}, @{term alpha_bp}] @{thm rtrm1_bp.induct} @{thm alpha_rtrm1_alpha_bp.induct} @{thms rtrm1.inject bp.inject} @{thms alpha1_inj} @{thms rtrm1.distinct bp.distinct} @{thms alpha_rtrm1.cases alpha_bp.cases} @{thms alpha1_eqvt} ctxt)) ctxt)) *}
 thm alpha1_equivp
 
-(*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 @{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*)
-
 quotient_type trm1 = rtrm1 / alpha_rtrm1
   by (rule alpha1_equivp(1))
 
@@ -227,12 +204,8 @@
 lemma bp_supp: "finite (supp (bp :: bp))"
   apply (induct bp)
   apply(simp_all add: supp_def)
-  apply (fold supp_def)
-  apply (simp add: supp_at_base)
-  apply(simp add: Collect_imp_eq)
-  apply(simp add: Collect_neg_eq[symmetric])
-  apply (fold supp_def)
-  apply (simp)
+  apply(simp add: supp_at_base supp_def[symmetric])
+  apply(simp add: Collect_imp_eq Collect_neg_eq[symmetric] supp_def)
   done
 
 instance trm1 :: fs
@@ -459,24 +432,14 @@
   "a \<approx>4l b \<Longrightarrow> (pi \<bullet> a) \<approx>4l (pi \<bullet> b)"
 sorry
 
-(*
-prove alpha4_transp_aux: {* (snd o snd) (build_alpha_refl_gl [@{term alpha_rtrm4}, @{term alpha_rtrm4_list}] ("x","y","z")) *}
-apply (tactic {* 
-transp_tac @{thm rtrm4.induct} @{thms alpha4_inj} @{thms rtrm4.inject list.inject} @{thms rtrm4.distinct list.distinct} @{thms alpha_rtrm4_list.cases alpha_rtrm4.cases} @{thms alpha1_eqvt} 1 *})
 local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha4_equivp}, []),
-  (build_equivps [@{term alpha_rtrm4}, @{term alpha_rtrm4_list}] @{thm rtrm4.induct} @{thm alpha_rtrm4_alpha_rtrm4_list.induct} @{thms rtrm4.inject list.inject} @{thms alpha4_inj} @{thms rtrm4.distinct list.distinct} @{thms alpha_rtrm4_list.cases list.cases} @{thms alpha4_eqvt} ctxt)) ctxt)) *}
-*)
-
-
-
-
-lemma alpha4_equivp: "equivp alpha_rtrm4" sorry
-lemma alpha4list_equivp: "equivp alpha_rtrm4_list" sorry
+  (build_equivps [@{term alpha_rtrm4}, @{term alpha_rtrm4_list}] @{thm rtrm4.induct} @{thm alpha_rtrm4_alpha_rtrm4_list.induct} @{thms rtrm4.inject list.inject} @{thms alpha4_inj} @{thms rtrm4.distinct list.distinct} @{thms alpha_rtrm4_list.cases alpha_rtrm4.cases} @{thms alpha4_eqvt} ctxt)) ctxt)) *}
+thm alpha4_equivp
 
 quotient_type 
   qrtrm4 = rtrm4 / alpha_rtrm4 and
   qrtrm4list = "rtrm4 list" / alpha_rtrm4_list
-  by (simp_all add: alpha4_equivp alpha4list_equivp)
+  by (simp_all add: alpha4_equivp)
 
 
 datatype rtrm5 =