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.

PSEUDO-TERMP    a predicate for recognizing term-like s-expressions

     Example Forms:
     (pseudo-termp '(car (cons x 'nil)))      ; has value t
     (pseudo-termp '(car x y z))              ; also has value t!
     (pseudo-termp '(delta (h x)))            ; has value t
     (pseudo-termp '(delta (h x) . 7))        ; has value nil (not a true-listp)
     (pseudo-termp '((lambda (x) (car x)) b)) ; has value t
     (pseudo-termp '(if x y 123))             ; has value nil (123 is not quoted)
     (pseudo-termp '(if x y '123))            ; has value t

If x is the quotation of a term, then (pseudo-termp x) is t.  However,
if x is not the quotation of a term it is not necessarily the case that
(pseudo-termp x) is nil.

See TERM for a discussion of the various meanings of the word
"term" in ACL2.  In its most strict sense, a term is either a legal
variable symbol, a quoted constant, or the application of an n-ary
function symbol or closed lambda-expression to n terms.  By "legal
variable symbol" we exclude constant symbols, such as t, nil, and
*ts-rational*.  By "quoted constants" we include 't (aka (quote t)),
'nil, '31, etc., and exclude constant names such as t, nil and
*ts-rational*, unquoted constants such as 31 or 1/2, and ill-formed
quote expressions such as (quote 3 4).  By "closed lambda expression" we
exclude expressions, such as (lambda (x) (cons x y)), containing free
variables in their bodies.  Terms typed by the user are translated into
strict terms for internal use in ACL2.

The predicate termp checks this strict sense of "term" with respect to a
given ACL2 logical world; See WORLD.  Many ACL2 functions, such
as the rewriter, require certain of their arguments to satisfy termp.
However, as of this writing, termp is in :program mode and thus cannot
be used effectively in conjectures to be proved.  Furthermore, if
regarded simply from the perspective of an effective guard for a
term-processing function, termp checks many irrelevant things.  (Does it
really matter that the variable symbols encountered never start and end
with an asterisk?)  For these reasons, we have introduced the notion of
a "pseudo-term" and embodied it in the predicate pseudo-termp, which is
easier to check, does not require the logical world as input, has :logic
mode, and is often perfectly suitable as a guard on term-processing
functions.

A pseudo-termp is either a symbol, a true list of length 2 beginning
with the word quote, the application of an n-ary pseudo-lambda
expression to a true list of n pseudo-terms, or the application of a
symbol to a true list of n pseudo-termps.  By an "n-ary pseudo-lambda
expression" we mean an expression of the form (lambda (v1 ... vn)
pterm), where the vi are symbols (but not necessarily distinct legal
variable symbols) and pterm is a pseudo-termp.

Metafunctions may use pseudo-termp as a guard.

READ-BYTE$    See IO.

READ-CHAR$    See IO.

READ-OBJECT    See IO.

REDEF    a common way to set ld-redefinition-action

     Example and General Form:
     ACL2 !>:redef

This command sets ld-redefinition-action to '(:query . :overwrite).

As explained elsewhere (see LD-REDEFINITION-ACTION), this allows
redefinition of functions and other events without undoing.  A query
will be made every time a redefinition is commanded; the user must
explicitly acknowledge that the redefinition is intentional.  It is
possible to set ld-redefinition-action so that the redefinition of
non-system functions occurs quietly.  See
LD-REDEFINITION-ACTION.

REDEF!    system hacker's redefinition command

     Example and General Form:
     ACL2 !>:redef!
     ACL2 p!>

This command sets ld-redefinition-action to '(:warn! . :overwrite) sets
the default defun-mode to :program, and invokes (set-state-ok t).

This is the ACL2 system hacker's redefinition command.  Note that even
system functions can be redefined with a mere warning.  Be careful!

REDEFINED-NAMES    to collect the names that have been redefined

     Example and General Forms:
     (redefined-names state)

This function collects names that have been redefined in the current
ACL2 state.  :Program mode functions that were reclassified to :logic
functions are not collected, since such reclassification cannot imperil
soundness because it is allowed only when the new and old definitions
are identical.

Thus, if (redefined-names state) returns nil then no unsafe definitions
have been made, regardless of ld-redefinition-action.  See
LD-REDEFINITION-ACTION.

REDUNDANT-EVENTS    allowing a name to be introduced "twice"

Sometimes an event will announce that it is "redundant".  When this
happens, no change to the logical world has occurred.  This happens when
the logical name being defined is already defined and has exactly the
same definition, from the logical point of view.  This feature permits
two independent books, each of which defines some name, to be included
sequentially provided they use exactly the same definition.

When are two logical-name definitions considered exactly the same?  It
depends upon the kind of name being defined.

A deflabel event is never redundant.  This means that if you have a
deflabel in a book and that book has been included (without error), then
references to that label denote the point in history at which the book
introduced the label.  See the note about shifting logical names, below.

A defun or mutual-recursion (or defuns) event is redundant if for each
function to be introduced, there has already been introduced a function
with the same name, the same formals, and syntactically identical guard,
type declarations, stobjs declarations and body (before macroexpansion),
and an appropriate mode (see the discussion of "appropriate modes"
below).  Exceptions: (1) If either definition is declared
:non-executable (see XARGS), then the two events must be
identical.  (2) It is permissible for one definition to have a :guard of
t and the other to have no explicit guard (hence, the guard is
implicitly t).

A verify-guards event is redundant if the function has already had its
guards verified.

A defaxiom or defthm event is redundant if there is already an axiom or
theorem of the given name and both the formula (after macroexpansion)
and the rule-classes are syntactically identical.  Note that a defaxiom
can make a subsequent defthm redundant, and a defthm can make a
subsequent defaxiom redundant as well.

A defconst is redundant if the name is already defined either with a
syntactically identical defconst event or one that defines it to have
the same value.

A defstobj is redundant if there is already a defstobj event with the
same name that has exactly the same field descriptors (see
DEFSTOBJ), in the same order, and with the same :renaming value if
:renaming is supplied for either event.

A defmacro is redundant if there is already a macro defined with the
same name and syntactically identical arguments, guard, and body.

A defpkg is redundant if a package of the same name with exactly the
same imports has been defined.

A deftheory is never redundant.  The "natural" notion of equivalent
deftheory forms is that the names and values of the two theory
expressions are the same.  But since most theory expressions are
sensitive to the context in which they occur, it seems unlikely to us
that two deftheorys coming from two sequentially included books will
ever have the same values.  So we prohibit redundant theory definitions.
If you try to define the same theory name twice, you will get a "name in
use" error.

An in-theory event is never redundant because it doesn't define any
name.

A push-untouchable event is redundant if every name supplied is already
a member of the untouchable symbols.

A set-body event is redundant if the indicated body is already the
current body.

Table and defdoc events are never redundant because they don't define
any name.

An encapsulate event is redundant if and only if a syntactically
identical encapsulate has already been executed under the same
default-defun-mode.

An include-book is redundant if the book has already been included.

See About Appropriate Modes,
guards,
types, stobjs, and bodies are identical.  When are the modes (:program
or :logic) "appropriate?"  Identical modes are appropriate.  But what if
the old mode was :program and the new mode is :logic?  This is
appropriate, provided the definition meets the requirements of the
logical definitional principle.  That is, you may redefine "redundantly"
a :program mode function as a :logic mode function provide the measure
conjectures can be proved.  This is what verify-termination does.  Now
consider the reverse style of redefinition.  Suppose the function was
defined in :logic mode and is being identically redefined in :program
mode.  This is inappropriate.  We do not permit the downgrading of a
function from :logic mode to :program mode, since that might produce a
logical world in which there were theorems about a :program mode
function, violating one of ACL2's basic assumptions.

See About Shifting Logical Names.
Consider the value of that theory expression in
two different sessions.  In session A, the book is included in a world
in which fn is not already defined, i.e., in a world in which the book's
definition of fn is not redundant.  In session B, the book is included
in a world in which fn is already identically defined.  In session B,
the book's definition of fn is redundant.  When fn is used as a logical
name in a theory expression, it denotes the point in history at which fn
was introduced.  Observe that those points are different in the two
sessions.  Hence, it is likely that theory expressions involving fn will
have different values in session A than in session B.

This may adversely affect the user of your book.  For example, suppose
your book creates a theory via deftheory that is advertised just to
contain the names generated by the book.  But suppose you compute the
theory as the very last event in the book using:

     (set-difference-theories (universal-theory :here)
                              (universal-theory fn))

where fn is the very first event in the book and happens to be a defun
event.  This expression returns the advertised set if fn is not already
defined when the book is included.  But if fn were previously
(identically) defined, the theory is larger than advertised.

The moral of this is simple: when building books that other people will
use, it is best to describe your theories in terms of logical names that
will not shift around when the books are included.  The best such names
are those created by deflabel.

See About Unfortunate Redundancies.
The following example shows how an attempt to
redefine a function can fail to make any change.

     (set-ld-redefinition-action '(:warn . :overwrite) state)
     (defmacro mac (x) x)
     (defun foo (x) (mac x))
     (defmacro mac (x) (list 'car x))
     (defun foo (x) (mac x)) ; redundant, unfortunately; foo does not change
     (thm (equal (foo 3) 3)) ; succeeds, showing that redef of foo didn't happen

The call of macro mac was expanded away when the first definition of foo
was processed, so the new definition of mac is not seen in foo unless
foo is redefined; yet our attempt at redefinition failed!  An easy
workaround is first to supply a different definition of foo, just before
the last definition of foo above.  Then that final definition will no
longer be redundant.

The phenomenon illustrated above can occur even without macros.  Here is
a more complex example, based on one supplied by Grant Passmore.

     (defun n3 () 0)
     (defun n4 () 1)
     (defun n5 () (> (n3) (n4))) ; body is normalized to nil
     (thm (equal (n5) nil)) ; succeeds, trivially
     (set-ld-redefinition-action '(:warn . :overwrite) state)
     (defun n3 () 2)

If now we execute (thm (equal (n5) nil)), it still succeeds even though
we expect (n5) = (> (n3) (n4)) = (> 2 1) = t.  That is because the body
of n5 was normalized to nil.  (Such normalization can be avoided; see
the brief discussion of :normalize in the documentation for defun.)  So,
given this unfortunate situation, one might expect at this point simply
to redefine n5 using the same definition as before, in order to pick up
the new definition of n3.  Such "redefinition" would, however, be
redundant, for the same reason as in the previous example: no syntactic
change was made to the definition.  The same workaround applies as
before: redefine n5 to be something different, and then redefine n5
again to be as desired.

A related phenomenon can occur for encapsulate.  As explained above, an
encapsulate event is redundant if it is identical to one already in the
database.  Consider then the following contrived example.

     (encapsulate () (defun foo (x) x))
     (set-ld-redefinition-action '(:warn . :overwrite) state)
     (defun foo (x) (cons x x))
     (encapsulate () (defun foo (x) x)) ; redundant!

The last encapsulate event is redundant because it meets the criterion
for redundancy: it is identical to the earlier encapsulate event.  A
workaround can be to add something trivial to the encapsulate, for
example:

     (encapsulate ()
       (deflabel try2) ; "Increment" to try3 next time, and so on.
       (defun foo (x) x))

The examples above are suggestive but by no means exhaustive.  Consider
the following example.

     (defstub f1 () => *)
     (set-ld-redefinition-action '(:warn . :overwrite) state)
     (defun f1 () 3)
     (defstub f1 () => *) ; redundant -- has no effect

The reason that the final defstub is redundant is that defstub is a
macro that expands to a call of encapsulate; so this is very similar to
the immediately preceding example.

RESTRICT    hints keyword :RESTRICT

See HINTS.

REWRITE-STACK-LIMIT    limiting the stack depth of the ACL2 rewriter

ACL2 users can create rules of class :rewrite (see RULE-CLASSES)
that have the potential of causing an infinite loop in the ACL2
rewriter.  This could lead to Lisp stack overflows and even segmentation
faults.  For this reason, the depth of certain calls of functions in the
ACL2 rewriter is limited by default using the value of the form
(rewrite-stack-limit (w state)).  To see the limit in action, execute
the following forms.

     (defthm app-assoc-1
       (equal (append (append x y) z)
              (append x y z)))
     (defthm app-assoc-2
       (equal (append x y z)
              (append (append x y) z)))
     (thm (equal (append a b c) xxx)
          ; try without these hints to see a slightly different error message
          :hints (("Goal" :do-not '(preprocess))))

The ensuing error message shows a stack of one greater than the value of
(rewrite-stack-limit (w state)), which by default is the value of the
constant *default-rewrite-stack-limit*.  The error message also explains
how to use :brr t and (cw-gstack) to find looping rewrite rules.

This limit can be changed; see SET-REWRITE-STACK-LIMIT.

For a related limit, see BACKCHAIN-LIMIT.

SAVING-AND-RESTORING    saving and restoring your logical state

One normally works on an ACL2-based project by developing books, which
can then be included when continuing on that project in later ACL2
sessions; see INCLUDE-BOOK.  However, this approach can be
time-consuming when there are very large collections of books to be
included.  See see SAVE-EXECfor the description of a utility
that saves your ACL2 state so that you can immediately re-start later in
that same state.

SHOW-BODIES    show the potential definition bodies

     Examples:
     (show-bodies foo)
     :show-bodies foo

A definition installs a so-called "body" of a function symbol, as do
certain :definition rules.  Such bodies are used in a number of ways,
including the application of :expand hints; see DEFINITION, in
particular the discussion of "body" there, and see HINTS for a
discussion of the :expand hint.  Also see SET-BODY for how to
change which of the available definitions (among the original definition
and appropriate :definition rules) is the one that provides the body.
The show-bodies command displays the available such bodies in an
appropriate format, starting with the one that is currently used as the
body.

     General Forms:
     (show-bodies function-symbol)
     :show-bodies function-symbol

SIGNATURE    how to specify the arity of a constrained function

     Examples:
     ((hd *) => *)
     ((printer * state) => (mv * * state))
     ((mach * mach-state * state) => (mv * mach-state)

     General Form:
     ((fn ...) => *)
     ((fn ...) => stobj)
     or
     ((fn ...) => (mv ...))

where fn is the constrained function symbol, ... is a list of asterisks
and/or the names of single-threaded objects and stobj is a
single-threaded object name.  ACL2 also supports an older style of
signature described below after we describe the preferred style.

Signatures specify three syntactic aspects of a function symbol: (1) the
"arity" or how many arguments the function takes, (2) the "multiplicity"
or how many results it returns via MV, and (3) which of those arguments
and results are single-threaded objects and which objects they are.

For a discussion of single-threaded objects, see STOBJ.  For the
current purposes it is sufficient to know that every single- threaded
object has a unique symbolic name and that state is the name of the only
built-in single-threaded object.  All other stobjs are introduced by the
user via defstobj.  An object that is not a single-threaded object is
said to be "ordinary."

The general form of a signature is ((fn x1 ... xn) => val).  So a
signature has two parts, separated by the symbol "=>".  The first part,
(fn x1 ... xn), is suggestive of a call of the constrained function.
The number of "arguments," n, indicates the arity of fn.  Each xi must
be a symbol.  If a given xi is the symbol "*" then the corresponding
argument must be ordinary.  If a given xi is any other symbol, that
symbol must be the name of a single-threaded object and the
corresponding argument must be that object.  No stobj name may occur
twice among the xi.

The second part, val, of a signature is suggestive of a term and
indicates the "shape" of the output of fn.  If val is a symbol then it
must be either the symbol "*" or the name of a single-threaded object.
In either case, the multiplicity of fn is 1 and val indicates whether
the result is ordinary or a stobj.  Otherwise, val is of the form (mv y1
... yk), where k > 1.  Each yi must be either the symbol "*" or the name
of a stobj.  Such a val indicates that fn has multiplicity k and the yi
indicate which results are ordinary and which are stobjs.  No stobj name
may occur twice among the yi.

Finally, a stobj name may appear in val only if appears among the xi.

Before ACL2 supported user-declared single-threaded objects there was
only one single-threaded object: ACL2's built-in notion of state.  The
notion of signature supported then gave a special role to the symbol
state and all other symbols were considered to denote ordinary objects.
ACL2 still supports the old form of signature, but it is limited to
functions that operate on ordinary objects or ordinary objects and
state.

     Old-Style General Form:
     (fn formals result)

where fn is the constrained function symbol, formals is a suitable list
of formal parameters for it, and result is either a symbol denoting that
the function returns one result or else result is an mv expression, (mv
s1 ... sn), where n>1, each si is a symbol, indicating that the function
returns n results.  At most one of the formals may be the symbol STATE,
indicating that corresponding argument must be ACL2's built-in state.
If state appears in formals then state may appear once in result.  All
"variable symbols" other than state in old style signatures denote
ordinary objects, regardless of whether the symbol has been defined to
be a single-threaded object name!

We also support a variation on old style signatures allowing the user to
declare which symbols (besides state) are to be considered
single-threaded object names.  This form is

     (fn formals result :stobjs names)

where names is either the name of a single-threaded object or else is a
list of such names.  Every name in names must have been previously
defined as a stobj via defstobj.

SIMPLE    :definition and :rewrite rules used in preprocessing

     Example of simple rewrite rule:
     (equal (car (cons x y)) x)

     Examples of simple definition:
     (defun file-clock-p (x) (integerp x))
     (defun naturalp (x)
       (and (integerp x) (>= x 0)))

The theorem prover output sometimes refers to "simple" definitions and
rewrite rules.  These rules can be used by the preprocessor, which is
one of the theorem prover's "processes" understood by the :do-not hint;
see HINTS.

The preprocessor expands certain definitions and uses certain rewrite
rules that it considers to be "fast".  There are two ways to qualify as
fast.  One is to be an "abbreviation", where a rewrite rule with no
hypotheses or loop stopper is an "abbreviation" if the right side
contains no more variable occurrences than the left side, and the right
side does not call the functions if, not or implies.  Definitions and
rewrite rules can both be abbreviations; the criterion for definitions
is similar, except that the definition must not be recursive.  The other
way to qualify applies only to a non-recursive definition, and applies
when its body is a disjunction or conjunction, according to a perhaps
subtle criterion that is intended to avoid case splits.

SPECIOUS-SIMPLIFICATION    nonproductive proof steps

Occasionally the ACL2 theorem prover reports that the current goal
simplifies to itself or to a set including itself.  Such simplifications
are said to be "specious" and are ignored in the sense that the theorem
prover acts as though no simplification were possible and tries the next
available proof technique.  Specious simplifications are almost always
caused by forcing.

The simplification of a formula proceeds primarily by the local
application of :rewrite, :type-prescription, and other rules to its
various subterms.  If no rewrite rules apply, the formula cannot be
simplified and is passed to the next ACL2 proof technique, which is
generally the elimination of destructors.  The experienced ACL2 user
pays special attention to such "maximally simplified" formulas; the
presence of unexpected terms in them indicates the need for additional
rules or the presence of some conflict that prevents existing rules from
working harmoniously together.

However, consider the following interesting possibility: local rewrite
rules apply but, when applied, reproduce the goal as one of its own
subgoals.  How can rewrite rules apply and reproduce the goal?  Of
course, one way is for one rule application to undo the effect of
another, as when commutativity is applied twice in succession to the
same term.  Another kind of example is when two rules conflict and
undermine each other.  For example, under suitable hypotheses, (length
x) might be rewritten to (+ 1 (length (cdr x))) by the :definition of
length and then a :rewrite rule might be used to "fold" that back to
(length x).  Generally speaking the presence of such "looping" rewrite
rules causes ACL2's simplifier either to stop gracefully because of
heuristics such as that described in the documentation for loop-stopper
or to cause a stack overflow because of indefinite recursion.

A more insidious kind of loop can be imagined: two rewrites in different
parts of the formula undo each other's effects "at a distance," that is,
without ever being applied to one another's output.  For example,
perhaps the first hypothesis of the formula is simplified to the second,
but then the second is simplified to the first, so that the end result
is a formula propositionally equivalent to the original one but with the
two hypotheses commuted.  This is thought to be impossible unless
forcing or case-splitting occurs, but if those features are exploited
(see FORCE and see CASE-SPLIT) it can be made to happen
relatively easily.

Here is a simple example.  Declare foo to be a function of one argument
returning one result:

     (defstub p1 (x) t)

Prove the following silly rule:

     (defthm bad
       (implies (case-split (p1 x))
                (p1 x)))

Now suppose we try the following.

     (thm (p1 x))

The rewrite rule bad will rewrite (p1 x) to t, but it will be unable to
prove the hypothesis (case-split (p1 x)).  As a result, the prover will
spawn a new goal, to prove (p1 x).  However, since this new goal is the
same as the original goal, ACL2 will recognize the simplification as
*specious* and consider the attempted simplification to have failed.

In other words, despite the rewriting, no progress was made!  In more
common cases, the original goal may simplify to a set of subgoals, one
of which includes the original goal.

If ACL2 were to adopt the new set of subgoals, it would loop
indefinitely.  Therefore, it checks whether the input goal is a member
of the output subgoals.  If so, it announces that the simplification is
"specious" and pretends that no simplification occurred.

"Maximally simplified" formulas that produce specious simplifications
are maximally simplified in a very technical sense: were ACL2 to apply
every applicable rule to them, no progress would be made.  Since ACL2
can only apply every applicable rule, it cannot make further progress
with the formula.  But the informed user can perhaps identify some rule
that should not be applied and make it inapplicable by disabling it,
allowing the simplifier to apply all the others and thus make progress.

When specious simplifications are a problem it might be helpful to
disable all forcing (including case-splits) and resubmit the formula to
observe whether forcing is involved in the loop or not.  See
FORCE.  The commands

     ACL2 !>:disable-forcing
     and
     ACL2 !>:enable-forcing

disable and enable the pragmatic effects of both force and case-split.
If the loop is broken when forcing is disabled, then it is very likely
some forced hypothesis of some rule is "undoing" a prior simplification.
The most common cause of this is when we force a hypothesis that is
actually false but whose falsity is somehow temporarily hidden (more
below).  To find the offending rule, compare the specious simplification
with its non-specious counterpart and look for rules that were
speciously applied that are not applied in the non-specious case.  Most
likely you will find at least one such rule and it will have a forced
hypothesis.  By disabling that rule, at least for the subgoal in
question, you may allow the simplifier to make progress on the subgoal.

STATE    the von Neumannesque ACL2 state object

The ACL2 state object is used extensively in programming the ACL2
system, and has been used in other ACL2 programs as well.  However, most
users, especially those interested in specification and verification (as
opposed to programming per se), need not be aware of the role of the
state object in ACL2, and will not write functions that use it
explicitly.  We say more about this point at the end of this
documentation topic.

The ACL2 state object is an example of a single-threaded object or
stobj.  ACL2 allows the user to define new single-threaded objects.
Generally, ACL2 may need to access the ACL2 state but should not
(cannot) change it except via a certain set of approved functions such
as defun and defthm.  If you need a state-like object to which you have
complete rights, you may want a stobj.

Key to the idea of our state is the notion of single-threadedness.  For
an explanation, see STOBJ.  The upshot of it is that state is a
variable symbol with severe restrictions on its use, so that it can be
passed into only certain functions in certain slots, and must be
returned by those functions that "modify" it.  Henceforth, we do not
discuss single-threaded objects in general (which the user can introduce
with defstobj) but one in particular, namely ACL2's state object.

The global table is perhaps the most visible portion of the state
object.  Using the interface functions @ and assign, a user may bind
global variables to the results of function evaluations (much as an
Nqthm user exploits the Nqthm utility r-loop).  See @, and
see ASSIGN.

ACL2 supports several facilities of a truly von Neumannesque state
machine character, including file io and global variables.  Logically
speaking, the state is a true list of the 14 components described below.
There is a "current" state object at the top-level of the ACL2 command
loop.  This object is understood to be the value of what would otherwise
be the free variable state appearing in top-level input.  When any
command returns a state object as one of its values, that object becomes
the new current state.  But ACL2 provides von Neumann style speed for
state operations by maintaining only one physical (as opposed to
logical) state object.  Operations on the state are in fact destructive.
This implementation does not violate the applicative semantics because
we enforce certain draconian syntactic rules regarding the use of state
objects.  For example, one cannot "hold on" to an old state, access the
components of a state arbitrarily, or "modify" a state object without
passing it on to subsequent state-sensitive functions.

Every routine that uses the state facilities (e.g. does io, or calls a
routine that does io), must be passed a "state object." And a routine
must return a state object if the routine modifies the state in any way.
Rigid syntactic rules governing the use of state objects are enforced by
the function translate, through which all ACL2 user input first passes.
State objects can only be "held" in the formal parameter state, never in
any other formal parameter and never in any structure (excepting a
multiple-value return list field which is always a state object).  State
objects can only be accessed with the primitives we specifically permit.
Thus, for example, one cannot ask, in code to be executed, for the
length of state or the car of state.  In the statement and proof of
theorems, there are no syntactic rules prohibiting arbitrary treatment
of state objects.

Logically speaking, a state object is a true list whose members are as
follows:

     Open-input-channels, an alist with keys that are symbols in package
     "ACL2-INPUT-CHANNEL".  The value (cdr) of each pair has the form
     ((:header type file-name open-time) . elements), where type is one
     of :character, :byte, or :object and elements is a list of things
     of the corresponding type, i.e. characters, integers of type (mod
     255), or lisp objects in our theory.  File-name is a string.
     Open-time is an integer.  See IO.

     Open-output-channels, an alist with keys that are symbols in
     package "ACL2-OUTPUT-CHANNEL".  The value of a pair has the form
     ((:header type file-name open-time) .  current-contents).  See
     IO.

     Global-table, an alist associating symbols (to be used as "global
     variables") with values.  See @, and see
     ASSIGN.

     T-stack, a list of arbitrary objects accessed and changed by the
     functions aref-t-stack and aset-t-stack.

     32-bit-integer-stack, a list of arbitrary 32-bit-integers accessed
     and changed by the functions aref-32-bit-integer-stack and
     aset-32-bit-integer-stack.

     Big-clock-entry, an integer, that is used logically to bound the
     amount of effort spent to evaluate a quoted form.

     Idates, a list of dates and times, used to implement the function
     print-current-idate, which prints the date and time.

     Run-times, a list of integers, used to implement the functions that
     let ACL2 report how much time was used, but inaccessible to the
     user.

     File-clock, an integer that is increased on every file opening and
     closing, and on each call of sys-call, and is used to maintain the
     consistency of the io primitives.

     Readable-files, an alist whose keys have the form (string type
     time), where string is a file name and time is an integer.  The
     value associated with such a key is a list of characters, bytes, or
     objects, according to type.  The time field is used in the
     following way: when it comes time to open a file for input, we will
     only look for a file of the specified name and type whose time
     field is that of file-clock.  This permits us to have a
     "probe-file" aspect to open-file: one can ask for a file, find it
     does not exist, but come back later and find that it does now
     exist.

     Written-files, an alist whose keys have the form (string type time1
     time2), where string is a file name, type is one of :character,
     :byte or :object, and time1 and time2 are integers.  Time1 and
     time2 correspond to the file-clock time at which the channel for
     the file was opened and closed.  This field is write-only; the only
     operation that affects this field is close-output-channel, which
     conses a new entry on the front.

     Read-files, a list of the form (string type time1 time2), where
     string is a file name and time1 and time2 were the times at which
     the file was opened for reading and closed.  This field is write
     only.

     Writeable-files, an alist whose keys have the form (string type
     time).  To open a file for output, we require that the name, type,
     and time be on this list.

     List-all-package-names-lst, a list of true-listps.  Roughly
     speaking, the car of this list is the list of all package names
     known to this Common Lisp right now and the cdr of this list is the
     value of this state variable after you look at its car.  The
     function, list-all-package-names, which takes the state as an
     argument, returns the car and cdrs the list (returning a new state
     too).  This essentially gives ACL2 access to what is provided by
     CLTL's list-all-packages.  Defpkg uses this feature to ensure that
     the about-to-be-created package is new in this lisp.  Thus, for
     example, in akcl it is impossible to create the package "COMPILER"
     with defpkg because it is on the list, while in Lucid that package
     name is not initially on the list.

     User-stobj-alist, an alist which associates user-defined
     single-threaded objects (see STOBJ) with their values.

We recommend avoiding the use of the state object when writing ACL2 code
intended to be used as a formal model of some system, for several
reasons.  First, the state object is complicated and contains many
components that are oriented toward implementation and are likely to be
irrelevant to the model in question.  Second, there is currently not
much support for reasoning about ACL2 functions that manipulate the
state object, beyond their logical definitions.  Third, the
documentation about state is not as complete as one might wish.

User-defined single-threaded objects offer the speed of state while
giving the user complete access to all the fields.  See STOBJ.

STOBJS    xargs keyword :STOBJS

See XARGS.

SUBVERSIVE-INDUCTIONS    why we restrict encapsulated recursive functions

See SUBVERSIVE-RECURSIONS.

SUBVERSIVE-RECURSIONS    why we restrict encapsulated recursive functions

Subtleties arise when one of the "constrained" functions, f, introduced
in the signature of an encapsulate event, is involved in the termination
argument for a non-local recursively defined function, g, in that
encapsulate.  During the processing of the encapsulated events, f is
locally defined to be some witness function, f'.  Properties of f' are
explicitly proved and exported from the encapsulate as the constraints
on the undefined function f.  But if f is used in a recursive g defined
within the encapsulate, then the termination proof for g may use
properties of f' -- the witness -- that are not explicitly set forth in
the constraints stated for f.

Such recursive g are said be "subversive" because if naively treated
they give rise to unsound induction schemes or (via functional
instantiation) recurrence equations that are impossible to satisfy.  We
illustrate what could go wrong below.

Subversive recursions are not banned outright.  Instead, they are
treated as part of the constraint.  That is, in the case above, the
definitional equation for g becomes one of the constraints on f.  This
is generally a severe restriction on future functional instantiations of
f.  In addition, ACL2 removes from its knowledge of g any suggestions
about legal inductions to "unwind" its recursion.

What should you do?  Often, the simplest response is to move the
offending recursive definition, e.g., g, out of the encapsulate.  That
is, introduce f by constraint and then define g as an "independent"
event.  You may need to constrain "additional" properties of f in order
to admit g, e.g., constrain it to reduce some ordinal measure.  However,
by separating the introduction of f from the admission of g you will
clearly identify the necessary constraints on f, functional
instantiations of f will be simpler, and g will be a useful function
which suggests inductions to the theorem prover.

Note that the functions introduced in the signature should not even
occur ancestrally in the termination proofs for non-local recursive
functions in the encapsulate.  That is, the constrained functions of an
encapsulate should not be reachable in the dependency graph of the
functions used in the termination arguments of recursive functions in
encapsulate.  If they are reachable, their definitions become part of
the constraints.

The following event illustrates the problem posed by subversive
recursions.

     (encapsulate (((f *) => *))
       (local (defun f (x) (cdr x)))
       (defun g (x)
         (if (consp x) (not (g (f x))) t)))

Suppose, contrary to how ACL2 works, that the encapsulate above were to
introduce no constraints on f on the bogus grounds that the only use of
f in the encapsulate is in an admissible function.  We discuss the
plausibility of this bogus argument in a moment.

Then it would be possible to prove the theorem:

     (defthm f-not-identity
       (not (equal (f '(a . b)) '(a . b)))
       :rule-classes nil
       :hints (("Goal" :use (:instance g (x '(a . b))))))

simply by observing that if (f '(a . b)) were '(a . b), then (g '(a
. b)) would be (not (g '(a . b))), which is impossible.

But then we could functionally instantiate f-not-identity, replacing f
by the identity function, to prove nil!  This is bad.

     (defthm bad
       nil
       :rule-classes nil
       :hints
       (("Goal" :use (:functional-instance f-not-identity (f identity)))))

This sequence of events was legal in versions of ACL2 prior to Version
1.5.  When we realized the problem we took steps to make it illegal.
However, our steps were insufficient and it was possible to sneak in a
subversive function (via mutual recursion) as late as Version 2.3.

We now turn to the plausibility of the bogus argument above.  Why might
one even be tempted to think that the definition of g above poses no
constraint on f?  Here is a very similar encapsulate.

     (encapsulate (((f *) => *))
       (local (defun f (x) (cdr x)))
       (defun map (x)
         (if (consp x)
             (cons (f x) (map (cdr x)))
           nil)))

Here map plays the role of g above.  Like g, map calls the constrained
function f.  But map truly does not constrain f.  In particular, the
definition of map could be moved "out" of the encapsulate so that map is
introduced afterwards.  The difference between map and g is that the
constrained function plays no role in the termination argument for the
one but does for the other.

As a "user-friendly" gesture, ACL2 implicitly moves map-like functions
out of encapsulations; logically speaking, they are introduced after the
encapsulation.  This simplifies the constraint.  This is done only for
"top-level" encapsulations.  When an encapsulate containing a non-empty
signature list is embedded in another encapsulate with a non-empty
signature list, no attempt is made to move map-like functions out.  The
user is advised, via the "infected" warning, to phrase the encapsulation
in the simplest way possible.

The lingering bug between Versions 1.5 and 2.3 mentioned above was due
to our failure to detect the g-like nature of some functions when they
were defined in mutually recursively cliques with other functions.  The
singly recursive case was recognized.  The bug arose because our
detection "algorithm" was based on the "suggested inductions" left
behind by successful definitions.  We failed to recall that
mutually-recursive definitions do not, as of this writing, make any
suggestions about inductions and so did not leave any traces of their
subversive natures.

SYNTAX    the syntax of ACL2 is that of Common Lisp

For the details of ACL2 syntax, see CLTL.  For examples of ACL2 syntax,
use :pe to print some of the ACL2 system code.  For example:

     :pe assoc-equal
     :pe dumb-occur
     :pe var-fn-count
     :pe add-linear-variable-to-alist

There is no comprehensive description of the ACL2 syntax yet, except
that found in CLTL.  Also see TERM.

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

     Example:
     Consider the :REWRITE rule created from

     (IMPLIES (SYNTAXP (NOT (AND (CONSP X)
                                 (EQ (CAR X) 'NORM))))
              (EQUAL (LXD X)
                     (LXD (NORM X)))).

The syntaxp hypothesis in this rule will allow the rule to be applied to
(lxd (trn a b)) but will not allow it to be applied to (lxd (norm a)).

     General Form:
     (SYNTAXP test)

Syntaxp always returns t and so may be added as a vacuous hypothesis.
However, when relieving the hypothesis, the test "inside" the syntaxp
form is actually treated as a meta-level proposition about the proposed
instantiation of the rule's variables and that proposition must evaluate
to true (non-nil) to "establish" the syntaxp hypothesis.

Note that the test of a syntaxp hypothesis does not, in general, deal
with the meaning or semantics or values of the terms, but rather with
their syntactic forms.  In the example above, the syntaxp hypothesis
allows the rule to be applied to every target of the form (lxd u),
provided u is not of the form (norm v).  Observe that without this
syntactic restriction the rule above could loop producing a sequence of
increasingly complex targets (lxd a), (lxd (norm a)), (lxd (norm (norm
a))), etc.  An intuitive reading of the rule might be "norm the argument
of lxd unless it has already been normed."

Note also that a syntaxp hypothesis deals with the syntactic form used
internally by ACL2, rather than that seen by the user.  In some cases
these are the same, but there can be subtle differences with which the
writer of a syntaxp hypothesis must be aware.  You can use :trans to
display this internal representation.

There are two types of syntaxp hypotheses.  The simpler type of syntaxp
hypothesis may be used as the nth hypothesis in a :rewrite or :linear
rule whose :corollary is (implies (and hyp1 ... hypn ... hypk) (equiv
lhs rhs)) provided test is a term, test contains at least one variable,
and every variable occuring freely in test occurs freely in lhs or in
some hypi, i<n.  In addition, test must not use any stobjs.  The case of
:meta rules is similar to the above, except that it applies to the
result of applying the hypothesis metafunction.  (Later below we will
describe the second type, an *extended* syntaxp hypothesis, which may
use state.)

We illustrate the use of simple syntaxp hypotheses by slightly
elaborating the example given above.  Consider a :rewrite rule whose
:corollary is:

     (IMPLIES (AND (RATIONALP X)
                   (SYNTAXP (NOT (AND (CONSP X)
                                      (EQ (CAR X) 'NORM)))))
              (EQUAL (LXD X)
                     (LXD (NORM X))))

How is this rule applied to (lxd (trn a b))?  First, we form a
substitution that instantiates the left-hand side of the conclusion of
the rule so that it is identical to the target term.  In the present
case, the substitution replaces x with (trn a b).

     (LXD X) ==> (LXD (trn a b)).

Then we backchain to establish the hypotheses, in order.  Ordinarily
this means that we instantiate each hypothesis with our substitution and
then attempt to rewrite the resulting instance to true.  Thus, in order
to relieve the first hypothesis above, we rewrite

     (RATIONALP (trn a b)).

If this rewrites to true, we continue.

Of course, most users are aware of some exceptions to this general
description of the way we relieve hypotheses.  For example, if a
hypothesis contains a "free-variable" -- one not bound by the current
substitution -- we attempt to extend the substitution by searching for
an instance of the hypothesis among known truths.  See
FREE-VARIABLES.  Forced hypotheses are another exception to the
general rule of how hypotheses are relieved.

Hypotheses marked with syntaxp, as in (syntaxp test), are also
exceptions.  We instantiate such a hypothesis; but instead of rewriting
the instantiated instance, we evaluate the instantiated test.  More
precisely, we evaluate test in an environment in which its variable
symbols are bound to the quotations of the terms to which those
variables are bound in the instantiating substitution.  So in the case
in point, we (in essence) evaluate

     (NOT (AND (CONSP '(trn a b)) (EQ (CAR '(trn a b)) 'NORM))).

This clearly evaluates to t.  When a syntaxp test evaluates to true, we
consider the syntaxp hypothesis to have been established; this is sound
because logically (syntaxp test) is t regardless of test.  If the test
evaluates to nil (or fails to evaluate because of guard violations) we
act as though we cannot establish the hypothesis and abandon the attempt
to apply the rule; it is always sound to give up.

The acute reader will have noticed something odd about the form

     (NOT (AND (CONSP '(trn a b)) (EQ (CAR '(trn a b)) 'NORM))).

When relieving the first hypothesis, (RATIONALP X), we substituted (trn
a b) for X; but when relieving the second hypothesis, (SYNTAXP (NOT (AND
(CONSP X) (EQ (CAR X) 'NORM)))), we substituted the quotation of (trn a
b) for X.  Why the difference?  Remember that in the first hypothesis we
are talking about the value of (trn a b) -- is it rational -- while in
the second one we are talking about its syntactic form.  Remember also
that Lisp, and hence ACL2, evaluates the arguments to a function before
applying the function to the resulting values. Thus, we are asking "Is
the list (trn a b) a consp and if so, is its car the symbol NORM?"  The
quotes on both (trn a b) and NORM are therefore necesary.  One can
verify this by defining trn to be, say cons, and then evaluating forms
such as

     (AND (CONSP '(trn a b)) (EQ (CAR '(trn a b)) 'NORM))
     (AND (CONSP (trn a b)) (EQ (CAR (trn a b)) NORM))
     (AND (CONSP (trn 'a 'b)) (EQ (CAR (trn 'a 'b)) NORM))
     (AND (CONSP '(trn a b)) (EQ '(CAR (trn a b)) "NORM))

at the top-level ACL2 prompt.

See SYNTAXP-EXAMPLES for more examples of the use of syntaxp.

An extended syntaxp hypothesis is similar to the simple type described
above, but it uses two additional variables, mfc and state, which must
not be bound by the left hand side or an earlier hypothesis of the rule.
They must be the last two variables mentioned by form; first mfc, then
state.  These two variables give access to the functions mfc-xxx; see
EXTENDED-METAFUNCTIONS.  As described there, mfc is bound to the
so-called metafunction-context and state to ACL2's state.  See
SYNTAXP-EXAMPLES for an example of the use of these extended syntaxp
hypotheses.