1\DOC
2
3\TYPE {MATCH_GOALSUB_RENAME_TAC : term quotation -> tactic}
4
5\SYNOPSIS
6Renames a goal in accordance with a pattern matched against a subterm
7of the goal.
8
9\KEYWORDS
10Renaming
11
12\DESCRIBE
13
14A call to {MATCH_GOALSUB_RENAME_TAC pat} attempts to find a match for
15the pattern {pat} in the current goal (using {gen_find_term} to find a
16sub-term of the goal that matches). If a match is found, the goal is
17adjusted so that the variables occurring in the pattern now also
18appear in the goal. This may rename variables in the goal, or even
19cause larger sub-terms to be replaced by variables (as with
20{SPEC_TAC}). Underscores may be used in {pat} to indicate ``don't
21care'' bindings, where no renaming or instantiation will take place.
22
23\FAILURE
24
25Fails if there is no sub-term of the goal that matches the pattern.
26Fails if the instantiation changes a pattern variable that already
27exists in the goal.
28
29\EXAMPLE
30
31If the goal is
32{
33    ?- !x. x * 2 < y * (z + 1) * (y + a)
34}
35then applying {Q.MATCH_GOALSUB_RENAME_TAC `y + c`} will match the
36pattern {y + c} against the various subterms within the goal. The
37first obvious match, with {z + 1} will be rejected because the
38variable {y} is free in the goal, and is treated as if it were a local
39constant. Because of this, {y + a} is the matching sub-term, and after
40renaming the goal becomes
41{
42    ?- !x. x * 2 < y * (z + 1) * (y + c)
43}
44
45
46\SEEALSO
47Q.MATCH_RENAME_TAC.
48
49\ENDDOC
50