		Search-engine friendly clone of the ACL2 documentation.

Witness-cp

Defquantexpr

Shortcut to perform both a defwitness and definstantiate.

Example:

(defquantexpr subsetp-equal
  :predicate (subsetp-equal x y)
  :quantifier :forall
  :witnesses ((k (subsetp-equal-witness x y)))
  :expr (implies (member-equal k x)
                 (member-equal k y))
  :witness-hints ('(:in-theory '(subsetp-equal-witness-correct)))
  :instance-hints ('(:in-theory '(subsetp-member))))

This expands to a defwitness and a definstantiate form. The names of the resulting rules are generated from the name (first argument) of the defquantexpr form; in this case they are subsetp-witnessing and subsetp-equal-instancing.

Witness-hints and instance-hints are the hints passed to the two forms.

Additional arguments:

instance-rulename, provide a custom name for the definstantiate rule.
instance-restriction, the :restriction argument passed to definstantiate.
wcp-witness-rulename, provide a custom name for the defwitness rule.
witness-restriction, the :restriction argument passed to defwitness
generalize. If nil, then the defwitness rule will not do generalization; otherwise, it will use the keys of :witnesses as the variable names.

The meaning of this form is as follows:

":predicate holds iff (:quantifier) (keys of :witnesses), :expr."

In our example above:

"(subsetp-equal x y) iff for all k,
   (implies (member-equal k x)
            (member-equal k y))."

An example of this with an existential quantifier:

(defquantexpr intersectp-equal
  :predicate (intersectp-equal x y)
  :quantifier :exists
  :witnesses ((k (intersectp-equal-witness x y)))
  :expr (and (member-equal k x)
             (member-equal k y))
  :witness-hints ('(:in-theory '(intersectp-equal-witness-correct)))
  :instance-hints ('(:in-theory '(intersectp-equal-member))))

meaning:

"(intersectp-equal x y) iff there exists k such that
    (and (member-equal k x)
         (member-equal k y))".

the values bound to each key in :witnesses should be witnesses for the existential quantifier in the direction of the bi-implication that involves (the forward direction for :exists and the backward for :forall):

for the first example,

"(let ((k (subsetp-equal-witness x y)))
     (implies (member-equal k x)
              (member-equal k y)))
  ==>
  (subsetp-equal x y)."

for the second example,

"(intersectp-equal x y)
  ==>
  (let ((k (intersectp-equal-witness x y)))
    (and (member-equal k x)
         (member-equal k y)))."