src/HOL/Tools/BNF/bnf_fp_def_sugar.ML

--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Mon Oct 06 13:33:04 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Mon Oct 06 13:33:15 2014 +0200
@@ -19,7 +19,8 @@
      map_sels: thm list,
      rel_injects: thm list,
      rel_distincts: thm list,
-     rel_sels: thm list}
+     rel_sels: thm list,
+     rel_intros: thm list}
 
   type fp_co_induct_sugar =
     {co_rec: term,
@@ -174,7 +175,8 @@
    map_sels: thm list,
    rel_injects: thm list,
    rel_distincts: thm list,
-   rel_sels: thm list};
+   rel_sels: thm list,
+   rel_intros: thm list};
 
 type fp_co_induct_sugar =
   {co_rec: term,
@@ -201,13 +203,14 @@
    fp_co_induct_sugar: fp_co_induct_sugar};
 
 fun morph_fp_bnf_sugar phi ({map_thms, map_disc_iffs, map_sels, rel_injects, rel_distincts,
-    rel_sels} : fp_bnf_sugar) =
+    rel_sels, rel_intros} : fp_bnf_sugar) =
   {map_thms = map (Morphism.thm phi) map_thms,
    map_disc_iffs = map (Morphism.thm phi) map_disc_iffs,
    map_sels = map (Morphism.thm phi) map_sels,
    rel_injects = map (Morphism.thm phi) rel_injects,
    rel_distincts = map (Morphism.thm phi) rel_distincts,
-   rel_sels = map (Morphism.thm phi) rel_sels};
+   rel_sels = map (Morphism.thm phi) rel_sels,
+   rel_intros = map (Morphism.thm phi) rel_intros};
 
 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) =
@@ -291,7 +294,7 @@
 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 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 noted =
+    rel_distinctss map_disc_iffss map_selss rel_selss rel_intross noted =
   let
     val fp_sugars =
       map_index (fn (kk, T) =>
@@ -308,7 +311,8 @@
             map_sels = nth map_selss kk,
             rel_injects = nth rel_injectss kk,
             rel_distincts = nth rel_distinctss kk,
-            rel_sels = nth rel_selss kk},
+            rel_sels = nth rel_selss kk,
+            rel_intros = nth rel_intross kk},
          fp_co_induct_sugar =
            {co_rec = nth co_recs kk,
             common_co_inducts = common_co_inducts,
@@ -468,7 +472,7 @@
       distincts, distinct_discsss, ...} : ctr_sugar)
     lthy =
   if live = 0 then
-    (([],[], [], [], [], [], []), lthy)
+    (([], [], [], [], [], [], [], []), lthy)
   else
     let
       val n = length ctr_Tss;
@@ -954,6 +958,7 @@
         map subst rel_inject_thms,
         map subst rel_distinct_thms,
         map subst rel_sel_thms,
+        map subst rel_intro_thms,
         map (map subst) set0_thmss), lthy')
     end;
 
@@ -2058,7 +2063,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_list7 o split_list)
+      |>> apsnd split_list o apfst (apsnd split_list4 o apfst split_list8 o split_list)
         o split_list;
 
     fun mk_simp_thms ({injects, distincts, case_thms, ...} : ctr_sugar) co_recs map_thms rel_injects
@@ -2091,7 +2096,8 @@
       end;
 
     fun derive_note_induct_recs_thms_for_types
-        ((((map_thmss, map_disc_iffss, map_selss, rel_injectss, rel_distinctss, rel_selss, setss),
+        ((((map_thmss, map_disc_iffss, map_selss, rel_injectss, rel_distinctss, rel_selss,
+            rel_intross, setss),
            (ctrss, _, ctr_defss, ctr_sugars)),
           (recs, rec_defs)), lthy) =
       let
@@ -2150,7 +2156,7 @@
         |-> 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
           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_injectss rel_distinctss map_disc_iffss map_selss rel_selss rel_intross
       end;
 
     fun derive_corec_transfer_thms lthy corecs corec_defs =
@@ -2169,7 +2175,8 @@
       end;
 
     fun derive_note_coinduct_corecs_thms_for_types
-        ((((map_thmss, map_disc_iffss, map_selss, rel_injectss, rel_distinctss, rel_selss, setss),
+        ((((map_thmss, map_disc_iffss, map_selss, rel_injectss, rel_distinctss, rel_selss,
+            rel_intross, setss),
            (_, _, ctr_defss, ctr_sugars)),
           (corecs, corec_defs)), lthy) =
       let
@@ -2265,6 +2272,7 @@
           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 map_disc_iffss map_selss rel_selss
+          rel_intross
       end;
 
     val lthy'' = lthy'