refactor fp_sugar move theorems

--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Fri Sep 26 14:43:26 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Fri Sep 26 14:43:28 2014 +0200
@@ -14,7 +14,8 @@
      ctr_sugar: Ctr_Sugar.ctr_sugar}
 
   type fp_bnf_sugar =
-    {rel_injects: thm list,
+    {map_thms: thm list,
+     rel_injects: thm list,
      rel_distincts: thm list}
 
   type fp_co_induct_sugar =
@@ -37,7 +38,6 @@
      absT_info: BNF_Comp.absT_info,
      fp_nesting_bnfs: BNF_Def.bnf list,
      live_nesting_bnfs: BNF_Def.bnf list,
-     maps: thm list,
      fp_ctr_sugar: fp_ctr_sugar,
      fp_bnf_sugar: fp_bnf_sugar,
      fp_co_induct_sugar: fp_co_induct_sugar};
@@ -163,11 +163,12 @@
 type fp_ctr_sugar =
   {ctrXs_Tss: typ list list,
    ctr_defs: thm list,
-   ctr_sugar: Ctr_Sugar.ctr_sugar}
+   ctr_sugar: Ctr_Sugar.ctr_sugar};
 
 type fp_bnf_sugar =
-  {rel_injects: thm list,
-   rel_distincts: thm list}
+  {map_thms: thm list,
+   rel_injects: thm list,
+   rel_distincts: thm list};
 
 type fp_co_induct_sugar =
   {co_rec: term,
@@ -176,7 +177,7 @@
    co_rec_def: thm,
    co_rec_thms: thm list,
    co_rec_discs: thm list,
-   co_rec_selss: thm list list}
+   co_rec_selss: thm list list};
 
 type fp_sugar =
   {T: typ,
@@ -189,14 +190,14 @@
    absT_info: absT_info,
    fp_nesting_bnfs: bnf list,
    live_nesting_bnfs: bnf list,
-   maps: thm list,
    fp_ctr_sugar: fp_ctr_sugar,
    fp_bnf_sugar: fp_bnf_sugar,
    fp_co_induct_sugar: fp_co_induct_sugar};
 
-fun morph_fp_bnf_sugar phi ({rel_injects, rel_distincts} : fp_bnf_sugar) =
-  {rel_injects = map (Morphism.thm phi) rel_injects,
-   rel_distincts = map (Morphism.thm phi) rel_distincts}
+fun morph_fp_bnf_sugar phi ({map_thms, rel_injects, rel_distincts} : fp_bnf_sugar) =
+  {map_thms = map (Morphism.thm phi) map_thms,
+   rel_injects = map (Morphism.thm phi) rel_injects,
+   rel_distincts = map (Morphism.thm phi) rel_distincts};
 
 fun morph_fp_co_induct_sugar phi ({co_rec, common_co_inducts, co_inducts, co_rec_def, co_rec_thms,
     co_rec_discs, co_rec_selss} : fp_co_induct_sugar) =
@@ -206,15 +207,15 @@
    co_rec_def = Morphism.thm phi co_rec_def,
    co_rec_thms = map (Morphism.thm phi) co_rec_thms,
    co_rec_discs = map (Morphism.thm phi) co_rec_discs,
-   co_rec_selss = map (map (Morphism.thm phi)) co_rec_selss}
+   co_rec_selss = map (map (Morphism.thm phi)) co_rec_selss};
 
 fun morph_fp_ctr_sugar phi ({ctrXs_Tss, ctr_defs, ctr_sugar} : fp_ctr_sugar) =
   {ctrXs_Tss = map (map (Morphism.typ phi)) ctrXs_Tss,
    ctr_defs = map (Morphism.thm phi) ctr_defs,
-   ctr_sugar = morph_ctr_sugar phi ctr_sugar}
+   ctr_sugar = morph_ctr_sugar phi ctr_sugar};
 
 fun morph_fp_sugar phi ({T, BT, X, fp, fp_res, fp_res_index, pre_bnf, absT_info, fp_nesting_bnfs,
-    live_nesting_bnfs, maps, fp_ctr_sugar, fp_bnf_sugar,
+    live_nesting_bnfs, fp_ctr_sugar, fp_bnf_sugar,
     fp_co_induct_sugar} : fp_sugar) =
   {T = Morphism.typ phi T,
    BT = Morphism.typ phi BT,
@@ -226,7 +227,6 @@
    absT_info = morph_absT_info phi absT_info,
    fp_nesting_bnfs = map (morph_bnf phi) fp_nesting_bnfs,
    live_nesting_bnfs = map (morph_bnf phi) live_nesting_bnfs,
-   maps = map (Morphism.thm phi) maps,
    fp_ctr_sugar = morph_fp_ctr_sugar phi fp_ctr_sugar,
    fp_bnf_sugar = morph_fp_bnf_sugar phi fp_bnf_sugar,
    fp_co_induct_sugar = morph_fp_co_induct_sugar phi fp_co_induct_sugar};
@@ -279,7 +279,7 @@
   register_fp_sugars_raw fp_sugars #> interpret_fp_sugars plugins fp_sugars;
 
 fun interpret_bnfs_register_fp_sugars plugins Ts BTs Xs fp pre_bnfs absT_infos fp_nesting_bnfs
-    live_nesting_bnfs fp_res ctrXs_Tsss ctr_defss ctr_sugars co_recs co_rec_defs mapss
+    live_nesting_bnfs fp_res ctrXs_Tsss ctr_defss ctr_sugars co_recs co_rec_defs map_thmss
     common_co_inducts co_inductss co_rec_thmss co_rec_discss co_rec_selsss rel_injectss
     rel_distinctss noted =
   let
@@ -288,13 +288,13 @@
         {T = T, BT = nth BTs kk, X = nth Xs kk, fp = fp, fp_res = fp_res, fp_res_index = kk,
          pre_bnf = nth pre_bnfs kk, absT_info = nth absT_infos kk,
          fp_nesting_bnfs = fp_nesting_bnfs, live_nesting_bnfs = live_nesting_bnfs,
-         maps = nth mapss kk,
          fp_ctr_sugar =
            {ctrXs_Tss = nth ctrXs_Tsss kk,
             ctr_defs = nth ctr_defss kk,
             ctr_sugar = nth ctr_sugars kk},
          fp_bnf_sugar =
-           {rel_injects = nth rel_injectss kk,
+           {map_thms = nth map_thmss kk,
+            rel_injects = nth rel_injectss kk,
             rel_distincts = nth rel_distinctss kk},
          fp_co_induct_sugar =
            {co_rec = nth co_recs kk,
@@ -2048,9 +2048,9 @@
       |>> apsnd split_list o apfst (apsnd split_list4 o apfst split_list4 o split_list)
         o split_list;
 
-    fun mk_simp_thms ({injects, distincts, case_thms, ...} : ctr_sugar) co_recs mapsx rel_injects
+    fun mk_simp_thms ({injects, distincts, case_thms, ...} : ctr_sugar) co_recs map_thms rel_injects
         rel_distincts setss =
-      injects @ distincts @ case_thms @ co_recs @ mapsx @ rel_injects @ rel_distincts @ flat setss;
+      injects @ distincts @ case_thms @ co_recs @ map_thms @ rel_injects @ rel_distincts @ flat setss;
 
     fun mk_co_rec_transfer_goals lthy co_recs =
       let
@@ -2078,7 +2078,7 @@
       end;
 
     fun derive_note_induct_recs_thms_for_types
-        ((((mapss, rel_injectss, rel_distinctss, setss), (ctrss, _, ctr_defss, ctr_sugars)),
+        ((((map_thmss, rel_injectss, rel_distinctss, setss), (ctrss, _, ctr_defss, ctr_sugars)),
           (recs, rec_defs)), lthy) =
       let
         val ((induct_thms, induct_thm, induct_attrs), (rec_thmss, rec_attrs)) =
@@ -2109,7 +2109,7 @@
             end;
 
         val simp_thmss =
-          map6 mk_simp_thms ctr_sugars rec_thmss mapss rel_injectss rel_distinctss setss;
+          map6 mk_simp_thms ctr_sugars rec_thmss map_thmss rel_injectss rel_distinctss setss;
 
         val common_notes =
           (if nn > 1 then
@@ -2135,7 +2135,7 @@
           (fst (dest_Type (hd fpTs)) ^ (implode (map (prefix "_") (tl fp_b_names)))) inductN
         |-> interpret_bnfs_register_fp_sugars plugins fpTs fpBTs Xs Least_FP pre_bnfs absT_infos
           fp_nesting_bnfs live_nesting_bnfs fp_res ctrXs_Tsss ctr_defss ctr_sugars recs rec_defs
-          mapss [induct_thm] (map single induct_thms) rec_thmss (replicate nn []) (replicate nn [])
+          map_thmss [induct_thm] (map single induct_thms) rec_thmss (replicate nn []) (replicate nn [])
           rel_injectss rel_distinctss
       end;
 
@@ -2155,7 +2155,7 @@
       end;
 
     fun derive_note_coinduct_corecs_thms_for_types
-        ((((mapss, rel_injectss, rel_distinctss, setss), (_, _, ctr_defss, ctr_sugars)),
+        ((((map_thmss, rel_injectss, rel_distinctss, setss), (_, _, ctr_defss, ctr_sugars)),
           (corecs, corec_defs)), lthy) =
       let
         val (([(coinduct_thms, coinduct_thm), (coinduct_strong_thms, coinduct_strong_thm)],
@@ -2216,7 +2216,7 @@
         val simp_thmss =
           map6 mk_simp_thms ctr_sugars
             (map3 flat_corec_thms corec_disc_thmss corec_disc_iff_thmss corec_sel_thmss)
-            mapss rel_injectss rel_distinctss setss;
+            map_thmss rel_injectss rel_distinctss setss;
 
         val common_notes =
           (set_inductN, set_induct_thms, nth set_induct_attrss) ::
@@ -2247,7 +2247,7 @@
         |> Local_Theory.notes (common_notes @ notes)
         |-> interpret_bnfs_register_fp_sugars plugins fpTs fpBTs Xs Greatest_FP pre_bnfs absT_infos
           fp_nesting_bnfs live_nesting_bnfs fp_res ctrXs_Tsss ctr_defss ctr_sugars corecs corec_defs
-          mapss [coinduct_thm, coinduct_strong_thm]
+          map_thmss [coinduct_thm, coinduct_strong_thm]
           (transpose [coinduct_thms, coinduct_strong_thms]) corec_thmss corec_disc_thmss
           corec_sel_thmsss rel_injectss rel_distinctss
       end;

--- a/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML	Fri Sep 26 14:43:26 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML	Fri Sep 26 14:43:28 2014 +0200
@@ -145,7 +145,7 @@
       end;
 
     val ctr_defss = map (#ctr_defs o #fp_ctr_sugar) fp_sugars0;
-    val mapss = map #maps fp_sugars0;
+    val mapss = map (#map_thms o #fp_bnf_sugar) fp_sugars0;
     val ctr_sugars = map2 target_ctr_sugar_of_fp_sugar fpTs fp_sugars0;
 
     val ctrss = map #ctrs ctr_sugars;
@@ -292,17 +292,18 @@
         val phi = Proof_Context.export_morphism names_lthy no_defs_lthy;
 
         fun mk_target_fp_sugar T X kk pre_bnf absT_info ctrXs_Tss ctr_defs ctr_sugar co_rec
-            co_rec_def maps co_inducts co_rec_thms co_rec_disc_thms co_rec_sel_thmss
+            co_rec_def map_thms co_inducts co_rec_thms co_rec_disc_thms co_rec_sel_thmss
             ({fp_bnf_sugar = {rel_injects, rel_distincts, ...}, ...} : fp_sugar) =
           {T = T, BT = T (*wrong but harmless*), X = X, fp = fp, fp_res = fp_res, fp_res_index = kk,
            pre_bnf = pre_bnf, absT_info = absT_info, fp_nesting_bnfs = fp_nesting_bnfs,
-           live_nesting_bnfs = live_nesting_bnfs, maps = maps,
+           live_nesting_bnfs = live_nesting_bnfs,
            fp_ctr_sugar =
              {ctrXs_Tss = ctrXs_Tss,
               ctr_defs = ctr_defs,
               ctr_sugar = ctr_sugar},
            fp_bnf_sugar =
-             {rel_injects = rel_injects,
+             {map_thms = map_thms,
+              rel_injects = rel_injects,
               rel_distincts = rel_distincts},
            fp_co_induct_sugar =
              {co_rec = co_rec,

--- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Fri Sep 26 14:43:26 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Fri Sep 26 14:43:28 2014 +0200
@@ -400,7 +400,7 @@
   | _ => not_codatatype ctxt res_T);
 
 fun map_thms_of_typ ctxt (Type (s, _)) =
-    (case fp_sugar_of ctxt s of SOME {maps, ...} => maps | NONE => [])
+    (case fp_sugar_of ctxt s of SOME {fp_bnf_sugar = {map_thms, ...}, ...} => map_thms | NONE => [])
   | map_thms_of_typ _ _ = [];
 
 fun corec_specs_of bs arg_Ts res_Ts callers callssss0 lthy0 =

--- a/src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML	Fri Sep 26 14:43:26 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML	Fri Sep 26 14:43:28 2014 +0200
@@ -76,13 +76,13 @@
      absT_info = trivial_absT_info_of fpT,
      fp_nesting_bnfs = [],
      live_nesting_bnfs = [],
-     maps = @{thms map_sum.simps},
      fp_ctr_sugar =
        {ctrXs_Tss = ctr_Tss,
         ctr_defs = @{thms Inl_def_alt Inr_def_alt},
         ctr_sugar = the_frozen_ctr_sugar_of ctxt fpT_name},
      fp_bnf_sugar =
-       {rel_injects = @{thms rel_sum_simps(1,4)},
+       {map_thms = @{thms map_sum.simps},
+        rel_injects = @{thms rel_sum_simps(1,4)},
         rel_distincts = @{thms rel_sum_simps(2,3)[THEN eq_False[THEN iffD1]]}},
      fp_co_induct_sugar =
        {co_rec = Const (@{const_name case_sum}, map (fn Ts => (Ts ---> C)) ctr_Tss ---> fpT --> C),
@@ -120,13 +120,13 @@
      absT_info = trivial_absT_info_of fpT,
      fp_nesting_bnfs = [],
      live_nesting_bnfs = [],
-     maps = @{thms map_prod_simp},
      fp_ctr_sugar =
        {ctrXs_Tss = [ctr_Ts],
         ctr_defs = @{thms Pair_def_alt},
         ctr_sugar = the_frozen_ctr_sugar_of ctxt fpT_name},
      fp_bnf_sugar =
-       {rel_injects = @{thms rel_prod_apply},
+       {map_thms = @{thms map_prod_simp},
+        rel_injects = @{thms rel_prod_apply},
         rel_distincts = []},
      fp_co_induct_sugar =
        {co_rec = Const (@{const_name case_prod}, (ctr_Ts ---> C) --> fpT --> C),