Hints as a Function of the Goal (not its Name)
Sometimes it is desirable to supply a hint whenever a certain term arises in a conjecture. For example, suppose we have proved
(defthm all-swaps-have-the-property (the-property (swap x)) :rule-classes nil)
and suppose that whenever
(if test '(:use (:instance all-swaps-have-the-property (x A))) nil)
where
Thus, the computed hint:
(if (occur-lst '(swap a) clause) '(:use (:instance all-swaps-have-the-property (x A))) nil)
will add the hypothesis
A COMMON MISTAKE users are likely to make is to forget that they are
dealing with translated terms. For example, suppose we wished to look for
(occur-lst '(SWAP (LIST 1 A)) clause)
because that presentation of the term contains macros and other abbreviations. By using :trans (see trans) we can obtain the translation of the target term. Then we can look for it with:
(occur-lst '(SWAP (CONS '1 (CONS A 'NIL))) clause)
Note in particular that you must
* eliminate all macros and * explicitly quote all constants.
We recommend using
An alternative is to use the expression
((NOT (CONSP X)) (SYMBOLP Y) (EQUAL (CONS '1 (CAR X)) Y))
``prettyifies'' to
(IMPLIES (AND (CONSP X) (NOT (SYMBOLP Y))) (EQUAL (CONS 1 (CAR X)) Y))
which is what you would see printed by ACL2 when the goal clause is that shown.
However, if you choose to convert your clauses to prettyified form, you
will have to write your own explorers (like our
We make one more note on this example. We said above that the computed hint:
(if (occur-lst '(swap a) clause) '(:use (:instance all-swaps-have-the-property (x A))) nil)
will add the hypothesis
It bears noting that the subgoals produced by induction and top-level
forcing round goals are not children. For example, suppose the hint above
fires on "Subgoal 3" and produces, say, "Subgoal 3'". Then the hint will
not fire on "Subgoal 3'" even though it (still) contains
But now suppose that "Subgoal 3'" is pushed for induction. Then the goals created by that induction, i.e., the base case and induction step, are not considered children of "Subgoal 3'". All of the original hints are available.
Alternatively, suppose that "Subgoal 3' is proved but forces some other
subgoal, "[1]Subgoal 1" which is attacked in Forcing Round 1. That
top-level forced subgoal is not a child. All the original hints are available
to it. Thus, if it contains