Optimized trailing 0 count for integers.
(trailing-0-count x) → *
To make this fast, be sure and include the "std/bitsets/bignum-extract-opt" book (reqires a ttag), which prevents this (at least on CCL64) from needing to create new bignums when run on bignums.
(defun trailing-0-count (x) (declare (xargs :guard (integerp x))) (let ((__function__ 'trailing-0-count)) (declare (ignorable __function__)) (mbe :logic (if (or (zip x) (logbitp 0 x)) 0 (+ 1 (trailing-0-count (logcdr x)))) :exec (if (eql 0 x) 0 (trailing-0-count-rec x 0)))))
(defthm trailing-0-count-properties (implies (not (zip x)) (let ((count (trailing-0-count x))) (and (logbitp count x) (equal (loghead count x) 0) (implies (< (nfix idx) count) (not (logbitp idx x)))))))
(defthm logand-of-minus-in-terms-of-trailing-0-count (implies (not (zip x)) (equal (logand x (- x)) (ash 1 (trailing-0-count x)))))
(defthm trailing-0-count-bound (implies (posp x) (< (trailing-0-count x) (integer-length x))) :rule-classes ((:linear :trigger-terms ((trailing-0-count x)))))
(defthm trailing-0-count-of-ifix-x (equal (trailing-0-count (ifix x)) (trailing-0-count x)))
(defthm trailing-0-count-int-equiv-congruence-on-x (implies (int-equiv x x-equiv) (equal (trailing-0-count x) (trailing-0-count x-equiv))) :rule-classes :congruence)