# HG changeset patch # User blanchet # Date 1393502697 -3600 # Node ID 367ec44763fdfce599f39c6015cb6452e5e0a0a2 # Parent a421f1ccfc9f9d32a488d1312144ba1228cd014f correct most general type for mutual recursion when several identical types are involved diff -r a421f1ccfc9f -r 367ec44763fd src/HOL/Tools/BNF/bnf_fp_def_sugar.ML --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Thu Feb 27 11:41:32 2014 +0100 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Thu Feb 27 13:04:57 2014 +0100 @@ -9,12 +9,14 @@ sig type fp_sugar = {T: typ, + X: typ, fp: BNF_Util.fp_kind, fp_res_index: int, fp_res: BNF_FP_Util.fp_result, pre_bnf: BNF_Def.bnf, nested_bnfs: BNF_Def.bnf list, nesting_bnfs: BNF_Def.bnf list, + ctrXs_Tss: typ list list, ctr_defs: thm list, ctr_sugar: Ctr_Sugar.ctr_sugar, co_iters: term list, @@ -61,9 +63,8 @@ * (string * term list * term list list * ((term list list * term list list list) * typ list) list) option) * Proof.context - val mk_coiter_fun_arg_types: typ list list list -> typ list -> int list -> term -> - typ list list - * (typ list list list list * typ list list list * typ list list list list * typ list) + val repair_nullary_single_ctr: typ list list -> typ list list + val mk_coiter_p_pred_types: typ list -> int list -> typ list list val define_iters: string list -> (typ list list * typ list list list list * term list list * term list list list list) list -> (string -> binding) -> typ list -> typ list -> term list -> Proof.context -> @@ -115,12 +116,14 @@ type fp_sugar = {T: typ, + X: typ, fp: fp_kind, fp_res_index: int, fp_res: fp_result, pre_bnf: bnf, nested_bnfs: bnf list, nesting_bnfs: bnf list, + ctrXs_Tss: typ list list, ctr_defs: thm list, ctr_sugar: Ctr_Sugar.ctr_sugar, co_iters: term list, @@ -131,16 +134,18 @@ disc_co_iterss: thm list list, sel_co_itersss: thm list list list}; -fun morph_fp_sugar phi ({T, fp, fp_res, fp_res_index, pre_bnf, nested_bnfs, nesting_bnfs, ctr_defs, - ctr_sugar, co_iters, maps, common_co_inducts, co_inducts, co_iter_thmss, disc_co_iterss, - sel_co_itersss} : fp_sugar) = +fun morph_fp_sugar phi ({T, X, fp, fp_res, fp_res_index, pre_bnf, nested_bnfs, nesting_bnfs, + ctrXs_Tss, ctr_defs, ctr_sugar, co_iters, maps, common_co_inducts, co_inducts, co_iter_thmss, + disc_co_iterss, sel_co_itersss} : fp_sugar) = {T = Morphism.typ phi T, + X = Morphism.typ phi X, fp = fp, fp_res = morph_fp_result phi fp_res, fp_res_index = fp_res_index, pre_bnf = morph_bnf phi pre_bnf, nested_bnfs = map (morph_bnf phi) nested_bnfs, nesting_bnfs = map (morph_bnf phi) nesting_bnfs, + ctrXs_Tss = map (map (Morphism.typ phi)) ctrXs_Tss, ctr_defs = map (Morphism.thm phi) ctr_defs, ctr_sugar = morph_ctr_sugar phi ctr_sugar, co_iters = map (Morphism.term phi) co_iters, @@ -178,17 +183,17 @@ Local_Theory.declaration {syntax = false, pervasive = true} (fn phi => Data.map (Symtab.update (key, morph_fp_sugar phi fp_sugar))); -fun register_fp_sugars fp pre_bnfs nested_bnfs nesting_bnfs (fp_res as {Ts, ...}) ctr_defss - ctr_sugars co_iterss mapss common_co_inducts co_inductss co_iter_thmsss disc_co_itersss - sel_co_iterssss lthy = +fun register_fp_sugars Xs fp pre_bnfs nested_bnfs nesting_bnfs (fp_res as {Ts, ...}) ctrXs_Tsss + ctr_defss ctr_sugars co_iterss mapss common_co_inducts co_inductss co_iter_thmsss + disc_co_itersss sel_co_iterssss lthy = (0, lthy) |> fold (fn T as Type (s, _) => fn (kk, lthy) => (kk + 1, - register_fp_sugar s {T = T, fp = fp, fp_res = fp_res, fp_res_index = kk, + register_fp_sugar s {T = T, X = nth Xs kk, fp = fp, fp_res = fp_res, fp_res_index = kk, pre_bnf = nth pre_bnfs kk, nested_bnfs = nested_bnfs, nesting_bnfs = nesting_bnfs, - ctr_defs = nth ctr_defss kk, ctr_sugar = nth ctr_sugars kk, co_iters = nth co_iterss kk, - maps = nth mapss kk, common_co_inducts = common_co_inducts, co_inducts = nth co_inductss kk, - co_iter_thmss = nth co_iter_thmsss kk, disc_co_iterss = nth disc_co_itersss kk, - sel_co_itersss = nth sel_co_iterssss kk} + ctrXs_Tss = nth ctrXs_Tsss kk, ctr_defs = nth ctr_defss kk, ctr_sugar = nth ctr_sugars kk, + co_iters = nth co_iterss kk, maps = nth mapss kk, common_co_inducts = common_co_inducts, + co_inducts = nth co_inductss kk, co_iter_thmss = nth co_iter_thmsss kk, + disc_co_iterss = nth disc_co_itersss kk, sel_co_itersss = nth sel_co_iterssss kk} lthy)) Ts |> snd; @@ -381,13 +386,13 @@ ([(g_Tss, y_Tssss, gss, yssss), (h_Tss, z_Tssss, hss, zssss)], lthy) end; +(*avoid "'a itself" arguments in coiterators*) +fun repair_nullary_single_ctr [[]] = [[@{typ unit}]] + | repair_nullary_single_ctr Tss = Tss; + fun mk_coiter_fun_arg_types0 ctr_Tsss Cs ns fun_Ts = let - (*avoid "'a itself" arguments in coiterators*) - fun repair_arity [[]] = [[@{typ unit}]] - | repair_arity Tss = Tss; - - val ctr_Tsss' = map repair_arity ctr_Tsss; + val ctr_Tsss' = map repair_nullary_single_ctr ctr_Tsss; val f_sum_prod_Ts = map range_type fun_Ts; val f_prod_Tss = map2 dest_sumTN_balanced ns f_sum_prod_Ts; val f_Tsss = map2 (map2 (dest_tupleT o length)) ctr_Tsss' f_prod_Tss; @@ -400,10 +405,6 @@ fun mk_coiter_p_pred_types Cs ns = map2 (fn n => replicate (Int.max (0, n - 1)) o mk_pred1T) ns Cs; -fun mk_coiter_fun_arg_types ctr_Tsss Cs ns dtor_coiter = - (mk_coiter_p_pred_types Cs ns, - mk_coiter_fun_arg_types0 ctr_Tsss Cs ns (binder_fun_types (fastype_of dtor_coiter))); - fun mk_coiters_args_types ctr_Tsss Cs ns dtor_coiter_fun_Tss lthy = let val p_Tss = mk_coiter_p_pred_types Cs ns; @@ -1385,9 +1386,9 @@ |> Spec_Rules.add Spec_Rules.Equational (map un_fold_of iterss, flat fold_thmss) |> Spec_Rules.add Spec_Rules.Equational (map co_rec_of iterss, flat rec_thmss) |> Local_Theory.notes (common_notes @ notes) |> snd - |> register_fp_sugars Least_FP pre_bnfs nested_bnfs nesting_bnfs fp_res ctr_defss ctr_sugars - iterss mapss [induct_thm] (map single induct_thms) (transpose [fold_thmss, rec_thmss]) - (replicate nn []) (replicate nn []) + |> register_fp_sugars Xs Least_FP pre_bnfs nested_bnfs nesting_bnfs fp_res ctrXs_Tsss + ctr_defss ctr_sugars iterss mapss [induct_thm] (map single induct_thms) + (transpose [fold_thmss, rec_thmss]) (replicate nn []) (replicate nn []) end; fun derive_note_coinduct_coiters_thms_for_types @@ -1450,8 +1451,8 @@ |> add_spec_rules un_fold_of sel_unfold_thmss unfold_thmss |> add_spec_rules co_rec_of sel_corec_thmss corec_thmss |> Local_Theory.notes (common_notes @ notes) |> snd - |> register_fp_sugars Greatest_FP pre_bnfs nested_bnfs nesting_bnfs fp_res ctr_defss - ctr_sugars coiterss mapss [coinduct_thm, strong_coinduct_thm] + |> register_fp_sugars Xs Greatest_FP pre_bnfs nested_bnfs nesting_bnfs fp_res ctrXs_Tsss + ctr_defss ctr_sugars coiterss mapss [coinduct_thm, strong_coinduct_thm] (transpose [coinduct_thms, strong_coinduct_thms]) (transpose [unfold_thmss, corec_thmss]) (transpose [disc_unfold_thmss, disc_corec_thmss]) (transpose [sel_unfold_thmsss, sel_corec_thmsss]) diff -r a421f1ccfc9f -r 367ec44763fd src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML --- a/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML Thu Feb 27 11:41:32 2014 +0100 +++ b/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML Thu Feb 27 13:04:57 2014 +0100 @@ -10,12 +10,12 @@ val unfold_lets_splits: term -> term val dest_map: Proof.context -> string -> term -> term * term list - val mutualize_fp_sugars: BNF_Util.fp_kind -> binding list -> typ list -> (term -> int list) -> + val mutualize_fp_sugars: BNF_Util.fp_kind -> binding list -> typ list -> term list -> term list list list list -> BNF_FP_Def_Sugar.fp_sugar list -> local_theory -> (BNF_FP_Def_Sugar.fp_sugar list * (BNF_FP_Def_Sugar.lfp_sugar_thms option * BNF_FP_Def_Sugar.gfp_sugar_thms option)) * local_theory - val nested_to_mutual_fps: BNF_Util.fp_kind -> binding list -> typ list -> (term -> int list) -> + val nested_to_mutual_fps: BNF_Util.fp_kind -> binding list -> typ list -> term list -> (term * term list list) list list -> local_theory -> (typ list * int list * BNF_FP_Def_Sugar.fp_sugar list * (BNF_FP_Def_Sugar.lfp_sugar_thms option * BNF_FP_Def_Sugar.gfp_sugar_thms option)) @@ -103,8 +103,13 @@ fun key_of_fp_eqs fp fpTs fp_eqs = Type (fp_case fp "l" "g", fpTs @ maps (fn (x, T) => [TFree x, T]) fp_eqs); +fun get_indices callers t = + callers + |> map_index (fn (i, v) => if exists_subterm (equal v) t then SOME i else NONE) + |> map_filter I; + (* TODO: test with sort constraints on As *) -fun mutualize_fp_sugars fp bs fpTs get_indices callssss fp_sugars0 no_defs_lthy0 = +fun mutualize_fp_sugars fp bs fpTs callers callssss fp_sugars0 no_defs_lthy0 = let val thy = Proof_Context.theory_of no_defs_lthy0; @@ -112,6 +117,8 @@ fun incompatible_calls ts = error ("Incompatible " ^ co_prefix fp ^ "recursive calls: " ^ commas (map qsotm ts)); + fun mutual_self_call caller t = + error ("Unsupported mutual self-call " ^ qsotm t ^ " from " ^ qsotm caller); fun nested_self_call t = error ("Unsupported nested self-call " ^ qsotm t); @@ -146,7 +153,7 @@ ||>> variant_tfrees fp_b_names; fun check_call_dead live_call call = - if null (get_indices call) then () else incompatible_calls [live_call, call]; + if null (get_indices callers call) then () else incompatible_calls [live_call, call]; fun freeze_fpTs_type_based_default (T as Type (s, Ts)) = (case filter (curry (op =) T o snd) (map_index I fpTs) of @@ -154,31 +161,36 @@ | _ => Type (s, map freeze_fpTs_type_based_default Ts)) | freeze_fpTs_type_based_default T = T; - fun freeze_fpTs_mutual_call calls T = - (case fold (union (op =)) (map get_indices calls) [] of - [] => freeze_fpTs_type_based_default T - | [kk] => nth Xs kk + fun freeze_fpTs_mutual_call kk fpT calls T = + (case fold (union (op =)) (map (get_indices callers) calls) [] of + [] => if T = fpT then nth Xs kk else freeze_fpTs_type_based_default T + | [kk'] => + if T = fpT andalso kk' <> kk then + mutual_self_call (nth callers kk) + (the (find_first (not o null o get_indices callers) calls)) + else + nth Xs kk' | _ => incompatible_calls calls); - fun freeze_fpTs_map (fpT as Type (_, Ts')) (callss, (live_call :: _, dead_calls)) + fun freeze_fpTs_map kk (fpT as Type (_, Ts')) (callss, (live_call :: _, dead_calls)) (Type (s, Ts)) = if Ts' = Ts then nested_self_call live_call else (List.app (check_call_dead live_call) dead_calls; - Type (s, map2 (freeze_fpTs_call fpT) + Type (s, map2 (freeze_fpTs_call kk fpT) (flatten_type_args_of_bnf (the (bnf_of no_defs_lthy s)) [] (transpose callss)) Ts)) - and freeze_fpTs_call fpT calls (T as Type (s, _)) = + and freeze_fpTs_call kk fpT calls (T as Type (s, _)) = (case map_partition (try (snd o dest_map no_defs_lthy s)) calls of ([], _) => (case map_partition (try (snd o dest_abs_or_applied_map no_defs_lthy s)) calls of - ([], _) => freeze_fpTs_mutual_call calls T - | callsp => freeze_fpTs_map fpT callsp T) - | callsp => freeze_fpTs_map fpT callsp T) - | freeze_fpTs_call _ _ T = T; + ([], _) => freeze_fpTs_mutual_call kk fpT calls T + | callsp => freeze_fpTs_map kk fpT callsp T) + | callsp => freeze_fpTs_map kk fpT callsp T) + | freeze_fpTs_call _ _ _ T = T; val ctr_Tsss = map (map binder_types) ctr_Tss; - val ctrXs_Tsss = map3 (map2 o map2 o freeze_fpTs_call) fpTs callssss ctr_Tsss; + val ctrXs_Tsss = map4 (map2 o map2 oo freeze_fpTs_call) kks fpTs callssss ctr_Tsss; val ctrXs_sum_prod_Ts = map (mk_sumTN_balanced o map HOLogic.mk_tupleT) ctrXs_Tsss; val ns = map length ctr_Tsss; @@ -254,11 +266,12 @@ val phi = Proof_Context.export_morphism no_defs_lthy no_defs_lthy0; - fun mk_target_fp_sugar T kk pre_bnf ctr_defs ctr_sugar co_iters maps co_inducts un_fold_thms - co_rec_thms disc_unfold_thms disc_corec_thms sel_unfold_thmss sel_corec_thmss = - {T = T, fp = fp, fp_res = fp_res, fp_res_index = kk, pre_bnf = pre_bnf, - nested_bnfs = nested_bnfs, nesting_bnfs = nesting_bnfs, ctr_defs = ctr_defs, - ctr_sugar = ctr_sugar, co_iters = co_iters, maps = maps, + fun mk_target_fp_sugar T X kk pre_bnf ctrXs_Tss ctr_defs ctr_sugar co_iters maps co_inducts + un_fold_thms co_rec_thms disc_unfold_thms disc_corec_thms sel_unfold_thmss + sel_corec_thmss = + {T = T, X = X, fp = fp, fp_res = fp_res, fp_res_index = kk, pre_bnf = pre_bnf, + nested_bnfs = nested_bnfs, nesting_bnfs = nesting_bnfs, ctrXs_Tss = ctrXs_Tss, + ctr_defs = ctr_defs, ctr_sugar = ctr_sugar, co_iters = co_iters, maps = maps, common_co_inducts = common_co_inducts, co_inducts = co_inducts, co_iter_thmss = [un_fold_thms, co_rec_thms], disc_co_iterss = [disc_unfold_thms, disc_corec_thms], @@ -266,9 +279,9 @@ |> morph_fp_sugar phi; val target_fp_sugars = - map14 mk_target_fp_sugar fpTs kks pre_bnfs ctr_defss ctr_sugars co_iterss mapss - (transpose co_inductss) un_fold_thmss co_rec_thmss disc_unfold_thmss disc_corec_thmss - sel_unfold_thmsss sel_corec_thmsss; + map16 mk_target_fp_sugar fpTs Xs kks pre_bnfs ctrXs_Tsss ctr_defss ctr_sugars co_iterss + mapss (transpose co_inductss) un_fold_thmss co_rec_thmss disc_unfold_thmss + disc_corec_thmss sel_unfold_thmsss sel_corec_thmsss; val n2m_sugar = (target_fp_sugars, fp_sugar_thms); in @@ -292,7 +305,9 @@ f (T, U) #> (if s = s' then fold (fold_subtype_pairs f) (Ts ~~ Us) else I) | fold_subtype_pairs f TU = f TU; -fun nested_to_mutual_fps fp actual_bs actual_Ts get_indices actual_callssss0 lthy = +val impossible_caller = Bound ~1; + +fun nested_to_mutual_fps fp actual_bs actual_Ts actual_callers actual_callssss0 lthy = let val qsoty = quote o Syntax.string_of_typ lthy; val qsotys = space_implode " or " o map qsoty; @@ -391,23 +406,23 @@ val common_name = mk_common_name (map Binding.name_of actual_bs); val bs = pad_list (Binding.name common_name) nn actual_bs; + val callers = pad_list impossible_caller nn actual_callers; fun permute xs = permute_like (op =) Ts perm_Ts xs; fun unpermute perm_xs = permute_like (op =) perm_Ts Ts perm_xs; val perm_bs = permute bs; + val perm_callers = permute callers; val perm_kks = permute kks; val perm_callssss0 = permute callssss0; val perm_fp_sugars0 = map (the o fp_sugar_of lthy o fst o dest_Type) perm_Ts; val perm_callssss = map2 (indexify_callsss o #ctrs o #ctr_sugar) perm_fp_sugars0 perm_callssss0; - val get_perm_indices = map (fn kk => find_index (curry (op =) kk) perm_kks) o get_indices; - val ((perm_fp_sugars, fp_sugar_thms), lthy) = if num_groups > 1 then - mutualize_fp_sugars fp perm_bs perm_frozen_gen_Ts get_perm_indices perm_callssss - perm_fp_sugars0 lthy + mutualize_fp_sugars fp perm_bs perm_frozen_gen_Ts perm_callers perm_callssss perm_fp_sugars0 + lthy else ((perm_fp_sugars0, (NONE, NONE)), lthy); diff -r a421f1ccfc9f -r 367ec44763fd src/HOL/Tools/BNF/bnf_fp_rec_sugar_util.ML --- a/src/HOL/Tools/BNF/bnf_fp_rec_sugar_util.ML Thu Feb 27 11:41:32 2014 +0100 +++ b/src/HOL/Tools/BNF/bnf_fp_rec_sugar_util.ML Thu Feb 27 13:04:57 2014 +0100 @@ -38,7 +38,6 @@ val mk_compN: int -> typ list -> term * term -> term val mk_comp: typ list -> term * term -> term - val get_free_indices: ((binding * typ) * 'a) list -> term -> int list val mk_co_iter: theory -> fp_kind -> typ -> typ list -> term -> term val mk_conjunctN: int -> int -> thm @@ -109,10 +108,6 @@ val mk_comp = mk_compN 1; -fun get_free_indices fixes t = map (fst #>> Binding.name_of #> Free) fixes - |> map_index (fn (i, v) => if exists_subterm (equal v) t then SOME i else NONE) - |> map_filter I; - fun mk_co_iter thy fp fpT Cs t = let val ((f_Cs, prebody), body) = strip_type (fastype_of t) |>> split_last; diff -r a421f1ccfc9f -r 367ec44763fd src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML --- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Thu Feb 27 11:41:32 2014 +0100 +++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Thu Feb 27 13:04:57 2014 +0100 @@ -370,33 +370,44 @@ (case fp_sugar_of ctxt s of SOME {maps, ...} => maps | NONE => []) | map_thms_of_typ _ _ = []; -fun corec_specs_of bs arg_Ts res_Ts get_indices callssss0 lthy0 = +fun corec_specs_of bs arg_Ts res_Ts callers callssss0 lthy0 = let val thy = Proof_Context.theory_of lthy0; - val ((missing_res_Ts, perm0_kks, - fp_sugars as {nested_bnfs, fp_res = {xtor_co_iterss = dtor_coiters1 :: _, ...}, - common_co_inducts = common_coinduct_thms, ...} :: _, (_, gfp_sugar_thms)), lthy) = - nested_to_mutual_fps Greatest_FP bs res_Ts get_indices callssss0 lthy0; + val ((missing_res_Ts, perm0_kks, fp_sugars as {nested_bnfs, co_iters = coiter1 :: _, + common_co_inducts = common_coinduct_thms, ...} :: _, + (_, gfp_sugar_thms)), lthy) = + nested_to_mutual_fps Greatest_FP bs res_Ts callers callssss0 lthy0; val perm_fp_sugars = sort (int_ord o pairself #fp_res_index) fp_sugars; val indices = map #fp_res_index fp_sugars; val perm_indices = map #fp_res_index perm_fp_sugars; - val perm_ctrss = map (#ctrs o #ctr_sugar) perm_fp_sugars; - val perm_ctr_Tsss = map (map (binder_types o fastype_of)) perm_ctrss; - val perm_gfpTs = map (body_type o fastype_of o hd) perm_ctrss; + val perm_gfpTs = map #T perm_fp_sugars; + val perm_ctrXs_Tsss' = map (repair_nullary_single_ctr o #ctrXs_Tss) perm_fp_sugars; val nn0 = length res_Ts; val nn = length perm_gfpTs; val kks = 0 upto nn - 1; - val perm_ns = map length perm_ctr_Tsss; + val perm_ns' = map length perm_ctrXs_Tsss'; + + val perm_Ts = map #T perm_fp_sugars; + val perm_Xs = map #X perm_fp_sugars; + val perm_Cs = map (domain_type o body_fun_type o fastype_of o co_rec_of o #co_iters) perm_fp_sugars; + val Xs_TCs = perm_Xs ~~ (perm_Ts ~~ perm_Cs); - val perm_Cs = map (fn {fp_res, fp_res_index, ...} => domain_type (body_fun_type (fastype_of - (co_rec_of (nth (#xtor_co_iterss fp_res) fp_res_index))))) perm_fp_sugars; - val (perm_p_Tss, (perm_q_Tssss, _, perm_f_Tssss, _)) = - mk_coiter_fun_arg_types perm_ctr_Tsss perm_Cs perm_ns (co_rec_of dtor_coiters1); + fun zip_corecT (Type (s, Us)) = [Type (s, map (mk_sumTN o zip_corecT) Us)] + | zip_corecT U = + (case AList.lookup (op =) Xs_TCs U of + SOME (T, C) => [T, C] + | NONE => [U]); + + val perm_p_Tss = mk_coiter_p_pred_types perm_Cs perm_ns'; + val perm_f_Tssss = + map2 (fn C => map (map (map (curry (op -->) C) o zip_corecT))) perm_Cs perm_ctrXs_Tsss'; + val perm_q_Tssss = + map (map (map (fn [_] => [] | [_, T] => [mk_pred1T (domain_type T)]))) perm_f_Tssss; val (perm_p_hss, h) = indexedd perm_p_Tss 0; val (perm_q_hssss, h') = indexedddd perm_q_Tssss h; @@ -915,7 +926,8 @@ val fun_names = map Binding.name_of bs; val basic_ctr_specss = map (basic_corec_specs_of lthy) res_Ts; - val has_call = exists_subterm (map (fst #>> Binding.name_of #> Free) fixes |> member (op =)); + val frees = map (fst #>> Binding.name_of #> Free) fixes; + val has_call = exists_subterm (member (op =) frees); val eqns_data = fold_map2 (dissect_coeqn lthy has_call fun_names sequentials basic_ctr_specss) (tag_list 0 (map snd specs)) of_specs_opt [] @@ -936,7 +948,7 @@ val ((n2m, corec_specs', _, coinduct_thm, strong_coinduct_thm, coinduct_thms, strong_coinduct_thms), lthy') = - corec_specs_of bs arg_Ts res_Ts (get_free_indices fixes) callssss lthy; + corec_specs_of bs arg_Ts res_Ts frees callssss lthy; val corec_specs = take actual_nn corec_specs'; val ctr_specss = map #ctr_specs corec_specs; diff -r a421f1ccfc9f -r 367ec44763fd src/HOL/Tools/BNF/bnf_lfp_compat.ML --- a/src/HOL/Tools/BNF/bnf_lfp_compat.ML Thu Feb 27 11:41:32 2014 +0100 +++ b/src/HOL/Tools/BNF/bnf_lfp_compat.ML Thu Feb 27 13:04:57 2014 +0100 @@ -99,8 +99,6 @@ | NONE => error ("Unsupported recursion via type constructor " ^ quote s ^ " not corresponding to new-style datatype (cf. \"datatype_new\")")); - fun get_var_indices (Var ((_, kk), _)) = [kk]; - val (Tparentss_kkssss, _) = nested_Tparentss_indicessss_of [] fpT1 0; val Tparentss = map fst Tparentss_kkssss; val Ts = map (fst o hd) Tparentss; @@ -110,14 +108,6 @@ val ctrss0 = map (#ctrs o #ctr_sugar) fp_sugars0; val ctr_Tsss0 = map (map (binder_types o fastype_of)) ctrss0; - fun apply_comps n kk = - mk_partial_compN n (replicate n @{typ unit} ---> @{typ unit}) - (Var ((Name.uu, kk), @{typ "unit => unit"})); - - val callssss = - map2 (map2 (map2 (fn kks => fn ctr_T => map (apply_comps (num_binder_types ctr_T)) kks))) - kkssss ctr_Tsss0; - val b_names = Name.variant_list [] (map base_name_of_typ Ts); val compat_b_names = map (prefix compatN) b_names; val compat_bs = map Binding.name compat_b_names; @@ -126,9 +116,18 @@ val nn_fp = length fpTs; val nn = length Ts; + val callers = map (fn kk => Var ((Name.uu, kk), @{typ "unit => unit"})) (0 upto nn - 1); + + fun apply_comps n kk = + mk_partial_compN n (replicate n @{typ unit} ---> @{typ unit}) (nth callers kk); + + val callssss = + map2 (map2 (map2 (fn kks => fn ctr_T => map (apply_comps (num_binder_types ctr_T)) kks))) + kkssss ctr_Tsss0; + val ((fp_sugars, (lfp_sugar_thms, _)), lthy) = if nn > nn_fp then - mutualize_fp_sugars Least_FP compat_bs Ts get_var_indices callssss fp_sugars0 lthy + mutualize_fp_sugars Least_FP compat_bs Ts callers callssss fp_sugars0 lthy else ((fp_sugars0, (NONE, NONE)), lthy); diff -r a421f1ccfc9f -r 367ec44763fd src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML --- a/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML Thu Feb 27 11:41:32 2014 +0100 +++ b/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML Thu Feb 27 13:04:57 2014 +0100 @@ -21,9 +21,9 @@ type lfp_rec_extension = {nested_simps: thm list, is_new_datatype: Proof.context -> string -> bool, - get_basic_lfp_sugars: binding list -> typ list -> (term -> int list) -> - (term * term list list) list list -> local_theory -> - typ list * int list * basic_lfp_sugar list * thm list * thm list * thm * bool * local_theory, + get_basic_lfp_sugars: binding list -> typ list -> term list -> + (term * term list list) list list -> local_theory -> + typ list * int list * basic_lfp_sugar list * thm list * thm list * thm * bool * local_theory, rewrite_nested_rec_call: Proof.context -> (term -> bool) -> (string -> int) -> typ list -> term -> term -> term -> term}; @@ -92,9 +92,9 @@ type lfp_rec_extension = {nested_simps: thm list, is_new_datatype: Proof.context -> string -> bool, - get_basic_lfp_sugars: binding list -> typ list -> (term -> int list) -> - (term * term list list) list list -> local_theory -> - typ list * int list * basic_lfp_sugar list * thm list * thm list * thm * bool * local_theory, + get_basic_lfp_sugars: binding list -> typ list -> term list -> + (term * term list list) list list -> local_theory -> + typ list * int list * basic_lfp_sugar list * thm list * thm list * thm * bool * local_theory, rewrite_nested_rec_call: Proof.context -> (term -> bool) -> (string -> int) -> typ list -> term -> term -> term -> term}; @@ -118,22 +118,22 @@ SOME {is_new_datatype, ...} => is_new_datatype ctxt | NONE => K false); -fun get_basic_lfp_sugars bs arg_Ts get_indices callssss lthy = +fun get_basic_lfp_sugars bs arg_Ts callers callssss lthy = (case Data.get (Proof_Context.theory_of lthy) of - SOME {get_basic_lfp_sugars, ...} => get_basic_lfp_sugars bs arg_Ts get_indices callssss lthy - | NONE => error "Not implemented yet"); + SOME {get_basic_lfp_sugars, ...} => get_basic_lfp_sugars bs arg_Ts callers callssss lthy + | NONE => error "Functionality not loaded yet"); fun rewrite_nested_rec_call ctxt = (case Data.get (Proof_Context.theory_of ctxt) of SOME {rewrite_nested_rec_call, ...} => rewrite_nested_rec_call ctxt); -fun rec_specs_of bs arg_Ts res_Ts get_indices callssss0 lthy0 = +fun rec_specs_of bs arg_Ts res_Ts callers callssss0 lthy0 = let val thy = Proof_Context.theory_of lthy0; val (missing_arg_Ts, perm0_kks, basic_lfp_sugars, nested_map_idents, nested_map_comps, induct_thm, n2m, lthy) = - get_basic_lfp_sugars bs arg_Ts get_indices callssss0 lthy0; + get_basic_lfp_sugars bs arg_Ts callers callssss0 lthy0; val perm_basic_lfp_sugars = sort (int_ord o pairself #fp_res_index) basic_lfp_sugars; @@ -427,7 +427,8 @@ |> map (fn (x, y) => the_single y handle List.Empty => raise PRIMREC ("missing equations for function " ^ quote x, [])); - val has_call = exists_subterm (map (fst #>> Binding.name_of #> Free) fixes |> member (op =)); + val frees = map (fst #>> Binding.name_of #> Free) fixes; + val has_call = exists_subterm (member (op =) frees); val arg_Ts = map (#rec_type o hd) funs_data; val res_Ts = map (#res_type o hd) funs_data; val callssss = funs_data @@ -444,7 +445,7 @@ | (b, _) :: _ => raise PRIMREC ("type of " ^ Binding.print b ^ " contains top sort", [])); val ((n2m, rec_specs, _, induct_thm, induct_thms), lthy) = - rec_specs_of bs arg_Ts res_Ts (get_free_indices fixes) callssss lthy0; + rec_specs_of bs arg_Ts res_Ts frees callssss lthy0; val actual_nn = length funs_data; @@ -469,7 +470,8 @@ |> map_filter (try (fn (x, [y]) => (#fun_name x, #user_eqn x, length (#left_args x) + length (#right_args x), #rec_thm y))) |> map2 (fn j => fn (fun_name, user_eqn, num_extra_args, rec_thm) => - mk_primrec_tac lthy' num_extra_args nested_map_idents nested_map_comps def_thms rec_thm + mk_primrec_tac lthy' num_extra_args nested_map_idents nested_map_comps def_thms + rec_thm |> K |> Goal.prove_sorry lthy' [] [] user_eqn (* for code extraction from proof terms: *) |> singleton (Proof_Context.export lthy' lthy) diff -r a421f1ccfc9f -r 367ec44763fd src/HOL/Tools/BNF/bnf_lfp_rec_sugar_more.ML --- a/src/HOL/Tools/BNF/bnf_lfp_rec_sugar_more.ML Thu Feb 27 11:41:32 2014 +0100 +++ b/src/HOL/Tools/BNF/bnf_lfp_rec_sugar_more.ML Thu Feb 27 13:04:57 2014 +0100 @@ -26,26 +26,26 @@ {T = T, fp_res_index = fp_res_index, C = C, fun_arg_Tsss = fun_arg_Tsss, ctr_defs = ctr_defs, ctr_sugar = ctr_sugar, recx = co_rec_of iters, rec_thms = co_rec_of iter_thmss}; -fun get_basic_lfp_sugars bs arg_Ts get_indices callssss0 lthy0 = +fun get_basic_lfp_sugars bs arg_Ts callers callssss0 lthy0 = let val ((missing_arg_Ts, perm0_kks, fp_sugars as {nested_bnfs, co_inducts = [induct_thm], ...} :: _, (lfp_sugar_thms, _)), lthy) = - nested_to_mutual_fps Least_FP bs arg_Ts get_indices callssss0 lthy0; + nested_to_mutual_fps Least_FP bs arg_Ts callers callssss0 lthy0; val Ts = map #T fp_sugars; + val Xs = map #X fp_sugars; val Cs = map (body_type o fastype_of o co_rec_of o #co_iters) fp_sugars; - val Ts_Cs = Ts ~~ Cs; + val Xs_TCs = Xs ~~ (Ts ~~ Cs); - fun zip_recT (T as Type (s, Ts)) = - (case AList.lookup (op =) Ts_Cs T of - SOME C => [T, C] - | NONE => [Type (s, map (HOLogic.mk_tupleT o zip_recT) Ts)]) - | zip_recT T = [T]; + fun zip_recT (Type (s, Us)) = [Type (s, map (HOLogic.mk_tupleT o zip_recT) Us)] + | zip_recT U = + (case AList.lookup (op =) Xs_TCs U of + SOME (T, C) => [T, C] + | NONE => [U]); - val ctrss = map (#ctrs o #ctr_sugar) fp_sugars; - val ctr_Tsss = map (map (binder_types o fastype_of)) ctrss; - val fun_arg_Tssss = map (map (map zip_recT)) ctr_Tsss; + val ctrXs_Tsss = map #ctrXs_Tss fp_sugars; + val fun_arg_Tssss = map (map (map zip_recT)) ctrXs_Tsss; val nested_map_idents = map (unfold_thms lthy @{thms id_def} o map_id0_of_bnf) nested_bnfs; val nested_map_comps = map map_comp_of_bnf nested_bnfs; diff -r a421f1ccfc9f -r 367ec44763fd src/HOL/Tools/BNF/bnf_util.ML --- a/src/HOL/Tools/BNF/bnf_util.ML Thu Feb 27 11:41:32 2014 +0100 +++ b/src/HOL/Tools/BNF/bnf_util.ML Thu Feb 27 13:04:57 2014 +0100 @@ -31,10 +31,18 @@ val map13: ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h -> 'i -> 'j -> 'k -> 'l -> 'm -> 'n) -> 'a list -> 'b list -> 'c list -> 'd list -> 'e list -> 'f list -> 'g list -> 'h list -> 'i list -> 'j list -> 'k list -> 'l list -> 'm list -> 'n list - val map14: - ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h -> 'i -> 'j -> 'k -> 'l -> 'm -> 'n -> 'o) -> + val map14: ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h -> 'i -> 'j -> 'k -> 'l -> 'm -> 'n -> + 'o) -> 'a list -> 'b list -> 'c list -> 'd list -> 'e list -> 'f list -> 'g list -> 'h list -> 'i list -> 'j list -> 'k list -> 'l list -> 'm list -> 'n list -> 'o list + val map15: ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h -> 'i -> 'j -> 'k -> 'l -> 'm -> 'n -> + 'o -> 'p) -> + 'a list -> 'b list -> 'c list -> 'd list -> 'e list -> 'f list -> 'g list -> 'h list -> + 'i list -> 'j list -> 'k list -> 'l list -> 'm list -> 'n list -> 'o list -> 'p list + val map16: ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h -> 'i -> 'j -> 'k -> 'l -> 'm -> 'n -> + 'o -> 'p -> 'q) -> + 'a list -> 'b list -> 'c list -> 'd list -> 'e list -> 'f list -> 'g list -> 'h list -> + 'i list -> 'j list -> 'k list -> 'l list -> 'm list -> 'n list -> 'o list -> 'p list -> 'q list val fold_map4: ('a -> 'b -> 'c -> 'd -> 'e -> 'f * 'e) -> 'a list -> 'b list -> 'c list -> 'd list -> 'e -> 'f list * 'e val fold_map5: ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g * 'f) -> @@ -202,6 +210,21 @@ map14 f x1s x2s x3s x4s x5s x6s x7s x8s x9s x10s x11s x12s x13s x14s | map14 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ = raise ListPair.UnequalLengths; +fun map15 _ [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] = [] + | map15 f (x1::x1s) (x2::x2s) (x3::x3s) (x4::x4s) (x5::x5s) (x6::x6s) (x7::x7s) (x8::x8s) + (x9::x9s) (x10::x10s) (x11::x11s) (x12::x12s) (x13::x13s) (x14::x14s) (x15::x15s) = + f x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 :: + map15 f x1s x2s x3s x4s x5s x6s x7s x8s x9s x10s x11s x12s x13s x14s x15s + | map15 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ = raise ListPair.UnequalLengths; + +fun map16 _ [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] = [] + | map16 f (x1::x1s) (x2::x2s) (x3::x3s) (x4::x4s) (x5::x5s) (x6::x6s) (x7::x7s) (x8::x8s) + (x9::x9s) (x10::x10s) (x11::x11s) (x12::x12s) (x13::x13s) (x14::x14s) (x15::x15s) + (x16::x16s) = + f x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 :: + map16 f x1s x2s x3s x4s x5s x6s x7s x8s x9s x10s x11s x12s x13s x14s x15s x16s + | map16 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ = raise ListPair.UnequalLengths; + fun fold_map4 _ [] [] [] [] acc = ([], acc) | fold_map4 f (x1::x1s) (x2::x2s) (x3::x3s) (x4::x4s) acc = let