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 >> Texcept 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

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

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.

Thu Sep 14 08:45:18 EDT 1995