		Search-engine friendly clone of the ACL2 documentation.

Bitops/parity

Parity

(parity n x) computes the parity of the low n bits of x, returning it as a bitp.

Signature
(parity n x) → p
Arguments: n — Guard (natp n).; x — Guard (integerp x).
Returns: p — Type (bitp p).

This has a simple recursive definition which should be easy to reason about. However, it isn't particularly efficient; see fast-parity for a more efficient, logically identical function.

Definitions and Theorems

Function: parity

(defun parity (n x)
  (declare (xargs :guard (and (natp n) (integerp x))))
  (let ((__function__ 'parity))
    (declare (ignorable __function__))
    (cond ((zp n) 0)
          (t (logxor (logand x 1)
                     (parity (1- n) (ash x -1)))))))

Theorem: bitp-of-parity

(defthm acl2::bitp-of-parity
  (b* ((p (parity n x))) (bitp p))
  :rule-classes :type-prescription)

Theorem: parity-of-nfix-n

(defthm acl2::parity-of-nfix-n
  (equal (parity (nfix n) x)
         (parity n x)))

Theorem: parity-nat-equiv-congruence-on-n

(defthm acl2::parity-nat-equiv-congruence-on-n
  (implies (nat-equiv n acl2::n-equiv)
           (equal (parity n x)
                  (parity acl2::n-equiv x)))
  :rule-classes :congruence)

Theorem: parity-of-ifix-x

(defthm acl2::parity-of-ifix-x
  (equal (parity n (ifix x))
         (parity n x)))

Theorem: parity-int-equiv-congruence-on-x

(defthm acl2::parity-int-equiv-congruence-on-x
  (implies (int-equiv x acl2::x-equiv)
           (equal (parity n x)
                  (parity n acl2::x-equiv)))
  :rule-classes :congruence)

Theorem: parity-decomp

(defthm parity-decomp
  (equal (logxor (parity m (logtail n x))
                 (parity n (loghead n x)))
         (parity (+ (nfix m) (nfix n)) x)))

Theorem: parity-of-logxor

(defthm parity-of-logxor
  (equal (parity n (logxor x y))
         (logxor (parity n x) (parity n y))))

Theorem: parity-of-0

(defthm parity-of-0
  (equal (parity n 0) 0))

Theorem: parity-of-loghead-split

(defthm parity-of-loghead-split
  (equal (parity m (loghead n x))
         (parity (min (nfix m) (nfix n)) x)))