1\DOC MATCH_RENAME_TAC
2
3\TYPE {Q.MATCH_RENAME_TAC : term quotation -> tactic}
4
5\SYNOPSIS
6Replaces selected terms with new variables by matching a pattern against the goal statement.
7
8\DESCRIBE
9When applied to the goal {(asl, w)}, the tactic {Q.MATCH_RENAME_TAC q ls}
10parses the quotation {q} in the context of the goal, producing a term to use as
11a pattern. The tactic then attempts a (first order) match of the pattern
12against the term {w}.
13
14For each variable {v} in the pattern, there will be an instantiation
15term {t}, such that the substitution
16{
17   pattern[v1 |-> t1, v2 |-> t2, ...]
18}
19produces {w}. The effect of the tactic is to then replace each {t}
20with the corresponding {v}, yielding a new goal. Note that underscores
21within a pattern, though strictly speaking variables, are not included
22in this reverse instantiation.
23
24\FAILURE
25{MATCH_RENAME_TAC} fails if the pattern provided does not match the
26goal, or if variables from the goal are used in the pattern in ways
27that make the pattern fail to type-check.
28
29\EXAMPLE
30If the current goal is
31{
32   ?- (f x = Pair C'' C0') ==> (f C'' = f C0')
33}
34then applying the tactic {Q.MATCH_RENAME_TAC `(f x = Pair c1 c2) ==> _`} results in
35the goal
36{
37   ?- (f x = Pair c1 c2) ==> (f c1 = f c2)
38}
39
40\COMMENTS
41This tactic is equivalent to first applying {Q.MATCH_ABBREV_TAC q}, then
42applying {Q.RM_ABBREV_TAC `v`} for each underscore in {q}.
43
44\SEEALSO
45Q.MATCH_ABBREV_TAC, Q.MATCH_ASSUM_RENAME_TAC
46
47\ENDDOC
48