Ctl+G Ctl+Dor 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:
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(or the equivalent
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
obligation or the entire obligation, if it is a single formula. For a
QED step, it is the
proof's current goal.
P => Qis transformed to the assumption
Pand the goal
\A x \in S : Pis transformed to the assumption
NEW x \in Sand the goal
P. The goal
\A x : Pis similarly split.
\E x \in S : Pis transformed to the two assumptions
NEW x \in S, P.
P1 /\ ... /\ Pn, is transformed to the
P1, ..., Pn. This transformation can be performed by the Decompose Proof command only if at least one of the conjuncts
Pican be further decomposed by the command.
\Esplitting 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
\/ 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 => \A 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.
You can use the command to transform the goal and/or usable assumptions that come from the
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.
\Eassumption generates new assumptions. Selecting this option causes those assumptions to be asserted by a
SUFFICES ASSUME/PROVEstep. Otherwise, these assumptions are added to each step of the decomposed proof to which they apply.
CASEsteps should be used instead of
ASSUME/PROVEsteps when possible.
Foo(x) == INSTANCE M WITH ...
LETdefinition 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.