RENAME_TAC : term quotation list -> tactic
The matching is done without reference to the goal’s existing free variables. If a variable in qs clashes with an existing variable in the goal, then the goal’s variable will be renamed away. It is sufficient for variables to have the same name to “clash”; they need not also have the same type. The search for matches begins by attempting to find matches against the whole of the goal, against whole assumptions, for sub-terms within the goal, and then sub-terms of assumptions. If multiple matches are possible, a variant tactic, Q.kRENAME_TAC, can be used: this tactic takes an additional “continuation” tactic argument that can be used to discriminate between these matches.
Patterns can use underscores to match anything without any change in the goal’s naming being introduced. Underscores can match against sub-terms that include bound variables. Matching is first-order.
x < y, y < z ?- x < f a
a < b, b < c ?- a < f a'
If Q.RENAME_TAC [`b < c`] is invoked on the same initial goal, the result is:
b < y, y < z ?- b < c
The 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:
(!a. f a < z), z < c ?- z < d
(!a. f a < x), x < c' ?- x < c
(!a. f a < z), z < c ?- z < d /\ P z
(!a. f a < z), z < c ?- x < d /\ P x
Note that Q.RENAME_TAC [q] is not the same as Q.RENAME1_TAC q. The latter pays attention to the goal’s free variables, using these to constrain the match to the pattern. In contrast, Q.RENAME_TAC completely ignores all of the goal’s free variables, such that using an existing name in a pattern doesn’t make any difference to the matching behaviour.