This is acl2-doc-emacs.info, produced by makeinfo version 4.5 from
acl2-doc-emacs.texinfo.
This is documentation for ACL2 Version 3.1
Copyright (C) 2006 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.
INFO-DIR-SECTION Math
START-INFO-DIR-ENTRY
* acl2: (acl2-doc-emacs.info). Applicative Common Lisp
END-INFO-DIR-ENTRY
File: acl2-doc-emacs.info, Node: The Tours, Next: The WARNING about the Trivial Consequence, Prev: The Time Taken to do the Associativity of App Proof, Up: Pages Written Especially for the Tours
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.
Flying Tour: *note A Flying Tour of ACL2:: Walking Tour: *note 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."
File: acl2-doc-emacs.info, Node: The WARNING about the Trivial Consequence, Next: Undocumented Topic, Prev: The Tours, Up: Pages Written Especially for the Tours
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.
File: acl2-doc-emacs.info, Node: Undocumented Topic, Next: Using the Associativity of App to Prove a Trivial Consequence, Prev: The WARNING about the Trivial Consequence, Up: Pages Written Especially for the Tours
Undocumented Topic Undocumented Topic
This topic has not yet been documented. Sorry
File: acl2-doc-emacs.info, Node: Using the Associativity of App to Prove a Trivial Consequence, Next: What Is ACL2(Q), Prev: Undocumented Topic, Up: Pages Written Especially for the Tours
Using the Associativity of App to Prove a Trivial Consequence Using the Associativity of App to Prove 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
Walking Tour: *note Overview of the Proof of a Trivial Consequence::
File: acl2-doc-emacs.info, Node: What Is ACL2(Q), Next: What is Required of the User(Q), Prev: Using the Associativity of App to Prove a Trivial Consequence, Up: Pages Written Especially for the Tours
What Is ACL2(Q) What Is ACL2?
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.
Flying Tour: *note What is a Mathematical Logic(Q)::
File: acl2-doc-emacs.info, Node: What is Required of the User(Q), Next: What is a Mathematical Logic(Q), Prev: What Is ACL2(Q), Up: Pages Written Especially for the Tours
What is Required of the User(Q) What is Required of the User?
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.
Flying Tour: *note How Long Does It Take to Become an Effective
User(Q)::
File: acl2-doc-emacs.info, Node: What is a Mathematical Logic(Q), Next: What is a Mechanical Theorem Prover(Q), Prev: What is Required of the User(Q), Up: Pages Written Especially for the Tours
What is a Mathematical Logic(Q) What is a Mathematical Logic?
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 *note 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.
Flying Tour: *note What is a Mechanical Theorem Prover(Q)::
File: acl2-doc-emacs.info, Node: What is a Mechanical Theorem Prover(Q), Next: What is a Mechanical Theorem Prover(Q) (cont), Prev: What is a Mathematical Logic(Q), Up: Pages Written Especially for the Tours
What is a Mechanical Theorem Prover(Q) What is a Mechanical Theorem Prover?
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.
Flying Tour: *note What is a Mechanical Theorem Prover(Q) (cont)::
File: acl2-doc-emacs.info, Node: What is a Mechanical Theorem Prover(Q) (cont), Next: You Must Think about the Use of a Formula as a Rule, Prev: What is a Mechanical Theorem Prover(Q), Up: Pages Written Especially for the Tours
What is a Mechanical Theorem Prover(Q) (cont) What is a Mechanical Theorem Prover? (cont)
To get around this, mechanical theorem provers often require help from
the user.
See *Note ACL2 as an Interactive Theorem Prover:: to continue downward.
Flying Tour: *note About Models::
File: acl2-doc-emacs.info, Node: You Must Think about the Use of a Formula as a Rule, Prev: What is a Mechanical Theorem Prover(Q) (cont), Up: Pages Written Especially for the Tours
You Must Think about the Use of a Formula as a Rule You Must Think about the Use of a Formula as a Rule
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)
Walking Tour: *note Using the Associativity of App to Prove a Trivial
Consequence::
File: acl2-doc-emacs.info, Node: REAL, Next: RELEASE-NOTES, Prev: Pages Written Especially for the Tours, Up: Top
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."
* Menu:
* I-CLOSE:: ACL2(r) test for whether two numbers are infinitesimally close
* I-LARGE:: ACL2(r) recognizer for infinitely large numbers
* I-LIMITED:: ACL2(r) recognizer for limited numbers
* I-SMALL:: ACL2(r) recognizer for infinitesimal numbers
* REAL-LISTP:: ACL2(r) recognizer for a true list of real numbers
* STANDARD-NUMBERP:: ACL2(r) recognizer for standard numbers
* STANDARD-PART:: ACL2(r) function mapping limited numbers to standard numbers
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.
File: acl2-doc-emacs.info, Node: I-CLOSE, Next: I-LARGE, Prev: REAL, Up: REAL
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 *note REAL::).
File: acl2-doc-emacs.info, Node: I-LARGE, Next: I-LIMITED, Prev: I-CLOSE, Up: 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
*note REAL::).
File: acl2-doc-emacs.info, Node: I-LIMITED, Next: I-SMALL, Prev: I-LARGE, Up: 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 *note
REAL::).
File: acl2-doc-emacs.info, Node: I-SMALL, Next: REAL-LISTP, Prev: I-LIMITED, Up: 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 *note
REAL::).
File: acl2-doc-emacs.info, Node: REAL-LISTP, Next: STANDARD-NUMBERP, Prev: I-SMALL, Up: 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 *note
REAL::).
File: acl2-doc-emacs.info, Node: STANDARD-NUMBERP, Next: STANDARD-PART, Prev: REAL-LISTP, Up: 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 *note I-LIMITED::).
This predicate is only defined in ACL2(r) (see *note REAL::).
File: acl2-doc-emacs.info, Node: STANDARD-PART, Prev: STANDARD-NUMBERP, Up: 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 *note I-CLOSE::) to x. This function
is only defined in ACL2(r) (see *note REAL::).
File: acl2-doc-emacs.info, Node: RELEASE-NOTES, Next: RULE-CLASSES, Prev: REAL, Up: Top
RELEASE-NOTES pointers to what has changed
* Menu:
* NOTE-2-0:: ACL2 Version 2.0 (July, 1997) Notes
* NOTE-2-1:: ACL2 Version 2.1 (December, 1997) Notes
* NOTE-2-2:: ACL2 Version 2.2 (August, 1998) Notes
* NOTE-2-3:: ACL2 Version 2.3 (October, 1998) Notes
* NOTE-2-4:: ACL2 Version 2.4 (August, 1999) Notes
* NOTE-2-5:: ACL2 Version 2.5 (June, 2000) Notes
* NOTE-2-5(R):: ACL2 Version 2.5(r) (June, 2000) Notes
* NOTE-2-6:: ACL2 Version 2.6 (November, 2001) Notes
* NOTE-2-6(R):: ACL2 Version 2.6(r) (November, 2001) Notes
* NOTE-2-7:: ACL2 Version 2.7 (November, 2002) Notes
* NOTE-2-7(R):: ACL2 Version 2.7(r) (November, 2002) Notes
* NOTE-2-8:: ACL2 Version 2.8 (March, 2004) Notes
* NOTE-2-8(R):: ACL2 Version 2.8(r) (March, 2003) Notes
* NOTE-2-9:: ACL2 Version 2.9 (October, 2004) Notes
* NOTE-2-9(R):: ACL2 Version 2.9(r) (October, 2004) Notes
* NOTE-2-9-1:: ACL2 Version 2.9.1 (December, 2004) Notes
* NOTE-2-9-2:: ACL2 Version 2.9.2 (April, 2005) Notes
* NOTE-2-9-3:: ACL2 Version 2.9.3 (August, 2005) Notes
* NOTE-2-9-4:: ACL2 Version 2.9.4 (February, 2006) Notes
* NOTE-2-9-5:: Changes in Version 3.0 since Version 2.9.4
* NOTE-3-0:: ACL2 Version 3.0 (June, 2006) Notes
* NOTE-3-0(R):: ACL2 Version 3.0(r) (June, 2006) Notes
* NOTE-3-0-1:: ACL2 Version 3.0.1 (August, 2006) Notes
* NOTE-3-0-1(R):: ACL2 Version 3.0.1(r) (August, 2006) Notes
* NOTE-3-0-2:: ACL2 Version 3.0.2 (December, 2006) Notes
* NOTE-3-1:: ACL2 Version 3.1 (December, 2006) Notes
* NOTE-3-1(R):: ACL2 Version 3.1(r) (December, 2006) Notes
* NOTE1:: Acl2 Version 1.1 Notes
* NOTE2:: Acl2 Version 1.2 Notes
* NOTE3:: Acl2 Version 1.3 Notes
* NOTE4:: Acl2 Version 1.4 Notes
* NOTE5:: Acl2 Version 1.5 Notes
* NOTE6:: Acl2 Version 1.6 Notes
* NOTE7:: ACL2 Version 1.7 (released October 1994) Notes
* NOTE8:: ACL2 Version 1.8 (May, 1995) Notes
* NOTE8-UPDATE:: ACL2 Version 1.8 (Summer, 1995) Notes
* NOTE9:: ACL2 Version 1.9 (Fall, 1996) Notes
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).
File: acl2-doc-emacs.info, Node: NOTE-2-0, Next: NOTE-2-1, Prev: RELEASE-NOTES, Up: RELEASE-NOTES
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.
File: acl2-doc-emacs.info, Node: NOTE-2-1, Next: NOTE-2-2, Prev: NOTE-2-0, Up: RELEASE-NOTES
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.
File: acl2-doc-emacs.info, Node: NOTE-2-2, Next: NOTE-2-3, Prev: NOTE-2-1, Up: RELEASE-NOTES
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.
File: acl2-doc-emacs.info, Node: NOTE-2-3, Next: NOTE-2-4, Prev: NOTE-2-2, Up: RELEASE-NOTES
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.
File: acl2-doc-emacs.info, Node: NOTE-2-4, Next: NOTE-2-5, Prev: NOTE-2-3, Up: RELEASE-NOTES
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.
File: acl2-doc-emacs.info, Node: NOTE-2-5, Next: NOTE-2-5(R), Prev: NOTE-2-4, Up: RELEASE-NOTES
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 *Note 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
*note 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 *note 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 *note 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 *Note 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 *note 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 *Note 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 *note 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 *Note
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 *Note 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 *note PATHNAME::, see *note CBD::, and see *note 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 *Note 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 *note DEFINE-PC-MACRO::) and proof-checker meta commands
(see *note 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 *Note 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.
File: acl2-doc-emacs.info, Node: NOTE-2-5(R), Next: NOTE-2-6, Prev: NOTE-2-5, Up: RELEASE-NOTES
NOTE-2-5(R) ACL2 Version 2.5(r) (June, 2000) Notes
Important changes to non-standard version:
Please see *note NOTE-2-5:: for changes to Version 2.5 of ACL2. We
hope to write more documentation for ACL2(r) in the future.
File: acl2-doc-emacs.info, Node: NOTE-2-6, Next: NOTE-2-6(R), Prev: NOTE-2-5(R), Up: RELEASE-NOTES
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 NOTE-2-6-NEW-FUNCTIONALITY::):
o Changes in proof engine (see *note NOTE-2-6-PROOFS::):
o Changes in rules and definitions (see *note NOTE-2-6-RULES::):
o Guard-related changes (see *note NOTE-2-6-GUARDS::):
o Proof-checker changes (see *note NOTE-2-6-PROOF-CHECKER::):
o System-level changes (see *note NOTE-2-6-SYSTEM::):
o Other (minor) changes (see *note NOTE-2-6-OTHER::):
* Menu:
* NOTE-2-6-GUARDS:: ACL2 Version 2.6 Notes on Guard-related Changes
* NOTE-2-6-NEW-FUNCTIONALITY:: ACL2 Version 2.6 Notes on New Functionality
* NOTE-2-6-OTHER:: ACL2 Version 2.6 Notes on Other (Minor) Changes
* NOTE-2-6-PROOF-CHECKER:: ACL2 Version 2.6 Notes on Proof-checker Changes
* NOTE-2-6-PROOFS:: ACL2 Version 2.6 Notes on Changes in Proof Engine
* NOTE-2-6-RULES:: ACL2 Version 2.6 Notes on Changes in Rules and Constants
* NOTE-2-6-SYSTEM:: ACL2 Version 2.6 Notes on System-level Changes
File: acl2-doc-emacs.info, Node: NOTE-2-6-GUARDS, Next: NOTE-2-6-NEW-FUNCTIONALITY, Prev: NOTE-2-6, Up: NOTE-2-6
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 *Note
STANDARD-CHAR-P:: and see *note 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).