Definstantiate
Add a witness-cp rule showing how to instantiate a universal
quantifier hypothesis (or an existential quantifier conclusion).
Example:
(definstantiate subsetp-equal-instancing
:predicate (subsetp-equal a b)
:vars (k)
:expr (implies (member-equal k a)
(member-equal k b))
:hints ('(:in-theory '(subsetp-member))))
The above example tells WITNESS-CP how to expand a hypothesis of the form
(subsetp-equal a b) or, equivalently, a conclusion of the form
(not (subsetp-equal a b)), by introducing a term of the form:
(implies (member-equal k a)
(member-equal k b))
For each of some various k, as determined by defexample rules
and any user-provided examples from the call of witness.
General Form
(definstantiate name
:predicate predicate
:vars vars
:expr expr
[: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 predicate. It
will replace these with a conjunction of several instantiations of expr,
with the free variables present in vars replaced by either user-provided
terms or terms generated by a defexample rule. It will use hints
to relieve the proof obligation that this replacement is sound, which is also
done when the definstantiate form is run.
Additional arguments:
You can syntactically restrict the application of an instantiation rule by
giving a restriction. The restriction may have free variables that
occur also in the predicate, term or the list of vars, as well as
acl2::world, standing for the ACL2 world. If a restriction is given,
then this replacement will only take place when it evaluates to a non-nil
value.
