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.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.General Form: 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.
