# HG changeset patch # User traytel # Date 1460044586 -7200 # Node ID 9ad0bac25a84688a5349875add284f8a25496b7b # Parent 75ca185db27f90a9ccfc4333f9da611e301767bc (un)folds are not legacy diff -r 75ca185db27f -r 9ad0bac25a84 src/HOL/Tools/BNF/bnf_fp_n2m.ML --- a/src/HOL/Tools/BNF/bnf_fp_n2m.ML Thu Apr 07 17:56:26 2016 +0200 +++ b/src/HOL/Tools/BNF/bnf_fp_n2m.ML Thu Apr 07 17:56:26 2016 +0200 @@ -512,7 +512,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_legacy = xtor_co_recs (*wrong*), xtor_co_recs = xtor_co_recs, + xtor_un_folds = 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*), @@ -522,13 +522,13 @@ xtor_map_unique = TrueI (*wrong*), 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_legacy = xtor_co_rec_thms (*wrong*), + xtor_un_fold_thms = xtor_co_rec_thms (*wrong*), xtor_co_rec_thms = xtor_co_rec_thms (*too general types and terms*), - xtor_un_fold_unique_legacy = TrueI (*too general types and terms*), + xtor_un_fold_unique = TrueI (*too general types and terms*), xtor_co_rec_unique = TrueI (*wrong*), - xtor_un_fold_o_maps_legacy = fp_rec_o_maps (*wrong*), + xtor_un_fold_o_maps = fp_rec_o_maps (*wrong*), xtor_co_rec_o_maps = fp_rec_o_maps (*theorems about old constants*), - xtor_un_fold_transfers_legacy = [], xtor_co_rec_transfers = [], + xtor_un_fold_transfers = [], 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 75ca185db27f -r 9ad0bac25a84 src/HOL/Tools/BNF/bnf_fp_util.ML --- a/src/HOL/Tools/BNF/bnf_fp_util.ML Thu Apr 07 17:56:26 2016 +0200 +++ b/src/HOL/Tools/BNF/bnf_fp_util.ML Thu Apr 07 17:56:26 2016 +0200 @@ -17,7 +17,7 @@ absT_infos: BNF_Comp.absT_info list, ctors: term list, dtors: term list, - xtor_un_folds_legacy: term list, + xtor_un_folds: term list, xtor_co_recs: term list, xtor_co_induct: thm, dtor_ctors: thm list, @@ -28,13 +28,13 @@ xtor_map_unique: thm, xtor_setss: thm list list, xtor_rels: thm list, - xtor_un_fold_thms_legacy: thm list, + xtor_un_fold_thms: thm list, xtor_co_rec_thms: thm list, - xtor_un_fold_unique_legacy: thm, + xtor_un_fold_unique: thm, xtor_co_rec_unique: thm, - xtor_un_fold_o_maps_legacy: thm list, + xtor_un_fold_o_maps: thm list, xtor_co_rec_o_maps: thm list, - xtor_un_fold_transfers_legacy: thm list, + xtor_un_fold_transfers: thm list, xtor_co_rec_transfers: thm list, xtor_rel_co_induct: thm, dtor_set_inducts: thm list} @@ -228,7 +228,7 @@ absT_infos: BNF_Comp.absT_info list, ctors: term list, dtors: term list, - xtor_un_folds_legacy: term list, + xtor_un_folds: term list, xtor_co_recs: term list, xtor_co_induct: thm, dtor_ctors: thm list, @@ -239,22 +239,22 @@ xtor_map_unique: thm, xtor_setss: thm list list, xtor_rels: thm list, - xtor_un_fold_thms_legacy: thm list, + xtor_un_fold_thms: thm list, xtor_co_rec_thms: thm list, - xtor_un_fold_unique_legacy: thm, + xtor_un_fold_unique: thm, xtor_co_rec_unique: thm, - xtor_un_fold_o_maps_legacy: thm list, + xtor_un_fold_o_maps: thm list, xtor_co_rec_o_maps: thm list, - xtor_un_fold_transfers_legacy: thm list, + xtor_un_fold_transfers: 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_legacy, +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_unique, xtor_setss, xtor_rels, xtor_un_fold_thms_legacy, xtor_co_rec_thms, - xtor_un_fold_unique_legacy, xtor_co_rec_unique, xtor_un_fold_o_maps_legacy, - xtor_co_rec_o_maps, xtor_un_fold_transfers_legacy, xtor_co_rec_transfers, xtor_rel_co_induct, + xtor_map_unique, xtor_setss, xtor_rels, xtor_un_fold_thms, xtor_co_rec_thms, + xtor_un_fold_unique, xtor_co_rec_unique, 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} = {Ts = map (Morphism.typ phi) Ts, bnfs = map (morph_bnf phi) bnfs, @@ -262,7 +262,7 @@ absT_infos = map (morph_absT_info phi) absT_infos, ctors = map (Morphism.term phi) ctors, dtors = map (Morphism.term phi) dtors, - xtor_un_folds_legacy = map (Morphism.term phi) xtor_un_folds_legacy, + xtor_un_folds = map (Morphism.term phi) xtor_un_folds, 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, @@ -273,13 +273,13 @@ xtor_map_unique = Morphism.thm phi xtor_map_unique, xtor_setss = map (map (Morphism.thm phi)) xtor_setss, xtor_rels = map (Morphism.thm phi) xtor_rels, - xtor_un_fold_thms_legacy = map (Morphism.thm phi) xtor_un_fold_thms_legacy, + 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_un_fold_unique_legacy = Morphism.thm phi xtor_un_fold_unique_legacy, + xtor_un_fold_unique = Morphism.thm phi xtor_un_fold_unique, xtor_co_rec_unique = Morphism.thm phi xtor_co_rec_unique, - xtor_un_fold_o_maps_legacy = map (Morphism.thm phi) xtor_un_fold_o_maps_legacy, + xtor_un_fold_o_maps = map (Morphism.thm phi) xtor_un_fold_o_maps, xtor_co_rec_o_maps = map (Morphism.thm phi) xtor_co_rec_o_maps, - xtor_un_fold_transfers_legacy = map (Morphism.thm phi) xtor_un_fold_transfers_legacy, + xtor_un_fold_transfers = map (Morphism.thm phi) xtor_un_fold_transfers, 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 75ca185db27f -r 9ad0bac25a84 src/HOL/Tools/BNF/bnf_gfp.ML --- a/src/HOL/Tools/BNF/bnf_gfp.ML Thu Apr 07 17:56:26 2016 +0200 +++ b/src/HOL/Tools/BNF/bnf_gfp.ML Thu Apr 07 17:56:26 2016 +0200 @@ -2616,16 +2616,16 @@ val fp_res = {Ts = Ts, bnfs = Jbnfs, pre_bnfs = bnfs, absT_infos = absT_infos, - ctors = ctors, dtors = dtors, xtor_un_folds_legacy = unfolds, xtor_co_recs = export corecs, + ctors = ctors, dtors = dtors, xtor_un_folds = unfolds, xtor_co_recs = export 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_unique = dtor_Jmap_unique_thm, xtor_setss = dtor_Jset_thmss', - xtor_rels = dtor_Jrel_thms, xtor_un_fold_thms_legacy = dtor_unfold_thms, - xtor_co_rec_thms = dtor_corec_thms, xtor_un_fold_unique_legacy = dtor_unfold_unique_thm, + xtor_rels = dtor_Jrel_thms, xtor_un_fold_thms = dtor_unfold_thms, + xtor_co_rec_thms = dtor_corec_thms, xtor_un_fold_unique = dtor_unfold_unique_thm, xtor_co_rec_unique = dtor_corec_unique_thm, - xtor_un_fold_o_maps_legacy = dtor_unfold_o_Jmap_thms, + xtor_un_fold_o_maps = dtor_unfold_o_Jmap_thms, xtor_co_rec_o_maps = dtor_corec_o_Jmap_thms, - xtor_un_fold_transfers_legacy = dtor_unfold_transfer_thms, + xtor_un_fold_transfers = 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 75ca185db27f -r 9ad0bac25a84 src/HOL/Tools/BNF/bnf_gfp_grec.ML --- a/src/HOL/Tools/BNF/bnf_gfp_grec.ML Thu Apr 07 17:56:26 2016 +0200 +++ b/src/HOL/Tools/BNF/bnf_gfp_grec.ML Thu Apr 07 17:56:26 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_legacy fp_res)); + (the_single (#xtor_un_folds 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; @@ -2159,9 +2159,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_legacy fp_res; - val dtor_unfold_unique = #xtor_un_fold_unique_legacy fp_res; - val [dtor_unfold_transfer] = #xtor_un_fold_transfers_legacy fp_res; + val [dtor_unfold_thm] = #xtor_un_fold_thms fp_res; + val dtor_unfold_unique = #xtor_un_fold_unique fp_res; + val [dtor_unfold_transfer] = #xtor_un_fold_transfers 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; @@ -2369,7 +2369,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_legacy fp_res)); + (the_single (#xtor_un_folds 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))); @@ -2409,9 +2409,9 @@ val fp_map_id = map_id_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_legacy fp_res; - val dtor_unfold_unique = #xtor_un_fold_unique_legacy fp_res; - val [dtor_unfold_transfer] = #xtor_un_fold_transfers_legacy fp_res; + val [dtor_unfold_thm] = #xtor_un_fold_thms fp_res; + val dtor_unfold_unique = #xtor_un_fold_unique fp_res; + val [dtor_unfold_transfer] = #xtor_un_fold_transfers 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)); @@ -2710,7 +2710,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_legacy fp_res)); + (the_single (#xtor_un_folds 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; @@ -2761,9 +2761,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_legacy fp_res; - val dtor_unfold_unique = #xtor_un_fold_unique_legacy fp_res; - val [dtor_unfold_transfer] = #xtor_un_fold_transfers_legacy fp_res; + val [dtor_unfold_thm] = #xtor_un_fold_thms fp_res; + val dtor_unfold_unique = #xtor_un_fold_unique fp_res; + val [dtor_unfold_transfer] = #xtor_un_fold_transfers 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 75ca185db27f -r 9ad0bac25a84 src/HOL/Tools/BNF/bnf_lfp.ML --- a/src/HOL/Tools/BNF/bnf_lfp.ML Thu Apr 07 17:56:26 2016 +0200 +++ b/src/HOL/Tools/BNF/bnf_lfp.ML Thu Apr 07 17:56:26 2016 +0200 @@ -1879,17 +1879,17 @@ val fp_res = {Ts = Ts, bnfs = Ibnfs, pre_bnfs = bnfs, absT_infos = absT_infos, - ctors = ctors, dtors = dtors, xtor_un_folds_legacy = folds, xtor_co_recs = export recs, + ctors = ctors, dtors = dtors, xtor_un_folds = folds, xtor_co_recs = export 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_unique = ctor_Imap_unique_thm, xtor_setss = ctor_Iset_thmss', - xtor_rels = ctor_Irel_thms, xtor_un_fold_thms_legacy = ctor_fold_thms, - xtor_co_rec_thms = ctor_rec_thms, xtor_un_fold_unique_legacy = ctor_fold_unique_thm, + xtor_rels = ctor_Irel_thms, xtor_un_fold_thms = ctor_fold_thms, + xtor_co_rec_thms = ctor_rec_thms, xtor_un_fold_unique = ctor_fold_unique_thm, xtor_co_rec_unique = ctor_rec_unique_thm, - xtor_un_fold_o_maps_legacy = ctor_fold_o_Imap_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_legacy = ctor_fold_transfer_thms, + xtor_un_fold_transfers = 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 75ca185db27f -r 9ad0bac25a84 src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML --- a/src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML Thu Apr 07 17:56:26 2016 +0200 +++ b/src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML Thu Apr 07 17:56:26 2016 +0200 @@ -36,15 +36,15 @@ val co_rec_unique_thm = map_id0_of_bnf fp_bnf RS @{thm ctor_rec_unique}; in {Ts = [fpT], bnfs = [fp_bnf], pre_bnfs = [ID_bnf], absT_infos = [trivial_absT_info_of fpT], - ctors = xtors, dtors = xtors, xtor_un_folds_legacy = co_recs, + ctors = xtors, dtors = xtors, xtor_un_folds = 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_unique = @{thm xtor_map_unique}, 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_unique_legacy = co_rec_unique_thm, xtor_co_rec_unique = co_rec_unique_thm, - 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_un_fold_thms = co_rec_thms, xtor_co_rec_thms = co_rec_thms, + xtor_un_fold_unique = co_rec_unique_thm, xtor_co_rec_unique = co_rec_unique_thm, + 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 = []} end;