--- a/Nominal/Rsp.thy	Fri Mar 26 09:23:23 2010 +0100
+++ b/Nominal/Rsp.thy	Fri Mar 26 10:07:26 2010 +0100
@@ -1,5 +1,5 @@
 theory Rsp
-imports Abs
+imports Abs Tacs
 begin
 
 ML {*
@@ -74,12 +74,8 @@
 *}
 
 ML {*
-fun ind_tac induct = (rtac impI THEN' etac induct) ORELSE' rtac induct
-*}
-
-ML {*
 fun fvbv_rsp_tac induct fvbv_simps ctxt =
-  ind_tac induct THEN_ALL_NEW
+  rel_indtac induct THEN_ALL_NEW
   (TRY o rtac @{thm TrueI}) THEN_ALL_NEW
   asm_full_simp_tac (HOL_basic_ss addsimps @{thms alpha_gen2}) THEN_ALL_NEW
   asm_full_simp_tac (HOL_ss addsimps (@{thm alpha_gen} :: fvbv_simps)) THEN_ALL_NEW
@@ -92,13 +88,12 @@
 fun sym_eqvts ctxt = map (fn x => sym OF [x]) (Nominal_ThmDecls.get_eqvts_thms ctxt)
 fun all_eqvts ctxt =
   Nominal_ThmDecls.get_eqvts_thms ctxt @ Nominal_ThmDecls.get_eqvts_raw_thms ctxt
-val split_conjs = REPEAT o etac conjE THEN' TRY o REPEAT_ALL_NEW (CHANGED o rtac conjI)
 *}
 
 ML {*
 fun constr_rsp_tac inj rsp =
   REPEAT o rtac impI THEN'
-  simp_tac (HOL_ss addsimps inj) THEN' split_conjs THEN_ALL_NEW
+  simp_tac (HOL_ss addsimps inj) THEN' split_conj_tac THEN_ALL_NEW
   (asm_simp_tac HOL_ss THEN_ALL_NEW (
    REPEAT o rtac @{thm exI[of _ "0 :: perm"]} THEN_ALL_NEW
    simp_tac (HOL_basic_ss addsimps @{thms alpha_gen2}) THEN_ALL_NEW
@@ -107,23 +102,6 @@
   ))
 *}
 
-(* Testing code
-local_setup {* snd o prove_const_rsp @{binding fv_rtrm2_rsp} [@{term rbv2}]
-  (fn _ => fv_rsp_tac @{thm alpha_rtrm2_alpha_rassign.inducts(2)} @{thms fv_rtrm2_fv_rassign.simps} 1) *}*)
-
-(*ML {*
-  val rsp_goals = map (const_rsp @{context}) [@{term rbv2}]
-  val (fixed, user_goals) = split_list (map (get_rsp_goal @{theory}) rsp_goals)
-  val fixed' = distinct (op =) (flat fixed)
-  val user_goal = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj user_goals)
-*}
-prove ug: {* user_goal *}
-ML_prf {*
-val induct = @{thm alpha_rtrm2_alpha_rassign.inducts(2)}
-val fv_simps = @{thms rbv2.simps}
-*} 
-*)
-
 ML {*
 fun perm_arg arg =
 let
@@ -150,13 +128,13 @@
 
 ML {*
 fun alpha_eqvt_tac induct simps ctxt =
-  ind_tac induct THEN_ALL_NEW
+  rel_indtac induct THEN_ALL_NEW
   simp_tac ((mk_minimal_ss ctxt) addsimps simps) THEN_ALL_NEW
-  REPEAT o etac @{thm exi[of _ _ "p"]} THEN' split_conjs THEN_ALL_NEW
+  REPEAT o etac @{thm exi[of _ _ "p"]} THEN' split_conj_tac THEN_ALL_NEW
   asm_full_simp_tac (HOL_ss addsimps (all_eqvts ctxt @ simps)) THEN_ALL_NEW
   asm_full_simp_tac (HOL_ss addsimps 
     @{thms supp_eqvt[symmetric] inter_eqvt[symmetric] empty_eqvt alpha_gen}) THEN_ALL_NEW
-  (split_conjs THEN_ALL_NEW TRY o resolve_tac
+  (split_conj_tac THEN_ALL_NEW TRY o resolve_tac
     @{thms fresh_star_permute_iff[of "- p", THEN iffD1] permute_eq_iff[of "- p", THEN iffD1]})
   THEN_ALL_NEW
   asm_full_simp_tac (HOL_ss addsimps (@{thms split_conv permute_minus_cancel permute_plus permute_eqvt[symmetric]} @ all_eqvts ctxt @ simps))
@@ -231,6 +209,8 @@
 end
 *}
 
+(** alpha_bn_rsp **)
+
 lemma equivp_rspl:
   "equivp r \<Longrightarrow> r a b \<Longrightarrow> r a c = r b c"
   unfolding equivp_reflp_symp_transp symp_def transp_def 
@@ -242,39 +222,38 @@
   by blast
 
 ML {*
-fun prove_alpha_bn_rsp alphas inducts exhausts inj_dis equivps ctxt (alpha_bn, n) =
+fun alpha_bn_rsp_tac simps res exhausts a ctxt =
+  rtac allI THEN_ALL_NEW
+  case_rules_tac ctxt a exhausts THEN_ALL_NEW
+  asm_full_simp_tac (HOL_ss addsimps simps) THEN_ALL_NEW
+  TRY o REPEAT_ALL_NEW (rtac @{thm arg_cong2[of _ _ _ _ "op \<and>"]}) THEN_ALL_NEW
+  TRY o eresolve_tac res THEN_ALL_NEW
+  asm_full_simp_tac (HOL_ss addsimps simps);
+*}
+
+
+ML {*
+fun build_alpha_bn_rsp_gl a alphas alpha_bn ctxt =
 let
-  val alpha = nth alphas n;
-  val ty = domain_type (fastype_of alpha);
-  val ([x, y, a], ctxt') = Variable.variant_fixes ["x","y","a"] ctxt;
-  val [l, r] = map (fn x => (Free (x, ty))) [x, y]
-  val lhs = HOLogic.mk_Trueprop (alpha $ l $ r)
-  val g1 =
-    Logic.mk_implies (lhs,
-      HOLogic.mk_Trueprop (HOLogic.mk_all (a, ty,
-        HOLogic.mk_eq (alpha_bn $ l $ Bound 0, alpha_bn $ r $ Bound 0))));
-  val g2 =
-    Logic.mk_implies (lhs,
-      HOLogic.mk_Trueprop (HOLogic.mk_all (a, ty,
-        HOLogic.mk_eq (alpha_bn $ Bound 0 $ l, alpha_bn $ Bound 0 $ r))));
-  val resl = map (fn x => @{thm equivp_rspl} OF [x]) equivps;
-  val resr = map (fn x => @{thm equivp_rspr} OF [x]) equivps;
-  fun tac {context, ...} = (
-    etac (nth inducts n) THEN_ALL_NEW
-    (TRY o rtac @{thm TrueI}) THEN_ALL_NEW rtac allI THEN_ALL_NEW
-    split_conjs THEN_ALL_NEW
-    InductTacs.case_rule_tac context a (nth exhausts n) THEN_ALL_NEW
-    asm_full_simp_tac (HOL_ss addsimps inj_dis) THEN_ALL_NEW
-    TRY o REPEAT_ALL_NEW (rtac @{thm arg_cong2[of _ _ _ _ "op \<and>"]}) THEN_ALL_NEW
-    TRY o eresolve_tac (resl @ resr) THEN_ALL_NEW
-    asm_full_simp_tac (HOL_ss addsimps inj_dis)
-  ) 1;
-  val t1 = Goal.prove ctxt [] [] g1 tac;
-  val t2 = Goal.prove ctxt [] [] g2 tac;
+  val ty = domain_type (fastype_of alpha_bn);
+  val (l, r) = the (AList.lookup (op=) alphas ty);
 in
-  Variable.export ctxt' ctxt [t1, t2]
+  ([HOLogic.mk_all (a, ty, HOLogic.mk_eq (alpha_bn $ l $ Bound 0, alpha_bn $ r $ Bound 0)),
+    HOLogic.mk_all (a, ty, HOLogic.mk_eq (alpha_bn $ Bound 0 $ l, alpha_bn $ Bound 0 $ r))], ctxt)
 end
 *}
 
+ML {*
+fun prove_alpha_bn_rsp alphas ind simps equivps exhausts alpha_bns ctxt =
+let
+  val ([a], ctxt') = Variable.variant_fixes ["a"] ctxt;
+  val resl = map (fn x => @{thm equivp_rspl} OF [x]) equivps;
+  val resr = map (fn x => @{thm equivp_rspr} OF [x]) equivps;
+  val ths_loc = prove_by_rel_induct alphas (build_alpha_bn_rsp_gl a) ind
+    (alpha_bn_rsp_tac simps (resl @ resr) exhausts a) alpha_bns ctxt
+in
+  Variable.export ctxt' ctxt ths_loc
+end
+*}
 
 end