247 map2 (fn C => map (map (map (curry (op -->) C) o maybe_unzipT))) Cs f_Tsss; |
245 map2 (fn C => map (map (map (curry (op -->) C) o maybe_unzipT))) Cs f_Tsss; |
248 val q_Tssss = |
246 val q_Tssss = |
249 map (map (map (fn [_] => [] | [_, C] => [mk_pred1T (domain_type C)]))) f_Tssss; |
247 map (map (map (fn [_] => [] | [_, C] => [mk_pred1T (domain_type C)]))) f_Tssss; |
250 val pf_Tss = map3 flat_preds_predsss_gettersss p_Tss q_Tssss f_Tssss; |
248 val pf_Tss = map3 flat_preds_predsss_gettersss p_Tss q_Tssss f_Tssss; |
251 in (q_Tssss, f_sum_prod_Ts, f_Tsss, f_Tssss, pf_Tss) end; |
249 in (q_Tssss, f_sum_prod_Ts, f_Tsss, f_Tssss, pf_Tss) end; |
252 in |
250 |
253 (p_Tss, mk_types single dtor_unfold_fun_Ts, mk_types unzip_corecT dtor_corec_fun_Ts) |
251 val (r_Tssss, g_sum_prod_Ts, g_Tsss, g_Tssss, pg_Tss) = mk_types single dtor_unfold_fun_Ts; |
254 end |
252 val (s_Tssss, h_sum_prod_Ts, h_Tsss, h_Tssss, ph_Tss) = mk_types unzip_corecT dtor_corec_fun_Ts; |
255 |
253 |
256 fun mk_unfold_corec_vars Cs p_Tss g_Tssss r_Tssss h_Tssss s_Tssss lthy = |
|
257 let |
|
258 val (((cs, pss), gssss), lthy) = |
254 val (((cs, pss), gssss), lthy) = |
259 lthy |
255 lthy |
260 |> mk_Frees "a" Cs |
256 |> mk_Frees "a" Cs |
261 ||>> mk_Freess "p" p_Tss |
257 ||>> mk_Freess "p" p_Tss |
262 ||>> mk_Freessss "g" g_Tssss; |
258 ||>> mk_Freessss "g" g_Tssss; |
266 val ((sssss, hssss_tl), lthy) = |
262 val ((sssss, hssss_tl), lthy) = |
267 lthy |
263 lthy |
268 |> mk_Freessss "q" s_Tssss |
264 |> mk_Freessss "q" s_Tssss |
269 ||>> mk_Freessss "h" (map (map (map tl)) h_Tssss); |
265 ||>> mk_Freessss "h" (map (map (map tl)) h_Tssss); |
270 val hssss = map2 (map2 (map2 cons)) hssss_hd hssss_tl; |
266 val hssss = map2 (map2 (map2 cons)) hssss_hd hssss_tl; |
|
267 |
|
268 val cpss = map2 (map o rapp) cs pss; |
|
269 |
|
270 fun mk_terms qssss fssss = |
|
271 let |
|
272 val pfss = map3 flat_preds_predsss_gettersss pss qssss fssss; |
|
273 val cqssss = map2 (map o map o map o rapp) cs qssss; |
|
274 val cfssss = map2 (map o map o map o rapp) cs fssss; |
|
275 in (pfss, cqssss, cfssss) end; |
|
276 |
|
277 val unfold_terms = mk_terms rssss gssss; |
|
278 val corec_terms = mk_terms sssss hssss; |
271 in |
279 in |
272 ((cs, pss, (gssss, rssss), (hssss, sssss)), lthy) |
280 ((cs, cpss, (unfold_terms, (g_sum_prod_Ts, g_Tsss, pg_Tss)), |
|
281 (corec_terms, (h_sum_prod_Ts, h_Tsss, ph_Tss))), lthy) |
273 end; |
282 end; |
274 |
|
275 fun mk_corec_like_terms cs pss qssss fssss = |
|
276 let |
|
277 val pfss = map3 flat_preds_predsss_gettersss pss qssss fssss; |
|
278 val cqssss = map2 (map o map o map o rapp) cs qssss; |
|
279 val cfssss = map2 (map o map o map o rapp) cs fssss; |
|
280 in (pfss, cqssss, cfssss) end; |
|
281 |
283 |
282 fun mk_map live Ts Us t = |
284 fun mk_map live Ts Us t = |
283 let val (Type (_, Ts0), Type (_, Us0)) = strip_typeN (live + 1) (fastype_of t) |>> List.last in |
285 let val (Type (_, Ts0), Type (_, Us0)) = strip_typeN (live + 1) (fastype_of t) |>> List.last in |
284 Term.subst_atomic_types (Ts0 @ Us0 ~~ Ts @ Us) t |
286 Term.subst_atomic_types (Ts0 @ Us0 ~~ Ts @ Us) t |
285 end; |
287 end; |
530 val exhausts = map #exhaust ctr_wrap_ress; |
532 val exhausts = map #exhaust ctr_wrap_ress; |
531 val disc_thmsss = map #disc_thmss ctr_wrap_ress; |
533 val disc_thmsss = map #disc_thmss ctr_wrap_ress; |
532 val discIss = map #discIs ctr_wrap_ress; |
534 val discIss = map #discIs ctr_wrap_ress; |
533 val sel_thmsss = map #sel_thmss ctr_wrap_ress; |
535 val sel_thmsss = map #sel_thmss ctr_wrap_ress; |
534 |
536 |
|
537 val ((cs, cpss, ((pgss, crssss, cgssss), _), ((phss, csssss, chssss), _)), names_lthy0) = |
|
538 mk_unfold_corec_terms_and_types fpTs Cs ns mss dtor_unfold_fun_Ts dtor_corec_fun_Ts lthy; |
|
539 |
535 val (((rs, us'), vs'), names_lthy) = |
540 val (((rs, us'), vs'), names_lthy) = |
536 lthy |
541 names_lthy0 |
537 |> mk_Frees "R" (map (fn T => mk_pred2T T T) fpTs) |
542 |> mk_Frees "R" (map (fn T => mk_pred2T T T) fpTs) |
538 ||>> Variable.variant_fixes fp_b_names |
543 ||>> Variable.variant_fixes fp_b_names |
539 ||>> Variable.variant_fixes (map (suffix "'") fp_b_names); |
544 ||>> Variable.variant_fixes (map (suffix "'") fp_b_names); |
540 |
545 |
541 val (p_Tss, (r_Tssss, _, _, g_Tssss, _), (s_Tssss, _, _, h_Tssss, _)) = |
|
542 mk_unfold_corec_types fpTs Cs ns mss dtor_unfold_fun_Ts dtor_corec_fun_Ts; |
|
543 |
|
544 val ((cs, pss, (gssss, rssss), (hssss, sssss)), names_lthy) = |
|
545 mk_unfold_corec_vars Cs p_Tss g_Tssss r_Tssss h_Tssss s_Tssss names_lthy; |
|
546 |
|
547 val cpss = map2 (map o rapp) cs pss; |
|
548 |
|
549 val us = map2 (curry Free) us' fpTs; |
546 val us = map2 (curry Free) us' fpTs; |
550 val udiscss = map2 (map o rapp) us discss; |
547 val udiscss = map2 (map o rapp) us discss; |
551 val uselsss = map2 (map o map o rapp) us selsss; |
548 val uselsss = map2 (map o map o rapp) us selsss; |
552 |
549 |
553 val vs = map2 (curry Free) vs' fpTs; |
550 val vs = map2 (curry Free) vs' fpTs; |
554 val vdiscss = map2 (map o rapp) vs discss; |
551 val vdiscss = map2 (map o rapp) vs discss; |
555 val vselsss = map2 (map o map o rapp) vs selsss; |
552 val vselsss = map2 (map o map o rapp) vs selsss; |
556 |
|
557 val (pgss, crssss, cgssss) = mk_corec_like_terms cs pss rssss gssss; |
|
558 val (phss, csssss, chssss) = mk_corec_like_terms cs pss sssss hssss; |
|
559 |
553 |
560 val ((coinduct_thms, coinduct_thm), (strong_coinduct_thms, strong_coinduct_thm)) = |
554 val ((coinduct_thms, coinduct_thm), (strong_coinduct_thms, strong_coinduct_thm)) = |
561 let |
555 let |
562 val uvrs = map3 (fn r => fn u => fn v => r $ u $ v) rs us vs; |
556 val uvrs = map3 (fn r => fn u => fn v => r $ u $ v) rs us vs; |
563 val uv_eqs = map2 (curry HOLogic.mk_eq) us vs; |
557 val uv_eqs = map2 (curry HOLogic.mk_eq) us vs; |
970 in |
964 in |
971 ((((gss, g_Tss, ysss), (hss, h_Tss, zsss)), |
965 ((((gss, g_Tss, ysss), (hss, h_Tss, zsss)), |
972 ([], [], (([], [], []), ([], [], [])), (([], [], []), ([], [], [])))), lthy) |
966 ([], [], (([], [], []), ([], [], [])), (([], [], []), ([], [], [])))), lthy) |
973 end |
967 end |
974 else |
968 else |
975 let |
969 mk_unfold_corec_terms_and_types fpTs Cs ns mss fp_fold_fun_Ts fp_rec_fun_Ts lthy |
976 val (p_Tss, (r_Tssss, g_sum_prod_Ts, g_Tsss, g_Tssss, pg_Tss), |
970 |>> pair (([], [], []), ([], [], [])); |
977 (s_Tssss, h_sum_prod_Ts, h_Tsss, h_Tssss, ph_Tss)) = |
|
978 mk_unfold_corec_types fpTs Cs ns mss fp_fold_fun_Ts fp_rec_fun_Ts; |
|
979 |
|
980 val ((cs, pss, (gssss, rssss), (hssss, sssss)), lthy) = |
|
981 mk_unfold_corec_vars Cs p_Tss g_Tssss r_Tssss h_Tssss s_Tssss lthy; |
|
982 |
|
983 val cpss = map2 (map o rapp) cs pss; |
|
984 in |
|
985 (((([], [], []), ([], [], [])), |
|
986 (cs, cpss, (mk_corec_like_terms cs pss rssss gssss, (g_sum_prod_Ts, g_Tsss, pg_Tss)), |
|
987 (mk_corec_like_terms cs pss sssss hssss, (h_sum_prod_Ts, h_Tsss, ph_Tss)))), lthy) |
|
988 end; |
|
989 |
971 |
990 fun define_ctrs_case_for_type (((((((((((((((((((((((((fp_bnf, fp_b), fpT), C), ctor), dtor), |
972 fun define_ctrs_case_for_type (((((((((((((((((((((((((fp_bnf, fp_b), fpT), C), ctor), dtor), |
991 fp_fold), fp_rec), ctor_dtor), dtor_ctor), ctor_inject), pre_map_def), pre_set_defs), |
973 fp_fold), fp_rec), ctor_dtor), dtor_ctor), ctor_inject), pre_map_def), pre_set_defs), |
992 pre_rel_def), fp_map_thm), fp_set_thms), fp_rel_thm), n), ks), ms), ctr_bindings), |
974 pre_rel_def), fp_map_thm), fp_set_thms), fp_rel_thm), n), ks), ms), ctr_bindings), |
993 ctr_mixfixes), ctr_Tss), disc_bindings), sel_bindingss), raw_sel_defaultss) no_defs_lthy = |
975 ctr_mixfixes), ctr_Tss), disc_bindings), sel_bindingss), raw_sel_defaultss) no_defs_lthy = |