--- a/Nominal/Rsp.thy	Thu Feb 25 12:15:11 2010 +0100
+++ b/Nominal/Rsp.thy	Thu Feb 25 12:30:50 2010 +0100
@@ -115,4 +115,54 @@
 *} 
 *)
 
+ML {*
+fun build_eqvts bind funs perms simps induct ctxt =
+let
+  val pi = Free ("p", @{typ perm});
+  val types = map (domain_type o fastype_of) funs;
+  val indnames = Name.variant_list ["p"] (Datatype_Prop.make_tnames (map body_type types));
+  val args = map Free (indnames ~~ types);
+  val perm_at = @{term "permute :: perm \<Rightarrow> atom set \<Rightarrow> atom set"}
+  fun eqvtc (fnctn, (arg, perm)) =
+    HOLogic.mk_eq ((perm_at $ pi $ (fnctn $ arg)), (fnctn $ (perm $ pi $ arg)))
+  val gl = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj (map eqvtc (funs ~~ (args ~~ perms))))
+  fun tac _ = (Datatype_Aux.indtac induct indnames THEN_ALL_NEW
+    (asm_full_simp_tac (HOL_ss addsimps
+      (@{thm atom_eqvt} :: (Nominal_ThmDecls.get_eqvts_thms ctxt) @ simps)))) 1
+  val thm = Goal.prove ctxt ("p" :: indnames) [] gl tac
+  val thms = HOLogic.conj_elims thm
+in
+  Local_Theory.note ((bind, [Attrib.internal (fn _ => Nominal_ThmDecls.eqvt_add)]), thms) ctxt
 end
+*}
+
+
+ML {*
+fun build_alpha_eqvts funs perms simps induct ctxt =
+let
+  val pi = Free ("p", @{typ perm});
+  val types = map (domain_type o fastype_of) funs;
+  val indnames = Name.variant_list ["p"] (Datatype_Prop.make_tnames (map body_type types));
+  val indnames2 = Name.variant_list ("p" :: indnames) (Datatype_Prop.make_tnames (map body_type types));
+  val args = map Free (indnames ~~ types);
+  val args2 = map Free (indnames2 ~~ types);
+  fun eqvtc ((alpha, perm), (arg, arg2)) =
+    HOLogic.mk_imp (alpha $ arg $ arg2,
+      (alpha $ (perm $ pi $ arg) $ (perm $ pi $ arg2)))
+  val gl = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj (map eqvtc ((funs ~~ perms) ~~ (args ~~ args2))))
+  fun tac _ = (((rtac impI THEN' etac induct) ORELSE' rtac induct) THEN_ALL_NEW
+    (asm_full_simp_tac (HOL_ss addsimps 
+      (@{thm atom_eqvt} :: (Nominal_ThmDecls.get_eqvts_thms ctxt) @ simps)))
+    THEN_ALL_NEW (TRY o REPEAT_ALL_NEW (CHANGED o rtac conjI) THEN_ALL_NEW
+      (etac @{thm alpha_gen_compose_eqvt})) THEN_ALL_NEW
+    (asm_full_simp_tac (HOL_ss addsimps 
+      (@{thm atom_eqvt} :: (Nominal_ThmDecls.get_eqvts_thms ctxt) @ simps)))
+) 1
+  val thm = Goal.prove ctxt ("p" :: indnames @ indnames2) [] gl tac
+in
+  map (fn x => mp OF [x]) (HOLogic.conj_elims thm)
+end
+*}
+
+
+end