23 |
23 |
24 val fp_sugar_of: local_theory -> string -> fp_sugar option |
24 val fp_sugar_of: local_theory -> string -> fp_sugar option |
25 |
25 |
26 val exists_subtype_in: typ list -> typ -> bool |
26 val exists_subtype_in: typ list -> typ -> bool |
27 val indexify_fst: ''a list -> (int -> ''a * 'b -> 'c) -> ''a * 'b -> 'c |
27 val indexify_fst: ''a list -> (int -> ''a * 'b -> 'c) -> ''a * 'b -> 'c |
|
28 val mk_fp_iter: bool -> typ list -> typ list -> term list -> term list * typ list |
28 val build_map: local_theory -> (typ * typ -> term) -> typ * typ -> term |
29 val build_map: local_theory -> (typ * typ -> term) -> typ * typ -> term |
29 |
30 |
30 val mk_iter_fun_arg_types_pairsss: typ list -> int list -> int list list -> term -> |
31 val mk_iter_fun_arg_types_pairsss: typ list -> int list -> int list list -> term -> |
31 (typ list * typ list) list list list |
32 (typ list * typ list) list list list |
32 val mk_fold_recs: Proof.context -> typ list -> typ list -> typ list -> int list -> |
33 val mk_folds_recs: Proof.context -> typ list -> typ list -> typ list -> int list -> |
33 int list list -> term list -> term list -> term list * term list |
34 int list list -> term list -> term list -> term list * term list |
34 val mk_unfold_corecs: Proof.context -> typ list -> typ list -> typ list -> int list -> |
35 val mk_unfolds_corecs: Proof.context -> typ list -> typ list -> typ list -> int list -> |
35 int list list -> term list -> term list -> term list * term list |
36 int list list -> term list -> term list -> term list * term list |
36 |
37 |
37 val derive_induct_fold_rec_thms_for_types: BNF_Def.bnf list -> term list -> term list -> thm -> |
38 val derive_induct_fold_rec_thms_for_types: BNF_Def.bnf list -> term list -> term list -> thm -> |
38 thm list -> thm list -> BNF_Def.bnf list -> BNF_Def.bnf list -> typ list -> typ list -> |
39 thm list -> thm list -> BNF_Def.bnf list -> BNF_Def.bnf list -> typ list -> typ list -> |
39 typ list -> term list list -> thm list list -> term list -> term list -> thm list -> thm list -> |
40 typ list -> term list list -> thm list list -> term list -> term list -> thm list -> thm list -> |
403 fun mk_iter_arg f xs = mk_tupled_fun (HOLogic.mk_tuple xs) f (flat_rec unzip_rec xs); |
404 fun mk_iter_arg f xs = mk_tupled_fun (HOLogic.mk_tuple xs) f (flat_rec unzip_rec xs); |
404 in |
405 in |
405 Term.list_comb (ctor_iter, map2 (mk_sum_caseN_balanced oo map2 mk_iter_arg) fss xsss) |
406 Term.list_comb (ctor_iter, map2 (mk_sum_caseN_balanced oo map2 mk_iter_arg) fss xsss) |
406 end; |
407 end; |
407 |
408 |
408 fun mk_fold_recs lthy fpTs As Cs ns mss ctor_folds ctor_recs = |
409 fun mk_folds_recs lthy fpTs As Cs ns mss ctor_folds ctor_recs = |
409 let |
410 let |
410 val (_, ctor_fold_fun_Ts) = mk_fp_iter true As Cs ctor_folds; |
411 val (_, ctor_fold_fun_Ts) = mk_fp_iter true As Cs ctor_folds; |
411 val (_, ctor_rec_fun_Ts) = mk_fp_iter true As Cs ctor_recs; |
412 val (_, ctor_rec_fun_Ts) = mk_fp_iter true As Cs ctor_recs; |
412 |
413 |
413 val (((gss, _, ysss), (hss, _, zsss)), _) = |
414 val (((gss, _, ysss), (hss, _, zsss)), _) = |
437 val cqfsss = map3 (map3 (map3 build_dtor_coiter_arg)) f_Tsss cqssss cfssss; |
438 val cqfsss = map3 (map3 (map3 build_dtor_coiter_arg)) f_Tsss cqssss cfssss; |
438 in |
439 in |
439 Term.list_comb (dtor_coiter, map5 mk_preds_getterss_join cs ns cpss f_sum_prod_Ts cqfsss) |
440 Term.list_comb (dtor_coiter, map5 mk_preds_getterss_join cs ns cpss f_sum_prod_Ts cqfsss) |
440 end; |
441 end; |
441 |
442 |
442 fun mk_unfold_corecs lthy fpTs As Cs ns mss dtor_unfolds dtor_corecs = |
443 fun mk_unfolds_corecs lthy fpTs As Cs ns mss dtor_unfolds dtor_corecs = |
443 let |
444 let |
444 val (_, dtor_unfold_fun_Ts) = mk_fp_iter true As Cs dtor_unfolds; |
445 val (_, dtor_unfold_fun_Ts) = mk_fp_iter true As Cs dtor_unfolds; |
445 val (_, dtor_corec_fun_Ts) = mk_fp_iter true As Cs dtor_corecs; |
446 val (_, dtor_corec_fun_Ts) = mk_fp_iter true As Cs dtor_corecs; |
446 |
447 |
447 val ((cs, cpss, unfold_only, corec_only), _) = |
448 val ((cs, cpss, unfold_only, corec_only), _) = |