### ACL2-PC::CASESPLIT

(primitive)
` `

split into two cases
Major Section: PROOF-CHECKER-COMMANDS

Example:
(casesplit (< x y)) -- assuming that we are at the top of the
conclusion, add (< x y) as a new top-level
hypothesis in the current goal, and create a
subgoal identical to the current goal except
that it has (not (< x y)) as a new top-level
hypothesis
General Form:
(casesplit expr &optional use-hyps-flag do-not-flatten-flag)

When the current subterm is the entire conclusion, this instruction
adds `expr`

as a new top-level hypothesis, and create a subgoal
identical to the existing current goal except that it has the
negation of `expr`

as a new top-level hypothesis. See also `claim`

.
The optional arguments control the use of governors and the
``flattening'' of new hypotheses, as we now explain.
The argument `use-hyps-flag`

is only of interest when there are
governors. (To read about governors, see the documentation for the
command `hyps`

). In that case, if `use-hyps-flag`

is not supplied or is
`nil`

, then the description above is correct; but otherwise, it is not
`expr`

but rather it is `(implies govs expr)`

that is added as a new
top-level hypothesis (and whose negation is added as a top-level
hypothesis for the new goal), where `govs`

is the conjunction of the
governors.

If `do-not-flatten-flag`

is supplied and not `nil`

, then that is
all there is to this command. Otherwise (thus this is the default),
when the claimed term (first argument) is a conjunction (`and`

) of
terms and the `claim`

instruction succeeds, then each (nested)
conjunct of the claimed term is added as a separate new top-level
hypothesis. Consider the following example, assuming there are no
governors.

(casesplit (and (and (< x y) (integerp a)) (equal r s)) t)

Three new top-level hypotheses are added to the current goal, namely
`(< x y)`

, `(integerp a)`

, and `(equal r s)`

. In that case, only
one hypothesis is added to create the new goal, namely the negation
of `(and (< x y) (integerp a) (equal r s))`

. If the negation of this
term had been `claim`

ed, then it would be the other way around: the
current goal would get a single new hypothesis while the new goal
would be created by adding three hypotheses.
**Remark:** It is allowed to use abbreviations in the hints.