--- a/src/HOL/BNF/Tools/bnf_def_tactics.ML Wed May 08 09:39:30 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_def_tactics.ML Wed May 08 09:45:30 2013 +0200
@@ -26,6 +26,7 @@
val mk_rel_conversep_le_tac: thm list -> thm -> thm -> thm -> thm list ->
{prems: thm list, context: Proof.context} -> tactic
val mk_rel_mono_tac: thm list -> thm -> {prems: 'a, context: Proof.context} -> tactic
+ val mk_rel_mono_strong_tac: thm -> thm list -> {prems: 'a, context: Proof.context} -> tactic
end;
structure BNF_Def_Tactics : BNF_DEF_TACTICS =
@@ -192,4 +193,15 @@
REPEAT_DETERM o eresolve_tac [exE, conjE], rtac @{thm relcomppI}, rtac @{thm conversepI},
etac @{thm GrpI}, atac, etac @{thm GrpI}, atac] 1;
+fun mk_rel_mono_strong_tac in_rel set_maps {context = ctxt, prems = _} =
+ if null set_maps then atac 1
+ else
+ unfold_tac [in_rel] ctxt THEN
+ REPEAT_DETERM (eresolve_tac [exE, CollectE, conjE] 1) THEN
+ hyp_subst_tac ctxt 1 THEN
+ unfold_tac set_maps ctxt THEN
+ EVERY' [rtac exI, rtac @{thm conjI[OF CollectI conjI[OF refl refl]]},
+ CONJ_WRAP' (K (etac @{thm Collect_split_mono_strong} THEN' atac)) set_maps] 1;
+
+
end;