• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
    • Theories
    • Rule-classes
      • Type-prescription
      • Rewrite
      • Meta
      • Linear
      • Definition
        • Force
          • Forcing-round
          • Failed-forcing
          • Immediate-force-modep
          • Disable-forcing
          • Enable-forcing
          • Disable-immediate-force-modep
          • Enable-immediate-force-modep
        • Syntaxp
        • Bind-free
        • Case-split
        • Simple
        • Set-body
        • Show-bodies
      • Clause-processor
      • Tau-system
      • Forward-chaining
      • Equivalence
      • Congruence
      • Free-variables
      • Executable-counterpart
      • Induction
      • Type-reasoning
      • Compound-recognizer
      • Rewrite-quoted-constant
      • Elim
      • Well-founded-relation-rule
      • Built-in-clause
      • Well-formedness-guarantee
      • Patterned-congruence
      • Rule-classes-introduction
      • Guard-holders
      • Refinement
      • Type-set-inverter
      • Generalize
      • Corollary
      • Induction-heuristics
      • Backchaining
      • Default-backchain-limit
    • Proof-builder
    • Recursion-and-induction
    • Hons-and-memoization
    • Events
    • Parallelism
    • History
    • Programming
    • Operational-semantics
    • Real
    • Start-here
    • Debugging
    • Miscellaneous
    • Output-controls
    • Macros
    • Interfacing-tools
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Force

Disable-forcing

To disallow forced case-splits

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

(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.