The ``proof environment'' and ``theorem'' data types are closely related and will be discussed together here.

A proof environment has five ingredients: a name (which can usually be thought of as a string but must technically be regarded as a term, because it may be parsed to determine the ``format'' of the theorem to be proved (no longer true; name a format are now distinct)), the left side of the equation being proved, the right side of the equation being proved, a list of names of axioms on which the theorem to be proved depends, and, finally, a list of booleans which represents the position of a specific subterm of the right side of the equation to be proved.

A theorem has a name, a ``format'' (a term which determines with what arguments the theorem should be invoked), a left side, and right side, a list of dependencies, and a list of theorems used by the module system.

It appears that the name and format ought to be distinct elements of proof environments (this is now the case). Dependencies are expected to be expanded to include dependencies on definitions and on programs; this will improve reaxiomatization and theorem export facilities.

There are no commands specifically manipulating the theorem type (theorems appear as components of theories, for which see below).

Proof environment commands include the following (for commands creating proof environments, see the workspace subsection; for command which actually prove theorems, see the theory subsection):

**envname**- See the name of the current environment.
**look***or*lookhere*or*lookback:- ``look'' displays
the right side of the equation (with the current subterm in braces)
above and the current subterm below. Invoked automatically by many
commands. ``Lookhere'' shows the current subterm only; ``lookback''
shows the left side of the equation.
**lookhyp <integer>:**- Displays the hypothesis indexed by the
integer (see discussion of the hypothesis facility above).
**lookhyps:**- Displays all hypotheses.
**seedeps:**- See the list of names of axioms on which the current
theorem depends.
**startover***or*starthere*or*workback:-
Manipulations of general equation structure. ``Startover'' sets
both sides of the equation to the left side and clears dependencies,
and ``starthere'' does the same with the right side. ``Workback''
interchanges the two sides of the equation and leaves dependencies
unaffected.
**left***or*right*or*up*or*top:- Basic
``movement commands''. These cause the current subterm to be reset
to its ``left child'', ``right child'', ``parent'', or the whole
right side of the equation, respectively. ``Constant function''
terms have only one ``child'', which is treated as both left and
right child; if one ``moves'' left or right from an atomic term, one
gets an error condition, but it is currently necessary to move up or
to the top to escape this condition (the list of booleans does get
set to the non-existent position!)
**upto***or*downtoleft*or*downtoright <term>:-
Sophisticated movement commands; they move as indicated (up, or down
to left or right) until a term matching the argument is reached. If
no such term is found, an error is reported; the position one ends
up in depends on the command.
**New movement commands:**- Commands
`uptols <theorem>`,`uptors <theorem>`,`dlls <theorem>`,`dlrs <theorem>`,`drrs <theorem>`, and`dlrs <theorem>`enable movement to places where theorems can be applied. Commands beginning with`upto-`implement ``upto''; commands beginning with`dr-`and`dl-`implement ``downtoleft'' and ``downtoright''; the suffix indicates ``left side'' or ``right side''. **ruleintro***or*revruleintro <term>:- Introduce an
application of a theorem or its converse (indicated by use of the
connectives ``=>'' or ``<='' respectively in the displayed
result). The theorem may have parameters, thus the argument must be
a term. The dependencies of this theorem are added.
**matchruleintro***or*targetruleintro <term>:-
Introduce an embedded theorem or theorem converse which matches a
given equation (the first command) or will convert the current
subterm to a given target term (the second command).
**altrule:**- If the current subterm is an infix term with infix
``=>'' or ``<='', convert the infix to =>>, <<= respectively
(or the reverse). This converts embedded theorems and converse
theorems to the form appropriate for lists of alternatives no more
than one of which should be applied.
**droprule:**- Drop an embedded theorem from the top level of the
current subterm.
**delay***or*undelay:- Introduce or eliminate the special
prefix ``#'' which converts operators with ``functional programs''
associated to ``inert'' form.
**lazy***or*unlazy:- Introduce or eliminate the full
laziness prefix
`##`. **execute***or*steps*or*onestep:- Invoke the
interpreter (resp. debugger) for the internal programming language.
In general terms, execute causes all embedded theorems to be applied
following a depth-first strategy; ``steps'' simulates ``execute''
step by step with some limited parallelism. More parallel versions
Execute and Steps of these commands are expected to be implemented.
The steps command goes into a loop which is broken by hitting ``q'';
it stops automatically if the term stabilizes. If you break out of
any of the tactic interpreters using Control-C, you should issue the
``top'' command to reset environment variables.
**applythm***or*applyconvthm <term>:- Apply the
indicated theorem or converse theorem (possibly with parameters);
does not apply any new embedded theorems produced by this
application. Useful for editing.
**applyenv***or*applyconvenv <term>:- As above, except
that saved environments are used.
**assign***or*assigninto <term> <term>:- Carries out
global assignments to variables; can affect both sides of the
equation under construction. The first argument is a variable term.
The second argument is any term. In the case of ``assign'', the
second argument is substituted for the first throughout the left and
right sides of the current equation. In the case of ``assigninto'',
the left and right sides of the current equation are substituted for
the variable first argument in the second argument to obtain the new
left and right sides.
**assignit <term>:**- Equivalent to the assign command with the
variable first argument given on the command line and the second
argument the current subterm.

Fri Sep 5 16:28:58 MDT 1997