next up previous contents
Next: The Syntax Lists Up: The Theory Environment Previous: The Theory Environment

Components of the Theory Environment

The theory environment consists of the constant and operator declaration list, the master theorem list, and some satellite declaration lists and lists containing syntactical information. A theory has a name which associates it with a file.

A list of operator precedences. Parity of the precedence determines left/right associativity (even gives right, odd left). Default precedence of all operators is 0.

Default left arguments:
A list of default left arguments for unary operators.

There is a list of declarations of constants, operators, and free variable operators (the last only for relative typing purposes; free variable operators which do not need to be typed do not need to be declared).

Opacity declarations:
A list of operators declared opaque.

A list of names of theorems which are intended to be proved; needed to make recursive tactics possible while preserving declaration checking for embedded theorems.

A list of constants and operators with the theorems which define them; the name of the theorem will be the same as the name of the defined object, if it is a constant.

Functional programs:
A list of automatic bindings of theorems to constants and operators, implementing functional programming in the tactic language.

There is a list of theorems; this also includes images of current and old saved proof environments. The structure of an individual theorem parallels the structure of a proof environment as noted above, with the addition of the list of theorems supporting the module system. Proof environments saved on the theorem list lose ``position of selected subterm'' information, since this is the one item in the structure of a proof environment that is not found in a theorem.

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