list-defuns

(defun firstn
  (n l)
  "The sublist of L consisting of its first N elements."
  (declare (xargs :guard (and (true-listp l) (integerp n) (<= 0 n))))
  (cond ((endp l) nil)
    ((zp n) nil)
    (t (cons (car l) (firstn (1- n) (cdr l))))))

(defun initial-sublistp
  (l1 l2)
  "Is the first list an initial sublist of the second?"
  (declare (xargs :guard (and (eqlable-listp l1) (eqlable-listp l2))))
  (cond ((endp l1) t)
    ((endp l2) nil)
    (t (and (eql (car l1) (car l2))
        (initial-sublistp (cdr l1) (cdr l2))))))

(defun initial-sublistp-eq
  (l1 l2)
  "Is the first list an initial sublist of the second?"
  (declare (xargs :guard (and (symbol-listp l1) (symbol-listp l2))))
  (cond ((endp l1) t)
    ((endp l2) nil)
    (t (and (eq (car l1) (car l2))
        (initial-sublistp-eq (cdr l1) (cdr l2))))))

(defun initial-sublistp-equal
  (l1 l2)
  "Is the first list an initial sublist of the second?"
  (declare (xargs :guard (and (true-listp l1) (true-listp l2))))
  (cond ((endp l1) t)
    ((endp l2) nil)
    (t (and (equal (car l1) (car l2))
        (initial-sublistp-equal (cdr l1) (cdr l2))))))

(defun memberp
  (x l)
  (declare (xargs :guard (if (eqlablep x)
        (true-listp l)
        (eqlable-listp l))))
  (consp (member x l)))

(defun memberp-eq
  (x l)
  (declare (xargs :guard (if (symbolp x)
        (true-listp l)
        (symbol-listp l))))
  (consp (member-eq x l)))

(defun memberp-equal
  (x l)
  (declare (xargs :guard (true-listp l)))
  (consp (member-equal x l)))

(defun nth-seg
  (i j l)
  "The sublist of L beginning at offset I for length J."
  (declare (xargs :guard (and (integerp i)
        (<= 0 i)
        (integerp j)
        (<= 0 j)
        (true-listp l))))
  (cond ((endp l) nil)
    ((zp i) (cond ((zp j) nil)
        (t (cons (car l) (nth-seg i (1- j) (cdr l))))))
    (t (nth-seg (1- i) j (cdr l)))))

(defun occurrences-ac
  (item lst acc)
  (declare (xargs :guard (and (true-listp lst)
        (or (eqlablep item) (eqlable-listp lst))
        (acl2-numberp acc))))
  (cond ((endp lst) acc)
    ((eql item (car lst)) (occurrences-ac item (cdr lst) (1+ acc)))
    (t (occurrences-ac item (cdr lst) acc))))

(defun occurrences
  (item lst)
  (declare (xargs :guard (and (true-listp lst)
        (or (eqlablep item) (eqlable-listp lst)))))
  (occurrences-ac item lst 0))

(defun occurrences-eq-ac
  (item lst acc)
  (declare (xargs :guard (and (true-listp lst)
        (or (symbolp item) (symbol-listp lst))
        (acl2-numberp acc))))
  (cond ((endp lst) acc)
    ((eq item (car lst)) (occurrences-eq-ac item (cdr lst) (1+ acc)))
    (t (occurrences-eq-ac item (cdr lst) acc))))

(defun occurrences-eq
  (item lst)
  (declare (xargs :guard (symbol-listp lst)))
  (occurrences-eq-ac item lst 0))

(defun occurrences-equal-ac
  (item lst acc)
  (declare (xargs :guard (and (true-listp lst) (acl2-numberp acc))))
  (cond ((endp lst) acc)
    ((equal item (car lst)) (occurrences-equal-ac item (cdr lst) (1+ acc)))
    (t (occurrences-equal-ac item (cdr lst) acc))))

(defun occurrences-equal
  (item lst)
  (declare (xargs :guard (true-listp lst)))
  (occurrences-equal-ac item lst 0))

(defun put-nth
  (n v l)
  "The list derived from L by replacing its Nth element with value V."
  (declare (xargs :guard (and (integerp n) (<= 0 n) (true-listp l))))
  (cond ((endp l) nil)
    ((zp n) (cons v (cdr l)))
    (t (cons (car l) (put-nth (1- n) v (cdr l))))))

(defun put-seg
  (i seg l)
  "The list derived from L by replacing its contents beginning
   at location I with the contents of SEG. The length of the resulting
   list equals the length of L."
  (declare (xargs :guard (and (integerp i) (<= 0 i) (true-listp seg) (true-listp l))))
  (cond ((endp l) nil)
    ((zp i) (cond ((endp seg) l)
        (t (cons (car seg) (put-seg i (cdr seg) (cdr l))))))
    (t (cons (car l) (put-seg (1- i) seg (cdr l))))))