Add a witness-cp rule providing a witness for an existential
quantifier hypothesis (or universal quantifier conclusion).
: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.)
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.
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.