Also see the ML Manual for Nuprl4.
Writing complicated tactics requires a thorough knowledge of the ML programming language [Gordon, Milner, & Wadsworth 79] and the information contained in chapter 9. It is an easy matter, however, to write simple tactics and to combine existing tactics with a minimal subset of ML. ML is a functional programming language with three important characteristics which make it a good language for expressing tactics:
type discipline with secure types. This allows type constraints on the arguments and results of functions to be expressed and enforced. For example, the result of a function may be constrained to be of type proof.
In order to understand the example tactics presented below it is not necessary to know many of the details of ML. The following summarizes some of the more important and less obvious language constructs. Functions in ML are defined as in
let divides x y = ((x/y)*y = x);;
This function has type
intintbool; that is, it maps integers to functions from integers to boolean values. There is also an explicit abstraction operator, , which stands for the more conventional . The previous function could have been defined as
let divides = \ x . \ y . ((x/y)*y = x);;
Exceptions are raised using the expression `` fail'' and handled ( caught) using ``?''. The result of evaluating exp1?exp2 is the result of evaluating exp1 unless a failure is encountered, in which case it is the result of evaluating exp2. For example, the following function returns false if y = 0.
let divides x y = (if y = 0 then fail else (y*(x/y)=x) ) ? false;;
In fact, because dividing by 0 causes a failure, we could define the same function with
let divides x y = (y*(x/y)=x)?false;;