--- a/Nominal/ExCoreHaskell.thy	Thu Mar 25 15:06:58 2010 +0100
+++ b/Nominal/ExCoreHaskell.thy	Thu Mar 25 17:30:46 2010 +0100
@@ -5,7 +5,6 @@
 (* core haskell *)
 
 ML {* val _ = recursive := false *}
-ML {* val _ = cheat_bn_eqvt := true *}
 ML {* val _ = cheat_bn_rsp := true *}
 ML {* val _ = cheat_const_rsp := true *}
 ML {* val _ = cheat_alpha_bn_rsp := true *}

--- a/Nominal/ExLet.thy	Thu Mar 25 15:06:58 2010 +0100
+++ b/Nominal/ExLet.thy	Thu Mar 25 17:30:46 2010 +0100
@@ -7,6 +7,8 @@
 atom_decl name
 
 ML {* val _ = recursive := false  *}
+
+
 nominal_datatype trm =
   Vr "name"
 | Ap "trm" "trm"

--- a/Nominal/Fv.thy	Thu Mar 25 15:06:58 2010 +0100
+++ b/Nominal/Fv.thy	Thu Mar 25 17:30:46 2010 +0100
@@ -1099,4 +1099,55 @@
   simp_tac (HOL_ss addsimps @{thms Collect_const finite.emptyI})
 *}
 
+(* 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,...} = ((fn _ => print_tac (PolyML.makestring names')) THEN'
+    InductTacs.induct_rules_tac context [(flat trm_gl_insts)] [ind]
+    THEN_ALL_NEW split_conjs 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 ((perm_at $ pi $ (fnctn $ arg)), (fnctn $ (perm_arg arg $ pi $ arg)))], ctxt)
+end
+*}
+
+ML {*
+fun prove_eqvt tys ind simps funs ctxt =
+let
+  val ([pi], ctxt') = Variable.variant_fixes ["p"] ctxt;
+  val pi = Free (pi, @{typ perm});
+  val tac = asm_full_simp_tac (HOL_ss addsimps (@{thm atom_eqvt} :: simps @ all_eqvts ctxt'))
+  val ths_loc = prove_by_induct tys (build_eqvt_gl pi) ind tac funs ctxt'
+  val ths = Variable.export ctxt' ctxt ths_loc
+  val add_eqvt = Attrib.internal (fn _ => Nominal_ThmDecls.eqvt_add)
+in
+  (ths, snd (Local_Theory.note ((Binding.empty, [add_eqvt]), ths) ctxt))
+end
+*}
+
+end

--- a/Nominal/Parser.thy	Thu Mar 25 15:06:58 2010 +0100
+++ b/Nominal/Parser.thy	Thu Mar 25 17:30:46 2010 +0100
@@ -287,8 +287,6 @@
 *}
 
 ML {* val cheat_equivp = Unsynchronized.ref false *}
-ML {* val cheat_bn_eqvt = Unsynchronized.ref false *}
-ML {* val cheat_fv_eqvt = Unsynchronized.ref false *}
 ML {* val cheat_alpha_eqvt = Unsynchronized.ref false *}
 ML {* val cheat_bn_rsp = Unsynchronized.ref false *}
 ML {* val cheat_fv_rsp = Unsynchronized.ref false *}
@@ -314,8 +312,9 @@
   val raw_bn_eqs = ProofContext.export lthy2 lthy raw_bn_eqs_loc
 
   val dtinfo = Datatype.the_info (ProofContext.theory_of lthy2) (hd raw_dt_names);
-  val descr = #descr dtinfo;
-  val sorts = #sorts dtinfo;
+  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_typs = map (fn i => typ_of_dtyp descr sorts (DtRec i)) (map fst descr)
   val all_full_tnames = map (fn (_, (n, _, _)) => n) descr;
   val dtinfos = map (Datatype.the_info (ProofContext.theory_of lthy2)) all_full_tnames;
@@ -345,39 +344,26 @@
     ((map (fn i => nth rel_distinct i) bn_nos) ~~ alpha_ts_bn))
   val alpha_eq_iff = build_alpha_inj alpha_intros (inject @ distincts) alpha_cases lthy4
   val _ = tracing "Proving equivariance";
-  fun build_bv_eqvt simps inducts (t, n) ctxt =
-    build_eqvts Binding.empty [t]
-      (if !cheat_bn_eqvt then (fn _ => fn _ => Skip_Proof.cheat_tac thy)
-       else build_eqvts_tac (nth inducts n) simps ctxt
-      ) ctxt
-  val (bv_eqvts, lthy5) = fold_map (build_bv_eqvt (raw_bn_eqs @ raw_perm_def) inducts) bns lthy4;
-  val fv_eqvt_tac =
-    if !cheat_fv_eqvt then (fn _ => fn _ => Skip_Proof.cheat_tac thy)
-    else build_eqvts_tac induct ((flat (map snd bv_eqvts)) @ fv_def @ raw_perm_def) lthy5
-  val (fv_eqvts, lthy6) = build_eqvts Binding.empty fv_ts_nobn fv_eqvt_tac lthy5;
-  val (fv_bn_eqvts, lthy6a) =
-    if fv_ts_bn = [] then ([], lthy6) else
-    fold_map (build_bv_eqvt ((flat (map snd bv_eqvts)) @ fv_def @ raw_perm_def) inducts)
-      (fv_ts_bn ~~ bn_nos) lthy6;
-  val raw_fv_bv_eqvt = flat (map snd bv_eqvts) @ (snd fv_eqvts) @ flat (map snd fv_bn_eqvts)
+  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_ts_nobn @ fv_ts_bn) lthy5
   fun alpha_eqvt_tac' _ =
     if !cheat_alpha_eqvt then Skip_Proof.cheat_tac thy
-    else alpha_eqvt_tac alpha_induct (raw_perm_def @ alpha_eq_iff @ raw_fv_bv_eqvt) lthy6a 1
-  val alpha_eqvt = build_alpha_eqvts alpha_ts alpha_eqvt_tac' lthy6a;
+    else alpha_eqvt_tac alpha_induct (raw_perm_def @ alpha_eq_iff) lthy6 1
+  val alpha_eqvt = build_alpha_eqvts alpha_ts alpha_eqvt_tac' lthy6;
   val _ = tracing "Proving equivalence";
   val (rfv_ts_nobn, rfv_ts_bn) = chop (length perms) ordered_fv_ts;
   val fv_alpha_all = combine_fv_alpha_bns (rfv_ts_nobn, rfv_ts_bn) (alpha_ts_nobn, alpha_ts_bn) bn_nos;
-  val reflps = build_alpha_refl fv_alpha_all alpha_ts induct alpha_eq_iff lthy6a;
+  val reflps = build_alpha_refl fv_alpha_all alpha_ts induct alpha_eq_iff lthy6;
   val alpha_equivp =
-    if !cheat_equivp then map (equivp_hack lthy6a) alpha_ts_nobn
+    if !cheat_equivp then map (equivp_hack lthy6) alpha_ts_nobn
     else build_equivps alpha_ts reflps alpha_induct
-      inject alpha_eq_iff distincts alpha_cases alpha_eqvt lthy6a;
+      inject alpha_eq_iff distincts alpha_cases alpha_eqvt lthy6;
   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 lthy7 = define_quotient_type
     (map (fn ((b, t), alpha) => (([], b, NoSyn), (t, alpha))) ((qty_binds ~~ all_typs) ~~ alpha_ts_nobn))
-    (ALLGOALS (resolve_tac alpha_equivp)) lthy6a;
+    (ALLGOALS (resolve_tac alpha_equivp)) lthy6;
   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)) =>
@@ -455,7 +441,7 @@
   val (_, lthy18) = Local_Theory.note ((suffix_bind "eq_iff", []), q_eq_iff) lthy17;
   val q_dis = map (lift_thm lthy18) rel_dists;
   val lthy19 = note_simp_suffix "distinct" q_dis lthy18;
-  val q_eqvt = map (lift_thm lthy19) raw_fv_bv_eqvt;
+  val q_eqvt = map (lift_thm lthy19) (bv_eqvt @ fv_eqvt);
   val (_, lthy20) = Local_Theory.note ((Binding.empty,
     [Attrib.internal (fn _ => Nominal_ThmDecls.eqvt_add)]), q_eqvt) lthy19;
   val _ = tracing "Finite Support";

--- a/Nominal/Rsp.thy	Thu Mar 25 15:06:58 2010 +0100
+++ b/Nominal/Rsp.thy	Thu Mar 25 17:30:46 2010 +0100
@@ -125,37 +125,14 @@
 *)
 
 ML {*
-fun build_eqvts_tac induct simps ctxt inds _ = (Datatype_Aux.indtac induct inds THEN_ALL_NEW
-    (asm_full_simp_tac (HOL_ss addsimps
-      (@{thm atom_eqvt} :: (Nominal_ThmDecls.get_eqvts_thms ctxt) @ (Nominal_ThmDecls.get_eqvts_raw_thms ctxt) @ simps)))) 1
-*}
-
-ML {*
 fun perm_arg arg =
 let
   val ty = fastype_of arg
 in
   Const (@{const_name permute}, @{typ perm} --> ty --> ty)
 end
-*}
 
-
-ML {*
-fun build_eqvts bind funs tac ctxt =
-let
-  val pi = Free ("p", @{typ perm});
-  val types = map (domain_type o fastype_of) funs;
-  val indnames = Name.variant_list ["p"] (Datatype_Prop.make_tnames types);
-  val args = map Free (indnames ~~ types);
-  val perm_at = @{term "permute :: perm \<Rightarrow> atom set \<Rightarrow> atom set"}
-  fun eqvtc (fnctn, arg) =
-    HOLogic.mk_eq ((perm_at $ pi $ (fnctn $ arg)), (fnctn $ (perm_arg arg $ pi $ arg)))
-  val gl = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj (map eqvtc (funs ~~ args)))
-  val thm = Goal.prove ctxt ("p" :: indnames) [] gl (tac indnames)
-  val thms = HOLogic.conj_elims thm
-in
-  Local_Theory.note ((bind, [Attrib.internal (fn _ => Nominal_ThmDecls.eqvt_add)]), thms) ctxt
-end
+val perm_at = @{term "permute :: perm \<Rightarrow> atom set \<Rightarrow> atom set"}
 *}
 
 lemma exi: "\<exists>(pi :: perm). P pi \<Longrightarrow> (\<And>(p :: perm). P p \<Longrightarrow> Q (pi \<bullet> p)) \<Longrightarrow> \<exists>pi. Q pi"