derive (co)rec uniformly from (un)fold
authortraytel
Thu Apr 07 17:56:22 2016 +0200 (2016-04-07)
changeset 6290552c5a25e0c96
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
     1.1 --- a/src/HOL/BNF_Fixpoint_Base.thy	Thu Apr 07 17:26:22 2016 +0200
     1.2 +++ b/src/HOL/BNF_Fixpoint_Base.thy	Thu Apr 07 17:56:22 2016 +0200
     1.3 @@ -242,6 +242,49 @@
     1.4  lemma top_conj: "top x \<and> P \<longleftrightarrow> P" "P \<and> top x \<longleftrightarrow> P"
     1.5    by blast+
     1.6  
     1.7 +lemma fst_convol': "fst (\<langle>f, g\<rangle> x) = f x"
     1.8 +  using fst_convol unfolding convol_def by simp
     1.9 +
    1.10 +lemma snd_convol': "snd (\<langle>f, g\<rangle> x) = g x"
    1.11 +  using snd_convol unfolding convol_def by simp
    1.12 +
    1.13 +lemma convol_expand_snd: "fst o f = g \<Longrightarrow> \<langle>g, snd o f\<rangle> = f"
    1.14 +  unfolding convol_def by auto
    1.15 +
    1.16 +lemma convol_expand_snd':
    1.17 +  assumes "(fst o f = g)"
    1.18 +  shows "h = snd o f \<longleftrightarrow> \<langle>g, h\<rangle> = f"
    1.19 +proof -
    1.20 +  from assms have *: "\<langle>g, snd o f\<rangle> = f" by (rule convol_expand_snd)
    1.21 +  then have "h = snd o f \<longleftrightarrow> h = snd o \<langle>g, snd o f\<rangle>" by simp
    1.22 +  moreover have "\<dots> \<longleftrightarrow> h = snd o f" by (simp add: snd_convol)
    1.23 +  moreover have "\<dots> \<longleftrightarrow> \<langle>g, h\<rangle> = f" by (subst (2) *[symmetric]) (auto simp: convol_def fun_eq_iff)
    1.24 +  ultimately show ?thesis by simp
    1.25 +qed
    1.26 +
    1.27 +lemma case_sum_expand_Inr_pointfree: "f o Inl = g \<Longrightarrow> case_sum g (f o Inr) = f"
    1.28 +  by (auto split: sum.splits)
    1.29 +
    1.30 +lemma case_sum_expand_Inr': "f o Inl = g \<Longrightarrow> h = f o Inr \<longleftrightarrow> case_sum g h = f"
    1.31 +  by (rule iffI) (auto simp add: fun_eq_iff split: sum.splits)
    1.32 +
    1.33 +lemma case_sum_expand_Inr: "f o Inl = g \<Longrightarrow> f x = case_sum g (f o Inr) x"
    1.34 +  by (auto split: sum.splits)
    1.35 +
    1.36 +lemma id_transfer: "rel_fun A A id id"
    1.37 +  unfolding rel_fun_def by simp
    1.38 +
    1.39 +lemma fst_transfer: "rel_fun (rel_prod A B) A fst fst"
    1.40 +  unfolding rel_fun_def by simp
    1.41 +
    1.42 +lemma snd_transfer: "rel_fun (rel_prod A B) B snd snd"
    1.43 +  unfolding rel_fun_def by simp
    1.44 +
    1.45 +lemma convol_transfer:
    1.46 +  "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"
    1.47 +  unfolding rel_fun_def convol_def by auto
    1.48 +
    1.49 +ML_file "Tools/BNF/bnf_fp_util_tactics.ML"
    1.50  ML_file "Tools/BNF/bnf_fp_util.ML"
    1.51  ML_file "Tools/BNF/bnf_fp_def_sugar_tactics.ML"
    1.52  ML_file "Tools/BNF/bnf_fp_def_sugar.ML"
     2.1 --- a/src/HOL/BNF_Greatest_Fixpoint.thy	Thu Apr 07 17:26:22 2016 +0200
     2.2 +++ b/src/HOL/BNF_Greatest_Fixpoint.thy	Thu Apr 07 17:56:22 2016 +0200
     2.3 @@ -31,14 +31,6 @@
     2.4  lemma neq_eq_eq_contradict: "\<lbrakk>t \<noteq> u; s = t; s = u\<rbrakk> \<Longrightarrow> P"
     2.5    by fast
     2.6  
     2.7 -lemma case_sum_expand_Inr: "f o Inl = g \<Longrightarrow> f x = case_sum g (f o Inr) x"
     2.8 -  by (auto split: sum.splits)
     2.9 -
    2.10 -lemma case_sum_expand_Inr': "f o Inl = g \<Longrightarrow> h = f o Inr \<longleftrightarrow> case_sum g h = f"
    2.11 -  apply rule
    2.12 -   apply (rule ext, force split: sum.split)
    2.13 -  by (rule ext, metis case_sum_o_inj(2))
    2.14 -
    2.15  lemma converse_Times: "(A \<times> B) ^-1 = B \<times> A"
    2.16    by fast
    2.17  
     3.1 --- a/src/HOL/BNF_Least_Fixpoint.thy	Thu Apr 07 17:26:22 2016 +0200
     3.2 +++ b/src/HOL/BNF_Least_Fixpoint.thy	Thu Apr 07 17:56:22 2016 +0200
     3.3 @@ -40,26 +40,6 @@
     3.4  lemma FieldI2: "(i, j) \<in> R \<Longrightarrow> j \<in> Field R"
     3.5    unfolding Field_def by auto
     3.6  
     3.7 -lemma fst_convol': "fst (\<langle>f, g\<rangle> x) = f x"
     3.8 -  using fst_convol unfolding convol_def by simp
     3.9 -
    3.10 -lemma snd_convol': "snd (\<langle>f, g\<rangle> x) = g x"
    3.11 -  using snd_convol unfolding convol_def by simp
    3.12 -
    3.13 -lemma convol_expand_snd: "fst o f = g \<Longrightarrow> \<langle>g, snd o f\<rangle> = f"
    3.14 -  unfolding convol_def by auto
    3.15 -
    3.16 -lemma convol_expand_snd':
    3.17 -  assumes "(fst o f = g)"
    3.18 -  shows "h = snd o f \<longleftrightarrow> \<langle>g, h\<rangle> = f"
    3.19 -proof -
    3.20 -  from assms have *: "\<langle>g, snd o f\<rangle> = f" by (rule convol_expand_snd)
    3.21 -  then have "h = snd o f \<longleftrightarrow> h = snd o \<langle>g, snd o f\<rangle>" by simp
    3.22 -  moreover have "\<dots> \<longleftrightarrow> h = snd o f" by (simp add: snd_convol)
    3.23 -  moreover have "\<dots> \<longleftrightarrow> \<langle>g, h\<rangle> = f" by (subst (2) *[symmetric]) (auto simp: convol_def fun_eq_iff)
    3.24 -  ultimately show ?thesis by simp
    3.25 -qed
    3.26 -
    3.27  lemma bij_betwE: "bij_betw f A B \<Longrightarrow> \<forall>a\<in>A. f a \<in> B"
    3.28    unfolding bij_betw_def by auto
    3.29  
    3.30 @@ -172,19 +152,6 @@
    3.31  lemma predicate2D_vimage2p: "\<lbrakk>R \<le> vimage2p f g S; R x y\<rbrakk> \<Longrightarrow> S (f x) (g y)"
    3.32    unfolding vimage2p_def by auto
    3.33  
    3.34 -lemma id_transfer: "rel_fun A A id id"
    3.35 -  unfolding rel_fun_def by simp
    3.36 -
    3.37 -lemma fst_transfer: "rel_fun (rel_prod A B) A fst fst"
    3.38 -  unfolding rel_fun_def by simp
    3.39 -
    3.40 -lemma snd_transfer: "rel_fun (rel_prod A B) B snd snd"
    3.41 -  unfolding rel_fun_def by simp
    3.42 -
    3.43 -lemma convol_transfer:
    3.44 -  "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"
    3.45 -  unfolding rel_fun_def convol_def by auto
    3.46 -
    3.47  lemma ssubst_Pair_rhs: "\<lbrakk>(r, s) \<in> R; s' = s\<rbrakk> \<Longrightarrow> (r, s') \<in> R"
    3.48    by (rule ssubst)
    3.49  
     4.1 --- a/src/HOL/Tools/BNF/bnf_fp_n2m.ML	Thu Apr 07 17:26:22 2016 +0200
     4.2 +++ b/src/HOL/Tools/BNF/bnf_fp_n2m.ML	Thu Apr 07 17:56:22 2016 +0200
     4.3 @@ -24,12 +24,6 @@
     4.4  open BNF_Tactics
     4.5  open BNF_FP_N2M_Tactics
     4.6  
     4.7 -fun force_typ ctxt T =
     4.8 -  Term.map_types Type_Infer.paramify_vars
     4.9 -  #> Type.constraint T
    4.10 -  #> Syntax.check_term ctxt
    4.11 -  #> singleton (Variable.polymorphic ctxt);
    4.12 -
    4.13  fun mk_prod_map f g =
    4.14    let
    4.15      val ((fAT, fBT), fT) = `dest_funT (fastype_of f);
     5.1 --- a/src/HOL/Tools/BNF/bnf_fp_util.ML	Thu Apr 07 17:26:22 2016 +0200
     5.2 +++ b/src/HOL/Tools/BNF/bnf_fp_util.ML	Thu Apr 07 17:56:22 2016 +0200
     5.3 @@ -188,6 +188,8 @@
     5.4    val mk_sum_Cinfinite: thm list -> thm
     5.5    val mk_sum_card_order: thm list -> thm
     5.6  
     5.7 +  val force_typ: Proof.context -> typ -> term -> term
     5.8 +
     5.9    val mk_xtor_rel_co_induct_thm: BNF_Util.fp_kind -> term list -> term list -> term list ->
    5.10      term list -> term list -> term list -> term list -> term list ->
    5.11      ({prems: thm list, context: Proof.context} -> tactic) -> Proof.context -> thm
    5.12 @@ -196,6 +198,10 @@
    5.13      ({prems: thm list, context: Proof.context} -> tactic) -> Proof.context -> thm list
    5.14    val mk_xtor_co_iter_o_map_thms: BNF_Util.fp_kind -> bool -> int -> thm -> thm list -> thm list ->
    5.15      thm list -> thm list -> thm list
    5.16 +  val derive_xtor_co_recs: BNF_Util.fp_kind -> binding list -> (typ list -> typ list) ->
    5.17 +    (typ list list * typ list) -> BNF_Def.bnf list -> term list -> term list ->
    5.18 +    thm -> thm list -> thm list -> thm list -> thm list -> local_theory ->
    5.19 +    (term list * (thm list * thm * thm list * thm list)) * local_theory
    5.20  
    5.21    val fixpoint_bnf: (binding -> binding) ->
    5.22        (binding list -> (string * sort) list -> typ list * typ list list -> BNF_Def.bnf list ->
    5.23 @@ -213,6 +219,7 @@
    5.24  open BNF_Comp
    5.25  open BNF_Def
    5.26  open BNF_Util
    5.27 +open BNF_FP_Util_Tactics
    5.28  
    5.29  type fp_result =
    5.30    {Ts: typ list,
    5.31 @@ -611,6 +618,232 @@
    5.32      split_conj_thm (un_fold_unique OF map (case_fp fp I mk_sym) unique_prems)
    5.33    end;
    5.34  
    5.35 +fun force_typ ctxt T =
    5.36 +  Term.map_types Type_Infer.paramify_vars
    5.37 +  #> Type.constraint T
    5.38 +  #> Syntax.check_term ctxt
    5.39 +  #> singleton (Variable.polymorphic ctxt);
    5.40 +
    5.41 +fun mk_xtor_un_fold_xtor_thms fp xtor_un_fold_unique_thm map_id0s =
    5.42 +  (xtor_un_fold_unique_thm OF
    5.43 +    map (fn thm => case_fp fp
    5.44 +      (mk_trans @{thm id_o}
    5.45 +        (mk_sym (thm RS @{thm trans[OF arg_cong2[of _ _ _ _ "op o", OF refl] o_id]})))
    5.46 +      (mk_trans (thm RS @{thm arg_cong2[of _ _ _ _ "op o", OF _ refl]})
    5.47 +        @{thm trans[OF id_o o_id[symmetric]]}))
    5.48 +    map_id0s)
    5.49 +  |> split_conj_thm |> map mk_sym;
    5.50 +
    5.51 +fun derive_xtor_co_recs fp bs mk_Ts (Dss, resDs) pre_bnfs xtors0 un_folds0
    5.52 +    xtor_un_fold_unique xtor_un_folds xtor_un_fold_transfers xtor_maps xtor_rels lthy =
    5.53 +  let
    5.54 +    fun co_swap pair = case_fp fp I swap pair;
    5.55 +    val mk_co_comp = curry (HOLogic.mk_comp o co_swap);
    5.56 +    fun mk_co_algT T U = case_fp fp (T --> U) (U --> T);
    5.57 +    val co_alg_funT = case_fp fp domain_type range_type;
    5.58 +    val mk_co_product = curry (case_fp fp mk_convol mk_case_sum);
    5.59 +    val co_proj1_const = case_fp fp fst_const (uncurry Inl_const o dest_sumT) o co_alg_funT;
    5.60 +    val co_proj2_const = case_fp fp snd_const (uncurry Inr_const o dest_sumT) o co_alg_funT;
    5.61 +    val mk_co_productT = curry (case_fp fp HOLogic.mk_prodT mk_sumT);
    5.62 +
    5.63 +    val n = length pre_bnfs;
    5.64 +    val live = live_of_bnf (hd pre_bnfs);
    5.65 +    val m = live - n;
    5.66 +    val ks = 1 upto n;
    5.67 +
    5.68 +    val map_id0s = map map_id0_of_bnf pre_bnfs;
    5.69 +    val map_comps = map map_comp_of_bnf pre_bnfs;
    5.70 +    val map_cong0s = map map_cong0_of_bnf pre_bnfs;
    5.71 +    val map_transfers = map map_transfer_of_bnf pre_bnfs;
    5.72 +    val sym_map_comp0s = map (mk_sym o map_comp0_of_bnf) pre_bnfs;
    5.73 +
    5.74 +    val deads = fold (union (op =)) Dss resDs;
    5.75 +    val ((((As, Bs), Xs), Ys), names_lthy) = lthy
    5.76 +      |> fold Variable.declare_typ deads
    5.77 +      |> mk_TFrees m
    5.78 +      ||>> mk_TFrees m
    5.79 +      ||>> mk_TFrees n
    5.80 +      ||>> mk_TFrees n;
    5.81 +
    5.82 +    val XFTs = @{map 2} (fn Ds => mk_T_of_bnf Ds (As @ Xs)) Dss pre_bnfs;
    5.83 +    val co_algXFTs = @{map 2} mk_co_algT XFTs Xs;
    5.84 +    val Ts = mk_Ts As;
    5.85 +    val un_foldTs = @{map 2} (fn T => fn X => co_algXFTs ---> mk_co_algT T X) Ts Xs;
    5.86 +    val un_folds = @{map 2} (force_typ names_lthy) un_foldTs un_folds0;
    5.87 +    val ABs = As ~~ Bs;
    5.88 +    val XYs = Xs ~~ Ys;
    5.89 +
    5.90 +    val Us = map (typ_subst_atomic ABs) Ts;
    5.91 +
    5.92 +    val TFTs = @{map 2} (fn Ds => mk_T_of_bnf Ds (As @ Ts)) Dss pre_bnfs;
    5.93 +
    5.94 +    val xtors = @{map 3} (force_typ names_lthy oo mk_co_algT) TFTs Ts xtors0;
    5.95 +
    5.96 +    val ids = map HOLogic.id_const As;
    5.97 +    val co_rec_Xs = @{map 2} mk_co_productT Ts Xs;
    5.98 +    val co_rec_Ys = @{map 2} mk_co_productT Us Ys;
    5.99 +    val co_rec_algXs = @{map 2} mk_co_algT co_rec_Xs Xs;
   5.100 +    val co_proj1s = map co_proj1_const co_rec_algXs;
   5.101 +    val co_rec_maps = @{map 2} (fn Ds =>
   5.102 +      mk_map_of_bnf Ds (As @ case_fp fp co_rec_Xs Ts) (As @ case_fp fp Ts co_rec_Xs)) Dss pre_bnfs;
   5.103 +    val co_rec_Ts = @{map 2} (fn Ds => mk_T_of_bnf Ds (As @ co_rec_Xs)) Dss pre_bnfs
   5.104 +    val co_rec_argTs = @{map 2} mk_co_algT co_rec_Ts Xs;
   5.105 +    val co_rec_resTs = @{map 2} mk_co_algT Ts Xs;
   5.106 +
   5.107 +    val (((co_rec_ss, fs), xs), names_lthy) = names_lthy
   5.108 +      |> mk_Frees "s" co_rec_argTs
   5.109 +      ||>> mk_Frees "f" co_rec_resTs
   5.110 +      ||>> mk_Frees "x" (case_fp fp TFTs Xs);
   5.111 +
   5.112 +    val co_rec_strs =
   5.113 +      @{map 3} (fn xtor => fn s => fn mapx =>
   5.114 +        mk_co_product (mk_co_comp xtor (list_comb (mapx, ids @ co_proj1s))) s)
   5.115 +      xtors co_rec_ss co_rec_maps;
   5.116 +
   5.117 +    val theta = Xs ~~ co_rec_Xs;
   5.118 +    val co_rec_un_folds = map (subst_atomic_types theta) un_folds;
   5.119 +
   5.120 +    val co_rec_spec0s = map (fn un_fold => list_comb (un_fold, co_rec_strs)) co_rec_un_folds;
   5.121 +
   5.122 +    val co_rec_ids = @{map 2} (mk_co_comp o co_proj1_const) co_rec_algXs co_rec_spec0s;
   5.123 +    val co_rec_specs = @{map 2} (mk_co_comp o co_proj2_const) co_rec_algXs co_rec_spec0s;
   5.124 +
   5.125 +    val co_recN = case_fp fp ctor_recN dtor_corecN;
   5.126 +    fun co_rec_bind i = nth bs (i - 1) |> Binding.prefix_name (co_recN ^ "_");
   5.127 +    val co_rec_def_bind = rpair [] o Binding.concealed o Thm.def_binding o co_rec_bind;
   5.128 +
   5.129 +    fun co_rec_spec i =
   5.130 +      fold_rev (Term.absfree o Term.dest_Free) co_rec_ss (nth co_rec_specs (i - 1));
   5.131 +
   5.132 +    val ((co_rec_frees, (_, co_rec_def_frees)), (lthy, lthy_old)) =
   5.133 +      lthy
   5.134 +      |> Local_Theory.open_target |> snd
   5.135 +      |> fold_map (fn i =>
   5.136 +        Local_Theory.define ((co_rec_bind i, NoSyn), (co_rec_def_bind i, co_rec_spec i))) ks
   5.137 +      |>> apsnd split_list o split_list
   5.138 +      ||> `Local_Theory.close_target;
   5.139 +
   5.140 +    val phi = Proof_Context.export_morphism lthy_old lthy;
   5.141 +    val co_rec_names = map (fst o dest_Const o Morphism.term phi) co_rec_frees;
   5.142 +    val co_recs = @{map 2} (fn name => fn resT =>
   5.143 +      Const (name, co_rec_argTs ---> resT)) co_rec_names co_rec_resTs;
   5.144 +    val co_rec_defs = map (fn def =>
   5.145 +      mk_unabs_def n (Morphism.thm phi def RS meta_eq_to_obj_eq)) co_rec_def_frees;
   5.146 +
   5.147 +    val xtor_un_fold_xtor_thms = mk_xtor_un_fold_xtor_thms fp xtor_un_fold_unique map_id0s;
   5.148 +
   5.149 +    val co_rec_id_thms =
   5.150 +      let
   5.151 +        val goal = @{map 2} (fn T => fn t => HOLogic.mk_eq (t, HOLogic.id_const T)) Ts co_rec_ids
   5.152 +          |> Library.foldr1 HOLogic.mk_conj |> HOLogic.mk_Trueprop;
   5.153 +        val vars = Variable.add_free_names lthy goal [];
   5.154 +      in
   5.155 +        Goal.prove_sorry lthy vars [] goal
   5.156 +          (fn {context = ctxt, prems = _} => mk_xtor_co_rec_id_tac ctxt xtor_un_fold_xtor_thms
   5.157 +            xtor_un_fold_unique xtor_un_folds map_comps)
   5.158 +          |> Thm.close_derivation
   5.159 +          |> split_conj_thm
   5.160 +      end;
   5.161 +
   5.162 +    val co_rec_app_ss = map (fn co_rec => list_comb (co_rec, co_rec_ss)) co_recs;
   5.163 +    val co_products = @{map 2} (fn T => mk_co_product (HOLogic.id_const T)) Ts co_rec_app_ss;
   5.164 +    val co_rec_maps_rev = @{map 2} (fn Ds =>
   5.165 +      mk_map_of_bnf Ds (As @ case_fp fp Ts co_rec_Xs) (As @ case_fp fp co_rec_Xs Ts)) Dss pre_bnfs;
   5.166 +    fun mk_co_app f g x = case_fp fp (f $ (g $ x)) (g $ (f $ x));
   5.167 +    val co_rec_expand_thms = map (fn thm => thm RS
   5.168 +      case_fp fp @{thm convol_expand_snd} @{thm case_sum_expand_Inr_pointfree}) co_rec_id_thms;
   5.169 +    val xtor_co_rec_thms =
   5.170 +      let
   5.171 +        fun mk_goal co_rec s mapx xtor x =
   5.172 +          let
   5.173 +            val lhs = mk_co_app co_rec xtor x;
   5.174 +            val rhs = mk_co_app s (list_comb (mapx, ids @ co_products)) x;
   5.175 +          in
   5.176 +            mk_Trueprop_eq (lhs, rhs)
   5.177 +          end;
   5.178 +        val goals = @{map 5} mk_goal co_rec_app_ss co_rec_ss co_rec_maps_rev xtors xs;
   5.179 +      in
   5.180 +        map2 (fn goal => fn un_fold =>
   5.181 +          Variable.add_free_names lthy goal []
   5.182 +          |> (fn vars => Goal.prove_sorry lthy vars [] goal
   5.183 +            (fn {context = ctxt, prems = _} =>
   5.184 +              mk_xtor_co_rec_tac ctxt un_fold co_rec_defs co_rec_expand_thms))
   5.185 +          |> Thm.close_derivation)
   5.186 +        goals xtor_un_folds
   5.187 +      end;
   5.188 +
   5.189 +    val co_product_fs = @{map 2} (fn T => mk_co_product (HOLogic.id_const T)) Ts fs;
   5.190 +    val co_rec_expand'_thms = map (fn thm =>
   5.191 +      thm RS case_fp fp @{thm convol_expand_snd'} @{thm case_sum_expand_Inr'}) co_rec_id_thms;
   5.192 +    val xtor_co_rec_unique_thm =
   5.193 +      let
   5.194 +        fun mk_prem f s mapx xtor =
   5.195 +          let
   5.196 +            val lhs = mk_co_comp f xtor;
   5.197 +            val rhs = mk_co_comp s (list_comb (mapx, ids @ co_product_fs));
   5.198 +          in
   5.199 +            mk_Trueprop_eq (co_swap (lhs, rhs))
   5.200 +          end;
   5.201 +        val prems = @{map 4} mk_prem fs co_rec_ss co_rec_maps_rev xtors;
   5.202 +        val concl = @{map 2} (curry HOLogic.mk_eq) fs co_rec_app_ss
   5.203 +          |> Library.foldr1 HOLogic.mk_conj |> HOLogic.mk_Trueprop;
   5.204 +        val goal = Logic.list_implies (prems, concl);
   5.205 +        val vars = Variable.add_free_names lthy goal [];
   5.206 +      in
   5.207 +        Goal.prove_sorry lthy vars [] goal
   5.208 +          (fn {context = ctxt, prems = _} => mk_xtor_co_rec_unique_tac ctxt fp co_rec_defs
   5.209 +            co_rec_expand'_thms xtor_un_fold_unique map_id0s sym_map_comp0s)
   5.210 +        |> Thm.close_derivation
   5.211 +      end;
   5.212 +
   5.213 +    val xtor_co_rec_o_map_thms = mk_xtor_co_iter_o_map_thms fp true m xtor_co_rec_unique_thm
   5.214 +      (map (mk_pointfree lthy) xtor_maps) (map (mk_pointfree lthy) xtor_co_rec_thms)
   5.215 +      sym_map_comp0s map_cong0s;
   5.216 +
   5.217 +    val ABphiTs = @{map 2} mk_pred2T As Bs;
   5.218 +    val XYphiTs = @{map 2} mk_pred2T Xs Ys;
   5.219 +
   5.220 +    val ((ABphis, XYphis), names_lthy) = names_lthy
   5.221 +      |> mk_Frees "R" ABphiTs
   5.222 +      ||>> mk_Frees "S" XYphiTs;
   5.223 +
   5.224 +    val pre_rels =
   5.225 +      @{map 2} (fn Ds => mk_rel_of_bnf Ds (As @ co_rec_Xs) (Bs @ co_rec_Ys)) Dss pre_bnfs;
   5.226 +    val rels = @{map 3} (fn T => fn T' => Thm.prop_of #> HOLogic.dest_Trueprop
   5.227 +        #> fst o dest_comb #> fst o dest_comb #> funpow n (snd o dest_comb)
   5.228 +        #> case_fp fp (fst o dest_comb #> snd o dest_comb) (snd o dest_comb) #> head_of
   5.229 +        #> force_typ names_lthy (ABphiTs ---> mk_pred2T T T'))
   5.230 +      Ts Us xtor_un_fold_transfers;
   5.231 +
   5.232 +    fun tac {context = ctxt, prems = _} = mk_xtor_co_rec_transfer_tac ctxt fp n m co_rec_defs
   5.233 +      xtor_un_fold_transfers map_transfers xtor_rels;
   5.234 +
   5.235 +    val mk_rel_co_product = case_fp fp mk_rel_prod mk_rel_sum;
   5.236 +    val rec_phis =
   5.237 +      map2 (fn rel => mk_rel_co_product (Term.list_comb (rel, ABphis))) rels XYphis;
   5.238 +
   5.239 +    val xtor_co_rec_transfer_thms =
   5.240 +      mk_xtor_co_iter_transfer_thms fp pre_rels rec_phis XYphis rels ABphis
   5.241 +        co_recs (map (subst_atomic_types (ABs @ XYs)) co_recs) tac lthy;
   5.242 +
   5.243 +    val notes =
   5.244 +      [(case_fp fp ctor_recN dtor_corecN, xtor_co_rec_thms),
   5.245 +       (case_fp fp ctor_rec_uniqueN dtor_corec_uniqueN, split_conj_thm xtor_co_rec_unique_thm),
   5.246 +       (case_fp fp ctor_rec_o_mapN dtor_corec_o_mapN, xtor_co_rec_o_map_thms),
   5.247 +       (case_fp fp ctor_rec_transferN dtor_corec_transferN, xtor_co_rec_transfer_thms)]
   5.248 +      |> map (apsnd (map single))
   5.249 +      |> maps (fn (thmN, thmss) =>
   5.250 +        map2 (fn b => fn thms =>
   5.251 +          ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])]))
   5.252 +        bs thmss);
   5.253 +
   5.254 +     val lthy = lthy |> Config.get lthy bnf_internals ? snd o Local_Theory.notes notes;
   5.255 +  in
   5.256 +    ((co_recs,
   5.257 +     (xtor_co_rec_thms, xtor_co_rec_unique_thm, xtor_co_rec_o_map_thms, xtor_co_rec_transfer_thms)),
   5.258 +      lthy)
   5.259 +  end;
   5.260 +
   5.261  fun fixpoint_bnf extra_qualify construct_fp bs resBs Ds0 fp_eqs comp_cache0 lthy =
   5.262    let
   5.263      val time = time lthy;
     6.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.2 +++ b/src/HOL/Tools/BNF/bnf_fp_util_tactics.ML	Thu Apr 07 17:56:22 2016 +0200
     6.3 @@ -0,0 +1,79 @@
     6.4 +(*  Title:      HOL/Tools/BNF/bnf_fp_util_tactics.ML
     6.5 +    Author:     Dmitriy Traytel, ETH Z├╝rich
     6.6 +    Copyright   2016
     6.7 +
     6.8 +Common tactics for datatype and codatatype constructions.
     6.9 +*)
    6.10 +
    6.11 +signature BNF_FP_UTIL_TACTICS =
    6.12 +sig
    6.13 +
    6.14 +val mk_xtor_co_rec_id_tac: Proof.context -> thm list -> thm -> thm list -> thm list -> tactic
    6.15 +val mk_xtor_co_rec_tac: Proof.context -> thm -> thm list -> thm list -> tactic
    6.16 +val mk_xtor_co_rec_unique_tac: Proof.context -> BNF_Util.fp_kind -> thm list -> thm list -> thm ->
    6.17 +  thm list -> thm list -> tactic
    6.18 +val mk_xtor_co_rec_transfer_tac: Proof.context -> BNF_Util.fp_kind -> int -> int -> thm list ->
    6.19 +  thm list -> thm list -> thm list -> tactic
    6.20 +
    6.21 +end
    6.22 +
    6.23 +structure BNF_FP_Util_Tactics =
    6.24 +struct
    6.25 +
    6.26 +open BNF_Tactics
    6.27 +open BNF_Util
    6.28 +
    6.29 +fun mk_xtor_co_rec_id_tac ctxt xtor_un_fold_xtors xtor_un_fold_unique xtor_un_folds map_comps =
    6.30 +  unfold_thms_tac ctxt (map mk_sym xtor_un_fold_xtors) THEN
    6.31 +  HEADGOAL (rtac ctxt xtor_un_fold_unique THEN_ALL_NEW EVERY' [rtac ctxt ext,
    6.32 +    SELECT_GOAL (unfold_thms_tac ctxt
    6.33 +      (o_apply :: @{thms fst_convol' id_o sum.case} @ map_comps @ xtor_un_folds)),
    6.34 +    rtac ctxt refl]);
    6.35 +
    6.36 +fun mk_xtor_co_rec_tac ctxt un_fold co_rec_defs co_rec_expand_thms =
    6.37 +  unfold_thms_tac ctxt (un_fold ::
    6.38 +    @{thms o_apply sum.case snd_convol' case_sum_o_inj(2)} @ co_rec_defs @ co_rec_expand_thms) THEN
    6.39 +    HEADGOAL (rtac ctxt refl);
    6.40 +
    6.41 +fun mk_xtor_co_rec_unique_tac ctxt fp co_rec_defs co_rec_expand's un_fold_unique map_ids map_comps =
    6.42 +  unfold_thms_tac ctxt (co_rec_defs @ co_rec_expand's) THEN
    6.43 +  HEADGOAL (EVERY' [rtac ctxt un_fold_unique]) THEN
    6.44 +  unfold_thms_tac ctxt (map_ids @ map_comps @ case_fp fp
    6.45 +    @{thms id_o o_id convol_o fst_convol o_assoc[symmetric]}
    6.46 +    @{thms id_o o_id o_case_sum case_sum_o_inj(1) o_assoc}) THEN
    6.47 +  ALLGOALS (etac ctxt (case_fp fp
    6.48 +    @{thm arg_cong2[of _ _ _ _ BNF_Def.convol, OF refl]}
    6.49 +    @{thm arg_cong2[of _ _ _ _ case_sum, OF refl]}));
    6.50 +
    6.51 +fun mk_xtor_co_rec_transfer_tac ctxt fp n m defs un_fold_transfers pre_T_map_transfers xtor_rels =
    6.52 +  case_fp fp
    6.53 +    (CONJ_WRAP (fn (def, un_fold_transfer) =>
    6.54 +        REPEAT_DETERM (HEADGOAL (rtac ctxt rel_funI)) THEN
    6.55 +        unfold_thms_tac ctxt [def, o_apply] THEN
    6.56 +        HEADGOAL (rtac ctxt @{thm rel_funD[OF snd_transfer]} THEN'
    6.57 +          etac ctxt (mk_rel_funDN_rotated (n + 1) un_fold_transfer) THEN'
    6.58 +          EVERY' (map2 (fn pre_T_map_transfer => fn xtor_rel =>
    6.59 +            etac ctxt (mk_rel_funDN_rotated 2 @{thm convol_transfer}) THEN'
    6.60 +            rtac ctxt (mk_rel_funDN_rotated 2 @{thm comp_transfer}) THEN'
    6.61 +            rtac ctxt (mk_rel_funDN (m + n) pre_T_map_transfer) THEN'
    6.62 +            REPEAT_DETERM_N m o rtac ctxt @{thm id_transfer} THEN'
    6.63 +            REPEAT_DETERM o rtac ctxt @{thm fst_transfer} THEN'
    6.64 +            rtac ctxt rel_funI THEN'
    6.65 +            etac ctxt (xtor_rel RS iffD2)) pre_T_map_transfers xtor_rels)))
    6.66 +      (defs ~~ un_fold_transfers))
    6.67 +    (CONJ_WRAP (fn (def, un_fold_transfer) =>
    6.68 +        REPEAT_DETERM (HEADGOAL (rtac ctxt rel_funI)) THEN
    6.69 +        unfold_thms_tac ctxt [def, o_apply] THEN
    6.70 +        HEADGOAL (rtac ctxt (mk_rel_funDN (n + 1) un_fold_transfer) THEN'
    6.71 +          EVERY' (map2 (fn pre_T_map_transfer => fn xtor_rel =>
    6.72 +            etac ctxt (mk_rel_funDN_rotated 2 @{thm case_sum_transfer}) THEN'
    6.73 +            rtac ctxt (mk_rel_funDN 2 @{thm comp_transfer}) THEN'
    6.74 +            rtac ctxt (mk_rel_funDN (m + n) pre_T_map_transfer) THEN'
    6.75 +            REPEAT_DETERM_N m o rtac ctxt @{thm id_transfer} THEN'
    6.76 +            REPEAT_DETERM_N n o rtac ctxt @{thm Inl_transfer} THEN'
    6.77 +            rtac ctxt rel_funI THEN'
    6.78 +            etac ctxt (xtor_rel RS iffD1)) pre_T_map_transfers xtor_rels) THEN'
    6.79 +          etac ctxt (mk_rel_funDN 1 @{thm Inr_transfer})))
    6.80 +      (defs ~~ un_fold_transfers));
    6.81 +
    6.82 +end
    6.83 \ No newline at end of file
     7.1 --- a/src/HOL/Tools/BNF/bnf_gfp.ML	Thu Apr 07 17:26:22 2016 +0200
     7.2 +++ b/src/HOL/Tools/BNF/bnf_gfp.ML	Thu Apr 07 17:56:22 2016 +0200
     7.3 @@ -1602,52 +1602,6 @@
     7.4  
     7.5      val timer = time (timer "ctor definitions & thms");
     7.6  
     7.7 -    val corec_Inl_sum_thms =
     7.8 -      let
     7.9 -        val mor = mor_comp_thm OF [mor_case_sum_thm, mor_unfold_thm];
    7.10 -      in
    7.11 -        map2 (fn unique => fn unfold_dtor =>
    7.12 -          trans OF [mor RS unique, unfold_dtor]) unfold_unique_mor_thms unfold_dtor_thms
    7.13 -      end;
    7.14 -
    7.15 -    fun corec_bind i = nth external_bs (i - 1) |> Binding.prefix_name (dtor_corecN ^ "_");
    7.16 -    val corec_def_bind = rpair [] o Binding.concealed o Thm.def_binding o corec_bind;
    7.17 -
    7.18 -    fun mk_corec_strs corec_ss =
    7.19 -      @{map 3} (fn dtor => fn sum_s => fn mapx =>
    7.20 -        mk_case_sum
    7.21 -          (HOLogic.mk_comp (Term.list_comb (mapx, passive_ids @ corec_Inls), dtor), sum_s))
    7.22 -      dtors corec_ss corec_maps;
    7.23 -
    7.24 -    fun corec_spec i T AT =
    7.25 -      fold_rev (Term.absfree o Term.dest_Free) corec_ss
    7.26 -        (HOLogic.mk_comp (mk_unfold Ts (mk_corec_strs corec_ss) i, Inr_const T AT));
    7.27 -
    7.28 -    val ((corec_frees, (_, corec_def_frees)), (lthy, lthy_old)) =
    7.29 -      lthy
    7.30 -      |> Local_Theory.open_target |> snd
    7.31 -      |> @{fold_map 3} (fn i => fn T => fn AT =>
    7.32 -        Local_Theory.define ((corec_bind i, NoSyn), (corec_def_bind i, corec_spec i T AT)))
    7.33 -          ks Ts activeAs
    7.34 -      |>> apsnd split_list o split_list
    7.35 -      ||> `Local_Theory.close_target;
    7.36 -
    7.37 -    val phi = Proof_Context.export_morphism lthy_old lthy;
    7.38 -    val corecs = map (Morphism.term phi) corec_frees;
    7.39 -    val corec_names = map (fst o dest_Const) corecs;
    7.40 -    fun mk_corecs Ts passives actives =
    7.41 -      let val Tactives = map2 (curry mk_sumT) Ts actives;
    7.42 -      in
    7.43 -        @{map 3} (fn name => fn T => fn active =>
    7.44 -          Const (name, Library.foldr (op -->)
    7.45 -            (map2 (curry op -->) actives (mk_FTs (passives @ Tactives)), active --> T)))
    7.46 -        corec_names Ts actives
    7.47 -      end;
    7.48 -    fun mk_corec ss i = Term.list_comb (Const (nth corec_names (i - 1), Library.foldr (op -->)
    7.49 -      (map fastype_of ss, domain_type (fastype_of (nth ss (i - 1))) --> nth Ts (i - 1))), ss);
    7.50 -    val corec_defs = map (fn def =>
    7.51 -      mk_unabs_def n (Morphism.thm phi def RS meta_eq_to_obj_eq)) corec_def_frees;
    7.52 -
    7.53      val ((((((((zs, Jzs), Jzs_copy), Jzs1), Jzs2), unfold_fs), corec_ss), phis), _) =
    7.54        lthy
    7.55        |> mk_Frees "b" activeAs
    7.56 @@ -1659,57 +1613,6 @@
    7.57        ||>> mk_Frees "s" corec_sTs
    7.58        ||>> mk_Frees "P" (map2 mk_pred2T Ts Ts);
    7.59  
    7.60 -    val case_sums =
    7.61 -      map2 (fn T => fn i => mk_case_sum (HOLogic.id_const T, mk_corec corec_ss i)) Ts ks;
    7.62 -    val dtor_corec_thms =
    7.63 -      let
    7.64 -        fun mk_goal i corec_s corec_map dtor z =
    7.65 -          let
    7.66 -            val lhs = dtor $ (mk_corec corec_ss i $ z);
    7.67 -            val rhs = Term.list_comb (corec_map, passive_ids @ case_sums) $ (corec_s $ z);
    7.68 -          in
    7.69 -            mk_Trueprop_eq (lhs, rhs)
    7.70 -          end;
    7.71 -        val goals = @{map 5} mk_goal ks corec_ss corec_maps_rev dtors zs;
    7.72 -      in
    7.73 -        @{map 3} (fn goal => fn unfold => fn map_cong0 =>
    7.74 -          Variable.add_free_names lthy goal []
    7.75 -          |> (fn vars => Goal.prove_sorry lthy vars [] goal
    7.76 -            (fn {context = ctxt, prems = _} => mk_corec_tac ctxt m corec_defs unfold map_cong0
    7.77 -              corec_Inl_sum_thms))
    7.78 -          |> Thm.close_derivation)
    7.79 -        goals dtor_unfold_thms map_cong0s
    7.80 -      end;
    7.81 -
    7.82 -    val corec_unique_mor_thm =
    7.83 -      let
    7.84 -        val id_fs = map2 (fn T => fn f => mk_case_sum (HOLogic.id_const T, f)) Ts unfold_fs;
    7.85 -        val prem = HOLogic.mk_Trueprop (mk_mor corec_UNIVs (mk_corec_strs corec_ss) UNIVs dtors id_fs);
    7.86 -        fun mk_fun_eq f i = HOLogic.mk_eq (f, mk_corec corec_ss i);
    7.87 -        val unique = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
    7.88 -          (map2 mk_fun_eq unfold_fs ks));
    7.89 -        val vars = fold (Variable.add_free_names lthy) [prem, unique] [];
    7.90 -      in
    7.91 -        Goal.prove_sorry lthy vars [] (Logic.mk_implies (prem, unique))
    7.92 -          (fn {context = ctxt, prems = _} => mk_corec_unique_mor_tac ctxt corec_defs
    7.93 -            corec_Inl_sum_thms unfold_unique_mor_thm)
    7.94 -          |> Thm.close_derivation
    7.95 -      end;
    7.96 -
    7.97 -    val map_id0s_o_id =
    7.98 -      map (fn thm =>
    7.99 -        mk_trans (thm RS @{thm arg_cong2[of _ _ _ _ "op o", OF _ refl]}) @{thm id_comp})
   7.100 -      map_id0s;
   7.101 -
   7.102 -    val (dtor_corec_unique_thms, dtor_corec_unique_thm) =
   7.103 -      `split_conj_thm (split_conj_prems n
   7.104 -        (mor_UNIV_thm RS iffD2 RS corec_unique_mor_thm)
   7.105 -        |> unfold_thms lthy (@{thms o_case_sum comp_id id_comp comp_assoc[symmetric]
   7.106 -           case_sum_o_inj(1)} @ map_id0s_o_id @ sym_map_comps)
   7.107 -        OF replicate n @{thm arg_cong2[of _ _ _ _ case_sum, OF refl]});
   7.108 -
   7.109 -    val timer = time (timer "corec definitions & thms");
   7.110 -
   7.111      val (coinduct_params, dtor_coinduct_thm) =
   7.112        let
   7.113          val rels = map (Term.subst_atomic_types ((activeAs ~~ Ts) @ (activeBs ~~ Ts))) relsAsBs;
   7.114 @@ -2661,9 +2564,6 @@
   7.115      val dtor_unfold_o_Jmap_thms = mk_xtor_co_iter_o_map_thms Greatest_FP false m
   7.116        dtor_unfold_unique_thm dtor_Jmap_o_thms (map (mk_pointfree lthy) dtor_unfold_thms)
   7.117        sym_map_comps map_cong0s;
   7.118 -    val dtor_corec_o_Jmap_thms = mk_xtor_co_iter_o_map_thms Greatest_FP true m
   7.119 -      dtor_corec_unique_thm dtor_Jmap_o_thms (map (mk_pointfree lthy) dtor_corec_thms)
   7.120 -      sym_map_comps map_cong0s;
   7.121  
   7.122      val rels = map2 (fn Ds => mk_rel_of_bnf Ds allAs allBs') Dss bnfs;
   7.123      val Jrels = if m = 0 then map HOLogic.eq_const Ts
   7.124 @@ -2676,20 +2576,19 @@
   7.125            (map map_transfer_of_bnf bnfs) dtor_unfold_thms)
   7.126          lthy;
   7.127  
   7.128 -    val corec_allAs = passiveAs @ map2 (curry mk_sumT) Ts activeAs;
   7.129 -    val corec_allBs = passiveBs @ map2 (curry mk_sumT) Ts' activeBs;
   7.130 -    val corec_rels = map2 (fn Ds => mk_rel_of_bnf Ds corec_allAs corec_allBs) Dss bnfs;
   7.131 -    val corec_activephis =
   7.132 -      map2 (fn Jrel => mk_rel_sum (Term.list_comb (Jrel, Jphis))) Jrels activephis;
   7.133 -    val dtor_corec_transfer_thms =
   7.134 -      mk_xtor_co_iter_transfer_thms Greatest_FP corec_rels corec_activephis activephis Jrels Jphis
   7.135 -        (mk_corecs Ts passiveAs activeAs) (mk_corecs Ts' passiveBs activeBs)
   7.136 -        (fn {context = ctxt, prems = _} => mk_dtor_corec_transfer_tac ctxt n m corec_defs
   7.137 -           dtor_unfold_transfer_thms (map map_transfer_of_bnf bnfs) dtor_Jrel_thms)
   7.138 -        lthy;
   7.139 -
   7.140      val timer = time (timer "relator coinduction");
   7.141  
   7.142 +    fun mk_Ts As = map (typ_subst_atomic (passiveAs ~~ As)) Ts;
   7.143 +    val export = map (Morphism.term (Local_Theory.target_morphism lthy))
   7.144 +    val ((corecs, (dtor_corec_thms, dtor_corec_unique_thm, dtor_corec_o_Jmap_thms,
   7.145 +        dtor_corec_transfer_thms)), lthy) = lthy
   7.146 +      |> derive_xtor_co_recs Greatest_FP external_bs mk_Ts (Dss, resDs) bnfs
   7.147 +        (export dtors) (export unfolds)
   7.148 +        dtor_unfold_unique_thm dtor_unfold_thms dtor_unfold_transfer_thms
   7.149 +        dtor_Jmap_thms dtor_Jrel_thms;
   7.150 +
   7.151 +    val timer = time (timer "recursor");
   7.152 +
   7.153      val common_notes =
   7.154        [(dtor_coinductN, [dtor_coinduct_thm]),
   7.155        (dtor_rel_coinductN, [Jrel_coinduct_thm])]
   7.156 @@ -2700,10 +2599,6 @@
   7.157        [(ctor_dtorN, ctor_dtor_thms),
   7.158        (ctor_exhaustN, ctor_exhaust_thms),
   7.159        (ctor_injectN, ctor_inject_thms),
   7.160 -      (dtor_corecN, dtor_corec_thms),
   7.161 -      (dtor_corec_o_mapN, dtor_corec_o_Jmap_thms),
   7.162 -      (dtor_corec_transferN, dtor_corec_transfer_thms),
   7.163 -      (dtor_corec_uniqueN, dtor_corec_unique_thms),
   7.164        (dtor_ctorN, dtor_ctor_thms),
   7.165        (dtor_exhaustN, dtor_exhaust_thms),
   7.166        (dtor_injectN, dtor_inject_thms),
   7.167 @@ -2721,7 +2616,7 @@
   7.168  
   7.169      val fp_res =
   7.170        {Ts = Ts, bnfs = Jbnfs, pre_bnfs = bnfs, absT_infos = absT_infos,
   7.171 -       ctors = ctors, dtors = dtors, xtor_un_folds_legacy = unfolds, xtor_co_recs = corecs,
   7.172 +       ctors = ctors, dtors = dtors, xtor_un_folds_legacy = unfolds, xtor_co_recs = export corecs,
   7.173         xtor_co_induct = dtor_coinduct_thm, dtor_ctors = dtor_ctor_thms, ctor_dtors = ctor_dtor_thms,
   7.174         ctor_injects = ctor_inject_thms, dtor_injects = dtor_inject_thms, xtor_maps = dtor_Jmap_thms,
   7.175         xtor_map_unique = dtor_Jmap_unique_thm, xtor_setss = dtor_Jset_thmss',
     8.1 --- a/src/HOL/Tools/BNF/bnf_lfp.ML	Thu Apr 07 17:26:22 2016 +0200
     8.2 +++ b/src/HOL/Tools/BNF/bnf_lfp.ML	Thu Apr 07 17:56:22 2016 +0200
     8.3 @@ -1202,50 +1202,6 @@
     8.4  
     8.5      val timer = time (timer "dtor definitions & thms");
     8.6  
     8.7 -    val fst_rec_pair_thms =
     8.8 -      let
     8.9 -        val mor = mor_comp_thm OF [mor_fold_thm, mor_convol_thm];
    8.10 -      in
    8.11 -        map2 (fn unique => fn fold_ctor =>
    8.12 -          trans OF [mor RS unique, fold_ctor]) fold_unique_mor_thms fold_ctor_thms
    8.13 -      end;
    8.14 -
    8.15 -    fun rec_bind i = nth external_bs (i - 1) |> Binding.prefix_name (ctor_recN ^ "_");
    8.16 -    val rec_def_bind = rpair [] o Binding.concealed o Thm.def_binding o rec_bind;
    8.17 -
    8.18 -    fun mk_rec_strs rec_ss =
    8.19 -      @{map 3} (fn ctor => fn prod_s => fn mapx =>
    8.20 -        mk_convol (HOLogic.mk_comp (ctor, Term.list_comb (mapx, passive_ids @ rec_fsts)), prod_s))
    8.21 -      ctors rec_ss rec_maps;
    8.22 -
    8.23 -    fun rec_spec i T AT =
    8.24 -      fold_rev (Term.absfree o Term.dest_Free) rec_ss
    8.25 -        (HOLogic.mk_comp (snd_const (HOLogic.mk_prodT (T, AT)), mk_fold Ts (mk_rec_strs rec_ss) i));
    8.26 -
    8.27 -    val ((rec_frees, (_, rec_def_frees)), (lthy, lthy_old)) =
    8.28 -      lthy
    8.29 -      |> Local_Theory.open_target |> snd
    8.30 -      |> @{fold_map 3} (fn i => fn T => fn AT =>
    8.31 -        Local_Theory.define ((rec_bind i, NoSyn), (rec_def_bind i, rec_spec i T AT))) ks Ts activeAs
    8.32 -      |>> apsnd split_list o split_list
    8.33 -      ||> `Local_Theory.close_target;
    8.34 -
    8.35 -    val phi = Proof_Context.export_morphism lthy_old lthy;
    8.36 -    val recs = map (Morphism.term phi) rec_frees;
    8.37 -    val rec_names = map (fst o dest_Const) recs;
    8.38 -    fun mk_recs Ts passives actives =
    8.39 -      let val Tactives = map2 (curry HOLogic.mk_prodT) Ts actives;
    8.40 -      in
    8.41 -        @{map 3} (fn name => fn T => fn active =>
    8.42 -          Const (name, Library.foldr (op -->)
    8.43 -            (map2 (curry op -->) (mk_FTs (passives @ Tactives)) actives, T --> active)))
    8.44 -        rec_names Ts actives
    8.45 -      end;
    8.46 -    fun mk_rec ss i = Term.list_comb (Const (nth rec_names (i - 1), Library.foldr (op -->)
    8.47 -      (map fastype_of ss, nth Ts (i - 1) --> range_type (fastype_of (nth ss (i - 1))))), ss);
    8.48 -    val rec_defs = map (fn def =>
    8.49 -      mk_unabs_def n (Morphism.thm phi def RS meta_eq_to_obj_eq)) rec_def_frees;
    8.50 -
    8.51      val (((((((((Izs, (Izs1, Izs1'))), (Izs2, Izs2')), xFs), yFs), fs), rec_ss), init_phis), _) =
    8.52        lthy
    8.53        |> mk_Frees "z" Ts
    8.54 @@ -1260,48 +1216,6 @@
    8.55      val phis = map2 retype_const_or_free (map mk_pred1T Ts) init_phis;
    8.56      val phi2s = map2 retype_const_or_free (map2 mk_pred2T Ts Ts') init_phis;
    8.57  
    8.58 -    val convols = map2 (fn T => fn i => mk_convol (HOLogic.id_const T, mk_rec rec_ss i)) Ts ks;
    8.59 -    val ctor_rec_thms =
    8.60 -      let
    8.61 -        fun mk_goal i rec_s rec_map ctor x =
    8.62 -          let
    8.63 -            val lhs = mk_rec rec_ss i $ (ctor $ x);
    8.64 -            val rhs = rec_s $ (Term.list_comb (rec_map, passive_ids @ convols) $ x);
    8.65 -          in
    8.66 -            mk_Trueprop_eq (lhs, rhs)
    8.67 -          end;
    8.68 -        val goals = @{map 5} mk_goal ks rec_ss rec_maps_rev ctors xFs;
    8.69 -      in
    8.70 -        map2 (fn goal => fn foldx =>
    8.71 -          Variable.add_free_names lthy goal []
    8.72 -          |> (fn vars => Goal.prove_sorry lthy vars [] goal
    8.73 -            (fn {context = ctxt, prems = _} => mk_rec_tac ctxt rec_defs foldx fst_rec_pair_thms))
    8.74 -          |> Thm.close_derivation)
    8.75 -        goals ctor_fold_thms
    8.76 -      end;
    8.77 -
    8.78 -    val rec_unique_mor_thm =
    8.79 -      let
    8.80 -        val id_fs = map2 (fn T => fn f => mk_convol (HOLogic.id_const T, f)) Ts fs;
    8.81 -        val prem = HOLogic.mk_Trueprop (mk_mor UNIVs ctors rec_UNIVs (mk_rec_strs rec_ss) id_fs);
    8.82 -        fun mk_fun_eq f i = HOLogic.mk_eq (f, mk_rec rec_ss i);
    8.83 -        val unique = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj (map2 mk_fun_eq fs ks));
    8.84 -        val vars = fold (Variable.add_free_names lthy) [prem, unique] [];
    8.85 -      in
    8.86 -        Goal.prove_sorry lthy vars [] (Logic.mk_implies (prem, unique))
    8.87 -          (fn {context = ctxt, prems = _} => mk_rec_unique_mor_tac ctxt rec_defs fst_rec_pair_thms
    8.88 -            fold_unique_mor_thm)
    8.89 -          |> Thm.close_derivation
    8.90 -      end;
    8.91 -
    8.92 -    val (ctor_rec_unique_thms, ctor_rec_unique_thm) =
    8.93 -      `split_conj_thm (split_conj_prems n
    8.94 -        (mor_UNIV_thm RS iffD2 RS rec_unique_mor_thm)
    8.95 -        |> unfold_thms lthy (@{thms convol_o comp_id id_comp comp_assoc fst_convol} @
    8.96 -           map_id0s @ sym_map_comps) OF replicate n @{thm arg_cong2[of _ _ _ _ convol, OF refl]});
    8.97 -
    8.98 -    val timer = time (timer "rec definitions & thms");
    8.99 -
   8.100      val (ctor_induct_thm, induct_params) =
   8.101        let
   8.102          fun mk_prem phi ctor sets x =
   8.103 @@ -1909,8 +1823,6 @@
   8.104  
   8.105      val ctor_fold_o_Imap_thms = mk_xtor_co_iter_o_map_thms Least_FP false m ctor_fold_unique_thm
   8.106        ctor_Imap_o_thms (map (mk_pointfree lthy) ctor_fold_thms) sym_map_comps map_cong0s;
   8.107 -    val ctor_rec_o_Imap_thms = mk_xtor_co_iter_o_map_thms Least_FP true m ctor_rec_unique_thm
   8.108 -      ctor_Imap_o_thms (map (mk_pointfree lthy) ctor_rec_thms) sym_map_comps map_cong0s;
   8.109  
   8.110      val Irels = if m = 0 then map HOLogic.eq_const Ts
   8.111        else map (mk_rel_of_bnf deads passiveAs passiveBs) Ibnfs;
   8.112 @@ -1927,19 +1839,17 @@
   8.113            (map map_transfer_of_bnf bnfs) ctor_fold_thms)
   8.114          lthy;
   8.115  
   8.116 -    val rec_allAs = passiveAs @ map2 (curry HOLogic.mk_prodT) Ts activeAs;
   8.117 -    val rec_allBs = passiveBs @ map2 (curry HOLogic.mk_prodT) Ts' activeBs;
   8.118 -    val rec_rels = map2 (fn Ds => mk_rel_of_bnf Ds rec_allAs rec_allBs) Dss bnfs;
   8.119 -    val rec_activephis =
   8.120 -      map2 (fn Irel => mk_rel_prod (Term.list_comb (Irel, Iphis))) Irels activephis;
   8.121 -    val ctor_rec_transfer_thms =
   8.122 -      mk_xtor_co_iter_transfer_thms Least_FP rec_rels rec_activephis activephis Irels Iphis
   8.123 -        (mk_recs Ts passiveAs activeAs) (mk_recs Ts' passiveBs activeBs)
   8.124 -        (fn {context = ctxt, prems = _} => mk_ctor_rec_transfer_tac ctxt n m rec_defs
   8.125 -           ctor_fold_transfer_thms (map map_transfer_of_bnf bnfs) ctor_Irel_thms)
   8.126 -        lthy;
   8.127 +    val timer = time (timer "relator induction");
   8.128  
   8.129 -    val timer = time (timer "relator induction");
   8.130 +    fun mk_Ts As = map (typ_subst_atomic (passiveAs ~~ As)) Ts;
   8.131 +    val export = map (Morphism.term (Local_Theory.target_morphism lthy))
   8.132 +    val ((recs, (ctor_rec_thms, ctor_rec_unique_thm, ctor_rec_o_Imap_thms, ctor_rec_transfer_thms)),
   8.133 +        lthy) = lthy
   8.134 +      |> derive_xtor_co_recs Least_FP external_bs mk_Ts (Dss, resDs) bnfs
   8.135 +        (export ctors) (export folds)
   8.136 +        ctor_fold_unique_thm ctor_fold_thms ctor_fold_transfer_thms ctor_Imap_thms ctor_Irel_thms;
   8.137 +
   8.138 +    val timer = time (timer "recursor");
   8.139  
   8.140      val common_notes =
   8.141        [(ctor_inductN, [ctor_induct_thm]),
   8.142 @@ -1955,11 +1865,7 @@
   8.143        (ctor_fold_o_mapN, ctor_fold_o_Imap_thms),
   8.144        (ctor_fold_transferN, ctor_fold_transfer_thms),
   8.145        (ctor_fold_uniqueN, ctor_fold_unique_thms),
   8.146 -      (ctor_rec_o_mapN, ctor_rec_o_Imap_thms),
   8.147 -      (ctor_rec_transferN, ctor_rec_transfer_thms),
   8.148 -      (ctor_rec_uniqueN, ctor_rec_unique_thms),
   8.149        (ctor_injectN, ctor_inject_thms),
   8.150 -      (ctor_recN, ctor_rec_thms),
   8.151        (dtor_ctorN, dtor_ctor_thms),
   8.152        (dtor_exhaustN, dtor_exhaust_thms),
   8.153        (dtor_injectN, dtor_inject_thms)]
   8.154 @@ -1973,7 +1879,7 @@
   8.155  
   8.156      val fp_res =
   8.157        {Ts = Ts, bnfs = Ibnfs, pre_bnfs = bnfs, absT_infos = absT_infos,
   8.158 -       ctors = ctors, dtors = dtors, xtor_un_folds_legacy = folds, xtor_co_recs = recs,
   8.159 +       ctors = ctors, dtors = dtors, xtor_un_folds_legacy = folds, xtor_co_recs = export recs,
   8.160         xtor_co_induct = ctor_induct_thm, dtor_ctors = dtor_ctor_thms,
   8.161         ctor_dtors = ctor_dtor_thms, ctor_injects = ctor_inject_thms,
   8.162         dtor_injects = dtor_inject_thms, xtor_maps = ctor_Imap_thms,