This section describes some of the tactics which have been written so far. If you have a copy of the system you should find most, if not all, of the described tactics in the ML files that come with it. Since these files for the most part are fairly well documented, and since the tactic collection is not stable, we limit ourselves here to describing briefly some of the tactics which are particularly useful and which provide an example of what can be done. See the files for the exact names and types of the described tactics.

One of the most tedious parts of reasoning in Nuprl
involves dealing with the
numerous trivial membership subgoals which arise. Looking at the rules,
one can see that many of them have subgoals of the form
` A in Ui`. Also, applying a lemma involves using the

There are several tactics whose function, in part, is to make the
rules easier to use. Most of the primitive rules in Nuprl
\
require arguments. This makes it difficult to chain them together
using the tacticals, so several tactics have been written
which apply an appropriate
member of a class of rules and guess the arguments required.
An example is the * tactic* ` intro`,
which handles all the
introduction steps except product and set intro, where
a ``witness'' term is required, and union intro, where one must decide
which half to prove. These tactics also deal with noncanonical forms.
That is, if a canonical form is expected, as in
the case of an elimination where the hypothesis must be a
canonical type, but a noncanonical form is encountered, as will
often happen if one defines the basic objects of his theory
to be extractions, then the tactic will first
use the direct computation rules to do any necessary reduction
steps.

Since the lemma rule causes the statement of the lemma to be put in the hypothesis list, proving goals whose conclusions are instances of previously proven results would be tedious without tactic support. A particularly useful tactic for this takes a theorem name and tries to match the goal's conclusion with part of the theorem in order to determine the terms with which to instantiate the theorem. If successful, the tactic will produce subgoals corresponding to the antecedents of the implication forming the theorem, the consequent of which was matched against the goal's conclusion.

Finally, we briefly discuss a set of functions which provide
support for implementing term--rewriting tactics. They are slight
modifications of what Paulson has written for
use in LCF [Paulson 83b] and which he used to write
the main tactics in his proof
of the correctness of the unification algorithm [Paulson 84].
The basic idea is to use analogues of the tacticals
` THEN`, ` ORELSE`, etc., as the basis for constructing
larger rewriting tactics from smaller ones. To this end we
define a type of * conversions*:

lettype conv = term -> (term # tactic).Given a term

Thu Sep 14 08:45:18 EDT 1995