The commands for the definition facility are given in the theory subsection. Here we discuss the theory of the definition facility briefly.

A term is said to be a ``parameter list" if it is built from variables using the operation ``," of pairing. A term is said to be in ``definition format" if it is either a constant or a term in definition format applied to a parameter list (using the infix ``@" of function application). A term is said to be in ``infix definition format" if it is the result of applying a unary prefix to a parameter list, the result of applying a binary prefix to two parameter lists, or the result of applying a term in infix definition format to a parameter list using the ``@" connective. The infix cannot be a variable or colon-initial infix.

A term in either definition format has a ``head", the sole constant or infix other than ``@" or ``," which appears.

A ``definition" is a theorem whose left side is in definition format or infix definition format and which serves as the definition of the head (whether constant or infix) of the left side of the equation.

A definition needs to satisfy a number of technical requirements. The head (the notion being defined) cannot have been declared at the time the definition is made. This avoids circular definition neatly. The right side must have no variables other than those which occur in the left side and must contain only declared constants and operators.

To understand the further requirements, it is necessary to explain the
relative type system of the prover. The types are indexed by integers
(including negative integers). Type *n*+1 can be thought of as the
type of functions from type *n* to type *n*. Terms do not have fixed
types, but subterms of a term are assigned types relative to the whole
term. The relative types of left and right arguments of an infix
subterm are determined by adding the left and right types associated
with that infix by its declaration to the type of the whole term; the
relative type of a prefix term is handled in the same way using the
underlying implementation of prefix terms as infix terms; the relative
type of the immediate subterm of a constant function subterm (of its
value) is one less than that of the parent term.

The relevant additional constraint on the form of definitions is that
each variable in the theorem (considering it as a single equation
term) occurs with the same relative type everywhere in the term. In
addition, no variable should occur in a term with an ``opaque"
operator at the top level, and no variable should occur in the left
argument of a function application infix in a theory started with the
`clearpredicative` command unless the ``impredicative" command has
been issued in that theory (this ``predicative'' state used to be the
default state of the prover - old theory files may need the
impredicative command).

Definitions do not have any axiom dependencies. They are projected to have definition dependencies soon so that definitions can be reconfigured in the same way that axioms can now be reconfigured.

The logic of the definition facility is the ``higher-order" logic of the prover; in conjunction with the logic prelude loaded as part of every theory, it gives an implicit logical strength equivalent to Russell's Theory of Types.

Fri Sep 5 16:28:58 MDT 1997