# 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