src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML

         | callsp => freeze_fpTs_map kk fpT callsp T)
       | freeze_fpTs_call _ _ _ T = T;
 
     val ctr_Tsss = map (map binder_types) ctr_Tss;
     val ctrXs_Tsss = map4 (map2 o map2 oo freeze_fpTs_call) kks fpTs callssss ctr_Tsss;
-    val ctrXs_sum_prod_Ts = map (mk_sumTN_balanced o map HOLogic.mk_tupleT) ctrXs_Tsss;
+    val ctrXs_repTs = map (mk_sumTN_balanced o map HOLogic.mk_tupleT) ctrXs_Tsss;
 
     val ns = map length ctr_Tsss;
     val kss = map (fn n => 1 upto n) ns;
     val mss = map (map length) ctr_Tsss;
 
-    val fp_eqs = map dest_TFree Xs ~~ ctrXs_sum_prod_Ts;
+    val fp_eqs = map dest_TFree Xs ~~ ctrXs_repTs;
     val key = key_of_fp_eqs fp fpTs fp_eqs;
   in
     (case n2m_sugar_of no_defs_lthy key of
       SOME n2m_sugar => (n2m_sugar, no_defs_lthy)
     | NONE =>

               val deads = deads_of_bnf bnf;
               val dead_Us =
                 map_filter (fn (T, U) => if member (op =) deads T then SOME U else NONE) (Ts ~~ Us);
             in fold Term.add_tfreesT dead_Us [] end);
 
-        val (pre_bnfs, (fp_res as {xtor_co_iterss = xtor_co_iterss0, xtor_co_induct, dtor_injects,
-               dtor_ctors, xtor_co_iter_thmss, ...}, lthy)) =
+        val fp_absT_infos = map #absT_info fp_sugars0;
+
+        val ((pre_bnfs, absT_infos), (fp_res as {xtor_co_iterss = xtor_co_iterss0, xtor_co_induct,
+               dtor_injects, dtor_ctors, xtor_co_iter_thmss, ...}, lthy)) =
           fp_bnf (construct_mutualized_fp fp fpTs fp_sugars0) fp_bs As' killed_As' fp_eqs
-            no_defs_lthy;
+            no_defs_lthy0;
+
+        val fp_abs_inverses = map #abs_inverse fp_absT_infos;
+        val fp_type_definitions = map #type_definition fp_absT_infos;
+
+        val abss = map #abs absT_infos;
+        val reps = map #rep absT_infos;
+        val absTs = map #absT absT_infos;
+        val repTs = map #repT absT_infos;
+        val abs_inverses = map #abs_inverse absT_infos;
 
         val nesting_bnfs = nesty_bnfs lthy ctrXs_Tsss As;
         val nested_bnfs = nesty_bnfs lthy ctrXs_Tsss Xs;
 
         val ((xtor_co_iterss, iters_args_types, coiters_args_types), _) =
-          mk_co_iters_prelims fp ctr_Tsss fpTs Cs ns mss xtor_co_iterss0 lthy;
+          mk_co_iters_prelims fp ctr_Tsss fpTs Cs absTs repTs ns mss xtor_co_iterss0 lthy;
 
         fun mk_binding b suf = Binding.suffix_name ("_" ^ suf) b;
 
         val ((co_iterss, co_iter_defss), lthy) =
           fold_map2 (fn b =>
-            (if fp = Least_FP then define_iters [foldN, recN] (the iters_args_types)
-             else define_coiters [unfoldN, corecN] (the coiters_args_types))
-              (mk_binding b) fpTs Cs) fp_bs xtor_co_iterss lthy
+            if fp = Least_FP then
+              define_iters [foldN, recN] (the iters_args_types) (mk_binding b) fpTs Cs reps
+            else
+              define_coiters [unfoldN, corecN] (the coiters_args_types) (mk_binding b) fpTs Cs abss)
+            fp_bs xtor_co_iterss lthy
           |>> split_list;
 
         val ((common_co_inducts, co_inductss, un_fold_thmss, co_rec_thmss, disc_unfold_thmss,
               disc_corec_thmss, sel_unfold_thmsss, sel_corec_thmsss), fp_sugar_thms) =
           if fp = Least_FP then
             derive_induct_iters_thms_for_types pre_bnfs (the iters_args_types) xtor_co_induct
-              xtor_co_iter_thmss nesting_bnfs nested_bnfs fpTs Cs Xs ctrXs_Tsss ctrss ctr_defss
-              co_iterss co_iter_defss lthy
+              xtor_co_iter_thmss nesting_bnfs nested_bnfs fpTs Cs Xs ctrXs_Tsss fp_abs_inverses
+              fp_type_definitions abs_inverses ctrss ctr_defss co_iterss co_iter_defss lthy
             |> `(fn ((inducts, induct, _), (fold_thmss, rec_thmss, _)) =>
               ([induct], [inducts], fold_thmss, rec_thmss, replicate nn [],
                replicate nn [], replicate nn [], replicate nn []))
             ||> (fn info => (SOME info, NONE))
           else
             derive_coinduct_coiters_thms_for_types pre_bnfs (the coiters_args_types) xtor_co_induct
               dtor_injects dtor_ctors xtor_co_iter_thmss nesting_bnfs fpTs Cs Xs ctrXs_Tsss kss mss
-              ns ctr_defss ctr_sugars co_iterss co_iter_defss
-              (Proof_Context.export lthy no_defs_lthy) lthy
+              ns fp_abs_inverses abs_inverses (fn thm => thm RS @{thm vimage2p_refl}) ctr_defss
+              ctr_sugars co_iterss co_iter_defss (Proof_Context.export lthy no_defs_lthy) lthy
             |> `(fn ((coinduct_thms_pairs, _), (unfold_thmss, corec_thmss, _),
                     (disc_unfold_thmss, disc_corec_thmss, _), _,
                     (sel_unfold_thmsss, sel_corec_thmsss, _)) =>
               (map snd coinduct_thms_pairs, map fst coinduct_thms_pairs, unfold_thmss,
                corec_thmss, disc_unfold_thmss, disc_corec_thmss, sel_unfold_thmsss,
                sel_corec_thmsss))
             ||> (fn info => (NONE, SOME info));
 
         val phi = Proof_Context.export_morphism no_defs_lthy no_defs_lthy0;
 
-        fun mk_target_fp_sugar T X kk pre_bnf ctrXs_Tss ctr_defs ctr_sugar co_iters maps co_inducts
-            un_fold_thms co_rec_thms disc_unfold_thms disc_corec_thms sel_unfold_thmss
+        fun mk_target_fp_sugar T X kk pre_bnf absT_info ctrXs_Tss ctr_defs ctr_sugar co_iters maps
+            co_inducts un_fold_thms co_rec_thms disc_unfold_thms disc_corec_thms sel_unfold_thmss
             sel_corec_thmss =
           {T = T, X = X, fp = fp, fp_res = fp_res, fp_res_index = kk, pre_bnf = pre_bnf,
-           nested_bnfs = nested_bnfs, nesting_bnfs = nesting_bnfs, ctrXs_Tss = ctrXs_Tss,
-           ctr_defs = ctr_defs, ctr_sugar = ctr_sugar, co_iters = co_iters, maps = maps,
-           common_co_inducts = common_co_inducts, co_inducts = co_inducts,
+           absT_info = absT_info, nested_bnfs = nested_bnfs, nesting_bnfs = nesting_bnfs,
+           ctrXs_Tss = ctrXs_Tss, ctr_defs = ctr_defs, ctr_sugar = ctr_sugar, co_iters = co_iters,
+           maps = maps, common_co_inducts = common_co_inducts, co_inducts = co_inducts,
            co_iter_thmss = [un_fold_thms, co_rec_thms],
            disc_co_iterss = [disc_unfold_thms, disc_corec_thms],
            sel_co_itersss = [sel_unfold_thmss, sel_corec_thmss]}
           |> morph_fp_sugar phi;
 
         val target_fp_sugars =
-          map16 mk_target_fp_sugar fpTs Xs kks pre_bnfs ctrXs_Tsss ctr_defss ctr_sugars co_iterss
-            mapss (transpose co_inductss) un_fold_thmss co_rec_thmss disc_unfold_thmss
+          map17 mk_target_fp_sugar fpTs Xs kks pre_bnfs absT_infos ctrXs_Tsss ctr_defss ctr_sugars
+            co_iterss mapss (transpose co_inductss) un_fold_thmss co_rec_thmss disc_unfold_thmss
             disc_corec_thmss sel_unfold_thmsss sel_corec_thmsss;
 
         val n2m_sugar = (target_fp_sugars, fp_sugar_thms);
       in
         (n2m_sugar, lthy |> register_n2m_sugar key n2m_sugar)