This is documentation for ACL2 Version 5.0
Copyright (C) 2012  University of Texas at Austin

This program is free software; you can redistribute it and/or modify
it under the terms of Version 2 of the GNU General Public License as
published by the Free Software Foundation.

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.

ACL2 as an Interactive Theorem Prover    ACL2 as an Interactive Theorem Prover

The ACL2 theorem prover finds proofs in the ACL2 logic.  It can be
automatic.  But most often the user must help it.

The user usually guides ACL2 by suggesting that it first prove key
lemmas.  Lemmas are just theorems used in the proofs of other theorems.

ACL2 as an Interactive Theorem Prover (cont)    ACL2 as an Interactive Theorem Prover (cont)

Next on the Walking Tour:  ACL2 System Architecture

When ACL2 proves a lemma, it is converted into one or more rules and
stored in a database.  The theorem prover is rule-driven.  By proving
lemmas you can configure ACL2 to behave in certain ways when it is
trying to prove formulas in a certain problem domain.  The expert user
can make ACL2 do amazingly "smart" looking things.

But it would be wrong to think that ACL2 knows the mathematical content
of a formula just because it has proved it.  What ACL2 knows -- all ACL2
knows -- is what is encoded in its rules.  There are many types of rules
(see RULE-CLASSES <>).

Many formulas can be effectively coded as rules.  But by the same
token, it is possible to encode a formula as a rule that is so
ineffective it cannot even prove itself!

The way a formula is stored as a rule is entirely up to the user.  That
is, you determine how ACL2 should use each formula that it proves.

The most common kind of rule is the rewrite rule.  It is so common that
if you don't tell ACL2 how to store a formula, it stores it as a rewrite
rule.

Next on the Walking Tour:  ACL2 System Architecture

ACL2 is an Untyped Language    ACL2 is an Untyped Language

The example

     ACL2 !>(app '(a b c) 27)
     (A B C . 27)

illustrates the fact that ACL2's logic is untyped (see About Types
for a brief discussion of the typed versus untyped nature of
the logic).

The definition of app makes no restriction of the arguments to lists.
The definition says that if the first argument satisfies endp <> then
return the second argument.  In this example, when app has recursed
three times down the cdr of its first argument, '(a b c), it reaches
the final nil, which satisfies endp, and so 27 is returned.  It is
naturally consed into the emerging list as the function returns from
successive recursive calls (since cons does not require its arguments to
be lists, either).  The result is an "improper" list, (a b c . 27).

You can think of (app x y) as building a binary tree by replacing the
right-most tip of the tree x with the tree y.

About Models    About Models

Next on the Flying Tour:  Models of Computer Hardware and Software

ACL2 is used to construct mathematical models of computer hardware and
software (i.e., "digital systems").

A mathematical model is a set of mathematical formulas used to predict
the behavior of some artifact.

The use of mathematical models allows faster and cheaper delivery of
better systems.

Models need not be complete or perfectly accurate to be useful to the
trained engineer.

See Models in Engineering for more discussion of these
assertions in an engineering context.

Next on the Flying Tour:  Models of Computer Hardware and Software

About Types    About Types

The universe of ACL2 objects includes objects of many different types.
For example, t is a "symbol" and 3 is an "integer."  Roughly speaking
the objects of ACL2 can be partitioned into the following types:

     Numbers                   3, -22/7, #c(3 5/2)
     Characters                #\A, #\a, #\Space
     Strings                   "This is a string."
     Symbols                   'abc, 'smith::abc
     Conses (or Ordered Pairs) '((a . 1) (b . 2))

When proving theorems it is important to know the types of object
returned by a term.  ACL2 uses a complicated heuristic algorithm,
called type-set <>, to determine what types of objects a term may
produce.  The user can more or less program the type-set algorithm by
proving type-prescription <> rules.

ACL2 is an "untyped" logic in the sense that the syntax is not typed:
It is legal to apply a function symbol of n arguments to any n terms,
regardless of the types of the argument terms.  Thus, it is permitted
to write such odd expressions as (+ t 3) which sums the symbol t and
the integer 3.  Common Lisp does not prohibit such expressions.  We
like untyped languages because they are simple to describe, though
proving theorems about them can be awkward because, unless one is
careful in the way one defines or states things, unusual cases (like (+
t 3)) can arise.

To make theorem proving easier in ACL2, the axioms actually define a
value for such terms.  The value of (+ t 3) is 3; under the ACL2
axioms, non-numeric arguments to + are treated as though they were 0.

You might immediately wonder about our claim that ACL2 is Common Lisp,
since (+ t 3) is "an error" (and will sometimes even "signal an error")
in Common Lisp.  It is to handle this problem that ACL2 has guards.  We
will discuss guards later in the Walking Tour.  However, many new users
simply ignore the issue of guards entirely and that is what we
recommend for now.

You should now return to the Walking Tour.

About the ACL2 Home Page    About the ACL2 Home Page

Next on the Flying Tour:  What Is ACL2(Q)

The ACL2 Home Page is integrated into the ACL2 online documentation.
Over 4 megabytes of hypertext is available here.

The vast majority of the text is user-level documentation.  For
example, to find out about rewrite <> rules you could click on the link.
(If you do that, remember to use your browser's Back Button to come back
here.)

The tiny warning signs <> mark links that lead out of the
introductory-level material and into the user documentation.  We advise
against following such links upon your first reading of the
documentation.

At the end of the tours you will have a chance to revisit them quickly
to explore alternative paths more fully.

Finally, every page contains two icons at the bottom.  The ACL2 icon
leads you back to the ACL2 Home Page.  The Index icon allows you to
browse an alphabetical listing of all the topics in ACL2's online
documentation.  But both icons take you off the main route of the tour.

Next on the Flying Tour:  What Is ACL2(Q)

About the Admission of Recursive Definitions    About the Admission of Recursive Definitions

You can't just add any formula as an axiom or definition and expect the
logic to stay sound!  For example, if we were permitted to define (APP
X Y) so that it was equal to (NOT (APP X Y)) then we could prove
anything.  The purported "definition" of APP must have several
properties to be admitted to the logic as a new axiom.

The key property a recursive definition must have is that the recursion
terminate.  This, along with some syntactic criteria, ensures us that
there exists a function satisfying the definition.

Termination must be proved before the definition is admitted.  This is
done in general by finding a measure of the arguments of the function
and a well-founded relation such that the arguments "get smaller" every
time a recursive branch is taken.

For app the measure is the "size" of the first argument, x, as
determined by the primitive function acl2-count <>.  The well-founded
relation used in this example is o-p <>, which is the standard ordering
on the ordinals less than "epsilon naught."  These particular choices
for app were made "automatically" by ACL2.  But they are in fact
determined by various "default" settings.  The user of ACL2 can change
the defaults or specify a "hint" to the defun <> command to specify the
measure and relation.

You should now return to the Walking Tour.

About the Prompt    About the Prompt

The string "ACL2 !>" is the ACL2 prompt.

The prompt tells the user that an ACL2 command <>is expected.  In
addition, the prompt tells us a little about the current state of the
ACL2 command interpreter.  We explain the prompt briefly below.  But
first we talk about the command interpreter.

An ACL2 command is generally a Lisp expression to be evaluated.  There
are some unusual commands (such as :q <> for quitting ACL2) which cause
other behavior.  But most commands are read, evaluated, and then have
their results printed.  Thus, we call the command interpreter a
"read-eval-print loop."  The ACL2 command interpreter is named LD <>
(after Lisp's "load").

When a command is read, all the symbols in it are converted to
uppercase.  Thus, typing (defun app ...) is the same as typing (DEFUN
APP ...) or (defun App ...).  There are ways to force lowercase case
characters into symbols but we won't discuss them here.  A consequence
of Common Lisp's default uppercasing is that you'll see a general lack
of concern over the case used when symbols are displayed in this
documentation.

In addition, symbols "belong" to "packages" which give the user a way to
control namespaces.  The prompt tells us which package is the default
one, namely "ACL2".  That means when we call car, for example, we are
invoking the standard definition of that symbol.  If the packager were
"JONES" then car would refer to the definition of that symbol in that
package (which may or may not be different depending on what symbols
were imported into that package.

A command like (defun app (x y) ...) causes ACL2 to evaluate the defun
<> function on app, (x y) and ....  When that command is evaluated it
prints some information to the terminal explaining the processing of
the proposed definition.  It returns the symbol APP as its value, which
is printed by the command interpreter.  (Actually, defun is not a
function but a macro <> which expands to a form that involves state <>,
a necessary precondition to printing output to the terminal and to
"changing" the set of axioms.  But we do not discuss this further here.)

The defun command is an example of a special kind of command called an
"event."  Events <> are those commands that change the "logical world"
by adding such things as axioms or theorems to ACL2's data base.  See
WORLD <>.  But not every command is an event command.

A command like (app '(1 2 3) '(4 5 6 7)) is an example of a non-event.
It is processed the same general way: the function app is applied to the
indicated arguments and the result is printed.  The function app does
not print anything and does not change the "world."

A third kind of command is one that display information about the
current logical world or that "roll back" to previous versions of the
world.  Such commands are called "history" <> commands.

What does the ACL2 prompt tell us about the read-eval-print loop?  The
prompt "ACL2 !>" tells us that the command will be read with
current-package <> set to "ACL2", that guard checking (see
SET-GUARD-CHECKING <>) is on ("!"), and that we are at the top-level
(there is only one ">").  For more about the prompt, see
DEFAULT-PRINT-PROMPT <>.

You should now return to the Walking Tour.

An Example Common Lisp Function Definition    An Example Common Lisp Function Definition

Next on the Walking Tour:  An Example of ACL2 in Use

Consider the binary trees x and y below.

In Lisp, x is written as the list '(A B) or, equivalently, as '(A B .
NIL).  Similarly, y may be written '(C D E).  Suppose we wish to
replace the right-most tip of x by the entire tree y.  This is denoted
(app x y), where app stands for "append".

We can define app with:

     (defun app (x y)                           ; Concatenate x and y.
       (declare (type (satisfies true-listp) x)); We expect x to end in NIL.
       (cond ((endp x) y)                       ; If x is empty, return y.
             (t (cons (car x)                   ; Else, copy first node
                      (app (cdr x) y)))))       ;  and recur into next.

If you defined this function in some Common Lisp, then to run app on the
x and y above you could then type

     (app '(A B) '(C D E))

and Common Lisp will print the result (A B C D E).

Next on the Walking Tour:  An Example of ACL2 in Use

An Example of ACL2 in Use    An Example of ACL2 in Use

Next on the Walking Tour:  How To Find Out about ACL2 Functions

To introduce you to ACL2 we will consider the app function discussed in
the Common Lisp page, except we will omit for the moment the declare
form, which in ACL2 is called a guard.

Guards are arbitrary ACL2 terms that express the "intended domain" of
functions.  In that sense, guards are akin to type signatures.  However,
Common Lisp and ACL2 are untyped programming languages: while the
language supports several different data types and the types of objects
can be determined by predicates at runtime, any type of object may be
passed to any function.  Thus, guards are "extra-logical."  Recognizing
both the practical and intellectual value of knowing that your
functions are applied to the kinds of objects you intend, ACL2 imposes
guards on Common Lisp and provides a means of proving that functions
are used as intended.  But the story is necessarily complicated and we
do not recommend it to the new user.  Get used to the fact that any
ACL2 function may be applied to any objects and program accordingly.
Read about guards later.

Here is the definition again

     (defun app (x y)
       (cond ((endp x) y)
             (t (cons (car x)
                      (app (cdr x) y)))))

The next few stops along the Walking Tour will show you

       * how to use the ACL2 documentation,
       * what happens when the above definition is submitted to ACL2,
       * what happens when you evaluate calls of app,
       * what one simple theorem about app looks like,
       * how ACL2 proves the theorem, and
       * how that theorem can be used in another proof.

Along the way we will talk about the definitional principle, types, the
ACL2 read-eval-print loop, and how the theorem prover works.

When we complete this part of the tour we will return briefly to the
notion of guards and revisit several of the topics above in that
context.

Next on the Walking Tour:  How To Find Out about ACL2 Functions

Analyzing Common Lisp Models    Analyzing Common Lisp Models

To analyze a model you must be able to reason about the operations and
relations involved.  Perhaps, for example, some aspect of the model
depends upon the fact that the concatenation operation is associative.

In any Common Lisp you can confirm that

     (app '(A B) (app '(C D) '(E F)))

and

     (app (app '(A B) '(C D)) '(E F)))

both evaluate to the same thing, (A B C D E F).

But what distinguishes ACL2 (the logic) from applicative Common Lisp
(the language) is that in ACL2 you can prove that the concatenation
function app is associative when its arguments are true-lists, whereas
in Common Lisp all you can do is test that proposition.

That is, in ACL2 it makes sense to say that the following formula is a
"theorem."

     Theorem Associativity of App
     (implies (and (true-listp a)
                   (true-listp b))
              (equal (app (app a b) c)
                     (app a (app b c))))

Theorems about the properties of models are proved by symbolically
manipulating the operations and relations involved.  If the
concatenation of sequences is involved in your model, then you may well
need the theorem above in order to that your model has some particular
property.

Common Lisp    Common Lisp

Next on the Walking Tour:  An Example Common Lisp Function Definition

The logic of ACL2 is based on Common Lisp.

Common Lisp is the standard list processing programming language.  It is
documented in: Guy L. Steele, Common Lisp The Language, Digital Press,
12 Crosby Drive, Bedford, MA 01730, 1990.  See also
`http://www.cs.cmu.edu/Web/Groups/AI/html/cltl/cltl2.html'.

ACL2 formalizes only a subset of Common Lisp.  It includes such
familiar Lisp functions as cons, car and cdr for creating and
manipulating list structures, various arithmetic primitives such as +,
*, expt and <=, and intern and symbol-name for creating and manipulating
symbols.  Control primitives include cond, case and if, as well as
function call, including recursion.  New functions are defined with
defun and macros with defmacro.  See PROGRAMMING <> for a list
of the Common Lisp primitives supported by ACL2.

ACL2 supports five of Common Lisp's datatypes:

* the precisely represented, unbounded numbers (integers, rationals,
and the complex numbers with rational components, called the "complex
rationals" here),

* the characters with ASCII codes between 0 and 255

* strings of such characters

* symbols (including packages)

* conses

ACL2 is a very small subset of full Common Lisp.  ACL2 does not include
the Common Lisp Object System (CLOS), higher order functions, circular
structures, and other aspects of Common Lisp that are non-applicative.
Roughly speaking, a language is applicative if it follows the rules of
function application.  For example, f(x) must be equal to f(x), which
means, among other things, that the value of f must not be affected by
"global variables" and the object x must not change over time.

Next on the Walking Tour:  An Example Common Lisp Function Definition

Common Lisp as a Modeling Language    Common Lisp as a Modeling Language

In ACL2 we have adopted Common Lisp as the basis of our modeling
language.  If you have already read our brief note on Common Lisp and
recall the example of app, please proceed.  Otherwise see Common Lisp
for an exceedingly brief introduction to Common Lisp and then
come back here.

In Common Lisp it is very easy to write systems of formulas that
manipulate discrete, inductively constructed data objects.  In building
a model you might need to formalize the notion of sequences and define
such operations as concatenation, length, whether one is a permutation
of the other, etc.  It is easy to do this in Common Lisp.  Furthermore,
if you have a Common Lisp "theory of sequences" you can run the
operations and relations you define.  That is, you can execute the
functions on concrete data to see what results your formulas produce.

If you define the function app as shown above and then type

     (app '(A B) '(C D E))

in any Common Lisp, the answer will be computed and will be (A B C D E).

The executable nature of Common Lisp and thus of ACL2 is very handy when
producing models.

But executability is not enough for a modeling language because the
purpose of models is to permit analysis.

See Analyzing Common Lisp Models to continue.

Conversion    Conversion to Uppercase

When symbols are read by Common Lisp they are converted to upper case.
Note carefully that this remark applies to the characters in _symbols_.
The characters in strings are not converted upper case.

To type a symbol containing lower case characters you can enclose the
symbol in vertical bars, as in |AbC| or you can put a "backslash"
before each lower case character you wish to preserve, as in A\bC.
|AbC| and A\bC are two different ways of writing the same symbol (just
like 2/4 and 1/2 are two different ways of writing the same rational
and 123 and 0123 are two different ways to write the same natural
number).  The symbol has three characters in its name, the middle one
of which is a lower case b.

Corroborating Models    Corroborating Models

Next on the Flying Tour:  Models of Computer Hardware and Software

After producing a model, it must be corroborated against reality.  The
Falling Body Model has been corroborated by a vast number of
experiments in which the time and distance were measured and compared
according to the formula.  In general all models must be corroborated
by experiment.

The Falling Body Model can be derived from deeper models, namely
Newton's laws of motion and the assertion that, over the limited
distances concerned, graviation exerts a constant acceleration on the
object.  When the model in question can be derived from other models,
it is the other models that are being corroborated by our experiments.

Because nature is not formal, we cannot prove that our models of it are
correct.  All we can do is test our models against nature's behavior.

Such testing often exposes restrictions on the applicability of our
models.  For example, the Falling Body Model is inaccurate if air
resistance is significant.  Thus, we learn not to use that model to
predict how long it takes a feather to fall from a 200 foot tower in
the earth's atmosphere.

In addition, attempts at corroboration might reveal that the model is
actually incorrect.  Careful measurements might expose the fact that the
gravitational force increases as the body falls closer to earth.  Very
careful measurements might reveal relativistic effects.  Technically,
the familiar Falling Body Model is just wrong, even under excessive
restrictions such as "in a perfect vacuum" and "over small distances."
But it is an incredibly useful model nonetheless.

There are several morals here.

Models need not be complete to be useful.

Models need not be perfectly accurate to be useful.

The user of a model must understand its limitations.

Next on the Flying Tour:  Models of Computer Hardware and Software

Evaluating App on Sample Input    Evaluating App on Sample Input

Next on the Walking Tour:  The Associativity of App

     ACL2 !>(app nil '(x y z))
     (X Y Z)

     ACL2 !>(app '(1 2 3) '(4 5 6 7))
     (1 2 3 4 5 6 7)

     ACL2 !>(app '(a b c d e f g) '(x y z))   ; see Conversion for an explanation
     (A B C D E F G X Y Z)

     ACL2 !>(app (app '(1 2) '(3 4)) '(5 6))
     (1 2 3 4 5 6)

     ACL2 !>(app '(1 2) (app '(3 4) '(5 6)))
     (1 2 3 4 5 6)

     ACL2!>(let ((a '(1 2))
                 (b '(3 4))
                 (c '(5 6)))
             (equal (app (app a b) c)
                    (app a (app b c))))
     T

As we can see from these examples, ACL2 functions can be executed more
or less as Common Lisp.

The last three examples suggest an interesting property of app.

Next on the Walking Tour:  The Associativity of App

Flawed Induction Candidates in App Example    Flawed Induction Candidates in App Example

Induction on a is unflawed: every occurrence of a in the conjecture

     (equal (app (app a b) c)
            (app a (app b c)))

is in a position being recursively decomposed!

Now look at the occurrences of b.  The first (shown in bold below) is
in a position that is held constant in the recursion of (app a b).  It
would be "bad" to induct on b here.

     (equal (app (app a b) c)
            (app a (app b c)))

Free Variables in Top-Level Input    Free Variables in Top-Level Input

     ACL2 !>(equal (app (app a b) c)
                   (app a (app b c))))

     ACL2 Error in TOP-LEVEL:  Global variables, such as C, B, and A, are
     not allowed. See :DOC ASSIGN and :DOC @.

ACL2 does not allow "global variables" in top-level input.  There is no
"top-level binding environment" to give meaning to these variables.

Thus, expressions involving no variables can generally be evaluated,

     ACL2 !>(equal (app (app '(1 2) '(3 4)) '(5 6))
                   (app '(1 2) (app '(3 4) '(5 6))))
     (1 2 3 4 5 6)

but expressions containing variables cannot.

There is an exception to this rule.  References to "single-threaded
objects" may appear in top-level forms.  See STOBJ <>.  A
single-threaded object is an ACL2 object, usually containing many
fields, whose use is syntactically restricted so that it may be given
as input only to certain functions and must be returned as output by
certain functions.  These restrictions allow single- threaded objects
to be efficiently manipulated.  For example, only a single copy of the
object actually exists, even though from a logical perspective one
might expect the object to be "copied on write."

The most commonly used single-threaded object in ACL2 is the ACL2 system
state, whose current value is always held in the variable state <>.

ACL2 provides a way for you to use state to save values of computations
at the top-level and refer to them later.  See assign <> and @ <>.

Functions for Manipulating these Objects    Functions for Manipulating these Objects

Next on the Flying Tour:  Modeling in ACL2

Consider a typical "stack" of control frames.

Suppose the model required that we express the idea of "the most recent
frame whose return program counter points into MAIN."

The natural expression of this notion involves

function application -- "fetch the return-pc of this frame"

case analysis --  "if the pc is MAIN, then ..."

iteration or recursion -- "pop this frame off and repeat."

The designers of ACL2 have taken the position that a programming
language is the natural language in which to define such notions,
provided the language has a mathematical foundation so that models can
be analyzed and properties derived logically.

Common Lisp is the language supported by ACL2.  To be precise, a small
applicative subset of Common Lisp is the language supported by ACL2.

Next on the Flying Tour:  Modeling in ACL2

Guards    Guards

Common Lisp functions are partial; they are not defined for all possible
inputs.  But ACL2 functions are total.  Roughly speaking, the logical
function of a given name in ACL2 is a completion of the Common Lisp
function of the same name obtained by adding some arbitrary but
"natural" values on arguments outside the "intended domain" of the
Common Lisp function.

ACL2 requires that every ACL2 function symbol have a "guard," which may
be thought of as a predicate on the formals of the function describing
the intended domain.  The guard on the primitive function car <>, for
example, is (or (consp x) (equal x nil)), which requires the argument to
be either an ordered pair or nil.  We will discuss later how to specify
a guard for a defined function; when one is not specified, the guard is
t which is just to say all arguments are allowed.

But guards are entirely extra-logical: they are not involved in the
axioms defining functions.  If you put a guard on a defined function,
the defining axiom added to the logic defines the function on all
arguments, not just on the guarded domain.

So what is the purpose of guards?

The key to the utility of guards is that we provide a mechanism, called
"guard verification," for checking that all the guards in a formula are
true.  See VERIFY-GUARDS.  This mechanism will attempt to prove
that all the guards encountered in the evaluation of a guarded function
are true every time they are encountered.

For a thorough discussion of guards, see the paper [km97] in the ACL2
bibliography.

Guessing the Type of a Newly Admitted Function    Guessing the Type of a Newly Admitted Function

When a function is admitted to the logic, ACL2 tries to "guess" what
type of object it returns.  This guess is codified as a term that
expresses a property of the value of the function.  For app the term is

     (OR (CONSP (APP X Y))
         (EQUAL (APP X Y) Y))

which says that app returns either a cons or its second argument.  This
formula is added to ACL2's rule base as a type-prescription <> rule.
Later we will discuss how rules are used by the ACL2 theorem prover.
The point here is just that when you add a definition, the data base of
rules is updated, not just by the addition of the definitional axiom,
but by several new rules.

You should now return to the Walking Tour.

Guiding the ACL2 Theorem Prover    Guiding the ACL2 Theorem Prover

Next on the Walking Tour:  ACL2 as an Interactive Theorem Prover (cont)

Now that you have seen the theorem prover in action you might be
curious as to how you guide it.

Look at the picture above.  It is meant to suggest that Q is an
important lemma needed for the proof of P.  Note that to lead the
prover to the proof of P the user first proves Q.  In a way, the
formulation and proof of Q is a hint to the prover about how to prove P.

The user usually doesn't think of Q or recognize the need to prove it
separately until he or she sees the theorem prover fail to prove P
without it "knowing" Q.

The way the user typically discovers the need for Q is to look at failed
proofs.

Next on the Walking Tour:  ACL2 as an Interactive Theorem Prover (cont)

Hey Wait!  Is ACL2 Typed or Untyped(Q)    Hey Wait!  Is ACL2 Typed or Untyped?

The example

     ACL2 !>(app 7 27)

     ACL2 Error in TOP-LEVEL:  The guard for the function symbol ENDP, which
     is (OR (CONSP X) (EQUAL X NIL)), is violated by the arguments in the
     call (ENDP 7).

illustrates the fact that while ACL2 is an untyped language the ACL2
evaluator can be configured so as to check "types" at runtime.  We
should not say "types" here but "guards."  See Undocumented Topic
for a discussion of guards.

The guard on endp <> requires its argument to be a true list.  Since 7
is not a true list, and since ACL2 is checking guards in this example,
an error is signaled by ACL2.  How do you know ACL2 is checking guards?
Because the prompt tells us (see About the Prompt) with its "!".

How Long Does It Take to Become an Effective User(Q)    How Long Does It Take to Become an Effective User?

Next on the Flying Tour:  Other Requirements

We expect that a talented undergraduate majoring in computer science (or
perhaps mathematics) will probably take several weeks to become an
effective ACL2 user.  The time will depend, of course, on that
student's familiarity with logic (or formal methods) and Lisp
programming, as well as willingness to read and study the ACL2 User's
Manual.

Of course, it is critical to do some projects in order to gain
proficiency.  (Hence access to an ACL2 implementation is also a
requirement, for example by downloading and installing following links
from the ACL2 home page.)  But it is critical to start with "toy"
projects before tackling a "grand challenge."

Next on the Flying Tour:  Other Requirements

How To Find Out about ACL2 Functions    How To Find Out about ACL2 Functions

Next on the Walking Tour:  How To Find Out about ACL2 Functions (cont)

Most ACL2 primitives are documented.  Here is the definition of app
again, with the documented topics highlighted.  <> All of the links
below lead into the ACL2 reference manual.  So follow these links if you
wish, but use your Back Button to return here!

     (defun app (x y)
       (cond ((endp x) y)
             (t (cons (car x)
                      (app (cdr x) y)))))

By following the link on endp <> we see that it is a Common Lisp
function and is defined to be the same as atom <>, which recognizes
non-conses.  But endp has a guard.  Since we are ignorning guards for
now, we'll ignore the guard issue on endp.

So this definition reads "to app x and y: if x is an atom, return y;
otherwise, app (cdr x) and y and then cons (car x) onto that."

Next on the Walking Tour:  How To Find Out about ACL2 Functions (cont)

How To Find Out about ACL2 Functions (cont)    How To Find Out about ACL2 Functions (cont)

Next on the Walking Tour:  The Admission of App

You can always use the Index <> icon below to find the documentation of
functions.  Try it.  Click on the Index icon below.  Then use the Find
command of your browser to find "endp" in that document and follow the
link.  But remember to come back here.

The ACL2 documentation is also available via Emacs' TexInfo, allowing
you to explore the hyperlinked documentation in the comfort of a text
editor that can also interact with ACL2.

In addition, runtime images of ACL2 have the hyperlinked text as a
large ACL2 data structure that can be explored with ACL2's :doc
command.  If you have ACL2 running, try the command :doc endp.

Another way to find out about ACL2 functions, if you have an ACL2 image
available, is to use the command :args <> which prints the formals,
type, and guard of a function symbol.

Of course, the ACL2 documentation can also be printed out as a very
long book but we do not recommend that!  See the ACL2 Home Page to
download the Postscript.

Now let's continue with app.

Next on the Walking Tour:  The Admission of App

Modeling in ACL2    Modeling in ACL2

Next on the Flying Tour:  Running Models

Below we define mc(s,n) to be the function that single-steps n times
from a given starting state, s.  In Common Lisp, "mc(s,n)" is written
(mc s n).

     (defun mc (s n)                     ; To step s n times:
      (if (zp n)                         ; If n is 0
          s                              ;    then return s
          (mc (single-step s) (- n 1)))) ;    else step single-step(s)
                                                           n-1 times.

This is an example of a formal model in ACL2.

Next on the Flying Tour:  Running Models

Models in Engineering    Models in Engineering

Frequently, engineers use mathematical models.  Use of such models
frequently lead to

better designs,

faster completion of acceptable products, and

reduced overall cost,

because models allow the trained user to study the design before it is
built and analyze its properties.  Usually, testing and analyzing a
model is cheaper and faster than fabricating and refabricating the
product.

Models of Computer Hardware and Software    Models of Computer Hardware and Software

Next on the Flying Tour:  A Typical State

Computing machines, whether hardware or software or some combintation,
are frequently modeled as "state machines."

To so model a computing machine we must represent its states as objects
in our mathematical framework.

Transitions are functions or relations on state objects.

In what language shall we define these objects, functions, and
relations?

The mathematical languages we were taught in high school

algebra,

geometry,

trignometry, and

calculus

are often inappropriate for modeling digital systems.  They primarily
let us talk about numbers and continuous functions.

To see what kind of expressive power we need, take a closer look at
what a typical state contains.

Next on the Flying Tour:  A Typical State

Name the Formula Above    Name the Formula Above

When the theorem prover explicitly assigns a name, like *1, to a
formula, it has decided to prove the formula by induction.

Nontautological Subgoals    Prover output omits some details

The theorem prover's proof output is intended to suggest an outline of
the reasoning process employed by its proof engine, which is virtually
always more than is necessary for the ACL2 user.  In particular, the
output often omits subgoals that are sufficiently trivial, including
tautologies.

Numbers in ACL2    Numbers in ACL2

ACL2 numbers are precisely represented and unbounded.  They can be
partitioned into the following subtypes:

     Rationals
      Integers
       Positive integers                3
       Zero                             0
       Negative Integers                -3
      Non-Integral Rationals
       Positive Non-Integral Rationals  19/3
       Negative Non-Integral Rationals  -22/7
     Complex Rational Numbers           #c(3 5/2) ; = 3+(5/2)i

Signed integer constants are usually written (as illustrated above) as
sequences of decimal digits, possibly preceded by + or -.  Decimal
points are not allowed.  Integers may be written in binary, as in #b1011
(= 23) and #b-111 (= -7).  Octal may also be used, #o-777 = -511.
Non-integral rationals are written as a signed decimal integer and an
unsigned decimal integer, separated by a slash.  Complex rationals are
written as #c(rpart ipart) where rpart and ipart are rationals.

Of course, 4/2 = 2/1 = 2 (i.e., not every rational written with a slash
is a non-integer).  Similarly, #c(4/2 0) = #c(2 0) = 2.

The common arithmetic functions and relations are denoted by +, -, *,
/, =, <, <=, > and >=.  However there are many others, e.g., floor,
ceiling, and lognot.  We suggest you see PROGRAMMING <> where
we list all of the primitive ACL2 functions.  Alternatively, see any
Common Lisp language documentation.

The primitive predicates for recognizing numbers are illustrated below.
The following ACL2 function will classify an object, x, according to
its numeric subtype, or else return 'NaN (not a number).  We show it
this way just to illustrate programming in ACL2.

     (defun classify-number (x)
       (cond ((rationalp x)
              (cond ((integerp x)
                     (cond ((< 0 x) 'positive-integer)
                           ((= 0 x) 'zero)
                           (t 'negative-integer)))
                    ((< 0 x) 'positive-non-integral-rational)
                    (t 'negative-non-integral-rational)))
             ((complex-rationalp x) 'complex-rational)
             (t 'NaN)))

On the Naming of Subgoals    On the Naming of Subgoals

Subgoal *1/2 is the induction step from the scheme, obtained by
instantiating the scheme with our conjecture.

We number the cases "backward", so this is case "2" of the proof of
"*1".  We number them backward so you can look at a subgoal number and
get an estimate for how close you are to the end.

Other Requirements    Other Requirements

Next on the Flying Tour:  The End of the Flying Tour

ACL2 is distributed on the Web without fee.

There is a License agreement, GPL Version 2 (see
`http://www.gnu.org/licenses/gpl-2.0.html'), as indicated near the top
of each source file.

ACL2 currently runs on Unix, Linux, Windows, and Macintosh OS X
operating systems.

It can be built in any of the following Common Lisps:

       * Allegro Common Lisp,
       * CCL (formerly OpenMCL)
       * CLISP,
       * CMU Common Lisp,
       * GCL (Gnu Common Lisp),
       * LispWorks, and
       * SBCL (Steel Bank Common Lisp)

Next on the Flying Tour:  The End of the Flying Tour

Overview of the Expansion of ENDP in the Base Case    Overview of the Expansion of ENDP in the Base Case

Subgoal *1/1 is the Base Case of our induction.  It simplifies to
Subgoal *1/1' by expanding the ENDP term in the hypothesis, just as we
saw in the earlier proof of Subgoal *1/2.

Overview of the Expansion of ENDP in the Induction Step    Overview of the Expansion of ENDP in the Induction Step

In this message the system is saying that Subgoal *1/2 has been
rewritten to the Subgoal *1/2', by expanding the definition of endp.
This is an example of simplification, one of the main proof techniques
used by the theorem prover.

See The Expansion of ENDP in the Induction Step (Step 0) if you
would like to step through the simplification of Subgoal *1/2.

Overview of the Final Simplification in the Base Case    Overview of the Final Simplification in the Base Case

The But is our signal that the goal is proved.

See The Final Simplification in the Base Case (Step 0) to step
through the proof.  It is very simple.

Overview of the Proof of a Trivial Consequence    Overview of the Proof of a Trivial Consequence

Next on the Walking Tour:  The End of the Walking Tour

     ACL2 !>(defthm trivial-consequence
              (equal (app (app (app (app x1 x2) (app x3 x4)) (app x5 x6)) x7)
                     (app x1 (app (app x2 x3) (app (app x4 x5) (app x6 x7))))))

     ACL2 Warning [Subsume] in ( DEFTHM TRIVIAL-CONSEQUENCE ...):  The previously
     added rule ASSOCIATIVITY-OF-APP subsumes the newly proposed :REWRITE
     rule TRIVIAL-CONSEQUENCE, in the sense that the old rule rewrites a
     more general target.  Because the new rule will be tried first, it
     may nonetheless find application.

     By the simple :rewrite rule ASSOCIATIVITY-OF-APP we reduce the conjecture
     to

     Goal'
     (EQUAL (APP X1
                 (APP X2
                      (APP X3 (APP X4 (APP X5 (APP X6 X7))))))
            (APP X1
                 (APP X2
                      (APP X3 (APP X4 (APP X5 (APP X6 X7))))))).

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

     Q.E.D.

     Summary
     Form:  ( DEFTHM TRIVIAL-CONSEQUENCE ...)
     Rules: ((:REWRITE ASSOCIATIVITY-OF-APP)
             (:FAKE-RUNE-FOR-TYPE-SET NIL))
     Warnings:  Subsume
     Time:  0.20 seconds (prove: 0.02, print: 0.00, other: 0.18)
      TRIVIAL-CONSEQUENCE

You might explore the links before moving on.

Next on the Walking Tour:  The End of the Walking Tour

Overview of the Simplification of the Base Case to T    Overview of the Simplification of the Base Case to T

Next on the Walking Tour:  The End of the Proof of the Associativity of App

     Subgoal *1/1
     (IMPLIES (ENDP A)
              (EQUAL (APP (APP A B) C)
                     (APP A (APP B C)))).

     By the simple :definition ENDP we reduce the conjecture to

     Subgoal *1/1'
     (IMPLIES (NOT (CONSP A))
              (EQUAL (APP (APP A B) C)
                     (APP A (APP B C)))).

     But simplification reduces this to T, using the :definition APP and
     primitive type reasoning.

Next on the Walking Tour:  The End of the Proof of the Associativity of App

Overview of the Simplification of the Induction Conclusion    Overview of the Simplification of the Induction Conclusion

In this message the system is saying that Subgoal *1/2' has been
rewritten to T using the rules noted.  The word "But" at the beginning
of the sentence is a signal that the goal has been proved.

See The Simplification of the Induction Conclusion (Step 0) to
step through the proof of Subgoal *1/2'.

Overview of the Simplification of the Induction Step to T    Overview of the Simplification of the Induction Step to T

Next on the Walking Tour:  Overview of the Simplification of the Base Case to T

     Subgoal *1/2
     (IMPLIES (AND (NOT (ENDP A))
                   (EQUAL (APP (APP (CDR A) B) C)
                          (APP (CDR A) (APP B C))))
              (EQUAL (APP (APP A B) C)
                     (APP A (APP B C)))).

     By the simple :definition ENDP we reduce the conjecture to

     Subgoal *1/2'
     (IMPLIES (AND (CONSP A)
                   (EQUAL (APP (APP (CDR A) B) C)
                          (APP (CDR A) (APP B C))))
              (EQUAL (APP (APP A B) C)
                     (APP A (APP B C)))).

     But simplification reduces this to T, using the :definition APP, the
     :rewrite rules CDR-CONS and CAR-CONS and primitive type reasoning.

Next on the Walking Tour:  Overview of the Simplification of the Base Case to T

Perhaps    Perhaps

The theorem prover's proof is printed in real time.  At the time it
prints "Perhaps" it does not know the proof will succeed.

Popping out of an Inductive Proof    Popping out of an Inductive Proof

Recall that our induction scheme (see The Proof of the Associativity of App
to revisit it) had two cases, the induction step
(Subgoal *1/2) and the base case (Subgoal *1/1).  Both have been proved!

Proving Theorems about Models    Proving Theorems about Models

Next on the Flying Tour:  What is Required of the User(Q)

But ACL2 is a logic.  We can prove theorems about the model.

     Theorem.  MC 'mult is a multiplier
     (implies (and (natp x)
                   (natp y))
              (equal (lookup 'z (mc (s 'mult x y) (mclk x)))
                     (* x y))).

This theorem says that a certain program running on the mc machine will
correctly multiply any two natural numbers.

It is a statement about an infinite number of test cases!

We know it is true about the model because we proved it.

Of course, models of actual machines usually only accept a finite
number of different inputs.  For example, engineers at Advanced Micro
Devices (AMD), Centaur, and IBM have ACL2 models of floating point
units that operate on double precision IEEE floating point numbers.
These are finite models.  But the size of their inputs is sufficiently
large that they are verified by the same mathematical methods used to
prove theorems about infinite state systems like our little mc.

Next on the Flying Tour:  What is Required of the User(Q)

Revisiting the Admission of App    Revisiting the Admission of App

Next on the Walking Tour:  Evaluating App on Sample Input

Here is the definition of app again with certain parts highlighted.  If
you are taking the Walking Tour, please read the text carefully and
click on each of the links below, except those marked <>.  Then come
back here.

     ACL2 !>(defun app (x y)
       (cond ((endp x) y)
             (t (cons (car x)
                      (app (cdr x) y)))))

     The admission of 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 APP is described by the theorem (OR
     (CONSP (APP X Y)) (EQUAL (APP X Y) Y)).  We used primitive type
     reasoning.

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

Next on the Walking Tour:  Evaluating App on Sample Input

Rewrite Rules are Generated from DEFTHM Events    Rewrite Rules are Generated from DEFTHM Events

Next on the Walking Tour:  You Must Think about the Use of a Formula as a Rule

By reading the documentation of defthm <> (and especially of its
:rule-classes <> argument) you would learn that when we submitted the
command

     (defthm associativity-of-app
       (equal (app (app a b) c)
              (app a (app b c))))

we not only command the system to prove that app is an associative
function but

       * we commanded it to use that fact as a rewrite rule.

That means that every time the system encounters a term of the form

     (app (app x y) z)

it will replace it with

     (app x (app y z))!

Next on the Walking Tour:  You Must Think about the Use of a Formula as a Rule

Running Models    Running Models

Next on the Flying Tour:  Symbolic Execution of Models

Suppose the machine being modeled is some kind of arithmetic unit.
Suppose the model can be initialized so as to multiply x times y and
leave the answer in z.  Then if we initialize s to multiply with x=5
and y=7 and run the machine long enough, we can read the answer 35 in
the final state.

Because ACL2 is a programming language, our model can be run or
executed.

If you defined the model in ACL2 and then typed

     (lookup 'z (mc (s 'mult 5 7) 29))

then ACL2 would compute 35.  (Here we assume that the function s creates
a state ready to run a given application on given inputs x and y.)  You
can emulate or test the model of your machine.

This is obvious because ACL2 is Common Lisp; and Common Lisp is a
programming language.

Next on the Flying Tour:  Symbolic Execution of Models

Subsumption of Induction Candidates in App Example    Subsumption of Induction Candidates in App Example

After collecting induction suggestions from these three terms

     (app a b)

     (app b c)

     (app a (app b c))

the system notices that the first and last suggest the same
decomposition of a: case split on whether a is empty (i.e., (endp a)),
and in the case where it is not empty, recursively process (cdr a).  So
we are left with two ideas about how to induct:

Decompose a as we would to unwind (app a b).

Decompose b as we would to unwind (app b c).

Suggested Inductions in the Associativity of App Example    Suggested Inductions in the Associativity of App Example

To find a plausible induction argument, the system studies the
recursions exhibited by the terms in the conjecture.

Roughly speaking, a call of a recursive function "suggests" an
induction if the argument position decomposed in recursion is occupied
by a variable.

In this conjecture, three terms suggest inductions:

     (app a b)

     (app b c)

     (app a (app b c))

The variable recursively decomposed is indicated in bold.

Symbolic Execution of Models    Symbolic Execution of Models

Next on the Flying Tour:  Proving Theorems about Models

But ACL2 is more than a programming language.

Initialize x to 5 and let y be any legal value.

Because ACL2 is a mathematical language, we can simplify the expression

     (lookup 'z (mc (s 'mult 5 y) 29))

and get (+ y y y y y).  This is symbolic execution because not all of
the parameters are known.

Next on the Flying Tour:  Proving Theorems about Models

The Admission of App    The Admission of App

Next on the Walking Tour:  Revisiting the Admission of App

Here is what it looks like to submit the definition of app to ACL2:

     ACL2 !>(defun app (x y)
       (cond ((endp x) y)
             (t (cons (car x)
                      (app (cdr x) y)))))

     The admission of 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 APP is
     described by the theorem (OR (CONSP (APP X Y)) (EQUAL (APP X Y) Y)).
     We used primitive type reasoning.

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

The text between the lines above is one interaction with the ACL2
command loop.  Interacting with the latest version of ACL2 may not
produce the very same output, but we trust you'll recognize the basics.

Above you see the user's input and how the system responds.  This little
example shows you what the syntax looks like and is a very typical
successful interaction with the definitional principle.

Let's look at it a little more closely.

Next on the Walking Tour:  Revisiting the Admission of App

The Associativity of App    The Associativity of App

Next on the Walking Tour:  The Theorem that App is Associative

     ACL2!>(let ((a '(1 2))
                 (b '(3 4))
                 (c '(5 6)))
             (equal (app (app a b) c)
                    (app a (app b c))))
     T

Observe that, for the particular a, b, and c above, (app (app a b) c)
returns the same thing as (app a (app b c)).  Perhaps app is
associative.  Of course, to be associative means that the above
property must hold for all values of a, b, and c, not just the ones
tested above.

Wouldn't it be cool if you could type

     ACL2!>(equal (app (app a b) c)
                  (app a (app b c)))

and have ACL2 compute the value T?  Well, you can't!  If you try it,
you'll get an error message!  The message says we can't evaluate that
form because it contains free variables, i.e., variables not given
values.  See Free Variables in Top-Level Input to see the
message.

We cannot evaluate a form on an infinite number of cases.  But we can
prove that a form is a theorem and hence know that it will always
evaluate to true.

Next on the Walking Tour:  The Theorem that App is Associative

The Base Case in the App Example    The Base Case in the App Example

This formula is the Base Case.  It consists of two parts, a test
identifying the non-inductive case and the conjecture to prove.

     (IMPLIES (ENDP A)                 ; Test
              (:P A B C))              ; Conjecture

When we prove this we can assume

       * A is empty

and we have to prove the conjecture for A.

The End of the Flying Tour    The End of the Flying Tour

This completes the Flying Tour.

We recommend that you now take A Walking Tour of ACL2.

Thanks.
Matt Kaufmann and J Moore

Next on the Walking Tour:  A Walking Tour of ACL2

The End of the Proof of the Associativity of App    The End of the Proof of the Associativity of App

Next on the Walking Tour:  Guiding the ACL2 Theorem Prover

     That completes the proof of *1.

     Q.E.D.

     Summary
     Form:  ( DEFTHM ASSOCIATIVITY-OF-APP ...)
     Rules: ((:REWRITE CDR-CONS)
             (:REWRITE CAR-CONS)
             (:DEFINITION NOT)
             (:DEFINITION ENDP)
             (:FAKE-RUNE-FOR-TYPE-SET NIL)
             (:DEFINITION APP))
     Warnings:  None
     Time:  0.27 seconds (prove: 0.10, print: 0.05, other: 0.12)
      ASSOCIATIVITY-OF-APP

Next on the Walking Tour:  Guiding the ACL2 Theorem Prover

The End of the Walking Tour    The End of the Walking Tour

This completes the Walking Tour.

We intend to document many other parts of the system this way, but we
just haven't gotten around to it.

To start the two tours over again from the beginning, click on the icons
below.  If you are really interested in learning how to use ACL2, we
recommend that you repeat each tour at least once more to explore
branches of the tour that you might have missed.

If you want to learn how to use the theorem prover, we now recommend
that you devote the time necessary to work your way through the
extended introduction to how to use the prover.

See INTRODUCTION-TO-THE-THEOREM-PROVER.

This will explain how to interact with ACL2 and has some sample
problems for you to solve including some challenge proofs to make ACL2
find.

We hope you enjoy ACL2.  We do.

Matt Kaufmann and J Strother Moore

Next on the Flying Tour:  A Flying Tour of ACL2 Next on the
Walking Tour:  A Walking Tour of ACL2

The Event Summary    The Event Summary

At the conclusion of most events (see About the Prompt for a
brief discussion of events or see EVENTS <>), ACL2 prints a
summary.  The summary for app is:

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

The "rules" listed are those used in function admission or proof
summarized.  What is actually listed are "runes" (see RUNE) <>)
which are list-structured names for rules in the ACL2 data base or
"world" <>.  Using theories <> you can "enable" and "disable" rules so
as to make them available (or not) to the ACL2 theorem prover.

The "warnings" mentioned (none are listed for app) remind the reader
whether the event provoked any warnings.  The warnings themselves would
have been printed earlier in the processing and this part of the
summary just names the earlier warnings printed.

The "time" indicates how much processing time was used and is divided
into three parts: the time devoted to proof, to printing, and to
syntactic checks, pre-processing and data base updates.  Despite the
fact that ACL2 is an applicative language it is possible to measure
time with ACL2 programs.  The state <> contains a clock.  The times are
printed in decimal notation but are actually counted in integral units.
Note that each time is a runtime, also known as a cpu time, as opposed
to being a real time, also known as a wall clock time.

The final APP is the value of the defun command and was printed by the
read-eval-print loop.  The fact that it is indented one space is a
subtle reminder that the command actually returned an "error triple",
consisting of a flag indicating (in this case) that no error occurred,
a value (in this case the symbol APP), and the final state <>).  See
LD-POST-EVAL-PRINT <> for some details.  If you really want to
follow that link, however, you might see LD <> first.

You should now return to the Walking Tour.

The Expansion of ENDP in the Induction Step (Step 0)    The Expansion of ENDP in the Induction Step (Step 0)

     Subgoal *1/2
     (IMPLIES (AND (NOT (ENDP A))
                   (EQUAL (APP (APP (CDR A) B) C)
                          (APP (CDR A) (APP B C))))
              (EQUAL (APP (APP A B) C)
                     (APP A (APP B C)))).

Click on the link above (the open parenthesis before ENDP) to replace
(ENDP A) by its definition.

The Expansion of ENDP in the Induction Step (Step 1)    The Expansion of ENDP in the Induction Step (Step 1)

     Subgoal *1/2
     (IMPLIES (AND (NOT (NOT (CONSP A)))
                   (EQUAL (APP (APP (CDR A) B) C)
                          (APP (CDR A) (APP B C))))
              (EQUAL (APP (APP A B) C)
                     (APP A (APP B C)))).

The bold text is the instantiated definition of ENDP.

Now click on the link above to simplify (NOT (NOT (CONSP A)))

The Expansion of ENDP in the Induction Step (Step 2)    The Expansion of ENDP in the Induction Step (Step 2)

     Subgoal *1/2'
     (IMPLIES (AND (CONSP A)
                   (EQUAL (APP (APP (CDR A) B) C)
                          (APP (CDR A) (APP B C))))
              (EQUAL (APP (APP A B) C)
                     (APP A (APP B C)))).

Note that this is Subgoal *1/2'.

You may see Overview of the Simplification of the Induction Step to T
to return to the main proof.

The Falling Body Model    The Falling Body Model

One particularly famous and very simple model is the equation of a
falling body: the distance d an object falls is proportional to the
square of the time t.  If the time is measured in seconds and the
distance in feet, the equation relating these two is

            2
     d = 16t

This equation is a model of falling objects.  It can be used to predict
how long it takes a cannonball to fall from the top of a 200 foot tower
(3.5 seconds).  This might be important if your product is designed to
drop cannonballs on moving targets.

The Final Simplification in the Base Case (Step 0)    the Final Simplification in the Base Case (Step 0)

     Subgoal *1/1'
     (IMPLIES (NOT (CONSP A))
              (EQUAL (APP (APP A B) C)
                     (APP A (APP B C)))).

Click on the link above to replace (APP A B) by its definition.  Note
that the hypothesis (NOT (CONSP A)) allows us to simplify the IF in APP
to its false branch this time.

The Final Simplification in the Base Case (Step 1)    the Final Simplification in the Base Case (Step 1)

     Subgoal *1/1'
     (IMPLIES (NOT (CONSP A))
              (EQUAL (APP B C)
                     (APP A (APP B C)))).

Click on the link above to expand the definition of APP.  Again, we
come out through the false branch because of the hypothesis.

The Final Simplification in the Base Case (Step 2)    the Final Simplification in the Base Case (Step 2)

     Subgoal *1/1'
     (IMPLIES (NOT (CONSP A))
              (EQUAL (APP B C)
                     (APP B C))).

Click on the link above to use the Axiom (EQUAL x x) = t

The Final Simplification in the Base Case (Step 3)    the Final Simplification in the Base Case (Step 3)

     Subgoal *1/1'
     (IMPLIES (NOT (CONSP A))
              T)

Now that its conclusion is identically T the IMPLIES will simplify to T
(not shown) and we are done with Subgoal *1/1'.

You may see Overview of the Simplification of the Base Case to T
to return to the main proof.

The First Application of the Associativity Rule    The First Application of the Associativity Rule

So here we see our associativity rule being used!

The rewriter sweeps the conjecture in a leftmost innermost fashion,
applying rewrite rules as it goes.

The associativity rule is used many times in this sweep.  The first
"target" is highlighted below.  Click on it to see what happens:

     Current Conjecture:
     (equal (app (app (app (app x1 x2) (app x3 x4)) (app x5 x6)) x7)
            (app x1 (app (app x2 x3) (app (app x4 x5) (app x6 x7)))))

The Induction Scheme Selected for the App Example    The Induction Scheme Selected for the App Example

     (AND
        (IMPLIES (AND (NOT (ENDP A))         ; Induction Step: test
                      (:P (CDR A) B C))      ;  and induction hypothesis
                 (:P A B C))                 ;  implies induction conclusion.
        (IMPLIES (ENDP A) (:P A B C)))       ; Base Case

The formula beginning with this parenthesis is the induction scheme
suggested by (APP A B) applied to (P A B C).

It is a conjunction (AND <>) of two formulas.

The first is the induction step and the second is the base case.

The Induction Step in the App Example    The Induction Step in the App Example

This formula is the Induction Step.  It basically consists of three
parts, a test identifying the inductive case, an induction hypothesis
and an induction conclusion.

     (IMPLIES (AND (NOT (ENDP A))      ; Test
                   (:P (CDR A) B C))   ; Induction Hypothesis
              (:P A B C))              ; Induction Conclusion

When we prove this we can assume

       * A is not empty, and that

       * the associativity conjecture holds for a ``smaller'' version of
         A, namely, (CDR A).

Under those hypotheses we have to prove the associativity conjecture
for A itself.

The Instantiation of the Induction Scheme    The Instantiation of the Induction Scheme

The induction scheme just shown is just an abbreviation for our real
goal.

To obtain our actual goals we have to replace the schema :P by the
associativity conjecture (instantiated as shown in the scheme).

This produces two actual goals, the induction step and the base case.

The Justification of the Induction Scheme    The Justification of the Induction Scheme

This paragraph explains why the induction selected is legal.  The
explanation is basically the same as the explanation for why the
recursion in (APP A B) terminates.

The Proof of the Associativity of App    The Proof of the Associativity of App

Next on the Walking Tour:  Overview of the Simplification of the Induction Step to T

Here is the theorem prover's output when it processes the defthm command
for the associativity of app.  We have highlighted text for which we
offer some explanation, and broken the presentation into several pages.
(The most recent version of ACL2 may print slightly different output
but the basics are the same.)  Just follow the Walking Tour after
exploring the explanations.

However, before exploring this output you should understand that ACL2
users rarely read successful proofs!  Instead, they look at certain
subgoals printed in failed proofs, figure whether and how those
subgoals can be proved, and give ACL2 directions for proving them,
usually by simply proving other lemmas.  Furthermore, to be a good user
of ACL2 you do not have to understand how the theorem prover works.
You just have to understand how to interact with it.  We explain this
in great detail later.  But basically all new users are curious to know
how ACL2 works and this little tour attempts to give some answers, just
to satisfy your curiosity.

     ACL2!>(defthm associativity-of-app
             (equal (app (app a b) c)
                    (app a (app b c))))

     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.

     We will induct according to a scheme suggested by (APP A B).  If we
     let  (:P A B C) denote *1 above then the induction scheme we'll use
     is
     (AND
        (IMPLIES (AND (NOT (ENDP A))
                      (:P (CDR A) B C))
                 (:P A B C))
        (IMPLIES (ENDP A) (:P A B C))).
     This induction is justified by the same argument used to admit APP,
     namely, the measure (ACL2-COUNT A) 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.

Next on the Walking Tour:  Overview of the Simplification of the Induction Step to T

The Q.E.D. Message    The Q.E.D. Message

Q.E.D. stands for "quod erat demonstrandum" which is Latin for "which
was to be demonstrated" and is the signal that a proof is completely
done.

The Rules used in the Associativity of App Proof    The Rules used in the Associativity of App Proof

Note that under Rules we list the runes <> of all the rules used in the
proof.  This list says that we used the rewrite rules CAR-CONS and
CDR-CONS, the definitions of the functions NOT, ENDP and APP, and
primitive type reasoning (which is how we simplified the IF and EQUAL
terms).

For what it is worth, IMPLIES and AND are actually macros <> that are
expanded into IF expressions before the proof ever begins.  The use of
macros is not reported among the rules.

The Simplification of the Induction Conclusion (Step 0)    the Simplification of the Induction Conclusion (Step 0)

     Subgoal *1/2'
     (IMPLIES (AND (CONSP A)
                   (EQUAL (APP (APP (CDR A) B) C)
                          (APP (CDR A) (APP B C))))
              (EQUAL (APP (APP A B) C)
                     (APP A (APP B C)))).

Click on the link above to replace (APP A B) by its definition.

The Simplification of the Induction Conclusion (Step 1)    the Simplification of the Induction Conclusion (Step 1)

     Subgoal *1/2'
     (IMPLIES (AND (CONSP A)
                   (EQUAL (APP (APP (CDR A) B) C)
                          (APP (CDR A) (APP B C))))
              (EQUAL (APP (IF (CONSP A)
                              (CONS (CAR A) (APP (CDR A) B))
                              B)
                          C)
                     (APP A (APP B C)))).

Note that the IF expression above is the simplified body of APP.  But
we know the test (CONSP A) is true, by the first hypothesis.  Click on
the link above to replace the test by T.  Actually this step and several
subsequent ones are done during the simplification of the body of APP
but we want to illustrate the basic principles of simplification without
bothering with every detail.

The Simplification of the Induction Conclusion (Step 10)    the Simplification of the Induction Conclusion (Step 10)

     Subgoal *1/2'
     (IMPLIES (AND (CONSP A)
                   (EQUAL (APP (APP (CDR A) B) C)
                          (APP (CDR A) (APP B C))))
              (EQUAL (APP (APP (CDR A) B) C)
                     (APP (CDR A) (APP B C)))).

Click on the link above to use the Induction Hypothesis (which is the
second of the two hypotheses above and which is identical to the
rewritten conclusion).

The Simplification of the Induction Conclusion (Step 11)    the Simplification of the Induction Conclusion (Step 11)

     Subgoal *1/2'
     (IMPLIES (AND (CONSP A)
                   (EQUAL (APP (APP (CDR A) B) C)
                          (APP (CDR A) (APP B C))))
              T)

Click on the link above to use the definition of IMPLIES.  Since the
conclusion of the implication is now identically T, the implication
simplifies to T.

The Simplification of the Induction Conclusion (Step 12)    the Simplification of the Induction Conclusion (Step 12)

     Subgoal *1/2'
     T

So, indeed, Subgoal *1/2' does simplify to T!

You can see that even in an example as simple as this one, quite a lot
happens in simplification.

You may see Overview of the Simplification of the Induction Step to T
to return to the main proof.

The Simplification of the Induction Conclusion (Step 2)    the Simplification of the Induction Conclusion (Step 2)

     Subgoal *1/2'
     (IMPLIES (AND (CONSP A)
                   (EQUAL (APP (APP (CDR A) B) C)
                          (APP (CDR A) (APP B C))))
              (EQUAL (APP (IF T
                              (CONS (CAR A) (APP (CDR A) B))
                              B)
                          C)
                     (APP A (APP B C)))).

Click on the link above to apply the Axiom (IF T x y) = x.

The Simplification of the Induction Conclusion (Step 3)    the Simplification of the Induction Conclusion (Step 3)

     Subgoal *1/2'
     (IMPLIES (AND (CONSP A)
                   (EQUAL (APP (APP (CDR A) B) C)
                          (APP (CDR A) (APP B C))))
              (EQUAL (APP (CONS (CAR A) (APP (CDR A) B))
                          C)
                     (APP A (APP B C)))).

Click on the link above to expand the definition of APP here.

The Simplification of the Induction Conclusion (Step 4)    the Simplification of the Induction Conclusion (Step 4)

     Subgoal *1/2'
     (IMPLIES (AND (CONSP A)
                   (EQUAL (APP (APP (CDR A) B) C)
                          (APP (CDR A) (APP B C))))
              (EQUAL (IF (CONSP (CONS (CAR A) (APP (CDR A) B)))
                         (CONS (CAR (CONS (CAR A) (APP (CDR A) B)))
                               (APP (CDR (CONS (CAR A) (APP (CDR A) B)))
                                    C))
                         C)
                     (APP A (APP B C)))).

Click on the link above to apply the Axiom (CONSP (CONS x y)) = T.

The Simplification of the Induction Conclusion (Step 5)    the Simplification of the Induction Conclusion (Step 5)

     Subgoal *1/2'
     (IMPLIES (AND (CONSP A)
                   (EQUAL (APP (APP (CDR A) B) C)
                          (APP (CDR A) (APP B C))))
              (EQUAL (IF T
                         (CONS (CAR (CONS (CAR A) (APP (CDR A) B)))
                               (APP (CDR (CONS (CAR A) (APP (CDR A) B)))
                                    C))
                         C)
                     (APP A (APP B C)))).

Click on the link above to apply the Axiom (CAR (CONS x y)) = x.

The Simplification of the Induction Conclusion (Step 6)    the Simplification of the Induction Conclusion (Step 6)

     Subgoal *1/2'
     (IMPLIES (AND (CONSP A)
                   (EQUAL (APP (APP (CDR A) B) C)
                          (APP (CDR A) (APP B C))))
              (EQUAL (IF T
                         (CONS (CAR A)
                               (APP (CDR (CONS (CAR A) (APP (CDR A) B)))
                                    C))
                         C)
                     (APP A (APP B C)))).

Click on the link above to apply the Axiom (CDR (CONS x y)) = y.

The Simplification of the Induction Conclusion (Step 7)    the Simplification of the Induction Conclusion (Step 7)

     Subgoal *1/2'
     (IMPLIES (AND (CONSP A)
                   (EQUAL (APP (APP (CDR A) B) C)
                          (APP (CDR A) (APP B C))))
              (EQUAL (IF T
                         (CONS (CAR A)
                               (APP (APP (CDR A) B)
                                    C))
                         C)
                     (APP A (APP B C)))).

Click on the link above to apply the Axiom (IF T x y) = x.

The Simplification of the Induction Conclusion (Step 8)    the Simplification of the Induction Conclusion (Step 8)

     Subgoal *1/2'
     (IMPLIES (AND (CONSP A)
                   (EQUAL (APP (APP (CDR A) B) C)
                          (APP (CDR A) (APP B C))))
              (EQUAL (CONS (CAR A)
                           (APP (APP (CDR A) B)
                                C))
                     (APP A (APP B C)))).

Click on the link above to expand the definition of APP here.  This
time, we'll do the whole expansion at once, including the
simplification of the resulting IF.  This is how ACL2 actually does it.

The Simplification of the Induction Conclusion (Step 9)    the Simplification of the Induction Conclusion (Step 9)

     Subgoal *1/2'
     (IMPLIES (AND (CONSP A)
                   (EQUAL (APP (APP (CDR A) B) C)
                          (APP (CDR A) (APP B C))))
              (EQUAL (CONS (CAR A)
                           (APP (APP (CDR A) B)
                                C))
                     (CONS (CAR A)
                           (APP (CDR A) (APP B C))))).

Click on the link above to apply the Axiom that (EQUAL (CONS x y) (CONS
u v)) is equal to the conjunction of (EQUAL x u) and (EQUAL y v).  In
this case, (EQUAL x u) is trivial, (EQUAL (CAR A) (CAR A)).

The Summary of the Proof of the Trivial Consequence    The Summary of the Proof of the Trivial Consequence

Note that at the conclusion of the proof, the system reminds you of the
earlier Warning.

It is a good idea, when the Q.E.D. flys by, to see if there were any
Warnings.

The Theorem that App is Associative    The Theorem that App is Associative

Next on the Walking Tour:  The Proof of the Associativity of App

     ACL2!>(defthm associativity-of-app
             (equal (app (app a b) c)
                    (app a (app b c))))

The formula above says app is associative.  The defthm <> command
instructs ACL2 to prove the formula and to name it
associativity-of-app.  Actually, the defthm command also builds the
formula into the data base as a rewrite <> rule, but we won't go into
that just yet.

What we will consider is how the ACL2 theorem prover proves this
formula.

If you proceed you will find the actual output of ACL2 in response to
the command above.  Some of the text is highlighted for the purposes of
the tour.  ACL2 does not highlight its output.

You will note that we sometimes highlight a single open parenthesis.
This is our way of drawing your attention to the subformula that begins
with that parenthesis.  By clicking on the parenthesis you will get an
explanation of the subformula or its processing.

Next on the Walking Tour:  The Proof of the Associativity of App

The Time Taken to do the Associativity of App Proof    The Time Taken to do the Associativity of App Proof

The time it took us to explain this proof may leave the impression that
the proof is complicated.  In a way, it is.  But it happens quickly.

The time taken to do this proof is about 1/10 second.  The rest of the
time (about 2/10 seconds) is spent in pre- and post-processing.

Basically, this proof flashes across your screen before you can read
it; you see the Q.E.D. and don't bother to scroll back to read it.  You
have more important things to do than read successful proofs.

The Tours    The Tours

ACL2 is a very large, multipurpose system.  You can use it as a
programming language, a specification language, a modeling language, a
formal mathematical logic, or a semi-automatic theorem prover, just to
name its most common uses.  It has been used on a number of industrial
applications.  If you're uncertain as to whether your project is
appropriate for ACL2 we urge you to look over this list or contact the
ACL2 developers.

This home page includes all of ACL2's online documentation, which is
quite extensive (over 4 megabytes).  To help ease your introduction to
ACL2, we have built two tours through this documentation.

If you are familiar with at least some of the industrial applications
of ACL2, then you will understand the distance between the simple
examples we talk about in these tours and the kinds of things ACL2
users do with the system.

Newcomers to ACL2 should first take the "Flying Tour."  Then, if you
want to know more, take the "Walking Tour."  On your first reading,
follow the two Tours linearly, clicking only on the icon of the Tour
you're on.  Beware of other links, which might jump you from one tour
to the other or into the reference manual!  Once you've had a coherent
overview of the system, you might quickly repeat both Tours to see if
there are unvisited links you're interested in, using your brower's
Back Button to return to your starting points.

If after all this you want to learn how to use the theorem prover (!),
see INTRODUCTION-TO-THE-THEOREM-PROVER.

To start a tour, click on the appropriate icon below.

Next on the Flying Tour:  A Flying Tour of ACL2 Next on the
Walking Tour:  A Walking Tour of ACL2

For readers using our :DOC or our TexInfo format in Emacs: The tours
will probably be unsatisfying because we use gif files and assume you
can navigate "back."

The WARNING about the Trivial Consequence    The WARNING about the Trivial Consequence

This Warning alerts us to the fact that when treated as a rewrite rule,
the new rule TRIVIAL-CONSEQUENCE, rewrites terms of the same form as a
rule we have already proved, namely ASSOCIATIVITY-OF-APP.

When you see this warning you should think about your rules!

In the current case, it would be a good idea not to make
TRIVIAL-CONSEQUENCE a rule at all.  We could do this with :rule-classes
<> nil.

ACL2 proceeds to try to prove the theorem, even though it printed some
warnings.  The basic assumption in ACL2 is that the user understands
what he or she is doing but may need a little reminding just to manage
a complicated set of facts.

Undocumented Topic    Undocumented Topic

This topic has not yet been documented.  Sorry

Using the Associativity of App to Prove a Trivial Consequence    Using the Associativity of App to Prove a Trivial Consequence

Next on the Walking Tour:  Overview of the Proof of a Trivial Consequence

If we have proved the associativity-of-app rule, then the following
theorem is trivial:

     (defthm trivial-consequence
       (equal (app (app (app (app x1 x2) (app x3 x4)) (app x5 x6)) x7)
              (app x1 (app (app x2 x3) (app (app x4 x5) (app x6 x7))))))

Below we show the proof

Next on the Walking Tour:  Overview of the Proof of a Trivial Consequence

What Is ACL2(Q)    What Is ACL2?

Next on the Flying Tour:  What is a Mathematical Logic(Q)

ACL2 is a mathematical logic together with a mechanical theorem prover
to help you reason in the logic.

The logic is just a subset of applicative Common Lisp.  (This link
takes you off the main route of the tour.  You'll see some Common Lisp
on the tour, so visit this later!)

The theorem prover is an "industrial strength" version of the
Boyer-Moore theorem prover, Nqthm.

Models of all kinds of computing systems can be built in ACL2, just as
in Nqthm, even though the formal logic is Lisp.

Once you've built an ACL2 model of a system, you can run it.

You can also use ACL2 to prove theorems about the model.

Next on the Flying Tour:  What is a Mathematical Logic(Q)

What is Required of the User(Q)    What is Required of the User?

Next on the Flying Tour:  How Long Does It Take to Become an Effective User(Q)

It is not easy to build ACL2 models of complex systems.  To do so, the
user must understand

       * the system being modeled, and

       * ACL2, at least as a programming language.

It is not easy to get ACL2 to prove hard theorems.  To do so, the user
must understand

       * the model,

       * ACL2 as a mathematical logic, and

       * be able to construct a proof (in interaction with ACL2).

ACL2 will help construct the proof but its primary role is to prevent
logical mistakes.  The creative burden -- the mathematical insight into
why the model has the desired property -- is the user's responsibility.

Next on the Flying Tour:  How Long Does It Take to Become an Effective User(Q)

What is a Mathematical Logic(Q)    What is a Mathematical Logic?

Next on the Flying Tour:  What is a Mechanical Theorem Prover(Q)

A mathematical logic is a formal system of formulas (axioms) and rules
for deriving other formulas, called theorems.

A proof is a derivation of a theorem.  To see a concrete proof tree,
see A Trivial Proof.

Why should you care?  The neat thing about Theorems is that they are
"true."  More precisely, if all the axioms are valid and the rules are
validity preserving, then anything derived from the axioms via the
rules is valid.

So, if you want to determine if some formula is true, prove it.

Next on the Flying Tour:  What is a Mechanical Theorem Prover(Q)

What is a Mechanical Theorem Prover(Q)    What is a Mechanical Theorem Prover?

Next on the Flying Tour:  What is a Mechanical Theorem Prover(Q) (cont)

A mechanical theorem prover is a computer program that finds proofs of
theorems.

The ideal mechanical theorem prover is automatic: you give it a formula
and it gives you a proof of that formula or tells you there is no proof.

Unfortunately, automatic theorem provers can be built only for very
simple logics (e.g., propositional calculus) and even then practical
considerations (e.g., how many centuries you are willing to wait) limit
the problems they can solve.

Next on the Flying Tour:  What is a Mechanical Theorem Prover(Q) (cont)

What is a Mechanical Theorem Prover(Q) (cont)    What is a Mechanical Theorem Prover? (cont)

Next on the Flying Tour:  About Models To get around this,
mechanical theorem provers often require help from the user.

See ACL2 as an Interactive Theorem Prover to continue downward.

Next on the Flying Tour:  About Models

You Must Think about the Use of a Formula as a Rule    You Must Think about the Use of a Formula as a Rule

Next on the Walking Tour:  Using the Associativity of App to Prove a Trivial Consequence

This is good and bad.

The good news is that you can program ACL2's simplifier.

The bad news is that when you command ACL2 to prove a theorem you must
give some thought to how that theorem is to be used as a rule!

For example, if after proving associativity-of-app as previously shown,
you engaged in the mathematically trivial act of proving it again but
with the equality reversed, you would have programmed ACL2's rewriter
to loop forever.

You can avoid adding any rule by using the command:

     (defthm associativity-of-app
       (equal (app (app a b) c)
              (app a (app b c)))
       :rule-classes nil)

Next on the Walking Tour:  Using the Associativity of App to Prove a Trivial Consequence

REAL    ACL2(r) support for real numbers

ACL2 supports rational numbers but not real numbers.  However, starting
with Version 2.5, a variant of ACL2 called "ACL2(r)" supports the real
numbers by way of non-standard analysis.  ACL2(r) was conceived and
first implemented by Ruben Gamboa in his Ph.D.  dissertation work,
supervised by Bob Boyer with active participation by Matt Kaufmann.

ACL2(r) has the same source files as ACL2.  After you download ACL2,
you can build ACL2(r) by executing the following command on the command
line in your acl2-sources directory, replacing <your_lisp> with a path
to your Lisp executable:

     make large-acl2r LISP=<your_lisp>

This will create an executable in your acl2-sources directory named
saved_acl2r.

Note that you should also download the `nonstd' books, from
`http://acl2-books.googlecode.com/files/nonstd-5.0.tar.gz' and then
certify them from your acl2-sources directory, shown here as <DIR>:

     make regression-nonstd ACL2=<DIR>/saved_acl2r

To check that you are running ACL2(r), see if the prompt includes the
string "(r)", e.g.:

     ACL2(r) !>

Or, look at (@ acl2-version) and see if "(r)" is a substring.

In ACL2 (as opposed to ACL2(r)), when we say "real" we mean "rational."

Caution: ACL2(r) should be considered experimental: although we
(Kaufmann and Moore) have carefully completed Gamboa's integration of
the reals into the ACL2 source code, our primary concern has been to
ensure unchanged behavior when ACL2 is compiled in the default manner,
i.e., without the non-standard extensions.  As for every release of
ACL2, at the time of a release we are unaware of soundness bugs in ACL2
or ACL2(r).

There is only limited documentation on the non-standard features of
ACL2(r).  We hope to provide more documentation for such features in
future releases.  Please feel free to query the authors if you are
interested in learning more about ACL2(r).  Gamboa's dissertation may
also be helpful.

I-CLOSE    ACL2(r) test for whether two numbers are infinitesimally close

(I-close x y) is true if and only if x-y is an infinitesimal number.
This predicate is only defined in ACL2(r) (see REAL).

I-LARGE    ACL2(r) recognizer for infinitely large numbers

(I-large x) is true if and only if x is non-zero and 1/x is an
infinitesimal number.  This predicate is only defined in ACL2(r) (see
REAL).

I-LIMITED    ACL2(r) recognizer for limited numbers

(I-limited x) is true if and only if x is a number that is not
infinitely large.  This predicate is only defined in ACL2(r) (see
REAL).

I-SMALL    ACL2(r) recognizer for infinitesimal numbers

(I-small x) is true if and only if x is an infinitesimal number
(possibly 0).  This predicate is only defined in ACL2(r) (see
REAL).

REAL-LISTP    ACL2(r) recognizer for a true list of real numbers

The predicate real-listp tests whether its argument is a true list of
real numbers.  This predicate is only defined in ACL2(r) (see
REAL).

STANDARD-PART    ACL2(r) function mapping limited numbers to standard numbers

(Standard-part x) is, for a given i-limited number x, the unique real
number infinitesimally close (see I-CLOSE) to x.  This function
is only defined in ACL2(r) (see REAL).

STANDARDP    ACL2(r) recognizer for standard objects

(Standardp x) is true if and only if x is a "standard" object.  This
notion of "standard" comes from non-standard analysis and is discussed
in Ruben Gamboa's dissertation.  In brief, all the familiar objects are
standard: e.g., the familiar real numbers are standard, but non-zero
infinitesimals are not standard, and the familiar integers are
standard, but not those that exceed every integer that you can express
in the usual way (1, 2, 3, and so on).  Similarly, the familiar lists
are standard, but not so a list that contains a large number of
integers, where "large" means more than the standard integers.  The set
of standard numbers is closed under the usual arithmetic operations,
hence the sum of a standard number and a non-zero infinitesimal is not
standard, though it is what is called "limited" (see I-LIMITED).

This predicate is only defined in ACL2(r) (see REAL).

RELEASE-NOTES    pointers to what has changed

This section of the online documentation contains notes on the changes
that distinguish successive released versions of ACL2.

The current version of ACL2 is the value of the constant (@
acl2-version).

NOTE-2-0    ACL2 Version 2.0 (July, 1997) Notes

This is the first version of ACL2 released under the copyright of the
University of Texas (UT).  Future releases of ACL2 will be made from UT
rather than Computational Logic, Inc. (CLI).  Version 2.0 is just
Version 1.9 as released by CLI, with a few bugs fixed.

A bug causing an infinite loop was fixed in functional instantiation.
The bug manifested itself when two conditions occurred simultaneously:
First, the functional substitution replaces a function symbol, e.g.,
FOO, with a LAMBDA expression containing a free variable (a variable
not among in the LAMBDA formals).  And, second, in one of the
constraints being instantiated there is a call of the function symbol
FOO within the scope of another LAMBDA expression.  Unless you used
such a functional substitution, this bug fix will not affect you.

Less important notes:

The implementation of PRINC$ was changed so that it was no longer
sensitive to the external setting of *print-base* and other Common Lisp
special variables.

Typographical errors were fixed in the documentation.

NOTE-2-1    ACL2 Version  2.1 (December, 1997) Notes

The identity function case-split has been added.  It is similar to
force but causes an immediate split of the top-level goal on whether
the indicated hypothesis is true.

Less important notes:

Minor bugs in the documentation were fixed.

NOTE-2-2    ACL2 Version  2.2 (August, 1998) Notes

Important changes:

A bug was fixed in the compile command, :comp.  The compiled code
produced by :comp in previous versions could be wildly incorrect
because of a confusion between the printer and the reader regarding
what was the current Lisp *package*.  This bug could manifest itself
only if you used the :comp command to compile previously uncompiled
functions while the current package was different from "ACL2".  What
happened in that situation depended upon what symbols were imported
into your current package.  The most likely behavior is that the
compiler would break or complain or the resulting compiled code would
call functions that did not exist.

There have been no other important changes to the code.

However, this release contains some useful new books, notably those on
the books subdirectories cli-misc and ihs.  Both have README files.
The ihs books provide support for integer hardware specifications.
These books were crucial to Bishop Brock's successful modeling of the
Motorola CAP.  We thank Bishop for producing them and we thank all
those who worked so hard to get these books released.  We highly
recommend the ihs books to those modeling ALUs and other arithmetic
components of microprocessors or programming languages.

In previous versions of ACL2, the arithmetic books, found on
books/arithmetic/, included the addition of several unproved axioms
stating properties of the rationals that we believed could be derived
from our "official" axioms but which we had not mechanically proved.
The axioms were found in the book rationals-with-axioms.lisp, which was
then used in the uppermost arithmetic books top.lisp and
top-with-meta.lisp.  John Cowles has now provided us with ACL2 proofs
of those "axioms" and so in this release you will find both
rationals-with-axioms.lisp and rationals-with-axioms-proved.lisp.  The
former is provided for compatibility's sake.  The latter is identical
but contains defthms where the former contains defaxioms.  The top-most
books have been rebuilt using "-axioms-proved" book.  Thanks John.

Less important notes:

Bishop Brock found a bug in translated-acl2-unwind-protectp4.  Jun
Sawada reported a bug in linear arithmetic that caused us not to prove
certain trivial theorems concluding with (not (equal i j)).  We have
fixed both.

We now prohibit definitions that call certain event commands such as
DEFTHM and TABLE because our Common Lisp implementations of them differ
from their ACL2 meanings (so that compiled books can be loaded
correctly and efficiently).

Minor bugs in the documentation were fixed.

NOTE-2-3    ACL2 Version  2.3 (October, 1998) Notes

Important changes:

Versions of ACL2 preceding this one contain a subtle soundness bug!  We
found a flaw in our detection of subversive-recursions.  The bug
allowed some subversive recursions to slip through undetected.

We believe it would have been difficult to have exploited this flaw
inadvertently.  In particular, the following five conditions are
necessary.
(1) Introduce a constrained function, say f, via an encapsulate.
(2) In the same encapsulation, define a clique of mutually recursive
functions.  This clique must be non-local and in :logic mode.
(3) In that mutually recursive clique, use the constrained function f
(perhaps indirectly) so that the termination argument for the clique
depends on properties of the witness for f.  Thus, f or some other
function dependent upon f, must be used in an argument in a recursive
call or in a term governing a recursive call.  Furthermore, the use of
f must be such that the termination proof cannot be done without
exploiting properties of the witness for f.  Other uses of the
constrained functions in the clique are ok.
(4) Fail to include the exploited properties of f among the constraints
of the encapsulation.
(5) Later, outside the encapsulation, explicitly use a functional
instantiation in which f is replaced by a function not enjoying the
crucial properties.
See subversive-recursions for details.

Less important notes:

We have begun to write some introductory tutorial material for those
who wish to learn to program in ACL2.  Most of this material is
HTML-based.  See the Hyper-Card on the ACL2 home page.

The documentation of verify-guards was improved to explain why one
might wish to verify the "guards" of a defthm event.  The missing
documentation was noticed by John Cowles.

A bug was fixed in cross fertilization.  The bug caused the system to
report that it had substituted one term for another when in fact no
substitution occurred.  The bug was noticed by Bill McCune.

NOTE-2-4    ACL2 Version  2.4 (August, 1999) Notes

Important changes:

We corrected a soundness bug in Version 2.3 related to the handling of
immediate-force-modep.  The bad behavior was noticed by Robert Krug.
Thanks!

We corrected a bug that permitted verify-guards to accept a function
even though a subfunction had not yet had its guards verified.  Thanks
to John Cowles for noticing this.

User defined single-threaded objects are now supported.  See stobj.

Less important notes:

We corrected a bug that prevented the intended expansion of some
recursive function calls.

We changed the handling of the primitive function ILLEGAL, which is
logically defined to be nil but which is programmed to signal an error,
so that when it is evaluated as part of a proof, it does not signal an
error.  The old handling of the function prevented some guard proofs
involving THE or LETs with internal declarations.

We corrected a bug that permitted some LOCAL DEFAXIOM events to slip
into certified books.

We corrected a bug that prevented the correct undoing of certain DEFPKG
forms.

Changes were made to support CMU Lisp.  Pete Manolios helped with these
changes.

Changes were made to make the make files more compatible with Allegro
Common Lisp.  Jun Sawada, who has been a great help with keeping ACL2
up and running at UT on various platforms, was especially helpful.
Thanks Jun.

NOTE-2-5    ACL2 Version  2.5 (June, 2000) Notes

Important Changes:

Concurrent with the release of ACL2 Version  2.5 is the publication of
two books about ACL2.  See the "Books and Papers about ACL2 and Its
Applications" on the ACL2 Home Page.

The books subdirectory now contains many new certifiable books,
including solutions to the exercises in the two published books and
full scripts for the case studies.  See books/README.html.

Improved Unix Makefile support for book certification has also been
written.  See books/README.html.

The list of symbols in *acl2-exports* has been considerably expanded.
If you have packages built by importing *acl2-exports* you might want
to look carefully at the new value of that constant.  The new value
includes all :logic mode functions as of Version  2.5, as well as all
documented macros and all built-in theorem names.

Include-book and certify-book were modified to have some additional
keyword arguments.  It is possible to certify a book containing
defaxiom and/or skip-proofs events and get warning messages or errors
signaled, according to the settings of these new flags.  In addition,
it is possible to specify in include-book whether the book must be
certified (under penalty of error if not).  The default values of these
new arguments cause warnings to be printed rather than errors signaled.

The above change involved altering the form of certificate files.  When
books certified under previous versions are included, more warnings
will be generated because these books are considered possibly to
contain defaxiom and/or skip-proofs events.

We anticipate further changes to this aspect of books and consider the
current mechanisms (for controlling whether warnings or errors are
signaled) just a prototype.  See also the discussion below of
"soundness related" warnings.  Your suggestions are welcome.

A discrepancy between ACL2 and Common Lisp was fixed, having to do with
declare ignore.  In past versions of ACL2, a formal parameter of a
defun was considered ignored if it was not used in the body, the guard
or the measure of the defun.  That meant that a variable used only in
the guard could not be declared ignored in ACL2; but some Common Lisp
compilers would complain because the variable was not used in the body.
Now, ACL2 considers a variable ignored if it is not used in the body.

ACL2 can now be built in releases 5.0 and later of Allegro Common Lisp.
(Other releases of Allegro Common Lisp and of other lisps continue to
be supported as well.)  This includes Allegro Common Lisp running on
Windows 98 platforms.  John Cowles helped us do some testing and
answered questions for us.  Thanks John!

We incorporated Ruben Gamboa's changes to allow the building of a
variant, ACL2(r), of ACL2, in which the user can reason about the real
numbers using non-standard analysis.  See REAL.  Note that
ACL2(r) and ACL2 have different underlying theories, and books
certified in one system may not be included in the other.  For backward
compatibility and to ensure a smooth transition, ACL2 is built by
default, not ACL2(r).  This is a compile-time switch; see the makefile
for instructions.  There should be no changes to ACL2 resulting from
the capability of building ACL2(r) from the same sources.  Also see
ACKNOWLEDGMENTS for more on the history of ACL2(r).

A large number of bugs (some affecting soundness) were fixed, and many
small new features were added.  See below.

Less Important Changes:

Some warnings are now considered "soundness related," namely, those
that advise you that an uncertified book has been included or that a
book containing DEFAXIOM or SKIP-PROOFS events.  (Technically,
DEFAXIOMs do not imperil soundness in the proof- theoretic sense,
though they may imperil the validity of theorems.  But you sould know
when a book has added an axiom to your logic!)  In previous versions of
ACL2, all warnings were inhibited if the token warning was included in
the argument to set-inhibit-output-lst.  Now, soundness related
warnings are printed even if warnings have been inhibited.  To inhibit
all warnings, supply the token warning! to set-inhibit-output-lst.

Several bugs in defstobj were fixed, relating to the possibility that
some of the subfunctions introduced by the defstobj were already
defined.

:Puff no longer tries to expand defstobj events.  Previously, the
attempt would cause a hard error.

A soundness bug was fixed.  The bug might have been exercised if you
had an alternative definition (implies hyps (equiv (fn ...) body)) in
which equiv is an equivalence relation other than EQUAL.  In this case,
calls of fn might have been expanded to body in places that were not
equiv-hittable.

An obscure soundness bug was fixed.  The bug was exercised only if you
had a metafunction with a computed hypothesis (i.e., a "meta hypothesis
function"), the hypothesis contained a free variable, i.e., a variable
not involved in the term being rewritten, and the free variable
occurred in the output of the metafunction.  The possibility of this
bug was brought to our attention by Robert Krug.

We fixed a bug in the handling of hide related to the question of
whether a variable symbol occurs in a term.  The old code did not find
the variable and could cause the system to throw away a hypothesis
about it on the grounds that it was never mentioned.  Rob Sumners
helped discover this problem.

The handling of :elim rules was generalized, permitting arbitrary known
equivalence relations instead of merely equal in the concluding
equality.

The printing of runes (rule names; see RUNE) used has been made
"deterministic," both in proof output and in proof attempt summaries,
by sorting the runes before printing.

The handling of free variables has been improved for hypotheses such as
(< 0 X), and more generally, any hypotheses involving a comparison with
0 (even for example (< X 1) where X is known to be an integer, which is
handled as (<= X 0)).  Thanks to Robert Krug for bringing relevant
examples to our attention.

A new value, :comp, has been implemented for the :load-compiled-file
keyword of include-book.  If this value is supplied, then a compiled
file will always be loaded, even if that requires creating the compiled
file first.

The event include-book now generates a warning when a compiled file is
expected but not found (see INCLUDE-BOOK).  Formerly, it only
did so when executed at the top level; it failed to generate the
warning when executed on behalf of a surrounding include-book command.

Certain redefinition warnings generated by Allegro Common Lisp have
been eliminated.

A new key has been implemented for the acl2-defaults-table,
:bogus-mutual-recursion-ok, set with :set-bogus-mutual-recursion-ok.
Thanks to David Russinoff for pointing out the utility of such a key.

A bug was fixed in defun-sk that prevented its generated events from
being accepted when guard verification is being performed.  Thanks to
Bill Young for bringing this problem to our attention.  A second bug
was brought to our attention by Pete Manolios, which was causing
certain defun-sk events to be rejected.  That problem has been fixed,
and an "Infected" warning has also been eliminated.

The command good-bye now works with Allegro Common Lisp.

A low-level bug was fixed that could, for example, cause an error such
as "Error: Expected 5 args but received 4 args" when interrupting a
local event.

A bug has been fixed in the proof-checker related to definition
expansion.  Thanks to Pete Manolios for bringing this to our attention
with a simple example.

A bug has been fixed related to the :bdd hint in the presence of
equivalence relations.  Thanks to Pete Manolios for bringing this to our
attention with a simple example.

The functions position and position-equal formerly required the second
argument to be a true list.  In accordance with Common Lisp, we now
also allow the second argument to be a string.  This could cause
earlier proofs about these functions to fail unless true-listp is known
to hold where necessary.

Robert Krug wrote a patch, which has been incorporated, to prevent
certain infinite loops that can arise in linear arithmetic.  Thanks,
Robert!

The macro let* no longer requires the bound variables to be distinct.

An obscure bug was fixed related to congruence rules.  The bug would
sometimes cause ACL2 to behave as though no rules (other than equality)
were available for some argument positions.  Thanks to Pete Manolios for
bringing this bug to our attention.

Documentation topics have been added for hard-error and prog2$, and the
documentation for illegal has been improved.  Thanks to Rob Sumners for
a useful suggestion in the examples in documentation for prog2$ and a
fix in documentation for sublis.

The event form certify-book was made more secure, in that it can now
catch attempts to write a book to disk during its certification.
Thanks to Rob Sumners for pointing out the insecurity of the existing
mechanism.

A Y2K problem was fixed with our applicative handling of dates.

Accessors and updaters for stobjs have been made more efficient when
the underlying lisp is Allegro Common Lisp, by the use of appropriate
simple array declarations.

A raw Lisp break had been possible when a certified book that had no
guard verification was included in a session after
(set-verify-guards-eagerness 2).  This has been fixed.

The keyword command :comp can now be used to compile only raw Lisp
functions, excluding executable counterparts, by supplying the argument
:raw.

Rewrite rule nth-of-character-listp was removed from source file
axioms.lisp since it is essentially subsumed by characterp-nth.

Printing has been sped up.  In one example the improvement was over 50%
in both Allegro and GCL.

We now allow printing in a "downcase" mode, where symbols are printed
in lower case.  All printing functions except print-object$ now print
characters in lower case for a symbol when the ACL2 state global
variable print-case has value :downcase and vertical bars are not
necessary for printing that symbol.  See IO for a discussion of
the macros acl2-print-case and set-acl2-print-case.  The default
printing remains unchanged, i.e., symbols are printed in upper case
when vertical bars are not required.

A low-level printing function (prin1$) was modified so that it is not
sensitive to various Common Lisp globals related to printing.  So for
example, the function fmt is no longer sensitive to the value of Common
Lisp global *print-case*.  (The preceding paragraph explains how to
control the case for printing in ACL2.)

The definition of array1p was fixed so that the :maximum-length of an
array must be strictly greater than the number specified in the
:dimensions field; they may no longer be equal.  This was always the
intention; the documentation (see ARRAYS) has remained
unchanged.  The corresponding change was also made to array2p.  Allegro
Common Lisp formerly caused an error when compress1 was called on an
array where the numbers above were equal; now, we get a guard violation
instead, which is appropriate.

In the context of theories, a name now represents not just the
corresponding :definition rune, as it has done in earlier versions of
ACL2, but also the corresponding :induction rune.  See THEORIES
for a discussion of runic designators.  Most users will rarely, if
ever, notice this change.  One situation where this change will make a
difference is after executing (in-theory (current-theory 'foo))
followed by (in-theory (enable bar)), where function bar is introduced
after event foo, and bar is recursively defined.  The latter in-theory
form now enables the rune (:induction bar), which implies that the
prover can use the induction scheme stored at definition time for bar.
Formerly, the rune (:induction bar) was not enabled by (in-theory
(enable bar)), and hence the induction scheme for bar was ignored even
when explicit :induct hints were supplied.

You may now supply xargs keyword pair :normalize nil in order to
prevent certain definitions from "hanging" when there are many
if-subexpressions.  see DEFUN.

We now translate type declarations of real into guards, as we have
already done for other types such as rational.  For example, (declare
(type real x)) generates the guard (rationalp x).  See
TYPE-SPEC.

The theorem prover now behaves reasonably under the combination of
specifying a value of t both for :otf-flg and for a hint
:do-not-induct.  Previously, it aborted the first time it would have
otherwise pushed a goal for induction, but now, it will continue and
wait until all induction subgoals have been pushed before it aborts.

We changed slightly the definition of round.  However, we believe that
the new definition is equivalent to the old.

The definition of Common Lisp function substitute has been added.

The following changes have been made in the use of file names within
ACL2.  We thank Warren Hunt and John Cowles for running some tests of
these changes on Macintosh and Windows 98 platforms (respectively).

     (1) Names of directories and files now use a syntax like that used
     for Unix (trademark of AT&T), where directories are separated using
     the "/" character even when the operating system is not Unix or
     Linux.  See PATHNAME.  ACL2 also continues to support its
     notion of _structured pathnames_ from Version  2.4 and before, but
     might not do so in future releases and hence no longer documents
     such syntax.

     (2) The command :set-cbd may now take a relative pathname as an
     argument.

     (3) When the macro ld is given a file name as a value for
     standard-oi, then if that file name is a relative pathname it
     refers to the result of prepending the connected book directory
     (see PATHNAME, see CBD, and see SET-CBD)
     in order to obtain an absolute pathname.  Simiarly for the ld
     specials standard-co and proofs-co.

It is no longer necessary to issue :set-state-ok t if you include a
stobj declaration for state, for example:

     (declare (xargs :stobjs state))

See DECLARE-STOBJS.

The proof-checker has been cleaned up a bit, including the
documentation and the capability (once again) to define pc-macro
commands (see DEFINE-PC-MACRO) and proof-checker meta commands
(see DEFINE-PC-META).

Recall that events generate summaries that include a line beginning
with "Warnings:", which is followed (on the same line) by zero or more
brief strings that summarize the warnings generated by that event.
Formerly, this warnings summary for an encapsulate or include-book
event did not include the summary strings for warnings generated by
subsidiary events.  This has been fixed.

Macro cw has been documented and now expands to a call of a ;logic mode
function.  See CW for a way to print to the screen without
having to involve the ACL2 state.  Thanks to Rob Sumners for suggesting
that we document this useful utility.

Functions duplicates, add-to-set-equal, intersection-eq, evens, and
odds are now :logic mode functions.

NOTE-2-5(R)    ACL2 Version  2.5(r) (June, 2000) Notes

Important changes to non-standard version:

Please see NOTE-2-5 for changes to Version  2.5 of ACL2.  We
hope to write more documentation for ACL2(r) in the future.

NOTE-2-6    ACL2 Version  2.6 (November, 2001) Notes

Because of the large number of modifications, we have divided up the
Version  2.6 notes into the following subtopics.

     o New functionality (see NOTE-2-6-NEW-FUNCTIONALITY):
     o Changes in proof engine (see NOTE-2-6-PROOFS):
     o Changes in rules and definitions (see NOTE-2-6-RULES):
     o Guard-related changes (see NOTE-2-6-GUARDS):
     o Proof-checker changes (see NOTE-2-6-PROOF-CHECKER):
     o System-level changes (see NOTE-2-6-SYSTEM):
     o Other (minor) changes (see NOTE-2-6-OTHER):

NOTE-2-6-GUARDS    ACL2 Version  2.6 Notes on Guard-related Changes

When you declare that a function treats certain formals as :stobjs, the
guard of the function is automatically extended to include the
corresponding stobj-recognizer calls.  For example, if a definition
includes (declare (xargs :stobjs (ST))) then the guard of the function
is changed by the addition of the conjunct (ST-P ST).

One impact of this is that if you use the built-in ACL2 state as a
formal parameter of a function, (STATE-P STATE) is added to the guard.
This may introduce a guard where there was none in previous versions of
the system.  In older versions, therefore, no attempt would be made to
verify-guards, while in the new version, we would attempt guard
verification.  You may wish to add (declare (xargs :verify-guards nil))
to such definitions.

A related change affects users who do not use stobjs or state.  In
previous versions of the system -- as now -- a type declaration
extended the guard you provided explicitly.  Thus, if you wrote
(declare (type integer n)) then (INTEGERP n) was added to your guard.
This is still the case and :stobjs recognizers are similarly added.
But in older versions of the system we "added" the conjuncts without
checking whether they were already present in the guard you provided.
This sometimes produced such guards as (and (integerp n) (integerp n))
where the first was produced by your type declaration and the second
was your :guard.  We now eliminate redundant conjuncts; this may
rearrange the order of the conjuncts.

The guard conjectures for functions using stobjs have been simplified
somewhat by taking advantage of the syntactic restrictions checked for
single-threaded objects.

The following functions have been modified so that character and string
arguments are restricted to standard characters.  (See
STANDARD-CHAR-P and see STANDARD-CHAR-LISTP.)

     upper-case-p lower-case-p char-upcase char-downcase
     string-downcase1 string-downcase string-upcase1 string-upcase
     char-equal string-equal1 string-equal

Also, function standard-string-alistp replaces function string-alistp,
with concomitant changes in the guard to assoc-string-equal, and in
variable *acl2-exports*.  Also, lemma
standard-string-alistp-forward-to-alistp replaces lemma
string-alistp-forward-to-alistp.  There is a new lemma
standard-char-p-nth, which has also been added to *acl2-exports*.

The guard had been inadvertently omitted from the definition of the
function substitute (and its subroutine substitute-ac).  This omission
has been corrected; also, the guard is slightly stronger than the
documentation had claimed (and that has been corrected).

NOTE-2-6-NEW-FUNCTIONALITY    ACL2 Version  2.6 Notes on New Functionality

A fundamental change is the provision of the "nu-rewriter" for
simplifying expressions composed of NTH, UPDATE-NTH, and
UPDATE-NTH-ARRAY applications and LET expressions and other calls of
non-recursive functions or LAMBDA expressions involving those symbols.
The nu-rewriter applies the obvious rewrite rule for (NTH i (UPDATE-NTH
j v s)) and the analogous rule for UPDATE-NTH-ARRAY.  See
NU-REWRITER  The nu-rewriter can be enabled with set-nu-rewriter-mode.

A new flag has been added to the xargs of defun permitting the
declaration that the function is non-executable.  The usage is (declare
(xargs :non-executable t)) and the effect is that the function has no
executable counterpart.  On the positive side:  the function is
permitted to use single-threaded object names and functions
arbitrarily, as in theorems rather than as in executable definitions.
Such functions are not permitted to declare any names :stobjs but
accessors, etc., may be used, just as in theorems.

A new flag has been added to permit the system to abbreviate output by
introducing LET* notation identifying common subterms.  The formula
being proved is not affected; this flag changes its displayed form
only.  See set-let*-abstractionp.

A "raw mode" has been added, primarily for faster loading of
applications.  see SET-RAW-MODE.

Functions alphorder and lexorder have been put in :logic mode.
Lexorder is now a total order ordering of the ACL2 universe, and
theorems are included to that effect.  Thanks to Pete Manolios for
suggesting the idea and providing events to use, and to Rob Sumners for
assistance with some modifications.  See also the new book
books/misc/total-order for an irreflexive total order.

The ACL2 user can now make system calls to the host operating system.
See SYS-CALL and see SYS-CALL-STATUS.  Thanks to Rob
Sumners for working out this idea with Pete Manolios and Robert Krug,
who we also thank, and for working out the implementation with us.

It is no longer required to use absolute pathnames in include-book
forms that have been executed before a certify-book.  Any relative
pathname strings in such contexts will be expanded into absolute
pathnames before they are saved in the portcullis of the certificate of
the book being certified.

ACL2 can now be built on top of Allegro Common Lisp 6.0, and also on
Windows platforms on top of Allegro Common Lisp and GCL.  Thanks to Pete
Manolios and Vinay K. Siddhavanahalli for their help with Windows.

Rob Sumners has designed and provided an initial implementation for two
improvements to defstobj (also see STOBJ).  First, array fields
can now be resized.  Resize and length functions are provided for array
fields, which can be used to resize stobj array fields dynamically.
The recognizers for array fields have been simplified to accommodate
this change, so that they only check that each element of the array
field has the specified type.  Second, performance has been improved
for stobjs with a large number of fields, by changing their Common Lisp
implementation to store the fields in a simple vector instead of a list.

Now stobjs may be bound locally; see WITH-LOCAL-STOBJ.  Thanks
to Rob Sumners, who encouraged us to implement this capability, was an
early user of it, and participated usefully in discussions on its
design.

New functions fms!, fmt!, and fmt1! are the same as their respective
functions without the "!," except that the "!" functions are guaranteed
to print forms that can be read back in (at a slight readability cost).

We added extended-metafunctions, metafunctions which allow state and
context sensitive rewriting to some extent.  We thank Robert Krug for
pushing for and on this idea.

The documentation has been improved.  In particular, a new
documentation topic provides a gentle introduction to ACL2 arrays --
see ARRAYS-EXAMPLE -- and additional documentation has been
provided for getting started with proof trees in emacs -- see
PROOF-TREE-EMACS.

New Makefile targets fasl and o have been added to the books/ directory
of the distribution.  For example, you might first certify books using
an ACL2 built on top of GCL (which creates compiled files with suffix
o).  Then, when standing in the books/ directory, you might execute the
command

     make fasl ACL2=my-allegro-acl2

which will create compiled (.fasl) files for Allegro Common Lisp,
assuming that my-allegro-acl2 starts up an ACL2 built on that Common
Lisp.

The macro let* now allows variables to be declared ignored.  See
LET* and see LET.

The user may now control backchaining.  This feature was designed and
primarily implemented by Robert Krug (though the authors of ACL2 are
resposible for any errors); thanks, Robert!  See
BACKCHAIN-LIMIT.

It is now possible to "slow down" the rate at which case splits are
generated by the simplifier.  See SET-CASE-SPLIT-LIMITATIONS.

Accesses to stobjs using nth or update-nth are now displayed using
symbolic constants instead of numeric indices.  For example, given the
event

     (defstobj foo a b :renaming ((b c)))

then the term (nth 0 foo) will be displayed (for example, during
proofs) as (nth *a* foo) while (nth 1 foo) will be displayed as (nth
*c* foo).  The defstobj event now correspondingly introduces a defconst
event for each field accessor function, introducing a constant whose
name is obtained from the accessor's name by prefixing and suffixin a
"*," as in the example above: accessor a generates (defconst *a* 0) and
accessor c generates (defconst *c* 1). See NTH-ALIASES-TABLE
for how to extend this feature for alternate names of stobjs.

Computed hints have been improved.  It is now possible to detect within
a computed hint whether the goal clause is stable under simplification;
it is also possible for a computed hint to change the list of available
hints.  See COMPUTED-HINTS.

It is now possible to provide "default hints" that are appended to the
hints explicitly provided.  See SET-DEFAULT-HINTS.

Using computed hints (see COMPUTED-HINTS) and default hints
(see SET-DEFAULT-HINTS) it is possible to implement a book that
supports "priority phased simplification."  Using this book you can
assign priorities to your rules and cause the theorem prover to
simplify each goal maximally under all the rules of one priority before
enabling rules of the next priority.  See books/misc/priorities.lisp.

The macro defabbrev has been improved to allow declare forms and
documentation strings and to do more error-checking.  Thanks to Rob
Sumners for designing this enhancement and providing the first
implementation.  See DEFABBREV.

Further changes were made to support CMU Lisp.  Wolfhard Buss helped
with these changes.

A new table was added that is used when printing proof output, so that
nests of right-associated calls of a binary function are replaced by
corresponding macro calls, as has been the case for binary-+ and +,
binary-append and append, and so on.  See ADD-BINOP.

Operators logand, logior, logxor, and logeqv are now macros (formerly,
they were functions) that call corresponding binary functions (e.g.,
binary-logand) defined in source file "axioms.lisp".  Thanks to Rob
Sumners for this enhancement.  Proof output will however continue to
show calls of logand, logior, logxor, and logeqv.

Function (allocate-fixnum-range fixnum-lo fixnum-hi) sets aside more
"permanent" fixnums in GCL.

ACL2 now runs under CLISP.  Thanks to Wolfhard Buss and Sam Steingold
for their assistance with the port.

Michael "Bogo" Bogomolny has created a search engine, accessible from
the ACL2 home page.  For that purpose he modified the HTML translator
to create one file per topic (a good idea in any case).  Thanks, Bogo!

An emacs file of potential (but optional) use for ACL2 users may be
found in emacs/emacs-acl2.el.  In particular, this file supports the
use of proof trees (see PROOF-TREE).

Some books have been added or modified.  In particular, Robert Krug has
contributed books/arithmetic-2/, which provides an alternative to the
existing collection of books about arithmetic, books/arithmetic/.  For a
discussion of the distributed books see the link to README.html in the
installation instructions.

NOTE-2-6-OTHER    ACL2 Version  2.6 Notes on Other (Minor) Changes

Warning strings are now case-insensitive.  See
SET-INHIBIT-WARNINGS.

ACL2 causes a warning when an in-theory hint or event causes a 0-ary
function's definition to be disabled but its :executable-counterpart to
be enabled.

A minor modification has been made to defstobj that can have a positive
impact on performance in Allegro Common Lisp.  (For Lisp hackers:  the
stobj name was formerly declared special, and that was disabling
Allegro's tail-merging routing for compilation of some recursive
functions using stobjs.)  The downside is that stobj names can no
longer be evaluated in raw Lisp.  However, raw Lisp is not the right
place to be evaluating ACL2 forms anyhow; see SET-RAW-MODE.  We
thank Rob Sumners for bringing this issue to our attention.

Before Version  2.6, there has been the following problem with defstub
and encapsulate in the case that the current package is not the ACL2
package.  If a signature was specified using the symbol =>, then that
symbol had have been imported into the current package from the ACL2
package when the current package was defined.  There are no longer any
package restrictions on the use of =>.  Thanks to John Cowles for
bringing this problem to our attention.

Bugs in defun-sk have been fixed.  Defun-sk forms introducing functions
of no arguments were failing to be admitted, for example: (defun-sk
always-p1 () (forall (x) (p1 x))).  Thanks to John Cowles for bringing
this problem to our attention.  Also, defun-sk failed on an example in
the documentation (see TUTORIAL4-DEFUN-SK-EXAMPLE), as pointed
out by Matyas Sustik; this bug has been fixed as well.

The trace mechanism has been fixed to handle stobjs, and to avoid the
printing of so-called _enabled structures_.

The brr command :type-alist now produces more readable output.

An include-book of an uncertified book no longer loads an associated
compiled file.

We added a few checks to make sure that the underlying lisp is
suitable, for example checking that the reader is case-insensitive and
reads in symbols with upper-case names where appropriate.

We now warn when forcing (see FORCE) or immediate force mode
(see IMMEDIATE-FORCE-MODEP) change state between enabled and
disabled.  Also see ENABLE-IMMEDIATE-FORCE-MODEP and see
DISABLE-IMMEDIATE-FORCE-MODEP for information about these new macros,
which may be used to control immediate force mode.

We have eliminated the use of a low-level raw Lisp constant,
*most-recent-multiplicity*.  Our test suite saw a speed-up of
approximately 2% as a result for an ACL2 image built on GCL (but no
significant speed-up for an ACL2 image built on Allegro Common Lisp).
We thank Rob Sumners for suggesting this improvement.

Fixnum declarations are now realized as (signed-byte 29) instead of
(signed-byte 27).  We check that the underlying Common Lisp recognizes
objects of type (signed-byte 29) as fixnums, with the exception of
CLISP, which is said to have an efficient bignum implementation.

A new documentation topic functional-instantiation-example illustrates
functional instantiation.

A bug has been fixed in the monitoring of runes (see MONITOR).
Thanks to Dave Greve for sending an example that clearly showed the
problem.

A warning is now issued when it is detected that a :type-prescription
rule may not be as strong as it appears because it is not sufficient to
prove itself by type reasoning.

An error is caused for rules of class :meta when the function symbol IF
is among the :trigger-fns.  (IF was ignored anyhow; the point of this
change is to avoid misleading the user.)

A minor bug has been fixed in :pr, evident for example if this command
was applied to IF.

A minor hole in :set-bogus-mutual-recursion-ok did not permit the
acceptance of mutual-recursion forms that include constant function
definitions.  This has been fixed.  Thanks to Eric Smith for coming up
with a simple example illustrating the problem.

The temporary files "TMP.lisp" and "TMP1.lisp" written out by :comp are
now written to the connected book directory (see CBD).

Previously, the Allegro compiler was not eliminating tail recursion for
executable counterparts of functions, because of the way one of its
flags had been set.  As a result, calls of functions whose guards had
not been verified could run out of stack space when this was not
necessary.  This situation has been fixed.

Executable counterparts could have slow array accesses.  This has been
fixed (specifically, constants are no longer replaced with their values
in the definitions of executable counterparts).

Various improvements have been made to the documentation.  Thanks in
particular to Eric Smith for pointing out a numbers of places where
fixes were in order.

File "mcl-acl2-startup.lisp" has been updated, thanks to feedback from
Philippe Georgelin.

Inefficiencies in GCL fixnum computations were remedied for macros +f
and *f.  Thanks to Rob Sumners for pointing out this issue.

NOTE-2-6-PROOF-CHECKER    ACL2 Version  2.6 Notes on Proof-checker Changes

The proof-checker command =, when used with no arguments, now reports
which hypothesis is being used.

The output from proof-checker command type-alist has been improved.

A slight change has been made to the proof-checker for commands
promote, casesplit, equiv, and =, so that terms of the form (if x nil
y) are recognized as conjunctions, (and (not x) y).  Thanks to Pete
Manolios for suggesting that we consider such a change.

There is a new proof-checker command print-all-concs that prints all
the conclusions of the unproved goals.

A new proof-checker command, runes, has been added.  It reports the
runes that have participated in the interactive proof up to the current
point.

NOTE-2-6-PROOFS    ACL2 Version  2.6 Notes on Changes in Proof Engine

Certain optimizations are performed when converting terms to clausal
form.  For example, (< 0 1) is known to be t, (HARD-ERROR ctx str
alist) is known to be nil, and (INTEGERP n) is known to imply
(RATIONALP n).

In earlier versions of ACL2, the conversion of a term to clausal form
expanded LAMBDA applications.  That may no longer occur.  Some proofs
may slow down (or fail) because your LAMBDA-expressions are not
expanded away when you "expected" them to be.

Robert Krug found a soundness bug in our linear arithmetic package.
The bug was caused by the derivation of an equation from two
inequalities without taking adequate precautions to ensure that both
sides of the inequalities were numeric.  Robert also kindly provided a
fix which we adopted.  Thanks Robert!

We fixed a bug that could prevent the application of a metatheorem.

A bug has been fixed that had caused bogus forcing rounds (see
FORCING-ROUND).  The bug could occur when the hypothesis of a rule
was forced (see FORCE) before the prover decided to start over
and prove the original goal by induction.  Thanks to Rob Sumners for
drawing our attention to this problem.

Some low-level fixes have been made that prevent certain infinite
loops, based on reports by users.  We thank Yunja Choi, Matt Wilding,
and Pete Manolios for reporting such problems.

An obscure potential soundness hole has been fixed by redoing the way
evaluation takes place in the ACL2 loop and during theorem proving.  We
expect that users will see no difference based on this change.  (Those
interested in the details can see the long comment "Essay on Evaluation
in ACL2" in source file interface-raw.lisp.)

A small change was made in computation for a heuristic that controls
backchaining.  This will speed up proofs dramatically in a very few
cases but should have a very small impact in general.

The simplifier has been modified to avoid eliminating hypotheses of
goals that can be established by contextual (specifically, type-set)
reasoning alone.  We believe that this change will generally strengthen
ACL2's reasoning engine, although on rare occasions a lemma that
formerly was provable may require user assistance.  Thanks to Robert
Krug for suggesting this change and providing its implementation.

Case splits are now limited, by default.  This may allow some proof
attempts to provide output where previously the prover would appear to
"go out to lunch."  For a more complete discussion, including
instructions for how users can control case splitting, see
SET-CASE-SPLIT-LIMITATIONS.

A bug has been fixed in the handling of :type-prescription rules by the
bdd package.  Thanks to Rob Sumners for discovering this bug and
supplying a helpful example.

ACL2 may now use the built-in induction scheme for a function symbol
even if that function symbol is disabled.  Formerly, if a function
symbol was disabled then its induction scheme was only considered if an
explicit induction hint was supplied, other than :induct t.

We eliminated the rule-class linear-alias.  This rule class was seldom
used and complicated the linear arithmetic decision procedure in ways
that made it difficult to extend to handle some non-linear special
cases.  The only use of the rule-class that we know of was in our own
nqthm books, which were an attempt to provide an embedding of the Nqthm
logic and theorem prover into ACL2.  But that facility was also
practically never used, as far as we know.  So both linear-alias rules
and the nqthm books have been eliminated.

In earlier versions of ACL2, when the IF-form of (AND p q) was assumed
true - as when rewriting the alpha expression in (IF (AND p q) alpha
beta) - the assumption mechanism did not deduce that p and q are true,
only that their conjunction, in its IF-form, is true.  This has long
been known as a deficiency in both ACL2 and the earlier Nqthm but it
was tedious to do better when one considered the full range of IF-forms
one might encounter in the test of another IF.  Rather than code all
the cases, we just waited until clausification got rid of them.  Robert
Krug developed a pretty nice treatment of the general case and we added
it in this version.  This also involved a surprising number of changes
elsewhere in the system because the improved handling of assumptions
caused the theorem prover often to "erase" hypotheses provided by :use
hints because it could simplify them to t.  Thank you Robert!

In response to a suggestion from Robert Krug, we added mfc-ap so that
extended metafunctions can take advantage of linear arithmetic.  See
EXTENDED-METAFUNCTIONS.

There is less delay in printing goals.  In previous versions, a goal
was not printed until its subgoals were created (or the goal was
proved).  Now, the goal is printed essentially as soon as it is created.

A small technical change has been made in the function term-order, to
give priority on the function symbol count over the weighting of
constants.  So for example, while previously the term (f) preceded the
constant 2, that is no longer the case.  If this change is noticed at
all, it will probably be noticed in how so-called _permutative_ rewrite
rules are applied; see LOOP-STOPPER.  Thanks to Robert Krug for
suggesting this improvement and providing part of the implemtation.

NOTE-2-6-RULES    ACL2 Version  2.6 Notes on Changes in Rules and Constants

The following symbols have been added to the list constant
*common-lisp-specials-and-constants*: REPLACE, FILL, CHARACTER, =,
BREAK, and PRIN1.  This was done in support of ports to Allegro 6.0 and
Windows platforms (see NOTE-2-6-NEW-FUNCTIONALITY).

The list of symbols in *acl2-exports* has been modified, for example to
include show-accumulated-persistence and the legal arguments to
set-inhibit-output-lst.

Functions zp and zip are now handled slightly differently.  They are
are now disabled, but each comes with a :rewrite rule that allows their
expansion on non-variable terms, and also with a :compound-recognizer
rule that avoids the need for opening up these functions when applied
to variables.  The resulting behavior should be very similar to the
behavior of previous versions, except that case splits will be avoided
when these functions are applied to variables.

Function standard-string-alistp replaces function string-alistp.  For
further discussion, see NOTE-2-6-GUARDS.

Rules of class :rewrite whose conclusion is a term of the form (equal
lhs rhs) have always been stored in the expected way:  lhs rewrites to
rhs.  This way of storing :rewrite rules has been extended to allow =,
eq, or eql in place of equal.

Rewrite rule nth-update-nth, in source file axioms.lisp, has been
strengthened.

A new rewrite rule equal-constant-+ has been added to the book
arithmetic/equalities.  This should generally be a beneficial change,
but existing proofs involving the arithmetic books could conceivably be
affected.

Function symbol-package-name and constant *main-lisp-package-name* have
undergone small changes.  This change should rarely be noticed by users
and is discussed elsewhere; see NOTE-2-6-SYSTEM.

We mention here that proofs involving stobjs may need to be modified
because of changes in auxiliary functions generated by defstobj.
(These changes were made in support of a new resizing capability,
mentioned elsewhere in these release notes; see
NOTE-2-6-NEW-FUNCTIONALITY.

In the distributed book directory books/arithmetic/, the book
rationals-with-axioms-proved.lisp has been renamed rationals.lisp.

(ACL2(r) only) Rewrite rules realp-+, realp-*, realp-unary-, and
realp-unary-/ have been added in analogy to existing rules rationalp-+,
rationalp-*, rationalp-unary-, and rationalp-unary-/.  Thanks to Jun
Sawada for suggesting this change.

The definition of aref1 has been modified slightly.  Previously, if
*my-a* were an array then (aref1 'some-name *my-a* :header)  would
evaluate to the cdr of the header of *my-a* rather than to its default.
See ARRAYS.

Changes have been made in the ihs books, based on suggestions from Jun
Sawada, that support its use with ACL2(r) (see REAL).  The
primary change is to replace calls of rationalp with calls of
real/rationalp, which should have no effect on users of standard ACL2.

NOTE-2-6-SYSTEM    ACL2 Version  2.6 Notes on System-level Changes

We modified the tracking of skip-proofs events and the use of state
global ld-skip-proofsp in order to avoid some soundness issues.  For
example, skip-proofs events buried in locally-included books are now
tracked.  The "Essay on Skip-proofs" in source file axioms.lisp gives
several examples of dicey behavior that is no longer supported.

We fixed a problem with some of the makefiles, so that recursive
invocations of make now use the version of make specified on the
command line.

Files were fixed to help non-Unix/Linux users with book certification.
Thanks to John Cowles for finding some problems and suggesting fixes to
books/certify-numbers.lisp, books/arithmetic/certify.lsp, and
books/cowles/certify.lsp.  We thank Scott Burson for noticing and
fixing some other such problems.  Moreover, a bdd test was being
ignored entirely in Version  2.5; this problem has been fixed as well.

A minor change in system function save-acl2-in-allegro will allow this
function to continue to work in Allegro CL versions starting (someday)
with 10.0.  Thanks to Art Flatau for suggesting such a fix.

The books/case-studies/ directory has been removed.  These books are in
support of the first (1998) ACL2 workshop, and are accessible via the
ACL2 home page on the Web,
`http://www.cs.utexas.edu/users/moore/acl2/'.  Also, the books/cli-misc
directory has been renamed books/misc, and the books/nqthm directory
has been removed.

The notion of ACL2 version has been slightly modified to catch
unsoundness due to implementation dependencies.  See VERSION.
Another change to eliminate such unsoundness is that built-in symbols
now have a symbol-package-name of "COMMON-LISP"; formerly, this string
was "LISP" for ACL2 images built on GCL.  See
SYMBOL-PACKAGE-NAME.  At a low level, the (undocumented) constant
*main-lisp-package-name* is now "COMMON-LISP"; before, it was "LISP"
for GCL.

NOTE-2-6(R)    ACL2 Version  2.6(r) (November, 2001) Notes

Important changes to non-standard version:  None since Version  2.5.

Please see NOTE-2-6 for changes to Version  2.6 of ACL2.  We
hope to write more documentation for ACL2(r) in the future.

NOTE-2-7    ACL2 Version  2.7 (November, 2002) Notes

The Version_2.7 notes are divided into the subtopics below.  Here we
give only a brief summary of a few of the changes that seem most likely
to impact existing proofs.  Not included in this brief summary, but
included in the subtopics, are descriptions of improvements (including
bug fixes and new functionality) that should not get in the way of
existing proof efforts.

In particular, please see NOTE-2-7-NEW-FUNCTIONALITY for
discussion of a number of new features that you may find useful.

Acknowledgements and elaboration, as well as other changes, can be
found in the subtopics listed below.

o Bug fixes (see NOTE-2-7-BUG-FIXES):

     + Three soundness bugs were fixed.  These bugs were probably
     rarely hit, so users may well not notice these changes.

     + Certify-book now requires :skip-proofs-ok t (respectively,
     :defaxioms-okp t) if there are skip-proofs (respectively,
     defaxiom) events in the book or any included sub-books.

     + When :by hints refer to a definition, they now use the original
     body of that definition rather than the simplfied ("normalized")
     body.

     + When ld is applied to a stringp file name, it now temporarily
     sets the connected book directory (see CBD) to the
     directory of that file while evaluating forms in that file.

o New functionality (see NOTE-2-7-NEW-FUNCTIONALITY):

     + ACL2 now works harder to apply :rewrite and :linear rules with
     free variables in the hypotheses.  See
     NOTE-2-7-NEW-FUNCTIONALITY, in particular its first two
     paragraphs, for details.  Forward-chaining also does more with
     free variables.

o Changes in proof engine (see NOTE-2-7-PROOFS):

     + Some prover heuristics have changed slightly.  Among other
     consequences, this can cause subgoal hints to change.  For
     example, suppose that the Version_2.6 proof of a particular
     theorem generated "Subgoal 2" and "Subgoal 1" while Version_2.7
     only generates the second of these.  Then a subgoal hint attached
     to "Subgoal 1" in Version_2.6 would have to be attached to "Goal'"
     in Version_2.7.  (See GOAL-SPEC.)  The full topic has
     details (see NOTE-2-7-PROOFS).

o Changes in rules and definitions (see NOTE-2-7-RULES):

     + The package name of a generated variable has changed for defcong.

o Guard-related changes (see NOTE-2-7-GUARDS):

     + Guard verification formerly succeeded in a few cases where it
     should have failed.

     + Guards generated from type declarations now use functions
     signed-byte-p and unsigned-byte-p, now defined in source file
     axioms.lisp and formerly defined rather similarly under books/ihs/.

o Proof-checker changes (see NOTE-2-7-PROOF-CHECKER):

     + See the above doc topic.

o System-level changes (see NOTE-2-7-SYSTEM):

     + See the above doc topic.

o Other changes (see NOTE-2-7-OTHER):

     + A new table, invisible-fns-table, takes the place of the
     handling of invisible functions in the acl2-defaults-table,

     + The theory-invariant event has been modified so that the default
     action is an error rather than a warning.

     +  Proof output that reports destructor elimination no longer uses
     the word "generalizing".

Again, please proceed to the subtopics for more thorough release notes.

NOTE-2-7-BUG-FIXES    ACL2 Version  2.7 Notes on Bug Fixes

Francisco J. Martin-Mateos emailed us a soundness bug (!) in our
handling of functional instantiation (for example see
FUNCTIONAL-INSTANTIATION-EXAMPLE).  We are grateful for that email,
which clearly illustrated the problem.  It is included just below the
definition of push-clause in ACL2 source file prove.lisp, where we have
fixed the bug.  This bug was fixed in a re-release of Version  2.6 in
February, 2002.

Rob Sumners emailed us a soundness bug (!) in function commutative-p1,
which is used by the ACL2 bdd package.  We are grateful for his help;
his email gave a proof of nil and also pointed to the problem function.
This bug was fixed in a re-release of Version  2.6 in February, 2002.

We discovered and fixed a soundness bug illustrated by the book below,
which was certifiable in Version  2.6 and ends in a proof of nil.  The
event (verify-guards foo) should have been rejected, because foo calls a
function whose guards have not been verified, namely, bar.  However,
ACL2 did not notice the call of function bar in the body of foo because
it was looking in the simplified (normalized) body of foo rather than
in the original body of foo.  During processing of the book below, the
logical definition of zp is used before (verify-guards foo), and (zp -3)
reduces to t in the logic.  After (verify-guards foo), ACL2 simplifies
(foo -3) by going into raw Lisp, where (zp -3) is evaluated and reduces
to nil.

       (in-package "ACL2")
       (defun bar (x)
         (zp x))
       (defthm zp-false-on-negatives
         (implies (< x 0)
                  (bar x))
         :rule-classes :type-prescription)
       (defun foo (x)
         (declare (xargs :guard (rationalp x)
                         :verify-guards nil))
         (if (< x 0)
             (if (bar x) 0 1) ; simplified body reduces this line to 0
           17))
       (defthm foo-of-minus-3-is-0
         (equal (foo -3) 0)
         :rule-classes nil)
       (verify-guards foo)
       (defthm foo-of-minus-3-is-1
         (equal (foo -3) 1)
         :rule-classes nil)
       (defthm bug
         nil
         :rule-classes nil
         :hints (("Goal" :use (foo-of-minus-3-is-0 foo-of-minus-3-is-1))))

The above bug exploited the fact that zp has a different definition in
raw Lisp than in the logic for arguments that violate its guard).  The
following example caused a hard error in raw Lisp, though not a
soundness error.

       (in-package "ACL2")
       (defun bar (x)
         (cons (car x) (car x)))
       (defun foo (x)
         (declare (xargs :guard t
                         :verify-guards nil))
         (if (bar x) x nil))
       (verify-guards foo)
       (defthm bug
         (equal (foo 3) t)
         :rule-classes nil)

We have made a minor change to the notion of the _formula_ of a function
symbol, related to the change above, which however is unlikely to be
noticeable.

In order to make it harder to hit problems like the guard problem
above, we have slighly modified the raw Lisp definition of zp.

A break-rewrite command, :ancestors, was broken, but has been fixed.
Thanks to Eric Smith for bringing the problem to our attention, and to
Robert Krug for supplying the final part of the fix.

Some proof-checker commands caused errors when all goals have already
been proved.  This has been fixed.  Thanks to Matt Wilding for
reporting this bug.

Fixed a bug in :comp.  When compiling uncompiled functions with very
large definitions, ACL2 was inserted a backslash (\) character into
generated files.

Fixed the :type-alist :brr command (see BRR-COMMANDS), whose
output was difficult to read when typed after an :eval..

Fixed some clumsy handling of errors when including an uncertified
book, for example, with the error message when including an uncertified
book with a bad deftheory event.  Thanks to Eric Smith for pointing out
this problem.

Two modifications to certify-book now cause it to reflect natural
expectations with respect to soundness.  First, it now has default
values of nil instead of t for keyword arguments :skip-proofs-okp and
:defaxioms-okp.  Thanks to Robert Krug for suggesting this change and
the ACL2 seminar at the University of Texas for discussing it.  Second,
when :skip-proofs-okp (respectively, :defaxioms-okp) is nil, either
explicitly or by default, then skip-proofs commands (respectively,
defaxiom events) are disallowed inside any included books, regardless
of the keyword parameters passed to include-book.  This had not been
the case for previous versions of ACL2, regardless of the values of
:skip-proofs-okp or :defaxioms-okp passed to include-book.

Improved warnings and errors for certify-book and include-book to
mention the portcullis as a possible source of skip-proofs and
defaxioms.

ACL2 formerly caused an error when hints in a :corollary were not
well-formed.  This situation could arise as follows when certifying a
book.  A lemma FOO is proved LOCALly to the book (or, is present in a
sub-book that is included locally).  The :corollary of a subsequent
theorem, BAR, disables that rule in a hint.  When BAR is proved, this
is not a problem.  But certify-book makes a second pass after
processing the events in a book: it essentially does an include-book.
During the include-book pass, FOO is not known (because it was local),
and therefore ACL2 fails to process the disable of FOO in an in-theory
hint.  The fix is that during include-book, hints are ignored in
corollaries just as they have been for the main theorem (or definition).

It was possible for guard verification to succeed where it should have
failed.  We have fixed the bug (which was in source function (ironically
named!) fcons-term-smart).  Thanks to Robert Krug for sending us an
example of bungled guard verification.  It turns out that this bug was
also present in Version_2.6.

The proof-checker command = has been improved.  Formerly, it could fail
to apply when certain implies terms were in the context.  Thanks to
Pete Manolios for bringing this problem to our attention.

The command add-binop failed to work.  This has been fixed.  Thanks to
Rob Sumners for pointing out this problem.  Also see
NOTE-2-7-OTHER for a discussion of how this and another table are no
longer part of the acl2-defaults-table.

Book certification could cause a segmentation fault in cases where the
certification world (see CERTIFY-BOOK) has a very large number
of events.  This has been fixed.

We now allow empty :use hints and empty hints, as requested by Eric
Smith.  Examples:

     ("Goal" :use ())
     ("Goal")

A large mutual-recursion nest could cause a stack overflow when
executing either :pr FN, :pr! FN, or :monitor (:definition FN) t, where
FN is in that large mutual recursion nest.  This has been fixed
(implementation detail:  function actual-props has been made
tail-recursive).  NOTE:  If you just want the definition of FN, :pf FN
can be much faster than :pr FN if FN is in a large mutual-recursion.

Hard Lisp errors could occur when including uncertified books.  This
has been fixed; ACL2 now does syntax-checking formerly omitted when
including uncertified books.

Previously, the evaluation of defstobj and mutual-recursion forms could
cause "undefined" warnings when the form was compiled.  This has been
fixed.  Thanks to Eric Smith for bring a mutual-recursion example to our
attention.

A bug has been fixed in the syntactic check for valid :loop-stopper
values.  Formerly, valid :loop-stopper values were erroneously
restricted to lists of length at most 2 (a minor problem, since these
lists typically have length 1), and the function symbol(s) need not
have been defined in the current ACL2 world.  Thanks to Eric Smith for
sending an example to demonstrate the latter problem.

Functions definitions that are :non-executable (see XARGS) had
never been recognized as redundant, but this has been fixed.  Thanks to
Vernon Austel for pointing out this problem.

Compilation using :comp now compiles user-defined :program mode
functions.  Formerly only :logic mode functions could be compiled using
:comp.

Handling of :by hints has been improved in essentially three ways.  The
primary change is that now, when the current goal exactly matches the
supplied lemma instance, the subsumption test will always succeeds (see
HINTS, in particular the discussion of :by).  Second, certain
proof failures involving :by hints were failing silently, with duplicate
messages "As indicated by the hint, this goal is subsumed by...."  This
could happen when the original goal was among the goals generated by
applying the hint.  This problem has been fixed by no longer
considering this proof step to be specious (see
SPECIOUS-SIMPLIFICATION).  Third and finally, when the lemma-instance
refers to a definition, the original body of that definition is used
rather than the simplfied ("normalized") body.

In addition to the obove, we now recognize more cases of specious
simplification (see SPECIOUS-SIMPLIFICATION).  Thanks to Eric
Smith for bringing this issue to our attention.

Fixed building of ACL2 under CLISP so that (1) the appropriate ACL2
startup message is printed out when ACL2 starts up, and (2) the lisp
process supplied to make, e.g., LISP=/usr/bin/clisp, is the one written
out to the saved ACL2 file.  Thanks to Dave Greve and Noah Friedman for
suggesting (2).  Also, ACL2 now works with CLISP 2.30.  We have
accommodated a change in CLISP's handling of streams and its
package-locking mechanism, as well as certain non-standard characters
that formerly could cause CLISP 2.30 to break, even when those
characters are in comments.

Eliminated compiler warnings for CMU Lisp.

Fixed an incorrect error supplied when book certification proceeded so
quickly that the file write dates of the book (.lisp file) and the
corresponding compiled file are equal.  Now that error only occurs if
the compiled file has a strictly earlier write date, which probably
should never happen.

Fixed an infinite loop when executing make clean-books (and hence make
with targets that call clean-books, namely, certify-books-fresh,
regression-fresh, and regression-nonstd-fresh), which could occur when
any subdirectories of books/ are missing -- even workshops/, which is
intended to be optional.  Thanks to Pete Manolios for pointing out this
bug.

The include-book command now works properly even when filenames, or
their directories or parent directories (etc.) are links.  Thanks to
Matt Wilding for pointing out this problem.

The commands :puff :puff* have been fixed.  Formerly, there was a bug
when :puff or :puff* caused the execution of an include-book for an
absolute pathname, P, that was other than the current connected book
directory (see CBD).  When including P, any subsidiary
include-book with a relative pathname would be erroneously considered
relative to the current cbd rather than relative to the directory of P.
Thanks to Pete Manolios and Matt Wilding for pointing out this problem.

It had been possible in a "large" ACL2 image to call verify-termination
successfully on built-in function sys-call, with undesirable results.
This hole has been plugged.  Thanks to Rob Sumners for pointing out
this problem.  The new function gc$ must also stay in :program mode.

ACL2 no longer warns when certifying a book based on local functions
whose guards have not yet been verified.  Thanks to Pete Manolios for
pointing out this issue.

An occasional "slow array warning" had been possible during proofs.  The
following sequence shows how to evoke that warning in previous versions.

     (in-theory (disable binary-append))
     (in-theory (enable binary-append))
     (in-theory (disable binary-append))
     (ubt 2)
     (thm (equal (car (cons x y)) x))

(See NOTE-2-7-OTHER for a discussion of a change to compress1 in
support of this fix; however, users should not need to read that
discussion.)

The raw Lisp code for defchoose had a small bug, which was only
evidenced in CLISP implementations as far as we know.  It has been
fixed.

When ld is applied to a stringp file name, it now temporarily sets the
connected book directory (see CBD) to the directory of that
file while evaluating forms in that file.  To see the effect of this
change, imagine a subdirectory "sub" of the current directory, and
imagine executing (ld "sub/foo.lisp"), where file foo.lisp contains the
form (include-book "bar").  Presumably the intention was to consider the
file bar.lisp in the same directory, sub/, as foo.lisp.  Ld now honors
that intention, but in previous versions "bar.lisp" would have been a
reference to a file in the current directory, not in sub/.

For users of run-acl2 [perhaps there are none!]: A fix has been provided
by a Debian user via Camm Maguire so that acl2-mode anyone using that?]
will work in Xemacs, which apparently uses variable
lisp-mode-shared-map rather than shared-lisp-mode-map.

ACL2 has, for a long time (always?), had a mechanism for avoiding
re-proving constraints generated by :functional-instance lemma-instances
in :use and :by hints.  But this mechanism had not applied to defined
(as opposed to constrained) functions.  This has been fixed.  Thanks to
Francisco J. Martin-Mateos (ChesKo) for pointing out this problem by
sending a clear example.

NOTE-2-7-GUARDS    ACL2 Version  2.7 Notes on Guard-related Changes

It was possible for guard verification to succeed where it should have
failed.  See the discussion under note-2-7-bug-fixes.

There have been changes in the guards generated from type declarations
for the following cases.  Thanks to Dave Greve and Matt Wilding for
suggesting such changes.

     (type (signed-byte n) val)
     (type (unsigned-byte n) val)
     (type (integer m n) val)

The following examples illustrate the changes.

     (type (signed-byte 4) x)
     ==> [old] (AND (INTEGERP X) (<= -8 X) (<= X 7))
     ==> [new] (SIGNED-BYTE-P 4 X)

     (type (unsigned-byte 4) x)
     ==> [old] (AND (INTEGERP X) (<= 0 X) (<= X 15))
     ==> [new] (UNSIGNED-BYTE-P 4 X)

NOTE-2-7-NEW-FUNCTIONALITY    ACL2 Version  2.7 Notes on New Functionality

ACL2 now has a more powerful technique for relieving a :rewrite or
:linear rule's hypothesis that contains free variables.  A new
documentation section has been written describing the handling free
variables in rules; see FREE-VARIABLES.  In brief, the primary
change is that when a free-variable match for the current hypothesis
fails to allow subsequent hypotheses to be relieved, then additional
matches may be attempted until they have all been tried.  Also see
RULE-CLASSES (discussion of :match-free).  Also see
SET-MATCH-FREE-ERROR, see SET-MATCH-FREE-DEFAULT, and see
ADD-MATCH-FREE-OVERRIDE for interfaces provided to the user for
controlling the way ACL2 deals with free variables in hypotheses.  We
thank Rob Sumners for several helpful discussions about the designs of
those interfaces, as well as Eric Smith and Robert Krug for helpful
related discussions.  Robert Krug also found a performance bug in a
preliminary version, for which we are grateful.

WARNING: Book certification attempts may take much longer now that, by
default, ACL2 looks for more free variable matches (see paragraph just
above).  You can get the old behavior by inserting the form

     (set-match-free-default :once)

just after the initial in-package form.  However, rules from included
books that have free variables can still slow down certification.  This
can be fixed by inserting

     (add-match-free-override :once t)

before the first event in the file that generates a proof.

Forward-chaining has been made more powerful in the presence of free
variables (see FREE-VARIABLES), thanks to a contribution by
Erik Reeber.  Both before and now, when an attempt is made to relieve
(prove) a hypothesis of a :forward-chaining rule in the case that at
least one variable in that hypothesis is not yet bound, ACL2 looks in
the current context for an instance of that hypothesis.  If it finds
one, then it binds the unbound variables and continues to the next
hyopothesis.  What is new is that ACL2 can now looks for multiple
instances of that hypothesis.  Consider the following example; an
explanation is below.

     (encapsulate (((op * *) => *))
                  (local (defun op (x y) (< x y)))
                  (defthm transitivity-of-op
                    (implies (and (op x y) (op y z)) (op x z))
                    :rule-classes :forward-chaining))

     ; fails in Version_2.6; succeeds in in Version_2.7
     (thm (implies (and (op a b) (op b c) (op b e)) (op a c)))

Before Version_2.7, the proof of the thm above fails.  When the
:forward-chaining rule transitivity-of-op binds x to a and y to b, it
then looks for an instance of (op y z) in the current context, with y
bound to b but z unbound.  It happens to find (op b e) before (op b c),
and it then adds (op a e) to the context.  But starting with
Version_2.7, it continues to look for additional instances and finds
(op b c) in the context as well, chaining forward to (op a c) and thus
proving the theorem.

A new macro, bind-free, provides a simple way to get much or most of
the power of metafunctions.  Thanks to Eric Smith for coming up with the
idea and to Robert Krug for providing an implementation (which we
modified only very slightly) and documentation. See BIND-FREE
and see BIND-FREE-EXAMPLES.

With the addition of bind-free (mentioned above), syntaxp has become a
macro, although that change should be transparent to the user.  More
importantly, the argument of syntaxp may now refer to variables mfc and
state, giving syntaxp some of the power of extended metafunctions; see
SYNTAXP and see EXTENDED-METAFUNCTIONS.  Thanks to
Robert Krug for implementing that extension.  Also, the argument of
syntaxp may now include calls of :program mode functions.  See
SYNTAXP and see SYNTAXP-EXAMPLES (thanks to Robert Krug for
updating the former and creating the latter documentation).

The linear-arithmetic decision procedure (see
LINEAR-ARITHMETIC) has now been extended so that ACL2 can reason
about non-linear arithmetic as well (see NON-LINEAR-ARITHMETIC
for how to turn on this feature).  We thank Robert Krug for the initial
implementation of this, and Eric Smith for finding a couple of bugs in
it.

Some trace utilities have been made available in the ACL2 loop.

     o Function trace$ (and also untrace$) calls the corresponding
     underlying Lisp routine trace (and untrace), which however
     continues (as it has for some time) to be enhanced for GCL and
     Allegro CL.

     o Macro open-trace-file causes trace output to go to a specified
     file.  Macro close-trace-file causes trace output to go to the
     screen (which is the default).

     o Macro with-error-trace (or, wet for short) causes a backtrace to
     be written out for many failures, including guard violations.  See
     TRACE, see TRACE$, and see :DOC wet [** NOTE:
     eliminated after Version  3.3].

A new theory, minimal-theory has been provided (see THEORIES).
It can be particularly useful for speeding up proofs involving :use
hints.

New events defund and defthmd behave exactly like defun and defthm,
respectively, except that these new events disable the new name.

The new macro with-output can be used to suppress output that would
normally result from evaluation of a form.

The form (pstack) can give the user an idea of what the prover has been
up to during a proof, or after a user-aborted proof.  Moreover, by
evaluating (verbose-pstack t) (see VERBOSE-PSTACK) one can get
trace-like information about prover functions, including time
summaries, printed to the screen during a proof.  Thanks to Bill Legato
and Robert Krug for initiating this work and to Robert for providing
some initial implementation.

The new command :comp-gcl is identical in functionality, except that it
always leaves .c and .h files when compiling in GCL.  Thanks to Rob
Sumners and Vernon Austel for suggesting such a capability.

The macro e/d provides a convenient way to enable some rules and
disable others.  It was formerly in a book supplied with the
distribution, books/ihs/ihs-init.lisp, written by Bishop Brock (who we
thank for providing this useful macro).

New distributed books include those in books/ordinals/,
books/rtl/rel3/, and books/misc/simplify-defuns.lisp (which is
documented in books/misc/simplify-defuns.txt).

The :expand hint now accepts a special value, :LAMBDAS, that tells the
ACL2 rewriter to expand all lambda applications (let expressions).  See
HINTS.

A new function zpf has been added as fast test against 0 for
nonnegative fixnums.

A new macro gc$ allows the user to call the garbage collector of the
underlying Common Lisp.  Thanks to Rob Sumners for suggesting this
feature.

It is now possible to monitor simple (abbreviation) rules.  However, as
a warning explains, they are still not considered monitored during
preprocessing; see MONITOR.  Thanks to Robert Krug for
providing this improvement.

The second argument of certify-book, if supplied, formerly had to be
either t or a non-negative integer.  Now it can be the symbol ?, in the
ACL2 package, indicating that the usual check should be suppressed on
the number of commands that have been executed to create the world in
which certify-book was called.

NOTE-2-7-OTHER    ACL2 Version  2.7 Notes on Miscellaneous Changes

Made several minor documentation improvements.  We are grateful to Eric
Smith for suggesting (most of) these.

Improved (show-bdd) (see BDD) to give more useful feedback when
there are "leaf" terms not known to be Boolean.

Sped up processing of large mutual-recursion nests.  In one large
example the speedup was roughly two orders of magnitude.

Modified event printing so that if both 'prove and 'event are
inhibited, then events are no longer printed on behalf of certify-book,
encapsulate, or defstobj.  Thanks to Eric Smith for prompting
consideration of such a change.

The following technical change was made to support with-error-trace and
wet (see NOTE-2-7-NEW-FUNCTIONALITY), but may be of interest to
those who do low-level programming using the ACL2 logical world.  The
'unnormalized-body property is now stored not only for functions defined
in :logic mode, but also for functions defined by the user in :program
mode.  (:Program mode Functions built into ACL2 still have their
'unnormalized-body property omitted, in order to save space.)

The handling of "invisible" functions for purposes of controlling
rewriting (see LOOP-STOPPER) has been moved to a new table; see
INVISIBLE-FNS-TABLE.  Macros that access and modify this table
are called "...-invisible-fns-table" in place of their former names,
"...-invisible-fns-alist."  This feature was formerly implemented in
the acl2-defaults-table, which prevented a book from exporting lists of
invisible functions intended to work with the rewrite rules developed in
the book.  Thanks to Eric Smith and Rob Sumners for suggesting this
change.  See SET-INVISIBLE-FNS-TABLE (formerly
set-invisible-fns-alist), and also see ADD-INVISIBLE-FNS and
see REMOVE-INVISIBLE-FNS, which provides ways to incrementally
add to and remove from this table, respectively.  The handling of
printing binary function call nests using macros (See
ADD-BINOP) has also been moved out of the acl2-defaults-table as
suggested by Eric and Rob, but this feature didn't work anyhow (see
NOTE-2-7-BUG-FIXES).  Incidentally, the symbols binop-table,
add-binop, and remove-binop have all been added to the list
*acl2-exports* (see ACL2-USER), add-invisible-fns and
remove-invisible-fns have been added to that list, and
set-invisible-fns-alist has been replaced in that list by
set-invisible-fns-table.  Function invisible-fns-alistp is no longer
defined and has been removed from *acl2-exports*.

We now enforce the stated restriction on the pairings in
macro-aliases-table (see MACRO-ALIASES-TABLE), namely, that it
associates names of macros with names of funcions (with respect to the
current ACL2 logical world).  We make a similar requirement on
invisible-fns-table.

The theory-invariant event has been modified so that the default action
is an error rather than a warning.  Thanks to Eric Smith for suggesting
this change.  Also, the value returned upon successful execution of a
theory-invariant event is now the key.

Proof output that reports destructor elimination no longer uses the word
"generalizing".  This small change may help in browsing proof output,
since now "generaliz" takes you to true uses of generalization.  Thanks
to Matyas Sustik for suggesting such a change.

The command :pl now prints an abbreviated controller-alist for
;definition rules.  Formerly the output from :pl could be overwhelming
when the supplied function was part of a large mutual-recursion nest.

The defaults for keyword parameters of certify-book have changed.  See
NOTE-2-7-BUG-FIXES, in particular, the discussion there of two
modifications to certify-book.

Technical changes have been made to compress1 and compress2 that should
usually be invisible to users.  The next paragraph describes them in
detail, only for competeness (i.e., that description can be ignored by
most users).  But first, here is an example showing an effect on users.
The slow array warning was not there previously.  Notice that the
warning only arises if the event form is changed.  The solution is to
be sure that redundant defconst forms are syntactically identical.

     ACL2 !>(defconst *a* (compress1 'demo
                                     '((:header :dimensions (5)
                                                :maximum-length 15
                                                :default uninitialized
                                                :name demo)
                                       (1 . one)
                                       (0 . zero))))

     Summary
     Form:  ( DEFCONST *A* ...)
     Rules: NIL
     Warnings:  None
     Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
      *A*
     ACL2 !>(aref1 'demo *a* 0)
     ZERO
     ACL2 !>(defconst *a* (compress1 'demo
                                     '((:header :dimensions (5)
                                                :maximum-length 15
                                                :default uninitialized
                                                :name demo)
                                       (1 . one)
                                       (0 . zero))))

     This event is redundant.  See :DOC redundant-events.

     Summary
     Form:  ( DEFCONST *A* ...)
     Rules: NIL
     Warnings:  None
     Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
      :REDUNDANT
     ACL2 !>(aref1 'demo *a* 0)
     ZERO
     ACL2 !>(defconst *a* (compress1 'demo
                                     '((:header :dimensions (5)
                                                :maximum-length 15
                                                :default uninitialized
                                                :name demo)
                                       (0 . zero)
                                       (1 . one))))

     This event is redundant.  See :DOC redundant-events.

     Summary
     Form:  ( DEFCONST *A* ...)
     Rules: NIL
     Warnings:  None
     Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
      :REDUNDANT
     ACL2 !>(aref1 'demo *a* 0)

     **********************************************************
     Slow Array Access!  A call of AREF1 on an array named
     DEMO is being executed slowly.  See :DOC slow-array-warning
     **********************************************************

     ZERO
     ACL2 !>

As before, the von Neumann structure stored in the 'acl2-array property
of the array name contains the array list object in its car.  However,
previously it was the case that compress1 and compress2 did not update
that car when its new value would be equal to its old value.  This was
done largely in support of some type-set tables defined using defconst
in type-set-b.lisp.  The new versions of compress1 and compress2 are
simpler in that no such exception is made in the case of equal lists,
although instead the entire compression process is short-circuited when
the input array list object is eq to the car of the 'acl2-array
property.  This change was made because the equality test was causing a
"slow array access" warning to be printed in rare cases during proofs,
as described elswhere (see NOTE-2-7-BUG-FIXES).

We no longer distribute documentation specific to Lucid Emacs.  The Info
documentation in directory doc/EMACS/ works well both for Gnu Emacs and
XEmacs.

A little-advertised macro, value, has long been allowed for top-level
forms in books; see EMBEDDED-EVENT-FORM.  This has been
replaced by a new macro, value-triple.  The two have the same semantics
at the top-level of books, where state is "live".  However, value-triple
should be used at the top-level of a book, while value should be used in
function definitions (as before).  This change eliminates a warning put
out by the Allegro Common Lisp compiler for top-level value forms in
books.

NOTE-2-7-PROOF-CHECKER    ACL2 Version  2.7 Notes on Proof-checker Changes

Output from the proof-checker can now be inhibited by supplying the
symbol proof-checker in the list given to set-inhibit-output-lst.

NOTE-2-7-PROOFS    ACL2 Version  2.7 Notes on Changes in Proof Engine

An improvement in the linear arithmetic heuristics has been provided by
Robert Krug.  For information about this change, search for the comment
in add-linear-lemma (file rewrite.lisp) that begins as follows.

     ; Previous to Version_2.7, we just went ahead and used the result of

Thanks, Robert!  Also thanks to Eric Smith for providing a motivating
example.

The non-linear-arithmetic addition (see NON-LINEAR-ARITHMETIC)
led to several small changes in the linear-arithmetic decision procedure
(see LINEAR-ARITHMETIC).  Two of these changes could affect
existing proofs.

     First, when we are setting up the initial arithmetic data-base
     (which we call the "pot-lst"), we have always scanned it to see if
     there were any pairs of inequalities from which we could derive a
     previously unknown equality.  In some cases we added this equality
     to the clause and in others we used it to rewrite the clause,
     substituting one side of the equality for the other throughout the
     clause.  Previously, the heuristics that we used to determine
     whether we performed the substitution differed from those used in
     several other places in the code.  This has now been regularized,
     and similar heuristics are now used throughout the code.

     The second change to the linear-arithmetic decision procedure is
     that we now explicitly add inequalities derived from type reasoning
     to the pot-lst.  Previously, we performed cancellations against
     these inequalities without adding them to the pot-lst.  This
     change results in there being more inequalities in the pot-lst
     than before, and so more chances for there to be a pair of
     inequalities from which an equality can be derived.  In effect,
     certain simple consequences of the current goal (see
     TYPE-SET) may now be added as hypotheses of the goal or used to
     peform equality substitutions.

A slight improvement has been made to the way certain rewrite rules are
stored.  It was already the case that a rewrite rule rule whose
conclusion C is not a call of a known equivalence relation (or eq, eql,
or =) is stored as (iff C t), except that if ACL2 can determine (using
its type-set mechanism) that C is Boolean, then the rule is stored as
(equal C t).  The iprovement is that if C and C' are Boolean, then a
rule stated as (iff C C') is stored as (equal C C').  Thanks to Pete
Manolios for providing an example that led us to consider this
improvement.

The heuristic use of equalities (fertilization) has been modified.
Previously, ACL2 would sometimes substitute using an equality but keep
the equality, and then undo the substitution by using the equality
again.  Now, when ACL2 keeps an equality after using it, it puts the
equality inside a call of hide.  Descendents of that goal that are
unchanged by simplification will have this call of hide removed so that
the equality can once again contribute to the proof.  This change can
cause some proofs to succeed that otherwise would fail.  In the
unlikely event that a proof fails that formerly succeeded, the
following hint on "Goal" may fix the problem (see HINTS):

     :expand ((:free (x) (hide x)))

We have refined the heuristics employed when an IF form is assumed true
or false.  Our previous attempt (see note-2-6-proofs for the original
announcement) was not as general as we had believed.  We have also
improved some low-level code responsible for rewriting IF expressions.
In earlier versions of ACL2, it was possible to have the truth or
falsity of an IF expression explicitly recorded in the type-alist, and
yet not use this information during rewriting.  This problem has been
corrected.  Thanks to Robert Krug for noticing this problem and
implementing the fix.

We have sped up the rewriter in some cases where there are large
collections of mutually-recursive functions (see
MUTUAL-RECURSION).  (Implementation notes: technically, we have
modified the way function being-openedp operates on the fnstack, and we
have modified *current-acl2-world-key-ordering* as described in the
essay above its definition.)

Forward-chaining is now done in the preprocessing phase of proof
attempts (see the discussion of :DO-NOT -- see HINTS).  This is
part of a technical change, made in support of translation of type
declarations to guards (see NOTE-2-7-GUARDS).  Previously,
whenever ACL2 checked for built-in-clauses, it then looked for a
contradiction using type-set reasoning if it did not find a suitable
built-in clause.  The change is to perform forward-chaining in such
cases (i.e., when a built-in clause is not found).

A couple of changes have been made in the generation of goals for
forcing-rounds.  Thanks to Eric Smith for bringing issues to our
attention that led to these changes.  For one, guards are no longer
relevant in such goal generation.  Formerly, the addition of a guard
could make a proof fail that otherwise succeeded.  Secondly, contextual
information is now always kept when it involves a constrained constant,
i.e., a zero-ary function introduced in the signature of an encapsulate.

NOTE-2-7-RULES    ACL2 Version  2.7 Notes on Changes in Rules and Constants

The defcong macro has been slightly changed.  The difference is that
the variable generated with suffix -EQUIV will now be in the same
package as the name of the variable from which it is generated, rather
than always belonging to the ACL2 package.  Thanks to Hanbing Liu for
suggesting this change.  (Note that a couple of books have been
modified to accommodate this change, e.g.,
books/finite-set-theory/set-theory.)

In Version_2.6, a change was made for rules of class :rewrite whose
conclusion is a term of the form (EQV lhs rhs), where EQV is =, eq, or
eql: the rule was stored as though EQV were equal.  (See
NOTE-2-6-RULES.)  This change has been extended to rules of class
:definition.

NOTE-2-7-SYSTEM    ACL2 Version  2.7 Notes on System-level Changes

ACL2 now runs (once again) under LispWorks, specifically, LispWorks
4.2.0.  However, we needed a patch, which presumably will be
unnecessary after 4.2.7.  From LispWorks support:

     Users with LispWorks4.2.7 should ask us at lisp-support@xanalys.com
     for the transform-if-node patch. It will be helpful if they quote
     (Lisp Support Call #11372) when doing so. Also, they must send a
     bug form generated from their LispWorks image: instructions at
     http://www.lispworks.com/support/bug-report.html.

File books/Makefile-generic has been improved so that failed attempts to
certify a book will cause the make to fail.  Previously, an existing
.cert file was left in place, and that sufficed for the make to be
considered a success.  Now, the old .cert file is first removed when
recertification is found to be necessary.

A change has been made to source file acl2.lisp to accommodate GCL
2.4.3.  (ACL2 Version  2.6 does not work with some versions of GCL
2.4.3.)

The error message has been improved when certain forms are typed to raw
Lisp and the ACL2 loop has never been entered (with (LP)).

The following symbols in the ACL2 package have been made untouchable,
meaning that they are not available to the user: ev-fncall, ev, ev-lst,
ev-acl2-unwind-protect, ev-fncall!, and user-stobj-alist-safe.  The
reason is that these functions can not be called safely except under
certain restrictions.  If you want to call the ACL2 evaluator, consider
using the built-in system functions trans-eval or
simple-translate-and-eval.

CLISP Version_2.30 implements a notion of "locking" the "LISP" package
that is incompatible with building ACL2.  (CLISP Version_2.27 does not
appear to have had this feature.)  We have gotten around this problem
by unlocking the "LISP" package in ACL2 images built on such CLISPs.

Automatic proclaiming for GCL, which has (for a long time) been done for
functions in compiled books, has been improved.  Formerly, the only
time a non-trivial output type (i.e., other than t) was inferred was
when macroexpansion produced an explicit call of the.  Now, if
expressions can also generate non-t output types.  Consider the
following example.

     (defmacro the-fixnum (n)
       (list 'the '(signed-byte 29) n))
     (defmacro 1+f (x)
       (list 'the-fixnum
             (list '1+ (list 'the-fixnum x))))
     (defun foo (x)
       (declare (type (unsigned-byte 27) x))
       (if (zp x)
           0
         (1+f (foo (1-f x)))))

Formerly, the proclaim forms for foo, before and after this
improvement, are as shown below.

     (PROCLAIM '(FTYPE (FUNCTION ((UNSIGNED-BYTE 27)) T) FOO))                ;old
     (PROCLAIM '(FTYPE (FUNCTION ((UNSIGNED-BYTE 27)) (SIGNED-BYTE 29)) FOO)) ;new

Compiler info messages sent to error stream were eliminated for CMUCL.

NOTE-2-7(R)    ACL2 Version  2.7(r) (November, 2002) Notes

In source file axioms.lisp, in order for proofs to succeed, (make
proofs), the definitions of acl2-count and explode-atom have been
modified slightly, and lemma standard-numberp-one [modified after
Version_3.4 to become standardp-one] has been given :rule-classes nil.

All skip-proofs forms have been eliminated from the nonstd books, thanks
to Ruben Gamboa.

The directory books/sqrt/, which was intended for ACL2(r), has been
moved to books/nonstd/sqrt/ and added as appropriate to
books/nonstd/Makefile.

Please see NOTE-2-7 for changes to Version_2.7 of ACL2.

NOTE-2-8    ACL2 Version  2.8 (March, 2004) Notes

BRIEF SUMMARY.

The Version_2.8 notes are divided into the indicated subtopics.  Here
we give only a brief summary of just a few of the major new features
and changes that seem most likely to impact existing proofs.  Not
included in this brief summary, but included in the subtopics, are
descriptions of many improvements (including bug fixes and new
functionality) that should not get in the way of existing proof
efforts.  In the description below we also omit discussion of changes
that will become clear by way of error messages if they affect you.

In particular, please see NOTE-2-8-NEW-FUNCTIONALITY for
discussion of a number of new features that you may find useful.

Acknowledgements and elaboration, as well as other changes, can be
found in the subtopics listed below.

o Some of the bug fixes (see NOTE-2-8-BUG-FIXES):

     + Some soundness bugs were fixed.

     + The handling of free variables in hypotheses (see
     FREE-VARIABLES) of rewrite and linear rules had a bug that
     prevented some proofs from going through.  Now that this bug has
     been fixed, you may find some proofs running much more slowly than
     before.  You can use accumulated-persistence and
     add-match-free-override to remedy this situation; see
     NOTE-2-8-BUG-FIXES for details.

     + The default-hints in the current logical world are no longer
     ignored by verify-guards.

     + Forms violating guard-checking such as (defconst *silly* (car
     3)) are now allowed in books.

o Some of the new functionality (see
NOTE-2-8-NEW-FUNCTIONALITY):

     + WARNING: You may find that control-d (in emacs, control-c
     control-d) can throw you completely out of Lisp where it had not
     formerly done so.

     + ACL2 now starts up inside the ACL2 loop -- that is, (LP) is
     executed automatically -- when built on CLISP or Allegro CL.  This
     was already the case for GCL and CMUCL, and it still is not true
     for LispWorks.

     + See NOTE-2-8-ORDINALS for a discussion of a significant
     change in ordinal represtation, and in particular, for how to
     preserve existing proofs that depend on the previous ordinal
     representation.

     + Macros mbe ("must be equal"), mbt ("must be true"), and defexec
     have been introduced, which allow the user to attach alternate
     executable definitions to functions.

     + The user can now control multiple matching for free variables in
     hypotheses for :forward-chaining rules, as has already been
     supported for :rewrite and :linear rules.

     + It is no longer necessary to specify (set-match-free-error nil)
     in order to avoid errors when a rule with free variables in its
     hypotheses is missing the :match-free field.

     + The form (break-on-error) causes, at least for most Lisps, entry
     into the Lisp debugger whenever ACL2 causes an error.

     + A new table has been provided so that advanced users can
     override the built-in untranslate functionality.  See
     USER-DEFINED-FUNCTIONS-TABLE.

     + The pstack (`process [prover] stack") mechanism, formerly denoted
     checkpoints, has been improved.  One of these improvements is to
     show actual parameters with (pstack t) rather than formals.

     + The defstobj event is now allowed to take an :inline argument,
     which can speed up execution.

     + Macro cw-gstack no longer takes arguments for the gstack or
     state.  To print terms in full rather than abbreviated: (cw-gstack
     :evisc-tuple nil).

     + The include-book event now has an additional (optional) keyword,
     :dir.  In particular, (include-book "foo/bar" :dir :system) will
     include the indicated book after prepending the path of the
     built-in books/ directory.  You will probably not find :dir
     :system to be useful if you move the executable image or
     distributed books; see INCLUDE-BOOK, in particular its
     "soundness warning".

     + The printing of results in raw mode (see SET-RAW-MODE)
     may now be partially controlled by the user:  see
     ADD-RAW-ARITY.

     + For those using Unix/Linux make:  A cert.acl2 file can contain
     forms to be evaluated before an appropriate certify-book command is
     invoked automatically (not included in cert.acl2).

o Some of the changes in the proof engine (see NOTE-2-8-PROOFS):

     + ACL2 now prevents certain rewriting loops; see
     REWRITE-STACK-LIMIT.

     + Small changes have been made to heuristics for controlling
     rewriting during proofs by induction and in handling certain
     "weak" compound-recognizer rules.

     + The handling of free variables in a hypothesis of a rewrite rule
     (see FREE-VARIABLES) has been improved in the case that
     the hypothesis is of the form (equiv x y), where equiv is a known
     equivalence relation (see EQUIVALENCE).

     + We have modified how the ACL2 simplifier handles the application
     of a defined function symbol to constant arguments, by avoiding
     the introduction of hide when evaluation fails if the term can be
     rewritten.

     + The generation of "Goal" for recursive (and mutually-recursive)
     definitions now uses the subsumption/replacement limitation
     (default 500).  See CASE-SPLIT-LIMITATIONS.

     + Default hints now apply to hints given in definitions, not just
     theorems.  See DEFAULT-HINTS.

     + Linear arithmetic now uses the conclusions of forward-chaining
     rules, and type-set now uses a small amount of linear reasoning
     when deciding inequalities.

o Some of the changes in rules, definitions, and constants (see
NOTE-2-8-RULES):

     + See the above doc topic.

o Guard-related changes are described in see NOTE-2-8-BUG-FIXES.

o Some of the proof-checker changes (see
NOTE-2-8-PROOF-CHECKER):

     + Added new proof-checker commands wrap1, wrap, and wrap-induct,
     to combine multiple conjuncts or goals.

     + The type-alist command now takes optional arguments that control
     whether or not the governors and/or conclusion are used in
     computing the context.

o Some of the system-level changes (see NOTE-2-8-SYSTEM):

     + ACL2 now runs on OpenMCL and on MCL 5.0.

o Some of the other changes (see NOTE-2-8-OTHER):

     + Emacs file emacs/emacs-acl2.el has been updated (see
     NOTE-2-8-OTHER for details).

     + When :pl is given a term other than a symbol, it will print all
     rewrite rules that match that term.

     + A new function, pkg-witness, returns a symbol in the given
     package.

     + The list constant *acl2-exports* has been extended.

     + A new release of the rtl library has been included:
     books/rtl/rel4/.  See the README file in that directory.

Again, please proceed to the subtopics for more thorough release notes.

NOTE-2-8-BUG-FIXES    ACL2 Version  2.8 Notes on Bug Fixes

We have fixed a soundness bug in the tautology checker's handling of
expressions of the form (not (not x)).  This bug has gone back at least
as far as Version_2.4.  All of the regression tests passed after the
fix, without modification.  So we hope that this bug has rarely bitten
anyone.  Thanks to Qiang Zhang for sending us a proof of nil that led
us to this fix: (thm (equal (and p q) (not (or (not p) (not q))))).
And thanks to Matyas Sustik for an observation that led to an
improvement of our initial fix.

The preceding version (2.7) introduced a soundness bug in handling of
ACL2 arrays, in which functions compress1 and compress2 were returning
the input alist rather than compressing it appropriately.  Here is a
proof of nil that no longer succeeds, based on a bug report from Warren
Hunt, who we thank for bringing this problem to our atttention.

     (defthm bad
       (not (let* ((ar2 (aset1 'my-array ar1 3 10))
                   (ar3 (compress1 'my-array ar2))
                   (ar4 (reverse (reverse ar2)))
                   (ar5 (compress1 'my-array ar4)))
              (and (equal ar2 ar4)
                   (not (equal ar3 ar5)))))
       :rule-classes nil)
     (defthm contradiction
       nil
       :rule-classes nil
       :hints (("Goal" :use
                ((:instance bad
                            (ar1 (compress1 'my-array
                                            '((3 . 5)
                                              (:HEADER :DIMENSIONS (5)
                                                       :MAXIMUM-LENGTH 6
                                                       :DEFAULT 0
                                                       :NAME MY-ARRAY)))))))))

On a related note, a new function flush-compress can be used for subtle
control of under-the-hood raw Lisp support for fast array access,
although we expect it to be very rare that users need this extra
support.

Previous versions have had two soundness bugs that can occur when using
the proof-checker:

     o The first bug pertains to the expand command, and hence x and
     x-dumb commands (which call expand); see
     PROOF-CHECKER-COMMANDS.  The bug can occur when applying the
     above commands when the current term is a call of a constrained
     function symbol for which there is a :definition rule.  Now, the
     expand command will succeed only when the function symbol of the
     current term is a defined function symbol, in which case the
     original definition is always used, in analogy to how the :expand
     hint works in the prover; see HINTS.  Thanks to John
     Erickson for sending an example that led us to wonder if there
     might be a soundness problem.

     o The second bug pertains to the s command (and commands that call
     it, e.g., s-prop).  The proof-checker forms a context out of the
     top-level hypotheses and the if-terms governing the current term.
     If there is a contradiction in the top-level hypotheses, the
     proof-checker can appropriately consider the goal to be proved,
     and it does so.  But formerly, the criterion was weaker:  the
     contradiction could involve the combination of the top-level
     hypotheses and if-term governors.  Thanks to Rob Sumners for
     noticing this bug.

A soundness bug could be provoked in some Lisps by applying defpkg to
the empty string.  This has been disallowed.

We fixed a soundness bug related to packages caused by a failure to
track axioms introduced locally on behalf of defpkg events.  See
HIDDEN-DEATH-PACKAGE.

We fixed a soundness bug caused by a failure to check that a
:type-prescription rule can be processed when proofs are skipped or
under a defequiv event.  The former case can occur when processing an
encapsulate or include-book event, where the rule could depend on a
local :compound-recognizer rule preceding the proposed
:type-prescription rule under the same encapsulate or include-book
event.  See LOCAL-INCOMPATIBILITY for such an example.

We fixed a potential soundness bug relating to reclassifying a :program
mode function to :logic mode (as done by verify-termination or the
submission of an appropriate "redundant" definition) without adequate
checking that stobj usage was identical.  Allegedly redundant
definitions must now preserve the stobjs declaration as well as the
formals, body, guard and type declarations.  We thank Vernon Austel for
pointing out this problem.

It was possible to get a raw Lisp error by introducing a locally defined
function with guard verification inhibited and then subsequently
introducing the same definition non-locally without that inhibition.
The following example will clarify.

     (encapsulate nil
       (local
         (defun foo (x) (declare (xargs :guard t :verify-guards nil)) (car x)))
       (defun foo (x) (declare (xargs :guard t)) (car x)))
     ; The following causes a raw lisp error because ACL2 runs the Common Lisp
     ; definition of foo, because it thinks that foo's guard of t was verified.
     (thm (equal (foo 3) xxx))

Thanks to Jared Davis for bringing this problem to our attention.  We
are particularly grateful to Jared because his example exploited this
bug by applying it to a function defined using mbe (introduced in this
same version, 2.8), in order to prove nil!

The sort of error message shown below can legitimately occur when
certifying a book in a certification world where there was an
include-book command with a relative pathname (see PATHNAME).
However, it was occurring more often than necessary.  This has been
fixed.

     ACL2 Error in (CERTIFY-BOOK "foo" ...): The certification world has
     include-book commands for book "bar" that correspond to different
     full pathnames, namely "/u/dir1/bar" and "/u/dir2/bar".  ACL2
     cannot currently certify a book in such a world.  To work around
     this problem, use an absolute pathname for at least one of these
     books (see :DOC pathname).

Bugs were fixed in with-output, in particular related to the use of
values :all.  Also, documentation for with-output has been improved.
Thanks to Vernon Austel for pointing out the bugs.

Fixed a lisp error occurring when bash proof-checker command was given
illegal syntax, e.g., (bash (("Goal" :in-theory (enable
binary-append)))) instead of (bash ("Goal" :in-theory (enable
binary-append))).

We added an appropriate guard to find-rules-of-rune, which will avoid
hard lisp errors when this function is called on non-rune arguments.
Thanks to Eric Smith for pointing out this issue.

It was possible for a redundant include-book form (see
REDUNDANT-EVENTS) to leave a command in the ACL2 logical world and to
cause (re-)loading of a compiled file.  These behaviors have been
fixed.  In particular, if book1 has already been included in the
current ACL2 world and (include-book "book1") occurs in book2, then the
compiled file for book1 will not be loaded again when book2 is
included.  Thanks to Dave Greve for bringing our attention to these
problems, and to Eric Smith for bringing up a special case earlier
(where "//" occurred in the book name).

The summary printed at the end of a proof had not listed :induction
rules used in a proof.  This has been corrected.

The use of proof trees in emacs redefined `control-c control-c' in such
a way that in telnet mode, the telnet session was interrupted and
perhaps could not be continued.  This has been fixed.

Source function load-theory-into-enabled-structure contained a
guard-violating call of compress1.  Thanks to Vernon Austel for
bringing this problem to our attention; even though this bug was benign
(as he pointed out), we like keeping the source code free of guard
violations.

A number of proof-checker atomic macros caused a hard error when all
goals have already been proved.  This has been fixed.  Thanks to John
Erickson for sending an example of the issue.

A bug has been fixed in add-match-free-override.  Formerly, a table
guard violation occurred when calling add-match-free-override more than
once with first argument other than :clear.

Defininitions of functions involving large constants could cause stack
overflows.  This has been fixed, at least in some of the most egregious
cases (by making a source function fn-count-evg tail-recursive).  Thanks
to Jared Davis for bringing this problem to our attention.

Evaluation of computed hints could cause stack overflows.  This has been
fixed.  Thanks to Eric Smith for bringing this problem to our attention.

Evaluation of :monitor on :definition runes is now fast even if the
specified function is part of a very large mutual-recursion nest.
Thanks to Eric Smith for sending an example showing that this wasn't
always the case.

Fixed a bug in books/bdd/cbf.lisp that was causing certification of
distributed bdd books to fail when the connected book directory (see
CBD) differs from the current working directory.  Thanks to
Scott Guthery for bringing this bug to our attention and supplying a
helpful log.

Duplicate rule names have been eliminated from warnings generated upon
the use of enabled :rewrite or :definition rules.  Thanks to Eric Smith
for pointing out this problem.

The trace utilities (see TRACE), as modified for GCL and
Allegro Common Lisp, had failed to show more than the first return
value for so-called "*1*" functions (essentially,
executable-counterpart functions) when they were returning multiple
values (via mv).  This has been fixed.  Thanks to Erik Reeber for
pointing out this problem.  Also, it is now possible to refer to
arglist in trace$ forms when ACL2 is built on GCL, not just when ACL2
is built on Allegro Common Lisp.

Uses of hide introduced during proofs by failed attempts to evaluate
constrained functions (see HIDE) are now tracked, so that the
rune (:DEFINITION HIDE) will show up in the summary.

The following bug, introduced back in Version  2.7, has been fixed.
The bug applied only to GCL and may well not have affected anyone.  But
the function proclamation computed by ACL2 for compilation usually had
an output type of nil where it should have been t.

The macro gc$ had a bug exhibited when it was supplied one or more
arguments.  This has been fixed.

The macro defabbrev broke when supplied a string and no documentation,
e.g., (defabbrev foo () "").  Thanks to Rob Sumners for noticing this
problem and providing a fix, which we have incorporated.

For ACL2 executables built on Allegro Common Lisp, a Lisp error
occurred when trace$ was called on other than a defined function
symbol.  Now ACL2 prints a more useful error message.

The proof-checker no longer accepts a (verify) command when some
function symbol in the original goal no longer exists in the current
ACL2 logical world.  Thanks to John Erickson for bringing this issue to
our attention.

The function ld-redefinition-action may now be called by the user.
Thanks to Vernon Austel for suggesting that we remove this symbol from
the list of so-called untouchables.

The handling of free variables in hypotheses (see
FREE-VARIABLES) of rewrite and linear rules had a bug that prevented
some proofs from going through.  Here is a simple example, essentially
provided by Diana Moisuc, who we thank for bringing this issue to our
attention.  The proof of the thm below had failed, but now will
succeed.  This particular bug prevented, for example, the :all behavior
from occurring when the first hypothesis of the rule does not have free
variables.  NOTE:  Now that this bug has been fixed, you may find some
proofs running much more slowly than before.  You can use
accumulated-persistence to locate rules that are slowing down your
proofs because of excessive attention to free variables, and then
execute add-match-free-override for those rules (or, just change the
rules themselves to specify :once in the :rule-classes).

     (defstub foo1 (* ) => *)
     (skip-proofs
      (defthm aux-foo1
        (implies (and (integerp a)
                      (integerp i)
                      (equal (foo1 0)  (list 0 i)))
                 (equal (foo1 a) (list 0 (+ a i))))
        :rule-classes ((:rewrite :match-free :all))))
     (thm
      (implies (and (integerp i)
                    (integerp a)
                    (equal (foo1 0) (list 0 i)))
               (equal (foo1 a) (list 0 (+ a i)))))

Formerly, creation of large arrays could cause an error in the
underlying Common Lisp implementation without helpful messages for the
user.  Now, we check Common Lisp restrictions on arrays and print a
helpful error message if they are violated, namely: each dimension must
be less than the value of Common Lisp constant array-dimension-limit,
and the product of the dimensions must be less than the value of Common
Lisp constant array-total-size-limit.  Thanks to Warren Hunt for
bringing this issue to our attention.  Note:  this change also removes
a former restriction of stobj array fields to size smaller than 2^28-1,
provided the underlying Lisp can support larger arrays.

The default-hints in the current logical world were ignored by
verify-guards.  This has been fixed.  Thanks to Jared Davis for
pointing out this bug and sending a helpful example.

The brr mechanism has been cleaned up in order to avoid hard errors and
infinite loops that can arrive when typing interrupts (control-c) or
end-of-files (control-d) inside the brr loop.  Thanks to Dave Greve,
Olga Matlin, Eric Smith, and Serita Van Groningen for bringing this
issue to our attention.  As a byproduct, if you type control-d (or if
inside emacs, control-c control-d), you may now quit entirely out of
ACL2 and lisp (see GOOD-BYE) in some cases where you formerly
would not have, for example when sitting at the ACL2 prompt (which
formerly, in Allegro Common Lisp for example, would merely take you
into raw Lisp rather than quitting everything).

We have eliminated structural flaws in the HTML documentation pages that
could make them unreadable in some browsers.  Thanks to Bill Young for
bringing this issue to our attention and to Joe Hendrix for diagnosing
the problem.

The proof-checker could run very slowly after many instructions in a
given session.  This has been fixed; thanks to Art Flatau for bringing
this problem to our attention.  (Implementation detail: We now keep
tag-trees duplicate-free when we accumulate them into state.  This
change could have minor speed advantages for some top-level proofs too,
not just in the proof-checker.)

The printing of accesses to stobjs using nth or update-nth has been done
using symbolic constants since ACL2 Version_2.6.  However, there was a
bug that prevented this feature from working for update-nth except at a
top-level call.  This has been fixed.  Thanks to Julien Schmaltz for
bringing this problem to our attention.  For example, consider these
events:

     (defstobj st field0 field1)
     (thm (equal (nth 1 (update-nth 0 17 st)) (car (cons xxx yyy)))
          :hints (("Goal" :in-theory (disable nth update-nth))))

Before the fix, the proof attempt of the above silly thm printed the
following.

     (NTH 1 (UPDATE-NTH *FIELD0* 17 ST))

After the fix, we instead see the following.

     (NTH *FIELD1* (UPDATE-NTH *FIELD0* 17 ST))

It is now possible to certify and subsequently include books that
require guard-checking to be off.  For example, the book can contain
the form (defconst *silly* (car 3)) even though 3 fails to satisfy the
guard of car.  Formerly, it was necessary to execute
:set-guard-checking nil before a certify-book or include-book in order
for such a form to be handled without error.  Thanks to Hanbing Liu for
bringing this problem to our attention.

Fixed a proof-checker bug that could cause probably cause strange error,
"Attempt to access the plist field".  Thanks to Bill Young for bringing
this problem to our attention.

Fixed a proof-checker bug that was failing to record applications of
rewrite rules using the proof-checker's :rewrite command, causing the
proof summary to omit mention of that rule (for example, when using the
proof-checker's :exit command to generate an :instructions hint).
Thanks to Bill Young for pointing out this bug.

Modernized some of the proof-tree emacs and infix printing stuff,
thanks to suggestions made by Camm Maguire.

NOTE-2-8-GUARDS    ACL2 Version  2.8 Notes on Guard-related Changes

All the guard-related changes may be found elsewhere; in particular,
see NOTE-2-8-BUG-FIXES.

NOTE-2-8-NEW-FUNCTIONALITY    ACL2 Version  2.8 Notes on New Functionality

WARNING: You may find that control-d (in emacs, control-c control-d)
can throw you completely out of Lisp where it had not formerly done so.

(CLISP and Allegro CL only) ACL2 now starts up inside the ACL2 loop --
that is, (LP) is executed automatically -- when built on CLISP or
Allegro CL.  This was already the case for GCL and CMUCL, and it still
is not true for LispWorks.  Thanks to Joe Corneli for bringing the CLISP
command-line option "-i" to our attention, which led to this CLISP
change and inspired reconsideration of how to do this for Allegro CL.

Pete Manolios and Daron Vroon have changed the representation of
ordinals in ACL2, defined algorithms for ordinal arithmetic, and
created a library of theorems to reason about ordinal arithmetic.  We
thank them for these nice contributions.  See NOTE-2-8-ORDINALS
for details, in particular, for how to preserve existing proofs that
depend on the previous ordinal representation.

Sometimes users create rules of class :rewrite that cause an infinite
loop in the ACL2 rewriter.  This has lead to Lisp stack overflows and
even segmentation faults.  Now, the depth of calls of functions in the
ACL2 rewriter is limited, and under user control.  See
REWRITE-STACK-LIMIT.

Macros mbe ("must be equal") and mbt ("must be true") have been
introduced, which allow the user to attach fast executable definitions
to (presumably slower) :logic mode functions.  Thanks to Vernon Austel
for a key idea.  Also provided is a macro defexec, which employs mbe
but enforces the requirement that the executable definition also
terminates.  Thanks to Jose Luis Ruiz Reina for collaborating in the
design and development of defexec, and for useful comments from a
number of others as well in the development of mbe including Joe
Hendrix and Rob Sumners.

Definitions have been added for functions rassoc-eq and rassoc-equal,
which are like rassoc but use different tests and have different
guards.  (Compare assoc-eq and assoc-equal, which are in similar
relation to assoc.)

The user can now control multiple matching for free variables in
hypotheses for :forward-chaining rules, as has already been supported
for :rewrite and :linear rules.  For :forward-chaining rules, "free
variables" are those in the hypotheses not bound by a given trigger
term.  As for :rewrite and :linear rules, free-variable matching may be
limited to the first successful attempt by specifying :match-free :once
with :forward-chaining in the :rule-classes, and
add-match-free-override may be used to modify the behavior of an
existing rule.  Thanks to Erik Reeber for most of the implementation of
these new capabilities, as well as significant assistance with a
corresponding new documentation topic (see
FREE-VARIABLES-EXAMPLES-FORWARD-CHAINING).

It is no longer necessary to specify (set-match-free-error nil) in order
to avoid errors when a rule with free variables in its hypotheses is
missing the :match-free field.  (This was already true during book
certification, but now it is the case in interactive sessions as well.)

The form (break-on-error) causes, at least for most Lisps, entry into
the Lisp debugger whenever ACL2 causes an error.  See
BREAK-ON-ERROR.  Thanks to John Erickson for providing encouragement
to provide this feature.

A new table has been provided so that advanced users can override the
built-in untranslate functionality.  See
USER-DEFINED-FUNCTIONS-TABLE.

The pstack mechanism (formerly denoted checkpoints) has been improved.
The "process [prover] stack," or pstack, is automatically printed when
proofs abort.  Evaluation of function calls on explicit arguments
during proofs is now tracked.  Actual parameters are shown with (pstack
t) rather than formals.  Thanks to Bill Legato for suggesting the first
two of these improvements and, in general, encouraging changes that
make ACL2 easier to use.

The defstobj event is now allowed to take an :inline argument, which
can speed up execution.  Thanks to Rob Sumners for suggesting and
implementing this new feature.

Macro assert$ has been added in order to make it easy to write
assertions in one's code.  Semantically, (assert$ test form) is the same
as form, but it causes a hard error (using illegal) if test evaluates
to nil.

Macro cw-gstack no longer takes arguments for the gstack or state.
However, it now takes a keyword argument (which is optional),
:evisc-tuple, that can be used to control how it prints terms.  In
particular, cw-gstack abbreviates large terms by default, but
(cw-gstack :evisc-tuple nil) causes terms to be printed in full.
Thanks to Robert Krug and Eric Smith for requesting this improvement.

The advanced user now has more control over the evisceration of terms.
See LD-EVISC-TUPLE, in particular the new paragraph on "The
printing of error messages and warnings."

The include-book event now has an additional (optional) keyword, :dir.
The value of :dir should be a keyword that is associated with an
absolute directory pathname to be used in place of the current book
directory (see CBD) for resolving the first argument of
include-book to an absolute pathname.  At start-up, the only such
keyword is :system, so that for example (include-book "arithmetic/top"
:dir :system) will include the book "arithmetic/top" under the "books/"
directory of your ACL2 installation.  But you can associate "projects"
with keywords using add-include-book-dir, e.g., (add-include-book-dir
:my-project "/u/smith/project0/").  See ADD-INCLUDE-BOOK-DIR
and also see DELETE-INCLUDE-BOOK-DIR and see
INCLUDE-BOOK.  Note: You will probably not find :dir :system to be
useful if the distributed books are not placed in the path of their
original location, pointed to by :dir :system, which will often happen
if the executable image is obtained from another site.  Also see
INCLUDE-BOOK, in particular its "soundness warning".

The printing of results in raw mode (see SET-RAW-MODE) may now
be partially controlled by the user:  see ADD-RAW-ARITY.  Also,
newlines are printed when necessary before the value is printed.

For those using Unix/Linux make: A cert.acl2 file can contain forms to
be evaluated before an appropriate certify-book command is invoked
automatically (not included in cert.acl2).

Jared Davis has contributed a new set of books for ordered finite set
theory to the standard distribution,
books/finite-set-theory/osets-0.81/.  See the README file in that
directory.  Thanks, Jared.

Robert Krug has contributed two related changes (thanks, Robert!) in
support of stronger arithmetic reasoning.  First, one can now enable
and disable nonlinear arithmetic with a :nonlinearp hint, which will
override the default provided by set-non-linearp (initially, nil).  See
HINTS.  Second, computed-hints can now have access to the
HISTORY, PSPV, and CTX variables of the waterfall, which (for example)
allows the writing of a hint which will enable nonlinear arithmetic on
precisely those goals that are stable-under-simplificationp.  See
COMPUTED-HINTS.

Robert Krug has contributed a new set of arithmetic books to the
standard distribution, books/arithmetic-3/.  See the README file in that
directory.  Thanks, Robert.

NOTE-2-8-ORDINALS    ACL2 Version  2.8 Notes on Changes to the Ordinals

Please see ORDINALS.

NOTE-2-8-OTHER    ACL2 Version  2.8 Notes on Miscellaneous Changes

Execution of table events has been sped up in many cases by avoiding
excessive consing.

ACL2 now warns if :rewrite (or :definition) rules contain free
variables on the right-hand side.  Thanks to Dave Greve for raising this
issue.

Emacs file emacs/emacs-acl2.el has been updated to better comprehend the
notion of the "ACL2 shell", which is the buffer to which ACL2 forms are
written by commands defined in the above file.  Thus, command control-t
e has been modified always to write to the ACL2 shell (which is
"*shell*" by default), and the following new commands have been defined.

     o control-t c
     Set the ACL2 shell to the current buffer.  o control-t b
     Change to the ACL2 shell.

The commands :pl and :pr may now be given a macro name that corresponds
via the macro-aliases-table to a function name, so that for example :pl
append is treated the same as :pl binary-append.  A more interesting
improvement, for :pl only, is that :pl may now take any term.  When :pl
is given a term other than a symbol, it will print all rewrite rules
that match that term.  Thanks to David Russinoff, Robert Krug, and Bill
Legato for getting this going.

A new function, pkg-witness, returns a symbol in the given package.

The installation instructions have been updated, for example to give
more guidance on obtaining Lisp implementations and to mention the
acl2-help mailing list.

Jared Davis has suggested some symbols to be added to *acl2-exports*,
and we have done so.  Thanks, Jared.

     o MFC (used in syntaxp and extended-metafunctions; thanks also to
     Robert Krug for this one) o ID, CLAUSE, WORLD, and
     STABLE-UNDER-SIMPLIFICATIONP (used   in computed-hints) o
     SET-DEFAULT-HINTS

The command :pe has been improved so that when the event is inside an
included book, the path of included books (from the top-level book down
to the one containing the event) is shown.  Thanks to Eric Smith
(perhaps among others) for pointing out the utility of this improvement.

A new release of the rtl library has been included: books/rtl/rel4/.
See the README file in that directory.

NOTE-2-8-PROOF-CHECKER    ACL2 Version  2.8 Notes on Proof-checker Changes

Added new proof-checker commands wrap1, wrap, and wrap-induct.  Wrap
replaces multiple goals by their conjunction: (wrap instr1 instr2 ...)
employs wrap1 so that the indicated instructions create only at most
one new goal.  Wrap-induct is a simple example of the use of wrap, so
that induction creates only one goal (the conjunction of the base and
induction steps).  Wrap1 can be used immediately after a prover call
(bash, prove, reduce, bdd, or induct) to collapse the new goals into
one.  See PROOF-CHECKER-COMMANDS.

The proof-checker command = failed to work as expected when a governing
IF-test of the current term is T.  This has been fixed (by fixing
source function conjuncts-of).  Thanks to Yoann Padioleau for bringing
this problem to our attention.

The type-alist command now takes optional arguments that control whether
or not the governors and/or conclusion are used in computing the context
that is printed (see PROOF-CHECKER-COMMANDS, specifically
subtopic type-alist).  Thanks to Rob Sumners for suggesting this
improvement.

The macro toggle-pc-macro has always taken an optional second argument
of atomic-macro or macro.  However, this was not clearly documented,
and those two symbols had to be in the ACL2 package.  Both of these
problems have been remedied.  Thanks to John Erickson for bringing the
lack of documentation of the second argument to our attention.

NOTE-2-8-PROOFS    ACL2 Version  2.8 Notes on Changes in Proof Engine

ACL2 now prevents certain rewriting loops; see
REWRITE-STACK-LIMIT.

During the computation of constraints for functional instantiation,
(prog2$ term1 term2) and (the type term2) are now treated as term2.

A change has been made in heuristics for controlling rewriting during
proofs by induction.  Formerly, during induction proofs, ACL2
suppressed rewriting of certain "induction hypothesis" terms, and
forced expansion of certain "induction conclusion" terms, until
rewriting had stabilized.  This meddling with the rewriter is still
turned off when rewriting has stabilized, but it is now turned off
earlier once an ancestor has been through the rewriter and the current
goal is free of "induction conclusion" terms.  Thanks to Dave Greve and
Matt Wilding for providing an example and associated analysis that led
us to look for a heuristic modification.

A change has been made in the heuristics for handling certain "weak"
compound-recognizer rules when building contexts.  Those who want to dig
deeply into this change are welcome to look at the code following the
call of most-recent-enabled-recog-tuple in the code for function
assume-true-false in the ACL2 sources.

The handling of free variables in a hypothesis of a rewrite rule (see
FREE-VARIABLES) has been improved in the case that the
hypothesis is of the form (equiv x y), where equiv is a known
equivalence relation (see EQUIVALENCE).  Previously, if the
rewriter was attempting to rewrite the hypothesis (equiv x y) of a
rewrite rule, in a context where x' is an instance of x, then the
rewriter could fail to notice a term (equiv x' y') true in the current
context where y' is an instance of y, in the case that x' precedes y'
in the term-order.  This has been remedied.  This improvement applies
regardless of whether x, y, or (we believe) both are already fully
instantiated in the present context.  Thanks to Joe Hendrix for
bringing up an example and to Vernon Austel for providing another,
simple example.

A very minor change has been made to the rewriter in the case that an
equality appears on the left-hand side of a :rewrite rule.  Formerly,
when such an equality (equal x y) was commuted to (equal y x) in order
for the rule to match the current term, then all equalities on the
instantiated right-hand side of the rule were commuted, except for
those occurring inside another equality.  The instantiated right-hand
side is no longer modified.  It seems very unlikely that this change
will cause proofs to fail, though we cannot completely rule out that
possibility.

We have modified how the ACL2 simplifier handles the application of a
defined function symbol to constant arguments in certain cases, which
we now describe.  As before, ACL2 attempts to simplify such a function
application by evaluation, provided the :executable-counterpart of the
function is enabled.  And as before, if that evaluation fails due to a
subroutine call of a constrained function (introduced by encapsulate),
ACL2 may wrap a call of hide around this function application.  (See
HIDE.)  But now, ACL2 attempts to apply definitions and rewrite
rules in the case that this evaluation fails, and only if the resulting
term is unchanged does ACL2 wrap hide around this function application.
Thanks to Matt Wilding for bringing up the idea of this modification.

The generation of "Goal" for recursive (and mutually-recursive)
definitions now uses the subsumption/replacement limitation (default
500).  See CASE-SPLIT-LIMITATIONS.

Default hints now apply to hints given in definitions, not just
theorems.  See DEFAULT-HINTS.

Thanks to Robert Krug for implementing the following two improvements
involving linear arithmetic reasoning: linear arithmetic now uses the
conclusions of forward-chaining rules, and type-set now uses a small
amount of linear reasoning when deciding inequalities.

NOTE-2-8-RULES    ACL2 Version  2.8 Notes on Changes in Rules, Definitions, and Constants

The theory minimal-theory has been changed by adding the definition
rune for mv-nth to the theory.  A corresponding change has been made to
the theory warning mechanism, which was failing to warn if the
definition of mv-nth is disabled, even though calls of mv-nth can be
expanded by special-purpose code in the rewriter.  Thanks to Serita Van
Groningen for pointing out this problem with the theory warning
mechanism.

The defevaluator event has been modified so that in the body of the
evaluator function, to add a new case (ATOM X) (returning nil) has been
inserted immediately after the case (EQ (CAR X) 'QUOTE).  This is a
no-op semantically but may speed up proofs.  Thanks to Warren Hunt for
suggesting this change.

A new form of :compound-recognizer rule is now allowed:

     (if (fn x) concl1 concl2)

This is equivalent to an existing form:

     (and (implies (fn x) concl1)
          (implies (not (fn x)) concl2))

Thanks to Josh Purinton for bringing this to our attention.

Rewrite rules realpart-+ and imagpart-+ have been added in order to
simplify the realpart and imagpart (respectively) of a sum.  They
follow from a theorem add-def-complex that equates a sum with the
complex number formed by adding real and imaginary parts.  All three of
these theorems may be found in source file axioms.lisp.  Thanks to Eric
Smith for raising a question leading to these additions, as well as to
Joe Hendrix and Vernon Austel for helpful suggestions.

NOTE-2-8-SYSTEM    ACL2 Version  2.8 Notes on System-level Changes

ACL2 now runs on OpenMCL, "an opensourced Common Lisp implementation,
derived from Digitool's Macintosh Common Lisp product."  Thanks to Greg
Wright and Robert Krug for doing most of the work for this port.

When (LP) is first executed, the underlying raw Lisp package will
change to "ACL2" (if that is not already the current package in raw
Lisp).  This is a minor change that will probably not be noticed, since
up to now it has probably been the case that the ACL2 executable starts
up with "ACL2" as the underlying raw Lisp package.  But this change was
made because we have been informed that ACL2 executables based on
OpenMCL need not start up with "ACL2" as the underlying raw Lisp
package.

ACL2 now runs on MCL 5.0.  Thanks to Pascal Costanza for updates to the
instructions in file mcl-acl2-startup.lisp and for an update to the
ACL2 sources (parameter *compiled-file-extension*).

NOTE-2-8(R)    ACL2 Version  2.8(r) (March, 2003) Notes

The Makefile has been modified by adding a new target, clean-links.
This can be used in order to remove all soft links, which is useful if
the directory is copied or moved to a new location or if there are file
system changes that cause problems with link pathnames.

Please also see NOTE-2-8 for changes to Version_2.8 of ACL2.

NOTE-2-9    ACL2 Version  2.9 (October, 2004) Notes

     *TABLE OF CONTENTS.*

     ==============================
     BUG FIXES.
     NEW FUNCTIONALITY.
     CHANGES IN PROOF ENGINE.
     GUARD-RELATED CHANGES.
     PROOF-CHECKER CHANGES.
     SYSTEM-LEVEL CHANGES.
     BOOK CHANGES.
     MISCELLANEOUS CHANGES.
     ==============================

*BUG FIXES.*

We fixed a soundness bug due to a conflict between user-supplied package
names and internal package names (obtained by prepending a Lisp
constant, *1*-package-prefix*) and user-supplied package names.  For
example, the form (defpkg "ACL2_*1*_MYPKG" ()) is no longer legal.
Thanks to Robert Krug for asking a question that led directly to the
discovery of this bug.

We fixed a soundness bug that allows :logic mode functions to call
:program mode functions.  The fix furthermore prevents functions with
guards verified from calling functions with guards not verified.  We
had thought we already prevented all this, but there was a problem with
the interaction of local definitions and redundancy checking (see
REDUNDANT-EVENTS).

We fixed a soundness bug that could occur when built-in functions were
called during macroexpansion (a hole in so-called "safe-mode").

Fixed a minor bug in system functions genvar1 and genvar, where eq had
been used in place of eql.  This bug was discovered during the plugging
of a hole in safe-mode, mentioned just above.

We fixed handling of the :inline keyword for defstobj, which previously
could cause raw Lisp errors in OpenMCL and CMU Common Lisp.  Thanks to
John Matthews for bringing this issue to our attention.

Calls of include-book could result in a state for which some function
definitions were not compiled that should have been.  The result could
be performance degradation or even stack overflows.  This situation
could arise in the following two ways.

     o Inclusion of a book with an absolute pathname that differs from
     the absolute pathname at certification time, presumably because of
     the use of soft links.  Thanks to Bob Boyer and Warren Hunt for
     bringing a stack overflow to our attention that led us to this fix.

     o Large mutual-recursion nests (more than 20 functions) are
     executed in a superior book.

We fixed some performance bugs that can increase the speed of
include-book calls by a factor of close to 2.  Thanks to Eric Smith for
asking if we could speed up include-book processing; we have done so in
the past, but primarily focusing on large mutual-recursion nests (which
have nothing in particular to do with the current improvements).  Also,
thanks to Rob Sumners for a very useful remark early in the process
that kept us from drawing an incorrect conclusion at that point.

We fixed :pl so that it can be run on a form that returns multiple
values, which it could not do previouslly.  Thanks to Eric Smith for
pointing out this problem.

Fixed a bug in the Allegro ACL2 trace utility (see TRACE$) that
was causing "10>" to be printed as "9>", "11>" to be printed as "10 >",
"12>" to be printed as "11 >", and so on.

Fixed a proof-checker bug that was preventing the use of the DV command
(or a numerical command) on let expressions.  Thanks to Bill Young for
pointing out this problem.

Fixed a bug in a comment on how to set ACL2_BOOKS_DIR in the makefile.
Thanks to Dave Greve for pointing out this problem.

Fixed a potential soundness bug in the linear arithmetic routines.
Thanks to Jared Davis for noticing this problem and to Robert Krug for
implementing the fix.  (Technical details: We had been assuming that
polynomials were being normalized - see the definition of good-polyp in
linear-a.lisp - but this assumption was false.)

When the macro open-trace-file is opened twice in succession, it now
automatically closes the first trace output channel before opening
another.

It is now possible to use make to build ACL2 on Windows systems that
support make.  Thanks to Pete Manolios and Mike Thomas for pointing out
the problem, to Jared Davis and Mike for helping us to analyze the
problem, and to Jared for testing the fix.

Fixed a bug in the guard of with-output that was causing a needless
guard violation.

*NEW FUNCTIONALITY.*

The new events add-default-hints and remove-default-hints allow one to
append to or subtract from the current list of default hints.  The
event set-default-hints continues to set the list of default hints,
discarding the previous value of the default-hints.  Note that
set-default-hints is still local to the encapsulate or book in which it
occurs, and add-default-hints has the same property, although neither
is implemented any longer using the acl2-defaults-table.  New events
add-default-hints!, remove-default-hints!, and set-default-hints! are
the same as add-default-hints, remove-default-hints, and
set-default-hints, respectively, except that the former three events
are not local to their enclosing encapsulate or book.  Thanks to Jared
Davis for suggesting these enhancements.

OpenMCL's tracing routines have been modified in a similar manner as
those of Allegro CL.  Thanks to Robert Krug for providing this
enhancement.

Guard-checking can now be caused to happen on recursive calls.  See
"GUARD-RELATED CHANGES" below for details.

Advanced users can now inhibit compilation of so-called "*1* functions"
with the :comp command; see COMP.  Thanks to Rob Sumners for
suggesting this enhancement.

Added new legal argument hard? for the er macro, which is now
documented.  See ER.  Thanks to Rob Sumners for a discussion
leading to this change.  Also, the three legal first arguments to er --
hard, hard?, and soft -- may now be in any package (thanks to Jared
Davis for bringing this issue to our attention).

We have removed the requirement that for a rule's hypothesis (bind-free
term var-list), at least one variable must occur free in term.  For
example, the expression (bind-free (bind-divisor a b) (x)) was legal
because a and b occur free in (bind-divisor a b); but (bind-free (foo
(bar)) (x)) was not legal.  The latter is no longer disallowed.
(Technical note: this allows bind-free to be used to create explicit
substitutions in metafunction hypotheses.)

The following two enhancements have been implemented for rules of class
:meta.  Thanks to Eric Smith for requesting more control of reasoning
with :meta rules, which led to these enhancements, and to him and
Robert Krug for helpful discussions.

     o It is now possible to control backchaining in rules of class
     :meta by providing a :backchain-limit-lst argument, as was already
     allowed for rules of class :rewrite and :linear.  See
     RULE-CLASSES.  However, unlike those other two rule classes, the
     value for :backchain-limit-lst is prohibited from being a
     non-empty list; it must be either nil or a non-negative integer.

     o (For advanced users.) It is now legal for hypothesis
     metafunctions to generate, in essense, calls of syntaxp and
     bind-free, handled essentially as they are handled in hypotheses
     of :rewrite and :linear rules.  We say "essentially" primarily
     because both syntaxp and bind-free are actually macros, but
     hypothesis metafunctions must generate translated terms (see
     TERM).  The enterprising advanced user can call :trans to see
     examples of translated terms corresponding to calls of syntaxp and
     bind-free.

A new command :trans! has been added, which is like :trans except that
:trans! ignored issues of single-threadedness.  See TRANS!.
Thanks to Eric Smith for suggesting this addition.

The :pf command now works when the argument is the name of a macro
associated with a function by macro-aliases-table.

*CHANGES IN PROOF ENGINE.*

The simplifier has been changed slightly in order to avoid using
forward-chaining facts derived from a literal (essentially, a top-level
hypothesis or conclusion) that has been rewritten.  As a practical
matter, this may mean that the user should not expect forward-chaining
to take place on a term that can be rewritten for any reason (generally
function expansion or application of rewrite rules).  Formerly, the
restriction was less severe: forward-chaining facts from a hypothesis
could be used as long as the hypothesis was not rewritten to t.  Thanks
to Art Flatau for providing an example that led us to make this change;
see the comments in source function rewrite-clause for details.

The rewriter has been modified to work slightly harder in relieving
hypotheses.  Thanks to Eric Smith for providing an example that
inspired the following, which illustrates the issue.  Suppose we
introduce functions foo and bar with the (non-local) properties shown
below.

      (encapsulate
       (((foo *) => *)
        ((bar *) => *))

       (local (defun foo (x) (declare (ignore x)) t))
       (local (defun bar (x) (declare (ignore x)) t))

       (defthm foo-holds
         (implies x
                  (equal (foo x) t)))
       (defthm bar-holds-propositionally
         (iff (bar x) t)))

Consider what happens when ACL2's rewriter is used to prove the
following theorem.

     (thm (foo (bar y)))

With ACL2's inside-out rewriting, (bar y) is first considered, but
rewrite rule bar-holds-propositionally does not apply because the
context requires preserving equality, not mere Boolean (iff)
equivalence.  Then the rewriter moves its attention outward and sees
the term (foo (bar y)).  It attempts to apply the rule foo-holds, in a
context created by binding its variable x to the term (bar y).  It then
attempts to relieve the hypothesis x of rule foo-holds in that context.
Before this change, ACL2 basically assumed that since rewriting was
inside out, then (bar y) had already been rewritten as much as
possible, so the rewrite of x in the aforementioned context (binding x
to (bar y)) simply returned (bar y), and the attempt to relieve the
hypothesis of foo-holds failed.  The change is essentially for ACL2's
rewriter to make a second pass through the rewriter when the attempt
fails to rewrite a variable to t, this time using the fact that we are
in a Boolean context.  (We mention that source function
rewrite-solidify-plus implements this idea, for those who want to dig
deeply into this issue.)  In our example, that means that the rewriter
considers (bar y) in a Boolean context, where it may apply the rule
bar-holds-propositionally to relieve the hypothesis successfully.

When (set-non-linearp t) has been executed, non-linear-arithmetic can
now be applied in some cases for which it previously was not.  Thanks
to Robert Krug for supplying this modification and to Julien Schmaltz
for providing a motivating example.

We modified the rewriter to avoid certain infinite loops caused by an
interaction of the opening of recursive functions with equality
reasoning.  (This change is documented in detail in the source code, in
particular functions rewrite-fncall and fnstack-term-member.)  Thanks
to Fares Fraij for sending us an example that led us to make this
change.

The :executable-counterpart of function hide is now disabled when ACL2
starts up.  This removes an anomoly, for example that

     (thm (not (equal 1 (* (hide 0) a))))

succeeded while

     (thm (equal (foo (equal 1 (* (hide 0) a))) (foo nil)))

failed.  Now both fail.

The theory *s-prop-theory* is no longer used by the proof-checker; it
has been replaced by (theory 'minimal-theory.  We have left the
constant *s-prop-theory* defined in the source code in support of
existing books, however.  This change eliminates annoying theory
warnings printed upon invocation of proof-checker commands s-prop, sl,
and split.

Terms are now kept in an internal form that avoids calls of primitive
functions (built-ins without explicit definitions; see code for
cons-term for details), in favor of the constants that result from
evlaluating those calls.  So for example, the internal form for (cons 1
2) is (quote (1 . 2)).  This change was made at around the same time as
changes in support of bind-free; see above.  One consequence is that the
splitting of goals into cases (technically, source function clausify and
even more technically, source function call-stack) has been modified,
which can cause subgoal numbers to change.

*GUARD-RELATED CHANGES.*

Guard-checking can now be caused to happen on recursive calls, where
this was formerly not the case for :program mode functions and, perhaps
more important, for :logic mode functions whose guards have not been
verified.  Moreover, a warning is printed when ACL2 does not rule out
the exclusion of guard-checking on recursive calls.  See
SET-GUARD-CHECKING.  Thanks to David Rager for bringing this issue to
our attention, and to Rob Sumners and the Univ. of Texas ACL2 seminar
in general for their feedback.

Guard violations are reported with less of the offending term hidden.
Thanks to Jared Davis for suggesting that we look at this issue.

*PROOF-CHECKER CHANGES.*

We fixed the proof-checker so that diving works as you might expect for
a macro call (op a b c) representing (binary-op a (binary-op b c)).  In
the past, if the current term was of the form (append t1 t2 t3), then
(DV 3) (and 3) would dive to t3 even though the corresponding function
call is (binary-append t1 (binary-append t2 t3)).  This is still the
case, but now this behavior holds for any macro associated with a
function in binop-table (see ADD-BINOP).  Moreover, users can
now write customized diving functions; see
DIVE-INTO-MACROS-TABLE, and also see books/misc/rtl-untranslate.lisp
for example calls to add-dive-into-macro.  Of course, the old behavior
can still be obtained using the proof-checker's DIVE command; see
PROOF-CHECKER-COMMANDS.

The runes command in the proof-checker now shows only the runes used by
the most recent primitive or macro command (as shown by :comm), unless
it is given a non-nil argument.  Also, proof-checker command
lemmas-used has been added as, in essence, an alias for runes.

(The following two items are also mentioned above under "BUG FIXES.")

Fixed a proof-checker bug that was preventing the use of the DV command
(or a numerical command) on let expressions.  Thanks to Bill Young for
pointing out this problem.

The theory *s-prop-theory* is no longer used by the proof-checker; it
has been replaced by (theory 'minimal-theory.  We have left the
constant *s-prop-theory* defined in the source code in support of
existing books, however.  This change eliminates annoying theory
warnings printed upon invocation of proof-checker commands s-prop, sl,
and split.

*SYSTEM-LEVEL CHANGES.*

Fixed a problem with building ACL2 on CMUCL in some systems (source
function save-acl2-in-cmulisp).  Thanks to Bill Pase for bringing this
to our attention.

The installation instructions have been extended to include
instructions for building on GCL in Mac OS X.  Thanks to Jun Sawada and
Camm Maguire.

Initial pre-allocation of space has been updated for GCL to reflect more
current GCL executables (we considered GCL 2.6.1-38).  This can help
avoid running out of memory for large ACL2 sessions.

The main Makefile has been replaced by GNUmakefile, in order to enforce
the use of GNU make.  If you use another make program, you'll get an
error message that may help you proceed.

(GCL only) SGC is no longer turned on for GCL 2.6 sub-versions through
2.6.3 if si::*optimize-maximum-pages* is bound to T, due to an apparent
issue with their interaction in those sub-versions.  Also, we have
eliminated preallocation for all versions after 2.6.1 because GCL
doesn't need it (comments are in source function save-acl2-in-akcl).
Thanks to Camm Maguire for excellent GCL help and guidance, and to Camm
and Bob Boyer for useful discussions.

We have removed support for so-called "small" images.  Thus, :doc, :pe
and :pc, verify-termination, and other commands are fully supported in
ACL2 saved images.  Because of this and other changes in the generation
of the so-called "*1*" logical functions, related to guards (as
described above in -GUARD-RELATED CHANGES", and related to the
discussion of safe-mode in "BUG FIXES" above), image sizes have
increased substantially.

We no longer time or run "nice" the certification of individual books.
The file books/Makefile-generic had done these by default, and some
individual distributed and workshop book directories had Makefiles that
did so as well.  Thanks to Mike Thomas, who pointed out the lack of
nice on some Windows systems (and we decided on this simple solution).
Overall targets in books/Makefile still time their runs by default, and
the partiular time program is now controlled by a Makefile variable.

Failures during make certify-books or make regression now show up in
the log as "**CERTIFICATION FAILED**", regardless of the operating
system (as long as it supports make).  Formerly, one searched for "**"
but this did not appear in openMCL runs.

We have eliminated "Undefined function" warnings that could occur in
OpenMCL.

*BOOK CHANGES.*

Reconciled the definitions of firstn in book/misc/csort.lisp,
books/bdd/bdd-primitives.lisp, books/ordinals/ordinal-definitions.lisp,
and books/data-structures/list-defuns.lisp.  Thanks to Ray Richards for
bringing this issue to our attention.

Distributed book books/misc/defpun now can handle stobjs where it did
not previously.  Thanks to John Matthews for bringing this issue to our
attention.

The "make" variable COMPILE_FLG in file books/Makefile-generic formerly
only had an effect if there was a cert.acl2 file present.  That
oversight has been remedied.

File "books/arithmetic/certify.lsp" was missing a certify-book command
for "natp-posp".  Thanks to John Cowles for noticing this deficiency
and supplying a fix.  (This file is of use to those who want to certify
the "books/arithmetic/" books without using "make".)

A few small changes have been made to "books/rtl/rel4".

Small changes were made to books misc/symbol-btree and
misc/rtl-untranslate.  In particular, the definition of symbol-btreep
was strengthened.

We made a minor fix to books/ordinals/e0-ordinal.lisp, adding
(verify-guards ob+) and hence (verify-guards ocmp) as well.  This was
necessitated by the fix prohibiting functions with guards verified from
calling functions with guards not verified (see also the related
discussion under "BUG FIXES" above).

*MISCELLANEOUS CHANGES.*

Further sped up processing of large mutual-recursion nests (extending
what was done for Version_2.7), perhaps by a factor of two in some
cases.

As promised in Version_2.5 (see NOTE-2-5), structured pathnames
are no longer supported.  So for example, the argument to include-book
must now be a string constant.

Some documentation has been improved, for stobjs thanks to suggestions
by John Matthews and much of the rest thanks to feedback from Eric
Smith.

The function current-package is now available to users (it has been
taken off the list of so-called "untouchables").  Thanks to Jared Davis
for bringing this issue to our attention.

The documentation for topic using-computed-hints-7 has been improved.
Thanks to Doug Harper and Eric Smith for inspiring this improvement.

We added several symbols to *acl2-exports*: cw, er, intern$,
set-case-split-limitations, and set-difference-eq.  Thanks to Jared
Davis for suggesting most of these.

Now, a table event that sets the value for a key, (table tbl key val
:put), is redundant (see REDUNDANT-EVENTS) when it does not
change the value associated with an existing key of the table.  In
particular, define-pc-macro is now fully redundant when it does not
change an existing proof-checker macro-command definition.  Thanks to
Bill Young for bringing the latter issue to our attention.

The definitions of unused system functions ev-w and ev-w-lst have been
deleted.

ACL2 now prints a warning if a defpkg event introduces a package name
with lower-case letters, since there is opportunity for later confusion
in that case.  Thanks to Frederic Peschanski for bringing this problem
to our attention and Sandip Ray for encouragement.

ACL2 now works in Version 19 of CMU Common Lisp.

The function sys-call has been modified so that for ACL2 built on
Allegro Common Lisp in Unix or Linux, the existing environment is used.
Thanks to Erik Reeber for bringing this issue to our attention.

The function disabledp can now be given a macro name that has a
corresponding function; see MACRO-ALIASES-TABLE.  Also,
disabledp now has a guard of t but causes a hard error on an
inappropriate argument.

NOTE-2-9(R)    ACL2 Version  2.9(r) (October, 2004) Notes

No changes have been made for support of non-standard analysis, other
than a minor modification or two in books/nonstd/ books.

Please also see NOTE-2-9 for changes to Version_2.9 of ACL2.

NOTE-2-9-1    ACL2 Version  2.9.1 (December, 2004) Notes

(GCL only) A bug in symbol-package-name has been fixed that could be
exploited to prove nil, and hence is a soundness bug.  Thanks to Dave
Greve for sending us an example of a problem with defcong (see below)
that led us to this discovery.

ACL2 now warns when defcong specifies equal as the first equivalence
relation, e.g., (defcong equal iff (member x y) 2).  The warning says
that the rule has no effect because equal already refines all other
equivalence relations.  Formerly, this caused an error unless
:event-name was supplied (see DEFCONG), and in fact the error
was a nasty raw Lisp error on GCL platforms due to some mishandling of
packages by ACL2 that has been fixed (see the paragraph about
symbol-package-name above).  Thanks to Dave Greve for sending a helpful
example in his report of this problem.

(GCL only) The build process was broken for GCL 2.6.0 (and perhaps some
earlier versions), and has been fixed.  Thanks to Jose Luis Ruiz-Reyna
for bringing this problem to our attention.

(GCL only) We have increased the hole size to at least 20% of max-pages,
which may eliminate some garbage collection at the expense of larger
virtual memory (not larger resident memory or larger image).  Thanks to
Camm Maguire for helpful explanations on this topic.

We have clarified the guard warning message that is printed during
evaluation of recursively-defined functions whose guards have not been
verified, for example:

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

And, ACL2 no longer prints that message when the guard was unspecified
for the function or was specified as T.  Thanks to Serita Nelesen for
bringing the latter issue to our attention.  Finally, ACL2 now prints
such a warning at most once during the evaluation of any top-level
form; thanks to Bill Young for pointing out this issue.

The function verbose-pstack has been enhanced to allow specified prover
functions *not* to be traced.  See VERBOSE-PSTACK.

Added lp, wet, and set-non-linearp to *acl2-exports*, and hence to the
"ACL2-USER" package.

The distributed book books/arithmetic-3/bind-free/integerp.lisp has
been modified in order to prevent potential looping; specifically, the
definition of function reduce-integerp-+-fn-1.  Thanks to Robert Krug
for providing this change.

A small improvement was made in the wet failure message when the error
occurs during translation to internal form.  Thanks to Jared Davis for
pointing out the obscurity of some wet error messages.

We have improved ACL2's evaluation mechanism for the function
bad-atom<=, which now is specified to return nil if neither argument is
a so-called "bad atom" (as recognized by function bad-atom).  The
following events had caused a hard error, for example.  (We're sorry
that bad-atom and bad-atom<= are not documented, but we also consider
it unlikely that anyone needs such documentation; otherwise, please
contact the implementors.)

     (defun foo (x y) (declare (xargs :guard t)) (bad-atom<= x y))
     (defun bar (x y) (declare (xargs :guard t)) (foo x y))
     (thm (equal (bar 3 4) 7))

We have also changed the guard on alphorder to require both arguments
to be atoms.

For forms (local x) that are skipped during include-book, or during the
second pass of certify-book or encapsulate, ACL2 had nevertheless
checked that x is a legal event form.  This is no longer the case.

The proof-checker now does non-linear arithmetic when appropriate.  It
had formerly ignored set-non-linearp executed in the ACL2 command loop.

Incremental releases are now supported.  See VERSION and
{obsolete after Version  4.3} set-tainted-okp.  Thanks to Hanbing Liu
for discovering a flaw in our original design.

The pattern-matching algorithm for :rewrite rules has been made
slightly more restrictive, thanks to a suggestion and examples from
Robert Krug.  For example, previously one could get an infinite loop as
follows.

     (defstub foo (x) t)
     (defaxiom foo-axiom
       (equal (foo (+ 1 x))
              (foo x)))
     (thm (foo 0)) ; or replace 0 by any integer!

That is because the term (foo 0) was considered to match against the
pattern (foo (+ 1 x)), with x bound to -1.  While such matching is
sound, it leads to an infinite loop since it allows foo-axiom to
rewrite (foo 0) to (foo -1), and then (foo -1) to (foo -2), and so on.
The fix is to insist that the new value, in this case -1, is no larger
in size according to acl2-count than the old value, in this case 0.
Since that test fails, the match is considered to fail and the loop no
longer occurs.  An analogous fix has been made for multiplication,
where now we only match when the new term is still a non-zero integer.
That change avoids a loop here.

     (defstub foo (x) t)
     (defaxiom foo-axiom
       (equal (foo (* 2 x))
              (foo x)))
     (thm (foo 0)) ; or try (thm (foo 4))

Added macro find-lemmas in books/misc/find-lemmas.lisp (see brief
documentation there) for finding all lemmas that mention all function
symbols in a given list.

:Restrict hints now work for :definition rules, though they continue to
be ignored by the preprocessor and hence you may want to use :do-not
'(preprocess) with any restrict hints.  Thanks to John Matthews for
pointing out the lack of support for :definition rules in :restrict
hints.

Some books have been updated.  In particular, there is a new directory
books/workshops/2004/ in workshops distribution, for the 2004 ACL2
workshop.  There is also a new version of Jared Davis's ordered sets
library, formerly in books/finite-set-theory/osets-0.81/ but now in
books/finite-set-theory/osets/.

Fixed a bug in the (under-the-hood) raw Lisp definition of defchoose,
which had been causing a warning in CMU Common Lisp.

[Technical improvements related to the use of "make dependencies" for
certifying distributed books:]
File books/Makefile-generic now does a better job with "make
dependencies," specifically with respect to handling *.acl2 files and
handling include-book commands with :dir :system.  Regarding the
latter, suppose for example that book basic.lisp contains the line:

     (include-book "arithmetic/top-with-meta" :dir :system)

Then make dependencies would generate the following line:

     basic.cert: $(ACL2_SRC_BOOKS)/arithmetic/top-with-meta.cert

Thus, if :dir :system is used with include-book, the corresponding
Makefile should define the variable ACL2_SRC_BOOKS.  A standard
Makefile header for a books directory could thus be as follows.

     # The following variable should represent the ACL2 source directory.  It is the
     # only variable in this Makefile that may need to be edited.
     ACL2_SRC = ../../../../../..

     ACL2_SRC_BOOKS = $(ACL2_SRC)/books
     include $(ACL2_SRC_BOOKS)/Makefile-generic
     ACL2 = $(ACL2_SRC)/saved_acl2

Finally, the "-s" flag may now be omitted when running "make
dependencies."

NOTE-2-9-2    ACL2 Version  2.9.2 (April, 2005) Notes

Also see NOTE-2-9-1 for other changes since the last
non-incremental release (Version_2.9).

There was a bug in non-linear arithmetic (see
NON-LINEAR-ARITHMETIC) that caused the following error:

     ACL2 !>(include-book "rtl/rel4/lib/top" :dir :system)
     ....
     ACL2 !>(set-non-linearp t)
      T
     ACL2 !>(thm
      (implies (and (bvecp a 77)
                    (bvecp b 50))
               (bvecp (fl (/ (* a b) (expt 2 23)))
                      104))
      :hints (("Goal" :in-theory (enable bvecp))))

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

     By the simple :definition BVECP, the :executable-counterparts of EXPT
     and UNARY-/ and the simple :rewrite rule ASSOCIATIVITY-OF-* we reduce
     the conjecture to

     Goal'
     (IMPLIES (AND (INTEGERP A)
                   (<= 0 A)
                   (< A 151115727451828646838272)
                   (INTEGERP B)
                   (<= 0 B)
                   (< B 1125899906842624))
              (BVECP (FL (* A B 1/8388608)) 104)).

     HARD ACL2 ERROR in VARIFY:  This should not have happened.  The supposed
     variable, '1/8388608, is instead a constant.

     ACL2 !>

Thanks to Robert Krug for providing a fix for the above error.

Guard-checking was being inhibited (since v2-9) for calls of built-in
primitives on explicit values, e.g., (car 3).  This has been fixed.

Guard-related warnings could be printed during proofs (this bug was
introduced in Version_2.9.1).  These warnings have been eliminated.

Compound-recognizer rules natp-compound-recognizer and
posp-compound-recognizer are now built into ACL2 for predicates natp
and posp, and hence have been deleted from book natp-posp.lisp (where
they were called natp-cr and posp-cr, respectively).

The function file-clock-p, which recognizes a component of the ACL2
state, is now defined using natp instead of integerp.  Thanks to Jared
Davis for suggesting this change.  (Technical explanation about
functions in ACL2 source file axioms.lisp: With a file-clock of -1, the
call of make-input-channel in open-input-channel will create a channel
that can't be closed; see the guard of close-input-channel.)

(Allegro CL users only) Support is now provided for building an Allegro
CL application, provided you have an Allegro CL dynamic runtime
license.  (Our belief is that with such a license, many users can use
the same application, rather than each user needing a separate
license.)  See new GNUmakefile target allegro-app and file
build-allegro-exe.cl for more information.

The new home page now contains a link to a new page other-releases.html,
which contains information about other ACL2 releases.  (This is in one's
local home page, but may not show up on the central ACL2 home page
until the next non-incremental release.)  Thanks to Warren Hunt for
suggesting this addition.

We thank Erik Reeber for suggesting a solution to output redirection
using sys-call, which we have described at the end of its documentation.

A new documentation topic fixes the flawed argument for conservativity
of the defchoose event that appears in Appendix B of Kaufmann and
Moore's paper, "Structured Theory Development for a Mechanized Logic"
(Journal of Automated Reasoning 26, no. 2 (2001), pp. 161-203).  See
CONSERVATIVITY-OF-DEFCHOOSE.  Thanks to John Cowles and Ruben
Gamboa for helpful feedback on drafts of this note.

The solution to exercise 6.15 in books/textbook/chap6/solutions.txt has
been fixed.  Thanks to Aaron Smith for pointing out the problem.

A new documentation topic defun-sk-example gives a little more help in
using defun-sk effectively.  Thanks to Julien Schmaltz for presenting
this example as a challenge.

(GCL only) There is now a way to speed up GCL builds of ACL2, at the
cost of perhaps a percent or so in performance of the resulting image.
Using make one supplies the following.

     LISP='gcl -eval "(defparameter user::*fast-acl2-gcl-build* t)"

Various makefiles have been improved in several ways.

     (1) Parallel book certification, using GNU make's -j option, can
     be used.

     (2) Book certifications now stops at the first failure if
     books/Makefile or books/Makefile-generic is used, and returns
     non-zero exit status.  However, the various make targets in the
     ACL2 source directory (regression, certify-books, etc.) still
     continue past failures unless you provide ACL2_IGNORE=' ' on the
     make command line.

     (3) The build process has been modified (file GNUmakefile) so that
     it stops upon a failed compile or a failed initialization.

     (4) The automatic dependency generation (from "make dependencies"
     has been improved so that commands of the form (ld "my-book.lisp")
     in .acl2 files cause the appropriate depedencies to be generated.

Thanks to comments from several users that led to the above Makefile
improvements: Ray Richards, Doug Harper, and the Rockwell ACL2 users
for (1) and (2) (and inspiring (4)), and David Rager for (2) and (3).
In particular, Doug Harper sent a replacement for the .date mechanism,
which was interfering with make -n; so, these files are no longer
written.

A mechanism has been added for saving output.  In particular, you can
now call ld on a file with output turned off, for efficiency, and yet
when a proof fails you can then display the proof attempt for the
failed (last) event.  See SET-SAVED-OUTPUT.  Another new
command -- see SET-PRINT-CLAUSE-IDS -- causes subgoal numbers
to be printed during proof attempts when output is inhibited.

Documentation has been added for using ACL2's makefile support to
automate the certification of collections of books.  See
BOOK-MAKEFILES.

Fixed a bug in sys-call-status that was causing hard Lisp errors.

Improved cw-gstack to allow a :frames argument to specify a range of
one or more frames to be printed.  see CW-GSTACK.

Fixed a bug in proof-checker command forwardchain.  Thanks to Ming-Hsiu
Wang for bringing this bug to our attention.

We have provided a mechanism for saving an executable image.  See
SAVING-AND-RESTORING and see SAVE-EXEC.  We have eliminated
obsolete functions note-lib and make-lib.

Modified the ground-zero theory so that it contains all of the built-in
rules (in ACL2 source file axioms.lisp).  It had formerly failed to
include rules from some definitions and theorems near the end of
axioms.lisp.

A new event, set-enforce-redundancy, allows the enforcement of defthm,
defun, and most other events during book development.  See
SET-ENFORCE-REDUNDANCY.

A bug has been fixed that had allowed deftheory events to cause a hard
Lisp error when calling union-theories on ill-formed theories after,
for example:

     :set-guard-checking nil
     (in-theory (union-theories '((:rewrite no-such-rule))
                                (current-theory 'ground-zero)))

The handling of guard checking has been modified somewhat in a way that
should only very rarely affect users.  (An "Essay on Guard Checking" in
the ACL2 source code explains this point to anyone interested in
implementation details.)

(GCL ONLY) Removed the -dir setting in the ACL2 wrapper script for GCL.
This should generally have no effect for most users, but it eliminates
a potential source of error down the road.

Several interesting new definitions and lemmas have been added to the
rtl library developed at AMD, and incorporated into books/rtl/rel4/lib/.
Other book changes include a change to lemma truncate-rem-elim in
books/ihs/quotient-remainder-lemmas.lisp, as suggested by Jared Davis.

The macro real/rationalp may now be referred to in in-theory events and
hints, thanks to a new add-macro-alias event.  Thanks to Jared Davis
for this suggestion.

ACL2 terms of the form (if p 'nil 't) are now printed as (not p), where
in some setting they had been printed as (and (not p) t).  Thanks to
Robert Krug for this improvement.

(GCL ONLY) Added profiling support, based heavily on code supplied by
Camm Maguire.  See file save-gprof.lsp for instructions.  Thanks to
Camm, and also to David Hardin for inspiring this addition.

Added support for preprocessing before printing (untranslating) a term.
See USER-DEFINED-FUNCTIONS-TABLE, in particular the discussion
of untranslate-preprocess.  Thanks to Jared Davis for inspiring this
addition, and for providing a book that takes advantage of it
(books/misc/untranslate-patterns.lisp).

The documentation has been improved for explaining how runes are
assigned; see RUNE.  Thanks to Robert Krug for pointing out
inaccuracies in the existing documentation.

NOTE-2-9-3    ACL2 Version  2.9.3 (August, 2005) Notes

Also see NOTE-2-9-1 and see NOTE-2-9-2 for other
changes since the last non-incremental release (Version_2.9).

We fixed a soundness bug that exploited the ability to define :program
mode functions that are improperly guarded, and then to use those
functions in defconst forms.  The fix is to evaluate defconst forms
using the same "safe-mode" that is used in macroexpansion (see
GUARDS-AND-EVALUATION).  Here is a proof of nil that succeeded in
Allegro Common Lisp (but not, for example, GCL).  See also a long
comment in source function defconst-fn for an example that does not
require the use of :set-guard-checking.

     :set-guard-checking nil ; execute before certifying the book below

     (in-package "ACL2")

     (encapsulate
      ()
      (local (defun f1 ()
               (declare (xargs :mode :program))
               (char-upcase (code-char 224))))
      (local (defconst *b* (f1)))
      (defun f1 ()
        (char-upcase (code-char 224)))
      (defconst *b* (f1))
      (defthm bad
        (not (equal *b* (code-char 224)))
        :rule-classes nil))

     (defthm ouch
       nil
       :hints (("Goal" :use bad))
       :rule-classes nil)

We fixed a soundness hole due to the fact that the "LISP" package does
not exist in OpenMCL.  We now explicitly disallow this package name as
an argument to defpkg.  Thanks to Bob Boyer and Warren Hunt for bringing
an issue to our attention that led to this fix.

ACL2 now requires all package names to consist of standard characters
(see STANDARD-CHAR-P, none of which is lower case.  The reason
is that we have seen at least one lisp implementation that does not
handle lower case package names correctly.  Consider for example the
following raw lisp log (some newlines omitted).

     >(make-package "foo")
     #<"foo" package>
     >(package-name (symbol-package 'FOO::A))
     "foo"
     >(package-name (symbol-package '|FOO|::A))
     "foo"
     >

Distributed book books/textbook/chap10/compiler, as well as workshop
books in directory books/workshops/2004/cowles-gamboa/support/, were
modified to accommodate the above change.

Added newline, add-to-set-eql, the-fixnum, and the-fixnum!  to
*acl2-exports*.  Thanks to Jared Davis for bringing these to our
attention.

Added a line to acl2.lisp to support CMUCL running on Mac OSX, thanks to
a suggestion from Fabricio Chalub Barbosa do Rosario.

The executable scripts for saved ACL2 images now include $*, so that
command-line arguments will be passed along.

(For GCL profiling only) Fixed a colon (:) that should have been a
semicolon (;) in file save-gprof.lsp.  Thanks to David Hardin for
pointing out this bug.

The documentation for :elim rules has been expanded and improved,
thanks to useful feedback from Hanbing Liu.

Fixed a bug in the guard for function include-book-dir.

For those who want to experiment with an alternate implementation of mv
and mv-let, there is now support for under-the-hood implementation of
these in terms of raw Lisp functions values and multiple-value-bind,
respectively.  The regression suite has seen about a 10% speed-up in
Allegro CL and about an 8% slowdown in GCL for builds with this change.
See the makefile (GNUmakefile) for examples of how to build ACL2 by
including the feature, :acl2-mv-as-values.  Source file init.lsp has
been renamed to init.lisp in support of this change (technical detail:
otherwise GCL loads the init file too soon, before its -eval argument
is evaluated).  Thanks to David Rager for inspiring this change, by
pointing out the problematic use of globals by the existing mv
implementation from the standpoint of supporting parallel evaluation.
This capability is experimental: there is likely to be some remaining
work to be done on it.

A change related to the one just above is that we now limit the maximum
number of arguments to any call of mv to 32.  Thanks to Bob Boyer for
raising a question that lead to this change.

Eliminated some compiler warnings in OpenMCL.

In the rtl library (books/rtl/rel4/), functions bits and setbits have
had their guards improved (as they had been too restrictive, especially
for setbits).

A new function time$ permits timing of forms, by using (under the hood)
the host Common Lisp's time utility.

We fixed an infinite loop that could occur during destructor elimination
(see ELIM).  Thanks to Sol Swords to bringing this to our
attention and sending a nice example, and to Doug Harper for sending a
second example that we also found useful.

The method of speeding up GCL-based builds (see NOTE-2-9-2) has
changed slightly from Version_2.9.2.  Now, in the make command:

       LISP='gcl -eval "(defparameter user::*fast-acl2-gcl-build* t)"

We improved the pretty-printer's handling of keywords.  For example,
before this change one might see the following printed by ACL2.

     (MODIFY TH S :KEY1 VAL1 :KEY2
             (IF (IF X Y Z) AAAAAAAAAA BBBBBBB))

Now, the above might print as follows.  Notice that we have avoided
breaking after a keyword (see KEYWORDP) that is preceded by
other forms on the same line.

     (MODIFY TH S
             :KEY1 VAL1
             :KEY2 (IF (IF X Y Z) AAAAAAAAAA BBBBBBB))

See NOTE-2-9-3-PPR-CHANGE for a detailed discussion of this
change.

(GCL ONLY) Evaluation in a break is no longer inhibited by ACL2 when
built on top of GCL, so GCL now matches other Common Lisps in this
respect.

For ACL2 built on most host Common Lisps, you will see the string [RAW
LISP] in the prompt, at least at a break, to emphasize that one is
inside a break and hence should probably quit from the break.  See
BREAKS.

Jared Davis suggested improvements to lemmas len-update-nth (in source
file axioms.lisp) and append-true-listp-type-prescription (in
books/meta/term-defuns.lisp), which have been incorporated.  The former
required a change in books/workshops book
2004/ruiz-et-al/support/q-dag-unification.cert, which has been made.

The proof-checker command rewrite allows further binding of free
variables in hypotheses, with new optional argument instantiate-free.
Proof-checker command show-rewrites (sr) gives corresponding additional
information.  Documentation for these commands has been improved; see
PROOF-CHECKER-COMMANDS.  Thanks to John Matthews and Bill Young
for suggestions and feedback leading to these improvements.

Fixed downcase printing so that the package name of a symbol is also
downcased.  For example, after execution of (defpkg "FOO" nil) and
(set-acl2-print-case :downcase), 'foo::ab will print back as the same,
rather than as 'FOO::ab.

It is now possible to control the output so that numbers are printed in
binary, octal, or hex, though the default is still radix 10.  See
SET-PRINT-BASE.  Note that in support of this change, built-in
functions explode-nonnegative-integer and explode-atom now take an
extra print-base argument.  Different support for radix conversion may
be found in a book newly contributed by Jun Sawada,
books/misc/radix.lisp.

Built-in axiom car-cdr-elim is now only an :elim rule.  It was formerly
both an :elim rule and a :rewrite rule.  A new rule, cons-car-cdr,
takes the place of the old :rewrite rule, but is instead a
hypothesis-free rule that can cause a case split (see source file
axioms.lisp).  Thanks to Jared Davis for suggesting this change.

Lemmas about alphorder (alphorder-reflexive, alphorder-transitive,
alphorder-anti-symmetric, and alphorder-total) are now available.
(They had been local in source file axioms.lisp.)  Thanks to Serita
Nelesen for bringing this issue to our attention.

ACL2 has, for some time, printed a space in the event summary after the
open parenthesis for a defthm event, in order to ease backward
searching for the original form, for example (defthm bar ...):

     Form:  ( DEFTHM BAR ...)

The intention was that this extra space should be printed for every
event form; but it was missing in some cases, for example, for
verify-guards.  This has been fixed.

In analogy to include-book, now ld takes the (optional) keyword
argument :dir.  Thanks to Jared Davis for providing an implementation of
this feature and to Eric Smith and Jeff Marshall for requesting this
feature.

We fixed a bug in include-book that could cause an error when
redefinition is on, for example:

     (set-ld-redefinition-action '(:warn! . :overwrite) state)
     (include-book "/u/acl2/books/arithmetic/top")

The behavior of include-book now matches the documentation: handling of
compiled files for uncertified books will follow the same rules as for
certified books.  In particular, if you create an object file in raw
Lisp for some book, then including that book will load that object
file.  Thanks to Jared Davis for bringing this issue to our attention.

New documentation explains the interaction of redefinition and
redundancy.  See REDUNDANT-EVENTS -- the "Note About
Unfortunate Redundancies" is new.  Thanks to Grant Passmore for
providing examples that led us to write this additional documentation.

Solutions to exercises in "How To Prove Theorems Formally"
(`http://www.cs.utexas.edu/users/moore/publications/how-to-prove-thms')
are now available in distributed book books/misc/how-to-prove-thms.lisp.
Also in that directory may be found a new book hanoi.lisp that contains
a solution to the Towers of Hanoi problem.