# HG changeset patch # User blanchet # Date 1473715075 -7200 # Node ID dca6fabd806006f5ed9ef71b7038dd884414d35a # Parent 0f5e735e364029fd14f1fe5cb48b0b743643d85b make (co)induct component of 'fp_sugar' optional, for the benefit of nonuniform (co)datatypes and other similar extensions diff -r 0f5e735e3640 -r dca6fabd8060 src/HOL/Tools/BNF/bnf_fp_def_sugar.ML --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Mon Sep 12 20:31:28 2016 +0200 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Mon Sep 12 23:17:55 2016 +0200 @@ -64,7 +64,7 @@ live_nesting_bnfs: BNF_Def.bnf list, fp_ctr_sugar: fp_ctr_sugar, fp_bnf_sugar: fp_bnf_sugar, - fp_co_induct_sugar: fp_co_induct_sugar} + fp_co_induct_sugar: fp_co_induct_sugar option} val transfer_plugin: string @@ -311,7 +311,7 @@ live_nesting_bnfs: bnf list, fp_ctr_sugar: fp_ctr_sugar, fp_bnf_sugar: fp_bnf_sugar, - fp_co_induct_sugar: fp_co_induct_sugar}; + fp_co_induct_sugar: fp_co_induct_sugar option}; val transfer_plugin = Plugin_Name.declare_setup @{binding transfer}; @@ -381,7 +381,7 @@ live_nesting_bnfs = map (morph_bnf phi) live_nesting_bnfs, fp_ctr_sugar = morph_fp_ctr_sugar phi fp_ctr_sugar, fp_bnf_sugar = morph_fp_bnf_sugar phi fp_bnf_sugar, - fp_co_induct_sugar = morph_fp_co_induct_sugar phi fp_co_induct_sugar}; + fp_co_induct_sugar = Option.map (morph_fp_co_induct_sugar phi) fp_co_induct_sugar}; val transfer_fp_sugar = morph_fp_sugar o Morphism.transfer_morphism; @@ -426,8 +426,8 @@ map_thmss common_co_inducts co_inductss co_rec_thmss co_rec_discss co_rec_selsss rel_injectss rel_distinctss map_disc_iffss map_selsss rel_selss rel_intross rel_casess pred_injectss set_thmss set_selsssss set_introsssss set_casess ctr_transferss case_transferss disc_transferss - co_rec_disc_iffss co_rec_codess co_rec_transferss common_rel_co_inducts rel_co_inductss - common_set_inducts set_inductss sel_transferss co_rec_o_mapss noted = + sel_transferss co_rec_disc_iffss co_rec_codess co_rec_transferss common_rel_co_inducts + rel_co_inductss common_set_inducts set_inductss co_rec_o_mapss noted = let val fp_sugars = map_index (fn (kk, T) => @@ -458,7 +458,7 @@ set_selssss = nth set_selsssss kk, set_introssss = nth set_introsssss kk, set_cases = nth set_casess kk}, - fp_co_induct_sugar = + fp_co_induct_sugar = SOME {co_rec = nth co_recs kk, common_co_inducts = common_co_inducts, co_inducts = nth co_inductss kk, @@ -2653,9 +2653,9 @@ recs rec_defs map_thmss [induct_thm] (map single induct_thms) rec_thmss (replicate nn []) (replicate nn []) rel_injectss rel_distinctss map_disc_iffss map_selsss rel_selss rel_intross rel_casess pred_injectss set_thmss set_selsssss set_introsssss set_casess - ctr_transferss case_transferss disc_transferss (replicate nn []) (replicate nn []) - rec_transfer_thmss common_rel_induct_thms rel_induct_thmss [] (replicate nn []) - sel_transferss rec_o_map_thmss + ctr_transferss case_transferss disc_transferss sel_transferss (replicate nn []) + (replicate nn []) rec_transfer_thmss common_rel_induct_thms rel_induct_thmss [] + (replicate nn []) rec_o_map_thmss end; fun derive_corec_transfer_thms lthy corecs corec_defs = @@ -2829,10 +2829,10 @@ (transpose [coinduct_thms, coinduct_strong_thms]) corec_thmss corec_disc_thmss corec_sel_thmsss rel_injectss rel_distinctss map_disc_iffss map_selsss rel_selss rel_intross rel_casess pred_injectss set_thmss set_selsssss set_introsssss set_casess - ctr_transferss case_transferss disc_transferss corec_disc_iff_thmss + ctr_transferss case_transferss disc_transferss sel_transferss corec_disc_iff_thmss (map single corec_code_thms) corec_transfer_thmss common_rel_coinduct_thms rel_coinduct_thmss set_induct_thms (replicate nn (if nn = 1 then set_induct_thms else [])) - sel_transferss map_o_corec_thmss + map_o_corec_thmss end; val lthy = lthy diff -r 0f5e735e3640 -r dca6fabd8060 src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML --- a/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML Mon Sep 12 20:31:28 2016 +0200 +++ b/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML Mon Sep 12 23:17:55 2016 +0200 @@ -304,7 +304,7 @@ fp_bnf_sugar = {map_disc_iffs, map_selss, rel_injects, rel_distincts, rel_sels, rel_intros, rel_cases, pred_injects, set_thms, set_selssss, set_introssss, set_cases, ...}, - fp_co_induct_sugar = {co_rec_disc_iffs, co_rec_codes, co_rec_transfers, + fp_co_induct_sugar = SOME {co_rec_disc_iffs, co_rec_codes, co_rec_transfers, co_rec_o_maps, common_rel_co_inducts, rel_co_inducts, common_set_inducts, set_inducts, ...}, ...} : fp_sugar) = @@ -334,7 +334,7 @@ set_selssss = set_selssss, set_introssss = set_introssss, set_cases = set_cases}, - fp_co_induct_sugar = + fp_co_induct_sugar = SOME {co_rec = co_rec, common_co_inducts = common_co_inducts, co_inducts = co_inducts, @@ -421,8 +421,9 @@ fun the_fp_sugar_of (T as Type (T_name, _)) = (case fp_sugar_of lthy T_name of - SOME (fp_sugar as {fp = fp', ...}) => if fp = fp' then fp_sugar else not_co_datatype T - | NONE => not_co_datatype T); + SOME (fp_sugar as {fp = fp', fp_co_induct_sugar = SOME _, ...}) => + if fp = fp' then fp_sugar else not_co_datatype T + | _ => not_co_datatype T); fun gather_types _ _ rev_seens gen_seen [] = (rev rev_seens, gen_seen) | gather_types lthy rho rev_seens gen_seen ((T as Type (_, tyargs)) :: Ts) = diff -r 0f5e735e3640 -r dca6fabd8060 src/HOL/Tools/BNF/bnf_fp_rec_sugar_transfer.ML --- a/src/HOL/Tools/BNF/bnf_fp_rec_sugar_transfer.ML Mon Sep 12 20:31:28 2016 +0200 +++ b/src/HOL/Tools/BNF/bnf_fp_rec_sugar_transfer.ML Mon Sep 12 23:17:55 2016 +0200 @@ -157,7 +157,7 @@ in Goal.prove lthy vars [] goal (fn {context = ctxt, prems = _} => mk_gfp_rec_sugar_transfer_tac ctxt def - (#co_rec_def (#fp_co_induct_sugar (nth fp_sugars kk))) + (#co_rec_def (the (#fp_co_induct_sugar (nth fp_sugars kk)))) (map (#type_definition o #absT_info) fp_sugars) (maps (#xtor_co_rec_transfers o #fp_res) fp_sugars) (map (rel_def_of_bnf o #pre_bnf) fp_sugars) diff -r 0f5e735e3640 -r dca6fabd8060 src/HOL/Tools/BNF/bnf_gfp_grec.ML --- a/src/HOL/Tools/BNF/bnf_gfp_grec.ML Mon Sep 12 20:31:28 2016 +0200 +++ b/src/HOL/Tools/BNF/bnf_gfp_grec.ML Mon Sep 12 23:17:55 2016 +0200 @@ -2110,7 +2110,7 @@ val sig_fp_bnf_sugar = #fp_bnf_sugar sig_fp_sugar; val ssig_fp_bnf_sugar = #fp_bnf_sugar ssig_fp_sugar; - val ssig_fp_induct_sugar = #fp_co_induct_sugar ssig_fp_sugar; + val ssig_fp_induct_sugar = the (#fp_co_induct_sugar ssig_fp_sugar); val sig_ctr_sugar = #ctr_sugar sig_fp_ctr_sugar; val ssig_ctr_sugar = #ctr_sugar ssig_fp_ctr_sugar; @@ -2331,8 +2331,8 @@ val sig_fp_bnf_sugar = #fp_bnf_sugar sig_fp_sugar; val old_ssig_fp_bnf_sugar = #fp_bnf_sugar old_ssig_fp_sugar; val ssig_fp_bnf_sugar = #fp_bnf_sugar ssig_fp_sugar; - val old_ssig_fp_induct_sugar = #fp_co_induct_sugar old_ssig_fp_sugar; - val ssig_fp_induct_sugar = #fp_co_induct_sugar ssig_fp_sugar; + val old_ssig_fp_induct_sugar = the (#fp_co_induct_sugar old_ssig_fp_sugar); + val ssig_fp_induct_sugar = the (#fp_co_induct_sugar ssig_fp_sugar); val old_ssig_ctr_sugar = #ctr_sugar old_ssig_fp_ctr_sugar; val sig_ctr_sugar = #ctr_sugar sig_fp_ctr_sugar; @@ -2683,9 +2683,9 @@ val old1_ssig_fp_bnf_sugar = #fp_bnf_sugar old1_ssig_fp_sugar; val old2_ssig_fp_bnf_sugar = #fp_bnf_sugar old2_ssig_fp_sugar; val ssig_fp_bnf_sugar = #fp_bnf_sugar ssig_fp_sugar; - val old1_ssig_fp_induct_sugar = #fp_co_induct_sugar old1_ssig_fp_sugar; - val old2_ssig_fp_induct_sugar = #fp_co_induct_sugar old2_ssig_fp_sugar; - val ssig_fp_induct_sugar = #fp_co_induct_sugar ssig_fp_sugar; + val old1_ssig_fp_induct_sugar = the (#fp_co_induct_sugar old1_ssig_fp_sugar); + val old2_ssig_fp_induct_sugar = the (#fp_co_induct_sugar old2_ssig_fp_sugar); + val ssig_fp_induct_sugar = the (#fp_co_induct_sugar ssig_fp_sugar); val old1_ssig_ctr_sugar = #ctr_sugar old1_ssig_fp_ctr_sugar; val old2_ssig_ctr_sugar = #ctr_sugar old2_ssig_fp_ctr_sugar; diff -r 0f5e735e3640 -r dca6fabd8060 src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML --- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Mon Sep 12 20:31:28 2016 +0200 +++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Mon Sep 12 23:17:55 2016 +0200 @@ -501,7 +501,7 @@ val thy = Proof_Context.theory_of lthy0; val ((missing_res_Ts, perm0_kks, fp_sugars as {fp_nesting_bnfs, - fp_co_induct_sugar = {common_co_inducts = common_coinduct_thms, ...}, ...} :: _, + fp_co_induct_sugar = SOME {common_co_inducts = common_coinduct_thms, ...}, ...} :: _, (_, gfp_sugar_thms)), lthy) = nested_to_mutual_fps (K true) Greatest_FP bs res_Ts callers callssss0 lthy0; @@ -525,7 +525,8 @@ val perm_Ts = map #T perm_fp_sugars; val perm_Xs = map #X perm_fp_sugars; val perm_Cs = - map (domain_type o body_fun_type o fastype_of o #co_rec o #fp_co_induct_sugar) perm_fp_sugars; + map (domain_type o body_fun_type o fastype_of o #co_rec o the o #fp_co_induct_sugar) + perm_fp_sugars; val Xs_TCs = perm_Xs ~~ (perm_Ts ~~ perm_Cs); fun zip_corecT (Type (s, Us)) = [Type (s, map (mk_sumTN o zip_corecT) Us)] @@ -592,8 +593,9 @@ end; fun mk_spec ({T, fp_ctr_sugar = {ctr_sugar as {exhaust_discs, sel_defs, ...}, ...}, - fp_co_induct_sugar = {co_rec = corec, co_rec_thms = corec_thms, co_rec_discs = corec_discs, - co_rec_selss = corec_selss, ...}, ...} : fp_sugar) p_is q_isss f_isss f_Tsss = + fp_co_induct_sugar = SOME {co_rec = corec, co_rec_thms = corec_thms, + co_rec_discs = corec_discs, co_rec_selss = corec_selss, ...}, ...} : fp_sugar) p_is q_isss + f_isss f_Tsss = {T = T, corec = mk_co_rec thy Greatest_FP perm_Cs' (substAT T) corec, exhaust_discs = exhaust_discs, sel_defs = sel_defs, fp_nesting_maps = maps (map_thms_of_type lthy o T_of_bnf) fp_nesting_bnfs, diff -r 0f5e735e3640 -r dca6fabd8060 src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML --- a/src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML Mon Sep 12 20:31:28 2016 +0200 +++ b/src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML Mon Sep 12 23:17:55 2016 +0200 @@ -104,7 +104,7 @@ [[[]], [@{thms setr.intros[OF refl]}]]], set_cases = @{thms setl.cases[simplified hypsubst_in_prems] setr.cases[simplified hypsubst_in_prems]}}, - fp_co_induct_sugar = + fp_co_induct_sugar = SOME {co_rec = Const (@{const_name case_sum}, map (fn Ts => (Ts ---> C)) ctr_Tss ---> fpT --> C), common_co_inducts = @{thms sum.induct}, co_inducts = @{thms sum.induct}, @@ -176,7 +176,7 @@ [[[], @{thms snds.intros[of "(a, b)" for a b, simplified snd_conv]}]]], set_cases = @{thms fsts.cases[simplified eq_fst_iff ex_neg_all_pos] snds.cases[simplified eq_snd_iff ex_neg_all_pos]}}, - fp_co_induct_sugar = + fp_co_induct_sugar = SOME {co_rec = Const (@{const_name case_prod}, (ctr_Ts ---> C) --> fpT --> C), common_co_inducts = @{thms prod.induct}, co_inducts = @{thms prod.induct}, diff -r 0f5e735e3640 -r dca6fabd8060 src/HOL/Tools/BNF/bnf_lfp_compat.ML --- a/src/HOL/Tools/BNF/bnf_lfp_compat.ML Mon Sep 12 20:31:28 2016 +0200 +++ b/src/HOL/Tools/BNF/bnf_lfp_compat.ML Mon Sep 12 23:17:55 2016 +0200 @@ -214,9 +214,9 @@ fun checked_fp_sugar_of s = (case fp_sugar_of lthy s of - SOME (fp_sugar as {fp, ...}) => + SOME (fp_sugar as {fp, fp_co_induct_sugar = SOME _, ...}) => if member (op =) prefs Include_GFPs orelse fp = Least_FP then fp_sugar else not_datatype s - | NONE => not_datatype s); + | _ => not_datatype s); val fpTs0 as Type (_, var_As) :: _ = map (#T o checked_fp_sugar_of o fst o dest_Type) @@ -299,10 +299,10 @@ val Xs' = map #X fp_sugars'; val ctrXs_Tsss' = map (map (map substAT) o #ctrXs_Tss o #fp_ctr_sugar) fp_sugars'; val ctrss' = map2 mk_ctr_of fp_sugars' fpTs'; - val {fp_co_induct_sugar = {common_co_inducts = induct :: _, ...}, ...} :: _ = fp_sugars'; - val inducts = map (hd o #co_inducts o #fp_co_induct_sugar) fp_sugars'; - val recs = map (#co_rec o #fp_co_induct_sugar) fp_sugars'; - val rec_thmss = map (#co_rec_thms o #fp_co_induct_sugar) fp_sugars'; + val {fp_co_induct_sugar = SOME {common_co_inducts = induct :: _, ...}, ...} :: _ = fp_sugars'; + val inducts = map (hd o #co_inducts o the o #fp_co_induct_sugar) fp_sugars'; + val recs = map (#co_rec o the o #fp_co_induct_sugar) fp_sugars'; + val rec_thmss = map (#co_rec_thms o the o #fp_co_induct_sugar) fp_sugars'; fun is_nested_rec_type (Type (@{type_name fun}, [_, T])) = member (op =) Xs' (body_type T) | is_nested_rec_type _ = false; diff -r 0f5e735e3640 -r dca6fabd8060 src/HOL/Tools/BNF/bnf_lfp_countable.ML --- a/src/HOL/Tools/BNF/bnf_lfp_countable.ML Mon Sep 12 20:31:28 2016 +0200 +++ b/src/HOL/Tools/BNF/bnf_lfp_countable.ML Mon Sep 12 23:17:55 2016 +0200 @@ -132,7 +132,7 @@ fun lfp_sugar_of s = (case fp_sugar_of ctxt s of - SOME (fp_sugar as {fp = Least_FP, ...}) => fp_sugar + SOME (fp_sugar as {fp = Least_FP, fp_co_induct_sugar = SOME _, ...}) => fp_sugar | _ => not_datatype s); val fpTs0 as Type (_, var_As) :: _ = @@ -153,16 +153,17 @@ HOLogic.eq_const fpT $ x $ Bound 0)); val fp_sugars as - {fp_nesting_bnfs, fp_co_induct_sugar = {common_co_inducts = induct :: _, ...}, ...} :: _ = + {fp_nesting_bnfs, fp_co_induct_sugar = SOME {common_co_inducts = induct :: _, ...}, + ...} :: _ = map (the o fp_sugar_of ctxt o fst o dest_Type) fpTs0; val ctr_sugars = map (#ctr_sugar o #fp_ctr_sugar) fp_sugars; val ctrss0 = map #ctrs ctr_sugars; val ns = map length ctrss0; - val recs0 = map (#co_rec o #fp_co_induct_sugar) fp_sugars; + val recs0 = map (#co_rec o the o #fp_co_induct_sugar) fp_sugars; val nchotomys = map #nchotomy ctr_sugars; val injectss = map #injects ctr_sugars; - val rec_thmss = map (#co_rec_thms o #fp_co_induct_sugar) fp_sugars; + val rec_thmss = map (#co_rec_thms o the o #fp_co_induct_sugar) fp_sugars; val map_comps' = map (unfold_thms ctxt @{thms comp_def} o map_comp_of_bnf) fp_nesting_bnfs; val inj_map_strongs' = map (Thm.permute_prems 0 ~1 o inj_map_strong_of_bnf) fp_nesting_bnfs; diff -r 0f5e735e3640 -r dca6fabd8060 src/HOL/Tools/BNF/bnf_lfp_rec_sugar_more.ML --- a/src/HOL/Tools/BNF/bnf_lfp_rec_sugar_more.ML Mon Sep 12 20:31:28 2016 +0200 +++ b/src/HOL/Tools/BNF/bnf_lfp_rec_sugar_more.ML Mon Sep 12 23:17:55 2016 +0200 @@ -28,12 +28,14 @@ fun is_new_datatype _ @{type_name nat} = true | is_new_datatype ctxt s = - (case fp_sugar_of ctxt s of SOME {fp = Least_FP, ...} => true | _ => false); + (case fp_sugar_of ctxt s of + SOME {fp = Least_FP, fp_co_induct_sugar = SOME _, ...} => true + | _ => false); fun basic_lfp_sugar_of C fun_arg_Tsss ({T, fp_res_index, fp_ctr_sugar = {ctr_sugar, ...}, - fp_co_induct_sugar = {co_rec = recx, co_rec_thms = rec_thms, ...}, ...} : fp_sugar) = - {T = T, fp_res_index = fp_res_index, C = C, fun_arg_Tsss = fun_arg_Tsss, ctr_sugar = ctr_sugar, - recx = recx, rec_thms = rec_thms}; + fp_co_induct_sugar = SOME {co_rec = recx, co_rec_thms = rec_thms, ...}, ...} : fp_sugar) = + {T = T, fp_res_index = fp_res_index, C = C, fun_arg_Tsss = fun_arg_Tsss, ctr_sugar = ctr_sugar, + recx = recx, rec_thms = rec_thms}; fun basic_lfp_sugars_of _ [@{typ nat}] _ _ lthy = ([], [0], [nat_basic_lfp_sugar], [], [], [], TrueI (*dummy*), [], false, lthy) @@ -41,7 +43,7 @@ let val ((missing_arg_Ts, perm0_kks, fp_sugars as {fp_nesting_bnfs, - fp_co_induct_sugar = {common_co_inducts = [common_induct], ...}, ...} :: _, + fp_co_induct_sugar = SOME {common_co_inducts = [common_induct], ...}, ...} :: _, (lfp_sugar_thms, _)), lthy) = nested_to_mutual_fps (K true) Least_FP bs arg_Ts callers callssss0 lthy0; @@ -49,7 +51,7 @@ val Ts = map #T fp_sugars; val Xs = map #X fp_sugars; - val Cs = map (body_type o fastype_of o #co_rec o #fp_co_induct_sugar) fp_sugars; + val Cs = map (body_type o fastype_of o #co_rec o the o #fp_co_induct_sugar) fp_sugars; val Xs_TCs = Xs ~~ (Ts ~~ Cs); fun zip_XrecT (Type (s, Us)) = [Type (s, map (HOLogic.mk_tupleT o zip_XrecT) Us)] diff -r 0f5e735e3640 -r dca6fabd8060 src/HOL/Tools/BNF/bnf_lfp_size.ML --- a/src/HOL/Tools/BNF/bnf_lfp_size.ML Mon Sep 12 20:31:28 2016 +0200 +++ b/src/HOL/Tools/BNF/bnf_lfp_size.ML Mon Sep 12 23:17:55 2016 +0200 @@ -97,7 +97,8 @@ rtac ctxt @{thm trans_less_add2})); fun generate_datatype_size (fp_sugars as ({T = Type (_, As), BT = Type (_, Bs), fp = Least_FP, - fp_res = {bnfs = fp_bnfs, ...}, fp_nesting_bnfs, live_nesting_bnfs, ...} : fp_sugar) :: _) + fp_res = {bnfs = fp_bnfs, ...}, fp_nesting_bnfs, live_nesting_bnfs, + fp_co_induct_sugar = SOME _, ...} : fp_sugar) :: _) lthy0 = let val data = Data.get (Context.Proof lthy0); @@ -108,8 +109,8 @@ val B_ify = Term.typ_subst_atomic (As ~~ Bs); - val recs = map (#co_rec o #fp_co_induct_sugar) fp_sugars; - val rec_thmss = map (#co_rec_thms o #fp_co_induct_sugar) fp_sugars; + val recs = map (#co_rec o the o #fp_co_induct_sugar) fp_sugars; + val rec_thmss = map (#co_rec_thms o the o #fp_co_induct_sugar) fp_sugars; val rec_Ts as rec_T1 :: _ = map fastype_of recs; val rec_arg_Ts = binder_fun_types rec_T1; val Cs = map body_type rec_Ts; @@ -337,7 +338,7 @@ curry HOLogic.mk_eq) size_gen_o_map_lhss size_gen_o_map_rhss; val rec_o_maps = - fold_rev (curry (op @) o #co_rec_o_maps o #fp_co_induct_sugar) fp_sugars []; + fold_rev (curry (op @) o #co_rec_o_maps o the o #fp_co_induct_sugar) fp_sugars []; val size_gen_o_map_thmss = if nested_size_gen_o_maps_complete then diff -r 0f5e735e3640 -r dca6fabd8060 src/HOL/Tools/Transfer/transfer_bnf.ML --- a/src/HOL/Tools/Transfer/transfer_bnf.ML Mon Sep 12 20:31:28 2016 +0200 +++ b/src/HOL/Tools/Transfer/transfer_bnf.ML Mon Sep 12 23:17:55 2016 +0200 @@ -248,7 +248,7 @@ val fp_ctr_sugar = #fp_ctr_sugar fp_sugar val transfer_rules = #ctr_transfers fp_ctr_sugar @ #case_transfers fp_ctr_sugar @ #disc_transfers fp_ctr_sugar @ #sel_transfers fp_ctr_sugar - @ (#co_rec_transfers o #fp_co_induct_sugar) fp_sugar + @ these (Option.map #co_rec_transfers (#fp_co_induct_sugar fp_sugar)) val transfer_attr = @{attributes [transfer_rule]} in map (fn thm => (Binding.empty_atts, [([thm], transfer_attr)])) transfer_rules