Defwitness
Add a witness-cp rule providing a witness for an existential
quantifier hypothesis (or universal quantifier conclusion).
Example:
(defwitness subsetp-witnessing
:predicate (not (subsetp-equal a b))
:expr (and (member-equal (subsetp-equal-witness a b) a)
(not (member-equal (subsetp-equal-witness a b) b)))
:generalize (((subsetp-equal-witness a b) . ssew))
:hints ('(:in-theory '(subsetp-equal-witness-correct))))
The above example tells witness-cp to expand any hypothesis of the
form (not (subsetp-equal a b)) or, equivalently, any conclusion of the
form (subsetp-equal a b), by generating a fresh variable named SSEW or similar
that represents an object that proves that A is not a subset of B (because that
object is in A but not B.)
General Form:
(defwitness name
:predicate predicate
:expr expr
[:generalize generalize]
[:hints hints]
[:restriction restriction])
The name of the rule can be used in Witness Rulesets; see def-witness-ruleset.
When witness-cp is given a Witness Ruleset that includes name,
it will look for literals in the clause that unify with the negation of
predicate. It will replace these by a term generated from expr. It
will then generalize away terms that are keys in generalize, replacing
them by fresh variables based on their corresponding values. It will use
hints to relieve the proof obligation that this replacement is sound,
which is also done when the defwitness form is run.
Additional Arguments
You can syntactically restrict the application of a witness rule by giving a
restriction. The restriction term may have free variables that occur
also in the predicate term, and may also use the variable acl2::world
to stand for the ACL2 world. If a restriction is given, then this
replacement will only take place when it evaluates to a non-nil value.
