src/HOL/Tools/BNF/bnf_fp_n2m.ML

n2m operates on (un)folds

(*  Title:      HOL/Tools/BNF/bnf_fp_n2m.ML
    Author:     Dmitriy Traytel, TU Muenchen
    Copyright   2013

Flattening of nested to mutual (co)recursion.
*)

signature BNF_FP_N2M =
sig
  val construct_mutualized_fp: BNF_Util.fp_kind -> int list -> typ list ->
    (int * BNF_FP_Util.fp_result) list -> binding list -> (string * sort) list ->
    typ list * typ list list -> BNF_Def.bnf list -> BNF_Comp.absT_info list -> local_theory ->
    BNF_FP_Util.fp_result * local_theory
end;

structure BNF_FP_N2M : BNF_FP_N2M =
struct

open BNF_Def
open BNF_Util
open BNF_Comp
open BNF_FP_Util
open BNF_FP_Def_Sugar
open BNF_Tactics
open BNF_FP_N2M_Tactics

fun mk_arg_cong ctxt n t =
  let
    val Us = fastype_of t |> strip_typeN n |> fst;
    val ((xs, ys), _) = ctxt
      |> mk_Frees "x" Us
      ||>> mk_Frees "y" Us;
    val goal = Logic.list_implies (@{map 2} (curry mk_Trueprop_eq) xs ys,
      mk_Trueprop_eq (list_comb (t, xs), list_comb (t, ys)));
    val vars = Variable.add_free_names ctxt goal [];
  in
    Goal.prove_sorry ctxt vars [] goal (fn {context = ctxt, prems = _} =>
      HEADGOAL (hyp_subst_tac ctxt THEN' rtac ctxt refl))
    |> Thm.close_derivation
  end;

fun construct_mutualized_fp fp mutual_cliques fpTs indexed_fp_ress bs resBs (resDs, Dss) bnfs
    (absT_infos : absT_info list) lthy =
  let
    val time = time lthy;
    val timer = time (Timer.startRealTimer ());

    val b_names = map Binding.name_of bs;
    val b_name = mk_common_name b_names;
    val b = Binding.name b_name;

    fun of_fp_res get = map (uncurry nth o swap o apsnd get) indexed_fp_ress;
    fun mk_co_algT T U = case_fp fp (T --> U) (U --> T);
    fun co_swap pair = case_fp fp I swap pair;
    val mk_co_comp = curry (HOLogic.mk_comp o co_swap);

    val dest_co_algT = co_swap o dest_funT;
    val co_alg_argT = case_fp fp range_type domain_type;
    val co_alg_funT = case_fp fp domain_type range_type;
    val rewrite_comp_comp = case_fp fp @{thm rewriteL_comp_comp} @{thm rewriteR_comp_comp};

    val fp_absT_infos = of_fp_res #absT_infos;
    val fp_bnfs = of_fp_res #bnfs;
    val fp_pre_bnfs = of_fp_res #pre_bnfs;

    val fp_absTs = map #absT fp_absT_infos;
    val fp_repTs = map #repT fp_absT_infos;
    val fp_abss = map #abs fp_absT_infos;
    val fp_reps = map #rep fp_absT_infos;
    val fp_type_definitions = map #type_definition fp_absT_infos;

    val absTs = map #absT absT_infos;
    val repTs = map #repT absT_infos;
    val absTs' = map (Logic.type_map (singleton (Variable.polymorphic lthy))) absTs;
    val repTs' = map (Logic.type_map (singleton (Variable.polymorphic lthy))) repTs;
    val abss = map #abs absT_infos;
    val reps = map #rep absT_infos;
    val abs_inverses = map #abs_inverse absT_infos;
    val type_definitions = map #type_definition absT_infos;

    val n = length bnfs;
    val deads = fold (union (op =)) Dss resDs;
    val As = subtract (op =) deads (map TFree resBs);
    val names_lthy = fold Variable.declare_typ (As @ deads) lthy;
    val m = length As;
    val live = m + n;

    val (((Xs, Ys), Bs), names_lthy) = names_lthy
      |> mk_TFrees n
      ||>> mk_TFrees n
      ||>> mk_TFrees m;

    val allAs = As @ Xs;
    val allBs = Bs @ Xs;
    val phiTs = map2 mk_pred2T As Bs;
    val thetaBs = As ~~ Bs;
    val fpTs' = map (Term.typ_subst_atomic thetaBs) fpTs;
    val fold_thetaAs = Xs ~~ fpTs;
    val fold_thetaBs = Xs ~~ fpTs';
    val pre_phiTs = map2 mk_pred2T fpTs fpTs';

    val ((ctors, dtors), (xtor's, xtors)) =
      let
        val ctors = map2 (force_typ names_lthy o (fn T => dummyT --> T)) fpTs (of_fp_res #ctors);
        val dtors = map2 (force_typ names_lthy o (fn T => T --> dummyT)) fpTs (of_fp_res #dtors);
      in
        ((ctors, dtors), `(map (Term.subst_atomic_types thetaBs)) (case_fp fp ctors dtors))
      end;

    val absATs = map (domain_type o fastype_of) ctors;
    val absBTs = map (Term.typ_subst_atomic thetaBs) absATs;
    val xTs = map (domain_type o fastype_of) xtors;
    val yTs = map (domain_type o fastype_of) xtor's;

    val absAs = @{map 3} (fn Ds => mk_abs o mk_T_of_bnf Ds allAs) Dss bnfs abss;
    val absBs = @{map 3} (fn Ds => mk_abs o mk_T_of_bnf Ds allBs) Dss bnfs abss;
    val fp_repAs = map2 mk_rep absATs fp_reps;
    val fp_repBs = map2 mk_rep absBTs fp_reps;

    val typ_subst_nonatomic_sorted = fold_rev (typ_subst_nonatomic o single);
    val sorted_theta = sort (int_ord o apply2 (Term.size_of_typ o fst)) (fpTs ~~ Xs)
    val sorted_fpTs = map fst sorted_theta;

    val nesting_bnfs = nesting_bnfs lthy
      [[map (typ_subst_nonatomic_sorted (rev sorted_theta) o range_type o fastype_of) fp_repAs]]
      allAs;
    val fp_or_nesting_bnfs = distinct (op = o apply2 T_of_bnf) (fp_bnfs @ nesting_bnfs);

    val (((((phis, phis'), pre_phis), xs), ys), names_lthy) = names_lthy
      |> mk_Frees' "R" phiTs
      ||>> mk_Frees "S" pre_phiTs
      ||>> mk_Frees "x" xTs
      ||>> mk_Frees "y" yTs;

    val rels =
      let
        fun find_rel T As Bs = fp_or_nesting_bnfs
          |> filter_out (curry (op = o apply2 name_of_bnf) BNF_Comp.DEADID_bnf)
          |> find_first (fn bnf => Type.could_unify (T_of_bnf bnf, T))
          |> Option.map (fn bnf =>
            let val live = live_of_bnf bnf;
            in (mk_rel live As Bs (rel_of_bnf bnf), live) end)
          |> the_default (HOLogic.eq_const T, 0);

        fun mk_rel (T as Type (_, Ts)) (Type (_, Us)) =
              let
                val (rel, live) = find_rel T Ts Us;
                val (Ts', Us') = fastype_of rel |> strip_typeN live |> fst |> map_split dest_pred2T;
                val rels = map2 mk_rel Ts' Us';
              in
                Term.list_comb (rel, rels)
              end
          | mk_rel (T as TFree _) _ = (nth phis (find_index (curry op = T) As)
              handle General.Subscript => HOLogic.eq_const T)
          | mk_rel _ _ = raise Fail "fpTs contains schematic type variables";
      in
        map2 (fold_rev Term.absfree phis' oo mk_rel) fpTs fpTs'
      end;

    val pre_rels = map2 (fn Ds => mk_rel_of_bnf Ds (As @ fpTs) (Bs @ fpTs')) Dss bnfs;

    val rel_unfolds = maps (no_refl o single o rel_def_of_bnf) fp_pre_bnfs;
    val rel_xtor_co_inducts = of_fp_res (split_conj_thm o #xtor_rel_co_induct)
      |> map (zero_var_indexes o unfold_thms lthy (id_apply :: rel_unfolds));

    val rel_defs = map rel_def_of_bnf bnfs;
    val rel_monos = map rel_mono_of_bnf bnfs;

    fun cast castA castB pre_rel =
      let
        val castAB = mk_vimage2p (Term.subst_atomic_types fold_thetaAs castA)
          (Term.subst_atomic_types fold_thetaBs castB);
      in
        fold_rev (fold_rev Term.absdummy) [phiTs, pre_phiTs]
          (castAB $ Term.list_comb (pre_rel, map Bound (live - 1 downto 0)))
      end;

    val castAs = map2 (curry HOLogic.mk_comp) absAs fp_repAs;
    val castBs = map2 (curry HOLogic.mk_comp) absBs fp_repBs;

    val fp_or_nesting_rel_eqs = no_refl (map rel_eq_of_bnf fp_or_nesting_bnfs);
    val fp_or_nesting_rel_monos = map rel_mono_of_bnf fp_or_nesting_bnfs;

    fun mutual_instantiate ctxt inst =
      let
        val thetas = AList.group (op =) (mutual_cliques ~~ inst);
      in
        map2 (infer_instantiate ctxt o the o AList.lookup (op =) thetas) mutual_cliques
      end;

    val rel_xtor_co_inducts_inst =
      let
        val extract =
          case_fp fp (snd o Term.dest_comb) (snd o Term.dest_comb o fst o Term.dest_comb);
        val raw_phis = map (extract o HOLogic.dest_Trueprop o Thm.concl_of) rel_xtor_co_inducts;
        val inst = map (fn (t, u) => (#1 (dest_Var t), Thm.cterm_of lthy u)) (raw_phis ~~ pre_phis);
      in
        mutual_instantiate lthy inst rel_xtor_co_inducts
      end

    val xtor_rel_co_induct =
      mk_xtor_rel_co_induct_thm fp (@{map 3} cast castAs castBs pre_rels) pre_phis rels phis xs ys
        xtors xtor's (mk_rel_xtor_co_induct_tac fp abs_inverses rel_xtor_co_inducts_inst rel_defs
          rel_monos fp_or_nesting_rel_eqs fp_or_nesting_rel_monos)
        lthy;

    val map_id0s = no_refl (map map_id0_of_bnf bnfs);

    val xtor_co_induct_thm =
      (case fp of
        Least_FP =>
          let
            val (Ps, names_lthy) = names_lthy
              |> mk_Frees "P" (map (fn T => T --> HOLogic.boolT) fpTs);
            fun mk_Grp_id P =
              let val T = domain_type (fastype_of P);
              in mk_Grp (HOLogic.Collect_const T $ P) (HOLogic.id_const T) end;
            val cts =
              map (SOME o Thm.cterm_of names_lthy) (map HOLogic.eq_const As @ map mk_Grp_id Ps);
            fun mk_fp_type_copy_thms thm = map (curry op RS thm)
              @{thms type_copy_Abs_o_Rep type_copy_vimage2p_Grp_Rep};
            fun mk_type_copy_thms thm = map (curry op RS thm)
              @{thms type_copy_Rep_o_Abs type_copy_vimage2p_Grp_Abs};
          in
            infer_instantiate' names_lthy cts xtor_rel_co_induct
            |> singleton (Proof_Context.export names_lthy lthy)
            |> unfold_thms lthy (@{thms eq_le_Grp_id_iff all_simps(1,2)[symmetric]} @
                fp_or_nesting_rel_eqs)
            |> funpow n (fn thm => thm RS spec)
            |> unfold_thms lthy (@{thm eq_alt} :: map rel_Grp_of_bnf bnfs @ map_id0s)
            |> unfold_thms lthy (@{thms vimage2p_id vimage2p_comp comp_apply comp_id
               Grp_id_mono_subst eqTrueI[OF subset_UNIV] simp_thms(22)} @
               maps mk_fp_type_copy_thms fp_type_definitions @
               maps mk_type_copy_thms type_definitions)
            |> unfold_thms lthy @{thms subset_iff mem_Collect_eq
               atomize_conjL[symmetric] atomize_all[symmetric] atomize_imp[symmetric]}
          end
      | Greatest_FP =>
          let
            val cts = NONE :: map (SOME o Thm.cterm_of lthy) (map HOLogic.eq_const As);
          in
            infer_instantiate' lthy cts xtor_rel_co_induct
            |> unfold_thms lthy (@{thms le_fun_def le_bool_def all_simps(1,2)[symmetric]} @
                fp_or_nesting_rel_eqs)
            |> funpow (2 * n) (fn thm => thm RS spec)
            |> Conv.fconv_rule (Object_Logic.atomize lthy)
            |> funpow n (fn thm => thm RS mp)
          end);

    val timer = time (timer "Nested-to-mutual (co)induction");

    val fold_preTs = map2 (fn Ds => mk_T_of_bnf Ds allAs) Dss bnfs;

    val fold_strTs = map2 mk_co_algT fold_preTs Xs;
    val resTs = map2 mk_co_algT fpTs Xs;

    val ((fold_strs, fold_strs'), names_lthy) = names_lthy
      |> mk_Frees' "s" fold_strTs;

    val fp_un_folds = of_fp_res #xtor_un_folds;
    val ns = map (length o #Ts o snd) indexed_fp_ress;

    fun force_fold i TU raw_un_fold =
      let
        val thy = Proof_Context.theory_of lthy;

        val approx_un_fold = raw_un_fold
          |> force_typ names_lthy (replicate (nth ns i) dummyT ---> TU);
        val subst = Term.typ_subst_atomic fold_thetaAs;

        fun mk_fp_absT_repT fp_repT fp_absT = mk_absT thy fp_repT fp_absT ooo mk_repT;
        val mk_fp_absT_repTs = @{map 5} mk_fp_absT_repT fp_repTs fp_absTs absTs repTs;

        val fold_preTs' = mk_fp_absT_repTs (map subst fold_preTs);

        val fold_pre_deads_only_Ts =
          map (typ_subst_nonatomic_sorted (map (rpair dummyT) (As @ sorted_fpTs))) fold_preTs';

        val (mutual_clique, TUs) =
          map_split dest_co_algT (binder_fun_types (fastype_of approx_un_fold))
          |>> map subst
          |> `(fn (_, Ys) => nth mutual_cliques
            (find_index (fn X => X = the (find_first (can dest_TFree) Ys)) Xs))
          ||> uncurry (map2 mk_co_algT);
        val cands = mutual_cliques ~~ map2 mk_co_algT fold_preTs' Xs;
        val js = find_indices (fn ((cl, cand), TU) =>
          cl = mutual_clique andalso Type.could_unify (TU, cand)) TUs cands;
        val Tpats = map (fn j => mk_co_algT (nth fold_pre_deads_only_Ts j) (nth Xs j)) js;
      in
        force_typ names_lthy (Tpats ---> TU) raw_un_fold
      end;

    fun mk_co_comp_abs_rep fp_absT absT fp_abs fp_rep abs rep t =
      case_fp fp (HOLogic.mk_comp (HOLogic.mk_comp (t, mk_abs absT abs), mk_rep fp_absT fp_rep))
        (HOLogic.mk_comp (mk_abs fp_absT fp_abs, HOLogic.mk_comp (mk_rep absT rep, t)));

    fun mk_un_fold b_opt un_folds lthy TU =
      let
        val thy = Proof_Context.theory_of lthy;

        val x = co_alg_argT TU;
        val i = find_index (fn T => x = T) Xs;
        val TUfold =
          (case find_first (fn f => body_fun_type (fastype_of f) = TU) un_folds of
            NONE => force_fold i TU (nth fp_un_folds i)
          | SOME f => f);

        val TUs = binder_fun_types (fastype_of TUfold);

        fun mk_s TU' =
          let
            fun mk_absT_fp_repT repT absT = mk_absT thy repT absT ooo mk_repT;

            val i = find_index (fn T => co_alg_argT TU' = T) Xs;
            val fp_abs = nth fp_abss i;
            val fp_rep = nth fp_reps i;
            val abs = nth abss i;
            val rep = nth reps i;
            val sF = co_alg_funT TU';
            val sF' =
              mk_absT_fp_repT (nth repTs' i) (nth absTs' i) (nth fp_absTs i) (nth fp_repTs i) sF
                handle Term.TYPE _ => sF;
            val F = nth fold_preTs i;
            val s = nth fold_strs i;
          in
            if sF = F then s
            else if sF' = F then mk_co_comp_abs_rep sF sF' fp_abs fp_rep abs rep s
            else
              let
                val smapT = replicate live dummyT ---> mk_co_algT sF' F;
                fun hidden_to_unit t =
                  Term.subst_TVars (map (rpair HOLogic.unitT) (Term.add_tvar_names t [])) t;
                val smap = map_of_bnf (nth bnfs i)
                  |> force_typ names_lthy smapT
                  |> hidden_to_unit;
                val smap_argTs = strip_typeN live (fastype_of smap) |> fst;
                fun mk_smap_arg T_to_U =
                  (if domain_type T_to_U = range_type T_to_U then
                    HOLogic.id_const (domain_type T_to_U)
                  else
                    fst (fst (mk_un_fold NONE un_folds lthy T_to_U)));
                val smap_args = map mk_smap_arg smap_argTs;
              in
                mk_co_comp_abs_rep sF sF' fp_abs fp_rep abs rep
                  (mk_co_comp s (Term.list_comb (smap, smap_args)))
              end
          end;
        val t = Term.list_comb (TUfold, map mk_s TUs);
      in
        (case b_opt of
          NONE => ((t, Drule.dummy_thm), lthy)
        | SOME b => Local_Theory.define ((b, NoSyn), ((Binding.concealed (Thm.def_binding b), []),
            fold_rev Term.absfree fold_strs' t)) lthy |>> apsnd snd)
      end;

    val foldN = case_fp fp ctor_foldN dtor_unfoldN;
    fun mk_un_folds lthy =
      fold2 (fn TU => fn b => fn ((un_folds, defs), lthy) =>
        mk_un_fold (SOME b) un_folds lthy TU |>> (fn (f, d) => (f :: un_folds, d :: defs)))
      resTs (map (Binding.suffix_name ("_" ^ foldN)) bs) (([], []), lthy)
      |>> map_prod rev rev;
    val ((raw_xtor_un_folds, raw_xtor_un_fold_defs), (lthy, raw_lthy)) = lthy
      |> Local_Theory.open_target |> snd
      |> mk_un_folds
      ||> `Local_Theory.close_target;

    val phi = Proof_Context.export_morphism raw_lthy lthy;

    val xtor_un_folds = map (Morphism.term phi) raw_xtor_un_folds;
    val xtor_un_fold_defs = map (Morphism.thm phi) raw_xtor_un_fold_defs;
    val xtor_un_folds' = map2 (fn raw => fn t => Const (fst (dest_Const t), fastype_of raw)) raw_xtor_un_folds xtor_un_folds;

    val fp_un_fold_o_maps = of_fp_res #xtor_un_fold_o_maps
      |> maps (fn thm => [thm, thm RS rewrite_comp_comp]);

    val un_folds = map (fn fold => Term.list_comb (fold, fold_strs)) raw_xtor_un_folds;
    val fold_mapTs = co_swap (As @ fpTs, As @ Xs);
    val pre_fold_maps = @{map 2} (fn Ds => uncurry (mk_map_of_bnf Ds) fold_mapTs) Dss bnfs
    fun mk_pre_fold_maps fs =
      map (fn mapx => Term.list_comb (mapx, map HOLogic.id_const As @ fs)) pre_fold_maps;

    val pre_map_defs = no_refl (map map_def_of_bnf bnfs);
    val fp_map_defs = no_refl (map map_def_of_bnf fp_pre_bnfs);
    val map_defs = pre_map_defs @ fp_map_defs;
    val pre_rel_defs = no_refl (map rel_def_of_bnf bnfs);
    val fp_rel_defs = no_refl (map rel_def_of_bnf fp_pre_bnfs);
    val rel_defs = pre_rel_defs @ fp_rel_defs;
    fun mk_Rep_o_Abs thm = (thm RS @{thm type_copy_Rep_o_Abs})
      |> (fn thm => [thm, thm RS rewrite_comp_comp]);
    val fp_Rep_o_Abss = maps mk_Rep_o_Abs fp_type_definitions;
    val pre_Rep_o_Abss = maps mk_Rep_o_Abs type_definitions;
    val Rep_o_Abss = fp_Rep_o_Abss @ pre_Rep_o_Abss;

    val unfold_map = map (unfold_thms lthy (id_apply :: pre_map_defs));
    val simp_thms = case_fp fp @{thm comp_assoc} @{thm comp_assoc[symmetric]} ::
      @{thms id_apply comp_id id_comp};

    val eq_thm_prop_untyped = Term.aconv_untyped o apply2 Thm.full_prop_of;

    val map_thms = no_refl (maps (fn bnf =>
       let val map_comp0 = map_comp0_of_bnf bnf RS sym
       in [map_comp0, map_comp0 RS rewrite_comp_comp, map_id0_of_bnf bnf] end)
      fp_or_nesting_bnfs) @
      remove eq_thm_prop_untyped (case_fp fp @{thm comp_assoc[symmetric]} @{thm comp_assoc})
      (map2 (fn thm => fn bnf =>
        @{thm type_copy_map_comp0_undo} OF
          (replicate 3 thm @ unfold_map [map_comp0_of_bnf bnf]) RS
          rewrite_comp_comp)
      type_definitions bnfs);

    val xtor_un_fold_thms =
      let
        val pre_fold_maps = mk_pre_fold_maps un_folds;
        fun mk_goals f xtor s smap fp_abs fp_rep abs rep =
          let
            val lhs = mk_co_comp f xtor;
            val rhs = mk_co_comp s smap;
          in
            HOLogic.mk_eq (lhs,
              mk_co_comp_abs_rep (co_alg_funT (fastype_of lhs)) (co_alg_funT (fastype_of rhs))
                fp_abs fp_rep abs rep rhs)
          end;

        val goals = @{map 8} mk_goals un_folds xtors fold_strs pre_fold_maps fp_abss fp_reps abss reps;

        val fp_un_folds = map (mk_pointfree lthy) (of_fp_res #xtor_un_fold_thms);

        val simps = flat [simp_thms, raw_xtor_un_fold_defs, map_defs, fp_un_folds,
          fp_un_fold_o_maps, map_thms, Rep_o_Abss];
      in
        Library.foldr1 HOLogic.mk_conj goals
        |> HOLogic.mk_Trueprop
        |> fold_rev Logic.all fold_strs
        |> (fn goal => Goal.prove_sorry raw_lthy [] [] goal
          (fn {context = ctxt, prems = _} => mk_xtor_un_fold_tac ctxt n simps))
        |> Thm.close_derivation
        |> Morphism.thm phi
        |> split_conj_thm
        |> map (fn thm => thm RS @{thm comp_eq_dest})
      end;

    val xtor_un_fold_o_maps = of_fp_res #xtor_un_fold_o_maps
      |> maps (fn thm => [thm, thm RS rewrite_comp_comp]);
    val xtor_un_fold_unique_thm =
      let
        val (fs, _) = names_lthy |> mk_Frees "f" resTs;
        val fold_maps = mk_pre_fold_maps fs;
        fun mk_prem f s mapx xtor fp_abs fp_rep abs rep =
          let
            val lhs = mk_co_comp f xtor;
            val rhs = mk_co_comp s mapx;
          in
            mk_Trueprop_eq (lhs,
              mk_co_comp_abs_rep (co_alg_funT (fastype_of lhs)) (co_alg_funT (fastype_of rhs))
                fp_abs fp_rep abs rep rhs)
          end;
        val prems = @{map 8} mk_prem fs fold_strs fold_maps xtors fp_abss fp_reps abss reps;
        val concl = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
          (map2 (curry HOLogic.mk_eq) fs un_folds));
        val vars = Variable.add_free_names raw_lthy concl [];
        val fp_un_fold_uniques0 = of_fp_res (split_conj_thm o #xtor_un_fold_unique)
          |> map (Drule.zero_var_indexes o unfold_thms lthy fp_map_defs);
        val names = fp_un_fold_uniques0
          |> map (Thm.concl_of #> HOLogic.dest_Trueprop
            #> HOLogic.dest_eq #> fst #> dest_Var #> fst);
        val inst = names ~~ map (Thm.cterm_of lthy) fs;
        val fp_un_fold_uniques = mutual_instantiate lthy inst fp_un_fold_uniques0;
        val map_arg_congs =
          map (fn bnf => mk_arg_cong lthy (live_of_bnf bnf) (map_of_bnf bnf)
            |> unfold_thms lthy (pre_map_defs @ simp_thms)) nesting_bnfs;
      in
        Goal.prove_sorry raw_lthy vars prems concl
          (mk_xtor_un_fold_unique_tac fp raw_xtor_un_fold_defs map_arg_congs xtor_un_fold_o_maps
            Rep_o_Abss fp_un_fold_uniques simp_thms map_thms map_defs)
          |> Thm.close_derivation
          |> case_fp fp I (fn thm => thm OF replicate n sym)
          |> Morphism.thm phi
      end;

    val ABs = As ~~ Bs;
    val XYs = Xs ~~ Ys;
    val ABphiTs = @{map 2} mk_pred2T As Bs;
    val XYphiTs = @{map 2} mk_pred2T Xs Ys;

    val ((ABphis, XYphis), _) = names_lthy
      |> mk_Frees "R" ABphiTs
      ||>> mk_Frees "S" XYphiTs;

    val pre_rels = @{map 2} (fn Ds => mk_rel_of_bnf Ds (As @ Xs) (Bs @ Ys)) Dss bnfs;

    val ns = map (fn i => length (filter (fn c => i = c) mutual_cliques)) mutual_cliques;

    val map_transfers = map (funpow live (fn thm => thm RS @{thm rel_funD})
        #> unfold_thms lthy pre_rel_defs)
      (map map_transfer_of_bnf bnfs);
    val fp_un_fold_transfers = map2 (fn n => funpow n (fn thm => thm RS @{thm rel_funD})
        #> unfold_thms lthy fp_rel_defs)
      ns (of_fp_res #xtor_un_fold_transfers);
    val pre_Abs_transfers = map (fn thm => @{thm Abs_transfer} OF [thm, thm]) type_definitions;
    val fp_Abs_transfers = map (fn thm => @{thm Abs_transfer} OF [thm, thm]) fp_type_definitions;
    val Abs_transfers = pre_Abs_transfers @ fp_Abs_transfers;

    fun tac {context = ctxt, prems = _} =
      mk_xtor_un_fold_transfer_tac ctxt n xtor_un_fold_defs rel_defs fp_un_fold_transfers
        map_transfers Abs_transfers fp_or_nesting_rel_eqs;

    val xtor_un_fold_transfer_thms =
      mk_xtor_co_iter_transfer_thms fp pre_rels XYphis XYphis rels ABphis
        xtor_un_folds' (map (subst_atomic_types (ABs @ XYs)) xtor_un_folds') tac lthy;

    val timer = time (timer "Nested-to-mutual (co)iteration");

    val xtor_maps = of_fp_res #xtor_maps;
    val xtor_rels = of_fp_res #xtor_rels;
    fun mk_Ts Cs = map (typ_subst_atomic (As ~~ Cs)) fpTs;
    val phi = Local_Theory.target_morphism lthy;
    val export = map (Morphism.term phi);
    val ((xtor_co_recs, (xtor_co_rec_thms, xtor_co_rec_unique_thm, xtor_co_rec_o_map_thms,
        xtor_co_rec_transfer_thms)), lthy) = lthy
      |> derive_xtor_co_recs fp bs mk_Ts (Dss, resDs) bnfs
        (export xtors) (export xtor_un_folds)
        xtor_un_fold_unique_thm xtor_un_fold_thms xtor_un_fold_transfer_thms xtor_maps xtor_rels
        (@{map 2} (curry (SOME o @{apply 2} (morph_absT_info phi))) fp_absT_infos absT_infos);

    val timer = time (timer "Nested-to-mutual (co)recursion");

    val common_notes =
      (case fp of
        Least_FP =>
        [(ctor_inductN, [xtor_co_induct_thm]),
         (ctor_rel_inductN, [xtor_rel_co_induct])]
      | Greatest_FP =>
        [(dtor_coinductN, [xtor_co_induct_thm]),
         (dtor_rel_coinductN, [xtor_rel_co_induct])])
      |> map (fn (thmN, thms) =>
        ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])]));

    val notes =
      (case fp of
        Least_FP => [(ctor_foldN, xtor_un_fold_thms)]
      | Greatest_FP => [(dtor_unfoldN, xtor_un_fold_thms)])
      |> map (apsnd (map single))
      |> maps (fn (thmN, thmss) =>
        map2 (fn b => fn thms =>
          ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])]))
        bs thmss);

    val lthy = lthy |> Config.get lthy bnf_internals
      ? snd o Local_Theory.notes (common_notes @ notes);

    (* These results are half broken. This is deliberate. We care only about those fields that are
       used by "primrec", "primcorecursive", and "datatype_compat". *)
    val fp_res =
      ({Ts = fpTs, bnfs = of_fp_res #bnfs, pre_bnfs = bnfs, absT_infos = absT_infos,
        dtors = dtors, ctors = ctors,
        xtor_un_folds = xtor_un_folds, xtor_co_recs = xtor_co_recs,
        xtor_co_induct = xtor_co_induct_thm,
        dtor_ctors = of_fp_res #dtor_ctors (*too general types*),
        ctor_dtors = of_fp_res #ctor_dtors (*too general types*),
        ctor_injects = of_fp_res #ctor_injects (*too general types*),
        dtor_injects = of_fp_res #dtor_injects (*too general types*),
        xtor_maps = of_fp_res #xtor_maps (*too general types and terms*),
        xtor_map_unique = xtor_un_fold_unique_thm (*wrong*),
        xtor_setss = of_fp_res #xtor_setss (*too general types and terms*),
        xtor_rels = of_fp_res #xtor_rels (*too general types and terms*),
        xtor_un_fold_thms = xtor_un_fold_thms,
        xtor_co_rec_thms = xtor_co_rec_thms,
        xtor_un_fold_unique = xtor_un_fold_unique_thm,
        xtor_co_rec_unique = xtor_co_rec_unique_thm,
        xtor_un_fold_o_maps = fp_un_fold_o_maps (*wrong*),
        xtor_co_rec_o_maps = xtor_co_rec_o_map_thms (*wrong*),
        xtor_un_fold_transfers = xtor_un_fold_transfer_thms,
        xtor_co_rec_transfers = xtor_co_rec_transfer_thms (*wrong*),
        xtor_rel_co_induct = xtor_rel_co_induct, dtor_set_inducts = []}
       |> morph_fp_result (Morphism.term_morphism "BNF" (singleton (Variable.polymorphic lthy))));
  in
    timer; (fp_res, lthy)
  end;

end;