34 val co_recs = [Const (@{const_name ctor_rec}, (fpT --> C) --> (fpT --> C))]; |
34 val co_recs = [Const (@{const_name ctor_rec}, (fpT --> C) --> (fpT --> C))]; |
35 val co_rec_thms = [map_id0_of_bnf fp_bnf RS @{thm ctor_rec}]; |
35 val co_rec_thms = [map_id0_of_bnf fp_bnf RS @{thm ctor_rec}]; |
36 val co_rec_unique_thm = map_id0_of_bnf fp_bnf RS @{thm ctor_rec_unique}; |
36 val co_rec_unique_thm = map_id0_of_bnf fp_bnf RS @{thm ctor_rec_unique}; |
37 in |
37 in |
38 {Ts = [fpT], bnfs = [fp_bnf], pre_bnfs = [ID_bnf], absT_infos = [trivial_absT_info_of fpT], |
38 {Ts = [fpT], bnfs = [fp_bnf], pre_bnfs = [ID_bnf], absT_infos = [trivial_absT_info_of fpT], |
39 ctors = xtors, dtors = xtors, xtor_un_folds_legacy = co_recs, |
39 ctors = xtors, dtors = xtors, xtor_un_folds = co_recs, |
40 xtor_co_recs = co_recs, xtor_co_induct = @{thm xtor_induct}, dtor_ctors = @{thms xtor_xtor}, |
40 xtor_co_recs = co_recs, xtor_co_induct = @{thm xtor_induct}, dtor_ctors = @{thms xtor_xtor}, |
41 ctor_dtors = @{thms xtor_xtor}, ctor_injects = @{thms xtor_inject}, |
41 ctor_dtors = @{thms xtor_xtor}, ctor_injects = @{thms xtor_inject}, |
42 dtor_injects = @{thms xtor_inject}, xtor_maps = [xtor_map], |
42 dtor_injects = @{thms xtor_inject}, xtor_maps = [xtor_map], |
43 xtor_map_unique = @{thm xtor_map_unique}, xtor_setss = [xtor_sets], xtor_rels = [xtor_rel], |
43 xtor_map_unique = @{thm xtor_map_unique}, xtor_setss = [xtor_sets], xtor_rels = [xtor_rel], |
44 xtor_un_fold_thms_legacy = co_rec_thms, xtor_co_rec_thms = co_rec_thms, |
44 xtor_un_fold_thms = co_rec_thms, xtor_co_rec_thms = co_rec_thms, |
45 xtor_un_fold_unique_legacy = co_rec_unique_thm, xtor_co_rec_unique = co_rec_unique_thm, |
45 xtor_un_fold_unique = co_rec_unique_thm, xtor_co_rec_unique = co_rec_unique_thm, |
46 xtor_un_fold_o_maps_legacy = [ctor_rec_o_map], xtor_co_rec_o_maps = [ctor_rec_o_map], |
46 xtor_un_fold_o_maps = [ctor_rec_o_map], xtor_co_rec_o_maps = [ctor_rec_o_map], |
47 xtor_un_fold_transfers_legacy = [], xtor_co_rec_transfers = [], |
47 xtor_un_fold_transfers = [], xtor_co_rec_transfers = [], |
48 xtor_rel_co_induct = xtor_rel_induct, dtor_set_inducts = []} |
48 xtor_rel_co_induct = xtor_rel_induct, dtor_set_inducts = []} |
49 end; |
49 end; |
50 |
50 |
51 fun fp_sugar_of_sum ctxt = |
51 fun fp_sugar_of_sum ctxt = |
52 let |
52 let |