Major Section: MISCELLANEOUS

The application of a rule to a term may cause a goal to simplify to more than one
subgoal. A rule with such an application is called a ``splitter''. Here, we
explain the output produced for splitters when proof output is enabled
(see set-inhibit-output-lst) and such reporting is turned on (as it is by
default) -- that is, when the value of `(`

`splitter-output`

`)`

is
true.

See set-splitter-output for how to turn off, or on, the reporting of splitters. Also see set-case-split-limitations for information on how to control case splits.

We begin by describing three types of splitters.

`if-intro`

: The rule application may have introduced a call of`IF`

, in the sense discussed at the end below.

`case-split`

: For the application of a rule with hypothesis of the form`(case-split <hyp>)`

,`<hyp>`

did not simplify to true or false.

`immed-forced`

: For the application of a rule with hypothesis of the form`(force <hyp>)`

,`<hyp>`

did not simplify to true or false, where immediate-force-modep is enabled (see immediate-force-modep).

These three annotations -- `if-intro`

, `case-split`

, and
`immed-forced`

-- may be used in proof output and summaries for
describing rule applications, as discussed below. A fourth annotation,
`forced`

, maybe also be used in proof output to indicate the application of
a rule with hypothesis of the form `(force <hyp>)`

when `<hyp>`

did not
simplify to true or false, where immediate-force-modep is disabled
(see immediate-force-modep). We don't consider such uses of `force`

to
be splitters, because they do not cause case splits (though they do produce
goals to prove after lower-case ``q.e.d.'' is printed); see force.

There are three kinds of output affected by splitters, illustrated in turn below using examples.

(a) During the proof, gag-mode off

(b) During the proof, gag-mode on

(c) Summary

Of course, (a) and (b) are skipped if proof output is inhibited, which (c) is skipped if summary output is inhibited; see set-inhibit-output-lst.

(a) During the proof, gag-mode off

With gag-mode off (or when using `:`

`pso`

, `:`

`psof`

, or
`:`

`psog`

) one normally gets an English commentary. The following
output indicates that at least one application of each rule `F`

and `G`

is of type `if-intro`

, at least one application of rules `G`

and `R1`

are of type `case-split`

, and at least one application of rule `R3`

is of
type `immed-forced`

. If immediate-force-modep is off then
```immed-forced`

'' would be replaced by ```forced`

''.

This simplifies, using the :definitions F (if-intro), G (case-split and if-intro) and H and the :rewrite rules R1, R2 (case-split), and R3 (immed-forced), to the following two conjectures.

Note that any such printing of ```forced`

'' is done even if
`(splitter-output)`

is false. Such forcing indication is also made when
raw proof format is used -- see set-raw-proof-format -- but in that
case, no indication is made for splitters in the proof output.

(b) During the proof, gag-mode on

With gag-mode on the proof output is greatly abbreviated. However, ``Splitter Notes'' are printed so that even with gag-mode on, one can get important information to help control large case splits, by disabling splitter rules as appropriate. These are printed at the point when a goal splits into subgoals. Here, for example, is the Splitter Note that corresponds to the output shown in (a) above. It shows the goal whose simplification has produced a split into more than one subgoal, and it shows how many subgoals have been created.

Splitter note (see :DOC splitter) for Subgoal *1/2.2.1' (2 subgoals). case-split: ((:DEFINITION G) (:REWRITE R2)) immed-forced: ((:REWRITE R3)) if-intro: ((:DEFINITION G) (:DEFINITION F))No such splitter notes are printed for the use of

`force`

(when
immediate-force-modep is off).(c) Summary

Here is a possible summary corresponding to our running example. In the summary, ``Splitter rules'' is omitted if there are no splitter rules, and a splitter type is only mentioned if there is at least one corresponding splitter rule.

Summary Form: ( THM ...) Rules: ((:DEFINITION F) (:DEFINITION G) (:DEFINITION H) (:REWRITE R1) (:REWRITE R2) (:REWRITE R3)) Splitter rules (see :DOC splitter): case-split: ((:DEFINITION G) (:REWRITE R2)) immed-forced: ((:REWRITE R3)) if-intro: ((:DEFINITION G) (:DEFINITION F)) Time: 0.01 seconds (prove: 0.00, print: 0.00, other: 0.00) Prover steps counted: 145No indication for ``

`forced`

'' is given for ``Splitter rules''. (As
discussed earlier above, the `force`

d hypotheses are not considered
relevant for determining splitter rule applications unless
immediate-force-modep is on.)We conclude by giving the criteria for a rewrite or definition rule
application to be a splitter of type `if-intro`

.

o Reporting of splitter rules is on, i.e., the value of

`(`

`splitter-output`

`)`

is true.o At least two subgoals are created, even before considering subgoals generated by hypotheses that are calls of

`case-split`

or`force`

.o The term to which the rule is applied is at the top level, rather than being encountered when trying to establish the hypothesis of a rule.

o The rule is a rewrite rule, a definition rule, or a meta rule.

o There is a call of the function symbol

`IF`

in the right-hand side of the rewrite rule; or, in the case of a definition rule, in the body of the definition; or, in the case of a meta rule, in the result of applying the metafunction.o There is a call of the function symbol

`IF`

in the result of rewriting: the right-hand side (for a rewrite rule), the definition body (for a definition rule), or the metafunction application (for a meta rule).

Any rule application meeting the above criteria will be considered a splitter
of type `if-intro`

, even if the call does not actually cause a case split.
For example, if you are proving `(implies (hyp x) (conc x))`

and rule R
rewrites `(hyp x)`

to `(if (h1 x) (h2 x) nil)`

, which is really the term
`(and (h1 x) (h2 x))`

, then R may be labelled as a splitter rule. If you
want to find the causes of case-splitting, the list of `if-intro`

splitters
can help you narrow your search, but may include irrelevant rules as well.

Finally, note that you may see splits not attributed to splitters. We
believe that this will be uncommon during simplification, though it can occur
for example when a call of `IF`

is in the body of a `LET`

expression,
i.e., in a call of a `LAMBDA`

expression. But splits caused by other
processes, notably destructor elimination (see elim), will typically not be
attributed to splitters.