20 dtor_ctors: thm list, |
20 dtor_ctors: thm list, |
21 ctor_dtors: thm list, |
21 ctor_dtors: thm list, |
22 ctor_injects: thm list, |
22 ctor_injects: thm list, |
23 dtor_injects: thm list, |
23 dtor_injects: thm list, |
24 xtor_maps: thm list, |
24 xtor_maps: thm list, |
25 xtor_set_thmss: thm list list, |
25 xtor_setss: thm list list, |
26 xtor_rel_thms: thm list, |
26 xtor_rel_thms: thm list, |
27 xtor_co_rec_thms: thm list, |
27 xtor_co_rec_thms: thm list, |
28 xtor_co_rec_o_maps: thm list, |
28 xtor_co_rec_o_maps: thm list, |
29 xtor_rel_co_induct: thm, |
29 xtor_rel_co_induct: thm, |
30 dtor_set_inducts: thm list, |
30 dtor_set_inducts: thm list, |
212 dtor_ctors: thm list, |
212 dtor_ctors: thm list, |
213 ctor_dtors: thm list, |
213 ctor_dtors: thm list, |
214 ctor_injects: thm list, |
214 ctor_injects: thm list, |
215 dtor_injects: thm list, |
215 dtor_injects: thm list, |
216 xtor_maps: thm list, |
216 xtor_maps: thm list, |
217 xtor_set_thmss: thm list list, |
217 xtor_setss: thm list list, |
218 xtor_rel_thms: thm list, |
218 xtor_rel_thms: thm list, |
219 xtor_co_rec_thms: thm list, |
219 xtor_co_rec_thms: thm list, |
220 xtor_co_rec_o_maps: thm list, |
220 xtor_co_rec_o_maps: thm list, |
221 xtor_rel_co_induct: thm, |
221 xtor_rel_co_induct: thm, |
222 dtor_set_inducts: thm list, |
222 dtor_set_inducts: thm list, |
223 xtor_co_rec_transfers: thm list}; |
223 xtor_co_rec_transfers: thm list}; |
224 |
224 |
225 fun morph_fp_result phi {Ts, bnfs, ctors, dtors, xtor_co_recs, xtor_co_induct, |
225 fun morph_fp_result phi {Ts, bnfs, ctors, dtors, xtor_co_recs, xtor_co_induct, |
226 dtor_ctors, ctor_dtors, ctor_injects, dtor_injects, xtor_maps, xtor_set_thmss, |
226 dtor_ctors, ctor_dtors, ctor_injects, dtor_injects, xtor_maps, xtor_setss, |
227 xtor_rel_thms, xtor_co_rec_thms, xtor_co_rec_o_maps, xtor_rel_co_induct, |
227 xtor_rel_thms, xtor_co_rec_thms, xtor_co_rec_o_maps, xtor_rel_co_induct, |
228 dtor_set_inducts, xtor_co_rec_transfers} = |
228 dtor_set_inducts, xtor_co_rec_transfers} = |
229 {Ts = map (Morphism.typ phi) Ts, |
229 {Ts = map (Morphism.typ phi) Ts, |
230 bnfs = map (morph_bnf phi) bnfs, |
230 bnfs = map (morph_bnf phi) bnfs, |
231 ctors = map (Morphism.term phi) ctors, |
231 ctors = map (Morphism.term phi) ctors, |
235 dtor_ctors = map (Morphism.thm phi) dtor_ctors, |
235 dtor_ctors = map (Morphism.thm phi) dtor_ctors, |
236 ctor_dtors = map (Morphism.thm phi) ctor_dtors, |
236 ctor_dtors = map (Morphism.thm phi) ctor_dtors, |
237 ctor_injects = map (Morphism.thm phi) ctor_injects, |
237 ctor_injects = map (Morphism.thm phi) ctor_injects, |
238 dtor_injects = map (Morphism.thm phi) dtor_injects, |
238 dtor_injects = map (Morphism.thm phi) dtor_injects, |
239 xtor_maps = map (Morphism.thm phi) xtor_maps, |
239 xtor_maps = map (Morphism.thm phi) xtor_maps, |
240 xtor_set_thmss = map (map (Morphism.thm phi)) xtor_set_thmss, |
240 xtor_setss = map (map (Morphism.thm phi)) xtor_setss, |
241 xtor_rel_thms = map (Morphism.thm phi) xtor_rel_thms, |
241 xtor_rel_thms = map (Morphism.thm phi) xtor_rel_thms, |
242 xtor_co_rec_thms = map (Morphism.thm phi) xtor_co_rec_thms, |
242 xtor_co_rec_thms = map (Morphism.thm phi) xtor_co_rec_thms, |
243 xtor_co_rec_o_maps = map (Morphism.thm phi) xtor_co_rec_o_maps, |
243 xtor_co_rec_o_maps = map (Morphism.thm phi) xtor_co_rec_o_maps, |
244 xtor_rel_co_induct = Morphism.thm phi xtor_rel_co_induct, |
244 xtor_rel_co_induct = Morphism.thm phi xtor_rel_co_induct, |
245 dtor_set_inducts = map (Morphism.thm phi) dtor_set_inducts, |
245 dtor_set_inducts = map (Morphism.thm phi) dtor_set_inducts, |