# Defrule

An enhanced version of defthm.

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

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