ihs-lemmas

(in-package "ACL2")

(defxdoc ihs-lemmas
  :parents (ihs)
  :short "A simple interface to the books of lemmas in the IHS libaray."
  :long "<p>Including the @('ihs-lemmas') book includes all of the books of
lemmas in the IHS library.  This book is typically included after the
@('ihs-definitions') book, e.g.,</p>

@({
  (include-book "ihs-definitions")
  (local (include-book "ihs-lemmas"))
})

<p>The above sequence extends the theory that existed before the inclusion of
the books with those definitions and lemmas provided be the included books.</p>

<p>To continue in a minimal theory that contains only the IHS libraries, you
may wish to see @(see minimal-ihs-theory).</p>")

(defsection minimal-ihs-theory
  :parents (ihs-lemmas)
  :short "Set up a minimal theory based on the @(see ihs) library."
  :long "<box><p>Note: Jared recommends against using @('minimal-ihs-theory').
In particular, it invokes @('(in-theory nil)'), which is probably not a good
idea most of the time.</p></box>

<p>Executing the macro call</p>

@({
    (local (minimal-ihs-theory))
})

<p>will set up a minimal theory based on the theories exported by the books in
the IHS libraries.  This is Bishop's preferred way to use the IHS library.</p>

@(def minimal-ihs-theory)"
  (defmacro minimal-ihs-theory
    nil
    '(progn (in-theory nil)
      (in-theory (enable basic-boot-strap
          ihs-math
          quotient-remainder-rules
          logops-lemmas-theory
          integer-range-p)))))