--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Thu Apr 10 17:48:15 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Thu Apr 10 17:48:16 2014 +0200
@@ -26,7 +26,8 @@
co_inducts: thm list,
co_rec_thms: thm list,
disc_co_recs: thm list,
- sel_co_recss: thm list list};
+ sel_co_recss: thm list list,
+ rel_injects: thm list};
val morph_fp_sugar: morphism -> fp_sugar -> fp_sugar
val transfer_fp_sugar: Proof.context -> fp_sugar -> fp_sugar
@@ -139,11 +140,12 @@
co_inducts: thm list,
co_rec_thms: thm list,
disc_co_recs: thm list,
- sel_co_recss: thm list list};
+ sel_co_recss: thm list list,
+ rel_injects: thm list};
fun morph_fp_sugar phi ({T, X, fp, fp_res, fp_res_index, pre_bnf, absT_info, nested_bnfs,
nesting_bnfs, ctrXs_Tss, ctr_defs, ctr_sugar, co_rec, maps, common_co_inducts, co_inducts,
- co_rec_thms, disc_co_recs, sel_co_recss} : fp_sugar) =
+ co_rec_thms, disc_co_recs, sel_co_recss, rel_injects} : fp_sugar) =
{T = Morphism.typ phi T,
X = Morphism.typ phi X,
fp = fp,
@@ -162,7 +164,8 @@
co_inducts = map (Morphism.thm phi) co_inducts,
co_rec_thms = map (Morphism.thm phi) co_rec_thms,
disc_co_recs = map (Morphism.thm phi) disc_co_recs,
- sel_co_recss = map (map (Morphism.thm phi)) sel_co_recss};
+ sel_co_recss = map (map (Morphism.thm phi)) sel_co_recss,
+ rel_injects = map (Morphism.thm phi) rel_injects};
val transfer_fp_sugar = morph_fp_sugar o Morphism.transfer_morphism o Proof_Context.theory_of;
@@ -206,7 +209,7 @@
fun register_fp_sugars Xs fp pre_bnfs absT_infos nested_bnfs nesting_bnfs (fp_res as {Ts, ...})
ctrXs_Tsss ctr_defss ctr_sugars co_recs mapss common_co_inducts co_inductss co_rec_thmss
- disc_co_recss sel_co_recsss lthy =
+ disc_co_recss sel_co_recsss rel_injects lthy =
(0, lthy)
|> fold (fn T as Type (s, _) => fn (kk, lthy) => (kk + 1,
register_fp_sugar s {T = T, X = nth Xs kk, fp = fp, fp_res = fp_res, fp_res_index = kk,
@@ -215,7 +218,7 @@
ctr_sugar = nth ctr_sugars kk, co_rec = nth co_recs 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, disc_co_recs = nth disc_co_recss kk,
- sel_co_recss = nth sel_co_recsss kk}
+ sel_co_recss = nth sel_co_recsss kk, rel_injects = nth rel_injects kk}
lthy)) Ts
|> snd;
@@ -1349,7 +1352,7 @@
|> Local_Theory.notes (common_notes @ notes) |> snd
|> register_fp_sugars Xs Least_FP pre_bnfs absT_infos nested_bnfs nesting_bnfs fp_res
ctrXs_Tsss ctr_defss ctr_sugars recs' mapss [induct_thm] (map single induct_thms)
- rec_thmss' (replicate nn []) (replicate nn [])
+ rec_thmss' (replicate nn []) (replicate nn []) rel_injects
end;
fun derive_note_coinduct_corecs_thms_for_types
@@ -1403,7 +1406,7 @@
|> register_fp_sugars Xs Greatest_FP pre_bnfs absT_infos nested_bnfs nesting_bnfs fp_res
ctrXs_Tsss ctr_defss ctr_sugars corecs mapss [coinduct_thm, strong_coinduct_thm]
(transpose [coinduct_thms, strong_coinduct_thms]) corec_thmss disc_corec_thmss
- sel_corec_thmsss
+ sel_corec_thmsss rel_injects
end;
val lthy'' = lthy'
--- a/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML Thu Apr 10 17:48:15 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML Thu Apr 10 17:48:16 2014 +0200
@@ -275,18 +275,19 @@
val phi = Proof_Context.export_morphism no_defs_lthy no_defs_lthy0;
fun mk_target_fp_sugar T X kk pre_bnf absT_info ctrXs_Tss ctr_defs ctr_sugar co_rec maps
- co_inducts co_rec_thms disc_corec_thms sel_corec_thmss =
+ co_inducts co_rec_thms disc_corec_thms sel_corec_thmss rel_injects =
{T = T, X = X, fp = fp, fp_res = fp_res, fp_res_index = kk, pre_bnf = pre_bnf,
absT_info = absT_info, nested_bnfs = nested_bnfs, nesting_bnfs = nesting_bnfs,
ctrXs_Tss = ctrXs_Tss, ctr_defs = ctr_defs, ctr_sugar = ctr_sugar, co_rec = co_rec,
maps = maps, common_co_inducts = common_co_inducts, co_inducts = co_inducts,
co_rec_thms = co_rec_thms, disc_co_recs = disc_corec_thms,
- sel_co_recss = sel_corec_thmss}
+ sel_co_recss = sel_corec_thmss, rel_injects = rel_injects}
|> morph_fp_sugar phi;
val target_fp_sugars =
- map14 mk_target_fp_sugar fpTs Xs kks pre_bnfs absT_infos ctrXs_Tsss ctr_defss ctr_sugars
- co_recs mapss (transpose co_inductss) co_rec_thmss disc_corec_thmss sel_corec_thmsss;
+ map15 mk_target_fp_sugar fpTs Xs kks pre_bnfs absT_infos ctrXs_Tsss ctr_defss ctr_sugars
+ co_recs mapss (transpose co_inductss) co_rec_thmss disc_corec_thmss sel_corec_thmsss
+ (map #rel_injects fp_sugars0);
val n2m_sugar = (target_fp_sugars, fp_sugar_thms);
in
--- a/src/HOL/Tools/BNF/bnf_util.ML Thu Apr 10 17:48:15 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_util.ML Thu Apr 10 17:48:16 2014 +0200
@@ -35,6 +35,10 @@
'o) ->
'a list -> 'b list -> 'c list -> 'd list -> 'e list -> 'f list -> 'g list -> 'h list ->
'i list -> 'j list -> 'k list -> 'l list -> 'm list -> 'n list -> 'o list
+ val map15: ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h -> 'i -> 'j -> 'k -> 'l -> 'm -> 'n ->
+ 'o -> 'p) ->
+ 'a list -> 'b list -> 'c list -> 'd list -> 'e list -> 'f list -> 'g list -> 'h list ->
+ 'i list -> 'j list -> 'k list -> 'l list -> 'm list -> 'n list -> 'o list -> 'p list
val fold_map4: ('a -> 'b -> 'c -> 'd -> 'e -> 'f * 'e) ->
'a list -> 'b list -> 'c list -> 'd list -> 'e -> 'f list * 'e
val fold_map5: ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g * 'f) ->
@@ -203,6 +207,14 @@
map14 f x1s x2s x3s x4s x5s x6s x7s x8s x9s x10s x11s x12s x13s x14s
| map14 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ = raise ListPair.UnequalLengths;
+fun map15 _ [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] = []
+ | map15 f (x1::x1s) (x2::x2s) (x3::x3s) (x4::x4s) (x5::x5s) (x6::x6s) (x7::x7s) (x8::x8s)
+ (x9::x9s) (x10::x10s) (x11::x11s) (x12::x12s) (x13::x13s) (x14::x14s) (x15::x15s) =
+ f x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 ::
+ map15 f x1s x2s x3s x4s x5s x6s x7s x8s x9s x10s x11s x12s x13s x14s x15s
+ | map15 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ = raise ListPair.UnequalLengths;
+
+
fun fold_map4 _ [] [] [] [] acc = ([], acc)
| fold_map4 f (x1::x1s) (x2::x2s) (x3::x3s) (x4::x4s) acc =
let