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