Consider the following (admittedly silly) example.
ACL2's output includes the following warning.
ACL2 Warning [Use] in ( THM ...): It is unusual to :USE the formula of an enabled :REWRITE or :DEFINITION rule, so you may want to consider disabling (:REWRITE CDR-CONS) in the hint provided for Subgoal *1/1. See :DOC using-enabled-rules.
The warning is saying that if you leave the rewrite rule enabled, ACL2 may
simplify away the hypothesis added by the
Recall (see hints) how
Consider the following tiny example.
(defun p (x) (cons x x)) (defthm car-p (equal (car (p x)) x)) (in-theory (disable p (:type-prescription p))) (thm (implies (equal (p x1) (p x2)) (equal x1 x2)) :hints (("Goal" :use ((:instance car-p (x x1)) (:instance car-p (x x2))))))
The proof of the final thm form fails, because the new hypotheses
are rewritten to
We augment the goal with the hypotheses provided by the :USE hint. These hypotheses can be derived from CAR-P via instantiation. We are left with the following subgoal. Goal' (IMPLIES (AND (EQUAL (CAR (P X1)) X1) (EQUAL (CAR (P X2)) X2)) (IMPLIES (EQUAL (P X1) (P X2)) (EQUAL X1 X2))). By the simple :rewrite rule CAR-P we reduce the conjecture to Goal'' (IMPLIES (EQUAL (P X1) (P X2)) (EQUAL X1 X2)).
When we disable the rule
(thm (implies (equal (p x1) (p x2)) (equal x1 x2)) :hints (("Goal" :use ((:instance car-p (x x1)) (:instance car-p (x x2))) :in-theory (disable car-p))))
In general, then, a solution is to disable the rewrite rule that you are
supplying in a