diff -r c042b3ad18a0 -r ec38e9f4352f src/HOL/BNF/Tools/bnf_fp_util.ML
--- a/src/HOL/BNF/Tools/bnf_fp_util.ML	Tue Aug 20 16:10:58 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_util.ML	Tue Aug 20 17:39:07 2013 +0200
@@ -179,6 +179,8 @@
   val mk_xtor_un_fold_o_map_thms: fp_kind -> bool -> int -> thm -> thm list -> thm list ->
     thm list -> thm list -> thm list
 
+  val mk_strong_coinduct_thm: int -> thm -> thm list -> thm list -> Proof.context -> thm
+
   val fp_bnf: (binding list -> (string * sort) list -> typ list * typ list list ->
       BNF_Def.bnf list -> local_theory -> 'a) ->
     binding list -> (string * sort) list -> ((string * sort) * typ) list -> local_theory ->
@@ -552,6 +554,24 @@
     split_conj_thm (un_fold_unique OF map (fp_case fp I mk_sym) unique_prems)
   end;
 
+fun mk_strong_coinduct_thm m coind rel_eqs rel_monos ctxt =
+  let
+    val n = Thm.nprems_of coind;
+    fun mk_inst phi = (phi, mk_union (phi, HOLogic.eq_const (fst (dest_pred2T (fastype_of phi)))))
+      |> pairself (certify ctxt);
+    val insts = Term.add_vars (Thm.prop_of coind) [] |> rev |> take n |> map (mk_inst o Var);
+    fun mk_unfold rel_eq rel_mono =
+      let
+        val eq = iffD2 OF [rel_eq RS @{thm predicate2_eqD}, refl];
+        val mono = rel_mono OF (replicate m @{thm order_refl} @ replicate n @{thm eq_subset});
+      in eq RS (mono RS @{thm predicate2D}) RS @{thm eqTrueI} end;
+    val unfolds = map2 mk_unfold rel_eqs rel_monos @ @{thms sup_fun_def sup_bool_def
+      imp_disjL all_conj_distrib subst_eq_imp simp_thms(18,21,35)};
+  in
+    Thm.instantiate ([], insts) coind
+    |> unfold_thms ctxt unfolds
+  end;
+
 fun fp_bnf construct_fp bs resBs eqs lthy =
   let
     val timer = time (Timer.startRealTimer ());