226 val rho = tvar_subst thy (fpTs0 @ Cs0) (fpTs @ Cs); |
226 val rho = tvar_subst thy (fpTs0 @ Cs0) (fpTs @ Cs); |
227 in |
227 in |
228 map (Term.subst_TVars rho) ts0 |
228 map (Term.subst_TVars rho) ts0 |
229 end; |
229 end; |
230 |
230 |
|
231 fun mk_set Ts t = |
|
232 subst_nonatomic_types (snd (Term.dest_Type (domain_type (fastype_of t))) ~~ Ts) t; |
|
233 |
231 fun unzip_recT (Type (@{type_name prod}, _)) T = [T] |
234 fun unzip_recT (Type (@{type_name prod}, _)) T = [T] |
232 | unzip_recT _ (Type (@{type_name prod}, Ts)) = Ts |
235 | unzip_recT _ (Type (@{type_name prod}, Ts)) = Ts |
233 | unzip_recT _ T = [T]; |
236 | unzip_recT _ T = [T]; |
234 |
237 |
235 fun unzip_corecT (Type (@{type_name sum}, _)) T = [T] |
238 fun unzip_corecT (Type (@{type_name sum}, _)) T = [T] |
526 ||>> mk_Freesss "x" ctr_Tsss |
529 ||>> mk_Freesss "x" ctr_Tsss |
527 ||>> Variable.variant_fixes fp_b_names; |
530 ||>> Variable.variant_fixes fp_b_names; |
528 |
531 |
529 val us = map2 (curry Free) us' fpTs; |
532 val us = map2 (curry Free) us' fpTs; |
530 |
533 |
531 fun mk_sets_nested bnf = |
534 fun mk_sets bnf = |
532 let |
535 let |
533 val Type (T_name, Us) = T_of_bnf bnf; |
536 val Type (T_name, Us) = T_of_bnf bnf; |
534 val lives = lives_of_bnf bnf; |
537 val lives = lives_of_bnf bnf; |
535 val sets = sets_of_bnf bnf; |
538 val sets = sets_of_bnf bnf; |
536 fun mk_set U = |
539 fun mk_set U = |
539 | i => nth sets i); |
542 | i => nth sets i); |
540 in |
543 in |
541 (T_name, map mk_set Us) |
544 (T_name, map mk_set Us) |
542 end; |
545 end; |
543 |
546 |
544 val setss_nested = map mk_sets_nested fp_nesting_bnfs; |
547 val setss_fp_nesting = map mk_sets fp_nesting_bnfs; |
545 |
548 |
546 val (induct_thms, induct_thm) = |
549 val (induct_thms, induct_thm) = |
547 let |
550 let |
548 fun mk_set Ts t = |
|
549 let val Type (_, Ts0) = domain_type (fastype_of t) in |
|
550 Term.subst_atomic_types (Ts0 ~~ Ts) t |
|
551 end; |
|
552 |
|
553 fun mk_raw_prem_prems _ (x as Free (_, Type _)) (X as TFree _) = |
551 fun mk_raw_prem_prems _ (x as Free (_, Type _)) (X as TFree _) = |
554 [([], (find_index (curry (op =) X) Xs + 1, x))] |
552 [([], (find_index (curry (op =) X) Xs + 1, x))] |
555 | mk_raw_prem_prems names_lthy (x as Free (s, Type (T_name, Ts0))) (Type (_, Xs_Ts0)) = |
553 | mk_raw_prem_prems names_lthy (x as Free (s, Type (T_name, Ts0))) (Type (_, Xs_Ts0)) = |
556 (case AList.lookup (op =) setss_nested T_name of |
554 (case AList.lookup (op =) setss_fp_nesting T_name of |
557 NONE => [] |
555 NONE => [] |
558 | SOME raw_sets0 => |
556 | SOME raw_sets0 => |
559 let |
557 let |
560 val (Xs_Ts, (Ts, raw_sets)) = |
558 val (Xs_Ts, (Ts, raw_sets)) = |
561 filter (exists_subtype_in Xs o fst) (Xs_Ts0 ~~ (Ts0 ~~ raw_sets0)) |
559 filter (exists_subtype_in Xs o fst) (Xs_Ts0 ~~ (Ts0 ~~ raw_sets0)) |
1296 |
1294 |
1297 val map_thms = map2 mk_map_thm ctr_defs' cxIns; |
1295 val map_thms = map2 mk_map_thm ctr_defs' cxIns; |
1298 val set_thmss = map mk_set_thms fp_set_thms; |
1296 val set_thmss = map mk_set_thms fp_set_thms; |
1299 val set_thms = flat set_thmss; |
1297 val set_thms = flat set_thmss; |
1300 |
1298 |
1301 fun mk_set Ts t = |
|
1302 subst_nonatomic_types (snd (Term.dest_Type (domain_type (fastype_of t))) ~~ Ts) t; |
|
1303 |
|
1304 val sets = map (mk_set (snd (Term.dest_Type fpT))) (sets_of_bnf fp_bnf); |
1299 val sets = map (mk_set (snd (Term.dest_Type fpT))) (sets_of_bnf fp_bnf); |
1305 |
1300 |
1306 val set_empty_thms = |
1301 val set_empty_thms = |
1307 let |
1302 let |
1308 val ctr_argT_namess = map ((fn Ts => fold Term.add_tfree_namesT Ts []) o |
1303 val ctr_argT_namess = map ((fn Ts => fold Term.add_tfree_namesT Ts []) o |