index-of

(in-package "ACL2")

(defsection index-of
  :parents (std/lists search)
  :short "@(call index-of) returns the index of the first occurrence of element
@('k') in list @('x') if it exists, @('NIL') otherwise."
  :long "Index-of is like the Common Lisp function @(tsee position), but only
  operates on lists and is not (logically) tail-recursive."
  (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))))))
  (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))))))
  (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))))))
  (defthm index-of-aux-eq-normalize
    (equal (index-of-aux-eq k x acc) (index-of-aux k x acc)))
  (defthm index-of-aux-eql-normalize
    (equal (index-of-aux-eql k x acc) (index-of-aux k x acc)))
  (defund index-of
    (k x)
    (declare (xargs :guard t :verify-guards nil))
    (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)))))
  (local (in-theory (enable index-of)))
  (defthm index-of-aux-removal
    (equal (index-of-aux k x acc)
      (and (index-of k x) (+ (index-of k x) (ifix acc)))))
  (verify-guards index-of)
  (defthm position-equal-ac-is-index-of-aux
    (implies (integerp acc)
      (equal (position-equal-ac k x acc) (index-of-aux k x acc))))
  (defthm index-of-iff-member
    (iff (index-of k x) (member k x)))
  (defthm integerp-of-index-of
    (iff (integerp (index-of k x)) (member k x)))
  (defthm natpp-of-index-of
    (iff (natp (index-of k x)) (member k x)))
  (defthm nth-of-index-when-member
    (implies (member k x) (equal (nth (index-of k x) x) k)))
  (defthm index-of-<-len
    (implies (member k x) (< (index-of k x) (len x)))
    :rule-classes :linear)
  (defthm index-of-append-first
    (implies (index-of k x)
      (equal (index-of k (append x y)) (index-of k x))))
  (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)))))
  (defthm index-of-append-neither
    (implies (and (not (index-of k x)) (not (index-of k y)))
      (not (index-of k (append x y)))))
  (defthmd 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)))))))