		Search-engine friendly clone of the ACL2 documentation.

Std/util

Defthm-natp

Prove rules about a term yielding values in natp.

Use the macro defthm-natp to prove a rewrite rule saying that some term yields a natp, a type-prescription corollary saying that the term yields a natp, and a linear corollary saying that the term yields a value greater than or equal to zero.

Usage:

(defthm-natp <theorem-name>
  :hyp <hypotheses>
  :concl <conclusion>
  :hints <usual ACL2 hints for the main theorem>)
  :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 form (if both :gen-type and :gen-linear are t):

(defthm <theorem-name>
  (implies <hypotheses>
           (natp <conclusion>))
  :hints <usual ACL2 hints>
  :otf-flg <t or nil>
  :rule-classes
  (:rewrite
   (:type-prescription
    :corollary
    (implies <hypotheses>
             (natp <conclusion>))
    :hints <usual ACL2 hints for the :type-prescription corollary>)
   (:linear
    :corollary
    (implies <hypotheses>
             (<= 0 <conclusion>))
    :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-unsigned-byte-p and defthm-signed-byte-p.