		Search-engine friendly clone of the ACL2 documentation.

Logbitp-mismatch

(logbitp-mismatch a b) finds the minimal bit-position for which a and b differ, or returns NIL if no such bit exists.

This is mainly useful for proving equal-by-logbitp, but it's also occasionally useful as a witness in other theorems.

Definitions and Theorems

Function: logbitp-mismatch

(defun logbitp-mismatch (a b)
  (declare (xargs :guard (and (integerp a) (integerp b))))
  (cond ((not (equal (logcar a) (logcar b))) 0)
        ((and (zp (integer-length a))
              (zp (integer-length b)))
         nil)
        (t (let ((tail (logbitp-mismatch (logcdr a)
                                         (logcdr b))))
             (and tail (+ 1 tail))))))

Theorem: logbitp-mismatch-under-iff

(defthm logbitp-mismatch-under-iff
  (iff (logbitp-mismatch a b)
       (not (equal (ifix a) (ifix b)))))

Theorem: logbitp-mismatch-correct

(defthm logbitp-mismatch-correct
  (implies (logbitp-mismatch a b)
           (not (equal (logbitp (logbitp-mismatch a b) a)
                       (logbitp (logbitp-mismatch a b) b)))))

Theorem: logbitp-mismatch-upper-bound

(defthm logbitp-mismatch-upper-bound
  (implies (logbitp-mismatch a b)
           (<= (logbitp-mismatch a b)
               (max (integer-length a)
                    (integer-length b))))
  :rule-classes ((:rewrite) (:linear)))

Theorem: logbitp-mismatch-upper-bound-for-nonnegatives

(defthm logbitp-mismatch-upper-bound-for-nonnegatives
  (implies (and (not (and (integerp a) (< a 0)))
                (not (and (integerp b) (< b 0)))
                (logbitp-mismatch a b))
           (< (logbitp-mismatch a b)
              (max (integer-length a)
                   (integer-length b))))
  :rule-classes ((:rewrite)
                 (:linear :trigger-terms ((logbitp-mismatch a b)))))

Theorem: integerp-of-logbitp-mismatch

(defthm integerp-of-logbitp-mismatch
  (iff (integerp (logbitp-mismatch a b))
       (logbitp-mismatch a b)))