split the current goal into cases
Major Section: PROOF-CHECKER-COMMANDS
Example: splitFor 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: SPLITReplace 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-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.
