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