This edition is intended primarily as an on-line user's manual for the associated ACL2 library of register-transfer logic and computer arithmetic, which is publicly available as a part of the standard ACL2 release through the University of Texas Web site, at
This document was generated using the LaTeX2HTML translator in order to facilitate its navigation with a Web browser. One feature provided by LaTeX2HTML is a hypertext link associated with every reference to a definition, lemma, or other labeled location in the text, thereby providing for its immediate retrieval. For example, this link to Lemma 11.2.1 of Chapter 11 may be followed with a click of the mouse, after which the browser's back button may be used to return the user to this preface.
Every definition or result is labeled with the name of the corresponding ACL2 event, as illustrated below.
PROOF: This result is easily established by the method of infinite descent.
PROOF: I have discovered a truly marvelous proof to this, which this page is too small to contain.
PROOF: Suppose we have a counterexample, , where . Then either is a power of 2, in which case it is divisible by 4, or is divisible by an odd prime . In the first case, we may write and hence,
Note that these event names are mouse-sensitive. When the user clicks on an event name in this window, the event appears in a second window, which is automatically created for the purpose of displaying ACL2 code. Similarly, clicking on the name of an event in the code window causes the informal version to appear in this window.
The events of interest are of two classes: defun and defthm. Definitions in the text usually correspond to defun events (although there are exceptions, e.g., Definition 1.1.1), and all derived results correspond to defthm events. Most results are labelled as lemmas, but several are classified instead as theorems for the sake of emphasis, and some as corollaries to suggest their dependence on preceding results. This classification is somewhat arbitrary has no significance from the formal (ACL2) perspective.
It is an important aspect of the theory that it has been completely formalized in the ACL2 logic. Consequently, every result appearing in the text is represented in the ACL2 code. In general, the formalization is straightforward, as illustrated by the foregoing example, with the caveat discussed in the preface: a hypothesis in the text version of a lemma stipulating that a variable is real-valued is replaced in the formalization by (rationalp x). In some cases, on the other hand, the user will notice that the hypotheses of ACL2 events are weaker than the informal versions: a hypothesis that is an integer might also be replaced by (rationalp x), or even omitted altogether. Thus, the statement that was proved mechanically is actually stronger than that which is claimed in the text. When this occurs, it may be assumed that the text version captures the cases of interest, while the weakening of hypotheses in the formal version may serve to speed up the application of the lemma by simplifying the task of the rewriter.
Moreover, the correspondence between informal results and defthm events is not quite bijective. Some events that are included for technical reasons are not sufficiently interesting from the reader's perspective to be represented in the text, although the ACL2 user is encouraged to examine the event files more closely. In other cases, for the sake of readability, several ACL2 events are combined into a single lemma. When this occurs, the events are grouped together in the ACL2 file and the text lemma is linked to the first event in the group.
Block Island, Rhode Island
David Russinoff 2017-08-01