like force but immediately splits the top-level goal on the hypothesis

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.