In
the study of logic a distinction is made between the logic being
studied, the * object language*, and the language
in which the study of
the logic is conducted, the * metalanguage* . In
our case the object
language is the type theory
. Thus far in this book we have conducted
the discussion of
using a combination of English and mathematics
as an
informal metalanguage. In
this chapter we introduce a formal metalanguage
based upon the ML
programming language [Gordon, Milner, & Wadsworth 79].

In ML the various parts of the object language---terms, declarations, proofs
and rules---are data types. By defining a formal metalanguage we have made
concrete the structure and elements of the object language. We can then write
ML programs that manipulate objects of the object language. Thus, for
example, we can write a program to return the subterms of a term or one
that substitutes a term for a free variable in a term. More importantly, we
can write ML functions which search for or transform proofs. We can then
use such automated proof techniques
and theorem--proving heuristics, * tactics* , while
writing proofs.

A tactic is a function written in ML which partially
automates the process
of theorem proving in Nuprl
. In any logic writing a formal proof is a
combination of insightful, interesting steps and tedious ones. Being
required to fill in every detail of a proof distracts one's attention from
the * important* parts of the proof and can be quite tiresome. The
refinement logic of Nuprl
is no exception to this. Given undecidability, we
cannot hope to fully automate the theorem--proving process. Ideally, then, we
would want the user to enter only the * central ideas* of a proof and
leave the details to be filled in by the system. Tactics offer a mechanism
whereby a sketch of a proof supplied by the user can often be completed
automatically and many simple proofs can be avoided altogether. Tactics
can also be used to automate more difficult patterns of proofs that occur
frequently so that essentially the same argument need not be repeated;
a tactic for that pattern of proof would be invoked
instead. The uses of tactics are many and need not be restricted to the
above. There is the potential in the tactic mechanism to express any
decision procedure, semidecision procedure or theorem--proving algorithm
which is valid in the Nuprl
logic.
As will be explained in detail below, the implementation of the
metalanguage makes sure that all proofs produced by tactics are
in fact valid
proofs. This makes it impossible to write
or use a tactic that produces an incorrect proof.

In there are predefined tactics that are always available. These include tactics of general use in theorem proving. The user can easily add new tactics that extend the predefined tactics or are specific to the domain of theorems being proved. The next two sections describe two different kinds of tactics: refinement tactics and transformation tactics. This is followed by an introduction to the ML programming language and an explanation of writing simple tactics. Chapter 9 contains a more detailed description of the metalanguage interface and information on writing tactics and examples of more complicated tactics.

Thu Sep 14 08:45:18 EDT 1995