Perform proofs without subsumption/replacement to preserve hypotheses that might otherwise be dropped.

In the course of a proof, ACL2 will sometimes drop hypotheses during subsumption/replacement that would otherwise have allowed it to complete the proof.

`quick-and-dirty-subsumption-replacement-step` and
`case-split-limitations` to stop subsumption/replacement in various
stages of the ACL2 simplifier. These hints can help preserve hypothesis
in a proof that the ACL2 simplifier might otherwise drop. The
macro is defined as follows:

(defmacro without-subsumption(form &key (cases 'nil)) `(encapsulate () (local (defun without-subsumption-disable-quick-and-dirty (x y) (declare (ignore x y) (xargs :guard t)) nil)) (local (defattach-system quick-and-dirty-srs without-subsumption-disable-quick-and-dirty)) (set-case-split-limitations '(0 ,cases)) ,form ))

Usage:

(include-book "tools/without-subsumption" :dir :system) (without-subsumption (defthm natp-implies-integerp (implies (natp n) (integerp n))) )