ACL2-pc::casesplit
(primitive)
split into two cases
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. Also see ACL2-pc::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 ACL2-pc::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
claimed, 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.
