next up previous contents
Next: The Tactic Language Up: Declarations Previous: Refinements: Embedded Theorems and

The Definition Facility

The commands defineconstant, defineinfix, definetypedinfix, and defineopaque can be used to define (and automatically declare) constants or operators.

The predeclared operators @ (function application) and , (ordered pair) have a special role in the definition facility.

A definition introduces an equation whose left side must have a special form.

We first define the class of argument lists. A free variable or iterated constant function of a free variable (built using brackets) is an argument list. Any pair (built using the , infix) of argument lists is an argument list. All argument lists are constructed in this way.

If a constant is being defined, the constant itself is a possible left side for its defining equation. If any term is an admissable left side, the term built by applying that term to an argument list (using the @ infix) is an admissable left side. All admissable left sides for constant definitions are constructed in this way.

If an operator is being defined, a unary or binary term whose left and right subterms (the left may, of course, not be present; a default left argument of defaultprefix is automatically declared in this case) are argument lists is an admissable left side. The result of applying an admissable left side to an argument list is an admissable left side. All admissable left sides for operator definitions are constructed in this way.

Notice that ``curried'' higher order functions can be implicitly defined!

The further conditions on a definition are that the constant or operator being defined be undeclared, but that all other constants appearing in the defining equation be declared, that every free variable occurring on the right side also occur on the left side (no operator variables may appear in a definition), and that the defining equation considered as a term (= is predeclared and has left and right types of 0) be stratified.

Implicit function definitions using this procedure are guaranteed to avoid paradox (they are valid in the context of New Foundations with urelements). The ability to apply the constant function operator to variables allows more control over the relative typing of arguments; attention to relative type is also important when currying is used (a curried function is not equivalent to a similar-looking function with an argument list built using pairing; relative types are quite different!).

The defineitconstant, defineitinfix and defineittypedinfix commands allow one to use the selected subterm of the right side of the current equation as the right side of a definition.


next up previous contents
Next: The Tactic Language Up: Declarations Previous: Refinements: Embedded Theorems and

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