--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Mon Oct 06 13:34:24 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Mon Oct 06 13:34:39 2014 +0200
@@ -12,7 +12,8 @@
{ctrXs_Tss: typ list list,
ctr_defs: thm list,
ctr_sugar: Ctr_Sugar.ctr_sugar,
- ctr_transfers: thm list}
+ ctr_transfers: thm list,
+ case_transfers: thm list}
type fp_bnf_sugar =
{map_thms: thm list,
@@ -174,7 +175,8 @@
{ctrXs_Tss: typ list list,
ctr_defs: thm list,
ctr_sugar: Ctr_Sugar.ctr_sugar,
- ctr_transfers: thm list};
+ ctr_transfers: thm list,
+ case_transfers: thm list};
type fp_bnf_sugar =
{map_thms: thm list,
@@ -239,11 +241,13 @@
co_rec_discs = map (Morphism.thm phi) co_rec_discs,
co_rec_selss = map (map (Morphism.thm phi)) co_rec_selss};
-fun morph_fp_ctr_sugar phi ({ctrXs_Tss, ctr_defs, ctr_sugar, ctr_transfers} : fp_ctr_sugar) =
+fun morph_fp_ctr_sugar phi ({ctrXs_Tss, ctr_defs, ctr_sugar, ctr_transfers,
+ case_transfers} : fp_ctr_sugar) =
{ctrXs_Tss = map (map (Morphism.typ phi)) ctrXs_Tss,
ctr_defs = map (Morphism.thm phi) ctr_defs,
ctr_sugar = morph_ctr_sugar phi ctr_sugar,
- ctr_transfers = map (Morphism.thm phi) ctr_transfers};
+ ctr_transfers = map (Morphism.thm phi) ctr_transfers,
+ case_transfers = map (Morphism.thm phi) case_transfers};
fun morph_fp_sugar phi ({T, BT, X, fp, fp_res, fp_res_index, pre_bnf, absT_info, fp_nesting_bnfs,
live_nesting_bnfs, fp_ctr_sugar, fp_bnf_sugar,
@@ -313,7 +317,7 @@
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 map_disc_iffss map_selss rel_selss rel_intross rel_casess set_thmss set_selss
- set_intross set_casess ctr_transferss noted =
+ set_intross set_casess ctr_transferss case_transferss noted =
let
val fp_sugars =
map_index (fn (kk, T) =>
@@ -324,7 +328,8 @@
{ctrXs_Tss = nth ctrXs_Tsss kk,
ctr_defs = nth ctr_defss kk,
ctr_sugar = nth ctr_sugars kk,
- ctr_transfers = nth ctr_transferss kk},
+ ctr_transfers = nth ctr_transferss kk,
+ case_transfers = nth case_transferss kk},
fp_bnf_sugar =
{map_thms = nth map_thmss kk,
map_disc_iffs = nth map_disc_iffss kk,
@@ -497,7 +502,7 @@
distincts, distinct_discsss, ...} : ctr_sugar)
lthy =
if live = 0 then
- (([], [], [], [], [], [], [], [], [], [], [], [], []), lthy)
+ (([], [], [], [], [], [], [], [], [], [], [], [], [], []), lthy)
else
let
val n = length ctr_Tss;
@@ -802,7 +807,7 @@
(thm, [consumes_attr, case_names_attr, cases_pred_attr ""])
end;
- val case_transfer_thms =
+ val case_transfer_thm =
let
val (S, names_lthy) = yield_singleton (mk_Frees "S") (mk_pred2T C E) names_lthy;
val caseA = mk_case As C casex;
@@ -950,7 +955,7 @@
|> map (fn (thms, attrs) => ((Binding.empty, attrs), [(thms, [])]));
val notes =
- [(case_transferN, [case_transfer_thms], K []),
+ [(case_transferN, [case_transfer_thm], K []),
(ctr_transferN, ctr_transfer_thms, K []),
(disc_transferN, disc_transfer_thms, K []),
(mapN, map_thms, K (code_attrs @ nitpicksimp_attrs @ simp_attrs)),
@@ -989,7 +994,8 @@
map subst set_sel_thms,
map subst set_intros_thms,
map subst set_cases_thms,
- map subst ctr_transfer_thms), lthy')
+ map subst ctr_transfer_thms,
+ [subst case_transfer_thm]), lthy')
end;
type lfp_sugar_thms = (thm list * thm * Token.src list) * (thm list list * Token.src list);
@@ -2093,7 +2099,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_list13 o split_list)
+ |>> apsnd split_list o apfst (apsnd split_list4 o apfst split_list14 o split_list)
o split_list;
fun mk_simp_thms ({injects, distincts, case_thms, ...} : ctr_sugar) co_recs map_thms rel_injects
@@ -2128,7 +2134,8 @@
fun derive_note_induct_recs_thms_for_types
((((map_thmss, map_disc_iffss, map_selss, rel_injectss, rel_distinctss, rel_selss,
- rel_intross, rel_casess, set_thmss, set_selss, set_intross, set_casess, ctr_transferss),
+ rel_intross, rel_casess, set_thmss, set_selss, set_intross, set_casess, ctr_transferss,
+ case_transferss),
(ctrss, _, ctr_defss, ctr_sugars)),
(recs, rec_defs)), lthy) =
let
@@ -2189,6 +2196,7 @@
map_thmss [induct_thm] (map single induct_thms) rec_thmss (replicate nn [])
(replicate nn []) rel_injectss rel_distinctss map_disc_iffss map_selss rel_selss
rel_intross rel_casess set_thmss set_selss set_intross set_casess ctr_transferss
+ case_transferss
end;
fun derive_corec_transfer_thms lthy corecs corec_defs =
@@ -2208,7 +2216,8 @@
fun derive_note_coinduct_corecs_thms_for_types
((((map_thmss, map_disc_iffss, map_selss, rel_injectss, rel_distinctss, rel_selss,
- rel_intross, rel_casess, set_thmss, set_selss, set_intross, set_casess, ctr_transferss),
+ rel_intross, rel_casess, set_thmss, set_selss, set_intross, set_casess, ctr_transferss,
+ case_transferss),
(_, _, ctr_defss, ctr_sugars)),
(corecs, corec_defs)), lthy) =
let
@@ -2305,6 +2314,7 @@
(transpose [coinduct_thms, coinduct_strong_thms]) corec_thmss corec_disc_thmss
corec_sel_thmsss rel_injectss rel_distinctss map_disc_iffss map_selss rel_selss
rel_intross rel_casess set_thmss set_selss set_intross set_casess ctr_transferss
+ case_transferss
end;
val lthy'' = lthy'