43 |
43 |
44 val mk_iter_fun_arg_types_pairsss: typ list -> int list -> int list list -> term -> |
44 val mk_iter_fun_arg_types_pairsss: typ list -> int list -> int list list -> term -> |
45 (typ list * typ list) list list list |
45 (typ list * typ list) list list list |
46 val define_fold_rec: (term list list * typ list list * term list list list) |
46 val define_fold_rec: (term list list * typ list list * term list list list) |
47 * (term list list * typ list list * term list list list) -> (string -> binding) -> typ list -> |
47 * (term list list * typ list list * term list list list) -> (string -> binding) -> typ list -> |
48 typ list -> typ list -> term -> term -> Proof.context -> |
48 typ list -> term -> term -> Proof.context -> (term * term * thm * thm) * Proof.context |
49 (term * term * thm * thm) * Proof.context |
|
50 val define_unfold_corec: term list * term list list |
49 val define_unfold_corec: term list * term list list |
51 * ((term list list * term list list list list * term list list list list) |
50 * ((term list list * term list list list list * term list list list list) |
52 * (typ list * typ list list list * typ list list)) |
51 * (typ list * typ list list list * typ list list)) |
53 * ((term list list * term list list list list * term list list list list) |
52 * ((term list list * term list list list list * term list list list list) |
54 * (typ list * typ list list list * typ list list)) -> |
53 * (typ list * typ list list list * typ list list)) -> |
55 (string -> binding) -> typ list -> typ list -> typ list -> term -> term -> Proof.context -> |
54 (string -> binding) -> typ list -> typ list -> term -> term -> Proof.context -> |
56 (term * term * thm * thm) * Proof.context |
55 (term * term * thm * thm) * Proof.context |
57 val derive_induct_fold_rec_thms_for_types: BNF_Def.bnf list -> term list -> term list -> thm -> |
56 val derive_induct_fold_rec_thms_for_types: BNF_Def.bnf list -> term list -> term list -> thm -> |
58 thm list -> thm list -> BNF_Def.bnf list -> BNF_Def.bnf list -> typ list -> typ list -> |
57 thm list -> thm list -> BNF_Def.bnf list -> BNF_Def.bnf list -> typ list -> typ list -> |
59 term list list -> thm list list -> term list -> term list -> thm list -> thm list -> |
58 term list list -> thm list list -> term list -> term list -> thm list -> thm list -> |
60 local_theory -> |
59 local_theory -> |
483 val cqfsss = map3 (map3 (map3 build_dtor_coiter_arg)) f_Tsss cqssss cfssss; |
482 val cqfsss = map3 (map3 (map3 build_dtor_coiter_arg)) f_Tsss cqssss cfssss; |
484 in |
483 in |
485 Term.list_comb (dtor_coiter, map4 mk_preds_getterss_join cs cpss f_sum_prod_Ts cqfsss) |
484 Term.list_comb (dtor_coiter, map4 mk_preds_getterss_join cs cpss f_sum_prod_Ts cqfsss) |
486 end; |
485 end; |
487 |
486 |
488 fun define_fold_rec (fold_only, rec_only) mk_binding fpTs As Cs ctor_fold ctor_rec lthy0 = |
487 fun define_fold_rec (fold_only, rec_only) mk_binding fpTs Cs ctor_fold ctor_rec lthy0 = |
489 let |
488 let |
490 val thy = Proof_Context.theory_of lthy0; |
489 val thy = Proof_Context.theory_of lthy0; |
491 |
490 |
492 val nn = length fpTs; |
491 val nn = length fpTs; |
493 |
492 |
518 val [foldx, recx] = map (mk_co_iter thy true fpT Cs o Morphism.term phi) csts; |
517 val [foldx, recx] = map (mk_co_iter thy true fpT Cs o Morphism.term phi) csts; |
519 in |
518 in |
520 ((foldx, recx, fold_def, rec_def), lthy') |
519 ((foldx, recx, fold_def, rec_def), lthy') |
521 end; |
520 end; |
522 |
521 |
523 fun define_unfold_corec (cs, cpss, unfold_only, corec_only) mk_binding fpTs As Cs dtor_unfold |
522 fun define_unfold_corec (cs, cpss, unfold_only, corec_only) mk_binding fpTs Cs dtor_unfold |
524 dtor_corec lthy0 = |
523 dtor_corec lthy0 = |
525 let |
524 let |
526 val thy = Proof_Context.theory_of lthy0; |
525 val thy = Proof_Context.theory_of lthy0; |
527 |
526 |
528 val nn = length fpTs; |
527 val nn = length fpTs; |
553 val [unfold_def, corec_def] = map (Morphism.thm phi) defs; |
552 val [unfold_def, corec_def] = map (Morphism.thm phi) defs; |
554 |
553 |
555 val [unfold, corec] = map (mk_co_iter thy false fpT Cs o Morphism.term phi) csts; |
554 val [unfold, corec] = map (mk_co_iter thy false fpT Cs o Morphism.term phi) csts; |
556 in |
555 in |
557 ((unfold, corec, unfold_def, corec_def), lthy') |
556 ((unfold, corec, unfold_def, corec_def), lthy') |
558 end; |
557 end ; |
559 |
558 |
560 fun derive_induct_fold_rec_thms_for_types pre_bnfs ctor_folds ctor_recs ctor_induct ctor_fold_thms |
559 fun derive_induct_fold_rec_thms_for_types pre_bnfs ctor_folds ctor_recs ctor_induct ctor_fold_thms |
561 ctor_rec_thms nesting_bnfs nested_bnfs fpTs Cs ctrss ctr_defss folds recs fold_defs rec_defs |
560 ctor_rec_thms nesting_bnfs nested_bnfs fpTs Cs ctrss ctr_defss folds recs fold_defs rec_defs |
562 lthy = |
561 lthy = |
563 let |
562 let |
1328 (((maps_sets_rels, (ctrs, xss, ctr_defs, ctr_sugar)), co_iter_res), lthy); |
1327 (((maps_sets_rels, (ctrs, xss, ctr_defs, ctr_sugar)), co_iter_res), lthy); |
1329 in |
1328 in |
1330 (wrap_ctrs |
1329 (wrap_ctrs |
1331 #> derive_maps_sets_rels |
1330 #> derive_maps_sets_rels |
1332 ##>> (if lfp then define_fold_rec (the fold_rec_args_types) |
1331 ##>> (if lfp then define_fold_rec (the fold_rec_args_types) |
1333 else define_unfold_corec (the unfold_corec_args_types)) |
1332 else define_unfold_corec (the unfold_corec_args_types)) mk_binding fpTs Cs fp_fold fp_rec |
1334 mk_binding fpTs As Cs fp_fold fp_rec |
|
1335 #> massage_res, lthy') |
1333 #> massage_res, lthy') |
1336 end; |
1334 end; |
1337 |
1335 |
1338 fun wrap_types_etc (wrap_types_etcs, lthy) = |
1336 fun wrap_types_etc (wrap_types_etcs, lthy) = |
1339 fold_map I wrap_types_etcs lthy |
1337 fold_map I wrap_types_etcs lthy |