23 xtor_map_thms: thm list, |
23 xtor_map_thms: thm list, |
24 xtor_set_thmss: thm list list, |
24 xtor_set_thmss: thm list list, |
25 xtor_rel_thms: thm list, |
25 xtor_rel_thms: thm list, |
26 xtor_co_rec_thms: thm list, |
26 xtor_co_rec_thms: thm list, |
27 xtor_co_rec_o_map_thms: thm list, |
27 xtor_co_rec_o_map_thms: thm list, |
28 rel_xtor_co_induct_thm: thm} |
28 rel_xtor_co_induct_thm: thm, |
|
29 dtor_set_induct_thms: thm list} |
29 |
30 |
30 val morph_fp_result: morphism -> fp_result -> fp_result |
31 val morph_fp_result: morphism -> fp_result -> fp_result |
31 |
32 |
32 type fp_sugar = |
33 type fp_sugar = |
33 {T: typ, |
34 {T: typ, |
235 xtor_map_thms: thm list, |
236 xtor_map_thms: thm list, |
236 xtor_set_thmss: thm list list, |
237 xtor_set_thmss: thm list list, |
237 xtor_rel_thms: thm list, |
238 xtor_rel_thms: thm list, |
238 xtor_co_rec_thms: thm list, |
239 xtor_co_rec_thms: thm list, |
239 xtor_co_rec_o_map_thms: thm list, |
240 xtor_co_rec_o_map_thms: thm list, |
240 rel_xtor_co_induct_thm: thm}; |
241 rel_xtor_co_induct_thm: thm, |
|
242 dtor_set_induct_thms: thm list}; |
241 |
243 |
242 fun morph_fp_result phi {Ts, bnfs, ctors, dtors, xtor_co_recs, xtor_co_induct, |
244 fun morph_fp_result phi {Ts, bnfs, ctors, dtors, xtor_co_recs, xtor_co_induct, |
243 dtor_ctors, ctor_dtors, ctor_injects, dtor_injects, xtor_map_thms, xtor_set_thmss, |
245 dtor_ctors, ctor_dtors, ctor_injects, dtor_injects, xtor_map_thms, xtor_set_thmss, |
244 xtor_rel_thms, xtor_co_rec_thms, xtor_co_rec_o_map_thms, rel_xtor_co_induct_thm} = |
246 xtor_rel_thms, xtor_co_rec_thms, xtor_co_rec_o_map_thms, rel_xtor_co_induct_thm, dtor_set_induct_thms} = |
245 {Ts = map (Morphism.typ phi) Ts, |
247 {Ts = map (Morphism.typ phi) Ts, |
246 bnfs = map (morph_bnf phi) bnfs, |
248 bnfs = map (morph_bnf phi) bnfs, |
247 ctors = map (Morphism.term phi) ctors, |
249 ctors = map (Morphism.term phi) ctors, |
248 dtors = map (Morphism.term phi) dtors, |
250 dtors = map (Morphism.term phi) dtors, |
249 xtor_co_recs = map (Morphism.term phi) xtor_co_recs, |
251 xtor_co_recs = map (Morphism.term phi) xtor_co_recs, |
255 xtor_map_thms = map (Morphism.thm phi) xtor_map_thms, |
257 xtor_map_thms = map (Morphism.thm phi) xtor_map_thms, |
256 xtor_set_thmss = map (map (Morphism.thm phi)) xtor_set_thmss, |
258 xtor_set_thmss = map (map (Morphism.thm phi)) xtor_set_thmss, |
257 xtor_rel_thms = map (Morphism.thm phi) xtor_rel_thms, |
259 xtor_rel_thms = map (Morphism.thm phi) xtor_rel_thms, |
258 xtor_co_rec_thms = map (Morphism.thm phi) xtor_co_rec_thms, |
260 xtor_co_rec_thms = map (Morphism.thm phi) xtor_co_rec_thms, |
259 xtor_co_rec_o_map_thms = map (Morphism.thm phi) xtor_co_rec_o_map_thms, |
261 xtor_co_rec_o_map_thms = map (Morphism.thm phi) xtor_co_rec_o_map_thms, |
260 rel_xtor_co_induct_thm = Morphism.thm phi rel_xtor_co_induct_thm}; |
262 rel_xtor_co_induct_thm = Morphism.thm phi rel_xtor_co_induct_thm, |
|
263 dtor_set_induct_thms = map (Morphism.thm phi) dtor_set_induct_thms}; (* No idea of what this is doing... *) |
261 |
264 |
262 type fp_sugar = |
265 type fp_sugar = |
263 {T: typ, |
266 {T: typ, |
264 BT: typ, |
267 BT: typ, |
265 X: typ, |
268 X: typ, |