This is documentation for ACL2 Version 3.6
Copyright (C) 2009  University of Texas at Austin

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

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

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

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

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; see ACL2-TUTORIAL.

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-CLAUSES.

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 has, with much help from Bill Young,
been substantially improved to a bona fide introduction, and has been
renamed acl2-tutorial.

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-CLAUSES

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

     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
       :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).

Related topics other than immediate subtopics:

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 :rule-classes ((:rewrite)) had been used.  Use
:rule-classes nil to specify that no rules are to be generated.

If :rule-classes class is specified, where class is a non-nil symbol,
it is as though :rule-classes ((class)) had been used.  Thus,
:rule-classes :forward-chaining is equivalent to :rule-classes
((:forward-chaining)).

We therefore now consider :rule-classes as a true list.  If any element
of that list is a keyword, replace it by the singleton list containing
that keyword.  Thus, :rule-classes (:rewrite :elim) is the same as
:rule-classes ((:rewrite) (:elim)).

Each element of the expanded value of :rule-classes must be a true list
whose car is one of the rule class keyword tokens listed above, e.g.,
:rewrite, :elim, etc., and whose cdr is a "keyword alist" alternately
listing keywords and values.  The keywords in this alist must be taken
from those shown below.  They may be listed in any order and most may
be omitted, as specified below.

     :Corollary -- its value, term, must be a term.  If omitted, this
     field defaults to thm.  The :corollary of a rule class object is
     the formula actually used to justify the rule created and thus
     determines the form of the rule.  Nqthm provided no similar
     capability: each rule was determined by thm, the theorem or axiom
     added.  ACL2 permits thm to be stated "elegantly" and then allows
     the :corollary of a rule class object to specify how that elegant
     statement is to be interpreted as a rule.  For the rule class
     object to be well-formed, its (defaulted) :corollary, term, must
     follow from thm.  Unless term is trivially implied by thm, using
     little more than propositional logic, the formula (implies thm
     term) is submitted to the theorem prover and the proof attempt
     must be successful.  During that proof attempt the values of
     :hints, :instructions, and :otf-flg, as provided in the rule class
     object, are provided as arguments to the prover.  Such auxiliary
     proofs give the sort of output that one expects from the prover.
     However, as noted above, corollaries that follow trivially are not
     submitted to the prover; thus, such corollaries cause no prover
     output.

     Note that before term is stored, all calls of macros in it are
     expanded away.  See TRANS.

     :Hints, :instructions, :otf-flg -- the values of these fields must
     satisfy the same restrictions placed on the fields of the same
     names in defthm.  These values are passed to the recursive call of
     the prover used to establish that the :corollary of the rule class
     object follows from the theorem or axiom thm.

     :Type-set -- this field may be supplied only if the :class is
     :type-set-inverter.  When provided, the value must be a type-set,
     an integer in a certain range.  If not provided, an attempt is
     made to compute it from the corollary.  See
     TYPE-SET-INVERTER.

     :Typed-term -- this field may be supplied only if the :class is
     :type-prescription.  When provided, the value is the term for which
     the :corollary is a type-prescription lemma.  If no :typed-term is
     provided in a :type-prescription rule class object, we try to
     compute heuristically an acceptable term.  See
     TYPE-PRESCRIPTION.

     :Trigger-terms -- this field may be supplied only if the :class is
     :forward-chaining or :linear.  When provided, the value is a list
     of terms, each of which is to trigger the attempted application of
     the rule.  If no :trigger-terms is provided, we attempt to compute
     heuristically an appropriate set of triggers.  See
     FORWARD-CHAINING or see LINEAR.

     :Trigger-fns -- this field must (and may only) be supplied if the
     :class is :meta.  Its value must be a list of function symbols.
     Terms with these symbols trigger the application of the rule.  See
     META.

     :Clique and :controller-alist -- these two fields may only be
     supplied if the :class is :definition.  If they are omitted, then
     ACL2 will attempt to guess them.  Suppose the :corollary of the
     rule is (implies hyp (equiv (fn a1 ... an) body)).  The value of
     the :clique field should be a true list of function symbols, and if
     non-nil must include fn.  These symbols are all the members of the
     mutually recursive clique containing this definition of fn.  That
     is, a call of any function in :clique is considered a "recursive
     call" for purposes of the expansion heuristics.  The value of the
     :controller-alist field should be an alist that maps each function
     symbol in the :clique to a list of t's and nil's of length equal
     to the arity of the function.  For example, if :clique consists of
     just two symbols, fn1 and fn2, of arities 2 and 3 respectively,
     then ((fn1 t nil) (fn2 nil t t)) is a legal value of
     :controller-alist.  The value associated with a function symbol in
     this alist is a "mask" specifying which argument slots of the
     function "control" the recursion for heuristic purposes.  Sloppy
     choice of :clique or :controller-alist can result in infinite
     expansion and stack overflow.

     :Install-body -- this field may only be supplied if the :class is
     :definition.  Its value must be t, nil, or the default,
     :normalize.  A value of t or :normalize will cause ACL2 to install
     this rule as the new body of the function being "defined" (fn in
     the paragraph just above); hence this definition will be installed
     for future :expand hints.  Furthermore, if this field is omitted
     or the value is :normalize, then this definition will be
     simplified using the so-called "normalization" procedure that is
     used when processing definitions made with defun.  You must
     explicitly specify :install-body nil in the following cases: fn
     (as above) is a member of the value of constant
     *definition-minimal-theory*, the arguments are not a list of
     distinct variables, equiv (as above) is not equal, or there are
     free variables in the hypotheses or right-hand side (see
     FREE-VARIABLES).  However, supplying :install-body nil will not
     affect the rewriter's application of the :definition rule, other
     than to avoid using the rule to apply :expand hints.  If a
     definition rule equates (f a1 ... ak) with body but there are
     hypotheses, hyps, then :expand hints will replace terms (f term1
     ... termk) by corresponding terms (if hyps body (hide (f term1 ...
     termk))).

     :Loop-stopper -- this field may only be supplied if the class is
     :rewrite.  Its value must be a list of entries each consisting of
     two variables followed by a (possibly empty) list of functions,
     for example ((x y binary-+) (u v foo bar)).  It will be used to
     restrict application of rewrite rules by requiring that the list
     of instances of the second variables must be "smaller" than the
     list of instances of the first variables in a sense related to the
     corresponding functions listed; see LOOP-STOPPER.  The
     list as a whole is allowed to be nil, indicating that no such
     restriction shall be made.  Note that any such entry that contains
     a variable not being instantiated, i.e., not occurring on the left
     side of the rewrite rule, will be ignored.  However, for
     simplicity we merely require that every variable mentioned should
     appear somewhere in the corresponding :corollary formula.

     :Pattern, :Condition, :Scheme -- the first and last of these
     fields must (and may only) be supplied if the class is :induction.
     :Condition is optional but may only be supplied if the class is
     :induction.  The values must all be terms and indicate,
     respectively, the pattern to which a new induction scheme is to be
     attached, the condition under which the suggestion is to be made,
     and a term which suggests the new scheme.  See INDUCTION.

     :Match-free -- this field must be :all or :once and may be
     supplied only if the :class is either :rewrite, :linear, or
     :forward-chaining.  See FREE-VARIABLES for a description
     of this field.  Note: Although this field is intended to be used
     for controlling retries of matching free variables in hypotheses,
     it is legal to supply it even if there are no such free variables.
     This can simplify the automated generation of rules, but note
     that when :match-free is supplied, the warning otherwise provided
     for the presence of free variables in hypotheses will be
     suppressed.

     Backchain-limit-lst -- this field may be supplied only if the
     :class is either :rewrite, :meta, or :linear.  It is further
     required either only one rule is generated from the formula or, at
     least, every such rule has the same list of hypotheses.  The value
     for :Backchain-limit-lst must be nil; a non-negative integer; or,
     except in the case of :meta rules, a true list each element of
     which is either nil or a non-negative integer.  If it is a list,
     its length must be equal to the number of hypotheses of the rule
     and each item in the list is the "backchain limit" associated with
     the corresponding hypothesis.  If backchain-limit-lst is a
     non-negative integer, it is defaulted to a list of the appropriate
     number of repetitions of that integer.  The backchain limit of a
     hypothesis is used to limit the effort that ACL2 will expend when
     relieving the hypothesis.  If it is NIL, no new limits are
     imposed; if it is an integer, the hypothesis will be limited to
     backchaining at most that many times.  Note that backchaining may
     be further limited by a global backchain-limit; see
     BACKCHAIN-LIMIT for details.  For a different way to reign in
     the rewriter, see REWRITE-STACK-LIMIT.  Jared Davis has
     pointed out that you can set this field to 0 to avoid any attempt
     to relieve forced hypotheses, which can lead to a significant
     speed-up in some cases.

Once thm has been proved (in the case of defthm) and each rule class
object has been checked for well-formedness (which might require
additional proofs), we consider each rule class object in turn to
generate and add rules.  Let :class be the class keyword token of the
ith class object (counting from left to right).  Generate the rune
(:class name . x), where x is nil if there is only one class and
otherwise x is i.  Then, from the :corollary of that object, generate
one or more rules, each of which has the name (:class name . x).  See
the :doc entry for each rule class to see how formulas determine rules.
Note that it is in principle possible for several rules to share the
same name; it happens whenever a :corollary determines more than one
rule.  This in fact only occurs for :rewrite, :linear, and
:forward-chaining class rules and only then if the :corollary is
essentially a conjunction.  (See the documentation for rewrite, linear,
or forward-chaining for details.)

BUILT-IN-CLAUSES    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 :expand hints as
described in the preceding paragraph.  Also see SET-BODY and
see SHOW-BODIES for how to change the body of a function symbol.

Note only that if you prove a definition rule for function foo, say,
foo-new-def, you will need to refer to that definition as foo-new-def
or as (:DEFINITION foo-new-def).  That is because a :definition rule
does not change the meaning of the symbol foo for :use hints, nor does
it change the meaning of the symbol foo in theory expressions; see
THEORIES, in particular the discussion there of runic
designators.  Similarly :pe foo and :pf foo will still show the
original definition of foo.

The definitional principle, defun, actually adds :definition rules.
Thus the handling of generalized definitions is exactly the same as for
"real" definitions because no distinction is made in the implementation.
Suppose (fn x y) is defun'd to be body.  Note that defun (or defuns or
mutual-recursion) can compute the clique for fn from the syntactic
presentation and it can compute the controllers from the termination
analysis.  Provided the definition is admissible, defun adds the
:definition rule (equal (fn x y) body).

ELIM    make a destructor elimination rule

See RULE-CLASSES for a general discussion of rule classes and
how they are used to build rules from formulas.  Here we describe the
class of :elim rules, which is fundamentally quite different from the
more common class of :rewrite rules.  Briefly put, a :rewrite rule
replaces instances of its left-hand side with corresponding instances
of its right-hand side.  But an :elim rule, on the other hand, has the
effect of generalizing so-called "destructor" function applications to
variables.  In essence, applicability of a :rewrite rule is based on
matching its left-hand side, while applicability of an :elim rule is
based on the presence of at least one destructor term.

For example, a conjecture about (car x) and (cdr x) can be replaced by
a conjecture about new variables x1 and x2, as shown in the following
example.  (Run the command :mini-proveall and search for CAR-CDR-ELIM
to see the full proof containing this excerpt.)

     Subgoal *1/1'
     (IMPLIES (AND (CONSP X)
                   (TRUE-LISTP (REV (CDR X))))
              (TRUE-LISTP (APP (REV (CDR X)) (LIST (CAR X))))).

     The destructor terms (CAR X) and (CDR X) can be eliminated by using
     CAR-CDR-ELIM to replace X by (CONS X1 X2), (CAR X) by X1 and (CDR X)
     by X2.  This produces the following goal.

     Subgoal *1/1''
     (IMPLIES (AND (CONSP (CONS X1 X2))
                   (TRUE-LISTP (REV X2)))
              (TRUE-LISTP (APP (REV X2) (LIST X1)))).

     This simplifies, using primitive type reasoning, to

     Subgoal *1/1'''
     (IMPLIES (TRUE-LISTP (REV X2))
              (TRUE-LISTP (APP (REV X2) (LIST X1)))).

The resulting conjecture is often simpler and hence more amenable to
proof.

The application of an :elim rule thus replaces a variable by a term that
contains applications of so-called "destructor" functions to that
variable.  The example above is typical: the variable x is replaced by
the term (cons (car x) (cdr x)), which applies a so-called "constructor"
function, cons, to applications (car x) and (cdr x) of destructor
functions car and cdr to that same variable, x.  But that is only part
of the story.  ACL2 then generalizes the destructor applications (car
x) and (cdr x) to new variables x1 and x2, respectively, and ultimately
the result is a simpler conjecture.

More generally, the application of an :elim rule replaces a variable by
a term containing applications of destructors; there need not be a
clear-cut notion of "constructor."  But the situation described above
is typical, and we will focus on it, giving full details when we
introduce the "General Form" below.

The example above employs the following built-in :elim rule named
car-cdr-elim.

     Example:
     (implies (consp x)                      when (car v) or (cdr v) appears
              (equal (cons (car x) (cdr x))  in a conjecture, and v is a
                     x))                     variable, consider replacing v by
                                             (cons a b), for two new variables
                                             a and b.

     Notice that the situation is complicated a bit by the fact that this
     replacement is only valid if the variable being replaced a cons structure.
     Thus, when ACL2 applies car-cdr-elim to replace a variable v, it will
     split into two cases: one case in which (consp v) is true, in which v
     is replaced by (cons (car v) (cdr v)) and then (car v) and
     (cdr v) are generalized to new variables; and one case in which
     (consp v) is false.  In practice, (consp v) is often provable,
     perhaps even literally present as a hypotheses; then of course there is no
     need to introduce the second case.  That is why there is no such second case
     in the example above.

     You might find :elim rules to be useful whenever you have in mind a data
     type that can be built up from its fields with a ``constructor'' function and
     whose fields can be accessed by corresponding ``destructor'' functions.  So
     for example, if you have a ``house'' data structure that represents a house
     in terms of its address, price, and color, you might have a rule like the
     following.
          Example:
          (implies (house-p x)
                   (equal (make-house (address x)
                                      (price x)
                                      (color x))
                          x))

     The application of such a rule is entirely analogous to the application of
     the rule car-cdr-elim discussed above.  We discuss such rules and their
     application more carefully below.

     General Form:
     (implies hyp (equiv lhs x))

where equiv is a known equivalence relation (see DEFEQUIV); x
is a variable symbol; and lhs contains one or more terms (called
"destructor terms") of the form (fn v1 ... vn), where fn is a function
symbol and the vi are distinct variable symbols, v1, ..., vn include
all the variable symbols in the formula, no fn occurs in lhs in more
than one destructor term, and all occurrences of x in lhs are inside
destructor terms.

To use an :elim rule, the theorem prover waits until a conjecture has
been maximally simplified.  It then searches for an instance of some
destructor term (fn v1 ... vn) in the conjecture, where the instance for
x is some variable symbol, vi, and every occurrence of vi outside the
destructor terms is in an equiv-hittable position.  If such an instance
is found, then the theorem prover instantiates the :elim formula as
indicated by the destructor term matched; splits the conjecture into two
goals, according to whether the instantiated hypothesis, hyp, holds; and
in the case that it does hold, generalizes all the instantiated
destructor terms in the conjecture to new variables and then replaces
vi in the conjecture by the generalized instantiated lhs.  An
occurrence of vi is "equiv-hittable" if sufficient congruence rules
(see DEFCONG) have been proved to establish that the
propositional value of the clause is not altered by replacing that
occurrence of vi by some equiv-equivalent term.

If an :elim rule is not applied when you think it should have been, and
the rule uses an equivalence relation, equiv, other than equal, it is
most likely that there is an occurrence of the variable that is not
equiv-hittable.  Easy occurrences to overlook are those in the
governing hypotheses.  If you see an unjustified occurrence of the
variable, you must prove the appropriate congruence rule to allow the
:elim to fire.

Further examples of how ACL2 :elim rules are used may be found in the
corresponding discussion of "Elimation of Destructors" for Nqthm, in
Section 10.4 of A Computational Logic Handbook.

EQUIVALENCE    mark a relation as an equivalence relation

See RULE-CLASSES for a general discussion of rule classes and
how they are used to build rules from formulas.  An example :corollary
formula from which a :equivalence rule might be built is as follows.
(We assume that r-equal has been defined.)

     Example:
     (and (booleanp (r-equal x y))
          (r-equal x x)
          (implies (r-equal x y) (r-equal y x))
          (implies (and (r-equal x y)
                        (r-equal y z))
                   (r-equal x z))).

Also see DEFEQUIV.

     General Form:
     (and (booleanp (equiv x y))
          (equiv x x)
          (implies (equiv x y) (equiv y x))
          (implies (and (equiv x y)
                        (equiv y z))
                   (equiv x z)))

except that the order of the conjuncts and terms and the choice of
variable symbols is unimportant.  The effect of such a rule is to
identify equiv as an equivalence relation.  Note that only Boolean
2-place function symbols can be treated as equivalence relations.  See
CONGRUENCE and see REFINEMENT for closely related
concepts.

The macro form (defequiv equiv) is an abbreviation for a defthm of
rule-class :equivalence that establishes that equiv is an equivalence
relation.  It generates the formula shown above.  See DEFEQUIV.

When equiv is marked as an equivalence relation, its reflexivity,
symmetry, and transitivity are built into the system in a deeper way
than via :rewrite rules.  More importantly, after equiv has been shown
to be an equivalence relation, lemmas about equiv, e.g.,

     (implies hyps (equiv lhs rhs)),

when stored as :rewrite rules, cause the system to rewrite certain
occurrences of (instances of) lhs to (instances of) rhs.  Roughly
speaking, an occurrence of lhs in the kth argument of some
fn-expression, (fn ... lhs' ...), can be rewritten to produce (fn ...
rhs' ...), provided the system "knows" that the value of fn is
unaffected by equiv-substitution in the kth argument.  Such knowledge
is communicated to the system via "congruence lemmas."

For example, suppose that r-equal is known to be an equivalence
relation.  The :congruence lemma

     (implies (r-equal s1 s2)
              (equal (fn s1 n) (fn s2 n)))

informs the rewriter that, while rewriting the first argument of
fn-expressions, it is permitted to use r-equal rewrite-rules.  See
CONGRUENCE for details about :congruence lemmas.
Interestingly, congruence lemmas are automatically created when an
equivalence relation is stored, saying that either of the equivalence
relation's arguments may be replaced by an equivalent argument.  That
is, if the equivalence relation is fn, we store congruence rules that
state the following fact:

     (implies (and (fn x1 y1)
                   (fn x2 y2))
              (iff (fn x1 x2) (fn y1 y2)))

Another aspect of equivalence relations is that of "refinement."  We
say equiv1 "refines" equiv2 iff (equiv1 x y) implies (equiv2 x y).
:refinement rules permit you to establish such connections between your
equivalence relations.  The value of refinements is that if the system
is trying to rewrite something while maintaining equiv2 it is permitted
to use as a :rewrite rule any refinement of equiv2.  Thus, if equiv1 is
a refinement of equiv2 and there are equiv1 rewrite-rules available,
they can be brought to bear while maintaining equiv2.  See
REFINEMENT.

The system initially has knowledge of two equivalence relations,
equality, denoted by the symbol equal, and propositional equivalence,
denoted by iff.  Equal is known to be a refinement of all equivalence
relations and to preserve equality across all arguments of all
functions.

Typically there are five steps involved in introducing and using a new
equivalence relation, equiv.

     (1) Define equiv,

     (2) prove the :equivalence lemma about equiv,

     (3) prove the :congruence lemmas that show where equiv can be used
     to maintain known relations,

     (4) prove the :refinement lemmas that relate equiv to known
     relations other than equal, and

     (5) develop the theory of conditional :rewrite rules that drive
     equiv rewriting.

More will be written about this as we develop the techniques.  For now,
here is an example that shows how to make use of equivalence relations
in rewriting.

Among the theorems proved below is

     (defthm insert-sort-is-id
       (perm (insert-sort x) x))

Here perm is defined as usual with delete and is proved to be an
equivalence relation and to be a congruence relation for cons and
member.

Then we prove the lemma

     (defthm insert-is-cons
       (perm (insert a x) (cons a x)))

which you must think of as you would (insert a x) = (cons a x).

Now prove (perm (insert-sort x) x).  The base case is trivial.  The
induction step is

        (consp x)
      & (perm (insert-sort (cdr x)) (cdr x))

     -> (perm (insert-sort x) x).

Opening insert-sort makes the conclusion be

        (perm (insert (car x) (insert-sort (cdr x))) x).

Then apply the induction hypothesis (rewriting (insert-sort (cdr x)) to
(cdr x)), to make the conclusion be

     (perm (insert (car x) (cdr x)) x)

Then apply insert-is-cons to get (perm (cons (car x) (cdr x)) x).  But
we know that (cons (car x) (cdr x)) is x, so we get (perm x x) which is
trivial, since perm is an equivalence relation.

Here are the events.

     (encapsulate (((lt * *) => *))
       (local (defun lt (x y) (declare (ignore x y)) nil))
       (defthm lt-non-symmetric (implies (lt x y) (not (lt y x)))))

     (defun insert (x lst)
       (cond ((atom lst) (list x))
             ((lt x (car lst)) (cons x lst))
             (t (cons (car lst) (insert x (cdr lst))))))

     (defun insert-sort (lst)
       (cond ((atom lst) nil)
             (t (insert (car lst) (insert-sort (cdr lst))))))

     (defun del (x lst)
       (cond ((atom lst) nil)
             ((equal x (car lst)) (cdr lst))
             (t (cons (car lst) (del x (cdr lst))))))

     (defun mem (x lst)
       (cond ((atom lst) nil)
             ((equal x (car lst)) t)
             (t (mem x (cdr lst)))))

     (defun perm (lst1 lst2)
       (cond ((atom lst1) (atom lst2))
             ((mem (car lst1) lst2)
              (perm (cdr lst1) (del (car lst1) lst2)))
             (t nil)))

     (defthm perm-reflexive
       (perm x x))

     (defthm perm-cons
       (implies (mem a x)
                (equal (perm x (cons a y))
                       (perm (del a x) y)))
       :hints (("Goal" :induct (perm x y))))

     (defthm perm-symmetric
       (implies (perm x y) (perm y x)))

     (defthm mem-del
       (implies (mem a (del b x)) (mem a x)))

     (defthm perm-mem
       (implies (and (perm x y)
                     (mem a x))
                (mem a y)))

     (defthm mem-del2
       (implies (and (mem a x)
                     (not (equal a b)))
                (mem a (del b x))))

     (defthm comm-del
       (equal (del a (del b x)) (del b (del a x))))

     (defthm perm-del
       (implies (perm x y)
                (perm (del a x) (del a y))))

     (defthm perm-transitive
       (implies (and (perm x y) (perm y z)) (perm x z)))

     (defequiv perm)

     (in-theory (disable perm
                         perm-reflexive
                         perm-symmetric
                         perm-transitive))

     (defcong perm perm (cons x y) 2)

     (defcong perm iff (mem x y) 2)

     (defthm atom-perm
       (implies (not (consp x)) (perm x nil))
       :rule-classes :forward-chaining
       :hints (("Goal" :in-theory (enable perm))))

     (defthm insert-is-cons
       (perm (insert a x) (cons a x)))

     (defthm insert-sort-is-id
       (perm (insert-sort x) x))

     (defun app (x y) (if (consp x) (cons (car x) (app (cdr x) y)) y))

     (defun rev (x)
       (if (consp x) (app (rev (cdr x)) (list (car x))) nil))

     (defcong perm perm (app x y) 2)

     (defthm app-cons
       (perm (app a (cons b c)) (cons b (app a c))))

     (defthm app-commutes
       (perm (app a b) (app b a)))

     (defcong perm perm (app x y) 1
       :hints (("Goal" :induct (app y x))))

     (defthm rev-is-id (perm (rev x) x))

     (defun == (x y)
       (if (consp x)
           (if (consp y)
               (and (equal (car x) (car y))
                    (== (cdr x) (cdr y)))
               nil)
           (not (consp y))))

     (defthm ==-reflexive (== x x))

     (defthm ==-symmetric (implies (== x y) (== y x)))

     (defequiv ==)

     (in-theory (disable ==-symmetric ==-reflexive))

     (defcong == == (cons x y) 2)

     (defcong == iff (consp x) 1)

     (defcong == == (app x y) 2)

     (defcong == == (app x y) 1)

     (defthm rev-rev (== (rev (rev x)) x))

FORWARD-CHAINING    make a rule to forward chain when a certain trigger arises

See RULE-CLASSES for a general discussion of rule classes and
how they are used to build rules from formulas.  An example :corollary
formula from which a :forward-chaining rule might be built is:

     Example:
     (implies (and (p x) (r x))        when (p a) appears in a formula to be
              (q (f x)))               simplified, try to establish (r a) and
                                       if successful, add (q (f a)) to the
                                       known assumptions

To specify the triggering terms provide a non-empty list of terms as
the value of the :trigger-terms field of the rule class object.

     General Form:
     Any theorem, provided an acceptable triggering term exists.

Forward chaining rules are generated from the corollary term as follows.
First, every let expression is expanded away (hence, so is every let*
and lambda expression), as is every call of a so-called "guard holder"
(must-be-equal, prog2$, ec-call, the).  If the resulting term has the
form (implies hyp concl), then concl is treated as a conjunction, with
one forward chaining rule with hypothesis hyp created for each
conjunct.  In the other case, where the corollary term is not an
implies, we process it as we process the conclusion in the first case.

The :trigger-terms field of a :forward-chaining rule class object
should be a non-empty list of terms, if provided, and should have
certain properties described below.  If the :trigger-terms field is not
provided, it defaults to the singleton list containing the "atom" of
the first hypothesis of the formula.  (The atom of (not x) is x; the
atom of any other term is the term itself.)  If there are no hypotheses
and no :trigger-terms were provided, an error is caused.

A triggering term is acceptable if it is not a variable, a quoted
constant, a lambda application, a let- (or let*-) expression, or a
not-expression, and every variable symbol in the conclusion of the
theorem either occurs in the hypotheses or occurs in the trigger.

:Forward-chaining rules are used by the simplifier before it begins to
rewrite the literals of the goal.  (Forward chaining is thus carried
out from scratch for each goal.)  If any term in the goal is an
instance of a trigger of some forward chaining rule, we try to
establish the hypotheses of that forward chaining theorem (from the
negation of the goal).  To relieve a hypothesis we only use type
reasoning, evaluation of ground terms, and presence among our known
assumptions.  We do not use rewriting.  So-called free variables in
hypotheses are treated specially; see FREE-VARIABLES.  If all
hypotheses are relieved, we add the instantiated conclusion to our known
assumptions.

_Caution_.  Forward chaining does not actually add terms to the goals
displayed during proof attempts.  Instead, it extends an associated
_context_, called "assumptions" in the preceding paragraph, that ACL2
builds from the goal currently being proved.  The context starts out
with "obvious" consequences of the negation of the goal.  For example,
if the goal is

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

then the context notes that (p x) and (q (f x)) are non-nil and (c x)
is nil.  Forward chaining is then used to expand the context.  For
example, if a forward chaining rule has (f x) as a trigger term and has
body (implies (p x) (r (f x))), then the context is extended by binding
(r (f x)) to non-nil.  Note however that since (r (f x)) is put into
the context, not the goal, it is _not_ further simplified.  If f is an
enabled nonrecursive function symbol then this forward chaining rule
may well be useless, since calls of f may be expanded away.

However, forward-chaining does support the linear arithmetic reasoning
package.  For example, suppose that forward-chaining puts (< (f x) (g
x)) into the context.  Then this inequality also goes into the linear
arithmetic data base, together with suitable instances of linear lemmas
whose trigger term is a call of g.  See LINEAR.

FREE-VARIABLES    free variables in rules

As described elsewhere (see RULE-CLASSES), ACL2 rules are
treated as implications for which there are zero or more hypotheses hj
to prove.  In particular, rules of class :rewrite may look like this:

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

Variables of hi are said to occur _free_ in the above :rewrite rule if
they do not occur in lhs or in any hj with j<i.  (To be precise, here
we are only discussing those variables that are not in the scope of a
let/let*/lambda that binds them.)  We also refer to these as the _free
variables_ of the rule.  ACL2 issues a warning or error when there are
free variables in a rule, as described below.  (Variables of rhs may be
considered free if they do not occur in lhs or in any hj.  But we do
not consider those in this discussion.)

In general, the _free variables_ of rules are those variables occurring
in their hypotheses (not let/let*/lambda-bound) that are not bound when
the rule is applied.  For rules of class :linear and :forward-chaining,
variables are bound by a trigger term.  (See RULE-CLASSES for a
discussion of the :trigger-terms field).  For rules of class
:type-prescription, variables are bound by the :typed-term field.

Let us discuss the method for relieving hypotheses of rewrite rules with
free variables.  Similar considerations apply to linear and
forward-chaining rules, while for other rules (in particular,
type-prescription rules), only one binding is tried, much as described
in the discussion about :once below.

See FREE-VARIABLES-EXAMPLES for more examples of how this all
works, including illustration of how the user can exercise some control
over it.  In particular, see FREE-VARIABLES-EXAMPLES-REWRITE
for an explanation of output from the break-rewrite facility in the
presence of rewriting failures involving free variables.

We begin with an example.  Does the proof of the thm below succeed?

     (defstub p2 (x y) t)

     (defaxiom p2-trans
       (implies (and (p2 x y)
                     (p2 y z))
                (equal (p2 x z) t))
       :rule-classes ((:rewrite :match-free :all)))

     (thm (implies (and (p2 a c)
                        (p2 a b)
                        (p2 c d))
                   (p2 a d)))

Consider what happens when the proof of the thm is attempted.  The ACL2
rewriter attempts to apply rule p2-trans to the conclusion, (p2 a d).
So, it binds variables x and z from the left-hand side of the
conclusion of p2-trans to terms a and d, respectively, and then
attempts to relieve the hypotheses of p2-trans.  The first hypothesis of
p2-trans, (p2 x y), is considered first.  Variable y is free in that
hypothesis, i.e., it has not yet been bound.  Since x is bound to a,
the rewriter looks through the context for a binding of y such that (p2
a y) is true, and it so happens that it first finds the term (p2 a b),
thus binding y to b.  Now it goes on to the next hypothesis, (p2 y z).
At this point y and z have already been bound to b and d; but (p2 b d)
cannot be proved.

So, in order for the proof of the thm to succeed, the rewriter needs to
backtrack and look for another way to instantiate the first hypothesis
of p2-trans.  Because :match-free :all has been specified, backtracking
does take place.  This time y is bound to c, and the subsequent
instantiated hypothesis becomes (p2 c d), which is true.  The
application of rule (p2-trans) succeeds and the theorem is proved.

If instead :match-free :all had been replaced by :match-free :once in
rule p2-trans, then backtracking would not occur, and the proof of the
thm would fail.

Next we describe in detail the steps used by the rewriter in dealing
with free variables.

ACL2 uses the following sequence of steps to relieve a hypothesis with
free variables, except that steps (1) and (3) are skipped for
:forward-chaining rules and step (3) is skipped for :type-prescription
rules.  First, if the hypothesis is of the form (force hyp0) or
(case-split hyp0), then replace it with hyp0.  (1) Suppose the
hypothesis has the form (equiv var term) where var is free and no
variable of term is free, and either equiv is equal or else equiv is a
known equivalence relation and term is a call of double-rewrite.  Then
bind var to the result of rewriting term in the current context.  (2)
Look for a binding of the free variables of the hypothesis so that the
corresponding instance of the hypothesis is known to be true in the
current context.  (3) Search all enabled, hypothesis-free rewrite rules
of the form (equiv lhs rhs), where lhs has no variables (other than
those bound by let, let*, or lambda), rhs is known to be true in the
current context, and equiv is typically equal but can be any equivalence
relation appropriate for the current context (see CONGRUENCE);
then attempt to bind the free variables so that the instantiated
hypothesis is lhs.  If all attempts fail and the original hypothesis is
a call of force or case-split, where forcing is enabled (see
FORCE) then the hypothesis is relieved, but in the split-off goals,
all free variables are bound to unusual names that call attention to
this odd situation.

When a rewrite or linear rule has free variables in the hypotheses, the
user generally needs to specify whether to consider only the first
instance found in steps (2) and (3) above, or instead to consider them
all.  Below we discuss how to specify these two options as ":once" or
":all" (the default), respectively.

Is it better to specify :once or :all?  We believe that :all is
generally the better choice because of its greater power, provided the
user does not introduce a large number of rules with free variables,
which has been known to slow down the prover due to combinatorial
explosion in the search (Steps (2) and (3) above).

Either way, it is good practice to put the "more substantial" hypotheses
first, so that the most likely bindings of free variables will be found
first (in the case of :all) or found at all (in the case of :once).  For
example, a rewrite rule like

     (implies (and (p1 x y)
                   (p2 x y))
              (equal (bar x) (bar-prime x)))

may never succeed if p1 is nonrecursive and enabled, since we may well
not find calls of p1 in the current context.  If however p2 is disabled
or recursive, then the above rule may apply if the two hypotheses are
switched.  For in that case, we can hope for a match of (p2 x y) in the
current context that therefore binds x and y; then the rewriter's full
power may be brought to bear to prove (p1 x y) for that x and y.

Moreover, the ordering of hypotheses can affect the efficiency of the
rewriter.  For example, the rule

     (implies (and (rationalp y)
                   (foo x y))
              (equal (bar x) (bar-prime x)))

may well be sub-optimal.  Presumably the intention is to rewrite (bar x)
to (bar-prime x) in a context where (foo x y) is explicitly known to be
true for some rational number y.  But y will be bound first to the
first term found in the current context that is known to represent a
rational number.  If the 100th such y that is found is the first one
for which (foo x y) is known to be true, then wasted work will have
been done on behalf of the first 99 such terms y -- unless :once has
been specified, in which case the rule will simply fail after the first
binding of y for which (rationalp y) is known to be true.  Thus, a
better form of the above rule is almost certainly the following.

     (implies (and (foo x y)
                   (rationalp y))
              (equal (bar x) (bar-prime x)))

_Specifying `once' or `all'._ One method for specifying :once or :all
for free-variable matching is to provide the :match-free field of the
:rule-classes of the rule, for example, (:rewrite :match-free :all).
See RULE-CLASSES.  However, there are global events that can be
used to specify :once or :all; see SET-MATCH-FREE-DEFAULT and
see ADD-MATCH-FREE-OVERRIDE.  Here are some examples.

     (set-match-free-default :once)    ; future rules without a :match-free field
                                       ; are stored as :match-free :once (but this
                                       ; behavior is local to a book)
     (add-match-free-override :once t) ; existing rules are treated as
                                       ; :match-free :once regardless of their
                                       ; original :match-free fields
     (add-match-free-override :once (:rewrite foo) (:rewrite bar . 2))
                                       ; the two indicated rules are treated as
                                       ; :match-free :once regardless of their
                                       ; original :match-free fields

_Some history._ Before Version  2.7 the ACL2 rewriter performed Step (2)
above first.  More significantly, it always acted as though :once had
been specified.  That is, if Step (2) did not apply, then the rewriter
took the first binding it found using either Steps (1) or (3), in that
order, and proceeded to relieve the remaining hypotheses without trying
any other bindings of the free variables of that hypothesis.

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

The examples in the two sub-topics of this topic illustrate the
handling of free variables in rules of class :rewrite (see
FREE-VARIABLES-EXAMPLES-REWRITE) and of class :forward-chaining (see
FREE-VARIABLES-EXAMPLES-FORWARD-CHAINING), respectively.  These
implicitly illustrate free-variables handling in rules of class :linear
as well.  Also see FREE-VARIABLES and see RULE-CLASSES.

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.

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

     ;;;;;;;;;;

FINALLY, here is an example illustrating 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.

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."

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.  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).

META    make a :meta rule (a hand-written simplifier)

See RULE-CLASSES for a general discussion of rule classes and
how they are used to build rules from formulas.  Meta rules extend the
ACL2 simplifier with hand-written code to transform certain terms to
equivalent ones.  To add a meta rule, the :corollary formula must
establish that the hand-written "metafunction" preserves the meaning of
the transformed term.

While our intention is that the set of ACL2 documentation topics is
self-contained, readers might find it useful to see the following paper
for an introduction to meta reasoning in ACL2.

     W. A. Hunt, Jr., R. B. Krug, M. Kaufmann, J S. Moore and E. W.
     Smith, "Meta Reasoning in ACL2."  TPHOLs 2005, ed. J. Hurd and T.
     F. Melham, LNCS 3603, Springer-Verlag, Berlin, 2005, pp. 163-178.

Example :corollary formulas from which :meta rules might be built are:

     Examples:
     (equal (evl x a)                  ; Modify the rewriter to use fn to
            (evl (fn x) a))            ; transform terms.  The :trigger-fns
                                       ; of the :meta rule-class specify
                                       ; the top-most function symbols of
                                       ; those x that are candidates for
                                       ; this transformation.

     (implies (and (pseudo-termp x)    ; As above, but this illustrates
                   (alistp a))         ; that without loss of generality we
              (equal (evl x a)         ; may restrict x to be shaped like a
                     (evl (fn x) a)))  ; term and a to be an alist.

     (implies (and (pseudo-termp x)    ; As above (with or without the
                   (alistp a)          ; hypotheses on x and a) with the
                   (evl (hyp-fn x) a)) ; additional restriction that the
              (equal (evl x a)         ; meaning of (hyp-fn x) is true in
                     (evl (fn x) a)))  ; the current context.  That is, the
                                       ; applicability of the transforma-
                                       ; tion may be dependent upon some
                                       ; computed hypotheses.

A non-nil list of function symbols must be supplied as the value of the
:trigger-fns field in a :meta rule class object.

     General Forms:
     (implies (and (pseudo-termp x)        ; this hyp is optional
                   (alistp a)              ; this hyp is optional
                   (ev (hyp-fn x ...) a))  ; this hyp is optional
              (equiv (ev x a)
                     (ev (fn x ...) a)))

where equiv is a known equivalence relation, x and a are distinct
variable names, and ev is an evaluator function (see below), and fn is
a function symbol, as is hyp-fn when provided.  The arguments to fn and
hyp-fn should be identical.  In the most common case, both take a
single argument, x, which denotes the term to be simplified.  If fn
and/or hyp-fn are guarded, their guards should be (implied by)
pseudo-termp.  See PSEUDO-TERMP.  We say the theorem above is a
"metatheorem" or "metalemma" and fn is a "metafunction", and hyp-fn is
a "hypothesis metafunction".

If "..." is empty, i.e., the metafunctions take just one argument, we
say they are "vanilla flavored."  If "..." is non-empty, we say the
metafunctions are "extended."  Extended metafunctions can access state
and context sensitive information to compute their results, within
certain limits.  We discuss vanilla metafunctions here and recommend a
thorough understanding of them before proceeding (at which time see
EXTENDED-METAFUNCTIONS).

Metafunctions and (if supplied) hypothesis metafunctions must be
executable.  That is, they cannot be constrained (i.e., introduced in
the signature of encapsulate events), nor can they be declared
:non-executable.  After all, there is no point in installing a
simplifier that cannot be run!

We defer discussion of the case in which there is a hypothesis
metafunction and for now address the case in which the other two
hypotheses are present.

In the discussion below, we refer to the argument, x, of fn and hyp-fn
as a "term."  When these metafunctions are executed by the simplifier,
they will be applied to (the quotations of) terms.  But during the
proof of the metatheorem itself, x may not be the quotation of a term.
If the pseudo-termp hypothesis is omitted, x may be any object.  Even
with the pseudo-termp hypothesis, x may merely "look like a term" but
use non-function symbols or function symbols of incorrect arity.  In
any case, the metatheorem is stronger than necessary to allow us to
apply the metafunctions to terms, as we do in the discussion below.  We
return later to the question of proving the metatheorem.

Suppose the general form of the metatheorem above is proved with the
pseudo-termp and alistp hypotheses.  Then when the simplifier
encounters a term, (h t1 ... tn), that begins with a function symbol,
h, listed in :trigger-fns, it applies the metafunction, fn, to the
quotation of the term, i.e., it evaluates (fn '(h t1 ... tn)) to obtain
some result, which can be written as 'val.  If 'val is different from
'(h t1 ... tn) and val is a term, then (h t1 ... tn) is replaced by
val, which is then passed along for further rewriting.  Because the
metatheorem establishes the correctness of fn for all terms (even
non-terms!), there is no restriction on which function symbols are
listed in the :trigger-fns.  Generally, of course, they should be the
symbols that head up the terms simplified by the metafunction fn.  See
TERM-TABLE for how one obtains some assistance towards
guaranteeing that val is indeed a term.

The "evaluator" function, ev, is a function that can evaluate a certain
class of expressions, namely, all of those composed of variables,
constants, and applications of a fixed, finite set of function symbols,
g1, ..., gk.  Generally speaking, the set of function symbols handled
by ev is chosen to be exactly the function symbols recognized and
manipulated by the metafunctions being introduced.  For example, if fn
manipulates expressions in which 'equal and 'binary-append occur as
function symbols, then ev is generally specified to handle equal and
binary-append.  The actual requirements on ev become clear when the
metatheorem is proved.  The standard way to introduce an evaluator is to
use the ACL2 macro defevaluator, though this is not strictly necessary.
See DEFEVALUATOR if you want details.

[Aside for the logic-minded.] Why are we justified in using
metafunctions this way?  Suppose (fn 'term1) is 'term2.  What justifies
replacing term1 by term2?  The first step is to assert that term1 is
(ev 'term1 a), where a is an alist that maps 'var to var, for each
variable var in term1.  This step is incorrect, because 'term1 may
contain function symbols other than the ones, g1, ..., gk, that ev
knows how to handle.  But we can grow ev to a "larger" evaluator, ev*,
an evaluator for all of the symbols that occur in term1 or term2.  We
can prove that ev* satisfies the constraints on ev, provided no
defaxiom events are adding constraints to ev (or callers of ev, and
recursively); ACL2 checks this additional property.  Hence, the
metatheorem holds for ev* in place of ev, by functional instantiation.
We can then carry out the proof of the equivalence of term1 and term2
as follows: Fix a to be an alist that maps the quotations of the
variables of term1 and term2 to themselves.  Then,
     ev* and a = (ev* (fn 'term1) a) ; (2) by the metatheorem for ev* = (ev*
     'term2 a) ; (3) by evaluation of fn = term2 ; (4) by construction of ev* and
     a
 Note that in line (2) above, where we appeal to the (functional
instantiation of the) metatheorem, we can relieve its (optional)
pseudo-termp and alistp hypotheses by appealing to the facts that term1
is a term and a is an alist by construction.  [End of Aside for the
logic-minded.]

There are subtleties related to the notion of "growing" ev to a
"larger" evaluator, as mentioned in the paragraph just above.  For
corresponding restrictions on :meta rules, see
EVALUATOR-RESTRICTIONS.

Finally, we turn to the second case, in which there is a hypothesis
metafunction.  In that case, consider as before what happens when the
simplifier encounters a term, (h t1 ... tn), where h is listed in
:trigger-fns.  This time, after it applies fn to '(h t1 ... tn) to
obtain the quotation of some new term, 'val, it then applies the
hypothesis metafunction, hyp-fn.  That is, it evaluates (hyp-fn '(h t1
... tn)) to obtain some result, which can be written as 'hyp-val.  If
hyp-val is not in fact a term, the metafunction is not used.  Provided
hyp-val is a term, the simplifier attempts to establish (by
conventional backchaining) that this term is non-nil in the current
context.  If this attempt fails, then the meta rule is not applied.
Otherwise, (h t1...tn) is replaced by val as in the previous case
(where there was no hypothesis metafunction).

Why is it justified to make this extension to the case of hypothesis
metafunctions?  First, note that the rule

     (implies (and (pseudo-termp x)
                   (alistp a)
                   (ev (hyp-fn x) a))
              (equal (ev x a)
                     (ev (fn x) a)))

is logically equivalent to the rule

     (implies (and (pseudo-termp x)
                   (alistp a))
              (equal (ev x a)
                     (ev (new-fn x) a)))

where (new-fn x) is defined to be (list 'if (hyp-fn x) (fn x) x).  (If
we're careful, we realize that this argument depends on making an
extension of ev to an evaluator ev* that handles if and the functions
manipulated by hyp-fn.)  If we write 'term for the quotation of the
present term, and if (hyp-fn 'term) and (fn 'term) are both terms, say
hyp1 and term1, then by the previous argument we know it is sound to
rewrite term to (if hyp1 term1 term).  But since we have established in
the current context that hyp1 is non-nil, we may simplify (if hyp1
term1 term) to term1, as desired.

We now discuss the role of the pseudo-termp hypothesis.  (Pseudo-termp
x) checks that x has the shape of a term.  Roughly speaking, it ensures
that x is a symbol, a quoted constant, or a true list consisting of a
lambda expression or symbol followed by some pseudo-terms.  Among the
properties of terms not checked by pseudo-termp are that variable
symbols never begin with ampersand, lambda expressions are closed, and
function symbols are applied to the correct number of arguments.  See
PSEUDO-TERMP.

There are two possible roles for pseudo-termp in the development of a
metatheorem: it may be used as the guard of the metafunction and/or
hypothesis metafunction and it may be used as a hypothesis of the
metatheorem.  Generally speaking, the pseudo-termp hypothesis is
included in a metatheorem only if it makes it easier to prove.  The
choice is yours.  (An extreme example of this is when the metatheorem
is invalid without the hypothesis!)  We therefore address ourselves the
question: should a metafunction have a pseudo-termp guard?  A
pseudo-termp guard for a metafunction, in connection with other
considerations described below, improves the efficiency with which the
metafunction is used by the simplifier.

To make a metafunction maximally efficient you should (a) provide it
with a pseudo-termp guard and exploit the guard when possible in coding
the body of the function (see GUARDS-AND-EVALUATION, especially
the section on efficiency issues), (b) verify the guards of the
metafunction (see VERIFY-GUARDS), and (c) compile the
metafunction (see COMP).  When these three steps have been
taken the simplifier can evaluate (fn 'term1) by running the compiled
"primary code" (see GUARDS-AND-EVALUATION) for fn directly in
Common Lisp.  (Note however that explicit compilation may be
suppressed, in which case it is presumably unnecessary anyhow; see
COMPILATION.)

Before discussing efficiency issues further, let us review for a moment
the general case in which we wish to evaluate (fn 'obj) for some :logic
function.  We must first ask whether the guards of fn have been
verified.  If not, we must evaluate fn by executing its logic
definition.  This effectively checks the guards of every subroutine and
so can be slow.  If, on the other hand, the guards of fn have been
verified, then we can run the primary code for fn, provided 'obj
satisfies the guard of fn.  So we must next evaluate the guard of fn on
'obj.  If the guard is met, then we run the primary code for fn,
otherwise we run the logic code.

Now in the case of a metafunction for which the three steps above have
been followed, we know the guard is (implied by) pseudo-termp and that
it has been verified.  Furthermore, we know without checking that the
guard is met (because term1 is a term and hence 'term1 is a
pseudo-termp).  Hence, we can use the compiled primary code directly.

We strongly recommend that you compile your metafunctions, as well as
all their subroutines (unless explicit compilation is suppressed; see
COMPILATION).  Guard verification is also recommended.

Finally, we present a very simple example of the use of :meta rules,
based on one provided by Robert Krug.  This example illustrates a trick
for avoiding undesired rewriting after applying a metafunction or any
other form of rewriting.  To elaborate: in general, the term t2
obtained by applying a metafunction to a term t1 is then handed
immediately to the rewriter, which descends recursively through the
arguments of function calls to rewrite t2 completely.  But if t2 shares
a lot of structure with t1, then it might not be worthwhile to rewrite
t2 immediately.  (A rewrite of t2 will occur anyhow the next time a
goal is generated.)  The trick involves avoiding this rewrite by
wrapping t2 inside a call of hide, which in turn is inside a call of a
user-defined "unhiding" function, unhide.

     (defun unhide (x)
       (declare (xargs :guard t))
       x)

     (defthm unhide-hide
       (equal (unhide (hide x))
              x)
       :hints (("Goal" :expand ((hide x)))))

     (in-theory (disable unhide))

     (defun my-plus (x y)
       (+ x y))

     (in-theory (disable my-plus))

     (defevaluator evl evl-list
       ((my-plus x y)
        (binary-+ x y)
        (unhide x)
        (hide x)))

     (defun meta-fn (term)
       (declare (xargs :guard (pseudo-termp term)))
       (if (and (consp term)
                (equal (length term) 3)
                (equal (car term) 'my-plus))
           `(UNHIDE (HIDE (BINARY-+ ,(cadr term) ,(caddr term))))
         term))

     (defthm my-meta-lemma
       (equal (evl term a)
              (evl (meta-fn term) a))
       :hints (("Goal" :in-theory (enable my-plus)))
       :rule-classes ((:meta :trigger-fns (my-plus))))

Notice that in the following (silly) conjectre, ACL2 initially does
only does the simplification directed by the metafunction; a second
goal is generated before the commuativity of addition can be applied.
If the above calls of UNHIDE and HIDE had been stripped off, then Goal'
would have been the term printed in Goal" below.

     ACL2 !>(thm
             (equal (my-plus b a)
                    ccc))

     This simplifies, using the :meta rule MY-META-LEMMA and the :rewrite
     rule UNHIDE-HIDE, to

     Goal'
     (EQUAL (+ B A) CCC).

     This simplifies, using the :rewrite rule COMMUTATIVITY-OF-+, to

     Goal''
     (EQUAL (+ A B) CCC).

The discussion above probably suffices to make good use of this (UNHIDE
(HIDE ...)) trick.  However, we invite the reader who wishes to
understand the trick in depth to evaluate the following form before
submitting the thm form above.

     (trace$ (rewrite :entry (list (take 2 arglist))
                      :exit (list (car values)))
             (rewrite-with-lemma :entry (list (take 2 arglist))
                                 :exit (take 2 values)))

The following annotated subset of the trace output (which may appear a
bit different depending on the underlying Common Lisp implementation)
explains how the trick works.

         2> (REWRITE ((MY-PLUS B A) NIL))>
           3> (REWRITE-WITH-LEMMA
                   ((MY-PLUS B A)
                    (REWRITE-RULE (:META MY-META-LEMMA)
                                  1822
                                  NIL EQUAL META-FN NIL META NIL NIL)))>

     We apply the meta rule, then recursively rewrite the result, which is the
     (UNHIDE (HIDE ...)) term shown just below.

             4> (REWRITE ((UNHIDE (HIDE (BINARY-+ B A)))
                          ((A . A) (B . B))))>
               5> (REWRITE ((HIDE (BINARY-+ B A))
                            ((A . A) (B . B))))>

     The HIDE protects its argument from being touched by the rewriter.

               <5 (REWRITE (HIDE (BINARY-+ B A)))>
               5> (REWRITE-WITH-LEMMA
                       ((UNHIDE (HIDE (BINARY-+ B A)))
                        (REWRITE-RULE (:REWRITE UNHIDE-HIDE)
                                      1806 NIL EQUAL (UNHIDE (HIDE X))
                                      X ABBREVIATION NIL NIL)))>

     Now we apply UNHIDE-HIDE, then recursively rewrite its right-hand
     side in an environment where X is bound to (BINARY-+ B A).

                 6> (REWRITE (X ((X BINARY-+ B A))))>

     Notice that at this point X is cached, so REWRITE just returns
     (BINARY-+ B A).

                 <6 (REWRITE (BINARY-+ B A))>
               <5 (REWRITE-WITH-LEMMA T (BINARY-+ B A))>
             <4 (REWRITE (BINARY-+ B A))>
           <3 (REWRITE-WITH-LEMMA T (BINARY-+ B A))>
         <2 (REWRITE (BINARY-+ B A))>

EVALUATOR-RESTRICTIONS    some restrictions on the use of evaluators in meta-level rules

Note: This topic, which explains some subtleties for evaluators, can
probably be skipped by most readers.

Rules of class :meta and of class :clause-processor are stated using
so-called "evaluator" functions.  Here we explains some restrictions
related to evaluators.  Below we refer primarily to :meta rules, but
the discussion applies equally to :clause-processor rules.

In a nutshell, we require that a rule's evaluator does not support
other functions in the rule, and we require that the evaluator not be
introduced under a non-trivial encapsulate.  We explain these
restrictions in detail below.

An argument given elsewhere (see META, in particular "Aside for
the logic-minded") explains that the correctness argument for appying
metatheoretic simplifiers requires that one be able to "grow" an
evaluator (see DEFEVALUATOR) to handle all functions in the
current ACL2 world.  Then we may, in essence, functionally instantiate
the original evaluator to the new ("grown") evaluator, provided that
the new evaluator satisfies all of the axioms of the original.  We
therefore require that the evaluator function does not support the
formula of any defaxiom event.  This notion of "support" (sometimes
denoted "is an ancestor of") is defined recursively as follows: a
function symbol supports a formula if either it occurs in that formula,
or else it supports the definition or constraint for some function
symbol that occurs in that formula.  Moreover, we require that neither
the evaluator function nor its list version support the definition or
constraint for any other function symbol occurring in the proposed :meta
theorem.

We also require that the evaluator does not support the formula of a
:meta rule's metafunction (nor, if there is one, hypothesis
metafunction) or of a :clause-processor rule's clause-processor
function.  This requirement, together with the analogous requirement
for defaxiom events stated above, are necessary in order to carry out
the functional instantiation argument alluded to above, as follows
(where the reader may find it useful to have some familiarity with the
paper "Structured Theory Development for a Mechanized Logic" (Journal
of Automated Reasoning 26, no. 2 (2001), pages 161-203).  By the usual
conservativity argument, we know that the rule follows logically from
the axiomatic events for its supporters.  This remains true if we
functionally instantiate the evaluator with one corresponding to all
the functions symbols of the current session, since none of the
definitions of supporters of defaxioms or metafunctions are hit by that
functional substitution.

Notice though that the argument above depends on knowing that the rule
is not itself an axiom about the evaluator!  Therefore, we also
restrict evaluators so that they are not defined in the scope of a
superior encapsulate event with non-empty signature, in order to avoid
an even more subtle problem.  The aforementioned correctness argument
depends on knowing that the rule is provable from the axioms on the
evaluator and metafunction (and hypothesis metafunction, if any).  The
additional restriction avoids unsoundness!  The following events, if
allowed, produce a proof that (f x) equals t even though, as shown
below, that does not follow logically from the axioms introduced.

     ; Introduce our metafunction.
     (defun my-cancel (term)
       (case-match term
         (('f ('g))
          *t*)
         (& term)))

     ; Introduce our evaluator and prove our meta rule, but in the same
     ; encapsulate!
     (encapsulate
      ((f (x) t))

      (local (defun f (x) (declare (ignore x)) t))

      (defevaluator evl evl-list
        ((f x)))

      (defthm correctness-of-my-cancel
        (equal (evl x a)
               (evl (my-cancel x) a))
        :rule-classes ((:meta :trigger-fns (f)))))

     ; Prove that (f x) = t.
     (encapsulate
      ()

      (local (defstub c () t))

      (local (encapsulate
              ()
              (local (defun g () (c)))
              (local (in-theory (disable g (g))))
              (local (defthm f-g
                       (equal (f (g)) t)
                       :rule-classes nil))
              (defthm f-c
                (equal (f (c)) t)
                :hints (("Goal" :use f-g
                         :in-theory (e/d (g) (correctness-of-my-cancel))))
                :rule-classes nil)))

      (defthm f-t
        (equal (f x) t)
        :hints (("Goal" :by (:functional-instance
                             f-c
                             (c (lambda () x)))))
        :rule-classes nil))

To see that the term (equal (f x) t) does not follow logically from the
axiomatic events above, consider following the above definition of
my-cancel with the following events instead.

     ; (defun my-cancel (term) ...) as before, then:

     (defun f (x)
       (not x))

     (defun g ()
       nil)

     (defevaluator evl evl-list
        ((f x) (g)))

These events imply the axiomatic events above, because we still have the
definition of my-cancel, we have a stronger defevaluator event, and we
can now prove correctness-of-my-cancel exactly as it is stated above.
So, the rule f-t is a logical consequence of the chronology of the
current session.  However, in the current session we can also prove the
following rule, which contradicts f-t.

     (defthm f-not-t
       (equal (f t) nil)
       :rule-classes nil)

It follows that the current session logically yields a contradiction!

Erik Reeber has taken the above example and modified it to prove nil in
ACL2 Version_3.1, as follows.

     (in-package "ACL2")

     (defun my-cancel (term)
        (case-match term
          (('f ('g))
           *t*)
          (('f2 ('g2))
           *t*)
          (& term)))

     (defun f2 (x)
        (not x))

     (defun g2 ()
        nil)

     (encapsulate
       ((f (x) t))

       (local (defun f (x) (declare (ignore x)) t))

       (defevaluator evl evl-list
         ((f x)
          (f2 x)
          (g2)))

       (defthm correctness-of-my-cancel
         (equal (evl x a)
                (evl (my-cancel x) a))
         :rule-classes ((:meta :trigger-fns (f)))))

     (encapsulate
       ()

       (local (defstub c () t))

       (local (encapsulate
               ()
               (local (defun g () (c)))
               (local (in-theory (disable g (g))))
               (local (defthm f-g
                        (equal (f (g)) t)
                        :rule-classes nil))
               (defthm f-c
                 (equal (f (c)) t)
                 :hints (("Goal" :use f-g
                          :in-theory (e/d (g) (correctness-of-my-cancel))))
                 :rule-classes nil)))

       (defthm f-t
         (equal (f x) t)
         :hints (("Goal" :by (:functional-instance
                              f-c
                              (c (lambda () x)))))
         :rule-classes nil))

     (defun g ()
        nil)

     ; Below is the expansion of the following defevaluator, changed slightly as
     ; indicated by comments.
     ; (defevaluator evl2 evl2-list ((f x) (f2 x) (g) (g2)))

     (ENCAPSULATE
       (((EVL2 * *) => *)
        ((EVL2-LIST * *) => *))
       (SET-INHIBIT-WARNINGS "theory")
       (LOCAL (IN-THEORY *DEFEVALUATOR-FORM-BASE-THEORY*))
       (LOCAL
        (MUTUAL-RECURSION (DEFUN EVL2 (X A)
                            (DECLARE (XARGS :VERIFY-GUARDS NIL
                                            :MEASURE (ACL2-COUNT X)
                                            :WELL-FOUNDED-RELATION O<
                                            :MODE :LOGIC))
                            (COND ((SYMBOLP X) (CDR (ASSOC-EQ X A)))
                                  ((ATOM X) NIL)
                                  ((EQ (CAR X) 'QUOTE) (CAR (CDR X)))
                                  ((CONSP (CAR X))
                                   (EVL2 (CAR (CDR (CDR (CAR X))))
                                         (PAIRLIS$ (CAR (CDR (CAR X)))
                                                   (EVL2-LIST (CDR X) A))))
                                  ((EQUAL (CAR X) 'F) ; changed f to f2 just below
                                   (F2 (EVL2 (CAR (CDR X)) A)))
                                  ((EQUAL (CAR X) 'F2)
                                   (F2 (EVL2 (CAR (CDR X)) A)))
                                  ((EQUAL (CAR X) 'G) (G))
                                  ((EQUAL (CAR X) 'G2) (G2))
                                  (T NIL)))
                          (DEFUN EVL2-LIST (X-LST A)
                            (DECLARE (XARGS :MEASURE (ACL2-COUNT X-LST)
                                            :WELL-FOUNDED-RELATION O<))
                            (COND ((ENDP X-LST) NIL)
                                  (T (CONS (EVL2 (CAR X-LST) A)
                                           (EVL2-LIST (CDR X-LST) A)))))))

       (DEFTHM EVL2-CONSTRAINT-1
         (IMPLIES (SYMBOLP X)
                  (EQUAL (EVL2 X A)
                         (CDR (ASSOC-EQ X A)))))
       (DEFTHM EVL2-CONSTRAINT-2
         (IMPLIES (AND (CONSP X) (EQUAL (CAR X) 'QUOTE))
                  (EQUAL (EVL2 X A) (CADR X))))
       (DEFTHM EVL2-CONSTRAINT-3
         (IMPLIES (AND (CONSP X) (CONSP (CAR X)))
                  (EQUAL (EVL2 X A)
                         (EVL2 (CADDAR X)
                               (PAIRLIS$ (CADAR X)
                                         (EVL2-LIST (CDR X) A))))))
       (DEFTHM EVL2-CONSTRAINT-4
         (IMPLIES (NOT (CONSP X-LST))
                  (EQUAL (EVL2-LIST X-LST A) NIL)))
       (DEFTHM EVL2-CONSTRAINT-5
         (IMPLIES (CONSP X-LST)
                  (EQUAL (EVL2-LIST X-LST A)
                         (CONS (EVL2 (CAR X-LST) A)
                               (EVL2-LIST (CDR X-LST) A)))))
       (DEFTHM EVL2-CONSTRAINT-6
         (IMPLIES (AND (CONSP X) (EQUAL (CAR X) 'F))
                  (EQUAL (EVL2 X A) ; changed f to f2 just below
                         (F2 (EVL2 (CADR X) A)))))
       (DEFTHM EVL2-CONSTRAINT-7
         (IMPLIES (AND (CONSP X) (EQUAL (CAR X) 'F2))
                  (EQUAL (EVL2 X A)
                         (F2 (EVL2 (CADR X) A)))))
       (DEFTHM EVL2-CONSTRAINT-8
         (IMPLIES (AND (CONSP X) (EQUAL (CAR X) 'G))
                  (EQUAL (EVL2 X A) (G))))
       (DEFTHM EVL2-CONSTRAINT-9
         (IMPLIES (AND (CONSP X) (EQUAL (CAR X) 'G2))
                  (EQUAL (EVL2 X A) (G2)))))

     (defthm f2-t
        (equal (f2 x) t)
        :hints (("Goal" :by (:functional-instance
                             f-t
                             (f f2)
                             (evl evl2)
                             (evl-list evl2-list)))))

     (defthm bug-implies-nil
        nil
        :hints (("Goal" :use ((:instance f2-t (x t)))))
        :rule-classes nil)

REFINEMENT    record that one equivalence relation refines another

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

     Example:
     (implies (bag-equal x y) (set-equal y x)).

Also see DEFREFINEMENT.

     General Form:
     (implies (equiv1 x y) (equiv2 x y))

Equiv1 and equiv2 must be known equivalence relations.  The effect of
such a rule is to record that equiv1 is a refinement of equiv2.  This
means that equiv1 :rewrite rules may be used while trying to maintain
equiv2.  See EQUIVALENCE for a general discussion of the issues.

The macro form (defrefinement equiv1 equiv2) is an abbreviation for a
defthm of rule-class :refinement that establishes that equiv1 is a
refinement of equiv2.  See DEFREFINEMENT.

Suppose we have the :rewrite rule

     (bag-equal (append a b) (append b a))

which states that append is commutative modulo bag-equality.  Suppose
further we have established that bag-equality refines set-equality.
Then when we are simplifying append expressions while maintaining
set-equality we use append's commutativity property, even though it was
proved for bag-equality.

Equality is known to be a refinement of all equivalence relations.  The
transitive closure of the refinement relation is maintained, so if
set-equality, say, is shown to be a refinement of some third sense of
equivalence, then bag-equality will automatially be known as a
refinement of that third equivalence.

:refinement lemmas cannot be disabled.  That is, once one equivalence
relation has been shown to be a refinement of another, there is no way
to prevent the system from using that information.  Of course,
individual :rewrite rules can be disabled.

More will be written about this as we develop the techniques.

REWRITE    make some :rewrite rules (possibly conditional ones)

See RULE-CLASSES for a general discussion of rule classes and
how they are used to build rules from formulas.  Example :corollary
formulas from which :rewrite rules might be built are:

     Example:
     (equal (+ x y) (+ y x))            replace (+ a b) by (+ b a) provided
                                        certain heuristics approve the
                                        permutation.

     (implies (true-listp x)            replace (append a nil) by a, if
              (equal (append x nil) x)) (true-listp a) rewrites to t

     (implies                           replace (member a (append b c)) by
         (and (eqlablep e)              (member a (append c b)) in contexts
              (true-listp x)            in which propositional equivalence
              (true-listp y))           is sufficient, provided (eqlablep a)
         (iff (member e (append x y))   (true-listp b) and (true-listp c)
              (member e (append y x)))) rewrite to t and the permutative
                                        heuristics approve

     * Menu:

     Related topics other than immediate subtopics:
     * BIND-FREE:: to bind free variables of a rewrite or linear rule

     * CASE-SPLIT:: like force but immediately splits the top-level goal on the hypothesis

     * FORCE:: identity function used to force a hypothesis

     * FREE-VARIABLES:: free variables in rules

     * SYNTAXP:: attach a heuristic filter on a :rewrite, :meta, or :linear rule

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

Note: One :rewrite rule class object might create many rewrite rules
from the :corollary formula.  To create the rules, we first translate
the formula (expanding all macros; also see TRANS).  Next, we
eliminate all lambdas; one may think of this step as simply
substituting away every let, let*, and mv-let in the formula.  We then
flatten the and and implies structure of the formula, transforming it
into a conjunction of formulas, each of the form

     (implies (and h1 ... hn) concl)

where no hypothesis is a conjunction and concl is neither a conjunction
nor an implication.  If necessary, the hypothesis of such a conjunct
may be vacuous.  We then further coerce each concl into the form (equiv
lhs rhs), where equiv is a known equivalence relation, by replacing any
concl not of that form by (iff concl t).  A concl of the form (not
term) is considered to be of the form (iff term nil).  By these steps
we reduce the given :corollary to a sequence of conjuncts, each of
which is of the form

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

where equiv is a known equivalence relation.  See EQUIVALENCE
for a general discussion of the introduction of new equivalence
relations.

We create a :rewrite rule for each such conjunct, if possible, and
otherwise cause an error.  It is possible to create a rewrite rule from
such a conjunct provided lhs is not a variable, a quoted constant, a
let-expression, a lambda application, or an if-expression.

A :rewrite rule is used when any instance of the lhs occurs in a
context in which the equivalence relation is operative.  First, we find
a substitution that makes lhs equal to the target term.  Then we attempt
to relieve the instantiated hypotheses of the rule.  Hypotheses that are
fully instantiated are relieved by recursive rewriting.  Hypotheses that
contain "free variables" (variables not assigned by the unifying
substitution) are relieved by attempting to guess a suitable instance
so as to make the hypothesis equal to some known assumption in the
context of the target.  If the hypotheses are relieved, and certain
restrictions that prevent some forms of infinite regress are met (see
LOOP-STOPPER), the target is replaced by the instantiated rhs,
which is then recursively rewritten.

ACL2's rewriting process has undergone some optimization.  In
particular, when a term t1 is rewritten to a new term t2, the rewriter
is then immediately applied to t2.  On rare occasions you may find that
you do not want this behavior, in which case you may wish to use a
trick involving hide; see META, near the end of that
documentation.

At the moment, the best description of how ACL2 :rewrite rules are used
is perhaps in the discussion of "Replacement Rules" on page 279 of A
Computational Logic Handbook (second edition).

TYPE-PRESCRIPTION    make a rule that specifies the type of a term

See RULE-CLASSES for a general discussion of rule classes and
how they are used to build rules from formulas.  Some example :corollary
formulas from which :type-prescription rules might be built are:

     Examples:
     (implies                           (nth n lst) is of type characterp
      (and (character-listp lst)        provided the two hypotheses can
           (< n (length lst)))          be established by type reasoning
      (characterp (nth n lst))).

     (implies                           (demodulize a lst 'value ans) is
      (and (atom a)                     either a nonnegative integer or
           (true-listp lst)             of the same type as ans, provided
           (member-equal a lst))        the hyps can be established by type
      (or (and                          reasoning
            (integerp
             (demodulize a lst 'value ans))
            (>= (demodulize a lst 'value ans) 0))
          (equal (demodulize a lst 'value ans) ans))).

To specify the term whose type (see TYPE-SET) is described by
the rule, provide that term as the value of the :typed-term field of
the rule class object.

     General Form:
     (implies hyps
              (or type-restriction1-on-pat
                  ...
                  type-restrictionk-on-pat
                  (equal pat var1)
                  ...
                  (equal pat varj)))

where pat is the application of some function symbol to some arguments,
each type-restrictioni-on-pat is a term involving pat and containing no
variables outside of the occurrences of pat, and each vari is one of
the variables of pat.  Generally speaking, the type-restriction terms
ought to be terms that inform us as to the type of pat.  Ideally, they
should be "primitive recognizing expressions" about pat; see
COMPOUND-RECOGNIZER.

If the :typed-term is not provided in the rule class object, it is
computed heuristically by looking for a term in the conclusion whose
type is being restricted.  An error is caused if no such term is found.

Roughly speaking, the effect of adding such a rule is to inform the ACL2
typing mechanism that pat has the type described by the conclusion, when
the hypotheses are true.  In particular, the type of pat is within the
union of the types described by the several disjuncts.  The "type
described by" (equal pat vari) is the type of vari.

More operationally, when asked to determine the type of a term that is
an instance of pat, ACL2 will first attempt to establish the hypotheses.
*This is done by type reasoning alone, not rewriting!*  However, if some
hypothesis is a call of force, then forcing may occur, which may
ultimately invoke the rewriter; see FORCE and see
CASE-SPLIT.  So-called free variables in hypotheses are treated
specially; see FREE-VARIABLES.  Provided the hypotheses are
established by type reasoning, ACL2 then unions the types described by
the type-restrictioni-on-pat terms together with the types of those
subexpressions of pat identified by the vari.  The final type computed
for a term is the intersection of the types implied by each applicable
rule.  Type prescription rules may be disabled.

Because only type reasoning is used to establish the hypotheses of
:type-prescription rules, some care must be taken with the hypotheses.
Suppose, for example, that the non-recursive function my-statep is
defined as

       (defun my-statep (x)
         (and (true-listp x)
              (equal (length x) 2)))

and suppose (my-statep s) occurs as a hypothesis of a
:type-prescription rule that is being considered for use in the proof
attempt for a conjecture with the hypothesis (my-statep s).  Since the
hypothesis in the conjecture is rewritten, it will become the
conjunction of (true-listp s) and (equal (length s) 2).  Those two
terms will be assumed to have type t in the context in which the
:type-prescription rule is tried.  But type reasoning will be unable to
deduce that (my-statep s) has type t in this context.  Thus, either
my-statep should be disabled (see DISABLE) during the proof
attempt or else the occurrence of (my-statep s) in the
:type-prescription rule should be replaced by the conjunction into
which it rewrites.

While this example makes it clear how non-recursive predicates can cause
problems, non-recursive functions in general can cause problems.  For
example, if (mitigate x) is defined to be (if (rationalp x) (1- x) x)
then the hypothesis (pred (mitigate s)) in the conjecture will rewrite,
opening mitigate and splitting the conjecture into two subgoals, one in
which (rationalp s) and (pred (1- x)) are assumed and the other in
which (not (rationalp s)) and (pred x) are assumed.  But (pred
(mitigate s)) will not be typed as t in either of these contexts.  The
moral is: beware of non-recursive functions occuring in the hypotheses
of :type-prescription rules.

Because of the freedom one has in forming the conclusion of a
type-prescription, we have to use heuristics to recover the pattern,
pat, whose type is being specified.  In some cases our heuristics may
not identify the intended term and the :type-prescription rule will be
rejected as illegal because the conclusion is not of the correct form.
When this happens you may wish to specify the pat directly.  This may
be done by using a suitable rule class token.  In particular, when the
token :type-prescription is used it means ACL2 is to compute pat with
its heuristics; otherwise the token should be of the form
(:type-prescription :typed-term pat), where pat is the term whose type
is being specified.

The defun event may generate a :type-prescription rule.  Suppose fn is
the name of the function concerned.  Then (:type-prescription fn) is
the rune given to the type-prescription, if any, generated for fn by
defun.  (The trivial rule, saying fn has unknown type, is not stored,
but defun still allocates the rune and the corollary of this rune is
known to be t.)

TYPE-SET-INVERTER    exhibit a new decoding for an ACL2 type-set

See RULE-CLASSES for a general discussion of rule classes and
how they are used to build rules from formulas.

     Example Rule Class:
     (:type-set-inverter
       :corollary (equal (and (counting-number x) (not (equal x 0)))
                         (and (integerp x) (< x 0)))
       :type-set 2)

     General Forms of Rule Class:
     :type-set-inverter, or
     (:type-set-inverter :type-set n)

     General Form of Theorem or Corollary:
     (EQUAL new-expr old-expr)

where n is a type-set (see TYPE-SET) and old-expr is the term
containing x as a free variable that ACL2 currently uses to recognize
type-set n.  For a given n, the exact form of old-expr is generated by

     (convert-type-set-to-term 'x n (ens state) (w state) nil)].

If the :type-set field of the rule-class is omitted, we attempt to
compute it from the right-hand side, old-expr, of the corollary.  That
computation is done by type-set-implied-by-term (see TYPE-SET).
However, it is possible that the type-set we compute from lhs does not
have the required property that when inverted with
convert-type-set-to-term the result is lhs.  If you omit :type-set and
an error is caused because lhs has the incorrect form, you should
manually specify both :type-set and the lhs generated by
convert-type-set-to-term.

The rule generated will henceforth make new-expr be the term used by
ACL2 to recognize type-set n.  If this rule is created by a defthm
event named name then the rune of the rule is (:type-set-inverter name)
and by disabling that rune you can prevent its being used to decode
type-sets.

Type-sets are inverted when forced assumptions are turned into formulas
to be proved.  In their internal form, assumptions are essentially
pairs consisting of a context and a goal term, which was forced.
Abstractly a context is just a list of hypotheses which may be assumed
while proving the goal term.  But actually contexts are alists which
pair terms with type-sets, encoding the current hypotheses.  For
example, if the original conjecture contained the hypothesis (integerp
x) then the context used while working on that conjecture will include
the assignment to x of the type-set *ts-integer*.

WELL-FOUNDED-RELATION    show that a relation is well-founded on a set

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 :well-founded-relation rule might be built is as
follows.  (Of course, the functions pairp, lex2p, and ordinate would
have to be defined first.)

     Example:
     (and (implies (pairp x) (o-p (ordinate x)))
          (implies (and (pairp x)
                        (pairp y)
                        (lex2p x y))
                   (o< (ordinate x) (ordinate y))))

The above example establishes that lex2p is a well-founded relation on
pairps.  We explain and give details below.

Exactly two general forms are recognized:

     General Forms
     (AND (IMPLIES (mp x) (O-P (fn x)))              ; Property 1
          (IMPLIES (AND (mp x)                       ; Property 2
                        (mp y)
                        (rel x y))
                   (O< (fn x) (fn y)))),

or

     (AND (O-P (fn x))                               ; Property 1
          (IMPLIES (rel x y)                         ; Property 2
                   (O< (fn x) (fn y))))

where mp, fn, and rel are function symbols, x and y are distinct
variable symbols, and no other :well-founded-relation theorem about fn
has been proved.  When the second general form is used, we act as
though the first form were used with mp being the function that ignores
its argument and returns t.  The discussion below therefore considers
only the first general form.

Note: We are very rigid when checking that the submitted formula is of
one of these forms.  For example, in the first form, we insist that all
the conjuncts appear in the order shown above.  Thus, interchanging the
two properties in the top-level conjunct or rearranging the hyptheses
in the second conjunct both produce unrecognized forms.  The
requirement that each fn be proved well-founded at most once ensures
that for each well-founded relation, fn, there is a unique mp that
recognizes the domain on which rel is well-founded.  We impose this
requirement simply so that rel can be used as a short-hand when
specifying the well-founded relations to be used in definitions;
otherwise the specification would have to indicate which mp was to be
used.

Mp is a predicate that recognizes the objects that are supposedly
ordered in a well-founded way by rel.  We call such an object an
"mp-measure" or simply a "measure" when mp is understood.  Property 1
tells us that every measure can be mapped into an ACL2 ordinal.  (See
O-P.)  This mapping is performed by fn.  Property 2 tells us
that if the measure x is smaller than the measure y according to rel
then the image of x under fn is a smaller than that of y, according to
the well-founded relation o<.  (See O<.)  Thus, the general
form of a :well-founded-relation formula establishes that there exists a
rel-order preserving embedding (namely via fn) of the mp-measures into
the ordinals.  We can thus conclude that rel is well-founded on
mp-measures.

Such well-founded relations are used in the admissibility test for
recursive functions, in particular, to show that the recursion
terminates.  To illustrate how such information may be used, consider a
generic function definition

     (defun g (x) (if (test x) (g (step x)) (base x))).

If rel has been shown to be well-founded on mp-measures, then g's
termination can be ensured by finding a measure, (m x), with the
property that m produces a measure:

     (mp (m x)),                                     ; Defun-goal-1

and that the argument to g gets smaller (when measured by m and
compared by rel) in the recursion,

     (implies (test x) (rel (m (step x)) (m x))).    ; Defun-goal-2

If rel is selected as the :well-founded-relation to be used in the
definition of g, the definitional principal will generate and attempt
to prove defun-goal-1 and defun-goal-2 to justify g.  We show later why
these two goals are sufficient to establish the termination of g.
Observe that neither the ordinals nor the embedding, fn, of the
mp-measures into the ordinals is involved in the goals generated by the
definitional principal.

Suppose now that a :well-founded-relation theorem has been proved for
mp and rel.  How can rel be "selected as the :well-founded-relation" by
defun?  There are two ways.  First, an xargs keyword to the defun event
allows the specification of a :well-founded-relation.  Thus, the
definition of g above might be written

     (defun g (x)
      (declare (xargs :well-founded-relation (mp . rel)))
      (if (test x) (g (step x)) (base x)))

Alternatively, rel may be specified as the
:default-well-founded-relation in acl2-defaults-table by executing the
event

     (set-well-founded-relation rel).

When a defun event does not explicitly specify the relation in its
xargs the default relation is used.  When ACL2 is initialized, the
default relation is o<.

Finally, though it is probably obvious, we now show that defun-goal-1
and defun-goal-2 are sufficient to ensure the termination of g provided
property-1 and property-2 of mp and rel have been proved.  To this end,
assume we have proved defun-goal-1 and defun-goal-2 as well as
property-1 and property-2 and we show how to admit g under the
primitive ACL2 definitional principal (i.e., using only the ordinals).
In particular, consider the definition event

     (defun g (x)
      (declare (xargs :well-founded-relation o<
                      :measure (fn (m x))))
      (if (test x) (g (step x)) (base x)))

Proof that g is admissible:  To admit the definition of g above we must
prove

     (o-p (fn (m x)))                        ; *1

and

     (implies (test x)                               ; *2
              (o< (fn (m (step x))) (fn (m x)))).

But *1 can be proved by instantiating property-1 to get

     (implies (mp (m x)) (o-p (fn (m x)))),

and then relieving the hypothesis with defun-goal-1, (mp (m x)).

Similarly, *2 can be proved by instantiating property-2 to get

     (implies (and (mp (m (step x)))
                   (mp (m x))
                   (rel (m (step x)) (m x)))
              (o< (fn (m (step x))) (fn (m x))))

and relieving the first two hypotheses by appealing to two instances of
defun-goal-1, thus obtaining

     (implies (rel (m (step x)) (m x))
              (o< (fn (m (step x))) (fn (m x)))).

By chaining this together with defun-goal-2,

     (implies (test x)
              (rel (m (step x)) (m x)))

we obtain *2.  Q.E.D.

STOBJ    single-threaded objects or "von Neumann bottlenecks"

In ACL2, a "single-threaded object" is a data structure whose use is so
syntactically restricted that only one instance of the object need ever
exist and its fields can be updated by destructive assignments.

Note: Novices are advised to avoid using single-threaded objects,
perhaps instead using distributed book
books/data-structures/structures.lisp.  At the least, consider using
(set-verify-guards-eagerness 0) to avoid guard verification.

The documentation in this section is laid out in the form of a tour that
visits the documented topics in a reasonable order.  We recommend that
you follow the tour the first time you read about stobjs.  The list of
all stobj topics is shown below.  The tour starts immediately
afterwards.  Also see DEFSTOBJ.

Related topics other than immediate subtopics:

As noted, a "single-threaded object" is a data structure whose use is so
syntactically restricted that only one instance of the object need ever
exist.  Updates to the object must be sequentialized.  This allows us to
update its fields with destructive assignments without wrecking the
axiomatic semantics of update-by-copy.  For this reason,
single-threaded objects are sometimes called "von Neumann bottlenecks."

From the logical perspective, a single-threaded object is an ordinary
ACL2 object, e.g., composed of integers and conses.  Logically
speaking, ordinary ACL2 functions are defined to allow the user to
"access" and "update" its fields.  Logically speaking, when fields in
the object, obj, are "updated" with new values, a new object, obj', is
constructed.

But suppose that by syntactic means we could ensure that there were no
more references to the "old" object, obj.  Then we could create obj' by
destructively modifying the memory locations involved in the
representation of obj.  The syntactic means is pretty simple but
draconian: the only reference to obj is in the variable named OBJ.

The consequences of this simple rule are far-reaching and require some
getting used to.  For example, if OBJ has been declared as a
single-threaded object name, then:

obj.

expression" that can be passed into that slot is the variable OBJ, not
merely a term that "evaluates to an obj"; thus, such functions can only
 operate on the current object.  So for example, instead of   (FOO
(UPDATE-FIELD1 3 ST)) write   (LET ((ST (UPDATE-FIELD1 3 ST))) (FOO
ST)).

those functions can only be applied to the current object.

to the variable OBJ.  Thus, for example, obj may not be consed   into a
list (which would create another pointer to it) or accessed or   copied
via "unapproved" means.

updater is called, the only variable which can hold its result is   OBJ.

(either as the sole value returned, or in (mv ... OBJ ...); see
MV).

that object becomes the new current value of OBJ.

What makes ACL2 different from other functional languages supporting
such operations (e.g., Haskell's "monads" and Clean's "uniqueness type
system") is that ACL2 also gives single-threaded objects an explicit
axiomatic semantics so that theorems can be proved about them.  In
particular, the syntactic restrictions noted above are enforced only
when single-threaded objects are used in function definitions (which
might be executed outside of the ACL2 read-eval-print loop in Common
Lisp).  The accessor and update functions for single-threaded objects
may be used without restriction in formulas to be proved.  Since
function evaluation is sometimes necessary during proofs, ACL2 must be
able to evaluate these functions on logical constants representing the
object, even when the constant is not "the current object."  Thus, ACL2
supports both the efficient von Neumann semantics and the clean
applicative semantics, and uses the first in contexts where execution
speed is paramount and the second during proofs.

To start the stobj tour, see STOBJ-EXAMPLE-1.

DECLARE-STOBJS    declaring a formal parameter name to be a single-threaded object

When a defun uses one of its formals as a single-threaded object
(stobj), the defun _must_ include a declaration that the formal is to
be so used.  An exception is the formal "state," which if not declared
as explained below, may still be used provided an appropriate global
"declaration" is issued: see SET-STATE-OK.

If the formal in question is counters then an appropriate declaration is

     (declare (xargs :stobjs counters))

or, more generally,

     (declare (xargs :stobjs (... counters ...)))

where all the single-threaded formals are listed.

For such a declaration to be legal it must be the case that all the
names have previously been defined as single-threaded objects with
defstobj.

When an argument is declared to be single-threaded the guard of the
function is augmented by conjoining to it the condition that the
argument satisfy the recognizer for the single-threaded object.
Furthermore, the syntactic checks done to enforce the legal use of
single-threaded objects are also sufficient to allow these guard
conjuncts to be automatically proved.

The obvious question arises:  Why does ACL2 insist that you declare
stobj names before using them in defuns if you can only declare names
that have already been defined with defstobj?  What would go wrong if a
formal were treated as a single-threaded object if and only if it had
already been so defined?

Suppose that one user, say Jones, creates a book in which counters is
defined as a single-threaded object.  Suppose another user, Smith,
creates a book in which counters is used as an ordinary formal
parameter.  Finally, suppose a third user, Brown, wishes to use both
books.  If Brown includes Jones' book first and then Smith's, then
Smith's function treats counters as single-threaded.  But if Brown
includes Smith's book first, the argument is treated as ordinary.

ACL2 insists on the declaration to ensure that the definition is
processed the same way no matter what the context.

RESIZE-LIST    list resizer in support of stobjs

(Resize-list lst n default-value) takes a list, lst, and a desired
length, n, for the result list, as well as a default-value to use for
the extra elements if n is greater than the length of lst.

Resize-list has a guard of t.  This function is called in the body of
function, resize-<a> where <a> is an array field of a stobj.  See
STOBJ and see DEFSTOBJ.

STOBJ-EXAMPLE-1    an example of the use of single-threaded objects

Suppose we want to sweep a tree and (1) count the number of interior
nodes, (2) count the number of tips and (3) keep a record of every tip
we encounter that is an integer.  We could use a single-threaded object
as our "accumulator".  Such an object would have three fields, one
holding the number of nodes seen so far, one holding the number of
tips, and one holding all the integer tips seen.

The following event declares counters to be a single-threaded object.

     (defstobj counters
       (NodeCnt     :type integer :initially 0)
       (TipCnt      :type integer :initially 0)
       (IntTipsSeen :type t       :initially nil))

It has three fields, NodeCnt, TipCnt, and IntTipsSeen.  (As always in
ACL2, capitalization is irrelevant in simple symbol names, so the first
name could be written nodecnt or NODECNT, etc.) Those are the name of
the accessor functions for the object.  The corresponding update
functions are named update-NodeCnt, update-TipCnt and
update-IntTipsSeen.

If you do not like the default function names chosen above, there is a
feature in the defstobj event that allows you to specify other names.

If you want to see the ACL2 definitions of all the functions defined by
this event, look at stobj-example-1-defuns.

If, after this event, we evaluate the top-level "global variable"
counters in the ACL2 read-eval-print loop we get:

     ACL2 !>counters
     <counters>

Note that the value printed is "<counters>".  Actually, the value of
counters in the logic is (0 0 NIL).  But ACL2 always prints
single-threaded objects in this non-informative way because they are
usually so big that to do otherwise would be unpleasant.

Had you tried to evaluate the "global variable" counters before
declaring it a single-threaded object, ACL2 would have complained that
it does not support global variables.  So a lesson here is that once
you have declared a new single-threaded object your top-level forms can
reference it.  In versions of ACL2 prior to Version  2.4 the only
variable enjoying this status was STATE.  single-threaded objects are a
straightforward generalization of the long-implemented von Neumann
state feature of ACL2.

We can access the fields of counters as with:

     ACL2 !>(NodeCnt counters)
     0
     ACL2 !>(IntTipsSeen counters)
     NIL

and we can set the fields of counters as with:

     ACL2 !>(update-NodeCnt 3 counters)
     <counters>
     ACL2 !>(NodeCnt counters)
     3

Observe that when we evaluate an expression that returns a counter
object, that object becomes the "current value" of counters.

Here is a function that "converts" the counters object to its
"ordinary" representation:

     (defun show-counters (counters)
       (declare (xargs :stobjs (counters)))
       (list (NodeCnt counters)
             (TipCnt counters)
             (IntTipsSeen counters)))

Observe that we _must_ declare, at the top of the defun, that we mean
to use the formal parameter counters as a single-threaded object!  If
we did not make this declaration, the body of show-counters would be
processed as though counters were an ordinary object.  An error would
be caused because the accessors used above cannot be applied to
anything but the single-threaded object counters.  If you want to know
why we insist on this declaration, see DECLARE-STOBJS.

When show-counters is admitted, the following message is printed:

     Since SHOW-COUNTERS is non-recursive, its admission is trivial.  We
     observe that the type of SHOW-COUNTERS is described by the theorem
     (AND (CONSP (SHOW-COUNTERS COUNTERS))
          (TRUE-LISTP (SHOW-COUNTERS COUNTERS))).
     We used primitive type reasoning.

     (SHOW-COUNTERS COUNTERS) => *.

     The guard conjecture for SHOW-COUNTERS is trivial to prove.
     SHOW-COUNTERS is compliant with Common Lisp.

The line above containing the "=>" is called the "signature" of
show-counters; it conveys the information that the first argument is
the single-threaded object counters and the only result is an ordinary
object.  Here is an example of another signature:

     (PROCESSOR * * COUNTERS) => (MV * COUNTERS)

which indicates that the function PROCESSOR (which we haven't shown
you) takes three arguments, the third of which is the COUNTERS stobj,
and returns two results, the second of which is the modified COUNTERS.

Returning to the admission of show-counters above, the last sentence
printed indicates that the guard conjectures for the function were
proved.  When some argument of a function is declared to be a
single-threaded object via the xargs :stobj, we automatically add
(conjoin) to the guard the condition that the argument satisfy the
recognizer for that single-threaded object.  In the case of
show-counters the guard is (countersp counters).

Here is an example of show-counters being called:

     ACL2 !>(show-counters counters)
     (3 0 NIL)

This is what we would see had we set the NodeCnt field of the initial
value of counters to 3, as we did earlier in this example.

We next wish to define a function to reset the counters object.  We
could define it this way:

     (defun reset-counters (counters)
       (declare (xargs :stobjs (counters)))
       (let ((counters (update-NodeCnt 0 counters)))
         (let ((counters (update-TipCnt 0 counters)))
           (update-IntTipsSeen nil counters))))

which "successively" sets the NodeCnt field to 0, then the TipCnt field
to 0, and then the IntTipsSeen field to nil and returns the resulting
object.

However, the nest of let expressions is tedious and we use this
definition instead.  This definition exploits a macro, here named "seq"
(for "sequentially") which evaluates each of the forms given, binding
their results successively to the stobj name given.

     (defun reset-counters (counters)
       (declare (xargs :stobjs (counters)))
       (seq counters
            (update-NodeCnt 0 counters)
            (update-TipCnt 0 counters)
            (update-IntTipsSeen nil counters)))

This definition is syntactically identical to the one above, after macro
expansion.  Our definition of seq is shown below and is not part of
native ACL2.

     (defmacro seq (stobj &rest rst)
       (cond ((endp rst) stobj)
             ((endp (cdr rst)) (car rst))
             (t `(let ((,stobj ,(car rst)))
                  (seq ,stobj ,@(cdr rst))))))

The signature printed for reset-counters is

     (RESET-COUNTERS COUNTERS) => COUNTERS.

Here is an example.

     ACL2 !>(show-counters counters)
     (3 0 NIL)
     ACL2 !>(reset-counters counters)
     <counters>
     ACL2 !>(show-counters counters)
     (0 0 NIL)

Here finally is a function that uses counters as a single-threaded
accumulator to collect the desired information about the tree x.

     (defun sweep-tree (x counters)
       (declare (xargs :stobjs (counters)))
       (cond ((atom x)
              (seq counters
                   (update-TipCnt (+ 1 (TipCnt counters)) counters)
                   (if (integerp x)
                       (update-IntTipsSeen (cons x (IntTipsSeen counters))
                                       counters)
                     counters)))
             (t (seq counters
                     (update-NodeCnt (+ 1 (NodeCnt counters)) counters)
                     (sweep-tree (car x) counters)
                     (sweep-tree (cdr x) counters)))))

We can paraphrase this definition as follows.  If x is an atom, then
increment the TipCnt field of counters and _then_, if x is an integer,
add x to the IntTipsSeen field, and return counters.  On the other
hand, if x is not an atom, then increment the NodeCnt field of
counters, and _then_ sweep the car of x and _then_ sweep the cdr of x
and return the result.

Here is an example of its execution.  We have displayed the input tree
in full dot notation so that the number of interior nodes is just the
number of dots.

     ACL2 !>(sweep-tree '((((a . 1) . (2 . b)) . 3)
                          . (4 . (5 . d)))
                        counters)
     <counters>
     ACL2 !>(show-counters counters)
     (7 8 (5 4 3 2 1))
     ACL2 !>(reset-counters counters)
     <counters>
     ACL2 !>(show-counters counters)
     (0 0 NIL)

The counters object has two integer fields and a field whose type is
unrestricted.  single-threaded objects support other types of fields,
such as arrays.  We deal with that in the stobj-example-2.  But we
recommend that you first consider the implementation issues for the
counters example (in stobj-example-1-implementation) and then consider
the proof issues (in stobj-example-1-proofs).

To continue the stobj tour, see STOBJ-EXAMPLE-2.

STOBJ-EXAMPLE-1-DEFUNS    the defuns created by the counters stobj

Consider the event shown in stobj-example-1:

     (defstobj counters
       (NodeCnt     :type integer :initially 0)
       (TipCnt      :type integer :initially 0)
       (IntTipsSeen :type t       :initially nil))

Here is a complete list of the defuns added by the event.

The careful reader will note that the counters argument below is _not_
declared with the :stobjs xarg even though we insist that the argument
be a stobj in calls of these functions.  This "mystery" is explained
below.

     (defun NodeCntp (x)                 ;;; Recognizer for 1st field
       (declare (xargs :guard t :verify-guards t))
       (integerp x))

     (defun TipCntp (x)                  ;;; Recognizer for 2nd field
       (declare (xargs :guard t :verify-guards t))
       (integerp x))

     (defun IntTipsSeenp (x)             ;;; Recognizer for 3rd field
       (declare (xargs :guard t :verify-guards t) (ignore x))
       t)

     (defun countersp (counters)         ;;; Recognizer for object
       (declare (xargs :guard t :verify-guards t))
       (and (true-listp counters)
            (= (length counters) 3)
            (NodeCntp (nth 0 counters))
            (TipCntp (nth 1 counters))
            (IntTipsSeenp (nth 2 counters))
            t))

     (defun create-counters ()           ;;; Creator for object
       (declare (xargs :guard t :verify-guards t))
       (list '0 '0 'nil))

     (defun NodeCnt (counters)           ;;; Accessor for 1st field
       (declare (xargs :guard (countersp counters) :verify-guards t))
       (nth 0 counters))

     (defun update-NodeCnt (v counters)  ;;; Updater for 1st field
       (declare (xargs :guard
                       (and (integerp v)
                            (countersp counters))
                       :verify-guards t))
       (update-nth 0 v counters))

     (defun TipCnt (counters)            ;;; Accessor for 2nd field
       (declare (xargs :guard (countersp counters) :verify-guards t))
       (nth 1 counters))

     (defun update-TipCnt (v counters)   ;;; Updater for 2nd field
       (declare (xargs :guard
                       (and (integerp v)
                            (countersp counters))
                       :verify-guards t))
       (update-nth 1 v counters))

     (defun IntTipsSeen (counters)       ;;; Accessor for 3rd field
       (declare (xargs :guard (countersp counters) :verify-guards t))
       (nth 2 counters))

     (defun update-IntTipsSeen (v counters) ;;; Updater for 3rd field
       (declare (xargs :guard (countersp counters) :verify-guards t))
       (update-nth 2 v counters))

Observe that there is a recognizer for each of the three fields and
then a recognizer for the counters object itself.  Then, for each
field, there is an accessor and an updater.

Observe also that the functions are guarded so that they expect a
countersp for their counters argument and an appropriate value for the
new field values.

You can see all of the defuns added by a defstobj event by executing
the event and then using the :pcb! command on the stobj name.  E.g.,

     ACL2 !>:pcb! counters

will print the defuns above.

We now clear up the "mystery" mentioned above.  Note, for example in
TipCnt, that the formal counters is used.  From the discussion in
stobj-example-1 it has been made clear that TipCnt can only be called
on the counters object.  And yet, in that same discussion it was said
that an argument is so treated only if it it declared among the :stobjs
in the definition of the function.  So why doesn't TipCnt include
something like (declare (xargs :stobjs (counters)))?

The explanation of this mystery is as follows.  At the time TipCnt was
defined, during the introduction of the counters stobj, the name
"counters" was not yet a single-threaded object.  The introduction of a
new single-threaded object occurs in three steps: (1) The new primitive
recognizers, accessors, and updaters are introduced as "ordinary
functions," producing their logical axiomatizations.  (2) The
executable counterparts are defined in raw Lisp to support destructive
updating.  (3) The new name is declared a single-threaded object to
ensure that all future use of these primitives respects the
single-threadedness of the object.  The functions defined as part of
the introduction of a new single-threaded object are the only functions
in the system that have undeclared stobj formals other than state.

You may return to stobj-example-1 here.

STOBJ-EXAMPLE-1-IMPLEMENTATION    the implementation of the counters stobj

the event

     (defstobj counters
       (NodeCnt     :type integer :initially 0)
       (TipCnt      :type integer :initially 0)
       (IntTipsSeen :type t       :initially nil))

discussed in stobj-example-1, creates a Common Lisp object to represent
the current value of counters.  That object is created by evaluating
either of the following "raw" (non-ACL2) Common Lisp forms:

     (create-counters)

     (vector (make-array 1 :element-type 'integer
                           :initial-element '0)
             (make-array 1 :element-type 'integer
                           :initial-element '0)
             'nil)

and the value is stored in the Common Lisp global variable named
*the-live-counters*.

Thus, the counters object is an array of length three.  The first two
elements are arrays of size 1 and are used to hold the NodeCnt and
TipCnt fields.  The third element is the IntTipsSeen field.  The first
two fields are represented by arrays so that we can implement the
integer type specification efficiently.  Generally, integers are
"boxed" in some Common Lisp implementations, for example, GCL.
Creating a new integer requires creating a new box to put it in.  But
in some lisps, including GCL, the integers inside arrays of integers
are not boxed.

The function NodeCnt is defined in raw Lisp as:

     (defun NodeCnt (counters)
       (the integer
            (aref (the (simple-array integer (1))
                       (svref counters 0))
                  0)))

Observe that the form (svref counters 0) is evaluated to get an array
of size 1, which is followed by a call of aref to access the 0th
element of that array.

The function update-NodeCnt is defined in raw Lisp as:

     (defun update-NodeCnt (v counters)
       (declare (type integer v))
       (progn
        (setf (aref (the (simple-array integer (1))
                         (svref counters 0))
                    0)
              (the integer v))
        counters))

Note that when this function is called, it does not create a new vector
of length three, but "smashes" the existing one.

One way to see all the raw Lisp functions defined by a given defstobj is
to evaluate the defstobj event and then evaluate, in the ACL2 loop, the
expression (nth 4 (global-val 'cltl-command (w state))).  Those
functions that contain (DECLARE (STOBJ-INLINE-FN T)) will generate
defabbrev forms because the :inline keyword of defstobj was supplied the
value t.  The rest will generate defuns.

We now recommend that you look at stobj-example-1-proofs.

STOBJ-EXAMPLE-1-PROOFS    some proofs involving the counters stobj

Consider again the event

     (defstobj counters
       (NodeCnt     :type integer :initially 0)
       (TipCnt      :type integer :initially 0)
       (IntTipsSeen :type t       :initially nil))

discussed in stobj-example-1, followed by the definition

     (defun reset-counters (counters)
       (declare (xargs :stobjs (counters)))
       (seq counters
            (update-NodeCnt 0 counters)
            (update-TipCnt 0 counters)
            (update-IntTipsSeen nil counters)))

which, because of the seq macro in stobj-example-1, is just syntactic
sugar for

     (defun reset-counters (counters)
       (declare (xargs :stobjs (counters)))
       (let ((counters (update-NodeCnt 0 counters)))
         (let ((counters (update-TipCnt 0 counters)))
           (update-IntTipsSeen nil counters)))).

Here is a simple theorem about reset-counters.

     (defthm reset-counters-is-constant
       (implies (countersp x)
                (equal (reset-counters x)
                       '(0 0 nil))))

Before we talk about how to prove this theorem, note that the theorem
is unusual in two respects.

First, it calls reset-counters on an argument other than the variable
counters!  That is allowed in theorems; logically speaking, the stobj
functions are indistinguishable from ordinary functions.  Their use is
syntactically restricted only in defuns, which might be compiled and
run in raw Lisp.  Those restrictions allow us to implement stobj
modification destructively.  But logically speaking, reset-counters and
other stobj "modifying" functions just create new objects,
constructively.

Second, the theorem above explicitly provides the hypothesis that
reset-counters is being applied to an object satisfying countersp.
Such a hypothesis is not always required: reset-counters is total and
will do something no matter what x is.  But in this particular case,
the result is not '(0 0 nil) unless x is, at least, a true-list of
length three.

To make a long story short, to prove theorems about stobj functions you
behave in exactly the way you would to prove the same theorems about the
same functions defined without the stobj features.

How can we prove the above theorem?  Unfolding the definition of
reset-counters shows that (reset-counters x) is equal to

     (update-IntTipsSeen nil
       (update-TipCnt 0
         (update-NodeCnt 0 x)))

which in turn is

     (update-nth 2 nil
      (update-nth 1 0
       (update-nth 0 0 x))).

Opening up the definition of update-nth reduces this to

     (list* 0 0 nil (cdddr x)).

This is clearly equal to '(0 0 nil), provided we know that (cdddr x) is
nil.

Unfortunately, that last fact requires a lemma.  The most specific
lemma we could provide is

     (defthm special-lemma-for-counters
       (implies (countersp x)
                (equal (cdddr x) nil)))

but if you try to prove that lemma you will find that it requires some
reasoning about len and true-listp.  Furthermore, the special lemma
above is of interest only for counters.

The following lemma about len is the one we prefer.

     (defthm equal-len-n
       (implies (syntaxp (quotep n))
                (equal (equal (len x) n)
                       (if (integerp n)
                           (if (< n 0)
                               nil
                             (if (equal n 0)
                                 (atom x)
                               (and (consp x)
                                    (equal (len (cdr x)) (- n 1)))))
                         nil))))

This lemma will simplify any equality in which a len expression is
equated to any explicitly given constant _n_, e.g., 3, reducing the
equation to a conjunction of consp terms about the first _n_ cdrs.

If the above lemma is available then ACL2 immediately proves

     (defthm reset-counters-is-constant
       (implies (countersp x)
                (equal (reset-counters x)
                       '(0 0 nil))))

The point is presumably well made: proving theorems about
single-threaded object accessors and updaters is no different than
proving theorems about other recursively defined functions on lists.

As we have seen, operations on stobjs turn into definitions involving
nth and update-nth in the logic.  Here are two lemmas that are useful
for simplifying terms involving nth and update-nth, which are therefore
useful in reasoning about single-threaded objects.

     (defthm update-nth-update-nth-same
       (implies (equal (nfix i1) (nfix i2))
                (equal (update-nth i1 v1 (update-nth i2 v2 l))
                       (update-nth i1 v1 l))))

     (defthm update-nth-update-nth-diff
       (implies (not (equal (nfix i1) (nfix i2)))
                (equal (update-nth i1 v1 (update-nth i2 v2 l))
                       (update-nth i2 v2 (update-nth i1 v1 l))))
       :rule-classes ((:rewrite :loop-stopper ((i1 i2)))))

These lemmas are due to Matt Wilding.  See NU-REWRITER for a
discussion of the efficient simplification of terms of the form (nth n
(update-nth key val lst)), which can be critical in settings involving
sequential bindings that commonly arise in operations involving stobjs.

We now recommend that you see STOBJ-EXAMPLE-2.

STOBJ-EXAMPLE-2    an example of the use of arrays in single-threaded objects

The following event

     (defstobj ms
       (pcn  :type integer                  :initially 0)
       (mem  :type (array integer (100000)) :initially -1)
       (code :type t                        :initially nil))

introduces a single-threaded object named ms (which stands for "machine
state").  The object has three fields, a pcn or program counter, a mem
or memory, and a code field.

The mem field is occupied by an object initially of type (array integer
(100000)).  Logically speaking, this is a list of length 100000, each
element of which is an integer.  But in the underlying implementation
of the ms object, this field is occupied by a raw Lisp array, initially
of size 100000.

You might expect the above defstobj to define the accessor function mem
and the updater update-mem.  _That does not happen!_.

The above event defines the accessor function memi and the updater
update-memi.  These functions do not access/update the mem field of the
ms object; they access/update the individual elements of the array in
that field.

In particular, the logical definitions of the two functions are:

     (defun memi (i ms)
       (declare (xargs :guard
                       (and (msp ms)
                            (integerp i)
                            (<= 0 i)
                            (< i (mem-length ms)))))
       (nth i (nth 1 ms)))

     (defun update-memi (i v ms)
       (declare (xargs :guard
                       (and (msp ms)
                            (integerp i)
                            (<= 0 i)
                            (< i (mem-length ms))
                            (integerp v))))
       (update-nth-array 1 i v ms))

For example, to access the 511th (0-based) memory location of the
current ms you could evaluate:

     ACL2 !>(memi 511 ms)
     -1

The answer is -1 initially, because that is the above-specified initial
value of the elements of the mem array.

To set that element you could do

     ACL2 !>(update-memi 511 777 ms)
     <ms>
     ACL2 !>(memi 511 ms)
     777

The raw Lisp implementing these two functions is shown below.

     (defun memi (i ms)
       (declare (type (integer 0 268435455) i))
       (the integer
            (aref (the (simple-array integer (*))
                       (svref ms 1))
                  (the (integer 0 268435455) i))))

     (defun update-memi (i v ms)
       (declare (type (integer 0 268435455) i)
                (type integer v))
       (progn
        (setf (aref (the (simple-array integer (*))
                         (svref ms 1))
                    (the (integer 0 268435455) i))
              (the integer v))
        ms))

If you want to see the raw Lisp supporting a defstobj, execute the
defstobj and then evaluate the ACL2 form (nth 4 (global-val
'cltl-command (w state))).

To continue the stobj tour, see STOBJ-EXAMPLE-3.

STOBJ-EXAMPLE-3    another example of a single-threaded object

The event

     (defstobj $s
       (x :type integer :initially 0)
       (a :type (array (integer 0 9) (3)) :initially 9 :resizable t))

introduces a stobj named $S.  The stobj has two fields, X and A.  The A
field is an array.  The X field contains an integer and is initially 0.
The A field contains a list of integers, each between 0 and 9,
inclusively.  (Under the hood, this "list" is actually implemented as
an array.)  Initially, the A field has three elements, each of which is
9.

This event introduces the following sequence of function definitions:

     (DEFUN XP (X) ...)               ; recognizer for X field
     (DEFUN AP (X) ...)               ; recognizer of A field
     (DEFUN $SP ($S) ...)             ; top-level recognizer for stobj $S
     (DEFUN CREATE-$S NIL ...)        ; creator for stobj $S
     (DEFUN X ($S) ...)               ; accessor for X field
     (DEFUN UPDATE-X (V $S) ...)      ; updater for X field
     (DEFUN A-LENGTH ($S) ...)        ; length of A field
     (DEFUN RESIZE-A (K $S) ...)      ; resizer for A field
     (DEFUN AI (I $S) ...)            ; accessor for A field at index I
     (DEFUN UPDATE-AI (I V $S) ...)   ; updater for A field at index I

Here is the definition of $SP:

     (DEFUN $SP ($S)
       (DECLARE (XARGS :GUARD T :VERIFY-GUARDS T))
       (AND (TRUE-LISTP $S)
            (= (LENGTH $S) 2)
            (XP (NTH 0 $S))
            (AP (NTH 1 $S))
            T))

This reveals that in order to satisfy $SP an object must be a true list
of length 2 whose first element satisfies XP and whose second satisfies
AP.  By printing the definition of AP one learns that it requires its
argument to be a true list, each element of which is an integer between
0 and 9.

The initial value of stobj $S is given by zero-ary "creator" function
CREATE-$S.  Creator functions may only be used in limited contexts.
See WITH-LOCAL-STOBJ.

Here is the definition of UPDATE-AI, the updater for the A field at
index I:

     (DEFUN UPDATE-AI (I V $S)
       (DECLARE (XARGS :GUARD
                       (AND ($SP $S)
                            (INTEGERP I)
                            (<= 0 I)
                            (< I (A-LENGTH $S))
                            (AND (INTEGERP V) (<= 0 V) (<= V 9)))
                       :VERIFY-GUARDS T))
       (UPDATE-NTH-ARRAY 1 I V $S))

By definition (UPDATE-NTH-ARRAY 1 I V $S) is (UPDATE-NTH 1 (UPDATE-NTH
I V (NTH 1 $S)) $S).  This may be a little surprising but should be
perfectly clear.

First, ignore the guard, since it is irrelevant in the logic.  Reading
from the inside out, (UPDATE-AI I V $S) extracts (NTH 1 $S), which is
array a of $S.  (Recall that NTH is 0-based.)  The next higher
expression in the definition above, (UPDATE-NTH I V a), "modifies" a by
setting its Ith element to V.  Call this a'.  The next higher
expression, (UPDATE-NTH 1 a' $S), "modifies" $S by setting its 1st
component to a'.  Call this result $s'.  Then $s' is the result
returned by UPDATE-AI.

So the first useful observation is that from the perspective of the
logic, the type "restrictions" on stobjs are irrelevant.  They are
"enforced" by ACL2's guard mechanism, not by the definitions of the
updater functions.

As one might also imagine, the accessor functions do not really "care,"
logically, whether they are applied to well-formed stobjs or not.  For
example, (AI I $S) is defined to be (NTH I (NTH 1 $S)).

Thus, you will not be able to prove that (AI 2 $S) is an integer.  That
is,

     (integerp (AI 2 $S))

is not a theorem, because $S may not be well-formed.

Now (integerp (AI 2 $S)) will always evaluate to T in the top-level
ACL2 command loop, because we insist that the current value of the
stobj $S always satisfies $SP by enforcing the guards on the updaters,
independent of whether guard checking is on or off; see
SET-GUARD-CHECKING.  But in a theorem $S is just another variable,
implicitly universally quantified.

So (integerp (AI 2 $S)) is not a theorem because it is not true when
the variable $S is instantiated with, say,

     '(1 (0 1 TWO))

because, logically speaking, (AI 2 '(1 (0 1 TWO))) evaluates to the
symbol TWO.  That is,

     (equal (AI 2 '(1 (0 1 TWO))) 'TWO)

is true.

However,

     (implies (and ($SP $S) (< 2 (A-LENGTH $S))) (integerp (AI 2 $S)))

is a theorem.  To prove it, you will have to prove a lemma about AP.
The following will do:

     (defthm ap-nth
       (implies (and (AP x)
                     (integerp i)
                     (<= 0 i)
                     (< i (len x)))
                (integerp (nth i x)))).

Similarly,

     (implies (and (integerp i)
                   (<= 0 i)
                   (< i (A-LENGTH $S))
                   (integerp v)
                   (<= 0 v)
                   (<= v 9))
              ($SP (UPDATE-AI i v $S)))

is not a theorem until you add the additional hypothesis ($SP $S).  To
prove the resulting theorem, you will need a lemma such as the
following.

     (defthm ap-update-nth
       (implies (and (AP a)
                     (integerp v)
                     (<= 0 v)
                     (<= v 9)
                     (integerp i)
                     (<= 0 i)
                     (< i (len a)))
                (AP (update-nth i v a))))

The moral here is that from the logical perspective, you must provide
the hypotheses that, as a programmer, you think are implicit on the
structure of your stobjs, and you must prove their invariance.  This is
a good area for further support, perhaps in the form of a library of
macros.

_Resizing Array Fields_

Recall the specification of the array field, A for the stobj $S
introduced above:

     (a :type (array (integer 0 9) (3)) :initially 9 :resizable t)

Logically, this field is a list, initially of length 3.  Under the
hood, this field is implemented using a Common Lisp array with 3
elements.  In some applications, one may wish to lengthen an array
field, or even (to reclaim space) to shrink an array field.  The
defstobj event provides functions to access the current length of an
array field and to change the array field, with default names obtained
by suffixing the field name with "LENGTH-" or prefixing it with
"RESIZE-," respectively.  The following log shows the uses of these
fields in the above example.

     ACL2 !>(A-LENGTH $S)
     3
     ACL2 !>(RESIZE-A 10 $S) ; change length of A to 10
     <$s>
     ACL2 !>(A-LENGTH $S)
     10
     ACL2 !>(AI 7 $S)        ; new elements get value from :initially
     9
     ACL2 !>(RESIZE-A 2 $S)  ; truncate A down to first 2 elements
     <$s>
     ACL2 !>(A-LENGTH $S)
     2
     ACL2 !>(AI 7 $S)        ; error:  access past array bound

     ACL2 Error in TOP-LEVEL:  The guard for the function symbol AI, which
     is (AND ($SP $S) (INTEGERP I) (<= 0 I) (< I (A-LENGTH $S))), is violated
     by the arguments in the call (AI 7 $S).

     ACL2 !>

Here are the definitions of the relevant functions for the above
example; also see RESIZE-LIST.

     (DEFUN A-LENGTH ($S)
       (DECLARE (XARGS :GUARD ($SP $S) :VERIFY-GUARDS T))
       (LEN (NTH 1 $S)))

     (DEFUN RESIZE-A (K $S)
       (DECLARE (XARGS :GUARD ($SP $S) :VERIFY-GUARDS T))
       (UPDATE-NTH 1
                   (RESIZE-LIST (NTH 1 $S) K 9)
                   $S))

It is important to note that the implementation of array resizing in
ACL2 involves copying the entire array into a newly allocated space and
thus can be quite costly if performed often.  This approach was chosen
in order to make array access and update as efficient as possible, with
the suspicion that for most applications, array access and update are
considerably more frequent than resizing (especially if the programmer
is aware of the relative costs beforehand).

It should also be noted that computations of lengths of stobj array
fields should be fast (constant-time) in all or most Common Lisp
implementations.

Finally, if :resizable t is not supplied as shown above, then an
attempt to resize the array will result in an error.  If you do not
intend to resize the array, it is better to omit the :resizable option
(or to supply :resizable nil), since then the length function will be
defined to return a constant, namely the initial length, which can
simplify guard proofs (compare with the definition of A-LENGTH above).

This completes the tour through the documentation of stobjs.  However,
you may now wish to read the documentation for the event that
introduces a new single-threaded object; see DEFSTOBJ.

WITH-LOCAL-STOBJ    locally bind a single-threaded object

See STOBJ for an introduction to single-threaded objects.

     Example Form:
     (with-local-stobj
      st
      (mv-let (result st)
              (compute-with-st x st)
              result))

With-local-stobj can be thought of as a macro, where the example form
above expands as follows.

     (mv-let (result st)
             (let ((st (create-st)))
               (compute-with-st x st))
             (declare (ignore st))
             result)

However, ACL2 expects you to use with-local-stobj, not its expansion.
More precisely, stobj creator functions are not allowed except
(implicitly) via with-local-stobj and in logic-only situations (like
theorems and hints).  Moreover, neither with-local-stobj nor its
expansions are legal when typed directly at the top-level loop.

     General Forms:
     (with-local-stobj stobj-name mv-let-form)
     (with-local-stobj stobj-name mv-let-form creator-name)

where stobj-name is the name of a stobj other than state, mv-let-form
is a call of mv-let, and if creator-name is supplied then it should be
the  name of the creator function for stobj-name; see DEFSTOBJ.
For the example form above, its expansion would use creator-name, if
supplied, in place of create-st.

With-local-stobj can be useful when a stobj is used to memoize
intermediate results during a computation, yet it is desired not to
make the stobj a formal parameter for the function and its callers.

ACL2 can reason about these "local stobjs," and in particular about
stobj creator functions.  For technical reasons, ACL2 will not allow
you to enable the :EXECUTABLE-COUNTERPART rune of a stobj creator
function.

Finally, here is a small example concocted in order to illustrate that
with-local-stobj calls can be nested.

     (defstobj st fld1)

     (defun foo ()
       (with-local-stobj
        st ; Let us call this the ``outer binding of st''.
        (mv-let (val10 val20 st)
          (let ((st (update-fld1 10 st)))
            ;; At this point the outer binding of st has fld1 = 10.
            (let ((result (with-local-stobj
                           st ; Let us call this the ``inner binding of st''.
                           (mv-let (val st)
                             (let ((st (update-fld1 20 st)))
                               ;; Now fld1 = 20 for the inner binding of st.
                               (mv (fld1 st) st))
                             val))))
              ;; So result has been bound to 20 above, but here we are once again
              ;; looking at the outer binding of st, where fld1 is still 10.
              (mv (fld1 st) result st)))
          (mv val10 val20))))

     (thm (equal (foo) (mv 10 20))) ; succeeds

SWITCHES-PARAMETERS-AND-MODES    a variety of ways to modify the ACL2 environment

The beginning user might pay special attention to documentation for
logic and program.  Other topics in this section can be read as one
gains familiarity with ACL2.

ACL2-CUSTOMIZATION    file of initial commands for ACL2 to run at startup

ACL2 provides a mechanism to load automatically a so-called "ACL2
customization file," via ld, the first time lp is called in an ACL2
session.  ACL2 looks for this file as follows.

     o If the host Lisp reads a non-empty value for the system's
     environment variable ACL2-CUSTOMIZATION, then that string value is
     used for the customization file name.  In this case, if the file
     does not exist or if the string is "NONE" then there is no
     customization file.  Notes.  (1) If the customization file name is
     a relative pathname (see PATHNAME), then the pathname is
     considered relative to the connected book directory (see
     CBD).  (2) If this variable is not already defined, then its
     value is set to NONE when the ACL2 makefile system is invoked
     (specifically, books/Makefile-generic).

     o Otherwise (empty environment variable value), file
     "acl2-customization.lsp" or "acl2-customization.lisp" on the
     connected book directory (see CBD), generally the current
     directory, is the customization file (in that order) if either
     exists.

     o Otherwise file "acl2-customization.lsp" or
     "acl2-customization.lisp" on your home directory is the
     customization file (in that order), if either exists (except, this
     case is skipped on Windows operating systems.

Except for the fact that this ld command is not typed explicitly by
you, it is a standard ld command, with one exception: any settings of
ld specials are remembered once this call of ld has completed.  For
example, suppose that you start your customization file with
(set-ld-skip-proofsp t state), so that proofs are skipped as it is
loaded with ld.  Then the ld special ld-skip-proofsp will remain t
after the ld has completed, causing proofs to be skipped in your ACL2
session, unless your customization file sets this variable back to nil,
say with (set-ld-skip-proofsp nil state).

If the customization file exists, it is loaded with ld using the usual
default values for the ld specials (see LD).  Thus, if an error
is encountered, no subsequent forms in the file will be evaluated.

To create a customization file it is recommended that you first give it
a name other than "acl2-customization.lsp" or "acl2-customization.lisp"
so that ACL2 does not try to include it prematurely when you next enter
lp.  Then, while in the uncustomized lp, explicitly invoke ld on your
evolving (but renamed) customization file until all forms are
successfully evaluated.  The same procedure is recommended if for some
reason ACL2 cannot successfully evaluate all forms in your
customization file: temporarily rename your customization file so that
ACL2 does not try to ld it automatically and then debug the new file by
explicit calls to ld.

WARNING!  If you certify a book after the (automatic) loading of a
customization file, the forms in that file will be part of the
portcullis of the books you certify!  That is, the forms in your
customization file at certification time will be loaded whenever
anybody uses the books you are certifying.  Since customization files
generally contain idiosyncratic commands, you may not want yours to be
part of the books you create for others.  Thus, if you have a
customization file then you may want to invoke :ubt 1 before certifying
any books; alternatively, see CERTIFY-BOOK! for automatic
invocation of ubt.

On the other hand, if you wish to prevent undoing commands from the
customization file, see RESET-PREHISTORY.

Finally, we note that except on Windows-based systems, if there is a
file acl2-init.lsp in your home directory, then it will be loaded into
raw Lisp when ACL2 is invoked.

ADD-BINOP    associate a function name with a macro name

     Example:
     (add-binop append binary-append)

This example associates the function symbol binary-append with the
macro name append.  As a result, theory functions will understand that
append refers to binary-append -- see ADD-MACRO-ALIAS -- and
moreover, proof output will be printed using append rather than
binary-append, e.g., (append x y z w) is printed rather than
(binary-append x (binary-append y (binary-append z w))).

The function symbol need not be binary; the name "add-binop" is legacy
from when that was the intention.  However, the folding of
right-associated arguments suggested above only takes place for binary
function symbols.

     General Form:
     (add-binop macro-name function-name)

This is a convenient way to add an entry to macro-aliases-table and at
the same time extend the :binop-table.  As suggested by the example
above, right-associated calls of a binary function in this table will
be printed as corresponding calls of macros.  Thus in the case of a
binary function symbol fn associated with macro name mac, then a call
(fn arg1 (fn arg2 (... (fn argk arg)))) will be displayed to the user as
though the "term" were (mac arg1 arg2 ... argk arg).  For a call (f a1
... ak) of a function symbol that is not binary, then the effect is
simply to replace f by the corresponding macro symbol.  See
MACRO-ALIASES-TABLE, see REMOVE-MACRO-ALIAS, see
BINOP-TABLE, and see REMOVE-BINOP.

ADD-DEFAULT-HINTS    add to the default hints

     Examples:
     (add-default-hints '((computed-hint-1 clause)
                          (computed-hint-2 clause
                                           stable-under-simplificationp)))
     (add-default-hints '((computed-hint-3 id clause world))
                        :at-end t)

Note: This is an event!  It does not print the usual event summary but
nevertheless changes the ACL2 logical world and is so recorded.  It is
local to the book or encapsulate form in which it occurs (see
ADD-DEFAULT-HINTS! for a corresponding non-local event).

     General Forms:
     (add-default-hints lst)
     (add-default-hints lst :at-end flg)

where lst is a list.  Generally speaking, the elements of lst should be
suitable for use as computed-hints.

This event is completely analogous to set-default-hints, the difference
being that add-default-hints appends the indicated hints to the front of
the list of default hints, so that they are tried first -- or, if flg
is supplied and evaluates to other than nil, at the end of the list, so
that they are tried last -- rather than *replacing* the default hints
with the indicated hints.  Each new hint is thus considered after each
existing hints when both are applied to the same goal.  Also See
SET-DEFAULT-HINTS, see REMOVE-DEFAULT-HINTS, and see
DEFAULT-HINTS.

Finally, note that the effects of set-default-hints, add-default-hints,
and remove-default-hints are local to the book in which they appear.
Thus, users who include a book with such forms will not have their
default hints affected by such forms.  In order to export the effect of
setting the default hints, use set-default-hints!, add-default-hints!,
or remove-default-hints!.

For a related feature, which however is only for advanced system
builders, see OVERRIDE-HINTS.

ADD-DEFAULT-HINTS!    add to the default hints non-locally

Please see ADD-DEFAULT-HINTS, which is the same as
add-default-hints!  except that the latter is not local to the
encapsulate or the book in which it occurs.  Probably add-default-hints
is to be preferred unless you have a good reason for wanting to export
the effect of this event outside the enclosing encapsulate or book.

ADD-DIVE-INTO-MACRO    associate proof-checker diving function with macro name

     Examples:
     (add-dive-into-macro cat expand-address-cat)

This feature is used so that the proof-checker's DV command and numeric
diving commands (e.g., 3) will dive properly into subterms.  Please see
DIVE-INTO-MACROS-TABLE.

ADD-INCLUDE-BOOK-DIR    associate directory to keyword for include-book's :dir argument

     Example Form:
     (add-include-book-dir :smith "/u/smith/")
      ; For (include-book "foo" :dir :smith), prepend "/u/smith/" to "foo".

     General Form:
     (add-include-book-dir kwd dir)

where kwd is a keywordp and dir is the pathname of a directory.  The
effect of this event is to modify the meaning of the :dir keyword
argument of include-book as indicated by the examples above, namely by
associating the indicated directory with the indicated keyword for
purposes of the include-book :dir argument.  By the "indicated
directory" we mean, in the case that the pathname is a relative
pathname, the directory relative to the current connected book
directory; see CBD.  See DELETE-INCLUDE-BOOK-DIR for
how to undo this effect.

A keyword that is already associated with a directory string by an
existing invocation of add-include-book-dir cannot be associated with a
different directory string.  If that is your intention, first apply
delete-include-book-dir to that keyword; see
DELETE-INCLUDE-BOOK-DIR.  If however the new directory string is
identical with the old, then the call of add-include-book-dir will be
redundant (see REDUNDANT-EVENTS).

The keyword :system can never be redefined.  It will always point to the
absolute pathname of the distributed books directory, which by default
is immediately under the directory where the ACL2 executable was
originally built (see INCLUDE-BOOK, in particular the
discussion there of "books directory").

Note: This is an event!  It does not print the usual event summary but
nevertheless changes the ACL2 logical world and is so recorded.

This macro generates a call (table acl2-defaults-table
:include-book-dir-alist ...)  and hence is local to any books and
encapsulate events in which it occurs. See ACL2-DEFAULTS-TABLE.
Even if you invoke add-include-book-dir before certifying a book, so
that this event is in a book's portcullis rather than the book itself,
nevertheless that add-include-book-dir event will not be visible after
the book is included.

ADD-INVISIBLE-FNS    make some unary functions invisible to the loop-stopper algorithm

     Examples:
     (add-invisible-fns binary-+ unary-- foo)

The setting above has makes unary functions unary- and foo "invisible"
for the purposes of applying permutative :rewrite rules to binary-+
trees.  Thus, arg and (unary- arg) will be given the same weight and
will be permuted so as to be adjacent.

     General Form:
     (add-invisible-fns top-fn unary-fn1 ... unary-fnk)

where top-fn is a function symbol and the unary-fni are unary function
symbols.

For more information see INVISIBLE-FNS-TABLE.  Also see
SET-INVISIBLE-FNS-TABLE, which explains how to set the entire table
in a single event, and see REMOVE-INVISIBLE-FNS.

ADD-MACRO-ALIAS    associate a function name with a macro name

     Example:
     (add-macro-alias append binary-append)

This example associates the function symbol binary-append with the
macro name append.  As a result, the name append may be used as a runic
designator (see THEORIES) by the various theory functions.  See
MACRO-ALIASES-TABLE for more details.

     General Form:
     (add-macro-alias macro-name function-name)

This is a convenient way to add an entry to macro-aliases-table.  See
MACRO-ALIASES-TABLE and also see REMOVE-MACRO-ALIAS.

ADD-MATCH-FREE-OVERRIDE    set :match-free value to :once or :all in existing rules

     Example Forms:
     (add-match-free-override :once t)
         ; Try only the first binding of free variables when relieving hypotheses
         ; of any rule of class :rewrite, :linear, or :forward-chaining.
     (add-match-free-override :all (:rewrite foo) (:rewrite bar))
         ; For rewrite rules foo and bar, try all bindings of free variables when
         ; relieving hypotheses.
     (add-match-free-override :clear)
         ; Restore :match-free to what was originally stored for each rule (either
         ; :all or :once).

As described elsewhere (see FREE-VARIABLES), a rewrite, linear,
or forward-chaining rule may have free variables in its hypotheses, and
ACL2 can be directed either to try all bindings (":all") or just the
first (":once") when relieving a hypothesis, as a basis for relieving
subsequent hypotheses.  This direction is generally provided by
specifying either :match-free :once or :match-free :all in the
:rule-classes of the rule, or by using the most recent
set-match-free-default event.  Also see RULE-CLASSES.

However, if a proof is going slowly, you may want to modify the
behavior of some such rules so that they use only the first match for
free variables in a hypothesis when relieving subsequent hypotheses,
rather than backtracking and trying additional matches as necessary.
The event (add-match-free-override :once t) has that effect.  Or at the
other extreme, perhaps you want to specify all rules as :all rules
except for a some specific exceptions.  Then you can execute
(add-match-free-override :all t) followed by, say,
(add-match-free-override :once (:rewrite foo) (:linear bar)).

     General Forms:
     (add-match-free-override :clear)
     (add-match-free-override flg t)
     (add-match-free-override flg rune1 rune2 ... runek)

where flg is :once or :all and the runei are runes.  If :clear is
specified then all rules will have the :all/:once behavior from when
they were first stored.  The second general form causes all rewrite
linear, and forward-chaining rules to have the behavior specified by
flg (:all or :once).  Finally, the last of these, where runes are
specified, is additive in the sense that only the indicated rules are
affected; all others keep the behavior they had just before this event
was executed (possible because of earlier add-match-free-override
events).

At the conclusion of this event, ACL2 prints out the list of all
:linear, :rewrite, and :forward-chaining runes whose rules contain free
variables in hypotheses that are to be bound :once, except that if
there are no overrides (value :clear was used), then :clear is printed.

This event only affects rules that exist at the time it is executed.
Future rules are not affected by the override.

Note: This is an event!  It does not print the usual event summary but
nevertheless changes the ACL2 logical world and is so recorded.  It
uses the acl2-defaults-table, and hence its effect is local to the book
or encapsulate form in which it occurs.

_Remarks_

Lists of the :rewrite, :linear, and :forward-chaining runes whose
behavior was originally :once or :all are returned by the following
forms, respectively.

     (free-var-runes :once (w state))
     (free-var-runes :all  (w state))

The form

     (match-free-override (w state))

evaluates to a pair, whose car is a number used by ACL2 to determine
whether a rune is sufficiently old to be affected by the override, and
whose cdr is the list of runes whose behavior is specified as :once by
add-match-free-override; except, if no runes have been overridden, then
the keyword :clear is returned.

ADD-NTH-ALIAS    associate one symbol with another for printing of nth/update-nth terms

     Example:
     (add-nth-alias st0 st)

This example associates the symbol st0 with the symbol st for purposes
of printing certain terms of the form (nth n st0) and (update-nth n val
st0).

     General Form:
     (add-nth-alias alias-name name)

This is a convenient way to add an entry to nth-aliases-table.  See
NTH-ALIASES-TABLE and also see REMOVE-NTH-ALIAS.

ADD-OVERRIDE-HINTS    add to the override-hints

See OVERRIDE-HINTS for a discussion of override-hints.  Here we
describe how to extend the list of override-hints.  Note that the
effects of add-override-hints events are local to the books or
encapsulate events in which they reside; see
ADD-OVERRIDE-HINTS! to avoid that restriction.  Also see
SET-OVERRIDE-HINTS to set a new list of override-hints to it,
ignoring the present list rather than adding to it.

     General Forms:
     (add-override-hints form)
     (add-override-hints form :at-end t)
     (add-override-hints form :at-end nil) ; default for :at-end

where form evaluates to a list of computed hint forms.  The effect of
this event is to extend the current list of override-hints by appending
the result of that evaluation.  The default is to append the evaluation
result to the front of the current list of override-hints, but if
:at-end t is specified, then the evaluation result is appended to the
end of the current list.

ADD-OVERRIDE-HINTS!    add non-locally to the override-hints

Add-override-hints! is the same as add-override-hints, except that the
former is not local to books or encapsulate events in which it occurs.
See ADD-OVERRIDE-HINTS; also see SET-OVERRIDE-HINTS.

BINOP-TABLE    associates binary function with the corresponding macro

     Examples:
     ACL2 !>(binop-table (w state))
     '((binary-+ . +)
       (binary-* . *)
       (binary-append . append)
       (binary-logand . logand)
       (binary-logior . logior)
       (binary-logxor . logxor)
       (binary-logeqv . logeqv))

See TABLE for a general discussion of tables.

See ADD-BINOP for a more general discussion of this table.

DEFAULT-HINTS-TABLE    a table used to provide hints for proofs

Please see SET-DEFAULT-HINTS, see ADD-DEFAULT-HINTS, and
see REMOVE-DEFAULT-HINTS for how to use this table.  For
completeness, we mention here that under the hood, these events all
update the default-hints-table by updating its key, t, for example as
follows.

     (table default-hints-table t
            '((computed-hint-1 clause)
              (computed-hint-2 clause
                               stable-under-simplificationp)))

The use of default hints is explained elsewhere; see
SET-DEFAULT-HINTS.

Advanced users only: see OVERRIDE-HINTS for an advanced variant
of default hints.

DEFAULT-VERIFY-GUARDS-EAGERNESS    See SET-VERIFY-GUARDS-EAGERNESS.