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.