A computed hint which produces :use hints of the given theorem, based on occurences of a pattern in the current goal clause.
Syntax: (instantiate-thm-for-matching-terms thm subst pattern &key restrict).
Arguments: THM is a theorem/definition name or rune, SUBST is a list of pairs such as
((var1 sub1) (var2 sub2) ... )
where each vari is a variable name and each sub1 is a term, usually containing free variables that are also free in PATTERN, and PATTERN is a pattern (pseudo-term) to be matched against the clause.
We translate the PATTERN and each term in the SUBST, so it's ok to use macros etc. within them.
For each subterm of CLAUSE that matches PATTERN, the unifying substitution is computed and applied to each of the subi terms in the SUBST.
For example, if I have some theorem FOO-BOUND, such as:
(defthm foo-bound (< (foo a b) (max (g a) (g b))))
and I'm proving the goal:
(implies (and (p (foo (bar z) (baz q))) (q (bar z) (buz y))) (r (foo (baz q) (bar y))))
and I provide the computed hint
(instantiate-thm-for-matching-terms foo-bound ((a c) (b d)) (foo c d))
this produces the hint:
:use ((:instance foo-bound (a (bar z)) (b (baz q))) (:instance foo-bound (a (baz q)) (b (bar y))))
The process by which this happens: The provided pattern
c -> (bar z), d -> (baz q)
and
c -> (baz q), d -> (bar y).
These two unifying substitutions are applied to the user-provided
substitution
Note: you may want to qualify this computed hint with STABLE-UNDER-SIMPLIFICATIONP or other conditions, and perhaps disable the theorem used. For example:
:hints ((and stable-under-simplificationp (let ((res (instantiate-thm-for-matching-terms foo-bound ((a c) (b d)) (foo c d)))) (and res (append res '(:in-theory (disable foo-bound)))))))