A theory consists of a list of theorems, a list of constant declarations, and some auxiliary lists of declarations. Theories can be saved to and loaded from files.

The lists which comprise a theory at this time (other than lists used by the parser which will be discussed below under Term) are

**CONSTANTS:**- Master list of constant declarations. Contains all
identifiers and operators; for operators, reports the relative types of
their arguments. Now contains comments.
**THEOREMS:**- Master list of theorems. For the structure of a
theorem, see above.
**PRETHEOREMS:**- List of identifiers or operators which will
eventually be proved as theorems (needed for recursive theorem
definitions).
**DEFINITIONS:**- List of defined identifiers and operators with
their defining theorems.
**PROGRAMS:**- List of bindings of identifiers and operators to
theorems used for simulation of functional programming.
**OPAQUE:**- List of operators declared as opaque to abstraction.

These could reasonably be collapsed into one or two master lists. Additional lists used by the parser referenced under Term below are also an essential part of a theory.

Theory commands include the following:

**declareconstant <string>:**- Declare an identifier as a
constant.
**declaretypedinfix <integer> <integer> <string>:**-
Declare an infix. The string is its form; the integers are the
``relative types'' of its left and right arguments.
**declareinfix <string>:**- Declare a ``flat'' infix (with both
relative types 0)
**declareunary <string>:**- Declare a unary prefix (its default
left argument will be
`defaultprefix`). **newcomment <string> <string>:**- Enter new comments (the
second string) on the declared object named by the first string (any
older comments will be superseded). These will be displayed by
declaration and theorem display commands.
**appendcomment <string> <string>:**- As
`newcomment`, except that comments are appended to existing comments. **makeunary <string>:**- Give an existing infix the default
left argument
`defaultprefix`. **declarepretheorem <string>:**- Declare an identifier (or
infix) as a prospective theorem (so that it can be introduced as an
embedded theorem; useful in cases of recursion).
**declareopaque <string>:**- Declare an operator as opaque to
abstraction. Used to declare new operator; an existing operator cannot be
made opaque.
**makescin***or*makescout <string> <string>:- These
commands allow the user to declare the function or operator denoted by
the first string argument to have input or output (resp.) restricted
to absolute types (strongly Cantorian sets). The second string
argument must be the name of a theorem witnessing this fact.
**proveprogram <string> <string>:**- Bind to the constant
or operator named by the first argument the theorem named by the second
as a ``functional program''.
**deprogram <string>:**- Remove any program bound to the
constant or operator named by the argument.
**pushtheorem***or*pushtheorem2 <string> <string>:-
Hide the theorem named by the first string in the module associated
with the theorem named by the second string. The hidden theorem is
only visible when the parent theorem is executing, but its name
remains reserved. The first version of the command posts a comment to
the declaration of the hidden theorem automatically; the second does
not.
**poptheorem***or*poptheorem2 <string> <string>:-
Reverses the effect of
`pushtheorem`.`poptheorem`posts a comment automatically to the declaration of the no longer hidden object;`poptheorem2`does not. **axiom <string> <term> <term>:**- Creates an axiom with
name the first string argument, left side the second argument and
right side the third argument. An axiom can be recognized by its
list of axiom dependencies consisting of its own name. Axioms
cannot take parameters, so the first argument does not need to be a
term.
**interaxiom <string>:**- If the current subterm is an
equation, makes it an axiom.
**prove <term>:**- Causes the equation expressed in the current
proof environment to be recorded as a theorem with name and
``format'' determined by the term argument (the argument will be
either the theorem name alone or the theorem name with a list of
parameters). The theorem to be proved cannot already be a theorem,
though it can be a pretheorem.
**reprove <term>:**- Allows one to change an existing theorem;
the only restriction enforced is that the dependencies of the
theorem cannot get stronger. Axioms and definitions cannot be
reproven.
**autoprove***or*autoreprove:- As ``prove'' or ``reprove'',
except that the format of the theorem proved is the name of the
current workspace. Especially useful in a workspace created by
``getleftside'', ``getrightside'' or ``autoedit''.
**impredicative:**- This command allows definitions of more general
form and allows the built-in RAISE theorem to work on non-flat
infixes. The default state of the prover is now impredicative.
**defineconstant <term> <term>:**- Introduce a theorem
defining a constant, with the same name as that constant. The
constant cannot previously have been declared. The first term is a
constant name or a constant applied to a list or lists of
parameters, which is the left side of the intended theorem; the
second term is the right side of the intended theorem. The
structure of the definition is checked. Definitions are recorded in
dependency lists like axioms.
**definetypedinfix <string> <integer> <integer> <term> <term>:**- As defineconstant, except that an infix with
specified left and right types is defined. The first string
argument is the name of the theorem to be added (since a solitary
infix is not a theorem name). The fourth and fifth arguments
correspond to the arguments of defineconstant.
**defineinfix <string> <term> <term>:**- Defines
``flat'' infixes (with both relative types 0). The first argument
is the theorem to be added; the second and third correspond to the
arguments of defineconstant.
**defineitconstant, defineittypedinfix, defineitinfix:**- have
arguments as above, except for the last, which is replaced by the
current subterm.
**defineopaque <string> <term> <term>:**- Defines opaque
operators. The arguments are as for ``definetypedinfix'', with the
omission of relative types. Stratification restrictions on the
definition are removed, but the use of the defined function in
definitions of anything non-opaque or in variable binding contexts
is strongly restricted.
**makeanaxiom <string>:**- Makes the theorem indicated by the
argument an axiom.
**proveanaxiom <string>:**- If the current proof environment contains
a proof of an axiom named by the argument, make that axiom a theorem with
the appropriate dependencies, making the appropriate adjustments of
dependencies through the whole theory.
**undefine <string>:**- Convert the definition of the constant
or operator named by the parameter to an axiom.
**defineprimitive <string>:**- If the theorem named by the
argument is of the appropriate form to serve as the definition of an
undefined notion, make it so.
**redefineconstant <string>:**- If the current proof
environment could serve as a definition of a constant now defined,
make it so, with global dependency modifications as appropriate.
The argument is the new name for the old definition theorem.
**redefineinfix <string>:**- If the current proof environment
could serve as a definition of an operator now defined, make it so,
with global dependency modifications as appropriate. The argument
is the name of the new defining theorem.
**Note:**- The preceding commands support reaxiomatization of
theories. This facility can also be used to support the use of as
yet unproved lemmas.
**thmdisplay <string>:**- Displays a theorem. Displays
comments. Displays names of module components (hidden theorems) but
not their contents.
**showalltheorems:**- Displays all theorems (in a loop from which
any key other than Enter breaks out).
**moddisplay <string>:**- Displays a module (a theorem and all
theorems hidden in its module).
**showallmodules:**- Displays all modules (in a loop from which
any key other than Enter breaks out).
**showrelevantthms:**- Displays all theorems which match (or whose
converses match) the current subterm nontrivially (i.e., it does not display
theorems which match all terms).
**showmatchthm <term>:**- Displays a theorem (if there are any) which
justifies the equation given as the argument.
**showdec <string>:**- Displays a constant or operator declaration. it
shows relative types and default left arguments in the case of operators usable
as prefixes. Displays comments.
**showalldecs:**- Shows all declarations (in a loop as with
showalltheorems).

Fri Sep 5 16:28:58 MDT 1997