• 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

• Loghead
• Logops-lemmas

Ihs/loghead-lemmas

Lemmas about loghead from the logops-lemmas book.

Definitions and Theorems

Theorem: loghead-identity

(defthm loghead-identity
  (implies (unsigned-byte-p size i)
           (equal (loghead size i) i)))

Theorem: loghead-loghead

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

Theorem: loghead-0-i

(defthm loghead-0-i
  (implies (integerp i)
           (equal (loghead 0 i) 0)))

Theorem: loghead-size-0

(defthm loghead-size-0
  (implies (and (integerp size) (>= size 0))
           (equal (loghead size 0) 0)))

Theorem: loghead-leq

(defthm loghead-leq
  (implies (and (>= i 0) (loghead-guard size i))
           (<= (loghead size i) i))
  :rule-classes ((:linear :trigger-terms ((loghead size i)))))

Theorem: loghead-logapp

(defthm loghead-logapp
  (implies (and (<= size1 size)
                (force (>= size1 0))
                (force (integerp size1))
                (logapp-guard size i j))
           (equal (loghead size1 (logapp size i j))
                  (loghead size1 i))))

Theorem: loghead-logrpl

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

Theorem: bitp-loghead-1

(defthm bitp-loghead-1
  (bitp (loghead 1 i))
  :rule-classes :type-prescription)

Theorem: loghead-+-cancel-0

(defthm loghead-+-cancel-0
  (implies (and (force (integerp j))
                (loghead-guard size i))
           (equal (equal (loghead size (+ i j))
                         (loghead size i))
                  (equal (loghead size j) 0))))

Theorem: loghead-+-cancel

(defthm loghead-+-cancel
  (implies (and (force (integerp size))
                (>= size 0)
                (force (integerp i))
                (force (integerp j))
                (force (integerp k)))
           (equal (equal (loghead size (+ i j))
                         (loghead size (+ i k)))
                  (equal (loghead size j)
                         (loghead size k)))))

Theorem: loghead-+-loghead

(defthm loghead-+-loghead
  (implies (and (force (integerp size))
                (>= size 0)
                (force (integerp i))
                (force (integerp j)))
           (equal (loghead size (+ i (loghead size j)))
                  (loghead size (+ i j)))))