diff -r a4743b7cd887 -r f65564bcf342 Nominal/Fv.thy
--- a/Nominal/Fv.thy	Sat Mar 20 16:27:51 2010 +0100
+++ b/Nominal/Fv.thy	Sat Mar 20 18:16:26 2010 +0100
@@ -655,7 +655,7 @@
 *}
 
 ML {*
-fun build_alpha_refl_gl alphas (x, y, z) =
+fun build_alpha_sym_trans_gl alphas (x, y, z) =
 let
   fun build_alpha alpha =
     let
@@ -668,26 +668,84 @@
         HOLogic.mk_all (z, ty,
           HOLogic.mk_imp (alpha $ var2 $ var3, alpha $ var $ var3)))
     in
-      ((alpha $ var $ var), (symp, transp))
+      (symp, transp)
     end;
-  val (refl_eqs, eqs) = split_list (map build_alpha alphas)
+  val eqs = map build_alpha alphas
   val (sym_eqs, trans_eqs) = split_list eqs
   fun conj l = @{term Trueprop} $ foldr1 HOLogic.mk_conj l
 in
-  (conj refl_eqs, (conj sym_eqs, conj trans_eqs))
+  (conj sym_eqs, conj trans_eqs)
+end
+*}
+
+ML {*
+fun build_alpha_refl_gl fv_alphas_lst =
+let
+  val (fvs_alphas, ls) = split_list fv_alphas_lst;
+  val (_, alpha_ts) = split_list fvs_alphas;
+  val tys = map (domain_type o fastype_of) alpha_ts;
+  val names = Datatype_Prop.make_tnames tys;
+  val args = map Free (names ~~ tys);
+  fun mk_alpha_refl arg (_, alpha) = alpha $ arg $ arg;
+  fun refl_eq_arg ((alpha, arg), l) =
+    foldr1 HOLogic.mk_conj
+      ((alpha $ arg $ arg) ::
+       (map (mk_alpha_refl arg) l))
+  val eqs = map refl_eq_arg ((alpha_ts ~~ args) ~~ ls)
+in
+  (names, HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj eqs))
 end
 *}
 
 ML {*
-fun reflp_tac induct inj ctxt =
+fun reflp_tac induct eq_iff ctxt =
   rtac induct THEN_ALL_NEW
-  simp_tac ((mk_minimal_ss ctxt) addsimps inj) THEN_ALL_NEW
+  simp_tac ((mk_minimal_ss ctxt) addsimps eq_iff) THEN_ALL_NEW
   split_conjs THEN_ALL_NEW REPEAT o rtac @{thm exI[of _ "0 :: perm"]}
   THEN_ALL_NEW split_conjs THEN_ALL_NEW asm_full_simp_tac (HOL_ss addsimps
      @{thms alpha_gen fresh_star_def fresh_zero_perm permute_zero ball_triv
        add_0_left supp_zero_perm Int_empty_left split_conv})
 *}
 
+ML {*
+fun build_alpha_refl fv_alphas_lst induct eq_iff ctxt =
+let
+  val (names, gl) = build_alpha_refl_gl fv_alphas_lst;
+  val refl_conj = Goal.prove ctxt names [] gl (fn _ => reflp_tac induct eq_iff ctxt 1);
+in
+  HOLogic.conj_elims refl_conj
+end
+*}
+
+ML {*
+fun build_alpha_alphabn fv_alphas_lst inducts eq_iff ctxt  =
+let
+  val (fvs_alphas, ls) = split_list fv_alphas_lst;
+  val (_, alpha_ts) = split_list fvs_alphas;
+  val tys = map (domain_type o fastype_of) alpha_ts;
+  val names = Datatype_Prop.make_tnames tys;
+  val names2 = Name.variant_list names names;
+  val args = map Free (names ~~ tys);
+  val args2 = map Free (names2 ~~ tys);
+  fun alpha_alphabn ((alpha, (arg, arg2)), (no, l)) =
+    if l = [] then [] else
+    let
+      val alpha_bns = map snd l;
+      val lhs = alpha $ arg $ arg2;
+      val rhs = foldr1 HOLogic.mk_conj (map (fn x => x $ arg $ arg2) alpha_bns);
+      val gl = Logic.mk_implies (HOLogic.mk_Trueprop lhs, HOLogic.mk_Trueprop rhs);
+      fun tac _ = (etac (nth inducts no) THEN_ALL_NEW TRY o rtac @{thm TrueI}
+        THEN_ALL_NEW asm_full_simp_tac (HOL_ss addsimps eq_iff)) 1
+      val th = Goal.prove ctxt (names @ names2) [] gl tac;
+    in
+      Project_Rule.projects ctxt (1 upto length l) th
+    end;
+  val eqs = map alpha_alphabn ((alpha_ts ~~ (args ~~ args2)) ~~ ((0 upto (length ls - 1)) ~~ ls));
+in
+  flat eqs
+end
+*}
+
 
 lemma exi_neg: "\<exists>(pi :: perm). P pi \<Longrightarrow> (\<And>(p :: perm). P p \<Longrightarrow> Q (- p)) \<Longrightarrow> \<exists>pi. Q pi"
 apply (erule exE)
@@ -787,25 +845,22 @@
 *}
 
 ML {*
-fun build_equivps alphas term_induct alpha_induct term_inj alpha_inj distinct cases eqvt ctxt =
+fun build_equivps alphas reflps alpha_induct term_inj alpha_inj distinct cases eqvt ctxt =
 let
   val ([x, y, z], ctxt') = Variable.variant_fixes ["x","y","z"] ctxt;
-  val (reflg, (symg, transg)) = build_alpha_refl_gl alphas (x, y, z)
-  fun reflp_tac' _ = reflp_tac term_induct alpha_inj ctxt 1;
+  val (symg, transg) = build_alpha_sym_trans_gl alphas (x, y, z)
   fun symp_tac' _ = symp_tac alpha_induct alpha_inj eqvt ctxt 1;
   fun transp_tac' _ = transp_tac ctxt alpha_induct alpha_inj term_inj distinct cases eqvt 1;
-  val reflt = Goal.prove ctxt' [] [] reflg reflp_tac';
-  val symt = Goal.prove ctxt' [] [] symg symp_tac';
-  val transt = Goal.prove ctxt' [] [] transg transp_tac';
-  val [refltg, symtg, transtg] = Variable.export ctxt' ctxt [reflt, symt, transt]
-  val reflts = HOLogic.conj_elims refltg
-  val symts = HOLogic.conj_elims symtg
-  val transts = HOLogic.conj_elims transtg
+  val symp_loc = Goal.prove ctxt' [] [] symg symp_tac';
+  val transp_loc = Goal.prove ctxt' [] [] transg transp_tac';
+  val [symp, transp] = Variable.export ctxt' ctxt [symp_loc, transp_loc]
+  val symps = HOLogic.conj_elims symp
+  val transps = HOLogic.conj_elims transp
   fun equivp alpha =
     let
       val equivp = Const (@{const_name equivp}, fastype_of alpha --> @{typ bool})
       val goal = @{term Trueprop} $ (equivp $ alpha)
-      fun tac _ = equivp_tac reflts symts transts 1
+      fun tac _ = equivp_tac reflps symps transps 1
     in
       Goal.prove ctxt [] [] goal tac
     end