SRW_TAC
bossLib.SRW_TAC : ssfrag list -> thm list -> tactic
Also exported as BasicProvers.SRW_TAC.
A version of RW_TAC with an implicit simpset.
A call to SRW_TAC [d1,...,dn] thlist produces the same result as
RW_TAC (srw_ss() ++ d1 ++ ... ++ dn) thlist
Failure
When applied to a goal, the tactic resulting from an application of
SRW_TAC may diverge.
Comments
There are two reasons why one might prefer SRW_TAC to RW_TAC.
Firstly, when a large number of datatypes are present in the TypeBase,
the implementation of RW_TAC has to merge the attendant
simplifications for each type onto its simpset argument each time it
is called. This can be rather time-consuming. Secondly, the simpset
returned by srw_ss() can be augmented with fragments from other
sources than the TypeBase, using the functions augment_srw_ss and
export_rewrites. This can make for a tool that is simple to use, and
powerful because of all its accumulated simpset fragments.
Naturally, the latter advantage can also be a disadvantage: if SRW_TAC
does too much because there is too much in the simpset underneath
srw_ss(), then there is no way to get around this using SRW_TAC.
Typical invocations of SRW_TAC will be of the form
SRW_TAC [][th1, th2,.. ]
The first argument, for lists of simpset fragments is for the
inclusion of fragments that are not always appropriate. An example of
such a fragment is numSimps.ARITH_ss, which embodies an arithmetic
decision procedure for the natural numbers.
See also
bossLib.srw_ss,
bossLib.augment_srw_ss,
BasicProvers.export_rewrites,
simpLib.SSFRAG