Remove-hyps
Macro for defining a theorem with a minimal set of hypotheses
For a call of defthm, defthmd, or thm, the
application of remove-hyps attempts to produce a minimal set of
hypotheses. For example:
(remove-hyps
(defthm nth-append
(implies (and (true-listp x)
(natp n)
(true-listp y))
(equal (nth n (append x y))
(if (< n (len x))
(nth n x)
(nth (- n (len x)) y))))
:rule-classes nil))
generates:
(DEFTHM NTH-APPEND
(IMPLIES (NATP N)
(EQUAL (NTH N (APPEND X Y))
(IF (< N (LEN X))
(NTH N X)
(NTH (- N (LEN X)) Y))))
:RULE-CLASSES NIL)
Note however that remove-hyps works by removing one hypothesis at a
time, with each resulting proof attempt made using a limited number of
steps (see with-prover-step-limit) that depends on the number of steps
taken before removing the hypothesis. So if the removal of a hypothesis
requires a proof that takes sufficiently many more steps than the original
proof, or if two or more hypotheses must be removed together for the proof to
succeed with fewer hypotheses, then the result will not have a minimal set of
hypotheses.
Acceptable forms are as follows, where HYP can be a conjunction of
hypotheses, (and HYP1 ... HYPn), and ``defthm NAME'' may be
replaced by ``defthmd NAME'' or ``THM''.
(defthm NAME (implies HYP CONCL) ...)
(defthm NAME CONCL ...)
(defthm NAME (let ... (implies HYP CONCL)) ...)
(defthm NAME (let ... CONCL) ...)
(defthm NAME (let* ... (implies HYP CONCL)) ...)
(defthm NAME (let* ... CONCL) ...)
Normally, before using remove-hyps, one succesfully submits the given
call of defthm, defthmd, or thm. Thus by default,
remove-hyps evaluates silently. To see output from proof attempts, add a
non-nil optional argument. For example, for event E, use (remove-hyps
E t).
Unless there is an error (for example, due to malformed input), then in the
case of a call of thm, the value returned is the keyword,
:REMOVE-HYPS-COMPLETED; otherwise, the value returned is the name of the
theorem. (Technically, the value returned is an error triple with such a
value; see error-triple.)
Consider the case that a call of remove-hyps is made in a context
where proofs are normally skipped (see ld-skip-proofsp). If this
happens while including a certified book with include-book, then
proofs will indeed be skipped, because the earlier result of this
remove-hyps call was saved in the book's certificate. But
otherwise, the tool temporarily turns off the skipping of proofs (that is,
restores the act of doing proofs) while it tries to remove hypotheses, to
avoid the undesirable situation that all hypotheses are removed merely because
all proofs succeed when skipping proofs.
Finally, note that when remove-hyps is applied to a call of
defthm or defthmd, then remove-hyps will conclude by submitting
the generated event to ACL2. But since thm does not modify the logical
world, remove-hyps does not perform an extra such call at the end
for calls of thm.
