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 event guarantees that if
this new predicate holds of `y`

and `z`

, then the term shown,
`(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 hold of `y`

and `z`

.
(defun exists-x-p0-and-q0 (y z) (declare (xargs :non-executable t)) (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) (declare (xargs :non-executable t)) (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.
Notice that the `defthm`

event just above, `forall-x-y-p0-and-q0-necc`

,
may not be of optimal form as a rewrite rule. Users sometimes find that when
the quantifier is `forall`

, it is useful to state this rule in a form where
the new quantified predicate is a hypothesis instead. In this case that form
would be as follows:

(defthm forall-x-y-p0-and-q0-necc (implies (forall-x-y-p0-and-q0 z) (and (p0 x y z) (q0 x y z))))ACL2 will turn this into one

`:`

`rewrite`

rule for each conjunct,
`(p0 x y z)`

and `(q0 x y z)`

, with hypothesis
`(forall-x-y-p0-and-q0 z)`

in each case. In order to get this effect, use
`:rewrite :direct`

, in this case as follows.
(defun-sk forall-x-y-p0-and-q0 (z) (forall (x y) (and (p0 x y z) (q0 x y z))) :rewrite :direct)

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) (declare (xargs :non-executable t)) (let ((v (skolem-name var1 ... varn))) term))(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))))

In the `forall`

case, however, the keyword pair `:rewrite :direct`

may be
supplied after the body of the `defun-sk`

form, in which case the
contrapositive of the above form is used instead:

(defthm fn-necc ;in case the quantifier is FORALL (implies (fn var1 ... varn) term))This is often a better choice for the "-NECC" rule, provided ACL2 can parse

`term`

as a `:`

`rewrite`

rule. A second possible value of the
`:rewrite`

argument of `defun-sk`

is `:default`

, which gives the same
behavior as when `:rewrite`

is omitted. Otherwise, the value of
`:rewrite`

should be the term to use as the body of the `fn-necc`

theorem
shown above; ACL2 will attempt to do the requisite proof in this case. If
that term is weaker than the default, the properties introduced by
`defun-sk`

may of course be weaker than they would be otherwise. Finally,
note that the `:rewrite`

keyword argument for `defun-sk`

only makes sense
if the quantifier is `forall`

; it is thus illegal if the quantifier is
`exists`

. Enough said about `:rewrite`

!
In the case that `bound-vars`

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

, the definition above (with no keywords) is the following
instead, but the theorem remains unchanged.

(defun fn (var1 ... varn) (declare (xargs :non-executable t)) (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.

Note the form `(declare (xargs :non-executable t))`

that appears in each
`defun`

above. These forms disable certain checks that are required for
execution, in particular the single-threaded use of `stobj`

s. However,
there is a price: calls of these defined functions cannot be evaluated.
Normally that is not a problem, since these notions involve quantifiers. But
you are welcome to replace this `declare`

form with your own, as follows:
if you supply a list of `declare`

forms to keyword argument
`:witness-dcls`

, these will become the declare forms in the generated
`defun`

.

`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, even when using the `:rewrite`

keyword
discussed above (in the `forall`

case), 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 more than one
`defun-sk`

event. 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! Also
see conservativity-of-defchoose for a technical argument that justifies the
logical conservativity of the `defchoose`

event in the sense of the paper
by Kaufmann and Moore entitled ``Structured Theory Development for a
Mechanized Logic'' (Journal of Automated Reasoning 26, no. 2 (2001),
pp. 161-203).