How to update the database

We assume you've read introduction-to-rewrite-rules-part-1 and introduction-to-key-checkpoints.

The theorem prover's heuristics are influenced by the database of rules and
the enabled/disabled status of the rules. You can think of the database as a
*global* hint, potentially affecting all parts of a proof attempt.

However, in addition to the ``global hint,'' it is possible to give
*local* hints that affect the theorem prover's behavior on specific
subgoals. We discuss the database here and discuss local hints later in the
tutorial.

The theorem prover's ``database'' is called the *ACL2 world*. You
change the world by issuing commands called *events*. The most common
events are

We recommend that upon the first reading of this tutorial you do not follow the links shown below! The links take you into the hypertext reference manual, where it is easy to get lost unless you're looking for detail about one specific feature.

See defun *name* of the function or predicate, the list of
*formal parameters*, *v1,...vn*, and the *body*:

(defunname(v1 ... vn)body)

If the event is accepted, a *definitional axiom* is added to the
world, *name* *v1...vn**body*, stored as a special
kind of unconditional rewrite rule. However, the *measure theorems* must be proved
to establish that recursively defined functions always terminate, by proving
that an *ordinal* measure of the formal parameters decreases in a
*well-founded* way in every recursive call. In addition, if
*guards* are being used to declare the *expected domain* of the
newly defined function, *guard theorems* might be proved to establish
that all functions stay within their expected domains. In any case, you may
provide additional information to the

(defunname(v1 ... vn) (declare (xargs ...))body)

The

See defthm *name* for the theorem you're trying to prove and a
*formula* stating the theorem. You may optionally supply some local
hints as we describe later in the tutorial. You may also optionally supply
some *rule classes* indicating how you want your formula stored as a
rule, after it is proved. We discuss the *rule classes*
below.

See in-theory *runes*.
A *theory* is just a set (list) of runes. The *current theory* is
the list of enabled runes and the

See include-book

; * for the most elementary arithmetic, needed for any problem ; that involves even simple addition and multiplication like ;(+ x (* 2 y) -3) : (include-book "arithmetic/top-with-meta" :dir :system) ; * for more complicated arithmetic involving non-linear terms like ;(* x y) ,(expt x (+ i j)) , andfloor andmod (include-book "arithmetic-5/top" :dir :system)

But for a complete list of system books, see books

See certify-book

See defconst

See defmacro *compute* the form to
which some type-in expands. For example, the primitive macro

See defstobj *single-threaded object* that
your functions may modify ``destructively'' provided they follow strict
syntactic rules.

See events

There are also commands that allow you to inspect the world, e.g., to print
the command that introduced a given name, to show all the commands back to a
certain one, undo the last command or more generally roll-back to an earlier
command. See history

**The Defthm Rule-Classes**

We've already discussed the key role that rules play in controlling the
behavior of the system. New rules are introduced primarily with the

To prove *formula* and generate, say a

(defthmnameformula:rule-classes (:rewrite :generalize))

If you wanted to rearrange the shape of the formula before generating the

(defthmnameformula:rule-classes ((:rewrite :corollary ...) :generalize)).

There are many classes of rules, affecting different parts of the system.
Each class is denoted by a keyword, e.g.,

We give some links below to other classes of rules. However, we recommend that you not follow these links upon your first reading of this tutorial!

See rewrite

See linear

(<= (len (delete e x)) (len x))

as a rewrite rule is that it only matches instances of that inequality and thus fails to match

(<= (LEN (DELETE E X)) (+ 1 (LEN X)))

ACL2 contains an extensible linear arithmetic decision procedure and by
storing inequalities as

See equivalence

(set-equal (rev x) x) (set-equal (append x y) (append y x))

You can make ACL2 use these two theorems as

(implies (set-equal a b) (iff (member e a) (member e b)))

gives the rewriter permission to use the above

See elim *destructor* functions
for *constructor* functions. In analogy with how ACL2 eliminates

See generalize

See induction

For a complete list of rule-classes, See rule-classes

If you are reading this as part of the tutorial introduction to the theorem
prover, use your browser's **Back Button** now to return to introduction-to-the-theorem-prover.