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.

Precedences:

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.

Declarations:

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.

Pretheorems:

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.

Definitions:

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.

Theorems:

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.