--- a/Nominal/NewParser.thy	Mon May 24 20:50:15 2010 +0100
+++ b/Nominal/NewParser.thy	Mon May 24 21:11:33 2010 +0100
@@ -349,21 +349,19 @@
     else raise TEST lthy3
 
   (* definition of raw alphas *)
-  val (alpha_ts, alpha_intros, alpha_cases, alpha_induct, lthy4) =
+  val (alpha_ts, alpha_bn_ts, alpha_intros, alpha_cases, alpha_induct, lthy4) =
     if get_STEPS lthy > 4 
     then define_raw_alpha descr sorts raw_bn_info raw_bclauses raw_fvs lthy3a
     else raise TEST lthy3a
   
-  val (alpha_ts_nobn, alpha_ts_bn) = chop (length raw_fvs) alpha_ts
-  
   val dts_names = map (fn (i, (s, _, _)) => (s, i)) descr;
   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 = flat (map (distinct_rel lthy4 alpha_cases) (rel_distinct ~~ alpha_ts));
   val rel_dists_bn = flat (map (distinct_rel lthy4 alpha_cases)
-    ((map (fn i => nth rel_distinct i) bn_nos) ~~ alpha_ts_bn))
+    ((map (fn i => nth rel_distinct i) bn_nos) ~~ alpha_bn_ts))
   
   (* definition of raw_alpha_eq_iff  lemmas *)
   val alpha_eq_iff = 
@@ -373,15 +371,27 @@
 
   val alpha_eq_iff_simp = map remove_loop alpha_eq_iff;
   
-  (* proving equivariance lemmas *)
+  (* proving equivariance lemmas for bns, fvs and alpha *)
   val _ = warning "Proving equivariance";
-  val (bv_eqvt, lthy5) = prove_eqvt all_tys induct_thm ((*raw_bn_eqs @*) raw_perm_defs) (map fst bns) lthy4
-  val (fv_eqvt, lthy6) = prove_eqvt all_tys induct_thm (raw_fv_defs @ raw_perm_defs) (raw_fvs @ raw_fv_bns) lthy5
-  val (alpha_eqvt, lthy6a) = Nominal_Eqvt.equivariance alpha_ts alpha_induct alpha_intros lthy6;
+  val (bv_eqvt, lthy5) = 
+    if get_STEPS lthy > 6
+    then prove_eqvt all_tys induct_thm (raw_bn_eqs @ raw_perm_defs) (map fst bns) lthy4
+    else raise TEST lthy4
+
+  val (fv_eqvt, lthy6) = 
+    if get_STEPS lthy > 7
+    then prove_eqvt all_tys induct_thm (raw_fv_defs @ raw_perm_defs) (raw_fvs @ raw_fv_bns) lthy5
+    else raise TEST lthy5
+
+  val (alpha_eqvt, lthy6a) =
+    if get_STEPS lthy > 8
+    then Nominal_Eqvt.equivariance alpha_ts alpha_induct alpha_intros lthy6
+    else raise TEST lthy6
+
 
   (* proving alpha equivalence *)
   val _ = warning "Proving equivalence";
-  val fv_alpha_all = combine_fv_alpha_bns (raw_fvs, raw_fv_bns) (alpha_ts_nobn, alpha_ts_bn) bn_nos;
+  val fv_alpha_all = combine_fv_alpha_bns (raw_fvs, raw_fv_bns) (alpha_ts, alpha_bn_ts) bn_nos;
   val reflps = build_alpha_refl fv_alpha_all alpha_ts induct_thm alpha_eq_iff_simp lthy6a;
   val alpha_equivp =
     if !cheat_equivp then map (equivp_hack lthy6a) alpha_ts
@@ -390,7 +400,7 @@
   val qty_binds = map (fn (_, b, _, _) => b) dts;
   val qty_names = map Name.of_binding qty_binds;
   val qty_full_names = map (Long_Name.qualify thy_name) qty_names
-  val (qtys, lthy7) = define_quotient_types qty_binds all_tys alpha_ts_nobn alpha_equivp lthy6a;
+  val (qtys, lthy7) = define_quotient_types qty_binds all_tys alpha_ts alpha_equivp lthy6a;
   val const_names = map Name.of_binding (flat (map (fn (_, _, _, t) => map (fn (b, _, _) => b) t) dts));
   val raw_consts =
     flat (map (fn (i, (_, _, l)) =>
@@ -399,7 +409,7 @@
           Datatype_Aux.typ_of_dtyp descr sorts (Datatype_Aux.DtRec i))) l) descr);
   val (consts, const_defs, lthy8) = quotient_lift_consts_export qtys (const_names ~~ raw_consts) lthy7;
   val _ = warning "Proving respects";
-  val bns_rsp_pre' = build_fvbv_rsps alpha_ts alpha_induct [] (*raw_bn_eqs*) (map fst bns) lthy8;
+  val bns_rsp_pre' = build_fvbv_rsps alpha_ts alpha_induct raw_bn_eqs (map fst bns) lthy8;
   val (bns_rsp_pre, lthy9) = fold_map (
     fn (bn_t, _) => prove_const_rsp qtys Binding.empty [bn_t] (fn _ =>
        resolve_tac bns_rsp_pre' 1)) bns lthy8;
@@ -416,11 +426,11 @@
     (fn _ => asm_simp_tac (HOL_ss addsimps alpha_eqvt) 1) lthy10;
   fun alpha_bn_rsp_tac _ = if !cheat_alpha_bn_rsp then Skip_Proof.cheat_tac thy
     else
-      let val alpha_bn_rsp_pre = prove_alpha_bn_rsp alpha_ts alpha_induct (alpha_eq_iff_simp @ rel_dists @ rel_dists_bn) alpha_equivp exhaust_thms alpha_ts_bn lthy11 in asm_simp_tac (HOL_ss addsimps alpha_bn_rsp_pre) 1 end;
+      let val alpha_bn_rsp_pre = prove_alpha_bn_rsp alpha_ts alpha_induct (alpha_eq_iff_simp @ rel_dists @ rel_dists_bn) alpha_equivp exhaust_thms alpha_bn_ts lthy11 in asm_simp_tac (HOL_ss addsimps alpha_bn_rsp_pre) 1 end;
   val (alpha_bn_rsps, lthy11a) = fold_map (fn cnst => prove_const_rsp qtys Binding.empty [cnst]
-    alpha_bn_rsp_tac) alpha_ts_bn lthy11
+    alpha_bn_rsp_tac) alpha_bn_ts lthy11
   fun const_rsp_tac _ =
-    let val alpha_alphabn = prove_alpha_alphabn alpha_ts alpha_induct alpha_eq_iff_simp alpha_ts_bn lthy11a
+    let val alpha_alphabn = prove_alpha_alphabn alpha_ts alpha_induct alpha_eq_iff_simp alpha_bn_ts lthy11a
       in constr_rsp_tac alpha_eq_iff_simp (fv_rsp @ bns_rsp @ reflps @ alpha_alphabn) 1 end
   val (const_rsps, lthy12) = fold_map (fn cnst => prove_const_rsp qtys Binding.empty [cnst]
     const_rsp_tac) raw_consts lthy11a
@@ -428,10 +438,10 @@
   val (qfv_ts, qfv_defs, lthy12a) = quotient_lift_consts_export qtys (qfv_names ~~ (raw_fvs @ raw_fv_bns)) lthy12;
   val (qfv_ts_nobn, qfv_ts_bn) = chop (length raw_perm_funs) qfv_ts;
   val qbn_names = map (fn (b, _ , _) => Name.of_binding b) bn_funs
-  val (qbn_ts, qbn_defs, lthy12b) = quotient_lift_consts_export qtys (qbn_names ~~ [] (*raw_bn_funs*)) lthy12a;
-  val qalpha_bn_names = map (unsuffix "_raw" o Long_Name.base_name o fst o dest_Const) alpha_ts_bn
-  val (qalpha_ts_bn, qalphabn_defs, lthy12c) = 
-    quotient_lift_consts_export qtys (qalpha_bn_names ~~ alpha_ts_bn) lthy12b;
+  val (qbn_ts, qbn_defs, lthy12b) = quotient_lift_consts_export qtys (qbn_names ~~ raw_bn_funs) lthy12a;
+  val qalpha_bn_names = map (unsuffix "_raw" o Long_Name.base_name o fst o dest_Const) alpha_bn_ts
+  val (qalpha_bn_ts, qalphabn_defs, lthy12c) = 
+    quotient_lift_consts_export qtys (qalpha_bn_names ~~ alpha_bn_ts) lthy12b;
   val _ = warning "Lifting permutations";
   val thy = Local_Theory.exit_global lthy12c;
   val perm_names = map (fn x => "permute_" ^ x) qty_names
@@ -455,7 +465,7 @@
   val lthy15 = note_simp_suffix "perm" q_perm lthy14a;
   val q_fv = map (lift_thm qtys lthy15) raw_fv_defs;
   val lthy16 = note_simp_suffix "fv" q_fv lthy15;
-  val q_bn = map (lift_thm qtys lthy16) [] (*raw_bn_eqs;*)
+  val q_bn = map (lift_thm qtys lthy16) raw_bn_eqs;
   val lthy17 = note_simp_suffix "bn" q_bn lthy16;
   val _ = warning "Lifting eq-iff";
   (*val _ = map tracing (map PolyML.makestring alpha_eq_iff);*)
@@ -479,7 +489,7 @@
   val lthy21 = Theory_Target.instantiation (qty_full_names, [], @{sort fs}) thy3;
   fun tac _ = Class.intro_classes_tac [] THEN (ALLGOALS (resolve_tac fin_supp))
   val lthy22 = Class.prove_instantiation_instance tac lthy21
-  val fv_alpha_all = combine_fv_alpha_bns (qfv_ts_nobn, qfv_ts_bn) (alpha_ts_nobn, qalpha_ts_bn) bn_nos;
+  val fv_alpha_all = combine_fv_alpha_bns (qfv_ts_nobn, qfv_ts_bn) (alpha_ts, qalpha_bn_ts) bn_nos;
   val (names, supp_eq_t) = supp_eq fv_alpha_all;
   val _ = warning "Support Equations";
   fun supp_eq_tac' _ = if !cheat_supp_eq then Skip_Proof.cheat_tac thy else

--- a/Nominal/nominal_dt_alpha.ML	Mon May 24 20:50:15 2010 +0100
+++ b/Nominal/nominal_dt_alpha.ML	Mon May 24 21:11:33 2010 +0100
@@ -9,7 +9,7 @@
 sig
   val define_raw_alpha: Datatype_Aux.descr -> (string * sort) list -> bn_info ->
     bclause list list list -> term list -> Proof.context -> 
-    term list * thm list * thm list * thm * local_theory
+    term list * term list * thm list * thm list * thm * local_theory
 end
 
 structure Nominal_Dt_Alpha: NOMINAL_DT_ALPHA =
@@ -219,18 +219,20 @@
       coind = false, no_elim = false, no_ind = false, skip_mono = true, fork_mono = false}
      all_alpha_names [] all_alpha_intros [] lthy
 
-  val alpha_trms_loc = #preds alphas;
+  val all_alpha_trms_loc = #preds alphas;
   val alpha_induct_loc = #raw_induct alphas;
   val alpha_intros_loc = #intrs alphas;
   val alpha_cases_loc = #elims alphas;
   val phi = ProofContext.export_morphism lthy' lthy;
 
-  val alpha_trms = map (Morphism.term phi) alpha_trms_loc;
+  val all_alpha_trms = map (Morphism.term phi) all_alpha_trms_loc;
   val alpha_induct = Morphism.thm phi alpha_induct_loc;
   val alpha_intros = map (Morphism.thm phi) alpha_intros_loc
   val alpha_cases = map (Morphism.thm phi) alpha_cases_loc
+
+  val (alpha_trms, alpha_bn_trms) = chop (length fvs) all_alpha_trms
 in
-  (alpha_trms, alpha_intros, alpha_cases, alpha_induct, lthy')
+  (alpha_trms, alpha_bn_trms, alpha_intros, alpha_cases, alpha_induct, lthy')
 end
 
 end (* structure *)