The Decompose Proof Command

The Decompose Proof command is executed by placing the cursor in a proof obligation, either a proof step or a theorem, and either typing Ctl+G Ctl+D or right-clicking and selecting the command. Clicking on the button labeled ? in the upper right corner of the command's pop-up window displays this page.

The command provides two basic ways to decompose a proof obligation into simpler obligations:

/\ decomposition: If formula P equals P1 /\ ... /\ Pn , then the proof of P can be broken into the proof of the n formulas P1, ... , Pn .
\/ decomposition (case split): If formula P equals P1 \/ ... \/ Pn , then the proof of ASSUME P PROVE Q can be broken into the proof of the n obligations ASSUME P1 PROVE Q, ..., ASSUME Pn PROVE Q (or the equivalent CASE steps).

Often, a proof obligation must be transformed into a different one in order to be decomposed into simpler obligations, where the decomposition may be done manually or by the Decompose Proof command. The command provides the following two such transformations that can be applied to the goal of an obligation. The goal is the PROVE formula of an ASSUME/PROVE obligation or the entire obligation, if it is a single formula. For a CASE or QED step, it is the proof's current goal.

=> splitting: A goal P => Q is transformed to the assumption P and the goal Q .
\A splitting: A goal \A x \in S : P is transformed to the assumption NEW x \in S and the goal P . The goal \A x : P is similarly split.

There are two such transformations that can be applied to an assumption of an ASSUME/PROVE obligation:

\E splitting: An assumption \E x \in S : P is transformed to the two assumptions NEW x \in S, P .
/\ splitting: An assumption P1 /\ ... /\ Pn , is transformed to the n assumptions P1, ..., Pn . This transformation can be performed by the Decompose Proof command only if at least one of the conjuncts Pi can be further decomposed by the command.

These transformations (decompositions and splittings) are effected by clicking on the appropriately labeled buttons. You can perform multiple transformations before generating the proof. The \/ decomposition and \E splitting transformations can be combined hierarchically. Clicking on the ← button undoes the last transformation that has not been undone.

The proof is generated by clicking a button that is either labeled by P or (for an /\ decomposition) by a button with P next to it.

Instead of generating an /\ or \/ decomposition, the button labeled P at the top of the command's dialog window generates a proof consisting of only a SUFFICES ASSUME ... PROVE step, constructed by splitting the original obligation, and a QED step. For example, starting from the obligation P => \A x \in S : Q , performing a => split followed by a \A split on the goal and then clicking on this button produces a proof like this:

   <3> SUFFICES ASSUME P, NEW x \in S
                PROVE  Q
     OBVIOUS
   <3> QED

The obligation to which you apply the Decompose Proof command must have either no proof or else a leaf proof, such as a BY proof or the proof OBVIOUS . If it has a leaf proof, that proof is made the proof of each of the simpler obligations into which the proof is decomposed. For a proof generated by the top P button (which does no decomposing), the obligation's leaf proof becomes the QED step's proof.

You can use the command to transform the goal and/or usable assumptions that come from the statement's ASSUME formulas and/or from previous statements. The formula to be transformed must either have the appropriate form or else consist of a single occurrence of a user-defined operator whose definition has that form. The command displays only assumptions that can be transformed and new assumptions that have been created so far by the current use of the command--the latter being displayed below a dashed line.

Options

There are three options that you can select.

Show Context: A context assumption is a usable assumption that comes from the theorem or from a previous step. Context assumptions are displayed (and can thus be transformed) if and only if this option is chosen.
Use SUFFICES: Splitting the goal or a \E assumption generates new assumptions. Selecting this option causes those assumptions to be asserted by a SUFFICES ASSUME/PROVE step. Otherwise, these assumptions are added to each step of the decomposed proof to which they apply.
Use CASE: This selection determines whether, in the created substeps of the proof of an \/ decomposition, CASE steps should be used instead of ASSUME/PROVE steps when possible.

Limitations

The following are the known problems and limitations of the command.

The command will not expand definitions that are imported into the current module by parametrized instantiation--that is, via a statement such as.
```
      Foo(x) == INSTANCE M WITH ... 
```
Decomposing a proof step may require renaming of bound identifiers to avoid name clashes. This renaming is not done for clashes with identifiers introduced by a LET definition within the step or by an expression in an argument of a user-defined operator whose definition is being expanded. This failure to avoid name clashes will cause parsing errors in the decomposed proof that must be fixed by hand.

↑ Viewing and Editing Structured Proofs