87 *}

    88 

    89 

    90 lemma exi: "\<exists>(pi :: perm). P pi \<Longrightarrow> (\<And>(p :: perm). P p \<Longrightarrow> Q (pi \<bullet> p)) \<Longrightarrow> \<exists>pi. Q pi"

    91 apply (erule exE)

    92 apply (rule_tac x="pi \<bullet> pia" in exI)

    93 by auto

    94 

    95 

    96 ML {*

    97 fun alpha_eqvt_tac induct simps ctxt =

    98   rtac induct THEN_ALL_NEW

    99   simp_tac (HOL_basic_ss addsimps simps) THEN_ALL_NEW split_conj_tac THEN_ALL_NEW

   100   REPEAT o etac @{thm exi[of _ _ "p"]} THEN' split_conj_tac THEN_ALL_NEW

   101   asm_full_simp_tac (HOL_ss addsimps (all_eqvts ctxt @ simps)) THEN_ALL_NEW

   102   asm_full_simp_tac (HOL_ss addsimps 

   103     @{thms supp_eqvt[symmetric] inter_eqvt[symmetric] empty_eqvt alphas prod_rel.simps prod_fv.simps}) THEN_ALL_NEW

   104   (split_conj_tac THEN_ALL_NEW TRY o resolve_tac

   105     @{thms fresh_star_permute_iff[of "- p", THEN iffD1] permute_eq_iff[of "- p", THEN iffD1]})

   106   THEN_ALL_NEW

   107   asm_full_simp_tac (HOL_ss addsimps (@{thms split_conv permute_minus_cancel permute_plus permute_eqvt[symmetric]} @ all_eqvts ctxt @ simps))

   108 *}

   109 

   110 ML {*

   111 fun build_alpha_eqvt alpha names =

   112 let

   113   val pi = Free ("p", @{typ perm});

   114   val (tys, _) = strip_type (fastype_of alpha)

   115   val indnames = Name.variant_list names (Datatype_Prop.make_tnames (map body_type tys));

   116   val args = map Free (indnames ~~ tys);

   117   val perm_args = map (fn x => mk_perm pi x) args

   118 in

   119   (HOLogic.mk_imp (list_comb (alpha, args), list_comb (alpha, perm_args)), indnames @ names)

   120 end

   121 *}

   122 

   123 ML {*

   124 fun build_alpha_eqvts funs tac ctxt =

   125 let

   126   val (gls, names) = fold_map build_alpha_eqvt funs ["p"]

   127   val gl = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj gls)

   128   val thm = Goal.prove ctxt names [] gl tac

   129 in

   130   map (fn x => mp OF [x]) (HOLogic.conj_elims thm)

   131 end