## 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 rewrite 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.

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