src/HOL/BNF/Tools/bnf_gfp.ML

     val ctor_dtor_corec_thms =
       map3 mk_ctor_dtor_unfold_like_thm dtor_inject_thms dtor_ctor_thms dtor_corec_thms;
 
     val timer = time (timer "corec definitions & thms");
 
-    (* TODO: Get rid of strong versions (since these can easily be derived from the weak ones). *)
-    val (dtor_map_coinduct_thm, coinduct_params, dtor_coinduct_thm, dtor_strong_coinduct_thm) =
+    val (dtor_map_coinduct_thm, coinduct_params, dtor_coinduct_thm) =
       let
         val zs = Jzs1 @ Jzs2;
         val frees = phis @ zs;
-
-        fun mk_phi strong_eq phi z1 z2 = if strong_eq
-          then Term.absfree (dest_Free z1) (Term.absfree (dest_Free z2)
-            (HOLogic.mk_disj (phi $ z1 $ z2, HOLogic.mk_eq (z1, z2))))
-          else phi;
-
-        fun phi_rels strong_eq =
-          map3 (fn phi => fn z1 => fn z2 => mk_phi strong_eq phi z1 z2) phis Jzs1 Jzs2;
 
         val rels = map (Term.subst_atomic_types ((activeAs ~~ Ts) @ (activeBs ~~ Ts))) relsAsBs;
 
         fun mk_concl phi z1 z2 = HOLogic.mk_imp (phi $ z1 $ z2, HOLogic.mk_eq (z1, z2));
         val concl = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
           (map3 mk_concl phis Jzs1 Jzs2));
 
-        fun mk_rel_prem strong_eq phi dtor rel Jz Jz_copy =
+        fun mk_rel_prem phi dtor rel Jz Jz_copy =
           let
-            val concl = Term.list_comb (rel, map HOLogic.eq_const passiveAs @ phi_rels strong_eq) $
+            val concl = Term.list_comb (rel, map HOLogic.eq_const passiveAs @ phis) $
               (dtor $ Jz) $ (dtor $ Jz_copy);
           in
             HOLogic.mk_Trueprop
               (list_all_free [Jz, Jz_copy] (HOLogic.mk_imp (phi $ Jz $ Jz_copy, concl)))
           end;
 
-        val rel_prems = map5 (mk_rel_prem false) phis dtors rels Jzs Jzs_copy;
-        val rel_strong_prems = map5 (mk_rel_prem true) phis dtors rels Jzs Jzs_copy;
-
+        val rel_prems = map5 mk_rel_prem phis dtors rels Jzs Jzs_copy;
         val dtor_coinduct_goal =
           fold_rev Logic.all frees (Logic.list_implies (rel_prems, concl));
-        val coinduct_params = rev (Term.add_tfrees dtor_coinduct_goal []);
 
         val dtor_coinduct =
           Goal.prove_sorry lthy [] [] dtor_coinduct_goal
             (K (mk_dtor_coinduct_tac m raw_coind_thm bis_rel_thm rel_congs))
           |> Thm.close_derivation;
 
-        fun mk_prem strong_eq phi dtor map_nth sets Jz Jz_copy FJz =
+        fun mk_prem phi dtor map_nth sets Jz Jz_copy FJz =
           let
             val xs = [Jz, Jz_copy];
 
             fun mk_map_conjunct nths x =
               HOLogic.mk_eq (Term.list_comb (map_nth, passive_ids @ nths) $ FJz, dtor $ x);
 
             fun mk_set_conjunct set phi z1 z2 =
               list_all_free [z1, z2]
                 (HOLogic.mk_imp (HOLogic.mk_mem (HOLogic.mk_prod (z1, z2), set $ FJz),
-                  mk_phi strong_eq phi z1 z2 $ z1 $ z2));
+                  phi $ z1 $ z2));
 
             val concl = list_exists_free [FJz] (HOLogic.mk_conj
               (Library.foldr1 HOLogic.mk_conj (map2 mk_map_conjunct [fstsTs, sndsTs] xs),
               Library.foldr1 HOLogic.mk_conj
                 (map4 mk_set_conjunct (drop m sets) phis Jzs1 Jzs2)));
           in
             fold_rev Logic.all xs (Logic.mk_implies
               (HOLogic.mk_Trueprop (Term.list_comb (phi, xs)), HOLogic.mk_Trueprop concl))
           end;
 
-        fun mk_prems strong_eq =
-          map7 (mk_prem strong_eq) phis dtors map_FT_nths prodFT_setss Jzs Jzs_copy FJzs;
-
-        val prems = mk_prems false;
-        val strong_prems = mk_prems true;
+        val prems = map7 mk_prem phis dtors map_FT_nths prodFT_setss Jzs Jzs_copy FJzs;
 
         val dtor_map_coinduct_goal = fold_rev Logic.all frees (Logic.list_implies (prems, concl));
         val dtor_map_coinduct =
           Goal.prove_sorry lthy [] [] dtor_map_coinduct_goal
             (K (mk_dtor_map_coinduct_tac m ks raw_coind_thm bis_def))
           |> Thm.close_derivation;
-
-        val cTs = map (SOME o certifyT lthy o TFree) coinduct_params;
-        val cts = map3 (SOME o certify lthy ooo mk_phi true) phis Jzs1 Jzs2;
-
-        val dtor_strong_coinduct = singleton (Proof_Context.export names_lthy lthy)
-          (Goal.prove_sorry lthy [] []
-            (fold_rev Logic.all zs (Logic.list_implies (rel_strong_prems, concl)))
-            (K (mk_dtor_strong_coinduct_tac lthy m cTs cts dtor_coinduct rel_monos rel_eqs)))
-          |> Thm.close_derivation;
-      in
-        (dtor_map_coinduct, rev (Term.add_tfrees dtor_map_coinduct_goal []),
-         dtor_coinduct, dtor_strong_coinduct)
-      end;
+      in
+        (dtor_map_coinduct, rev (Term.add_tfrees dtor_map_coinduct_goal []), dtor_coinduct)
+      end;
+
+    (* TODO: Get rid of strong versions (since these can easily be derived from the weak ones). *)
+    val dtor_strong_coinduct_thm =
+      mk_strong_coinduct_thm m dtor_coinduct_thm rel_eqs rel_monos lthy;
 
     val timer = time (timer "coinduction");
 
     fun mk_dtor_map_DEADID_thm dtor_inject map_id =
       trans OF [iffD2 OF [dtor_inject, id_apply], map_id RS sym];