19 val nested_simps = @{thms o_def[abs_def] id_def split fst_conv snd_conv}; |
19 val nested_simps = @{thms o_def[abs_def] id_def split fst_conv snd_conv}; |
20 |
20 |
21 fun is_new_datatype ctxt s = |
21 fun is_new_datatype ctxt s = |
22 (case fp_sugar_of ctxt s of SOME {fp = Least_FP, ...} => true | _ => false); |
22 (case fp_sugar_of ctxt s of SOME {fp = Least_FP, ...} => true | _ => false); |
23 |
23 |
24 fun basic_lfp_sugar_of C fun_arg_Tsss ({T, fp_res_index, ctr_defs, ctr_sugar, co_rec = recx, |
24 fun basic_lfp_sugar_of C fun_arg_Tsss ({T, fp_res_index, ctr_sugar, co_rec = recx, |
25 co_rec_thms = rec_thms, ...} : fp_sugar) = |
25 co_rec_thms = rec_thms, ...} : 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_sugar = ctr_sugar, |
27 ctr_sugar = ctr_sugar, recx = recx, rec_thms = rec_thms}; |
27 recx = recx, rec_thms = rec_thms}; |
28 |
28 |
29 fun get_basic_lfp_sugars bs arg_Ts callers 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 {fp_nesting_bnfs, common_co_inducts = [common_induct], ...} :: _, |
32 fp_sugars as {fp_nesting_bnfs, common_co_inducts = [common_induct], ...} :: _, |