This is documentation for ACL2 Version 3.5
Copyright (C) 2009  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.

ACL2-PC||RETAIN    (atomic macro)
drop all *but* the indicated top-level hypotheses

     Example:
     (RETAIN 2 3) -- keep the second and third hypotheses, and drop
                     the rest

     General Form:
     (retain &rest args)

Drop all top-level hypotheses *except* those with the indicated indices.

There must be at least one argument, and all must be in range (i.e.
integers between one and the number of top-level hypotheses, inclusive).

ACL2-PC||RETRIEVE    (macro)
re-enter the proof-checker

     Examples:
     (retrieve associativity-of-permutationp)
     retrieve

     General Form:
     (retrieve &optional name)

Must be used from outside the interactive proof-checker loop.  If name
is supplied and not nil, this causes re-entry to the interactive
proof-checker loop in the state at which save was last executed for the
indicated name.  (See documentation for save.)  If name is nil or is
not supplied, then the user is queried regarding which proof-checker
state to re-enter.  The query is omitted, however, if there only one
proof-checker state is present that was saved with save, in which case
that is the one that is used.  See also unsave.

ACL2-PC||REWRITE    (primitive)
apply a rewrite rule

     Examples:
     (rewrite reverse-reverse)
        -- apply the rewrite rule `reverse-reverse'
     (rewrite (:rewrite reverse-reverse))
        -- same as above
     (rewrite 2)
        -- apply the second rewrite rule, as displayed by show-rewrites
     rewrite
        -- apply the first rewrite rule, as displayed by show-rewrites
     (rewrite transitivity-of-< ((y 7)))
        -- apply the rewrite rule transitivity-of-< with the substitution
           that associates 7 to the ``free variable'' y
     (rewrite foo ((x 2) (y 3)) t)
        -- apply the rewrite rule foo by substituting 2 and 3 for free
           variables x and y, respectively, and also binding all other
           free variables possible by using the current context
           (hypotheses and governors)

     General Form:
     (rewrite &optional rule-id substitution instantiate-free)

Replace the current subterm with a new term by applying a rewrite rule.
The replacement will be done according to the information provided by
the show-rewrites (sr) command.

If rule-id is a positive integer n, then the nth rewrite rule as
displayed by show-rewrites is the one that is applied.  If rule-id is
nil or is not supplied, then it is treated as the number 1.  Otherwise,
rule-id should be either a rune of or name of a rewrite rule.  If a
name is supplied, then any rule of that name may be used.  We say more
about this, and describe the other optional arguments, below.

Consider first the following example.  Suppose that the current subterm
is (reverse (reverse y)) and that there is a rewrite rule called
reverse-reverse of the form

     (implies (true-listp x)
              (equal (reverse (reverse x)) x)) .

Then the instruction (rewrite reverse-reverse) would cause the current
subterm to be replaced by y and would create a new goal with conclusion
(true-listp y).  An exception is that if the top-level hypotheses imply
(true-listp y) using only "trivial reasoning" (more on this below),
then no new goal is created.

If the rule-id argument is a number or is not supplied, then the system
will store an instruction of the form (rewrite name ...), where name is
the name of a rewrite rule; this is in order to make it easier to replay
instructions when there have been changes to the history.  Actually,
instead of the name (whether the name is supplied or calculated), the
system stores the rune if there is any chance of ambiguity.  (Formally,
"ambiguity" here means that the rune being applied is of the form
(:rewrite name . index), where index is not nil.)

Speaking in general, then, a rewrite instruction works as follows:

First, a rewrite rule is selected according to the arguments of the
rewrite instruction.  The selection is made as explained under "General
Form" above.

Next, the left-hand side of the rule is matched with the current
subterm, i.e., a substitution unify-subst is found such that if one
instantiates the left-hand side of the rule with unify-subst, then one
obtains the current subterm.  If this match fails, then the instruction
fails.

Next, an attempt is made to relieve (discharge) the hypotheses, much as
the theorem prover relieves hypotheses except that there is no call to
the rewriter.  First, the substitution unify-subst is extended with the
substitution argument, which may bind free variables (see
FREE-VARIABLES).  Each hypothesis of the rewrite rule is then
considered in turn, from first to last.  For each hypothesis, first the
current substitution is applied, and then the system checks whether the
hypothesis is "clearly" true in the current context.  If there are
variables in the hypotheses of the rewrite rule that are not bound by
the current substitution, then a weak attempt is made to extend that
substitution so that the hypothesis is present in the current context
(see the documentation for the proof-checker hyps command under
proof-checker-commands), much as would be done by the theorem prover's
rewriter.

If in the process above there are free variables, but the proof-checker
can see how to bind them to relieve all hypotheses, then it will do so
in both the show-rewrites (sr) and rewrite commands.  But normally, if
even one hypothesis remains unrelieved, then no automatic extension of
the substitution is made.  Except, if instantiate-free is not nil, then
that extension to the substitution is kept.

Finally, the instruction is applied as follows.  The current subterm is
replaced by applying the final substitution described above to the
right-hand side of the selected rewrite rule.  And, one new subgoal is
created for each unrelieved hypothesis of the rule, whose top-level
hypotheses are the governors and top-level hypotheses of the current
goal and whose conclusion and current subterm are the instance, by that
same final substitution, of that unrelieved hypothesis.

*Remark:*  The substitution argument should be a list whose elements
have the form (variable term), where term may contain abbreviations.

ACL2-PC||RUN-INSTR-ON-GOAL    (macro)
auxiliary to THEN

See documentation for then.

ACL2-PC||RUN-INSTR-ON-NEW-GOALS    (macro)
auxiliary to then

See documentation for then.

ACL2-PC||RUNES    (macro)
print the runes (definitions, lemmas, ...) used

     Examples and general forms:
     (runes t)   ; print all runes used during this interactive proof
     (runes nil) ; print all runes used by the most recent command
     (runes)     ; same as (runes nil)
     runes       ; same as (runes nil)

This command does not change the proof-checker state.  Rather, it
simply reports runes (see RUNE) that have participated in the
interactive proof.

Note that (runes nil) will show the runes used by the most recent
primitive or macro command (as displayed by :comm).

ACL2-PC||S    (primitive)
simplify the current subterm

     Examples:
     S  -- simplify the current subterm
     (S :backchain-limit 2 :normalize t :expand (append x z))
        -- simplify the current subterm, but during the rewriting
           process first ``normalize'' it by pushing IFs to the
           top-level, and also force the term (append x z) to be
           expanded during the rewriting process

     General Form:
     (s &key rewrite normalize backchain-limit repeat in-theory hands-off
             expand)

Simplify the current subterm according to the keyword parameters
supplied.  First if-normalization is applied (unless the normalize
argument is nil), i.e., each subterm of the form (f ... (if test x y)
...)  is replaced by the term (if test (f ... x ...) (f ... y ...))
except, of course, when f is if and the indicated if subterm is in the
second or third argument position.  Then rewriting is applied (unless
the rewrite argument is nil).  Finally this pair of actions is repeated
-- until the rewriting step causes no change in the term.  A
description of each parameter follows.

     :rewrite -- default t

When non-nil, instructs the system to use ACL2's rewriter (or,
something close to it) during simplification.

     :normalize -- default t

When non-nil, instructs the system to use if-normalization (as
described above) during simplification.

     :backchain-limit -- default 0

Sets the number of recursive calls to the rewriter that are allowed for
backchaining.  Even with the default of 0, some reasoning is allowed
(technically speaking, type-set reasoning is allowed) in the relieving
of hypotheses.

     :repeat -- default 0

Sets the number of times the current term is to be rewritten.  If this
value is t, then the default is used (as specified by the constant
*default-s-repeat-limit*).

     :in-theory, :hands-off, :expand

These have their usual meaning; see HINTS.

*Remark:*  if conditional rewrite rules are used that cause case splits
because of the use of force, then appropriate new subgoals will be
created, i.e., with the same current subterm (and address) but with
each new (forced) hypothesis being negated and then used to create a
corresponding new subgoal.  In that case, the current goal will have
all such new hypotheses added to the list of top-level hypotheses.

ACL2-PC||S-PROP    (atomic macro)
simplify propositionally

     Example:
     s-prop

     General Form:
     (s-prop &rest names)

Simplify, using the default settings for s (which include
if-normalization and rewriting without real backchaining), but with
respect to a theory in which only basic functions and rules (the ones in
(theory 'minimal-theory)), together with the names (or parenthesized
names) in the &rest argument names, are enabled.

See also the documentation for s.

ACL2-PC||SAVE    (macro)
save the proof-checker state (state-stack)

     Example:
     (save lemma3-attempt)

     General Form:
     (save &optional name do-it-flg)

Saves the current proof-checker state by "associating" it with the
given name.  Submit (retrieve name) to Lisp to get back to this
proof-checker state.  If verify was originally supplied with an event
name, then the argument can be omitted in favor of that name as the
default.

*Remark* that if a save has already been done with the indicated name
(or the default event name), then the user will be queried regarding
whether to go ahead with the save -- except, if do-it-flg is supplied
and not nil, then there will be no query and the save will be effected.

See also the documentation for retrieve and unsave.

ACL2-PC||SEQUENCE    (meta)
run the given list of instructions according to a multitude of
options

     Example:
     (sequence (induct p prove) t)

See also the definitions of commands do-all, do-strict, protect, and
succeed.

     General Form:
     (sequence
      instruction-list
      &optional
      strict-flg protect-flg success-expr no-prompt-flg no-restore-flg)

Each instruction in the list instruction-list is run, and the
instruction "succeeds" if every instruction in instruction-list
"succeeds".  However, it might "succeed" even if some instructions in
the list "fail"; more generally, the various arguments control a number
of aspects of the running of the instructions.  All this is explained
in the paragraphs below.  First we embark on a general discussion of
the instruction interpreter, including the notions of "succeed" and
"fail".

*Remark:*  The arguments are *not* evaluated, except (in a sense) for
success-expr, as described below.

Each primitive and meta instruction can be thought of as returning an
error triple (in the standard ACL2 sense), say (erp val state).  An
instruction (primitive or meta) "succeeds" if erp is nil and val is not
nil; otherwise it "fails".  (When we use the words "succeed" or "fail"
in this technical sense, we'll always include them in double quotes.)
If an instruction "fails," we say that that the failure is "soft" if
erp is nil; otherwise the failure is "hard".  The sequence command
gives the user control over how to treat "success" and "failure" when
sequencing instructions, though we have created a number of handy macro
commands for this purpose, notably do-all, do-strict and protect.

Here is precisely what happens when a sequence instruction is run.  The
instruction interpreter is run on the instructions supplied in the
argument instruction-list (in order).  The interpreter halts the first
time there is a hard "failure." except that if strict-flg is supplied
and not nil, then the interpreter halts the first time there is any
"failure."  The error triple (erp val state) returned by the sequence
instruction is the triple returned by the last instruction executed
(or, the triple (nil t state) if instruction-list is nil), except for
the following provision.  If success-expr is supplied and not nil, then
it is evaluated with the state global variables erp and val (in ACL2
package) bound to the corresponding components of the error triple
returned (as described above).  At least two values should be returned,
and the first two of these will be substituted for erp and val in the
triple finally returned by sequence.  For example, if success-expr is
(mv erp val), then no change will be made to the error triple, and if
instead it is (mv nil t), then the sequence instruction will "succeed".

That concludes the description of the error triple returned by a
sequence instruction, but it remains to explain the effects of the
arguments protect-flg and no-prompt-flg.

If protect-flg is supplied and not nil and if also the instruction
"fails" (i.e., the error component of the triple is not nil or the
value component is nil), then the state is reverted so that the
proof-checker's state (including the behavior of restore) is set back
to what it was before the sequence instruction was executed.
Otherwise, unless no-restore-flg is set, the state is changed so that
the restore command will now undo the effect of this sequence
instruction (even if there were nested calls to sequence).

Finally, as each instruction in instruction-list is executed, the
prompt and that instruction will be printed, unless the global state
variable print-prompt-and-instr-flg is unbound or nil and the parameter
no-prompt-flg is supplied and not nil.

ACL2-PC||SHOW-ABBREVIATIONS    (macro)
display the current abbreviations

     Examples:
     (show-abbreviations v w)
        -- assuming that v and w currently abbreviate terms,
           then this instruction displays them together with
           the terms they abbreviate
     show-abbreviations
        -- display all abbreviations

See also add-abbreviation and remove-abbreviations.  In particular, the
documentation for add-abbreviation contains a general discussion of
abbreviations.

     General Form:
     (show-abbreviations &rest vars)

Display each argument in vars together with the term it abbreviates (if
any).  If there are no arguments, i.e. the instruction is simply
show-abbreviations, then display all abbreviations together with the
terms they abbreviate.

If the term abbreviated by a variable, say v, contains a proper subterm
that is also abbreviate by (another) variable, then both the
unabbreviated term and the abbreviated term (but not using (? v) to
abbreviate the term) are displayed with together with v.

ACL2-PC||SHOW-REWRITES    (macro)
display the applicable rewrite rules

     Example:
     show-rewrites

     General Form:
     (show-rewrites &optional rule-id enabled-only-flg)

Display rewrite rules whose left-hand side matches the current subterm.
This command shows how the rewrite command can be applied.  If rule-id
is supplied and is a name (non-nil symbol) or a rune, then only the
corresponding rewrite rule(s) will be displayed, while if rule-id is a
positive integer n, then only the nth rule that would be in the list is
displayed.  In each case, the display will point out when a rule is
currently disabled (in the interactive environment), except that if
enabled-only-flg is supplied and not nil, then disabled rules will not
be displayed at all.  Finally, among the free variables of any rule
(those occurring in the rule that do not occur in the left-hand side of
its conclusion), those that would remain free if the rule were applied
will be displayed.  See also the documentation for rewrite.

ACL2-PC||SKIP    (macro)
"succeed" without doing anything

     Example and General Form:
     skip

Make no change in the state-stack, but "succeed".  Same as (sequence
nil).

ACL2-PC||SL    (atomic macro)
simplify with lemmas

     Examples:
     sl
     (sl 3)

     General Form:
     (sl &optional backchain-limit)

Simplify, but with all function definitions disabled (see
FUNCTION-THEORY in the top-level ACL2 loop), except for a few basic
functions (the ones in (theory 'minimal-theory)).  The backchain-limit
has a default of 0, but if is supplied and not nil, then it should be a
nonnegative integer; see the documentation for s.

WARNING: This command completely ignores in-theory commands that are
executed inside the proof-checker.

ACL2-PC||SPLIT    (atomic macro)
split the current goal into cases

     Example:
     split

For example, if the current goal has one hypothesis (or x y) and a
conclusion of (and a b), then split will create four new goals:

     one with hypothesis X and conclusion A
     one with hypothesis X and conclusion B
     one with hypothesis Y and conclusion A
     one with hypothesis Y and conclusion B.

     General Form:
     SPLIT

Replace the current goal by subgoals whose conjunction is equivalent
(primarily by propositional reasoning) to the original goal, where each
such goal cannot be similarly split.

*Remark:*  The new goals will all have their hypotheses promoted; in
particular, no conclusion will have a top function symbol of implies.
Also note that split will fail if there is exactly one new goal created
and it is the same as the existing current goal.

The way split really works is to call the ACL2 theorem prover with only
simplification (and preprocessing) turned on, and with only a few
built-in functions (especially, propositional ones) enabled, namely,
the ones in the list (theory 'minimal-theory).  However, because the
prover is called, type-set reasoning can be used to eliminate some
cases.  For example, if (true-listp x) is in the hypotheses, then
probably (true-listp (cdr x)) will be reduced to t.

ACL2-PC||SR    (macro)
same as SHOW-REWRITES

     Example:
     sr

     General Form:
     (sr &optional rule-id)

See the documentation for show-rewrites, as sr and show-rewrites are
identical.

ACL2-PC||SUCCEED    (macro)
run the given instructions, and "succeed"

     Example:
     (succeed induct p prove)

     General Form:
     (succeed &rest instruction-list)

Run the indicated instructions until there is a hard "failure", and
"succeed".  (See the documentation for sequence for an explanation of
"success" and "failure".)

ACL2-PC||TH    (macro)
print the top-level hypotheses and the current subterm

     Examples:
     th               -- print all (top-level) hypotheses and the current
                         subterm
     (th (1 3) (2 4)) -- print hypotheses 1 and 3 and governors 2 and 4,
                         and the current subterm
     (th (1 3) t)     -- print hypotheses 1 and 3 and all governors, and
                         the current subterm

     General Form:
     (th &optional hyps-indices govs-indices)

Print hypotheses and the current subterm.  The printing of hypotheses
(and perhaps governors) are controlled as in the hyps command; see its
documentation.

Historical note:  The name th is adapted from the Gypsy Verification
Environment, where th abbreviates the command theorem, which says to
print information on the current goal.

ACL2-PC||THEN    (macro)
apply one instruction to current goal and another to new subgoals

     Example:
     (then induct prove)

     General Form:
     (then first-instruction &optional completion must-succeed-flg)

Run first-instruction, and then run completion (another instruction) on
each subgoal created by first-instruction.  If must-succeed-flg is
supplied and not nil, then immediately remove the effects of each
invocation of completion that "fails".

The default for completion is reduce.

ACL2-PC||TOP    (atomic macro)
move to the top of the goal

     Example and General Form:
     top

For example, if the conclusion is (= x (* (- y) z)) and the current
subterm is y, then after executing top, the current subterm will be the
same as the conclusion, i.e., (= x (* (- y) z)).

Top is the same as (up n), where n is the number of times one needs to
execute up in order to get to the top of the conclusion.  The top
command fails if one is already at the top of the conclusion.

See also up, dive, nx, and bk.

ACL2-PC||TYPE-ALIST    (macro)
display the type-alist from the current context

     Examples:
     (type-alist t t) ; display type-alist based on both conclusion and governors
     type-alist       ; same as (type-alist nil t) -- governors only
     (type-alist nil) ; same as (type-alist nil t) -- governors only
     (type-alist t)   ; same as (type-alist t nil) -- conclusion only
     (type-alist nil nil) ; display type-alist without considering
                          ; conclusion or governors

     General Form:
     (type-alist &optional concl-flg govs-flg)

where if govs-flg is omitted, it defaults to (not concl-flg).

Display the current assumptions as a type-alist.  Note that this
display includes the result of forward chaining.

There are two basic reasons contemplated for using this command.

1. The theorem prover has failed (either outside the proof-checker or
using a proof-checker command such as bash or reduce and you want to
debug by getting an idea of what the prover knows about the context.

     a. You really are interested in the context for the current term.
     Include hypotheses and governors (i.e., accounting for tests of
     surrounding if-expressions that must be true or false) but not the
     current conclusion (which the theorem prover's heuristics would
     generally ignore for contextual information).  Command:
     (type-alist nil t) ; equivalently, type-alist or (type-alist nil)

     b. You are not thinking in particular about the current term; you
     just want to get an idea of the context that the prover would
     build at the top-level, for forward-chaining.  Incorporate the
     conclusion but not the governors.  Command:
     (type-alist t nil) ; equivalently, (type-alist t)

2. You intend to use one of the proof-checker-commands that does
simplification, such as s or x, and you want to see the context.  Then
include the surrounding if-term governors but not the goal's
conclusion.  Command:
(type-alist nil t) ; equivalently, type-alist or (type-alist nil)

See TYPE-SET (also see TYPE-PRESCRIPTION) for
information about ACL2's type system, which can assist in understanding
the output of the type-alist command.

ACL2-PC||UNDO    (meta)
undo some instructions

     Examples:
     (undo 7)
     undo

     General Forms:

     (undo n) -- Undo the last n instructions.  The argument n should be
                 a positive integer.

     undo     -- Same as (undo 1).

*Remark:*  To remove the effect of an undo command, use restore.  See
the documentation for details.

*Remark:*  If the argument n is greater than the total number of
interactive instructions in the current session, then (undo n) will
simply take you back to the start of the session.

The undo meta command always "succeeds"; it returns (mv nil t state)
unless its optional argument is supplied and of the wrong type (i.e.
not a positive integer) or there are no instructions to undo.

ACL2-PC||UNSAVE    (macro)
remove a proof-checker state

     Example:
     (unsave assoc-of-append)

     General Form:
     (unsave &optional name)

Eliminates the association of a proof-checker state with name, if name
is supplied and not nil.  The name may be nil or not supplied, in which
case it defaults to the event name supplied with the original call to
verify (if there is one -- otherwise, the instruction "fails" and there
is no change).  The ACL2 function unsave may also be executed outside
the interactive loop, with the same syntax.

See also documentation for save and retrieve.

ACL2-PC||UP    (primitive)
move to the parent (or some ancestor) of the current subterm

     Examples:  if the conclusion is (= x (* (- y) z)) and the
                current subterm is y, then we have:
     up or (up 1) -- the current subterm becomes (- y)
     (up 2)       -- the current subterm becomes (* (- y) z)
     (up 3)       -- the current subterm becomes the entire conclusion
     (up 4)       -- no change; can't go up that many levels

     General Form:
     (up &optional n)

Move up n levels in the conclusion from the current subterm, where n is
a positive integer.  If n is not supplied or is nil, then move up 1
level, i.e., treat the instruction as (up 1).

See also dive, top, nx, and bk.

ACL2-PC||USE    (atomic macro)
use a lemma instance

     Example:
     (USE true-listp-append
          (:instance assoc-of-append (x a) (y b) (z c)))
     -- Add two top-level hypotheses, one the lemma called
        true-listp-append, and the other an instance of the lemma called
        assoc-of-append by the substitution in which x is assigned a, y
        is assigned b, and z is assigned c.

     General Form:
     (use &rest args)

Add the given lemma instances to the list of top-level hypotheses.  See
HINTS for the syntax of :use hints in defthm, which is
essentially the same as the syntax here (see the example above).

This command calls the prove command, and hence should only be used at
the top of the conclusion.

ACL2-PC||WRAP    (atomic macro)
execute the indicated instructions and combine all the new goals

     Example:
     (wrap induct) ; induct, then replace first new goal by the conjunction of all
                   ; the new goals, and drop all new goals after the first

     General Form:
     (wrap &rest instrs)

First the instructions in instrs are executed, as in do-all.  If this
"fails" then no additional action is taken.  Otherwise, the current goal
after execution of instrs is conjoined with all "new" goals, in the
sense that their names are not among the names of goals at the time
instrs was begun.  This conjunction becomes the new current goal and
those "new" goals are dropped.

See the code for the proof-checker command wrap-induct for an example
of the use of wrap.

ACL2-PC||WRAP-INDUCT    (atomic macro)
same as induct, but create a single goal

     Examples:
     wrap-induct
     (wrap-induct t)
     (wrap-induct (append (reverse x) y))

     General Form:
     (wrap-induct &optional term)

The wrap-induct command is identical to the proof-checker induct
command, except that only a single goal is created:  the conjunction of
the base and induction steps.

Note:  The output will generally indicate that more than goal has been
created, e.g.:

     Creating two new goals:  (MAIN . 1) and (MAIN . 2).

However, wrap-induct always creates a unique goal (when it succeeds).  A
subsequent message clarifies this, for example:

     NOTE: Created ONLY one new goal, which is the current goal:
       (MAIN . 1)

ACL2-PC||WRAP1    (primitive)
combine goals into a single goal

     Examples:
     ; Keep (main . 1) and (main . 2) if they exist, as well as the current goal;
     ; and for each other goal, conjoin it into the current goal and delete it:
     (wrap1 ((main . 1) (main . 2)))

     ; As explained below, conjoin all subsequent siblings of the current goal
     ; into the current goal, and then delete them:
     (wrap1)

     General Form:
     (wrap1 &optional kept-goal-names)

If kept-goal-names is not nil, the current goal is replaced by
conjoining it with all goals other than the current goal and those
indicated by kept-goal-names, and those other goals are deleted.  If
kept-goal-names is omitted, then the the current goal must be of the
form (name . n), and the goals to conjoin into the current goal (and
delete) are those with names of the form (name . k) for k >= n.

NOTE: Wrap1 always "succeeds", even if there are no other goals to
conjoin into the current goal (a message is printed in that case), and
it always leaves you with no hypotheses at the top of the current goal's
conclusion (as though top and demote had been executed, if necessary).

Also see proof-checker documentation for wrap (see
PROOF-CHECKER-COMMANDS).

ACL2-PC||X    (atomic macro)
expand and (maybe) simplify function call at the current subterm

     Examples:
     x --  expand and simplify.

For example, if the current subterm is (append a b), then after x the
current subterm will probably be (cons (car a) (append (cdr a) b)) if
(consp a) and (true-listp a) are among the top-level hypotheses and
governors.  If there are no top-level hypotheses and governors, then
after x the current subterm will probably be:

     (if (true-listp x)
         (if x
             (cons (car x) (append (cdr x) y))
           y)
       (apply 'binary-append (list x y))).

     General Form:
     (X &key
        rewrite normalize backchain-limit in-theory hands-off expand)

Expand the function call at the current subterm, and simplify using the
same conventions as with the s command (see documentation for s).

Unlike s, it is permitted to set both :rewrite and :normalize to nil,
which will result in no simplification; see x-dumb.

*Remark* (obscure):  On rare occasions the current address may be
affected by the use of x.  For example, suppose we have the definition

     (defun g (x) (if (consp x) x 3))

and then we enter the proof-checker with

     (verify (if (integerp x) (equal (g x) 3) t)) .

Then after invoking the instruction (dive 2 1), so that the current
subterm is (g x), followed by the instruction x, we would expect the
conclusion to be (if (integerp x) (equal 3 3) t).  However, the system
actually replaces (equal 3 3) with t (because we use the ACL2
term-forming primitives), and hence the conclusion is actually (if
(integerp x) (equal 3 3) t).  Therefore, the current address is put at
(2) rather than (2 1).  In such cases, a warning "NOTE" will be printed
to the terminal.

The other primitive commands to which the above "truncation" note
applies are equiv, rewrite, and s.

ACL2-PC||X-DUMB    (atomic macro)
expand function call at the current subterm, without simplifying

     General Form:
     x-dumb:  expand without simplification.

Same as (expand t new-goals-flg keep-all-guards-flg).  See
documentation for expand.

See also x, which allows simplification.

RETRIEVE    re-enter a (specified) proof-checker state

     Examples:
     (retrieve associativity-of-permutationp)
     retrieve

     General Form:
     (retrieve &optional name)

See ACL2-PC||RETRIEVE, or use (help retrieve) inside the
interactive proof-checker loop.  Also see UNSAVE.

TOGGLE-PC-MACRO    change an ordinary macro command to an atomic macro, or vice-versa

     Example:
     (toggle-pc-macro pro)

Change pro from an atomic macro command to an ordinary one (or
vice-versa, if pro happens to be an ordinary macro command)

     General Form:
     (toggle-pc-macro name &optional new-tp)

If name is an atomic macro command then this turns it into an ordinary
one, and vice-versa.  However, if new-tp is supplied and not nil, then
it should be the new type (the symbol macro or atomic-macro, in any
package), or else there is no change.

UNSAVE    remove a proof-checker state

     Example:
     (unsave assoc-of-append)

     General Form:
     (unsave name)

Eliminates the association of a proof-checker state with name.  See
UNSAVE or see ACL2-PC||UNSAVE.

Also see ACL2-PC||SAVE and see RETRIEVE.

VERIFY    enter the interactive proof checker

For proof-checker command summaries, see PROOF-CHECKER.

     Examples:
     (VERIFY (implies (and (true-listp x) (true-listp y))
                           (equal (append (append x y) z)
                                  (append x (append y z)))))
        -- Attempt to prove the given term interactively.

     (VERIFY (p x)
             :event-name p-always-holds
             :rule-classes (:rewrite :generalize)
             :instructions ((rewrite p-always-holds-lemma)
                            change-goal))
        -- Attempt to prove (p x), where the intention is to call the
           resulting DEFTHM event by the name p-always-holds, with
           rule-classes as indicated.  The two indicated instructions
           will be run immediately to start the proof.

     (VERIFY)
        -- Re-enter the proof-checker in the state at which is was last
           left.

     General Form:
     (VERIFY &OPTIONAL raw-term
             &KEY
             event-name
             rule-classes
             instructions)

Verify is the function used for entering the proof-checker's
interactive loop.

PROOF-TREE    proof tree displays

A view of ACL2 proofs may be obtained by way of "proof tree displays."
The emacs environment is easily customized to provide window-based
proof tree displays that assist in traversing and making sense of the
proof transcript; see PROOF-TREE-EMACS.  Proof tree displays
may be turned on with the command :start-proof-tree and may be turned
off with the command :stop-proof-tree; see START-PROOF-TREE and
see STOP-PROOF-TREE.

Here is an example of a proof tree display, with comments.  Lines
marked with "c" are considered "checkpoints," i.e., goals whose
scrutiny may be of particular value.

     ( DEFTHM PLUS-TREE-DEL ...)    ;currently proving PLUS-TREE-DEL
        1 Goal preprocess   ;"Goal" creates 1 subgoal by preprocessing
        2 |  Goal' simp     ;"Goal'" creates 2 subgoals by simplification
     c  0 |  |  Subgoal 2 PUSH *1   ;"Subgoal 2" pushes "*1" for INDUCT
     ++++++++++++++++++++++++++++++ ;first pass thru waterfall completed
     c  6 *1 INDUCT                 ;Proof by induction of "*1" has
          |  <5 more subgoals>      ; created 6 top-level subgoals.  At
                                    ; this point, one of those 6 has been
                                    ; proved, and 5 remain to be proved.
                                    ; We are currently working on the
                                    ; first of those 5 remaining goals.

See PROOF-TREE-EXAMPLES for many examples that contain proof
tree displays.  But first, we summarize the kinds of lines that may
appear in a proof tree display.  The simplest form of a proof tree
display is a header showing the current event, followed by list of
lines, each having one of the following forms.

         n <goal> <process> ...

Says that the indicated goal created n subgoals using the indicated
process.  Here "..." refers to possible additional information.

     c   n <goal> <process> ...

As above, but calls attention to the fact that this goal is a
"checkpoint" in the sense that it may be of particular interest.  Some
displays may overwrite "c" with ">" to indicate the current checkpoint
being shown in the proof transcript.

          |  <goal> ...
          |  |  <k subgoals>

Indicates that the goal just above this line, which is pointed to by the
rightmost vertical bar ("|"), has k subgoals, none of which have yet
been processed.

          |  <goal> ...
          |  |  <k more subgoals>

As above, except that some subgoals have already been processed.

     ++++++++++++++++++++++++++++++

Separates successive passes through the "waterfall".  Thus, this
"fencepost" mark indicates the start of a new proof by induction or of a
new forcing round.

See PROOF-TREE-EXAMPLES for detailed examples.  To learn how to
turn off proof tree displays or to turn them back on again, see
STOP-PROOF-TREE and see START-PROOF-TREE, respectively. See
CHECKPOINT-FORCED-GOALS to learn how to mark goals as
checkpoints that force the creation of goals in forcing rounds.
Finally, see PROOF-TREE-DETAILS for some points not covered
elsewhere.

CHECKPOINT-FORCED-GOALS    Cause forcing goals to be checkpointed in proof trees

     Example forms:
     (checkpoint-forced-goals t)
     (checkpoint-forced-goals nil)

Also see PROOF-TREE.

By default, goals are not marked as checkpoints by a proof tree display
(as described elsewhere; see PROOF-TREE) merely because they
force some hypotheses, thus possibly contributing to a forcing round.
However, some users may want such behavior, which will occur once the
command (checkpoint-forced-goals t) has been executed.  To return to the
default behavior, use the command (checkpoint-forced-goals nil).

PROOF-TREE-DETAILS    proof tree details not covered elsewhere

See PROOF-TREE for an introduction to proof trees, and for a
list of related topics.  Here we present some details not covered
elsewhere.

1.  When proof tree display is enabled (because the command
:stop-proof-tree has not been executed, or has been superseded by a
later :start-proof-tree command), then time summaries will include the
time for proof tree display.  This time includes the time spent
computing with proof trees, such as the pruning process described
briefly above.  Even when proof trees are not displayed, such as when
their display is turned off in the middle of a proof, this time will be
printed if it is not 0.

2.  When a goal is given a :bye in a proof (see HINTS), it is
treated for the purpose of proof tree display just as though it had
been proved.

3.  Several state global variables affect proof tree display.  (@
proof-tree-indent) is initially the string "| ":  it is the string that
is laid down the appropriate number of times to effect indentation.  (@
proof-tree-buffer-width) is initially the value of
(fmt-soft-right-margin state), and is used to prevent printing of the
annotation "(forced ...)" in any greater column than this value.
However, (assign proof-tree-buffer-width nil) to avoid any such
suppression.  Finally, (@ checkpoint-processors) is a list of processors
from the constant list *preprocess-clause-ledge*, together with
:induct.  You may remove elements of (@ checkpoint-processors) to limit
which processes are considered checkpoints, but note that this can
affect what is printed by gag-mode (see SET-GAG-MODE).

4.  When :otf-flg is not set to t in a proof, and the prover then
decides to revert to the original goal and prove it by induction, the
proof tree display will reflect this fact as shown here:

     c  0 |  |  Subgoal 2 PUSH (reverting)

5. The usual failure message is printed as part of the prooftree display
when a proof has failed.

PROOF-TREE-EMACS    using emacs with proof trees

Within emacs, proof trees provide a sort of structure for the linear
proof transcript output by the ACL2 prover.  Below we explain how to
get proof trees set up in your emacs environment.

To get started, it suffices to load the distributed ACL2 emacs file,
which has lots more than just proof tree support (documented near the
top of that file), as follows.  Thus, you can put the following form in
your ~/.emacs file, where DIR refers to your ACL2 source directory
(typically called acl2-sources/).

     (load "DIR/emacs/emacs-acl2.el")

Then you can start the proof tree display by issuing the following emacs
command:  M-x start-proof-tree.

If you prefer not to load the ACL2 emacs file as shown above, you can
instead put the following forms in your ~/.emacs file (where DIR is as
above) and then issue the above M-x command.

     (setq *acl2-interface-dir*
           "DIR/interface/emacs/")

     (autoload 'start-proof-tree
       (concat *acl2-interface-dir* "top-start-shell-acl2")
       "Enable proof tree logging in a prooftree buffer."
       t)

Once the above is taken care of, then to start using proof trees you do
two things.  In emacs, start a shell (meta-x shell) and evaluate:

        M-x start-proof-tree

Also, in your ACL2, evaluate

       :start-proof-tree

If you want to turn off proof trees, evaluate this in emacs

        M-x stop-proof-tree

and evaluate this in your ACL2 session:

       :stop-proof-tree

When you do M-x start-proof-tree for the first time in your emacs
session, you will be prompted for some information.  You can avoid the
prompt by putting the following in your .emacs file.  The defaults are
as shown, but you can of course change them.

       (setq *acl2-proof-tree-height* 17)
       (setq *checkpoint-recenter-line* 3)
       (setq *mfm-buffer* "*shell*")

Alternatively, you can put the following in your ~/.emacs file in order
to start proof trees without any queries.

       (start-proof-tree-noninteractive "*shell*")

Once you start proof trees (meta-x start-proof-tree), you will have
defined the key bindings shown by executing C-z h in emacs.  Also see
PROOF-TREE-BINDINGS for that additional documentation.

If you want proof-trees to be displayed in a separate emacs frame to the
side, then you can put the following forms in your .emacs file above the
load of emacs-acl2.el described above.  But you may wish to edit the
second form, in particular the number 2048.

     (start-proof-tree-noninteractive "*shell*")
     (cond ((and (eq window-system 'x)
                 (fboundp 'x-display-pixel-width)
                 (= (x-display-pixel-width) 2048) ; for a wide monitor
                 )
            (delete-other-windows)
            (if (boundp 'emacs-startup-hook) ; false in xemacs
                (push 'new-prooftree-frame emacs-startup-hook))))

The file interface/emacs/README-mouse.doc discusses an extension of ACL2
proof trees that allows the mouse to be used with menus.  That
extension may well work, but it is no longer supported.  The basic
proof tree interface, however, is supported and is what is described in
detail elsewhere; see PROOF-TREE.  Thanks to Mike Smith for his
major role in providing emacs support for proof trees.

PROOF-TREE-BINDINGS    using emacs with proof trees

The key bindings set up when you start proof trees are shown below.
See PROOF-TREE-EMACS for how to get started with proof trees.

        C-z h               help
        C-z ?               help

Provides information about proof-tree/checkpoint tool.  Use `C-h d' to
get more detailed information for specific functions.

        C-z c               Go to checkpoint

Go to a checkpoint, as displayed in the "prooftree" buffer with the
character c in the first column.  With non-zero prefix argument: move
the point in the ACL2 buffer (emacs variable *mfm-buffer*) to the first
checkpoint displayed in the "prooftree" buffer, suspend the proof tree
(see suspend-proof-tree), and move the cursor below that checkpoint in
the "prooftree" buffer.  Without a prefix argument, go to the first
checkpoint named below the point in the "prooftree" buffer (or if there
is none, to the first checkpoint).  Note however that unless the proof
tree is suspended or the ACL2 proof is complete or interrupted, the
cursor will be generally be at the bottom of the "prooftree" buffer
each time it is modified, which causes the first checkpoint to be the
one that is found.

If the prefix argument is 0, move to the first checkpoint but do not
keep suspended.

        C-z g               Goto subgoal

Go to the specified subgoal in the ACL2 buffer (emacs variable
*mfm-buffer*) that lies closest to the end of that buffer - except if
the current buffer is "prooftree" when this command is invoked, the
subgoal is the one from the proof whose tree is displayed in that
buffer.  A default is obtained, when possible, from the current line of
the current buffer.

        C-z r               Resume proof tree

Resume original proof tree display, re-creating buffer "prooftree" if
necessary.  See also suspend-proof-tree.  With prefix argument: push the
mark, do not modify the windows, and move point to end of *mfm-buffer*.

        C-z s               Suspend proof tree

Freeze the contents of the "prooftree" buffer, until resume-proof-tree
is invoked.  Unlike stop-proof-tree, the only effect of
suspend-proof-tree is to stop putting characters into the "prooftree"
buffer; in particular, strings destined for that buffer continue NOT to
be put into the primary buffer, which is the value of the emacs variable
*mfm-buffer*.

       C-z o                Select other frame
       C-z b                Switch to "prooftree" buffer
       C-z B                Switch to frame called "prooftree-frame"

These commands move between buffers and frames, as indicated.  The
first of these has nothing specifically to do with proof trees, but is
handy if you have at least two emacs frames displayed.  The second
takes you to the "prooftree" buffer (in the current frame), while the
third takes you to the frame called "prooftree-frame", creating it if
it does not already exist.

PROOF-TREE-EXAMPLES    proof tree example

See PROOF-TREE for an introduction to proof trees, and for a
list of related topics.  Here we present a detailed example followed by
a shorter example that illustrates proof by induction.

Consider the guard proof for the definition of a function
cancel_equal_plus; the body of this definition is of no importance
here.  The first proof tree display is:

     ( DEFUN CANCEL_EQUAL_PLUS ...)
       18 Goal preprocess
          |  <18 subgoals>

This is to be read as follows.

      At this stage of the proof we have encountered the top-level goal,
     named "Goal", which generated 18 subgoals using the  "preprocess"
     process.  We have not yet begun to work on those  subgoals.

The corresponding message from the ordinary prover output is:

      By case analysis we reduce the conjecture to the following 18
     conjectures.

Note that the field just before the name of the goal ("Goal"), which
here contains the number 18, indicates the number of cases (children)
created by the goal using the indicated process.  This number will
remain unchanged as long as this goal is displayed.

The next proof tree display is:

     ( DEFUN CANCEL_EQUAL_PLUS ...)
       18 Goal preprocess
        1 |  Subgoal 18 simp
          |  |  <1 subgoal>
          |  <17 more subgoals>

which indicates that at this point, the prover has used the
simplification ("simp") process on Subgoal 18 to create one subgoal
("<1 subgoal>").  The vertical bar ("|") below "Subgoal 18",
accompanied by the line below it, signifies that there are 17 siblings
of Subgoal 18 that remain to be processed.

The next proof tree displayed is:

     ( DEFUN CANCEL_EQUAL_PLUS ...)
       18 Goal preprocess
        1 |  Subgoal 18 simp
     c  2 |  |  Subgoal 18' ELIM
          |  |  |  <2 subgoals>
          |  <17 more subgoals>

Let us focus on the fourth line of this display:

     c  2 |  |  Subgoal 18' ELIM

The "c" field marks this goal as a "checkpoint", i.e., a goal worthy of
careful scrutiny.  In fact, any goal that creates children by a process
other than "preprocess" or "simp" is marked as a checkpoint.  In this
case, the destructor-elimination ("ELIM") process has been used to
create subgoals of this goal.  The indentation shows that this goal,
Subgoal 18', is a child of Subgoal 18.  The number "2" indicates that 2
subgoals have been created (by ELIM).  Note that this information is
consistent with the line just below it, which says "<2 subgoals>".

Finally, the last line of this proof tree display,

          |  <17 more subgoals>

is connected by vertical bars ("|") up to the string "Subgoal 18",
which suggests that there are 17 immediate subgoals of Goal remaining to
process after Subgoal 18.  Note that this line is indented one level
from the second line, which is the line for the goal named "Goal".  The
display is intended to suggest that the subgoals of Goal that remain to
be proved consist of Subgoal 18 together with 17 more subgoals.

The next proof tree display differs from the previous one only in that
now, Subgoal 18' has only one more subgoal to be processed.

     ( DEFUN CANCEL_EQUAL_PLUS ...)
       18 Goal preprocess
        1 |  Subgoal 18 simp
     c  2 |  |  Subgoal 18' ELIM
          |  |  |  <1 more subgoal>
          |  <17 more subgoals>

Note that the word "more" in "<1 more subgoal>" tells us that there was
originally more than one subgoal of Subgoal 18.  In fact that
information already follows from the line above, which (as previously
explained) says that Subgoal 18' originally created 2 subgoals.

The next proof tree display occurs when the prover completes the proof
of that "1 more subgoal" referred to above.

     ( DEFUN CANCEL_EQUAL_PLUS ...)
       18 Goal preprocess
          |  <17 more subgoals>

Then, Subgoal 17 is processed and creates one subgoal, by
simplification:

     ( DEFUN CANCEL_EQUAL_PLUS ...)
       18 Goal preprocess
        1 |  Subgoal 17 simp
          |  |  <1 subgoal>
          |  <16 more subgoals>

... and so on.

Later in the proof one might find the following successive proof tree
displays.

     ( DEFUN CANCEL_EQUAL_PLUS ...)
       18 Goal preprocess
          |  <9 more subgoals>

     ( DEFUN CANCEL_EQUAL_PLUS ...)

       18 Goal preprocess
        0 |  Subgoal 9 simp (FORCED)
          |  <8 more subgoals>

These displays tell us that Subgoal 9 simplified to t (note that the
"0" shows clearly that no subgoals were created), but that some rule's
hypotheses were forced.  Although this goal is not checkpointed (i.e.,
no "c" appears on the left margin), one can cause such goals to be
checkpointed; see CHECKPOINT-FORCED-GOALS.

In fact, the proof tree displayed at the end of the "main proof"(the
0-th forcing round) is as follows.

     ( DEFUN CANCEL_EQUAL_PLUS ...)
       18 Goal preprocess
        0 |  Subgoal 9 simp (FORCED)
        0 |  Subgoal 8 simp (FORCED)
        0 |  Subgoal 7 simp (FORCED)
        0 |  Subgoal 6 simp (FORCED)
        0 |  Subgoal 4 simp (FORCED)
        0 |  Subgoal 3 simp (FORCED)

This is followed by the following proof tree display at the start of
the forcing round.

       18 Goal preprocess
        0 |  Subgoal 9 simp (FORCED [1]Subgoal 4)
        0 |  Subgoal 8 simp (FORCED [1]Subgoal 6)
        0 |  Subgoal 7 simp (FORCED [1]Subgoal 1)
        0 |  Subgoal 6 simp (FORCED [1]Subgoal 3)
        0 |  Subgoal 4 simp (FORCED [1]Subgoal 5)
        0 |  Subgoal 3 simp (FORCED [1]Subgoal 2)
     ++++++++++++++++++++++++++++++
        6 [1]Goal FORCING-ROUND
        2 |  [1]Subgoal 6 preprocess
          |  |  <2 subgoals>
          |  <5 more subgoals>

This display shows which goals to "blame" for the existence of each
goal in the forcing round.  For example, Subgoal 9 is to blame for the
creation of [1]Subgoal 4.

Actually, there is no real goal named "[1]Goal".  However, the line

        6 [1]Goal FORCING-ROUND

appears in the proof tree display to suggest a "parent" of the six
top-level goals in that forcing round.  As usual, the numeric field
before the goal name contains the original number of children of that
(virtual, in this case) goal -- in this case, 6.

In our example proof, Subgoal 6 eventually gets proved, without doing
any further forcing.  At that point, the proof tree display looks as
follows.

     ( DEFUN CANCEL_EQUAL_PLUS ...)
       18 Goal preprocess
        0 |  Subgoal 9 simp (FORCED [1]Subgoal 4)
        0 |  Subgoal 7 simp (FORCED [1]Subgoal 1)
        0 |  Subgoal 6 simp (FORCED [1]Subgoal 3)
        0 |  Subgoal 4 simp (FORCED [1]Subgoal 5)
        0 |  Subgoal 3 simp (FORCED [1]Subgoal 2)
     ++++++++++++++++++++++++++++++
        6 [1]Goal FORCING-ROUND
          |  <5 more subgoals>

Notice that the line for Subgoal 8,

        0 |  Subgoal 8 simp (FORCED [1]Subgoal 6)

no longer appears.  That is because the goal [1]Subgoal 6 has been
proved, along with all its children; and hence, the proof of Subgoal 8
no longer depends on any further reasoning.

The final two proof tree displays in our example are as follows.

     ( DEFUN CANCEL_EQUAL_PLUS ...)
       18 Goal preprocess
        0 |  Subgoal 7 simp (FORCED [1]Subgoal 1)
     ++++++++++++++++++++++++++++++
        6 [1]Goal FORCING-ROUND
        2 |  [1]Subgoal 1 preprocess
        1 |  |  [1]Subgoal 1.1 preprocess
        1 |  |  |  [1]Subgoal 1.1' simp
     c  3 |  |  |  |  [1]Subgoal 1.1'' ELIM
          |  |  |  |  |  <1 more subgoal>

     ( DEFUN CANCEL_EQUAL_PLUS ...)
     <<PROOF TREE IS EMPTY>>

The explanation for the empty proof tree is simple: once [1]Subgoal
1.1.1 was proved, nothing further remained to be proved.  In fact, the
much sought-after "Q.E.D." appeared shortly after the final proof tree
was displayed.

Let us conclude with a final, brief example that illustrates proof by
induction.  Partway through the proof one might come across the
following proof tree display.

     ( DEFTHM PLUS-TREE-DEL ...)
        1 Goal preprocess
        2 |  Goal' simp
     c  0 |  |  Subgoal 2 PUSH *1
          |  |  <1 more subgoal>

This display says that in the attempt to prove a theorem called
plus-tree-del, preprocessing created the only child Goal' from Goal, and
Goal' simplified to two subgoals.  Subgoal 2 is immediately pushed for
proof by induction, under the name "*1".  In fact if Subgoal 1
simplifies to t, then we see the following successive proof tree
displays after the one shown above.

     ( DEFTHM PLUS-TREE-DEL ...)
        1 Goal preprocess
        2 |  Goal' simp
     c  0 |  |  Subgoal 2 PUSH *1

     ( DEFTHM PLUS-TREE-DEL ...)
        1 Goal preprocess
        2 |  Goal' simp
     c  0 |  |  Subgoal 2 PUSH *1
     ++++++++++++++++++++++++++++++
     c  6 *1 INDUCT
          |  <5 more subgoals>

The separator "+++++..." says that we are beginning another trip through
the waterfall.  In fact this trip is for a proof by induction (as
opposed to a forcing round), as indicated by the word "INDUCT".
Apparently *1.6 was proved immediately, because it was not even
displayed; a goal is only displayed when there is some work left to do
either on it or on some goal that it brought (perhaps indirectly) into
existence.

Once a proof by induction is completed, the "PUSH" line that refers to
that proof is eliminated ("pruned").  So for example, when the present
proof by induction is completed, the line

     c  0 |  |  Subgoal 2 PUSH *1

is eliminated, which in fact causes the lines above it to be eliminated
(since they no longer refer to unproved children).  Hence, at that
point one might expect to see:

     ( DEFTHM PLUS-TREE-DEL ...)
     <<PROOF TREE IS EMPTY>>

However, if the proof by induction of *1 necessitates further proofs by
induction or a forcing round, then this "pruning" will not yet be done.

START-PROOF-TREE    start displaying proof trees during proofs

Also see PROOF-TREE and see STOP-PROOF-TREE.  Note that
:start-proof-tree works by removing 'proof-tree from the
inhibit-output-lst; see SET-INHIBIT-OUTPUT-LST.

Explanations of proof tree displays, including emacs support, may be
found elsewhere; see PROOF-TREE and see
PROOF-TREE-EMACS.  In a nutshell: :start-proof-tree causes proof tree
display to be turned on, once it has been turned off by
:stop-proof-tree.

Do not attempt to invoke start-proof-tree during an interrupt in the
middle of a proof.

STOP-PROOF-TREE    stop displaying proof trees during proofs

Also see PROOF-TREE and see START-PROOF-TREE.  Note that
:stop-proof-tree works by adding 'proof-tree to the inhibit-output-lst;
see SET-INHIBIT-OUTPUT-LST.

Proof tree displays are explained in the documentation for proof-tree.
:Stop-proof-tree causes proof tree display to be turned off.

It is permissible to submit the form (stop-proof-tree) during a break.
Thus, you can actually turn off proof tree display in the middle of a
proof by interrupting ACL2 and submitting the form (stop-proof-tree) in
raw Lisp.

Pages Written Especially for the Tours    Pages Written Especially for the Tours

The ACL2 Home Page is generated from ACL2's online documentation
strings.  (How else could we achieve the total integration of ACL2's
online documentation with the home page?)  This page is just an
artifact of the structure of our documentation strings:  each string
must belong to a "major section" of the documentation database.  This
page is not structured to be used by a person browsing via the Web.  It
contains, in an arbitrary order, the pages written specificially for
the Web user.

Furthermore, browsing the pages below via the ACL2 :DOC command or via
TexInfo is often unsatisfying because those browsers do not support gif
files and the notion of going "back" to a node just visited.  If you
wish to look at the pages below, we strongly recommend that you do so
via a HTML-based Web browser.  Indeed, you should simply visit ACL2's
Home Page and take one of the Tours.

Generally, the topics listed above will not be of use to the ACL2 user.

A Flying Tour of ACL2    A Flying Tour of ACL2

Next on the Flying Tour:  About the ACL2 Home Page

On this tour you will learn a little about what ACL2 is for rather than
how ACL2 works.  At the top and bottom bottom of the "page" (which may
extend beyond the end of your screen) there is a small "flying tour"
icon.  Click on either icon to go to the next page of the tour.

The tour visits the following topics sequentially.

     The Flight Plan
     * This Documentation
     * What is ACL2?
     * Mathematical Logic
     * Mechanical Theorem Proving
     * Mathematical Models in General
     * Mathematical Models of Computing Machines
          Formalizing Models
          Running Models
          Symbolic Execution of Models
          Proving Theorems about Models
     * Requirements of ACL2
          The User's Skills
          Training
          Host System

We intend the tour to take about 10 minutes of your time.  Some pages
on the tour contain pointers to other documents.  You need not follow
these pointers to stay on the tour.

Next on the Flying Tour:  About the ACL2 Home Page

A Sketch of How the Rewriter Works    A Sketch of How the Rewriter Works

Below we show the first target term, extracted from the current
conjecture.  Below it we show the associativity rule.

The variables of the rewrite rule are instantiated so that the
left-hand side of the rule matches the target:

          variable          term from target
            a                     x1
            b                     x2
            c                     (app x3 x4)

Then the target is replaced by the instantiated right-hand side of the
rule.

Sometimes rules have hypotheses.  To make a long story short, if the
rule has hypotheses, then after matching the left-hand side, the
rewriter instantiates the hypotheses and rewrites them recursively.
This is called backchaining.  If they all rewrite to true, then the
target is replaced as above.

For more details on how the ACL2 rewriter works, see Boyer and Moore's
book A Computational Logic, Academic Press, 1979.

A Tiny Warning Sign    A Tiny Warning Sign

This warning sign, which usually appears as "",  indicates that the
link it marks takes you into ACL2's online  documentation.

The documentation is a vast graph of documented topics intended to
help the _user_ of ACL2 rather than the _potential user_.  If  you are
exploring ACL2's home page to learn about the system,  perhaps you
should go back rather than follow the link marked with  this sign.  But
you are welcome to explore the online documentation  as well.  Good
luck.

A Trivial Proof    A Trivial Proof

A Typical State    A Typical State

Next on the Flying Tour:  Functions for Manipulating these Objects

Observe that the states in typical models talk about

     booleans    integers   vectors     records   caches
     bits        symbols    arrays      stacks    files
     characters  strings    sequences   tables    directories

These objects are discrete rather than continuous; furthermore they are
built incrementally or inductively by repeatedly using primitive
operations to put together smaller pieces.

The functions we need to manipulate these objects do things like
concatenate, reverse, sort, search, count, etc.

Next on the Flying Tour:  Functions for Manipulating these Objects

A Walking Tour of ACL2    A Walking Tour of ACL2

Next on the Walking Tour:  Common Lisp

On this tour you will learn a little more about the ACL2 logic, the
theorem prover, and the user interface.

This time we will stick with really simple things, such as the
associativity of list concatenation.

We assume you have taken the Flying Tour but that you did not
necessarily follow all the "off-tour" links.  So this tour may revisit
some pages you've seen.  Just follow the Walking Tour icon at the top
or bottom of each page.

On this tour you will see many more links marked <>.  We would like to
discourage you from following these links right now.  However we
encourage you to note them.  Basically, the <> sign here illustrates
the documentation and introduces you to its main entry points.  Once
you have started to use ACL2 you can take the Walking Tour again but
pursue more of the indicated links.

Next on the Walking Tour:  Common Lisp

ACL2 Characters    ACL2 Characters

ACL2 accepts 256 distinct characters, which are the characters
obtained by applying the function code-char <> to each  integer from 0
to 255.  Among these, Common Lisp designates certain  ones as
*standard-characters*, namely those of the form  (code-char n) where n
is from 33 to 126, together with  #\Newline and #\Space.  The actual
standard characters may  be viewed by evaluating the constant expression
*standard-chars*.

The standard character constants are written by writing a hash mark
followed by a backslash (#\) followed by the character.

The function characterp <> recognizes characters.  For more  details,
See CHARACTERS <>.

ACL2 Conses or Ordered Pairs    ACL2 Conses or Ordered Pairs

The function cons <> creates an ordered pair.  Car <> and cdr <> return
the first and second components, respectively, of an ordered pair.  The
function consp <> recognizes ordered pairs.

Ordered pairs are used to represent lists and trees.  See any Common
Lisp documentation for a discussion of how list constants are written
and for the many list processing functions available.  Also, see
PROGRAMMING <> where we list all the ACL2 primitive functions.

Here are some examples of list constants to suggest their syntax.

     '(a . b)                ; a pair whose car is 'a and cdr is 'b
     '(a . nil)              ; a pair whose car is 'a and cdr is nil
     '(a)                    ; another way to write the same thing
     '(a b)                  ; a pair whose car is 'a and cdr is '(b)
     '(a b c)                ; a pair whose car is 'a and cdr is '(b c)
                             ;  i.e., a list of three symbols, a, b, and c.
     '((a . 1) (b . 2))      ; a list of two pairs

It is useful to distinguish "proper" conses from "improper" ones, the
former being those cons trees whose right-most branch terminates with
nil.  A "true list" (see TRUE-LISTP <>) is either nil or a
proper cons.  (A b c . 7) is an improper cons and hence not a true list.

ACL2 Strings    ACL2 Strings

Strings of ACL2 characters are written as sequences of characters
delimited by "double quotation marks" (").  To put a double quotation
mark in a string (or, any other character such as backslash or newline
that seems to cause problems), escape it by preceding it with a
backslash (\).

The function stringp <> recognizes strings and char <> will fetch the
nth character of a string.  There are many other primitives for
handling strings, such as string< <> for comparing two strings
lexicographically.  We suggest you See PROGRAMMING <> where we
list all of the primitive ACL2 functions.  Alternatively, see any
Common Lisp language documentation.

ACL2 Symbols    ACL2 Symbols

Common Lisp's symbols are a data type representing words.  They are
frequently regarded as atomic objects in the sense that they are not
frequently broken down into their constituents.  Often the only
important properties of symbols is that they are not numbers,
characters, strings, or lists and that two symbols are not equal if
they look different (!).  Examples of symbols include PLUS and
SMITH::ABC.  All function and variable names in ACL2 are symbols.  When
symbols are used as constants they must be quoted, as in 'PLUS.

The symbol T is commonly used as the Boolean "true."  The symbol NIL is
commonly used both as the Boolean "false" and as the "empty list."
Despite sometimes being called the "empty list" NIL is a symbol not an
"empty cons."  Unlike other symbols, T and NIL may be used as constants
without quoting them.

Usually, symbols are written as sequences of alphanumeric characters
other than those denoting numbers.  Thus, A12, +1A and 1+ are symbols
but +12 is a number.  Roughly speaking, when symbols are read lower
case characters are converted to upper case, so we frequently do not
distinguish ABC from Abc or abc.  See Conversion for
information about case conversion when symbols are read.  However, any
character can be used in a symbol, but some characters must be
"escaped" to allow the Lisp reader to parse the sequence as a symbol.
For example, |Abc| is a symbol whose first character is capitalized and
whose remaining characters are in lower case.  |An odd duck| is a symbol
containing two #\Space characters.  See any Common Lisp documentation
for the syntactic rules for symbols.

Technically, a symbol is a special kind of pair consisting of a package
name (which is a string) and a symbol name (which is also a string).
(See SYMBOL-PACKAGE-NAME <> and see SYMBOL-NAME <>.)
The symbol SMITH::ABC is said to be in package "SMITH" and to have the
symbol name "ABC".  The symbol ABC in package "SMITH" is generally not
equal to the symbol ABC in package "JONES".  However, it is possible to
"import" symbols from one package into another one, but in ACL2 this
can only be done when the package is created.  (See DEFPKG <>.)
If the current-package <> is "SMITH" then SMITH::ABC may be more
briefly written as just ABC.  Intern <> "creates" a symbol of a given
name in a given package.

ACL2 System Architecture    ACL2 System Architecture

Next on the Walking Tour:  Rewrite Rules are Generated from DEFTHM Events

The user interacts with the theorem prover by giving it definitions,
theorems and advice (e.g., "use this lemma."), often in the form of
books books <>.

The theorem prover uses the rules in the library of books the user has
selected.

The theorem prover prints its proof attempts to the user.

When a theorem is proved it is converted to a rule under the control of
the user's rule-classes <>.

The informed user can make ACL2 do amazing things.

Next on the Walking Tour:  Rewrite Rules are Generated from DEFTHM Events

ACL2 as an Interactive Theorem Prover    ACL2 as an Interactive Theorem Prover

The ACL2 theorem prover finds proofs in the ACL2 logic.  It can be
automatic.  But most often the user must help it.

The user usually guides ACL2 by suggesting that it first prove key
lemmas.  Lemmas are just theorems used in the proofs of other theorems.

See ACL2 as an Interactive Theorem Prover (cont) to continue.

ACL2 as an Interactive Theorem Prover (cont)    ACL2 as an Interactive Theorem Prover (cont)

Next on the Walking Tour:  ACL2 System Architecture

Theorems, lemmas, definitions, and advice of various sorts can be
stored in books <>.

When a theorem or definition is stored in a book, the user can specify
how it should be used in the future.  When viewed this way, theorems
and definitions are thought of as rules.

The ACL2 theorem prover is rule driven.  The rules are obtained from
books.

See ACL2 System Architecture to continue.

Next on the Walking Tour:  ACL2 System Architecture

ACL2 is an Untyped Language    ACL2 is an Untyped Language

The example

     ACL2 !>(app '(a b c) 27)
     (A B C . 27)

illustrates the fact that ACL2's logic is untyped (see About Types
for a brief discussion of the typed versus untyped nature of
the logic).

The definition of app makes no restriction of the arguments to lists.
The definition says that if the first argument satisfies endp <> then
return the second argument.  In this example, when app has recursed
three times down the cdr of its first argument, '(a b c), it reaches
the final nil, which satisfies endp, and so 27 is returned.  It is
naturally consed into the emerging list as the function returns from
successive recursive calls (since cons does not require its arguments
to be lists, either).  The result is an "improper" list, (a b c . 27).

You can think of (app x y) as building a binary tree by replacing the
right-most tip of the tree x with the tree y.

About Models    About Models

Next on the Flying Tour:  Models of Computer Hardware and Software

ACL2 is used to construct mathematical models of computer hardware and
software (i.e., "digital systems").

A mathematical model is a set of mathematical formulas used to predict
the behavior of some artifact.

The use of mathematical models allows faster and cheaper delivery of
better systems.

Models need not be complete or perfectly accurate to be useful to the
trained engineer.

See Models in Engineering for more discussion of these
assertions in an engineering context.

Next on the Flying Tour:  Models of Computer Hardware and Software

About Types    About Types

The universe of ACL2 objects includes objects of many different types.
For example, t is a "symbol" and 3 is an "integer."  Roughly speaking
the objects of ACL2 can be partitioned into the following types:

     Numbers                   3, -22/7, #c(3 5/2)
     Characters                #\A, #\a, #\Space
     Strings                   "This is a string."
     Symbols                   'abc, 'smith::abc
     Conses (or Ordered Pairs) '((a . 1) (b . 2))

When proving theorems it is important to know the types of object
returned by a term.  ACL2 uses a complicated heuristic algorithm,
called type-set <>, to determine what types of objects a  term may
produce.  The user can more or less program the  type-set algorithm by
proving type-prescription <>  rules.

ACL2 is an "untyped" logic in the sense that the syntax is not  typed:
It is legal to apply a function symbol of n arguments to any  n terms,
regardless of the types of the argument terms.  Thus, it is  permitted
to write such odd expressions as (+ t 3) which sums the  symbol t and
the integer 3.  Common Lisp does not prohibit such  expressions.  We
like untyped languages because they are simple to  describe, though
proving theorems about them can be awkward because,  unless one is
careful in the way one defines or states things,  unusual cases (like
(+ t 3)) can arise.

To make theorem proving easier in ACL2, the axioms actually define a
value for such terms.  The value of (+ t 3) is 3; under the ACL2
axioms, non-numeric arguments to + are treated as though they  were 0.

You might immediately wonder about our claim that ACL2 is Common  Lisp,
since (+ t 3) is "an error" (and will sometimes even  "signal an
error") in Common Lisp.  It is to handle this problem that  ACL2 has
guards.  We will discuss guards later in the Walking Tour.   However,
many new users simply ignore the issue of guards entirely.

You should now return to the Walking Tour.

About the ACL2 Home Page    About the ACL2 Home Page

Next on the Flying Tour:  What Is ACL2(Q)

The ACL2 Home Page is integrated into the ACL2 online documentation.
Over 1.5 megabytes of text is available here.

The vast majority of the text is user-level documentation.  For
example, to find out about rewrite <> rules you could click on the word
"rewrite <>."  But before you do that remember that you must then use
your browser's back commands to come back here.

The tiny warning signs <> mark pointers that lead out of the
introductory-level material and into the user documentation.  If you are
taking the Flying Tour, we advise you to avoid following such pointers
the first time; it is easy to get lost in the full documentation unless
you are pursuing the answer to a specific question.  If you do wander
down these other paths, remember you can back out to a page containing
the Flying Tour icon to resume the tour.

At the end of the tour you will have a chance to return to The Flight
Plan where you can revisit the main stops of the Flying Tour and
explore the alternative paths more fully.

Finally, every page contains two icons at the bottom.  The ACL2 icon
leads you back to the ACL2 Home Page.  The Index icon allows you to
browse an alphabetical listing of all the topics in ACL2's online
documentation.

Next on the Flying Tour:  What Is ACL2(Q)

About the Admission of Recursive Definitions    About the Admission of Recursive Definitions

You can't just add any formula as an axiom or definition and expect the
logic to stay sound!  The purported "definition" of APP must have
several properties to be admitted to the logic as a new axiom

The key property a recursive definition must have is that the recursion
terminate.  This, along with some syntactic criteria, ensures us that
there exists a function satisfying the definition.

Termination must be proved before the definition is admitted.  This is
done in general by finding a measure of the arguments of the function
and a well-founded relation such that the arguments "get smaller" every
time a recursive branch is taken.

For app the measure is the "size" of the first argument, x, as
determined by the primitive function acl2-count <>.  The well-founded
relation used in this example is o-p <>, which is the standard ordering
on the ordinals less than "epsilon naught."  These particular choices
for app were made "automatically" by ACL2.  But they are in fact
determined by various "default" settings.  The user of ACL2 can change
the defaults or specify a "hint" to the defun <> command to specify the
measure and relation.

You should now return to the Walking Tour.

About the Prompt    About the Prompt

The string "ACL2 !>" is the ACL2 prompt.

The prompt tells the user that an ACL2 command <>is expected.  In
addition, the prompt tells us a little about the current state of the
ACL2 command interpreter.  We explain the prompt briefly below.  But
first we talk about the command interpreter.

An ACL2 command is generally a Lisp expression to be evaluated.  There
are some unusual commands (such as :q <> for quitting ACL2) which cause
other behavior.  But most commands are read, evaluated, and then have
their results printed.  Thus, we call the command interpreter a
"read-eval-print loop."  The ACL2 command interpreter is named LD <>
(after Lisp's "load").

A command like (defun app (x y) ...) causes ACL2 to evaluate the defun
<> function on app, (x y) and ....  When that command is evaluated it
prints some information to the terminal explaining the processing of
the proposed definition.  It returns the symbol APP as its value, which
is printed by the command interpreter.  (Actually, defun is not a
function but a macro which expands to a form that involves state <>, a
necessary precondition to printing output to the terminal and to
"changing" the set of axioms.  But we do not discuss this further here.)

The defun command is an example of a special kind of command called an
"event."  Events <> are those commands that change the "logical world"
by adding such things as axioms or theorems to ACL2's data base.  See
WORLD <>.  But not every command is an event command.

A command like (app '(1 2 3) '(4 5 6 7)) is an example of a non-event.
It is processed the same general way:  the function app is applied to
the indicated arguments and the result is printed.  The function app
does not print anything and does not change the "world."

A third kind of command are those that display information about the
current logical world or that "backup" to previous versions of the
world.  Such commands are called "history" <> commands.

What does the ACL2 prompt tell us about the read-eval-print loop?  The
prompt "ACL2 !>" tells us that the command will be read with
current-package <> set to "ACL2", that guard checking (see
SET-GUARD-CHECKING <>) is on ("!"), and that we are at the top-level
(there is only one ">").  For more about the prompt, see
DEFAULT-PRINT-PROMPT <>.

You should now return to the Walking Tour.

An Example Common Lisp Function Definition    An Example Common Lisp Function Definition

Next on the Walking Tour:  An Example of ACL2 in Use

Consider the binary trees x and y below.

In Lisp, x is written as the list '(A B) or, equivalently, as '(A B .
NIL).  Similarly, y may be written '(C D E).  Suppose we wish to
replace the right-most tip of x by the entire tree y.   This is denoted
(app x y), where app stands for "append".

We can define app with:

     (defun app (x y)                           ; Concatenate x and y.
       (declare (type (satisfies true-listp) x)); We expect x to end in NIL.
       (cond ((endp x) y)                       ; If x is empty, return y.
             (t (cons (car x)                   ; Else, copy first node
                      (app (cdr x) y)))))       ;  and recur into next.

If you defined this function in some Common Lisp, then to run app on
the x and y above you could then type

     (app '(A B) '(C D E))

and Common Lisp will print the result (A B C D E).

Next on the Walking Tour:  An Example of ACL2 in Use

An Example of ACL2 in Use    An Example of ACL2 in Use

Next on the Walking Tour:  How To Find Out about ACL2 Functions

To introduce you to ACL2 we will consider the app function discussed in
the Common Lisp page, except we will omit for the moment the declare
form, which in ACL2 is called a guard.    We will deal with guards
later.

Here is the definition again

     (defun app (x y)
       (cond ((endp x) y)
             (t (cons (car x)
                      (app (cdr x) y)))))

The next few stops along the Walking Tour will show you

       * how to use the ACL2 documentation,
       * what happens when the above definition is submitted to ACL2,
       * what happens when you evaluate calls of app,
       * what one simple theorem about app looks like,
       * how ACL2 proves the theorem, and
       * how that theorem can be used in another proof.

Along the way we will talk about the definitional principle, types, the
ACL2 read-eval-print loop, and how the theorem prover works.

When we complete this part of the tour we will introduce the notion of
guards and revisit several of the topics above in that context.

Next on the Walking Tour:  How To Find Out about ACL2 Functions

Analyzing Common Lisp Models    Analyzing Common Lisp Models

To analyze a model you must be able to reason about the operations and
relations involved.  Perhaps, for example, some aspect of the model
depends upon the fact that the concatenation operation is associative.

In any Common Lisp you can confirm that

     (app '(A B) (app '(C D) '(E F)))

and

     (app (app '(A B) '(C D)) '(E F)))

both evaluate to the same thing, (A B C D E F).

But what distinguishes ACL2 (the logic) from applicative Common Lisp
(the language) is that in ACL2 you can prove that the concatenation
function app is associative when its arguments are true-lists, whereas
in Common Lisp all you can do is test that proposition.

That is, in ACL2 it makes sense to say that the following formula is a
"theorem."

     Theorem Associativity of App
     (implies (and (true-listp a)
                   (true-listp b))
              (equal (app (app a b) c)
                     (app a (app b c))))

Theorems about the properties of models are proved by symbolically
manipulating the operations and relations involved.  If the
concatenation of sequences is involved in your model, then you may well
need the theorem above in order to that your model has some particular
property.

Common Lisp    Common Lisp

Next on the Walking Tour:  An Example Common Lisp Function Definition

The logic of ACL2 is based on Common Lisp.

Common Lisp is the standard list processing programming language.  It
is documented in:  Guy L. Steele, Common Lisp The Language, Digital
Press, 12 Crosby Drive, Bedford, MA 01730, 1990.  See also
`http://www.cs.cmu.edu/Web/Groups/AI/html/cltl/cltl2.html'.

ACL2 formalizes only a subset of Common Lisp.  It includes such
familiar Lisp functions as cons, car and cdr for creating and
manipulating list structures, various arithmetic primitives such as +,
*, expt and <=, and intern and symbol-name for creating and
manipulating symbols.  Control primitives include cond, case and if, as
well as function call, including recursion.  New functions are defined
with defun and macros with defmacro.  See PROGRAMMING <> for a
list of the Common Lisp primitives supported by ACL2.

ACL2 is a very small subset of full Common Lisp.  ACL2 does not include
the Common Lisp Object System (CLOS), higher order functions, circular
structures, and other aspects of Common Lisp that are non-applicative.
Roughly speaking, a language is applicative if it follows the rules of
function application.  For example, f(x) must be equal to f(x), which
means, among other things, that the value of f must not be affected by
"global variables" and the object x must not change over time.

See An Example Common Lisp Function Definition for a simple
example of Common Lisp.

Next on the Walking Tour:  An Example Common Lisp Function Definition

Common Lisp as a Modeling Language    Common Lisp as a Modeling Language

In ACL2 we have adopted Common Lisp as the basis of our modeling
language.  If you have already read our brief note on Common Lisp and
recall the example of app, please proceed.  Otherwise see Common Lisp
for an exceedingly brief introduction to Common Lisp and then
come back here.

In Common Lisp it is very easy to write systems of formulas that
manipulate discrete, inductively constructed data objects.  In building
a model you might need to formalize the notion of sequences and define
such operations as concatenation, length, whether one is a permutation
of the other, etc.  It is easy to do this in Common Lisp.  Furthermore,
if you have a Common Lisp "theory of sequences" you can run the
operations and relations you define.  That is, you can execute the
functions on concrete data to see what results your formulas produce.

If you define the function app as shown above and then type

     (app '(A B) '(C D E))

in any Common Lisp, the answer will be computed and will be (A B C D E).

The executable nature of Common Lisp and thus of ACL2 is very handy
when producing models.

But executability is not enough for a modeling language because the
purpose of models is to permit analysis.

See Analyzing Common Lisp Models to continue.

Conversion    Conversion to Uppercase

When symbols are read by Common Lisp they are converted to upper case.
Note carefully that this remark applies to the characters in _symbols_.
The characters in strings are not converted upper case.

To type a symbol containing lower case characters you can enclose the
symbol in vertical bars, as in |AbC| or you can put a "backslash"
before each lower case character you wish to preserve, as in A\bC.
|AbC| and A\bC are two different ways of writing the same symbol (just
like 2/4 and 1/2 are two different ways of writing the same rational).
The symbol has three characters in its name, the middle one of which is
a lower case b.

Corroborating Models    Corroborating Models

Next on the Flying Tour:  Models of Computer Hardware and Software

After producing a model, it must be corroborated against reality.  The
Falling Body Model has been corroborated by a vast number of
experiments in which the time and distance were measured and compared
according to the formula.  In general all models must be corroborated
by experiment.

The Falling Body Model can be derived from deeper models, namely
Newton's laws of motion and the assertion that, over the limited
distances concerned, graviation exerts a constant acceleration on the
object.  When the model in question can be derived from other models,
it is the other models that are being corroborated by our experiments.

Because nature is not formal, we cannot prove that our models of it are
correct.  All we can do is test our models against nature's behavior.

Such testing often exposes restrictions on the applicability of our
models.  For example, the Falling Body Model is inaccurate if air
resistance is significant.  Thus, we learn not to use that model to
predict how long it takes a feather to fall from a 200 foot tower in
the earth's atmosphere.

In addition, attempts at corroboration might reveal that the model is
actually incorrect.  Careful measurements might expose the fact that
the gravitational force increases as the body falls closer to earth.
Very careful measurements might reveal relativistic effects.
Technically, the familiar Falling Body Model is just wrong, even under
excessive restrictions such as "in a perfect vacuum" and "over small
distances."  But it is an incredibly useful model nonetheless.

There are several morals here.

Models need not be complete to be useful.

Models need not be perfectly accurate to be useful.

The user of a model must understand its limitations.

Next on the Flying Tour:  Models of Computer Hardware and Software

Evaluating App on Sample Input    Evaluating App on Sample Input

Next on the Walking Tour:  The Associativity of App

     ACL2 !>(app nil '(x y z))
     (X Y Z)

     ACL2 !>(app '(1 2 3) '(4 5 6 7))
     (1 2 3 4 5 6 7)

     ACL2 !>(app '(a b c d e f g) '(x y z))   ; see Conversion for an explanation
     (A B C D E F G X Y Z)

     ACL2 !>(app (app '(1 2) '(3 4)) '(5 6))
     (1 2 3 4 5 6)

     ACL2 !>(app '(1 2) (app '(3 4) '(5 6)))
     (1 2 3 4 5 6)

     ACL2!>(let ((a '(1 2))
                 (b '(3 4))
                 (c '(5 6)))
             (equal (app (app a b) c)
                    (app a (app b c))))
     T

As we can see from these examples, ACL2 functions can be executed more
or less as Common Lisp.

The last three examples suggest an interesting property of app.

Next on the Walking Tour:  The Associativity of App

Flawed Induction Candidates in App Example    Flawed Induction Candidates in App Example

Induction on a is unflawed:  every occurrence of a in the conjecture

     (equal (app (app a b) c)
            (app a (app b c)))

is in a position being recursively decomposed!

Now look at the occurrences of b.  The first (shown in bold below) is
in a position that is held constant in the recursion of (app a b).  It
would be "bad" to induct on b here.

     (equal (app (app a b) c)
            (app a (app b c)))

Free Variables in Top-Level Input    Free Variables in Top-Level Input

     ACL2 !>(equal (app (app a b) c)
                   (app a (app b c))))

     ACL2 Error in TOP-LEVEL:  Global variables, such as C, B, and A, are
     not allowed. See :DOC ASSIGN and :DOC @.

ACL2 does not allow "global variables" in top-level input.  There is no
"top-level binding environment" to give meaning to these variables.

Thus, expressions involving no variables can generally be evaluated,

     ACL2 !>(equal (app (app '(1 2) '(3 4)) '(5 6))
                   (app '(1 2) (app '(3 4) '(5 6))))
     (1 2 3 4 5 6)

but expressions containing variables cannot.

There is an exception to rule.  References to "single-threaded objects"
may appear in top-level forms.  See STOBJ <>.  A
single-threaded object is an ACL2 object, usually containing many
fields, whose use is syntactically restricted so that it may be given
as input only to certain functions and must be returned as output by
certain functions.  These restrictions allow single- threaded objects
to be efficiently manipulated.  For example, only a single copy of the
object actually exists, even though from a logical perspective one
might expect the object to be "copied on write."

The most commonly used single-threaded object in ACL2 is the ACL2
system state, whose current value is always held in the variable state
<>.

ACL2 provides a way for you to use state to save values of computations
at the top-level and refer to them later.  See assign <> and @ <>.

Functions for Manipulating these Objects    Functions for Manipulating these Objects

Next on the Flying Tour:  Modeling in ACL2

Consider a typical "stack" of control frames.

Suppose the model required that we express the idea of "the most recent
frame whose return program counter points into MAIN."

The natural expression of this notion involves

function application - "fetch the return-pc of this frame"

case analysis -  "if the pc is MAIN, then ..."

iteration or recursion - "pop this frame off and repeat."

The designers of ACL2 have taken the position that a programming
language is the natural language in which to define such notions,
provided the language has a mathematical foundation so that models can
be analyzed and properties derived logically.

is the language supported by ACL2.  See Common Lisp for an
optional and very brief introduction to Common Lisp.

Next on the Flying Tour:  Modeling in ACL2

Guards    Guards

Common Lisp functions are partial; they are not defined for all
possible inputs.  But ACL2 functions are total.  Roughly speaking, the
logical function of a given name in ACL2 is a completion of the Common
Lisp function of the same name obtained by adding some arbitrary but
"natural" values on arguments outside the "intended domain" of the
Common Lisp function.

ACL2 requires that every ACL2 function symbol have a "guard," which may
be thought of as a predicate on the formals of the function describing
the intended domain.  The guard on the primitive function car <>, for
example, is (or (consp x) (equal x nil)), which requires the argument
to be either an ordered pair or nil.  We will discuss later how to
specify a guard for a defined function; when one is not specified, the
guard is t which is just to say all arguments are allowed.

But guards are entirely extra-logical:  they are not involved in the
axioms defining functions.  If you put a guard on a defined function,
the defining axiom added to the logic defines the function on all
arguments, not just on the guarded domain.

So what is the purpose of guards?

The key to the utility of guards is that we provide a mechanism, called
"guard verification," for checking that all the guards in a formula are
true.  See VERIFY-GUARDS.  This mechanism will attempt to prove
that all the guards encountered in the evaluation of a guarded function
are true every time they are encountered.

For a thorough discussion of guards, see the paper [km97] in the ACL2
bibliography.

Guessing the Type of a Newly Admitted Function    Guessing the Type of a Newly Admitted Function

When a function is admitted to the logic, ACL2 tries to "guess" what
type of object it returns.  This guess is codified as a term that
expresses a property of the value of the function.  For app the term is

     (OR (CONSP (APP X Y))
         (EQUAL (APP X Y) Y))

which says that app returns either a cons or its second argument.  This
formula is added to ACL2's rule base as a type-prescription <> rule.
Later we will discuss how rules are used by the ACL2 theorem prover.
The point here is just that when you add a definition, the data base of
rules is updated, not just by the addition of the definitional axiom,
but by several new rules.

You should now return to the Walking Tour.

Guiding the ACL2 Theorem Prover    Guiding the ACL2 Theorem Prover

Next on the Walking Tour:  ACL2 as an Interactive Theorem Prover (cont)

Now that you have seen the theorem prover in action you might be
curious as to how you guide it.

The idea is that the user submits conjectures and advice and reads the
proof attempts as they are produced.

Most of the time, the conjectures submitted are lemmas to be used in
the proofs of other theorems.

Next on the Walking Tour:  ACL2 as an Interactive Theorem Prover (cont)

Hey Wait!  Is ACL2 Typed or Untyped(Q)    Hey Wait!  Is ACL2 Typed or Untyped?

The example

     ACL2 !>(app 7 27)

     ACL2 Error in TOP-LEVEL:  The guard for the function symbol ENDP, which
     is (OR (CONSP X) (EQUAL X NIL)), is violated by the arguments in the
     call (ENDP 7).

illustrates the fact that while ACL2 is an untyped language the ACL2
evaluator can be configured so as to check "types" at runtime.  We
should not say "types" here but "guards."  See Undocumented Topic
for a discussion of guards.

The guard on endp <> requires its argument to be a true list.  Since 7
is not a true list, and since ACL2 is checking guards in this example,
an error is signaled by ACL2.  How do you know ACL2 is checking guards?
Because the prompt tells us (see About the Prompt) with its
"!".

How Long Does It Take to Become an Effective User(Q)    How Long Does It Take to Become an Effective User?

Next on the Flying Tour:  Other Requirements

The training time depends primarily on the background of the user.

We expect that a user who

       * has a bachelor's degree in computer science or mathematics,

       * has some experience with formal methods,

       * has had some exposure to Lisp programming and is comfortable
         with the Lisp notation,

       * is familiar with and has unlimited access to a Common Lisp
         host processor, operating system, and text editor (we
         use Sun workstations running Unix and GNU Emacs),

       * is willing to read and study the ACL2 documentation, and

       * is given the opportunity to start with ``toy'' projects before
         being expected to tackle the company's Grand Challenge,

will probably take several months to become an effective ACL2 user.

Next on the Flying Tour:  Other Requirements

How To Find Out about ACL2 Functions    How To Find Out about ACL2 Functions

Next on the Walking Tour:  How To Find Out about ACL2 Functions (cont)

Most ACL2 primitives are documented.  Here is the definition of app
again, with the documented topics highlighted.  <> All of the links
below lead into the ACL2 online documentation, 1.5 megabytes of
hyperlinked text.  So follow these links around, but remember to come
back here!

     (defun app (x y)
       (cond ((endp x) y)
             (t (cons (car x)
                      (app (cdr x) y)))))

By following the link on endp <> we see that it is a Common Lisp
function and is defined to be the same as atom <>, which recognizes
non-conses.  But endp has a guard.  Since we are ignorning guards for
now, we'll ignore the guard issue on endp.

So this definition reads "to app x and y:  if x is an atom, return y;
otherwise, app (cdr x) and y and then cons (car x) onto that."

Next on the Walking Tour:  How To Find Out about ACL2 Functions (cont)

How To Find Out about ACL2 Functions (cont)    How To Find Out about ACL2 Functions (cont)

Next on the Walking Tour:  The Admission of App

You can always use the Index <> to find the documentation of functions.
Try it.  Click on the Index icon below.  Then use the Find command of
your browser to find "endp" in that document and follow the link.  But
remember to come back here.

The ACL2 documentation is also available via Emacs' TexInfo, allowing
you to explore the hyperlinked documentation in the comfort of a text
editor that can also interact with ACL2.

In addition, runtime images of ACL2 have the hyperlinked text as a
large ACL2 data structure that can be explored with ACL2's :doc
command.  If you have ACL2 running, try the command :doc endp.

Another way to find out about ACL2 functions, if you have an ACL2 image
available, is to use the command :args <> which prints the formals,
type, and guard of a function symbol.

Of course, the ACL2 documentation can also be printed out as 700 page
book.  See the ACL2 Home Page to download the Postscript.

Now let's continue with app.

Next on the Walking Tour:  The Admission of App

Modeling in ACL2    Modeling in ACL2

Next on the Flying Tour:  Running Models

Below we define mc(s,n) to be the function that single-steps n times
from a given starting state, s.  In Common Lisp, "mc(s,n)" is written
(mc s n).

     (defun mc (s n)                     ; To step s n times:
      (if (zp n)                         ; If n is 0
          s                              ;    then return s
          (mc (single-step s) (- n 1)))) ;    else step single-step(s)
                                                           n-1 times.

This is an example of a formal model in ACL2.

Next on the Flying Tour:  Running Models

Models in Engineering    Models in Engineering

Frequently, engineers use mathematical models.  Use of such models
frequently lead to

better designs,

faster completion of acceptable products, and

reduced overall cost,

because models allow the trained user to study the design before it is
built and analyze its properties.  Usually, testing and analyzing a
model is cheaper and faster than fabricating and refabricating the
product.

See The Falling Body Model to continue.

Models of Computer Hardware and Software    Models of Computer Hardware and Software

Next on the Flying Tour:  A Typical State

Computing machines, whether hardware or software or some combintation,
are frequently modeled as "state machines."

To so model a computing machine we must represent its states as objects
in our mathematical framework.

Transitions are functions or relations on state objects.

In what language shall we define these objects, functions, and
relations?

The mathematical languages we were taught in high school

algebra,

geometry,

trignometry, and

calculus

are inappropriate for modeling digital systems.  They primarily let us
talk about numbers and continuous functions.

To see what kind of expressive power we need, take a closer look at
what a typical state contains.

Next on the Flying Tour:  A Typical State

Name the Formula Above    Name the Formula Above

When the theorem prover explicitly assigns a name, like *1, to a
formula, it has decided to prove the formula by induction.

Nontautological Subgoals    Prover output omits some details

The theorem prover's proof output is intended to suggest an outline of
the reasoning process employed by its proof engine, which is virtually
always more than is necessary for the ACL2 user.  In particular, the
output often omits subgoals that are sufficiently trivial, including
tautologies.

Numbers in ACL2    Numbers in ACL2

The numbers in ACL2 can be partitioned into the following subtypes:

      Rationals
       Integers
        Positive integers                3
        Zero                             0
        Negative Integers                -3
       Non-Integral Rationals
        Positive Non-Integral Rationals  19/3
        Negative Non-Integral Rationals  -22/7
      Complex Rational Numbers           #c(3 5/2) ; = 3+(5/2)i

Signed integer constants are usually written (as illustrated above)  as
sequences of decimal digits, possibly preceded by + or -.   Decimal
points are not allowed.  Integers may be written in binary,  as in
#b1011 (= 23) and #b-111 (= -7).  Octal may also be  used, #o-777 =
-511.  Non-integral rationals are written as a  signed decimal integer
and an unsigned decimal integer, separated by  a slash.  Complex
rationals are written as #c(rpart ipart) where  rpart and ipart are
rationals.

Of course, 4/2 = 2/1 = 2 (i.e., not every rational written with a slash
is a non-integer).  Similarly, #c(4/2 0) = #c(2 0) = 2.

The common arithmetic functions and relations are denoted by +,  -, *,
/, =, <, <=, > and >=.  However there  are many others, e.g., floor,
ceiling, and lognot.  We  suggest you see PROGRAMMING <> where
we list all of the primitive  ACL2 functions.  Alternatively, see any
Common Lisp language  documentation.

The primitive predicates for recognizing numbers are illustrated
below.  The following ACL2 function will classify an object, x,
according to its numeric subtype, or else return 'NaN (not a  number).
We show it this way just to illustrate programming in  ACL2.

      (defun classify-number (x)
        (cond ((rationalp x)
               (cond ((integerp x)
                      (cond ((< 0 x) 'positive-integer)
                            ((= 0 x) 'zero)
                            (t 'negative-integer)))
                     ((< 0 x) 'positive-non-integral-rational)
                     (t 'negative-non-integral-rational)))
              ((complex-rationalp x) 'complex-rational)
              (t 'NaN)))

On the Naming of Subgoals    On the Naming of Subgoals

Subgoal *1/2 is the induction step from the scheme, obtained by
instantiating the scheme with our conjecture.

We number the cases "backward", so this is case "2" of the proof of
"*1".  We number them backward so you can look at a subgoal number and
get an estimate for how close you are to the end.

Other Requirements    Other Requirements

Next on the Flying Tour:  The End of the Flying Tour

ACL2 is distributed on the Web without fee.

There is a License agreement, which is available via the ACL2 Home Page
link below.

ACL2 currently runs on Unix, Linux, Windows, and Macintosh operating
systems.

It can be built in any of the following Common Lisps:

       * Allegro,
       * GCL (Gnu Common Lisp),
       * Lispworks,
       * CLISP,
       * CMU Common Lisp,
       * SBCL, and
       * CCL (OpenMCL)

Next on the Flying Tour:  The End of the Flying Tour

Overview of the Expansion of ENDP in the Base Case    Overview of the Expansion of ENDP in the Base Case

Subgoal *1/1 is the Base Case of our induction.  It simplifies to
Subgoal *1/1' by expanding the ENDP term in the hypothesis, just as we
saw in the earlier proof of Subgoal *1/2.

Overview of the Expansion of ENDP in the Induction Step    Overview of the Expansion of ENDP in the Induction Step

In this message the system is saying that Subgoal *1/2 has been
rewritten to the Subgoal *1/2', by expanding the definition of endp.
This is an example of simplification, one of the main proof techniques
used by the theorem prover.

See The Expansion of ENDP in the Induction Step (Step 0) if you
would like to step through the simplification of Subgoal *1/2.

Overview of the Final Simplification in the Base Case    Overview of the Final Simplification in the Base Case

The But is our signal that the goal is proved.

See The Final Simplification in the Base Case (Step 0) to step
through the proof.  It is very simple.

Overview of the Proof of a Trivial Consequence    Overview of the Proof of a Trivial Consequence

Next on the Walking Tour:  The End of the Walking Tour

     ACL2 !>(defthm trivial-consequence
              (equal (app (app (app (app x1 x2) (app x3 x4)) (app x5 x6)) x7)
                     (app x1 (app (app x2 x3) (app (app x4 x5) (app x6 x7))))))

     ACL2 Warning [Subsume] in ( DEFTHM TRIVIAL-CONSEQUENCE ...):  The previously
     added rule ASSOCIATIVITY-OF-APP subsumes the newly proposed :REWRITE
     rule TRIVIAL-CONSEQUENCE, in the sense that the old rule rewrites a
     more general target.  Because the new rule will be tried first, it
     may nonetheless find application.

     By the simple :rewrite rule ASSOCIATIVITY-OF-APP we reduce the conjecture
     to

     Goal'
     (EQUAL (APP X1
                 (APP X2
                      (APP X3 (APP X4 (APP X5 (APP X6 X7))))))
            (APP X1
                 (APP X2
                      (APP X3 (APP X4 (APP X5 (APP X6 X7))))))).

     But we reduce the conjecture to T, by primitive type reasoning.

     Q.E.D.

     Summary
     Form:  ( DEFTHM TRIVIAL-CONSEQUENCE ...)
     Rules: ((:REWRITE ASSOCIATIVITY-OF-APP)
             (:FAKE-RUNE-FOR-TYPE-SET NIL))
     Warnings:  Subsume
     Time:  0.20 seconds (prove: 0.02, print: 0.00, other: 0.18)
      TRIVIAL-CONSEQUENCE

You might explore the links before moving on.

Next on the Walking Tour:  The End of the Walking Tour

Overview of the Simplification of the Base Case to T    Overview of the Simplification of the Base Case to T

Next on the Walking Tour:  The End of the Proof of the Associativity of App

     Subgoal *1/1
     (IMPLIES (ENDP A)
              (EQUAL (APP (APP A B) C)
                     (APP A (APP B C)))).

     By the simple :definition ENDP we reduce the conjecture to

     Subgoal *1/1'
     (IMPLIES (NOT (CONSP A))
              (EQUAL (APP (APP A B) C)
                     (APP A (APP B C)))).

     But simplification reduces this to T, using the :definition APP and
     primitive type reasoning.

Next on the Walking Tour:  The End of the Proof of the Associativity of App

Overview of the Simplification of the Induction Conclusion    Overview of the Simplification of the Induction Conclusion

In this message the system is saying that Subgoal *1/2' has been
rewritten T using the rules noted.  The word "But" at the beginning of
the sentence is a signal that the goal has been proved.

See The Simplification of the Induction Conclusion (Step 0) to
step through the proof of Subgoal *1/2'.

Overview of the Simplification of the Induction Step to T    Overview of the Simplification of the Induction Step to T

Next on the Walking Tour:  Overview of the Simplification of the Base Case to T

     Subgoal *1/2
     (IMPLIES (AND (NOT (ENDP A))
                   (EQUAL (APP (APP (CDR A) B) C)
                          (APP (CDR A) (APP B C))))
              (EQUAL (APP (APP A B) C)
                     (APP A (APP B C)))).

     By the simple :definition ENDP we reduce the conjecture to

     Subgoal *1/2'
     (IMPLIES (AND (CONSP A)
                   (EQUAL (APP (APP (CDR A) B) C)
                          (APP (CDR A) (APP B C))))
              (EQUAL (APP (APP A B) C)
                     (APP A (APP B C)))).

     But simplification reduces this to T, using the :definition APP, the
     :rewrite rules CDR-CONS and CAR-CONS and primitive type reasoning.

Next on the Walking Tour:  Overview of the Simplification of the Base Case to T

Perhaps    Perhaps

The theorem prover's proof is printed in real time.  At the time it
prints "Perhaps" it does not know the proof will succeed.

Popping out of an Inductive Proof    Popping out of an Inductive Proof

Recall that our induction scheme (see The Proof of the Associativity of App
to revisit it) had two cases, the induction step
(Subgoal *1/2) and the base case (Subgoal *1/1).  Both have been proved!

Proving Theorems about Models    Proving Theorems about Models

Next on the Flying Tour:  What is Required of the User(Q)

But ACL2 is a logic.  We can prove theorems about the model.

     Theorem.  MC 'mult is a multiplier
     (implies (and (natp x)
                   (natp y))
              (equal (lookup 'z (mc (s 'mult x y) (mclk x)))
                     (* x y))).

This theorem says that a certain program running on the mc machine will
correctly multiply any two natural numbers.

It is a statement about an infinite number of test cases!

We know it is true about the model because we proved it.

Next on the Flying Tour:  What is Required of the User(Q)

Revisiting the Admission of App    Revisiting the Admission of App

Next on the Walking Tour:  Evaluating App on Sample Input

Here is the definition of app again with certain parts highlighted.  If
you are taking the Walking Tour, please read the text carefully and
click on each of the links below, except those marked <>.  Then come
back here.

     ACL2 !>(defun app (x y)
       (cond ((endp x) y)
             (t (cons (car x)
                      (app (cdr x) y)))))

     The admission of APP is trivial, using the
     relation O< <> (which is known to be well-founded on
     the domain recognized by O-P <>) and the measure
     (ACL2-COUNT <> X).  We observe that the
     type of APP is described by the theorem (OR
     (CONSP (APP X Y)) (EQUAL (APP X Y) Y)).  We used primitive type
     reasoning.

     Summary
     Form:  ( DEFUN APP ...)
     Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL))
     Warnings:  None
     Time:  0.03 seconds (prove: 0.00, print: 0.00, other: 0.03)
      APP

Next on the Walking Tour:  Evaluating App on Sample Input

Rewrite Rules are Generated from DEFTHM Events    Rewrite Rules are Generated from DEFTHM Events

Next on the Walking Tour:  You Must Think about the Use of a Formula as a Rule

By reading the documentation of defthm <> (and especially of its
:rule-classes <> argument) you would learn that when we submitted the
command

     (defthm associativity-of-app
       (equal (app (app a b) c)
              (app a (app b c))))

we not only command the system to prove that app is an associative
function but

       * we commanded it to use that fact as a rewrite rule.

That means that every time the system encounters a term of the form

     (app (app x y) z)

it will replace it with

     (app x (app y z))!

Next on the Walking Tour:  You Must Think about the Use of a Formula as a Rule

Running Models    Running Models

Next on the Flying Tour:  Symbolic Execution of Models

Suppose the machine being modeled is some kind of arithmetic unit.
Suppose the model can be initialized so as to multiply x times y and
leave the answer in z.  Then if we initialize s to multiply with x=5
and y=7 and run the machine long enough, we can read the answer 35 in
the final state.

Because ACL2 is a programming language, our model can be run or
executed.

If you defined the model in ACL2 and then typed

     > (lookup 'z (mc (s 'mult 5 7) 29))

then ACL2 would compute 35.  You can emulate or test the model of your
machine.

This is obvious because ACL2 is Common Lisp; and Common Lisp is a
programming language.

Next on the Flying Tour:  Symbolic Execution of Models

Subsumption of Induction Candidates in App Example    Subsumption of Induction Candidates in App Example

After collecting induction suggestions from these three terms

     (app a b)

     (app b c)

     (app a (app b c))

the system notices that the first and last suggest the same
decomposition of a.  So we are left with two ideas about how to induct:

Decompose a as we would to unwind (app a b).

Decompose b as we would to unwind (app b c).

Suggested Inductions in the Associativity of App Example    Suggested Inductions in the Associativity of App Example

To find a plausible induction argument, the system studies the
recursions exhibited by the terms in the conjecture.

Roughly speaking, a call of a recursive function "suggests" an
induction if the argument position decomposed in recursion is occupied
by a variable.

In this conjecture, three terms suggest inductions:

     (app a b)

     (app b c)

     (app a (app b c))

The variable recursively decomposed is indicated in bold.

Symbolic Execution of Models    Symbolic Execution of Models

Next on the Flying Tour:  Proving Theorems about Models

But ACL2 is more than a programming language.

Initialize x to 5 and let y be any legal value.

Because ACL2 is a mathematical language, we can simplify the expression

     (lookup 'z (mc (s 'mult 5 y) 29))

and get (+ y y y y y).  This is symbolic execution because not all of
the parameters are known.

Next on the Flying Tour:  Proving Theorems about Models

The Admission of App    The Admission of App

Next on the Walking Tour:  Revisiting the Admission of App

Here is what it looks like to submit the definition of app to ACL2:

     ACL2 !>(defun app (x y)
       (cond ((endp x) y)
             (t (cons (car x)
                      (app (cdr x) y)))))

     The admission of APP is trivial, using the relation O< (which
     is known to be well-founded on the domain recognized by O-P)
     and the measure (ACL2-COUNT X).  We observe that the type of APP is
     described by the theorem (OR (CONSP (APP X Y)) (EQUAL (APP X Y) Y)).
     We used primitive type reasoning.

     Summary
     Form:  ( DEFUN APP ...)
     Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL))
     Warnings:  None
     Time:  0.03 seconds (prove: 0.00, print: 0.00, other: 0.03)
      APP

The text between the lines above is one interaction with the ACL2
command loop.

Above you see the user's input and how the system responds.  This
little example shows you what the syntax looks like and is a very
typical successful interaction with the definitional principle.

Let's look at it a little more closely.

Next on the Walking Tour:  Revisiting the Admission of App

The Associativity of App    The Associativity of App

Next on the Walking Tour:  The Theorem that App is Associative

     ACL2!>(let ((a '(1 2))
                 (b '(3 4))
                 (c '(5 6)))
             (equal (app (app a b) c)
                    (app a (app b c))))
     T

Observe that, for the particular a, b, and c above, (app (app a b) c)
returns the same thing as (app a (app b c)).  Perhaps app is
associative.  Of course, to be associative means that the above
property must hold for all values of a, b, and c, not just the ones
tested above.

Wouldn't it be cool if you could type

     ACL2!>(equal (app (app a b) c)
                  (app a (app b c)))

and have ACL2 compute the value T?  Well, you can't!  If you try it,
you'll get an error message!  The message says we can't evaluate that
form because it contains free variables, i.e., variables not given
values.  See Free Variables in Top-Level Input to see the
message.

We cannot evaluate a form on an infinite number of cases.  But we can
prove that a form is a theorem and hence know that it will always
evaluate to true.

Next on the Walking Tour:  The Theorem that App is Associative

The Base Case in the App Example    The Base Case in the App Example

This formula is the Base Case.  It consists of two parts, a test
identifying the non-inductive case and the conjecture to prove.

     (IMPLIES (ENDP A)                 ; Test
              (:P A B C))              ; Conjecture

When we prove this we can assume

       * A is empty

and we have to prove the conjecture for A.

The End of the Flying Tour    The End of the Flying Tour

This completes the Flying Tour.

You may wish now to go back and revisit selected nodes of the Flying
Tour so that you can explore some of the branches not on the Tour.  You
can do so via The Flight Plan.  These branches mainly provide some
background and motivational material, rather than details of ACL2.

If you would like to learn more about ACL2 itself, we recommend that
you now take the walking Tour.  You may do so by clicking on the
Walking Tour icon below.

Thanks.
Matt Kaufmann and J Moore

Next on the Walking Tour:  A Walking Tour of ACL2

The End of the Proof of the Associativity of App    The End of the Proof of the Associativity of App

Next on the Walking Tour:  Guiding the ACL2 Theorem Prover

     That completes the proof of *1.

     Q.E.D.

     Summary
     Form:  ( DEFTHM ASSOCIATIVITY-OF-APP ...)
     Rules: ((:REWRITE CDR-CONS)
             (:REWRITE CAR-CONS)
             (:DEFINITION NOT)
             (:DEFINITION ENDP)
             (:FAKE-RUNE-FOR-TYPE-SET NIL)
             (:DEFINITION APP))
     Warnings:  None
     Time:  0.27 seconds (prove: 0.10, print: 0.05, other: 0.12)
      ASSOCIATIVITY-OF-APP

Next on the Walking Tour:  Guiding the ACL2 Theorem Prover

The End of the Walking Tour    The End of the Walking Tour

This completes the Walking Tour.

We intend to document many other parts of the system this way, but we
just haven't gotten around to it.

If you feel like reading more, see TUTORIAL-EXAMPLES in the
documentation.  There you will find several challenging but simple
applications.  At the conclusion of the examples is a simple challenge
to try.

We hope you enjoy ACL2.  We do.

Matt Kaufmann and J Strother Moore

The Event Summary    The Event Summary

At the conclusion of most events (see About the Prompt for a
brief discussion of events or see EVENTS <>), ACL2 prints a
summary.  The summary for app is:

     Summary
     Form:  ( DEFUN APP ...)
     Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL))
     Warnings:  None
     Time:  0.03 seconds (prove: 0.00, print: 0.00, other: 0.03)
      APP

The "rules" listed are those used in function admission or proof
summarized.  What is actually listed are "runes" (see RUNE) <>)
which are list-structured names for rules in the ACL2 data base or
"world" <>.  Using theories <> you can "enable" and "disable" rules so
as to make them available (or not) to the ACL2 theorem prover.

The "warnings" mentioned (none are listed for app) remind the reader
whether the event provoked any warnings.  The warnings themselves would
have been printed earlier in the processing and this part of the
summary just names the earlier warnings printed.

The "time" indicates how much processing time was used and is divided
into three parts:  the time devoted to proof, to printing, and to
syntactic checks, pre-processing and data base updates.  Despite the
fact that ACL2 is an applicative language it is possible to measure
time with ACL2 programs.  The state <> contains a clock.  The times are
printed in decimal notation but are actually counted in integral units.

The final APP is the value of the defun command and was printed by the
read-eval-print loop.  The fact that it is indented one space is a
subtle reminder that the command actually returned an "error triple",
consisting of a flag indicating (in this case) that no error occurred,
a value (in this case the symbol APP), and the final state <>).  See
LD-POST-EVAL-PRINT <> for some details.  If you really want to
follow that link, however, you might see LD <> first.

You should now return to the Walking Tour.

The Expansion of ENDP in the Induction Step (Step 0)    The Expansion of ENDP in the Induction Step (Step 0)

     Subgoal *1/2
     (IMPLIES (AND (NOT (ENDP A))
                   (EQUAL (APP (APP (CDR A) B) C)
                          (APP (CDR A) (APP B C))))
              (EQUAL (APP (APP A B) C)
                     (APP A (APP B C)))).

Click on the link above (the open parenthesis before ENDP) to replace
(ENDP A) by its definition.

The Expansion of ENDP in the Induction Step (Step 1)    The Expansion of ENDP in the Induction Step (Step 1)

     Subgoal *1/2
     (IMPLIES (AND (NOT (NOT (CONSP A)))
                   (EQUAL (APP (APP (CDR A) B) C)
                          (APP (CDR A) (APP B C))))
              (EQUAL (APP (APP A B) C)
                     (APP A (APP B C)))).

The bold text is the instantiated definition of ENDP.

Now click on the link above to simplify (NOT (NOT (CONSP A)))

The Expansion of ENDP in the Induction Step (Step 2)    The Expansion of ENDP in the Induction Step (Step 2)

     Subgoal *1/2'
     (IMPLIES (AND (CONSP A)
                   (EQUAL (APP (APP (CDR A) B) C)
                          (APP (CDR A) (APP B C))))
              (EQUAL (APP (APP A B) C)
                     (APP A (APP B C)))).

Note that this is Subgoal *1/2'.

You may see Overview of the Simplification of the Induction Step to T
to return to the main proof.

The Falling Body Model    The Falling Body Model

One particularly famous and very simple model is the equation of a
falling body:  the distance d an object falls is proportional to the
square of the time t.  If the time is measured in seconds and the
distance in feet, the equation relating these two is

            2
     d = 16t

This equation is a model of falling objects.  It can be used to predict
how long it takes a cannonball to fall from the top of a 200 foot tower
(3.5 seconds).  This might be important if your product is designed to
drop cannonballs on moving targets.

See Corroborating Models to continue

The Final Simplification in the Base Case (Step 0)    the Final Simplification in the Base Case (Step 0)

     Subgoal *1/1'
     (IMPLIES (NOT (CONSP A))
              (EQUAL (APP (APP A B) C)
                     (APP A (APP B C)))).

Click on the link above to replace (APP A B) by its definition.  Note
that the hypothesis (NOT (CONSP A)) allows us to simplify the IF in APP
to its false branch this time.

The Final Simplification in the Base Case (Step 1)    the Final Simplification in the Base Case (Step 1)

     Subgoal *1/1'
     (IMPLIES (NOT (CONSP A))
              (EQUAL (APP B C)
                     (APP A (APP B C)))).

Click on the link above to expand the definition of APP.  Again, we
come out through the false branch because of the hypothesis.

The Final Simplification in the Base Case (Step 2)    the Final Simplification in the Base Case (Step 2)

     Subgoal *1/1'
     (IMPLIES (NOT (CONSP A))
              (EQUAL (APP B C)
                     (APP B C))).

Click on the link above to use the Axiom (EQUAL x x) = t

The Final Simplification in the Base Case (Step 3)    the Final Simplification in the Base Case (Step 3)

     Subgoal *1/1'
     (IMPLIES (NOT (CONSP A))
              T)

Now that its conclusion is identically T the IMPLIES will simplify to T
(not shown) and we are done with Subgoal *1/1'.

You may see Overview of the Simplification of the Base Case to T
to return to the main proof.

The First Application of the Associativity Rule    The First Application of the Associativity Rule

So here we see our associativity rule being used!

The rewriter sweeps the conjecture in a leftmost innermost fashion,
applying rewrite rules as it goes.

The associativity rule is used many times in this sweep.  The first
"target" is highlighted below.  Click on it to see what happens:

     Current Conjecture:
     (equal (app (app (app (app x1 x2) (app x3 x4)) (app x5 x6)) x7)
            (app x1 (app (app x2 x3) (app (app x4 x5) (app x6 x7)))))

The Induction Scheme Selected for the App Example    The Induction Scheme Selected for the App Example

     (AND
        (IMPLIES (AND (NOT (ENDP A))         ; Induction Step: test
                      (:P (CDR A) B C))      ;  and induction hypothesis
                 (:P A B C))                 ;  implies induction conclusion.
        (IMPLIES (ENDP A) (:P A B C)))       ; Base Case

The formula beginning with this parenthesis is the induction scheme
suggested by (APP A B) applied to (P A B C).

It is a conjunction (AND <>) of two formulas.

The first is the induction step and the second is the base case.

The Induction Step in the App Example    The Induction Step in the App Example

This formula is the Induction Step.  It basically consists of three
parts, a test identifying the inductive case, an induction hypothesis
and an induction conclusion.

     (IMPLIES (AND (NOT (ENDP A))      ; Test
                   (:P (CDR A) B C))   ; Induction Hypothesis
              (:P A B C))              ; Induction Conclusion

When we prove this we can assume

       * A is not empty, and that

       * the associativity conjecture holds for a ``smaller'' version of
         A, namely, (CDR A).

Under those hypotheses we have to prove the associativity conjecture
for A itself.

The Instantiation of the Induction Scheme    The Instantiation of the Induction Scheme

The induction scheme just shown is just an abbreviation for our real
goal.

To obtain our actual goals we have to replace the schema :P by the
associativity conjecture (instantiated as shown in the scheme).

This produces two actual goals, the induction step and the base case.

The Justification of the Induction Scheme    The Justification of the Induction Scheme

This paragraph explains why the induction selected is legal.  The
explanation is basically the same as the explanation for why the
recursion in (APP A B) terminates.

The Proof of the Associativity of App    The Proof of the Associativity of App

Next on the Walking Tour:  Overview of the Simplification of the Induction Step to T

Here is the theorem prover's output when it processes the defthm
command for the associativity of app.  We have highlighted text for
which we offer some explanation, and broken the presentation into
several pages.  Just follow the Walking Tour after exploring the
explanations.

     ACL2!>(defthm associativity-of-app
             (equal (app (app a b) c)
                    (app a (app b c))))

     Name the formula above *1.

     Perhaps we can prove *1 by induction.  Three induction schemes are
     suggested by this conjecture.  Subsumption reduces that number to two.
     However, one of these is flawed and so we are left with one viable
     candidate.

     We will induct according to a scheme suggested by (APP A B).  If we
     let  (:P A B C) denote *1 above then the induction scheme we'll use
     is
     (AND
        (IMPLIES (AND (NOT (ENDP A))
                      (:P (CDR A) B C))
                 (:P A B C))
        (IMPLIES (ENDP A) (:P A B C))).
     This induction is justified by the same argument used to admit APP,
     namely, the measure (ACL2-COUNT A) is decreasing according to the relation
     O< (which is known to be well-founded on the domain recognized
     by O-P).  When applied to the goal at hand the above induction
     scheme produces the following two nontautological subgoals.

Next on the Walking Tour:  Overview of the Simplification of the Induction Step to T

The Q.E.D. Message    The Q.E.D. Message

Q.E.D. stands for "quod erat demonstrandum" which is Latin for "which
was to be demonstrated" and is the signal that a proof is completely
done.

The Rules used in the Associativity of App Proof    The Rules used in the Associativity of App Proof

Note that under Rules we list the runes <> of all the rules used in the
proof.  This list says that we used the rewrite rules CAR-CONS and
CDR-CONS, the definitions of the functions NOT, ENDP and APP, and
primitive type reasoning (which is how we simplified the IF and EQUAL
terms).

For what it is worth, IMPLIES and AND are actually macros <> that are
expanded into IF expressions before the proof ever begins.  The use of
macros is not reported among the rules.

The Simplification of the Induction Conclusion (Step 0)    the Simplification of the Induction Conclusion (Step 0)

     Subgoal *1/2'
     (IMPLIES (AND (CONSP A)
                   (EQUAL (APP (APP (CDR A) B) C)
                          (APP (CDR A) (APP B C))))
              (EQUAL (APP (APP A B) C)
                     (APP A (APP B C)))).

Click on the link above to replace (APP A B) by its definition.

The Simplification of the Induction Conclusion (Step 1)    the Simplification of the Induction Conclusion (Step 1)

     Subgoal *1/2'
     (IMPLIES (AND (CONSP A)
                   (EQUAL (APP (APP (CDR A) B) C)
                          (APP (CDR A) (APP B C))))
              (EQUAL (APP (IF (CONSP A)
                              (CONS (CAR A) (APP (CDR A) B))
                              B)
                          C)
                     (APP A (APP B C)))).

Note that the IF expression above is the simplified body of APP.  But
we know the test (CONSP A) is true, by the first hypothesis.  Click on
the link above to replace the test by T.  Actually this step and
several subsequent ones are done during the simplification of the body
of APP but we want to illustrate the basic principles of simplification
without bothering with every detail.

The Simplification of the Induction Conclusion (Step 10)    the Simplification of the Induction Conclusion (Step 10)

     Subgoal *1/2'
     (IMPLIES (AND (CONSP A)
                   (EQUAL (APP (APP (CDR A) B) C)
                          (APP (CDR A) (APP B C))))
              (EQUAL (APP (APP (CDR A) B) C)
                     (APP (CDR A) (APP B C)))).

Click on the link above to use the Induction Hypothesis (which is the
second of the two hypotheses above and which is identical to the
rewritten conclusion).

The Simplification of the Induction Conclusion (Step 11)    the Simplification of the Induction Conclusion (Step 11)

     Subgoal *1/2'
     (IMPLIES (AND (CONSP A)
                   (EQUAL (APP (APP (CDR A) B) C)
                          (APP (CDR A) (APP B C))))
              T)

Click on the link above to use the definition of IMPLIES.  Since the
conclusion of the implication is now identically T, the implication
simplifies to T.

The Simplification of the Induction Conclusion (Step 12)    the Simplification of the Induction Conclusion (Step 12)

     Subgoal *1/2'
     T

So, indeed, Subgoal *1/2' does simplify to T!

You can see that even in an example as simple as this one, quite a lot
happens in simplification.

You may see Overview of the Simplification of the Induction Step to T
to return to the main proof.

The Simplification of the Induction Conclusion (Step 2)    the Simplification of the Induction Conclusion (Step 2)

     Subgoal *1/2'
     (IMPLIES (AND (CONSP A)
                   (EQUAL (APP (APP (CDR A) B) C)
                          (APP (CDR A) (APP B C))))
              (EQUAL (APP (IF T
                              (CONS (CAR A) (APP (CDR A) B))
                              B)
                          C)
                     (APP A (APP B C)))).

Click on the link above to apply the Axiom (IF T x y) = x.

The Simplification of the Induction Conclusion (Step 3)    the Simplification of the Induction Conclusion (Step 3)

     Subgoal *1/2'
     (IMPLIES (AND (CONSP A)
                   (EQUAL (APP (APP (CDR A) B) C)
                          (APP (CDR A) (APP B C))))
              (EQUAL (APP (CONS (CAR A) (APP (CDR A) B))
                          C)
                     (APP A (APP B C)))).

Click on the link above to apply the expand the definition of APP here.

The Simplification of the Induction Conclusion (Step 4)    the Simplification of the Induction Conclusion (Step 4)

     Subgoal *1/2'
     (IMPLIES (AND (CONSP A)
                   (EQUAL (APP (APP (CDR A) B) C)
                          (APP (CDR A) (APP B C))))
              (EQUAL (IF (CONSP (CONS (CAR A) (APP (CDR A) B)))
                         (CONS (CAR (CONS (CAR A) (APP (CDR A) B)))
                               (APP (CDR (CONS (CAR A) (APP (CDR A) B)))
                                    C))
                         C)
                     (APP A (APP B C)))).

Click on the link above to apply the Axiom (CONSP (CONS x y)) = T.

The Simplification of the Induction Conclusion (Step 5)    the Simplification of the Induction Conclusion (Step 5)

     Subgoal *1/2'
     (IMPLIES (AND (CONSP A)
                   (EQUAL (APP (APP (CDR A) B) C)
                          (APP (CDR A) (APP B C))))
              (EQUAL (IF T
                         (CONS (CAR (CONS (CAR A) (APP (CDR A) B)))
                               (APP (CDR (CONS (CAR A) (APP (CDR A) B)))
                                    C))
                         C)
                     (APP A (APP B C)))).

Click on the link above to apply the Axiom (CAR (CONS x y)) = x.

The Simplification of the Induction Conclusion (Step 6)    the Simplification of the Induction Conclusion (Step 6)

     Subgoal *1/2'
     (IMPLIES (AND (CONSP A)
                   (EQUAL (APP (APP (CDR A) B) C)
                          (APP (CDR A) (APP B C))))
              (EQUAL (IF T
                         (CONS (CAR A)
                               (APP (CDR (CONS (CAR A) (APP (CDR A) B)))
                                    C))
                         C)
                     (APP A (APP B C)))).

Click on the link above to apply the Axiom (CDR (CONS x y)) = y.

The Simplification of the Induction Conclusion (Step 7)    the Simplification of the Induction Conclusion (Step 7)

     Subgoal *1/2'
     (IMPLIES (AND (CONSP A)
                   (EQUAL (APP (APP (CDR A) B) C)
                          (APP (CDR A) (APP B C))))
              (EQUAL (IF T
                         (CONS (CAR A)
                               (APP (APP (CDR A) B)
                                    C))
                         C)
                     (APP A (APP B C)))).

Click on the link above to apply the Axiom (IF T x y) = x.

The Simplification of the Induction Conclusion (Step 8)    the Simplification of the Induction Conclusion (Step 8)

     Subgoal *1/2'
     (IMPLIES (AND (CONSP A)
                   (EQUAL (APP (APP (CDR A) B) C)
                          (APP (CDR A) (APP B C))))
              (EQUAL (CONS (CAR A)
                           (APP (APP (CDR A) B)
                                C))
                     (APP A (APP B C)))).

Click on the link above to expand the definition of APP here.  This
time, we'll do the whole expansion at once, including the
simplification of the resulting IF.  This is how ACL2 actually does it.

The Simplification of the Induction Conclusion (Step 9)    the Simplification of the Induction Conclusion (Step 9)

     Subgoal *1/2'
     (IMPLIES (AND (CONSP A)
                   (EQUAL (APP (APP (CDR A) B) C)
                          (APP (CDR A) (APP B C))))
              (EQUAL (CONS (CAR A)
                           (APP (APP (CDR A) B)
                                C))
                     (CONS (CAR A)
                           (APP (CDR A) (APP B C))))).

Click on the link above to apply the Axiom that (EQUAL (CONS x y) (CONS
u v)) is equal to the conjunction of (EQUAL x u) and (EQUAL y v).  In
this case, (EQUAL x u) is trivial, (EQUAL (CAR A) (CAR A)).

The Summary of the Proof of the Trivial Consequence    The Summary of the Proof of the Trivial Consequence

Note that at the conclusion of the proof, the system reminds you of the
earlier Warning.

It is a good idea, when the Q.E.D. flys by, to see if there were any
Warnings.

The Theorem that App is Associative    The Theorem that App is Associative

Next on the Walking Tour:  The Proof of the Associativity of App

     ACL2!>(defthm associativity-of-app
             (equal (app (app a b) c)
                    (app a (app b c))))

The formula above says app is associative.  The defthm <> command
instructs ACL2 to prove the formula and to name it
associativity-of-app.  Actually, the defthm command also builds the
formula into the data base as a rewrite <> rule, but we won't go into
that just yet.

What we will consider is how the ACL2 theorem prover proves this
formula.

If you proceed you will find the actual output of ACL2 in response to
the command above.  Some of the text is highlighted for the purposes of
the tour.  ACL2 does not highlight its output.

You will note that we sometimes highlight a single open parenthesis.
This is our way of drawing your attention to the subformula that begins
with that parenthesis.  By clicking on the parenthesis you will get an
explanation of the subformula or its processing.

Next on the Walking Tour:  The Proof of the Associativity of App

The Time Taken to do the Associativity of App Proof    The Time Taken to do the Associativity of App Proof

The time it took us to explain this proof may leave the impression that
the proof is complicated.  In a way, it is.  But it happens quickly.

The time taken to do this proof is about 1/10 second.  The rest of the
time (about 2/10 seconds) is spent in pre- and post-processing.

Basically, this proof flashes across your screen before you can read
it; you see the Q.E.D. and don't bother to scroll back to read it.  You
have more important things to do than read successful proofs.

The Tours    The Tours

ACL2 is a very large, multipurpose system.  You can use it as a
programming language, a specification language, a modeling language, a
formal mathematical logic, or a semi-automatic theorem prover, just to
name its most common uses.

This home page includes all of ACL2's online documentation, which is
quite extensive.  To help ease your introduction to ACL2, we have built
two tours through this documentation.

Newcomers to ACL2 should first take the "Flying Tour."  Then, if you
want to know more, take the "Walking Tour."

To start a tour, click on the appropriate icon below.

Next on the Flying Tour:  A Flying Tour of ACL2 Next on the
Walking Tour:  A Walking Tour of ACL2

For readers using Web browsers:  This "page" actually contains many
other pages of our documentation, organized alphabetically and separated
by many blank lines.  Be careful when using the scroll bar!

For readers using our :DOC or our TexInfo format in Emacs:  The tours
will probably be unsatisfying because we use gif files and assume you
can navigate "back."

The WARNING about the Trivial Consequence    The WARNING about the Trivial Consequence

This Warning alerts us to the fact that when treated as a rewrite rule,
the new rule TRIVIAL-CONSEQUENCE, rewrites terms of the same form as a
rule we have already proved, namely ASSOCIATIVITY-OF-APP.

When you see this warning you should think about your rules!

In the current case, it would be a good idea not to make
TRIVIAL-CONSEQUENCE a rule at all.  We could do this with :rule-classes
<> nil.

ACL2 proceeds to try to prove the theorem, even though it printed some
warnings.  The basic assumption in ACL2 is that the user understands
what he or she is doing but may need a little reminding just to manage
a complicated set of facts.

Undocumented Topic    Undocumented Topic

This topic has not yet been documented.  Sorry

Using the Associativity of App to Prove a Trivial Consequence    Using the Associativity of App to Prove a Trivial Consequence

Next on the Walking Tour:  Overview of the Proof of a Trivial Consequence

If we have proved the associativity-of-app rule, then the following
theorem is trivial:

     (defthm trivial-consequence
       (equal (app (app (app (app x1 x2) (app x3 x4)) (app x5 x6)) x7)
              (app x1 (app (app x2 x3) (app (app x4 x5) (app x6 x7))))))

Below we show the proof

Next on the Walking Tour:  Overview of the Proof of a Trivial Consequence

What Is ACL2(Q)    What Is ACL2?

Next on the Flying Tour:  What is a Mathematical Logic(Q)

ACL2 is a mathematical logic together with a mechanical theorem prover
to help you reason in the logic.

The logic is just a subset of applicative Common Lisp.

The theorem prover is an "industrial strength" version of the
Boyer-Moore theorem prover, Nqthm.

Models of all kinds of computing systems can be built in ACL2, just as
in Nqthm, even though the formal logic is Lisp.

Once you've built an ACL2 model of a system, you can run it.

You can also use ACL2 to prove theorems about the model.

Next on the Flying Tour:  What is a Mathematical Logic(Q)

What is Required of the User(Q)    What is Required of the User?

Next on the Flying Tour:  How Long Does It Take to Become an Effective User(Q)

It is not easy to build ACL2 models of complex systems.  To do so, the
user must understand

       * the system being modeled, and

       * ACL2, at least as a programming language.

It is not easy to get ACL2 to prove hard theorems.  To do so, the user
must understand

       * the model,

       * ACL2 as a mathematical logic, and

       * be able to construct a proof (in interaction with ACL2).

ACL2 will help construct the proof but its primary role is to prevent
logical mistakes.  The creative burden - the mathematical insight into
why the model has the desired property - is the user's responsibility.

Next on the Flying Tour:  How Long Does It Take to Become an Effective User(Q)

What is a Mathematical Logic(Q)    What is a Mathematical Logic?

Next on the Flying Tour:  What is a Mechanical Theorem Prover(Q)

A mathematical logic is a formal system of formulas (axioms) and rules
for deriving other formulas, called theorems.

A proof is a derivation of a theorem.  To see a concrete proof tree,
see A Trivial Proof.

Why should you care?  The neat thing about Theorems is that they are
"true."  More precisely, if all the axioms are valid and the rules are
validity preserving, then anything derived from the axioms via the
rules is valid.

So, if you want to determine if some formula is true, prove it.

Next on the Flying Tour:  What is a Mechanical Theorem Prover(Q)

What is a Mechanical Theorem Prover(Q)    What is a Mechanical Theorem Prover?

Next on the Flying Tour:  What is a Mechanical Theorem Prover(Q) (cont)

A mechanical theorem prover is a computer program that finds proofs of
theorems.

The ideal mechanical theorem prover is automatic:  you give it a
formula and it gives you a proof of that formula or tells you there is
no proof.

Unfortunately, automatic theorem provers can be built only for very
simple logics (e.g., propositional calculus) and even then practical
considerations (e.g., how many centuries you are willing to wait) limit
the problems they can solve.

Next on the Flying Tour:  What is a Mechanical Theorem Prover(Q) (cont)

What is a Mechanical Theorem Prover(Q) (cont)    What is a Mechanical Theorem Prover? (cont)

Next on the Flying Tour:  About Models

To get around this, mechanical theorem provers often require help from
the user.

See ACL2 as an Interactive Theorem Prover to continue downward.

Next on the Flying Tour:  About Models

You Must Think about the Use of a Formula as a Rule    You Must Think about the Use of a Formula as a Rule

Next on the Walking Tour:  Using the Associativity of App to Prove a Trivial Consequence

This is good and bad.

The good news is that you can program ACL2's simplifier.

The bad news is that when you command ACL2 to prove a theorem you must
give some thought to how that theorem is to be used as a rule!

For example, if you engaged in the mathematically trivial act of proving
the associativity rule again, but with the equality reversed, you would
have programmed ACL2's rewriter to loop forever.

You can avoid adding any rule by using the command:

     (defthm associativity-of-app
       (equal (app (app a b) c)
              (app a (app b c)))
       :rule-classes nil)

Next on the Walking Tour:  Using the Associativity of App to Prove a Trivial Consequence

REAL    ACL2(r) support for real numbers

ACL2 supports rational numbers but not real numbers.  However, starting
with Version  2.5, a variant of ACL2 called "ACL2(r)" supports the real
numbers by way of non-standard analysis.  ACL2(r) was conceived and
first implemented by Ruben Gamboa in his Ph.D.  dissertation work,
supervised by Bob Boyer with active participation by Matt Kaufmann.
The Makefile provided with ACL2 has target large-acl2r for building
ACL2(r) images.  To see which image you have, see if the prompt
includes the string "(r)", e.g.:

     ACL2(r) !>

Or, look at (@ acl2-version) and see if "(r)" is a substring.

In ACL2 (as opposed to ACL2(r)), when we say "real" we mean "rational."

Caution:  ACL2(r) should be considered experimental as of Version 2.5:
although we (Kaufmann and Moore) have carefully completed Gamboa's
integration of the reals into the ACL2 source code, our primary concern
to date has been to ensure unchanged behavior when ACL2 is compiled in
the default manner, i.e., without the non-standard extensions.  As for
every release of ACL2, at the time of this release we are unaware of
soundness bugs in ACL2 Version  2.5.  We are confident that ACL2(r)
will behave much as it does now and will ultimately be sound; but we
have not yet argued the soundness of every detail of the integration.

There is only limited documentation on the non-standard features of
ACL2(r).  We hope to provide more documentation for such features in
future releases.  Please feel free to query the authors if you are
interested in learning more about ACL2(r).  Gamboa's dissertation may
also be helpful.

I-CLOSE    ACL2(r) test for whether two numbers are infinitesimally close

(I-close x y) is true if and only if x-y is an infinitesimal number.
This predicate is only defined in ACL2(r) (see REAL).

I-LARGE    ACL2(r) recognizer for infinitely large numbers

(I-large x) is true if and only if x is non-zero and 1/x is an
infinitesimal number.  This predicate is only defined in ACL2(r) (see
REAL).

I-LIMITED    ACL2(r) recognizer for limited numbers

(I-limited x) is true if and only if x is a number that is not
infinitely large.  This predicate is only defined in ACL2(r) (see
REAL).

I-SMALL    ACL2(r) recognizer for infinitesimal numbers

(I-small x) is true if and only if x is an infinitesimal number
(possibly 0).  This predicate is only defined in ACL2(r) (see
REAL).

REAL-LISTP    ACL2(r) recognizer for a true list of real numbers

The predicate real-listp tests whether its argument is a true list of
real numbers.  This predicate is only defined in ACL2(r) (see
REAL).

STANDARD-PART    ACL2(r) function mapping limited numbers to standard numbers

(Standard-part x) is, for a given i-limited number x, the unique real
number infinitesimally close (see I-CLOSE) to x.  This function
is only defined in ACL2(r) (see REAL).

STANDARDP    ACL2(r) recognizer for standard objects

(Standardp x) is true if and only if x is a "standard" object.  This
notion of "standard" comes from non-standard analysis and is discussed
in Ruben Gamboa's dissertation.  In brief, all the familiar objects are
standard: e.g., the familiar real numbers are standard, but non-zero
infinitesimals are not standard, and the familiar integers are
standard, but not those that exceed every integer that you can express
in the usual way (1, 2, 3, and so on).  Similarly, the familiar lists
are standard, but not so a list that contains a large number of
integers, where "large" means more than the standard integers.  The set
of standard numbers is closed under the usual arithmetic operations,
hence the sum of a standard number and a non-zero infinitesimal is not
standard, though it is what is called "limited" (see I-LIMITED).

This predicate is only defined in ACL2(r) (see REAL).

RELEASE-NOTES    pointers to what has changed

This section of the online documentation contains notes on the changes
that distinguish successive released versions of ACL2.

The current version of ACL2 is the value of the constant (@
acl2-version).

NOTE-2-0    ACL2 Version 2.0 (July, 1997) Notes

This is the first version of ACL2 released under the copyright of the
University of Texas (UT).  Future releases of ACL2 will be made from UT
rather than Computational Logic, Inc. (CLI).  Version 2.0 is just
Version 1.9 as released by CLI, with a few bugs fixed.

A bug causing an infinite loop was fixed in functional instantiation.
The bug manifested itself when two conditions occurred simultaneously:
First, the functional substitution replaces a function symbol, e.g.,
FOO, with a LAMBDA expression containing a free variable (a variable
not among in the LAMBDA formals).  And, second, in one of the
constraints being instantiated there is a call of the function symbol
FOO within the scope of another LAMBDA expression.  Unless you used
such a functional substitution, this bug fix will not affect you.

Less important notes:

The implementation of PRINC$ was changed so that it was no longer
sensitive to the external setting of *print-base* and other Common Lisp
special variables.

Typographical errors were fixed in the documentation.

NOTE-2-1    ACL2 Version  2.1 (December, 1997) Notes

The identity function case-split has been added.  It is similar to
force but causes an immediate split of the top-level goal on whether
the indicated hypothesis is true.

Less important notes:

Minor bugs in the documentation were fixed.

NOTE-2-2    ACL2 Version  2.2 (August, 1998) Notes

Important changes:

A bug was fixed in the compile command, :comp.  The compiled code
produced by :comp in previous versions could be wildly incorrect
because of a confusion between the printer and the reader regarding
what was the current Lisp *package*.  This bug could manifest itself
only if you used the :comp command to compile previously uncompiled
functions while the current package was different from "ACL2".  What
happened in that situation depended upon what symbols were imported
into your current package.  The most likely behavior is that the
compiler would break or complain or the resulting compiled code would
call functions that did not exist.

There have been no other important changes to the code.

However, this release contains some useful new books, notably those on
the books subdirectories cli-misc and ihs.  Both have README files.
The ihs books provide support for integer hardware specifications.
These books were crucial to Bishop Brock's successful modeling of the
Motorola CAP.  We thank Bishop for producing them and we thank all
those who worked so hard to get these books released.  We highly
recommend the ihs books to those modeling ALUs and other arithmetic
components of microprocessors or programming languages.

In previous versions of ACL2, the arithmetic books, found on
books/arithmetic/, included the addition of several unproved axioms
stating properties of the rationals that we believed could be derived
from our "official" axioms but which we had not mechanically proved.
The axioms were found in the book rationals-with-axioms.lisp, which was
then used in the uppermost arithmetic books top.lisp and
top-with-meta.lisp.  John Cowles has now provided us with ACL2 proofs
of those "axioms" and so in this release you will find both
rationals-with-axioms.lisp and rationals-with-axioms-proved.lisp.  The
former is provided for compatibility's sake.  The latter is identical
but contains defthms where the former contains defaxioms.  The top-most
books have been rebuilt using "-axioms-proved" book.  Thanks John.

Less important notes:

Bishop Brock found a bug in translated-acl2-unwind-protectp4.  Jun
Sawada reported a bug in linear arithmetic that caused us not to prove
certain trivial theorems concluding with (not (equal i j)).  We have
fixed both.

We now prohibit definitions that call certain event commands such as
DEFTHM and TABLE because our Common Lisp implementations of them differ
from their ACL2 meanings (so that compiled books can be loaded
correctly and efficiently).

Minor bugs in the documentation were fixed.

NOTE-2-3    ACL2 Version  2.3 (October, 1998) Notes

Important changes:

Versions of ACL2 preceding this one contain a subtle soundness bug!  We
found a flaw in our detection of subversive-recursions.  The bug
allowed some subversive recursions to slip through undetected.

We believe it would have been difficult to have exploited this flaw
inadvertently.  In particular, the following five conditions are
necessary.
(1) Introduce a constrained function, say f, via an encapsulate.
(2) In the same encapsulation, define a clique of mutually recursive
functions.  This clique must be non-local and in :logic mode.
(3) In that mutually recursive clique, use the constrained function f
(perhaps indirectly) so that the termination argument for the clique
depends on properties of the witness for f.  Thus, f or some other
function dependent upon f, must be used in an argument in a recursive
call or in a term governing a recursive call.  Furthermore, the use of
f must be such that the termination proof cannot be done without
exploiting properties of the witness for f.  Other uses of the
constrained functions in the clique are ok.
(4) Fail to include the exploited properties of f among the constraints
of the encapsulation.
(5) Later, outside the encapsulation, explicitly use a functional
instantiation in which f is replaced by a function not enjoying the
crucial properties.
See subversive-recursions for details.

Less important notes:

We have begun to write some introductory tutorial material for those
who wish to learn to program in ACL2.  Most of this material is
HTML-based.  See the Hyper-Card on the ACL2 home page.

The documentation of verify-guards was improved to explain why one
might wish to verify the "guards" of a defthm event.  The missing
documentation was noticed by John Cowles.

A bug was fixed in cross fertilization.  The bug caused the system to
report that it had substituted one term for another when in fact no
substitution occurred.  The bug was noticed by Bill McCune.

NOTE-2-4    ACL2 Version  2.4 (August, 1999) Notes

Important changes:

We corrected a soundness bug in Version 2.3 related to the handling of
immediate-force-modep.  The bad behavior was noticed by Robert Krug.
Thanks!

We corrected a bug that permitted verify-guards to accept a function
even though a subfunction had not yet had its guards verified.  Thanks
to John Cowles for noticing this.

User defined single-threaded objects are now supported.  See stobj.

Less important notes:

We corrected a bug that prevented the intended expansion of some
recursive function calls.

We changed the handling of the primitive function ILLEGAL, which is
logically defined to be nil but which is programmed to signal an error,
so that when it is evaluated as part of a proof, it does not signal an
error.  The old handling of the function prevented some guard proofs
involving THE or LETs with internal declarations.

We corrected a bug that permitted some LOCAL DEFAXIOM events to slip
into certified books.

We corrected a bug that prevented the correct undoing of certain DEFPKG
forms.

Changes were made to support CMU Lisp.  Pete Manolios helped with these
changes.

Changes were made to make the make files more compatible with Allegro
Common Lisp.  Jun Sawada, who has been a great help with keeping ACL2
up and running at UT on various platforms, was especially helpful.
Thanks Jun.

NOTE-2-5    ACL2 Version  2.5 (June, 2000) Notes

Important Changes:

Concurrent with the release of ACL2 Version  2.5 is the publication of
two books about ACL2.  See the "Books and Papers about ACL2 and Its
Applications" on the ACL2 Home Page.

The books subdirectory now contains many new certifiable books,
including solutions to the exercises in the two published books and
full scripts for the case studies.  See books/README.html.

Improved Unix Makefile support for book certification has also been
written.  See books/README.html.

The list of symbols in *acl2-exports* has been considerably expanded.
If you have packages built by importing *acl2-exports* you might want
to look carefully at the new value of that constant.  The new value
includes all :logic mode functions as of Version  2.5, as well as all
documented macros and all built-in theorem names.

Include-book and certify-book were modified to have some additional
keyword arguments.  It is possible to certify a book containing
defaxiom and/or skip-proofs events and get warning messages or errors
signaled, according to the settings of these new flags.  In addition,
it is possible to specify in include-book whether the book must be
certified (under penalty of error if not).  The default values of these
new arguments cause warnings to be printed rather than errors signaled.

The above change involved altering the form of certificate files.  When
books certified under previous versions are included, more warnings
will be generated because these books are considered possibly to
contain defaxiom and/or skip-proofs events.

We anticipate further changes to this aspect of books and consider the
current mechanisms (for controlling whether warnings or errors are
signaled) just a prototype.  See also the discussion below of
"soundness related" warnings.  Your suggestions are welcome.

A discrepancy between ACL2 and Common Lisp was fixed, having to do with
declare ignore.  In past versions of ACL2, a formal parameter of a
defun was considered ignored if it was not used in the body, the guard
or the measure of the defun.  That meant that a variable used only in
the guard could not be declared ignored in ACL2; but some Common Lisp
compilers would complain because the variable was not used in the body.
Now, ACL2 considers a variable ignored if it is not used in the body.

ACL2 can now be built in releases 5.0 and later of Allegro Common Lisp.
(Other releases of Allegro Common Lisp and of other lisps continue to
be supported as well.)  This includes Allegro Common Lisp running on
Windows 98 platforms.  John Cowles helped us do some testing and
answered questions for us.  Thanks John!

We incorporated Ruben Gamboa's changes to allow the building of a
variant, ACL2(r), of ACL2, in which the user can reason about the real
numbers using non-standard analysis.  See REAL.  Note that
ACL2(r) and ACL2 have different underlying theories, and books
certified in one system may not be included in the other.  For backward
compatibility and to ensure a smooth transition, ACL2 is built by
default, not ACL2(r).  This is a compile-time switch; see the makefile
for instructions.  There should be no changes to ACL2 resulting from
the capability of building ACL2(r) from the same sources.  Also see
ACKNOWLEDGMENTS for more on the history of ACL2(r).

A large number of bugs (some affecting soundness) were fixed, and many
small new features were added.  See below.

Less Important Changes:

Some warnings are now considered "soundness related," namely, those
that advise you that an uncertified book has been included or that a
book containing DEFAXIOM or SKIP-PROOFS events.  (Technically,
DEFAXIOMs do not imperil soundness in the proof- theoretic sense,
though they may imperil the validity of theorems.  But you sould know
when a book has added an axiom to your logic!)  In previous versions of
ACL2, all warnings were inhibited if the token warning was included in
the argument to set-inhibit-output-lst.  Now, soundness related
warnings are printed even if warnings have been inhibited.  To inhibit
all warnings, supply the token warning! to set-inhibit-output-lst.

Several bugs in defstobj were fixed, relating to the possibility that
some of the subfunctions introduced by the defstobj were already
defined.

:Puff no longer tries to expand defstobj events.  Previously, the
attempt would cause a hard error.

A soundness bug was fixed.  The bug might have been exercised if you
had an alternative definition (implies hyps (equiv (fn ...) body)) in
which equiv is an equivalence relation other than EQUAL.  In this case,
calls of fn might have been expanded to body in places that were not
equiv-hittable.

An obscure soundness bug was fixed.  The bug was exercised only if you
had a metafunction with a computed hypothesis (i.e., a "meta hypothesis
function"), the hypothesis contained a free variable, i.e., a variable
not involved in the term being rewritten, and the free variable
occurred in the output of the metafunction.  The possibility of this
bug was brought to our attention by Robert Krug.

We fixed a bug in the handling of hide related to the question of
whether a variable symbol occurs in a term.  The old code did not find
the variable and could cause the system to throw away a hypothesis
about it on the grounds that it was never mentioned.  Rob Sumners
helped discover this problem.

The handling of :elim rules was generalized, permitting arbitrary known
equivalence relations instead of merely equal in the concluding
equality.

The printing of runes (rule names; see RUNE) used has been made
"deterministic," both in proof output and in proof attempt summaries,
by sorting the runes before printing.

The handling of free variables has been improved for hypotheses such as
(< 0 X), and more generally, any hypotheses involving a comparison with
0 (even for example (< X 1) where X is known to be an integer, which is
handled as (<= X 0)).  Thanks to Robert Krug for bringing relevant
examples to our attention.

A new value, :comp, has been implemented for the :load-compiled-file
keyword of include-book.  If this value is supplied, then a compiled
file will always be loaded, even if that requires creating the compiled
file first.

The event include-book now generates a warning when a compiled file is
expected but not found (see INCLUDE-BOOK).  Formerly, it only
did so when executed at the top level; it failed to generate the
warning when executed on behalf of a surrounding include-book command.

Certain redefinition warnings generated by Allegro Common Lisp have
been eliminated.

A new key has been implemented for the acl2-defaults-table,
:bogus-mutual-recursion-ok, set with :set-bogus-mutual-recursion-ok.
Thanks to David Russinoff for pointing out the utility of such a key.

A bug was fixed in defun-sk that prevented its generated events from
being accepted when guard verification is being performed.  Thanks to
Bill Young for bringing this problem to our attention.  A second bug
was brought to our attention by Pete Manolios, which was causing
certain defun-sk events to be rejected.  That problem has been fixed,
and an "Infected" warning has also been eliminated.

The command good-bye now works with Allegro Common Lisp.

A low-level bug was fixed that could, for example, cause an error such
as "Error: Expected 5 args but received 4 args" when interrupting a
local event.

A bug has been fixed in the proof-checker related to definition
expansion.  Thanks to Pete Manolios for bringing this to our attention
with a simple example.

A bug has been fixed related to the :bdd hint in the presence of
equivalence relations.  Thanks to Pete Manolios for bringing this to our
attention with a simple example.

The functions position and position-equal formerly required the second
argument to be a true list.  In accordance with Common Lisp, we now
also allow the second argument to be a string.  This could cause
earlier proofs about these functions to fail unless true-listp is known
to hold where necessary.

Robert Krug wrote a patch, which has been incorporated, to prevent
certain infinite loops that can arise in linear arithmetic.  Thanks,
Robert!

The macro let* no longer requires the bound variables to be distinct.

An obscure bug was fixed related to congruence rules.  The bug would
sometimes cause ACL2 to behave as though no rules (other than equality)
were available for some argument positions.  Thanks to Pete Manolios for
bringing this bug to our attention.

Documentation topics have been added for hard-error and prog2$, and the
documentation for illegal has been improved.  Thanks to Rob Sumners for
a useful suggestion in the examples in documentation for prog2$ and a
fix in documentation for sublis.

The event form certify-book was made more secure, in that it can now
catch attempts to write a book to disk during its certification.
Thanks to Rob Sumners for pointing out the insecurity of the existing
mechanism.

A Y2K problem was fixed with our applicative handling of dates.

Accessors and updaters for stobjs have been made more efficient when
the underlying lisp is Allegro Common Lisp, by the use of appropriate
simple array declarations.

A raw Lisp break had been possible when a certified book that had no
guard verification was included in a session after
(set-verify-guards-eagerness 2).  This has been fixed.

The keyword command :comp can now be used to compile only raw Lisp
functions, excluding executable counterparts, by supplying the argument
:raw.

Rewrite rule nth-of-character-listp was removed from source file
axioms.lisp since it is essentially subsumed by characterp-nth.

Printing has been sped up.  In one example the improvement was over 50%
in both Allegro and GCL.

We now allow printing in a "downcase" mode, where symbols are printed
in lower case.  All printing functions except print-object$ now print
characters in lower case for a symbol when the ACL2 state global
variable print-case has value :downcase and vertical bars are not
necessary for printing that symbol.  See IO for a discussion of
the macros acl2-print-case and set-acl2-print-case.  The default
printing remains unchanged, i.e., symbols are printed in upper case
when vertical bars are not required.

A low-level printing function (prin1$) was modified so that it is not
sensitive to various Common Lisp globals related to printing.  So for
example, the function fmt is no longer sensitive to the value of Common
Lisp global *print-case*.  (The preceding paragraph explains how to
control the case for printing in ACL2.)

The definition of array1p was fixed so that the :maximum-length of an
array must be strictly greater than the number specified in the
:dimensions field; they may no longer be equal.  This was always the
intention; the documentation (see ARRAYS) has remained
unchanged.  The corresponding change was also made to array2p.  Allegro
Common Lisp formerly caused an error when compress1 was called on an
array where the numbers above were equal; now, we get a guard violation
instead, which is appropriate.

In the context of theories, a name now represents not just the
corresponding :definition rune, as it has done in earlier versions of
ACL2, but also the corresponding :induction rune.  See THEORIES
for a discussion of runic designators.  Most users will rarely, if
ever, notice this change.  One situation where this change will make a
difference is after executing (in-theory (current-theory 'foo))
followed by (in-theory (enable bar)), where function bar is introduced
after event foo, and bar is recursively defined.  The latter in-theory
form now enables the rune (:induction bar), which implies that the
prover can use the induction scheme stored at definition time for bar.
Formerly, the rune (:induction bar) was not enabled by (in-theory
(enable bar)), and hence the induction scheme for bar was ignored even
when explicit :induct hints were supplied.

You may now supply xargs keyword pair :normalize nil in order to
prevent certain definitions from "hanging" when there are many
if-subexpressions.  see DEFUN.

We now translate type declarations of real into guards, as we have
already done for other types such as rational.  For example, (declare
(type real x)) generates the guard (rationalp x).  See
TYPE-SPEC.

The theorem prover now behaves reasonably under the combination of
specifying a value of t both for :otf-flg and for a hint
:do-not-induct.  Previously, it aborted the first time it would have
otherwise pushed a goal for induction, but now, it will continue and
wait until all induction subgoals have been pushed before it aborts.

We changed slightly the definition of round.  However, we believe that
the new definition is equivalent to the old.

The definition of Common Lisp function substitute has been added.

The following changes have been made in the use of file names within
ACL2.  We thank Warren Hunt and John Cowles for running some tests of
these changes on Macintosh and Windows 98 platforms (respectively).

     (1) Names of directories and files now use a syntax like that used
     for Unix (trademark of AT&T), where directories are separated using
     the "/" character even when the operating system is not Unix or
     Linux.  See PATHNAME.  ACL2 also continues to support its
     notion of _structured pathnames_ from Version  2.4 and before, but
     might not do so in future releases and hence no longer documents
     such syntax.

     (2) The command :set-cbd may now take a relative pathname as an
     argument.

     (3) When the macro ld is given a file name as a value for
     standard-oi, then if that file name is a relative pathname it
     refers to the result of prepending the connected book directory
     (see PATHNAME, see CBD, and see SET-CBD)
     in order to obtain an absolute pathname.  Simiarly for the ld
     specials standard-co and proofs-co.

It is no longer necessary to issue :set-state-ok t if you include a
stobj declaration for state, for example:

     (declare (xargs :stobjs state))

See DECLARE-STOBJS.

The proof-checker has been cleaned up a bit, including the
documentation and the capability (once again) to define pc-macro
commands (see DEFINE-PC-MACRO) and proof-checker meta commands
(see DEFINE-PC-META).

Recall that events generate summaries that include a line beginning
with "Warnings:", which is followed (on the same line) by zero or more
brief strings that summarize the warnings generated by that event.
Formerly, this warnings summary for an encapsulate or include-book
event did not include the summary strings for warnings generated by
subsidiary events.  This has been fixed.

Macro cw has been documented and now expands to a call of a ;logic mode
function.  See CW for a way to print to the screen without
having to involve the ACL2 state.  Thanks to Rob Sumners for suggesting
that we document this useful utility.

Functions duplicates, add-to-set-equal, intersection-eq, evens, and
odds are now :logic mode functions.

NOTE-2-5(R)    ACL2 Version  2.5(r) (June, 2000) Notes

Important changes to non-standard version:

Please see NOTE-2-5 for changes to Version  2.5 of ACL2.  We
hope to write more documentation for ACL2(r) in the future.

NOTE-2-6    ACL2 Version  2.6 (November, 2001) Notes

Because of the large number of modifications, we have divided up the
Version  2.6 notes into the following subtopics.

     o New functionality (see NOTE-2-6-NEW-FUNCTIONALITY):
     o Changes in proof engine (see NOTE-2-6-PROOFS):
     o Changes in rules and definitions (see NOTE-2-6-RULES):
     o Guard-related changes (see NOTE-2-6-GUARDS):
     o Proof-checker changes (see NOTE-2-6-PROOF-CHECKER):
     o System-level changes (see NOTE-2-6-SYSTEM):
     o Other (minor) changes (see NOTE-2-6-OTHER):

NOTE-2-6-GUARDS    ACL2 Version  2.6 Notes on Guard-related Changes

When you declare that a function treats certain formals as :stobjs, the
guard of the function is automatically extended to include the
corresponding stobj-recognizer calls.  For example, if a definition
includes (declare (xargs :stobjs (ST))) then the guard of the function
is changed by the addition of the conjunct (ST-P ST).

One impact of this is that if you use the built-in ACL2 state as a
formal parameter of a function, (STATE-P STATE) is added to the guard.
This may introduce a guard where there was none in previous versions of
the system.  In older versions, therefore, no attempt would be made to
verify-guards, while in the new version, we would attempt guard
verification.  You may wish to add (declare (xargs :verify-guards nil))
to such definitions.

A related change affects users who do not use stobjs or state.  In
previous versions of the system -- as now -- a type declaration
extended the guard you provided explicitly.  Thus, if you wrote
(declare (type integer n)) then (INTEGERP n) was added to your guard.
This is still the case and :stobjs recognizers are similarly added.
But in older versions of the system we "added" the conjuncts without
checking whether they were already present in the guard you provided.
This sometimes produced such guards as (and (integerp n) (integerp n))
where the first was produced by your type declaration and the second
was your :guard.  We now eliminate redundant conjuncts; this may
rearrange the order of the conjuncts.

The guard conjectures for functions using stobjs have been simplified
somewhat by taking advantage of the syntactic restrictions checked for
single-threaded objects.

The following functions have been modified so that character and string
arguments are restricted to standard characters.  (See
STANDARD-CHAR-P and see STANDARD-CHAR-LISTP.)

     upper-case-p lower-case-p char-upcase char-downcase
     string-downcase1 string-downcase string-upcase1 string-upcase
     char-equal string-equal1 string-equal

Also, function standard-string-alistp replaces function string-alistp,
with concomitant changes in the guard to assoc-string-equal, and in
variable *acl2-exports*.  Also, lemma
standard-string-alistp-forward-to-alistp replaces lemma
string-alistp-forward-to-alistp.  There is a new lemma
standard-char-p-nth, which has also been added to *acl2-exports*.

The guard had been inadvertently omitted from the definition of the
function substitute (and its subroutine substitute-ac).  This omission
has been corrected; also, the guard is slightly stronger than the
documentation had claimed (and that has been corrected).

NOTE-2-6-NEW-FUNCTIONALITY    ACL2 Version  2.6 Notes on New Functionality

A fundamental change is the provision of the "nu-rewriter" for
simplifying expressions composed of NTH, UPDATE-NTH, and
UPDATE-NTH-ARRAY applications and LET expressions and other calls of
non-recursive functions or LAMBDA expressions involving those symbols.
The nu-rewriter applies the obvious rewrite rule for (NTH i (UPDATE-NTH
j v s)) and the analogous rule for UPDATE-NTH-ARRAY.  See
NU-REWRITER  The nu-rewriter can be enabled with set-nu-rewriter-mode.

A new flag has been added to the xargs of defun permitting the
declaration that the function is non-executable.  The usage is (declare
(xargs :non-executable t)) and the effect is that the function has no
executable counterpart.  On the positive side:  the function is
permitted to use single-threaded object names and functions
arbitrarily, as in theorems rather than as in executable definitions.
Such functions are not permitted to declare any names :stobjs but
accessors, etc., may be used, just as in theorems.

A new flag has been added to permit the system to abbreviate output by
introducing LET* notation identifying common subterms.  The formula
being proved is not affected; this flag changes its displayed form
only.  See set-let*-abstractionp.

A "raw mode" has been added, primarily for faster loading of
applications.  see SET-RAW-MODE.

Functions alphorder and lexorder have been put in :logic mode.
Lexorder is now a total order ordering of the ACL2 universe, and
theorems are included to that effect.  Thanks to Pete Manolios for
suggesting the idea and providing events to use, and to Rob Sumners for
assistance with some modifications.  See also the new book
books/misc/total-order for an irreflexive total order.

The ACL2 user can now make system calls to the host operating system.
See SYS-CALL and see SYS-CALL-STATUS.  Thanks to Rob
Sumners for working out this idea with Pete Manolios and Robert Krug,
who we also thank, and for working out the implementation with us.

It is no longer required to use absolute pathnames in include-book
forms that have been executed before a certify-book.  Any relative
pathname strings in such contexts will be expanded into absolute
pathnames before they are saved in the portcullis of the certificate of
the book being certified.

ACL2 can now be built on top of Allegro Common Lisp 6.0, and also on
Windows platforms on top of Allegro Common Lisp and GCL.  Thanks to Pete
Manolios and Vinay K. Siddhavanahalli for their help with Windows.

Rob Sumners has designed and provided an initial implementation for two
improvements to defstobj (also see STOBJ).  First, array fields
can now be resized.  Resize and length functions are provided for array
fields, which can be used to resize stobj array fields dynamically.
The recognizers for array fields have been simplified to accommodate
this change, so that they only check that each element of the array
field has the specified type.  Second, performance has been improved
for stobjs with a large number of fields, by changing their Common Lisp
implementation to store the fields in a simple vector instead of a list.

Now stobjs may be bound locally; see WITH-LOCAL-STOBJ.  Thanks
to Rob Sumners, who encouraged us to implement this capability, was an
early user of it, and participated usefully in discussions on its
design.

New functions fms!, fmt!, and fmt1! are the same as their respective
functions without the "!," except that the "!" functions are guaranteed
to print forms that can be read back in (at a slight readability cost).

We added extended-metafunctions, metafunctions which allow state and
context sensitive rewriting to some extent.  We thank Robert Krug for
pushing for and on this idea.

The documentation has been improved.  In particular, a new
documentation topic provides a gentle introduction to ACL2 arrays --
see ARRAYS-EXAMPLE -- and additional documentation has been
provided for getting started with proof trees in emacs -- see
PROOF-TREE-EMACS.

New Makefile targets fasl and o have been added to the books/ directory
of the distribution.  For example, you might first certify books using
an ACL2 built on top of GCL (which creates compiled files with suffix
o).  Then, when standing in the books/ directory, you might execute the
command

     make fasl ACL2=my-allegro-acl2

which will create compiled (.fasl) files for Allegro Common Lisp,
assuming that my-allegro-acl2 starts up an ACL2 built on that Common
Lisp.

The macro let* now allows variables to be declared ignored.  See
LET* and see LET.

The user may now control backchaining.  This feature was designed and
primarily implemented by Robert Krug (though the authors of ACL2 are
resposible for any errors); thanks, Robert!  See
BACKCHAIN-LIMIT.

It is now possible to "slow down" the rate at which case splits are
generated by the simplifier.  See SET-CASE-SPLIT-LIMITATIONS.

Accesses to stobjs using nth or update-nth are now displayed using
symbolic constants instead of numeric indices.  For example, given the
event

     (defstobj foo a b :renaming ((b c)))

then the term (nth 0 foo) will be displayed (for example, during
proofs) as (nth *a* foo) while (nth 1 foo) will be displayed as (nth
*c* foo).  The defstobj event now correspondingly introduces a defconst
event for each field accessor function, introducing a constant whose
name is obtained from the accessor's name by prefixing and suffixin a
"*," as in the example above: accessor a generates (defconst *a* 0) and
accessor c generates (defconst *c* 1). See NTH-ALIASES-TABLE
for how to extend this feature for alternate names of stobjs.

Computed hints have been improved.  It is now possible to detect within
a computed hint whether the goal clause is stable under simplification;
it is also possible for a computed hint to change the list of available
hints.  See COMPUTED-HINTS.

It is now possible to provide "default hints" that are appended to the
hints explicitly provided.  See SET-DEFAULT-HINTS.

Using computed hints (see COMPUTED-HINTS) and default hints
(see SET-DEFAULT-HINTS) it is possible to implement a book that
supports "priority phased simplification."  Using this book you can
assign priorities to your rules and cause the theorem prover to
simplify each goal maximally under all the rules of one priority before
enabling rules of the next priority.  See books/misc/priorities.lisp.

The macro defabbrev has been improved to allow declare forms and
documentation strings and to do more error-checking.  Thanks to Rob
Sumners for designing this enhancement and providing the first
implementation.  See DEFABBREV.

Further changes were made to support CMU Lisp.  Wolfhard Buss helped
with these changes.

A new table was added that is used when printing proof output, so that
nests of right-associated calls of a binary function are replaced by
corresponding macro calls, as has been the case for binary-+ and +,
binary-append and append, and so on.  See ADD-BINOP.

Operators logand, logior, logxor, and logeqv are now macros (formerly,
they were functions) that call corresponding binary functions (e.g.,
binary-logand) defined in source file "axioms.lisp".  Thanks to Rob
Sumners for this enhancement.  Proof output will however continue to
show calls of logand, logior, logxor, and logeqv.

Function (allocate-fixnum-range fixnum-lo fixnum-hi) sets aside more
"permanent" fixnums in GCL.

ACL2 now runs under CLISP.  Thanks to Wolfhard Buss and Sam Steingold
for their assistance with the port.

Michael "Bogo" Bogomolny has created a search engine, accessible from
the ACL2 home page.  For that purpose he modified the HTML translator
to create one file per topic (a good idea in any case).  Thanks, Bogo!

An emacs file of potential (but optional) use for ACL2 users may be
found in emacs/emacs-acl2.el.  In particular, this file supports the
use of proof trees (see PROOF-TREE).

Some books have been added or modified.  In particular, Robert Krug has
contributed books/arithmetic-2/, which provides an alternative to the
existing collection of books about arithmetic, books/arithmetic/.  For a
discussion of the distributed books see the link to README.html in the
installation instructions.

NOTE-2-6-OTHER    ACL2 Version  2.6 Notes on Other (Minor) Changes

Warning strings are now case-insensitive.  See
SET-INHIBIT-WARNINGS.

ACL2 causes a warning when an in-theory hint or event causes a 0-ary
function's definition to be disabled but its :executable-counterpart to
be enabled.

A minor modification has been made to defstobj that can have a positive
impact on performance in Allegro Common Lisp.  (For Lisp hackers:  the
stobj name was formerly declared special, and that was disabling
Allegro's tail-merging routing for compilation of some recursive
functions using stobjs.)  The downside is that stobj names can no
longer be evaluated in raw Lisp.  However, raw Lisp is not the right
place to be evaluating ACL2 forms anyhow; see SET-RAW-MODE.  We
thank Rob Sumners for bringing this issue to our attention.

Before Version  2.6, there has been the following problem with defstub
and encapsulate in the case that the current package is not the ACL2
package.  If a signature was specified using the symbol =>, then that
symbol had have been imported into the current package from the ACL2
package when the current package was defined.  There are no longer any
package restrictions on the use of =>.  Thanks to John Cowles for
bringing this problem to our attention.

Bugs in defun-sk have been fixed.  Defun-sk forms introducing functions
of no arguments were failing to be admitted, for example: (defun-sk
always-p1 () (forall (x) (p1 x))).  Thanks to John Cowles for bringing
this problem to our attention.  Also, defun-sk failed on an example in
the documentation (see TUTORIAL4-DEFUN-SK-EXAMPLE), as pointed
out by Matyas Sustik; this bug has been fixed as well.

The trace mechanism has been fixed to handle stobjs, and to avoid the
printing of so-called _enabled structures_.

The brr command :type-alist now produces more readable output.

An include-book of an uncertified book no longer loads an associated
compiled file.

We added a few checks to make sure that the underlying lisp is
suitable, for example checking that the reader is case-insensitive and
reads in symbols with upper-case names where appropriate.

We now warn when forcing (see FORCE) or immediate force mode
(see IMMEDIATE-FORCE-MODEP) change state between enabled and
disabled.  Also see ENABLE-IMMEDIATE-FORCE-MODEP and see
DISABLE-IMMEDIATE-FORCE-MODEP for information about these new macros,
which may be used to control immediate force mode.

We have eliminated the use of a low-level raw Lisp constant,
*most-recent-multiplicity*.  Our test suite saw a speed-up of
approximately 2% as a result for an ACL2 image built on GCL (but no
significant speed-up for an ACL2 image built on Allegro Common Lisp).
We thank Rob Sumners for suggesting this improvement.

Fixnum declarations are now realized as (signed-byte 29) instead of
(signed-byte 27).  We check that the underlying Common Lisp recognizes
objects of type (signed-byte 29) as fixnums, with the exception of
CLISP, which is said to have an efficient bignum implementation.

A new documentation topic functional-instantiation-example illustrates
functional instantiation.

A bug has been fixed in the monitoring of runes (see MONITOR).
Thanks to Dave Greve for sending an example that clearly showed the
problem.

A warning is now issued when it is detected that a :type-prescription
rule may not be as strong as it appears because it is not sufficient to
prove itself by type reasoning.

An error is caused for rules of class :meta when the function symbol IF
is among the :trigger-fns.  (IF was ignored anyhow; the point of this
change is to avoid misleading the user.)

A minor bug has been fixed in :pr, evident for example if this command
was applied to IF.

A minor hole in :set-bogus-mutual-recursion-ok did not permit the
acceptance of mutual-recursion forms that include constant function
definitions.  This has been fixed.  Thanks to Eric Smith for coming up
with a simple example illustrating the problem.

The temporary files "TMP.lisp" and "TMP1.lisp" written out by :comp are
now written to the connected book directory (see CBD).

Previously, the Allegro compiler was not eliminating tail recursion for
executable counterparts of functions, because of the way one of its
flags had been set.  As a result, calls of functions whose guards had
not been verified could run out of stack space when this was not
necessary.  This situation has been fixed.

Executable counterparts could have slow array accesses.  This has been
fixed (specifically, constants are no longer replaced with their values
in the definitions of executable counterparts).

Various improvements have been made to the documentation.  Thanks in
particular to Eric Smith for pointing out a numbers of places where
fixes were in order.

File "mcl-acl2-startup.lisp" has been updated, thanks to feedback from
Philippe Georgelin.

Inefficiencies in GCL fixnum computations were remedied for macros +f
and *f.  Thanks to Rob Sumners for pointing out this issue.

NOTE-2-6-PROOF-CHECKER    ACL2 Version  2.6 Notes on Proof-checker Changes

The proof-checker command =, when used with no arguments, now reports
which hypothesis is being used.

The output from proof-checker command type-alist has been improved.

A slight change has been made to the proof-checker for commands
promote, casesplit, equiv, and =, so that terms of the form (if x nil
y) are recognized as conjunctions, (and (not x) y).  Thanks to Pete
Manolios for suggesting that we consider such a change.

There is a new proof-checker command print-all-concs that prints all
the conclusions of the unproved goals.

A new proof-checker command, runes, has been added.  It reports the
runes that have participated in the interactive proof up to the current
point.

NOTE-2-6-PROOFS    ACL2 Version  2.6 Notes on Changes in Proof Engine

Certain optimizations are performed when converting terms to clausal
form.  For example, (< 0 1) is known to be t, (HARD-ERROR ctx str
alist) is known to be nil, and (INTEGERP n) is known to imply
(RATIONALP n).

In earlier versions of ACL2, the conversion of a term to clausal form
expanded LAMBDA applications.  That may no longer occur.  Some proofs
may slow down (or fail) because your LAMBDA-expressions are not
expanded away when you "expected" them to be.

Robert Krug found a soundness bug in our linear arithmetic package.
The bug was caused by the derivation of an equation from two
inequalities without taking adequate precautions to ensure that both
sides of the inequalities were numeric.  Robert also kindly provided a
fix which we adopted.  Thanks Robert!

We fixed a bug that could prevent the application of a metatheorem.

A bug has been fixed that had caused bogus forcing rounds (see
FORCING-ROUND).  The bug could occur when the hypothesis of a rule
was forced (see FORCE) before the prover decided to start over
and prove the original goal by induction.  Thanks to Rob Sumners for
drawing our attention to this problem.

Some low-level fixes have been made that prevent certain infinite
loops, based on reports by users.  We thank Yunja Choi, Matt Wilding,
and Pete Manolios for reporting such problems.

An obscure potential soundness hole has been fixed by redoing the way
evaluation takes place in the ACL2 loop and during theorem proving.  We
expect that users will see no difference based on this change.  (Those
interested in the details can see the long comment "Essay on Evaluation
in ACL2" in source file interface-raw.lisp.)

A small change was made in computation for a heuristic that controls
backchaining.  This will speed up proofs dramatically in a very few
cases but should have a very small impact in general.

The simplifier has been modified to avoid eliminating hypotheses of
goals that can be established by contextual (specifically, type-set)
reasoning alone.  We believe that this change will generally strengthen
ACL2's reasoning engine, although on rare occasions a lemma that
formerly was provable may require user assistance.  Thanks to Robert
Krug for suggesting this change and providing its implementation.

Case splits are now limited, by default.  This may allow some proof
attempts to provide output where previously the prover would appear to
"go out to lunch."  For a more complete discussion, including
instructions for how users can control case splitting, see
SET-CASE-SPLIT-LIMITATIONS.

A bug has been fixed in the handling of :type-prescription rules by the
bdd package.  Thanks to Rob Sumners for discovering this bug and
supplying a helpful example.

ACL2 may now use the built-in induction scheme for a function symbol
even if that function symbol is disabled.  Formerly, if a function
symbol was disabled then its induction scheme was only considered if an
explicit induction hint was supplied, other than :induct t.

We eliminated the rule-class linear-alias.  This rule class was seldom
used and complicated the linear arithmetic decision procedure in ways
that made it difficult to extend to handle some non-linear special
cases.  The only use of the rule-class that we know of was in our own
nqthm books, which were an attempt to provide an embedding of the Nqthm
logic and theorem prover into ACL2.  But that facility was also
practically never used, as far as we know.  So both linear-alias rules
and the nqthm books have been eliminated.

In earlier versions of ACL2, when the IF-form of (AND p q) was assumed
true - as when rewriting the alpha expression in (IF (AND p q) alpha
beta) - the assumption mechanism did not deduce that p and q are true,
only that their conjunction, in its IF-form, is true.  This has long
been known as a deficiency in both ACL2 and the earlier Nqthm but it
was tedious to do better when one considered the full range of IF-forms
one might encounter in the test of another IF.  Rather than code all
the cases, we just waited until clausification got rid of them.  Robert
Krug developed a pretty nice treatment of the general case and we added
it in this version.  This also involved a surprising number of changes
elsewhere in the system because the improved handling of assumptions
caused the theorem prover often to "erase" hypotheses provided by :use
hints because it could simplify them to t.  Thank you Robert!

In response to a suggestion from Robert Krug, we added mfc-ap so that
extended metafunctions can take advantage of linear arithmetic.  See
EXTENDED-METAFUNCTIONS.

There is less delay in printing goals.  In previous versions, a goal
was not printed until its subgoals were created (or the goal was
proved).  Now, the goal is printed essentially as soon as it is created.

A small technical change has been made in the function term-order, to
give priority on the function symbol count over the weighting of
constants.  So for example, while previously the term (f) preceded the
constant 2, that is no longer the case.  If this change is noticed at
all, it will probably be noticed in how so-called _permutative_ rewrite
rules are applied; see LOOP-STOPPER.  Thanks to Robert Krug for
suggesting this improvement and providing part of the implemtation.

NOTE-2-6-RULES    ACL2 Version  2.6 Notes on Changes in Rules and Constants

The following symbols have been added to the list constant
*common-lisp-specials-and-constants*: REPLACE, FILL, CHARACTER, =,
BREAK, and PRIN1.  This was done in support of ports to Allegro 6.0 and
Windows platforms (see NOTE-2-6-NEW-FUNCTIONALITY).

The list of symbols in *acl2-exports* has been modified, for example to
include show-accumulated-persistence and the legal arguments to
set-inhibit-output-lst.

Functions zp and zip are now handled slightly differently.  They are
are now disabled, but each comes with a :rewrite rule that allows their
expansion on non-variable terms, and also with a :compound-recognizer
rule that avoids the need for opening up these functions when applied
to variables.  The resulting behavior should be very similar to the
behavior of previous versions, except that case splits will be avoided
when these functions are applied to variables.

Function standard-string-alistp replaces function string-alistp.  For
further discussion, see NOTE-2-6-GUARDS.

Rules of class :rewrite whose conclusion is a term of the form (equal
lhs rhs) have always been stored in the expected way:  lhs rewrites to
rhs.  This way of storing :rewrite rules has been extended to allow =,
eq, or eql in place of equal.

Rewrite rule nth-update-nth, in source file axioms.lisp, has been
strengthened.

A new rewrite rule equal-constant-+ has been added to the book
arithmetic/equalities.  This should generally be a beneficial change,
but existing proofs involving the arithmetic books could conceivably be
affected.

Function symbol-package-name and constant *main-lisp-package-name* have
undergone small changes.  This change should rarely be noticed by users
and is discussed elsewhere; see NOTE-2-6-SYSTEM.

We mention here that proofs involving stobjs may need to be modified
because of changes in auxiliary functions generated by defstobj.
(These changes were made in support of a new resizing capability,
mentioned elsewhere in these release notes; see
NOTE-2-6-NEW-FUNCTIONALITY.

In the distributed book directory books/arithmetic/, the book
rationals-with-axioms-proved.lisp has been renamed rationals.lisp.

(ACL2(r) only) Rewrite rules realp-+, realp-*, realp-unary-, and
realp-unary-/ have been added in analogy to existing rules rationalp-+,
rationalp-*, rationalp-unary-, and rationalp-unary-/.  Thanks to Jun
Sawada for suggesting this change.

The definition of aref1 has been modified slightly.  Previously, if
*my-a* were an array then (aref1 'some-name *my-a* :header)  would
evaluate to the cdr of the header of *my-a* rather than to its default.
See ARRAYS.

Changes have been made in the ihs books, based on suggestions from Jun
Sawada, that support its use with ACL2(r) (see REAL).  The
primary change is to replace calls of rationalp with calls of
real/rationalp, which should have no effect on users of standard ACL2.

NOTE-2-6-SYSTEM    ACL2 Version  2.6 Notes on System-level Changes

We modified the tracking of skip-proofs events and the use of state
global ld-skip-proofsp in order to avoid some soundness issues.  For
example, skip-proofs events buried in locally-included books are now
tracked.  The "Essay on Skip-proofs" in source file axioms.lisp gives
several examples of dicey behavior that is no longer supported.

We fixed a problem with some of the makefiles, so that recursive
invocations of make now use the version of make specified on the
command line.

Files were fixed to help non-Unix/Linux users with book certification.
Thanks to John Cowles for finding some problems and suggesting fixes to
books/certify-numbers.lisp, books/arithmetic/certify.lsp, and
books/cowles/certify.lsp.  We thank Scott Burson for noticing and
fixing some other such problems.  Moreover, a bdd test was being
ignored entirely in Version  2.5; this problem has been fixed as well.

A minor change in system function save-acl2-in-allegro will allow this
function to continue to work in Allegro CL versions starting (someday)
with 10.0.  Thanks to Art Flatau for suggesting such a fix.

The books/case-studies/ directory has been removed.  These books are in
support of the first (1998) ACL2 workshop, and are accessible via the
ACL2 home page on the Web,
`http://www.cs.utexas.edu/users/moore/acl2/'.  Also, the books/cli-misc
directory has been renamed books/misc, and the books/nqthm directory
has been removed.

The notion of ACL2 version has been slightly modified to catch
unsoundness due to implementation dependencies.  See VERSION.
Another change to eliminate such unsoundness is that built-in symbols
now have a symbol-package-name of "COMMON-LISP"; formerly, this string
was "LISP" for ACL2 images built on GCL.  See
SYMBOL-PACKAGE-NAME.  At a low level, the (undocumented) constant
*main-lisp-package-name* is now "COMMON-LISP"; before, it was "LISP"
for GCL.

NOTE-2-6(R)    ACL2 Version  2.6(r) (November, 2001) Notes

Important changes to non-standard version:  None since Version  2.5.

Please see NOTE-2-6 for changes to Version  2.6 of ACL2.  We
hope to write more documentation for ACL2(r) in the future.

NOTE-2-7    ACL2 Version  2.7 (November, 2002) Notes

The Version_2.7 notes are divided into the subtopics below.  Here we
give only a brief summary of a few of the changes that seem most likely
to impact existing proofs.  Not included in this brief summary, but
included in the subtopics, are descriptions of improvements (including
bug fixes and new functionality) that should not get in the way of
existing proof efforts.

In particular, please see NOTE-2-7-NEW-FUNCTIONALITY for
discussion of a number of new features that you may find useful.

Acknowledgements and elaboration, as well as other changes, can be
found in the subtopics listed below.

o Bug fixes (see NOTE-2-7-BUG-FIXES):

     + Three soundness bugs were fixed.  These bugs were probably
     rarely hit, so users may well not notice these changes.

     + Certify-book now requires :skip-proofs-ok t (respectively,
     :defaxioms-okp t) if there are skip-proofs (respectively,
     defaxiom) events in the book or any included sub-books.

     + When :by hints refer to a definition, they now use the original
     body of that definition rather than the simplfied ("normalized")
     body.

     + When ld is applied to a stringp file name, it now temporarily
     sets the connected book directory (see CBD) to the
     directory of that file while evaluating forms in that file.

o New functionality (see NOTE-2-7-NEW-FUNCTIONALITY):

     + ACL2 now works harder to apply :rewrite and :linear rules with
     free variables in the hypotheses.  See
     NOTE-2-7-NEW-FUNCTIONALITY, in particular its first two
     paragraphs, for details.  Forward-chaining also does more with
     free variables.

o Changes in proof engine (see NOTE-2-7-PROOFS):

     + Some prover heuristics have changed slightly.  Among other
     consequences, this can cause subgoal hints to change.  For
     example, suppose that the Version_2.6 proof of a particular
     theorem generated "Subgoal 2" and "Subgoal 1" while Version_2.7
     only generates the second of these.  Then a subgoal hint attached
     to "Subgoal 1" in Version_2.6 would have to be attached to "Goal'"
     in Version_2.7.  (See GOAL-SPEC.)  The full topic has
     details (see NOTE-2-7-PROOFS).

o Changes in rules and definitions (see NOTE-2-7-RULES):

     + The package name of a generated variable has changed for defcong.

o Guard-related changes (see NOTE-2-7-GUARDS):

     + Guard verification formerly succeeded in a few cases where it
     should have failed.

     + Guards generated from type declarations now use functions
     signed-byte-p and unsigned-byte-p, now defined in source file
     axioms.lisp and formerly defined rather similarly under books/ihs/.

o Proof-checker changes (see NOTE-2-7-PROOF-CHECKER):

     + See the above doc topic.

o System-level changes (see NOTE-2-7-SYSTEM):

     + See the above doc topic.

o Other changes (see NOTE-2-7-OTHER):

     + A new table, invisible-fns-table, takes the place of the
     handling of invisible functions in the acl2-defaults-table,

     + The theory-invariant event has been modified so that the default
     action is an error rather than a warning.

     +  Proof output that reports destructor elimination no longer uses
     the word "generalizing".

Again, please proceed to the subtopics for more thorough release notes.

NOTE-2-7-BUG-FIXES    ACL2 Version  2.7 Notes on Bug Fixes

Francisco J. Martin-Mateos emailed us a soundness bug (!) in our
handling of functional instantiation (for example see
FUNCTIONAL-INSTANTIATION-EXAMPLE).  We are grateful for that email,
which clearly illustrated the problem.  It is included just below the
definition of push-clause in ACL2 source file prove.lisp, where we have
fixed the bug.  This bug was fixed in a re-release of Version  2.6 in
February, 2002.

Rob Sumners emailed us a soundness bug (!) in function commutative-p1,
which is used by the ACL2 bdd package.  We are grateful for his help;
his email gave a proof of nil and also pointed to the problem function.
This bug was fixed in a re-release of Version  2.6 in February, 2002.

We discovered and fixed a soundness bug illustrated by the book below,
which was certifiable in Version  2.6 and ends in a proof of nil.  The
event (verify-guards foo) should have been rejected, because foo calls a
function whose guards have not been verified, namely, bar.  However,
ACL2 did not notice the call of function bar in the body of foo because
it was looking in the simplified (normalized) body of foo rather than
in the original body of foo.  During processing of the book below, the
logical definition of zp is used before (verify-guards foo), and (zp -3)
reduces to t in the logic.  After (verify-guards foo), ACL2 simplifies
(foo -3) by going into raw Lisp, where (zp -3) is evaluated and reduces
to nil.

       (in-package "ACL2")
       (defun bar (x)
         (zp x))
       (defthm zp-false-on-negatives
         (implies (< x 0)
                  (bar x))
         :rule-classes :type-prescription)
       (defun foo (x)
         (declare (xargs :guard (rationalp x)
                         :verify-guards nil))
         (if (< x 0)
             (if (bar x) 0 1) ; simplified body reduces this line to 0
           17))
       (defthm foo-of-minus-3-is-0
         (equal (foo -3) 0)
         :rule-classes nil)
       (verify-guards foo)
       (defthm foo-of-minus-3-is-1
         (equal (foo -3) 1)
         :rule-classes nil)
       (defthm bug
         nil
         :rule-classes nil
         :hints (("Goal" :use (foo-of-minus-3-is-0 foo-of-minus-3-is-1))))

The above bug exploited the fact that zp has a different definition in
raw Lisp than in the logic for arguments that violate its guard).  The
following example caused a hard error in raw Lisp, though not a
soundness error.

       (in-package "ACL2")
       (defun bar (x)
         (cons (car x) (car x)))
       (defun foo (x)
         (declare (xargs :guard t
                         :verify-guards nil))
         (if (bar x) x nil))
       (verify-guards foo)
       (defthm bug
         (equal (foo 3) t)
         :rule-classes nil)

We have made a minor change to the notion of the _formula_ of a function
symbol, related to the change above, which however is unlikely to be
noticeable.

In order to make it harder to hit problems like the guard problem
above, we have slighly modified the raw Lisp definition of zp.

A break-rewrite command, :ancestors, was broken, but has been fixed.
Thanks to Eric Smith for bringing the problem to our attention, and to
Robert Krug for supplying the final part of the fix.

Some proof-checker commands caused errors when all goals have already
been proved.  This has been fixed.  Thanks to Matt Wilding for
reporting this bug.

Fixed a bug in :comp.  When compiling uncompiled functions with very
large definitions, ACL2 was inserted a backslash (\) character into
generated files.

Fixed the :type-alist :brr command (see BRR-COMMANDS), whose
output was difficult to read when typed after an :eval..

Fixed some clumsy handling of errors when including an uncertified
book, for example, with the error message when including an uncertified
book with a bad deftheory event.  Thanks to Eric Smith for pointing out
this problem.

Two modifications to certify-book now cause it to reflect natural
expectations with respect to soundness.  First, it now has default
values of nil instead of t for keyword arguments :skip-proofs-okp and
:defaxioms-okp.  Thanks to Robert Krug for suggesting this change and
the ACL2 seminar at the University of Texas for discussing it.  Second,
when :skip-proofs-okp (respectively, :defaxioms-okp) is nil, either
explicitly or by default, then skip-proofs commands (respectively,
defaxiom events) are disallowed inside any included books, regardless
of the keyword parameters passed to include-book.  This had not been
the case for previous versions of ACL2, regardless of the values of
:skip-proofs-okp or :defaxioms-okp passed to include-book.

Improved warnings and errors for certify-book and include-book to
mention the portcullis as a possible source of skip-proofs and
defaxioms.

ACL2 formerly caused an error when hints in a :corollary were not
well-formed.  This situation could arise as follows when certifying a
book.  A lemma FOO is proved LOCALly to the book (or, is present in a
sub-book that is included locally).  The :corollary of a subsequent
theorem, BAR, disables that rule in a hint.  When BAR is proved, this
is not a problem.  But certify-book makes a second pass after
processing the events in a book: it essentially does an include-book.
During the include-book pass, FOO is not known (because it was local),
and therefore ACL2 fails to process the disable of FOO in an in-theory
hint.  The fix is that during include-book, hints are ignored in
corollaries just as they have been for the main theorem (or definition).

It was possible for guard verification to succeed where it should have
failed.  We have fixed the bug (which was in source function (ironically
named!) fcons-term-smart).  Thanks to Robert Krug for sending us an
example of bungled guard verification.  It turns out that this bug was
also present in Version_2.6.

The proof-checker command = has been improved.  Formerly, it could fail
to apply when certain implies terms were in the context.  Thanks to
Pete Manolios for bringing this problem to our attention.

The command add-binop failed to work.  This has been fixed.  Thanks to
Rob Sumners for pointing out this problem.  Also see
NOTE-2-7-OTHER for a discussion of how this and another table are no
longer part of the acl2-defaults-table.

Book certification could cause a segmentation fault in cases where the
certification world (see CERTIFY-BOOK) has a very large number
of events.  This has been fixed.

We now allow empty :use hints and empty hints, as requested by Eric
Smith.  Examples:

     ("Goal" :use ())
     ("Goal")

A large mutual-recursion nest could cause a stack overflow when
executing either :pr FN, :pr! FN, or :monitor (:definition FN) t, where
FN is in that large mutual recursion nest.  This has been fixed
(implementation detail:  function actual-props has been made
tail-recursive).  NOTE:  If you just want the definition of FN, :pf FN
can be much faster than :pr FN if FN is in a large mutual-recursion.

Hard Lisp errors could occur when including uncertified books.  This
has been fixed; ACL2 now does syntax-checking formerly omitted when
including uncertified books.

Previously, the evaluation of defstobj and mutual-recursion forms could
cause "undefined" warnings when the form was compiled.  This has been
fixed.  Thanks to Eric Smith for bring a mutual-recursion example to our
attention.

A bug has been fixed in the syntactic check for valid :loop-stopper
values.  Formerly, valid :loop-stopper values were erroneously
restricted to lists of length at most 2 (a minor problem, since these
lists typically have length 1), and the function symbol(s) need not
have been defined in the current ACL2 world.  Thanks to Eric Smith for
sending an example to demonstrate the latter problem.

Functions definitions that are :non-executable (see XARGS) had
never been recognized as redundant, but this has been fixed.  Thanks to
Vernon Austel for pointing out this problem.

Compilation using :comp now compiles user-defined :program mode
functions.  Formerly only :logic mode functions could be compiled using
:comp.

Handling of :by hints has been improved in essentially three ways.  The
primary change is that now, when the current goal exactly matches the
supplied lemma instance, the subsumption test will always succeeds (see
HINTS, in particular the discussion of :by).  Second, certain
proof failures involving :by hints were failing silently, with duplicate
messages "As indicated by the hint, this goal is subsumed by...."  This
could happen when the original goal was among the goals generated by
applying the hint.  This problem has been fixed by no longer
considering this proof step to be specious (see
SPECIOUS-SIMPLIFICATION).  Third and finally, when the lemma-instance
refers to a definition, the original body of that definition is used
rather than the simplfied ("normalized") body.

In addition to the obove, we now recognize more cases of specious
simplification (see SPECIOUS-SIMPLIFICATION).  Thanks to Eric
Smith for bringing this issue to our attention.

Fixed building of ACL2 under CLISP so that (1) the appropriate ACL2
startup message is printed out when ACL2 starts up, and (2) the lisp
process supplied to make, e.g., LISP=/usr/bin/clisp, is the one written
out to the saved ACL2 file.  Thanks to Dave Greve and Noah Friedman for
suggesting (2).  Also, ACL2 now works with CLISP 2.30.  We have
accommodated a change in CLISP's handling of streams and its
package-locking mechanism, as well as certain non-standard characters
that formerly could cause CLISP 2.30 to break, even when those
characters are in comments.

Eliminated compiler warnings for CMU Lisp.

Fixed an incorrect error supplied when book certification proceeded so
quickly that the file write dates of the book (.lisp file) and the
corresponding compiled file are equal.  Now that error only occurs if
the compiled file has a strictly earlier write date, which probably
should never happen.

Fixed an infinite loop when executing make clean-books (and hence make
with targets that call clean-books, namely, certify-books-fresh,
regression-fresh, and regression-nonstd-fresh), which could occur when
any subdirectories of books/ are missing -- even workshops/, which is
intended to be optional.  Thanks to Pete Manolios for pointing out this
bug.

The include-book command now works properly even when filenames, or
their directories or parent directories (etc.) are links.  Thanks to
Matt Wilding for pointing out this problem.

The commands :puff :puff* have been fixed.  Formerly, there was a bug
when :puff or :puff* caused the execution of an include-book for an
absolute pathname, P, that was other than the current connected book
directory (see CBD).  When including P, any subsidiary
include-book with a relative pathname would be erroneously considered
relative to the current cbd rather than relative to the directory of P.
Thanks to Pete Manolios and Matt Wilding for pointing out this problem.

It had been possible in a "large" ACL2 image to call verify-termination
successfully on built-in function sys-call, with undesirable results.
This hole has been plugged.  Thanks to Rob Sumners for pointing out
this problem.  The new function gc$ must also stay in :program mode.

ACL2 no longer warns when certifying a book based on local functions
whose guards have not yet been verified.  Thanks to Pete Manolios for
pointing out this issue.

An occasional "slow array warning" had been possible during proofs.  The
following sequence shows how to evoke that warning in previous versions.

     (in-theory (disable binary-append))
     (in-theory (enable binary-append))
     (in-theory (disable binary-append))
     (ubt 2)
     (thm (equal (car (cons x y)) x))

(See NOTE-2-7-OTHER for a discussion of a change to compress1 in
support of this fix; however, users should not need to read that
discussion.)

The raw Lisp code for defchoose had a small bug, which was only
evidenced in CLISP implementations as far as we know.  It has been
fixed.

When ld is applied to a stringp file name, it now temporarily sets the
connected book directory (see CBD) to the directory of that
file while evaluating forms in that file.  To see the effect of this
change, imagine a subdirectory "sub" of the current directory, and
imagine executing (ld "sub/foo.lisp"), where file foo.lisp contains the
form (include-book "bar").  Presumably the intention was to consider the
file bar.lisp in the same directory, sub/, as foo.lisp.  Ld now honors
that intention, but in previous versions "bar.lisp" would have been a
reference to a file in the current directory, not in sub/.

For users of run-acl2 [perhaps there are none!]: A fix has been provided
by a Debian user via Camm Maguire so that acl2-mode anyone using that?]
will work in Xemacs, which apparently uses variable
lisp-mode-shared-map rather than shared-lisp-mode-map.

ACL2 has, for a long time (always?), had a mechanism for avoiding
re-proving constraints generated by :functional-instance lemma-instances
in :use and :by hints.  But this mechanism had not applied to defined
(as opposed to constrained) functions.  This has been fixed.  Thanks to
Francisco J. Martin-Mateos (ChesKo) for pointing out this problem by
sending a clear example.

NOTE-2-7-GUARDS    ACL2 Version  2.7 Notes on Guard-related Changes

It was possible for guard verification to succeed where it should have
failed.  See the discussion under note-2-7-bug-fixes.

There have been changes in the guards generated from type declarations
for the following cases.  Thanks to Dave Greve and Matt Wilding for
suggesting such changes.

     (type (signed-byte n) val)
     (type (unsigned-byte n) val)
     (type (integer m n) val)

The following examples illustrate the changes.

     (type (signed-byte 4) x)
     ==> [old] (AND (INTEGERP X) (<= -8 X) (<= X 7))
     ==> [new] (SIGNED-BYTE-P 4 X)

     (type (unsigned-byte 4) x)
     ==> [old] (AND (INTEGERP X) (<= 0 X) (<= X 15))
     ==> [new] (UNSIGNED-BYTE-P 4 X)

NOTE-2-7-NEW-FUNCTIONALITY    ACL2 Version  2.7 Notes on New Functionality

ACL2 now has a more powerful technique for relieving a :rewrite or
:linear rule's hypothesis that contains free variables.  A new
documentation section has been written describing the handling free
variables in rules; see FREE-VARIABLES.  In brief, the primary
change is that when a free-variable match for the current hypothesis
fails to allow subsequent hypotheses to be relieved, then additional
matches may be attempted until they have all been tried.  Also see
RULE-CLASSES (discussion of :match-free).  Also see
SET-MATCH-FREE-ERROR, see SET-MATCH-FREE-DEFAULT, and see
ADD-MATCH-FREE-OVERRIDE for interfaces provided to the user for
controlling the way ACL2 deals with free variables in hypotheses.  We
thank Rob Sumners for several helpful discussions about the designs of
those interfaces, as well as Eric Smith and Robert Krug for helpful
related discussions.  Robert Krug also found a performance bug in a
preliminary version, for which we are grateful.

WARNING: Book certification attempts may take much longer now that, by
default, ACL2 looks for more free variable matches (see paragraph just
above).  You can get the old behavior by inserting the form

     (set-match-free-default :once)

just after the initial in-package form.  However, rules from included
books that have free variables can still slow down certification.  This
can be fixed by inserting

     (add-match-free-override :once t)

before the first event in the file that generates a proof.

Forward-chaining has been made more powerful in the presence of free
variables (see FREE-VARIABLES), thanks to a contribution by
Erik Reeber.  Both before and now, when an attempt is made to relieve
(prove) a hypothesis of a :forward-chaining rule in the case that at
least one variable in that hypothesis is not yet bound, ACL2 looks in
the current context for an instance of that hypothesis.  If it finds
one, then it binds the unbound variables and continues to the next
hyopothesis.  What is new is that ACL2 can now looks for multiple
instances of that hypothesis.  Consider the following example; an
explanation is below.

     (encapsulate (((op * *) => *))
                  (local (defun op (x y) (< x y)))
                  (defthm transitivity-of-op
                    (implies (and (op x y) (op y z)) (op x z))
                    :rule-classes :forward-chaining))

     ; fails in Version_2.6; succeeds in in Version_2.7
     (thm (implies (and (op a b) (op b c) (op b e)) (op a c)))

Before Version_2.7, the proof of the thm above fails.  When the
:forward-chaining rule transitivity-of-op binds x to a and y to b, it
then looks for an instance of (op y z) in the current context, with y
bound to b but z unbound.  It happens to find (op b e) before (op b c),
and it then adds (op a e) to the context.  But starting with
Version_2.7, it continues to look for additional instances and finds
(op b c) in the context as well, chaining forward to (op a c) and thus
proving the theorem.

A new macro, bind-free, provides a simple way to get much or most of
the power of metafunctions.  Thanks to Eric Smith for coming up with the
idea and to Robert Krug for providing an implementation (which we
modified only very slightly) and documentation. See BIND-FREE
and see BIND-FREE-EXAMPLES.

With the addition of bind-free (mentioned above), syntaxp has become a
macro, although that change should be transparent to the user.  More
importantly, the argument of syntaxp may now refer to variables mfc and
state, giving syntaxp some of the power of extended metafunctions; see
SYNTAXP and see EXTENDED-METAFUNCTIONS.  Thanks to
Robert Krug for implementing that extension.  Also, the argument of
syntaxp may now include calls of :program mode functions.  See
SYNTAXP and see SYNTAXP-EXAMPLES (thanks to Robert Krug for
updating the former and creating the latter documentation).

The linear-arithmetic decision procedure (see
LINEAR-ARITHMETIC) has now been extended so that ACL2 can reason
about non-linear arithmetic as well (see NON-LINEAR-ARITHMETIC
for how to turn on this feature).  We thank Robert Krug for the initial
implementation of this, and Eric Smith for finding a couple of bugs in
it.

Some trace utilities have been made available in the ACL2 loop.

     o Function trace$ (and also untrace$) calls the corresponding
     underlying Lisp routine trace (and untrace), which however
     continues (as it has for some time) to be enhanced for GCL and
     Allegro CL.

     o Macro open-trace-file causes trace output to go to a specified
     file.  Macro close-trace-file causes trace output to go to the
     screen (which is the default).

     o Macro with-error-trace (or, wet for short) causes a backtrace to
     be written out for many failures, including guard violations.  See
     TRACE, see TRACE$, and see :DOC wet [** NOTE:
     eliminated after Version  3.3].

A new theory, minimal-theory has been provided (see THEORIES).
It can be particularly useful for speeding up proofs involving :use
hints.

New events defund and defthmd behave exactly like defun and defthm,
respectively, except that these new events disable the new name.

The new macro with-output can be used to suppress output that would
normally result from evaluation of a form.

The form (pstack) can give the user an idea of what the prover has been
up to during a proof, or after a user-aborted proof.  Moreover, by
evaluating (verbose-pstack t) (see VERBOSE-PSTACK) one can get
trace-like information about prover functions, including time
summaries, printed to the screen during a proof.  Thanks to Bill Legato
and Robert Krug for initiating this work and to Robert for providing
some initial implementation.

The new command :comp-gcl is identical in functionality, except that it
always leaves .c and .h files when compiling in GCL.  Thanks to Rob
Sumners and Vernon Austel for suggesting such a capability.

The macro e/d provides a convenient way to enable some rules and
disable others.  It was formerly in a book supplied with the
distribution, books/ihs/ihs-init.lisp, written by Bishop Brock (who we
thank for providing this useful macro).

New distributed books include those in books/ordinals/,
books/rtl/rel3/, and books/misc/simplify-defuns.lisp (which is
documented in books/misc/simplify-defuns.txt).

The :expand hint now accepts a special value, :LAMBDAS, that tells the
ACL2 rewriter to expand all lambda applications (let expressions).  See
HINTS.

A new function zpf has been added as fast test against 0 for
nonnegative fixnums.

A new macro gc$ allows the user to call the garbage collector of the
underlying Common Lisp.  Thanks to Rob Sumners for suggesting this
feature.

It is now possible to monitor simple (abbreviation) rules.  However, as
a warning explains, they are still not considered monitored during
preprocessing; see MONITOR.  Thanks to Robert Krug for
providing this improvement.

The second argument of certify-book, if supplied, formerly had to be
either t or a non-negative integer.  Now it can be the symbol ?, in the
ACL2 package, indicating that the usual check should be suppressed on
the number of commands that have been executed to create the world in
which certify-book was called.

NOTE-2-7-OTHER    ACL2 Version  2.7 Notes on Miscellaneous Changes

Made several minor documentation improvements.  We are grateful to Eric
Smith for suggesting (most of) these.

Improved (show-bdd) (see BDD) to give more useful feedback when
there are "leaf" terms not known to be Boolean.

Sped up processing of large mutual-recursion nests.  In one large
example the speedup was roughly two orders of magnitude.

Modified event printing so that if both 'prove and 'event are
inhibited, then events are no longer printed on behalf of certify-book,
encapsulate, or defstobj.  Thanks to Eric Smith for prompting
consideration of such a change.

The following technical change was made to support with-error-trace and
wet (see NOTE-2-7-NEW-FUNCTIONALITY), but may be of interest to
those who do low-level programming using the ACL2 logical world.  The
'unnormalized-body property is now stored not only for functions defined
in :logic mode, but also for functions defined by the user in :program
mode.  (:Program mode Functions built into ACL2 still have their
'unnormalized-body property omitted, in order to save space.)

The handling of "invisible" functions for purposes of controlling
rewriting (see LOOP-STOPPER) has been moved to a new table; see
INVISIBLE-FNS-TABLE.  Macros that access and modify this table
are called "...-invisible-fns-table" in place of their former names,
"...-invisible-fns-alist."  This feature was formerly implemented in
the acl2-defaults-table, which prevented a book from exporting lists of
invisible functions intended to work with the rewrite rules developed in
the book.  Thanks to Eric Smith and Rob Sumners for suggesting this
change.  See SET-INVISIBLE-FNS-TABLE (formerly
set-invisible-fns-alist), and also see ADD-INVISIBLE-FNS and
see REMOVE-INVISIBLE-FNS, which provides ways to incrementally
add to and remove from this table, respectively.  The handling of
printing binary function call nests using macros (See
ADD-BINOP) has also been moved out of the acl2-defaults-table as
suggested by Eric and Rob, but this feature didn't work anyhow (see
NOTE-2-7-BUG-FIXES).  Incidentally, the symbols binop-table,
add-binop, and remove-binop have all been added to the list
*acl2-exports* (see ACL2-USER), add-invisible-fns and
remove-invisible-fns have been added to that list, and
set-invisible-fns-alist has been replaced in that list by
set-invisible-fns-table.  Function invisible-fns-alistp is no longer
defined and has been removed from *acl2-exports*.

We now enforce the stated restriction on the pairings in
macro-aliases-table (see MACRO-ALIASES-TABLE), namely, that it
associates names of macros with names of funcions (with respect to the
current ACL2 logical world).  We make a similar requirement on
invisible-fns-table.

The theory-invariant event has been modified so that the default action
is an error rather than a warning.  Thanks to Eric Smith for suggesting
this change.  Also, the value returned upon successful execution of a
theory-invariant event is now the key.

Proof output that reports destructor elimination no longer uses the word
"generalizing".  This small change may help in browsing proof output,
since now "generaliz" takes you to true uses of generalization.  Thanks
to Matyas Sustik for suggesting such a change.

The command :pl now prints an abbreviated controller-alist for
;definition rules.  Formerly the output from :pl could be overwhelming
when the supplied function was part of a large mutual-recursion nest.

The defaults for keyword parameters of certify-book have changed.  See
NOTE-2-7-BUG-FIXES, in particular, the discussion there of two
modifications to certify-book.

Technical changes have been made to compress1 and compress2 that should
usually be invisible to users.  The next paragraph describes them in
detail, only for competeness (i.e., that description can be ignored by
most users).  But first, here is an example showing an effect on users.
The slow array warning was not there previously.  Notice that the
warning only arises if the event form is changed.  The solution is to
be sure that redundant defconst forms are syntactically identical.

     ACL2 !>(defconst *a* (compress1 'demo
                                     '((:header :dimensions (5)
                                                :maximum-length 15
                                                :default uninitialized
                                                :name demo)
                                       (1 . one)
                                       (0 . zero))))

     Summary
     Form:  ( DEFCONST *A* ...)
     Rules: NIL
     Warnings:  None
     Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
      *A*
     ACL2 !>(aref1 'demo *a* 0)
     ZERO
     ACL2 !>(defconst *a* (compress1 'demo
                                     '((:header :dimensions (5)
                                                :maximum-length 15
                                                :default uninitialized
                                                :name demo)
                                       (1 . one)
                                       (0 . zero))))

     This event is redundant.  See :DOC redundant-events.

     Summary
     Form:  ( DEFCONST *A* ...)
     Rules: NIL
     Warnings:  None
     Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
      :REDUNDANT
     ACL2 !>(aref1 'demo *a* 0)
     ZERO
     ACL2 !>(defconst *a* (compress1 'demo
                                     '((:header :dimensions (5)
                                                :maximum-length 15
                                                :default uninitialized
                                                :name demo)
                                       (0 . zero)
                                       (1 . one))))

     This event is redundant.  See :DOC redundant-events.

     Summary
     Form:  ( DEFCONST *A* ...)
     Rules: NIL
     Warnings:  None
     Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
      :REDUNDANT
     ACL2 !>(aref1 'demo *a* 0)

     **********************************************************
     Slow Array Access!  A call of AREF1 on an array named
     DEMO is being executed slowly.  See :DOC slow-array-warning
     **********************************************************

     ZERO
     ACL2 !>

As before, the von Neumann structure stored in the 'acl2-array property
of the array name contains the array list object in its car.  However,
previously it was the case that compress1 and compress2 did not update
that car when its new value would be equal to its old value.  This was
done largely in support of some type-set tables defined using defconst
in type-set-b.lisp.  The new versions of compress1 and compress2 are
simpler in that no such exception is made in the case of equal lists,
although instead the entire compression process is short-circuited when
the input array list object is eq to the car of the 'acl2-array
property.  This change was made because the equality test was causing a
"slow array access" warning to be printed in rare cases during proofs,
as described elswhere (see NOTE-2-7-BUG-FIXES).

We no longer distribute documentation specific to Lucid Emacs.  The Info
documentation in directory doc/EMACS/ works well both for Gnu Emacs and
XEmacs.

A little-advertised macro, value, has long been allowed for top-level
forms in books; see EMBEDDED-EVENT-FORM.  This has been
replaced by a new macro, value-triple.  The two have the same semantics
at the top-level of books, where state is "live".  However, value-triple
should be used at the top-level of a book, while value should be used in
function definitions (as before).  This change eliminates a warning put
out by the Allegro Common Lisp compiler for top-level value forms in
books.

NOTE-2-7-PROOF-CHECKER    ACL2 Version  2.7 Notes on Proof-checker Changes

Output from the proof-checker can now be inhibited by supplying the
symbol proof-checker in the list given to set-inhibit-output-lst.

NOTE-2-7-PROOFS    ACL2 Version  2.7 Notes on Changes in Proof Engine

An improvement in the linear arithmetic heuristics has been provided by
Robert Krug.  For information about this change, search for the comment
in add-linear-lemma (file rewrite.lisp) that begins as follows.

     ; Previous to Version_2.7, we just went ahead and used the result of

Thanks, Robert!  Also thanks to Eric Smith for providing a motivating
example.

The non-linear-arithmetic addition (see NON-LINEAR-ARITHMETIC)
led to several small changes in the linear-arithmetic decision procedure
(see LINEAR-ARITHMETIC).  Two of these changes could affect
existing proofs.

     First, when we are setting up the initial arithmetic data-base
     (which we call the "pot-lst"), we have always scanned it to see if
     there were any pairs of inequalities from which we could derive a
     previously unknown equality.  In some cases we added this equality
     to the clause and in others we used it to rewrite the clause,
     substituting one side of the equality for the other throughout the
     clause.  Previously, the heuristics that we used to determine
     whether we performed the substitution differed from those used in
     several other places in the code.  This has now been regularized,
     and similar heuristics are now used throughout the code.

     The second change to the linear-arithmetic decision procedure is
     that we now explicitly add inequalities derived from type reasoning
     to the pot-lst.  Previously, we performed cancellations against
     these inequalities without adding them to the pot-lst.  This
     change results in there being more inequalities in the pot-lst
     than before, and so more chances for there to be a pair of
     inequalities from which an equality can be derived.  In effect,
     certain simple consequences of the current goal (see
     TYPE-SET) may now be added as hypotheses of the goal or used to
     peform equality substitutions.

A slight improvement has been made to the way certain rewrite rules are
stored.  It was already the case that a rewrite rule rule whose
conclusion C is not a call of a known equivalence relation (or eq, eql,
or =) is stored as (iff C t), except that if ACL2 can determine (using
its type-set mechanism) that C is Boolean, then the rule is stored as
(equal C t).  The iprovement is that if C and C' are Boolean, then a
rule stated as (iff C C') is stored as (equal C C').  Thanks to Pete
Manolios for providing an example that led us to consider this
improvement.

The heuristic use of equalities (fertilization) has been modified.
Previously, ACL2 would sometimes substitute using an equality but keep
the equality, and then undo the substitution by using the equality
again.  Now, when ACL2 keeps an equality after using it, it puts the
equality inside a call of hide.  Descendents of that goal that are
unchanged by simplification will have this call of hide removed so that
the equality can once again contribute to the proof.  This change can
cause some proofs to succeed that otherwise would fail.  In the
unlikely event that a proof fails that formerly succeeded, the
following hint on "Goal" may fix the problem (see HINTS):

     :expand ((:free (x) (hide x)))

We have refined the heuristics employed when an IF form is assumed true
or false.  Our previous attempt (see note-2-6-proofs for the original
announcement) was not as general as we had believed.  We have also
improved some low-level code responsible for rewriting IF expressions.
In earlier versions of ACL2, it was possible to have the truth or
falsity of an IF expression explicitly recorded in the type-alist, and
yet not use this information during rewriting.  This problem has been
corrected.  Thanks to Robert Krug for noticing this problem and
implementing the fix.

We have sped up the rewriter in some cases where there are large
collections of mutually-recursive functions (see
MUTUAL-RECURSION).  (Implementation notes: technically, we have
modified the way function being-openedp operates on the fnstack, and we
have modified *current-acl2-world-key-ordering* as described in the
essay above its definition.)

Forward-chaining is now done in the preprocessing phase of proof
attempts (see the discussion of :DO-NOT -- see HINTS).  This is
part of a technical change, made in support of translation of type
declarations to guards (see NOTE-2-7-GUARDS).  Previously,
whenever ACL2 checked for built-in-clauses, it then looked for a
contradiction using type-set reasoning if it did not find a suitable
built-in clause.  The change is to perform forward-chaining in such
cases (i.e., when a built-in clause is not found).

A couple of changes have been made in the generation of goals for
forcing-rounds.  Thanks to Eric Smith for bringing issues to our
attention that led to these changes.  For one, guards are no longer
relevant in such goal generation.  Formerly, the addition of a guard
could make a proof fail that otherwise succeeded.  Secondly, contextual
information is now always kept when it involves a constrained constant,
i.e., a zero-ary function introduced in the signature of an encapsulate.

NOTE-2-7-RULES    ACL2 Version  2.7 Notes on Changes in Rules and Constants

The defcong macro has been slightly changed.  The difference is that
the variable generated with suffix -EQUIV will now be in the same
package as the name of the variable from which it is generated, rather
than always belonging to the ACL2 package.  Thanks to Hanbing Liu for
suggesting this change.  (Note that a couple of books have been
modified to accommodate this change, e.g.,
books/finite-set-theory/set-theory.)

In Version_2.6, a change was made for rules of class :rewrite whose
conclusion is a term of the form (EQV lhs rhs), where EQV is =, eq, or
eql: the rule was stored as though EQV were equal.  (See
NOTE-2-6-RULES.)  This change has been extended to rules of class
:definition.

NOTE-2-7-SYSTEM    ACL2 Version  2.7 Notes on System-level Changes

ACL2 now runs (once again) under Lispworks, specifically, Lispworks
4.2.0.  However, we needed a patch, which presumably will be
unnecessary after 4.2.7.  From Lispworks support:

     Users with LispWorks4.2.7 should ask us at lisp-support@xanalys.com
     for the transform-if-node patch. It will be helpful if they quote
     (Lisp Support Call #11372) when doing so. Also, they must send a
     bug form generated from their LispWorks image: instructions at
     http://www.lispworks.com/support/bug-report.html.

File books/Makefile-generic has been improved so that failed attempts to
certify a book will cause the make to fail.  Previously, an existing
.cert file was left in place, and that sufficed for the make to be
considered a success.  Now, the old .cert file is first removed when
recertification is found to be necessary.

A change has been made to source file acl2.lisp to accommodate GCL
2.4.3.  (ACL2 Version  2.6 does not work with some versions of GCL
2.4.3.)

The error message has been improved when certain forms are typed to raw
Lisp and the ACL2 loop has never been entered (with (LP)).

The following symbols in the ACL2 package have been made untouchable,
meaning that they are not available to the user: ev-fncall, ev, ev-lst,
ev-acl2-unwind-protect, ev-fncall!, and user-stobj-alist-safe.  The
reason is that these functions can not be called safely except under
certain restrictions.  If you want to call the ACL2 evaluator, consider
using the built-in system functions trans-eval or
simple-translate-and-eval.

CLISP Version_2.30 implements a notion of "locking" the "LISP" package
that is incompatible with building ACL2.  (CLISP Version_2.27 does not
appear to have had this feature.)  We have gotten around this problem
by unlocking the "LISP" package in ACL2 images built on such CLISPs.

Automatic proclaiming for GCL, which has (for a long time) been done for
functions in compiled books, has been improved.  Formerly, the only
time a non-trivial output type (i.e., other than t) was inferred was
when macroexpansion produced an explicit call of the.  Now, if
expressions can also generate non-t output types.  Consider the
following example.

     (defmacro the-fixnum (n)
       (list 'the '(signed-byte 29) n))
     (defmacro 1+f (x)
       (list 'the-fixnum
             (list '1+ (list 'the-fixnum x))))
     (defun foo (x)
       (declare (type (unsigned-byte 27) x))
       (if (zp x)
           0
         (1+f (foo (1-f x)))))

Formerly, the proclaim forms for foo, before and after this
improvement, are as shown below.

     (PROCLAIM '(FTYPE (FUNCTION ((UNSIGNED-BYTE 27)) T) FOO))                ;old
     (PROCLAIM '(FTYPE (FUNCTION ((UNSIGNED-BYTE 27)) (SIGNED-BYTE 29)) FOO)) ;new

Compiler info messages sent to error stream were eliminated for CMUCL.

NOTE-2-7(R)    ACL2 Version  2.7(r) (November, 2002) Notes

In source file axioms.lisp, in order for proofs to succeed, (make
proofs), the definitions of acl2-count and explode-atom have been
modified slightly, and lemma standard-numberp-one [modified after
Version_3.4 to become standardp-one] has been given :rule-classes nil.

All skip-proofs forms have been eliminated from the nonstd books, thanks
to Ruben Gamboa.

The directory books/sqrt/, which was intended for ACL2(r), has been
moved to books/nonstd/sqrt/ and added as appropriate to
books/nonstd/Makefile.

Please see NOTE-2-7 for changes to Version_2.7 of ACL2.

NOTE-2-8    ACL2 Version  2.8 (March, 2004) Notes

BRIEF SUMMARY.

The Version_2.8 notes are divided into the indicated subtopics.  Here
we give only a brief summary of just a few of the major new features
and changes that seem most likely to impact existing proofs.  Not
included in this brief summary, but included in the subtopics, are
descriptions of many improvements (including bug fixes and new
functionality) that should not get in the way of existing proof
efforts.  In the description below we also omit discussion of changes
that will become clear by way of error messages if they affect you.

In particular, please see NOTE-2-8-NEW-FUNCTIONALITY for
discussion of a number of new features that you may find useful.

Acknowledgements and elaboration, as well as other changes, can be
found in the subtopics listed below.

o Some of the bug fixes (see NOTE-2-8-BUG-FIXES):

     + Some soundness bugs were fixed.

     + The handling of free variables in hypotheses (see
     FREE-VARIABLES) of rewrite and linear rules had a bug that
     prevented some proofs from going through.  Now that this bug has
     been fixed, you may find some proofs running much more slowly than
     before.  You can use accumulated-persistence and
     add-match-free-override to remedy this situation; see
     NOTE-2-8-BUG-FIXES for details.

     + The default-hints in the current logical world are no longer
     ignored by verify-guards.

     + Forms violating guard-checking such as (defconst *silly* (car
     3)) are now allowed in books.

o Some of the new functionality (see
NOTE-2-8-NEW-FUNCTIONALITY):

     + WARNING: You may find that control-d (in emacs, control-c
     control-d) can throw you completely out of Lisp where it had not
     formerly done so.

     + ACL2 now starts up inside the ACL2 loop -- that is, (LP) is
     executed automatically -- when built on CLISP or Allegro CL.  This
     was already the case for GCL and CMUCL, and it still is not true
     for Lispworks.

     + See NOTE-2-8-ORDINALS for a discussion of a significant
     change in ordinal represtation, and in particular, for how to
     preserve existing proofs that depend on the previous ordinal
     representation.

     + Macros mbe ("must be equal"), mbt ("must be true"), and defexec
     have been introduced, which allow the user to attach alternate
     executable definitions to functions.

     + The user can now control multiple matching for free variables in
     hypotheses for :forward-chaining rules, as has already been
     supported for :rewrite and :linear rules.

     + It is no longer necessary to specify (set-match-free-error nil)
     in order to avoid errors when a rule with free variables in its
     hypotheses is missing the :match-free field.

     + The form (break-on-error) causes, at least for most Lisps, entry
     into the Lisp debugger whenever ACL2 causes an error.

     + A new table has been provided so that advanced users can
     override the built-in untranslate functionality.  See
     USER-DEFINED-FUNCTIONS-TABLE.

     + The pstack (`process [prover] stack") mechanism, formerly denoted
     checkpoints, has been improved.  One of these improvements is to
     show actual parameters with (pstack t) rather than formals.

     + The defstobj event is now allowed to take an :inline argument,
     which can speed up execution.

     + Macro cw-gstack no longer takes arguments for the gstack or
     state.  To print terms in full rather than abbreviated: (cw-gstack
     :evisc-tuple nil).

     + The include-book event now has an additional (optional) keyword,
     :dir.  In particular, (include-book "foo/bar" :dir :system) will
     include the indicated book after prepending the path of the
     built-in books/ directory.  You will probably not find :dir
     :system to be useful if you move the executable image or
     distributed books; see INCLUDE-BOOK, in particular its
     "soundness warning".

     + The printing of results in raw mode (see SET-RAW-MODE)
     may now be partially controlled by the user:  see
     ADD-RAW-ARITY.

     + For those using Unix/Linux make:  A cert.acl2 file can contain
     forms to be evaluated before an appropriate certify-book command is
     invoked automatically (not included in cert.acl2).

o Some of the changes in the proof engine (see NOTE-2-8-PROOFS):

     + ACL2 now prevents certain rewriting loops; see
     REWRITE-STACK-LIMIT.

     + Small changes have been made to heuristics for controlling
     rewriting during proofs by induction and in handling certain
     "weak" compound-recognizer rules.

     + The handling of free variables in a hypothesis of a rewrite rule
     (see FREE-VARIABLES) has been improved in the case that
     the hypothesis is of the form (equiv x y), where equiv is a known
     equivalence relation (see EQUIVALENCE).

     + We have modified how the ACL2 simplifier handles the application
     of a defined function symbol to constant arguments, by avoiding
     the introduction of hide when evaluation fails if the term can be
     rewritten.

     + The generation of "Goal" for recursive (and mutually-recursive)
     definitions now uses the subsumption/replacement limitation
     (default 500).  See CASE-SPLIT-LIMITATIONS.

     + Default hints now apply to hints given in definitions, not just
     theorems.  See DEFAULT-HINTS.

     + Linear arithmetic now uses the conclusions of forward-chaining
     rules, and type-set now uses a small amount of linear reasoning
     when deciding inequalities.

o Some of the changes in rules, definitions, and constants (see
NOTE-2-8-RULES):

     + See the above doc topic.

o Guard-related changes are described in see NOTE-2-8-BUG-FIXES.

o Some of the proof-checker changes (see
NOTE-2-8-PROOF-CHECKER):

     + Added new proof-checker commands wrap1, wrap, and wrap-induct,
     to combine multiple conjuncts or goals.

     + The type-alist command now takes optional arguments that control
     whether or not the governors and/or conclusion are used in
     computing the context.

o Some of the system-level changes (see NOTE-2-8-SYSTEM):

     + ACL2 now runs on OpenMCL and on MCL 5.0.

o Some of the other changes (see NOTE-2-8-OTHER):

     + Emacs file emacs/emacs-acl2.el has been updated (see
     NOTE-2-8-OTHER for details).

     + When :pl is given a term other than a symbol, it will print all
     rewrite rules that match that term.

     + A new function, pkg-witness, returns a symbol in the given
     package.

     + The list constant *acl2-exports* has been extended.

     + A new release of the rtl library has been included:
     books/rtl/rel4/.  See the README file in that directory.

Again, please proceed to the subtopics for more thorough release notes.