343 ML {*

   343 

   344 fun build_eqvt_gl pi frees fnctn ctxt =

   344 

   345 let

   345 end

   346   val typ = domain_type (fastype_of fnctn);

   347   val arg = the (AList.lookup (op=) frees typ);

   348 in

   349   ([HOLogic.mk_eq (mk_perm pi (fnctn $ arg), fnctn $ (mk_perm pi arg))], ctxt)

   350 end

   351 *}

   352 

   353 ML {*

   354 fun prove_eqvt tys ind simps funs ctxt =

   355 let

   356   val ([pi], ctxt') = Variable.variant_fixes ["p"] ctxt;

   357   val pi = Free (pi, @{typ perm});

   358   val tac = asm_full_simp_tac (HOL_ss addsimps (@{thms atom_eqvt permute_list.simps} @ simps @ all_eqvts ctxt'))

   359   val ths_loc = prove_by_induct tys (build_eqvt_gl pi) ind tac funs ctxt'

   360   val ths = Variable.export ctxt' ctxt ths_loc

   361   val add_eqvt = Attrib.internal (fn _ => Nominal_ThmDecls.eqvt_add)

   362 in

   363   (ths, snd (Local_Theory.note ((Binding.empty, [add_eqvt]), ths) ctxt))

   364 end

   365 *}

   366 

   367 end