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

PROOF-OF-WELL-FOUNDEDNESS    a proof that o< is well-founded on o-ps

The soundness of ACL2 rests in part on the well-foundedness of o< on
o-ps.  This can be taken as obvious if one is willing to grant that
those concepts are simply encodings of the standard mathematical
notions of the ordinals below epsilon-0 and its natural ordering
relation.  But it is possible to prove that o< is well-founded on o-ps
without having to assert any connection to the ordinals and that is
what we do here.  The book books/ordinals/proof-of-well-foundedness
carries out the proof outlined below in ACL2, using only that the
natural numbers are well-founded.

Before outlining the above mentioned proof, we note that in the
analogous documentation page of ACL2 Version_2.7, there is a proof of
the well-foundedness of e0-ord-< on e0-ordinalps, the less-than relation
and recognizer for the old ordinals (that is, for the ordinals
appearing in ACL2 up through that version).  Manolios and Vroon have
given a proof in ACL2 Version_2.7 that the current ordinals (based on
o< and o-p) are order-isomorphic to the old ordinals (based on e0-ord-<
and e0-ordinalp).  Their proof establishes that switching from the old
ordinals to the current ordinals preserves the soundness of ACL2.  For
details see their paper:

     Manolios, Panagiotis & Vroon, Daron.
     Ordinal arithmetic in ACL2.
     Kaufmann, Matt, & Moore, J Strother (eds).
     Fourth International Workshop on the ACL2 Theorem
     Prover and Its Applications (ACL2-2003),
     July, 2003.
     See URL http://www.cs.utexas.edu/users/moore/acl2/workshop-2003/.

We now give an outline of the above mentioned proof of
well-foundedness.  We first observe three facts about o< on ordinals
that have been proved by ACL2 using only structural induction on lists.
These theorems can be proved by hand.

     (defthm transitivity-of-o<
       (implies (and (o< x y)
                     (o< y z))
                (o< x z))
       :rule-classes nil)

     (defthm non-circularity-of-o<
       (implies (o< x y)
                (not (o< y x)))
       :rule-classes nil)

     (defthm trichotomy-of-o<
       (implies (and (o-p x)
                     (o-p y))
                (or (equal x y)
                    (o< x y)
                    (o< y x)))
       :rule-classes nil)

These three properties establish that o< orders the o-ps.  To put such
a statement in the most standard mathematical nomenclature, we can
define the macro:

     (defmacro o<= (x y)
       `(not (o< ,y ,x)))

and then establish that o<= is a relation that is a simple, complete
(i.e., total) order on ordinals by the following three lemmas, which
have been proved:

     (defthm antisymmetry-of-o<=
       (implies (and (o-p x)
                     (o-p y)
                     (o<= x y)
                     (o<= y x))
                (equal x y))
       :rule-classes nil
       :hints (("Goal" :use non-circularity-of-o<)))

     (defthm transitivity-of-o<=
       (implies (and (o-p x)
                     (o-p y)
                     (o<= x y)
                     (o<= y z))
                (o<= x z))
       :rule-classes nil
       :hints (("Goal" :use transitivity-of-o<)))

     (defthm trichotomy-of-o<=
       (implies (and (o-p x)
                     (o-p y))
                (or (o<= x y)
                    (o<= y x)))
       :rule-classes nil
       :hints (("Goal" :use trichotomy-of-o<)))

Crucially important to the proof of the well-foundedness of o< on o-ps
is the concept of ordinal-depth, abbreviated od:

     (defun od (l)
       (if (o-finp l)
           0
         (1+ (od (o-first-expt l)))))

If the od of an o-p x is smaller than that of an o-p y, then x is o< y:

     (defun od-1 (x y)
       (if (o-finp x)
           (list x y)
         (od-1 (o-first-expt x) (o-first-expt y))))

     (defthm od-implies-ordlessp
       (implies (and (o-p x)
                     (< (od x) (od y)))
                (o< x y))
       :hints (("Goal"
                :induct (od-1 x y))))

Remark.  A consequence of this lemma is the fact that if s = s(1),
s(2), ... is an infinite, o< descending sequence of o-ps, then
od(s(1)), od(s(2)), ... is a "weakly" descending sequence of
non-negative integers: od(s(i)) is greater than or equal to od(s(i+1)).

_Lemma Main._  For each non-negative integer n, o< well-orders the set
of o-ps with od less than or equal to n .

      Base Case.  n = 0.  The o-ps with 0 od are the non-negative
      integers.  On the non-negative integers, o< is the same as <.

      Induction Step.  n > 0.  We assume that o< well-orders the
      o-ps with od less than n.

        If o< does not well-order the o-ps with od less than or equal to n,
        consider, D, the set of infinite, o< descending sequences of o-ps of od
        less than or equal to n.  The first element of a sequence in D has od n.
        Therefore, the o-first-expt of the first element of a sequence in D has od
        n-1.  Since o<, by IH, well-orders the o-ps with od less than n, the set
        of o-first-expts of first elements of the sequences in D has a minimal
        element, which we denote by B and which has od of n-1.

        Let k be the minimum integer such that for some infinite, o< descending
        sequence s of o-ps with od less than or equal to n, the first element of s
        has an o-first-expt of B and an o-first-coeff of k.  Notice that k is
        positive.

        Having fixed B and k, let s = s(1), s(2), ... be an infinite, o<
        descending sequence of o-ps with od less than or equal to n such that s(1)
        has a o-first-expt of B and an o-first-coeff of k.

        We show that each s(i) has a o-first-expt of B and an o-first-coeff of
        k. For suppose that s(j) is the first member of s either with o-first-expt
        B and o-first-coeff m (m neq k) or with o-first-expt B' and o-first-coeff
        B' (B' neq B). If (o-first-expt s(j)) = B', then B' has od n-1 (otherwise,
        by IH, s would not be infinite) and B' is o< B, contradicting the
        minimality of B. If 0 < m < k, then the fact that the sequence beginning
        at s(j) is infinitely descending contradicts the minimality of k. If m >
        k, then s(j) is greater than its predecessor; but this contradicts the
        fact that s is descending.

        Thus, by the definition of o<, for s to be a decreasing sequence of o-ps,
        (o-rst s(1)), (o-rst s(2)), ... must be a decreasing sequence. We end by
        showing this cannot be the case. Let t = t(1), t(2), ... be an infinite
        sequence of o-ps such that t(i) = (o-rst s(i)). Then t is infinitely
        descending. Furthermore, t(1) begins with an o-p B' that is o< B. Since t
        is in D, t(1) has od n, therefore, B' has od n-1. But this contradicts the
        minimality of B. Q.E.D.

Theorem.  o< well-orders the o-ps.  Proof.  Every infinite, o<
descending sequence of o-ps has the property that each member has od
less than or equal to the od, n, of the first member of the sequence.
This contradicts Lemma Main.  Q.E.D.

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.

REDEF    a common way to set ld-redefinition-action

     Example and General Form:
     ACL2 !>:redef

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

This command allows redefinition of functions and other events without
undoing, but with a query that requires the user to acknowledge that the
redefinition is intentional.  To avoid that query, see REDEF!
or for more options, see LD-REDEFINITION-ACTION.

REDEF!    a common way to set ld-redefinition-action

     Example and General Form:
     ACL2 !>:redef!

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

This command allows redefinition of functions and other events without
undoing, but with a warning.  The command :redef is similar, but
queries the user first before doing the redefinition.  For more related
options, see LD-REDEFINITION-ACTION.

REDEF+    system hacker's redefinition command

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

This command is intended only for system hackers, not typical users.  It
sets ld-redefinition-action to '(:warn! . :overwrite), sets the default
defun-mode to :program, and invokes set-state-ok with value t.  It also
introduces (defttag :redef+), so that redefinition of system functions
will be permitted; see DEFTTAG.  Finally, it removes as
untouchable all variables and functions.

This command is intended for those who are modifying ACL2 source code
definitions.  Thus, 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.  See also the Notes below.

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, :measure, 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).  (3) The :measure check is avoided if we are skipping
proofs (for example, during include-book), and otherwise, the new
definition may have a :measure of (:? v1 ... vk), where (v1 ... vk)
enumerates the variables occurring in the measure stored for the old
definition.

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 corresponding list of untouchable symbols.

A remove-untouchable event is redundant if no name supplied is a member
of the corresponding list of untouchable symbols.

A reset-prehistory event is redundant if it does not cause any change.

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

Defdoc events are never redundant because they don't define any name.
A table event also does not define any name, but it is redundant when
it sets the value already associated with a key of the table, or when
it sets an entire table (using keyword :clear) to its existing value;
see TABLE.

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.

_Note About Built-in (Predefined) Functions and Macros:_

Redundancy is restricted for built-in macros and functions that have
special raw Lisp code.  Such redundancy is only legal in the context of
LOCAL.  This restriction is needed for soundness, for technical reasons
omitted here (details may be found in a long comment about
redundant-events in source function chk-acceptable-defuns).

_Note About Appropriate Modes:_

Suppose a function is being redefined and that the formals, 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.

_Note About Shifting Logical Names:_

Suppose a book defines a function fn and later uses fn as a logical
name in a theory expression.  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.

_Note About Unfortunate Redundancies:_

Notice that our syntactic criterion for redundancy of defun events does
not allow redefinition to take effect unless there is a syntactic change
in the definition.  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.

REORDER    hints keyword :REORDER

See HINTS.

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-EXEC for 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 made using defun 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.

     Acl2-oracle, a list of objects, used for example to implement the
     functions that let ACL2 report how much time was used, but
     inaccessible to the user.  Also see WITH-PROVER-TIME-LIMIT.

     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.