## DEFUN-SK

define a function whose body has an outermost quantifier
```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

General Form:
(defun-sk fn (var1 ... varn) body
&key doc quant-ok skolem-name thm-name witness-dcls)
```
where `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.

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 case that `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)
(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, 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! 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.