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