# HG changeset patch
# User traytel
# Date 1377007858 -7200
# Node ID c042b3ad18a021e9498de6895e6a9d9ceee3ba2b
# Parent  c0217c4a6b2dae45d2bcb730c1e49155e862a747
don't derive unused low-level theorem

diff -r c0217c4a6b2d -r c042b3ad18a0 src/HOL/BNF/Tools/bnf_gfp.ML
--- a/src/HOL/BNF/Tools/bnf_gfp.ML	Tue Aug 20 16:10:58 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_gfp.ML	Tue Aug 20 16:10:58 2013 +0200
@@ -2020,8 +2020,7 @@
     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_map_strong_coinduct_thm, dtor_strong_coinduct_thm) =
+    val (dtor_map_coinduct_thm, coinduct_params, dtor_coinduct_thm, dtor_strong_coinduct_thm) =
       let
         val zs = Jzs1 @ Jzs2;
         val frees = phis @ zs;
@@ -2102,16 +2101,9 @@
             (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;
-
-        val dtor_map_strong_coinduct = singleton (Proof_Context.export names_lthy lthy)
-          (Goal.prove_sorry lthy [] []
-            (fold_rev Logic.all zs (Logic.list_implies (strong_prems, concl)))
-            (K (mk_dtor_map_strong_coinduct_tac ks cTs cts dtor_map_coinduct bis_def
-              (tcoalg_thm RS bis_Id_on_thm))))
-          |> Thm.close_derivation;
       in
         (dtor_map_coinduct, rev (Term.add_tfrees dtor_map_coinduct_goal []),
-         dtor_coinduct, dtor_map_strong_coinduct, dtor_strong_coinduct)
+         dtor_coinduct, dtor_strong_coinduct)
       end;
 
     val timer = time (timer "coinduction");
@@ -2902,8 +2894,6 @@
       val common_notes =
         [(dtor_coinductN, [dtor_coinduct_thm]),
         (dtor_map_coinductN, [dtor_map_coinduct_thm]),
-        (dtor_map_strong_coinductN, [dtor_map_strong_coinduct_thm]),
-        (dtor_strong_coinductN, [dtor_strong_coinduct_thm]),
         (rel_coinductN, [Jrel_coinduct_thm]),
         (dtor_unfold_transferN, dtor_unfold_transfer_thms)]
         |> map (fn (thmN, thms) =>
diff -r c0217c4a6b2d -r c042b3ad18a0 src/HOL/BNF/Tools/bnf_gfp_tactics.ML
--- a/src/HOL/BNF/Tools/bnf_gfp_tactics.ML	Tue Aug 20 16:10:58 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_gfp_tactics.ML	Tue Aug 20 16:10:58 2013 +0200
@@ -39,8 +39,6 @@
   val mk_corec_unique_mor_tac: thm list -> thm list -> thm -> {prems: 'a, context: Proof.context} ->
     tactic
   val mk_dtor_map_coinduct_tac: int -> int list -> thm -> thm -> tactic
-  val mk_dtor_map_strong_coinduct_tac: int list -> ctyp option list -> cterm option list -> thm ->
-    thm -> thm -> tactic
   val mk_dtor_set_tac: int -> thm -> thm -> thm list -> tactic
   val mk_dtor_coinduct_tac: int -> thm -> thm -> thm list -> tactic
   val mk_dtor_strong_coinduct_tac: Proof.context -> int -> ctyp option list ->
@@ -1024,20 +1022,6 @@
         rtac CollectI, etac (refl RSN (2, @{thm subst_Pair}))]) ks] 1
   end;
 
-fun mk_dtor_map_strong_coinduct_tac ks cTs cts dtor_map_coinduct bis_def bis_Id_on =
-  EVERY' [rtac rev_mp, rtac (Drule.instantiate' cTs cts dtor_map_coinduct),
-    EVERY' (map (fn i =>
-      EVERY' [etac disjE, REPEAT_DETERM o dtac @{thm meta_spec}, etac meta_mp,
-        atac, rtac rev_mp, rtac subst, rtac bis_def, rtac bis_Id_on,
-        rtac impI, dtac conjunct2, dtac (mk_conjunctN (length ks) i), REPEAT_DETERM o etac allE,
-        etac impE, etac @{thm Id_on_UNIV_I}, REPEAT_DETERM o eresolve_tac [bexE, conjE, CollectE],
-        rtac exI, rtac conjI, etac conjI, atac,
-        CONJ_WRAP' (K (EVERY' [REPEAT_DETERM o resolve_tac [allI, impI],
-          rtac disjI2, rtac @{thm Id_onD}, etac set_mp, atac])) ks])
-    ks),
-    rtac impI, REPEAT_DETERM o etac conjE,
-    CONJ_WRAP' (K (rtac impI THEN' etac mp THEN' etac disjI1)) ks] 1;
-
 fun mk_map_tac m n cT unfold map_comp' map_cong0 =
   EVERY' [rtac ext, rtac (o_apply RS trans RS sym), rtac (o_apply RS trans RS sym),
     rtac (unfold RS trans), rtac (Thm.permute_prems 0 1 (map_comp' RS box_equals)), rtac map_cong0,