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

I-AM-HERE    a convenient marker for use with rebuild

     Example Input File for Rebuild:
     (defun fn1 (x y) ...)
     (defthm lemma1 ...)
     (defthm lemma2 ...)
     (i-am-here)
     The following lemma won't go through.  I started
     typing the hint but realized I need to prove a
     lemma first.  See the failed proof attempt in foo.bar.
     I'm going to quit for the night now and resume tomorrow
     from home.

     (defthm lemma3 ...
       :hints (("Goal" :use (:instance ???
     ...

By putting an (i-am-here) form at the "frontier" of an evolving file of
commands, you can use rebuild to load the file up to the (i-am-here).
I-am-here simply returns an ld error triple and any form that "causes an
error" will do the same job.  Note that the text of the file after the
(i-am-here) need not be machine readable.

IMMEDIATE-FORCE-MODEP    when executable counterpart is enabled,
 forced hypotheses are attacked immediately

Also see DISABLE-IMMEDIATE-FORCE-MODEP and see
ENABLE-IMMEDIATE-FORCE-MODEP.

This function symbol is defined simply to provide a rune which can be
enabled and disabled.  Enabling

     (:executable-counterpart immediate-force-modep)

causes ACL2 to attack forced hypotheses immediately instead of delaying
them to the next forcing round.

     Example Hints
     :in-theory (disable (:executable-counterpart immediate-force-modep))
                ; delay forced hyps to forcing round
     :in-theory (enable (:executable-counterpart immediate-force-modep))
                ; split on forced hyps immediately

See FORCE for background information.  When a forced hypothesis
cannot be established a record is made of that fact and the proof
continues.  When the proof succeeds a "forcing round" is undertaken in
which the system attempts to prove each of the forced hypotheses
explicitly.  However, if the rune (:executable-counterpart
immediate-force-modep) is enabled at the time the hypothesis is forced,
then ACL2 does not delay the attempt to prove that hypothesis but
undertakes the attempt more or less immediately.

IN-PACKAGE    select current package

     Example:
     (in-package "MY-PKG")

     General Form:
     (in-package str)

where str is a string that names an existing ACL2 package, i.e., one of
the initial packages such as "KEYWORD" or "ACL2" or a package introduced
with defpkg.  For a complete list of the known packages created with
defpkg, evaluate

     (strip-cars (known-package-alist state)).

See DEFPKG.  An ACL2 book (see BOOKS) must contain a
single in-package form, which must be the first form in that book.

INDUCT    hints keyword :INDUCT

See HINTS.

KEYWORD-COMMANDS    how keyword commands are processed

     Examples:
     user type-in                 form evaluated
     :pc 5                        (ACL2::PC '5)
     :pcs app rev                 (ACL2::PCS 'app 'rev)
     :length (1 2 3)              (ACL2::LENGTH '(1 2 3))

When a keyword, :key, is read as a command, ACL2 determines whether the
symbol with the same name in the "ACL2" package, acl2::key, is a
function or simple macro of n arguments.  If so, ACL2 reads n more
objects, obj1, ..., objn, and then acts as though it had read the
following form (for a given key):

     (ACL2::key 'obj1 ... 'objn)

Thus, by using the keyword command hack you avoid typing the
parentheses, the "ACL2" package name, and the quotation marks.

Note the generality of this hack.  Almost any function or macro in the
"ACL2" package can be so invoked, not just "commands."  Indeed, there is
no such thing as a distinguished class of commands.  The one caveat is
that the keyword hack can be used to invoke a macro only if that macro
has a simple argument list -- one containing no lambda keywords (such as
&rest), since they complicate or render impossible the task of deciding
how many objects to read.  Users may take advantage of the keyword
command hack by defining functions and macros in the "ACL2" package.

LAMBDA    See TERM.

LD-ERROR-ACTION    determines ld's response to an error

Ld-error-action is an ld special (see LD).  The accessor is
(ld-error-action state) and the updater is (set-ld-error-action val
state).  Ld-error-action must be :continue, :return, or :error.  The
initial value of ld-error-action is :continue, which means that the
top-level ACL2 command loop will not exit when an error is caused by
user-typein.  But the default value for ld-error-action on calls of ld
is :return.

The general-purpose ACL2 read-eval-print loop, ld, reads forms from
standard-oi, evaluates them and prints the result to standard-co.
However, there are various flags that control ld's behavior and
ld-error-action is one of them.  If, while ld-error-triples is t, a form
evaluates to three results, the first of which is non-nil and the third
of which is state, an error is said to have occurred.  If an error
occurs, ld's action depends on ld-error-action.  If it is :continue, ld
just continues processing the forms in standard-oi.  If it is :return,
ld stops and returns as though it had emptied the channel.  If it is
:error, ld stops and returns, signalling an error to its caller.

LD-ERROR-TRIPLES    determines whether a form caused an error during ld

Ld-error-triples is an ld special (see LD).  The accessor is
(ld-error-triples state) and the updater is (set-ld-error-triples val
state).  Ld-error-triples must be either t or nil.  The initial value of
ld-error-triples is t.

The general-purpose ACL2 read-eval-print loop, ld, reads forms from
standard-oi, evaluates them and prints the result to standard-co.
However, there are various flags that control ld's behavior and
ld-error-triples is one of them.  If this variable has the value t then
when a form evaluates to 3 values, the first of which is non-nil and the
third of which is state, an error is deemed to have occurred.  When an
error occurs in evaluating a form, ld rolls back the ACL2 world to the
configuration it had at the conclusion of the last error-free form.
Then ld takes the action determined by ld-error-action.

LD-EVISC-TUPLE    determines whether ld suppresses details when printing

Ld-evisc-tuple is an ld special (see LD).  The accessor is
(ld-evisc-tuple state) and the updater is (set-ld-evisc-tuple val
state).  Ld-evisc-tuple must be either nil or a list of the form

     (alist print-level print-length hiding-cars)

where alist is an alist that pairs objects to strings, print-level and
print-length are either nil or non-negative integers, and hiding-cars is
a list of symbols.  The initial value of ld-evisc-tuple is nil.

The general-purpose ACL2 read-eval-print loop, ld, reads forms from
standard-oi, evaluates them and prints the result to standard-co.
However, there are various flags that control ld's behavior and
ld-evisc-tuple is one of them.  Ld may print the forms it is evaluating
and/or the results of evaluation.  If the value of ld-evisc-tuple is a
list as shown above, then ld "eviscerates" the objects it prints before
printing them.  To "eviscerate" an object we replace certain
substructures within it by strings which are printed in their stead.
Print-level and print-length, above, are used as described in CLTL (pp
372) to replace those substructures deeper than print-level by "#" and
those longer than print-length by "...".  Alist is used to replace any
substructure occuring as a key in alist by the corresponding string.
Finally, any consp x that starts with one of the symbols in hiding-cars
is printed as <hidden>.

The printing of error messages and warnings, as well as certain other
output, uses a different such evisc-tuple, (default-evisc-tuple state).
The advanced user can override this evisc-tuple with the state global
user-default-evisc-tuple.  Similarly, some other printing uses yet
another evisc-tuple, (term-evisc-tuple t state), which can be overridden
with state global user-term-evisc-tuple.  We may document these
mechanisms more fully if there is sufficient user interest.

LD-KEYWORD-ALIASES    allows the abbreviation of some keyword commands

     Example:
     (set-ld-keyword-aliases '((:q 0 q-fn)
                               (:e 0 exit-acl2-macro))
                             state)

Ld-keyword-aliases is an ld special (see LD).  The accessor is
(ld-keyword-aliases state) and the updater is (set-ld-keyword-aliases
val state).  Ld-keyword-aliases must be an alist, each element of which
is of the form (:keyword n fn), where :keyword is a keyword, n is a
nonnegative integer, and fn is a function symbol of arity n, a macro
symbol, or a lambda expression of arity n.  When keyword is typed as an
ld command, n more forms are read, x1, ..., xn, and the form (fn 'x1
... 'xn) is then evaluated.  The initial value of ld-keyword-aliases is
nil.

In the example above, :q has been redefined to have the effect of
executing (q-fn), so for example if you define

     (defmacro q-fn ()
       '(er soft 'q "You un-bound :q and now we have a soft error."))

then :q will cause an error, and if you define

     (defmacro exit-acl2-macro () '(exit-ld state))

then :e will cause the effect (it so happens) that :q normally has.  If
you prefer :e to :q for exiting the ACL2 loop, you might even want to
put such definitions of q-fn and exit-acl2-macro together with the
set-ld-keyword-aliases form above in your "acl2-customization.lisp"
file; see ACL2-CUSTOMIZATION.

The general-purpose ACL2 read-eval-print loop, ld, reads forms from
standard-oi, evaluates them and prints the result to standard-co.
However, there are various flags that control ld's behavior and
ld-keyword-aliases is one of them.  Ld-keyword-aliases affects how
keyword commands are parsed.  Generally speaking, ld's command
interpreter reads ":fn x1 ... xn" as "(fn 'x1 ... 'xn)" when :fn is a
keyword and fn is the name of an n-ary function.  But this parse is
overridden, as described above, for the keywords bound in
ld-keyword-aliases.

LD-POST-EVAL-PRINT    determines whether and how ld prints the result of evaluation

Ld-post-eval-print is an ld special (see LD).  The accessor is
(ld-post-eval-print state) and the updater is (set-ld-post-eval-print
val state).  Ld-post-eval-print must be either t, nil, or
:command-conventions.  The initial value of ld-post-eval-print is
:command-conventions.

The general-purpose ACL2 read-eval-print loop, ld, reads forms from
standard-oi, evaluates them and prints the result to standard-co.
However, there are various flags that control ld's behavior and
ld-post-eval-print is one of them.  If this global variable is t, ld
prints the result.  In the case of a form that produces a multiple
value, ld prints the list containing all the values (which, logically
speaking, is what the form returned).  If ld-post-eval-print is nil, ld
does not print the values.  This is most useful when ld is used to load
a previously processed file.

Finally, if ld-post-eval-print is :command-conventions then ld prints
the result but treats "error triples" specially.  An "error triple" is a
result, (mv erp val state), that consists of three values, the third of
which is state.  Many ACL2 functions use such triples to signal errors.
The convention is that if erp (the first value) is nil, then the
function is returning val (the second value) as its conventional single
result and possibly side-effecting state (as with some output).  If erp
is t, then an error has been caused, val is irrelevant and the error
message has been printed in the returned state.  Example ACL2 functions
that follow this convention include defun and in-package.  If such
"error producing" functions are evaluated while ld-post-eval-print is
set to t, then you would see them producing lists of length 3.  This is
disconcerting to users accustomed to Common Lisp (where these functions
produce single results but sometimes cause errors or side-effect state).

When ld-post-eval-print is :command-conventions and a form produces an
error triple (mv erp val state) as its value, ld prints nothing if erp
is non-nil and otherwise ld prints just val.  Because it is a
misrepresentation to suggest that just one result was returned, ld
prints the value of the global variable 'triple-print-prefix before
printing val.  'triple-print-prefix is initially " ", which means that
when non-erroneous error triples are being abbreviated to val, val
appears one space off the left margin instead of on the margin.

In addition, when ld-post-eval-print is :command-conventions and the
value component of an error triple is the keyword :invisible then ld
prints nothing.  This is the way certain commands (e.g., :pc) appear to
return no value.

By printing nothing when an error has been signalled, ld makes it appear
that the error (whose message has already appeared in state) has
"thrown" the computation back to load without returning a value.  By
printing just val otherwise, we suppress the fact that state has
possibly been changed.

LD-PRE-EVAL-FILTER    determines which forms ld evaluates

Ld-pre-eval-filter is an ld special (see LD).  The accessor is
(ld-pre-eval-filter state) and the updater is (set-ld-pre-eval-filter
val state).  Ld-pre-eval-filter must be either :all, :query, or a new
name that could be defined (e.g., by defun or defconst).  The initial
value of ld-pre-eval-filter is :all.

The general-purpose ACL2 read-eval-print loop, ld, reads forms from
standard-oi, evaluates them and prints the result to standard-co.
However, there are various flags that control ld's behavior and
ld-pre-eval-filter is one of them.  If the filter is :all, then every
form read is evaluated.  If the filter is :query, then after a form is
read it is printed to standard-co and the user is asked if the form is
to be evaluated or skipped.  If the filter is a new name, then all forms
are evaluated until that name is introduced, at which time ld terminates
normally.

The :all filter is, of course, the normal one.  :Query is useful if you
want to replay selected the commands in some file.  The new name filter
is used if you wish to replay all the commands in a file up through the
introduction of the given one.

LD-PRE-EVAL-PRINT    determines whether ld prints the forms to be eval'd

Ld-pre-eval-print is an ld special (see LD).  The accessor is
(ld-pre-eval-print state) and the updater is (set-ld-pre-eval-print val
state).  Ld-pre-eval-print must be either t, nil, or :never.  The
initial value of ld-pre-eval-print is nil.

The general-purpose ACL2 read-eval-print loop, ld, reads forms from
standard-oi, evaluates them and prints the result to standard-co.
However, there are various flags that control ld's behavior and
ld-pre-eval-print is one of them.  If this global variable is t, then
before evaluating the form just read from standard-oi, ld prints the
form to standard-co.  If the variable is nil, no such printing occurs.
The t option is useful if you are reading from a file of commands and
wish to assemble a complete script of the session in standard-co.

The value :never of ld-pre-eval-print is rarely used.  During the
evaluation of encapsulate and of certify-book forms, subsidiary events
are normally printed, even if ld-pre-eval-print is nil.  Thus for
example, when the user submits an encapsulate form, all subsidiary
events are generally printed even in the default situation where
ld-pre-eval-print is nil.  But occasionally one may want to suppress
such printing.  In that case, ld-pre-eval-print should be set to :never.
As described elsewhere (see SET-INHIBIT-OUTPUT-LST), another way
to suppress such printing is to execute (set-inhibit-output-lst lst)
where lst evaluates to a list including 'prove and 'event.

LD-PROMPT    determines the prompt printed by ld

Ld-prompt is an ld special (see LD).  The accessor is (ld-prompt
state) and the updater is (set-ld-prompt val state).  Ld-prompt must be
either nil, t, or a function symbol that, when given an open output
character channel and state, prints the desired prompt to the channel
and returns two values: the number of characters printed and the state.
The initial value of ld-prompt is t.

The general-purpose ACL2 read-eval-print loop, ld, reads forms from
standard-oi, evaluates them and prints the result to standard-co.
However, there are various flags that control ld's behavior and
ld-prompt is one of them.  Ld-prompt determines whether ld prints a
prompt before reading the next form from standard-oi.  If ld-prompt is
nil, ld prints no prompt.  If ld-prompt is t, the default prompt printer
is used, which displays information that includes the current package,
default defun-mode, guard checking status (on or off), and
ld-skip-proofsp; see DEFAULT-PRINT-PROMPT.

If ld-prompt is neither nil nor t, then it should be a function name,
fn, such that (fn channel state) will print the desired prompt to
channel in state and return (mv col state), where col is the number of
characters output (on the last line output).  You may define your own
prompt printing function.

If you supply an inappropriate prompt function, i.e., one that causes an
error or does not return the correct number and type of results, the
following odd prompt will be printed instead:

     Bad Prompt
     See :DOC ld-prompt>

which will lead you to this message.  You should either call ld
appropriately next time or assign an appropriate value to ld-prompt.

LD-QUERY-CONTROL-ALIST    how to default answers to queries

Ld-query-control-alist is an ld special (see LD).  The accessor
is (ld-query-control-alist state) and the updater is
(set-ld-query-control-alist val state).  Roughly speaking,
ld-query-control-alist is either nil (meaning all queries should be
interactive), t (meaning all should default to the first accepted
response), or an alist that pairs query ids to keyword responses.  The
alist may end in either t or nil, indicating the default value for all
ids not listed explicitly.  Formally, the ld-query-control-alist must
satisfy ld-query-control-alistp.  The initial ld-query-control-alist is
nil, which means all queries are handled interactively.

When an ACL2 query is raised, a unique identifying symbol is printed in
parentheses after the word "Query".  This symbol, called the "query id,"
can be used in conjunction with ld-query-control-alist to prevent the
query from being handled interactively.  By "handled interactively" we
mean that the query is printed to *standard-co* and a response is read
from *standard-oi*.  The alist can be used to obtain a "default value"
for each query id.  If this value is nil, then the query is handled
interactively.  In all other cases, the system handles the query without
interaction (although text may be printed to standard-co to make it
appear that an interaction has occurred; see below).  If the default
value is t, the system acts as though the user responded to the query by
typing the first response listed among the acceptable responses.  If the
default value is neither nil nor t, then it must be a keyword and one of
the acceptable responses.  In that case, the system acts as though the
user responded with the given keyword.

Next, we discuss how the ld-query-control-alist assigns a default value
to each query id.  It assigns each id the first value paired with the id
in the alist, or, if no such pair appears in the alist, it assigns the
final cdr of the alist as the value.  Thus, nil assigns all ids nil.  T
assigns all ids t.  '((:filter . nil) (:sysdef . :n) . t) assigns nil to
the :filter query, :n to the :sysdef query, and t to all others.

It remains only to discuss how the system prints text when the default
value is not nil, i.e., when the query is handled without interaction.
In fact, it is allowed to pair a query id with a singleton list
containing a keyword, rather than a keyword, and this indicates that no
printing is to be done.  Thus for the example above, :sysdef queries
would be handled noninteractively, with printing done to simulate the
interaction.  But if we change the example so that :sysdef is paired
with (:n), i.e., if ld-query-control-alist is '((:filter . nil) (:sysdef
:n) . t), then no such printing would take place for sysdef queries.
Instead, the default value of :n would be assigned "quietly".

LD-REDEFINITION-ACTION    to allow redefinition without undoing

Ld-redefinition-action is an ld special (see LD).  The accessor
is (ld-redefinition-action state) and the updater is
(set-ld-redefinition-action val state).  *If* ld-redefinition-action
*is* non-nil *then ACL2 is liable to be made unsafe or unsound by*
*ill-considered definitions*.  The keyword command :redef will set
ld-redefinition-action to a convenient setting allowing unsound
redefinition.  See below.

When ld-redefinition-action is nil, redefinition is prohibited.  In that
case, an error message is printed upon any attempt to introduce a name
that is already in use.  There is one exception to this rule.  It is
permitted to redefine a function symbol in :program mode to be a
function symbol in :logic mode provided the formals and body remain the
same.  This is the standard way a function "comes into" logical
existence.

Throughout the rest of this discussion we exclude from our meaning of
"redefinition" the case in which a function in :program mode is
identically redefined in :logic mode.  At one time, ACL2 freely
permitted the signature-preserving redefinition of :program mode
functions but it no longer does.  See REDEFINING-PROGRAMS.

When ld-redefinition-action is non-nil, you are allowed to redefine a
name that is already in use.  *The system may be rendered unsound* by
such an act.  It is important to understand how dangerous redefinition
is.  Suppose fn is a function symbol that is called from within some
other function, say g.  Suppose fn is redefined so that its arity
changes.  Then the definition of g is rendered syntactically ill-formed
by the redefinition.  This can be devastating since the entire ACL2
system assumes that terms in its data base are well-formed.  For
example, if ACL2 executes g by running the corresponding function in raw
Common Lisp the redefinition of fn may cause raw lisp to break in
irreparable ways.  As Lisp programmers we live with this all the time by
following the simple rule: after changing the syntax of a function don't
run any function that calls it via its old syntax.  This rule also works
in the context of the evaluation of ACL2 functions, but it is harder to
follow in the context of ACL2 deductions, since it is hard to know
whether the data base contains a path leading the theorem prover from
facts about one function to facts about another.  Finally, of course,
even if the data base is still syntactically well-formed there is no
assurance that all the rules stored in it are valid.  For example,
theorems proved about g survive the redefinition of fn but may have
crucially depended on the properties of the old fn.  In summary, we
repeat the warning: *all bets are off if you set* ld-redefinition-action
to *non*-nil.

If at any point in a session you wish to see the list of all names that
have been redefined, see REDEFINED-NAMES.

That said, we'll give you enough rope to hang yourself.  When
ld-redefinition-action is non-nil, it must be a pair, (a .  b).  The
value of a determines how the system interacts with you when a
redefinition is submitted.  The value of b allows you to specify how the
property list of the redefined name is to be "renewed" before the
redefinition.

There are several dimensions to the space of possibilities controlled by
part a: Do you want to be queried each time you redefine a name, so you
can confirm your intention?  (We sometimes make typing mistakes or
simply forget we have used that name already.)  Do you want to see a
warning stating that the name has been redefined?  Do you want ACL2
system functions given special protection from possible redefinition?
Below are the choices for part a:

     :query -- every attempt to redefine a name will produce a query.
     The query will allow you to abort the redefinition or proceed.  It
     will will also allow you to specify the part b for this
     redefinition.  :Query is the recommended setting for users who wish
     to dabble in redefinition.

     :warn -- any user-defined function may be redefined but a
     post-redefinition warning is printed.  The attempt to redefine a
     system name produces a query.  If you are prototyping and testing a
     big system in ACL2 this is probably the desired setting for part a.

     :doit -- any user-defined function may be redefined silently
     (without query or warning) but when an attempt is made to redefine
     a system function, a query is made.  This setting is recommended
     when you start making massive changes to your prototyped system
     (and tire of even the warning messages issued by :warn).

In support of our own ACL2 systems programming there are two other
settings.  We suggest ordinary users not use them.

     :warn! -- every attempt to redefine a name produces a warning but
     no query.  Since ACL2 system functions can be redefined this way,
     this setting should be used by the only-slightly-less-than
     supremely confident ACL2 system hacker.

     :doit! -- this setting allows any name to be redefined silently
     (without query or warnings).  ACL2 system functions are fair game.
     This setting is reserved for the supremely confident ACL2 system
     hacker.  (Actually, this setting is used when we are loading
     massively modified versions of the ACL2 source files.)

Part b of ld-redefinition-action tells the system how to "renew" the
property list of the name being redefined.  There are two choices:

     :erase -- erase all properties stored under the name, or

     :overwrite -- preserve existing properties and let the redefining
     overwrite them.

It should be stressed that neither of these b settings is guaranteed to
result in an entirely satisfactory state of affairs after the
redefinition.  Roughly speaking, :erase returns the property list of the
name to the state it was in when the name was first introduced.  Lemmas,
type information, etc., stored under that name are lost.  Is that what
you wanted?  Sometimes it is, as when the old definition is "completely
wrong." But other times the old definition was "almost right" in the
sense that some of the work done with it is still (intended to be)
valid.  In that case, :overwrite might be the correct b setting.  For
example if fn was a function and is being re-defun'd with the same
signature, then the properties stored by the new defun should overwrite
those stored by the old defun but the properties stored by defthms will
be preserved.

In addition, neither setting will cause ACL2 to erase properties stored
under other symbols!  Thus, if FOO names a rewrite rule which rewrites a
term beginning with the function symbol BAR and you then redefine FOO to
rewrite a term beginning with the function symbol BAZ, then the old
version of FOO is still available (because the rule itself was added to
the rewrite rules for BAR, whose property list was not cleared by
redefining FOO).

The b setting is only used as the default action when no query is made.
If you choose a setting for part a that produces a query then you will
have the opportunity, for each redefinition, to specify whether the
property list is to be erased or overwritten.

The keyword command :redef sets ld-redefinition-action to the pair
(:query . :overwrite).  Since the resulting query will give you the
chance to specify :erase instead of :overwrite, this setting is quite
convenient.  But when you are engaged in heavy-duty prototyping, you may
wish to use a setting such as :warn or even :doit.  For that you will
have to invoke a form such as:

     (set-ld-redefinition-action '(:doit . :overwrite) state) .

Encapsulate causes somewhat odd interaction with the user if
redefinition occurs within the encapsulation because the encapsulated
event list is processed several times.  For example, if the redefinition
action causes a query and a non-local definition is actually a
redefinition, then the query will be posed twice, once during each pass.
C'est la vie.

Finally, it should be stressed again that redefinition is dangerous
because not all of the rules about a name are stored on the property
list of the name.  Thus, redefinition can render ill-formed terms stored
elsewhere in the data base or can preserve now-invalid rules.  See
REDUNDANT-EVENTS, in particular the section "Note About Unfortunate
Redundancies," for more discussion of potential pitfalls of
redefinition.

LD-SKIP-PROOFSP    how carefully ACL2 processes your commands

     Examples:
     ACL2 !>(set-ld-skip-proofsp t state)
      T
     ACL2 !s>(set-ld-skip-proofsp nil state)
      NIL
     ACL2 !>(set-ld-skip-proofsp 'include-book state)
      INCLUDE-BOOK
     ACL2 !s>

A global variable in the ACL2 state, called 'ld-skip-proofsp, determines
the thoroughness with which ACL2 processes your commands.  This variable
may take on one of three values: t, nil or 'include-book.  When
ld-skip-proofsp is non-nil, the system assumes that which ought to be
proved and is thus unsound.  The form (set-ld-skip-proofsp flg state) is
the general-purpose way of setting ld-skip-proofsp.  This global
variable is an "ld special," which is to say, you may call ld in such a
way as to "bind" this variable for the dynamic extent of the ld.

When ld-skip-proofsp is non-nil, the default prompt displays the
character s.  Thus, the prompt

     ACL2 !s>

means that the default defun-mode is :logic (otherwise the character p,
for :program, would also be printed; see DEFAULT-PRINT-PROMPT)
but "proofs are being skipped."

Observe that there are two legal non-nil values, t and 'include-book.
When ld-skip-proofsp is t, ACL2 skips all proof obligations but
otherwise performs all other required analysis of input events.  When
ld-skip-proofsp is 'include-book, ACL2 skips not only proof obligations
but all analysis except that required to compute the effect of
successfully executed events.  To explain the distinction, let us
consider one particular event, say a defun.  Very roughly speaking, a
defun event normally involves a check of the syntactic well-formedness
of the submitted definition, the generation and proof of the termination
conditions, and the computation and storage of various rules such as a
:definition rule and some :type-prescription rules.  By "normally" above
we mean when ld-skip-proofsp is nil.  How does a defun behave when
ld-skip-proofsp is non-nil?

If ld-skip-proofsp is t, then defun performs the syntactic
well-formedness checks and computes and stores the various rules, but it
does not actually carry out the termination proofs.  If ld-skip-proofsp
is 'include-book, defun does not do the syntactic well-formedness check
nor does it carry out the termination proof.  Instead, it merely
computes and stores the rules under the assumption that the checks and
proofs would all succeed.  Observe that a setting of 'include-book is
"stronger" than a setting of t in the sense that 'include-book causes
defun to assume even more about the admissibility of the event than t
does.

As one might infer from the choice of name, the include-book event sets
ld-skip-proofsp to 'include-book when processing the events in a book
being loaded.  Thus, include-book does the miminal work necessary to
carry out the effects of every event in the book.  The syntactic checks
and proof obligations were, presumably, successfully carried out when
the book was certified.

A non-nil value for ld-skip-proofsp also affects the system's output
messages.  Event summaries (the paragraphs that begin "Summary" and
display the event forms, rules used, etc.) are not printed when
ld-skip-proofsp is non-nil.  Warnings and observations are printed when
ld-skip-proofsp is t but are not printed when it is 'include-book.

Intuitively, ld-skip-proofsp t means skip just the proofs and otherwise
do all the work normally required for an event; while ld-skip-proofsp
'include-book is "stronger" and means do as little as possible to
process events.  In accordance with this intuition, local events are
processed when ld-skip-proofsp is t but are skipped when ld-skip-proofsp
is 'include-book.

The ACL2 system itself uses only two settings, nil and 'include-book,
the latter being used only when executing the events inside of a book
being included.  The ld-skip-proofsp setting of t is provided as a
convenience to the user.  For example, suppose one has a file of events.
By loading it with ld with ld-skip-proofsp set to t, the events can all
be checked for syntactic correctness and assumed without proof.  This is
a convenient way to recover a state lost by a system crash or to
experiment with a modification of an events file.

The foregoing discussion is actually based on a lie.  ld-skip-proofsp is
allowed two other values, 'initialize-acl2 and
'include-book-with-locals.  The first causes behavior similar to t but
skips local events and avoids some error checks that would otherwise
prevent ACL2 from properly booting.  The second is identical to
'include-book but also executes local events.  These additional values
are not intended for use by the user, but no barriers to their use have
been erected.

We close by reminding the user that ACL2 is potentially unsound if
ld-skip-proofsp is ever set by the user.  We provide access to it simply
to allow experimentation and rapid reconstruction of lost or modified
logical worlds.

LD-VERBOSE    determines whether ld prints "ACL2 Loading ..."

Ld-verbose is an ld special (see LD).  The accessor is
(ld-verbose state) and the updater is (set-ld-verbose val state).
Ld-verbose must be t, nil or a string or consp suitable for fmt printing
via the ~@ command.  The initial value of ld-verbose is a fmt message
that prints the ACL2 version number, ld level and connected book
directory.

Before processing the forms in standard-oi, ld may print a header.  The
printing of this header is controlled by ld-verbose.  If ld-verbose is
nil, no header is printed.  If it is t, ld prints the message

        ACL2 loading <file>

where <file> is the input channel supplied to ld.  A similar message is
printed when ld completes.  If ld-verbose is neither t nor nil then it
is presumably a header and is printed with the ~@ fmt directive before
ld begins to read and process forms.  In this case the ~@ fmt directive
is interpreted in an environment in which #\v is the ACL2 version
string, #\l is the level of the current recursion in ld and/or wormhole,
and #\c is the connected book directory (cbd).

LEMMA-INSTANCE    an object denoting an instance of a theorem

Lemma instances are the objects one provides via :use and :by hints (see
HINTS) to bring to the theorem prover's attention some
previously proved or easily provable fact.  A typical use of the :use
hint is given below.  The value specified is a list of five lemma
instances.

     :use (reverse-reverse
           (:type-prescription app)
           (:instance assoc-of-app
                      (x a) (y b) (z c))
           (:functional-instance p-f
                                 (p consp) (f flatten))
           (:instance (:theorem (equal x x))
                      (x (flatten a))))

Observe that an event name can be a lemma instance.  The :use hint
allows a single lemma instance to be provided in lieu of a list, as in:

     :use reverse-reverse

or

     :use (:instance assoc-of-app (x a) (y b) (z c))

A lemma instance denotes a formula which is either known to be a theorem
or which must be proved to be a theorem before it can be used.  To use a
lemma instance in a particular subgoal, the theorem prover adds the
formula as a hypothesis to the subgoal before the normal theorem proving
heuristics are applied.

A lemma instance, or lmi, is of one of the following five forms:

(1) name, where name names a previously proved theorem, axiom, or
definition and denotes the formula (theorem) of that name.

(2) rune, where rune is a rune (see RUNE) denoting the
:corollary justifying the rule named by the rune.

(3) (:theorem term), where term is any term alleged to be a theorem.
Such a lemma instance denotes the formula term.  But before using such a
lemma instance the system will undertake to prove term.

(4) (:instance lmi (v1 t1) ... (vn tn)), where lmi is recursively a
lemma instance, the vi's are distinct variables and the ti's are terms.
Such a lemma instance denotes the formula obtained by instantiating the
formula denoted by lmi, replacing each vi by ti.

(5) (:functional-instance lmi (f1 g1) ... (fn gn)), where lmi is
recursively a lemma instance and each fi is an "instantiable" function
symbol of arity ni and gi is a function symbol or a pseudo-lambda
expression of arity ni.  An instantiable function symbol is any defined
or constrained function symbol except the primitives not, member,
implies, and o<, and a few others, as listed by the constant
*non-instantiable-primitives*.  These are built-in in such a way that we
cannot recover the constraints on them. A pseudo-lambda expression is an
expression of the form (lambda (v1 ... vn) body) where the vi are
distinct variable symbols and body is any term.  No a priori relation is
imposed between the vi and the variables of body, i.e., body may ignore
some vi's and may contain "free" variables.  However, we do not permit v
to occur freely in body if the functional substitution is to be applied
to any formula (lmi or the constraints to be satisfied) that contains v
as a variable.  This is our draconian restriction to avoid capture.  If
you happen to violate this restriction by choosing a v that does occur,
say in one of the relevant constraints, an informative error message
will be printed.  That message will list for you the illegal choices for
v in the context in which the functional substitution is offered.  A
:functional-instance lemma instance denotes the formula obtained by
functionally instantiating the formula denoted by lmi, replacing fi by
gi.  However, before such a lemma instance can be used, the system will
generate proof obligations arising from the replacement of the fi's by
the gi's in constraints that "support" the lemma to be functionally
instantiated; see CONSTRAINT.  One might expect that if the same
instantiated constraint were generated on behalf of several events, then
each of those instances would have to be proved.  However, for the sake
of efficiency, ACL2 stores the fact that such an instantiated constraint
has been proved and avoids it in future events.

Obscure case for definitions.  If the lemma instance refers to a
:definition rune, then it refers to the corollary formula of that rune,
which can be a simplified ("normalized") form of the original formula.
However, if the hint is a :by hint and the lemma instance is based on a
name (i.e., a symbol), rather than a rune, then the formula is the
original formula of the event, as shown by :pe, rather than the
normalized version, as shown by :pf.  This is as one would expect: If
you supply the name of an event, you expect it to refer to the original
event.  For :use hints we use the simplified (normalized) form instead,
which is reasonable since one would expect simplification during the
proof that re-traces the normalization done at the time the rule was
created.

See FUNCTIONAL-INSTANTIATION-EXAMPLE for an example of the use
of :functional-instance (so-called "functional instantiation)."

LINEAR-ARITHMETIC    A description of the linear arithmetic decision procedure

We describe the procedure very roughly here.  Fundamental to the
procedure is the notion of a linear polynomial inequality.  A "linear
polynomial" is a sum of terms, each of which is the product of a
rational constant and an "unknown."  The "unknown" is permitted to be 1
simply to allow a term in the sum to be constant.  Thus, an example
linear polynomial is 3*x + 7*a + 2; here x and a are the (interesting)
unknowns.  However, the unknowns need not be variable symbols.  For
example, (length x) might be used as an unknown in a linear polynomial.
Thus, another linear polynomial is 3*(length x) + 7*a.  A "linear
polynomial inequality" is an inequality (either < or <=) relation
between two linear polynomials.  Note that an equality may be considered
as a pair of inequalities; e.q., 3*x + 7*a + 2 = 0 is the same as the
conjunction of 3*x + 7*a + 2 <= 0 and 0 <= 3*x + 7*a + 2.

Certain linear polynomial inequalities can be combined by
cross-multiplication and addition to permit the deduction of a third
inequality with fewer unknowns.  If this deduced inequality is
manifestly false, a contradiction has been deduced from the assumed
inequalities.

For example, suppose we have two assumptions

     p1:       3*x + 7*a <  4
     p2:               3 <  2*x

and we wish to prove that, given p1 and p2, a < 0.  As suggested above,
we proceed by assuming the negation of our goal

     p3:               0 <= a.

and looking for a contradiction.

By cross-multiplying and adding the first two inequalities, (that is,
multiplying p1 by 2, p2 by 3 and adding the respective sides), we deduce
the intermediate result

     p4:  6*x + 14*a + 9 < 8 + 6*x

which, after cancellation, is:

     p4:        14*a + 1 <  0.

If we then cross-multiply and add p3 to p4, we get

     p5:               1 <= 0,

a contradiction.  Thus, we have proved that p1 and p2 imply the negation
of p3.

All of the unknowns of an inequality must be eliminated by cancellation
in order to produce a constant inequality.  We can choose to eliminate
the unknowns in any order, but we eliminate them in term-order, largest
unknowns first.  (See TERM-ORDER.)  That is, two polys are
cancelled against each other only when they have the same largest
unknown.  For instance, in the above example we see that x is the
largest unknown in each of p1 and p2, and a in p3 and p4.

Now suppose that this procedure does not produce a contradiction but
instead yields a set of nontrivial inequalities.  A contradiction might
still be deduced if we could add to the set some additional inequalities
allowing further cancellations.  That is where :linear lemmas come in.
When the set of inequalities has stabilized under cross-multiplication
and addition and no contradiction is produced, we search the data base
of :linear rules for rules about the unknowns that are candidates for
cancellation (i.e., are the largest unknowns in their respective
inequalities).  See LINEARfor a description of how :linear rules
are used.

See also non-linear-arithmetic for a description of an extension to the
linear-arithmetic procedure described here.

LOCAL-INCOMPATIBILITY    when non-local events won't replay in isolation

Sometimes a "local incompatibility" is reported while attempting to
embed some events, as in an encapsulate or include-book.  This is
generally due to the use of a locally defined name in a non-local event
or the failure to make a witnessing definition local.

local incompatibilities may be detected while trying to execute the
strictly non-local events of an embedding.  For example, encapsulate
operates by first executing all the events (local and non-local) with
ld-skip-proofsp nil, to confirm that they are all admissible.  Then it
attempts merely to assume the non-local ones to create the desired
theory, by executing the events with ld-skip-proofsp set to
'include-book.  Similarly, include-book assumes the non-local ones, with
the understanding that a previously successful certify-book has
performed the admissiblity check.

How can a sequence of events admitted with ld-skip-proofsp nil fail when
ld-skip-proofsp is 'include-book?  The key observation is that in the
latter case only the non-local events are processed.  The local ones are
skipped and so the non-local ones must not depend upon them.

Two typical mistakes are suggested by the detection of a local
incompatibility: (1) a locally defined function or macro was used in a
non-local event (and, in the case of encapsulate, was not included among
the signatures) and (2) the witnessing definition of a function that was
included among the signatures of an encapsulate was not made local.

An example of mistake (1) would be to include among your encapsulated
events both (local (defun fn ...)) and (defthm lemma (implies (fn ...)
...)).  Observe that fn is defined locally but a formula involving fn is
defined non-locally.  In this case, either the defthm should be made
local or the defun should be made non-local.

An example of mistake (2) would be to include (fn (x) t) among your
signatures and then to write (defun fn (x) ...) in your events, instead
of (local (defun fn ...)).

One subtle aspect of encapsulate is that if you constrain any member of
a mutually recursive clique you must define the entire clique locally
and then you must constrain those members of it you want axiomatized
non-locally.

Errors due to local incompatibility should never occur in the assumption
of a fully certified book.  Certification ensures against it.
Therefore, if include-book reports an incompatibility, we assert that
earlier in the processing of the include-book a warning was printed
advising you that some book was uncertified.  If this is not the case --
if include-book reports an incompatibility and there has been no prior
warning about lack of certification -- please report it to us.

When a local incompatibility is detected, we roll-back to the world in
which we started the encapsulate or include-book.  That is, we discard
the intermediate world created by trying to process the events skipping
proofs.  This is clean, but we realize it is very frustrating because
the entire sequence of events must be processed from scratch.  Assuming
that the embedded events were, once upon a time, processed as top-level
commands (after all, at some point you managed to create this sequence
of commands so that the local and non-local ones together could survive
a pass in which proofs were done), it stands to reason that we could
define a predicate that would determine then, before you attempted to
embed them, if local incompatibilities exist.  We hope to do that,
eventually.

We conclude with a subtle example of local incompatibility.  The problem
is that in order for foo-type-prescription to be admitted using the
specified :typed-term (foo x), the conclusion (my-natp (foo x)) depends
on my-natp being a compound-recognizer.  This is fine on the first pass
of the encapsulate, during which lemma my-natp-cr is admitted.  But
my-natp-cr is skipped on the second pass because it is marked local, and
this causes foo-type-prescription to fail on the second pass.

     (defun my-natp (x)
       (declare (xargs :guard t))
       (and (integerp x)
            (<= 0 x)))

     (defun foo (x)
       (nfix x))

     (encapsulate
      ()
      (local (defthm my-natp-cr
               (equal (my-natp x)
                      (and (integerp x)
                           (<= 0 x)))
               :rule-classes :compound-recognizer))
      (defthm foo-type-prescription
        (my-natp (foo x))
        :hints (("Goal" :in-theory (enable foo)))
        :rule-classes ((:type-prescription :typed-term (foo x)))))