Info file: acl2-doc-emacs.info,    -*-Text-*-
produced by `texinfo-format-buffer'
from file `acl2-doc-emacs.texinfo'
using `texinfmt.el' version 2.32 of 19 November 1993.



This is documentation for ACL2 Version 1.8 Copyright (C) 1989-95
Computational Logic, Inc. (CLI).  All rights reserved.





File: acl2-doc-emacs.info, Node: DEFUNS, Next: DISABLE-FORCING, Prev: DEFUN-MODE-CAVEAT, Up: MISCELLANEOUS

DEFUNS    an alternative to mutual-recursion


     Example:
     (DEFUNS
      (evenlp (x)
        (if (consp x) (oddlp (cdr x)) t))
      (oddlp (x)
        (if (consp x) (evenlp (cdr x)) nil)))

     General Form:
     (DEFUNS defuns-tuple1 ... defuns-tuplen)

is equivalent to

     (MUTUAL-RECURSION
       (DEFUN . defuns-tuple1)
       ...
       (DEFUN . defuns-tuplen))

In fact, defuns is the more primitive of the two and mutual-recursion is
just a macro that expands to a call of defun after stripping off the
defun at the car of each argument to mutual-recursion.  We provide and
use mutual-recursion rather than defuns because by leaving the defuns in
place, mutual-recursion forms can be processed by the Emacs tags
program.  See *Note MUTUAL-RECURSION::.



File: acl2-doc-emacs.info, Node: DISABLE-FORCING, Next: DISABLEDP, Prev: DEFUNS, Up: MISCELLANEOUS

DISABLE-FORCING    to disallow forced case splits


     General Form:
     ACL2 !>:disable-forcing   ; disallow forced case splits

See *Note FORCE:: for a discussion of forced case splits.

Disable-forcing is a macro that disables the executable counterpart of
the function symbol force; see *Note FORCE::.  When you want to disable
forcing in hints, use a form such as:

     :in-theory (disable (:executable-counterpart force))





File: acl2-doc-emacs.info, Node: DISABLEDP, Next: E0-ORD-<, Prev: DISABLE-FORCING, Up: MISCELLANEOUS

DISABLEDP    determine whether a given name or rune is disabled


     Examples:

     :disabledp foo   ; returns a list of all disabled runes whose base
                      ; symbol is foo (see *Note RUNE::)
     (disabledp 'foo) ; same as above (i.e., :disabledp foo)
     :disabledp (:rewrite bar . 1) ; returns t if the indicated rune is
                                   ; disabled, else nil
     (disabledp (:rewrite bar . 1)); same as immediately above


Also see *Note PR::, which gives much more information about the rules
associated with a given event.

Disabledp takes one argument, an event name or a rune.  In the former
case it returns the list of disabled runes associated with that name (in
the sense that the rune's "base symbol" is that name; see *Note RUNE::).
In the latter case it returns t if the given rune is disabled, and nil
otherwise.



File: acl2-doc-emacs.info, Node: E0-ORD-<, Next: E0-ORDINALP, Prev: DISABLEDP, Up: MISCELLANEOUS

E0-ORD-<    the well-founded less-than relation on ordinals up to epsilon-0

If x and y are both e0-ordinalps (see *Note E0-ORDINALP::) then
(e0-ord-< x y) is true iff x is strictly less than y.  e0-ord-< is
well-founded on the e0-ordinalps.  When x and y are both nonnegative
integers, e0-ord-< is just the familiar < relation.

e0-ord-< plays a key role in the formal underpinnings of the ACL2 logic.
In order for a recursive definition to be admissible it must be proved
to "terminate."  By terminate we mean that the arguments to the function
"get smaller" as the function recurses and this sense of size comparison
must be such that there is no "infinitely descending" sequence of ever
smaller arguments.  That is, the relation used to compare successive
arguments must be well-founded on the domain being measured.

The most basic way ACL2 provides to prove termination requires the user
to supply (perhaps implicitly) a mapping of the argument tuples into the
ordinals with some "measure" expression in such a way that the measures
of the successive argument tuples produced by recursion decrease
according to the relation e0-ord-<.  The validity of this method rests
on the well-foundedness of e0-ord-< on the e0-ordinalps.

Without loss of generality, suppose the definition in question
introduces the function f, with one formal parameter x (which might be a
list of objects).  Then we require that there exist a measure
expression, (m x), that always produces an e0-ordinalp.  Furthermore,
consider any recursive call, (f (d x)), in the body of the definition.
Let hyps be the conjunction terms (each of which is either the test of
an if in the body or else the negation of such a test) describing the
path through the body to the recursive call in question.  Then it must
be a theorem that

       (IMPLIES hyps (E0-ORD-< (m (d x)) (m x))).

When we say e0-ord-< is "well-founded" on the e0-ordinalps we mean that
there is no infinite sequence of e0-ordinalps such that each is smaller
than its predecessor in the sequence.  Thus, the theorems that must be
proved about f when it is introduced establish that it cannot recur
forever because each time a recursive call is taken (m x) gets smaller.
From this, and the syntactic restrictions on definitions, it can be
shown (as on page 44 in "A Computational Logic", Boyer and Moore,
Academic Press, 1979) that there exists a function satisfying the
definition; intuitively, the value assigned to any given x by the
alleged function is that computed by a sufficiently large machine.
Hence, the logic is consistent if the axiom defining f is added.

See *Note E0-ORDINALP:: for a discussion of the ordinals and how to
compare two ordinals.

The definitional principle permits the use of relations other than
e0-ord-< but they must first be proved to be well-founded on some
domain.  See *Note WELL-FOUNDED-RELATION::.  Roughly put, alternative
relations are shown well-founded by providing an order-preserving
mapping from their domain into the ordinals.  See *Note DEFUN:: for
details on how to specify which well-founded relation is to be used.



File: acl2-doc-emacs.info, Node: E0-ORDINALP, Next: EMBEDDED-EVENT-FORM, Prev: E0-ORD-<, Up: MISCELLANEOUS

E0-ORDINALP    a recognizer for the ordinals up to epsilon-0

Using the nonnegative integers and lists we can represent the ordinals
up to epsilon-0.  The ACL2 notion of ordinal is the same as that found
in nqthm-1992 and both are very similar to the development given in "New
Version of the Consistency Proof for Elementary Number Theory" in The
Collected Papers of Gerhard Gentzen, ed. M.E. Szabo, North-Holland
Publishing Company, Amsterdam, 1969, pp 132-213.

The following essay is intended to provide intuition about ordinals.
The truth, of course, lies simply in the ACL2 definitions of e0-ordinalp
and e0-ord-<.

Very intuitively, think of each non-zero natural number as by being
denoted by a series of the appropriate number of strokes, i.e.,

     0             0
     1             |
     2             ||
     3             |||
     4             ||||
     ...           ...

Then "omega," here written as w, is the ordinal that might be written as

     w             |||||...,

i.e., an infinite number of strokes.  Addition here is just
concatenation.  Observe that adding one to the front of w in the picture
above produces w again, which gives rise to a standard definition of w:
w is the least ordinal such that adding another stroke at the beginning
does not change the ordinal.

We denote by w+w or w*2 the "doubly infinite" sequence that we might
write as follows.

     w*2           |||||... |||||... 

One way to think of w*2 is that it is obtained by replacing each stroke
in 2 (||) by w.  Thus, one can imagine w*3, w*4, etc., which leads
ultimately to the idea of "w*w," the ordinal obtained by replacing each
stroke in w by w.  This is also written as "omega squared" or w^2, or:

      2
     w             |||||... |||||... |||||... |||||... |||||... ...

We can analogously construct w^3 by replacing each stroke in w by w^2
(which, it turns out, is the same as replacing each stroke in w^2 by w).
That is, we can construct w^3 as w copies of w^2,

      3              2       2       2       2
     w              w  ...  w  ...  w  ...  w ... ...

Then we can construct w^4 as w copies of w^3, w^5 as w copies of w^4,
etc., ultimately suggesting w^w.  We can then stack omegas, i.e.,
(w^w)^w etc.  Consider the "limit" of all of those stacks, which we
might display as follows.

            .         
           .
          .
         w
        w
       w
      w
     w

That is epsilon-0.

Below we begin listing some ordinals up to epsilon-0; the reader can
fill in the gaps at his or her leisure.  We show in the left column the
conventional notation, using w as "omega," and in the right column the
ACL2 object representing the corresponding ordinal.

       ordinal            ACL2 representation

       0                  0
       1                  1
       2                  2
       3                  3
       ...                ...
       w                 '(1 . 0)
       w+1               '(1 . 1)
       w+2               '(1 . 2)
       ...                ...
       w*2               '(1 1 . 0)
       (w*2)+1           '(1 1 . 1)
       ...                ...
       w*3               '(1 1 1 . 0)
       (w*3)+1           '(1 1 1 . 1)
       ...                ...

        2
       w                 '(2 . 0)
       ...                ...

        2
       w +w*4+3          '(2 1 1 1 1 . 3)
       ...                ...

        3
       w                 '(3 . 0)
       ...                ...


        w
       w                 '((1 . 0) . 0)
       ...                ...

        w  99
       w +w  +4w+3       '((1 . 0) 99 1 1 1 1 . 3)
       ...                ...

         2
        w
       w                 '((2 . 0) . 0)

       ...                ...

         w
        w
       w                 '(((1 . 0) . 0) . 0)
       ...                ...

Observe that the sequence of e0-ordinalps starts with the nonnegative
integers.  This is convenient because it means that if a term, such as a
measure expression for justifying a recursive function (see *Note
E0-ORD-<::) must produce an e0-ordinalp it suffices for it to produce a
nonnegative integer.

The ordinals listed above are listed in ascending order.  This is the
ordering tested by e0-ord-<.

The "epsilon-0 ordinals" of ACL2 are recognized by the recursively
defined function e0-ordinalp.  The base case of the recursion tells us
that positive integers are epsilon-0 ordinals.  Otherwise, an epsilon-0
ordinal is a cons pair (o1 . o2), where o1 is a non-0 epsilon-0 ordinal,
o2 is an epsilon-0 ordinal, and if o2 is not an integer then its car
(which, by the foregoing, must be an epsilon-0 ordinal) is no greater
than o1.  Thus, if you think of a (non-integer) epsilon-0 ordinal as a
list, each element is an non-0 epsilon-0 ordinal, the ordinals are
listed in weakly descending order, and the final cdr of the list is an
integer.

The function e0-ord-< compares two epsilon-0 ordinals, x and y.  If both
are integers, e0-ord-< is just x<y.  If one is an integer and the other
is a cons, the integer is the smaller.  Otherwise, the ordinals in their
cars are compared recursively and determines which is smaller unless the
cars are equal, in which case the ordinals in their cdrs are compared.

Fundamental to ACL2 is the fact that e0-ord-< is well-founded on
epsilon-0 ordinals.  That is, there is no "infinitely descending chain"
of such ordinals.  See *Note PROOF-OF-WELL-FOUNDEDNESS::.



File: acl2-doc-emacs.info, Node: EMBEDDED-EVENT-FORM, Next: ENABLE-FORCING, Prev: E0-ORDINALP, Up: MISCELLANEOUS

EMBEDDED-EVENT-FORM    forms that may be embedded in other events


     Examples:
     (defun hd (x) (if (consp x) (car x) 0))
     (local (defthm lemma23 ...))
     (progn (defun fn1 ...)
            (local (defun fn2 ...))
            ...)

     General Form:
     An embedded event form is a term, x, such that

       x is a call of an event function other than DEFPKG (see the
       documentation for `events' for a listing of the event functions);

       x is of the form (LOCAL x1) where x1 is an embedded event form;

       x is of the form (PROGN x1 ... xn), where each xi is an embedded
       event form;

       x is of the form (VALUE &), where & is any term;

       x macroexpands to one of the forms above.

An exception: an embedded event form may not set the acl2-defaults-table
when in the context of local.  Thus for example, the form

     (local (table acl2-defaults-table :defun-mode :program))

is not an embedded event form, nor is the form (local (program)), since
the latter sets the acl2-defaults-table implicitly.  An example at the
end of the discussion below illustrates why there is this restriction.

When an embedded event is executed while ld-skip-proofsp is
'include-book, those parts of it inside local forms are ignored.  Thus,

        (progn (defun f1 () 1)
               (local (defun f2 () 2))
               (defun f3 () 3))

will define f1, f2, and f3 when ld-skip-proofsp is nil but will define
only f1 and f3 when ld-skip-proofsp is 'include-book.

*Discussion:*

Encapsulate and include-book place restrictions on the kinds of forms
that may be processed.  These restrictions insure that the non-local
events (which will ultimately be processed with ld-skip-proofs t) are
indeed admissible provided that the sequence of local and non-local
events is admissible when ld-skip-proofs is nil.

Local permits the hiding of an event or group of events in the sense
that local events are processed when we are trying to establish the
admissibility of a sequence of embedded events but are ignored when we
are constructing the world produced by assuming that sequence.  Thus,
for example, a particularly ugly and inefficient :rewrite rule might be
made local to an encapsulate that "exports" a desirable theorem whose
proof requires the ugly lemma.

To see why we can't allow just anything in as an embedded event,
consider allowing the form

     (if (ld-skip-proofsp state)
         (defun foo () 2)
         (defun foo () 1))

followed by

     (defthm foo-is-1 (equal (foo) 1)).

When we process the events with ld-skip-proofsp, nil the second defun is
executed and the defthm succeeds.  But when we process the events with
ld-skip-proofsp 'include-book, the second defun is executed, so that foo
no longer has the same definition it did when we proved foo-is-1.  Thus,
an invalid formula is assumed when we process the defthm while skipping
proofs.  Thus, the first form above is not a legal embedded event form.

Defpkg is not allowed because it affects how things are read after it is
executed.  But all the forms embedded in an event are read before any
are executed.  That is,

     (encapsulate nil
                  (defpkg "MY-PKG" nil)
                  (defun foo () 'my-pkg::bar))

makes no sense since my-pkg::bar must have been read before the defpkg
for "MY-PKG" was executed.

Finally, let us elaborate on the restriction mentioned earlier related
to the acl2-defaults-table.  Consider the following form.

     (encapsulate
      ()
      (local (program))
      (defun foo (x)
        (if (equal 0 x)
            0
          (1+ (foo (- x))))))

See *Note LOCAL-INCOMPATIBILITY:: for a discussion of how encapsulate
processes event forms.  Briefly, on the first pass through the events
the definition of foo will be accepted in defun mode :program, and hence
accepted.  But on the second pass the form (local (program)) is skipped
because it is marked as local, and hence foo is accepted in defun mode
:logic.  Yet, no proof has been performed in order to admit foo, and in
fact, it is not hard to prove a contradiction from this definition!



File: acl2-doc-emacs.info, Node: ENABLE-FORCING, Next: ENTER-BOOT-STRAP-MODE, Prev: EMBEDDED-EVENT-FORM, Up: MISCELLANEOUS

ENABLE-FORCING    to allow forced case splits


     General Form:
     ACL2 !>:enable-forcing    ; allowed forced case splits

See *Note FORCE:: for a discussion of forced case splits.

Enable-forcing is a macro that enables the executable counterpart of the
function symbol force; see *Note FORCE::.  When you want to enable
forcing in hints, use a form such as:

     :in-theory (enable (:executable-counterpart force))





File: acl2-doc-emacs.info, Node: ENTER-BOOT-STRAP-MODE, Next: ESCAPE-TO-COMMON-LISP, Prev: ENABLE-FORCING, Up: MISCELLANEOUS

ENTER-BOOT-STRAP-MODE    The first millisecond of the Big Bang

ACL2 functions, e.g., if, that show enter-boot-strap-mode as their
defining command are in fact primitives.  It is impossible for the
system to display defining axioms about these symbols.

Enter-boot-strap-mode is a Common Lisp function but not an ACL2
function.  It magically creates from nil an ACL2 property list world
that lets us start the boot-strapping process.  That is, once
enter-boot-strap-mode has created its world, it is possible to process
the defconsts, defuns, and defaxioms, necessary to bring up the rest of
the system.  Before that world is created, the attempt by ACL2 even to
translate a defun form, say, would produce an error because defun is
undefined.

Several ACL2 functions show enter-boot-strap-mode as their defining
command.  Among them are if, cons, car, and cdr.  These functions are
characterized by axioms rather than definitional equations --- axioms
that in most cases are built into our code and hence do not have any
explicit representation among the rules and formulas in the system.



File: acl2-doc-emacs.info, Node: ESCAPE-TO-COMMON-LISP, Next: EVISCERATE-HIDE-TERMS, Prev: ENTER-BOOT-STRAP-MODE, Up: MISCELLANEOUS

ESCAPE-TO-COMMON-LISP    escaping to Common Lisp


     Example:
     ACL2 !>:Q


There is no Common Lisp escape feature in the lp.  This is part of the
price of purity.  To execute a form in Common Lisp as opposed to ACL2,
exit lp with :q, submit the desired forms to the Common Lisp
read-eval-print loop, and reenter ACL2 with (lp).



File: acl2-doc-emacs.info, Node: EVISCERATE-HIDE-TERMS, Next: EXECUTABLE-COUNTERPART, Prev: ESCAPE-TO-COMMON-LISP, Up: MISCELLANEOUS

EVISCERATE-HIDE-TERMS    to print (hide ...) as <hidden>


     Example:
     (assign eviscerate-hide-terms t)
     (assign eviscerate-hide-terms nil)


Eviscerate-hide-terms is a state global variable whose value is either t
or nil.  The variable affects how terms are displayed.  If t, terms of
the form (hide ...) are printed as <hidden>.  Otherwise, they are
printed normally.



File: acl2-doc-emacs.info, Node: EXECUTABLE-COUNTERPART, Next: EXIT-BOOT-STRAP-MODE, Prev: EVISCERATE-HIDE-TERMS, Up: MISCELLANEOUS

EXECUTABLE-COUNTERPART    a rule for computing the value of a function


     Examples:
     (:executable-counterpart length)

which may be abbreviated in theories as

     (length)


Every defun introduces at least two rules used by the theorem prover.
Suppose fn is the name of a defun'd function.  Then (:definition fn) is
the rune (see *Note RUNE::) naming the rule that allows the simplifier
to replace calls of fn by its instantiated body.
(:executable-counterpart fn) is the rune for the rule for how to
evaluate the function on known constants.

When typing theories it is convenient to know that (fn) is a runic
designator that denotes (:executable-counterpart fn).  See *Note
THEORIES::.

If (:executable-counterpart fn) is enabled, then when applications of fn
to known constants are seen by the simplifier they are computed out by
executing the Common Lisp code for fn (with the appropriate handling of
guards).  Suppose fact is defined as the factorial function.  If the
executable counterpart rune of fact, (:executable-counterpart fact), is
enabled when the simplifier encounters (fact 12), then that term will be
"immediately" expanded to 479001600.

Such one-step expansions are sometimes counterproductive because they
prevent the anticipated application of certain lemmas about the
subroutines of the expanded function.  Such computed expansions can be
prevented by disabling the executable counterpart rune of the relevant
function.  For example, if (:executable-counterpart fact) is disabled,
(fact 12) will not be expanded by computation.  In this situation, (fact
12) may be rewritten to (* 12 (fact 11)), using the rule named
(:definition fact), provided the system's heuristics permit the
introduction of the term (fact 11).  Note that lemmas about
multiplication may then be applicable (while such lemmas would be
inapplicable to 479001600).  In many proofs it is desirable to disable
the executable counterpart runes of certain functions to prevent their
expansion by computation.  See *Note EXECUTABLE-COUNTERPART-THEORY::.

Finally: What do we do about functions that are "constrained" rather
than defined, such as the following?  (See *Note ENCAPSULATE::.)

     (encapsulate ((foo (x) t))
                  (local (defun foo (x) x)))

Does foo have an executable counterpart?  Yes: since the vast majority
of functions have sensible executable counterparts, it was decided that
*all* functions, even such "constrained" ones, have executable
counterparts.  We essentially "trap" when such calls are inappropriate.
Thus, consider for example:

     (defun bar (x)
       (if (rationalp x)
           (+ x 1)
         (foo x)))

If the term (bar '3) is encountered by the ACL2 rewriter during a proof,
and if the :executable-counterpart of bar is enabled, then it will be
invoked to reduce this term to '4.  However, if the term (bar 'a) is
encountered during a proof, then since 'a is not a rationalp and since
the :executable-counterpart of foo is only a "trap," then this call of
the :executable-counterpart of bar will result in a "trap." In that
case, the rewriter will return the term (hide (bar 'a)) so that it never
has to go through this process again.  See *Note HIDE::.



File: acl2-doc-emacs.info, Node: EXIT-BOOT-STRAP-MODE, Next: FAILED-FORCING, Prev: EXECUTABLE-COUNTERPART, Up: MISCELLANEOUS

EXIT-BOOT-STRAP-MODE    the end of pre-history

Exit-boot-strap-mode is the last step in creating the ACL2 world in
which the user lives.  It has command number 0.  Commands before it are
part of the system initialization and extend all the way back to :min.
Commands after it are those of the user.

Exit-boot-strap-mode is a Common Lisp function but not an ACL2 function.
It is called when every defconst, defun, etc., in our source code has
been processed under ACL2 and the world is all but complete.
exit-boot-strap-mode has only one job: to signal the completion of the
boot-strapping.



File: acl2-doc-emacs.info, Node: FAILED-FORCING, Next: FAILURE, Prev: EXIT-BOOT-STRAP-MODE, Up: MISCELLANEOUS

FAILED-FORCING    how to deal with a proof failure in a forcing round

See *Note FORCING-ROUND:: for a background discussion of the notion of
forcing rounds.  When a proof fails during a forcing round it means that
the "gist" of the proof succeeded but some "technical detail" failed.
The first question you must ask yourself is whether the forced goals are
indeed theorems.  We discuss the possibilities below.

If you believe the forced goals are theorems, you should follow the
usual methodology for "fixing" failed ACL2 proofs, e.g., the
identification of key lemmas and their timely and proper use as rules.
See *Note FAILURE:: and see *Note PROOF-TREE::.

The rules designed for the goals of forcing rounds are often just what
is needed to prove the forced hypothesis at the time it is forced.
Thus, you may find that when the system has been "taught" how to prove
the goals of the forcing round no forcing round is needed.  This is
intended as a feature to help structure the discovery of the necessary
rules.

If a hint must be provided to prove a goal in a forcing round, the
appropriate "goal specifier" (the string used to identify the goal to
which the hint is to be applied) is just the text printed on the line
above the formula, e.g., "[1]Subgoal *1/3"".  See *Note GOAL-SPEC::.

If you solve a forcing problem by giving explicit hints for the goals of
forcing rounds, you might consider whether you could avoid forcing the
assumption in the first place by giving those hints in the appropriate
places of the main proof.  This is one reason that we print out the
origins of each forced assumption.  An argument against this style,
however, is that an assumption might be forced in hundreds of places in
the main goal and proved only once in the forcing round, so that by
delaying the proof you actually save time.

We now turn to the possibility that some goal in the forcing round is
not a theorem.

There are two possibilities to consider.  The first is that the original
theorem has insufficient hypotheses to insure that all the forced
hypotheses are in fact always true.  The "fix" in this case is to amend
the original conjecture so that it has adequate hypotheses.

A more difficult situation can arise and that is when the conjecture has
sufficient hypotheses but they are not present in the forcing round
goal.  This can be caused by what we call "premature" forcing.

Because ACL2 rewrites from the inside out, it is possible that it will
force hypotheses while the context is insufficient to establish them.
Consider trying to prove (p x (foo x)).  We first rewrite the formula in
an empty context, i.e., assuming nothing.  Thus, we rewrite (foo x) in
an empty context.  If rewriting (foo x) forces anything, that forced
assumption will have to be proved in an empty context.  This will likely
be impossible.

On the other hand, suppose we did not attack (foo x) until after we had
expanded p.  We might find that the value of its second argument, (foo
x), is relevant only in some cases and in those cases we might be able
to establish the hypotheses forced by (foo x).  Our premature forcing is
thus seen to be a consequence of our "over eager" rewriting.

Here, just for concreteness, is an example you can try.  In this
example, (foo x) rewrites to x but has a forced hypothesis of (rationalp
x).  P does a case split on that very hypothesis and uses its second
argument only when x is known to be rational.  Thus, the hypothesis for
the (foo x) rewrite is satisfied.  On the false branch of its case
split, p simplies to (p1 x) which can be proved under the assumption
that x is not rational.


     (defun p1 (x) (not (rationalp x)))
     (defun p (x y)(if (rationalp x) (equal x y) (p1 x)))
     (defun foo (x) x)
     (defthm foo-rewrite (implies (force (rationalp x)) (equal (foo x) x)))
     (in-theory (disable foo))

The attempt then to do (thm (p x (foo x))) forces the unprovable goal
(rationalp x).

Since all "formulas" are presented to the theorem prover as single terms
with no hypotheses (e.g., since implies is a function), this problem
would occur routinely were it not for the fact that the theorem prover
expands certain "simple" definitions immediately without doing anything
that can cause a hypothesis to be forced.  See *Note SIMPLE::.  This
does not solve the problem, since it is possible to hide the
propositional structure arbitrarily deeply.  For example, one could
define p, above, recursively so that the test that x is rational and the
subsequent first "real" use of y occurred arbitrarily deeply.

Therefore, the problem remains: what do you do if an impossible goal is
forced and yet you know that the original conjecture was adequately
protected by hypotheses?

One alternative is to disable forcing entirely.  See *Note
DISABLE-FORCING::.  Another is to disable the rule that caused the
force.

A third alternative is to prove that the negation of the main goal
implies the forced hypothesis.  For example,

     (defthm not-p-implies-rationalp
       (implies (not (p x (foo x))) (rationalp x))
       :rule-classes nil)

Observe that we make no rules from this formula.  Instead, we merely
:use it in the subgoal where we must establish (rationalp x).

     (thm (p x (foo x))
          :hints (("Goal" :use not-p-implies-rationalp)))

When we said, above, that (p x (foo x)) is first rewritten in an empty
context we were misrepresenting the situation slightly.  When we rewrite
a literal we know what literal we are rewriting and we implicitly assume
it false.  This assumption is "dangerous" in that it can lead us to
simplify our goal to nil and give up -- we have even seen people make
the mistake of assuming the negation of what they wished to prove and
then via a very complicated series of transformations convince
themselves that the formula is false.  Because of this "tail biting" we
make very weak use of the negation of our goal.  But the use we make of
it is sufficient to establish the forced hypothesis above.

A fourth alternative is to weaken your desired theorem so as to make
explicit the required hypotheses, e.g., to prove

     (defthm rationalp-implies-main
       (implies (rationalp x) (p x (foo x)))
       :rule-classes nil)

This of course is unsatisfying because it is not what you originally
intended.  But all is not lost.  You can now prove your main theorem
from this one, letting the implies here provide the necessary case
split.

     (thm (p x (foo x))
          :hints (("Goal" :use rationalp-implies-main)))




File: acl2-doc-emacs.info, Node: FAILURE, Next: FIND-RULES-OF-RUNE, Prev: FAILED-FORCING, Up: MISCELLANEOUS

FAILURE    how to deal with a proof failure

When ACL2 gives up it does not mean that the submitted conjecture is
invalid, even if the last formula ACL2 printed in its proof attempt is
manifestly false.  Since ACL2 sometimes generalizes the goal being
proved, it is possible it adopted an invalid subgoal as a legitimate
(but doomed) strategy for proving a valid goal.  Nevertheless,
conjectures submitted to ACL2 are often invalid and the proof attempt
often leads the careful reader to the realization that a hypothesis has
been omitted or that some special case has been forgotten.  It is good
practice to ask yourself, when you see a proof attempt fail, whether the
conjecture submitted is actually a theorem.

If you think the conjecture is a theorem, then you must figure out from
ACL2's output what you know that ACL2 doesn't about the functions in the
conjecture and how to impart that knowledge to ACL2 in the form of
rules.  Books could be written about this, but they haven't been yet.
However, see *Note PROOF-TREE:: for a utility that may be very helpful
in locating parts of the failed proof that are of particular interest.
See also the discussion of how to read Nqthm proofs and how to use Nqthm
rules in "A Computational Logic Handbook" by Boyer and Moore (Academic
Press, 1988).

If the failure occurred during a forcing round, see *Note
FAILED-FORCING::.



File: acl2-doc-emacs.info, Node: FIND-RULES-OF-RUNE, Next: FORCE, Prev: FAILURE, Up: MISCELLANEOUS

FIND-RULES-OF-RUNE    find the rules named rune


     General Form:
     (find-rules-of-rune rune wrld)


This function finds all the rules in wrld with :rune rune.  It returns a
list of rules in their internal form (generally as described by the
corresponding defrec).  Decyphering these rules is difficult since one
cannot always look at a rule object and decide what kind of record it is
without exploiting many system invariants (e.g., that :rewrite runes
only name rewrite-rules).

At the moment this function returns nil if the rune in question is a
:refinement rune, because there is no object representing :refinement
rules.  (:refinement rules cause changes in the 'coarsenings
properties.)  In addition, if the rune is an :equivalence rune, then
congruence rules with that rune will be returned -- because :equivalence
lemmas generate some congruence rules -- but the fact that a certain
function is now known to be an equivalence relation is not represented
by any rule object and so no such rule is returned.  (The fact that the
function is an equivalence relation is encoded entirely in its presence
as a 'coarsening of equal.)



File: acl2-doc-emacs.info, Node: FORCE, Next: FORCING-ROUND, Prev: FIND-RULES-OF-RUNE, Up: MISCELLANEOUS

FORCE    identity function used to force a case split

When a hypothesis of a conditional rule has the form (force hyp) it is
logically equivalent to hyp but has a pragmatic effect.  In particular,
when the rule is considered, the needed instance of the hypothesis,
hyp', is assumed and a special case is generated, requiring the system
to prove that hyp' is true in the current context.  The proofs of all
such "forced assumptions" are delayed until the successful completion of
the main goal.  See *Note FORCING-ROUND::.

Forcing should only be used on hypotheses that are always expected to be
true, such as the guards of functions.  All the power of the theorem
prover is brought to bear on a forced hypothesis and no backtracking is
possible.  If the :executable-counterpart of the function force is
disabled, then no hypothesis is forced.  See *Note ENABLE-FORCING:: and
see *Note DISABLE-FORCING::.

It sometimes happens that a conditional rule is not applied because some
hypothesis, hyp, could not be relieved, even though the required
instance of hyp, hyp', can be shown true in the context.  This happens
when insufficient resources are brought to bear on hyp' at the time we
try to relieve it.  A sometimes desirable alternative behavior is for
the system to assume hyp', apply the rule, and to generate explicitly a
special case to show that hyp' is true in the context.  This is called
"forcing" hyp.  It can be arranged by restating the rule so that the
offending hypothesis, hyp, is embedded in a call of force, as in (force
hyp).  By using the :corollary field of the rule-classes entry, a
hypothesis can be forced without changing the statement of the theorem
from which the rule is derived.

Technically, force is just a function of one argument that returns that
argument.  It is generally enabled and hence evaporates during
simplification.  But its presence among the hypotheses of a conditional
rule causes case splitting to occur if the hypothesis cannot be
conventionally relieved.

Since a forced hypothesis must be provable whenever the rule is
otherwise applicable, forcing should be used only on hypotheses that are
expected always to be true.  A common situation is when the hypothesis
is in fact a guard (or part of a guard) of some function involved in the
pattern that triggers the rule.  Intuitively, if that pattern term
occurs in the current conjecture, then its guards had better be true,
since otherwise nothing is known about the term.

A particularly common situation in which some hypotheses should be
forced is in "most general" type-prescription lemmas.  If a single lemma
describes the "expected" type of a function, for all "expected"
arguments, then it is probably a good idea to force the hypotheses of
the lemma.  Thus, every time a term involving the function arises, the
term will be given the expected type and its arguments will be required
to be of the expected type.  In applying this advice it might be wise to
avoid forcing those hypotheses that are in fact just type predicates on
the arguments, since the routine that applies type-prescription lemmas
has fairly thorough knowledge of the types of all terms.

Force can have the additional benefit of causing the ACL2 typing
mechanism to interact with the ACL2 rewriter to establish the hypotheses
of type-prescription rules.  To understand this remark, think of the
ACL2 type reasoning system as a rather primitive rule-based theorem
prover for questions about Common Lisp types, e.g., "does this
expression produce a consp?"  "does this expression produce some kind of
ACL2 number, e.g., an integerp, a rationalp, or a complex-rationalp?"
etc.  It is driven by type-prescription rules.  To relieve the
hypotheses of such rules, the type system recursively invokes itself.
This can be done for any hypothesis, whether it is "type-like" or not,
since any proposition, p, can be phrased as the type-like question "does
p produce an object of type nil?"  However, as you might expect, the
type system is not very good at establishing hypotheses that are not
type-like, unless they happen to be assumed explicitly in the context in
which the question is posed, e.g., "If p produces a consp then does p
produce nil?"  If type reasoning alone is insufficient to prove some
instance of a hypothesis, then the instance will not be proved by the
type system and a type-prescription rule with that hypothesis will be
inapplicable in that case.  But by embedding such hypotheses in force
expressions you can effectively cause the type system to "punt" them to
the rest of the theorem prover.  Of course, as already noted, this
should only be done on hypotheses that are "always true."  In
particular, if rewriting is required to establish some hypothesis of a
type-prescription rule, then the rule will be found inapplicable because
the hypothesis will not be established by type reasoning alone.

The ACL2 rewriter uses the type reasoning system as a subsystem.  It is
therefore possible that the type system will force a hypothesis that the
rewriter could establish.  Before a forced hypothesis is reported out of
the rewriter, we try to establish it by rewriting.

This makes the following surprising behavior possible: A
type-prescription rule fails to apply because some true hypothesis is
not being relieved.  The user changes the rule so as to *force* the
hypothesis.  The system then applies the rule but reports no forcing.
How can this happen?  The type system "punted" the forced hypothesis to
the rewriter, which established it.

Finally, we should mention that the rewriter is never willing to force
when there is an if term present in the goal being simplified.  Since
and and or terms are merely abbreviations for if terms, they also
prevent forcing.



File: acl2-doc-emacs.info, Node: FORCING-ROUND, Next: GENERALIZED-BOOLEANS, Prev: FORCE, Up: MISCELLANEOUS

FORCING-ROUND    a section of a proof dealing with forced assumptions

If ACL2 "forces" some hypothesis of some rule to be true, it is obliged
later to prove the hypothesis.  See *Note FORCE::.  ACL2 delays the
consideration of forced hypotheses until the main goal has been proved.
It then undertakes a new round of proofs in which the main goal is
essentially the conjunction of all hypotheses forced in the preceding
proof.  Call this round of proofs the "Forcing Round."  Additional
hypotheses may be forced by the proofs in the Forcing Round.  The
attempt to prove these hypotheses is delayed until the Forcing Round has
been successfully completed.  Then a new Forcing Round is undertaken to
prove the recently forced hypotheses and this continues until no
hypotheses are forced.  Thus, there is a succession of Forcing Rounds.

The Forcing Rounds are enumerated starting from 1.  The Goals and
Subgoals of a Forcing Round are printed with the round's number
displayed in square brackets.  Thus, "[1]Subgoal 1.3" means that the
goal in question is Subgoal 1.3 of the 1st forcing round.  To supply a
hint for use in the proof of that subgoal, you should use the goal
specifier "[1]Subgoal 1.3".  See *Note GOAL-SPEC::.

When a round is successfully completed -- and for these purposes you may
think of the proof of the main goal as being the 0th forcing round --
the system collects all of the assumptions forced by the just-completed
round.  Here, an assumption should be thought of as an implication,
(implies context hyp), where context describes the context in which hyp
was assumed true.  Before undertaking the proofs of these assumptions,
we try to "clean them up" in an effort to reduce the amount of work
required.  This is often possible because the forced assumptions are
generated by the same rule being applied repeatedly in a given context.

For example, suppose the main goal is about some term (pred (xtrans i)
i) and that some rule rewriting pred contains a forced hypothesis that
the first argument is a good-inputp.  Suppose that during the proof of
Subgoal 14 of the main goal, (good-inputp (xtrans i)) is forced in a
context in which i is an integerp and x is a consp.  (Note that x is
irrelevant.)  Suppose finally that during the proof of Subgoal 28,
(good-inputp (xtrans i)) is forced "again," but this time in a context
in which i is a rationalp and x is a symbolp.  Since the forced
hypothesis does not mention x, we deem the contextual information about
x to be irrelevant and discard it from both contexts.  We are then left
with two forced assumptions: (implies (integerp i) (good-inputp (xtrans
i))) from Subgoal 14, and (implies (rationalp i) (good-inputp (xtrans
i))) from Subgoal 28.  Note that if we can prove the assumption required
by Subgoal 28 we can easily get that for Subgoal 14, since the context
of Subgoal 28 is the more general.  Thus, in the next forcing round we
will attempt to prove just

     (implies (rationalp i) (good-inputp (xtrans i)))

and "blame" both Subgoal 14 and Subgoal 28 of the previous round for
causing us to prove this.

By delaying and collecting the forced assumptions until the completion
of the "main goal" we gain two advantages.  First, the user gets
confirmation that the "gist" of the proof is complete and that all that
remains are "technical details."  Second, by delaying the proofs of the
forced assumptions ACL2 can undertake the proof of each assumption only
once, no matter how many times it was forced in the main goal.

In order to indicate which proof steps of the previous round were
responsible for which forced assumptions, we print a sentence explaining
the origins of each newly forced goal.  For example,

     [1]Subgoal 1, below, will focus on
     (GOOD-INPUTP (XTRANS I)),
     which was forced in
      Subgoal 14, above,
       by applying (:REWRITE PRED-CRUNCHER) to
       (PRED (XTRANS I) I),
      and
      Subgoal 28, above,
       by applying (:REWRITE PRED-CRUNCHER) to
       (PRED (XTRANS I) I).


In this entry, "[1]Subgoal 1" is the name of a goal which will be proved
in the next forcing round.  On the next line we display the forced
hypothesis, call it x, which is (good-inputp (xtrans i)) in this
example.  This term will be the conclusion of the new subgoal.  Since
the new subgoal will be printed in its entirety when its proof is
undertaken, we do not here exhibit the context in which x was forced.
The sentence then lists (possibly a succession of) a goal name from the
just-completed round and some step in the proof of that goal that forced
x.  In the example above we see that Subgoals 14 and 28 of the
just-completed proof forced (good-inputp (xtrans i)) by applying
(:rewrite pred-cruncher) to the term (pred (xtrans i) i).

If one were to inspect the theorem prover's description of the proof
steps applied to Subgoals 14 and 28 one would find the word "forced" (or
sometimes "forcibly") occurring in the commentary.  Whenever you see
that word in the output, you know you will get a subsequent forcing
round to deal with the hypotheses forced.  Similarly, if at the
beginning of a forcing round a rune is blamed for causing a force in
some subgoal, inspection of the commentary for that subgoal will reveal
the word "forced" after the rule name blamed.

Most forced hypotheses come from within the prover's simplifier.  When
the simplifier encounters a hypothesis of the form (force hyp) it first
attempts to establish it by rewriting hyp to, say, hyp'.  If the truth
or falsity of hyp' is known, forcing is not required.  Otherwise, the
simplifier actually forces hyp'.  That is, the x mentioned above is
hyp', not hyp, when the forced subgoal was generated by the simplifier.

Once the system has printed out the origins of the newly forced goals,
it proceeds to the next forcing round, where those goals are
individually displayed and attacked.

At the beginning of a forcing round, the enabled structure defaults to
the global enabled structure.  For example, suppose some rune, rune, is
globally enabled.  Suppose in some event you disable the rune at "Goal"
and successfully prove the goal but force "[1]Goal".  Then during the
proof of "[1]Goal", rune is enabled "again."  The right way to think
about this is that the rune is "still" enabled.  That is, it is enabled
globally and each forcing round resumes with the global enabled
structure.



File: acl2-doc-emacs.info, Node: GENERALIZED-BOOLEANS, Next: GOAL-SPEC, Prev: FORCING-ROUND, Up: MISCELLANEOUS

GENERALIZED-BOOLEANS    potential soundness issues related to ACL2 predicates

The discussion below outlines a potential source of unsoundness in ACL2.
Although to our knowledge there is no existing Lisp implementation in
which this problem can arise, nevertheless we feel compelled to explain
this situation.

Consider for example the question: What is the value of (equal 3 3)?
According to the ACL2 axioms, it's t.  And as far as we know, based on
considerable testing, the value is t in every Common Lisp
implementation.  However, according the Common Lisp draft proposed ANSI
standard, any non-nil value could result.  Thus for example, (equal 3 3)
is allowed by the standard to be 17.

The Common Lisp standard specifies (or soon will) that a number of
Common Lisp functions that one might expect to return Boolean values
may, in fact, return arbitrary values.  Examples of such functions are
equal, rationalp, and <; a much more complete list is given below.
Indeed, we dare to say that every Common Lisp function that one may
believe returns only Booleans is, nevertheless, not specified by the
standard to have that property, with the exceptions of the functions not
and null.  The standard refers to such arbitrary values as "generalized
Booleans," but in fact this terminology makes no restriction on those
values.  Rather, it merely specifies that they are to be viewed, in an
informal sense, as being either nil or not nil.

This situation is problematic for ACL2, which axiomatizes these
functions to return Booleans.  The problem is that because (for
efficiency and simplicity) ACL2 makes very direct use of compiled Common
Lisp functions to support the execution of its functions, there is in
principle a potential for unsoundness due to these "generalized
Booleans."  For example, ACL2's equal function is defined to be Common
Lisp's equal.  Hence if in Common Lisp the form (equal 3 3) were to
evaluate to 17, then in ACL2 we could prove (using the
:executable-counterpart of equal) (equal (equal 3 3) 17).  However, ACL2
can also prove (equal (equal x x) t), and these two terms together are
contradictory, since they imply (instantiating x in the second term by
3) that (equal 3 3) is both equal to 17 and to t.

To make matters worse, the standard allows (equal 3 3) to evaluate to
*different* non-nil values every time.  That is: equal need not even be
a function!

Fortunately, no existing Lisp implementation takes advantage of the
flexibility to have (most of) its predicates return generalized
Booleans, as far as we know.  We may implement appropriate safeguards in
future releases of ACL2, in analogy to (indeed, probably extending) the
existing safeguards by way of guards (see *Note GUARD::).  For now,
we'll sleep a bit better knowing that we have been up-front about this
potential problem.

The following list of functions contains all those that are defined in
Common Lisp to return generalized Booleans but are assumed by ACL2 to
return Booleans.  In addition, the functions acl2-numberp and
complex-rationalp are directly defined in terms of respective Common
Lisp functions numberp and complexp.

     /=
     <
     =
     alpha-char-p
     atom
     char-equal
     char<
     char<=
     char>
     char>=
     characterp
     consp
     digit-char-p
     endp
     eq
     eql
     equal
     evenp
     integerp
     keywordp
     listp
     logbitp
     logtest
     lower-case-p
     minusp
     oddp
     plusp
     rationalp
     standard-char-p
     string-equal
     string<
     string<=
     string>
     string>=
     stringp
     subsetp
     symbolp
     upper-case-p
     zerop





File: acl2-doc-emacs.info, Node: GOAL-SPEC, Next: GUARD, Prev: GENERALIZED-BOOLEANS, Up: MISCELLANEOUS

GOAL-SPEC    to indicate where a hint is to be used


     Examples:
     "Goal"
     "goal"
     "Subgoal *1/3""
     "subgoal *1/3""
     "[2]Subgoal *1/3""


When hints are given to the theorem prover, a goal-spec is provided to
specify the goal to which the hints are to be applied.  The hints
provided are carried along innocuously until the named goal arises.
When it arises, the hints are "activated" for that goal and its
descendents.

A legal goal specification may be extracted from the theorem prover's
output.  Certain lines clearly label formulas, as in

     Subgoal *1/3.2'
     (IMPLIES ... ...)

and these lines all give rise to goal specifications.  In general, these
lines all start either with "Goal" or "Subgoal" or else with those words
preceded by a number in square brackets, as in

     [1]Subgoal *1/3.2'
     (IMPLIES ... ...).

A goal specification may be obtained by deleting any surrounding
whitespace from such a line and embedding the text in string quotation
marks.  Thus

     "[1]Subgoal *1/3.2'"

is the goal specifier for the goal above.

As noted, a hint is applied to a goal when the hint's goal specification
matches the name ACL2 assigns to the goal.  The matching algorithm is
case-insensitive.  Thus, alternative goal specifications for the goal
above are "[1]subgoal *1/3.2'" and "[1]SUBGOAL *1/3.2'".  The matching
algorithm does not tolerate non-case discrepancies.  Thus,
"[1]Subgoal*1/3.2'" and " [1]Subgoal *1/3.2'" are unacceptable.

Sometimes a formula is given two names, e.g.,

     Subgoal *1/14.2'
     (IMPLIES ... 
              ...)
     Name the formula above *1.1.

It is the first name (the one that starts with "Goal" or "Subgoal") and
not the second which constitutes a legal goal-spec.  Roughly speaking,
when the system prints the line containing the goal specification, it
activates any hints that are attached to that goal-spec.  Consider the
example above.  Suppose Subgoal *1/14.2' could be proved by using a
certain lemma instance.  Then the appropriate entry in the hints would
be:

     ("Subgoal *1/14.2'" :use ...)

This might surprise you because the system appears to do nothing to
*1/14.2' besides push it for a subsequent induction.  But actually
between the time the system printed the goal-spec line and the time it
decides to push the goal, you can think of the system as trying
everything it has.  So a use hint activated when Subgoal *1/14.2' arises
is just what you want.

But what if you want to give an :induct hint?  By the time induction is
tried, the formula has been given the name *1.1.  Well, this is one you
just have to remember:

     ("Subgoal *1/14.2'" :induct ...).

When the above hint is activated the :induct directive short-circuits
the rest of the processing and sends immediately the formula into the
pool of goals to prove by induction.  The induct hint is attached to the
formula in the pool and when the time comes to turn our attention to
that goal, the induct advice is followed.