# HG changeset patch # User blanchet # Date 1370587739 -7200 # Node ID 2f286a2b7f980cf273e3f1a502b2eee998d0a44a # Parent 9f14280aa0808d359c2b64982236bbd7adce7b7f [mq]: tuning diff -r 9f14280aa080 -r 2f286a2b7f98 src/HOL/BNF/Tools/bnf_fp_def_sugar.ML --- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML Thu Jun 06 22:01:42 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML Fri Jun 07 08:48:59 2013 +0200 @@ -818,6 +818,7 @@ (Logic.list_implies (seq_conds (HOLogic.mk_Trueprop oo mk_maybe_not) n k cps, mk_Trueprop_eq (fcoiter $ c, Term.list_comb (ctr, take m cfs')))); + (* TODO: get rid of "mk_U" *) val mk_U = typ_subst_nonatomic (map2 pair Cs fpTs); fun intr_coiters fcoiters [] [cf] = @@ -1049,9 +1050,9 @@ map dest_TFree Xs ~~ map (Term.typ_subst_atomic (As ~~ unsorted_As)) ctrXs_sum_prod_Ts; val (pre_bnfs, (fp_res as {bnfs = fp_bnfs as any_fp_bnf :: _, ctors = ctors0, dtors = dtors0, - xtor_un_folds = xtor_un_folds0, xtor_co_recs = xtor_co_recs0, xtor_co_induct, - xtor_strong_co_induct, dtor_ctors, ctor_dtors, ctor_injects, xtor_map_thms, - xtor_set_thmss, xtor_rel_thms, xtor_un_fold_thms, xtor_co_rec_thms, ...}, lthy)) = + xtor_co_iterss = xtor_co_iterss0, xtor_co_induct, xtor_strong_co_induct, dtor_ctors, + ctor_dtors, ctor_injects, xtor_map_thms, xtor_set_thmss, xtor_rel_thms, + xtor_co_iter_thmss, ...}, lthy)) = fp_bnf (construct_fp mixfixes map_bs rel_bs set_bss) fp_bs (map dest_TFree unsorted_As) fp_eqs no_defs_lthy0; @@ -1098,14 +1099,13 @@ val kss = map (fn n => 1 upto n) ns; val mss = map (map length) ctr_Tsss; - val (([xtor_un_folds, xtor_co_recs], fold_rec_args_types, unfold_corec_args_types), lthy) = - mk_un_fold_co_rec_prelims fp fpTs Cs ns mss [xtor_un_folds0, xtor_co_recs0] lthy; + val ((xtor_co_iterss', fold_rec_args_types, unfold_corec_args_types), lthy) = + mk_un_fold_co_rec_prelims fp fpTs Cs ns mss (transpose xtor_co_iterss0) lthy; - fun define_ctrs_case_for_type (((((((((((((((((((((((((fp_bnf, fp_b), fpT), C), ctor), dtor), - xtor_un_fold), xtor_co_rec), ctor_dtor), dtor_ctor), ctor_inject), pre_map_def), - pre_set_defs), pre_rel_def), fp_map_thm), fp_set_thms), fp_rel_thm), n), ks), ms), - ctr_bindings), ctr_mixfixes), ctr_Tss), disc_bindings), sel_bindingss), raw_sel_defaultss) - no_defs_lthy = + fun define_ctrs_case_for_type ((((((((((((((((((((((((fp_bnf, fp_b), fpT), C), ctor), dtor), + xtor_co_iters), ctor_dtor), dtor_ctor), ctor_inject), pre_map_def), pre_set_defs), + pre_rel_def), fp_map_thm), fp_set_thms), fp_rel_thm), n), ks), ms), ctr_bindings), + ctr_mixfixes), ctr_Tss), disc_bindings), sel_bindingss), raw_sel_defaultss) no_defs_lthy = let val fp_b_name = Binding.name_of fp_b; @@ -1295,7 +1295,7 @@ ##>> (if fp = Least_FP then define_iters [foldN, recN] (the fold_rec_args_types) else define_coiters [unfoldN, corecN] (the unfold_corec_args_types)) - mk_binding fpTs Cs [xtor_un_fold, xtor_co_rec] + mk_binding fpTs Cs xtor_co_iters #> massage_res, lthy') end; @@ -1316,9 +1316,9 @@ let val ((induct_thm, induct_thms, induct_attrs), (fold_thmss, fold_attrs), (rec_thmss, rec_attrs)) = - derive_induct_fold_rec_thms_for_types pre_bnfs [xtor_un_folds, xtor_co_recs] - (the fold_rec_args_types) xtor_co_induct [xtor_un_fold_thms, xtor_co_rec_thms] - nesting_bnfs nested_bnfs fpTs Cs Xs ctrXs_Tsss ctrss ctr_defss iterss' iter_defss' lthy; + derive_induct_fold_rec_thms_for_types pre_bnfs xtor_co_iterss' + (the fold_rec_args_types) xtor_co_induct (transpose xtor_co_iter_thmss) nesting_bnfs + nested_bnfs fpTs Cs Xs ctrXs_Tsss ctrss ctr_defss iterss' iter_defss' lthy; val induct_type_attr = Attrib.internal o K o Induct.induct_type; @@ -1353,10 +1353,9 @@ (disc_unfold_thmss, disc_corec_thmss, disc_coiter_attrs), (disc_unfold_iff_thmss, disc_corec_iff_thmss, disc_coiter_iff_attrs), (sel_unfold_thmss, sel_corec_thmss, sel_coiter_attrs)) = - derive_coinduct_unfold_corec_thms_for_types pre_bnfs [xtor_un_folds, xtor_co_recs] - xtor_co_induct xtor_strong_co_induct dtor_ctors [xtor_un_fold_thms, xtor_co_rec_thms] - nesting_bnfs nested_bnfs fpTs Cs As kss mss ns ctr_defss ctr_sugars coiterss' - coiter_defss' lthy; + derive_coinduct_unfold_corec_thms_for_types pre_bnfs xtor_co_iterss' xtor_co_induct + xtor_strong_co_induct dtor_ctors (transpose xtor_co_iter_thmss) nesting_bnfs nested_bnfs + fpTs Cs As kss mss ns ctr_defss ctr_sugars coiterss' coiter_defss' lthy; val coinduct_type_attr = Attrib.internal o K o Induct.coinduct_type; @@ -1404,7 +1403,7 @@ val lthy' = lthy |> fold_map define_ctrs_case_for_type (fp_bnfs ~~ fp_bs ~~ fpTs ~~ Cs ~~ ctors ~~ dtors ~~ - xtor_un_folds ~~ xtor_co_recs ~~ ctor_dtors ~~ dtor_ctors ~~ ctor_injects ~~ pre_map_defs ~~ + (transpose xtor_co_iterss') ~~ ctor_dtors ~~ dtor_ctors ~~ ctor_injects ~~ pre_map_defs ~~ pre_set_defss ~~ pre_rel_defs ~~ xtor_map_thms ~~ xtor_set_thmss ~~ xtor_rel_thms ~~ ns ~~ kss ~~ mss ~~ ctr_bindingss ~~ ctr_mixfixess ~~ ctr_Tsss ~~ disc_bindingss ~~ sel_bindingsss ~~ raw_sel_defaultsss) diff -r 9f14280aa080 -r 2f286a2b7f98 src/HOL/BNF/Tools/bnf_fp_util.ML --- a/src/HOL/BNF/Tools/bnf_fp_util.ML Thu Jun 06 22:01:42 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_fp_util.ML Fri Jun 07 08:48:59 2013 +0200 @@ -15,8 +15,7 @@ bnfs: BNF_Def.bnf list, ctors: term list, dtors: term list, - xtor_un_folds: term list, - xtor_co_recs: term list, + xtor_co_iterss: term list list, xtor_co_induct: thm, xtor_strong_co_induct: thm, dtor_ctors: thm list, @@ -25,8 +24,7 @@ xtor_map_thms: thm list, xtor_set_thmss: thm list list, xtor_rel_thms: thm list, - xtor_un_fold_thms: thm list, - xtor_co_rec_thms: thm list} + xtor_co_iter_thmss: thm list list} val morph_fp_result: morphism -> fp_result -> fp_result val eq_fp_result: fp_result * fp_result -> bool @@ -185,8 +183,7 @@ bnfs: BNF_Def.bnf list, ctors: term list, dtors: term list, - xtor_un_folds: term list, - xtor_co_recs: term list, + xtor_co_iterss: term list list, xtor_co_induct: thm, xtor_strong_co_induct: thm, dtor_ctors: thm list, @@ -195,18 +192,16 @@ xtor_map_thms: thm list, xtor_set_thmss: thm list list, xtor_rel_thms: thm list, - xtor_un_fold_thms: thm list, - xtor_co_rec_thms: thm list}; + xtor_co_iter_thmss: thm list list}; -fun morph_fp_result phi {Ts, bnfs, ctors, dtors, xtor_un_folds, xtor_co_recs, xtor_co_induct, +fun morph_fp_result phi {Ts, bnfs, ctors, dtors, xtor_co_iterss, xtor_co_induct, xtor_strong_co_induct, dtor_ctors, ctor_dtors, ctor_injects, xtor_map_thms, xtor_set_thmss, - xtor_rel_thms, xtor_un_fold_thms, xtor_co_rec_thms} = + xtor_rel_thms, xtor_co_iter_thmss} = {Ts = map (Morphism.typ phi) Ts, bnfs = map (morph_bnf phi) bnfs, ctors = map (Morphism.term phi) ctors, dtors = map (Morphism.term phi) dtors, - xtor_un_folds = map (Morphism.term phi) xtor_un_folds, - xtor_co_recs = map (Morphism.term phi) xtor_co_recs, + xtor_co_iterss = map (map (Morphism.term phi)) xtor_co_iterss, xtor_co_induct = Morphism.thm phi xtor_co_induct, xtor_strong_co_induct = Morphism.thm phi xtor_strong_co_induct, dtor_ctors = map (Morphism.thm phi) dtor_ctors, @@ -215,8 +210,7 @@ xtor_map_thms = map (Morphism.thm phi) xtor_map_thms, xtor_set_thmss = map (map (Morphism.thm phi)) xtor_set_thmss, xtor_rel_thms = map (Morphism.thm phi) xtor_rel_thms, - xtor_un_fold_thms = map (Morphism.thm phi) xtor_un_fold_thms, - xtor_co_rec_thms = map (Morphism.thm phi) xtor_co_rec_thms}; + xtor_co_iter_thmss = map (map (Morphism.thm phi)) xtor_co_iter_thmss}; fun eq_fp_result ({bnfs = bnfs1, ...} : fp_result, {bnfs = bnfs2, ...} : fp_result) = eq_list eq_bnf (bnfs1, bnfs2); diff -r 9f14280aa080 -r 2f286a2b7f98 src/HOL/BNF/Tools/bnf_gfp.ML --- a/src/HOL/BNF/Tools/bnf_gfp.ML Thu Jun 06 22:01:42 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_gfp.ML Fri Jun 07 08:48:59 2013 +0200 @@ -3107,13 +3107,13 @@ bs thmss) in timer; - ({Ts = Ts, bnfs = Jbnfs, ctors = ctors, dtors = dtors, xtor_un_folds = unfolds, - xtor_co_recs = corecs, xtor_co_induct = dtor_coinduct_thm, + ({Ts = Ts, bnfs = Jbnfs, ctors = ctors, dtors = dtors, + xtor_co_iterss = transpose [unfolds, corecs], xtor_co_induct = dtor_coinduct_thm, xtor_strong_co_induct = dtor_strong_coinduct_thm, dtor_ctors = dtor_ctor_thms, ctor_dtors = ctor_dtor_thms, ctor_injects = ctor_inject_thms, xtor_map_thms = folded_dtor_map_thms, xtor_set_thmss = folded_dtor_set_thmss', - xtor_rel_thms = dtor_Jrel_thms, xtor_un_fold_thms = ctor_dtor_unfold_thms, - xtor_co_rec_thms = ctor_dtor_corec_thms}, + xtor_rel_thms = dtor_Jrel_thms, + xtor_co_iter_thmss = transpose [ctor_dtor_unfold_thms, ctor_dtor_corec_thms]}, lthy |> Local_Theory.notes (common_notes @ notes) |> snd) end; diff -r 9f14280aa080 -r 2f286a2b7f98 src/HOL/BNF/Tools/bnf_lfp.ML --- a/src/HOL/BNF/Tools/bnf_lfp.ML Thu Jun 06 22:01:42 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_lfp.ML Fri Jun 07 08:48:59 2013 +0200 @@ -1856,13 +1856,13 @@ bs thmss) in timer; - ({Ts = Ts, bnfs = Ibnfs, ctors = ctors, dtors = dtors, xtor_un_folds = folds, - xtor_co_recs = recs, xtor_co_induct = ctor_induct_thm, + ({Ts = Ts, bnfs = Ibnfs, ctors = ctors, dtors = dtors, xtor_co_iterss = transpose [folds, recs], + xtor_co_induct = ctor_induct_thm, xtor_strong_co_induct = ctor_induct_thm, dtor_ctors = dtor_ctor_thms, ctor_dtors = ctor_dtor_thms, ctor_injects = ctor_inject_thms, xtor_map_thms = folded_ctor_map_thms, xtor_set_thmss = folded_ctor_set_thmss', - xtor_rel_thms = ctor_Irel_thms, xtor_un_fold_thms = ctor_fold_thms, - xtor_co_rec_thms = ctor_rec_thms}, + xtor_rel_thms = ctor_Irel_thms, + xtor_co_iter_thmss = transpose [ctor_fold_thms, ctor_rec_thms]}, lthy |> Local_Theory.notes (common_notes @ notes) |> snd) end;