src/HOL/Tools/BNF/bnf_fp_n2m.ML
changeset 55060 3105434fb02f
parent 55058 4e700eb471d4
child 55061 a0adf838e2d1
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Tools/BNF/bnf_fp_n2m.ML	Mon Jan 20 18:24:56 2014 +0100
     1.3 @@ -0,0 +1,378 @@
     1.4 +(*  Title:      HOL/BNF/Tools/bnf_fp_n2m.ML
     1.5 +    Author:     Dmitriy Traytel, TU Muenchen
     1.6 +    Copyright   2013
     1.7 +
     1.8 +Flattening of nested to mutual (co)recursion.
     1.9 +*)
    1.10 +
    1.11 +signature BNF_FP_N2M =
    1.12 +sig
    1.13 +  val construct_mutualized_fp: BNF_FP_Util.fp_kind  -> typ list -> BNF_FP_Def_Sugar.fp_sugar list ->
    1.14 +    binding list -> (string * sort) list -> typ list * typ list list -> BNF_Def.bnf list ->
    1.15 +    local_theory -> BNF_FP_Util.fp_result * local_theory
    1.16 +end;
    1.17 +
    1.18 +structure BNF_FP_N2M : BNF_FP_N2M =
    1.19 +struct
    1.20 +
    1.21 +open BNF_Def
    1.22 +open BNF_Util
    1.23 +open BNF_FP_Util
    1.24 +open BNF_FP_Def_Sugar
    1.25 +open BNF_Tactics
    1.26 +open BNF_FP_N2M_Tactics
    1.27 +
    1.28 +fun force_typ ctxt T =
    1.29 +  map_types Type_Infer.paramify_vars
    1.30 +  #> Type.constraint T
    1.31 +  #> Syntax.check_term ctxt
    1.32 +  #> singleton (Variable.polymorphic ctxt);
    1.33 +
    1.34 +fun mk_prod_map f g =
    1.35 +  let
    1.36 +    val ((fAT, fBT), fT) = `dest_funT (fastype_of f);
    1.37 +    val ((gAT, gBT), gT) = `dest_funT (fastype_of g);
    1.38 +  in
    1.39 +    Const (@{const_name map_pair},
    1.40 +      fT --> gT --> HOLogic.mk_prodT (fAT, gAT) --> HOLogic.mk_prodT (fBT, gBT)) $ f $ g
    1.41 +  end;
    1.42 +
    1.43 +fun mk_sum_map f g =
    1.44 +  let
    1.45 +    val ((fAT, fBT), fT) = `dest_funT (fastype_of f);
    1.46 +    val ((gAT, gBT), gT) = `dest_funT (fastype_of g);
    1.47 +  in
    1.48 +    Const (@{const_name sum_map}, fT --> gT --> mk_sumT (fAT, gAT) --> mk_sumT (fBT, gBT)) $ f $ g
    1.49 +  end;
    1.50 +
    1.51 +fun construct_mutualized_fp fp fpTs fp_sugars bs resBs (resDs, Dss) bnfs lthy =
    1.52 +  let
    1.53 +    fun steal get = map (of_fp_sugar (get o #fp_res)) fp_sugars;
    1.54 +
    1.55 +    val n = length bnfs;
    1.56 +    val deads = fold (union (op =)) Dss resDs;
    1.57 +    val As = subtract (op =) deads (map TFree resBs);
    1.58 +    val names_lthy = fold Variable.declare_typ (As @ deads) lthy;
    1.59 +    val m = length As;
    1.60 +    val live = m + n;
    1.61 +    val ((Xs, Bs), names_lthy) = names_lthy
    1.62 +      |> mk_TFrees n
    1.63 +      ||>> mk_TFrees m;
    1.64 +    val allAs = As @ Xs;
    1.65 +    val phiTs = map2 mk_pred2T As Bs;
    1.66 +    val theta = As ~~ Bs;
    1.67 +    val fpTs' = map (Term.typ_subst_atomic theta) fpTs;
    1.68 +    val pre_phiTs = map2 mk_pred2T fpTs fpTs';
    1.69 +
    1.70 +    fun mk_co_algT T U = fp_case fp (T --> U) (U --> T);
    1.71 +    fun co_swap pair = fp_case fp I swap pair;
    1.72 +    val dest_co_algT = co_swap o dest_funT;
    1.73 +    val co_alg_argT = fp_case fp range_type domain_type;
    1.74 +    val co_alg_funT = fp_case fp domain_type range_type;
    1.75 +    val mk_co_product = curry (fp_case fp mk_convol mk_sum_case);
    1.76 +    val mk_map_co_product = fp_case fp mk_prod_map mk_sum_map;
    1.77 +    val co_proj1_const = fp_case fp (fst_const o fst) (uncurry Inl_const o dest_sumT o snd);
    1.78 +    val mk_co_productT = curry (fp_case fp HOLogic.mk_prodT mk_sumT);
    1.79 +    val dest_co_productT = fp_case fp HOLogic.dest_prodT dest_sumT;
    1.80 +
    1.81 +    val ((ctors, dtors), (xtor's, xtors)) =
    1.82 +      let
    1.83 +        val ctors = map2 (force_typ names_lthy o (fn T => dummyT --> T)) fpTs (steal #ctors);
    1.84 +        val dtors = map2 (force_typ names_lthy o (fn T => T --> dummyT)) fpTs (steal #dtors);
    1.85 +      in
    1.86 +        ((ctors, dtors), `(map (Term.subst_atomic_types theta)) (fp_case fp ctors dtors))
    1.87 +      end;
    1.88 +
    1.89 +    val xTs = map (domain_type o fastype_of) xtors;
    1.90 +    val yTs = map (domain_type o fastype_of) xtor's;
    1.91 +
    1.92 +    val (((((phis, phis'), pre_phis), xs), ys), names_lthy) = names_lthy
    1.93 +      |> mk_Frees' "R" phiTs
    1.94 +      ||>> mk_Frees "S" pre_phiTs
    1.95 +      ||>> mk_Frees "x" xTs
    1.96 +      ||>> mk_Frees "y" yTs;
    1.97 +
    1.98 +    val fp_bnfs = steal #bnfs;
    1.99 +    val pre_bnfs = map (of_fp_sugar #pre_bnfs) fp_sugars;
   1.100 +    val pre_bnfss = map #pre_bnfs fp_sugars;
   1.101 +    val nesty_bnfss = map (fn sugar => #nested_bnfs sugar @ #nesting_bnfs sugar) fp_sugars;
   1.102 +    val fp_nesty_bnfss = fp_bnfs :: nesty_bnfss;
   1.103 +    val fp_nesty_bnfs = distinct eq_bnf (flat fp_nesty_bnfss);
   1.104 +
   1.105 +    val rels =
   1.106 +      let
   1.107 +        fun find_rel T As Bs = fp_nesty_bnfss
   1.108 +          |> map (filter_out (curry eq_bnf BNF_Comp.DEADID_bnf))
   1.109 +          |> get_first (find_first (fn bnf => Type.could_unify (T_of_bnf bnf, T)))
   1.110 +          |> Option.map (fn bnf =>
   1.111 +            let val live = live_of_bnf bnf;
   1.112 +            in (mk_rel live As Bs (rel_of_bnf bnf), live) end)
   1.113 +          |> the_default (HOLogic.eq_const T, 0);
   1.114 +
   1.115 +        fun mk_rel (T as Type (_, Ts)) (Type (_, Us)) =
   1.116 +              let
   1.117 +                val (rel, live) = find_rel T Ts Us;
   1.118 +                val (Ts', Us') = fastype_of rel |> strip_typeN live |> fst |> map_split dest_pred2T;
   1.119 +                val rels = map2 mk_rel Ts' Us';
   1.120 +              in
   1.121 +                Term.list_comb (rel, rels)
   1.122 +              end
   1.123 +          | mk_rel (T as TFree _) _ = (nth phis (find_index (curry op = T) As)
   1.124 +              handle General.Subscript => HOLogic.eq_const T)
   1.125 +          | mk_rel _ _ = raise Fail "fpTs contains schematic type variables";
   1.126 +      in
   1.127 +        map2 (fold_rev Term.absfree phis' oo mk_rel) fpTs fpTs'
   1.128 +      end;
   1.129 +
   1.130 +    val pre_rels = map2 (fn Ds => mk_rel_of_bnf Ds (As @ fpTs) (Bs @ fpTs')) Dss bnfs;
   1.131 +
   1.132 +    val rel_unfoldss = map (maps (fn bnf => no_refl [rel_def_of_bnf bnf])) pre_bnfss;
   1.133 +    val rel_xtor_co_inducts = steal (split_conj_thm o #rel_xtor_co_induct_thm)
   1.134 +      |> map2 (fn unfs => unfold_thms lthy (id_apply :: unfs)) rel_unfoldss;
   1.135 +
   1.136 +    val rel_defs = map rel_def_of_bnf bnfs;
   1.137 +    val rel_monos = map rel_mono_of_bnf bnfs;
   1.138 +
   1.139 +    val rel_xtor_co_induct_thm =
   1.140 +      mk_rel_xtor_co_induct_thm fp pre_rels pre_phis rels phis xs ys xtors xtor's
   1.141 +        (mk_rel_xtor_co_induct_tactic fp rel_xtor_co_inducts rel_defs rel_monos) lthy;
   1.142 +
   1.143 +    val rel_eqs = no_refl (map rel_eq_of_bnf fp_nesty_bnfs);
   1.144 +    val map_id0s = no_refl (map map_id0_of_bnf bnfs);
   1.145 +
   1.146 +    val xtor_co_induct_thm =
   1.147 +      (case fp of
   1.148 +        Least_FP =>
   1.149 +          let
   1.150 +            val (Ps, names_lthy) = names_lthy
   1.151 +              |> mk_Frees "P" (map (fn T => T --> HOLogic.boolT) fpTs);
   1.152 +            fun mk_Grp_id P =
   1.153 +              let val T = domain_type (fastype_of P);
   1.154 +              in mk_Grp (HOLogic.Collect_const T $ P) (HOLogic.id_const T) end;
   1.155 +            val cts = map (SOME o certify lthy) (map HOLogic.eq_const As @ map mk_Grp_id Ps);
   1.156 +          in
   1.157 +            cterm_instantiate_pos cts rel_xtor_co_induct_thm
   1.158 +            |> singleton (Proof_Context.export names_lthy lthy)
   1.159 +            |> unfold_thms lthy (@{thms eq_le_Grp_id_iff all_simps(1,2)[symmetric]} @ rel_eqs)
   1.160 +            |> funpow n (fn thm => thm RS spec)
   1.161 +            |> unfold_thms lthy (@{thm eq_alt} :: map rel_Grp_of_bnf bnfs @ map_id0s)
   1.162 +            |> unfold_thms lthy @{thms Grp_id_mono_subst eqTrueI[OF subset_UNIV] simp_thms(22)}
   1.163 +            |> unfold_thms lthy @{thms subset_iff mem_Collect_eq
   1.164 +               atomize_conjL[symmetric] atomize_all[symmetric] atomize_imp[symmetric]}
   1.165 +            |> unfold_thms lthy (maps set_defs_of_bnf bnfs)
   1.166 +          end
   1.167 +      | Greatest_FP =>
   1.168 +          let
   1.169 +            val cts = NONE :: map (SOME o certify lthy) (map HOLogic.eq_const As);
   1.170 +          in
   1.171 +            cterm_instantiate_pos cts rel_xtor_co_induct_thm
   1.172 +            |> unfold_thms lthy (@{thms le_fun_def le_bool_def all_simps(1,2)[symmetric]} @ rel_eqs)
   1.173 +            |> funpow (2 * n) (fn thm => thm RS spec)
   1.174 +            |> Conv.fconv_rule (Object_Logic.atomize lthy)
   1.175 +            |> funpow n (fn thm => thm RS mp)
   1.176 +          end);
   1.177 +
   1.178 +    val fold_preTs = map2 (fn Ds => mk_T_of_bnf Ds allAs) Dss bnfs;
   1.179 +    val fold_pre_deads_only_Ts = map2 (fn Ds => mk_T_of_bnf Ds (replicate live dummyT)) Dss bnfs;
   1.180 +    val rec_theta = Xs ~~ map2 mk_co_productT fpTs Xs;
   1.181 +    val rec_preTs = map (Term.typ_subst_atomic rec_theta) fold_preTs;
   1.182 +
   1.183 +    val fold_strTs = map2 mk_co_algT fold_preTs Xs;
   1.184 +    val rec_strTs = map2 mk_co_algT rec_preTs Xs;
   1.185 +    val resTs = map2 mk_co_algT fpTs Xs;
   1.186 +
   1.187 +    val (((fold_strs, fold_strs'), (rec_strs, rec_strs')), names_lthy) = names_lthy
   1.188 +      |> mk_Frees' "s" fold_strTs
   1.189 +      ||>> mk_Frees' "s" rec_strTs;
   1.190 +
   1.191 +    val co_iters = steal #xtor_co_iterss;
   1.192 +    val ns = map (length o #pre_bnfs) fp_sugars;
   1.193 +    fun substT rho (Type (@{type_name "fun"}, [T, U])) = substT rho T --> substT rho U
   1.194 +      | substT rho (Type (s, Ts)) = Type (s, map (typ_subst_nonatomic rho) Ts)
   1.195 +      | substT _ T = T;
   1.196 +    fun force_iter is_rec i TU TU_rec raw_iters =
   1.197 +      let
   1.198 +        val approx_fold = un_fold_of raw_iters
   1.199 +          |> force_typ names_lthy
   1.200 +            (replicate (nth ns i) dummyT ---> (if is_rec then TU_rec else TU));
   1.201 +        val TUs = binder_fun_types (Term.typ_subst_atomic (Xs ~~ fpTs) (fastype_of approx_fold));
   1.202 +        val js = find_indices Type.could_unify
   1.203 +          TUs (map (Term.typ_subst_atomic (Xs ~~ fpTs)) fold_strTs);
   1.204 +        val Tpats = map (fn j => mk_co_algT (nth fold_pre_deads_only_Ts j) (nth Xs j)) js;
   1.205 +        val iter = raw_iters |> (if is_rec then co_rec_of else un_fold_of);
   1.206 +      in
   1.207 +        force_typ names_lthy (Tpats ---> TU) iter
   1.208 +      end;
   1.209 +
   1.210 +    fun mk_iter b_opt is_rec iters lthy TU =
   1.211 +      let
   1.212 +        val x = co_alg_argT TU;
   1.213 +        val i = find_index (fn T => x = T) Xs;
   1.214 +        val TUiter =
   1.215 +          (case find_first (fn f => body_fun_type (fastype_of f) = TU) iters of
   1.216 +            NONE => nth co_iters i
   1.217 +              |> force_iter is_rec i
   1.218 +                (TU |> (is_none b_opt andalso not is_rec) ? substT (fpTs ~~ Xs))
   1.219 +                (TU |> (is_none b_opt) ? substT (map2 mk_co_productT fpTs Xs ~~ Xs))
   1.220 +          | SOME f => f);
   1.221 +        val TUs = binder_fun_types (fastype_of TUiter);
   1.222 +        val iter_preTs = if is_rec then rec_preTs else fold_preTs;
   1.223 +        val iter_strs = if is_rec then rec_strs else fold_strs;
   1.224 +        fun mk_s TU' =
   1.225 +          let
   1.226 +            val i = find_index (fn T => co_alg_argT TU' = T) Xs;
   1.227 +            val sF = co_alg_funT TU';
   1.228 +            val F = nth iter_preTs i;
   1.229 +            val s = nth iter_strs i;
   1.230 +          in
   1.231 +            (if sF = F then s
   1.232 +            else
   1.233 +              let
   1.234 +                val smapT = replicate live dummyT ---> mk_co_algT sF F;
   1.235 +                fun hidden_to_unit t =
   1.236 +                  Term.subst_TVars (map (rpair HOLogic.unitT) (Term.add_tvar_names t [])) t;
   1.237 +                val smap = map_of_bnf (nth bnfs i)
   1.238 +                  |> force_typ names_lthy smapT
   1.239 +                  |> hidden_to_unit;
   1.240 +                val smap_argTs = strip_typeN live (fastype_of smap) |> fst;
   1.241 +                fun mk_smap_arg TU =
   1.242 +                  (if domain_type TU = range_type TU then
   1.243 +                    HOLogic.id_const (domain_type TU)
   1.244 +                  else if is_rec then
   1.245 +                    let
   1.246 +                      val (TY, (U, X)) = TU |> dest_co_algT ||> dest_co_productT;
   1.247 +                      val T = mk_co_algT TY U;
   1.248 +                    in
   1.249 +                      (case try (force_typ lthy T o build_map lthy co_proj1_const o dest_funT) T of
   1.250 +                        SOME f => mk_co_product f
   1.251 +                          (fst (fst (mk_iter NONE is_rec iters lthy (mk_co_algT TY X))))
   1.252 +                      | NONE => mk_map_co_product
   1.253 +                          (build_map lthy co_proj1_const
   1.254 +                            (dest_funT (mk_co_algT (dest_co_productT TY |> fst) U)))
   1.255 +                          (HOLogic.id_const X))
   1.256 +                    end
   1.257 +                  else
   1.258 +                    fst (fst (mk_iter NONE is_rec iters lthy TU)))
   1.259 +                val smap_args = map mk_smap_arg smap_argTs;
   1.260 +              in
   1.261 +                HOLogic.mk_comp (co_swap (s, Term.list_comb (smap, smap_args)))
   1.262 +              end)
   1.263 +          end;
   1.264 +        val t = Term.list_comb (TUiter, map mk_s TUs);
   1.265 +      in
   1.266 +        (case b_opt of
   1.267 +          NONE => ((t, Drule.dummy_thm), lthy)
   1.268 +        | SOME b => Local_Theory.define ((b, NoSyn), ((Binding.conceal (Thm.def_binding b), []),
   1.269 +            fold_rev Term.absfree (if is_rec then rec_strs' else fold_strs') t)) lthy |>> apsnd snd)
   1.270 +      end;
   1.271 +
   1.272 +    fun mk_iters is_rec name lthy =
   1.273 +      fold2 (fn TU => fn b => fn ((iters, defs), lthy) =>
   1.274 +        mk_iter (SOME b) is_rec iters lthy TU |>> (fn (f, d) => (f :: iters, d :: defs)))
   1.275 +      resTs (map (Binding.suffix_name ("_" ^ name)) bs) (([], []), lthy)
   1.276 +      |>> apfst rev o apsnd rev;
   1.277 +    val foldN = fp_case fp ctor_foldN dtor_unfoldN;
   1.278 +    val recN = fp_case fp ctor_recN dtor_corecN;
   1.279 +    val (((raw_un_folds, raw_un_fold_defs), (raw_co_recs, raw_co_rec_defs)), (lthy, raw_lthy)) =
   1.280 +      lthy
   1.281 +      |> mk_iters false foldN
   1.282 +      ||>> mk_iters true recN
   1.283 +      ||> `Local_Theory.restore;
   1.284 +
   1.285 +    val phi = Proof_Context.export_morphism raw_lthy lthy;
   1.286 +
   1.287 +    val un_folds = map (Morphism.term phi) raw_un_folds;
   1.288 +    val co_recs = map (Morphism.term phi) raw_co_recs;
   1.289 +
   1.290 +    val (xtor_un_fold_thms, xtor_co_rec_thms) =
   1.291 +      let
   1.292 +        val folds = map (fn f => Term.list_comb (f, fold_strs)) raw_un_folds;
   1.293 +        val recs = map (fn r => Term.list_comb (r, rec_strs)) raw_co_recs;
   1.294 +        val fold_mapTs = co_swap (As @ fpTs, As @ Xs);
   1.295 +        val rec_mapTs = co_swap (As @ fpTs, As @ map2 mk_co_productT fpTs Xs);
   1.296 +        val pre_fold_maps =
   1.297 +          map2 (fn Ds => fn bnf =>
   1.298 +            Term.list_comb (uncurry (mk_map_of_bnf Ds) fold_mapTs bnf,
   1.299 +              map HOLogic.id_const As @ folds))
   1.300 +          Dss bnfs;
   1.301 +        val pre_rec_maps =
   1.302 +          map2 (fn Ds => fn bnf =>
   1.303 +            Term.list_comb (uncurry (mk_map_of_bnf Ds) rec_mapTs bnf,
   1.304 +              map HOLogic.id_const As @ map2 (mk_co_product o HOLogic.id_const) fpTs recs))
   1.305 +          Dss bnfs;
   1.306 +
   1.307 +        fun mk_goals f xtor s smap =
   1.308 +          ((f, xtor), (s, smap))
   1.309 +          |> pairself (HOLogic.mk_comp o co_swap)
   1.310 +          |> HOLogic.mk_eq;
   1.311 +
   1.312 +        val fold_goals = map4 mk_goals folds xtors fold_strs pre_fold_maps
   1.313 +        val rec_goals = map4 mk_goals recs xtors rec_strs pre_rec_maps;
   1.314 +
   1.315 +        fun mk_thms ss goals tac =
   1.316 +          Library.foldr1 HOLogic.mk_conj goals
   1.317 +          |> HOLogic.mk_Trueprop
   1.318 +          |> fold_rev Logic.all ss
   1.319 +          |> (fn goal => Goal.prove_sorry raw_lthy [] [] goal tac)
   1.320 +          |> Thm.close_derivation
   1.321 +          |> Morphism.thm phi
   1.322 +          |> split_conj_thm
   1.323 +          |> map (fn thm => thm RS @{thm comp_eq_dest});
   1.324 +
   1.325 +        val pre_map_defs = no_refl (map map_def_of_bnf bnfs);
   1.326 +        val fp_pre_map_defs = no_refl (map map_def_of_bnf pre_bnfs);
   1.327 +
   1.328 +        val map_unfoldss = map (maps (fn bnf => no_refl [map_def_of_bnf bnf])) pre_bnfss;
   1.329 +        val unfold_map = map2 (fn unfs => unfold_thms lthy (id_apply :: unfs)) map_unfoldss;
   1.330 +
   1.331 +        val fp_xtor_co_iterss = steal #xtor_co_iter_thmss;
   1.332 +        val fp_xtor_un_folds = map (mk_pointfree lthy o un_fold_of) fp_xtor_co_iterss |> unfold_map;
   1.333 +        val fp_xtor_co_recs = map (mk_pointfree lthy o co_rec_of) fp_xtor_co_iterss |> unfold_map;
   1.334 +
   1.335 +        val fp_co_iter_o_mapss = steal #xtor_co_iter_o_map_thmss;
   1.336 +        val fp_fold_o_maps = map un_fold_of fp_co_iter_o_mapss |> unfold_map;
   1.337 +        val fp_rec_o_maps = map co_rec_of fp_co_iter_o_mapss |> unfold_map;
   1.338 +        val fold_thms = fp_case fp @{thm o_assoc[symmetric]} @{thm o_assoc} ::
   1.339 +          @{thms id_apply o_apply o_id id_o map_pair.comp map_pair.id sum_map.comp sum_map.id};
   1.340 +        val rec_thms = fold_thms @ fp_case fp
   1.341 +          @{thms fst_convol map_pair_o_convol convol_o}
   1.342 +          @{thms sum_case_o_inj(1) sum_case_o_sum_map o_sum_case};
   1.343 +        val map_thms = no_refl (maps (fn bnf =>
   1.344 +          [map_comp0_of_bnf bnf RS sym, map_id0_of_bnf bnf]) fp_nesty_bnfs);
   1.345 +
   1.346 +        fun mk_tac defs o_map_thms xtor_thms thms {context = ctxt, prems = _} =
   1.347 +          unfold_thms_tac ctxt
   1.348 +            (flat [thms, defs, pre_map_defs, fp_pre_map_defs, xtor_thms, o_map_thms, map_thms]) THEN
   1.349 +          CONJ_WRAP (K (HEADGOAL (rtac refl))) bnfs;
   1.350 +
   1.351 +        val fold_tac = mk_tac raw_un_fold_defs fp_fold_o_maps fp_xtor_un_folds fold_thms;
   1.352 +        val rec_tac = mk_tac raw_co_rec_defs fp_rec_o_maps fp_xtor_co_recs rec_thms;
   1.353 +      in
   1.354 +        (mk_thms fold_strs fold_goals fold_tac, mk_thms rec_strs rec_goals rec_tac)
   1.355 +      end;
   1.356 +
   1.357 +    (* These results are half broken. This is deliberate. We care only about those fields that are
   1.358 +       used by "primrec_new", "primcorecursive", and "datatype_new_compat". *)
   1.359 +    val fp_res =
   1.360 +      ({Ts = fpTs,
   1.361 +        bnfs = steal #bnfs,
   1.362 +        dtors = dtors,
   1.363 +        ctors = ctors,
   1.364 +        xtor_co_iterss = transpose [un_folds, co_recs],
   1.365 +        xtor_co_induct = xtor_co_induct_thm,
   1.366 +        dtor_ctors = steal #dtor_ctors (*too general types*),
   1.367 +        ctor_dtors = steal #ctor_dtors (*too general types*),
   1.368 +        ctor_injects = steal #ctor_injects (*too general types*),
   1.369 +        dtor_injects = steal #dtor_injects (*too general types*),
   1.370 +        xtor_map_thms = steal #xtor_map_thms (*too general types and terms*),
   1.371 +        xtor_set_thmss = steal #xtor_set_thmss (*too general types and terms*),
   1.372 +        xtor_rel_thms = steal #xtor_rel_thms (*too general types and terms*),
   1.373 +        xtor_co_iter_thmss = transpose [xtor_un_fold_thms, xtor_co_rec_thms],
   1.374 +        xtor_co_iter_o_map_thmss = steal #xtor_co_iter_o_map_thmss (*theorem about old constant*),
   1.375 +        rel_xtor_co_induct_thm = rel_xtor_co_induct_thm}
   1.376 +       |> morph_fp_result (Morphism.term_morphism "BNF" (singleton (Variable.polymorphic lthy))));
   1.377 +  in
   1.378 +    (fp_res, lthy)
   1.379 +  end;
   1.380 +
   1.381 +end;