24 fun basic_lfp_sugar_of C fun_arg_Tsss ({T, fp_res_index, ctr_defs, ctr_sugar, co_iters = iters, |
24 fun basic_lfp_sugar_of C fun_arg_Tsss ({T, fp_res_index, ctr_defs, ctr_sugar, co_iters = iters, |
25 co_iter_thmss = iter_thmss, ...} : fp_sugar) = |
25 co_iter_thmss = iter_thmss, ...} : fp_sugar) = |
26 {T = T, fp_res_index = fp_res_index, C = C, fun_arg_Tsss = fun_arg_Tsss, ctr_defs = ctr_defs, |
26 {T = T, fp_res_index = fp_res_index, C = C, fun_arg_Tsss = fun_arg_Tsss, ctr_defs = ctr_defs, |
27 ctr_sugar = ctr_sugar, recx = co_rec_of iters, rec_thms = co_rec_of iter_thmss}; |
27 ctr_sugar = ctr_sugar, recx = co_rec_of iters, rec_thms = co_rec_of iter_thmss}; |
28 |
28 |
29 fun get_basic_lfp_sugars bs arg_Ts get_indices callssss0 lthy0 = |
29 fun get_basic_lfp_sugars bs arg_Ts callers callssss0 lthy0 = |
30 let |
30 let |
31 val ((missing_arg_Ts, perm0_kks, |
31 val ((missing_arg_Ts, perm0_kks, |
32 fp_sugars as {nested_bnfs, co_inducts = [induct_thm], ...} :: _, (lfp_sugar_thms, _)), |
32 fp_sugars as {nested_bnfs, co_inducts = [induct_thm], ...} :: _, (lfp_sugar_thms, _)), |
33 lthy) = |
33 lthy) = |
34 nested_to_mutual_fps Least_FP bs arg_Ts get_indices callssss0 lthy0; |
34 nested_to_mutual_fps Least_FP bs arg_Ts callers callssss0 lthy0; |
35 |
35 |
36 val Ts = map #T fp_sugars; |
36 val Ts = map #T fp_sugars; |
|
37 val Xs = map #X fp_sugars; |
37 val Cs = map (body_type o fastype_of o co_rec_of o #co_iters) fp_sugars; |
38 val Cs = map (body_type o fastype_of o co_rec_of o #co_iters) fp_sugars; |
38 val Ts_Cs = Ts ~~ Cs; |
39 val Xs_TCs = Xs ~~ (Ts ~~ Cs); |
39 |
40 |
40 fun zip_recT (T as Type (s, Ts)) = |
41 fun zip_recT (Type (s, Us)) = [Type (s, map (HOLogic.mk_tupleT o zip_recT) Us)] |
41 (case AList.lookup (op =) Ts_Cs T of |
42 | zip_recT U = |
42 SOME C => [T, C] |
43 (case AList.lookup (op =) Xs_TCs U of |
43 | NONE => [Type (s, map (HOLogic.mk_tupleT o zip_recT) Ts)]) |
44 SOME (T, C) => [T, C] |
44 | zip_recT T = [T]; |
45 | NONE => [U]); |
45 |
46 |
46 val ctrss = map (#ctrs o #ctr_sugar) fp_sugars; |
47 val ctrXs_Tsss = map #ctrXs_Tss fp_sugars; |
47 val ctr_Tsss = map (map (binder_types o fastype_of)) ctrss; |
48 val fun_arg_Tssss = map (map (map zip_recT)) ctrXs_Tsss; |
48 val fun_arg_Tssss = map (map (map zip_recT)) ctr_Tsss; |
|
49 |
49 |
50 val nested_map_idents = map (unfold_thms lthy @{thms id_def} o map_id0_of_bnf) nested_bnfs; |
50 val nested_map_idents = map (unfold_thms lthy @{thms id_def} o map_id0_of_bnf) nested_bnfs; |
51 val nested_map_comps = map map_comp_of_bnf nested_bnfs; |
51 val nested_map_comps = map map_comp_of_bnf nested_bnfs; |
52 in |
52 in |
53 (missing_arg_Ts, perm0_kks, map3 basic_lfp_sugar_of Cs fun_arg_Tssss fp_sugars, |
53 (missing_arg_Ts, perm0_kks, map3 basic_lfp_sugar_of Cs fun_arg_Tssss fp_sugars, |