		Search-engine friendly clone of the ACL2 documentation.

Bitops/merge

Merge-4-u2s

Concatenate 4 2-bit numbers together to form an 8-bit result.

Signature
(merge-4-u2s a3 a2 a1 a0) → result
Returns: result — Type (natp result).

Definitions and Theorems

Function: merge-4-u2s$inline

(defun acl2::merge-4-u2s$inline (a3 a2 a1 a0)
 (declare (type (unsigned-byte 2) a3 a2 a1 a0))
 (declare (xargs :guard t))
 (let ((__function__ 'merge-4-u2s))
  (declare (ignorable __function__))
  (mbe
     :logic
     (logapp* 2 (nfix a0)
              (nfix a1)
              (nfix a2)
              (nfix a3)
              0)
     :exec
     (b* ((ans a0)
          (ans (the (unsigned-byte 8)
                    (logior (the (unsigned-byte 8) (ash a1 (* 1 2)))
                            (the (unsigned-byte 8) ans))))
          (ans (the (unsigned-byte 8)
                    (logior (the (unsigned-byte 8) (ash a2 (* 2 2)))
                            (the (unsigned-byte 8) ans)))))
       (the (unsigned-byte 8)
            (logior (the (unsigned-byte 8) (ash a3 (* 3 2)))
                    (the (unsigned-byte 8) ans)))))))

Theorem: natp-of-merge-4-u2s

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

Theorem: unsigned-byte-p-8-of-merge-4-u2s

(defthm unsigned-byte-p-8-of-merge-4-u2s
  (unsigned-byte-p 8 (merge-4-u2s a3 a2 a1 a0))
  :rule-classes
  ((:rewrite
        :corollary
        (implies (>= (nfix n) 8)
                 (unsigned-byte-p n (merge-4-u2s a3 a2 a1 a0)))
        :hints (("Goal" :in-theory (disable unsigned-byte-p))))))

Theorem: merge-4-u2s-is-merge-unsigneds

(defthm merge-4-u2s-is-merge-unsigneds
  (equal (merge-4-u2s a3 a2 a1 a0)
         (merge-unsigneds 2
                          (list (nfix a3)
                                (nfix a2)
                                (nfix a1)
                                (nfix a0)))))

Basic nat-equiv congruences.

Theorem: nat-equiv-implies-equal-merge-4-u2s-4

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

Theorem: nat-equiv-implies-equal-merge-4-u2s-3

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

Theorem: nat-equiv-implies-equal-merge-4-u2s-2

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

Theorem: nat-equiv-implies-equal-merge-4-u2s-1

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