To disallow forced case-splits
ACL2 !>:disable-forcing ; disallow forced case splits
See force and see case-split for a discussion of forced case
splits, which are inhibited by this command.
Disable-forcing is actually a macro that disables the executable-counterpart of the function symbol force; see force.
When you want to use hints to turn off forced case splits, use a form
such as one of the following (these are equivalent).
:in-theory (disable (:executable-counterpart force))
:in-theory (disable (force))
The following example shows how this works. First evaluate these
(defstub f1 (x) t)
(defstub f2 (x) t)
(defaxiom ax (implies (case-split (f2 x)) (f1 x)))
(thm (f1 x))
You will see the application of the rule, ax, in the proof of the
thm call above. However, if you first evaluate
(disable-forcing), then there will be no application of ax. To
restore forced case splitting, see enable-forcing.