Major Section: BOOKS
Example Book:The first form in a book must be; This book defines my app function and the theorem that it is ; associative. One irrelevant help lemma is proved first but ; it is local and so not seen by include-book. I depend on the ; inferior book "weird-list-primitives" from which I get ; definitions of hd and tl.
(in-package "MY-PKG")
(include-book "weird-list-primitives")
(defun app (x y) (if (consp x) (cons (hd x) (app (tl x) y)) y))
(local (defthm help-lemma (implies (true-listp x) (equal (app x nil) x))))
(defthm app-is-associative (equal (app (app a b) c) (app a (app b c))))
(in-package "pkg") where
"pkg" is some package name known to ACL2 whenever the book is
certified. The rest of the forms in a book are embedded event
forms, i.e., defuns, defthms, etc., some of which may be
marked local. See embedded-event-form. The usual Common
Lisp commenting conventions are provided. Note that since a book
consists of embedded event forms, we can talk about the
``local'' and ``non-local'' events of a book.
Because in-package is not an embedded event form, the only
in-package in a book is the initial one. Because defpkg is
not an embedded event form, a book can never contain a defpkg
form. Because include-book is an embedded event form, books may
contain references to other books. This makes books structured
objects.
When the forms in a book are read from the file, they are read with
current-package set to the package named in the in-package
form at the top of the file. The effect of this is that all symbols
are interned in that package, except those whose packages are given
explicitly with the ``::'' notation. For example, if a book begins
with (in-package "ACL2-X") and then contains the form
(defun fn (x)
(acl2::list 'car x))
then defun, fn, x, and car are all interned in the
"ACL2-X" package. I.e., it is as though the following form
were read instead:
(acl2-x::defun acl2-x::fn (acl2-x::x)
(acl2::list 'acl2-x::car acl2-x::x)).
Of course, acl2-x::defun would be the same symbol as
acl2::defun if the "ACL2-X" package imported acl2::defun.
If each book has its own unique package name and all the names
defined within the book are in that package, then name clashes
between books are completely avoided. This permits the construction
of useful logical worlds by the successive inclusion of many books.
Although it is often too much trouble to manage several packages,
their judicious use is a way to minimize name clashes. Often, a
better way is to use local; see local.
How does include-book know the definitions of the packages used in a
book, since defpkgs cannot be among the forms? More generally,
how do we know that the forms in a book will be admissible in the
host logical world of an include-book? See certificate for
answers to these questions.
