Next: Starting Out
Up: The Proof Environment
Previous: Applying Theorems as Rewrite
The proof environment is a data structure containing the following
- The environment has a name. This may take the form of a
term serving as the default format for the theorem to be proved
(name and parameters). It is not necessary for the user to set the
name. It is automatically set by certain commands, and it can be
viewed using the envname command.
- left side of theorem:
- This is often but not always the term
originally entered by the user. Assignment commands affect both
sides of the current equation, and it is possible to switch the two
sides using the workback command.
- right side of theorem:
- This is the term being viewed by the
- position of selected subterm:
- A list of booleans is used to
indicate the selected subterm; an integer representing the number of
nested variable binding contexts in which it is found is also
- current dependencies:
- Axioms and definitions on which the
proof so far depends are listed. Such information is maintained as
an element of theorems and tactics as well.
The data structure representing a stored theorem has exactly the
same structure, except that it does not include a ``position of
selected subterm'', and it includes an additional component
supporting the module system described below. The system takes
advantage of this; saved proof environments are kept on the theorem
list, though they cannot be used as theorems.
Fri Sep 5 16:28:58 MDT 1997