		Search-engine friendly clone of the ACL2 documentation.

4vec-operations

4vec-idx->4v

Like logbit for 4vecs, for fixed indices, producing an 4v-style ACL2::4vp.

Signature
(4vec-idx->4v n x) → bit
Arguments: n — The bit position to extract.
Guard (natp n).; x — The 4vec to extract it from.
Guard (4vec-p x).
Returns: bit — Type (acl2::4vp bit).

This function is mainly used in correspondence theorems that show the relationship between our 4vec-operations and the simple, four-valued bit operations provided in the 4v library.

Definitions and Theorems

Function: 4vec-idx->4v

(defun 4vec-idx->4v (n x)
  (declare (xargs :guard (and (natp n) (4vec-p x))))
  (let ((__function__ '4vec-idx->4v))
    (declare (ignorable __function__))
    (b* (((4vec x)) (n (lnfix n)))
      (if (logbitp n x.upper)
          (if (logbitp n x.lower)
              (acl2::4vt)
            (acl2::4vx))
        (if (logbitp n x.lower)
            (acl2::4vz)
          (acl2::4vf))))))

Theorem: 4vp-of-4vec-idx->4v

(defthm 4vp-of-4vec-idx->4v
  (b* ((bit (4vec-idx->4v n x)))
    (acl2::4vp bit))
  :rule-classes :rewrite)

Theorem: 4vec-idx->4v-of-nfix-n

(defthm 4vec-idx->4v-of-nfix-n
  (equal (4vec-idx->4v (nfix n) x)
         (4vec-idx->4v n x)))

Theorem: 4vec-idx->4v-nat-equiv-congruence-on-n

(defthm 4vec-idx->4v-nat-equiv-congruence-on-n
  (implies (nat-equiv n n-equiv)
           (equal (4vec-idx->4v n x)
                  (4vec-idx->4v n-equiv x)))
  :rule-classes :congruence)

Theorem: 4vec-idx->4v-of-4vec-fix-x

(defthm 4vec-idx->4v-of-4vec-fix-x
  (equal (4vec-idx->4v n (4vec-fix x))
         (4vec-idx->4v n x)))

Theorem: 4vec-idx->4v-4vec-equiv-congruence-on-x

(defthm 4vec-idx->4v-4vec-equiv-congruence-on-x
  (implies (4vec-equiv x x-equiv)
           (equal (4vec-idx->4v n x)
                  (4vec-idx->4v n x-equiv)))
  :rule-classes :congruence)

Theorem: 4vec-idx->4v-when-3vec-p

(defthm 4vec-idx->4v-when-3vec-p
  (implies (3vec-p x)
           (not (equal (4vec-idx->4v n x) 'z))))

Theorem: 4vec-idx->4v-of-3vec-fix

(defthm 4vec-idx->4v-of-3vec-fix
  (equal (4vec-idx->4v n (3vec-fix x))
         (let ((x4v (4vec-idx->4v n x)))
           (if (eq x4v 'z) 'x x4v))))