This is documentation for ACL2 Version 3.3
Copyright (C) 2007  University of Texas at Austin

This program is free software; you can redistribute it and/or modify
it under the terms of the GNU General Public License as published by
the Free Software Foundation; either version 2 of the License, or
(at your option) any later version.

This program is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
GNU General Public License for more details.

You should have received a copy of the GNU General Public License
along with this program; if not, write to the Free Software
Foundation, Inc., 675 Mass Ave, Cambridge, MA 02139, USA.

Written by:  Matt Kaufmann and J Strother Moore
Department of Computer Sciences
University of Texas at Austin
Austin, TX 78712-1188 U.S.A.

DEFUN    define a function symbol

     Examples:
     (defun app (x y)
       (if (consp x)
           (cons (car x) (app (cdr x) y))
           y))

     (defun fact (n)
       (declare (xargs :guard (and (integerp n)
                                   (>= n 0))))
       (if (zp n)
           1
           (* n (fact (1- n)))))

     General Form:
     (defun fn (var1 ... varn) doc-string dcl ... dcl body),

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.  The definitional axiom is
logically admissible provided certain restrictions are met.  These are
sketched below.

Note that ACL2 does not support the use of lambda-list keywords (such
as &optional) in the formals list of functions.  We do support some
such keywords in macros and often you can achieve the desired syntax by
defining a macro in addition to the general version of your function.
See DEFMACRO.  The documentation string, doc-string, is
optional; for a description of its form, see DOC-STRING.

The _declarations_ (see DECLARE), dcl, are also optional.  If
more than one dcl form appears, they are effectively grouped together
as one.  Perhaps the most commonly used ACL2 specific declaration is of
the form (declare (xargs :guard g :measure m)).  This declaration in
the defun of some function fn has the effect of making the "guard" for
fn be the term g and the "measure" be the term m.  The notion of
"measure" is crucial to ACL2's definitional principle.  The notion of
"guard" is not, and is discussed elsewhere; see VERIFY-GUARDS
and see SET-VERIFY-GUARDS-EAGERNESS.  Note that the :measure is
ignored in :program mode; see DEFUN-MODE.

We now briefly discuss the ACL2 definitional principle, using the
following definition form which is offered as a more or less generic
example.

     (defun fn (x y)
       (declare (xargs :guard (g x y)
                       :measure (m x y)))
       (if (test x y)
           (stop x y)
           (step (fn (d x) y))))

Note that in our generic example, fn has just two arguments, x and y,
the guard and measure terms involve both of them, and the body is a
simple case split on (test x y) leading to a "non-recursive" branch,
(stop x y), and a "recursive" branch.  In the recursive branch, fn is
called after "decrementing" x to (d x) and some step function is
applied to the result.  Of course, this generic example is quite
specific in form but is intended to illustrate the more general case.

Provided this definition is admissible under the logic, as outlined
below, it adds the following axiom to the logic.

     Defining Axiom:
     (fn x y)
       =
     (if (test x y)
         (stop x y)
       (step (fn (d x) y)))

Note that the guard of fn has no bearing on this logical axiom.

This defining axiom is actually implemented in the ACL2 system by a
:definition rule, namely

     (equal (fn x y)
            (if (test a b)
                (stop a b)
              (step (fn (d a) b)))).

See DEFINITION for a discussion of how definition rules are
applied.  Roughly speaking, the rule causes certain instances of (fn x
y) to be replaced by the corresponding instances of the body above.
This is called "opening up" (fn x y).  The instances of (fn x y) opened
are chosen primarily by heuristics which determine that the recursive
calls of fn in the opened body (after simplification) are more
desirable than the unopened call of fn.

This discussion has assumed that the definition of fn was admissible.
Exactly what does that mean?  First, fn must be a previously
unaxiomatized function symbol (however, see
LD-REDEFINITION-ACTION).  Second, the formal parameters must be
distinct variable names.  Third, the guard, measure, and body should
all be terms and should mention no free variables except the formal
parameters.  Thus, for example, body may not contain references to
"global" or "special" variables; ACL2 constants or additional formals
should be used instead.

The final conditions on admissibility concern the termination of the
recursion.  Roughly put, all applications of fn must terminate.  In
particular, there must exist a binary relation, rel, and some unary
predicate mp such that rel is well-founded on objects satisfying mp,
the measure term m must always produce something satisfying mp, and the
measure term must decrease according to rel in each recursive call,
under the hypothesis that all the tests governing the call are
satisfied.  By the meaning of well-foundedness, we know there are no
infinitely descending chains of successively rel-smaller mp-objects.
Thus, the recursion must terminate.

The only primitive well-founded relation in ACL2 is o< (see
O<), which is known to be well-founded on the o-ps (see O-P).
For the proof of well-foundedness, see
PROOF-OF-WELL-FOUNDEDNESS.  However it is possible to add new
well-founded relations.  For details, see
WELL-FOUNDED-RELATION.  We discuss later how to specify which
well-founded relation is selected by defun and in the present
discussion we assume, without loss of generality, that it is o< on the
o-ps.

For example, for our generic definition of fn above, with measure term
(m x y), two theorems must be proved.  The first establishes that m
produces an ordinal:

     (o-p (m x y)).

The second shows that m decreases in the (only) recursive call of fn:

     (implies (not (test x y))
              (o< (m (d x) y) (m x y))).

Observe that in the latter formula we must show that the "m-size" of (d
x) and y is "smaller than" the m-size of x and y, provided the test,
(test x y), in the body fails, thus leading to the recursive call (fn
(d x) y).

See O< for a discussion of this notion of "smaller than."  It
should be noted that the most commonly used ordinals are the natural
numbers and that on natural numbers, o< is just the familiar "less
than" relation (<).  Thus, it is very common to use a measure m that
returns a nonnegative integer, for then (o-p (m x y)) becomes a simple
conjecture about the type of m and the second formula above becomes a
conjecture about the less-than relationship of nonnegative integer
arithmetic.

The most commonly used measure function is acl2-count, which computes a
nonnegative integer size for all ACL2 objects.  See ACL2-COUNT.

Probably the most common recursive scheme in Lisp programming is when
some formal is supposed to be a list and in the recursive call it is
replaced by its cdr.  For example, (test x y) might be simply (atom x)
and (d x) might be (cdr x).  In that case, (acl2-count x) is a suitable
measure because the acl2-count of a cons is strictly larger than the
acl2-counts of its car and cdr.  Thus, "recursion by car" and
"recursion by cdr" are trivially admitted if acl2-count is used as the
measure and the definition protects every recursive call by a test
insuring that the decremented argument is a consp.  Similarly,
"recursion by 1-" in which a positive integer formal is decremented by
one in recursion, is also trivially admissible.  See
BUILT-IN-CLAUSES to extend the class of trivially admissible
recursive schemes.

We now turn to the question of which well-founded relation defun uses.
It should first be observed that defun must actually select both a
relation (e.g., o<) and a domain predicate (e.g., o-p) on which that
relation is known to be well-founded.  But, as noted elsewhere (see
WELL-FOUNDED-RELATION), every known well-founded relation has a
unique domain predicate associated with it and so it suffices to
identify simply the relation here.

The xargs field of a declare permits the explicit specification of any
known well-founded relation with the keyword :well-founded-relation.
An example is given below.  If the xargs for a defun specifies a
well-founded relation, that relation and its associated domain
predicate are used in generating the termination conditions for the
definition.

If no :well-founded-relation is specified, defun uses the
:well-founded-relation specified in the acl2-defaults-table.  See
SET-WELL-FOUNDED-RELATION to see how to set the default well-founded
relation (and, implicitly, its domain predicate).  The initial default
well-founded relation is o< (with domain predicate o-p).

This completes the brief sketch of the ACL2 definitional principle.

On very rare occasions ACL2 will seem to "hang" when processing a
definition, especially if there are many subexpressions of the body
whose function symbol is if (or which macroexpand to such an
expression).  In those cases you may wish to supply the following to
xargs:  :normalize nil.  This is an advanced feature that turns off
ACL2's usual propagation upward of if tests.

The following example illustrates all of the available declarations,
but is completely nonsensical.  For documentation, see XARGS and
see HINTS.

     (defun example (x y z a b c i j)
       (declare (ignore a b c)
                (type integer i j)
                (xargs :guard (symbolp x)
                       :measure (- i j)
                       :well-founded-relation my-wfr
                       :hints (("Goal"
                                :do-not-induct t
                                :do-not '(generalize fertilize)
                                :expand ((assoc x a) (member y z))
                                :restrict ((<-trans ((x x) (y (foo x)))))
                                :hands-off (length binary-append)
                                :in-theory (set-difference-theories
                                             (current-theory :here)
                                             '(assoc))
                                :induct (and (nth n a) (nth n b))
                                :use ((:instance assoc-of-append
                                                 (x a) (y b) (z c))
                                      (:functional-instance
                                        (:instance p-f (x a) (y b))
                                        (p consp)
                                        (f assoc)))))
                       :guard-hints (("Subgoal *1/3'"
                                      :use ((:instance assoc-of-append
                                                       (x a) (y b) (z c)))))
                       :mode :logic
                       :normalize nil
                       :verify-guards nil
                       :non-executable t
                       :otf-flg t))
       (example-body x y z i j))

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

     * Menu:

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

DEFUN-SK-EXAMPLE    a simple example using defun-sk

The following example illustrates how to do proofs about functions
defined with defun-sk.  The events below can be put into a certifiable
book (see BOOKS).  The example is contrived and rather silly,
in that it shows how to prove that a quantified notion implies itself,
where the antecedent and conclusion are defined with different defun-sk
events.  But it illustrates the formulas that are generated by
defun-sk, and how to use them.  Thanks to Julien Schmaltz for
presenting this example as a challenge.

     (in-package "ACL2")

     (encapsulate
      (((p *) => *)
       ((expr *) => *))

      (local (defun p (x) x))
      (local (defun expr (x) x)))

     (defun-sk forall-expr1 (x)
       (forall (y) (implies (p x) (expr y))))

     (defun-sk forall-expr2 (x)
       (forall (y) (implies (p x) (expr y)))))

     ; We want to prove the theorem my-theorem below.  What axioms are there that
     ; can help us?  If you submit the command

     ; :pcb! forall-expr1

     ; then you will see the following two key events.  (They are completely
     ; analogous of course for FORALL-EXPR2.)

     #|
     (DEFUN FORALL-EXPR1 (X)
       (LET ((Y (FORALL-EXPR1-WITNESS X)))
            (IMPLIES (P X) (EXPR Y))))

     (DEFTHM FORALL-EXPR1-NECC
       (IMPLIES (NOT (IMPLIES (P X) (EXPR Y)))
                (NOT (FORALL-EXPR1 X)))
       :HINTS
       (("Goal" :USE FORALL-EXPR1-WITNESS)))
     |#

     ; We see that the latter has value when FORALL-EXPR1 occurs negated in a
     ; conclusion, or (therefore) positively in a hypothesis.  A good rule to
     ; remember is that the former has value in the opposite circumstance: negated
     ; in a hypothesis or positively in a conclusion.

     ; In our theorem, FORALL-EXPR2 occurs positively in the conclusion, so its
     ; definition should be of use.  We therefore leave its definition enabled,
     ; and disable the definition of FORALL-EXPR1.

     #|
     (thm
       (implies (and (p x) (forall-expr1 x))
                (forall-expr2 x))
       :hints (("Goal" :in-theory (disable forall-expr1))))

     ; which yields this unproved subgoal:

     (IMPLIES (AND (P X) (FORALL-EXPR1 X))
              (EXPR (FORALL-EXPR2-WITNESS X)))
     |#

     ; Now we can see how to use FORALL-EXPR1-NECC to complete the proof, by
     ; binding y to (FORALL-EXPR2-WITNESS X).

     ; We use defthmd below so that the following doesn't interfere with the
     ; second proof, in my-theorem-again that follows.
     (defthmd my-theorem
       (implies (and (p x) (forall-expr1 x))
                (forall-expr2 x))
       :hints (("Goal"
                :use ((:instance forall-expr1-necc
                                 (x x)
                                 (y (forall-expr2-witness x)))))))

     ; The following illustrates a more advanced technique to consider in such
     ; cases.  If we disable forall-expr1, then we can similarly succeed by having
     ; FORALL-EXPR1-NECC applied as a :rewrite rule, with an appropriate hint in how
     ; to instantiate its free variable.  See :doc hints.

     (defthm my-theorem-again
       (implies (and (P x) (forall-expr1 x))
                (forall-expr2 x))
       :hints (("Goal"
                :in-theory (disable forall-expr1)
                :restrict ((forall-expr1-necc
                            ((y (forall-expr2-witness x))))))))

EXISTS    existential quantifier

The symbol exists (in the ACL2 package) represents existential
quantification in the context of a defun-sk form.  See DEFUN-SK
and see FORALL.

See QUANTIFIERS for an example illustrating how the use of
recursion, rather than explicit quantification with defun-sk, may be
preferable.

FORALL    universal quantifier

The symbol forall (in the ACL2 package) represents universal
quantification in the context of a defun-sk form.  See DEFUN-SK
and see EXISTS.

See QUANTIFIERS for an example illustrating how the use of
recursion, rather than explicit quantification with defun-sk, may be
preferable.

QUANTIFIERS    issues about quantification in ACL2

ACL2 supports first-order quantifiers exists and forall by way of the
defun-sk event.  However, proof support for quantification is quite
limited.  Therefore, we recommend using recursion in place of defun-sk
when possible (following common ACL2 practice).

For example, the notion "every member of x has property p" can be
defined either with recursion or explicit quantification, but proofs
may be simpler when recursion is used.  We illustrate this point with
two proofs of the same informal claim, one of which uses recursion
which the other uses explicit quantification.  Notice that with
recursion, the proof goes through fully automatically; but this is far
from true with explicit quantification (especially notable is the ugly
hint).

The informal claim for our examples is:  If every member a of each of
two lists satisfies the predicate (p a), then this holds of their
append; and, conversely.

See QUANTIFIERS-USING-RECURSION for a solution to this example
using recursion.

See QUANTIFIERS-USING-DEFUN-SK for a solution to this example
using defun-sk.  Also See QUANTIFIERS-USING-DEFUN-SK-EXTENDED
for an elaboration on that solution.

QUANTIFIERS-USING-DEFUN-SK    quantification example

See QUANTIFIERS for the context of this example.  It should be
compared to a corresponding example in which a simpler proof is
attained by using recursion in place of explicit quantification; see
QUANTIFIERS-USING-RECURSION.

     (in-package "ACL2")

     ; We prove that if every member A of each of two lists satisfies the
     ; predicate (P A), then this holds of their append; and, conversely.

     ; Here is a solution using explicit quantification.

     (defstub p (x) t)

     (defun-sk forall-p (x)
       (forall a (implies (member a x)
                          (p a))))

     (defthm member-append
       (iff (member a (append x1 x2))
            (or (member a x1) (member a x2))))

     (defthm forall-p-append
       (equal (forall-p (append x1 x2))
              (and (forall-p x1) (forall-p x2)))
       :hints (("Goal" ; ``should'' disable forall-p-necc, but no need
                :use
                ((:instance forall-p-necc
                            (x (append x1 x2))
                            (a (forall-p-witness x1)))
                 (:instance forall-p-necc
                            (x (append x1 x2))
                            (a (forall-p-witness x2)))
                 (:instance forall-p-necc
                            (x x1)
                            (a (forall-p-witness (append x1 x2))))
                 (:instance forall-p-necc
                            (x x2)
                            (a (forall-p-witness (append x1 x2))))))))

Also see QUANTIFIERS-USING-DEFUN-SK-EXTENDED for an elaboration
on this example.

QUANTIFIERS-USING-DEFUN-SK-EXTENDED    quantification example with details

See QUANTIFIERS-USING-DEFUN-SK for the context of this example.

     (in-package "ACL2")

     ; We prove that if every member A of each of two lists satisfies the
     ; predicate (P A), then this holds of their append; and, conversely.

     ; Here is a solution using explicit quantification.

     (defstub p (x) t)

     (defun-sk forall-p (x)
       (forall a (implies (member a x)
                          (p a))))

     ; The defun-sk above introduces the following axioms.  The idea is that
     ; (FORALL-P-WITNESS X) picks a counterexample to (forall-p x) if there is one.

     #|
     (DEFUN FORALL-P (X)
       (LET ((A (FORALL-P-WITNESS X)))
            (IMPLIES (MEMBER A X) (P A))))

     (DEFTHM FORALL-P-NECC
       (IMPLIES (NOT (IMPLIES (MEMBER A X) (P A)))
                (NOT (FORALL-P X)))
       :HINTS (("Goal" :USE FORALL-P-WITNESS)))
     |#

     ; The following lemma seems critical.

     (defthm member-append
       (iff (member a (append x1 x2))
            (or (member a x1) (member a x2))))

     ; The proof of forall-p-append seems to go out to lunch, so we break into
     ; directions as shown below.

     (defthm forall-p-append-forward
       (implies (forall-p (append x1 x2))
                (and (forall-p x1) (forall-p x2)))
       :hints (("Goal" ; ``should'' disable forall-p-necc, but no need
                :use
                ((:instance forall-p-necc
                            (x (append x1 x2))
                            (a (forall-p-witness x1)))
                 (:instance forall-p-necc
                            (x (append x1 x2))
                            (a (forall-p-witness x2)))))))

     (defthm forall-p-append-reverse
       (implies (and (forall-p x1) (forall-p x2))
                (forall-p (append x1 x2)))
       :hints (("Goal"
                :use
                ((:instance forall-p-necc
                            (x x1)
                            (a (forall-p-witness (append x1 x2))))
                 (:instance forall-p-necc
                            (x x2)
                            (a (forall-p-witness (append x1 x2))))))))

     (defthm forall-p-append
       (equal (forall-p (append x1 x2))
              (and (forall-p x1) (forall-p x2)))
       :hints (("Goal" :use (forall-p-append-forward
                             forall-p-append-reverse))))

QUANTIFIERS-USING-RECURSION    recursion for implementing quantification

The following example illustrates the use of recursion as a means of
avoiding proof difficulties that can arise from the use of explicit
quantification (via defun-sk).  See QUANTIFIERS for more about
the context of this example.

     (in-package "ACL2")

     ; We prove that if every member A of each of two lists satisfies the
     ; predicate (P A), then this holds of their append; and, conversely.

     ; Here is a solution using recursively-defined functions.

     (defstub p (x) t)

     (defun all-p (x)
       (if (atom x)
           t
         (and (p (car x))
              (all-p (cdr x)))))

     (defthm all-p-append
       (equal (all-p (append x1 x2))
              (and (all-p x1) (all-p x2))))

DEFUND    define a function symbol and then disable it

Use defund instead of defun when you want to disable a function
immediately after its definition.  This macro has been provided for
users who prefer working in a mode where functions are only enabled
when explicitly directed by :in-theory.  Specifically, the form

     (defund NAME FORMALS ...)

expands to:

     (progn
       (defun NAME FORMALS ...)
       (with-output
        :off summary
        (in-theory (disable NAME)))
       (value NAME)).

Only the :definition rule (and, for recursively defined functions, the
:induction rule) for the function are disabled, and the summary for the
in-theory event is suppressed.

Note that defund commands are never redundant (see
REDUNDANT-EVENTS).  If the function has already been defined, then
the in-theory event will still be executed.

See DEFUN for documentation of defun.

ENCAPSULATE    constrain some functions and/or hide some events

The following example illustrates the idea of encapsulate.

     (encapsulate

     ; Introduce a function foo of one argument that returns one value:
      ( ((foo *) => *) )

     ; Introduce a ``witness'' (example) for foo, marked as local so that
     ; it is not exported:
      (local (defun foo (x) x))

     ; Introduce a non-local property to be exported:
      (defthm foo-preserves-consp
        (implies (consp x)
     	      (consp (foo x))))
     )

The form above introduces a new function symbol, foo, with the indicated
property and no definition.  In fact, the output from ACL2 concludes as
follows.

     The following constraint is associated with the function FOO:

     (IMPLIES (CONSP X) (CONSP (FOO X)))

We turn now to more complete documentation.

     Other Examples:
     (encapsulate (((an-element *) => *))

     ; The list of signatures above could also be written
     ;            ((an-element (lst) t))

       (local (defun an-element (lst)
                (if (consp lst) (car lst) nil)))
       (local (defthm member-equal-car
                 (implies (and lst (true-listp lst))
                          (member-equal (car lst) lst))))
       (defthm thm1
          (implies (null lst) (null (an-element lst))))
       (defthm thm2
          (implies (and (true-listp lst)
                        (not (null lst)))
                   (member-equal (an-element lst) lst))))

     (encapsulate
      () ; empty signature: no constrained functions indicated

      (local (defthm hack
               (implies (and (syntaxp (quotep x))
                             (syntaxp (quotep y)))
                        (equal (+ x y z)
                               (+ (+ x y) z)))))

      (defthm nthcdr-add1-conditional
        (implies (not (zp (1+ n)))
                 (equal (nthcdr (1+ n) x)
                        (nthcdr n (cdr x))))))

     General Form:
     (encapsulate (signature ... signature)
       ev1
       ...
       evn)

where each signature is a well-formed signature (see
SIGNATURE), each signature describes a different function symbol, and
each evi is an embedded event form (See EMBEDDED-EVENT-FORM).
There must be at least one evi.  The evi inside local special forms are
called "local" events below.  Events that are not local are sometimes
said to be "exported" by the encapsulation.  We make the further
restriction that no defaxiom event may be introduced in the scope of an
encapsulate (not even by encapsulate or include-book events that are
among the evi).  Furthermore, no non-local include-book event is
permitted in the scope of any encapsulate with a non-empty list of
signatures.

To be well-formed, an encapsulate event must have the properties that
each event in the body (including the local ones) can be successfully
executed in sequence and that in the resulting theory, each function
mentioned among the signatures was introduced via a local event and has
the signature listed.  (A utility is provided to assist in debugging
failures of such execution; see REDO-FLAT.)  In addition, the
body may contain no "local incompatibilities" which, roughly stated,
means that the events that are not local must not syntactically require
symbols defined by local events, except for the functions listed in the
signatures.  See LOCAL-INCOMPATIBILITY.  Finally, no non-local
recursive definition in the body may involve in its suggested induction
scheme any function symbol listed among the signatures.  See
SUBVERSIVE-RECURSIONS.

The result of an encapsulate event is an extension of the logic in
which, roughly speaking, the functions listed in the signatures are
constrained to have the signatures listed and to satisfy the non-local
theorems proved about them.  In fact, other functions introduced in the
encapsulate event may be considered to have "constraints" as well.
(See CONSTRAINT for details, which are only relevant to
functional instantiation.)  Since the constraints were all theorems in
the "ephemeral" or "local" theory, we are assured that the extension
produced by encapsulate is sound.  In essence, the local definitions of
the constrained functions are just "witness functions" that establish
the consistency of the constraints.  Because those definitions are
local, they are not present in the theory produced by encapsulation.
Encapsulate also exports all rules generated by its non-local events,
but rules generated by local events are not exported.

The default-defun-mode for the first event in an encapsulation is the
default defun-mode "outside" the encapsulation.  But since events
changing the defun-mode are permitted within the body of an
encapsulate, the default defun-mode may be changed.  However,
defun-mode changes occurring within the body of the encapsulate are not
exported.  In particular, the acl2-defaults-table after an encapsulate
is always the same as it was before the encapsulate, even though the
encapsulate body might contain defun-mode changing events, :program and
:logic.  See DEFUN-MODE.  More generally, after execution of an
encapsulate event, the value of acl2-defaults-table is restored to what
it was immediately before that event was executed.  See
ACL2-DEFAULTS-TABLE.

Theorems about the constrained function symbols may then be proved --
theorems whose proofs necessarily employ only the constraints.  Thus,
those theorems may be later functionally instantiated, as with the
:functional-instance lemma instance (see LEMMA-INSTANCE), to
derive analogous theorems about different functions, provided the
constraints (see CONSTRAINT) can be proved about the new
functions.

Observe that if the signatures list is empty, encapsulate may still be
useful for deriving theorems to be exported whose proofs require lemmas
you prefer to hide (i.e., made local).

The order of the events in the vicinity of an encapsulate is confusing.
We discuss it in some detail here because when logical names are being
used with theory functions to compute sets of rules, it is sometimes
important to know the order in which events were executed.  (See
LOGICAL-NAME and see THEORY-FUNCTIONS.)  What, for example,
is the set of function names extant in the middle of an encapsulation?

If the most recent event is previous and then you execute an
encapsulate constraining an-element with two non-local events in its
body, thm1 and thm2, then the order of the events after the
encapsulation is (reading chronologically forward): previous, thm1,
thm2, an-element (the encapsulate itself).  Actually, between previous
and thm1 certain extensions were made to the world by the superior
encapsulate, to permit an-element to be used as a function symbol in
thm1.

Finally, we note that an encapsulate event is redundant if and only if
a syntactically identical encapsulate has already been executed under
the same default-defun-mode.  See REDUNDANT-EVENTS.

EVISC-TABLE    support for abbreviated output

The evisc-table is an ACL2 table (see TABLE) whose purpose is
to modify the print representations of specified non-nil objects.  When
a key (some object) is associated with a string value, then that string
is printed instead of that key (as an abbreviation).  For example, the
following log shows how to abbreviate the key (a b c) with the token
<my-abc-list>.

     ACL2 !>(table evisc-table '(a b c) "<my-abc-list>")

     Summary
     Form:  ( TABLE EVISC-TABLE ...)
     Rules: NIL
     Warnings:  None
     Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
      EVISC-TABLE
     ACL2 !>'(a b c)
     <my-abc-list>
     ACL2 !>'(4 5 a b c)
     (4 5 . <my-abc-list>)
     ACL2 !>

Every value in this table must be either a string or nil, where nil
eliminates any association of the key with an abbreviation.  Continuing
with the log above:

     ACL2 !>(table evisc-table '(a b c) nil)

     Summary
     Form:  ( TABLE EVISC-TABLE ...)
     Rules: NIL
     Warnings:  None
     Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
      EVISC-TABLE
     ACL2 !>'(a b c)
     (A B C)
     ACL2 !>'(4 5 a b c)
     (4 5 A B C)
     ACL2 !>

It can be particularly helpful to use this table to abbreviate a
constant introduced by defconst by prefixing the constant name with
"#,", as we now describe.  Consider first the following example.

     (defconst *abc* '(1 2 3 4 5 6 7 8))
     (table evisc-table *abc*
       (concatenate 'string "#," (symbol-name '*abc*)))

Then the constant *abc* is printed as follows -- very helpful if its
associated structure is significantly larger than the 8-element list of
numbers shown above!

     ACL2 !>*abc*
     #,*ABC*
     ACL2 !>

What's more, the ACL2 reader will replace #,*C*, where *C* is defined by
defconst, by its value, regardless of evisc-table; see
SHARP-COMMA-READER.  Continuing with the example above, we have:

     ACL2 !>(cdr (quote #,*ABC*))
     (2 3 4 5 6 7 8)
     ACL2 !>

Of course, more care needs to be taken if packages are involved (see
DEFPKG), as we now illustrate.

     ACL2 !>(defpkg "FOO" nil)

     Summary
     Form:  ( DEFPKG "FOO" ...)
     Rules: NIL
     Warnings:  None
     Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
      "FOO"
     ACL2 !>(defconst foo::*a* '(1 2 3))

     Summary
     Form:  ( DEFCONST FOO::*A* ...)
     Rules: NIL
     Warnings:  None
     Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
      FOO::*A*
     ACL2 !>(table evisc-table foo::*a* "#,foo::*a*")

     Summary
     Form:  ( TABLE EVISC-TABLE ...)
     Rules: NIL
     Warnings:  None
     Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
      EVISC-TABLE
     ACL2 !>foo::*a*
     #,foo::*a*
     ACL2 !>'#,foo::*a*
     #,foo::*a*
     ACL2 !>(cdr '#,foo::*a*)
     (2 3)
     ACL2 !>

IN-ARITHMETIC-THEORY    designate ``current'' theory for some rewriting done in linear arithmetic

     Example:
     (in-arithmetic-theory '(lemma1 lemma2))

     General Form:
     (in-arithmetic-theory term :doc doc-string)

where term is a term that when evaluated will produce a theory (see
THEORIES), and doc-string is an optional documentation string
not beginning with ":doc-section ...".  Except for the variable world,
term must contain no free variables.  Term is evaluated with the
variable world bound to the current world to obtain a theory and the
corresponding runic theory (see THEORIES) is then made the
current theory.  Thus, immediately after the in-arithmetic-theory, a
rule is enabled iff its rule name is a member of the runic
interpretation (see THEORIES) of some member of the value of
term.

Warning:  If term involves macros such as ENABLE and DISABLE you will
probably not get what you expect!  Those macros are defined relative to
the CURRENT-THEORY.  But in this context you might wish they were
defined in terms of the "CURRENT-ARITHMETIC-THEORY" which is not
actually a defined function.  We do not anticipate that users will
repeatedly modify the arithmetic theory.  We expect term most often to
be a constant list of runes and so have not provided "arithmetic theory
manipulation functions" analogous to CURRENT-THEORY and ENABLE.

BECAUSE NO UNIQUE name is associated with an in-arithmetic-theory event,
there is no way we can store the documentation string doc-string in our
il[documentation] data base.  Hence, we actually prohibit doc-string
from having the form of an ACL2 documentation string; see
DOC-STRING.

See NON-LINEAR-ARITHMETIC.

IN-THEORY    designate ``current'' theory (enabling its rules)

     Example:
     (in-theory (set-difference-theories
                  (universal-theory :here)
                  '(flatten (:executable-counterpart flatten))))

     General Form:
     (in-theory term :doc doc-string)

where term is a term that when evaluated will produce a theory (see
THEORIES), and doc-string is an optional documentation string
not beginning with ":doc-section ...".  Except for the variable world,
term must contain no free variables.  Term is evaluated with the
variable world bound to the current world to obtain a theory and the
corresponding runic theory (see THEORIES) is then made the
current theory.  Thus, immediately after the in-theory, a rule is
enabled iff its rule name is a member of the runic interpretation (see
THEORIES) of some member of the value of term.  See
THEORY-FUNCTIONS for a list of the commonly used theory manipulation
functions.

Because no unique name is associated with an in-theory event, there is
no way we can store the documentation string doc-string in our
documentation data base.  Hence, we actually prohibit doc-string from
having the form of an ACL2 documentation string; see DOC-STRING.

Note that it is often useful to surround in-theory events with local,
that is, to use (local (in-theory ...)).  This use of local in
encapsulate events and books will prevent the effect of this theory
change from being exported outside the context of that encapsulate or
book.

Also see HINTS for a discussion of the :in-theory hint,
including some explanation of the important point that an :in-theory
hint will always be evaluated relative to the current ACL2 logical
world, not relative to the theory of a previous goal.