		Search-engine friendly clone of the ACL2 documentation.

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