ACL2-pc::split
(atomic macro)
split the current goal into cases
Example:
split
For example, if the current goal has one hypothesis (or x y) and a
conclusion of (and a b), then split will create four new goals:
one with hypothesis X and conclusion A
one with hypothesis X and conclusion B
one with hypothesis Y and conclusion A
one with hypothesis Y and conclusion B.
General Form:
SPLIT
Replace the current goal by subgoals whose conjunction is equivalent
(primarily by propositional reasoning) to the original goal, where each such
goal cannot be similarly split.
Remark: The new goals will all have their hypotheses promoted; in
particular, no conclusion will have a top function symbol of implies.
Also note that split will fail if there is exactly one new goal created
and it is the same as the existing current goal.
The way split really works is to call the ACL2 theorem prover with
only simplification (and preprocessing) turned on, and with only a few
built-in functions (especially, propositional ones) enabled, namely, the ones
in the list (theory 'minimal-theory). However, because the prover is
called, type-reasoning can be used to eliminate some cases. For
example, if (true-listp x) is in the hypotheses, then probably
(true-listp (cdr x)) will be reduced to t.
