--- 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
--- 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};
--- 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
--- 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;
--- 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
--- 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 =