diff -r 4b949985cf57 -r f731e9aff866 Nominal/Fv.thy
--- a/Nominal/Fv.thy	Thu Mar 25 17:30:46 2010 +0100
+++ b/Nominal/Fv.thy	Thu Mar 25 20:12:57 2010 +0100
@@ -1150,4 +1150,56 @@
 end
 *}
 
+ML {*
+fun prove_by_alpha_induct alphas build_goal ind utac inputs ctxt =
+let
+  val tys = map (domain_type o fastype_of) alphas;
+  val names = Datatype_Prop.make_tnames tys;
+  val (namesl, ctxt') = Variable.variant_fixes names ctxt;
+  val (namesr, ctxt'') = Variable.variant_fixes names ctxt';
+  val freesl = map Free (namesl ~~ tys);
+  val freesr = map Free (namesr ~~ tys);
+  val (gls_lists, ctxt'') = fold_map (build_goal (tys ~~ (freesl ~~ freesr))) inputs ctxt'';
+  val gls = flat gls_lists;
+  fun trm_gls_map t = filter (exists_subterm (fn s => s = t)) gls;
+  val trm_gl_lists = map trm_gls_map freesl;
+  val trm_gls = map mk_conjl trm_gl_lists;
+  val pgls = map
+    (fn ((alpha, gl), (l, r)) => HOLogic.mk_imp (alpha $ l $ r, gl)) 
+    ((alphas ~~ trm_gls) ~~ (freesl ~~ freesr))
+  val gl = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj pgls);
+(*  val _ = tracing (PolyML.makestring gl); *)
+  fun tac {context,...} = (ind_tac ind THEN_ALL_NEW split_conjs THEN_ALL_NEW utac) 1
+  val th_loc = Goal.prove ctxt'' [] [] gl tac
+  val ths_loc = HOLogic.conj_elims th_loc
+  val ths = Variable.export ctxt'' ctxt ths_loc
+in
+  filter (fn x => not (prop_of x = prop_of @{thm TrueI})) ths
 end
+*}
+
+ML {*
+fun build_rsp_gl alphas fnctn ctxt =
+let
+  val typ = domain_type (fastype_of fnctn);
+  val (argl, argr) = the (AList.lookup (op=) alphas typ);
+in
+  ([HOLogic.mk_eq (fnctn $ argl, fnctn $ argr)], ctxt)
+end
+*}
+
+ML {*
+fun fvbv_rsp_tac' simps ctxt =
+  asm_full_simp_tac (HOL_basic_ss addsimps @{thms alpha_gen2}) THEN_ALL_NEW
+  asm_full_simp_tac (HOL_ss addsimps (@{thm alpha_gen} :: simps)) THEN_ALL_NEW
+  REPEAT o eresolve_tac [conjE, exE] THEN_ALL_NEW
+  asm_full_simp_tac (HOL_ss addsimps simps) THEN_ALL_NEW
+  TRY o blast_tac (claset_of ctxt)
+*}
+
+ML {*
+fun build_fvbv_rsps alphas ind simps fnctns ctxt =
+  prove_by_alpha_induct alphas build_rsp_gl ind (fvbv_rsp_tac' simps ctxt) fnctns ctxt
+*}
+
+end