		Search-engine friendly clone of the ACL2 documentation.

Index-of

(index-of k x) returns the index of the first occurrence of element k in list x if it exists, NIL otherwise.

Index-of is like the Common Lisp function position, but only operates on lists and is not (logically) tail-recursive.

Definitions and Theorems

Function: index-of-aux

(defun index-of-aux (k x acc)
  (declare (type (integer 0 *) acc))
  (cond ((atom x) nil)
        ((equal k (car x))
         (mbe :logic (ifix acc) :exec acc))
        (t (index-of-aux k (cdr x)
                         (+ 1 (mbe :logic (ifix acc) :exec acc))))))

Function: index-of-aux-eq

(defun index-of-aux-eq (k x acc)
  (declare (type (integer 0 *) acc)
           (type symbol k))
  (cond ((atom x) nil)
        ((eq k (car x))
         (mbe :logic (ifix acc) :exec acc))
        (t (index-of-aux k (cdr x)
                         (+ 1 (mbe :logic (ifix acc) :exec acc))))))

Function: index-of-aux-eql

(defun index-of-aux-eql (k x acc)
  (declare (type (integer 0 *) acc)
           (xargs :guard (eqlablep k)))
  (cond ((atom x) nil)
        ((eql k (car x))
         (mbe :logic (ifix acc) :exec acc))
        (t (index-of-aux k (cdr x)
                         (+ 1 (mbe :logic (ifix acc) :exec acc))))))

Theorem: index-of-aux-eq-normalize

(defthm index-of-aux-eq-normalize
  (equal (index-of-aux-eq k x acc)
         (index-of-aux k x acc)))

Theorem: index-of-aux-eql-normalize

(defthm index-of-aux-eql-normalize
  (equal (index-of-aux-eql k x acc)
         (index-of-aux k x acc)))

Function: index-of

(defun index-of (k x)
  (declare (xargs :guard t))
  (mbe :logic (cond ((atom x) nil)
                    ((equal k (car x)) 0)
                    (t (let ((res (index-of k (cdr x))))
                         (and res (+ 1 res)))))
       :exec (cond ((symbolp k) (index-of-aux-eq k x 0))
                   ((eqlablep k) (index-of-aux-eql k x 0))
                   (t (index-of-aux k x 0)))))

Theorem: index-of-aux-removal

(defthm index-of-aux-removal
  (equal (index-of-aux k x acc)
         (and (index-of k x)
              (+ (index-of k x) (ifix acc)))))

Theorem: position-equal-ac-is-index-of-aux

(defthm position-equal-ac-is-index-of-aux
  (implies (integerp acc)
           (equal (position-equal-ac k x acc)
                  (index-of-aux k x acc))))

Theorem: index-of-iff-member

(defthm index-of-iff-member
  (iff (index-of k x) (member k x)))

Theorem: integerp-of-index-of

(defthm integerp-of-index-of
  (iff (integerp (index-of k x))
       (member k x)))

Theorem: natpp-of-index-of

(defthm natpp-of-index-of
  (iff (natp (index-of k x))
       (member k x)))

Theorem: nth-of-index-when-member

(defthm nth-of-index-when-member
  (implies (member k x)
           (equal (nth (index-of k x) x) k)))

Theorem: index-of-<-len

(defthm index-of-<-len
  (implies (member k x)
           (< (index-of k x) (len x)))
  :rule-classes :linear)

Theorem: index-of-append-first

(defthm index-of-append-first
  (implies (index-of k x)
           (equal (index-of k (append x y))
                  (index-of k x))))

Theorem: index-of-append-second

(defthm index-of-append-second
  (implies (and (not (index-of k x))
                (index-of k y))
           (equal (index-of k (append x y))
                  (+ (len x) (index-of k y)))))

Theorem: index-of-append-neither

(defthm index-of-append-neither
  (implies (and (not (index-of k x))
                (not (index-of k y)))
           (not (index-of k (append x y)))))

Theorem: index-of-append-split

(defthm index-of-append-split
  (equal (index-of k (append x y))
         (or (index-of k x)
             (and (index-of k y)
                  (+ (len x) (index-of k y))))))

Subtopics

Index-of-theorems: Some theorems about the library function index-of.