# HG changeset patch # User blanchet # Date 1370526549 -7200 # Node ID 30d516bbf19fac7d2c50511108b519a92400d67d # Parent 597fcdb7ea64d2749937ad6046037a53e3f73225 tuning diff -r 597fcdb7ea64 -r 30d516bbf19f src/HOL/BNF/Tools/bnf_fp_def_sugar.ML --- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML Thu Jun 06 15:49:09 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML Thu Jun 06 15:49:09 2013 +0200 @@ -52,10 +52,10 @@ (string -> binding) -> typ list -> typ list -> term list -> Proof.context -> (term list * thm list) * Proof.context val define_coiters: term list * term list list - * ((term list list * term list list list list * term list list list list) - * (typ list * typ list list list * typ list list)) - * ((term list list * term list list list list * term list list list list) - * (typ list * typ list list list * typ list list)) -> + * ((term list list * term list list list list * term list list list list) + * (typ list * typ list list list * typ list list)) + * ((term list list * term list list list list * term list list list list) + * (typ list * typ list list list * typ list list)) -> (string -> binding) -> typ list -> typ list -> term list -> Proof.context -> (term list * thm list) * Proof.context val derive_induct_fold_rec_thms_for_types: BNF_Def.bnf list -> term list list -> @@ -65,11 +65,10 @@ thm list list -> local_theory -> (thm * thm list * Args.src list) * (thm list list * Args.src list) * (thm list list * Args.src list) - val derive_coinduct_unfold_corec_thms_for_types: BNF_Def.bnf list -> term list -> term list -> - thm -> thm -> thm list -> thm list -> thm list -> BNF_Def.bnf list -> BNF_Def.bnf list -> - typ list -> typ list -> typ list -> int list list -> int list list -> int list -> - thm list list -> BNF_Ctr_Sugar.ctr_sugar list -> term list list -> thm list list -> - local_theory -> + val derive_coinduct_unfold_corec_thms_for_types: BNF_Def.bnf list -> term list list -> thm -> + thm -> thm list -> thm list list -> BNF_Def.bnf list -> BNF_Def.bnf list -> typ list -> + typ list -> typ list -> int list list -> int list list -> int list -> thm list list -> + BNF_Ctr_Sugar.ctr_sugar list -> term list list -> thm list list -> local_theory -> (thm * thm list * thm * thm list * Args.src list) * (thm list list * thm list list * Args.src list) * (thm list list * thm list list) * (thm list list * thm list list * Args.src list) @@ -360,21 +359,21 @@ ((cs, cpss, (unfold_args, unfold_types), (corec_args, corec_types)), lthy) end; -fun mk_un_fold_co_rec_prelims fp fpTs Cs ns mss xtor_co_iterss0 lthy = +fun mk_un_fold_co_rec_prelims fp fpTs Cs ns mss xtor_co_iterss0' lthy = let val thy = Proof_Context.theory_of lthy; - val (xtor_co_iter_fun_Tss, xtor_co_iterss) = - map (mk_co_iters thy fp fpTs Cs #> `(mk_fp_iter_fun_types o hd)) xtor_co_iterss0 + val (xtor_co_iter_fun_Tss', xtor_co_iterss') = + map (mk_co_iters thy fp fpTs Cs #> `(mk_fp_iter_fun_types o hd)) xtor_co_iterss0' |> split_list; val ((fold_rec_args_types, unfold_corec_args_types), lthy') = if fp = Least_FP then - mk_fold_rec_args_types Cs ns mss xtor_co_iter_fun_Tss lthy |>> (rpair NONE o SOME) + mk_fold_rec_args_types Cs ns mss xtor_co_iter_fun_Tss' lthy |>> (rpair NONE o SOME) else - mk_unfold_corec_args_types Cs ns mss xtor_co_iter_fun_Tss lthy |>> (pair NONE o SOME) + mk_unfold_corec_args_types Cs ns mss xtor_co_iter_fun_Tss' lthy |>> (pair NONE o SOME) in - ((xtor_co_iterss, fold_rec_args_types, unfold_corec_args_types), lthy') + ((xtor_co_iterss', fold_rec_args_types, unfold_corec_args_types), lthy') end; fun mk_map live Ts Us t = @@ -700,9 +699,9 @@ (fold_thmss, code_simp_attrs), (rec_thmss, code_simp_attrs)) end; -fun derive_coinduct_unfold_corec_thms_for_types pre_bnfs dtor_unfolds dtor_corecs dtor_coinduct - dtor_strong_induct dtor_ctors dtor_unfold_thms dtor_corec_thms nesting_bnfs nested_bnfs fpTs Cs - As kss mss ns ctr_defss ctr_sugars [unfolds, corecs] [unfold_defs, corec_defs] lthy = +fun derive_coinduct_unfold_corec_thms_for_types pre_bnfs [dtor_unfolds, dtor_corecs] dtor_coinduct + dtor_strong_induct dtor_ctors [dtor_unfold_thms, dtor_corec_thms] nesting_bnfs nested_bnfs fpTs + Cs As kss mss ns ctr_defss ctr_sugars [unfolds, corecs] [unfold_defs, corec_defs] lthy = let val nn = length pre_bnfs; @@ -948,8 +947,8 @@ coiter_thm RS arg_cong' RS sel_thm' end; - fun mk_sel_coiter_thms coiterss = - map3 (map3 (map2 o mk_sel_coiter_thm)) coiterss selsss sel_thmsss |> map flat; + fun mk_sel_coiter_thms coiter_thmss = + map3 (map3 (map2 o mk_sel_coiter_thm)) coiter_thmss selsss sel_thmsss |> map flat; val sel_unfold_thmss = mk_sel_coiter_thms unfold_thmss; val sel_corec_thmss = mk_sel_coiter_thms corec_thmss; @@ -1335,13 +1334,13 @@ fun derive_and_note_induct_fold_rec_thms_for_types ((((mapsx, rel_injects, rel_distincts, setss), (ctrss, _, ctr_defss, ctr_sugars)), - (iterss, iter_defss)), lthy) = + (iterss', iter_defss')), lthy) = 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; + 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; @@ -1361,13 +1360,13 @@ in lthy |> Local_Theory.notes (common_notes @ notes) |> snd - |> register_fp_sugars Least_FP pre_bnfs fp_res ctr_defss ctr_sugars iterss induct_thm + |> register_fp_sugars Least_FP pre_bnfs fp_res ctr_defss ctr_sugars iterss' induct_thm induct_thm [fold_thmss, rec_thmss] end; fun derive_and_note_coinduct_unfold_corec_thms_for_types ((((mapsx, rel_injects, rel_distincts, setss), (_, _, ctr_defss, ctr_sugars)), - (coiterss, coiter_defss)), lthy) = + (coiterss', coiter_defss')), lthy) = let val ((coinduct_thm, coinduct_thms, strong_coinduct_thm, strong_coinduct_thms, coinduct_attrs), @@ -1376,10 +1375,10 @@ (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_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; val coinduct_type_attr = Attrib.internal o K o Induct.coinduct_type; @@ -1421,8 +1420,8 @@ in lthy |> Local_Theory.notes (anonymous_notes @ common_notes @ notes) |> snd - |> register_fp_sugars Greatest_FP pre_bnfs fp_res ctr_defss ctr_sugars coiterss coinduct_thm - strong_coinduct_thm [unfold_thmss, corec_thmss] + |> register_fp_sugars Greatest_FP pre_bnfs fp_res ctr_defss ctr_sugars coiterss' + coinduct_thm strong_coinduct_thm [unfold_thmss, corec_thmss] end; val lthy' = lthy