This is documentation for ACL2 Version 3.4
Copyright (C) 2008  University of Texas at Austin

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

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

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

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

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.

See Corroborating Models to continue

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.  Just follow the Walking Tour after exploring the
explanations.

     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 apply the 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.

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

Newcomers to ACL2 should first take the "Flying Tour."  Then, if you
want to know more, take the "Walking Tour."

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 Web browsers:  This "page" actually contains many
other pages of our documentation, organized alphabetically and separated
by many blank lines.  Be careful when using the scroll bar!

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.

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 you engaged in the mathematically trivial act of proving
the associativity rule 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.
The Makefile provided with ACL2 has target large-acl2r for building
ACL2(r) images.  To see which image you have, 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 as of Version 2.5:
although we (Kaufmann and Moore) have carefully completed Gamboa's
integration of the reals into the ACL2 source code, our primary concern
to date 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 this release we believe ACL2
Version  2.5 is sound.  We are confident that ACL2(r) will behave much
as it does now and will ultimately be sound; but we have not yet argued
the soundness of every detail of the integration.

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-NUMBERP    ACL2(r) recognizer for standard numbers

(Standard-numberp x) is true if and only if x is a "standard" number.
This notion of "standard" comes from non-standard analysis and is
discussed in Ruben Gamboa's dissertation.  In brief, all the familiar
real numbers are standard, but non-zero infinitesimals are not
standard, nor are numbers that exceed every integer that you can
express in the usual way (1, 2, 3, and so on).  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).

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

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.