		Search-engine friendly clone of the ACL2 documentation.

Proof-automation

Without-subsumption

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

without-subsumption is a simple macro that allows you to perform proofs without subsumption/replacement to preserve hypotheses that might otherwise be dropped during clausification.

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

without-subsumption uses both 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)))
 )