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.

(assert$ test form)

Raises an error if the given test fails.

Examples:

> (assert$ (< 0 1) t)

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.

Examples:

> (defaxiom sbar (equal t nil)               :rule-classes nil               :doc ":Doc-Section ...")

(deflabel name :doc doc-string)

Defines a label, for adding a landmark and/or adding a documentation topic.

Examples:

> (deflabel interp-section               :doc ":Doc-Section ...")

eval:588:0: deflabel: undefined in: deflabel

(defstub name args-sig => output-sig :doc doc-string)

(deftheory name term :doc doc-string)

Defines a theory (to enable or disable a set of rules)

Examples:

> (deftheory interp-theory                (set-difference-theories                  (universal-theory :here)                  (universal-theory 'interp-section)))

(defthm name term :rule-classes rule-classes :instructions instructions :hints        hints :otf-flg      otf-flg :doc          doc-string)

Defines a theorem to be proved and named.

Examples:

> (defthm x+x=2x (= (+ x x) (* 2 x)))

(in-theory term :doc doc-string)

Examples:

> (in-theory (set-difference-theories                  (universal-theory :here)                  '(flatten (:executable-counterpart flatten))))

(include-book "<basename>")

(include-book "<basename>" :dir :system)

(include-book "<basename>" :dir :teachpacks)

The include-book form imports definitions from a file called a book. Dracula supports three variants.

  (include-book "my-path/my-book")

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 expressions.

  (include-book "my-path/my-book" :dir :system)

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 ACL2 Books for the list of books supported by Dracula.

  (include-book "my-path/my-book" :dir :teachpack)

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 Teachpacks for the list of provided teachpacks.

(mutual-recursion def1 ... defn)

For defining mutually-recursive functions.

Examples:

> (mutual-recursion      (defun evenlp (x)        (if (consp x) (oddlp (cdr x)) t))      (defun oddlp (x)        (if (consp x) (evenlp (cdr x)) nil)))

(theory-invariant term :key key :error t/nil)

(defconst name val)

Defines a constant value. The name must begin and end with asterisks.

Examples:

> (defconst *PI* 22/7)

> (* 2 *PI*)

44/7

(defun name (args) (declare decl ...) ... body)

Defines a function.

Examples:

> (defun absolute-value (x)          (cond            ((< x 0) (* -1 x))            (t x)))

> (absolute-value 5)

5

> (absolute-value -5)

5

(declare d ...)

Used in defun to give ACL2 extra information about a function.

(defequiv pred)

Declares pred to be an equivalence predicate. It is equivalent to the following, with the supplied name substituted for pred in all identifiers:

(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))