# HG changeset patch # User blanchet # Date 1370599915 -7200 # Node ID ff05e50efa0df4e6552a556f316bb2a5268e497b # Parent a83404aca047540cadf0b540fe6fb279f588ebf4 tuning diff -r a83404aca047 -r ff05e50efa0d src/HOL/BNF/Tools/bnf_fp_def_sugar.ML --- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML Fri Jun 07 12:00:29 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML Fri Jun 07 12:11:55 2013 +0200 @@ -53,7 +53,7 @@ (term list * thm list) * Proof.context val derive_induct_iters_thms_for_types: BNF_Def.bnf list -> term list list -> (typ list list * typ list list list list * term list list * term list list list list) list -> - thm -> thm list list -> BNF_Def.bnf list -> BNF_Def.bnf list -> typ list -> typ list -> + thm list -> thm list list -> BNF_Def.bnf list -> BNF_Def.bnf list -> typ list -> typ list -> typ list -> typ list list list -> term list list -> thm list list -> term list list -> thm list list -> local_theory -> (thm * thm list * Args.src list) * (thm list list * Args.src list) @@ -61,7 +61,7 @@ val derive_coinduct_coiters_thms_for_types: BNF_Def.bnf list -> term list list -> term list * term list list * ((term list list * term list list list list * term list list list list) * 'a) list -> - thm -> thm -> thm list -> thm list list -> BNF_Def.bnf list -> BNF_Def.bnf list -> typ list -> + thm list -> 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) @@ -520,7 +520,7 @@ end; fun derive_induct_iters_thms_for_types pre_bnfs (ctor_iters1 :: _) [fold_args_types, rec_args_types] - ctor_induct ctor_iter_thmss nesting_bnfs nested_bnfs fpTs Cs Xs ctrXs_Tsss ctrss ctr_defss + [ctor_induct] ctor_iter_thmss nesting_bnfs nested_bnfs fpTs Cs Xs ctrXs_Tsss ctrss ctr_defss iterss iter_defss lthy = let val iterss' = transpose iterss; @@ -682,8 +682,8 @@ fun derive_coinduct_coiters_thms_for_types pre_bnfs (dtor_coiters1 :: _) (cs, cpss, [(unfold_args as (pgss, crssss, cgssss), _), (corec_args as (phss, csssss, chssss), _)]) - dtor_coinduct dtor_strong_induct dtor_ctors dtor_coiter_thmss nesting_bnfs nested_bnfs fpTs Cs - As kss mss ns ctr_defss ctr_sugars coiterss coiter_defss lthy = + dtor_coinducts dtor_ctors dtor_coiter_thmss nesting_bnfs nested_bnfs fpTs Cs As kss mss ns + ctr_defss ctr_sugars coiterss coiter_defss lthy = let val coiterss' = transpose coiterss; val coiter_defss' = transpose coiter_defss; @@ -794,7 +794,8 @@ |> Drule.zero_var_indexes |> `(conj_dests nn); in - (postproc nn (prove dtor_coinduct goal), postproc nn (prove dtor_strong_induct strong_goal)) + (postproc nn (prove (co_induct_of dtor_coinducts) goal), + postproc nn (prove (strong_co_induct_of dtor_coinducts) strong_goal)) end; fun mk_coinduct_concls ms discs ctrs = @@ -1057,9 +1058,8 @@ 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_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)) = + xtor_co_iterss = xtor_co_iterss0, xtor_co_inducts, 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; @@ -1324,7 +1324,7 @@ val ((induct_thm, induct_thms, induct_attrs), (fold_thmss, fold_attrs), (rec_thmss, rec_attrs)) = derive_induct_iters_thms_for_types pre_bnfs xtor_co_iterss (the iters_args_types) - xtor_co_induct xtor_co_iter_thmss nesting_bnfs nested_bnfs fpTs Cs Xs ctrXs_Tsss ctrss + xtor_co_inducts 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; @@ -1360,10 +1360,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_coiters_thms_for_types pre_bnfs xtor_co_iterss - (the coiters_args_types) xtor_co_induct xtor_strong_co_induct dtor_ctors - xtor_co_iter_thmss nesting_bnfs nested_bnfs fpTs Cs As kss mss ns ctr_defss ctr_sugars - coiterss coiter_defss lthy; + derive_coinduct_coiters_thms_for_types pre_bnfs xtor_co_iterss (the coiters_args_types) + xtor_co_inducts dtor_ctors 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; diff -r a83404aca047 -r ff05e50efa0d src/HOL/BNF/Tools/bnf_fp_util.ML --- a/src/HOL/BNF/Tools/bnf_fp_util.ML Fri Jun 07 12:00:29 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_fp_util.ML Fri Jun 07 12:11:55 2013 +0200 @@ -16,8 +16,7 @@ ctors: term list, dtors: term list, xtor_co_iterss: term list list, - xtor_co_induct: thm, - xtor_strong_co_induct: thm, + xtor_co_inducts: thm list, dtor_ctors: thm list, ctor_dtors: thm list, ctor_injects: thm list, @@ -28,7 +27,7 @@ val morph_fp_result: morphism -> fp_result -> fp_result val eq_fp_result: fp_result * fp_result -> bool - val weak_co_induct_of: 'a list -> 'a + val co_induct_of: 'a list -> 'a val strong_co_induct_of: 'a list -> 'a val un_fold_of: 'a list -> 'a val co_rec_of: 'a list -> 'a @@ -188,8 +187,7 @@ ctors: term list, dtors: term list, xtor_co_iterss: term list list, - xtor_co_induct: thm, - xtor_strong_co_induct: thm, + xtor_co_inducts: thm list, dtor_ctors: thm list, ctor_dtors: thm list, ctor_injects: thm list, @@ -198,16 +196,14 @@ xtor_rel_thms: thm list, xtor_co_iter_thmss: thm list list}; -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_co_iter_thmss} = +fun morph_fp_result phi {Ts, bnfs, ctors, dtors, xtor_co_iterss, xtor_co_inducts, dtor_ctors, + ctor_dtors, ctor_injects, xtor_map_thms, xtor_set_thmss, 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_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, + xtor_co_inducts = map (Morphism.thm phi) xtor_co_inducts, dtor_ctors = map (Morphism.thm phi) dtor_ctors, ctor_dtors = map (Morphism.thm phi) ctor_dtors, ctor_injects = map (Morphism.thm phi) ctor_injects, @@ -219,7 +215,7 @@ fun eq_fp_result ({bnfs = bnfs1, ...} : fp_result, {bnfs = bnfs2, ...} : fp_result) = eq_list eq_bnf (bnfs1, bnfs2); -fun weak_co_induct_of [w, _] = w; +fun co_induct_of (i :: _) = i; fun strong_co_induct_of [_, s] = s; fun un_fold_of [f, _] = f; diff -r a83404aca047 -r ff05e50efa0d src/HOL/BNF/Tools/bnf_gfp.ML --- a/src/HOL/BNF/Tools/bnf_gfp.ML Fri Jun 07 12:00:29 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_gfp.ML Fri Jun 07 12:11:55 2013 +0200 @@ -3108,8 +3108,8 @@ in timer; ({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, + xtor_co_iterss = transpose [unfolds, corecs], + xtor_co_inducts = [dtor_coinduct_thm, 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, diff -r a83404aca047 -r ff05e50efa0d src/HOL/BNF/Tools/bnf_lfp.ML --- a/src/HOL/BNF/Tools/bnf_lfp.ML Fri Jun 07 12:00:29 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_lfp.ML Fri Jun 07 12:11:55 2013 +0200 @@ -1857,11 +1857,9 @@ in timer; ({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_co_inducts = [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_co_iter_thmss = transpose [ctor_fold_thms, ctor_rec_thms]}, lthy |> Local_Theory.notes (common_notes @ notes) |> snd) end;