Filtering...

defthmr

books/kestrel/utilities/defthmr

Included Books

top
other
(in-package "ACL2")
include-book
(include-book "xdoc/top" :dir :system)
other
(defxdoc defthmr
  :parents (defthm events kestrel-utilities)
  :short "Submit a theorem, as a @(see rewrite) rule only if possible."
  :long "<p>@('Defthmr') stands for ``defthm rule''.  It is a macro that is
 intended to be equivalent to @(tsee defthm) &mdash; in particular, it takes
 the same arguments as @('defthm') &mdash; but when necessary it avoids the
 default of @(':rule-classes :rewrite').  Here we also document @('defthmdr'),
 which is similar to @('defthmr') but when a rewrite rule is created, it is
 immediately disabled; thus @('defthmdr') is to @('defthmd') as @('defthmr') is
 to @('defthm').</p>

 @({
 Examples:

 (defthmr symbol-name-abc
   (equal (symbol-name 'abc) "ABC"))

 (defthmdr symbol-name-intern$-acl2
   (equal (symbol-name (intern$ name "ACL2")) name))

 General Forms:

 (defthmr  name term ...) ; same keyword arguments accepted as for defthm
 (defthmdr name term ...) ; same keyword arguments accepted as for defthm
 })

 <p>In the first example above, the use of @('defthm') would cause an
 error:</p>

 @({
 ACL2 !>(defthm symbol-name-abc
          (equal (symbol-name 'abc) "ABC"))


 ACL2 Error in ( DEFTHM SYMBOL-NAME-ABC ...):  A :REWRITE rule generated
 from SYMBOL-NAME-ABC is illegal because it rewrites the term 'T to
 itself! ....
 })

 <p>The problem is that the internal form for the term @('(equal (symbol-name
 'abc) "ABC")') is, perhaps surprisingly, @(''T').  The reason is that ACL2
 evaluates calls of undefined primitives, such as @(tsee symbol-name) and
 @(tsee equal), when translating to internal form.</p>

 <p>@('Defthmr') and @('defthmdr') avoid this problem by adding
 @(':rule-classes nil') in such cases.  The two examples above thus generate
 the following events.  In the first example, the addition of @(':rule-classes nil')
 avoids the error discussed above, by instructing ACL2 to avoid the default
 behavior of attempting to store the theorem as a @(see rewrite) rule.  The
 second example has no such problem (because of the variable, @('name')), so
 ACL2 treats that @('defthmdr') simply as @('defthmd').</p>

 @({
 (defthm symbol-name-abc
   (equal (symbol-name 'abc) "ABC")
   :rule-classes nil)

 (defthmd symbol-name-intern$-acl2
   (equal (symbol-name (intern$ name "ACL2")) name))
 })

 <p>Note that if a @(':rule-classes') keyword argument is supplied, then the
 given call of @('defthmr') or @('defthmdr') simply expands directly to the
 corresponding call of @('defthm') or @('defthmd'), respectively.</p>")
other
(defpointer defthmdr defthmr)
other
(program)
other
(set-state-ok t)
defthmr-fnfunction
(defun defthmr-fn
  (name term args disabledp ctx state)
  (let ((wrld (w state)))
    (mv-let (erp tterm state)
      (translate term t t t ctx wrld state)
      (cond (erp (mv (msg "An ill-formed term was submitted to ~x0 (see message ~
                      above)."
              (if disabledp
                'defthmdr
                'defthmr))
            nil
            state))
        (t (state-global-let* ((inhibit-output-lst *valid-output-names*))
            (mv-let (erp val state)
              (chk-acceptable-rewrite-rule nil
                name
                nil
                nil
                tterm
                ctx
                (ens state)
                (w state)
                state)
              (declare (ignore val))
              (cond (erp (value `(defthm ,NAME ,TERM ,@ARGS :rule-classes nil)))
                (t (let ((deft (if disabledp
                         'defthmd
                         'defthm)))
                    (value `(,DEFT ,NAME ,TERM ,@ARGS))))))))))))
defthmrmacro
(defmacro defthmr
  (name term
    &rest
    args
    &key
    (rule-classes 'nil rule-classes-p)
    instructions
    hints
    otf-flg)
  (declare (ignore rule-classes instructions hints otf-flg))
  (cond (rule-classes-p `(defthm ,NAME ,TERM ,@ARGS))
    (t `(make-event (defthmr-fn ',NAME
          ',TERM
          ',ARGS
          nil
          '(defthmr . ,NAME)
          state)))))
defthmdrmacro
(defmacro defthmdr
  (name term
    &rest
    args
    &key
    rule-classes
    instructions
    hints
    otf-flg)
  (declare (ignore instructions hints otf-flg))
  (cond (rule-classes `(defthmd ,NAME ,TERM ,@ARGS))
    (t `(make-event (defthmr-fn ',NAME ',TERM ',ARGS t '(defthmr . ,NAME) state)))))
other
(table ppr-special-syms 'defthmr 1)
other
(table ppr-special-syms 'defthmdr 1)
other
(logic)
local
(local (progn (defthmr symbol-name-abc (equal (symbol-name 'abc) "ABC"))
    (defthmr app-assoc
      (equal (append (append x y) z) (append x y z)))
    (defthmr integerp-0 (integerp 0))
    (defthmr integerp-0-explicit-rule-classes-nil
      (integerp 0)
      :rule-classes nil)
    (defthmdr car-append
      (equal (car (append x y))
        (if (consp x)
          (car x)
          (car y))))
    (defthmdr integerp-0-alt (integerp 0) :otf-flg t)))