src/HOL/Tools/BNF/bnf_fp_n2m.ML
author traytel
Thu Apr 07 17:56:22 2016 +0200 (2016-04-07)
changeset 62905 52c5a25e0c96
parent 62863 e0b894bba6ff
child 62907 9ad0bac25a84
permissions -rw-r--r--
derive (co)rec uniformly from (un)fold
     1 (*  Title:      HOL/Tools/BNF/bnf_fp_n2m.ML
     2     Author:     Dmitriy Traytel, TU Muenchen
     3     Copyright   2013
     4 
     5 Flattening of nested to mutual (co)recursion.
     6 *)
     7 
     8 signature BNF_FP_N2M =
     9 sig
    10   val construct_mutualized_fp: BNF_Util.fp_kind -> int list -> typ list ->
    11     (int * BNF_FP_Util.fp_result) list -> binding list -> (string * sort) list ->
    12     typ list * typ list list -> BNF_Def.bnf list -> BNF_Comp.absT_info list -> local_theory ->
    13     BNF_FP_Util.fp_result * local_theory
    14 end;
    15 
    16 structure BNF_FP_N2M : BNF_FP_N2M =
    17 struct
    18 
    19 open BNF_Def
    20 open BNF_Util
    21 open BNF_Comp
    22 open BNF_FP_Util
    23 open BNF_FP_Def_Sugar
    24 open BNF_Tactics
    25 open BNF_FP_N2M_Tactics
    26 
    27 fun mk_prod_map f g =
    28   let
    29     val ((fAT, fBT), fT) = `dest_funT (fastype_of f);
    30     val ((gAT, gBT), gT) = `dest_funT (fastype_of g);
    31   in
    32     Const (@{const_name map_prod},
    33       fT --> gT --> HOLogic.mk_prodT (fAT, gAT) --> HOLogic.mk_prodT (fBT, gBT)) $ f $ g
    34   end;
    35 
    36 fun mk_map_sum f g =
    37   let
    38     val ((fAT, fBT), fT) = `dest_funT (fastype_of f);
    39     val ((gAT, gBT), gT) = `dest_funT (fastype_of g);
    40   in
    41     Const (@{const_name map_sum}, fT --> gT --> mk_sumT (fAT, gAT) --> mk_sumT (fBT, gBT)) $ f $ g
    42   end;
    43 
    44 fun construct_mutualized_fp fp flat_mutual_cliques fpTs indexed_fp_ress bs resBs (resDs, Dss) bnfs
    45     (absT_infos : absT_info list) lthy =
    46   let
    47     val time = time lthy;
    48     val timer = time (Timer.startRealTimer ());
    49 
    50     val b_names = map Binding.name_of bs;
    51     val b_name = mk_common_name b_names;
    52     val b = Binding.name b_name;
    53 
    54     fun of_fp_res get = map (uncurry nth o swap o apsnd get) indexed_fp_ress;
    55     fun mk_co_algT T U = case_fp fp (T --> U) (U --> T);
    56     fun co_swap pair = case_fp fp I swap pair;
    57     val mk_co_comp = HOLogic.mk_comp o co_swap;
    58     val co_productC = case_fp fp @{type_name prod} @{type_name sum};
    59 
    60     val dest_co_algT = co_swap o dest_funT;
    61     val co_alg_argT = case_fp fp range_type domain_type;
    62     val co_alg_funT = case_fp fp domain_type range_type;
    63     val mk_co_product = curry (case_fp fp mk_convol mk_case_sum);
    64     val mk_map_co_product = case_fp fp mk_prod_map mk_map_sum;
    65     val co_proj1_const = case_fp fp (fst_const o fst) (uncurry Inl_const o dest_sumT o snd);
    66     val mk_co_productT = curry (case_fp fp HOLogic.mk_prodT mk_sumT);
    67     val dest_co_productT = case_fp fp HOLogic.dest_prodT dest_sumT;
    68     val rewrite_comp_comp = case_fp fp @{thm rewriteL_comp_comp} @{thm rewriteR_comp_comp};
    69 
    70     val fp_absT_infos = of_fp_res #absT_infos;
    71     val fp_bnfs = of_fp_res #bnfs;
    72     val pre_bnfs = of_fp_res #pre_bnfs;
    73 
    74     val fp_absTs = map #absT fp_absT_infos;
    75     val fp_repTs = map #repT fp_absT_infos;
    76     val fp_abss = map #abs fp_absT_infos;
    77     val fp_reps = map #rep fp_absT_infos;
    78     val fp_type_definitions = map #type_definition fp_absT_infos;
    79 
    80     val absTs = map #absT absT_infos;
    81     val repTs = map #repT absT_infos;
    82     val absTs' = map (Logic.type_map (singleton (Variable.polymorphic lthy))) absTs;
    83     val repTs' = map (Logic.type_map (singleton (Variable.polymorphic lthy))) repTs;
    84     val abss = map #abs absT_infos;
    85     val reps = map #rep absT_infos;
    86     val abs_inverses = map #abs_inverse absT_infos;
    87     val type_definitions = map #type_definition absT_infos;
    88 
    89     val n = length bnfs;
    90     val deads = fold (union (op =)) Dss resDs;
    91     val As = subtract (op =) deads (map TFree resBs);
    92     val names_lthy = fold Variable.declare_typ (As @ deads) lthy;
    93     val m = length As;
    94     val live = m + n;
    95 
    96     val ((Xs, Bs), names_lthy) = names_lthy
    97       |> mk_TFrees n
    98       ||>> mk_TFrees m;
    99 
   100     val allAs = As @ Xs;
   101     val allBs = Bs @ Xs;
   102     val phiTs = map2 mk_pred2T As Bs;
   103     val thetaBs = As ~~ Bs;
   104     val fpTs' = map (Term.typ_subst_atomic thetaBs) fpTs;
   105     val fold_thetaAs = Xs ~~ fpTs;
   106     val fold_thetaBs = Xs ~~ fpTs';
   107     val rec_theta = Xs ~~ map2 mk_co_productT fpTs Xs;
   108     val pre_phiTs = map2 mk_pred2T fpTs fpTs';
   109 
   110     val ((ctors, dtors), (xtor's, xtors)) =
   111       let
   112         val ctors = map2 (force_typ names_lthy o (fn T => dummyT --> T)) fpTs (of_fp_res #ctors);
   113         val dtors = map2 (force_typ names_lthy o (fn T => T --> dummyT)) fpTs (of_fp_res #dtors);
   114       in
   115         ((ctors, dtors), `(map (Term.subst_atomic_types thetaBs)) (case_fp fp ctors dtors))
   116       end;
   117 
   118     val absATs = map (domain_type o fastype_of) ctors;
   119     val absBTs = map (Term.typ_subst_atomic thetaBs) absATs;
   120     val xTs = map (domain_type o fastype_of) xtors;
   121     val yTs = map (domain_type o fastype_of) xtor's;
   122 
   123     val absAs = @{map 3} (fn Ds => mk_abs o mk_T_of_bnf Ds allAs) Dss bnfs abss;
   124     val absBs = @{map 3} (fn Ds => mk_abs o mk_T_of_bnf Ds allBs) Dss bnfs abss;
   125     val fp_repAs = map2 mk_rep absATs fp_reps;
   126     val fp_repBs = map2 mk_rep absBTs fp_reps;
   127 
   128     val typ_subst_nonatomic_sorted = fold_rev (typ_subst_nonatomic o single);
   129     val sorted_theta = sort (int_ord o apply2 (Term.size_of_typ o fst)) (fpTs ~~ Xs)
   130     val sorted_fpTs = map fst sorted_theta;
   131 
   132     val nesting_bnfs = nesting_bnfs lthy
   133       [[map (typ_subst_nonatomic_sorted (rev sorted_theta) o range_type o fastype_of) fp_repAs]]
   134       allAs;
   135     val fp_or_nesting_bnfs = distinct (op = o apply2 T_of_bnf) (fp_bnfs @ nesting_bnfs);
   136 
   137     val (((((phis, phis'), pre_phis), xs), ys), names_lthy) = names_lthy
   138       |> mk_Frees' "R" phiTs
   139       ||>> mk_Frees "S" pre_phiTs
   140       ||>> mk_Frees "x" xTs
   141       ||>> mk_Frees "y" yTs;
   142 
   143     val rels =
   144       let
   145         fun find_rel T As Bs = fp_or_nesting_bnfs
   146           |> filter_out (curry (op = o apply2 name_of_bnf) BNF_Comp.DEADID_bnf)
   147           |> find_first (fn bnf => Type.could_unify (T_of_bnf bnf, T))
   148           |> Option.map (fn bnf =>
   149             let val live = live_of_bnf bnf;
   150             in (mk_rel live As Bs (rel_of_bnf bnf), live) end)
   151           |> the_default (HOLogic.eq_const T, 0);
   152 
   153         fun mk_rel (T as Type (_, Ts)) (Type (_, Us)) =
   154               let
   155                 val (rel, live) = find_rel T Ts Us;
   156                 val (Ts', Us') = fastype_of rel |> strip_typeN live |> fst |> map_split dest_pred2T;
   157                 val rels = map2 mk_rel Ts' Us';
   158               in
   159                 Term.list_comb (rel, rels)
   160               end
   161           | mk_rel (T as TFree _) _ = (nth phis (find_index (curry op = T) As)
   162               handle General.Subscript => HOLogic.eq_const T)
   163           | mk_rel _ _ = raise Fail "fpTs contains schematic type variables";
   164       in
   165         map2 (fold_rev Term.absfree phis' oo mk_rel) fpTs fpTs'
   166       end;
   167 
   168     val pre_rels = map2 (fn Ds => mk_rel_of_bnf Ds (As @ fpTs) (Bs @ fpTs')) Dss bnfs;
   169 
   170     val rel_unfolds = maps (no_refl o single o rel_def_of_bnf) pre_bnfs;
   171     val rel_xtor_co_inducts = of_fp_res (split_conj_thm o #xtor_rel_co_induct)
   172       |> map (zero_var_indexes o unfold_thms lthy (id_apply :: rel_unfolds));
   173 
   174     val rel_defs = map rel_def_of_bnf bnfs;
   175     val rel_monos = map rel_mono_of_bnf bnfs;
   176 
   177     fun cast castA castB pre_rel =
   178       let
   179         val castAB = mk_vimage2p (Term.subst_atomic_types fold_thetaAs castA)
   180           (Term.subst_atomic_types fold_thetaBs castB);
   181       in
   182         fold_rev (fold_rev Term.absdummy) [phiTs, pre_phiTs]
   183           (castAB $ Term.list_comb (pre_rel, map Bound (live - 1 downto 0)))
   184       end;
   185 
   186     val castAs = map2 (curry HOLogic.mk_comp) absAs fp_repAs;
   187     val castBs = map2 (curry HOLogic.mk_comp) absBs fp_repBs;
   188 
   189     val fp_or_nesting_rel_eqs = no_refl (map rel_eq_of_bnf fp_or_nesting_bnfs);
   190     val fp_or_nesting_rel_monos = map rel_mono_of_bnf fp_or_nesting_bnfs;
   191 
   192     val rel_xtor_co_inducts_inst =
   193       let
   194         val extract =
   195           case_fp fp (snd o Term.dest_comb) (snd o Term.dest_comb o fst o Term.dest_comb);
   196         val raw_phis = map (extract o HOLogic.dest_Trueprop o Thm.concl_of) rel_xtor_co_inducts;
   197         val thetas =
   198           AList.group (op =)
   199             (flat_mutual_cliques ~~
   200               map (fn (t, u) => (#1 (dest_Var t), Thm.cterm_of lthy u)) (raw_phis ~~ pre_phis));
   201       in
   202         map2 (infer_instantiate lthy o the o AList.lookup (op =) thetas)
   203         flat_mutual_cliques rel_xtor_co_inducts
   204       end
   205 
   206     val xtor_rel_co_induct =
   207       mk_xtor_rel_co_induct_thm fp (@{map 3} cast castAs castBs pre_rels) pre_phis rels phis xs ys
   208         xtors xtor's (mk_rel_xtor_co_induct_tactic fp abs_inverses rel_xtor_co_inducts_inst rel_defs
   209           rel_monos fp_or_nesting_rel_eqs fp_or_nesting_rel_monos)
   210         lthy;
   211 
   212     val map_id0s = no_refl (map map_id0_of_bnf bnfs);
   213 
   214     val xtor_co_induct_thm =
   215       (case fp of
   216         Least_FP =>
   217           let
   218             val (Ps, names_lthy) = names_lthy
   219               |> mk_Frees "P" (map (fn T => T --> HOLogic.boolT) fpTs);
   220             fun mk_Grp_id P =
   221               let val T = domain_type (fastype_of P);
   222               in mk_Grp (HOLogic.Collect_const T $ P) (HOLogic.id_const T) end;
   223             val cts =
   224               map (SOME o Thm.cterm_of names_lthy) (map HOLogic.eq_const As @ map mk_Grp_id Ps);
   225             fun mk_fp_type_copy_thms thm = map (curry op RS thm)
   226               @{thms type_copy_Abs_o_Rep type_copy_vimage2p_Grp_Rep};
   227             fun mk_type_copy_thms thm = map (curry op RS thm)
   228               @{thms type_copy_Rep_o_Abs type_copy_vimage2p_Grp_Abs};
   229           in
   230             infer_instantiate' names_lthy cts xtor_rel_co_induct
   231             |> singleton (Proof_Context.export names_lthy lthy)
   232             |> unfold_thms lthy (@{thms eq_le_Grp_id_iff all_simps(1,2)[symmetric]} @
   233                 fp_or_nesting_rel_eqs)
   234             |> funpow n (fn thm => thm RS spec)
   235             |> unfold_thms lthy (@{thm eq_alt} :: map rel_Grp_of_bnf bnfs @ map_id0s)
   236             |> unfold_thms lthy (@{thms vimage2p_id vimage2p_comp comp_apply comp_id
   237                Grp_id_mono_subst eqTrueI[OF subset_UNIV] simp_thms(22)} @
   238                maps mk_fp_type_copy_thms fp_type_definitions @
   239                maps mk_type_copy_thms type_definitions)
   240             |> unfold_thms lthy @{thms subset_iff mem_Collect_eq
   241                atomize_conjL[symmetric] atomize_all[symmetric] atomize_imp[symmetric]}
   242           end
   243       | Greatest_FP =>
   244           let
   245             val cts = NONE :: map (SOME o Thm.cterm_of lthy) (map HOLogic.eq_const As);
   246           in
   247             infer_instantiate' lthy cts xtor_rel_co_induct
   248             |> unfold_thms lthy (@{thms le_fun_def le_bool_def all_simps(1,2)[symmetric]} @
   249                 fp_or_nesting_rel_eqs)
   250             |> funpow (2 * n) (fn thm => thm RS spec)
   251             |> Conv.fconv_rule (Object_Logic.atomize lthy)
   252             |> funpow n (fn thm => thm RS mp)
   253           end);
   254 
   255     val timer = time (timer "Nested-to-mutual (co)induction");
   256 
   257     val fold_preTs = map2 (fn Ds => mk_T_of_bnf Ds allAs) Dss bnfs;
   258     val rec_preTs = map (Term.typ_subst_atomic rec_theta) fold_preTs;
   259 
   260     val rec_strTs = map2 mk_co_algT rec_preTs Xs;
   261     val resTs = map2 mk_co_algT fpTs Xs;
   262 
   263     val ((rec_strs, rec_strs'), names_lthy) = names_lthy
   264       |> mk_Frees' "s" rec_strTs;
   265 
   266     val xtor_co_recs = of_fp_res #xtor_co_recs;
   267     val ns = map (length o #Ts o snd) indexed_fp_ress;
   268 
   269     fun foldT_of_recT recT =
   270       let
   271         val ((FTXs, Ys), TX) = strip_fun_type recT |>> map_split dest_co_algT;
   272         val Zs = union op = Xs Ys;
   273         fun subst (Type (C, Ts as [_, X])) =
   274             if C = co_productC andalso member op = Zs X then X else Type (C, map subst Ts)
   275           | subst (Type (C, Ts)) = Type (C, map subst Ts)
   276           | subst T = T;
   277       in
   278         map2 (mk_co_algT o subst) FTXs Ys ---> TX
   279       end;
   280 
   281     fun force_rec i TU raw_rec =
   282       let
   283         val thy = Proof_Context.theory_of lthy;
   284 
   285         val approx_rec = raw_rec
   286           |> force_typ names_lthy (replicate (nth ns i) dummyT ---> TU);
   287         val subst = Term.typ_subst_atomic fold_thetaAs;
   288 
   289         fun mk_fp_absT_repT fp_repT fp_absT = mk_absT thy fp_repT fp_absT ooo mk_repT;
   290         val mk_fp_absT_repTs = @{map 5} mk_fp_absT_repT fp_repTs fp_absTs absTs repTs;
   291 
   292         val fold_preTs' = mk_fp_absT_repTs (map subst fold_preTs);
   293 
   294         val fold_pre_deads_only_Ts =
   295           map (typ_subst_nonatomic_sorted (map (rpair dummyT) (As @ sorted_fpTs))) fold_preTs';
   296 
   297         val (mutual_clique, TUs) =
   298           map_split dest_co_algT (binder_fun_types (foldT_of_recT (fastype_of approx_rec)))
   299           |>> map subst
   300           |> `(fn (_, Ys) => nth flat_mutual_cliques
   301             (find_index (fn X => X = the (find_first (can dest_TFree) Ys)) Xs))
   302           ||> uncurry (map2 mk_co_algT);
   303         val cands = flat_mutual_cliques ~~ map2 mk_co_algT fold_preTs' Xs;
   304         val js = find_indices (fn ((cl, cand), TU) =>
   305           cl = mutual_clique andalso Type.could_unify (TU, cand)) TUs cands;
   306         val Tpats = map (fn j => mk_co_algT (nth fold_pre_deads_only_Ts j) (nth Xs j)) js;
   307       in
   308         force_typ names_lthy (Tpats ---> TU) raw_rec
   309       end;
   310 
   311     fun mk_co_comp_abs_rep fp_absT absT fp_abs fp_rep abs rep t =
   312       case_fp fp (HOLogic.mk_comp (HOLogic.mk_comp (t, mk_abs absT abs), mk_rep fp_absT fp_rep))
   313         (HOLogic.mk_comp (mk_abs fp_absT fp_abs, HOLogic.mk_comp (mk_rep absT rep, t)));
   314 
   315     fun mk_rec b_opt recs lthy TU =
   316       let
   317         val thy = Proof_Context.theory_of lthy;
   318 
   319         val x = co_alg_argT TU;
   320         val i = find_index (fn T => x = T) Xs;
   321         val TUrec =
   322           (case find_first (fn f => body_fun_type (fastype_of f) = TU) recs of
   323             NONE => force_rec i TU (nth xtor_co_recs i)
   324           | SOME f => f);
   325 
   326         val TUs = binder_fun_types (fastype_of TUrec);
   327 
   328         fun mk_s TU' =
   329           let
   330             fun mk_absT_fp_repT repT absT = mk_absT thy repT absT ooo mk_repT;
   331 
   332             val i = find_index (fn T => co_alg_argT TU' = T) Xs;
   333             val fp_abs = nth fp_abss i;
   334             val fp_rep = nth fp_reps i;
   335             val abs = nth abss i;
   336             val rep = nth reps i;
   337             val sF = co_alg_funT TU';
   338             val sF' =
   339               mk_absT_fp_repT (nth repTs' i) (nth absTs' i) (nth fp_absTs i) (nth fp_repTs i) sF
   340                 handle Term.TYPE _ => sF;
   341             val F = nth rec_preTs i;
   342             val s = nth rec_strs i;
   343           in
   344             if sF = F then s
   345             else if sF' = F then mk_co_comp_abs_rep sF sF' fp_abs fp_rep abs rep s
   346             else
   347               let
   348                 val smapT = replicate live dummyT ---> mk_co_algT sF' F;
   349                 fun hidden_to_unit t =
   350                   Term.subst_TVars (map (rpair HOLogic.unitT) (Term.add_tvar_names t [])) t;
   351                 val smap = map_of_bnf (nth bnfs i)
   352                   |> force_typ names_lthy smapT
   353                   |> hidden_to_unit;
   354                 val smap_argTs = strip_typeN live (fastype_of smap) |> fst;
   355                 fun mk_smap_arg T_to_U =
   356                   (if domain_type T_to_U = range_type T_to_U then
   357                     HOLogic.id_const (domain_type T_to_U)
   358                   else
   359                     let
   360                       val (TY, (U, X)) = T_to_U |> dest_co_algT ||> dest_co_productT;
   361                       val T = mk_co_algT TY U;
   362                       fun mk_co_proj TU =
   363                         build_map lthy [] (fn TU =>
   364                           let val ((T1, T2), U) = TU |> co_swap |>> dest_co_productT in
   365                             if T1 = U then co_proj1_const TU
   366                             else mk_co_comp (mk_co_proj (co_swap (T1, U)),
   367                               co_proj1_const (co_swap (mk_co_productT T1 T2, T1)))
   368                           end)
   369                           TU;
   370                       fun default () =
   371                         mk_co_product (mk_co_proj (dest_funT T))
   372                           (fst (fst (mk_rec NONE recs lthy (mk_co_algT TY X))));
   373                     in
   374                       if can dest_co_productT TY then
   375                         mk_map_co_product (mk_co_proj (co_swap (dest_co_productT TY |> fst, U)))
   376                           (HOLogic.id_const X)
   377                         handle TYPE _ => default () (*N2M involving "prod" type*)
   378                       else
   379                         default ()
   380                     end)
   381                 val smap_args = map mk_smap_arg smap_argTs;
   382               in
   383                 mk_co_comp_abs_rep sF sF' fp_abs fp_rep abs rep
   384                   (mk_co_comp (s, Term.list_comb (smap, smap_args)))
   385               end
   386           end;
   387         val t = Term.list_comb (TUrec, map mk_s TUs);
   388       in
   389         (case b_opt of
   390           NONE => ((t, Drule.dummy_thm), lthy)
   391         | SOME b => Local_Theory.define ((b, NoSyn), ((Binding.concealed (Thm.def_binding b), []),
   392             fold_rev Term.absfree rec_strs' t)) lthy |>> apsnd snd)
   393       end;
   394 
   395     val recN = case_fp fp ctor_recN dtor_corecN;
   396     fun mk_recs lthy =
   397       fold2 (fn TU => fn b => fn ((recs, defs), lthy) =>
   398         mk_rec (SOME b) recs lthy TU |>> (fn (f, d) => (f :: recs, d :: defs)))
   399       resTs (map (Binding.suffix_name ("_" ^ recN)) bs) (([], []), lthy)
   400       |>> map_prod rev rev;
   401     val ((raw_xtor_co_recs, raw_xtor_co_rec_defs), (lthy, raw_lthy)) = lthy
   402       |> Local_Theory.open_target |> snd
   403       |> mk_recs
   404       ||> `Local_Theory.close_target;
   405 
   406     val phi = Proof_Context.export_morphism raw_lthy lthy;
   407 
   408     val xtor_co_recs = map (Morphism.term phi) raw_xtor_co_recs;
   409 
   410     val fp_rec_o_maps = of_fp_res #xtor_co_rec_o_maps
   411       |> maps (fn thm => [thm, thm RS rewrite_comp_comp]);
   412 
   413     val xtor_co_rec_thms =
   414       let
   415         val recs = map (fn r => Term.list_comb (r, rec_strs)) raw_xtor_co_recs;
   416         val rec_mapTs = co_swap (As @ fpTs, As @ map2 mk_co_productT fpTs Xs);
   417         val pre_rec_maps =
   418           map2 (fn Ds => fn bnf =>
   419             Term.list_comb (uncurry (mk_map_of_bnf Ds) rec_mapTs bnf,
   420               map HOLogic.id_const As @ map2 (mk_co_product o HOLogic.id_const) fpTs recs))
   421           Dss bnfs;
   422 
   423         fun mk_goals f xtor s smap fp_abs fp_rep abs rep =
   424           let
   425             val lhs = mk_co_comp (f, xtor);
   426             val rhs = mk_co_comp (s, smap);
   427           in
   428             HOLogic.mk_eq (lhs,
   429               mk_co_comp_abs_rep (co_alg_funT (fastype_of lhs)) (co_alg_funT (fastype_of rhs))
   430                 fp_abs fp_rep abs rep rhs)
   431           end;
   432 
   433         val goals = @{map 8} mk_goals recs xtors rec_strs pre_rec_maps fp_abss fp_reps abss reps;
   434 
   435         val pre_map_defs = no_refl (map map_def_of_bnf bnfs);
   436         val fp_pre_map_defs = no_refl (map map_def_of_bnf pre_bnfs);
   437 
   438         val unfold_map = map (unfold_thms lthy (id_apply :: pre_map_defs));
   439 
   440         val fp_xtor_co_recs = map (mk_pointfree lthy) (of_fp_res #xtor_co_rec_thms);
   441 
   442         val fold_thms = case_fp fp @{thm comp_assoc} @{thm comp_assoc[symmetric]} ::
   443           map (fn thm => thm RS rewrite_comp_comp) @{thms map_prod.comp map_sum.comp} @
   444           @{thms id_apply comp_id id_comp map_prod.comp map_prod.id map_sum.comp map_sum.id};
   445         val rec_thms = fold_thms @ case_fp fp
   446           @{thms fst_convol map_prod_o_convol convol_o fst_comp_map_prod}
   447           @{thms case_sum_o_inj(1) case_sum_o_map_sum o_case_sum map_sum_o_inj(1)};
   448 
   449         val eq_thm_prop_untyped = Term.aconv_untyped o apply2 Thm.full_prop_of;
   450 
   451         val map_thms = no_refl (maps (fn bnf =>
   452            let val map_comp0 = map_comp0_of_bnf bnf RS sym
   453            in [map_comp0, map_comp0 RS rewrite_comp_comp, map_id0_of_bnf bnf] end)
   454           fp_or_nesting_bnfs) @
   455           remove eq_thm_prop_untyped (case_fp fp @{thm comp_assoc[symmetric]} @{thm comp_assoc})
   456           (map2 (fn thm => fn bnf =>
   457             @{thm type_copy_map_comp0_undo} OF
   458               (replicate 3 thm @ unfold_map [map_comp0_of_bnf bnf]) RS
   459               rewrite_comp_comp)
   460           type_definitions bnfs);
   461 
   462         fun mk_Rep_o_Abs thm = (thm RS @{thm type_copy_Rep_o_Abs})
   463           |> (fn thm => [thm, thm RS rewrite_comp_comp]);
   464 
   465         val fp_Rep_o_Abss = maps mk_Rep_o_Abs fp_type_definitions;
   466         val Rep_o_Abss = maps mk_Rep_o_Abs type_definitions;
   467 
   468         fun tac {context = ctxt, prems = _} =
   469           unfold_thms_tac ctxt (flat [rec_thms, raw_xtor_co_rec_defs, pre_map_defs,
   470             fp_pre_map_defs, fp_xtor_co_recs, fp_rec_o_maps, map_thms, fp_Rep_o_Abss,
   471             Rep_o_Abss]) THEN
   472           CONJ_WRAP (K (HEADGOAL (rtac ctxt refl))) bnfs;
   473       in
   474         Library.foldr1 HOLogic.mk_conj goals
   475         |> HOLogic.mk_Trueprop
   476         |> fold_rev Logic.all rec_strs
   477         |> (fn goal => Goal.prove_sorry raw_lthy [] [] goal tac)
   478         |> Thm.close_derivation
   479         |> Morphism.thm phi
   480         |> split_conj_thm
   481         |> map (fn thm => thm RS @{thm comp_eq_dest})
   482       end;
   483 
   484     val timer = time (timer "Nested-to-mutual (co)recursion");
   485 
   486     val common_notes =
   487       (case fp of
   488         Least_FP =>
   489         [(ctor_inductN, [xtor_co_induct_thm]),
   490          (ctor_rel_inductN, [xtor_rel_co_induct])]
   491       | Greatest_FP =>
   492         [(dtor_coinductN, [xtor_co_induct_thm]),
   493          (dtor_rel_coinductN, [xtor_rel_co_induct])])
   494       |> map (fn (thmN, thms) =>
   495         ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])]));
   496 
   497     val notes =
   498       (case fp of
   499         Least_FP => [(ctor_recN, xtor_co_rec_thms)]
   500       | Greatest_FP => [(dtor_corecN, xtor_co_rec_thms)])
   501       |> map (apsnd (map single))
   502       |> maps (fn (thmN, thmss) =>
   503         map2 (fn b => fn thms =>
   504           ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])]))
   505         bs thmss);
   506 
   507     val lthy = lthy |> Config.get lthy bnf_internals
   508       ? snd o Local_Theory.notes (common_notes @ notes);
   509 
   510     (* These results are half broken. This is deliberate. We care only about those fields that are
   511        used by "primrec", "primcorecursive", and "datatype_compat". *)
   512     val fp_res =
   513       ({Ts = fpTs, bnfs = of_fp_res #bnfs, pre_bnfs = bnfs, absT_infos = absT_infos,
   514         dtors = dtors, ctors = ctors,
   515         xtor_un_folds_legacy = xtor_co_recs (*wrong*), xtor_co_recs = xtor_co_recs,
   516         xtor_co_induct = xtor_co_induct_thm,
   517         dtor_ctors = of_fp_res #dtor_ctors (*too general types*),
   518         ctor_dtors = of_fp_res #ctor_dtors (*too general types*),
   519         ctor_injects = of_fp_res #ctor_injects (*too general types*),
   520         dtor_injects = of_fp_res #dtor_injects (*too general types*),
   521         xtor_maps = of_fp_res #xtor_maps (*too general types and terms*),
   522         xtor_map_unique = TrueI (*wrong*),
   523         xtor_setss = of_fp_res #xtor_setss (*too general types and terms*),
   524         xtor_rels = of_fp_res #xtor_rels (*too general types and terms*),
   525         xtor_un_fold_thms_legacy = xtor_co_rec_thms (*wrong*),
   526         xtor_co_rec_thms = xtor_co_rec_thms (*too general types and terms*),
   527         xtor_un_fold_unique_legacy = TrueI (*too general types and terms*),
   528         xtor_co_rec_unique = TrueI (*wrong*),
   529         xtor_un_fold_o_maps_legacy = fp_rec_o_maps (*wrong*),
   530         xtor_co_rec_o_maps = fp_rec_o_maps (*theorems about old constants*),
   531         xtor_un_fold_transfers_legacy = [], xtor_co_rec_transfers = [],
   532         xtor_rel_co_induct = xtor_rel_co_induct, dtor_set_inducts = []}
   533        |> morph_fp_result (Morphism.term_morphism "BNF" (singleton (Variable.polymorphic lthy))));
   534   in
   535     timer; (fp_res, lthy)
   536   end;
   537 
   538 end;