Conceptually it is convenient to think of tactics
as mappings from proofs
to proofs. The actual implementation of tactics, however, is not quite
that simple. The actual type
of tactics
is
tactic = proof -> proof list # validation,
where proof is the type of (possibly incomplete) proofs and
validation = proof list -> proof.
The idea is that a tactic decomposes a goal proof G into a
finite list of subgoals, 
, and a
validation,
v. The
subgoals are degenerate proofs, i.e., proofs which have only the top--level
sequent filled in and have no refinement rule or subgoals.
We say that a
proof 
achieves
the subgoal 
if the
top--level sequent of 
is the same as the top--level sequent of 
.
The validation, v, takes a list 
,
where each 
achieves 
,
and produces a proof P that achieves G. (Note that wherever we
speak of proof in the context of ML, we mean possibly incomplete proofs.)
Thus a tactic completes some portion of a proof and produces
subgoals that it was unable to prove completely and a
validation that will take any achievement of those subgoals and produce an
achievement of the original goal. If the validation is applied to
achievements 
that are complete proofs, then the result of
the validation is a complete proof of the goal G. In particular, if the
tactic produces an empty list of subgoals then the validation applied to
the empty list produces a complete proof of the goal.
The advantage of this system becomes apparent when one composes tactics. Since a tactic produces an explicit list of subgoals a different (or the same) tactic can easily be applied to each of the subgoals; the tactics thus decompose goals in a top--down manner. This makes it easy to write specialized and modular tactics and to write special tacticals for composing tactics. This system has the disadvantage, however, that it does not easily accommodate a bottom--up style of tactic.
The Nuprl system recognizes two kinds of tactics: refinement tactics and transformation tactics. A refinement tactic operates like a derived rule of inference. Applying a refinement tactic results in the name of the tactic appearing as the refinement rule and any unproved subgoals produced by the tactic appearing as subgoals to the refinement. The following are the actual steps that occur when a refinement tactic is invoked.
The four steps above assume that the tactic terminates without producing an error or throwing a failure that propagates to the top level. If such an event does occur then the error or failure message is reported to the user and the refinement is marked as bad; this behavior exactly mimics the failure of a primitive refinement rule.
Transformation tactics have the effect of mapping proofs to proofs. The result of a transformation tactic is spliced into the proof where the tactic was invoked and takes the place of any previous proof. The following are the steps that occur when a transformation tactic is invoked.
The key difference between refinement and transformation tactics is that transformation tactics are allowed to examine the subproof that is below the current node whereas refinement tactics are not. The result of a transformation tactic will, in general, depend upon the result of the examination. Since most tactics do not depend on the subproof below the designated node, they may be used as either transformation tactics or refinement tactics; in fact, since a refinement tactic cannot examine the subproof, any refinement tactic may be used as a transformation tactic. The main implementation difference between refinement tactics and transformation tactics is how the result of the tactic is used. In the former the actual proof constructed by the tactic is hidden from the user, and only the remaining unproved subgoals are displayed. In the latter the result is explicitly placed in the proof.