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

PROGRAMMING    built-in ACL2 functions

The built-in ACL2 functions that one typically uses in writing programs
are listed below.  See their individual documentations.  We do not
bother to document the some of the more obscure functions provided by
ACL2 that do not correspond to functions of Common Lisp.

Related topics other than immediate subtopics:

See any documentation for Common Lisp for more details on many of these
functions.

*    multiplication macro

* is really a macro that expands to calls of the function binary-*.  So
for example

     (* x y 4 z)

represents the same term as

     (binary-* x (binary-* y (binary-* 4 z))).

See BINARY-*.

* is a Common Lisp function.  See any Common Lisp documentation for
more information.

*STANDARD-CI*    an ACL2 character-based analogue of CLTL's *standard-input*

The value of the ACL2 constant *standard-ci* is an open character input
channel that is synonymous to Common Lisp's *standard-input*.

ACL2 character input from *standard-ci* is actually obtained by reading
characters from the stream named by Common Lisp's *standard-input*.
That is, by changing the setting of *standard-input* in raw Common Lisp
you can change the source from which ACL2 reads on the channel
*standard-ci*.  See *STANDARD-CO*.

*STANDARD-CO*    the ACL2 analogue of CLTL's *standard-output*

The value of the ACL2 constant *standard-co* is an open character
output channel that is synonymous to Common Lisp's *standard-output*.

ACL2 character output to *standard-co* will go to the stream named by
Common Lisp's *standard-output*.  That is, by changing the setting of
*standard-output* in raw Common Lisp you can change the actual
destination of ACL2 output on the channel named by *standard-co*.
Observe that this happens without changing the logical value of
*standard-co* (which is some channel symbol).  Changing the setting of
*standard-output* in raw Common Lisp essentially just changes the map
that relates ACL2 to the physical world of terminals, files, etc.

To see the value of this observation, consider the following.  Suppose
you write an ACL2 function which does character output to the constant
channel *standard-co*.  During testing you see that the output actually
goes to your terminal.  Can you use the function to output to a file?
Yes, if you are willing to do a little work in raw Common Lisp: open a
stream to the file in question, set *standard-output* to that stream,
call your ACL2 function, and then close the stream and restore
*standard-output* to its nominal value.  Similar observations can be
made about the two ACL2 input channels, *standard-oi* and
*standard-ci*, which are analogues of *standard-input*.

Another reason you might have for wanting to change the actual streams
associated with *standard-oi* and *standard-co* is to drive the ACL2
top-level loop, ld, on alternative input and output streams.  This end
can be accomplished easily within ACL2 by either calling ld on the
desired channels or file names or by resetting the ACL2 state global
variables 'standard-oi and 'standard-co which are used by ld.  See
STANDARD-OI and see STANDARD-CO.

*STANDARD-OI*    an ACL2 object-based analogue of CLTL's *standard-input*

The value of the ACL2 constant *standard-oi* is an open object input
channel that is synonymous to Common Lisp's *standard-input*.

ACL2 object input from *standard-oi* is actually obtained by reading
from the stream named by Common Lisp's *standard-input*.  That is, by
changing the setting of *standard-input* in raw Common Lisp you can
change the source from which ACL2 reads on the channel *standard-oi*.
See *STANDARD-CO*.

+    addition macro

+ is really a macro that expands to calls of the function binary-+.  So
for example

     (+ x y 4 z)

represents the same term as

     (binary-+ x (binary-+ y (binary-+ 4 z))).

See BINARY-+.

-    macro for subtraction and negation

See BINARY-+ for addition and see UNARY-- for negation.

Note that - represents subtraction as follows:

     (- x y)

represents the same term as

     (+ x (- y))

which is really

     (binary-+ x (unary-- y)).

Also note that - represents arithmetic negation as follows:

     (- x)

expands to

     (unary-- x).

/    macro for division and reciprocal

See BINARY-* for multiplication and see UNARY-/ for
reciprocal.

Note that / represents division as follows:

     (/ x y)

represents the same term as

     (* x (/ y))

which is really

     (binary-* x (unary-/ y)).

Also note that / represents reciprocal as follows:

     (/ x)

expands to

     (unary-/ x).

/ is a Common Lisp macro.  See any Common Lisp documentation for more
information.

/=    test inequality of two numbers

(/= x y) is logically equivalent to (not (equal x y)).

Unlike equal, /= has a guard requiring both of its arguments to be
numbers.  Generally, /= is executed more efficiently than a combination
of not and equal.

For a discussion of the various ways to test against 0, See
ZERO-TEST-IDIOMS.

/= is a Common Lisp function.  See any Common Lisp documentation for
more information.

1+    increment by 1

(1+ x) is the same as (+ 1 x).  See +.

1+ is a Common Lisp function.  See any Common Lisp documentation for
more information.

1-    decrement by 1

(1- x) is the same as (- x 1).  See -.

1- is a Common Lisp function.  See any Common Lisp documentation for
more information.

<    less-than

Completion Axiom:

     (equal (< x y)
            (if (and (rationalp x)
                     (rationalp y))
                (< x y)
              (let ((x1 (if (acl2-numberp x) x 0))
                    (y1 (if (acl2-numberp y) y 0)))
                (or (< (realpart x1) (realpart y1))
                    (and (equal (realpart x1) (realpart y1))
                         (< (imagpart x1) (imagpart y1)))))))

Guard for (< x y):

     (and (rationalp x) (rationalp y))

Notice that like all arithmetic functions, < treats non-numeric inputs
as 0.

This function has the usual meaning on the rational numbers, but is
extended to the complex rational numbers using the lexicographic order:
first the real parts are compared, and if they are equal, then the
imaginary parts are compared.

<=    less-than-or-equal test

<= is a macro, and (<= x y) expands to the same thing as (not (< y x)).
See <.

<= is a Common Lisp function.  See any Common Lisp documentation for
more information.

=    test equality of two numbers

(= x y) is logically equivalent to (equal x y).

Unlike equal, = has a guard requiring both of its arguments to be
numbers.  Generally, = is executed more efficiently than equal.

For a discussion of the various ways to test against 0, See
ZERO-TEST-IDIOMS.

= is a Common Lisp function.  See any Common Lisp documentation for
more information.

>    greater-than test

> is a macro, and (> x y) expands to the same thing as (< y x).  See
<.

> is a Common Lisp function.  See any Common Lisp documentation for
more information.

>=    greater-than-or-equal test

>= is a macro, and (>= x y) expands to the same thing as (not (< x y)).
See <.

>= is a Common Lisp function.  See any Common Lisp documentation for
more information.

ABS    the absolute value of a real number

(Abs x) is -x if x is negative and is x otherwise.

The guard for abs requires its argument to be a rational (real, in
ACL2(r)) number.

Abs is a Common Lisp function.  See any Common Lisp documentation for
more information.

From "Common Lisp the Language" page 205, we must not allow complex x
as an argument to abs in ACL2, because if we did we would have to
return a number that might be a floating point number and hence not an
ACL2 object.

ACL2-NUMBERP    recognizer for numbers

(acl2-numberp x) is true if and only if x is a number, i.e., a rational
or complex rational number.

ACL2-USER    a package the ACL2 user may prefer

This package imports the standard Common Lisp symbols that ACL2
supports and also a few symbols from package "ACL2" that are commonly
used when interacting with ACL2.  You may prefer to select this as your
current package so as to avoid colliding with ACL2 system names.

This package imports the symbols listed in
*common-lisp-symbols-from-main-lisp-package*, which contains hundreds
of CLTL function and macro names including those supported by ACL2 such
as cons, car, and cdr.  It also imports the symbols in *acl2-exports*,
which contains a few symbols that are frequently used while interacting
with the ACL2 system, such as implies, defthm, and rewrite.  It imports
nothing else.

Thus, names such as alistp, member-equal, and type-set, which are
defined in the "ACL2" package are not present here.  If you find
yourself frequently colliding with names that are defined in "ACL2" you
might consider selecting "ACL2-USER" as your current package (see
IN-PACKAGE).  If you select "ACL2-USER" as the current package, you
may then simply type member-equal to refer to acl2-user::member-equal,
which you may define as you see fit.  Of course, should you desire to
refer to the "ACL2" version of member-equal, you will have to use the
"ACL2::" prefix, e.g., acl2::member-equal.

If, while using "ACL2-USER" as the current package, you find that there
are symbols from "ACL2" that you wish we had imported into it (because
they are frequently used in interaction), please bring those symbols to
our attention.  For example, should union-theories and universal-theory
be imported?  Except for stabilizing on the "frequently used" names
from "ACL2", we intend never to define a symbol whose
symbol-package-name is "ACL2-USER".

ACONS    constructor for association lists

(Acons key datum alist) equals the result of consing the pair (cons key
datum) to the front of the association list alist.

(Acons key datum alist) has a guard of (alistp alist).  Acons is a
Common Lisp function.  See any Common Lisp documentation for more
information.

ADD-TO-SET-EQ    add a symbol to a list

For a symbol x and a true list lst, (add-to-set-eq x lst) is the result
of consing x on to the front of lst, unless x is already a member of
lst, in which case it equals lst.

(add-to-set-eq x lst) has a guard that lst is a true list and moreover,
either x is a symbol or lst is a list of symbols.

ADD-TO-SET-EQL    add an object to a list

For an object x and a true list lst, (add-to-set-eql x lst) is the
result of consing x on to the front of lst, unless x is already a
member of lst, in which case it equals lst.

(add-to-set-eql x lst) has a guard that lst is a true list and
moreover, either x is eqlablep or lst is an eqlable-listp.

ADD-TO-SET-EQUAL    add an object to a list

For an object x and a true list lst, (add-to-set-equal x lst) is the
result of consing x on to the front of lst, unless x is already a
member of lst, in which case it equals lst.

(add-to-set-equal x lst) has a guard that lst is a true list.

ALISTP    recognizer for association lists

(alistp x) is true if and only if x is a list of cons pairs.

(alistp x) has a guard of t.

ALLOCATE-FIXNUM-RANGE    set aside fixnums in GCL

(Allocate-fixnum-range fixnum-lo fixnum-hi) causes Gnu Common Lisp
(GCL) to create a persistent table for the integers between fixnum-lo
and fixnum-hi (both bounds inclusive). This table is referenced first
when any integer is boxed and the existing box in the table is used if
the integer is in bounds.  This can speed up GCL considerably by
avoiding wasteful fixnum boxing.  Here, fixnum-lo and fixnum-hi should
be fixnums, more specifically of type (signed-byte 30), with fixnum-lo
<= fixnum-hi.

When this function is executed in a Lisp implementation other than GCL,
it has no side effect.  This function always returns nil.

ALPHA-CHAR-P    recognizer for alphabetic characters

(Alpha-char-p x) is true if and only if x is a alphabetic character,
i.e., one of the characters #a, #b, ..., #z, #A, #B, ..., #Z.

The guard for alpha-char-p requires its argument to be a character.

Alpha-char-p is a Common Lisp function.  See any Common Lisp
documentation for more information.

ALPHORDER    total order on atoms

Alphorder is a non-strict total order, a "less than or equal," on
atoms.  By "non-strict total order" we mean a function that always
returns t or nil and satisfies the following properties.

     o Antisymmetry:  XrY & YrX -> X=Y

     o Transitivity:  XrY & YrZ -> XrZ

     o Trichotomy:  XrY v YrX

Also see LEXORDER, which extends alphorder to all objects.

(Alphorder x y) has a guard of (and (atom x) (atom y)).

Within a single type: rationals are compared arithmetically, complex
rationals are compared lexicographically, characters are compared via
their char-codes, and strings and symbols are compared with alphabetic
ordering.  Across types, rationals come before complexes, complexes
come before characters, characters before strings, and strings before
symbols.  We also allow for "bad atoms," i.e., atoms that are not legal
Lisp objects but make sense in the ACL2 logic; these come at the end,
after symbols.

AND    conjunction

And is the macro for conjunctions.  And takes any number of arguments.
And returns nil if one of the arguments is nil, but otherwise returns
the last argument.  If there are no arguments, and returns t.

And is a Common Lisp macro.  See any Common Lisp documentation for more
information.

APPEND    concatenate two or more lists

Append, which takes two or more arguments, expects all the arguments
except perhaps the last to be true (null-terminated) lists.  It returns
the result of concatenating all the elements of all the given lists
into a single list.  Actually, in ACL2 append is a macro that expands
into calls of the binary function binary-append.

Append is a Common Lisp function.  See any Common Lisp documentation
for more information.

ASH    arithmetic shift operation

(ash i c) is the result of taking the two's complement representation
of the integer i and shifting it by c bits:  shifting left and padding
with c 0 bits if c is positive, shifting right and dropping (abs c)
bits if c is negative, and simply returning i if c is 0.

The guard for ash requires that its arguments are integers.

Ash is a Common Lisp function.  See any Common Lisp documentation for
more information.

ASSERT$    cause a hard error if the given test is false

     General Form:
     (assert$ test form)

where test returns a single value and form is arbitrary.  Semantically,
this call of assert$ is equivalent to form.  However, it causes a hard
error (using illegal) if the value of test is nil.

ASSOC    look up key in association list, using eql as test

(Assoc x alist) is the first member of alist whose car is x, or nil if
no such member exists.

(Assoc x alist) is provably the same in the ACL2 logic as (assoc-equal
x alist).  It has a stronger guard than assoc-equal because it uses eql
to test whether x is equal to the car of a given member of alist.  Its
guard requires that alist is an alistp, and moreover, either (eqlablep
x) or all cars of members of alist are eqlablep.  See
ASSOC-EQUAL and see ASSOC-EQ.

Assoc is a Common Lisp function.  See any Common Lisp documentation for
more information.  Since ACL2 functions cannot take keyword arguments
(though macros can), the ACL2 functions assoc-equal and assoc-eq are
defined to correspond to calls of the Common Lisp function assoc whose
keyword argument :test is equal or eq, respectively.

ASSOC-EQ    look up key in association list, using eq as test

(Assoc-eq x alist) is the first member of alist whose car is x, or nil
if no such member exists.

(Assoc-eq x alist) is provably the same in the ACL2 logic as (assoc x
alist) and (assoc-equal x alist), but it has a stronger guard because
it uses eq for a more efficient test for whether x is equal to a given
key of alist.  Its guard requires that alist is an association list
(see ALISTP), and moreover, either x is a symbol or all keys of
alist are symbols, i.e., alist is a symbol-alistp.

ASSOC-EQUAL    look up key in association list

(Assoc-equal x alist) is the first member of alist whose car is x, or
nil if no such member exists.

(Assoc-equal x alist) has a guard of (alistp alist), and returns the
first member of alist whose car is x, or nil if no such member exists.
Thus, assoc-equal has the same functionality as the Common Lisp
function assoc, except that it uses the equal function to test whether
x is the same as each successive `key' of alist.  See ASSOC and
see ASSOC-EQ.

ASSOC-KEYWORD    look up key in a keyword-value-listp

If l is a list of even length of the form (k1 a1 k2 a2 ... kn an),
where each ki is a keyword, then (assoc-keyword key l) is the first
tail of l starting with key if key is some ki, and is nil otherwise.

The guard for (assoc-keyword key l) is (keyword-value-listp l).

ASSOC-STRING-EQUAL    look up key, a string, in association list

(Assoc-string-equal x alist) is similar to assoc-equal.  However, for
string x and alist alist, the comparison of x with successive keys in
alist is done using string-equal rather than equal.

The guard for assoc-string-equal requires that x is a string and alist
is an alist.

ATOM    recognizer for atoms

(atom x) is true if and only if x is an atom, i.e., not a cons pair.

Atom has a guard of t, and is a Common Lisp function.  See any Common
Lisp documentation for more information.

ATOM-LISTP    recognizer for a true list of atoms

The predicate atom-listp tests whether its argument is a true-listp of
atoms, i.e., of non-conses.

BINARY-*    multiplication function

Completion Axiom:

     (equal (binary-* x y)
            (if (acl2-numberp x)
                (if (acl2-numberp y)
                    (binary-* x y)
                  0)
              0))

Guard for (binary-* x y):

     (and (acl2-numberp x) (acl2-numberp y))

Notice that like all arithmetic functions, binary-* treats non-numeric
inputs as 0.

Calls of the macro * expand to calls of binary-*; see *.

BINARY-+    addition function

Completion Axiom:

     (equal (binary-+ x y)
            (if (acl2-numberp x)
                (if (acl2-numberp y)
                    (binary-+ x y)
                  x)
              (if (acl2-numberp y)
                  y
                0)))

Guard for (binary-+ x y):

     (and (acl2-numberp x) (acl2-numberp y))

Notice that like all arithmetic functions, binary-+ treats non-numeric
inputs as 0.

Calls of the macro + expand to calls of binary-+; see +.

BINARY-APPEND    concatenate two lists

This binary function implements append, which is a macro in ACL2.  See
APPEND

The guard for binary-append requires the first argument to be a
true-listp.

BOOLEANP    recognizer for booleans

(Booleanp x) is t if x is t or nil, and is nil otherwise.

See GENERALIZED-BOOLEANS for a discussion of a potential
soundness problem for ACL2 related to the question:  Which Common Lisp
functions are known to return Boolean values?

BUTLAST    all but a final segment of a list

(Butlast l n) is the list obtained by removing the last n elements from
the true list l.  The following is a theorem (though it takes some
effort, including lemmas, to get ACL2 to prove it).

     (implies (and (integerp n)
                   (<= 0 n)
                   (true-listp l))
              (equal (length (butlast l n))
                     (if (< n (length l))
                         (- (length l) n)
                       0)))

For related functions, see TAKE and see NTHCDR.

The guard for (butlast l n) requires that n is a nonnegative integer
and lst is a true list.

Butlast is a Common Lisp function.  See any Common Lisp documentation
for more information.  Note:  In Common Lisp the second argument of
butlast is optional, but in ACL2 it is required.

CAAAAR    car of the caaar

See any Common Lisp documentation for details.

CAAADR    car of the caadr

See any Common Lisp documentation for details.

CAAAR    car of the caar

See any Common Lisp documentation for details.

CAADAR    car of the cadar

See any Common Lisp documentation for details.

CAADDR    car of the caddr

See any Common Lisp documentation for details.

CAADR    car of the cadr

See any Common Lisp documentation for details.

CAAR    car of the car

See any Common Lisp documentation for details.

CADAAR    car of the cdaar

See any Common Lisp documentation for details.

CADADR    car of the cdadr

See any Common Lisp documentation for details.

CADAR    car of the cdar

See any Common Lisp documentation for details.

CADDAR    car of the cddar

See any Common Lisp documentation for details.

CADDDR    car of the cdddr

See any Common Lisp documentation for details.

CADDR    car of the cddr

See any Common Lisp documentation for details.

CADR    car of the cdr

See any Common Lisp documentation for details.

CAR    returns the first element of a non-empty list, else nil

Completion Axiom:

     (equal (car x)
            (cond
             ((consp x)
              (car x))
             (t nil)))

Guard:

     (or (consp x) (equal x nil))

Notice that in the ACL2 logic, car returns nil for every atom.

CASE    conditional based on if-then-else using eql

     Example Form:
     (case typ
       ((:character foo)
        (open file-name :direction :output))
       (bar (open-for-bar file-name))
       (otherwise
        (my-error "Illegal.")))

is the same as

     (cond ((member typ '(:character foo))
            (open file-name :direction :output))
           ((eql typ 'bar)
            (open-for-bar file-name))
           (t (my-error "Illegal.")))

which in turn is the same as

     (if (member typ '(:character foo))
         (open file-name :direction :output)
         (if (eql typ 'bar)
             (open-for-bar file-name)
             (my-error "Illegal.")))

Notice the quotations that appear in the example above: '(:character
foo) and 'bar.

     General Forms:
     (case expr
       (x1 val-1)
       ...
       (xk val-k)
       (otherwise val-k+1))

     (case expr
       (x1 val-1)
       ...
       (xk val-k)
       (t val-k+1))

     (case expr
       (x1 val-1)
       ...
       (xk val-k))

where each xi is either eqlablep or a true list of eqlablep objects.
The final otherwise or t case is optional.

Case is defined in Common Lisp.  See any Common Lisp documentation for
more information.

CASE-MATCH    pattern matching or destructuring

     General Form:
     (case-match x
       (pat1 dcl1 body1)
       ...
       (patk dclk bodyk))

where x is a variable symbol, the pati are structural patterns as
described below, the dcli are optional declare forms and the bodyi are
terms.  Return the value(s) of the bodyi corresponding to the first
pati matching x, or nil if none matches.

Pattern Language:
With the few special exceptions described below, matching requires that
the cons structure of x be isomorphic to that of the pattern, down to
the atoms in the pattern.  Non-symbol atoms in the pattern match only
themselves.  Symbols in the pattern denote variables which match
anything and which are bound by a successful match to the corresponding
substructure of x.  Variables that occur more than once must match the
same (EQUAL) structure in every occurrence.

     Exceptions:
     &               Matches anything and is not bound.  Repeated
                       occurrences of & in a pattern may match different
                       structures.
     nil, t, *sym*   These symbols cannot be bound and match only their
                       global values.
     !sym            where sym is a symbol that is already bound in the
                       context of the case-match, matches only the
                       current binding of sym.
     'obj            Matches only itself.

Some examples are shown below.

Below we show some sample patterns and examples of things they match
and do not match.

     pattern       matches         non-matches
     (x y y)       (ABC 3 3)       (ABC 3 4)    ; 3 is not 4
     (fn x . rst)  (P (A I) B C)   (ABC)        ; NIL is not (x . rst)
                   (J (A I))                    ; rst matches nil
     ('fn (g x) 3) (FN (H 4) 3)    (GN (G X) 3) ; 'fn matches only itself
     (& t & !x)    ((A) T (B) (C))              ; provided x is '(C)

Consider the two binary trees that contain three leaves.  They might be
described as (x . (y . z)) and ((x . y) . z), where x, y, and z are
atomic.  Suppose we wished to recognize those trees.  The following
case-match would do:

     (case-match tree
       ((x . (y . z))
        (and (atom x) (atom y) (atom z)))
       (((x . y) . z)
        (and (atom x) (atom y) (atom z))))

Suppose we wished to recognize such trees where all three tips are
identical.  Suppose further we wish to return the tip if the tree is
one of those recognized ones and to return the number 7 otherwise.

     (case-match tree
       ((x . (x . x))
        (if (atom x) x 7))
       (((x . x) . x)
        (if (atom x) x 7))
       (& 7))

Note that case-match returns nil if no pati matches.  Thus if we must
return 7 in that case, we have to add as the final pattern the &, which
always matches anything.

CDAAAR    cdr of the caaar

See any Common Lisp documentation for details.

CDAADR    cdr of the caadr

See any Common Lisp documentation for details.

CDAAR    cdr of the caar

See any Common Lisp documentation for details.

CDADAR    cdr of the cadar

See any Common Lisp documentation for details.

CDADDR    cdr of the caddr

See any Common Lisp documentation for details.

CDADR    cdr of the cadr

See any Common Lisp documentation for details.

CDAR    cdr of the car

See any Common Lisp documentation for details.

CDDAAR    cdr of the cdaar

See any Common Lisp documentation for details.

CDDADR    cdr of the cdadr

See any Common Lisp documentation for details.

CDDAR    cdr of the cdar

See any Common Lisp documentation for details.

CDDDAR    cdr of the cddar

See any Common Lisp documentation for details.

CDDDDR    cdr of the cdddr

See any Common Lisp documentation for details.