An enhanced version of defthm.
(encapsulate () (local (in-theory (e/d ...))) (defthm ...))with ACL2::rulesets integration.
You can give
(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
Theory hints are especially common.
One option is to just give a top-level
As an alternative,
Another option is to provide a non-
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
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
(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)))