This is documentation for ACL2 Version 3.3
Copyright (C) 2007  University of Texas at Austin

This program is free software; you can redistribute it and/or modify
it under the terms of the GNU General Public License as published by
the Free Software Foundation; either version 2 of the License, or
(at your option) any later version.

This program is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
GNU General Public License for more details.

You should have received a copy of the GNU General Public License
along with this program; if not, write to the Free Software
Foundation, Inc., 675 Mass Ave, Cambridge, MA 02139, USA.

Written by:  Matt Kaufmann and J Strother Moore
Department of Computer Sciences
University of Texas at Austin
Austin, TX 78712-1188 U.S.A.

MORE!    another response to ``(type :more for more, :more! for the rest)''

NOTE:  The command :more! only makes sense at the terminal.

     Example:
     ACL2 !>:more!

will print all of the remaining documentation started by the last :doc
or :more-doc.

See MORE for some background.  Typing :more! will print all
remaining blocks of documentation.

:More! is like :more except that it prints all the text at once.  For
example, if you type :doc name you will see some text followed by
"(type :more for more, :more! for the rest)".  If you then type simply
:more! you will see all of the details, while if you type :more you
will be fed the next block of details.

MORE-DOC    a continuation of the :doc documentation

NOTE:  The :more-doc command only makes sense at the terminal.

     Examples:
     ACL2 !>:more-doc DEFTHM
     ACL2 !>:more-doc logical-name

Often it is assumed in the text provided by :more-doc name that you
have read the text provided by :doc name.

:More-doc just continues spewing out at you the documentation string
provided with a definition.  If the user has done his job, :doc will
probably remind you of the basics and :more-doc, if read after :doc,
will address obscure details that are nevertheless worth noting.

When :more-doc types "(type :more for more, :more! for the rest)" you
can get the next block of the continuation by typing :more or all of
the remaining blocks by typing :more!.  See MORE.

NQTHM-TO-ACL2    ACL2 analogues of Nqthm functions and commands

     Example Forms:
     :nqthm-to-acl2 prove-lemma   ; Display ACL2 topic(s) and/or print
                                  ; information corresponding to Nqthm
                                  ; PROVE-LEMMA command.
     (nqthm-to-acl2 'prove-lemma) ; Same as above.

     General Form:
     (nqthm-to-acl2 name)

where name is a notion documented for Nqthm:  either a function in the
Nqthm logic, or a command.  If there is corresponding information
available for ACL2, it will be printed in response to this command.
This information is not intended to be completely precise, but rather,
is intended to help those familiar with Nqthm to make the transition to
ACL2.

We close with two tables that contain all the information used by this
nqthm-to-acl2 command.  The first shows the correspondence between
functions in the Nqthm logic and corresponding ACL2 functions (when
possible); the second is similar, but for commands rather than
functions.

     Nqthm functions  -->     ACL2
     ----------------------------------------
     ADD1          -->  1+
     ADD-TO-SET    -->  ADD-TO-SET-EQUAL and ADD-TO-SET-EQ
     AND           -->  AND
     APPEND        -->  APPEND and BINARY-APPEND
     APPLY-SUBR    -->  No correspondent, but see the documentation for
                        DEFEVALUATOR and META.
     APPLY$        -->  No correspondent, but see the documentation for
                        DEFEVALUATOR and META.
     ASSOC         -->  ASSOC-EQUAL, ASSOC and ASSOC-EQ
     BODY          -->  No correspondent, but see the documentation for
                        DEFEVALUATOR and META.
     CAR           -->  CAR
     CDR           -->  CDR
     CONS          -->  CONS
     COUNT         -->  ACL2-COUNT
     DIFFERENCE    -->  -
     EQUAL         -->  EQUAL, EQ, EQL and =
     EVAL$         -->  No correspondent, but see the documentation for
                        DEFEVALUATOR and META.
     FALSE         -->  Nqthm's F corresponds to the ACL2 symbol NIL.
     FALSEP        -->  NOT and NULL
     FORMALS       -->  No correspondent, but see the documentation for
                        DEFEVALUATOR and META.
     GEQ           -->  >=
     GREATERP      -->  >
     IDENTITY      -->  IDENTITY
     IF            -->  IF
     IFF           -->  IFF
     IMPLIES       -->  IMPLIES
     LEQ           -->  <=
     LESSP         -->  <
     LISTP         -->  CONSP
     LITATOM       -->  SYMBOLP
     MAX           -->  MAX
     MEMBER        -->  MEMBER-EQUAL, MEMBER and MEMBER-EQ
     MINUS         -->  - and UNARY--
     NEGATIVEP     -->  MINUSP
     NEGATIVE-GUTS -->  ABS
     NLISTP        -->  ATOM
     NOT           -->  NOT
     NUMBERP       -->  ACL2-NUMBERP, INTEGERP and RATIONALP
     OR            -->  OR
     ORDINALP      -->  O-P
     ORD-LESSP     -->  O<
     PACK          -->  See intern and coerce.
     PAIRLIST      -->  PAIRLIS$
     PLUS          -->  + and BINARY-+
     QUOTIENT      -->  /
     REMAINDER     -->  REM and MOD
     STRIP-CARS    -->  STRIP-CARS
     SUB1          -->  1-
     TIMES         -->  * and BINARY-*
     TRUE          -->  The symbol T.
     UNION         -->  UNION-EQUAL and UNION-EQ
     UNPACK        -->  See symbol-name and coerce.
     V&C$          -->  No correspondent, but see the documentation for
                        DEFEVALUATOR and META.
     V&C-APPLY$    -->  No correspondent, but see the documentation for
                        DEFEVALUATOR and META.
     ZERO          -->  The number 0.
     ZEROP         -->  ZP

     ========================================

     Nqthm commands   -->     ACL2
     ----------------------------------------
     ACCUMULATED-PERSISTENCE
                   -->  ACCUMULATED-PERSISTENCE
     ADD-AXIOM     -->  DEFAXIOM
     ADD-SHELL     -->  There is no shell principle in ACL2.
     AXIOM         -->  DEFAXIOM
     BACKQUOTE-SETTING
                   -->  Backquote is supported in ACL2, but not
                        currently documented.
     BOOT-STRAP    -->  GROUND-ZERO
     BREAK-LEMMA   -->  MONITOR
     BREAK-REWRITE -->  BREAK-REWRITE
     CH            -->  PBT
                        See also :DOC history.
     CHRONOLOGY    -->  PBT
                        See also :DOC history.
     COMMENT       -->  DEFLABEL
     COMPILE-UNCOMPILED-DEFNS
                   -->  COMP
     CONSTRAIN     -->  See :DOC encapsulate and :DOC local.
     DATA-BASE     -->  Perhaps the closest ACL2 analogue of DATA-BASE
                        is PROPS.  But see :DOC history for a collection
                        of commands for querying the ACL2 database
                        (``world'').  Note that the notions of
                        supporters and dependents are not supported in
                        ACL2.
     DCL           -->  DEFSTUB
     DEFN          -->  DEFUN and DEFMACRO
     DEFTHEORY     -->  DEFTHEORY
     DISABLE       -->  DISABLE
     DISABLE-THEORY
                   -->  See :DOC theories.  The Nqthm command
                        (DISABLE-THEORY FOO) corresponds roughly to the
                        ACL2 command
                        (in-theory (set-difference-theories
                                     (current-theory :here)
                                     (theory 'foo))).
     DO-EVENTS     -->  LD
     DO-FILE       -->  LD
     ELIM          -->  ELIM
     ENABLE        -->  ENABLE
     ENABLE-THEORY -->  See :DOC theories.  The Nqthm command
                        (ENABLE-THEORY FOO) corresponds roughly to the
                        ACL2 command
                        (in-theory (union-theories
                                     (theory 'foo)
                                     (current-theory :here))).
     EVENTS-SINCE  -->  PBT
     FUNCTIONALLY-INSTANTIATE
                   -->  ACL2 provides a form of the :USE hint that
                        corresponds roughly to the
                        FUNCTIONALLY-INSTANTIATE event of Nqthm. See
                        :DOC lemma-instance.
     GENERALIZE    -->  GENERALIZE
     HINTS         -->  HINTS
     LEMMA         -->  DEFTHM
     MAINTAIN-REWRITE-PATH
                   -->  BRR
     MAKE-LIB      -->  There is no direct analogue of Nqthm's notion of
                        ``library.''  See :DOC books for a description
                        of ACL2's mechanism for creating and saving
                        collections of events.
     META          -->  META
     NAMES         -->  NAME
     NOTE-LIB      -->  INCLUDE-BOOK
     PPE           -->  PE
     PROVE         -->  THM
     PROVEALL      -->  See :DOC ld and :DOC certify-book.  The latter
                        corresponds to Nqthm's PROVE-FILE,which may be
                        what you're interested in,really.
     PROVE-FILE    -->  CERTIFY-BOOK
     PROVE-FILE-OUT
                   -->  CERTIFY-BOOK
     PROVE-LEMMA   -->  DEFTHM
                        See also :DOC hints.
     R-LOOP        -->  The top-level ACL2 loop is an evaluation loop as
                        well, so no analogue of R-LOOP is necessary.
     REWRITE       -->  REWRITE
     RULE-CLASSES  -->  RULE-CLASSES
     SET-STATUS    -->  IN-THEORY
     SKIM-FILE     -->  LD-SKIP-PROOFSP
     TOGGLE        -->  IN-THEORY
     TOGGLE-DEFINED-FUNCTIONS
                   -->  EXECUTABLE-COUNTERPART-THEORY
     TRANSLATE     -->  TRANS and TRANS1
     UBT           -->  UBT and U
     UNBREAK-LEMMA -->  UNMONITOR
     UNDO-BACK-THROUGH
                   -->  UBT
     UNDO-NAME     -->  See :DOC ubt.  There is no way to undo names in
                        ACL2 without undoing back through such names.
                        However, see :DOC ld-skip-proofsp for
                        information about how to quickly recover the
                        state.

EVENTS    functions that extend the logic

Any extension of the syntax of ACL2 (i.e., the definition of a new
constant or macro), the axioms (i.e., the definition of a function), or
the rule data base (i.e., the proof of a theorem), constitutes a
logical "event."  Events change the ACL2 logical world (see
WORLD).  Indeed, the only way to change the ACL2 world is via the
successful evaluation of an event function.  Every time the world is
changed by an event, a landmark is left on the world and it is thus
possible to identify the world "as of" the evaluation of a given event.
An event may introduce new logical names.  Some events introduce no
new names (e.g., verify-guards), some introduce exactly one (e.g.,
defmacro and defthm), and some may introduce many (e.g., encapsulate ).

ACL2 typically completes processing of an event by printing a summary
that includes a breakdown of time used and, unless proofs are skipped
(see LD-SKIP-PROOFSP) or summary output is inhibited (see
SET-INHIBIT-OUTPUT-LST), information about the proof attempt (if any)
including a list of rules used and a summary of warnings.  A detail:
The time is calculated using Common Lisp function get-internal-run-time,
which may ignore calls to external tools (see SYS-CALL and see
CLAUSE-PROCESSOR).

ADD-CUSTOM-KEYWORD-HINT    add a new custom keyword hint

     Examples:
     (add-custom-keyword-hint :my-hint (my-hint-fn val ...))

     (add-custom-keyword-hint :my-hint
                              (my-hint-fn val ...)
                              :checker (my-hint-checker-fn val ...))

     General Form:
     (add-custom-keyword-hint :key term1 :checker term2)

where :key is a keywordp not among the primitive keyword hints listed
in *hint-keywords*, the :checker argument is optional, and term1 and
(if supplied) term2 are terms with certain free-variable and signature
restrictions described below.  Henceforth, :key is treated as a custom
keyword hint, e.g., the user can employ :key in hints to defthm, such
as:

     (defthm name ...
       :hints (("Subgoal *1/1'" ... :key val ...))).

Custom keyword hints are complicated.  To use them you must understand
state, multiple values (e.g., mv and mv-let), ACL2's notion of error
triples (as briefly explained in ld-error-triples and er-progn), how to
generate "soft" errors with er, how to use fmt-strings to control
output, how to use computed hints (see COMPUTED-HINTS) and some
aspects of ACL2's internal event processing.  Furthermore, it is
possible to implement a custom keyword hint that can make an event
non-reproducible!  So we recommend that these hints be developed by
ACL2 experts.  Basically the custom keyword feature allows the
implementors and other experts to extend the hint facility without
modifying the ACL2 sources.

Term1 is called the "generator" term and term2 is called the "checker"
term of the custom keyword hint :key.  Together they specify the
semantics of the new custom keyword hint :key.  Roughly speaking, when
a custom keyword hint is supplied by the user, as in

     (defthm name ...
       :hints (("Subgoal *1/1'" ... :my-hint val ...))).

the checker term is evaluated on val to check that val is of the
expected shape.  Provided val passes the check, the generator term is
used to compute a standard hint.  Like computed hints, the generator of
a custom keyword hint is allowed to inspect the actual clause on which
it is being fired.  Indeed, it is allowed to inspect the entire list of
hints (standard and custom) supplied for that clause.  Thus, in the
most general case, a custom keyword hint is just a very special kind of
computed hint.

The generator, term1, must have no free variables other than:

     (val keyword-alist
      id clause world stable-under-simplificationp
      hist pspv ctx state).

Moreover, either term1 must evaluate to a single non-stobj value, or
else it must be single-threaded in state and have the standard
error-triple output signature, (mv * * state).

The restrictions on the checker, term2, are that it be single-threaded
in state, have the standard error-triple output signature, (mv * *
state), and have no free variables other than:

     (val world ctx state).

For an explanation of how custom keyword hints are processed, see
CUSTOM-KEYWORD-HINTS.

To delete a previously added custom keyword hint, see
REMOVE-CUSTOM-KEYWORD-HINT.

Note: This is an event!  It does not print the usual event summary but
nevertheless changes the ACL2 logical world and is so recorded.

ASSERT-EVENT    assert that a given form returns a non-nil value

     Examples:
     (assert-event (equal (+ 3 4) 7))
     (assert-event (equal (+ 3 4) 7) :msg (msg "Error: ~x0" 'equal-check))
     (assert-event (equal (+ 3 4) 7) :on-skip-proofs t)

     General Forms:
     (assert-event form)
     (assert-event form :on-skip-proofs t)

Assert-event takes a ground form, i.e., one with no free variables;
stobjs are allowed but only a single non-stobj value can be returned.
The form is then evaluated and if the result is nil, then a so-called
hard error (see ER) results.  This evaluation is however not
done if proofs are being skipped, as during include-book (also see
SKIP-PROOFS and see LD-SKIP-PROOFSP), unless
:on-skip-proofs t is supplied.

Normally, if an assert-event call fails then a generic failure message
is printed, showing the offending form.  However, if keyword argument
:msg is supplied, then the failure message is printed as with fmt
argument ~@0; see FMT.  In particular, :msg is typically a
string or a call (msg str arg-0 arg-1 ... arg-k), where str is a string
and each arg-i is the value to be associated with #i upon formatted
printing (as with fmt) of the string str.

This form may be put into a book to be certified (see BOOKS),
because assert-event is a macro whose calls expand to calls of
value-triple (see EMBEDDED-EVENT-FORM).  When certifying a
book, guard-checking is off, as though (set-guard-checking nil) has
been evaluated; see SET-GUARD-CHECKING.  That, together with a
"safe mode," guarantees that assert-event forms are evaluated in the
logic without guard violations while certifying a book.

COMP    compile some ACL2 functions

NOTE: Comp is a no-op if explicit compilation is suppressed; see
COMPILATION.  The documentation here assumes that this is not the
case.

     Examples:
     :comp t          ; compile all uncompiled ACL2 functions
     (comp t)         ; same as above, but can be put into a book
     (comp :exec)     ; compile all uncompiled logic (``*1*'') definitions
     :comp foo        ; compile the defined function foo
     :comp (:raw foo) ; compile the raw Lisp version of the defined function foo
                        but not the corresponding logic definition
     :comp (foo bar)  ; compile the defined functions foo and bar
     :comp (foo (:raw bar))  ; compile the defined functions foo and bar, but for
                             ; bar do not compile the corresponding logic definition

     General Form:
     :comp specifier
     where specifier is one of the following:

       t                     compile all user-defined ACL2 functions that are
                               currently uncompiled (redefined built-in functions
                               are not recompiled)
       :exec                 same as t, except that only logic versions are
                               compiled (see below), not raw Lisp definitions
       :raw                  same as t, except that only raw Lisp definitions are
                               compiled, not logic version (see below)
       (name-1 ... name-k)   a non-empty list of names of functions defined by
                               DEFUN in ACL2, except that each name-i can be of
                               the form (:raw sym) or (:exec sym), where sym is
                             the name of such a function
       name                  same as (name)

When you define a function in ACL2, you are really causing two
definitions to be made "under the hood" in Common Lisp: the definition
is submitted explicitly to raw Lisp, but so is a corresponding "logic
definition".  If guards have not been verified, then only the logic
definition will be evaluated; see GUARDS-AND-EVALUATION, in
particular the section titled "Guards and evaluation V: efficiency
issues".

Thus, if you are not verifying guards and you want the benefit of Lisp
compilation for speed and space efficiency, then you may want to place
the form (comp :exec) in your books.

Generally it is not necessary to place the form (comp t), or the form
(comp :raw), in a book, because certify-book compiles the raw Lisp
definitions anyhow, by default.  But you may wish to put (comp t) or
(comp fn1 fn2 ... fnk) in a book when such a form precedes expensive
calls of functions, for example for proofs involving calls of functions
on large constants, or to support computationally expensive
macroexpansion.

As suggested by the examples above, if a function specifier is of the
form (:raw fn), then fn will be compiled in raw Common Lisp but its
corresponding logic definition will not be compiled; and for (:exec fn),
it's the other way around.

The use of :comp creates various files whose names start with "TMP*",
but then deletes them.  If you want to keep these files around for some
reason, evaluate (assign keep-tmp-files t).

Also see SET-COMPILE-FNS for a way to compile each function as
it is defined.  But note that set-compile-fns is ignored during
include-book.

:cited-by Programming

COMP-GCL    compile some ACL2 functions leaving .c and .h files

Comp-gcl is for use by experts who want to examine the results of GCL
compilation, and it may only be used with ACL2 implementations built on
top of GCL.  It takes exactly the same arguments as comp, and has the
same basic functionality (see COMP), but has two additional
effects.  First, files "TMP.lisp" and "TMP1.lisp" are always created,
even when a single function is specified.  Second, comp-gcl always
leaves files "TMP.c", "TMP.h", "TMP1.c", and "TMP1.h" when compilation
is complete.

DEFABBREV    a convenient form of macro definition for simple expansions

     Examples:
     (defabbrev snoc (x y) (append y (list x)))
     (defabbrev sq (x) (declare (type (signed-byte 8) x)) (* x x))

     General Form:
     (defabbrev name (v1 ... vn) doc-string decl1 ... declk body)

where name is a new function symbol, the vi are distinct variable
symbols, and body is a term.  The decli, if supplied, should be legal
declare forms; see DECLARE.  Doc-string is an optional
documentation string; see DOC-STRING.

Roughly speaking, the defabbrev event is akin to defining f so that (f
v1 ... vn) = body.  But rather than do this by adding a new axiom,
defabbrev defines f to be a macro so that (f a1 ... an) expands to
body, with the "formals," vi, replaced by the "actuals," ai.

For example, if snoc is defined as shown in the first example above,
then (snoc (+ i j) temp) is just an abbreviation for

     (append temp (list (+ i j))).

In order to generate efficiently executable Lisp code, the macro that
defabbrev introduces uses a let to bind the "formals" to the "actuals."
Consider the second example above.  Logically speaking, (sq (ack i j))
is an abbreviation for (* (ack i j) (ack i j)).  But in fact the macro
for sq introduced by defabbrev actually arranges for (sq (ack i j)) to
expand to:

     (let ((x (ack i j)))
       (* x x))

which executes more efficiently than (* (ack i j) (ack i j)).

In the theorem prover, the let above expands to

     ((lambda (x) (* x x)) (ack i j))

and thence to (* (ack i j) (ack i j)).

It is important to note that the term in body should not contain a call
of name -- i.e., defabbrev should not be used in place of defun when
the function is recursive.  ACL2 will not complain when the defabbrev
form is processed, but instead ACL2 will more than likely go into an
infinite loop during macroexpansion of any form that has a call of name.

It is also important to note that the parameters of any call of a macro
defined by defabbrev will, as is the case for the parameters of a
function call, be evaluated before the body is evaluated, since this is
the evaluation order of let.  This may lead to some errors or
unexpected inefficiencies during evaluation if the body contains any
conditionally evaluted forms like cond, case, or if.  Consider the
following example.

     (defabbrev foo (x y)
       (if (test x) (bar y) nil))

Notice a typical one-step expansion of a call of foo (see
TRANS1):

     ACL2 !>:trans1 (foo expr1 expr2)
      (LET ((X EXPR1) (Y EXPR2))
           (IF (TEST X) (BAR Y) NIL))
     ACL2 !>

Now imagine that expr2 is a complicated expression whose evaluation is
intended only when the predicate test holds of expr1.  The expansion
above suggests that expr2 will always be evaluated by the call (foo
expr1 expr2), which may be inefficient (since perhaps we only need that
value when test is true of expr1).  The evaluation of expr2 may even
cause an error, for example in :program mode if the expression expr2 has
been constructed in a manner that could cause a guard violation unless
test holds of expr1.

DEFAXIOM    add an axiom

WARNING: We strongly recommend that you not add axioms.  If at all
possible you should use defun or mutual-recursion to define new
concepts recursively or use encapsulate to constrain them
constructively.  If your goal is to defer a proof by using a top-down
style, consider using skip-proofs; see the discussion on "Top-Down
Proof" in Section B.1.2 of "Computer-Aided Reasoning: An Approach."
Adding new axioms frequently renders the logic inconsistent.

     Example:
     (defaxiom sbar (equal t nil)
               :rule-classes nil
               :doc ":Doc-Section ...")

     General Form:
     (defaxiom name term
              :rule-classes rule-classes
              :doc          doc-string)

where name is a new symbolic name (see NAME), term is a term
intended to be a new axiom, and rule-classes and doc-string are as
described in the corresponding documentation topics .  The two keyword
arguments are optional.  If :rule-classes is not supplied, the list
(:rewrite) is used; if you wish the axiom to generate no rules, specify
:rule-classes nil.

DEFCHOOSE    define a Skolem (witnessing) function

     Examples:
     (defchoose choose-x-for-p-and-q (x) (y z)
       (and (p x y z)
            (q x y z)))

     (defchoose choose-x-for-p-and-q x (y z) ; equivalent to the above
       (and (p x y z)
            (q x y z)))

     ; The following is as above, but strengthens the axiom added to pick a sort
     ; of canonical witness, as described below.
     (defchoose choose-x-for-p-and-q x (y z)
       (and (p x y z)
            (q x y z))
       :strengthen t)

     (defchoose choose-x-and-y-for-p-and-q (x y) (z)
       (and (p x y z)
            (q x y z)))

     * Menu:

     * CONSERVATIVITY-OF-DEFCHOOSE:: proof of conservativity of defchoose

     General Form:
     (defchoose fn
                (bound-var1 ... bound-varn)
                (free-var1 ... free-vark)
                body
                :doc doc-string
                :strengthen b),

where fn is the symbol you wish to define and is a new symbolic name
(see NAME), (bound-var1 ... bound-varn) is a list of distinct
`bound' variables (see below), (free-var1 ... free-vark) is the list of
formal parameters of fn and is disjoint from the bound variables, and
body is a term.  The use of lambda-list keywords (such as &optional) is
not allowed.  The documentation string argument, :doc doc-string, is
optional; for a description of the form of doc-string see
DOC-STRING.  The :strengthen keyword argument is optional; if
supplied, it must be t or nil.

The system treats fn very much as though it were declared in the
signature of an encapsulate event, with a single axiom exported as
described below.  If you supply a :use hint (see HINTS), :use
fn, it will refer to that axiom.  No rule (of class :rewrite or
otherwise; see RULE-CLASSES) is created for fn.

Defchoose is only executed in defun-mode :logic; see
DEFUN-MODE.  Also see DEFUN-SK.

In the most common case, where there is only one bound variable, it is
permissible to omit the enclosing parentheses on that variable.  The
effect is the same whether or not those parentheses are omitted.  We
describe this case first, where there is only one bound variable, and
then address the other case.  Both cases are discussed assuming
:strengthen is nil, which is the default.  We deal with the case
:strengthen t at the end.

The effect of the form

     (defchoose fn bound-var (free-var1 ... free-vark)
       body)

is to introduce a new function symbol, fn, with formal parameters
(free-var1 ... free-vark).  Now consider the following axiom, which
states that fn picks a value of bound-var so that the body will be
true, if such a value exists:

     (1)   (implies body
                    (let ((bound-var (fn free-var1 ... free-vark)))
                      body))

This axiom is "clearly conservative" under the conditions expressed
above: the function fn simply picks out a "witnessing" value of
bound-var if there is one.  For a rigorous statement and proof of this
conservativity claim, see CONSERVATIVITY-OF-DEFCHOOSE.

Next consider the case that there is more than one bound variable, i.e.,
there is more than one bound-var in the following.

     (defchoose fn
                (bound-var1 ... bound-varn)
                (free-var1 ... free-vark)
                body)

Then fn returns a multiple value with n componenets, and formula (1)
above is expressed using mv-let as follows:

     (implies body
              (mv-let (bound-var1 ... bound-varn)
                      (fn free-var1 ... free-vark)
                      body))

We now discuss the case that :strengthen t is supplied.  For simplicity
we return to our first example, with a single free variable, y.  The
idea is that if we pick the "smallest" witnessing bound-var for two
different free variables y and y1, then either those two witnesses are
the same, or else one is less than the other, in which case the smaller
one is a witness for its free variable but not for the other.  (See
comments in source function defchoose-constraint-extra for more
details.)  Below, body1 is the result of replacing y by y1 in body.

     (2)   (or (equal (fn y) (fn y1))
               (let ((bound-var (fn y)))
                 (and body
                      (not body1)))
               (let ((bound-var (fn y1)))
                 (and body1
                      (not body))))

An important application of this additional axiom is to be able to
define a "fixing" function that picks a canonical representative of
each equivalence class, for a given equivalence relation.  The
following events illustrate this point.

     (encapsulate
      ((equiv (x y) t))
      (local (defun equiv (x y) (equal x y)))
      (defequiv equiv))

     (defchoose efix (x) (y)
       (equiv x y)
       :strengthen t)

     (defthm equiv-implies-equal-efix-1
       (implies (equiv y y1)
                (equal (efix y) (efix y1)))
       :hints (("Goal" :use efix))
       :rule-classes (:congruence))

     (defthm efix-fixes
       (equiv (efix x) x)
       :hints (("Goal" :use ((:instance efix (y x))))))

If there is more than one bound variable, then (2) is modified in
complete analogy to (1) to use mv-let in place of let.

Comment for logicians:  As we point out in the documentation for
defun-sk, defchoose is "appropriate," by which we mean that it is
conservative, even in the presence of epsilon-0 induction.  For a
proof, See CONSERVATIVITY-OF-DEFCHOOSE.