DEFCHOOSE

define a Skolem (witnessing) function 
Major Section:  EVENTS


Examples:
(defchoose choose-x-for-p-and-q (x) (y z)
  (and (p x y z)
       (q x y z)))


(defchoose choose-x-for-p-and-q x (y z) ; equivalent to the above
  (and (p x y z)
       (q x y z)))


(defchoose choose-x-and-y-for-p-and-q (x y) (z)
  (and (p x y z)
       (q x y z)))


General Form:
(defchoose fn 
           (bound-var1 ... bound-varn)
           (free-var1 ... free-vark)
           doc-string ; optional
           body),
where fn is the symbol you wish to define and is a new symbolic name (see name), (bound-var1 ... bound-varn) is a list of distinct `bound' variables (see below), (free-var1 ... free-vark) is the list of formal parameters of fn and is disjoint from the bound variables, and body is a term. The use of lambda-list keywords (such as &optional) is not allowed. The documentation string, doc-string, is optional; for a description of its form, see doc-string.

In the most common case, where there is only one bound variable, it is permissible to omit the enclosing parentheses on that variable. The effect is the same whether or not those parentheses are omitted. We describe this case first, where there is only one bound variable, and address the other case at the end.

The effect of the form 

(defchoose fn bound-var (free-var1 ... free-vark)
  body)
is to introduce a new function symbol, fn, with formal parameters (free-var1 ... free-vark), and the following axiom stating that fn picks a value of bound-var so that the body will be true, if such a value exists: 
(implies body
         (let ((bound-var (fn free-var1 ... free-vark)))
           body))
This axiom is ``clearly'' conservative under the conditions expressed above: the function fn merely picks out a ``witnessing'' value of bound-var if there is one. The system in fact treats fn very much as though it were declared in the signature of an encapsulate event, with the axiom above as the only axiom exported.

If there is more than one bound variable, as in 

(defchoose fn 
           (bound-var1 ... bound-varn)
           (free-var1 ... free-vark)
           body)
then fn returns n multiple values, and the defining axiom is expressed using mv-let (see mv-let) as follows: 
(implies body
         (mv-let (bound-var1 ... bound-varn)
                 (fn free-var1 ... free-vark)
                 body))

Defchoose is only executed in defun-mode :logic; see defun-mode.

Also see defun-sk.

Comment for logicians: As we point out in the documentation for defun-sk, defchoose is ``appropriate,'' by which we mean that it is conservative, even in the presence of epsilon-0 induction. This fact is shown in a paper by ACL2 authors Kaufmann and Moore, entitled ``Structured Theory Development for a Mechanized Logic'' (Journal of Automated Reasoning 26, no. 2 (2001), pp. 161-203).