next up previous contents
Next: List of Error Messages Up: Command Reference Previous: Term Syntax and Display

The Logic of the Definition Facility

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.


next up previous contents
Next: List of Error Messages Up: Command Reference Previous: Term Syntax and Display

Randall Holmes
Fri Sep 5 16:28:58 MDT 1997