derive (co)rec uniformly from (un)fold
authortraytel
Thu, 07 Apr 2016 17:56:22 +0200
changeset 62905 52c5a25e0c96
parent 62904 94535e6dd168
child 62906 75ca185db27f
derive (co)rec uniformly from (un)fold
src/HOL/BNF_Fixpoint_Base.thy
src/HOL/BNF_Greatest_Fixpoint.thy
src/HOL/BNF_Least_Fixpoint.thy
src/HOL/Tools/BNF/bnf_fp_n2m.ML
src/HOL/Tools/BNF/bnf_fp_util.ML
src/HOL/Tools/BNF/bnf_fp_util_tactics.ML
src/HOL/Tools/BNF/bnf_gfp.ML
src/HOL/Tools/BNF/bnf_lfp.ML
--- a/src/HOL/BNF_Fixpoint_Base.thy	Thu Apr 07 17:26:22 2016 +0200
+++ b/src/HOL/BNF_Fixpoint_Base.thy	Thu Apr 07 17:56:22 2016 +0200
@@ -242,6 +242,49 @@
 lemma top_conj: "top x \<and> P \<longleftrightarrow> P" "P \<and> top x \<longleftrightarrow> P"
   by blast+
 
+lemma fst_convol': "fst (\<langle>f, g\<rangle> x) = f x"
+  using fst_convol unfolding convol_def by simp
+
+lemma snd_convol': "snd (\<langle>f, g\<rangle> x) = g x"
+  using snd_convol unfolding convol_def by simp
+
+lemma convol_expand_snd: "fst o f = g \<Longrightarrow> \<langle>g, snd o f\<rangle> = f"
+  unfolding convol_def by auto
+
+lemma convol_expand_snd':
+  assumes "(fst o f = g)"
+  shows "h = snd o f \<longleftrightarrow> \<langle>g, h\<rangle> = f"
+proof -
+  from assms have *: "\<langle>g, snd o f\<rangle> = f" by (rule convol_expand_snd)
+  then have "h = snd o f \<longleftrightarrow> h = snd o \<langle>g, snd o f\<rangle>" by simp
+  moreover have "\<dots> \<longleftrightarrow> h = snd o f" by (simp add: snd_convol)
+  moreover have "\<dots> \<longleftrightarrow> \<langle>g, h\<rangle> = f" by (subst (2) *[symmetric]) (auto simp: convol_def fun_eq_iff)
+  ultimately show ?thesis by simp
+qed
+
+lemma case_sum_expand_Inr_pointfree: "f o Inl = g \<Longrightarrow> case_sum g (f o Inr) = f"
+  by (auto split: sum.splits)
+
+lemma case_sum_expand_Inr': "f o Inl = g \<Longrightarrow> h = f o Inr \<longleftrightarrow> case_sum g h = f"
+  by (rule iffI) (auto simp add: fun_eq_iff split: sum.splits)
+
+lemma case_sum_expand_Inr: "f o Inl = g \<Longrightarrow> f x = case_sum g (f o Inr) x"
+  by (auto split: sum.splits)
+
+lemma id_transfer: "rel_fun A A id id"
+  unfolding rel_fun_def by simp
+
+lemma fst_transfer: "rel_fun (rel_prod A B) A fst fst"
+  unfolding rel_fun_def by simp
+
+lemma snd_transfer: "rel_fun (rel_prod A B) B snd snd"
+  unfolding rel_fun_def by simp
+
+lemma convol_transfer:
+  "rel_fun (rel_fun R S) (rel_fun (rel_fun R T) (rel_fun R (rel_prod S T))) BNF_Def.convol BNF_Def.convol"
+  unfolding rel_fun_def convol_def by auto
+
+ML_file "Tools/BNF/bnf_fp_util_tactics.ML"
 ML_file "Tools/BNF/bnf_fp_util.ML"
 ML_file "Tools/BNF/bnf_fp_def_sugar_tactics.ML"
 ML_file "Tools/BNF/bnf_fp_def_sugar.ML"
--- a/src/HOL/BNF_Greatest_Fixpoint.thy	Thu Apr 07 17:26:22 2016 +0200
+++ b/src/HOL/BNF_Greatest_Fixpoint.thy	Thu Apr 07 17:56:22 2016 +0200
@@ -31,14 +31,6 @@
 lemma neq_eq_eq_contradict: "\<lbrakk>t \<noteq> u; s = t; s = u\<rbrakk> \<Longrightarrow> P"
   by fast
 
-lemma case_sum_expand_Inr: "f o Inl = g \<Longrightarrow> f x = case_sum g (f o Inr) x"
-  by (auto split: sum.splits)
-
-lemma case_sum_expand_Inr': "f o Inl = g \<Longrightarrow> h = f o Inr \<longleftrightarrow> case_sum g h = f"
-  apply rule
-   apply (rule ext, force split: sum.split)
-  by (rule ext, metis case_sum_o_inj(2))
-
 lemma converse_Times: "(A \<times> B) ^-1 = B \<times> A"
   by fast
 
--- a/src/HOL/BNF_Least_Fixpoint.thy	Thu Apr 07 17:26:22 2016 +0200
+++ b/src/HOL/BNF_Least_Fixpoint.thy	Thu Apr 07 17:56:22 2016 +0200
@@ -40,26 +40,6 @@
 lemma FieldI2: "(i, j) \<in> R \<Longrightarrow> j \<in> Field R"
   unfolding Field_def by auto
 
-lemma fst_convol': "fst (\<langle>f, g\<rangle> x) = f x"
-  using fst_convol unfolding convol_def by simp
-
-lemma snd_convol': "snd (\<langle>f, g\<rangle> x) = g x"
-  using snd_convol unfolding convol_def by simp
-
-lemma convol_expand_snd: "fst o f = g \<Longrightarrow> \<langle>g, snd o f\<rangle> = f"
-  unfolding convol_def by auto
-
-lemma convol_expand_snd':
-  assumes "(fst o f = g)"
-  shows "h = snd o f \<longleftrightarrow> \<langle>g, h\<rangle> = f"
-proof -
-  from assms have *: "\<langle>g, snd o f\<rangle> = f" by (rule convol_expand_snd)
-  then have "h = snd o f \<longleftrightarrow> h = snd o \<langle>g, snd o f\<rangle>" by simp
-  moreover have "\<dots> \<longleftrightarrow> h = snd o f" by (simp add: snd_convol)
-  moreover have "\<dots> \<longleftrightarrow> \<langle>g, h\<rangle> = f" by (subst (2) *[symmetric]) (auto simp: convol_def fun_eq_iff)
-  ultimately show ?thesis by simp
-qed
-
 lemma bij_betwE: "bij_betw f A B \<Longrightarrow> \<forall>a\<in>A. f a \<in> B"
   unfolding bij_betw_def by auto
 
@@ -172,19 +152,6 @@
 lemma predicate2D_vimage2p: "\<lbrakk>R \<le> vimage2p f g S; R x y\<rbrakk> \<Longrightarrow> S (f x) (g y)"
   unfolding vimage2p_def by auto
 
-lemma id_transfer: "rel_fun A A id id"
-  unfolding rel_fun_def by simp
-
-lemma fst_transfer: "rel_fun (rel_prod A B) A fst fst"
-  unfolding rel_fun_def by simp
-
-lemma snd_transfer: "rel_fun (rel_prod A B) B snd snd"
-  unfolding rel_fun_def by simp
-
-lemma convol_transfer:
-  "rel_fun (rel_fun R S) (rel_fun (rel_fun R T) (rel_fun R (rel_prod S T))) BNF_Def.convol BNF_Def.convol"
-  unfolding rel_fun_def convol_def by auto
-
 lemma ssubst_Pair_rhs: "\<lbrakk>(r, s) \<in> R; s' = s\<rbrakk> \<Longrightarrow> (r, s') \<in> R"
   by (rule ssubst)
 
--- a/src/HOL/Tools/BNF/bnf_fp_n2m.ML	Thu Apr 07 17:26:22 2016 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_n2m.ML	Thu Apr 07 17:56:22 2016 +0200
@@ -24,12 +24,6 @@
 open BNF_Tactics
 open BNF_FP_N2M_Tactics
 
-fun force_typ ctxt T =
-  Term.map_types Type_Infer.paramify_vars
-  #> Type.constraint T
-  #> Syntax.check_term ctxt
-  #> singleton (Variable.polymorphic ctxt);
-
 fun mk_prod_map f g =
   let
     val ((fAT, fBT), fT) = `dest_funT (fastype_of f);
--- a/src/HOL/Tools/BNF/bnf_fp_util.ML	Thu Apr 07 17:26:22 2016 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_util.ML	Thu Apr 07 17:56:22 2016 +0200
@@ -188,6 +188,8 @@
   val mk_sum_Cinfinite: thm list -> thm
   val mk_sum_card_order: thm list -> thm
 
+  val force_typ: Proof.context -> typ -> term -> term
+
   val mk_xtor_rel_co_induct_thm: BNF_Util.fp_kind -> term list -> term list -> term list ->
     term list -> term list -> term list -> term list -> term list ->
     ({prems: thm list, context: Proof.context} -> tactic) -> Proof.context -> thm
@@ -196,6 +198,10 @@
     ({prems: thm list, context: Proof.context} -> tactic) -> Proof.context -> thm list
   val mk_xtor_co_iter_o_map_thms: BNF_Util.fp_kind -> bool -> int -> thm -> thm list -> thm list ->
     thm list -> thm list -> thm list
+  val derive_xtor_co_recs: BNF_Util.fp_kind -> binding list -> (typ list -> typ list) ->
+    (typ list list * typ list) -> BNF_Def.bnf list -> term list -> term list ->
+    thm -> thm list -> thm list -> thm list -> thm list -> local_theory ->
+    (term list * (thm list * thm * thm list * thm list)) * local_theory
 
   val fixpoint_bnf: (binding -> binding) ->
       (binding list -> (string * sort) list -> typ list * typ list list -> BNF_Def.bnf list ->
@@ -213,6 +219,7 @@
 open BNF_Comp
 open BNF_Def
 open BNF_Util
+open BNF_FP_Util_Tactics
 
 type fp_result =
   {Ts: typ list,
@@ -611,6 +618,232 @@
     split_conj_thm (un_fold_unique OF map (case_fp fp I mk_sym) unique_prems)
   end;
 
+fun force_typ ctxt T =
+  Term.map_types Type_Infer.paramify_vars
+  #> Type.constraint T
+  #> Syntax.check_term ctxt
+  #> singleton (Variable.polymorphic ctxt);
+
+fun mk_xtor_un_fold_xtor_thms fp xtor_un_fold_unique_thm map_id0s =
+  (xtor_un_fold_unique_thm OF
+    map (fn thm => case_fp fp
+      (mk_trans @{thm id_o}
+        (mk_sym (thm RS @{thm trans[OF arg_cong2[of _ _ _ _ "op o", OF refl] o_id]})))
+      (mk_trans (thm RS @{thm arg_cong2[of _ _ _ _ "op o", OF _ refl]})
+        @{thm trans[OF id_o o_id[symmetric]]}))
+    map_id0s)
+  |> split_conj_thm |> map mk_sym;
+
+fun derive_xtor_co_recs fp bs mk_Ts (Dss, resDs) pre_bnfs xtors0 un_folds0
+    xtor_un_fold_unique xtor_un_folds xtor_un_fold_transfers xtor_maps xtor_rels lthy =
+  let
+    fun co_swap pair = case_fp fp I swap pair;
+    val mk_co_comp = curry (HOLogic.mk_comp o co_swap);
+    fun mk_co_algT T U = case_fp fp (T --> U) (U --> T);
+    val co_alg_funT = case_fp fp domain_type range_type;
+    val mk_co_product = curry (case_fp fp mk_convol mk_case_sum);
+    val co_proj1_const = case_fp fp fst_const (uncurry Inl_const o dest_sumT) o co_alg_funT;
+    val co_proj2_const = case_fp fp snd_const (uncurry Inr_const o dest_sumT) o co_alg_funT;
+    val mk_co_productT = curry (case_fp fp HOLogic.mk_prodT mk_sumT);
+
+    val n = length pre_bnfs;
+    val live = live_of_bnf (hd pre_bnfs);
+    val m = live - n;
+    val ks = 1 upto n;
+
+    val map_id0s = map map_id0_of_bnf pre_bnfs;
+    val map_comps = map map_comp_of_bnf pre_bnfs;
+    val map_cong0s = map map_cong0_of_bnf pre_bnfs;
+    val map_transfers = map map_transfer_of_bnf pre_bnfs;
+    val sym_map_comp0s = map (mk_sym o map_comp0_of_bnf) pre_bnfs;
+
+    val deads = fold (union (op =)) Dss resDs;
+    val ((((As, Bs), Xs), Ys), names_lthy) = lthy
+      |> fold Variable.declare_typ deads
+      |> mk_TFrees m
+      ||>> mk_TFrees m
+      ||>> mk_TFrees n
+      ||>> mk_TFrees n;
+
+    val XFTs = @{map 2} (fn Ds => mk_T_of_bnf Ds (As @ Xs)) Dss pre_bnfs;
+    val co_algXFTs = @{map 2} mk_co_algT XFTs Xs;
+    val Ts = mk_Ts As;
+    val un_foldTs = @{map 2} (fn T => fn X => co_algXFTs ---> mk_co_algT T X) Ts Xs;
+    val un_folds = @{map 2} (force_typ names_lthy) un_foldTs un_folds0;
+    val ABs = As ~~ Bs;
+    val XYs = Xs ~~ Ys;
+
+    val Us = map (typ_subst_atomic ABs) Ts;
+
+    val TFTs = @{map 2} (fn Ds => mk_T_of_bnf Ds (As @ Ts)) Dss pre_bnfs;
+
+    val xtors = @{map 3} (force_typ names_lthy oo mk_co_algT) TFTs Ts xtors0;
+
+    val ids = map HOLogic.id_const As;
+    val co_rec_Xs = @{map 2} mk_co_productT Ts Xs;
+    val co_rec_Ys = @{map 2} mk_co_productT Us Ys;
+    val co_rec_algXs = @{map 2} mk_co_algT co_rec_Xs Xs;
+    val co_proj1s = map co_proj1_const co_rec_algXs;
+    val co_rec_maps = @{map 2} (fn Ds =>
+      mk_map_of_bnf Ds (As @ case_fp fp co_rec_Xs Ts) (As @ case_fp fp Ts co_rec_Xs)) Dss pre_bnfs;
+    val co_rec_Ts = @{map 2} (fn Ds => mk_T_of_bnf Ds (As @ co_rec_Xs)) Dss pre_bnfs
+    val co_rec_argTs = @{map 2} mk_co_algT co_rec_Ts Xs;
+    val co_rec_resTs = @{map 2} mk_co_algT Ts Xs;
+
+    val (((co_rec_ss, fs), xs), names_lthy) = names_lthy
+      |> mk_Frees "s" co_rec_argTs
+      ||>> mk_Frees "f" co_rec_resTs
+      ||>> mk_Frees "x" (case_fp fp TFTs Xs);
+
+    val co_rec_strs =
+      @{map 3} (fn xtor => fn s => fn mapx =>
+        mk_co_product (mk_co_comp xtor (list_comb (mapx, ids @ co_proj1s))) s)
+      xtors co_rec_ss co_rec_maps;
+
+    val theta = Xs ~~ co_rec_Xs;
+    val co_rec_un_folds = map (subst_atomic_types theta) un_folds;
+
+    val co_rec_spec0s = map (fn un_fold => list_comb (un_fold, co_rec_strs)) co_rec_un_folds;
+
+    val co_rec_ids = @{map 2} (mk_co_comp o co_proj1_const) co_rec_algXs co_rec_spec0s;
+    val co_rec_specs = @{map 2} (mk_co_comp o co_proj2_const) co_rec_algXs co_rec_spec0s;
+
+    val co_recN = case_fp fp ctor_recN dtor_corecN;
+    fun co_rec_bind i = nth bs (i - 1) |> Binding.prefix_name (co_recN ^ "_");
+    val co_rec_def_bind = rpair [] o Binding.concealed o Thm.def_binding o co_rec_bind;
+
+    fun co_rec_spec i =
+      fold_rev (Term.absfree o Term.dest_Free) co_rec_ss (nth co_rec_specs (i - 1));
+
+    val ((co_rec_frees, (_, co_rec_def_frees)), (lthy, lthy_old)) =
+      lthy
+      |> Local_Theory.open_target |> snd
+      |> fold_map (fn i =>
+        Local_Theory.define ((co_rec_bind i, NoSyn), (co_rec_def_bind i, co_rec_spec i))) ks
+      |>> apsnd split_list o split_list
+      ||> `Local_Theory.close_target;
+
+    val phi = Proof_Context.export_morphism lthy_old lthy;
+    val co_rec_names = map (fst o dest_Const o Morphism.term phi) co_rec_frees;
+    val co_recs = @{map 2} (fn name => fn resT =>
+      Const (name, co_rec_argTs ---> resT)) co_rec_names co_rec_resTs;
+    val co_rec_defs = map (fn def =>
+      mk_unabs_def n (Morphism.thm phi def RS meta_eq_to_obj_eq)) co_rec_def_frees;
+
+    val xtor_un_fold_xtor_thms = mk_xtor_un_fold_xtor_thms fp xtor_un_fold_unique map_id0s;
+
+    val co_rec_id_thms =
+      let
+        val goal = @{map 2} (fn T => fn t => HOLogic.mk_eq (t, HOLogic.id_const T)) Ts co_rec_ids
+          |> Library.foldr1 HOLogic.mk_conj |> HOLogic.mk_Trueprop;
+        val vars = Variable.add_free_names lthy goal [];
+      in
+        Goal.prove_sorry lthy vars [] goal
+          (fn {context = ctxt, prems = _} => mk_xtor_co_rec_id_tac ctxt xtor_un_fold_xtor_thms
+            xtor_un_fold_unique xtor_un_folds map_comps)
+          |> Thm.close_derivation
+          |> split_conj_thm
+      end;
+
+    val co_rec_app_ss = map (fn co_rec => list_comb (co_rec, co_rec_ss)) co_recs;
+    val co_products = @{map 2} (fn T => mk_co_product (HOLogic.id_const T)) Ts co_rec_app_ss;
+    val co_rec_maps_rev = @{map 2} (fn Ds =>
+      mk_map_of_bnf Ds (As @ case_fp fp Ts co_rec_Xs) (As @ case_fp fp co_rec_Xs Ts)) Dss pre_bnfs;
+    fun mk_co_app f g x = case_fp fp (f $ (g $ x)) (g $ (f $ x));
+    val co_rec_expand_thms = map (fn thm => thm RS
+      case_fp fp @{thm convol_expand_snd} @{thm case_sum_expand_Inr_pointfree}) co_rec_id_thms;
+    val xtor_co_rec_thms =
+      let
+        fun mk_goal co_rec s mapx xtor x =
+          let
+            val lhs = mk_co_app co_rec xtor x;
+            val rhs = mk_co_app s (list_comb (mapx, ids @ co_products)) x;
+          in
+            mk_Trueprop_eq (lhs, rhs)
+          end;
+        val goals = @{map 5} mk_goal co_rec_app_ss co_rec_ss co_rec_maps_rev xtors xs;
+      in
+        map2 (fn goal => fn un_fold =>
+          Variable.add_free_names lthy goal []
+          |> (fn vars => Goal.prove_sorry lthy vars [] goal
+            (fn {context = ctxt, prems = _} =>
+              mk_xtor_co_rec_tac ctxt un_fold co_rec_defs co_rec_expand_thms))
+          |> Thm.close_derivation)
+        goals xtor_un_folds
+      end;
+
+    val co_product_fs = @{map 2} (fn T => mk_co_product (HOLogic.id_const T)) Ts fs;
+    val co_rec_expand'_thms = map (fn thm =>
+      thm RS case_fp fp @{thm convol_expand_snd'} @{thm case_sum_expand_Inr'}) co_rec_id_thms;
+    val xtor_co_rec_unique_thm =
+      let
+        fun mk_prem f s mapx xtor =
+          let
+            val lhs = mk_co_comp f xtor;
+            val rhs = mk_co_comp s (list_comb (mapx, ids @ co_product_fs));
+          in
+            mk_Trueprop_eq (co_swap (lhs, rhs))
+          end;
+        val prems = @{map 4} mk_prem fs co_rec_ss co_rec_maps_rev xtors;
+        val concl = @{map 2} (curry HOLogic.mk_eq) fs co_rec_app_ss
+          |> Library.foldr1 HOLogic.mk_conj |> HOLogic.mk_Trueprop;
+        val goal = Logic.list_implies (prems, concl);
+        val vars = Variable.add_free_names lthy goal [];
+      in
+        Goal.prove_sorry lthy vars [] goal
+          (fn {context = ctxt, prems = _} => mk_xtor_co_rec_unique_tac ctxt fp co_rec_defs
+            co_rec_expand'_thms xtor_un_fold_unique map_id0s sym_map_comp0s)
+        |> Thm.close_derivation
+      end;
+
+    val xtor_co_rec_o_map_thms = mk_xtor_co_iter_o_map_thms fp true m xtor_co_rec_unique_thm
+      (map (mk_pointfree lthy) xtor_maps) (map (mk_pointfree lthy) xtor_co_rec_thms)
+      sym_map_comp0s map_cong0s;
+
+    val ABphiTs = @{map 2} mk_pred2T As Bs;
+    val XYphiTs = @{map 2} mk_pred2T Xs Ys;
+
+    val ((ABphis, XYphis), names_lthy) = names_lthy
+      |> mk_Frees "R" ABphiTs
+      ||>> mk_Frees "S" XYphiTs;
+
+    val pre_rels =
+      @{map 2} (fn Ds => mk_rel_of_bnf Ds (As @ co_rec_Xs) (Bs @ co_rec_Ys)) Dss pre_bnfs;
+    val rels = @{map 3} (fn T => fn T' => Thm.prop_of #> HOLogic.dest_Trueprop
+        #> fst o dest_comb #> fst o dest_comb #> funpow n (snd o dest_comb)
+        #> case_fp fp (fst o dest_comb #> snd o dest_comb) (snd o dest_comb) #> head_of
+        #> force_typ names_lthy (ABphiTs ---> mk_pred2T T T'))
+      Ts Us xtor_un_fold_transfers;
+
+    fun tac {context = ctxt, prems = _} = mk_xtor_co_rec_transfer_tac ctxt fp n m co_rec_defs
+      xtor_un_fold_transfers map_transfers xtor_rels;
+
+    val mk_rel_co_product = case_fp fp mk_rel_prod mk_rel_sum;
+    val rec_phis =
+      map2 (fn rel => mk_rel_co_product (Term.list_comb (rel, ABphis))) rels XYphis;
+
+    val xtor_co_rec_transfer_thms =
+      mk_xtor_co_iter_transfer_thms fp pre_rels rec_phis XYphis rels ABphis
+        co_recs (map (subst_atomic_types (ABs @ XYs)) co_recs) tac lthy;
+
+    val notes =
+      [(case_fp fp ctor_recN dtor_corecN, xtor_co_rec_thms),
+       (case_fp fp ctor_rec_uniqueN dtor_corec_uniqueN, split_conj_thm xtor_co_rec_unique_thm),
+       (case_fp fp ctor_rec_o_mapN dtor_corec_o_mapN, xtor_co_rec_o_map_thms),
+       (case_fp fp ctor_rec_transferN dtor_corec_transferN, xtor_co_rec_transfer_thms)]
+      |> map (apsnd (map single))
+      |> maps (fn (thmN, thmss) =>
+        map2 (fn b => fn thms =>
+          ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])]))
+        bs thmss);
+
+     val lthy = lthy |> Config.get lthy bnf_internals ? snd o Local_Theory.notes notes;
+  in
+    ((co_recs,
+     (xtor_co_rec_thms, xtor_co_rec_unique_thm, xtor_co_rec_o_map_thms, xtor_co_rec_transfer_thms)),
+      lthy)
+  end;
+
 fun fixpoint_bnf extra_qualify construct_fp bs resBs Ds0 fp_eqs comp_cache0 lthy =
   let
     val time = time lthy;
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/BNF/bnf_fp_util_tactics.ML	Thu Apr 07 17:56:22 2016 +0200
@@ -0,0 +1,79 @@
+(*  Title:      HOL/Tools/BNF/bnf_fp_util_tactics.ML
+    Author:     Dmitriy Traytel, ETH Z├╝rich
+    Copyright   2016
+
+Common tactics for datatype and codatatype constructions.
+*)
+
+signature BNF_FP_UTIL_TACTICS =
+sig
+
+val mk_xtor_co_rec_id_tac: Proof.context -> thm list -> thm -> thm list -> thm list -> tactic
+val mk_xtor_co_rec_tac: Proof.context -> thm -> thm list -> thm list -> tactic
+val mk_xtor_co_rec_unique_tac: Proof.context -> BNF_Util.fp_kind -> thm list -> thm list -> thm ->
+  thm list -> thm list -> tactic
+val mk_xtor_co_rec_transfer_tac: Proof.context -> BNF_Util.fp_kind -> int -> int -> thm list ->
+  thm list -> thm list -> thm list -> tactic
+
+end
+
+structure BNF_FP_Util_Tactics =
+struct
+
+open BNF_Tactics
+open BNF_Util
+
+fun mk_xtor_co_rec_id_tac ctxt xtor_un_fold_xtors xtor_un_fold_unique xtor_un_folds map_comps =
+  unfold_thms_tac ctxt (map mk_sym xtor_un_fold_xtors) THEN
+  HEADGOAL (rtac ctxt xtor_un_fold_unique THEN_ALL_NEW EVERY' [rtac ctxt ext,
+    SELECT_GOAL (unfold_thms_tac ctxt
+      (o_apply :: @{thms fst_convol' id_o sum.case} @ map_comps @ xtor_un_folds)),
+    rtac ctxt refl]);
+
+fun mk_xtor_co_rec_tac ctxt un_fold co_rec_defs co_rec_expand_thms =
+  unfold_thms_tac ctxt (un_fold ::
+    @{thms o_apply sum.case snd_convol' case_sum_o_inj(2)} @ co_rec_defs @ co_rec_expand_thms) THEN
+    HEADGOAL (rtac ctxt refl);
+
+fun mk_xtor_co_rec_unique_tac ctxt fp co_rec_defs co_rec_expand's un_fold_unique map_ids map_comps =
+  unfold_thms_tac ctxt (co_rec_defs @ co_rec_expand's) THEN
+  HEADGOAL (EVERY' [rtac ctxt un_fold_unique]) THEN
+  unfold_thms_tac ctxt (map_ids @ map_comps @ case_fp fp
+    @{thms id_o o_id convol_o fst_convol o_assoc[symmetric]}
+    @{thms id_o o_id o_case_sum case_sum_o_inj(1) o_assoc}) THEN
+  ALLGOALS (etac ctxt (case_fp fp
+    @{thm arg_cong2[of _ _ _ _ BNF_Def.convol, OF refl]}
+    @{thm arg_cong2[of _ _ _ _ case_sum, OF refl]}));
+
+fun mk_xtor_co_rec_transfer_tac ctxt fp n m defs un_fold_transfers pre_T_map_transfers xtor_rels =
+  case_fp fp
+    (CONJ_WRAP (fn (def, un_fold_transfer) =>
+        REPEAT_DETERM (HEADGOAL (rtac ctxt rel_funI)) THEN
+        unfold_thms_tac ctxt [def, o_apply] THEN
+        HEADGOAL (rtac ctxt @{thm rel_funD[OF snd_transfer]} THEN'
+          etac ctxt (mk_rel_funDN_rotated (n + 1) un_fold_transfer) THEN'
+          EVERY' (map2 (fn pre_T_map_transfer => fn xtor_rel =>
+            etac ctxt (mk_rel_funDN_rotated 2 @{thm convol_transfer}) THEN'
+            rtac ctxt (mk_rel_funDN_rotated 2 @{thm comp_transfer}) THEN'
+            rtac ctxt (mk_rel_funDN (m + n) pre_T_map_transfer) THEN'
+            REPEAT_DETERM_N m o rtac ctxt @{thm id_transfer} THEN'
+            REPEAT_DETERM o rtac ctxt @{thm fst_transfer} THEN'
+            rtac ctxt rel_funI THEN'
+            etac ctxt (xtor_rel RS iffD2)) pre_T_map_transfers xtor_rels)))
+      (defs ~~ un_fold_transfers))
+    (CONJ_WRAP (fn (def, un_fold_transfer) =>
+        REPEAT_DETERM (HEADGOAL (rtac ctxt rel_funI)) THEN
+        unfold_thms_tac ctxt [def, o_apply] THEN
+        HEADGOAL (rtac ctxt (mk_rel_funDN (n + 1) un_fold_transfer) THEN'
+          EVERY' (map2 (fn pre_T_map_transfer => fn xtor_rel =>
+            etac ctxt (mk_rel_funDN_rotated 2 @{thm case_sum_transfer}) THEN'
+            rtac ctxt (mk_rel_funDN 2 @{thm comp_transfer}) THEN'
+            rtac ctxt (mk_rel_funDN (m + n) pre_T_map_transfer) THEN'
+            REPEAT_DETERM_N m o rtac ctxt @{thm id_transfer} THEN'
+            REPEAT_DETERM_N n o rtac ctxt @{thm Inl_transfer} THEN'
+            rtac ctxt rel_funI THEN'
+            etac ctxt (xtor_rel RS iffD1)) pre_T_map_transfers xtor_rels) THEN'
+          etac ctxt (mk_rel_funDN 1 @{thm Inr_transfer})))
+      (defs ~~ un_fold_transfers));
+
+end
\ No newline at end of file
--- a/src/HOL/Tools/BNF/bnf_gfp.ML	Thu Apr 07 17:26:22 2016 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp.ML	Thu Apr 07 17:56:22 2016 +0200
@@ -1602,52 +1602,6 @@
 
     val timer = time (timer "ctor definitions & thms");
 
-    val corec_Inl_sum_thms =
-      let
-        val mor = mor_comp_thm OF [mor_case_sum_thm, mor_unfold_thm];
-      in
-        map2 (fn unique => fn unfold_dtor =>
-          trans OF [mor RS unique, unfold_dtor]) unfold_unique_mor_thms unfold_dtor_thms
-      end;
-
-    fun corec_bind i = nth external_bs (i - 1) |> Binding.prefix_name (dtor_corecN ^ "_");
-    val corec_def_bind = rpair [] o Binding.concealed o Thm.def_binding o corec_bind;
-
-    fun mk_corec_strs corec_ss =
-      @{map 3} (fn dtor => fn sum_s => fn mapx =>
-        mk_case_sum
-          (HOLogic.mk_comp (Term.list_comb (mapx, passive_ids @ corec_Inls), dtor), sum_s))
-      dtors corec_ss corec_maps;
-
-    fun corec_spec i T AT =
-      fold_rev (Term.absfree o Term.dest_Free) corec_ss
-        (HOLogic.mk_comp (mk_unfold Ts (mk_corec_strs corec_ss) i, Inr_const T AT));
-
-    val ((corec_frees, (_, corec_def_frees)), (lthy, lthy_old)) =
-      lthy
-      |> Local_Theory.open_target |> snd
-      |> @{fold_map 3} (fn i => fn T => fn AT =>
-        Local_Theory.define ((corec_bind i, NoSyn), (corec_def_bind i, corec_spec i T AT)))
-          ks Ts activeAs
-      |>> apsnd split_list o split_list
-      ||> `Local_Theory.close_target;
-
-    val phi = Proof_Context.export_morphism lthy_old lthy;
-    val corecs = map (Morphism.term phi) corec_frees;
-    val corec_names = map (fst o dest_Const) corecs;
-    fun mk_corecs Ts passives actives =
-      let val Tactives = map2 (curry mk_sumT) Ts actives;
-      in
-        @{map 3} (fn name => fn T => fn active =>
-          Const (name, Library.foldr (op -->)
-            (map2 (curry op -->) actives (mk_FTs (passives @ Tactives)), active --> T)))
-        corec_names Ts actives
-      end;
-    fun mk_corec ss i = Term.list_comb (Const (nth corec_names (i - 1), Library.foldr (op -->)
-      (map fastype_of ss, domain_type (fastype_of (nth ss (i - 1))) --> nth Ts (i - 1))), ss);
-    val corec_defs = map (fn def =>
-      mk_unabs_def n (Morphism.thm phi def RS meta_eq_to_obj_eq)) corec_def_frees;
-
     val ((((((((zs, Jzs), Jzs_copy), Jzs1), Jzs2), unfold_fs), corec_ss), phis), _) =
       lthy
       |> mk_Frees "b" activeAs
@@ -1659,57 +1613,6 @@
       ||>> mk_Frees "s" corec_sTs
       ||>> mk_Frees "P" (map2 mk_pred2T Ts Ts);
 
-    val case_sums =
-      map2 (fn T => fn i => mk_case_sum (HOLogic.id_const T, mk_corec corec_ss i)) Ts ks;
-    val dtor_corec_thms =
-      let
-        fun mk_goal i corec_s corec_map dtor z =
-          let
-            val lhs = dtor $ (mk_corec corec_ss i $ z);
-            val rhs = Term.list_comb (corec_map, passive_ids @ case_sums) $ (corec_s $ z);
-          in
-            mk_Trueprop_eq (lhs, rhs)
-          end;
-        val goals = @{map 5} mk_goal ks corec_ss corec_maps_rev dtors zs;
-      in
-        @{map 3} (fn goal => fn unfold => fn map_cong0 =>
-          Variable.add_free_names lthy goal []
-          |> (fn vars => Goal.prove_sorry lthy vars [] goal
-            (fn {context = ctxt, prems = _} => mk_corec_tac ctxt m corec_defs unfold map_cong0
-              corec_Inl_sum_thms))
-          |> Thm.close_derivation)
-        goals dtor_unfold_thms map_cong0s
-      end;
-
-    val corec_unique_mor_thm =
-      let
-        val id_fs = map2 (fn T => fn f => mk_case_sum (HOLogic.id_const T, f)) Ts unfold_fs;
-        val prem = HOLogic.mk_Trueprop (mk_mor corec_UNIVs (mk_corec_strs corec_ss) UNIVs dtors id_fs);
-        fun mk_fun_eq f i = HOLogic.mk_eq (f, mk_corec corec_ss i);
-        val unique = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
-          (map2 mk_fun_eq unfold_fs ks));
-        val vars = fold (Variable.add_free_names lthy) [prem, unique] [];
-      in
-        Goal.prove_sorry lthy vars [] (Logic.mk_implies (prem, unique))
-          (fn {context = ctxt, prems = _} => mk_corec_unique_mor_tac ctxt corec_defs
-            corec_Inl_sum_thms unfold_unique_mor_thm)
-          |> Thm.close_derivation
-      end;
-
-    val map_id0s_o_id =
-      map (fn thm =>
-        mk_trans (thm RS @{thm arg_cong2[of _ _ _ _ "op o", OF _ refl]}) @{thm id_comp})
-      map_id0s;
-
-    val (dtor_corec_unique_thms, dtor_corec_unique_thm) =
-      `split_conj_thm (split_conj_prems n
-        (mor_UNIV_thm RS iffD2 RS corec_unique_mor_thm)
-        |> unfold_thms lthy (@{thms o_case_sum comp_id id_comp comp_assoc[symmetric]
-           case_sum_o_inj(1)} @ map_id0s_o_id @ sym_map_comps)
-        OF replicate n @{thm arg_cong2[of _ _ _ _ case_sum, OF refl]});
-
-    val timer = time (timer "corec definitions & thms");
-
     val (coinduct_params, dtor_coinduct_thm) =
       let
         val rels = map (Term.subst_atomic_types ((activeAs ~~ Ts) @ (activeBs ~~ Ts))) relsAsBs;
@@ -2661,9 +2564,6 @@
     val dtor_unfold_o_Jmap_thms = mk_xtor_co_iter_o_map_thms Greatest_FP false m
       dtor_unfold_unique_thm dtor_Jmap_o_thms (map (mk_pointfree lthy) dtor_unfold_thms)
       sym_map_comps map_cong0s;
-    val dtor_corec_o_Jmap_thms = mk_xtor_co_iter_o_map_thms Greatest_FP true m
-      dtor_corec_unique_thm dtor_Jmap_o_thms (map (mk_pointfree lthy) dtor_corec_thms)
-      sym_map_comps map_cong0s;
 
     val rels = map2 (fn Ds => mk_rel_of_bnf Ds allAs allBs') Dss bnfs;
     val Jrels = if m = 0 then map HOLogic.eq_const Ts
@@ -2676,20 +2576,19 @@
           (map map_transfer_of_bnf bnfs) dtor_unfold_thms)
         lthy;
 
-    val corec_allAs = passiveAs @ map2 (curry mk_sumT) Ts activeAs;
-    val corec_allBs = passiveBs @ map2 (curry mk_sumT) Ts' activeBs;
-    val corec_rels = map2 (fn Ds => mk_rel_of_bnf Ds corec_allAs corec_allBs) Dss bnfs;
-    val corec_activephis =
-      map2 (fn Jrel => mk_rel_sum (Term.list_comb (Jrel, Jphis))) Jrels activephis;
-    val dtor_corec_transfer_thms =
-      mk_xtor_co_iter_transfer_thms Greatest_FP corec_rels corec_activephis activephis Jrels Jphis
-        (mk_corecs Ts passiveAs activeAs) (mk_corecs Ts' passiveBs activeBs)
-        (fn {context = ctxt, prems = _} => mk_dtor_corec_transfer_tac ctxt n m corec_defs
-           dtor_unfold_transfer_thms (map map_transfer_of_bnf bnfs) dtor_Jrel_thms)
-        lthy;
-
     val timer = time (timer "relator coinduction");
 
+    fun mk_Ts As = map (typ_subst_atomic (passiveAs ~~ As)) Ts;
+    val export = map (Morphism.term (Local_Theory.target_morphism lthy))
+    val ((corecs, (dtor_corec_thms, dtor_corec_unique_thm, dtor_corec_o_Jmap_thms,
+        dtor_corec_transfer_thms)), lthy) = lthy
+      |> derive_xtor_co_recs Greatest_FP external_bs mk_Ts (Dss, resDs) bnfs
+        (export dtors) (export unfolds)
+        dtor_unfold_unique_thm dtor_unfold_thms dtor_unfold_transfer_thms
+        dtor_Jmap_thms dtor_Jrel_thms;
+
+    val timer = time (timer "recursor");
+
     val common_notes =
       [(dtor_coinductN, [dtor_coinduct_thm]),
       (dtor_rel_coinductN, [Jrel_coinduct_thm])]
@@ -2700,10 +2599,6 @@
       [(ctor_dtorN, ctor_dtor_thms),
       (ctor_exhaustN, ctor_exhaust_thms),
       (ctor_injectN, ctor_inject_thms),
-      (dtor_corecN, dtor_corec_thms),
-      (dtor_corec_o_mapN, dtor_corec_o_Jmap_thms),
-      (dtor_corec_transferN, dtor_corec_transfer_thms),
-      (dtor_corec_uniqueN, dtor_corec_unique_thms),
       (dtor_ctorN, dtor_ctor_thms),
       (dtor_exhaustN, dtor_exhaust_thms),
       (dtor_injectN, dtor_inject_thms),
@@ -2721,7 +2616,7 @@
 
     val fp_res =
       {Ts = Ts, bnfs = Jbnfs, pre_bnfs = bnfs, absT_infos = absT_infos,
-       ctors = ctors, dtors = dtors, xtor_un_folds_legacy = unfolds, xtor_co_recs = corecs,
+       ctors = ctors, dtors = dtors, xtor_un_folds_legacy = unfolds, xtor_co_recs = export corecs,
        xtor_co_induct = dtor_coinduct_thm, dtor_ctors = dtor_ctor_thms, ctor_dtors = ctor_dtor_thms,
        ctor_injects = ctor_inject_thms, dtor_injects = dtor_inject_thms, xtor_maps = dtor_Jmap_thms,
        xtor_map_unique = dtor_Jmap_unique_thm, xtor_setss = dtor_Jset_thmss',
--- a/src/HOL/Tools/BNF/bnf_lfp.ML	Thu Apr 07 17:26:22 2016 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp.ML	Thu Apr 07 17:56:22 2016 +0200
@@ -1202,50 +1202,6 @@
 
     val timer = time (timer "dtor definitions & thms");
 
-    val fst_rec_pair_thms =
-      let
-        val mor = mor_comp_thm OF [mor_fold_thm, mor_convol_thm];
-      in
-        map2 (fn unique => fn fold_ctor =>
-          trans OF [mor RS unique, fold_ctor]) fold_unique_mor_thms fold_ctor_thms
-      end;
-
-    fun rec_bind i = nth external_bs (i - 1) |> Binding.prefix_name (ctor_recN ^ "_");
-    val rec_def_bind = rpair [] o Binding.concealed o Thm.def_binding o rec_bind;
-
-    fun mk_rec_strs rec_ss =
-      @{map 3} (fn ctor => fn prod_s => fn mapx =>
-        mk_convol (HOLogic.mk_comp (ctor, Term.list_comb (mapx, passive_ids @ rec_fsts)), prod_s))
-      ctors rec_ss rec_maps;
-
-    fun rec_spec i T AT =
-      fold_rev (Term.absfree o Term.dest_Free) rec_ss
-        (HOLogic.mk_comp (snd_const (HOLogic.mk_prodT (T, AT)), mk_fold Ts (mk_rec_strs rec_ss) i));
-
-    val ((rec_frees, (_, rec_def_frees)), (lthy, lthy_old)) =
-      lthy
-      |> Local_Theory.open_target |> snd
-      |> @{fold_map 3} (fn i => fn T => fn AT =>
-        Local_Theory.define ((rec_bind i, NoSyn), (rec_def_bind i, rec_spec i T AT))) ks Ts activeAs
-      |>> apsnd split_list o split_list
-      ||> `Local_Theory.close_target;
-
-    val phi = Proof_Context.export_morphism lthy_old lthy;
-    val recs = map (Morphism.term phi) rec_frees;
-    val rec_names = map (fst o dest_Const) recs;
-    fun mk_recs Ts passives actives =
-      let val Tactives = map2 (curry HOLogic.mk_prodT) Ts actives;
-      in
-        @{map 3} (fn name => fn T => fn active =>
-          Const (name, Library.foldr (op -->)
-            (map2 (curry op -->) (mk_FTs (passives @ Tactives)) actives, T --> active)))
-        rec_names Ts actives
-      end;
-    fun mk_rec ss i = Term.list_comb (Const (nth rec_names (i - 1), Library.foldr (op -->)
-      (map fastype_of ss, nth Ts (i - 1) --> range_type (fastype_of (nth ss (i - 1))))), ss);
-    val rec_defs = map (fn def =>
-      mk_unabs_def n (Morphism.thm phi def RS meta_eq_to_obj_eq)) rec_def_frees;
-
     val (((((((((Izs, (Izs1, Izs1'))), (Izs2, Izs2')), xFs), yFs), fs), rec_ss), init_phis), _) =
       lthy
       |> mk_Frees "z" Ts
@@ -1260,48 +1216,6 @@
     val phis = map2 retype_const_or_free (map mk_pred1T Ts) init_phis;
     val phi2s = map2 retype_const_or_free (map2 mk_pred2T Ts Ts') init_phis;
 
-    val convols = map2 (fn T => fn i => mk_convol (HOLogic.id_const T, mk_rec rec_ss i)) Ts ks;
-    val ctor_rec_thms =
-      let
-        fun mk_goal i rec_s rec_map ctor x =
-          let
-            val lhs = mk_rec rec_ss i $ (ctor $ x);
-            val rhs = rec_s $ (Term.list_comb (rec_map, passive_ids @ convols) $ x);
-          in
-            mk_Trueprop_eq (lhs, rhs)
-          end;
-        val goals = @{map 5} mk_goal ks rec_ss rec_maps_rev ctors xFs;
-      in
-        map2 (fn goal => fn foldx =>
-          Variable.add_free_names lthy goal []
-          |> (fn vars => Goal.prove_sorry lthy vars [] goal
-            (fn {context = ctxt, prems = _} => mk_rec_tac ctxt rec_defs foldx fst_rec_pair_thms))
-          |> Thm.close_derivation)
-        goals ctor_fold_thms
-      end;
-
-    val rec_unique_mor_thm =
-      let
-        val id_fs = map2 (fn T => fn f => mk_convol (HOLogic.id_const T, f)) Ts fs;
-        val prem = HOLogic.mk_Trueprop (mk_mor UNIVs ctors rec_UNIVs (mk_rec_strs rec_ss) id_fs);
-        fun mk_fun_eq f i = HOLogic.mk_eq (f, mk_rec rec_ss i);
-        val unique = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj (map2 mk_fun_eq fs ks));
-        val vars = fold (Variable.add_free_names lthy) [prem, unique] [];
-      in
-        Goal.prove_sorry lthy vars [] (Logic.mk_implies (prem, unique))
-          (fn {context = ctxt, prems = _} => mk_rec_unique_mor_tac ctxt rec_defs fst_rec_pair_thms
-            fold_unique_mor_thm)
-          |> Thm.close_derivation
-      end;
-
-    val (ctor_rec_unique_thms, ctor_rec_unique_thm) =
-      `split_conj_thm (split_conj_prems n
-        (mor_UNIV_thm RS iffD2 RS rec_unique_mor_thm)
-        |> unfold_thms lthy (@{thms convol_o comp_id id_comp comp_assoc fst_convol} @
-           map_id0s @ sym_map_comps) OF replicate n @{thm arg_cong2[of _ _ _ _ convol, OF refl]});
-
-    val timer = time (timer "rec definitions & thms");
-
     val (ctor_induct_thm, induct_params) =
       let
         fun mk_prem phi ctor sets x =
@@ -1909,8 +1823,6 @@
 
     val ctor_fold_o_Imap_thms = mk_xtor_co_iter_o_map_thms Least_FP false m ctor_fold_unique_thm
       ctor_Imap_o_thms (map (mk_pointfree lthy) ctor_fold_thms) sym_map_comps map_cong0s;
-    val ctor_rec_o_Imap_thms = mk_xtor_co_iter_o_map_thms Least_FP true m ctor_rec_unique_thm
-      ctor_Imap_o_thms (map (mk_pointfree lthy) ctor_rec_thms) sym_map_comps map_cong0s;
 
     val Irels = if m = 0 then map HOLogic.eq_const Ts
       else map (mk_rel_of_bnf deads passiveAs passiveBs) Ibnfs;
@@ -1927,19 +1839,17 @@
           (map map_transfer_of_bnf bnfs) ctor_fold_thms)
         lthy;
 
-    val rec_allAs = passiveAs @ map2 (curry HOLogic.mk_prodT) Ts activeAs;
-    val rec_allBs = passiveBs @ map2 (curry HOLogic.mk_prodT) Ts' activeBs;
-    val rec_rels = map2 (fn Ds => mk_rel_of_bnf Ds rec_allAs rec_allBs) Dss bnfs;
-    val rec_activephis =
-      map2 (fn Irel => mk_rel_prod (Term.list_comb (Irel, Iphis))) Irels activephis;
-    val ctor_rec_transfer_thms =
-      mk_xtor_co_iter_transfer_thms Least_FP rec_rels rec_activephis activephis Irels Iphis
-        (mk_recs Ts passiveAs activeAs) (mk_recs Ts' passiveBs activeBs)
-        (fn {context = ctxt, prems = _} => mk_ctor_rec_transfer_tac ctxt n m rec_defs
-           ctor_fold_transfer_thms (map map_transfer_of_bnf bnfs) ctor_Irel_thms)
-        lthy;
+    val timer = time (timer "relator induction");
 
-    val timer = time (timer "relator induction");
+    fun mk_Ts As = map (typ_subst_atomic (passiveAs ~~ As)) Ts;
+    val export = map (Morphism.term (Local_Theory.target_morphism lthy))
+    val ((recs, (ctor_rec_thms, ctor_rec_unique_thm, ctor_rec_o_Imap_thms, ctor_rec_transfer_thms)),
+        lthy) = lthy
+      |> derive_xtor_co_recs Least_FP external_bs mk_Ts (Dss, resDs) bnfs
+        (export ctors) (export folds)
+        ctor_fold_unique_thm ctor_fold_thms ctor_fold_transfer_thms ctor_Imap_thms ctor_Irel_thms;
+
+    val timer = time (timer "recursor");
 
     val common_notes =
       [(ctor_inductN, [ctor_induct_thm]),
@@ -1955,11 +1865,7 @@
       (ctor_fold_o_mapN, ctor_fold_o_Imap_thms),
       (ctor_fold_transferN, ctor_fold_transfer_thms),
       (ctor_fold_uniqueN, ctor_fold_unique_thms),
-      (ctor_rec_o_mapN, ctor_rec_o_Imap_thms),
-      (ctor_rec_transferN, ctor_rec_transfer_thms),
-      (ctor_rec_uniqueN, ctor_rec_unique_thms),
       (ctor_injectN, ctor_inject_thms),
-      (ctor_recN, ctor_rec_thms),
       (dtor_ctorN, dtor_ctor_thms),
       (dtor_exhaustN, dtor_exhaust_thms),
       (dtor_injectN, dtor_inject_thms)]
@@ -1973,7 +1879,7 @@
 
     val fp_res =
       {Ts = Ts, bnfs = Ibnfs, pre_bnfs = bnfs, absT_infos = absT_infos,
-       ctors = ctors, dtors = dtors, xtor_un_folds_legacy = folds, xtor_co_recs = recs,
+       ctors = ctors, dtors = dtors, xtor_un_folds_legacy = folds, xtor_co_recs = export recs,
        xtor_co_induct = ctor_induct_thm, dtor_ctors = dtor_ctor_thms,
        ctor_dtors = ctor_dtor_thms, ctor_injects = ctor_inject_thms,
        dtor_injects = dtor_inject_thms, xtor_maps = ctor_Imap_thms,