--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Fri Sep 26 14:36:54 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Fri Sep 26 14:41:08 2014 +0200
@@ -9,7 +9,11 @@
signature BNF_FP_DEF_SUGAR =
sig
type fp_ctr_sugar = {}
- type fp_bnf_sugar = {}
+
+ type fp_bnf_sugar =
+ {rel_injects: thm list,
+ rel_distincts: thm list}
+
type fp_co_induct_sugar = {}
type fp_sugar =
@@ -34,8 +38,6 @@
co_rec_thms: thm list,
co_rec_discs: thm list,
co_rec_selss: thm list list,
- rel_injects: thm list,
- rel_distincts: thm list,
fp_ctr_sugar: fp_ctr_sugar,
fp_bnf_sugar: fp_bnf_sugar,
fp_co_induct_sugar: fp_co_induct_sugar};
@@ -159,7 +161,11 @@
val set_selN = "set_sel";
type fp_ctr_sugar = {}
-type fp_bnf_sugar = {}
+
+type fp_bnf_sugar =
+ {rel_injects: thm list,
+ rel_distincts: thm list}
+
type fp_co_induct_sugar = {}
type fp_sugar =
@@ -184,16 +190,18 @@
co_rec_thms: thm list,
co_rec_discs: thm list,
co_rec_selss: thm list list,
- rel_injects: thm list,
- rel_distincts: thm list,
fp_ctr_sugar: fp_ctr_sugar,
fp_bnf_sugar: fp_bnf_sugar,
fp_co_induct_sugar: fp_co_induct_sugar};
+fun morph_fp_bnf_sugar phi ({rel_injects, rel_distincts} : fp_bnf_sugar) =
+ {rel_injects = map (Morphism.thm phi) rel_injects,
+ rel_distincts = map (Morphism.thm phi) rel_distincts}
+
fun morph_fp_sugar phi ({T, BT, X, fp, fp_res, fp_res_index, pre_bnf, absT_info, fp_nesting_bnfs,
live_nesting_bnfs, ctrXs_Tss, ctr_defs, ctr_sugar, co_rec, co_rec_def, maps, common_co_inducts,
- co_inducts, co_rec_thms, co_rec_discs, co_rec_selss, rel_injects, rel_distincts,
- fp_ctr_sugar, fp_bnf_sugar, fp_co_induct_sugar} : fp_sugar) =
+ co_inducts, co_rec_thms, co_rec_discs, co_rec_selss, fp_ctr_sugar, fp_bnf_sugar,
+ fp_co_induct_sugar} : fp_sugar) =
{T = Morphism.typ phi T,
BT = Morphism.typ phi BT,
X = Morphism.typ phi X,
@@ -215,10 +223,8 @@
co_rec_thms = map (Morphism.thm phi) co_rec_thms,
co_rec_discs = map (Morphism.thm phi) co_rec_discs,
co_rec_selss = map (map (Morphism.thm phi)) co_rec_selss,
- rel_injects = map (Morphism.thm phi) rel_injects,
- rel_distincts = map (Morphism.thm phi) rel_distincts,
fp_ctr_sugar = fp_ctr_sugar,
- fp_bnf_sugar = fp_bnf_sugar,
+ fp_bnf_sugar = morph_fp_bnf_sugar phi fp_bnf_sugar,
fp_co_induct_sugar = fp_co_induct_sugar};
val transfer_fp_sugar = morph_fp_sugar o Morphism.transfer_morphism;
@@ -282,8 +288,8 @@
co_rec = nth co_recs kk, co_rec_def = nth co_rec_defs kk, maps = nth mapss kk,
common_co_inducts = common_co_inducts, co_inducts = nth co_inductss kk,
co_rec_thms = nth co_rec_thmss kk, co_rec_discs = nth co_rec_discss kk,
- co_rec_selss = nth co_rec_selsss kk, rel_injects = nth rel_injectss kk,
- rel_distincts = nth rel_distinctss kk, fp_ctr_sugar = {}, fp_bnf_sugar = {},
+ co_rec_selss = nth co_rec_selsss kk, fp_ctr_sugar = {},
+ fp_bnf_sugar = {rel_injects = nth rel_injectss kk, rel_distincts = nth rel_distinctss kk},
fp_co_induct_sugar = {}}
|> morph_fp_sugar (substitute_noted_thm noted)) Ts;
in
--- a/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML Fri Sep 26 14:36:54 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML Fri Sep 26 14:41:08 2014 +0200
@@ -293,15 +293,15 @@
fun mk_target_fp_sugar T X kk pre_bnf absT_info ctrXs_Tss ctr_defs ctr_sugar co_rec
co_rec_def maps co_inducts co_rec_thms co_rec_disc_thms co_rec_sel_thmss
- ({rel_injects, rel_distincts, ...} : fp_sugar) =
+ ({fp_bnf_sugar = {rel_injects, rel_distincts, ...}, ...} : fp_sugar) =
{T = T, BT = T (*wrong but harmless*), X = X, fp = fp, fp_res = fp_res, fp_res_index = kk,
pre_bnf = pre_bnf, absT_info = absT_info, fp_nesting_bnfs = fp_nesting_bnfs,
live_nesting_bnfs = live_nesting_bnfs, ctrXs_Tss = ctrXs_Tss, ctr_defs = ctr_defs,
ctr_sugar = ctr_sugar, co_rec = co_rec, co_rec_def = co_rec_def, maps = maps,
common_co_inducts = common_co_inducts, co_inducts = co_inducts,
co_rec_thms = co_rec_thms, co_rec_discs = co_rec_disc_thms,
- co_rec_selss = co_rec_sel_thmss, rel_injects = rel_injects,
- rel_distincts = rel_distincts, fp_ctr_sugar = {}, fp_bnf_sugar = {},
+ co_rec_selss = co_rec_sel_thmss, fp_ctr_sugar = {},
+ fp_bnf_sugar = {rel_injects = rel_injects, rel_distincts = rel_distincts},
fp_co_induct_sugar = {}}
|> morph_fp_sugar phi;
--- a/src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML Fri Sep 26 14:36:54 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML Fri Sep 26 14:41:08 2014 +0200
@@ -87,10 +87,10 @@
co_rec_thms = @{thms sum.case},
co_rec_discs = [],
co_rec_selss = [],
- rel_injects = @{thms rel_sum_simps(1,4)},
- rel_distincts = @{thms rel_sum_simps(2,3)[THEN eq_False[THEN iffD1]]},
fp_ctr_sugar = {},
- fp_bnf_sugar = {},
+ fp_bnf_sugar = {
+ rel_injects = @{thms rel_sum_simps(1,4)},
+ rel_distincts = @{thms rel_sum_simps(2,3)[THEN eq_False[THEN iffD1]]}},
fp_co_induct_sugar = {}}
end;
@@ -131,10 +131,10 @@
co_rec_thms = @{thms prod.case},
co_rec_discs = [],
co_rec_selss = [],
- rel_injects = @{thms rel_prod_apply},
- rel_distincts = [],
fp_ctr_sugar = {},
- fp_bnf_sugar = {},
+ fp_bnf_sugar = {
+ rel_injects = @{thms rel_prod_apply},
+ rel_distincts = []},
fp_co_induct_sugar = {}}
end;
--- a/src/HOL/Tools/Transfer/transfer_bnf.ML Fri Sep 26 14:36:54 2014 +0200
+++ b/src/HOL/Tools/Transfer/transfer_bnf.ML Fri Sep 26 14:41:08 2014 +0200
@@ -348,7 +348,7 @@
else thm RS (@{thm eq_onp_same_args} RS iffD1))
|> kill_top
end
- val rel_injects = #rel_injects fp_sugar
+ val rel_injects = #rel_injects (#fp_bnf_sugar fp_sugar)
in
rel_injects
|> map (Local_Defs.unfold lthy [@{thm conj_assoc}])