		Search-engine friendly clone of the ACL2 documentation.

Ihs/logand-lemmas

Lemmas about logand from the logops-lemmas book.

Definitions and Theorems

Theorem: commutativity-of-logand

(defthm commutativity-of-logand
  (equal (logand i j) (logand j i)))

Theorem: simplify-logand

(defthm simplify-logand
  (and (equal (logand 0 i) 0)
       (equal (logand -1 i) (ifix i))))

Theorem: logand-=-minus-1

(defthm logand-=-minus-1
  (equal (equal (logand i j) -1)
         (and (equal i -1) (equal j -1))))

Theorem: unsigned-byte-p-logand

(defthm unsigned-byte-p-logand
  (implies (and (or (unsigned-byte-p size i)
                    (unsigned-byte-p size j))
                (force (integerp i))
                (force (integerp j)))
           (unsigned-byte-p size (logand i j))))

Theorem: logand-upper-bound

(defthm logand-upper-bound
  (implies (and (>= i 0) (integerp j))
           (<= (logand i j) i))
  :rule-classes
  ((:linear :corollary (implies (and (>= i 0) (integerp j))
                                (<= (logand i j) i)))
   (:linear :corollary (implies (and (>= i 0) (integerp j))
                                (<= (logand j i) i)))))

Theorem: logand-logior

(defthm logand-logior
  (implies (and (integerp x)
                (integerp y)
                (integerp z))
           (equal (logand x (logior y z))
                  (logior (logand x y) (logand x z)))))

Theorem: logand-logxor

(defthm logand-logxor
  (implies (and (force (integerp i))
                (force (integerp j))
                (force (integerp k)))
           (equal (logand i (logxor j k))
                  (logxor (logand i j) (logand i k)))))