This is documentation for ACL2 Version 3.4
Copyright (C) 2008  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.

QUANTIFIER-TUTORIAL    A Beginner's Guide to Reasoning about Quantification in ACL2

The initial version of this tutorial was written by Sandip Ray.
Additions and revisions are welcome.  Sandip has said:

     "This is a collection of notes that I wrote to remind myself of
     how to reason about quantifiers when I just started.  Most users
     after they have gotten the hang of quantifiers probably will not
     need this and will be able to use their intuitions to guide them
     in the process.  But since many ACL2 users are not used to
     quantification, I am hoping that this set of notes might help them
     to think clearly while reasoning about quantifiers in ACL2."

Many ACL2 papers start with the sentence "ACL2 is a quantifier-free
first-order logic of recursive functions."  It is true that the _syntax_
of ACL2 is quantifier-free; every formula is assumed to be universally
quantified over all free variables in the formula.  But the _logic_ in
fact does afford arbitrary first-order quantification.  This is
obtained in ACL2 using a construct called defun-sk.  See
DEFUN-SK.

Many ACL2 users do not think in terms of quantifiers.  The focus is
almost always on defining recursive functions and reasoning about them
using induction.  That is entirely justified, in fact, since proving
theorems about recursive functions by induction plays to the strengths
of the theorem prover.  Nevertheless there are situations where it is
reasonable and often useful to think in terms of quantifiers.  However,
reasoning about quantifiers requires that you get into the mindset of
thinking about theorems in terms of quantification.  This note is about
how to do this effectively given ACL2's implementation of
quantification.  This does not discuss defun-sk in detail, but merely
shows some examples.  A detailed explanation of the implementation is
in the ACL2 documentation (see DEFUN-SK); also see
CONSERVATIVITY-OF-DEFCHOOSE.

[Note: Quantifiers can be used for some pretty cool things in ACL2.
Perhaps the most interesting example is the way of using quantifiers to
introduce arbitrary tail-recursive equations; see the paper "Partial
Functions in ACL2" by Panagiotis Manolios and J Strother Moore.  This
note does not address applications of quantifiers, but merely how you
would reason about them once you think you want to use them.]

Assume that you have some function P.  I have just left P as a unary
function stub below, since I do not care about what P is.

     (defstub P (*) => *)

Now suppose you want to specify the concept that "there exists some x
such that (P x) holds".  ACL2 allows you to write that directly using
quantifiers.

     (defun-sk exists-P () (exists x (P x)))

If you submit the above form in ACL2 you will see that the theorem
prover specifies two functions exists-p and exists-p-witness, and
exports the following constraints:

     1.  (defun exists-P () (P (exists-P-witness)))
     2.  (defthm exists-P-suff (implies (p x) (exists-p)))

Here exists-P-witness is a new function symbol in the current ACL2
theory.  What do the constraints above say?  Notice the constraint
exists-p-suff.  It says that if you can provide any x such that (P x)
holds, then you know that exists-p holds.  Think of the other
constraint (definition of exists-p) as going the other way.  That is, it
says that if exists-p holds, then there is some x, call it
(exists-p-witness), for which P holds.  Notice that nothing else is
known about exists-p-witness than the two constraints above.

[Note: exists-p-witness above is actually defined in ACL2 using a
special form called defchoose.  See DEFCHOOSE.  This note does
not talk about defchoose.  So far as this note is concerned, think of
exists-p-witness as a new function symbol that has been generated
somehow in ACL2, about which nothing other than the two facts above is
known.]

Similarly, you can talk about the concept that "for all x (P x) holds."
This can be specified in ACL2 by the form:

     (defun-sk forall-P () (forall x (P x)))

This produces the following two constraints:

     1.  (defun forall-P () (P (forall-p-witness)))
     2.  (defthm forall-p-necc (implies (not (P x)) (not (forall-p))))

To understand these, think of for-all-p-witness as producing some x
which does not satisfy P, if such a thing exists.  The constraint
forall-p-necc merely says that if forall-p holds then P is satisfied
for every x.  (To see this more clearly, just think of the
contrapositive of the formula shown.) The other constraint (definition
of forall-p) implies that if forall-p does not hold then there is some
x, call it (forall-p-witness), which does not satisfy P.  To see this,
just consider the following formula which is immediately derivable from
the definition.

     (implies (not (forall-p)) (not (P (forall-witness))))

The description above suggests that to reason about quantifiers, the
following Rules of Thumb, familiar to most any student of logic, are
useful.

     RT1: To prove (exists-p), construct some object A such that P
     holds for A and then use exists-P-suff.

     RT2: If you assume exists-P in your hypothesis, use the definition
     of exists-p to know that P holds for exists-p-witness.  To use this
     to prove a theorem, you must be able to derive the theorem based
     on the hypothesis that P holds for something, whatever the
     something is.

     RT3: To prove forall-P, prove the theorem (P x) (that is, that P
     holds for an arbitrary x), and then simply instantiate the
     definition of forall-p, that is, show that P holds for the witness.

     RT4: If you assume forall-p in the hypothesis of the theorem, see
     how you can prove your conclusion if indeed you were given (P x)
     as a theorem.  Possibly for the conclusion to hold, you needed
     that P holds for some specific set of x values.  Then use the
     theorem forall-p-necc by instantiating it for the specific x
     values you care about.

Perhaps the above is too terse.  In the remainder of the note, we will
consider several examples of how this is done to prove theorems in ACL2
that involve quantified notions.

Let us consider two trivial theorems.  Assume that for some unary
function r, you have proved (r x) as a theorem.  Let us see how you can
prove that (1) there exists some x such that (r x) holds, and (2) for
all x (r x) holds.

We first model these things using defun-sk.  Below, r is simply some
function for which (r x) is a theorem.

     (encapsulate
      (((r *) => *))
      (local (defun r (x) (declare (ignore x)) t))
      (defthm r-holds (r x)))

     (defun-sk exists-r () (exists x (r x)))
     (defun-sk forall-r () (forall x (r x)))

ACL2 does not have too much reasoning support for quantifiers.  So in
most cases, one would need :use hints to reason about quantifiers.  In
order to apply :use hints, it is preferable to keep the function
definitions and theorems disabled.

     (in-theory (disable exists-r exists-r-suff forall-r forall-r-necc))

Let us now prove that there is some x such that (r x) holds.  Since we
want to prove exists-r, we must use exists-r-suff by RT1.  We do not
need to construct any instance here since r holds for all x by the
theorem above.

     (defthm exists-r-holds
       (exists-r)
       :hints (("Goal" :use ((:instance exists-r-suff)))))

Let us now prove the theorem that for all x, (r x) holds.  By RT3, we
must be able to prove it by definition of forall-r.

     (defthm forall-r-holds
       (forall-r)
       :hints (("Goal" :use ((:instance (:definition forall-r))))))

[Note: Probably no ACL2 user in his or her right mind would prove the
theorems exists-r-holds and forall-r-holds above.  The theorems shown
are only for demonstration purposes.]

For the remainder of this note we will assume that we have two stubbed
out unary functions M and N, and we will look at proving some quantified
properties of these functions.

     (defstub M (*) => *)
     (defstub N (*) => *)

Let us now define the predicates all-M, all-N, ex-M, and ex-N
specifying the various quantifications.

     (defun-sk all-M () (forall x (M x)))
     (defun-sk all-N () (forall x (N x)))
     (defun-sk some-M () (exists x (M x)))
     (defun-sk some-N () (exists x (N x)))

     (in-theory (disable all-M all-N all-M-necc all-N-necc))
     (in-theory (disable some-M some-N some-M-suff some-N-suff))

Let us prove the classic distributive properties of quantification: the
distributivity of universal quantification over conjunction, and the
distributivity of existential quantification over disjunction.  We can
state these properties informally in "pseudo ACL2" notation as follows:

     1.  (exists x: (M x)) or (exists x: (N x)) <=> (exists x: (M x) or (N x))
     2.  (forall x: (M x)) and (forall: x (N x)) <=> (forall x: (M x) and (N x))

To make these notions formal we of course need to define the formulas
at the right-hand sides of 1 and 2.  So we define some-MN and all-MN to
capture these concepts.

     (defun-sk some-MN () (exists x (or (M x) (N x))))
     (defun-sk all-MN () (forall x (and (M x) (N x))))

     (in-theory (disable all-MN all-MN-necc some-MN some-MN-suff))

First consider proving property 1.  The formal statement of this
theorem would be: (iff (some-MN) (or (some-M) (some-N))).

How do we prove this theorem?  Looking at RT1-RT4 above, note that they
suggest how one should reason about quantification when one has an
"implication".  But here we have an "equivalence".  This suggests
another rule of thumb.

     RT5: Whenever possible, prove an equivalence involving quantifiers
     by proving two implications.

Let us apply RT5 to prove the theorems above.  So we will first prove:
(implies (some-MN) (or (some-M) (some-N)))

How can we prove this?  This involves assuming a quantified predicate
(some-MN), so we must use RT2 and apply the definition of some-MN.
Since the conclusion involves a disjunction of two quantified
predicates, by RT1 we must be able to construct two objects A and B
such that either M holds for A or N holds for B, so that we can then
invoke some-M-suff and some-N-suff to prove the conclusion.  But now
notice that if some-MN is true, then there is already an object, in fact
some-MN-witness, such that either M holds for it, or N holds for it.
And we know this is the case from the definition of some-MN! So we will
simply prove the theorem instantiating some-M-suff and some-N-suff with
this witness.  The conclusion is that the following event will go
through with ACL2.

     (defthm le1
       (implies (some-MN)
                (or (some-M) (some-N)))
       :rule-classes nil
       :hints (("Goal"
                 :use ((:instance (:definition some-MN))
                       (:instance some-M-suff
                                  (x (some-MN-witness)))
                       (:instance some-N-suff
                                  (x (some-MN-witness)))))))

This also suggests the following rule of thumb:

     RT6: If a conjecture involves assuming an existentially quantified
     predicate in the hypothesis from which you are trying to prove an
     existentially quantified predicate, use the witness of the
     existential quantification in the hypothesis to construct the
     witness for the existential quantification in the conclusion.

Let us now try to prove the converse of le1, that is: (implies (or
(some-M) (some-N)) (some-MN))

Since the hypothesis is a disjunction, we will just prove each case
individually instead of proving the theorem by a :cases hint.  So we
prove the following two lemmas.

     (defthm le2
       (implies (some-M) (some-MN))
       :rule-classes nil
       :hints (("Goal"
                 :use ((:instance (:definition some-M))
                       (:instance some-MN-suff
                                  (x (some-M-witness)))))))

     (defthm le3
       (implies (some-N) (some-MN))
       :rule-classes nil
       :hints (("Goal"
                 :use ((:instance (:definition some-N))
                       (:instance some-MN-suff
                                  (x (some-N-witness)))))))

Note that the hints above are simply applications of RT6 as in le1.
With these lemmas, of course the main theorem is trivial.

     (defthmd |some disjunction|
       (iff (some-MN) (or (some-M) (some-N)))
       :hints (("Goal"
                 :use ((:instance le1)
                       (:instance le2)
                       (:instance le3)))))

Let us now prove the distributivity of universal quantification over
conjunction, that is, the formula: (iff (all-MN) (and (all-M) (all-N)))

Applying RT5, we will again decompose this into two implications.  So
consider first the one-way implication: (implies (and (all-M) (all-N))
(all-MN)).

Here we get to assume all-M and all-N.  Thus by RT4 we can use
all-M-necc and all-N-necc to think as if we are given the formulas (M
x) and (N x) as theorems.  The conclusion here is also a universal
quantification, namely we have to prove all-MN.  Then RT3 tells us to
proceed as follows.  Take any object y.  Try to find an instantiation z
of the hypothesis that implies (and (M y) (N y)).  Then instantiate y
with all-MN-witness.  Note that the hypothesis lets us assume (M x) and
(N x) to be theorems.  Thus to justify we need to instantiate x with y,
and in this case, therefore, with all-MN-witness.  To make the long
story short, the following event goes through with ACL2:

     (defthm lf1
        (implies (and (all-M) (all-N))
                 (all-MN))
         :rule-classes nil
         :hints (("Goal"
                   :use ((:instance (:definition all-MN))
                         (:instance all-M-necc (x (all-MN-witness)))
                         (:instance all-N-necc (x (all-MN-witness)))))))

This suggests the following rule of thumb which is a dual of RT6:

     RT7: If a conjecture assumes some universally quantified predicate
     in the hypothesis and its conclusion asserts a universallly
     quantified predicate, then instantiate the "necessary condition"
     (forall-mn-necc) of the hypothesis with the witness of the
     conclusion to prove the conjecture.

Applying RT7 now we can easily prove the other theorems that we need to
show that universal quantification distributes over conjunction.  Let
us just go through this motion in ACL2.

     (defthm lf2
       (implies (all-MN)
                (all-M))
       :rule-classes nil
       :hints (("Goal"
                 :use ((:instance (:definition all-M))
                       (:instance all-MN-necc
                                  (x (all-M-witness)))))))

     (defthm lf3
       (implies (all-MN)
                (all-N))
       :rule-classes nil
       :hints (("Goal"
                 :use ((:instance (:definition all-N))
                       (:instance all-MN-necc
                                  (x (all-N-witness)))))))

     (defthmd |all conjunction|
       (iff (all-MN)
            (and (all-M) (all-N)))
      :hints (("Goal" :use ((:instance lf1)
                            (:instance lf2)
                            (:instance lf3)))))

The rules of thumb for universal and existential quantification should
make you realize the duality of their use.  Every reasoning method
about universal quantification can be cast as a way of reasoning about
existential quantification, and vice versa.  Whether you reason using
universal and existential quantifiers depends on what is natural in a
particular context.  But just for the sake of completeness let us prove
the duality of universal and existential quantifiers.  So what we want
to prove is the following:

     3.  (forall x (not (M x))) = (not (exists x (M x)))

We first formalize the notion of (forall x (not (M x))) as a
quantification.

     (defun-sk none-M () (forall x (not (M x))))
     (in-theory (disable none-M none-M-necc))

So we now want to prove: (equal (none-M) (not (some-M))).

As before, we should prove this as a pair of implications.  So let us
prove first: (implies (none-M) (not (some-M))).

This may seem to assert an existential quantification in the
conclusion, but rather, it asserts the _negation_ of an existential
quantification.  We are now trying to prove that something does not
exist.  How do we do that?  We can show that nothing satisfies M by
just showing that (some-M-witness) does not satisfy M.  This suggests
the following rule of thumb:

     RT8: When you encounter the negation of an existential
     quantification think in terms of a universal quantification, and
     vice-versa.

Ok, so now applying RT8 and RT3 you should be trying to apply the
definition of some-M.  The hypothesis is just a pure (non-negated)
universal quantification so you should apply RT4.  A blind application
lets us prove the theorem as below.

     (defthm nl1
       (implies (none-M) (not (some-M)))
       :rule-classes nil
       :hints (("Goal"
                 :use ((:instance (:definition some-M))
                       (:instance none-M-necc (x (some-M-witness)))))))

How about the converse implication?  I have deliberately written it as
(implies (not (none-M)) (some-M)) instead of switching the left-hand and
right-hand sides of nl1, which would have been equivalent.  Again, RH8
tells us how to reason about it, in this case using RH2, and we succeed.

     (defthm nl2
       (implies (not (none-M)) (some-M))
       :rule-classes nil
       :hints (("Goal"
                 :use ((:instance (:definition none-M))
                       (:instance some-M-suff (x (none-M-witness)))))))

So finally we just go through the motions of proving the equality.

     (defthmd |forall not = not exists|
       (equal (none-M) (not (some-M)))
       :hints (("Goal"
                 :use ((:instance nl1)
                       (:instance nl2)))))

Let us now see if we can prove a slightly more advanced theorem which
can be stated informally as: If there is a natural number x which
satisfies M, then there is a least natural number y that satisfies M.

[Note: Any time I have had to reason about existential quantification I
have had to do this particular style of reasoning and state that if
there is an object satisfying a predicate, then there is also a
"minimal" object satisfying the predicate.]

Let us formalize this concept.  We first define the concept of
existence of a natural number satisfying x.

     (defun-sk some-nat-M () (exists x (and (natp x) (M x))))
     (in-theory (disable some-nat-M some-nat-M-suff))

We now talk about what it means to say that x is the least number
satisfying M.

     (defun-sk none-below (y)
       (forall r (implies (and (natp r) (< r y)) (not (M r))))))
     (in-theory (disable none-below none-below-necc))

     (defun-sk min-M () (exists y (and (M y) (natp y) (none-below y))))
     (in-theory (disable min-M min-M-suff))

The predicate none-below says that no natural number less than y
satisfies M.  The predicate min-M says that there is some natural
number y satisfying M such that none-below holds for y.

So the formula we want to prove is: (implies (some-nat-M) (min-M)).

Since the formula requires that we prove an existential quantification,
RT1 tells us to construct some object satisfying the predicate over
which we are quantifying.  We should then be able to instantiate
min-M-suff with this object.  That predicate says that the object must
be the least natural number that satisfies M.  Since such an object is
uniquely computable if we know that there exists some natural number
satisfying M, let us just write a recursive function to compute it.
This function is least-M below.

     (defun least-M-aux (i bound)
       (declare (xargs :measure (nfix (- (1+ bound) i))))
       (cond ((or (not (natp i))
                  (not (natp bound))
                  (> i bound))
              0)
            ((M i) i)
            (t (least-M-aux (+ i 1) bound))))

     (defun least-M (bound) (least-M-aux 0 bound))

Let us now reason about this function as one does typically.  So we
prove that this object is indeed the least natural number that
satisfies M, assuming that bound is a natural number that satisfies M.

     (defthm least-aux-produces-an-M
       (implies (and (natp i)
                     (natp bound)
                     (<= i bound)
                     (M bound))
                (M (least-M-aux i bound))))

     (defthm least-<=bound
       (implies (<= 0 bound)
                (<= (least-M-aux i bound) bound)))

     (defthm least-aux-produces-least
       (implies (and (natp i)
                     (natp j)
                     (natp bound)
                     (<= i j)
                     (<= j bound)
                     (M j))
                 (<= (least-M-aux i bound) j)))

     (defthm least-aux-produces-natp
       (natp (least-M-aux i bound)))

     (defthmd least-is-minimal-satisfying-m
       (implies (and (natp bound)
                     (natp i)
                      (< i (least-M bound)))
                (not (M i)))
       :hints (("Goal"
                 :in-theory (disable least-aux-produces-least least-<=bound)
                 :use ((:instance least-<=bound
                                  (i 0))
                       (:instance least-aux-produces-least
                                  (i 0)
                                  (j i))))))

     (defthm least-has-m
       (implies (and (natp bound)
     		  (m bound))
     	     (M (least-M bound))))

     (defthm least-is-natp
       (natp (least-M bound)))

So we have done that, and hopefully this is all that we need about
least-M.  So we disable everything.

     (in-theory (disable least-M natp))

Now of course we note that the statement of the conjecture we are
interested in has two quantifiers, an inner forall (from none-below)
and an outer exists (from min-M).  Since ACL2 is not very good with
quantification, we hold its hands to reason with the quantifier part.
So we will first prove something about the forall and then use it to
prove what we need about the exists.

     RT9: When you face nested quantifiers, reason about each nesting
     separately.

So what do we want to prove about the inner quantifier?  Looking
carefully at the definition of none-below we see that it is saying that
for all natural numbers r < y, (M r) does not hold.  Well, how would we
want to use this fact when we want to prove our final theorem?  We
expect that we will instantiate min-M-suff with the object (least-M
bound) where we know (via the outermost existential quantifier) that M
holds for bound, and we will then want to show that none-below holds for
(least-M bound).  So let us prove that for any natural number (call it
bound), none-below holds for (least-M bound).  For the final theorem we
only need it for natural numbers satisfying M, but note that from the
lemma least-is-minimal-satisfying-m we really do not need that bound
satisfies M.

So we are now proving: (implies (natp bound) (none-below (least-M
bound))).

Well since this is a standard case of proving a universally quantified
predicate, we just apply RT3.  We have proved that for all naturals i <
(least-M bound), i does not satisfy M (lemma
least-is-minimal-satisfying-M), so we merely need the instantiation of
that lemma with none-below-witness of the thing we are trying to prove,
that is, (least-M bound).  The theorem below thus goes through.

     (defthm least-is-minimal
       (implies (natp bound)
                (none-below (least-M bound)))
       :hints (("Goal"
                 :use ((:instance (:definition none-below)
                                  (y (least-M bound)))
                       (:instance least-is-minimal-satisfying-m
                                  (i (none-below-witness (least-M bound))))))))

Finally we are in the outermost existential quantifier, and are in the
process of applying min-M-suff.  What object should we instantiate it
with?  We must instantiate it with (least-M bound) where bound is an
object which must satisfy M and is a natural.  We have such an object,
namely (some-nat-M-witness) which we know have all these qualities given
the hypothesis.  So the proof now is just RT1 and RT2.

     (defthm |minimal exists|
       (implies (some-nat-M) (min-M))
       :hints (("Goal"
                 :use ((:instance min-M-suff
                                  (y (least-M (some-nat-M-witness))))
                       (:instance (:definition some-nat-M))))))

If you are comfortable with the reasoning above, then you are
comfortable with quantifiers and probably will not need these notes any
more.  In my opinion, the best way of dealing with ACL2 is to ask
yourself why you think something is a theorem, and the rules of thumb
above are simply guides to the questions that you need to ask when you
are dealing with quantification.

Here is just a simple exercise for you to test if you understand the
reasoning process.

Exercise:

In the example above we showed that if there exists a natural number x
satisfying M then there is another natural number y such that y
satisfies M and for every natural number z < y, z does not.  What would
happen if we remove the restriction of x, y, and z being naturals?  Of
course, we will not talk about < any more, but suppose you use the
total order on all ACL2 objects (from "books/misc/total-order").  More
concretely, consider the definition of some-M above.  Let us now define
two other functions:

     (include-book "misc/total-order" :dir :system)

     (defun-sk none-below-2 (y)
       (forall r (implies (<< r y) (not (M r)))))

     (defun-sk min-M2 () (exists y (and (M y) (none-below-2 y))))

The question is whether (implies (some-M) (min-M2)) is a theorem.  Can
you prove it?  Can you disprove it?

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, you may prefer 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.

But perhaps first, see DEFUN-SK for an ACL2 utility to
introduce first-order quantification in a direct way.  Examples of the
use of defun-sk are also available: see DEFUN-SK-EXAMPLE and
see TUTORIAL4-DEFUN-SK-EXAMPLE for basic examples, and see
QUANTIFIER-TUTORIAL for a more complete, careful beginner's
introduction that takes you through typical kinds of quantifier-based
reasoning in ACL2.

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

We conclude by an example showing some extra care that may be important
to consider taking.  We start with:

     (defconst |*BaR*| '(3 4))

Then the following works just fine; but try it without the extra code
for the may-need-slashes case and you'll see that the sharp-comma
printing is missing.  First:

     (table evisc-table
            |*BaR*|
            (let ((x (symbol-name '|*BaR*|)))
              (if (may-need-slashes x)
                  (concatenate 'string "#,|" x "|")
                (concatenate 'string "#," x))))

Then:

     ACL2 !>|*BaR*|
     #,|*BaR*|
     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.