		Search-engine friendly clone of the ACL2 documentation.

A4vec-operations

A4vec-zero-ext

Symbolic version of 4vec-zero-ext.

Signature
(a4vec-zero-ext n x mask) → res
Arguments: n — Place to zero extend or truncate.
Guard (a4vec-p n).; x — Vector to zero extend at this place.
Guard (a4vec-p x).; mask — Care mask for the result.
Guard (4vmask-p mask).
Returns: res — Type (a4vec-p res).

We just reuse a4vec-concat since it already provides special optimization to avoid problems due to large masks.

Definitions and Theorems

Function: a4vec-zero-ext

(defun a4vec-zero-ext (n x mask)
  (declare (xargs :guard (and (a4vec-p n)
                              (a4vec-p x)
                              (4vmask-p mask))))
  (let ((__function__ 'a4vec-zero-ext))
    (declare (ignorable __function__))
    (a4vec-concat n x (a4vec-0) mask)))

Theorem: a4vec-p-of-a4vec-zero-ext

(defthm a4vec-p-of-a4vec-zero-ext
  (b* ((res (a4vec-zero-ext n x mask)))
    (a4vec-p res))
  :rule-classes :rewrite)

Theorem: a4vec-zero-ext-correct

(defthm a4vec-zero-ext-correct
  (4vec-mask-equiv (a4vec-eval (a4vec-zero-ext n x mask)
                               env)
                   (4vec-zero-ext (a4vec-eval n env)
                                  (a4vec-eval x env))
                   mask))

Theorem: a4vec-zero-ext-of-a4vec-fix-n

(defthm a4vec-zero-ext-of-a4vec-fix-n
  (equal (a4vec-zero-ext (a4vec-fix n) x mask)
         (a4vec-zero-ext n x mask)))

Theorem: a4vec-zero-ext-a4vec-equiv-congruence-on-n

(defthm a4vec-zero-ext-a4vec-equiv-congruence-on-n
  (implies (a4vec-equiv n n-equiv)
           (equal (a4vec-zero-ext n x mask)
                  (a4vec-zero-ext n-equiv x mask)))
  :rule-classes :congruence)

Theorem: a4vec-zero-ext-of-a4vec-fix-x

(defthm a4vec-zero-ext-of-a4vec-fix-x
  (equal (a4vec-zero-ext n (a4vec-fix x) mask)
         (a4vec-zero-ext n x mask)))

Theorem: a4vec-zero-ext-a4vec-equiv-congruence-on-x

(defthm a4vec-zero-ext-a4vec-equiv-congruence-on-x
  (implies (a4vec-equiv x x-equiv)
           (equal (a4vec-zero-ext n x mask)
                  (a4vec-zero-ext n x-equiv mask)))
  :rule-classes :congruence)

Theorem: a4vec-zero-ext-of-4vmask-fix-mask

(defthm a4vec-zero-ext-of-4vmask-fix-mask
  (equal (a4vec-zero-ext n x (4vmask-fix mask))
         (a4vec-zero-ext n x mask)))

Theorem: a4vec-zero-ext-4vmask-equiv-congruence-on-mask

(defthm a4vec-zero-ext-4vmask-equiv-congruence-on-mask
  (implies (4vmask-equiv mask mask-equiv)
           (equal (a4vec-zero-ext n x mask)
                  (a4vec-zero-ext n x mask-equiv)))
  :rule-classes :congruence)