This is documentation for ACL2 Version 4.0
Copyright (C) 2010  University of Texas at Austin

This program is free software; you can redistribute it and/or modify
it under the terms of the GNU General Public License as published by
the Free Software Foundation; either version 2 of the License, or
(at your option) any later version.

This program is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
GNU General Public License for more details.

You should have received a copy of the GNU General Public License
along with this program; if not, write to the Free Software
Foundation, Inc., 675 Mass Ave, Cambridge, MA 02139, USA.

Written by:  Matt Kaufmann and J Strother Moore
Department of Computer Sciences
University of Texas at Austin
Austin, TX 78712-1188 U.S.A.

LOGIC-KNOWLEDGE-TAKEN-FOR-GRANTED    background knowledge in ACL2 logic for theorem prover tutorial

You might think that in order to use the theorem prover you have to know
the mathematical logic supported by ACL2.  But you need to know a lot
less about it than you might think.

Technically, a theorem is a formula that can be derived from axioms by
using rules of inference.  Thus, to do a proof you have to know (a) the
syntax of formulas, (b) the axioms, and (c) the rules of inference.
Traditionally, these things are spelled out in excruciating detail in
treatments of mathematical logic - and for good reason.

The whole point of proving theorems is that it is a way to determine
that a formula is "always true" (under some model of the axioms).  By
"always true" we actually mean what logicians mean when they say the
formula is valid: true in the model, for all possible values the
variables.  Here by "model of the axioms" we mean an understanding of
the meaning of the various function symbols so that the axioms are true
for all values of the variables.  If the variables in your conjecture
can take on an infinite number of values, proof is often the only way
to determine that a conjecture is "always true."  So if proof is being
used to determine that a questionable formula is always true the proof
must be carried out flawlessly.  Thus, the (a) syntax, (b) axioms, and
(c) rules of inference must be described precisely and followed to the
letter.

But formal mathematical logic was invented to explain how people
reason.  To the extent that logic mimics human reasoning, proofs can be
seen as just extremely carefully crafted arguments.  Given that ACL2 is
responsible for following the rules "to the letter," your main job is
"explain" the big leaps.

To use the theorem prover you must understand (a) the syntax, because
you must be able to write formulas flawlessly.  But you don't have to
know (b) the axioms and (c) the rules of inference at nearly the same
level of precision, as long as you understand the basic structure and
language of proofs.

Below is part of a proof of a certain theorem.  You ought to be able to
understand the following.  Since what we describe is a proof of one
case of the formula, we hope that you're convinced that the formula
holds for that case.

Read this and follow the links to confirm that you understand what
happens.  Be sure to then use your browser's Back Button to return to
this page and continue.

An Annotated Proof of

     (implies (true-listp z)
              (equal (rev (rev z)) z))

"We will prove that reversing the reverse of a true-listp yields the
original list.  The formula stating this is above.  We will prove it by
induction on the list structure of z.

The base case of the induction is:

     (implies (endp z)
              (implies (true-listp z)
                       (equal (rev (rev z)) z))).

This formula is equivalent, by propositional calculus, to

     (implies (and (endp z)
                   (true-listp z))
              (equal (rev (rev z)) z))

Rewriting with the definition of endp produces:

     (implies (and (not (consp z))
                   (true-listp z))
              (equal (rev (rev z)) z))

Rewriting repeatedly starting with the definition of true-listp
produces:

     (implies (and (not (consp z))
                   (equal z nil))
              (equal (rev (rev z)) z))

Then using the second hypothesis, just substituting equals for equals,
we get

     (implies (and (not (consp z))
                   (equal z nil))
              (equal (rev (rev nil)) nil))

Since the conclusion involves no variables, we can evaluate it, getting

     (implies (and (not (consp z))
                   (equal z nil))
              T)

But this is an instance of the tautology (implies p T).  Thus, the base
case is proved."

Now it is time for a little quiz.  There are just three questions.

Q1:  The case above was the Base Case of an inductive proof of

     (implies (true-listp z)
              (equal (rev (rev z)) z))

in which we did induction on the structure of the linear list z.  What
is the Induction Step?  That is, what do you have to prove besides the
Base Case to complete this inductive proof?

Below are four commonly given answers; choose one.  Then look here to
find out if you're right.

     Induction Step - Choice (i):
     (implies (not (endp z))
              (implies (true-listp z)
                       (equal (rev (rev z)) z)))

     Induction Step - Choice (ii):
     (implies (true-listp (cdr z))
              (equal (rev (rev (cdr z))) (cdr z)))

     Induction Step - Choice (iii):
     (implies (and (not (endp z))
                   (equal (rev (rev (cdr x))) (cdr x)))
              (implies (true-listp z)
                       (equal (rev (rev z)) z)))

     Induction Step - Choice (iv):
     (implies (and (not (endp z))
                   (implies (true-listp (cdr z))
                            (equal (rev (rev (cdr z))) (cdr z))))
              (implies (true-listp z)
                       (equal (rev (rev z)) z)))

Q2: To prove the Induction Step we must prove one or more of the goals
below.

Which combinations are sufficient to imply the Induction Step?  Decide
what is required and then look here to find out if you're right.  To
help you, the Induction Step is of the form:

     Induction Step:
     (implies (and c
                   (implies p' q'))
              (implies p q))

and beside each candidate subgoal we show its structure in those terms.

     Subgoal (i):
     (implies (and (not (endp z))                        ; (implies (and c
                   (true-listp z))                       ;               p)
              (true-listp (cdr z)))                      ;          p')

     Subgoal (ii):
     (implies (and (not (endp z))                        ; (implies (and c
                   (true-listp z)                        ;               p
                   (equal (rev (rev (cdr z))) (cdr z)))  ;               q')
              (equal (rev (rev z)) z))                   ;          q)

     Subgoal (iii):
     (implies (and (not (endp z))                        ; (implies (and c
                   (equal (rev (rev (cdr z))) (cdr z)))  ;               q')
              (equal (rev (rev z)) z))                   ;          q)

     Subgoal (iv):
     (implies (and (not (endp z))                        ; (implies (and c
                   (true-listp (cdr z))                  ;               p'
                   (equal (rev (rev (cdr z))) (cdr z)))  ;               q')
              (equal (rev (rev z)) z))                   ;          q)

Q3: Suppose you know the theorem

     Theorem:
     (implies (p (f x))
              (equal (g (h x))
                     x))

and you wish to rewrite the target (g (h a)) to a in

     Goal Conjecture:
     (implies (and (q (f a))
                   (r a))
              (s (g (h a))))

What must you prove to relieve the hypothesis of Theorem?

After you've thought about it, look here for our answer.

End of the Quiz

If this page made sense, you're ready to read the introduction to the
theorem prover.

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.

LOGIC-KNOWLEDGE-TAKEN-FOR-GRANTED-BASE-CASE    a brief explanation of base cases

According to the sentence, the conjecture being proved is "reversing
the reverse of a true-listp yields the original list."  The formula
corresponding to this conjecture is:

     (implies (true-listp z)
              (equal (rev (rev z)) z)).

We're also told that this is an inductive proof.  Evidently we're doing
an induction on the structure of the list z.  Then the Base Case is the
formula:

     (implies (endp z)
              (implies (true-listp z)
                       (equal (rev (rev z)) z))).

Now use your browser's Back Button to return to the example proof in
logic-knowledge-taken-for-granted.

LOGIC-KNOWLEDGE-TAKEN-FOR-GRANTED-EQUALS-FOR-EQUALS    substitution of equals for equals

Anytime you have an equality hypothesis relating two terms, e.g.,

     (equal lhs rhs)

it is legal to substitute one for the other anyplace else in the
formula.  Doing so does not change the truthvalue of the formula.

You can use a negated equality this way provided it appears in the
conclusion.  For example, it is ok to transform

     (implies (true-listp x)
              (not (equal x 23)))

to

     (implies (true-listp 23)
              (not (equal x 23)))

by substitutions of equals for equals.  That is because, by
propositional calculus, we could rearrange the formulas into their
contrapositive forms:

     (implies (equal x 23)
              (not (true-listp x)))

and

     (implies (equal x 23)
              (not (true-listp 23)))

and see the equality as a hypothesis and the substitution of 23 for x as
sensible.

Sometimes people speak loosely and say "substitution of equals for
equals" when they really mean "substitutions of equivalents for
equivalents."  Equality, as tested by EQUAL, is only one example of an
equivalence relation.  The next most common is propositional
equivalence, as tested by IFF.  You can use propositional equivalence
hypotheses to substitute one side for the other provided the target
term occurs in a propositional place, as discussed at the bottom of
propositional calculus.

Now use your browser's Back Button to return to the example proof in
logic-knowledge-taken-for-granted.

LOGIC-KNOWLEDGE-TAKEN-FOR-GRANTED-EVALUATION    evaluation during proofs

Any time you are proving a formula and see a subterm in the formula
that contains no variables, you can just evaluate the subterm.

This is familiar from algebra:  It is not uncommon to rearrange a
polynominal to collect all the constants and then add them up:

     (3x + 2 + 7y + 2)
     =
     (3x + 7y + (2 + 2))
     =
     (3x + 7y + 4).

That last step is just evaluation.

It happens often in ACL2 proofs because theorems involve constants and
defined functions and when those constants "drift into the maw" of a
function, the function call can be eliminated and replaced by a new
constant.  ACL2 does this automatically; you don't have to tell it.  In
fact, there are a few occasions where you might prefer it not evaluate
and those are the ones you have to look out for!  They'll be obvious
when they happen because you'll see a mysterious constant crop up in
the proof.

Evaluation is legal because it is just the repeated use of
unconditional rewriting to replace definitions by their instantiated
bodies until no function calls remain.

Now use your browser's Back Button to return to the example proof in
logic-knowledge-taken-for-granted.

LOGIC-KNOWLEDGE-TAKEN-FOR-GRANTED-INDUCTIVE-PROOF    a brief explanation of induction

We start by showing classical induction on the natural numbers in an
ACL2 setting before turning to a more general treatment of induction.

Classical Induction on Natural Numbers: Induction is familiar in the
arithmetic setting.  Let (p n) denote some formula involving the
variable n (and perhaps some other variables which we don't exhibit).
Then to prove (p n), for all n, by classical induction on the
construction of the natural numbers, prove each of the following:

     Base Case:
     (implies (zp n) (p n))

     Induction Step:
     (implies (and (not (zp n))
                   (p (- n 1)))
              (p n))

The Base Case establishes that p holds for 0.  In fact, because of the
definition of zp <>, it establishes that (p n) holds when n is 0 and it
holds when n is not a natural number.

The Induction Step establishes that if n is a natural number other than
0, and if p holds for n-1, then p holds for n.  The hypothesis (p (- n
1)) above is called the induction hypothesis.

Note that if the Base Case and Induction Step are valid, then we know
(p n), for all n.  You can convince yourself of this by picking any
object and asking "how do I know p holds for this object?"  For example,
(p -7), (p 'abc), and (p 0) are all established by the Base Case.  What
about (p 1)?  That follows from (p 0), given the Induction Step.  Why?
To prove (p 1) using the Induction Step, you have to establish (not (zp
1)), which is true, and (p (- 1 1)), which is (p 0), which is true by
the Base Case.  So (p 1) is true.  Similar reasoning proves (p 2) from
from (p 1), etc.  Clearly, for every natural number other than 0 we
could reason like this to show that p holds.  Since the Base Case
handled all the objects that are not natural numbers, and handled 0, we
know (p n), for all n.

There is a duality between recursion and induction that ACL2 exploits.
The fact that the Base and Induction steps above are sufficient to
prove p for all objects is related to the fact that the following
recursion defines a total, terminating function:

     (defun nat-recursion (n)
       (if (zp n)
           n
           (nat-recursion (- n 1))))

When this function is admitted we have to prove that if (zp n) does not
hold, then (- n 1) is smaller, in some sense, than n.  This sense of
"smaller" is determined by some measure of the arguments.  That measure
must return an ordinal (ordinals <>), but the most common measures
return natural numbers, which are among the ordinals.  Furthermore,
that measure should insure that the terms in the recursive calls are
smaller than the formals, i.e., the measure of (- n 1) must be smaller
than the measure of n, when the recursive branches are taken.  This
sense of "smaller" must be well-founded:  it must be impossible to have
an infinitely descending chain of smaller things.  This is true of the
less-than relation on the ordinals (see o< <>).  Well-foundedness means
that eventually any recursion must "bottom out" because things can't
keep getting smaller forever.

The recursion in nat-recursion suggests the induction shown above: the
Base Case is defined by the if branch that does not lead to a recursive
call.  The Induction Step is defined by the other branch.  The
induction hypothesis is defined by what we recur on, i.e., (- n 1).  The
theorems proved when nat-recursion is introduced justify the classical
induction scheme noted above.

Every recursively defined ACL2 function suggests a legal induction and
vice versa.

Furthermore, every call of a recursively defined function on distinct
variable symbols also suggests a legal induction:  just take the
induction suggested by the function's recursive definition after
renaming the formal parameters to be the variables in the call.

For example, it should be clear that (nat-recursion a) suggests a Base
Case defined by (zp a), and induction step defined by (not (zp a)) and
an induction hypothesis about (- a 1).

Note that the term (fact n) suggests the same classical induction on
natural numbers shown above, where fact is defined as follows (even
though we've used the formal parameter k below).

     (defun fact (k)
       (if (zp k)
           1
           (* k (fact (- k 1)))))

The induction suggested by a term like (fact n) is insensitive to the
name of the formal parameter used in the defun.

The induction suggested by a function or term is insensitive to the
value returned by the function or term.

It doesn't matter what the function returns in its "base case" (e.g., 1
in fact) or what the function "does" to its recursive call (e.g.,
multiply by k in the defun of fact).

All that matters is (i) how the if structure breaks down the cases on
k, (ii) which branches lead to recursion, and (iii) what arguments are
passed to the recursive calls.  Those things determine (i) the case
analysis of the induction scheme, (ii) which cases are Base Cases and
which are Induction Steps, and (iii) what the induction hypotheses are.

For a selection of common inductions schemes in ACL2 (e.g., on the
structure of natural numbers, lists, and trees and on several variables
at once, multiple base cases, multiple induction hypotheses, multiple
induction steps, etc.)  check this link.

Every legal ACL2 induction corresponds to an admissible recursive
function and vice versa.  Similarly, every legal ACL2 induction
corresponds to a call of a recursively defined function on distinct
variables.

ACL2 chooses which induction to do by looking at the terms that occur
in the conjecture.  For many elementary theorems, ACL2 chooses the
right induction by itself.

You may occasionally need to tell it what induction to do.  You do that
by showing it a term that suggests the induction you want.  We'll
explain how you communicate this to ACL2 later.  If you understand how
recursive functions suggest inductions, then you know what you need to
know to use ACL2.

The main point of this discussion of induction is familiarize you with
the basic terms:  Base Case (of which there may be several), Induction
Step (of which there may be several), Induction Hypothesis (of which
there may be several in each Induction Step), measure and well-founded
relation justifying an induction, and the induction suggested by a term
or recursive function definition.  Furthermore, every Induction
Hypothesis is always an instance of the conjecture being proved: each
induction hypothesis is obtained from the conjecture being proved by
applying a substitution replacing variables by terms.

If you are reviewing the material taken for granted about logic while
working your way through the introduction to the theorem prover, please
use your browser's Back Button to return to the example proof in
logic-knowledge-taken-for-granted.

LOGIC-KNOWLEDGE-TAKEN-FOR-GRANTED-INSTANCE    a brief explanation of substitution instances

Let p and q be terms or formulas (there is no difference in ACL2).
Then we say p is an instance or substitution instance of q if and only
if p can be obtained from q by uniformly replacing the variables of q
by terms.  Sometimes we call p the target and q the pattern because by
choosing appropriate replacements we can make the pattern match many
different targets.

For example, the following target is an instance of the given pattern:

     target:      (APP (APP (REV A) (REV B)) (REV C))
     pattern:     (APP (APP   x       y    ) (REV z))

The replacement or substitution used in this match of the pattern to the
target is:

     variable in pattern          replacement term
     x                              (REV A)
     y                              (REV B)
     z                              C

Such substitutions are usually written this way in ACL2:

     ((x  (REV A))
      (y  (REV B))
      (z  C)).

Please use your browser's Back Button to return to the page that
mentioned "instance."

LOGIC-KNOWLEDGE-TAKEN-FOR-GRANTED-PROPOSITIONAL-CALCULUS    a brief explanation of propositional calculus

It is impossible in this short introduction to teach you propositional
calculus if you don't already know it!

A typical use of propositional calculus is to observe that

     (implies (endp z)
              (implies (true-listp z)
                       (equal (rev (rev z)) z)))

is equivalent to:

      (implies (and (endp z)
                    (true-listp z))
               (equal (rev (rev z)) z))

If this is surprising and you know propositional calculus, then the
problem might be our notation.  We're exploiting the tautology

     (p --> (q --> r)) <--> ((p & q) --> r)

where --> and <--> are meant to be the traditional arrows denoting
logical implication and logical equivalence.

If you don't know propositional calculus, we'll say just a few things
to help ease your journey.

A propositional formula, in ACL2, is any formula written entirely in
terms of variable symbols, T, NIL, and the propositional functions AND,
OR, NOT, IMPLIES, and IFF.  The "tautology" above in traditional
notation is this propositional formula in ACL2:

     (IFF (IMPLIES P (IMPLIES Q R))
          (IMPLIES (AND P Q) R)).

If you have a formula like

     (implies hyp
              concl)

then we say that formula is an implication, that hyp is the hypothesis,
and that concl is the conclusion.  If the hypothesis is an and
expression, as in

     (implies (and hyp1
                   hyp2
                   ...)
              concl)

then we call hyp1 is the first hypothesis, hyp2 is the second
hypothesis, etc.

If a term is of the form

     (and term1 term2 ...)

we say it is a conjunction and that term1 is the first conjunct, term2
is the second conjunct, etc.  We treat an or-term analogously but call
it a disjunction and its arguments are disjuncts.

A tautology is any propositional formula that can be proved by testing
it under all combinations of Boolean assignments to its variables.  We
give an example of such a truth-table proof below, but hasten to add
that ACL2 does not generally use truth tables to recognize tautologies.
It primarily uses IF-normalization and BDDs to recognize tautologies,
which can be seen as a mix of symbolic manipulation and case analysis.

Many tautologies have names, but ACL2 doesn't refer to them by name
because it derives them from first principles.  We list a few here
because we sometimes use the names in our documentation; more
importantly, you should look at these formulas and convince yourself
that they're always true for all Boolean values of the variables:

     Double Negation:
     (iff (not (not p)) p)

     DeMorgan:
     (iff (not (and p q))
          (or (not p) (not q)))

     Distributivity:
     (iff (and p (or q r))
          (or (and p q)
              (and p r)))

     Promotion:
     (iff (implies p (implies q r))
          (implies (and p q) r))

     Implicative Disjunction:
     (iff (implies p q)
          (or (not p) q))

     Contrapositive:
     (iff (implies p q)
          (implies (not q) (not p)))

     Generalized Contrapositive:
     (iff (implies (and p r) q)
          (implies (and p (not q)) (not r)))

There are, of course, many others, even with these same names!  For
example, there is a dual version of DeMorgan showing how not
distributes over or, a dual version of Distributivity for or over and,
etc.

Dealing with propositional calculus will not generally be a problem for
you because it is decidable and ACL2 has procedures that decide
propositional formulas.  However, propositional calculus can lead to
exponential explosion and can thus explain why ACL2 has "gone out to
lunch."  In addition, sometimes if you are curious as to why ACL2 is
working on a certain subgoal the reason can be traced back to
propositional calculus.

The most common example of this is that to prove a formula of the form

     (implies (implies p1 q1)
              (implies p2 q2))

propositional calculus will convert it to

     (and (implies (and p2 (not p1)) q2)
          (implies (and p2 q1) q2))

Many users are surprised that the first conjunct above does not have q1
as a hypothesis.  If you ever stare at an ACL2 goal and say to yourself
"A hypothesis is missing!" the chances are that propositional calculus
is "to blame."  In particular, if you are trying to prove that (implies
p1 q1) implies something, you must deal with the case that (implies p1
q1) is true because p1 is false.  Think about it.

Now we illustrate the truth table method for deciding tautologies, even
though that is not what ACL2 generally uses.  Consider the formula
called Promotion above:

     (IFF (IMPLIES P (IMPLIES Q R))
          (IMPLIES (AND P Q) R))

The formula above is a tautology.  It contains three variables, P, Q,
and R, and so there are 8 combinations of Boolean assignments to them.
If we let

     formula1:  (IMPLIES P (IMPLIES Q R))
     formula2:  (IMPLIES (AND P Q) R)

then we wish to test the formula (IFF formula1 formula2):

     P   Q   R       formula1   formula2   (IFF formula1 formula2)
     ---------
     T   T   T            T         T       T
     T   T   NIL          NIL       NIL     T
     T   NIL T            T         T       T
     T   NIL NIL          T         T       T
     NIL T   T            T         T       T
     NIL T   NIL          T         T       T
     NIL NIL T            T         T       T
     NIL NIL NIL          T         T       T

So we see that the formula always returns T and is thus a tautology.

Recall that in the original example at the top of this page we were
trying to prove the formula

     (implies (endp z)
              (implies (true-listp z)
                       (equal (rev (rev z)) z)))

This formula is an instance of

     (implies p (implies q r)).

The substitution required by the match is

     sigma:
     ((p    (endp z))
      (q    (true-listp z))
      (r    (equal (rev (rev z)) z)))

Since we know the tautology:

     (iff (implies p (implies q r))
          (implies (and p q) r)).

is always true no matter what Boolean values p, q, and r have, then we
know this instance of it (obtained by applying the substitution sigma
above) is always true:

     (iff (implies (endp z)                            formula1'
                   (implies (true-listp z)
                            (equal (rev (rev z)) z)))
          (implies (and (endp z)                       formula2'
                        (true-listp z))
                   (equal (rev (rev z)) z))).

Thus, if we're trying to prove formula1' it is permitted to try to to
prove formula2' instead, because they return the same truthvalue.

This sketch of propositional reasoning in ACL2 is a little suspect
because we didn't address the possibility that the substitution might
replace the propositional variables by non-propositional terms.  But
the tautology was verified only on Boolean values for those variables.
This actually works out because in ACL2 all propositional testing is
done against nil and any non-nil value, including t, is as good as
another.  However, the tautology allows us to replace one formula by
the other only in contexts in which we just care about propositional
truth, i.e., whether the formula is nil or not.  When we prove a
formula in ACL2 we are really establishing that it never returns nil,
i.e., no matter what the values of the variables, the value of the
formula is non-nil.

A very simple example of this is with Double Negation.

     (iff (not (not p)) p)

is a tautology.  This means that if we were trying to prove

     (implies (not (not p)) ...)

we could transform it to

     (implies p ...).

But if we were trying to prove:

     (equal (not (not p)) p)

we could not prove it by using Double Negation!  The formula above
claims that (not (not p)) and p have identical values.  They do not!
For example, (not (not 3)) is t, not 3.  However, (not (not 3)) and t
are propositionally equivalent (i.e., satisfy iff) because one is as
good as the other in a test.  That is what Double Negation says.

As long as you only use propositional formulas in propositional places
this aspect of ACL2 should not affect you.

Now please use your browser's Back Button to return to the example
proof in logic-knowledge-taken-for-granted.

LOGIC-KNOWLEDGE-TAKEN-FOR-GRANTED-Q1-ANSWER    the inductive step of the rev-rev proof - Answer to Question 1

The correct answer to Question 1 in logic-knowledge-taken-for-granted
is Choice (iv).

The Induction Step of the inductive proof of

     (implies (true-listp z)
              (equal (rev (rev z)) z))

for an induction on the linear list z is:

     Induction Step:
     (implies (and (not (endp z))
                   (implies (true-listp (cdr z))
                            (equal (rev (rev (cdr z))) (cdr z))))
              (implies (true-listp z)
                       (equal (rev (rev z)) z)))

The second hypothesis above is the the induction hypothesis.  The
conclusion above is the formula we are trying to prove.  Each induction
hypothesis is always an instance of the formula being proved, i.e., it
is obtained from the formula being proved by uniformly replacing the
variables in the formula with terms.  Notice how the induction
hypothesis above is the same as the induction conclusion, except that
all the zs have been replaced by (cdr z).

If you thought the right answer was

     Induction Step - Choice (i):
     (implies (not (endp z))
              (implies (true-listp z)
                       (equal (rev (rev z)) z)))

then perhaps you didn't understand that we're doing an inductive proof.
Certainly if you prove the Base Case already discussed and you prove
Choice (i) above, then you will have proved the goal conjecture, but you
would have done it by simple case analysis:  prove it when (endp z) and
prove it when (not (endp z)).  While logically valid, you probably can't
prove Choice (i) directly because you have no induction hypothesis to
work with.

If you thought the right answer was:

     Induction Step - Choice (ii):
     (implies (true-listp (cdr z))
              (equal (rev (rev (cdr z))) (cdr z)))

then perhaps you misunderstand the difference between the Induction Step
and the Induction Hypothesis.  The Induction Step is the "other half"
of the main proof, balancing the Base Case.  The Induction Hypothesis is
just a hypothesis you get to use during the Induction Step.  The
question Q1 asked what is the Induction Step.

If you thought the right answer was:

     Induction Step - Choice (iii):
     (implies (and (not (endp z))
                   (equal (rev (rev (cdr x))) (cdr x))) ; "induction hyp"
              (implies (true-listp z)
                       (equal (rev (rev z)) z)))

then you are making the most common mistake newcomers make to
induction.  You are giving yourself an "induction hypothesis" that is
not an instance of the conjecture you're proving.  This alleged
induction hypothesis says that (rev (rev (cdr x))) is (cdr x), whereas
the correct induction hypothesis says those two terms are equal if
(true-listp (cdr x)).  This alleged induction hypothesis is a stronger
claim than we're trying to prove.  It turns out that by making this
mistake you can "prove" conjectures that are not always true!
Remember:  the induction hypothesis is always an instance of the
conjecture you're proving, not just some piece of it.  Of course, ACL2
"knows" this and will never make this mistake.  But we remind you of it
because there may be times when you intuit a different hypothesis and
don't understand why ACL2 doesn't use it.

If this doesn't make sense, perhaps you should read about induction
again.

When you understand why Choice (iv) is the correct answer, use your
browser's Back Button to return to logic-knowledge-taken-for-granted
and go to question Q2.

LOGIC-KNOWLEDGE-TAKEN-FOR-GRANTED-Q2-ANSWER    the inductive step of the rev-rev proof - Answer to Question 2

The correct answer to Question 2 in logic-knowledge-taken-for-granted
is Subgoal (i) plus any one of the other other three.  For your
reference, the four choices were:

     Subgoal (i):
     (implies (and (not (endp z))
                   (true-listp z))
              (true-listp (cdr z)))

     Subgoal (ii):
     (implies (and (not (endp z))
                   (true-listp z)
                   (equal (rev (rev (cdr z))) (cdr z)))
              (equal (rev (rev z)) z))

     Subgoal (iii):
     (implies (and (not (endp z))
                   (equal (rev (rev (cdr z))) (cdr z)))
              (equal (rev (rev z)) z))

     Subgoal (iv):
     (implies (and (not (endp z))
                   (true-listp (cdr z))
                   (equal (rev (rev (cdr z))) (cdr z)))
              (equal (rev (rev z)) z))

In particular, it is wrong to think the Induction Step of the proof of

     (implies (true-listp z)
              (equal (rev (rev z)) z))

can be established by proving just Subgoal (ii), Subgoal (iii), Subgoal
(iv), or combinations of those three.  You must also prove Subgoal (i)
or something like it!

The Inductive Step for the conjecture above is

     Induction Step:
     (implies (and (not (endp z))
                   ; Induction Hypothesis:
                   (implies (true-listp (cdr z))
                            (equal (rev (rev (cdr z))) (cdr z))))
              ; Induction Conclusion:
              (implies (true-listp z)
                       (equal (rev (rev z)) z)))

Note that the Inductive Hypothesis is an implication:

     (implies (true-listp (cdr z))
              (equal (rev (rev (cdr z))) (cdr z)))

This hypothesis can be true two different ways.  The "normal" way - the
way everybody remembers - is that (true-listp (cdr z)) is true and thus
(equal (rev (rev (cdr z))) (cdr z)) is true.  But the way many people
forget is that (true-listp (cdr z)) is false.  You must prove the
Induction Step even in this "forgetable" case.

In this case, the Induction Step simplifies to

     Induction Step:
     (implies (and (not (endp z))
                   (not (true-listp (cdr z))))
              (implies (true-listp z)
                       (equal (rev (rev z)) z)))

By Promotion (see the list of tautologies in our discussion of
propositional calculus) this is

     Induction Step':
     (implies (and (not (endp z))
                   (not (true-listp (cdr z)))
                   (true-listp z))
              (equal (rev (rev z)) z))

Using the Contrapositive and rearranging the order of the hypotheses
(see propositional calculus again), this is

     Induction Step":
     (implies (and (not (endp z))
                   (true-listp z)
                   (not (equal (rev (rev z)) z)))
              (true-listp (cdr z)))

Notice that Subgoal (i) implies Induction Step":

     Subgoal (i):
     (implies (and (not (endp z))
                   (truelistp z))
              (truelistp (cdr z)))

Every inductive proof of an implication raises a case like this.  If we
denote the conjecture (implies p q) as p --> q, then the Induction Step
will look like this:

       ( c  &  (p'  --->  q'))
     --->
       (p ---> q)

where c is the test that determines the inductive step, (e.g., (not
(endp z))) and p' and q' are inductive instances of p and q.  Promotion
produces

       ( c  & p & (p'  --->  q'))
     --->
       q

It is then very common to prove that p implies p',

     (i):
     (c & p) ---> p'

and then prove that q' implies q,

     (ii):
     (c & p & q') ---> q

These correspond exactly to our choices Subgoal (i) and Subgoal (ii).

It is sometimes helpful to remember this diagram:

     (c  &  (p'  --->  q')
             ^         |
             |         |
             |         v
      -->   (p   --->  q )

When you understand why Subgoals (i) and (ii) are sufficient, use your
browser's Back Button to return to logic-knowledge-taken-for-granted
and go to question Q3.

LOGIC-KNOWLEDGE-TAKEN-FOR-GRANTED-Q3-ANSWER    the inductive step of the rev-rev proof - Answer to Question 2

The correct answer to Question 3 in logic-knowledge-taken-for-granted
is that you need to prove

     Subgoal to Relieve Hyp 1:
     (implies (and (q (f a))
                   (r a))
              (p (f a)))

in order to use

     Theorem:
     (implies (p (f x))
              (equal (g (h x))
                     x))

to rewrite the target (g (h a)) to a in

     Goal Conjecture:
     (implies (and (q (f a))
                   (r a))
              (s (g (h a))))

If you don't see why, re-read the discussion of rewriting again.
Forgetting about the need to relieve hypotheses is a common mistake in
informal proofs.  ACL2 won't forget to relieve them.  But if you forget
about the need to do it, you may be confused when ACL2 doesn't see the
"proof" you see!

Now use your browser's Back Button to return to the end of quiz in
logic-knowledge-taken-for-granted.

LOGIC-KNOWLEDGE-TAKEN-FOR-GRANTED-REWRITING    a brief explanation of rewriting from the logical perspective

First we give two examples of rewriting.  Then we give a rather detailed
description.  We recommend you read the description, even if you
understand the two examples, just so that you learn our terminology.

Example 1:  Suppose your goal conjecture is:

     Goal Conjecture:
     (implies (and (endp z)
                   (true-listp z))
              (equal (rev (rev z)) z))

Then you can use the following theorem (actually the definitional axiom
introduced by the defun of endp):

     Definitional Axiom: endp
     (equal (endp x)
            (not (consp x))).

to rewrite the Goal Conjecture to

     Rewritten Goal Conjecture:
     (implies (and (not (consp z))
                   (true-listp z))
              (equal (rev (rev z)) z))

Note that in this example, rewriting replaced the call of endp by its
body after instantiating its body with the actuals from the call.  This
is sometimes just called expanding the definition of endp.  (The
notions of formal, body, call, and actuals are discussed in
programming-knowledge-taken-for-granted.)

Expanding a definition is an example of unconditional rewriting.  All
definitions in ACL2 are just bare equalities relating a call of the
function on its formals to its body.  Any time you use an equality
theorem, whether a definitional equality or something more general like

     (equal (append (append x y) z)
            (append x (append y z)))

to replace an instance of one side by the corresponding instance of the
other in a goal conjecture, we call that unconditional rewriting with
the equality.

Example 2:  Suppose your goal conjecture is:

     Goal Conjecture:
     (implies (and (subsetp a b)
                   (true-listp b)
                   (member e a))
              (< (len (rm e b)) (len b))).

This conjecture may be read "if a is a subset of the true-listp b and e
is a member of a, then the result of removing e from b has a shorter
length than b."

You can use the following theorem:

     Theorem:
     (implies (member u v)
              (equal (len (rm u v))
                     (- (len v) 1)))

to rewrite the Goal Conjecture to

     Rewritten Goal Conjecture:
     (implies (and (subsetp a b)
                   (true-listp b)
                   (member e a))
              (< (- (len b) 1) (len b))).

To do this you must know that the following subgoal is provable:

     Subgoal to Relieve Hyp 1:
     (implies (and (subsetp a b)
                   (true-listp b)
                   (member e a))
              (member e b)).

This is an example of conditional rewriting.  In order to use the
Theorem we had to establish that its hypotheses are satisfied.  That is
called relieving the hypotheses and was done by proving the Subgoal to
Relieve Hyp 1.  Conditional rewriting is the most commonly used proof
technique in ACL2.

Unconditional rewriting is just a special case, where there are no
hypotheses to relieve.

Expanding a definition is just another special case, where there are no
hypotheses to relieve and the pattern is easy to match because it is a
call of a function on distinct variables.

This page discusses rewriting from the logical perspective.  It is
important that you are familiar with the notions of a pattern term being
an instance of a target term.  We often say the pattern matches the
target.  These notions involve a corresponding substitution of terms
for variables.  All these notions are discussed in the link for
"instance" above and we recommend you read it before continuing.  Then
use your browser's Back Button to come back here.

You should also be aware of the terms introduced in our discussion of
propositional calculus.

Rewriting is a fundamental rule of inference in our system.  The rule
allows you to use a theorem, i.e., an axiom, lemma, or definition, to
replace one term by another in the goal conjecture you're trying to
prove.

Suppose you have a theorem that is of the form (or can be put into the
form):

     Theorem:
     (implies (and hyp1
                   ...
                   hypk)
              (equal pattern
                     replacement))

From the logical perspective we don't care how the theorem was actually
written when it was proved.  It might have no hypotheses (in which case
the hypi could just be t), or it could have been written in a different
but equivalent propositional style, (or (not hyp1) ...), or the
equality could have been written the other way around, (equal
replacement pattern).  Such syntactic details don't matter.  Just take
a theorem and use propositional calculus to rearrange it equivalently
into this form for the purposes of this one rewrite step.

Suppose pattern is an instance of some target term, target that occurs
in your goal conjecture.  Let the corresponding substitution be sigma.
If sigma does not contain a binding for every variable that occurs in
Theorem, then extend sigma to sigma' by adding one binding for each
such variable.  (This is necessary only if pattern does not contain
every variable in Theorem.)

Let replacement' be the result of instantiating replacement with sigma'.
Let hypi' be the result of instantiating hypi with sigma'.

Then the Rewrite Rule of Inference tells us it is permitted to replace
that occurrence of target in the goal by replacement' - if you can prove
each hypi' in this context.  We make this last condition clear in a
moment.

The justification for this is that Theorem is true for all values of the
variables.  Hence, it is true for the values specified by sigma'.  If
the hypi' are true, then the target is really equal to replacement'.
But it is always permitted to replace something by something it's equal
to.

Rewriting thus involves several steps:

(1) Finding a target and a theorem to use to rewrite it to some more
desirable replacement.

(2) Instantiating pattern in the (rearranged) theorem to match target.

(3) Extending sigma to sigma' to bind all the variables in Theorem.

(4) Establishing that the sigma' instances of each of the hypi hold.
This is called relieving the hypotheses of the theorem and is discussed
in greater detail below.

(5) Replacing the occurrence of target in the goal conjecture by the
sigma' instance of replacement, provided all the hypotheses are
relieved.

Step (4) above, relieving the hypotheses, requires first identifying the
"context" of the target in the goal conjecture.  To do this, use
propositional calculus to rearrange the goal conjecture so the
occurrence of target is in the conclusion and let context be the
hypothesis.

     Rearranged Conjecture:
     (implies context
              (... target ...))

To relieve the hypotheses you must then prove each of the following
subgoals:

     Subgoal to Relieve Hyp i:
     (implies context hypi').

It is important to note that this description of rewriting with Theorem
describes the process from a strictly logical perspective.  The syntax
of the theorem and the goal don't matter.  You're free to use
propositional calculus to rearrange them to put them into the
appropriate forms to fit the descriptions given.  Clearly, if you have
a candidate Theorem in the "wrong" form and but it can be rearranged
with propositional calculus into the "right" form, then that rearranged
theorem is also a Theorem and can be used as described.  But in the
actual implementation of ACL2, the syntactic form of a proved Theorem
affects how it is used by rewriting.  If a proved theorem takes the
form of an implication concluding with an equality, ACL2 treats the
left-hand side of the equality as pattern and the right-hand side as
replacement, unless you tell it otherwise.  We'll discuss this later.

Furthermore, being from the logical perspective this discussion of
rewriting does not address (a) how you extend simga to sigma' - any
extension will do provided it allows you to relieve the hypotheses.
The ACL2 theorem prover uses certain heuristics which we'll discuss
later, including methods by which you can guide the system in the
selection.

Crucially, it does not discuss whether it is a good idea to do a
particular rewrite!  For example, the definitional equality:

     (equal (len x)
            (if (endp x)
                0
                (+ 1 (len (cdr x)))))

may be used repeatedly, endlessly, to replace (len a) by an ever
growing sequence of terms:

     (len a)
     =
     (if (endp a)
         0
         (+ 1 (len (cdr a))))
     =
     (if (endp a)
         0
         (+ 1 (if (endp (cdr a))
                  0
                  (+ 1 (len (cdr (cdr a)))))))
     = ...

The ACL2 implmentation of rewriting uses certain heuristics and the you
can guide the system in its choices.  We'll discuss this later.

Now use your browser's Back Button to return to the example proof in
logic-knowledge-taken-for-granted.

LOGIC-KNOWLEDGE-TAKEN-FOR-GRANTED-REWRITING-REPEATEDLY    further information on expanding definitions via rewriting

We assume you've read about "instances" and picked up our basic
terminology including the ideas of matching a pattern term to a target
term, obtaining a substitution and how to instantiate a term with a
substitution.  We use these notions below without further citation.

In addition, we assume you've read about "rewriting" where we
introduced the idea of treating a theorem (axiom, definition, or lemma)
as a conditional rewrite rule and replaced one term by an equivalent one
provided we can relieve the hypotheses.

Suppose you're trying to prove formula1 and you transform it to
formula2 by rewriting.  What happened?

     formula1:
     (implies (and (not (consp z))
                   (true-listp z))
              (equal (rev (rev z)) z))

     formula2:
     (implies (and (not (consp z))
                   (equal z nil))
              (equal (rev (rev z)) z))

Evidently we replaced (true-listp z) by (equal z nil).  But how did
that happen?  What really happened was the sequential application of
several unconditional rewrites and the use of replacement of equals by
equals.

The definition of true-listp is:

     (defun true-listp (x)
       (if (consp x)
           (true-listp (cdr x))
           (equal x nil))).

By rewriting once with the definition of true-listp, we transform
formula1 to:

     formula1':
     (implies (and (not (consp z))
                   (if (consp z)
                       (true-listp (cdr z))
                       (equal z nil)))
              (equal (rev (rev z)) z)).

Note how the call of true-listp has been replaced by the entire body of
true-listp.

Next, note that the first hypothesis above is that (consp z) is false.
That is, (not (consp z)) is the same as (equal (consp z) nil).  Thus,
replacement of equals by equals means we can transform formula1' to

     formula1":
     (implies (and (not (consp z))
                   (if nil
                       (true-listp (cdr z))
                       (equal z nil)))
              (equal (rev (rev z)) z)).

(We will explore replacement of equals by equals later.)

Furthermore, we know the basic axiom about if:

     Axiom if-nil:
     (if nil x y) = y.

Rewriting with this particular axiom, using (if nil x y) as the pattern
and y as the replacement, will transform formula1" to

     formula2:
     (implies (and (not (consp z))
                   (equal z nil))
              (equal (rev (rev z)) z)).

Often when we say we derived one formula from another by "expansion"
and or by "rewriting" we take many rewrite steps, as here.  We
typically use hypotheses of the formula without noting "replacement of
equals by equals" as when we replaced (consp z) by nil, and we
typically omit to mention the use of basic axioms like if-nil above.

Now use your browser's Back Button to return to the example proof in
logic-knowledge-taken-for-granted.

POST-INDUCTION-KEY-CHECKPOINTS    reading post-induction key checkpoints

Each post-induction key checkpoint is a theorem if and only if the
original conjecture was a theorem.  The reason is that each subgoal
produced by induction concludes with the original formula and
simplification preserves equivalence.

So if you see a post-induction key checkpoint that is not a theorem,
stop looking at the checkpoints!  Your original conjecture is not a
theorem!  Fix it.

If you're convinced all the post-induction conjectures are theorems, ask
whether each has the hypotheses you'd need to prove it.  If the case
analysis feels inappropriate or induction hypotheses seem to be missing,
then ACL2 might have done the wrong induction.  Find the induction
scheme it did by reading the first induction message printed after the
conjecture was submitted.  If it is wrong, then extend ACL2's induction
analysis or tell ACL2 what induction to do, as explained shortly.

But before you decide the induction hypothesis is missing, look closely
for contradictions among the hypotheses of the checkpoint formula.  For
example, perhaps one of the hypotheses is (MEMBER e x) and another is
(NOT (MEMBER e' x')) where e, x, e', and x' are possibly complicated
expressions.

Is it possible that e and e' are equal and x and x' are equal?  If so,
then the two hypotheses are contradictory and the checkpoint would be
proved if you could find rules that would simplify those expressions to
their common forms.  So look for theorems about those subexpressions.

Or maybe you can get e and e' to reduce to some common d but but find
that x and x' are really different.  Then ask whether

     (implies (member d x) (member d x'))

If you could prove that, the key checkpoint would be proved.  Of course,
you may need other hypotheses from the checkpoint to state your
theorems.

If you have been working your way through the tutorial introduction to
the theorem prover, use your browser's Back Button now to
introduction-to-key-checkpoints.

PRACTICE-FORMULATING-STRONG-RULES    a few simple checkpoints suggesting strong rules

Consider these definitions:

     (defun rev (x)
       (if (endp x)
           nil
           (append (rev (cdr x)) (list (car x)))))

     (defun nats-below (j)
       (if (zp j)
           '(0)
           (cons j (nats-below (- j 1)))))

We assume you are familiar with such ACL2 built-ins as append, member,
subsetp and true-listp.  When we use throw-away names like FOO, BAR,
and MUM below we mean to suggest some arbitrary function you shouldn't
think about!  We're just trying to train your eye to ignore irrelevant
things.

Below are some terms that should suggest rewrite rules to you.  Imagine
that each of these terms occurs in some Key Checkpoint.  What rules
come to mind?  Try to think of the strongest rules you can.

Term 1:
(TRUE-LISTP (APPEND (FOO A) (BAR B)))

Answers:  See PRACTICE-FORMULATING-STRONG-RULES-1

Term 2:
(TRUE-LISTP (REV (FOO A)))

Answers:  See PRACTICE-FORMULATING-STRONG-RULES-2

Term 3:
(MEMBER (FOO A) (APPEND (BAR B) (MUM C)))

Answers:  See PRACTICE-FORMULATING-STRONG-RULES-3

Term 4:
(SUBSETP (APPEND (FOO A) (BAR B)) (MUM C))

Answers:  See PRACTICE-FORMULATING-STRONG-RULES-4

Term 5:
(SUBSETP (FOO A) (APPEND (BAR B) (MUM C)))

Answers:  See PRACTICE-FORMULATING-STRONG-RULES-5

Term 6:
(MEMBER (FOO A) (NATS-BELOW (BAR B)))

Answers:  See PRACTICE-FORMULATING-STRONG-RULES-6

We recommend doing all of these little exercises.  When you're
finished, use your browser's Back Button to return to
strong-rewrite-rules.

PRACTICE-FORMULATING-STRONG-RULES-1    rules suggested by (TRUE-LISTP (APPEND (FOO A) (BAR B)))

What rules come to mind when looking at the following subterm of a Key
Checkpoint?  Think of strong rules (see STRONG-REWRITE-RULES).

     (TRUE-LISTP (APPEND (FOO A) (BAR B)))

Obviously, you must think about the conditions under which (APPEND x y)
returns a true-list.  Recall that APPEND concatentates x and y, with y
being the terminal sublist.  Its definition is equivalent to

     (defun append (x y)
       (if (endp x)
           y
           (cons (car x)
                 (append (cdr x) y))))

Technical Note:  Append is really a macro that permits you to write
calls of append with more than two arguments.

In a sense, append "expects" its arguments to be lists ending in nil,
so-called true-listps.  (Such expectations are formalized in ACL2 by
the notion of the "guard" <> of the function, but we strongly recommend
not investigating guards until you're good at using the system.)

New users frequently start every new theorem by listing all their
expectations on the arguments of functions in the problem.  For
example, if the new user wants to make some statement about when
(append x y) is a true-listp, it is not uncommon for him or her first
to write:

     (implies (and (true-listp x)
                   (true-listp y))
              ...)

to get "comfortable."  Then, thinking about when (append x y) is a
true-listp is easy:  it always returns a true-listp.  It's always a
true-listp."  This thinking produces the theorem:

     (defthm true-listp-append-really-weak
       (implies (and (true-listp x)
                     (true-listp y))
                (true-listp (append x y))))

You'll note we gave it a name suggesting it is "really weak."

One sense in which it is weak is that it has an unnecessary hypothesis.
If y is a true-listp, then (append x y) is too, whether x is a
true-listp or not.  In ACL2, all functions are total.  Logically
speaking, it doesn't matter whether endp expects its argument to be a
true-listp or not, it behaves.  (Append x y) either returns y or a cons
whose second argument is generated by append.  Thus, if y is a
true-listp, the answer is too.  So here is an improved version of the
rule:

     (defthm true-listp-append-weak
       (implies (true-listp y)
                (true-listp (append x y))))

We still think of it as "weak" because it has a hypothesis that limits
its applicability.

The strong version of the rule is

     (defthm true-listp-append-strong
       (equal (true-listp (append x y))
              (true-listp y))).

That is, append returns a true-listp precisely when its second argument
is a true-listp.  We recommend that the strong version be made a
:rewrite <> rule.

The weak version of the rule allows us to reduce (TRUE-LISTP (APPEND x
y)) to true if we can show that (TRUE-LISTP y) is true.  But suppose
(TRUE-LISTP y) is actually false.  Then (TRUE-LISTP (APPEND x y)) would
not simplify under the weak version of the rule.  But under the strong
version it would simplify to NIL.

Technical Note: The weak version of the rule is a useful
:type-prescription <> rule.  The type mechanism cannot currently
exploit the strong version of the rule.

The strategy of "getting comfortable" by adding a bunch of hypotheses
before you know you need them is not conducive to creating strong
rules.  We tend to state the main relationship that we intuit about
some function and then add the hypotheses we need to make it true.  In
this case, there were no necessary hypotheses.  But if there are, we
first identify them and then we ask "what can I say about the function
if these hypotheses aren't true?"  and try to strengthen the statement
still further.

Use your browser's Back Button now to return to
practice-formulating-strong-rules.

PRACTICE-FORMULATING-STRONG-RULES-2    rules suggested by (TRUE-LISTP (REV (FOO A)))

What rules come to mind when looking at the following subterm of a Key
Checkpoint?  Think of strong rules (see STRONG-REWRITE-RULES).

     (TRUE-LISTP (REV (FOO A)))

The definition of rev in this problem is

     (defun rev (x)
       (if (endp x)
           nil
           (append (rev (cdr x)) (list (car x)))))

Since the definition terminates with an endp test and otherwise cdrs
the argument, the author of rev was clearly expecting x to be a
true-listp.  (Indeed, the "guard" <> for rev must require include
(true-listp x) since that is endp's guard.)  So you're naturally
justified in limiting your thoughts about (rev x) to x that are
true-lists.  This gives rise to the theorem:

     (defthm true-listp-rev-weak
       (implies (true-listp x)
                (true-listp (rev x))))

This is the kind of thinking illustrated in the earlier append example
(see PRACTICE-FORMULATING-STRONG-RULES-1) and, to paraphrase Z
in Men in Black, it exemplifies "everything we've come to expect from
years of training with typed languages."

But logically speaking, the definition of rev does not require x to be
a true-listp.  It can be any object at all: ACL2 functions are total.
Rev either returns nil or the result of appending a singleton list onto
the right end of its recursive result.  That append always returns a
true-listp since the singleton list is a true list.  (See
PRACTICE-FORMULATING-STRONG-RULES-1.)

So this is a theorem and a very useful :rewrite <> rule:

     (defthm true-listp-rev-strong
       (true-listp (rev x))).

Use your browser's Back Button now to return to
practice-formulating-strong-rules.

PRACTICE-FORMULATING-STRONG-RULES-3    rules suggested by (MEMBER (FOO A) (APPEND (BAR B) (MUM C)))

What rules come to mind when looking at the following subterm of a Key
Checkpoint?  Think of strong rules (see STRONG-REWRITE-RULES).

     (MEMBER (FOO A) (APPEND (BAR B) (MUM C)))

Since (append x y) contains all the members of x and all the members of
y, e is a member of (append x y) precisely when e is a member of x or
of y.  So a strong statement of this is:

     (defthm member-append-strong-false
       (equal (member e (append x y))
              (or (member e x)
                  (member e y))))

However, this is not a theorem because member is not Boolean.  (Member
e x), for example, returns the first tail of x that starts with e, or
else nil.  To see an example of this formula that evaluates to nil, let

     e = 3
     x = '(1 2 3)
     y = '(4 5 6).

Then the left-hand side, (member e (append x y)) evaluates to (3 4 5 6)
while the right-hand side evaluates to (3).

However, the two sides are propositionally equivalent (both either nil
or non-nil together).  So this is a useful :rewrite <> rule:

     (defthm member-append-strong
       (iff (member e (append x y))
            (or (member e x)
                (member e y)))).

It tells the system that whenever it encounters an instance of (MEMBER
e (APPEND x y)) in a propositional occurrence (where only its
truthvalue is relevant), it should be replaced by this disjunction of
(MEMBER e x) and (MEMBER e y).

The following two formulas are true but provide much weaker rules and
we would not add them:

     (implies (member e x) (member e (append x y)))

     (implies (member e y) (member e (append x y)))

because they each cause the system to backchain upon seeing (MEMBER e
(APPEND x y)) expressions and will not apply unless one of the two
side-conditions can be established.

There is a rewrite rule that is even stronger than member-append-strong.
It is suggested by the counterexample, above, for the EQUAL version of
the rule.

     (defthm member-append-really-strong
       (equal (member e (append x y))
              (if (member e x)
                  (append (member e x) y)
                  (member e y))))

While member-append-strong only rewrites member-append expressions
occurring propositionally, the -really-strong version rewrites every
occurrence.

However, this rule will be more useful than member-append-strong only
if you have occurrences of member in non-propositional places.  For
example, suppose you encountered a term like:

     (CONS (MEMBER e (APPEND x y)) z).

Then the -strong rule does not apply but the -really-strong rule does.

Furthermore, the -really-strong rule, by itself, is not quite as good as
the -strong rule in propositional settings!  For example, if you have
proved the -really-strong rule, you'll notice that the system still has
to use induction to prove

     (IMPLIES (MEMBER E A)
              (MEMBER E (APPEND B A))).

The -really-strong rule would rewrite it to

     (IMPLIES (MEMBER E A)
              (IF (MEMBER E A)
                  (APPEND (MEMBER E A) B)
                  (MEMBER E B)))

which would further simplify to

     (IMPLIES (MEMBER E A)
              (APPEND (MEMBER E A) B))

What lemma does this suggest?  The answer is the rather odd:

     (implies x (append x y))

which rewrites propositional occurrences of (APPEND x y) to T if x is
non-nil.  This is an inductive fact about append.

A problem with the -really-strong rule is that it transforms even
propositional occurrences of member into mixed propositional and
non-propositional occurrences.

     (defthm member-append-really-strong
       (equal (member e (append x y))      ; <-- even if this is a propositional occurrence
              (if (member e x)
                  (append (member e x) y)  ; <-- the member in here is not!
                  (member e y))))

So if you are using the -really-strong lemma in a situation in which
all your member expressions are used propositionally, you'll suddenly
find yourself confronted with non-propositional uses of member.

Our advice is not to use the -really-strong version unless your
application is inherently using member in a non-propositional way.

Use your browser's Back Button now to return to
practice-formulating-strong-rules.

PRACTICE-FORMULATING-STRONG-RULES-4    rules suggested by (SUBSETP (APPEND (FOO A) (BAR B)) (MUM C))

What rules come to mind when looking at the following subterm of a Key
Checkpoint?  Think of strong rules (see STRONG-REWRITE-RULES).

     (SUBSETP (APPEND (FOO A) (BAR B)) (MUM C))

When is (append x y) a subset of z?  When everything in x is in z and
everything in y is in z.  We would make it a rewrite rule:

     (defthm subsetp-append-1-strong
       (equal (subsetp (append x y) z)
              (and (subsetp x z)
                   (subsetp y z))))

We put the "-1-" in the name because there is a comparable theorem for
when the append is in the second argument of the subsetp; see
PRACTICE-FORMULATING-STRONG-RULES-5.

This strong rule is better than the conditional rule;

     (defthm subsetp-append-1-weak
       (implies (and (subsetp x z)
                     (subsetp y z))
                (subsetp (append x y) z)))

for all the usual reasons.

Use your browser's Back Button now to return to
practice-formulating-strong-rules.

PRACTICE-FORMULATING-STRONG-RULES-5    rules suggested by (SUBSETP (FOO A) (APPEND (BAR B) (MUM C)))

What rules come to mind when looking at the following subterm of a Key
Checkpoint?  Think of strong rules (see STRONG-REWRITE-RULES).

     (SUBSETP (FOO A) (APPEND (BAR B) (MUM C)))

When is x a subset of (append y z)?  Clearly it is if x is a subset of y
or x is a subset of z.  We could write that:

     (defthm subsetp-append-2-weak
       (implies (or (subsetp x y)
                    (subsetp x z))
                (subsetp x (append y z))))

The rule generated from this is:  "if you ever encounter (an instance
of) (SUBSETP x (APPEND y z)), backchain to the or above and try to
establish it.  If you can establish it, replace the target by T."

This does not fully characterize the situation though.  For example,
'(1 2 3 4) is a subset of (append '(1 3) '(2 4)) without being a subset
of either argument of the append.

However, no obvious equivalence comes to mind - indeed, to express any
of the ideas floating around here requires defining and introducing more
functions, which is not recommended unless those functions are already
in the problem.

For example, if you defined the concept of "set-minus" so that
(set-minus x y) consists of those elements of x not in y, then you
could prove:

     (defthm subset-append-2-strong-but-messy
       (equal (subsetp x (append y z))
              (and (subsetp (set-minus x z) y)
                   (subsetp (set-minus x y) z))))

But this rewrite rule would "trade" append away and introduce set-minus.
That might be a good strategy if set-minus were already in the problem.
But if it were not, it might not be.  We wouldn't recommend this rule
unless it were helpful in normalizing the expressions in the problem.

We recommend sticking with the weak version of the rule,

     (defthm subsetp-append-2-weak
       (implies (or (subsetp x y)
                    (subsetp x z))
                (subsetp x (append y z)))).

This illustrates the fact that sometimes there is no strong version of
a rule!

Use your browser's Back Button now to return to
practice-formulating-strong-rules.

PRACTICE-FORMULATING-STRONG-RULES-6    rules suggested by (MEMBER (FOO A) (NATS-BELOW (BAR B)))

What rules come to mind when looking at the following subterm of a Key
Checkpoint?  Think of strong rules (see STRONG-REWRITE-RULES).

     (MEMBER (FOO A) (NATS-BELOW (BAR B)))

The definition of NATS-BELOW is

     (defun nats-below (j)
       (if (zp j)
           '(0)
           (cons j (nats-below (- j 1)))))

Thus, (nats-below 7) is (7 6 5 4 3 2 1 0).  So when is k a member of
(nats-below j)?

The weakest version is

     (defthm member-nats-below-weak
       (implies (and (natp k)
                     (natp j)
                     (<= k j))
                (member k (nats-below j))))

But clearly we could improve this to:

     (defthm member-nats-below-weak-better
       (implies (and (natp k)
                     (natp j))
                (iff (member k (nats-below j))
                     (<= k j))))

or even

     (defthm member-nats-below-weak-better
       (implies (natp j)
                (iff (member k (nats-below j))
                     (and (natp k)
                          (<= k j)))))

Clearly though, we'd like to get rid of the (natp j) hypothesis and the
neatest plausible version is:

     (defthm member-nats-below-weak-neatest
       (iff (member k (nats-below j))
            (and (natp j)
                 (natp k)
                 (<= k j))))

But it is not a theorem!  For example, if j is -1 and k is 0, then the
left-hand side above returns t, because (nats-below j) is (0), but the
right-hand side is nil.

But this suggests a strategy for dealing with necessary hypotheses,
like (natp j).  We can move them into an IF on the right-hand side!
Something like this might be a useful rewrite rule:

     (iff (member k (nats-below j))
          (if (natp j)
              (and (natp k)
                   (<= k j))
              ...)).

We know, from member-nats-below-weak-better, that if (natp j) is true,
the member is equivalent to (and (natp k) (<= k j)).  So now consider
what we know if (natp j) is false.  If we can think of some term it's
equivalent to nd that term is simpler than the member expression, we
have a strong rule.

But by inspection of the definition of nats-below, we see that when
(natp j) is false, (nats-below j) is the list (0) because (zp j) is t.
That is, nats-below treats all non-natural arguments like they were 0.
Thus, when (natp j) is false, (member k (nats-below j)) is (member k
'(0)), which is (equal k 0).

So the strong version is

     (defthm member-nats-below-strong
        (iff (member k (nats-below j))
             (if (natp j)
                 (and (natp k)
                      (<= k j))
                 (equal k 0))))

This is a great :rewrite <> rule.  It gets rid of the member and
nats-below and introduces arithmetic.

This example illustrates the idea of putting an if on the
right-hand-side of the equivalence.  Many users tend to limit
themselves to propositional forms inside iff or to simple expressions
inside of equal.  But it is quite natural to use if to express what the
answer is:  if j is a natural, then k is in (nats-below j) precisely if
k is a natural less than or equal to j; if j is not a natural, then k
is in (nats-below j) precisely if k is 0.

Use if to lay out the cases you must consider, if you can think of a
simpler, equivalent expression for every possible case.

Use your browser's Back Button now to return to
practice-formulating-strong-rules.

PROGRAMMING-KNOWLEDGE-TAKEN-FOR-GRANTED    background knowledge in ACL2 programming for theorem prover tutorial

This brief review of the programming language is presented as a
sequence of questions and answers meant to test your knowledge of the
ACL2 programming language.  If you want a gentle introduction to the
programming language, see
`http://www.cs.utexas.edu/users/moore/publications/gentle-intro-to-acl2-programming.html'.

Before we get started with the programming drill, let us remind you
that all we're interested in here is the language, not the "program
development environment."  It's impossible to program in ACL2 or any
other language without a decent environment, one that at the very least
includes a way to prepare and edit files of programs.  The two most
popular program development environments among ACL2 users are Emacs <>
and the Eclipse-based ACL2-Sedan <>.  The Sedan provides the most
support for the new user, including real-time syntax checking and a
facility for testing among many other features.  But in this drill
we're not interested in the program development environment, we're
interested in your understanding of the ACL2 language.

Q: What do you think this command does?

     (defun rev (x)
       (if (endp x)
           nil
           (append (rev (cdr x)) (list (car x)))))

A:  It defines a function named rev that takes one argument, treats it
like a list, and reverses the order of the elements in that list.  To
figure this out from the definition, you have to know that append
concatenates two lists.  Logically speaking, the defun of rev adds the
axiom:

     (rev x)
     =
     (if (endp x)
         nil
         (append (rev (cdr x)) (list (car x)))),

implicitly quantified for all x.

Q:  Given the defun of rev above, what are the formal parameters?  What
is the body of the definition?  Write down a call of append that occurs
in the body of rev.  What are the actuals of that call?  A:  The
formals of rev is the list of variables after the first rev in the
defun, namely (x).  We say x is the first (and only) formal here.  The
body of rev is the entire if-expression.  The only call of append in
the body is

     (append (rev (cdr x)) (list (car x)))

and the actuals of that call are, respectively, (rev (cdr x)) and (list
(car x)).

Q: What do you get if you evaluate (rev '(a b c d))?  A: (D C B A).

Q: How did rev change the case of the elements, e.g., lowercase a was
in the input list but uppercase A was in the output?  A: This is a
trick question.  Rev doesn't change the case of the elements.  ACL2 is
case-insensitive when dealing with symbols.  The symbol a is read in as
the symbol A.  Thus, when writing function names, for example, we can
write rev, Rev, REV, or even ReV and always be referring to the
function REV.  By default, ACL2 prints symbols in uppercase.

Q: What does (rev '((a b c) "Abc" "a" b #\c)) return?  A: (#\c B "a"
"Abc" (A B C)).  If you thought the answer was any of these, then you
need to think or read more carefully:

     (#\C B "A" "ABC" (A B C))

     (#\C B "A" "ABC" (C B A))

The first wrong answer above is wrong because Lisp is "case
insensitive" only for symbols, not for character objects like #\c (the
lowercase character c) or for strings.   Furthermore, "A" is a string,
not a symbol; it is different from A.  The second wrong answer above is
wrong because rev does not go into the individual elements of the list,
it just reverses the order of the elements.  So it doesn't change the
element (A B C) to (C B A).

Q: In the question about what (rev '(a b c d)) returns, we put a quote
mark before the (a b c d) but not before the answer, (D C B A).  Why?
A:  The phrase "x evaluates to y" treats x as a term to be evaluated
and y as an object.  (Rev '(a b c d)) is a term to be evaluated and
denotes a call of the function rev on the value of the argument term
'(a b c d).  The value of that argument term is the object (a b c d).
The value of the call of rev is the object (d c b a).  If you have an
object, obj, and you wish to create a term whose value is obj, then you
put a quote mark in front of it, 'obj.

Q: Can rev be applied to something other than a list?  A:  Yes, every
ACL2 function can be applied to any object.  ACL2 is an untyped
programming language:  every variable ranges over the entire universe of
objects.  In normal usage, rev is applied to lists but there is nothing
about the syntax of the language that prevents it being applied to
non-lists.

Q: So what does (rev 23) evaluate to?  A:  Nil.

Q: Why?  A:  Because (endp 23) is t, because endp is defined:

     (defun endp (x) (not (consp x)))

Thus, if rev is applied to anything that is not a cons, it returns nil.

Q: So what does (rev '(a b c . d)) evaluate to?  A:  (c b a).  To
explain why requires demonstrating that you know what (a b c . d)
means.  It is the object computed by evaluating:

     (cons 'a
           (cons 'b
                 (cons 'c
                       'd))).

That is, it is a list whose "terminal marker" is the atom D.  Rev
treats that list exactly as it treats the nil-terminated list of the
same elements, (a b c), because (endp 'D) = (endp nil) = t.

Q: What does (rev 1 2 3) evaluate to?  A: That's a trick question.  Rev
takes one argument, not three.  So (rev 1 2 3) is an ill-formed term.

Q: What does (rev '(a b c . d . nil)) evaluate to?  A:  That is a trick
question.  There is no such object.  In Lisp's "dot notation" every dot
must be followed by a well-formed object and then a close parenthesis.
Usually that "well-formed object" is an atom.  If it is not an atom,
i.e., if it is a cons, then the entire expression could have been
written without that dot.  For example, (a b c . (d e)) is an object,
but it could be written (a b c d e).

Q: Do (rev (rev x)) and x always evaluate to the same object?  A: No.
(Rev (rev 23)) evaluates to nil, not 23.

Q: Do (rev (rev x)) and x always evaluate to the same object when x is
a cons?  A:  No.  (rev (rev '(a b c . d))) evaluates to (a b c), not (a
b c . d).

Q: When are (rev (rev x)) and x equal?  A: When the terminal marker of
x is nil.

Q: Can you define a Lisp function that recognizes nil-terminated lists?
A:  Yes, but it is not necessary for the user to define that concept
because Common Lisp provides such a function which is logically defined
as follows:

     (defun true-listp (x)
       (if (consp x)
           (true-listp (cdr x))
           (equal x nil))).

This can be paraphrased: (true-listp x) means that if x is a cons, its
cdr is a true-listp and if x is not a cons, it must be nil.  Thus,
(true-listp '(a b c)) is t and (true-listp '(a b c . d)) is nil.

Q: Can you write a Lisp formula that says "If z is a nil-terminated
list then reversing the result of reversing z is z"?

A:  Yes:

     (implies (true-listp z)
              (equal (rev (rev z)) z)).

Q:  Is this all there is to ACL2 programming?  A:  No!  ACL2 provides
many other features.  For a full list of all the primitive functions in
ACL2 see PROGRAMMING <>.  Some highlights for the beginner are
mentioned below, but all of the links below ought to be tagged with the
<> sign.

* list:  build a nil-terminated list from the values of n terms, e.g.,
(list x (+ 1 x) (+ 2 x)) returns (3 4 5) if x is 3.

* list*: build a non-nil terminated list of n objects from the values
of n+1 terms, e.g., (list* x (+ 1 x) (+ 2 x) (* -1 x)) returns the list
(3 4 5 . -3) if x is 3.

* and, or, not, implies, iff:  The propositional connectives.  And and
or are allowed to take a varying number of arguments, e.g., (and p q r)
is just an abbreviation for (and p (and q r)).  In Lisp, and returns
nil if any of its arguments evaluates to nil; otherwise it returns the
value of the last argument!  Thus, (and t t 3) returns 3!  If you
object to the idea that and is not Boolean, don't give it non-Boolean
arguments!  Similarly, or returns the value of the first argument that
evaluates to non-nil, or nil if they all evaluate to nil.  Both and and
or can be thought of as "lazy" in that they don't always have to
evaluate all their arguments.  This is really accomplished by treating
and and or as abbrevations for if nests.

* +, *, -, /, floor, mod, <, <=, >=, >: the Lisp elementary arithmetic
operators.  Both + and * allow varying numbers of arguments.  All the
arithmetic operators default non-numeric arguments to 0.  If you don't
like the idea that (+ 1 2 t) is 3, don't ask + to add t to something!

* natp, integerp, rationalp, characterp, stringp, symbolp, consp:  the
recognizers for the primitive data types.  The first three recognize
subsets of the ACL2 numeric universe.  The naturals are a subset of the
integers, the integers are a subset of the rationals, and the rationals
are a subset of the objects recognized by acl2-numberp, which also
includes the complex-rationalps.  The other recognizers listed above
recognize characters, strings, symbols, and conses.

* cond:  a convenient way to write a cascading nest of ifs, e.g.,

     (cond ((not (natp x)) 'non-natural)
           ((equal x 0) 'zero)
           ((evenp x) 'positive-even)
           (t 'positive-odd))

abbreviates

     (if (not (natp x))
         'non-natural
         (if (equal x 0)
             'zero
             (if (evenp x)
                 'positive-even
                 'positive-odd))).

* case:  a convenient way to case split on the identity of an object.

     (case key
       (non-natural -1)
       (zero 0)
       ((positive-even positive-odd) 'positive-natural)
       (otherwise 'unknown))

abbreviates

     (cond ((eql key 'non-natural) -1)
           ((eql key 'zero) 0)
           ((member key '(positive-even positive-odd))
            'positive-natural)
           (t 'unknown)).

* user defined macros:  using defmacro <> you can introduce your own
abbreviations.  We recommend you not do this until you're good at list
processing since macros are functions that build objects representing
terms.

* mutual-recursion:  allows you to define mutually-recursive functions.

* mv and mv-let:  allow functions to return "multiple-values".  In
Lisp, such functions return vectors of values, the vectors are
represented as lists of values, but the implementations are generally
more efficient.  For example, (mv x y z) returns a "vector" consisting
of the values of x, y, and z.

     (mv-let (a b c)
             (foo x)
             (bar a b c x))

evaluates (foo x), treats the result as a vector of three values, binds
the variables a, b, and c to those three values, and evaluates and
returns (bar a b c x).

ACL2 also provides many other features, such as single-threaded objects
which may be "destructively modified" (see STOBJ <>, including
a very special single-threaded object that records the state <> of the
ACL2 system), file input and output (see IO <>), applicative
arrays (see ARRAYS <>) and property lists (see GETPROP
<>) and other facilities necessary for it to be a practical programming
language.  However, we strongly recommend that as a new user you stay
away from these features until you are good at proving theorems about
elementary list processing!

If this little drill made sense to you, you know enough of the
programming language to get started. Use your browser's Back Button now
to return to introduction-to-the-theorem-prover.

If you are uncomfortable with ACL2 programming, we recommend that you
study
`http://www.cs.utexas.edu/users/moore/publications/gentle-intro-to-acl2-programming.html'
and
`http://www.cs.utexas.edu/users/moore/publications/acl2-programming-exercises1.html'.

However, we strongly recommend that you first invest in learning either
the Emacs or Eclipse-based ACL2-Sedan program development environments,
since it is foolish to try to learn how to program in a stand-alone
read-eval-print loop!

While getting started, many users find the Hyper-Card a handy index
into the documentation for the ACL2 language:

`http://www.cs.utexas.edu/users/moore/publications/hyper-card.html'

Once you are comfortable with the ACL2 programming language, use your
browser's Back Button to return to introduction-to-the-theorem-prover.

SPECIAL-CASES-FOR-REWRITE-RULES    convenient short forms for rewrite rule formulas

In principle, every rewrite rule is made from a formula of this shape:

     (IMPLIES (AND hyp1 ... hypk)
              (eqv lhs rhs))

where eqv is either EQUAL or IFF and the result of expanding any
abbreviations in lhs is the application of some function symbol other
than IF.

* In the special case where there is only one hyp term, i.e., k=1, the
(AND hyp1) can be written hyp1.

* In the special case where there are no hyp terms, k=0, the (AND) term
is logically just T and the whole IMPLIES can be dropped; such a
formula may be written as an unconditional EQUAL or IFF term.

* If you build a rewrite rule from a formula that concludes with (NOT
x), it is treated as though it were (EQUAL x NIL), which is logically
equivalent to what you typed.

* If you build a rewrite rule from a formula that concludes with an
AND, ACL2 will build a rewrite rule for each conjunct of the AND.  This
is because

     (IMPLIES hyp (AND concl1 concl2))

is propositionally equivalent to

     (AND (IMPLIES hyp concl1)
          (IMPLIES hyp concl2)).

However, if you use an OR-expression as a hypothesis, ACL2 does not do
the dual transformation.  Thus, (IMPLIES (OR hyp1 hyp2) concl)
generates one rewrite rule.

* Finally, if you build a rewrite rule from a formula that does not
conclude with an EQUAL, an IFF, a NOT, or an AND, but with some other
term, say, lhs, then ACL2 acts like you typed (IFF lhs T), which is
logically equivalent to what you typed.

Thus, regardless of what you type, every rule has k hypotheses.  For
unconditional rules, k is 0 and the hypotheses are vacuously true.
Whether or not you write an EQUAL or an IFF in the conclusion, every
rule is either an equality or a propositional equivalence, every rule
has a left-hand side, and every rule has a right-hand side.

Use your browser's Back Button now to return to
introduction-to-rewrite-rules-part-1.

SPECIFIC-KINDS-OF-FORMULAS-AS-REWRITE-RULES    advice about how to handle commonly occurring formulas as rewrite rules

Below we give you some guidelines for handling specific, commonly
occurring situations.

* Associativity:  If a function f is associative, prove

     (equal (f (f x y) z) (f x (f y z)))

ACL2 will use this to flatten f-nests "to the right."

* Commutativity:  If a function f is commutative, prove both

     (equal (f x y) (f y x))

and

     (equal (f x (f y z)) (f y (f x z)))

ACL2's heuristics will use these rules to order the arguments
alphabetically, so that (f B (f D (f A C))) becomes (f A (f B (f C D))).

* Distributivity:  If you have a pair of functions f and g so that (f x
(g y z)) is (g (f x y) (f x z)) or some other form of distributivity is
provable, arrange your rules to move the lighter function symbol up and
the heavier one toward the variable symbols.  For example, our
arithmetic libraries drive multiplication through addition, producing
sums of products rather than products of sums.

* Identity and Other Laws: Prove the obvious identity and zero laws (or
at least anticipate that you might need them down the road) so as to
eliminate operators.

* Get Rid of Tail Recursive Functions: A corollary to the above advice
concerns tail recursive functions that use auxiliary variables.  New
users often define concepts using tail recursions, accumulating partial
results in auxiliary variables, because creating such functions is
similar to programming with while loops.  Expert users will use tail
recursion when necessary for execution efficiency.  But tail recursive
functions are messy to reason about: their auxiliary variables have to
be properly initialized to make the functions compute the expected
results, but to state inductively provable properties of tail recursive
functions you must identify the invariants on those auxiliary
variables.  This problem tends not to happen with primitive recursive
functions.  A primitive recursive function is one that recurs down one
variable and holds all the other variables constant in recursion.  Most
tail-recursive functions can be written elegantly as primitive
recursive functions, though one might have to ignore the programmer's
desire to make things efficient and define auxiliary functions to
appropriately transform the value returned by the recursive call.  The
classic example is reverse defined in terms of the auxiliary function
append versus reverse defined tail recursively with an accumulator.  By
introducing append you introduce a concept about which you can state
lemmas and decompose the proofs of properties of reverse.  So if your
problem involves tail recursive functions with auxiliary variables,
define the primitive recursive version, prove that the tail recursive
function is equivalent to the primitive recursive one, and arrange the
rewrite rule to eliminate the tail recursive function.

* Get Rid of Mutually Recursive Functions: Similarly, if you have used
mutual-recursion to introduce a clique of mutually recursive functions,
f1, f2, ..., you will find that to reason about any one function in the
nest you have to reason about all of them.  Any mutually recursive
function can be defined in a singly recursive way.  So do that and then
prove a rewrite rule that gets rid of all the mutually recursive
functions by proving

     (and (equal (f1 ...) (g1 ...))
          (equal (f2 ...) (g2 ...))
          ...)

where the gi are singly recursive.  You may need to appeal to a trick to
define the gi: define a singly recursive function that takes a flag
argument and mimics whichever mutually recursive function the flag
specifies.  See MUTUAL-RECURSION <> and see
MUTUAL-RECURSION-PROOF-EXAMPLE <>.

If you got to this documentation page from the tutorial discussion of
rewrite rules, use your browser's Back Button now to return to
introduction-to-rewrite-rules-part-2.

STRONG-REWRITE-RULES    formulating good rewrite rules

Suppose you notice the following term in a Key Checkpoint:

     (MEMBER (CAR A) (REV B)).

You might think of two theorems for handling this term, which we'll
call the "weak" and "strong" version of member-rev.

     (defthm member-rev-weak
       (implies (member e b)
                (member e (rev b)))).

     (defthm member-rev-strong
       (iff (member e (rev b))
            (member e b))).

The "strong" version logically implies the "weak" version and so
deserves the adjective.  (Recall that "p <--> q" is just "p --> q" and
"q --> p."  So the strong version quite literally says everything the
weak version does and then some.)

But the "strong" version also produces a better rewrite rule.  Here are
the rules generated from these two formulas, phrased as directives to
ACL2's simplifier:

member-rev-weak: If you ever see an instance of (MEMBER e (REV b)),
backchain to (MEMBER e b) (i.e., turn your attention to that term) and
if you can show that it is true, replace (MEMBER e (REV b)) by T.

member-rev-strong:  If you ever see an instance of (MEMBER e (REV b)),
replace it by (MEMBER e b).

Technical Note: Actually, both rules concern propositional occurrences
of the "target" expression, (MEMBER e (REV b)), i.e., occurrences of
the target in which its truthvalue is the only thing of relevance.
(Recall that (MEMBER x y) returns the tail of y starting with x!
Evaluate some simple MEMBER expressions, like (MEMBER 3 '(1 2 3 4 5))
to see what we mean.)  Both theorems tell us about circumstances in
which the target is non-NIL (i.e., "true") without telling us its
identity.  But ACL2 keeps track of when the target is in a
propositional occurrence and can use such rules to rewrite the target
to propositionally equivalent terms.

So the strong version is better because it will always eliminate
(MEMBER e (REV b)) in favor of (MEMBER e b).  That simpler expression
may be further reduced if the context allows it.  But in any case, the
strong version eliminates REV from the problem.  The weak version only
eliminates REV when a side-condition can be proved.

While either version may permit us to prove the Key Checkpoint that
"suggested" the rule, the strong version is a better rule to have in the
database going forward.

For example, suppose NATS-BELOW returns the list of natural numbers
below its argument.  Imagine two alternative scenarios in which a key
checkpoint is about to arise involving this term:

     (MEMBER K (REV (NATS-BELOW J)))

Scenario 1 is when you've got the strong version in your database: it
will rewrite the key checkpoint term to

     (MEMBER K (NATS-BELOW J))

and that's what you'll see in the printed checkpoint unless other rules
reduce it further.

Scenario 2 is when you have only the weak version in your database: the
weak rule will attempt to reduce the term above to T and will, if there
are sufficient rules and hypotheses about K's membership in (NATS-BELOW
J).  But if no such rules or hypotheses are available, you'll be
confronted with a key checkpoint involving

     (MEMBER K (REV (NATS-BELOW J)))

and it will not be obvious that the problem would go away if you could
establish that K is in (NATS-BELOW J).  Clearly, Scenario 1 is better.

We recommend that you now practice formulating strong versions of rules
suggested by terms you might see.  See
PRACTICE-FORMULATING-STRONG-RULES.

When you are finished with that, use your browser's Back Button to
return to introduction-to-key-checkpoints.

STARTUP    How to start using ACL2; the ACL2 command loop

When you start up ACL2, you'll probably find yourself inside the ACL2
command loop, as indicated by the following prompt.

       ACL2 !>

If not, you should type (LP).  See LP, which has a lot more
information about the ACL2 command loop.

You should now be in ACL2.  The current "default-defun-mode" is :logic;
the other mode is :program, which would cause the letter p to be
printed in the prompt.  :Logic means that any function we define is not
only executable but also is axiomatically defined in the ACL2 logic.
See DEFUN-MODE and see DEFAULT-DEFUN-MODE.  For example
we can define a function my-cons as follows.  (You may find it useful
to start up ACL2 and submit this and other commands below to the ACL2
command loop, as we won't include output below.)

       ACL2 !>(defun my-cons (x y) (cons x y))

An easy theorem may then be proved:  the car of (my-cons a b) is A.

       ACL2 !>(defthm car-my-cons (equal (car (my-cons a b)) a))

You can place raw Lisp forms to evaluate at start-up into file
acl2-init.lsp in your home directory, except on Windows systems.  For
example, if you put the following into acl2-init.lsp, then ACL2 will
print "HI" when it starts up.

     (print "HI")

But be careful; all bets are off when you submit forms to raw Lisp, so
this capability should only be used when you are hacking or when you
are setting some Lisp parameters (e.g., (setq si::*notify-gbc* nil) to
turn off garbage collection notices in GCL).

Notice that unlike Nqthm, the theorem command is defthm rather than
prove-lemma.  See DEFTHM, which explains (among other things)
that the default is to turn theorems into rewrite rules.

Various keyword commands are available to query the ACL2 "world", or
database.  For example, we may view the definition of my-cons by
invoking a command to print events, as follows.

       ACL2 !>:pe my-cons

Also see PE.  We may also view all the lemmas that rewrite
terms whose top function symbol is car by using the following command,
whose output will refer to the lemma car-my-cons proved above.

       ACL2 !>:pl car

Also see PL.  Finally, we may print all the commands back
through the initial world as follows.

       ACL2 !>:pbt 0

See HISTORY for a list of commands, including these, for
viewing the current ACL2 world.

Continue with the documentation for annotated-acl2-scripts to see a
simple but illustrative example in the use of ACL2 for reasoning about
functions.

TIDBITS    some basic hints for using ACL2

See BOOKS for a discussion of books.  Briefly, a book is a file
whose name ends in ".lisp" that contains ACL2 events; see
EVENTS.

See HISTORY for a list of useful commands.  Some examples:

       :pbt :here      ; print the current event
       :pbt (:here -3) ; print the last four events
       :u              ; undo the last event
       :pe append      ; print the definition of append

See DOCUMENTATION to learn how to print documentation to the
terminal.  There are also versions of the documentation for Mosaic,
Emacs Info, and hardcopy.

There are quite a few kinds of rules allowed in ACL2 besides :rewrite
rules, though we hope that beginners won't usually need to be aware of
them.  See RULE-CLASSES for details.  In particular, there is
support for congruence rewriting.  See RUNE ("RUle NamE") for a
description of the various kinds of rules in the system.  Also see
THEORIES for a description of how to build theories of runes,
which are often used in hints; see HINTS.

A "programming mode" is supported; see PROGRAM, see
DEFUN-MODE, and see DEFAULT-DEFUN-MODE.  It can be useful to
prototype functions after executing the command :program, which will
cause definitions to be syntaxed-checked only.

ACL2 supports mutual recursion, though this feature is not tied into
the automatic discovery of induction schemas and is often not the best
way to proceed when you expect to be reasoning about the functions.
See DEFUNS; also see MUTUAL-RECURSION.

See LD for discussion of how to load files of events.  There
are many options to ld, including ones to suppress proofs and to
control output.

The :otf-flg (Onward Thru the Fog FLaG) is a useful feature that Nqthm
users have often wished for.  It prevents the prover from aborting a
proof attempt and inducting on the original conjecture.  See
OTF-FLG.

ACL2 supports redefinition and redundancy in events; see
LD-REDEFINITION-ACTION and see REDUNDANT-EVENTS.

A proof-tree display feature is available for use with Emacs.  This
feature provides a view of ACL2 proofs that can be much more useful
than reading the stream of characters output by the theorem prover as
its "proof."  See PROOF-TREE.

An interactive feature similar to Pc-Nqthm is supported in ACL2.  See
VERIFY and see PROOF-CHECKER.

ACL2 allows you to monitor the use of rewrite rules.  See
BREAK-REWRITE.

See ARRAYS to read about applicative, fast arrays in ACL2.

To quit the ACL2 command loop, or (in akcl) to return to the ACL2
command loop after an interrupt, type :q.  To continue (resume) after
an interrupt (in akcl), type :r.  To cause an interrupt (in akcl under
Unix (trademark of AT&T)), hit control-C (twice, if inside Emacs).  To
exit ACL2 altogether, first type :q to exit the ACL2 command loop, and
then exit Lisp (by typing (user::bye) in akcl).

See STATE to read about the von Neumannesque ACL2 state object
that records the "current state" of the ACL2 session.  Also see
@, and see ASSIGN, to learn about reading and setting
global state variables.

If you want your own von Neumannesque object, e.g., a structure that
can be "destructively modified" but which must be used with some
syntactic restrictions, see STOBJ.

TIPS    some hints for using the ACL2 prover

We present here some tips for using ACL2 effectively.  Though this
collection is somewhat _ad hoc_, we try to provide some organization,
albeit somewhat artificial:  for example, the sections overlap, and no
particular order is intended.  This material has been adapted by Bill
Young from a very similar list for Nqthm that appeared in the
conclusion of:  "Interaction with the Boyer-Moore Theorem Prover: A
Tutorial Study Using the Arithmetic-Geometric Mean Theorem," by Matt
Kaufmann and Paolo Pecchiari, CLI Technical Report 100, June, 1995.  We
also draw from a similar list in Chapter 13 of "A Computational Logic
Handbook" by R.S. Boyer and J S. Moore (Academic Press, 1988).  We'll
refer to this as "ACLH" below.

These tips are organized roughly as follows.

     A. ACL2 Basics

     B. Strategies for creating events

     C. Dealing with failed proofs

     D. Performance tips

     E. Miscellaneous tips and knowledge

     F. Some things you DON'T need to know

_ACL2 BASICS_

A1. The ACL2 logic.
This is a logic of total functions.  For example, if A and B are less
than or equal to each other, then we need to know something more in
order to conclude that they are equal (e.g., that they are numbers).
This kind of twist is important in writing definitions; for example, if
you expect a function to return a number, you may want to apply the
function fix or some variant (e.g., nfix or ifix) in case one of the
formals is to be returned as the value.

ACL2's notion of ordinals is important on occasion in supplying
"measure hints" for the acceptance of recursive definitions.  Be sure
that your measure is really an ordinal.  Consider the following
example, which ACL2 fails to admit (as explained below).

       (defun cnt (name a i x)
         (declare (xargs :measure (+ 1 i)))
         (cond ((zp (+ 1 i))
                0)
               ((equal x (aref1 name a i))
                (1+ (cnt name a (1- i) x)))
               (t (cnt name a (1- i) x))))

One might think that (+ 1 i) is a reasonable measure, since we know
that (+ 1 i) is a positive integer in any recursive call of cnt, and
positive integers are ACL2 ordinals (see O-P).  However, the
ACL2 logic requires that the measure be an ordinal unconditionally, not
just under the governing assumptions that lead to recursive calls.  An
appropriate fix is to apply nfix to (+ 1 i), i.e., to use

       (declare (xargs :measure (nfix (+ 1 i))))

in order to guarantee that the measure will always be an ordinal (in
fact, a positive integer).

For more about admissibility of recursive definitions, see
DEFUN, in particular the discussion of termination.

A2. Simplification.
The ACL2 simplifier is basically a rewriter, with some "linear
arithmetic" thrown in.  One needs to understand the notion of
conditional rewriting.  See REWRITE.

A3. Parsing of rewrite rules.
ACL2 parses rewrite rules roughly as explained in ACLH, _except_ that
it never creates "unusual" rule classes.  In ACL2, if you want a
:linear rule, for example, you must specify :linear in the
:rule-classes.  See RULE-CLASSES, and also see REWRITE
and see LINEAR.

A4. Linear arithmetic.
On this subject, it should suffice to know that the prover can handle
truths about + and -, and that linear rules (see above) are somehow
"thrown in the pot" when the prover is doing such reasoning.  Perhaps
it's also useful to know that linear rules can have hypotheses, and
that conditional rewriting is used to relieve those hypotheses.

A5. Events.
Over time, the expert ACL2 user will know some subtleties of its
events.  For example, in-theory events and hints are important, and
they distinguish between a function and its executable counterpart.

_B. STRATEGIES FOR CREATING EVENTS_

In this section, we concentrate on the use of definitions and rewrite
rules.  There are quite a few kinds of rules allowed in ACL2 besides
rewrite rules, though most beginning users probably won't usually need
to be aware of them.  See RULE-CLASSES for details.  In
particular, there is support for congruence rewriting.  Also see
RUNE ("RUle NamE") for a description of the various kinds of rules in
the system.

B1. Use high-level strategy.
Decompose theorems into "manageable" lemmas (admittedly, experience
helps here) that yield the main result "easily."  It's important to be
able to outline non-trivial proofs by hand (or in your head).  In
particular, avoid submitting goals to the prover when there's no reason
to believe that the goal will be proved and there's no "sense" of how
an induction argument would apply.  It is often a good idea to avoid
induction in complicated theorems unless you have a reason to believe
that it is appropriate.

B2. Write elegant definitions.
Try to write definitions in a reasonably modular style, especially
recursive ones.  Think of ACL2 as a programming language whose
procedures are definitions and lemmas, hence we are really suggesting
that one follow good programming style (in order to avoid duplication
of "code," for example).

When possible, complex functions are best written as compositions of
simpler functions.  The theorem prover generally performs better on
primitive recursive functions than on more complicated recursions (such
as those using accumulating parameters).

Avoid large non-recursive definitions which tend to lead to large case
explosions.  If such definitions are necessary, try to prove all
relevant facts about the definitions and then disable them.

Whenever possible, avoid mutual recursion if you care to prove anything
about your functions.  The induction heuristics provide essentially no
help with reasoning about mutually defined functions.  Mutually
recursive functions can usually be combined into a single function with
a "flag" argument.  (However, see
MUTUAL-RECURSION-PROOF-EXAMPLE for a small example of proof involving
mutually recursive functions.)

B3. Look for analogies.
Sometimes you can easily edit sequences of lemmas into sequences of
lemmas about analogous functions.

B4. Write useful rewrite rules.
As explained in A3 above, every rewrite rule is a directive to the
theorem prover, usually to replace one term by another.  The directive
generated is determined by the syntax of the defthm submitted.  Never
submit a rewrite rule unless you have considered its interpretation as
a proof directive.

B4a.  Rewrite rules should simplify.
Try to write rewrite rules whose right-hand sides are in some sense
"simpler than" (or at worst, are variants of) the left-hand sides.
This will help to avoid infinite loops in the rewriter.

B4b.  Avoid needlessly expensive rules.
Consider a rule whose conclusion's left-hand side (or, the entire
conclusion) is a term such as (consp x) that matches many terms
encountered by the prover.  If in addition the rule has complicated
hypotheses, this rule could slow down the prover greatly.  Consider
switching the conclusion and a complicated hypothesis (negating each)
in that case.

B4c. The "Knuth-Bendix problem".
Be aware that left sides of rewrite rules should match the "normalized
forms", where "normalization" (rewriting) is inside out.  Be sure to
avoid the use of nonrecursive function symbols on left sides of rewrite
rules, except when those function symbols are disabled, because they
tend to be expanded away before the rewriter would encounter an
instance of the left side of the rule.  Also assure that subexpressions
on the left hand side of a rule are in simplified form.

B4d. Avoid proving useless rules.
Sometimes it's tempting to prove a rewrite rule even before you see how
it might find application.  If the rule seems clean and important, and
not unduly expensive, that's probably fine, especially if it's not too
hard to prove.  But unless it's either part of the high-level strategy
or, on the other hand, intended to get the prover past a particular
unproved goal, it may simply waste your time to prove the rule, and
then clutter the database of rules if you are successful.

B4e. State rules as strongly as possible, usually.
It's usually a good idea to state a rule in the strongest way possible,
both by eliminating unnecessary hypotheses and by generalizing
subexpressions to variables.

Advanced users may choose to violate this policy on occasion, for
example in order to avoid slowing down the prover by excessive
attempted application of the rule.  However, it's a good rule of thumb
to make the strongest rule possible, not only because it will then
apply more often, but also because the rule will often be easier to
prove (see also B6 below).  New users are sometimes tempted to put in
extra hypotheses that have a "type restriction" appearance, without
realizing that the way ACL2 handles (total) functions generally lets it
handle trivial cases easily.

B4f. Avoid circularity.
A stack overflow in a proof attempt almost always results from circular
rewriting.  Use brr to investigate the stack; see BREAK-LEMMA.
Because of the complex heuristics, it is not always easy to define just
when a rewrite will cause circularity.  See the very good discussion of
this topic in ACLH.

See BREAK-LEMMA for a trick involving use of the forms brr t
and (cw-gstack) for inspecting loops in the rewriter.

B4g. Remember restrictions on permutative rules.
Any rule that permutes the variables in its left hand side could cause
circularity.  For example, the following axiom is automatically
supplied by the system:

       (defaxiom commutativity-of-+
                 (equal (+ x y) (+ y x))).

This would obviously lead to dangerous circular rewriting if such
"permutative" rules were not governed by a further restriction.  The
restriction is that such rules will not produce a term that is
"lexicographically larger than" the original term (see
LOOP-STOPPER).  However, this sometimes prevents intended rewrites.
See Chapter 13 of ACLH for a discussion of this problem.

B5. Conditional vs. unconditional rewrite rules.
It's generally preferable to form unconditional rewrite rules unless
there is a danger of case explosion.  That is, rather than pairs of
rules such as

     (implies p
              (equal term1 term2))

and

     (implies (not p)
              (equal term1 term3))

consider:

     (equal term1
            (if p term2 term3))

However, sometimes this strategy can lead to case explosions: IF terms
introduce cases in ACL2.  Use your judgment.  (On the subject of IF:
COND, CASE, AND, and OR are macros that abbreviate IF forms, and
propositional functions such as IMPLIES quickly expand into IF terms.)

B6. Create elegant theorems.
Try to formulate lemmas that are as simple and general as possible.
For example, sometimes properties about several functions can be
"factored" into lemmas about one function at a time.  Sometimes the
elimination of unnecessary hypotheses makes the theorem easier to
prove, as does generalizing first by hand.

B7. Use defaxioms temporarily to explore possibilities.
When there is a difficult goal that seems to follow immediately (by a
:use hint or by rewriting) from some other lemmas, you can create those
lemmas as defaxiom events (or, the application of skip-proofs to defthm
events) and then double-check that the difficult goal really does
follow from them.  Then you can go back and try to turn each defaxiom
into a defthm.  When you do that, it's often useful to disable any
additional rewrite rules that you prove in the process, so that the
"difficult goal" will still be proved from its lemmas when the process
is complete.

Better yet, rather than disabling rewrite rules, use the local
mechanism offered by encapsulate to make temporary rules completely
local to the problem at hand.  See ENCAPSULATE and see
LOCAL.

B9. Use books.
Consider using previously certified books, especially for arithmetic
reasoning.  This cuts down the duplication of effort and starts your
specification and proof effort from a richer foundation.  See the file
"doc/README" in the ACL2 distribution for information on books that
come with the system.

_C. DEALING WITH FAILED PROOFS_

C1. Look in proof output for goals that can't be further simplified.
Use the "proof-tree" utility to explore the proof space.  However, you
don't need to use that tool to use the "checkpoint" strategy.  The idea
is to think of ACL2 as a "simplifier" that either proves the theorem or
generates some goal to consider.  That goal is the first "checkpoint,"
i.e., the first goal that does not further simplify.  Exception:  it's
also important to look at the induction scheme in a proof by induction,
and if induction seems appropriate, then look at the first checkpoint
_after_ the induction has begun.

Consider whether the goal on which you focus is even a theorem.
Sometimes you can execute it for particular values to find a
counterexample.

When looking at checkpoints, remember that you are looking for any
reason at all to believe the goal is a theorem.  So for example,
sometimes there may be a contradiction in the hypotheses.

Don't be afraid to skip the first checkpoint if it doesn't seem very
helpful.  Also, be willing to look a few lines up or down from the
checkpoint if you are stuck, bearing in mind however that this practice
can be more distracting than helpful.

C2. Use the "break rewrite" facility.
Brr and related utilities let you inspect the "rewrite stack."  These
can be valuable tools in large proof efforts.  See BREAK-LEMMA
for an introduction to these tools, and see BREAK-REWRITE for
more complete information.

The break facility is especially helpful in showing you why a
particular rewrite rule is not being applied.

C3. Use induction hints when necessary.  Of course, if you can define
your functions so that they suggest the correct inductions to ACL2, so
much the better!  But for complicated inductions, induction hints are
crucial.  See HINTS for a description of :induct hints.

C4. Use the "Proof Checker" to explore.
The verify command supplied by ACL2 allows one to explore problem areas
"by hand."  However, even if you succeed in proving a conjecture with
verify, it is useful to prove it without using it, an activity that
will often require the discovery of rewrite rules that will be useful
in later proofs as well.

C5. Don't have too much patience.
Interrupt the prover fairly quickly when simplification isn't
succeeding.

C6. Simplify rewrite rules.
When it looks difficult to relieve the hypotheses of an existing
rewrite rule that "should" apply in a given setting, ask yourself if
you can eliminate a hypothesis from the existing rewrite rule.  If so,
it may be easier to prove the new version from the old version (and
some additional lemmas), rather than to start from scratch.

C7. Deal with base cases first.
Try getting past the base case(s) first in a difficult proof by
induction.  Usually they're easier than the inductive step(s), and
rules developed in proving them can be useful in the inductive step(s)
too.  Moreover, it's pretty common that mistakes in the statement of a
theorem show up in the base case(s) of its proof by induction.

C8. Use :expand hints.  Consider giving :expand hints.  These are
especially useful when a proof by induction is failing.  It's almost
always helpful to open up a recursively defined function that is
supplying the induction scheme, but sometimes ACL2 is too timid to do
so; or perhaps the function in question is disabled.

_D. PERFORMANCE TIPS_

D1. Disable rules.
There are a number of instances when it is crucial to disable rules,
including (often) those named explicitly in :use hints.  Also, disable
recursively defined functions for which you can prove what seem to be
all the relevant properties.  The prover can spend significant time
"behind the scenes" trying to open up recursively defined functions,
where the only visible effect is slowness.

D2. Turn off the "break rewrite" facility.  Remember to execute :brr
nil after you've finished with the "break rewrite" utility (see
BREAK-REWRITE), in order to bring the prover back up to full speed.

_E. MISCELLANEOUS TIPS AND KNOWLEDGE_

E1. Order of application of rewrite rules.
Keep in mind that the most recent rewrite rules in the history are
tried first.

E2. Relieving hypotheses is not full-blown theorem proving.
Relieving hypotheses on rewrite rules is done by rewriting and linear
arithmetic alone, not by case splitting or by other prover processes
"below" simplification.

E3. "Free variables" in rewrite rules.
The set of "free variables" of a rewrite rule is defined to contain
those variables occurring in the rule that do not occur in the left-hand
side of the rule.  It's often a good idea to avoid rules containing
free variables because they are "weak," in the sense that hypotheses
containing such variables can generally only be proved when they are
"obviously" present in the current context.  This weakness suggests
that it's important to put the most "interesting" (specific) hypotheses
about free variables first, so that the right instances are considered.
For example, suppose you put a very general hypothesis such as (consp
x) first.  If the context has several terms around that are known to be
consps, then x may be bound to the wrong one of them.  For much more
information on free variables, see FREE-VARIABLES.

E4. Obtaining information Use :pl foo to inspect rewrite rules whose
left hand sides are applications of the function foo.  Another approach
to seeing which rewrite rules apply is to enter the proof-checker with
verify, and use the show-rewrites or sr command.

E5. Consider esoteric rules with care.
If you care to see RULE-CLASSES and peruse the list of
subtopics (which will be listed right there in most versions of this
documentation), you'll see that ACL2 supports a wide variety of rules
in addition to :rewrite rules.  Should you use them?  This is a complex
question that we are not ready to answer with any generality.  Our
general advice is to avoid relying on such rules as long as you doubt
their utility.  More specifically:  be careful not to use conditional
type prescription rules, as these have been known to bring ACL2 to its
knees, unless you are conscious that you are doing so and have reason
to believe that they are working well.

_F. SOME THINGS YOU DON'T NEED TO KNOW_

Most generally:  you shouldn't usually need to be able to predict too
much about ACL2's behavior.  You should mainly just need to be able to
react to it.

F1. Induction heuristics.
Although it is often important to read the part of the prover's output
that gives the induction scheme chosen by the prover, it is not
necessary to understand how the prover made that choice.  (Granted,
advanced users may occasionally gain minor insight from such knowledge.
But it's truly minor in many cases.)  What _is_ important is to be
able to tell it an appropriate induction when it doesn't pick the right
one (after noticing that it doesn't).  See C3 above.

F2. Heuristics for expanding calls of recursively defined functions.
As with the previous topic, the important thing isn't to understand
these heuristics but, rather, to deal with cases where they don't seem
to be working.  That amounts to supplying :expand hints for those calls
that you want opened up, which aren't.  See also C8 above.

F3. The "waterfall".
As discussed many times already, a good strategy for using ACL2 is to
look for checkpoints (goals stable under simplification) when a proof
fails, perhaps using the proof-tree facility.  Thus, it is reasonable
to ignore almost all the prover output, and to avoid pondering the
meaning of the other "processes" that ACL2 uses besides simplification
(such as elimination, cross-fertilization, generalization, and
elimination of irrelevance).  For example, you don't need to worry
about prover output that mentions "type reasoning" or "abbreviations,"
for example.

BDD    ordered binary decision diagrams with rewriting

Ordered binary decision diagrams (OBDDs, often simply called BDDs) are
a technique, originally published by Randy Bryant, for the efficient
simplification of Boolean expressions.  In ACL2 we combine this
technique with rewriting to handle arbitrary ACL2 terms that can
represent not only Boolean values, but non-Boolean values as well.  In
particular, we provide a setting for deciding equality of bit vectors
(lists of Boolean values).

An introduction to BDDs for the automated reasoning community may be
found in "Introduction to the OBDD Algorithm for the ATP Community" by
J Moore, Journal of Automated Reasoning (1994), pp. 33-45.  (This paper
also appears as Technical Report #84 from Computational Logic, Inc.)

Further information about BDDs in ACL2 can be found in the subtopics of
this documentation section.  In particular, see
BDD-INTRODUCTION for a good starting place that provides a number of
examples.

See HINTS for a description of :bdd hints.  For quick
reference, here is an example; but only the :vars part of the hint is
required, as explained in the documentation for hints.  The values
shown are the defaults.

     (:vars nil :bdd-constructors (cons) :prove t :literal :all)

We suggest that you next visit the documentation topic BDD-INTRODUCTION.

BDD-ALGORITHM    summary of the BDD algorithm in ACL2

The BDD algorithm in ACL2 uses a combination of manipulation of IF
terms and unconditional rewriting.  In this discussion we begin with
some relevant mathematical theory.  This is followed by a description
of how ACL2 does BDDs, including concluding discussions of soundness,
completeness, and efficiency.

We recommend that you read the other documentation about BDDs in ACL2
before reading the rather technical material that follows.  See
BDD.

Here is an outline of our presentation.  Readers who want a user
perspective, without undue mathematical theory, may wish to skip to
Part (B), referring to Part (A) only on occasion if necessary.

(A) *Mathematical Considerations*

     (A1) BDD term order

     (A2) BDD-constructors and BDD terms, and their connection with
     aborting the BDD algorithm

     (A3) Canonical BDD terms

     (A4) A theorem stating the equivalence of provable and syntactic
     equality for canonical BDD terms

(B) *Algorithmic Considerations*

     (B1) BDD rules (rules used by the rewriting portion of the ACL2 BDD
     algorithm)

     (B2) Terms "known to be Boolean"

     (B3) An "IF-lifting" operation used by the algorithm, as well as an
     iterative version of that operation

     (B4) The ACL2 BDD algorithm

     (B5) Soundness and Completeness of the ACL2 BDD algorithm

     (B6) Efficiency considerations

(A) *Mathematical Considerations*

(A1) _BDD term order_

Our BDD algorithm creates a total "BDD term order" on ACL2 terms, on
the fly.  We use this order in our discussions below of IF-lifting and
of canonical BDD terms, and in the algorithm's use of commutativity.
The particular order is unimportant, except that we guarantee (for
purposes of commutative functions) that constants are smaller in this
order than non-constants.

(A2) _BDD-constructors_ (assumed to be '(cons)) and _BDD terms_

We take as given a list of function symbols that we call the
"BDD-constructors."  By default, the only BDD-constructor is cons,
although it is legal to specify any list of function symbols as the
BDD-constructors, either by using the acl2-defaults-table (see
ACL2-DEFAULTS-TABLE) or by supplying a :BDD-CONSTRUCTORS hint (see
HINTS).  Warning: this capability is largely untested and may
produce undesirable results.  Henceforth, except when explicitly stated
to the contrary, we assume that BDD-constructors is '(cons).

Roughly speaking, a BDD term is the sort of term produced by our BDD
algorithm, namely a tree with all cons nodes lying above all non-CONS
nodes.  More formally, a term is said to be a BDD term if it contains
*no* subterm of either of the following forms, where f is not CONS.

     (f ... (CONS ...) ...)

     (f ... 'x ...)  ; where (consp x) = t

We will see that whenever the BDD algorithm attempts to create a term
that is not a BDD term, it aborts instead.  Thus, whenever the
algorithm completes without aborting, it creates a BDD term.

(A3) _Canonical BDD terms_

We can strengthen the notion of "BDD term" to a notion of "canonical
BDD term" by imposing the following additional requirements, for every
subterm of the form (IF x y z):

     (a) x is a variable, and it precedes (in the BDD term order) every
     variable occurring in y or z;

     (b) y and z are syntactically distinct; and,

     (c) it is not the case that y is t and z is nil.

We claim that it follows easily from our description of the BDD
algorithm that every term it creates is a canonical BDD term, assuming
that the variables occurring in all such terms are treated by the
algorithm as being Boolean (see (B2) below) and that the terms contain
no function symbols other than IF and CONS.  Thus, under those
assumptions the following theorem shows that the BDD algorithm never
creates distinct terms that are provably equal, a property that is
useful for completeness and efficiency (as we explain in (B5) and (B6)
below).

(A4) _Provably equal canonical BDD terms are identical_

We believe that the following theorem and proof are routine extensions
of a standard result and proof to terms that allow calls of CONS.

*Theorem*.  Suppose that t1 and t2 are canonical BDD terms that contain
no function symbols other than IF and CONS.  Also suppose that (EQUAL
t1 t2) is a theorem.  Then t1 and t2 are syntactically identical.

Proof of theorem:  By induction on the total number of symbols
occurring in these two terms.  First suppose that at least one term is
a variable; without loss of generality let it be t1.  We must prove
that t2 is syntactically the same as t1.  Now it is clearly consistent
that (EQUAL t1 t2) is false if t2 is a call of CONS (to see this,
simply let t1 be an value that is not a CONSP).  Similarly, t2 cannot
be a constant or a variable other than t1.  The remaining possibility
to rule out is that t2 is of the form (IF t3 t4 t5), since by
assumption its function symbol must be IF or CONS and we have already
handled the latter case.  Since t2 is canonical, we know that t3 is a
variable.  Since (EQUAL t1 t2) is provable, i.e.,

     (EQUAL t1 (if t3 t4 t5))

is provable, it follows that we may substitute either t or nil for t3
into this equality to obtain two new provable equalities.  First,
suppose that t1 and t3 are distinct variables.  Then these
substitutions show that t1 is provably equal to both t4 and t5 (since
t3 does not occur in t4 or t5 by property (a) above, as t2 is
canonical), and hence t4 and t5 are provably equal to each other, which
implies by the inductive hypothesis that they are the same term -- and
this contradicts the assumption that t2 is canonical (property (b)).
Therefore t1 and t3 are the same variable, i.e., the equality displayed
above is actually (EQUAL t1 (if t1 t4 t5)).  Substituting t and then
nil for t1 into this provable equality lets us prove (EQUAL t t4) and
(EQUAL nil t5), which by the inductive hypothesis implies that t4 is
(syntactically) the term t and t5 is nil.  That is, t2 is (IF t1 t
nil), which contradicts the assumption that t2 is canonical (property
(c)).

Next, suppose that at least one term is a call of IF.  Our first
observation is that the other term is also a call of IF.  For if the
other is a call of CONS, then they cannot be provably equal, because
the former has no function symbols other than IF and hence is Boolean
when all its variables are assigned Boolean values.  Also, if the other
is a constant, then both branches of the IF term are provably equal to
that constant and hence these branches are syntactically identical by
the inductive hypothesis, contradicting property (b).  Hence, we may
assume for this case that both terms are calls of IF; let us write them
as follows.

     t0:  (IF t1 t2 t3)
     u0:  (IF u1 u2 u3)

Note that t1 and u1 are variables, by property (a) of canonical BDD
terms.  First we claim that t1 does not strictly precede u1 in the BDD
term order.  For suppose t1 does strictly precede u1.  Then property
(a) of canonical BDD terms guarantees that t1 does not occur in u0.
Hence, an argument much like one used above shows that u0 is provably
equal to both t2 (substituting t for t1) and t3 (substituting nil for
t1), and hence t2 and t3 are provably equal.  That implies that they
are identical terms, by the inductive hypothesis, which then
contradicts property (b) for t0.  Similarly, u1 does not strictly
precede t1 in the BDD term order.  Therefore, t1 and u1 are the same
variable.  By substituting t for this variable we see that t2 and u2
are provably equal, and hence they are equal by the inductive
hypothesis.  Similarly, by substituting nil for t1 (and u1) we see that
t3 and u3 are provably, hence syntactically, equal.

We have covered all cases in which at least one term is a variable or
at least one term is a call of IF.  If both terms are constants, then
provable and syntactic equality are clearly equivalent.  Finally, then,
we may assume that one term is a call of CONS and the other is a
constant or a call of CONS.  The constant case is similar to the CONS
case if the constant is a CONSP, so we omit it; while if the constant
is not a CONSP then it is not provably equal to a call of CONS; in fact
it is provably _not_ equal!

So, we are left with a final case, in which canonical BDD terms (CONS
t1 t2) and (CONS u1 u2) are provably equal, and we want to show that t1
and u1 are syntactically equal as are t2 and u2.  These conclusions are
easy consequences of the inductive hypothesis, since the ACL2 axiom
CONS-EQUAL (which you can inspect using :PE) shows that equality of the
given terms is equivalent to the conjunction of (EQUAL t1 t2) and
(EQUAL u1 u2).  Q.E.D.

(B) *Algorithmic Considerations*

(B1) _BDD rules_

A rule of class :rewrite (see RULE-CLASSES) is said to be a
"BDD rewrite rule" if and only if it satisfies the following criteria.
(1) The rule is enabled.  (2) Its equivalence relation is equal.  (3)
It has no hypotheses.  (4) Its :loop-stopper field is nil, i.e., it is
not a permutative rule.  (5) All variables occurring in the rule occur
in its left-hand side (i.e., there are no "free variables"; see
REWRITE).  A rule of class :definition (see RULE-CLASSES) is
said to be a "BDD definition rule" if it satisfies all the criteria
above (except (4), which does not apply), and moreover the top function
symbol of the left-hand side was not recursively (or mutually
recursively) defined.  Technical point:  Note that this additional
criterion is independent of whether or not the indicated function
symbol actually occurs in the right-hand side of the rule.

Both BDD rewrite rules and BDD definition rules are said to be "BDD
rules."

(B2) _Terms "known to be Boolean"_

We apply the BDD algorithm in the context of a top-level goal to prove,
namely, the goal at which the :BDD hint is attached.  As we run the BDD
algorithm, we allow ourselves to say that a set of terms is "known to
be Boolean" if we can verify that the goal is provable from the
assumption that at least one of the terms is not Boolean.
Equivalently, we allow ourselves to say that a set of terms is "known
to be Boolean" if we can verify that the original goal is provably
equivalent to the assertion that if all terms in the set are Boolean,
then the goal holds.  The notion "known to be Boolean" is conservative
in the sense that there are generally sets of terms for which the above
equivalent criteria hold and yet the sets of terms are not noted as as
being "known to be Boolean."  However, ACL2 uses a number of tricks,
including type-set reasoning and analysis of the structure of the
top-level goal, to attempt to establish that a sufficiently inclusive
set of terms is known to be Boolean.

From a practical standpoint, the algorithm determines a set of terms
known to be Boolean; we allow ourselves to say that each term in this
set is "known to be Boolean."  The algorithm assumes that these terms
are indeed Boolean, and can make use of that assumption.  For example,
if t1 is known to be Boolean then the algorithm simplifies (IF t1 t
nil) to t1; see (iv) in the discussion immediately below.

(B3) _IF-lifting_ and the _IF-lifting-for-IF loop_

Suppose that one has a term of the form (f ... (IF test x y) ...),
where f is a function symbol other than CONS.  Then we say that
"IF-lifting" test "from" this term produces the following term, which
is provably equal to the given term.

     (if test
         (f ... x ...)  ; resulting true branch
         (f ... y ...)) ; resulting false branch

Here, we replace each argument of f of the form (IF test .. ..), for
the same test, in the same way.  In this case we say that "IF-lifting
applies to" the given term, "yielding the test" test and with the
"resulting two branches" displayed above.  Whenever we apply
IF-lifting, we do so for the available test that is least in the BDD
term order (see (A1) above).

We consider arguments v of f that are "known to be Boolean" (see above)
to be replaced by (IF v t nil) for the purposes of IF-lifting, i.e.,
before IF-lifting is applied.

There is one special case, however, for IF-lifting.  Suppose that the
given term is of the form (IF v y z) where v is a variable and is the
test to be lifted out (i.e., it is least in the BDD term order among
the potential tests).  Moroever, suppose that neither y nor z is of the
form (IF v W1 W2) for that same v.  Then IF-lifting does not apply to
the given term.

We may now describe the IF-lifting-for-IF loop, which applies to terms
of the form (IF test tbr fbr) where the algorithm has already produced
test, tbr, and fbr.  First, if test is nil then we return fbr, while if
test is a non-nil constant or a call of CONS then we return tbr.
Otherwise, we see if IF-lifting applies.  If IF-lifting does not apply,
then we return (IF test tbr fbr).  Otherwise, we apply IF-lifting to
obtain a term of the form (IF x y z), by lifting out the appropriate
test.  Now we recursively apply the IF-lifting-for-IF loop to the term
(IF x y z), unless any of the following special cases apply.

     (i) If y and z are the same term, then return y.

     (ii) Otherwise, if x and z are the same term, then replace z by
     nil before recursively applying IF-lifting-for-IF.

     (iii) Otherwise, if x and y are the same term and y is known to be
     Boolean, then replace y by t before recursively applying
     IF-lifting-for-IF.

     (iv) If z is nil and either x and y are the same term or x is
     "known to be Boolean" and y is t, then return x.

NOTE:  When a variable x is known to be Boolean, it is easy to see that
the form (IF x t nil) is always reduced to x by this algorithm.

(B4) _The ACL2 BDD algorithm_

We are now ready to present the BDD algorithm for ACL2.  It is given an
ACL2 term, x, as well as an association list va that maps variables to
terms, including all variables occurring in x.  We maintain the
invariant that whenever a variable is mapped by va to a term, that term
has already been constructed by the algorithm, except:  initially va
maps every variable occurring in the top-level term to itself.  The
algorithm proceeds as follows.  We implicitly ordain that whenever the
BDD algorithm attempts to create a term that is not a BDD term (as
defined above in (A2)), it aborts instead.  Thus, whenever the
algorithm completes without aborting, it creates a BDD term.

     If x is a variable, return the result of looking it up in va.

     If x is a constant, return x.

     If x is of the form (IF test tbr fbr), then first run the
     algorithm on test with the given va to obtain test'.  If test' is
     nil, then return the result fbr' of running the algorithm on fbr
     with the given va.  If test' is a constant other than nil, or is a
     call of CONS, then return the result tbr' of running the algorithm
     on tbr with the given va.  If tbr is identical to fbr, return tbr.
     Otherwise, return the result of applying the IF-lifting-for-IF
     loop (described above) to the term (IF test' tbr' fbr').

     If x is of the form (IF* test tbr fbr), then compute the result
     exactly as though IF were used rather than IF*, except that if
     test' is not a constant or a call of CONS (see paragraph above),
     then abort the BDD computation.  Informally, the tests of IF*
     terms are expected to "resolve."  NOTE:  This description shows
     how IF* can be used to implement conditional rewriting in the BDD
     algorithm.

     If x is a LAMBDA expression ((LAMBDA vars body) . args) (which
     often corresponds to a LET term; see LET), then first form
     an alist va' by binding each v in vars to the result of running
     the algorithm on the corresponding member of args, with the
     current alist va.  Then, return the result of the algorithm on
     body in the alist va'.

     Otherwise, x is of the form (f x1 x2 ... xn), where f is a
     function symbol other than IF or IF*.  In that case, let xi' be
     the result of running the algorithm on xi, for i from 1 to n,
     using the given alist va.  First there are a few special cases.
     If f is EQUAL then we return t if x1' is syntactically identical
     to x2' (where this test is very fast; see (B6) below); we return
     x1' if it is known to be Boolean and x2' is t; and similarly, we
     return x2' if it is known to be Boolean and x1' is t.  Next, if
     each xi' is a constant and the :executable-counterpart of f is
     enabled, then the result is obtained by computation.  Next, if f
     is BOOLEANP and x1' is known to be Boolean, t is returned.
     Otherwise, we proceed as follows, first possibly swapping the
     arguments if they are out of (the BDD term) order and if f is
     known to be commutative (see below).  If a BDD rewrite rule (as
     defined above) matches the term (f x1'... xn'), then the most
     recently stored such rule is applied.  If there is no such match
     and f is a BDD-constructor, then we return (f x1'... xn').
     Otherwise, if a BDD definition rule matches this term, then the
     most recently stored such rule (which will usually be the original
     definition for most users) is applied.  If none of the above
     applies and neither does IF-lifting, then we return (f x1'...
     xn').  Otherwise we apply IF-lifting to (f x1'... xn') to obtain a
     term (IF test tbr fbr); but we aren't done yet.  Rather, we run
     the BDD algorithm (using the same alist) on tbr and fbr to obtain
     terms tbr' and fbr', and we return (IF test tbr' fbr') unless tbr'
     is syntactically identical to fbr', in which case we return tbr'.

When is it the case that, as said above, "f is known to be
commutative"?  This happens when an enabled rewrite rule is of the form
(EQUAL (f X Y) (f Y X)).  Regarding swapping the arguments in that
case:  recall that we may assume very little about the BDD term order,
essentially only that we swap the two arguments when the second is a
constant and the first is not, for example, in (+ x 1).  Other than
that situation, one cannot expect to predict accurately when the
arguments of commutative operators will be swapped.

(B5) Soundness and Completeness of the ACL2 BDD algorithm

Roughly speaking, "soundness" means that the BDD algorithm should give
correct answers, and "completeness" means that it should be powerful
enough to prove all true facts.  Let us make the soundness claim a
little more precise, and then we'll address completeness under suitable
hypotheses.

*Claim* (Soundness).  If the ACL2 BDD algorithm runs to completion on
an input term t0, then it produces a result that is provably equal to
t0.

We leave the proof of this claim to the reader.  The basic idea is
simply to check that each step of the algorithm preserves the meaning
of the term under the bindings in the given alist.

Let us start our discussion of completeness by recalling the theorem
proved above in (A4).

*Theorem*.  Suppose that t1 and t2 are canonical BDD terms that contain
no function symbols other than IF and CONS.  Also suppose that (EQUAL
t1 t2) is a theorem.  Then t1 and t2 are syntactically identical.

Below we show how this theorem implies the following completeness
property of the ACL2 BDD algorithm.  We continue to assume that CONS is
the only BDD-constructor.

*Claim* (Completeness).  Suppose that t1 and t2 are provably equal
terms, under the assumption that all their variables are known to be
Boolean.  Assume further that under this same assumption, top-level
runs of the ACL2 BDD algorithm on these terms return terms that contain
only the function symbols IF and CONS.  Then the algorithm returns the
same term for both t1 and t2, and the algorithm reduces (EQUAL t1 t2)
to t.

Why is this claim true?  First, notice that the second part of the
conclusion follows immediately from the first, by definition of the
algorithm.  Next, notice that the terms u1 and u2 obtained by running
the algorithm on t1 and t2, respectively, are provably equal to t1 and
t2, respectively, by the Soundness Claim.  It follows that u1 and u2
are provably equal to each other.  Since these terms contain no
function symbols other than IF or CONS, by hypothesis, the Claim now
follows from the Theorem above together with the following lemma.

*Lemma*.  Suppose that the result of running the ACL2 BDD algorithm on
a top-level term t0 is a term u0 that contains only the function
symbols IF and CONS, where all variables of t0 are known to be Boolean.
Then u0 is a canonical BDD term.

Proof:  left to the reader.  Simply follow the definition of the
algorithm, with a separate argument for the IF-lifting-for-IF loop.

Finally, let us remark on the assumptions of the Completeness Claim
above.  The assumption that all variables are known to be Boolean is
often true; in fact, the system uses the forward-chaining rule
boolean-listp-forward (you can see it using :pe) to try to establish
this assumption, if your theorem has a form such as the following.

     (let ((x (list x0 x1 ...))
           (y (list y0 y1 ...)))
       (implies (and (boolean-listp x)
                     (boolean-listp y))
                ...))

Moreover, the :BDD hint can be used to force the prover to abort if it
cannot check that the indicated variables are known to be Boolean; see
HINTS.

Finally, consider the effect in practice of the assumption that the
terms resulting from application of the algorithm contain calls of IF
and CONS only.  Typical use of BDDs in ACL2 takes place in a theory
(see THEORIES) in which all relevant non-recursive function
symbols are enabled and all recursive function symbols possess enabled
BDD rewrite rules that tell them how open up.  For example, such a rule
may say how to expand on a given function call's argument that has the
form (CONS a x), while another may say how to expand when that argument
is nil).  (See for example the rules append-cons and append-nil in the
documentation for IF*.)  We leave it to future work to formulate a
theorem that guarantees that the BDD algorithm produces terms
containing calls only of IF and CONS assuming a suitably "complete"
collection of rewrite rules.

(B6) _Efficiency considerations_

Following Bryant's algorithm, we use a graph representation of terms
created by the BDD algorithm's computation.  This representation enjoys
some important properties.

     (Time efficiency) The test for syntactic equality of BDD terms is
     very fast.

     (Space efficiency) Equal BDD data structures are stored identically
     in memory.

_Implementation note._  The representation actually uses a sort of hash
table for BDD terms that is implemented as an ACL2 1-dimensional array.
See ARRAYS.  In addition, we use a second such hash table to
avoid recomputing the result of applying a function symbol to the
result of running the algorithm on its arguments.  We believe that
these uses of hash tables are standard.  They are also discussed in
Moore's paper on BDDs; see BDD for the reference.

BDD-INTRODUCTION    examples illustrating the use of BDDs in ACL2

See BDD for a brief introduction to BDDs in ACL2 and for
pointers to other documentation on BDDs in ACL2.  Here, we illustrate
the use of BDDs in ACL2 by way of some examples.  For a further
example, see IF*.

Let us begin with a really simple example.  (We will explain the :bdd
hint (:vars nil) below.)

     ACL2 !>(thm (equal (if a b c) (if (not a) c b))
                 :hints (("Goal" :bdd (:vars nil)))) ; Prove with BDDs

     [Note:  A hint was supplied for our processing of the goal above.
     Thanks!]

     But simplification with BDDs (7 nodes) reduces this to T, using the
     :definitions EQUAL and NOT.

     Q.E.D.

     Summary
     Form:  ( THM ...)
     Rules: ((:DEFINITION EQUAL) (:DEFINITION NOT))
     Warnings:  None
     Time:  0.18 seconds (prove: 0.05, print: 0.02, other: 0.12)

     Proof succeeded.
     ACL2 !>

The :bdd hint (:vars nil) indicates that BDDs are to be used on the
indicated goal, and that any so-called "variable ordering" may be used:
ACL2 may use a convenient order that is far from optimal.  It is
beyond the scope of the present documentation to address the issue of
how the user may choose good variable orderings.  Someday our
implementation of BDDs may be improved to include heuristically-chosen
variable orderings rather than rather random ones.

Here is a more interesting example.

     (defun v-not (x)
     ; Complement every element of a list of Booleans.
       (if (consp x)
           (cons (not (car x)) (v-not (cdr x)))
         nil))

     ; Now we prove a rewrite rule that explains how to open up v-not on
     ; a consp.
     (defthm v-not-cons
       (equal (v-not (cons x y))
              (cons (not x) (v-not y))))

     ; Finally, we prove for 7-bit lists that v-not is self-inverting.
     (thm
      (let ((x (list x0 x1 x2 x3 x4 x5 x6)))
        (implies (boolean-listp x)
                 (equal (v-not (v-not x)) x)))
      :hints (("Goal" :bdd
                      ;; Note that this time we specify a variable order.
                      (:vars (x0 x1 x2 x3 x4 x5 x6)))))

It turns out that the variable order doesn't seem to matter in this
example; using several orders we found that 30 nodes were created, and
the proof time was about 1/10 of a second on a (somewhat enhanced)
Sparc 2.  The same proof took about a minute and a half without any
:bdd hint!  This observation is a bit misleading perhaps, since the
theorem for arbitrary x,

     (thm
      (implies (boolean-listp x)
               (equal (v-not (v-not x)) x)))

only takes about 1.5 times as long as the :bdd proof for 7 bits, above!
Nevertheless, BDDs can be very useful in reducing proof time,
especially when there is no regular structure to facilitate proof by
induction, or when the induction scheme is so complicated to construct
that significant user effort is required to get the proof by induction
to go through.

Finally, consider the preceding example, with a :bdd hint of (say)
(:vars nil), but with the rewrite rule v-not-cons above disabled.  In
that case, the proof fails, as we see below.  That is because the BDD
algorithm in ACL2 uses hypothesis-free :rewrite rules,
:executable-counterparts, and nonrecursive definitions, but it does not
use recursive definitions.

Notice that when we issue the (show-bdd) command, the system's response
clearly shows that we need a rewrite rule for simplifying terms of the
form (v-not (cons ...)).

     ACL2 !>(thm
             (let ((x (list x0 x1 x2 x3 x4 x5 x6)))
               (implies (boolean-listp x)
                        (equal (v-not (v-not x)) x)))
             :hints (("Goal" :bdd (:vars nil)
                      :in-theory (disable v-not-cons))))

     [Note:  A hint was supplied for our processing of the goal above.
     Thanks!]

     ACL2 Error in ( THM ...):  Attempted to create V-NOT node during BDD
     processing with an argument that is a call of a bdd-constructor,
     which would produce a non-BDD term (as defined in :DOC
     bdd-algorithm).  See :DOC show-bdd.

     Summary
     Form:  ( THM ...)
     Rules: NIL
     Warnings:  None
     Time:  0.58 seconds (prove: 0.13, print: 0.00, other: 0.45)

     ******** FAILED ********  See :DOC failure  ******** FAILED ********
     ACL2 !>(show-bdd)

     BDD computation on Goal yielded 17 nodes.
     ==============================

     BDD computation was aborted on Goal, and hence there is no
     falsifying assignment that can be constructed.  Here is a backtrace
     of calls, starting with the top-level call and ending with the one
     that led to the abort.  See :DOC show-bdd.

     (LET ((X (LIST X0 X1 X2 X3 X4 X5 ...)))
          (IMPLIES (BOOLEAN-LISTP X)
                   (EQUAL (V-NOT (V-NOT X)) X)))
       alist: ((X6 X6) (X5 X5) (X4 X4) (X3 X3) (X2 X2) (X1 X1) (X0 X0))

     (EQUAL (V-NOT (V-NOT X)) X)
       alist: ((X (LIST X0 X1 X2 X3 X4 X5 ...)))

     (V-NOT (V-NOT X))
       alist: ((X (LIST X0 X1 X2 X3 X4 X5 ...)))

     (V-NOT X)
       alist: ((X (LIST X0 X1 X2 X3 X4 X5 ...)))
     ACL2 !>

The term that has caused the BDD algorithm to abort is thus (V-NOT X),
where X has the value (LIST X0 X1 X2 X3 X4 X5 ...), i.e., (CONS X0
(LIST X1 X2 X3 X4 X5 ...)).  Thus, we see the utility of introducing a
rewrite rule to simplify terms of the form (V-NOT (CONS ...)).  The
moral of this story is that if you get an error of the sort shown
above, you may find it useful to execute the command (show-bdd) and use
the result as advice that suggests the left hand side of a rewrite rule.

Here is another sort of failed proof.  In this version we have omitted
the hypothesis that the input is a bit vector.  Below we use show-bdd
to see what went wrong, and use the resulting information to construct
a counterexample.  This failed proof corresponds to a slightly modified
input theorem, in which x is bound to the 4-element list (list x0 x1 x2
x3).

     ACL2 !>(thm
             (let ((x (list x0 x1 x2 x3)))
               (equal (v-not (v-not x)) x))
             :hints (("Goal" :bdd
                      ;; This time we do not specify a variable order.
                      (:vars nil))))

     [Note:  A hint was supplied for our processing of the goal above.
     Thanks!]

     ACL2 Error in ( THM ...):  The :BDD hint for the current goal has
     successfully simplified this goal, but has failed to prove it.
     Consider using (SHOW-BDD) to suggest a counterexample; see :DOC
     show-bdd.

     Summary
     Form:  ( THM ...)
     Rules: NIL
     Warnings:  None
     Time:  0.18 seconds (prove: 0.07, print: 0.00, other: 0.12)

     ******** FAILED ********  See :DOC failure  ******** FAILED ********
     ACL2 !>(show-bdd)

     BDD computation on Goal yielded 73 nodes.
     ==============================

     Falsifying constraints:
     ((X0 "Some non-nil value")
      (X1 "Some non-nil value")
      (X2 "Some non-nil value")
      (X3 "Some non-nil value")
      ((EQUAL 'T X0) T)
      ((EQUAL 'T X1) T)
      ((EQUAL 'T X2) T)
      ((EQUAL 'T X3) NIL))

     ==============================

     Term obtained from BDD computation on Goal:

     (IF X0
         (IF X1
             (IF X2 (IF X3 (IF # # #) (IF X3 # #))
                 (IF X2 'NIL (IF X3 # #)))
             (IF X1 'NIL
                 (IF X2 (IF X3 # #) (IF X2 # #))))
         (IF X0 'NIL
             (IF X1 (IF X2 (IF X3 # #) (IF X2 # #))
                 (IF X1 'NIL (IF X2 # #)))))

     ACL2 Query (:SHOW-BDD):  Print the term in full?  (N, Y, W or ?):
     n ; I've seen enough.  The assignment shown above suggests
       ; (though not conclusively) that if we bind x3 to a non-nil
       ; value other than T, and bind x0, x1, and x2 to t, then we
       ; this may give us a counterexample.
     ACL2 !>(let ((x0 t) (x1 t) (x2 t) (x3 7))
              (let ((x (list x0 x1 x2 x3)))
                ;; Let's use LIST instead of EQUAL to see how the two
                ;; lists differ.
                (list (v-not (v-not x)) x)))
     ((T T T T) (T T T 7))
     ACL2 !>

See IF* for another example.

IF*    for conditional rewriting with BDDs

The function IF* is defined to be IF, but it is used in a special way
by ACL2's BDD package.

As explained elsewhere (see BDD-ALGORITHM), ACL2's BDD
algorithm gives special treatment to terms of the form (IF* TEST TBR
FBR).  In such cases, the algorithm simplifies TEST first, and the
result of that simplification must be a constant (normally t or nil,
but any non-nil explicit value is treated like t here).  Otherwise, the
algorithm aborts.

Thus, IF* may be used to implement a sort of conditional rewriting for
ACL2's BDD package, even though this package only nominally supports
unconditional rewriting.  The following contrived example should make
this point clear.

Suppose that we want to prove that (nthcdr (length x) (append x y)) is
equal to y, but that we would be happy to prove this only for lists
having length 4.  We can state such a theorem as follows.

     (let ((x (list x0 x1 x2 x3)))
       (equal (nthcdr (length x) (append x y))
              y))

If we want to prove this formula with a :BDD hint, then we need to have
appropriate rewrite rules around.  First, note that LENGTH is defined
as follows (try :PE LENGTH):

     (length x)
      =
     (if (stringp x)
         (len (coerce x 'list))
         (len x))

Since BDD-based rewriting is merely very simple unconditional rewriting
(see BDD-ALGORITHM), we expect to have to prove a rule reducing
STRINGP of a CONS:

     (defthm stringp-cons
       (equal (stringp (cons x y))
              nil))

Now we need a rule to compute the LEN of X, because the definition of
LEN is recursive and hence not used by the BDD package.

     (defthm len-cons
       (equal (len (cons a x))
              (1+ (len x))))

We imagine this rule simplifying (LEN (LIST X0 X1 X2 X3)) in terms of
(LEN (LIST X1 X2 X3)), and so on, and then finally (LEN nil) should be
computed by execution (see BDD-ALGORITHM).

We also need to imagine simplifying (APPEND X Y), where still X is
bound to (LIST X0 X1 X2 X3).  The following two rules suffice for this
purpose (but are needed, since APPEND, actually BINARY-APPEND, is
recursive).

     (defthm append-cons
       (equal (append (cons a x) y)
              (cons a (append x y))))

     (defthm append-nil
       (equal (append nil x)
              x))

Finally, we imagine needing to simplify calls of NTHCDR, where the the
first argument is a number (initially, the length of (LIST X0 X1 X2
X3), which is 4).  The second lemma below is the traditional way to
accomplish that goal (when not using BDDs), by proving a conditional
rewrite rule.  (The first lemma is only proved in order to assist in
the proof of the second lemma.)

     (defthm fold-constants-in-+
       (implies (and (syntaxp (quotep x))
                     (syntaxp (quotep y)))
                (equal (+ x y z)
                       (+ (+ x y) z))))

     (defthm nthcdr-add1-conditional
       (implies (not (zp (1+ n)))
                (equal (nthcdr (1+ n) x)
                       (nthcdr n (cdr x)))))

The problem with this rule is that its hypothesis makes it a
conditional rewrite rule, and conditional rewrite rules are not used by
the BDD package.  (See BDD-ALGORITHM for a discussion of "BDD
rules.")  (Note that the hypothesis cannot simply be removed; the
resulting formula would be false for n = -1 and x = '(a), for example.)
We can solve this problem by using IF*, as follows; comments follow.

     (defthm nthcdr-add1
       (equal (nthcdr (+ 1 n) x)
              (if* (zp (1+ n))
                   x
                   (nthcdr n (cdr x)))))

How is nthcdr-add1 applied by the BDD package?  Suppose that the BDD
computation encounters a term of the form (NTHCDR (+ 1 N) X).  Then the
BDD package will apply the rewrite rule nthcdr-add1.  The first thing
it will do when attempting to simplify the right hand side of that rule
is to attempt to simplify the term (ZP (1+ N)).  If N is an explicit
number (which is the case in the scenario we envision), this test will
reduce (assuming the executable counterparts of ZP and BINARY-+ are
enabled) to t or to nil.  In fact, the lemmas above (not including the
lemma nthcdr-add1-conditional) suffice to prove our goal:

     (thm (let ((x (list x0 x1 x2 x3)))
            (equal (nthcdr (length x) (append x y))
                   y))
          :hints (("Goal" :bdd (:vars nil))))

If we execute the following form that disables the definition and
executable counterpart of the function ZP

     (in-theory (disable zp (zp)))

before attempting the proof of the theorem above, we can see more
clearly the point of using IF*.  In this case, the prover makes the
following report.

     ACL2 Error in ( THM ...):  Unable to resolve test of IF* for term

     (IF* (ZP (+ 1 N)) X (NTHCDR N (CDR X)))

     under the bindings

     ((X (CONS X0 (CONS X1 (CONS X2 #)))) (N '3))

     -- use SHOW-BDD to see a backtrace.

If we follow the advice above, we can see rather clearly what happened.
See SHOW-BDD.

     ACL2 !>(show-bdd)

     BDD computation on Goal yielded 21 nodes.
     ==============================

     BDD computation was aborted on Goal, and hence there is no
     falsifying assignment that can be constructed.  Here is a backtrace
     of calls, starting with the top-level call and ending with the one
     that led to the abort.  See :DOC show-bdd.

     (LET ((X (LIST X0 X1 X2 X3)))
          (EQUAL (NTHCDR (LENGTH X) (APPEND X Y)) Y))
       alist: ((Y Y) (X3 X3) (X2 X2) (X1 X1) (X0 X0))

     (NTHCDR (LENGTH X) (APPEND X Y))
       alist: ((X (LIST X0 X1 X2 X3)) (Y Y))

     (IF* (ZP (+ 1 N)) X (NTHCDR N (CDR X)))
       alist: ((X (LIST* X0 X1 X2 X3 Y)) (N 3))
     ACL2 !>

Each of these term-alist pairs led to the next, and the test of the
last one, namely (ZP (+ 1 N)) where N is bound to 3, was not simplified
to t or to nil.

What would have happened if we had used IF in place of IF* in the rule
nthcdr-add1?  In that case, if ZP and its executable counterpart were
disabled then we would be put into an infinite loop!  For, each time a
term of the form (NTHCDR k V) is encountered by the BDD package (where
k is an explicit number), it will be rewritten in terms of (NTHCDR k-1
(CDR V)).  We would prefer that if for some reason the term (ZP (+ 1
N)) cannot be decided to be t or to be nil, then the BDD computation
should simply abort.

Even if there were no infinite loop, this kind of use of IF* is useful
in order to provide feedback of the form shown above whenever the test
of an IF term fails to simplify to t or to nil.

SHOW-BDD    inspect failed BDD proof attempts

Attempts to use BDDs (see BDD), using :bdd hints, can fail for
various reasons.  Sometimes it is useful to explore such failures.  To
do so, one may simply execute the form

     (show-bdd)

inside the ACL2 loop.  The system's response is generally
self-explanatory.  Perhaps you have already seen show-bdd used in some
examples (see BDD-INTRODUCTION and see IF*).  Here we
give some details about show-bdd.

(Show-bdd) prints the goal to which the BDD procedure was applied and
reports the number of nodes created during the BDD computation,
followed by additional information depending on whether or not the
computation ran to completion or aborted (for reasons explained
elsewhere; see BDD-ALGORITHM).  If the computation did abort, a
backtrace is printed that should be useful in understanding where the
problem lies.  Otherwise, (show-bdd) prints out "falsifying
constraints."  This list of pairs associates terms with values and
suggests how to construct a binding list for the variables in the
conjecture that will falsify the conjecture.  It also prints out the
term that is the result of simplifying the input term.  In each of
these cases, parts of the object may be hidden during printing, in
order to avoid creating reams of uninteresting output.  If so, the user
will be queried about whether he wishes to see the entire object (alist
or term), which may be quite large.  The following responses are legal:

       w -- Walk around the object with a structure editor

     t -- Print the object in full

     nil -- Do not print any more of the object

Show-bdd actually has four optional arguments, probably rarely used.
The general form is

     (show-bdd goal-name goal-ans falsifying-ans term-ans)

where goal-name is the name of the goal on which the :bdd hint was used
(or, nil if the system should find such a goal), goal-ans is the answer
to be used in place of the query for whether to print the input goal in
full, falsifying-ans is the answer to be used in place of the query for
whether to print the falsifying constraints in full, and term-ans is
the answer to be used in place of the query for whether to print the
resulting term in full.

BOOKS    files of ACL2 event forms

This documentation topic is about ACL2 input files.  However, there are
two traditional (paper) books published about ACL2: a textbook and a
case studies book.  Further information on those two paper books is
available by following links from the ACL2 home page,
`http://www.cs.utexas.edu/users/moore/acl2/'.

A "book" is a file of ACL2 events that have been certified as
admissible.  Using include-book you can construct a new logical world
by assuming the events in any number of mutually compatible books.
Relevant documented topics are listed below.  Following this list is a
"guided tour" through the topics.

You can contribute books to the ACL2 community and obtain updates
inbetween ACL2 releases by visiting the acl2-books project web page,
`http://acl2-books.googlecode.com/'.

Related topics other than immediate subtopics:

_Introduction._

A "book" is a file of ACL2 forms.  Books are prepared entirely by the
user of the system, i.e., they are "source" files not "object" files.
Some of the forms in a book are marked local and the others are
considered "non-local."

Include-book lets you load a book into any ACL2 world.  If completed
without error, the inclusion of a book extends the logic of the host
world by the addition of just the non-local events in the book.  You
may extend the world by successively including a variety of books to
obtain the desired collection of definitions and rules.  Unless name
conflicts occur (which are detected and signalled) inclusion of a book
is consistency preserving provided the book itself is consistent as
discussed later.  However, include-book merely assumes the validity of
the events in a book; if you include a book that contains an
inconsistency (e.g., an inadmissible definition) then the resulting
theory is inconsistent.

It is possible to "certify" a book, with certify-book, guaranteeing
that the error-free inclusion of the certified forms will produce a
consistent extension of a consistent logic.  Certification processes
both the local and non-local forms, so you can mark as local those
events you need for certification that you want to hide from users of
the book (e.g., hacks, crocks, and kludges on the way to a good set of
:rewrite rules).  Certification can also "compile" a book, thereby
speeding up the execution of the functions defined within it.  The
desire to compile books is largely responsible for the restrictions we
put on the forms allowed in books.

Extensive documentation is available on the various aspects of books.
We recommend that you read it all before using books.  It has been
written so as to make sense when read in a certain linear sequence,
called the "guided tour", though in general you may browse through it
randomly.  If you are on the guided tour, you should next read the
documentation on book-example (see BOOK-EXAMPLE).

BOOK-COMPILED-FILE    creating and loading of compiled and expansion files for books

An effect of compilation is to speed up the execution of the functions
defined wit a the book.  Compilation can also remove tail recursion,
thus avoiding stack overflows.  The presence of compiled code for the
functions in the book should not otherwise affect the performance of
ACL2.  See GUARD for a discussion; also See COMPILATION.

By default, the certify-book command compiles the book that it
certifies.  see CERTIFY-BOOK for how to control this behavior.

By default, the include-book command loads the compiled file for the
book.  The details of how this loading works are subtle, and do not
need to be understood by most users.  The ACL2 source code contains an
"Essay on Hash Table Support for Compilation" that explains such
details for those interested.  All that users should generally need to
know about this is that the compiled file is always the result of
compiling a so-called "expansion file", which contains certain
additional code besides the book itself.  The relevance to users of the
expansion file is that it can be loaded if the compiled file is missing
(except when :load-compiled-file t is specified by the include-book
form), and its existence is required in order for include-book to
create a book's compiled file, as described below.

Most users can skip the remainder of this documentation topic, which
addresses the uncommon activity of using include-book to compile books.

Include-book can be made to compile a book by supplying its keyword
argument :load-compiled-file the value :comp.  However, a compiled file
can only be produced if there is already an _expansion file_ that is at
least as recent as the book's certificate.  Such a file, whose name
happens to be the result of concatenating the string "@expansion.lsp"
to the book name (without the ".lisp" suffix), is created by
certify-book when state global variable 'save-expansion-file has a
non-nil value.  That will be the case if ACL2 started up when
environment variable ACL2_SAVE_EXPANSION was t (or any value that is
not the empty string and whose string-upcase is not "NIL"), until the
time (if any) that 'save-expansion-file is assigned a different value by
the user.  In most respects, the :comp setting is treated exactly the
same as :warn; but after all events in the book are processed, the
expansion file is compiled if a compiled file was not loaded, after
which the resulting compiled file is loaded.

One can thus, for example, compile the distributed books for several
different host Lisps -- useful when installing ACL2 executables at the
same site that are built on different host Lisps.  A convenient way to
do this in an environment that provides Gnu make is to certify books
using the shell command "make regression" in the acl2-sources/
directory, after setting environment variable ACL2_SAVE_EXPANSION to t,
and then moving to the books directory and executing the appropriate
make commands to compile the books (targets fasl, o, and so on,
according to the compiled file extension for the host Lisp).

We conclude by saying more about the :load-compiled-file argument of
include-book.  We assume that state global 'compiler-enabled has a
non-nil value; otherwise :load-compiled-file is always treated as nil.

We do not consider raw mode below (see SET-RAW-MODE), which
presents a special case: ACL2 will attempt to load the book itself
whenever it would otherwise load the expansion or compiled file, but
cannot (either because the :load-compiled-file argument is nil, or for
each of the expansion and compiled files, either it does not exist or
it is out of date with respect to the .cert file).

The :load-compiled-file argument is not recursive: calls of
include-book that are inside the book supplied to include-book use
their own :load-compiled-file arguments.  However, those subsidiary
include-book calls can nevertheless be sensitive to the
:load-compiled-file arguments of enclosing include-book calls, as
follows.  If :load-compiled-file has value t, then every subsidiary
include-book is required to load a compiled file.  Moreover, if a book's
compiled file or expansion file is loaded in raw Lisp, then an attempt
will be made to load the compiled file or expansion file for any
include-book form encountered during that load.  If that attempt fails,
then that load immediately aborts, as does its parent load, and so on
up the chain.  If, when going up the chain, an include-book is aborted
for which keyword argument :load-compiled-file has value t, then an
error occurs.

When loading a book's compiled file or expansion file, FILE, it is
possible to encounter an include-book form for a book that has no
suitable compiled file or expansion file.  In that case, the load of
FILE is aborted at that point.  Similarly, the load of FILE is aborted
in the case that this include-book form has a suitable compiled file or
expansion file whose load is itself aborted.  Thus, whenever any
include-book aborts, so do all of its parent include-books, up the
chain.  Such an abort causes an error when the include-book form
specifies a :load-compiled-file value of t.

BOOK-CONTENTS    restrictions on the forms inside books

     Example Book:

     ; This book defines my app function and the theorem that it is
     ; associative.  One irrelevant help lemma is proved first but
     ; it is local and so not seen by include-book.  I depend on the
     ; inferior book "weird-list-primitives" from which I get
     ; definitions of hd and tl.

     (in-package "MY-PKG")

     (include-book "weird-list-primitives")

     (defun app (x y) (if (consp x) (cons (hd x) (app (tl x) y)) y))

     (local
      (defthm help-lemma
        (implies (true-listp x) (equal (app x nil) x))))

     (defthm app-is-associative
       (equal (app (app a b) c) (app a (app b c))))

The first form in a book must be (in-package "pkg") where "pkg" is some
package name known to ACL2 whenever the book is certified.  The rest of
the forms in a book are embedded event forms, i.e., defuns, defthms,
etc., some of which may be marked local.  See
EMBEDDED-EVENT-FORM.  The usual Common Lisp commenting conventions
are provided.  Note that since a book consists of embedded event forms,
we can talk about the "local" and "non-local" events of a book.

Because in-package is not an embedded event form, the only in-package
in a book is the initial one.  Because defpkg is not an embedded event
form, a book can never contain a defpkg form.  Because include-book is
an embedded event form, books may contain references to other books.
This makes books structured objects.

When the forms in a book are read from the file, they are read with
current-package set to the package named in the in-package form at the
top of the file.  The effect of this is that all symbols are interned
in that package, except those whose packages are given explicitly with
the "::" notation.  For example, if a book begins with (in-package
"ACL2-X") and then contains the form

       (defun fn (x)
         (acl2::list 'car x))

then defun, fn, x, and car are all interned in the "ACL2-X" package.
I.e., it is as though the following form were read instead:

       (acl2-x::defun acl2-x::fn (acl2-x::x)
           (acl2::list 'acl2-x::car acl2-x::x)).

Of course, acl2-x::defun would be the same symbol as acl2::defun if the
"ACL2-X" package imported acl2::defun.

If each book has its own unique package name and all the names defined
within the book are in that package, then name clashes between books
are completely avoided.  This permits the construction of useful
logical worlds by the successive inclusion of many books.  Although it
is often too much trouble to manage several packages, their judicious
use is a way to minimize name clashes.  Often, a better way is to use
local; see LOCAL.

How does include-book know the definitions of the packages used in a
book, since defpkgs cannot be among the forms?  More generally, how do
we know that the forms in a book will be admissible in the host logical
world of an include-book?  See CERTIFICATE for answers to these
questions.

BOOK-EXAMPLE    how to create, certify, and use a simple book

Suppose you have developed a sequence of admissible events which you
want to turn into a book.  We call this "publishing" the book.  This
note explains how to do that.

A key idea of books is that they are "incremental" in the sense that
when you include a book in a host logical world, the world is
incrementally extended by the results established in that book.  This
is allowed only if every name defined by the incoming book is either
new or is already identically defined.  See REDUNDANT-EVENTS.
This is exactly the same problem faced by a programmer who wishes to
provide a utility to other people: how can he make sure he doesn't
create name conflicts?  The solution, in Common Lisp, is also the same:
use packages.  While books and packages have a very tenuous formal
connection (every book must start with an in-package), the creation of
a book is intimately concerned with the package issue.  Having
motivated what would otherwise appear as an unnecessary fascination
with packages below, we now proceed with a description of how to
publish a book.

Just to be concrete, let's suppose you have already gotten ACL2 to
accept the following sequence of commands, starting in the ACL2 initial
state.

        (defpkg "ACL2-MY-BOOK"
                (union-eq *common-lisp-symbols-from-main-lisp-package*
                          *acl2-exports*))
        (in-package "ACL2-MY-BOOK")
        (defun app (x y)
          (if (consp x) (cons (car x) (app (cdr x) y)) y))
        (defun rev (x)
          (if (consp x) (app (rev (cdr x)) (list (car x))) nil))
        (defthm rev-app-hack
          (equal (rev (app a (list x))) (cons x (rev a))))
        (defthm rev-rev
          (implies (acl2::true-listp x) (equal (rev (rev x)) x)))

Observe that the first form above defines a package (which imports the
symbols defined in CLTL such as if and cons and the symbols used to
command ACL2 such as defun and defthm).  The second form selects that
package as the current one.  All subsequent forms are read into that
package.  The remaining forms are just event forms: defuns and defthms
in this case.

Typically you would have created a file with Emacs containing these
forms and you will have submitted each of them interactively to ACL2 to
confirm that they are all admissible.  That interactive verification
should start in ACL2's initial world -- although you might, of course,
start your sequence of events with some include-books to build a more
elaborate world.

The first step towards publishing a book containing the results above
is to create a file that starts with the in-package and then contains
the rest of the forms.  Let's call that file "my-book.lisp".  The name
is unimportant, except it must end with ".lisp".  If there are events
that you do not wish to be available to the user of the book -- e.g.,
lemmas you proved on your way toward proving the main ones -- you may
so mark them by enclosing them in local forms.  See LOCAL.  Let
us suppose you wish to hide rev-app-hack above.  You may also add
standard Lisp comments to the file.  The final content of "my-book.lisp"
might be:

      ; This book contains my app and rev functions and the theorem
      ; that rev is its own inverse.

        (in-package "ACL2-MY-BOOK")
        (defun app (x y)
          (if (consp x) (cons (car x) (app (cdr x) y)) y))
        (defun rev (x)
          (if (consp x) (app (rev (cdr x)) (list (car x))) nil))

      ; The following hack is not exported.
        (local (defthm rev-app-hack
          (equal (rev (app a (list x))) (cons x (rev a)))))

        (defthm rev-rev
          (implies (acl2::true-listp x) (equal (rev (rev x)) x)))

The file shown above *is* the book.  By the time this note is done you
will have seen how to certify that the book is correct, how to compile
it, and how to use it in other host worlds.  Observe that the defpkg is
not in the book.  It cannot be: Common Lisp compilers disagree on how
to treat new package definitions appearing in files to be compiled.

Since a book is just a source file typed by the user, ACL2 provides a
mechanism for checking that the events are all admissible and then
marking the file as checked.  This is called certification.  To certify
"my-book.lisp" you should first get into ACL2 with an initial world.
Then, define the package needed by the book, by typing the following
defpkg to the ACL2 prompt:

     ACL2 !>(defpkg "ACL2-MY-BOOK"
                    (union-eq *common-lisp-symbols-from-main-lisp-package*
                              *acl2-exports*))

Then execute the command:

     ACL2 !>(certify-book "my-book" 1 t) ; the `t' is in fact the default

Observe that you do not type the ".lisp" part of the file name.  For
purposes of books, the book's name is "my-book" and by the time all is
said and done, there will be several extensions in addition to the
".lisp" extension associated with it.

The 1 tells certify-book that you acknowledge that there is one command
in this "certification world" (namely the defpkg).  To use the book,
any prospective host world must be extended by the addition of whatever
commands occurred before certification.  It would be a pity to certify
a book in a world containing junk because that junk will become the
"portcullis" guarding entrance to the book.  The t above tells
certify-book that you wish to compile "my-book.lisp" also (but see
COMPILATION for an exception).  Certify-book makes many checks
but by far the most important and time-consuming one is that it
"proves" every event in the file.

When certify-book is done it will have created two new files.  The
first will be called "my-book.cert" and contains the "certificate"
attesting to the admissibility of the events in "my-book.lisp".  The
certificate contains the defpkg and any other forms necessary to
construct the certification world.  It also contains various check sums
used to help you keep track of which version of "my-book.lisp" was
certified.

The second file that may be created by certify-book is the compiled
version of "my-book.lisp" and will have a name that is assigned by the
host compiler (e.g., "my-book.o" in GCL, "my-book.fasl" in SBCL).
Certify-book will also load this object file.  When certify-book is
done, you may throw away the logical world it created, for example by
executing the command :u.

To use the book later in any ACL2 session, just execute the event
(include-book "my-book").  This will do the necessary defpkg, load the
non-local events in "my-book.lisp" and then may load the compiled code
for the non-local functions defined in that file.  Checks are made to
ensure that the certificate file exists and describes the version of
"my-book.lisp" that is read.  The compiled code is loaded if and only
if it exists and has a later write date than the source file (but see
COMPILATION for an exception).

Since include-book is itself an event, you may put such forms into
other books.  Thus it is possible for the inclusion of a single book to
lead to the inclusion of many others.  The check sum information
maintained in certificates helps deal with the version control problem
of the referenced books.  I.e., if this version of "my-book" is used
during the certification of "your-book", then the certificate for
"your-book" includes the check sum of this version of "my-book".  If a
later (include-book "your-book") finds a version of "my-book" with a
different check sum, an error is signalled.  But check sums are not
perfect and the insecurity of the host file system prevents ACL2 from
guaranteeing the logical soundness of an include-book event, even for a
book that appears to have a valid certificate (they can be forged,
after all).  (See CERTIFICATE for further discussion.)

This concludes the example of how to create, certify and use a book.
If you wish, you could now review the documentation for book-related
topics (see BOOKS) and browse through them.  They'll probably
make sense in this context.  Alternatively, you could continue the
"guided tour" through the rest of the documentation of books.  See
BOOK-NAME, following the pointer given at the conclusion.

BOOK-MAKEFILES    makefile support provided with the ACL2 distribution

This topic describes the ACL2 methodology for using makefiles to assist
in the automation of the certification of collections of ACL2 books.  We
assume here a familiarity with Unix/Linux make.  We also assume that you
are using GNU make rather than some other flavor of make.

ACL2's regression suite is run using Makefiles that include
books/Makefile-generic.  You can look at existing Makefiles to
understand how to create your own Makefiles.  Here are the six steps to
follow to create a Makefile for a directory that contains books to be
certified, and certify them using that Makefile.  Below these steps we
conclude with discussion of other capabilties provided by
books/Makefile-generic.

1. It is most common to use an ACL2 executable named saved_acl2 that
resides in the parent directory of the distributed books/ directory.  In
this case, unless you are using a very old version of GNU make (version
3.80, at least, works fine), you should be able to skip the following
sentence, because the ACL2 `make' variable will be set automatically.
Otherwise, define the ACL2 variable using ?= to point to your ACL2
executable (though this may be omitted for directories directly under
the distributed books directory), for example:

     ACL2 ?= ../../../saved_acl2

(For Makefile experts: we use ?= instead of = or := because of the
protocol used by the ACL2 make system: command-line values are passed
explicitly with recursive calls of make to override the Makefile values
of ACL2, which in turn need to be able to override the environment value
of ACL2 from books/Makefile-generic).

Also include the file Makefile-generic in the distributed books
directory.  For example, file books/arithmetic-3/pass1/Makefile starts
as follows.

     include ../../Makefile-generic

If you also have a line defining ACL2 as explained above, put that line
just above this include line.

2. (Optional; usually skipped.)  Set the INHIBIT variable if you want to
see more than the summary output.  For example, if you want to see the
same output as you would normally see at the terminal, put this line in
your Makefile after the `ACL2 ?=' and ~c[include]' lines.

     INHIBIT = (assign inhibit-output-lst (list (quote proof-tree)))

For other values to use for INHIBIT, see SET-INHIBIT-OUTPUT-LST
and see the original setting of INHIBIT in books/Makefile-generic.

3. Specify the books to be certified.  If every file with extension
.lisp is a book that you want to certify, you can skip this step.
Otherwise, put a line in your Makefile after the ones above that
specifies the books to be certified.  The following example, from an
old version of books/finite-set-theory/osets/Makefile, should make this
clear.

     BOOKS = computed-hints fast instance map membership outer primitives \
             quantify set-order sets sort

But better yet, use the extension .lsp for any Lisp or ACL2 files that
are not to be certified, so that the definition of BOOKS can be omitted.

4. Create .acl2 files for books that are to be certified in other than
the initial ACL2 world (see PORTCULLIS).  For example, if you
look in books/arithmetic/equalities.acl2 you will see defpkg forms
followed by a certify-book command, because it was determined that
defpkg forms were necessary in the certification world in order to
certify the equalities book.  In general, for each <book-name>.lisp
whose certification requires a non-initial certification world, you
will need a corresponding <book-name>.acl2 file that ends with the
appropriate certify-book command.  Of course, you can also use .acl2
files with initial certification worlds, for example if you want to
pass optional arguments to certify-book.

You also have the option of creating a file cert.acl2 that has a special
role.  When file <book-name>.lisp is certified, if there is no file
<book-name>.acl2 but there is a file cert.acl2, then cert.acl2 will be
used as <book-name>.acl2 would have been used, as described in the
preceding paragraph, except that the appropriate certify-book command
will be generated automatically -- no certify-book command should occur
in cert.acl2.

It is actually allowed to put raw lisp forms in a .acl2 file (presumably
preceded by :q or (value :q) and followed by (lp)).  But this is not
recommended; we make no guarantees about certification performed any
time after raw Lisp has been entered in the ACL2 session.

5. Generally, the next step is to include the following line after the
`include' of Makefile-generic (see the first step above).

     -include Makefile-deps

This will cause `make' to create and then include a file Makefile-deps
that contains "dependency" lines needed by make.  If those dependencies
are somehow flawed, it may be because you have include-book forms that
are not truly including books, for example in multi-line comments
(#|..|#).  These will be ignored if preceded by a semicolon (;), or if
you add a line break after "include-book."  But instead, you can create
dependency lines yourself by running the command

     make dependencies

and pasting the result into the end of your Makefile, and editing as you
see fit.

6. Run make.  This will generate a <book-name>.out file for each
<book-name>.lisp file being certified, which is the result of
redirecting ACL2's standard output.  Note that make will stop at the
first failure, but you can use make -i to force make to continue past
failures.  You can also use the -j option to speed things up if you
have a multi-core machine, e.g., make -j 8 in a book directory or, if
in the ACL2 sources directory, make -j 8 regression.

This concludes the basic instructions for creating a Makefile in a
directory including books.  Here are some other capabilities offered by
books/Makefile-subdirs.

*Subdirectory support.*  There is support for subdirectories.  For
example, file books/arithmetic-3/Makefile formerly had the following
contents.

     DIRS = pass1 bind-free floor-mod
     include ../Makefile-subdirs

This indicated that we are to run make in subdirectories pass1/,
bind-free/, and floor-mod of the current directory (namely,
books/arithmetic-3/).

However, there is also subdirectory support when the current directory
has books as well.  File books/arithmetic-3/Makefile contains the
following lines (current in ACL2 Version_3.6).

     arith-top: top all
     all: top

     DIRS = pass1 bind-free floor-mod
     include ../Makefile-subdirs
     include ../Makefile-generic

     -include Makefile-deps

The first line is optional because ../../saved_acl2 is the default and
the directory is a sub-sub-directory of the distribution directory; but
it is harmless to include this line.  The other additional lines
support certifying books in the subdirectories before certifying the
books in the present directory, in the customary make style.

Specifically, the top target is defined in ../Makefile-subdirs to call
make in each subdirectory in DIRS.  We have set the default target in
the example above to a new name, arith-top, that makes that top target
before making the all target.  The all target, in turn, is the top
(default) target in ../Makefile-generic, and is responsible for
certifying books in the current directory.

Use Makefile-psubdirs instead of Makefile-subdirs if certification of a
book in a subdirectory never depends on certification of a book in a
different subdirectory, because then make's -j option can allow
subdirectories to be processed in parallel.

*Cleaning up.*  We note that there is a clean target.  Thus,

     make clean

will remove all .cert files, files resulting from compilation, and other
"junk"; see the full list under "clean:" in books/Makefile-generic.

*System books.* An environment variable ACL2_SYSTEM_BOOKS is generally
set automatically (at least in GNU make versions 3.80 and 3.81), so you
can probably skip reading the following paragraph unless your attempt
to certify distributed books fails to locate those books properly.

The environment variable ACL2_SYSTEM_BOOKS can be set to the books/
directory under which the books reside that are distributed with ACL2.
A Unix-style pathname, typically ending in books/ or books, is
permissible.  In most cases, your ACL2 executable is a small script in
which you can set this environment variable just above the line on
which the actual ACL2 image is invoked, for example:

     export ACL2_SYSTEM_BOOKS
     ACL2_SYSTEM_BOOKS=/home/acl2/v3-2/acl2-sources/books

However, you can also set ACL2_SYSTEM_BOOKS as a make variable, by
setting it in your Makefile before the first target definition, e.g.:

     ACL2_SYSTEM_BOOKS = /home/acl2/v3-2/acl2-sources/books

*Compilation support.*  Finally, books/Makefile-generic provides
support for compiling books that are already certified (but see
COMPILATION for an exception).  For example, suppose that you have
certified books in GCL, resulting in compiled files with the .o
extension.  Now suppose you would like to compile the books for Allegro
Common Lisp, whose compiled files have the .fasl extension.  The
following command will work if you have included books/Makefile-generic
in your Makefile.

     make fasl

In general, the compiled file extension for a Lisp supported by ACL2
will be a target name for building compiled files for all your books
(after certifying the books, if not already up-to-date on
certification).

BOOK-NAME    conventions associated with book names

     Examples:
     "list-processing"
     "/usr/home/smith/my-arith"

Book names are string constants that can be elaborated into file names.
We elaborate book names by concatenating the "connected book
directory" (see CBD) string on the left and some "extension,"
such as ".lisp", on the right.  However, the connected book directory
is not added if the book name itself already represents an absolute
file name.  Furthermore, include-book and certify-book temporarily
reset the connected book directory to be the directory of the book
being processed.  This allows include-book forms to use file names
without explicit mention of the enclosing book's directory.  This in
turn allows books (together with those that they include, using
include-book) to be moved between directories while maintaining their
certification and utility.

You may wish to read elsewhere for details of ACL2 file name
conventions (see PATHNAME), for a discussion of the filename
that is the result of the elaboration described here (see
FULL-BOOK-NAME), and for details of the concept of the connected book
directory (see CBD).  For details of how include-book (see
INCLUDE-BOOK) and certify-book (see CERTIFY-BOOK) use
these concepts, see below.

Often a book name is simply the familiar name of the file.  (See
FULL-BOOK-NAME for discussion of the notions of "directory string,"
"familiar name," and "extension".  These concepts are not on the guided
tour through books and you should read them separately.)  However, it
is permitted for book names to include a directory or part of a
directory name.  Book names never include the extension, since ACL2
must routinely tack several different extensions onto the name during
include-book.  For example, include-book uses the ".lisp", ".cert" and
possibly the ".o" or ".lbin" extensions of the book name.

Book names are elaborated into full file names by include-book and
certify-book.  This elaboration is sensitive to the "connected book
directory." The connected book directory is an absolute filename string
(see PATHNAME) that is part of the ACL2 state.  (You may wish
to see CBD and to see SET-CBD -- note that these are
not on the guided tour).  If a book name is an absolute filename
string, ACL2 elaborates it simply by appending the desired extension to
the right.  If a book name is a relative filename string, ACL2 appends
the connected book directory on the left and the desired extension on
the right.

Note that it is possible that the book name includes some partial
specification of the directory.  For example, if the connected book
directory is "/usr/home/smith/" then the book name
"project/task-1/arith" is a book name that will be elaborated to

     "/usr/home/smith/project/task-1/arith.lisp".

Observe that while the events in this "arith" book are being processed
the connected book directory will temporarily be set to

     "/usr/home/smith/project/task-1/".

Thus, if the book requires other books, e.g.,

     (include-book "naturals")

then it is not necessary to specify the directory on which they reside
provided that directory is the same as the superior book.

This inheritance of the connected book directory and its use to
elaborate the names of inferior books makes it possible to move books
and their inferiors to new directories, provided they maintain the same
relative relationship.  It is even possible to move with ease whole
collections of books to different filesystems that use a different
operating system than the one under which the original certification
was performed.

The ".cert" extension of a book, if it exists, is presumed to contain
the most recent certificate for the book.  See CERTIFICATE (or,
if you are on the guided tour, wait until the tour gets there).

See BOOK-CONTENTS to continue the guided tour.

CBD    connected book directory string

     Example:
     ACL2 !>:cbd
     "/usr/home/smith/"

The connected book directory is a nonempty string that specifies a
directory as an absolute pathname.  (See PATHNAME for a
discussion of file naming conventions.)  When include-book is given a
relative book name it elaborates it into a full book name, essentially
by appending the connected book directory string to the left and
".lisp" to the right.  (For details, see BOOK-NAME and also see
FULL-BOOK-NAME.)  Furthermore, include-book temporarily sets
the connected book directory to the directory string of the resulting
full book name so that references to inferior books in the same
directory may omit the directory.  See SET-CBD for how to set
the connected book directory string.

     General Form:
     (cbd)

This is a macro that expands into a term involving the single free
variable state.  It returns the connected book directory string.

The connected book directory (henceforth called the "cbd") is used by
include-book to elaborate the supplied book name into a full book name
(see FULL-BOOK-NAME).  For example, if the cbd is
"/usr/home/smith/" then the elaboration of the book-name
"project/task-1/arith" (to the ".lisp" extension) is
"/usr/home/smith/project/task-1/arith.lisp".  That full-book-name is
what include-book opens to read the source text for the book.

The cbd may be changed using set-cbd (see SET-CBD).
Furthermore, during the processing of the events in a book,
include-book sets the cbd to be the directory string of the
full-book-name of the book.  Thus, if the cbd is "/usr/home/smith/"
then during the processing of events by

     (include-book "project/task-1/arith")

the cbd will be set to "/usr/home/smith/project/task-1/".  Note that if
"arith" recursively includes a subbook, say "naturals", that resides on
the same directory, the include-book event for it may omit the
specification of that directory.  For example, "arith" might contain
the event

       (include-book "naturals").

In general, suppose we have a superior book and several inferior books
which are included by events in the superior book.  Any inferior book
residing on the same directory as the superior book may be referenced
in the superior without specification of the directory.

We call this a "relative" as opposed to "absolute" naming.  The use of
relative naming is preferred because it permits books (and their
accompanying inferiors) to be moved between directories while
maintaining their certificates and utility.  Certified books that
reference inferiors by absolute file names are unusable (and rendered
uncertified) if the inferiors are moved to new directories.

_Technical Note and a Challenge to Users:_

After elaborating the book name to a full book name, include-book opens
a channel to the file to process the events in it.  In some host Common
Lisps, the actual file opened depends upon a notion of "connected
directory" similar to our connected book directory.  Our intention in
always elaborating book names into absolute filename strings (see
PATHNAME for terminology) is to circumvent the sensitivity to the
connected directory.  But we may have insufficient control over this
since the ultimate file naming conventions are determined by the host
operating system rather than Common Lisp (though, we do check that the
operating system "appears" to be one that we "know" about).  Here is a
question, which we'll pose assuming that we have an operating system
that calls itself "Unix."  Suppose we have a file name, filename, that
begins with a slash, e.g., "/usr/home/smith/...".  Consider two
successive invocations of CLTL's

     (open filename :direction :input)

separated only by a change to the operating system's notion of
connected directory.  Must these two invocations produce streams to the
same file?  A candidate string might be something like
"/usr/home/smith/*/usr/local/src/foo.lisp" which includes some
operating system-specific special character to mean "here insert the
connected directory" or, more generally, "here make the name dependent
on some non-ACL2 aspect of the host's state."  If such "tricky" name
strings beginning with a slash exist, then we have failed to isolate
ACL2 adequately from the operating system's file naming conventions.
Once upon a time, ACL2 did not insist that the cbd begin with a slash
and that allowed the string "foo.lisp" to be tricky because if one were
connected to "/usr/home/smith/" then with the empty cbd "foo.lisp" is a
full book name that names the same file as "/usr/home/smith/foo.lisp".
If the actual file one reads is determined by the operating system's
state then it is possible for ACL2 to have two distinct "full book
names" for the same file, the "real" name and the "tricky" name.  This
can cause ACL2 to include the same book twice, not recognizing the
second one as redundant.

CERTIFICATE    how a book is known to be admissible and where its defpkgs reside

A book, say "arith", is said to have a "certificate" if there is a file
named "arith.cert".  Certificates are created by the function
certify-book and inspected by include-book.  Check sums are used to
help ensure that certificates are legitimate and that the corresponding
book has not been modified since certification.  But because the file
system is insecure and check sums are not perfect it is possible for
the inclusion of a book to cause inconsistency even though the book
carries an impeccable certificate.

The certificate includes the version number of the certifying ACL2.  A
book is considered uncertified if it is included in an ACL2 with a
different version number.

The presence of a "valid" certificate file for a book attests to two
things: all of the events of the book are admissible in a certain
extension of the initial ACL2 logic, and the non-local events of the
book are independent of the local ones (see
LOCAL-INCOMPATIBILITY).  In addition, the certificate contains the
commands used to construct the world in which certification occurred.
Among those commands, of course, are the defpkgs defining the packages
used in the book.  When a book is included into a host world, that
world is first extended by the commands listed in the certificate for
the book.  Unless that causes an error due to name conflicts, the
extension ensures that all the packages used by the book are
identically defined in the host world.

_Security:_

Because the host file system is insecure, there is no way ACL2 can
guarantee that the contents of a book remain the same as when its
certificate was written.  That is, between the time a book is certified
and the time it is used, it may be modified.  Furthermore, certificates
can be counterfeited.  Check sums (see CHECK-SUM) are used to
help detect such problems.  But check sums provide imperfect security:
two different files can have the same check sum.

Therefore, from the strictly logical point of view, one must consider
even the inclusion of certified books as placing a burden on the user:

     The non-erroneous inclusion of a certified book is consistency
     preserving provided (a) the objects read by include-book from the
     certificate were the objects written there by a certify-book and
     (b) the forms read by include-book from the book itself are the
     forms read by the corresponding certify-book.

We say that a given execution of include-book is "certified" if a
certificate file for the book is present and well-formed and the check
sum information contained within it supports the conclusion that the
events read by the include-book are the ones checked by certify-book.
When an uncertified include-book occurs, warnings are printed or errors
are caused.  But even if no warning is printed, you must accept burdens
(a) and (b) if you use books.  These burdens are easier to live with if
you protect your books so that other users cannot write to them, you
abstain from running concurrent ACL2 jobs, and you abstain from
counterfeiting certificates.  But even on a single user uniprocessor,
you can shoot yourself in the foot by using the ACL2 io primitives to
fabricate an inconsistent book and the corresponding certificate.

Note that part (a) of the burden described above implies, in
particular, that there are no guarantees when a certificate is copied.
When books are renamed (as by copying them), it is recommended that
their certificates be removed and the books be recertified.  The
expectation is that recertification will go through without a hitch if
relative pathnames are used.  See PATHNAME, which is not on the
guided tour.

Certificates essentially contain two parts, a portcullis and a keep.
There is a third part, an expansion-alist, in order to record
expansions if make-event has been used, but the user need not be
concerned with that level of detail.

See PORTCULLIS to continue the guided tour through books.

CERTIFY-BOOK    how to produce a certificate for a book

     Examples:
     (certify-book "my-arith")        ; certify in a world with 0 commands
     (certify-book "my-arith" 3)      ; ... in a world with 3 commands
     (certify-book "my-arith" ?)      ; ... in a world without checking the
                                        ;     number of commands
     (certify-book "my-arith" 0 nil)  ; ... do not compile
     (certify-book "my-arith" 0 t)    ; ... compile (default)
     (certify-book "my-arith" 0 t :ttags (foo))
                                        ; ... allow trust tag (ttag) foo
     (certify-book "my-arith" 0 t :ttags :all)
                                        ; ... allow all trust tags (ttags)
     (certify-book "my-arith" t)      ; certify from world of old certificate

     General Form:
     (certify-book book-name
                   k                           ; [default 0]
                   compile-flg                 ; [default generally t]
                   :defaxioms-okp t/nil        ; [default nil]
                   :skip-proofs-okp t/nil      ; [default nil]
                   :ttags ttags                ; [default nil]
                   )

where book-name is a book name (see BOOK-NAME), k is either t or
an integer used to indicate your approval of the "certification world,"
and compile-flg can control whether the book is to be compiled.

The second argument, k, is optional; it defaults to 0.

We next describe the meaning of compile-flg and how it defaults.  If
explicit compilation has been suppressed by (set-compiler-enabled nil),
then compile-flg is coerced to nil; see COMPILATION.  Otherwise
compile-flg may be given the value of t, indicating that the book is to
be compiled, or else nil.  Finally, suppose that compile-flg is not
supplied.  If environment variable ACL2_COMPILE_FLG is defined, then
its value should be T or NIL after converting to upper-case, in which
case compile-flg is considered to have value t or nil (respectively).
Otherwise compile-flg defaults to t.

Two keyword arguments, :defaxioms-okp and :skip-proofs-okp, determine
how the system handles the inclusion of defaxiom events and skip-proofs
events, respectively, in the book.  The value t allows such events, but
prints a warning message.  The value nil is the default, and causes an
error if such an event is found.

The keyword argument :ttags may normally be omitted.  A few constructs,
used for example if you are building your own system based on ACL2, may
require it.  See DEFTTAG for an explanation of this argument.

If you use guards, please note certify-book is executed as though
(set-guard-checking nil) has been evaluated; see
SET-GUARD-CHECKING.  If you want guards checked, consider using ld
instead, or in addition; see LD.

For a general discussion of books, see BOOKS.  Certify-book is
akin to what we have historically called a "proveall": all the forms in
the book are "proved" to guarantee their admissibility.  More
precisely, certify-book (1) reads the forms in the book, confirming
that the appropriate packages are defined in the certification world;
(2) does the full admissibility checks on each form (proving
termination of recursive functions, proving theorems, etc.), checking
as it goes that each form is an embedded event form (see
EMBEDDED-EVENT-FORM); (3) rolls the world back to the initial
certification world and does an include-book of the book to check for
local incompatibilities (see LOCAL-INCOMPATIBILITY); (4) writes
a certificate recording not only that the book was certified but also
recording the commands necessary to recreate the certification world
(so the appropriate packages can be defined when the book is included
in other worlds) and the check sums of all the books involved (see
CERTIFICATE); (5) compiles the book if so directed (and then
loads the object file in that case).  The result of executing a
certify-book command is the creation of a single new event, which is
actually an include-book event.  If you don't want its included events
in your present world, simply execute :ubt :here afterwards.

Certify-book requires that the default defun-mode (see
DEFAULT-DEFUN-MODE) be :logic when certification is attempted.  If
the mode is not :logic, an error is signalled.

An error will occur if certify-book has to deal with any uncertified
book other than the one on which it was called.  For example, if the
book being certified includes another book, that subbook must already
have been certified.

Certification occurs in some logical world, called the "certification
world." That world must contain the defpkgs needed to read and execute
the forms in the book.  The commands necessary to recreate that world
from the ACL2 initial world will be copied into the certificate created
for the book.  Those commands will be re-executed whenever the book is
included, to ensure that the appropriate packages (and all other names
used in the certification world) are correctly defined.  The certified
book will be more often usable if the certification world is kept to a
minimal extension of the ACL2 initial world.  Thus, before you call
certify-book for the first time on a book, you should get into the
initial ACL2 world (e.g., with :ubt 1 or just starting a new version of
ACL2), defpkg the desired packages, and then invoke certify-book.

The k argument to certify-book must be either a nonnegative integer or
else one of the symbols t or ? in the ACL2 package.  If k is an
integer, then it must be the number of commands that have been executed
after the initial ACL2 world to create the world in which certify-book
was called.  One way to obtain this number is by doing :pbt :start to
see all the commands back to the first one.

If k is t it means that certify-book should use the same world used in
the last certification of this book.  K may be t only if you call
certify-book in the initial ACL2 world and there is a certificate on
file for the book being certified.  (Of course, the certificate is
probably invalid.)  In this case, certify-book reads the old
certificate to obtain the portcullis commands and executes them to
recreate the certification world.

Finally, k may be ?, in which case there is no check made on the
certification world.  That is, if k is ? then no action related to the
preceding two paragraphs is performed, which can be a nice convenience
but at the cost of eliminating a potentially valuable check that the
certification world may be as expected.

If you have a certified book that has remained unchanged for some time
you are unlikely even to remember the appropriate defpkgs for it.  If
you begin to change the book, don't throw away its certificate file just
because it has become invalid!  It is an important historical document
until the book is re-certified.

When certify-book is directed to produce a compiled file, it calls the
Common Lisp function compile-file on the original source file.  This
creates a compiled file with an extension known to ACL2, e.g., if the
book is named "my-book" then the source file is "my-book.lisp" and the
compiled file under GCL will be "my-book.o" while under SBCL it will be
"my-book.fasl".  The compiled file is then loaded.  When include-book
is used later on "my-book" it will automatically load the compiled
file, provided the compiled file has a later write date than the source
file.  The only effect of such compilation and loading is that the
functions defined in the book execute faster.  See GUARD for a
discussion of the issues, and if you want more details about books and
compilation, see BOOK-COMPILED-FILE.

When certify-book is directed not to produce a compiled file, it will
delete any existing compiled file for the book, so as not to mislead
include-book into loading the now outdated compiled file.  Otherwise,
certify-book will create a temporarily "expansion file" to compile,
obtained by appending the string "@expansion.lsp" to the end of the book
name.  Remark: Users may ignore that file, which is automatically
deleted unless state global variable 'save-expansion-file has been set,
presumably by a system developer, to a non-nil value; see
BOOK-COMPILED-FILE for more information about hit issue, including the
role of environment variable ACL2_SAVE_EXPANSION.

After execution of a certify-book form, the value of
acl2-defaults-table is restored to what it was immediately before that
certify-book form was executed.  See ACL2-DEFAULTS-TABLE.

This completes the tour through the documentation of books.

FULL-BOOK-NAME    book naming conventions assumed by ACL2

For this discussion we assume that the resident operating system is
Unix (trademark of AT&T), but analogous remarks apply to other
operating systems supported by ACL2, in particular, the Macintosh
operating system where `:' plays roughly the role of `/' in Unix; see
PATHNAME.

ACL2 defines a "full book name" to be an "absolute filename string,"
that may be divided into contiguous sections:  a "directory string", a
"familiar name" and an "extension".  See PATHNAME for the
definitions of "absolute," "filename string," and other notions
pertaining to naming files.  Below we exhibit the three sections of one
such string:

     "/usr/home/smith/project/arith.lisp"

     "/usr/home/smith/project/"           ; directory string
                             "arith"      ; familiar name
                                  ".lisp" ; extension

The sections are marked by the rightmost slash and rightmost dot, as
shown below.

     "/usr/home/smith/project/arith.lisp"
                             |     |
                             slash dot
                             |     |
     "/usr/home/smith/project/"           ; directory string
                             "arith"      ; familiar name
                                  ".lisp" ; extension

The directory string includes (and terminates with) the rightmost
slash.  The extension includes (and starts with) the rightmost dot.
The dot must be strictly to the right of the slash so that the familiar
name is well-defined and nonempty.

If you are using ACL2 on a system in which file names do not have this
form, please contact the authors and we'll see what we can do about
generalizing ACL2's conventions.

KEEP    how we know if include-book read the correct files

The certificate (see CERTIFICATE for general information) of a
certified file is divided into two parts, a portcullis and a keep.
These names come from castle lore.  The keep is the strongest and
usually tallest tower of a castle from which the entire courtyard can
be surveyed by the defenders.  The keep of a book is a list of file
names and check sums used after the book has been included, to
determine if the files read were (up to check sum) those certified.

Once the portcullis is open, include-book can enter the book and read
the event forms therein.  The non-local event forms are in fact
executed, extending the host theory.  That may read in other books.
When that has been finished, the keep of the certificate is inspected.
The keep is a list of the book names which are included (hereditarily
through all subbooks) in the certified book (including the certified
book itself) together with the check sums of the objects in those books
at the time of certification.  We compare the check sums of the books
just included to the check sums of the books stored in the keep.  If
differences are found then we know that the book or one of its subbooks
has been changed since certification.

See INCLUDE-BOOK to continue the guided tour through books.

MAKEFILES    See BOOK-MAKEFILES.

PATHNAME    introduction to filename conventions in ACL2

The notion of pathname objects from Common Lisp is not supported in
ACL2, nor is the function pathname.  However, ACL2 supports file
operations, using conventions for naming files based on those of the
Unix (trademark of AT&T) operating system, so that the character / is
used to terminate directory names.  Some file names are "absolute"
(complete) descriptions of a file or directory; others are "relative"
to the current working directory or to the connected book directory
(see CBD).  We emphasize that even for users of Windows-based
systems or Macintosh computers, ACL2 file names are in the Unix style.
We will call these _ACL2 pathnames_, often omitting the "ACL2."

Pathnames starting with the directory separator (/) or the tilde
character (~) are absolute pathnames.  All other pathnames are relative
pathnames.  An exception is in the Microsoft Windows operating system,
where it is illegal for the pathname to start with a tilde character
but the drive may be included, e.g., "c:/home/smith/acl2/book-1.lisp".
In fact, the drive _must_ be included in the portcullis of a book; see
PORTCULLIS.  Note also that some host Common Lisps will not
support pathnames starting with "~", for example ~smith, though ACL2
will generally support those starting with "~/" regardless of the host
Common Lisp.

Consider the following examples.  The filename string

     "/home/smith/acl2/book-1.lisp"

is an absolute pathname, with top-level directory "home", under that
the directory "smith" and then the directory "acl2", and finally,
within that directory the file "book-1.lisp".  If the connected book
directory is "/home/smith/" (see CBD), then the filename string
above also corresponds to the relative filename string
"acl2/book1.lisp".

Finally, we note that (on non-Windows systems) the pathname "~" and
pathnames starting with "~/" are illegal in books being certified.
Otherwise, a subsidiary include-book form would have a different
meaning at certification time than at a later time when the certified
book is included by a different user.

PORTCULLIS    the gate guarding the entrance to a certified book

The certificate (see CERTIFICATE for general information) of a
certified file is divided into two parts, a portcullis and a keep.
These names come from castle lore.  The portcullis of a castle is an
iron grate that slides up through the ceiling of the tunnel-like
entrance.  The portcullis of a book ensures that include-book does not
start to read the book until the appropriate context has been created.

Technically, the portcullis consists of the version number of the
certifying ACL2, a list of commands used to create the "certification
world" and an alist specifying the check sums of all the books included
in that world.  The portcullis is constructed automatically by
certify-book from the world in which certify-book is called, but that
world must have certain properties described below.  After listing the
properties we discuss the issues in a more leisurely manner.

Each command in the portcullis must be either a defpkg form or an
embedded event form (see EMBEDDED-EVENT-FORM).

Consider a book to be certified.  The book is a file containing event
forms.  Suppose the file contains references to such symbols as
my-pkg::fn and acl2-arith::cancel, but that the book itself does not
create the packages.  Then a hard Lisp error would be caused merely by
the attempt to read the expressions in the book.  The corresponding
defpkgs cannot be written into the book itself because the book must be
compilable and Common Lisp compilers differ on the rules concerning the
inline definition of new packages.  The only safe course is to make all
defpkgs occur outside of compiled files.

More generally, when a book is certified it is certified within some
logical world.  That "certification world" contains not only the
necessary defpkgs but also, perhaps, function and constant definitions
and maybe even references to other books.  When certify-book creates
the certificate for a file it recovers from the certification world the
commands used to create that world from the initial ACL2 world.  Those
commands become part of the portcullis for the certified book.  In
addition, certify-book records in the portcullis the check sums (see
CHECK-SUM) of all the books included in the certification world.

Include-book presumes that it is impossible even to read the contents
of a certified book unless the portcullis can be "raised." To raise the
portcullis we must be able to execute (possibly redundantly, but
certainly without error), all of the commands in the portcullis and
then verify that the books thus included were identical to those used
to build the certification world (up to check sum).  This raising of
the portcullis must be done delicately since defpkgs are present: we
cannot even read a command in the portcullis until we have successfully
executed the previous ones, since packages are being defined.

Clearly, a book is most useful if it is certified in the most
elementary extension possible of the initial logic.  If, for example,
your certification world happens to contain a defpkg for "MY-PKG" and
the function foo, then those definitions become part of the portcullis
for the book.  Every time the book is included, those names will be
defined and will have to be either new or redundant (see
REDUNDANT-EVENTS).  But if those names were not necessary to the
certification of the book, their presence would unnecessarily restrict
the utility of the book.

See KEEP to continue the guided tour of books.

SET-CBD    to set the connected book directory

     Example Forms:
     ACL2 !>:set-cbd "/usr/home/smith/"
     ACL2 !>:set-cbd "my-acl2/books"

See CBD for a description of the connected book directory.

     General Form:
     (set-cbd str)

where str is a nonempty string that represents the desired directory
(see PATHNAME).  This command sets the connected book directory
(see CBD) to the string representing the indicated directory.
Thus, this command may determine which files are processed by
include-book and certify-book commands typed at the top-level.
However, the cbd is also temporarily set by those two book processing
commands.

IMPORTANT:  Pathnames in ACL2 are in the Unix (trademark of AT&T)
style.  That is, the character "/" separates directory components of a
pathname, and pathnames are absolute when they start with this
character, and relative otherwise.  See PATHNAME.

UNCERTIFIED-BOOKS    invalid certificates and uncertified books

Include-book has a special provision for dealing with uncertified
books: If the file has no certificate or an invalid certificate (i.e.,
one whose check sums describe files other than the ones actually read),
a warning is printed and the book is otherwise processed as though it
were certified and had an open portcullis.  (For details see
BOOKS, see CERTIFICATE, and see PORTCULLIS.)

This can be handy, but it can have disastrous consequences.

The provision allowing uncertified books to be included can have
disastrous consequences, ranging from hard lisp errors, to damaged
memory, to quiet logical inconsistency.

It is possible for the inclusion of an uncertified book to render the
logic inconsistent.  For example, one of its non-local events might be
(defthm t-is-nil (equal t nil)).  It is also possible for the inclusion
of an uncertified book to cause hard errors or breaks into raw Common
Lisp.  For example, if the file has been edited since it was certified,
it may contain too many open parentheses, causing Lisp to read past
"end of file." Similarly, it might contain non-ACL2 objects such as
3.1415 or ill-formed event forms that cause ACL2 code to break.

Even if a book is perfectly well formed and could be certified (in a
suitable extension of ACL2's initial world), its uncertified inclusion
might cause Lisp errors or inconsistencies!  For example, it might
mention packages that do not exist in the host world.  The portcullis
of a certified book ensures that the correct defpkgs have been
admitted, but if a book is read without actually raising its
portcullis, symbols in the file, e.g., acl2-arithmetic::fn, could cause
"unknown package" errors in Common Lisp.  Perhaps the most subtle
disaster occurs if the host world does have a defpkg for each package
used in the book but the host defpkg imports different symbols than
those required by the portcullis.  In this case, it is possible that
formulas which were theorems in the certified book are non-theorems in
the host world, but those formulas can be read without error and will
then be quietly assumed.

In short, if you include an uncertified book, *all bets are off*
regarding the validity of the future behavior of ACL2.

That said, it should be noted that ACL2 is pretty tough and if errors
don't occur, the chances are that deductions after the inclusion of an
uncertified book are probably justified in the (possibly inconsistent)
logical extension obtained by assuming the admissibility and validity
of the definitions and conjectures in the book.

BREAK-REWRITE    the read-eval-print loop entered to monitor rewrite rules

ACL2 allows the user to monitor the application of rewrite rules.  When
monitored rules are about to be tried by the rewriter, an interactive
break occurs and the user is allowed to watch and, in a limited sense,
control the attempt to apply the rule.  This interactive loop, which is
technically just a call of the standard top-level ACL2 read-eval-print
loop, ld, on a "wormhole state" (see WORMHOLE), is called
"break-rewrite."  While in break-rewrite, certain keyword commands are
available for accessing information about the context in which the
lemma is being tried.  These keywords are called break-rewrite
"commands."

Also see DMR (Dynamically Monitor Rewrites) for a related
utility, which allows you to watch progress of the rewriter in real
time.

To abort from inside break-rewrite at any time, execute

For further information, see the related :doc topics listed below.

Related topics other than immediate subtopics:

As explained in the documentation for monitor, it is possible to cause
the ACL2 rewriter to monitor the attempted application of selected
rules.  When such a rule is about to be tried, the rewriter evaluates
its break condition and if the result is non-nil, break-rewrite is
entered.

Break-rewrite permits the user to inspect the current state by
evaluating break-rewrite commands.  Type :help in break-rewrite to see
what the break-rewrite commands are.  However, break-rewrite is
actually just a call of the general ACL2 read-eval-print loop, ld, on a
certain state and the break-rewrite commands are simply aliases
provided by the ld-special ld-keyword-aliases.  See LD for
details about this read-eval-print loop.  Thus, with a few exceptions,
anything you can do at the ACL2 top-level can be done within
break-rewrite.  For example, you can evaluate arbitrary expressions,
use the keyword command hack, access documentation, print events, and
even define functions and prove theorems.  However, the "certain state"
upon which ld was called is a "wormhole state" (see WORMHOLE)
because break-rewrite is not allowed to have any effect upon the
behavior of rewrite.  What this means, very roughly but understandably,
is that break-rewrite operates on a copy of the state being used by
rewrite and when break-rewrite exits the wormhole closes and the state
"produced" by break-rewrite disappears.  Thus, break-rewrite lets you
query the state of the rewriter and even do experiments involving
proofs, etc., but these experiments have no effect on the ongoing proof
attempt.

When you first enter break-rewrite a simple herald is printed such as:

     (3 Breaking (:rewrite lemma12) on (delta a (+ 1 j)):

The integer after the open parenthesis indicates the depth of nested
break-rewrite calls.  In this discussion we use 3 consistently for this
integer.  Unless you abort or somehow enter unbalanced parentheses into
the script, the entire session at a given depth will be enclosed in
balanced parentheses, making it easy to skip over them in Emacs.

You then will see the break-rewrite prompt:

     3 ACL2 !>

The leading integer is, again, the depth.  Because breaks often occur
recursively it is convenient always to know the level with which you
are interacting.

You may type arbitrary commands as in the top-level ACL2 loop.  For
example, you might type:

     3 ACL2 !>:help

or

     3 ACL2 !>:pe lemma12

More likely, upon entering break-rewrite you will determine the context
of the attempted application.  Here are some useful commands:

     3 ACL2 >:target           ; the term being rewritten
     3 ACL2 >:unify-subst      ; the unifying substitution
     3 ACL2 >:path             ; the stack of goals pursued by the rewriter
                               ; starting at the top-level clause being simplified
                               ; and ending with the current application

At this point in the interaction the system has not yet tried to apply
the monitored rule.  That is, it has not tried to establish the
hypotheses, considered the heuristic cost of backchaining, rewritten
the right-hand side of the conclusion, etc.  When you are ready for it
to try the rule you can type one of several different "proceed"
commands.  The basic proceed commands are :ok, :go, and :eval.

     :ok

exits break-rewrite without further interaction.  When break-rewrite
exits it prints "3)", closing the parenthesis that opened the level 3
interaction.

     :go

exits break-rewrite without further interaction, but prints out the
result of the application attempt, i.e., whether the application
succeeded, if so, what the :target term was rewritten to, and if not
why the rule was not applicable.

     :eval

causes break-rewrite to attempt to apply the rule but interaction at
this level of break-rewrite resumes when the attempt is complete.  When
control returns to this level of break-rewrite a message indicating the
result of the application attempt (just as in :go) is printed, followed
by the prompt for additional user input.

Generally speaking, :ok and :go are used when the break in question is
routine or uninteresting and :eval is used when the break is one that
the user anticipates is causing trouble.  For example, if you are
trying to determine why a lemma isn't being applied to a given term and
the :target of the current break-rewrite is the term in question, you
would usually :eval the rule and if break-rewrite reports that the rule
failed then you are in a position to determine why, for example by
carefully inspecting the :type-alist of governing assumptions or why
some hypothesis of the rule could not be established.

It is often the case that when you are in break-rewrite you wish to
change the set of monitored runes.  This can be done by using :monitor
and :unmonitor as noted above.  For example, you might want to monitor
a certain rule, say hyp-reliever, just when it is being used while
attempting to apply another rule, say main-lemma.  Typically then you
would monitor main-lemma at the ACL2 top-level, start the
proof-attempt, and then in the break-rewrite in which main-lemma is
about to be tried, you would install a monitor on hyp-reliever.  If
during the ensuing :eval hyp-reliever is broken you will know it is
being used under the attempt to apply main-lemma.

However, once hyp-reliever is being monitored it will be monitored even
after main-lemma has been tried.  That is, if you let the proof attempt
proceed then you may see many other breaks on hyp-reliever, breaks that
are not "under" the attempt to apply main-lemma.  One way to prevent
this is to :eval the application of main-lemma and then :unmonitor
hyp-reliever before exiting.  But this case arises so often that ACL2
supports several additional "flavors" of proceed commands.

:Ok!, :go!, and :eval! are just like their counterparts (:ok, :go, and
:eval, respectively), except that while processing the rule that is
currently broken no runes are monitored.  When consideration of the
current rule is complete, the set of monitored runes is restored to its
original setting.

:Ok$, :go$, and :eval$ are similar but take an additional argument
which must be a list of runes.  An example usage of :eval$ is

     3 ACL2 !>:eval$ ((:rewrite hyp-reliever))

These three commands temporarily install unconditional breaks on the
runes listed, proceed with the consideration of the currently broken
rule, and then restore the set of monitored rules to its original
setting.

Thus, there are nine ways to proceed from the initial entry into
break-rewrite although we often speak as though there are two, :ok and
:eval, and leave the others implicit.  We group :go with :ok because in
all their flavors they exit break-rewrite without further interaction
(at the current level).  All the flavors of :eval require further
interaction after the rule has been tried.

To abort a proof attempt and return to the top-level of ACL2 you may at
any time type (a!) followed by a carriage return.  If you are not in a
raw Lisp break, you may type :a! instead.  The utility p! is completely
analogous to a! except that it pops up only one ld level.  If you have
just entered the break-rewrite loop, this will pop you out of that loop,
back to the proof.  See A! and see P!.

We now address ourselves to the post-:eval interaction with
break-rewrite.  As noted, that interaction begins with break-rewrite's
report on the results of applying the rule: whether it worked and
either what it produced or why it failed.  This information is also
printed by certain keyword commands available after :eval, namely
:wonp, :rewritten-rhs, and :failure-reason.  In addition, by using brr@
(see BRR@) you can obtain this information in the
form of ACL2 data objects.  This allows the development of more
sophisticated "break conditions"; see MONITOR for examples.  In
this connection we point out the macro form (ok-if term).  See
OK-IF.  This command exits break-rewrite if term evaluates to non-nil
and otherwise does not exit.  Thus it is possible to define macros that
provide other kinds of exits from break-rewrite.  The only way to exit
break-rewrite after :eval is :ok (or, equivalently, the use of ok-if).

ACL2 users who wish to know more about break-rewrite so that they can
develop more convenient ways to monitor rules are encouraged to speak
to J Moore.

The rest of this documentation discusses a few implementation details
of break-rewrite and may not be interesting to the typical user.

There is no ACL2 function named break-rewrite.  It is an illusion
created by appropriate calls to two functions named brkpt1 and brkpt2.
As previously noted, break-rewrite is ld operating on a wormhole state.
One might therefore wonder how break-rewrite can apply a rule and then
communicate the results back to the rewriter running in the external
state.  The answer is that it cannot.  Nothing can be communicated
through a wormhole.  In fact, brkpt1 and brkpt2 are each calls of ld
running on wormhole states.  Brkpt1 implements the pre-:eval
break-rewrite and brkpt2 implements the post-:eval break-rewrite.  The
rewriter actually calls brkpt1 before attempting to apply a rule and
calls brkpt2 afterwards.  In both cases, the rewriter passes into the
wormhole the relevant information about the current context.  Logically
brkpt1 and brkpt2 are no-ops and rewrite ignores the nil they return.
But while control is in them the execution of rewrite is suspended and
cannot proceed until the break-rewrite interactions complete.

This design causes a certain anomoly that might be troubling.  Suppose
that inside break-rewrite before :evaling a rule (i.e., in the brkpt1
wormhole state) you define some function, foo.  Suppose then you :eval
the rule and eventually control returns to break-rewrite (i.e., to
brkpt2 on a wormhole state with the results of the application in it).
You will discover that foo is no longer defined!  That is because the
wormhole state created during your pre-:eval interaction is lost when
we exit the wormhole to resume the proof attempt.  The post-:eval
wormhole state is in fact identical to the initial pre-:eval state
(except for the results of the application) because rewrite did not
change the external state and both wormhole states are copies of it.  A
similar issue occurs with the use of trace utilities: all effects of
calling trace$ and untrace$ are erased when you proceed from a break in
the break-rewrite loop.

There is a lot more to know about break-rewrite, most of which is
fairly easy to learn from looking at the code, since it is all
expressed in ACL2.  Feel free to ask questions of J Moore.

BREAK-LEMMA    a quick introduction to breaking rewrite rules in ACL2

     Example:
     :brr t                          ; if you haven't done that yet
     :monitor (:rewrite lemma12) t   ; to install a break point on the
                                     ; rule named (:rewrite lemma12)

ACL2 does not support Nqthm's break-lemma but supports a very similar
and more powerful break facility.  Suppose some proof is failing;
apparently some particular rule is not being used and you wish to learn
why.  Then you need the ACL2 break-rewrite facility.  See
BREAK-REWRITE and all of its associated :doc topics for details.  The
following basic steps are required.

(1) To enable the "break rewrite" feature, you must first execute

     ACL2 !>:brr t

at the top-level of ACL2.  Equivalently, evaluate (brr t).
Break-rewrite stays enabled until you disable it with (brr nil).  When
break-rewrite is enabled the ACL2 rewriter will run slower than normal
but you will be able to monitor the attempts to apply specified rules.

(2) Decide what runes (see RUNE) you wish to monitor.  For
example, you might want to know why (:rewrite lemma12 . 2) is not being
used in the attempted proof.  That, by the way, is the name of the
second rewrite rule generated from the event named lemma12.

The command

     ACL2 !>:monitor (:rewrite lemma12 . 2) t

will install an "unconditional" break point on that rule.  The "t" at
the end of the command means it is unconditional, i.e., a break will
occur every time the rule is tried.  ACL2 supports conditional breaks
also, in which case the t is replaced by an expression that evaluates
to non-nil when you wish for a break to occur.  See MONITOR.
The above keyword command is, of course, equivalent to

     ACL2 !>(monitor '(:rewrite lemma12 . 2) t)

which you may also type.  You may install breaks on as many rules as
you wish.  You must use monitor on each rule.  You may also change the
break condition on a rule with monitor.  Use unmonitor (see
UNMONITOR) to remove a rule from the list of monitored rules.

(3) Then try the proof again.  When a monitored rule is tried by the
rewriter you will enter an interactive break, called break-rewrite.
See BREAK-REWRITE for a detailed description.  Very simply,
break-rewrite lets you inspect the context of the attempted application
both before and after the attempt.  When break-rewrite is entered it
will print out the "target" term being rewritten.  If you type :go
break-rewrite will try the rule and then exit, telling you (a) whether
the rule was applied, (b) if so, how the target was rewritten, and (c)
if not, why the rule failed.  There are many other commands.  See
BRR-COMMANDS.

(4) When you have finished using the break-rewrite feature you should
disable it to speed up the rewriter.  You can disable it with

     ACL2 !>:brr nil

The list of monitored rules and their break conditions persists but is
ignored.  If you enable break-rewrite later, the list of monitored
rules will be displayed and will be used again by rewrite.

You should disable the break-rewrite feature whenever you are not
intending to use it, even if the list of monitored rules is empty,
because the rewriter is slowed down as long as break-rewrite is enabled.

If you get a stack overflow, see CW-GSTACK.

BRR    to enable or disable the breaking of rewrite rules

     Example:
     :brr t       ; enable
     :brr nil     ; disable

     General Form:
     (brr flg)

where flg evaluates to t or nil.  This function modifies state so that
the attempted application of certain rewrite rules are "broken." "Brr"
stands for "break-rewrite" and can be thought of as a mode with two
settings.  The normal mode is "disabled."

When brr mode is "enabled" the ACL2 rewriter monitors the attempts to
apply certain rules and advises the user of those attempts by entering
an interactive wormhole break.  From within this break the user can
watch selected application attempts.  See BREAK-REWRITE.  The
user can also interact with the system during brr breaks via
brr-commands.

The rules monitored are selected by using the monitor and unmonitor
commands.  It is possible to break a rune "conditionally" in the sense
that an interactive break will occur only if a specified predicate is
true of the environment at the time of the attempted application.  See
MONITOR and see UNMONITOR.

Even if a non-empty set of rules has been selected, no breaks will occur
unless brr mode is enabled.  Thus, the first time in a session that you
wish to monitor a rewrite rule, use :brr t to enable brr mode.
Thereafter you may select runes to be monitored with monitor and
unmonitor with the effect that whenever monitored rules are tried (and
their break conditions are met) an interactive break will occur.  Be
advised that when brr mode is enabled the rewriter is somewhat slower
than normal.  Furthermore, that sluggishness persists even if no runes
are monitored.  You may regain normal performance -- regardless of what
runes are monitored -- by disabling brr mode with :brr nil.

Why isn't brr mode disabled automatically when no runes are monitored?
More generally, why does ACL2 have brr mode at all?  Why not just test
whether there are monitored runes?  If you care about the answers, see
WHY-BRR.

BRR Mode and Console Interrupts: If the system is operating in brr mode
and you break into raw Lisp (as by causing a console interrupt or
happening upon a signalled Lisp error; see BREAKS), you can
return to the ACL2 top-level, outside any brr environment, by executing
(abort!).  Otherwise, the normal way to quit from such a break (for
example :q in GCL, :reset in Allegro CL, and q in CMU CL) will return
to the innermost ACL2 read-eval-print loop, which may or may not be the
top-level of your ACL2 session!  In particular, if the break happens to
occur while ACL2 is within the brr environment (in which it is
preparing to read brr-commands), the abort will merely return to that
brr environment.  Upon exiting that environment, normal theorem proving
is continued (and the brr environment may be entered again in response
to subsequent monitored rule applications).  Before returning to the brr
environment, ACL2 "cleans up" from the interrupted brr processing.
However, it is not possible (given the current implementation) to clean
up perfectly.  This may have two side-effects.  First, the system may
occasionally print the self-explanatory "Cryptic BRR Message 1" (or 2),
informing you that the system has attempted to recover from an aborted
brr environment.  Second, it is possible that subsequent brr behavior
in that proof will be erroneous because the cleanup was done
incorrectly.  The moral is that you should not trust what you learn
from brr if you have interrupted and aborted brr processing during the
proof.  These issues do not affect the behavior or soundness of the
theorem prover.

BRR-COMMANDS    Break-Rewrite Commands

     :a!             abort to ACL2 top-level
     :p!             pop one level (exits a top-level break-rewrite loop)
     :target         term being rewritten
     :unify-subst    substitution making :lhs equal :target
     :hyps           hypotheses of the rule
     :hyp i          ith hypothesis of the rule
     :lhs            left-hand side of rule's conclusion
     :rhs            right-hand side of rule's conclusion
     :type-alist     type assumptions governing :target
     :initial-ttree  ttree before :eval (see TTREE)
     :ancestors      negations of backchaining hypotheses being pursued
     :wonp           indicates if application succeed (after :eval)
     :rewritten-rhs  rewritten :rhs (after :eval)
     :final-ttree    ttree after :eval (see TTREE)
     :failure-reason reason rule failed (after :eval)
     :path           rewrite's path from top clause to :target
     :frame i        ith frame in :path
     :top            top-most frame in :path
     :ok             exit break
     :go             exit break, printing result
     :eval           try rule and re-enter break afterwards
     :ok!            :ok but no recursive breaks
     :go!            :go but no recursive breaks
     :eval!          :eval but no recursive breaks
     :ok$ runes      :ok with runes monitored during recursion
     :go$ runes      :go with runes monitored during recursion
     :eval$ runes    :eval with runes monitored during recursion
     :help           this message
     :standard-help  :help message from ACL2 top-level

Break-rewrite is just a call of the standard ACL2 read-eval-print loop,
ld, on a "wormhole" state.  Thus, you may execute most commands you
might normally execute at the top-level of ACL2.  However, all state
changes you cause from within break-rewrite are lost when you exit or
:eval the rule.  You cannot modify stobjs from within the break.  See
BREAK-REWRITE for more details and see LD for general
information about the standard ACL2 read-eval-print loop.

BRR@    to access context sensitive information within break-rewrite

     Example:
     (brr@ :target)      ; the term being rewritten
     (brr@ :unify-subst) ; the unifying substitution

     General Form:
     (brr@ :symbol)

where :symbol is one of the following keywords.  Those marked with *
probably require an implementor's knowledge of the system to use
effectively.  They are supported but not well documented.  More is said
on this topic following the table.

     :symbol             (brr@ :symbol)
     -------             ---------------------

     :target             the term to be rewritten.  This term is an
                         instantiation of the left-hand side of the
                         conclusion of the rewrite-rule being broken.
                         This term is in translated form!  Thus, if
                         you are expecting (equal x nil) -- and your
                         expectation is almost right -- you will see
                         (equal x 'nil); similarly, instead of (cadr a)
                         you will see (car (cdr a)).  In translated
                         forms, all constants are quoted (even nil, t,
                         strings and numbers) and all macros are
                         expanded.

     :unify-subst        the substitution that, when applied to :target,
                         produces the left-hand side of the rule being
                         broken.  This substitution is an alist pairing
                         variable symbols to translated (!) terms.

     :wonp               t or nil indicating whether the rune was
                         successfully applied.  (brr@ :wonp) returns
                         nil if evaluated before :EVALing the rule.

     :rewritten-rhs      the result of successfully applying the rule
                         or else nil if (brr@ :wonp) is nil.  The result
                         of successfully applying the rule is always a
                         translated (!) term and is never nil.

     :failure-reason     some non-nil lisp object indicating why the rule
                         was not applied or else nil.  Before the rule is
                         :EVALed, (brr@ :failure-reason) is nil.  After
                         :EVALing the rule, (brr@ :failure-reason) is nil
                         if (brr@ :wonp) is t.  Rather than document the
                         various non-nil objects returned as the failure
                         reason, we encourage you simply to evaluate
                         (brr@ :failure-reason) in the contexts of interest.
                         Alternatively, study the ACL2 function tilde-@-
                         failure-reason-phrase.

     :lemma           *  the rewrite rule being broken.  For example,
                         (access rewrite-rule (brr@ :lemma) :lhs) will
                         return the left-hand side of the conclusion
                         of the rule.

     :type-alist      *  a display of the type-alist governing :target.
                         Elements on the displayed list are of the form
                         (term type), where term is a term and type
                         describes information about term assumed to hold
                         in the current context.  The type-alist may be
                         used to determine the current assumptions, e.g.,
                         whether A is a CONSP.

     :ancestors       *  a stack of frames indicating the backchain history
                         of the current context.  The theorem prover is in
                         the process of trying to establish each hypothesis
                         in this stack.  Thus, the negation of each hypothesis
                         can be assumed false.  Each frame also records the
                         rules on behalf of which this backchaining is being
                         done and the weight (function symbol count) of the
                         hypothesis.  All three items are involved in the
                         heuristic for preventing infinite backchaining.
                         Exception:  Some frames are ``binding hypotheses''
                         (equal var term) or (equiv var (double-rewrite term))
                         that bind variable var to the result of rewriting
                         term.

     :gstack          *  the current goal stack.  The gstack is maintained
                         by rewrite and is the data structure printed as the
                         current ``path.''  Thus, any information derivable
                         from the :path brr command is derivable from gstack.
                         For example, from gstack one might determine that
                         the current term is the second hypothesis of a
                         certain rewrite rule.

In general brr@-expressions are used in break conditions, the
expressions that determine whether interactive breaks occur when
monitored runes are applied.  See MONITOR.  For example, you
might want to break only those attempts in which one particular term is
being rewritten or only those attempts in which the binding for the
variable a is known to be a consp.  Such conditions can be expressed
using ACL2 system functions and the information provided by brr@.
Unfortunately, digging some of this information out of the internal
data structures may be awkward or may, at least, require intimate
knowledge of the system functions.  But since conditional expressions
may employ arbitrary functions and macros, we anticipate that a set of
convenient primitives will gradually evolve within the ACL2 community.
It is to encourage this evolution that brr@ provides access to the *'d
data.

MONITOR    to monitor the attempted application of a rule name

     Example:
     (monitor '(:rewrite assoc-of-app) 't)
     :monitor (:rewrite assoc-of-app) t
     :monitor (:definition app) (equal (brr@ :target) '(app c d))

     General Form:
     (monitor rune term)

where rune is a rune and term is a term, called the "break condition."
Rune must be either a :rewrite rune or a :definition rune.

When a rune is monitored any attempt to apply it may result in an
interactive break in an ACL2 "wormhole state." There you will get a
chance to see how the application proceeds.  See BREAK-REWRITE
for a description of the interactive loop entered.  Whether an
interactive break occurs depends on the value of the break condition
expression associated with the monitored rune.

NOTE: Some :rewrite rules are considered "simple abbreviations"; see
SIMPLE.  These can be be monitored, but only at certain times
during the proof.  Monitoring is carried out by code inside the
rewriter but abbreviation rules may be applied by a special purpose
simplifier inside the so-called _preprocess_ phase of a proof.  If you
desire to monitor an abbreviation rule, a warning will be printed
suggesting that you may want to supply the hint :DO-NOT '(PREPROCESS);
see HINTS.  Without such a hint, an abbreviation rule can be
applied during the preprocess phase of a proof, and no such application
will cause an interactive break.

To remove a rune from the list of monitored runes, use unmonitor.  To
see which runes are monitored and what their break conditions are,
evaluate (monitored-runes).

Monitor, unmonitor and monitored-runes are macros that expand into
expressions involving state.  While these macros appear to return the
list of monitored runes this is an illusion.  They all print monitored
rune information to the comment window and then return error triples
instructing ld to print nothing.  It is impossible to return the list
of monitored runes because it exists only in the wormhole state with
which you interact when a break occurs.  This allows you to change the
monitored runes and their conditions during the course of a proof
attempt without changing the state in which the the proof is being
constructed.

Unconditional break points are obtained by using the break condition t.
We now discuss conditional break points.  The break condition, expr,
must be a term that contains no free variables other than state and
that returns a single non-state result.  In fact, the result should be
nil, t, or a true list of commands to be fed to the resulting
interactive break.  Whenever the system attempts to use the associated
rule, expr is evaluated in the wormhole interaction state.  A break
occurs only if the result of evaluating expr is non-nil.  If the result
is a true list, that list is appended to the front of standard-oi and
hence is taken as the initial user commands issued to the interactive
break.

In order to develop effective break conditions it must be possible to
access context sensitive information, i.e., information about the
context in which the monitored rune is being tried.  The brr@ macro may
be used in break conditions to access such information as the term
being rewritten and the current governing assumptions.  This
information is not stored in the proof state but is transferred into
the wormhole state when breaks occur.  The macro form is (brr@ :sym)
where :sym is one of several keyword symbols, including :target (the
term being rewritten), :unify-subst (the substitution that instantiates
the left-hand side of the conclusion of the rule so that it is the
target term), and :type-alist (the governing assumptions).  See
BRR@.

For example,

     ACL2 !>:monitor (:rewrite assoc-of-app)
                     (equal (brr@ :target) '(app a (app b c)))

will monitor (:rewrite assoc-of-app) but will cause an interactive
break only when the target term, the term being rewritten, is (app a
(app b c)).

Because break conditions are evaluated in the interaction environment,
the user developing a break condition for a given rune can test
candidate break conditions before installing them.  For example,
suppose an unconditional break has been installed on a rune, that an
interactive break has occurred and that the user has determined both
that this particular application is uninteresting and that many more
such applications will likely occur.  An appropriate response would be
to develop an expression that recognizes such applications and returns
nil.  Of course, the hard task is figuring out what makes the current
application uninteresting.  But once a candidate expression is
developed, the user can evaluate it in the current context simply to
confirm that it returns nil.

Recall that when a break condition returns a non-nil true list that
list is appended to the front of standard-oi.  For example,

     ACL2 !>:monitor (:rewrite assoc-of-app) '(:go)

will cause (:rewrite assoc-of-app) to be monitored and will make the
break condition be '(:go).  This break condition always evaluates the
non-nil true list (:go).  Thus, an interactive break will occur every
time (:rewrite assoc-of-app) is tried.  The break is fed the command
:go.  Now the command :go causes break-rewrite to (a) evaluate the
attempt to apply the lemma, (b) print the result of that attempt, and
(c) exit from the interactive break and let the proof attempt continue.
Thus, in effect, the above :monitor merely "traces" the attempted
applications of the rune but never causes an interactive break
requiring input from the user.

It is possible to use this feature to cause a conditional break where
the effective break condition is tested *after* the lemma has been
tried.  For example:

     ACL2 !>:monitor (:rewrite lemma12)
                     '(:unify-subst
                       :eval$ nil
                       :ok-if (or (not (brr@ :wonp))
                                  (not (equal (brr@ :rewritten-rhs) '(foo a))))
                       :rewritten-rhs)

causes the following behavior when (:rewrite lemma12) is tried.  A
break always occurs, but it is fed the commands above.  The first,
:unify-subst, causes break-rewrite to print out the unifying
substitution.  Then in response to :eval$ nil the lemma is tried but
with all runes temporarily unmonitored.  Thus no breaks will occur
during the rewriting of the hypotheses of the lemma.  When the attempt
has been made, control returns to break-rewrite (which will print the
results of the attempt, i.e., whether the lemma was applied, if so what
the result is, if not why it failed).  The next command, the :ok-if
with its following expression, is a conditional exit command.  It means
exit break-rewrite if either the attempt was unsuccessful, (not (brr@
:wonp)), or if the result of the rewrite is any term other than (foo
a).  If this condition is met, the break is exited and the remaining
break commands are irrelevant.  If this condition is not met then the
next command, :rewritten-rhs, prints the result of the application
(which in this contrived example is known to be (foo a)).  Finally, the
list of supplied commands is exhausted but break-rewrite expects more
input.  Therefore, it begins prompting the user for input.  The end
result, then, of the above :monitor command is that the rune in
question is elaborately traced and interactive breaks occur whenever it
rewrites its target to (foo a).

We recognize that the above break condition is fairly arcane.  We
suspect that with experience we will develop some useful idioms.  For
example, it is straightforward now to define macros that monitor runes
in the ways suggested by the following names:  trace-rune,
break-if-target-is, and break-if-result-is.  For example, the last
could be defined as

     (defmacro break-if-result-is (rune term)
       `(monitor ',rune
                 '(quote (:eval :ok-if
                                (not (equal (brr@ :rewritten-rhs) ',term))))))

(Note however that the submitted term must be in translated form.)

Since we don't have any experience with this kind of control on lemmas
we thought it best to provide a general (if arcane) mechanism and hope
that the ACL2 community will develop the special cases that we find
most convenient.

MONITORED-RUNES    print the monitored runes and their break conditions

     Example and General Form:
     :monitored-runes

This macro prints a list, each element of which is of the form (rune
expr), showing each monitored rune and its current break condition.

OK-IF    conditional exit from break-rewrite

     Example Form:
     :ok-if (null (brr@ :wonp))

     General Form:
     :ok-if expr

where expr is a term involving no free variables other than state and
returning one non-state result which is treated as Boolean.  This form
is intended to be executed from within break-rewrite (see
BREAK-REWRITE).

Consider first the simple situation that the (ok-if term) is a command
read by break-rewrite.  Then, if the term is non-nil, break-rewrite
exits and otherwise it does not.

More generally, ok-if returns an ACL2 error triple (mv erp val state).
(See LD for more on error triples.)  If any form being
evaluated as a command by break-rewrite returns the triple returned by
(ok-if term) then the effect of that form is to exit break-rewrite if
term is non-nil.  Thus, one might define a function or macro that
returns the value of ok-if expressions on all outputs and thus create a
convenient new way to exit break-rewrite.

The exit test, term, generally uses brr@ to access context sensitive
information about the attempted rule application.  See BRR@.
Ok-if is useful inside of command sequences produced by
break conditions.  See MONITOR.  :ok-if is most useful after an
:eval command has caused break-rewrite to try to apply the rule because
in the resulting break environment expr can access such things as
whether the rule succeeded, if so, what term it produced, and if not,
why.  There is no need to use :ok-if before :evaling the rule since the
same effects could be achieved with the break condition on the rule
itself.  Perhaps we should replace this concept with
:eval-and-break-if?  Time will tell.

UNMONITOR    to stop monitoring a rule name

     Examples:
     (unmonitor '(:rewrite assoc-of-app))
     :unmonitor (:rewrite assoc-of-app)
     :unmonitor :all

     General Forms:
     (unmonitor rune)
     (unmonitor :all)

Here, rune is a rune that is currently among those with break points
installed.  This function removes the break.

Subtle point:  Because you may want to unmonitor a "rune" that is no
longer a rune in the current ACL2 world, we don't actually check this
about rune.  Instead, we simply check that rune is a consp beginning
with a keywordp.  That way, you'll know you've made a mistake if you
try to :unmonitor binary-append instead of :unmonitor (:definition
binary-append), for example.

DOCUMENTATION    functions that display documentation

This section explains the ACL2 online documentation system.  Thus, most
of it assumes that you are typing at the terminal, inside an ACL2
session.  If you are reading this description in another setting (for
example, in a web browser, in Emacs info, or on paper), simply ignore
the parts of this description that involve typing at the terminal.

ACL2 users are welcome to contribute additional documentation.  See the
web page `http://www.cs.utexas.edu/users/moore/acl2/contrib/'.

For an introduction to the ACL2 online documentation system, type :more
below.  Whenever the documentation system concludes with "(type :more
for more, :more! for the rest)" you may type :more to see the next
block of documentation.

Topics related to documentation are documented individually:

To view the documentation in a web browser, open a browser to file
doc/HTML/acl2-doc.html under your ACL2 source directory, or just go to
the ACL2 home page at `http://www.cs.utexas.edu/users/moore/acl2/'.

To use Emacs Info (inside Emacs), first load distributed file
emacs/emacs-acl2.el (perhaps inside your .emacs file) and then execute
meta-x acl2-info.  In order to see true links to external web pages,
you may find the following addition to your .emacs file to be helpful.

     ; For emacs-version 22 or (presumably) later, you can probably set
     ; arrange that in Emacs Info, URLs become links, in the sense that
     ; if you hit <RETURN> while standing on a URL, then you will be
     ; taken to that location in a web browser.  If this does not happen
     ; automatically, then evaluating the `setq' form below might work
     ; if you have firefox.  If that does not work, then you can probably
     ; figure out what to do as follows.  First type
     ;   control-h v browse-url-browser-function
     ; and then from the resulting help page,
     ; hit <return> on the link ``customize'' in:
     ; ``You can customize this variable''
     ; and then follow instructions.
     (setq browse-url-browser-function (quote browse-url-firefox))

There is a print version of the documentation, though we recommend
using one of the other methods (web, Emacs Info, or online) to browse
it.  If you really want the print version, you can find it here:
`http://www.cs.utexas.edu/users/moore/publications/acl2-book.ps.gz'.

Below we focus on how to access the online documentation, but some of
the discussion is relevant to other formats.

The ACL2 online documentation feature allows you to see extensive
documentation on many ACL2 functions and ideas.  You may use the
documentation facilities to document your own ACL2 functions and
theorems.

If there is some name you wish to know more about, then type

     ACL2 !>:doc name

in the top-level loop.  If the name is documented, a brief blurb will
be printed.  If the name is not documented, but is "similar" to some
documented names, they will be listed.  Otherwise, nil is returned.

Every name that is documented contains a one-line description, a few
notes, and some details.  :Doc will print the one-liner and the notes.
When :doc has finished it stops with the message "(type :more for more,
:more! for the rest)" to remind you that details are available.  If you
then type

     ACL2 !>:more

a block of the continued text will be printed, again concluding with
"(type :more for more, :more! for the rest)" if the text continues
further, or concluding with "*-" if the text has been exhausted.  By
continuing to type :more until exhausting the text you can read
successive blocks.  Alternatively, you can type :more! to get all the
remaining blocks.

If you want to get the details and don't want to see the elementary
stuff typed by :doc name, type:

     ACL2 !>:MORE-DOC name

We have documented not just function names but names of certain
important ideas too.  For example, see REWRITE and see
META to learn about :rewrite rules and :meta rules, respectively.
See HINTS to learn about the structure of the :hints argument
to the prover.  The deflabel event (see DEFLABEL) is a way to
introduce a logical name for no reason other than to attach
documentation to it; also see DEFDOC.

How do you know what names are documented?  There is a documentation
data base which is querried with the :docs command.

The documentation data base is divided into sections.  The sections are
listed by

     ACL2 !>:docs *

Each section has a name, sect, and by typing

     ACL2 !>:docs sect

or equivalently

     ACL2 !>:doc sect

you will get an enumeration of the topics within that section.  Those
topics can be further explored by using :doc (and :more) on them.  In
fact the section name itself is just a documented name.  :more
generally gives an informal overview of the general subject of the
section.

     ACL2 !>:docs **

will list all documented topics, by section.  This fills several pages
but might be a good place to start.

If you want documentation on some topic, but none of our names or brief
descriptions seem to deal with that topic, you can invoke a command to
search the text in the data base for a given string.  This is like the
GNU Emacs "apropos" command.

     ACL2 !>:docs "functional inst"

will list every documented topic whose :doc or :more-doc text includes
the substring "functional inst", where case and the exact number of
spaces are irrelevant.

If you want documentation on an ACL2 function or macro and the
documentation data base does not contain any entries for it, there are
still several alternatives.

     ACL2 !>:args fn

will print the arguments and some other relevant information about the
named function or macro.  This information is all gleaned from the
definition (not from the documentation data base) and hence this is a
definitive way to determine if fn is defined as a function or macro.

You might also want to type:

     ACL2 !>:pc fn

which will print the command which introduced fn.  You should see
COMMAND-DESCRIPTOR for details on the kinds of input you can give the
:pc command.

The entire ACL2 documentation data base is user extensible.  That is,
if you document your function definitions or theorems, then that
documentation is made available via the data base and its query
commands.

The implementation of our online documentation system makes use of
Common Lisp's "documentation strings." While Common Lisp permits a
documentation string to be attached to any defined concept, Common Lisp
assigns no interpretation to these strings.  ACL2 attaches special
significance to documentation strings that begin with the characters
":doc-section".  When such a documentation string is seen, it is stored
in the data base and may be displayed via :doc, :more, :docs, etc.
Such documentation strings must follow rigid syntactic rules to permit
their processing by our commands.  These are spelled out elsewhere; see
DOC-STRING.

A description of the structure of the documentation data base may also
be found; see DOC-STRING.

Finally: To build the HTML documentation, proceed with the following
sequence of steps.

     1. In the doc/ subdirectory of the ACL2 distribution, start ACL2
     and then evaluate (certify-book "write-acl2-html").

     2. Exit ACL2 and start it up again (or, evaluate :u).

     3. Include the documented books within your ACL2 loop using
     include-book.

     4. Evaluate (include-book "../doc/write-acl2-html" :dir :system).

     5. Call macro write-html-file, following the instructions at the
     end of distributed file doc/write-acl2-html.lisp.

*TERMINAL-MARKUP-TABLE*    a markup table used for printing to the terminal

The value of the ACL2 constant *terminal-markup-table* is an association
list pairing markup keys with strings, to be used for printing to the
terminal.  See MARKUP for a description of the ACL2 markup
language.

The entries in *terminal-markup-table* are of the form

     (key flag . fmt-string)

where key is one of the doc-string tilde directives (see
MARKUP), flag is a Boolean as described below, and fmt-string is a
string as expected by the ACL2 printing function fmt.  The system
arranges that for any arg, when an expression ~key[arg] is encountered
by the documentation printer, fmt will print fmt-string in an
association list, binding keys based on arg as follows.

     #\p --- the `pointer'     ; only used if flag is t
     #\s --- the print name version of the pointer, e.g., |abc| or ABC
     #\c --- the parent file   ; only used if flag is t
     #\t --- the displayed text
     #\T --- uppercased displayed text

The first three entries are used only when the flag associated with key
is t, indicating that the argument arg of ~key is to be parsed as
starting with a symbol; for example, ~key[foo bar] will bind #\p to the
symbol FOO.

The discussion of the above association list for printing fmt-string
applies when printing documentation to other than the terminal as well.
Such tools exist for Texinfo and for HTML; see files
doc/write-acl2-html.lisp and doc/write-acl2-texinfo.lisp distributed
with ACL2.

ARGS    args, guard, type, constraint, etc., of a function symbol

     Example:
     :args assoc-eq

Args takes one argument, a symbol which must be the name of a function
or macro, and prints out the formal parameters, the guard expression,
the output signature, the deduced type, the constraint (if any), and
whether documentation about the symbol is available via :doc.

DOC    brief documentation (type :doc name)

NOTE:  The :doc command only makes sense at the terminal.  Furthermore
it only works at the terminal when a "full-size" image has been built.
Most users will probably access the ACL2 documentation in other ways,
as explained in the file "doc/README" that comes with the ACL2
distribution.

     Examples:
     ACL2 !>:doc DEFTHM          ; print documentation of DEFTHM
     ACL2 !>:doc logical-name    ; print documentation of LOGICAL-NAME
     ACL2 !>:doc "MY-PKG"      ; print documentation of "MY-PKG"

     Related Topics:
     :more                      ; continues last :doc or :more-doc text
     :more-doc name             ; prints more documentation for name
     :docs **                   ; lists all documented symbols
     :docs "compil"             ; documented symbols apropos "compil"
     :DOC documentation         ; describes how documentation works

     General Form:
     ACL2>:doc logical-name

where logical-name is a logical name (see LOGICAL-NAME) for
which you hope there is documentation.  Chances are there is no
documentation at the moment, but we are working on adding documentation
strings for all the user level ACL2 functions.

For a general discussion of our treatment of documentation strings, see
DOCUMENTATION.

This is the first cut at online documentation.  Users can be
particularly helpful by sending mail on the inadequacies of the system.
Address it just to Moore and put Documentation in the subject line.
There are several things that trouble me about what I've done here.

First, many concepts aren't documented.  Ultimately, I'd like to .
document (a) every CLTL primitive (e.g., case and coerce) and (b) every
ACL2 extension (e.g., aref1 and getprop).  But so far I have focussed
on documenting (c) the ACL2 system primitives (e.g., defthm and what
hints look like).  My priorities are (c), then (b), and then (a),
following the philosophy that the most unstable features should get
online documentation in these early releases.  Having gotten the basic
documentation in place, I'll document new things as they are added, and
in response to your pleas I'll try to add documentation to old things
that are widely regarded as important.

Second, I worry that the existing documentation is unhelpful because it
provides too much or too little detail, or it provides the detail too
far away from where it is needed.  Please be on the lookout for this.
Did you get what you needed when you appealed to :doc or :more-doc?  If
not, what was it you needed?  Would more cross-references help?  Did
you get lost in maze of cross-references?

DOC!    all the documentation for a name (type :doc! name)

NOTE:  The :doc! command only makes sense at the terminal.

     Examples:
     ACL2 !>:doc! defthm
     ACL2 !>:doc! certificate

This command is like :doc name followed by :more!.  It prints all the
documentation of name.

DOC-STRING    formatted documentation strings

     Examples:
     ":Doc-Section name
     one-liner~/notes~/details"

     ":Doc-Section name
     one-liner~/
     notes~/
     details~/
     :cite old-name1
     :cited-by old-name2"

Use (get-doc-string 'name state) to see other examples.

Documentation strings not beginning with ":Doc-Section" (case is
irrelevant) are ignored.  See MARKUP for how to supply
formatting information (such as fonts and displayed text) in
documentation strings.

ACL2 attaches special importance to documentation strings beginning
with the header ":Doc-Section" (or any variant thereof obtained by
changing case).  Any documentation string that does not begin with such
a header is considered unformatted and is ignored.  For the rest of
this discussion, we use the phrase "documentation string" as though it
read "formatted documentation string."

Documentation strings are always processed in the context of some
symbol, name, being defined.  (Indeed, if an event defines no symbol,
e.g., verify-guards or in-theory, then it is not permitted to have a
formatted documentation string.)  The string will be associated with
name in the "documentation data base." The data base is divided into
"sections" and each section is named by a symbol.  Among the sections
are events, documentation, history, other, and miscellaneous.  A
complete list of the sections may be obtained by typing :docs * at the
terminal.  You can create new sections.  The main purpose of sections
is simply to partition the large set of names into smaller subsets
whose contents can be enumerated separately.  The idea is that the user
may remember (or recognize) the relevant section name and then read its
contents to find interesting items.

Within a section are "documentation tuples" which associate with each
documented name its documentation string and a list of related
documented names, called the "related names" of the name.  When :doc
prints the documentation for name, it always lists the related names.

When a formatted documentation string is submitted with the defining
event of some name, the section name and an initial set of related
names are parsed from the string.  In addition, the formatted string
contains various "levels" of detail that are printed out at different
times.  Finally, it is possible for a string to cause the newly
documented name to be added to the related names of any previously
documented name.  Thus, as new names are introduced they can be grouped
with old ones.

The general form of an ACL2 formatted documentation string is

     ":DOC-SECTION <section-name>
       <one-liner>~/
       <notes>~/
       <details>~/
       :CITE <n1>
       ...
       :CITE <nn>
       :CITED-BY <m1>
       ...
       :CITED-BY <mm>"

Before we explain this, let it be noted that (get-doc-string name
state) will return the documentation string associated with name in the
documentation data base.  You may want to call get-doc-string on 'pe
and 'union-theories just to see some concrete documentation strings.
This documentation string, which is rather long, is under 'doc-string.

A formatted documentation string has five parts: the header and
section-name (terminating in the first #\Newline), the <one-liner>,
<notes>, and <details> (each terminating in a tilde-slash ("~/") pair),
and a citation part.  These five parts are parsed into six components.
<section-name> is read as the name of a symbol, section-name.
<one-liner>, <notes>, and <details> are arbitrary sequences of
characters (ignoring initial white space and not including the
tilde-slash pairs which terminate them).  The <ni> are read as symbols
and assembled into a list called the "cite" symbols.  The <mi> are read
as symbols and assembled into a list called the "cited-by" symbols.
See the warning below regarding the hackish nature of our symbol reader.

Section-name must either be a previously documented symbol or else be
name, the symbol being documented.  To open a new section of the data
base, named section-name, you should define the logical name
section-name (as by deflabel or any other event; also see
DEFDOC) and attach to it a documentation string for section
section-name.  You might wish to print out the documentation string we
use for some of our section names, e.g., (get-doc-string 'events
state).  By forcing section names to be documented symbols, we permit
sections themselves to have one line descriptions and discussions,
presented by the standard documentation facilities like the facilities
:doc and :more-doc that may be used at the terminal.

Each of the ni's and mi's must be previously documented symbols.

Both <one-liner> and <details> must be non-empty, i.e., must contain
some non-whitespace characters.  <notes> may be empty.  The :cites and
:cited-bys pairs may be intermingled and may be separated by either
newlines or spaces.  The citation part may be empty.  When the citation
part is empty, the tilde-slash pair terminating the <details> part may
be omitted.  Thus, the simplest form of a formatted documentation
string is:

     ":Doc-Section <section-name>
      <one-liner>~/~/
      <details>"

Since white space at the front of <one-liner>, <notes> and <details> is
ignored, we often precede those parts by #\Newlines to make the strings
easier to read in our source files.  We also typically indent all of
the text in the string by starting each line with a few spaces.  (The
Emacs commands for formatting Lisp get confused if you have arbitrary
characters on the left margin.)  We assume that every line in
<one-liner>, <notes>, and <details> starts with at least as many spaces
as <one-liner> does, i.e., we assume they are all indented the same
amount (or more).  Let d be the number of spaces separating <one-liner>
from the #\Newline preceding it.  When the various parts are printed,
we "de-indent" by stripping out the first d spaces following each
#\Newline.

However, we find that when documentation is printed flush against the
left margin it is difficult to distinguish the documentation text from
previous output.  We therefore prefix each line we print by a special
pad of characters.  By default, this pad is "| " so that documentation
text has a vertical bar running down the left margin.  But the pad is
just the value of the global variable doc-prefix and you may assign it
any string you wish.

To add such a string to the data base under the symbol name we make a
new entry in the section-name section of the data base.  The entry
associates name with the string and uses the string's cites list as the
initial value of the related names field.  In addition, we add name to
the related names field of each of the names listed in the string's
cited-by list.  We also add name to the related names field of its
section-name.  Observe that the cites list in a string is only the
initial value of the related names of the names.  Future documentation
strings may add to it via :cited-by or :doc-section.  Indeed, this is
generally the case.  We discuss this further below.

When a brief description of name is required (as by :docs **), name and
<one-liner> are printed.  <one-liner> is usually printed starting in
column 15 (however see PRINT-DOC-START-COLUMN).  Despite its
name, <one-liner> need not be one line.  It usually is one line,
however.

When you type :doc name at the terminal, the first response will be to
print name and <one-liner>.  Then :doc prints <notes>, if any.  Then,
if name is the name of a section, it prints the <one-liner>s for each
of its related names.  For example, try :doc events.  If name is not a
section name but does have some related names, they are merely listed
but not explained.  Try :doc theory-functions.  :more-doc name prints
<details>.

Our style is to let each new concept add itself to the related names of
old concepts.  To do otherwise increases the chances that documentation
gets outdated because one often forgets to update supposedly complete
lists of the relevant topics when new topics are invented.  For
example, :doc theory-functions lists each available theory function.
But get-doc-string of 'theory-functions just shows a few examples and
has an empty cites list.  From where do we get the names of the theory
functions listed by :doc?  The answer is that each theory function has
its own documentation string and those strings each specify :cited-by
theory-functions.  See for example get-doc-string of 'union-theories.
So by the time the entire system is assembled, the related names of
'theory-functions contains all the (documented) theory functions.  This
makes it easy to add new theory functions without changing the general
discussion in 'theory-functions.

When an event or command form is printed, as by :pe or :pc, that
contains a formatted documentation string, we do not print the actual
documentation string (since they are usually large and distracting).
Instead we print the string:

       "Documentation available via :doc"

inviting you to use :doc and :more-doc (or get-doc-string) if you wish
to see the documentation at the terminal.

_Warning on Reading Symbols from Strings:_ When we read a symbol, such
as the section-symbol, from a documentation string, we use a quick and
dirty imitation of the much more powerful CLTL read program.  In
particular, we scan past any whitespace, collect all the characters we
see until we get to more whitespace or the end of the string, convert
the characters to upper case, make a string out of them, and intern
that string.  Thus, if you typed ":Doc-Section 123 ..." we would read
the 123 as the symbol |123|.  Observe that special characters, such as
parentheses and escape characters, are not afforded their usual
reverence by our hack.  Furthermore, the question arises: in which
package do we intern the symbol?  The answer is, usually, the package
containing the name being defined.  I.e., if you are documenting
my-pkg::name and you attach a documentation string that begins
":Doc-Section: Machines ..." then the section-symbol will be
my-pkg::machines.  We recognize two special cases. If the first
character read is a colon, we use the keyword package.  If the first
five characters read are acl2:: then we intern in the "ACL2" package.
Our own section names, e.g., events, are in the "ACL2" package.

In a related area, when you ask for the documentation of a name, e.g.,
when you type :doc name at the terminal, that name is read with the
full ACL2 reader, not the hack just described.  That name is read into
the current package.  Thus, if you are operating in-package "MY-PKG"
and type :doc events, what is read is my-pkg::events.  The data base
may not contain an entry for this symbol.  Before reporting that no
documentation exists, we try acl2::events.

One last note: defpkg permits a formatted documentation string, which
is associated in the data base with the name of the package.  But the
name of the package is a string, not a symbol.  It is permitted to
access the documentation of a string (i.e., package name).  But there
are no facilities for getting such a stringp name into the related
names of another name nor of making such stringp names be section
names.  That is because we always read symbols from strings and never
read strings from strings.  I.e., if you did write "Doc-Section
\"MY-PKG\" ..." it would read in as a weird symbol.

DOCS    available documentation topics (by section)

NOTE:  The :docs command only makes sense at the terminal.

When the :docs command is given a stringp argument it searches the text
produced by :doc and :more-doc and lists all the documented topics
whose text contains the given string.  For purposes of this string
matching we ignore distinctions of case and the amount and kind (but
not presence) of white space.  We also treat hyphen as whitespace.

However, the following examples show how :docs can be used on other than
string patterns.

     Examples:
     ACL2 !>:docs *           ; lists documentation sections
     ACL2 !>:docs **          ; lists all documented topics within all sections
     ACL2 !>:docs events      ; lists all topics in section EVENTS
     ACL2 !>:docs "compil"    ; lists topics ``apropos''

The data base of formatted documentation strings is structured into
sections.  Within a section are topics.  Each topic has a one-liner,
some notes, and some detailed discussions.  The :docs command provides
a view of the entire data base.

:docs takes one argument, as described below:

     arg               effect

     *                 list all section headings in the data base
     **                list all section headings and all topics within
                       each section
     name              list all topics in the section named name (where
                       name is some symbol other than * and **).  This
                       is always the same as :doc name.
     pattern           list all topics whose :doc or :more-doc text
                       mentions the string pattern.  For purposes of this
                       string matching we ignore distinctions of case and
                       the amount and kind (but not presence) of white
                       space.  We also treat hyphen as whitespace.

HELP    brief survey of ACL2 features

     Example:
     ACL2 !>:help

See LP for general information about the top-level command
environment for ACL2.