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





General Form:
(defun-sk fn (var1 ... varn) body
  &key doc quant-ok skolem-name thm-name)
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 more elaborate example than those above, see Tutorial4-Defun-Sk-Example.

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


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