• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
    • Theories
    • Rule-classes
    • Proof-builder
    • Recursion-and-induction
    • Hons-and-memoization
    • Events
    • Parallelism
    • History
    • Programming
    • Operational-semantics
    • Real
    • Start-here
    • Debugging
    • Miscellaneous
      • Term
      • Ld
      • Hints
      • Type-set
      • Ordinals
      • Clause
      • ACL2-customization
      • With-prover-step-limit
      • Set-prover-step-limit
      • With-prover-time-limit
      • Local-incompatibility
      • Set-case-split-limitations
      • Subversive-recursions
      • Specious-simplification
      • Defsum
      • Gcl
      • Oracle-timelimit
      • Thm
      • Defopener
      • Case-split-limitations
      • Set-gc-strategy
      • Default-defun-mode
      • Top-level
      • Reader
      • Ttags-seen
      • Adviser
      • Ttree
      • Abort-soft
      • Defsums
      • Gc$
      • With-timeout
      • Coi-debug::fail
      • Expander
        • Defthm?
        • Symsim
      • Gc-strategy
      • Coi-debug::assert
      • Sin-cos
      • Def::doc
      • Syntax
      • Subversive-inductions
    • Output-controls
    • Macros
    • Interfacing-tools
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Expander

Symsim

Simplify given term and hypotheses.

Example:

(symsim (append x y)
        ((not (atom x)) (not (cdr x)))
        :hints (("Goal" :expand
                 ((true-listp x)
                  (true-listp (cdr x))
                  (append x y)))))

yields

Simplified term:
  (CONS (CAR X) Y)
Simplified hyps:
 ((CONSP X) (NOT (CDR X)))~/

General Form:
(symsim term hyps
        :hints             hints
        :inhibit-output    inhibit-flg ; t, :prove, :all, or nil, default t
        :prove-assumptions prove-flg   ; t, nil, or (default) any other value
        :print-flg         print-flg   ; t or nil, default nil
        :simplify-hyps-p   flg         ; t, nil, or :no-split; default t
)

where term is a term to be simplified assuming that each hyp in the list hyps is true, and hints is as described in its documentation. The keyword arguments above are all optional, and behave as you might expect. In particular, set :simplify-hyps-p to nil if you do not want the hyps to be simplified; otherwise, case splitting may occur in the course of their simplification.

Prover output is inhibited if :inhibit-output is t (the default). Only proof output is inhibited if :inhibit-output is :prove (so for example, summaries and warnings are printed), and all prover output is shown or inhibited if :inhibit-output is nil or :all, respectively.

See rewrite$ for a flexible, convenient interface to the ACL2 rewriter that can be called programmatically. Also see defthm?, which is related to symsim and is a bit more thoroughly documented. Here are some examples that should help give an idea of how symsim works. (The name, by the way, is short for "symbolically simulate".) Try these, as well as the examples shown above.

(symsim (append x y)
        nil
        :hints (("Goal" :expand
                 ((true-listp x)
                  (append x y)
                  (append (cdr x) y)))))

; Generates three cases:
(symsim (append x y)
        ((true-listp x))
        :hints (("Goal" :expand
                 ((true-listp x)
                  (true-listp (cdr x))
                  (append x y)
                  (append (cdr x) y)))))

; Let's illustrate the role of FORCE.  The following rule
; forces append to open up, and comes into play below.
(defthm true-listp-expand-append
  (implies (and (force (true-listp x))
                x)
           (equal (append x y)
                  (cons (car x) (append (cdr x) y)))))

; Generates assumption forced by preceding rule.
(symsim (append x y)
        ((not (atom x))))

; But now we fail; but why?  See next form.
(symsim (append x y)
        ((consp x))
        :prove-assumptions t)

; Let's not inhibit output.  Then we can see the failed forcing round.
(symsim (append x y)
        ((consp x))
        :prove-assumptions t
        :inhibit-output nil)

; As above, but doesn't deal with generated forced assumptions at all (just
; drops them on the floor).
(symsim (append x y)
        ((consp x))
        :prove-assumptions nil)