src/HOL/Tools/BNF/bnf_fp_def_sugar.ML

      co_rec_discs: thm list,
      co_rec_disc_iffs: thm list,
      co_rec_selss: thm list list,
      co_rec_codes: thm list,
      co_rec_transfers: thm list,
+     rec_o_maps: thm list,
      common_rel_co_inducts: thm list,
      rel_co_inducts: thm list,
      common_set_inducts: thm list,
      set_inducts: thm list}
 

 val sel_transferN = "sel_transfer";
 val corec_codeN = "corec_code";
 val corec_transferN = "corec_transfer";
 val map_disc_iffN = "map_disc_iff";
 val map_selN = "map_sel";
+val rec_o_mapN = "rec_o_map";
 val rec_transferN = "rec_transfer";
 val set_casesN = "set_cases";
 val set_introsN = "set_intros";
 val set_inductN = "set_induct";
 val set_selN = "set_sel";

    co_rec_discs: thm list,
    co_rec_disc_iffs: thm list,
    co_rec_selss: thm list list,
    co_rec_codes: thm list,
    co_rec_transfers: thm list,
+   rec_o_maps: thm list,
    common_rel_co_inducts: thm list,
    rel_co_inducts: thm list,
    common_set_inducts: thm list,
    set_inducts: thm list};
 

    set_selssss = map (map (map (map (Morphism.thm phi)))) set_selssss,
    set_introssss = map (map (map (map (Morphism.thm phi)))) set_introssss,
    set_cases = map (Morphism.thm phi) set_cases};
 
 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_disc_iffs, co_rec_selss, co_rec_codes, co_rec_transfers,
+    co_rec_discs, co_rec_disc_iffs, co_rec_selss, co_rec_codes, co_rec_transfers, rec_o_maps,
     common_rel_co_inducts, rel_co_inducts, common_set_inducts, set_inducts} : fp_co_induct_sugar) =
   {co_rec = Morphism.term phi co_rec,
    common_co_inducts = map (Morphism.thm phi) common_co_inducts,
    co_inducts = map (Morphism.thm phi) co_inducts,
    co_rec_def = Morphism.thm phi co_rec_def,

    co_rec_discs = map (Morphism.thm phi) co_rec_discs,
    co_rec_disc_iffs = map (Morphism.thm phi) co_rec_disc_iffs,
    co_rec_selss = map (map (Morphism.thm phi)) co_rec_selss,
    co_rec_codes = map (Morphism.thm phi) co_rec_codes,
    co_rec_transfers = map (Morphism.thm phi) co_rec_transfers,
+   rec_o_maps = map (Morphism.thm phi) rec_o_maps,
    common_rel_co_inducts = map (Morphism.thm phi) common_rel_co_inducts,
    rel_co_inducts = map (Morphism.thm phi) rel_co_inducts,
    common_set_inducts = map (Morphism.thm phi) common_set_inducts,
    set_inducts = map (Morphism.thm phi) set_inducts};
 

     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 map_disc_iffss map_selsss rel_selss rel_intross rel_casess set_thmss set_selsssss
     set_introsssss set_casess ctr_transferss case_transferss disc_transferss co_rec_disc_iffss
     co_rec_codess co_rec_transferss common_rel_co_inducts rel_co_inductss common_set_inducts
-    set_inductss sel_transferss noted =
+    set_inductss sel_transferss rec_o_mapss noted =
   let
     val fp_sugars =
       map_index (fn (kk, T) =>
         {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,

             co_rec_discs = nth co_rec_discss kk,
             co_rec_disc_iffs = nth co_rec_disc_iffss kk,
             co_rec_selss = nth co_rec_selsss kk,
             co_rec_codes = nth co_rec_codess kk,
             co_rec_transfers = nth co_rec_transferss kk,
+            rec_o_maps = nth rec_o_mapss kk,
             common_rel_co_inducts = common_rel_co_inducts,
             rel_co_inducts = nth rel_co_inductss kk,
             common_set_inducts = common_set_inducts,
             set_inducts = nth set_inductss kk}}
         |> morph_fp_sugar (substitute_noted_thm noted)) Ts;

 
     val ((pre_bnfs, absT_infos), (fp_res as {bnfs = fp_bnfs as any_fp_bnf :: _, ctors = ctors0,
              dtors = dtors0, xtor_co_recs = xtor_co_recs0, xtor_co_induct, dtor_ctors,
              ctor_dtors, ctor_injects, dtor_injects, xtor_maps, xtor_setss, xtor_rels,
              xtor_co_rec_thms, xtor_rel_co_induct, dtor_set_inducts,
-             xtor_co_rec_transfers, ...},
+             xtor_co_rec_transfers, xtor_co_rec_o_maps, ...},
            lthy)) =
       fp_bnf (construct_fp mixfixes map_bs rel_bs set_bss) fp_bs (map dest_TFree unsorted_As)
         (map dest_TFree killed_As) fp_eqs no_defs_lthy
       handle BAD_DEAD (X, X_backdrop) =>
         (case X_backdrop of

     val pre_map_defs = map map_def_of_bnf pre_bnfs;
     val pre_set_defss = map set_defs_of_bnf pre_bnfs;
     val pre_rel_defs = map rel_def_of_bnf pre_bnfs;
     val fp_nesting_set_maps = maps set_map_of_bnf fp_nesting_bnfs;
     val live_nesting_map_id0s = map map_id0_of_bnf live_nesting_bnfs;
+    val live_nesting_map_ident0s = map map_ident0_of_bnf live_nesting_bnfs;
     val live_nesting_set_maps = maps set_map_of_bnf live_nesting_bnfs;
     val live_nesting_rel_eqs = map rel_eq_of_bnf live_nesting_bnfs;
 
     val live = live_of_bnf any_fp_bnf;
     val _ =

       @{map 3} (fn alive => fn A as TFree (_, S) => fn B =>
           if alive then resort_tfree_or_tvar S B else A)
         (liveness_of_fp_bnf num_As any_fp_bnf) As Bs0;
 
     val B_ify_T = Term.typ_subst_atomic (As ~~ Bs);
+    val live_AsBs = filter (op <>) (As ~~ Bs);
 
     val ctors = map (mk_ctor As) ctors0;
     val dtors = map (mk_dtor As) dtors0;
 
     val fpTs = map (domain_type o fastype_of) dtors;

       injects @ distincts @ case_thms @ co_recs @ map_thms @ rel_injects @ rel_distincts @
       set_thmss;
 
     fun mk_co_rec_transfer_goals lthy co_recs =
       let
-        val liveAsBs = filter (op <>) (As ~~ Bs);
-        val B_ify = Term.subst_atomic_types (liveAsBs @ (Cs ~~ Es));
+        val B_ify = Term.subst_atomic_types (live_AsBs @ (Cs ~~ Es));
 
         val ((Rs, Ss), names_lthy) = lthy
-          |> mk_Frees "R" (map (uncurry mk_pred2T) liveAsBs)
+          |> mk_Frees "R" (map (uncurry mk_pred2T) live_AsBs)
           ||>> mk_Frees "S" (map2 mk_pred2T Cs Es);
 
         val co_recBs = map B_ify co_recs;
       in
         (Rs, Ss, map2 (mk_parametricity_goal lthy (Rs @ Ss)) co_recs co_recBs, names_lthy)

                xtor_co_rec_transfers pre_rel_defs live_nesting_rel_eqs)
         |> Conjunction.elim_balanced nn
         |> Proof_Context.export names_lthy lthy
         |> map Thm.close_derivation
       end;
+
+    fun derive_rec_o_map_thmss lthy recs rec_defs =
+      if live = 0 then replicate nn []
+      else
+        let
+          fun variant_names n pre = fst (Variable.variant_fixes (replicate n pre) lthy);
+
+          val maps0 = map map_of_bnf fp_bnfs;
+          val ABs = As ~~ Bs
+          val liveness = map (op <>) ABs;
+          val f_names = variant_names num_As "f";
+          val fs = map2 (curry Free) f_names (map (op -->) ABs);
+          val live_gs = AList.find (op =) (fs ~~ liveness) true;
+
+          val gmaps = map (fn map0 => Term.list_comb (mk_map live As Bs map0, live_gs)) maps0;
+
+          val rec_Ts as rec_T1 :: _ = map fastype_of recs;
+          val rec_arg_Ts = binder_fun_types rec_T1;
+
+          val B_ify_T = Term.typ_subst_atomic (As ~~ Bs);
+
+          val num_rec_args = length rec_arg_Ts;
+          val g_Ts = map B_ify_T rec_arg_Ts;
+          val g_names = variant_names num_rec_args "g";
+          val gs = map2 (curry Free) g_names g_Ts;
+          val grecs = map (fn recx => Term.list_comb (Term.map_types B_ify_T recx, gs)) recs;
+
+          val rec_o_map_lhss = map2 (curry HOLogic.mk_comp) grecs gmaps;
+
+          val ABfs = ABs ~~ fs;
+
+          fun mk_rec_arg_arg (x as Free (_, T)) =
+            let val U = B_ify_T T in
+              if T = U then x else build_map lthy [] (the o AList.lookup (op =) ABfs) (T, U) $ x
+            end;
+
+          fun mk_rec_o_map_arg rec_arg_T h =
+            let
+              val x_Ts = binder_types rec_arg_T;
+              val m = length x_Ts;
+              val x_names = variant_names m "x";
+              val xs = map2 (curry Free) x_names x_Ts;
+              val xs' = map mk_rec_arg_arg xs;
+            in
+              fold_rev Term.lambda xs (Term.list_comb (h, xs'))
+            end;
+
+          fun mk_rec_o_map_rhs recx =
+            let val args = map2 mk_rec_o_map_arg rec_arg_Ts gs in
+              Term.list_comb (recx, args)
+            end;
+
+          val rec_o_map_rhss = map mk_rec_o_map_rhs recs;
+
+          val rec_o_map_goals =
+            map2 (fold_rev (fold_rev Logic.all) [fs, gs] o HOLogic.mk_Trueprop oo
+              curry HOLogic.mk_eq) rec_o_map_lhss rec_o_map_rhss;
+          val rec_o_map_thms =
+            @{map 3} (fn goal => fn rec_def => fn ctor_rec_o_map =>
+                Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, ...} =>
+                  mk_rec_o_map_tac ctxt rec_def pre_map_defs live_nesting_map_ident0s abs_inverses
+                    ctor_rec_o_map)
+                |> Thm.close_derivation)
+              rec_o_map_goals rec_defs xtor_co_rec_o_maps;
+        in
+          map single rec_o_map_thms
+        end;
 
     fun derive_note_induct_recs_thms_for_types
         ((((map_thmss, map_disc_iffss, map_selsss, rel_injectss, rel_distinctss, rel_selss,
             rel_intross, rel_casess, set_thmss, set_selsssss, set_introsssss,
             set_casess, ctr_transferss, case_transferss, disc_transferss, sel_transferss),

             in
               ((map single rel_induct_thms, single common_rel_induct_thm),
                (rel_induct_attrs, rel_induct_attrs))
             end;
 
+        val rec_o_map_thmss = derive_rec_o_map_thmss lthy recs rec_defs;
+
         val simp_thmss =
           @{map 6} mk_simp_thms ctr_sugars rec_thmss map_thmss rel_injectss rel_distinctss set_thmss;
 
         val common_notes =
           (if nn > 1 then

           |> massage_simple_notes fp_common_name;
 
         val notes =
           [(inductN, map single induct_thms, fn T_name => induct_attrs @ [induct_type_attr T_name]),
            (recN, rec_thmss, K rec_attrs),
+           (rec_o_mapN, rec_o_map_thmss, K []),
            (rec_transferN, rec_transfer_thmss, K []),
            (rel_inductN, rel_induct_thmss, K (rel_induct_attrs @ [induct_pred_attr ""])),
            (simpsN, simp_thmss, K [])]
           |> massage_multi_notes fp_b_names fpTs;
       in

           map_thmss [induct_thm] (map single induct_thms) rec_thmss (replicate nn [])
           (replicate nn []) rel_injectss rel_distinctss map_disc_iffss map_selsss rel_selss
           rel_intross rel_casess set_thmss set_selsssss set_introsssss set_casess ctr_transferss
           case_transferss disc_transferss (replicate nn []) (replicate nn []) rec_transfer_thmss
           common_rel_induct_thms rel_induct_thmss [] (replicate nn []) sel_transferss
+          rec_o_map_thmss
       end;
 
     fun derive_corec_transfer_thms lthy corecs corec_defs =
       let
         val (Rs, Ss, goals, names_lthy) = mk_co_rec_transfer_goals lthy corecs;

           (transpose [coinduct_thms, coinduct_strong_thms]) corec_thmss corec_disc_thmss
           corec_sel_thmsss rel_injectss rel_distinctss map_disc_iffss map_selsss rel_selss
           rel_intross rel_casess set_thmss set_selsssss set_introsssss set_casess ctr_transferss
           case_transferss disc_transferss corec_disc_iff_thmss (map single corec_code_thms)
           corec_transfer_thmss common_rel_coinduct_thms rel_coinduct_thmss set_induct_thms
-          (replicate nn (if nn = 1 then set_induct_thms else [])) sel_transferss
+          (replicate nn (if nn = 1 then set_induct_thms else [])) sel_transferss (replicate nn [])
       end;
 
     val lthy'' = lthy'
       |> live > 0 ? fold2 (fn Type (s, _) => fn bnf => register_bnf_raw s bnf) fpTs fp_bnfs
       |> fold_map (define_ctrs_dtrs_for_type fp) (fp_bnfs ~~ fp_bs ~~ fpTs ~~ ctors ~~ dtors ~~