Major Section: MISCELLANEOUS
When a hypothesis of a conditional rule has the form
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
hyp holds in the current context, it goes ahead and
applies the rule anyhow, but creates a subgoal in which that
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
case-splitdoes 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