--- a/Nominal/Nominal2.thy	Wed Jun 29 23:08:44 2011 +0100
+++ b/Nominal/Nominal2.thy	Thu Jun 30 02:19:59 2011 +0100
@@ -232,14 +232,9 @@
       (raw_inject_thms @ raw_distinct_thms) raw_size_thms lthy3b
     
   val _ = trace_msg (K "Defining alpha relations...")
-  val (alpha_trms, alpha_bn_trms, alpha_intros, alpha_cases, alpha_induct, alpha_result, lthy4) =
+  val (alpha_result, lthy4) =
     define_raw_alpha raw_dt_names raw_tys raw_cns_info raw_bn_info raw_bclauses raw_fvs lthy3c
     
-  val _ = tracing ("alpha_induct\n" ^ Syntax.string_of_term lthy3c (prop_of alpha_induct))
-  val _ = tracing ("alpha_intros\n" ^ cat_lines (map (Syntax.string_of_term lthy4 o prop_of) alpha_intros))
-
-  val alpha_tys = map (domain_type o fastype_of) alpha_trms  
-
   val _ = trace_msg (K "Proving distinct theorems...")
   val alpha_distincts = 
     raw_prove_alpha_distincts lthy4 alpha_result raw_distinct_thms raw_dt_names
@@ -267,7 +262,11 @@
   val lthy5 = snd (Local_Theory.note ((Binding.empty, [eqvt_attr]), raw_fv_eqvt) lthy_tmp)
 
   val alpha_eqvt =
-    Nominal_Eqvt.raw_equivariance (alpha_trms @ alpha_bn_trms) alpha_induct alpha_intros lthy5
+    let
+      val AlphaResult {alpha_trms, alpha_bn_trms, alpha_raw_induct, alpha_intros, ...} = alpha_result
+    in
+      Nominal_Eqvt.raw_equivariance (alpha_trms @ alpha_bn_trms) alpha_raw_induct alpha_intros lthy5
+    end
 
   val alpha_eqvt_norm = map (Nominal_ThmDecls.eqvt_transform lthy5) alpha_eqvt
 
@@ -281,35 +280,27 @@
     raw_prove_equivp lthy5 alpha_result alpha_refl_thms alpha_sym_thms alpha_trans_thms
 
   val _ = trace_msg (K "Proving alpha implies bn...")
-  val alpha_bn_imp_thms = 
-    raw_prove_bn_imp alpha_trms alpha_bn_trms alpha_intros alpha_induct lthy5 
-
-  val _ = tracing ("alpha_bn_imp_thms:\n" ^ cat_lines (map (Syntax.string_of_term lthy5 o prop_of) alpha_bn_imp_thms))
+  val alpha_bn_imp_thms = raw_prove_bn_imp lthy5 alpha_result
 
   val _ = trace_msg (K "Proving respectfulness...")
   val raw_funs_rsp_aux = 
-    raw_fv_bn_rsp_aux alpha_trms alpha_bn_trms raw_fvs 
-      raw_bns raw_fv_bns alpha_induct (raw_bn_defs @ raw_fv_defs) lthy5
+    raw_fv_bn_rsp_aux lthy5 alpha_result raw_fvs raw_bns raw_fv_bns (raw_bn_defs @ raw_fv_defs) 
   
   val raw_funs_rsp = map mk_funs_rsp raw_funs_rsp_aux
 
   val raw_size_rsp = 
-    raw_size_rsp_aux (alpha_trms @ alpha_bn_trms) alpha_induct 
-      (raw_size_thms @ raw_size_eqvt) lthy5
+    raw_size_rsp_aux lthy5 alpha_result (raw_size_thms @ raw_size_eqvt)
       |> map mk_funs_rsp
 
   val raw_constrs_rsp = 
-    raw_constrs_rsp (flat raw_constrs) alpha_trms alpha_intros
-      (alpha_bn_imp_thms @ raw_funs_rsp_aux) lthy5 
+    raw_constrs_rsp lthy5 alpha_result (flat raw_constrs) (alpha_bn_imp_thms @ raw_funs_rsp_aux) 
     
   val alpha_permute_rsp = map mk_alpha_permute_rsp alpha_eqvt
 
   val alpha_bn_rsp = 
-    raw_alpha_bn_rsp alpha_bn_trms alpha_bn_equivp_thms alpha_bn_imp_thms
+    raw_alpha_bn_rsp alpha_result alpha_bn_equivp_thms alpha_bn_imp_thms
 
-  val raw_perm_bn_rsp =
-    raw_perm_bn_rsp (alpha_trms @ alpha_bn_trms) raw_perm_bns alpha_induct 
-      alpha_intros raw_perm_bn_simps lthy5
+  val raw_perm_bn_rsp =raw_perm_bn_rsp lthy5 alpha_result raw_perm_bns raw_perm_bn_simps
 
   (* noting the quot_respects lemmas *)
   val (_, lthy6) = 
@@ -321,7 +312,11 @@
   val qty_descr = map (fn (vs, bind, mx, _) => (vs, bind, mx)) dts
      
   val (qty_infos, lthy7) = 
-    define_qtypes qty_descr alpha_tys alpha_trms alpha_equivp_thms lthy6
+    let
+      val AlphaResult {alpha_trms, alpha_tys, ...} = alpha_result
+    in
+      define_qtypes qty_descr alpha_tys alpha_trms alpha_equivp_thms lthy6
+    end
 
   val qtys = map #qtyp qty_infos
   val qty_full_names = map (fst o dest_Type) qtys
@@ -341,7 +336,11 @@
     map2 (fn (b, _, _) => fn t => ("fv_" ^ Variable.check_name b, t, NoSyn)) bn_funs raw_fv_bns
 
   val qalpha_bns_descr = 
-    map2 (fn (b, _, _) => fn t => ("alpha_" ^ Variable.check_name b, t, NoSyn)) bn_funs  alpha_bn_trms
+    let
+      val AlphaResult {alpha_bn_trms, ...} = alpha_result 
+    in
+      map2 (fn (b, _, _) => fn t => ("alpha_" ^ Variable.check_name b, t, NoSyn)) bn_funs  alpha_bn_trms
+    end
 
   val qperm_descr =
     map2 (fn n => fn t => ("permute_" ^ n, Type.legacy_freeze t, NoSyn)) qty_names raw_perm_funs
@@ -484,7 +483,6 @@
      ||>> Local_Theory.note ((thms_suffix "fsupp", []), qfsupp_thms)
      ||>> Local_Theory.note ((thms_suffix "supp", []), qsupp_constrs)
      ||>> Local_Theory.note ((thms_suffix "fresh", []), qfresh_constrs)
-     ||>> Local_Theory.note ((thms_suffix "raw_alpha", []), alpha_intros)
      ||>> Local_Theory.note ((thms_suffix "perm_bn_simps", []), qperm_bn_simps)
      ||>> Local_Theory.note ((thms_suffix "bn_finite", []), qbn_finite_thms)
      ||>> Local_Theory.note ((thms_suffix "perm_bn_alpha", []), qperm_bn_alpha_thms)

--- a/Nominal/nominal_dt_alpha.ML	Wed Jun 29 23:08:44 2011 +0100
+++ b/Nominal/nominal_dt_alpha.ML	Thu Jun 30 02:19:59 2011 +0100
@@ -10,8 +10,7 @@
   val comb_binders: Proof.context -> bmode -> term list -> (term option * int) list -> term
 
   val define_raw_alpha: string list -> typ list -> cns_info list -> bn_info list -> 
-    bclause list list list -> term list -> Proof.context -> 
-    term list * term list * thm list * thm list * thm * alpha_result * local_theory
+    bclause list list list -> term list -> Proof.context -> alpha_result * local_theory
 
   val induct_prove: typ list -> (typ * (term -> term)) list -> thm -> 
     (Proof.context -> int -> tactic) -> Proof.context -> thm list
@@ -26,14 +25,13 @@
   val raw_prove_trans: Proof.context -> alpha_result -> thm list -> thm list -> thm list
   val raw_prove_equivp: Proof.context -> alpha_result -> thm list -> thm list -> thm list -> 
     thm list * thm list
-  val raw_prove_bn_imp: term list -> term list -> thm list -> thm -> Proof.context -> thm list
-  val raw_fv_bn_rsp_aux: term list -> term list -> term list -> term list -> 
-    term list -> thm -> thm list -> Proof.context -> thm list
-  val raw_size_rsp_aux: term list -> thm -> thm list -> Proof.context -> thm list
-  val raw_constrs_rsp: term list -> term list -> thm list -> thm list -> Proof.context -> thm list
-  val raw_alpha_bn_rsp: term list -> thm list -> thm list -> thm list
-  val raw_perm_bn_rsp: term list -> term list -> thm -> thm list -> thm list -> 
-    Proof.context -> thm list
+  val raw_prove_bn_imp: Proof.context -> alpha_result -> thm list
+  val raw_fv_bn_rsp_aux: Proof.context -> alpha_result -> term list -> term list -> term list -> 
+    thm list -> thm list
+  val raw_size_rsp_aux: Proof.context -> alpha_result -> thm list -> thm list
+  val raw_constrs_rsp: Proof.context -> alpha_result -> term list -> thm list -> thm list
+  val raw_alpha_bn_rsp: alpha_result -> thm list -> thm list -> thm list
+  val raw_perm_bn_rsp: Proof.context -> alpha_result -> term list -> thm list -> thm list
   
   val mk_funs_rsp: thm -> thm
   val mk_alpha_permute_rsp: thm -> thm 
@@ -267,20 +265,14 @@
     val alpha_cases = map (Morphism.thm phi) alpha_cases_loc
 
     val (alpha_trms, alpha_bn_trms) = chop (length fvs) all_alpha_trms
-    val alpha_tys = 
-      alpha_trms
-      |> map fastype_of
-      |> map domain_type
-
-    val alpha_bn_tys = 
-      alpha_bn_trms
-      |> map fastype_of
-      |> map domain_type
+    
+    val alpha_tys = map (domain_type o fastype_of) alpha_trms
+    val alpha_bn_tys = map (domain_type o fastype_of) alpha_bn_trms
 
     val alpha_names = map (fst o dest_Const) alpha_trms  
     val alpha_bn_names = map (fst o dest_Const) alpha_bn_trms
-
-    val alpha_result = AlphaResult 
+  in
+    (AlphaResult
       {alpha_names = alpha_names,
        alpha_trms = alpha_trms,
        alpha_tys = alpha_tys,
@@ -289,9 +281,7 @@
        alpha_bn_tys = alpha_bn_tys, 
        alpha_intros = alpha_intros,
        alpha_cases = alpha_cases,
-       alpha_raw_induct = alpha_raw_induct}
-  in
-    (alpha_trms, alpha_bn_trms, alpha_intros, alpha_cases, alpha_raw_induct, alpha_result, lthy')
+       alpha_raw_induct = alpha_raw_induct}, lthy')
   end
 
 
@@ -645,11 +635,13 @@
 
 (* proves that alpha_raw implies alpha_bn *)
 
-fun raw_prove_bn_imp_tac pred_names alpha_intros ctxt = 
+fun raw_prove_bn_imp_tac alpha_result ctxt = 
   SUBPROOF (fn {prems, context, ...} => 
     let
+      val AlphaResult {alpha_names, alpha_intros, ...} = alpha_result 
+
       val prems' = flat (map Datatype_Aux.split_conj_thm prems)
-      val prems'' = map (transform_prem1 context pred_names) prems'
+      val prems'' = map (transform_prem1 context alpha_names) prems'
     in
       HEADGOAL 
         (REPEAT_ALL_NEW 
@@ -660,24 +652,28 @@
                      resolve_tac alpha_intros ]))
     end) ctxt
 
-fun raw_prove_bn_imp alpha_trms alpha_bn_trms alpha_intros alpha_induct ctxt =
+
+fun raw_prove_bn_imp ctxt alpha_result =
   let
+    val AlphaResult {alpha_trms, alpha_tys, alpha_bn_trms, alpha_raw_induct, ...} = alpha_result 
+
     val arg_ty = domain_type o fastype_of 
-    val alpha_names =  map (fst o dest_Const) alpha_trms
-    val ty_assoc = map (fn t => (arg_ty t, t)) alpha_trms
+    val ty_assoc = alpha_tys ~~ alpha_trms
     val props = map (fn t => (lookup ty_assoc (arg_ty t), fn (x, y) => t $ x $ y)) alpha_bn_trms
   in
-    alpha_prove (alpha_trms @ alpha_bn_trms) props alpha_induct 
-      (raw_prove_bn_imp_tac alpha_names alpha_intros) ctxt
+    alpha_prove (alpha_trms @ alpha_bn_trms) props alpha_raw_induct 
+      (raw_prove_bn_imp_tac alpha_result) ctxt
   end
 
 
 (* respectfulness for fv_raw / bn_raw *)
 
-fun raw_fv_bn_rsp_aux alpha_trms alpha_bn_trms fvs bns fv_bns alpha_induct simps ctxt =
+fun raw_fv_bn_rsp_aux ctxt alpha_result fvs bns fv_bns simps =
   let
-    val arg_ty = fst o dest_Type o domain_type o fastype_of 
-    val ty_assoc = map (fn t => (arg_ty t, t)) alpha_trms
+    val AlphaResult {alpha_trms, alpha_tys, alpha_bn_trms, alpha_raw_induct, ...} = alpha_result 
+
+    val arg_ty = domain_type o fastype_of 
+    val ty_assoc = alpha_tys ~~ alpha_trms
     fun mk_eq' t x y = HOLogic.mk_eq (t $ x, t $ y)
 
     val prop1 = map (fn t => (lookup ty_assoc (arg_ty t), fn (x, y) => mk_eq' t x y)) fvs
@@ -687,28 +683,29 @@
     val ss = HOL_ss addsimps (simps @ @{thms alphas prod_fv.simps set.simps append.simps} 
       @ @{thms Un_assoc Un_insert_left Un_empty_right Un_empty_left}) 
   in
-    alpha_prove (alpha_trms @ alpha_bn_trms) (prop1 @ prop2 @ prop3) alpha_induct 
+    alpha_prove (alpha_trms @ alpha_bn_trms) (prop1 @ prop2 @ prop3) alpha_raw_induct 
       (K (asm_full_simp_tac ss)) ctxt
   end
 
 
 (* respectfulness for size *)
 
-fun raw_size_rsp_aux all_alpha_trms alpha_induct simps ctxt =
+fun raw_size_rsp_aux ctxt alpha_result simps =
   let
-    val arg_tys = map (domain_type o fastype_of) all_alpha_trms
-
+    val AlphaResult {alpha_trms, alpha_tys, alpha_bn_trms, alpha_bn_tys, alpha_raw_induct, ...} = 
+      alpha_result 
+    
     fun mk_prop ty (x, y) = HOLogic.mk_eq 
       (HOLogic.size_const ty $ x, HOLogic.size_const ty $ y)
 
-    val props = map2 (fn trm => fn ty => (trm, mk_prop ty)) all_alpha_trms arg_tys 
+    val props = (alpha_trms @ alpha_bn_trms) ~~ (map mk_prop (alpha_tys @ alpha_bn_tys)) 
   
     val ss = HOL_ss addsimps (simps @ @{thms alphas prod_alpha_def prod_rel_def 
       permute_prod_def prod.cases prod.recs})
 
     val tac = (TRY o REPEAT o etac @{thm exE}) THEN' asm_full_simp_tac ss
   in
-    alpha_prove all_alpha_trms props alpha_induct (K tac) ctxt
+    alpha_prove (alpha_trms @ alpha_bn_trms) props alpha_raw_induct (K tac) ctxt
   end
 
 
@@ -726,12 +723,12 @@
     THEN_ALL_NEW (TRY o (rtac exi_zero) THEN' asm_full_simp_tac post_ss)
   end
 
-fun raw_constrs_rsp constrs alpha_trms alpha_intros simps ctxt =
+fun raw_constrs_rsp ctxt alpha_result constrs simps =
   let
-    val alpha_arg_tys = map (domain_type o fastype_of) alpha_trms
-  
+    val AlphaResult {alpha_trms, alpha_tys, alpha_intros, ...} = alpha_result 
+
     fun lookup ty = 
-      case AList.lookup (op=) (alpha_arg_tys ~~ alpha_trms) ty of
+      case AList.lookup (op=) (alpha_tys ~~ alpha_trms) ty of
         NONE => HOLogic.eq_const ty
       | SOME alpha => alpha 
   
@@ -763,8 +760,10 @@
 
 (* we have to reorder the alpha_bn_imps theorems in order
    to be in order with alpha_bn_trms *)
-fun raw_alpha_bn_rsp alpha_bn_trms alpha_bn_equivp alpha_bn_imps =
+fun raw_alpha_bn_rsp alpha_result alpha_bn_equivp alpha_bn_imps =
   let
+    val AlphaResult {alpha_bn_trms, ...} = alpha_result 
+
     fun mk_map thm =
       thm |> `prop_of
           |>> List.last  o snd o strip_comb
@@ -787,11 +786,12 @@
 val perm_bn_rsp = @{lemma "(!x y p. R x y --> R (f p x) (f p y)) ==> (op= ===> R ===> R) f f"
  by (simp add: fun_rel_def)}
 
-fun raw_prove_perm_bn_tac pred_names alpha_intros simps ctxt = 
+fun raw_prove_perm_bn_tac alpha_result simps ctxt = 
   SUBPROOF (fn {prems, context, ...} => 
     let
+      val AlphaResult {alpha_names, alpha_bn_names, alpha_intros, ...} = alpha_result 
       val prems' = flat (map Datatype_Aux.split_conj_thm prems)
-      val prems'' = map (transform_prem1 context pred_names) prems'
+      val prems'' = map (transform_prem1 context (alpha_names @ alpha_bn_names)) prems'
     in
       HEADGOAL 
         (simp_tac (HOL_basic_ss addsimps (simps @ prems'))
@@ -804,11 +804,13 @@
                      resolve_tac alpha_intros ]))
     end) ctxt
 
-fun raw_perm_bn_rsp alpha_trms perm_bns alpha_induct alpha_intros simps ctxt =
+fun raw_perm_bn_rsp ctxt alpha_result perm_bns simps =
   let
-    val arg_ty = domain_type o fastype_of
+    val AlphaResult {alpha_trms, alpha_tys, alpha_bn_trms, alpha_bn_tys, alpha_raw_induct, ...} = 
+      alpha_result 
+
     val perm_bn_ty = range_type o range_type o fastype_of
-    val ty_assoc = map (fn t => (arg_ty t, t)) alpha_trms
+    val ty_assoc = (alpha_tys @ alpha_bn_tys) ~~ (alpha_trms @ alpha_bn_trms)
 
     val ([p], ctxt') = Variable.variant_fixes ["p"] ctxt		   
     val p = Free (p, @{typ perm})
@@ -820,12 +822,10 @@
         (alpha_trm, fn (x, y) => alpha_trm $ (t $ p $ x) $ (t $ p $ y))
       end
 
-    val goals = map mk_prop perm_bns
-    val alpha_names =  map (fst o dest_Const) alpha_trms       
-    
+    val goals = map mk_prop perm_bns    
   in
-    alpha_prove alpha_trms goals alpha_induct 
-      (raw_prove_perm_bn_tac alpha_names alpha_intros simps) ctxt
+    alpha_prove (alpha_trms @ alpha_bn_trms) goals alpha_raw_induct 
+      (raw_prove_perm_bn_tac alpha_result simps) ctxt
      |> ProofContext.export ctxt' ctxt
      |> map atomize
      |> map single