src/HOL/Tools/BNF/bnf_fp_n2m.ML
author blanchet
Wed Apr 23 10:23:27 2014 +0200 (2014-04-23)
changeset 56650 1f9ab71d43a5
parent 56640 0a35354137a5
child 57303 498a62e65f5f
permissions -rw-r--r--
no need to make 'size' generation an interpretation -- overkill
     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     BNF_FP_Util.fp_sugar 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 force_typ ctxt T =
    28   Term.map_types Type_Infer.paramify_vars
    29   #> Type.constraint T
    30   #> Syntax.check_term ctxt
    31   #> singleton (Variable.polymorphic ctxt);
    32 
    33 fun mk_prod_map f g =
    34   let
    35     val ((fAT, fBT), fT) = `dest_funT (fastype_of f);
    36     val ((gAT, gBT), gT) = `dest_funT (fastype_of g);
    37   in
    38     Const (@{const_name map_prod},
    39       fT --> gT --> HOLogic.mk_prodT (fAT, gAT) --> HOLogic.mk_prodT (fBT, gBT)) $ f $ g
    40   end;
    41 
    42 fun mk_map_sum f g =
    43   let
    44     val ((fAT, fBT), fT) = `dest_funT (fastype_of f);
    45     val ((gAT, gBT), gT) = `dest_funT (fastype_of g);
    46   in
    47     Const (@{const_name map_sum}, fT --> gT --> mk_sumT (fAT, gAT) --> mk_sumT (fBT, gBT)) $ f $ g
    48   end;
    49 
    50 fun construct_mutualized_fp fp cliques fpTs (fp_sugars : fp_sugar list) bs resBs (resDs, Dss) bnfs
    51     (absT_infos : absT_info list) lthy =
    52   let
    53     fun of_fp_res get =
    54       map (fn {fp_res, fp_res_index, ...} => nth (get fp_res) fp_res_index) fp_sugars;
    55 
    56     fun mk_co_algT T U = case_fp fp (T --> U) (U --> T);
    57     fun co_swap pair = case_fp fp I swap pair;
    58     val mk_co_comp = HOLogic.mk_comp o co_swap;
    59     val co_productC = BNF_FP_Rec_Sugar_Util.case_fp fp @{type_name prod} @{type_name sum};
    60 
    61     val dest_co_algT = co_swap o dest_funT;
    62     val co_alg_argT = case_fp fp range_type domain_type;
    63     val co_alg_funT = case_fp fp domain_type range_type;
    64     val mk_co_product = curry (case_fp fp mk_convol mk_case_sum);
    65     val mk_map_co_product = case_fp fp mk_prod_map mk_map_sum;
    66     val co_proj1_const = case_fp fp (fst_const o fst) (uncurry Inl_const o dest_sumT o snd);
    67     val mk_co_productT = curry (case_fp fp HOLogic.mk_prodT mk_sumT);
    68     val dest_co_productT = case_fp fp HOLogic.dest_prodT dest_sumT;
    69     val rewrite_comp_comp = case_fp fp @{thm rewriteL_comp_comp} @{thm rewriteR_comp_comp};
    70 
    71     val fp_absT_infos = map #absT_info fp_sugars;
    72     val fp_bnfs = of_fp_res #bnfs;
    73     val pre_bnfs = map #pre_bnf fp_sugars;
    74     val nesty_bnfss = map (fn sugar => #nested_bnfs sugar @ #nesting_bnfs sugar) fp_sugars;
    75     val fp_nesty_bnfss = fp_bnfs :: nesty_bnfss;
    76     val fp_nesty_bnfs = distinct (op = o pairself T_of_bnf) (flat fp_nesty_bnfss);
    77 
    78     val fp_absTs = map #absT fp_absT_infos;
    79     val fp_repTs = map #repT fp_absT_infos;
    80     val fp_abss = map #abs fp_absT_infos;
    81     val fp_reps = map #rep fp_absT_infos;
    82     val fp_type_definitions = map #type_definition fp_absT_infos;
    83 
    84     val absTs = map #absT absT_infos;
    85     val repTs = map #repT absT_infos;
    86     val absTs' = map (Logic.type_map (singleton (Variable.polymorphic lthy))) absTs;
    87     val repTs' = map (Logic.type_map (singleton (Variable.polymorphic lthy))) repTs;
    88     val abss = map #abs absT_infos;
    89     val reps = map #rep absT_infos;
    90     val abs_inverses = map #abs_inverse absT_infos;
    91     val type_definitions = map #type_definition absT_infos;
    92 
    93     val n = length bnfs;
    94     val deads = fold (union (op =)) Dss resDs;
    95     val As = subtract (op =) deads (map TFree resBs);
    96     val names_lthy = fold Variable.declare_typ (As @ deads) lthy;
    97     val m = length As;
    98     val live = m + n;
    99 
   100     val ((Xs, Bs), names_lthy) = names_lthy
   101       |> mk_TFrees n
   102       ||>> mk_TFrees m;
   103 
   104     val allAs = As @ Xs;
   105     val allBs = Bs @ Xs;
   106     val phiTs = map2 mk_pred2T As Bs;
   107     val thetaBs = As ~~ Bs;
   108     val fpTs' = map (Term.typ_subst_atomic thetaBs) fpTs;
   109     val fold_thetaAs = Xs ~~ fpTs;
   110     val fold_thetaBs = Xs ~~ fpTs';
   111     val rec_theta = Xs ~~ map2 mk_co_productT fpTs Xs;
   112     val pre_phiTs = map2 mk_pred2T fpTs fpTs';
   113 
   114     val ((ctors, dtors), (xtor's, xtors)) =
   115       let
   116         val ctors = map2 (force_typ names_lthy o (fn T => dummyT --> T)) fpTs (of_fp_res #ctors);
   117         val dtors = map2 (force_typ names_lthy o (fn T => T --> dummyT)) fpTs (of_fp_res #dtors);
   118       in
   119         ((ctors, dtors), `(map (Term.subst_atomic_types thetaBs)) (case_fp fp ctors dtors))
   120       end;
   121 
   122     val absATs = map (domain_type o fastype_of) ctors;
   123     val absBTs = map (Term.typ_subst_atomic thetaBs) absATs;
   124     val xTs = map (domain_type o fastype_of) xtors;
   125     val yTs = map (domain_type o fastype_of) xtor's;
   126 
   127     val absAs = map3 (fn Ds => mk_abs o mk_T_of_bnf Ds allAs) Dss bnfs abss;
   128     val absBs = map3 (fn Ds => mk_abs o mk_T_of_bnf Ds allBs) Dss bnfs abss;
   129     val fp_repAs = map2 mk_rep absATs fp_reps;
   130     val fp_repBs = map2 mk_rep absBTs fp_reps;
   131 
   132     val (((((phis, phis'), pre_phis), xs), ys), names_lthy) = names_lthy
   133       |> mk_Frees' "R" phiTs
   134       ||>> mk_Frees "S" pre_phiTs
   135       ||>> mk_Frees "x" xTs
   136       ||>> mk_Frees "y" yTs;
   137 
   138     val rels =
   139       let
   140         fun find_rel T As Bs = fp_nesty_bnfss
   141           |> map (filter_out (curry (op = o pairself name_of_bnf) BNF_Comp.DEADID_bnf))
   142           |> get_first (find_first (fn bnf => Type.could_unify (T_of_bnf bnf, T)))
   143           |> Option.map (fn bnf =>
   144             let val live = live_of_bnf bnf;
   145             in (mk_rel live As Bs (rel_of_bnf bnf), live) end)
   146           |> the_default (HOLogic.eq_const T, 0);
   147 
   148         fun mk_rel (T as Type (_, Ts)) (Type (_, Us)) =
   149               let
   150                 val (rel, live) = find_rel T Ts Us;
   151                 val (Ts', Us') = fastype_of rel |> strip_typeN live |> fst |> map_split dest_pred2T;
   152                 val rels = map2 mk_rel Ts' Us';
   153               in
   154                 Term.list_comb (rel, rels)
   155               end
   156           | mk_rel (T as TFree _) _ = (nth phis (find_index (curry op = T) As)
   157               handle General.Subscript => HOLogic.eq_const T)
   158           | mk_rel _ _ = raise Fail "fpTs contains schematic type variables";
   159       in
   160         map2 (fold_rev Term.absfree phis' oo mk_rel) fpTs fpTs'
   161       end;
   162 
   163     val pre_rels = map2 (fn Ds => mk_rel_of_bnf Ds (As @ fpTs) (Bs @ fpTs')) Dss bnfs;
   164 
   165     val rel_unfolds = maps (no_refl o single o rel_def_of_bnf) pre_bnfs;
   166     val rel_xtor_co_inducts = of_fp_res (split_conj_thm o #rel_xtor_co_induct_thm)
   167       |> map (unfold_thms lthy (id_apply :: rel_unfolds));
   168 
   169     val rel_defs = map rel_def_of_bnf bnfs;
   170     val rel_monos = map rel_mono_of_bnf bnfs;
   171 
   172     fun cast castA castB pre_rel =
   173       let
   174         val castAB = mk_vimage2p (Term.subst_atomic_types fold_thetaAs castA)
   175           (Term.subst_atomic_types fold_thetaBs castB);
   176       in
   177         fold_rev (fold_rev Term.absdummy) [phiTs, pre_phiTs]
   178           (castAB $ Term.list_comb (pre_rel, map Bound (live - 1 downto 0)))
   179       end;
   180 
   181     val castAs = map2 (curry HOLogic.mk_comp) absAs fp_repAs;
   182     val castBs = map2 (curry HOLogic.mk_comp) absBs fp_repBs;
   183 
   184     val rel_xtor_co_induct_thm =
   185       mk_rel_xtor_co_induct_thm fp (map3 cast castAs castBs pre_rels) pre_phis rels phis xs ys xtors
   186         xtor's (mk_rel_xtor_co_induct_tactic fp abs_inverses rel_xtor_co_inducts rel_defs rel_monos)
   187         lthy;
   188 
   189     val rel_eqs = no_refl (map rel_eq_of_bnf fp_nesty_bnfs);
   190     val map_id0s = no_refl (map map_id0_of_bnf bnfs);
   191 
   192     val xtor_co_induct_thm =
   193       (case fp of
   194         Least_FP =>
   195           let
   196             val (Ps, names_lthy) = names_lthy
   197               |> mk_Frees "P" (map (fn T => T --> HOLogic.boolT) fpTs);
   198             fun mk_Grp_id P =
   199               let val T = domain_type (fastype_of P);
   200               in mk_Grp (HOLogic.Collect_const T $ P) (HOLogic.id_const T) end;
   201             val cts = map (SOME o certify lthy) (map HOLogic.eq_const As @ map mk_Grp_id Ps);
   202             fun mk_fp_type_copy_thms thm = map (curry op RS thm)
   203               @{thms type_copy_Abs_o_Rep type_copy_vimage2p_Grp_Rep};
   204             fun mk_type_copy_thms thm = map (curry op RS thm)
   205               @{thms type_copy_Rep_o_Abs type_copy_vimage2p_Grp_Abs};
   206           in
   207             cterm_instantiate_pos cts rel_xtor_co_induct_thm
   208             |> singleton (Proof_Context.export names_lthy lthy)
   209             |> unfold_thms lthy (@{thms eq_le_Grp_id_iff all_simps(1,2)[symmetric]} @ rel_eqs)
   210             |> funpow n (fn thm => thm RS spec)
   211             |> unfold_thms lthy (@{thm eq_alt} :: map rel_Grp_of_bnf bnfs @ map_id0s)
   212             |> unfold_thms lthy (@{thms vimage2p_id vimage2p_comp comp_apply comp_id
   213                Grp_id_mono_subst eqTrueI[OF subset_UNIV] simp_thms(22)} @
   214                maps mk_fp_type_copy_thms fp_type_definitions @
   215                maps mk_type_copy_thms type_definitions)
   216             |> unfold_thms lthy @{thms subset_iff mem_Collect_eq
   217                atomize_conjL[symmetric] atomize_all[symmetric] atomize_imp[symmetric]}
   218           end
   219       | Greatest_FP =>
   220           let
   221             val cts = NONE :: map (SOME o certify lthy) (map HOLogic.eq_const As);
   222           in
   223             cterm_instantiate_pos cts rel_xtor_co_induct_thm
   224             |> unfold_thms lthy (@{thms le_fun_def le_bool_def all_simps(1,2)[symmetric]} @ rel_eqs)
   225             |> funpow (2 * n) (fn thm => thm RS spec)
   226             |> Conv.fconv_rule (Object_Logic.atomize lthy)
   227             |> funpow n (fn thm => thm RS mp)
   228           end);
   229 
   230     val fold_preTs = map2 (fn Ds => mk_T_of_bnf Ds allAs) Dss bnfs;
   231     val rec_preTs = map (Term.typ_subst_atomic rec_theta) fold_preTs;
   232 
   233     val rec_strTs = map2 mk_co_algT rec_preTs Xs;
   234     val resTs = map2 mk_co_algT fpTs Xs;
   235 
   236     val ((rec_strs, rec_strs'), names_lthy) = names_lthy
   237       |> mk_Frees' "s" rec_strTs;
   238 
   239     val co_recs = of_fp_res #xtor_co_recs;
   240     val ns = map (length o #Ts o #fp_res) fp_sugars;
   241 
   242     fun substT rho (Type (@{type_name fun}, [T, U])) = substT rho T --> substT rho U
   243       | substT rho (Type (s, Ts)) = Type (s, map (typ_subst_nonatomic rho) Ts)
   244       | substT _ T = T;
   245 
   246     val typ_subst_nonatomic_sorted = fold_rev (typ_subst_nonatomic o single);
   247 
   248     fun foldT_of_recT recT =
   249       let
   250         val ((FTXs, Xs), TX) = strip_fun_type recT |>> map_split dest_co_algT;
   251         fun subst (Type (C, Ts as [_, X])) =
   252             if C = co_productC andalso member op = Xs X then X else Type (C, map subst Ts)
   253           | subst (Type (C, Ts)) = Type (C, map subst Ts)
   254           | subst T = T;
   255       in
   256         map2 (mk_co_algT o subst) FTXs Xs ---> TX
   257       end;
   258 
   259     fun force_rec i TU TU_rec raw_rec =
   260       let
   261         val thy = Proof_Context.theory_of lthy;
   262 
   263         val approx_rec = raw_rec
   264           |> force_typ names_lthy (replicate (nth ns i) dummyT ---> TU_rec);
   265         val subst = Term.typ_subst_atomic fold_thetaAs;
   266 
   267         fun mk_fp_absT_repT fp_repT fp_absT = mk_absT thy fp_repT fp_absT ooo mk_repT;
   268         val mk_fp_absT_repTs = map5 mk_fp_absT_repT fp_repTs fp_absTs absTs repTs;
   269 
   270         val fold_preTs' = mk_fp_absT_repTs (map subst fold_preTs);
   271 
   272         val fold_pre_deads_only_Ts =
   273           map (typ_subst_nonatomic_sorted (map (rpair dummyT) (As @ fpTs))) fold_preTs';
   274 
   275         val (clique, TUs) =
   276           map_split dest_co_algT (binder_fun_types (foldT_of_recT (fastype_of approx_rec)))
   277           |>> map subst
   278           |> `(fn (_, Ys) =>
   279             nth cliques (find_index (fn X => X = the (find_first (can dest_TFree) Ys)) Xs))
   280           ||> uncurry (map2 mk_co_algT);
   281         val cands = cliques ~~ map2 mk_co_algT fold_preTs' Xs;
   282         val js = find_indices (fn ((cl, cand), TU) =>
   283           cl = clique andalso Type.could_unify (TU, cand)) TUs cands;
   284         val Tpats = map (fn j => mk_co_algT (nth fold_pre_deads_only_Ts j) (nth Xs j)) js;
   285       in
   286         force_typ names_lthy (Tpats ---> TU) raw_rec
   287       end;
   288 
   289     fun mk_co_comp_abs_rep fp_absT absT fp_abs fp_rep abs rep t =
   290       case_fp fp (HOLogic.mk_comp (HOLogic.mk_comp (t, mk_abs absT abs), mk_rep fp_absT fp_rep))
   291         (HOLogic.mk_comp (mk_abs fp_absT fp_abs, HOLogic.mk_comp (mk_rep absT rep, t)));
   292 
   293     fun mk_rec b_opt recs lthy TU =
   294       let
   295         val thy = Proof_Context.theory_of lthy;
   296 
   297         val x = co_alg_argT TU;
   298         val i = find_index (fn T => x = T) Xs;
   299         val TUrec =
   300           (case find_first (fn f => body_fun_type (fastype_of f) = TU) recs of
   301             NONE => 
   302               force_rec i TU
   303                 (TU |> is_none b_opt ? substT (map2 mk_co_productT fpTs Xs ~~ Xs)) (nth co_recs i)
   304           | SOME f => f);
   305 
   306         val TUs = binder_fun_types (fastype_of TUrec);
   307 
   308         fun mk_s TU' =
   309           let
   310             fun mk_absT_fp_repT repT absT = mk_absT thy repT absT ooo mk_repT;
   311 
   312             val i = find_index (fn T => co_alg_argT TU' = T) Xs;
   313             val fp_abs = nth fp_abss i;
   314             val fp_rep = nth fp_reps i;
   315             val abs = nth abss i;
   316             val rep = nth reps i;
   317             val sF = co_alg_funT TU';
   318             val sF' =
   319               mk_absT_fp_repT (nth repTs' i) (nth absTs' i) (nth fp_absTs i) (nth fp_repTs i) sF
   320                 handle Term.TYPE _ => sF;
   321             val F = nth rec_preTs i;
   322             val s = nth rec_strs i;
   323           in
   324             if sF = F then s
   325             else if sF' = F then mk_co_comp_abs_rep sF sF' fp_abs fp_rep abs rep s
   326             else
   327               let
   328                 val smapT = replicate live dummyT ---> mk_co_algT sF' F;
   329                 fun hidden_to_unit t =
   330                   Term.subst_TVars (map (rpair HOLogic.unitT) (Term.add_tvar_names t [])) t;
   331                 val smap = map_of_bnf (nth bnfs i)
   332                   |> force_typ names_lthy smapT
   333                   |> hidden_to_unit;
   334                 val smap_argTs = strip_typeN live (fastype_of smap) |> fst;
   335                 fun mk_smap_arg TU =
   336                   (if domain_type TU = range_type TU then
   337                     HOLogic.id_const (domain_type TU)
   338                   else
   339                     let
   340                       val (TY, (U, X)) = TU |> dest_co_algT ||> dest_co_productT;
   341                       val T = mk_co_algT TY U;
   342                     in
   343                       (case try (force_typ names_lthy T o build_map lthy co_proj1_const o dest_funT) T of
   344                         SOME f => mk_co_product f
   345                           (fst (fst (mk_rec NONE recs lthy (mk_co_algT TY X))))
   346                       | NONE => mk_map_co_product
   347                           (build_map lthy co_proj1_const
   348                             (dest_funT (mk_co_algT (dest_co_productT TY |> fst) U)))
   349                           (HOLogic.id_const X))
   350                     end)
   351                 val smap_args = map mk_smap_arg smap_argTs;
   352               in
   353                 mk_co_comp_abs_rep sF sF' fp_abs fp_rep abs rep
   354                   (mk_co_comp (s, Term.list_comb (smap, smap_args)))
   355               end
   356           end;
   357         val t = Term.list_comb (TUrec, map mk_s TUs);
   358       in
   359         (case b_opt of
   360           NONE => ((t, Drule.dummy_thm), lthy)
   361         | SOME b => Local_Theory.define ((b, NoSyn), ((Binding.conceal (Thm.def_binding b), []),
   362             fold_rev Term.absfree rec_strs' t)) lthy |>> apsnd snd)
   363       end;
   364 
   365     val recN = case_fp fp ctor_recN dtor_corecN;
   366     fun mk_recs lthy =
   367       fold2 (fn TU => fn b => fn ((recs, defs), lthy) =>
   368         mk_rec (SOME b) recs lthy TU |>> (fn (f, d) => (f :: recs, d :: defs)))
   369       resTs (map (Binding.suffix_name ("_" ^ recN)) bs) (([], []), lthy)
   370       |>> apfst rev o apsnd rev;
   371     val ((raw_co_recs, raw_co_rec_defs), (lthy, raw_lthy)) = lthy
   372       |> mk_recs
   373       ||> `Local_Theory.restore;
   374 
   375     val phi = Proof_Context.export_morphism raw_lthy lthy;
   376 
   377     val co_recs = map (Morphism.term phi) raw_co_recs;
   378 
   379     val fp_rec_o_maps = of_fp_res #xtor_co_rec_o_map_thms
   380       |> maps (fn thm => [thm, thm RS rewrite_comp_comp]);
   381 
   382     val xtor_co_rec_thms =
   383       let
   384         val recs = map (fn r => Term.list_comb (r, rec_strs)) raw_co_recs;
   385         val rec_mapTs = co_swap (As @ fpTs, As @ map2 mk_co_productT fpTs Xs);
   386         val pre_rec_maps =
   387           map2 (fn Ds => fn bnf =>
   388             Term.list_comb (uncurry (mk_map_of_bnf Ds) rec_mapTs bnf,
   389               map HOLogic.id_const As @ map2 (mk_co_product o HOLogic.id_const) fpTs recs))
   390           Dss bnfs;
   391 
   392         fun mk_goals f xtor s smap fp_abs fp_rep abs rep =
   393           let
   394             val lhs = mk_co_comp (f, xtor);
   395             val rhs = mk_co_comp (s, smap);
   396           in
   397             HOLogic.mk_eq (lhs,
   398               mk_co_comp_abs_rep (co_alg_funT (fastype_of lhs)) (co_alg_funT (fastype_of rhs))
   399                 fp_abs fp_rep abs rep rhs)
   400           end;
   401 
   402         val goals = map8 mk_goals recs xtors rec_strs pre_rec_maps fp_abss fp_reps abss reps;
   403 
   404         val pre_map_defs = no_refl (map map_def_of_bnf bnfs);
   405         val fp_pre_map_defs = no_refl (map map_def_of_bnf pre_bnfs);
   406 
   407         val unfold_map = map (unfold_thms lthy (id_apply :: pre_map_defs));
   408 
   409         val fp_xtor_co_recs = map (mk_pointfree lthy) (of_fp_res #xtor_co_rec_thms);
   410 
   411         val fold_thms = case_fp fp @{thm comp_assoc} @{thm comp_assoc[symmetric]} ::
   412           map (fn thm => thm RS rewrite_comp_comp) @{thms map_prod.comp map_sum.comp} @
   413           @{thms id_apply comp_id id_comp map_prod.comp map_prod.id map_sum.comp map_sum.id};
   414         val rec_thms = fold_thms @ case_fp fp
   415           @{thms fst_convol map_prod_o_convol convol_o}
   416           @{thms case_sum_o_inj(1) case_sum_o_map_sum o_case_sum};
   417 
   418         val eq_thm_prop_untyped = Term.aconv_untyped o pairself Thm.full_prop_of;
   419 
   420         val map_thms = no_refl (maps (fn bnf =>
   421            let val map_comp0 = map_comp0_of_bnf bnf RS sym
   422            in [map_comp0, map_comp0 RS rewrite_comp_comp, map_id0_of_bnf bnf] end) fp_nesty_bnfs) @
   423           remove eq_thm_prop_untyped (case_fp fp @{thm comp_assoc[symmetric]} @{thm comp_assoc})
   424           (map2 (fn thm => fn bnf =>
   425             @{thm type_copy_map_comp0_undo} OF
   426               (replicate 3 thm @ unfold_map [map_comp0_of_bnf bnf]) RS
   427               rewrite_comp_comp)
   428           type_definitions bnfs);
   429 
   430         fun mk_Rep_o_Abs thm = thm RS @{thm type_copy_Rep_o_Abs} RS rewrite_comp_comp;
   431 
   432         val fp_Rep_o_Abss = map mk_Rep_o_Abs fp_type_definitions;
   433         val Rep_o_Abss = map mk_Rep_o_Abs type_definitions;
   434 
   435         fun tac {context = ctxt, prems = _} =
   436           unfold_thms_tac ctxt (flat [rec_thms, raw_co_rec_defs, pre_map_defs, fp_pre_map_defs,
   437             fp_xtor_co_recs, fp_rec_o_maps, map_thms, fp_Rep_o_Abss, Rep_o_Abss]) THEN
   438           CONJ_WRAP (K (HEADGOAL (rtac refl))) bnfs;
   439       in
   440         Library.foldr1 HOLogic.mk_conj goals
   441         |> HOLogic.mk_Trueprop
   442         |> fold_rev Logic.all rec_strs
   443         |> (fn goal => Goal.prove_sorry raw_lthy [] [] goal tac)
   444         |> Thm.close_derivation
   445         |> Morphism.thm phi
   446         |> split_conj_thm
   447         |> map (fn thm => thm RS @{thm comp_eq_dest})
   448       end;
   449 
   450     (* These results are half broken. This is deliberate. We care only about those fields that are
   451        used by "primrec", "primcorecursive", and "datatype_compat". *)
   452     val fp_res =
   453       ({Ts = fpTs, bnfs = of_fp_res #bnfs, dtors = dtors, ctors = ctors,
   454         xtor_co_recs = co_recs, xtor_co_induct = xtor_co_induct_thm,
   455         dtor_ctors = of_fp_res #dtor_ctors (*too general types*),
   456         ctor_dtors = of_fp_res #ctor_dtors (*too general types*),
   457         ctor_injects = of_fp_res #ctor_injects (*too general types*),
   458         dtor_injects = of_fp_res #dtor_injects (*too general types*),
   459         xtor_map_thms = of_fp_res #xtor_map_thms (*too general types and terms*),
   460         xtor_set_thmss = of_fp_res #xtor_set_thmss (*too general types and terms*),
   461         xtor_rel_thms = of_fp_res #xtor_rel_thms (*too general types and terms*),
   462         xtor_co_rec_thms = xtor_co_rec_thms,
   463         xtor_co_rec_o_map_thms = fp_rec_o_maps (*theorems about old constants*),
   464         rel_xtor_co_induct_thm = rel_xtor_co_induct_thm}
   465        |> morph_fp_result (Morphism.term_morphism "BNF" (singleton (Variable.polymorphic lthy))));
   466   in
   467     (fp_res, lthy)
   468   end;
   469 
   470 end;