		Search-engine friendly clone of the ACL2 documentation.

Ihs/logbitp-lemmas

Lemmas about logbitp and logbit from the logops-lemmas book.

We prove a set of lemmas about logbitp, then prove the analogous lemmas about logbit, which is defined in terms of logbitp.

Definitions and Theorems

Theorem: logbitp-0-minus-1

(defthm logbitp-0-minus-1
  (implies (and (integerp pos) (>= pos 0))
           (and (not (logbitp pos 0))
                (logbitp pos -1))))

Theorem: logbit-0-minus-1

(defthm logbit-0-minus-1
  (implies (and (integerp pos)
                (>= pos 0)
                (integerp i))
           (and (equal (logbit pos 0) 0)
                (equal (logbit pos -1) 1))))

Theorem: logbitp-loghead

(defthm logbitp-loghead
  (implies (and (loghead-guard size i)
                (force (integerp pos))
                (force (>= pos 0)))
           (equal (logbitp pos (loghead size i))
                  (if (< pos size) (logbitp pos i) nil))))

Theorem: logbit-loghead

(defthm logbit-loghead
  (implies (and (loghead-guard size i)
                (force (integerp pos))
                (force (>= pos 0))
                (< pos size))
           (equal (logbit pos (loghead size i))
                  (if (< pos size) (logbit pos i) 0))))

Theorem: logbitp-logtail

(defthm logbitp-logtail
  (implies (and (logtail-guard pos i)
                (force (integerp pos1))
                (force (>= pos1 0)))
           (equal (logbitp pos1 (logtail pos i))
                  (logbitp (+ pos pos1) i))))

Theorem: logbit-logtail

(defthm logbit-logtail
  (implies (and (logtail-guard pos i)
                (force (integerp pos1))
                (force (>= pos1 0)))
           (equal (logbit pos1 (logtail pos i))
                  (logbit (+ pos pos1) i))))

Theorem: logbitp-logapp

(defthm logbitp-logapp
  (implies (and (logapp-guard size i j)
                (force (integerp pos))
                (force (>= pos 0)))
           (equal (logbitp pos (logapp size i j))
                  (if (< pos size)
                      (logbitp pos i)
                    (logbitp (- pos size) j)))))

Theorem: logbit-logapp

(defthm logbit-logapp
  (implies (and (logapp-guard size i j)
                (force (integerp pos))
                (force (>= pos 0)))
           (equal (logbit pos (logapp size i j))
                  (if (< pos size)
                      (logbit pos i)
                    (logbit (- pos size) j)))))

Theorem: logbitp-logrpl

(defthm logbitp-logrpl
  (implies (and (logrpl-guard size i j)
                (force (integerp pos))
                (force (>= pos 0)))
           (equal (logbitp pos (logrpl size i j))
                  (if (< pos size)
                      (logbitp pos i)
                    (logbitp pos j)))))

Theorem: logbit-logrpl

(defthm logbit-logrpl
  (implies (and (logrpl-guard size i j)
                (force (integerp pos))
                (force (>= pos 0)))
           (equal (logbit pos (logrpl size i j))
                  (if (< pos size)
                      (logbit pos i)
                    (logbit pos j)))))

Theorem: logbitp-lognot

(defthm logbitp-lognot
  (implies (and (integerp pos)
                (>= pos 0)
                (integerp i))
           (equal (logbitp pos (lognot i))
                  (not (logbitp pos i)))))

Theorem: logbit-lognot

(defthm logbit-lognot
  (implies (and (integerp pos)
                (>= pos 0)
                (integerp i))
           (equal (logbit pos (lognot i))
                  (b-not (logbit pos i)))))

Theorem: logbitp-lognotu

(defthm logbitp-lognotu
  (implies (and (integerp pos)
                (>= pos 0)
                (integerp i)
                (force (integerp size))
                (force (>= size 0)))
           (equal (logbitp pos (lognotu size i))
                  (if (< pos size)
                      (not (logbitp pos i))
                    nil))))

Theorem: logbit-lognotu

(defthm logbit-lognotu
  (implies (and (integerp pos)
                (>= pos 0)
                (integerp i)
                (force (integerp size))
                (force (>= size 0)))
           (equal (logbit pos (lognotu size i))
                  (if (< pos size)
                      (b-not (logbit pos i))
                    0))))