----------------------------------------------------------------------
MATCH_ASSUM_ABBREV_TAC                                             (Q)
----------------------------------------------------------------------
Q.MATCH_ASSUM_ABBREV_TAC : term quotation -> tactic

SYNOPSIS
Introduces abbreviations by matching a pattern against an assumption.

DESCRIBE
When applied to the goal {(asl, w)}, the tactic {Q.MATCH_ASSUM_ABBREV_TAC q}
parses the quotation {q} in the context of the goal, producing a term to use as
a pattern. The tactic then attempts a (first order) match of the pattern
against each term in {asl}, stopping on the first matching assumption {a}.
Variables that occur in both the pattern and the goal are treated as “local
constants”, and will not acquire instantiations.

For each variable {v} in the pattern that has not been treated as a local
constant, there will be an instantiation term {t}, such that the substitution
{pattern[v1 |-> t1, v2 |-> t2, ...]} produces {a}. The effect of the tactic is
to then perform abbreviations in the goal, replacing each {t} with the
corresponding {v}, and adding assumptions of the form {Abbrev(v = t)} to the
goal.

FAILURE
{MATCH_ABBREV_TAC} fails if the pattern provided does not match any assumption,
or if variables from the goal are used in the pattern in ways that make the
pattern fail to type-check.

COMMENTS
This tactic improves on the following tedious workflow:
{Q.PAT_ASSUM pat MP_TAC}, {Q.MATCH_ABBREV_TAC `pat ==> X`}, {Q.UNABBREV_TAC `X`},
{STRIP_TAC}.

SEEALSO
Q.MATCH_ABBREV_TAC, Q.MATCH_ASSUM_RENAME_TAC.

----------------------------------------------------------------------