The Old 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.

There are two basic ways to decompose a proof obligation into simpler obligtions:

/\ decomposition

If  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  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 .

Often, a proof obligation must be transformed into an equivalent one in order to be decomposed by /\ or \/ decomposition. There are two 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.)

=> splitting

A goal  P => Q  is equivalent to the assumption  P  and the goal  Q .

\A splitting

A goal  \A x \in S : P  is equivalent to the assumption  NEW x \in S  and the goal  P .  The goal  \A x : P  is similarly split.

/\ splitting

An assumption  P1 /\ ... /\ Pn , is equivalent to the  n  assumptions  P1, ..., Pn .

\E splitting

An assumption  \E x \in S : P  is equivalent to the two assumptions  NEW x \in S, P . The goal  \E x : P  is similarly split.

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 => \E 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.

Options

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 assumption are added to each of the decomposed proof steps. 

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.  One reason not to choose this option is that the Decompose Command does not decompose CASE steps.

Limitations

• The command will not expand definitions that come from a different module.



• Decomposing a proof step may require renaming of bound identifiers to avoid name clashes.  This renaming is not done for clashes with names defined by LET definitions within the step.  This can cause parsing errors in the decomposed proof.