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

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

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

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

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

NOTE-3-2-1    ACL2 Version  3.2.1 (June, 2007) Notes

NOTE!  New users can ignore these release notes, because the
documentation has been updated to reflect all changes that are recorded
here.

(OpenMCL and multi-threaded SBCL only) Fixed a soundness bug in the
evaluation of mbe forms in the presence of Lisp feature
:acl2-mv-as-values.  Thanks to Sol Swords for reporting this problem and
sending a simple proof of nil (which can be found in a comment in the
ACL2 sources, in (deflabel note-3-2-1 ...)).

Added a new utility, dmr (Dynamicaly Monitor Rewrites), for watching
the activity of the rewriter and some other proof processes.  See
DMR.  We thank Robert Krug for useful contributions.

Fixed a bug in evaluation of calls of with-prover-time-limit.

Fixed the writing of executable scripts when building ACL2, so that the
build-time value of environment variable ACL2_SYSTEM_BOOKS is no longer
written there.  Thanks to Dave Greve for discussing this change.

Fixed bugs in :pl (which are similarly present in the proof-checker's
sr (show-rewrites) command.  The first bug was evident from the
following forms sent by Robert Krug, which caused an error.

     (include-book "arithmetic-3/floor-mod/floor-mod" :dir :system)
     :pl (mod (+ 1 x) n)

The second bug was due to a failure to take note of which rules are
disabled, and could be seen by executing the following (very slow!).

     (defstub modulus () t)
     (include-book "arithmetic-3/floor-mod/floor-mod" :dir :system)
     :pl (mod (+ x y) (modulus))

Modified certify-book so that by default, all executable-counterpart
functions (sometimes called "*1* functions") are compiled.  This is the
behavior that was already supported with a compile-flg argument of
:all; the change is that argument t now has this behavior as well (and
:all is supported only for legacy purposes).  A new value for
compile-flg, :raw, gives the behavior formerly produced by value t,
namely where executable-counterpart functions are not compiled.  The
above changes are irrelevant if compilation is suppressed; see
COMPILATION.  Finally, if environment variable ACL2_COMPILE_FLG is
set, then after converting to upper-case this environment variable's
value of "T", "NIL", or ":RAW" will determine the value of the optional
compile-flg argument to be t, nil, or :raw, respectively, when this
argument is not explicitly supplied.

Modified include-book so that :comp argument now acts like :comp!,
i.e., compiling a file that includes the file together with all
executable counterpart (so-called "*1*") functions.  A new argument,
:comp-raw, has the behavior that :comp had formerly, i.e., compiling
the actual book only.

The function nonnegative-integer-quotient is now computed in raw Lisp
by calling floor on its arguments.  This change was suggested by Peter
Dillinger, in order to avoid stack overflows such as reported by Daron
Vroon.  A new book, books/misc/misc2/misc.lisp, contains a proof of
equivalence of nonnegative-integer-quotient and floor, and serves as a
repository for other miscellaeous proofs, including those justifying
ACL2 modifications such as this one.

Enhanced accumulated-persistence to break down results by useful vs.
useless rule applications.  In particular, this provides information
about which rules were ever applied successfully, as requested by Bill
Young.

Added coverage of :meta rules to the accumulated-persistence statistics.

Fixed a bug that was causing a :clause-processor hint to fire on a
subgoal of the goal to which it was attached, when the original
application didn't change the clause.  Thanks to Dave Greve for
pointing out this bug and providing a useful example.

Fixed a bug in handling of computed hints related to the
stable-under-simplificationp parameter (see COMPUTED-HINTS).
There were actually two bugs.  A minor but confusing bug was that the
same goal was printed twice upon application of such a hint.  The major
bug was that :use hints (as well as other "top" hints: :by, :cases, and
:clause-processor) were not being applied properly.  Thanks to Jared
Davis for sending an example some time ago that showed the duplicate
printing, and to Dave Greve for sending an example showing
mis-application of :clause-processor hints.  Note that you may find
that existing computed hints using the stable-under-simplificationp
parameter no longer have the same behavior; see a comment about
computed hints in note-3-2-1, ACL2 source file ld.lisp, for an example
of how you might want to fix such computed hints.

David Russinoff has contributed an updated version of
books/quadratic-reciprocity/ including minor modifications of the
treatment of prime numbers and a proof that there exist infinitely many
primes.  Thanks to David for contributing this work, and to Jose Luis
Ruiz-Reina for posing the challenge.

Reduced the sizes of some certificate (.cert) files by relaxing the
test that allows original defpkg events to be placed there, rather than
evaluating the import list term into an explicit list of symbols.

Improved execution efficiency slightly for function rcdp in file
books/misc/records.lisp, by using mbe to introduce a tail-recursive
body.

The executable script generated by save-exec (and by the normal build
process) now includes a time stamp as a comment.  Thanks to Jared Davis
for suggesting this change in order to support his use of omake.  In the
process, we also arranged that the startup banner for an executable
created by save-exec shows all of the build (save) times, not just the
one for the original image.

Sped up most redundant defpkg events by avoiding evaluation and sorting
of the imports list in the case of identical event forms.  And, for
defpkg events that are not redundant, sped up their processing in
Allegro CL (and perhaps other Lisps, but apparently not GCL) by using
our own import function.

Modified add-include-book-dir so that it refuses to associate a keyword
with a different directory string than one it is already bound to.  See
DELETE-INCLUDE-BOOK-DIR for how to remove the existing binding
first.  Thanks to Robert Krug for pointing out that without this
change, one can find it difficult to debug a failure due to rebinding a
keyword with add-include-book-dir.

Added a new value for the :do-not-induct hint (see HINTS),
:otf-flg-override, which causes ACL2 to ignore the :otf-flg when
considering whether to abort the proof because of a :do-not-induct
hint.  Thanks to Daron Vroon for suggesting such an addition.

Modified the printing of messages for entering and exiting raw mode
(see SET-RAW-MODE), so that in particular they are inhibited
during include-book or whenever observations are inhibited (see
SET-INHIBIT-OUTPUT-LST).  Thanks to Peter Dillinger for suggesting
such a change.

(For system hackers only.)  The handling of events of the form (progn!
(state-global-let* ...)) had a bug that was causing bindings to be
evaluated twice.  Moreover, the use of system function
state-global-let* is suspect in raw Lisp.  We have eliminated special
treatment of state-global-let* by progn! in favor of a new keyword
argument, state-global-bindings, that provides the intended
functionality.  See PROGN!.  Moreover, special handling that
allowed make-event forms under state-global-let* has been removed; the
desired effect can be obtained using (progn! :state-global-bindings
...).  Thanks to Peter Dillinger for pointing out the above bug and
collaborating on these changes.

Incorporated backward-compatible enhancements to
books/misc/expander.lisp from Daron Vroon (documented near the top of
that file).

The specification of :backchain-limit-lst had required that only a
single (:rewrite, :linear, or :meta) rule be generated.  We have
weakened this restriction to allow more than one rule provided that
each rule has the same list of hypotheses.  For example, the rule class
(:rewrite :backchain-limit-lst 1) is now legal for the corollary
formula (implies (f x) (and (g x) (h x))), where this was not formerly
the case.  Thanks to Dave Greve for bringing this issue to our
attention.

NOTE-3-2-1(R)    ACL2 Version  3.2.1(r) (June, 2007) Notes

Please also see NOTE-3-2-1 for changes to Version  3.2.1 of
ACL2.

NOTE-3-3    ACL2 Version  3.3 (November, 2007) Notes

NOTE!  New users can ignore these release notes, because the
documentation has been updated to reflect all changes that are recorded
here.

Below we roughly organize the changes since Version  3.2.1 into new
features, bug fixes, prover algorithm enhancements, and miscellaneous.
Also see NOTE-3-2-1 for other changes since Version  3.2.

*NEW FEATURES*

A new "gag-mode" provides less verbose, more helpful feedback from the
theorem prover, in support of The Method (see THE-METHOD).  See
SET-GAG-MODE.  We recommend the use of gag-mode, which may
become the default in future ACL2 releases, and we welcome suggestions
for improvement.  We thank Robert Krug and Sandip Ray for helpful
feedback in the design of gag-mode.  Note that when proofs fail, then
even without gag-mode and even if proof output is inhibited, the
summary will contain a useful listing of so-called "key checkpoints"
(see SET-GAG-MODE).

Added support for a leading `~' in filenames.  Thanks to Bob Boyer for
suggesting this enhancement.  Note that since `~/' depends on the user,
it is disallowed in books to be certified (see CERTIFY-BOOK),
since otherwise an include-book form in a book, b, could have a
different meaning at certification time than at the time include-book
is later executed on book b.

Made a change to allow (time$ FORM) and (with-prover-time-limit TIME
FORM) when FORM includes make-event calls that change the ACL2 world.
Thanks to Jared Davis for requesting such support for time$.

Computed hints (see COMPUTED-HINTS) may now produce a so-called
"error triple", i.e., a result of the form (mv erp val state), where a
non-nil erp causes an error, and otherwise val is the value of the
hint.  It remains legal for a computed hint to return a single ordinary
value; indeed, the symbol form of a computed hint must still be a
function that returns an ordinary single value.

New hints provide additional control of the theorem prover, as follows.
See HINTS for more details, and see new distributed book
directory books/hints/ for examples, in particular file
basic-tests.lisp in that directory for simple examples.

     o The hint :OR (hints-1 ... hints-k) causes an attempt to prove the
     specified goal using each hints-i in turn, until the first of these
     succeeds.  If none succeeds, then the prover proceeds after
     heuristically choosing the "best" result, taking into account the
     goals pushed in each case for proof by induction.

     o A custom hint is a keyword that the user associates with a
     corresponding hint-generating function by invoking
     add-custom-keyword-hint.  Thus, a custom hint may be viewed as a
     convenient sort of computed hint.

     o A custom hint, :MERGE, is implemented in distributed book
     books/hints/merge.lisp.  It is useful for combining hints.

     o A sophisticated yet useful custom hint is the :CONSIDER hint
     implemented in distributed book books/hints/consider-hint.lisp.
     With this hint, you can for example give the equivalent of a :USE
     hint without the need to supply an instantiation.  Include that
     book in order to see documentation online with :doc consideration,
     and see the book books/hints/consider-hint-tests.lisp for examples.

A new hint, :reorder, allows the specification of which subgoals are to
be considered first.  Thanks to Sandip Ray for putting forward this
idea.

Enhanced set-saved-output by supporting a second argument of :same,
which avoids changing which output is inhibited.

Added macros thm? and not-thm? to distributed book
books/make-event/eval.lisp, so that it's easy to test within a certified
book that a proof attempt succeeds or that it fails.

Added printing function cw!, which is analogous to cw just as fmt! is
to fmt, i.e., printing so that the result can be read back in.  Thanks
to Jared Davis for suggesting this enhancement (after doing his own
implementation).

The ACL2 customization file can now be specified using environment
variable ACL2-CUSTOMIZATION.  See ACL2-CUSTOMIZATION.  Thanks
to Peter Dillinger for requesting this feature.

Added new emacs capabilities for proof trees (all documented in emacs):

     o New function start-proof-tree-noninteractive, for example
     (start-proof-tree-noninteractive "*shell*")

     o C-z o      Switch to another frame

     o C-z b      Switch to prooftree buffer

     o C-z B      Switch to prooftree buffer in "prooftree-frame" frame

Added Common Lisp function, search, as a macro in logic mode, with
limited support for keyword arguments.  Thanks to Warren Hunt for
requesting this addition.

Sandip Ray has contributed a book, books/make-event/defrefine.lisp, that
provides a collection of macros to aid in reasoning about ACL2
functions via refinement.

Wrote and incorporated new utility for listing all the theorems in an
included book.  See books/misc/book-thms.lisp.  Thanks to Jared Davis
for requesting this functionality.

The new distributed book misc/defp.lisp generalizes the defpun macro to
allow more general forms of tail recursion.

(Low-level printing improvement) A new function,
set-ppr-flat-right-margin, allows the right margin for certain kinds of
"flat" printing to exceed column 40.  Thanks to Jared Davis for pointing
out that state global variables 'fmt-hard-right-margin and
'fmt-soft-right-margin are not alone sufficient to extend the right
margin in all cases.

The event add-include-book-dir can now take a relative pathname as an
argument.  Formerly, it required an absolute pathname.

A new book, books/misc/defopener.lisp, provides a utility creating a
theorem that equates a term with its simplification.

ACL2 now provides limited support for the Common Lisp primitive FLET,
which supports local function bindings.  See FLET.  Thanks to
Warren Hunt for requesting this feature.

Added a definition of boole$, a close analogue of Common Lisp function
boole.  Thanks to Bob Boyer for providing an initial implementation.

*BUG FIXES*

Fixed defstobj to inhibit a potentially useless theory warning.

Fixed a bug in the application of certify-book to relative pathnames
for files in other than the current directory.  Thanks to Amr Helmy for
bringing this bug to our attention.

Fixed a bug in :pl and :pr for displaying rules of class :meta.  Thanks
to Jared Davis for finding this bug and providing a fix.

Formerly, set-default-backchain-limit was not a legal event form for
encapsulate forms and books.  This has been fixed.  Thanks to Robert
Krug and Sandip Ray for bringing this bug to our attention.

Fixed the handling of hints in proof-checker commands for the prover,
such as bash -- see PROOF-CHECKER-COMMANDS -- so that the user
can override the default settings of hints, in particular of :do-not
and :do-not-induct hints attached to "Goal".  This fix also applies to
the distributed book misc/bash.lisp, where Robert Krug noticed that he
got an error with :hints (("Goal" :do-not '(preprocess))); we thank
Robert for pointing out this problem.

Fixed a bug in handling of stobjs occurring in guards of functions whose
guards have been verified.  In such cases, a raw Lisp error was possible
when proving theorems about non-"live" stobjs.  We thank Daron Vroon
for sending us an example that highlighted this bug.  The following
(simpler) example causes such an error in previous versions of ACL2.

     (defstobj st fld)
     (defun foo (st)
       (declare (xargs :stobjs st :guard (fld st)))
       st)
     (thm (equal (foo '(3))
                 '(3)))

The dmr feature for dynamic monitoring of rewrites had a bug, where the
file used for communicating with emacs was the same for all users,
based on who built the ACL2 executable image.  This has been fixed.
Thanks to Robert Krug for bringing this bug to our attention.

Fixed a bug in some warnings, in particular the warning for including an
uncertified book, that was giving an incorrect warning summary string.

Inclusion of uncertified books erroneously re-used make-event
expansions that were stored in stale certificates.  This is no longer
the case.  Thanks to Jared Davis for bringing this bug to our attention.

Fixed a bug that was disallowing calls of with-output in events that
were executing before calling certify-book.

Modified the functionality of binop-table so other than binary function
symbols are properly supported (hence with no action based on
right-associated arguments).  See ADD-BINOP.

Fixed small proof-checker issues related to packages.  Emacs commands
ctrl-t d and ctrl-t ctrl-d now work properly with colon (`:') and
certain other punctuation characters.  The p-top command now prints
"***" regardless of the current package.

Fixed a bug that allowed certify-book to succeed without specifying
value t for keyword argument :skip-proofs-okp, even with include-book
events in the certification world depending on events executed under
skip-proofs.

Improved show-accumulated-persistence in the following two ways.
Thanks to Robert Krug and Bill Young for requesting these improvements
and for providing useful feedback.

     o It can provide more complete information when aborting a proof.

     o The :frames reported for a rule are categorized as "useful" and
     "useless" according to whether they support "useful" or "useless"
     :tries of that rule, respectively.  See
     ACCUMULATED-PERSISTENCE for further explanation.

Modified make-event so that the reported time and warnings include
those from the expansion phase.  In analogy with encapsulate and progn,
the rules reported still do not include those from subsidiary events
(including the expansion phase).  A related change to ld avoids
resetting summary information (time, warnings) with each top-level form
evaluation; events already handle this information themselves.

Fixed set-inhibit-output-lst so that all warnings are inhibited when
warning! but not warning is included in the list.  Formerly, only
soundness-related warnings were inhibited in this case.  Thanks to Eric
Smith for bringing this bug to our attention.

Distributed directory doc/HTML/ now again includes installation
instructions (which was missing in Version_3.2.1), in
doc/HTML/installation/installation.html.

Some fixes have been made for proof-tree support.

     o Proof-tree output is no longer inhibited automatically during
     certify-book, though it continues to be inhibited by default (i.e.,
     ACL2 continues to start up as though set-inhibit-output-lst has
     been called with argument '(proof-tree)).

     o Fixed a bug in Xemacs support for proof-tree help keys C-z h and
     C-z ?.

     o Fixed a bug in proof-trees that was failing to deal with the
     case that a goal pushed for proof by induction is subsumed by such
     a goal to be proved later.  Now, the proof-tree display regards
     such subsumed goals as proved, as is reported in the theorem
     prover's output.

Fixed a bug that was disallowing value-triple forms inside encapsulate
forms in a certification world (see PORTCULLIS).

If the :load-compiled-file argument of a call of include-book is :comp,
then an existing compiled file will be loaded, provided it is more
recent than the corresponding book (i.e., .lisp file).  A bug was
causing the compiled file to be deleted and then reconstructed in the
case of :comp, where this behavior was intended only for :comp!.

Fixed a bug that was avoiding compilation of some executable
counterparts (sometimes called "*1* functions") during certify-book,
and also during include-book with :load-compiled-file value of :comp or
:comp!).  Thanks to Eric Smith for sending a small example to bring this
bug to our attention.

Incorporated a fix from Eric Smith for a typo (source function
ancestors-check1) that could cause hard Lisp errors.  Thanks, Eric!

Fixed the following issues with packages and book certificates.  See
HIDDEN-DEATH-PACKAGE if you are generally interested in such
issues, and for associated examples, see comments on "Fixed the
following issues with packages" in note-3-3 in the ACL2 source code.

     o Reduced the size of .cert files by eliminating some unnecessary
     defpkg events generated for the portcullis.

     o Fixed a bug that has caused errors when reading symbols from a
     portcullis that are in undefined packages defined in locally
     included books.

     o Fixed a bug that could lead to failure of include-book caused by
     a subtle interaction between set-ignore-ok and defpkg events
     generated for the portcullis of a certificate.

*PROVER ALGORITHM ENHANCEMENTS*

Non-linear arithmetic (see NON-LINEAR-ARITHMETIC) has been
improved to be more efficient or more powerful in some cases.  Thanks
to Robert Krug for contributing these improvements.

Improved certain (so-called "type-set") reasoning about whether or not
expressions denote integers.  Thanks to Robert Krug for contributing
code to implement this change, along with examples illustrating its
power that are now distributed in the book
books/misc/integer-type-set-test.lisp.

Improved ACL2's heuristics for relieving hypotheses, primarily to use
linear reasoning on conjuncts and disjuncts of the test of an if
expression.  For example, given a hypothesis of the form (if (or term1
term2) ...), ACL2 will now use linear reasoning to attempt to prove
both term1 and term2, not merely for term2.  Thanks to Robert Krug for
supplying examples illustrating the desirability of such an improvement
and for useful discussions about the fix.

Made a slight heuristic change, so that when a hypothesis with let or
mv-let subterms (i.e. lambda subterms) rewrites to t, then that
hypothesis is necessarily eliminated.  Thanks to Jared Davis for sending
an example that led us to develop this change, and thanks to Robert
Krug for a helpful discussion.

*MISCELLANEOUS*

Added documentation on how to use make-event to avoid duplicating
expensive computations, thanks to Jared Davis.  See
USING-TABLES-EFFICIENTLY.

Modified the error message for calls of undefined functions to show the
arguments.  Thanks to Bob Boyer for requesting this enhancement.

Modified utilies :pr, :pr!, :pl, and :show-bodies to incorporate code
contributed by Jared Davis.  That code defines low-level source
functions info-for-xxx that collect information about rules, which is
thus available to advanced users.

Dynamic monitoring of rewrites (see DMR) has been improved in
the following ways, as suggested by Robert Krug.

     o Some stale entries from the rewrite stack are no longer printed,
     in particular above ADD-POLYNOMIAL-INEQUALITIES.

     o An additional rewrite stack entry is made when entering
     non-linear arithmetic (see NON-LINEAR-ARITHMETIC).

     o An ADD-POLYNOMIAL-INEQUALITIES entry is printed with a counter,
     to show how often this process is called.

Modified save-exec so that the newly-saved image will have the same raw
Lisp package as the existing saved image.  This is a very technical
change that will likely not impact most users; for example, the package
in the ACL2 read-eval-print loop (see LP) had already persisted
from the original to newly-saved image.  Thanks to Jared Davis for
suggesting this change.

Changed make-event expansion so that changes to set-saved-output,
set-print-clause-ids, set-fmt-soft-right-margin, and
set-fmt-hard-right-margin will persist after being evaluated during
make-event expansion.  (Specifically, *protected-system-state-globals*
has been modified; see MAKE-EVENT-DETAILS.)  Thanks to Jared
Davis for bringing this issue to our attention.

Output from the proof-checker is now always enabled when invoking
verify, even if it is globally inhibited (see
SET-INHIBIT-OUTPUT-LST).

Improved the message printed when an :induct hint fails, to give more
information in some cases.  Thanks to Rex Page for suggesting where an
improvement could be made and providing useful feedback on an initial
improvement.

Added a warning for congruence rules (see DEFCONG) that specify
iff as the second equivalence relation when equal can be used instead.
Those who heed these warnings can eliminate certain subsequent
double-rewrite warnings for rewrite rules with conclusions of the form
(iff term1 term2), and hence implicitly for Boolean conclusions term1
that are interpreted as (iff term1 t).  Thanks to Sarah Weissman for
sending us an example that highlighted the need for such a warning.

Modified macro :redef! (which is for system implementors) so that it
eliminates untouchables.

Several improvements have been made to the experimental hons/memoization
version of ACL2.  See HONS-AND-MEMOIZATION.

The distributed books directory, (@ distributed-books-dir), is now
printed in the start-up message.

NOTE-3-3(R)    ACL2 Version  3.3(r) (xxx, 20xx) Notes

Please also see NOTE-3-3 for changes to Version  3.3 of ACL2.

NOTE-3-4    ACL2 Version  3.4 (August, 2008) Notes

NOTE!  New users can ignore these release notes, because the
documentation has been updated to reflect all changes that are recorded
here.

Below we roughly organize the changes since Version  3.3 into changes to
existing features, new features, bug fixes, new and updated books, and
Emacs support.  Each change is described just once, though of course
many changes could be placed in more than one category.

*CHANGES TO EXISTING FEATURES*

Fixed a long-standing potential infinite loop in the rewriter.  Thanks
to Sol Swords for sending a concise example illustrating the looping
behavior.  (Those interested in details are welcome to look at the
comment about loop behavior in source function rewrite-equal.)

Incorporated a slight strengthening of non-linear arithmetic
contributed by Robert Krug (thanks, Robert).  With non-linear
arithmetic enabled, the problem was essentially that ACL2 made the
following "optimization": given inequalities (< a u) and (< b v), for
positive rational constants a and b terms u and v of which at least one
is known to be rational, infer (< (* a b) (* u v)).  Without this
optimization, however, ACL2 now infers the stronger inequality obtained
by direct multiplication of the two given inequalities.  To see the
effect of this change, submit the event (set-non-linearp t) followed by:

     (thm (implies (and (rationalp x) (< 3 x)
                        (rationalp y) (< 4 y))
                   (< 0 (+ 12 (* -4 x) (* -3 y) (* x y)))))

The utility set-checkpoint-summary-limit has been modified in several
ways: it now takes a single argument (no longer takes state as an
argument); a natural number n abbreviates the pair (n . n); the
argument is no longer evaluated, but it still optionally may be quoted;
and a new value, t, suppresses all printing of the checkpoint summary.
Thanks to Jared Davis for suggesting most of these improvements.

There was formerly a restriction on mbe that the :exec argument may not
contain a call of mbe.  This restriction has been removed, thanks to a
request from Jared Davis and Sol Swords.  Thanks also to Sandip Ray, who
pointed out that this restriction may have been in place in order that
defexec can guarantee termination using the :exec code; its
documentation has therefore been updated to clarify this situation.

Rules of class :rewrite are now stored by performing certain logical
simplifications on the left side of the conclusion: (prog2$ X Y) is
replaced by Y, (mbe :logic X :exec Y) is replaced by X (more precisely,
the analogous change is made to the generated call of must-be-equal);
and (the TYPE X) is replaced by X (again, the change is actually made
on the macroexpanded form).  Thanks to Jared Davis and Sol Swords for
requesting this change.  An analogous change has also been made for
rules of class :forward-chaining.

The trace$ utility has been reimplemented to work independently of the
underlying Lisp trace.  It thus works the same for every host Lisp,
except as provided by an interface to the underlying host Lisp trace
(the :native option).  Note that the host Lisp trace continues to be
modified for GCL, Allegro CL, and CCL (OpenMCL); see TRACE.
See TRACE$ for updated detailed documentation on tracing
options, many of which are new, for example an :evisc-tuple option that
can be set to :no-print if you want the function traced without the
usual entry and exit printing.  The previous trace$ had some issues,
including the following, which have all been fixed.  Thanks to Peter
Dillinger for assistance in determining desired functionality of the
new trace$ and for helping to test it.

     Recursive calls were not always shown in the trace for two reasons.
     (1) Compiler inlining could prevent recursive calls from being
     shown in the trace, in particular in CCL (OpenMCL).  Thanks to
     Jared Davis and Warren Hunt for pointing out this issue and
     requesting a fix, and to Bob Boyer and Gary Byers for relevant
     helpful discussions.  (2) ACL2's algorithm for producing
     executable counterparts prevented tracing of recursive calls even
     after (set-guard-checking :none).  Thanks to Peter Dillinger for
     requesting a fix.

     It was possible to exploit a bug in the interaction of multiple
     values and trace to prove a contradiction.  An example is in a
     comment in (deflabel note-3-4 ...) in the ACL2 source code.

     Certain large structures could cause expensive computations for
     printing even when a :cond condition was specified and evaluated
     to nil.

     Trace! now suppresses printing of the event summary, and returns
     the value that would be returned (if there is an active trust tag)
     by the corresponding call of trace$.

     Some bugs have been fixed in the underlying native trace installed
     by ACL2 for GCL, Allegro CL, and CCL (OpenMCL), including the
     following.  In GCL it had been impossible to use the variable
     ARGLIST in a :cond expression.  In Allegro CL and CCL, a trace$
     bug mishandled tracing non-ACL2 functions when directives such as
     :entry and :exit were supplied.  GCL trace now hides the world
     even when tracing non-ACL2 functions.  Tracing in CCL no longer
     causes a Lisp error when untracing a traced function defined
     outside the ACL2 loop; for example (trace$ len1) followed by
     (untrace$ len1) no longer causes an error.

The macro wet has been changed, for the better we think.  see
WET.

The generation of goals for forcing-rounds has been changed to avoid
dropping assumptions formerly deemed "irrelevant".  (A simple example
may be found in a comment in source function unencumber-assumption,
source file prove.lisp.)  Thanks to Jared Davis for sending us an
example that led us to make this change.

Modified the implementation of make-event so that in the certificate of
a book, local events arising from make-event forms are elided.  For
example, if (make-event <form>) expands to (local <expanded-form>),
then where the latter had been stored in the certificate, now instead
(local (value-triple :ELIDED)) will be stored.  Thanks to Eric Smith
for requesting this improvement.  He has reported that a preliminary
version of this improvement shrunk a couple of his .cert files from
perhaps 40MB each to about 140K each.

Now, a table event that sets the entire table, (table tbl nil alist
:clear), is redundant (see REDUNDANT-EVENTS) when the supplied
alist is equal to the current value of the table.  Thanks to Peter
Dillinger for requesting this change.

The event constructor progn! now returns the value that is returned by
evaluation of its final form if no error occurs, except that it still
returns nil if the that final evaluation leaves ACL2 in raw-mode.

:Pso and :psog have been improved so that they show the key checkpoint
summary at the end of a failed proof.  (For a discussion of key
checkpoints, see SET-GAG-MODE.)  As a result, a call of
set-checkpoint-summary-limit now affects subsequent evaluation of :pso
and :psog.  In particular, you no longer need to reconstruct a proof
(by calling thm or defthm) in order to see key checkpoints that were
omitted due to the limit; just call set-checkpoint-summary-limit and
then run :pso or :psog.

The proof-checker behaves a little differently under gag-mode.  Now,
proof-checker commands that call the theorem prover to create new
proof-checker goals, such as bash and induct (see
PROOF-CHECKER-COMMANDS), will show key checkpoints when in gag-mode.
As before, proof-checker commands pso and pso! (and now, also psog) --
see PSO, see PSOG, and see PSO! -- can then
show the unedited proof log.  However, unlike proof attempts done in
the ACL2 loop, such proof attempts will not show a summary of key
checkpoints at the end, because from a prover perspective, all such
goals were considered to be temporarily "proved" by giving them "byes",
to be dispatched by later proof-checker commands.

A little-known feature had been that a measure of 0 was treated as
though no measure was given.  This has been changed so that now, a
measure of nil is treated as though no measure was given.

Expanded *acl2-exports* to include every documented symbol whose name
starts with "SET-".  Thanks to Jared Davis for remarking that
set-debugger-enable was omitted from *acl2-exports*, which led to this
change.

The trace mechanism has been improved so that the :native and
:multiplicity options can be used together for Lisps that support the
trace :exit keyword.  These Lisps include GCL and Allegro CL, whose
native trace utilities have been modified for ACL2.  For SBCL and CCL
(OpenMCL), which use the built-in Lisp mechanism for returning multiple
values in ACL2 (see MV), the use of :multiplicity with :native
remains unnecessary and will be ignored.  In support of this change, the
modification of native Allegro CL tracing for ACL2 was fixed to handle
:exit forms correctly that involve mv.

*NEW FEATURES*

The command :redef! is just like :redef, but prints a warning rather
than doing a query.  The old version of :redef! was for system hackers
and has been renamed to :redef+.

Introduced a new utility for evaluating a function call using the
so-called executable counterpart -- that is, executing the call in the
logic rather than in raw Lisp.  See EC-CALL.  Thanks to Sol
Swords for requesting this utility and participating in its high-level
design.

See PRINT-GV for a new utility that assists with debugging guard
violations. Thanks to Jared Davis for requesting more tool assistance
for debugging guard violations.

Improved the guard violation error message to show the positions of the
formals, following to a suggestion of Peter Dillinger.

Added new guard-debug capability to assist in debugging failed attempts
at guard verification.  See GUARD-DEBUG.  Thanks to Jared Davis
for requesting a tool to assist in such debugging and to him, Robert
Krug, and Sandip Ray for useful discussions.

New utilities provide the formula to be proved by verify-guards.  See
VERIFY-GUARDS-FORMULA and see GUARD-OBLIGATION, Thanks
to Mark Reitblatt for making a request leading to these utilities.
These utilities can be applied to a term, not just an event name;
thanks to Peter Dillinger for correspondence that led to this extension.

A new utility causes runes to be printed as lists in proof output from
simplification, as is done already in proof summaries.  See
SET-RAW-PROOF-FORMAT.  Thanks to Jared Davis for requesting this
utility.

An experimental capability allows for parallel evaluation.  See
PARALLELISM.  Thanks to David Rager for providing an initial
implementation of this capability.

Defined xor in analogy to iff.  Thanks to Bob Boyer, Warren Hunt, and
Sol Swords for providing this definition.

Improved distributed file doc/write-acl2-html.lisp so that it can now be
used to build HTML documentation files for documentation strings in user
books.  See the comment in the definition of macro
acl2::write-html-file at the end of that file.  Thanks to Dave Greve and
John Powell for requesting this improvement.

It is now possible to specify :hints for non-recursive function
definitions (which can be useful when definitions are automatically
generated).  See SET-BOGUS-DEFUN-HINTS-OK.  Thanks to Sol
Swords for requesting such a capability.

Keyword argument :dir is now supported for rebuild just as it has been
for ld.

We relaxed the criteria for functional substitutions, so that a function
symbol can be bound to a macro symbol that corresponds to a function
symbol in the sense of macro-aliases-table.  So for example, a
functional substitution can now contain the doublet (f +), where
previously it would have been required instead to contain (f binary-+).

We now allow arbitrary packages in raw mode (see SET-RAW-MODE)
-- thanks to Jared Davis for requesting this enhancement -- and more
than that, we allow arbitrary Common Lisp in raw mode.  Note however
that for arbitrary packages, you need to be in raw mode when the input
is read, not just when the input form is evaluated.

Two new keywords are supported by the with-output macro.  A :gag-mode
keyword argument suppresses some prover output as is done by
set-gag-mode.  Thanks to Jared Davis for asking for a convenient way to
set gag-mode inside a book, in particular perhaps for a single theorem;
this keyword provides that capability.  A :stack keyword allows
sub-events of progn or encapsulate to "pop" the effect of a superior
with-output call.  Thanks to Peter Dillinger for requesting such a
feature.  See WITH-OUTPUT.

The command good-bye and its aliases exit and quit now all take an
optional status argument, which provides the Unix exit status for the
underlying process.  Thanks to Florian Haftmann for sending a query to
the ACL2 email list that led to this enhancement.

Keyword commands now work for macros whose argument lists have lambda
list keywords.  For a macro with a lambda list keyword in its argument
list, the corresponding keyword command reads only the minimum number
of required arguments.  See KEYWORD-COMMANDS.

It is now legal to declare variables ignorable in let* forms, as in
(let* ((x (+ a b)) ...) (declare (ignorable x)) ...).  Thanks to Jared
Davis for requesting this enhancement.

Added a warning when more than one hint is supplied explicitly for the
same goal.  It continues to be the case that only the first hint
applicable to a given goal will be applied, as specified in the
user-supplied list of :hints followed by the default-hints-table.
Thanks to Mark Reitblatt for sending a question that led both to adding
this clarification to the documentation and to adding this warning.

You may now use set-non-linear, set-let*-abstraction, set-tainted-ok,
and set-ld-skip-proofs in place of their versions ending in "p".
Thanks to Jared Davis for suggesting consideration of such a change.
All "set-" utilites now have a version without the final "p" (and most
do not have a version with the final "p").

Added a "Loop-Stopper" warning when a :rewrite rule is specified with a
:loop-stopper field that contains illegal entries that will be ignored.
Thanks to Jared Davis for recommending such a warning.

Added a substantial documentation topic that provides a beginner's
guide to the use of quantification with defun-sk in ACL2.  Thanks to
Sandip Ray for contributing this guide, to which we have made only very
small modifications.  See QUANTIFIER-TUTORIAL.

Defun-sk now allows the keyword option :strengthen t, which will
generate the extra constraint that that is generated for the
corresponding defchoose event; see DEFCHOOSE.  Thanks to Dave
Greve for suggesting this feature.

*BUG FIXES*

Fixed a soundness bug related to the use of mbe inside encapsulate
events.  An example proof of nil (before the fix) is in a comment in
(deflabel note-3-4 ...) in the ACL2 source code.  We therefore no
longer allow calls of mbe inside encapsulate events that have non-empty
signatures.

Fixed a bug related to the definition of a function supporting the
macro value-triple.  Although this bug was very unlikely to affect any
user, it could be carefully exploited to make ACL2 unsound:

     (defthm fact
       (equal (caadr (caddr (value-triple-fn '(foo 3) nil nil)))
              'value) ; but it's state-global-let* in the logic
       :rule-classes nil)
     (defthm contradiction
       nil
       :hints (("Goal" :use fact :in-theory (disable (value-triple-fn))))
       :rule-classes nil)

Non-LOCAL definitions of functions or macros are no longer considered
redundant with built-ins when the built-ins have special raw Lisp code,
because ACL2 was unsound without this restriction!  A comment about
redundant definitions in source function chk-acceptable-defuns shows
how one could prove nil without this new restriction.  Note that system
utility :redef+ removes this restriction.

Although ACL2 already prohibited the use of certain built-in :program
mode functions for verify-termination and during macroexpansion, we
have computed a much more complete list of functions that need such
restrictions, the value of constant
*primitive-program-fns-with-raw-code*.

Modified what is printed when a proof fails, to indicate more clearly
which event failed.

Fixed a problem with dmr in CCL (OpenMCL) that was causing a raw Lisp
break after an interrupt in some cases.  Thanks to Gary Byers for a
suggestion leading to this fix.

Fixed bugs in proof-checker code for dealing with free variables in
hypotheses.

Upon an abort, the printing of pstack and gag-mode summary information
for other than GCL was avoided when inside a call of ld.  This has been
fixed.

(Windows only) Fixed bugs for ACL2 built on SBCL on Windows, including
one that prevented include-book parameters :dir :system from working,
and one that prevented certain compilation.  Thanks to Peter Dillinger
for bringing these to our attention and supplying a fix for the second.
Thanks also to Andrew Gacek for bringing include-book issues to our
attention.  Also, fixed writing of file saved_acl2 at build time so
that for Windows, Unix-style pathnames are used.

Fixed a hard Lisp error that could occur with keywords as table names,
e.g., (table :a :a nil :put).  Thanks to Dave Greve for bringing this
problem to our attention and providing this example.

Fixed handling of :OR hints so that proof attempts under an :OR hint do
not abort (reverting to induction on the original input conjecture)
prematurely.  Thanks to Robert Krug for pointing out this problem and
pointing to a possible initial fix.

(SBCL and CLISP only) It is now possible to read symbols in the
"COMMON-LISP" package inside the ACL2 command loop (see LP).
This could cause a raw Lisp error in previous versions of ACL2 whose
host Common Lisp was SBCL or CLISP.  Thanks to Peter Dillinger for
bringing this issue to our attention.

Fixed a bug that was preventing certain hints, such as :do-not hints,
from being used after the application of an :or hint.  Thanks to Robert
Krug for bringing this bug to our attention.

(Hons version only) Fixed a bug in the interaction of memoize (hons
version only) with event processing, specifically in interaction with
failures inside a call of progn or encapsulate.  Thanks to Jared Davis
for bringing this bug to our attention and sending an example.  A
simplified example may be found in a comment in source function
table-cltl-cmd, source file history-management.lisp; search for
"Version_3.3" there.

Fixed cw-gstack so that its :evisc-tuple is applied to the top clause,
instead of using (4 5 nil nil) in all cases.  If no :evisc-tuple is
supplied then (term-evisc-tuple t state) is used for the top clause, as
it is already used for the rest of the stack.

Fixed a bug in the interaction of proof-trees with :induct hint value
:otf-flg-override.  Thanks to Peter Dillinger for reporting this bug
and sending an example that evokes it.

Fixed bugs in :pr and find-rules-of-rune for the case of rule class
:elim.  Thanks to Robert Krug and Jared Davis for bringing these
related bugs to our attention.

Improved failure messages so that the key checkpoints are printed only
once when there is a proof failure.  Formerly, a proof failure would
cause the key checkpoints to be printed for every encapsulate or
certify-book superior to the proof attempt.

Fixed a bug in generation of guards for calls of pkg-witness.  Thanks
to Mark Reitblatt for sending an example showing this bug.  The bug can
be in play when you see the message:  "HARD ACL2 ERROR in
MAKE-LAMBDA-APPLICATION: Unexpected unbound vars ("")".  A distillation
of Mark's example that causes this hard error is as follows.

     (defun foo (x)
       (declare (xargs :guard t))
       (let ((y x)) (pkg-witness y)))

The cond macro now accepts test/value pairs of the form (T val) in
other than the last position, such as the first such pair in (cond (t
1) (nil 2) (t 3)).  Thanks to Jared Davis for sending this example and
pointing out that ACL2 was sometimes printing goals that have such a
form, and hence cannot be submitted back to ACL2.  A few macros
corresponding to cond in some books under books/rtl and books/bdd were
similarly modified.  (A second change will probably not be noticeable,
because it doesn't affect the final result: singleton cond clauses now
generate a call of or in a single step of macroexpansion, not of if.
For example, (cond (a) (b x) (t y)) now expands to (OR A (IF B X Y))
instead of (IF A A (IF B X Y)).  See the source code for cond-macro for
a comment about this change.)

Fixed a bug in the interaction of proof-checker command DV, including
numeric ("diving") commands, with the add-binop event.  Specifically,
if you executed (add-binop mac fn) with fn having arity other than 2, a
proof-checker command such as 3 or (dv 3) at a call of mac could have
the wrong effect.  We also fixed a bug in diving with DV into certain
AND and OR calls.  Thanks for Mark Reitblatt for bringing these
problems to our attention with helpful examples.

Fixed a couple of bugs that were causing an error, "HARD ACL2 ERROR in
RENEW-NAME/OVERWRITE".  Thanks to Sol Swords for bringing the first of
these bugs to our attention.

Fixed a bug that could cause certify-book to fail in certain cases
where there are local make-event forms.

Fixed a bug in start-proof-tree that could cause Lisp to hang or
produce an error.  Thanks to Carl Eastlund for sending an example to
bring this bug to our attention.

Fixed a bug in the proof output, which was failing to report cases
where the current goal simplifies to itself or to a set including itself
(see SPECIOUS-SIMPLIFICATION).

Fixed a bug in with-prover-time-limit that was causing a raw Lisp error
for a bad first argument.  Thanks to Peter Dillinger for pointing out
this bug.

The following was claimed in :doc note-3-3, but was not fixed until the
present release:
Distributed directory doc/HTML/ now again includes installation
instructions, in doc/HTML/installation/installation.html.

In certain Common Lisp implementations -- CCL (OpenMCL) and Lispworks,
at least -- an interrupt could leave you in a break such that quitting
the break would not show the usual summary of key checkpoints.  This
has been fixed.

*NEW AND UPDATED BOOKS*

Updated books/clause-processors/SULFA/ with a new version from Erik
Reeber; thanks, Erik.

Added new books directory tools/ from Sol Swords.  See
books/tools/Readme.lsp for a summary of what these books provide.

The distributed book books/misc/file-io.lisp includes a new utility,
write-list!, which is like write-list except that it calls
open-output-channel! instead of open-output-channel.  Thanks to Sandip
Ray for requesting this utility and assisting with its implementation.

Added record-update macro supplied by Sandip Ray to distributed book
books/misc/records.lisp.

Sandip Ray has contributed books that prove soundness and completeness
of different proof strategies used in sequential program verification.
Distributed directory books/proofstyles/ has three new directories
comprising that contribution: soundness/, completeness/, and
counterexamples/.  The existing books/proofstyles/ directory has been
moved to its subdirectory invclock/.

Jared Davis has contributed a profiling utility for ACL2 built on CCL
(OpenMCL).  See books/misc/oprof.lisp.  Thanks, Jared.

ACL2 utilities getprop and putprop take advantage of under-the-hood
Lisp (hashed) property lists.  The new book books/misc/getprop.lisp
contains an example showing how this works.

Added the following new book directories: books/paco/, which includes a
small ACL2-like prover; and books/models/jvm/m5, which contains the
definition of one of the more elaborate JVM models, M5, along with other
files including JVM program correctness proofs.  See files Readme.lsp in
these directories, and file README in the latter.

Added books about sorting in books/sorting.  See Readme.lsp in that
directory for documentation.

Added book books/misc/computed-hint-rewrite.lisp to provide an interface
to the rewriter for use in computed hints.  Thanks to Jared Davis for
requesting this feature.

Jared Davis has provided a pseudorandom number generator, in
books/misc/random.lisp.

Robert Krug has contributed a new library, books/arithmetic-4/, for
reasoning about arithmetic.  He characterizes it as being more powerful
than its predecessor, books/arithmetic-3/, and without its predecessor's
rewriting loops, but significantly slower than its predecessor on some
theorems.

Incorporated changes from Peter Dillinger to verify guards for
functions in books/ordinals/lexicographic-ordering.lisp (and one in
ordinal-definitions.lisp in that directory).

A new directory, books/hacking/, contains a library for those who wish
to use trust tags to modify or extend core ACL2 behavior.  Thanks to
Peter Dillinger for contributing this library.  Obsolete version
books/misc/hacker.lisp has been deleted.  Workshop contribution
books/workshops/2007/dillinger-et-al/code/ is still included with the
workshops/ tar file, but should be considered deprecated.

In books/make-event/assert.lisp, changed assert! and assert!-stobj to
return (value-triple :success) upon success instead of (value-triple
nil), following a suggestion from Jared Davis.

*EMACS SUPPORT*

Changed emacs/emacs-acl2.el so that the fill column default (for the
right margin) is only set (still to 79) in lisp-mode.

Modified Emacs support in file emacs/emacs-acl2.el so that names of
events are highlighted just as defun has been highlighted when it is
called.  Search in the above file for font-lock-add-keywords for
instructions on how to eliminate this change.

The name of the temporary file used by some Emacs utilities defined in
file emacs/emacs-acl2.el has been changed to have extension .lsp instead
of .lisp; thus it is now temp-emacs-file.lsp.  Also, `make' commands to
`clean' books will delete such files (specifically,
books/Makefile-generic has been changed to delete temp-emacs-file.lsp).

NOTE-3-4(R)    ACL2 Version  3.4(r) (August, 2008) Notes

Please also see NOTE-3-4 for changes to Version  3.4 of ACL2.

Fixed makefiles, books/nonstd/Makefile and GNUmakefile.  The old set-up
seemed to work fine as long as all books certified, but it was really
broken, for example only certifying some of the books in
books/nonstd/nsa/, and then only when required by books in other
directories.  Also fixed the "clean" target to clean links rather than
to make links.

NOTE-3-5    ACL2 Version  3.5 (May, 2009) Notes

NOTE!  New users can ignore these release notes, because the
documentation has been updated to reflect all changes that are recorded
here.

Below we roughly organize the changes since Version  3.4 into the
following categories: changes to existing features, new features,
heuristic improvements, bug fixes, new and updated books, Emacs
support, and experimental hons version.  Each change is described in
just one category, though of course many changes could be placed in
more than one category.

*CHANGES TO EXISTING FEATURES*

Many improvements have been made to ACL2's "evisceration" mechanism for
hiding substructures of objects before they are printed, and to related
documentation:

     o A new documentation topic explains evisc-tuples.  See
     EVISC-TUPLE.

     o A new interface, set-evisc-tuple, has been provided for setting
     the four global evisc-tuples.  See SET-EVISC-TUPLE.

     o A new mode, "iprinting", allows eviscerated output to be read
     back in.  See SET-IPRINT.

     o Function default-evisc-tuple has been deprecated and will
     probably be eliminated in future releases; use abbrev-evisc-tuple
     instead.  Also eliminated is the brr-term-evisc-tuple (also the
     user-brr-term-evisc-tuple).  The term-evisc-tuple controls
     printing formerly controlled by the brr-term-evisc-tuple or
     user-brr-term-evisc-tuple.

     o ACL2 output is done in a more consistent manner, respecting the
     intention of those four global evisc-tuples.  In particular, more
     proof output is sensitive to the term-evisc-tuple.  Again, see
     SET-EVISC-TUPLE.

     o A special value, :DEFAULT, may be provided to set-evisc-tuple in
     order to restore these evisc-tuples to their original settings.

     o (Details for heavy users of the evisc-tuple mechanism) (1) There
     are no longer state globals named user-term-evisc-tuple or
     user-default-evisc-tuple.  (2) Because of the above-mentioned
     :DEFAULT, if you have referenced state globals directly, you
     should use accessors instead, for example (abbrev-evisc-tuple
     state) instead of (@ abbrev-evisc-tuple).  (3) For uniformity,
     set-trace-evisc-tuple now takes a second argument, state.

Improved break-on-error in several ways.  First, it breaks earlier in a
more appropriate place.  Thanks to Dave Greve for highlighting this
problem with the existing implementation.  Also, break-on-error now
breaks on hard errors, not only soft errors (see ER, options
hard and hard?).  Thanks to Warren Hunt and Anna Slobodova for sending
an example that showed a flaw in an initial improvement.  Finally, new
options cause printing of the call stack for some host Common Lisps.
See BREAK-ON-ERROR.  Thanks to Bob Boyer for requesting this
feature.

Trace! may now be used in raw Lisp (though please note that all
soundness claims are off any time you evaluate forms in raw Lisp!).
Thanks to Bob Boyer for feedback that led to this enhancement.

ACL2 now searches for file acl2-customization.lsp in addition to (and
just before) its existing search for acl2-customization.lisp; See
ACL2-CUSTOMIZATION.  Thanks to Jared Davis for suggesting this change,
which supports the methodology that files with a .lisp extension are
certifiable books (thus avoiding the need to set the BOOKS variable in
makefiles; see BOOK-MAKEFILES).

Improved the error message for illegal declare forms of the form (type
(satisfies ...)).  Thanks to Dave Greve for sending an example
highlighting the issue.

If trace output is going to a file (because open-trace-file has been
executed), then a note will be printed to that effect at the time that
a call of trace$ or trace! is applied to one or more trace specs.

The notion of redundancy (see REDUNDANT-EVENTS) has been made
more restrictive for mutual-recursion events.  Now, if either the old
or new event is a mutual-recursion event, then redundancy requires that
both are mutual-recursion events that define the same set of function
symbols.  Although we are not aware of any soundness bugs fixed by this
modification, nevertheless we believe that it reduces the risk of
soundness bugs in the future.

The definition of trace* has been moved to a book, misc/trace1.lisp.  A
new version, used in ACL2s, is in book misc/trace-star.lisp.  Trace
utilities trace$ and trace! are still built into ACL2.

Certain certificate files will now be much smaller, by printing in a way
that takes advantage of structure sharing.  Certifying the following
example produces a .cert file of over 3M before this change, but less
than 1K after the change.

     (defun nest (i)
       ;; Makes an exponentially-sized nest of conses i deep.
       (if (zp i)
           nil
         (let ((next (nest (1- i))))
           (cons next next))))

     (make-event
      `(defconst *big* ',(nest 20)))

Thanks to Sol Swords for providing the above example and to him as well
as to Bob Boyer, Jared Davis, and Warren Hunt for encouraging
development of this improvement.  We have also applied this improvement
to the printing of function definitions to files on behalf of
certify-book and comp.

Names of symbols are now printed with vertical bars according to the
Common Lisp spec.  Formerly, if the first character of a symbol name
could be the first character of the print representation of a number,
then the symbol was printed using vertical bars (|..|) around its name.
Now, a much more restrictive test for "potential numbers" is used,
which can result in fewer such vertical bars.  Base 16 is now carefully
considered as well; see SET-PRINT-BASE.  Thanks to Bob Boyer
for requesting this improvement.  Note that macros set-acl2-print-base
and set-acl2-print-case have been replaced by functions; see
SET-PRINT-BASE and see SET-PRINT-CASE.

The ACL2 reader now supports `#.' syntax in place of the `#, syntax
formerly supported.  Thanks to Bob Boyer for requesting this change.
See SHARP-DOT-READER.  NOTE that because of this change, `#.'
no longer causes an abort; instead please use (a!) or optionally, if in
the ACL2 loop, :a!; see A!.

Some small changes have been made related to gag-mode:

     o Gag-mode now suppresses some messages that were being printed
     upon encountering disjunctive splits from :OR hints.  Thanks to Sol
     Swords for suggesting this improvement.

     o ACL2 had printed "Q.E.D." with all output suppressed and
     gag-mode enabled.  Now, "Q.E.D." will be suppressed when PROVE and
     SUMMARY output are suppressed, even if gag-mode is enabled.

     o The use of set-gag-mode had drastic effects on the inhibited
     output (see SET-INHIBIT-OUTPUT-LST), basically inhibiting
     nearly all output (even most warnings) when turning on gag-mode
     and enabling all output except proof-tree output when turning off
     gag-mode.  Now, set-gag-mode only inhibits or enables proof
     (PROVE) output, according to whether gag-mode is being turned on
     or off (respectively).  The related utility set-saved-output has
     also been modified, basically to eliminate :all as a first
     argument and to allow t and :all as second arguments, for
     inhibiting prover output or virtually all output, respectively
     (see SET-SAVED-OUTPUT).

A defstub event signature specifying output of the form (mv ...) now
introduces a :type-prescription rule asserting that the new function
returns a true-listp result.  Thanks to Bob Boyer for sending the
following example, which motivated this change.

     (defstub census (*) => (mv * *))
     (defn foo (x)
       (mv-let (a1 a2)
               (census x)
               (list a1 a2)))

Improved the efficiency of string-append so that in raw Lisp, it calls
concatenate.  Thanks to Jared Davis for suggesting this change,
including the use of mbe.  A minor change was made to the definition of
concatenate to support this change, and the lemma append-to-nil was
added (see below).

The checksum algorithm used for certificate files of books has been
changed.  Thanks to Jared Davis for contributing the new code.  This
change will likely not be noticed unless one is using the experimental
hons version of ACL2, where it can greatly speed up book certification
and inclusion because of function memoization (of source function
fchecksum-obj).

Fewer calls are made to the checksum algorithm on behalf of
certify-book and a few other operations.  Thanks to Jared Davis for
providing data that helped lead us to these changes.

Formatted printing directives ~p, ~q, ~P, and ~Q are deprecated, though
still supported.  See FMT.  Instead, please use ~x, ~y, ~X, and
~Y (respectively).  As a by-product, rule names in proof output are no
longer hyphenated.

A new keyword, :multiplicity, is available for tracing raw Lisp
functions using the ACL2 trace utility.  See TRACE$.

Users may now control whether or not a slow array access results in a
warning printed to the screen (which is the default, as before), and if
so, whether or not the warning is followed by a break.  See
SLOW-ARRAY-WARNING.

On linux-like systems (including Mac OS X and SunOS), :comp will now
write its temporary files into the "/tmp" directory, which is the value
of state global 'tmp-dir.  You can change that directory with (assign
tmp-dir "<your_temp_directory_path>").

The messages printed for uncertified books have been enhanced.  Thanks
to Jared Davis for requesting such an improvement.

A function definition that would be redundant if in :logic mode is now
considered redundant even if it (the new definition) is in :program
mode.  That is, if a definition is "downgraded" from :logic to :program
mode, the latter (:program mode) definition is considered redundant.
Previously, such redundancy was disallowed, but we have relaxed that
restriction because of a scenario brought to our attention by Jared
Davis: include a book with the :logic mode definition, and then include
a book with the :program mode definition followed by
verify-termination.  Thanks, Jared.

The ACL2 reader no longer accepts characters other than those
recognized by standard-char-p except for #\Tab, #\Page, and #\Rubout
(though it still accepts strings containing such characters).  As a
result, no make-event expansion is allowed to contain any such
unacceptable character or string.  Thanks to Sol Swords for sending an
example that led us to make this restriction.  A simple example is the
following book:

     (in-package "ACL2")
     (defconst *my-null* (code-char 0))
     (make-event `(defconst *new-null* ,*my-null*))

For this book, a call of certify-book formerly broke during the
compilation phase, but if there was no compilation, then a call of
include-book broke.  Now, the error occurs upon evaluation of the
make-event form.

ACL2 now collects up guards from declare forms more as a user might
expect, without introducing an unexpected ordering of conjuncts.  We
thank Jared Davis for sending us the following illustrative example,
explained below.

     (defun f (x n)
       (declare (xargs :guard (and (stringp x)
                                   (natp n)
                                   (= (length x) n)))
                (type string x)
                (ignore x n))
       t)

Formerly, a guard was generated for this example by unioning the
conjuncts from the :guard onto a list containing the term (string x)
generated from the type declaration, resulting in an effective guard of:

     (and (natp n)
          (= (length x) n)
          (stringp x))

The guard of this guard failed to be verified because (stringp x)) now
comes after the call (length x).  With the fix, contributions to the
guards are collected up in the order in which they appear.  So in the
above example, the effective guard is the specified :guard; the
contribution (stringp x) comes later, and is thus dropped since it is
redundant.  NOTE by the way that if :guard and :stobjs are specified in
the same xargs form, then for purposes of collecting up the effective
guard as described above, :stobjs will be treated as through it comes
before the :guard.

Modified close-output-channel to try to do a better job flushing
buffers.  Thanks to Bob Boyer for helpful correspondence.

The notion of "subversive recursion" has been modified so that some
functions are no longer marked as subversive.  See
SUBVERSIVE-RECURSIONS, in particular the discussion elaborating on
the notion of "involved in the termination argument" at the end of that
documentation topic.

Formerly, :type-prescription rules for new definitions inside
encapsulate forms were sometimes added as constraints.  This is no
longer the case.  See also discussion of the "soundness bug in the
forming of constraints", which is related.

*NEW FEATURES*

It is now possible to affect ACL2's termination analysis (and resulting
induction analysis).  Thanks to Peter Dillinger for requesting this
feature.  The default behavior is essentially unchanged.  But for
example, the following definition is accepted by ACL2 because of the
use of the new :ruler-extenders features; See RULER-EXTENDERS.

       (defun f (x)
         (declare (xargs :ruler-extenders :all))
         (cons 3
               (if (consp x)
                   (f (cdr x))
                 nil)))

The following lemma was added in support of the improvement to
string-append described above:

     (defthm append-to-nil
       (implies (true-listp x)
                (equal (append x nil)
                       x)))

A mechanism has been provided for users to contribute documentation.
See MANAGING-ACL2-PACKAGES for an example, which contains a
link to an external web page on effective use of ACL2 packages, kindly
provided by Jared Davis.  ACL2 documentation strings may now link to
external web pages using the new symbol, ~url; see MARKUP.  Of
course, those links appear in the web version of the documentation, but
you made need to take a bit of action in order for these to appear as
links in the Emacs Info version; see DOCUMENTATION.

Added intersectp (similar to intersectp-eq and intersectp-equal).

The user now has more control over how ACL2 prints forms; See
PRINT-CONTROL.  Thanks to Bob Boyer for useful discussions leading to
this enhancement.

Some Common Lisp implementations only allow the syntax
pkg-name::expression when expression is a symbol.  The ACL2 reader has
been modified to support a package prefix for arbitrary expressions;
see SHARP-BANG-READER.  Thanks to Hanbing Liu for a query that
led to this feature and to Pascal J. Bourguignon for suggesting an
implmentation.

Ill-formed documentation strings need not cause an error.  See
SET-IGNORE-DOC-STRING-ERROR.  Thanks to Bob Boyer for requesting this
feature.

Type declarations are now permitted in let* forms; see LET*,
see DECLARE, and see TYPE-SPEC.

(For Lisp programmers) Macro with-live-state has been provided for
programmers who refer to free variable STATE, for example with macros
that generate uses of STATE, and want to avoid compiler warnings when
evaluating in raw Lisp.  For example, the following form can be
submitted either inside or outside the ACL2 loop to get the desired
effect (see DOC-STRING): (with-live-state (f-put-global
'doc-prefix " " state)).  For another example use of this macro, see
the definition of trace$ (ACL2 source file other-events.lisp).

(System hackers only) Added :redef- to undo the effect of :redef+.  See
REDEF-.

Function random$ is a built-in random number generator.  See
RANDOM$.  Thanks to Sol Swords for requesting this feature and
providing an initial implementation.

*HEURISTIC IMPROVEMENTS*

Sped up guard generation for some functions with large if-then-else
structures in their bodies.  Thanks to Sol Swords for sending an
illustrative example.

Sped up guard generation in some cases by evaluating ground
(variable-free) subexpressions.  Thanks to Bob Boyer for sending a
motivating example: (defn foo (x) (case x ((1 2) 1) ((3 4) 3) ... ((999
1000) 999))).

Modified slightly a heuristic association of "size" with constants,
which can result in significant speed-ups in proofs involving constants
that are very large cons trees.

Added a restriction in the linear arithmetic procedure for deleting
polynomial inequalities from the linear database.  Formerly, an
inequality could be deleted if it was implied by another inequality.
Now, such deletion requires that certain heuristic "parent tree"
information is at least as restrictive for the weaker inequality as for
the stronger.  Thanks to Dave Greve for bringing a relevant example to
our attention and working with us to figure out some surprising
behavior, and to Robert Krug for making a key observation leading to
the fix.

(GCL especially) Improved compiled code slightly by communicating to
raw Lisp the output type when a function body is of the form (the
character ...).  This tiny improvement will probably only be observed
in GCL, if at all.

Applied a correction suggested by Robert Krug to the variant of
term-order used in parts of ACL2's arithmetic reasoning.

*BUG FIXES*

Fixed bugs in the handling of flet expressions, one of which had the
capability of rendering ACL2 unsound.  Thanks to Sol Swords for
pointing out two issues and sending examples.  One example illustrated
how ACL2 was in essence throwing away outer flet bindings when
processing an inner flet.  We have exploited that example to prove a
contradiction, as follows: this book was certifiable before this fix.

     (in-package "ACL2")

     (defun a (x)
       (list 'c x))

     ; Example from Sol Swords, which failed to be admitted (claiming that
     ; function A is undefined) without the above definition of A.
     (defun foo1 (x y)
        (flet ((a (x) (list 'a x)))
          (flet ((b (y) (list 'b y)))
            (b (a (list x y))))))

     (defthm not-true
       (equal (foo1 3 4)
              '(b (c (3 4))))
       :hints (("Goal"
                :in-theory
                (disable (:executable-counterpart foo1))))
       :rule-classes nil)

     (defthm contradiction
       nil
       :hints (("Goal" :use not-true))
       :rule-classes nil)

Sol's second example, below, pointed to a second bug related to
computing output signatures in the presence of nested flet expressions,
which we have also fixed: this form failed before the fix.

     :trans (flet ((foo (a) (list (flet ((bar (b) b)) a)))) x)

Fixed a subtle soundness bug in the forming of constraints from deduced
type prescriptions.  As a result, when ACL2 prints a warning message
labeling encapsulated functions as "subversive", ACL2 will no longer
deduce :type-prescription rules for those functions.  Examples that
exploit the bug in ACL2 Version_3.4 may be found in comments in ACL2
source function convert-type-set-to-term (file other-processes.lisp) and
especially in function putprop-type-prescription-lst (file
defuns.lisp).  For more on the general issue of "subversive
recursions," see SUBVERSIVE-RECURSIONS.)

Fixed a soundness bug in the handling of inequalities by the type-set
mechanism, which was using the inequality database inside the body of a
lambda.

Fixed a long-standing soundness bug in compress1 and compress2, whose
raw Lisp code gave the logically incorrect result in the case of a
single entry other than the header, where that entry mapped an index to
the default value.  Also fixed soundness bugs in compress1, in the case
of :order >, where the raw Lisp code could drop the header from the
result or, when the input alist had entries in ascending order, fail to
return an alist in descending order.  For example, the following book
certified successfully.

     (in-package "ACL2")
     (defthm true-formula-1
       (equal (compress1 'a '((:HEADER :DIMENSIONS (4) :MAXIMUM-LENGTH 5
                                       :DEFAULT 1 :NAME A :ORDER <)
                              (1 . 1)))
              '((:HEADER :DIMENSIONS (4) :MAXIMUM-LENGTH 5
                         :DEFAULT 1 :NAME A :ORDER <)))
       :hints (("Goal" :in-theory (disable (compress1))))
       :rule-classes nil)
     (defthm ouch-1
       nil
       :hints (("Goal" :use true-formula-1))
       :rule-classes nil)
     (defthm true-formula-2
       (equal (compress1 'a '((:HEADER :DIMENSIONS (4) :MAXIMUM-LENGTH 5
                                       :DEFAULT NIL :NAME A :ORDER >)
                              (1 . 1)
                              (2 . 2)))
              '((:HEADER :DIMENSIONS (4) :MAXIMUM-LENGTH 5
                         :DEFAULT NIL :NAME A :ORDER >)
                (2 . 2)
                (1 . 1)))
       :hints (("Goal" :in-theory (disable (compress1))))
       :rule-classes nil)
     (defthm ouch-2
       nil
       :hints (("Goal" :use true-formula-2))
       :rule-classes nil)
     (defthm true-formula-3
       (equal (compress1 'a '((:HEADER :DIMENSIONS (3) :MAXIMUM-LENGTH 4
                                       :NAME A :ORDER >)
                              (1 . B)
                              (0 . A)))
              '((:HEADER :DIMENSIONS (3) :MAXIMUM-LENGTH 4
                         :NAME A :ORDER >)
                (1 . B)
                (0 . A)))
       :hints (("Goal" :in-theory (disable (compress1))))
       :rule-classes nil)
     (defthm ouch-3
       nil
       :hints (("Goal" :use true-formula-3))
       :rule-classes nil)

Fixed a soundness bug involving measured subsets and verify-termination,
by changing verify-termination so that it uses make-event.  See
VERIFY-TERMINATION, in particular the discussion about make-event
near the end of that documentation topic.  Peter Dillinger first raised
the idea to us of making such a change; when we found this soundness
bug, we were certainly happy to do so!

Fixed a bug that could cause a hard Lisp error but not, apparently,
unsoundness.  The bug was in the lack of attention to the order of
guard and type declarations when checking for redundancy.  In the
following example, the second definition was redundant during the first
pass of the encapsulate form.  The second definition, however, was
stored on the second pass with a guard of (and (consp (car x)) (consp
x)), which caused a hard Lisp error when evaluating (foo 3) due to a
misguided attempt to evaluate (car 3) in raw Lisp.  The fix is to
restrict redundancy of definitions so that the guard and type
declarations must be in the same order for the two definitions.

     (encapsulate
      ()
      (local (defun foo (x)
               (declare (xargs :guard (consp x)))
               (declare (xargs :guard (consp (car x))))
               x))
      (defun foo (x)
        (declare (xargs :guard (consp (car x))))
        (declare (xargs :guard (consp x)))
        x))
     ; Now we get a hard Lisp error from evaluation of the guard of foo:
     (foo 3)

Fixed a bug in the guard violation report for function
intern-in-package-of-symbol.  Thanks to Dave Greve for bringing this
bug to our attention.

Made a change to allow certain hints, in particular certain
:clause-processor hints, that had previously caused errors during
termination proofs by viewing the function being defined as not yet
existing.  Thanks to Sol Swords for bringing this issue to our
attention with a nice example.

ACL2 now properly handles interrupts (via control-c) issued during
printing of the checkpoint summary.  Previously it was possible on some
platforms to make ACL2 hang when interrupting both during a proof and
during the ensuing printing of the checkpoint summary.  Thanks to Jared
Davis and Sol Swords for bringing this problem to our attention.

Fixed a bug that was preventing, inside some book "b", the use of a
:dir argument to include-book that refers to a directory defined using
add-include-book-dir earlier in the book "b".  (We found this
ourselves, but we thank John Cowles for observing it independently and
sending us a nice example.)

(GCL and CCL only) Fixed a bug in certain under-the-hood type
inferencing.  Thanks to Sol Swords for sending an example using stobjs
defined with the :inline keyword, along with a helpful backtrace in
CCL, and to Gary Byers for his debugging help.

Fixed a bug in print-gv, which was mishandling calls of functions with
more than one argument.

Fixed a bug in the handling of AND and OR terms by the proof-checker
command DV, including numeric ("diving") commands.  Thanks for Mark
Reitblatt for bringing this problems to our attention with a helpful
example.

Fixed printing of goal names resulting from the application of :OR
hints so that they aren't ugly when working in other than the "ACL2"
package.  Thanks to Sol Swords for bringing this issue to our attention.

Fixed proof-tree printing so that interrupts will not cause problems
with hiding ordinary output because of incomplete proof-tree output.
Thanks to Peter Dillinger for pointing out this issue.

Fixed a hard error that could be caused by mishandling a forced
hypothesis during forward-chaining.  Thanks to Peter Dillinger for
bringing this bug to our attention by sending a useful example.

Fixed a bug that could cause simplifications to fail because of alleged
"specious simplification."  This bug could appear when deriving an
equality from the linear arithmetic database, and then attempting to
add this equality to the current goal's hypotheses when it was already
present.  Thanks to Eric Smith for sending a helpful example (in July
2005!) that helped us debug this issue.

Fixed a bug in processing of :type-set-inverter rules.

Fixed a bug that was causing an error, at least for an underlying Lisp
of CCL (OpenMCL), when ec-call was applied to a term returning multiple
values.  Thanks to Sol Swords for sending an example that brought this
bug to our attention.

Fixed handling of array orders to treat keyword value :order :none
correctly from an array's header.  Previously, there were two problems.
One problem was that :order :none was treated like the default for
:order, <, while :order nil was treated in the manner specified by
:order :none (see ARRAYS).  Now, both :order :none and :order
nil are treated as :order nil had been treated, i.e., so that there is
no reordering of the alist by compress1.  The other problem with this
case of :order was that the :maximum-length field of the header was not
being respected: the length could grow without bound.  Now, as
previously explained (but not previously implemented) -- see
ARRAYS -- a compress1 call made on behalf of aset1 causes a hard
error if the header of the supplied array specifies an :order of :none
or nil.

An ignorable declare form had caused an error in some contexts when it
should have been allowed.  In particular, this problem could arise when
using an ignorable declaration at the top level in a defabbrev form.
It could also arise upon calling verify-termination when the
corresponding defun form contained an ignorable declaration at the top
level.  These bugs have been fixed.

Contrary to existing documentation (see MAKE-EVENT-DETAILS),
the value of "ld special variable" ld-skip-proofsp was always set to nil
during make-event expansion, not merely when the make-event form has a
non-nil value for keyword parameter :check-expansion.  This has been
fixed.  Thanks to Sol Swords for bringing this issue to our attention.

We have disallowed the certification of a book when not at the
top-level, either directly in the top-level loop or at the top level of
ld.  Before this restriction, the following would certify a book with a
definition such as (defun foo (x) (h x)) that calls function h before
defining it, if the certification was by way of the form such as:

     (er-progn (defun h (x) x) (certify-book "my-book"))

But a subsequent include-book of "my-book" would then fail, because h
is not defined at the top level.

Printing with fmt directive ~c now works properly even when the
print-base is other than 10.  Thanks to Sol Swords for reporting this
bug and providing a fix for it.

(SBCL, CMUCL, and CCL only) Fixed a bug in sys-call-status in the case
that the underlying Common Lisp is SBCL, CMUCL, or CCL (OpenMCL).
Thanks to Jun Sawada for bringing this bug to our attention and
providing a fix.

Fixed a bug that was preventing local defstobj events in encapsulate
events.  Thanks to Jared Davis for bringing this bug to our attention.

Fixed a bug evidenced by error message "Unexpected form in certification
world", which could result from attempting to certify a book after
evaluating an encapsulate form with a local defmacro.  Thanks to Jared
Davis for pointing out ths bug and sending the example:

     (encapsulate
      ()
      (local (defmacro foo (x) `(table foo 'bar ,x)))
      (local (foo 3)))

Formerly, evaluating a trace$ form inside a wormhole such as the
break-rewrite loop could leave the user in a bad state after returning
to the top level, in which that function could not be untraced.  This
has been fixed.  Note however that when you proceed from a break in the
break-rewrite loop, the tracing state will be the same as it was when
you entered that break: all effects of calling trace$ and untrace$ are
erased when you proceed from the break.

A :guard of (and) is no longer ignored.  Thanks to Sol Swords for
bringing this bug to our attention.

A bug has been fixed that could result in needlessly weak induction
schemes in the case that a recursive call is made in the first argument
of prog2$.  This has been fixed by including prog2$ as a default
ruler-extender in the new ruler-extenders feature (see above, and see
RULER-EXTENDERS).  For details on this bug see Example 11 in
distributed book books/misc/misc2/ruler-extenders-tests.lisp.

(For CCL/OpenMCL on Windows) ACL2 should now build on CCL (OpenMCL) on
Windows.  Thanks to David Rager for bringing this issue to our
attention and helping with a fix that worked for CCL 1.2, and to the
CCL team for improving handling of Windows-style filenames in CCL 1.3.

*NEW AND UPDATED BOOKS*

See `http://code.google.com/p/acl2-books/wiki/BooksSince34' for a list
of books in Version  3.5 of ACL2 but not Version  3.4.

Run the shell command

     svn log -r 94:HEAD

to see all changes to books/ since the release of Version  3.4.

Here are just a few highlights.

Thanks largely to Jared Davis, many Makefiles have been improved to do
automatic dependency analysis.  See BOOK-MAKEFILES for how to
get your own Makefiles to do this by adding a line: -include
Makefile-deps.

Libraries books/arithmetic-4/ and books/rtl/rel7/ have been eliminated
from the default book certification (make regression), in favor of new
libraries books/arithmetic-5/ and books/rtl/rel8/ contributed by Robert
Krug and Hanbing Liu, respectively.  They and Jun Sawada have arranged
the compatibility of these libraries; i.e., it is possible to evaluate
both of the following in the same session:

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

Library books/rtl/rel1/ is no longer certified by default (though it is
still distributed in support of ACL2(r); see REAL).

*EMACS SUPPORT*

Slightly modified Control-t e (defined in emacs/emacs-acl2.el) to
comprehend the notion of an "ACL2 scope", and added Control-t o to
insert a superior encapsulate defining such a scope.  See the Emacs
documentation for Control-t e (generally obtained after typing
Control-h k).

Modified distributed file emacs/emacs-acl2.el so that if you put the
following two forms in your ~/.emacs file above the form that loads
emacs/emacs-acl2.el, then Emacs will not start up a shell.  Thanks to
Terry Parks for leading us to this modification.

     (defvar acl2-skip-shell nil)
     (setq acl2-skip-shell t)

*EXPERIMENTAL HONS VERSION*

Bob Boyer and others have contributed numerous changes for the
experimental "hons" version of ACL2 (see HONS-AND-MEMOIZATION).

The ACL2 state can now be queried with (@ hons-enabled) so that a
result of t says that one is in the experimental hons version, while
nil says the opposite.

NOTE-3-5(R)    ACL2 Version  3.5(r) (May, 2009) Notes

Please also see NOTE-3-5 for changes in Version  3.5 of ACL2.

This release incorporates improvements from Ruben Gamboa in support for
non-standard analysis in ACL2(r), in the following ways:

ACL2(r) now supports non-classical objects that are not also numeric,
e.g., non-classical cons pairs.  Consequently, the built-in
standard-numberp has been replaced with standardp.

If f is a classical function, the value (f x1 ... xn) is guaranteed to
be standard when the xi are standard.  ACL2(r) can now recognize this
fact automatically, using defun-std.  For example, the following can be
used to assert that the square root of 2 is a standard value.

     (defthm-std sqrt-2-rational
       (standardp (acl2-sqrt 2)))

More generally, the expression (f x1 ... xn) can contain free variables,
but the result is guaranteed to be standard when the variables take on
standard variables, as in the following:

     (defthm-std sqrt-x-rational
       (implies (standardp x)
                (standardp (acl2-sqrt x))))

A potential soundness bug in encapsulate was fixed.  Specifically, when
a classical, constrained function is instantiated with a lambda
expression containing free variables, it may produce non-standard
values depending on the values of the free variables.  This means that
the functional instantiation cannot be used to justify a non-classical
theorem.  For example, consider the following sequence:

     (encapsulate
       ((f (x) t))
       (local (defun f (x) x)))
     (defthm-std f-x-standard
       (implies (standardp x)
                (standardp (f x))))
     (defthm plus-x-standard
       (implies (standardp x)
                (standardp (+ x y)))
       :hints (("Goal"
                :use ((:functional-instance f-x-standard
                                            (f (lambda (x) (+ x y))))))))
     (defthm plus-x-eps-not-standard
       (implies (standardp x)
                (not (standardp (+ x (/ (i-large-integer)))))))
     (defthm nil-iff-t
       nil
       :hints (("Goal"
               :use ((:instance plus-x-standard
                                (y (/ (i-large-integer))))
                     (:instance plus-x-eps-not-standard)))))

ACL2(r) also supports the introduction of non-classical functions with
defchoose.  These behave just as normal functions introduced with
defchoose, but they have a non-classical choice property.

Finally, ACL2(r) now comes with a revamped library supporting
non-standard analysis, still distributed separately as books/nonstd/.
The new library uses defchoose to state more natural and useful
versions of the IVT, MVT, etc.  It also supports the introduction of
inverse functions, e.g., logarithms.  Finally, the library has much
more extensive support for differentiation.

NOTE-3-6    ACL2 Version  3.6 (August, 2009) Notes

NOTE!  New users can ignore these release notes, because the
documentation has been updated to reflect all changes that are recorded
here.

Below we roughly organize the changes since Version  3.5 into the
following categories of changes: existing features, new features,
heuristic improvements, bug fixes, distributed books, Emacs support,
and experimental hons-and-memoization version.  Each change is
described in just one category, though of course many changes could be
placed in more than one category.

Note that (starting with ACL2 Version  3.5) Lispworks is no longer
supported as a platform for ACL2, as the Lispworks compiler could not
handle the ACL2 sources; see comments in the ACL2 sources about
"function size" being "too large".

*CHANGES TO EXISTING FEATURES*

In the xargs declare form, the function symbol (or symbols, plural, in
the case of mutual-recursion) being defined may now be used in the
specified :measure and :guard terms.  Note that, the definition(s) of
the new symbol(s) are still not used in the termination proof.  Thanks
to Daron Vroon for discussions leading to this addition for the measure
and to Dave Greve for requesting such an enhancement for the guard.

Processing of the :guard-hints in an xargs declare form is now delayed
until the start of guard verification.  As a result, the function
symbol(s) being defined may now be used as one might expect in such
hints, for example in an :in-theory form.  Thanks to Jared Davis for
suggesting that we make such an improvement and providing an example.

Made a low-level change to make-event in support of the ACL2s utility
"dynamic-make-event".  Thanks to Peter Dillinger for explaining the
issue leading to this change.

Modified the failure message printed when a measure conjecture fails to
be proved, to indicate whether or not the hint :ruler-extenders :all
would create a different measure conjecture.  Thanks to Peter Dillinger
for suggesting such a modification.

A call of add-default-hints had added hints to the end of the current
list of default hints.  Now, it adds them to the beginning of that
list, so that they are tried first.  However, add-default-hints now
takes a keyword argument, :at-end.  If that argument is supplied and
evaluates to other than nil, then the previous behavior occurs.

When save-exec is used to save ACL2 images, the build dates are now
printed on separate lines at startup and in the executable script.
Thanks To Bob Boyer for requesting some newlines.

Forward-chaining rules are now generated so that every let (also let*
and lambda) expression is expanded away, as is every call of a
so-called "guard holder" (must-be-equal, prog2$, ec-call, the).  These
were formerly only expanded away in the conclusion.  Thanks to Konrad
Slind for a helpful email leading to this change.

Current-theory now causes a hard error when applied to a name not found
in the current ACL2 logical world, rather than simply returning nil.

When the underlying Common Lisp is GCL, ACL2 no longer uses the #n=
reader macro when writing out certain files, including certificate
files.  In all other Lisps, it now uses the #n= "print-circle" feature
not only for certificate files and "expansion.lsp" files written for
example in support of make-event, but also for files written in support
of :comp.  This is all managed with new state global variable
print-circle-files; see PRINT-CONTROL.  Thanks to Dave Greve
for pointing out that GCL is limited by default to 1024 indices for #n=.

*NEW FEATURES*

A documentation topic explains in some detail how hints work with the
ACL2 proof "waterfall": see HINTS-AND-THE-WATERFALL.  This
topic may be useful to those who write computed hints (see
COMPUTED-HINTS) or other advanced hints.

Added a new hint keyword, :no-thanks, that avoids printing the usual
"Thanks" message for hints.  Thanks to Peter Dillinger for requesting
this feature.

Added a new hint keyword, :backtrack, that checks the goals produced by
processing a goal, and can cause the goal to be re-processed using a new
hint.  See HINTS.  Thanks to Pete Manolios for a conversation
that led to the idea of this hint.

Added a new class of hints, override-hints, that is similar to
default-hints, except that override-hints are always applied, even if
the user has supplied a hint explicitly for the goal.  See
OVERRIDE-HINTS.  Thanks to Pete Manolios and Harsh Raju Chamarthi for
useful discussions on this topic, including its application to testing.

When a goal ready to be pushed for proof by induction is given the new
hint ":do-not-induct :otf", it is indeed pushed for proof by induction,
rather than causing immediate failure as in the case of the hint
":do-not-induct t".  Instead, the proof fails when the goal is later
picked to be proved by induction.  Thanks to Peter Dillinger for
discussions leading to this feature.

Related to computed hints only: Each history entry in the list stored in
variable HIST (see COMPUTED-HINTS) now has a :CLAUSE field,
which provide's access to a goal's parent, parent's parent, and so on
(within the same induction and forcing round only).

It is now possible to inhibit warnings produced by in-theory events and
hints that occur when certain built-in definitions and
executable-counterparts are disabled: just evaluate (assign
verbose-theory-warning nil).  Thanks to Jared Davis (and probably
others in the past) for requesting such a mechanism.

*HEURISTIC IMPROVEMENTS*

A source function (linearize-lst) was replaced by tail-recursive code,
which can avoid a stack overflow.  Thanks to Dave Greve for sending a
helpful example.

The heuristics for limiting forward-chaining have been slightly relaxed,
to allow derivations based on the occurrence of all arguments of the
forward-chaining rule's conclusion in the goal (after stripping leading
calls of NOT).  Thanks to Dave Greve for contributing this improvement
and providing a motivating example.

We simplified induction schemes by eliminating each hypothesis of the
form (not (equal term (quote const))) for which some other hypothesis
in the same case equates term with some (presumably other) quoted
constant.  Thanks to Dave Greve for requesting an improvement of this
sort.

*BUG FIXES*

Fixed a soundness bug related to redundancy of encapsulate events (see
REDUNDANT-EVENTS) and ruler-extenders.  A proof of nil in ACL2
Version  3.5 appears in a comment in (deflabel note-3-6 ...) in the ACL2
source code.  The fix is to insist that in order for one encapsulate
event to be redundant with another, they must be evaluated with the same
default-ruler-extenders.  Analogous to this issue of
default-ruler-extenders for encapsulates is an issue of the
default-verify-guards-eagerness, which has similarly been fixed.

Fixed soundness bugs related to the handling of subversive-recursions
for constraints.  Proofs of nil in ACL2 Version  3.5 appear in a
comment in (deflabel note-3-6 ...) in the ACL2 source code.

Fixed a bug that could cause the following error during calls of
certify-book in the presence of calls of skip-proofs in the book:

        ACL2 Warning [Skip-proofs] in

        HARD ACL2 ERROR in FMT0: Illegal Fmt Syntax.  The tilde-@ directive at
        position 0 of the string below is illegal because its variable evaluated
        to 0, which is neither a string nor a list.

        "~@0"

Thanks to Dave Greve for reporting this bug and making available a very
helpful test case.

The :corollary of a rule (see RULE-CLASSES) failed to use the
default-hints of the logical world.  This has been fixed.

(CCL only) We removed a call, for CCL 1.3 (and beyond) only, of foreign
function sync in the closing of output channels.  Thanks to Daron Vroon
for reporting issues with such a call on a non-Intel platform.

Fixed a bug in reporting failures when monitoring rewrite rules with
free variables in the hypotheses, that could cause a hard Lisp error
(from which ACL2 continues, however).  Thanks to Eric Smith for sending
a very helpful example with his bug report.

Fixed the handling of :induct hints, which had thrown away hint
information from parent goals.  For example, the thm form below failed
to prove even though the second hint is in some sense superfluous;
induction occurs automatically at "Goal'" even without the hint on
that.  The failure was due to discarding the hint information on "Goal".

     (in-theory (disable append))
     (thm (equal (cdr (cons a (append (append x y) z))) (append x y z))
          :hints
          (("Goal" :in-theory (enable append))
           ("Goal'" :induct t) ; failed unless this line is commented out
           ))

Fixed a bug in the args command that was failing to show the formals of
primitives (built-in functions like consp that do not come with explicit
definitions).  Thanks to John Cowles for pointing out this bug.  (At a
lower level, the bug was that primitives failed to have 'stobjs-in or
'stobjs-out properties.)

Fixed bugs in the utility supporting moving directories of certified
books, sometimes used in Debian builds (as described in source function
make-certificate-file).  Thanks to Alan Dunn for pointing out such a
bug, in paths associated with defpkg events in portcullis commands in
certificates (which are used for error reporting).  There were also
bugs, now fixed, that prevented renaming some book paths.  Please note
that this mechanism is not guaranteed to be sound; in particular, it
can probably misbehave when macros are used to generate portcullis
events.  However, it seems likely that such issues will be very rare.

Eliminated warnings that could arise when tracing a function with
trace$.  Now, when trace$ is applied to a function without option
:native, that function's declarations and documentation are discarded.

Fixed a bug that could cause a failure when building an executable image
using SBCL as the underlying Common Lisp.  Thanks to Jun Sawada for
reporting this failure.  We made a similar fix for CMUCL.

Fixed a bug in save-exec in the case that an absolute pathnanme is
supplied.  Thanks to Jared Davis for bringing this bug to our attention.

Fixed a bug in the use of trace$ with the :native and :multiplicity
options that caused hard errors for some underlying Lisps.

Fixed a bug in the interaction of trace$ and :comp, which caused error
as comp tried to re-trace functions that it temporarily untraced.

*NEW AND UPDATED BOOKS AND RELATED INFRASTRUCTURE*

See `http://code.google.com/p/acl2-books/wiki/BooksSince35' for a list
of books in Version  3.6 of ACL2 but not Version  3.5.  For _changes_ to
existing books rather than _additions_, see the log entries at
`http://code.google.com/p/acl2-books/source/list' starting with revision
r286 up through revision r329.

It is no longer required to specify a value for environment (or `make')
variable ACL2_SYSTEM_BOOKS when running make in the distributed book
directory, even when that directory is not under the directory
containing the ACL2 executable.  Thanks to Peter Dillinger for
providing this improvement, by modifying books/Makefile-generic and, as
needed, distributed book Makefiles.

Thanks to Peter Dillinger, some books in support of the ACL2 Sedan
(ACL2s) are more easily available for ACL2 users who do not use ACL2s.
See ACL2-SEDAN.

*EMACS SUPPORT*

If the following form is evaluated before the load of
emacs/emacs-acl2.el, then variables are now set to reflect the directory
containing that file.

     (if (boundp '*acl2-sources-dir*)
         (makunbound '*acl2-sources-dir*))

Fixed info-dir-entry line in generated info file (by patching
doc/write-acl2-texinfo.lisp).  Thanks to Alan Dunn for providing this
patch.

*EXPERIMENTAL HONS VERSION*

Bob Boyer and others have contributed numerous changes for the
experimental "hons" version of ACL2 (see HONS-AND-MEMOIZATION).
A number of these have been crafted to work specifically with CCL
(Clozure Common Lisp, formerly OpenMCL), which is now required as the
underlying Lisp for the "hons" version of ACL2.

A heuristic (source function too-many-ifs has been made more scalable
(for the non-HONS version as well, in fact), but with no functional
change.  Thanks to Jared Davis for noticing performance issues and
suggesting fixes.

Other changes including the following, quoting Bob Boyer:

     The CCL CASE macro now does better than a dumb linear search in
     some CASEes.

     SH and CSH are functions to talk to the underlying Gnu-Linux from
     CCL.  Good for repeated calling when you simply cannot afford the
     copying cost of a FORK because you are using, say, a dozen
     gigabytes.

     Added CCL compiler-macros for IF and OR, to support some
     'coverage' analysis, cf. IF-REPORT, extending the profiling.

     Introduced the type 'mfixnum' so that things like counting honses
     and counting calls to memoized or profiled functions can run fast
     in CCL 64 bits and yet still run at all under 32 bits.

     Moved all HONSes to CCL's newish static space, which permits the
     address of a cons to be used as a hash key, as in most Lisps.
     (CCL moves most conses and most everything when it does a
     compacting-gc.)

     Quite a few changes in the memoize-fn reporting.

     Added a timer facility, cf. call-with-timeout.  Good for running
     under throttle some gross thoughts like 'Is it true that you can't
     fit 12 pigeons into 11 holes' on some propositional calculus
     systems/functions.

     Added rwx-size, pid-owner-cmdlines, rss, and proc-stat to help see
     what is really going on virtually in Gnu-Linux.

     Fixed at least one bug in compact-print-file and helped make its
     integration into ACL2's read-object$ a little more sound.  Still
     worried some about *print-readably* vs. readtable-case.  Does
     anyone else stay awake late at night worrying about readtable-case?

     Revised how the *watch-dog-process* interrupts the main process
     for the thousandth time, cf. watch.  Haven't changed it in weeks,
     which means that (a) it is getting tolerable or (b) I've run out
     of gas.

NOTE-3-6(R)    ACL2 Version  3.6(r) (August, 2009) Notes

Please also see NOTE-3-6 for changes in Version  3.6 of ACL2.

NOTE-3-6-1    ACL2 Version  3.6.1 (September, 2009) Notes

NOTE!  New users can ignore these release notes, because the
documentation has been updated to reflect all changes that are recorded
here.

The essential changes to ACL2 since Version  3.6 are the two bug fixes
described below.  There was also some functionality-neutral code
refactoring, as requested by Daron Vroon in support of the ACL2 Sedan
(see ACL2-SEDAN).  Also see
`http://code.google.com/p/acl2-books/wiki/BooksSince36' for a list of
books in Version  3.6.1 of ACL2 but not Version  3.6.  For _changes_ to
existing books rather than _additions_, see the log entries at
`http://code.google.com/p/acl2-books/source/list' starting with
revision r329 up through revision 350.

Fixed a soundness bug in the handling of ruler-extenders, specifically
in the handling of LET-expressions.  Thanks to Pete Manolios, who sent
us a proof of nil, essentially as follows.  In the termination proof for
foo below, the binding of x to (cons t x) was not substituted into the
recursive call of foo for purposes of the termination proof.

     (defun foo (x)
       (declare (xargs :ruler-extenders :all))
       (let ((x (cons t x)))
         (if (endp (cdr x))
             x
           (cons t (foo (cdr x))))))

     (defthm foo-bad
       nil
       :hints (("Goal"
                :use ((:instance foo (x '(3))))
                :in-theory (disable foo (foo))))
       :rule-classes nil)

Fixed a typo in code supporting ruler-extenders (specifically, swapped
arguments in a recursive call of ACL2 source function
get-ruler-extenders2, which could cause problems for functions defined
using mutual-recursion).  Thanks to Daron Vroon for bringing this bug
to our attention, pointing out the swapped arguments.

NOTE-4-0    ACL2 Version  4.0 (July, 2010) Notes

NOTE!  New users can ignore these release notes, because the
documentation has been updated to reflect all changes that are recorded
here.

Below we roughly organize the changes since Version  3.6.1 into the
following categories of changes: existing features, new features,
heuristic improvements, bug fixes, distributed books, Emacs support,
and experimental versions.  Each change is described in just one
category, though of course many changes could be placed in more than
one category.  Also see NOTE-3-6-1 for other changes since
Version  3.6.

*CHANGES TO EXISTING FEATURES*

There have been extensive changes to the handling of compiled files for
books, which may generally be invisible to most users.  The basic idea
is that when compiled files are loaded on behalf of include-book, they
are now loaded before events in the book are processed, not afterwards.
This can speed up calls of include-book, especially if the underlying
Lisp compiles all definitions on the fly (as is the case for CCL and
SBCL).  One functional change is that for keyword argument
:load-compiled-file of include-book, the values :comp-raw, :try, and
:comp! are no longer legal.  (Note that the handling of :comp-raw was
actually broken, so it seems that this value wasn't actually used by
anyone; also, the handling of :comp! formerly could cause an error in
some Lisp platforms, including SBCL.)  Another change is that if
include-book is called with :load-compiled-file t, then each sub-book
must have a compiled file or a so-called "expansion file"; see
BOOK-COMPILED-FILE.  In the unlikely event that this presents a
problem, the makefile provides a way to build with compilation
disabled; see COMPILATION.  Users of raw mode (see
SET-RAW-MODE) will be happy to know that include-book now works if
there an up-to-date compiled file for the book, since portcullis
commands are now incorporated into that compiled file.  The mechanism
for saving expansion files has changed, and the :save-expansion
argument of certify-book has been eliminated; see CERTIFY-BOOK.
More discussion of ACL2's new handling of book compilation is
described in a new documentation topic; see BOOK-COMPILED-FILE.

It was possible to get a hard Lisp error when certifying a book with a
redundant defconst form whose term is not identical to the existing
defconst form for the same name.  The following example illustrates the
problem, which has been fixed (as part of the change in handling of
compiled files for books, described above).  Imagine that after the
initial (in-package "ACL2") form, file foo.lisp has just the form
(defconst *a* (append nil nil)).  Then before the fix, we could have:

       ACL2 !>(defconst *a* nil)
       [[output omitted]]
       ACL2 !>(certify-book "foo" 1)
       [[initial output omitted]
       * Step 5:  Compile the functions defined in "/v/joe/foo.lisp".
       Compiling /v/joe/foo.lisp.
       End of Pass 1.
       End of Pass 2.
       OPTIMIZE levels: Safety=0 (No runtime error checking), Space=0, Speed=3
       Finished compiling /vjoe/foo.lisp.
       Loading /v/joe/foo.lisp

       Error: Illegal attempt to redeclare the constant *A*.

The wormhole facility has been changed to repair a bug that allowed
guard violations to go undetected.  The major change has to do with the
treatment of what used to be called the "pseudo-flag" argument which has
been replaced by a quoted lambda expression.  See
NOTE-4-0-WORMHOLE-CHANGES for help in converting calls of wormhole.
Also see see WORMHOLE and see WORMHOLE-EVAL.

The function assign-wormhole-output has been eliminated but its
functionality can be provided by wormhole-eval.

The ACL2 tutorial has been greatly expanded, for example to include a
self-contained discussion of rewriting.  See ACL2-TUTORIAL.

Formerly, the mbe macro and must-be-equal function were disallowed in
any definition within an encapsulate having a non-empty signature.
Now, these are allowed provided the definition has been declared to be
non-executable (see DEFUN-NX).  As a result, defevaluator
events may now include must-be-equal among the function symbols known
by the evaluator; this had not previously been allowed.  Thanks to Sol
Swords for discussions leading to this relaxation for defevaluator.

Princ$ now prints strings more efficiently.  Thanks to Jared Davis for
suggesting the improvements to princ$.

The use of xargs declaration :non-executable t no longer requires the
absence of state or declared stobjs among the formal parameters of a
function definition.  As before, the use of :non-executable t turns off
single-threadedness checking for the body, and also as before, attempts
to execute the function will fail.  Thanks to Sol Swords for requesting
this relaxation (for automatic generation of so-called "flag functions"
for definitions using mutual-recursion).

The documentation has been improved for explaining to advanced users the
details of the ACL2 hint mechanism; see
HINTS-AND-THE-WATERFALL, and see the example about
nonlinearp-default-hint in distributed book
books/hints/basic-tests.lisp.  Thanks to Robert Krug for useful
discussions, in particular suggesting the above example as one to be
explained with the documentation.

The time$ macro has been enhanced to allow user control of the timing
message that is printed, and of when it is printed.  See TIME$.
Thanks to Jared Davis for providing the essential design, helpful
documentation (largely incorporated), and an initial implementation for
raw Lisp.

The :ttags argument to include-book had been required when including a
certified book that uses trust tags.  This is no longer the case:
essentially, :ttags defaults to :all except that warnings will be
printed.  Thanks to Jared Davis for requesting such a relaxation, and
to him and Sandip Ray for useful discussions.

The definition of mv-let has been modified so that the single-step
macroexpansion (see TRANS1) of its calls can be evaluated.
Thanks to Pete Manolios for bringing this evaluation issue to our
attention and ensuing discussions.

All calls of so-called "guard-holders" -- prog2$, must-be-equal (from
calls of see MBE), ec-call, and mv-list -- are now removed
before storing hypotheses of rules of class :rewrite or :linear.
Thanks to Sol Swords for requesting this enhancement and sending the
following example in the case of rewrite rules.

     (defthm foo
       (prog2$ (cw "asdf")
               (and (equal (car (cons x y)) x)
                    (equal (cdr (cons x y)) y))))

The handling of fmt directive ~s has been modified so that if the
argument is a symbol that would normally be printed using vertical bars
(|), then that symbol is printed as with ~f.  Thanks to Jared Davis for
providing the following example showing that treatment of ~s was a bit
unexpected: (cw "~s0.~%" '|fo\|o|).

Error messages have been improved for ill-formed terms (in ACL2's
so-called "translation" routines).  Thanks to Jared Davis for
requesting such an enhancement.

Modified defun-sk so that it executes in :logic mode.  Previously,
evaluation of a defun-sk event in :program mode caused a somewhat
inscrutable error, but now, :program mode is treated the same as :logic
mode for purposes of defun-sk.

The "system hacker" commands (redef+) and (redef-) are now embedded
event forms (see EMBEDDED-EVENT-FORM), hence may be used in
books as well as in progn and encapsulate events.  Also, these two
commands are now no-ops in raw Lisp.

The function symbol worldp (in the "ACL2" package) has been renamed to
plist-worldp.

The function gc$-fn (resulting from macroexpansion of gc$) is now in
:logic mode.  Thanks to Jared Davis for requesting this change.

The user now has control over whether compilation is used, for example
whether or not certify-book compiles by default, using function
set-compiler-enabled.  See COMPILATION.

Modified the conversion of relative to absolute pathnames in portcullis
commands for book certification.  Now, more pathnames remain as relative
pathnames.

The "Ttags" warning that can be printed by include-book is now given
even if set-inhibit-output-lst has specified `warning'.  To suppress
it, specify warning! instead, for example, (set-inhibit-output-lst
'(acl2::warning! acl2::proof-tree)).

On occasion, ACL2 prints the message "Flushing current installed world"
as it cleans up when certain actions (installing a world) are
interrupted.  This operation has been sped up considerably.  If your
session includes many events, you can probably speed up any such
operation further by invoking reset-prehistory.  Thanks to Jared Davis
for sending a query that led us to make this improvement.

Calls of the form (ec-call (must-be-equal logic exec)) are no longer
allowed, since we do not have confidence that they would be handled
correctly.

The underlying function for good-bye (and hence for exit and quit) is
now in :logic mode.  Thanks to Jared Davis for requesting this
enhancement.

We now require that every function symbol in the signature of an
encapsulate event have a :logic mode definition at the end of the first
pass, not merely a :program mode definition (which formerly was
sufficient).  You can still define such a function in :program mode,
provided it is followed by a :logic mode definition (where of course
both definitions are local, since we are discussing functions is
introduced in the signature).  Thanks to Carl Eastlund for bringing
this issue to our attention.  (Note: An analogous modification has been
made for :bdd hints as well.)

The following functions now have raw Lisp implementations that may run
faster than their ACL2 definitions: assoc-eq, assoc-equal, member-eq,
member-equal, subsetp-eq, subsetp-equal, remove-eq, remove-equal,
position-eq, and position-equal.  Thanks to Jared Davis for suggesting
that we consider such an improvement.

We now avoid infinite loops caused when tracing functions that implement
trace$.  Thanks to Rob Sumners and Eric Smith for useful discussions.

The implementation of trace! has been modified slightly, to accommodate
the fix for "some holes in the handling of trust tags" described later,
below.

This item applies unless the host Lisp is GCL.  An interrupt
(control-c) will now cause a proof to exit normally in most cases, by
simulating a timeout, as though with-prover-time-limit had been called
with a time-limit of 0.  If the first interrupt doesn't terminate the
proof, a second one should do so (because a different, more "severe"
mechanism is used after the first attempt).  As a result, redo-flat
should work as one might expect even if a proof is interrupted.  Thanks
to Dave Greve for requesting this enhancement to redo-flat.  Technical
note: for reasons related to this change, time-limits are no longer
checked in evaluator functions (ev-fncall, ev, ev-lst, ev-fncall-w,
ev-w, and ev-w-lst).

It is now legal for proof-checker macro-commands to appear in
:instructions that are used in place of :hints.  Thanks to Sandip Ray
for (most recently) requesting this feature.

The value of :command-conventions for ld special variable
ld-post-eval-print is now treated as though it were t if the value ld
special variable ld-error-triples is nil.  The following example
illustrates this change.

     ACL2 !>(ld-post-eval-print state) ; default
     :COMMAND-CONVENTIONS
     ACL2 !>(ld-error-triples state) ; default
     T
     ACL2 !>(set-ld-error-triples nil state)
     *** Then, before the change:
     ACL2 !>(mv t 3 state)
      3
     *** Instead, after the change:
     ACL2 !>(mv t 3 state)
     (T 3 <state>)

The default behavior of ld has been changed.  Formerly when an error
occurred that halted a subsidiary call of ld, then the parent ld would
continue.  That is no longer the case.  Consider the following example.

     (ld '((ld '((defun f (x) x)
                 (defun bad (x)) ; ERROR -- missing the body
                 ))
           (defun g (x) x)))

Formerly, g would be defined in the resulting logical world.  Now, the
error halts not only the inner ld but also the outer ld.  See
LD, and for details of the new default value for :ld-error-action,
:RETURN!, see see LD-ERROR-ACTION.  Also see the paragraph
below about a new utility, :p!.  Thanks to Robert Krug and Sandip Ray
for helpful discussions.

Environment variable ACL2-CUSTOMIZATION has been replaced by
ACL2_CUSTOMIZATION -- that is, the hyphen has been replaced by an
underscore -- so that it can be set conveniently in the bash shell.
See ACL2-CUSTOMIZATION.

The "Warnings:" summary is now omitted when there are no warnings,
where formerly "Warnings:  None" was printed.  Thanks to Jared Davis
for suggesting this change.

We have modified the generation of constraints for encapsulate events
in two primary ways, neither of them likely to affect many users.  One
change is that the virtual movement of definitions and theorems to in
front of an encapsulate event, or of definitions to behind that event,
is no longer inhibited in the case of nested encapsulates with non-empty
signatures.  The following example illustrates the other change, as
discussed below.

     (encapsulate
      ((f (x) t))
      (local (defun f (x) x))
      (defun g (x) (cons x (f x)))
      (defun h (x) (g x))
      (defthm h-is-f (equal (car (h x)) x)))

Previously, the constraint on f and h was essentially the conjunction
of the definition of h and the theorem h-is-f.  Now, the definition of
g is conjoined as well; moreover, g receives the same constraint as do
f and h, where previously g was only constrained by its definition.
While we are not aware of a soundness bug caused by the previous
approach, the new approach follows more precisely the intended notion
of constraint.

The use of trace$ (or trace!) option :multiplicity had been required
when option :native was supplied.  This is no longer the case.  Also, a
bug has been fixed that had prevented :multiplicity from working
properly in GCL and Allegro CL.

Several errors have been eliminated that formerly occurred when the
constraints for a function symbol were unknown because it was
constrained using a dependent clause-processor (see
DEFINE-TRUSTED-CLAUSE-PROCESSOR.  Now, it is assumed that the
supporters argument in a define-trusted-clause-processor event is such
that every ancestor of any function symbol constrained by the "promised
encapsulate" of that event among, or ancestral in, those supporters.
Thanks to Sol Swords, Sandip Ray, and Jared Davis for helpful
discussions.

The notion of constraint for functions introduced by defun has been
modified slightly.  No longer do we remove from the body of the
definition calls of so-called "guard-holders": prog2$, must-be-equal,
ec-call, and mv-list, and uses of the-error generated by the.  Also, we
now expand calls of the-error with the same aggressive heuristics
applied to a number of other functions (technically, adding it to the
list *expandable-boot-strap-non-rec-fns*).

*NEW FEATURES*

A new event, defattach, allows evaluation of calls of constrained
(encapsulated) functions.  In particular, users can now, in principle,
soundly modify ACL2 source code; please feel free to contact the ACL2
implementors if you are interested in doing so.  See DEFATTACH.

Eric Smith has noticed that if you exit the break-rewrite loop using
:a! during an ld of a file, then all changes to the logical world are
discarded that were made during that call of ld.  A new utility, :p!,
pops just one level instead, and avoids discarding that work.  (This
change is related to an item above, "The default behavior of ld has
been changed.")  Thanks to Eric for pointing out this issue.

New function mv-list is the identity function logically, but converts
multiple values to lists.  The first argument is the number of values,
so an example form is as follows, where foo returns three values:
(mv-list 3 (foo x y)).  Thanks to Sol Swords for requesting this
feature and for reporting a soundness bug in one of our preliminary
implementations.

A new state global variable, host-lisp, has as its value a keyword
whose value depends on the underlying Common Lisp implementation.  Use
(@ host-lisp) to see its value.

It is now possible to write documentation for HTML without error when
there are links to nonexistent documentation topics.  See the comments
in macro acl2::write-html-file at the end of file
doc/write-acl2-html.lisp.  When there are such errors, they should be
easier to understand than previously.  Thanks to Alan Dunn for
providing the initial modifications.

It is now possible to inhibit specified parts of the Summary printed at
the conclusion of an event.  See SET-INHIBITED-SUMMARY-TYPES.
Also see WITH-OUTPUT, in particular the discussion of the new
:summary keyword.  Thanks to Sol Swords for requesting more control
over the Summary.

A new :hints keyword, :case-split-limitations, can override the default
case-split-limitations settings (see
SET-CASE-SPLIT-LIMITATIONS) in the simplifier.  Thanks to Ian Johnson
for requesting this addition and providing an initial implementation.

It is now possible to defer and avoid some ttag-related output; see
SET-DEFERRED-TTAG-NOTES.  Thanks to Jared Davis for requesting
less verbosity from ttag-related output.

A new command, :pl2, allows you to restrict the rewrite rules printed
that apply to a given term.  See PL2.  Thanks to Robert Krug for
requesting such a capability.

ACL2 now provides a utility for canonicalizing filenames, so that soft
links are resolved; see CANONICAL-PATHNAME.  Moreover, ACL2
uses this utility in its own sources, which can eliminate some issues.
In particular, include-book with argument :ttags :all no longer breaks
when given a book name differing from the book name that was used at
certification time; thanks to Sol Swords for reporting that problem.
Also, certain errors have been eliminated involving the combination of
packages in the certification world and trust tags; thanks to Jared
Davis for sending an example of that problem.

You can now suppress or enable guard-checking for an individual form;
see WITH-GUARD-CHECKING.  Thanks to Sol Swords for requesting
this feature.

The walkabout utility has been documented (thanks to Rob Sumners for
suggesting this documentation).  This utility can make it easy to
explore a large cons tree.  New interactive commands (pp n) and (pp
print-level print-length) have been added to restrict how much of the
current object is displayed.  See WALKABOUT.

Rules of class :type-prescription may now be provided a
:backchain-limit-lst keyword.  The default behavior is unchanged, but
now type-set is sensitive not only to the new :backchain-limit-lst of a
:type-prescription rule (if supplied) but to the
default-backchain-limit of the current logical world.  Setting of
backchain-limits can now specify either the new (type-set) limit or the
old limit (for rewriting); see SET-DEFAULT-BACKCHAIN-LIMIT and
see SET-BACKCHAIN-LIMIT.  Moreover, the functions
default-backchain-limit and backchain-limit now take a second argument
of :ts or :rewrite to specify which backchain-limit is desired.

*HEURISTIC IMPROVEMENTS*

The so-called "too-many-ifs" heuristic has been modified.  Such a
heuristic has been employed in ACL2 (and previous Boyer-Moore provers)
for many years, in order to limit the introduction of calls of IF by
non-recursive functions.  Most users need not be concerned with this
change, but two proofs in the regression suite (out of thousands)
needed trivial adjustment, so user proofs could need tweaking.  In one
application, this modification sped up proofs by 15%; but the change in
runtime for the regression suite is negligible, so such speedups may
vary.  Thanks to Sol Swords for providing a test from ACL2 runs at
Centaur Technology, which was useful in re-tuning this heuristic.

Guard proof obligations could have size quadratic in the number of
clauses in a case statement.  This inefficiency has been removed with a
change that eliminates a hypothesis of the form (not (eql term
constant)) when there is already a stronger hypothesis, equating the
same term with a different constant.  Thanks to Sol Swords for bringing
this problem to our attention and suggesting an alternate approach to
solving it, which we may consider in the future if related efficiency
problems persist.

We adjusted the heuristics for determining induction schemes in the
presence of ruler-extenders, when handling calls of a function symbol
that is a ruler-extender, in either of two cases: either the function
takes only one argument; or the function is prog2$ or ec-call, and the
first argument contains no recursive call.  These cases are treated
more directly as though the ruler-extender call is replaced by the
unique (in the case of prog2$ and ec-call, the second) argument.

A new :type-prescription rule, true-listp-append, has been added:

     (implies (true-listp b)
              (true-listp (append a b)))

If you are interested in the motivation for adding this rule, see
comments in true-listp-append in ACL2 source file axioms.lisp.

The use of :forward-chaining lemmas has been improved slightly.  In
previous versions, a conclusion derived by forward chaining was
discarded if it was derivable by type-set reasoning, since it was
"already provable."  But this heuristic prevented the conclusion from
triggering further forward chaining.  This has been fixed.  Thanks to
Dave Greve for pointing out this problem.

The fundamental utility that turns an IF expression into a set of
clauses has been optimized to better handle tests of the form (equal x
'constant) and their negations.  This eliminates an exponential
explosion in large case analyses.  But it comes at the inconveience of
sometimes reordering the clauses produced.  The latter aspect of this
change may require you to change some Subgoal numbers in proof hints.
We apologize for the inconvenience.

Certification can now run faster (specifically, the compilation phase)
for books with very large structures generated by make-event, when
there is significant sharing of substructure, because of a custom
optimization of the Lisp reader.  Thanks to Sol Swords for bringing
this efficiency issue to our attention.

Jared Davis reported inefficiency in certain make-event evaluation due
to a potentially expensive "bad lisp object" check on the expansion
produced by the make-event.  This check has been eliminated except in
the case that the expansion introduces packages (for example, by
including a book during the expansion phase that introduces packages).
Thanks to Jared for providing a helpful example.

The application of rules of class :induction had the potential to loop
(as commented in ACL2 source function apply-induction-rule).  This has
been fixed.  Thanks to Daron Vroon and Pete Manolios for sending nice
examples causing the loop.

Heuristics have been tweaked so that false goals may be simplified to
nil that had formerly been left unchanged by simplification, perhaps
resulting in useless and distracting proofs by induction.  Thanks to
Pete Manolios for pointing out this issue by sending the following
example: (thm (<= (+ 1 (acl2-count x)) 0)).  (Technical explanation:
When every literal in a clause simplifies to nil, even though we might
not normally delete one or more such literals, we will replace the
entire clause by the false clause.)

Improved the efficiency of the built-in function, take.  Thanks to Bob
Boyer for suggesting this improvement.

ACL2 can now use evaluation to relieve hypotheses when applying
:type-prescription rules.  Thanks to Peter Dillinger and Dave Greve for
requesting this enhancement, and to Robert Krug for a relevant
discussion long ago.

Evaluation has been sped up during theorems for calls of mv-let, by
avoiding repeated evaluation of the expression to which its variables
are bound.  Thanks to Sol Swords for requesting this improvement and
sending an illustrative example.

Modified a heuristic to avoid the opening up non-recursive function
calls on calls of hide involving if-expressions.  For example, the thm
form below is now admitted

     (defun bar (x)
       (cons x x))
     (thm (equal (bar (hide (if a b c)))
          (cons (hide (if a b c)) (hide (if a b c)))))

*BUG FIXES*

Fixed a soundness bug in destructor elimination, which was preventing
some cases from being generated.  Thanks to Eric Smith for reporting
this bug and sending a helpful example.  (Technical detail: the fixes
were in ACL2 source functions apply-instantiated-elim-rule and
eliminate-destructors-clause1, and comments in the former contain Eric's
example.)

Fixed a bug that supported a proof of nil by exploiting the fact that
portcullis commands were not included in check-sum computations in a
book's certificate.  For such a proof of nil, see the relevant comment
in the ACL2 source file ld.lisp under (deflabel note-4-0 ...).

Changed the implementation of add-include-book-dir.  The previous
implementation could allow relative pathnames to be stored in the
portcullis commands of certificates of books, which perhaps could lead
to unsoundness (though we did not try to exploit this to prove nil).
Thanks to Jared Davis for reporting a bug in our first new
implementation.  An additional change to both add-include-book-dir and
delete-include-book-dir is that these now work in raw-mode (see
SET-RAW-MODE).  (Thanks to Dave Greve for suggesting a reduction in
the warnings we produced related to raw-mode.)  Note that it is no
longer permitted to make a direct call of the form (table
acl2-defaults-table :include-book-dir-alist ...); use
add-include-book-dir instead.

Fixed a soundness bug related to xargs keyword :non-executable.  New
macros, defun-nx and defund-nx, have been provided for declaring
functions to be non-executable; see DEFUN-NX.  While we expect
this bug to occur only rarely if at all in practice, the following
example shows how it could be evoked.

       ;;;;;;;;;;;;;;;;;;;;
       ;;; Book sub.lisp
       ;;;;;;;;;;;;;;;;;;;;
       (in-package "ACL2")
       (defun f ()
         (declare (xargs :guard t
                         :non-executable t))
         (mv-let (a b c)
                 (mv 3 4)
                 (declare (ignore a b))
                 c))
       (defun g ()
         (declare (xargs :guard t))
         (prog2$ (mv-let (x y z)
                         (mv 2 3 4)
                         (declare (ignore x y z))
                         nil)
                 (f)))
       (defthm g-nil
         (equal (g) nil)
         :hints (("Goal" :in-theory (disable (f))))
         :rule-classes nil)
       ;;;;;;;;;;;;;;;;;;;;
       ;;; Book top.lisp
       ;;;;;;;;;;;;;;;;;;;;
       (in-package "ACL2")
       (include-book "sub")
       (defthm contradiction
         nil
         :hints (("Goal" :use g-nil))
         :rule-classes nil)

The modification described above pertaining to defun-nx also prevents
execution of non-executable functions that have been traced.  The
following example illustrates the problem; now, the following defun of
g is illegal, and the problem disappears if defun-nx is used instead.

     (defun g (x) ; Use defun-nx to avoid an error after Version_3.6.1.
       (declare (xargs :guard t :non-executable t))
       x)
     (g 3) ; causes error, as expected
     (trace$ g)
     (g 3) ; returned 3 before the bug fix; after fix, causes error as expected

A hard error was possible when attempting to include an uncertified book
containing events of the form (make-event '(local ...)).  This has been
fixed.  Thanks to Sol Swords for bringing this issue to our attention.

Fixed a bug in the heuristic improvement described for Version_3.6 (see
NOTE-3-6) as "We simplified induction schemes...."  The bug had
prevented, in unusual cases such as the following (notice the impossible
case), a proof by induction.

     (defun foo (a x)
       (and (consp x)
            (case a
              (0 (foo (car x) (cdr x)))
              (1 (foo (cdr x) (car x)))
              (0 (foo a (cons x x))))))
     (in-theory (disable (:type-prescription foo)))
     (thm (atom (foo a x)))

Macro cw-gstack did not work with an :evisc-tuple argument.  This has
been fixed by changing cw-gstack so that it now evaluates its
arguments.  Thanks to Sol Swords for bringing this bug to our attention.

Fixed a bug in :pso during the printing of failure messages for
termination proofs.

Fixed a bug in the handling of #. (see SHARP-DOT-READER).
Thanks to Bob Boyer for bringing this bug to our attention.

Replaced a hard Lisp error with a clean error, in certain cases that a
:hints value is erroneously supplied as a non-nil atom.  Example: (thm
(equal x x) :hints 3).

Fixed a bug in the interaction of function tracing with conversion of a
function from :program to :logic mode.  The following example
illustrates what had been wrong.

     (defun f (x)
       (declare (xargs :mode :program))
       (car x))
     (f 3) ; raw Lisp hard error
     (trace$ f)
     (f 3) ; raw Lisp hard error (still)
     (defun f (x) (car x)) ; upgrade f to :logic mode
     (f 3) ; clean guard violation; f is no longer traced
     (trace$) ; uh oh - f is shown as traced
     (untrace$ f)
     (f 3) ; OUCH: hard Lisp error because old :program mode definition of
           ; the executable counterpart (sometimes called *1*f) was restored!

Made a fix so that when building ACL2 with make option ACL2_SAFETY=3,
there will no longer be any safety-0 compiled code generated.  Thanks
to Gary Byers for bringing this bug to our attention.

Fixed a bug in the handling of override-hints that generate custom
keyword hints (see CUSTOM-KEYWORD-HINTS) involving the variable
stable-under-simplificationp.  Thanks to Ian Johnson for bringing this
bug to our attention with explanation that included a helpful example,
included as comment in the ACL2 source code for function
apply-override-hint.

The saved_acl2 script in CLISP could contain unexpected characters where
simple newlines were expected.  Dave Greve found this in a Cygwin
environment on Windows.  Thanks to Dave for reporting this bug and
experimenting with a fix, and thanks to the CLISP folks for providing
helpful information.

Fixed a bug that could make :oops cause an error.  Also, the oops
command can no longer take you back before a reset-prehistory event.

(GCL only) Fixed a bug that could occur when calling trace in raw Lisp
in GCL.

Proof summaries have been improved, so that they account for runes used
in rewriting that takes place when generating goals to be proved in a
forcing round.  Thanks to Jared Davis for sending us an example
illustrating this issue.

Fixed a bug that (at least in CCL) could put extra backslashes (`\') in
a pathname that ACL2 writes out to the executable script created by a
build.  Thanks to Gary Byers for explaining that the CCL behavior is
legal (for our previous use of Common Lisp function merge-pathnames).

We closed some holes in the handling of trust tags (also known as
"ttags"; see DEFTTAG) by include-book.  The following example
illustrates this rather subtle situation.  Consider the following book.

     (in-package "ACL2")
     (make-event
      (er-progn
       (encapsulate
        ()
        (defttag :foo)
        (value-triple "Imagine something bad here!"))
       (value '(value-triple :some-value)))
      :check-expansion t)

Formerly, the following commands succeeded.

     (certify-book "test3" 0 t :ttags :all)
     :u
     (include-book "test3" :ttags nil)

But because of make-event keyword argument :check-expansion t, we know
that the event (defttag :foo) is evaluated by the above include-book
form, and hence the :ttags argument of include-book, above, should have
specified :foo.  The problem was that defttag forms evaluated during
make-event expansion did not contribute to the trust tag information
stored in the book's certificate.  Note: Because of this change, one
should avoid using make-event with :check-expansion t when the
expansion would introduce a defttag event during include-book but not
certify-book time.  For an example illustrating this issue, see
MAKE-EVENT-DETAILS, specifically the new version of the section
labeled "A note on ttags" at the end of that documentation topic.

Closed a small loophole that had the potential, in rare circumstances,
to violate atomicity of under-the-hood updates for ACL2 arrays.

The following example was formerly allowed, but resulted in a
guard-verified function (here, g) whose guard proof obligation is not a
theorem outside the encapsulate event.  We now disallow guard
verification for functions introduced non-locally inside an encapsulate
event unless we determine that the proof obligations hold outside the
encapsulate event as well.

     (encapsulate
      ((f (x) t))
      (local (defun f (x) (declare (xargs :guard t)) (consp x)))
      ;; ERROR!
      (defun g (x)
        (declare (xargs :guard (f x)))
        (car x)))

The use of :comp on stobj functions had potentially caused a hard Lisp
error; for example, this could occur when (defstobj foo fld) was
followed by :comp foop.  This has been fixed.

Fixed a bug that could cause a raw Lisp error when the first argument of
with-local-stobj is not a symbol.

It had been possible to use the reserved keyword
:computed-hints-replacement as the name of a custom keyword hint (see
CUSTOM-KEYWORD-HINTS).  This has been fixed.  Thanks to Dave
Greve, who pointed out a confusing hint error message (which has also
been fixed) that led us to this issue.

Fixed a bug that could cause a hard Lisp error, instead of a graceful
ACL2 error, if keyword :backchain-limit-lst in a rule class is given a
cons that is not a true list, such as (1 . 1).

Eliminated an error that could occur when redefining a function as a
macro and then compiling, as in the example below.

     (defun foo (x) x)
     :redef!
     (defmacro foo (x) x)
     :comp t

Thanks to Eric Smith for sending the above example in his bug report.

Fixed a bug that could result in an assertion when a clause-processor
causes an error.

*NEW AND UPDATED BOOKS AND RELATED INFRASTRUCTURE*

See `http://code.google.com/p/acl2-books/source/list' for a record of
books changed or added since the preceding release, with log entries.

We note in particular the new system/ directory, which begins to specify
ACL2 system code in anticipation of opening the architecture of ACL2
(see DEFATTACH for a relevant tool).  Some system functions
were changed slightly (but with the expectation of not generally
affecting ACL2 behavior) in support of the development of this
directory.  Those interested in contributing to further such efforts
are invited to contact the ACL2 implementors.

New utilities have been provided for certifying most of the distributed
books with more make-level paralellism.  For example, we have obtained
close to a 12x reduction in time by using `make -j 24 regression-fast'
on a 24-processor machine.  For more information see
books/make-targets, or to include the books/workshops in the regression
run, see books/regression-targets.  Thanks to Sol Swords for providing
these nice utilities.

The top-level makefile, GNUmakefile, has been fixed so that the build
processes (which are inherently sequential) will ignore the -j option of
make.  Note that regressions can still, however, be done in parallel, as
the -j option will be passed automatically to the appropriate make
command.

*EMACS SUPPORT*

*EXPERIMENTAL VERSIONS*

The HONS version, supported primarily by Bob Boyer and Warren Hunt (see
HONS-AND-MEMOIZATION), has undergone numerous improvements.  For
example, keyword argument :FORGET is now supported when calling memoize
from within the ACL2 loop, and system function worse-than is memoized
with the :condition that both terms are function applications (clearing
the memo-table after each prover invocation).  Thanks to Jared Davis
and Sol Swords for investigating the memoization of worse-than, and
with suitable condition.  Thanks also to Jared Davis for contributing
structural modifications to the implementation of hons.

David Rager contributed modifications to the parallel version (see
PARALLELISM), which include taking advantage of atomic
increments available at least since Version 1.0.21 of SBCL and Version
1.3 of CCL.

NOTE-4-0-WORMHOLE-CHANGES    how to convert calls of wormhole for Version  4.0

Here we describe how to convert an "old-style" call of wormhole -- that
is, a call suitable for ACL2 versions preceding  4.0 -- in which the
pseudo-flag was t.  In order to convert such a call

     (wormhole t 'name input form ...)

to a new-style call, the following steps must be carried out.  Note
that the wormhole name must always be quoted now.

First, eliminate the first argument, t, and add a new second argument
that is the quoted lambda expression

     '(lambda (whs) (set-wormhole-entry-code whs :ENTER))

Setting the entry code to :ENTER is not necessary if you maintain the
invariant (after initialization) that it is always :ENTER.  In that
case, the simpler quoted lambda will suffice:

     '(lambda (whs) whs)

Second, change the form argument so that instead of talking about the
state-global variable wormhole-output it talks about the state-global
variable wormhole-status.  Look for (@ wormhole-output), (assign
wormhole-output ...), (f-get-global 'wormhole-output ...) and
(f-put-global 'wormhole-output ...) in form and replace them with
expressions involving wormhole-status.

However, remember that the old data stored in wormhole-output is now in
the wormhole-data component of the wormhole-status.  Thus, for example,
an old use of (@ wormhole-output) will typically be replaced by
(wormhole-data (@ wormhole-status)) and an old use of (assign
wormhole-output ...) will typically be replaced by

     (assign wormhole-status (set-wormhole-data (@ wormhole-status) ...))

In summary, an old-style call like

     (wormhole t 'name
               input
               '(...1 (@ wormhole-output) ...2
                 ...3 (assign wormhole-output ...4) ...5)
               ...6)

can become

     (wormhole 'name
               '(lambda (whs) (set-wormhole-entry-code whs :ENTER))
     	    input
               '(...1 (wormhole-data (@ wormhole-status)) ...2
                 ...3 (assign wormhole-status
                             (set-wormhole-data (@ wormhole-status)
                                                ...4) ...5)
               ...6)

In any case, and especially if your wormhole call had a pseudo-flag
other than t, we recommend that you see WORMHOLE.

NOTE-4-0(R)    ACL2 Version  4.0(r) (July, 2010) Notes

Please see NOTE-4-0 for changes in Version  4.0 of ACL2.

NOTE-4-1    ACL2 Version  4.1 (September, 2010) Notes

NOTE!  New users can ignore these release notes, because the
documentation has been updated to reflect all changes that are recorded
here.

Below we roughly organize the changes since Version 4.1 into the
following categories of changes: existing features, new features,
heuristic improvements, bug fixes, distributed books, Emacs support,
and experimental versions.  Each change is described in just one
category, though of course many changes could be placed in more than
one category.

*CHANGES TO EXISTING FEATURES*

The guard associated with calls of the macro, search, has been weakened
so that now, given strings are no longer restricted to contain only
standard characters unless the :test argument is char-equal.

Modified the writing of "hidden defpkg" forms into certificate files
(see HIDDEN-DEFPKG), to support moving certificate files for
distributed books, as is done by ACL2s (see ACL2-SEDAN) and
Debian releases of ACL2.  Thanks to Camm Maguire for reporting a
problem with Debian releases of ACL2 that led to this change.

Expanded the constant *acl2-exports* by adding intersection-equal to
the list.  Thanks to Jared Davis for requesting this change.

The :comp utility now compiles functions that have code conditionalized
for raw Lisp only (presumably because a trust tag was active when they
were defined).  Previously, this was not the case when :comp was
applied to more than a single function symbol.

*NEW FEATURES*

A new macro, top-level, allows evaluation directly in the top level
loop for forms that normally need to be evaluated inside function
bodies, such as with-local-stobj.  See TOP-LEVEL.  Thanks to
Jared Davis for requesting such a utility.

Added count, a Common Lisp function, to ACL2.  In support of that
addition, also added rewrite rule eqlablep-nth.

*HEURISTIC IMPROVEMENTS*

[None this time.]

*BUG FIXES*

We fixed a soundness bug that could occur when a function that returns
multiple values that is called in its own guard.  Thanks to Sol Swords
for reporting this bug and sending a small self-contained example,
which is included in a comment in the function chk-acceptable-defuns1
in ACL2 source file defuns.lisp.

It was possible to cause an error when giving theory hints during
redefinition of functions.  This has been fixed.  Thanks to Ian Johnson
for sending an example that nicely illustrated this problem.

Fixed system function io? for the case that formal parameter commentp
is t and vars is non-empty.  Thanks to David Rager for bringing to our
attention the fact that io? was broken for such a combination of
parameters.

Not exactly a bug fix, but: defun-sk was breaking when a :guard is
specified, so we have improved the documentation (see DEFUN-SK)
to explain how to provide verified guards for a function introduced by
defun-sk.  Thanks to Jared Davis for bringing this issue to our
attention.

Made a fix to the handling of interrupts, which in rare cases might
have left one in a state where all subsequent proof attempts were
labeled as "Aborting due to an interrupt".

Fixed :pso and related utilities, so that when proof output is
redirected to a file, all summary output goes to that file rather than
to the terminal.

(GCL on Windows only) Removed an inappropriate check, resulting in an
error about "pathname-device," that could prevent Windows GCL builds of
ACL2.  Thanks to Camm Maguire for reporting this problem and a helpful
discussion.

(Windows only) Modified the computation of canonical pathnames to avoid
issues of case-insensitivity, in particular for the drive (e.g., "C:"
vs. "c:").  Thanks to Harsh Raju Chamarthi for reporting this issue and
helping with its debugging.

(Windows only) The value of (@ distributed-books-dir) no longer will be
missing the Windows drive prefix, for example, "C:".  Thanks to Harsh
Raju Chamarthi for reporting this issue and helping with its debugging.

*NEW AND UPDATED BOOKS AND RELATED INFRASTRUCTURE*

See `http://code.google.com/p/acl2-books/source/list' for a record of
books changed or added since the preceding release, with log entries.

Modified books/Makefile-generic by adding a new BOOKS_SKIP_COMP
variable, which is used in Makefiles in some subdirectories of books/,
in order to avoid errors when compiling certified books for multiple
Lisps.

*EMACS SUPPORT*

Distributed file emacs/emacs-acl2.el has been modified so that the forms
control-t e and control-t control-e now pick up package markers (see
SHARP-BANG-READER), in the following sense: if the top-level
form is preceded by a line starting with #!, then that line is included
in the inserted string.  Thanks to Jared Davis for suggesting this
enhancement and providing a preliminary implementation.

*EXPERIMENTAL VERSIONS*

For the HONS version there have been some changes to memoize:

     Memoize accepts a new keyword, :recursive, that is a synonym for
     the existing keyword :inline.  Thanks to Sol Swords for requesting
     this addition.  Moreover, it is now enforced that these keywords
     have Boolean values.

     Memoize may now be called on :program mode functions.  Thanks to
     Sol Swords for requesting this enhancement.

     A bug has been fixed.  Now, if memoize is called with a
     :condition-fn (with value other than nil or t), then the guard of
     the memoized function and the :condition-fn must be the same.
     Previously, one could exploit the lack of such a check to get a
     hard Lisp error, for example as follows.

               (defun f (x) (declare (xargs :guard t)) x)
               (defun cf (x) (declare (xargs :guard (consp x))) (car x))
               (memoize 'f :condition-fn 'cf)
               (f 3)

     Memoization is now illegal for built-in functions that use
     underlying raw Lisp in their implementations.  To see why,
     consider the form (gc$), which is a macro call expanding to
     (gc$-fn nil).  Previously, after evaluation of (memoize 'gc$-fn),
     a call of gc$ would no longer call the garbage collector, which
     had been invoked by raw Lisp code.  Now, evaluation of (memoize
     'gc$-fn) causes an error.

NOTE-4-1(R)    ACL2 Version  4.1(r) (September, 2010) Notes

Please see NOTE-4-1 for changes in Version  4.1 of ACL2.

NOTE1    Acl2 Version 1.1 Notes

The new features are extensively documented.  The relevant topics are:

Related topics other than immediate subtopics:

It is especially important to read all of of the documentation for
books before trying to use books.  However, the new :more keyword
command is so handy for reading long documentation strings that we
recommend you start with :doc more if reading at the terminal.  Some
documentation has been written for guards which you might find
interesting.

NOTE2    Acl2 Version 1.2 Notes

Hacker mode has been eliminated and programming mode has been added.
Programming mode is unsound but does syntax checking and permits
redefinitions of names.  See :doc load-mode and :doc g-mode.

The arguments to ld have changed.  Ld is now much more sophisticated.
See LD.

For those occasions on which you wish to look at a large list structure
that you are afraid to print, try (walkabout x state), where x is an
Acl2 expression that evaluates to the structure in question.  I am
afraid there is no documentation yet, but it is similar in spirit to
the Interlisp structure editor.  You are standing on an object and
commands move you around in it.  E.g., 1 moves you to its first
element, 2 to its second, etc.; 0 moves you up to its parent; nx and bk
move you to its next sibling and previous sibling; pp prettyprints it;
q exits returning nil; = exits returning the thing you're standing on;
(= symb) assigns the thing you're standing on to the state global
variable symb.

Several new hints have been implemented, including :by and :do-not.
The old :do-not-generalize has been scrapped in favor of such new hints
as :do-not (generalize elim).  :By lets you say "this goal is subsumed
by" a given lemma instance.  The :by hint also lets you say "this goal
can't be proved yet but skip it and see how the rest of the proof
goes." See HINTS.

NOTE3    Acl2 Version 1.3 Notes

Programming mode has been eliminated.  Instead, all functions have a
"color" which indicates what can be done with the function.  For
example, :red functions can be executed but have no axioms describing
them.  Thus, :red functions can be introduced after passing a simple
syntactic check and they can be redefined without undoing.  But nothing
of consequence can be proved about them.  At the other extreme are
:gold functions which can be executed and which also have passed both
the termination and the guard verification proofs.  The color of a
function can be specified with the new xargs keyword, :color, which, if
omitted defaults to the global setting of ld-color.  Ld-color replaces
load-mode.  Setting ld-color to :red causes behavior similar to the old
:g-mode.  Setting ld-color to :gold causes behavior similar to the old
:v-mode.  It is possible to prototype your system in :red and then
convert :red functions to :blue individually by calling
verify-termination on them.  They can then be converted to :gold with
verify-guards.  This allows us to undertake to verify the termination
and guards of system functions.  See :doc color for an introduction to
the use of colors.

Type prescription rules have been added.  Recall that in Nqthm, some
rewrite rules were actually stored as "type-prescriptions."  Such rules
allow the user to inform Nqthm's primitive type mechanism as to the
kinds of shells returned by a function.  Earlier versions of Acl2 did
not have an analogous kind of rule because Acl2's type mechanism is
complicated by guards.  Version 1.3 supports type-prescription rules.
See TYPE-PRESCRIPTION.

Three more new rule-classes implement congruence-based rewriting.  It
is possible to identify a binary relation as an equivalence relation
(see EQUIVALENCE), to show that one equivalence relation
refines another (see REFINEMENT) and to show that a given
equivalence relation is maintained when rewriting a given function
call, e.g., (fn ...xk...), by maintaining another equivalence relation
while rewriting the kth argument (see CONGRUENCE).  If r has
been shown to be an equivalence relation and then (implies hyps (r (foo
x) (bar x))) is proved as a :rewrite rule, then instances of (foo x)
will be replaced by corresponding instances of (bar x) provided the
instance occurs in a slot where the maintainence of r-equivalence is
known to be sufficient and hyps can be established as usual.

In Version 1.2, rule-classes were simple keywords, e.g., :rewrite or
:elim.  In Version 1.3, rule-classes have been elaborated to allow you
to specify how the theorem ought to be used as a rule.  That is, the
new rule-classes allows you to separate the mathematical statement of
the formula from its interpretation as a rule.  See
RULE-CLASSES.

Rules used to be named by symbols, e.g., car and car-cons were the
names of rules.  Unfortunately, this was ambiguous because there are
three rules associated with function symbols: the symbolic definition,
the executable counterpart, and the type-prescription; many different
rules might be associated with theorems, depending on the rule classes.
In Version 1.3 rules are named by "runes" (which is just short hand
for "rule names").  Example runes are (:definition car),
(:executable-counterpart car), and (:type-prescription car . 1).  Every
rule added by an event has a different name and you can enable and
disable them independently.  See RUNE and see THEORIES.

The identity function force, of one argument, has been added and given
a special interpretation by the functions responsible for establishing
hypotheses in backchaining: When the system fails to establish some
hypothesis of the form (force term), it simply assumes it is true and
goes on, delaying until later the establishment of term.  In
particular, pushes a new subgoal to prove term in the current context.
When that subgoal is attacked, all of the resources of the theorem
prover, not just rewriting, are brought to bear.  Thus, for example, if
you wish to prove the rule (implies (good-statep s) (equal (exec s n)
s')) and it is your expectation that every time exec appears its first
argument is a good-statep then you might write the rule as (implies
(force (good-statep s)) (equal (exec s n) s')).  This rule is
essentially an unconditional rewrite of (exec s n) to s' that spawns
the new goal (good-statep s).  See FORCE.  Because you can now
specify independently how a theorem is used as a rule, you need not
write the force in the actual theorem proved.  See RULE-CLASSES.

Version 1.3 supports a facility similar to Nqthm's break-lemma.  See
BREAK-REWRITE.  You can install "monitors" on runes that will
cause interactive breaks under certain conditions.

Acl2 also provides "wormholes" which allow you to write functions that
cause interaction with the user but which do not require that you have
access to state.  See WORMHOLE.

The rewriter now automatically backchains to stronger recognizers.
There is no user hook to this feature but it may simplify some proofs
with which older versions of Acl2 had trouble.  For example, if the
rewriter is trying to prove (rationalp (foo a b c)) it is now smart
enough to try lemmas that match with (integerp (foo a b c)).

NOTE4    Acl2 Version 1.4 Notes

Once again ld only takes one required argument, as the bind-flg has
been deleted.

Three commands have been added in the spirit of :pe.  :Pe! is similar
to :pe but it prints all events with the given name, rather than just
the most recent.  The command :pf prints the corollary formula
corresponding to a name or rune.  The command :pl (print lemmas) prints
rules whose top function symbol is the given name.  See PE!,
see PF, and see PL.

Book naming conventions have been changed somewhat.  The once-required
.lisp extension is now prohibited!  Directories are supported,
including a notion of "connected book directory".  See
BOOK-NAME.  Also, the second argument of certify-book is now
optional, defaulting to 0.

Compilation is now supported inside the Acl2 loop.  See COMP
and see SET-COMPILE-FNS.

The default color is now part of the Acl2 world; see :doc
default-color.  Ld-color is no longer an ld special.  Instead, colors
are events; see the documentation for red, pink, blue, and gold.

A table exists for controlling whether Acl2 prints comments when it
forces hypotheses of rules; see :doc force-table.  Also, it is now
possible to turn off the forcing of assumptions by disabling the
definition of force; see FORCE.

The event defconstant is no longer supported, but a very similar event,
defconst, has been provided in its place.  See DEFCONST.

The event for defining congruence relations is now defcong (formerly,
defcon).

Patterns are now allowed in :expand hints.  See the documentation for
:expand inside the documentation for hints.

We have improved the way we report rules used by the simplifier.  All
runes of the same type are reported together in the running commentary
associated with each goal, so that for example, executable counterparts
are listed separately from definitions, and rewrite rules are listed
separately from linear rules.  The preprocessor now mentions "simple"
rules; see SIMPLE.

The mechanism for printing warning messages for new rewrite rules,
related to subsumption, now avoids worrying about nonrecursive function
symbols when those symbols are disabled.  These messages have also been
eliminated for the case where the old rule is a :definition rule.

Backquote has been modified so that it can usually provide predictable
results when used on the left side of a rewrite rule.

Time statistics are now printed even when an event fails.

The Acl2 trace package has been modified so that it prints using the
values of the Lisp globals *print-level* and *print-length*
(respectively).

Table has been modified so that the :clear option lets you replace the
entire table with one that satisfies the val and key guards (if any);
see TABLE.

We have relaxed the translation rules for :measure hints to defun, so
that the the same rules apply to these terms that apply to terms in
defthm events.  In particular, in :measure hints mv is treated just
like list, and state receives no special handling.

The loop-stopper test has been relaxed.  The old test required that
every new argument be strictly less than the corresponding old argument
in a certain term-order.  The new test uses a lexicographic order on
term lists instead.  For example, consider the following rewrite rule.

       (equal
        (variable-update var1
                         val1 (variable-update var2 val2 vs))
        (variable-update var2
                         val2 (variable-update var1 val1 vs)))

This rule is permutative.  Now imagine that we want to apply this rule
to the term

       (variable-update u y (variable-update u x vs)).

Since the actual corresponding to both var1 and var2 is u, which is not
strictly less than itself in the term-order, this rule would fail to be
applied in this situation when using the old test.  However, since the
pair (u x) is lexicographically less than the pair (u y) with respect
to our term-order, the rule is in fact applied using our new test.

Messages about events now contain a space after certain left
parentheses, in order to assist emacs users.  For example, the event

       (defthm abc (equal (+ (len x) 0) (len x)))

leads to a summary containing the line

       Form:  ( DEFTHM ABC ...)

and hence, if you search backwards for "(defthm abc", you won't stop at
this message.

More tautology checking is done during a proof; in fact, no goal
printed to the screen, except for the results of applying :use and :by
hints or the top-level goals from an induction proof, are known to Acl2
to be tautologies.

The ld-query-control-alist may now be used to suppress printing of
queries; see LD-QUERY-CONTROL-ALIST.

Warning messages are printed with short summary strings, for example
the string "Use" in the following message.

       Acl2 Warning [Use] in DEFTHM:  It is unusual to :USE an enabled
       :REWRITE or :DEFINITION rule, so you may want to consider
       disabling FOO.

At the end of the event, just before the time is printed, all such
summary strings are printed out.

The keyword command :u has been introduced as an abbreviation for :ubt
:max.  Printing of query messages is suppressed by :u.

The keyword :cheat is no longer supported by any event form.

Some irrelevant formals are detected; see IRRELEVANT-FORMALS.

A bug in the application of metafunctions was fixed: now if the output
of a metafunction is equal to its input, the application of the
metafunction is deemed unsuccessful and the next metafunction is tried.

An example has been added to the documentation for equivalence to
suggest how to make use of equivalence relations in rewriting.

The following Common Lisp functions have been added to Acl2:
alpha-char-p, upper-case-p, lower-case-p, char-upcase, char-downcase,
string-downcase, string-upcase, and digit-charp-p.

A documentation section called proof-checker has been added for the
interactive facility, whose documentation has been slightly improved.
See in particular the documentation for proof-checker, verify, and
macro-command.

A number of events that had been inadvertently disallowed in books are
now permitted in books.  These are:  defcong, defcor, defequiv,
defrefinement, defstub, and verify-termination.

NOTE5    Acl2 Version 1.5 Notes

Acl2 now allows "complex rationals," which are complex numbers whose
real parts are rationals and whose imaginary parts are non-zero
rationals.  See COMPLEX.

A new way of handling forced hypotheses has been implemented.  Rather
than cause a case split at the time the force occurs, we complete the
main proof and then embark on one or more "forcing rounds" in which we
try to prove the forced hypotheses.  See FORCING-ROUND.  To
allow us to compare the new handling of force with the old, Version 1.5
implements both and uses a flag in state to determine which method
should be used.  Do (assign old-style-forcing t) if you want force to
be handled as it was in Version 1.4.  However, we expect to eliminate
the old-style forcing eventually because we think the new style is more
effective.  To see the difference between the two approaches to
forcing, try proving the associativity of append under both settings of
old-style-forcing.  To get the new behavior invoke:

     (thm (implies (and (true-listp a) (true-listp b))
                   (equal (append (append a b) c)
                          (append a (append b c)))))

Then (assign old-style-forcing t) and invoke the thm command above
again.

A new :cases hints allows proof by cases.  See HINTS.

Include-book and encapsulate now restore the acl2-defaults-table when
they complete.  See INCLUDE-BOOK and see ENCAPSULATE.

The guards on many Acl2 primitives defined in axioms.lisp have been
weakened to permit them to be used in accordance with lisp custom and
tradition.

It is possible to attach heuristic filters to :rewrite rules to limit
their applicability.  See SYNTAXP.

A tutorial has been added (but as of Version_3.6.1 it has become
obsolete).

Events now print the Summary paragraph listing runes used, time, etc.,
whether they succeed or fail.  The format of the "failure banner" has
been changed but still has multiple asterisks in it.  Thm also prints a
Summary, whether it succeeds or fails; but thm is not an event.

A new event form skip-proofs has been added; see SKIP-PROOFS.

A user-specific customization facility has been added in the form of a
book that is automatically included, if it exists on the current
directory.  See ACL2-CUSTOMIZATION.

A facility for conditional metalemmas has been implemented; see
META.

The acceptable values for ld-skip-proofsp have changed.  In the old
version (Version 1.4), a value of t meant that proofs and local events
are to be skipped.  In Version 1.5, a value of t means proofs (but not
local events) are to be skipped.  A value of 'include-book means proofs
and local events are to be skipped.  There are two other, more obscure,
acceptable values.  See LD-SKIP-PROOFSP.

In order to turn off the forcing of assumptions, one should now disable
the :executable-counterpart of force (rather than the :definition of
force, as in the previous release); see FORCE.

The macros enable-forcing and disable-forcing make it convenient to
enable or disable forcing.  See ENABLE-FORCING and see
DISABLE-FORCING.

The new commands :pr and :pr! print the rules created by an event or
command.  See PR and see PR!.

The new history commands :puff and :puff* will replace a compound
command such as an encapsulate or include-book by the sequence of
events in it.  That is, they "puff up" or "lift" the subevents of a
command to the command level, eliminating the formerly superior command
and lengthening the history.  This is useful if you want to "partially
undo" an encapsulate or book or other compound command so you can
experiment.  See PUFF and see PUFF*.

Theory expressions now are allowed to use the free variable world and
prohibited from using the free variable state.  See THEORIES,
although it is essentially the same as before except it mentions world
instead of state.  See WORLD for a discussion of the Acl2
logical world.  Allowing in-theory events to be state-sensitive
violated an important invariant about how books behaved.

Table keys and values now are allowed to use the free variable world
and prohibited from using the free variable state.  See the note above
about theory expressions for some explanation.

The macro for minus, -, used to expand (- x 3) to (+ x -3) and now
expands it to (+ -3 x) instead.  The old macro, if used in the
left-hand sides of rewrite rules, produced inapplicable rules because
the constant occurs in the second argument of the +, but potential
target terms generally had the constant in the first argument position
because of the effect of commutativity-of-+.

A new class of rule, :linear-alias rules, allows one to implement the
nqthm package and similar hacks in which a disabled function is to be
known equivalent to an arithmetic function.

A new class of rule, :built-in-clause rules, allows one to extend the
set of clauses proved silently by defun during measure and guard
processing.  See BUILT-IN-CLAUSE.

The new command pcb! is like pcb but sketches the command and then
prints its subsidiary events in full.  See PCB!.

:Rewrite class rules may now specify the :loop-stopper field.  See
RULE-CLASSES and see LOOP-STOPPER.

The rules for how loop-stoppers control permutative rewrite rules have
been changed.  One effect of this change is that now when the built-in
commutativity rules for + are used, the terms a and (- a) are permuted
into adjacency.  For example, (+ a b (- a)) is now normalized by the
commutativity rules to (+ a (- a) b); in Version 1.4, b was considered
syntactically smaller than (- a) and so (+ a b (- a)) is considered to
be in normal form.  Now it is possible to arrange for unary functions
be be considered "invisible" when they are used in certain contexts.
By default, unary- is considered invisible when its application appears
in the argument list of binary-+.  See LOOP-STOPPER and see
:DOC set-invisible-fns-table.

Extensive documentation has been provided on the topic of Acl2's "term
ordering."  See TERM-ORDER.

Calls of ld now default ld-error-action to :return rather than to the
current setting.

The command descriptor :x has been introduced and is synonymous with
:max, the most recently executed command.  History commands such as
:pbt print a :x beside the most recent command, simply to indicate that
it *is* the most recent one.

The command descriptor :x-23 is synonymous with (:x -23).  More
generally, every symbol in the keyword package whose first character is
#\x and whose remaining characters parse as a negative integer is
appropriately understood.  This allows :pbt :x-10 where :pbt (:max -10)
or :pbt (:here -10) were previously used.  The old forms are still
legal.

The order of the arguments to defcong has been changed.

The simplifier now reports the use of unspecified built-in type
information about the primitives with the phrase "primitive type
reasoning."  This phrase may sometimes occur in situations where
"propositional calculus" was formerly credited with the proof.

The function pairlis has been replaced in the code by a new function
pairlis$, because Common Lisp does not adequately specify its pairlis
function.

Some new Common Lisp functions have been added, including logtest,
logcount, integer-length, make-list, remove-duplicates, string, and
concatenate.  The source file /slocal/src/acl2/axioms.lisp is the
ultimate reference regarding Common Lisp functions in Acl2.

The functions defuns and theory-invariant have been documented.  See
DEFUNS and see THEORY-INVARIANT.

A few symbols have been added to the list *acl2-exports*.

A new key has been implemented for the acl2-defaults-table,
:irrelevant-formals-ok.  See SET-IRRELEVANT-FORMALS-OK.

The connected book directory, cbd, must be nonempty and begin and end
with a slash.  It is set (and displayed) automatically upon your first
entry to lp.  You may change the setting with set-cbd.  See CBD.

:oops will undo the last :ubt.  See OOPS.

Documentation has been written about the ordinals.  See :DOC e0-ordinalp
and see :DOC e0-ord-<.  [Note added later: Starting with Version_2.8,
instead see O-P and see O<.

The color events -- (red), (pink), (blue), and (gold) -- may no longer
be enclosed inside calls of local, for soundness reasons.  In fact,
neither may any event that sets the acl2-defaults-table.  See
EMBEDDED-EVENT-FORM.

See LD-KEYWORD-ALIASES for an example of how to change the exit
keyword from :q to something else.

The attempt to install a monitor on :rewrite rules stored as simple
abbreviations now causes an error because the application of
abbreviations is not tracked.

A new message is sometimes printed by the theorem prover, indicating
that a given simplification is "specious" because the subgoals it
produces include the input goal.  In Version 1.4 this was detected but
not reported, causing behavior some users found bizarre.  See
SPECIOUS-SIMPLIFICATION.

:Definition rules are no longer always required to specify the :clique
and :controller-alist fields; those fields can be defaulted to
system-determined values in many common instances.  See
DEFINITION.

A warning is printed if a macro form with keyword arguments is given
duplicate keyword values.  Execute (thm t :doc nil :doc "ignored") and
read the warning printed.

A new restriction has been placed on encapsulate.  Non-local recursive
definitions inside the encapsulate may not use, in their tests and
recursive calls, the constrained functions introduced by the
encapsulate.  See SUBVERSIVE-RECURSIONS.  (Note added in
Version  2.3:  Subversive recursions were first recognized by us here
in Version 1.5, but our code for recognizing them was faulty and the
bug was not fixed until Version  2.3.)

The events defequiv, defcong, defrefinement, and defevaluator have been
reimplemented so that they are just macros that expand into appropriate
defthm or encapsulate events; they are no longer primitive events.  See
the documentation of each affected event.

The defcor event, which was a shorthand for a defthm that established a
corollary of a named, previously proved event, has been eliminated
because its implementation relied on a technique we have decided to ban
from our code.  If you want the effect of a defcor in Version 1.5 you
must submit the corresponding defthm with a :by hint naming the
previously proved event.

Error reporting has been improved for inappropriate in-theory hints and
events, and for syntax errors in rule classes, and for non-existent
filename arguments to ld.

Technical Note:  We now maintain the Third Invariant on type-alists, as
described in the Essay on the Invariants on Type-alists, and
Canonicality.  This change will affect some proofs, for example, by
causing a to rewrite more quickly to c when (equiv a b) and (equiv b c)
are both known and c is the canonical representative of the three.

NOTE6    Acl2 Version 1.6 Notes

A new key has been implemented for the acl2-defaults-table, :ignore-ok.
See SET-IGNORE-OK.

It is now legal to have color events, such as (red), in the portcullis
of a book.  More generally, it is legal to set the acl2-defaults-table
in the portcullis of a book.  For example, if you execute :red and then
certify a book, the event (red) will show up in the portcullis of that
book, and hence the definitions in that book will all be red (except
when overridden by appropriate declarations or events).  When that book
is included, then as always, its portcullis must first be "raised," and
that will cause the default color to become red before the events in
the book are executed.  As always, the value of acl2-defaults-table
immediately after execution of an include-book, certify-book, or
encapsulate form will be the same as it was immediately before
execution (and hence, so will the default color).  See
PORTCULLIS and, for more about books, see BOOKS.

A theory ground-zero has been defined to contain exactly those rules
that are enabled when Acl2 starts up.  See GROUND-ZERO.

The function nth is now enabled, correcting an oversight from Version
1.5.

Customization files no longer need to meet the syntactic restrictions
put on books; rather, they can contain arbitrary Acl2 forms.  See
ACL2-CUSTOMIZATION.

Structured directory names and structured file names are supported; see
especially the documentation for pathname, book-name, and cbd.

Acl2 now works with some Common Lisp implementations other than akcl,
including Lucid, Allegro, and MCL.

A facility has been added for displaying proof trees, especially using
emacs; see PROOF-TREE.

There is a considerable amount of new documentation, in particular for
the printing functions fmt, fmt1, and fms, and for the notion of Acl2
term (see TERM).

It is possible to introduce new well-founded relations, to specify
which relation should be used by defun, and to set a default relation.
See WELL-FOUNDED-RELATION.

It is possible to make functions suggest new inductions.  See
INDUCTION.

It is possible to change how Acl2 expresses type-set information; in
particular, this affects what clauses are proved when forced
assumptions are generated.  See TYPE-SET-INVERTER.

A new restriction has been added to defpkg, having to do with undoing.
If you undo a defpkg and define the same package name again, the
imports list must be identical to the previous imports or else an
explanatory error will occur.  See
PACKAGE-REINCARNATION-IMPORT-RESTRICTIONS.

Theory-invariant and set-irrelevant-formals-ok are now embedded event
forms.

The command :good-bye may now be used to quit entirely out of Lisp,
thus losing your work forever.  This command works in akcl but may not
work in every Common Lisp.

A theory ground-zero has been added that contains exactly the enabled
rules in the startup theory.  See GROUND-ZERO.

Define-pc-macro and define-pc-atomic-macro now automatically define
:red functions.  (It used to be necessary, in general, to change color
to :red before invoking these.)

For a proof of the well-foundedness of e0-ord-< on the e0-ordinalps,
see PROOF-OF-WELL-FOUNDEDNESS.  [Note added later: Starting with
Version_2.8, o< and o-p replace e0-ord-< and e0-ordinalp, respectively.]

Free variables are now handled properly for hypotheses of
:type-prescription rules.

When the system is loaded or saved, state is now bound to
*the-live-state*.

Certify-book has been modified so that when it compiles a file, it
loads that object file.

Defstub has been modified so that it works when the color is hot (:red
or :pink).

Several basic, but not particularly commonly used, events have been
added or changed.  The obscure axiom symbol-name-intern has been
modified.  The definition of firstn has been changed.  Butlast is now
defined.  The definition of integer-length has been modified.  The
left-hand side of the rewrite rule rational-implies2 has been changed
from (* (numerator x) (/ (denominator x))) to (* (/ (denominator x))
(numerator x)), in order to respect the fact that unary-/ is invisible
with respect to binary-*.  See LOOP-STOPPER.

The `preprocess' process in the waterfall (see HINTS for a
discussion of the :do-not hint) has been changed so that it works to
avoid case-splitting.  The `simplify' process refuses to force (see
FORCE) when there are if terms, including and and or terms, in
the goal being simplified.

The function apply is no longer introduced automatically by translation
of user input to internal form when functions are called on
inappropriate explicit values, e.g., (car 3).

The choice of which variable to use as the measured variable in a
recursive definition has been very slightly changed.

NOTE7    ACL2 Version 1.7 (released October 1994) Notes

Include-book now takes (optionally) an additional keyword argument,
indicating whether a compiled file is to be loaded.  The default
behavior is unchanged, except that a warning is printed when a compiled
file is not loaded.  See INCLUDE-BOOK.

A markup language for documentation strings has been implemented, and
many of the source files have been marked up using this language
(thanks largely to the efforts of Laura Lawless).  See MARKUP.
Moreover, there are translators that we have used to provide versions
of the ACL2 documentation in info (for use in emacs), html (for
Mosaic), and tex (for hardcopy) formats.

A new event defdoc has been implemented.  It is like deflabel, but
allows redefinition of doc strings and has other advantages.  See
DEFDOC.

We used to ignore corollaries when collecting up the axioms introduced
about constrained functions.  That bug has been fixed.  We thank John
Cowles for bringing this bug to our attention.

The macro defstub now allows a :doc keyword argument, so that
documentation may be attached to the name being introduced.

A new command nqthm-to-acl2 has been added to help Nqthm users to make
the transition to ACL2.  See NQTHM-TO-ACL2, which also includes
a complete listing of the relevant tables.

Many function names, especially of the form "foo-lst", have been
changed in order to support the following convention, for any "foo":

     (foo-listp lst) represents the notion (for x in lst always foop x).

A complete list of these changes may be found at the end of this note.
All of them except symbolp-listp and list-of-symbolp-listp have the
string "-lst" in their names.  Note also that keyword-listp has been
renamed keyword-value-listp.

Accumulated persistence has been implemented.  It is not connected to
:brr or rule monitoring.  See ACCUMULATED-PERSISTENCE.

:Trigger-terms has been added for :linear rule classes, so you can hang
a linear rule under any addend you want.  See LINEAR, which has
been improved and expanded.

ACL2 now accepts 256 characters and includes the Common Lisp functions
code-char and char-code.  However, ACL2 controls the lisp reader so
that #\c may only be used when c is a single standard character or one
of Newline, Space, Page, Rubout, Tab.  If you want to enter other
characters use code-char, e.g., (coerce (list (code-char 7) (code-char
240) #a) 'string).  See CHARACTERS.  Note:  our current
handling of characters makes the set of theorems different under
Macintosh Common Lisp (MCL) than under other Common Lisps.  We hope to
rectify this situation before the final release of ACL2.

A new table, macro-aliases-table, has been implemented, that associates
macro names with function names.  So for example, since append is
associated with binary-append, the form (disable append) it is
interpreted as though it were (disable binary-append).  See
MACRO-ALIASES-TABLE, see ADD-MACRO-ALIAS and see
REMOVE-MACRO-ALIAS.

The implementation of conditional metalemmas has been modified so that
the metafunction is applied before the hypothesis metafunction is
applied.  See META.

The Common Lisp functions acons and endp have been defined in the ACL2
logic.

We have added the symbol declare to the list *acl2-exports*, and hence
to the package "ACL2-USER".

A new hint, :restrict, has been implemented.  See HINTS.

It used to be that if :ubt were given a number that is greater than the
largest current command number, it treated that number the same as
:max.  Now, an error is caused.

The table :force-table has been eliminated.

A command :disabledp (and macro disabledp) has been added; see
DISABLEDP.

Compilation via :set-compile-fns is now suppressed during include-book.
In fact, whenever the state global variable ld-skip-proofsp has value
'include-book.

Here are some less important changes, additions, and so on.

Unlike previous releases, we have not proved all the theorems in
axioms.lisp; instead we have simply assumed them.  We have deferred
such proofs because we anticipate a fairly major changed in Version 1.8
in how we deal with guards.

We used to (accidentally) prohibit the "redefinition" of a table as a
function.  That is no longer the case.

The check for whether a corollary follows tautologically has been sped
up, at the cost of making the check less "smart" in the following
sense:  no longer do we expand primitive functions such as implies
before checking this propositional implication.

The command ubt! has been modified so that it never causes or reports
an error.  See UBT!.

ACL2 now works in Harlequin Lispworks.

The user can now specify the :trigger-terms for :linear rules.  See
LINEAR.

The name of the system is now "ACL2"; no longer is it "Acl2".

The raw lisp counterpart of theory-invariant is now defined to be a
no-op as is consistent with the idea that it is just a call of table.

A bug was fixed that caused proof-checker instructions to be executed
when ld-skip-proofsp was t.

The function rassoc has been added, along with a corresponding function
used in its guard, r-eqlable-alistp.

The in-theory event and hint now print a warning not only when certain
"primitive" :definition rules are disabled, but also when certain
"primitive" :executable-counterpart rules are disabled.

The modified version of trace provided by ACL2, for use in raw Lisp,
has been modified so that the lisp special variable *trace-alist* is
consulted.  This alist associates, using eq, values with their print
representations.  For example, initially *trace-alist* is a one-element
list containing the pair (cons state '|*the-live-state*|).

The system now prints an observation when a form is skipped because the
default color is :red or :pink.  (Technically:  when-cool has been
modified.)

Additional protection exists when you submit a form to raw Common Lisp
that should only be submitted inside the ACL2 read-eval-print loop.

Here is a complete list of the changes in function names described near
the top of this note, roughly of the form

     foo-lst --> foo-listp

meaning:  the name "foo-lst" has been changed to "foo-listp."

     symbolp-listp    --> symbol-listp
     list-of-symbolp-listp  --> symbol-list-listp
                            {for consistency with change to symbol-listp}
     rational-lst     --> rational-listp
                          {which in fact was already defined as well}
     integer-lst      --> integer-listp
     character-lst    --> character-listp
     stringp-lst      --> string-listp
     32-bit-integer-lst   --> 32-bit-integer-listp
     typed-io-lst     --> typed-io-listp
     open-channel-lst --> open-channel-listp
     readable-files-lst   --> readable-files-listp
     written-file-lst --> written-file-listp
     read-file-lst    --> read-file-listp
     writeable-file-lst   --> writable-file-listp
                          {note change in spelling of ``writable''}
     writeable-file-lst1  --> writable-file-listp1
     pseudo-termp-lst     --> pseudo-term-listp
     hot-termp-lst --> hot-term-listp {by analogy with pseudo-term-listp}
     weak-termp-lst   --> weak-term-listp
     weak-termp-lst-lst   --> weak-termp-list-listp
     ts-builder-case-lstp -> ts-builder-case-listp
     quotep-lst       --> quote-listp
     termp-lst        --> term-listp
     instr-lst        --> instr-listp
     spliced-instr-lst    --> spliced-instr-listp
     rewrite-fncallp-lst  --> rewrite-fncallp-listp
     every-occurrence-equiv-hittablep1-lst -->
                 every-occurrence-equiv-hittablep1-listp
     some-occurrence-equiv-hittablep1-lst  -->
                 some-occurrence-equiv-hittablep1-listp
                 {by analogy with the preceding, even though it's a
                  ``some'' instead of ``all'' predicate]
     almost-quotep1-lst   --> almost-quotep1-listp
     ffnnames-subsetp-lst --> ffnnames-subsetp-listp
     boolean-lstp     --> boolean-listp
     subst-expr1-lst-okp  --> subst-expr1-ok-listp

NOTE8    ACL2 Version 1.8 (May, 1995) Notes

See NOTE8-UPDATE for yet more recent changes.

Guards have been eliminated from the ACL2 logic.  A summary is
contained in this brief note.  Also see DEFUN-MODE and see
SET-GUARD-CHECKING.

Guards may be included in defuns as usual but are ignored from the
perspective of admission to the logic: functions must terminate on all
arguments.

As in Nqthm, primitive functions, e.g., + and car, logically default
unexpected arguments to convenient values.  Thus, (+ 'abc 3) is 3 and
(car 'abc) is nil.  See PROGRAMMING, and see the documentation
for the individual primitive functions.

In contrast to earlier versions of ACL2, Version 1.8 logical functions
are executed at Nqthm speeds even when guards have not been verified.
In versions before 1.8, such functions were interpreted by ACL2.

Colors have been eliminated.  Two "defun-modes" are supported, :program
and :logic.  Roughly speaking, :program does what :red used to do,
namely, allow you to prototype functions for execution without any
proof burdens.  :Logic mode does what :blue used to do, namely, allow
you to add a new definitional axiom to the logic.  A global
default-defun-mode is comparable to the old default color.  The system
comes up in :logic mode.  To change the global defun-mode, type
:program or :logic at the top-level.  To specify the defun-mode of a
defun locally use

     (declare (xargs :mode mode)).

The prompt has changed.  The initial prompt, indicating :logic mode, is

     ACL2 !>

If you change to :program mode the prompt becomes

     ACL2 p!>

Guards can be seen as having either of two roles: (a) they are a
specification device allowing you to characterize the kinds of inputs a
function "should" have, or (b) they are an efficiency device allowing
logically defined functions to be executed directly in Common Lisp.  If
a guard is specified, as with xargs :guard, then it is "verified" at
defun-time (unless you also specify xargs :verify-guards nil).  Guard
verification means what it always has: the input guard is shown to
imply the guards on all subroutines in the body.  If the guards of a
function are verified, then a call of the function on inputs satisfying
the guard can be computed directly by Common Lisp.  Thus, verifying the
guards on your functions will allow them to execute more efficiently.
But it does not affect their logical behavior and since you will
automatically get Nqthm speeds on unverified logical definitions, most
users will probably use guards either as a specification device or only
use them when execution efficiency is extremely important.

Given the presence of guards in the system, two issues are unavoidable.
Are guards verified as part of the defun process?  And are guards
checked when terms are evaluated?  We answer both of those questions
below.

Roughly speaking, in its initial state the system will try to verify
the guards of a defun if a :guard is supplied in the xargs and will not
try otherwise.  However, guard verification in defun can be inhibited
"locally" by supplying the xargs :verify-guards nil.  "Global"
inhibition can be obtained via the :set-verify-guards-eagerness.  If
you do not use the :guard xargs, you will not need to think about guard
verification.

We now turn to the evaluation of expressions.  Even if your functions
contain no guards, the primitive functions do and hence you have the
choice: when you submit an expression for evaluation do you mean for
guards to be checked at runtime or not?  Put another way, do you mean
for the expression to be evaluated in Common Lisp (if possible) or in
the logic?  Note: If Common Lisp delivers an answer, it will be the
same as in the logic, but it might be erroneous to execute the form in
Common Lisp.  For example, should (car 'abc) cause a guard violation
error or return nil?

The top-level ACL2 loop has a variable which controls which sense of
execution is provided.  To turn "guard checking on," by which we mean
that guards are checked at runtime, execute the top-level form
:set-guard-checking t.  To turn it off, do :set-guard-checking nil.
The status of this variable is reflected in the prompt.

     ACL2 !>

means guard checking is on and

     ACL2 >

means guard checking is off.  The exclamation mark can be thought of as
"barring" certain computations.  The absence of the mark suggests the
absence of error messages or unbarred access to the logical axioms.
Thus, for example

     ACL2 !>(car 'abc)

will signal an error, while

     ACL2 >(car 'abc)

will return nil.

Note that whether or not guards are checked at runtime is independent
of whether you are operating in :program mode or :logic mode and
whether theorems are being proved or not.  (Although it must be added
that functions defined in :program mode cannot help but check their
guards because no logical definition exists.)

Version 1.8 permits the verification of the guards of theorems, thus
insuring that all instances of the theorem will evaluate without error
in Common Lisp.  To verify the guards of a theorem named name execute
the event

     (verify-guards name).

If a theorem's guards have been verified, the theorem is guaranteed to
evaluate without error to non-nil in Common Lisp (provided resource
errors do not arise).

Caveat about verify-guards: implies is a function symbol, so in the
term (implies p q), p cannot be assumed true when q is evaluated; they
are both evaluated "outside."  Hence, you cannot generally verify the
guards on a theorem if implies is used to state the hypotheses.  Use if
instead.  In a future version of ACL2, implies will likely be a macro.

See sum-list-example.lisp for a nice example of the use of Version 1.8.
This is roughly the same as the documentation for guard-example.

We have removed the capability to do "old-style-forcing" as existed
before Version 1.5.  See NOTE5.

NOTE:  Some low level details have, of course, changed.  One such
change is that there are no longer two distinct type prescriptions
stored when a function is admitted with its guards verified.  So for
example, the type prescription rune for binary-append is now

     (:type-prescription binary-append)

while in Versions 1.7 and earlier, there were two such runes:

     (:type-prescription binary-append . 1)
     (:type-prescription binary-append . 2)

Nqthm-style forcing on linear arithmetic assumptions is no longer
executed when forcing is disabled.

Functional instantiation now benefits from a trick also used in Nqthm:
once a constraint generated by a :functional-instance lemma instance
(see LEMMA-INSTANCE) has been proved on behalf of a successful
event, it will not have to be re-proved on behalf of a later event.

1+ and 1- are now macros in the logic, not functions.  Hence, for
example, it is "safe" to use them on left-hand sides of rewrite rules,
without invoking the common warning about the presence of nonrecursive
function symbols.

A new documentation section file-reading-example illustrates how to
process forms in a file.

A new proof-checker command forwardchain has been added; see
ACL2-PC||FORWARDCHAIN.

It is now possible to use quantifiers.  See DEFUN-SK and see
DEFCHOOSE.

There is a new event set-inhibit-warnings, which allows the user to
turn off warnings of various types.  see SET-INHIBIT-WARNINGS.

An unsoundness relating encapsulate and :functional-instance hints has
been remedied, with a few small effects visible at the user level.  The
main observable effect is that defaxiom and non-local include-book
events are no longer allowed in the scope of any encapsulate event that
has a non-empty signature.

When certify-book is called, we now require that the default defun-mode
(see DEFAULT-DEFUN-MODE) be :logic.  On a related note, the
default defun-mode is irrelevant to include-book; the mode is always
set to :logic initially, though it may be changed within the book and
reverts to its original value at the conclusion of the include-book.  A
bug in include-book prevented it from acting this way even though the
documentation said otherwise.

The documentation has been substantially improved.  A new section
"Programming" contains documentation of many useful functions provided
by ACL2; see PROGRAMMING.  Also, the documentation has been
"marked up" extensively.  Thus in particular, users of Mosaic will find
many links in the documentation.

The symbols force, mv-nth, and acl2-count have been added to the list
*acl2-exports*.

We now permit most names from the main Lisp package to be used as
names, except for names that define functions, macros, or constants.
See NAME.

We have changed the list of imports from the Common Lisp package to
ACL2, i.e., the list *common-lisp-symbols-from-main-lisp-package*, to
be exactly those external symbols of the Common Lisp package as
specified by the draft Common Lisp standard.  In order to accommodate
this change, we have renamed some ACL2 functions as shown below, but
these and other ramifications of this change should be transparent to
most ACL2 users.

     warning      --> warning$
     print-object --> print-object$

Proof trees are no longer enabled by default.  To start them up,
:start-proof-tree.

We have added the capability of building smaller images.  The easiest
way to do this on a Unix (trademark of AT&T) system is: make small.

Here we will put some less important changes, additions, and so on.

We have added definitions for the Common Lisp function position (for
the test eql), as well as corresponding versions position-equal and
position-eq that use tests equal and eq, respectively.  See
POSITION, see POSITION-EQUAL, and see POSITION-EQ.

The defthm event rational-listp-implies-rationalp-car no longer exists.

We fixed a bug in the hint mechanism that applied :by, :cases, and :use
hints to the first induction goal when the prover reverted to proving
the original goal by induction.

We fixed a bug in the handling of (set-irrelevant-formals-ok :warn).

In support of removing the old-style forcing capability, we deleted the
initialization of state global old-style-forcing and deleted the
definitions of recover-assumptions, recover-assumptions-from-goal,
remove-assumptions1, remove-assumptions, and split-on-assumptions, and
we renamed split-on-assumptions1 to split-on-assumptions.

The special value 'none in the proof-checker commands claim and = has
been replaced by :none.

A bug in the handling of hints by subgoals has been fixed.  For
example, formerly a :do-not hint could be "erased" by a :use hint on a
subgoal.  Thanks go to Art Flatau for noticing the bug.

The functions weak-termp and weak-term-listp have been deleted, and
their calls have been replaced by corresponding calls of pseudo-termp
and pseudo-term-listp.  The notion of pseudo-termp has been slightly
strenthened by requiring that terms of the form (quote ...) have length
2.

Performance has been improved in various ways.  At the prover level,
backchaining through the recognizer alist has been eliminated in order
to significantly speed up ACL2's rewriter.  Among the other prover
changes (of which there are several, all technical):  we no longer
clausify the input term when a proof is interrupted in favor of
inducting on the input term.  At the IO level, we have improved
performance somewhat by suitable declarations and proclamations.  These
include technical modifications to the macros mv and mv-let, and
introduction of a macro the-mv analogous to the macro the but for forms
returning multiple values.

The function spaces now takes an extra argument, the current column.

A bug in the proof-checker equiv command was fixed.

The function intersectp has been deleted, because it was essentially
duplicated by the function intersectp-equal.

We now proclaim functions in AKCL and GCL before compiling books.  This
should result in somewhat increased speed.

The function repeat has been eliminated; use make-list instead.

The proof-checker command expand has been fixed so that it eliminates
let (lambda) expressions when one would expect it to.

A new primitive function, mv-nth, has been introduced.  Mv-nth is
equivalent to nth and is used in place of nth in the translation of
mv-let expressions.  This allows the user to control the simplification
of mv-let expressions without affecting how nth is treated.  In that
spirit, the rewriter has been modified so that certain mv-nth
expressions, namely those produced in the translation of (mv-let (a b
c)(mv x y z) p), are given special treatment.

A minor bug in untranslate has been fixed, which for example will fix
the printing of conjunctions.

Translate now takes a logicp argument, which indicates whether it
enforces the restriction that :program mode functions do not occur in
the result.

The modified version of trace provided by ACL2, for use in raw Lisp,
has been modified so that the lisp special variable *trace-alist* has a
slightly different functionality.  This alist associates, using eq,
symbols with the print representations of their values.  For example,
initially *trace-alist* is a one-element list containing the pair (cons
'state '|*the-live-state*|).  Thus, one may cons the pair (cons '*foo*
"It's a FOO!") on to *trace-alist*; then until *foo* is defined, this
change will have no effect, but after for example

     (defconst *foo* 17)

then trace will print 17 as "It's a FOO!".

Trace also traces the corresponding logic function.

Proof-tree display has been improved slightly in the case of successful
proofs and certain event failures.

The function positive-integer-log2 has been deleted.

The macro skip-proofs now prints a warning message when it is
encountered in the context of an encapsulate event or a book.  See
SKIP-PROOFS.

Some functions related to the-fn and wormhole1 now have defun-mode
:program, but this change is almost certain to be inconsequential to
all users.

NOTE8-UPDATE    ACL2 Version 1.8 (Summer, 1995) Notes

ACL2 can now use Ordered Binary Decision Diagram technology.  See
BDD.  There is also a proof-checker bdd command.

ACL2 is now more respectful of the intention of the function hide.  In
particular, it is more careful not to dive inside any call of hide
during equality substitution and case splitting.

The ld special (see LD) ld-pre-eval-print may now be used to
turn off printing of input forms during processing of encapsulate and
certify-book forms, by setting it to the value :never, i.e.,
(set-ld-pre-eval-print :never state).  See LD-PRE-EVAL-PRINT.

The TUTORIAL documentation section (now obsolete) has, with much help
from Bill Young, been substantially improved to a bona fide
introduction.

The term pretty-printer has been modified to introduce (<= X Y) as an
abbreviation for (not (< Y X)).

Forward chaining and linear arithmetic now both benefit from the
evaluation of ground subterms.

A new macro set-inhibit-output-lst has been defined.  This should be
used when setting the state global inhibit-output-lst; see
SET-INHIBIT-OUTPUT-LST and see PROOF-TREE.

The test for redundancy in definitions includes the guard and type
declarations.  See REDUNDANT-EVENTS.

See GENERALIZED-BOOLEANS for a discussion of a potential
soundness problem for ACL2 related to the question:  Which Common Lisp
functions are known to return Boolean values?

Here we will put some less important changes, additions, and so on.

A bug has been fixed so that now, execution of :comp t (see
COMP) correctly handles non-standard characters.

A bug in digit-char-p has been fixed, so that the "default" is nil
rather than 0.

True-listp now tests the final cdr against nil using eq instead of
equal, for improved efficiency.  The logical meaning is, however,
unchanged.

Put-assoc-equal has been added to the logic (it used to have
:defun-mode :program, and has been documented.

NOTE9    ACL2 Version 1.9 (Fall, 1996) Notes

By default, when the system is started it is illegal to use the
variable STATE as a formal parameter of a function definition.  The aim
is to prevent novice users from stumbling into the Byzantine syntactic
restrictions on that variable symbol.  Use

     :set-state-ok t

or, equivalently,

     (set-state-ok t)

to switch back to the old default mode.  See SET-STATE-OK

Set-state-ok is an event that affects the ACL2 defaults table (see
ACL2-DEFAULTS-TABLE).  Recall that when books are included, the
defaults table is restored to its pre-inclusion state.  Thus, while a
set-state-ok form will permit the book to define a state-using
function, it will not permit the user of the book to make such a
definition.  We recommend putting (set-state-ok t) in any book that
defines a state using function.

Books certified under Version 1.8 must be recertified under Version
1.9.  See :DOC version.

The simplifier has been made to look out for built-in clauses, whereas
in past versions such clauses were only noticed by the "preprocessor"
at the top of the waterfall.  THIS CHANGE MAY PREVENT OLD SCRIPTS FROM
REPLAYING!  The undesirable side-effect is caused by the fact that
:HINTS require you to refer to clauses by their exact name (see
GOAL-SPEC) and because the new simplifier proves more clauses than
before, the goals produced have different names.  Thus, if a script
uses :HINTS that refer to clauses other than "Goal", e.g., "Subgoal
1.3" then the hint may be applied to a different subgoal than
originally intended.

The use of built-in-clauses has been made more efficient.  If a set of
clauses arise often in a piece of work, it might be advantageous to
build them in even if that results in a large set (hundreds?) of
built-in clauses.  See BUILT-IN-CLAUSE

Wormholes can now be used in :logic mode functions. See WORMHOLE

It is now possible to provide "computed hints."  For example, have you
ever wished to say "in all goals with a name like this, :use that" or
"if this term is in the subgoal, then :use that"?  Well, see
COMPUTED-HINTS and the extraordinarily long example in see
USING-COMPUTED-HINTS.

Hide terms may be rewritten with :rewrite rules about hide.  See
HIDE, where we also now explain why hide terms are sometimes
introduced into your proof attempts.

A bug that sometimes caused the "non-lazy IF" hard error message was
fixed.

A bug that sometimes caused a hard error in forward chaining was fixed.

A bug in print-rules (:pr) was fixed.

We report the use of :executable-counterparts in the evaluation of
SYNTAXP forms.

Some documentation errors were fixed.

A bug in parent-tree tracking in add-literal-and-pt was fixed.

A bug in ok$, go$ and eval$ was fixed.

Clausify now optimizes (mv-nth 'k (list x0 ... xk ... xn)) to xk.

RULE-CLASSES    adding rules to the data base

     Example Form (in a defthm from books/finite-set-theory/total-ordering.lisp):
     (defthm <<-trichotomy
       (implies (and (ordinaryp x)
                     (ordinaryp y))
                (or (<< x y)
                    (equal x y)
                    (<< y x)))
       :rule-classes
       ((:rewrite :corollary
                  (implies (and (ordinaryp x)
                                (ordinaryp y)
                                (not (<< x y))
                                (not (equal x y)))
                           (<< y x)))))

     General Form:
     a true list of rule class objects as defined below

     Special Cases:
     a symbol abbreviating a single rule class object

ACL2 provides users with the ability to create a number of different
kinds of rules, including (conditional) rewrite rules but also
including others.  Don't be put off by the long description to follow;
usually, you'll probably want to use rewrite rules.  More on this below.

A rule class object is either one of the :class keywords or else is a
list of the form shown below.  Those fields marked with "(!)"  are
required when the :class is as indicated.

     (:class
       :COROLLARY term
       :TRIGGER-FNS (fn1 ... fnk) ; provided :class = :META (!)
       :TRIGGER-TERMS (t1 ... tk) ; provided :class = :FORWARD-CHAINING
                                  ;       or :class = :LINEAR
       :TYPE-SET n                ; provided :class = :TYPE-SET-INVERTER
       :TYPED-TERM term           ; provided :class = :TYPE-PRESCRIPTION
       :CLIQUE (fn1 ... fnk)      ; provided :class = :DEFINITION
       :CONTROLLER-ALIST alist    ; provided :class = :DEFINITION
       :INSTALL-BODY directive    ; provided :class = :DEFINITION
       :LOOP-STOPPER alist        ; provided :class = :REWRITE
       :PATTERN term              ; provided :class = :INDUCTION (!)
       :CONDITION term            ; provided :class = :INDUCTION
       :SCHEME term               ; provided :class = :INDUCTION (!)
       :MATCH-FREE all-or-once    ; provided :class = :REWRITE
                                          or :class = :LINEAR
                                          or :class = :FORWARD-CHAINING
       :BACKCHAIN-LIMIT-LST limit ; provided :class = :REWRITE
                                          or :class = :META
                                          or :class = :LINEAR
                                          or :class = :TYPE-PRESCRIPTION
       :HINTS hints               ; provided instrs = nil
       :INSTRUCTIONS instrs       ; provided  hints = nil
       :OTF-FLG flg)

When rule class objects are provided by the user, most of the fields are
optional and their values are computed in a context sensitive way.
When a :class keyword is used as a rule class object, all relevant
fields are determined contextually.  Each rule class object in
:rule-classes causes one or more rules to be added to the data base.
The :class keywords are documented individually under the following
names.  Note that when one of these names is used as a :class, it is
expected to be in the keyword package (i.e., the names below should be
preceded by a colon but the ACL2 documentation facilities do not permit
us to use keywords below).

See also force, case-split, syntaxp, and bind-free for "pragmas" one
can wrap around individual hypotheses of linear and rewrite rules to
affect how the hypothesis is relieved.

Before we get into the discussion of rule classes, let us return to an
important point.  In spite of the large variety of rule classes
available, at present we recommend that new ACL2 users rely almost
exclusively on (conditional) rewrite rules.  A reasonable but slightly
bolder approach is to use :type-prescription and :forward-chaining
rules for "type-theoretic" rules, especially ones whose top-level
function symbol is a common one like true-listp or consp; see
TYPE-PRESCRIPTION and see FORWARD-CHAINING.  However, the
rest of the rule classes are really not intended for widespread use,
but rather are mainly for experts.

We expect that we will write more about the question of which kind of
rule to use.  For now: when in doubt, use a :rewrite rule.

:Rule-classes is an optional keyword argument of the defthm (and
defaxiom) event.  In the following, let name be the name of the event
and let thm be the formula to be proved or added as an axiom.

If :rule-classes is not specified in a defthm (or defaxiom) event, it
is as though what was specified was to make one or more :rewrite rules,
i.e., as though :rule-classes ((:rewrite)) had been used.  Use
:rule-classes nil to specify that no rules are to be generated.

If :rule-classes class is specified, where class is a non-nil symbol,
it is as though :rule-classes ((class)) had been used.  Thus,
:rule-classes :forward-chaining is equivalent to :rule-classes
((:forward-chaining)).

We therefore now consider :rule-classes as a true list.  If any element
of that list is a keyword, replace it by the singleton list containing
that keyword.  Thus, :rule-classes (:rewrite :elim) is the same as
:rule-classes ((:rewrite) (:elim)).

Each element of the expanded value of :rule-classes must be a true list
whose car is one of the rule class keyword tokens listed above, e.g.,
:rewrite, :elim, etc., and whose cdr is a "keyword alist" alternately
listing keywords and values.  The keywords in this alist must be taken
from those shown below.  They may be listed in any order and most may
be omitted, as specified below.

     :Corollary -- its value, term, must be a term.  If omitted, this
     field defaults to thm.  The :corollary of a rule class object is
     the formula actually used to justify the rule created and thus
     determines the form of the rule.  Nqthm provided no similar
     capability: each rule was determined by thm, the theorem or axiom
     added.  ACL2 permits thm to be stated "elegantly" and then allows
     the :corollary of a rule class object to specify how that elegant
     statement is to be interpreted as a rule.  For the rule class
     object to be well-formed, its (defaulted) :corollary, term, must
     follow from thm.  Unless term is trivially implied by thm, using
     little more than propositional logic, the formula (implies thm
     term) is submitted to the theorem prover and the proof attempt
     must be successful.  During that proof attempt the values of
     :hints, :instructions, and :otf-flg, as provided in the rule class
     object, are provided as arguments to the prover.  Such auxiliary
     proofs give the sort of output that one expects from the prover.
     However, as noted above, corollaries that follow trivially are not
     submitted to the prover; thus, such corollaries cause no prover
     output.

     Note that before term is stored, all calls of macros in it are
     expanded away.  See TRANS.

     :Hints, :instructions, :otf-flg -- the values of these fields must
     satisfy the same restrictions placed on the fields of the same
     names in defthm.  These values are passed to the recursive call of
     the prover used to establish that the :corollary of the rule class
     object follows from the theorem or axiom thm.

     :Type-set -- this field may be supplied only if the :class is
     :type-set-inverter.  When provided, the value must be a type-set,
     an integer in a certain range.  If not provided, an attempt is
     made to compute it from the corollary.  See
     TYPE-SET-INVERTER.

     :Typed-term -- this field may be supplied only if the :class is
     :type-prescription.  When provided, the value is the term for which
     the :corollary is a type-prescription lemma.  If no :typed-term is
     provided in a :type-prescription rule class object, we try to
     compute heuristically an acceptable term.  See
     TYPE-PRESCRIPTION.

     :Trigger-terms -- this field may be supplied only if the :class is
     :forward-chaining or :linear.  When provided, the value is a list
     of terms, each of which is to trigger the attempted application of
     the rule.  If no :trigger-terms is provided, we attempt to compute
     heuristically an appropriate set of triggers.  See
     FORWARD-CHAINING or see LINEAR.

     :Trigger-fns -- this field must (and may only) be supplied if the
     :class is :meta.  Its value must be a list of function symbols.
     Terms with these symbols trigger the application of the rule.  See
     META.

     :Clique and :controller-alist -- these two fields may only be
     supplied if the :class is :definition.  If they are omitted, then
     ACL2 will attempt to guess them.  Suppose the :corollary of the
     rule is (implies hyp (equiv (fn a1 ... an) body)).  The value of
     the :clique field should be a true list of function symbols, and if
     non-nil must include fn.  These symbols are all the members of the
     mutually recursive clique containing this definition of fn.  That
     is, a call of any function in :clique is considered a "recursive
     call" for purposes of the expansion heuristics.  The value of the
     :controller-alist field should be an alist that maps each function
     symbol in the :clique to a list of t's and nil's of length equal
     to the arity of the function.  For example, if :clique consists of
     just two symbols, fn1 and fn2, of arities 2 and 3 respectively,
     then ((fn1 t nil) (fn2 nil t t)) is a legal value of
     :controller-alist.  The value associated with a function symbol in
     this alist is a "mask" specifying which argument slots of the
     function "control" the recursion for heuristic purposes.  Sloppy
     choice of :clique or :controller-alist can result in infinite
     expansion and stack overflow.

     :Install-body -- this field may only be supplied if the :class is
     :definition.  Its value must be t, nil, or the default,
     :normalize.  A value of t or :normalize will cause ACL2 to install
     this rule as the new body of the function being "defined" (fn in
     the paragraph just above); hence this definition will be installed
     for future :expand hints.  Furthermore, if this field is omitted
     or the value is :normalize, then this definition will be
     simplified using the so-called "normalization" procedure that is
     used when processing definitions made with defun.  You must
     explicitly specify :install-body nil in the following cases: fn
     (as above) is a member of the value of constant
     *definition-minimal-theory*, the arguments are not a list of
     distinct variables, equiv (as above) is not equal, or there are
     free variables in the hypotheses or right-hand side (see
     FREE-VARIABLES).  However, supplying :install-body nil will not
     affect the rewriter's application of the :definition rule, other
     than to avoid using the rule to apply :expand hints.  If a
     definition rule equates (f a1 ... ak) with body but there are
     hypotheses, hyps, then :expand hints will replace terms (f term1
     ... termk) by corresponding terms (if hyps body (hide (f term1 ...
     termk))).

     :Loop-stopper -- this field may only be supplied if the class is
     :rewrite.  Its value must be a list of entries each consisting of
     two variables followed by a (possibly empty) list of functions,
     for example ((x y binary-+) (u v foo bar)).  It will be used to
     restrict application of rewrite rules by requiring that the list
     of instances of the second variables must be "smaller" than the
     list of instances of the first variables in a sense related to the
     corresponding functions listed; see LOOP-STOPPER.  The
     list as a whole is allowed to be nil, indicating that no such
     restriction shall be made.  Note that any such entry that contains
     a variable not being instantiated, i.e., not occurring on the left
     side of the rewrite rule, will be ignored.  However, for
     simplicity we merely require that every variable mentioned should
     appear somewhere in the corresponding :corollary formula.

     :Pattern, :Condition, :Scheme -- the first and last of these
     fields must (and may only) be supplied if the class is :induction.
     :Condition is optional but may only be supplied if the class is
     :induction.  The values must all be terms and indicate,
     respectively, the pattern to which a new induction scheme is to be
     attached, the condition under which the suggestion is to be made,
     and a term which suggests the new scheme.  See INDUCTION.

     :Match-free -- this field must be :all or :once and may be
     supplied only if the :class is either :rewrite, :linear, or
     :forward-chaining.  See FREE-VARIABLES for a description
     of this field.  Note: Although this field is intended to be used
     for controlling retries of matching free variables in hypotheses,
     it is legal to supply it even if there are no such free variables.
     This can simplify the automated generation of rules, but note
     that when :match-free is supplied, the warning otherwise provided
     for the presence of free variables in hypotheses will be
     suppressed.

     Backchain-limit-lst -- this field may be supplied only if the
     :class is either :rewrite, :meta, :linear, or :type-prescription.
     It is further required either only one rule is generated from the
     formula or, at least, every such rule has the same list of
     hypotheses.  The value for :backchain-limit-lst must be nil; a
     non-negative integer; or, except in the case of :meta rules, a true
     list each element of which is either nil or a non-negative
     integer.  If it is a list, its length must be equal to the number
     of hypotheses of the rule and each item in the list is the
     "backchain limit" associated with the corresponding hypothesis.
     If backchain-limit-lst is a non-negative integer, it is defaulted
     to a list of the appropriate number of repetitions of that
     integer.  The backchain limit of a hypothesis is used to limit the
     effort that ACL2 will expend when relieving the hypothesis.  If it
     is NIL, no new limits are imposed; if it is an integer, the
     hypothesis will be limited to backchaining at most that many
     times.  Note that backchaining may be further limited by a global
     backchain-limit; see BACKCHAIN-LIMIT for details.  For a
     different way to reign in the rewriter, see
     REWRITE-STACK-LIMIT.  Jared Davis has pointed out that you can
     set this field to 0 to avoid any attempt to relieve forced
     hypotheses, which can lead to a significant speed-up in some cases.

Once thm has been proved (in the case of defthm) and each rule class
object has been checked for well-formedness (which might require
additional proofs), we consider each rule class object in turn to
generate and add rules.  Let :class be the class keyword token of the
ith class object (counting from left to right).  Generate the rune
(:class name . x), where x is nil if there is only one class and
otherwise x is i.  Then, from the :corollary of that object, generate
one or more rules, each of which has the name (:class name . x).  See
the :doc entry for each rule class to see how formulas determine rules.
Note that it is in principle possible for several rules to share the
same name; it happens whenever a :corollary determines more than one
rule.  This in fact only occurs for :rewrite, :linear, and
:forward-chaining class rules and only then if the :corollary is
essentially a conjunction.  (See the documentation for rewrite, linear,
or forward-chaining for details.)

BUILT-IN-CLAUSE    to build a clause into the simplifier

See RULE-CLASSES for a general discussion of rule classes and
how they are used to build rules from formulas.  A :built-in-clause
rule can be built from any formula other than propositional
tautologies.  Roughly speaking, the system uses the list of built-in
clauses as the first method of proof when attacking a new goal.  Any
goal that is subsumed by a built in clause is proved "silently."

ACL2 maintains a set of "built-in" clauses that are used to
short-circuit certain theorem proving tasks.  We discuss this at length
below.  When a theorem is given the rule class :built-in-clause ACL2
flattens the implies and and structure of the :corollary formula so as
to obtain a set of formulas whose conjunction is equivalent to the
given corollary.  It then converts each of these to clausal form and
adds each clause to the set of built-in clauses.

For example, the following :corollary (regardless of the definition of
abl)

     (and (implies (and (true-listp x)
                        (not (equal x nil)))
                   (< (acl2-count (abl x))
                      (acl2-count x)))
          (implies (and (true-listp x)
                        (not (equal nil x)))
                   (< (acl2-count (abl x))
                      (acl2-count x))))

will build in two clauses,

     {(not (true-listp x))
      (equal x nil)
      (< (acl2-count (abl x)) (acl2-count x))}

and

     {(not (true-listp x))
      (equal nil x)
      (< (acl2-count (abl x)) (acl2-count x))}.

We now give more background.

Recall that a clause is a set of terms, implicitly representing the
disjunction of the terms.  Clause c1 is "subsumed" by clause c2 if some
instance of c2 is a subset c1.

For example, let c1 be

     {(not (consp l))
      (equal a (car l))
      (< (acl2-count (cdr l)) (acl2-count l))}.

Then c1 is subsumed by c2, shown below,

     {(not (consp x))
      ; second term omitted here
      (< (acl2-count (cdr x)) (acl2-count x))}

because we can instantiate x in c2 with l to obtain a subset of c1.

Observe that c1 is the clausal form of

     (implies (and (consp l)
                   (not (equal a (car l))))
              (< (acl2-count (cdr l)) (acl2-count l))),

c2 is the clausal form of

     (implies (consp l)
              (< (acl2-count (cdr l)) (acl2-count l)))

and the subsumption property just means that c1 follows trivially from
c2 by instantiation.

The set of built-in clauses is just a set of known theorems in clausal
form.  Any formula that is subsumed by a built-in clause is thus a
theorem.  If the set of built-in theorems is reasonably small, this
little theorem prover is fast.  ACL2 uses the "built-in clause check"
in four places: (1) at the top of the iteration in the prover - thus if
a built-in clause is generated as a subgoal it will be recognized when
that goal is considered, (2) within the simplifier so that no built-in
clause is ever generated by simplification, (3) as a filter on the
clauses generated to prove the termination of recursively defun'd
functions and (4) as a filter on the clauses generated to verify the
guards of a function.

The latter two uses are the ones that most often motivate an extension
to the set of built-in clauses.  Frequently a given formalization
problem requires the definition of many functions which require
virtually identical termination and/or guard proofs.  These proofs can
be short-circuited by extending the set of built-in clauses to contain
the most general forms of the clauses generated by the definitional
schemes in use.

The attentive user might have noticed that there are some recursive
schemes, e.g., recursion by cdr after testing consp, that ACL2 just
seems to "know" are ok, while for others it generates measure clauses
to prove.  Actually, it always generates measure clauses but then
filters out any that pass the built-in clause check.  When ACL2 is
initialized, the clause justifying cdr recursion after a consp test is
added to the set of built-in clauses.  (That clause is c2 above.)

Note that only a subsumption check is made; no rewriting or
simplification is done.  Thus, if we want the system to "know" that cdr
recursion is ok after a negative atom test (which, by the definition of
atom, is the same as a consp test), we have to build in a second
clause.  The subsumption algorithm does not "know" about commutative
functions.  Thus, for predictability, we have built in commuted
versions of each clause involving commutative functions.  For example,
we build in both

     {(not (integerp x))
      (< 0 x)
      (= x 0)
      (< (acl2-count (+ -1 x)) (acl2-count x))}

and the commuted version

     {(not (integerp x))
      (< 0 x)
      (= 0 x)
      (< (acl2-count (+ -1 x)) (acl2-count x))}

so that the user need not worry whether to write (= x 0) or (= 0 x) in
definitions.

:built-in-clause rules added by the user can be enabled and disabled.

CLAUSE-PROCESSOR    make or apply a :clause-processor rule (goal-level simplifier)

Also see DEFINE-TRUSTED-CLAUSE-PROCESSOR for documentation of
an analogous utility that does not require the clause-processor to be
proved correct.  But please read the present documentation before
reading about that utility.  Both utilities designate functions
"clause-processors".  Such functions must be executable -- hence not
constrained by virtue of being introduced in the signature of an
encapsulate -- and must respect stobj and output arity restrictions.
For example, something like (car (mv ...)) is illegal; also see
SIGNATURE.

We begin this documentation with an introduction, focusing on an
example, and then conclude with details.  You might find it most useful
simply to look at the examples in distributed directory
books/clause-processors/; see file Readme.lsp in that directory.

A :clause-processor rule installs a simplifier at the level of goals,
where a goal is represented as a _clause_: a list of terms that is
implicitly viewed as a disjunction (the application of OR).  For
example, if ACL2 prints a goal in the form (implies (and p q) r), then
the clause might be the one-element list containing the internal
representation of this term -- (implies (if p q 'nil) r) -- but more
likely, the corresponding clause is ((not p) (not q) r).  Note that the
members of a clause are _translated_ terms; see TERM.  For
example, they do not contains calls of the macro AND, and constants are
quoted.

Note that clause-processor simplifiers are similar to metafunctions, and
similar efficiency considerations apply.  See META, in
particular the discussion on how to "make a metafunction maximally
efficient."

Unlike rules of class :meta, rules of class :clause-processor must be
applied by explicit :clause-processor hints; they are not applied
automatically (unless by way of computed hints; see
COMPUTED-HINTS).  But :clause-processor rules can be useful in
situations for which it is more convenient to code a simplifier that
manipulates the entire goal clause rather than individual subterms of
terms in the clause.

We begin with a simple illustrative example: a clause-processor that
assumes an alleged fact and creates a separate goal to prove that fact.
We can extend the hypotheses of the current goal with a term by adding
the negation of that term to the clause (disjunctive) representation of
that goal.  So the following returns two clauses: the result of adding
term as a hypothesis to the input clause, as just described, and a
second clause consisting only of that term.

     (defun note-fact-clause-processor (cl term)
       (declare (xargs :guard t)) ; optional, for better efficiency
       (list (cons (list 'not term)
                   cl)
             (list term)))

As with :meta rules, we need to introduce a suitable evaluator; see
DEFEVALUATOR if you want details.  Since we expect to reason
about the function NOT, because of its role in
note-fact-clause-processor as defined above, we include NOT in the set
of functions known to this evaluator.  We also include IF, as is often
a good idea.

     (defevaluator evl0 evl0-list
       ((not x) (if x y z)))

ACL2 can now prove the following theorem automatically.  (Of course,
:clause-processor rules about clause-processor functions less trivial
than note-fact-clause-processor may require lemmas to be proved first!)
The function disjoin takes a clause and returns its disjunction (the
result of applying OR to its members), and conjoin-clauses applies
disjoin to every element of a given list of clauses and then conjoins
(applies AND) to the corresponding list of resulting terms.

     (defthm correctness-of-note-fact-clause-processor
       (implies (and (pseudo-term-listp cl)
                     (alistp a)
                     (evl0 (conjoin-clauses
                            (note-fact-clause-processor cl term))
                           a))
                (evl0 (disjoin cl) a))
       :rule-classes :clause-processor)

Now let us submit a silly but illustrative example theorem to ACL2, to
show how a corresponding :clause-processor hint is applied.  The hint
says to apply the clause-processor function,
note-fact-clause-processor, to the current goal clause and a "user
hint" as the second argument of that function, in this case (equal a
a).  Thus, a specific variable, clause, is always bound to the current
goal clause for the evaluation of the :clause-processor hint, to
produce a list of clauses.  Since two subgoals are created below, we
know that this list contained two clauses.  Indeed, these are the
clauses returned when note-fact-clause-processor is applied to two
arguments:  the current clause, which is the one-element list ((equal
(car (cons x y)) x)), and the user hint, (equal a a).

     ACL2 !>(thm (equal (car (cons x y))
                        x)
                 :hints
                 (("Goal"
                   :clause-processor
                   (note-fact-clause-processor clause '(equal a a)))))

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

     We now apply the verified :CLAUSE-PROCESSOR function NOTE-FACT-CLAUSE-
     PROCESSOR to produce two new subgoals.

     Subgoal 2
     (IMPLIES (EQUAL A A)
              (EQUAL (CAR (CONS X Y)) X)).

     But we reduce the conjecture to T, by the :executable-counterpart of
     IF and the simple :rewrite rule CAR-CONS.

     Subgoal 1
     (EQUAL A A).

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

     Q.E.D.

     Summary
     Form:  ( THM ...)
     Rules: ((:EXECUTABLE-COUNTERPART IF)
             (:EXECUTABLE-COUNTERPART NOT)
             (:FAKE-RUNE-FOR-TYPE-SET NIL)
             (:REWRITE CAR-CONS))
     Warnings:  None
     Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)

     Proof succeeded.
     ACL2 !>

That concludes our introduction to clause-processor rules and hints.
We turn now to detailed documentation.

The signature of a clause-processor function, CL-PROC, must have one of
the following forms.  Here, each st_i is a stobj (possibly state) while
the other parameters and results are not stobjs (see DEFSTOBJ).
Note that there need not be input stobjs in [3] -- i.e., k can be 0 --
and even if there are, there need not be output stobjs.

     [1]  ((CL-PROC cl) => cl-list)

     [2]  ((CL-PROC cl hint) => cl-list)

     [3]  ((CL-PROC cl hint st_1 ... st_k) => (erp cl-list st_i1 ... st_in))

In [3], we think of the first component of the result as an error flag.
Indeed, a proof will instantly abort if that error flag is not nil.

We next discuss the legal forms of :clause-processor rules, followed
below by a discussion of :clause-processor hints.  In the discussion
below, we use lower-case names to represent specific symbols, for
example implies, and we use upper-case names to represent more
arbitrary pieces of syntax (which we will describe), for example, CL.

If a :rule-classes specification includes :clause-processor, then the
corresponding term must have the form

     (implies (and (pseudo-term-listp CL)
                   (alistp A)
                   (EVL (conjoin-clauses <CL-LIST>)
                         B))
              (EVL (disjoin CL) A))

where: EVL is a known evaluator; CL and A are distinct non-stobj
variables; and <CL-LIST> is an expression representing the clauses
returned by the clause-processor function CL-PROC, whose form depends on
the signature of that function, as follows.  Typically B is A, but it
can be any term (useful when generalization is occurring; see the
example "Test generalizing alist" in
books/clause-processors/basic-examples.lisp).  For cases [1] and [2]
above, <CL-LIST> is of the form (CL-PROC CL) or (CL-PROC CL HINT),
respectively, where in the latter case HINT is a non-stobj variable
distinct from the variables CL and A.  For case [3], <CL-LIST> is of
the form

     (clauses-result (CL-PROC CL HINT st_1 ... st_k))

where the st_i are the specific stobj names mentioned in [3].
Logically, clauses-result returns the cadr if the car is NIL, and
otherwise (for the error case) returns a list containing the empty
(false) clause.  So in the non-error case, clauses-result picks out the
second result, denoted cl-list in [3] above, and in the error case the
implication above trivially holds.

In the above theorem, we are asked to prove (EVL (disjoin CL) A)
assuming that the conjunction of all clauses produced by the clause
processor evaluates to a non-nil value under some alist B.  In fact, we
can choose B so as to allow us to assume evaluations of the generated
clauses over many different alists.  This technique is discussed in the
distributed book books/clause-processors/multi-env-trick.lisp, which
introduces some macros that may be helpful in accomplishing proofs of
this type.

The clause-processor function, CL, must have a guard that ACL2 can
trivially prove from the hypotheses that the first argument of CL is
known to be a pseudo-term-listp and any stobj arguments are assumed to
satisfy their stobj predicates.

Next we specify the legal forms for :clause-processor hints.  These
depend on the signature as described in [1] through [3] above.  Below,
as above, CL-PROC is the clause-processor function, and references to
"clause" refer to that exact variable (not, for example, to cl).  In
each of the three cases, the forms shown for that case are equivalent;
in particular, the :function syntax is simply a convenience for the
final form in each case.

Signature [1], ((cl-proc cl) => cl-list):

     :clause-processor CL-PROC
     :clause-processor (:function CL-PROC)
     :clause-processor (CL-PROC clause)

or any term macroexpanding to (CL-PROC clause).

Signature [2], ((cl-proc cl hint) => cl-list):

     :clause-processor (:function CL-PROC :hint HINT)
     :clause-processor (CL-PROC clause HINT)

or any term macroexpanding to (CL-PROC clause HINT), where HINT is any
term with at most CLAUSE free.

Signature [3], ((CL-PROC cl hint ...) => (erp cl-list ...))

     :clause-processor (:function CL-PROC :hint HINT)
     :clause-processor (CL-PROC clause HINT st_1 ... st_k)

or any term macroexpanding to (CL-PROC clause HINT st_1 ... st_k), where
HINT is any term with at most CLAUSE free.

A :clause-processor hint causes the proof to abort if the result
returned by evaluating the suitable CL-PROC call, as above, is not a
list of clauses, i.e., a list of (translated) term lists.  The proof
also aborts if in case [3] the first (erp) value returned is not nil,
in which case erp is used for printing an error message as follows: if
it is a string, then that string is printed; but if it is a non-empty
true list whose first element is a string, then it is printed as though
by (fmt ~@0 (list (cons #\0 erp)) ...) (see FMT).  Otherwise, a
non-nil erp value causes a generic error message to be printed.

If there is no error as above, but the CL-PROC call returns clause list
whose single element is equal to the input clause, then the hint is
ignored since we are left with the goal with which we started.  In that
case, the other prover processes are then applied as usual.

You can see all current :clause-processor rules by issuing the following
command: (print-clause-processor-rules).

The following paper discusses ACL2 clause-processors at a high level
suitable for a non-ACL2 audience:

     M. Kaufmann, J S. Moore, S. Ray, and E. Reeber, "Integrating
     External Deduction Tools with ACL2."  _Journal of Applied Logic_
     (Special Issue: Empirically Successful Computerized Reasoning),
     Volume 7, Issue 1, March 2009, pp. 3-25.  Also published online
     (DOI 10.1016/j.jal.2007.07.002).  Preliminary version in:
     Proceedings of the 6th International Workshop on the
     Implementation of Logics (IWIL 2006) (C. Benzmueller, B. Fischer,
     and G. Sutcliffe, editors), CEUR Workshop Proceedings Vol. 212,
     Phnom Penh, Cambodia, pp. 7-26, November 2006,
     `http://ceur-ws.org/Vol-212/'.

COMPOUND-RECOGNIZER    make a rule used by the typing mechanism

See RULE-CLASSES for a general discussion of rule classes and
how they are used to build rules from formulas.  An example :corollary
formula from which a :compound-recognizer rule might be built is:

     Example:
     (implies (alistp x)         When (alistp x) is assumed true,
              (true-listp x))    add the additional hypothesis that x
                                 is of primitive type true-listp.

     General Forms:
     (implies (fn x) concl)               ; (1)
     (implies (not (fn x)) concl)         ; (2)
     (and (implies (fn x) concl1)         ; (3)
          (implies (not (fn x)) concl2))
     (if (fn x) concl1 concl2)            ; (4)
     (iff (fn x) concl)                   ; (5)
     (equal (fn x) concl)                 ; (6)

where fn is a Boolean valued function of one argument, x is a variable
symbol, and the system can deduce some restriction on the primitive
type of x from the assumption that concl holds.  The third restriction
is vague but one way to understand it is to weaken it a little to "and
concl is a non-tautological conjunction or disjunction of the primitive
type recognizers listed below."

The primitive ACL2 types and a suitable primitive recognizing
expression for each are listed below.

       type                suitable primitive recognizer

       zero                (equal x 0)
       negative integers   (and (integerp x) (< x 0))
       positive integers   (and (integerp x) (> x 0))
       negative ratio      (and (rationalp x)
                                (not (integerp x))
                                (< x 0))
       positive ratio      (and (rationalp x)
                                (not (integerp x))
                                (> x 0))
       complex rational    (complex-rationalp x)
       nil                 (equal x nil)
       t                   (equal x t)
       other symbols       (and (symbolp x)
                                (not (equal x nil))
                                (not (equal x t)))
       proper conses       (and (consp x)
                                (true-listp x))
       improper conses     (and (consp x)
                                (not (true-listp x)))
       strings             (stringp x)
       characters          (characterp x)

Thus, a suitable concl to recognize the naturals would be (or (equal x
0) (and (integerp x) (> x 0))) but it turns out that we also permit
(and (integerp x) (>= x 0)).  Similarly, the true-lists could be
specified by

     (or (equal x nil) (and (consp x) (true-listp x)))

but we in fact allow (true-listp x).  When time permits we will
document more fully what is allowed or implement a macro that permits
direct specification of the desired type in terms of the primitives.

There are essentially four forms of :compound-recognizer rules, as the
third and fourth forms are equivalent, as are the fifth and sixth.  We
explain how such rules are used by considering the individual forms.

Consider a rule of the first form, (implies (fn x) concl).  The effect
of such a rule is that when the rewriter assumes (fn x) true, as it
would while diving through (if (fn x) xxx ...) to rewrite xxx, it
restricts the type of x as specified by concl.  However, when assuming
(fn x) false, as necessary in (if (fn x) ... xxx), the rule permits no
additional assumptions about the type of x.  For example, if fn is
primep, i.e., the predicate that recognizes prime numbers, then
(implies (primep x) (and (integerp x) (>= x 0))) is a compound
recognizer rule of the first form.  When (primep x) is assumed true,
the rewriter gains the additional information that x is a natural
number.  When (primep x) is assumed false, no additional information is
gained -- since x may be a non-prime natural or may not even be a
natural.

The second general form addresses itself to the symmetric case, when
assuming (fn x) false permits type restrictions on x but assuming (fn
x) true permits no such restrictions.  For example, if we defined exprp
to be the recognizer for well-formed expressions for some language in
which all symbols, numbers, character objects and strings were
well-formed -- e.g., the well-formedness rules only put restrictions on
expressions represented by consps -- then the theorem (implies (not
(exprp x)) (consp x)) is a rule of the second form.  Assuming (exprp x)
true tells us nothing about the type of x; assuming it false tells us x
is a consp.

The third and fourth general forms, which are really equivalent, address
themselves to the case where one type may be deduced from (fn x) and a
generally unrelated type may be deduced from its negation.  If we
modified the expression recognizer above so that character objects are
illegal, then rules of the third and fourth forms are

     (and (implies (exprp x) (not (characterp x)))
          (implies (not (exprp x)) (or (consp x) (characterp x)))).
     (if (exprp x)
         (not (characterp x))
       (or (consp x) (characterp x)))

Finally, rules of the fifth and sixth classes address the case where fn
recognizes all and only the objects whose type is described.  In these
cases, fn is really just a new name for some "compound recognizers."
The classic example is (booleanp x), which is just a handy combination
of two primitive types:

     (iff (booleanp x) (or (equal x t) (equal x nil))).

Often it is best to disable fn after proving that it is a compound
recognizer, since (fn x) will not be recognized as a compound
recognizer once it has been expanded.

Every time you prove a new compound recognizer rule about fn it
overrides all previously proved compound recognizer rules about fn.
Thus, if you want to establish the type implied by (fn x) and you want
to establish the type implied by (not (fn x)), you must prove a
compound recognizer rule of the third, fourth, fifth, or sixth forms.
Proving a rule of the first form followed by one of the second only
leaves the second fact in the data base.

Compound recognizer rules can be disabled with the effect that older
rules about fn, if any, are exposed.

If you prove more than one compound recognizer rule for a function, you
may see a *warning* message to the effect that the new rule is not as
"restrictive" as the old.  That is, the new rules do not give the
rewriter strictly more type information than it already had.  The new
rule is stored anyway, overriding the old, if enabled.  You may be
playing subtle games with enabling or rewriting.  But two other
interpretions are more likely, we think.  One is that you have
forgotten about an earlier rule and should merely print it out to make
sure it says what you know and then forget your new rule.  The other is
that you meant to give the system more information and the system has
simply been unable to extract the intended type information from the
term you placed in the conclusion of the new rule.  Given our lack of
specificity in saying how type information is extracted from rules, you
can hardly blame yourself for this problem.  Sorry.  If you suspect
you've been burned this way, you should rephrase the new rule in terms
of the primitive recognizing expressions above and see if the warning
is still given.  It would also be helpful to let us see your example so
we can consider it as we redesign this stuff.

Compound recognizer rules are similar to :forward-chaining rules in
that the system deduces new information from the act of assuming
something true or false.  If a compound recognizer rule were stored as
a forward chaining rule it would have essentially the same effect as
described, when it has any effect at all.  The important point is that
:forward-chaining rules, because of their more general and expensive
form, are used "at the top level" of the simplification process: we
forward chain from assumptions in the goal being proved.  But compound
recognizer rules are built in at the bottom-most level of the
simplifier, where type reasoning is done.

All that said, compound recognizer rules are a rather fancy,
specialized mechanism.  It may be more appropriate to create
:forward-chaining rules instead of :compound-recognizer rules.

CONGRUENCE    the relations to maintain while simplifying arguments

See RULE-CLASSES for a general discussion of rule classes and
how they are used to build rules from formulas.  An example :corollary
formula from which a :congruence rule might be built is:

     Example:
     (implies (set-equal x y)
              (iff (memb e x) (memb e y))).

Also see DEFCONG and see EQUIVALENCE.

     General Form:
     (implies (equiv1 xk xk-equiv)
              (equiv2 (fn x1... xk       ...xn)
                      (fn x1... xk-equiv ...xn)))

where equiv1 and equiv2 are known equivalence relations, fn is an n-ary
function symbol and the xi and xk-equiv are all distinct variables.
The effect of such a rule is to record that the equiv2-equivalence of
fn-expressions can be maintained if, while rewriting the kth argument
position, equiv1-equivalence is maintained.  See EQUIVALENCE
for a general discussion of the issues.  We say that equiv2, above, is
the "outside equivalence" in the rule and equiv1 is the "inside
equivalence for the kth argument"

The macro form (defcong equiv1 equiv2 (fn x1 ... x1) k) is an
abbreviation for a defthm of rule-class :congruence that attempts to
establish that equiv2 is maintained by maintaining equiv1 in fn's kth
argument.  The defcong macro automatically generates the general
formula shown above.  See DEFCONG.

The memb example above tells us that (memb e x) is propositionally
equivalent to (memb e y), provided x and y are set-equal.  The outside
equivalence is iff and the inside equivalence for the second argument
is set-equal.  If we see a memb expression in a propositional context,
e.g., as a literal of a clause or test of an if (but not, for example,
as an argument to cons), we can rewrite its second argument maintaining
set-equality.  For example, a rule stating the commutativity of append
(modulo set-equality) could be applied in this context.  Since equality
is a refinement of all equivalence relations, all equality rules are
always available.  See REFINEMENT.

All known :congruence rules about a given outside equivalence and fn
can be used independently.  That is, consider two :congruence rules
with the same outside equivalence, equiv, and about the same function
fn.  Suppose one says that equiv1 is the inside equivalence for the
first argument and the other says equiv2 is the inside equivalence for
the second argument.  Then (fn a b) is equiv (fn a' b') provided a is
equiv1 to a' and b is equiv2 to b'.  This is an easy consequence of the
transitivity of equiv.  It permits you to think independently about the
inside equivalences.

Furthermore, it is possible that more than one inside equivalence for a
given argument slot will maintain a given outside equivalence.  For
example, (length a) is equal to (length a') if a and a' are related
either by list-equal or by string-equal.  You may prove two (or more)
:congruence rules for the same slot of a function.  The result is that
the system uses a new, "generated" equivalence relation for that slot
with the result that rules of both (or all) kinds are available while
rewriting.

:Congruence rules can be disabled.  For example, if you have two
different inside equivalences for a given argument position and you
find that the :rewrite rules for one are unexpectedly preventing the
application of the desired rule, you can disable the rule that
introduced the unwanted inside equivalence.

_Remark on Replacing IFF by EQUAL._ You may encounter a warning
suggesting that a congruence rule "can be strengthened by replacing the
second equivalence relation, IFF, by EQUAL."  Suppose for example that
this warning occurs when you submit the following rule:

     (defcong equiv1 iff (fn x y) 2)

which is shorthand for the following:

     (defthm equiv1-implies-iff-fn-2
            (implies (equiv1 y y-equiv)
                     (iff (fn x y) (fn x y-equiv)))
            :rule-classes (:congruence))

The warning is telling you that ACL2 was able to deduce that fn always
returns a Boolean, and hence a trivial but useful consequence is
obtained by replacing iff by equal --

     (defcong equiv1 equal (fn x y) 2)

-- which is shorthand for the following:

     (defthm equiv1-implies-equal-fn-2
            (implies (equiv1 y y-equiv)
                     (equal (fn x y) (fn x y-equiv)))
            :rule-classes (:congruence))

If you have difficulty proving the latter directly, you can derive it
from the former by giving a suitable hint, minimally as follows.

     (defcong equiv1 equal (fn x y) 2
       :hints (("Goal"
                :use equiv1-implies-iff-fn-2
                :in-theory
                (union-theories '((:type-prescription fn))
                                (theory 'minimal-theory)))))

By heeding this warning, you may avoid unnecessary double-rewrite
warnings later.  We now explain why, but see DOUBLE-REWRITE for
relevant background material.

For example, suppose you have proved the "iff" version of the
congruence rule above, and later you submit the following rewrite rule.

     (defthm equal-list-perm
       (implies (equiv1 x y)
                (fn x y)))

Since fn is known to return a Boolean, ACL2 performs an optimization
that stores this rule as though it were the following.

     (defthm equal-list-perm
       (implies (equiv1 x y)
                (equal (fn x y) t)))

Thus, if ACL2's rewriter sees a term (fn a b) in a context where the
equivalence relation iff is not being maintained, then it cannot use
rule equiv1-implies-iff-fn-2, so it rewrites argument a without the
benefit of knowing that it suffices to maintain equiv1; and then it
caches the result.  When ACL2 subsequently attempts to relieve the
hypothesis (equiv1 x y), it will rewrite x simply by returning the
rewritten value of a from the result cache.  This is unfortunate if a
could have been rewritten more completely under maintainance of the
equivalence relation equiv1 -- which is legal in the hypothesis since a
is an argument of equiv1, which is an equivalence relation.  The user
who observes the warning from rule equiv1-implies-iff-fn-2, and
replaces it with equiv1-implies-equal-fn-2, will avoid this unfortunate
case.

DEFINITION    make a rule that acts like a function definition

See RULE-CLASSES for a general discussion of rule classes and
how they are used to build rules from formulas.  An example :corollary
formula from which a :definition rule might be built is:

     Example:
     (implies (true-listp x)
              (equal (len x)
                     (if (null x)
                         0
                         (if (null (cdr x))
                             1
                             (+ 2 (len (cddr x)))))))

     General Form:
     (implies hyp (equiv (fn a1 ... an) body))

where equiv is an equivalence relation and fn is a function symbol
other than if, hide, force or case-split.  Such rules allow
"alternative" definitions of fn to be proved as theorems but used as
definitions.  These rules are not true "definitions" in the sense that
they (a) cannot introduce new function symbols and (b) do not have to be
terminating recursion schemes.  They are just conditional rewrite rules
that are controlled the same way we control recursive definitions.  We
call these "definition rules" or "generalized definitions".

Consider the general form above.  Generalized definitions are stored
among the :rewrite rules for the function "defined," fn above, but the
procedure for applying them is a little different.  During rewriting,
instances of (fn a1 ... an) are replaced by corresponding instances of
body provided the hyps can be established as for a :rewrite rule and
the result of rewriting body satisfies the criteria for function
expansion.  There are two primary criteria, either of which permits
expansion.  The first is that the "recursive" calls of fn in the
rewritten body have arguments that already occur in the goal
conjecture.  The second is that the "controlling" arguments to fn are
simpler in the rewritten body.

The notions of "recursive call" and "controllers" are complicated by the
provisions for mutually recursive definitions.  Consider a "clique" of
mutually recursive definitions.  Then a "recursive call" is a call to
any function defined in the clique and an argument is a "controller" if
it is involved in the measure that decreases in all recursive calls.
These notions are precisely defined by the definitional principle and
do not necessarily make sense in the context of generalized
definitional equations as implemented here.

But because the heuristics governing the use of generalized definitions
require these notions, it is generally up to the user to specify which
calls in body are to be considered recursive and what the controlling
arguments are.  This information is specified in the :clique and
:controller-alist fields of the :definition rule class.

The :clique field is the list of function symbols to be considered
recursive calls of fn.  In the case of a non-recursive definition, the
:clique field is empty; in a singly recursive definition, it should
consist of the singleton list containing fn; otherwise it should be a
list of all of the functions in the mutually recursive clique with this
definition of fn.

If the :clique field is not provided it defaults to nil if fn does not
occur as a function symbol in body and it defaults to the singleton
list containing fn otherwise.  Thus, :clique must be supplied by the
user only when the generalized definition rule is to be treated as one
of several in a mutually recursive clique.

The :controller-alist is an alist that maps each function symbol in the
:clique to a mask specifying which arguments are considered controllers.
The mask for a given member of the clique, fn, must be a list of t's
and nil's of length equal to the arity of fn.  A t should be in each
argument position that is considered a "controller" of the recursion.
For a function admitted under the principle of definition, an argument
controls the recursion if it is one of the arguments measured in the
termination argument for the function.  But in generalized definition
rules, the user is free to designate any subset of the arguments as
controllers.  Failure to choose wisely may result in the "infinite
expansion" of definitional rules but cannot render ACL2 unsound since
the rule being misused is a theorem.

If the :controller-alist is omitted it can sometimes be defaulted
automatically by the system.  If the :clique is nil, the
:controller-alist defaults to nil.  If the :clique is a singleton
containing fn, the :controller-alist defaults to the controller alist
computed by (defun fn args body).  (The user can obtain some control
over this analysis by setting the default ruler-extenders; see
RULER-EXTENDERS.)  If the :clique contains more than one function,
the user must supply the :controller-alist specifying the controllers
for each function in the clique.  This is necessary since the system
cannot determine and thus cannot analyze the other definitional
equations to be included in the clique.

For example, suppose fn1 and fn2 have been defined one way and it is
desired to make "alternative" mutually recursive definitions available
to the rewriter.  Then one would prove two theorems and store each as a
:definition rule.  These two theorems would exhibit equations
"defining" fn1 and fn2 in terms of each other.  No provision is here
made for exhibiting these two equations as a system of equations.  One
is proved and then the other.  It just so happens that the user intends
them to be treated as mutually recursive definitions.  To achieve this
end, both :definition rules should specify the :clique (fn1 fn2) and
should specify a suitable :controller-alist.  If, for example, the new
definition of fn1 is controlled by its first argument and the new
definition of fn2 is controlled by its second and third (and they each
take three arguments) then a suitable :controller-alist would be ((fn1
t nil nil) (fn2 nil t t)).  The order of the pairs in the alist is
unimportant, but there must be a pair for each function in the clique.

Inappropriate heuristic advice via :clique and :controller-alist can
cause "infinite expansion" of generalized definitions, but cannot render
ACL2 unsound.

Note that the actual definition of fn1 has the runic name (:definition
fn1).  The runic name of the alternative definition is (:definition
lemma), where lemma is the name given to the event that created the
generalized :definition rule.  This allows theories to switch between
various "definitions" of the functions.

By default, a :definition rule establishes the so-called "body" of a
function.  The body is used by :expand hints, and it is also used
heuristically by the theorem prover's preprocessing (the initial
simplification using "simple" rules that is controlled by the
preprocess symbol in :do-not hints), induction analysis, and the
determination for when to warn about non-recursive functions in rules.
The body is also used by some heuristics involving whether a function is
recursively defined, and by the expand, x, and x-dumb commands of the
proof-checker.

See RULE-CLASSES for a discussion of the optional field
:install-body of :definition rules, which controls whether a
:definition rule is used as described in the paragraph above.  Note
that even if :install-body nil is supplied, the rewriter will still
rewrite with the :definition rule; in that case, ACL2 just won't
install a new body for the top function symbol of the left-hand side of
the rule, which for example affects the application of :expand hints as
described in the preceding paragraph.  Also see SET-BODY and
see SHOW-BODIES for how to change the body of a function symbol.

Note only that if you prove a definition rule for function foo, say,
foo-new-def, you will need to refer to that definition as foo-new-def
or as (:DEFINITION foo-new-def).  That is because a :definition rule
does not change the meaning of the symbol foo for :use hints, nor does
it change the meaning of the symbol foo in theory expressions; see
THEORIES, in particular the discussion there of runic
designators.  Similarly :pe foo and :pf foo will still show the
original definition of foo.

The definitional principle, defun, actually adds :definition rules.
Thus the handling of generalized definitions is exactly the same as for
"real" definitions because no distinction is made in the implementation.
Suppose (fn x y) is defun'd to be body.  Note that defun (or defuns or
mutual-recursion) can compute the clique for fn from the syntactic
presentation and it can compute the controllers from the termination
analysis.  Provided the definition is admissible, defun adds the
:definition rule (equal (fn x y) body).

ELIM    make a destructor elimination rule

See RULE-CLASSES for a general discussion of rule classes and
how they are used to build rules from formulas.  Here we describe the
class of :elim rules, which is fundamentally quite different from the
more common class of :rewrite rules.  Briefly put, a :rewrite rule
replaces instances of its left-hand side with corresponding instances
of its right-hand side.  But an :elim rule, on the other hand, has the
effect of generalizing so-called "destructor" function applications to
variables.  In essence, applicability of a :rewrite rule is based on
matching its left-hand side, while applicability of an :elim rule is
based on the presence of at least one destructor term.

For example, a conjecture about (car x) and (cdr x) can be replaced by
a conjecture about new variables x1 and x2, as shown in the following
example.  (Run the command :mini-proveall and search for CAR-CDR-ELIM
to see the full proof containing this excerpt.)

     Subgoal *1/1'
     (IMPLIES (AND (CONSP X)
                   (TRUE-LISTP (REV (CDR X))))
              (TRUE-LISTP (APP (REV (CDR X)) (LIST (CAR X))))).

     The destructor terms (CAR X) and (CDR X) can be eliminated by using
     CAR-CDR-ELIM to replace X by (CONS X1 X2), (CAR X) by X1 and (CDR X)
     by X2.  This produces the following goal.

     Subgoal *1/1''
     (IMPLIES (AND (CONSP (CONS X1 X2))
                   (TRUE-LISTP (REV X2)))
              (TRUE-LISTP (APP (REV X2) (LIST X1)))).

     This simplifies, using primitive type reasoning, to

     Subgoal *1/1'''
     (IMPLIES (TRUE-LISTP (REV X2))
              (TRUE-LISTP (APP (REV X2) (LIST X1)))).

The resulting conjecture is often simpler and hence more amenable to
proof.

The application of an :elim rule thus replaces a variable by a term that
contains applications of so-called "destructor" functions to that
variable.  The example above is typical: the variable x is replaced by
the term (cons (car x) (cdr x)), which applies a so-called "constructor"
function, cons, to applications (car x) and (cdr x) of destructor
functions car and cdr to that same variable, x.  But that is only part
of the story.  ACL2 then generalizes the destructor applications (car
x) and (cdr x) to new variables x1 and x2, respectively, and ultimately
the result is a simpler conjecture.

More generally, the application of an :elim rule replaces a variable by
a term containing applications of destructors; there need not be a
clear-cut notion of "constructor."  But the situation described above
is typical, and we will focus on it, giving full details when we
introduce the "General Form" below.

The example above employs the following built-in :elim rule named
car-cdr-elim.

     Example:
     (implies (consp x)                      when (car v) or (cdr v) appears
              (equal (cons (car x) (cdr x))  in a conjecture, and v is a
                     x))                     variable, consider replacing v by
                                             (cons a b), for two new variables
                                             a and b.

     Notice that the situation is complicated a bit by the fact that this
     replacement is only valid if the variable being replaced a cons structure.
     Thus, when ACL2 applies car-cdr-elim to replace a variable v, it will
     split into two cases: one case in which (consp v) is true, in which v
     is replaced by (cons (car v) (cdr v)) and then (car v) and
     (cdr v) are generalized to new variables; and one case in which
     (consp v) is false.  In practice, (consp v) is often provable,
     perhaps even literally present as a hypotheses; then of course there is no
     need to introduce the second case.  That is why there is no such second case
     in the example above.

     You might find :elim rules to be useful whenever you have in mind a data
     type that can be built up from its fields with a ``constructor'' function and
     whose fields can be accessed by corresponding ``destructor'' functions.  So
     for example, if you have a ``house'' data structure that represents a house
     in terms of its address, price, and color, you might have a rule like the
     following.
          Example:
          (implies (house-p x)
                   (equal (make-house (address x)
                                      (price x)
                                      (color x))
                          x))

     The application of such a rule is entirely analogous to the application of
     the rule car-cdr-elim discussed above.  We discuss such rules and their
     application more carefully below.

     General Form:
     (implies hyp (equiv lhs x))

where equiv is a known equivalence relation (see DEFEQUIV); x
is a variable symbol; and lhs contains one or more terms (called
"destructor terms") of the form (fn v1 ... vn), where fn is a function
symbol and the vi are distinct variable symbols, v1, ..., vn include
all the variable symbols in the formula, no fn occurs in lhs in more
than one destructor term, and all occurrences of x in lhs are inside
destructor terms.

To use an :elim rule, the theorem prover waits until a conjecture has
been maximally simplified.  It then searches for an instance of some
destructor term (fn v1 ... vn) in the conjecture, where the instance for
x is some variable symbol, vi, and every occurrence of vi outside the
destructor terms is in an equiv-hittable position.  If such an instance
is found, then the theorem prover instantiates the :elim formula as
indicated by the destructor term matched; splits the conjecture into two
goals, according to whether the instantiated hypothesis, hyp, holds; and
in the case that it does hold, generalizes all the instantiated
destructor terms in the conjecture to new variables and then replaces
vi in the conjecture by the generalized instantiated lhs.  An
occurrence of vi is "equiv-hittable" if sufficient congruence rules
(see DEFCONG) have been proved to establish that the
propositional value of the clause is not altered by replacing that
occurrence of vi by some equiv-equivalent term.

If an :elim rule is not applied when you think it should have been, and
the rule uses an equivalence relation, equiv, other than equal, it is
most likely that there is an occurrence of the variable that is not
equiv-hittable.  Easy occurrences to overlook are those in the
governing hypotheses.  If you see an unjustified occurrence of the
variable, you must prove the appropriate congruence rule to allow the
:elim to fire.

Further examples of how ACL2 :elim rules are used may be found in the
corresponding discussion of "Elimation of Destructors" for Nqthm, in
Section 10.4 of A Computational Logic Handbook.

EQUIVALENCE    mark a relation as an equivalence relation

See RULE-CLASSES for a general discussion of rule classes and
how they are used to build rules from formulas.  An example :corollary
formula from which a :equivalence rule might be built is as follows.
(We assume that r-equal has been defined.)

     Example:
     (and (booleanp (r-equal x y))
          (r-equal x x)
          (implies (r-equal x y) (r-equal y x))
          (implies (and (r-equal x y)
                        (r-equal y z))
                   (r-equal x z))).

Also see DEFEQUIV.

     General Form:
     (and (booleanp (equiv x y))
          (equiv x x)
          (implies (equiv x y) (equiv y x))
          (implies (and (equiv x y)
                        (equiv y z))
                   (equiv x z)))

except that the order of the conjuncts and terms and the choice of
variable symbols is unimportant.  The effect of such a rule is to
identify equiv as an equivalence relation.  Note that only Boolean
2-place function symbols can be treated as equivalence relations.  See
CONGRUENCE and see REFINEMENT for closely related
concepts.

The macro form (defequiv equiv) is an abbreviation for a defthm of
rule-class :equivalence that establishes that equiv is an equivalence
relation.  It generates the formula shown above.  See DEFEQUIV.

When equiv is marked as an equivalence relation, its reflexivity,
symmetry, and transitivity are built into the system in a deeper way
than via :rewrite rules.  More importantly, after equiv has been shown
to be an equivalence relation, lemmas about equiv, e.g.,

     (implies hyps (equiv lhs rhs)),

when stored as :rewrite rules, cause the system to rewrite certain
occurrences of (instances of) lhs to (instances of) rhs.  Roughly
speaking, an occurrence of lhs in the kth argument of some
fn-expression, (fn ... lhs' ...), can be rewritten to produce (fn ...
rhs' ...), provided the system "knows" that the value of fn is
unaffected by equiv-substitution in the kth argument.  Such knowledge
is communicated to the system via "congruence lemmas."

For example, suppose that r-equal is known to be an equivalence
relation.  The :congruence lemma

     (implies (r-equal s1 s2)
              (equal (fn s1 n) (fn s2 n)))

informs the rewriter that, while rewriting the first argument of
fn-expressions, it is permitted to use r-equal rewrite-rules.  See
CONGRUENCE for details about :congruence lemmas.
Interestingly, congruence lemmas are automatically created when an
equivalence relation is stored, saying that either of the equivalence
relation's arguments may be replaced by an equivalent argument.  That
is, if the equivalence relation is fn, we store congruence rules that
state the following fact:

     (implies (and (fn x1 y1)
                   (fn x2 y2))
              (iff (fn x1 x2) (fn y1 y2)))

Another aspect of equivalence relations is that of "refinement."  We
say equiv1 "refines" equiv2 iff (equiv1 x y) implies (equiv2 x y).
:refinement rules permit you to establish such connections between your
equivalence relations.  The value of refinements is that if the system
is trying to rewrite something while maintaining equiv2 it is permitted
to use as a :rewrite rule any refinement of equiv2.  Thus, if equiv1 is
a refinement of equiv2 and there are equiv1 rewrite-rules available,
they can be brought to bear while maintaining equiv2.  See
REFINEMENT.

The system initially has knowledge of two equivalence relations,
equality, denoted by the symbol equal, and propositional equivalence,
denoted by iff.  Equal is known to be a refinement of all equivalence
relations and to preserve equality across all arguments of all
functions.

Typically there are five steps involved in introducing and using a new
equivalence relation, equiv.

     (1) Define equiv,

     (2) prove the :equivalence lemma about equiv,

     (3) prove the :congruence lemmas that show where equiv can be used
     to maintain known relations,

     (4) prove the :refinement lemmas that relate equiv to known
     relations other than equal, and

     (5) develop the theory of conditional :rewrite rules that drive
     equiv rewriting.

More will be written about this as we develop the techniques.  For now,
here is an example that shows how to make use of equivalence relations
in rewriting.

Among the theorems proved below is

     (defthm insert-sort-is-id
       (perm (insert-sort x) x))

Here perm is defined as usual with delete and is proved to be an
equivalence relation and to be a congruence relation for cons and
member.

Then we prove the lemma

     (defthm insert-is-cons
       (perm (insert a x) (cons a x)))

which you must think of as you would (insert a x) = (cons a x).

Now prove (perm (insert-sort x) x).  The base case is trivial.  The
induction step is

        (consp x)
      & (perm (insert-sort (cdr x)) (cdr x))

     -> (perm (insert-sort x) x).

Opening insert-sort makes the conclusion be

        (perm (insert (car x) (insert-sort (cdr x))) x).

Then apply the induction hypothesis (rewriting (insert-sort (cdr x)) to
(cdr x)), to make the conclusion be

     (perm (insert (car x) (cdr x)) x)

Then apply insert-is-cons to get (perm (cons (car x) (cdr x)) x).  But
we know that (cons (car x) (cdr x)) is x, so we get (perm x x) which is
trivial, since perm is an equivalence relation.

Here are the events.

     (encapsulate (((lt * *) => *))
       (local (defun lt (x y) (declare (ignore x y)) nil))
       (defthm lt-non-symmetric (implies (lt x y) (not (lt y x)))))

     (defun insert (x lst)
       (cond ((atom lst) (list x))
             ((lt x (car lst)) (cons x lst))
             (t (cons (car lst) (insert x (cdr lst))))))

     (defun insert-sort (lst)
       (cond ((atom lst) nil)
             (t (insert (car lst) (insert-sort (cdr lst))))))

     (defun del (x lst)
       (cond ((atom lst) nil)
             ((equal x (car lst)) (cdr lst))
             (t (cons (car lst) (del x (cdr lst))))))

     (defun mem (x lst)
       (cond ((atom lst) nil)
             ((equal x (car lst)) t)
             (t (mem x (cdr lst)))))

     (defun perm (lst1 lst2)
       (cond ((atom lst1) (atom lst2))
             ((mem (car lst1) lst2)
              (perm (cdr lst1) (del (car lst1) lst2)))
             (t nil)))

     (defthm perm-reflexive
       (perm x x))

     (defthm perm-cons
       (implies (mem a x)
                (equal (perm x (cons a y))
                       (perm (del a x) y)))
       :hints (("Goal" :induct (perm x y))))

     (defthm perm-symmetric
       (implies (perm x y) (perm y x)))

     (defthm mem-del
       (implies (mem a (del b x)) (mem a x)))

     (defthm perm-mem
       (implies (and (perm x y)
                     (mem a x))
                (mem a y)))

     (defthm mem-del2
       (implies (and (mem a x)
                     (not (equal a b)))
                (mem a (del b x))))

     (defthm comm-del
       (equal (del a (del b x)) (del b (del a x))))

     (defthm perm-del
       (implies (perm x y)
                (perm (del a x) (del a y))))

     (defthm perm-transitive
       (implies (and (perm x y) (perm y z)) (perm x z)))

     (defequiv perm)

     (in-theory (disable perm
                         perm-reflexive
                         perm-symmetric
                         perm-transitive))

     (defcong perm perm (cons x y) 2)

     (defcong perm iff (mem x y) 2)

     (defthm atom-perm
       (implies (not (consp x)) (perm x nil))
       :rule-classes :forward-chaining
       :hints (("Goal" :in-theory (enable perm))))

     (defthm insert-is-cons
       (perm (insert a x) (cons a x)))

     (defthm insert-sort-is-id
       (perm (insert-sort x) x))

     (defun app (x y) (if (consp x) (cons (car x) (app (cdr x) y)) y))

     (defun rev (x)
       (if (consp x) (app (rev (cdr x)) (list (car x))) nil))

     (defcong perm perm (app x y) 2)

     (defthm app-cons
       (perm (app a (cons b c)) (cons b (app a c))))

     (defthm app-commutes
       (perm (app a b) (app b a)))

     (defcong perm perm (app x y) 1
       :hints (("Goal" :induct (app y x))))

     (defthm rev-is-id (perm (rev x) x))

     (defun == (x y)
       (if (consp x)
           (if (consp y)
               (and (equal (car x) (car y))
                    (== (cdr x) (cdr y)))
               nil)
           (not (consp y))))

     (defthm ==-reflexive (== x x))

     (defthm ==-symmetric (implies (== x y) (== y x)))

     (defequiv ==)

     (in-theory (disable ==-symmetric ==-reflexive))

     (defcong == == (cons x y) 2)

     (defcong == iff (consp x) 1)

     (defcong == == (app x y) 2)

     (defcong == == (app x y) 1)

     (defthm rev-rev (== (rev (rev x)) x))

FORWARD-CHAINING    make a rule to forward chain when a certain trigger arises

See RULE-CLASSES for a general discussion of rule classes and
how they are used to build rules from formulas.  An example :corollary
formula from which a :forward-chaining rule might be built is:

     Example:
     (implies (and (p x) (r x))        when (p a) appears in a formula to be
              (q (f x)))               simplified, try to establish (r a) and
                                       if successful, add (q (f a)) to the
                                       known assumptions

To specify the triggering terms provide a non-empty list of terms as
the value of the :trigger-terms field of the rule class object.

     General Form:
     Any theorem, provided an acceptable triggering term exists.

Forward chaining rules are generated from the corollary term as follows.
First, every let expression is expanded away (hence, so is every let*
and lambda expression), as is every call of a so-called "guard holder"
(must-be-equal, prog2$, ec-call, mv-list, the).  If the resulting term
has the form (implies hyp concl), then concl is treated as a
conjunction, with one forward chaining rule with hypothesis hyp created
for each conjunct.  In the other case, where the corollary term is not
an implies, we process it as we process the conclusion in the first
case.

The :trigger-terms field of a :forward-chaining rule class object
should be a non-empty list of terms, if provided, and should have
certain properties described below.  If the :trigger-terms field is not
provided, it defaults to the singleton list containing the "atom" of
the first hypothesis of the formula.  (The atom of (not x) is x; the
atom of any other term is the term itself.)  If there are no hypotheses
and no :trigger-terms were provided, an error is caused.

A triggering term is acceptable if it is not a variable, a quoted
constant, a lambda application, a let- (or let*-) expression, or a
not-expression, and every variable symbol in the conclusion of the
theorem either occurs in the hypotheses or occurs in the trigger.

:Forward-chaining rules are used by the simplifier before it begins to
rewrite the literals of the goal.  (Forward chaining is thus carried
out from scratch for each goal.)  If any term in the goal is an
instance of a trigger of some forward chaining rule, we try to
establish the hypotheses of that forward chaining theorem (from the
negation of the goal).  To relieve a hypothesis we only use type
reasoning, evaluation of ground terms, and presence among our known
assumptions.  We do not use rewriting.  So-called free variables in
hypotheses are treated specially; see FREE-VARIABLES.  If all
hypotheses are relieved, we add the instantiated conclusion to our known
assumptions.

_Caution_.  Forward chaining does not actually add terms to the goals
displayed during proof attempts.  Instead, it extends an associated
_context_, called "assumptions" in the preceding paragraph, that ACL2
builds from the goal currently being proved.  The context starts out
with "obvious" consequences of the negation of the goal.  For example,
if the goal is

     (implies (and (p x) (q (f x)))
              (c x))

then the context notes that (p x) and (q (f x)) are non-nil and (c x)
is nil.  Forward chaining is then used to expand the context.  For
example, if a forward chaining rule has (f x) as a trigger term and has
body (implies (p x) (r (f x))), then the context is extended by binding
(r (f x)) to non-nil.  Note however that since (r (f x)) is put into
the context, not the goal, it is _not_ further simplified.  If f is an
enabled nonrecursive function symbol then this forward chaining rule
may well be useless, since calls of f may be expanded away.

However, forward-chaining does support the linear arithmetic reasoning
package.  For example, suppose that forward-chaining puts (< (f x) (g
x)) into the context.  Then this inequality also goes into the linear
arithmetic data base, together with suitable instances of linear lemmas
whose trigger term is a call of g.  See LINEAR.

FREE-VARIABLES    free variables in rules

As described elsewhere (see RULE-CLASSES), ACL2 rules are
treated as implications for which there are zero or more hypotheses hj
to prove.  In particular, rules of class :rewrite may look like this:

     (implies (and h1 ... hn)
              (fn lhs rhs))

Variables of hi are said to occur _free_ in the above :rewrite rule if
they do not occur in lhs or in any hj with j<i.  (To be precise, here
we are only discussing those variables that are not in the scope of a
let/let*/lambda that binds them.)  We also refer to these as the _free
variables_ of the rule.  ACL2 issues a warning or error when there are
free variables in a rule, as described below.  (Variables of rhs may be
considered free if they do not occur in lhs or in any hj.  But we do
not consider those in this discussion.)

In general, the _free variables_ of rules are those variables occurring
in their hypotheses (not let/let*/lambda-bound) that are not bound when
the rule is applied.  For rules of class :linear and :forward-chaining,
variables are bound by a trigger term.  (See RULE-CLASSES for a
discussion of the :trigger-terms field).  For rules of class
:type-prescription, variables are bound by the :typed-term field.

Let us discuss the method for relieving hypotheses of rewrite rules with
free variables.  Similar considerations apply to linear and
forward-chaining rules, while for other rules (in particular,
type-prescription rules), only one binding is tried, much as described
in the discussion about :once below.

See FREE-VARIABLES-EXAMPLES for more examples of how this all
works, including illustration of how the user can exercise some control
over it.  In particular, see FREE-VARIABLES-EXAMPLES-REWRITE
for an explanation of output from the break-rewrite facility in the
presence of rewriting failures involving free variables.

We begin with an example.  Does the proof of the thm below succeed?

     (defstub p2 (x y) t)

     (defaxiom p2-trans
       (implies (and (p2 x y)
                     (p2 y z))
                (equal (p2 x z) t))
       :rule-classes ((:rewrite :match-free :all)))

     (thm (implies (and (p2 a c)
                        (p2 a b)
                        (p2 c d))
                   (p2 a d)))

Consider what happens when the proof of the thm is attempted.  The ACL2
rewriter attempts to apply rule p2-trans to the conclusion, (p2 a d).
So, it binds variables x and z from the left-hand side of the
conclusion of p2-trans to terms a and d, respectively, and then
attempts to relieve the hypotheses of p2-trans.  The first hypothesis of
p2-trans, (p2 x y), is considered first.  Variable y is free in that
hypothesis, i.e., it has not yet been bound.  Since x is bound to a,
the rewriter looks through the context for a binding of y such that (p2
a y) is true, and it so happens that it first finds the term (p2 a b),
thus binding y to b.  Now it goes on to the next hypothesis, (p2 y z).
At this point y and z have already been bound to b and d; but (p2 b d)
cannot be proved.

So, in order for the proof of the thm to succeed, the rewriter needs to
backtrack and look for another way to instantiate the first hypothesis
of p2-trans.  Because :match-free :all has been specified, backtracking
does take place.  This time y is bound to c, and the subsequent
instantiated hypothesis becomes (p2 c d), which is true.  The
application of rule (p2-trans) succeeds and the theorem is proved.

If instead :match-free :all had been replaced by :match-free :once in
rule p2-trans, then backtracking would not occur, and the proof of the
thm would fail.

Next we describe in detail the steps used by the rewriter in dealing
with free variables.

ACL2 uses the following sequence of steps to relieve a hypothesis with
free variables, except that steps (1) and (3) are skipped for
:forward-chaining rules and step (3) is skipped for :type-prescription
rules.  First, if the hypothesis is of the form (force hyp0) or
(case-split hyp0), then replace it with hyp0.  (1) Suppose the
hypothesis has the form (equiv var term) where var is free and no
variable of term is free, and either equiv is equal or else equiv is a
known equivalence relation and term is a call of double-rewrite.  Then
bind var to the result of rewriting term in the current context.  (2)
Look for a binding of the free variables of the hypothesis so that the
corresponding instance of the hypothesis is known to be true in the
current context.  (3) Search all enabled, hypothesis-free rewrite rules
of the form (equiv lhs rhs), where lhs has no variables (other than
those bound by let, let*, or lambda), rhs is known to be true in the
current context, and equiv is typically equal but can be any equivalence
relation appropriate for the current context (see CONGRUENCE);
then attempt to bind the free variables so that the instantiated
hypothesis is lhs.  If all attempts fail and the original hypothesis is
a call of force or case-split, where forcing is enabled (see
FORCE) then the hypothesis is relieved, but in the split-off goals,
all free variables are bound to unusual names that call attention to
this odd situation.

When a rewrite or linear rule has free variables in the hypotheses, the
user generally needs to specify whether to consider only the first
instance found in steps (2) and (3) above, or instead to consider them
all.  Below we discuss how to specify these two options as ":once" or
":all" (the default), respectively.

Is it better to specify :once or :all?  We believe that :all is
generally the better choice because of its greater power, provided the
user does not introduce a large number of rules with free variables,
which has been known to slow down the prover due to combinatorial
explosion in the search (Steps (2) and (3) above).

Either way, it is good practice to put the "more substantial" hypotheses
first, so that the most likely bindings of free variables will be found
first (in the case of :all) or found at all (in the case of :once).  For
example, a rewrite rule like

     (implies (and (p1 x y)
                   (p2 x y))
              (equal (bar x) (bar-prime x)))

may never succeed if p1 is nonrecursive and enabled, since we may well
not find calls of p1 in the current context.  If however p2 is disabled
or recursive, then the above rule may apply if the two hypotheses are
switched.  For in that case, we can hope for a match of (p2 x y) in the
current context that therefore binds x and y; then the rewriter's full
power may be brought to bear to prove (p1 x y) for that x and y.

Moreover, the ordering of hypotheses can affect the efficiency of the
rewriter.  For example, the rule

     (implies (and (rationalp y)
                   (foo x y))
              (equal (bar x) (bar-prime x)))

may well be sub-optimal.  Presumably the intention is to rewrite (bar x)
to (bar-prime x) in a context where (foo x y) is explicitly known to be
true for some rational number y.  But y will be bound first to the
first term found in the current context that is known to represent a
rational number.  If the 100th such y that is found is the first one
for which (foo x y) is known to be true, then wasted work will have
been done on behalf of the first 99 such terms y -- unless :once has
been specified, in which case the rule will simply fail after the first
binding of y for which (rationalp y) is known to be true.  Thus, a
better form of the above rule is almost certainly the following.

     (implies (and (foo x y)
                   (rationalp y))
              (equal (bar x) (bar-prime x)))

_Specifying `once' or `all'._ One method for specifying :once or :all
for free-variable matching is to provide the :match-free field of the
:rule-classes of the rule, for example, (:rewrite :match-free :all).
See RULE-CLASSES.  However, there are global events that can be
used to specify :once or :all; see SET-MATCH-FREE-DEFAULT and
see ADD-MATCH-FREE-OVERRIDE.  Here are some examples.

     (set-match-free-default :once)    ; future rules without a :match-free field
                                       ; are stored as :match-free :once (but this
                                       ; behavior is local to a book)
     (add-match-free-override :once t) ; existing rules are treated as
                                       ; :match-free :once regardless of their
                                       ; original :match-free fields
     (add-match-free-override :once (:rewrite foo) (:rewrite bar . 2))
                                       ; the two indicated rules are treated as
                                       ; :match-free :once regardless of their
                                       ; original :match-free fields

_Some history._ Before Version  2.7 the ACL2 rewriter performed Step (2)
above first.  More significantly, it always acted as though :once had
been specified.  That is, if Step (2) did not apply, then the rewriter
took the first binding it found using either Steps (1) or (3), in that
order, and proceeded to relieve the remaining hypotheses without trying
any other bindings of the free variables of that hypothesis.

FREE-VARIABLES-EXAMPLES    examples pertaining to free variables in rules

The examples in the two sub-topics of this topic illustrate the
handling of free variables in rules of class :rewrite (see
FREE-VARIABLES-EXAMPLES-REWRITE) and of class :forward-chaining (see
FREE-VARIABLES-EXAMPLES-FORWARD-CHAINING), respectively.  These
implicitly illustrate free-variables handling in rules of class :linear
as well.  Also see FREE-VARIABLES and see RULE-CLASSES.