tuning
authorblanchet
Thu, 06 Jun 2013 15:49:09 +0200
changeset 52320 597fcdb7ea64
parent 52319 37a3b00759dc
child 52321 30d516bbf19f
tuning
src/HOL/BNF/Tools/bnf_fp_def_sugar.ML
--- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Thu Jun 06 15:49:08 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Thu Jun 06 15:49:09 2013 +0200
@@ -47,17 +47,17 @@
 
   val mk_iter_fun_arg_typessss: typ list -> int list -> int list list -> term ->
     typ list list list list
-  val define_fold_rec:
+  val define_iters: string list ->
     (typ list list * typ list list list list * term list list * term list list list list) list ->
     (string -> binding) -> typ list -> typ list -> term list -> Proof.context ->
-    (term * term * thm * thm) * Proof.context
-  val define_unfold_corec: term list * term list list
+    (term list * thm list) * Proof.context
+  val define_coiters: term list * term list list
       * ((term list list * term list list list list * term list list list list)
          * (typ list * typ list list list * typ list list))
       * ((term list list * term list list list list * term list list list list)
          * (typ list * typ list list list * typ list list)) ->
     (string -> binding) -> typ list -> typ list -> term list -> Proof.context ->
-    (term * term * thm * thm) * Proof.context
+    (term list * thm list) * Proof.context
   val derive_induct_fold_rec_thms_for_types: BNF_Def.bnf list -> term list list ->
     (typ list list * typ list list list list * term list list * term list list list list) list ->
     thm -> thm list list -> BNF_Def.bnf list -> BNF_Def.bnf list -> typ list -> typ list ->
@@ -68,8 +68,8 @@
   val derive_coinduct_unfold_corec_thms_for_types: BNF_Def.bnf list -> term list -> term list ->
     thm -> thm -> thm list -> thm list -> thm list -> BNF_Def.bnf list -> BNF_Def.bnf list ->
     typ list -> typ list -> typ list -> int list list -> int list list -> int list ->
-    thm list list -> BNF_Ctr_Sugar.ctr_sugar list -> term list -> term list -> thm list ->
-    thm list -> local_theory ->
+    thm list list -> BNF_Ctr_Sugar.ctr_sugar list -> term list list -> thm list list ->
+    local_theory ->
     (thm * thm list * thm * thm list * Args.src list)
     * (thm list list * thm list list * Args.src list)
     * (thm list list * thm list list) * (thm list list * thm list list * Args.src list)
@@ -146,8 +146,8 @@
   Local_Theory.declaration {syntax = false, pervasive = true}
     (fn phi => Data.map (Symtab.update_new (key, morph_fp_sugar phi fp_sugar)));
 
-fun register_fp_sugars fp pre_bnfs (fp_res as {Ts, ...}) ctr_defss ctr_sugars un_folds co_recs
-    co_induct strong_co_induct un_fold_thmss co_rec_thmss lthy =
+fun register_fp_sugars fp pre_bnfs (fp_res as {Ts, ...}) ctr_defss ctr_sugars [un_folds, co_recs]
+    co_induct strong_co_induct [un_fold_thmss, co_rec_thmss] lthy =
   (0, lthy)
   |> fold (fn T as Type (s, _) => fn (kk, lthy) => (kk + 1,
     register_fp_sugar s {T = T, fp = fp, index = kk, pre_bnfs = pre_bnfs, fp_res = fp_res,
@@ -473,16 +473,15 @@
     Term.list_comb (dtor_coiter, map4 mk_preds_getterss_join cs cpss f_sum_prod_Ts cqfsss)
   end;
 
-fun define_fold_rec [fold_args_types, rec_args_types] mk_binding fpTs Cs [ctor_fold, ctor_rec]
-    lthy0 =
+fun define_iters iterNs iter_args_typess mk_binding fpTs Cs ctor_iters lthy0 =
   let
     val thy = Proof_Context.theory_of lthy0;
 
     val nn = length fpTs;
 
-    val fpT_to_C as Type (_, [fpT, _]) = snd (strip_typeN nn (fastype_of ctor_fold));
+    val fpT_to_C as Type (_, [fpT, _]) = snd (strip_typeN nn (fastype_of (hd ctor_iters)));
 
-    fun generate_iter (suf, ctor_iter, (f_Tss, _, fss, xssss)) =
+    fun generate_iter suf (f_Tss, _, fss, xssss) ctor_iter =
       let
         val res_T = fold_rev (curry (op --->)) f_Tss fpT_to_C;
         val b = mk_binding suf;
@@ -491,8 +490,7 @@
             mk_iter_body ctor_iter fss xssss);
       in (b, spec) end;
 
-    val binding_specs =
-      map generate_iter [(foldN, ctor_fold, fold_args_types), (recN, ctor_rec, rec_args_types)];
+    val binding_specs = map3 generate_iter iterNs iter_args_typess ctor_iters;
 
     val ((csts, defs), (lthy', lthy)) = lthy0
       |> apfst split_list o fold_map (fn (b, spec) =>
@@ -502,15 +500,15 @@
 
     val phi = Proof_Context.export_morphism lthy lthy';
 
-    val [fold_def, rec_def] = map (Morphism.thm phi) defs;
+    val iter_defs = map (Morphism.thm phi) defs;
 
-    val [foldx, recx] = map (mk_co_iter thy Least_FP fpT Cs o Morphism.term phi) csts;
+    val iters = map (mk_co_iter thy Least_FP fpT Cs o Morphism.term phi) csts;
   in
-    ((foldx, recx, fold_def, rec_def), lthy')
+    ((iters, iter_defs), lthy')
   end;
 
 (* TODO: merge with above function? *)
-fun define_unfold_corec (cs, cpss, unfold_args_types, corec_args_types) mk_binding fpTs Cs
+fun define_coiters (cs, cpss, unfold_args_types, corec_args_types) mk_binding fpTs Cs
     [dtor_unfold, dtor_corec] lthy0 =
   let
     val thy = Proof_Context.theory_of lthy0;
@@ -541,12 +539,12 @@
 
     val phi = Proof_Context.export_morphism lthy lthy';
 
-    val [unfold_def, corec_def] = map (Morphism.thm phi) defs;
+    val coiter_defs = map (Morphism.thm phi) defs;
 
-    val [unfold, corec] = map (mk_co_iter thy Greatest_FP fpT Cs o Morphism.term phi) csts;
+    val coiters = map (mk_co_iter thy Greatest_FP fpT Cs o Morphism.term phi) csts;
   in
-    ((unfold, corec, unfold_def, corec_def), lthy')
-  end ;
+    ((coiters, coiter_defs), lthy')
+  end;
 
 fun derive_induct_fold_rec_thms_for_types pre_bnfs [ctor_folds, ctor_recs]
     [fold_args_types, rec_args_types] ctor_induct [ctor_fold_thms, ctor_rec_thms] nesting_bnfs
@@ -704,7 +702,7 @@
 
 fun derive_coinduct_unfold_corec_thms_for_types pre_bnfs dtor_unfolds dtor_corecs dtor_coinduct
     dtor_strong_induct dtor_ctors dtor_unfold_thms dtor_corec_thms nesting_bnfs nested_bnfs fpTs Cs
-    As kss mss ns ctr_defss ctr_sugars unfolds corecs unfold_defs corec_defs lthy =
+    As kss mss ns ctr_defss ctr_sugars [unfolds, corecs] [unfold_defs, corec_defs] lthy =
   let
     val nn = length pre_bnfs;
 
@@ -1318,16 +1316,16 @@
         (wrap_ctrs
          #> derive_maps_sets_rels
          ##>>
-           (if fp = Least_FP then define_fold_rec (the fold_rec_args_types)
-            else define_unfold_corec (the unfold_corec_args_types))
+           (if fp = Least_FP then define_iters [foldN, recN] (the fold_rec_args_types)
+            else define_coiters (the unfold_corec_args_types))
              mk_binding fpTs Cs [xtor_un_fold, xtor_co_rec]
          #> massage_res, lthy')
       end;
 
     fun wrap_types_etc (wrap_types_etcs, lthy) =
       fold_map I wrap_types_etcs lthy
-      |>> apsnd split_list4 o apfst (apsnd split_list4 o apfst split_list4 o split_list)
-        o split_list;
+      |>> apsnd (apsnd transpose o apfst transpose o split_list)
+        o apfst (apsnd split_list4 o apfst split_list4 o split_list) o split_list;
 
     val mk_simp_thmss =
       map7 (fn {injects, distincts, case_thms, ...} => fn un_folds => fn co_recs =>
@@ -1337,14 +1335,13 @@
 
     fun derive_and_note_induct_fold_rec_thms_for_types
         ((((mapsx, rel_injects, rel_distincts, setss), (ctrss, _, ctr_defss, ctr_sugars)),
-          (folds, recs, fold_defs, rec_defs)), lthy) =
+          (iterss, iter_defss)), lthy) =
       let
         val ((induct_thm, induct_thms, induct_attrs), (fold_thmss, fold_attrs),
              (rec_thmss, rec_attrs)) =
           derive_induct_fold_rec_thms_for_types pre_bnfs [xtor_un_folds, xtor_co_recs]
             (the fold_rec_args_types) xtor_co_induct [xtor_un_fold_thms, xtor_co_rec_thms]
-            nesting_bnfs nested_bnfs fpTs Cs Xs ctrXs_Tsss ctrss ctr_defss [folds, recs]
-            [fold_defs, rec_defs] lthy;
+            nesting_bnfs nested_bnfs fpTs Cs Xs ctrXs_Tsss ctrss ctr_defss iterss iter_defss lthy;
 
         val induct_type_attr = Attrib.internal o K o Induct.induct_type;
 
@@ -1364,13 +1361,13 @@
       in
         lthy
         |> Local_Theory.notes (common_notes @ notes) |> snd
-        |> register_fp_sugars Least_FP pre_bnfs fp_res ctr_defss ctr_sugars folds recs induct_thm
-          induct_thm fold_thmss rec_thmss
+        |> register_fp_sugars Least_FP pre_bnfs fp_res ctr_defss ctr_sugars iterss induct_thm
+          induct_thm [fold_thmss, rec_thmss]
       end;
 
     fun derive_and_note_coinduct_unfold_corec_thms_for_types
         ((((mapsx, rel_injects, rel_distincts, setss), (_, _, ctr_defss, ctr_sugars)),
-          (unfolds, corecs, unfold_defs, corec_defs)), lthy) =
+          (coiterss, coiter_defss)), lthy) =
       let
         val ((coinduct_thm, coinduct_thms, strong_coinduct_thm, strong_coinduct_thms,
               coinduct_attrs),
@@ -1381,8 +1378,8 @@
              (sel_unfold_thmss, sel_corec_thmss, sel_coiter_attrs)) =
           derive_coinduct_unfold_corec_thms_for_types pre_bnfs xtor_un_folds xtor_co_recs
             xtor_co_induct xtor_strong_co_induct dtor_ctors xtor_un_fold_thms xtor_co_rec_thms
-            nesting_bnfs nested_bnfs fpTs Cs As kss mss ns ctr_defss ctr_sugars unfolds corecs
-            unfold_defs corec_defs lthy;
+            nesting_bnfs nested_bnfs fpTs Cs As kss mss ns ctr_defss ctr_sugars coiterss
+            coiter_defss lthy;
 
         val coinduct_type_attr = Attrib.internal o K o Induct.coinduct_type;
 
@@ -1424,8 +1421,8 @@
       in
         lthy
         |> Local_Theory.notes (anonymous_notes @ common_notes @ notes) |> snd
-        |> register_fp_sugars Greatest_FP pre_bnfs fp_res ctr_defss ctr_sugars unfolds corecs
-          coinduct_thm strong_coinduct_thm unfold_thmss corec_thmss
+        |> register_fp_sugars Greatest_FP pre_bnfs fp_res ctr_defss ctr_sugars coiterss coinduct_thm
+          strong_coinduct_thm [unfold_thmss, corec_thmss]
       end;
 
     val lthy' = lthy