--- 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 *)