--- a/Nominal/Ex/SingleLet.thy	Mon May 31 19:57:29 2010 +0200
+++ b/Nominal/Ex/SingleLet.thy	Tue Jun 01 15:01:05 2010 +0200
@@ -24,23 +24,6 @@
 where
   "bn (As x t) = {atom x}"
 
-thm permute_trm_raw_permute_assg_raw.simps[no_vars]
-thm fv_trm_raw.simps[no_vars] fv_assg_raw.simps[no_vars] fv_bn_raw.simps[no_vars] bn_raw.simps[no_vars]
-thm alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.intros[no_vars]
-
-ML {* val {inducts, ... } = Function.get_info @{context} @{term "fv_trm_raw"}*}
-ML {* Rule_Cases.strict_mutual_rule @{context} (the inducts) *}
-
-lemma
- shows "p1 \<bullet> fv_trm_raw trm_raw = fv_trm_raw (p1 \<bullet> trm_raw)"
- and "p1 \<bullet> fv_assg_raw assg_raw = fv_assg_raw (p1 \<bullet> assg_raw)"
- and "p1 \<bullet> fv_bn_raw assg_raw = fv_bn_raw (p1 \<bullet> assg_raw)"
-apply(induct trm_raw and assg_raw and assg_raw rule: fv_trm_raw_fv_assg_raw_fv_bn_raw.induct)
-apply(perm_simp add: fv_trm_raw.simps fv_assg_raw.simps fv_bn_raw.simps, rule refl)+
-done
-
-
-
 ML {* Inductive.the_inductive *}
 thm trm_assg.fv
 thm trm_assg.supp

--- 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";

--- a/Nominal/Perm.thy	Mon May 31 19:57:29 2010 +0200
+++ b/Nominal/Perm.thy	Tue Jun 01 15:01:05 2010 +0200
@@ -5,9 +5,9 @@
   "../Nominal-General/Nominal2_Eqvt" 
   "Nominal2_FSet"
   "Abs"
-(*uses ("nominal_dt_rawperm.ML")
+uses ("nominal_dt_rawperm.ML")
      ("nominal_dt_rawfuns.ML")
-     ("nominal_dt_alpha.ML")*)
+     ("nominal_dt_alpha.ML")
 begin
 
 use "nominal_dt_rawperm.ML"

--- a/Nominal/nominal_dt_rawfuns.ML	Mon May 31 19:57:29 2010 +0200
+++ b/Nominal/nominal_dt_rawfuns.ML	Tue Jun 01 15:01:05 2010 +0200
@@ -25,7 +25,10 @@
   val listify: Proof.context -> term -> term
 
   val define_raw_fvs: Datatype_Aux.descr -> (string * sort) list -> bn_info ->
-    bclause list list list -> thm list -> Proof.context -> term list * term list * thm list * local_theory
+    bclause list list list -> thm list -> Proof.context -> 
+    term list * term list * thm list * thm list * local_theory
+ 
+  val raw_prove_eqvt: term list -> thm list -> thm list -> Proof.context -> thm list
 end
 
 
@@ -228,15 +231,52 @@
 
   val (info, lthy'') = prove_termination (Local_Theory.restore lthy')
 
-  val {fs, simps, ...} = info;
+  val {fs, simps, inducts, ...} = info;
 
   val morphism = ProofContext.export_morphism lthy'' lthy
   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)
+  val simps_exp = map (Morphism.thm morphism) (the simps)
+  val fv_bns_inducts_exp = map (Morphism.thm morphism) (the inducts)
+in
+  (fv_frees_exp, fv_bns_exp, simps_exp, fv_bns_inducts_exp, lthy'')
+end
+
+
+(** equivarance proofs **)
+
+fun mk_eqvt_goal pi const arg =
+let
+  val lhs = mk_perm pi (const $ arg)
+  val rhs = const $ (mk_perm pi arg)  
 in
-  (fv_frees_exp, fv_bns_exp, simps_exp, lthy'')
+  HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))
+end
+
+fun raw_prove_eqvt consts ind_thms simps ctxt =
+let 
+  val ([p], ctxt') = Variable.variant_fixes ["p"] ctxt
+  val p = Free (p, @{typ perm})
+  val arg_tys = 
+    consts
+    |> map fastype_of
+    |> map domain_type 
+  val (arg_names, ctxt'') = Variable.variant_fixes (replicate (length arg_tys) "") ctxt'
+  val args = map Free (arg_names ~~ arg_tys)
+  val goals = map2 (mk_eqvt_goal p) consts args
+  val insts = map (single o SOME) arg_names
+  val const_names = map (fst o dest_Const) consts
+  fun tac ctxt = 
+    Object_Logic.full_atomize_tac
+    THEN' InductTacs.induct_rules_tac ctxt insts ind_thms 
+    THEN_ALL_NEW   
+      (asm_full_simp_tac (HOL_basic_ss addsimps simps)
+       THEN' Nominal_Permeq.eqvt_tac ctxt simps const_names
+       THEN' asm_simp_tac HOL_basic_ss)
+in
+  Goal.prove_multi ctxt' [] [] goals (fn {context, ...} => (HEADGOAL (tac context)))
+  |> ProofContext.export ctxt'' ctxt
 end
 
 end (* structure *)