• 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

Defthm?

Generate a theorem.

Example:

(defthm? app-simplify
  (implies (true-listp x)
           (equal (append x y)
                  ?))
  :hints (("Goal" :expand ((true-listp x)
                           (true-listp (cdr x))
                           (append x y))))
  ; show some output
  :print-flg t)

General Forms:

(DEFTHM? name
  (IMPLIES hyps (equiv term ?))
  :hints             hints
  :prove-assumptions prove-flg ; t or nil, default t
  :print-flg         print-flg ; t or nil, default nil
  :simplify-hyps-p   flg       ; t, nil, or :no-split; default t
)

(DEFTHM? name
  (equiv term ?)
  :hints             hints
  :prove-assumptions prove-flg ; t or nil, default t
  :print-flg         print-flg ; t or nil, default nil
  :simplify-hyps-p   flg       ; t, nil, or :no-split; default t
)

where name is a new symbolic name (see name), term is a term to be simplified assuming hyps is true, and hints is as described in its documentation. The four 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.

If the given term cannot be simplified, then the event fails. Otherwise, the result is an encapsulate event with one or more defthm events of the form of the theorem, except with hyps simplified (and even omitted if simplified to t) and term simplified under the assumption that hyps is true. The reason that there can be more than one defthm event is that hyps may simplify to an expression that generates a case split, for example if it simplifies to an if expression that does not represent a conjunction.

In general, simplification may generate assumptions because of force. By default, an attempt is made to prove these assumptions, which must succeed or else this event fails. However, if :prove-assumptions is nil, then roughly speaking, no proof of forced hypotheses is attempted until after simplification is complete. The documentation of :prove-assumptions is admittedly weak here; feel free to experiment.

See rewrite$ for a flexible, convenient interface to the ACL2 rewriter that can be called programmatically. Also see symsim.

Here are some examples, including the one above. Try them out and see what happens.

; Doesn't simplify, so fails:
(defthm? app-simplify
  (implies (true-listp x)
           (equal (append x y)
                  ?))
  :hints (("Goal" :expand (true-listp x))))

:pbt 0

; The following creates one event, but maybe we'd prefer cases to be
; broken out into separate events.  That comes next.
(defthm? app-simplify
  (implies (true-listp x)
           (equal (append x y)
                  ?))
  :hints (("Goal" :expand (append x y))))

:pbt 0
:pe :here
:pe APP-SIMPLIFY
:u

(defthm? app-simplify
  (implies (true-listp x)
           (equal (append x y)
                  ?))
  :hints (("Goal" :expand ((true-listp x)
                           (true-listp (cdr x))
                           (append x y))))
  ; show some extra output; this is optional
  :print-flg t)

:pe :here
:u