Case-split
Like force but immediately splits the top-level goal on the hypothesis
Case-split is a 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 interactive proof-builder, case-split behaves like
force.
Function: case-split
(defun case-split (x)
(declare (xargs :guard t))
x)
