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

### DEFUN-SK-EXAMPLE -- a simple example using

`defun-sk`

### 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 simple example, see defun-sk-example. For a more elaborate example,
see Tutorial4-Defun-Sk-Example. Also 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 one of the following two theorems (as indicated) 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.

`Defun-sk`

is a macro implemented using `defchoose`

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

`logic`

; see defun-mode and
see defchoose.

If you find that the rewrite rules introduced with a particular use of
`defun-sk`

are not ideal, then at least two reasonable courses of action
are available for you. Perhaps the best option is to prove the `rewrite`

rules you want. If you see a pattern for creating rewrite rules from your
`defun-sk`

events, you might want to write a macro that executes a
`defun-sk`

followed by one or more `defthm`

events. Another option is
to write your own variant of the `defun-sk`

macro, say, `my-defun-sk`

,
for example by modifying a copy of the definition of `defun-sk`

from the
ACL2 sources.

If you want to represent nested quantifiers, you can use multiple
`defun-sk`

events. For example, in order to represent

(forall x (exists y (p x y z)))you can 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`

.

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'' (Journal of Automated Reasoning 26, no. 2 (2001),
pp. 161-203) explains why our use of `defchoose`

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

induction.