--- a/Nominal/NewFv.thy	Fri Apr 30 13:57:59 2010 +0200
+++ b/Nominal/NewFv.thy	Fri Apr 30 14:48:13 2010 +0200
@@ -271,17 +271,20 @@
     Function.prove_termination NONE
       (Lexicographic_Order.lexicographic_order_tac true lthy) lthy
 
-  val (info, lthy') = Function.add_function all_fv_names all_fv_eqs
+  val (_, lthy') = Function.add_function all_fv_names all_fv_eqs
     Function_Common.default_config pat_completeness_auto lthy
 
-  val lthy'' = prove_termination (Local_Theory.restore lthy')
+  val (info, lthy'') = prove_termination (Local_Theory.restore lthy')
+
+  val {fs, simps, ...} = info;
 
   val morphism = ProofContext.export_morphism lthy'' lthy
-  val fv_frees_exp = map (Morphism.term morphism) fv_frees
-  val fv_bns_exp = map (Morphism.term morphism) fv_bns
+  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)
 in
-  ((fv_frees_exp, fv_bns_exp), @{thms refl}, lthy'')
+  ((fv_frees_exp, fv_bns_exp), simps_exp, lthy'')
 end
 *}
 

--- a/Nominal/NewParser.thy	Fri Apr 30 13:57:59 2010 +0200
+++ b/Nominal/NewParser.thy	Fri Apr 30 14:48:13 2010 +0200
@@ -2,7 +2,7 @@
 imports "../Nominal-General/Nominal2_Base" 
         "../Nominal-General/Nominal2_Eqvt" 
         "../Nominal-General/Nominal2_Supp" 
-        "Perm" "NewFv" "NewAlpha"
+        "Perm" "NewFv" "NewAlpha" "Tacs" "Equivp"
 begin
 
 section{* Interface for nominal_datatype *}
@@ -266,6 +266,8 @@
 
   val dtinfo = Datatype.the_info (ProofContext.theory_of lthy1) (hd raw_dt_names);
   val {descr, sorts, ...} = dtinfo;
+  fun nth_dtyp i = typ_of_dtyp descr sorts (DtRec i);
+  val raw_tys = map (fn (i, _) => nth_dtyp i) descr;
 
   val all_full_tnames = map (fn (_, (n, _, _)) => n) descr;
   val dtinfos = map (Datatype.the_info (ProofContext.theory_of lthy1)) all_full_tnames;
@@ -283,16 +285,29 @@
   fun export_fun f (t, l) = (f t, map (map (apsnd (Option.map f))) l);
   val raw_bns_exp = map (apsnd (map (export_fun (Morphism.term morphism_2_0)))) raw_bns;
   val bn_funs_decls = flat (map (fn (ith, l) => map (fn (bn, data) => (bn, ith, data)) l) raw_bns_exp);
+  val raw_bn_eqs = ProofContext.export lthy2 lthy raw_bn_eqs_loc
   val thy = Local_Theory.exit_global lthy2;
   val lthy3 = Theory_Target.init NONE thy;
+  val raw_bn_funs = map (fn (f, _, _) => f) bn_funs_decls;
 
   val ((fv, fvbn), fv_def, lthy3a) = define_raw_fv dtinfo bn_funs_decls raw_bclauses lthy3;
   val (((alpha_ts, alpha_intros), (alpha_cases, alpha_induct)), lthy4) =
     define_raw_alpha dtinfo bn_funs_decls raw_bclauses fv lthy3a;
   val (alpha_ts_nobn, alpha_ts_bn) = chop (length fv) alpha_ts
-
+  val dts_names = map (fn (i, (s, _, _)) => (s, i)) (#descr dtinfo);
+  val bn_tys = map (domain_type o fastype_of) raw_bn_funs;
+  val bn_nos = map (dtyp_no_of_typ dts_names) bn_tys;
+  val bns = raw_bn_funs ~~ bn_nos;
+  val rel_dists = flat (map (distinct_rel lthy4 alpha_cases)
+    (rel_distinct ~~ alpha_ts_nobn));
+  val rel_dists_bn = flat (map (distinct_rel lthy4 alpha_cases)
+    ((map (fn i => nth rel_distinct i) bn_nos) ~~ alpha_ts_bn))
+  val alpha_eq_iff = build_rel_inj alpha_intros (inject @ distincts) alpha_cases lthy4
+  val _ = tracing "Proving equivariance";
+  val (bv_eqvt, lthy5) = prove_eqvt raw_tys induct (raw_bn_eqs @ raw_perm_def) (map fst bns) lthy4
+  val (fv_eqvt, lthy6) = prove_eqvt raw_tys induct (fv_def @ raw_perm_def) (fv @ fvbn) lthy5
 in
-  ((raw_dt_names, raw_bn_funs_loc, raw_bn_eqs_loc, raw_bclauses, raw_bns), lthy4)
+  ((raw_dt_names, raw_bn_funs_loc, raw_bn_eqs_loc, raw_bclauses, raw_bns), lthy6)
 end
 *}
 
@@ -540,6 +555,7 @@
   All xs::"name fset" ty::"ty_raw" bind_res xs in ty
 thm fv_tys_raw.simps
 thm alpha_tys_raw.intros
+thm eqvts
 
 (* some further tests *)
 

--- a/Nominal/Parser.thy	Fri Apr 30 13:57:59 2010 +0200
+++ b/Nominal/Parser.thy	Fri Apr 30 14:48:13 2010 +0200
@@ -391,8 +391,7 @@
     define_fv_alpha_export dtinfo raw_binds_flat bn_funs_decls lthy3;
   val (fv, fvbn) = chop (length perms) fv_ts;
 
-  val (alpha_ts_nobn, alpha_ts_bn) = chop (length perms) alpha_ts
-  val alpha_inducts = Project_Rule.projects lthy4 (1 upto (length dts)) alpha_induct;
+  val (alpha_ts_nobn, alpha_ts_bn) = chop (length fv) alpha_ts
   val dts_names = map (fn (i, (s, _, _)) => (s, i)) (#descr dtinfo);
   val bn_tys = map (domain_type o fastype_of) raw_bn_funs;
   val bn_nos = map (dtyp_no_of_typ dts_names) bn_tys;
@@ -476,7 +475,7 @@
     snd (Local_Theory.note ((suffix_bind s, [Attrib.internal (K Simplifier.simp_add)]), th) ctxt);
   val (_, lthy14) = Local_Theory.note ((suffix_bind "induct",
     [Attrib.internal (K (Rule_Cases.case_names constr_names))]), [Rule_Cases.name constr_names q_induct]) lthy13;
-  val q_inducts = Project_Rule.projects lthy13 (1 upto (length alpha_inducts)) q_induct
+  val q_inducts = Project_Rule.projects lthy13 (1 upto (length fv)) q_induct
   val (_, lthy14a) = Local_Theory.note ((suffix_bind "inducts", []), q_inducts) lthy14;
   val q_perm = map (lift_thm qtys lthy14) raw_perm_def;
   val lthy15 = note_simp_suffix "perm" q_perm lthy14a;