		Search-engine friendly clone of the ACL2 documentation.

Bitops/merge

Merge-2-u16s

Concatenate 2 16-bit numbers together to form an 32-bit result.

Signature
(merge-2-u16s a1 a0) → result
Returns: result — Type (natp result).

Definitions and Theorems

Function: merge-2-u16s$inline

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

Theorem: natp-of-merge-2-u16s

(defthm acl2::natp-of-merge-2-u16s
  (b* ((result (acl2::merge-2-u16s$inline a1 a0)))
    (natp result))
  :rule-classes :type-prescription)

Theorem: unsigned-byte-p-32-of-merge-2-u16s

(defthm unsigned-byte-p-32-of-merge-2-u16s
 (unsigned-byte-p 32 (merge-2-u16s a1 a0))
 :rule-classes
 ((:rewrite
       :corollary (implies (>= (nfix n) 32)
                           (unsigned-byte-p n (merge-2-u16s a1 a0)))
       :hints (("Goal" :in-theory (disable unsigned-byte-p))))))

Theorem: merge-2-u16s-is-merge-unsigneds

(defthm merge-2-u16s-is-merge-unsigneds
  (equal (merge-2-u16s a1 a0)
         (merge-unsigneds 16 (list (nfix a1) (nfix a0)))))

Basic nat-equiv congruences.

Theorem: nat-equiv-implies-equal-merge-2-u16s-2

(defthm nat-equiv-implies-equal-merge-2-u16s-2
  (implies (nat-equiv a0 a0-equiv)
           (equal (merge-2-u16s a1 a0)
                  (merge-2-u16s a1 a0-equiv)))
  :rule-classes (:congruence))

Theorem: nat-equiv-implies-equal-merge-2-u16s-1

(defthm nat-equiv-implies-equal-merge-2-u16s-1
  (implies (nat-equiv a1 a1-equiv)
           (equal (merge-2-u16s a1 a0)
                  (merge-2-u16s a1-equiv a0)))
  :rule-classes (:congruence))