499 fun corec_specs_of bs arg_Ts res_Ts callers callssss0 lthy0 = |
499 fun corec_specs_of bs arg_Ts res_Ts callers callssss0 lthy0 = |
500 let |
500 let |
501 val thy = Proof_Context.theory_of lthy0; |
501 val thy = Proof_Context.theory_of lthy0; |
502 |
502 |
503 val ((missing_res_Ts, perm0_kks, fp_sugars as {fp_nesting_bnfs, |
503 val ((missing_res_Ts, perm0_kks, fp_sugars as {fp_nesting_bnfs, |
504 fp_co_induct_sugar = {common_co_inducts = common_coinduct_thms, ...}, ...} :: _, |
504 fp_co_induct_sugar = SOME {common_co_inducts = common_coinduct_thms, ...}, ...} :: _, |
505 (_, gfp_sugar_thms)), lthy) = |
505 (_, gfp_sugar_thms)), lthy) = |
506 nested_to_mutual_fps (K true) Greatest_FP bs res_Ts callers callssss0 lthy0; |
506 nested_to_mutual_fps (K true) Greatest_FP bs res_Ts callers callssss0 lthy0; |
507 |
507 |
508 val coinduct_attrs_pair = |
508 val coinduct_attrs_pair = |
509 (case gfp_sugar_thms of SOME ((_, attrs_pair), _, _, _, _) => attrs_pair | NONE => ([], [])); |
509 (case gfp_sugar_thms of SOME ((_, attrs_pair), _, _, _, _) => attrs_pair | NONE => ([], [])); |
523 val perm_ns' = map length perm_ctrXs_Tsss'; |
523 val perm_ns' = map length perm_ctrXs_Tsss'; |
524 |
524 |
525 val perm_Ts = map #T perm_fp_sugars; |
525 val perm_Ts = map #T perm_fp_sugars; |
526 val perm_Xs = map #X perm_fp_sugars; |
526 val perm_Xs = map #X perm_fp_sugars; |
527 val perm_Cs = |
527 val perm_Cs = |
528 map (domain_type o body_fun_type o fastype_of o #co_rec o #fp_co_induct_sugar) perm_fp_sugars; |
528 map (domain_type o body_fun_type o fastype_of o #co_rec o the o #fp_co_induct_sugar) |
|
529 perm_fp_sugars; |
529 val Xs_TCs = perm_Xs ~~ (perm_Ts ~~ perm_Cs); |
530 val Xs_TCs = perm_Xs ~~ (perm_Ts ~~ perm_Cs); |
530 |
531 |
531 fun zip_corecT (Type (s, Us)) = [Type (s, map (mk_sumTN o zip_corecT) Us)] |
532 fun zip_corecT (Type (s, Us)) = [Type (s, map (mk_sumTN o zip_corecT) Us)] |
532 | zip_corecT U = |
533 | zip_corecT U = |
533 (case AList.lookup (op =) Xs_TCs U of |
534 (case AList.lookup (op =) Xs_TCs U of |
590 @{map 14} mk_ctr_spec ctrs discs selss p_ios q_isss f_isss f_Tsss discIs sel_thmss |
591 @{map 14} mk_ctr_spec ctrs discs selss p_ios q_isss f_isss f_Tsss discIs sel_thmss |
591 distinct_discsss collapses corec_thms corec_discs corec_selss |
592 distinct_discsss collapses corec_thms corec_discs corec_selss |
592 end; |
593 end; |
593 |
594 |
594 fun mk_spec ({T, fp_ctr_sugar = {ctr_sugar as {exhaust_discs, sel_defs, ...}, ...}, |
595 fun mk_spec ({T, fp_ctr_sugar = {ctr_sugar as {exhaust_discs, sel_defs, ...}, ...}, |
595 fp_co_induct_sugar = {co_rec = corec, co_rec_thms = corec_thms, co_rec_discs = corec_discs, |
596 fp_co_induct_sugar = SOME {co_rec = corec, co_rec_thms = corec_thms, |
596 co_rec_selss = corec_selss, ...}, ...} : fp_sugar) p_is q_isss f_isss f_Tsss = |
597 co_rec_discs = corec_discs, co_rec_selss = corec_selss, ...}, ...} : fp_sugar) p_is q_isss |
|
598 f_isss f_Tsss = |
597 {T = T, corec = mk_co_rec thy Greatest_FP perm_Cs' (substAT T) corec, |
599 {T = T, corec = mk_co_rec thy Greatest_FP perm_Cs' (substAT T) corec, |
598 exhaust_discs = exhaust_discs, sel_defs = sel_defs, |
600 exhaust_discs = exhaust_discs, sel_defs = sel_defs, |
599 fp_nesting_maps = maps (map_thms_of_type lthy o T_of_bnf) fp_nesting_bnfs, |
601 fp_nesting_maps = maps (map_thms_of_type lthy o T_of_bnf) fp_nesting_bnfs, |
600 fp_nesting_map_ident0s = map map_ident0_of_bnf fp_nesting_bnfs, |
602 fp_nesting_map_ident0s = map map_ident0_of_bnf fp_nesting_bnfs, |
601 fp_nesting_map_comps = map map_comp_of_bnf fp_nesting_bnfs, |
603 fp_nesting_map_comps = map map_comp_of_bnf fp_nesting_bnfs, |