Atc-hide-rules
Rules about hide.
In the new modular proofs generated by ATC,
we use hide to prevent ACL2's rewriter
from changing certain terms in ways
that defeat the modular proof strategy.
In at least one case, we have observed that ACL2
produces terms of the form (hide ((lambda (x) x) t)),
which should be just t,
but because of the hide,
the term does not get rewritten to t.
Thus, we add and use a fairly ad hoc rule to resolve the situation.
A rule that just rewrites the above term to t is insufficient,
as we found by experimenting in that case where the term arises.
Instead, the rule below works:
it has a generic argument to hide,
and a hypothesis that equates it to the pattern we want to resolve.
Definitions and Theorems
Theorem: hide-of-lambda
(defthm hide-of-lambda
(implies (equal term ((lambda (x) x) t))
(hide term)))