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

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

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

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

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

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

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.

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 subset (if p2 \in G and p2 extends
p1 then p1 \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 ((x_1 ... 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 p0 in P, p1 in P,
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 us 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 and its
corollary, since p0 \in G we have:

     (1)   M[G] |= ~phi(y0).
     (2)   For all y1 <| y0, 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.