18 map_disc_iffs: thm list, |
18 map_disc_iffs: thm list, |
19 map_sels: thm list, |
19 map_sels: thm list, |
20 rel_injects: thm list, |
20 rel_injects: thm list, |
21 rel_distincts: thm list, |
21 rel_distincts: thm list, |
22 rel_sels: thm list, |
22 rel_sels: thm list, |
23 rel_intros: thm list} |
23 rel_intros: thm list, |
|
24 rel_cases: thm list} |
24 |
25 |
25 type fp_co_induct_sugar = |
26 type fp_co_induct_sugar = |
26 {co_rec: term, |
27 {co_rec: term, |
27 common_co_inducts: thm list, |
28 common_co_inducts: thm list, |
28 co_inducts: thm list, |
29 co_inducts: thm list, |
174 map_disc_iffs: thm list, |
175 map_disc_iffs: thm list, |
175 map_sels: thm list, |
176 map_sels: thm list, |
176 rel_injects: thm list, |
177 rel_injects: thm list, |
177 rel_distincts: thm list, |
178 rel_distincts: thm list, |
178 rel_sels: thm list, |
179 rel_sels: thm list, |
179 rel_intros: thm list}; |
180 rel_intros: thm list, |
|
181 rel_cases: thm list}; |
180 |
182 |
181 type fp_co_induct_sugar = |
183 type fp_co_induct_sugar = |
182 {co_rec: term, |
184 {co_rec: term, |
183 common_co_inducts: thm list, |
185 common_co_inducts: thm list, |
184 co_inducts: thm list, |
186 co_inducts: thm list, |
201 fp_ctr_sugar: fp_ctr_sugar, |
203 fp_ctr_sugar: fp_ctr_sugar, |
202 fp_bnf_sugar: fp_bnf_sugar, |
204 fp_bnf_sugar: fp_bnf_sugar, |
203 fp_co_induct_sugar: fp_co_induct_sugar}; |
205 fp_co_induct_sugar: fp_co_induct_sugar}; |
204 |
206 |
205 fun morph_fp_bnf_sugar phi ({map_thms, map_disc_iffs, map_sels, rel_injects, rel_distincts, |
207 fun morph_fp_bnf_sugar phi ({map_thms, map_disc_iffs, map_sels, rel_injects, rel_distincts, |
206 rel_sels, rel_intros} : fp_bnf_sugar) = |
208 rel_sels, rel_intros, rel_cases} : fp_bnf_sugar) = |
207 {map_thms = map (Morphism.thm phi) map_thms, |
209 {map_thms = map (Morphism.thm phi) map_thms, |
208 map_disc_iffs = map (Morphism.thm phi) map_disc_iffs, |
210 map_disc_iffs = map (Morphism.thm phi) map_disc_iffs, |
209 map_sels = map (Morphism.thm phi) map_sels, |
211 map_sels = map (Morphism.thm phi) map_sels, |
210 rel_injects = map (Morphism.thm phi) rel_injects, |
212 rel_injects = map (Morphism.thm phi) rel_injects, |
211 rel_distincts = map (Morphism.thm phi) rel_distincts, |
213 rel_distincts = map (Morphism.thm phi) rel_distincts, |
212 rel_sels = map (Morphism.thm phi) rel_sels, |
214 rel_sels = map (Morphism.thm phi) rel_sels, |
213 rel_intros = map (Morphism.thm phi) rel_intros}; |
215 rel_intros = map (Morphism.thm phi) rel_intros, |
|
216 rel_cases = map (Morphism.thm phi) rel_cases}; |
214 |
217 |
215 fun morph_fp_co_induct_sugar phi ({co_rec, common_co_inducts, co_inducts, co_rec_def, co_rec_thms, |
218 fun morph_fp_co_induct_sugar phi ({co_rec, common_co_inducts, co_inducts, co_rec_def, co_rec_thms, |
216 co_rec_discs, co_rec_selss} : fp_co_induct_sugar) = |
219 co_rec_discs, co_rec_selss} : fp_co_induct_sugar) = |
217 {co_rec = Morphism.term phi co_rec, |
220 {co_rec = Morphism.term phi co_rec, |
218 common_co_inducts = map (Morphism.thm phi) common_co_inducts, |
221 common_co_inducts = map (Morphism.thm phi) common_co_inducts, |
292 register_fp_sugars_raw fp_sugars #> interpret_fp_sugars plugins fp_sugars; |
295 register_fp_sugars_raw fp_sugars #> interpret_fp_sugars plugins fp_sugars; |
293 |
296 |
294 fun interpret_bnfs_register_fp_sugars plugins Ts BTs Xs fp pre_bnfs absT_infos fp_nesting_bnfs |
297 fun interpret_bnfs_register_fp_sugars plugins Ts BTs Xs fp pre_bnfs absT_infos fp_nesting_bnfs |
295 live_nesting_bnfs fp_res ctrXs_Tsss ctr_defss ctr_sugars co_recs co_rec_defs map_thmss |
298 live_nesting_bnfs fp_res ctrXs_Tsss ctr_defss ctr_sugars co_recs co_rec_defs map_thmss |
296 common_co_inducts co_inductss co_rec_thmss co_rec_discss co_rec_selsss rel_injectss |
299 common_co_inducts co_inductss co_rec_thmss co_rec_discss co_rec_selsss rel_injectss |
297 rel_distinctss map_disc_iffss map_selss rel_selss rel_intross noted = |
300 rel_distinctss map_disc_iffss map_selss rel_selss rel_intross rel_casess noted = |
298 let |
301 let |
299 val fp_sugars = |
302 val fp_sugars = |
300 map_index (fn (kk, T) => |
303 map_index (fn (kk, T) => |
301 {T = T, BT = nth BTs kk, X = nth Xs kk, fp = fp, fp_res = fp_res, fp_res_index = kk, |
304 {T = T, BT = nth BTs kk, X = nth Xs kk, fp = fp, fp_res = fp_res, fp_res_index = kk, |
302 pre_bnf = nth pre_bnfs kk, absT_info = nth absT_infos kk, |
305 pre_bnf = nth pre_bnfs kk, absT_info = nth absT_infos kk, |
310 map_disc_iffs = nth map_disc_iffss kk, |
313 map_disc_iffs = nth map_disc_iffss kk, |
311 map_sels = nth map_selss kk, |
314 map_sels = nth map_selss kk, |
312 rel_injects = nth rel_injectss kk, |
315 rel_injects = nth rel_injectss kk, |
313 rel_distincts = nth rel_distinctss kk, |
316 rel_distincts = nth rel_distinctss kk, |
314 rel_sels = nth rel_selss kk, |
317 rel_sels = nth rel_selss kk, |
315 rel_intros = nth rel_intross kk}, |
318 rel_intros = nth rel_intross kk, |
|
319 rel_cases = nth rel_casess kk}, |
316 fp_co_induct_sugar = |
320 fp_co_induct_sugar = |
317 {co_rec = nth co_recs kk, |
321 {co_rec = nth co_recs kk, |
318 common_co_inducts = common_co_inducts, |
322 common_co_inducts = common_co_inducts, |
319 co_inducts = nth co_inductss kk, |
323 co_inducts = nth co_inductss kk, |
320 co_rec_def = nth co_rec_defs kk, |
324 co_rec_def = nth co_rec_defs kk, |
470 ctr_Tss abs |
474 ctr_Tss abs |
471 ({casex, case_thms, discs, selss, ctrs, exhaust, exhaust_discs, disc_thmss, sel_thmss, injects, |
475 ({casex, case_thms, discs, selss, ctrs, exhaust, exhaust_discs, disc_thmss, sel_thmss, injects, |
472 distincts, distinct_discsss, ...} : ctr_sugar) |
476 distincts, distinct_discsss, ...} : ctr_sugar) |
473 lthy = |
477 lthy = |
474 if live = 0 then |
478 if live = 0 then |
475 (([], [], [], [], [], [], [], []), lthy) |
479 (([], [], [], [], [], [], [], [], []), lthy) |
476 else |
480 else |
477 let |
481 let |
478 val n = length ctr_Tss; |
482 val n = length ctr_Tss; |
479 val ks = 1 upto n; |
483 val ks = 1 upto n; |
480 val ms = map length ctr_Tss; |
484 val ms = map length ctr_Tss; |
957 map subst map_sel_thms, |
961 map subst map_sel_thms, |
958 map subst rel_inject_thms, |
962 map subst rel_inject_thms, |
959 map subst rel_distinct_thms, |
963 map subst rel_distinct_thms, |
960 map subst rel_sel_thms, |
964 map subst rel_sel_thms, |
961 map subst rel_intro_thms, |
965 map subst rel_intro_thms, |
|
966 [subst rel_cases_thm], |
962 map (map subst) set0_thmss), lthy') |
967 map (map subst) set0_thmss), lthy') |
963 end; |
968 end; |
964 |
969 |
965 type lfp_sugar_thms = (thm list * thm * Token.src list) * (thm list list * Token.src list); |
970 type lfp_sugar_thms = (thm list * thm * Token.src list) * (thm list list * Token.src list); |
966 |
971 |
2061 #> massage_res, lthy') |
2066 #> massage_res, lthy') |
2062 end; |
2067 end; |
2063 |
2068 |
2064 fun wrap_ctrs_derive_map_set_rel_thms_define_co_rec_for_types (wrap_one_etc, lthy) = |
2069 fun wrap_ctrs_derive_map_set_rel_thms_define_co_rec_for_types (wrap_one_etc, lthy) = |
2065 fold_map I wrap_one_etc lthy |
2070 fold_map I wrap_one_etc lthy |
2066 |>> apsnd split_list o apfst (apsnd split_list4 o apfst split_list8 o split_list) |
2071 |>> apsnd split_list o apfst (apsnd split_list4 o apfst split_list9 o split_list) |
2067 o split_list; |
2072 o split_list; |
2068 |
2073 |
2069 fun mk_simp_thms ({injects, distincts, case_thms, ...} : ctr_sugar) co_recs map_thms rel_injects |
2074 fun mk_simp_thms ({injects, distincts, case_thms, ...} : ctr_sugar) co_recs map_thms rel_injects |
2070 rel_distincts setss = |
2075 rel_distincts setss = |
2071 injects @ distincts @ case_thms @ co_recs @ map_thms @ rel_injects @ rel_distincts @ flat setss; |
2076 injects @ distincts @ case_thms @ co_recs @ map_thms @ rel_injects @ rel_distincts @ flat setss; |
2095 |> map Thm.close_derivation |
2100 |> map Thm.close_derivation |
2096 end; |
2101 end; |
2097 |
2102 |
2098 fun derive_note_induct_recs_thms_for_types |
2103 fun derive_note_induct_recs_thms_for_types |
2099 ((((map_thmss, map_disc_iffss, map_selss, rel_injectss, rel_distinctss, rel_selss, |
2104 ((((map_thmss, map_disc_iffss, map_selss, rel_injectss, rel_distinctss, rel_selss, |
2100 rel_intross, setss), |
2105 rel_intross, rel_casess, setss), |
2101 (ctrss, _, ctr_defss, ctr_sugars)), |
2106 (ctrss, _, ctr_defss, ctr_sugars)), |
2102 (recs, rec_defs)), lthy) = |
2107 (recs, rec_defs)), lthy) = |
2103 let |
2108 let |
2104 val ((induct_thms, induct_thm, induct_attrs), (rec_thmss, rec_attrs)) = |
2109 val ((induct_thms, induct_thm, induct_attrs), (rec_thmss, rec_attrs)) = |
2105 derive_induct_recs_thms_for_types plugins pre_bnfs recs_args_types xtor_co_induct |
2110 derive_induct_recs_thms_for_types plugins pre_bnfs recs_args_types xtor_co_induct |
2154 |>> name_noted_thms |
2159 |>> name_noted_thms |
2155 (fst (dest_Type (hd fpTs)) ^ (implode (map (prefix "_") (tl fp_b_names)))) inductN |
2160 (fst (dest_Type (hd fpTs)) ^ (implode (map (prefix "_") (tl fp_b_names)))) inductN |
2156 |-> interpret_bnfs_register_fp_sugars plugins fpTs fpBTs Xs Least_FP pre_bnfs absT_infos |
2161 |-> interpret_bnfs_register_fp_sugars plugins fpTs fpBTs Xs Least_FP pre_bnfs absT_infos |
2157 fp_nesting_bnfs live_nesting_bnfs fp_res ctrXs_Tsss ctr_defss ctr_sugars recs rec_defs |
2162 fp_nesting_bnfs live_nesting_bnfs fp_res ctrXs_Tsss ctr_defss ctr_sugars recs rec_defs |
2158 map_thmss [induct_thm] (map single induct_thms) rec_thmss (replicate nn []) (replicate nn []) |
2163 map_thmss [induct_thm] (map single induct_thms) rec_thmss (replicate nn []) (replicate nn []) |
2159 rel_injectss rel_distinctss map_disc_iffss map_selss rel_selss rel_intross |
2164 rel_injectss rel_distinctss map_disc_iffss map_selss rel_selss rel_intross rel_casess |
2160 end; |
2165 end; |
2161 |
2166 |
2162 fun derive_corec_transfer_thms lthy corecs corec_defs = |
2167 fun derive_corec_transfer_thms lthy corecs corec_defs = |
2163 let |
2168 let |
2164 val (Rs, Ss, goals, names_lthy) = mk_co_rec_transfer_goals lthy corecs; |
2169 val (Rs, Ss, goals, names_lthy) = mk_co_rec_transfer_goals lthy corecs; |
2174 |> map Thm.close_derivation |
2179 |> map Thm.close_derivation |
2175 end; |
2180 end; |
2176 |
2181 |
2177 fun derive_note_coinduct_corecs_thms_for_types |
2182 fun derive_note_coinduct_corecs_thms_for_types |
2178 ((((map_thmss, map_disc_iffss, map_selss, rel_injectss, rel_distinctss, rel_selss, |
2183 ((((map_thmss, map_disc_iffss, map_selss, rel_injectss, rel_distinctss, rel_selss, |
2179 rel_intross, setss), |
2184 rel_intross, rel_casess, setss), |
2180 (_, _, ctr_defss, ctr_sugars)), |
2185 (_, _, ctr_defss, ctr_sugars)), |
2181 (corecs, corec_defs)), lthy) = |
2186 (corecs, corec_defs)), lthy) = |
2182 let |
2187 let |
2183 val (([(coinduct_thms, coinduct_thm), (coinduct_strong_thms, coinduct_strong_thm)], |
2188 val (([(coinduct_thms, coinduct_thm), (coinduct_strong_thms, coinduct_strong_thm)], |
2184 (coinduct_attrs, common_coinduct_attrs)), |
2189 (coinduct_attrs, common_coinduct_attrs)), |
2270 |-> interpret_bnfs_register_fp_sugars plugins fpTs fpBTs Xs Greatest_FP pre_bnfs absT_infos |
2275 |-> interpret_bnfs_register_fp_sugars plugins fpTs fpBTs Xs Greatest_FP pre_bnfs absT_infos |
2271 fp_nesting_bnfs live_nesting_bnfs fp_res ctrXs_Tsss ctr_defss ctr_sugars corecs corec_defs |
2276 fp_nesting_bnfs live_nesting_bnfs fp_res ctrXs_Tsss ctr_defss ctr_sugars corecs corec_defs |
2272 map_thmss [coinduct_thm, coinduct_strong_thm] |
2277 map_thmss [coinduct_thm, coinduct_strong_thm] |
2273 (transpose [coinduct_thms, coinduct_strong_thms]) corec_thmss corec_disc_thmss |
2278 (transpose [coinduct_thms, coinduct_strong_thms]) corec_thmss corec_disc_thmss |
2274 corec_sel_thmsss rel_injectss rel_distinctss map_disc_iffss map_selss rel_selss |
2279 corec_sel_thmsss rel_injectss rel_distinctss map_disc_iffss map_selss rel_selss |
2275 rel_intross |
2280 rel_intross rel_casess |
2276 end; |
2281 end; |
2277 |
2282 |
2278 val lthy'' = lthy' |
2283 val lthy'' = lthy' |
2279 |> live > 0 ? fold2 (fn Type (s, _) => fn bnf => register_bnf_raw s bnf) fpTs fp_bnfs |
2284 |> live > 0 ? fold2 (fn Type (s, _) => fn bnf => register_bnf_raw s bnf) fpTs fp_bnfs |
2280 |> fold_map define_ctrs_dtrs_for_type (fp_bnfs ~~ fp_bs ~~ fpTs ~~ ctors ~~ dtors ~~ |
2285 |> fold_map define_ctrs_dtrs_for_type (fp_bnfs ~~ fp_bs ~~ fpTs ~~ ctors ~~ dtors ~~ |