Major Section: INTRODUCTION-TO-THE-THEOREM-PROVER

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
`defun`

for defining new functions (and predicates) and `defthm`

for
proving new theorems. Both add rules to the database. Here are some
commonly used events.

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 to define a new function or predicate symbol. Definitional axioms
are just a kind of `rewrite`

rule, but `defun`

may also add rules
affecting the determination of the type of a term and rules affecting the
induction analysis. When you issue a `defun`

command you will always supply
the *name* of the function or predicate, the list of *formal parameters*, *v1,...vn*, and
the *body*:

(defunIf the event is accepted, aname(v1 ... vn)body)

`(`

`)`

=`defun`

event may require
theorems to be proved. Specifically, `defun`

event, coded as part of the `declaration`

that
Common Lisp allows:
(defunThename(v1 ... vn) (declare (xargs ...))body)

`xargs`

(``extra arguments to `defun`

'') entry may specify, among
other things, the measure to use in the termination proof, hints for use by
the prover during the termination proof, the guard of the new function, and
hints for use by the prover during the guard verification step.
See defthm to prove a theorem and to add it as a rule of one or more
specified rule-classes. When you issue a `defthm`

command you always
specify a *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 `defthm`

*rule classes* below.

See in-theory to enable or disable rules. Rules have names derived from the
names you give to functions and theorems, e.g., `(:REWRITE LEFT-IDENTITY-OF-FOO . 2)`

for the second rewrite rule you created from the
theorem named `LEFT-IDENTITY-OF-FOO`

. Rule names are called *runes*. A
*theory* is just a set (list) of runes. The *current theory* is the
list of enabled runes and the `in-theory`

event can add runes to or delete
runes from the current theory.

See include-book to change the world by loading a certified file of other events.
The most common use of `include-book`

is to load ``system'' books -- books written by
other ACL2 users who have released them for distribution to the community.
The most common books loaded are probably the arithmetic books:

; * for the most elementary arithmetic, needed for any problem ; that involves even simple addition and multiplication like ;But for a complete list of system books, see books .`(+ 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))`

, and`floor`

and`mod`

(include-book "arithmetic-5/top" :dir :system)

See certify-book to certify a file of events for reuse later.

See defconst to define a new constant, allowing you to write a
symbol, e.g., `*weekdays*`

in place of some object, e.g.,
`'(MON TUE WED THU FRI)`

in formulas.

See defmacro to define a new syntactic abbreviation. The macro facility in
Lisp is quite powerful, allowing you to *compute* the form to which some
type-in expands. For example, the primitive macro `COND`

is defined so
that `(COND ((P X) 1)((Q X) 2)(T 3))`

expands to
`(IF (P X) 1 (IF (Q X) 2 3))`

.

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

See events for a complete list of the ACL2 events. There are events to allow mutually recursive definitions, to introduce some new function symbols constrained to satisfy given axioms, to allow the temporary introduction of a ``local'' event to help prove some goal theorem and then disappear, to provide the power of first-order quantification and a choice operator, and many other features.

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 primiarily with the
`defthm`

event, though `defun`

and other events may introduce rules.

To prove *formula* and generate, say a `:rewrite`

rule and a `:generalize`

rule from it, you would write

(defthmIf you wanted to rearrange the shape of the formula before generating thenameformula:rule-classes (:rewrite :generalize))

`:rewrite`

rule
you could provide a `:corollary`

modifier to the `:rewrite`

rule class:
(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., `:REWRITE`

, `:LINEAR`

, etc.
You are responsible for specifying the class(es) of rules to be generated
from a given formula and several different rules (possibly of different
classes) may be derived from a single formula. Each class admits optional
modifiers that allow you finer control over each rule. Each class admits
the `:corollary`

modifier with which you can rearrange the formula before
a rule of that class is generated. This allows you to state a theorem in
its most elegant form for publication purposes but store it as a rule with
the most appropriate hypotheses and conclusion. Other modifiers tend to
be specific to certain rule classes, but for example, `:rewrite`

rule
modifiers include an optional limit on the depth of backchaining and
options for handling free variables.

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 for a description of how to create a rewrite rule.

See LINEAR for a description of how to store theorems concluding with arithmetic inequalities. The trouble with storing

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

`:linear`

rules you can make that decision procedure aware of
the basic inequalities between non-primitive numerically valued terms.
See EQUIVALENCE , see CONGRUENCE , and see REFINEMENT
to learn how to introduce a new equivalence relation to the
rewriter. For example, suppose you define `set-equal`

so that it returns
t precisely if its two arguments are lists containing the same elements,
regardless of order or number of occurrences. Note that under this sense of
``equivalence'', `(rev x)`

is the identity function and `append`

is
commutative, for example.

(set-equal (rev x) x)You can make ACL2 use these two theorems as(set-equal (append x y) (append y x))

`:rewrite`

rules to replace
instances of `(REV x)`

and `(APPEND x y)`

by `set-equal`

terms, even
though the results are not actually `EQUAL`

. This is possible provided the
target occurs in a context admitting `set-equal`

as a congruence relation.
For example, the `:congruence`

rule:
(implies (set-equal a b) (iff (member e a) (member e b)))gives the rewriter permission to use the above

`set-equal`

rules as
rewrite rules in the second argument of any `member`

expression being used
in a propositional way.
See ELIM for a description of how to make the system adopt a
``change of variable'' tactic that can trade in *destructor* functions for
*constructor* functions. In analogy with how ACL2 eliminates `(CAR X)`

and `(CDR X)`

by replacing `X`

with `(CONS A B)`

, you can make it
eliminate other destructors. For example, the system book
`"arithmetic-5/top"`

provides an `elim`

rule that eliminates `(floor x y)`

and `(mod x y)`

by replacing `x`

by `(+ r (* y q))`

, so that the
`floor`

expression becomes `q`

and the `mod`

expression becomes `r`

.
When introducing your own `elim`

rules you will probably also need to into
introduce `generalize`

rules (see below) so that the new variables are
appropriately constrained.

See GENERALIZE for a description of how you can make ACL2 restrict the new
variables it introduces when generalizing. ACL2 will sometimes replace a
term by a new variable and with `generalize`

rules you can insure that the
new variable symbol has certain properties of the term it replaces.

See INDUCTION for a description of how to tailor the inductions suggested by
a term. Most of the time when ACL2 chooses the ``wrong'' induction, the
easiest fix is with a local `:induct`

hint (see below). But if the same
problem arises repeatedly in several theorems, you might want to ``educate''
ACL2's induction heuristic.

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.