src/HOL/BNF/Tools/bnf_fp_sugar.ML

 
 signature BNF_FP_SUGAR =
 sig
   val datatypes: bool ->
     (mixfix list -> (string * sort) list option -> binding list -> typ list * typ list list ->
-      BNF_Def.BNF list -> local_theory ->
-      (BNF_Def.BNF list * term list * term list * term list * term list * thm * thm list *
-         thm list * thm list * thm list * thm list list * thm list * thm list * thm list) *
-      local_theory) ->
+      BNF_Def.BNF list -> local_theory -> BNF_FP.fp_result * local_theory) ->
     bool * ((((typ * sort) list * binding) * mixfix) * ((((binding * binding) *
       (binding * typ) list) * (binding * term) list) * mixfix) list) list ->
     local_theory -> local_theory
   val parse_datatype_cmd: bool ->
     (mixfix list -> (string * sort) list option -> binding list -> typ list * typ list list ->
-      BNF_Def.BNF list -> local_theory ->
-      (BNF_Def.BNF list * term list * term list * term list * term list * thm * thm list *
-         thm list * thm list * thm list * thm list list * thm list * thm list * thm list) *
-      local_theory) ->
+      BNF_Def.BNF list -> local_theory -> BNF_FP.fp_result * local_theory) ->
     (local_theory -> local_theory) parser
 end;
 
 structure BNF_FP_Sugar : BNF_FP_SUGAR =
 struct

 open BNF_Util
 open BNF_Wrap
 open BNF_Def
 open BNF_FP
 open BNF_FP_Sugar_Tactics
+
+val mp_conj = @{thm mp_conj};
 
 val simp_attrs = @{attributes [simp]};
 val code_simp_attrs = Code.add_default_eqn_attrib :: simp_attrs;
 
 fun split_list4 xs = (map #1 xs, map #2 xs, map #3 xs, map #4 xs);

 fun mk_map live Ts Us t =
   let val (Type (_, Ts0), Type (_, Us0)) = strip_typeN (live + 1) (fastype_of t) |>> List.last in
     Term.subst_atomic_types (Ts0 @ Us0 ~~ Ts @ Us) t
   end;
 
+fun mk_rel live Ts Us t =
+  let val [Type (_, Ts0), Type (_, Us0)] = binder_types (snd (strip_typeN live (fastype_of t))) in
+    Term.subst_atomic_types (Ts0 @ Us0 ~~ Ts @ Us) t
+  end;
+
 fun liveness_of_fp_bnf n bnf =
   (case T_of_bnf bnf of
     Type (_, Ts) => map (not o member (op =) (deads_of_bnf bnf)) Ts
   | _ => replicate n false);
 

   if length As = length As' then map2 merge_type_arg As As' else cannot_merge_types ();
 
 fun is_triv_implies thm =
   op aconv (Logic.dest_implies (Thm.prop_of thm))
   handle TERM _ => false;
+
+fun reassoc_conjs thm =
+  reassoc_conjs (thm RS @{thm conj_assoc[THEN iffD1]})
+  handle THM _ => thm;
 
 fun type_args_constrained_of (((cAs, _), _), _) = cAs;
 fun type_binding_of (((_, b), _), _) = b;
 fun mixfix_of ((_, mx), _) = mx;
 fun ctr_specs_of (_, ctr_specs) = ctr_specs;

     val _ = (case subtract (op =) (map dest_TFree As) rhs_As' of
         [] => ()
       | A' :: _ => error ("Extra type variable on right-hand side: " ^
           quote (Syntax.string_of_typ no_defs_lthy (TFree A'))));
 
-    fun eq_fpT (T as Type (s, Us)) (Type (s', Us')) =
+    fun eq_fpT_check (T as Type (s, Us)) (Type (s', Us')) =
         s = s' andalso (Us = Us' orelse error ("Illegal occurrence of recursive type " ^
           quote (Syntax.string_of_typ fake_lthy T)))
-      | eq_fpT _ _ = false;
+      | eq_fpT_check _ _ = false;
 
     fun freeze_fp (T as Type (s, Us)) =
-        (case find_index (eq_fpT T) fake_Ts of ~1 => Type (s, map freeze_fp Us) | j => nth Xs j)
+        (case find_index (eq_fpT_check T) fake_Ts of
+          ~1 => Type (s, map freeze_fp Us)
+        | kk => nth Xs kk)
       | freeze_fp T = T;
 
     val ctr_TsssXs = map (map (map freeze_fp)) fake_ctr_Tsss;
     val ctr_sum_prod_TsXs = map (mk_sumTN_balanced o map HOLogic.mk_tupleT) ctr_TsssXs;
 
     val fp_eqs =
       map dest_TFree Xs ~~ map (Term.typ_subst_atomic (As ~~ unsorted_As)) ctr_sum_prod_TsXs;
 
     (* TODO: clean up list *)
     val (pre_bnfs, ((fp_bnfs as any_fp_bnf :: _, dtors0, ctors0, fp_folds0, fp_recs0, fp_induct,
-           dtor_ctors, ctor_dtors, ctor_injects, fp_map_thms, fp_set_thmss, fp_rel_thms,
-           fp_fold_thms, fp_rec_thms), lthy)) =
+           fp_strong_induct, dtor_ctors, ctor_dtors, ctor_injects, fp_map_thms, fp_set_thmss,
+           fp_rel_thms, fp_fold_thms, fp_rec_thms), lthy)) =
       fp_bnf construct_fp fp_bs mixfixes (map dest_TFree unsorted_As) fp_eqs no_defs_lthy0;
 
     val timer = time (Timer.startRealTimer ());
 
     fun add_nesty_bnf_names Us =

 
     val pre_map_defs = map map_def_of_bnf pre_bnfs;
     val pre_set_defss = map set_defs_of_bnf pre_bnfs;
     val pre_rel_defs = map rel_def_of_bnf pre_bnfs;
     val nested_set_natural's = maps set_natural'_of_bnf nested_bnfs;
+    val nesting_map_ids = map map_id_of_bnf nesting_bnfs;
     val nesting_set_natural's = maps set_natural'_of_bnf nesting_bnfs;
-    val nesting_map_ids = map map_id_of_bnf nesting_bnfs;
 
     val live = live_of_bnf any_fp_bnf;
 
     val Bs =
       map3 (fn alive => fn A as TFree (_, S) => fn B => if alive then resort_tfree S B else A)

     val fp_fold_fun_Ts = fst (split_last (binder_types (fastype_of any_fp_fold)));
     val fp_rec_fun_Ts = fst (split_last (binder_types (fastype_of any_fp_rec)));
 
     val (((fold_only as (gss, _, _), rec_only as (hss, _, _)),
           (zs, cs, cpss, unfold_only as ((pgss, crgsss), _), corec_only as ((phss, cshsss), _))),
-         names_lthy) =
+         names_lthy0) =
       if lfp then
         let
           val y_Tsss =
             map3 (fn n => fn ms => map2 dest_tupleT ms o dest_sumTN_balanced n o domain_type)
               ns mss fp_fold_fun_Ts;

 
             val rel_infos = (ctr_defs' ~~ xss ~~ cxIns, ctr_defs' ~~ yss ~~ cyIns);
 
             fun mk_rel_thm postproc ctr_defs' xs cxIn ys cyIn =
               fold_thms lthy ctr_defs'
-                 (unfold_thms lthy (pre_rel_def ::
-                      (if lfp then [] else [dtor_ctor]) @ sum_prod_thms_rel)
+                 (unfold_thms lthy (pre_rel_def :: (if lfp then [] else [dtor_ctor]) @
+                      sum_prod_thms_rel)
                     (cterm_instantiate_pos (nones @ [SOME cxIn, SOME cyIn]) fp_rel_thm))
               |> postproc |> thaw (xs @ ys);
 
             fun mk_pos_rel_thm (((ctr_def', xs), cxIn), ((_, ys), cyIn)) =
-              mk_rel_thm (perhaps (try (fn th => th RS @{thm eq_sym_Unity_imp}))) [ctr_def']
-                xs cxIn ys cyIn;
+              mk_rel_thm (unfold_thms lthy @{thms eq_sym_Unity_conv}) [ctr_def'] xs cxIn ys cyIn;
 
             val pos_rel_thms = map mk_pos_rel_thm (op ~~ rel_infos);
 
             fun mk_half_neg_rel_thm (((xctr_def', xs), cxIn), ((yctr_def', ys), cyIn)) =
               mk_rel_thm (fn thm => thm RS @{thm eq_False[THEN iffD1]}) [xctr_def', yctr_def']

     fun build_map build_arg (Type (s, Ts)) (Type (_, Us)) =
       let
         val bnf = the (bnf_of lthy s);
         val live = live_of_bnf bnf;
         val mapx = mk_map live Ts Us (map_of_bnf bnf);
-        val TUs = map dest_funT (fst (strip_typeN live (fastype_of mapx)));
-        val args = map build_arg TUs;
-      in Term.list_comb (mapx, args) end;
+        val TUs' = map dest_funT (fst (strip_typeN live (fastype_of mapx)));
+      in Term.list_comb (mapx, map build_arg TUs') end;
 
     (* TODO: Add map, sets, rel simps *)
     val mk_simp_thmss =
-      map3 (fn (_, _, injects, distincts, cases, _, _, _) => fn rec_likes => fn fold_likes =>
+      map3 (fn (_, _, _, injects, distincts, cases, _, _, _) => fn rec_likes => fn fold_likes =>
         injects @ distincts @ cases @ rec_likes @ fold_likes);
 
     fun derive_induct_fold_rec_thms_for_types (((ctrss, xsss, ctr_defss, wrap_ress), (folds, recs,
         fold_defs, rec_defs)), lthy) =
       let
-        val (((phis, phis'), us'), names_lthy) =
+        val (((ps, ps'), us'), names_lthy) =
           lthy
           |> mk_Frees' "P" (map mk_pred1T fpTs)
           ||>> Variable.variant_fixes fp_b_names;
 
         val us = map2 (curry Free) us' fpTs;

                       val xysets = map (pair x) (ys ~~ sets);
                       val ppremss = map (mk_raw_prem_prems names_lthy') ys;
                     in
                       flat (map2 (map o apfst o cons) xysets ppremss)
                     end)
-                | i => [([], (i + 1, x))])
+                | kk => [([], (kk + 1, x))])
               | mk_raw_prem_prems _ _ = [];
 
             fun close_prem_prem xs t =
               fold_rev Logic.all (map Free (drop (nn + length xs)
-                (rev (Term.add_frees t (map dest_Free xs @ phis'))))) t;
+                (rev (Term.add_frees t (map dest_Free xs @ ps'))))) t;
 
             fun mk_prem_prem xs (xysets, (j, x)) =
               close_prem_prem xs (Logic.list_implies (map (fn (x', (y, set)) =>
                   HOLogic.mk_Trueprop (HOLogic.mk_mem (y, set $ x'))) xysets,
-                HOLogic.mk_Trueprop (nth phis (j - 1) $ x)));
+                HOLogic.mk_Trueprop (nth ps (j - 1) $ x)));
 
             fun mk_raw_prem phi ctr ctr_Ts =
               let
                 val (xs, names_lthy') = names_lthy |> mk_Frees "x" ctr_Ts;
                 val pprems = maps (mk_raw_prem_prems names_lthy') xs;
               in (xs, pprems, HOLogic.mk_Trueprop (phi $ Term.list_comb (ctr, xs))) end;
 
             fun mk_prem (xs, raw_pprems, concl) =
               fold_rev Logic.all xs (Logic.list_implies (map (mk_prem_prem xs) raw_pprems, concl));
 
-            val raw_premss = map3 (map2 o mk_raw_prem) phis ctrss ctr_Tsss;
+            val raw_premss = map3 (map2 o mk_raw_prem) ps ctrss ctr_Tsss;
 
             val goal =
               Library.foldr (Logic.list_implies o apfst (map mk_prem)) (raw_premss,
-                HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj (map2 (curry (op $)) phis us)));
+                HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj (map2 (curry (op $)) ps us)));
 
             val kksss = map (map (map (fst o snd) o #2)) raw_premss;
 
             val ctor_induct' = fp_induct OF (map mk_sumEN_tupled_balanced mss);
 
-            val induct_thm =
+            val thm =
               Skip_Proof.prove lthy [] [] goal (fn {context = ctxt, ...} =>
                 mk_induct_tac ctxt nn ns mss kksss (flat ctr_defss) ctor_induct'
                   nested_set_natural's pre_set_defss)
               |> singleton (Proof_Context.export names_lthy lthy)
+              |> Thm.close_derivation;
           in
-            `(conj_dests nn) induct_thm
+            `(conj_dests nn) thm
           end;
 
         (* TODO: Generate nicer names in case of clashes *)
         val induct_cases = Datatype_Prop.indexify_names (maps (map base_name_of_ctr) ctrss);
 

 
             fun mk_goal fss frec_like xctr f xs fxs =
               fold_rev (fold_rev Logic.all) (xs :: fss)
                 (mk_Trueprop_eq (frec_like $ xctr, Term.list_comb (f, fxs)));
 
-            fun build_call frec_likes maybe_tick (T, U) =
+            fun build_rec_like frec_likes maybe_tick (T, U) =
               if T = U then
                 id_const T
               else
                 (case find_index (curry (op =) T) fpTs of
-                  ~1 => build_map (build_call frec_likes maybe_tick) T U
-                | j => maybe_tick (nth us j) (nth frec_likes j));
+                  ~1 => build_map (build_rec_like frec_likes maybe_tick) T U
+                | kk => maybe_tick (nth us kk) (nth frec_likes kk));
 
             fun mk_U maybe_mk_prodT =
               typ_subst (map2 (fn fpT => fn C => (fpT, maybe_mk_prodT fpT C)) fpTs Cs);
 
-            fun intr_calls frec_likes maybe_cons maybe_tick maybe_mk_prodT (x as Free (_, T)) =
+            fun intr_rec_likes frec_likes maybe_cons maybe_tick maybe_mk_prodT (x as Free (_, T)) =
               if member (op =) fpTs T then
-                maybe_cons x [build_call frec_likes (K I) (T, mk_U (K I) T) $ x]
+                maybe_cons x [build_rec_like frec_likes (K I) (T, mk_U (K I) T) $ x]
               else if exists_fp_subtype T then
-                [build_call frec_likes maybe_tick (T, mk_U maybe_mk_prodT T) $ x]
+                [build_rec_like frec_likes maybe_tick (T, mk_U maybe_mk_prodT T) $ x]
               else
                 [x];
 
-            val gxsss = map (map (maps (intr_calls gfolds (K I) (K I) (K I)))) xsss;
-            val hxsss = map (map (maps (intr_calls hrecs cons tick (curry HOLogic.mk_prodT)))) xsss;
+            val gxsss = map (map (maps (intr_rec_likes gfolds (K I) (K I) (K I)))) xsss;
+            val hxsss =
+              map (map (maps (intr_rec_likes hrecs cons tick (curry HOLogic.mk_prodT)))) xsss;
 
             val fold_goalss = map5 (map4 o mk_goal gss) gfolds xctrss gss xsss gxsss;
             val rec_goalss = map5 (map4 o mk_goal hss) hrecs xctrss hss xsss hxsss;
 
             val fold_tacss =

                 ctr_defss;
             val rec_tacss =
               map2 (map o mk_rec_like_tac pre_map_defs nesting_map_ids rec_defs) fp_rec_thms
                 ctr_defss;
 
-            fun prove goal tac = Skip_Proof.prove lthy [] [] goal (tac o #context);
+            fun prove goal tac =
+              Skip_Proof.prove lthy [] [] goal (tac o #context)
+              |> Thm.close_derivation;
           in
             (map2 (map2 prove) fold_goalss fold_tacss,
              map2 (map2 prove) rec_goalss rec_tacss)
           end;
 

       end;
 
     fun derive_coinduct_unfold_corec_thms_for_types (((ctrss, _, ctr_defss, wrap_ress), (unfolds,
         corecs, unfold_defs, corec_defs)), lthy) =
       let
+        val nesting_rel_eqs = map rel_eq_of_bnf nesting_bnfs;
+
         val discss = map (map (mk_disc_or_sel As) o #1) wrap_ress;
-        val selsss = map #2 wrap_ress;
-        val disc_thmsss = map #6 wrap_ress;
-        val discIss = map #7 wrap_ress;
-        val sel_thmsss = map #8 wrap_ress;
-
-        val (us', _) =
+        val selsss = map (map (map (mk_disc_or_sel As)) o #2) wrap_ress;
+        val exhaust_thms = map #3 wrap_ress;
+        val disc_thmsss = map #7 wrap_ress;
+        val discIss = map #8 wrap_ress;
+        val sel_thmsss = map #9 wrap_ress;
+
+        val (((rs, us'), vs'), names_lthy) =
           lthy
-          |> Variable.variant_fixes fp_b_names;
+          |> mk_Frees "R" (map (fn T => mk_pred2T T T) fpTs)
+          ||>> Variable.variant_fixes fp_b_names
+          ||>> Variable.variant_fixes (map (suffix "'") fp_b_names);
 
         val us = map2 (curry Free) us' fpTs;
-
-        val (coinduct_thms, coinduct_thm) =
+        val udiscss = map2 (map o rapp) us discss;
+        val uselsss = map2 (map o map o rapp) us selsss;
+
+        val vs = map2 (curry Free) vs' fpTs;
+        val vdiscss = map2 (map o rapp) vs discss;
+        val vselsss = map2 (map o map o rapp) vs selsss;
+
+        val ((coinduct_thms, coinduct_thm), (strong_coinduct_thms, strong_coinduct_thm)) =
           let
+            val uvrs = map3 (fn r => fn u => fn v => r $ u $ v) rs us vs;
+            val uv_eqs = map2 (curry HOLogic.mk_eq) us vs;
+            val strong_rs =
+              map4 (fn u => fn v => fn uvr => fn uv_eq =>
+                fold_rev Term.lambda [u, v] (HOLogic.mk_disj (uvr, uv_eq))) us vs uvrs uv_eqs;
+
+            fun build_rel_step build_arg (Type (s, Ts)) =
+              let
+                val bnf = the (bnf_of lthy s);
+                val live = live_of_bnf bnf;
+                val rel = mk_rel live Ts Ts (rel_of_bnf bnf);
+                val Ts' = map domain_type (fst (strip_typeN live (fastype_of rel)));
+              in Term.list_comb (rel, map build_arg Ts') end;
+
+            fun build_rel rs' T =
+              (case find_index (curry (op =) T) fpTs of
+                ~1 =>
+                if exists_fp_subtype T then build_rel_step (build_rel rs') T
+                else HOLogic.eq_const T
+              | kk => nth rs' kk);
+
+            fun build_rel_app rs' usel vsel =
+              fold rapp [usel, vsel] (build_rel rs' (fastype_of usel));
+
+            fun mk_prem_ctr_concls rs' n k udisc usels vdisc vsels =
+              (if k = n then [] else [HOLogic.mk_eq (udisc, vdisc)]) @
+              (if null usels then
+                 []
+               else
+                 [Library.foldr HOLogic.mk_imp (if n = 1 then [] else [udisc, vdisc],
+                    Library.foldr1 HOLogic.mk_conj (map2 (build_rel_app rs') usels vsels))]);
+
+            fun mk_prem_concl rs' n udiscs uselss vdiscs vselss =
+              Library.foldr1 HOLogic.mk_conj
+                (flat (map5 (mk_prem_ctr_concls rs' n) (1 upto n) udiscs uselss vdiscs vselss))
+              handle List.Empty => @{term True};
+
+            fun mk_prem rs' uvr u v n udiscs uselss vdiscs vselss =
+              fold_rev Logic.all [u, v] (Logic.mk_implies (HOLogic.mk_Trueprop uvr,
+                HOLogic.mk_Trueprop (mk_prem_concl rs' n udiscs uselss vdiscs vselss)));
+
+            val concl =
+              HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
+                (map3 (fn uvr => fn u => fn v => HOLogic.mk_imp (uvr, HOLogic.mk_eq (u, v)))
+                   uvrs us vs));
+
+            fun mk_goal rs' =
+              Logic.list_implies (map8 (mk_prem rs') uvrs us vs ns udiscss uselsss vdiscss vselsss,
+                concl);
+
+            val goal = mk_goal rs;
+            val strong_goal = mk_goal strong_rs;
+
+            fun prove dtor_coinduct' goal =
+              Skip_Proof.prove lthy [] [] goal (fn {context = ctxt, ...} =>
+                mk_coinduct_tac ctxt nesting_rel_eqs nn ns dtor_coinduct' pre_rel_defs dtor_ctors
+                  exhaust_thms ctr_defss disc_thmsss sel_thmsss)
+              |> singleton (Proof_Context.export names_lthy lthy)
+              |> Thm.close_derivation;
+
             fun postproc nn thm =
               Thm.permute_prems 0 nn
-                (if nn = 1 then thm RS mp else funpow nn (fn thm => thm RS @{thm mp_conj}) thm)
-              |> Drule.zero_var_indexes;
-
-            val coinduct_thm = fp_induct;
+                (if nn = 1 then thm RS mp
+                 else funpow nn (fn thm => reassoc_conjs (thm RS mp_conj)) thm)
+              |> Drule.zero_var_indexes
+              |> `(conj_dests nn);
           in
-            `(conj_dests nn) coinduct_thm
+            (postproc nn (prove fp_induct goal), postproc nn (prove fp_strong_induct strong_goal))
           end;
 
         fun mk_maybe_not pos = not pos ? HOLogic.mk_not;
 
         val z = the_single zs;

             fun mk_goal pfss c cps fcorec_like n k ctr m cfs' =
               fold_rev (fold_rev Logic.all) ([c] :: pfss)
                 (Logic.list_implies (seq_conds (HOLogic.mk_Trueprop oo mk_maybe_not) n k cps,
                    mk_Trueprop_eq (fcorec_like $ c, Term.list_comb (ctr, take m cfs'))));
 
-            fun build_call frec_likes maybe_tack (T, U) =
+            fun build_corec_like fcorec_likes maybe_tack (T, U) =
               if T = U then
                 id_const T
               else
                 (case find_index (curry (op =) U) fpTs of
-                  ~1 => build_map (build_call frec_likes maybe_tack) T U
-                | j => maybe_tack (nth cs j, nth us j) (nth frec_likes j));
+                  ~1 => build_map (build_corec_like fcorec_likes maybe_tack) T U
+                | kk => maybe_tack (nth cs kk, nth us kk) (nth fcorec_likes kk));
 
             fun mk_U maybe_mk_sumT =
               typ_subst (map2 (fn C => fn fpT => (maybe_mk_sumT fpT C, fpT)) Cs fpTs);
 
-            fun intr_calls frec_likes maybe_mk_sumT maybe_tack cqf =
+            fun intr_corec_likes fcorec_likes maybe_mk_sumT maybe_tack cqf =
               let val T = fastype_of cqf in
                 if exists_subtype (member (op =) Cs) T then
-                  build_call frec_likes maybe_tack (T, mk_U maybe_mk_sumT T) $ cqf
+                  build_corec_like fcorec_likes maybe_tack (T, mk_U maybe_mk_sumT T) $ cqf
                 else
                   cqf
               end;
 
-            val crgsss' = map (map (map (intr_calls gunfolds (K I) (K I)))) crgsss;
-            val cshsss' = map (map (map (intr_calls hcorecs (curry mk_sumT) (tack z)))) cshsss;
+            val crgsss' = map (map (map (intr_corec_likes gunfolds (K I) (K I)))) crgsss;
+            val cshsss' =
+              map (map (map (intr_corec_likes hcorecs (curry mk_sumT) (tack z)))) cshsss;
 
             val unfold_goalss =
               map8 (map4 oooo mk_goal pgss) cs cpss gunfolds ns kss ctrss mss crgsss';
             val corec_goalss =
               map8 (map4 oooo mk_goal phss) cs cpss hcorecs ns kss ctrss mss cshsss';

             val corec_tacss =
               map3 (map oo mk_disc_corec_like_iff_tac) case_splitss' corec_thmss disc_thmsss;
 
             fun prove goal tac =
               Skip_Proof.prove lthy [] [] goal (tac o #context)
-              |> Thm.close_derivation
-              |> singleton (Proof_Context.export names_lthy no_defs_lthy);
+              |> singleton (Proof_Context.export names_lthy0 no_defs_lthy)
+              |> Thm.close_derivation;
 
             fun proves [_] [_] = []
               | proves goals tacs = map2 prove goals tacs;
           in
             (map2 proves unfold_goalss unfold_tacss,

         val anonymous_notes =
           [(flat safe_unfold_thmss @ flat safe_corec_thmss, simp_attrs)]
           |> map (fn (thms, attrs) => ((Binding.empty, attrs), [(thms, [])]));
 
         val common_notes =
-          (if nn > 1 then [(coinductN, [coinduct_thm], [])] (* FIXME: attribs *) else [])
+          (if nn > 1 then
+             (* FIXME: attribs *)
+             [(coinductN, [coinduct_thm], []),
+              (strong_coinductN, [strong_coinduct_thm], [])]
+           else
+             [])
           |> map (fn (thmN, thms, attrs) =>
             ((Binding.qualify true fp_common_name (Binding.name thmN), attrs), [(thms, [])]));
 
         val notes =
           [(coinductN, map single coinduct_thms, []), (* FIXME: attribs *)

            (disc_unfold_iffsN, disc_unfold_iff_thmss, simp_attrs),
            (disc_unfoldsN, disc_unfold_thmss, simp_attrs),
            (sel_unfoldsN, sel_unfold_thmss, simp_attrs),
            (sel_corecsN, sel_corec_thmss, simp_attrs),
            (simpsN, simp_thmss, []),
+           (strong_coinductN, map single strong_coinduct_thms, []), (* FIXME: attribs *)
            (unfoldsN, unfold_thmss, [])]
           |> maps (fn (thmN, thmss, attrs) =>
             map_filter (fn (_, []) => NONE | (b, thms) =>
               SOME ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), attrs),
                 [(thms, [])])) (fp_bs ~~ thmss));