• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
    • 100-theorems
    • Arithmetic
    • Bit-vectors
      • Sparseint
      • Bitops
      • Bv
      • Ihs
        • Logops-definitions
        • Math-lemmas
        • Ihs-theories
        • Ihs-init
        • Logops
          • Logops-lemmas
            • Logops-recursive-definitions-theory
            • Ihs/logbitp-lemmas
            • Ihs/logtail-lemmas
            • Ihs/loghead-lemmas
            • Ihs/logrpl-lemmas
            • Ihs/logand-lemmas
            • Ihs/logapp-lemmas
            • Ihs/logcar-lemmas
            • Ihs/integer-length-lemmas
            • Ihs/unsigned-byte-p-lemmas
            • Ihs/logcons-lemmas
            • Signed-byte-p-logops
            • Ihs/logxor-lemmas
            • Ihs/logior-lemmas
            • Ihs/logext-lemmas
            • Ihs/logextu-lemmas
            • Ihs/signed-byte-p-lemmas
            • Ihs/lognotu-lemmas
            • Ihs/lognot-lemmas
            • Ihs/logmaskp-lemmas
            • Ihs/ash-lemmas
            • Logops-lemmas-theory
            • Ihs/wrb-lemmas
            • Ihs/logite-lemmas
      • Rtl
    • Algebra
  • Testing-utilities

• Logbitp
• Logbit
• Logops-lemmas

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