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

--- a/Nominal/LFex.thy	Sat Mar 20 16:27:51 2010 +0100
+++ b/Nominal/LFex.thy	Sat Mar 20 18:16:26 2010 +0100
@@ -6,7 +6,7 @@
 atom_decl ident
 
 ML {* val _ = cheat_fv_rsp := false *}
-ML {* val _ = cheat_const_rsp := false *}
+ML {* val _ = cheat_alpha_bn_rsp := false *}
 ML {* val _ = cheat_equivp := false *}
 
 nominal_datatype kind =

--- a/Nominal/Parser.thy	Sat Mar 20 16:27:51 2010 +0100
+++ b/Nominal/Parser.thy	Sat Mar 20 18:16:26 2010 +0100
@@ -267,7 +267,7 @@
 
 (* These 2 are critical, we don't know how to do it in term5 *)
 ML {* val cheat_fv_rsp = Unsynchronized.ref true *}
-ML {* val cheat_const_rsp = Unsynchronized.ref true *} (* For alpha_bn 0 and alpha_bn_rsp *)
+ML {* val cheat_alpha_bn_rsp = Unsynchronized.ref true *}
 
 ML {* val cheat_equivp = Unsynchronized.ref true *}
 
@@ -332,9 +332,11 @@
     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;
   val _ = tracing "Proving equivalence";
+  val fv_alpha_all = combine_fv_alpha_bns (fv_ts_nobn, fv_ts_bn) (alpha_ts_nobn, alpha_ts_bn) bn_nos;
+  val reflps = build_alpha_refl fv_alpha_all induct alpha_eq_iff lthy6a;
   val alpha_equivp =
     if !cheat_equivp then map (equivp_hack lthy6a) alpha_ts_nobn
-    else build_equivps alpha_ts induct alpha_induct
+    else build_equivps alpha_ts reflps alpha_induct
       inject alpha_eq_iff distincts alpha_cases alpha_eqvt lthy6a;
   val qty_binds = map (fn (_, b, _, _) => b) dts;
   val qty_names = map Name.of_binding qty_binds;
@@ -361,10 +363,13 @@
   val ((_, fv_rsp), lthy10) = prove_const_rsp Binding.empty fv_ts fv_rsp_tac lthy9
   val (perms_rsp, lthy11) = prove_const_rsp Binding.empty perms
     (fn _ => asm_simp_tac (HOL_ss addsimps alpha_eqvt) 1) lthy10;
-  fun const_rsp_tac _ = if !cheat_const_rsp then Skip_Proof.cheat_tac thy
-    else constr_rsp_tac alpha_eq_iff (fv_rsp @ bns_rsp) alpha_equivp 1
-  val (const_rsps, lthy12) = fold_map (fn cnst => prove_const_rsp Binding.empty [cnst]
-    const_rsp_tac) (raw_consts @ alpha_ts_bn) lthy11
+  val alpha_alphabn = build_alpha_alphabn fv_alpha_all alpha_inducts alpha_eq_iff lthy11;
+  fun const_rsp_tac _ = constr_rsp_tac alpha_eq_iff (fv_rsp @ bns_rsp @ reflps @ alpha_alphabn) 1
+  fun alpha_bn_rsp_tac x = if !cheat_alpha_bn_rsp then Skip_Proof.cheat_tac thy else const_rsp_tac x
+  val (const_rsps, lthy11a) = fold_map (fn cnst => prove_const_rsp Binding.empty [cnst]
+    const_rsp_tac) raw_consts lthy11
+  val (alpha_bn_rsps, lthy12) = fold_map (fn cnst => prove_const_rsp Binding.empty [cnst]
+    alpha_bn_rsp_tac) alpha_ts_bn lthy11a
   val qfv_names = map (unsuffix "_raw" o Long_Name.base_name o fst o dest_Const) ordered_fv_ts
   val (qfv_ts, qfv_defs, lthy12a) = quotient_lift_consts_export (qfv_names ~~ ordered_fv_ts) lthy12;
   val (qfv_ts_nobn, qfv_ts_bn) = chop (length perms) qfv_ts;

--- a/Nominal/Rsp.thy	Sat Mar 20 16:27:51 2010 +0100
+++ b/Nominal/Rsp.thy	Sat Mar 20 18:16:26 2010 +0100
@@ -95,18 +95,15 @@
 *}
 
 ML {*
-fun constr_rsp_tac inj rsp equivps =
-let
-  val reflps = map (fn x => @{thm equivp_reflp} OF [x]) equivps
-in
+fun constr_rsp_tac inj rsp =
   REPEAT o rtac impI THEN'
   simp_tac (HOL_ss addsimps inj) THEN' split_conjs THEN_ALL_NEW
   (asm_simp_tac HOL_ss THEN_ALL_NEW (
-   rtac @{thm exI[of _ "0 :: perm"]} THEN'
-   asm_full_simp_tac (HOL_ss addsimps (rsp @ reflps @
-     @{thms alpha_gen fresh_star_def fresh_zero_perm permute_zero ball_triv}))
+   REPEAT o rtac @{thm exI[of _ "0 :: perm"]} THEN_ALL_NEW
+   simp_tac (HOL_basic_ss addsimps @{thms alpha_gen2}) THEN_ALL_NEW
+   asm_full_simp_tac (HOL_ss addsimps (rsp @
+     @{thms alpha_gen fresh_star_def fresh_zero_perm permute_zero ball_triv add_0_left}))
   ))
-end
 *}
 
 (* Testing code

--- a/Nominal/TySch.thy	Sat Mar 20 16:27:51 2010 +0100
+++ b/Nominal/TySch.thy	Sat Mar 20 18:16:26 2010 +0100
@@ -5,7 +5,7 @@
 atom_decl name
 
 ML {* val _ = cheat_fv_rsp := false *}
-ML {* val _ = cheat_const_rsp := false *}
+ML {* val _ = cheat_alpha_bn_rsp := false *}
 ML {* val _ = cheat_equivp := false *}
 
 nominal_datatype t =
@@ -14,6 +14,51 @@
 and tyS =
   All xs::"name fset" ty::"t" bind xs in ty
 
+lemma size_eqvt: "size (pi \<bullet> x) = size x"
+sorry (* Can this be shown? *)
+
+instantiation t and tyS :: size begin
+
+quotient_definition
+  "size_t :: t \<Rightarrow> nat"
+is
+  "size :: t_raw \<Rightarrow> nat"
+
+quotient_definition
+  "size_tyS :: tyS \<Rightarrow> nat"
+is
+  "size :: tyS_raw \<Rightarrow> nat"
+
+lemma size_rsp:
+  "alpha_t_raw x y \<Longrightarrow> size x = size y"
+  "alpha_tyS_raw a b \<Longrightarrow> size a = size b"
+  apply (induct rule: alpha_t_raw_alpha_tyS_raw.inducts)
+  apply (simp_all only: t_raw_tyS_raw.size)
+  apply (simp_all only: alpha_gen)
+  apply clarify
+  apply (simp_all only: size_eqvt)
+  done
+
+lemma [quot_respect]:
+  "(alpha_t_raw ===> op =) size size"
+  "(alpha_tyS_raw ===> op =) size size"
+  by (simp_all add: size_rsp)
+
+lemma [quot_preserve]:
+  "(rep_t ---> id) size = size"
+  "(rep_tyS ---> id) size = size"
+  by (simp_all add: size_t_def size_tyS_def)
+
+instance
+  by default
+
+end
+
+thm t_raw_tyS_raw.size(4)[quot_lifted]
+thm t_raw_tyS_raw.size(5)[quot_lifted]
+thm t_raw_tyS_raw.size(6)[quot_lifted]
+
+
 thm t_tyS.fv
 thm t_tyS.eq_iff
 thm t_tyS.bn

--- a/TODO	Sat Mar 20 16:27:51 2010 +0100
+++ b/TODO	Sat Mar 20 18:16:26 2010 +0100
@@ -24,10 +24,10 @@
 
 - strong induction rules
 
-- show support equations
+- check support equations for more bindings per constructor
 
 - automate the proofs that are currently proved with sorry:
-  alpha_equivp, fv_rsp, alpha_bn_rsp, alpha_bn_reflp
+  alpha_equivp, fv_rsp, alpha_bn_rsp
 
 - store information about defined nominal datatypes, so that
   it can be used to define new types that depend on these