		Search-engine friendly clone of the ACL2 documentation.

Bitops/merge

Merge-4-bits

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

Signature
(merge-4-bits a3 a2 a1 a0) → result
Arguments: 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-4-bits$inline

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

Theorem: natp-of-merge-4-bits

(defthm acl2::natp-of-merge-4-bits
        (b* ((result (acl2::merge-4-bits$inline a3 a2 a1 a0)))
            (natp result))
        :rule-classes :type-prescription)

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

(defthm unsigned-byte-p-4-of-merge-4-bits
        (unsigned-byte-p 4 (merge-4-bits a3 a2 a1 a0)))

Theorem: merge-4-bits-is-merge-unsigneds

(defthm merge-4-bits-is-merge-unsigneds
        (equal (merge-4-bits a3 a2 a1 a0)
               (merge-unsigneds 1
                                (list (bfix a3)
                                      (bfix a2)
                                      (bfix a1)
                                      (bfix a0)))))

Basic bit-equiv congruences.

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

(defthm bit-equiv-implies-equal-merge-4-bits-4
        (implies (bit-equiv a0 a0-equiv)
                 (equal (merge-4-bits a3 a2 a1 a0)
                        (merge-4-bits a3 a2 a1 a0-equiv)))
        :rule-classes (:congruence))

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

(defthm bit-equiv-implies-equal-merge-4-bits-3
        (implies (bit-equiv a1 a1-equiv)
                 (equal (merge-4-bits a3 a2 a1 a0)
                        (merge-4-bits a3 a2 a1-equiv a0)))
        :rule-classes (:congruence))

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

(defthm bit-equiv-implies-equal-merge-4-bits-2
        (implies (bit-equiv a2 a2-equiv)
                 (equal (merge-4-bits a3 a2 a1 a0)
                        (merge-4-bits a3 a2-equiv a1 a0)))
        :rule-classes (:congruence))

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

(defthm bit-equiv-implies-equal-merge-4-bits-1
        (implies (bit-equiv a3 a3-equiv)
                 (equal (merge-4-bits a3 a2 a1 a0)
                        (merge-4-bits a3-equiv a2 a1 a0)))
        :rule-classes (:congruence))