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

NOTE-4-2    ACL2 Version  4.2 (January, 2011) 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.2 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 accumulated-persistence utility can now do finer-grained tracking,
providing data for individual hypotheses and the conclusion of a rule.
See ACCUMULATED-PERSISTENCE.  To try this out, evaluate the form
(accumulated-persistence :all); then see
ACCUMULATED-PERSISTENCE for a discussion of display options using
show-accumulated-persistence.  Thanks to Dave Greve for suggesting this
new capability and collaborating on its design and implementation.

The defattach utility now permits the use of :program mode functions,
though this requires the use of a trust tag (see DEFTTAG).  See
DEFATTACH and for discussion of the new capability, see
DEFPROXY, which explains how part of this change involves allowing
:program mode functions to be declared non-executable.

Redefinition (see LD-REDEFINITION-ACTION) is no longer
permitted for functions that have attachments (see DEFATTACH).
In such cases, the attachment must be removed first, e.g. with
(defattach foo nil).

Made small changes to mv-nth and defun-sk in order to permit guard
verification of functions introduced with more than one quantified
variable in a defun-sk form.  The change to mv-nth is to weaken the
guard by eliminating the requirement that the second argument satisfy
true-listp, and replacing the call of endp in the definition body by a
corresponding call of atom.  The new definition of mv-nth is thus
logically equivalent to the old definition, but with a weaker guard.
Thanks to Sol Swords for sending the following example, for which the
final verify-guards form had failed but now succeeds.

     (defstub foo (a b c) nil)
     (defun-sk forall-a-b-foo (c)
        (forall (a b) (foo a b c))
        :witness-dcls ((declare (Xargs :guard t
                                       :verify-guards nil))))
     (verify-guards forall-a-b-foo)

The implementations of prog2$, time$, with-prover-time-limit,
with-guard-checking, mbe (and must-be-equal), and ec-call have changed.
See the discussion below of the new utility, return-last.  A
consequence is that trace$ is explicitly disallowed for these and
related symbols, which formerly could cause hard Lisp errors, because
they are now macros.  Tracing of return-last is also disallowed.
Another consequence is that time$ now prints a more abbreviated message
by default, but a version of the old behavior can be obtained with
:mintime nil.

The following utilities no longer print an observation about raw-mode
transitions: set-raw-mode-on, set-raw-mode-on!, set-raw-mode, and
set-raw-mode-off.  Thanks to Jared Davis for suggestion this change in
the case of include-book (which proved awkward to restrict to that
case).

The system function translate-and-test now permits its LAMBDA form to
refer to the variable WORLD, which is bound to the current ACL2 logical
world.

Modified abort handling to avoid talking about an interrupt when the
error was caused by a Lisp error rather than an interrupt.

The value of the constant *acl2-exports*, which is still a list, has
been extended significantly, though only with the addition of symbols
that one might reasonably have expected all along to belong to this
list.  A new distributed book, books/misc/check-acl2-exports.lisp,
checks (at certification time) that no documented constant, macro, or
function symbol in the "ACL2" package has been accidentally omitted from
*acl2-exports*.  Thanks to Dave Greve for helpful discussions related to
this change.

Improved the built-in `untranslate' functions to produce let*
expressions when appropriate (more to help with tools that call
untranslate and the like, than to help with proof output).'

The utility redo-flat now works for certify-book failures, just as it
continues to work for failures of encapsulate and progn.

The following only affects users who use trust tags to add to list
values of either of the state global variables
program-fns-with-raw-code or logic-fns-with-raw-code.  For functions
that belong to either of the above two lists, trace$ will supply a
default value of :fncall to keyword :notinline, to avoid discarding
raw-Lisp code for the function.

The guard of the macro intern has been strengthened so that its second
argument may no longer be either the symbol *main-lisp-package-name* or
the string "COMMON-LISP".  That change supports another change, namely
that the following symbols in the "COMMON-LISP" package are no longer
allowed into ACL2: symbols in that package that are not members of the
list constant *common-lisp-symbols-from-main-lisp-package* yet are
imported into the "COMMON-LISP" package from another package.  See
PKG-IMPORTS and see SYMBOL-PACKAGE-NAME.  To see why we
made that change, consider for example the following theorem, which
ACL2 was able to prove when the host Lisp is GCL.

     (let ((x "ALLOCATE") (y 'car))
       (implies (and (stringp x)
                     (symbolp y)
                     (equal (symbol-package-name y)
                            "COMMON-LISP"))
                (equal (symbol-package-name (intern-in-package-of-symbol x y))
                       "SYSTEM")))

Now suppose that one includes a book with this theorem (with
:rule-classes nil), using an ACL2 built on top of a different host
Lisp, say CCL, that does not import the symbol SYSTEM::ALLOCATE into
the "COMMON-LISP" package.  Then then one can prove nil by giving this
theorem as a :use hint.

The axioms introduced by defpkg have changed.  See the discussion of
pkg-imports under "NEW FEATURES" below.

The error message for free variables (e.g., in definition bodies and
guards) now supplies additional information when there are governing IF
conditions.  Thanks to Jared Davis for requesting this enhancement and
collaborating in its design.

The command :redef- now turns off redefinition.

Improved proof output in the case of a :clause-processor hint that
proves the goal, so that the clause-processor function name is printed.

The proof-checker command `then' now stops at the first failure (if
any).

It is no longer permitted to submit definitions in :logic mode for
merely part of an existing mutual-recursion event.  Such an action left
the user in an odd state and seemed a potential soundness hole.

The function break$ is now in :logic mode.  Thanks to Jared Davis for
requesting this enhancement.

The macro verify-termination now provides clearer output in the case
that it is redundant.  More important perhaps, as a courtesy it now
causes an error when applied to a constrained function, since
presumably such an application was unintended (as the constrained
function could never have been in :program mode).  Note that if one
desires different behavior, one can create one's own version of
verify-termination (but with a different name).

Improved the guards for the following functions, often weakening them,
to reflect more precisely the requirements for calling eq:
alist-difference-eq, intersection-eq, intersection1-eq, intersectp-eq,
not-in-domain-eq, set-difference-assoc-eq, set-equalp-eq, and union-eq.
Thanks to Jared Davis for pointing out this issue for intersectp-eq.

(CCL only) Made a change that can reduce the size of a compiled file
produced by certify-book when the host Lisp is CCL, by discarding source
information (for example, discarding local events).

*NEW FEATURES*

See the discussion above about new statistics that can be gathered by
the accumulated-persistence utility.

A new hint, :instructions, allows use of the proof-checker at the level
of hints to the prover.  Thanks to Pete Manolios for requesting this
feature (in 2001!).  See INSTRUCTIONS.

(For system hackers) There are new versions of system functions
translate1 and translate, namely translate1-cmp and translate-cmp
respectively, that do not take or return state.  See the Essay on
Context-message Pairs for relevant information.  Thanks to David Rager
for collaborating on this enhancement.

A new utility, return-last, is now the unique ACL2 function that can
pass back a multiple value result from one of its arguments.  Thus, now
the following are macros whose calls ultimately expand to calls of
return-last: prog2$, time$, with-prover-time-limit,
with-guard-checking, mbe (and must-be-equal), and ec-call.  With an
active trust tag, an advanced user can now write code that has side
effects in raw Lisp; see RETURN-LAST.  Thanks to Jared Davis
for requesting this feature.

A new function, pkg-imports, specifies the list of symbols imported
into a given package.  The axioms for defpkg have been strengthened,
taking advantage of this function.  Now one can prove theorems using
ACL2 that we believe could not previously be proved using ACL2, for
example the following.

     (equal (symbol-package-name (intern-in-package-of-symbol str t))
            (symbol-package-name (intern-in-package-of-symbol str nil)))

Thanks to Sol Swords for a helpful report, which included the example
above.  See PKG-IMPORTS and see DEFPKG.

Added function no-duplicatesp-eq.

Added a new hint keyword, :backchain-limit-rw, to control the level of
backchaining for rewrite, meta, and linear rules.  This overrides, for
the current goal and (as with :in-theory hints) descendent goals, the
default backchain-limit (see SET-BACKCHAIN-LIMIT).  Thanks to
Jared Davis for requesting this feature.

Support is now provided for creating and certifying books that do not
depend on trust tags, in the case that the only use of trust tags is
during make-event expansion.  See SET-WRITE-ACL2X.  Thanks to
Sol Swords for reporting a couple of bugs in a preliminary
implementation.

Function (file-write-date$ filename state) has been added, giving the
write date of the given file.

See FORWARD-CHAINING-REPORTS for how to get new reports on the
forward chaining activity occurring in your proof attempts.  Thanks to
Dave Greve for inspiring the addition of this utility.

It is now possible to use ACL2's printing utilities to return strings,
by opening output channels to the keyword :STRING rather than to
filenames.  See IO.  Thanks to Jared Davis for a helpful
conversation that led us to add this feature.

*HEURISTIC IMPROVEMENTS*

We have slightly improved the handling of :forward-chaining rules that
contain free variables.  Formerly, such rules might fire only once,
when the first match for a free variable is discovered, and would not
fire again even if subsequent forward chaining made available another
match.  This made it difficult to predict whether a rule with free
variables would fire or not, depending as it did on the order in which
newly derived conclusions were added.  The new handling is a little
slower but more predictable.  Thanks to Dave Greve for sending a helpful
example that led us to consider making such an improvement.

We have slightly improved the so-called "type-set" heuristics to work a
bit harder on terms of the form (rec term), where rec is a so-called
"compound-recognizer" function, that is, a function with a
corresponding enabled :compound-recognizer rule.  Thanks to Jared Davis
for sending a helpful example (found, in essence, in the modified
function type-set-rec, source file type-set-b.lisp).

We made three heuristic improvements in the way contexts (so-called
"type-alists") are computed from goals ("clauses").  Although these
changes did not noticeably affect timing results for the ACL2 regression
suite, they can be very helpful for goals with many hypotheses.  Thanks
to Dave Greve for sending a useful example (one where we found a goal
with 233 hypotheses!).

The algorithm for substituting alists into terms was modified.  This
change is unlikely to affect many users, but in one example it resulted
in a speed-up of about 21%.  Thanks to Dave Greve for supplying that
example.

Sped up include-book a bit by memoizing checksums of symbols.  (This
change pertains to "normal" ACL2 only, not the hons version (see
HONS-AND-MEMOIZATION, where such memoization already occurred.)  We
found about a 23% speed-up on an example from Dave Greve.

Made a small change to the algorithm used to prove hypotheses of
:type-prescription rules (ACL2 source function type-set-relieve-hyps).
One change avoids a linear walk through the context (the "type-alist"
structure), while the other could avoid storing unnecessary forced
assumptions (into the so-called "tag-tree").

*BUG FIXES*

Fixed a long-standing soundness bug caused by the interaction of forced
hypotheses with destructor elimination.  The fix was to avoid using
forcing when building the context (so-called "type-alist") when the
goal is considered for destructor elimination; those who are interested
can see a discussion in source function eliminate-destructors-clause1,
which includes a proof of nil that no longer succeeds.  A similar fix
was made for generalization, though we have not exploited the previous
code to prove nil in that case.

Fixed a bug that allowed book certification to ignore skip-proofs around
encapsulate events.  Thus, a book could contain an event of the form
(skip-proofs (encapsulate ...)), and a call of certify-book on that
book could succeed even without supplying keyword :skip-proofs-okp t.
This bug was introduced in Version  3.5 (May, 2009).

Fixed a bug that could occur when including a book that attempts to
redefine a function as a macro, or vice-versa.  (For details of the
issue, see the comment in the definition of variable
*hcomp-fn-macro-restore-ht* in source file other-events.lisp.)

(Windows only) Fixed handling of the Windows drive so that an executable
image saved on one machine can be used on another, even with a different
drive.  Thanks to Harsh Raju Chamarthi for reporting this issue and
doing a lot of testing and collaboration to help us get this right.

Made a change to avoid possible low-level errors, such as bus errors,
when quitting ACL2 by calling good-bye or its synonyms.  This was
occurring in CCL, and we are grateful to Gary Byers for helping us find
the source of those errors (which basically was that ACL2 was
attempting to quit while already in the process of quitting).

Fixed a bug in with-guard-checking, which was being ignored in function
bodies.

Fixed a bug in top-level, which was not reverting the logical world
when an error resulted from evaluation of the given form.  Thanks to
Jared Davis for bringing this bug to our attention.

Fixed a long-standing bug (back through Version  2.7) that was
discarding changes to the connected book directory (see CBD)
when exiting and then re-entering the top-level ACL2 loop (with lp).

In some host Lisps, it has been possible to be in a situation where it
is impossible to interrupt checkpoint printing during the summary.  We
had thought this solved when the host Lisp was CCL, but Sol Swords sent
us an example (for which we are grateful) illustrating that this
behavior could occur.  This has been fixed.

Fixed a bug in a proof obligation generated for :meta and
:clause-processor rules, that the guard on the metafunction or
clause-processor function, fn, holds under suitable assumptions.  Those
assumptions include not only that the first argument of fn satisfies
pseudo-termp, but also that all stobj inputs satisfy the corresponding
stobj recognizer predicates.  We had erroneously considered stobj
outputs of fn instead of stobj inputs.  Thanks to Sol Swords for
bringing this bug to our attention with a simple example, and correctly
pointing us to the bug in our code.

Fixed the following bugs in defattach.  We hadn't always been applying
the full functional substitution when generating guard proof
obligations.  We had been able to hit an assertion when reattaching to
more than one function.  Attachment was permitted in the case of an
untouchable function (see REMOVE-UNTOUCHABLE).  Finally, the
guard proof obligation could fail in the case that the two functions
have different formal parameter lists, as in the following example.

     (encapsulate
      ((foo (x) x :guard (symbolp x)))
      (local (defun foo (x) x)))
     (defun bar (x2)
       (declare (xargs :guard (symbolp x2)))
       x2)
     (defattach foo bar)

Fixed a raw Lisp error that could be caused by including a book using
make-event to define a function symbol in a locally-introduced package.
An example appears in a comment in ACL2 source function
write-expansion-file.

Made a change that can prevent an error near the end of book
certification when the underlying Host Lisp is Allegro Common Lisp, in
the case that environment variable ACL2_SYSTEM_BOOKS has been set to
the name of a directory with a parent that is a soft link.  Thanks to
Dave Greve for supplying an example to led us to this fix, which
involves avoiding Allegro CL's implementation of the Common Lisp
function, truename.

Fixed a bug that was failing to substitute fully using bindings of free
variables in forced hypotheses.  A related change is that instead of
binding such a free variable to a new variable of the form ???-Y, the
new variable is now of the form UNBOUND-FREE-Y.

Fixed a bug that could inhibit the printing of certain theory warnings
(and probably, in the other direction, cause inappropriate such
printing).

We eliminated excessive "Raw-mode" warnings about add-include-book-dir
that could be generated by the use of raw-mode during include-book.
Thanks to Dave Greve for bringing this issue to our attention.

Fixed the printing of results from forms within an encapsulate, so that
they are abbreviated according to the ld-evisc-tuple.

It is now possible to evaluate stobj-related forms after evaluating
:set-guard-checking :none or :set-guard-checking nil, even in cases
where such evaluation formerly caused a guard violation due to a bug in
ACL2.  Here is an example of an error that no longer occurs.

     ACL2 !>(defstobj st fld)

     Summary
     Form:  ( DEFSTOBJ ST ...)
     Rules: NIL
     Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
      ST
     ACL2 !>(set-guard-checking :none)

     Turning off guard checking entirely.  To allow execution in raw Lisp
     for functions with guards other than T, while continuing to mask guard
     violations, :SET-GUARD-CHECKING NIL.  See :DOC set-guard-checking.

     ACL2 >(fld st)

     ACL2 Error in TOP-LEVEL:  The guard for the function call (FLD ST),
     which is (STP ST), is violated by the arguments in the call (FLD ST).
     [... etc. ...]

You can understand how things now work by imagining that when a function
introduced by defstobj is called, guard-checking values of :none or nil
are temporarily converted to t.  Thanks to Pete Manolios, Ian Johnson,
and Harsh Raju Chamarthi for requesting this improvement.

Fixed a bug in which the wrong attachment could be made when the same
function has an attachment in a book and another in the certification
world of that book (possibly even built into ACL2), if the load of a
compiled file is aborted because a sub-book's compiled file is missing.
The bug has been present since the time that defattach was added
(Version_4.0).  An example may be found in a comment in the deflabel
for note-4-2 (ACL2 source file ld.lisp).

The :doc and related utilities now cause a clean error when provided
other than a symbol.  Thanks to Jared Davis for pointing out the raw
Lisp error that had occurred in such cases.

It had been the case that in raw-mode (see SET-RAW-MODE), it
was possible to confuse include-book when including a book in a
directory different from the current directory.  This has been fixed.
Thanks to Hanbing Liu for bringing this problem to our attention with a
small example.

*NEW AND UPDATED BOOKS AND RELATED INFRASTRUCTURE*

Many changes have been made to the distributed books, thanks to an
active ACL2 community.  You can contribute books and obtain updates
between ACL2 releases by visiting the acl2-books project web page,
`http://acl2-books.googlecode.com/'.

There is new Makefile support for certifying just some of the
distributed books.  See BOOK-MAKEFILES, in particular
discussion of the variable ACL2_BOOK_DIRS.  Thanks to Sandip Ray for
requesting this enhancement.

The documentation for make-event now points to a new book,
books/make-event/defrule.lisp, that shows how make-event can be used to
do macroexpansion before generating events.  Thanks to Carl Eastlund for
useful interaction on the acl2-help mailing list that led us to add this
example.

*EMACS SUPPORT*

Incorporated a version of changes from Jared Davis to the control-t f
emacs utility (distributed file emacs/emacs-acl2.el), so that one can
fill a format string from anywhere within the string.

*EXPERIMENTAL VERSIONS*

We refrain from listing changes here to experimental versions, other
than an enhancement to the HONS version that can reduce sizes of
certificate files, by applying hons-copy to introduce structure sharing
(ACL2 source function make-certificate-file1).

NOTE-4-2(R)    ACL2 Version  4.2(r) (January, 2011) Notes

Please see NOTE-4-2 for changes in Version  4.2 of ACL2.

NOTE-4-3    ACL2 Version  4.3 (July, 2011) 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.2 into the
following categories of changes: existing features, new features,
heuristic improvements, bug fixes, changes at the system level and to
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*

Significant changes have been made for list-processing primitives such
as member and assoc; see EQUALITY-VARIANTS.  In summary:
instead of separate functions based on eq, eql, and equal, there is
essentially just one function, which is based on equal; the eq and eql
variants are logically just the equal variant.  For example, member-eq
and member are macros that generate corresponding calls of member-equal
in the logic, although in raw Lisp they will execute using tests eq and
eql, respectively.  References to any of these in logical contexts such
as theories are now references to the function based on equal; for
example, the hint :in-theory (disable member) is completely equivalent
to the hint :in-theory (disable member-equal).  Distributed books have
been modified as necessary to accommodate this change.  While the need
for such changes was relatively infrequent, changes were for example
needed in contexts where terms are manipulated directly; for example,
defevaluator needs to mention member-equal rather than member, just as
it was already the case to mention, say, binary-append rather than
append.  Again, see EQUALITY-VARIANTS for more information
about equality variants.

A few improvements were made in support of the modified treatment of
equality variants discussed above.  The changes include the following.

     o We now allow the use of macro aliases (see
     MACRO-ALIASES-TABLE in :trigger-fns of rules (see
     RULE-CLASSES).

     o We now remove so-called "guard holders" (including calls of
     return-last, hence of mbe) in :trigger-terms of rules.

     o We also remove guard holders in formulas of :congruence and
     type-prescription rules.

     o Macros union-eq and intersection-eq can now take any positive
     number of arguments, and union-eq can take zero arguments.
     (Thanks to Jared Davis for requesting this enhancement.)  The same
     can be said for new macros union$ and intersection$, respectively.

     o A few changes were made to built-in theorems from source file
     axioms.lisp, in particular disabling :type-prescription rule
     consp-assoc-equal (formerly two enabled rules, consp-assoc-eq and
     consp-assoc) but adding this theorem as a :forward-chaining rule,
     and similarly for
     true-list-listp-forward-to-true-listp-assoc-equal (and eliminating
     rule true-list-listp-forward-to-true-listp-assoc-eq; and disabling
     rule true-listp-cadr-assoc-eq-for-open-channels-p.  Also, theorem
     all-boundp-preserves-assoc has been renamed to
     all-boundp-preserves-assoc-equal and also strengthened.

     o Some guards were slightly improved (logically weaker or the
     same).

Improved get-output-stream-string$ to allow for a context and to do
genuine error printing instead of using cw.  See IO.

Added the symbols flet and with-local-stobj to *acl2-exports*.

A small change was made to the processing of more than one :guard
declaration for the same function.  In particular, a guard of t is
essentially ignored.

Attachments are now allowed during evaluation of the first argument of
prog2$ even in contexts (such as proofs) during which the use of
attachments is normally prohibited.  More generally, the second of the
three arguments of return-last has this property, except in the case of
mbe (or related macros like mbe1), where the exec argument may provide
the value.  Thanks to Sol Swords for useful discussions leading us to
implement this enhancement.

The restriction has been removed that prohibited the use of mbe inside
encapsulate events with a non-empty signature.  This restriction was
introduced in Version  3.4, but has not been necessary since Version
4.0, when we first started disallowing guard verification for functions
introduced non-locally inside such encapsulate events.

We weakened the checks involving common ancestors for evaluator and
meta (and clause-processor) functions (see
EVALUATOR-RESTRICTIONS) so that except in the mbe case, the
next-to-last argument of return-last is not considered.  Thanks to Sol
Swords for bringing this issue to our attention.

The macro append no longer requires at least two arguments.  Thanks to
Dave Greve for requesting this enhancement.

(Mostly for system hackers) Now, break-on-error breaks at a more
appropriate (earlier) time for certain system functions that do not
return state, such as translate11.  Thanks to David Rager for
requesting this improvement.

Show-accumulated-persistence may take a new argument, :runes, which
simply causes an alphabetical list of runes to be printed out.

Improved trace$ so that :entry, :exit, and :cond forms may reference
state even if the function being traced does not include state as a
formal.

The system function acl2x-expansion-alist now takes a second argument,
namely state.  This change allows for more flexibility in the sorts of
attachments that can be made to this function (see DEFATTACH).
Thanks to Jared Davis and Sol Swords for requesting this enhancement
and providing a preliminary implementation.

An obscure proof-checker change, unlikely to affect users, replaces the
state global variables erp, val, print-macroexpansion-flg, and
print-prompt-and-instr-flg by pc-erp, pc-val,
pc-print-macroexpansion-flg, and pc-print-prompt-and-instr-flg,
respectively.

State globals fmt-hard-right-margin and fmt-soft-right-margin are now
untouchable (see SET-FMT-HARD-RIGHT-MARGIN and see
PUSH-UNTOUCHABLE).  If you bind these state globals with
state-global-let*, then you will need to do so with appropriate setteres
to restore their values, for example as follows.

       (state-global-let*
        ((fmt-hard-right-margin 500 set-fmt-hard-right-margin)
         (fmt-soft-right-margin 480 set-fmt-soft-right-margin))
        ...)

The error message has been improved for the case of evaluating an
undefined function that has an attachment (see DEFATTACH).
Thanks to Jared Davis for sending the following example, which
illustrates the additional part of the message.

       ACL2 !>(defstub foo (x) t)
       [[... output omitted ...]]
       ACL2 !>(defattach foo identity)
       [[... output omitted ...]]
       ACL2 !>(defconst *x* (foo 3))

       ACL2 Error in ( DEFCONST *X* ...):  ACL2 cannot ev the call of undefined
       function FOO on argument list:

       (3)

       Note that because of logical considerations, attachments (including
       IDENTITY) must not be called in this context.

       [[... additional output omitted ...]]

The directory string supplied to add-include-book-dir no longer must
terminate with the `/' character, as had been required in some Lisp
implementations.  Thanks to Sol Swords for bringing this issue to our
attention.

We no longer print induction schemes with gag-mode; use :pso if you
want to see them.  Thanks to Dave Greve for this suggestion.

It is now legal to supply a constant for a stobj array dimension.  See
DEFSTOBJ.  Thanks to Warren Hunt for requesting this
enhancement.

We cleaned up a few issues with defpkg.

     o It is no longer illegal to submit a defpkg form in raw-mode (see
     SET-RAW-MODE).  Thanks to Jun Sawada for reporting an
     example in which an include-book form submitted in raw-mode caused
     an error because of a `hidden' defpkg form (see
     HIDDEN-DEFPKG).  There will no longer be an error in such cases.

     o It had been the case that locally including a book could make it
     possible to use a package defined by that book.  Consider for
     example the following book, foo.lisp.

          (in-package "ACL2")
          (local (include-book "arithmetic/top" :dir :system))

     After certifying this book, it had been possible to admit the
     following events in a new session.

          (include-book "foo")
          (defconst acl2-asg::*foo* 3)
          (defconst *c* 'acl2-asg::xyz)

     In Version_4.3, neither of these defconst events is admitted.

     o A hard Lisp error is now avoided that had been possible in rare
     cases when including books with hidden packages (see
     HIDDEN-DEFPKG). An example may be found in a comment in the
     deflabel for note-4-3 (in ACL2 source file ld.lisp).

The undocumented (but sometimes useful) functions packn1 and packn are
now guard-verified :logic mode functions.  Thanks to Sandip Ray for
requesting this enhancement.

It had been the case that when including a book, functions defined in
the book's certification world (that is, in its portcullis commands)
were typically not given compiled code.  That has been fixed.

The commands :pl and :pl2 have been improved, primarily by printing
information for more rule classes.  See PL and see PL2.
See also the item below about the new proof-checker command,
show-type-prescriptions.

*NEW FEATURES*

New macros mv?-let and mv? extend the funtionality of mv-let and mv
(respectively) to the case of a single value.

Macro with-local-state is available for system programmers who wish bind
state locally, essentially using with-local-stobj.  But this should
only be done with extreme care, and it requires an active trust tag;
see WITH-LOCAL-STATE.

Formatted printing functions now have analogues that print to strings
and do not take an output channel or state as arguments.  See
PRINTING-TO-STRINGS.

The system function ancestors-check is now available for verified
modification by users, i.e., attachment using (defattach
ancestors-check <your_function>).  Thanks to Robert Krug for providing
the necessary proof support, which we modified only in small ways.

New macros, observation-cw and warning$-cw, provide formatted printing
of observations and warnings (respectively) without state.  Thanks to
Harsh Raju Chamarthi and David Rager for requests leading to these
utilities.  Observation-cw is now used in some of the distributed books
(thanks to Robert Krug for useful interaction for that).

The proof-checker command type-alist (see
PROOF-CHECKER-COMMANDS) now takes an optional third argument that
causes the production of forward-chaining reports (see
FORWARD-CHAINING-REPORTS).  Thanks to Dave Greve for requesting such
an enhancement.

The reports generated by forward-chaining, forward-chaining-reports,
have been changed to indicate when a conclusion reached by forward
chaining is REDUNDANT with respect to the type information already
known.  Thanks to Dave Greve for suggesting this enhancement.

The utility with-prover-time-limit is now legal for events (see
EMBEDDED-EVENT-FORM).  For example, the following is now legal.

     (encapsulate
      ()
      (with-prover-time-limit
       2
       (defthm append-assoc
         (equal (append (append x y) z)
                (append x (append y z))))))

The new utility with-prover-step-limit is analogous to the utility
with-prover-time-limit, but counts "prover steps" rather than checking
for time elapsed.  See WITH-PROVER-STEP-LIMIT.  Also see
SET-PROVER-STEP-LIMIT to provide a default step-limit.  Note that just
as with-prover-time-limit may now be used to create events, as
discussed just above, with-prover-step-limit may also be used to create
events.  Thanks to Carl Eastlund for requesting support for step-limits.

The macro progn$ is analogous to prog2$, but allows an arbitrary number
of arguments.  For example:

     ACL2 !>:trans1 (progn$ (f1 x) (f2 x) (f3 x))
      (PROG2$ (F1 X) (PROG2$ (F2 X) (F3 X)))
     ACL2 !>

Thanks to David Rager for contributing this macro.

The macro defattach may now be supplied the argument :skip-checks
:cycles.  In this case, as with argument :skip-checks t, a trust tag is
reuired (see DEFTTAG), and no logical claims are made.  The
effect is to avoid the usual check that the extended ancestor relation
has no cycles (see DEFATTACH).  Thanks to Dave Greve for
requesting this feature.

You can now limit the printing of subgoal names when using
:set-gag-mode :goals.  See SET-PRINT-CLAUSE-IDS.  Thanks to
Karl Hoech for a suggestion leading to this enhancement.

A new proof-checker command, show-type-prescriptions, or st for short,
provides information about :type-prescription rules that match a given
term.  Thanks to Dave Greve for requesting this enhancement.  See also
the item above about related improvements to commands :pl and :pl2.

*HEURISTIC IMPROVEMENTS*

ACL2 now avoids some repeated attempts to rewrite hypotheses of rewrite
rules.  See SET-RW-CACHE-STATE for a discussion of this
behavior and how to avoid it.  The default behavior has been observed
to reduce by 11% the overall time required to complete a regression.
Here are the directories that had the top three time decreases and top
three time increases, shown in seconds.

       -368 coi/gacc (1064 down to 696: decrease of 35%)
       -220 workshops/1999/ste (664 down to 444: decrease of 33%)
       -148 unicode (331 down to 183: decrease of 45%)
       ....
         +7 workshops/2002/cowles-flat/support (229 up to 236: increase of 3%)
         +8 workshops/1999/ivy/ivy-v2/ivy-sources (508 up to 516: increase of 2%)
        +12 workshops/2009/hardin/deque-stobj (78 up to 91: increase of 17%)

The so-called "ancestors check," which is used to limit backchaining,
has been strengthened so that two calls of equal are considered the same
even if their arguments appear in the opposite order.  Thanks to Robert
Krug for providing an implementation and a useful discussion.

The check for irrelevant-formals in processing of defuns has been made
more efficient.  Thanks to Eric Smith for reporting this issue in 2001
(!) and thanks to Warren Hunt for recently sending an example.  For that
example, we have seen the time for the irrelevant-formals check reduced
from about 10 seconds to about 0.04 seconds.

(GCL only) The macro mv has been modified so that certain fixnum boxing
can be avoided.

(Allegro CL only) We have set to nil four Allegro CL variables that
otherwise enable storing of certain source information (for details,
see the discussion of "cross-referencing" in ACL2 source file
acl2-init.lisp).  As a result of this change we have about a 6% speedup
on the regression suite, but a 27% time reduction on an example that
includes a lot of books.

Exhaustive matching for the case of free-variables has been extended to
type-prescription rules, in analogy to the default setting :match-free
:all already in place for rewrite, linear, and forward-chaining rules.
See FREE-VARIABLES-TYPE-PRESCRIPTION.  Thanks to Dave Greve for
requesting this enhancement.

*BUG FIXES*

A soundness bug was fixed in some raw-Lisp code implementing the
function, take.  Thanks to Sol Swords for pointing out this bug with
(essentially) the following proof of nil.

     (defthmd take-1-nil-logic
       (equal (take 1 nil) '(nil))
       :hints(("Goal" :in-theory (disable (take)))))
     (thm nil :hints (("Goal" :use take-1-nil-logic)))

Calls of mbe in "safe-mode" situations -- i.e., during evaluation of
defconst, value-triple, and defpkg forms, and during macroexpansion --
are now guard-checked.  Thus, in these situations both the :logic and
:exec forms will be evaluated, with an error if the results are not
equal.  Formerly, only the :logic form was evaluated, which was a
soundness bug that could be exploited to prove nil.  For a such a proof
and a bit of further explanation, see the example at the top of the
comments for (deflabel note-4-3 ..) in ACL2 source file ld.lisp.

It had been possible to prove nil by proving the following theorem
using ACL2 built on CCL and then proving its negation using ACL2 built
on a different host Lisp.

     (defthm host-lisp-is-ccl
       (equal (cdr (assoc 'host-lisp *initial-global-table*))
              :ccl)
       :rule-classes nil)

This hole has been plugged by moving the setting of 'host-lisp out of
the constant *initial-global-table*.

Fixed trace$ for arguments that are stobj accessors or updaters.  It
also gives an informative error in this case when the accessor or
updater is a macro (because the introducing defstobj event specified
:inline t).

Avoided a potential error that could occur when no user home directory
is located.  Our previous solution for Windows simply avoided looking
for ACL2 customization files (see ACL2-CUSTOMIZATION) and
acl2-init.lsp files in a user's home directory.  With this change, we
handle such files the same for Windows as for non-Windows systems: we
always look for ACL2 customization files (see
ACL2-CUSTOMIZATION) and acl2-init.lsp files in a user's home
directory, but only if such a directory exists.  Thanks to Hanbing Liu
for reporting this issue.

(GCL only) Fixed a bug that prevented the use of
get-output-stream-string$ when the host Lisp is GCL.

Fixed with-live-state to work properly for executable counterparts
(so-called "*1*" functions).

Fixed a bug in the error message caused by violating the guard of a
macro call.

Fixed a bug in an error message that one could get when calling
defattach with argument :skip-checks t to attach to a :program mode
function symbol that was introduced with defun.  (This is indeed an
error, but the message was confusing.)  Thanks to Robert Krug for
bringing this bug to our attention.

Fixed a bug in the loop-checking done on behalf of defattach, which
could miss a loop.  For an example, see the comment about loop-checking
in the comments for (deflabel note-4-3 ..) in ACL2 source file ld.lisp.

Terms of the form (hide <term>) without free variables could be
simplified, contrary to the purpose of hide.  This is no longer the
case,  Thanks to Dave Greve for reporting this issue.

An infinite loop could occur when an error was encountered in a call of
wormhole-eval, for example with the following form, and this has been
fixed.

     (wormhole-eval 'demo
                    '(lambda ()
                       (er hard 'my-top "Got an error!"))
                    nil)

Fixed a bug in detection of package redefinition.  While we have no
example demonstrating this as a soundness bug, we cannot rule it out.

Fixed a bug in the message produced by an erroneous call of flet.
Thanks to Jared Davis for reporting this bug and sending a helpful
example.

For a failed defaxiom or defthm event, we now avoid printing runes that
are used only in processing proposed rules to be stored, but not in the
proof itself.  Thanks to Dave Greve for sending us an example that led
us to make this fix.

ACL2 did not reliably enforce the restriction against non-local
include-book events inside encapsulate events, as illustrated by the
following examples.

     ; not permitted (as expected)
     (encapsulate () (include-book "foo"))

     ; permitted (as expected)
     (encapsulate () (local (include-book "foo")))

     ; formerly permitted (surprisingly); now, not permitted
     (local (encapsulate () (include-book "foo")))

Moreover, the corresponding error message has been fixed.  Thanks to
Jared Davis and Sandip Ray for relevant discussions.

When include-book is given a first argument that is not a string, a
more graceful error now occurs, where previously an ugly raw Lisp error
had occurred.  Thanks to Eric Smith for bringing this bug to our
attention.

Fixed a bug in an error message that was printed when an unexpected
expression has occurred where a declare form is expected.

(Since all functions are compiled when the host Lisp is CCL or SBCL, the
following bug fix did not occur for those host Lisps.)  After
evaluation of (set-compile-fns t), all defined functions are expected
to run with compiled code; but this was not the case for functions
exported from an encapsulate event.  This has been fixed.

It had been the case that the :puff command was broken for include-book
form whose book had been certified in a world with an
add-include-book-dir event.  This has been fixed.

Evaluation of stobj updaters (see DEFSTOBJ) may no longer use
attachments (see DEFATTACH).  This is a subtle point that will
likely not affect many users.  Thanks to Jared Davis for bringing this
issue to our attention; a slight variant of his example appears in a
comment in ACL2 source function oneify-cltl-code.

It had been the case that even when a stobj creator function was
declared to be untouchable (see PUSH-UNTOUCHABLE), a
with-local-stobj form based on that same stobj was permitted.  Now,
such forms are not admitted.  Thanks to Jared Davis for a query leading
to this fix.

Fixed a buggy message upon guard violations, which was suggesting the
use of (set-guard-checking :none) in some cases when guard-checking was
already set to :none.

It had been possible to get a hard Lisp error when computing with
ec-call in books.  The following is an example of such a book, whose
certification no longer causes an error.

     (in-package "ACL2")
     (defun f (x) x)
     (defconst *c* (ec-call (f 3)))
     (defun g (x) (cons x x))

The command :pl2, and also the proof-checker commands rewrite and
show-rewrites (and hence their respective aliases r and sr), now take
rule-id arguments that can be :definition runes.  These commands dealt
with definition rules already, e.g.

     :pl2 (append x y) binary-append

but they did not allow explicit specification of :definition runes,
e.g.:

     :pl2 (append x y) (:definition binary-append)

The following example illustrates a bug in the processing of (admittedly
obscure) hints of the form :do-not-induct name, where name is not t,
:otf-flg-override, :otf, or nil.  In this example, ACL2 had essentially
ignored the hint and reverted to prove the original goal by induction,
rather than to skip the goal temporarily as is expected for such hints.
Thanks to David Rager for a helpful discussion.

     (thm (and (equal (append (append x y) z) (append x y z))
               (equal (append (append x2 y2) z2) (append x2 y2 z2)))
          :hints (("Subgoal 1" :do-not-induct some-name)))

Fixed a slight bug in the definitions of built-in theories.  For
example, in a fresh ACL2 session the value of the following form is nil,
but formerly included several :definition runes.

     (let ((world (w state)))
       (set-difference-theories (function-theory :here)
                                (function-theory 'ground-zero)))

*CHANGES AT THE SYSTEM LEVEL AND TO DISTRIBUTED BOOKS*

Many changes have been made to the distributed books, as recorded in
svn logs under the `Source' and 'Updates' links at
`http://acl2-books.googlecode.com/'.  Here we list some of the more
significant changes.

     o A large library has been graciously contributed by the formal
     verification group at Centaur Technology.  See books/centaur/ and,
     in particular, file books/centaur/README, which explains how the
     library depends on the experimental HONS extension (see
     HONS-AND-MEMOIZATION).

     o Among the new books is an illustration of defattach,
     books/misc/defattach-example.lisp, as well as a variant of
     defattach that avoids the need for guard verification,
     books/misc/defattach-bang.lisp.

     o Distributed book books/misc/trace1.lisp has been deleted.  It had
     provided slightly more friendly trace output for new users, but
     distributed book books/misc/trace-star.lisp may be better suited
     for that purpose.

ACL2 can once again be built on LispWorks (i.e., as the host Lisp), at
least with LispWorks 6.0.  Thanks to David Rager for useful
conversations.  Several changes have been made from previous
LispWorks-based ACL2 executables:
o ACL2 now starts up in its read-eval-print loop.
o You can save an image with save-exec.
o Multiprocessing is not enabled.
o The stack size is managed using a LispWorks variable that causes the
stack to grow as needed.
o When ACL2 is built a script file is written, as is done for other host
Lisps.  Thus, (assuming that no PREFIX is specified), saved_acl2 is
just a small text file that invokes a binary executable, which for
Lispworks is saved_acl2.lw.

The HTML documentation no longer has extra newlines in <pre>
environments.

Statistics on ACL2 code size may be found in distributed file
doc/acl2-code-size.txt.  This file and other information can be found in
a new documentation topic, about-acl2.

Fixed the build process to pay attention to environment variable
ACL2_SYSTEM_BOOKS (which may be supplied as a command-line argument to
`make').  An ACL2 executable can thus now be built even when there is no
books/ subdirectory if a suitable replacement directory is supplied.

Some warnings from the host Lisp are now suppressed that could formerly
appear.  For example, the warnings shown below occurs in Version  4.2
using Allegro CL, but not in Version  4.3.

     ACL2 !>(progn (set-ignore-ok t)
                   (set-irrelevant-formals-ok t)
                   (defun bar (x y)
                     x))
     [[.. output omitted ..]]
      BAR
     ACL2 !>:comp bar
     ; While compiling BAR:
     Warning: Variable Y is never used.
     ; While compiling (LABELS ACL2_*1*_ACL2::BAR ACL2_*1*_ACL2::BAR):
     Warning: Variable Y is never used.
      BAR
     ACL2 !>

*EMACS SUPPORT*

The distributed Emacs file emacs/emacs-acl2.el now indents calls of
er@par and warning$@par the same way that calls of defun are indented.

*EXPERIMENTAL VERSIONS*

The parallel version (see PARALLELISM) now supports parallel
evaluation of the "waterfall" part of the ACL2 prover; see
SET-WATERFALL-PARALLELISM.  Thanks to David Rager for doing the
primary design and implementation work.

A new macro, spec-mv-let, supports speculative and parallel execution
in the parallel version, courtesy of David Rager.

Among the enchancements for the HONS version (see
HONS-AND-MEMOIZATION) are the following.

     Memoized functions may now be traced (see TRACE$).  Thanks
     to Sol Swords for requesting this enhancement.

     Memoize-summary and clear-memoize-statistics are now :logic mode
     functions that return nil.  Thanks to Sol Swords for this
     enhancement.

     Memoize is now explicitly illegal for constrained functions.
     (Already such memoization was ineffective.)

     A new keyword argument, :AOKP, controls whether or not to allow
     memoization to take advantage of attachments; see MEMOIZE
     and for relevant background, see DEFATTACH.

     Memoize is now illegal by default for :logic mode functions that
     have not had their guards verified.  See MEMOIZE (keyword
     :ideal-okp) and see ACL2-DEFAULTS-TABLE (key
     :memoize-ideal-okp) for and explanation of this restriction and
     how to avoid it.

     History commands such as :pe and :pbt now display "M" or "m" to
     indicate memoized functions.  See PC.

NOTE-4-3(R)    ACL2 Version  4.3(r) (July, 2011) Notes

Please see NOTE-4-3 for changes in Version  4.3 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
     (except that a macro alias can stand in for a function symbol; see
     ADD-MACRO-ALIAS).  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.  (This field is not implemented for other rule
     classes, including the :type-prescription rule class.)  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
     different ways to reign in the rewriter, see
     REWRITE-STACK-LIMIT and see SET-PROVER-STEP-LIMIT.
     Jared Davis has pointed out that you can set the
     :backchain-limit-lst 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.

The structure of this documentation is as follows.  First we give a
brief overview of forward chaining and contrast it to backchaining
(rewriting).  Then we lay out the syntactic restrictions on
:forward-chaining rules.  Then we give more details about the process
and point to a tool to assist you in debugging your :forward-chaining
rules.

_Overview and When to Use Forward Chaining_

Forward chaining is performed as part of the simplification process:
before the goal is rewritten a _context_ is established.  The context
tells the theorem prover what may be assumed during the rewriting,
e.g., to establish hypotheses of rewrite rules.  For example, if the
goal is (implies (and (p A) (q A)) (r A)), then when (r A) is being
rewritten, the context tells us we may assume (p A) and (q A).  Forward
chaining is used to extend the context before rewriting begins.  For
example, the :forward-chaining rule (implies (p x) (p1 x)) would add
(p1 A) to the context.

Forward chaining and backchaining are duals.  If a rewrite rule
requires that (p1 A) be established and (p A) is known, it could be
done either by making (implies (p x) (p1 x)) a :forward-chaining rule
or a :rewrite rule.  Which should you choose?

As a rule of thumb, if a conclusion like (p1 A) is expected to be
widely needed, it is better to derive it via forward chaining because
then it is available "for free" during the rewriting after paying the
one-time cost of forward chaining.  Alternatively, if (p1 A) is a rather
special hypothesis of key importance to only a few rewrite rules, it is
best to derive it only when needed.  Thus forward chaining is pro-active
and backward chaining (rewriting) is reactive.

_Syntactic Restrictions_

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,"
mv-list or return-last (the latter resulting from macroexpansion of
calls of prog2$, must-be-equal or mbe), ec-call, and a few others), or
`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.

_More Details about Forward Chaining_

: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, and certain heuristics approve of the newly
derived conclusion, we add the instantiated conclusion to our known
assumptions.  Since this might introduce new terms into the assumptions,
forward chaining is repeated.  Heuristic approval of each new addition
is necessary to avoid infinite looping as would happen with the rule
(implies (p x) (p (f x))), which might otherwise forward chain from (p
A) to (p (f A)) to (p (f (f A))), etc.

_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.  (For insiders: forward
chaining extends the type-alist.)  The context starts out with "obvious"
consequences of the negation of the goal.  For example, if the goal is

     (implies (and (p A) (q (f A)))
              (c A))

then the context notes that (p A) and (q (f A)) are non-nil and (c A)
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 A)) to non-nil, provided the heuristics approve of this
extension.  Note however that since (r (f A)) is put into the context,
not the goal, you will not see it in the goal formula.  Furthermore, the
assumption added to the context is just the instantiation of the
conclusion of the rule, with no simplification or rewriting applied.
Thus, for example, if it contains an enabled non-recursive function
symbol it is unlikely ever to match a (rewritten) term arising during
subsequent simplification of the goal.

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.

Debugging :forward-chaining rules can be difficult since their effects
are not directly visible on the goal being simplified.  Tools are
available to help you discover what forward chaining has occurred see
FORWARD-CHAINING-REPORTS.

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 may issue 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, and type-prescription rules.

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, as well as an
example exploring "binding hypotheses" as described below.

Note that the :match-free mechanism discussed below does not apply to
type-prescription rules.  See FREE-VARIABLES-TYPE-PRESCRIPTION
for a discussion of how to control free-variable matchng for
type-prescription rules.

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.  We call this a "binding hypothesis."  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'._

As noted above, the following discussion applies only to rewrite,
linear, and forward-chaining rules.  See
FREE-VARIABLES-TYPE-PRESCRIPTION for a discussion of analogous
considerations for type-prescription rules.

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.

FREE-VARIABLES-EXAMPLES-FORWARD-CHAINING    examples pertaining to free variables in forward-chaining rules

The following examples illustrate ACL2's handling of free variables in
forward-chaining rules, as well as user control over how such free
variables are handled.  See FREE-VARIABLES for a background
discussion.

     ; First let us introduce a transitive operation, op, and prove a
     ; forward-chaining rule stating the transitivity of op.

     (encapsulate
      (((op * *) => *))
      (local (defun op (x y) (< x y)))
      (defthm transitivity-of-op
        (implies (and (op x y) (op y z)) (op x z))
        :rule-classes :forward-chaining))

     ; The following theorem is proved by forward chaining, using the above rule.

     (thm
      (implies (and (op u v) (op v w) (op v a))
               (op u w)))

     ; The proof of the theorem just above succeeds because the term (op u v)
     ; triggers the application of forward-chaining rule transitivity-of-op,
     ; binding x to u and y to v.  Free variable z of that rule is bound to both w
     ; and to a, resulting in the addition of both (op u w) and (op u a) to the
     ; context.  However, (op v a) happens to be at the front of the context, so
     ; if only one free-variable binding had been allowed, then z would have only
     ; been bound to a, not to w, as we now illustrate.

     (add-match-free-override :once (:forward-chaining transitivity-of-op))

     (thm ; FAILS!
      (implies (and (op u v) (op v w) (op v a))
               (op u w)))

     :ubt! 1

     ; Starting over, this time we prove transitivity-of-op as a :match-free :once
     ; forward-chaining rule.  Note that the presence of :match-free eliminates
     ; the free-variables warning that we got the first time.

     (encapsulate
      (((op * *) => *))
      (local (defun op (x y) (< x y)))
      (defthm transitivity-of-op
        (implies (and (op x y) (op y z)) (op x z))
        :rule-classes ((:forward-chaining :match-free :once))))

     (thm ; FAILS!
      (implies (and (op u v) (op v w) (op v a))
               (op u w)))

     ; Notice that if we swap the order of the last two hypotheses the theorem
     ; goes through, because this time (op v w) is first in the context.

     (thm ; SUCCEEDS!
      (implies (and (op u v) (op v a) (op v w))
               (op u w)))

     :u

     ; Now let's try setting the default to :once.

     (set-match-free-default :once)

     ; We still get a free-variables warning when we admit this forward-chaining rule.

     (encapsulate
      (((op * *) => *))
      (local (defun op (x y) (< x y)))
      (defthm transitivity-of-op
        (implies (and (op x y) (op y z)) (op x z))
        :rule-classes ((:forward-chaining))))

     ; This theorem fails--as it should.

     (thm ; FAILS!
      (implies (and (op u v) (op v w) (op v a))
               (op u w)))

     ; But if we convert this rule (or here, all possible rules) to :all rules,
     ; then the proof succeeds.

     (add-match-free-override :all t)

     (thm ; SUCCEEDS!
      (implies (and (op u v) (op v w) (op v a))
               (op u w)))

     ; Now let's test a relatively slow :all case (the next thm below).

     :ubt! 1

     (encapsulate
      (((op1 *) => *)
       ((op3 * * *) => *))
      (local (defun op1 (x) (declare (ignore x)) t))
      (local (defun op3 (x0 x1 x2)
               (declare (ignore x0 x1 x2))
               t))
      (defthm op1-op3-property
        (implies (and (op1 x0) (op1 x1) (op1 x2))
                 (op3 x0 x1 x2))
        :rule-classes ((:forward-chaining :match-free :all))))

     ; The following succeeds, but takes a little time (about a second in one run).

     (thm (implies
           (and (op1 a0) (op1 a1) (op1 a2) (op1 a3) (op1 a4) (op1 a5)
                (op1 a6) (op1 a7) (op1 a8) (op1 a9) (op1 a10) (op1 a11)
                (op1 a12) (op1 a13) (op1 a14) (op1 a15) (op1 a16)
                (op1 a17) (op1 a18) (op1 a19) (op1 a20))
           (op3 a5 a6 a0)))

     (add-match-free-override :once t)

     ; The same theorem now fails because of the add-match-free-override, but is
     ; more than an order of magnitude faster.

     (thm (implies
           (and (op1 a0) (op1 a1) (op1 a2) (op1 a3) (op1 a4) (op1 a5)
                (op1 a6) (op1 a7) (op1 a8) (op1 a9) (op1 a10) (op1 a11)
                (op1 a12) (op1 a13) (op1 a14) (op1 a15) (op1 a16)
                (op1 a17) (op1 a18) (op1 a19) (op1 a20))
           (op3 a5 a6 a0)))

     ; A slight variant succeeds in a negligible amount of time (still with the
     ; :once override above).

     (thm (implies
           (and (op1 a0) (op1 a1) (op1 a2) (op1 a3) (op1 a4) (op1 a5)
                (op1 a6) (op1 a7) (op1 a8) (op1 a9) (op1 a10) (op1 a11)
                (op1 a12) (op1 a13) (op1 a14) (op1 a15) (op1 a16)
                (op1 a17) (op1 a18) (op1 a19) (op1 a20))
           (op3 a5 a20 a20)))

     ; Reality check: This shouldn't give a free-variables warning, and everything
     ; should work great since there are no free variables with this trigger term.

     :ubt! 1

     (encapsulate
      (((op1 *) => *)
       ((op7 * * * * * * *) => *))
      (local (defun op1 (x)
               (declare (ignore x))
               t))
      (local (defun op7 (x0 x1 x2 x3 x4 x5 x6)
               (declare (ignore x0 x1 x2 x3 x4 x5 x6))
               t))
      (defthm op1-op7-property
        (implies (and (op1 x0) (op1 x1) (op1 x2)
                      (op1 x3) (op1 x4) (op1 x5) (op1 x6))
                 (op7 x0 x1 x2 x3 x4 x5 x6))
        :rule-classes ((:forward-chaining
                        :trigger-terms ((op7 x0 x1 x2 x3 x4 x5 x6))))))

     ; The following then succeeds, and very quickly.

     (thm (implies (and (op1 a0) (op1 a1) (op1 a2)
                        (op1 a3) (op1 a4) (op1 a5) (op1 a6))
                   (op7 a4 a6 a5 a6 a6 a6 a6)))

FREE-VARIABLES-EXAMPLES-REWRITE    examples pertaining to free variables in rewrite rules

The following examples illustrate ACL2's handling of free variables in
rewrite rules, as well as user control over how such free variables are
handled.  See FREE-VARIABLES for a background discussion.

     ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
     ;;; Example 1
     ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

     (defstub p2 (x y) t) ; introduce unconstrained function

     ; Get warning because of free variable.  This would be an error if you had
     ; first executed (set-match-free-error t) in order to force yourself to
     ; specify :match-free (illustrated later, below).
     (defaxiom p2-trans
       (implies (and (p2 x y)
                     (p2 y z))
                (p2 x z)))

     ; Succeeds.
     (thm (implies (and (p2 a c)
                        (p2 a b)
                        (p2 c d))
                   (p2 a d)))

     ; The following causes an error because p2-trans is not a rune.
     (add-match-free-override :once p2-trans)

     ; After the following, the rewrite rule p2-trans will only allow one
     ; attempt per hypothesis to bind free variables.
     (add-match-free-override :once (:rewrite p2-trans))

     ; Now this same theorem fails to be proved.  Here's why.  The
     ; context for proving (p2 a d) happens to include the hypotheses in
     ; reverse order.  So when the first hypothesis of p2-trans, namely
     ; (p2 x y), is relieved, where x is bound to a (as we are attempting
     ; to rewrite the current literal (p2 a d)), we find (p2 a b) in the
     ; context before (p2 a c) and hence y is bound to b.  The
     ; instantiated second hypothesis of p2-trans is thus (p2 b d), and
     ; the proof fails.  Before the add-match-free-override form above,
     ; the proof succeeded because the rewriter was allowed to backtrack
     ; and find the other binding for the first hypothesis of p2-trans,
     ; namely, y bound to c.  Then the instantiated second hypothesis of
     ; p2-trans is (p2 c d), which is known to be true in the current
     ; context.
     (thm (implies (and (p2 a c)
                        (p2 a b)
                        (p2 c d))
                   (p2 a d)))

     ; Return to original behavior for binding free variables.
     (add-match-free-override :all t)

     ; Succeeds once again.
     (thm (implies (and (p2 a c)
                        (p2 a b)
                        (p2 c d))
                   (p2 a d)))

     (u) ; undo (add-match-free-override :all t)

     ; This is an error, since no further arguments should appear after
     ; :clear.
     (add-match-free-override :clear t)

     ; Return all rules to original behavior for binding free variables,
     ; regardless of which previous add-match-free-override forms have
     ; been executed.
     (add-match-free-override :clear)

     ; This succeeds just as it did originally.
     (thm (implies (and (p2 a c)
                        (p2 a b)
                        (p2 c d))
                   (p2 a d)))

     (ubt! 'p2-trans) ; back to the start, except retain the defstub

     ; Require that :match-free be specified for :linear and :rewrite rules with
     ; free variables.
     (set-match-free-error t)

     ; Fails because :match-free is missing.
     (defaxiom p2-trans
       (implies (and (p2 x y)
                     (p2 y z))
                (p2 x z)))

     ; Fails because :match-free must be followed by :once or :all.
     (defaxiom p2-trans
       (implies (and (p2 x y)
                     (p2 y z))
                (p2 x z))
       :rule-classes ((:rewrite :match-free nil)))

     ; Succeeds, this time with no warning at all.
     (defaxiom p2-trans
       (implies (and (p2 x y)
                     (p2 y z))
                (p2 x z))
       :rule-classes ((:rewrite :match-free :once)))

     ; Fails because we only bind once (see earlier long comment).
     (thm (implies (and (p2 a c)
                        (p2 a b)
                        (p2 c d))
                   (p2 a d)))

     ; Treat p2-trans as though `:match-free :all' had been specified.
     (add-match-free-override :all (:rewrite p2-trans))

     ; Succeeds since more than one binding is allowed for p2-trans.
     (thm (implies (and (p2 a c)
                        (p2 a b)
                        (p2 c d))
                   (p2 a d)))

     (u)
     (u)

     ; Specify that future :linear and :rewrite rules with free variables
     ; that do not have :match-free specified are treated as though
     ; `:match-free :once' were specified.
     (set-match-free-default :once)

     ; Succeeds without error since `:match-free' is specified, as described
     ; above.  But there is a warning, since :match-free is not specified for this
     ; :rewrite rule.
     (defaxiom p2-trans
       (implies (and (p2 x y)
                     (p2 y z))
                (p2 x z)))

     ; Fails since only single bindings are allowed for p2-trans.
     (thm (implies (and (p2 a c)
                        (p2 a b)
                        (p2 c d))
                   (p2 a d)))

     ; Treat p2-trans as though `:match-free :all' had been specified.
     (add-match-free-override :all t)

     ; Succeeds.
     (thm (implies (and (p2 a c)
                        (p2 a b)
                        (p2 c d))
                   (p2 a d)))

     ; Test searching of ground units, i.e. rewrite rules without variables on the
     ; left side of the conclusion, for use in relieving hypotheses with free
     ; variables.  This is a very contrived example.

     (ubt! 1) ; back to the start

     (encapsulate
      (((p1 *) => *)
       ((p2 * *) => *)
       ((p3 *) => *)
       ((a) => *)
       ((b) => *))
      (local (defun p1 (x) x))
      (local (defun p2 (x y) (list x y)))
      (local (defun p3 (x) x))
      (local (defun a () 0))
      (local (defun b () 0)))

     ; Allow default of :match-free :all (form may be omitted).
     (set-match-free-error nil)

     (defaxiom ax1
       (implies (and (p2 x y)
                     (p1 y))
                (p3 x)))

     (defaxiom p2-a-b
       (p2 (a) (b)))

     (defaxiom p2-a-a
       (p2 (a) (a)))

     (defaxiom p1-b
       (p1 (b)))

     ; Succeeds; see long comment below on next attempt to prove this
     ; theorem.
     (thm (implies (p2 (a) y)
                   (p3 (a))))

     ; Now ax1 will only relieve hypothesis (p2 x y) for one binding of y:
     (add-match-free-override :once t)

     ; Fails when ax1 attempts to rewrite the conclusion to true, because
     ; the most recent ground unit for hypothesis (p2 x y) with x bound
     ; to (a) is rule p2-a-a, which binds y to (a).  If more than one ground
     ; unit could be used then we would backtrack and apply rule p2-a-b,
     ; which binds y to (b) and hence hypothesis (p1 y) of ax1 is
     ; relieved by rule p1-b.
     (thm (implies (p2 (a) y)
                   (p3 (a))))

     ; Return rules to original :match-free behavior.
     (add-match-free-override :clear)

     ; Succeeds once again.
     (thm (implies (p2 (a) y)
                   (p3 (a))))

     ; Just for kicks, change the behavior of a built-in rule irrelevant
     ; to the proof at hand.
     (add-match-free-override :once (:rewrite string<-l-trichotomy))

     ; Still succeeds.
     (thm (implies (p2 (a) y)
                   (p3 (a))))

     ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
     ;;; Example 2
     ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

The next example illustrates the use of the break-rewrite facility to
get information about handling of free variables by the rewriter.
Explanation is given after this (edited) transcript.  Input begins on
lines with a prompt (search for "ACL2"); the rest is output.

     ACL2 !>(encapsulate
             ((p1 (u x) t)
              (bad (x) t)
              (p2 (x y z) t)
              (bar (x y) t)
              (foo (x y) t)
              (poo (x y) t)
              (prop (u) t))

             (local (defun p1 (u x) (declare (ignore u x)) nil))
             (local (defun bad (x) (declare (ignore x)) nil))
             (local (defun p2 (x y z) (declare (ignore x y z)) nil))
             (local (defun bar (x y) (declare (ignore x y)) nil))
             (local (defun foo (x y) (declare (ignore x y)) nil))
             (local (defun poo (x y) (declare (ignore x y)) nil))
             (local (defun prop (u) (declare (ignore u)) t))

             (defthm foo-poo
               (implies (syntaxp (equal y 'y3))
                        (equal (foo x y)
                               (poo x y))))

             (defthm lemma-1
               (implies (and (p1 u x)
                             (bad x)
                             (p2 x y z)
                             (bar x y)
                             (equal x x) ; admittedly silly!
                             (foo x y))
                        (prop u))
               :rule-classes ((:rewrite :match-free :all))))

     ; [[ output omitted ]]

     Summary
     Form:  ( ENCAPSULATE ((P1 ...) ...) ...)
     Rules: NIL
     Warnings:  Subsume and Non-rec
     Time:  0.08 seconds (prove: 0.00, print: 0.01, other: 0.06)
      T
     ACL2 !>:brr t
     The monitored runes are:
     NIL
      T
     ACL2 !>:monitor (:rewrite lemma-1) t
     (((:REWRITE LEMMA-1) 'T))
     ACL2 !>(thm (implies (and (p1 u0 x1)
                               (bad x1)
                               (bad x3)
                               (bar x3 y1)
                               (bar x3 y3)
                               (p1 u0 x2)
                               (p1 u0 x3)
                               (p2 x3 y1 z1)
                               (p2 x3 y3 z1))
                          (prop u0)))

     (1 Breaking (:REWRITE LEMMA-1) on (PROP U0):
     1 ACL2 >:eval

     1x (:REWRITE LEMMA-1) failed because :HYP 1 contains free variables.
     The following display summarizes the attempts to relieve hypotheses
     by binding free variables; see :DOC free-variables.

         [1] X : X1
     Failed because :HYP 3 contains free variables Y and Z, for which no
     suitable bindings were found.
         [1] X : X2
     Failed because :HYP 2 rewrote to (BAD X2).
         [1] X : X3
             [3] Z : Z1
                 Y : Y1
     Failed because :HYP 6 rewrote to (FOO X3 Y1).
             [3] Z : Z1
                 Y : Y3
     Failed because :HYP 6 rewrote to (POO X3 Y3).

     1 ACL2 >:unify-subst
          U : U0
     1 ACL2 >

The :eval command above asks the rewriter to attempt to apply the
rewrite rule lemma-1 to the term (prop u0), shown just above the line
with :eval.  As we can see at the end, the variable u in the conclusion
of lemma-1 is being bound to the variable u0 in the conjecture.  The
first hypothesis of lemma-1 is (p1 u x), so the rewriter looks for some
x for which (p1 u0 x) is known to be true.  It finds x1, and then goes
on to consider the second hypothesis, (bad x).  Since the theorem we
are proving has (bad x1) in the hypothesis and x is currently bound to
x1, the rewriter is satisfied and moves on to the third hypothesis of
lemma-1, (p2 x y z).  However, x is bound to x1 and there are no
instances of y and z for which (p2 x1 y z) is known in the current
context.  All of the above analysis is summarized in the first part of
the output from :eval above:

         [1] X : X1
     Failed because :HYP 3 contains free variables Y and Z, for which no
     suitable bindings were found.

Thus, the binding of x to x1 on behalf of the first hypothesis has
failed.

The rewriter now backs up to look for other values of x that satisfy the
first hypothesis, and finds x2 because our current theorem has a
hypothesis of (p1 u0 x2).  But this time, the second hypothesis of
lemma-1, (bad x), is not known to be true for x; that is, (bad x2) does
not rewrite to t; in fact, it rewrites to itself.  That explains the
next part of the output from :eval above:

         [1] X : X2
     Failed because :HYP 2 rewrote to (BAD X2).

The rewriter now backs up again to look for other values of x that
satisfy the first hypothesis, and finds x3 because our current theorem
has a hypothesis of (p1 u0 x3).  This time, the second hypothesis of
lemma-1 is not a problem, and moreover, the rewriter is able to bind y
and z to y1 and z1, respectively, in order to satisfy the third
hypothesis, (p2 x y z): that is, (p2 x2 y1 z1) is known in the current
context.  That explains more of the above output from :eval:

         [1] X : X3
             [3] Z : Z1
                 Y : Y1

Unfortunately, the sixth hypothesis, (foo x y), rewrites to itself
under the above bindings:

     Failed because :HYP 6 rewrote to (FOO X3 Y1).

So the rewriter looks for other bindings to satisfy the third
hypothesis and finds these.

             [3] Z : Z1
                 Y : Y3

This time, the sixth hypothesis can be rewritten under the above
bindings, from (foo x3 y3) to (poo x3 y3) by lemma foo-poo, but still
not to t.

     Failed because :HYP 6 rewrote to (POO X3 Y3).

There are no more free variable bindings to try, so this concludes the
output from :eval.

     ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
     ;;; Example 3
     ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

The next pair of examples illustrates so-called "binding hypotheses"
(see FREE-VARIABLES) and explores some of their subtleties.
The first shows binding hypotheses in action on a simple example.  The
second shows how binding hypotheses interact with equivalence relations
and explains the role of double-rewrite.

Our first example sets up a theory with two user-supplied rewrite
rules, one of which has a binding hypothesis.  Below we explain how
that binding hypothesis contributes to the proof.

     ; Define some unary functions.
     (defun f (x) (declare (ignore x)) t)
     (defun g (x) x)
     (defun h (x) x)
     (defun k (x) x)

     ; Prove some simple lemmas.  Note the binding hypothesis in g-rewrite.
     (defthm f-k-h
       (f (k (h x))))
     (defthm g-rewrite
            (implies (and (equal y (k x)) ; binding hypothesis
                          (f y))
                     (equal (g x) y)))

     ; Restrict to a theory that includes the above lemmas but avoids the above
     ; definitions.
     (in-theory (union-theories (theory 'minimal-theory)
                                '(f-k-h g-rewrite)))

     ; Prove a theorem.
     (thm (equal (g (h a)) (k (h a))))

Let us look at how ACL2 uses the above binding hypothesis in the proof
of the preceding thm form.  The rewriter considers the term (g (h a))
and finds a match with the left-hand side of the rule g-rewrite, binding
x to (h a).  The first hypothesis binds y to the result of rewriting (k
x) in the current context, where the variable x is bound to the term (h
a); thus y is bound to (k (h a)).  The second hypothesis, (f y), is
then rewritten under this binding, and the result is t by application
of the rewrite rule f-k-h.  The rule g-rewrite is then applied under
the already-mentioned binding of x to (h a).  This rule application
triggers a recursive rewrite of the right-hand side of g-rewrite, which
is y, in a context where y is bound (as discussed above) to (k (h a)).
The result of this rewrite is that same term, (k (h a)).  The original
call of equal then trivially rewrites to t.

We move on now to our second example, which is similar but involves a
user-defined equivalence relation.  You may find it helpful to review
:equivalence rules; see EQUIVALENCE.

Recall that when a hypothesis is a call of an equivalence relation
other than equal, the second argument must be a call of double-rewrite
in order for the hypothesis to be treated as a binding hypothesis.
That is indeed the case below; an explanation follows.

     ; Define an equivalence relation.
     (defun my-equiv (x y) (equal x y))
     (defequiv my-equiv) ; introduces rule MY-EQUIV-IS-AN-EQUIVALENCE

     ; Define some unary functions
     (defun f (x) (declare (ignore x)) t)
     (defun g (x) x)
     (defun h1 (x) x)
     (defun h2 (x) x)

     ; Prove some simple lemmas.  Note the binding hypothesis in lemma-3.
     (defthm lemma-1
       (my-equiv (h1 x) (h2 x)))
     (defthm lemma-2
       (f (h2 x)))
     (defthm lemma-3
            (implies (and (my-equiv y (double-rewrite x)) ; binding hypothesis
                          (f y))
                     (equal (g x) y)))

     ; Restrict to a theory that includes the above lemmas but avoids the above
     ; definitions.
     (in-theory (union-theories (theory 'minimal-theory)
                                '(lemma-1 lemma-2 lemma-3
                                          my-equiv-is-an-equivalence)))

     ; Prove a theorem.
     (thm (equal (g (h1 a)) (h2 a)))

The proof succeeds much as in the first example, but the following
observation is key: when ACL2 binds y upon considering the first
hypothesis of lemma-3, it rewrites the term (double-rewrite x) in a
context where it need only preserve the equivalence relation my-equiv.
At this point, x is bound by applying lemma-3 to the term (g (h1 a));
so, x is bound to (h1 a).  The rule lemma-1 then applies to rewrite
this occurrence of x to (h2 a), but only because it suffices to
preserve my-equiv.  Thus y is ultimately bound to (h2 a), and the proof
succeeds as one would expect.

If we tweak the above example slightly by disabling the user's
equivalence rune, then the proof of the thm form fails because the
above rewrite of (double-rewrite x) is done in a context where it no
longer suffices to preserve my-equiv as we dive into the second
argument of my-equiv in the first hypothesis of lemma-3; so, lemma-1
does not apply this time.

     (in-theory (union-theories (theory 'minimal-theory)
                                '(lemma-1 lemma-2 lemma-3)))

     ; Proof fails in this case!
     (thm (equal (g (h1 a)) (h2 a)))

FREE-VARIABLES-TYPE-PRESCRIPTION    matching for free variable in type-prescription rules

We assume familiarity with the issue of dealing with free variables in
hypotheses; see FREE-VARIABLES.

By default, starting with Version  4.3, ACL2 attempts all possible
matches for free variables.  Consider the following example.

     (defstub f1 (x) t)
     (defstub f2 (x y) t)
     (defstub f3 (y) t)

     (defaxiom f1-prop
       (implies (and (f2 x y) ; <-- y is free in this hypothesis
                     (f3 y))
                (f1 x))       ; <-- (f1 x) is the type-term (type is `non-nil')
       :rule-classes :type-prescription)

     ; Succeeds:
     (thm (implies (and (f2 a b)
                        (f3 b))
                   (f1 a)))

     ; The following fails unless we try more than one match for free variables in
     ; hypotheses.
     (thm (implies (and (f2 a b)
                        (f2 a c)
                        (f2 a d)
                        (f3 b))
                   (f1 a)))

There may be times when you want to match only the first free variable.
In that case, you can write a function of two arguments, the
type-prescription rune being applied and the current ACL2 world, that
prohibits multiple matching for those times.  Your function is then
`attached' to the built-in constrained function, oncep-ts.  The
following examples are intended to explain how this works.

First, let us disallow all mutliple matching of free variables (i.e.,
implement the behavior often referred to as ":match-free :once"; see
FREE-VARIABLES).

     (defun oncep-tp-always (rune wrld)
       (declare (ignore rune wrld)
                (xargs :mode :logic :guard t))
       t)

     (defattach oncep-tp oncep-tp-always)

The second thm form above will now fail, because only one free-variable
match is permitted for the first hypothesis of rule f1-prop above.

Now suppose that instead, we want to disallow multiple matches for free
variables in hypotheses of type-prescription rules _except_ for the
rule f1-prop above.  With the following events, the second thm form
above once again succeeds.

     (defun oncep-tp-always-except-f1-prop (rune wrld)
       (declare (ignore wrld)
                (xargs :mode :logic :guard (and (consp rune)
                                                (consp (cdr rune))
                                                (symbolp (cadr rune)))))
       (not (eq (base-symbol rune) 'f1-prop)))

     (defattach oncep-tp oncep-tp-always-except-f1-prop)

In general, your defattach event will attach a function symbol to
oncep-tp.  The guard of that function symbol must be implied by the
tuard of oncep-tp:

     ACL2 !>:args oncep-tp

     Function         ONCEP-TP
     Formals:         (RUNE WRLD)
     Signature:       (ONCEP-TP * *)
                      => *
     Guard:           (AND (PLIST-WORLDP WRLD)
                           (CONSP RUNE)
                           (CONSP (CDR RUNE))
                           (SYMBOLP (CADR RUNE)))
     Guards Verified: T
     Defun-Mode:      :logic
     Type:            built-in (or unrestricted)

      ONCEP-TP
     ACL2 !>

GENERALIZE    make a rule to restrict generalizations

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 :generalize rule might be built is:

     Example:
     any theorem

     General Form:
     any theorem

To use such a :generalize rule, the system waits until it has decided
to generalize some term, term, by replacing it with some new variable
v.  If any :generalize formula can be instantiated so that some
non-variable subterm becomes term, then that instance of the formula is
added as a hypothesis.

At the moment, the best description of how ACL2 :generalize rules are
used may be found in the discussion of "Generalize Rules," page 248 of
A Computational Logic Handbook, or "Generalization," page 132 of
"Computer-Aided Reasoning: An Approach."  Also see
INTRODUCTION-TO-THE-THEOREM-PROVER for detailed tutorial on using ACL2
to prove theorems, which includes some discussion of generalization.

INDUCTION    make a rule that suggests a certain induction

     Example:
     (:induction :corollary t  ; the theorem proved is irrelevant!
                 :pattern (* 1/2 i)
                 :condition (and (integerp i) (>= i 0))
                 :scheme (recursion-by-sub2 i))

In ACL2, as in Nqthm, the functions in a conjecture "suggest" the
inductions considered by the system.  Because every recursive function
must be admitted with a justification in terms of a measure that
decreases in a well-founded way on a given set of "controlling"
arguments, every recursive function suggests a dual induction scheme
that "unwinds" the function from a given application.

For example, since append (actually binary-append, but we'll ignore the
distinction here) decomposes its first argument by successive cdrs as
long as it is a non-nil true list, the induction scheme suggested by
(append x y) has a base case supposing x to be either not a true list
or to be nil and then has an induction step in which the induction
hypothesis is obtained by replacing x by (cdr x).  This substitution
decreases the same measure used to justify the definition of append.
Observe that an induction scheme is suggested by a recursive function
application only if the controlling actuals are distinct variables, a
condition that is sufficient to ensure that the "substitution" used to
create the induction hypothesis is indeed a substitution and that it
drives down a certain measure.  In particular, (append (foo x) y) does
not suggest an induction unwinding append because the induction scheme
suggested by (append x y) requires that we substitute (cdr x) for x and
we cannot do that if x is not a variable symbol.

Once ACL2 has collected together all the suggested induction schemes it
massages them in various ways, combining some to simultaneously unwind
certain cliques of functions and vetoing others because they "flaw"
others.  We do not further discuss the induction heuristics here; the
interested reader should see Chapter XIV of A Computational Logic
(Boyer and Moore, Academic Press, 1979) which represents a fairly
complete description of the induction heuristics of ACL2.

However, unlike Nqthm, ACL2 provides a means by which the user can
elaborate the rules under which function applications suggest induction
schemes.  Such rules are called :induction rules.  The definitional
principle automatically creates an :induction rule, named (:induction
fn), for each admitted recursive function, fn.  It is this rule that
links applications of fn to the induction scheme it suggests.
Disabling (:induction fn) will prevent fn from suggesting the induction
scheme derived from its recursive definition.  It is possible for the
user to create additional :induction rules by using the :induction rule
class in defthm.

Technically we are "overloading" defthm by using it in the creation of
:induction rules because no theorem need be proved to set up the
heuristic link represented by an :induction rule.  However, since
defthm is generally used to create rules and rule-class objects are
generally used to specify the exact form of each rule, we maintain that
convention and introduce the notion of an :induction rule.  An
:induction rule can be created from any lemma whatsoever.

     General Form of an :induction Lemma or Corollary:
     T

     General Form of an :induction rule-class:
     (:induction :pattern pat-term
                 :condition cond-term
                 :scheme scheme-term)

where pat-term, cond-term, and scheme-term are all terms, pat-term is
the application of a function symbol, fn, scheme-term is the
application of a function symbol, rec-fn, that suggests an induction,
and, finally, every free variable of cond-term and scheme-term is a
free variable of pat-term.  We actually check that rec-fn is either
recursively defined -- so that it suggests the induction that is
intrinsic to its recursion -- or else that another :induction rule has
been proved linking a call of rec-fn as the :pattern to some scheme.

The induction rule created is used as follows.  When an instance of the
:pattern term occurs in a conjecture to be proved by induction and the
corresponding instance of the :condition term is known to be non-nil
(by type reasoning alone), the corresponding instance of the :scheme
term is created and the rule "suggests" the induction, if any,
suggested by that term.  (Analysis of that term may further involve
induction rules, though the applied rule is removed from consideration
during that further analysis, in order to avoid looping.)  If rec-fn is
recursive, then the suggestion is the one that unwinds that recursion.

Consider, for example, the example given above,

     (:induction :pattern (* 1/2 i)
                 :condition (and (integerp i) (>= i 0))
                 :scheme (recursion-by-sub2 i)).

In this example, we imagine that recursion-by-sub2 is the function:

     (defun recursion-by-sub2 (i)
       (if (and (integerp i)
                (< 1 i))
           (recursion-by-sub2 (- i 2))
           t))

Observe that this function recursively decomposes its integer argument
by subtracting 2 from it repeatedly and stops when the argument is 1 or
less.  The value of the function is irrelevant; it is its induction
scheme that concerns us.  The induction scheme suggested by
(recursion-by-sub2 i) is

     (and (implies (not (and (integerp i) (< 1 i)))   ; base case
                   (:p i))
          (implies (and (and (integerp i) (< 1 i))    ; induction step
                        (:p (- i 2)))
                   (:p i)))

We can think of the base case as covering two situations.  The first is
when i is not an integer.  The second is when the integer i is 0 or 1.
In the base case we must prove (:p i) without further help.  The
induction step deals with those integer i greater than 1, and
inductively assumes the conjecture for i-2 while proving it for i.  Let
us call this scheme "induction on i by twos."

Suppose the above :induction rule has been added.  Then an occurrence
of, say, (* 1/2 k) in a conjecture to be proved by induction would
suggest, via this rule, an induction on k by twos, provided k was known
to be a nonnegative integer.  This is because the induction rule's
:pattern is matched in the conjecture, its :condition is satisfied, and
the :scheme suggested by the rule is that derived from
(recursion-by-sub2 k), which is induction on k by twos.  Similarly, the
term (* 1/2 (length l)) would suggest no induction via this rule, even
though the rule "fires" because it creates the :scheme
(recursion-by-sub2 (length l)) which suggests no inductions unwinding
recursion-by-sub2 (since the controlling argument of recursion-by-sub2
in this :scheme is not a variable symbol).

Continuing this example one step further illustrates the utility of
:induction rules.  We could define the function recursion-by-cddr that
suggests the induction scheme decomposing its consp argument two cdrs
at a time.  We could then add the :induction rule linking (* 1/2
(length x)) to (recursion-by-cddr x) and arrange for (* 1/2 (length l))
to suggest induction on l by cddr.

Observe that :induction rules require no proofs to be done.  Such a
rule is merely a heuristic link between the :pattern term, which may
occur in conjectures to be proved by induction, and the :scheme term,
from which an induction scheme may be derived.  Hence, when an
:induction rule-class is specified in a defthm event, the theorem
proved is irrelevant.  The easiest theorem to prove is, of course, t.
Thus, we suggest that when an :induction rule is to be created, the
following form be used:

     (defthm name T
       :rule-classes ((:induction :pattern pat-term
                                  :condition cond-term
                                  :scheme scheme-term)))

The name of the rule created is (:induction name).  When that rune is
disabled the heuristic link between pat-term and scheme-term is broken.

LINEAR    make some arithmetic inequality rules

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 :linear rule might be built is:

     Example:
     (implies (and (eqlablep e)           if inequality reasoning begins to
                   (true-listp x))        consider how (length (member a b))
              (<= (length (member e x))   compares to any other term, add to
                  (length x)))            set of known inequalities the fact
                                          that it is no larger than (length b),
                                          provided (eqlablep a) and (true-listp b)
                                          rewrite to t

     General Form:
     (and ...
          (implies (and ...hi...)
                   (implies (and ...hk...)
                            (and ...
                                 (rel lhs rhs)
                                 ...)))
          ...)

Note: One :linear rule class object might create many linear arithmetic
rules from the :corollary formula.  To create the rules, we first
flatten the and and implies structure of the formula, transforming it
into a conjunction of formulas, each of the form

     (implies (and h1 ... hn) (rel lhs rhs))

where no hypothesis is a conjunction and rel is one of the inequality
relations <, <=, =, >, or >=.  If necessary, the hypothesis of such a
conjunct may be vacuous.  We create a :linear rule for each such
conjunct, if possible, and otherwise cause an error.

Each rule has one or more "trigger terms" which may be specified by the
user using the :trigger-terms field of the rule class or which may be
defaulted to values chosen by the system.  We discuss the determination
of trigger terms after discussing how linear rules are used.

:Linear rules are used by an arithmetic decision procedure during
rewriting.  See LINEAR-ARITHMETIC and see
NON-LINEAR-ARITHMETIC.  Here we assume that the reader is familiar
with the material described in linear-arithmetic.

Recall that we eliminate the unknowns of an inequality in term-order,
largest unknowns first.  (See TERM-ORDER.)  In order to
facilitate this strategy, we store the inequalities in "linear pots".
For purposes of the present discussion, let us say that an inequality
is "about" its largest unknown.  Then, all of the inequalities about a
particular unknown are stored in the same linear pot, and the pot is
said to be "labeled" with that unknown.  This storage layout groups all
of the inequalities which are potential candidates for cancellation
with each other into one place.  It is also key to the efficient
operation of :linear rules.

If the arithmetic decision procedure has stabilized and not yielded a
contradiction, we scan through the list of linear pots examining each
label as we go.  If the trigger term of some :linear rule can be
instantiated to match the label, we so instantiate that rule and
attempt to relieve the hypotheses with general-purpose rewriting.  If
we are successful, we add the rule's instantiated conclusion to our set
of inequalities.  This may let cancellation continue.

Note: Problems may arise if you explicitly store a linear lemma under a
trigger term that, when instantiated, is not the largest unknown in the
instantiated concluding inequality.  Suppose for example you store the
linear rule (<= (fn i j) (/ i (* j j))) under the trigger term (fn i j).
Then when the system "needs" an inequality about (fn a b), (i.e.,
because (fn a b) is the label of some linear pot, and hence the largest
unknown in some inequality), it will appeal to the rule and deduce (<=
(fn a b) (/ a (* b b))).  However, the largest unknown in this
inequality is (/ a (* b b)) and hence it will be stored in a linear pot
labeled with (/ a (* b b)).  The original, triggering inequality which
is in a pot about (fn a b) will therefore not be cancelled against the
new one.  It is generally best to specify as a trigger term one of the
"maximal" terms of the polynomial, as described below.

We now describe how the trigger terms are determined.  Most of the
time, the trigger terms are not specified by the user and are instead
selected by the system.  However, the user may specify the terms by
including an explicit :trigger-terms field in the rule class, e.g.,

     General Form of a Linear Rule Class:
     (:LINEAR :COROLLARY formula
              :TRIGGER-TERMS (term1 ... termk))

Each termi must be a term and must not be a variable, quoted constant,
lambda application, let-expression or if-expression.  In addition, each
termi must be such that if all the variables in the term are
instantiated and then the hypotheses of the corollary formula are
relieved (possibly instantiating additional free variables), then all
the variables in the concluding inequality are instantiated.  We
generate a linear rule for each conjuctive branch through the corollary
and store each rule under each of the specified triggers.  Thus, if the
corollary formula contains several conjuncts, the variable restrictions
on the termi must hold for each conjunct.

If :trigger-terms is omitted the system computes a set of trigger terms.
Each conjunct of the corollary formula may be given a unique set of
triggers depending on the variables that occur in the conjunct and the
addends that occur in the concluding inequality.  In particular, the
trigger terms for a conjunct is the list of all "maximal addends" in
the concluding inequality.

The "addends" of (+ x y) and (- x y) are the union of the addends of x
and y.  The addends of (- x) and (* n x), where n is a rational
constant, is just {x}.  The addends of an inequality are the union of
the addends of the left- and right-hand sides.  The addends of any
other term, x, is {x}.

A term is maximal for a conjunct (implies hyps concl) of the corollary
if (a) the term is a non-variable, non-quote, non-lambda application,
non-let and non-if expression, (b) the term contains enough variables
so that when they are instantiated and the hypotheses are relieved
(which may bind some free variables; see FREE-VARIABLES) then
all the variables in concl are instantiated, and (c) no other addend is
always "bigger" than the term, in the technical sense described below.

The technical notion referenced above depends on the notion of
_fn-count_, the number of function symbols in a term, and
_pseudo-fn-count_, which is essentially the number of function symbols
implicit in a constant (see TERM-ORDER, specifically the
discussion of "pseudo-function application count" at the end).  We say
term1 is always bigger than term2 if all instances of term1 have a
larger fn-count (actually lexicographic order of fn-count and
pseudo-fn-count) than the corresponding instances of term2.  This is
equivalent to saying that the fn-count of term1 is larger than that of
term2 (by "fn-count" here we mean the lexicographic order of fn-count
and pseudo-fn-count) and the variable bag for term2 is a subbag of that
for term1.  For example, (/ a (* b b)) is always bigger than (fn a b)
because the first has two function applications and {a b} is a subbag
of a b b, but (/ a (* b b)) is not always bigger than (fn a x).