Define a function whose body has an outermost quantifier

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))) :strengthen t) General Form: (defun-sk fn (var1 ... varn) dcl_1 dcl_2 ... dcl_k body &key rewrite quant-ok skolem-name thm-name strengthen constrain verbose)

where `declare` forms, and

For a simple example, see defun-sk-example. For a more elaborate
example, see Tutorial4-Defun-Sk-Example. See quantifier-tutorial for a careful beginner's introduction that takes you
through typical kinds of quantifier-based reasoning in ACL2. Also see quantifiers for an example illustrating how the use of recursion, rather than
explicit quantification with

Below we describe the

(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 `defun-nx`; for now, consider `defun`.) Conversely, the second event below guarantees that if there
is any

(defun-nx 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

(defun-nx 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

Notice that the `defthm` event just above,

(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,

(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 of

The third argument,

(Q bound-vars term)

where: `forall` or `exists`, in the
"ACL2" package; `state`; and

The result of this event is to introduce a ``Skolem function,'' whose name
is the keyword argument `defthm` event may be supplied as the value of the keyword argument
`exists`, and "-NECC" in the case that the quantifier is `forall`.

(defun-nx fn (var1 ... varn) (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

(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 `rewrite` rule. A second possible value of
the

In the case that

(defun-nx fn (var1 ... varn) (mv-let (bv1 ... bvk) (skolem-name var1 ... varn) term))

In order to emphasize that the last element of the list, `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 `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.

The use of `defun-nx` above, rather than `defun`, disables
certain checks that are required for evaluation, for example in the passing of
multiple values. However, there is a price: calls of these defined functions
cannot be evaluated; see defun-nx. Normally that is not a problem,
since these notions involve quantifiers. But if you prefer that `defun`
be used instead of `declare`
forms, given as the `defun`. If the `xargs` declaration form `defun`
will be used in place of `defun-nx`.

Guard verification is performed for `set-verify-guards-eagerness`. Technical note: such
guard verification is implemented through a generated call of `verify-guards` after the `trans1` to see the expansion.

`defchoose`. Hence, it
should only be executed in defun-mode `logic`; see defun-mode and see defchoose. You can use the command `pcb!` to see the event generated by a call of the

An advanced feature is argument

If you find that the rewrite rules introduced with a particular use of
`rewrite` rules you want. If you see a pattern for creating rewrite
rules from your `defthm` events.
Another option is to write your own variant of the

There is one more keyword argument not explained above: `definition` that equates

If you want to represent nested quantifiers, you can use more than one

(forall x (exists y (p x y z)))

you can use

(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

Note for ACL2(r) users (see real): In ACL2(r), the keyword

Note that this way of implementing quantifiers is not a new idea. Hilbert
was certainly aware of it in the first half of the 20th century! 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).

- Define-sk
- A very fine alternative to
`defun-sk`. - Quantifier-tutorial
- A Beginner's Guide to Reasoning about Quantification in ACL2
- Defun-sk-queries
- Utilities to query
`defun-sk`functions. - Quantifiers
- Issues about quantification in ACL2
- Defun-sk-example
- A simple example using
`defun-sk` - Defund-sk
- Define a function with quantifier and disable it and its associated rewrite rule.
- Forall
- Universal quantifier
- Def::un-sk
- An extension of defun-sk that supports automated skolemization and instantiation of quantified formulae
- Equiv
- A macro to prove that a universally quantified formula is a paramaterized equivalence relation
- Exists
- Existential quantifier
- Congruence
- A macro to prove congruence rules for quantified formulae and their associated witnesses