1\DOC MATCH_RENAME_TAC 2 3\TYPE {Q.MATCH_RENAME_TAC : term quotation -> tactic} 4 5\SYNOPSIS 6Replaces selected terms with new variables by matching a pattern against the goal statement. 7 8\DESCRIBE 9When applied to the goal {(asl, w)}, the tactic {Q.MATCH_RENAME_TAC q ls} 10parses the quotation {q} in the context of the goal, producing a term to use as 11a pattern. The tactic then attempts a (first order) match of the pattern 12against the term {w}. 13 14For each variable {v} in the pattern, there will be an instantiation 15term {t}, such that the substitution 16{ 17 pattern[v1 |-> t1, v2 |-> t2, ...] 18} 19produces {w}. The effect of the tactic is to then replace each {t} 20with the corresponding {v}, yielding a new goal. Note that underscores 21within a pattern, though strictly speaking variables, are not included 22in this reverse instantiation. 23 24\FAILURE 25{MATCH_RENAME_TAC} fails if the pattern provided does not match the 26goal, or if variables from the goal are used in the pattern in ways 27that make the pattern fail to type-check. 28 29\EXAMPLE 30If the current goal is 31{ 32 ?- (f x = Pair C'' C0') ==> (f C'' = f C0') 33} 34then applying the tactic {Q.MATCH_RENAME_TAC `(f x = Pair c1 c2) ==> _`} results in 35the goal 36{ 37 ?- (f x = Pair c1 c2) ==> (f c1 = f c2) 38} 39 40\COMMENTS 41This tactic is equivalent to first applying {Q.MATCH_ABBREV_TAC q}, then 42applying {Q.RM_ABBREV_TAC `v`} for each underscore in {q}. 43 44\SEEALSO 45Q.MATCH_ABBREV_TAC, Q.MATCH_ASSUM_RENAME_TAC 46 47\ENDDOC 48