		Search-engine friendly clone of the ACL2 documentation.

Listpos

(listpos x y) returns the starting position of the first occurrence of the sublist x within the list y, or NIL if there is no such occurrence.

See also sublistp, which is closely related.

Definitions and Theorems

Function: listpos

(defun listpos (x y)
  (declare (xargs :guard t))
  (cond ((prefixp x y) 0)
        ((atom y) nil)
        (t (let ((pos-in-cdr (listpos x (cdr y))))
             (and pos-in-cdr (+ 1 pos-in-cdr))))))

Theorem: listpos-when-atom-left

(defthm listpos-when-atom-left
  (implies (atom x)
           (equal (listpos x y) 0)))

Theorem: listpos-when-atom-right

(defthm listpos-when-atom-right
  (implies (atom y)
           (equal (listpos x y)
                  (if (atom x) 0 nil))))

Theorem: listpos-of-list-fix-left

(defthm listpos-of-list-fix-left
  (equal (listpos (list-fix x) y)
         (listpos x y)))

Theorem: listpos-of-list-fix-right

(defthm listpos-of-list-fix-right
  (equal (listpos x (list-fix y))
         (listpos x y)))

Theorem: list-equiv-implies-equal-listpos-1

(defthm list-equiv-implies-equal-listpos-1
  (implies (list-equiv x x-equiv)
           (equal (listpos x y)
                  (listpos x-equiv y)))
  :rule-classes (:congruence))

Theorem: list-equiv-implies-equal-listpos-2

(defthm list-equiv-implies-equal-listpos-2
  (implies (list-equiv y y-equiv)
           (equal (listpos x y)
                  (listpos x y-equiv)))
  :rule-classes (:congruence))

Theorem: listpos-under-iff

(defthm listpos-under-iff
  (iff (listpos x y) (sublistp x y)))

Theorem: natp-of-listpos

(defthm natp-of-listpos
  (equal (natp (listpos x y))
         (sublistp x y)))

Theorem: integerp-of-listpos

(defthm integerp-of-listpos
  (equal (integerp (listpos x y))
         (sublistp x y)))

Theorem: rationalp-of-listpos

(defthm rationalp-of-listpos
  (equal (rationalp (listpos x y))
         (sublistp x y)))

Theorem: acl2-numberp-of-listpos

(defthm acl2-numberp-of-listpos
  (equal (acl2-numberp (listpos x y))
         (sublistp x y)))

Theorem: listpos-lower-bound-weak

(defthm listpos-lower-bound-weak
  (<= 0 (listpos x y))
  :rule-classes (:linear))

Theorem: listpos-upper-bound-weak

(defthm listpos-upper-bound-weak
  (<= (listpos x y) (len y))
  :rule-classes ((:rewrite) (:linear)))

Theorem: listpos-upper-bound-strong-1

(defthm listpos-upper-bound-strong-1
  (equal (< (listpos x y) (len y))
         (consp y))
  :rule-classes
  ((:rewrite)
   (:linear :corollary (implies (consp y)
                                (< (listpos x y) (len y))))))

Theorem: listpos-upper-bound-strong-2

(defthm listpos-upper-bound-strong-2
  (implies (sublistp x y)
           (<= (listpos x y) (- (len y) (len x))))
  :rule-classes ((:rewrite) (:linear)))

Theorem: listpos-complete

(defthm listpos-complete
  (implies (prefixp x (nthcdr n y))
           (and (listpos x y)
                (<= (listpos x y) (nfix n))))
  :rule-classes
  ((:rewrite)
   (:linear :corollary (implies (prefixp x (nthcdr n y))
                                (<= (listpos x y) (nfix n))))))