ACL2 Version 2.0
|
|
ACL2 Version 2.0
|
Here are the two common entries to the documentation graph:
|
Major Topics (Table of Contents)
|
|
Index of all documented topics
|
, indicate that the links lead out of
introductory level material and into user-level material. It is easy for the
newcomer to get lost.
Here is how we recommend you use this documentation.
If you are a newcomer to ACL2, we do not recommend that you wander off into the full documentation. Instead start with the tours the tours.
If you are a serious ACL2 student and have taken the tours and done the tutorials, we recommend you read selected topics from ``Major Topics'':
-- the top-level commands like 
DEFUN and DEFTHM
-- all the Common Lisp functions ACL2 supports
-- how you can influence ACL2's behavior with rules,
-- how to create re-usable databases of rules.
Finally, experienced users tend mostly to use the ``Index'' to lookup concepts mentioned in error messages or vaguely remembered from their past experiences with ACL2.
Note: If ACL2 has been installed on your local system, the HTML documentation
should also be available locally. You can minimize network traffic by
browsing your local copy. Suppose ACL2 was installed on
/usr/jones/acl2/v2-0. Then the local URL for this page is
file:/usr/jones/acl2/v2-0/acl2-sources/doc/HTML/acl2-doc.html.
Many ACL2 users set a browser bookmark to this file and use their browser to
access the documentation during everyday use of ACL2. If you obtain ACL2,
please encourage users to use the local copy of the documentation rather than
access it across the Web.
Note: The documentation is available in four forms: 3.5 megabytes of postscript
(which prints as an 800 page book), HTML, EMAC's Texinfo, and ACL2's own :DOC
commands. The
documentation, in all four forms, is distributed with the source code for the
system. See the doc/ subdirectory of the directory upon which ACL2
is installed.
In its native state, ACL2 ``knows'' very little about arithmetic and other
commonly used mathematical theories. Such knowledge is imparted to ACL2 in the
form of ``books'' written by users; books contain definitions and theorems that
ACL2 interprets as rules to guide its search for a proof. Users have
written some books that may help you. We list a few of them here. The pathnames
below are relative to the books/ subdirectory of the ACL2 directory.
arithmetic/top-with-meta -- elementary arithmetic
data-structures/list-defuns -- definitions of list functions
data-structures/list-defthms -- theorems about list functions
data-structures/deflist -- a tool for defining typed lists
data-structures/list-theory -- brings in all three of the above books
data-structures/set-defuns -- definitions of set functions
data-structures/set-defthms -- theorems about set functions
data-structures/set-theory -- brings in both the definitions and theorems
data-structures/alist-defuns -- definitions of alist functions
data-structures/alist-defthms -- theorems about alist functions
data-structures/defalist -- a tool for defining typed alists
data-structures/alist-theory -- brings in all three of the above books
data-structures/number-list-defuns -- definitions about lists of numbers
data-structures/number-list-defthms -- theorems about number list functions
data-structures/number-list-theory -- brings in both the definitions and theorems
data-structures/structures -- a tool for definining typed record structures
(include-book name), where name is the full pathname of the
book.
An infix syntax for ACL2 has been implemented by Michael Smith. Two capabilities are supported.
Function idiv (m : integer, n : integer | n ~= 0)
{ ifix ( m/n ) };
/* Idiv takes two integer arguments, the second of which cannot = zero */
Theorem distributivity-of-minus-over-plus
{-(x + y) = -x + -y};
Theorem car-nth-0 { consp(x) -> x.car = x[0] };