1\DOC 2 3\TYPE {MATCH_ASMSUB_RENAME_TAC : term quotation -> string list -> tactic} 4 5\SYNOPSIS 6Finds a match for a pattern in assumptions; instantiates goal to rename or abbreviate. 7 8\DESCRIBE 9 10When applied to the goal {(asl,w)}, the tactic 11{Q.MATCH_ASMSUB_RENAME_TAC q} parses the quotation {q} in the context 12of the goal, producing a term {pat} to use as a pattern. The tactic 13then attempts a (first order) match of {pat} against each term in 14{asl}, stopping when it finds an assumption that either matches {pat} 15in its entirety, or has a sub-term that matches {pat} (holding 16existing free variables from the goal constant). 17 18In either case, the match will return an instantiation mapping the 19fresh free variables of {pat} to terms occurring in the goal. This 20instantiation drops its bindings for variables whose names begin with 21an underscore, is next reversed, and is finally applied to the goal. 22This will both cause free variables in the goal to be renamed, and for 23larger terms to be replaced by variables (similar to what happens with 24the use of {SPEC_TAC}). 25 26\FAILURE 27 28Fails if there is no valid match for the pattern among the assumptions 29and their sub-terms. A valid match will not bind variables that are 30bound in the assumption being searched. 31 32\EXAMPLE 33 34In the following example, the variable {x} is treated as if a 35constant, so the search for a match with the pattern does not succeed 36on the first assumption (featuring {P}). Instead the second assumption 37provides the instantiation, and so the variable {z} in the original is 38renamed to {n}. 39{ 40 > Q.MATCH_ASMSUB_RENAME_TAC `x < n` 41 ([``P(y < m):bool``, ``Q(x < z) : bool``], ``x + z < 10``); 42 val it = ([([``P (y < m)``, ``Q (x < n)``], ``x + n < 10``)], 43 fn): goal list * validation 44} 45 46\SEEALSO 47Q.MATCH_ASSUM_RENAME_TAC, Q.MATCH_GOALSUB_RENAME_TAC. 48 49\ENDDOC 50