--- a/Nominal/Fv.thy	Thu Mar 25 15:06:58 2010 +0100
+++ b/Nominal/Fv.thy	Thu Mar 25 17:30:46 2010 +0100
@@ -1099,4 +1099,55 @@
   simp_tac (HOL_ss addsimps @{thms Collect_const finite.emptyI})
 *}
 
+(* Given function for buildng a goal for an input, prepares a
+   one common goals for all the inputs and proves it by induction
+   together *)
+ML {*
+fun prove_by_induct tys build_goal ind utac inputs ctxt =
+let
+  val names = Datatype_Prop.make_tnames tys;
+  val (names', ctxt') = Variable.variant_fixes names ctxt;
+  val frees = map Free (names' ~~ tys);
+  val (gls_lists, ctxt'') = fold_map (build_goal (tys ~~ frees)) 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 frees;
+  val trm_gl_insts = map2 (fn n => fn l => [NONE, if l = [] then NONE else SOME n]) names' trm_gl_lists
+  val trm_gls = map mk_conjl trm_gl_lists;
+  val gl = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj trm_gls);
+  fun tac {context,...} = ((fn _ => print_tac (PolyML.makestring names')) THEN'
+    InductTacs.induct_rules_tac context [(flat trm_gl_insts)] [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_eqvt_gl pi frees fnctn ctxt =
+let
+  val typ = domain_type (fastype_of fnctn);
+  val arg = the (AList.lookup (op=) frees typ);
+in
+  ([HOLogic.mk_eq ((perm_at $ pi $ (fnctn $ arg)), (fnctn $ (perm_arg arg $ pi $ arg)))], ctxt)
+end
+*}
+
+ML {*
+fun prove_eqvt tys ind simps funs ctxt =
+let
+  val ([pi], ctxt') = Variable.variant_fixes ["p"] ctxt;
+  val pi = Free (pi, @{typ perm});
+  val tac = asm_full_simp_tac (HOL_ss addsimps (@{thm atom_eqvt} :: simps @ all_eqvts ctxt'))
+  val ths_loc = prove_by_induct tys (build_eqvt_gl pi) ind tac funs ctxt'
+  val ths = Variable.export ctxt' ctxt ths_loc
+  val add_eqvt = Attrib.internal (fn _ => Nominal_ThmDecls.eqvt_add)
+in
+  (ths, snd (Local_Theory.note ((Binding.empty, [add_eqvt]), ths) ctxt))
+end
+*}
+
+end