--- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML Mon Sep 09 13:47:58 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML Mon Sep 09 14:22:11 2013 +0200
@@ -18,6 +18,7 @@
ctr_defss: thm list list,
ctr_sugars: BNF_Ctr_Sugar.ctr_sugar list,
co_iterss: term list list,
+ mapss: thm list list,
co_inducts: thm list,
co_iter_thmsss: thm list list list,
disc_co_itersss: thm list list list,
@@ -120,6 +121,7 @@
ctr_defss: thm list list,
ctr_sugars: ctr_sugar list,
co_iterss: term list list,
+ mapss: thm list list,
co_inducts: thm list,
co_iter_thmsss: thm list list list,
disc_co_itersss: thm list list list,
@@ -132,13 +134,14 @@
T1 = T2 andalso fp1 = fp2 andalso index1 = index2 andalso eq_fp_result (fp_res1, fp_res2);
fun morph_fp_sugar phi {T, fp, index, pre_bnfs, nested_bnfs, nesting_bnfs, fp_res, ctr_defss,
- ctr_sugars, co_iterss, co_inducts, co_iter_thmsss, disc_co_itersss, sel_co_iterssss} =
+ ctr_sugars, co_iterss, mapss, co_inducts, co_iter_thmsss, disc_co_itersss, sel_co_iterssss} =
{T = Morphism.typ phi T, fp = fp, index = index, pre_bnfs = map (morph_bnf phi) pre_bnfs,
nested_bnfs = map (morph_bnf phi) nested_bnfs, nesting_bnfs = map (morph_bnf phi) nesting_bnfs,
fp_res = morph_fp_result phi fp_res,
ctr_defss = map (map (Morphism.thm phi)) ctr_defss,
ctr_sugars = map (morph_ctr_sugar phi) ctr_sugars,
co_iterss = map (map (Morphism.term phi)) co_iterss,
+ mapss = map (map (Morphism.thm phi)) mapss,
co_inducts = map (Morphism.thm phi) co_inducts,
co_iter_thmsss = map (map (map (Morphism.thm phi))) co_iter_thmsss,
disc_co_itersss = map (map (map (Morphism.thm phi))) disc_co_itersss,
@@ -167,12 +170,12 @@
(fn phi => Data.map (Symtab.default (key, morph_fp_sugar phi fp_sugar)));
fun register_fp_sugars fp pre_bnfs nested_bnfs nesting_bnfs (fp_res as {Ts, ...}) ctr_defss
- ctr_sugars co_iterss co_inducts co_iter_thmsss disc_co_itersss sel_co_iterssss lthy =
+ ctr_sugars co_iterss mapss co_inducts co_iter_thmsss disc_co_itersss sel_co_iterssss lthy =
(0, lthy)
|> fold (fn T as Type (s, _) => fn (kk, lthy) => (kk + 1,
register_fp_sugar s {T = T, fp = fp, index = kk, pre_bnfs = pre_bnfs,
nested_bnfs = nested_bnfs, nesting_bnfs = nesting_bnfs, fp_res = fp_res,
- ctr_defss = ctr_defss, ctr_sugars = ctr_sugars, co_iterss = co_iterss,
+ ctr_defss = ctr_defss, ctr_sugars = ctr_sugars, co_iterss = co_iterss, mapss = mapss,
co_inducts = co_inducts, co_iter_thmsss = co_iter_thmsss, disc_co_itersss = disc_co_itersss,
sel_co_iterssss = sel_co_iterssss}
lthy)) Ts
@@ -1414,7 +1417,7 @@
@ rel_distincts @ flat setss);
fun derive_and_note_induct_iters_thms_for_types
- ((((mapsx, rel_injects, rel_distincts, setss), (ctrss, _, ctr_defss, ctr_sugars)),
+ ((((mapss, rel_injects, rel_distincts, setss), (ctrss, _, ctr_defss, ctr_sugars)),
(iterss, iter_defss)), lthy) =
let
val ((induct_thms, induct_thm, induct_attrs), (fold_thmss, fold_attrs),
@@ -1426,7 +1429,7 @@
val induct_type_attr = Attrib.internal o K o Induct.induct_type;
val simp_thmss =
- mk_simp_thmss ctr_sugars fold_thmss rec_thmss mapsx rel_injects rel_distincts setss;
+ mk_simp_thmss ctr_sugars fold_thmss rec_thmss mapss rel_injects rel_distincts setss;
val common_notes =
(if nn > 1 then [(inductN, [induct_thm], induct_attrs)] else [])
@@ -1442,11 +1445,11 @@
lthy
|> Local_Theory.notes (common_notes @ notes) |> snd
|> register_fp_sugars Least_FP pre_bnfs nested_bnfs nesting_bnfs fp_res ctr_defss ctr_sugars
- iterss [induct_thm] (transpose [fold_thmss, rec_thmss]) [] []
+ iterss mapss [induct_thm] (transpose [fold_thmss, rec_thmss]) [] []
end;
fun derive_and_note_coinduct_coiters_thms_for_types
- ((((mapsx, rel_injects, rel_distincts, setss), (_, _, ctr_defss, ctr_sugars)),
+ ((((mapss, rel_injects, rel_distincts, setss), (_, _, ctr_defss, ctr_sugars)),
(coiterss, coiter_defss)), lthy) =
let
val (([(coinduct_thms, coinduct_thm), (strong_coinduct_thms, strong_coinduct_thm)],
@@ -1472,7 +1475,7 @@
mk_simp_thmss ctr_sugars
(map3 flat_coiter_thms safe_unfold_thmss disc_unfold_thmss sel_unfold_thmss)
(map3 flat_coiter_thms safe_corec_thmss disc_corec_thmss sel_corec_thmss)
- mapsx rel_injects rel_distincts setss;
+ mapss rel_injects rel_distincts setss;
val anonymous_notes =
[(flat safe_unfold_thmss @ flat safe_corec_thmss, simp_attrs)]
@@ -1504,7 +1507,7 @@
lthy
|> Local_Theory.notes (anonymous_notes @ common_notes @ notes) |> snd
|> register_fp_sugars Greatest_FP pre_bnfs nested_bnfs nesting_bnfs fp_res ctr_defss
- ctr_sugars coiterss [coinduct_thm, strong_coinduct_thm]
+ ctr_sugars coiterss mapss [coinduct_thm, strong_coinduct_thm]
(transpose [unfold_thmss, corec_thmss]) (transpose [disc_unfold_thmss, disc_corec_thmss])
(transpose [sel_unfold_thmsss, sel_corec_thmsss])
end;