		Search-engine friendly clone of the ACL2 documentation.

Digits-any-base

Defthm-dab-return-types

Introduce additional return type theorems for the conversions from natural numbers to digits.

Given an equality theorem of the form (equal (dab-digit-listp BASE VAR) TERM<VAR>), where BASE is an integer greater than 1, VAR is a variable, and TERM<VAR> is a term with VAR as the only free variable, this macro generates six theorems of the form TERM<(CONV BASE nat)> or TERM<(CONV BASE width nat)>, where CONV is one of the conversions nat=>bendian*, nat=>bendian+, nat=>bendian, nat=>lendian*, nat=>lendian+, and nat=>lendian, where TERM<(CONV BASE nat)> is the result of replacing VAR with (CONV BASE nat) in TERM<VAR>, and where TERM<(CONV BASE width nat)> is the result of replacing VAR with (CONV BASE width nat) in TERM<VAR> These are additional return type theorems for these conversions.

The name of the equality theorem is the first argument of this macro. The name of each generated return type theorem is PREFIX-CONV, where PREFIX is the second argument of this macro and CONV is the conversion.

The theorems are generated inside a defsection whose topic (name), :parents, :short, and :long are supplied as keyword arguments. If the topic is not supplied, no defsection is generated. If any of :parents, :short, or :long is not supplied, the defsection has no corresponding :parents, :short, or :long.

This macro does not thoroughly validates its inputs. However, its implementation is quite simple, and understanding failures due to incorrect inputs should be easy. Regardless, this macro may be extended to more thoroughly validate its inputs in the future.

Macro: defthm-dab-return-types

(defmacro defthm-dab-return-types
          (eq-thm-name prefix &key (topic 'nil topicp)
                       (parents 'nil parentsp)
                       (short '"" shortp)
                       (long '"" longp))
 (declare (xargs :guard (and (symbolp eq-thm-name)
                             (symbolp prefix)
                             (symbolp topic)
                             (symbol-listp parents)
                             (stringp short)
                             (stringp long))))
 (cons
  'make-event
  (cons
   (cons
    'defthm-dab-return-types-fn
    (cons
     (cons 'quote (cons eq-thm-name 'nil))
     (cons
      (cons 'quote (cons prefix 'nil))
      (cons
       (cons 'quote (cons topic 'nil))
       (cons
        (cons 'quote (cons topicp 'nil))
        (cons
         (cons 'quote (cons parents 'nil))
         (cons
             (cons 'quote (cons parentsp 'nil))
             (cons (cons 'quote (cons short 'nil))
                   (cons (cons 'quote (cons shortp 'nil))
                         (cons (cons 'quote (cons long 'nil))
                               (cons (cons 'quote (cons longp 'nil))
                                     '((w state)))))))))))))
   'nil)))

Subtopics

Defthm-dab-return-types-fn: Event form to introduce additional return type theorems for the conversions from natural numbers to digits.