# 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