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