maybe-defthm - ACL2 Book

other

(in-package "STD")

other

(include-book "std/util/bstar" :dir :system)

maybe-defthm-as-rewritemacro

(defmacro maybe-defthm-as-rewrite
  (name concl &key hints)
  "Concl must be a HYP-FREE and already TRANSLATED term"
  `(make-event (b* ((name ',STD::NAME) (concl ',STD::CONCL)
        (hints ',STD::HINTS)
        ((unless (pseudo-termp concl)) (er hard?
            'maybe-defthm-as-rewrite
            "Expected concl to be a translated term, but got ~x0"
            concl)
          (value '(value-triple :error)))
        (thm `(defthm ,STD::NAME ,STD::CONCL :hints ,STD::HINTS))
        (ens (ens state))
        (wrld (w state))
        ((mv msg
           ?eqv
           ?lhs0
           ?lhs
           ?rhs
           ?ttree) (interpret-term-as-rewrite-rule nil
            name
            nil
            (remove-guard-holders concl wrld)
            nil
            ens
            wrld))
        ((when msg) (value '(value-triple :invisible))))
      (value thm))))

is-theorem-pfunction

(defun is-theorem-p
  (name world)
  (declare (xargs :mode :program))
  (fgetprop name 'theorem nil world))

enable-if-theoremmacro

(defmacro enable-if-theorem
  (name)
  `(make-event (let ((name ',STD::NAME))
      (if (is-theorem-p name (w state))
        (value `(in-theory (enable ,STD::NAME)))
        (value `(value-triple :invisible))))))

disable-if-theoremmacro

(defmacro disable-if-theorem
  (name)
  `(make-event (let ((name ',STD::NAME))
      (if (is-theorem-p name (w state))
        (value `(in-theory (disable ,STD::NAME)))
        (value `(value-triple :invisible))))))