MATCH_ASMSUB_RENAME_TACQ.MATCH_ASMSUB_RENAME_TAC : term quotation -> string list -> tacticFinds a match for a pattern in assumptions; instantiates goal to rename or abbreviate.
When applied to the goal (asl,w), the tactic
Q.MATCH_ASMSUB_RENAME_TAC q parses the quotation
q in the context of the goal, producing a term
pat to use as a pattern. The tactic then attempts a (first
order) match of pat against each term in asl,
stopping when it finds an assumption that either matches
pat in its entirety, or has a sub-term that matches
pat (holding existing free variables from the goal
constant).
In either case, the match will return an instantiation mapping the
fresh free variables of pat to terms occurring in the goal.
This instantiation drops its bindings for variables whose names begin
with an underscore, is next reversed, and is finally applied to the
goal. This will both cause free variables in the goal to be renamed, and
for larger terms to be replaced by variables (similar to what happens
with the use of SPEC_TAC).
Fails if there is no valid match for the pattern among the assumptions and their sub-terms. A valid match will not bind variables that are bound in the assumption being searched.
In the following example, the variable x is treated as
if a constant, so the search for a match with the pattern does not
succeed on the first assumption (featuring P). Instead the
second assumption provides the instantiation, and so the variable
z in the original is renamed to n.
> Q.MATCH_ASMSUB_RENAME_TAC `x < n`
([``P(y < m):bool``, ``Q(x < z) : bool``], ``x + z < 10``);
val it = ([([``P (y < m)``, ``Q (x < n)``], ``x + n < 10``)],
fn): goal list * validation