Variant of `defthm` supporting guard verification

After a `defthm` event introduces a name, `verify-guards` can be called on that theorem name, just as it can be called on
a function symbol. However, the proof obligation for verifying guards
is often not a theorem. After presenting the general form for

Example Form: (defthmg true-listp-member-equal (implies (true-listp x) (true-listp (member-equal a x)))) General Form: (defthmg name body ;;; defthm arguments: :rule-classes rule-classes :instructions instructions :hints hints :otf-flg otf-flg ;;; new arguments: :verify-guards verify-guards :guard-hints guard-hints)

where all but the last two keyword arguments are exactly as for `defthm`. If `verify-guards` on

We now consider in some detail the example displayed above. Consider it
again, but this time with

(defthm true-listp-member-equal (implies (true-listp x) (true-listp (member-equal a x))))

The proof succeeds, after which we might try to call `verify-guards`.
But `member-equal` requires that its second
argument satisfy `true-listp`.

A way to allow guard verification for such a theorem is to replace
`impliez`, whose calls expand to calls of
`trans1`).

ACL2 !>:trans1 (impliez (true-listp x) (true-listp (member-equal a x))) (IF (TRUE-LISTP X) (TRUE-LISTP (MEMBER-EQUAL A X)) T) ACL2 !>

When *not* lead to
evaluation of the

But simply changing

ACL2 !>(defthm true-listp-member-equal (impliez (true-listp x) (true-listp (member-equal a x)))) ACL2 Error in ( DEFTHM TRUE-LISTP-MEMBER-EQUAL ...): A :REWRITE rule generated from TRUE-LISTP-MEMBER-EQUAL is illegal because it rewrites the IF-expression (IF (TRUE-LISTP X) (TRUE-LISTP (MEMBER-EQUAL A X)) 'T). For general information about rewrite rules in ACL2, see :DOC rewrite.

The error message is basically telling us that we need `corollary` equal to the original theorem,
as follows.

(defthm true-listp-member-equal (impliez (true-listp x) (true-listp (member-equal a x))) :rule-classes ((:rewrite :corollary (implies (true-listp x) (true-listp (member-equal a x))))))

Now the intended rewrite rule is stored, and also we can verify guards,
since the guard proof obligation is based on the body of the

(verify-guards true-listp-member-equal)

The purpose of `progn` containing the
`hints` to streamline the process).

(DEFTHM TRUE-LISTP-MEMBER-EQUAL (IMPLIEZ (TRUE-LISTP X) (TRUE-LISTP (MEMBER-EQUAL A X))) :RULE-CLASSES ((:REWRITE :COROLLARY (IMPLIES (TRUE-LISTP X) (TRUE-LISTP (MEMBER-EQUAL A X))) :HINTS (("Goal" :IN-THEORY (THEORY 'MINIMAL-THEORY)))))) (VERIFY-GUARDS TRUE-LISTP-MEMBER-EQUAL)

If `rule-classes` are supplied explicitly, these will be
handled appropriately: for each rule class, if a

The following more complex (but rather nonsensical) example illustrates the
various arguments of

(defthmg true-listp-member-equal (implies (true-listp x) (true-listp (member-equal a x))) :verify-guards t :guard-hints (("Goal" :use car-cons)) :hints (("Goal" :induct (member-equal a x))) :rule-classes (:rewrite (:rewrite ; awful rule with free variable :corollary (implies (not (true-listp (member-equal a x))) (not (true-listp x)))) :type-prescription) :otf-flg t)

Here are the two events generated after successfully evaluating the form
above. Notice that the rule class with an explicit

(DEFTHM TRUE-LISTP-MEMBER-EQUAL (IMPLIEZ (TRUE-LISTP X) (TRUE-LISTP (MEMBER-EQUAL A X))) :RULE-CLASSES ((:REWRITE :COROLLARY (IMPLIES (TRUE-LISTP X) (TRUE-LISTP (MEMBER-EQUAL A X))) :HINTS (("Goal" :IN-THEORY (THEORY 'MINIMAL-THEORY)))) (:REWRITE :COROLLARY (IMPLIES (NOT (TRUE-LISTP (MEMBER-EQUAL A X))) (NOT (TRUE-LISTP X)))) (:TYPE-PRESCRIPTION :COROLLARY (IMPLIES (TRUE-LISTP X) (TRUE-LISTP (MEMBER-EQUAL A X))) :HINTS (("Goal" :IN-THEORY (THEORY 'MINIMAL-THEORY))))) :HINTS (("Goal" :INDUCT (MEMBER-EQUAL A X))) :OTF-FLG T) (VERIFY-GUARDS TRUE-LISTP-MEMBER-EQUAL :HINTS (("Goal" :USE CAR-CONS)))