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.
(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))))
"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.,
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.
in-package is not an embedded event form, the only
in-package in a book is the initial one. Because
not an embedded event form, a book can never contain a
include-book is an embedded event form, books may
contain references to other books. This makes books structured
When the forms in a book are read from the file, they are read with
current-package set to the package named in the
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
(in-package "ACL2-X") and then contains the form
(defun fn (x) (acl2::list 'car x))then
carare 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::defunwould be the same symbol as
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 multiple packages,
their judicious use is a way to minimize name clashes. Often, a
better way is to use
local; see local.
include-book know the definitions of the packages used in a
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.