1\DOC
2
3\TYPE {RENAME_TAC : term quotation list -> tactic}
4
5\SYNOPSIS
6Renames free variables or subterms within a goal.
7
8\KEYWORDS
9
10\DESCRIBE
11A call to {RENAME_TAC qs} searches the current goal for matches to the
12patterns in the list {qs}, and then substitutes out the matches (in
13the ``reverse direction'') so that the goal becomes one that uses the
14names from {qs}. This can cause subterms within the goal to turn into
15simple variables, but the usual intention is to rename free variables
16into the variables that appear in the patterns.
17
18The matching is done without reference to the goal's existing free
19variables. If a variable in {qs} clashes with an existing variable in
20the goal, then the goal's variable will be renamed away. It is
21sufficient for variables to have the same name to ``clash''; they need
22not also have the same type. The search for matches begins by
23attempting to find matches against the whole of the goal, against
24whole assumptions, for sub-terms within the goal, and then sub-terms
25of assumptions. If multiple matches are possible, a variant tactic,
26{Q.kRENAME_TAC}, can be used: this tactic takes an additional
27``continuation'' tactic argument that can be used to discriminate
28between these matches.
29
30Patterns can use underscores to match anything without any change in
31the goal's naming being introduced. Underscores can match against
32sub-terms that include bound variables. Matching is first-order.
33
34\FAILURE
35Fails if it is impossible to consistently match the combination of
36patterns in the provided list of quotations ({qs}).
37
38\EXAMPLE
39If the goal is of the form
40{
41   x < y, y < z ?- x < f a
42}
43then invoking {Q.RENAME_TAC [`b < c`, `a < b`]} will produce the sub-goal:
44{
45   a < b, b < c ?- a < f a'
46}
47where the goal's original {a} variable (which is not even of type
48{num}), has been renamed away from {a} because that variable occurs in the
49patterns. (If the right hand side of the inequality was simply {a} and
50was thus of type num, it would also be renamed to {a'}.)
51
52If {Q.RENAME_TAC [`b < c`]} is invoked on the same initial goal, the result is:
53{
54   b < y, y < z ?- b < c
55}
56illustrating the way in which variables can eliminate more complicated sub-terms.
57
58The useful way in which underscores in patterns can be used to ``dodge'' terms including bound variables is illustrated in the next example, where the initial goal is:
59{
60   (!a. f a < z), z < c ?- z < d
61}
62After applying {Q.RENAME_TAC [`_ < x`, `x < c`]}, the goal becomes
63{
64   (!a. f a < x), x < c' ?- x < c
65}
66The goal was chosen for the match to the second pattern because the goal is considered first. If the initial goal had been
67{
68   (!a. f a < z), z < c ?- z < d /\ P z
69}
70then the result of the same application would be
71{
72   (!a. f a < z), z < c ?- x < d /\ P x
73}
74because whole assumptions are considered before sub-terms of the goal.
75
76\COMMENTS
77This function is also available under the name {bossLib.rename}.
78
79Note that {Q.RENAME_TAC [q]} is *not* the same as {Q.RENAME1_TAC q}.
80The latter pays attention to the goal's free variables, using these to
81constrain the match to the pattern. In contrast, {Q.RENAME_TAC}
82completely ignores all of the goal's free variables, such that using
83an existing name in a pattern doesn't make any difference to the
84matching behaviour.
85
86\SEEALSO
87Q.RENAME1_TAC.
88
89\ENDDOC
90