This is documentation for ACL2 Version 3.1
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.

STRING    coerce to a string

(String x) coerces x to a string.  If x is already a string, then it is
returned unchanged; if x is a symbol, then its symbol-name is returned;
and if x is a character, the corresponding one-character string is
returned.

The guard for string requires its argument to be a string, a symbol, or
a character.

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

STRING-APPEND    concatenate two strings

NOTE:  It is probably more efficient to use the Common Lisp function
concatenate in place of string-append.  That is,

     (string-append str1 str2)

is equal to

     (concatenate 'string str1 str2).

At any rate, string-append takes two arguments, which are both strings
(if the guard is to be met), and returns a string obtained
concatenating together the characters in the first string followed by
those in the second.  See CONCATENATE.

STRING-DOWNCASE    in a given string, turn upper-case characters into lower-case

For a string x, (string-downcase x) is the result of applying
char-downcase to each character in x.

The guard for string-downcase requires its argument to be a string
containing only standard characters.

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

STRING-EQUAL    string equality without regard to case

For strings str1 and str2, (string-equal str1 str2) is true if and only
str1 and str2 are the same except perhaps for the cases of their
characters.

The guard on string-equal requires that its arguments are strings
consisting of standard characters (see STANDARD-CHAR-LISTP).

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

STRING-LISTP    recognizer for a true list of strings

The predicate string-listp tests whether its argument is a true-listp
of strings.

STRING-UPCASE    in a given string, turn lower-case characters into upper-case

For a string x, (string-upcase x) is the result of applying char-upcase
to each character in x.

The guard for string-upcase requires its argument to be a string
containing only standard characters.

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

STRING<    less-than test for strings

(String< str1 str2) is non-nil if and only if the string str1 precedes
the string str2 lexicographically, where character inequalities are
tested using char<.  When non-nil, (string< str1 str2) is the first
position (zero-based) at which the strings differ.  Here are some
examples.

     ACL2 !>(string< "abcd" "abu")
     2
     ACL2 !>(string< "abcd" "Abu")
     NIL
     ACL2 !>(string< "abc" "abcde")
     3
     ACL2 !>(string< "abcde" "abc")
     NIL

The guard for string< specifies that its arguments are strings.

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

STRING<=    less-than-or-equal test for strings

(String<= str1 str2) is non-nil if and only if the string str1 precedes
the string str2 lexicographically or the strings are equal.  When
non-nil, (string<= str1 str2) is the first position (zero-based) at
which the strings differ, if they differ, and otherwise is their common
length.  See STRING<.

The guard for string<= specifies that its arguments are strings.

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

STRING>    greater-than test for strings

(String> str1 str2) is non-nil if and only if str2 precedes str1
lexicographically.  When non-nil, (string> str1 str2) is the first
position (zero-based) at which the strings differ.  See STRING<.

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

STRING>=    less-than-or-equal test for strings

(String>= str1 str2) is non-nil if and only if the string str2 precedes
the string str1 lexicographically or the strings are equal.  When
non-nil, (string>= str1 str2) is the first position (zero-based) at
which the strings differ, if they differ, and otherwise is their common
length.  See STRING>.

The guard for string>= specifies that its arguments are strings.

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

STRINGP    recognizer for strings

(stringp x) is true if and only if x is a string.

STRIP-CARS    collect up all first components of pairs in a list

(strip-cars x) is the list obtained by walking through the list x and
collecting up all first components (cars).  This function is
implemented in a tail-recursive way, despite its logical definition.

(strip-cars x) has a guard of (alistp x).

STRIP-CDRS    collect up all second components of pairs in a list

(strip-cdrs x) has a guard of (alistp x), and returns the list obtained
by walking through the list x and collecting up all second components
(cdrs).  This function is implemented in a tail-recursive way, despite
its logical definition.

SUBLIS    substitute an alist into a tree

(Sublis alist tree) is obtained by replacing every leaf of tree with
the result of looking that leaf up in the association list alist.
However, a leaf is left unchanged if it is not found as a key in alist.

Leaves are lookup up using the function assoc.  The guard for (sublis
alist tree) requires (eqlable-alistp alist).  This guard ensures that
the guard for assoc will be met for each lookup generated by sublis.

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

SUBSEQ    subsequence of a string or list

For any natural numbers start and end, where start <= end <= (length
seq), (subseq seq start end) is the subsequence of seq from index start
up to, but not including, index end.  End may be nil, which which case
it is treated as though it is (length seq), i.e., we obtain the
subsequence of seq from index start all the way to the end.

The guard for (subseq seq start end) is that seq is a true list or a
string, start and end are integers (except, end may be nil, in which
case it is treated as (length seq) for ther rest of this discussion),
and 0 <= start <= end <= (length seq).

Subseq is a Common Lisp function.  See any Common Lisp documentation
for more information.  Note:  In Common Lisp the third argument of
subseq is optional, but in ACL2 it is required, though it may be nil as
explained above.

SUBSETP    test if every member of one list is a member of the other

(Subsetp x y) is true if and only if every member of the list x is a
member of the list y.

Membership is tested using the function member.  Thus, the guard for
subsetp requires that its arguments are true lists, and moreover, at
least one satisfies eqlable-listp.  This guard ensures that the guard
for member will be met for each call generated by subsetp.

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

SUBSETP-EQUAL    check if all members of one list are members of the other

(Subsetp-equal x y) returns t if every member of x is a member of y,
where membership is tested using member-equal.

The guard for subsetp-equal requires both arguments to be true lists.
Subsetp-equal has the same functionality as the Common Lisp function
subsetp, except that it uses the equal function to test membership
rather than eql.

SUBST    a single substitution into a tree

(Subst new old tree) is obtained by substituting new for every
occurence of old in the given tree.

Equality to old is determined using the function eql.  The guard for
(subst new old tree) requires (eqlablep old), which ensures that the
guard for eql will be met for each comparison generated by subst.

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

SUBSTITUTE    substitute into a string or a list, using eql as test

(Substitute new old seq) is the result of replacing each occurrence of
old in seq, which is a list or a string, with new.

The guard for substitute requires that either seq is a string and new
is a character, or else:  seq is a true-listp such that either all of
its members are eqlablep or old is eqlablep.

Substitute is a Common Lisp function.  See any Common Lisp
documentation for more information.  Since ACL2 functions cannot take
keyword arguments (though macros can), the test used in substitute is
eql.

SYMBOL-<    less-than test for symbols

(symbol-< x y) is non-nil if and only if either the symbol-name of the
symbol x lexicographially precedes the symbol-name of the symbol y (in
the sense of string<) or else the symbol-names are equal and the
symbol-package-name of x lexicographically precedes that of y (in the
same sense).  So for example, (symbol-< 'abcd 'abce) and (symbol-<
'acl2::abcd 'foo::abce) are true.

The guard for symbol specifies that its arguments are symbols.

SYMBOL-ALISTP    recognizer for association lists with symbols as keys

(Symbol-alistp x) is true if and only if x is a list of pairs of the
form (cons key val) where key is a symbolp.

SYMBOL-LISTP    recognizer for a true list of symbols

The predicate symbol-listp tests whether its argument is a true list of
symbols.

SYMBOL-NAME    the name of a symbol (a string)

Completion Axiom:

     (equal (symbol-name x)
            (if (symbolp x)
                (symbol-name x)
              ""))

Guard for (symbol-name x):

     (symbolp x)

SYMBOL-PACKAGE-NAME    the name of the package of a symbol (a string)

Completion Axiom:

     (equal (symbol-package-name x)
            (if (symbolp x)
                (symbol-package-name x)
              ""))

Guard for (symbol-package-name x):

     (symbolp x)

Note:  If the ACL2 image is built on GCL, then symbol-package-name
diverges from the name of the symbol's package in raw Lisp, in the case
that this package is the main Lisp package.  For example,
(symbol-package-name 'car) evaluates to "COMMON-LISP" regardless of of
the underlying Lisp implementation, even though the name of the main
Lisp package in GCL is "LISP".

SYMBOLP    recognizer for symbols

(symbolp x) is true if and only if x is a symbol.

SYS-CALL    make a system call to the host operating system

     Example Forms:
     (sys-call "cp" '("foo.lisp" "foo-copied.lisp"))
     (prog2$ (sys-call "cp" '("foo.lisp" "foo-copied.lisp"))
             (sys-call-status state))

The first argument of sys-call is a command for the host operating
system, and the second argument is a list of strings that are the
arguments for that command.  In GCL and perhaps other lisps, you can
put the arguments with the command; but this is not the case, for
example, in Allegro CL running on Linux.

The use of prog2$ above is optional, but illustrates a typical sort of
use when one wishes to get the return status.  See
SYS-CALL-STATUS.

     General Form:
     (sys-call cmd args)

This function logically returns nil.  However, it makes the indicated
call to the host operating system, as described above, using a function
supplied "under the hood" by the underlying Lisp system.  On occasions
where one wishes to obtain the numeric status returned by the host
operating system (or more precisely, by the Lisp function under the
hood that passes the system call to the host operating system), one may
do so;  see SYS-CALL-STATUS.  The status value is the value
returned by that Lisp function, which may well be the same numeric
value returned by the host operating system for the underlying system
call.

Note that sys-call does not touch the ACL2 state; however,
sys-call-status updates the file-clock field of the state.  One may
view that update as modifying the fileclock to be at least as recent as
the time of the most recent sys-call.

Be careful if you use sys-call!  It can be used for example to overwrite
files, or worse!  The following example from Bob Boyer shows how to use
sys-call to execute, in effect, arbitrary Lisp forms.  ACL2 provides a
"trust tag" mechanism that requires execution of a defttag form before
you can use sys-call; see DEFTTAG.  (Note: The setting of the
raw Lisp variable *features* below is just to illustrate that any such
mischief is possible.  Normally *features* is a list with more than a
few elements.)

     % cat foo
     print *0x85d2064=0x838E920
     detach
     q
     % acl2
     ... boilerplate deleted
     ACL2 !>(sys-call "gdb -p $PPID -w < foo >& /dev/null " nil)
     NIL
     ACL2 !>:q

     Exiting the ACL2 read-eval-print loop.  To re-enter, execute (LP).
     ACL2>*features*

     (:AKCL-SET-MV)

     ACL2>

Finally, we make a comment about output redirection, which also applies
to other related features that one may expect of a shell.  Sys-call
does not directly support output redirection.  If you want to run a
program, P, and redirect its output, we suggest that you create a
wrapper script, W to call instead.  Thus W might be a shell script
containing the line:

     P $* >& foo.out

If this sort of solution proves inadequate, please contact the ACL2
implementors and perhaps we can come up with a solution.

SYS-CALL-STATUS    exit status from the preceding system call

This function returns two values, (mv status state).  The first is the
status returned by the most recent invocation of function sys-call; see
SYS-CALL.  The second is the ACL2 state object, which is also
the input to this function.

The function sys-call makes a system call to the host operating system
using a function supplied "under the hood" by the underlying Lisp
system.  The status value is the value returned by that Lisp function,
which may well be the same numeric value returned by the host operating
system for the underlying system call.  For more information, see
SYS-CALL.

TAKE    initial segment of a list

For any natural number n not exceeding the length of l, (take n l)
collects the first n elements of the list l.

The following is a theorem (though it takes some effort, including
lemmas, to get ACL2 to prove it):

     (equal (length (take n l)) (nfix n))

If n is is an integer greater than the length of l, then take pads the
list with the appropriate number of nil elements.  Thus, the following
is also a theorem.

     (implies (and (integerp n)
                   (true-listp l)
                   (<= (length l) n))
              (equal (take n l)
                     (append l (make-list (- n (length l))))))

For related functions, see NTHCDR and see BUTLAST.

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

TENTH    tenth member of the list

See any Common Lisp documentation for details.

THE    run-time type check

(The typ val) checks that val satisfies the type specification typ (see
TYPE-SPEC).  An error is caused if the check fails, and
otherwise, val is the value of this expression.  Here are some examples.

     (the integer 3)       ; returns 3
     (the (integer 0 6) 3) ; returns 3
     (the (integer 0 6) 7) ; causes an error

See TYPE-SPEC for a discussion of the legal type specifications.

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

THIRD    third member of the list

See any Common Lisp documentation for details.

TRUE-LIST-LISTP    recognizer for true (proper) lists of true lists

True-list-listp is the function that checks whether its argument is a
list that ends in, or equals, nil, and furthermore, all of its elements
have that property.  Also see TRUE-LISTP.

TRUE-LISTP    recognizer for proper (null-terminated) lists

True-listp is the function that checks whether its argument is a list
that ends in, or equals, nil.

TRUNCATE    division returning an integer by truncating toward 0

     Example Forms:
     ACL2 !>(truncate 14 3)
     4
     ACL2 !>(truncate -14 3)
     -4
     ACL2 !>(truncate 14 -3)
     -4
     ACL2 !>(truncate -14 -3)
     4
     ACL2 !>(truncate -15 -3)
     5

(Truncate i j) is the result of taking the quotient of i and j and
dropping the fraction.  For example, the quotient of -14 by 3 is -4
2/3, so dropping the fraction 2/3, we obtain a result for (truncate -14
3) of -4.

The guard for (truncate i j) requires that i and j are rational (real,
in ACL2(r)) numbers and j is non-zero.

Truncate is a Common Lisp function.  However, note that unlike Common
Lisp, the ACL2 truncate function returns only a single value,

TYPE-SPEC    type specifiers in declarations

     Examples:
     The symbol INTEGER in (declare (type INTEGER i j k)) is a type-spec.  Other
     type-specs supported by ACL2 include RATIONAL, COMPLEX, (INTEGER 0 127),
     (RATIONAL 1 *), CHARACTER, and ATOM.

The type-specs and their meanings (when applied to the variable x as in
(declare (type type-spec x)) are given below.

     type-spec              meaning
     (AND type1 ... typek)  (AND (p1 X) ... (pk X))
                            where (pj x) is the meaning for type-spec typej
     ATOM                   (ATOM X)
     BIT                    (OR (EQUAL X 1) (EQUAL X 0))
     CHARACTER              (CHARACTERP X)
     COMPLEX,               (AND (COMPLEX-RATIONALP X)
     (COMPLEX RATIONAL)          (RATIONALP (REALPART X))
                                 (RATIONALP (IMAGPART X)))
     (COMPLEX type)         (AND (COMPLEX-RATIONALP X)
                                 (p (REALPART X))
                                 (p (IMAGPART X)))
                            where (p x) is the meaning for type-spec type
     CONS                   (CONSP X)
     INTEGER                (INTEGERP X)
     (INTEGER i j)          (AND (INTEGERP X)   ; See notes below
                                 (<= i X)
                                 (<= X j))
     (MEMBER x1 ... xn)     (MEMBER X '(x1 ... xn))
     (MOD i)                same as (INTEGER 0 i-1)
     NIL                    NIL
     (NOT type)             (NOT (p X))
                            where (p x) is the meaning for type-spec type
     NULL                   (EQ X NIL)
     (OR type1 ... typek)   (OR (p1 X) ... (pk X))
                            where (pj x) is the meaning for type-spec typej
     RATIO                  (AND (RATIONALP X) (NOT (INTEGERP X)))
     RATIONAL               (RATIONALP X)
     (RATIONAL i j)         (AND (RATIONALP X)  ; See notes below
                                 (<= i X)
                                 (<= X j))
     REAL                   (RATIONALP X)       ; (REALP X) in ACL2(r)
     (REAL i j)             (AND (RATIONALP X)  ; See notes below
                                 (<= i X)
                                 (<= X j))
     (SATISFIES pred)       (pred X) ; Lisp requires a unary function, not a macro
     SIGNED-BYTE            (INTEGERP X)
     (SIGNED-BYTE i)        same as (INTEGER -2**i-1 (2**i-1)-1)
     STANDARD-CHAR          (STANDARD-CHARP X)
     STRING                 (STRINGP X)
     (STRING max)           (AND (STRINGP X) (EQUAL (LENGTH X) max))
     SYMBOL                 (SYMBOLP X)
     T                      T
     UNSIGNED-BYTE          same as (INTEGER 0 *)
     (UNSIGNED-BYTE i)      same as (INTEGER 0 (2**i)-1)

_Notes:_

In general, (integer i j) means

          (AND (INTEGERP X)
               (<= i X)
               (<= X j)).

But if i is the symbol *, the first inequality is omitted.  If j is the
symbol *, the second inequality is omitted.  If instead of being an
integer, the second element of the type specification is a list
containing an integer, (i), then the first inequality is made strict.
An analogous remark holds for the (j) case.  The RATIONAL and REAL type
specifiers are similarly generalized.

UNARY--    arithmetic negation function

Completion Axiom:

     (equal (unary-- x)
            (if (acl2-numberp x)
                (unary-- x)
              0))

Guard for (unary- x):

     (acl2-numberp x)

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

Calls of the macro - on one argument expand to calls of unary-; see
-.

UNARY-/    reciprocal function

Completion Axiom:

     (equal (unary-/ x)
            (if (and (acl2-numberp x)
                     (not (equal x 0)))
                (unary-/ x)
              0))

Guard for (unary-/ x):

     (and (acl2-numberp x)
          (not (equal x 0)))

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

Calls of the macro / on one argument expand to calls of unary-/; see
/.

UNION-EQ    union of two lists of symbols

(Union-eq x y) equals a list whose members (see MEMBER-EQ)
contains the members of x and the members of y.  More precisely, the
resulting list is the same as one would get by first deleting the
members of y from x, and then concatenating the result to the front of
y.

The guard for union-eq requires both arguments to be true lists, but in
fact further requires the first list to contain only symbols, as the
function member-eq is used to test membership (with eq).  See
UNION-EQUAL.

UNION-EQUAL    union of two lists

(Union-equal x y) equals a list whose members (see
MEMBER-EQUAL) contains the members of x and the members of y.  More
precisely, the resulting list is the same as one would get by first
deleting the members of y from x, and then concatenating the result to
the front of y.

The guard for union-equal requires both arguments to be true lists.
Essentially, union-equal has the same functionality as the Common Lisp
function union, except that it uses the equal function to test
membership rather than eql.  However, we do not include the function
union in ACL2, because the Common Lisp language does not specify the
order of the elements in the list that it returns.

UPDATE-NTH    modify a list by putting the given value at the given position

(Update-nth key val l) returns a list that is the same as the list l,
except that the value at the 0-based position key (a natural number) is
val.

If key is an integer at least as large as the length of l, then l will
be padded with the appropriate number of nil elements, as illustrated
by the following example.

     ACL2 !>(update-nth 8 'z '(a b c d e))
     (A B C D E NIL NIL NIL Z)

We have the following theorem.

     (implies (and (true-listp l)
                   (integerp key)
                   (<= 0 key))
              (equal (length (update-nth key val l))
                     (if (< key (length l))
                         (length l)
                       (+ 1 key))))

The guard of update-nth requires that its first (position) argument is
a natural number and its last (list) argument is a true list.

UPPER-CASE-P    recognizer for upper case characters

(Upper-case-p x) is true if and only if x is an upper case character,
i.e., a member of the list #A, #B, ..., #Z.

The guard for upper-case-p requires its argument to be a standard
character (see STANDARD-CHAR-P).

Upper-case-p is a Common Lisp function.  See any Common Lisp
documentation for more information.

WRITE-BYTE$    See IO.

ZERO-TEST-IDIOMS    how to test for 0

Below are six commonly used idioms for testing whether x is 0.  Zip and
zp are the preferred termination tests for recursions down the integers
and naturals, respectively.

     idiom       logical              guard              primary
                 meaning                              compiled code*

     (equal x 0)(equal x 0)        t                   (equal x 0)

     (eql x 0)  (equal x 0)        t                   (eql x 0)

     (zerop x)  (equal x 0)        x is a number       (= x 0)

     (= x 0)    (equal x 0)        x is a number       (= x 0)

     (zip x)    (equal (ifix x) 0) x is an integer     (= x 0)

     (zp x)     (equal (nfix x) 0) x is a natural      (int= x 0)

     (zpf x)    (equal (nfix x) 0) x is a fixnum >= 0  (eql (the-fixnum x) 0)

*See GUARDS-AND-EVALUATION, especially the subsection titled
"Guards and evaluation V: efficiency issues".  Primary code is relevant
only if guards are verified.  The "compiled code" shown is only
suggestive.

The first four idioms all have the same logical meaning and differ only
with respect to their executability and efficiency.  In the absence of
compiler optimizing, (= x 0) is probably the most efficient, (equal x
0) is probably the least efficient, and (eql x 0) is in between.
However, an optimizing compiler could always choose to compile (equal x
0) as (eql x 0) and, in situations where x is known at compile-time to
be numeric, (eql x 0) as (= x 0).  So efficiency considerations must, of
course, be made in the context of the host compiler.

Note also that (zerop x) and (= x 0) are indistinguishable.  They have
the same meaning and the same guard, and can reasonably be expected to
generate equally efficient code.

Note that (zip x) and (zp x) do not have the same logical meanings as
the others or each other.  They are not simple tests for equality to 0.
They each coerce x into a restricted domain, zip to the integers and
zp to the natural numbers, choosing 0 for x when x is outside the
domain.  Thus, 1/2, #c(1 3), and 'abc, for example, are all
"recognized" as zero by both zip and zp.  But zip reports that -1 is
different from 0 while zp reports that -1 "is" 0.  More precisely, (zip
-1) is nil while (zp -1) is t.

Note that the last five idioms all have guards that restrict their
Common Lisp executability.  If these last five are used in situations
in which guards are to be verified, then proof obligations are incurred
as the price of using them.  If guard verification is not involved in
your project, then the first five can be thought of as synonymous.

Zip and zp are not provided by Common Lisp but are ACL2-specific
functions.  Why does ACL2 provide these functions?  The answer has to
do with the admission of recursively defined functions and efficiency.
Zp is provided as the zero-test in situations where the controlling
formal parameter is understood to be a natural number.  Zip is
analogously provided for the integer case.  We illustrate below.

Here is an admissible definition of factorial

     (defun fact (n) (if (zp n) 1 (* n (fact (1- n)))))

Observe the classic recursion scheme: a test against 0 and recursion by
1-.  Note however that the test against 0 is expressed with the zp
idiom.  Note also the absence of a guard making explicit our intention
that n is a natural number.

This definition of factorial is readily admitted because when (zp n)

is false (i.e., nil) then n is a natural number other than 0 and so (1-
n) is less than n.  The base case, where (zp n) is true, handles all
the "unexpected" inputs, such as arise with (fact -1) and (fact 'abc).
When calls of fact are evaluated, (zp n) checks (integerp n) and (> n
0).  Guard verification is unsuccessful for this definition of fact
because zp requires its argument to be a natural number and there is no
guard on fact, above.  Thus the primary raw lisp for fact is
inaccessible and only the :logic definition (which does runtime "type"
checking) is used in computation.  In summary, this definition of
factorial is easily admitted and easily manipulated by the prover but
is not executed as efficiently as it could be.

Runtime efficiency can be improved by adding a guard to the definition.

     (defun fact (n)
       (declare (xargs :guard (and (integerp n) (>= n 0))))
       (if (zp n) 1 (* n (fact (1- n)))))

This guarded definition has the same termination conditions as before -
termination is not sensitive to the guard.  But the guards can be
verified.  This makes the primary raw lisp definition accessible during
execution.  In that definition, the (zp n) above is compiled as (= n
0), because n will always be a natural number when the primary code is
executed.  Thus, by adding a guard and verifying it, the elegant and
easily used definition of factorial is also efficiently executed on
natural numbers.

Now let us consider an alternative definition of factorial in which (=
n 0) is used in place of (zp n).

     (defun fact (n) (if (= n 0) 1 (* n (fact (1- n)))))

This definition does not terminate.  For example (fact -1) gives rise
to a call of (fact -2), etc.  Hence, this alternative is inadmissible.
A plausible response is the addition of a guard restricting n to the
naturals:

     (defun fact (n)
      (declare (xargs :guard (and (integerp n) (>= n 0))))
      (if (= n 0) 1 (* n (fact (1- n)))))

But because the termination argument is not sensitive to the guard, it
is still impossible to admit this definition.  To influence the
termination argument one must change the conditions tested.  Adding a
runtime test that n is a natural number would suffice and allow both
admission and guard verification.  But such a test would slow down the
execution of the compiled function.

The use of (zp n) as the test avoids this dilemma.  Zp provides the
logical equivalent of a runtime test that n is a natural number but the
execution efficiency of a direct = comparison with 0, at the expense of
a guard conjecture to prove.  In addition, if guard verification and
most-efficient execution are not needed, then the use of (zp n) allows
the admission of the function without a guard or other extraneous
verbiage.

While general rules are made to be broken, it is probably a good idea
to get into the habit of using (zp n) as your terminating "0 test"
idiom when recursing down the natural numbers.  It provides the logical
power of testing that n is a non-0 natural number and allows efficient
execution.

We now turn to the analogous function, zip.  Zip is the preferred
0-test idiom when recursing through the integers toward 0.  Zip
considers any non-integer to be 0 and otherwise just recognizes 0.  A
typical use of zip is in the definition of integer-length, shown below.
(ACL2 can actually accept this definition, but only after appropriate
lemmas have been proved.)

     (defun integer-length (i)
       (declare (xargs :guard (integerp i)))
       (if (zip i)
           0
         (if (= i -1)
           0
           (+ 1 (integer-length (floor i 2))))))

Observe that the function recurses by (floor i 2).  Hence, calling the
function on 25 causes calls on 12, 6, 3, 1, and 0, while calling it on
-25 generates calls on -13, -7, -4, -2, and -1.  By making (zip i) the
first test, we terminate the recursion immediately on non-integers.
The guard, if present, can be verified and allows the primary raw lisp
definition to check (= i 0) as the first terminating condition (because
the primary code is executed only on integers).

ZEROP    test an acl2-number against 0

(zerop x) is t if x is 0 and is nil otherwise.  Thus, it is logically
equivalent to (equal x 0).

(Zerop x) has a guard requiring x to be numeric and can be expected to
execute more efficiently than (equal x 0) in properly guarded compiled
code.

In recursions down the natural numbers, (zp x) is preferred over (zerop
x) because the former coerces x to a natural and allows the termination
proof.  In recursions through the integers, (zip x) is preferred.  See
ZERO-TEST-IDIOMS.

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

ZIP    testing an ``integer'' against 0

(Zip i) is logically equivalent to (equal (ifix i) 0) and is the
preferred termination test for recursion through the integers.  (Zip i)
returns t if i is 0 or not an integer; it returns nil otherwise.  Thus,

        i         (zip i)
        3         nil
        0         t
        -2        nil
        5/2       t
        #c(1 3)   t
        'abc      t

(Zip i) has a guard requiring i to be an integer.

For a discussion of the various idioms for testing against 0, see
ZERO-TEST-IDIOMS.

Zip is typically used as the termination test in recursions through the
integers.  It has the advantage of "coercing" its argument to an
integer and hence allows the definition to be admitted without an
explicit type check in the body.  Guard verification allows zip to be
compiled as a direct =-comparision with 0.

ZP    testing a ``natural'' against 0

(Zp n) is logically equivalent to (equal (nfix n) 0) and is the
preferred termination test for recursion down the natural numbers. (Zp
n) returns t if n is 0 or not a natural number; it returns nil
otherwise.  Thus, in the ACL2 logic (ignoring the issue of guards):

         n       (zp n)
        3         nil
        0         t
        -1        t
        5/2       t
        #c(1 3)   t
        'abc      t

(Zp n) has a guard requiring n to be a natural number.

For a discussion of the various idioms for testing against 0, see
ZERO-TEST-IDIOMS.

Zp is typically used as the termination test in recursions down the
natural numbers.  It has the advantage of "coercing" its argument to a
natural and hence allows the definition to be admitted without an
explicit type check in the body.  Guard verification allows zp to be
compiled as a direct =-comparision with 0.

ZPF    testing a nonnegative fixnum against 0

Zpf is exactly the same as zp, except that zpf is intended for, and
faster for, fixnum arguments.  Its guard is specified with a type
declaration, (type (unsigned-byte 28) x).  (See DECLARE and see
TYPE-SPEC.)  Also see ZP.

PROOF-CHECKER    support for low-level interaction

Call this up with (verify ...).

This is an interactive system for checking theorems in ACL2.  One
enters it using VERIFY; see VERIFY.  The result of an
interactive session is a defthm event with an :instructions parameter
supplied; see the documentation for proof-checker command exit (in
package "ACL2-PC").  Such an event can be replayed later in a new ACL2
session with the "proof-checker" loaded.

A tutorial is available on the world-wide web:

     http://www.cs.utexas.edu/users/kaufmann/tutorial/rev3.html

The tutorial illustrates more than just the proof-checker.  The portion
relevant to the proof-checker may be accessed directly:

     http://www.cs.utexas.edu/users/kaufmann/tutorial/rev3.html#slide29

Individual proof-checker commands are documented in subsection
proof-checker-commands.

DEFINE-PC-HELP    define a macro command whose purpose is to print something

     Example:
     (define-pc-help pp ()
       (if (goals t)
           (io? proof-checker nil state
                (state-stack)
                (fms0 "~|~y0~|"
                      (list (cons #0
                                  (fetch-term (conc t)
                                              (current-addr t))))))
         (print-all-goals-proved-message state)))

     General Form:
     (define-pc-help name args &rest body)

This defines a macro command named name, as explained further below.
The body should (after removing optional declarations) be a form that
returns state as its single value.   Typically, it will just print
something.

What (define-pc-help name args &rest body) really does is to create a
call of define-pc-macro that defines name to take arguments args, to
have the declarations indicated by all but the last form in body, and
to have a body that (via pprogn) first executes the form in the last
element of body and then returns a call to the command skip (which will
return (mv nil t state)).

DEFINE-PC-MACRO    define a proof-checker macro command

     Example:
     (define-pc-macro ib (&optional term)
       (value
        (if term
            `(then (induct ,term) bash)
          `(then induct bash))))

The example above captures a common paradigm:  one attempts to prove
the current goal by inducting and then simplifying the resulting goals.
(see PROOF-CHECKER-COMMANDS for documentation of the command
then, which is itself a pc-macro command, and commands induct and
bash.)  Rather than issuing (then induct bash), or worse yet issuing
induct and then issuing bash for each resulting goals, the above
definition of ib would let you issue ib and get the same effect.

     General Form:
     (define-pc-macro cmd args doc-string dcl ... dcl body)

where cmd is the name of the pc-macro than you want to define, args is
its list of formal parameters.  Args may include lambda-list keywords
&optional and &rest; see MACRO-ARGS, but note that here, args
may not include &key or &whole.

The value of body should be an ACL2 "error triple," i.e., have the form
(mv erp xxx state) for some erp and xxx.  If erp is nil, then xxx is
handed off to the proof-checker's instruction interpreter.  Otherwise,
evaluation typically halts.  We may write more on the full story later
if there is interest in reading it.

DEFINE-PC-META    define a proof-checker meta command

Built-in proof-checker meta commands include undo and restore, and
others (lisp, exit, and sequence); see PROOF-CHECKER-COMMANDS.
The advanced proof-checker user can define these as well.  See ACL2
source file proof-checker-b.lisp for examples, and contact the ACL2
implementors if those examples do not provide sufficient documentation.

INSTRUCTIONS    instructions to the proof checker

     Example:
     :instructions (induct prove promote (dive 1) x
                           (dive 2) = top (drop 2) prove)

See DEFTHM for the role of :instructions in place of :hints.
As illustrated by the example above, the value associated with
:instructions is a list of proof-checker commands.  At the moment the
best way to understand the idea of the interactive proof-checker (see
PROOF-CHECKER and see VERIFY) is probably to read the
first 11 pages of CLI Technical Report 19, which describes the
corresponding facility for Nqthm.

When inside the interactive loop (i.e., after executing verify), use
help to get a list of legal instructions and (help instr) to get help
for the instruction instr.

MACRO-COMMAND    compound command for the proof-checker

The proof-checker (see PROOF-CHECKER) allows the user to supply
interactive commands.  Compound commands, called macro commands, may be
defined; these expand into zero or more other commands.  Some of these
are "atomic" macro commands; these are viewed as a single command step
when completed successfully.

More documentation will be written on the proof-checker.  For now, we
simply point out that there are lots of examples of the use of
define-pc-macro and define-pc-atomic-macro in the ACL2 source file
"proof-checker-b.lisp".  The former is used to create macro commands,
which can be submitted to the interactive loop (see VERIFY) and
will "expand" into zero or more commands.  The latter is similar,
except that the undoing mechanism (see ACL2-PC||UNDO)
understands atomic macro commands to represent single interactive
commands.  Also see ACL2-PC||COMM and see
ACL2-PC||COMMANDS for a discussion of the display of interactive
commands.

Also see TOGGLE-PC-MACRO for how to change a macro command to
an atomic macro command, and vice versa.