--- a/Nominal/Rsp.thy	Mon Mar 22 10:15:46 2010 +0100
+++ b/Nominal/Rsp.thy	Mon Mar 22 14:07:07 2010 +0100
@@ -73,20 +73,21 @@
 end
 *}
 
-
+ML {*
+fun ind_tac induct = (rtac impI THEN' etac induct) ORELSE' rtac induct
+*}
 
 ML {*
-fun fvbv_rsp_tac induct fvbv_simps =
-  ((((rtac impI THEN' etac induct) ORELSE' rtac induct) THEN_ALL_NEW
-  (TRY o rtac @{thm TrueI})) THEN_ALL_NEW
-  asm_full_simp_tac
-  (HOL_ss addsimps (@{thm alpha_gen} :: fvbv_simps))
-  THEN_ALL_NEW (REPEAT o eresolve_tac [conjE, exE] THEN'
-  asm_full_simp_tac
-  (HOL_ss addsimps (@{thm alpha_gen} :: fvbv_simps))))
+fun fvbv_rsp_tac induct fvbv_simps ctxt =
+  ind_tac 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
+  REPEAT o eresolve_tac [conjE, exE] THEN_ALL_NEW
+  asm_full_simp_tac (HOL_ss addsimps fvbv_simps) THEN_ALL_NEW
+  TRY o blast_tac (claset_of ctxt)
 *}
 
-
 ML {*
 fun sym_eqvts ctxt = map (fn x => sym OF [x]) (Nominal_ThmDecls.get_eqvts_thms ctxt)
 fun all_eqvts ctxt =
@@ -124,10 +125,6 @@
 *)
 
 ML {*
-fun ind_tac induct = (rtac impI THEN' etac induct) ORELSE' rtac induct
-*}
-
-ML {*
 fun build_eqvts_tac induct simps ctxt inds _ = (Datatype_Aux.indtac induct inds THEN_ALL_NEW
     (asm_full_simp_tac (HOL_ss addsimps
       (@{thm atom_eqvt} :: (Nominal_ThmDecls.get_eqvts_thms ctxt) @ (Nominal_ThmDecls.get_eqvts_raw_thms ctxt) @ simps)))) 1
@@ -219,4 +216,48 @@
   build_eqvts Binding.empty [t] (build_eqvts_tac (nth inducts n) simps ctxt) ctxt
 *}
 
+ML {*
+fun prove_fv_rsp fv_alphas_lst all_alphas tac ctxt =
+let
+  val (fvs_alphas, ls) = split_list fv_alphas_lst;
+  val (fv_ts, alpha_ts) = split_list fvs_alphas;
+  val tys = map (domain_type o fastype_of) alpha_ts;
+  val names = Datatype_Prop.make_tnames tys;
+  val names2 = Name.variant_list names names;
+  val args = map Free (names ~~ tys);
+  val args2 = map Free (names2 ~~ tys);
+  fun mk_fv_rsp arg arg2 (fv, alpha) = HOLogic.mk_eq ((fv $ arg), (fv $ arg2));
+  fun fv_rsp_arg (((fv, alpha), (arg, arg2)), l) =
+    HOLogic.mk_imp (
+     (alpha $ arg $ arg2),
+     (foldr1 HOLogic.mk_conj
+       (HOLogic.mk_eq (fv $ arg, fv $ arg2) ::
+       (map (mk_fv_rsp arg arg2) l))));
+  val nobn_eqs = map fv_rsp_arg (((fv_ts ~~ alpha_ts) ~~ (args ~~ args2)) ~~ ls);
+  fun mk_fv_rsp_bn arg arg2 (fv, alpha) =
+    HOLogic.mk_imp (
+      (alpha $ arg $ arg2),
+      HOLogic.mk_eq ((fv $ arg), (fv $ arg2)));
+  fun fv_rsp_arg_bn ((arg, arg2), l) =
+    map (mk_fv_rsp_bn arg arg2) l;
+  val bn_eqs = flat (map fv_rsp_arg_bn ((args ~~ args2) ~~ ls));
+  val (_, add_alphas) = chop (length (nobn_eqs @ bn_eqs)) all_alphas;
+  val atys = map (domain_type o fastype_of) add_alphas;
+  val anames = Name.variant_list (names @ names2) (Datatype_Prop.make_tnames atys);
+  val aargs = map Free (anames ~~ atys);
+  val aeqs = map2 (fn alpha => fn arg => HOLogic.mk_imp (alpha $ arg $ arg, @{term True}))
+    add_alphas aargs;
+  val eq = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj (nobn_eqs @ bn_eqs @ aeqs));
+  val th = Goal.prove ctxt (names @ names2) [] eq tac;
+  val ths = HOLogic.conj_elims th;
+  val (ths_nobn, ths_bn) = chop (length ls) ths;
+  fun project (th, l) =
+    Project_Rule.projects ctxt (1 upto (length l + 1)) (hd (Project_Rule.projections ctxt th))
+  val ths_nobn_pr = map project (ths_nobn ~~ ls);
+in
+  (flat ths_nobn_pr @ ths_bn)
 end
+*}
+
+
+end