Proof Environment and Theorem

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.