--- a/Nominal/NewParser.thy	Mon May 31 19:57:29 2010 +0200
+++ b/Nominal/NewParser.thy	Tue Jun 01 15:01:05 2010 +0200
@@ -275,7 +275,7 @@
   val (info, lthy3) = prove_termination (Local_Theory.restore lthy2)
   val {fs, simps, inducts, ...} = info;
 
-  val raw_bn_induct = Rule_Cases.strict_mutual_rule lthy3 (the inducts)
+  val raw_bn_induct = (the inducts)
   val raw_bn_eqs = the simps
 
   val raw_bn_info = 
@@ -319,71 +319,6 @@
 setup STEPS_setup
 
 ML {*
-fun mk_conjl props =
-  fold (fn a => fn b =>
-    if a = @{term True} then b else
-    if b = @{term True} then a else
-    HOLogic.mk_conj (a, b)) (rev props) @{term True};
-*}
-
-ML {*
-val split_conj_tac = REPEAT o etac conjE THEN' TRY o REPEAT_ALL_NEW (CHANGED o rtac conjI)
-*}
-
-(* Given function for buildng a goal for an input, prepares a
-   one common goals for all the inputs and proves it by induction
-   together *)
-ML {*
-fun prove_by_induct tys build_goal ind utac inputs ctxt =
-let
-  val names = Datatype_Prop.make_tnames tys;
-  val (names', ctxt') = Variable.variant_fixes names ctxt;
-  val frees = map Free (names' ~~ tys);
-  val (gls_lists, ctxt'') = fold_map (build_goal (tys ~~ frees)) inputs ctxt';
-  val gls = flat gls_lists;
-  fun trm_gls_map t = filter (exists_subterm (fn s => s = t)) gls;
-  val trm_gl_lists = map trm_gls_map frees;
-  val trm_gl_insts = map2 (fn n => fn l => [NONE, if l = [] then NONE else SOME n]) names' trm_gl_lists
-  val trm_gls = map mk_conjl trm_gl_lists;
-  val gl = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj trm_gls);
-  fun tac {context,...} = (
-    InductTacs.induct_rules_tac context [(flat trm_gl_insts)] [ind]
-    THEN_ALL_NEW split_conj_tac THEN_ALL_NEW utac) 1
-  val th_loc = Goal.prove ctxt'' [] [] gl tac
-  val ths_loc = HOLogic.conj_elims th_loc
-  val ths = Variable.export ctxt'' ctxt ths_loc
-in
-  filter (fn x => not (prop_of x = prop_of @{thm TrueI})) ths
-end
-*}
-
-ML {*
-fun build_eqvt_gl pi frees fnctn ctxt =
-let
-  val typ = domain_type (fastype_of fnctn);
-  val arg = the (AList.lookup (op=) frees typ);
-in
-  ([HOLogic.mk_eq (mk_perm pi (fnctn $ arg), fnctn $ (mk_perm pi arg))], ctxt)
-end
-*}
-
-ML {*
-fun prove_eqvt tys ind simps funs ctxt =
-let
-  val ([p], ctxt') = Variable.variant_fixes ["p"] ctxt;
-  val p = Free (p, @{typ perm})
-  val simp_set = @{thms atom_eqvt permute_list.simps} @ simps @ all_eqvts ctxt'
-  val tac = asm_full_simp_tac (HOL_ss addsimps simp_set)
-  val ths_loc = prove_by_induct tys (build_eqvt_gl p) ind tac funs ctxt'
-  val ths = Variable.export ctxt' ctxt ths_loc
-  val add_eqvt = Attrib.internal (fn _ => Nominal_ThmDecls.eqvt_add)
-  val _ = tracing ("eqvt thms\n" ^ cat_lines (map (Syntax.string_of_term ctxt o prop_of) ths))
-in
-  (ths, snd (Local_Theory.note ((Binding.empty, [add_eqvt]), ths) ctxt))
-end
-*}
-
-ML {*
 fun nominal_datatype2 dts bn_funs bn_eqs bclauses lthy =
 let
   (* definition of the raw datatypes *)
@@ -411,7 +346,6 @@
     then raw_bn_decls dt_names raw_dts raw_bn_funs raw_bn_eqs constr_thms lthy0
     else raise TEST lthy0
 
-
   val bn_nos = map (fn (_, i, _) => i) raw_bn_info;
   val bns = raw_bn_funs ~~ bn_nos;
 
@@ -431,7 +365,7 @@
   (* definition of raw fv_functions *)
   val lthy3 = Theory_Target.init NONE thy;
 
-  val (raw_fvs, raw_fv_bns, raw_fv_defs, lthy3a) = 
+  val (raw_fvs, raw_fv_bns, raw_fv_defs, raw_fv_bns_induct, lthy3a) = 
     if get_STEPS lthy2 > 3 
     then define_raw_fvs descr sorts raw_bn_info raw_bclauses constr_thms lthy3
     else raise TEST lthy3
@@ -454,25 +388,35 @@
 
   (* proving equivariance lemmas for bns, fvs and alpha *)
   val _ = warning "Proving equivariance";
-  val (bv_eqvt, lthy5) = 
+  val bn_eqvt = 
     if get_STEPS lthy > 6
-    then prove_eqvt all_tys induct_thm (raw_bn_eqs @ raw_perm_defs) raw_bn_funs lthy4
+    then raw_prove_eqvt raw_bn_funs raw_bn_induct (raw_bn_eqs @ raw_perm_defs) lthy4
     else raise TEST lthy4
 
-  val (fv_eqvt, lthy6) = 
+  val add_eqvt = Attrib.internal (K Nominal_ThmDecls.eqvt_add)
+  val (_, lthy_tmp) = Local_Theory.note ((Binding.empty, [add_eqvt]), bn_eqvt) lthy4
+
+  val fv_eqvt = 
     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
+    then raw_prove_eqvt (raw_fvs @ raw_fv_bns) raw_fv_bns_induct (raw_fv_defs @ raw_perm_defs) lthy_tmp
+    else raise TEST lthy4
+ 
+  val (_, lthy_tmp') = Local_Theory.note ((Binding.empty, [add_eqvt]), fv_eqvt) lthy_tmp
 
   val (alpha_eqvt, lthy6a) =
     if get_STEPS lthy > 8
-    then Nominal_Eqvt.equivariance alpha_trms alpha_induct alpha_intros lthy6
-    else raise TEST lthy6
+    then Nominal_Eqvt.equivariance alpha_trms alpha_induct alpha_intros lthy_tmp'
+    else raise TEST lthy4
 
+  val _ = 
+    if get_STEPS lthy > 9
+    then true else raise TEST lthy4
 
   (* proving alpha equivalence *)
   val _ = warning "Proving equivalence";
-  val fv_alpha_all = combine_fv_alpha_bns (raw_fvs, raw_fv_bns) (alpha_trms, alpha_bn_trms) bn_nos;
+
+  val fv_alpha_all = combine_fv_alpha_bns (raw_fvs, raw_fv_bns) (alpha_trms, alpha_bn_trms) bn_nos
+
   val reflps = build_alpha_refl fv_alpha_all alpha_trms induct_thm alpha_eq_iff lthy6a;
   val alpha_equivp =
     if !cheat_equivp then map (equivp_hack lthy6a) alpha_trms
@@ -559,7 +503,7 @@
   val (_, lthy18) = Local_Theory.note ((suffix_bind "eq_iff", []), q_eq_iff) lthy17;
   val q_dis = map (lift_thm qtys lthy18) alpha_distincts;
   val lthy19 = note_simp_suffix "distinct" q_dis lthy18;
-  val q_eqvt = map (lift_thm qtys lthy19) (bv_eqvt @ fv_eqvt);
+  val q_eqvt = map (lift_thm qtys lthy19) (bn_eqvt @ fv_eqvt);
   val (_, lthy20) = Local_Theory.note ((Binding.empty,
     [Attrib.internal (fn _ => Nominal_ThmDecls.eqvt_add)]), q_eqvt) lthy19;
   val _ = warning "Supports";