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

This manual documents ACL2 Version 3.5.

ACL2-TUTORIAL    tutorial introduction to ACL2

This section contains a tutorial introduction to ACL2, some examples of
the use of ACL2, and pointers to additional information.

You might also find CLI Technical Report 101 helpful for a high-level
view of the design goals of ACL2.

If you are already familiar with Nqthm, see NQTHM-TO-ACL2 for
help in making the transition from Nqthm to ACL2.

If you would like more familiarity with Nqthm, we suggest CLI Technical
Report 100, which works through a non-trivial example.  A short version
of that paper, which is entitled "Interaction with the Boyer-Moore
Theorem Prover:  A Tutorial Study Using the Arithmetic-Geometric Mean
Theorem," is to appear in the Journal of Automated Reasoning's special
issue on induction, probably in 1995 or 1996.  Readers may well find
that this paper indirectly imparts useful information about the
effective use of ACL2.

ACL2-AS-STANDALONE-PROGRAM    Calling ACL2 from another program

ACL2 is intended for interactive use.  It is generally unrealistic to
expect it to prove theorems fully automatically; see THE-METHOD.

Nevertheless, here we describe an approach for how to call the ACL2
theorem prover noninteractively.  These steps can of course be modified
according to your needs.  Here, we illustrate how to call ACL2 from
another Lisp program (or an arbitrary program) to attempt to prove an
arithmetic theorem.

*=== STEP 1: ===*

Build a suitable ACL2 image by starting ACL2 and then executing the
following forms.  In particular, these define a macro, try-thm, that
causes ACL2 to exit with with an exit status indicating success or
failure of a proof attempt.

     (include-book "arithmetic-4/top" :dir :system)
     (defmacro try-thm (&rest args)
       `(mv-let (erp val state)
                (with-prover-time-limit 3 (thm ,@args))
                (declare (ignore val))
                (prog2$ (if erp (exit 1) (exit 0)) state))))
     (reset-prehistory) ; optional
     :q
     (save-exec "arith-acl2" "Included arithmetic-4/top")

If you prefer, above you can replace 3 by some other number of seconds
as a time limit for the prover.  Also, you can replace

     (with-prover-time-limit 3 (thm ,@args))

by

     (with-output :off :all (with-prover-time-limit 3 (thm ,@args)))

if you want to turn off output.  It may be best to leave the output on,
instead eliminating it in the calling program (see Step 3 below).

*=== STEP 2: ===*

Try a little test.  In that same directory try this:

     echo '(try-thm (equal x x))' | ./arith-acl2
     echo $?

The exit status should be 0, indicating success.  Now try this:

     echo '(try-thm (not (equal x x)))' | ./arith-acl2
     echo $?

The exit status should be 1, indicating failure.

*=== STEP 3: ===*

Create a shell script that automates Step 2, for example:

     #!/bin/sh
     (echo "(try-thm $1)" | ./arith-acl2) >& /dev/null
     exit $?

*=== STEP 4: ===*

Try your script from a Lisp program, if you like.  Here is how you can
do it in SBCL, for example.  ( Different Lisps have different ways to
do this, as summarized in function system-call in ACL2 source file
acl2-init.lisp.)

     (defun provable? (x)
       (let ((status
              (process-exit-code
               (sb-ext:run-program "./try-thm.sh" (list (format nil "~s" x))
                                   :output t :search t))))
         (eql status 0)))

Then here is a log:

       * (provable? '(equal x y))

       NIL
       * (provable? '(equal x x))

       T
       *

Certainly refinements are possible - for example the above doesn't
distinguish between unprovable and ill-formed input.  But it's a start.

ACL2-SEDAN    ACL2 Sedan interface

Many successful ACL2 users run in an shell under Emacs; see
EMACS.  However, those not familiar with Emacs may prefer to start
with an Eclipse-based interface developed by Peter Dillinger and Pete
Manolios called the "ACL2 Sedan", or "ACL2s".  As of this writing, the
home page for ACL2s is `http://acl2s.peterd.org/acl2s/doc/'.

EMACS    emacs support for ACL2

Many successful ACL2 users run in an shell under the Emacs editor.  If
you do so, then you may wish to load the distributed file
emacs/emacs-acl2.el.  The file begins with considerable comments
describing what it offers.

If you are not comfortable with Emacs, you may prefer to use an
Eclipse-based interface; see ACL2-SEDAN.

INTRODUCTION    introduction to ACL2

This section contains introductory material on ACL2 including what ACL2
is, how to get started using the system, how to read the output, and
other introductory topics.  It was written almost entirely by Bill
Young of Computational Logic, Inc.

You might also find CLI Technical Report 101 helpful, especially if you
are familiar with Nqthm.  If you would like more familiarity with
Nqthm, we suggest CLI Technical Report 100.

_OVERVIEW_

ACL2 is an automated reasoning system developed (for the first 9 years)
at Computational Logic, Inc. and (from January, 1997) at the University
of Texas at Austin.  It is the successor to the Nqthm (or Boyer-Moore)
logic and proof system and its Pc-Nqthm interactive enhancement.  The
acronym ACL2 actually stands for "A Computational Logic for Applicative
Common Lisp".  This title suggests several distinct but related aspects
of ACL2.

We assume that readers of the ACL2 documentation have at least a very
slight familiarity with some Lisp-like language.  We will address the
issue of prerequisites further, in "ABOUT THIS TUTORIAL" below.

As a *logic*, ACL2 is a formal system with rigorously defined syntax
and semantics.  In mathematical parlance, the ACL2 logic is a
first-order logic of total recursive functions providing mathematical
induction on the ordinals up to epsilon-0 and two extension principles:
one for recursive definition and one for constrained introduction of
new function symbols, here called encapsulation.  The syntax of ACL2 is
that of Common Lisp; ACL2 specifications are "also" Common Lisp
programs in a way that we will make clear later.  In less formal
language, the ACL2 logic is an integrated collection of rules for
defining (or axiomatizing) recursive functions, stating properties of
those functions, and rigorously establishing those properties.  Each of
these activities is mechanically supported.

As a *specification language*, ACL2 supports modeling of systems of
various kinds.  An ACL2 function can equally be used to express purely
formal relationships among mathematical entities, to describe
algorithms, or to capture the intended behavior of digital systems.
For digital systems, an ACL2 specification is a mathematical *model*
that is intended to formalize relevant aspects of system behavior.
Just as physics allows us to model the behavior of continuous physical
systems, ACL2 allows us to model digital systems, including many with
physical realizations such as computer hardware.  As early as the
1930's Church, Kleene, Turing and others established that recursive
functions provide an expressive formalism for modeling digital
computation.  Digital computation should be understood in a broad
sense, covering a wide variety of activities including almost any
systematic or algorithmic activity, or activity that can be reasonably
approximated in that way.  This ranges from the behavior of a digital
circuit to the behavior of a programming language compiler to the
behavior of a controller for a physical system (as long as the system
can be adequately modeled discretely).  All of these have been modeled
using ACL2 or its predecessor Nqthm.

ACL2 is a *computational* logic in at least three distinct senses.
First, the theory of recursive functions is often considered the
mathematics of computation.  Church conjectured that any "effective
computation" can be modeled as a recursive function.  Thus, ACL2
provides an expressive language for modeling digital systems.  Second,
many ACL2 specifications are executable.  In fact, recursive functions
written in ACL2 *are* Common Lisp functions that can be submitted to
any compliant Common Lisp compiler and executed (in an environment
where suitable ACL2-specific macros and functions are defined).  Third,
ACL2 is computational in the sense that calculation is heavily
integrated into the reasoning process.  Thus, an expression with
explicit constant values but no free variables can be simplified by
calculation rather than by complex logical manipulations.

ACL2 is a powerful, automated *theorem prover* or proof checker.  This
means that a competent user can utilize the ACL2 system to discover
proofs of theorems stated in the ACL2 logic or to check previously
discovered proofs.  The basic deductive steps in an ACL2-checked proof
are often quite large, due to the sophisticated combination of decision
procedures, conditional rewriting, mathematical and structural
induction, propositional simplification, and complex heuristics to
orchestrate the interactions of these capabilities.  Unlike some
automated proof systems, ACL2 does not produce a formal proof.
However, we believe that if ACL2 certifies the "theoremhood" of a given
conjecture, then such a formal proof exists and, therefore, the theorem
is valid.  The ultimate result of an ACL2 proof session is a collection
of "events," possibly grouped into "books," that can be replayed in
ACL2.  Therefore, a proof can be independently validated by any ACL2
user.

ACL2 may be used in purely automated mode in the shallow sense that
conjectures are submitted to the prover and the user does not interact
with the proof attempt (except possibly to stop it) until the proof
succeeds or fails.  However, any non-trivial proof attempt is actually
interactive, since successful proof "events" influence the subsequent
behavior of the prover.  For example, proving a lemma may introduce a
rule that subsequently is used automatically by the prover.  Thus, any
realistic proof attempt, even in "automatic" mode, is really an
interactive dialogue with the prover to craft a sequence of events
building an appropriate theory and proof rules leading up to the proof
of the desired result.  Also, ACL2 supports annotating a theorem with
"hints" designed to guide the proof attempt.  By supplying appropriate
hints, the user can suggest proof strategies that the prover would not
discover automatically.  There is a "proof-tree" facility (see
PROOF-TREE) that allows the user to monitor the progress and
structure of a proof attempt in real-time.  Exploring failed proof
attempts is actually where heavy-duty ACL2 users spend most of their
time.

ACL2 can also be used in a more explicitly interactive mode.  The
"proof-checker" subsystem of ACL2 allows exploration of a proof on a
fairly low level including expanding calls of selected function
symbols, invoking specific rewrite rules, and selectively navigating
around the proof.  This facility can be used to gain sufficient insight
into the proof to construct an automatic version, or to generate a
detailed interactive-style proof that can be replayed in batch mode.

Because ACL2 is all of these things -- computational logic,
specification language, programming system, and theorem prover -- it is
more than the sum of its parts.  The careful integration of these
diverse aspects has produced a versatile automated reasoning system
suitable for building highly reliable digital systems.  In the
remainder of this tutorial, we will illustrate some simple uses of this
automated reasoning system.

_ABOUT THIS TUTORIAL_

ACL2 is a complex system with a vast array of features, bells and
whistles.  However, it is possible to perform productive work with the
system using only a small portion of the available functionality.  The
goals of this tutorial are to:

     familiarize the new user with the most basic features of and modes
     of interaction with ACL2;

     familiarize her with the form of output of the system; and

     work through a graduated series of examples.

The more knowledge the user brings to this system, the easier it will
be to become proficient.  On one extreme:  the *ideal* user of ACL2 is
an expert Common Lisp programmer, has deep understanding of automated
reasoning, and is intimately familiar with the earlier Nqthm system.
Such ideal users are unlikely to need this tutorial.  However, without
some background knowledge, the beginning user is likely to become
extremely confused and frustrated by this system.  We suggest that a
new user of ACL2 should:

     (a) have a little familiarity with Lisp, including basic Lisp
     programming and prefix notation (a Lisp reference manual such as
     Guy Steele's "Common Lisp:  The Language" is also helpful);

     (b) be convinced of the utility of formal modeling; and

     (c) be willing to gain familiarity with basic automated theorem
     proving topics such as rewriting and algebraic simplification.

We will not assume any deep familiarity with Nqthm (the so-called
"Boyer-Moore Theorem Prover"), though the book "A Computational Logic
Handbook" by Boyer and Moore (Academic Press, 1988) is an extremely
useful reference for many of the topics required to become a competent
ACL2 user.  We'll refer to it as ACLH below.

As we said in the introduction, ACL2 has various facets.  For example,
it can be used as a Common Lisp programming system to construct
application programs.  In fact, the ACL2 system itself is a large
Common Lisp program constructed almost entirely within ACL2.  Another
use of ACL2 is as a specification and modeling tool.  That is the
aspect we will concentrate on in the remainder of this tutorial.

_GETTING STARTED_

This section is an abridged version of what's available elsewhere; feel
free to see STARTUP for more details.

How you start ACL2 will be system dependent, but you'll probably type
something like "acl2" at your operating system prompt.  Consult your
system administrator for details.

When you start up ACL2, you'll probably find yourself inside the ACL2
command loop, as indicated by the following prompt.

       ACL2 !>

If not, you should type (LP).  See LP, which has a lot more
information about the ACL2 command loop.

There are two "modes" for using ACL2, :logic and :program.  When you
begin ACL2, you will ordinarily be in the :logic mode.  This means that
any new function defined is not only executable but also is
axiomatically defined in the ACL2 logic.  (See DEFUN-MODE and
see DEFAULT-DEFUN-MODE.)  Roughly speaking, :program mode is
available for using ACL2 as a programming language without some of the
logical burdens necessary for formal reasoning.  In this tutorial we
will assume that we always remain in :logic mode and that our purpose is
to write formal models of digital systems and to reason about them.

Now, within the ACL2 command loop you can carry out various kinds of
activities, including the folllowing.  (We'll see examples later of
many of these.)

     define new functions (see DEFUN);

     execute functions on concrete data;

     pose and attempt to prove conjectures about previously defined
     functions (see DEFTHM);

     query the ACL2 "world" or database (e.g., see PE); and

     numerous other things.

In addition, there is extensive on-line documentation, of which this
tutorial introduction is a part.

_INTERACTING WITH ACL2_

The standard means of interacting with ACL2 is to submit a sequence of
forms for processing by the ACL2 system.  These forms are checked for
syntactic and semantic acceptability and appropriately processed by the
system.  These forms can be typed directly at the ACL2 prompt.
However, most successful ACL2 users prefer to do their work using the
Emacs text editor, maintaining an Emacs "working" buffer in which forms
are edited.  Those forms are then copied to the ACL2 interaction
buffer, which is often the "*shell*" buffer.

In some cases, processing succeeds and makes some change to the ACL2
"logical world," which affects the processing of subsequent forms.  How
can this processing fail?  For example, a proposed theorem will be
rejected unless all function symbols mentioned have been previously
defined.  Also the ability of ACL2 to discover the proof of a theorem
may depend on the user previously having proved other theorems.  Thus,
the order in which forms are submitted to ACL2 is quite important.
Maintaining forms in an appropriate order in your working buffer will
be helpful for re-playing the proof later.

One of the most common events in constructing a model is introducing
new functions.  New functions are usually introduced using the defun
form; we'll encounter some exceptions later.  Proposed function
definitions are checked to make sure that they are syntactically and
semantically acceptable (e.g., that all mentioned functions have been
previously defined) and, for recursive functions, that their recursive
calls *terminate*.  A recursive function definition is guaranteed to
terminate if there is some some "measure" of the arguments and a
"well-founded" ordering such that the arguments to the function get
smaller in each recursive call.  See WELL-FOUNDED-RELATION.

For example, suppose that we need a function that will append two lists
together.  (We already have one in the ACL2 append function; but
suppose perversely that we decide to define our own.)  Suppose we
submit the following definition (you should do so as well and study the
system output):

       (defun my-app (x y)
         (if (atom x)
             y
           (cons (car x) (my-app x y))))

The system responds with the following message:

       ACL2 Error in ( DEFUN MY-APP ...):  No :MEASURE was supplied with
       the definition of MY-APP.  Our heuristics for guessing one have not
       made any suggestions.  No argument of the function is tested along
       every branch and occurs as a proper subterm at the same argument
       position in every recursive call.  You must specify a :MEASURE.  See
       :DOC defun.

This means that the system could not find an expression involving the
formal parameters x and y that decreases under some well-founded order
in every recursive call (there is only one such call).  It should be
clear that there is no such measure in this case because the only
recursive call doesn't change the arguments at all.  The definition is
obviously flawed; if it were accepted and executed it would loop
forever.  Notice that a definition that is rejected is not stored in
the system database; there is no need to take any action to have it
"thrown away."  Let's try again with the correct definition.  The
interaction now looks like (we're also putting in the ACL2 prompt; you
don't type that):

       ACL2 !>(defun my-app (x y)
                (if (atom x)
                    y
                  (cons (car x) (my-app (cdr x) y))))

       The admission of MY-APP is trivial, using the relation O<
       (which is known to be well-founded on the domain recognized by
       O-P) and the measure (ACL2-COUNT X).  We observe that the
       type of MY-APP is described by the theorem
       (OR (CONSP (MY-APP X Y)) (EQUAL (MY-APP X Y) Y)).
       We used primitive type reasoning.

       Summary
       Form:  ( DEFUN MY-APP ...)
       Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL))
       Warnings:  None
       Time:  0.07 seconds (prove: 0.00, print: 0.00, other: 0.07)
       MY-APP

Notice that this time the function definition was accepted.  We didn't
have to supply a measure explicitly; the system inferred one from the
form of the definition.  On complex functions it may be necessary to
supply a measure explicitly.  (See XARGS.)

The system output provides several pieces of information.

     The revised definition is acceptable.  The system realized that
     there is a particular measure (namely, (acl2-count x)) and a
     well-founded relation (o<) under which the arguments of my-app get
     smaller in recursion.  Actually, the theorem prover proved several
     theorems to admit my-app.  The main one was that when (atom x) is
     false the acl2-count of (cdr x) is less than (in the o< sense) the
     acl2-count of x.  Acl2-count is the most commonly used measure of
     the "size" of an ACL2 object.  o< is the ordering relation on
     ordinals less than epsilon-0.  On the natural numbers it is just
     ordinary "<".

     The observation printed about "the type of MY-APP" means that
     calls of the function my-app will always return a value that is
     either a cons pair or is equal to the second parameter.

     The summary provides information about which previously introduced
     definitions and lemmas were used in this proof, about some notable
     things to watch out for (the Warnings), and about how long this
     event took to process.

Usually, it's not important to read this information.  However, it is a
good habit to scan it briefly to see if the type information is
surprising to you or if there are Warnings.  We'll see an example of
them later.

After a function is accepted, it is stored in the database and
available for use in other function definitions or lemmas.  To see the
definition of any function use the :pe command (see PE).  For
example,

       ACL2 !>:pe my-app
        L       73:x(DEFUN MY-APP (X Y)
                           (IF (ATOM X)
                               Y (CONS (CAR X) (MY-APP (CDR X) Y))))

This displays the definition along with some other relevant
information.  In this case, we know that this definition was processed
in :logic mode (the "L") and was the 73rd command processed in the
current session.

We can also try out our newly defined function on some sample data.  To
do that, just submit a form to be evaluated to ACL2.  For example,

       ACL2 !>(my-app '(0 1 2) '(3 4 5))
       (0 1 2 3 4 5)
       ACL2 !>(my-app nil nil)
       NIL
       ACL2 !>

Now suppose we want to prove something about the function just
introduced.  We conjecture, for example, that the length of the append
of two lists is the sum of their lengths.  We can formulate this
conjecture in the form of the following ACL2 defthm form.

       (defthm my-app-length
         (equal (len (my-app x y))
                (+ (len x) (len y))))

First of all, how did we know about the functions len and +, etc.?  The
answer to that is somewhat unsatisfying -- we know them from our past
experience in using Common Lisp and ACL2.  It's hard to know that a
function such as len exists without first knowing some Common Lisp.  If
we'd guessed that the appropriate function was called length (say, from
our knowledge of Lisp) and tried :pe length, we would have seen that
length is defined in terms of len, and we could have explored from
there.  Luckily, you can write a lot of ACL2 functions without knowing
too many of the primitive functions.

Secondly, why don't we need some "type" hypotheses?  Does it make sense
to append things that are not lists?  Well, yes.  ACL2 and Lisp are
both quite weakly typed.  For example, inspection of the definition of
my-app shows that if x is not a cons pair, then (my-app x y) always
returns y, no matter what y is.

Thirdly, would it matter if we rewrote the lemma with the equality
reversed, as follows?

       (defthm my-app-length2
         (equal (+ (len x) (len y))
                (len (my-app x y)))).

The two are *logically* equivalent, but...yes, it would make a big
difference.  Recall our remark that a lemma is not only a "fact" to be
proved; it also is used by the system to prove other later lemmas.  The
current lemma would be stored as a rewrite rule.  (See
RULE-CLASSES.)  For a rewrite rule, a conclusion of the form (EQUAL
LHS RHS) means to replace instances of the LHS by the appropriate
instance of the RHS.  Presumably, it's better to rewrite (len (my-app x
y)) to (+ (len x) (len y)) than the other way around.  The reason is
that the system "knows" more about + than it does about the new
function symbol my-app.

So let's see if we can prove this lemma.  Submitting our preferred
defthm to ACL2 (do it!), we get the following interaction:

               --------------------------------------------------
     ACL2 !>(defthm my-app-length
       (equal (len (my-app x y))
              (+ (len x) (len y))))

     Name the formula above *1.

     Perhaps we can prove *1 by induction.  Three induction schemes are
     suggested by this conjecture.  These merge into two derived
     induction schemes.  However, one of these is flawed and so we are
     left with one viable candidate.

     We will induct according to a scheme suggested by (LEN X), but
     modified to accommodate (MY-APP X Y).  If we let (:P X Y) denote *1
     above then the induction scheme we'll use is
     (AND (IMPLIES (NOT (CONSP X)) (:P X Y))
          (IMPLIES (AND (CONSP X) (:P (CDR X) Y))
                   (:P X Y))).
     This induction is justified by the same argument used to admit LEN,
     namely, the measure (ACL2-COUNT X) is decreasing according to the
     relation O< (which is known to be well-founded on the domain
     recognized by O-P).  When applied to the goal at hand the
     above induction scheme produces the following two nontautological
     subgoals.

     Subgoal *1/2
     (IMPLIES (NOT (CONSP X))
              (EQUAL (LEN (MY-APP X Y))
                     (+ (LEN X) (LEN Y)))).

     But simplification reduces this to T, using the :definitions of FIX,
     LEN and MY-APP, the :type-prescription rule LEN, the :rewrite rule
     UNICITY-OF-0 and primitive type reasoning.

     Subgoal *1/1
     (IMPLIES (AND (CONSP X)
                   (EQUAL (LEN (MY-APP (CDR X) Y))
                          (+ (LEN (CDR X)) (LEN Y))))
              (EQUAL (LEN (MY-APP X Y))
                     (+ (LEN X) (LEN Y)))).

     This simplifies, using the :definitions of LEN and MY-APP, primitive
     type reasoning and the :rewrite rules COMMUTATIVITY-OF-+ and
     CDR-CONS, to

     Subgoal *1/1'
     (IMPLIES (AND (CONSP X)
                   (EQUAL (LEN (MY-APP (CDR X) Y))
                          (+ (LEN Y) (LEN (CDR X)))))
              (EQUAL (+ 1 (LEN (MY-APP (CDR X) Y)))
                     (+ (LEN Y) 1 (LEN (CDR X))))).

     But simplification reduces this to T, using linear arithmetic,
     primitive type reasoning and the :type-prescription rule LEN.

     That completes the proof of *1.

     Q.E.D.

     Summary
     Form:  ( DEFTHM MY-APP-LENGTH ...)
     Rules: ((:REWRITE UNICITY-OF-0)
             (:DEFINITION FIX)
             (:REWRITE COMMUTATIVITY-OF-+)
             (:DEFINITION LEN)
             (:REWRITE CDR-CONS)
             (:DEFINITION MY-APP)
             (:TYPE-PRESCRIPTION LEN)
             (:FAKE-RUNE-FOR-TYPE-SET NIL)
             (:FAKE-RUNE-FOR-LINEAR NIL))
     Warnings:  None
     Time:  0.30 seconds (prove: 0.13, print: 0.05, other: 0.12)
      MY-APP-LENGTH
               --------------------------------------------------

Wow, it worked!  In brief, the system first tried to rewrite and
simplify as much as possible.  Nothing changed; we know that because it
said "Name the formula above *1."  Whenever the system decides to name
a formula in this way, we know that it has run out of techniques to use
other than proof by induction.

The induction performed by ACL2 is structural or "Noetherian"
induction.  You don't need to know much about that except that it is
induction based on the structure of some object.  The heuristics infer
the structure of the object from the way the object is recursively
decomposed by the functions used in the conjecture.  The heuristics of
ACL2 are reasonably good at selecting an induction scheme in simple
cases.  It is possible to override the heuristic choice by providing an
:induction hint (see HINTS).  In the case of the theorem above,
the system inducts on the structure of x as suggested by the
decomposition of x in both (my-app x y) and (len x).  In the base case,
we assume that x is not a consp.  In the inductive case, we assume that
it is a consp and assume that the conjecture holds for (cdr x).

There is a close connection between the analysis that goes on when a
function like my-app is accepted and when we try to prove something
inductively about it.  That connection is spelled out well in Boyer and
Moore's book "A Computational Logic," if you'd like to look it up.  But
it's pretty intuitive.  We accepted my-app because the "size" of the
first argument x decreases in the recursive call.  That tells us that
when we need to prove something inductively about my-app, it's a good
idea to try an induction on the size of the first argument.  Of course,
when you have a theorem involving several functions, it may be
necessary to concoct a more complicated induction schema, taking
several of them into account.  That's what's meant by "merging" the
induction schemas.

The proof involves two cases: the base case, and the inductive case.
You'll notice that the subgoal numbers go *down* rather than up, so you
always know how many subgoals are left to process.  The base case
(Subgoal *1/2) is handled by opening up the function definitions,
simplifying, doing a little rewriting, and performing some reasoning
based on the types of the arguments.  You'll often encounter references
to system defined lemmas (like unicity-of-0).  You can always look at
those with :pe; but, in general, assume that there's a lot of
simplification power under the hood that's not too important to
understand fully.

The inductive case (Subgoal *1/1) is also dispatched pretty easily.
Here we assume the conjecture true for the cdr of the list and try to
prove it for the entire list.  Notice that the prover does some
simplification and then prints out an updated version of the goal
(Subgoal *1/1').  Examining these gives you a pretty good idea of
what's going on in the proof.

Sometimes one goal is split into a number of subgoals, as happened with
the induction above.  Sometimes after some initial processing the
prover decides it needs to prove a subgoal by induction; this subgoal
is given a name and pushed onto a stack of goals.  Some steps, like
generalization (see ACLH), are not necessarily validity preserving;
that is, the system may adopt a false subgoal while trying to prove a
true one.  (Note that this is ok in the sense that it is not "unsound."
The system will fail in its attempt to establish the false subgoal and
the main proof attempt will fail.)  As you gain facility with using the
prover, you'll get pretty good at recognizing what to look for when
reading a proof script.  The prover's proof-tree utility helps with
monitoring an ongoing proof and jumping to designated locations in the
proof (see PROOF-TREE).  See TIPS for a number of useful
pointers on using the theorem prover effectively.

When the prover has successfully proved all subgoals, the proof is
finished.  As with a defun, a summary of the proof is printed.  This
was an extremely simple proof, needing no additional guidance.  More
realistic examples typically require the user to look carefully at the
failed proof log to find ways to influence the prover to do better on
its next attempt.  This means either:  proving some rules that will
then be available to the prover, changing the global state in ways that
will affect the proof, or providing some hints locally that will
influence the prover's behavior.  Proving this lemma (my-app-length) is
an example of the first.  Since this is a rewrite rule, whenever in a
later proof an instance of the form (LEN (MY-APP X Y)) is encountered,
it will be rewritten to the corresponding instance of (+ (LEN X) (LEN
Y)).  Disabling the rule by executing the command

       (in-theory (disable my-app-length)),

is an example of a global change to the behavior of the prover since
this rewrite will not be performed subsequently (unless the rule is
again enabled).  Finally, we can add a (local) disable "hint" to a
defthm, meaning to disable the lemma only in the proof of one or more
subgoals.  For example:

       (defthm my-app-length-commutativity
         (equal (len (my-app x y))
                (len (my-app y x)))
         :hints (("Goal" :in-theory (disable my-app-length))))

In this case, the hint supplied is a bad idea since the proof is much
harder with the hint than without it.  Try it both ways.

By the way, to undo the previous event use :u (see U).  To undo
back to some earlier event use :ubt (see UBT).  To view the
current event use :pe :here.  To list several events use :pbt (see
PBT).

Notice the form of the hint in the previous example (see
HINTS).  It specifies a goal to which the hint applies.  "Goal"
refers to the top-level goal of the theorem.  Subgoals are given unique
names as they are generated.  It may be useful to suggest that a
function symbol be disabled only for Subgoal 1.3.9, say, and a
different function enabled only on Subgoal 5.2.8.  Overuse of such
hints often suggests a poor global proof strategy.

We now recommend that you visit documentation on additional examples.
See TUTORIAL-EXAMPLES.

STARTUP    How to start using ACL2; the ACL2 command loop

When you start up ACL2, you'll probably find yourself inside the ACL2
command loop, as indicated by the following prompt.

       ACL2 !>

If not, you should type (LP).  See LP, which has a lot more
information about the ACL2 command loop.

You should now be in ACL2.  The current "default-defun-mode" is :logic;
the other mode is :program, which would cause the letter p to be
printed in the prompt.  :Logic means that any function we define is not
only executable but also is axiomatically defined in the ACL2 logic.
See DEFUN-MODE and see DEFAULT-DEFUN-MODE.  For example
we can define a function my-cons as follows.  (You may find it useful
to start up ACL2 and submit this and other commands below to the ACL2
command loop, as we won't include output below.)

       ACL2 !>(defun my-cons (x y) (cons x y))

An easy theorem may then be proved:  the car of (my-cons a b) is A.

       ACL2 !>(defthm car-my-cons (equal (car (my-cons a b)) a))

You can place raw Lisp forms to evaluate at start-up into file
acl2-init.lsp in your home directory, except on Windows systems.  For
example, if you put the following into acl2-init.lsp, then ACL2 will
print "HI" when it starts up.

     (print "HI")

But be careful; all bets are off when you submit forms to raw Lisp, so
this capability should only be used when you are hacking or when you
are setting some Lisp parameters (e.g., (setq si::*notify-gbc* nil) to
turn off garbage collection notices in GCL).

Notice that unlike Nqthm, the theorem command is defthm rather than
prove-lemma.  See DEFTHM, which explains (among other things)
that the default is to turn theorems into rewrite rules.

Various keyword commands are available to query the ACL2 "world", or
database.  For example, we may view the definition of my-cons by
invoking a command to print events, as follows.

       ACL2 !>:pe my-cons

Also see PE.  We may also view all the lemmas that rewrite
terms whose top function symbol is car by using the following command,
whose output will refer to the lemma car-my-cons proved above.

       ACL2 !>:pl car

Also see PL.  Finally, we may print all the commands back
through the initial world as follows.

       ACL2 !>:pbt 0

See HISTORY for a list of commands, including these, for
viewing the current ACL2 world.

Continue with the documentation for tutorial-examples to see a simple
but illustrative example in the use of ACL2 for reasoning about
functions.

TIDBITS    some basic hints for using ACL2

See BOOKS for a discussion of books.  Briefly, a book is a file
whose name ends in ".lisp" that contains ACL2 events; see
EVENTS.

See HISTORY for a list of useful commands.  Some examples:

       :pbt :here      ; print the current event
       :pbt (:here -3) ; print the last four events
       :u              ; undo the last event
       :pe append      ; print the definition of append

See DOCUMENTATION to learn how to print documentation to the
terminal.  There are also versions of the documentation for Mosaic,
Emacs Info, and hardcopy.

There are quite a few kinds of rules allowed in ACL2 besides :rewrite
rules, though we hope that beginners won't usually need to be aware of
them.  See RULE-CLASSES for details.  In particular, there is
support for congruence rewriting.  See RUNE ("RUle NamE") for a
description of the various kinds of rules in the system.  Also see
THEORIES for a description of how to build theories of runes,
which are often used in hints; see HINTS.

A "programming mode" is supported; see PROGRAM, see
DEFUN-MODE, and see DEFAULT-DEFUN-MODE.  It can be useful to
prototype functions after executing the command :program, which will
cause definitions to be syntaxed-checked only.

ACL2 supports mutual recursion, though this feature is not tied into
the automatic discovery of induction schemas and is often not the best
way to proceed when you expect to be reasoning about the functions.
See DEFUNS; also see MUTUAL-RECURSION.

See LD for discussion of how to load files of events.  There
are many options to ld, including ones to suppress proofs and to
control output.

The :otf-flg (Onward Thru the Fog FLaG) is a useful feature that Nqthm
users have often wished for.  It prevents the prover from aborting a
proof attempt and inducting on the original conjecture.  See
OTF-FLG.

ACL2 supports redefinition and redundancy in events; see
LD-REDEFINITION-ACTION and see REDUNDANT-EVENTS.

A proof-tree display feature is available for use with Emacs.  This
feature provides a view of ACL2 proofs that can be much more useful
than reading the stream of characters output by the theorem prover as
its "proof."  See PROOF-TREE.

An interactive feature similar to Pc-Nqthm is supported in ACL2.  See
VERIFY and see PROOF-CHECKER.

ACL2 allows you to monitor the use of rewrite rules.  See
BREAK-REWRITE.

See ARRAYS to read about applicative, fast arrays in ACL2.

To quit the ACL2 command loop, or (in akcl) to return to the ACL2
command loop after an interrupt, type :q.  To continue (resume) after
an interrupt (in akcl), type :r.  To cause an interrupt (in akcl under
Unix (trademark of AT&T)), hit control-C (twice, if inside Emacs).  To
exit ACL2 altogether, first type :q to exit the ACL2 command loop, and
then exit Lisp (by typing (user::bye) in akcl).

See STATE to read about the von Neumannesque ACL2 state object
that records the "current state" of the ACL2 session.  Also see
@, and see ASSIGN, to learn about reading and setting
global state variables.

If you want your own von Neumannesque object, e.g., a structure that
can be "destructively modified" but which must be used with some
syntactic restrictions, see STOBJ.

TIPS    some hints for using the ACL2 prover

We present here some tips for using ACL2 effectively.  Though this
collection is somewhat _ad hoc_, we try to provide some organization,
albeit somewhat artificial:  for example, the sections overlap, and no
particular order is intended.  This material has been adapted by Bill
Young from a very similar list for Nqthm that appeared in the
conclusion of:  "Interaction with the Boyer-Moore Theorem Prover: A
Tutorial Study Using the Arithmetic-Geometric Mean Theorem," by Matt
Kaufmann and Paolo Pecchiari, CLI Technical Report 100, June, 1995.  We
also draw from a similar list in Chapter 13 of "A Computational Logic
Handbook" by R.S. Boyer and J S. Moore (Academic Press, 1988).  We'll
refer to this as "ACLH" below.

These tips are organized roughly as follows.

     A. ACL2 Basics

     B. Strategies for creating events

     C. Dealing with failed proofs

     D. Performance tips

     E. Miscellaneous tips and knowledge

     F. Some things you DON'T need to know

_ACL2 BASICS_

*A1. The ACL2 logic.*
This is a logic of total functions.  For example, if A and B are less
than or equal to each other, then we need to know something more in
order to conclude that they are equal (e.g., that they are numbers).
This kind of twist is important in writing definitions; for example, if
you expect a function to return a number, you may want to apply the
function fix or some variant (e.g., nfix or ifix) in case one of the
formals is to be returned as the value.

ACL2's notion of ordinals is important on occasion in supplying
"measure hints" for the acceptance of recursive definitions.  Be sure
that your measure is really an ordinal.  Consider the following
example, which ACL2 fails to admit (as explained below).

       (defun cnt (name a i x)
         (declare (xargs :measure (+ 1 i)))
         (cond ((zp (+ 1 i))
                0)
               ((equal x (aref1 name a i))
                (1+ (cnt name a (1- i) x)))
               (t (cnt name a (1- i) x))))

One might think that (+ 1 i) is a reasonable measure, since we know
that (+ 1 i) is a positive integer in any recursive call of cnt, and
positive integers are ACL2 ordinals (see O-P).  However, the
ACL2 logic requires that the measure be an ordinal unconditionally, not
just under the governing assumptions that lead to recursive calls.  An
appropriate fix is to apply nfix to (+ 1 i), i.e., to use

       (declare (xargs :measure (nfix (+ 1 i))))

in order to guarantee that the measure will always be an ordinal (in
fact, a positive integer).

For more about admissibility of recursive definitions, see
DEFUN, in particular the discussion of termination.

*A2. Simplification.*
The ACL2 simplifier is basically a rewriter, with some "linear
arithmetic" thrown in.  One needs to understand the notion of
conditional rewriting.  See REWRITE.

*A3. Parsing of rewrite rules.*
ACL2 parses rewrite rules roughly as explained in ACLH, _except_ that
it never creates "unusual" rule classes.  In ACL2, if you want a
:linear rule, for example, you must specify :linear in the
:rule-classes.  See RULE-CLASSES, and also see REWRITE
and see LINEAR.

*A4. Linear arithmetic.*
On this subject, it should suffice to know that the prover can handle
truths about + and -, and that linear rules (see above) are somehow
"thrown in the pot" when the prover is doing such reasoning.  Perhaps
it's also useful to know that linear rules can have hypotheses, and
that conditional rewriting is used to relieve those hypotheses.

*A5. Events.*
Over time, the expert ACL2 user will know some subtleties of its
events.  For example, in-theory events and hints are important, and
they distinguish between a function and its executable counterpart.

_B. STRATEGIES FOR CREATING EVENTS_

In this section, we concentrate on the use of definitions and rewrite
rules.  There are quite a few kinds of rules allowed in ACL2 besides
rewrite rules, though most beginning users probably won't usually need
to be aware of them.  See RULE-CLASSES for details.  In
particular, there is support for congruence rewriting.  Also see
RUNE ("RUle NamE") for a description of the various kinds of rules in
the system.

*B1. Use high-level strategy.*
Decompose theorems into "manageable" lemmas (admittedly, experience
helps here) that yield the main result "easily."  It's important to be
able to outline non-trivial proofs by hand (or in your head).  In
particular, avoid submitting goals to the prover when there's no reason
to believe that the goal will be proved and there's no "sense" of how
an induction argument would apply.  It is often a good idea to avoid
induction in complicated theorems unless you have a reason to believe
that it is appropriate.

*B2. Write elegant definitions.*
Try to write definitions in a reasonably modular style, especially
recursive ones.  Think of ACL2 as a programming language whose
procedures are definitions and lemmas, hence we are really suggesting
that one follow good programming style (in order to avoid duplication
of "code," for example).

When possible, complex functions are best written as compositions of
simpler functions.  The theorem prover generally performs better on
primitive recursive functions than on more complicated recursions (such
as those using accumulating parameters).

Avoid large non-recursive definitions which tend to lead to large case
explosions.  If such definitions are necessary, try to prove all
relevant facts about the definitions and then disable them.

Whenever possible, avoid mutual recursion if you care to prove anything
about your functions.  The induction heuristics provide essentially no
help with reasoning about mutually defined functions.  Mutually
recursive functions can usually be combined into a single function with
a "flag" argument.  (However, see
MUTUAL-RECURSION-PROOF-EXAMPLE for a small example of proof involving
mutually recursive functions.)

*B3. Look for analogies.*
Sometimes you can easily edit sequences of lemmas into sequences of
lemmas about analogous functions.

*B4. Write useful rewrite rules.*
As explained in A3 above, every rewrite rule is a directive to the
theorem prover, usually to replace one term by another.  The directive
generated is determined by the syntax of the defthm submitted.  Never
submit a rewrite rule unless you have considered its interpretation as
a proof directive.

*B4a.  Rewrite rules should simplify.*
Try to write rewrite rules whose right-hand sides are in some sense
"simpler than" (or at worst, are variants of) the left-hand sides.
This will help to avoid infinite loops in the rewriter.

*B4b.  Avoid needlessly expensive rules.*
Consider a rule whose conclusion's left-hand side (or, the entire
conclusion) is a term such as (consp x) that matches many terms
encountered by the prover.  If in addition the rule has complicated
hypotheses, this rule could slow down the prover greatly.  Consider
switching the conclusion and a complicated hypothesis (negating each)
in that case.

*B4c. The "Knuth-Bendix problem".*
Be aware that left sides of rewrite rules should match the "normalized
forms", where "normalization" (rewriting) is inside out.  Be sure to
avoid the use of nonrecursive function symbols on left sides of rewrite
rules, except when those function symbols are disabled, because they
tend to be expanded away before the rewriter would encounter an
instance of the left side of the rule.  Also assure that subexpressions
on the left hand side of a rule are in simplified form.

*B4d. Avoid proving useless rules.*
Sometimes it's tempting to prove a rewrite rule even before you see how
it might find application.  If the rule seems clean and important, and
not unduly expensive, that's probably fine, especially if it's not too
hard to prove.  But unless it's either part of the high-level strategy
or, on the other hand, intended to get the prover past a particular
unproved goal, it may simply waste your time to prove the rule, and
then clutter the database of rules if you are successful.

*B4e. State rules as strongly as possible, usually.*
It's usually a good idea to state a rule in the strongest way possible,
both by eliminating unnecessary hypotheses and by generalizing
subexpressions to variables.

Advanced users may choose to violate this policy on occasion, for
example in order to avoid slowing down the prover by excessive
attempted application of the rule.  However, it's a good rule of thumb
to make the strongest rule possible, not only because it will then
apply more often, but also because the rule will often be easier to
prove (see also B6 below).  New users are sometimes tempted to put in
extra hypotheses that have a "type restriction" appearance, without
realizing that the way ACL2 handles (total) functions generally lets it
handle trivial cases easily.

*B4f. Avoid circularity.*
A stack overflow in a proof attempt almost always results from circular
rewriting.  Use brr to investigate the stack; see BREAK-LEMMA.
Because of the complex heuristics, it is not always easy to define just
when a rewrite will cause circularity.  See the very good discussion of
this topic in ACLH.

See BREAK-LEMMA for a trick involving use of the forms brr t
and (cw-gstack) for inspecting loops in the rewriter.

*B4g. Remember restrictions on permutative rules.*
Any rule that permutes the variables in its left hand side could cause
circularity.  For example, the following axiom is automatically
supplied by the system:

       (defaxiom commutativity-of-+
                 (equal (+ x y) (+ y x))).

This would obviously lead to dangerous circular rewriting if such
"permutative" rules were not governed by a further restriction.  The
restriction is that such rules will not produce a term that is
"lexicographically larger than" the original term (see
LOOP-STOPPER).  However, this sometimes prevents intended rewrites.
See Chapter 13 of ACLH for a discussion of this problem.

*B5. Conditional vs. unconditional rewrite rules.*
It's generally preferable to form unconditional rewrite rules unless
there is a danger of case explosion.  That is, rather than pairs of
rules such as

     (implies p
              (equal term1 term2))

and

     (implies (not p)
              (equal term1 term3))

consider:

     (equal term1
            (if p term2 term3))

However, sometimes this strategy can lead to case explosions: IF terms
introduce cases in ACL2.  Use your judgment.  (On the subject of IF:
COND, CASE, AND, and OR are macros that abbreviate IF forms, and
propositional functions such as IMPLIES quickly expand into IF terms.)

*B6. Create elegant theorems.*
Try to formulate lemmas that are as simple and general as possible.
For example, sometimes properties about several functions can be
"factored" into lemmas about one function at a time.  Sometimes the
elimination of unnecessary hypotheses makes the theorem easier to
prove, as does generalizing first by hand.

*B7. Use* defaxioms *temporarily to explore possibilities.*
When there is a difficult goal that seems to follow immediately (by a
:use hint or by rewriting) from some other lemmas, you can create those
lemmas as defaxiom events (or, the application of skip-proofs to defthm
events) and then double-check that the difficult goal really does
follow from them.  Then you can go back and try to turn each defaxiom
into a defthm.  When you do that, it's often useful to disable any
additional rewrite rules that you prove in the process, so that the
"difficult goal" will still be proved from its lemmas when the process
is complete.

Better yet, rather than disabling rewrite rules, use the local
mechanism offered by encapsulate to make temporary rules completely
local to the problem at hand.  See ENCAPSULATE and see
LOCAL.

*B9. Use books.*
Consider using previously certified books, especially for arithmetic
reasoning.  This cuts down the duplication of effort and starts your
specification and proof effort from a richer foundation.  See the file
"doc/README" in the ACL2 distribution for information on books that
come with the system.

_C. DEALING WITH FAILED PROOFS_

*C1. Look in proof output for goals that can't be further simplified.*
Use the "proof-tree" utility to explore the proof space.  However, you
don't need to use that tool to use the "checkpoint" strategy.  The idea
is to think of ACL2 as a "simplifier" that either proves the theorem or
generates some goal to consider.  That goal is the first "checkpoint,"
i.e., the first goal that does not further simplify.  Exception:  it's
also important to look at the induction scheme in a proof by induction,
and if induction seems appropriate, then look at the first checkpoint
_after_ the induction has begun.

Consider whether the goal on which you focus is even a theorem.
Sometimes you can execute it for particular values to find a
counterexample.

When looking at checkpoints, remember that you are looking for any
reason at all to believe the goal is a theorem.  So for example,
sometimes there may be a contradiction in the hypotheses.

Don't be afraid to skip the first checkpoint if it doesn't seem very
helpful.  Also, be willing to look a few lines up or down from the
checkpoint if you are stuck, bearing in mind however that this practice
can be more distracting than helpful.

*C2. Use the "break rewrite" facility.*
Brr and related utilities let you inspect the "rewrite stack."  These
can be valuable tools in large proof efforts.  See BREAK-LEMMA
for an introduction to these tools, and see BREAK-REWRITE for
more complete information.

The break facility is especially helpful in showing you why a
particular rewrite rule is not being applied.

*C3. Use induction hints when necessary.* Of course, if you can define
your functions so that they suggest the correct inductions to ACL2, so
much the better!  But for complicated inductions, induction hints are
crucial.  See HINTS for a description of :induct hints.

*C4. Use the "Proof Checker" to explore.*
The verify command supplied by ACL2 allows one to explore problem areas
"by hand."  However, even if you succeed in proving a conjecture with
verify, it is useful to prove it without using it, an activity that
will often require the discovery of rewrite rules that will be useful
in later proofs as well.

*C5. Don't have too much patience.*
Interrupt the prover fairly quickly when simplification isn't
succeeding.

*C6. Simplify rewrite rules.*
When it looks difficult to relieve the hypotheses of an existing
rewrite rule that "should" apply in a given setting, ask yourself if
you can eliminate a hypothesis from the existing rewrite rule.  If so,
it may be easier to prove the new version from the old version (and
some additional lemmas), rather than to start from scratch.

*C7. Deal with base cases first.*
Try getting past the base case(s) first in a difficult proof by
induction.  Usually they're easier than the inductive step(s), and
rules developed in proving them can be useful in the inductive step(s)
too.  Moreover, it's pretty common that mistakes in the statement of a
theorem show up in the base case(s) of its proof by induction.

*C8. Use* :expand *hints.* Consider giving :expand hints.  These are
especially useful when a proof by induction is failing.  It's almost
always helpful to open up a recursively defined function that is
supplying the induction scheme, but sometimes ACL2 is too timid to do
so; or perhaps the function in question is disabled.

_D. PERFORMANCE TIPS_

*D1. Disable rules.*
There are a number of instances when it is crucial to disable rules,
including (often) those named explicitly in :use hints.  Also, disable
recursively defined functions for which you can prove what seem to be
all the relevant properties.  The prover can spend significant time
"behind the scenes" trying to open up recursively defined functions,
where the only visible effect is slowness.

*D2. Turn off the "break rewrite" facility.* Remember to execute :brr
nil after you've finished with the "break rewrite" utility (see
BREAK-REWRITE), in order to bring the prover back up to full speed.

_E. MISCELLANEOUS TIPS AND KNOWLEDGE_

*E1. Order of application of rewrite rules.*
Keep in mind that the most recent rewrite rules in the history are
tried first.

*E2. Relieving hypotheses is not full-blown theorem proving.*
Relieving hypotheses on rewrite rules is done by rewriting and linear
arithmetic alone, not by case splitting or by other prover processes
"below" simplification.

*E3. "Free variables" in rewrite rules.*
The set of "free variables" of a rewrite rule is defined to contain
those variables occurring in the rule that do not occur in the left-hand
side of the rule.  It's often a good idea to avoid rules containing
free variables because they are "weak," in the sense that hypotheses
containing such variables can generally only be proved when they are
"obviously" present in the current context.  This weakness suggests
that it's important to put the most "interesting" (specific) hypotheses
about free variables first, so that the right instances are considered.
For example, suppose you put a very general hypothesis such as (consp
x) first.  If the context has several terms around that are known to be
consps, then x may be bound to the wrong one of them.  For much more
information on free variables, see FREE-VARIABLES.

*E4. Obtaining information* Use :pl foo to inspect rewrite rules whose
left hand sides are applications of the function foo.  Another approach
to seeing which rewrite rules apply is to enter the proof-checker with
verify, and use the show-rewrites or sr command.

*E5. Consider esoteric rules with care.*
If you care to see RULE-CLASSES and peruse the list of
subtopics (which will be listed right there in most versions of this
documentation), you'll see that ACL2 supports a wide variety of rules
in addition to :rewrite rules.  Should you use them?  This is a complex
question that we are not ready to answer with any generality.  Our
general advice is to avoid relying on such rules as long as you doubt
their utility.  More specifically:  be careful not to use conditional
type prescription rules, as these have been known to bring ACL2 to its
knees, unless you are conscious that you are doing so and have reason
to believe that they are working well.

_F. SOME THINGS YOU DON'T NEED TO KNOW_

Most generally:  you shouldn't usually need to be able to predict too
much about ACL2's behavior.  You should mainly just need to be able to
react to it.

*F1. Induction heuristics.*
Although it is often important to read the part of the prover's output
that gives the induction scheme chosen by the prover, it is not
necessary to understand how the prover made that choice.  (Granted,
advanced users may occasionally gain minor insight from such knowledge.
But it's truly minor in many cases.)  What _is_ important is to be
able to tell it an appropriate induction when it doesn't pick the right
one (after noticing that it doesn't).  See C3 above.

*F2. Heuristics for expanding calls of recursively defined functions.*
As with the previous topic, the important thing isn't to understand
these heuristics but, rather, to deal with cases where they don't seem
to be working.  That amounts to supplying :expand hints for those calls
that you want opened up, which aren't.  See also C8 above.

*F3. The "waterfall".*
As discussed many times already, a good strategy for using ACL2 is to
look for checkpoints (goals stable under simplification) when a proof
fails, perhaps using the proof-tree facility.  Thus, it is reasonable
to ignore almost all the prover output, and to avoid pondering the
meaning of the other "processes" that ACL2 uses besides simplification
(such as elimination, cross-fertilization, generalization, and
elimination of irrelevance).  For example, you don't need to worry
about prover output that mentions "type reasoning" or "abbreviations,"
for example.

TUTORIAL-EXAMPLES    examples of ACL2 usage

Beginning users may find these examples at least as useful as the
extensive documentation on particular topics.  We suggest that you read
these in the following order:

     Tutorial1-Towers-of-Hanoi
     Tutorial2-Eights-Problem
     Tutorial3-Phonebook-Example
     Tutorial4-Defun-Sk-Example
     Tutorial5-Miscellaneous-Examples

You may also wish to visit the other introductory sections, startup and
tidbits.  These contain further information related to the use of ACL2.

When you feel you have read enough examples, you might want to try the
following very simple example on your own.  First define the notion of
the "fringe" of a tree, where we identify trees simply as cons
structures, with atoms at the leaves.  For example:

       ACL2 !>(fringe '((a . b) c . d))
       (A B C D)

Next, define the notion of a "leaf" of a tree, i.e., a predicate leaf-p
that is true of an atom if and only if that atom appears at the tip of
the tree.  Define this notion without referencing the function fringe.
Finally, prove the following theorem, whose proof may well be automatic
(i.e., not require any lemmas).

       (defthm leaf-p-iff-member-fringe
         (iff (leaf-p atm x)
              (member-equal atm (fringe x))))

For a solution, see SOLUTION-TO-SIMPLE-EXAMPLE.

SOLUTION-TO-SIMPLE-EXAMPLE    solution to a simple example

To see a statement of the problem solved below, see
TUTORIAL-EXAMPLES.

Here is a sequence of ACL2 events that illustrates the use of ACL2 to
make definitions and prove theorems.  We will introduce the notion of
the fringe of a tree, as well as the notion of a leaf of a tree, and
then prove that the members of the fringe are exactly the leaves.

We begin by defining the fringe of a tree, where we identify trees
simply as cons structures, with atoms at the leaves.  The definition is
recursive, breaking into two cases.  If x is a cons, then the fringe of
x is obtained by appending together the fringes of the car and cdr
(left and right child) of x.  Otherwise, x is an atom and its fringe is
the one-element list containing only x.

       (defun fringe (x)
         (if (consp x)
             (append (fringe (car x))
                     (fringe (cdr x)))
           (list x)))

Now that fringe has been defined, let us proceed by defining the notion
of an atom appearing as a "leaf", with the goal of proving that the
leaves of a tree are exactly the members of its fringe.

       (defun leaf-p (atm x)
         (if (consp x)
             (or (leaf-p atm (car x))
                 (leaf-p atm (cdr x)))
           (equal atm x)))

The main theorem is now as follows.  Note that the rewrite rule below
uses the equivalence relation iff (see EQUIVALENCE) rather than
equal, since member returns the tail of the given list that begins with
the indicated member, rather than returning a Boolean.  (Use :pe member
to see the definition of member.)

       (defthm leaf-p-iff-member-fringe
         (iff (leaf-p atm x)
              (member-equal atm (fringe x))))

TUTORIAL1-TOWERS-OF-HANOI    The Towers of Hanoi Example

This example was written almost entirely by Bill Young of Computational
Logic, Inc.

We will tackle the famous "Towers of Hanoi" problem.  This problem is
illustrated by the following picture.

               |        |        |
               |        |        |
              ---       |        |
             -----      |        |
            -------     |        |

               A        B        C

We have three pegs -- a, b, and c -- and n disks of different sizes.
The disks are all initially on peg a.  The goal is to move all disks to
peg c while observing the following two rules.

1. Only one disk may be moved at a time, and it must start and finish
the move as the topmost disk on some peg;

2. A disk can never be placed on top of a smaller disk.

Let's consider some simple instances of this problem.  If n = 1, i.e.,
only one disk is to be moved, simply move it from a to c.  If n = 2,
i.e., two disks are to be moved, the following sequence of moves
suffices:  move from a to b, move from a to c, move from b to c.

In general, this problem has a straightforward recursive solution.
Suppose that we desire to move n disks from a to c, using b as the
intermediate peg.  For the basis, we saw above that we can always move
a single disk from a to c.  Now if we have n disks and assume that we
can solve the problem for n-1 disks, we can move n disks as follows.
First, move n-1 disks from a to b using c as the intermediate peg; move
the single disk from a to c; then move n-1 disks from b to c using a as
the intermediate peg.

In ACL2, we can write a function that will return the sequence of
moves.  One such function is as follows.  Notice that we have two base
cases.  If (zp n) then n is not a positive integer; we treat that case
as if n were 0 and return an empty list of moves.  If n is 1, then we
return a list containing the single appropriate move.  Otherwise, we
return the list containing exactly the moves dictated by our recursive
analysis above.

       (defun move (a b)
         (list 'move a 'to b))

       (defun hanoi (a b c n)
         (if (zp n)
             nil
           (if (equal n 1)
               (list (move a c))
             (append (hanoi a c b (1- n))
                     (cons (move a c)
                           (hanoi b a c (1- n)))))))

Notice that we give hanoi four arguments:  the three pegs, and the
number of disks to move.  It is necessary to supply the pegs because,
in recursive calls, the roles of the pegs differ.  In any execution of
the algorithm, a given peg will sometimes be the source of a move,
sometimes the destination, and sometimes the intermediate peg.

After submitting these functions to ACL2, we can execute the hanoi
function on various specific arguments.  For example:

       ACL2 !>(hanoi 'a 'b 'c 1)
       ((MOVE A TO C))

       ACL2 !>(hanoi 'a 'b 'c 2)
       ((MOVE A TO B)
        (MOVE A TO C)
        (MOVE B TO C))

       ACL2 !>(hanoi 'a 'b 'c 3)
       ((MOVE A TO C)
        (MOVE A TO B)
        (MOVE C TO B)
        (MOVE A TO C)
        (MOVE B TO A)
        (MOVE B TO C)
        (MOVE A TO C))

From the algorithm it is clear that if it takes m moves to transfer n
disks, it will take (m + 1 + m) = 2m + 1 moves for n+1 disks.  From
some simple calculations, we see that we need the following number of
moves in specific cases:

        Disks   0   1   2   3   4   5   6   7  ...
        Moves   0   1   3   7  15  31  63  127 ...

The pattern is fairly clear.  To move n disks requires (2^n - 1) moves.
Let's attempt to use ACL2 to prove that fact.

First of all, how do we state our conjecture?  Recall that hanoi
returns a list of moves.  The length of the list (given by the function
len) is the number of moves required.  Thus, we can state the following
conjecture.

       (defthm hanoi-moves-required-first-try
         (equal (len (hanoi a b c n))
                (1- (expt 2 n))))

When we submit this to ACL2, the proof attempt fails.  Along the way we
notice subgoals such as:

       Subgoal *1/1'
       (IMPLIES (NOT (< 0 N))
                (EQUAL 0 (+ -1 (EXPT 2 N)))).

This tells us that the prover is considering cases that are
uninteresting to us, namely, cases in which n might be negative.  The
only cases that are really of interest are those in which n is a
non-negative natural number.  Therefore, we revise our theorem as
follows:

       (defthm hanoi-moves-required
         (implies (and (integerp n)
                       (<= 0 n))    ;; n is at least 0
                  (equal (len (hanoi a b c n))
                         (1- (expt 2 n)))))

and submit it to ACL2 again.

Again the proof fails.  Examining the proof script we encounter the
following text.  (How did we decide to focus on this goal?  Some
information is provided in ACLH, and the ACL2 documentation on tips may
be helpful.  But the simplest answer is:  this was the first goal
suggested by the "proof-tree" tool below the start of the proof by
induction.  See PROOF-TREE.)

       Subgoal *1/5''
       (IMPLIES (AND (INTEGERP N)
                     (< 0 N)
                     (NOT (EQUAL N 1))
                     (EQUAL (LEN (HANOI A C B (+ -1 N)))
                            (+ -1 (EXPT 2 (+ -1 N))))
                     (EQUAL (LEN (HANOI B A C (+ -1 N)))
                            (+ -1 (EXPT 2 (+ -1 N)))))
                (EQUAL (LEN (APPEND (HANOI A C B (+ -1 N))
                                    (CONS (LIST 'MOVE A 'TO C)
                                          (HANOI B A C (+ -1 N)))))
                       (+ -1 (* 2 (EXPT 2 (+ -1 N))))))

It is difficult to make much sense of such a complicated goal.
However, we do notice something interesting.  In the conclusion is a
term of the following shape.

        (LEN (APPEND ... ...))

We conjecture that the length of the append of two lists should be the
sum of the lengths of the lists.  If the prover knew that, it could
possibly have simplified this term earlier and made more progress in
the proof.  Therefore, we need a rewrite rule that will suggest such a
simplification to the prover.  The appropriate rule is:

       (defthm len-append
         (equal (len (append x y))
                (+ (len x) (len y))))

We submit this to the prover, which proves it by a straightforward
induction.  The prover stores this lemma as a rewrite rule and will
subsequently (unless we disable the rule) replace terms matching the
left hand side of the rule with the appropriate instance of the term on
the right hand side.

We now resubmit our lemma hanoi-moves-required to ACL2.  On this
attempt, the proof succeeds and we are done.

One bit of cleaning up is useful.  We needed the hypotheses that:

       (and (integerp n) (<= 0 n)).

This is an awkward way of saying that n is a natural number; natural is
not a primitive data type in ACL2.  We could define a function
naturalp, but it is somewhat more convenient to define a macro as
follows:

       (defmacro naturalp (x)
         (list 'and (list 'integerp x)
                       (list '<= 0 x)))

Subsequently, we can use (naturalp n) wherever we need to note that a
quantity is a natural number.  See DEFMACRO for more
information about ACL2 macros.  With this macro, we can reformulate our
theorem as follows:

       (defthm hanoi-moves-required
         (implies (naturalp n)
                  (equal (len (hanoi a b c n))
                         (1- (expt 2 n))))).

Another interesting (but much harder) theorem asserts that the list of
moves generated by our hanoi function actually accomplishes the desired
goal while following the rules.  When you can state and prove that
theorem, you'll be a very competent ACL2 user.

By the way, the name "Towers of Hanoi" derives from a legend that a
group of Vietnamese monks works day and night to move a stack of 64
gold disks from one diamond peg to another, following the rules set out
above.  We're told that the world will end when they complete this
task.  From the theorem above, we know that this requires
18,446,744,073,709,551,615 moves:

       ACL2 !>(1- (expt 2 64))
       18446744073709551615
       ACL2 !>

We're guessing they won't finish any time soon.

TUTORIAL2-EIGHTS-PROBLEM    The Eights Problem Example

This example was written almost entirely by Bill Young of Computational
Logic, Inc.

This simple example was brought to our attention as one that Paul
Jackson has solved using the NuPrl system.  The challenge is to prove
the theorem:

       for all n > 7, there exist naturals i and j such that: n = 3i + 5j.

In ACL2, we could phrase this theorem using quantification.  However we
will start with a constructive approach, i.e., we will show that values
of i and j exist by writing a function that will construct such values
for given n.  Suppose we had a function (split n) that returns an
appropriate pair (i . j).  Our theorem would be as follows:

       (defthm split-splits
         (let ((i (car (split n)))
               (j (cdr (split n))))
           (implies (and (integerp n)
                         (< 7 n))
                    (and (integerp i)
                         (<= 0 i)
                         (integerp j)
                         (<= 0 j)
                         (equal (+ (* 3 i) (* 5 j))
                                n)))))

That is, assuming that n is a natural number greater than 7, (split n)
returns values i and j that are in the appropriate relation to n.

Let's look at a few cases:

       8 = 3x1 + 5x1;    11 = 3x2 + 5x1;     14 = 3x3 + 5x1;   ...
       9 = 3x3 + 5x0;    12 = 3x4 + 5x0;     15 = 3x5 + 5x0;   ...
      10 = 3x0 + 5x2;    13 = 3x1 + 5x2;     16 = 3x2 + 5x2;   ...

Maybe you will have observed a pattern here; any natural number larger
than 10 can be obtained by adding some multiple of 3 to 8, 9, or 10.
This gives us the clue to constructing a proof.   It is clear that we
can write split as follows:

       (defun bump-i (x)
         ;; Bump the i component of the pair
         ;; (i . j) by 1.
         (cons (1+ (car x)) (cdr x)))

       (defun split (n)
         ;; Find a pair (i . j) such that
         ;; n = 3i + 5j.
         (if (or (zp n) (< n 8))
             nil ;; any value is really reasonable here
           (if (equal n 8)
               (cons 1 1)
             (if (equal n 9)
                 (cons 3 0)
               (if (equal n 10)
                   (cons 0 2)
                 (bump-i (split (- n 3))))))))

Notice that we explicitly compute the values of i and j for the cases
of 8, 9, and 10, and for the degenerate case when n is not a natural or
is less than 8.  For all naturals greater than n, we decrement n by 3
and bump the number of 3's (the value of i) by 1.  We know that the
recursion must terminate because any integer value greater than 10 can
eventually be reduced to 8, 9, or 10 by successively subtracting 3.

Let's try it on some examples:

       ACL2 !>(split 28)
       (6 . 2)

       ACL2 !>(split 45)
       (15 . 0)

       ACL2 !>(split 335)
       (110 . 1)

Finally, we submit our theorem split-splits, and the proof succeeds.
In this case, the prover is "smart" enough to induct according to the
pattern indicated by the function split.

For completeness, we'll note that we can state and prove a quantified
version of this theorem.  We introduce the notion split-able to mean
that appropriate i and j exist for n.

       (defun-sk split-able (n)
         (exists (i j)
                 (equal n (+ (* 3 i) (* 5 j)))))

Then our theorem is given below.  Notice that we prove it by observing
that our previous function split delivers just such an i and j (as we
proved above).

       (defthm split-splits2
         (implies (and (integerp n)
                       (< 7 n))
                  (split-able n))
         :hints (("Goal" :use (:instance split-able-suff
                                         (i (car (split n)))
                                         (j (cdr (split n)))))))

Unfortunately, understanding the mechanics of the proof requires
knowing something about the way defun-sk works.  See DEFUN-SK
or see TUTORIAL4-DEFUN-SK-EXAMPLE for more on that subject.

TUTORIAL3-PHONEBOOK-EXAMPLE    A Phonebook Specification

The other tutorial examples are rather small and entirely self
contained.  The present example is rather more elaborate, and makes use
of a feature that really adds great power and versatility to ACL2,
namely:  the use of previously defined collections of lemmas, in the
form of "books."

This example was written almost entirely by Bill Young of Computational
Logic, Inc.

This example is based on one developed by Ricky Butler and Sally
Johnson of NASA Langley for the PVS system, and subsequently revised by
Judy Crow, et al, at SRI.  It is a simple phone book specification.  We
will not bother to follow their versions closely, but will instead
present a style of specification natural for ACL2.

The idea is to model an electronic phone book with the following
properties.

     Our phone book will store the phone numbers of a city.

     It must be possible to retrieve a phone number, given a name.

     It must be possible to add and delete entries.

Of course, there are numerous ways to construct such a model.  A
natural approach within the Lisp/ACL2 context is to use "association
lists" or "alists."  Briefly, an alist is a list of pairs (key .
value) associating a value with a key.  A phone book could be an alist
of pairs (name . pnum).  To find the phone number associated with a
given name, we merely search the alist until we find the appropriate
pair.  For a large city, such a linear list would not be efficient, but
at this point we are interested only in *modeling* the problem, not in
deriving an efficient implementation.  We could address that question
later by proving our alist model equivalent, in some desired sense, to
a more efficient data structure.

We could build a theory of alists from scratch, or we can use a
previously constructed theory (book) of alist definitions and facts.
By using an existing book, we build upon the work of others, start our
specification and proof effort from a much richer foundation, and
hopefully devote more of our time to the problem at hand.
Unfortunately, it is not completely simple for the new user to know
what books are available and what they contain.  We hope later to
improve the documentation of the growing collection of books available
with the ACL2 distribution; for now, the reader is encouraged to look
in the README file in the books subdirectory.  For present purposes,
the beginning user can simply take our word that a book exists
containing useful alist definitions and facts.  On our local machine,
these definitions and lemmas can be introduced into the current theory
using the command:

       (include-book "/slocal/src/acl2/v1-9/books/public/alist-defthms")

This book has been "certified," which means that the definitions and
lemmas have been mechanically checked and stored in a safe manner.
(See BOOKS and see INCLUDE-BOOK for details.)

Including this book makes available a collection of functions including
the following:

     (ALISTP A)    ; is A an alist (actually a primitive ACL2 function)

     (BIND X V A)  ; associate the key X with value V in alist A

     (BINDING X A) ; return the value associated with key X in alist A

     (BOUND? X A)  ; is key X associated with any value in alist A

     (DOMAIN A)    ; return the list of keys bound in alist A

     (RANGE A)     ; return the list of values bound to keys in alist A

     (REMBIND X A) ; remove the binding of key X in alist A

Along with these function definitions, the book also provides a number
of proved lemmas that aid in simplifying expressions involving these
functions.  (See RULE-CLASSES for the way in which lemmas are
used in simplification and rewriting.)  For example,

       (defthm bound?-bind
         (equal (bound? x (bind y v a))
                (or (equal x y)
                    (bound? x a))))

asserts that x will be bound in (bind y v a) if and only if: either x =
y or x was already bound in a.  Also,

       (defthm binding-bind
         (equal (binding x (bind y v a))
                (if (equal x y)
                    v
                  (binding x a))))

asserts that the resulting binding will be v, if x = y, or the binding
that x had in a already, if not.

Thus, the inclusion of this book essentially extends our specification
and reasoning capabilities by the addition of new operations and facts
about these operations that allow us to build further specifications on
a richer and possibly more intuitive foundation.

However, it must be admitted that the use of a book such as this has
two potential limitations:

     the definitions available in a book may not be ideal for your
     particular problem;

     it is (extremely) likely that some useful facts (especially,
     rewrite rules) are not available in the book and will have to be
     proved.

For example, what is the value of binding when given a key that is not
bound in the alist?  We can find out by examining the function
definition.  Look at the definition of the binding function (or any
other defined function), using the :pe command:

       ACL2 !>:pe binding
          d     33  (INCLUDE-BOOK
                         "/slocal/src/acl2/v1-9/books/public/alist-defthms")

       >V d          (DEFUN BINDING (X A)
                            "The value bound to X in alist A."
                            (DECLARE (XARGS :GUARD (ALISTP A)))
                            (CDR (ASSOC-EQUAL X A)))

This tells us that binding was introduced by the given include-book
form, is currently disabled in the current theory, and has the
definition given by the displayed defun form.  We see that binding is
actually defined in terms of the primitive assoc-equal function.  If we
look at the definition of assoc-equal:

       ACL2 !>:pe assoc-equal
        V     -489  (DEFUN ASSOC-EQUAL (X ALIST)
                           (DECLARE (XARGS :GUARD (ALISTP ALIST)))
                           (COND ((ENDP ALIST) NIL)
                                 ((EQUAL X (CAR (CAR ALIST)))
                                  (CAR ALIST))
                                 (T (ASSOC-EQUAL X (CDR ALIST)))))

we can see that assoc-equal returns nil upon reaching the end of an
unsuccessful search down the alist.  So binding returns (cdr nil) in
that case, which is nil.  Notice that we could also have investigated
this question by trying some simple examples.

       ACL2 !>(binding 'a nil)
       NIL

       ACL2 !>(binding 'a (list (cons 'b 2)))
       NIL

These definitions aren't ideal for all purposes. For one thing, there's
nothing that keeps us from having nil as a value bound to some key in
the alist.  Thus, if binding returns nil we don't always know if that
is the value associated with the key in the alist, or if that key is
not bound.  We'll have to keep that ambiguity in mind whenever we use
binding in our specification.  Suppose instead that we wanted binding
to return some error string on unbound keys.  Well, then we'd just have
to write our own version of binding.  But then we'd lose much of the
value of using a previously defined book.  As with any specification
technique, certain tradeoffs are necessary.

Why not take a look at the definitions of other alist functions and see
how they work together to provide the ability to construct and search
alists?  We'll be using them rather heavily in what follows so it will
be good if you understand basically how they work.  Simply start up
ACL2 and execute the form shown earlier, but substituting our directory
name for the top-level ACL2 directory with yours.  Alternatively, the
following should work if you start up ACL2 in the directory of the ACL2
sources:

       (include-book "books/public/alist-defthms")

Then, you can use :pe to look at function definitions.  You'll soon
discover that almost all of the definitions are built on definitions of
other, more primitive functions, as binding is built on assoc-equal.
You can look at those as well, of course, or in many cases visit their
documentation.

The other problem with using a predefined book is that it will seldom
be "sufficiently complete," in the sense that the collection of rewrite
rules supplied won't be adequate to prove everything we'd like to know
about the interactions of the various functions.  If it were, there'd
be no real reason to know that binding is built on top of assoc-equal,
because everything we'd need to know about binding would be nicely
expressed in the collection of theorems supplied with the book.
However, that's very seldom the case.  Developing such a collection of
rules is currently more art than science and requires considerable
experience.  We'll encounter examples later of "missing" facts about
binding and our other alist functions.  So, let's get on with the
example.

Notice that alists are mappings of keys to values; but, there is no
notion of a "type" associated with the keys or with the values.  Our
phone book example, however, does have such a notion of types; we map
names to phone numbers.  We can introduce these "types" by explicitly
defining them, e.g., names are strings and phone numbers are integers.
Alternatively, we can *partially define* or axiomatize a recognizer for
names without giving a full definition.  A way to safely introduce such
"constrained" function symbols in ACL2 is with the encapsulate form.
For example, consider the following form.

       (encapsulate
         ;; Introduce a recognizer for names and give a ``type'' lemma.
         (((namep *) => *))
         ;;
         (local (defun namep (x)
                  ;; This declare is needed to tell
                  ;; ACL2 that we're aware that the
                  ;; argument x is not used in the body
                  ;; of the function.
                  (declare (ignore x))
                  t))
         ;;
         (defthm namep-booleanp
           (booleanp (namep x))))

This encapsulate form introduces the new function namep of one argument
and one result and constrains (namep x) to be Boolean, for all inputs
x.  More generally, an encapsulation establishes an environment in
which functions can be defined and theorems and rules added without
necessarily introducing those functions, theorems, and rules into the
environment outside the encapsulation.  To be admissible, all the
events in the body of an encapsulate must be admissible.  But the
effect of an encapsulate is to assume only the non-local events.

The first "argument" to encapsulate, ((namep (x) t)) above, declares
the intended signatures of new function symbols that will be "exported"
from the encapsulation without definition.  The local defun of name
defines name within the encapsulation always to return t.  The defthm
event establishes that namep is Boolean.  By making the defun local but
the defthm non-local this encapsulate constrains the undefined function
namep to be Boolean; the admissibility of the encapsulation establishes
that there exists a Boolean function (namely the constant function
returning t).

We can subsequently use namep as we use any other Boolean function,
with the proviso that we know nothing about it except that it always
returns either t or nil.  We use namep to "recognize" legal keys for
our phonebook alist.

We wish to do something similar to define what it means to be a legal
phone number.  We submit the following form to ACL2:

       (encapsulate
         ;; Introduce a recognizer for phone numbers.
         (((pnump *) => *))
         ;;
         (local (defun pnump (x)
                  (not (equal x nil))))
         ;;
         (defthm pnump-booleanp
           (booleanp (pnump x)))
         ;;
         (defthm nil-not-pnump
           (not (pnump nil)))).

This introduces a Boolean-valued recognizer pnump, with the additional
proviso that the constant nil is not a pnump.  We impose this
restriction to guarantee that we'll never bind a name to nil in our
phone book and thereby introduce the kind of ambiguity described above
regarding the use of binding.

Now a legal phone book is an alist mapping from nameps to pnumps.  We
can define this as follows:

       (defun name-phonenum-pairp (x)
         ;; Recognizes a pair of (name . pnum).
         (and (consp x)
              (namep (car x))
              (pnump (cdr x))))

       (defun phonebookp (l)
         ;; Recognizes a list of such pairs.
         (if (not (consp l))
             (null l)
           (and (name-phonenum-pairp (car l))
                (phonebookp (cdr l)))))

Thus, a phone book is really a list of pairs (name . pnum).  Notice
that we have not assumed that the keys of the phone book are distinct.
We'll worry about that question later.  (It is not always desirable to
insist that the keys of an alist be distinct.  But it may be a useful
requirement for our specific example.)

Now we are ready to define some of the functions necessary for our
phonebook example.  The functions we need are:

     (IN-BOOK? NM BK)          ; does NM have a phone number in BK

     (FIND-PHONE NM BK)        ; find NM's phone number in phonebook BK

     (ADD-PHONE NM PNUM BK)    ; give NM the phone number PNUM in BK

     (CHANGE-PHONE NM PNUM BK) ; change NM's phone number to PNUM in BK

     (DEL-PHONE NM PNUM)       ; remove NM's phone number from BK

Given our underlying theory of alists, it is easy to write these
functions.  But we must take care to specify appropriate "boundary"
behavior.  Thus, what behavior do we want when, say, we try to change
the phone number of a client who is not currently in the book?  As
usual, there are numerous possibilities; here we'll assume that we
return the phone book unchanged if we try anything "illegal."

Possible definitions of our phone book functions are as follows.
(Remember, an include-book form such as the ones shown earlier must be
executed in order to provide definitions for functions such as bound?.)

       (defun in-book? (nm bk)
         (bound? nm bk))

       (defun find-phone (nm bk)
         (binding nm bk))

       (defun add-phone (nm pnum bk)
         ;; If nm already in-book?, make no change.
         (if (in-book? nm bk)
             bk
           (bind nm pnum bk)))

       (defun change-phone (nm pnum bk)
         ;; Make a change only if nm already has a phone number.
         (if (in-book? nm bk)
             (bind nm pnum bk)
           bk))

       (defun del-phone (nm bk)
         ;; Remove the binding from bk, if there is one.
         (rembind nm bk))

Notice that we don't have to check whether a name is in the book before
deleting, because rembind is essentially a no-op if nm is not bound in
bk.

In some sense, this completes our specification.  But we can't have any
real confidence in its correctness without validating our specification
in some way.  One way to do so is by proving some properties of our
specification.  Some candidate properties are:

     1. A name will be in the book after we add it.

     2. We will find the most recently added phone number for a client.

     3. If we change a number, we'll find the change.

     4. Changing and then deleting a number is the same as just
     deleting.

     5. A name will not be in the book after we delete it.

Let's formulate some of these properties.  The first one, for example,
is:

       (defthm add-in-book
         (in-book? nm (add-phone nm pnum bk))).

You may wonder why we didn't need any hypotheses about the "types" of
the arguments.  In fact, add-in-book is really expressing a property
that is true of alists in general, not just of the particular variety
of alists we are dealing with.  Of course, we could have added some
extraneous hypotheses and proved:

       (defthm add-in-book
         (implies (and (namep nm)
                       (pnump pnum)
                       (phonebookp bk))
                  (in-book? nm (add-phone nm pnum bk)))),

but that would have yielded a weaker and less useful lemma because it
would apply to fewer situations.  In general, it is best to state
lemmas in the most general form possible and to eliminate unnecessary
hypotheses whenever possible.  The reason for that is simple: lemmas
are usually stored as rules and used in later proofs.  For a lemma to
be used, its hypotheses must be relieved (proved to hold in that
instance); extra hypotheses require extra work.  So we avoid them
whenever possible.

There is another, more important observation to make about our lemma.
Even in its simpler form (without the extraneous hypotheses), the lemma
add-in-book may be useless as a rewrite rule.  Notice that it is stated
in terms of the non-recursive functions in-book? and add-phone.  If such
functions appear in the left hand side of the conclusion of a lemma,
the lemma may not ever be used.  Suppose in a later proof, the theorem
prover encountered a term of the form:

       (in-book? nm (add-phone nm pnum bk)).

Since we've already proved add-in-book, you'd expect that this would be
immediately reduced to true.  However, the theorem prover will often
"expand" the non-recursive definitions of in-book?  and add-phone using
their definitions *before* it attempts rewriting with lemmas.  After
this expansion, lemma add-in-book won't "match" the term and so won't
be applied.  Look back at the proof script for add-in-proof and you'll
notice that at the very end the prover warned you of this potential
difficulty when it printed:

       Warnings:  Non-rec
       Time:  0.18 seconds (prove: 0.05, print: 0.00, other: 0.13)
       ADD-IN-BOOK

The "Warnings" line notifies you that there are non-recursive function
calls in the left hand side of the conclusion and that this problem
might arise.  Of course, it may be that you don't ever plan to use the
lemma for rewriting or that your intention is to disable these
functions.  Disabled functions are not expanded and the lemma should
apply.  However, you should always take note of such warnings and
consider an appropriate response.  By the way, we noted above that
binding is disabled.  If it were not, none of the lemmas about binding
in the book we included would likely be of much use for exactly the
reason we just gave.

For our current example, let's assume that we're just investigating the
properties of our specifications and not concerned about using our
lemmas for rewriting.  So let's go on.  If we really want to avoid the
warnings, we can add :rule-classes nil to each defthm event; see
RULE-CLASSES.

Property 2 is:  we always find the most recently added phone number for
a client.  Try the following formalization:

       (defthm find-add-first-cut
         (equal (find-phone nm (add-phone nm pnum bk))
                pnum))

and you'll find that the proof attempt fails.  Examining the proof
attempt and our function definitions, we see that the lemma is false if
nm is already in the book.  We can remedy this situation by
reformulating our lemma in at least two different ways:

       (defthm find-add1
         (implies (not (in-book? nm bk))
                  (equal (find-phone nm (add-phone nm pnum bk))
                         pnum)))

       (defthm find-add2
         (equal (find-phone nm (add-phone nm pnum bk))
                (if (in-book? nm bk)
                    (find-phone nm bk)
                    pnum)))

For technical reasons, lemmas such as find-add2, i.e., which do not
have hypotheses, are usually slightly preferable.  This lemma is stored
as an "unconditional" rewrite rule (i.e., has no hypotheses) and,
therefore, will apply more often than find-add1.  However, for our
current purposes either version is all right.

Property 3 says: If we change a number, we'll find the change.  This is
very similar to the previous example.  The formalization is as follows.

       (defthm find-change
         (equal (find-phone nm (change-phone nm pnum bk))
                (if (in-book? nm bk)
                    pnum
                  (find-phone nm bk))))

Property 4 says: changing and then deleting a number is the same as
just deleting.  We can model this as follows.

       (defthm del-change
         (equal (del-phone nm (change-phone nm pnum bk))
                (del-phone nm bk)))

Unfortunately, when we try to prove this, we encounter subgoals that
seem to be true, but for which the prover is stumped.  For example,
consider the following goal.  (Note:  endp holds of lists that are
empty.)

       Subgoal *1/4
       (IMPLIES (AND (NOT (ENDP BK))
                     (NOT (EQUAL NM (CAAR BK)))
                     (NOT (BOUND? NM (CDR BK)))
                     (BOUND? NM BK))
                (EQUAL (REMBIND NM (BIND NM PNUM BK))
                       (REMBIND NM BK))).

Our intuition about rembind and bind tells us that this goal should be
true even without the hypotheses.  We attempt to prove the following
lemma.

       (defthm rembind-bind
         (equal (rembind nm (bind nm pnum bk))
                (rembind nm bk)))

The prover proves this by induction, and stores it as a rewrite rule.
After that, the prover has no difficulty in proving del-change.

The need to prove lemma rembind-bind illustrates a point we made early
in this example:  the collection of rewrite rules supplied by a
previously certified book will almost never be everything you'll need.
It would be nice if we could operate purely in the realm of names,
phone numbers, and phone books without ever having to prove any new
facts about alists.  Unfortunately, we needed a fact about the relation
between rembind and bind that wasn't supplied with the alists theory.
Hopefully, such omissions will be rare.

Finally, let's consider our property 5 above:  a name will not be in
the book after we delete it.  We formalize this as follows:

       (defthm in-book-del
         (not (in-book? nm (del-phone nm bk))))

This proves easily.  But notice that it's only true because del-phone
(actually rembind) removes *all* occurrences of a name from the phone
book.  If it only removed, say, the first one it encountered, we'd need
a hypothesis that said that nm occurs at most once in bk.  Ah, maybe
that's a property you hadn't considered.  Maybe you want to ensure that
*any* name occurs at most once in any valid phonebook.

To complete this example, let's consider adding an *invariant* to our
specification.  In particular, suppose we want to assure that no client
has more than one associated phone number.  One way to ensure this is
to require that the domain of the alist is a "set" (has no duplicates).

       (defun setp (l)
         (if (atom l)
             (null l)
           (and (not (member-equal (car l) (cdr l)))
                (setp (cdr l)))))

       (defun valid-phonebookp (bk)
         (and (phonebookp bk)
              (setp (domain bk))))

Now, we want to show under what conditions our operations preserve the
property of being a valid-phonebookp.  The operations in-book?  and
find-phone don't return a phone book, so we don't really need to worry
about them.  Since we're really interested in the "types" of values
preserved by our phonebook functions, let's look at the types of those
operations as well.

       (defthm in-book-booleanp
         (booleanp (in-book? nm bk)))

       (defthm in-book-namep
         (implies (and (phonebookp bk)
                       (in-book? nm bk))
                  (namep nm))
         :hints (("Goal" :in-theory (enable bound?))))

       (defthm find-phone-pnump
         (implies (and (phonebookp bk)
                       (in-book? nm bk))
                  (pnump (find-phone nm bk)))
         :hints (("Goal" :in-theory (enable bound? binding))))

Note the ":hints" on the last two lemmas.  Neither of these would prove
without these hints, because once again there are some facts about
bound? and binding not available in our current context.  Now, we could
figure out what those facts are and try to prove them.  Alternatively,
we can enable bound? and binding and hope that by opening up these
functions, the conjectures will reduce to versions that the prover does
know enough about or can prove by induction.  In this case, this
strategy works.  The hints tell the prover to enable the functions in
question when considering the designated goal.

Below we develop the theorems showing that add-phone, change-phone, and
del-phone preserve our proposed invariant.  Notice that along the way
we have to prove some subsidiary facts, some of which are pretty ugly.
It would be a good idea for you to try, say,
add-phone-preserves-invariant without introducing the following four
lemmas first.  See if you can develop the proof and only add these
lemmas as you need assistance.  Then try
change-phone-preserves-invariant and del-phone-preserves-invariant.
They will be easier.  It is illuminating to think about why
del-phone-preserves-invariant does not need any "type" hypotheses.

       (defthm bind-preserves-phonebookp
         (implies (and (phonebookp bk)
                       (namep nm)
                       (pnump num))
                  (phonebookp (bind nm num bk))))

       (defthm member-equal-strip-cars-bind
         (implies (and (not (equal x y))
                       (not (member-equal x (strip-cars a))))
                  (not (member-equal x (strip-cars (bind y z a))))))

       (defthm bind-preserves-domain-setp
         (implies (and (alistp bk)
                       (setp (domain bk)))
                  (setp (domain (bind nm num bk))))
         :hints (("Goal" :in-theory (enable domain))))

       (defthm phonebookp-alistp
         (implies (phonebookp bk)
                  (alistp bk)))

       (defthm ADD-PHONE-PRESERVES-INVARIANT
         (implies (and (valid-phonebookp bk)
                       (namep nm)
                       (pnump num))
                  (valid-phonebookp (add-phone nm num bk)))
         :hints (("Goal" :in-theory (disable domain-bind))))

       (defthm CHANGE-PHONE-PRESERVES-INVARIANT
         (implies (and (valid-phonebookp bk)
                       (namep nm)
                       (pnump num))
                  (valid-phonebookp (change-phone nm num bk)))
         :hints (("Goal" :in-theory (disable domain-bind))))

       (defthm remove-equal-preserves-setp
         (implies (setp l)
                  (setp (remove-equal x l))))

       (defthm rembind-preserves-phonebookp
         (implies (phonebookp bk)
                  (phonebookp (rembind nm bk))))

       (defthm DEL-PHONE-PRESERVES-INVARIANT
         (implies (valid-phonebookp bk)
                  (valid-phonebookp (del-phone nm bk))))

As a final test of your understanding, try to formulate and prove an
invariant that says that no phone number is assigned to more than one
name.  The following hints may help.

     1. Define the appropriate invariant.  (Hint: remember the function
     range.)

     2. Do our current definitions of add-phone and change-phone
     necessarily preserve this property?  If not, consider what
     hypotheses are necessary in order to guarantee that they do
     preserve this property.

     3. Study the definition of the function range and notice that it
     is defined in terms of the function strip-cdrs.  Understand how
     this defines the range of an alist.

     4. Formulate the correctness theorems and attempt to prove them.
     You'll probably benefit from studying the invariant proof above.
     In particular, you may need some fact about the function strip-cdrs
     analogous to the lemma member-equal-strip-cars-bind above.

Below is one solution to this exercise.  Don't look at the solution,
however, until you've struggled a bit with it.  Notice that we didn't
actually change the definitions of add-phone and change-phone, but
added a hypothesis saying that the number is "new."  We could have
changed the definitions to check this and return the phonebook
unchanged if the number was already in use.

       (defun pnums-in-use (bk)
         (range bk))

       (defun phonenums-unique (bk)
         (setp (pnums-in-use bk)))

       (defun new-pnump (pnum bk)
         (not (member-equal pnum (pnums-in-use bk))))

       (defthm member-equal-strip-cdrs-rembind
         (implies (not (member-equal x (strip-cdrs y)))
                  (not (member-equal x (strip-cdrs (rembind z y))))))

       (defthm DEL-PHONE-PRESERVES-PHONENUMS-UNIQUE
         (implies (phonenums-unique bk)
                  (phonenums-unique (del-phone nm bk)))
         :hints (("Goal" :in-theory (enable range))))

       (defthm strip-cdrs-bind-non-member
         (implies (and (not (bound? x a))
                       (alistp a))
                  (equal (strip-cdrs (bind x y a))
                         (append (strip-cdrs a) (list y))))
         :hints (("Goal" :in-theory (enable bound?))))

       (defthm setp-append-list
         (implies (setp l)
                  (equal (setp (append l (list x)))
                         (not (member-equal x l)))))

       (defthm ADD-PHONE-PRESERVES-PHONENUMS-UNIQUE
         (implies (and (phonenums-unique bk)
                       (new-pnump pnum bk)
                       (alistp bk))
                  (phonenums-unique (add-phone nm pnum bk)))
         :hints (("Goal" :in-theory (enable range))))

       (defthm member-equal-strip-cdrs-bind
         (implies (and (not (member-equal z (strip-cdrs a)))
                       (not (equal z y)))
                  (not (member-equal z (strip-cdrs (bind x y a))))))

       (defthm CHANGE-PHONE-PRESERVES-PHONENUMS-UNIQUE
         (implies (and (phonenums-unique bk)
                       (new-pnump pnum bk)
                       (alistp bk))
                  (phonenums-unique (change-phone nm pnum bk)))
         :hints (("Goal" :in-theory (enable range))))

TUTORIAL4-DEFUN-SK-EXAMPLE    example of quantified notions

This example illustrates the use of defun-sk and defthm events to
reason about quantifiers.  See DEFUN-SK.  For a more through,
systematic beginner's introduction to quantification in ACL2, see
QUANTIFIER-TUTORIAL.

Many users prefer to avoid the use of quantifiers, since ACL2 provides
only very limited support for reasoning about quantifiers.

Here is a list of events that proves that if there are arbitrarily
large numbers satisfying the disjunction (OR P R), then either there
are arbitrarily large numbers satisfying P or there are arbitrarily
large numbers satisfying R.

     ; Introduce undefined predicates p and r.
     (defstub p (x) t)
     (defstub r (x) t)

     ; Define the notion that something bigger than x satisfies p.
     (defun-sk some-bigger-p (x)
       (exists y (and (< x y) (p y))))

     ; Define the notion that something bigger than x satisfies r.
     (defun-sk some-bigger-r (x)
       (exists y (and (< x y) (r y))))

     ; Define the notion that arbitrarily large x satisfy p.
     (defun-sk arb-lg-p ()
       (forall x (some-bigger-p x)))

     ; Define the notion that arbitrarily large x satisfy r.
     (defun-sk arb-lg-r ()
       (forall x (some-bigger-r x)))

     ; Define the notion that something bigger than x satisfies p or r.
     (defun-sk some-bigger-p-or-r (x)
       (exists y (and (< x y) (or (p y) (r y)))))

     ; Define the notion that arbitrarily large x satisfy p or r.
     (defun-sk arb-lg-p-or-r ()
       (forall x (some-bigger-p-or-r x)))

     ; Prove the theorem promised above.  Notice that the functions open
     ; automatically, but that we have to provide help for some rewrite
     ; rules because they have free variables in the hypotheses.  The
     ; ``witness functions'' mentioned below were introduced by DEFUN-SK.

     (thm
      (implies (arb-lg-p-or-r)
               (or (arb-lg-p)
                   (arb-lg-r)))
      :hints (("Goal"
               :use
               ((:instance some-bigger-p-suff
                           (x (arb-lg-p-witness))
                           (y (some-bigger-p-or-r-witness
                               (max (arb-lg-p-witness)
                                    (arb-lg-r-witness)))))
                (:instance some-bigger-r-suff
                           (x (arb-lg-r-witness))
                           (y (some-bigger-p-or-r-witness
                               (max (arb-lg-p-witness)
                                    (arb-lg-r-witness)))))
                (:instance arb-lg-p-or-r-necc
                           (x (max (arb-lg-p-witness)
                                   (arb-lg-r-witness))))))))

     ; And finally, here's a cute little example.  We have already
     ; defined above the notion (some-bigger-p x), which says that
     ; something bigger than x satisfies p.  Let us introduce a notion
     ; that asserts that there exists both y and z bigger than x which
     ; satisfy p.  On first glance this new notion may appear to be
     ; stronger than the old one, but careful inspection shows that y and
     ; z do not have to be distinct.  In fact ACL2 realizes this, and
     ; proves the theorem below automatically.

     (defun-sk two-bigger-p (x)
       (exists (y z) (and (< x y) (p y) (< x z) (p z))))

     (thm (implies (some-bigger-p x) (two-bigger-p x)))

     ; A technical point:  ACL2 fails to prove the theorem above
     ; automatically if we take its contrapositive, unless we disable
     ; two-bigger-p as shown below.  That is because ACL2 needs to expand
     ; some-bigger-p before applying the rewrite rule introduced for
     ; two-bigger-p, which contains free variables.  The moral of the
     ; story is:  Don't expect too much automatic support from ACL2 for
     ; reasoning about quantified notions.

     (thm (implies (not (two-bigger-p x)) (not (some-bigger-p x)))
          :hints (("Goal" :in-theory (disable two-bigger-p))))

TUTORIAL5-MISCELLANEOUS-EXAMPLES    miscellaneous ACL2 examples

The following examples are more advanced examples of usage of ACL2.
They are included largely for reference, in case someone finds them
useful.

FILE-READING-EXAMPLE    example of reading files in ACL2

This example illustrates the use of ACL2's IO primitives to read the
forms in a file.  See IO.

This example provides a solution to the following problem.  Let's say
that you have a file that contains s-expressions.  Suppose that you
want to build a list by starting with nil, and updating it
"appropriately" upon encountering each successive s-expression in the
file.  That is, suppose that you have written a function update-list
such that (update-list obj current-list) returns the list obtained by
"updating" current-list with the next object, obj, encountered in the
file.  The top-level function for processing such a file, returning the
final list, could be defined as follows.  Notice that because it opens
a channel to the given file, this function modifies state and hence
must return state.  Thus it actually returns two values:  the final
list and the new state.

       (defun process-file (filename state)
         (mv-let
          (channel state)
          (open-input-channel filename :object state)
          (mv-let (result state)
                  (process-file1 nil channel state) ;see below
                  (let ((state (close-input-channel channel state)))
                    (mv result state)))))

The function process-file1 referred to above takes the currently
constructed list (initially, nil), together with a channel to the file
being read and the state, and returns the final updated list.  Notice
that this function is tail recursive.  This is important because many
Lisp compilers will remove tail recursion, thus avoiding the potential
for stack overflows when the file contains a large number of forms.

       (defun process-file1 (current-list channel state)
         (mv-let (eofp obj state)
                 (read-object channel state)
                 (cond
                  (eofp (mv current-list state))
                  (t (process-file1 (update-list obj current-list)
                                    channel state)))))

FUNCTIONAL-INSTANTIATION-EXAMPLE    a small proof demonstrating functional instantiation

The example below demonstrates the use of functional instantiation,
that is, the use of a generic result in proving a result about specific
functions.  In this example we constrain a function to be associative
and commutative, with an identity or "root," on a given domain.  Next,
we define a corresponding function that applies the constrained
associative-commutative function to successive elements of a list.  We
then prove that the latter function gives the same value when we first
reverse the elements of the list.  Finally, we use functional
instantiation to derive the corresponding result for the function that
multiplies successive elements of a list.

The details of the proof (such as the in-theory event and particulars
of the lemmas) are not the point here.  Rather, the point is to
demonstrate the interaction of encapsulate events and
:functional-instance lemma-instances.  Of course, if you are interested
in details then you may find it helpful to run these events through
ACL2.

Also see CONSTRAINT for more about :functional-instance and see
LEMMA-INSTANCE for general information about the use of
previously-proved lemmas.

     (in-package "ACL2")

     (encapsulate
      (((ac-fn * *) => *)
       ((ac-fn-domain *) => *)
       ((ac-fn-root) => *))
      (local (defun ac-fn (x y) (+ x y)))
      (local (defun ac-fn-root () 0))
      (local (defun ac-fn-domain (x) (acl2-numberp x)))
      (defthm ac-fn-comm
        (equal (ac-fn x y)
               (ac-fn y x)))
      (defthm ac-fn-assoc
        (equal (ac-fn (ac-fn x y) z)
               (ac-fn x (ac-fn y z))))
      (defthm ac-fn-id
        (implies (ac-fn-domain x)
                 (equal (ac-fn (ac-fn-root) x)
                        x)))
      (defthm ac-fn-closed
        (and (ac-fn-domain (ac-fn x y))
             (ac-fn-domain (ac-fn-root)))))

     ;;;;;;;;;;;;;;;;;;;;;;;
     ; End of encapsulate. ;
     ;;;;;;;;;;;;;;;;;;;;;;;

     ; Define a ``fold'' function that iteratively applies ac-fn over a list.
     (defun ac-fn-list (x)
       (if (atom x)
           (ac-fn-root)
         (ac-fn (car x)
                (ac-fn-list (cdr x)))))

     ; Recognize lists all of whose elements are in the intended domain.
     (defun ac-fn-domain-list (x)
       (if (atom x)
           t
         (and (ac-fn-domain (car x))
              (ac-fn-domain-list (cdr x)))))

     ; Define a list reverse function.
     (defun rev (x)
       (if (atom x)
           nil
         (append (rev (cdr x))
                 (list (car x)))))

     ; The following is needed for proving ac-fn-list-append, which is
     ; needed for proving ac-fn-list-rev.
     (defthm ac-fn-list-closed
        (ac-fn-domain (ac-fn-list x)))

     ; Needed for proving ac-fn-list-rev:
     (defthm ac-fn-list-append
       (implies (and (ac-fn-domain-list x)
                     (ac-fn-domain-list y))
                (equal (ac-fn-list (append x y))
                       (ac-fn (ac-fn-list x)
                              (ac-fn-list y)))))

     ; Needed for proving ac-fn-list-rev:
     (defthm ac-fn-domain-list-rev
       (equal (ac-fn-domain-list (rev x))
              (ac-fn-domain-list x)))

     ; The following is a good idea because without it, the proof attempt
     ; for ac-fn-list-rev (see just below) fails with the term (HIDE
     ; (AC-FN-LIST NIL)).  It is often a good idea to disable
     ; executable-counterparts of functions that call constrained
     ; functions.
     (in-theory (disable (:executable-counterpart ac-fn-list)))

     (defthm ac-fn-list-rev
       (implies (ac-fn-domain-list x)
                (equal (ac-fn-list (rev x))
                       (ac-fn-list x))))

     ; Our goal now is to apply functional instantiation to ac-fn-list-rev
     ; in order to prove the corresponding theorem, times-list-rev, based
     ; on * instead of ac-fn.

     (defun times-list (x)
       (if (atom x)
           1
         (* (car x)
            (times-list (cdr x)))))

     (defun acl2-number-listp (x)
       (if (atom x)
           t
         (and (acl2-numberp (car x))
              (acl2-number-listp (cdr x)))))

     ; The following relies on the following built-in rules for * (whose
     ; statements correspond directly to their names): commutativity-of-*,
     ; associativity-of-*, and unicity-of-1.

     (defthm times-list-rev
       (implies (acl2-number-listp x)
                (equal (times-list (rev x))
                       (times-list x)))
       :hints (("Goal"
                :use
                ((:functional-instance
                  ac-fn-list-rev
                  ;; Instantiate the generic functions:
                  (ac-fn *)
                  (ac-fn-root (lambda () 1))
                  (ac-fn-domain acl2-numberp)
                  ;; Instantiate the other relevant functions:
                  (ac-fn-list times-list)
                  (ac-fn-domain-list acl2-number-listp))))))

GUARD-EXAMPLE    a brief transcript illustrating guards in ACL2

This note addresses the question:  what is the use of guards in ACL2?
Although we recommend that beginners try to avoid guards for a while,
we hope that the summary here is reasonably self-contained and will
provide a reasonable introduction to guards in ACL2.  For a more
systematic discussion, see GUARD.  For a summary of that topic,
see GUARD-QUICK-REFERENCE.

Before we get into the issue of guards, let us note that there are two
important "modes":

defun-mode -- "Does this defun add an axiom (`:logic mode') or not
(`:program mode')?"  (See DEFUN-MODE.)  Only :logic mode
functions can have their "guards verified" via mechanized proof; see
VERIFY-GUARDS.

set-guard-checking -- "Should runtime guard violations signal an error
(:all, and usually with t or :nowarn) or go undetected (nil, :none)?
Equivalently, are expressions evaluated in Common Lisp or in the
logic?"  (See SET-GUARD-CHECKING.)

_Prompt examples_

Here some examples of the relation between the ACL2 prompt and the
"modes" discussed above.  Also see DEFAULT-PRINT-PROMPT.  The
first examples all have ld-skip-proofsp nil; that is, proofs are _not_
skipped.

       ACL2 !>    ; logic mode with guard checking on
       ACL2 >     ; logic mode with guard checking off
       ACL2 p!>   ; program mode with guard checking on
       ACL2 p>    ; program mode with guard checking off

Here are some examples with default-defun-mode of :logic.

       ACL2 >     ; guard checking off, ld-skip-proofsp nil
       ACL2 s>    ; guard checking off, ld-skip-proofsp t
       ACL2 !>    ; guard checking on, ld-skip-proofsp nil
       ACL2 !s>   ; guard checking on, ld-skip-proofsp t

_Sample session_

     ACL2 !>(+ 'abc 3)

     ACL2 Error in TOP-LEVEL: The guard for the function symbol
     BINARY-+, which is (AND (ACL2-NUMBERP X) (ACL2-NUMBERP Y)),
     is violated by the arguments in the call (+ 'ABC 3).

     ACL2 !>:set-guard-checking nil
     ;;;; verbose output omitted here
     ACL2 >(+ 'abc 3)
     3
     ACL2 >(< 'abc 3)
     T
     ACL2 >(< 3 'abc)
     NIL
     ACL2 >(< -3 'abc)
     T
     ACL2 >:set-guard-checking t

     Turning guard checking on, value T.

     ACL2 !>(defun sum-list (x)
             (declare (xargs :guard (integer-listp x)
                             :verify-guards nil))
             (cond ((endp x) 0)
                   (t (+ (car x) (sum-list (cdr x))))))

     The admission of SUM-LIST is trivial, using the relation
     O< (which is known to be well-founded on the domain
     recognized by O-P) and the measure (ACL2-COUNT X).
     We observe that the type of SUM-LIST is described by the
     theorem (ACL2-NUMBERP (SUM-LIST X)).  We used primitive type
     reasoning.

     Summary
     Form:  ( DEFUN SUM-LIST ...)
     Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL))
     Warnings:  None
     Time:  0.03 seconds
        (prove: 0.00, print: 0.00, proof tree: 0.00, other: 0.03)
      SUM-LIST
     ACL2 !>(sum-list '(1 2 3))

     ACL2 Warning [Guards] in TOP-LEVEL:  Guard-checking will be inhibited
     on recursive calls of the executable counterpart (i.e., in the ACL2
     logic) of SUM-LIST.  To check guards on all recursive calls:
       (set-guard-checking :all)
     To leave behavior unchanged except for inhibiting this message:
       (set-guard-checking :nowarn)

     6
     ACL2 !>(sum-list '(1 2 abc 3))

     ACL2 Error in TOP-LEVEL: The guard for the function symbol
     BINARY-+, which is (AND (ACL2-NUMBERP X) (ACL2-NUMBERP Y)),
     is violated by the arguments in the call (+ 'ABC 3).

     ACL2 !>:set-guard-checking nil
     ;;;; verbose output omitted here
     ACL2 >(sum-list '(1 2 abc 3))
     6
     ACL2 >(defthm sum-list-append
            (equal (sum-list (append a b))
                   (+ (sum-list a) (sum-list b))))

     << Starting proof tree logging >>

     Name the formula above *1.

     Perhaps we can prove *1 by induction.  Three induction
     schemes are suggested by this conjecture.  Subsumption
     reduces that number to two.  However, one of these is flawed
     and so we are left with one viable candidate.

     ...

     That completes the proof of *1.

     Q.E.D.

_Guard verification vs. defun_

           Declare Form                        Guards Verified?

       (declare (xargs :mode :program ...))          no
       (declare (xargs :guard g))                    yes
       (declare (xargs :guard g :verify-guards nil)) no
       (declare (xargs ...<no :guard>...))           no

     ACL2 >:pe sum-list
      l        8  (DEFUN SUM-LIST (X)
                   (DECLARE (XARGS :GUARD (INTEGER-LISTP X)
                                   :VERIFY-GUARDS NIL))
                   (COND ((ENDP X) 0)
                         (T (+ (CAR X) (SUM-LIST (CDR X))))))
     ACL2 >(verify-guards sum-list)
     The non-trivial part of the guard conjecture for SUM-LIST,
     given the :type-prescription rule SUM-LIST, is

     Goal
     (AND (IMPLIES (AND (INTEGER-LISTP X) (NOT (CONSP X)))
                   (EQUAL X NIL))
          (IMPLIES (AND (INTEGER-LISTP X) (NOT (ENDP X)))
                   (INTEGER-LISTP (CDR X)))
          (IMPLIES (AND (INTEGER-LISTP X) (NOT (ENDP X)))
                   (ACL2-NUMBERP (CAR X)))).

     ...

     ACL2 >:pe sum-list
      lv       8  (DEFUN SUM-LIST (X)
                   (DECLARE (XARGS :GUARD (INTEGER-LISTP X)
                                   :VERIFY-GUARDS NIL))
     ACL2 >:set-guard-checking t

     Turning guard checking on, value T.

     ACL2 !>(sum-list '(1 2 abc 3))

     ACL2 Error in TOP-LEVEL: The guard for the function symbol
     SUM-LIST, which is (INTEGER-LISTP X), is violated by the
     arguments in the call (SUM-LIST '(1 2 ABC ...)).  See :DOC trace for a useful
     debugging utility.  See :DOC set-guard-checking for information about
     suppressing this check with (set-guard-checking :none), as recommended for
     new users.

     ACL2 !>:set-guard-checking nil
     ;;;; verbose output omitted here
     ACL2 >(sum-list '(1 2 abc 3))
     6
     ACL2 >:comp sum-list
     Compiling gazonk0.lsp.
     End of Pass 1.
     End of Pass 2.
     Finished compiling gazonk0.lsp.
     Loading gazonk0.o
     start address -T 1bbf0b4 Finished loading gazonk0.o
     Compiling gazonk0.lsp.
     End of Pass 1.
     End of Pass 2.
     Finished compiling gazonk0.lsp.
     Loading gazonk0.o
     start address -T 1bc4408 Finished loading gazonk0.o
      SUM-LIST
     ACL2 >:q

     Exiting the ACL2 read-eval-print loop.
     ACL2>(trace sum-list)
     (SUM-LIST)

     ACL2>(lp)

     ACL2 Version 1.8.  Level 1.  Cbd "/slocal/src/acl2/v1-9/".
     Type :help for help.
     ACL2 >(sum-list '(1 2 abc 3))
     6
     ACL2 >(sum-list '(1 2 3))
       1> (SUM-LIST (1 2 3))>
         2> (SUM-LIST (2 3))>
           3> (SUM-LIST (3))>
             4> (SUM-LIST NIL)>
             <4 (SUM-LIST 0)>
           <3 (SUM-LIST 3)>
         <2 (SUM-LIST 5)>
       <1 (SUM-LIST 6)>
     6
     ACL2 >:pe sum-list-append
               9  (DEFTHM SUM-LIST-APPEND
                          (EQUAL (SUM-LIST (APPEND A B))
                                 (+ (SUM-LIST A) (SUM-LIST B))))
     ACL2 >(verify-guards sum-list-append)

     The non-trivial part of the guard conjecture for
     SUM-LIST-APPEND, given the :type-prescription rule SUM-LIST,
     is

     Goal
     (AND (TRUE-LISTP A)
          (INTEGER-LISTP (APPEND A B))
          (INTEGER-LISTP A)
          (INTEGER-LISTP B)).

     ...

     ****** FAILED ******* See :DOC failure ****** FAILED ******
     ACL2 >(defthm common-lisp-sum-list-append
              (if (and (integer-listp a)
                       (integer-listp b))
                  (equal (sum-list (append a b))
                         (+ (sum-list a) (sum-list b)))
                  t)
              :rule-classes nil)

     << Starting proof tree logging >>

     By the simple :rewrite rule SUM-LIST-APPEND we reduce the
     conjecture to

     Goal'
     (IMPLIES (AND (INTEGER-LISTP A)
                   (INTEGER-LISTP B))
              (EQUAL (+ (SUM-LIST A) (SUM-LIST B))
                     (+ (SUM-LIST A) (SUM-LIST B)))).

     But we reduce the conjecture to T, by primitive type
     reasoning.

     Q.E.D.
     ;;;; summary omitted here
     ACL2 >(verify-guards common-lisp-sum-list-append)

     The non-trivial part of the guard conjecture for
     COMMON-LISP-SUM-LIST-APPEND, given the :type-prescription
     rule SUM-LIST, is

     Goal
     (AND (IMPLIES (AND (INTEGER-LISTP A)
                        (INTEGER-LISTP B))
                   (TRUE-LISTP A))
          (IMPLIES (AND (INTEGER-LISTP A)
                        (INTEGER-LISTP B))
                   (INTEGER-LISTP (APPEND A B)))).

     ...

     Q.E.D.

     That completes the proof of the guard theorem for
     COMMON-LISP-SUM-LIST-APPEND.  COMMON-LISP-SUM-LIST-APPEND
     is compliant with Common Lisp.
     ;;;; Summary omitted here.
     ACL2 >(defthm foo (consp (mv x y)))

     ...

     Q.E.D.

     ACL2 >(verify-guards foo)

     ACL2 Error in (VERIFY-GUARDS FOO): The number of values we
     need to return is 1 but the number of values returned by the
     call (MV X Y) is 2.

     > (CONSP (MV X Y))

     ACL2 Error in (VERIFY-GUARDS FOO): The guards for FOO cannot
     be verified because the theorem has the wrong syntactic
     form.  See :DOC verify-guards.

MUTUAL-RECURSION-PROOF-EXAMPLE    a small proof about mutually recursive functions

Sometimes one wants to reason about mutually recursive functions.
Although this is possible in ACL2, it can be a bit awkward.  This
example is intended to give some ideas about how one can go about such
proofs.

For an introduction to mutual recursion in ACL2, see
MUTUAL-RECURSION.

We begin by defining two mutually recursive functions:  one that
collects the variables from a term, the other that collects the
variables from a list of terms.  We actually imagine the term argument
to be a pseudo-termp; see PSEUDO-TERMP.

     (mutual-recursion

     (defun free-vars1 (term ans)
       (cond ((atom term)
              (add-to-set-eq term ans))
             ((fquotep term) ans)
             (t (free-vars1-lst (fargs term) ans))))

     (defun free-vars1-lst (lst ans)
       (cond ((atom lst) ans)
             (t (free-vars1-lst (cdr lst)
                                (free-vars1 (car lst) ans)))))

     )

The idea of the following function is that it suggests a proof by
induction in two cases, according to the top-level if structure of the
body.  In one case, (atom x) is true, and the theorem to be proved
should be proved under no additional hypotheses except for (atom x).
In the other case, (not (atom x)) is assumed together with three
instances of the theorem to be proved, one for each recursive call in
this case.  So, one instance substitutes (car x) for x; one substitutes
(cdr x) for x; and the third substitutes (cdr x) for x and (free-vars1
(car x) ans) for ans.  If you think about how you would go about a hand
proof of the theorem to follow, you'll come up with a similar scheme.

     (defun symbol-listp-free-vars1-induction (x ans)
       (if (atom x)
     ; then we just make sure x and ans aren't considered irrelevant
           (list x ans)
         (list (symbol-listp-free-vars1-induction (car x) ans)
               (symbol-listp-free-vars1-induction (cdr x) ans)
               (symbol-listp-free-vars1-induction
                (cdr x)
                (free-vars1 (car x) ans)))))

We now prove the two theorems together as a conjunction, because the
inductive hypotheses for one are sometimes needed in the proof of the
other (even when you do this proof on paper!).

     (defthm symbol-listp-free-vars1
       (and (implies (and (pseudo-termp x)
                          (symbol-listp ans))
                     (symbol-listp (free-vars1 x ans)))
            (implies (and (pseudo-term-listp x)
                          (symbol-listp ans))
                     (symbol-listp (free-vars1-lst x ans))))
       :hints
       (("Goal" :induct (symbol-listp-free-vars1-induction x ans))))

The above works, but let's try for a more efficient proof, which avoids
cluttering the proof with irrelevant (false) inductive hypotheses.

     (ubt 'symbol-listp-free-vars1-induction)

     (defun symbol-listp-free-vars1-induction (flg x ans)

     ; Flg is non-nil (or t) if we are ``thinking'' of a single term.

       (if (atom x)
           (list x ans)
         (if flg
             (symbol-listp-free-vars1-induction nil (cdr x) ans)
           (list (symbol-listp-free-vars1-induction t (car x) ans)
                 (symbol-listp-free-vars1-induction
                  nil
                  (cdr x)
                  (free-vars1 (car x) ans))))))

We now state the theorem as a conditional, so that it can be proved
nicely using the induction scheme that we have just coded.  The prover
will not store an if term as a rewrite rule, but that's OK (as long as
we tell it not to try), because we're going to derive the corollaries
of interest later and make *them* into rewrite rules.

     (defthm symbol-listp-free-vars1-flg
       (if flg
           (implies (and (pseudo-termp x)
                         (symbol-listp ans))
                    (symbol-listp (free-vars1 x ans)))
         (implies (and (pseudo-term-listp x)
                       (symbol-listp ans))
                  (symbol-listp (free-vars1-lst x ans))))
       :hints
       (("Goal" :induct (symbol-listp-free-vars1-induction flg x ans)))
       :rule-classes nil)

And finally, we may derive the theorems we are interested in as
immediate corollaries.

     (defthm symbol-listp-free-vars1
       (implies (and (pseudo-termp x)
                     (symbol-listp ans))
                (symbol-listp (free-vars1 x ans)))
       :hints (("Goal" :by (:instance symbol-listp-free-vars1-flg
                                      (flg t)))))

     (defthm symbol-listp-free-vars1-lst
       (implies (and (pseudo-term-listp x)
                     (symbol-listp ans))
                (symbol-listp (free-vars1-lst x ans)))
       :hints (("Goal" :by (:instance symbol-listp-free-vars1-flg
                                      (flg nil)))))

BDD    ordered binary decision diagrams with rewriting

Ordered binary decision diagrams (OBDDs, often simply called BDDs) are
a technique, originally published by Randy Bryant, for the efficient
simplification of Boolean expressions.  In ACL2 we combine this
technique with rewriting to handle arbitrary ACL2 terms that can
represent not only Boolean values, but non-Boolean values as well.  In
particular, we provide a setting for deciding equality of bit vectors
(lists of Boolean values).

An introduction to BDDs for the automated reasoning community may be
found in "Introduction to the OBDD Algorithm for the ATP Community" by
J Moore, Journal of Automated Reasoning (1994), pp. 33-45.  (This paper
also appears as Technical Report #84 from Computational Logic, Inc.)

Further information about BDDs in ACL2 can be found in the subtopics of
this documentation section.  In particular, see
BDD-INTRODUCTION for a good starting place that provides a number of
examples.

See HINTS for a description of :bdd hints.  For quick
reference, here is an example; but only the :vars part of the hint is
required, as explained in the documentation for hints.  The values
shown are the defaults.

     (:vars nil :bdd-constructors (cons) :prove t :literal :all)

We suggest that you next visit the documentation topic BDD-INTRODUCTION.

BDD-ALGORITHM    summary of the BDD algorithm in ACL2

The BDD algorithm in ACL2 uses a combination of manipulation of IF
terms and unconditional rewriting.  In this discussion we begin with
some relevant mathematical theory.  This is followed by a description
of how ACL2 does BDDs, including concluding discussions of soundness,
completeness, and efficiency.

We recommend that you read the other documentation about BDDs in ACL2
before reading the rather technical material that follows.  See
BDD.

Here is an outline of our presentation.  Readers who want a user
perspective, without undue mathematical theory, may wish to skip to
Part (B), referring to Part (A) only on occasion if necessary.

(A) *Mathematical Considerations*

     (A1) BDD term order

     (A2) BDD-constructors and BDD terms, and their connection with
     aborting the BDD algorithm

     (A3) Canonical BDD terms

     (A4) A theorem stating the equivalence of provable and syntactic
     equality for canonical BDD terms

(B) *Algorithmic Considerations*

     (B1) BDD rules (rules used by the rewriting portion of the ACL2 BDD
     algorithm)

     (B2) Terms "known to be Boolean"

     (B3) An "IF-lifting" operation used by the algorithm, as well as an
     iterative version of that operation

     (B4) The ACL2 BDD algorithm

     (B5) Soundness and Completeness of the ACL2 BDD algorithm

     (B6) Efficiency considerations

(A) *Mathematical Considerations*

(A1) _BDD term order_

Our BDD algorithm creates a total "BDD term order" on ACL2 terms, on
the fly.  We use this order in our discussions below of IF-lifting and
of canonical BDD terms, and in the algorithm's use of commutativity.
The particular order is unimportant, except that we guarantee (for
purposes of commutative functions) that constants are smaller in this
order than non-constants.

(A2) _BDD-constructors_ (assumed to be '(cons)) and _BDD terms_

We take as given a list of function symbols that we call the
"BDD-constructors."  By default, the only BDD-constructor is cons,
although it is legal to specify any list of function symbols as the
BDD-constructors, either by using the acl2-defaults-table (see
ACL2-DEFAULTS-TABLE) or by supplying a :BDD-CONSTRUCTORS hint (see
HINTS).  Warning: this capability is largely untested and may
produce undesirable results.  Henceforth, except when explicitly stated
to the contrary, we assume that BDD-constructors is '(cons).

Roughly speaking, a BDD term is the sort of term produced by our BDD
algorithm, namely a tree with all cons nodes lying above all non-CONS
nodes.  More formally, a term is said to be a BDD term if it contains
*no* subterm of either of the following forms, where f is not CONS.

     (f ... (CONS ...) ...)

     (f ... 'x ...)  ; where (consp x) = t

We will see that whenever the BDD algorithm attempts to create a term
that is not a BDD term, it aborts instead.  Thus, whenever the
algorithm completes without aborting, it creates a BDD term.

(A3) _Canonical BDD terms_

We can strengthen the notion of "BDD term" to a notion of "canonical
BDD term" by imposing the following additional requirements, for every
subterm of the form (IF x y z):

     (a) x is a variable, and it precedes (in the BDD term order) every
     variable occurring in y or z;

     (b) y and z are syntactically distinct; and,

     (c) it is not the case that y is t and z is nil.

We claim that it follows easily from our description of the BDD
algorithm that every term it creates is a canonical BDD term, assuming
that the variables occurring in all such terms are treated by the
algorithm as being Boolean (see (B2) below) and that the terms contain
no function symbols other than IF and CONS.  Thus, under those
assumptions the following theorem shows that the BDD algorithm never
creates distinct terms that are provably equal, a property that is
useful for completeness and efficiency (as we explain in (B5) and (B6)
below).

(A4) _Provably equal canonical BDD terms are identical_

We believe that the following theorem and proof are routine extensions
of a standard result and proof to terms that allow calls of CONS.

*Theorem*.  Suppose that t1 and t2 are canonical BDD terms that contain
no function symbols other than IF and CONS.  Also suppose that (EQUAL
t1 t2) is a theorem.  Then t1 and t2 are syntactically identical.

Proof of theorem:  By induction on the total number of symbols
occurring in these two terms.  First suppose that at least one term is
a variable; without loss of generality let it be t1.  We must prove
that t2 is syntactically the same as t1.  Now it is clearly consistent
that (EQUAL t1 t2) is false if t2 is a call of CONS (to see this,
simply let t1 be an value that is not a CONSP).  Similarly, t2 cannot
be a constant or a variable other than t1.  The remaining possibility
to rule out is that t2 is of the form (IF t3 t4 t5), since by
assumption its function symbol must be IF or CONS and we have already
handled the latter case.  Since t2 is canonical, we know that t3 is a
variable.  Since (EQUAL t1 t2) is provable, i.e.,

     (EQUAL t1 (if t3 t4 t5))

is provable, it follows that we may substitute either t or nil for t3
into this equality to obtain two new provable equalities.  First,
suppose that t1 and t3 are distinct variables.  Then these
substitutions show that t1 is provably equal to both t4 and t5 (since
t3 does not occur in t4 or t5 by property (a) above, as t2 is
canonical), and hence t4 and t5 are provably equal to each other, which
implies by the inductive hypothesis that they are the same term -- and
this contradicts the assumption that t2 is canonical (property (b)).
Therefore t1 and t3 are the same variable, i.e., the equality displayed
above is actually (EQUAL t1 (if t1 t4 t5)).  Substituting t and then
nil for t1 into this provable equality lets us prove (EQUAL t t4) and
(EQUAL nil t5), which by the inductive hypothesis implies that t4 is
(syntactically) the term t and t5 is nil.  That is, t2 is (IF t1 t
nil), which contradicts the assumption that t2 is canonical (property
(c)).

Next, suppose that at least one term is a call of IF.  Our first
observation is that the other term is also a call of IF.  For if the
other is a call of CONS, then they cannot be provably equal, because
the former has no function symbols other than IF and hence is Boolean
when all its variables are assigned Boolean values.  Also, if the other
is a constant, then both branches of the IF term are provably equal to
that constant and hence these branches are syntactically identical by
the inductive hypothesis, contradicting property (b).  Hence, we may
assume for this case that both terms are calls of IF; let us write them
as follows.

     t0:  (IF t1 t2 t3)
     u0:  (IF u1 u2 u3)

Note that t1 and u1 are variables, by property (a) of canonical BDD
terms.  First we claim that t1 does not strictly precede u1 in the BDD
term order.  For suppose t1 does strictly precede u1.  Then property
(a) of canonical BDD terms guarantees that t1 does not occur in u0.
Hence, an argument much like one used above shows that u0 is provably
equal to both t2 (substituting t for t1) and t3 (substituting nil for
t1), and hence t2 and t3 are provably equal.  That implies that they
are identical terms, by the inductive hypothesis, which then
contradicts property (b) for t0.  Similarly, u1 does not strictly
precede t1 in the BDD term order.  Therefore, t1 and u1 are the same
variable.  By substituting t for this variable we see that t2 and u2
are provably equal, and hence they are equal by the inductive
hypothesis.  Similarly, by substituting nil for t1 (and u1) we see that
t3 and u3 are provably, hence syntactically, equal.

We have covered all cases in which at least one term is a variable or
at least one term is a call of IF.  If both terms are constants, then
provable and syntactic equality are clearly equivalent.  Finally, then,
we may assume that one term is a call of CONS and the other is a
constant or a call of CONS.  The constant case is similar to the CONS
case if the constant is a CONSP, so we omit it; while if the constant
is not a CONSP then it is not provably equal to a call of CONS; in fact
it is provably _not_ equal!

So, we are left with a final case, in which canonical BDD terms (CONS
t1 t2) and (CONS u1 u2) are provably equal, and we want to show that t1
and u1 are syntactically equal as are t2 and u2.  These conclusions are
easy consequences of the inductive hypothesis, since the ACL2 axiom
CONS-EQUAL (which you can inspect using :PE) shows that equality of the
given terms is equivalent to the conjunction of (EQUAL t1 t2) and
(EQUAL u1 u2).  Q.E.D.

(B) *Algorithmic Considerations*

(B1) _BDD rules_

A rule of class :rewrite (see RULE-CLASSES) is said to be a
"BDD rewrite rule" if and only if it satisfies the following criteria.
(1) The rule is enabled.  (2) Its equivalence relation is equal.  (3)
It has no hypotheses.  (4) Its :loop-stopper field is nil, i.e., it is
not a permutative rule.  (5) All variables occurring in the rule occur
in its left-hand side (i.e., there are no "free variables"; see
REWRITE).  A rule of class :definition (see RULE-CLASSES) is
said to be a "BDD definition rule" if it satisfies all the criteria
above (except (4), which does not apply), and moreover the top function
symbol of the left-hand side was not recursively (or mutually
recursively) defined.  Technical point:  Note that this additional
criterion is independent of whether or not the indicated function
symbol actually occurs in the right-hand side of the rule.

Both BDD rewrite rules and BDD definition rules are said to be "BDD
rules."

(B2) _Terms "known to be Boolean"_

We apply the BDD algorithm in the context of a top-level goal to prove,
namely, the goal at which the :BDD hint is attached.  As we run the BDD
algorithm, we allow ourselves to say that a set of terms is "known to
be Boolean" if we can verify that the goal is provable from the
assumption that at least one of the terms is not Boolean.
Equivalently, we allow ourselves to say that a set of terms is "known
to be Boolean" if we can verify that the original goal is provably
equivalent to the assertion that if all terms in the set are Boolean,
then the goal holds.  The notion "known to be Boolean" is conservative
in the sense that there are generally sets of terms for which the above
equivalent criteria hold and yet the sets of terms are not noted as as
being "known to be Boolean."  However, ACL2 uses a number of tricks,
including type-set reasoning and analysis of the structure of the
top-level goal, to attempt to establish that a sufficiently inclusive
set of terms is known to be Boolean.

From a practical standpoint, the algorithm determines a set of terms
known to be Boolean; we allow ourselves to say that each term in this
set is "known to be Boolean."  The algorithm assumes that these terms
are indeed Boolean, and can make use of that assumption.  For example,
if t1 is known to be Boolean then the algorithm simplifies (IF t1 t
nil) to t1; see (iv) in the discussion immediately below.

(B3) _IF-lifting_ and the _IF-lifting-for-IF loop_

Suppose that one has a term of the form (f ... (IF test x y) ...),
where f is a function symbol other than CONS.  Then we say that
"IF-lifting" test "from" this term produces the following term, which
is provably equal to the given term.

     (if test
         (f ... x ...)  ; resulting true branch
         (f ... y ...)) ; resulting false branch

Here, we replace each argument of f of the form (IF test .. ..), for
the same test, in the same way.  In this case we say that "IF-lifting
applies to" the given term, "yielding the test" test and with the
"resulting two branches" displayed above.  Whenever we apply
IF-lifting, we do so for the available test that is least in the BDD
term order (see (A1) above).

We consider arguments v of f that are "known to be Boolean" (see above)
to be replaced by (IF v t nil) for the purposes of IF-lifting, i.e.,
before IF-lifting is applied.

There is one special case, however, for IF-lifting.  Suppose that the
given term is of the form (IF v y z) where v is a variable and is the
test to be lifted out (i.e., it is least in the BDD term order among
the potential tests).  Moroever, suppose that neither y nor z is of the
form (IF v W1 W2) for that same v.  Then IF-lifting does not apply to
the given term.

We may now describe the IF-lifting-for-IF loop, which applies to terms
of the form (IF test tbr fbr) where the algorithm has already produced
test, tbr, and fbr.  First, if test is nil then we return fbr, while if
test is a non-nil constant or a call of CONS then we return tbr.
Otherwise, we see if IF-lifting applies.  If IF-lifting does not apply,
then we return (IF test tbr fbr).  Otherwise, we apply IF-lifting to
obtain a term of the form (IF x y z), by lifting out the appropriate
test.  Now we recursively apply the IF-lifting-for-IF loop to the term
(IF x y z), unless any of the following special cases apply.

     (i) If y and z are the same term, then return y.

     (ii) Otherwise, if x and z are the same term, then replace z by
     nil before recursively applying IF-lifting-for-IF.

     (iii) Otherwise, if x and y are the same term and y is known to be
     Boolean, then replace y by t before recursively applying
     IF-lifting-for-IF.

     (iv) If z is nil and either x and y are the same term or x is
     "known to be Boolean" and y is t, then return x.

NOTE:  When a variable x is known to be Boolean, it is easy to see that
the form (IF x t nil) is always reduced to x by this algorithm.

(B4) _The ACL2 BDD algorithm_

We are now ready to present the BDD algorithm for ACL2.  It is given an
ACL2 term, x, as well as an association list va that maps variables to
terms, including all variables occurring in x.  We maintain the
invariant that whenever a variable is mapped by va to a term, that term
has already been constructed by the algorithm, except:  initially va
maps every variable occurring in the top-level term to itself.  The
algorithm proceeds as follows.  We implicitly ordain that whenever the
BDD algorithm attempts to create a term that is not a BDD term (as
defined above in (A2)), it aborts instead.  Thus, whenever the
algorithm completes without aborting, it creates a BDD term.

     If x is a variable, return the result of looking it up in va.

     If x is a constant, return x.

     If x is of the form (IF test tbr fbr), then first run the
     algorithm on test with the given va to obtain test'.  If test' is
     nil, then return the result fbr' of running the algorithm on fbr
     with the given va.  If test' is a constant other than nil, or is a
     call of CONS, then return the result tbr' of running the algorithm
     on tbr with the given va.  If tbr is identical to fbr, return tbr.
     Otherwise, return the result of applying the IF-lifting-for-IF
     loop (described above) to the term (IF test' tbr' fbr').

     If x is of the form (IF* test tbr fbr), then compute the result
     exactly as though IF were used rather than IF*, except that if
     test' is not a constant or a call of CONS (see paragraph above),
     then abort the BDD computation.  Informally, the tests of IF*
     terms are expected to "resolve."  NOTE:  This description shows
     how IF* can be used to implement conditional rewriting in the BDD
     algorithm.

     If x is a LAMBDA expression ((LAMBDA vars body) . args) (which
     often corresponds to a LET term; see LET), then first form
     an alist va' by binding each v in vars to the result of running
     the algorithm on the corresponding member of args, with the
     current alist va.  Then, return the result of the algorithm on
     body in the alist va'.

     Otherwise, x is of the form (f x1 x2 ... xn), where f is a
     function symbol other than IF or IF*.  In that case, let xi' be
     the result of running the algorithm on xi, for i from 1 to n,
     using the given alist va.  First there are a few special cases.
     If f is EQUAL then we return t if x1' is syntactically identical
     to x2' (where this test is very fast; see (B6) below); we return
     x1' if it is known to be Boolean and x2' is t; and similarly, we
     return x2' if it is known to be Boolean and x1' is t.  Next, if
     each xi' is a constant and the :executable-counterpart of f is
     enabled, then the result is obtained by computation.  Next, if f
     is BOOLEANP and x1' is known to be Boolean, t is returned.
     Otherwise, we proceed as follows, first possibly swapping the
     arguments if they are out of (the BDD term) order and if f is
     known to be commutative (see below).  If a BDD rewrite rule (as
     defined above) matches the term (f x1'... xn'), then the most
     recently stored such rule is applied.  If there is no such match
     and f is a BDD-constructor, then we return (f x1'... xn').
     Otherwise, if a BDD definition rule matches this term, then the
     most recently stored such rule (which will usually be the original
     definition for most users) is applied.  If none of the above
     applies and neither does IF-lifting, then we return (f x1'...
     xn').  Otherwise we apply IF-lifting to (f x1'... xn') to obtain a
     term (IF test tbr fbr); but we aren't done yet.  Rather, we run
     the BDD algorithm (using the same alist) on tbr and fbr to obtain
     terms tbr' and fbr', and we return (IF test tbr' fbr') unless tbr'
     is syntactically identical to fbr', in which case we return tbr'.

When is it the case that, as said above, "f is known to be
commutative"?  This happens when an enabled rewrite rule is of the form
(EQUAL (f X Y) (f Y X)).  Regarding swapping the arguments in that
case:  recall that we may assume very little about the BDD term order,
essentially only that we swap the two arguments when the second is a
constant and the first is not, for example, in (+ x 1).  Other than
that situation, one cannot expect to predict accurately when the
arguments of commutative operators will be swapped.

(B5) Soundness and Completeness of the ACL2 BDD algorithm

Roughly speaking, "soundness" means that the BDD algorithm should give
correct answers, and "completeness" means that it should be powerful
enough to prove all true facts.  Let us make the soundness claim a
little more precise, and then we'll address completeness under suitable
hypotheses.

*Claim* (Soundness).  If the ACL2 BDD algorithm runs to completion on
an input term t0, then it produces a result that is provably equal to
t0.

We leave the proof of this claim to the reader.  The basic idea is
simply to check that each step of the algorithm preserves the meaning
of the term under the bindings in the given alist.

Let us start our discussion of completeness by recalling the theorem
proved above in (A4).

*Theorem*.  Suppose that t1 and t2 are canonical BDD terms that contain
no function symbols other than IF and CONS.  Also suppose that (EQUAL
t1 t2) is a theorem.  Then t1 and t2 are syntactically identical.

Below we show how this theorem implies the following completeness
property of the ACL2 BDD algorithm.  We continue to assume that CONS is
the only BDD-constructor.

*Claim* (Completeness).  Suppose that t1 and t2 are provably equal
terms, under the assumption that all their variables are known to be
Boolean.  Assume further that under this same assumption, top-level
runs of the ACL2 BDD algorithm on these terms return terms that contain
only the function symbols IF and CONS.  Then the algorithm returns the
same term for both t1 and t2, and the algorithm reduces (EQUAL t1 t2)
to t.

Why is this claim true?  First, notice that the second part of the
conclusion follows immediately from the first, by definition of the
algorithm.  Next, notice that the terms u1 and u2 obtained by running
the algorithm on t1 and t2, respectively, are provably equal to t1 and
t2, respectively, by the Soundness Claim.  It follows that u1 and u2
are provably equal to each other.  Since these terms contain no
function symbols other than IF or CONS, by hypothesis, the Claim now
follows from the Theorem above together with the following lemma.

*Lemma*.  Suppose that the result of running the ACL2 BDD algorithm on
a top-level term t0 is a term u0 that contains only the function
symbols IF and CONS, where all variables of t0 are known to be Boolean.
Then u0 is a canonical BDD term.

Proof:  left to the reader.  Simply follow the definition of the
algorithm, with a separate argument for the IF-lifting-for-IF loop.

Finally, let us remark on the assumptions of the Completeness Claim
above.  The assumption that all variables are known to be Boolean is
often true; in fact, the system uses the forward-chaining rule
boolean-listp-forward (you can see it using :pe) to try to establish
this assumption, if your theorem has a form such as the following.

     (let ((x (list x0 x1 ...))
           (y (list y0 y1 ...)))
       (implies (and (boolean-listp x)
                     (boolean-listp y))
                ...))

Moreover, the :BDD hint can be used to force the prover to abort if it
cannot check that the indicated variables are known to be Boolean; see
HINTS.

Finally, consider the effect in practice of the assumption that the
terms resulting from application of the algorithm contain calls of IF
and CONS only.  Typical use of BDDs in ACL2 takes place in a theory
(see THEORIES) in which all relevant non-recursive function
symbols are enabled and all recursive function symbols possess enabled
BDD rewrite rules that tell them how open up.  For example, such a rule
may say how to expand on a given function call's argument that has the
form (CONS a x), while another may say how to expand when that argument
is nil).  (See for example the rules append-cons and append-nil in the
documentation for IF*.)  We leave it to future work to formulate a
theorem that guarantees that the BDD algorithm produces terms
containing calls only of IF and CONS assuming a suitably "complete"
collection of rewrite rules.

(B6) _Efficiency considerations_

Following Bryant's algorithm, we use a graph representation of terms
created by the BDD algorithm's computation.  This representation enjoys
some important properties.

     (Time efficiency) The test for syntactic equality of BDD terms is
     very fast.

     (Space efficiency) Equal BDD data structures are stored identically
     in memory.

_Implementation note._  The representation actually uses a sort of hash
table for BDD terms that is implemented as an ACL2 1-dimensional array.
See ARRAYS.  In addition, we use a second such hash table to
avoid recomputing the result of applying a function symbol to the
result of running the algorithm on its arguments.  We believe that
these uses of hash tables are standard.  They are also discussed in
Moore's paper on BDDs; see BDD for the reference.

BDD-INTRODUCTION    examples illustrating the use of BDDs in ACL2

See BDD for a brief introduction to BDDs in ACL2 and for
pointers to other documentation on BDDs in ACL2.  Here, we illustrate
the use of BDDs in ACL2 by way of some examples.  For a further
example, see IF*.

Let us begin with a really simple example.  (We will explain the :bdd
hint (:vars nil) below.)

     ACL2 !>(thm (equal (if a b c) (if (not a) c b))
                 :hints (("Goal" :bdd (:vars nil)))) ; Prove with BDDs

     [Note:  A hint was supplied for our processing of the goal above.
     Thanks!]

     But simplification with BDDs (7 nodes) reduces this to T, using the
     :definitions EQUAL and NOT.

     Q.E.D.

     Summary
     Form:  ( THM ...)
     Rules: ((:DEFINITION EQUAL) (:DEFINITION NOT))
     Warnings:  None
     Time:  0.18 seconds (prove: 0.05, print: 0.02, other: 0.12)

     Proof succeeded.
     ACL2 !>

The :bdd hint (:vars nil) indicates that BDDs are to be used on the
indicated goal, and that any so-called "variable ordering" may be used:
ACL2 may use a convenient order that is far from optimal.  It is
beyond the scope of the present documentation to address the issue of
how the user may choose good variable orderings.  Someday our
implementation of BDDs may be improved to include heuristically-chosen
variable orderings rather than rather random ones.

Here is a more interesting example.

     (defun v-not (x)
     ; Complement every element of a list of Booleans.
       (if (consp x)
           (cons (not (car x)) (v-not (cdr x)))
         nil))

     ; Now we prove a rewrite rule that explains how to open up v-not on
     ; a consp.
     (defthm v-not-cons
       (equal (v-not (cons x y))
              (cons (not x) (v-not y))))

     ; Finally, we prove for 7-bit lists that v-not is self-inverting.
     (thm
      (let ((x (list x0 x1 x2 x3 x4 x5 x6)))
        (implies (boolean-listp x)
                 (equal (v-not (v-not x)) x)))
      :hints (("Goal" :bdd
                      ;; Note that this time we specify a variable order.
                      (:vars (x0 x1 x2 x3 x4 x5 x6)))))

It turns out that the variable order doesn't seem to matter in this
example; using several orders we found that 30 nodes were created, and
the proof time was about 1/10 of a second on a (somewhat enhanced)
Sparc 2.  The same proof took about a minute and a half without any
:bdd hint!  This observation is a bit misleading perhaps, since the
theorem for arbitrary x,

     (thm
      (implies (boolean-listp x)
               (equal (v-not (v-not x)) x)))

only takes about 1.5 times as long as the :bdd proof for 7 bits, above!
Nevertheless, BDDs can be very useful in reducing proof time,
especially when there is no regular structure to facilitate proof by
induction, or when the induction scheme is so complicated to construct
that significant user effort is required to get the proof by induction
to go through.

Finally, consider the preceding example, with a :bdd hint of (say)
(:vars nil), but with the rewrite rule v-not-cons above disabled.  In
that case, the proof fails, as we see below.  That is because the BDD
algorithm in ACL2 uses hypothesis-free :rewrite rules,
:executable-counterparts, and nonrecursive definitions, but it does not
use recursive definitions.

Notice that when we issue the (show-bdd) command, the system's response
clearly shows that we need a rewrite rule for simplifying terms of the
form (v-not (cons ...)).

     ACL2 !>(thm
             (let ((x (list x0 x1 x2 x3 x4 x5 x6)))
               (implies (boolean-listp x)
                        (equal (v-not (v-not x)) x)))
             :hints (("Goal" :bdd (:vars nil)
                      :in-theory (disable v-not-cons))))

     [Note:  A hint was supplied for our processing of the goal above.
     Thanks!]

     ACL2 Error in ( THM ...):  Attempted to create V-NOT node during BDD
     processing with an argument that is a call of a bdd-constructor,
     which would produce a non-BDD term (as defined in :DOC
     bdd-algorithm).  See :DOC show-bdd.

     Summary
     Form:  ( THM ...)
     Rules: NIL
     Warnings:  None
     Time:  0.58 seconds (prove: 0.13, print: 0.00, other: 0.45)

     ******** FAILED ********  See :DOC failure  ******** FAILED ********
     ACL2 !>(show-bdd)

     BDD computation on Goal yielded 17 nodes.
     ==============================

     BDD computation was aborted on Goal, and hence there is no
     falsifying assignment that can be constructed.  Here is a backtrace
     of calls, starting with the top-level call and ending with the one
     that led to the abort.  See :DOC show-bdd.

     (LET ((X (LIST X0 X1 X2 X3 X4 X5 ...)))
          (IMPLIES (BOOLEAN-LISTP X)
                   (EQUAL (V-NOT (V-NOT X)) X)))
       alist: ((X6 X6) (X5 X5) (X4 X4) (X3 X3) (X2 X2) (X1 X1) (X0 X0))

     (EQUAL (V-NOT (V-NOT X)) X)
       alist: ((X (LIST X0 X1 X2 X3 X4 X5 ...)))

     (V-NOT (V-NOT X))
       alist: ((X (LIST X0 X1 X2 X3 X4 X5 ...)))

     (V-NOT X)
       alist: ((X (LIST X0 X1 X2 X3 X4 X5 ...)))
     ACL2 !>

The term that has caused the BDD algorithm to abort is thus (V-NOT X),
where X has the value (LIST X0 X1 X2 X3 X4 X5 ...), i.e., (CONS X0
(LIST X1 X2 X3 X4 X5 ...)).  Thus, we see the utility of introducing a
rewrite rule to simplify terms of the form (V-NOT (CONS ...)).  The
moral of this story is that if you get an error of the sort shown
above, you may find it useful to execute the command (show-bdd) and use
the result as advice that suggests the left hand side of a rewrite rule.

Here is another sort of failed proof.  In this version we have omitted
the hypothesis that the input is a bit vector.  Below we use show-bdd
to see what went wrong, and use the resulting information to construct
a counterexample.  This failed proof corresponds to a slightly modified
input theorem, in which x is bound to the 4-element list (list x0 x1 x2
x3).

     ACL2 !>(thm
             (let ((x (list x0 x1 x2 x3)))
               (equal (v-not (v-not x)) x))
             :hints (("Goal" :bdd
                      ;; This time we do not specify a variable order.
                      (:vars nil))))

     [Note:  A hint was supplied for our processing of the goal above.
     Thanks!]

     ACL2 Error in ( THM ...):  The :BDD hint for the current goal has
     successfully simplified this goal, but has failed to prove it.
     Consider using (SHOW-BDD) to suggest a counterexample; see :DOC
     show-bdd.

     Summary
     Form:  ( THM ...)
     Rules: NIL
     Warnings:  None
     Time:  0.18 seconds (prove: 0.07, print: 0.00, other: 0.12)

     ******** FAILED ********  See :DOC failure  ******** FAILED ********
     ACL2 !>(show-bdd)

     BDD computation on Goal yielded 73 nodes.
     ==============================

     Falsifying constraints:
     ((X0 "Some non-nil value")
      (X1 "Some non-nil value")
      (X2 "Some non-nil value")
      (X3 "Some non-nil value")
      ((EQUAL 'T X0) T)
      ((EQUAL 'T X1) T)
      ((EQUAL 'T X2) T)
      ((EQUAL 'T X3) NIL))

     ==============================

     Term obtained from BDD computation on Goal:

     (IF X0
         (IF X1
             (IF X2 (IF X3 (IF # # #) (IF X3 # #))
                 (IF X2 'NIL (IF X3 # #)))
             (IF X1 'NIL
                 (IF X2 (IF X3 # #) (IF X2 # #))))
         (IF X0 'NIL
             (IF X1 (IF X2 (IF X3 # #) (IF X2 # #))
                 (IF X1 'NIL (IF X2 # #)))))

     ACL2 Query (:SHOW-BDD):  Print the term in full?  (N, Y, W or ?):
     n ; I've seen enough.  The assignment shown above suggests
       ; (though not conclusively) that if we bind x3 to a non-nil
       ; value other than T, and bind x0, x1, and x2 to t, then we
       ; this may give us a counterexample.
     ACL2 !>(let ((x0 t) (x1 t) (x2 t) (x3 7))
              (let ((x (list x0 x1 x2 x3)))
                ;; Let's use LIST instead of EQUAL to see how the two
                ;; lists differ.
                (list (v-not (v-not x)) x)))
     ((T T T T) (T T T 7))
     ACL2 !>

See IF* for another example.

IF*    for conditional rewriting with BDDs

The function IF* is defined to be IF, but it is used in a special way
by ACL2's BDD package.

As explained elsewhere (see BDD-ALGORITHM), ACL2's BDD
algorithm gives special treatment to terms of the form (IF* TEST TBR
FBR).  In such cases, the algorithm simplifies TEST first, and the
result of that simplification must be a constant (normally t or nil,
but any non-nil explicit value is treated like t here).  Otherwise, the
algorithm aborts.

Thus, IF* may be used to implement a sort of conditional rewriting for
ACL2's BDD package, even though this package only nominally supports
unconditional rewriting.  The following contrived example should make
this point clear.

Suppose that we want to prove that (nthcdr (length x) (append x y)) is
equal to y, but that we would be happy to prove this only for lists
having length 4.  We can state such a theorem as follows.

     (let ((x (list x0 x1 x2 x3)))
       (equal (nthcdr (length x) (append x y))
              y))

If we want to prove this formula with a :BDD hint, then we need to have
appropriate rewrite rules around.  First, note that LENGTH is defined
as follows (try :PE LENGTH):

     (length x)
      =
     (if (stringp x)
         (len (coerce x 'list))
         (len x))

Since BDD-based rewriting is merely very simple unconditional rewriting
(see BDD-ALGORITHM), we expect to have to prove a rule reducing
STRINGP of a CONS:

     (defthm stringp-cons
       (equal (stringp (cons x y))
              nil))

Now we need a rule to compute the LEN of X, because the definition of
LEN is recursive and hence not used by the BDD package.

     (defthm len-cons
       (equal (len (cons a x))
              (1+ (len x))))

We imagine this rule simplifying (LEN (LIST X0 X1 X2 X3)) in terms of
(LEN (LIST X1 X2 X3)), and so on, and then finally (LEN nil) should be
computed by execution (see BDD-ALGORITHM).

We also need to imagine simplifying (APPEND X Y), where still X is
bound to (LIST X0 X1 X2 X3).  The following two rules suffice for this
purpose (but are needed, since APPEND, actually BINARY-APPEND, is
recursive).

     (defthm append-cons
       (equal (append (cons a x) y)
              (cons a (append x y))))

     (defthm append-nil
       (equal (append nil x)
              x))

Finally, we imagine needing to simplify calls of NTHCDR, where the the
first argument is a number (initially, the length of (LIST X0 X1 X2
X3), which is 4).  The second lemma below is the traditional way to
accomplish that goal (when not using BDDs), by proving a conditional
rewrite rule.  (The first lemma is only proved in order to assist in
the proof of the second lemma.)

     (defthm fold-constants-in-+
       (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)))))

The problem with this rule is that its hypothesis makes it a
conditional rewrite rule, and conditional rewrite rules are not used by
the BDD package.  (See BDD-ALGORITHM for a discussion of "BDD
rules.")  (Note that the hypothesis cannot simply be removed; the
resulting formula would be false for n = -1 and x = '(a), for example.)
We can solve this problem by using IF*, as follows; comments follow.

     (defthm nthcdr-add1
       (equal (nthcdr (+ 1 n) x)
              (if* (zp (1+ n))
                   x
                   (nthcdr n (cdr x)))))

How is nthcdr-add1 applied by the BDD package?  Suppose that the BDD
computation encounters a term of the form (NTHCDR (+ 1 N) X).  Then the
BDD package will apply the rewrite rule nthcdr-add1.  The first thing
it will do when attempting to simplify the right hand side of that rule
is to attempt to simplify the term (ZP (1+ N)).  If N is an explicit
number (which is the case in the scenario we envision), this test will
reduce (assuming the executable counterparts of ZP and BINARY-+ are
enabled) to t or to nil.  In fact, the lemmas above (not including the
lemma nthcdr-add1-conditional) suffice to prove our goal:

     (thm (let ((x (list x0 x1 x2 x3)))
            (equal (nthcdr (length x) (append x y))
                   y))
          :hints (("Goal" :bdd (:vars nil))))

If we execute the following form that disables the definition and
executable counterpart of the function ZP

     (in-theory (disable zp (zp)))

before attempting the proof of the theorem above, we can see more
clearly the point of using IF*.  In this case, the prover makes the
following report.

     ACL2 Error in ( THM ...):  Unable to resolve test of IF* for term

     (IF* (ZP (+ 1 N)) X (NTHCDR N (CDR X)))

     under the bindings

     ((X (CONS X0 (CONS X1 (CONS X2 #)))) (N '3))

     -- use SHOW-BDD to see a backtrace.

If we follow the advice above, we can see rather clearly what happened.
See SHOW-BDD.

     ACL2 !>(show-bdd)

     BDD computation on Goal yielded 21 nodes.
     ==============================

     BDD computation was aborted on Goal, and hence there is no
     falsifying assignment that can be constructed.  Here is a backtrace
     of calls, starting with the top-level call and ending with the one
     that led to the abort.  See :DOC show-bdd.

     (LET ((X (LIST X0 X1 X2 X3)))
          (EQUAL (NTHCDR (LENGTH X) (APPEND X Y)) Y))
       alist: ((Y Y) (X3 X3) (X2 X2) (X1 X1) (X0 X0))

     (NTHCDR (LENGTH X) (APPEND X Y))
       alist: ((X (LIST X0 X1 X2 X3)) (Y Y))

     (IF* (ZP (+ 1 N)) X (NTHCDR N (CDR X)))
       alist: ((X (LIST* X0 X1 X2 X3 Y)) (N 3))
     ACL2 !>

Each of these term-alist pairs led to the next, and the test of the
last one, namely (ZP (+ 1 N)) where N is bound to 3, was not simplified
to t or to nil.

What would have happened if we had used IF in place of IF* in the rule
nthcdr-add1?  In that case, if ZP and its executable counterpart were
disabled then we would be put into an infinite loop!  For, each time a
term of the form (NTHCDR k V) is encountered by the BDD package (where
k is an explicit number), it will be rewritten in terms of (NTHCDR k-1
(CDR V)).  We would prefer that if for some reason the term (ZP (+ 1
N)) cannot be decided to be t or to be nil, then the BDD computation
should simply abort.

Even if there were no infinite loop, this kind of use of IF* is useful
in order to provide feedback of the form shown above whenever the test
of an IF term fails to simplify to t or to nil.

SHOW-BDD    inspect failed BDD proof attempts

Attempts to use BDDs (see BDD), using :bdd hints, can fail for
various reasons.  Sometimes it is useful to explore such failures.  To
do so, one may simply execute the form

     (show-bdd)

inside the ACL2 loop.  The system's response is generally
self-explanatory.  Perhaps you have already seen show-bdd used in some
examples (see BDD-INTRODUCTION and see IF*).  Here we
give some details about show-bdd.

(Show-bdd) prints the goal to which the BDD procedure was applied and
reports the number of nodes created during the BDD computation,
followed by additional information depending on whether or not the
computation ran to completion or aborted (for reasons explained
elsewhere; see BDD-ALGORITHM).  If the computation did abort, a
backtrace is printed that should be useful in understanding where the
problem lies.  Otherwise, (show-bdd) prints out "falsifying
constraints."  This list of pairs associates terms with values and
suggests how to construct a binding list for the variables in the
conjecture that will falsify the conjecture.  It also prints out the
term that is the result of simplifying the input term.  In each of
these cases, parts of the object may be hidden during printing, in
order to avoid creating reams of uninteresting output.  If so, the user
will be queried about whether he wishes to see the entire object (alist
or term), which may be quite large.  The following responses are legal:

       w -- Walk around the object with a structure editor

     t -- Print the object in full

     nil -- Do not print any more of the object

Show-bdd actually has four optional arguments, probably rarely used.
The general form is

     (show-bdd goal-name goal-ans falsifying-ans term-ans)

where goal-name is the name of the goal on which the :bdd hint was used
(or, nil if the system should find such a goal), goal-ans is the answer
to be used in place of the query for whether to print the input goal in
full, falsifying-ans is the answer to be used in place of the query for
whether to print the falsifying constraints in full, and term-ans is
the answer to be used in place of the query for whether to print the
resulting term in full.

BOOKS    files of ACL2 event forms

This documentation topic is about ACL2 input files.  However, there are
two traditional (paper) books published about ACL2: a textbook and a
case studies book.  Further information on those two paper books is
available by following links from the ACL2 home page,
`http://www.cs.utexas.edu/users/moore/acl2/'.

A "book" is a file of ACL2 events that have been certified as
admissible.  Using include-book you can construct a new logical world
by assuming the events in any number of mutually compatible books.
Relevant documented topics are listed below.  Following this list is a
"guided tour" through the topics.

You can contribute books to the ACL2 community and obtain updates
inbetween ACL2 releases by visiting the acl2-books project web page,
`http://acl2-books.googlecode.com/'.

Related topics other than immediate subtopics:

_Introduction._

A "book" is a file of ACL2 forms.  Books are prepared entirely by the
user of the system, i.e., they are "source" files not "object" files.
Some of the forms in a book are marked local and the others are
considered "non-local."

Include-book lets you load a book into any ACL2 world.  If completed
without error, the inclusion of a book extends the logic of the host
world by the addition of just the non-local events in the book.  You
may extend the world by successively including a variety of books to
obtain the desired collection of definitions and rules.  Unless name
conflicts occur (which are detected and signalled) inclusion of a book
is consistency preserving provided the book itself is consistent as
discussed later.  However, include-book merely assumes the validity of
the events in a book; if you include a book that contains an
inconsistency (e.g., an inadmissible definition) then the resulting
theory is inconsistent.

It is possible to "certify" a book, with certify-book, guaranteeing
that the error-free inclusion of the certified forms will produce a
consistent extension of a consistent logic.  Certification processes
both the local and non-local forms, so you can mark as local those
events you need for certification that you want to hide from users of
the book (e.g., hacks, crocks, and kludges on the way to a good set of
:rewrite rules).  Certification can also "compile" a book, thereby
speeding up the execution of the functions defined within it.  The
desire to compile books is largely responsible for the restrictions we
put on the forms allowed in books.

Extensive documentation is available on the various aspects of books.
We recommend that you read it all before using books.  It has been
written so as to make sense when read in a certain linear sequence,
called the "guided tour", though in general you may browse through it
randomly.  If you are on the guided tour, you should next read the
documentation on book-example (see BOOK-EXAMPLE).

BOOK-CONTENTS    restrictions on the forms inside books

     Example Book:

     ; This book defines my app function and the theorem that it is
     ; associative.  One irrelevant help lemma is proved first but
     ; it is local and so not seen by include-book.  I depend on the
     ; inferior book "weird-list-primitives" from which I get
     ; definitions of hd and tl.

     (in-package "MY-PKG")

     (include-book "weird-list-primitives")

     (defun app (x y) (if (consp x) (cons (hd x) (app (tl x) y)) y))

     (local
      (defthm help-lemma
        (implies (true-listp x) (equal (app x nil) x))))

     (defthm app-is-associative
       (equal (app (app a b) c) (app a (app b c))))

The first form in a book must be (in-package "pkg") where "pkg" is some
package name known to ACL2 whenever the book is certified.  The rest of
the forms in a book are embedded event forms, i.e., defuns, defthms,
etc., some of which may be marked local.  See
EMBEDDED-EVENT-FORM.  The usual Common Lisp commenting conventions
are provided.  Note that since a book consists of embedded event forms,
we can talk about the "local" and "non-local" events of a book.

Because in-package is not an embedded event form, the only in-package
in a book is the initial one.  Because defpkg is not an embedded event
form, a book can never contain a defpkg form.  Because include-book is
an embedded event form, books may contain references to other books.
This makes books structured objects.

When the forms in a book are read from the file, they are read with
current-package set to the package named in the in-package form at the
top of the file.  The effect of this is that all symbols are interned
in that package, except those whose packages are given explicitly with
the "::" notation.  For example, if a book begins with (in-package
"ACL2-X") and then contains the form

       (defun fn (x)
         (acl2::list 'car x))

then defun, fn, x, and car are all interned in the "ACL2-X" package.
I.e., it is as though the following form were read instead:

       (acl2-x::defun acl2-x::fn (acl2-x::x)
           (acl2::list 'acl2-x::car acl2-x::x)).

Of course, acl2-x::defun would be the same symbol as acl2::defun if the
"ACL2-X" package imported acl2::defun.

If each book has its own unique package name and all the names defined
within the book are in that package, then name clashes between books
are completely avoided.  This permits the construction of useful
logical worlds by the successive inclusion of many books.  Although it
is often too much trouble to manage several packages, their judicious
use is a way to minimize name clashes.  Often, a better way is to use
local; see LOCAL.

How does include-book know the definitions of the packages used in a
book, since defpkgs cannot be among the forms?  More generally, how do
we know that the forms in a book will be admissible in the host logical
world of an include-book?  See CERTIFICATE for answers to these
questions.

BOOK-EXAMPLE    how to create, certify, and use a simple book

Suppose you have developed a sequence of admissible events which you
want to turn into a book.  We call this "publishing" the book.  This
note explains how to do that.

A key idea of books is that they are "incremental" in the sense that
when you include a book in a host logical world, the world is
incrementally extended by the results established in that book.  This
is allowed only if every name defined by the incoming book is either
new or is already identically defined.  See REDUNDANT-EVENTS.
This is exactly the same problem faced by a programmer who wishes to
provide a utility to other people: how can he make sure he doesn't
create name conflicts?  The solution, in Common Lisp, is also the same:
use packages.  While books and packages have a very tenuous formal
connection (every book must start with an in-package), the creation of
a book is intimately concerned with the package issue.  Having
motivated what would otherwise appear as an unnecessary fascination
with packages below, we now proceed with a description of how to
publish a book.

Just to be concrete, let's suppose you have already gotten ACL2 to
accept the following sequence of commands, starting in the ACL2 initial
state.

        (defpkg "ACL2-MY-BOOK"
                (union-eq *common-lisp-symbols-from-main-lisp-package*
                          *acl2-exports*))
        (in-package "ACL2-MY-BOOK")
        (defun app (x y)
          (if (consp x) (cons (car x) (app (cdr x) y)) y))
        (defun rev (x)
          (if (consp x) (app (rev (cdr x)) (list (car x))) nil))
        (defthm rev-app-hack
          (equal (rev (app a (list x))) (cons x (rev a))))
        (defthm rev-rev
          (implies (acl2::true-listp x) (equal (rev (rev x)) x)))

Observe that the first form above defines a package (which imports the
symbols defined in CLTL such as if and cons and the symbols used to
command ACL2 such as defun and defthm).  The second form selects that
package as the current one.  All subsequent forms are read into that
package.  The remaining forms are just event forms: defuns and defthms
in this case.

Typically you would have created a file with Emacs containing these
forms and you will have submitted each of them interactively to ACL2 to
confirm that they are all admissible.  That interactive verification
should start in ACL2's initial world -- although you might, of course,
start your sequence of events with some include-books to build a more
elaborate world.

The first step towards publishing a book containing the results above
is to create a file that starts with the in-package and then contains
the rest of the forms.  Let's call that file "my-book.lisp".  The name
is unimportant, except it must end with ".lisp".  If there are events
that you do not wish to be available to the user of the book -- e.g.,
lemmas you proved on your way toward proving the main ones -- you may
so mark them by enclosing them in local forms.  See LOCAL.  Let
us suppose you wish to hide rev-app-hack above.  You may also add
standard Lisp comments to the file.  The final content of "my-book.lisp"
might be:

      ; This book contains my app and rev functions and the theorem
      ; that rev is its own inverse.

        (in-package "ACL2-MY-BOOK")
        (defun app (x y)
          (if (consp x) (cons (car x) (app (cdr x) y)) y))
        (defun rev (x)
          (if (consp x) (app (rev (cdr x)) (list (car x))) nil))

      ; The following hack is not exported.
        (local (defthm rev-app-hack
          (equal (rev (app a (list x))) (cons x (rev a)))))

        (defthm rev-rev
          (implies (acl2::true-listp x) (equal (rev (rev x)) x)))

The file shown above *is* the book.  By the time this note is done you
will have seen how to certify that the book is correct, how to compile
it, and how to use it in other host worlds.  Observe that the defpkg is
not in the book.  It cannot be: Common Lisp compilers disagree on how
to treat new package definitions appearing in files to be compiled.

Since a book is just a source file typed by the user, ACL2 provides a
mechanism for checking that the events are all admissible and then
marking the file as checked.  This is called certification.  To certify
"my-book.lisp" you should first get into ACL2 with an initial world.
Then, define the package needed by the book, by typing the following
defpkg to the ACL2 prompt:

     ACL2 !>(defpkg "ACL2-MY-BOOK"
                    (union-eq *common-lisp-symbols-from-main-lisp-package*
                              *acl2-exports*))

Then execute the command:

     ACL2 !>(certify-book "my-book" 1 t) ; the `t' is in fact the default

Observe that you do not type the ".lisp" part of the file name.  For
purposes of books, the book's name is "my-book" and by the time all is
said and done, there will be several extensions in addition to the
".lisp" extension associated with it.

The 1 tells certify-book that you acknowledge that there is one command
in this "certification world" (namely the defpkg).  To use the book,
any prospective host world must be extended by the addition of whatever
commands occurred before certification.  It would be a pity to certify
a book in a world containing junk because that junk will become the
"portcullis" guarding entrance to the book.  The t above tells
certify-book that you wish to compile "my-book.lisp" also (but see
COMPILATION for an exception).  Certify-book makes many checks
but by far the most important and time-consuming one is that it
"proves" every event in the file.

When certify-book is done it will have created two new files.  The
first will be called "my-book.cert" and contains the "certificate"
attesting to the admissibility of the events in "my-book.lisp".  The
certificate contains the defpkg and any other forms necessary to
construct the certification world.  It also contains various check sums
used to help you keep track of which version of "my-book.lisp" was
certified.

The second file that may be created by certify-book is the compiled
version of "my-book.lisp" and will have a name that is assigned by the
host compiler (e.g., "my-book.o" in GCL, "my-book.fasl" in SBCL).
Certify-book will also load this object file.  When certify-book is
done, you may throw away the logical world it created, for example by
executing the command :u.

To use the book later in any ACL2 session, just execute the event
(include-book "my-book").  This will do the necessary defpkg, load the
non-local events in "my-book.lisp" and then may load the compiled code
for the non-local functions defined in that file.  Checks are made to
ensure that the certificate file exists and describes the version of
"my-book.lisp" that is read.  The compiled code is loaded if and only
if it exists and has a later write date than the source file (but see
COMPILATION for an exception).

Since include-book is itself an event, you may put such forms into
other books.  Thus it is possible for the inclusion of a single book to
lead to the inclusion of many others.  The check sum information
maintained in certificates helps deal with the version control problem
of the referenced books.  I.e., if this version of "my-book" is used
during the certification of "your-book", then the certificate for
"your-book" includes the check sum of this version of "my-book".  If a
later (include-book "your-book") finds a version of "my-book" with a
different check sum, an error is signalled.  But check sums are not
perfect and the insecurity of the host file system prevents ACL2 from
guaranteeing the logical soundness of an include-book event, even for a
book that appears to have a valid certificate (they can be forged,
after all).  (See CERTIFICATE for further discussion.)

This concludes the example of how to create, certify and use a book.
If you wish, you could now review the documentation for book-related
topics (see BOOKS) and browse through them.  They'll probably
make sense in this context.  Alternatively, you could continue the
"guided tour" through the rest of the documentation of books.  See
BOOK-NAME, following the pointer given at the conclusion.

BOOK-MAKEFILES    makefile support provided with the ACL2 distribution

This topic describes the ACL2 methodology for using makefiles to assist
in the automation of the certification of collections of ACL2 books.  We
assume here a familiarity with Unix/Linux make.  We also assume that you
are using GNU make rather than some other flavor of make.

ACL2's regression suite is run using Makefiles that include
books/Makefile-generic.  You can look at existing Makefiles to
understand how to create your own Makefiles.  Here are the six steps to
follow to create a Makefile for a directory that contains books to be
certified, and certify them using that Makefile.  Below these steps we
conclude with discussion of other capabilties provided by
books/Makefile-generic.

1. Define the ACL2 variable using ?= to point to your ACL2 executable
(though this may be omitted for directories directly under the
distributed books directory).  Also include the file Makefile-generic
in the distributed books directory.  For example, file
books/arithmetic-3/pass1/Makefile starts as follows.

     ACL2 ?= ../../../saved_acl2
     include ../../Makefile-generic

(For Makefile experts: we define ACL2 using ?= instead of with = or :=
because of the protocol used by the ACL2 make system: command-line
values are passed explicitly with recursive calls of make to override
the Makefile values of ACL2, which in turn need to be able to override
the environment value of ACL2 from books/Makefile-generic).

2. (Optional; usually skipped.)  Set the INHIBIT variable if you want to
see more than the summary output.  For example, if you want to see the
same output as you would normally see at the terminal, put this line in
your Makefile after the `ACL2 ?=' and ~c[include]' lines.

     INHIBIT = (assign inhibit-output-lst (list (quote proof-tree)))

For other values to use for INHIBIT, see SET-INHIBIT-OUTPUT-LST
and see the original setting of INHIBIT in books/Makefile-generic.

3. Specify the books to be certified.  If every file with extension
.lisp is a book that you want to certify, you can skip this step.
Otherwise, put a line in your Makefile after the ones above that
specifies the books to be certified.  The following example, from an
old version of books/finite-set-theory/osets/Makefile, should make this
clear.

     BOOKS = computed-hints fast instance map membership outer primitives \
             quantify set-order sets sort

But better yet, use the extension .lsp for any Lisp or ACL2 files that
are not to be certified, so that the definition of BOOKS can be omitted.

4. Create .acl2 files for books that are to be certified in other than
the initial ACL2 world (see PORTCULLIS).  For example, if you
look in books/arithmetic/equalities.acl2 you will see defpkg forms
followed by a certify-book command, because it was determined that
defpkg forms were necessary in the certification world in order to
certify the equalities book.  In general, for each <book-name>.lisp
whose certification requires a non-initial certification world, you
will need a corresponding <book-name>.acl2 file that ends with the
appropriate certify-book command.  Of course, you can also use .acl2
files with initial certification worlds, for example if you want to
pass optional arguments to certify-book.

You also have the option of creating a file cert.acl2 that has a special
role.  When file <book-name>.lisp is certified, if there is no file
<book-name>.acl2 but there is a file cert.acl2, then cert.acl2 will be
used as <book-name>.acl2 would have been used, as described in the
preceding paragraph, except that the appropriate certify-book command
will be generated automatically -- no certify-book command should occur
in cert.acl2.

It is actually allowed to put raw lisp forms in a .acl2 file (presumably
preceded by :q or (value :q) and followed by (lp)).  But this is not
recommended; we make no guarantees about certification performed any
time after raw Lisp has been entered in the ACL2 session.

5. Generally, the next step is to include the following line after the
`include' of Makefile-generic (see the first step above).

     -include Makefile-deps

This will cause `make' to create and then include a file Makefile-deps
that contains "dependency" lines needed by make.  If those dependencies
are somehow flawed, it may be because you have include-book forms that
are not truly including books, for example in multi-line comments
(#|..|#).  These will be ignored if preceded by a semicolon (;), or if
you add a line break after "include-book."  But instead, you can create
dependency lines yourself by running the command

     make dependencies

and pasting the result into the end of your Makefile, and editing as you
see fit.

6. Run make.  This will generate a <book-name>.out file for each
<book-name>.lisp file being certified, which is the result of
redirecting ACL2's standard output.  Note that make will stop at the
first failure, but you can use make -i to force make to continue past
failures.  You can also use the -j option to speed things up if you
have a multi-core machine, e.g., make -j 8 in a book directory or, if
in the ACL2 sources directory, make -j 8 regression.

This concludes the basic instructions for creating a Makefile in a
directory including books.  Here are some other capabilities offered by
books/Makefile-subdirs.

*Subdirectory support.*  There is support for subdirectories.  For
example, file books/arithmetic-3/Makefile formerly had the following
contents.

     DIRS = pass1 bind-free floor-mod
     include ../Makefile-subdirs

This indicated that we are to run make in subdirectories pass1/,
bind-free/, and floor-mod of the current directory (namely,
books/arithmetic-3/).

However, there is also subdirectory support when the current directory
has books as well.  Here are the contents of
books/arithmetic-3/Makefile as of ACL2 Version_3.2.

     ACL2 = ../../saved_acl2

     arith-top: top all
     all: top

     DIRS = pass1 bind-free floor-mod
     include ../Makefile-subdirs
     include ../Makefile-generic

     top.cert: top.lisp
     top.cert: bind-free/top.cert
     top.cert: floor-mod/floor-mod.cert
     top.cert: floor-mod/mod-expt-fast.cert

The first line is optional because ../../saved_acl2 is the default and
the directory is a sub-sub-directory of the distribution directory; but
it is harmless to include this line.  The other additional lines
support certifying books in the subdirectories before certifying the
books in the present directory, in the customary make style.

Specifically, the top target is defined in ../Makefile-subdirs to call
make in each subdirectory in DIRS.  We have set the default target in
the example above to a new name, arith-top, that makes that top target
before making the all target.  The all target, in turn, is the top
(default) target in ../Makefile-generic, and is responsible for
certifying books in the current directory.

Use Makefile-psubdirs instead of Makefile-subdirs if certification of a
book in a subdirectory never depends on certification of a book in a
different subdirectory, because then make's -j option can allow
subdirectories to be processed in parallel.

*Cleaning up.*  We note that there is a clean target.  Thus,

     make clean

will remove all .cert files, files resulting from compilation, and other
"junk"; see the full list under "clean:" in books/Makefile-generic.

*System books.*  The environment variable ACL2_SYSTEM_BOOKS can be set
to the books/ directory under which the books reside that are
distributed with ACL2.  A Unix-style pathname, typically ending in
books/ or books, is permissible.  In most cases, your ACL2 executable
is a small script in which you can set this environment variable just
above the line on which the actual ACL2 image is invoked, for example:

     export ACL2_SYSTEM_BOOKS
     ACL2_SYSTEM_BOOKS=/home/acl2/v3-2/acl2-sources/books

However, you can also set ACL2_SYSTEM_BOOKS as a make variable, by
setting it in your Makefile before the first target definition, e.g.:

     ACL2_SYSTEM_BOOKS = /home/acl2/v3-2/acl2-sources/books

*Compilation support.*  Finally, books/Makefile-generic provides
support for compiling books that are already certified (but see
COMPILATION for an exception).  For example, suppose that you have
certified books in GCL, resulting in compiled files with the .o
extension.  Now suppose you would like to compile the books for Allegro
Common Lisp, whose compiled files have the .fasl extension.  The
following command will work if you have included books/Makefile-generic
in your Makefile.

     make fasl

In general, the compiled file extension for a Lisp supported by ACL2
will be a target name for building compiled files for all your books
(after certifying the books, if not already up-to-date on
certification).

BOOK-NAME    conventions associated with book names

     Examples:
     "list-processing"
     "/usr/home/smith/my-arith"

Book names are string constants that can be elaborated into file names.
We elaborate book names by concatenating the "connected book
directory" (see CBD) string on the left and some "extension,"
such as ".lisp", on the right.  However, the connected book directory
is not added if the book name itself already represents an absolute
file name.  Furthermore, include-book and certify-book temporarily
reset the connected book directory to be the directory of the book
being processed.  This allows include-book forms to use file names
without explicit mention of the enclosing book's directory.  This in
turn allows books (together with those that they include, using
include-book) to be moved between directories while maintaining their
certification and utility.

You may wish to read elsewhere for details of ACL2 file name
conventions (see PATHNAME), for a discussion of the filename
that is the result of the elaboration described here (see
FULL-BOOK-NAME), and for details of the concept of the connected book
directory (see CBD).  For details of how include-book (see
INCLUDE-BOOK) and certify-book (see CERTIFY-BOOK) use
these concepts, see below.

Often a book name is simply the familiar name of the file.  (See
FULL-BOOK-NAME for discussion of the notions of "directory string,"
"familiar name," and "extension".  These concepts are not on the guided
tour through books and you should read them separately.)  However, it
is permitted for book names to include a directory or part of a
directory name.  Book names never include the extension, since ACL2
must routinely tack several different extensions onto the name during
include-book.  For example, include-book uses the ".lisp", ".cert" and
possibly the ".o" or ".lbin" extensions of the book name.

Book names are elaborated into full file names by include-book and
certify-book.  This elaboration is sensitive to the "connected book
directory." The connected book directory is an absolute filename string
(see PATHNAME) that is part of the ACL2 state.  (You may wish
to see CBD and to see SET-CBD -- note that these are
not on the guided tour).  If a book name is an absolute filename
string, ACL2 elaborates it simply by appending the desired extension to
the right.  If a book name is a relative filename string, ACL2 appends
the connected book directory on the left and the desired extension on
the right.

Note that it is possible that the book name includes some partial
specification of the directory.  For example, if the connected book
directory is "/usr/home/smith/" then the book name
"project/task-1/arith" is a book name that will be elaborated to

     "/usr/home/smith/project/task-1/arith.lisp".

Observe that while the events in this "arith" book are being processed
the connected book directory will temporarily be set to

     "/usr/home/smith/project/task-1/".

Thus, if the book requires other books, e.g.,

     (include-book "naturals")

then it is not necessary to specify the directory on which they reside
provided that directory is the same as the superior book.

This inheritance of the connected book directory and its use to
elaborate the names of inferior books makes it possible to move books
and their inferiors to new directories, provided they maintain the same
relative relationship.  It is even possible to move with ease whole
collections of books to different filesystems that use a different
operating system than the one under which the original certification
was performed.

The ".cert" extension of a book, if it exists, is presumed to contain
the most recent certificate for the book.  See CERTIFICATE (or,
if you are on the guided tour, wait until the tour gets there).

See BOOK-CONTENTS to continue the guided tour.

CBD    connected book directory string

     Example:
     ACL2 !>:cbd
     "/usr/home/smith/"

The connected book directory is a nonempty string that specifies a
directory as an absolute pathname.  (See PATHNAME for a
discussion of file naming conventions.)  When include-book is given a
relative book name it elaborates it into a full book name, essentially
by appending the connected book directory string to the left and
".lisp" to the right.  (For details, see BOOK-NAME and also see
FULL-BOOK-NAME.)  Furthermore, include-book temporarily sets
the connected book directory to the directory string of the resulting
full book name so that references to inferior books in the same
directory may omit the directory.  See SET-CBD for how to set
the connected book directory string.

     General Form:
     (cbd)

This is a macro that expands into a term involving the single free
variable state.  It returns the connected book directory string.

The connected book directory (henceforth called the "cbd") is used by
include-book to elaborate the supplied book name into a full book name
(see FULL-BOOK-NAME).  For example, if the cbd is
"/usr/home/smith/" then the elaboration of the book-name
"project/task-1/arith" (to the ".lisp" extension) is
"/usr/home/smith/project/task-1/arith.lisp".  That full-book-name is
what include-book opens to read the source text for the book.

The cbd may be changed using set-cbd (see SET-CBD).
Furthermore, during the processing of the events in a book,
include-book sets the cbd to be the directory string of the
full-book-name of the book.  Thus, if the cbd is "/usr/home/smith/"
then during the processing of events by

     (include-book "project/task-1/arith")

the cbd will be set to "/usr/home/smith/project/task-1/".  Note that if
"arith" recursively includes a subbook, say "naturals", that resides on
the same directory, the include-book event for it may omit the
specification of that directory.  For example, "arith" might contain
the event

       (include-book "naturals").

In general, suppose we have a superior book and several inferior books
which are included by events in the superior book.  Any inferior book
residing on the same directory as the superior book may be referenced
in the superior without specification of the directory.

We call this a "relative" as opposed to "absolute" naming.  The use of
relative naming is preferred because it permits books (and their
accompanying inferiors) to be moved between directories while
maintaining their certificates and utility.  Certified books that
reference inferiors by absolute file names are unusable (and rendered
uncertified) if the inferiors are moved to new directories.

_Technical Note and a Challenge to Users:_

After elaborating the book name to a full book name, include-book opens
a channel to the file to process the events in it.  In some host Common
Lisps, the actual file opened depends upon a notion of "connected
directory" similar to our connected book directory.  Our intention in
always elaborating book names into absolute filename strings (see
PATHNAME for terminology) is to circumvent the sensitivity to the
connected directory.  But we may have insufficient control over this
since the ultimate file naming conventions are determined by the host
operating system rather than Common Lisp (though, we do check that the
operating system "appears" to be one that we "know" about).  Here is a
question, which we'll pose assuming that we have an operating system
that calls itself "Unix."  Suppose we have a file name, filename, that
begins with a slash, e.g., "/usr/home/smith/...".  Consider two
successive invocations of CLTL's

     (open filename :direction :input)

separated only by a change to the operating system's notion of
connected directory.  Must these two invocations produce streams to the
same file?  A candidate string might be something like
"/usr/home/smith/*/usr/local/src/foo.lisp" which includes some
operating system-specific special character to mean "here insert the
connected directory" or, more generally, "here make the name dependent
on some non-ACL2 aspect of the host's state."  If such "tricky" name
strings beginning with a slash exist, then we have failed to isolate
ACL2 adequately from the operating system's file naming conventions.
Once upon a time, ACL2 did not insist that the cbd begin with a slash
and that allowed the string "foo.lisp" to be tricky because if one were
connected to "/usr/home/smith/" then with the empty cbd "foo.lisp" is a
full book name that names the same file as "/usr/home/smith/foo.lisp".
If the actual file one reads is determined by the operating system's
state then it is possible for ACL2 to have two distinct "full book
names" for the same file, the "real" name and the "tricky" name.  This
can cause ACL2 to include the same book twice, not recognizing the
second one as redundant.

CERTIFICATE    how a book is known to be admissible and where its defpkgs reside

A book, say "arith", is said to have a "certificate" if there is a file
named "arith.cert".  Certificates are created by the function
certify-book and inspected by include-book.  Check sums are used to
help ensure that certificates are legitimate and that the corresponding
book has not been modified since certification.  But because the file
system is insecure and check sums are not perfect it is possible for
the inclusion of a book to cause inconsistency even though the book
carries an impeccable certificate.

The certificate includes the version number of the certifying ACL2.  A
book is considered uncertified if it is included in an ACL2 with a
different version number.

The presence of a "valid" certificate file for a book attests to two
things: all of the events of the book are admissible in a certain
extension of the initial ACL2 logic, and the non-local events of the
book are independent of the local ones (see
LOCAL-INCOMPATIBILITY).  In addition, the certificate contains the
commands used to construct the world in which certification occurred.
Among those commands, of course, are the defpkgs defining the packages
used in the book.  When a book is included into a host world, that
world is first extended by the commands listed in the certificate for
the book.  Unless that causes an error due to name conflicts, the
extension ensures that all the packages used by the book are
identically defined in the host world.

_Security:_

Because the host file system is insecure, there is no way ACL2 can
guarantee that the contents of a book remain the same as when its
certificate was written.  That is, between the time a book is certified
and the time it is used, it may be modified.  Furthermore, certificates
can be counterfeited.  Check sums (see CHECK-SUM) are used to
help detect such problems.  But check sums provide imperfect security:
two different files can have the same check sum.

Therefore, from the strictly logical point of view, one must consider
even the inclusion of certified books as placing a burden on the user:

     The non-erroneous inclusion of a certified book is consistency
     preserving provided (a) the objects read by include-book from the
     certificate were the objects written there by a certify-book and
     (b) the forms read by include-book from the book itself are the
     forms read by the corresponding certify-book.

We say that a given execution of include-book is "certified" if a
certificate file for the book is present and well-formed and the check
sum information contained within it supports the conclusion that the
events read by the include-book are the ones checked by certify-book.
When an uncertified include-book occurs, warnings are printed or errors
are caused.  But even if no warning is printed, you must accept burdens
(a) and (b) if you use books.  These burdens are easier to live with if
you protect your books so that other users cannot write to them, you
abstain from running concurrent ACL2 jobs, and you abstain from
counterfeiting certificates.  But even on a single user uniprocessor,
you can shoot yourself in the foot by using the ACL2 io primitives to
fabricate an inconsistent book and the corresponding certificate.

Note that part (a) of the burden described above implies, in
particular, that there are no guarantees when a certificate is copied.
When books are renamed (as by copying them), it is recommended that
their certificates be removed and the books be recertified.  The
expectation is that recertification will go through without a hitch if
relative pathnames are used.  See PATHNAME, which is not on the
guided tour.

Certificates essentially contain two parts, a portcullis and a keep.
There is a third part, an expansion-alist, in order to record
expansions if make-event has been used, but the user need not be
concerned with that level of detail.

See PORTCULLIS to continue the guided tour through books.

CERTIFY-BOOK    how to produce a certificate for a book

     Examples:
     (certify-book "my-arith")        ; certify in a world with 0 commands
     (certify-book "my-arith" 3)      ; ... in a world with 3 commands
     (certify-book "my-arith" ?)      ; ... in a world without checking the
                                        ;     number of commands
     (certify-book "my-arith" 0 nil)  ; ... do not compile
     (certify-book "my-arith" 0 t)    ; ... compile (default)
     (certify-book "my-arith" 0 :raw) ; ... compile except for exececutable
                                        ;     counterparts
     (certify-book "my-arith" 0 t :ttags (foo))
                                        ; ... allow trust tag (ttag) foo
     (certify-book "my-arith" 0 t :ttags :all)
                                        ; ... allow all trust tags (ttags)
     (certify-book "my-arith" t)      ; certify from world of old certificate

     General Form:
     (certify-book book-name k compile-flg
                   :defaxioms-okp t/nil        ; [default nil]
                   :skip-proofs-okp t/nil      ; [default nil]
                   :save-expansion :save/t/nil ; [default nil]
                   :ttags ttags                ; [default nil]
                   )

where book-name is a book name (see BOOK-NAME), k is either t or
an integer used to indicate your approval of the "certification world."
Compile-flg indicates whether you wish to compile the (functions in
the) book.  Compile-flg generally defaults to t, meaning to compile;
nil means do not compile.  However, if explicit compilation is
suppressed then compile-flg is coerced to nil; see COMPILATION.
Otherwise, if compile-flg is not supplied but environment variable
ACL2_COMPILE_FLG is defined, then after its string value is coerced to
upper-case, compile-flg is considered to have value t if that string is
"T", nil if that string is "NIL", and :all if that string is "ALL";
otherwise it is an error.

The second argument k is optional as well; it defaults to 0.

Two keyword arguments, :defaxioms-okp and :skip-proofs-okp, determine
how the system handles the inclusion of defaxiom events and skip-proofs
events, respectively, in the book.  The value t allows such events, but
prints a warning message.  The value nil is the default, and causes an
error if such an event is found.

The keyword argument :ttags may normally be omitted.  A few constructs,
used for example if you are building your own system based on ACL2, may
require it.  See DEFTTAG for an explanation of this argument.

If you use guards, please note certify-book is executed as though
(set-guard-checking nil) has been evaluated; see
SET-GUARD-CHECKING.  If you want guards checked, consider using ld
instead, or in addition; see LD.

To advanced users only: in the rare case that you are want to save
compilation time and space in return for skipping compilation of the
executable counterparts of functions defined in the book, you may supply
a value of :raw for compile-flg.  The default setting of t is however
recommended for any book whose functions are called during
macroexpansion, because evaluation during macroexpansion is done in a
"safe mode" that avoids calling raw Lisp functions (see
GUARDS-AND-EVALUATION).  (The setting :all is allowed as an alias for
t, for legacy reasons.)

The keyword argument :save-expansion controls whether or not a so-called
"book expansion" file is written, obtained by appending the string
"@expansion.lsp" to the end of the book name.  See MAKE-EVENT
for discussion of the book expansion; in a nutshell, make-event calls
generate forms that replace them in the book expansion.  Book expansion
is skipped if compile-flg and :save-expansion are both nil.  Otherwise,
the values of nil and t for :save-expansion cause the book expansion to
be created only when a make-event form occurs in a book (i.e., only if
there is some expansion), or if at least one executable counterpart is
to be compiled (see preceding paragraph).  If the book expansion is
created, then it is deleted after compilation if :save-expansion is
nil.  Finally, if :save-expansion is :save, then the book expansion
file is created in all cases, and is not deleted.

For a general discussion of books, see BOOKS.  Certify-book is
akin to what we have historically called a "proveall": all the forms in
the book are "proved" to guarantee their admissibility.  More
precisely, certify-book (1) reads the forms in the book, confirming
that the appropriate packages are defined in the certification world;
(2) does the full admissibility checks on each form (proving
termination of recursive functions, proving theorems, etc.), checking
as it goes that each form is an embedded event form (see
EMBEDDED-EVENT-FORM); (3) rolls the world back to the initial
certification world and does an include-book of the book to check for
local incompatibilities (see LOCAL-INCOMPATIBILITY); (4) writes
a certificate recording not only that the book was certified but also
recording the commands necessary to recreate the certification world (so
the appropriate packages can be defined when the book is included in
other worlds) and the check sums of all the books involved (see
CERTIFICATE); (5) compiles the book if so directed (and then loads
the object file in that case).  The result of executing a certify-book
command is the creation of a single new event, which is actually an
include-book event.  If you don't want its included events in your
present world, simply execute :ubt :here afterwards.

Certify-book requires that the default defun-mode (see
DEFAULT-DEFUN-MODE) be :logic when certification is attempted.  If
the mode is not :logic, an error is signalled.

An error will occur if certify-book has to deal with any uncertified
book other than the one on which it was called.  For example, if the
book being certified includes another book, that subbook must already
have been certified.

Certification occurs in some logical world, called the "certification
world." That world must contain the defpkgs needed to read and execute
the forms in the book.  The commands necessary to recreate that world
from the ACL2 initial world will be copied into the certificate created
for the book.  Those commands will be re-executed whenever the book is
included, to ensure that the appropriate packages (and all other names
used in the certification world) are correctly defined.  The certified
book will be more often usable if the certification world is kept to a
minimal extension of the ACL2 initial world.  Thus, before you call
certify-book for the first time on a book, you should get into the
initial ACL2 world (e.g., with :ubt 1 or just starting a new version of
ACL2), defpkg the desired packages, and then invoke certify-book.

The k argument to certify-book must be either a nonnegative integer or
else one of the symbols t or ? in the ACL2 package.  If k is an
integer, then it must be the number of commands that have been executed
after the initial ACL2 world to create the world in which certify-book
was called.  One way to obtain this number is by doing :pbt :start to
see all the commands back to the first one.

If k is t it means that certify-book should use the same world used in
the last certification of this book.  K may be t only if you call
certify-book in the initial ACL2 world and there is a certificate on
file for the book being certified.  (Of course, the certificate is
probably invalid.)  In this case, certify-book reads the old
certificate to obtain the portcullis commands and executes them to
recreate the certification world.

Finally, k may be ?, in which case there is no check made on the
certification world.  That is, if k is ? then no action related to the
preceding two paragraphs is performed, which can be a nice convenience
but at the cost of eliminating a potentially valuable check that the
certification world may be as expected.

If you have a certified book that has remained unchanged for some time
you are unlikely even to remember the appropriate defpkgs for it.  If
you begin to change the book, don't throw away its certificate file
just because it has become invalid!  It is an important historical
document until the book is re-certified.

When certify-book is directed to produce a compiled file, it calls the
Common Lisp function compile-file on the original source file.  This
creates a compiled file with an extension known to ACL2, e.g., if the
book is named "my-book" then the source file is "my-book.lisp" and the
compiled file under GCL will be "my-book.o" while under SBCL it will be
"my-book.fasl".  The compiled file is then loaded.  When include-book
is used later on "my-book" it will automatically load the compiled
file, provided the compiled file has a later write date than the source
file.  The only effect of such compilation and loading is that the
functions defined in the book execute faster.  See GUARD for a
discussion of the issues.

When certify-book is directed not to produce a compiled file, it will
delete any existing compiled file for the book, so as not to mislead
include-book into loading the now outdated compiled file.

After execution of a certify-book form, the value of
acl2-defaults-table is restored to what it was immediately before that
certify-book form was executed.  See ACL2-DEFAULTS-TABLE.

This completes the tour through the documentation of books.

FULL-BOOK-NAME    book naming conventions assumed by ACL2

For this discussion we assume that the resident operating system is
Unix (trademark of AT&T), but analogous remarks apply to other
operating systems supported by ACL2, in particular, the Macintosh
operating system where `:' plays roughly the role of `/' in Unix; see
PATHNAME.

ACL2 defines a "full book name" to be an "absolute filename string,"
that may be divided into contiguous sections:  a "directory string", a
"familiar name" and an "extension".  See PATHNAME for the
definitions of "absolute," "filename string," and other notions
pertaining to naming files.  Below we exhibit the three sections of one
such string:

     "/usr/home/smith/project/arith.lisp"

     "/usr/home/smith/project/"           ; directory string
                             "arith"      ; familiar name
                                  ".lisp" ; extension

The sections are marked by the rightmost slash and rightmost dot, as
shown below.

     "/usr/home/smith/project/arith.lisp"
                             |     |
                             slash dot
                             |     |
     "/usr/home/smith/project/"           ; directory string
                             "arith"      ; familiar name
                                  ".lisp" ; extension

The directory string includes (and terminates with) the rightmost
slash.  The extension includes (and starts with) the rightmost dot.
The dot must be strictly to the right of the slash so that the familiar
name is well-defined and nonempty.

If you are using ACL2 on a system in which file names do not have this
form, please contact the authors and we'll see what we can do about
generalizing ACL2's conventions.

KEEP    how we know if include-book read the correct files

The certificate (see CERTIFICATE for general information) of a
certified file is divided into two parts, a portcullis and a keep.
These names come from castle lore.  The keep is the strongest and
usually tallest tower of a castle from which the entire courtyard can
be surveyed by the defenders.  The keep of a book is a list of file
names and check sums used after the book has been included, to
determine if the files read were (up to check sum) those certified.

Once the portcullis is open, include-book can enter the book and read
the event forms therein.  The non-local event forms are in fact
executed, extending the host theory.  That may read in other books.
When that has been finished, the keep of the certificate is inspected.
The keep is a list of the book names which are included (hereditarily
through all subbooks) in the certified book (including the certified
book itself) together with the check sums of the objects in those books
at the time of certification.  We compare the check sums of the books
just included to the check sums of the books stored in the keep.  If
differences are found then we know that the book or one of its subbooks
has been changed since certification.

See INCLUDE-BOOK to continue the guided tour through books.

MAKEFILES    See BOOK-MAKEFILES.

PATHNAME    introduction to filename conventions in ACL2

The notion of pathname objects from Common Lisp is not supported in
ACL2, nor is the function pathname.  However, ACL2 supports file
operations, using conventions for naming files based on those of the
Unix (trademark of AT&T) operating system, so that the character / is
used to terminate directory names.  Some file names are "absolute"
(complete) descriptions of a file or directory; others are "relative"
to the current working directory or to the connected book directory
(see CBD).  We emphasize that even for users of Windows-based
systems or Macintosh computers, ACL2 file names are in the Unix style.
We will call these _ACL2 pathnames_, often omitting the "ACL2."

Pathnames starting with the directory separator (/) or the tilde
character (~) are absolute pathnames.  All other pathnames are relative
pathnames.  An exception is in the Microsoft Windows operating system,
where it is illegal for the pathname to start with a tilde character
but the drive may be included, e.g., "c:/home/smith/acl2/book-1.lisp".
In fact, the drive _must_ be included in the portcullis of a book; see
PORTCULLIS.  Note also that some host Common Lisps will not
support pathnames starting with "~", for example ~smith, though ACL2
will generally support those starting with "~/" regardless of the host
Common Lisp.

Consider the following examples.  The filename string

     "/home/smith/acl2/book-1.lisp"

is an absolute pathname, with top-level directory "home", under that
the directory "smith" and then the directory "acl2", and finally,
within that directory the file "book-1.lisp".  If the connected book
directory is "/home/smith/" (see CBD), then the filename string
above also corresponds to the relative filename string
"acl2/book1.lisp".

Finally, we note that (on non-Windows systems) the pathname "~" and
pathnames starting with "~/" are illegal in books being certified.
Otherwise, a subsidiary include-book form would have a different
meaning at certification time than at a later time when the certified
book is included by a different user.

PORTCULLIS    the gate guarding the entrance to a certified book

The certificate (see CERTIFICATE for general information) of a
certified file is divided into two parts, a portcullis and a keep.
These names come from castle lore.  The portcullis of a castle is an
iron grate that slides up through the ceiling of the tunnel-like
entrance.  The portcullis of a book ensures that include-book does not
start to read the book until the appropriate context has been created.

Technically, the portcullis consists of the version number of the
certifying ACL2, a list of commands used to create the "certification
world" and an alist specifying the check sums of all the books included
in that world.  The portcullis is constructed automatically by
certify-book from the world in which certify-book is called, but that
world must have certain properties described below.  After listing the
properties we discuss the issues in a more leisurely manner.

Each command in the portcullis must be either a defpkg form or an
embedded event form (see EMBEDDED-EVENT-FORM).

Consider a book to be certified.  The book is a file containing event
forms.  Suppose the file contains references to such symbols as
my-pkg::fn and acl2-arith::cancel, but that the book itself does not
create the packages.  Then a hard Lisp error would be caused merely by
the attempt to read the expressions in the book.  The corresponding
defpkgs cannot be written into the book itself because the book must be
compilable and Common Lisp compilers differ on the rules concerning the
inline definition of new packages.  The only safe course is to make all
defpkgs occur outside of compiled files.

More generally, when a book is certified it is certified within some
logical world.  That "certification world" contains not only the
necessary defpkgs but also, perhaps, function and constant definitions
and maybe even references to other books.  When certify-book creates
the certificate for a file it recovers from the certification world the
commands used to create that world from the initial ACL2 world.  Those
commands become part of the portcullis for the certified book.  In
addition, certify-book records in the portcullis the check sums (see
CHECK-SUM) of all the books included in the certification world.

Include-book presumes that it is impossible even to read the contents
of a certified book unless the portcullis can be "raised." To raise the
portcullis we must be able to execute (possibly redundantly, but
certainly without error), all of the commands in the portcullis and
then verify that the books thus included were identical to those used
to build the certification world (up to check sum).  This raising of
the portcullis must be done delicately since defpkgs are present: we
cannot even read a command in the portcullis until we have successfully
executed the previous ones, since packages are being defined.

Clearly, a book is most useful if it is certified in the most
elementary extension possible of the initial logic.  If, for example,
your certification world happens to contain a defpkg for "MY-PKG" and
the function foo, then those definitions become part of the portcullis
for the book.  Every time the book is included, those names will be
defined and will have to be either new or redundant (see
REDUNDANT-EVENTS).  But if those names were not necessary to the
certification of the book, their presence would unnecessarily restrict
the utility of the book.

See KEEP to continue the guided tour of books.

SET-CBD    to set the connected book directory

     Example Forms:
     ACL2 !>:set-cbd "/usr/home/smith/"
     ACL2 !>:set-cbd "my-acl2/books"

See CBD for a description of the connected book directory.

     General Form:
     (set-cbd str)

where str is a nonempty string that represents the desired directory
(see PATHNAME).  This command sets the connected book directory
(see CBD) to the string representing the indicated directory.
Thus, this command may determine which files are processed by
include-book and certify-book commands typed at the top-level.
However, the cbd is also temporarily set by those two book processing
commands.

IMPORTANT:  Pathnames in ACL2 are in the Unix (trademark of AT&T)
style.  That is, the character "/" separates directory components of a
pathname, and pathnames are absolute when they start with this
character, and relative otherwise.  See PATHNAME.

UNCERTIFIED-BOOKS    invalid certificates and uncertified books

Include-book has a special provision for dealing with uncertified
books: If the file has no certificate or an invalid certificate (i.e.,
one whose check sums describe files other than the ones actually read),
a warning is printed and the book is otherwise processed as though it
were certified and had an open portcullis.  (For details see
BOOKS, see CERTIFICATE, and see PORTCULLIS.)

This can be handy, but it can have disastrous consequences.

The provision allowing uncertified books to be included can have
disastrous consequences, ranging from hard lisp errors, to damaged
memory, to quiet logical inconsistency.

It is possible for the inclusion of an uncertified book to render the
logic inconsistent.  For example, one of its non-local events might be
(defthm t-is-nil (equal t nil)).  It is also possible for the inclusion
of an uncertified book to cause hard errors or breaks into raw Common
Lisp.  For example, if the file has been edited since it was certified,
it may contain too many open parentheses, causing Lisp to read past
"end of file." Similarly, it might contain non-ACL2 objects such as
3.1415 or ill-formed event forms that cause ACL2 code to break.

Even if a book is perfectly well formed and could be certified (in a
suitable extension of ACL2's initial world), its uncertified inclusion
might cause Lisp errors or inconsistencies!  For example, it might
mention packages that do not exist in the host world.  The portcullis
of a certified book ensures that the correct defpkgs have been
admitted, but if a book is read without actually raising its
portcullis, symbols in the file, e.g., acl2-arithmetic::fn, could cause
"unknown package" errors in Common Lisp.  Perhaps the most subtle
disaster occurs if the host world does have a defpkg for each package
used in the book but the host defpkg imports different symbols than
those required by the portcullis.  In this case, it is possible that
formulas which were theorems in the certified book are non-theorems in
the host world, but those formulas can be read without error and will
then be quietly assumed.

In short, if you include an uncertified book, *all bets are off*
regarding the validity of the future behavior of ACL2.

That said, it should be noted that ACL2 is pretty tough and if errors
don't occur, the chances are that deductions after the inclusion of an
uncertified book are probably justified in the (possibly inconsistent)
logical extension obtained by assuming the admissibility and validity
of the definitions and conjectures in the book.

BREAK-REWRITE    the read-eval-print loop entered to monitor rewrite rules

ACL2 allows the user to monitor the application of rewrite rules.  When
monitored rules are about to be tried by the rewriter, an interactive
break occurs and the user is allowed to watch and, in a limited sense,
control the attempt to apply the rule.  This interactive loop, which is
technically just a call of the standard top-level ACL2 read-eval-print
loop, ld, on a "wormhole state" (see WORMHOLE), is called
"break-rewrite."  While in break-rewrite, certain keyword commands are
available for accessing information about the context in which the
lemma is being tried.  These keywords are called break-rewrite
"commands."

Also see DMR (Dynamically Monitor Rewrites) for a related
utility, which allows you to watch progress of the rewriter in real
time.

To abort from inside break-rewrite at any time, execute

For further information, see the related :doc topics listed below.

Related topics other than immediate subtopics:

As explained in the documentation for monitor, it is possible to cause
the ACL2 rewriter to monitor the attempted application of selected
rules.  When such a rule is about to be tried, the rewriter evaluates
its break condition and if the result is non-nil, break-rewrite is
entered.

Break-rewrite permits the user to inspect the current state by
evaluating break-rewrite commands.  Type :help in break-rewrite to see
what the break-rewrite commands are.  However, break-rewrite is
actually just a call of the general ACL2 read-eval-print loop, ld, on a
certain state and the break-rewrite commands are simply aliases
provided by the ld-special ld-keyword-aliases.  See LD for
details about this read-eval-print loop.  Thus, with a few exceptions,
anything you can do at the ACL2 top-level can be done within
break-rewrite.  For example, you can evaluate arbitrary expressions,
use the keyword command hack, access documentation, print events, and
even define functions and prove theorems.  However, the "certain state"
upon which ld was called is a "wormhole state" (see WORMHOLE)
because break-rewrite is not allowed to have any effect upon the
behavior of rewrite.  What this means, very roughly but understandably,
is that break-rewrite operates on a copy of the state being used by
rewrite and when break-rewrite exits the wormhole closes and the state
"produced" by break-rewrite disappears.  Thus, break-rewrite lets you
query the state of the rewriter and even do experiments involving
proofs, etc., but these experiments have no effect on the ongoing proof
attempt.

When you first enter break-rewrite a simple herald is printed such as:

     (3 Breaking (:rewrite lemma12) on (delta a (+ 1 j)):

The integer after the open parenthesis indicates the depth of nested
break-rewrite calls.  In this discussion we use 3 consistently for this
integer.  Unless you abort or somehow enter unbalanced parentheses into
the script, the entire session at a given depth will be enclosed in
balanced parentheses, making it easy to skip over them in Emacs.

You then will see the break-rewrite prompt:

     3 ACL2 !>

The leading integer is, again, the depth.  Because breaks often occur
recursively it is convenient always to know the level with which you
are interacting.

You may type arbitrary commands as in the top-level ACL2 loop.  For
example, you might type:

     3 ACL2 !>:help

or

     3 ACL2 !>:pe lemma12

More likely, upon entering break-rewrite you will determine the context
of the attempted application.  Here are some useful commands:

     3 ACL2 >:target           ; the term being rewritten
     3 ACL2 >:unify-subst      ; the unifying substitution
     3 ACL2 >:path             ; the stack of goals pursued by the rewriter
                               ; starting at the top-level clause being simplified
                               ; and ending with the current application

At this point in the interaction the system has not yet tried to apply
the monitored rule.  That is, it has not tried to establish the
hypotheses, considered the heuristic cost of backchaining, rewritten
the right-hand side of the conclusion, etc.  When you are ready for it
to try the rule you can type one of several different "proceed"
commands.  The basic proceed commands are :ok, :go, and :eval.

     :ok

exits break-rewrite without further interaction.  When break-rewrite
exits it prints "3)", closing the parenthesis that opened the level 3
interaction.

     :go

exits break-rewrite without further interaction, but prints out the
result of the application attempt, i.e., whether the application
succeeded, if so, what the :target term was rewritten to, and if not
why the rule was not applicable.

     :eval

causes break-rewrite to attempt to apply the rule but interaction at
this level of break-rewrite resumes when the attempt is complete.  When
control returns to this level of break-rewrite a message indicating the
result of the application attempt (just as in :go) is printed, followed
by the prompt for additional user input.

Generally speaking, :ok and :go are used when the break in question is
routine or uninteresting and :eval is used when the break is one that
the user anticipates is causing trouble.  For example, if you are
trying to determine why a lemma isn't being applied to a given term and
the :target of the current break-rewrite is the term in question, you
would usually :eval the rule and if break-rewrite reports that the rule
failed then you are in a position to determine why, for example by
carefully inspecting the :type-alist of governing assumptions or why
some hypothesis of the rule could not be established.

It is often the case that when you are in break-rewrite you wish to
change the set of monitored runes.  This can be done by using :monitor
and :unmonitor as noted above.  For example, you might want to monitor
a certain rule, say hyp-reliever, just when it is being used while
attempting to apply another rule, say main-lemma.  Typically then you
would monitor main-lemma at the ACL2 top-level, start the
proof-attempt, and then in the break-rewrite in which main-lemma is
about to be tried, you would install a monitor on hyp-reliever.  If
during the ensuing :eval hyp-reliever is broken you will know it is
being used under the attempt to apply main-lemma.

However, once hyp-reliever is being monitored it will be monitored even
after main-lemma has been tried.  That is, if you let the proof attempt
proceed then you may see many other breaks on hyp-reliever, breaks that
are not "under" the attempt to apply main-lemma.  One way to prevent
this is to :eval the application of main-lemma and then :unmonitor
hyp-reliever before exiting.  But this case arises so often that ACL2
supports several additional "flavors" of proceed commands.

:Ok!, :go!, and :eval! are just like their counterparts (:ok, :go, and
:eval, respectively), except that while processing the rule that is
currently broken no runes are monitored.  When consideration of the
current rule is complete, the set of monitored runes is restored to its
original setting.

:Ok$, :go$, and :eval$ are similar but take an additional argument
which must be a list of runes.  An example usage of :eval$ is

     3 ACL2 !>:eval$ ((:rewrite hyp-reliever))

These three commands temporarily install unconditional breaks on the
runes listed, proceed with the consideration of the currently broken
rule, and then restore the set of monitored rules to its original
setting.

Thus, there are nine ways to proceed from the initial entry into
break-rewrite although we often speak as though there are two, :ok and
:eval, and leave the others implicit.  We group :go with :ok because in
all their flavors they exit break-rewrite without further interaction
(at the current level).  All the flavors of :eval require further
interaction after the rule has been tried.

To abort a proof attempt and return to the top-level of ACL2 you may at
any time type (a!)  followed by a carriage return.  If you are not in a
raw Lisp break, you may type :a! instead.

We now address ourselves to the post-:eval interaction with
break-rewrite.  As noted, that interaction begins with break-rewrite's
report on the results of applying the rule: whether it worked and
either what it produced or why it failed.  This information is also
printed by certain keyword commands available after :eval, namely
:wonp, :rewritten-rhs, and :failure-reason.  In addition, by using brr@
(see BRR@) you can obtain this information in the
form of ACL2 data objects.  This allows the development of more
sophisticated "break conditions"; see MONITOR for examples.  In
this connection we point out the macro form (ok-if term).  See
OK-IF.  This command exits break-rewrite if term evaluates to non-nil
and otherwise does not exit.  Thus it is possible to define macros that
provide other kinds of exits from break-rewrite.  The only way to exit
break-rewrite after :eval is :ok (or, equivalently, the use of ok-if).

ACL2 users who wish to know more about break-rewrite so that they can
develop more convenient ways to monitor rules are encouraged to speak
to J Moore.

The rest of this documentation discusses a few implementation details
of break-rewrite and may not be interesting to the typical user.

There is no ACL2 function named break-rewrite.  It is an illusion
created by appropriate calls to two functions named brkpt1 and brkpt2.
As previously noted, break-rewrite is ld operating on a wormhole state.
One might therefore wonder how break-rewrite can apply a rule and then
communicate the results back to the rewriter running in the external
state.  The answer is that it cannot.  Nothing can be communicated
through a wormhole.  In fact, brkpt1 and brkpt2 are each calls of ld
running on wormhole states.  Brkpt1 implements the pre-:eval
break-rewrite and brkpt2 implements the post-:eval break-rewrite.  The
rewriter actually calls brkpt1 before attempting to apply a rule and
calls brkpt2 afterwards.  In both cases, the rewriter passes into the
wormhole the relevant information about the current context.  Logically
brkpt1 and brkpt2 are no-ops and rewrite ignores the nil they return.
But while control is in them the execution of rewrite is suspended and
cannot proceed until the break-rewrite interactions complete.

This design causes a certain anomoly that might be troubling.  Suppose
that inside break-rewrite before :evaling a rule (i.e., in the brkpt1
wormhole state) you define some function, foo.  Suppose then you :eval
the rule and eventually control returns to break-rewrite (i.e., to
brkpt2 on a wormhole state with the results of the application in it).
You will discover that foo is no longer defined!  That is because the
wormhole state created during your pre-:eval interaction is lost when
we exit the wormhole to resume the proof attempt.  The post-:eval
wormhole state is in fact identical to the initial pre-:eval state
(except for the results of the application) because rewrite did not
change the external state and both wormhole states are copies of it.  A
similar issue occurs with the use of trace utilities: all effects of
calling trace$ and untrace$ are erased when you proceed from a break in
the break-rewrite loop.

There is a lot more to know about break-rewrite, most of which is
fairly easy to learn from looking at the code, since it is all
expressed in ACL2.  Feel free to ask questions of J Moore.

BREAK-LEMMA    a quick introduction to breaking rewrite rules in ACL2

     Example:
     :brr t                          ; if you haven't done that yet
     :monitor (:rewrite lemma12) t   ; to install a break point on the
                                     ; rule named (:rewrite lemma12)

ACL2 does not support Nqthm's break-lemma but supports a very similar
and more powerful break facility.  Suppose some proof is failing;
apparently some particular rule is not being used and you wish to learn
why.  Then you need the ACL2 break-rewrite facility.  See
BREAK-REWRITE and all of its associated :doc topics for details.  The
following basic steps are required.

(1) To enable the "break rewrite" feature, you must first execute

     ACL2 !>:brr t

at the top-level of ACL2.  Equivalently, evaluate (brr t).
Break-rewrite stays enabled until you disable it with (brr nil).  When
break-rewrite is enabled the ACL2 rewriter will run slower than normal
but you will be able to monitor the attempts to apply specified rules.

(2) Decide what runes (see RUNE) you wish to monitor.  For
example, you might want to know why (:rewrite lemma12 . 2) is not being
used in the attempted proof.  That, by the way, is the name of the
second rewrite rule generated from the event named lemma12.

The command

     ACL2 !>:monitor (:rewrite lemma12 . 2) t

will install an "unconditional" break point on that rule.  The "t" at
the end of the command means it is unconditional, i.e., a break will
occur every time the rule is tried.  ACL2 supports conditional breaks
also, in which case the t is replaced by an expression that evaluates
to non-nil when you wish for a break to occur.  See MONITOR.
The above keyword command is, of course, equivalent to

     ACL2 !>(monitor '(:rewrite lemma12 . 2) t)

which you may also type.  You may install breaks on as many rules as
you wish.  You must use monitor on each rule.  You may also change the
break condition on a rule with monitor.  Use unmonitor (see
UNMONITOR) to remove a rule from the list of monitored rules.

(3) Then try the proof again.  When a monitored rule is tried by the
rewriter you will enter an interactive break, called break-rewrite.
See BREAK-REWRITE for a detailed description.  Very simply,
break-rewrite lets you inspect the context of the attempted application
both before and after the attempt.  When break-rewrite is entered it
will print out the "target" term being rewritten.  If you type :go
break-rewrite will try the rule and then exit, telling you (a) whether
the rule was applied, (b) if so, how the target was rewritten, and (c)
if not, why the rule failed.  There are many other commands.  See
BRR-COMMANDS.

(4) When you have finished using the break-rewrite feature you should
disable it to speed up the rewriter.  You can disable it with

     ACL2 !>:brr nil

The list of monitored rules and their break conditions persists but is
ignored.  If you enable break-rewrite later, the list of monitored
rules will be displayed and will be used again by rewrite.

You should disable the break-rewrite feature whenever you are not
intending to use it, even if the list of monitored rules is empty,
because the rewriter is slowed down as long as break-rewrite is enabled.

If you get a stack overflow, see CW-GSTACK.

BRR    to enable or disable the breaking of rewrite rules

     Example:
     :brr t       ; enable
     :brr nil     ; disable

     General Form:
     (brr flg)

where flg evaluates to t or nil.  This function modifies state so that
the attempted application of certain rewrite rules are "broken." "Brr"
stands for "break-rewrite" and can be thought of as a mode with two
settings.  The normal mode is "disabled."

When brr mode is "enabled" the ACL2 rewriter monitors the attempts to
apply certain rules and advises the user of those attempts by entering
an interactive wormhole break.  From within this break the user can
watch selected application attempts.  See BREAK-REWRITE.  The
user can also interact with the system during brr breaks via
brr-commands.

The rules monitored are selected by using the monitor and unmonitor
commands.  It is possible to break a rune "conditionally" in the sense
that an interactive break will occur only if a specified predicate is
true of the environment at the time of the attempted application.  See
MONITOR and see UNMONITOR.

Even if a non-empty set of rules has been selected, no breaks will occur
unless brr mode is enabled.  Thus, the first time in a session that you
wish to monitor a rewrite rule, use :brr t to enable brr mode.
Thereafter you may select runes to be monitored with monitor and
unmonitor with the effect that whenever monitored rules are tried (and
their break conditions are met) an interactive break will occur.  Be
advised that when brr mode is enabled the rewriter is somewhat slower
than normal.  Furthermore, that sluggishness persists even if no runes
are monitored.  You may regain normal performance -- regardless of what
runes are monitored -- by disabling brr mode with :brr nil.

Why isn't brr mode disabled automatically when no runes are monitored?
More generally, why does ACL2 have brr mode at all?  Why not just test
whether there are monitored runes?  If you care about the answers, see
WHY-BRR.

BRR Mode and Console Interrupts: If the system is operating in brr mode
and you break into raw Lisp (as by causing a console interrupt or
happening upon a signalled Lisp error; see BREAKS), you can
return to the ACL2 top-level, outside any brr environment, by executing
(abort!).  Otherwise, the normal way to quit from such a break (for
example :q in GCL, :reset in Allegro CL, and q in CMU CL) will return
to the innermost ACL2 read-eval-print loop, which may or may not be the
top-level of your ACL2 session!  In particular, if the break happens to
occur while ACL2 is within the brr environment (in which it is
preparing to read brr-commands), the abort will merely return to that
brr environment.  Upon exiting that environment, normal theorem proving
is continued (and the brr environment may be entered again in response
to subsequent monitored rule applications).  Before returning to the brr
environment, ACL2 "cleans up" from the interrupted brr processing.
However, it is not possible (given the current implementation) to clean
up perfectly.  This may have two side-effects.  First, the system may
occasionally print the self-explanatory "Cryptic BRR Message 1" (or 2),
informing you that the system has attempted to recover from an aborted
brr environment.  Second, it is possible that subsequent brr behavior
in that proof will be erroneous because the cleanup was done
incorrectly.  The moral is that you should not trust what you learn
from brr if you have interrupted and aborted brr processing during the
proof.  These issues do not affect the behavior or soundness of the
theorem prover.

BRR-COMMANDS    Break-Rewrite Commands

     :a!             abort to ACL2 top-level
     :target         term being rewritten
     :unify-subst    substitution making :lhs equal :target
     :hyps           hypotheses of the rule
     :hyp i          ith hypothesis of the rule
     :lhs            left-hand side of rule's conclusion
     :rhs            right-hand side of rule's conclusion
     :type-alist     type assumptions governing :target
     :initial-ttree  ttree before :eval (see TTREE)
     :ancestors      negations of backchaining hypotheses being pursued
     :wonp           indicates if application succeed (after :eval)
     :rewritten-rhs  rewritten :rhs (after :eval)
     :final-ttree    ttree after :eval (see TTREE)
     :failure-reason reason rule failed (after :eval)
     :path           rewrite's path from top clause to :target
     :frame i        ith frame in :path
     :top            top-most frame in :path
     :ok             exit break
     :go             exit break, printing result
     :eval           try rule and re-enter break afterwards
     :ok!            :ok but no recursive breaks
     :go!            :go but no recursive breaks
     :eval!          :eval but no recursive breaks
     :ok$ runes      :ok with runes monitored during recursion
     :go$ runes      :go with runes monitored during recursion
     :eval$ runes    :eval with runes monitored during recursion
     :help           this message
     :standard-help  :help message from ACL2 top-level

Break-rewrite is just a call of the standard ACL2 read-eval-print loop,
ld, on a "wormhole" state.  Thus, you may execute most commands you
might normally execute at the top-level of ACL2.  However, all state
changes you cause from within break-rewrite are lost when you exit or
:eval the rule.  You cannot modify stobjs from within the break.  See
BREAK-REWRITE for more details and see LD for general
information about the standard ACL2 read-eval-print loop.

BRR@    to access context sensitive information within break-rewrite

     Example:
     (brr@ :target)      ; the term being rewritten
     (brr@ :unify-subst) ; the unifying substitution

     General Form:
     (brr@ :symbol)

where :symbol is one of the following keywords.  Those marked with *
probably require an implementor's knowledge of the system to use
effectively.  They are supported but not well documented.  More is said
on this topic following the table.

     :symbol             (brr@ :symbol)
     -------             ---------------------

     :target             the term to be rewritten.  This term is an
                         instantiation of the left-hand side of the
                         conclusion of the rewrite-rule being broken.
                         This term is in translated form!  Thus, if
                         you are expecting (equal x nil) -- and your
                         expectation is almost right -- you will see
                         (equal x 'nil); similarly, instead of (cadr a)
                         you will see (car (cdr a)).  In translated
                         forms, all constants are quoted (even nil, t,
                         strings and numbers) and all macros are
                         expanded.

     :unify-subst        the substitution that, when applied to :target,
                         produces the left-hand side of the rule being
                         broken.  This substitution is an alist pairing
                         variable symbols to translated (!) terms.

     :wonp               t or nil indicating whether the rune was
                         successfully applied.  (brr@ :wonp) returns
                         nil if evaluated before :EVALing the rule.

     :rewritten-rhs      the result of successfully applying the rule
                         or else nil if (brr@ :wonp) is nil.  The result
                         of successfully applying the rule is always a
                         translated (!) term and is never nil.

     :failure-reason     some non-nil lisp object indicating why the rule
                         was not applied or else nil.  Before the rule is
                         :EVALed, (brr@ :failure-reason) is nil.  After
                         :EVALing the rule, (brr@ :failure-reason) is nil
                         if (brr@ :wonp) is t.  Rather than document the
                         various non-nil objects returned as the failure
                         reason, we encourage you simply to evaluate
                         (brr@ :failure-reason) in the contexts of interest.
                         Alternatively, study the ACL2 function tilde-@-
                         failure-reason-phrase.

     :lemma           *  the rewrite rule being broken.  For example,
                         (access rewrite-rule (brr@ :lemma) :lhs) will
                         return the left-hand side of the conclusion
                         of the rule.

     :type-alist      *  a display of the type-alist governing :target.
                         Elements on the displayed list are of the form
                         (term type), where term is a term and type
                         describes information about term assumed to hold
                         in the current context.  The type-alist may be
                         used to determine the current assumptions, e.g.,
                         whether A is a CONSP.

     :ancestors       *  a stack of frames indicating the backchain history
                         of the current context.  The theorem prover is in
                         the process of trying to establish each hypothesis
                         in this stack.  Thus, the negation of each hypothesis
                         can be assumed false.  Each frame also records the
                         rules on behalf of which this backchaining is being
                         done and the weight (function symbol count) of the
                         hypothesis.  All three items are involved in the
                         heuristic for preventing infinite backchaining.
                         Exception:  Some frames are ``binding hypotheses''
                         (equal var term) or (equiv var (double-rewrite term))
                         that bind variable var to the result of rewriting
                         term.

     :gstack          *  the current goal stack.  The gstack is maintained
                         by rewrite and is the data structure printed as the
                         current ``path.''  Thus, any information derivable
                         from the :path brr command is derivable from gstack.
                         For example, from gstack one might determine that
                         the current term is the second hypothesis of a
                         certain rewrite rule.

In general brr@-expressions are used in break conditions, the
expressions that determine whether interactive breaks occur when
monitored runes are applied.  See MONITOR.  For example, you
might want to break only those attempts in which one particular term is
being rewritten or only those attempts in which the binding for the
variable a is known to be a consp.  Such conditions can be expressed
using ACL2 system functions and the information provided by brr@.
Unfortunately, digging some of this information out of the internal
data structures may be awkward or may, at least, require intimate
knowledge of the system functions.  But since conditional expressions
may employ arbitrary functions and macros, we anticipate that a set of
convenient primitives will gradually evolve within the ACL2 community.
It is to encourage this evolution that brr@ provides access to the *'d
data.

MONITOR    to monitor the attempted application of a rule name

     Example:
     (monitor '(:rewrite assoc-of-app) 't)
     :monitor (:rewrite assoc-of-app) t
     :monitor (:definition app) (equal (brr@ :target) '(app c d))

     General Form:
     (monitor rune term)

where rune is a rune and term is a term, called the "break condition."
Rune must be either a :rewrite rune or a :definition rune.

When a rune is monitored any attempt to apply it may result in an
interactive break in an ACL2 "wormhole state." There you will get a
chance to see how the application proceeds.  See BREAK-REWRITE
for a description of the interactive loop entered.  Whether an
interactive break occurs depends on the value of the break condition
expression associated with the monitored rune.

NOTE: Some :rewrite rules are considered "simple abbreviations"; see
SIMPLE.  These can be be monitored, but only at certain times
during the proof.  Monitoring is carried out by code inside the
rewriter but abbreviation rules may be applied by a special purpose
simplifier inside the so-called _preprocess_ phase of a proof.  If you
desire to monitor an abbreviation rule, a warning will be printing
suggesting that you may want to supply the hint :DO-NOT '(PREPROCESS);
see HINTS.  Without such a hint, an abbreviation rule can be
applied during the preprocess phase of a proof, and no such application
will cause an interactive break.

To remove a rune from the list of monitored runes, use unmonitor.  To
see which runes are monitored and what their break conditions are,
evaluate (monitored-runes).

Monitor, unmonitor and monitored-runes are macros that expand into
expressions involving state.  While these macros appear to return the
list of monitored runes this is an illusion.  They all print monitored
rune information to the comment window and then return error triples
instructing ld to print nothing.  It is impossible to return the list
of monitored runes because it exists only in the wormhole state with
which you interact when a break occurs.  This allows you to change the
monitored runes and their conditions during the course of a proof
attempt without changing the state in which the the proof is being
constructed.

Unconditional break points are obtained by using the break condition t.
We now discuss conditional break points.  The break condition, expr,
must be a term that contains no free variables other than state and
that returns a single non-state result.  In fact, the result should be
nil, t, or a true list of commands to be fed to the resulting
interactive break.  Whenever the system attempts to use the associated
rule, expr is evaluated in the wormhole interaction state.  A break
occurs only if the result of evaluating expr is non-nil.  If the result
is a true list, that list is appended to the front of standard-oi and
hence is taken as the initial user commands issued to the interactive
break.

In order to develop effective break conditions it must be possible to
access context sensitive information, i.e., information about the
context in which the monitored rune is being tried.  The brr@ macro may
be used in break conditions to access such information as the term
being rewritten and the current governing assumptions.  This
information is not stored in the proof state but is transferred into
the wormhole state when breaks occur.  The macro form is (brr@ :sym)
where :sym is one of several keyword symbols, including :target (the
term being rewritten), :unify-subst (the substitution that instantiates
the left-hand side of the conclusion of the rule so that it is the
target term), and :type-alist (the governing assumptions).  See
BRR@.

For example,

     ACL2 !>:monitor (:rewrite assoc-of-app)
                     (equal (brr@ :target) '(app a (app b c)))

will monitor (:rewrite assoc-of-app) but will cause an interactive
break only when the target term, the term being rewritten, is (app a
(app b c)).

Because break conditions are evaluated in the interaction environment,
the user developing a break condition for a given rune can test
candidate break conditions before installing them.  For example,
suppose an unconditional break has been installed on a rune, that an
interactive break has occurred and that the user has determined both
that this particular application is uninteresting and that many more
such applications will likely occur.  An appropriate response would be
to develop an expression that recognizes such applications and returns
nil.  Of course, the hard task is figuring out what makes the current
application uninteresting.  But once a candidate expression is
developed, the user can evaluate it in the current context simply to
confirm that it returns nil.

Recall that when a break condition returns a non-nil true list that
list is appended to the front of standard-oi.  For example,

     ACL2 !>:monitor (:rewrite assoc-of-app) '(:go)

will cause (:rewrite assoc-of-app) to be monitored and will make the
break condition be '(:go).  This break condition always evaluates the
non-nil true list (:go).  Thus, an interactive break will occur every
time (:rewrite assoc-of-app) is tried.  The break is fed the command
:go.  Now the command :go causes break-rewrite to (a) evaluate the
attempt to apply the lemma, (b) print the result of that attempt, and
(c) exit from the interactive break and let the proof attempt continue.
Thus, in effect, the above :monitor merely "traces" the attempted
applications of the rune but never causes an interactive break
requiring input from the user.

It is possible to use this feature to cause a conditional break where
the effective break condition is tested *after* the lemma has been
tried.  For example:

     ACL2 !>:monitor (:rewrite lemma12)
                     '(:unify-subst
                       :eval$ nil
                       :ok-if (or (not (brr@ :wonp))
                                  (not (equal (brr@ :rewritten-rhs) '(foo a))))
                       :rewritten-rhs)

causes the following behavior when (:rewrite lemma12) is tried.  A
break always occurs, but it is fed the commands above.  The first,
:unify-subst, causes break-rewrite to print out the unifying
substitution.  Then in response to :eval$ nil the lemma is tried but
with all runes temporarily unmonitored.  Thus no breaks will occur
during the rewriting of the hypotheses of the lemma.  When the attempt
has been made, control returns to break-rewrite (which will print the
results of the attempt, i.e., whether the lemma was applied, if so what
the result is, if not why it failed).  The next command, the :ok-if
with its following expression, is a conditional exit command.  It means
exit break-rewrite if either the attempt was unsuccessful, (not (brr@
:wonp)), or if the result of the rewrite is any term other than (foo
a).  If this condition is met, the break is exited and the remaining
break commands are irrelevant.  If this condition is not met then the
next command, :rewritten-rhs, prints the result of the application
(which in this contrived example is known to be (foo a)).  Finally, the
list of supplied commands is exhausted but break-rewrite expects more
input.  Therefore, it begins prompting the user for input.  The end
result, then, of the above :monitor command is that the rune in
question is elaborately traced and interactive breaks occur whenever it
rewrites its target to (foo a).

We recognize that the above break condition is fairly arcane.  We
suspect that with experience we will develop some useful idioms.  For
example, it is straightforward now to define macros that monitor runes
in the ways suggested by the following names:  trace-rune,
break-if-target-is, and break-if-result-is.  For example, the last
could be defined as

     (defmacro break-if-result-is (rune term)
       `(monitor ',rune
                 '(quote (:eval :ok-if
                                (not (equal (brr@ :rewritten-rhs) ',term))))))

(Note however that the submitted term must be in translated form.)

Since we don't have any experience with this kind of control on lemmas
we thought it best to provide a general (if arcane) mechanism and hope
that the ACL2 community will develop the special cases that we find
most convenient.

MONITORED-RUNES    print the monitored runes and their break conditions

     Example and General Form:
     :monitored-runes

This macro prints a list, each element of which is of the form (rune
expr), showing each monitored rune and its current break condition.

OK-IF    conditional exit from break-rewrite

     Example Form:
     :ok-if (null (brr@ :wonp))

     General Form:
     :ok-if expr

where expr is a term involving no free variables other than state and
returning one non-state result which is treated as Boolean.  This form
is intended to be executed from within break-rewrite (see
BREAK-REWRITE).

Consider first the simple situation that the (ok-if term) is a command
read by break-rewrite.  Then, if the term is non-nil, break-rewrite
exits and otherwise it does not.

More generally, ok-if returns an ACL2 error triple (mv erp val state).
(See LD for more on error triples.)  If any form being
evaluated as a command by break-rewrite returns the triple returned by
(ok-if term) then the effect of that form is to exit break-rewrite if
term is non-nil.  Thus, one might define a function or macro that
returns the value of ok-if expressions on all outputs and thus create a
convenient new way to exit break-rewrite.

The exit test, term, generally uses brr@ to access context sensitive
information about the attempted rule application.  See BRR@.
Ok-if is useful inside of command sequences produced by
break conditions.  See MONITOR.  :ok-if is most useful after an
:eval command has caused break-rewrite to try to apply the rule because
in the resulting break environment expr can access such things as
whether the rule succeeded, if so, what term it produced, and if not,
why.  There is no need to use :ok-if before :evaling the rule since the
same effects could be achieved with the break condition on the rule
itself.  Perhaps we should replace this concept with
:eval-and-break-if?  Time will tell.

UNMONITOR    to stop monitoring a rule name

     Examples:
     (unmonitor '(:rewrite assoc-of-app))
     :unmonitor (:rewrite assoc-of-app)
     :unmonitor :all

     General Forms:
     (unmonitor rune)
     (unmonitor :all)

Here, rune is a rune that is currently among those with break points
installed.  This function removes the break.

Subtle point:  Because you may want to unmonitor a "rune" that is no
longer a rune in the current ACL2 world, we don't actually check this
about rune.  Instead, we simply check that rune is a consp beginning
with a keywordp.  That way, you'll know you've made a mistake if you
try to :unmonitor binary-append instead of :unmonitor (:definition
binary-append), for example.

DOCUMENTATION    functions that display documentation

This section explains the ACL2 online documentation system.  Thus, most
of it assumes that you are typing at the terminal, inside an ACL2
session.  If you are reading this description in another setting (for
example, in a web browser, in Emacs info, or on paper), simply ignore
the parts of this description that involve typing at the terminal.

For an introduction to the ACL2 online documentation system, type :more
below.  Whenever the documentation system concludes with "(type :more
for more, :more! for the rest)" you may type :more to see the next
block of documentation.

Topics related to documentation are documented individually:

To view the documentation in a web browser, open a browser to file
doc/HTML/acl2-doc.html under your ACL2 source directory, or just go to
the ACL2 home page at `http://www.cs.utexas.edu/users/moore/acl2/'.

To use Emacs Info (inside Emacs), first load distributed file
emacs/emacs-acl2.el (perhaps inside your .emacs file) and then execute
meta-x acl2-info.  In order to see true links to external web pages,
you may find the following addition to your .emacs file to be helpful.

     ; For emacs-version 22 or (presumably) later, you can probably set
     ; arrange that in Emacs Info, URLs become links, in the sense that
     ; if you hit <RETURN> while standing on a URL, then you will be
     ; taken to that location in a web browser.  If this does not happen
     ; automatically, then evaluating the `setq' form below might work
     ; if you have firefox.  If that does not work, then you can probably
     ; figure out what to do as follows.  First type
     ;   control-h v browse-url-browser-function
     ; and then from the resulting help page,
     ; hit <return> on the link ``customize'' in:
     ; ``You can customize this variable''
     ; and then follow instructions.
     (setq browse-url-browser-function (quote browse-url-firefox))

There is print version of the documentation, though we recommend using
one of the other methods (web, Emacs Info, or online) to browse it.  If
you really want the print version, you can find it here:
`http://www.cs.utexas.edu/users/moore/publications/acl2-book.ps.gz'.

Below we focus on how to access the online documentation, but some of
the discussion is relevant to other formats.

The ACL2 online documentation feature allows you to see extensive
documentation on many ACL2 functions and ideas.  You may use the
documentation facilities to document your own ACL2 functions and
theorems.

If there is some name you wish to know more about, then type

     ACL2 !>:doc name

in the top-level loop.  If the name is documented, a brief blurb will
be printed.  If the name is not documented, but is "similar" to some
documented names, they will be listed.  Otherwise, nil is returned.

Every name that is documented contains a one-line description, a few
notes, and some details.  :Doc will print the one-liner and the notes.
When :doc has finished it stops with the message "(type :more for more,
:more! for the rest)" to remind you that details are available.  If you
then type

     ACL2 !>:more

a block of the continued text will be printed, again concluding with
"(type :more for more, :more! for the rest)" if the text continues
further, or concluding with "*-" if the text has been exhausted.  By
continuing to type :more until exhausting the text you can read
successive blocks.  Alternatively, you can type :more! to get all the
remaining blocks.

If you want to get the details and don't want to see the elementary
stuff typed by :doc name, type:

     ACL2 !>:MORE-DOC name

We have documented not just function names but names of certain
important ideas too.  For example, see REWRITE and see
META to learn about :rewrite rules and :meta rules, respectively.
See HINTS to learn about the structure of the :hints argument
to the prover.  The deflabel event (see DEFLABEL) is a way to
introduce a logical name for no reason other than to attach
documentation to it; also see DEFDOC.

How do you know what names are documented?  There is a documentation
data base which is querried with the :docs command.

The documentation data base is divided into sections.  The sections are
listed by

     ACL2 !>:docs *

Each section has a name, sect, and by typing

     ACL2 !>:docs sect

or equivalently

     ACL2 !>:doc sect

you will get an enumeration of the topics within that section.  Those
topics can be further explored by using :doc (and :more) on them.  In
fact the section name itself is just a documented name.  :more
generally gives an informal overview of the general subject of the
section.

     ACL2 !>:docs **

will list all documented topics, by section.  This fills several pages
but might be a good place to start.

If you want documentation on some topic, but none of our names or brief
descriptions seem to deal with that topic, you can invoke a command to
search the text in the data base for a given string.  This is like the
GNU Emacs "apropos" command.

     ACL2 !>:docs "functional inst"

will list every documented topic whose :doc or :more-doc text includes
the substring "functional inst", where case and the exact number of
spaces are irrelevant.

If you want documentation on an ACL2 function or macro and the
documentation data base does not contain any entries for it, there are
still several alternatives.

     ACL2 !>:args fn

will print the arguments and some other relevant information about the
named function or macro.  This information is all gleaned from the
definition (not from the documentation data base) and hence this is a
definitive way to determine if fn is defined as a function or macro.

You might also want to type:

     ACL2 !>:pc fn

which will print the command which introduced fn.  You should see
COMMAND-DESCRIPTOR for details on the kinds of input you can give the
:pc command.

The entire ACL2 documentation data base is user extensible.  That is,
if you document your function definitions or theorems, then that
documentation is made available via the data base and its query
commands.

The implementation of our online documentation system makes use of
Common Lisp's "documentation strings." While Common Lisp permits a
documentation string to be attached to any defined concept, Common Lisp
assigns no interpretation to these strings.  ACL2 attaches special
significance to documentation strings that begin with the characters
":doc-section".  When such a documentation string is seen, it is stored
in the data base and may be displayed via :doc, :more, :docs, etc.
Such documentation strings must follow rigid syntactic rules to permit
their processing by our commands.  These are spelled out elsewhere; see
DOC-STRING.

A description of the structure of the documentation data base may also
be found; see DOC-STRING.

*TERMINAL-MARKUP-TABLE*    a markup table used for printing to the terminal

The value of the ACL2 constant *terminal-markup-table* is an association
list pairing markup keys with strings, to be used for printing to the
terminal.  See MARKUP for a description of the ACL2 markup
language.

The entries in *terminal-markup-table* are of the form

     (key . fmt-string)

where key is one of the doc-string tilde directives (see
MARKUP), and fmt-string is a string as expected by the ACL2 printing
function fmt.  The system arranges that for any arg, when an expression
~key[arg] is encountered by the documentation printer, fmt will print
fmt-string in the association list where #\a is bound to arg and #\A is
bound to the result of applying the function string-upcase to arg.

It is possible to implement tools in ACL2 for printing documentation to
other than the terminal.  In fact, such tools exist for Texinfo and for
HTML.  For now, discussion of this capability is beyond the scope of
the present topic.

ARGS    args, guard, type, constraint, etc., of a function symbol

     Example:
     :args assoc-eq

Args takes one argument, a symbol which must be the name of a function
or macro, and prints out the formal parameters, the guard expression,
the output signature, the deduced type, the constraint (if any), and
whether documentation about the symbol is available via :doc.

DOC    brief documentation (type :doc name)

NOTE:  The :doc command only makes sense at the terminal.  Furthermore
it only works at the terminal when a "full-size" image has been built.
Most users will probably access the ACL2 documentation in other ways,
as explained in the file "doc/README" that comes with the ACL2
distribution.

     Examples:
     ACL2 !>:doc DEFTHM          ; print documentation of DEFTHM
     ACL2 !>:doc logical-name    ; print documentation of LOGICAL-NAME
     ACL2 !>:doc "MY-PKG"      ; print documentation of "MY-PKG"

     Related Topics:
     :more                      ; continues last :doc or :more-doc text
     :more-doc name             ; prints more documentation for name
     :docs **                   ; lists all documented symbols
     :docs "compil"             ; documented symbols apropos "compil"
     :DOC documentation         ; describes how documentation works

     General Form:
     ACL2>:doc logical-name

where logical-name is a logical name (see LOGICAL-NAME) for
which you hope there is documentation.  Chances are there is no
documentation at the moment, but we are working on adding documentation
strings for all the user level ACL2 functions.

For a general discussion of our treatment of documentation strings, see
DOCUMENTATION.

This is the first cut at online documentation.  Users can be
particularly helpful by sending mail on the inadequacies of the system.
Address it just to Moore and put Documentation in the subject line.
There are several things that trouble me about what I've done here.

First, many concepts aren't documented.  Ultimately, I'd like to .
document (a) every CLTL primitive (e.g., case and coerce) and (b) every
ACL2 extension (e.g., aref1 and getprop).  But so far I have focussed
on documenting (c) the ACL2 system primitives (e.g., defthm and what
hints look like).  My priorities are (c), then (b), and then (a),
following the philosophy that the most unstable features should get
online documentation in these early releases.  Having gotten the basic
documentation in place, I'll document new things as they are added, and
in response to your pleas I'll try to add documentation to old things
that are widely regarded as important.

Second, I worry that the existing documentation is unhelpful because it
provides too much or too little detail, or it provides the detail too
far away from where it is needed.  Please be on the lookout for this.
Did you get what you needed when you appealed to :doc or :more-doc?  If
not, what was it you needed?  Would more cross-references help?  Did
you get lost in maze of cross-references?

DOC!    all the documentation for a name (type :doc! name)

NOTE:  The :doc! command only makes sense at the terminal.

     Examples:
     ACL2 !>:doc! defthm
     ACL2 !>:doc! certificate

This command is like :doc name followed by :more!.  It prints all the
documentation of name.

DOC-STRING    formatted documentation strings

     Examples:
     ":Doc-Section name
     one-liner~/notes~/details"

     ":Doc-Section name
     one-liner~/
     notes~/
     details~/
     :cite old-name1
     :cited-by old-name2"

Use (get-doc-string 'name state) to see other examples.

Documentation strings not beginning with ":Doc-Section" (case is
irrelevant) are ignored.  See MARKUP for how to supply
formatting information (such as fonts and displayed text) in
documentation strings.

ACL2 attaches special importance to documentation strings beginning
with the header ":Doc-Section" (or any variant thereof obtained by
changing case).  Any documentation string that does not begin with such
a header is considered unformatted and is ignored.  For the rest of
this discussion, we use the phrase "documentation string" as though it
read "formatted documentation string."

Documentation strings are always processed in the context of some
symbol, name, being defined.  (Indeed, if an event defines no symbol,
e.g., verify-guards or in-theory, then it is not permitted to have a
formatted documentation string.)  The string will be associated with
name in the "documentation data base." The data base is divided into
"sections" and each section is named by a symbol.  Among the sections
are events, documentation, history, other, and miscellaneous.  A
complete list of the sections may be obtained by typing :docs * at the
terminal.  You can create new sections.  The main purpose of sections
is simply to partition the large set of names into smaller subsets
whose contents can be enumerated separately.  The idea is that the user
may remember (or recognize) the relevant section name and then read its
contents to find interesting items.

Within a section are "documentation tuples" which associate with each
documented name its documentation string and a list of related
documented names, called the "related names" of the name.  When :doc
prints the documentation for name, it always lists the related names.

When a formatted documentation string is submitted with the defining
event of some name, the section name and an initial set of related
names are parsed from the string.  In addition, the formatted string
contains various "levels" of detail that are printed out at different
times.  Finally, it is possible for a string to cause the newly
documented name to be added to the related names of any previously
documented name.  Thus, as new names are introduced they can be grouped
with old ones.

The general form of an ACL2 formatted documentation string is

     ":DOC-SECTION <section-name>
       <one-liner>~/
       <notes>~/
       <details>~/
       :CITE <n1>
       ...
       :CITE <nn>
       :CITED-BY <m1>
       ...
       :CITED-BY <mm>"

Before we explain this, let it be noted that (get-doc-string name
state) will return the documentation string associated with name in the
documentation data base.  You may want to call get-doc-string on 'pe
and 'union-theories just to see some concrete documentation strings.
This documentation string, which is rather long, is under 'doc-string.

A formatted documentation string has five parts: the header and
section-name (terminating in the first #\Newline), the <one-liner>,
<notes>, and <details> (each terminating in a tilde-slash ("~/") pair),
and a citation part.  These five parts are parsed into six components.
<section-name> is read as the name of a symbol, section-name.
<one-liner>, <notes>, and <details> are arbitrary sequences of
characters (ignoring initial white space and not including the
tilde-slash pairs which terminate them).  The <ni> are read as symbols
and assembled into a list called the "cite" symbols.  The <mi> are read
as symbols and assembled into a list called the "cited-by" symbols.
See the warning below regarding the hackish nature of our symbol reader.

Section-name must either be a previously documented symbol or else be
name, the symbol being documented.  To open a new section of the data
base, named section-name, you should define the logical name
section-name (as by deflabel or any other event; also see
DEFDOC) and attach to it a documentation string for section
section-name.  You might wish to print out the documentation string we
use for some of our section names, e.g., (get-doc-string 'events
state).  By forcing section names to be documented symbols, we permit
sections themselves to have one line descriptions and discussions,
presented by the standard documentation facilities like the facilities
:doc and :more-doc that may be used at the terminal.

Each of the ni's and mi's must be previously documented symbols.

Both <one-liner> and <details> must be non-empty, i.e., must contain
some non-whitespace characters.  <notes> may be empty.  The :cites and
:cited-bys pairs may be intermingled and may be separated by either
newlines or spaces.  The citation part may be empty.  When the citation
part is empty, the tilde-slash pair terminating the <details> part may
be omitted.  Thus, the simplest form of a formatted documentation
string is:

     ":Doc-Section <section-name>
      <one-liner>~/~/
      <details>"

Since white space at the front of <one-liner>, <notes> and <details> is
ignored, we often precede those parts by #\Newlines to make the strings
easier to read in our source files.  We also typically indent all of
the text in the string by starting each line with a few spaces.  (The
Emacs commands for formatting Lisp get confused if you have arbitrary
characters on the left margin.)  We assume that every line in
<one-liner>, <notes>, and <details> starts with at least as many spaces
as <one-liner> does, i.e., we assume they are all indented the same
amount (or more).  Let d be the number of spaces separating <one-liner>
from the #\Newline preceding it.  When the various parts are printed,
we "de-indent" by stripping out the first d spaces following each
#\Newline.

However, we find that when documentation is printed flush against the
left margin it is difficult to distinguish the documentation text from
previous output.  We therefore prefix each line we print by a special
pad of characters.  By default, this pad is "| " so that documentation
text has a vertical bar running down the left margin.  But the pad is
just the value of the global variable doc-prefix and you may assign it
any string you wish.

To add such a string to the data base under the symbol name we make a
new entry in the section-name section of the data base.  The entry
associates name with the string and uses the string's cites list as the
initial value of the related names field.  In addition, we add name to
the related names field of each of the names listed in the string's
cited-by list.  We also add name to the related names field of its
section-name.  Observe that the cites list in a string is only the
initial value of the related names of the names.  Future documentation
strings may add to it via :cited-by or :doc-section.  Indeed, this is
generally the case.  We discuss this further below.

When a brief description of name is required (as by :docs **), name and
<one-liner> are printed.  <one-liner> is usually printed starting in
column 15 (however see PRINT-DOC-START-COLUMN).  Despite its
name, <one-liner> need not be one line.  It usually is one line,
however.

When you type :doc name at the terminal, the first response will be to
print name and <one-liner>.  Then :doc prints <notes>, if any.  Then,
if name is the name of a section, it prints the <one-liner>s for each
of its related names.  For example, try :doc events.  If name is not a
section name but does have some related names, they are merely listed
but not explained.  Try :doc theory-functions.  :more-doc name prints
<details>.

Our style is to let each new concept add itself to the related names of
old concepts.  To do otherwise increases the chances that documentation
gets outdated because one often forgets to update supposedly complete
lists of the relevant topics when new topics are invented.  For
example, :doc theory-functions lists each available theory function.
But get-doc-string of 'theory-functions just shows a few examples and
has an empty cites list.  From where do we get the names of the theory
functions listed by :doc?  The answer is that each theory function has
its own documentation string and those strings each specify :cited-by
theory-functions.  See for example get-doc-string of 'union-theories.
So by the time the entire system is assembled, the related names of
'theory-functions contains all the (documented) theory functions.  This
makes it easy to add new theory functions without changing the general
discussion in 'theory-functions.

When an event or command form is printed, as by :pe or :pc, that
contains a formatted documentation string, we do not print the actual
documentation string (since they are usually large and distracting).
Instead we print the string:

       "Documentation available via :doc"

inviting you to use :doc and :more-doc (or get-doc-string) if you wish
to see the documentation at the terminal.

_Warning on Reading Symbols from Strings:_ When we read a symbol, such
as the section-symbol, from a documentation string, we use a quick and
dirty imitation of the much more powerful CLTL read program.  In
particular, we scan past any whitespace, collect all the characters we
see until we get to more whitespace or the end of the string, convert
the characters to upper case, make a string out of them, and intern
that string.  Thus, if you typed ":Doc-Section 123 ..." we would read
the 123 as the symbol |123|.  Observe that special characters, such as
parentheses and escape characters, are not afforded their usual
reverence by our hack.  Furthermore, the question arises: in which
package do we intern the symbol?  The answer is, usually, the package
containing the name being defined.  I.e., if you are documenting
my-pkg::name and you attach a documentation string that begins
":Doc-Section: Machines ..." then the section-symbol will be
my-pkg::machines.  We recognize two special cases. If the first
character read is a colon, we use the keyword package.  If the first
five characters read are acl2:: then we intern in the "ACL2" package.
Our own section names, e.g., events, are in the "ACL2" package.

In a related area, when you ask for the documentation of a name, e.g.,
when you type :doc name at the terminal, that name is read with the
full ACL2 reader, not the hack just described.  That name is read into
the current package.  Thus, if you are operating in-package "MY-PKG"
and type :doc events, what is read is my-pkg::events.  The data base
may not contain an entry for this symbol.  Before reporting that no
documentation exists, we try acl2::events.

One last note: defpkg permits a formatted documentation string, which
is associated in the data base with the name of the package.  But the
name of the package is a string, not a symbol.  It is permitted to
access the documentation of a string (i.e., package name).  But there
are no facilities for getting such a stringp name into the related
names of another name nor of making such stringp names be section
names.  That is because we always read symbols from strings and never
read strings from strings.  I.e., if you did write "Doc-Section
\"MY-PKG\" ..." it would read in as a weird symbol.