		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))))