## CASE-SPLIT

like force but immediately splits the top-level goal on the hypothesis
Major Section: MISCELLANEOUS

`Case-split`

is an variant of `force`

, which has similar special
treatment in hypotheses of rules for the same rule-classes as for
`force`

(see force). This treatment takes place for rule classes
`:`

`rewrite`

, `:`

`linear`

, `:`

`type-prescription`

,
`:`

`definition`

, `:`

`meta`

(actually in that case, the result of
evaluating the hypothesis metafunction call), and
`:`

`forward-chaining`

.

When a hypothesis of a conditional rule (of one of the classes listed above)
has the form `(case-split hyp)`

it is logically equivalent to `hyp`

.
However it affects the application of the rule generated as follows: if ACL2
attempts to apply the rule but cannot establish that the required instance of
`hyp`

holds in the current context, it considers the hypothesis true
anyhow, but (assuming all hypotheses are seen to be true and the rule is
applied) creates a subgoal in which that instance of `hyp`

is assumed
false. (There are exceptions, noted below.)

For example, given the rule

(defthm p1->p2
(implies (case-split (p1 x))
(p2 x)))

then an attempt to prove
(implies (p3 x) (p2 (car x)))

can give rise to a single subgoal:
(IMPLIES (AND (NOT (P1 (CAR X))) (P3 X))
(P2 (CAR X))).

Unlike `force`

, `case-split`

does not delay the ``false case'' to a
forcing round but tackles it more or less immediately.The special ``split'' treatment of `case-split`

can be disabled by
disabling forcing: see force for a discussion of disabling forcing, and also
see disable-forcing. Finally, we should mention that the rewriter is never
willing to split when there is an `if`

term present in the goal being
simplified. Since `and`

terms and `or`

terms are merely
abbreviations for `if`

terms, they also prevent splitting. Note that
`if`

terms are ultimately eliminated using the ordinary flow of the proof
(but see set-case-split-limitations), so `case-split`

will ultimately
function as intended.

When in the proof checker, `case-split`

behaves like `force`

.