Abstraction and reduction by built-in tactics

The semantic interpretation of bracket terms as functions is enforced by the three built-in tactics BIND, EVAL and UNEVAL.

BIND takes a parameter: when BIND @ T is applied to a term U at level l, the effect is to translate U to level l+1, replace all occurrences of the result of translating T to level l+1 in the translation of U by occurrences of ?[l+1] (we hope that this is a pardonable abuse of notation), enclose the result in brackets and apply it (using @ to represent function application) to T; this process only succeeds if the bracket term obtained is stratified (otherwise U is unchanged). In terms of $\lambda$-notation, the result can be described as $(\lambda x.U[x/T])(T)$.

EVAL takes no parameter; when EVAL is applied to a term of the form [T] @ U at level l, the effect is to translate U to level l+1, replace ?[l+1] with the translated form of U in T, and translate this modified form of T from level ?[l+1] to level l; this modified form of T is the result. Mathematically, this is simply $\beta$-reduction, and it always succeeds.

UNEVAL is a little more esoteric, and it took some experience to realize that it was needed. When UNEVAL @ [T] is applied to U, the result is a term of the form [T] @ X precisely if there is such a term which would reduce to U on application of EVAL. The effect of UNEVAL is to rewrite an expression as a value of the function given as its parameter if this is possible.

The project of providing built-in support to synthetic abstraction and reduction algorithms found in the original prover EFTTP (as discussed in our reference [14]) and still supported by little-used features of Mark2 has been abandoned. Synthetic abstraction and reduction algorithms are straightforward to implement in the tactic language of Mark2 or Watson. We are still carrying out investigations in this area using the Watson tactic language as a tool. But we no longer see it as reasonable to support this in the prover's built-in logic.