Up: Command Reference
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
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
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):
- 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).
- Displays all hypotheses.
- See the list of names of axioms on which the current
- 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
- left or right or up or top:
``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).
- 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.
- Drop an embedded theorem from the top level of the
- 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.
Up: Command Reference
Fri Sep 5 16:28:58 MDT 1997