		Search-engine friendly clone of the ACL2 documentation.

Std/util

Defthm-signed-byte-p

Prove rules about a term yielding values in signed-byte-p.

Use the macro defthm-signed-byte-p to prove a rewrite rule saying that some term yields a signed-byte-p, a type-prescription corollary saying that the term yields an integerp, and a linear corollary saying that the term yields a value greater than or equal to (- (expt 2 (1- bound))) and less than (expt 2 (1- bound)).

Usage:

(defthm-signed-byte-p <theorem-name>
  :hyp <hypotheses>
  :bound <n>
  :concl <conclusion>
  :hints <usual ACL2 hints for the main theorem>
  :gen-rewrite <t or nil> ;; Make main theorem a :rewrite rule
  :gen-type <t or nil>    ;; Generate :type-prescription corollary
  :gen-linear <t or nil>  ;; Generate :linear corollary
  :hyp-t <hypotheses for the :type-prescription corollary>
  :hyp-l <hypotheses for the :linear corollary>
  :hints-t <usual ACL2 hints for the :type-prescription corollary>
  :hints-l <usual ACL2 hints for the :linear corollary>
  :otf-flg <t or nil>)

The above form produces a theorem of the following form (if both :gen-type and :gen-linear are t and :gen-rewrite is t or unsupplied):

(defthm <theorem-name>
  (implies <hypotheses>
           (signed-byte-p <n> <conclusion>))
  :hints <usual ACL2 hints for the main theorem>
  :otf-flg <t or nil>
  :rule-classes
  (:rewrite
   (:type-prescription
    :corollary
    (implies <hypotheses for the :type-prescription corollary>
             (integerp <conclusion>))
    :hints <usual ACL2 hints for the :type-prescription corollary>)
   (:linear
    :corollary
    (implies <hypotheses for the :linear corollary>
             (and (<= (- (expt 2 (1- <n>)) <conclusion>))
                  (< <conclusion> (expt 2 (1- <n>)))))
    :hints <usual ACL2 hints for the :linear corollary>)))

If :hints-t is not supplied, hints to prove the type prescription corollary are generated automatically. In this case, the hypotheses for the type prescription corollary must trivially subsume the ones for the main theorem specified by :hyp; in particular, they may have additional conjuncts or additional calls to force. Analogous remarks apply to :hints-l.

Also see the related macros defthm-natp and defthm-unsigned-byte-p.