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.

GUARD-EVALUATION-EXAMPLES-SCRIPT    a script to show combinations of defun-modes and guard-checking

Below is a script that illustrates the combination of defun-modes ---
:program mode, :logic mode without guards verified, and :logic mode with
guards verified -- with values from set-guard-checking -- t (the
default), :all, :none, and nil.  (It does not illustrate the value
:nowarn, which is the same as t except for inhibiting a warning.)  The
script also illustrates cases where the guard is not, or is, t.

See GUARD-EVALUATION-EXAMPLES-LOG for result of running this
script.  Before presenting the script below, we give some instructions
in case you want to run it yourself.

See SET-GUARD-CHECKING for discussion of the interaction between
defun-modes and guard-checking that is illustrated by this script.  Also
see GUARD-EVALUATION-TABLE for a succinct table, with associated
discussion, that covers in detail the interactions illustrated here.

The script mentions the running of "Tracing Code".  The code is the
following sequence of commands.

     (trace$ fact)
     :set-guard-checking t
     (fact 2)
     (fact t)
     :set-guard-checking :all
     (fact 2)
     (fact t)
     :set-guard-checking :none
     (fact 2)
     (fact t)
     :set-guard-checking nil
     (fact 2)
     (fact t)

If you want to run the script yourself, you may find it handy to use the
following Emacs keyboard macro for running the tracing code in 2-window
mode, with the cursor in the window with the script and ACL2 running in
the other window.

     (fset 'step-guard-script
        [?C-a ?C-  ?C-e ?M-w ?C-a ?C-n
         ?C-x ?o ?M-> ?C-y return ?C-x ?o])

     ; Put it on a key (if you have defined the indicated keymap by using
     ; emacs/emacs-acl2.el):
     (define-key ctl-t-keymap "r" 'step-guard-script)

The script follows.

     ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
     ;;; Program mode
     ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

     (defun fact (x)
              (declare (xargs :guard (integerp x)
                              :mode :program))
              (if (posp x)
                  (* x (fact (1- x)))
                1))

     ; Run the Tracing Code here.  It shows execution in raw Lisp in the t and nil
     ; cases of :set-guard-checking, but not in the :all or :none cases.  We get a
     ; guard violation for argument t in the case :set-guard-checking t.

     :u

     (defun fact (x)
              (declare (xargs :guard t
                              :mode :program))
              (if (posp x)
                  (* x (fact (1- x)))
                1))

     ; Run the Tracing Code here.  It should give the same results as above,
     ; except that we no longer get a guard violation in the case
     ; :set-guard-checking t.

     :u

     ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
     ;;; Logic mode, guard other than t
     ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

     (defun fact (x)
              (declare (xargs :guard (integerp x)
                              :verify-guards nil
                              :mode :logic))
              (if (posp x)
                  (* x (fact (1- x)))
                1))

     ; Run the Tracing Code here.  It should give guard violations for (fact t)
     ; with guard-checking set to t or :all.  It should never run in raw Lisp,
     ; because we have not verified guards.  In the t case, we should get a
     ; warning about avoiding the guard check on recursive calls.

     (verify-guards fact)

     ; Run the Tracing Code here.  The results should be as described just above,
     ; except that now we go into raw Lisp for (fact 2) with guard-checking other
     ; than :none.

     :u
     :u

     ; The following definition is the same as above, except that guards are
     ; verified.

     (defun fact (x)
              (declare (xargs :guard (integerp x)
                              :mode :logic))
              (if (posp x)
                  (* x (fact (1- x)))
                1))

     ; Run the Tracing Code here.  We should get the same traces as in the
     ; immediately preceding case, since guards had been verified in both cases.

     :u

     ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
     ;;; Logic mode, guard t
     ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

     (defun fact (x)
              (declare (xargs :guard t
                              :verify-guards nil
                              :mode :logic))
              (if (posp x)
                  (* x (fact (1- x)))
                1))

     ; Run the Tracing Code here.  We should never go in to raw Lisp, because
     ; guards have not been verified.  We will see the same traces for (fact 2) as
     ; with the (integerp x) guard above with :verify-guards nil specified, except
     ; that there is no warning for :set-guard-checking t about recursive calls.
     ; And, there are no guard violations for (fact t), of course, since posp
     ; (necessarily, if we are to verify guards) has a guard of t.

     (verify-guards fact)

     ; Run the Tracing Code here.  Now that guards have been verified, the :none
     ; trace for (fact 2) differs from the corresponding (guard-verified) trace
     ; for guard (integerp x) because now the guard is t, so we can (and do) go
     ; directly into raw Lisp without the need to check the guard.  The (fact 2)
     ; traces other than for :none are the same as in the corresponding trace for
     ; guard (integerp x).  And of course (fact t) now computes without guard
     ; violations, and using raw Lisp even in the :none case,

GUARD-EVALUATION-TABLE    a table that shows combinations of defun-modes and guard-checking

See SET-GUARD-CHECKING for an introduction to the topic
discussed here.  Also see GUARD for a general discussion of
guards, and see GUARD-EVALUATION-EXAMPLES-SCRIPT for a script
that illustrates combinations presented below.

The table below illustrates the interaction of the defun-mode with the
value supplied to set-guard-checking.  The first row considers functions
defined in :program mode; the other two consider functions defined in
:logic mode.  The columns correspond to four values of state global
'guard-checking-on, as supplied to set-guard-checking.  (A fifth value,
:nowarn, is similar to t but suppresses warnings encountered with t (as
explained in those warning messages), and is not considered here.)

Below this table, we make some comments about its entries, ordered by
row and then by column.  For example, when we refer to "b2" we are
discussing the execution of a :logic mode function whose guards have not
been verified, after having executed :set-guard-checking :all.

        guard-checking-on:  (1)t      (2):all   (3):none   (4)nil

      (a) :program             a1        a2        a3        a4
      (b) guards not verified  b1        b2        b3        b4
      (c) guards verified      c1        c2        c3        c4

a1. Check the guard upon entry, then use the raw Lisp code if the guard
checks (else cause an error).  This is a common setting when one wants a
little guard checking but also wants the efficiency of raw Lisp.  But
note that you can get raw Lisp errors.  For example, if you make the
definition (defun foo (x) (car x)) in :program mode and execute
:set-guard-checking t, and then execute (foo 3), you will likely get an
error from the call (car 3) made in raw Lisp.

a2. Check the guard, without exception.  Thus, we never run the raw Lisp
code in this case.  This can be useful when testing :program mode
functions, but you may want to run :comp t or at least :comp :exec in
this case, so that the execution is done using compiled code.

a3. Do not check the guard.  For :program mode functions, we never run
the raw Lisp code in this case; so if you care about efficiency, see the
comment in a2 above about :comp.  This combination is useful if you are
using ACL2 as a programming language and do not want to prove theorems
about your functions or suffer guard violations.  In this case, you can
forget about any connection between ACL2 and Common Lisp.

a4. Run the raw Lisp code without checking guards at all.  Thus, for
:program mode functions, the nil setting is often preferable to the
:none setting because you get the efficiency of raw Lisp execution.
However, with nil you can therefore get hard Lisp errors as in a1 above.

b1. Guards are checked at the top-level, though not at self-recursive
calls.  We never run the raw Lisp code in this case; guards would need
to be verified first.

b2. Unlike the t setting, guards are checked even on self-recursive
calls.  But like the t setting, we do not run the raw Lisp code.  Use
this setting if you want guards checked on each recursive call in spite
of the cost of doing so.

b3, b4. Execution avoids the raw Lisp code and never checks guards.  The
nil and :none settings behave the same in this case (i.e., for :logic
mode functions whose guards have not been verified).

c1, c2. Guards are checked.  If the checks pass, evaluation takes place
using the raw Lisp code.  If the checks fail, we get a guard violation.
Either way, we do not execute "in the logic"; we only execute using the
raw Lisp code.  Note that t and :all behave the same in this case,
(i.e. for :logic mode functions whose guards have been verified).

c3, c4. For the :none and nil settings, :logic mode functions whose
guards have been verified will never cause guard violations.  However,
with nil, guards are still checked: if the check succeeds, then
evaluation is done using the raw Lisp code, and if not, it is done by
the "logic" code, including self-recursive calls (though unlike the t
case, we will not see a warning about this).  But with :none, no guard
checking is done, so the only time the raw Lisp code will be executed is
when the guard is t (so that no evaluation is necessary).  Thus, if you
use :none and you want a function (foo x) with guard (g x) to execute
using raw Lisp code, you can write a "wrapper" function with a guard of
t:

     (defun foo-wrap (x)
       (if (g x)
           (foo x)
         'do-not-case))

If you want the speed of executing raw Lisp code and you have
non-trivial guards on functions that you want to call at the top-level,
use nil rather than :none.

GUARD-INTRODUCTION    introduction to guards in ACL2

Most users can probably profit by avoiding dealing with guards most of
the time.  If they seem to get in the way, they can be "turned off"
using the command :set-guard-checking nil; for more about this, see
SET-GUARD-CHECKING.  For more about guards in general, see
GUARD.

The guard on a function symbol is a formula about the formals of the
function.  To see the guard on a function, use the keyword command
:args.  See ARGS.  To specify the guard on a function at
defun-time, use the :guard xarg.  See XARGS.

Guards can be seen as having either of two roles: (a) they are a
specification device allowing you to characterize the kinds of inputs a
function "should" have, or (b) they are an efficiency device allowing
logically defined functions to be executed directly in Common Lisp.
Briefly: If the guards of a function definition are "verified" (see
VERIFY-GUARDS), then the evaluation of a call of that function
on arguments satisfying its guard will have the following property:

     All subsequent function calls during that evaluation will be on
     arguments satisfying the guard of the called function.

The consequence of this fact for (a) is that your specification function
is well-formed, in the sense that the values returned by this function
on appropriate arguments only depend on the restrictions of the called
functions to their intended domains.  The consequence of this fact for
(b) is that in the ACL2 system, when a function whose guards have been
verified is called on arguments that satisfy its guard, then the raw
lisp function defined by this function's defun event is used to evaluate
the call.  Note however that even when the user-supplied defun is not
used, ACL2 uses a corresponding "executable counterpart" that generally
performs, we expect, nearly as well as the raw lisp function.  See
COMP to see how compilation can speed up both kinds of execution.

Let us turn next to the issue of the relationship between guards and
evaluation.  See GUARDS-AND-EVALUATION.

GUARD-MISCELLANY    miscellaneous remarks about guards

The discussion of guards concludes here with a few miscellaneous
remarks.  (Presumably you found this documentation by following a link;
see GUARDS-FOR-SPECIFICATION.)  For further information related
to guards other than what you find under "guard," see any of the
following documentation topics: guard-example,
set-verify-guards-eagerness, set-guard-checking, and verify-guards.

Defun can be made to try to verify the guards on a function.  This is
controlled by the "defun-mode" of the defun; see DEFUN-MODE.
The defun-mode is either as specified with the :mode xarg of the defun
or else defaults to the default defun-mode.  See
DEFAULT-DEFUN-MODE.  If the defun-mode of the defun is :logic and
either a :guard is specified or :verify-guards t is specified in the
xargs, then we attempt to verify the guards of the function.  Otherwise
we do not.

It is sometimes impossible for the system to verify the guards of a
recursive function at definition time.  For example, the guard
conjectures might require the invention and proof of some inductively
derived property of the function (as often happens when the value of a
recursive call is fed to a guarded subroutine).  So sometimes it is
necessary to define the function using :verify-guards nil then to state
and prove key theorems about the function, and only then have the system
attempt guard verification.  Post-defun guard verification is achieved
via the event verify-guards.  See VERIFY-GUARDS.

It should be emphasized that guard verification affects only two things:
how fast ACL2 can evaluate the function and whether the function is
executed correctly by raw Common Lisp, without guard violations.  Since
ACL2 does not use the raw Common Lisp definition of a function to
evaluate its calls unless that function's guards have been verified, the
latter effect is felt only if you run functions in raw Common Lisp
rather than via ACL2's command loop.

Guard verification does not otherwise affect the theorem prover or the
semantics of a definition.  If you are not planning on running your
function on "big" inputs and you don't care if your function runs
correctly in raw Common Lisp (e.g., you have formalized some abstract
mathematical property and just happened to use ACL2 as your language),
there is no need to suffer through guard verification.  Often users
start by not doing guard verification and address that problem later.
Sometimes you are driven to it, even in mathematical projects, because
you find that you want to run your functions particularly fast or in raw
Common Lisp.

If certify-book is used to compile a file, and the file contains
functions with unverified guard conjectures, then you will be warned
that the compiled file cannot be loaded into raw Common Lisp with the
expectation that the functions will run correctly.  This is just the
same point we have been making: ACL2 and Common Lisp agree only on the
restricted domains specified by our guards.  When guards are violated,
Common Lisp can do anything.  When you call a compiled function on
arguments violating its guards, the chances are only increased that
Common Lisp will go berserk, because compiled functions generally check
fewer things at runtime and tend to be more fragile than interpreted
ones.

GUARD-QUICK-REFERENCE    brief summary of guard checking and guard verification

For a careful introduction to guards, see GUARD.

I. GUARD CHECKING DURING EXECUTION

*Effect*

Guards on definitions are checked at execution time (except for guards
on subsidiary calls of recursive or mutually recursive functions).

*When does it happen*

By default, guards are checked for all forms submitted at the top level.

*To disable*

:set-guard-checking nil ; skip raw Lisp if there is a guard violation
:set-guard-checking :none ; skip guard checking entirely

*To (re-)enable*

:set-guard-checking t

See SET-GUARD-CHECKING for more options.

II. GUARD VERIFICATION

*Effect*

A proof is attempted of the obligations arising from the guards of
subsidiary functions in a defun, defthm, or defaxiom event.  In the case
of a defun, the guard itself is also verified (under an implicit guard
of t).

*When does it happen*

Only names of defined functions, defthms, and defaxioms are subject to
guard verification.  Guard verification may occur when functions are
defined (using defun), but it requires an explicit call of verify-guards
in order to verify guards for defthms and defaxioms.  Constrained
functions (see ENCAPSULATE) may not have their guards verified.

(verify-guards foo ...)

causes guard verification for the defun, defthm, or defaxiom named by
foo, if it has not already been successfully done.  The default
defun-mode (see DEFAULT-DEFUN-MODE) must be :logic, or else this
event is ignored.

(defun foo ...)

causes guard verification of foo if and only if the following conditions
are both met.  (However, see SET-VERIFY-GUARDS-EAGERNESS for how
to change this behavior.)

     1. Foo is processed in :logic mode (either by setting mode :logic
     globally, or by including :mode :logic in the xargs declaration).

     2. The xargs declaration (see XARGS) either specifies
     :guard or specifies :verify-guards t (or both).

(verify-termination foo ...)

causes guard verification of foo if foo is a function currently defined
in :program mode and the appropriate xargs are supplied, as discussed
for the case of defun above.  The default defun-mode (see
DEFAULT-DEFUN-MODE) must be :logic, or else this event is ignored.

GUARDS-AND-EVALUATION    the relationship between guards and evaluation

The guard has no effect on the logical axiom added by the definition of
a function.  It does, however, have consequences for how calls of that
function are evaluated in ACL2.  We begin by explaining those
consequences, when ACL2 is in its default "mode," i.e., as originally
brought up.  In subsequent discussion we'll consider other ways that
guards can interact with evaluation.

For more about guards in general, see GUARD.  For in-depth
discussion of the interaction between the defun-mode and guard checking,
see SET-GUARD-CHECKING, see GUARD-EVALUATION-TABLE, see
GUARD-EVALUATION-EXAMPLES-SCRIPT, and see
GUARD-EVALUATION-EXAMPLES-LOG.  Also see GENERALIZED-BOOLEANS
for discussion about a subtle issue in the evaluation of certain Common
Lisp functions.

*Guards and evaluation I: the default*

Consider the following very simple definition.

     (defun foo (x) (cons 1 (cdr x)))

First consider how raw Common Lisp behaves when evaluating calls of this
function.  To evaluate (foo x) for some expression x, first x is
evaluated to some value v, and then (cons 1 (cdr x)) is evaluated with x
bound to v.  For example, if v is (cons 'a 3), then Common Lisp computes
(cons 1 3).  But if (for example) v is a number, e.g., 7, then there is
no way to predict what Common Lisp might do.  Some implementations would
cause "sensible" errors, others might return nonsense, still others
might crash the host machine.  The results tend toward the catastrophic
if the call of foo in question is in compiled code.

Now by default, ACL2 evaluates calls of foo exactly as Common Lisp does,
except that it uses guards to check the "legality" of each function
call.  So for example, since (cdr x) has a guard of (or (consp x) (equal
x nil)), the call (foo 7) would cause a "guard violation," as
illustrated below.

     ACL2 !>(foo 7)

     ACL2 Error in TOP-LEVEL:  The guard for the function symbol CDR, which
     is (OR (CONSP X) (EQUAL X NIL)), is violated by the arguments in the
     call (CDR 7).

     ACL2 !>

Thus, the relation between evaluation in ACL2 and evaluation in Common
Lisp is that the two produce the very same results, provided there is no
guard violation.

*Guards and evaluation II:* :set-guard-checking.

The ACL2 logic is a logic of total functions.  That is, every
application of a function defined has a completely specified result.
See the documentation for each individual primitive for the
specification of what it returns when its guard is violated; for
example, see CDR.

The presence of guards thus introduces a choice in the sense of
evaluation.  When you type a form for evaluation do you mean for guards
to be checked or not?  Put another way, do you mean for the form to be
evaluated in Common Lisp (if possible) or in the ACL2 logic?  Note: If
Common Lisp delivers an answer, it will be the same as in the logic, but
it might be erroneous to execute the form in Common Lisp.  For example,
the ACL2 logic definition of cdr implies that the cdr of an atom is nil;
see CDR.  So: should (cdr 7) cause a guard violation error or
return nil?

The top-level ACL2 loop has a variable which controls which sense of
execution is provided.  By default, "guard checking" is on, by which we
mean that guards are checked at runtime, in the sense already described.
To allow execution to proceed in the logic when there is a guard
violation, do :set-guard-checking nil; or evaluate :set-guard-checking
:none to skip guard checking entirely.  To turn "guard checking" back
on, execute the top-level form :set-guard-checking t.  The status of
guard checking reflected in the prompt; guard-checking is "on" when the
prompt contains an exclamation mark (also see
DEFAULT-PRINT-PROMPT).  For example,

     ACL2 !>

means guard checking is on and

     ACL2 >

means guard checking is off.  The exclamation mark can be thought of as
"barring" certain computations.  The absence of the mark suggests the
absence of error messages or unbarred access to the logical axioms.
Thus, for example

     ACL2 !>(car 'abc)

will signal an error, while

     ACL2 >(car 'abc)

will return nil.  To return to our previous example: with guard checking
off, (foo 7) evaluates to (cons 1 nil).  Also see
SET-GUARD-CHECKING.

*Guards and evaluation III: guard verification*

Consider the defininition of foo given above, but modified so that a
reasonable guard of (consp x) is specified, as shown below.

     (defun foo (x)
       (declare (xargs :guard (consp x)))
       (cons 1 (cdr x)))

We say "reasonable guard" above because if x is such that (consp x)
holds, then the call of cdr in the evaluation of (foo x) will not cause
a guard violation.  Thus, it "should" be legal to evaluate (foo x), for
any such x, simply by evaluating this form in raw Common Lisp.

The verify-guards event has been provided for this purpose.  Details may
be found elsewhere; see VERIFY-GUARDS.  Briefly, for any defined
function fn, the event (verify-guards fn) attempts to check the
condition discussed above, that whenever fn is called on arguments that
satisfy its guard, the evaluation of this call will proceed without any
guard violation.  (Moreover, the guard itself should be evaluable
without any guard violation.)  If this check is successful, then future
calls of this sort will be evaluated in raw Common Lisp.

Returning to our example above, the (verify-guards foo) will succeed
because the guard (consp x) of foo implies the guard generated from the
call (cdr x) in the body of the definition, namely, (or (consp x) (equal
x nil)) (see CDR).  Then the evaluation of (foo (cons 'a 3))
will take place in raw Common Lisp, because (cons 'a 3) satisfies the
guard of foo.

This ability to dive into raw Common Lisp hinges on the proof that the
guards you attach to your own functions are sufficient to ensure that
the guards encountered in the body are satisfied.  This is called "guard
verification." Once a function has had its guards verified, then ACL2
can evaluate the function somewhat faster (but see "Guards and
evaluation V: efficiency issues" below).  Perhaps more importantly, ACL2
can also guarantee that the function will be evaluated correctly by any
implementation of Common Lisp (provided the guard of the function is
satisfied on the input).  That is, if you have verified the guards of a
system of functions and you have determined that they work as you wish
in your host ACL2 (perhaps by proving it, perhaps by testing), then they
will work identically in any Common Lisp.

There is a subtlety to our treatment of evaluation of calls of functions
whose guards have been verified.  If the function's guard is not
satisfied by such a call, then no further attempt is made to evaluate
any call of that function in raw lisp during the course of evaluation of
that call.  This is obvious if guard checking is on, because an error is
signalled the first time its guard is violated; but in fact it is also
true when guard checking is off.  See GUARD-EXAMPLE for an
example.

*Guards and evaluation IV: functions having :program mode*

Strictly speaking, functions in :program mode (see DEFUN-MODE)
do not have definitions in the ACL2 logic.  So what does it mean to
evaluate calls of such functions in ACL2?  In general we treat :program
functions much as we treat :logic functions whose guards have been
verified, except that when no error occurs then the corresponding raw
Lisp function is always called.  (We say "in general" because there are
exceptions, discussed in the "Aside" just below.)  Note that when the
guard of a function in :logic mode is violated, there is still a value
that the ACL2 logic proves is equal to the given call.  But the same
cannot be said for a function in :program mode.  Nevertheless, for the
sake of convenience we go ahead and evaluate the corresponding raw Lisp
function except in the situation where the guard is violated and
guard-checking is on, aside from the following:

*Aside*.  There are exceptions to the use of raw Lisp, discussed just
above, to evaluate calls of :program mode functions.  The primary one is
that after :set-guard-checking :none, evaluation of user-defined
:program mode function calls is done in the ACL2 logic, not in raw Lisp.
The more obscure exception is that during macroexpansion and evaluation
of defconst forms, ACL2 enters a "safe mode" in which this escape to raw
Lisp is prevented.  The following example illustrates how the user can
experiment directly with safe mode, though it is preferred to use
:set-guard-checking :none if you are happy to skip all guard checking
and evaluate forms in the logic.

     ACL2 !>(defun foo (x)
              (declare (xargs :mode :program :guard t))
              (car x))

     Summary
     Form:  ( DEFUN FOO ...)
     Rules: NIL
     Warnings:  None
     Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
      FOO
     ACL2 !>(foo 3)
     Error: Attempt to take the car of 3 which is not listp.
       [condition type: SIMPLE-ERROR]

     Restart actions (select using :continue):
      0: Return to Top Level (an "abort" restart).
      1: Abort entirely from this process.
     [1] ACL2(2): :pop
     ACL2 !>(assign safe-mode t)
      T
     ACL2 !>(foo 3)

     ACL2 Error in TOP-LEVEL:  The guard for the function symbol CAR, which
     is (OR (CONSP X) (EQUAL X NIL)), is violated by the arguments in the
     call (CAR 3).  See :DOC wet for how you might be able to get an error
     backtrace.

     ACL2 !>(assign safe-mode nil)
      NIL
     ACL2 !>(foo 3)
     Error: Attempt to take the car of 3 which is not listp.
       [condition type: SIMPLE-ERROR]

     Restart actions (select using :continue):
      0: Return to Top Level (an "abort" restart).
      1: Abort entirely from this process.
     [1] ACL2(2):

The other exception occurs after set-guard-checking can be called with a
value of :all; see SET-GUARD-CHECKING.  *End of aside.*

Thus, as with :logic functions: when a guard has been satisfied on a
call of a function with :program mode, no subsidiary guard checking will
be done.

Notice that by treating functions in :program mode like functions whose
guards have been verified, we are using raw lisp to compute their values
when their guards are met.  We do not check guards any further once raw
lisp is invoked.  This can lead to hard lisp errors if the guards are
not appropriate, as illustrated below.

     ACL2 >:program
     ACL2 p>(defun foo (x)
             (declare (xargs :guard t))
             (cons 1 (cdr x)))

     Summary
     Form:  ( DEFUN FOO ...)
     Rules: NIL
     Warnings:  None
     Time:  0.02 seconds (prove: 0.00, print: 0.00, proof tree: 0.00, other: 0.02)
      FOO
     ACL2 p>(foo 3)

     Error: 3 is not of type LIST.
     Fast links are on: do (use-fast-links nil) for debugging
     Error signalled by CDR.
     Broken at COND.  Type :H for Help.
     ACL2>>

See DEFUN-MODE-CAVEAT.

However, here is a way to get ACL2 to do run-time guard checking for
user-defined :program mode functions.  With this method, ACL2 will
evaluate calls of user-defined :program mode functions in a manner that
follows their ACL2 definitions.  Simply execute the following in the
ACL2 loop to put ACL2 into a "safe mode."

     (f-put-global 'safe-mode t state)

Let us revisit the example above, using safe mode.  Notice that the
guard of cdr is now being checked, because the executable counterpart of
foo is being called even though the guard is t.

     ACL2 !>(f-put-global 'safe-mode t state)
     <state>
     ACL2 !>:program
     ACL2 p!>(defun foo (x)
               (declare (xargs :guard t))
               (cons 1 (cdr x)))

     Summary
     Form:  ( DEFUN FOO ...)
     Rules: NIL
     Warnings:  None
     Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
      FOO
     ACL2 p!>(foo 3)

     ACL2 Error in TOP-LEVEL:  The guard for the function symbol CDR, which
     is (OR (CONSP X) (EQUAL X NIL)), is violated by the arguments in the
     call (CDR 3).  You may be able to see a trace of calls leading up to
     this violation by executing (wet <form>), where <form> is the form
     you submitted to the ACL2 loop.  See :DOC wet for how to get an error
     backtrace.

     ACL2 p!>(wet (foo 3))

     ACL2 Error in WITH-ERROR-TRACE:  The guard for the function symbol
     CDR, which is (OR (CONSP X) (EQUAL X NIL)), is violated by the arguments
     in the call (CDR 3).  (Backtrace is below.)

     1> (ACL2_*1*_ACL2::FOO 3)

     ACL2 p!>

If we go back into "unsafe" mode, then we once again see a raw Lisp
error, as we now illustrate.

     ACL2 p!>(f-put-global 'safe-mode nil state)
     <state>
     ACL2 p!>(foo 3)

     Error: 3 is not of type LIST.
     Fast links are on: do (si::use-fast-links nil) for debugging
     Error signalled by CDR.
     Broken at COND.  Type :H for Help.
     ACL2>>

*Guards and evaluation V: efficiency issues*

We have seen that by verifying the guards for a :logic function, we
arrange that raw lisp is used for evaluation of calls of such functions
when the arguments satisfy its guard.

This has several apparent advantages over the checking of guards as we
go.  First, the savings is magnified as your system of functions gets
deeper: the guard is checked upon the top-level entry to your system and
then raw Common Lisp does all the computing.  Second, if the raw Common
Lisp is compiled, enormous speed-ups are possible.  Third, if your
Common Lisp or its compiler does such optimizations as tail-recursion
removal, raw Common Lisp may be able to compute your functions on input
much "bigger" than ACL2 can.

The first of these advantages is quite important if you have complicated
guards.  However, the other two advantages are probably not very
important, as we now explain.

When a function is defined in :logic mode, its defun is executed in raw
Common Lisp.  (We might call this the "primary" raw lisp definition of
the function.)  However, a corresponding "logic definition" is also
executed.  The "logic definition" is a defun in raw lisp that checks
guards at runtime and escapes to the primary raw lisp definition if the
guard holds of the arguments and the function has already had its guards
verified.  Otherwise the logic definition executes the body of the
function by calling the logic definitions of each subroutine.  Now it is
true that compilation generally speeds up execution enormously.
However, the :comp command (see COMP) compiles both of the raw
lisp definitions associated with a :logic function.  Also, we have
attempted to arrange that for every tail recursion removal done on the
actual defun, a corresponding tail recursion removal is done on the
"logic definition."

We believe that in most cases, the logic definition executes almost as
fast as the primary raw lisp definition, at least if the evaluation of
the guards is fast.  So, the main advantage of guard verification is
probably that it lets you know that the function may be executed safely
in raw lisp, returning the value predicted by the ACL2 logic, whenever
its arguments satisfy its guard.  We envision the development of systems
of applicative lisp functions that have been developed and reasoned
about using ACL2 but which are intended for evaluation in raw Common
Lisp (perhaps with only a small "core" of ACL2 loaded), so this
advantage of guard verification is important.

Nevertheless, guard verification might be important for optimal
efficiency when the functions make use of type declarations.  For
example, at this writing, the GCL implementation of Common Lisp can
often take great advantage of declare forms that assign small integer
types to formal parameters.

To continue the discussion of guards, see
GUARDS-FOR-SPECIFICATION to read about the use of guards as a
specification device.

GUARDS-FOR-SPECIFICATION    guards as a specification device

A use of guard verification that has nothing to do with efficiency is as
a way to gain confidence in specifications.  This use has the feel of
"types" in many traditional programming languages, though guards allow
much greater expressiveness than most systems of types (and
unfortunately, as a result they are not syntactically checkable).

For more discussion of guards in general, see GUARD.

Suppose you have written a collection of function definitions that are
intended to specify the behavior of some system.  Perhaps certain
functions are only intended to be called on certain sorts of inputs, so
you attach guards to those functions in order to "enforce" that
requirement.  And then, you verify the guards for all those functions.

Then what have you gained, other than somewhat increased efficiency of
execution (as explained above), which quite possibly isn't your main
concern?  You have gained the confidence that when evaluating any call
of a (specification) function whose arguments satisfy that function's
guard, all subsequent function calls during the course of evaluation
will have this same property, that the arguments satisfy the guard of
the calling function.  In logical terms, we can say that the equality of
the original call with the returned value is provable from weakened
versions of the definitions, where each definitional axiom is replaced
by an implication whose antecedent is the requirement that the arguments
satisfy the guard and whose consequent is the original axiom.  For
example,

     (defun foo (x)
       (declare (xargs :guard (consp x)))
       (cons 1 (cdr x)))

originally generates the axiom

     (equal (foo x)
            (cons 1 (cdr x)))

but in fact, when evaluation involves no guard violation then the
following weaker axiom suffices in the justification of the evaluation.

     (implies (consp x)
              (equal (foo x)
                     (cons 1 (cdr x))))

If you are following links to read this documentation as a hypertext
style document, then please see GUARD-MISCELLANY.  This
concludes our discussion of guards with miscellaneous remarks, and also
contains pointers to related topics.

GUARD-HINTS    xargs keyword :GUARD-HINTS

See XARGS.

HANDS-OFF    hints keyword :HANDS-OFF

See HINTS.

HIDE    hide a term from the rewriter

Hide is actually the identity function: (hide x) = x for all x.
However, terms of the form (hide x) are ignored by the ACL2 rewriter,
except when explicit :expand hints are given for such terms (see
HINTS) or when rewrite rules explicitly about hide are available.  An
:expand hint that removes all calls of hide is:

     :expand ((:free (x) (hide x)))

The above hint can be particularly useful when ACL2's equality
heuristics apply hide to an equality after substituting it into the rest
of the goal, if that goal (or a subgoal of it) fails to be proved.

Hide terms are also ignored by the induction heuristics.

Sometimes the ACL2 simplifier inserts hide terms into a proof attempt
out of the blue, as it were.  Why and what can you do about it?  Suppose
you have a constrained function, say constrained-fn, and you define
another function, say another-fn, in terms of it, as in:

     (defun another-fn (x y z)
       (if (big-hairy-test x y z)
           (constrained-fn x y z)
           t))

Suppose the term (another-fn 'a 'b 'c) arises in a proof.  Since the
arguments are all constants, ACL2 will try to reduce such a term to a
constant by executing the definition of another-fn.  However, after a
possibly extensive computation (because of big-hairy-test) the execution
fails because of the unevaluable call of constrained-fn.  To avoid
subsequent attempts to evaluate the term, ACL2 embeds it in a hide
expression, i.e., rewrites it to (hide (another-fn 'a 'b 'c)).

You might think this rarely occurs since all the arguments of another-fn
must be constants.  You would be right except for one special case: if
another-fn takes no arguments, i.e., is a constant function, then every
call of it fits this case.  Thus, if you define a function of no
arguments in terms of a constrained function, you will often see
(another-fn) rewrite to (hide (another-fn)).

We do not hide the term if the executable counterpart of the function is
disabled -- because we do not try to evaluate it in the first place.
Thus, to prevent the insertion of a hide term into the proof attempt,
you can globally disable the executable counterpart of the offending
defined function, e.g.,

     (in-theory (disable (:executable-counterpart another-fn))).

It is conceivable that you cannot afford to do this: perhaps some calls
of the offending function must be computed while others cannot be.  One
way to handle this situation is to leave the executable counterpart
enabled, so that hide terms are introduced on the calls that cannot be
computed, but prove explicit :rewrite rules for each of those hide
terms.  For example, suppose that in the proof of some theorem, thm, it
is necessary to leave the executable counterpart of another-fn enabled
but that the call (another-fn 1 2 3) arises in the proof and cannot be
computed.  Thus the proof attempt will introduce the term (hide
(another-fn 1 2 3)).  Suppose that you can show that (another-fn 1 2 3)
is (contrained-fn 1 2 3) and that such a step is necessary to the proof.
Unfortunately, proving the rewrite rule

     (defthm thm-helper
       (equal (another-fn 1 2 3) (constrained-fn 1 2 3)))

would not help the proof of thm because the target term is hidden inside
the hide.  However,

     (defthm thm-helper
       (equal (hide (another-fn 1 2 3)) (constrained-fn 1 2 3)))

would be applied in the proof of thm and is the rule you should prove.

Now to prove thm-helper you need to use the two "tricks" which have
already been discussed.  First, to eliminate the hide term in the proof
of thm-helper you should include the hint :expand (hide (another-fn 1 2
3)).  Second, to prevent the hide term from being reintroduced when the
system tries and fails to evaluate (another-fn 1 2 3) you should include
the hint :in-theory (disable (:executable-counterpart another-fn)).
Thus, thm-helper will actually be:

     (defthm thm-helper
       (equal (hide (another-fn 1 2 3)) (constrained-fn 1 2 3))
       :hints
       (("Goal" :expand (hide (another-fn 1 2 3))
                :in-theory (disable (:executable-counterpart another-fn)))))

See EVISCERATE-HIDE-TERMS for how to affect the printing of hide
terms.

HINTS    advice to the theorem proving process

     Examples:
     The following :hints value is nonsensical.  Nevertheless, it
     illustrates all of the available hint keywords:

     :hints (("Goal"
              :do-not-induct t
              :do-not '(generalize fertilize)
              :expand ((assoc x a)
                       :lambdas
                       (:free (y) (:with member (member y z))))
              :restrict ((<-trans ((x x) (y (foo x)))))
              :hands-off (length binary-append)
              :in-theory (set-difference-theories
                           (current-theory :here)
                           '(assoc))
              :induct (and (nth n a) (nth n b))
              :use ((:instance assoc-of-append
                               (x a) (y b) (z c))
                    (:functional-instance
                      (:instance p-f (x a) (y b))
                      (p consp)
                      (f assoc)))
              :bdd (:vars (c a0 b0 a1 b1) :prove nil :bdd-constructors (cons))
              :cases ((true-listp a) (consp a))
              :by (:instance rev-rev (x (cdr z)))
              :nonlinearp t))

A very common hint is the :use hint, which in general takes as its value
a list of "lemma instances" (see LEMMA-INSTANCE) but which
allows a single lemma name as a special case:

     :hints (("[1]Subgoal *1/1.2'" :use lemma23))

ACL2 also provides "computed hints" for the advanced user.  See
COMPUTED-HINTS

Background: Hints are allowed in all events that use the theorem prover.
During defun events there are two different uses of the theorem prover:
one to prove termination and another to verify the guards.  To pass a
hint to the theorem prover during termination proofs, use the :hints
keyword in the defun's xargs declaration.  To pass a hint to the theorem
prover during the guard verification of defun, use the :guard-hints
keyword in the defun's xargs declaration.  The verify-guards event and
the defthm event also use the theorem prover.  To pass hints to them,
use the :hints keyword argument to the event.

     General Form of Common :hints:
       ((goal-spec :key1 val1 ... :keyn valn)
        ...
        (goal-spec :key1 val1 ... :keyn valn))

where goal-spec is as described in the documentation for goal-spec and
the keys and their respective values are shown below with their
interpretations.  (We also provide "computed hints" but discuss them
separately; see COMPUTED-HINTS.)

:DO-NOT-INDUCT

Value is t, name or nil, indicating whether induction is permitted under
the specified goal.  If value is t, then the attempt to apply induction
to the indicated goal or any subgoal under the indicated goal will
immediately cause the theorem prover to report failure.  Thus, the
indicated goal must be proved entirely by simplification, destructor
elimination, and the other "waterfall" processes.  Induction to prove
the indicated goal (or any subgoal) is not permitted.  See however the
:induct hint below.  If value is a symbol other than t or nil, the
theorem prover will give a "bye" to any subgoal that would otherwise be
attacked with induction.  This will cause the theorem prover to fail
eventually but will collect the necessary subgoals.  If value is nil,
this hint means induction is permitted.  Since that is the default,
there is no reason to use the value nil.

:DO-NOT

Value is a term having at most the single free variable world, which
when evaluated (with world bound to the current ACL2 logical world)
produces a list of symbols that is a subset of the list

     (preprocess ;propositional logic, simple rules
      simplify   ;as above plus rewriting, linear arithmetic
      eliminate-destructors
      fertilize  ;use of equalities
      generalize
      eliminate-irrelevance).

The hint indicates that the "processes" named should not be used at or
below the goal in question.  Thus, to prevent generalization and
fertilization, say, include the hint

     :do-not '(generalize fertilize)

If value is a single symbol, as in

     :do-not generalize,

it is taken to be '(value).

:EXPAND

Value is a true list of terms, each of which is of one of the forms (let
((v1 t1)...) b) or (fn t1 ... tn), where fn is a defined function symbol
with formals v1, ..., vn, and body b.  Such a term is said to be
"expandable:" it can be replaced by the result of substituting the ti's
for the vi's in b.  The terms listed in the :expand hint are expanded
when they are encountered by the simplifier while working on the
specified goal or any of its subgoals.  We permit value to be a single
such term instead of a singleton list.  *Notes*: (1) Allowed are "terms"
of the form (:free (var1 var2 ...  varn) pattern) where the indicated
variables are distinct and pattern is a term.  Such "terms" indicate
that we consider the indicated variables to be instantiatable, in the
following sense: whenever the simplifier encounters a term that can be
obtained from pattern by instantiating the variables (var1 var2 ...
varn), then it expands that term.  (2) Also allowed are "terms" of the
form (:with name term), where name is a function symbol, a macro name
that denotes a function symbol (see MACRO-ALIASES-TABLE), or a
rune.  The corresponding rule of class :rewrite, which is often a
definition rule but need not be, is then used in place of the current
body for the function symbol of term; see SHOW-BODIES and see
SET-BODY.  If the rule is of the form (implies hyp (equiv lhs
rhs)), then after matching lhs to the current term in a context that is
maintaining equivalence relation equiv, ACL2 will replace the current
term with (if hyp rhs (hide term)), or just rhs if the rule is just
(equal lhs rhs).  (3) A combination of both :free and :with, as
described above, is legal.  (4) The term :LAMBDAS is treated specially.
It denotes the list of all lambda applications (i.e., let expressions)
encountered during the proof.  Conceptually, this use of :LAMBDAS tells
ACL2 to treat lambda applications as a notation for substitutions,
rather than as function calls whose opening is subject to the ACL2
rewriter's heuristics (specifically, not allowing lambda applications to
open when they introduce "too many" if terms).

:HANDS-OFF

Value is a true list of function symbols or lambda expressions,
indicating that under the specified goal applications of these functions
are not to be rewritten.  Value may also be a single function symbol or
lambda expression instead of a list.

:IN-THEORY

Value is a "theory expression," i.e., a term having at most the single
free variable world which when evaluated (with world bound to the
current ACL2 logical world (see WORLD)) will produce a theory to
use as the current theory for the goal specified.  See THEORIES.

Note that an :IN-THEORY hint will always be evaluated relative to the
current ACL2 logical world, not relative to the theory of a previous
goal.  Consider the following example.

     (defthm prop
       (p (f (g x)))
       :hints (("Goal"      :in-theory (disable f))
               ("Subgoal 3" :in-theory (enable  g))))

Consider in particular the theory in effect at Subgoal 3.  This call of
the enable macro enables g relative to the current-theory of the current
logical world, *not* relative to the theory produced by the hint at
Goal.  Thus, the disable of f on behalf of the hint at Goal will be lost
at Subgoal 3, and f will be enabled at Subgoal 3 if was enabled globally
when prop was submitted.

:INDUCT

Value is either t or a term containing at least one recursively defined
function symbol; if t, this hint indicates that the system should
proceed to apply its induction heuristic to the specified goal produced
(without trying simplification, etc.); if value is a term other than t,
then not only should the system apply induction immediately, but it
should analyze value rather than the goal to generate its induction
scheme.  Merging and the other induction heuristics are applied.  Thus,
if value contains several mergeable inductions, the "best" will be
created and chosen.  E.g., the :induct hint

      (and (nth i a) (nth j a))

suggests simultaneous induction on i, j, and a.

If both an :induct and a :do-not-induct hint are supplied for a given
goal then the indicated induction is applied to the goal and the
:do-not-induct hint is inherited by all subgoals generated.

:USE

Value is a lemma-instance or a true list of lemma-instances, indicating
that the propositions denoted by the instances be added as hypotheses to
the specified goal.  See LEMMA-INSTANCE.  Note that :use makes
the given instances available as ordinary hypotheses of the formula to
be proved.  The :instance form of a lemma-instance permits you to
instantiate the free variables of previously proved theorems any way you
wish; but it is up to you to provide the appropriate instantiations
because once the instances are added as hypotheses their variables are
no longer instantiable.  These new hypotheses participate fully in all
subsequent rewriting, etc.  If the goal in question is in fact an
instance of a previously proved theorem, you may wish to use :by below.
Note that theories may be helpful when employing :use hints; see
MINIMAL-THEORY.

:BDD

This hint indicates that ordered binary decision diagrams (BDDs) with
rewriting are to be used to prove or simplify the goal.  See BDD
for an introduction to the ACL2 BDD algorithm.

Value is a list of even length, such that every other element, starting
with the first, is one of the keywords :vars, :bdd-constructors, :prove,
or :literal.  Each keyword that is supplied should be followed by a
value of the appropriate form, as shown below; for others, a default is
used.  Although :vars must always be supplied, we expect that most users
will be content with the defaults used for the other values.

:vars -- A list of ACL2 variables, which are to be treated as Boolean
variables.  The prover must be able to check, using trivial reasoning
(see TYPE-SET), that each of these variables is Boolean in the
context of the current goal.  Note that the prover will use very simple
heuristics to order any variables that do not occur in :vars (so that
they are "greater than" the variables that do occur in :vars), and these
heuristics are often far from optimal.  In addition, any variables not
listed may fail to be assumed Boolean by the prover, which is likely to
seriously impede the effectiveness of ACL2's BDD algorithm.  Thus, users
are encouraged *not* to rely on the default order, but to supply a list
of variables instead.  Finally, it is allowed to use a value of t for
vars.  This means the same as a nil value, except that the BDD algorithm
is directed to fail unless it can guarantee that all variables in the
input term are known to be Boolean (in a sense discussed elsewhere; see
BDD-ALGORITHM).

:literal -- An indication of which part of the current goal should
receive BDD processing.  Possible values are:

       :all     treat entire goal as a single literal (the default)
       :conc    process the conclusion
       n        process the hypothesis with index n (1, 2, ...)

:bdd-constructors -- When supplied, this value should be a list of
function symbols in the current ACL2 world; it is (cons) by default,
unless :bdd-constructors has a value in the acl2-defaults-table by
default, in which case that value is the default.  We expect that most
users will be content with the default.  See BDD-ALGORITHM for
information about how this value is used.

:prove -- When supplied, this value should be t or nil; it is t by
default.  When the goal is not proved and this value is t, the entire
proof will abort.  Use the value nil if you are happy to the proof to go
on with the simplified term.

:CASES

Value is a non-empty list of terms.  For each term in the list, a new
goal is created from the current goal by assuming that term; and also,
in essence, one additional new goal is created by assuming all the terms
in the list false.  We say "in essence" because if the disjunction of
the terms supplied is a tautology, then that final goal will be a
tautology and hence will in fact never actually be created.

:BY

Value is a lemma-instance, nil, or a new event name. If the value is a
lemma-instance (see LEMMA-INSTANCE), then it indicates that the
goal (when viewed as a clause) is either equal to the proposition
denoted by the instance, or is subsumed by that proposition when both
are viewed as clauses.  To view a formula as a clause, union together
the negations of the hypotheses and add the conclusion.  For example,

     (IMPLIES (AND (h1 t1) (h2 t2)) (c t1))

may be viewed as the clause

     {~(h1 t1) ~(h2 t2) (c t1)}.

Clause c1 is "subsumed" by clause c2 iff some instance of c2 is a subset
of c1.  For example, the clause above is subsumed by {~(h1 x) (c x)},
which when viewed as a formula is (implies (h1 x) (c x)).

If the value is nil or a new name, the prover does not even attempt to
prove the goal to which this hint is attached.  Instead the goal is
given a "bye", i.e., it is skipped and the proof attempt continues as
though the goal had been proved.  If the prover terminates without error
then it reports that the proof would have succeeded had the indicated
goals been proved and it prints an appropriate defthm form to define
each of the :by names.  The "name" nil means "make up a name."

The system does not attempt to check the uniqueness of the :by names
(supplied or made up), since by the time those goals are proved the
namespace will be cluttered still further.  Therefore, the final list of
"appropriate" defthm forms may be impossible to admit without some
renaming by the user.  If you must invent new names, remember to
substitute the new ones for the old ones in the :by hints themselves.

:RESTRICT

Warning: This is a sophisticated hint, suggested by Bishop Brock, that
is intended for advanced users.  In particular, :restrict hints are
ignored by the preprocessor, so you might find it useful to give the
hint :do-not '(preprocess) when using any :restrict hints, at least if
the rules in question are abbreviations (see SIMPLE).

Value is an association list.  Its members are of the form
(x subst1 subst2 ...), where: x is either (1) a rune whose
car is :rewrite or :definition or (2) an event name
corresponding to one or more such runes; and (subst1 subst2 ...) is
a non-empty list of substitutions, i.e., of association lists pairing
variables with terms.  First consider the case that x is a
:rewrite or :definition rune.  Recall that without
this hint, the rule named x is used by matching its left-hand side (call
it lhs) against the term currently being considered by the rewriter, that
is, by attempting to find a substitution s such that the instantiation of
lhs using s is equal to that term.  If however the :restrict hint
contains (x subst1 subst2 ...), then this behavior will be modified by
restricting s so that it must extend subst1; and if there is no such
s, then s is restricted so that it must extend subst2; and so on,
until the list of substitutions is exhausted.  If no such s is found,
then the rewrite or definition rule named x is not applied to that term.
Finally, if x is an event name corresponding to one or more
:rewrite or :definition runes (that is, x is the
"base symbol" of such runes; see RUNE), say runes r1,
... rn, then the meaning is the same except that
(x subst1 subst2 ...) is replaced by (ri subst1 subst2 ...) for each i.
Once this replacement is complete, the hint may not contain two members
whose car is the same rune.

Note that the substitutions in :restrict hints refer to the variables
actually appearing in the goals, not to the variables appearing in the
rule being restricted.

Here is an example, supplied by Bishop Brock.  Suppose that the database
includes the following rewrite rule, which is probably kept disabled.
(We ignore the question of how to prove this rule.)

     cancel-<-*$free:
     (implies (and (rationalp x)
                   (rationalp y)
                   (rationalp z))
              (equal (< y z)
                     (if (< x 0)
                         (> (* x y) (* x z))
                       (if (> x 0)
                           (< (* x y) (* x z))
                         (hide (< y z))))))

Then ACL2 can prove the following theorem (unless other rules get in the
way), essentially by multiplying both sides by x.

     (thm
       (implies (and (rationalp x)
                     (< 1 x))
                (< (/ x) 1))
       :hints
       (("Goal"
         :in-theory (enable cancel-<-*$free)
         :restrict ((cancel-<-*$free ((x x) (y (/ x)) (z 1)))))))

The :restrict hint above says that the variables x, y, and z in the
rewrite rule cancel-<-*$free above should be instantiated respectively
by x, (/ x), and 1.  Thus (< y z) becomes (< (/ x) 1), and this
inequality is replaced by the corresponding instance of the
right-hand-side of cancel-<-*$free.  Since the current conjecture
assumes (< 1 x), that instance of the right-hand side simplifies to

     (< (* x (/ x)) (* x 1))

which in turn simplifies to (< 1 x), a hypothesis in the present
theorem.

:NONLINEARP

Value is t or nil, indicating whether non-linear-arithmetic is active.
The default value is nil.  See NON-LINEAR-ARITHMETIC.