--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Nominal/Unused.thy	Wed May 12 16:39:10 2010 +0200
@@ -0,0 +1,43 @@
+lemma exi: "\<exists>(pi :: perm). P pi \<Longrightarrow> (\<And>(p :: perm). P p \<Longrightarrow> Q (pi \<bullet> p)) \<Longrightarrow> \<exists>pi. Q pi"
+apply (erule exE)
+apply (rule_tac x="pi \<bullet> pia" in exI)
+by auto
+
+ML {*
+fun alpha_eqvt_tac induct simps ctxt =
+  rtac induct THEN_ALL_NEW
+  simp_tac (HOL_basic_ss addsimps simps) THEN_ALL_NEW split_conj_tac THEN_ALL_NEW
+  REPEAT o etac @{thm exi[of _ _ "p"]} THEN' split_conj_tac THEN_ALL_NEW
+  asm_full_simp_tac (HOL_ss addsimps (all_eqvts ctxt @ simps)) THEN_ALL_NEW
+  asm_full_simp_tac (HOL_ss addsimps
+    @{thms supp_eqvt[symmetric] inter_eqvt[symmetric] empty_eqvt alphas prod_rel.simps prod_fv.simps}) THEN_ALL_NEW
+  (split_conj_tac THEN_ALL_NEW TRY o resolve_tac
+    @{thms fresh_star_permute_iff[of "- p", THEN iffD1] permute_eq_iff[of "- p", THEN iffD1]})
+  THEN_ALL_NEW
+  asm_full_simp_tac (HOL_ss addsimps (@{thms split_conv permute_minus_cancel permute_plus permute_eqvt[symmetric]} @ all_eqvts ctxt @ simps))
+*}
+
+ML {*
+fun build_alpha_eqvt alpha names =
+let
+  val pi = Free ("p", @{typ perm});
+  val (tys, _) = strip_type (fastype_of alpha)
+  val indnames = Name.variant_list names (Datatype_Prop.make_tnames (map body_type tys));
+  val args = map Free (indnames ~~ tys);
+  val perm_args = map (fn x => mk_perm pi x) args
+in
+  (HOLogic.mk_imp (list_comb (alpha, args), list_comb (alpha, perm_args)), indnames @ names)
+end
+*}
+
+ML {*
+fun build_alpha_eqvts funs tac ctxt =
+let
+  val (gls, names) = fold_map build_alpha_eqvt funs ["p"]
+  val gl = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj gls)
+  val thm = Goal.prove ctxt names [] gl tac
+in
+  map (fn x => mp OF [x]) (HOLogic.conj_elims thm)
+end
+*}
+