176 map_sels: thm list, |
177 map_sels: thm list, |
177 rel_injects: thm list, |
178 rel_injects: thm list, |
178 rel_distincts: thm list, |
179 rel_distincts: thm list, |
179 rel_sels: thm list, |
180 rel_sels: thm list, |
180 rel_intros: thm list, |
181 rel_intros: thm list, |
181 rel_cases: thm list}; |
182 rel_cases: thm list, |
|
183 set_thms: thm list}; |
182 |
184 |
183 type fp_co_induct_sugar = |
185 type fp_co_induct_sugar = |
184 {co_rec: term, |
186 {co_rec: term, |
185 common_co_inducts: thm list, |
187 common_co_inducts: thm list, |
186 co_inducts: thm list, |
188 co_inducts: thm list, |
203 fp_ctr_sugar: fp_ctr_sugar, |
205 fp_ctr_sugar: fp_ctr_sugar, |
204 fp_bnf_sugar: fp_bnf_sugar, |
206 fp_bnf_sugar: fp_bnf_sugar, |
205 fp_co_induct_sugar: fp_co_induct_sugar}; |
207 fp_co_induct_sugar: fp_co_induct_sugar}; |
206 |
208 |
207 fun morph_fp_bnf_sugar phi ({map_thms, map_disc_iffs, map_sels, rel_injects, rel_distincts, |
209 fun morph_fp_bnf_sugar phi ({map_thms, map_disc_iffs, map_sels, rel_injects, rel_distincts, |
208 rel_sels, rel_intros, rel_cases} : fp_bnf_sugar) = |
210 rel_sels, rel_intros, rel_cases, set_thms} : fp_bnf_sugar) = |
209 {map_thms = map (Morphism.thm phi) map_thms, |
211 {map_thms = map (Morphism.thm phi) map_thms, |
210 map_disc_iffs = map (Morphism.thm phi) map_disc_iffs, |
212 map_disc_iffs = map (Morphism.thm phi) map_disc_iffs, |
211 map_sels = map (Morphism.thm phi) map_sels, |
213 map_sels = map (Morphism.thm phi) map_sels, |
212 rel_injects = map (Morphism.thm phi) rel_injects, |
214 rel_injects = map (Morphism.thm phi) rel_injects, |
213 rel_distincts = map (Morphism.thm phi) rel_distincts, |
215 rel_distincts = map (Morphism.thm phi) rel_distincts, |
214 rel_sels = map (Morphism.thm phi) rel_sels, |
216 rel_sels = map (Morphism.thm phi) rel_sels, |
215 rel_intros = map (Morphism.thm phi) rel_intros, |
217 rel_intros = map (Morphism.thm phi) rel_intros, |
216 rel_cases = map (Morphism.thm phi) rel_cases}; |
218 rel_cases = map (Morphism.thm phi) rel_cases, |
|
219 set_thms = map (Morphism.thm phi) set_thms}; |
217 |
220 |
218 fun morph_fp_co_induct_sugar phi ({co_rec, common_co_inducts, co_inducts, co_rec_def, co_rec_thms, |
221 fun morph_fp_co_induct_sugar phi ({co_rec, common_co_inducts, co_inducts, co_rec_def, co_rec_thms, |
219 co_rec_discs, co_rec_selss} : fp_co_induct_sugar) = |
222 co_rec_discs, co_rec_selss} : fp_co_induct_sugar) = |
220 {co_rec = Morphism.term phi co_rec, |
223 {co_rec = Morphism.term phi co_rec, |
221 common_co_inducts = map (Morphism.thm phi) common_co_inducts, |
224 common_co_inducts = map (Morphism.thm phi) common_co_inducts, |
295 register_fp_sugars_raw fp_sugars #> interpret_fp_sugars plugins fp_sugars; |
298 register_fp_sugars_raw fp_sugars #> interpret_fp_sugars plugins fp_sugars; |
296 |
299 |
297 fun interpret_bnfs_register_fp_sugars plugins Ts BTs Xs fp pre_bnfs absT_infos fp_nesting_bnfs |
300 fun interpret_bnfs_register_fp_sugars plugins Ts BTs Xs fp pre_bnfs absT_infos fp_nesting_bnfs |
298 live_nesting_bnfs fp_res ctrXs_Tsss ctr_defss ctr_sugars co_recs co_rec_defs map_thmss |
301 live_nesting_bnfs fp_res ctrXs_Tsss ctr_defss ctr_sugars co_recs co_rec_defs map_thmss |
299 common_co_inducts co_inductss co_rec_thmss co_rec_discss co_rec_selsss rel_injectss |
302 common_co_inducts co_inductss co_rec_thmss co_rec_discss co_rec_selsss rel_injectss |
300 rel_distinctss map_disc_iffss map_selss rel_selss rel_intross rel_casess noted = |
303 rel_distinctss map_disc_iffss map_selss rel_selss rel_intross rel_casess set_thmss noted = |
301 let |
304 let |
302 val fp_sugars = |
305 val fp_sugars = |
303 map_index (fn (kk, T) => |
306 map_index (fn (kk, T) => |
304 {T = T, BT = nth BTs kk, X = nth Xs kk, fp = fp, fp_res = fp_res, fp_res_index = kk, |
307 {T = T, BT = nth BTs kk, X = nth Xs kk, fp = fp, fp_res = fp_res, fp_res_index = kk, |
305 pre_bnf = nth pre_bnfs kk, absT_info = nth absT_infos kk, |
308 pre_bnf = nth pre_bnfs kk, absT_info = nth absT_infos kk, |
314 map_sels = nth map_selss kk, |
317 map_sels = nth map_selss kk, |
315 rel_injects = nth rel_injectss kk, |
318 rel_injects = nth rel_injectss kk, |
316 rel_distincts = nth rel_distinctss kk, |
319 rel_distincts = nth rel_distinctss kk, |
317 rel_sels = nth rel_selss kk, |
320 rel_sels = nth rel_selss kk, |
318 rel_intros = nth rel_intross kk, |
321 rel_intros = nth rel_intross kk, |
319 rel_cases = nth rel_casess kk}, |
322 rel_cases = nth rel_casess kk, |
|
323 set_thms = nth set_thmss kk}, |
320 fp_co_induct_sugar = |
324 fp_co_induct_sugar = |
321 {co_rec = nth co_recs kk, |
325 {co_rec = nth co_recs kk, |
322 common_co_inducts = common_co_inducts, |
326 common_co_inducts = common_co_inducts, |
323 co_inducts = nth co_inductss kk, |
327 co_inducts = nth co_inductss kk, |
324 co_rec_def = nth co_rec_defs kk, |
328 co_rec_def = nth co_rec_defs kk, |
962 map subst rel_inject_thms, |
966 map subst rel_inject_thms, |
963 map subst rel_distinct_thms, |
967 map subst rel_distinct_thms, |
964 map subst rel_sel_thms, |
968 map subst rel_sel_thms, |
965 map subst rel_intro_thms, |
969 map subst rel_intro_thms, |
966 [subst rel_cases_thm], |
970 [subst rel_cases_thm], |
967 map (map subst) set0_thmss), lthy') |
971 map subst set_thms), lthy') |
968 end; |
972 end; |
969 |
973 |
970 type lfp_sugar_thms = (thm list * thm * Token.src list) * (thm list list * Token.src list); |
974 type lfp_sugar_thms = (thm list * thm * Token.src list) * (thm list list * Token.src list); |
971 |
975 |
972 fun morph_lfp_sugar_thms phi ((inducts, induct, induct_attrs), (recss, rec_attrs)) = |
976 fun morph_lfp_sugar_thms phi ((inducts, induct, induct_attrs), (recss, rec_attrs)) = |
2070 fold_map I wrap_one_etc lthy |
2074 fold_map I wrap_one_etc lthy |
2071 |>> apsnd split_list o apfst (apsnd split_list4 o apfst split_list9 o split_list) |
2075 |>> apsnd split_list o apfst (apsnd split_list4 o apfst split_list9 o split_list) |
2072 o split_list; |
2076 o split_list; |
2073 |
2077 |
2074 fun mk_simp_thms ({injects, distincts, case_thms, ...} : ctr_sugar) co_recs map_thms rel_injects |
2078 fun mk_simp_thms ({injects, distincts, case_thms, ...} : ctr_sugar) co_recs map_thms rel_injects |
2075 rel_distincts setss = |
2079 rel_distincts set_thmss = |
2076 injects @ distincts @ case_thms @ co_recs @ map_thms @ rel_injects @ rel_distincts @ flat setss; |
2080 injects @ distincts @ case_thms @ co_recs @ map_thms @ rel_injects @ rel_distincts @ |
|
2081 set_thmss; |
2077 |
2082 |
2078 fun mk_co_rec_transfer_goals lthy co_recs = |
2083 fun mk_co_rec_transfer_goals lthy co_recs = |
2079 let |
2084 let |
2080 val liveAsBs = filter (op <>) (As ~~ Bs); |
2085 val liveAsBs = filter (op <>) (As ~~ Bs); |
2081 val B_ify = Term.subst_atomic_types (liveAsBs @ (Cs ~~ Es)); |
2086 val B_ify = Term.subst_atomic_types (liveAsBs @ (Cs ~~ Es)); |
2100 |> map Thm.close_derivation |
2105 |> map Thm.close_derivation |
2101 end; |
2106 end; |
2102 |
2107 |
2103 fun derive_note_induct_recs_thms_for_types |
2108 fun derive_note_induct_recs_thms_for_types |
2104 ((((map_thmss, map_disc_iffss, map_selss, rel_injectss, rel_distinctss, rel_selss, |
2109 ((((map_thmss, map_disc_iffss, map_selss, rel_injectss, rel_distinctss, rel_selss, |
2105 rel_intross, rel_casess, setss), |
2110 rel_intross, rel_casess, set_thmss), |
2106 (ctrss, _, ctr_defss, ctr_sugars)), |
2111 (ctrss, _, ctr_defss, ctr_sugars)), |
2107 (recs, rec_defs)), lthy) = |
2112 (recs, rec_defs)), lthy) = |
2108 let |
2113 let |
2109 val ((induct_thms, induct_thm, induct_attrs), (rec_thmss, rec_attrs)) = |
2114 val ((induct_thms, induct_thm, induct_attrs), (rec_thmss, rec_attrs)) = |
2110 derive_induct_recs_thms_for_types plugins pre_bnfs recs_args_types xtor_co_induct |
2115 derive_induct_recs_thms_for_types plugins pre_bnfs recs_args_types xtor_co_induct |
2132 ((map single rel_induct_thms, single common_rel_induct_thm), |
2137 ((map single rel_induct_thms, single common_rel_induct_thm), |
2133 (rel_induct_attrs, rel_induct_attrs)) |
2138 (rel_induct_attrs, rel_induct_attrs)) |
2134 end; |
2139 end; |
2135 |
2140 |
2136 val simp_thmss = |
2141 val simp_thmss = |
2137 map6 mk_simp_thms ctr_sugars rec_thmss map_thmss rel_injectss rel_distinctss setss; |
2142 map6 mk_simp_thms ctr_sugars rec_thmss map_thmss rel_injectss rel_distinctss set_thmss; |
2138 |
2143 |
2139 val common_notes = |
2144 val common_notes = |
2140 (if nn > 1 then |
2145 (if nn > 1 then |
2141 [(inductN, [induct_thm], K induct_attrs), |
2146 [(inductN, [induct_thm], K induct_attrs), |
2142 (rel_inductN, common_rel_induct_thms, K common_rel_induct_attrs)] |
2147 (rel_inductN, common_rel_induct_thms, K common_rel_induct_attrs)] |
2158 (* for "datatype_realizer.ML": *) |
2163 (* for "datatype_realizer.ML": *) |
2159 |>> name_noted_thms |
2164 |>> name_noted_thms |
2160 (fst (dest_Type (hd fpTs)) ^ (implode (map (prefix "_") (tl fp_b_names)))) inductN |
2165 (fst (dest_Type (hd fpTs)) ^ (implode (map (prefix "_") (tl fp_b_names)))) inductN |
2161 |-> interpret_bnfs_register_fp_sugars plugins fpTs fpBTs Xs Least_FP pre_bnfs absT_infos |
2166 |-> interpret_bnfs_register_fp_sugars plugins fpTs fpBTs Xs Least_FP pre_bnfs absT_infos |
2162 fp_nesting_bnfs live_nesting_bnfs fp_res ctrXs_Tsss ctr_defss ctr_sugars recs rec_defs |
2167 fp_nesting_bnfs live_nesting_bnfs fp_res ctrXs_Tsss ctr_defss ctr_sugars recs rec_defs |
2163 map_thmss [induct_thm] (map single induct_thms) rec_thmss (replicate nn []) (replicate nn []) |
2168 map_thmss [induct_thm] (map single induct_thms) rec_thmss (replicate nn []) |
2164 rel_injectss rel_distinctss map_disc_iffss map_selss rel_selss rel_intross rel_casess |
2169 (replicate nn []) rel_injectss rel_distinctss map_disc_iffss map_selss rel_selss |
|
2170 rel_intross rel_casess set_thmss |
2165 end; |
2171 end; |
2166 |
2172 |
2167 fun derive_corec_transfer_thms lthy corecs corec_defs = |
2173 fun derive_corec_transfer_thms lthy corecs corec_defs = |
2168 let |
2174 let |
2169 val (Rs, Ss, goals, names_lthy) = mk_co_rec_transfer_goals lthy corecs; |
2175 val (Rs, Ss, goals, names_lthy) = mk_co_rec_transfer_goals lthy corecs; |
2179 |> map Thm.close_derivation |
2185 |> map Thm.close_derivation |
2180 end; |
2186 end; |
2181 |
2187 |
2182 fun derive_note_coinduct_corecs_thms_for_types |
2188 fun derive_note_coinduct_corecs_thms_for_types |
2183 ((((map_thmss, map_disc_iffss, map_selss, rel_injectss, rel_distinctss, rel_selss, |
2189 ((((map_thmss, map_disc_iffss, map_selss, rel_injectss, rel_distinctss, rel_selss, |
2184 rel_intross, rel_casess, setss), |
2190 rel_intross, rel_casess, set_thmss), |
2185 (_, _, ctr_defss, ctr_sugars)), |
2191 (_, _, ctr_defss, ctr_sugars)), |
2186 (corecs, corec_defs)), lthy) = |
2192 (corecs, corec_defs)), lthy) = |
2187 let |
2193 let |
2188 val (([(coinduct_thms, coinduct_thm), (coinduct_strong_thms, coinduct_strong_thm)], |
2194 val (([(coinduct_thms, coinduct_thm), (coinduct_strong_thms, coinduct_strong_thm)], |
2189 (coinduct_attrs, common_coinduct_attrs)), |
2195 (coinduct_attrs, common_coinduct_attrs)), |
2241 |> split_list; |
2247 |> split_list; |
2242 |
2248 |
2243 val simp_thmss = |
2249 val simp_thmss = |
2244 map6 mk_simp_thms ctr_sugars |
2250 map6 mk_simp_thms ctr_sugars |
2245 (map3 flat_corec_thms corec_disc_thmss corec_disc_iff_thmss corec_sel_thmss) |
2251 (map3 flat_corec_thms corec_disc_thmss corec_disc_iff_thmss corec_sel_thmss) |
2246 map_thmss rel_injectss rel_distinctss setss; |
2252 map_thmss rel_injectss rel_distinctss set_thmss; |
2247 |
2253 |
2248 val common_notes = |
2254 val common_notes = |
2249 (set_inductN, set_induct_thms, nth set_induct_attrss) :: |
2255 (set_inductN, set_induct_thms, nth set_induct_attrss) :: |
2250 (if nn > 1 then |
2256 (if nn > 1 then |
2251 [(coinductN, [coinduct_thm], K common_coinduct_attrs), |
2257 [(coinductN, [coinduct_thm], K common_coinduct_attrs), |
2275 |-> interpret_bnfs_register_fp_sugars plugins fpTs fpBTs Xs Greatest_FP pre_bnfs absT_infos |
2281 |-> interpret_bnfs_register_fp_sugars plugins fpTs fpBTs Xs Greatest_FP pre_bnfs absT_infos |
2276 fp_nesting_bnfs live_nesting_bnfs fp_res ctrXs_Tsss ctr_defss ctr_sugars corecs corec_defs |
2282 fp_nesting_bnfs live_nesting_bnfs fp_res ctrXs_Tsss ctr_defss ctr_sugars corecs corec_defs |
2277 map_thmss [coinduct_thm, coinduct_strong_thm] |
2283 map_thmss [coinduct_thm, coinduct_strong_thm] |
2278 (transpose [coinduct_thms, coinduct_strong_thms]) corec_thmss corec_disc_thmss |
2284 (transpose [coinduct_thms, coinduct_strong_thms]) corec_thmss corec_disc_thmss |
2279 corec_sel_thmsss rel_injectss rel_distinctss map_disc_iffss map_selss rel_selss |
2285 corec_sel_thmsss rel_injectss rel_distinctss map_disc_iffss map_selss rel_selss |
2280 rel_intross rel_casess |
2286 rel_intross rel_casess set_thmss |
2281 end; |
2287 end; |
2282 |
2288 |
2283 val lthy'' = lthy' |
2289 val lthy'' = lthy' |
2284 |> live > 0 ? fold2 (fn Type (s, _) => fn bnf => register_bnf_raw s bnf) fpTs fp_bnfs |
2290 |> live > 0 ? fold2 (fn Type (s, _) => fn bnf => register_bnf_raw s bnf) fpTs fp_bnfs |
2285 |> fold_map define_ctrs_dtrs_for_type (fp_bnfs ~~ fp_bs ~~ fpTs ~~ ctors ~~ dtors ~~ |
2291 |> fold_map define_ctrs_dtrs_for_type (fp_bnfs ~~ fp_bs ~~ fpTs ~~ ctors ~~ dtors ~~ |