A few examples should give enough of the flavor of tactic writing in the Nuprl context to permit the reader to build substantial tactics of his own. Our first example is a very simple one which encodes a frequently used pattern of reasoning, namely, case analysis. When called as a refinement tactic with an argument which is a union type (i.e., of the form A|B) cases will do a seq with its argument and then do an elim on the copy of the term which appears in the hypothesis list of the second subgoal. The effect is essentially to implement a derived rule of the form
>> T by cases 'A|B'
>> A | B
A >> T
B >> T
except that any of the subgoals which the auto--tactic manages
to prove will not appear.
(Note the use of the quotes to make text into an ML
term.)
The following is the implementation of the tactic.
let cases union_term =
refine (seq [union_term] [`nil`])
THENL
[IDTAC
;\pf.
refine (union_elim (length (hypotheses pf)) `nil` `nil`)
pf
]
THEN
TRY (COMPLETE immediate)
;;
The first refine above will do the seq rule;
the `nil` argument means that the new hypothesis in the
second subgoal generated will not have a tag. The two members of
the list following the THENL are what will be applied to the
two subgoals resulting from the seq. The first one
simply leaves alone the introduced union term, and the
second does the elimination. The only complication is that
the rule constructor union_elim requires the number of the
hypothesis to be eliminated as an argument; in this case it is the last one,
so the length of the current hypothesis list is the required
number.
Since the length of the actual proof to which refine is
applied is necessary, the second tactic in the list of tactics is actually
a lambda term.
Recall that the type of tactics is proof->proof list # validation.
Therefore, if X is a piece of ML
code which uses
an identifier pf and which is of type tactic
under the assumption that pf is of type proof, then
pf.(X pf) is also a tactic. When it is applied to
a proof pf will be bound to the proof, and then
the tactic defined by X will be applied.
In the last line an attempt is made to
prove completely all of the unproved subgoals generated so far.
The next example illustrates some of the other functions available in the ML environment of Nuprl . Given an integer, bring_hyp returns a refinement tactic implementing the rule
>> T' by bring_hyp i
>> T->T'
where T is the type in hypothesis i.
This is often useful when it is desired that the substitutions
done by an elimination be done in a hypothesis also; using
this tactic, doing the elimination and then doing an introduction
accomplishes this.
Figure 
shows the implementation of this tactic.
The function select takes an integer n and
a list and returns the 
element of the list, and
type_of_declaration breaks down a declaration into
its two components and returns the second part. make_function_term
takes an identifier x and terms A and B to a term x:A->B.
Note that because of the intended purpose of the tactic
no attempt is made to prove one of the generated subgoals.
