## CASE-SPLIT

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

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

it is logically equivalent to `hyp`

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

holds in the current context, it goes ahead and
applies the rule anyhow, but creates a subgoal in which that
instance of `hyp`

is assumed false.

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.
When in the proof checker, `case-split`

behaves like `force`

.