Q.MATCH_ASSUM_RENAME_TAC : term quotation -> string list -> tactic
STRUCTURE
SYNOPSIS
Replaces selected terms with new variables by matching a pattern against an assumption.
DESCRIPTION
When applied to the goal (asl, w), the tactic Q.MATCH_ASSUM_RENAME_TAC q ls 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.

For each variable v in the pattern, 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 replace each t with the corresponding v, yielding a new goal. The list ls is of exceptions: if a variable v’s name appears in ls, then no replacement of v for t is made.

FAILURE
MATCH_ASSUM_RENAME_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.
EXAMPLE
If the current goal is
  (f x = Pair C'' C0') ?- (f C'' = f C0')
then applying the tactic Q.MATCH_ASSUM_RENAME_TAC `X = Pair c1 c2` ["X"] results in the goal
  (f x = Pair c1 c2) ?- (f c1 = f c2)
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`, markerLib.RM_ALL_ABBREVS_TAC, STRIP_TAC.
SEEALSO
HOL  Kananaskis-10