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.

TYPE-SET    how type information is encoded in ACL2

To help you experiment with type-sets we briefly note the following
utility functions.

(type-set-quote x) will return the type-set of the object x.  For
example, (type-set-quote "test") is 2048 and (type-set-quote '(a b c))
is 512.

(type-set 'term nil nil nil nil (ens state) (w state) nil nil nil) will
return the type-set of term.  For example,

     (type-set '(integerp x) nil nil nil nil (ens state) (w state) nil nil nil)

will return (mv 192 nil).  192, otherwise known as *ts-boolean*, is the
type-set containing t and nil.  The second result may be ignored in
these experiments.  Term must be in the translated, internal form shown
by :trans.  See TRANS and see TERM.

(type-set-implied-by-term 'x nil 'term (ens state)(w state) nil) will
return the type-set deduced for the variable symbol x assuming the
translated term, term, true.  The second result may be ignored in these
experiments.  For example,

     (type-set-implied-by-term 'v nil '(integerp v)
                               (ens state) (w state) nil)

returns 11.

(convert-type-set-to-term 'x ts (ens state) (w state) nil) will return
a term whose truth is equivalent to the assertion that the term x has
type-set ts.  The second result may be ignored in these experiments.
For example

     (convert-type-set-to-term 'v 523 (ens state) (w state) nil)

returns a term expressing the claim that v is either an integer or a
non-nil true-list.  523 is the logical-or of 11 (which denotes the
integers) with 512 (which denotes the non-nil true-lists).

The "actual primitive types" of ACL2 are listed in
*actual-primitive-types*, whose elements are shown below.  Each actual
primitive type denotes a set -- sometimes finite and sometimes not --
of ACL2 objects and these sets are pairwise disjoint.  For example,
*ts-zero* denotes the set containing 0 while *ts-positive-integer*
denotes the set containing all of the positive integers.

     *TS-ZERO*                  ;;; {0}
     *TS-POSITIVE-INTEGER*      ;;; positive integers
     *TS-POSITIVE-RATIO*        ;;; positive non-integer rationals
     *TS-NEGATIVE-INTEGER*      ;;; negative integers
     *TS-NEGATIVE-RATIO*        ;;; negative non-integer rationals
     *TS-COMPLEX-RATIONAL*      ;;; complex rationals
     *TS-NIL*                   ;;; {nil}
     *TS-T*                     ;;; {t}
     *TS-NON-T-NON-NIL-SYMBOL*  ;;; symbols other than nil, t
     *TS-PROPER-CONS*           ;;; null-terminated non-empty lists
     *TS-IMPROPER-CONS*         ;;; conses that are not proper
     *TS-STRING*                ;;; strings
     *TS-CHARACTER*             ;;; characters

The actual primitive types were chosen by us to make theorem proving
convenient.  Thus, for example, the actual primitive type *ts-nil*
contains just nil so that we can encode the hypothesis "x is nil" by
saying "x has type *ts-nil*" and the hypothesis "x is non-nil" by
saying "x has type complement of *ts-nil*."  We similarly devote a
primitive type to t, *ts-t*, and to a third type,
*ts-non-t-non-nil-symbol*, to contain all the other ACL2 symbols.

Let *ts-other* denote the set of all Common Lisp objects other than
those in the actual primitive types.  Thus, *ts-other* includes such
things as floating point numbers and CLTL array objects.  The actual
primitive types together with *ts-other* constitute what we call
*universe*.  Note that *universe* is a finite set containing one more
object than there are actual primitive types; that is, here we are
using *universe* to mean the finite set of primitive types, not the
infinite set of all objects in all of those primitive types.
*Universe* is a partitioning of the set of all Common Lisp objects:
every object belongs to exactly one of the sets in *universe*.

Abstractly, a "type-set" is a subset of *universe*.  To say that a
term, x, "has type-set ts" means that under all possible assignments to
the variables in x, the value of x is a member of some member of ts.
Thus, (cons x y) has type-set {*ts-proper-cons* *ts-improper-cons*}.  A
term can have more than one type-set.  For example, (cons x y) also has
the type-set {*ts-proper-cons* *ts-improper-cons* *ts-nil*}.
Extraneous types can be added to a type-set without invalidating the
claim that a term "has" that type-set.  Generally we are interested in
the smallest type-set a term has, but because the entire theorem-proving
problem for ACL2 can be encoded as a type-set question, namely, "Does p
have type-set complement of *ts-nil*?," finding the smallest type-set
for a term is an undecidable problem.  When we speak informally of
"the" type-set we generally mean "the type-set found by our heuristics"
or "the type-set assumed in the current context."

Note that if a type-set, ts, does not contain *ts-other* as an element
then it is just a subset of the actual primitive types.  If it does
contain *ts-other* it can be obtained by subtracting from *universe*
the complement of ts.  Thus, every type-set can be written as a
(possibly complemented) subset of the actual primitive types.

By assigning a unique bit position to each actual primitive type we can
encode every subset, s, of the actual primitive types by the
nonnegative integer whose ith bit is on precisely if s contains the ith
actual primitive type.  The type-sets written as the complement of s
are encoded as the twos-complement of the encoding of s.  Those
type-sets are thus negative integers.  The bit positions assigned to
the actual primitive types are enumerated from 0 in the same order as
the types are listed in *actual-primitive-types*.  At the concrete
level, a type-set is an integer between *min-type-set* and
*max-type-set*, inclusive.

For example, *ts-nil* has bit position 6.  The type-set containing just
*ts-nil* is thus represented by 64.  If a term has type-set 64 then the
term is always equal to nil.  The type-set containing everything but
*ts-nil* is the twos-complement of 64, which is -65.  If a term has
type-set -65, it is never equal to nil.  By "always" and "never" we
mean under all, or under no, assignments to the variables, respectively.

Here is a more complicated example.  Let s be the type-set containing
all of the symbols and the natural numbers.  The relevant actual
primitive types, their bit positions and their encodings are:

     actual primitive type       bit    value

     *ts-zero*                    0       1
     *ts-positive-integer*        1       2
     *ts-nil*                     6      64
     *ts-t*                       7     128
     *ts-non-t-non-nil-symbol*    8     256

Thus, the type-set s is represented by (+ 1 2 64 128 256) = 451.  The
complement of s, i.e., the set of all objects other than the natural
numbers and the symbols, is -452.

UNTRANSLATE    See USER-DEFINED-FUNCTIONS-TABLE.

USE    hints keyword :USE

See HINTS.

USING-COMPUTED-HINTS    how to use computed hints

Computed hints (see COMPUTED-HINTS) are extraordinarily
powerful.  We show a few examples here to illustrate their use.  We
recommend that the using-computed-hints-n topics be read in the order
using-computed-hints-1, using-computed-hints-2, and so on.

Related topics other than immediate subtopics:

USING-COMPUTED-HINTS-1    Driving Home the Basics

The common hint

     ("Subgoal 3.2.1''" :use lemma42)

has the same effect as the computed hint

     (if (equal id '((0) (3 2 1) . 2))
         '(:use lemma42)
         nil)

which, of course, is equivalent to

     (and (equal id '((0) (3 2 1) . 2))
          '(:use lemma42))

which is also equivalent to the computed hint

     my-special-hint

provided the following defun has first been executed

     (defun my-special-hint (id clause world)
       (declare (xargs :mode :program)
                (ignore clause world))
       (if (equal id '((0) (3 2 1) . 2))
           '(:use lemma42)
           nil))

It is permitted for the defun to be in :LOGIC mode (see
DEFUN-MODE) also.

Just to be concrete, the following three events all behave the same way
(if my-special-hint is as above):

     (defthm main (big-thm a b c)
       :hints (("Subgoal 3.2.1''" :use lemma42)))

     (defthm main (big-thm a b c)
       :hints ((and (equal id '((0) (3 2 1) . 2)) '(:use lemma42))))

     (defthm main (big-thm a b c)
       :hints (my-special-hint))

USING-COMPUTED-HINTS-2    One Hint to Every Top-Level Goal in a Forcing Round

Suppose the main proof completes with a forcing round on three
subgoals, "[1]Subgoal 3", "[1]Subgoal 2", and "[1]Subgoal 1".  Suppose
you wish to :use lemma42 in all top-level goals of the first forcing
round.  This can be done supplying the hint

     (if test '(:use lemma42) nil),

where test is an expression that returns t when ID is one of the clause
ids in question.

         goal-spec     (parse-clause-id goal-spec)

     "[1]Subgoal 3"        ((1) (3) . 0)
     "[1]Subgoal 2"        ((1) (2) . 0)
     "[1]Subgoal 1"        ((1) (1) . 0)

Recall (see CLAUSE-IDENTIFIER) that parse-clause-id maps from a
goal spec to a clause id, so you can use that function on the goal
specs printed in the failed proof attempt to determine the clause ids
in question.

So one acceptable test is

     (member-equal id '(((1) (3) . 0)
                        ((1) (2) . 0)
                        ((1) (1) . 0)))

or you could use parse-clause-id in your computed hint if you don't
want to see clause ids in your script:

     (or (equal id (parse-clause-id "[1]Subgoal 3"))
         (equal id (parse-clause-id "[1]Subgoal 2"))
         (equal id (parse-clause-id "[1]Subgoal 1")))

or you could use the inverse function (see CLAUSE-IDENTIFIER):

     (member-equal (string-for-tilde-@-clause-id-phrase id)
                   '("[1]Subgoal 3"
                     "[1]Subgoal 2"
                     "[1]Subgoal 1"))

Recall that what we've shown above are the tests to use in the computed
hint.  The hint itself is (if test '(:use lemma42) nil) or something
equivalent like (and test '(:use lemma42)).

The three tests above are all equivalent.  They suffer from the problem
of requiring the explicit enumeration of all the goal specs in the
first forcing round.  A change in the script might cause more forced
subgoals and the ones other than those enumerated would not be given
the hint.

You could write a test that recognizes all first round top-level
subgoals no matter how many there are.  Just think of the programming
problem:  how do I recognize all the clause id's of the form ((1) (n) .
0)?  Often you can come to this formulation of the problem by using
parse-clause-id on a few of the candidate goal-specs to see the common
structure.  A suitable test in this case is:

     (and (equal (car id) '(1))     ; forcing round 1, top-level (pre-induction)
          (equal (len (cadr id)) 1) ; Subgoal n (not Subgoal n.i ...)
          (equal (cddr id) 0))      ; no primes

The test above is "overkill" because it recognizes precisely the clause
ids in question.  But recall that once a computed hint is used, it is
(by default) removed from the hints available to the children of the
clause.  Thus, we can widen the set of clause ids recognized to include
all the children without worrying that the hint will be applied to
those children.

In particular, the following test supplies the hint to every top-level
goal of the first forcing round:

     (equal (car id) '(1))

You might worry that it would also supply the hint to the subgoal
produced by the hint - the cases we ruled out by the "overkill" above.
But that doesn't happen since the hint is unavailable to the children.
You could even write:

     (equal (car (car id)) 1)

which would supply the hint to every goal of the form "[1]Subgoal ..."
and again, because we see and fire on the top-level goals first, we
will not fire on, say, "[1]Subgoal *1.3/2", i.e., the id '((1 1 3) (2)
. 0) even though the test recognizes that id.

Finally, the following test supplies the hint to every top-level goal
of every forcing round (except the 0th, which is the "gist" of the
proof, not "really" a forcing round):

     (not (equal (car (car id)) 0))

Recall again that in all the examples above we have exhibited the test
in a computed hint of the form (if test '(:key1 val1 ...) nil).

USING-COMPUTED-HINTS-3    Hints as a Function of the Goal (not its Name)

Sometimes it is desirable to supply a hint whenever a certain term
arises in a conjecture.  For example, suppose we have proved

     (defthm all-swaps-have-the-property
        (the-property (swap x))
        :rule-classes nil)

and suppose that whenever (SWAP A) occurs in a goal, we wish to add the
additional hypothesis that (THE-PROPERTY (SWAP A)).  Note that this is
equivalent supplying the hint

     (if test
         '(:use (:instance all-swaps-have-the-property (x A)))
         nil)

where test answers the question "does the clause contain (SWAP A)?"
That question can be asked with (occur-lst '(SWAP A) clause).  Briefly,
occur-lst takes the representation of a translated term, x, and a list
of translated terms, y, and determines whether x occurs as a subterm of
any term in y.  (By "subterm" here we mean proper or improper, e.g.,
the subterms of (CAR X) are X and (CAR X).)

Thus, the computed hint:

     (if (occur-lst '(swap a) clause)
         '(:use (:instance all-swaps-have-the-property (x A)))
         nil)

will add the hypothesis (THE-PROPERTY (SWAP A)) to every goal
containing (SWAP A) - except the children of goals to which the
hypothesis was added.

A COMMON MISTAKE users are likely to make is to forget that they are
dealing with translated terms.  For example, suppose we wished to look
for (SWAP (LIST 1 A)) with occur-lst.  We would never find it with

     (occur-lst '(SWAP (LIST 1 A)) clause)

because that presentation of the term contains macros and other
abbreviations.  By using :trans (see TRANS) we can obtain the
translation of the target term.  Then we can look for it with:

     (occur-lst '(SWAP (CONS '1 (CONS A 'NIL))) clause)

Note in particular that you must

     * eliminate all macros and
     * explicitly quote all constants.

We recommend using :trans to obtain the translated form of the terms in
which you are interested, before programming your hints.

An alternative is to use the expression (prettyify-clause clause nil
nil) in your hint to convert the current goal clause into the
s-expression that is actually printed.  For example, the clause

     ((NOT (CONSP X)) (SYMBOLP Y) (EQUAL (CONS '1 (CAR X)) Y))

"prettyifies" to

     (IMPLIES (AND (CONSP X)
                   (NOT (SYMBOLP Y)))
              (EQUAL (CONS 1 (CAR X)) Y))

which is what you would see printed by ACL2 when the goal clause is
that shown.

However, if you choose to convert your clauses to prettyified form, you
will have to write your own explorers (like our occur-lst), because all
of the ACL2 term processing utilities work on translated and/or clausal
forms.  This should not be taken as a terrible burden.  You will, at
least, gain the benefit of knowing what you are really looking for,
because your explorers will be looking at exactly the s-expressions you
see at your terminal.  And you won't have to wade through our still
undocumented term/clause utilities.  The approach will slow things down
a little, since you will be paying the price of independently consing
up the prettyified term.

We make one more note on this example.  We said above that the computed
hint:

     (if (occur-lst '(swap a) clause)
         '(:use (:instance all-swaps-have-the-property (x A)))
         nil)

will add the hypothesis (THE-PROPERTY (SWAP A)) to every goal
containing (SWAP A) - except the children of goals to which the
hypothesis was added.

It bears noting that the subgoals produced by induction and top-level
forcing round goals are not children.  For example, suppose the hint
above fires on "Subgoal 3" and produces, say, "Subgoal 3'".  Then the
hint will not fire on "Subgoal 3'" even though it (still) contains
(SWAP A) because "Subgoal 3'" is a child of a goal on which the hint
fired.

But now suppose that "Subgoal 3'" is pushed for induction.  Then the
goals created by that induction, i.e., the base case and induction
step, are not considered children of "Subgoal 3'".  All of the original
hints are available.

Alternatively, suppose that "Subgoal 3' is proved but forces some other
subgoal, "[1]Subgoal 1" which is attacked in Forcing Round 1.  That
top-level forced subgoal is not a child.  All the original hints are
available to it.  Thus, if it contains (SWAP A), the hint will fire and
supply the hypothesis, producing "[1]Subgoal 1'".  This may be
unnecessary, as the hypothesis might already be present in "[1]Subgoal
1".  In this case, no harm is done.  The hint won't fire on "[1]Subgoal
1" because it is a child of "[1]Subgoal 1" and the hint fired on that.

USING-COMPUTED-HINTS-4    Computing the Hints

So far we have used computed hints only to compute when a fixed set of
keys and values are to be used as a hint.  But computed hints can, of
course, compute the set of keys and values.  You might, for example,
write a hint that recognizes when a clause "ought" to be provable by a
:BDD hint and generate the appropriate hint.  You might build in a set
of useful lemmas and check to see if the clause is provable :BY one of
them.  You can keep all function symbols disabled and use computed
hints to compute which ones you want to :EXPAND.  In general, you can
write a theorem prover for use in your hints, provided you can get it
do its job by directing our theorem prover.

Suppose for example we wish to find every occurrence of an instance of
(SWAP x) and provide the corresponding instance of
ALL-SWAPS-HAVE-THE-PROPERTY.  Obviously, we must explore the clause
looking for instances of (SWAP x) and build the appropriate instances
of the lemma.  We could do this in many different ways, but below we
show a general purpose set of utilities for doing it.  The functions
are not defined in ACL2 but could be defined as shown.

Our plan is:  (1) Find all instances of a given pattern (term) in a
clause, obtaining a set of substitutions.  (2) Build a set of :instance
expressions for a given lemma name and set of substitutions.  (3)
Generate a :use hint for those instances when instances are found.

The pair of functions below find all instances of a given pattern term
in either a term or a list of terms.  The functions each return a list
of substitutions, each substitution accounting for one of the matches
of pat to a subterm.  At this level in ACL2 substitutions are lists of
pairs of the form (var . term).  All terms mentioned here are presumed
to be in translated form.

The functions take as their third argument a list of substitutions
accumulated to date and add to it the substitutions produced by
matching pat to the subterms of the term.  We intend this accumulator
to be nil initially.  If the returned value is nil, then no instances
of pat occurred.

     (mutual-recursion

     (defun find-all-instances (pat term alists)
      (declare (xargs :mode :program))
      (mv-let
       (instancep alist)
       (one-way-unify pat term)
       (let ((alists (if instancep (add-to-set-equal alist alists) alists)))
         (cond
          ((variablep term) alists)
          ((fquotep term) alists)
          ((flambdap (ffn-symb term))
           (find-all-instances pat
                               (lambda-body (ffn-symb term))
                               (find-all-instances-list pat (fargs term) alists)))
          (t (find-all-instances-list pat (fargs term) alists))))))

     (defun find-all-instances-list (pat list-of-terms alists)
      (declare (xargs :mode :program))
      (cond
       ((null list-of-terms) alists)
       (t (find-all-instances pat
                              (car list-of-terms)
                              (find-all-instances-list pat
                                                       (cdr list-of-terms)
                                                       alists))))))

We now turn our attention to converting a list of substitutions into a
list of lemma instances, each of the form

     (:INSTANCE name (var1 term1) ... (vark termk))

as written in :use hints.  In the code shown above, substitutions are
lists of pairs of the form (var . term), but in lemma instances we must
write "doublets."  So here we show how to convert from one to the other:

     (defun pairs-to-doublets (alist)
       (declare (xargs :mode :program))
       (cond ((null alist) nil)
             (t (cons (list (caar alist) (cdar alist))
                      (pairs-to-doublets (cdr alist))))))

Now we can make a list of lemma instances:

     (defun make-lemma-instances (name alists)
       (declare (xargs :mode :program))
       (cond
        ((null alists) nil)
        (t (cons (list* :instance name (pairs-to-doublets (car alists)))
                 (make-lemma-instances name (cdr alists))))))

Finally, we can package it all together into a hint function.  The
function takes a pattern, pat, which must be a translated term, the
name of a lemma, name, and a clause.  If some instances of pat occur in
clause, then the corresponding instances of name are :USEd in the
computed hint.  Otherwise, the hint does not apply.

     (defun add-corresponding-instances (pat name clause)
       (declare (xargs :mode :program))
       (let ((alists (find-all-instances-list pat clause nil)))
         (cond
          ((null alists) nil)
          (t (list :use (make-lemma-instances name alists))))))

The design of this particular hint function makes it important that the
variables of the pattern be the variables of the named lemma and that
all of the variables we wish to instantiate occur in the pattern.  We
could, of course, redesign it to allow "free variables" or some sort of
renaming.

We could now use this hint as shown below:

     (defthm ... ...
       :hints ((add-corresponding-instances
                '(SWAP x)
                'ALL-SWAPS-HAVE-THE-PROPERTY
                clause)))

The effect of the hint above is that any time a clause arises in which
any instance of (SWAP x) appears, we add the corresponding instance of
ALL-SWAPS-HAVE-THE-PROPERTY.  So for example, if Subgoal *1/3.5
contains the subterm (SWAP (SWAP A)) then this hint fires and makes the
system behave as though the hint:

     ("Subgoal *1/3.5"
      :USE ((:INSTANCE ALL-SWAPS-HAVE-THE-PROPERTY (X A))
            (:INSTANCE ALL-SWAPS-HAVE-THE-PROPERTY (X (SWAP A)))))

had been present.

USING-COMPUTED-HINTS-5    Debugging Computed Hints

We have found that it is sometimes helpful to define hints so that they
print out messages to the terminal when they fire, so you can see what
hint was generated and which of your computed hints did it.

To that end we have defined a macro we sometimes use.  Suppose you have
a :hints specification such as:

     :hints (computed-hint-fn (hint-expr id))

If you defmacro the macro below you could then write instead:

     :hints ((show-hint computed-hint-fn 1)
             (show-hint (hint-expr id) 2))

with the effect that whenever either hint is fired (i.e., returns
non-nil), a message identifying the hint by the marker (1 or 2, above)
and the non-nil value is printed.

     (defmacro show-hint (hint &optional marker)
       (cond
        ((and (consp hint)
              (stringp (car hint)))
         hint)
        (t
         `(let ((marker ,marker)
                (ans ,(if (symbolp hint)
                          `(,hint id clause world stable-under-simplificationp)
                        hint)))
            (if ans
                (prog2$
                 (cw "~%***** Computed Hint~#0~[~/ (from hint ~x1)~]~%~x2~%~%"
                     (if (null marker) 0 1)
                     marker
                     (cons (string-for-tilde-@-clause-id-phrase id)
                           ans))
                 ans)
              nil)))))

Note that when show-hint is applied to a hint that is a symbol, e.g.,
computed-hint-fn, it applies the symbol to the four computed-hint
arguments: id, clause, world, and stable-under-simplificationp.  If
computed-hint-fn is of arity 3 the code above would cause an error.
One way to avoid it is to write

     :hints ((show-hints (computed-hint-fn id clause world) 1)
             (show-hint (hint-expr id) 2)).

If you only use computed hints of arity 3, you might eliminate the
occurrence of stable-under-simplificationp in the definition of
show-hint above.

Putting a show-hint around a common hint has no effect.  If you find
yourself using this utility let us know and we'll consider putting it
into the system itself.  But it does illustrate that you can use
computed hints to do unusual things.

USING-COMPUTED-HINTS-6    Using the computed-hint-replacement feature

So far none of our computed hints have used the
:COMPUTED-HINT-REPLACEMENT feature.  We now illustrate that.

The :computed-hint-replacement feature can easily lead to loops.  So as
you experiment with the examples in this section and your own hints
using this feature, be ready to interrupt the theorem prover and abort!

A non-looping use of the :computed-hint-replacement feature would be a
hint like this:

     (if (certain-terms-present clause)
         '(:computed-hint-replacement t
           :in-theory (enable lemma25))
         '(:computed-hint-replacement t
           :in-theory (disable lemma25)))

In this hint, if certain terms are present in clause, as determined by
the function with the obvious name (here undefined), then this hint
enables lemma25 and otherwise disables it.  Lemma25 might be a very
expensive lemma, e.g., one that matches frequently and has an expensive
and rarely established hypothesis.  One might wish it enabled only
under certain conditions.  Recall that theories are inherited by
children.  So once lemma25 is enabled it "stays" enabled for the
children, until disabled; and vice versa.  If the
:computed-hint-replacement feature were not present and computed hints
were always deleted after they had been used, then lemma25 would be
left enabled (or disabled) for all the childen produced by the first
firing of the hint.  But with the arrangement here, every subgoal gets
a theory deemed suitable by the hint, and the hint persists.

Now we will set up a toy to allow us to play with computed hints to
understand them more deeply.  To follow the discussion it is best to
execute the following events.

     (defstub wrapper (x) t)
     (defaxiom wrapper-axiom (wrapper x) :rule-classes nil)

Now submit the following event and watch what happens.

     (thm (equal u v)
       :hints (`(:use (:instance wrapper-axiom (x a)))))

The theorem prover adds (wrapper a) to the goal and then abandons the
proof attempt because it cannot prove the subgoal.  Since the computed
hint is deleted upon use, the hint is not applied to the subgoal (i.e.,
the child of the goal).

What happens if we do the following?

     (thm (equal u v)
       :hints (`(:computed-hint-replacement t
                 :use (:instance wrapper-axiom (x a)))))

As one might expect, this loops forever: The hint is applied to the
child and adds the hypothesis again.  When the hint fires, nothing is
actually changed, since (wrapper a) is already in the subgoal.

So let's change the experiment a little.  Let's make the hint add the
hypothesis (wrapper p) where p is the first literal of the clause.
This is silly but it allows us to explore the behavior of computed
hints a little more.

     (thm (equal u v)
       :hints (`(:use (:instance wrapper-axiom (x ,(car clause))))))

So in this case, the theorem prover changes the goal to

     (IMPLIES (WRAPPER (EQUAL U V)) (EQUAL U V))

which then simplifies to

     (IMPLIES (WRAPPER NIL) (EQUAL U V))

because the concluding equality can be assumed false in the hypothesis
(e.g., think of the contrapositive version).  Nothing else happens
because the hint has been removed and so is not applicable to the child.

Now consider the following - and be ready to interrupt it and abort!

     (thm (equal u v)
       :hints (`(:computed-hint-replacement t
                 :use (:instance wrapper-axiom (x ,(car clause))))))

This time the hint is not removed and so is applied to the child.  So
from Goal we get

     Goal'
     (IMPLIES (WRAPPER (EQUAL U V))
              (EQUAL U V))

and then

     Goal''
     (IMPLIES (AND (WRAPPER (NOT (WRAPPER (EQUAL U V))))
                   (WRAPPER (EQUAL U V)))
              (EQUAL U V))

etc.

First, note that the hint is repeatedly applied to its children.  That
is because we wrote :computed-hint-replacement t.  But second, note
that Goal' is not even being simplified before Goal" is produced from
it.  If it were being simplified, the (equal u v)'s in the hypotheses
would be replaced by nil.  This is a feature.  It means after a
computed hint has fired, other hints are given a chance at the result,
even the hint itself unless it is removed from the list of hints.

As an exercise, let's arrange for the hint to stay around and be
applied indefinitely but with a simplification between each use of the
the hint.  To do this we need to pass information from one application
of the hint to the next, essentially to say "stay around but don't
fire."

First, we will define a function to use in the hint.  This is more than
a mere convenience; it allows the hint to "reproduce itself" in the
replacement.

     (defun wrapper-challenge (clause parity)
       (if parity
           `(:computed-hint-replacement ((wrapper-challenge clause nil))
             :use (:instance wrapper-axiom (x ,(car clause))))
           `(:computed-hint-replacement ((wrapper-challenge clause t)))))

Note that this function is not recursive, even though it uses its own
name.  That is because the occurrence of its name is in a quoted
constant.

Now consider the following.  What will it do?

     (thm (equal u v)
       :hints ((wrapper-challenge clause t)))

First, observe that this is a legal hint because it is a term that
mentions only the free variable CLAUSE.  When defining hint functions
you may sometimes think their only arguments are the four variables id,
clause, world, and stable-under-simplificationp.  That is not so.  But
in your hints you must call those functions so that those are the only
free variables.  Note also that the occurrence of clause inside the
:computed-hint-replacement is not an occurrence of the variable clause
but just a constant.  Just store this note away for a moment.  We'll
return to it momentarily.

Second, the basic cleverness of this hint is that every time it fires
it reproduces itself with the opposite parity.  When the parity is t it
actually changes the goal by adding a hypothesis.  When the parity is
nil it doesn't change the goal and so allows simplification to proceed
- but it swaps the parity back to t.  What you can see with this simple
toy is that we can use the computed hints to pass information from
parent to child.

Ok, so what happens when the event above is executed?  Try it.  You will
see that ACL2 applied the hint the first time.  It doesn't get around to
printing the output because an error is caused before it can print.
But here is a blow-by-blow description of what happens.  The hint is
evaluated on Goal with the clause ((equal u v)).  It produces a hint
exactly as though we had typed:

     ("Goal" :use (:instance wrapper-axiom (x (equal u v))))

which is applied to this goal. In addition, it produces the new hints
argument

     :hints ((wrapper-challenge clause nil)).

By applying the "Goal" hint we get the new subgoal

     Goal'
     (implies (wrapper (equal u v))
              (equal u v))

but this is not printed because, before printing it, the theorem prover
looks for hints to apply to it and finds

     (wrapper-challenge clause nil)

That is evaluated and produces a hint exactly as though we had typed:

     ("Goal'" )

and the new hints argument:

     :hints ((wrapper-challenge clause nil)).

But if you supply the hint ("Goal'" ), ACL2 will signal an error
because it does not allow you to specify an empty hint!

So the definition of wrapper-challenge above is almost correct but
fatally flawed.  We need a non-empty "no-op" hint.  One such hint is to
tell the system to expand a term that will always be expanded anyway.
So undo wrapper-challenge, redefine it, and try the proof again.  Now
remember the observation about clause that we asked you to "store"
above.  The new definition of wrapper-challenge illustrates what we
meant.  Note that the first formal parameter of wrapper-challenge,
below, is no longer named clause but is called cl instead.  But the
"call" of wrapper-challenge in the replacements is on clause.  This may
seem to violate the rule that a function definition cannot use
variables other than the formals.  But the occurrences of clause below
are not variables but constants in an object that will eventually be
treated as hint term.

     :ubt wrapper-challenge

     (defun wrapper-challenge (cl parity)
       (if parity
           `(:computed-hint-replacement ((wrapper-challenge clause nil))
             :use (:instance wrapper-axiom (x ,(car cl))))
           `(:computed-hint-replacement ((wrapper-challenge clause t))
             :expand ((atom zzz)))))

     (thm (equal u v)
       :hints ((wrapper-challenge clause t)))

This time, things go as you might have expected!  Goal' is produced and
simplified, to

     Goal''
     (implies (wrapper nil)
              (equal u v)).

Simplification gets a chance because when the new hint
(wrapper-challenge clause nil) is fired it does not change the goal.
But it does change the parity in the hints argument so that before
Goal" is simplified again, the hint fires and adds the hypothesis:

     Goal'''
     (IMPLIES (AND (WRAPPER (NOT (WRAPPER NIL)))
                   (WRAPPER NIL))
              (EQUAL U V)).

This simplifies, replacing the first (NOT (WRAPPER NIL)) by NIL, since
(WRAPPER NIL) is known to be true here.  Thus the goal simplifies to

     Goal'4'
     (IMPLIES (WRAPPER NIL) (EQUAL U V)).

The process repeats indefinitely.

So we succeeded in getting a hint to fire indefinitely but allow a full
simplification between rounds.

USING-COMPUTED-HINTS-7    Using the stable-under-simplificationp flag

A problem with the example in using-computed-hints-6 is that exactly
one simplification occurs between each (effective) firing of the hint.
Much more commonly we wish to fire a hint once a subgoal has become
stable under simplification.

A classic example of this is when we are dealing with an interpreter
for some state machine.  We typically do not want the "step" function
to open up on the symbolic representation of a state until that state
has been maximally simplified.  We will illustrate with a simple state
machine.

Let us start by defining the step function, stp, and the corresponding
run function that applies it a given number of times.

     (defun stp (s)
       (+ 1 s))

     (defun run (s n)
       (if (zp n)
           s
           (run (stp s) (- n 1))))

The step function here is trivial:  a state is just a number and the
step function increments it.  In this example we will not be interested
in the theorems we prove but in how we prove them.  The formula we will
focus on is

     (thm (equal (run s 7) xxx))

This is not a theorem, of course.  But we want to test our advice on
non-theorems because we do not want the advice to work only for proofs
that succeed.  (In the past, we gave advice about using computed hints
and that advice caused the theorem prover to run forever when given
formulas that it couldn't prove - but most of the time the system is
presented with formulas it cannot prove!)

Furthermore, without some kind of additional rules, the (run s 7)
expression in the conjecture above will not expand at all, because
ACL2's heuristics do not approve.

In fact, we do not want to take chances that run will be expanded - we
want to control its expansion completely.  Therefore, disable run.

     (in-theory (disable run))

Now, what do we want?  (That is always a good question to ask!)  We want
(run s 7) to expand "slowly."  In particular, we want it to expand
once, to (run (stp s) 6).  Then we want the stp to be expanded and
fully simplified before the run expression is expanded again.  That is,
we want to force the expansion of run whenever the goal is stable under
simplification.  This is sometimes called "staged simplification."

We can achieve staged simplification for any given function symbol by
defining the functions shown below and then using a simple computed
hint:

     (thm (equal (run s 7) xxx)
          :hints ((stage run)))

By inspecting how stage is defined you can see how to extend it, but we
explain as we go.  To experiment, you can just paste the definitions
(and defmacro) below into your ACL2 shell and then try the thm command.

First, define this pair of mutually recursive functions.
Find-first-call finds the first call of the function symbol fn in a
given term.

     (mutual-recursion
      (defun find-first-call (fn term)
      ; Find the first call of fn in term.
       (cond ((variablep term) nil)
             ((fquotep term) nil)
             ((equal (ffn-symb term) fn)
              term)
             (t (find-first-call-lst fn (fargs term)))))
      (defun find-first-call-lst (fn lst)
      ; Find the first call of fn in a list of terms.
       (cond ((endp lst) nil)
             (t (or (find-first-call fn (car lst))
                    (find-first-call-lst fn (cdr lst)))))))

We will arrange for the computed hint to generate an :EXPAND hint for
the first call of fn, whenever the goal becomes stable under
simplification.  If no call is found, the hint will do nothing.  To
make sure the hint will not loop indefinitely (for example, by forcing
fn to expand only to have the rewriter "fold" it back up again), we
will provide the hint with a bound that stops it after some number of
iterations.  Here is the basic function that creates the expand hint
and replaces itself to count down.

     (defun stage1 (fn max clause flg)
     ; If the clause is stable under simplification and there is a call of
     ; fn in it, expand it.  But don't do it more than max times.
      (let ((temp (and flg
                       (find-first-call-lst fn clause))))
        (if temp
            (if (zp max)
                (cw "~%~%HINT PROBLEM:  The maximum repetition count of ~
                     your STAGE hint been reached without eliminating ~
                     all of the calls of ~x0.  You could supply a larger ~
                     count with the optional second argument to STAGE ~
                     (which defaults to 100).  But think about what is ~
                     happening! Is each stage permanently eliminating a ~
                     call of ~x0?~%~%"
                    fn)
              `(:computed-hint-replacement
                 ((stage1 ',fn ,(- max 1)
                          clause
                          stable-under-simplificationp))
                :expand (,temp)))
          nil)))

Suppose that when stage1 is called, fn is the function we want to
expand, max is the maximum number of iterations of this expansion,
clause is the current goal clause, and flg is the value of the
stable-under-simplificationp flag.  Then if clause is stable and we can
find a call of fn in it, we ask whether max is exhausted.  If so, we
print an "error message" to the comment window with cw and return nil
(the value of cw).  That nil means the hint does nothing.  But if max
is not yet exhausted, we return a new hint.  As you can see above, the
hint replaces itself with another stage1 hint with the same fn and a
decremented max to be applied to the new clause and the then-current
value of stable-under-simplificationp.  The hint also contains an
:expand directive for the call of fn found.

Thus, if the computed hint was:

     (stage1 'run 5 clause stable-under-simplificationp)

and (run s 7) occurs in the clause, then it will generate

     (:computed-hint-replacement
       ((stage1 'run 4 clause stable-under-simplificationp))
      :expand ((run s 7)))

which will in turn replace the old stage1 hint with the new one and
will apply :expand ((run s 7)) to the current goal.

We can make this more convenient by defining the macro:

     (defmacro stage (fn &optional (max '100))
      `(stage1 ',fn ,max clause stable-under-simplificationp))

Note that the macro allows us to either provide the maximum bound or
let it default to 100.

Henceforth, we can type

     (thm (equal (run s 7) xxx)
          :hints ((stage run)))

to stage the opening of run up to 100 times, or we can write

     (thm (equal (run s 7) xxx)
          :hints ((stage run 5)))

to stage it only 5 times.  In the latter example, the system with print
a "error message" after the fifth expansion.

Note that if we executed

     (set-default-hints '((stage run)))

then we could attack all theorems (involving run) with staged
simplification (up to bound 100), without typing an explicit hint.

     (thm (equal (run s 7) xxx))

Using techniques similar to those above we have implemented "priority
phased simplification" and provided it as a book.  See
books/misc/priorities.lisp.  This is an idea suggested by Pete
Manolios, by which priorities may be assigned to rules and then the
simplifier simplifies each subgoal maximally under the rules of a given
priority before enabling the rules of the next priority level.  The
book above documents both how we implement it with computed hints and
how to use it.

Here is another example of using the stable-under-simplificationp flag
to delay certain actions.  It defines a default hint, see
DEFAULT-HINTS, which will enable non-linear-arithmetic on precisely
those goals which are stable-under-simplificationp.  It also uses the
HISTORY and PSPV variables to determine when toggling
non-linear-arithmetic is appropriate.  These variables are documented
only in the source code.  If you start using these variables
extensively, please contact the developers of ACL2 or Robert Krug
(rkrug@cs.utexas.edu) and let us know how we can help.

     (defun nonlinearp-default-hint (stable-under-simplificationp hist pspv)
       (cond (stable-under-simplificationp
              (if (not (access rewrite-constant
                               (access prove-spec-var pspv :rewrite-constant)
                               :nonlinearp))
                  '(:computed-hint-replacement t
                    :nonlinearp t)
                nil))
             ((access rewrite-constant
                      (access prove-spec-var pspv :rewrite-constant)
                      :nonlinearp)
              (if (not (equal (caar hist) 'SETTLED-DOWN-CLAUSE))
                  '(:computed-hint-replacement t
                    :nonlinearp nil)
                nil))
             (t
              nil)))

USING-COMPUTED-HINTS-8    Some Final Comments

None of the examples show the use of the variable WORLD, which is
allowed in computed hints.  There are some (undocumented) ACL2
utilities that might be useful in programming hints, but these
utilities need access to the ACL2 logical world (see WORLD).

A very useful fact to know is that (table-alist name world) returns an
alist representation of the current value of the table named name.

The ACL2 source code is littered with :program mode functions for
manipulating world.  In our source code, the world is usually bound a
variable named wrld; so searching our code for that name might be
helpful.

Using these utilities to look at the WORLD one can, for example,
determine whether a symbol is defined recursively or not, get the body
and formals of a defined function, or fetch the statement of a given
lemma.  Because these utilities are not yet documented, we do not
expect users to employ WORLD in computed hints.  But experts might and
it might lead to the formulation of a more convenient language for
computed hints.

None of our examples illustrated the 7 argument form of a computed hint,
(fn ID CLAUSE WORLD STABLE-UNDER-SIMPLIFICATIONP HIST PSPV CTX).  When
used, the variables HIST, PSPV, and CTX, are bound to the clause
history, the package of "special variables" governing the clause, and
the "error message context."  These variables are commonly used
throughout our source code but are, unfortunately, undocumented.
Again, we expect a few experts will find them useful in developing
computed hints.

If you start using computed hints extensively, please contact the
developers of ACL2 and let us know what you are doing with them and how
we can help.