Major Section: INTRODUCTION-TO-THE-THEOREM-PROVER

We assume you've read introduction-to-rewrite-rules-part-1, introduction-to-key-checkpoints, and introduction-to-the-database.

You may give the theorem prover a hint that is specific to a particular subgoal generated during a proof attempt. Of course, you learn the name of the subgoal by inspecting the key checkpoints or other proof output. You are not expected to anticipate the need for hints at specific subgoals; instead, you usually deduce that a hint is required because the subgoals is not proved but you see that existing rules and context make it provable.

The most common hint is to enable and/or disable a particular rule on some particular subgoal.

(defthmThe hint above tells the rewriter that just before it begins to work onnameformula:hints (("Subgoal *1/3.2''" :in-theory (disable nth-nthcdr))))

`Subgoal *1/3.2''`

it should switch to a local theory in which all of the
rules generated from the event `nth-nthcdr`

are disabled. That local
theory remains the one in use for all descendent subgoals generated from the
one named, until and unless one of those descendent subgoals has an
`:in-theory`

hint associated with it. There are many kinds of hints
besides `:in-theory`

and in general, after each subgoal name, you can give
various forms of advice and list various adjustments you wish to make to the
context in which the prover is operating when it begins addressing the subgoal
named.
The top-level goal is always named `Goal`

. Thus
(defthmhas the effect of usingnameformula:hints (("Goal" ...hints1...) ("Subgoal *1/3.2''" ...hints2...)))

`Subgoal *1/3.2''`

and
its children, where There are a few hints which ``take effect'' exactly on the subgoal to which they are attached and are not inherited by their descendents.

Here is an incomplete list of some of the more common hints; we note the ones that do not pass on their effects to their descendents. We recommend that you not follow the advanced links (marked ``'') below until you have read the entire tutorial.

See in-theory for how to enable and/or disable rules. The new theory is
computed by a ``theory expression'' (see theories ) such as
`(disable nth-nthcdr)`

and typically makes adjustments such as additions
or deletions to the global current theory. All the relevant new theories
are computed before the proof begins. Thus, in

(defthmthe theory mentioned fornameformula:hints (("Goal" :in-theory (disable rule1)) ("Subgoal *1/3.2''" (disable rule2))))

`Goal`

is the global current theory minus `rule1`

,
while the theory mentioned for its descendent, `Subgoal *1/3.2''`

, is the global
current theory minus `rule2`

. In particular, if both `rule1`

and `rule2`

are
enabled in the global current theory, then `rule1`

is enabled during the
processing of `Subgoal *1/3.2''`

because it was not removed explicitly there.
See use for how to force the theorem prover to take note of
particular instances of particular theorems; in particular, the instances
are created and added as hypotheses to the subgoal in question. The hint is
not inherited by the descendents of the subgoal
(since the formula being proved has been modified by the hint). If the rule
you are using (with a `:use`

hint) is an enabled rewrite rule, it might interfere
with the added hypothesis -- by rewriting itself to `T`

-- and thus often you will
both `:use ...`

and `:in-theory (disable ...)`

.

See expand for how to tell the theorem prover to expand one or more function calls whenever encountered.

See cases for how to force the theorem prover to do a case split to prove the subgoal under each of an exhaustive list of cases given in the hint. This hint takes action specifically at the named subgoal and is not passed down to its children.

See induct for how to tell the theorem prover to go immediately into induction for the subgoal in question, and to use the induction scheme suggested by the hint rather than the one suggested by the terms in the subgoal itself. This hint is not inherited by its descendents.

See hints for a complete list of all hints, and see hints-and-the-waterfall for a more thorough description of how the effects of hints at a subgoal are inherited by the descendents.

If you are reading this as part of the tutorial introduction to the theorem
prover, use your browser's **Back Button** now to return to
introduction-to-the-theorem-prover.