--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Sun Oct 05 20:30:58 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Mon Oct 06 13:32:41 2014 +0200
@@ -15,6 +15,7 @@
type fp_bnf_sugar =
{map_thms: thm list,
+ map_disc_iffs: thm list,
rel_injects: thm list,
rel_distincts: thm list}
@@ -167,6 +168,7 @@
type fp_bnf_sugar =
{map_thms: thm list,
+ map_disc_iffs: thm list,
rel_injects: thm list,
rel_distincts: thm list};
@@ -194,8 +196,9 @@
fp_bnf_sugar: fp_bnf_sugar,
fp_co_induct_sugar: fp_co_induct_sugar};
-fun morph_fp_bnf_sugar phi ({map_thms, rel_injects, rel_distincts} : fp_bnf_sugar) =
+fun morph_fp_bnf_sugar phi ({map_thms, map_disc_iffs, rel_injects, rel_distincts} : fp_bnf_sugar) =
{map_thms = map (Morphism.thm phi) map_thms,
+ map_disc_iffs = map (Morphism.thm phi) map_disc_iffs,
rel_injects = map (Morphism.thm phi) rel_injects,
rel_distincts = map (Morphism.thm phi) rel_distincts};
@@ -281,7 +284,7 @@
fun interpret_bnfs_register_fp_sugars plugins Ts BTs Xs fp pre_bnfs absT_infos fp_nesting_bnfs
live_nesting_bnfs fp_res ctrXs_Tsss ctr_defss ctr_sugars co_recs co_rec_defs map_thmss
common_co_inducts co_inductss co_rec_thmss co_rec_discss co_rec_selsss rel_injectss
- rel_distinctss noted =
+ rel_distinctss map_disc_iffss noted =
let
val fp_sugars =
map_index (fn (kk, T) =>
@@ -294,6 +297,7 @@
ctr_sugar = nth ctr_sugars kk},
fp_bnf_sugar =
{map_thms = nth map_thmss kk,
+ map_disc_iffs = nth map_disc_iffss kk,
rel_injects = nth rel_injectss kk,
rel_distincts = nth rel_distinctss kk},
fp_co_induct_sugar =
@@ -455,7 +459,7 @@
distincts, distinct_discsss, ...} : ctr_sugar)
lthy =
if live = 0 then
- (([], [], [], []), lthy)
+ (([], [], [], [], []), lthy)
else
let
val n = length ctr_Tss;
@@ -804,8 +808,7 @@
else
Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced goals)
(fn {context = ctxt, prems = _} =>
- mk_map_disc_iff_tac ctxt (certify ctxt ta) exhaust (flat disc_thmss)
- map_thms)
+ mk_map_disc_iff_tac ctxt (certify ctxt ta) exhaust (flat disc_thmss) map_thms)
|> Conjunction.elim_balanced (length goals)
|> Proof_Context.export names_lthy lthy
|> map Thm.close_derivation
@@ -936,8 +939,8 @@
val subst = Morphism.thm (substitute_noted_thm noted);
in
- ((map subst map_thms, map subst rel_inject_thms, map subst rel_distinct_thms,
- map (map subst) set0_thmss), lthy')
+ ((map subst map_thms, map subst map_disc_iff_thms, map subst rel_inject_thms,
+ map subst rel_distinct_thms, map (map subst) set0_thmss), lthy')
end;
type lfp_sugar_thms = (thm list * thm * Token.src list) * (thm list list * Token.src list);
@@ -2041,7 +2044,7 @@
fun wrap_ctrs_derive_map_set_rel_thms_define_co_rec_for_types (wrap_one_etc, lthy) =
fold_map I wrap_one_etc lthy
- |>> apsnd split_list o apfst (apsnd split_list4 o apfst split_list4 o split_list)
+ |>> apsnd split_list o apfst (apsnd split_list4 o apfst split_list5 o split_list)
o split_list;
fun mk_simp_thms ({injects, distincts, case_thms, ...} : ctr_sugar) co_recs map_thms rel_injects
@@ -2074,7 +2077,8 @@
end;
fun derive_note_induct_recs_thms_for_types
- ((((map_thmss, rel_injectss, rel_distinctss, setss), (ctrss, _, ctr_defss, ctr_sugars)),
+ ((((map_thmss, map_disc_iffss, rel_injectss, rel_distinctss, setss),
+ (ctrss, _, ctr_defss, ctr_sugars)),
(recs, rec_defs)), lthy) =
let
val ((induct_thms, induct_thm, induct_attrs), (rec_thmss, rec_attrs)) =
@@ -2132,7 +2136,7 @@
|-> interpret_bnfs_register_fp_sugars plugins fpTs fpBTs Xs Least_FP pre_bnfs absT_infos
fp_nesting_bnfs live_nesting_bnfs fp_res ctrXs_Tsss ctr_defss ctr_sugars recs rec_defs
map_thmss [induct_thm] (map single induct_thms) rec_thmss (replicate nn []) (replicate nn [])
- rel_injectss rel_distinctss
+ rel_injectss rel_distinctss map_disc_iffss
end;
fun derive_corec_transfer_thms lthy corecs corec_defs =
@@ -2151,7 +2155,8 @@
end;
fun derive_note_coinduct_corecs_thms_for_types
- ((((map_thmss, rel_injectss, rel_distinctss, setss), (_, _, ctr_defss, ctr_sugars)),
+ ((((map_thmss, map_disc_iffss, rel_injectss, rel_distinctss, setss),
+ (_, _, ctr_defss, ctr_sugars)),
(corecs, corec_defs)), lthy) =
let
val (([(coinduct_thms, coinduct_thm), (coinduct_strong_thms, coinduct_strong_thm)],
@@ -2245,7 +2250,7 @@
fp_nesting_bnfs live_nesting_bnfs fp_res ctrXs_Tsss ctr_defss ctr_sugars corecs corec_defs
map_thmss [coinduct_thm, coinduct_strong_thm]
(transpose [coinduct_thms, coinduct_strong_thms]) corec_thmss corec_disc_thmss
- corec_sel_thmsss rel_injectss rel_distinctss
+ corec_sel_thmsss rel_injectss rel_distinctss map_disc_iffss
end;
val lthy'' = lthy'
--- a/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML Sun Oct 05 20:30:58 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML Mon Oct 06 13:32:41 2014 +0200
@@ -293,7 +293,7 @@
fun mk_target_fp_sugar T X kk pre_bnf absT_info ctrXs_Tss ctr_defs ctr_sugar co_rec
co_rec_def map_thms co_inducts co_rec_thms co_rec_disc_thms co_rec_sel_thmss
- ({fp_bnf_sugar = {rel_injects, rel_distincts, ...}, ...} : fp_sugar) =
+ ({fp_bnf_sugar = {map_disc_iffs, 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,
@@ -303,6 +303,7 @@
ctr_sugar = ctr_sugar},
fp_bnf_sugar =
{map_thms = map_thms,
+ map_disc_iffs = map_disc_iffs,
rel_injects = rel_injects,
rel_distincts = rel_distincts},
fp_co_induct_sugar =
--- a/src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML Sun Oct 05 20:30:58 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML Mon Oct 06 13:32:41 2014 +0200
@@ -82,6 +82,7 @@
ctr_sugar = the_frozen_ctr_sugar_of ctxt fpT_name},
fp_bnf_sugar =
{map_thms = @{thms map_sum.simps},
+ map_disc_iffs = [],
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 =
@@ -126,6 +127,7 @@
ctr_sugar = the_frozen_ctr_sugar_of ctxt fpT_name},
fp_bnf_sugar =
{map_thms = @{thms map_prod_simp},
+ map_disc_iffs = [],
rel_injects = @{thms rel_prod_apply},
rel_distincts = []},
fp_co_induct_sugar =