case-split behaves like force.
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. (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 forcing. 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.