include map theorems in datastructure for "primcorec"

--- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Mon Sep 09 13:47:58 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Mon Sep 09 14:22:11 2013 +0200
@@ -18,6 +18,7 @@
      ctr_defss: thm list list,
      ctr_sugars: BNF_Ctr_Sugar.ctr_sugar list,
      co_iterss: term list list,
+     mapss: thm list list,
      co_inducts: thm list,
      co_iter_thmsss: thm list list list,
      disc_co_itersss: thm list list list,
@@ -120,6 +121,7 @@
    ctr_defss: thm list list,
    ctr_sugars: ctr_sugar list,
    co_iterss: term list list,
+   mapss: thm list list,
    co_inducts: thm list,
    co_iter_thmsss: thm list list list,
    disc_co_itersss: thm list list list,
@@ -132,13 +134,14 @@
   T1 = T2 andalso fp1 = fp2 andalso index1 = index2 andalso eq_fp_result (fp_res1, fp_res2);
 
 fun morph_fp_sugar phi {T, fp, index, pre_bnfs, nested_bnfs, nesting_bnfs, fp_res, ctr_defss,
-    ctr_sugars, co_iterss, co_inducts, co_iter_thmsss, disc_co_itersss, sel_co_iterssss} =
+    ctr_sugars, co_iterss, mapss, co_inducts, co_iter_thmsss, disc_co_itersss, sel_co_iterssss} =
   {T = Morphism.typ phi T, fp = fp, index = index, pre_bnfs = map (morph_bnf phi) pre_bnfs,
     nested_bnfs = map (morph_bnf phi) nested_bnfs, nesting_bnfs = map (morph_bnf phi) nesting_bnfs,
    fp_res = morph_fp_result phi fp_res,
    ctr_defss = map (map (Morphism.thm phi)) ctr_defss,
    ctr_sugars = map (morph_ctr_sugar phi) ctr_sugars,
    co_iterss = map (map (Morphism.term phi)) co_iterss,
+   mapss = map (map (Morphism.thm phi)) mapss,
    co_inducts = map (Morphism.thm phi) co_inducts,
    co_iter_thmsss = map (map (map (Morphism.thm phi))) co_iter_thmsss,
    disc_co_itersss = map (map (map (Morphism.thm phi))) disc_co_itersss,
@@ -167,12 +170,12 @@
     (fn phi => Data.map (Symtab.default (key, morph_fp_sugar phi fp_sugar)));
 
 fun register_fp_sugars fp pre_bnfs nested_bnfs nesting_bnfs (fp_res as {Ts, ...}) ctr_defss
-    ctr_sugars co_iterss co_inducts co_iter_thmsss disc_co_itersss sel_co_iterssss lthy =
+    ctr_sugars co_iterss mapss co_inducts co_iter_thmsss disc_co_itersss sel_co_iterssss 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,
         nested_bnfs = nested_bnfs, nesting_bnfs = nesting_bnfs, fp_res = fp_res,
-        ctr_defss = ctr_defss, ctr_sugars = ctr_sugars, co_iterss = co_iterss,
+        ctr_defss = ctr_defss, ctr_sugars = ctr_sugars, co_iterss = co_iterss, mapss = mapss,
         co_inducts = co_inducts, co_iter_thmsss = co_iter_thmsss, disc_co_itersss = disc_co_itersss,
         sel_co_iterssss = sel_co_iterssss}
       lthy)) Ts
@@ -1414,7 +1417,7 @@
           @ rel_distincts @ flat setss);
 
     fun derive_and_note_induct_iters_thms_for_types
-        ((((mapsx, rel_injects, rel_distincts, setss), (ctrss, _, ctr_defss, ctr_sugars)),
+        ((((mapss, rel_injects, rel_distincts, setss), (ctrss, _, ctr_defss, ctr_sugars)),
           (iterss, iter_defss)), lthy) =
       let
         val ((induct_thms, induct_thm, induct_attrs), (fold_thmss, fold_attrs),
@@ -1426,7 +1429,7 @@
         val induct_type_attr = Attrib.internal o K o Induct.induct_type;
 
         val simp_thmss =
-          mk_simp_thmss ctr_sugars fold_thmss rec_thmss mapsx rel_injects rel_distincts setss;
+          mk_simp_thmss ctr_sugars fold_thmss rec_thmss mapss rel_injects rel_distincts setss;
 
         val common_notes =
           (if nn > 1 then [(inductN, [induct_thm], induct_attrs)] else [])
@@ -1442,11 +1445,11 @@
         lthy
         |> Local_Theory.notes (common_notes @ notes) |> snd
         |> register_fp_sugars Least_FP pre_bnfs nested_bnfs nesting_bnfs fp_res ctr_defss ctr_sugars
-          iterss [induct_thm] (transpose [fold_thmss, rec_thmss]) [] []
+          iterss mapss [induct_thm] (transpose [fold_thmss, rec_thmss]) [] []
       end;
 
     fun derive_and_note_coinduct_coiters_thms_for_types
-        ((((mapsx, rel_injects, rel_distincts, setss), (_, _, ctr_defss, ctr_sugars)),
+        ((((mapss, rel_injects, rel_distincts, setss), (_, _, ctr_defss, ctr_sugars)),
           (coiterss, coiter_defss)), lthy) =
       let
         val (([(coinduct_thms, coinduct_thm), (strong_coinduct_thms, strong_coinduct_thm)],
@@ -1472,7 +1475,7 @@
           mk_simp_thmss ctr_sugars
             (map3 flat_coiter_thms safe_unfold_thmss disc_unfold_thmss sel_unfold_thmss)
             (map3 flat_coiter_thms safe_corec_thmss disc_corec_thmss sel_corec_thmss)
-            mapsx rel_injects rel_distincts setss;
+            mapss rel_injects rel_distincts setss;
 
         val anonymous_notes =
           [(flat safe_unfold_thmss @ flat safe_corec_thmss, simp_attrs)]
@@ -1504,7 +1507,7 @@
         lthy
         |> Local_Theory.notes (anonymous_notes @ common_notes @ notes) |> snd
         |> register_fp_sugars Greatest_FP pre_bnfs nested_bnfs nesting_bnfs fp_res ctr_defss
-          ctr_sugars coiterss [coinduct_thm, strong_coinduct_thm]
+          ctr_sugars coiterss mapss [coinduct_thm, strong_coinduct_thm]
           (transpose [unfold_thmss, corec_thmss]) (transpose [disc_unfold_thmss, disc_corec_thmss])
           (transpose [sel_unfold_thmsss, sel_corec_thmsss])
       end;

--- a/src/HOL/BNF/Tools/bnf_fp_n2m_sugar.ML	Mon Sep 09 13:47:58 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_n2m_sugar.ML	Mon Sep 09 14:22:11 2013 +0200
@@ -59,6 +59,7 @@
         end;
 
       val ctr_defss = map (of_fp_sugar #ctr_defss) fp_sugars0;
+      val mapss = map (of_fp_sugar #mapss) fp_sugars0;
       val ctr_sugars0 = map2 target_ctr_sugar_of_fp_sugar fpTs fp_sugars0;
 
       val ctrss = map #ctrs ctr_sugars0;
@@ -168,7 +169,7 @@
       fun mk_target_fp_sugar (kk, T) =
         {T = T, fp = fp, index = kk, pre_bnfs = pre_bnfs, nested_bnfs = nested_bnfs,
          nesting_bnfs = nesting_bnfs, fp_res = fp_res, ctr_defss = ctr_defss,
-         ctr_sugars = ctr_sugars, co_inducts = co_inducts, co_iterss = co_iterss,
+         ctr_sugars = ctr_sugars, co_iterss = co_iterss, mapss = mapss, co_inducts = co_inducts,
          co_iter_thmsss = transpose [un_fold_thmss, co_rec_thmss],
          disc_co_itersss = transpose [disc_unfold_thmss, disc_corec_thmss],
          sel_co_iterssss = transpose [sel_unfold_thmsss, sel_corec_thmsss]}

--- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML	Mon Sep 09 13:47:58 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML	Mon Sep 09 14:22:11 2013 +0200
@@ -272,6 +272,18 @@
 
 fun find_index_eq hs h = find_index (curry (op =) h) hs;
 
+(*FIXME: remove special cases for products and sum once they are registered as datatypes*)
+fun map_thms_of_typ ctxt (Type (s, _)) =
+    if s = @{type_name prod} then
+      @{thms map_pair_simp}
+    else if s = @{type_name sum} then
+      @{thms sum_map.simps}
+    else
+      (case fp_sugar_of ctxt s of
+        SOME {index, mapss, ...} => nth mapss index
+      | NONE => [])
+  | map_thms_of_typ _ _ = [];
+
 val lose_co_rec = false (*FIXME: try true?*);
 
 fun rec_specs_of bs arg_Ts res_Ts get_indices callssss0 lthy =
@@ -361,7 +373,7 @@
 
     val ((nontriv, missing_res_Ts, perm0_kks,
           fp_sugars as {nested_bnfs, fp_res = {xtor_co_iterss = dtor_coiters1 :: _, ...},
-          co_inducts = coinduct_thms, ...} :: _), lthy') =
+            co_inducts = coinduct_thms, ...} :: _), lthy') =
       nested_to_mutual_fps lose_co_rec Greatest_FP bs res_Ts get_indices callssss0 lthy;
 
     val perm_fp_sugars = sort (int_ord o pairself #index) fp_sugars;
@@ -446,7 +458,7 @@
           disc_co_itersss = disc_coitersss, sel_co_iterssss = sel_coiterssss, ...}
         p_is q_isss f_isss f_Tsss =
       {corec = mk_co_iter thy Greatest_FP (substAT T) perm_Cs' (co_rec_of (nth coiterss index)),
-       nested_maps = [] (*FIXME*),
+       nested_maps = maps (map_thms_of_typ lthy o T_of_bnf) nested_bnfs,
        nested_map_idents = map (unfold_thms lthy [id_def] o map_id0_of_bnf) nested_bnfs,
        nested_map_comps = map map_comp_of_bnf nested_bnfs,
        ctr_specs = mk_ctr_specs index ctr_sugars p_is q_isss f_isss f_Tsss coiter_thmsss