This is documentation for ACL2 Version 3.4
Copyright (C) 2008  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.

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

See 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 FAILURE and see 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 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 ensure 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 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
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)))

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.  The "key checkpoint" information printed at the end of the
summary provides a fine place to start.  See THE-METHOD for a
general discussion of how to prove theorems with ACL2.  Also see
SET-GAG-MODE for discussion of key checkpoints and an abbreviated
output mode that focuses attention on them.  You may find it most
useful to start by focusing on key checkpoints that are not under a
proof by induction, if any, both because these are more likely to
suggest useful lemmas and because they are more likely to be theorems;
for example, generalization may have occurred before a proof by
induction has begun.  If you need more information than is provided by
the key checkpoints -- although this should rarely be necessary -- then
you can look at the full proof, perhaps with the aid of certain
utilities: see PROOF-TREE, see SET-GAG-MODE, and see
SET-SAVED-OUTPUT.

For information on a tool to help debug failures of encapsulate and
progn events, see REDO-FLAT.

See also the book "Computer-Aided Reasoning: An Approach" (Kaufmann,
Manolios, Moore), as well as 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
FAILED-FORCING.

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

FORCE    identity function used to force a hypothesis

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 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 ENABLE-FORCING and
see DISABLE-FORCING.  Forced goals can be attacked immediately
(see IMMEDIATE-FORCE-MODEP) or in a subsequent forcing round
(see FORCING-ROUND).  Also see CASE-SPLIT.

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 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 terms and or terms are merely abbreviations for if terms, they also
prevent forcing.  Note that if terms are ultimately eliminated using
the ordinary flow of the proof (but see
SET-CASE-SPLIT-LIMITATIONS), allowing force ultimately to function as
intended.  Moreover, forcing can be disabled, as described above; also
see DISABLE-FORCING.

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

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.

GAG-MODE    verbosity of proof output

Please see SET-GAG-MODE for an explanation of gag-mode, which
can take any of the following values:

     (gag-mode) ; generally evaluates to t, nil, or :goals

GC$    invoke the garbage collector

This function is provided so that the user can call the garbage
collector of the underlying Lisp from inside the ACL2 loop.
Specifically, a call of gc$ is translated into a call of a function
below on the same arguments.

     Allegro CL:            excl:gc
     GCL                    si::gbc
     CLISP                  ext:gc
     CMU Common Lisp        system::gc
     SBCL                   sb-ext:gc
     Macintosh Common Lisp  ccl::gc

The arguments, if any, are as documented in the underlying Common Lisp.
It is up to the user to pass in the right arguments, although we may
do some rudimentary checks.

This function always returns nil.

GCL    tips on building and using ACL2 based on Gnu Common Lisp

See the installation instructions for basic information about building
ACL2 on top of GCL, including information about where to fetch GCL.
Here, we provide some tips that may be useful.

1. You can place forms to evaluate at start-up into file init.lsp in the
directory where you are starting ACL2 (GCL), or into file acl2-init.lsp
in your home directory.  For example, in order to evaluate both of the
lisp forms mentioned in 2 below, you could put them both into init.lsp
in the current directory or in ~/acl2-init.lsp (either way, without
(lp) or :q):

     (setq si::*optimize-maximum-pages* nil)
     (si::allocate 'cons 75000 t)

Note that if you want to put ACL2 patches in this file, you should
precede them with (in-package "ACL2").

2. Suppose you run out of space, for example with an error like this:

        Error: The storage for CONS is exhausted.
          Currently, 59470 pages are allocated.
          Use ALLOCATE to expand the space.

The following suggestion from Camm Maguire will minimize the heap size,
at the cost of more garbage collection time.

     :q   ; exit the ACL2 loop
     (setq si::*optimize-maximum-pages* nil)
     (lp) ; re-enter the ACL2 loop

A second thing to try, suggested by several people, is to preallocate
more pages before the run, e.g.:

     :q   ; exit the ACL2 loop
     (si::allocate 'cons 75000 t)
     (lp) ; re-enter the ACL2 loop

Also see RESET-KILL-RING for a suggestion on how to free up
space.

3. Windows users have seen this error:

     cc1.exe: unrecognized option `-fno-zero-initialized-in-bss'

Camm Maguire suggests that a solution may be to evaluate the following
in GCL before building ACL2.

     (in-package 'compiler)
     (let* ((x `-fno-zero-initialized-in-bss')
            (i (search x *cc*)))
             (setq *cc* (concatenate 'string
                                     (subseq *cc* 0 i)
                                     (subseq *cc* (+ i (length x))))))

4. It is possible to profile using ACL2 built on GCL.  See file
save-gprof.lsp in the ACL2 source directory.

5. Some versions of GCL may have garbage-collector bugs that, on rare
occasions, cause ACL2 (when built on GCL) to break.  If you run into
this, a solution may be to execute the following:

     :q
     (si::sgc-on nil)
     (lp)

Alternatively, put (si::sgc-on nil) in your ~/acl2-init.lsp file.

A full regression test and found that this decreased performance by
about 10%.  But even with that, GCL may be the fastest Common Lisp for
ACL2 on Linux (performance figures may often be found by following the
"Recent changes" link on the ACL2 home page).

6. GCL operations on numbers can sometimes be sped up, perhaps by up to
two orders of magnitude, by suitable declare forms (also see
TYPE-SPEC).  The following example, developed with Warren Hunt and
Serita Nelesen, illustrates the use of such declarations.

     ; File iplus.lisp:
     ; Operations on naturals together with positive infinity (represented as -1).

     ; After (ld "iplus.lisp"), escape to raw Lisp with :q and then eavluate
     ; (disassemble 'big-test).  You should see lots of arithmetic operations
     ; in C code, but no calls of C functions CMPmake_fixnum or number_plus.

     (in-package "ACL2")

     (defmacro i-max ()
       (expt 2 (1- 28)))

     (defmacro i+ (x y)
       `(the (signed-byte 28)
             (let ((x ,x)
                   (y ,y))
               (declare (type (signed-byte 28) x y))
               (cond ((or (< x 0)
                          (< y 0))
                      -1)
                     (t (let ((result
                               (the (signed-byte 29) (+ x y))))
                          (declare (type (signed-byte 29) result))
                          (cond ((>= result (i-max)) -1)
                                (t (the (signed-byte 28) result)))))))))

     (defmacro imin (x y)
       `(the (signed-byte 28)
             (let ((x ,x)
                   (y ,y))
               (declare (type (signed-byte 28) x y))
               (cond ((< x 0)
                      (cond ((< y 0) -1)
                            (t y)))
                     ((< y 0)
                      x)
                     (t
                      (the (signed-byte 28) (min x y)))))))

     (defun big-test (x y z)
       (declare (type (signed-byte 28) x y z))
       (imin (i+ x y)
             (i+ y (imin x z))))

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.

GUARD    restricting the domain of a function

The ACL2 system provides a mechanism for restricting a function
definition to a particular domain.  Although such restrictions, which
are called "guards," are actually ignored by the ACL2 _logic_, they can
be useful as a specification device or as a means of causing the
execution of definitions directly in Common Lisp.  To make such a
restriction, use the :guard xarg to defun.  See XARGS for a
discussion of how to use :guard.  The general issue of guards and guard
verification is discussed in the topics listed below.

Related topics other than immediate subtopics:

To begin further discussion of guards, see GUARD-INTRODUCTION.
That section directs the reader to further sections for more details.
To see just a summary of some commands related to guards, see
GUARD-QUICK-REFERENCE.

EXTRA-INFO    generate markers to indicate sources of guard proof obligations

See GUARD-DEBUG for a discussion of this function, which is
useful for debugging failures during guard verification.

GUARD-DEBUG    generate markers to indicate sources of guard proof obligations

ACL2 guard verification (see GUARD) is often best avoided by
beginning users of ACL2.  When guard verification is employed, it can
generate numerous goals, some of which may not be theorems if the
definition being processed has bugs.  It can be difficult to find such
bugs.  This documentation topic explains a capability provided by ACL2
to help find such bugs.

(Extra-info x y) always returns t by definition.  However, if guard
verification takes place with a non-nil setting of guard-debug (see
below), then the goals generated for guard verification can include
hypotheses that are calls of extra-info.  Typically, such a hypothesis
is of the following form:

     (extra-info '(:guard (:body F))
                 '(G ARG1 ... ARGk))

The above form indicates that the goal in which it occurs was generated
to verify that the guard of the function F is satisfied by the
arguments ARG1 through ARGk, where the term (G ARG1 ... ARGk) occurs in
the body of the function F whose guard verification is in progress.  If
however the above call of G occurs in the guard of F instead of the
body of F, then :body is replaced by :guard above:

     (extra-info '(:guard (:guard F))
                 '(G ARG1 ... ARGk))

If the same proof obligation (goal clause) arises from more than one
occurrence of the same call, then a single goal will be generated,
which has several extra-info hypotheses added to show the multiple
sources of that proof obligation.

All rules (see RUNE) associated with extra-info are disabled by
default, so that hypotheses of the form described above are not
simplified to t.  These hypotheses are intended to ride along for free:
you can generally expect the proof to have the same structure whether
or not the :guard-debug option is supplied, though on rare occasions
the proofs may diverge.

It remains to explain the notion of a guard-debug setting of t, that
is, to explain how to obtain the additional hypotheses described above.
If guards are being verified during processing of a defun event
(whether or not inside a call of mutual-recursion), then one specifies
:guard-debug t in an xargs declaration of a declare form; see
XARGS.  If however the guard verification is on behalf of a
verify-guards call, whether for a definition or a theorem, then one
specifies the keyword argument :guard-debug t.