# HG changeset patch
# User kuncar
# Date 1397144896 -7200
# Node ID 20cfb18a53ba1d625071ad6b8cd399ef6ba5d3d1
# Parent  3373f5d1e07480bfbb889358957a173e12ceba86
export theorems

diff -r 3373f5d1e074 -r 20cfb18a53ba src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
--- 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'
diff -r 3373f5d1e074 -r 20cfb18a53ba src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML
--- 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
diff -r 3373f5d1e074 -r 20cfb18a53ba src/HOL/Tools/BNF/bnf_util.ML
--- 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