# HG changeset patch
# User blanchet
# Date 1347131066 -7200
# Node ID 1c5d6e2eb0c64d3f1e98a50d86868464b800ada2
# Parent  2a3cb4c71b8708bc867d95679f794d25f55eb43e
tuning

diff -r 2a3cb4c71b87 -r 1c5d6e2eb0c6 src/HOL/Codatatype/Tools/bnf_fp_sugar.ML
--- a/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Sat Sep 08 21:04:26 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Sat Sep 08 21:04:26 2012 +0200
@@ -47,9 +47,6 @@
 
 fun tick v f = Term.lambda v (HOLogic.mk_prod (v, f $ v))
 
-fun popescu_zip [] [fs] = fs
-  | popescu_zip (p :: ps) (fs :: fss) = p :: fs @ popescu_zip ps fss;
-
 fun cannot_merge_types () = error "Mutually recursive types must have the same type parameters";
 
 fun merge_type_arg_constrained ctxt (T, c) (T', c') =
@@ -190,9 +187,9 @@
         if member (op =) Cs U then Us else [T]
       | dest_rec_pair T = [T];
 
-    val (((gss, g_Tss, ysss), (hss, h_Tss, zssss)),
-         (cs, cpss, p_Tss, coiter_extra as ((pgss, cgsss), g_sum_prod_Ts, g_prod_Tss, g_Tsss),
-          corec_extra as ((phss, chsss), h_sum_prod_Ts, h_prod_Tss, h_Tsss))) =
+    val ((iter_only as (gss, g_Tss, yssss), rec_only as (hss, h_Tss, zssss)),
+         (cs, cpss, p_Tss, coiter_only as ((pgss, cgsss), g_sum_prod_Ts, g_prod_Tss, g_Tsss),
+          corec_only as ((phss, chsss), h_sum_prod_Ts, h_prod_Tss, h_Tsss))) =
       if lfp then
         let
           val y_Tsss =
@@ -215,7 +212,7 @@
             lthy
             |> mk_Freessss "x" z_Tssss;
         in
-          (((gss, g_Tss, ysss), (hss, h_Tss, zssss)),
+          (((gss, g_Tss, map (map (map single)) ysss), (hss, h_Tss, zssss)),
            ([], [], [], (([], []), [], [], []), (([], []), [], [], [])))
         end
       else
@@ -223,6 +220,9 @@
           val p_Tss =
             map2 (fn C => fn n => replicate (Int.max (0, n - 1)) (C --> HOLogic.boolT)) Cs ns;
 
+          fun popescu_zip [] [fs] = fs
+            | popescu_zip (p :: ps) (fs :: fss) = p :: fs @ popescu_zip ps fss;
+
           fun mk_types fun_Ts =
             let
               val f_sum_prod_Ts = map range_type fun_Ts;
@@ -338,36 +338,37 @@
         fun some_lfp_sugar no_defs_lthy =
           let
             val fpT_to_C = fpT --> C;
-            val iter_T = fold_rev (curry (op --->)) g_Tss fpT_to_C;
-            val rec_T = fold_rev (curry (op --->)) h_Tss fpT_to_C;
 
-            val iter_binder = Binding.suffix_name ("_" ^ iterN) b;
-            val rec_binder = Binding.suffix_name ("_" ^ recN) b;
+            fun generate_iter_like (suf, fp_iter_like, (fss, f_Tss, xssss)) =
+              let
+                val res_T = fold_rev (curry (op --->)) f_Tss fpT_to_C;
+
+                val binder = Binding.suffix_name ("_" ^ suf) b;
 
-            val iter_spec =
-              mk_Trueprop_eq (lists_bmoc gss (Free (Binding.name_of iter_binder, iter_T)),
-                Term.list_comb (fp_iter, map2 (mk_sum_caseN oo map2 mk_uncurried_fun) gss ysss));
-            val rec_spec =
-              mk_Trueprop_eq (lists_bmoc hss (Free (Binding.name_of rec_binder, rec_T)),
-                Term.list_comb (fp_rec, map2 (mk_sum_caseN oo map2 mk_uncurried2_fun) hss zssss));
+                val spec =
+                  mk_Trueprop_eq (lists_bmoc fss (Free (Binding.name_of binder, res_T)),
+                    Term.list_comb (fp_iter_like,
+                      map2 (mk_sum_caseN oo map2 mk_uncurried2_fun) fss xssss));
+              in (binder, spec) end;
 
-            val (([raw_iter, raw_rec], [raw_iter_def, raw_rec_def]), (lthy', lthy)) = no_defs_lthy
+            val iter_likes =
+              [(iterN, fp_iter, iter_only),
+               (recN, fp_rec, rec_only)];
+
+            val (binders, specs) = map generate_iter_like iter_likes |> split_list;
+
+            val ((csts, defs), (lthy', lthy)) = no_defs_lthy
               |> apfst split_list o fold_map2 (fn b => fn spec =>
                 Specification.definition (SOME (b, NONE, NoSyn), ((Thm.def_binding b, []), spec))
-                #>> apsnd snd) [iter_binder, rec_binder] [iter_spec, rec_spec]
+                #>> apsnd snd) binders specs
               ||> `Local_Theory.restore;
 
             (*transforms defined frees into consts (and more)*)
             val phi = Proof_Context.export_morphism lthy lthy';
 
-            val iter_def = Morphism.thm phi raw_iter_def;
-            val rec_def = Morphism.thm phi raw_rec_def;
+            val [iter_def, rec_def] = map (Morphism.thm phi) defs;
 
-            val iter0 = Morphism.term phi raw_iter;
-            val rec0 = Morphism.term phi raw_rec;
-
-            val iter = mk_iter_like As Cs iter0;
-            val recx = mk_iter_like As Cs rec0;
+            val [iter, recx] = map (mk_iter_like As Cs o Morphism.term phi) csts;
           in
             ((ctrs, iter, recx, v, xss, ctr_defs, iter_def, rec_def), lthy)
           end;
@@ -383,19 +384,19 @@
 
                 val binder = Binding.suffix_name ("_" ^ suf) b;
 
-                fun mk_join c n cps sum_prod_T prod_Ts cfss =
+                fun mk_popescu_join c n cps sum_prod_T prod_Ts cfss =
                   Term.lambda c (mk_IfN sum_prod_T cps
                     (map2 (mk_InN prod_Ts) (map HOLogic.mk_tuple cfss) (1 upto n)));
 
                 val spec =
                   mk_Trueprop_eq (lists_bmoc pfss (Free (Binding.name_of binder, res_T)),
                     Term.list_comb (fp_iter_like,
-                      map6 mk_join cs ns cpss f_sum_prod_Ts f_prod_Tss cfsss));
+                      map6 mk_popescu_join cs ns cpss f_sum_prod_Ts f_prod_Tss cfsss));
               in (binder, spec) end;
 
             val coiter_likes =
-              [(coiterN, fp_iter, coiter_extra),
-               (corecN, fp_rec, corec_extra)];
+              [(coiterN, fp_iter, coiter_only),
+               (corecN, fp_rec, corec_only)];
 
             val (binders, specs) = map generate_coiter_like coiter_likes |> split_list;
 
@@ -437,7 +438,7 @@
               fold_rev (fold_rev Logic.all) (xs :: fss)
                 (mk_Trueprop_eq (fiter_like $ xctr, Term.list_comb (f, fxs)));
 
-            fun build_iter_like fiter_likes maybe_tick =
+            fun build_call fiter_likes maybe_tick =
               let
                 fun build (T, U) =
                   if T = U then
@@ -459,9 +460,9 @@
 
             fun repair_calls fiter_likes maybe_cons maybe_tick maybe_prodT (x as Free (_, T)) =
               if member (op =) fpTs T then
-                maybe_cons x [build_iter_like fiter_likes (K I) (T, mk_U (K I) T) $ x]
+                maybe_cons x [build_call fiter_likes (K I) (T, mk_U (K I) T) $ x]
               else if exists_subtype (member (op =) fpTs) T then
-                [build_iter_like fiter_likes maybe_tick (T, mk_U maybe_prodT T) $ x]
+                [build_call fiter_likes maybe_tick (T, mk_U maybe_prodT T) $ x]
               else
                 [x];
 
@@ -512,11 +513,11 @@
                 (Logic.list_implies (seq_conds mk_cond n k cps,
                    mk_Trueprop_eq (fcoiter_like $ c, Term.list_comb (ctr, cfs'))));
 
-            fun repair_coiter_like_call fcoiter_likes (cf as Free (_, Type (_, [_, T])) $ _) =
+            fun repair_call fcoiter_likes (cf as Free (_, Type (_, [_, T])) $ _) =
               (case find_index (curry (op =) T) Cs of ~1 => cf | j => nth fcoiter_likes j $ cf);
 
-            val cgsss = map (map (map (repair_coiter_like_call gcoiters))) cgsss;
-            val chsss = map (map (map (repair_coiter_like_call hcorecs))) chsss;
+            val cgsss = map (map (map (repair_call gcoiters))) cgsss;
+            val chsss = map (map (map (repair_call hcorecs))) chsss;
 
             val goal_coiterss =
               map7 (map3 oooo mk_goal_coiter_like pgss) cs cpss gcoiters ns kss ctrss cgsss;