Major Section: EVENTS

Examples: (defun-sk exists-x-p0-and-q0 (y z) (exists x (and (p0 x y z) (q0 x y z))))(defun-sk exists-x-p0-and-q0 (y z) ; equivalent to the above (exists (x) (and (p0 x y z) (q0 x y z))))

(defun-sk forall-x-y-p0-and-q0 (z) (forall (x y) (and (p0 x y z) (q0 x y z))))

### EXISTS -- existential quantifier

### FORALL -- universal quantifier

### QUANTIFIERS -- issues about quantification in ACL2

`fn`

is the symbol you wish to define and is a new symbolic
name (see name), `(var1 ... varn)`

is its list of formal
parameters (see name), and `body`

is its body, which must be
quantified as described below. The `&key`

argument `doc`

is an optional
documentation string to be associated with `fn`

; for a description
of its form, see doc-string. In the case that `n`

is 1, the list
`(var1)`

may be replaced by simply `var1`

. The other arguments are
explained below. For a more elaborate example than those above,
see Tutorial4-Defun-Sk-Example.
See quantifiers for an example illustrating how the use of
recursion, rather than explicit quantification with `defun-sk`

, may be
preferable.

Below we describe the `defun-sk`

event precisely. First, let us
consider the examples above. The first example, again, is:

(defun-sk exists-x-p0-and-q0 (y z) (exists x (and (p0 x y z) (q0 x y z))))It is intended to represent the predicate with formal parameters

`y`

and `z`

that holds when for some `x`

, `(and (p0 x y z) (q0 x y z))`

holds. In fact `defun-sk`

is a macro that adds the following two
`events`

, as shown just below. The first axiom guarantees that if
this new predicate holds of `y`

and `z`

, then the term in question,
`(exists-x-p0-and-q0-witness y z)`

, is an example of the `x`

that is
therefore supposed to exist. (Intuitively, we are axiomatizing
`exists-x-p0-and-q0-witness`

to pick a witness if there is one.)
Conversely, the second event below guarantees that if there is any
`x`

for which the term in question holds, then the new predicate does
indeed holds of `y`

and `z`

.
(defun exists-x-p0-and-q0 (y z) (let ((x (exists-x-p0-and-q0-witness y z))) (and (p0 x y z) (q0 x y z)))) (defthm exists-x-p0-and-q0-suff (implies (and (p0 x y z) (q0 x y z)) (exists-x-p0-and-q0 y z)))Now let us look at the third example from the introduction above:

(defun-sk forall-x-y-p0-and-q0 (z) (forall (x y) (and (p0 x y z) (q0 x y z))))The intention is to introduce a new predicate

`(forall-x-y-p0-and-q0 z)`

which states that the indicated conjunction
holds of all `x`

and all `y`

together with the given `z`

. This time, the
axioms introduced are as shown below. The first event guarantees
that if the application of function `forall-x-y-p0-and-q0-witness`

to
`z`

picks out values `x`

and `y`

for which the given term
`(and (p0 x y z) (q0 x y z))`

holds, then the new predicate
`forall-x-y-p0-and-q0`

holds of `z`

. Conversely, the (contrapositive
of) the second axiom guarantees that if the new predicate holds of
`z`

, then the given term holds for all choices of `x`

and `y`

(and that
same `z`

).
(defun forall-x-y-p0-and-q0 (z) (mv-let (x y) (forall-x-y-p0-and-q0-witness z) (and (p0 x y z) (q0 x y z)))) (defthm forall-x-y-p0-and-q0-necc (implies (not (and (p0 x y z) (q0 x y z))) (not (forall-x-y-p0-and-q0 z))))The examples above suggest the critical property of

`defun-sk`

: it
indeed does introduce the quantified notions that it claims to
introduce.
We now turn to a detailed description `defun-sk`

, starting with a
discussion of its arguments as shown in the "General Form" above.

The third argument, `body`

, must be of the form

(Q bound-vars term)where:

`Q`

is the symbol `forall`

or `exists`

(in the "ACL2"
package), `bound-vars`

is a variable or true list of variables
disjoint from `(var1 ... varn)`

and not including `state`

, and
`term`

is a term. The case that `bound-vars`

is a single variable
`v`

is treated exactly the same as the case that `bound-vars`

is
`(v)`

.
The result of this event is to introduce a ``Skolem function,''
whose name is the keyword argument `skolem-name`

if that is
supplied, and otherwise is the result of modifying `fn`

by
suffixing "-WITNESS" to its name. The following definition and
the following two theorems are introduced for `skolem-name`

and `fn`

in the case that `bound-vars`

(see above) is a single
variable `v`

. The name of the `defthm`

event may be supplied as
the value of the keyword argument `:thm-name`

; if it is not
supplied, then it is the result of modifying `fn`

by suffixing
"-SUFF" to its name in the case that the quantifier is `exists`

,
and "-NECC" in the case that the quantifier is `forall`

.

(defun fn (var1 ... varn) (let ((v (skolem-name var1 ... varn))) term))In the case that(defthm fn-suff ;in case the quantifier is EXISTS (implies term (fn var1 ... varn)))

(defthm fn-necc ;in case the quantifier is FORALL (implies (not term) (not (fn var1 ... varn))))

`bound-vars`

is a list of at least two variables, say
`(bv1 ... bvk)`

, the definition above is the following instead, but
the theorem remains unchanged.
(defun fn (var1 ... varn) (mv-let (bv1 ... bvk) (skolem-name var1 ... varn) term))

In order to emphasize that the last element of the list `body`

is a
term, `defun-sk`

checks that the symbols `forall`

and `exists`

do
not appear anywhere in it. However, on rare occasions one might
deliberately choose to violate this convention, presumably because
`forall`

or `exists`

is being used as a variable or because a
macro call will be eliminating ``calls of'' `forall`

and `exists`

.
In these cases, the keyword argument `quant-ok`

may be supplied a
non-`nil`

value. Then `defun-sk`

will permit `forall`

and
`exists`

in the body, but it will still cause an error if there is
a real attempt to use these symbols as quantifiers.

Those who want a more flexible version of `defun-sk`

that allows
nested quantifiers, should contact the implementors. In the
meantime, if you want to represent nested quantifiers, you have to
manage that yourself. For example, in order to represent

(forall x (exists y (p x y z)))you would use

`defun-sk`

twice, for example as follows.
(defun-sk exists-y-p (x z) (exists y (p x y z)))(defun-sk forall-x-exists-y-p (z) (forall x (exists-y-p x z)))

Some distracting and unimportant warnings are inhibited during
`defun-sk`

.

`Defun-sk`

is implemented using `defchoose`

, and hence should only
be executed in defun-mode `:`

`logic`

; see defun-mode and
see defchoose.

Note that this way of implementing quantifiers is not a new idea.
Hilbert was certainly aware of it 60 years ago! A paper by ACL2
authors Kaufmann and Moore, entitled ``Structured Theory Development
for a Mechanized Logic'' (to appear in the Journal of Automated
Reasoning, 2000) explains why our use of `defchoose`

is
appropriate, even in the presence of `epsilon-0`

induction.