		Search-engine friendly clone of the ACL2 documentation.

Bitops/merge

Merge-8-bits

Concatenate 8 bits together to form an 8-bit natural.

Signature
(merge-8-bits a7 a6 a5 a4 a3 a2 a1 a0) → result
Arguments: a7 — Guard (bitp a7).; a6 — Guard (bitp a6).; a5 — Guard (bitp a5).; a4 — Guard (bitp a4).; a3 — Guard (bitp a3).; a2 — Guard (bitp a2).; a1 — Guard (bitp a1).; a0 — Guard (bitp a0).
Returns: result — Type (natp result).

Definitions and Theorems

Function: merge-8-bits$inline

(defun acl2::merge-8-bits$inline (a7 a6 a5 a4 a3 a2 a1 a0)
  (declare (xargs :guard (and (bitp a7)
                              (bitp a6)
                              (bitp a5)
                              (bitp a4)
                              (bitp a3)
                              (bitp a2)
                              (bitp a1)
                              (bitp a0))))
  (declare (type bit a7 a6 a5 a4 a3 a2 a1 a0))
  (declare (xargs :split-types t))
  (let ((__function__ 'merge-8-bits))
    (declare (ignorable __function__))
    (mbe :logic
         (logapp* 1 (bfix a0)
                  (bfix a1)
                  (bfix a2)
                  (bfix a3)
                  (bfix a4)
                  (bfix a5)
                  (bfix a6)
                  (bfix a7)
                  0)
         :exec
         (b* ((ans a0)
              (ans (the (unsigned-byte 8)
                        (logior (the (unsigned-byte 8) (ash a1 1))
                                (the (unsigned-byte 8) ans))))
              (ans (the (unsigned-byte 8)
                        (logior (the (unsigned-byte 8) (ash a2 2))
                                (the (unsigned-byte 8) ans))))
              (ans (the (unsigned-byte 8)
                        (logior (the (unsigned-byte 8) (ash a3 3))
                                (the (unsigned-byte 8) ans))))
              (ans (the (unsigned-byte 8)
                        (logior (the (unsigned-byte 8) (ash a4 4))
                                (the (unsigned-byte 8) ans))))
              (ans (the (unsigned-byte 8)
                        (logior (the (unsigned-byte 8) (ash a5 5))
                                (the (unsigned-byte 8) ans))))
              (ans (the (unsigned-byte 8)
                        (logior (the (unsigned-byte 8) (ash a6 6))
                                (the (unsigned-byte 8) ans)))))
           (the (unsigned-byte 8)
                (logior (the (unsigned-byte 8) (ash a7 7))
                        (the (unsigned-byte 8) ans)))))))

Theorem: natp-of-merge-8-bits

(defthm acl2::natp-of-merge-8-bits
  (b* ((result (acl2::merge-8-bits$inline a7 a6 a5 a4 a3 a2 a1 a0)))
    (natp result))
  :rule-classes :type-prescription)

Theorem: unsigned-byte-p-8-of-merge-8-bits

(defthm unsigned-byte-p-8-of-merge-8-bits
  (unsigned-byte-p 8
                   (merge-8-bits a7 a6 a5 a4 a3 a2 a1 a0)))

Theorem: merge-8-bits-is-merge-unsigneds

(defthm merge-8-bits-is-merge-unsigneds
  (equal (merge-8-bits a7 a6 a5 a4 a3 a2 a1 a0)
         (merge-unsigneds 1
                          (list (bfix a7)
                                (bfix a6)
                                (bfix a5)
                                (bfix a4)
                                (bfix a3)
                                (bfix a2)
                                (bfix a1)
                                (bfix a0)))))

Basic bit-equiv congruences.

Theorem: bit-equiv-implies-equal-merge-8-bits-8

(defthm bit-equiv-implies-equal-merge-8-bits-8
  (implies (bit-equiv a0 a0-equiv)
           (equal (merge-8-bits a7 a6 a5 a4 a3 a2 a1 a0)
                  (merge-8-bits a7 a6 a5 a4 a3 a2 a1 a0-equiv)))
  :rule-classes (:congruence))

Theorem: bit-equiv-implies-equal-merge-8-bits-7

(defthm bit-equiv-implies-equal-merge-8-bits-7
  (implies (bit-equiv a1 a1-equiv)
           (equal (merge-8-bits a7 a6 a5 a4 a3 a2 a1 a0)
                  (merge-8-bits a7 a6 a5 a4 a3 a2 a1-equiv a0)))
  :rule-classes (:congruence))

Theorem: bit-equiv-implies-equal-merge-8-bits-6

(defthm bit-equiv-implies-equal-merge-8-bits-6
  (implies (bit-equiv a2 a2-equiv)
           (equal (merge-8-bits a7 a6 a5 a4 a3 a2 a1 a0)
                  (merge-8-bits a7 a6 a5 a4 a3 a2-equiv a1 a0)))
  :rule-classes (:congruence))

Theorem: bit-equiv-implies-equal-merge-8-bits-5

(defthm bit-equiv-implies-equal-merge-8-bits-5
  (implies (bit-equiv a3 a3-equiv)
           (equal (merge-8-bits a7 a6 a5 a4 a3 a2 a1 a0)
                  (merge-8-bits a7 a6 a5 a4 a3-equiv a2 a1 a0)))
  :rule-classes (:congruence))

Theorem: bit-equiv-implies-equal-merge-8-bits-4

(defthm bit-equiv-implies-equal-merge-8-bits-4
  (implies (bit-equiv a4 a4-equiv)
           (equal (merge-8-bits a7 a6 a5 a4 a3 a2 a1 a0)
                  (merge-8-bits a7 a6 a5 a4-equiv a3 a2 a1 a0)))
  :rule-classes (:congruence))

Theorem: bit-equiv-implies-equal-merge-8-bits-3

(defthm bit-equiv-implies-equal-merge-8-bits-3
  (implies (bit-equiv a5 a5-equiv)
           (equal (merge-8-bits a7 a6 a5 a4 a3 a2 a1 a0)
                  (merge-8-bits a7 a6 a5-equiv a4 a3 a2 a1 a0)))
  :rule-classes (:congruence))

Theorem: bit-equiv-implies-equal-merge-8-bits-2

(defthm bit-equiv-implies-equal-merge-8-bits-2
  (implies (bit-equiv a6 a6-equiv)
           (equal (merge-8-bits a7 a6 a5 a4 a3 a2 a1 a0)
                  (merge-8-bits a7 a6-equiv a5 a4 a3 a2 a1 a0)))
  :rule-classes (:congruence))

Theorem: bit-equiv-implies-equal-merge-8-bits-1

(defthm bit-equiv-implies-equal-merge-8-bits-1
  (implies (bit-equiv a7 a7-equiv)
           (equal (merge-8-bits a7 a6 a5 a4 a3 a2 a1 a0)
                  (merge-8-bits a7-equiv a6 a5 a4 a3 a2 a1 a0)))
  :rule-classes (:congruence))