• Top
  • Documentation
  • Books
  • Recursion-and-induction
  • Boolean-reasoning
  • Debugging
  • Projects
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
    • Theories
    • Rule-classes
    • Proof-builder
    • Hons-and-memoization
    • Events
    • History
    • Parallelism
    • Programming
      • Defun
      • Declare
      • System-utilities
      • Stobj
      • State
        • World
          • Logical-name
          • Formula
          • Redefined-names
          • Retract-world
          • Extend-world
          • Getprop
          • Getpropc
          • Putprop
          • Props
        • Io
        • Wormhole
        • Programming-with-state
        • W
        • Set-state-ok
        • Random$
      • Memoize
      • Mbe
      • Io
      • Defpkg
      • Apply$
      • Mutual-recursion
      • Loop$
      • Programming-with-state
      • Arrays
      • Characters
      • Time$
      • Loop$-primer
      • Fast-alists
      • Defmacro
      • Defconst
      • Evaluation
      • Guard
      • Equality-variants
      • Compilation
      • Hons
      • ACL2-built-ins
      • Developers-guide
      • System-attachments
      • Advanced-features
      • Set-check-invariant-risk
      • Numbers
      • Irrelevant-formals
      • Efficiency
      • Introduction-to-programming-in-ACL2-for-those-who-know-lisp
      • Redefining-programs
      • Lists
      • Invariant-risk
      • Errors
      • Defabbrev
      • Conses
      • Alists
      • Set-register-invariant-risk
      • Strings
      • Program-wrapper
      • Get-internal-time
      • Basics
      • Packages
      • Defmacro-untouchable
      • Primitive
      • <<
      • Revert-world
      • Set-duplicate-keys-action
      • Unmemoize
      • Symbols
      • Def-list-constructor
      • Easy-simplify-term
      • Defiteration
      • Defopen
      • Sleep
    • Start-here
    • Real
    • Debugging
    • Miscellaneous
    • Output-controls
    • Macros
    • Interfacing-tools
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Testing-utilities
  • Math

• History
• World
• ACL2-built-ins

Formula

The formula of a name or rune

The ACL2 system function, formula, returns the term associated with a given rune or symbolic name, returning nil if there is no such term. Note that a non-nil result will be an ACL2 ``translated'' term (see term). Most ACL2 users probably will have no reason to know about this function. But here we document this function for those who write system-level tools, since they might find this interface to the ACL2 logical world to be useful.

When ACL2 is given a :use or :by hint, it looks for the term stored in the ACL2 logical world that is associated with the name given in the hint, which is a symbol or a rune. (See lemma-instance.) The utility used to find that term is formula, which ACL2 invokes as follows.

(formula x t wrld)   ; for :use hints
(formula x nil wrld) ; for :by hints

The second argument can affect whether or not to use a normalized version of the term (in particular, a definition body) associated with x; see normalize. The value is t for :use hints because normalizing a term simplifies it, which is often desirable. But for a :by hint, the non-normalized version of the term is used in order to increase the chance that the necessary subsumption test will succeed. Even if the second argument is t, normalization might not take place. In the unlikely case that you need to know more precisely the effect of supplying t, see the source code for formula.

Here are some examples. Note that (w state) returns the current ACL2 logical world. First let us submit a few events.

(defun f1 (x) (cons 3 x))
(defun f2 (x y) (implies x y))
(defthm one-rule
  (and (equal (* 2 y) (+ y y))
       (equal (* 3 y) (+ y y y))))
(defthm two-rules
  t
  :rule-classes ((:rewrite :corollary (equal (* 2 y) (+ y y)))
                 (:rewrite :corollary (equal (* 3 y) (+ y y y)))))

Then:

ACL2 !>(formula 'f1 nil (w state))
(EQUAL (F1 X) (CONS '3 X))
ACL2 !>(formula 'f1 t (w state))
(EQUAL (F1 X) (CONS '3 X))
ACL2 !>(formula 'f2 nil (w state))
(EQUAL (F2 X Y) (IMPLIES X Y))
ACL2 !>(formula 'f2 t (w state))
(EQUAL (F2 X Y)
       (IF X (IF Y 'T 'NIL) 'T))
ACL2 !>(formula 'one-rule nil (w state))
(IF (EQUAL (BINARY-* '2 Y) (BINARY-+ Y Y))
    (EQUAL (BINARY-* '3 Y)
           (BINARY-+ Y (BINARY-+ Y Y)))
    'NIL)
ACL2 !>(equal (formula 'one-rule nil (w state)) (formula 'one-rule t (w state)))
T
ACL2 !>(formula 'two-rules nil (w state))
'T
ACL2 !>(formula 'two-rules t (w state))
'T
ACL2 !>(formula '(:rewrite two-rules . 1) nil (w state))
(EQUAL (BINARY-* '2 Y) (BINARY-+ Y Y))
ACL2 !>(formula '(:rewrite two-rules . 2) nil (w state))
(EQUAL (BINARY-* '3 Y)
       (BINARY-+ Y (BINARY-+ Y Y)))
ACL2 !>(formula 'no-such-rule nil (w state))
NIL
ACL2 !>