--- a/Nominal/Terms.thy	Thu Feb 25 08:40:52 2010 +0100
+++ b/Nominal/Terms.thy	Thu Feb 25 09:22:29 2010 +0100
@@ -1,5 +1,5 @@
 theory Terms
-imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "Abs" "Perm" "Fv" "Rsp" "../../Attic/Prove"
+imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "Abs" "Perm" "Fv" "Rsp" "../Attic/Prove"
 begin
 
 atom_decl name
@@ -62,12 +62,37 @@
 apply (rule alpha_bp_eq_eq)
 done
 
+ML {*
+fun build_eqvts funs perms simps induct ctxt =
+let
+  val pi = Free ("pi", @{typ perm});
+  val types = map (domain_type o fastype_of) funs;
+  val fv_indnames = Datatype_Prop.make_tnames (map body_type types);
+  val args = map Free (fv_indnames ~~ types);
+  val perm_at = Const (@{const_name permute}, @{typ "perm \<Rightarrow> atom set \<Rightarrow> atom set"})
+  fun eqvtc (fv, (arg, perm)) =
+    HOLogic.mk_eq ((perm_at $ pi $ (fv $ arg)), (fv $ (perm $ pi $ arg)))
+  val gl = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj (map eqvtc (funs ~~ (args ~~ perms))))
+  fun tac _ = (indtac induct fv_indnames THEN_ALL_NEW
+    (asm_full_simp_tac (HOL_ss addsimps 
+      (@{thm atom_eqvt} :: (Nominal_ThmDecls.get_eqvts_thms ctxt) @ simps)))) 1
+in
+  Goal.prove ctxt ("pi" :: fv_indnames) [] gl tac
+end
+*}
+
+ML {*
+build_eqvts [@{term bv1}] [@{term "permute :: perm \<Rightarrow> bp \<Rightarrow> bp"}] (@{thms bv1.simps permute_rtrm1_permute_bp.simps}) @{thm rtrm1_bp.inducts(2)} @{context}
+*}
 lemma bv1_eqvt[eqvt]:
   shows "(pi \<bullet> bv1 x) = bv1 (pi \<bullet> x)"
   apply (induct x)
   apply (simp_all add: eqvts atom_eqvt)
   done
 
+ML {*
+build_eqvts [@{term fv_rtrm1}, @{term fv_bp}] [@{term "permute :: perm \<Rightarrow> rtrm1 \<Rightarrow> rtrm1"},@{term "permute :: perm \<Rightarrow> bp \<Rightarrow> bp"}] (@{thms fv_rtrm1_fv_bp.simps permute_rtrm1_permute_bp.simps}) @{thm rtrm1_bp.induct} @{context}
+*}
 lemma fv_rtrm1_eqvt[eqvt]:
     "(pi\<bullet>fv_rtrm1 t) = fv_rtrm1 (pi\<bullet>t)"
     "(pi\<bullet>fv_bp b) = fv_bp (pi\<bullet>b)"