--- a/src/HOL/Library/bnf_lfp_countable.ML Fri Sep 26 15:10:02 2014 +0200
+++ b/src/HOL/Library/bnf_lfp_countable.ML Fri Sep 26 19:38:26 2014 +0200
@@ -150,16 +150,17 @@
HOLogic.mk_imp (HOLogic.mk_eq (encode_fun $ x, encode_fun $ Bound 0),
HOLogic.eq_const fpT $ x $ Bound 0));
- val fp_sugars as {fp_nesting_bnfs, common_co_inducts = induct :: _, ...} :: _ =
+ val fp_sugars as
+ {fp_nesting_bnfs, fp_co_induct_sugar = {common_co_inducts = induct :: _, ...}, ...} :: _ =
map (the o fp_sugar_of ctxt o fst o dest_Type) fpTs0;
- val ctr_sugars = map #ctr_sugar fp_sugars;
+ val ctr_sugars = map (#ctr_sugar o #fp_ctr_sugar) fp_sugars;
val ctrss0 = map #ctrs ctr_sugars;
val ns = map length ctrss0;
- val recs0 = map #co_rec fp_sugars;
+ val recs0 = map (#co_rec o #fp_co_induct_sugar) fp_sugars;
val nchotomys = map #nchotomy ctr_sugars;
val injectss = map #injects ctr_sugars;
- val rec_thmss = map #co_rec_thms fp_sugars;
+ val rec_thmss = map (#co_rec_thms o #fp_co_induct_sugar) fp_sugars;
val map_comps' = map (unfold_thms ctxt @{thms comp_def} o map_comp_of_bnf) fp_nesting_bnfs;
val inj_map_strongs' = map (Thm.permute_prems 0 ~1 o inj_map_strong_of_bnf) fp_nesting_bnfs;
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Fri Sep 26 15:10:02 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Fri Sep 26 19:38:26 2014 +0200
@@ -8,6 +8,25 @@
signature BNF_FP_DEF_SUGAR =
sig
+ type fp_ctr_sugar =
+ {ctrXs_Tss: typ list list,
+ ctr_defs: thm list,
+ ctr_sugar: Ctr_Sugar.ctr_sugar}
+
+ type fp_bnf_sugar =
+ {map_thms: thm list,
+ rel_injects: thm list,
+ rel_distincts: thm list}
+
+ type fp_co_induct_sugar =
+ {co_rec: term,
+ common_co_inducts: thm list,
+ co_inducts: thm list,
+ co_rec_def: thm,
+ co_rec_thms: thm list,
+ co_rec_discs: thm list,
+ co_rec_selss: thm list list}
+
type fp_sugar =
{T: typ,
BT: typ,
@@ -19,19 +38,9 @@
absT_info: BNF_Comp.absT_info,
fp_nesting_bnfs: BNF_Def.bnf list,
live_nesting_bnfs: BNF_Def.bnf list,
- ctrXs_Tss: typ list list,
- ctr_defs: thm list,
- ctr_sugar: Ctr_Sugar.ctr_sugar,
- co_rec: term,
- co_rec_def: thm,
- maps: thm list,
- common_co_inducts: thm list,
- co_inducts: thm list,
- 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};
val morph_fp_sugar: morphism -> fp_sugar -> fp_sugar
val transfer_fp_sugar: theory -> fp_sugar -> fp_sugar
@@ -151,6 +160,25 @@
val set_inductN = "set_induct";
val set_selN = "set_sel";
+type fp_ctr_sugar =
+ {ctrXs_Tss: typ list list,
+ ctr_defs: thm list,
+ ctr_sugar: Ctr_Sugar.ctr_sugar};
+
+type fp_bnf_sugar =
+ {map_thms: thm list,
+ rel_injects: thm list,
+ rel_distincts: thm list};
+
+type fp_co_induct_sugar =
+ {co_rec: term,
+ common_co_inducts: thm list,
+ co_inducts: thm list,
+ co_rec_def: thm,
+ co_rec_thms: thm list,
+ co_rec_discs: thm list,
+ co_rec_selss: thm list list};
+
type fp_sugar =
{T: typ,
BT: typ,
@@ -162,23 +190,33 @@
absT_info: absT_info,
fp_nesting_bnfs: bnf list,
live_nesting_bnfs: bnf list,
- ctrXs_Tss: typ list list,
- ctr_defs: thm list,
- ctr_sugar: Ctr_Sugar.ctr_sugar,
- co_rec: term,
- co_rec_def: thm,
- maps: thm list,
- common_co_inducts: thm list,
- co_inducts: thm list,
- 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 ({map_thms, rel_injects, rel_distincts} : fp_bnf_sugar) =
+ {map_thms = map (Morphism.thm phi) map_thms,
+ rel_injects = map (Morphism.thm phi) rel_injects,
+ rel_distincts = map (Morphism.thm phi) rel_distincts};
+
+fun morph_fp_co_induct_sugar phi ({co_rec, common_co_inducts, co_inducts, co_rec_def, co_rec_thms,
+ co_rec_discs, co_rec_selss} : fp_co_induct_sugar) =
+ {co_rec = Morphism.term phi co_rec,
+ common_co_inducts = map (Morphism.thm phi) common_co_inducts,
+ co_inducts = map (Morphism.thm phi) co_inducts,
+ co_rec_def = Morphism.thm phi co_rec_def,
+ 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};
+
+fun morph_fp_ctr_sugar phi ({ctrXs_Tss, ctr_defs, ctr_sugar} : 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};
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_sugar) =
+ live_nesting_bnfs, 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,
@@ -189,19 +227,9 @@
absT_info = morph_absT_info phi absT_info,
fp_nesting_bnfs = map (morph_bnf phi) fp_nesting_bnfs,
live_nesting_bnfs = map (morph_bnf phi) live_nesting_bnfs,
- 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,
- co_rec = Morphism.term phi co_rec,
- co_rec_def = Morphism.thm phi co_rec_def,
- maps = map (Morphism.thm phi) maps,
- common_co_inducts = map (Morphism.thm phi) common_co_inducts,
- co_inducts = map (Morphism.thm phi) co_inducts,
- 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 = morph_fp_ctr_sugar phi fp_ctr_sugar,
+ fp_bnf_sugar = morph_fp_bnf_sugar phi fp_bnf_sugar,
+ fp_co_induct_sugar = morph_fp_co_induct_sugar phi fp_co_induct_sugar};
val transfer_fp_sugar = morph_fp_sugar o Morphism.transfer_morphism;
@@ -251,7 +279,7 @@
register_fp_sugars_raw fp_sugars #> interpret_fp_sugars plugins fp_sugars;
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 mapss
+ 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 =
let
@@ -260,12 +288,22 @@
{T = T, BT = nth BTs kk, X = nth Xs kk, fp = fp, fp_res = fp_res, fp_res_index = kk,
pre_bnf = nth pre_bnfs kk, absT_info = nth absT_infos kk,
fp_nesting_bnfs = fp_nesting_bnfs, live_nesting_bnfs = live_nesting_bnfs,
- ctrXs_Tss = nth ctrXs_Tsss kk, ctr_defs = nth ctr_defss kk, ctr_sugar = nth ctr_sugars kk,
- 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 =
+ {ctrXs_Tss = nth ctrXs_Tsss kk,
+ ctr_defs = nth ctr_defss kk,
+ ctr_sugar = nth ctr_sugars kk},
+ fp_bnf_sugar =
+ {map_thms = nth map_thmss kk,
+ rel_injects = nth rel_injectss kk,
+ rel_distincts = nth rel_distinctss kk},
+ fp_co_induct_sugar =
+ {co_rec = nth co_recs kk,
+ common_co_inducts = common_co_inducts,
+ co_inducts = nth co_inductss kk,
+ co_rec_def = nth co_rec_defs 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}}
|> morph_fp_sugar (substitute_noted_thm noted)) Ts;
in
register_fp_sugars_raw fp_sugars
@@ -600,9 +638,13 @@
val consumes_attr = Attrib.internal (K (Rule_Cases.consumes 1));
val cases_set_attr =
Attrib.internal (K (Induct.cases_pred (name_of_set set)));
+
+ val ctr_names = quasi_unambiguous_case_names (flat
+ (map (uncurry mk_names o map_prod length name_of_ctr) (premss ~~ ctrAs)));
+ val case_names_attr = Attrib.internal (K (Rule_Cases.case_names ctr_names));
in
(* TODO: @{attributes [elim?]} *)
- (thm, [consumes_attr, cases_set_attr])
+ (thm, [consumes_attr, cases_set_attr, case_names_attr])
end) setAs)
end;
@@ -2006,9 +2048,9 @@
|>> apsnd split_list o apfst (apsnd split_list4 o apfst split_list4 o split_list)
o split_list;
- fun mk_simp_thms ({injects, distincts, case_thms, ...} : ctr_sugar) co_recs mapsx rel_injects
+ fun mk_simp_thms ({injects, distincts, case_thms, ...} : ctr_sugar) co_recs map_thms rel_injects
rel_distincts setss =
- injects @ distincts @ case_thms @ co_recs @ mapsx @ rel_injects @ rel_distincts @ flat setss;
+ injects @ distincts @ case_thms @ co_recs @ map_thms @ rel_injects @ rel_distincts @ flat setss;
fun mk_co_rec_transfer_goals lthy co_recs =
let
@@ -2036,7 +2078,7 @@
end;
fun derive_note_induct_recs_thms_for_types
- ((((mapss, rel_injectss, rel_distinctss, setss), (ctrss, _, ctr_defss, ctr_sugars)),
+ ((((map_thmss, 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)) =
@@ -2067,7 +2109,7 @@
end;
val simp_thmss =
- map6 mk_simp_thms ctr_sugars rec_thmss mapss rel_injectss rel_distinctss setss;
+ map6 mk_simp_thms ctr_sugars rec_thmss map_thmss rel_injectss rel_distinctss setss;
val common_notes =
(if nn > 1 then
@@ -2093,7 +2135,7 @@
(fst (dest_Type (hd fpTs)) ^ (implode (map (prefix "_") (tl fp_b_names)))) inductN
|-> 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
- mapss [induct_thm] (map single induct_thms) rec_thmss (replicate nn []) (replicate nn [])
+ map_thmss [induct_thm] (map single induct_thms) rec_thmss (replicate nn []) (replicate nn [])
rel_injectss rel_distinctss
end;
@@ -2113,7 +2155,7 @@
end;
fun derive_note_coinduct_corecs_thms_for_types
- ((((mapss, rel_injectss, rel_distinctss, setss), (_, _, ctr_defss, ctr_sugars)),
+ ((((map_thmss, 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)],
@@ -2174,7 +2216,7 @@
val simp_thmss =
map6 mk_simp_thms ctr_sugars
(map3 flat_corec_thms corec_disc_thmss corec_disc_iff_thmss corec_sel_thmss)
- mapss rel_injectss rel_distinctss setss;
+ map_thmss rel_injectss rel_distinctss setss;
val common_notes =
(set_inductN, set_induct_thms, nth set_induct_attrss) ::
@@ -2205,7 +2247,7 @@
|> Local_Theory.notes (common_notes @ notes)
|-> interpret_bnfs_register_fp_sugars plugins fpTs fpBTs Xs Greatest_FP pre_bnfs absT_infos
fp_nesting_bnfs live_nesting_bnfs fp_res ctrXs_Tsss ctr_defss ctr_sugars corecs corec_defs
- mapss [coinduct_thm, coinduct_strong_thm]
+ 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
end;
--- a/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML Fri Sep 26 15:10:02 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML Fri Sep 26 19:38:26 2014 +0200
@@ -136,7 +136,7 @@
val nn = length fpTs;
val kks = 0 upto nn - 1;
- fun target_ctr_sugar_of_fp_sugar fpT ({T, ctr_sugar, ...} : fp_sugar) =
+ fun target_ctr_sugar_of_fp_sugar fpT ({T, fp_ctr_sugar = {ctr_sugar, ...}, ...} : fp_sugar) =
let
val rho = Vartab.fold (cons o apsnd snd) (Sign.typ_match thy (T, fpT) Vartab.empty) [];
val phi = Morphism.term_morphism "BNF" (Term.subst_TVars rho);
@@ -144,8 +144,8 @@
morph_ctr_sugar phi ctr_sugar
end;
- val ctr_defss = map #ctr_defs fp_sugars0;
- val mapss = map #maps fp_sugars0;
+ val ctr_defss = map (#ctr_defs o #fp_ctr_sugar) fp_sugars0;
+ val mapss = map (#map_thms o #fp_bnf_sugar) fp_sugars0;
val ctr_sugars = map2 target_ctr_sugar_of_fp_sugar fpTs fp_sugars0;
val ctrss = map #ctrs ctr_sugars;
@@ -292,16 +292,27 @@
val phi = Proof_Context.export_morphism names_lthy no_defs_lthy;
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) =
+ 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) =
{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}
+ live_nesting_bnfs = live_nesting_bnfs,
+ fp_ctr_sugar =
+ {ctrXs_Tss = ctrXs_Tss,
+ ctr_defs = ctr_defs,
+ ctr_sugar = ctr_sugar},
+ fp_bnf_sugar =
+ {map_thms = map_thms,
+ rel_injects = rel_injects,
+ rel_distincts = rel_distincts},
+ fp_co_induct_sugar =
+ {co_rec = co_rec,
+ common_co_inducts = common_co_inducts,
+ co_inducts = co_inducts,
+ co_rec_def = co_rec_def,
+ co_rec_thms = co_rec_thms,
+ co_rec_discs = co_rec_disc_thms,
+ co_rec_selss = co_rec_sel_thmss}}
|> morph_fp_sugar phi;
val target_fp_sugars =
@@ -451,7 +462,8 @@
val perm_callssss0 = permute callssss0;
val perm_fp_sugars0 = map (the o fp_sugar_of lthy o fst o dest_Type) perm_Ts;
- val perm_callssss = map2 (indexify_callsss o #ctrs o #ctr_sugar) perm_fp_sugars0 perm_callssss0;
+ val perm_callssss =
+ map2 (indexify_callsss o #ctrs o #ctr_sugar o #fp_ctr_sugar) perm_fp_sugars0 perm_callssss0;
val ((perm_fp_sugars, fp_sugar_thms), lthy) =
if length perm_Tss = 1 then
--- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Fri Sep 26 15:10:02 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Fri Sep 26 19:38:26 2014 +0200
@@ -400,7 +400,7 @@
| _ => not_codatatype ctxt res_T);
fun map_thms_of_typ ctxt (Type (s, _)) =
- (case fp_sugar_of ctxt s of SOME {maps, ...} => maps | NONE => [])
+ (case fp_sugar_of ctxt s of SOME {fp_bnf_sugar = {map_thms, ...}, ...} => map_thms | NONE => [])
| map_thms_of_typ _ _ = [];
fun corec_specs_of bs arg_Ts res_Ts callers callssss0 lthy0 =
@@ -408,7 +408,8 @@
val thy = Proof_Context.theory_of lthy0;
val ((missing_res_Ts, perm0_kks, fp_sugars as {fp_nesting_bnfs,
- common_co_inducts = common_coinduct_thms, ...} :: _, (_, gfp_sugar_thms)), lthy) =
+ fp_co_induct_sugar = {common_co_inducts = common_coinduct_thms, ...}, ...} :: _,
+ (_, gfp_sugar_thms)), lthy) =
nested_to_mutual_fps (K true) Greatest_FP bs res_Ts callers callssss0 lthy0;
val coinduct_attrs_pair =
@@ -420,7 +421,8 @@
val perm_indices = map #fp_res_index perm_fp_sugars;
val perm_fpTs = map #T perm_fp_sugars;
- val perm_ctrXs_Tsss' = map (repair_nullary_single_ctr o #ctrXs_Tss) perm_fp_sugars;
+ val perm_ctrXs_Tsss' =
+ map (repair_nullary_single_ctr o #ctrXs_Tss o #fp_ctr_sugar) perm_fp_sugars;
val nn0 = length res_Ts;
val nn = length perm_fpTs;
@@ -429,7 +431,8 @@
val perm_Ts = map #T perm_fp_sugars;
val perm_Xs = map #X perm_fp_sugars;
- val perm_Cs = map (domain_type o body_fun_type o fastype_of o #co_rec) perm_fp_sugars;
+ val perm_Cs =
+ map (domain_type o body_fun_type o fastype_of o #co_rec o #fp_co_induct_sugar) perm_fp_sugars;
val Xs_TCs = perm_Xs ~~ (perm_Ts ~~ perm_Cs);
fun zip_corecT (Type (s, Us)) = [Type (s, map (mk_sumTN o zip_corecT) Us)]
@@ -495,9 +498,9 @@
distinct_discsss collapses corec_thms corec_discs corec_selss
end;
- fun mk_spec ({T, ctr_sugar as {exhaust_discs, sel_defs, ...}, co_rec = corec,
- co_rec_thms = corec_thms, co_rec_discs = corec_discs,
- co_rec_selss = corec_selss, ...} : fp_sugar) p_is q_isss f_isss f_Tsss =
+ fun mk_spec ({T, fp_ctr_sugar = {ctr_sugar as {exhaust_discs, sel_defs, ...}, ...},
+ fp_co_induct_sugar = {co_rec = corec, co_rec_thms = corec_thms, co_rec_discs = corec_discs,
+ co_rec_selss = corec_selss, ...}, ...} : fp_sugar) p_is q_isss f_isss f_Tsss =
{corec = mk_co_rec thy Greatest_FP perm_Cs' (substAT T) corec, exhaust_discs = exhaust_discs,
sel_defs = sel_defs,
fp_nesting_maps = maps (map_thms_of_typ lthy o T_of_bnf) fp_nesting_bnfs,
--- a/src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML Fri Sep 26 15:10:02 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML Fri Sep 26 19:38:26 2014 +0200
@@ -76,19 +76,22 @@
absT_info = trivial_absT_info_of fpT,
fp_nesting_bnfs = [],
live_nesting_bnfs = [],
- ctrXs_Tss = ctr_Tss,
- ctr_defs = @{thms Inl_def_alt Inr_def_alt},
- ctr_sugar = the_frozen_ctr_sugar_of ctxt fpT_name,
- co_rec = Const (@{const_name case_sum}, map (fn Ts => (Ts ---> C)) ctr_Tss ---> fpT --> C),
- co_rec_def = @{thm ctor_rec_def_alt[of "case_sum f1 f2" for f1 f2]},
- maps = @{thms map_sum.simps},
- common_co_inducts = @{thms sum.induct},
- co_inducts = @{thms sum.induct},
- 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 =
+ {ctrXs_Tss = ctr_Tss,
+ ctr_defs = @{thms Inl_def_alt Inr_def_alt},
+ ctr_sugar = the_frozen_ctr_sugar_of ctxt fpT_name},
+ fp_bnf_sugar =
+ {map_thms = @{thms map_sum.simps},
+ 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 =
+ {co_rec = Const (@{const_name case_sum}, map (fn Ts => (Ts ---> C)) ctr_Tss ---> fpT --> C),
+ common_co_inducts = @{thms sum.induct},
+ co_inducts = @{thms sum.induct},
+ co_rec_def = @{thm ctor_rec_def_alt[of "case_sum f1 f2" for f1 f2]},
+ co_rec_thms = @{thms sum.case},
+ co_rec_discs = [],
+ co_rec_selss = []}}
end;
fun fp_sugar_of_prod ctxt =
@@ -117,19 +120,22 @@
absT_info = trivial_absT_info_of fpT,
fp_nesting_bnfs = [],
live_nesting_bnfs = [],
- ctrXs_Tss = [ctr_Ts],
- ctr_defs = @{thms Pair_def_alt},
- ctr_sugar = the_frozen_ctr_sugar_of ctxt fpT_name,
- co_rec = Const (@{const_name case_prod}, (ctr_Ts ---> C) --> fpT --> C),
- co_rec_def = @{thm ctor_rec_def_alt[of "case_prod f" for f]},
- maps = @{thms map_prod_simp},
- common_co_inducts = @{thms prod.induct},
- co_inducts = @{thms prod.induct},
- co_rec_thms = @{thms prod.case},
- co_rec_discs = [],
- co_rec_selss = [],
- rel_injects = @{thms rel_prod_apply},
- rel_distincts = []}
+ fp_ctr_sugar =
+ {ctrXs_Tss = [ctr_Ts],
+ ctr_defs = @{thms Pair_def_alt},
+ ctr_sugar = the_frozen_ctr_sugar_of ctxt fpT_name},
+ fp_bnf_sugar =
+ {map_thms = @{thms map_prod_simp},
+ rel_injects = @{thms rel_prod_apply},
+ rel_distincts = []},
+ fp_co_induct_sugar =
+ {co_rec = Const (@{const_name case_prod}, (ctr_Ts ---> C) --> fpT --> C),
+ common_co_inducts = @{thms prod.induct},
+ co_inducts = @{thms prod.induct},
+ co_rec_def = @{thm ctor_rec_def_alt[of "case_prod f" for f]},
+ co_rec_thms = @{thms prod.case},
+ co_rec_discs = [],
+ co_rec_selss = []}}
end;
val _ = Theory.setup (map_local_theory (fn lthy =>
--- a/src/HOL/Tools/BNF/bnf_lfp_compat.ML Fri Sep 26 15:10:02 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_compat.ML Fri Sep 26 19:38:26 2014 +0200
@@ -236,7 +236,7 @@
fun mk_typ_descr index (Type (T_name, Ts)) ({ctrs, ...} : ctr_sugar) =
(index, (T_name, map mk_dtyp Ts, map (mk_ctr_descr Ts) ctrs));
- val fp_ctr_sugars = map (#ctr_sugar o checked_fp_sugar_of) fpT_names;
+ val fp_ctr_sugars = map (#ctr_sugar o #fp_ctr_sugar o checked_fp_sugar_of) fpT_names;
val orig_descr = map3 mk_typ_descr (0 upto nn_fp - 1) fpTs fp_ctr_sugars;
val all_infos = Old_Datatype_Data.get_all thy;
val (orig_descr' :: nested_descrs) =
@@ -290,16 +290,17 @@
else
((fp_sugars, (NONE, NONE)), lthy);
- fun mk_ctr_of ({ctr_sugar = {ctrs, ...}, ...} : fp_sugar) (Type (_, Ts)) = map (mk_ctr Ts) ctrs;
+ fun mk_ctr_of ({fp_ctr_sugar = {ctr_sugar = {ctrs, ...}, ...}, ...} : fp_sugar) (Type (_, Ts)) =
+ map (mk_ctr Ts) ctrs;
val substAT = Term.typ_subst_atomic (var_As ~~ As);
val Xs' = map #X fp_sugars';
- val ctrXs_Tsss' = map (map (map substAT) o #ctrXs_Tss) fp_sugars';
+ val ctrXs_Tsss' = map (map (map substAT) o #ctrXs_Tss o #fp_ctr_sugar) fp_sugars';
val ctrss' = map2 mk_ctr_of fp_sugars' fpTs';
- val {common_co_inducts = induct :: _, ...} :: _ = fp_sugars';
- val inducts = map (hd o #co_inducts) fp_sugars';
- val recs = map #co_rec fp_sugars';
- val rec_thmss = map #co_rec_thms fp_sugars';
+ val {fp_co_induct_sugar = {common_co_inducts = induct :: _, ...}, ...} :: _ = fp_sugars';
+ val inducts = map (hd o #co_inducts o #fp_co_induct_sugar) fp_sugars';
+ val recs = map (#co_rec o #fp_co_induct_sugar) fp_sugars';
+ val rec_thmss = map (#co_rec_thms o #fp_co_induct_sugar) fp_sugars';
fun is_nested_rec_type (Type (@{type_name fun}, [_, T])) = member (op =) Xs' (body_type T)
| is_nested_rec_type _ = false;
@@ -317,8 +318,9 @@
val rec'_names = map (fst o dest_Const) recs';
val rec'_thms = flat rec'_thmss;
- fun mk_info (kk, {T = Type (T_name0, _), ctr_sugar = {casex, exhaust, nchotomy, injects,
- distincts, case_thms, case_cong, case_cong_weak, split, split_asm, ...}, ...} : fp_sugar) =
+ fun mk_info (kk, {T = Type (T_name0, _), fp_ctr_sugar = {ctr_sugar = {casex, exhaust, nchotomy,
+ injects, distincts, case_thms, case_cong, case_cong_weak, split,
+ split_asm, ...}, ...}, ...} : fp_sugar) =
(T_name0,
{index = kk, descr = descr, inject = injects, distinct = distincts, induct = induct',
inducts = inducts', exhaust = exhaust, nchotomy = nchotomy, rec_names = rec'_names,
--- a/src/HOL/Tools/BNF/bnf_lfp_rec_sugar_more.ML Fri Sep 26 15:10:02 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_rec_sugar_more.ML Fri Sep 26 19:38:26 2014 +0200
@@ -24,8 +24,8 @@
| is_new_datatype ctxt s =
(case fp_sugar_of ctxt s of SOME {fp = Least_FP, ...} => true | _ => false);
-fun basic_lfp_sugar_of C fun_arg_Tsss ({T, fp_res_index, ctr_sugar, co_rec = recx,
- co_rec_thms = rec_thms, ...} : fp_sugar) =
+fun basic_lfp_sugar_of C fun_arg_Tsss ({T, fp_res_index, fp_ctr_sugar = {ctr_sugar, ...},
+ fp_co_induct_sugar = {co_rec = recx, co_rec_thms = rec_thms, ...}, ...} : fp_sugar) =
{T = T, fp_res_index = fp_res_index, C = C, fun_arg_Tsss = fun_arg_Tsss, ctr_sugar = ctr_sugar,
recx = recx, rec_thms = rec_thms};
@@ -34,7 +34,7 @@
| basic_lfp_sugars_of bs arg_Ts callers callssss0 lthy0 =
let
val ((missing_arg_Ts, perm0_kks,
- fp_sugars as {fp_nesting_bnfs, common_co_inducts = [common_induct], ...} :: _,
+ fp_sugars as {fp_nesting_bnfs, fp_co_induct_sugar = {common_co_inducts = [common_induct], ...}, ...} :: _,
(lfp_sugar_thms, _)), lthy) =
nested_to_mutual_fps (K true) Least_FP bs arg_Ts callers callssss0 lthy0;
@@ -42,7 +42,7 @@
val Ts = map #T fp_sugars;
val Xs = map #X fp_sugars;
- val Cs = map (body_type o fastype_of o #co_rec) fp_sugars;
+ val Cs = map (body_type o fastype_of o #co_rec o #fp_co_induct_sugar) fp_sugars;
val Xs_TCs = Xs ~~ (Ts ~~ Cs);
fun zip_XrecT (Type (s, Us)) = [Type (s, map (HOLogic.mk_tupleT o zip_XrecT) Us)]
@@ -51,7 +51,7 @@
SOME (T, C) => [T, C]
| NONE => [U]);
- val ctrXs_Tsss = map #ctrXs_Tss fp_sugars;
+ val ctrXs_Tsss = map (#ctrXs_Tss o #fp_ctr_sugar) fp_sugars;
val fun_arg_Tssss = map (map (map zip_XrecT)) ctrXs_Tsss;
val fp_nesting_map_ident0s = map map_ident0_of_bnf fp_nesting_bnfs;
--- a/src/HOL/Tools/BNF/bnf_lfp_size.ML Fri Sep 26 15:10:02 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_size.ML Fri Sep 26 19:38:26 2014 +0200
@@ -93,8 +93,8 @@
val B_ify = Term.typ_subst_atomic (As ~~ Bs);
- val recs = map #co_rec fp_sugars;
- val rec_thmss = map #co_rec_thms fp_sugars;
+ val recs = map (#co_rec o #fp_co_induct_sugar) fp_sugars;
+ val rec_thmss = map (#co_rec_thms o #fp_co_induct_sugar) fp_sugars;
val rec_Ts as rec_T1 :: _ = map fastype_of recs;
val rec_arg_Ts = binder_fun_types rec_T1;
val Cs = map body_type rec_Ts;
@@ -283,7 +283,7 @@
val pre_map_defs = map map_def_of_bnf pre_bnfs;
val live_nesting_map_ident0s = map map_ident0_of_bnf live_nesting_bnfs;
val abs_inverses = map (#abs_inverse o #absT_info) fp_sugars;
- val rec_defs = map #co_rec_def fp_sugars;
+ val rec_defs = map (#co_rec_def o #fp_co_induct_sugar) fp_sugars;
val gmaps = map (fn map0 => Term.list_comb (mk_map live As Bs map0, live_gs)) maps0;
--- a/src/HOL/Tools/SMT/smt_datatypes.ML Fri Sep 26 15:10:02 2014 +0200
+++ b/src/HOL/Tools/SMT/smt_datatypes.ML Fri Sep 26 19:38:26 2014 +0200
@@ -71,13 +71,13 @@
| info :: _ => (map (pair (hd fps)) (get_typedef_decl info T Ts), ctxt))
in
(case BNF_FP_Def_Sugar.fp_sugar_of ctxt n of
- SOME {fp, fp_res = {Ts = fp_Ts, ...}, ctr_sugar, ...} =>
+ SOME {fp, fp_res = {Ts = fp_Ts, ...}, fp_ctr_sugar = {ctr_sugar, ...}, ...} =>
if member (op =) fps fp then
let
val ns = map (fst o dest_Type) fp_Ts
val mutual_fp_sugars = map_filter (BNF_FP_Def_Sugar.fp_sugar_of ctxt) ns
val Xs = map #X mutual_fp_sugars
- val ctrXs_Tsss = map #ctrXs_Tss mutual_fp_sugars
+ val ctrXs_Tsss = map (#ctrXs_Tss o #fp_ctr_sugar) mutual_fp_sugars
(* Datatypes nested through datatypes and codatatypes nested through codatatypes are
allowed. So are mutually (co)recursive (co)datatypes. *)
--- a/src/HOL/Tools/Transfer/transfer_bnf.ML Fri Sep 26 15:10:02 2014 +0200
+++ b/src/HOL/Tools/Transfer/transfer_bnf.ML Fri Sep 26 19:38:26 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}])