# HG changeset patch
# User desharna
# Date 1412595408 -7200
# Node ID 15337ad0537030cccf01249d09d86d5ef7ff1e7e
# Parent  1f4a2d8142fef0262a7241f3ef3fff2e0e2e4a88
add 'set_inducts' to 'fp_sugar'

diff -r 1f4a2d8142fe -r 15337ad05370 src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Mon Oct 06 13:36:47 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Mon Oct 06 13:36:48 2014 +0200
@@ -43,7 +43,8 @@
      co_rec_transfers: thm list,
      common_rel_co_inducts: thm list,
      rel_co_inducts: thm list,
-     common_set_inducts: thm list}
+     common_set_inducts: thm list,
+     set_inducts: thm list}
 
   type fp_sugar =
     {T: typ,
@@ -213,7 +214,8 @@
    co_rec_transfers: thm list,
    common_rel_co_inducts: thm list,
    rel_co_inducts: thm list,
-   common_set_inducts: thm list};
+   common_set_inducts: thm list,
+   set_inducts: thm list};
 
 type fp_sugar =
   {T: typ,
@@ -247,7 +249,7 @@
 
 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_disc_iffs, co_rec_selss, co_rec_codes, co_rec_transfers,
-    common_rel_co_inducts, rel_co_inducts, common_set_inducts} : fp_co_induct_sugar) =
+    common_rel_co_inducts, rel_co_inducts, common_set_inducts, set_inducts} : 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,
@@ -260,7 +262,8 @@
    co_rec_transfers = map (Morphism.thm phi) co_rec_transfers,
    common_rel_co_inducts = map (Morphism.thm phi) common_rel_co_inducts,
    rel_co_inducts = map (Morphism.thm phi) rel_co_inducts,
-   common_set_inducts = map (Morphism.thm phi) common_set_inducts};
+   common_set_inducts = map (Morphism.thm phi) common_set_inducts,
+   set_inducts = map (Morphism.thm phi) set_inducts};
 
 fun morph_fp_ctr_sugar phi ({ctrXs_Tss, ctr_defs, ctr_sugar, ctr_transfers, case_transfers,
     disc_transfers} : fp_ctr_sugar) =
@@ -340,7 +343,8 @@
     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 rel_intross rel_casess set_thmss set_selss
     set_intross set_casess ctr_transferss case_transferss disc_transferss co_rec_disc_iffss
-    co_rec_codess co_rec_transferss common_rel_co_inducts rel_co_inductss common_set_inducts noted =
+    co_rec_codess co_rec_transferss common_rel_co_inducts rel_co_inductss common_set_inducts
+    set_inductss noted =
   let
     val fp_sugars =
       map_index (fn (kk, T) =>
@@ -380,7 +384,8 @@
             co_rec_transfers = nth co_rec_transferss kk,
             common_rel_co_inducts = common_rel_co_inducts,
             rel_co_inducts = nth rel_co_inductss kk,
-            common_set_inducts = common_set_inducts}}
+            common_set_inducts = common_set_inducts,
+            set_inducts = nth set_inductss kk}}
         |> morph_fp_sugar (substitute_noted_thm noted)) Ts;
   in
     register_fp_sugars_raw fp_sugars
@@ -2228,7 +2233,7 @@
           (replicate nn []) rel_injectss rel_distinctss map_disc_iffss map_selss rel_selss
           rel_intross rel_casess set_thmss set_selss set_intross set_casess ctr_transferss
           case_transferss disc_transferss (replicate nn []) (replicate nn []) rec_transfer_thmss
-          common_rel_induct_thms rel_induct_thmss []
+          common_rel_induct_thms rel_induct_thmss [] (replicate nn [])
       end;
 
     fun derive_corec_transfer_thms lthy corecs corec_defs =
@@ -2348,6 +2353,7 @@
           rel_intross rel_casess set_thmss set_selss set_intross set_casess ctr_transferss
           case_transferss disc_transferss corec_disc_iff_thmss (map single corec_code_thms)
           corec_transfer_thmss common_rel_coinduct_thms rel_coinduct_thmss set_induct_thms
+          (replicate nn (if nn = 1 then set_induct_thms else []))
       end;
 
     val lthy'' = lthy'
diff -r 1f4a2d8142fe -r 15337ad05370 src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML	Mon Oct 06 13:36:47 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML	Mon Oct 06 13:36:48 2014 +0200
@@ -297,7 +297,7 @@
               fp_bnf_sugar = {map_disc_iffs, map_sels, rel_injects, rel_distincts, rel_sels,
                 rel_intros, rel_cases, set_thms, set_sels, set_intros, set_cases, ...},
               fp_co_induct_sugar = {co_rec_disc_iffs, co_rec_codes, co_rec_transfers,
-                common_rel_co_inducts, rel_co_inducts, common_set_inducts, ...},
+                common_rel_co_inducts, rel_co_inducts, common_set_inducts, set_inducts, ...},
               ...} : 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,
@@ -335,7 +335,8 @@
               co_rec_transfers = co_rec_transfers,
               common_rel_co_inducts = common_rel_co_inducts,
               rel_co_inducts = rel_co_inducts,
-              common_set_inducts = common_set_inducts}}
+              common_set_inducts = common_set_inducts,
+              set_inducts = set_inducts}}
           |> morph_fp_sugar phi;
 
         val target_fp_sugars =
diff -r 1f4a2d8142fe -r 15337ad05370 src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML	Mon Oct 06 13:36:47 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML	Mon Oct 06 13:36:48 2014 +0200
@@ -109,7 +109,8 @@
         co_rec_transfers = [],
         common_rel_co_inducts = [],
         rel_co_inducts = [],
-        common_set_inducts = []}}
+        common_set_inducts = [],
+        set_inducts = []}}
   end;
 
 fun fp_sugar_of_prod ctxt =
@@ -171,7 +172,8 @@
         co_rec_transfers = [],
         common_rel_co_inducts = [],
         rel_co_inducts = [],
-        common_set_inducts = []}}
+        common_set_inducts = [],
+        set_inducts = []}}
   end;
 
 val _ = Theory.setup (map_local_theory (fn lthy =>