# HG changeset patch
# User blanchet
# Date 1437060348 -7200
# Node ID 685b169d06112100e97cb0c2fe79283f5c5acb1f
# Parent  c4bc0691860b79f39c21344b53633ce8d8859fcb
tuning

diff -r c4bc0691860b -r 685b169d0611 src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Thu Jul 16 17:25:44 2015 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Thu Jul 16 17:25:48 2015 +0200
@@ -1663,6 +1663,25 @@
       (transpose setss)
   end;
 
+fun mk_coinduct_strong_thm coind rel_eqs rel_monos mk_vimage2p ctxt =
+  let
+    val n = Thm.nprems_of coind;
+    val m = Thm.nprems_of (hd rel_monos) - n;
+    fun mk_inst phi =
+      (phi, Thm.cterm_of ctxt (mk_union (Var phi, HOLogic.eq_const (fst (dest_pred2T (#2 phi))))));
+    val insts = Term.add_vars (Thm.prop_of coind) [] |> rev |> take n |> map mk_inst;
+    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 mk_vimage2p (eq RS (mono RS @{thm predicate2D})) RS 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 derive_coinduct_corecs_thms_for_types pre_bnfs (x, cs, cpss, (((pgss, _, _, _), cqgsss), _))
     dtor_coinduct dtor_injects dtor_ctors dtor_corec_thms live_nesting_bnfs fpTs Cs Xs ctrXs_Tsss
     kss mss ns fp_abs_inverses abs_inverses mk_vimage2p ctr_defss (ctr_sugars : ctr_sugar list)
diff -r c4bc0691860b -r 685b169d0611 src/HOL/Tools/BNF/bnf_fp_util.ML
--- a/src/HOL/Tools/BNF/bnf_fp_util.ML	Thu Jul 16 17:25:44 2015 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_util.ML	Thu Jul 16 17:25:48 2015 +0200
@@ -194,8 +194,6 @@
   val mk_xtor_un_fold_o_map_thms: BNF_Util.fp_kind -> bool -> int -> thm -> thm list -> thm list ->
     thm list -> thm list -> thm list
 
-  val mk_coinduct_strong_thm: thm -> thm list -> thm list -> (thm -> thm) -> Proof.context -> thm
-
   val fp_bnf: (binding list -> (string * sort) list -> typ list * typ list list ->
       BNF_Def.bnf list -> BNF_Comp.absT_info list -> local_theory -> 'a) ->
     binding list -> (string * sort) list -> (string * sort) list -> ((string * sort) * typ) list ->
@@ -603,25 +601,6 @@
     split_conj_thm (un_fold_unique OF map (case_fp fp I mk_sym) unique_prems)
   end;
 
-fun mk_coinduct_strong_thm coind rel_eqs rel_monos mk_vimage2p ctxt =
-  let
-    val n = Thm.nprems_of coind;
-    val m = Thm.nprems_of (hd rel_monos) - n;
-    fun mk_inst phi =
-      (phi, Thm.cterm_of ctxt (mk_union (Var phi, HOLogic.eq_const (fst (dest_pred2T (#2 phi))))))
-    val insts = Term.add_vars (Thm.prop_of coind) [] |> rev |> take n |> map mk_inst;
-    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 mk_vimage2p (eq RS (mono RS @{thm predicate2D})) RS 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 Ds0 fp_eqs lthy =
   let
     val time = time lthy;