		Search-engine friendly clone of the ACL2 documentation.

Std/util

Defrule

An enhanced version of defthm.

defrule is a drop-in replacement for defthm that adds:

A more concise syntax for ACL2::hints that target "Goal".

A very concise syntax for

(encapsulate ()
  (local (in-theory (e/d ...)))
  (defthm ...))

with ACL2::rulesets integration.

Integration with xdoc. You can give :parents, :short, and :long documentation right at the top level of the defrule.
The ability to make the theorem local.
The ability to provide lemmas and include books in support of the theorem's proof.

Top-level Hints

You can give "Goal" hints directly at the top level of the rule. For example:

(defrule repeated-insert           -->  (defthm repeated-insert
  (equal (insert a (insert a X))          (equal (insert a (insert a X))
         (insert a X))                           (insert a X))
  :induct t                               :hints(("Goal"
  :expand ((...)))                                :induct t
                                                  :expand ((...))))

This works for any hint except for :instructions. If you give top-level hints and a "Goal" hint, the top-level hints will be appended onto the front of the explicit "Goal" hint.

Theory Support

Theory hints are especially common.

One option is to just give a top-level :in-theory hint, and it just gets attached to goal. But note that such hints are not inherited when you give an in-theory hint in a subgoal. This can be quite confusing and annoying.

As an alternative, defrule also adds top-level :enable, :disable, and :e/d options. When you use these keywords, they turn into a local theory event that is submitted before your defthm. That way, they're part of the theory that is inherited by all subgoals.

To make :enable, :disable, and :e/d slightly more powerful, they are actually integrated with the ACL2::rulesets book. In particular, these keywords are always translated into an ACL2::e/d*.

Support for Local

Another option is to provide a non-nil value to the keyword argument :local. This results in surrounding the rule with a local.

Supporting Lemmas and Books

We often write lemmas in support of one larger theorem. In this case, you can provide these lemmas as a list of events with the :prep-lemmas argument. Despite the name, it is also possible to include function definitions with the :prep-lemmas keyword; for instance, when a recursive function is needed to serve as an induction scheme. Note that including a book via :prep-lemmas does not work.

To include a book or many books for use in the main theorem you are proving, supply a list of include-book commands with the :prep-books argument.

Some examples:

(defrule foo            -->  (encapsulate ()
   ...                         (local (in-theory (e/d* (append) (revappend))))
   :enable append              (defthm foo ...))
   :disable revappend)

(defrule bar            -->  (encapsulate ()
   ...                         (local (in-theory (e/d* (append rev)
   :enable (append rev)                                revappend
   :disable revappend                                  (logior)
   :e/d ((logior) (logand)))                           (logand)))
                               (defthm bar ...))

(defrule baz            -->  (local
    ...                        (encapsulate ()
    :local t)                    (defthm baz ...)))

(defrule lets-loop                  --> (defsection lets-loop
  (equal (+ x y)                          (local
         (+ y x))                          (encapsulate ()
                                            (defrule pretend-we-need-this
  :prep-lemmas                                ...)
  ((defrule pretend-we-need-this            (defrule pretend-we-need-this-too
     ...)                                     ...)))
   (defrule pretend-we-need-this-too        (local (progn (include-book
     ...))                                                "arithmetic/top"
                                                          :dir :system)))
  :prep-books                             (defthm lets-loop (equal (+ x y) (+ y x))
    ((include-book "arithmetic/top"             ...))
    :dir :system)))

Subtopics

Rule: A thm-like version of defrule.
Defruledl: Variant of defrule that disables the theorem afterwards and makes it local.
Defruled: Variant of defrule that disables the theorem afterwards.
Defrulel: Variant of defrule that makes the theorem local.