make (co)induct component of 'fp_sugar' optional, for the benefit of nonuniform (co)datatypes and other similar extensions

--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Mon Sep 12 20:31:28 2016 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Mon Sep 12 23:17:55 2016 +0200
@@ -64,7 +64,7 @@
      live_nesting_bnfs: BNF_Def.bnf list,
      fp_ctr_sugar: fp_ctr_sugar,
      fp_bnf_sugar: fp_bnf_sugar,
-     fp_co_induct_sugar: fp_co_induct_sugar}
+     fp_co_induct_sugar: fp_co_induct_sugar option}
 
   val transfer_plugin: string
 
@@ -311,7 +311,7 @@
    live_nesting_bnfs: bnf list,
    fp_ctr_sugar: fp_ctr_sugar,
    fp_bnf_sugar: fp_bnf_sugar,
-   fp_co_induct_sugar: fp_co_induct_sugar};
+   fp_co_induct_sugar: fp_co_induct_sugar option};
 
 val transfer_plugin = Plugin_Name.declare_setup @{binding transfer};
 
@@ -381,7 +381,7 @@
    live_nesting_bnfs = map (morph_bnf phi) live_nesting_bnfs,
    fp_ctr_sugar = morph_fp_ctr_sugar phi fp_ctr_sugar,
    fp_bnf_sugar = morph_fp_bnf_sugar phi fp_bnf_sugar,
-   fp_co_induct_sugar = morph_fp_co_induct_sugar phi fp_co_induct_sugar};
+   fp_co_induct_sugar = Option.map (morph_fp_co_induct_sugar phi) fp_co_induct_sugar};
 
 val transfer_fp_sugar = morph_fp_sugar o Morphism.transfer_morphism;
 
@@ -426,8 +426,8 @@
     map_thmss common_co_inducts co_inductss co_rec_thmss co_rec_discss co_rec_selsss rel_injectss
     rel_distinctss map_disc_iffss map_selsss rel_selss rel_intross rel_casess pred_injectss
     set_thmss set_selsssss set_introsssss 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 set_inductss sel_transferss co_rec_o_mapss noted =
+    sel_transferss co_rec_disc_iffss co_rec_codess co_rec_transferss common_rel_co_inducts
+    rel_co_inductss common_set_inducts set_inductss co_rec_o_mapss noted =
   let
     val fp_sugars =
       map_index (fn (kk, T) =>
@@ -458,7 +458,7 @@
             set_selssss = nth set_selsssss kk,
             set_introssss = nth set_introsssss kk,
             set_cases = nth set_casess kk},
-         fp_co_induct_sugar =
+         fp_co_induct_sugar = SOME
            {co_rec = nth co_recs kk,
             common_co_inducts = common_co_inducts,
             co_inducts = nth co_inductss kk,
@@ -2653,9 +2653,9 @@
           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_selsss rel_selss
           rel_intross rel_casess pred_injectss set_thmss set_selsssss set_introsssss set_casess
-          ctr_transferss case_transferss disc_transferss (replicate nn []) (replicate nn [])
-          rec_transfer_thmss common_rel_induct_thms rel_induct_thmss [] (replicate nn [])
-          sel_transferss rec_o_map_thmss
+          ctr_transferss case_transferss disc_transferss sel_transferss (replicate nn [])
+          (replicate nn []) rec_transfer_thmss common_rel_induct_thms rel_induct_thmss []
+          (replicate nn []) rec_o_map_thmss
       end;
 
     fun derive_corec_transfer_thms lthy corecs corec_defs =
@@ -2829,10 +2829,10 @@
           (transpose [coinduct_thms, coinduct_strong_thms]) corec_thmss corec_disc_thmss
           corec_sel_thmsss rel_injectss rel_distinctss map_disc_iffss map_selsss rel_selss
           rel_intross rel_casess pred_injectss set_thmss set_selsssss set_introsssss set_casess
-          ctr_transferss case_transferss disc_transferss corec_disc_iff_thmss
+          ctr_transferss case_transferss disc_transferss sel_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 []))
-          sel_transferss map_o_corec_thmss
+          map_o_corec_thmss
       end;
 
     val lthy = lthy

--- a/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML	Mon Sep 12 20:31:28 2016 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML	Mon Sep 12 23:17:55 2016 +0200
@@ -304,7 +304,7 @@
               fp_bnf_sugar = {map_disc_iffs, map_selss, rel_injects, rel_distincts, rel_sels,
                 rel_intros, rel_cases, pred_injects, set_thms, set_selssss, set_introssss,
                 set_cases, ...},
-              fp_co_induct_sugar = {co_rec_disc_iffs, co_rec_codes, co_rec_transfers,
+              fp_co_induct_sugar = SOME {co_rec_disc_iffs, co_rec_codes, co_rec_transfers,
                 co_rec_o_maps, common_rel_co_inducts, rel_co_inducts, common_set_inducts,
                 set_inducts, ...},
               ...} : fp_sugar) =
@@ -334,7 +334,7 @@
               set_selssss = set_selssss,
               set_introssss = set_introssss,
               set_cases = set_cases},
-           fp_co_induct_sugar =
+           fp_co_induct_sugar = SOME
              {co_rec = co_rec,
               common_co_inducts = common_co_inducts,
               co_inducts = co_inducts,
@@ -421,8 +421,9 @@
 
     fun the_fp_sugar_of (T as Type (T_name, _)) =
       (case fp_sugar_of lthy T_name of
-        SOME (fp_sugar as {fp = fp', ...}) => if fp = fp' then fp_sugar else not_co_datatype T
-      | NONE => not_co_datatype T);
+        SOME (fp_sugar as {fp = fp', fp_co_induct_sugar = SOME _, ...}) =>
+        if fp = fp' then fp_sugar else not_co_datatype T
+      | _ => not_co_datatype T);
 
     fun gather_types _ _ rev_seens gen_seen [] = (rev rev_seens, gen_seen)
       | gather_types lthy rho rev_seens gen_seen ((T as Type (_, tyargs)) :: Ts) =

--- a/src/HOL/Tools/BNF/bnf_fp_rec_sugar_transfer.ML	Mon Sep 12 20:31:28 2016 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_rec_sugar_transfer.ML	Mon Sep 12 23:17:55 2016 +0200
@@ -157,7 +157,7 @@
      in
        Goal.prove lthy vars [] goal (fn {context = ctxt, prems = _} =>
          mk_gfp_rec_sugar_transfer_tac ctxt def
-           (#co_rec_def (#fp_co_induct_sugar (nth fp_sugars kk)))
+           (#co_rec_def (the (#fp_co_induct_sugar (nth fp_sugars kk))))
            (map (#type_definition o #absT_info) fp_sugars)
            (maps (#xtor_co_rec_transfers o #fp_res) fp_sugars)
            (map (rel_def_of_bnf o #pre_bnf) fp_sugars)

--- a/src/HOL/Tools/BNF/bnf_gfp_grec.ML	Mon Sep 12 20:31:28 2016 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp_grec.ML	Mon Sep 12 23:17:55 2016 +0200
@@ -2110,7 +2110,7 @@
 
     val sig_fp_bnf_sugar = #fp_bnf_sugar sig_fp_sugar;
     val ssig_fp_bnf_sugar = #fp_bnf_sugar ssig_fp_sugar;
-    val ssig_fp_induct_sugar = #fp_co_induct_sugar ssig_fp_sugar;
+    val ssig_fp_induct_sugar = the (#fp_co_induct_sugar ssig_fp_sugar);
 
     val sig_ctr_sugar = #ctr_sugar sig_fp_ctr_sugar;
     val ssig_ctr_sugar = #ctr_sugar ssig_fp_ctr_sugar;
@@ -2331,8 +2331,8 @@
     val sig_fp_bnf_sugar = #fp_bnf_sugar sig_fp_sugar;
     val old_ssig_fp_bnf_sugar = #fp_bnf_sugar old_ssig_fp_sugar;
     val ssig_fp_bnf_sugar = #fp_bnf_sugar ssig_fp_sugar;
-    val old_ssig_fp_induct_sugar = #fp_co_induct_sugar old_ssig_fp_sugar;
-    val ssig_fp_induct_sugar = #fp_co_induct_sugar ssig_fp_sugar;
+    val old_ssig_fp_induct_sugar = the (#fp_co_induct_sugar old_ssig_fp_sugar);
+    val ssig_fp_induct_sugar = the (#fp_co_induct_sugar ssig_fp_sugar);
 
     val old_ssig_ctr_sugar = #ctr_sugar old_ssig_fp_ctr_sugar;
     val sig_ctr_sugar = #ctr_sugar sig_fp_ctr_sugar;
@@ -2683,9 +2683,9 @@
     val old1_ssig_fp_bnf_sugar = #fp_bnf_sugar old1_ssig_fp_sugar;
     val old2_ssig_fp_bnf_sugar = #fp_bnf_sugar old2_ssig_fp_sugar;
     val ssig_fp_bnf_sugar = #fp_bnf_sugar ssig_fp_sugar;
-    val old1_ssig_fp_induct_sugar = #fp_co_induct_sugar old1_ssig_fp_sugar;
-    val old2_ssig_fp_induct_sugar = #fp_co_induct_sugar old2_ssig_fp_sugar;
-    val ssig_fp_induct_sugar = #fp_co_induct_sugar ssig_fp_sugar;
+    val old1_ssig_fp_induct_sugar = the (#fp_co_induct_sugar old1_ssig_fp_sugar);
+    val old2_ssig_fp_induct_sugar = the (#fp_co_induct_sugar old2_ssig_fp_sugar);
+    val ssig_fp_induct_sugar = the (#fp_co_induct_sugar ssig_fp_sugar);
 
     val old1_ssig_ctr_sugar = #ctr_sugar old1_ssig_fp_ctr_sugar;
     val old2_ssig_ctr_sugar = #ctr_sugar old2_ssig_fp_ctr_sugar;

--- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Mon Sep 12 20:31:28 2016 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Mon Sep 12 23:17:55 2016 +0200
@@ -501,7 +501,7 @@
     val thy = Proof_Context.theory_of lthy0;
 
     val ((missing_res_Ts, perm0_kks, fp_sugars as {fp_nesting_bnfs,
-          fp_co_induct_sugar = {common_co_inducts = common_coinduct_thms, ...}, ...} :: _,
+          fp_co_induct_sugar = SOME {common_co_inducts = common_coinduct_thms, ...}, ...} :: _,
           (_, gfp_sugar_thms)), lthy) =
       nested_to_mutual_fps (K true) Greatest_FP bs res_Ts callers callssss0 lthy0;
 
@@ -525,7 +525,8 @@
     val perm_Ts = map #T perm_fp_sugars;
     val perm_Xs = map #X perm_fp_sugars;
     val perm_Cs =
-      map (domain_type o body_fun_type o fastype_of o #co_rec o #fp_co_induct_sugar) perm_fp_sugars;
+      map (domain_type o body_fun_type o fastype_of o #co_rec o the o #fp_co_induct_sugar)
+        perm_fp_sugars;
     val Xs_TCs = perm_Xs ~~ (perm_Ts ~~ perm_Cs);
 
     fun zip_corecT (Type (s, Us)) = [Type (s, map (mk_sumTN o zip_corecT) Us)]
@@ -592,8 +593,9 @@
       end;
 
     fun mk_spec ({T, fp_ctr_sugar = {ctr_sugar as {exhaust_discs, sel_defs, ...}, ...},
-        fp_co_induct_sugar = {co_rec = corec, co_rec_thms = corec_thms, co_rec_discs = corec_discs,
-        co_rec_selss = corec_selss, ...}, ...} : fp_sugar) p_is q_isss f_isss f_Tsss =
+        fp_co_induct_sugar = SOME {co_rec = corec, co_rec_thms = corec_thms,
+        co_rec_discs = corec_discs, co_rec_selss = corec_selss, ...}, ...} : fp_sugar) p_is q_isss
+        f_isss f_Tsss =
       {T = T, corec = mk_co_rec thy Greatest_FP perm_Cs' (substAT T) corec,
        exhaust_discs = exhaust_discs, sel_defs = sel_defs,
        fp_nesting_maps = maps (map_thms_of_type lthy o T_of_bnf) fp_nesting_bnfs,

--- a/src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML	Mon Sep 12 20:31:28 2016 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML	Mon Sep 12 23:17:55 2016 +0200
@@ -104,7 +104,7 @@
           [[[]], [@{thms setr.intros[OF refl]}]]],
         set_cases = @{thms setl.cases[simplified hypsubst_in_prems]
           setr.cases[simplified hypsubst_in_prems]}},
-     fp_co_induct_sugar =
+     fp_co_induct_sugar = SOME
        {co_rec = Const (@{const_name case_sum}, map (fn Ts => (Ts ---> C)) ctr_Tss ---> fpT --> C),
         common_co_inducts = @{thms sum.induct},
         co_inducts = @{thms sum.induct},
@@ -176,7 +176,7 @@
           [[[], @{thms snds.intros[of "(a, b)" for a b, simplified snd_conv]}]]],
         set_cases = @{thms fsts.cases[simplified eq_fst_iff ex_neg_all_pos]
           snds.cases[simplified eq_snd_iff ex_neg_all_pos]}},
-     fp_co_induct_sugar =
+     fp_co_induct_sugar = SOME
        {co_rec = Const (@{const_name case_prod}, (ctr_Ts ---> C) --> fpT --> C),
         common_co_inducts = @{thms prod.induct},
         co_inducts = @{thms prod.induct},

--- a/src/HOL/Tools/BNF/bnf_lfp_compat.ML	Mon Sep 12 20:31:28 2016 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_compat.ML	Mon Sep 12 23:17:55 2016 +0200
@@ -214,9 +214,9 @@
 
     fun checked_fp_sugar_of s =
       (case fp_sugar_of lthy s of
-        SOME (fp_sugar as {fp, ...}) =>
+        SOME (fp_sugar as {fp, fp_co_induct_sugar = SOME _, ...}) =>
         if member (op =) prefs Include_GFPs orelse fp = Least_FP then fp_sugar else not_datatype s
-      | NONE => not_datatype s);
+      | _ => not_datatype s);
 
     val fpTs0 as Type (_, var_As) :: _ =
       map (#T o checked_fp_sugar_of o fst o dest_Type)
@@ -299,10 +299,10 @@
     val Xs' = map #X fp_sugars';
     val ctrXs_Tsss' = map (map (map substAT) o #ctrXs_Tss o #fp_ctr_sugar) fp_sugars';
     val ctrss' = map2 mk_ctr_of fp_sugars' fpTs';
-    val {fp_co_induct_sugar = {common_co_inducts = induct :: _, ...}, ...} :: _ = fp_sugars';
-    val inducts = map (hd o #co_inducts o #fp_co_induct_sugar) fp_sugars';
-    val recs = map (#co_rec o #fp_co_induct_sugar) fp_sugars';
-    val rec_thmss = map (#co_rec_thms o #fp_co_induct_sugar) fp_sugars';
+    val {fp_co_induct_sugar = SOME {common_co_inducts = induct :: _, ...}, ...} :: _ = fp_sugars';
+    val inducts = map (hd o #co_inducts o the o #fp_co_induct_sugar) fp_sugars';
+    val recs = map (#co_rec o the o #fp_co_induct_sugar) fp_sugars';
+    val rec_thmss = map (#co_rec_thms o the o #fp_co_induct_sugar) fp_sugars';
 
     fun is_nested_rec_type (Type (@{type_name fun}, [_, T])) = member (op =) Xs' (body_type T)
       | is_nested_rec_type _ = false;

--- a/src/HOL/Tools/BNF/bnf_lfp_countable.ML	Mon Sep 12 20:31:28 2016 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_countable.ML	Mon Sep 12 23:17:55 2016 +0200
@@ -132,7 +132,7 @@
 
       fun lfp_sugar_of s =
         (case fp_sugar_of ctxt s of
-          SOME (fp_sugar as {fp = Least_FP, ...}) => fp_sugar
+          SOME (fp_sugar as {fp = Least_FP, fp_co_induct_sugar = SOME _, ...}) => fp_sugar
         | _ => not_datatype s);
 
       val fpTs0 as Type (_, var_As) :: _ =
@@ -153,16 +153,17 @@
             HOLogic.eq_const fpT $ x $ Bound 0));
 
       val fp_sugars as
-          {fp_nesting_bnfs, fp_co_induct_sugar = {common_co_inducts = induct :: _, ...}, ...} :: _ =
+          {fp_nesting_bnfs, fp_co_induct_sugar = SOME {common_co_inducts = induct :: _, ...},
+           ...} :: _ =
         map (the o fp_sugar_of ctxt o fst o dest_Type) fpTs0;
       val ctr_sugars = map (#ctr_sugar o #fp_ctr_sugar) fp_sugars;
 
       val ctrss0 = map #ctrs ctr_sugars;
       val ns = map length ctrss0;
-      val recs0 = map (#co_rec o #fp_co_induct_sugar) fp_sugars;
+      val recs0 = map (#co_rec o the o #fp_co_induct_sugar) fp_sugars;
       val nchotomys = map #nchotomy ctr_sugars;
       val injectss = map #injects ctr_sugars;
-      val rec_thmss = map (#co_rec_thms o #fp_co_induct_sugar) fp_sugars;
+      val rec_thmss = map (#co_rec_thms o the o #fp_co_induct_sugar) fp_sugars;
       val map_comps' = map (unfold_thms ctxt @{thms comp_def} o map_comp_of_bnf) fp_nesting_bnfs;
       val inj_map_strongs' = map (Thm.permute_prems 0 ~1 o inj_map_strong_of_bnf) fp_nesting_bnfs;
 

--- a/src/HOL/Tools/BNF/bnf_lfp_rec_sugar_more.ML	Mon Sep 12 20:31:28 2016 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_rec_sugar_more.ML	Mon Sep 12 23:17:55 2016 +0200
@@ -28,12 +28,14 @@
 
 fun is_new_datatype _ @{type_name nat} = true
   | is_new_datatype ctxt s =
-    (case fp_sugar_of ctxt s of SOME {fp = Least_FP, ...} => true | _ => false);
+    (case fp_sugar_of ctxt s of
+      SOME {fp = Least_FP, fp_co_induct_sugar = SOME _, ...} => true
+    | _ => false);
 
 fun basic_lfp_sugar_of C fun_arg_Tsss ({T, fp_res_index, fp_ctr_sugar = {ctr_sugar, ...},
-    fp_co_induct_sugar = {co_rec = recx, co_rec_thms = rec_thms, ...}, ...} : fp_sugar) =
-  {T = T, fp_res_index = fp_res_index, C = C, fun_arg_Tsss = fun_arg_Tsss, ctr_sugar = ctr_sugar,
-   recx = recx, rec_thms = rec_thms};
+    fp_co_induct_sugar = SOME {co_rec = recx, co_rec_thms = rec_thms, ...}, ...} : fp_sugar) =
+    {T = T, fp_res_index = fp_res_index, C = C, fun_arg_Tsss = fun_arg_Tsss, ctr_sugar = ctr_sugar,
+     recx = recx, rec_thms = rec_thms};
 
 fun basic_lfp_sugars_of _ [@{typ nat}] _ _ lthy =
     ([], [0], [nat_basic_lfp_sugar], [], [], [], TrueI (*dummy*), [], false, lthy)
@@ -41,7 +43,7 @@
     let
       val ((missing_arg_Ts, perm0_kks,
             fp_sugars as {fp_nesting_bnfs,
-              fp_co_induct_sugar = {common_co_inducts = [common_induct], ...}, ...} :: _,
+              fp_co_induct_sugar = SOME {common_co_inducts = [common_induct], ...}, ...} :: _,
             (lfp_sugar_thms, _)), lthy) =
         nested_to_mutual_fps (K true) Least_FP bs arg_Ts callers callssss0 lthy0;
 
@@ -49,7 +51,7 @@
 
       val Ts = map #T fp_sugars;
       val Xs = map #X fp_sugars;
-      val Cs = map (body_type o fastype_of o #co_rec o #fp_co_induct_sugar) fp_sugars;
+      val Cs = map (body_type o fastype_of o #co_rec o the o #fp_co_induct_sugar) fp_sugars;
       val Xs_TCs = Xs ~~ (Ts ~~ Cs);
 
       fun zip_XrecT (Type (s, Us)) = [Type (s, map (HOLogic.mk_tupleT o zip_XrecT) Us)]

--- a/src/HOL/Tools/BNF/bnf_lfp_size.ML	Mon Sep 12 20:31:28 2016 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_size.ML	Mon Sep 12 23:17:55 2016 +0200
@@ -97,7 +97,8 @@
     rtac ctxt @{thm trans_less_add2}));
 
 fun generate_datatype_size (fp_sugars as ({T = Type (_, As), BT = Type (_, Bs), fp = Least_FP,
-        fp_res = {bnfs = fp_bnfs, ...}, fp_nesting_bnfs, live_nesting_bnfs, ...} : fp_sugar) :: _)
+        fp_res = {bnfs = fp_bnfs, ...}, fp_nesting_bnfs, live_nesting_bnfs,
+        fp_co_induct_sugar = SOME _, ...} : fp_sugar) :: _)
       lthy0 =
     let
       val data = Data.get (Context.Proof lthy0);
@@ -108,8 +109,8 @@
 
       val B_ify = Term.typ_subst_atomic (As ~~ Bs);
 
-      val recs = map (#co_rec o #fp_co_induct_sugar) fp_sugars;
-      val rec_thmss = map (#co_rec_thms o #fp_co_induct_sugar) fp_sugars;
+      val recs = map (#co_rec o the o #fp_co_induct_sugar) fp_sugars;
+      val rec_thmss = map (#co_rec_thms o the o #fp_co_induct_sugar) fp_sugars;
       val rec_Ts as rec_T1 :: _ = map fastype_of recs;
       val rec_arg_Ts = binder_fun_types rec_T1;
       val Cs = map body_type rec_Ts;
@@ -337,7 +338,7 @@
                 curry HOLogic.mk_eq) size_gen_o_map_lhss size_gen_o_map_rhss;
 
             val rec_o_maps =
-              fold_rev (curry (op @) o #co_rec_o_maps o #fp_co_induct_sugar) fp_sugars [];
+              fold_rev (curry (op @) o #co_rec_o_maps o the o #fp_co_induct_sugar) fp_sugars [];
 
             val size_gen_o_map_thmss =
               if nested_size_gen_o_maps_complete then

--- a/src/HOL/Tools/Transfer/transfer_bnf.ML	Mon Sep 12 20:31:28 2016 +0200
+++ b/src/HOL/Tools/Transfer/transfer_bnf.ML	Mon Sep 12 23:17:55 2016 +0200
@@ -248,7 +248,7 @@
     val fp_ctr_sugar = #fp_ctr_sugar fp_sugar
     val transfer_rules = #ctr_transfers fp_ctr_sugar @ #case_transfers fp_ctr_sugar
       @ #disc_transfers fp_ctr_sugar @ #sel_transfers fp_ctr_sugar
-      @ (#co_rec_transfers o #fp_co_induct_sugar) fp_sugar
+      @ these (Option.map #co_rec_transfers (#fp_co_induct_sugar fp_sugar))
     val transfer_attr = @{attributes [transfer_rule]}
   in
     map (fn thm => (Binding.empty_atts, [([thm], transfer_attr)])) transfer_rules