# HG changeset patch # User traytel # Date 1377517486 -7200 # Node ID 222ea6acbdd65747fec329fd9e350f461661f25d # Parent 2333fae25719de67d9c1956d6b18538b53cc926d moved derivation of ctor_dtor_unfold to sugar (streamlines fp_result interface) diff -r 2333fae25719 -r 222ea6acbdd6 src/HOL/BNF/Tools/bnf_fp_def_sugar.ML --- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML Mon Aug 26 12:14:41 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML Mon Aug 26 13:44:46 2013 +0200 @@ -70,9 +70,10 @@ val derive_coinduct_coiters_thms_for_types: BNF_Def.bnf list -> string * term list * term list list * ((term list list * term list list list) * (typ list * typ list list)) list -> - thm -> thm list -> thm list 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 -> (thm list -> thm list) -> local_theory -> + thm -> thm list -> thm list -> thm list 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 -> (thm list -> thm list) -> + local_theory -> ((thm list * 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) @@ -727,9 +728,15 @@ fun derive_coinduct_coiters_thms_for_types pre_bnfs (z, cs, cpss, coiters_args_types as [((pgss, crgsss), _), ((phss, cshsss), _)]) - dtor_coinduct dtor_ctors dtor_coiter_thmss nesting_bnfs fpTs Cs As kss mss ns ctr_defss - ctr_sugars coiterss coiter_defss export_args lthy = + dtor_coinduct dtor_injects dtor_ctors dtor_coiter_thmss nesting_bnfs fpTs Cs As kss mss ns + ctr_defss ctr_sugars coiterss coiter_defss export_args lthy = let + fun mk_ctor_dtor_coiter_thm dtor_inject dtor_ctor coiter = + iffD1 OF [dtor_inject, trans OF [coiter, dtor_ctor RS sym]]; + + val ctor_dtor_coiter_thmss = + map3 (map oo mk_ctor_dtor_coiter_thm) dtor_injects dtor_ctors dtor_coiter_thmss; + val coiterss' = transpose coiterss; val coiter_defss' = transpose coiter_defss; @@ -896,10 +903,10 @@ val unfold_tacss = map3 (map oo mk_coiter_tac unfold_defs nesting_map_ids'') - (map un_fold_of dtor_coiter_thmss) pre_map_defs ctr_defss; + (map un_fold_of ctor_dtor_coiter_thmss) pre_map_defs ctr_defss; val corec_tacss = map3 (map oo mk_coiter_tac corec_defs nesting_map_ids'') - (map co_rec_of dtor_coiter_thmss) pre_map_defs ctr_defss; + (map co_rec_of ctor_dtor_coiter_thmss) pre_map_defs ctr_defss; fun prove goal tac = Goal.prove_sorry lthy [] [] goal (tac o #context) @@ -1111,7 +1118,8 @@ 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, dtor_ctors, ctor_dtors, ctor_injects, - xtor_map_thms, xtor_set_thmss, xtor_rel_thms, xtor_co_iter_thmss, ...}, lthy)) = + dtor_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; @@ -1404,8 +1412,8 @@ (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 (the coiters_args_types) xtor_co_induct - dtor_ctors xtor_co_iter_thmss nesting_bnfs fpTs Cs As kss mss ns ctr_defss ctr_sugars - coiterss coiter_defss (Proof_Context.export lthy' no_defs_lthy) lthy; + dtor_injects dtor_ctors xtor_co_iter_thmss nesting_bnfs fpTs Cs As kss mss ns ctr_defss + ctr_sugars coiterss coiter_defss (Proof_Context.export lthy' no_defs_lthy) lthy; val coinduct_type_attr = Attrib.internal o K o Induct.coinduct_type; diff -r 2333fae25719 -r 222ea6acbdd6 src/HOL/BNF/Tools/bnf_fp_util.ML --- a/src/HOL/BNF/Tools/bnf_fp_util.ML Mon Aug 26 12:14:41 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_fp_util.ML Mon Aug 26 13:44:46 2013 +0200 @@ -21,6 +21,7 @@ dtor_ctors: thm list, ctor_dtors: thm list, ctor_injects: thm list, + dtor_injects: thm list, xtor_map_thms: thm list, xtor_set_thmss: thm list list, xtor_rel_thms: thm list, @@ -210,6 +211,7 @@ dtor_ctors: thm list, ctor_dtors: thm list, ctor_injects: thm list, + dtor_injects: thm list, xtor_map_thms: thm list, xtor_set_thmss: thm list list, xtor_rel_thms: thm list, @@ -218,8 +220,8 @@ rel_co_induct_thm: thm}; fun morph_fp_result phi {Ts, bnfs, ctors, dtors, xtor_co_iterss, xtor_co_induct, dtor_ctors, - ctor_dtors, ctor_injects, xtor_map_thms, xtor_set_thmss, xtor_rel_thms, xtor_co_iter_thmss, - xtor_co_iter_o_map_thmss, rel_co_induct_thm} = + ctor_dtors, ctor_injects, dtor_injects, xtor_map_thms, xtor_set_thmss, xtor_rel_thms, + xtor_co_iter_thmss, xtor_co_iter_o_map_thmss, rel_co_induct_thm} = {Ts = map (Morphism.typ phi) Ts, bnfs = map (morph_bnf phi) bnfs, ctors = map (Morphism.term phi) ctors, @@ -229,6 +231,7 @@ dtor_ctors = map (Morphism.thm phi) dtor_ctors, ctor_dtors = map (Morphism.thm phi) ctor_dtors, ctor_injects = map (Morphism.thm phi) ctor_injects, + dtor_injects = map (Morphism.thm phi) dtor_injects, 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, diff -r 2333fae25719 -r 222ea6acbdd6 src/HOL/BNF/Tools/bnf_gfp.ML --- a/src/HOL/BNF/Tools/bnf_gfp.ML Mon Aug 26 12:14:41 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_gfp.ML Mon Aug 26 13:44:46 2013 +0200 @@ -1923,12 +1923,6 @@ val ctor_inject_thms = map (fn thm => thm RS @{thm inj_eq}) inj_ctor_thms; val ctor_exhaust_thms = map (fn thm => thm RS exE) ctor_nchotomy_thms; - fun mk_ctor_dtor_unfold_like_thm dtor_inject dtor_ctor unfold = - iffD1 OF [dtor_inject, trans OF [unfold, dtor_ctor RS sym]]; - - val ctor_dtor_unfold_thms = - map3 mk_ctor_dtor_unfold_like_thm dtor_inject_thms dtor_ctor_thms dtor_unfold_thms; - val timer = time (timer "ctor definitions & thms"); val corec_Inl_sum_thms = @@ -2015,9 +2009,6 @@ |> Local_Defs.unfold lthy (@{thms o_sum_case o_id id_o o_assoc sum_case_o_inj(1)} @ map_ids @ sym_map_comps) OF replicate n @{thm arg_cong2[of _ _ _ _ sum_case, OF refl]}); - val ctor_dtor_corec_thms = - map3 mk_ctor_dtor_unfold_like_thm dtor_inject_thms dtor_ctor_thms dtor_corec_thms; - val timer = time (timer "corec definitions & thms"); val (dtor_map_coinduct_thm, coinduct_params, dtor_coinduct_thm) = @@ -2876,8 +2867,6 @@ val notes = [(ctor_dtorN, ctor_dtor_thms), - (ctor_dtor_corecN, ctor_dtor_corec_thms), - (ctor_dtor_unfoldN, ctor_dtor_unfold_thms), (ctor_exhaustN, ctor_exhaust_thms), (ctor_injectN, ctor_inject_thms), (dtor_corecN, dtor_corec_thms), @@ -2899,10 +2888,11 @@ ({Ts = Ts, bnfs = Jbnfs, ctors = ctors, dtors = dtors, xtor_co_iterss = transpose [unfolds, corecs], xtor_co_induct = dtor_coinduct_thm, dtor_ctors = dtor_ctor_thms, - ctor_dtors = ctor_dtor_thms, ctor_injects = ctor_inject_thms, + ctor_dtors = ctor_dtor_thms, + ctor_injects = ctor_inject_thms, dtor_injects = dtor_inject_thms, xtor_map_thms = folded_dtor_map_thms, xtor_set_thmss = folded_dtor_set_thmss', xtor_rel_thms = dtor_Jrel_thms, - xtor_co_iter_thmss = transpose [ctor_dtor_unfold_thms, ctor_dtor_corec_thms], + xtor_co_iter_thmss = transpose [dtor_unfold_thms, dtor_corec_thms], xtor_co_iter_o_map_thmss = transpose [dtor_unfold_o_map_thms, dtor_corec_o_map_thms], rel_co_induct_thm = Jrel_coinduct_thm}, lthy |> Local_Theory.notes (common_notes @ notes) |> snd) diff -r 2333fae25719 -r 222ea6acbdd6 src/HOL/BNF/Tools/bnf_lfp.ML --- a/src/HOL/BNF/Tools/bnf_lfp.ML Mon Aug 26 12:14:41 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_lfp.ML Mon Aug 26 13:44:46 2013 +0200 @@ -1860,8 +1860,9 @@ timer; ({Ts = Ts, bnfs = Ibnfs, ctors = ctors, dtors = dtors, xtor_co_iterss = transpose [folds, recs], xtor_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, + ctor_injects = ctor_inject_thms, dtor_injects = dtor_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], xtor_co_iter_o_map_thmss = transpose [ctor_fold_o_map_thms, ctor_rec_o_map_thms], rel_co_induct_thm = Irel_induct_thm},