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),
fnis 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
fnand is disjoint from the bound variables, and
bodyis a term. The use of
lambda-listkeywords (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
fnpicks a value of
bound-varso 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
fnmerely picks out a ``witnessing'' value of
bound-varif there is one. The system in fact treats
fnvery much as though it were declared in the signature of an
encapsulateevent, 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
nmultiple 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
Also see defun-sk.
Comment for logicians: As we point out in the documentation for
defchoose is ``appropriate,'' by which we mean that
it is conservative, even in the presence of
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).