--- 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) =>
--- 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,