ACL2-PC::SPLIT

(atomic macro) split the current goal into cases
Major Section:  PROOF-CHECKER-COMMANDS

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.

Note: 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 *s-prop-theory*. However, because the prover is called, type-set 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.