Compound Terms

terms constructed with operators:

Terms are constructed with unary prefix or binary infix operators in the obvious way. Spaces are not needed between atomic terms and operators; the only situation where spaces are needed inside a term is when an infix is followed by a prefix (and this can be avoided by using parentheses).

The default order of operations is that all operators have the same precedence and associate to the right as far as possible. The user can set the precedence of an operator (and reset it at any time). Parentheses ( ) may be freely used in user-entered terms; unneeded parentheses are not displayed by the prover. The precedence of an operator is a non-negative integer; higher integers represent operators which bind more tightly, and the choice of left or right association for binary operators is determined by the parity of the precedence (even associates to the right, odd to the left).

As noted above, a prefix operator is always regarded as an abbreviation for a binary operator with the same shape with a default left argument depending on the operator. Default left arguments for operators can be set individually by the user.

variable binding contexts:

The operation of enclosing a term in brackets [ ] produces a variable-binding context (a lambda-term). The variable bound in a context is determined by the depth of brackets: ?1 is bound in the outermost context, ?2 in the next to outermost, and so forth. Details of change of variables when substitution occurs are automated. There are restrictions on the ``relative types'' with which bound variables can occur in variable binding contexts which will be explained below; terms which do not meet these criteria will be parsed but rejected on the application of further tests.

The simplest use of the variable binding context is as a constant function constructor, when the bound variable is not present.

Limited higher-order matching is now available. At level 1 (?1 free) the term ?f @ ?1 matches any level 1 term: ``?f'' will match the result of binding this term with brackets. Similarly, substitution of a function defined by a variable binding context for ?f in this term will actually cause the ``unbinding'' of the function. Terms of the forms ?f@?2 have similar privileges at level 2 (?2 free), and similarly for each level. This allows the direct proof of a theorem equivalent to the built-in theorem VALUE. When new variables are introduced by theorems, they are introduced as functions of the appropriate bound variable for the level at which they are introduced (this prevents the application of theorems which introduce new variables in cases where a stratification error would be introduced; this is an unintended side-effect, but it is fairly easy to work around by replacing theorems which introduce new variables with theorems to which the values of the new variables are supplied as parameters).