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.

BIBLIOGRAPHY    reports about ACL2

For a list of notes and reports about ACL2, see

http://www.cs.utexas.edu/users/moore/publications/acl2-papers.html.

Below is a list of notes and reports pertaining to ACL2.

BIND-FREE    to bind free variables of a rewrite or linear rule

     Examples:
     (IMPLIES (AND (RATIONALP LHS)
                   (RATIONALP RHS)
                   (BIND-FREE (FIND-MATCH-IN-PLUS-NESTS LHS RHS) (X)))
              (EQUAL (EQUAL LHS RHS)
                     (EQUAL (+ (- X) LHS) (+ (- X) RHS))))

     (IMPLIES (AND (BIND-FREE
                     (FIND-RATIONAL-MATCH-IN-TIMES-NESTS LHS RHS MFC STATE)
                     (X))
                   (RATIONALP X)
                   (CASE-SPLIT (NOT (EQUAL X 0))))
              (EQUAL (< LHS RHS)
                     (IF (< 0 X)
                         (< (* (/ X) LHS) (* (/ X) RHS))
                        (< (* (/ X) RHS) (* (/ X) LHS)))))

General Forms:

     (BIND-FREE term var-list)
     (BIND-FREE term t)
     (BIND-FREE term)

A rule which uses a bind-free hypothesis has similarities to both a rule
which uses a syntaxp hypothesis and to a :meta rule.  Bind-free is like
syntaxp, in that it logically always returns t but may affect the
application of a :rewrite or :linear rule when it is called at the
top-level of a hypothesis.  It is like a :meta rule, in that it allows
the user to perform transformations of terms under progammatic control.

Note that a bind-free hypothesis does not, in general, deal with the
meaning or semantics or values of the terms, but rather with their
syntactic forms.  Before attempting to write a rule which uses
bind-free, the user should be familiar with syntaxp and the internal
form that ACL2 uses for terms.  This internal form is similar to what
the user sees, but there are subtle and important differences.  Trans
can be used to view this internal form.

Just as for a syntaxp hypothesis, there are two types of bind-free
hypotheses.  The simpler type of bind-free hypothesis may be used as the
nth hypothesis in a :rewrite or :linear rule whose :corollary is
(implies (and hyp1 ... hypn ... hypk) (equiv lhs rhs)) provided term is
a term, term contains at least one variable, and every variable occuring
freely in term occurs freely in lhs or in some hypi, i<n.  In addition,
term must not use any stobjs.  (Later below we will describe the second
type, an *extended* bind-free hypothesis, which may use state.)

We begin our description of bind-free by examining the first example
above in some detail.

We wish to write a rule which will cancel "like" addends from both sides
of an equality.  Clearly, one could write a series of rules such as

     (DEFTHM THE-HARD-WAY-2-1
        (EQUAL (EQUAL (+ A X B)
                      (+ X C))
               (EQUAL (+ A B)
                      (FIX C))))

with one rule for each combination of positions the matching addends
might be found in (if one knew before-hand the maximum number of addends
that would appear in a sum).  But there is a better way.  (In what
follows, we assume the presence of an appropriate set of rules for
simplifying sums.)

Consider the following definitions and theorem:

     (DEFUN INTERSECTION-EQUAL (X Y)
       (COND ((ENDP X)
              NIL)
             ((MEMBER-EQUAL (CAR X) Y)
              (CONS (CAR X) (INTERSECTION-EQUAL (CDR X) Y)))
             (T
              (INTERSECTION-EQUAL (CDR X) Y))))

     (DEFUN PLUS-LEAVES (TERM)
       (IF (EQ (FN-SYMB TERM) 'BINARY-+)
           (CONS (FARGN TERM 1)
                 (PLUS-LEAVES (FARGN TERM 2)))
         (LIST TERM)))

     (DEFUN FIND-MATCH-IN-PLUS-NESTS (LHS RHS)
       (IF (AND (EQ (FN-SYMB LHS) 'BINARY-+)
                (EQ (FN-SYMB RHS) 'BINARY-+))
           (LET ((COMMON-ADDENDS (INTERSECTION-EQUAL (PLUS-LEAVES LHS)
                                                     (PLUS-LEAVES RHS))))
             (IF COMMON-ADDENDS
                 (LIST (CONS 'X (CAR COMMON-ADDENDS)))
               NIL))
         NIL))

     (DEFTHM CANCEL-MATCHING-ADDENDS-EQUAL
       (IMPLIES (AND (RATIONALP LHS)
                     (RATIONALP RHS)
                     (BIND-FREE (FIND-MATCH-IN-PLUS-NESTS LHS RHS) (X)))
                (EQUAL (EQUAL LHS RHS)
                       (EQUAL (+ (- X) LHS) (+ (- X) RHS)))))

How is this rule applied to the following term?

     (equal (+ 3 (expt a n) (foo a c))
            (+ (bar b) (expt a n)))

As mentioned above, the internal form of an ACL2 term is not always what
one sees printed out by ACL2.  In this case, by using :trans one can see
that the term is stored internally as

     (equal (binary-+ '3
                      (binary-+ (expt a n) (foo a c)))
            (binary-+ (bar b) (expt a n))).

When ACL2 attempts to apply cancel-matching-addends-equal to the term
under discussion, it first forms a substitution that instantiates the
left-hand side of the conclusion so that it is identical to the target
term.  This substitution is kept track of by the substitution alist:

     ((LHS . (binary-+ '3
                        (binary-+ (expt a n) (foo a c))))
      (RHS . (binary-+ (bar b) (expt a n)))).

ACL2 then attempts to relieve the hypotheses in the order they were
given. Ordinarily this means that we instantiate each hypothesis with
our substitution and then attempt to rewrite the resulting instance to
true.  Thus, in order to relieve the first hypothesis, we rewrite:

     (RATIONALP (binary-+ '3
                           (binary-+ (expt a n) (foo a c)))).

Let us assume that the first two hypotheses rewrite to t.  How do we
relieve the bind-free hypothesis?  Just as for a syntaxp hypothesis,
ACL2 evaluates (find-match-in-plus-nests lhs rhs) in an environment
where lhs and rhs are instantiated as determined by the substitution.
In this case we evaluate

     (FIND-MATCH-IN-PLUS-NESTS '(binary-+ '3
                                           (binary-+ (expt a n) (foo a c)))
                               '(binary-+ (bar b) (expt a n))).

Observe that, just as in the case of a syntaxp hypothesis, we substitute
the quotation of the variables bindings into the term to be evaluated.
See SYNTAXP for the reasons for this.  The result of this
evaluation, ((X . (EXPT A N))), is then used to extend the substitution
alist:

     ((X . (EXPT A N))
      (LHS . (binary-+ '3
                        (binary-+ (expt a n) (foo a c))))
      (RHS . (binary-+ (bar b) (expt a n)))),

and this extended substitution determines
cancel-matching-addends-equal's result:

     (EQUAL (+ (- X) LHS) (+ (- X) RHS))
     ==>
     (EQUAL (+ (- (EXPT A N)) 3 (EXPT A N) (FOO A C))
            (+ (- (EXPT A N)) (BAR B) (EXPT A N))).

Question: What is the internal form of this result?

Hint: Use :trans.

When this rule fires, it adds the negation of a common term to both
sides of the equality by selecting a binding for the otherwise-free
variable x, under programmatic control.  Note that other mechanisms such
as the binding of free-variables may also extend the substitution alist.

Just as for a syntaxp test, a bind-free form signals failure by
returning nil.  However, while a syntaxp test signals success by
returning true, a bind-free form signals success by returning an alist
which is used to extend the current substitution alist.  Because of this
use of the alist, there are several restrictions on it -- in particular
the alist must only bind variables, these variables must not be already
bound by the substitution alist, and the variables must be bound to ACL2
terms.  If term returns an alist and the alist meets these restrictions,
we append the alist to the substitution alist and use the result as the
new current substitution alist.  This new current substitution alist is
then used when we attempt to relieve the next hypothesis or, if there
are no more, instantiate the right hand side of the rule.

There is also a second, optional, var-list argument to a bind-free
hypothesis.  If provided, it must be either t or a list of variables.
If it is not provided, it defaults to t.  If it is a list of variables,
this second argument is used to place a further restriction on the
possible values of the alist to be returned by term: any variables bound
in the alist must be present in the list of variables.  We strongly
recommend the use of this list of variables, as it allows some
consistency checks to be performed at the time of the rule's admittance
which are not possible otherwise.

An extended bind-free hypothesis is similar to the simple type described
above, but it uses two additional variables, mfc and state, which must
not be bound by the left hand side or an earlier hypothesis of the rule.
They must be the last two variables mentioned by term: first mfc, then
state.  These two variables give access to the functions mfc-xxx; see
EXTENDED-METAFUNCTIONS.  As described there, mfc is bound to the
so-called metafunction-context and state to ACL2's state.  See
BIND-FREE-EXAMPLESfor examples of the use of these extended bind-free
hypotheses.

BIND-FREE-EXAMPLES    examples pertaining to bind-free hypotheses

See BIND-FREE for a basic discussion of the use of bind-free to
control rewriting.

We give examples of the use of bind-free hypotheses from the perspective
of a user interested in reasoning about arithmetic, but it should be
clear that bind-free can be used for many other purposes also.

EXAMPLE 1: Cancel a common factor.

     (defun bind-divisor (a b)

     ; If a and b are polynomials with a common factor c, we return a
     ; binding for x.  We could imagine writing get-factor to compute the
     ; gcd, or simply to return a single non-invertible factor.

       (let ((c (get-factor a b)))
         (and c (list (cons 'x c)))))

     (defthm cancel-factor
       ;; We use case-split here to ensure that, once we have selected
       ;; a binding for x, the rest of the hypotheses will be relieved.
       (implies (and (acl2-numberp a)
                     (acl2-numberp b)
                     (bind-free (bind-divisor a b) (x))
                     (case-split (not (equal x 0)))
                     (case-split (acl2-numberp x)))
                (iff (equal a b)
                     (equal (/ a x) (/ b x)))))

EXAMPLE 2: Pull integer summand out of floor.  Note: This example has an
*extended* bind-free hypothesis, which uses the term (find-int-in-sum
sum mfc state).

     (defun fl (x)
       ;; This function is defined, and used, in the IHS books.
       (floor x 1))

     (defun int-binding (term mfc state)
       ;; The call to mfc-ts returns the encoded type of term.
       ;; Thus, we are asking if term is known by type reasoning to
       ;; be an integer.
       (declare (xargs :stobjs (state) :mode :program))
       (if (ts-subsetp (mfc-ts term mfc state)
                       *ts-integer*)
             (list (cons 'int term))
       nil))

     (defun find-int-in-sum (sum mfc state)
       (declare (xargs :stobjs (state) :mode :program))
       (if (and (nvariablep sum)
                (not (fquotep sum))
                (eq (ffn-symb sum) 'binary-+))
           (or (int-binding (fargn sum 1) mfc state)
               (find-int-in-sum (fargn sum 2) mfc state))
         (int-binding sum mfc state)))

     ; Some additional work is required to prove the following.  So for
     ; purposes of illustration, we wrap skip-proofs around the defthm.

     (skip-proofs
      (defthm cancel-fl-int
       ;; The use of case-split is probably not needed, since we should
       ;; know that int is an integer by the way we selected it.  But this
       ;; is safer.
        (implies (and (acl2-numberp sum)
                      (bind-free (find-int-in-sum sum mfc state) (int))
                      (case-split (integerp int)))
                 (equal (fl sum)
                        (+ int (fl (- sum int)))))
        :rule-classes ((:rewrite :match-free :all)))
     )

     ; Arithmetic libraries will have this sort of lemma.
     (defthm hack (equal (+ (- x) x y) (fix y)))

     (in-theory (disable fl))

     (thm (implies (and (integerp x) (acl2-numberp y))
                   (equal (fl (+ x y)) (+ x (fl y)))))

EXAMPLE 3: Simplify terms such as (equal (+ a (* a b)) 0)

     (defun factors (product)
       ;; We return a list of all the factors of product.  We do not
       ;; require that product actually be a product.
       (if (eq (fn-symb product) 'BINARY-*)
           (cons (fargn product 1)
                 (factors (fargn product 2)))
         (list product)))

     (defun make-product (factors)
       ;; Factors is assumed to be a list of ACL2 terms.  We return an
       ;; ACL2 term which is the product of all the ellements of the
       ;; list factors.
       (cond ((atom factors)
              "1)
             ((null (cdr factors))
              (car factors))
             ((null (cddr factors))
              (list 'BINARY-* (car factors) (cadr factors)))
             (t
              (list 'BINARY-* (car factors) (make-product (cdr factors))))))

     (defun quotient (common-factors sum)
       ;; Common-factors is a list of ACL2 terms.   Sum is an ACL2 term each
       ;; of whose addends have common-factors as factors.  We return
       ;; (/ sum (make-product common-factors)).
       (if (eq (fn-symb sum) 'BINARY-+)
           (let ((first (make-product (set-difference-equal (factors (fargn sum 1))
                                                            common-factors))))
             (list 'BINARY-+ first (quotient common-factors (fargn sum 2))))
         (make-product (set-difference-equal (factors sum)
                                             common-factors))))

     (defun intersection-equal (x y)
       (cond ((endp x)
              nil)
             ((member-equal (car x) y)
              (cons (car x) (intersection-equal (cdr x) y)))
             (t
              (intersection-equal (cdr x) y))))

     (defun common-factors (factors sum)
       ;; Factors is a list of the factors common to all of the addends
       ;; examined so far.  On entry, factors is a list of the factors in
       ;; the first addend of the original sum, and sum is the rest of the
       ;; addends.  We sweep through sum, trying to find a set of factors
       ;; common to all the addends of sum.
       (declare (xargs :measure (acl2-count sum)))
       (cond ((null factors)
              nil)
             ((eq (fn-symb sum) 'BINARY-+)
              (common-factors (intersection-equal factors (factors (fargn sum 1)))
                              (fargn sum 2)))
             (t
              (intersection-equal factors (factors sum)))))

     (defun simplify-terms-such-as-a+ab-rel-0-fn (sum)
       ;; If we can find a set of factors common to all the addends of sum,
       ;; we return an alist binding common to the product of these common
       ;; factors and binding quotient to (/ sum common).
       (if (eq (fn-symb sum) 'BINARY-+)
           (let ((common-factors (common-factors (factors (fargn sum 1))
                                                 (fargn sum 2))))
             (if common-factors
                 (let ((common (make-product common-factors))
                       (quotient (quotient common-factors sum)))
                   (list (cons 'common common)
                         (cons 'quotient quotient)))
               nil))
         nil))

     (defthm simplify-terms-such-as-a+ab-=-0
       (implies (and (bind-free
                      (simplify-terms-such-as-a+ab-rel-0-fn sum)
                      (common quotient))
                     (case-split (acl2-numberp common))
                     (case-split (acl2-numberp quotient))
                     (case-split (equal sum
                                        (* common quotient))))
                (equal (equal sum 0)
                       (or (equal common 0)
                           (equal quotient 0)))))

     (thm (equal (equal (+ u (* u v)) 0)
           (or (equal u 0) (equal v -1))))

BREAKS    Common Lisp breaks

     Example:
     Broken at PROVE.  Type :H for Help.
     >>:Q

     ACL2 !>

You may interrupt the system by typing various control character
sequences.  The precise sequences are determined by the host Lisp and
operating system environment.  For example, in GCL and Allegro Common
Lisp, a console interrupt is caused by typing "ctrl-c".  If, however,
the GCL or Allegro is running in an Emacs shell buffer, one must type
"ctrl-c ctrl-c".

If a break occurs, e.g. because of a bug in ACL2 or a user interrupt,
the break will run a Common Lisp read-eval-print loop, not an ACL2
read-eval-print loop.  This may not be obvious if the prompts in the two
loops are similar.  Because you are typing to a Common Lisp evaluator,
you must be careful.  It is possible to damage your ACL2 state in
irreparable ways by executing non-ACL2 Common Lisp.  It is even possible
to disrupt and render inaccurate the interrupted evaluation of a simple
ACL2 expression.

Quitting from the break (as with :q in GCL, :reset in Allegro CL, and q
in CMU CL) will return to the innermost ACL2 read-eval-print loop.
Before the loop is continued, any pending cleanup forms from
acl2-unwind-protects are evaluated (unless acl2::*acl2-panic-exit-flg*
is non-nil, in which case no cleanup is done).  Note that if you are
within a brr environment when the break occurs, quitting from the break
will only return you to that environment, not to the top of ACL2's
read-eval-print loop.

For ACL2 built on most host Common Lisps, you will see the string [RAW
LISP] in the prompt at a break, to emphasize that one is inside a break
and hence should quit from the break.  For some host Common Lisps, the
top-level prompt also contains the string [RAW LISP].  See
PROMPT for how to control printing of that string.

If you submit the token #. to the raw lisp break, an abort is generally
executed.  (Some underlying Lisp systems, however, reset the read table
(*readtable*), in which case you should type a number after #. and then
follow the directions in the preceding paragraph.)  Control is passed to
the outermost ACL2 read-eval-print loop (lp).  Again, unwind-protection
cleanup forms are executed first.

BY    hints keyword :BY

See HINTS.

CASE-SPLIT    like force but immediately splits the top-level goal on the hypothesis

When a hypothesis of a conditional rule has the form (case-split hyp) it
is logically equivalent to hyp.  However it affects the application of
the rule generated as follows: if ACL2 attempts to apply the rule but
cannot establish that the required instance of hyp holds in the current
context, it considers the hypothesis true anyhow, but (assuming all
hypotheses are seen to be true and the rule is applied) creates a
subgoal in which that instance of hyp is assumed false.  (There are
exceptions, noted below.)

For example, given the rule

     (defthm p1->p2
       (implies (case-split (p1 x))
                (p2 x)))

then an attempt to prove

     (implies (p3 x) (p2 (car x)))

can give rise to a single subgoal:

     (IMPLIES (AND (NOT (P1 (CAR X))) (P3 X))
              (P2 (CAR X))).

Unlike force, case-split does not delay the "false case" to a forcing
round but tackles it more or less immediately.

The special "split" treatment of case-split can be disabled by disabling
forcing: see FORCE for a discussion of disabling forcing, and
also see DISABLE-FORCING.  Finally, we should mention that the
rewriter is never willing to split when there is an if term present in
the goal being simplified.  Since and terms and or terms are merely
abbreviations for if terms, they also prevent splitting.  Note that if
terms are ultimately eliminated using the ordinary flow of the proof
(but see SET-CASE-SPLIT-LIMITATIONS), so case-split will
ultimately function as intended.

When in the proof checker, case-split behaves like force.

CASE-SPLIT-LIMITATIONS    a list of two "numbers" limiting the number of cases produced at once

     Examples:
     ACL2 !>(case-split-limitations (w state))
     (500 100)

With the setting above, clausify will not try subsumption/replacement if
more than 500 clauses are involved.  Furthermore, the simplifier, as it
sweeps over a clause, will inhibit further case splits when it has
accumulated 100 subgoals.  This inhibition is implemented by continuing
to rewrite subsequent literals but not splitting out their cases.  This
can produce literals containing IFs.

See SET-CASE-SPLIT-LIMITATIONS for a more general discussion.

CASES    hints keyword :CASES

See HINTS.

CHECK-SUM    assigning "often unique" integers to files and objects

A "check sum" is an integer in some fixed range computed from the
printed representation of an object, e.g., the sum, modulo 2**32, of the
ascii codes of all the characters in the printed representation.

Ideally, you would like the check sum of an object to be uniquely
associated with that object, like a fingerprint.  It could then be used
as a convenient way to recognize the object in the future: you could
remember the check sum (which is relatively small) and when an object is
presented to you and alleged to be the special one you could compute its
check sum and see if indeed it was.  Alas, there are many more objects
than check sums (after all, each check sum is an object, and then
there's t).  So you try to design a check sum algorithm that maps
similar looking objects far apart, in the hopes that corruptions and
counterfeits -- which appear to be similar to the object -- have
different check sums.  Nevertheless, the best you can do is a
many-to-one map.  If an object with a different check sum is presented,
you can be positive it is not the special object.  But if an object with
the same check sum is presented, you have no grounds for positive
identification.

The basic check sum algorithm in ACL2 is called check-sum-obj, which
computes the check sum of an ACL2 object.  Roughly speaking, we scan the
print representation of the object and, for each character encountered,
we multiply the ascii code of the character times its position in the
stream (modulo a certain prime) and then add (modulo a certain prime)
that into the running sum.  This is inaccurate in many senses (for
example, we don't always use the ascii code and we see numbers as though
they were printed in base 127) but indicates the basic idea.

ACL2 uses check sums to increase security in the books mechanism; see
CERTIFICATE.

CLAUSE-IDENTIFIER    the internal form of a goal-spec

To each goal-spec, str, there corresponds a clause-identifier produced
by (parse-clause-id str).  For example,

     (parse-clause-id "[2]Subgoal *4.5.6/7.8.9"'")

returns ((2 4 5 6) (7 8 9) . 3).

The function string-for-tilde-@-clause-id-phrase inverts parse-clause-id
in the sense that given a clause identifier it returns the corresponding
goal-spec.

As noted in the documentation for goal-spec, each clause printed in the
theorem prover's proof attempt is identified by a name.  When these
names are represented as strings they are called "goal specs."  Such
strings are used to specify where in the proof attempt a given hint is
to be applied.  The function parse-clause-id converts goal-specs into
clause identifiers, which are cons-trees containing natural numbers.

Examples of goal-specs and their corresponding clause identifiers are
shown below.

                  parse-clause-id
                        -->

     "Goal"                       ((0) NIL . 0)
     "Subgoal 3.2.1'"             ((0) (3 2 1) . 1)
     "[2]Subgoal *4.5.6/7.8.9"'" ((2 4 5 6) (7 8 9) . 3)

                        <--
           string-for-tilde-@-clause-id-phrase

The caar of a clause id specifies the forcing round, the cdar specifies
the goal being proved by induction, the cadr specifies the particular
subgoal, and the cddr is the number of primes in that subgoal.

Internally, the system maintains clause ids, not goal-specs.  The system
prints clause ids in the form shown by goal-specs.  When a goal-spec is
used in a hint, it is parsed (before the proof attempt begins) into a
clause id.  During the proof attempt, the system watches for the clause
id and uses the corresponding hint when the id arises.  (Because of the
expense of creating and garbage collecting a lot of strings, this design
is more efficient than the alternative.)

CLOSE-INPUT-CHANNEL    See IO.

CLOSE-OUTPUT-CHANNEL    See IO.

COMMAND    forms you type at the top-level, but...

...the word "command" usually refers to a top-level form whose
evaluation produces a new logical world.

     Typical commands are:
     (defun foo (x) (cons x x))
     (defthm consp-foo (consp (foo x)))
     (defrec pair (hd . tl) nil)

The first two forms are examples of commands that are in fact primitive
events.  See EVENTS.  Defrec, on the other hand, is a macro that
expands into a progn of several primitive events.  In general, a world
extending command generates one or more events.

Both events and commands leave landmarks on the world that enable us to
determine how the given world was created from the previous one.  Most
of your interactions will occur at the command level, i.e., you type
commands, you print previous commands, and you undo back through
commands.  Commands are denoted by command descriptors.  See
COMMAND-DESCRIPTOR.

COMMAND-DESCRIPTOR    an object describing a particular command typed by the user

     Examples:

     :max      ; the command most recently typed by the user
     :x        ; synonymous with :max
     (:x -1)   ; the command before the most recent one
     (:x -2)   ; the command before that
     :x-2      ; synonymous with (:x -2)
     5         ; the fifth command typed by the user
     1         ; the first command typed by the user
     0         ; the last command of the system initialization
     -1        ; the next-to-last initialization command
     :min      ; the first command of the initialization
     fn        ; the command that introduced the logical name fn
     (:search (defmacro foo-bar))
               ; the first command encountered in a search from :max to
               ; 0 that either contains defmacro and foo-bar in the
               ; command form or contains defmacro and foo-bar in some
               ; event within its block.

The recorded history of your interactions with the top-level ACL2
command loop is marked by the commands you typed that changed the
logical world.  Each such command generated one or more events, since
the only way for you to change the logical world is to execute an event
function.  See COMMAND and see EVENTS.  We divide
history into "command blocks," grouping together each world changing
command and its events.  A "command descriptor" is an object that can be
used to describe a particular command in the history of the ongoing
session.

Each command is assigned a unique integer called its "command number"
which indicates the command's position in the chronological ordering of
all of the commands ever executed in this session (including those
executed to initialize the system).  We assign the number 1 to the first
command you type to ACL2.  We assign 2 to the second and so on.  The
non-positive integers are assigned to "prehistoric" commands, i.e., the
commands used to initialize the ACL2 system: 0 is the last command of
the initialization, -1 is the one before that, etc.

The legal command descriptors are described below.  We use n to denote
any integer, sym to denote any logical name (see LOGICAL-NAME),
and cd to denote, recursively, any command descriptor.

      command                   command
     descriptor                described

     :max   -- the most recently executed command (i.e., the one with
               the largest command number)
     :x     -- synonymous with :max
     :x-k   -- synonymous with (:x -k), if k is an integer and k>0
     :min   -- the earliest command (i.e., the one with the smallest
               command number and hence the first command of the system
               initialization)
     n      -- command number n  (If n is not in the
               range :min<=n<=:max, n is replaced by the nearest of :min
               and :max.)
     sym    -- the command that introduced the logical name sym
     (cd n) -- the command whose number is n plus the command number of
               the command described by cd
     (:search pat cd1 cd2)
               In this command descriptor, pat must be either an atom or
               a true list of atoms and cd1 and cd2 must be command
               descriptors.  We search the interval from cd1 through cd2
               for the first command that matches pat.  Note that if cd1
               occurs chronologically after cd2, the search is
               "backwards" through history while if cd1 occurs
               chronologically before cd2, the search is "forwards".  A
               backwards search will find the most recent match; a
               forward search will find the chronologically earliest
               match.  A command matches pat if either the command form
               itself or one of the events in the block contains pat (or
               all of the atoms in pat if pat is a list).
     (:search pat)
               the command found by (:search pat :max 0), i.e., the most
               recent command matching pat that was part of the user's
               session, not part of the system initialization.

COMPUTED-HINTS    computing advice to the theorem proving process

     General Form of :hints:
     (hint1 hint2 ... hintk)

Each element, hinti, must be either a common hint or a computed hint.

A common hint is of the form

     (goal-spec :key1 val1 ... :keyn valn)

where goal-spec is as specified in goal-spec and each :keyi and vali is
as specified in hints.

A computed hint is either a function symbol, fn, of three, four or seven
arguments or is any term whose only free variables are among ID, CLAUSE,
WORLD, STABLE-UNDER-SIMPLIFICATIONP, HIST, PSPV, and CTX.  The function
symbol case is treated as an abbreviation of the term (fn ID CLAUSE
WORLD), (fn ID CLAUSE WORLD STABLE-UNDER-SIMPLIFICATIONP), or (fn ID
CLAUSE WORLD STABLE-UNDER-SIMPLIFICATIONP HIST PSPV CTX) as appropriate
for the arity of fn.  (Note that this tells you which argument of fn is
which.)  In the discussion below we assume all computed hints are of the
term form.

The evaluation of the term (in a context in which its variables are
bound as described below) should be either nil, indicating that the hint
is not applicable to the clause in question, or else the value is an
alternating list of :keyi vali "pairs."  Except possibly for the first
keyword, the :keyi vali pairs should be as specified in hints.  That is,
those elements of the result should be hint settings as you might have
typed in a common hint.  The first keyword is allowed to be
:COMPUTED-HINT-REPLACEMENT.  Its value should be nil, t, or a list of
terms.  If this keyword is not present, the default value of nil is
provided.

The evaluation of a hint term is done with guard checking turned off
(see SET-GUARD-CHECKING); e.g., the form (car 23) in a computed
hint returns nil as per the axioms.

When a non-nil value is returned, the keyword/value pairs (other than
the optional :COMPUTED-HINT-REPLACEMENT) are used as the hint for the
subgoal in question.  Thus, your job as the programmer of computed hints
is to generate the list of keys and values you would have typed had you
supplied a common hint for the subgoal. (In particular, any theory
expressions in it are evaluated with respect to the global
current-theory, not whatever theory is active at the subgoal in
question.)  If the generated list of keywords and values is illegal, an
error will be signaled and the proof attempt will be aborted.

The purpose of the :COMPUTED-HINT-REPLACEMENT keyword and its value,
chr, is to change the list of hints.  If chr is nil, then the hint which
was applied is removed from the list of hints that is passed down to the
children of the subgoal in question.  This is the default.  If chr is t,
then the hint is left in list of hints.  This means that the same hint
may act on the children of the subgoal.  Otherwise, chr must be a list
of terms, each of which is treated as a computed hint.  The hint which
was applied is deleted from the list of hints and the hints in chr are
added to the list of hints passed to the children of the subgoal.  The
ability to compute new hints and pass them down allows strange and
wonderful behavior.

For these purposes, the goals produced by induction and the top-level
goals of forcing rounds are not considered children; all original hints
are available to them.

After a computed hint is applied to a goal and before the goal is
processed, the remaining applicable computed hints are applied.  For
hint settings, such as :USE, that modify the goal, the effect of more
than one applicable hint just compounds.  But for hint settings, such as
:IN-THEORY that determine the context of the subsequent goal processing,
only the last applicable hint is effective.

It remains only to describe the bindings of the four variables.

Suppose the theorem prover is working on some clause, clause, named by
some goal-spec, e.g., "Subgoal *1/2"'" in some logical world, world.
Corresponding to the printed goal-spec is an internal data structure
called a "clause identifier" id.  See CLAUSE-IDENTIFIER.

In the case of a common hint, the hint applies if the goal-spec of the
hint is the same as the goal-spec of the clause in question.

In the case of a computed hint, the variable ID is bound to the clause
id, the variable CLAUSE is bound to the (translated form of the) clause,
and the variable WORLD is bound to the current ACL2 world.  The variable
STABLE-UNDER-SIMPLIFICATIONP is bound to t or nil.  It is bound to t
only if the clause is known to be stable under simplification.  That is,
the simplifier has been applied to the clause and did not change it.
Such a clause is sometimes known as a "simplification checkpoint."  It
is frequently useful to inject hints (e.g., to enable a rule or provide
a :use hint) only when the goal in question has stabilized.  If a hint
is provided, the processing of the clause starts over with
simplification.

For some instruction about how to use computed hints, see
USING-COMPUTED-HINTS.

CONSTRAINT    restrictions on certain functions introduced in encapsulate events

Suppose that a given theorem, thm, is to be functionally instantiated
using a given functional substitution, alist.  (See
LEMMA-INSTANCE, or for an example, see
FUNCTIONAL-INSTANTIATION-EXAMPLE.)  What is the set of proof
obligations generated?  It is the set obtained by applying alist to all
terms, tm, such that (a) tm mentions some function symbol in the domain
of alist, and (b) either (i) tm arises from the "constraint" on a
function symbol ancestral in thm or in some defaxiom or (ii) tm is the
body of a defaxiom.  Here, a function symbol is "ancestral" in thm if
either it occurs in thm, or it occurs in the definition of some function
symbol that occurs in thm, and so on.

The remainder of this note explains what we mean by "constraint" in the
words above.

In a certain sense, function symbols are introduced in essentially two
ways.  The most common way is to use defun (or when there is mutual
recursion, mutual-recursion or defuns).  There is also a mechanism for
introducing "witness functions"; see DEFCHOOSE.  The
documentation for these events describes the axioms they introduce,
which we will call here their "definitional axioms."  These definitional
axioms are generally the constraints on the function symbols that these
axioms introduce.

However, when a function symbol is introduced in the scope of an
encapsulate event, its constraints may differ from the definitional
axioms introduced for it.  For example, suppose that a function's
definition is local to the encapsulate; that is, suppose the function is
introduced in the signature of the encapsulate.  Then its constraints
include, at the least, those non-local theorems and definitions in the
encapsulate that mention the function symbol.

Actually, it will follow from the discussion below that if the signature
is empty for an encapsulate, then the constraint on each of its new
function symbols is exactly the definitional axiom introduced for it.
Intuitively, we view such encapsulates just as we view include-book
events.  But the general case, where the signature is not empty, is more
complicated.

In the discussion that follows we describe in detail exactly which
constraints are associated with which function symbols that are
introduced in the scope of an encapsulate event.  In order to simplify
the exposition we make two cuts at it.  In the first cut we present an
over-simplified explanation that nevertheless captures the main ideas.
In the second cut we complete our explanation by explaining how we view
certain events as being "lifted" out of the encapsulate, resulting in a
possibly smaller encapsulate, which becomes the target of the algorithm
described in the first cut.

At the end of this note we present an example showing why a more naive
approach is unsound.

Finally, before we start our "first cut," we note that constrained
functions always have guards of T.  This makes sense when one considers
that a constrained function's "guard" only appears in the context of a
local defun, which is skipped.  Note also that any information you want
"exported" outside an encapsulate event must be there as an explicit
definition or theorem.  For example, even if a function foo has output
type (mv t t) in its signature, the system will not know (true-listp
(foo x)) merely on account of this information.  Thus, if you are using
functions like foo (constrained mv functions) in a context where you are
verifying guards, then you should probably provide a :type-prescription
rule for the constrained function, for example, the :type-prescription
rule (true-listp (foo x)).

*First cut at constraint-assigning algorithm.* Quite simply, the
formulas introduced in the scope of an encapsulate are conjoined, and
each function symbol introduced by the encapsulate is assigned that
conjunction as its constraint.

Clearly this is a rather severe algorithm.  Let us consider two possible
optimizations in an informal manner before presenting our second cut.

Consider the (rather artificial) event below.  The function before1 does
not refer at all, even indirectly, to the locally-introduced function
sig-fn, so it is unfortunate to saddle it with constraints about sig-fn.

     (encapsulate
      (((sig-fn *) => *))

      (defun before1 (x)
        (if (consp x)
            (before1 (cdr x))
          x))

      (local (defun sig-fn (x) (cons x x)))

      (defthm sig-fn-prop
        (consp (sig-fn x)))
      )

We would like to imagine moving the definition of before1 to just in
front of this encapsulate, as follows.

     (defun before1 (x)
       (if (consp x)
           (before1 (cdr x))
         x))

     (encapsulate
      (((sig-fn *) => *))

      (local (defun sig-fn (x) (cons x x)))

      (defthm sig-fn-prop
        (consp (sig-fn x)))
      )

Thus, we will only assign the constraint (consp (sig-fn x)), from the
theorem sig-fn-prop, to the function sig-fn, not to the function
before1.

More generally, suppose an event in an encapsulate event does not
mention any function symbol in the signature of the encapsulate, nor any
function symbol that mentions any such function symbol, and so on.  (We
might say that no function symbol from the signature is an "ancestor" of
any function symbol occurring in the event.)  Then we imagine moving the
event, so that it appears in front of the encapsulate.  We don't
actually move it, but we pretend we do when it comes time to assign
constraints.  Thus, such definitions only introduce definitional axioms
as the constraints on the function symbols being defined, and such
theorems introduce no constraints.

Once this first optimization is performed, we have in mind a set of
"constrained functions."  These are the functions introduced in the
encapsulate that would remain after moving some of them out, as
indicated above.  Consider the collection of all formulas introduced by
the encapsulate, except the definitional axioms, that mention these
constrained functions.  So for example, in the event below, no such
formula mentions the function symbol after1.

     (encapsulate
      (((sig-fn *) => *))

      (local (defun sig-fn (x) (cons x x)))

      (defthm sig-fn-prop
        (consp (sig-fn x)))

      (defun after1 (x)
        (sig-fn x))
      )

We can see that there is really no harm in imagining that we move the
definition of after1 out of the encapsulate, to just after the
encapsulate.

Many subtle aspects of this rearrangement process have been omitted.
For example, suppose the function fn uses sig-fn, the latter being a
function in the signature of the encapsulation.  Suppose a formula about
fn is proved in the encapsulation.  Then from the discussion above fn is
among the constrained functions of the encapsulate: it cannot be moved
before the encapsulate and it cannot be moved after the encapsulation.
But why is fn constrained?  The reason is that the theorem proved about
fn may impose or express constraints on sig-fn.  That is, the theorem
proved about fn may depend upon properties of the witness used for
sig-fn.  Here is a simple example:

     (encapsulate
      (((sig-fn *) => *))

      (local (defun sig-fn (x) (declare (ignore x)) 0))

      (defun fn (lst)
        (if (endp lst)
            t
            (and (integerp (sig-fn (car lst)))
                 (fn (cdr lst)))))

      (defthm fn-always-true
        (fn lst)))

In this example, there are no explicit theorems about sig-fn, i.e., no
theorems about it explicitly.  One might therefore conclude that it is
completely unconstrained.  But the witness we chose for it always
returns an integer.  The function fn uses sig-fn and we prove that fn
always returns true.  Of course, the proof of this theorem depends upon
the properties of the witness for sig-fn, even though those properties
were not explicitly "called out" in theorems proved about sig-fn. It
would be unsound to move fn after the encapsulate.  It would also be
unsound to constrain sig-fn to satisfy just fn-always-true without
including in the constraint the relation between sig-fn and fn.  Hence
both sig-fn and fn are constrained by this encapsulation and the
constraint imposed on each is the same and states the relation between
the two as characterized by the equation defining fn as well as the
property that fn always returns true.  Suppose, later, one proved a
theorem about sig-fn and wished to functional instantiate it.  Then one
must also functionally instantiate fn, even if it is not involved in the
theorem, because it is only through fn that sig-fn inherits its
constrained properties.

This is a pathological example that illustrate a trap into which one may
easily fall: rather than identify the key properties of the constrained
function the user has foreshadowed its intended application and
constrained those notions.  Clearly, the user wishing to introduce the
sig-fn above would be well-advised to use the following instead:

     (encapsulate
      (((sig-fn *) => *))
      (local (defun sig-fn (x) (declare (ignore x)) 0))
      (defthm integerp-sig-fn
        (integerp (sig-fn x))))

     (defun fn (lst)
       (if (endp lst)
           t
         (and (integerp (sig-fn (car lst)))
              (fn (cdr lst)))))

     (defthm fn-always-true
        (fn lst)))

Note that sig-fn is constrained merely to be an integer.  It is the only
constrained function.  Now fn is introduced after the encapsulation, as
a simple function that uses sig-fn.  We prove that fn always returns
true, but this fact does not constrain sig-fn.  Future uses of sig-fn do
not have to consider fn at all.

Sometimes it is necessary to introduce a function such as fn within the
encapsulate merely to state the key properties of the undefined function
sig-fn.  But that is unusual and the user should understand that both
functions are being constrained.

Another subtle aspect of encapsulation that has been brushed over so far
has to do with exactly how functions defined within the encapsulation
use the signature functions.  For example, above we say "Consider the
collection of all formulas introduced by the encapsulate, *except the
definitional axioms*, that mention these constrained functions."  We
seem to suggest that a definitional axiom which mentions a constrained
function can be moved out of the encapsulation and considered part of
the "post-encapsulation" extension of the logic, if the defined function
is not used in any non-definitional formula proved in the encapsulation.
For example, in the encapsulation above that constrained sig-fn and
introduced fn within the encapsulation, fn was constrained because we
proved the formula fn-always-true within the encapsulation.  Had we not
proved fn-always-true within the encapsulation, fn could have been moved
after the encapsulation.  But this suggests an unsound rule because
whether such a function can be moved after the encapsulate depend on
whether its *admission* used properties of the witnesses!  In
particular, we say a function is "subversive" if any of its governing
tests or the actuals in any recursive call involve a function in which
the signature functions are ancestral.

Another aspect we have not discussed is what happens to nested
encapsulations when each introduces constrained functions.  We say an
encapsulate event is "trivial" if it introduces no constrained
functions, i.e., if its signatures is nil.  Trivial encapsulations are
just a way to wrap up a collection of events into a single event.

From the foregoing discussion we see we are interested in exactly
how we can "rearrange" the events in a non-trivial encapsulation
-- moving some "before" the encapsulation and others "after" the
encapsulation.  We are also interested in which functions introduced by
the encapsulation are "constrained" and what the "constraints" on each
are.

We may summarize the observations above as follows, after which we
conclude with a more elaborate example.

*Second cut at constraint-assigning algorithm.* First, we focus only on
non-trivial encapsulations that neither contain nor are contained in
non-trivial encapsulations.  (Nested non-trivial encapsulations are not
rearranged at all: do not put anything in such a nest unless you mean
for it to become part of the constraints generated.)  Second, in what
follows we only consider the non-local events of such an encapsulate,
assuming that they satisfy the restriction of using no locally defined
function symbols other than the signature functions.  Given such an
encapsulate event, move, to just in front of it and in the same order,
all definitions and theorems for which none of the signature functions
is ancestral.  Now collect up all formulas (theorems) introduced in the
encapsulate other than definitional axioms.  Add to this set any of
those definitional equations that is either subversive or defines a
function used in a formula in the set.  The conjunction of the resulting
set of formulas is called the "constraint" and the set of all the
signature functions of the encapsulate together with all function
symbols defined in the encapsulate and mentioned in the constraint is
called the "constrained functions."  Assign the constraint to each of
the constrained functions.  Move, to just after the encapsulate, the
definitions of all function symbols defined in the encapsulate that have
been omitted from the constraint.

Implementation note.  In the implementation we do not actually move
events, but we create constraints that pretend that we did.

Here is an example illustrating our constraint-assigning algorithm.  It
builds on the preceding examples.

     (encapsulate
      (((sig-fn *) => *))

      (defun before1 (x)
        (if (consp x)
            (before1 (cdr x))
          x))

      (local (defun sig-fn (x) (cons x x)))

      (defthm sig-fn-prop
        (consp (sig-fn x)))

      (defun during (x)
        (if (consp x)
            x
          (cons (car (sig-fn x))
                17)))

      (defun before2 (x)
        (before1 x))

      (defthm before2-prop
        (atom (before2 x)))

      (defthm during-prop
        (implies (and (atom x)
                      (before2 x))
                 (equal (car (during x))
                        (car (sig-fn x)))))

      (defun after1 (x)
        (sig-fn x))

      (defchoose after2 (x) (u)
        (and (< u x) (during x)))
      )

Only the functions sig-fn and during receive extra constraints.  The
functions before1 and before2 are viewed as moving in front of the
encapsulate, as is the theorem before2-prop.  The functions after1 and
after2 are viewed as being moved past the encapsulate.  Notice that the
formula (consp (during x)) is a conjunct of the constraint.  It comes
from the :type-prescription rule deduced during the definition of the
function during.  The implementation reports the following.

     (SIG-FN X) is axiomatized to return one result.

     In addition, we export AFTER2, AFTER1, DURING-PROP, BEFORE2-PROP, BEFORE2,
     DURING, SIG-FN-PROP and BEFORE1.

     The following constraint is associated with both of the functions DURING
     and SIG-FN:

     (AND (EQUAL (DURING X)
                 (IF (CONSP X)
                     X (CONS (CAR (SIG-FN X)) 17)))
          (CONSP (DURING X))
          (CONSP (SIG-FN X))
          (IMPLIES (AND (ATOM X) (BEFORE2 X))
                   (EQUAL (CAR (DURING X))
                          (CAR (SIG-FN X)))))

We conclude by asking (and to a certain extent, answering) the following
question: Isn't there an approach to assigning constraints that avoids
over-constraining more simply than our "second cut" above?  Perhaps it
seems that given an encapsulate, we should simply assign to each locally
defined function the theorems exported about that function.  If we
adopted that simple approach the events below would be admissible.

     (encapsulate
      (((foo *) => *))
      (local (defun foo (x) x))
      (defun bar (x)
        (foo x))
      (defthm bar-prop
        (equal (bar x) x)
        :rule-classes nil))

     (defthm foo-id
       (equal (foo x) x)
       :hints (("Goal" :use bar-prop)))

     ; The following event is not admissible in ACL2.

     (defthm ouch!
       nil
       :rule-classes nil
       :hints
       (("Goal" :use
         ((:functional-instance foo-id
                                (foo (lambda (x) (cons x x))))))))

Under the simple approach we have in mind, bar is constrained to satisfy
both its definition and bar-prop because bar mentions a function
declared in the signature list of the encapsulation.  In fact, bar is
so-constrained in the ACL2 semantics of encapsulation and the first two
events above (the encapsulate and the consequence that foo must be the
identity function) are actually admissible.  But under the simple
approach to assigning constraints, foo is unconstrained because no
theorem about it is exported.  Under that approach, ouch! is proveable
because foo can be instantiated in foo-id to a function other than the
identity function.

It's tempting to think we can fix this by including definitions, not
just theorems, in constraints.  But consider the following slightly more
elaborate example.  The problem is that we need to include as a
constraint on foo not only the definition of bar, which mentions foo
explicitly, but also abc, which has foo as an ancestor.

     (encapsulate
      (((foo *) => *))
      (local (defun foo (x) x))
      (local (defthm foo-prop
               (equal (foo x) x)))
      (defun bar (x)
        (foo x))
      (defun abc (x)
        (bar x))
      (defthm abc-prop
        (equal (abc x) x)
        :rule-classes nil))

     (defthm foo-id
       (equal (foo x) x)
       :hints (("Goal" :use abc-prop)))

     ; The following event is not admissible in ACL2.

     (defthm ouch!
       nil
       :rule-classes nil
       :hints
       (("Goal" :use
         ((:functional-instance foo-id
                                (foo (lambda (x) (cons x x)))
                                (bar (lambda (x) (cons x x))))))))