1\DOC
2
3\TYPE {MATCH_ASMSUB_RENAME_TAC : term quotation -> string list -> tactic}
4
5\SYNOPSIS
6Finds a match for a pattern in assumptions; instantiates goal to rename or abbreviate.
7
8\DESCRIBE
9
10When applied to the goal {(asl,w)}, the tactic
11{Q.MATCH_ASMSUB_RENAME_TAC q} parses the quotation {q} in the context
12of the goal, producing a term {pat} to use as a pattern. The tactic
13then attempts a (first order) match of {pat} against each term in
14{asl}, stopping when it finds an assumption that either matches {pat}
15in its entirety, or has a sub-term that matches {pat} (holding
16existing free variables from the goal constant).
17
18In either case, the match will return an instantiation mapping the
19fresh free variables of {pat} to terms occurring in the goal. This
20instantiation drops its bindings for variables whose names begin with
21an underscore, is next reversed, and is finally applied to the goal.
22This will both cause free variables in the goal to be renamed, and for
23larger terms to be replaced by variables (similar to what happens with
24the use of {SPEC_TAC}).
25
26\FAILURE
27
28Fails if there is no valid match for the pattern among the assumptions
29and their sub-terms. A valid match will not bind variables that are
30bound in the assumption being searched.
31
32\EXAMPLE
33
34In the following example, the variable {x} is treated as if a
35constant, so the search for a match with the pattern does not succeed
36on the first assumption (featuring {P}). Instead the second assumption
37provides the instantiation, and so the variable {z} in the original is
38renamed to {n}.
39{
40   > Q.MATCH_ASMSUB_RENAME_TAC `x < n`
41       ([``P(y < m):bool``, ``Q(x < z) : bool``], ``x + z < 10``);
42   val it = ([([``P (y < m)``, ``Q (x < n)``], ``x + n < 10``)],
43             fn): goal list * validation
44}
45
46\SEEALSO
47Q.MATCH_ASSUM_RENAME_TAC, Q.MATCH_GOALSUB_RENAME_TAC.
48
49\ENDDOC
50