B System Commands

B System Commands

In this appendix, we describe all commands that the user can apply to control the system. Some commands are only applicable in declaration mode (when the system is processing declarations as described in Appendix "The Specification Language), others are only applicable in proving mode (when the system is constructing the proof of a formula under the guidance of the user); some commands are applicable in both modes.

Every command has a textual representation that can be typed in on the command line⁸. If the system is executed with its GUI and is running in proving mode, all applicable commands can be also selected from a menu that pops up when pressing the button . Additionally various commands can be applied by pressing a button in the prover's GUI or by selecting an item in the menu associated to every formula in a proof state (which specializes the command for the application to this formula). A few commands can be selected from the GUI's window menu "File".

Derivation Rules and Sequents

The effect of some commands of the proof states is explained by derivation rules that sketch the logical foundation of these commands. For a command that generates from the current state with label [S] various child states [S1], [S2], ... which is displayed in the proof tree as

[S] c
  [S1] 
  [S2]
  ...

the corresponding rule has the form

[E] A_1, ... |- B_1, ...
[E] A_2, ... |- B_2, ...
...
------------------------
[E] A, ... |- B, ...

where a sequent [E] A, ...|- B, ... represents a proof state with declaration environment E, assumptions A, ... and goals B, .... The sequent below the line represents the proof state labeled [S], the sequents above the line represent the child states [S1], [S2], ...generated by the application of the command. Consequently, the rule can be read "from bottom to top" as

Furthermore, a sequent of the special form [E] |- a:T means "in environment E, expression e has type T"; a sequent [E] |- I:T=V means "in environment E, constant I has type T and value V" The environment [E,a:T] is derived from environment [E] by adding the declaration of a constant a of type T (shadowing any previous declaration of a constant with the same name).

Type Checking Conditions

If the prover command contains a value expression, it may give rise to a type checking condition. The prover handles this condition by generating a child state (in addition to the child states generated anyway by the command) with the type checking condition as a single goal (which may be automatically discharged by a decision procedure as in declaration mode, or by an user-controlled proof).

Proof Status

Every proof of a formula has a couple of status attributes which are displayed in the menu of the formula. These attributes are:

Trust Status: "trusted" or "untrusted"

When a proof is read from file, it is given status "trusted", if none of the declarations and proofs on which the proof depends has changed since the time that the proof was generated. Replaying the proof thus cannot trigger an error. Otherwise the proof is given status "untrusted"; replaying the proof may trigger errors. Replaying an untrusted proof promotes its status to "trusted" (after having removed from the proof those commands that yielded errors in the replay).

Completion Status: "closed" or "open"

A proof is closed, if every leaf of the proof tree denotes a proof situation that is automatically closed by the prover (via the application of an internal or external decision procedure). Otherwise the proof is "open": there are still proof states that require investigation by the user.

Dependence Status: "absolute" or "relative"

A complete proof is "absolute", if it does not depend on assumptions introduced by application of command lemma or only on assumptions which have themselves absolute proofs. Otherwise the proof is "relative": its correctness depends on formulas that still need proof.

Proof Replay

When a previously stored proof is replayed but the formula to be proved has changed since the generation of the proof, the proof is marked as "untrusted" and a warning is issued that errors may occur in the replay. There are two kinds of errors possible:

• A proof command triggers an error, i.e. the command applicable in a state of the original proof is not applicable any more in the corresponding state of the new proof. In this case, the system gives the user the possibility to provide a substitution command which is executed instead of the original command (continuing the replay of the proof subtrees on the child states). If the user abandons the offer, the corresponding proof state remains open (i.e. the proof subtrees corresponding to the child states are lost).
• A proof command generates in the new proof not the same number of child states than in the original proof. In this case, the system asks the user to map the new child states to the old child states such that the proof trees recorded for the child states are not completely lost.

In the first kind of error, the possibility to substitute a proof command is mainly useful if the command has failed because it refers to the label of a formula that has changed since the proof was created. In this case, the user may investigate the proof state, find the corresponding formula, and then execute the command again with a reference to the new label; the remainder of the proof is thus preserved.

As an example for the second kind of error, let us assume that the command scatter has in the original proof of a formula f been applied to a goal a / b generating two child states, one with goal a and one with goal b. If afterwards the declaration of f has been changed such that in the corresponding state of the new proof the goal has form a / b / c, the proof replay gives the following dialog:

Formula f already has a (skeleton) proof 
  (proof status: untrusted)
Replay skeleton proof (y/n)? y
Warning: proof is untrusted, errors may occur.
Warning: problem in state [gda].
In the old proof, command "scatter" generated 
  2 states:
0:	expand a
1:	expand b
In the new proof, the command generates 3 states 
  with the following goals:
0:	a
1:	b
2:	c
You can now map ranges [a..b] of new states to 
  equally sized ranges [c..] of old states.
Enter start state a (0..2, -1 to abort): 0
Enter end state b (0..1, -1 to abort): 1
Enter start state c (0..0, -1 to abort): 0
Enter start state a (0..2, -1 to abort): -1
You have constructed the following mapping:
New states [0..1] are mapped to old states [0..1].
Do you want to use this mapping (y/n)? y
Proof state [wtn] is closed by decision procedure.
Proof state [nxu] is closed by decision procedure.
Proof replay successful.

If no mapping is provided by the user (answer -1 in the dialog), the proof trees generated for the child states in the old proof are lost.

B System Commands