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.

ADD-BINOP    associate a binary function name with a macro name

     Example:
     (add-binop append binary-append)

This example associates the function symbol binary-append with the macro
name append.  As a result, theory functions will understand that append
refers to binary-append -- see ADD-MACRO-ALIAS --- and moreover,
proof output will be printed using append rather than binary-append,
e.g., (append x y z w) is printed rather than (binary-append x
(binary-append y (binary-append z w))).

     General Form:
     (add-binop macro-name function-name)

This is a convenient way to add an entry to macro-aliases-table and at
the same time extend the :binop-table.  See MACRO-ALIASES-TABLE,
see REMOVE-MACRO-ALIAS, see BINOP-TABLE, and see
REMOVE-BINOP.

ADD-DEFAULT-HINTS    add to the default hints

     Examples:
     (add-default-hints '((computed-hint-1 clause)
                          (computed-hint-2 clause
                                           stable-under-simplificationp)))

Note: This is an event!  It does not print the usual event summary but
nevertheless changes the ACL2 logical world and is so recorded.  It is
local to the book or encapsulate form in which it occurs (see
ADD-DEFAULT-HINTS! for a corresponding non-local event).

     General Form:
     (add-default-hints lst)

where lst is a list.  Generally speaking, the elements of lst should be
suitable for use as computed-hints.

This event is completely analogous to set-default-hints, the difference
being that add-default-hints appends the indicated hints to the list of
default hints, rather than *replacing* the default hints with the
indicated hints.

Finally, note that the effects of set-default-hints, add-default-hints,
and remove-default-hints are local to the book in which they appear.
Thus, users who include a book with such forms will not have their
default hints affected by such forms.  In order to export the effect of
setting the default hints, use set-default-hints!, add-default-hints!,
or remove-default-hints!.

ADD-DEFAULT-HINTS!    add to the default hints non-locally

Please see ADD-DEFAULT-HINTS, which is the same as
add-default-hints!  except that the latter is not local to the
encapsulate or the book in which it occurs.  Probably add-default-hints
is to be preferred unless you have a good reason for wanting to export
the effect of this event outside the enclosing encapsulate or book.

ADD-DIVE-INTO-MACRO    associate proof-checker diving function with macro name

     Examples:
     (add-dive-into-macro cat expand-address-cat)

This feature is used so that the proof-checker's DV command and numeric
diving commands (e.g., 3) will dive properly into subterms.  Please see
DIVE-INTO-MACROS-TABLE.

ADD-INCLUDE-BOOK-DIR    associate directory to keyword for include-book's :dir argument

     Example Form:
     (add-include-book-dir :smith "/u/smith/")
      ; For (include-book "foo" :dir :smith), prepend "/u/smith/" to "foo".

     General Form:
     (add-include-book-dir kwd dir)

where kwd is a keywordp and dir is the absolute pathname (see
PATHNAME) of a directory.  The effect of this event is to modify the
meaning of the :dir keyword argument of include-book as indicated by the
examples above, namely by associating the indicated directory with the
indicated keyword for purposes of the include-book :dir argument.  See
DELETE-INCLUDE-BOOK-DIR for how to undo this effect.

Caveat: The keyword :system cannot be redefined.  It will always point
to the absolute pathname of the distributed books directory, which by
default is immediately under the directory where the ACL2 executable was
originally built (see INCLUDE-BOOK, in particular the discussion
there of "books directory").

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

This macro generates a call (table acl2-defaults-table
:include-book-dir-alist ...)  and hence is local to any books and
encapsulate events in which is occurs. See ACL2-DEFAULTS-TABLE.

ADD-INVISIBLE-FNS    make some unary functions invisible to the loop-stopper algorithm

     Examples:
     (add-invisible-fns binary-+ unary-- foo)

The setting above has makes unary functions unary-- and foo "invisible"
for the purposes of applying permutative :rewrite rules to binary-+
trees.  Thus, arg and (unary-- arg) will be given the same weight and
will be permuted so as to be adjacent.

     General Form:
     (add-invisible-fns top-fn unary-fn1 ... unary-fnk)

where top-fn is a function symbol and the unary-fni are unary function
symbols.

For more information see INVISIBLE-FNS-TABLE.  Also see
SET-INVISIBLE-FNS-TABLE, which explains how to set the entire table in
a single event, and see REMOVE-INVISIBLE-FNS.

ADD-MACRO-ALIAS    associate a function name with a macro name

     Example:
     (add-macro-alias append binary-append)

This example associates the function symbol binary-append with the macro
name append.  As a result, the name append may be used as a runic
designator (see THEORIES) by the various theory functions.  See
MACRO-ALIASES-TABLE for more details.

     General Form:
     (add-macro-alias macro-name function-name)

This is a convenient way to add an entry to macro-aliases-table.  See
MACRO-ALIASES-TABLE and also see REMOVE-MACRO-ALIAS.

ADD-MATCH-FREE-OVERRIDE    set :match-free value to :once or :all in existing rules

     Example Forms:
     (add-match-free-override :once t)
         ; Try only the first binding of free variables when relieving hypotheses
         ; of any rule of class :rewrite, :linear, or :forward-chaining.
     (add-match-free-override :all (:rewrite foo) (:rewrite bar))
         ; For rewrite rules foo and bar, try all bindings of free variables when
         ; relieving hypotheses.
     (add-match-free-override :clear)
         ; Restore :match-free to what was originally stored for each rule (either
         ; :all or :once).

As described elsewhere (see FREE-VARIABLES), a rewrite, linear,
or forward-chaining rule may have free variables in its hypotheses, and
ACL2 can be directed either to try all bindings (":all") or just the
first (":once") when relieving a hypothesis, as a basis for relieving
subsequent hypotheses.  This direction is generally provided by
specifying either :match-free :once or :match-free :all in the
:rule-classes of the rule, or by using the most recent
set-match-free-default event.  Also see RULE-CLASSES.

However, if a proof is going slowly, you may want to modify the behavior
of some such rules so that they use only the first match for free
variables in a hypothesis when relieving subsequent hypotheses, rather
than backtracking and trying additional matches as necessary.  The event
(add-match-free-override :once t) has that effect.  Or at the other
extreme, perhaps you want to specify all rules as :all rules except for
a some specific exceptions.  Then you can execute
(add-match-free-override :all t) followed by, say,
(add-match-free-override :once (:rewrite foo) (:linear bar)).

     General Forms:
     (add-match-free-override :clear)
     (add-match-free-override flg t)
     (add-match-free-override flg rune1 rune2 ... runek)

where flg is :once or :all and the runei are runes.  If :clear is
specified then all rules will have the :all/:once behavior from when
they were first stored.  The second general form causes all rewrite
linear, and forward-chaining rules to have the behavior specified by flg
(:all or :once).  Finally, the last of these, where runes are specified,
is additive in the sense that only the indicated rules are affected; all
others keep the behavior they had just before this event was executed
(possible because of earlier add-match-free-override events).

At the conclusion of this event, ACL2 prints out the list of all
:linear, :rewrite, and :forward-chaining runes whose rules contain free
variables in hypotheses that are to be bound :once, except that if there
are no overrides (value :clear was used), then :clear is printed.

This event only affects rules that exist at the time it is executed.
Future rules are not affected by the override.

Note: This is an event!  It does not print the usual event summary but
nevertheless changes the ACL2 logical world and is so recorded.  It uses
the acl2-defaults-table, and hence its effect is local to the book or
encapsulate form in which it occurs.

*Remarks*

Lists of the :rewrite, :linear, and :forward-chaining runes whose
behavior was originally :once or :all are returned by the following
forms, respectively.

     (free-var-runes :once (w state))
     (free-var-runes :all  (w state))

The form

     (match-free-override (w state))

evaluates to a pair, whose car is a number used by ACL2 to determine
whether a rune is sufficiently old to be affected by the override, and
whose cdr is the list of runes whose behavior is specified as :once by
add-match-free-override; except, if no runes have been overridden, then
the keyword :clear is returned.

ADD-NTH-ALIAS    associate one symbol with another for printing of nth/update-nth terms

     Example:
     (add-nth-alias st0 st)

This example associates the symbol st0 with the symbol st for purposes
of printing certain terms of the form (nth n st0) and (update-nth n val
st0).

     General Form:
     (add-nth-alias alias-name name)

This is a convenient way to add an entry to nth-aliases-table.  See
NTH-ALIASES-TABLE and also see REMOVE-NTH-ALIAS.

BINOP-TABLE    associates binary function with the corresponding macro

     Examples:
     ACL2 !>(binop-table (w state))
     '((binary-+ . +)
       (binary-* . *)
       (binary-append . append)
       (binary-logand . logand)
       (binary-logior . logior)
       (binary-logxor . logxor)
       (binary-logeqv . logeqv))

See TABLE for a general discussion of tables.

See ADD-BINOP for a more general discussion of this table.

COMP    compile some ACL2 functions

     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 defined ACL2 functions that are currently
                               uncompiled
       :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 to 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.

DEFAULT-HINTS-TABLE    a table used to provide hints for proofs

Please see SET-DEFAULT-HINTS, see ADD-DEFAULT-HINTS, and
see REMOVE-DEFAULT-HINTS for how to use this table.  For
completeness, we mention here that under the hood, these events all
update the default-hints-table by updating its unique key, t, for
example as follows.

     (table default-hints-table t
            '((computed-hint-1 clause)
              (computed-hint-2 clause
                               stable-under-simplificationp)))

The use of default hints is explained elsewhere; see
SET-DEFAULT-HINTS.

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)))

     (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)
                doc-string ; optional
                body),

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, doc-string, is optional; for a
description of its form, see DOC-STRING.

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
address the other case 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), and the following axiom stating that fn picks
a value of bound-var so that the body will be true, if such a value
exists:

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

This axiom is "clearly" conservative under the conditions expressed
above: the function fn merely picks out a "witnessing" value of
bound-var if there is one.  The system in fact treats fn very much as
though it were declared in the signature of an encapsulate event, with
the axiom above as the only axiom exported.  If you supply a :use hint
(see HINTS), :use fn, it will refer to this axiom.  No rule (of
class :rewrite or otherwise; see RULE-CLASSES) is created for
fn.

If there is more than one bound variable, as in

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

then fn returns n a multiple value, and the defining axiom is expressed
using mv-let (see MV-LET) as follows:

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

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

Also see DEFUN-SK.

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.

CONSERVATIVITY-OF-DEFCHOOSE    proof of conservativity of defchoose

This documentation topic provides underlying theory.  It is of
theoretical interest only; it has no relationship to the effective use
of ACL2.

The argument below for the conservativity of defchoose replaces the
terse and somewhat misleading reference to a forcing argument in
Appendix B of the paper by ACL2 authors Kaufmann and Moore, "Structured
Theory Development for a Mechanized Logic" (Journal of Automated
Reasoning 26, no. 2 (2001), pp. 161-203).

Our basic idea is to to take a (countable) first-order structure for
ACL2, M, together with a function symbol, f, introduced by defchoose,
and find a way to expand M with an interpretation of f (without changing
the universe of M) so that e0-induction continues to hold in the
expansion.  A remark at the end of this documentation topic shows why
care is necessary.  A concept called "forcing", originally introduced by
Paul Cohen for set theory, has long since been adapted by logicians (in
a simplified form) to model theory.  This simplified model-theoretic
forcing provides the means for making our careful expansion.

The forcing argument presented below is intended to be completely
self-contained for those familiar with basic first-order logic and ACL2.
No background in forcing (model-theoretic or otherwise) is expected,
though we do expect a rudimentary background in first-order logic and
familiarity with the following.

Preliminaries.  We write s[p<-p0] to denote the result of extending or
modifying the assignment s by binding p to p0.  Now let A be a subset of
the universe U of a first-order structure M.  A is said to be
"first-order definable with parameters" in M if for some formula phi,
variable x, and assignment s binding the free variables of phi except
perhaps for x, A = {a \in U: M |= phi[s[x<-a]].  Note that we are
writing "\in" to denote set membership.  Finally, we indicate the end of
a proof (or of a theorem statement, when the proof is omitted) with the
symbol "-|".

We gratefully acknowledge very helpful feedback from John Cowles, who
found several errors in a draft of this note and suggested the
exercises.  We also thank Ruben Gamboa for helpful feedback, and we
thank Jim Schmerl for an observation that led us directly to this proof
in the first place.

We are given a consistent first-order theory T, extending the ACL2
ground-zero theory, that satisfies the e0-induction scheme.  We wish to
show that the extension of T by the following arbitrary defchoose event
is conservative, where g is a new function symbol.

          (defchoose g <bound-vars> <free-vars> <body>)

Note that by "the extension of T" here we mean the extension of T by not
only the new defchoose axiom displayed just below, but also the addition
of e0-induction axioms for formulas in the language with the new
defchoose function symbol, g.

          <body> -> (LET <free-vars> = g(<bound-vars>) in <body>)

By definition of conservativity, since proofs are finite, it clearly
suffices to consider an arbitrary finite subset of T.  Then by the
completeness, soundness, and downward Lowenheim-Skolem theorems of
first-order logic, it suffices to show that an arbitrary countable model
of T can be expanded (i.e., by interpreting the new symbol g without
changing the universe of the model) to a model of the corresponding
defchoose axiom above, in which all e0-induction axioms hold in the
language of that model.

Below, we will carry out a so-called *forcing* construction, which
allows us to expand any countable model M of T to a model M[G] that
satisfies e0-induction and also satisfies the above axiom generated from
the above defchoose event.  The ideas in this argument are standard in
model theory; no novelty is claimed here.

Fix a countable model M of a theory T that satisfies e0-induction and
extends the ACL2 ground-zero theory.  Also fix the above defchoose
axiom, where g is not in the language of T.

We start by defining a partial order P as follows.  Let Nb and Nf be the
lengths of <bound-vars> and <free-vars>, respectively.  P consists of
all fn in M such that the following formula is true in M.  Roughly
speaking, it says that fn is a finite function witnessing the above
requirement for g.

            alistp(fn) &
            no-duplicatesp-equal(strip-cars(fn)) &
            (forall <bound-vars>, <free-vars> .
               (member-equal(cons(<bound-vars>,<free-vars>), fn) ->
                (length(<bound-vars>) = Nb &
                 length(<free-vars>)  = Nf &
                 ((exists <free-vars> . <body>) -> <body>))))

P is ordered by subset, i.e., we say that p2 *extends* p1 if p1 is a
subset (not necessarily proper) of p2 (more precisely, M |=
subsetp-equal(p1,p2)).

Remark.  The original argument in Appendix B of the aforementioned paper
can essentially be salvaged, as we now show.  The key observation is
that the particular choice of P is nearly irrelevant for the argument
that follows below.  In particular, we can instead define P to consist
of finite one-one functions with domain contained in the set of natural
numbers.  More precisely, consider the following definitions.

          (defun function-p (fn)
            (declare (xargs :guard t))
            (and (alistp fn)
                 (no-duplicatesp-equal (strip-cars fn))))

          (defun nat-listp (x)
            (declare (xargs :guard t))
            (cond ((atom x)
                   (equal x nil))
                  (t (and (natp (car x))
                          (nat-listp (cdr x))))))

          (defun nat-function-p (x)
            (and (function-p x)
                 (nat-listp (strip-cars x))))

and define inverse as follows.

          (defun inverse (fn)
            (declare (xargs :guard (alistp fn)))
            (if (endp fn)
                nil
              (cons (cons (cdar fn) (caar fn))
                    (inverse (cdr fn)))))

Then P may instead be defined to consist of those fn for which
nat-function-p(fn) & function-p(inverse(fn)).  With this alternate
definition of P, the argument below then goes through virtually
unchanged, and we get an expansion M[G] of M in which there is a
definable enumeration of the universe.  The conservativity of defchoose
then follows easily because the function being introduced can be defined
explicitly using that enumeration (namely, always pick the least witness
in the sense of the enumeration).

End of Remark.

Next we present the relevant forcing concepts from model theory.

A *dense* subset of P is a subset D of P such that for every p \in P,
there is d \in D such that d extends p.  A subset G of P is *generic*
with respect to a collection Ds of dense subsets of P, also written "G
is Ds-generic," if G is closed under extension (if p1 \in G and p1
extends p2 then p2 \in G), G is pairwise compatible (the union-equal of
any two elements of G is in G), and every set in Ds has non-empty
intersection with G.

For p \in P, we say that a subset D of P is *dense beyond* p if for all
p1 extending p there exists p2 extending p1 such that p2 \in D.  This
notion makes sense even for D not a subset of P if we treat elements of
D not in P as nil.

Proposition 1.  For any partial order P and countable collection Ds of
dense subsets of P, there is a Ds-generic subset of P.

Proof.  Let Ds = {D0,D1,D2,...}.  Define a sequence <p_0,p_1,...> such
that for all i, p_i \in Di and p_(i+1) extends p_i.  Let G = {p \in P:
for some i, pi extends p}.  Then G is Ds-generic. -|

Note that P is first-order definable (with parameters) in M.  Let Df be
the set of dense subsets of P that are first-order definable (with
parameters) in M.  A standard argument shows there are only countably
many first-order definitions with parameters in a countable model M --
for example, we can Goedel number all terms and then all formulas --
hence, Df is countable.

By Proposition 1, let G be Df-generic.  Notice that for any list x of
length Nb in M, the set of elements f of P for which x is in the domain
of f is dense and first-order definable.  We may thus define a function
g0 as follows: g0(x_1,...,x_Nb) = y if there is some element of G
containing the pair ((x1_ ... x_Nb) . y).  It is easy to see that g0 is
a total function on M.  Let L be the language of T and let L[g] be the
union of L with a set containing a single new function symbol, g.  Let
M[G] be the expansion of M to L[g] obtained by interpreting g to be g0
(see also Proposition 5 below).

So now we have fixed M, P, Df, G, and g0, where G is Df-generic.

Proposition 2.  Let Df be the set of dense subsets of P that are
first-order definable (with parameters) in M.  Suppose that p \in G and
D \in Df.  Then for some q \in G extending p, q \in D.

Proof.  Let D0 be the set of p' \in D that either extend p or have no
extension in D that extends p.  We leave it as a straightforward
exercise to show that D0 is dense, and D0 is clearly first-order
definable (with parameters) in M.  So by genericity of G, we may pick q
\in D0 such that q \in G.  Thus q \in D.  By definition of generic, some
extension q1 of both p and q belongs to G.  Pick q2 \in D extending q1;
thus q has an extension in D that extends p (namely, q2), so by
definition of D0, q extends p. -|

Definition of forcing.  Let phi(x1,...,xk) be a first-order formula in
L[g] and let p \in P.  We define a formula of L, denoted "p ||- phi" ("p
forces phi"), by recursion on phi (in the metatheory) as follows.
(Here, we view "or" and "forall" as abbreviations.)

       If phi is atomic, then let phi'(A) be the result of replacing,
     inside-out, each subterm of the form g(x_1,...,x_Nb) with the term
     (cdr (assoc-equal (list x_1 ... x_Nb) A)), where A is neither p nor
     a variable occurring in phi.  Then p ||- phi is defined as follows:
     "The set {A \in P: A extends p and phi'(A)} is dense beyond p".
     That is, p ||- phi is the following formula:

              (forall p1 \in P extending p)
               (exists p2 \in P extending p1) phi'(p2).

       p ||- ~phi is: (forall p' \in P extending p) ~(p' ||- phi)

       p ||- phi_1 & phi_2 is: (p ||- phi_1) & (p ||- phi_2)

       p ||- (exists x) phi is: (exists x) (p ||- phi)

We will need the following definition later.

Definition.  p ||-w phi (p *weakly forces* phi) is an abbreviation for p
||- ~~phi.

The following exercises were suggested by John Cowles as a means for
gaining familiarity with the definition of forcing.

Exercise 1. Consider the formula (phi_1 OR phi_2) as an abbreviation for
~(~phi_1 & ~phi_2), Show that p ||- (phi_1 OR phi_2) is equivalent to
the following.

          (forall p' \in P extending p) (exists p" \in P extending p')
           ((p" ||- phi_1) OR (p" ||- phi_2))

Exercise 2. Consider the formula (forall x)phi as an abbreviation for
~(exists x)~phi, Show that p ||- (forall x)phi is equivalent to the
following.

          (forall x)
           (forall p1 \in P extending p)
            (exists p2 \in P extending p1) (p2 ||- phi).

Exercise 3. Prove that p ||-w phi is equivalent to the following.

          (forall p' \in P extending p)
           (exists p" \in P extending p') (p" ||- phi).

Exercise 4. Let phi be a formula of L[g].  Prove: M |= (p ||-
phi)[s[p<-p0]] implies M |= (p ||-w phi)[s[p<-p0]].

Exercise 5. Let phi be a formula of L[g].  Prove: M |= (p ||-
~phi)[s[p<-p0]] iff M |= (p ||-w ~phi)[s[p<-p0]].

[End of exercises.]

The definition of forcing stipulates how to view "p ||- phi(x1,...,xk)"
as a new formula theta(p,x1,...,xk).  That is, "||-" transforms
formulas, so for any first-order formula phi, "p ||- phi" is just
another first-order formula.  That observation shows that a formula such
as ((p ||- phi) OR (p ||- ~phi)) is really just another first-order
formula.  The following proposition thus follows easily.

Proposition 3. For any formula phi of L[g], {p0: M |= ((p ||- phi) OR (p
||- ~phi))[s[p<-p0]]]} is a dense subset of P, which (since it is
first-order definable with parameters in M) intersects G. -|

The following proposition is easily proved by a structural induction on
phi, and is left to the reader.

Proposition 4. Let phi be a formula of L[g].  Suppose

M |= (p ||- phi)[s[p<-p0]] and p1 extends p0.  Then

M |= (p ||- phi)[s[p<-p1]]. -|

We will also need the following.

Proposition 5. The following is dense for any finite set S of Nb-tuples:
{p \in P: for some <x_1 ... x_Nb> \in S, (list x_1 ... x_Nb) \in
strip-cars(p)}.  Thus, the function g0 is a total function. -|

The next lemma tells that the sentences true in M[G] are those that are
forced by an element of G.

Truth Lemma.  Let phi be a formula in L[g], let s be an assignment to
the free variables of phi, and let p be a variable not in the domain of
s.  Then M[G] |= phi[s] iff for some p0 \in G, M |= (p ||-
phi)[s[p<-p0]].

Proof.  The proof is by induction on the structure of phi.  First
suppose phi is atomic.  Let D* be the set of elements p0 \in P such that
every assoc-equal evaluation from the definition of forcing phi returns
a pair when A is bound to p0.  (Intuitively, this means that p0 is a
sufficiently large approximation from any G containing p0 to make sense
of phi in M[G].)  We make the following claim.

     (*)   For all p0 \in G such that p0 \in D*,
           M[G] |= phi[s] iff M |= (p ||- phi)[s[p<-p0]].

To prove the claim, fix p0 in both G and D*, and recall the function g0
constructed from G in the definition of M[G].  Suppose that t_1, ...,
t_Nb are terms and g(t_1, ..., t_Nb) is a subterm of phi.  Then s
assigns a value in M to each of the t_i.  Let a_i be the value assigned
by s to t_i.  Then g0(a_1, ..., a_Nb) = (cdr (assoc-equal (list a_1
... a_Nb) p0)), as the assoc-equal is a pair (since p0 \in D*) and has
the indicated value (because p0 \in G).  It follows by the definition of
formula phi' in the definition of forcing:

          M[G] |= phi[s]  iff  M |= phi'(p)[s[p<-p0]]

Moreover, because p0 \in D* it is clear that this holds if p0 is
replaced by an arbitrary extension of p0.  Then (*) easily follows.

By Proposition 5, D* is dense, so there is some p0 in the intersection
of D* and G.  The forward direction of the conclusion then follows by
(*).  The reverse direction is clear from (*) by application of
Proposition 2 to D* and Proposition 4.

Next, suppose M[G] |= ~phi[x].  Then it is not the case that M[G] |=
phi, so by the inductive hypothesis, there is no p0 \in G for which M |=
(p ||- phi)[s[p<-p0]].  By Proposition 3, there is p0 \in G for which M
|= (p ||- ~phi)[s[p<-p0]].  For the other direction, suppose it is not
the case that M[G] |= ~phi[s].  So M[G] |= phi[s], and by the inductive
hypothesis, there is p0 \in G for which M |= (p ||- phi)[s[p<-p0]].  It
follows that there is no p1 \in G for which M |= (p ||- ~phi)[s[p<-p1]],
since from such p1 we can find a common extension p2 of p0 and p1 (since
G is generic), and since p2 extends p0 then by Proposition 4, M |= (p
||- phi)[s[p<-p2]], contradicting (by definition of forcing) M |= (p ||-
~phi)[s[p<-p1]] since p2 extends p1.

The case (phi_1 & phi_2) follows easily from the inductive hypothesis.
For the forward direction, apply Proposition 4 and the observation that
by genericity, if p0 \in G and p1 \in G then p0 and p1 they have a
common extension in G.

Finally, the case (exists x) phi follows trivially from the inductive
hypothesis. -|

Truth Lemma Corollary.  The Truth Lemma holds with ||-w replacing ||-.

Proof.  This is clear by applying the Truth Lemma to ~~phi. -|

Here is our main theorem.  Recall that all first-order theories in our
ACL2 context satisfy the e0-induction scheme.

Theorem.  M[G] satisfies e0-induction.

Proof.  We consider an arbitrary instance of e0-induction in L[g],
stated using a strict well-founded relation <| and a formula phi.  We
write phi(y) to indicate that y may be among the free variables of phi,
and phi(y<-x) to denote the result of substituting x for y in phi.

       theta(y):   (forall y) [((forall x <| y) phi(y<-x)) -> phi(y)]
                -> (forall y) phi(y)

Our goal is to prove that theta holds in M[G].

Below, we abuse notation by leaving assignments implicit and by writing
"p ||- phi(y0)" to signify that the formula (p ||- phi(y)) is true in M
under the extension of the explicit assignment that binds y to y0.  We
believe that the intended meaning will be clear.

Consider the following set D.

       D = {p \in P: either p ||-w phi(y0) for all y0,
                     or else
                     for some y0, p ||- ~phi(y0) and
                                  for all y1 <| y0 p ||-w phi(y1)}.

The set D is clearly first-order definable (with parameters) in M.  We
claim that D is a dense subset of P.  For suppose p0 \in P; we find p1
\in D extending p0, as follows.  If p0 ||-w phi(y0) for all y0, then we
may take p1 to be p0.  Otherwise, by definition of ||-w and ||-, there
is some y0 such that for some extension p0' of p0, p0' ||- ~phi(y0).
Pick a <|-minimal such y0, and correspondingly pick p1 so that p1
extends p0 and p1 ||- ~phi(y0).  In order to show that p1 \in D, it
remains to show that for all y1 <| y0, p1 ||-w phi(y1), i.e., there is
no q extending p1 such that q ||- ~phi(y1).  This is indeed the case
since otherwise q and y1 would contradict the <|-minimality of y0.

Applying the genericity of G and just-proved density of D, pick p0 \in G
such that p0 \in D.  If p0 ||-w phi(y0) for all y0, then by the Truth
Lemma Corollary, M[G] |= phi(y0) for all y0, and thus M[G] |= theta.
Otherwise, since p0 \in D we may choose y0 such that p0 ||- ~phi(y0) and
for all y1 <| y0, p0 ||-w phi(y1).  By the Truth Lemma, since p0 \in G
we have:

     (1)   M[G] |= ~phi(y0).
     (2)   For all y1 <| y0, M[G] |= ~~phi(y1), i.e., M[G] |= phi(y1).

It follows that the antecedent of theta is false in M[G], as witnessed
by y = y0; thus M[G] |= theta. -|

Remark.  We close by returning, as promised above, to the question of
why so much care is necessary in constructing an expansion of M.  We
assume familiarity here with the notion of a "non-standard" natural
number of M, i.e., one that is greater than the interpretation of any
term that has the form (+ 1 1 1 ... 1).  Here is a very simple example
that illustrates the need for some care.  Consider the following event,
which introduces a function foo with the following property: for all x,
if natp(x) then natp(foo(x)).

          (defchoose foo (y) (x)
            (implies (natp x) (natp y)))

Certainly we can build a model of the above property from a model M of
the ground-zero theory, by interpreting foo so that for all x for which
M satisfies natp(x), foo(x) is also a natp in M.  But suppose we start
with a non-standard model M of the ground-zero theory, and we happen to
define foo(x) to be 1 for all non-standard natural numbers x and 0 for
all other x.  The resulting expansion of M will not satisfy the
e0-induction scheme or even the ordinary natural number induction
scheme: foo(0)=0 holds in that expansion as does the implication
foo(n)=0 => foo(n+1)=0 for every natural number n of M, standard or not;
and yet foo(k)=0 fails for every non-standard natural number k of M.

DEFCONG    prove that one equivalence relation preserves another in a given
 argument position of a given function

     Example:
     (defcong set-equal iff (memb x y) 2)

     is an abbreviation for
     (defthm set-equal-implies-iff-memb-2
       (implies (set-equal y y-equiv)
                (iff (memb x y) (memb x y-equiv)))
       :rule-classes (:congruence))

See CONGRUENCE and also see EQUIVALENCE.

     General Form:
     (defcong equiv1 equiv2 term k
       :rule-classes rule-classes
       :instructions instructions
       :hints hints
       :otf-flg otf-flg
       :event-name event-name
       :doc doc)

where equiv1 and equiv2 are known equivalence relations, term is a call
of a function fn on the correct number of distinct variable arguments
(fn x1 ... xn), k is a positive integer less than or equal to the arity
of fn, and other arguments are as specified in the documentation for
defthm.  The defcong macro expands into a call of defthm.  The name of
the defthm event is equiv1-implies-equiv2-fn-k unless an :event-name
keyword argument is supplied for the name.  The term of the theorem is

     (implies (equiv1 xk yk)
              (equiv2 (fn x1... xk ...xn)
                      (fn x1... yk ...xn))).

The rule-class :congruence is added to the rule-classes specified, if it
is not already there.  All other arguments to the generated defthm form
are as specified by the keyword arguments above.

DEFCONST    define a constant

     Examples:
     (defconst *digits* '(0 1 2 3 4 5 6 7 8 9))
     (defconst *n-digits* (the unsigned-byte (length *digits*)))

     General Form:
     (defconst name term doc-string)

where name is a symbol beginning and ending with the character *, term
is a variable-free term that is evaluated to determine the value of the
constant, and doc-string is an optional documentation string (see
DOC-STRING).

When a constant symbol is used as a term, ACL2 replaces it by its value;
see TERM.

It may be of interest to note that defconst is implemented at the lisp
level using defparameter, as opposed to defconstant.  (Implementation
note: this is important for proper support of undoing and redefinition.)

DEFDOC    add a documentation topic

     Examples:
     (defdoc interp-section
        ":Doc-Section ...")

     General Form:
     (defdoc name doc-string)

where name is a symbol or string to be documented and doc-string is a
documentation string (see DOC-STRING).  This event adds the
documentation string for symbol name to the :doc data base.  It may also
be used to change the documentation for name if name already has
documentation.  The difference between this event and deflabel is that,
unlike deflabel (but like table), it does not mark the current history
with the name.  But like deflabel, defdoc events are never considered
redundant (see REDUNDANT-EVENTS).

See DEFLABEL for a means of attaching a documentation string to
a name that marks the current history with that name.  We now elaborate
further on how defdoc may be useful in place of deflabel.

It is usually sufficient to use deflabel when you might be tempted to
use defdoc.  However, unlike deflabel, defdoc does not mark the current
history with name.  Thus, defdoc is useful for introducing the
documentation for a defun or deftheory event, for example, several
events before the function or theory is actually defined.

For example, suppose you want to define a theory (using deftheory).  You
need to prove the lemmas in that theory before executing the deftheory
event.  However, it is quite natural to define a :doc-section (see
DOC-STRING) whose name is the name of the theory to be defined, and
put the documentation for that theory's lemmas into that :doc-section.
Defdoc is ideal for this purpose, since it can be used to introduce the
:doc-section, followed by the lemmas referring to that :doc-section, and
finally concluded with a deftheory event of the same name.  If deflabel
were used instead of defdoc, for example, then the deftheory event would
be disallowed because the name is already in use by the deflabel event.

We also imagine that some users will want to use defdoc to insert the
documentation for a function under development.  This defdoc event would
be followed by definitions of all the subroutines of that function,
followed in turn by the function definition itself.

Any time defdoc is used to attach documentation to an already-documented
name, the name must not be attached to a new :doc-section.  We make this
requirement as a way of avoiding loops in the documentation tree.  When
documentation is redefined, a warning will be printed to the terminal.

DEFEQUIV    prove that a function is an equivalence relation

     Example:
     (defequiv set-equal)

     is an abbreviation for
     (defthm set-equal-is-an-equivalence
       (and (booleanp (set-equal x y))
            (set-equal x x)
            (implies (set-equal x y) (set-equal y x))
            (implies (and (set-equal x y)
                          (set-equal y z))
                     (set-equal x z)))
       :rule-classes (:equivalence))

See EQUIVALENCE.

     General Form:
     (defequiv fn
       :rule-classes rule-classes
       :instructions instructions
       :hints hints
       :otf-flg otf-flg
       :event-name event-name
       :doc doc)

where fn is a function symbol of arity 2, event-name, if supplied, is a
symbol, and all other arguments are as specified in the documentation
for defthm.  The defequiv macro expands into a call of defthm.  The name
of the defthm is fn-is-an-equivalence, unless event-name is supplied, in
which case event-name is the name used.  The term generated for the
defthm event states that fn is Boolean, reflexive, symmetric, and
transitive.  The rule-class :equivalence is added to the rule-classes
specified, if it is not already there.  All other arguments to the
generated defthm form are as specified by the other keyword arguments
above.

DEFEVALUATOR    introduce an evaluator function

     Example:
     (defevaluator evl evl-list
       ((length x) (member x y)))

See META.

     General Form:
     (defevaluator ev ev-list
        ((g1 x1 ... xn_1)
         ...
         (gk x1 ... xn_k))

where ev and ev-list are new function symbols and g1, ..., gk are old
function symbols with the indicated number of formals, i.e., each gi has
n_i formals.

This function provides a convenient way to constrain ev and ev-list
to be mutually-recursive evaluator functions for the symbols g1,
..., gk.  Roughly speaking, an evaluator function for a fixed,
finite set of function symbols is a restriction of the universal
evaluator to terms composed of variables, constants, lambda expressions,
and applications of the given functions.  However, evaluator functions
are constrained rather than defined, so that the proof that a given
metafunction is correct vis-a-vis a particular evaluator function can be
lifted (by functional instantiation) to a proof that it is correct for
any larger evaluator function.  See META for a discussion of
metafunctions.

Defevaluator executes an encapsulate after generating the appropriate
defun and defthm events.  Perhaps the easiest way to understand what
defevaluator does is to execute the keyword command

     :trans1 (defevaluator evl evl-list ((length x) (member x y)))

and inspect the output.  This trick is also useful in the rare case that
the event fails because a hint is needed.  In that case, the output of
:trans1 can be edited by adding hints, then submitted directly.

Formally, ev is said to be an "evaluator function for g1,
..., gk, with mutually-recursive counterpart ev-list" iff
ev and ev-list are constrained functions satisfying just the constraints
discussed below.

Ev and ev-list must satisfy constraints (1)-(4) and (k):

     (1) How to ev a variable symbol:
         (implies (symbolp x)
                  (equal (ev x a) (cdr (assoc-eq x a))))

     (2) How to ev a constant:
         (implies (and (consp x)
                       (equal (car x) 'quote))
                  (equal (ev x a) (cadr x)))

     (3) How to ev a lambda application:
         (implies (and (consp x)
                       (consp (car x)))
                  (equal (ev x a)
                         (ev (caddar x)
                             (pairlis$ (cadar x)
                                       (ev-list (cdr x) a)))))

     (4) How to ev an argument list:
         (implies (consp x-lst)
                  (equal (ev-list x-lst a)
                         (cons (ev (car x-lst) a)
                               (ev-list (cdr x-lst) a))))
         (implies (not (consp x-lst))
                  (equal (ev-list x-lst a)
                         nil))

     (k) For each i from 1 to k, how to ev an application of gi,
         where gi is a function symbol of n arguments:
         (implies (and (consp x)
                       (equal (car x) 'gi))
                  (equal (ev x a)
                         (gi (ev x1 a)
                             ...
                             (ev xn a)))),
         where xi is the (cad...dr x) expression equivalent to (nth i x).

Defevaluator defines suitable witnesses for ev and ev-list, proves the
theorems about them, and constrains ev and ev-list appropriately.  We
expect defevaluator to work without assistance from you, though the
proofs do take some time and generate a lot of output.  The proofs are
done in the context of a fixed theory, namely the value of the constant
*defevaluator-form-base-theory*.

(Aside: (3) above may seem surprising, since the bindings of a are not
included in the environment that is used to evaluate the lambda body,
(caddar x).  However, ACL2 lambda expressions are all *closed*: in
(lambda (v1 ... vn) body), the only free variables in body are among the
vi.  See TERM.)