--- a/Nominal/nominal_dt_rawfuns.ML	Mon May 31 19:57:29 2010 +0200
+++ b/Nominal/nominal_dt_rawfuns.ML	Tue Jun 01 15:01:05 2010 +0200
@@ -25,7 +25,10 @@
   val listify: Proof.context -> term -> term
 
   val define_raw_fvs: Datatype_Aux.descr -> (string * sort) list -> bn_info ->
-    bclause list list list -> thm list -> Proof.context -> term list * term list * thm list * local_theory
+    bclause list list list -> thm list -> Proof.context -> 
+    term list * term list * thm list * thm list * local_theory
+ 
+  val raw_prove_eqvt: term list -> thm list -> thm list -> Proof.context -> thm list
 end
 
 
@@ -228,15 +231,52 @@
 
   val (info, lthy'') = prove_termination (Local_Theory.restore lthy')
 
-  val {fs, simps, ...} = info;
+  val {fs, simps, inducts, ...} = info;
 
   val morphism = ProofContext.export_morphism lthy'' lthy
   val fs_exp = map (Morphism.term morphism) fs
 
   val (fv_frees_exp, fv_bns_exp) = chop (length fv_frees) fs_exp
-  val simps_exp = Morphism.fact morphism (the simps)
+  val simps_exp = map (Morphism.thm morphism) (the simps)
+  val fv_bns_inducts_exp = map (Morphism.thm morphism) (the inducts)
+in
+  (fv_frees_exp, fv_bns_exp, simps_exp, fv_bns_inducts_exp, lthy'')
+end
+
+
+(** equivarance proofs **)
+
+fun mk_eqvt_goal pi const arg =
+let
+  val lhs = mk_perm pi (const $ arg)
+  val rhs = const $ (mk_perm pi arg)  
 in
-  (fv_frees_exp, fv_bns_exp, simps_exp, lthy'')
+  HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))
+end
+
+fun raw_prove_eqvt consts ind_thms simps ctxt =
+let 
+  val ([p], ctxt') = Variable.variant_fixes ["p"] ctxt
+  val p = Free (p, @{typ perm})
+  val arg_tys = 
+    consts
+    |> map fastype_of
+    |> map domain_type 
+  val (arg_names, ctxt'') = Variable.variant_fixes (replicate (length arg_tys) "") ctxt'
+  val args = map Free (arg_names ~~ arg_tys)
+  val goals = map2 (mk_eqvt_goal p) consts args
+  val insts = map (single o SOME) arg_names
+  val const_names = map (fst o dest_Const) consts
+  fun tac ctxt = 
+    Object_Logic.full_atomize_tac
+    THEN' InductTacs.induct_rules_tac ctxt insts ind_thms 
+    THEN_ALL_NEW   
+      (asm_full_simp_tac (HOL_basic_ss addsimps simps)
+       THEN' Nominal_Permeq.eqvt_tac ctxt simps const_names
+       THEN' asm_simp_tac HOL_basic_ss)
+in
+  Goal.prove_multi ctxt' [] [] goals (fn {context, ...} => (HEADGOAL (tac context)))
+  |> ProofContext.export ctxt'' ctxt
 end
 
 end (* structure *)