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 P
equals
P1 /\ ... /\ Pn
,
then the proof of P
can be broken into the
proof of the n
formulas
P1, ... , Pn
.
\/
decomposition (case split)
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 P => Q
is transformed to the assumption P
and the goal Q
.
\A
splitting
\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.
ASSUME
/PROVE
obligation:
\E
splitting
\E x \in S : P
is transformed to the two assumptions
NEW x \in S, P
.
/\
splitting 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.
\/
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.
SUFFICES
\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.
CASE
\/
decomposition, CASE
steps should be used instead of ASSUME/PROVE
steps when possible.
Foo(x) == INSTANCE M WITH ...
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.