# HG changeset patch # User blanchet # Date 1459159547 -7200 # Node ID f3248e77c96023365327b07c05cbc11d2d51652b # Parent 2ceae1e761bd75ce88d4e67915080fa8c825d458 added '_legacy' suffixes diff -r 2ceae1e761bd -r f3248e77c960 src/HOL/Tools/BNF/bnf_fp_n2m.ML --- a/src/HOL/Tools/BNF/bnf_fp_n2m.ML Mon Mar 28 12:05:47 2016 +0200 +++ b/src/HOL/Tools/BNF/bnf_fp_n2m.ML Mon Mar 28 12:05:47 2016 +0200 @@ -518,7 +518,7 @@ val fp_res = ({Ts = fpTs, bnfs = of_fp_res #bnfs, pre_bnfs = bnfs, absT_infos = absT_infos, dtors = dtors, ctors = ctors, - xtor_un_folds = xtor_co_recs (*wrong*), xtor_co_recs = xtor_co_recs, + xtor_un_folds_legacy = xtor_co_recs (*wrong*), xtor_co_recs = xtor_co_recs, xtor_co_induct = xtor_co_induct_thm, dtor_ctors = of_fp_res #dtor_ctors (*too general types*), ctor_dtors = of_fp_res #ctor_dtors (*too general types*), @@ -527,12 +527,12 @@ xtor_maps = of_fp_res #xtor_maps (*too general types and terms*), xtor_map_uniques = [], xtor_setss = of_fp_res #xtor_setss (*too general types and terms*), xtor_rels = of_fp_res #xtor_rels (*too general types and terms*), - xtor_un_fold_thms = xtor_co_rec_thms (*wrong*), + xtor_un_fold_thms_legacy = xtor_co_rec_thms (*wrong*), xtor_co_rec_thms = xtor_co_rec_thms (*too general types and terms*), - xtor_un_fold_uniques = [], xtor_co_rec_uniques = [], - xtor_un_fold_o_maps = fp_rec_o_maps (*wrong*), + xtor_un_fold_uniques_legacy = [], xtor_co_rec_uniques = [], + xtor_un_fold_o_maps_legacy = fp_rec_o_maps (*wrong*), xtor_co_rec_o_maps = fp_rec_o_maps (*theorems about old constants*), - xtor_un_fold_transfers = [], xtor_co_rec_transfers = [], + xtor_un_fold_transfers_legacy = [], xtor_co_rec_transfers = [], xtor_rel_co_induct = xtor_rel_co_induct, dtor_set_inducts = []} |> morph_fp_result (Morphism.term_morphism "BNF" (singleton (Variable.polymorphic lthy)))); in diff -r 2ceae1e761bd -r f3248e77c960 src/HOL/Tools/BNF/bnf_fp_util.ML --- a/src/HOL/Tools/BNF/bnf_fp_util.ML Mon Mar 28 12:05:47 2016 +0200 +++ b/src/HOL/Tools/BNF/bnf_fp_util.ML Mon Mar 28 12:05:47 2016 +0200 @@ -17,7 +17,7 @@ absT_infos: BNF_Comp.absT_info list, ctors: term list, dtors: term list, - xtor_un_folds: term list, + xtor_un_folds_legacy: term list, xtor_co_recs: term list, xtor_co_induct: thm, dtor_ctors: thm list, @@ -28,13 +28,13 @@ xtor_map_uniques: thm list, xtor_setss: thm list list, xtor_rels: thm list, - xtor_un_fold_thms: thm list, + xtor_un_fold_thms_legacy: thm list, xtor_co_rec_thms: thm list, - xtor_un_fold_uniques: thm list, + xtor_un_fold_uniques_legacy: thm list, xtor_co_rec_uniques: thm list, - xtor_un_fold_o_maps: thm list, + xtor_un_fold_o_maps_legacy: thm list, xtor_co_rec_o_maps: thm list, - xtor_un_fold_transfers: thm list, + xtor_un_fold_transfers_legacy: thm list, xtor_co_rec_transfers: thm list, xtor_rel_co_induct: thm, dtor_set_inducts: thm list} @@ -220,7 +220,7 @@ absT_infos: BNF_Comp.absT_info list, ctors: term list, dtors: term list, - xtor_un_folds: term list, + xtor_un_folds_legacy: term list, xtor_co_recs: term list, xtor_co_induct: thm, dtor_ctors: thm list, @@ -231,29 +231,30 @@ xtor_map_uniques: thm list, xtor_setss: thm list list, xtor_rels: thm list, - xtor_un_fold_thms: thm list, + xtor_un_fold_thms_legacy: thm list, xtor_co_rec_thms: thm list, - xtor_un_fold_uniques: thm list, + xtor_un_fold_uniques_legacy: thm list, xtor_co_rec_uniques: thm list, - xtor_un_fold_o_maps: thm list, + xtor_un_fold_o_maps_legacy: thm list, xtor_co_rec_o_maps: thm list, - xtor_un_fold_transfers: thm list, + xtor_un_fold_transfers_legacy: thm list, xtor_co_rec_transfers: thm list, xtor_rel_co_induct: thm, dtor_set_inducts: thm list}; -fun morph_fp_result phi {Ts, bnfs, pre_bnfs, absT_infos, ctors, dtors, xtor_un_folds, xtor_co_recs, - xtor_co_induct, dtor_ctors, ctor_dtors, ctor_injects, dtor_injects, xtor_maps, xtor_map_uniques, - xtor_setss, xtor_rels, xtor_un_fold_thms, xtor_co_rec_thms, xtor_un_fold_uniques, - xtor_co_rec_uniques, xtor_un_fold_o_maps, xtor_co_rec_o_maps, xtor_un_fold_transfers, - xtor_co_rec_transfers, xtor_rel_co_induct, dtor_set_inducts} = +fun morph_fp_result phi {Ts, bnfs, pre_bnfs, absT_infos, ctors, dtors, xtor_un_folds_legacy, + xtor_co_recs, xtor_co_induct, dtor_ctors, ctor_dtors, ctor_injects, dtor_injects, xtor_maps, + xtor_map_uniques, xtor_setss, xtor_rels, xtor_un_fold_thms_legacy, xtor_co_rec_thms, + xtor_un_fold_uniques_legacy, xtor_co_rec_uniques, xtor_un_fold_o_maps_legacy, + xtor_co_rec_o_maps, xtor_un_fold_transfers_legacy, xtor_co_rec_transfers, xtor_rel_co_induct, + dtor_set_inducts} = {Ts = map (Morphism.typ phi) Ts, bnfs = map (morph_bnf phi) bnfs, pre_bnfs = map (morph_bnf phi) pre_bnfs, absT_infos = map (morph_absT_info phi) absT_infos, ctors = map (Morphism.term phi) ctors, dtors = map (Morphism.term phi) dtors, - xtor_un_folds = map (Morphism.term phi) xtor_un_folds, + xtor_un_folds_legacy = map (Morphism.term phi) xtor_un_folds_legacy, xtor_co_recs = map (Morphism.term phi) xtor_co_recs, xtor_co_induct = Morphism.thm phi xtor_co_induct, dtor_ctors = map (Morphism.thm phi) dtor_ctors, @@ -264,13 +265,13 @@ xtor_map_uniques = map (Morphism.thm phi) xtor_map_uniques, xtor_setss = map (map (Morphism.thm phi)) xtor_setss, xtor_rels = map (Morphism.thm phi) xtor_rels, - xtor_un_fold_thms = map (Morphism.thm phi) xtor_un_fold_thms, + xtor_un_fold_thms_legacy = map (Morphism.thm phi) xtor_un_fold_thms_legacy, xtor_co_rec_thms = map (Morphism.thm phi) xtor_co_rec_thms, - xtor_un_fold_uniques = map (Morphism.thm phi) xtor_un_fold_uniques, + xtor_un_fold_uniques_legacy = map (Morphism.thm phi) xtor_un_fold_uniques_legacy, xtor_co_rec_uniques = map (Morphism.thm phi) xtor_co_rec_uniques, - xtor_un_fold_o_maps = map (Morphism.thm phi) xtor_un_fold_o_maps, + xtor_un_fold_o_maps_legacy = map (Morphism.thm phi) xtor_un_fold_o_maps_legacy, xtor_co_rec_o_maps = map (Morphism.thm phi) xtor_co_rec_o_maps, - xtor_un_fold_transfers = map (Morphism.thm phi) xtor_un_fold_transfers, + xtor_un_fold_transfers_legacy = map (Morphism.thm phi) xtor_un_fold_transfers_legacy, xtor_co_rec_transfers = map (Morphism.thm phi) xtor_co_rec_transfers, xtor_rel_co_induct = Morphism.thm phi xtor_rel_co_induct, dtor_set_inducts = map (Morphism.thm phi) dtor_set_inducts}; diff -r 2ceae1e761bd -r f3248e77c960 src/HOL/Tools/BNF/bnf_gfp.ML --- a/src/HOL/Tools/BNF/bnf_gfp.ML Mon Mar 28 12:05:47 2016 +0200 +++ b/src/HOL/Tools/BNF/bnf_gfp.ML Mon Mar 28 12:05:47 2016 +0200 @@ -2693,15 +2693,16 @@ val fp_res = {Ts = Ts, bnfs = Jbnfs, pre_bnfs = bnfs, absT_infos = absT_infos, - ctors = ctors, dtors = dtors, xtor_un_folds = unfolds, xtor_co_recs = corecs, + ctors = ctors, dtors = dtors, xtor_un_folds_legacy = unfolds, xtor_co_recs = corecs, xtor_co_induct = dtor_coinduct_thm, dtor_ctors = dtor_ctor_thms, ctor_dtors = ctor_dtor_thms, ctor_injects = ctor_inject_thms, dtor_injects = dtor_inject_thms, xtor_maps = dtor_Jmap_thms, xtor_map_uniques = dtor_Jmap_unique_thms, xtor_setss = dtor_Jset_thmss', - xtor_rels = dtor_Jrel_thms, xtor_un_fold_thms = dtor_unfold_thms, - xtor_co_rec_thms = dtor_corec_thms, xtor_un_fold_uniques = dtor_unfold_unique_thms, - xtor_co_rec_uniques = dtor_corec_unique_thms, xtor_un_fold_o_maps = dtor_unfold_o_Jmap_thms, + xtor_rels = dtor_Jrel_thms, xtor_un_fold_thms_legacy = dtor_unfold_thms, + xtor_co_rec_thms = dtor_corec_thms, xtor_un_fold_uniques_legacy = dtor_unfold_unique_thms, + xtor_co_rec_uniques = dtor_corec_unique_thms, + xtor_un_fold_o_maps_legacy = dtor_unfold_o_Jmap_thms, xtor_co_rec_o_maps = dtor_corec_o_Jmap_thms, - xtor_un_fold_transfers = dtor_unfold_transfer_thms, + xtor_un_fold_transfers_legacy = dtor_unfold_transfer_thms, xtor_co_rec_transfers = dtor_corec_transfer_thms, xtor_rel_co_induct = Jrel_coinduct_thm, dtor_set_inducts = dtor_Jset_induct_thms}; in diff -r 2ceae1e761bd -r f3248e77c960 src/HOL/Tools/BNF/bnf_gfp_grec.ML --- a/src/HOL/Tools/BNF/bnf_gfp_grec.ML Mon Mar 28 12:05:47 2016 +0200 +++ b/src/HOL/Tools/BNF/bnf_gfp_grec.ML Mon Mar 28 12:05:47 2016 +0200 @@ -2135,7 +2135,7 @@ val dead_pre_map = mk_map1 lthy Y Z preT dead_pre_bnf; val fp_rel = mk_relN lthy live_EsFs fpT fp_bnf; val dtor_unfold = mk_co_rec (Proof_Context.theory_of lthy) Greatest_FP [Z] fpT - (the_single (#xtor_un_folds fp_res)); + (the_single (#xtor_un_folds_legacy fp_res)); val Sig = mk_ctr As (the_single (#ctrs sig_ctr_sugar)); val unsig = mk_disc_or_sel As (the_single (the_single (#selss sig_ctr_sugar))); val sig_rel = mk_relN lthy live_AsBs sig_T sig_bnf; @@ -2160,9 +2160,9 @@ val [ctor_dtor] = #ctor_dtors fp_res; val [dtor_ctor] = #dtor_ctors fp_res; val [dtor_inject] = #dtor_injects fp_res; - val [dtor_unfold_thm] = #xtor_un_fold_thms fp_res; - val [dtor_unfold_unique] = #xtor_un_fold_uniques fp_res; - val [dtor_unfold_transfer] = #xtor_un_fold_transfers fp_res; + val [dtor_unfold_thm] = #xtor_un_fold_thms_legacy fp_res; + val [dtor_unfold_unique] = #xtor_un_fold_uniques_legacy fp_res; + val [dtor_unfold_transfer] = #xtor_un_fold_transfers_legacy fp_res; val [dtor_rel_thm] = #xtor_rels fp_res; val unsig_thm = the_single (the_single (#sel_thmss sig_ctr_sugar)); val [sig_map_thm] = #map_thms sig_fp_bnf_sugar; @@ -2370,7 +2370,7 @@ val dead_pre_rel = mk_rel1 lthy Y Z preT dead_pre_bnf; val fp_rel = mk_relN lthy live_EsFs fpT fp_bnf; val dtor_unfold = mk_co_rec (Proof_Context.theory_of lthy) Greatest_FP [Z] fpT - (the_single (#xtor_un_folds fp_res)); + (the_single (#xtor_un_folds_legacy fp_res)); val dead_k_map = mk_map1 lthy Y Z k_T dead_k_bnf; val Sig = mk_ctr res_As (the_single (#ctrs sig_ctr_sugar)); val unsig = mk_disc_or_sel res_As (the_single (the_single (#selss sig_ctr_sugar))); @@ -2412,9 +2412,9 @@ val fp_rel_eq = rel_eq_of_bnf fp_bnf; val [ctor_dtor] = #ctor_dtors fp_res; val [dtor_inject] = #dtor_injects fp_res; - val [dtor_unfold_thm] = #xtor_un_fold_thms fp_res; - val [dtor_unfold_unique] = #xtor_un_fold_uniques fp_res; - val [dtor_unfold_transfer] = #xtor_un_fold_transfers fp_res; + val [dtor_unfold_thm] = #xtor_un_fold_thms_legacy fp_res; + val [dtor_unfold_unique] = #xtor_un_fold_uniques_legacy fp_res; + val [dtor_unfold_transfer] = #xtor_un_fold_transfers_legacy fp_res; val fp_k_T_rel_eqs = map rel_eq_of_bnf (map_filter (bnf_of lthy) (fold add_type_namesT [fpT, k_T] [])); val unsig_thm = the_single (the_single (#sel_thmss sig_ctr_sugar)); @@ -2713,7 +2713,7 @@ val dead_pre_rel = mk_rel1 lthy Y Z preT dead_pre_bnf; val fp_rel = mk_relN lthy live_EsFs fpT fp_bnf; val dtor_unfold = mk_co_rec (Proof_Context.theory_of lthy) Greatest_FP [Z] fpT - (the_single (#xtor_un_folds fp_res)); + (the_single (#xtor_un_folds_legacy fp_res)); val Sig = mk_ctr res_As (the_single (#ctrs sig_ctr_sugar)); val unsig = mk_disc_or_sel res_As (the_single (the_single (#selss sig_ctr_sugar))); val sig_rel = mk_relN lthy live_AsBs sig_T sig_bnf; @@ -2764,9 +2764,9 @@ val fp_rel_eq = rel_eq_of_bnf fp_bnf; val [ctor_dtor] = #ctor_dtors fp_res; val [dtor_inject] = #dtor_injects fp_res; - val [dtor_unfold_thm] = #xtor_un_fold_thms fp_res; - val [dtor_unfold_unique] = #xtor_un_fold_uniques fp_res; - val [dtor_unfold_transfer] = #xtor_un_fold_transfers fp_res; + val [dtor_unfold_thm] = #xtor_un_fold_thms_legacy fp_res; + val [dtor_unfold_unique] = #xtor_un_fold_uniques_legacy fp_res; + val [dtor_unfold_transfer] = #xtor_un_fold_transfers_legacy fp_res; val unsig_thm = the_single (the_single (#sel_thmss sig_ctr_sugar)); val [sig_map_thm] = #map_thms sig_fp_bnf_sugar; val old1_sig_map_comp = map_comp_of_bnf old1_sig_bnf; diff -r 2ceae1e761bd -r f3248e77c960 src/HOL/Tools/BNF/bnf_lfp.ML --- a/src/HOL/Tools/BNF/bnf_lfp.ML Mon Mar 28 12:05:47 2016 +0200 +++ b/src/HOL/Tools/BNF/bnf_lfp.ML Mon Mar 28 12:05:47 2016 +0200 @@ -1952,15 +1952,17 @@ val fp_res = {Ts = Ts, bnfs = Ibnfs, pre_bnfs = bnfs, absT_infos = absT_infos, - ctors = ctors, dtors = dtors, xtor_un_folds = folds, xtor_co_recs = recs, + ctors = ctors, dtors = dtors, xtor_un_folds_legacy = folds, xtor_co_recs = recs, xtor_co_induct = ctor_induct_thm, dtor_ctors = dtor_ctor_thms, ctor_dtors = ctor_dtor_thms, ctor_injects = ctor_inject_thms, dtor_injects = dtor_inject_thms, xtor_maps = ctor_Imap_thms, xtor_map_uniques = ctor_Imap_unique_thms, xtor_setss = ctor_Iset_thmss', - xtor_rels = ctor_Irel_thms, xtor_un_fold_thms = ctor_fold_thms, - xtor_co_rec_thms = ctor_rec_thms, xtor_un_fold_uniques = ctor_fold_unique_thms, - xtor_co_rec_uniques = ctor_rec_unique_thms, xtor_un_fold_o_maps = ctor_fold_o_Imap_thms, - xtor_co_rec_o_maps = ctor_rec_o_Imap_thms, xtor_un_fold_transfers = ctor_fold_transfer_thms, + xtor_rels = ctor_Irel_thms, xtor_un_fold_thms_legacy = ctor_fold_thms, + xtor_co_rec_thms = ctor_rec_thms, xtor_un_fold_uniques_legacy = ctor_fold_unique_thms, + xtor_co_rec_uniques = ctor_rec_unique_thms, + xtor_un_fold_o_maps_legacy = ctor_fold_o_Imap_thms, + xtor_co_rec_o_maps = ctor_rec_o_Imap_thms, + xtor_un_fold_transfers_legacy = ctor_fold_transfer_thms, xtor_co_rec_transfers = ctor_rec_transfer_thms, xtor_rel_co_induct = Irel_induct_thm, dtor_set_inducts = []}; in diff -r 2ceae1e761bd -r f3248e77c960 src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML --- a/src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML Mon Mar 28 12:05:47 2016 +0200 +++ b/src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML Mon Mar 28 12:05:47 2016 +0200 @@ -35,15 +35,15 @@ val co_rec_thms = [map_id0_of_bnf fp_bnf RS @{thm ctor_rec}]; in {Ts = [fpT], bnfs = [fp_bnf], pre_bnfs = [ID_bnf], absT_infos = [trivial_absT_info_of fpT], - ctors = xtors, dtors = xtors, xtor_un_folds = co_recs, + ctors = xtors, dtors = xtors, xtor_un_folds_legacy = co_recs, xtor_co_recs = co_recs, xtor_co_induct = @{thm xtor_induct}, dtor_ctors = @{thms xtor_xtor}, ctor_dtors = @{thms xtor_xtor}, ctor_injects = @{thms xtor_inject}, dtor_injects = @{thms xtor_inject}, xtor_maps = [xtor_map], xtor_map_uniques = [], - xtor_setss = [xtor_sets], xtor_rels = [xtor_rel], xtor_un_fold_thms = co_rec_thms, - xtor_co_rec_thms = co_rec_thms, xtor_un_fold_uniques = [], xtor_co_rec_uniques = [], - xtor_un_fold_o_maps = [ctor_rec_o_map], xtor_co_rec_o_maps = [ctor_rec_o_map], - xtor_un_fold_transfers = [], xtor_co_rec_transfers = [], xtor_rel_co_induct = xtor_rel_induct, - dtor_set_inducts = []} + xtor_setss = [xtor_sets], xtor_rels = [xtor_rel], xtor_un_fold_thms_legacy = co_rec_thms, + xtor_co_rec_thms = co_rec_thms, xtor_un_fold_uniques_legacy = [], xtor_co_rec_uniques = [], + xtor_un_fold_o_maps_legacy = [ctor_rec_o_map], xtor_co_rec_o_maps = [ctor_rec_o_map], + xtor_un_fold_transfers_legacy = [], xtor_co_rec_transfers = [], + xtor_rel_co_induct = xtor_rel_induct, dtor_set_inducts = []} end; fun fp_sugar_of_sum ctxt =