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.