Environment modification commands:

assign:

The assign command takes two string arguments, both terms. If the second term matches the first, the induced substitution is applied to both sides of the equation under construction.

assignit:

The assignit command takes one string argument. It has the effect of the assign command with its argument as first argument and the currently selected subterm as second argument.

assigninto:

The assigninto command takes two arguments, a free variable and a term. Each side of the equation under construction is replaced by the result of substituting the appropriate side of the equation for the variable argument in the term argument.

unification:

The unification command takes one string argument. It applies substitutions into both the argument (interpreted as a term) and both sides of the current equation, in such a way as to make the new form of the argument the same as the new form of the currently selected subterm, if this is possible. If it is not possible, an error message is issued and nothing in the environment is changed. Restriction: terms with free occurrences of bound variables will not be matched with free variables, since this makes it hard to determine whether global substitutions are legitimate. u is an abbreviation for this command.

ul:

As unification, except that the argument is the name of a theorem and the left side of that theorem is unified with the currently selected subterm. The effect is to attempt to make substitutions which make the theorem applicable.

ur:

As unification, except that the argument is the name of a theorem and the right side of that theorem is unified with the currently selected subterm. The effect is to attempt to make substitutions which make the converse of the theorem applicable.

initializecounter:

This command takes a unit argument. It has the effect of resetting the new variable counter to 1.

ruleintro:

The ruleintro command takes a string argument, a term. The string argument is introduced as an embedded theorem attached to the current subterm by the => infix of direct theorem application. ri is an abbreviation for ruleintro.

revruleintro:

The revruleintro command takes a string argument, a term. The string argument is introduced as an embedded theorem attached to the current subterm by the <= infix of converse theorem application. rri is an abbreviation for revruleintro.

inputri:

The inputri command takes a string argument. It is used to supply theorems to be applied to the INPUT tactic. When paused after an execution of INPUT, issue the inputri command with the desired argument, then issue ; to resume execution. iri is an abbreviation for inputri.

targetruleintro:

The targetruleintro command takes a string argument, a term. It will cause a theorem to be introduced which will have the effect of rewriting the selected subterm to the argument, if there is such a theorem. tri is an abbreviation for targetruleintro.

matchtri:

As targetruleintro, but looks for theorems which will give a result matching the argument in structure, rather than an identical result. Theorems are displayed as a side-effect. mtri is an abbreviation for matchtri.

anothermatchtri:

If issued immediately after matchtri (or anothermatchtri this command will search for another suitable theorem. Theorems are displayed as a side-effect. amtri is an abbreviation for matchtri.

tri2:

As targetruleintro, except that it searches for two-step proofs. Very slow!

trimetric:

Takes two arguments, an integer and a target term. Looks for a proof that the selected subterm is equal to the target term, in a number of steps bounded by the integer argument. Proofs must satisfy a condition of ``approaching'' the target term at each step; it does not search all possible proofs. Experimental!

droprule:

The droprule command takes a unit argument. If the currently selected subterm has => or <= as top-level infix, the indicated embedded theorem is dropped.

altruleintro:

This command takes one string argument, a term. If the currently selected subterm has => or <= as top-level infix, the argument is appended to the left subterm (the embedded theorem) using the =>> infix. This is different from the effect in Mark2, though the signalled intention to rewrite is the same. ari is an abbreviation for altruleintro.

altrevruleintro:

This command takes one string argument, a term. If the currently selected subterm has => or <= as top-level infix, the argument is appended to the left subterm (the embedded theorem) using the <<= infix. This is different from the effect in Mark2, though the signalled intention to rewrite is the same. arri is an abbreviation for altruleintro.

execute:

This command takes a unit argument. The tactic interpreter is invoked to carry out all intentions to rewrite indicated by embedded theorems, following a depth-first strategy. ex is an abbreviation for execute.

steps:

This command takes a unit argument. This is a trace command. The tactic interpreter is simulated, carrying out intentions to rewrite indicated by embedded theorems which are applied to terms containing no embedded theorems (innermost applications of embedded theorems). One step is carried out at a time: enter ; to see the next step or e; to quit (in old versions, hit enter to see the next step or q to quit).

stepsnorules:

This command takes a unit argument. As steps, except that embedded theorems are not displayed in the terms, and new terms are displayed only when there are changes other than changes to embedded theorems. This can conceivably go into an infinite loop, which is not the case for steps.

settracelevel:

This command takes a string argument followed by an integer argument. The theorem (in intention, tactic) named by the string argument is assigned a ``trace level'' equal to the integer argument. When steps is executed, theorems with a high enough ``trace level'' (see next command) are executed all at once instead of being traced through their execution. This allows fine-tuning of the trace function provided by steps.

settrace:

This command sets the cutoff value of ``trace level'' above which the steps command executes tactics completely in one step. See previous command.

applyenv:

This command takes a single string argument, the name of a saved environment. The saved environment represented by the argument is applied as a rewrite rule in the direct sense to the currently selected subterm.

applyconvenv:

This command takes a single string argument, the name of a saved environment. The saved environment represented by the argument is applied as a rewrite rule in the converse sense to the currently selected subterm.

cmatch:

This command takes a unit argument. It turns commutative matching on or off. Strict matching is still used by the on-success and on-failure rule infixes. Not available in the official release, but found in a posted draft version. We have decided not to use this.