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.

LOGICAL-NAME    a name created by a logical event

     Examples:
     assoc
     caddr
     +
     "ACL2-USER"
     "arith"
     "project/task-1/arith.lisp"
     :here

A logical name is either a name introduced by some event, such as defun,
defthm, or include-book, or else is the keyword :here, which refers to
the most recent such event.  See EVENTS.  Every logical name is
either a symbol or a string.  For the syntactic rules on names, see
NAME.  The symbols name functions, macros, constants, axioms,
theorems, labels, and theories.  The strings name packages or books.  We
permit the keyword symbol :here to be used as a logical name denoting
the most recently completed event.

The logical name introduced by an include-book is the full book name
string for the book (see FULL-BOOK-NAME).  Thus, under the
appropriate setting for the current book directory (see CBD) the
event (include-book "arith") may introduce the logical name

     "/usr/home/smith/project/task-1/arith.lisp" .

Under a different cbd setting, it may introduce a different logical
name, perhaps

     "/local/src/acl2/library/arith.lisp" .

It is possible that identical include-book events forms in a session
introduce two different logical names because of the current book
directory.

A logical name that is a string is either a package name or a book name.
If it is not a package name, we support various conventions to interpret
it as a book name.  If it does not end with the string ".lisp" we extend
it appropriately.  Then, we search for any book name that has the given
logical name as a terminal substring.  Suppose (include-book "arith") is
the only include-book so far and that
"/usr/home/smith/project/task-1/arith.lisp" is the source file it
processed.  Then "arith", "arith.lisp" and "task-1/arith.lisp" are all
logical names identifying that include-book event (unless they are
package names).  Now suppose a second (include-book "arith") is executed
and processes "/local/src/acl2/library/arith.lisp".  Then "arith" is no
longer a logical name, because it is ambiguous.  However, "task-1/arith"
is a logical name for the first include-book and "library/arith" is a
logical name for the second.  Indeed, the first can be named by
"1/arith" and the second by "y/arith".

Logical names are used primarily in the theory manipulation functions,
e.g., universal-theory and current-theory with which you may obtain some
standard theories as of some point in the historical past.  The
reference points are the introductions of logical names, i.e., the past
is determined by the events it contains.  One might ask, "Why not
discuss the past with the much more flexible language of command
descriptors?" (See COMMAND-DESCRIPTOR.)  The reason is that
inside of such events as encapsulate or macro commands that expand to
progns of events, command descriptors provide too coarse a grain.

When logical names are used as referents in theory expressions used in
books, one must consider the possibility that the defining event within
the book in question becomes redundant by the definition of the name
prior to the assumption of the book.  See REDUNDANT-EVENTS.

LOOP-STOPPER    limit application of permutative rewrite rules

See RULE-CLASSES for a discussion of the syntax of the
:loop-stopper field of :rewrite rule-classes.  Here we describe how that
field is used, and also how that field is created when the user does not
explicitly supply it.

For example, the built-in :rewrite rule commutativity-of-+,

     (implies (and (acl2-numberp x)
                   (acl2-numberp y))
              (equal (+ x y) (+ y x))),

creates a rewrite rule with a loop-stopper of ((x y binary-+)).  This
means, very roughly, that the term corresponding to y must be "smaller"
than the term corresponding to x in order for this rule to apply.
However, the presence of binary-+ in the list means that certain
functions that are "invisible" with respect to binary-+ (by default,
unary-- is the only such function) are more or less ignored when making
this "smaller" test.  We are much more precise below.

Our explanation of loop-stopping is in four parts.  First we discuss
ACL2's notion of "term order."  Next, we bring in the notion of
"invisibility", and use it together with term order to define orderings
on terms that are used in the loop-stopping algorithm.  Third, we
describe that algorithm.  These topics all assume that we have in hand
the :loop-stopper field of a given rewrite rule; the fourth and final
topic describes how that field is calculated when it is not supplied by
the user.

ACL2 must sometimes decide which of two terms is syntactically simpler.
It uses a total ordering on terms, called the "term order."  Under this
ordering constants such as '(a b c) are simpler than terms containing
variables such as x and (+ 1 x).  Terms containing variables are ordered
according to how many occurrences of variables there are.  Thus x and (+
1 x) are both simpler than (cons x x) and (+ x y).  If variable counts
do not decide the order, then the number of function applications are
tried.  Thus (cons x x) is simpler than (+ x (+ 1 y)) because the latter
has one more function application.  Finally, if the number of function
applications do not decide the order, a lexicographic ordering on Lisp
objects is used.  See TERM-ORDER for details.

When the loop-stopping algorithm is controlling the use of permutative
:rewrite rules it allows term1 to be moved leftward over term2 only if
term1 is smaller, in a suitable sense.  Note: The sense used in
loop-stopping is *not* the above explained term order but a more
complicated ordering described below.  The use of a total ordering stops
rules like commutativity from looping indefinitely because it allows (+
b a) to be permuted to (+ a b) but not vice versa, assuming a is smaller
than b in the ordering.  Given a set of permutative rules that allows
arbitrary permutations of the tips of a tree of function calls, this
will normalize the tree so that the smallest argument is leftmost and
the arguments ascend in the order toward the right.  Thus, for example,
if the same argument appears twice in the tree, as x does in the
binary-+ tree denoted by the term (+ a x b x), then when the allowed
permutations are done, all occurrences of the duplicated argument in the
tree will be adjacent, e.g., the tree above will be normalized to (+ a b
x x).

Suppose the loop-stopping algorithm used term order, as noted above, and
consider the binary-+ tree denoted by (+ x y (- x)).  The arguments here
are in ascending term order already.  Thus, no permutative rules are
applied.  But because we are inside a +-expression it is very convenient
if x and (- x) could be given virtually the same position in the
ordering so that y is not allowed to separate them.  This would allow
such rules as (+ i (- i) j) = j to be applied.  In support of this, the
ordering used in the control of permutative rules allows certain unary
functions, e.g., the unary minus function above, to be "invisible" with
respect to certain "surrounding" functions, e.g., + function above.

Briefly, a unary function symbol fn1 is invisible with respect to a
function symbol fn2 if fn2 belongs to the value of fn1 in
invisible-fns-table; also see SET-INVISIBLE-FNS-TABLE, which
explains its format and how it can be set by the user.  Roughly
speaking, "invisible" function symbols are ignored for the purposes of
the term-order test.

Consider the example above, (+ x y (- x)).  The translated version of
this term is (binary-+ x (binary-+ y (unary-- x))).  The initial
invisible-fns-table makes unary-- invisible with repect to binary-+.
The commutativity rule for binary-+ will attempt to swap y and (unary--
x) and the loop-stopping algorithm is called to approve or disapprove.
If term order is used, the swap will be disapproved.  But term order is
not used.  While the loop-stopping algorithm is permuting arguments
inside a binary-+ expression, unary-- is invisible.  Thus, insted of
comparing y with (unary-- x), the loop-stopping algorithm compares y
with x, approving the swap because x comes before y.

Here is a more precise specification of the total order used for
loop-stopping with respect to a list, fns, of functions that are to be
considered invisible.  Let x and y be distinct terms; we specify when "x
is smaller than y with respect to fns."  If x is the application of a
unary function symbol that belongs to fns, replace x by its argument.
Repeat this process until the result is not the application of such a
function; let us call the result x-guts.  Similarly obtain y-guts from
y.  Now if x-guts is the same term as y-guts, then x is smaller than y
in this order iff x is smaller than y in the standard term order.  On
the other hand, if x-guts is different than y-guts, then x is smaller
than y in this order iff x-guts is smaller than y-guts in the standard
term order.

Now we may describe the loop-stopping algorithm.  Consider a rewrite
rule with conclusion (equiv lhs rhs) that applies to a term x in a given
context; see REWRITE.  Suppose that this rewrite rule has a
loop-stopper field (technically, the :heuristic-info field) of ((x1 y1
. fns-1) ... (xn yn . fns-n)).  (Note that this field can be observed by
using the command :pr with the name of the rule; see PR.)  We
describe when rewriting is permitted.  The simplest case is when the
loop-stopper list is nil (i.e., n is 0); in that case, rewriting is
permitted.  Otherwise, for each i from 1 to n let xi' be the actual term
corresponding to the variable xi when lhs is matched against the term to
be rewritten, and similarly correspond yi' with y.  If xi' and yi' are
the same term for all i, then rewriting is not permitted.  Otherwise,
let k be the least i such that xi' and yi' are distinct.  Let fns be the
list of all functions that are invisible with respect to every function
in fns-k, if fns-k is non-empty; otherwise, let fns be nil.  Then
rewriting is permitted if and only if yi' is smaller than xi' with
respect to fns, in the sense defined in the preceding paragraph.

It remains only to describe how the loop-stopper field is calculated for
a rewrite rule when this field is not supplied by the user.  (On the
other hand, to see how the user may specify the :loop-stopper, see
RULE-CLASSES.)  Suppose the conclusion of the rule is of the form
(equiv lhs rhs).  First of all, if rhs is not an instance of the left
hand side by a substitution whose range is a list of distinct variables,
then the loop-stopper field is nil.  Otherwise, consider all pairs (u
. v) from this substitution with the property that the first occurrence
of v appears in front of the first occurrence of u in the print
representation of rhs.  For each such u and v, form a list fns of all
functions fn in lhs with the property that u or v (or both) appears as a
top-level argument of a subterm of lhs with function symbol fn.  Then
the loop-stopper for this rewrite rule is a list of all lists (u v
. fns).

LP    the Common Lisp entry to ACL2

To enter the ACL2 command loop from Common Lisp, call the Common Lisp
program lp (which stands for "loop," as in "read-eval-print loop" or
"command loop.")  The ACL2 command loop is actually coded in ACL2 as the
function ld (which stands for "load").  The command loop is just what
you get by loading from the standard object input channel,
*standard-oi*.  Calling ld directly from Common Lisp is possible but
fragile because hard lisp errors or aborts throw you out of ld and back
to the top-level of Common Lisp.  Lp calls ld in such a way as to
prevent this and is thus the standard way to get into the ACL2 command
loop.  Also see ACL2-CUSTOMIZATION for information on the
loading of an initialization file.

All of the visible functionality of lp is in fact provided by ld, which
is written in ACL2 itself.  Therefore, you should see LDfor
detailed documentation of the ACL2 command loop.  We sketch it below,
for novice users.

Every expression typed to the ACL2 top-level must be an ACL2 expression.

Any ACL2 expression may be submitted for evaluation.  Well-formedness is
checked.  Some well-formed expressions cannot be evaluated because they
involve (at some level) undefined constrained functions (see
ENCAPSULATE).  In addition, ACL2 does not allow "global variables" in
expressions to be evaluated.  Thus, (car '(a b c)) is legal and
evaluates to A, but (car x) is not, because there is no "global context"
or binding environment that gives meaning to the variable symbol x.

There is an exception to the global variable rule outlined above:
single-threaded objects (see STOBJ) may be used as global
variables in top-level expressions.  The most commonly used such object
is the ACL2 "current state," which is the value of the variable symbol
state.  This variable may occur in the top-level form to be evaluated,
but must be passed only to ACL2 functions "expecting" state as described
in the documentation for state and for stobjs in general.  If the form
returns a new state object as one of its values, then that is considered
the new "current" state for the evaluation of the subsequent form.  See
STATE.

ACL2 provides some support for the functionality usually provided by
global variables in a read-eval-print loop, namely the saving of the
result of a computation for subsequent re-use in another expression.
See ASSIGN and see @.

If the form read is a single keyword, e.g., :pe or :ubt, then special
procedures are followed.  See KEYWORD-COMMANDS.

The command loop keeps track of the commands you have typed and allows
you to review them, display them, and roll the logical state back to
that created by any command.  See HISTORY.

ACL2 makes the convention that if a top-level form returns three values,
the last of which is an ACL2 state, then the first is treated as a flag
that means "an error occurred," the second is the value to be printed if
no error occurred, and the third is (of course) the new state.  When "an
error occurs" no value is printed.  Thus, if you execute a top-level
form that happens to return three such values, only the second will be
printed (and that will only happen if the first is nil!).  See
LD for details.

MACRO-ARGS    the formals list of a macro definition

     Examples:
     (x y z)
     (x y z &optional max (base '10 basep))
     (x y &rest rst)
     (x y &key max base)
     (&whole sexpr x y)

The "lambda-list" of a macro definition may include simple formal
parameter names as well as appropriate uses of the following lambda-list
keywords from CLTL (pp. 60 and 145), respecting the order shown:

       &whole,
       &optional,
       &rest,
       &body,
       &key, and
       &allow-other-keys.

ACL2 does not support &aux and &environment.  In addition, we make the
following restrictions:

     (1) initialization forms in &optional and &key specifiers must be
     quoted values;

     (2) &allow-other-keys may only be used once, as the last specifier;
     and

     (3) destructuring is not allowed.

You are encouraged to experiment with the macro facility.  One way to do
so is to define a macro that does nothing but return the quotation of
its arguments, e.g.,

     (defmacro demo (x y &optional opt &key key1 key2)
       (list 'quote (list x y opt key1 key2)))

You may then execute the macro on some sample forms, e.g.,

       term                         value
     (demo 1 2)                (1 2 NIL NIL NIL)
     (demo 1 2 3)              (1 2 3 NIL NIL)
     (demo 1 2 :key1 3)        error:  non-even key/value arglist
                               (because :key1 is used as opt)
     (demo 1 2 3 :key2 5)      (1 2 3 NIL 5)

In particular, Common Lisp specifies that if you use both &rest and
&key, then both will be bound using the same list of arguments.  The
following example should serve to illustrate how this works.

     ACL2 !>(defmacro foo (&rest args &key k1 k2 k3)
              (list 'quote (list args k1 k2 k3)))

     Summary
     Form:  ( DEFMACRO FOO ...)
     Rules: NIL
     Warnings:  None
     Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
      FOO
     ACL2 !>(foo :k1 3 :k2 4 :k3 5)
     ((:K1 3 :K2 4 :K3 5) 3 4 5)
     ACL2 !>(foo :k1 3 :k2 4)
     ((:K1 3 :K2 4) 3 4 NIL)
     ACL2 !>

Also see TRANS.

MEASURE    xargs keyword :MEASURE

See XARGS.

MODE    xargs keyword :MODE

See XARGS.

NAME    syntactic rules on logical names

     Examples                 Counter-Examples

     PRIMEP               91         (not a symbolp)
     F-AC-23              :CHK-LIST  (in KEYWORD package)
     1AX                  *PACKAGE*  (in the Lisp Package)
     |Prime Number|       1E3        (not a symbolp)

Many different ACL2 entities have names, e.g., functions, macros,
variables, constants, packages, theorems, theories, etc.  Package names
are strings.  All other names are symbols and may not be in the
"KEYWORD" package.  Moreover, names of functions, macros, constrained
functions, and constants, other than those that are predefined, must not
be in the "main Lisp package" (which is ("LISP" or "COMMON-LISP",
according to whether we are following CLTL1 or CLTL2).  An analogous
restriction on variables is given below.

T, nil, and all names above except those that begin with ampersand (&)
are names of variables or constants.  T, nil, and those names beginning
and ending with star (*) are constants.  All other such names are
variables.

Note that names that start with ampersand, such as &rest, may be lambda
list keywords and are reserved for such use whether or not they are in
the CLTL constant lambda-list-keywords.  (See pg 82 of CLTL2.)  That is,
these may not be used as variables.  Unlike constants, variables may be
in the main Lisp package as long as they are in the original list of
imports from that package to ACL2, the list
*common-lisp-symbols-from-main-lisp-package*, and do not belong to a
list of symbols that are potentially "global."  This latter list is the
value of *common-lisp-specials-and-constants*.

Our restrictions pertaining to the main Lisp package take into account
that some symbols, e.g., lambda-list-keywords and boole-c2, are
"special."  Permitting them to be bound could have harmful effects.  In
addition, the Common Lisp language does not allow certain manipulations
with many symbols of that package.  So, we stay away from them, except
for allowing certain variables as indicated above.

NON-EXECUTABLE    xargs keyword :NON-EXECUTABLE

See XARGS.

NON-LINEAR-ARITHMETIC    Non-linear Arithmetic

This documentation topic is divided into two parts.  We first discuss
the practical aspect of how to use the non-linear arithmetic extension
to ACL2, and then the theory behind it.  We assume that the reader is
familiar with the material in linear-arithmetic and that on :linear
rules.

We begin our discussion of how to use non-linear arithmetic with a
simple example.  Assume that we wish to prove:

     (thm
      (implies (and (rationalp x)
                    (rationalp y)
                    (rationalp z)
                    (< 0 y)
                    (< x (* y z)))
               (< (floor x y) z)))

Note that (floor x y) <= (/ x y).  Note also that if we divide both
sides of x < (* y z) by y, since 0 < y, we obtain (/ x y) < z.  By
chaining these two inequalities together, we get the inequality we
desired to prove.

We now proceed with our example session:

     (skip-proofs
      (progn

     ; Since the truth of this theorem depends on the linear properties
     ; of floor, we will need the linear lemma:

        (defthm floor-bounds-1
            (implies (and (rationalp x)
                          (rationalp y))
                     (and (< (+ (/ x y) -1)
                             (floor x y))
                          (<= (floor x y)
                              (/ x y))))
            :rule-classes ((:linear :trigger-terms ((floor x y)))))

     ; We now disable floor, so that the linear lemma will be used.

        (in-theory (disable floor))

     ; We create five rewrite rules which we will use during non-linear
     ; arithmetic.  The necessity for these is due to one of the differences in
     ; ACL2's behaviour when non-linear arithmetic is turned on.  Although
     ; the conclusions of linear lemmas have always been rewritten before
     ; they are used, now, when non-linear arithmetic is turned on, the
     ; conclusions are rewritten under a different theory than under "normal"
     ; rewriting.  This theory is also used in other, similar, circumstances
     ; described below.

        (defthm |arith (* -1 x)|
            (equal (* -1 x)
                   (- x)))

        (defthm |arith (* 1 x)|
            (equal (* 1 x)
                   (fix x)))

        (defthm |arith (* x (/ x) y)|
            (equal (* x (/ x) y)
                   (if (equal (fix x) 0)
                       0
                       (fix y))))

        (defthm |arith (* y x)|
            (equal (* y x)
                   (* x y)))

        (defthm |arith (fix x)|
            (implies (acl2-numberp x)
                     (equal (fix x)
                            x))))
      )  ; End skip-proofs.

     ; We disable the above rewrite rules from normal use.

     (in-theory (disable |arith (* -1 x)|
                         |arith (* 1 x)|
                         |arith (* x (/ x) y)|
                         |arith (* y x)|
                         |arith (fix x)|))

     ; We create an arithmetic-theory.  Note that we must give a quoted
     ; constant for the theory -- none of the normal theory-functions
     ; are applicable to in-arithmetic-theory.

     (in-arithmetic-theory '(|arith (* -1 x)|
                             |arith (* 1 x)|
                             |arith (* x (/ x) y)|
                             |arith (* y x)|
                             |arith (fix x)|))

     ; We turn non-linear arithmetic on.

     (set-non-linearp t)

     ; We can now go ahead and prove our theorem.

     (thm
      (implies (and (rationalp x)
                    (rationalp y)
                    (rationalp z)
                    (< 0 y)
                    (< x (* y z)))
               (< (floor x y) z)))

The above example illustrates the two practical requirements for using
non-linear arithmetic in ACL2.  First, one must set up an
arithmetic-theory.  Usually, one would not set up an arithmetic-theory
on one's own but would instead load a library book or books which do so.
Second, one must turn the non-linear arithmetic extension on.  This one
must do explicitly -- no book can do this for you.

For a brief discussion of why this is so, even though (set-non-linearp
t) is an embeddable event, see ACL2-DEFAULTS-TABLE (in
particular, the final paragraph).  (Note that (set-non-linearp t)
modifies the acl2-defaults-table.)  Also see SET-NON-LINEARP,
see EMBEDDED-EVENT-FORM, and see EVENTS.

You can also enable non-linear arithmetic with the hint :nonlinearp t.
See HINTS.  We, in fact, recommend the use of a hint which will
enable nonlinear arithmetic only when the goal has stabilized under
rewriting.  Using default-hints can make this easier.

     (defun nonlinearp-default-hint (stable-under-simplificationp hist pspv)
       (cond (stable-under-simplificationp
              (if (not (access rewrite-constant
                               (access prove-spec-var pspv :rewrite-constant)
                               :nonlinearp))
                  '(:computed-hint-replacement t :nonlinearp t)
                nil))
             ((access rewrite-constant
                      (access prove-spec-var pspv :rewrite-constant)
                      :nonlinearp)
              (if (not (equal (caar hist) 'SETTLED-DOWN-CLAUSE))
                  '(:computed-hint-replacement t :nonlinearp nil)
                nil))
             (t nil)))

     (set-default-hints '((nonlinearp-default-hint stable-under-simplificationp
                                                   hist pspv)))

This has proven to be a helpful strategy which allows faster proof
times.

We now proceed to briefly describe the theory behind the non-linear
extension to ACL2.  In linear-arithmetic it was stated that, "[L]inear
polynomial inequalities can be combined by cross-multiplication and
addition to permit the deduction of a third inequality...."  That is, if

     0 < poly1,
     0 < poly2,

and c and d are rational constants, then

     0 < c*poly1 + d*poly2.

Similarly, given the above,

     0 < poly1*poly2.

In the linear arithmetic case, we are taking advantage of the facts that
multiplication by a positive rational constant does not change the sign
of a polynomial and that the sum of two positive polynomials is itself
positive.  In the non-linear arithmetic case, we are using the fact that
the product of two positive polynomials is itself positive.

For example, suppose we have the three assumptions:

     p1:  3*x*y + 7*a < 4
     p2:            3 < 2*x  or p2': 0 < -3 + 2*x
     p3:            1 < y    or p3': 0 < -1 + y,

and we wish to prove that a < 0.  As described elsewhere (see
LINEAR-ARITHMETIC), we proceed by assuming the negation of our goal:

     p4:            0 <= a,

and looking for a contradiction.

There are no cancellations which can be performed by linear arithmetic
in the above situation.  (Recall that two polynomials are cancelled
against each other only when they have the same largest unknown.)
However, p1 has a product as its largest unknown, and for each of the
factors of that product there is a poly that has that factor as a
largest unknown.  When non-linear arithmetic is enabled, ACL2 will
therefore multiply p1' and p2' obtaining

     p5:            0 < 3 + -2*x + -3*y + 2*x*y.

The addition of this polynomial will allow cancelation to continue and,
in this case, we will prove our goal.  Thus, just as ACL2 adds two
polynomials together when they have the same largest unknown of opposite
signs in order to create a new "smaller" polynomial; so ACL2 multiplies
polynomials together when the product of their largest unknowns is
itself the largest unknown of another polynomial.  As the use of :linear
lemmas to further seed the arithmetic data base may allow cancellation
to proceed, so may the use of non-linear arithmetic.

This multiplication of polynomials is the other situation in which terms
are rewritten under the arithemtic-theory rather than the normal one.
Because this may be done so often, and because the individual factors
have presumably already been rewritten, it is important that this be
done in an efficient way.  The use of a small, specialized, theory helps
avoid the repeated application of rewrite rules to already stabilized
terms.

NONLINEARP    hints keyword :NONLINEARP

See HINTS.

NORMALIZE    xargs keyword :NORMALIZE

See XARGS.

NU-REWRITER    rewriting NTH/UPDATE-NTH expressions

The rewriter contains special provisions for rewriting expressions
composed of nth, update-nth, update-nth-array, together with let
expressions and other applications of non-recursive functions or lambda
expressions.  For details see the paper "Rewriting for Symbolic
Execution of State Machine Models" by J Strother Moore.  Also see
SET-NU-REWRITER-MODE.

The "nu-rewriter" is a recent addition to the main rewrite engine in
ACL2.  Consider the expression

      (let ((s (update-nth 1 (new-a x s) s)))
        (let ((s (update-nth 2 (new-b x s) s)))
          (let ((s (update-nth 3 (new-c x s) s)))
            s)))

If the lets in this expression are expanded, a very large expression
results because of the duplicate occurrences of s:

     (update-nth 3
                 (new-c x
                        (update-nth 2
                                    (new-b x
                                           (update-nth 1
                                                       (new-a x s)
                                                       s))
                                    (update-nth 1
                                                (new-a x s)
                                                s)))
                 (update-nth 2
                             (new-b x
                                    (update-nth 1
                                                (new-a x s)
                                                s))
                             (update-nth 1
                                         (new-a x s)
                                         s))).

This expansion of the let expression can be very expensive in space and
time.  In particular, the (new-a x s) expression might be rewritten many
times.

Now imagine asking what 2nd component of the structure is.  That is,
consider

      (nth 2
           (let ((s (update-nth 1 (new-a x s) s)))
             (let ((s (update-nth 2 (new-b x s) s)))
               (let ((s (update-nth 3 (new-c x s) s)))
                 s))))

The normal ACL2 rewrite engine would answer this question by first
rewriting the arguments to the nth expression; in particular, it would
expand the nested let expression to the large nested update-nth
expression and then, using rules such as

     (defthm nth-update-nth
       (equal (nth m (update-nth n val l))
              (if (equal (nfix m) (nfix n))
                  val (nth m l))))

would reduce the expression to (new-b x (update-nth 1 (new-a x s) s)).

The purpose of the nu-rewriter is to allow simplifications like this
without first expanding the lets.  The "nu" in the name is an acronym
for "nth/update-nth".  The nu-rewriter knows how to move an nth into a
let without expanding the let and how to simplify it if it nestles up
against an update-nth.

There are four characteristics of this problem: the presence of nth, the
presence of update-nth, the use of let to provide "sequential" updates,
and the use of constant indices.  Nth and update-nth need not occur
explicitly; they may be used inside of definitions of "wrapper"
functions.

Because the nu-rewriter changes the order in which things are rewritten,
its routine use can make ACL2 unable to reproduce old proofs.  It is
therefore switched off by default.  If your application exhibits the
characteristics above, you might wish to switch the nu-rewriter on using
set-nu-rewriter-mode.

More will eventually be written about the nu-rewriter.  However, it is
described in detail in the paper cited at the beginning of this
documentation topic.

OBDD    ordered binary decision diagrams with rewriting

See BDD for information on this topic.

OPEN-INPUT-CHANNEL    See IO.

OPEN-INPUT-CHANNEL-P    See IO.

OPEN-OUTPUT-CHANNEL    See IO.

OPEN-OUTPUT-CHANNEL-P    See IO.

ORDINALS    ordinals in ACL2

Ordinals are used in ACL2 for proving termination in the admission of
recursive function definitions.  For a proof that the ACL2 ordinals are
well-founded, see PROOF-OF-WELL-FOUNDEDNESS.

The representation of ordinals changed in ACL2 Version_2.8, and is due
to Pete Manolios and Daron Vroon.  They have also defined algorithms for
ordinal arithmetic, created a library of theorems to reason about
ordinal arithmetic, and written the rest of this documentation in order
to explain this change.  We thank them for their efforts.  Although they
have provided the implementation and even modified the distributed books
and workshop books as needed, we have looked over their work and are
maintaining it (and this documentation); if there are any bugs, they
should be considered ours (Matt Kaufmann and J Moore).

A book is included for compatibility with the representation before
Version_2.8.  For books that contain events relying on the previous
ordinal implementation, insert the following lines before the first such
event:

     (include-book "ordinals/e0-ordinal" :dir :system)
     (set-well-founded-relation e0-ord-<)

The new ordinal representation is based on a slightly different version
of Cantor Normal Form than that used by the old ordinals.  An advantage
of the new representation is that it is exponentially more succinct than
the old representation.

While pre-Version_2.8 ACL2 versions provided built-in functions for
checking if an object is an ordinal and for comparing two ordinals, they
did not provide support for reasoning about and constructing ordinals.
The books in the directory books/ordinals provide such support.  First,
they provide efficient algorithms for ordinal arithmetic (including
addition, subtraction, multiplication, and exponentiation).  The
algorithms and their complexity are described in the following paper.

     Manolios, Panagiotis & Vroon, Daron.
     Algorithms for ordinal arithmetic.
     Baader, Franz (ed),
     19th International Conference on Automated Deduction--CADE-19.
     Pages 243-257 of LNAI, vol. 2741.  Springer-Verlag.

Second, the algorithms are mechanically verified and libraries of
theorems which can be used to automate reasoning involving the ordinals
are provided.  For details, see the following 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 describe aspects of the above mentioned books in more detail.

The new ordering function is o< and the new ordinal recognizer is o-p.
See also natp, posp, o<=, o>, o>=, o-first-expt, o-first-coeff, o-rst,
make-ord, o-finp, and o-infp.

The old ordinals were based on the following formulation of Cantor
Normal Form:

For any ordinal, a < epsilon-0, there exist natural numbers p and n, and
ordinals a1 >= a2 >= ... >= an > 0 such that a > a1 and a = w^(a1) +
w^(a2) + ... + w^(an) + p.

Thus, a predicate recognizing ACL2's old ordinals is given by the
following definition.

     (defun e0-ordinalp (x)
       (if (consp x)
           (and (e0-ordinalp (car x))
                (not (equal (car x) 0))
                (e0-ordinalp (cdr x))
                (or (atom (cdr x))
                    (not (e0-ord-< (car x) (cadr x)))))
         (and (integerp x)
              (>= x 0))))

The new representation is based on a corollary to the above theorem,
which we get by the left distributive property of ordinal multiplication
over ordinal addition. Thus, w^a + w^a = (w^a)2, w^a + w^a + w^a =
(w^a)3 and so forth. The corollary is as follows:

For any ordinal, a < epsilon-0, there exist natural numbers p and n,
positive integers x1, x2, ..., xn and ordinals a1 > a2 > ... > an > 0
such that a > a1 and a = w^(a1)x1 + w^(a2)x2 + ... + w^(an)xn + p.

Instead of representing an ordinal as a list of non-increasing ordinals,
we represent it as a list of exponent-coefficient pairs, such that the
exponents are strictly decreasing (see O-P).  Note that this
representation is exponentially more efficient than the old
representation.

The ordinal arithmetic functions: o+, o-, o*, and o^ are defined in the
ordinals library (in the subdirectory books/ordinals). To use them,
include the book ordinals-without-arithmetic or ordinals, depending on
whether you want the arithmetic books included or not (ordinals includes
books/arithmetic/top-with-meta). To use the old ordinals, include the
book e0-ordinal and run the command (set-well-founded-relation e0-ord-<)

The file books/arithmetic/natp-posp is a book for reasoning about posp
and natp.  We recommend using this book if you have to reason about posp
and natp.  It is included in books/arithmetic/top, which is included in
books/arithmetic/top-with-meta, which is included in
books/ordinals/ordinals.

If you have a good reason to use the old definitions of the ordinals
(e.g., because of legacy code and theorems), then we provide a
convenient way to do this.  In the book ordinal-isomorphism we prove
that the new ordinals are order-isomorphic to the old ordinals and thus
theorems proved in one context can be directly transferred to the other.
For an example of how to do this, look at the book defmul in the
directory books/workshops/2000/ruiz/multiset.

The ordinals books have been used to prove non-trivial theorems.  For a
good example, see the books in the directory
books/workshops/2003/sustik/support, where Matyas Sustik proves
Dickson's lemma.

Finally, many termination proofs can be carried out with weaker
orderings than the ordinals up to epsilon-0.  For example, many
inductive theorem provers only know that the lexicographic ordering on
natural numbers is well-founded.  The book lexicographic-ordering
contains a definition of such an ordering l< whose arguments are either
a list of natural numbers, or a natural number.  In the book we prove
that l< is well-founded (that is, we prove a :well-founded-relation
defthm and provide a macro llist to simplify the generation of measure
functions.  We also show how to use l< to prove that the famous
Ackermann function terminates.  Finally, since l< does something
reasonable with natural numbers, it gets along with acl2-count, the
default measure chosen by ACL2.

OTF-FLG    pushing all the initial subgoals

The value of this flag is normally nil.  If you want to prevent the
theorem prover from abandoning its initial work upon pushing the second
subgoal, set :otf-flg to t.

Suppose you submit a conjecture to the theorem prover and the system
splits it up into many subgoals.  Any subgoal not proved by other
methods is eventually set aside for an attempted induction proof.  But
upon setting aside the second such subgoal, the system chickens out and
decides that rather than prove n>1 subgoals inductively, it will abandon
its initial work and attempt induction on the originally submitted
conjecture.  The :otf-flg (Onward Thru the Fog) allows you to override
this chickening out. When :otf-flg is t, the system will push all the
initial subgoals and proceed to try to prove each, independently, by
induction.

Even when you don't expect induction to be used or to succeed, setting
the :otf-flg is a good way to force the system to generate and display
all the initial subgoals.

For defthm and thm, :otf-flg is a keyword argument that is a peer to
:rule-classes and :hints.  It may be supplied as in the following
examples; also see DEFTHM.

     (thm (my-predicate x y) :rule-classes nil :otf-flg t)

     (defthm append-assoc
       (equal (append (append x y) z)
              (append x (append y z)))
       :hints (("Goal" :induct t))
       :otf-flg t)

The :otf-flg may be supplied to defun via the xargs declare option.
When you supply an :otf-flg hint to defun, the flag is effective for the
termination proofs and the guard proofs, if any.

PACKAGE-REINCARNATION-IMPORT-RESTRICTIONS    re-defining undone defpkgs

Suppose (defpkg "pkg" imports) is the most recently executed successful
definition of "pkg" in this ACL2 session and that it has since been
undone, as by :ubt.  Any future attempt in this session to define "pkg"
as a package must specify an identical imports list.

The restriction stems from the need to implement the reinstallation of
saved logical worlds as in error recovery and the :oops command.
Suppose that the new defpkg attempts to import some symbol, a::sym, not
imported by the previous definition of "pkg".  Because it was not
imported in the original package, the symbol pkg::sym, different from
a::sym, may well have been created and may well be used in some saved
worlds.  Those saved worlds are Common Lisp objects being held for you
"behind the scenes."  In order to import a::sym into "pkg" now we would
have to unintern pkg::sym, rendering those saved worlds ill-formed.  It
is because of saved worlds that we do not actually clear out a package
when it is undone.

At one point we thought it was sound to allow the new defpkg to import a
subset of the old.  But that is incorrect.  Suppose the old definition
of "pkg" imported a::sym but the new one does not.  Suppose we allowed
that and implemented it simply by setting the imports of "pkg" to the
new subset.  Then consider the conjecture (eq a::sym pkg::sym).  This
ought not be a theorem because we did not import a::sym into "pkg".  But
in fact in AKCL it is a theorem because pkg::sym is read as a::sym
because of the old imports.

PEEK-CHAR$    See IO.

PRINT-DOC-START-COLUMN    printing the one-liner

     Examples:
     (assign print-doc-start-column nil)
     (assign print-doc-start-column 17)

This state global variable controls the column in which the "one-liner"
of a formatted documentation string is printed.  Generally, when :doc is
used to print a documentation string, the name of the documented concept
is printed and then :doc tabs over to print-doc-start-column and prints
the one-liner.  If the name extends past the desired column, :doc
outputs a carriage return and then tabs over to the column.  If
print-doc-start-column is nil, :doc just starts the one-liner two spaces
from the end of the name, on the same line.  The initial value of
print-doc-start-column is 15.

PRINT-OBJECT$    See IO.

PROMPT    the prompt printed by ld

The prompt printed by ACL2 conveys information about various "modes."
See DEFAULT-PRINT-PROMPT and see LD-PROMPT for details.

The prompt during raw Lisp breaks is, with most Common Lisp
implementations, adjusted by ACL2 to include the string "[RAW LISP"], in
order to reminder users not to submit ACL2 forms there; see
BREAKS.  For Lisps that seem to use the same code for printing prompts
at the top-level as in breaks, the top-level prompt is similarly
adjusted.  For Lisps with the above prompt adjustment, The following
forms may be executed in raw Lisp (i.e., after typing :q).

     (install-new-raw-prompt) ; install prompt with [RAW LISP] as described above
     (install-old-raw-prompt) ; revert to original prompt from host Common Lisp

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.