Major Section: EVENTS

Examples: (defchoose choose-x-for-p-and-q (x) (y z) (and (p x y z) (q x y z)))where(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),

`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).