1.3 Events and Definitions
ACL2 events are special terms which define new functions or logical rules.
Defined names are in scope within their own definition and below; forward
references are not allowed. Use the mutual-recursion event for
mutually recursive functions.
Raises an error if the given test fails.
| > (assert$ (< 0 1) t)|
| > (assert$ (< 1 0) t)|
assert$: Assertion failed!
(< 1 0)
|(defaxiom name term :rule-classes rule-classes :doc doc-string)|
Defines an axiom. Using defaxiom
is not recommended.
Defines a label, for adding a landmark and/or adding a documentation topic.
| > (deflabel interp-section|
| :doc ":Doc-Section ...")|
|(defstub name args-sig => output-sig :doc doc-string)|
Defines a theory (to enable or disable a set of rules)
| > (deftheory interp-theory|
| (universal-theory :here)|
| (universal-theory 'interp-section)))|
|(defthm name term|
|(defthmd name term|
These two forms both define a theorem to be proved and named.
form defines an enabled function that will be
automatically used in subsequent proof attempts.
form defines a disabled function that must be
explicitly mentioned in hints.
| > (in-theory (set-difference-theories|
| (universal-theory :here)|
| '(flatten (:executable-counterpart flatten))))|
form imports definitions from a file called a
. Dracula supports three variants.
Without a :dir option, Dracula adds a ".lisp" extension to the base
name and attempts to load a file relative to the current directory. In the case
above, the program must reside in a directory with a "my-path" subdirectory
containing a book named "my-book.lisp".
Books must be valid Dracula programs; they must start with
(in-package "ACL2"); and they must contain only events, no top-level
This variant loads a book from the system directory included with an ACL2
installation. Dracula simulates only a couple of the definitions from these
books, but allows other books to be included for theorem proving purposes. See
for the list of books supported by Dracula.
The third variant loads one of the books provided with Dracula, called
teachpacks. These books make use of DrScheme features such as interactive
animations and other i/o, and are also reflected in the ACL2 logic. See
for the list of provided teachpacks.
For defining mutually-recursive functions.
Defines a constant value. The name must begin and end with asterisks.
| > (defconst *PI* 22/7)|
| > (* 2 *PI*)|
|(defun name (args) (declare decl ...) ... body)|
|(defund name (args) (declare decl ...) ... body)|
These two forms both define a function.
form defines a logically-enabled function, about which
proof attempts can reason automatically.
form defines a logically-disabled function, about which
proof attempts may only reason if given a hint.
| > (defun absolute-value (x)|
| ((< x 0) (* -1 x))|
| (t x)))|
| > (absolute-value 5)|
| > (absolute-value -5)|
| > (defun square-of (x)|
| (* x x))|
| > (square-of 3)|
| > (square-of -3)|
Used in defun
to give ACL2 extra information
about a function.
Declares pred to be an equivalence predicate. It is equivalent to the
following, with the supplied name substituted for pred in all
| (defthm pred-is-an-equivalence|
| (and (booleanp (pred x y))|
| (pred x x)|
| (implies (pred x y) (pred y x))|
| (implies (and (pred x y)|
| (pred y z))|
| (pred x z)))|
| :rule-classes (:equivalence))|