		Search-engine friendly clone of the ACL2 documentation.

Integer-formats

Char+short+int+long+llong+bool-format-wfp

Check if the formats of char, short, int, long, long long, and _Bool objects are well-formed.

Signature
(char+short+int+long+llong+bool-format-wfp format) → yes/no
Arguments: format — Guard (char+short+int+long+llong+bool-formatp format).
Returns: yes/no — Type (booleanp yes/no).

The formats for char objects already include their own well-formedness in their definition. We impose well-formedness on the other formats.

Definitions and Theorems

Function: char+short+int+long+llong+bool-format-wfp

(defun char+short+int+long+llong+bool-format-wfp (format)
 (declare
     (xargs :guard (char+short+int+long+llong+bool-formatp format)))
 (b* (((char+short+int+long+llong+bool-format format)
       format))
  (and
   (integer-format-short-wfp format.short format.uchar format.schar)
   (integer-format-int-wfp format.int format.uchar format.short)
   (integer-format-long-wfp format.long format.uchar format.int)
   (integer-format-llong-wfp format.llong format.uchar format.long)
   (bool-format-wfp format.bool format.uchar))))

Theorem: booleanp-of-char+short+int+long+llong+bool-format-wfp

(defthm booleanp-of-char+short+int+long+llong+bool-format-wfp
  (b* ((yes/no (char+short+int+long+llong+bool-format-wfp format)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Theorem: char+short+int+long+llong+bool-format-wf-short-bit-size-lower-bound

(defthm
 char+short+int+long+llong+bool-format-wf-short-bit-size-lower-bound
 (implies
     (char+short+int+long+llong+bool-format-wfp format)
     (>= (integer-format->bit-size
              (char+short+int+long+llong+bool-format->short format))
         16))
 :rule-classes :linear)

Theorem: char+short+int+long+llong+bool-format-wf-int-bit-size-lower-bound

(defthm
  char+short+int+long+llong+bool-format-wf-int-bit-size-lower-bound
  (implies
       (char+short+int+long+llong+bool-format-wfp format)
       (>= (integer-format->bit-size
                (char+short+int+long+llong+bool-format->int format))
           16))
  :rule-classes :linear)

Theorem: char+short+int+long+llong+bool-format-wf-long-bit-size-lower-bound

(defthm
 char+short+int+long+llong+bool-format-wf-long-bit-size-lower-bound
 (implies
      (char+short+int+long+llong+bool-format-wfp format)
      (>= (integer-format->bit-size
               (char+short+int+long+llong+bool-format->long format))
          32))
 :rule-classes :linear)

Theorem: char+short+int+long+llong+bool-format-wf-llong-bit-size-lower-bound

(defthm
 char+short+int+long+llong+bool-format-wf-llong-bit-size-lower-bound
 (implies
     (char+short+int+long+llong+bool-format-wfp format)
     (>= (integer-format->bit-size
              (char+short+int+long+llong+bool-format->llong format))
         64))
 :rule-classes :linear)

Theorem: char+short+int+long+llong+bool-format-wfp-of-char+short+int+long+llong+bool-format-fix-format

(defthm
 char+short+int+long+llong+bool-format-wfp-of-char+short+int+long+llong+bool-format-fix-format
 (equal (char+short+int+long+llong+bool-format-wfp
             (char+short+int+long+llong+bool-format-fix format))
        (char+short+int+long+llong+bool-format-wfp format)))

Theorem: char+short+int+long+llong+bool-format-wfp-char+short+int+long+llong+bool-format-equiv-congruence-on-format

(defthm
 char+short+int+long+llong+bool-format-wfp-char+short+int+long+llong+bool-format-equiv-congruence-on-format
 (implies
   (char+short+int+long+llong+bool-format-equiv format format-equiv)
   (equal (char+short+int+long+llong+bool-format-wfp format)
          (char+short+int+long+llong+bool-format-wfp format-equiv)))
 :rule-classes :congruence)