Ctl+G Ctl+Dor right-clicking and selecting the command.
There are two basic ways to decompose a proof obligation into simpler obligtions:
P1 /\ ... /\ Pn, then the proof of
Pcan be broken into the proof of the
P1, ... , Pn.
\/decomposition (case split)
P1 \/ ... \/ Pn, then the proof of
ASSUME P PROVE Qcan be broken into the proof of the
ASSUME P1 PROVE Q, ..., ASSUME Pn PROVE Q.
Often, a proof obligation must be transformed into an equivalent one in order to be decomposed
\/ decomposition. There are two transformations that can be
applied to the goal of an obligation. (The goal is the
PROVE formula of an
obligation or the entire obligation, if it is a single formula.)
P => Qis equivalent to the assumption
Pand the goal
\A x \in S : Pis equivalent to the assumption
NEW x \in Sand the goal
P. The goal
\A x : Pis similarly split.
P1 /\ ... /\ Pn, is equivalent to the
nassumptions P1, ..., Pn .
\E x \in S : Pis equivalent to the two assumptions
NEW x \in S, P. The goal
\E x : Pis similarly split.
\Esplittings can be combined hierarchically.)
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
\/ 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
For example, starting from the obligation
P => \E x \in S : Q, performing
=> 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.
\Eassumption generates new assumptions. Selecting this option causes those assumptions to be asserted by a
SUFFICES ASSUME/PROVEstep. Otherwise, these assumption are added to each of the decomposed proof steps.
CASEsteps should be used instead of
ASSUME/PROVEsteps when possible. One reason not to choose this option is that the Decompose Command does not decompose
LETdefinitions within the step. This can cause parsing errors in the decomposed proof.