deflist - ACL2 Book

Included Books

other

(in-package "ACL2")

include-book

(include-book "list-defuns")

include-book

(include-book "utilities")

local

(local (include-book "list-defthms"))

list-type00-defunencapsulate

(encapsulate ((elem-type00 (x) boolean) (list-type00 (l) boolean))
  (local (in-theory '(ground-zero)))
  (local (defun elem-type00 (x) (declare (ignore)) (integerp x)))
  (local (defun list-type00
      (l)
      (cond ((atom l) (eq l nil))
        (t (and (elem-type00 (car l)) (list-type00 (cdr l)))))))
  (defthm list-type00-defun
    (iff (list-type00 l)
      (cond ((atom l) (eq l nil))
        (t (and (elem-type00 (car l)) (list-type00 (cdr l))))))
    :rule-classes ((:rewrite :corollary (implies (atom l) (equal (list-type00 l) (null l)))) (:rewrite :corollary (equal (list-type00 (cons x l))
          (and (elem-type00 x) (list-type00 l)))))))

list-type10-defunencapsulate

(encapsulate ((elem-type10 (x a) boolean) (list-type10 (l a) boolean))
  (local (in-theory '(ground-zero)))
  (local (defun elem-type10 (x a) (declare (ignore a)) (integerp x)))
  (local (defun list-type10
      (l a)
      (cond ((atom l) (eq l nil))
        (t (and (elem-type10 (car l) a) (list-type10 (cdr l) a))))))
  (defthm list-type10-defun
    (iff (list-type10 l a)
      (cond ((atom l) (eq l nil))
        (t (and (elem-type10 (car l) a) (list-type10 (cdr l) a)))))
    :rule-classes ((:rewrite :corollary (implies (atom l) (equal (list-type10 l a) (null l)))) (:rewrite :corollary (equal (list-type10 (cons x l) a)
          (and (elem-type10 x a) (list-type10 l a)))))))

list-type11-defunencapsulate

(encapsulate ((elem-type11 (a x) boolean) (list-type11 (a l) boolean))
  (local (in-theory '(ground-zero)))
  (local (defun elem-type11 (a x) (declare (ignore a)) (integerp x)))
  (local (defun list-type11
      (a l)
      (cond ((atom l) (eq l nil))
        (t (and (elem-type11 a (car l)) (list-type11 a (cdr l)))))))
  (defthm list-type11-defun
    (iff (list-type11 a l)
      (cond ((atom l) (eq l nil))
        (t (and (elem-type11 a (car l)) (list-type11 a (cdr l))))))
    :rule-classes ((:rewrite :corollary (implies (atom l) (equal (list-type11 a l) (null l)))) (:rewrite :corollary (equal (list-type11 a (cons x l))
          (and (elem-type11 a x) (list-type11 a l)))))))

replace-equalfunction

(defun replace-equal
  (a b l)
  (declare (xargs :guard (true-listp l)))
  (cond ((endp l) nil)
    ((equal (car l) a) (cons b (replace-equal a b (cdr l))))
    (t (cons (car l) (replace-equal a b (cdr l))))))

my-conjoinfunction

(defun my-conjoin
  (termlist1 termlist2)
  (declare (xargs :guard (and (true-listp termlist1)
        (true-listp termlist2)
        (or (consp termlist1) (consp termlist2)))))
  (let ((termlist (append termlist1 termlist2)))
    (cond ((= (len termlist) 1) (car termlist))
      (t (fcons-term 'and termlist)))))

my-conjunctsmutual-recursion

(mutual-recursion (defun my-conjuncts
    (term)
    (cond ((eq term t) nil)
      ((atom term) (list term))
      ((eq (car term) 'and) (my-conjuncts-list (cdr term)))
      (t (list term))))
  (defun my-conjuncts-list
    (termlist)
    (cond ((atom termlist) nil)
      (t (append (my-conjuncts (car termlist))
          (my-conjuncts-list (cdr termlist)))))))

list-type-true-listp-lemmamacro

(defmacro list-type-true-listp-lemma
  (elem-type-fn list-type-fn formals &optional (guard 't))
  (declare (ignore elem-type-fn))
  `(implies ,(MY-CONJOIN (MY-CONJUNCTS GUARD) `((,LIST-TYPE-FN ,@FORMALS)))
    (true-listp l)))

list-type-true-listp00theorem

(defthm list-type-true-listp00
  (list-type-true-listp-lemma elem-type00 list-type00 (l))
  :rule-classes :forward-chaining :hints (("Goal" :induct t)))

list-type-true-listp10theorem

(defthm list-type-true-listp10
  (list-type-true-listp-lemma elem-type10 list-type10 (l a))
  :rule-classes :forward-chaining :hints (("Goal" :induct t)))

list-type-true-listp11theorem

(defthm list-type-true-listp11
  (list-type-true-listp-lemma elem-type11 list-type11 (a l))
  :rule-classes :forward-chaining :hints (("Goal" :induct t)))

list-type-cons-lemmamacro

(defmacro list-type-cons-lemma
  (elem-type-fn list-type-fn formals &optional (guard 't))
  (let* ((vars (unique-symbols 1
         (intern-in-package-of-symbol "X" list-type-fn)
         formals)) (var (car vars)))
    `(implies ,(MY-CONJOIN (MY-CONJUNCTS GUARD)
  `((,ELEM-TYPE-FN
     ,@(IF (SYMBOLP ELEM-TYPE-FN)
           (REPLACE-EQUAL 'L VAR FORMALS)
           (LIST VAR)))
    (,LIST-TYPE-FN ,@FORMALS)))
      (,LIST-TYPE-FN ,@(REPLACE-EQUAL 'L `(CONS ,VAR L) FORMALS)))))

list-type-cons00theorem

(defthm list-type-cons00
  (list-type-cons-lemma elem-type00 list-type00 (l))
  :rule-classes nil)

list-type-cons10theorem

(defthm list-type-cons10
  (list-type-cons-lemma elem-type10 list-type10 (l a))
  :rule-classes nil)

list-type-cons11theorem

(defthm list-type-cons11
  (list-type-cons-lemma elem-type11 list-type11 (a l))
  :rule-classes nil)

list-type-cdr-lemmamacro

(defmacro list-type-cdr-lemma
  (elem-type-fn list-type-fn formals &optional (guard 't))
  (declare (ignore elem-type-fn))
  `(implies ,(MY-CONJOIN (MY-CONJUNCTS GUARD) `((,LIST-TYPE-FN ,@FORMALS)))
    (,LIST-TYPE-FN ,@(REPLACE-EQUAL 'L '(CDR L) FORMALS))))

list-type-cdr00theorem

(defthm list-type-cdr00
  (list-type-cdr-lemma elem-type00 list-type00 (l)))

list-type-cdr10theorem

(defthm list-type-cdr10
  (list-type-cdr-lemma elem-type10 list-type10 (l a)))

list-type-cdr11theorem

(defthm list-type-cdr11
  (list-type-cdr-lemma elem-type11 list-type11 (a l)))

in-theory

(in-theory (disable list-type-cdr00 list-type-cdr10 list-type-cdr11))

list-type-append-lemmamacro

(defmacro list-type-append-lemma
  (elem-type-fn list-type-fn formals &optional (guard 't))
  (declare (ignore elem-type-fn))
  (let* ((vars (unique-symbols 2
         (intern-in-package-of-symbol "L" list-type-fn)
         formals)) (var1 (car vars))
      (var2 (cadr vars)))
    `(implies ,(MY-CONJOIN (MY-CONJUNCTS GUARD) `((TRUE-LISTP ,VAR1)))
      (equal (,LIST-TYPE-FN ,@(REPLACE-EQUAL 'L `(APPEND ,VAR1 ,VAR2) FORMALS))
        (and (,LIST-TYPE-FN ,@(REPLACE-EQUAL 'L VAR1 FORMALS))
          (,LIST-TYPE-FN ,@(REPLACE-EQUAL 'L VAR2 FORMALS)))))))

list-type-append00theorem

(defthm list-type-append00
  (list-type-append-lemma elem-type00 list-type00 (l))
  :rule-classes nil
  :hints (("Goal" :induct t)))

list-type-append10theorem

(defthm list-type-append10
  (list-type-append-lemma elem-type10 list-type10 (l a))
  :rule-classes nil
  :hints (("Goal" :induct t)))

list-type-append11theorem

(defthm list-type-append11
  (list-type-append-lemma elem-type11 list-type11 (a l))
  :rule-classes nil
  :hints (("Goal" :induct t)))

list-type-firstn-lemmamacro

(defmacro list-type-firstn-lemma
  (elem-type-fn list-type-fn formals &optional (guard 't))
  (declare (ignore elem-type-fn))
  (let* ((vars (unique-symbols 1
         (intern-in-package-of-symbol "N" list-type-fn)
         formals)) (var (car vars)))
    `(implies ,(MY-CONJOIN (MY-CONJUNCTS GUARD) `((,LIST-TYPE-FN ,@FORMALS)))
      (,LIST-TYPE-FN ,@(REPLACE-EQUAL 'L `(FIRSTN ,VAR L) FORMALS)))))

list-type-firstn00theorem

(defthm list-type-firstn00
  (list-type-firstn-lemma elem-type00 list-type00 (l))
  :rule-classes nil
  :hints (("Goal" :induct t :in-theory (enable list-type-cdr00))))

list-type-firstn10theorem

(defthm list-type-firstn10
  (list-type-firstn-lemma elem-type10 list-type10 (l a))
  :rule-classes nil
  :hints (("Goal" :induct t :in-theory (enable list-type-cdr10))))

list-type-firstn11theorem

(defthm list-type-firstn11
  (list-type-firstn-lemma elem-type11 list-type11 (a l))
  :rule-classes nil
  :hints (("Goal" :induct t :in-theory (enable list-type-cdr11))))

list-type-last-lemmamacro

(defmacro list-type-last-lemma
  (elem-type-fn list-type-fn formals &optional (guard 't))
  (declare (ignore elem-type-fn))
  `(implies ,(MY-CONJOIN (MY-CONJUNCTS GUARD) `((,LIST-TYPE-FN ,@FORMALS)))
    (,LIST-TYPE-FN ,@(REPLACE-EQUAL 'L '(LAST L) FORMALS))))

list-type-last00theorem

(defthm list-type-last00
  (list-type-last-lemma elem-type00 list-type00 (l))
  :rule-classes nil
  :hints (("Goal" :induct t)))

list-type-last10theorem

(defthm list-type-last10
  (list-type-last-lemma elem-type10 list-type10 (l a))
  :rule-classes nil
  :hints (("Goal" :induct t)))

list-type-last11theorem

(defthm list-type-last11
  (list-type-last-lemma elem-type11 list-type11 (a l))
  :rule-classes nil
  :hints (("Goal" :induct t)))

list-type-make-list-lemmamacro

(defmacro list-type-make-list-lemma
  (elem-type-fn list-type-fn formals &optional (guard 't))
  (let* ((vars (unique-symbols 3
         (intern-in-package-of-symbol "X" list-type-fn)
         formals)) (var1 (car vars))
      (var2 (cadr vars))
      (var3 (caddr vars))
      (guards (my-conjuncts guard))
      (rule `(iff (,LIST-TYPE-FN ,@(REPLACE-EQUAL 'L `(MAKE-LIST-AC ,VAR1 ,VAR2 ,VAR3) FORMALS))
          (and (or (zp ,VAR1)
              (,ELEM-TYPE-FN ,@(IF (SYMBOLP ELEM-TYPE-FN)
      (REPLACE-EQUAL 'L VAR2 FORMALS)
      (LIST VAR2))))
            (,LIST-TYPE-FN ,@(REPLACE-EQUAL 'L VAR3 FORMALS))))))
    (cond (guards `(implies ,(MY-CONJOIN GUARDS NIL) ,RULE))
      (t rule))))

list-type-make-list00theorem

(defthm list-type-make-list00
  (list-type-make-list-lemma elem-type00 list-type00 (l))
  :rule-classes nil
  :hints (("Goal" :induct t :in-theory (enable list-type-cdr00))))

list-type-make-list10theorem

(defthm list-type-make-list10
  (list-type-make-list-lemma elem-type10 list-type10 (l a))
  :rule-classes nil
  :hints (("Goal" :induct t :in-theory (enable list-type-cdr10))))

list-type-make-list11theorem

(defthm list-type-make-list11
  (list-type-make-list-lemma elem-type11 list-type11 (a l))
  :rule-classes nil
  :hints (("Goal" :induct t :in-theory (enable list-type-cdr11))))

list-type-nthcdr-lemmamacro

(defmacro list-type-nthcdr-lemma
  (elem-type-fn list-type-fn formals &optional (guard 't))
  (declare (ignore elem-type-fn))
  (let* ((vars (unique-symbols 1
         (intern-in-package-of-symbol "N" list-type-fn)
         formals)) (var (car vars)))
    `(implies ,(MY-CONJOIN (MY-CONJUNCTS GUARD) `((,LIST-TYPE-FN ,@FORMALS)))
      (,LIST-TYPE-FN ,@(REPLACE-EQUAL 'L `(NTHCDR ,VAR L) FORMALS)))))

list-type-nthcdr00theorem

(defthm list-type-nthcdr00
  (list-type-nthcdr-lemma elem-type00 list-type00 (l))
  :hints (("Goal" :induct t :in-theory (enable list-type-cdr00))))

list-type-nthcdr10theorem

(defthm list-type-nthcdr10
  (list-type-nthcdr-lemma elem-type10 list-type10 (l a))
  :hints (("Goal" :induct t :in-theory (enable list-type-cdr10))))

list-type-nthcdr11theorem

(defthm list-type-nthcdr11
  (list-type-nthcdr-lemma elem-type11 list-type11 (a l))
  :hints (("Goal" :induct t :in-theory (enable list-type-cdr11))))

list-type-nth-seg-lemmamacro

(defmacro list-type-nth-seg-lemma
  (elem-type-fn list-type-fn formals &optional (guard 't))
  (declare (ignore elem-type-fn))
  (let* ((vars (unique-symbols 2
         (intern-in-package-of-symbol "N" list-type-fn)
         formals)) (var1 (car vars))
      (var2 (cadr vars)))
    `(implies ,(MY-CONJOIN (MY-CONJUNCTS GUARD) `((,LIST-TYPE-FN ,@FORMALS)))
      (,LIST-TYPE-FN ,@(REPLACE-EQUAL 'L `(NTH-SEG ,VAR1 ,VAR2 L) FORMALS)))))

list-type-nth-seg00theorem

(defthm list-type-nth-seg00
  (list-type-nth-seg-lemma elem-type00 list-type00 (l))
  :rule-classes nil
  :hints (("Goal" :induct t :in-theory (enable list-type-cdr00))))

list-type-nth-seg10theorem

(defthm list-type-nth-seg10
  (list-type-nth-seg-lemma elem-type10 list-type10 (l a))
  :rule-classes nil
  :hints (("Goal" :induct t :in-theory (enable list-type-cdr10))))

list-type-nth-seg11theorem

(defthm list-type-nth-seg11
  (list-type-nth-seg-lemma elem-type11 list-type11 (a l))
  :rule-classes nil
  :hints (("Goal" :induct t :in-theory (enable list-type-cdr11))))

list-type-put-nth-lemmamacro

(defmacro list-type-put-nth-lemma
  (elem-type-fn list-type-fn formals &optional (guard 't))
  (let* ((vars (unique-symbols 2
         (intern-in-package-of-symbol "N" list-type-fn)
         formals)) (var1 (car vars))
      (var2 (cadr vars)))
    `(implies ,(MY-CONJOIN (MY-CONJUNCTS GUARD) `((,LIST-TYPE-FN ,@FORMALS)))
      (iff (,LIST-TYPE-FN ,@(REPLACE-EQUAL 'L `(PUT-NTH ,VAR1 ,VAR2 L) FORMALS))
        (if (< (nfix ,VAR1) (len l))
          (,ELEM-TYPE-FN ,@(IF (SYMBOLP ELEM-TYPE-FN)
      (REPLACE-EQUAL 'L VAR2 FORMALS)
      (LIST VAR2)))
          t)))))

list-type-put-nth00theorem

(defthm list-type-put-nth00
  (list-type-put-nth-lemma elem-type00 list-type00 (l))
  :rule-classes nil
  :hints (("Goal" :induct t :in-theory (enable list-type-cdr00))))

list-type-put-nth10theorem

(defthm list-type-put-nth10
  (list-type-put-nth-lemma elem-type10 list-type10 (l a))
  :rule-classes nil
  :hints (("Goal" :induct t :in-theory (enable list-type-cdr10))))

list-type-put-nth11theorem

(defthm list-type-put-nth11
  (list-type-put-nth-lemma elem-type11 list-type11 (a l))
  :rule-classes nil
  :hints (("Goal" :induct t :in-theory (enable list-type-cdr11))))

list-type-put-seg-lemmamacro

(defmacro list-type-put-seg-lemma
  (elem-type-fn list-type-fn formals &optional (guard 't))
  (declare (ignore elem-type-fn))
  (let* ((vars (unique-symbols 2
         (intern-in-package-of-symbol "N" list-type-fn)
         formals)) (var1 (car vars))
      (var2 (cadr vars)))
    `(implies ,(MY-CONJOIN (MY-CONJUNCTS GUARD)
  `((,LIST-TYPE-FN ,@FORMALS)
    (,LIST-TYPE-FN ,@(REPLACE-EQUAL 'L VAR2 FORMALS))))
      (,LIST-TYPE-FN ,@(REPLACE-EQUAL 'L `(PUT-SEG ,VAR1 ,VAR2 L) FORMALS)))))

list-type-put-seg00theorem

(defthm list-type-put-seg00
  (list-type-put-seg-lemma elem-type00 list-type00 (l))
  :rule-classes nil
  :hints (("Goal" :induct t :in-theory (enable list-type-cdr00))))

list-type-put-seg10theorem

(defthm list-type-put-seg10
  (list-type-put-seg-lemma elem-type10 list-type10 (l a))
  :rule-classes nil
  :hints (("Goal" :induct t :in-theory (enable list-type-cdr10))))

list-type-put-seg11theorem

(defthm list-type-put-seg11
  (list-type-put-seg-lemma elem-type11 list-type11 (a l))
  :rule-classes nil
  :hints (("Goal" :induct t :in-theory (enable list-type-cdr11))))

list-type-remove-equal-lemmamacro

(defmacro list-type-remove-equal-lemma
  (elem-type-fn list-type-fn formals &optional (guard 't))
  (declare (ignore elem-type-fn))
  (let* ((vars (unique-symbols 1
         (intern-in-package-of-symbol "N" list-type-fn)
         formals)) (var (car vars)))
    `(implies ,(MY-CONJOIN (MY-CONJUNCTS GUARD) `((,LIST-TYPE-FN ,@FORMALS)))
      (,LIST-TYPE-FN ,@(REPLACE-EQUAL 'L `(REMOVE-EQUAL ,VAR L) FORMALS)))))

list-type-remove-equal00theorem

(defthm list-type-remove-equal00
  (list-type-remove-equal-lemma elem-type00 list-type00 (l))
  :rule-classes nil
  :hints (("Goal" :induct t :in-theory (enable list-type-cdr00))))

list-type-remove-equal10theorem

(defthm list-type-remove-equal10
  (list-type-remove-equal-lemma elem-type10 list-type10 (l a))
  :rule-classes nil
  :hints (("Goal" :induct t :in-theory (enable list-type-cdr10))))

list-type-remove-equal11theorem

(defthm list-type-remove-equal11
  (list-type-remove-equal-lemma elem-type11 list-type11 (a l))
  :rule-classes nil
  :hints (("Goal" :induct t :in-theory (enable list-type-cdr11))))

list-type-revappend-lemmamacro

(defmacro list-type-revappend-lemma
  (elem-type-fn list-type-fn formals &optional (guard 't))
  (declare (ignore elem-type-fn))
  (let* ((vars (unique-symbols 2
         (intern-in-package-of-symbol "L" list-type-fn)
         formals)) (var1 (car vars))
      (var2 (cadr vars)))
    `(implies ,(MY-CONJOIN (MY-CONJUNCTS GUARD)
  `((,LIST-TYPE-FN ,@(REPLACE-EQUAL 'L VAR1 FORMALS))
    (,LIST-TYPE-FN ,@(REPLACE-EQUAL 'L VAR2 FORMALS))))
      (,LIST-TYPE-FN ,@(REPLACE-EQUAL 'L `(REVAPPEND ,VAR1 ,VAR2) FORMALS)))))

list-type-revappend00theorem

(defthm list-type-revappend00
  (list-type-revappend-lemma elem-type00 list-type00 (l))
  :hints (("Goal" :induct t :in-theory (enable list-type-cdr00))))

list-type-revappend10theorem

(defthm list-type-revappend10
  (list-type-revappend-lemma elem-type10 list-type10 (l a))
  :hints (("Goal" :induct t :in-theory (enable list-type-cdr10))))

list-type-revappend11theorem

(defthm list-type-revappend11
  (list-type-revappend-lemma elem-type11 list-type11 (a l))
  :hints (("Goal" :induct t :in-theory (enable list-type-cdr11))))

in-theory

(in-theory (disable list-type-revappend00
    list-type-revappend10
    list-type-revappend11))

list-type-reverse-lemmamacro

(defmacro list-type-reverse-lemma
  (elem-type-fn list-type-fn formals &optional (guard 't))
  (declare (ignore elem-type-fn))
  `(implies ,(MY-CONJOIN (MY-CONJUNCTS GUARD) `((,LIST-TYPE-FN ,@FORMALS)))
    (,LIST-TYPE-FN ,@(REPLACE-EQUAL 'L '(REVERSE L) FORMALS))))

list-type-reverse00theorem

(defthm list-type-reverse00
  (list-type-reverse-lemma elem-type00 list-type00 (l))
  :rule-classes nil
  :hints (("Goal" :do-not-induct t
     :in-theory (enable list-type-revappend00))))

list-type-reverse10theorem

(defthm list-type-reverse10
  (list-type-reverse-lemma elem-type10 list-type10 (l a))
  :rule-classes nil
  :hints (("Goal" :do-not-induct t
     :in-theory (enable list-type-revappend10))))

list-type-reverse11theorem

(defthm list-type-reverse11
  (list-type-reverse-lemma elem-type11 list-type11 (a l))
  :rule-classes nil
  :hints (("Goal" :do-not-induct t
     :in-theory (enable list-type-revappend11))))

list-type-take-lemmamacro

(defmacro list-type-take-lemma
  (elem-type-fn list-type-fn formals &optional (guard 't))
  (declare (ignore elem-type-fn))
  (let* ((nvars (unique-symbols 1
         (intern-in-package-of-symbol "N" list-type-fn)
         formals)) (nvar (car nvars)))
    `(implies ,(MY-CONJOIN (MY-CONJUNCTS GUARD)
  `((,LIST-TYPE-FN ,@FORMALS) (<= ,NVAR (LEN L))))
      (,LIST-TYPE-FN ,@(REPLACE-EQUAL 'L `(TAKE ,NVAR L) FORMALS)))))

list-type-take00theorem

(defthm list-type-take00
  (list-type-take-lemma elem-type00 list-type00 (l))
  :hints (("Goal" :induct t
     :in-theory (enable list-type-cdr00 list-type-revappend00))))

list-type-take10theorem

(defthm list-type-take10
  (list-type-take-lemma elem-type10 list-type10 (l a))
  :hints (("Goal" :induct t
     :in-theory (enable list-type-cdr10 list-type-revappend10))))

list-type-take11theorem

(defthm list-type-take11
  (list-type-take-lemma elem-type11 list-type11 (a l))
  :hints (("Goal" :induct t
     :in-theory (enable list-type-cdr11 list-type-revappend11))))

list-type-butlast-lemmamacro

(defmacro list-type-butlast-lemma
  (elem-type-fn list-type-fn formals &optional (guard 't))
  (declare (ignore elem-type-fn))
  (let* ((vars (unique-symbols 1
         (intern-in-package-of-symbol "N" list-type-fn)
         formals)) (var (car vars)))
    `(implies ,(MY-CONJOIN (MY-CONJUNCTS GUARD) `((,LIST-TYPE-FN ,@FORMALS) (<= 0 ,VAR)))
      (,LIST-TYPE-FN ,@(REPLACE-EQUAL 'L `(BUTLAST L ,VAR) FORMALS)))))

list-type-butlast00theorem

(defthm list-type-butlast00
  (list-type-butlast-lemma elem-type00 list-type00 (l))
  :rule-classes nil
  :hints (("Goal" :do-not-induct t
     :in-theory (e/d (butlast) (take-is-xfirstn first-n-ac-non-recursive)))))

list-type-butlast10theorem

(defthm list-type-butlast10
  (list-type-butlast-lemma elem-type10 list-type10 (l a))
  :rule-classes nil
  :hints (("Goal" :do-not-induct t
     :in-theory (e/d (butlast) (take-is-xfirstn first-n-ac-non-recursive)))))

list-type-butlast11theorem

(defthm list-type-butlast11
  (list-type-butlast-lemma elem-type11 list-type11 (a l))
  :rule-classes nil
  :hints (("Goal" :do-not-induct t
     :in-theory (e/d (butlast) (take-is-xfirstn first-n-ac-non-recursive)))))

list-type-subseq-lemmamacro

(defmacro list-type-subseq-lemma
  (elem-type-fn list-type-fn formals &optional (guard 't))
  (declare (ignore elem-type-fn))
  (let* ((startvars (unique-symbols 1
         (intern-in-package-of-symbol "START" list-type-fn)
         formals)) (startvar (car startvars))
      (endvars (unique-symbols 1
          (intern-in-package-of-symbol "END" list-type-fn)
          formals))
      (endvar (car endvars)))
    `(implies ,(MY-CONJOIN (MY-CONJUNCTS GUARD)
  `((,LIST-TYPE-FN ,@FORMALS) (INTEGERP ,STARTVAR) (<= 0 ,STARTVAR)
    (<= ,STARTVAR (LEN L))
    (OR (NULL ,ENDVAR) (AND (INTEGERP ,ENDVAR) (<= ,ENDVAR (LEN L))))))
      (,LIST-TYPE-FN ,@(REPLACE-EQUAL 'L `(SUBSEQ L ,STARTVAR ,ENDVAR) FORMALS)))))

list-type-subseq00theorem

(defthm list-type-subseq00
  (list-type-subseq-lemma elem-type00 list-type00 (l))
  :rule-classes nil
  :hints (("Goal" :do-not-induct t
     :in-theory (e/d (subseq) (take-is-xfirstn first-n-ac-non-recursive)))))

list-type-subseq10theorem

(defthm list-type-subseq10
  (list-type-subseq-lemma elem-type10 list-type10 (l a))
  :rule-classes nil
  :hints (("Goal" :do-not-induct t
     :in-theory (e/d (subseq) (take-is-xfirstn first-n-ac-non-recursive)))))

list-type-subseq11theorem

(defthm list-type-subseq11
  (list-type-subseq-lemma elem-type11 list-type11 (a l))
  :rule-classes nil
  :hints (("Goal" :do-not-induct t
     :in-theory (e/d (subseq) (take-is-xfirstn first-n-ac-non-recursive)))))

list-type-update-nth-lemmamacro

(defmacro list-type-update-nth-lemma
  (elem-type-fn list-type-fn formals &optional (guard 't))
  (let* ((nvars (unique-symbols 1
         (intern-in-package-of-symbol "N" list-type-fn)
         formals)) (nvar (car nvars))
      (valvars (unique-symbols 1
          (intern-in-package-of-symbol "VAL" list-type-fn)
          formals))
      (valvar (car valvars)))
    `(implies ,(MY-CONJOIN (MY-CONJUNCTS GUARD)
  `((,LIST-TYPE-FN ,@FORMALS)
    (,ELEM-TYPE-FN
     ,@(IF (SYMBOLP ELEM-TYPE-FN)
           (REPLACE-EQUAL 'L VALVAR FORMALS)
           (LIST VALVAR)))
    (<= ,NVAR (LEN L))))
      (,LIST-TYPE-FN ,@(REPLACE-EQUAL 'L `(UPDATE-NTH ,NVAR ,VALVAR L) FORMALS)))))

list-type-update-nth00theorem

(defthm list-type-update-nth00
  (list-type-update-nth-lemma elem-type00 list-type00 (l))
  :rule-classes nil)

list-type-update-nth10theorem

(defthm list-type-update-nth10
  (list-type-update-nth-lemma elem-type10 list-type10 (l a))
  :rule-classes nil)

list-type-update-nth11theorem

(defthm list-type-update-nth11
  (list-type-update-nth-lemma elem-type11 list-type11 (a l))
  :rule-classes nil)

list-type-initial-sublistp-equal-lemmamacro

(defmacro list-type-initial-sublistp-equal-lemma
  (elem-type-fn list-type-fn formals &optional (guard 't))
  (declare (ignore elem-type-fn))
  (let* ((xvars (unique-symbols 1
         (intern-in-package-of-symbol "X" list-type-fn)
         formals)) (xvar (car xvars)))
    `(implies ,(MY-CONJOIN (MY-CONJUNCTS GUARD)
  `((,LIST-TYPE-FN ,@FORMALS) (TRUE-LISTP ,XVAR)
    (INITIAL-SUBLISTP-EQUAL ,XVAR L)))
      (,LIST-TYPE-FN ,@(REPLACE-EQUAL 'L XVAR FORMALS)))))

list-type-initial-sublistp-equal00theorem

(defthm list-type-initial-sublistp-equal00
  (list-type-initial-sublistp-equal-lemma elem-type00
    list-type00
    (l))
  :rule-classes nil
  :hints (("Goal" :induct t :in-theory (enable list-type-cdr00))))

list-type-initial-sublistp-equal10theorem

(defthm list-type-initial-sublistp-equal10
  (list-type-initial-sublistp-equal-lemma elem-type10
    list-type10
    (l a))
  :rule-classes nil
  :hints (("Goal" :induct t :in-theory (enable list-type-cdr10))))

list-type-initial-sublistp-equal11theorem

(defthm list-type-initial-sublistp-equal11
  (list-type-initial-sublistp-equal-lemma elem-type11
    list-type11
    (a l))
  :rule-classes nil
  :hints (("Goal" :induct t :in-theory (enable list-type-cdr11))))

list-type-member-equal-lemmamacro

(defmacro list-type-member-equal-lemma
  (elem-type-fn list-type-fn formals &optional (guard 't))
  (let* ((vars (unique-symbols 1
         (intern-in-package-of-symbol "X" list-type-fn)
         formals)) (var (car vars)))
    `(implies ,(MY-CONJOIN (MY-CONJUNCTS GUARD)
  `((MEMBER-EQUAL ,VAR L) (,LIST-TYPE-FN ,@FORMALS)))
      (,ELEM-TYPE-FN ,@(IF (SYMBOLP ELEM-TYPE-FN)
      (REPLACE-EQUAL 'L VAR FORMALS)
      (LIST VAR))))))

list-type-member-equal00theorem

(defthm list-type-member-equal00
  (list-type-member-equal-lemma elem-type00 list-type00 (l))
  :rule-classes :rewrite :hints (("Goal" :induct t :in-theory (enable list-type-cdr00))))

list-type-member-equal10theorem

(defthm list-type-member-equal10
  (list-type-member-equal-lemma elem-type10 list-type10 (l a))
  :rule-classes :rewrite :hints (("Goal" :induct t :in-theory (enable list-type-cdr10))))

list-type-member-equal11theorem

(defthm list-type-member-equal11
  (list-type-member-equal-lemma elem-type11 list-type11 (a l))
  :rule-classes :rewrite :hints (("Goal" :induct t :in-theory (enable list-type-cdr11))))

list-type-memberp-equal-lemmamacro

(defmacro list-type-memberp-equal-lemma
  (elem-type-fn list-type-fn formals &optional (guard 't))
  (let ((var (intern-in-package-of-symbol "X"
         'x-unlikely-variable-name-x)))
    `(implies ,(MY-CONJOIN `((MEMBERP-EQUAL ,VAR L) (,LIST-TYPE-FN ,@FORMALS))
  (MY-CONJUNCTS GUARD))
      (,ELEM-TYPE-FN ,@(IF (SYMBOLP ELEM-TYPE-FN)
      (REPLACE-EQUAL 'L VAR FORMALS)
      (LIST VAR))))))

list-type-memberp-equal00theorem

(defthm list-type-memberp-equal00
  (list-type-memberp-equal-lemma elem-type00 list-type00 (l))
  :rule-classes nil
  :hints (("Goal" :induct (member-equal x-unlikely-variable-name-x l)
     :in-theory (enable list-type-cdr00 memberp-equal))))

list-type-memberp-equal10theorem

(defthm list-type-memberp-equal10
  (list-type-memberp-equal-lemma elem-type10
    list-type10
    (l a))
  :rule-classes nil
  :hints (("Goal" :induct (member-equal x-unlikely-variable-name-x l)
     :in-theory (enable list-type-cdr10))))

list-type-memberp-equal11theorem

(defthm list-type-memberp-equal11
  (list-type-memberp-equal-lemma elem-type11
    list-type11
    (a l))
  :rule-classes nil
  :hints (("Goal" :induct (member-equal x-unlikely-variable-name-x l)
     :in-theory (enable list-type-cdr11))))

list-type-remove-duplicates-equal-lemmamacro

(defmacro list-type-remove-duplicates-equal-lemma
  (elem-type-fn list-type-fn formals &optional (guard 't))
  (declare (ignore elem-type-fn))
  `(implies ,(MY-CONJOIN (MY-CONJUNCTS GUARD) `((,LIST-TYPE-FN ,@FORMALS)))
    (,LIST-TYPE-FN ,@(REPLACE-EQUAL 'L `(REMOVE-DUPLICATES-EQUAL L) FORMALS))))

list-type-remove-duplicates-equal00theorem

(defthm list-type-remove-duplicates-equal00
  (list-type-remove-duplicates-equal-lemma elem-type00
    list-type00
    (l))
  :hints (("Goal" :induct t)))

list-type-remove-duplicates-equal10theorem

(defthm list-type-remove-duplicates-equal10
  (list-type-remove-duplicates-equal-lemma elem-type10
    list-type10
    (l a))
  :hints (("Goal" :induct t)))

list-type-remove-duplicates-equal11theorem

(defthm list-type-remove-duplicates-equal11
  (list-type-remove-duplicates-equal-lemma elem-type11
    list-type11
    (a l))
  :hints (("Goal" :induct t)))

list-type-car-lemmamacro

(defmacro list-type-car-lemma
  (elem-type-fn list-type-fn formals &optional (guard 't))
  `(implies ,(MY-CONJOIN (MY-CONJUNCTS GUARD) `((,LIST-TYPE-FN ,@FORMALS) L))
    (,ELEM-TYPE-FN ,@(IF (SYMBOLP ELEM-TYPE-FN)
      (REPLACE-EQUAL 'L '(CAR L) FORMALS)
      (LIST '(CAR L))))))

list-type-car00theorem

(defthm list-type-car00
  (list-type-car-lemma elem-type00 list-type00 (l))
  :rule-classes nil)

list-type-car10theorem

(defthm list-type-car10
  (list-type-car-lemma elem-type10 list-type10 (l a))
  :rule-classes nil)

list-type-car11theorem

(defthm list-type-car11
  (list-type-car-lemma elem-type11 list-type11 (a l))
  :rule-classes nil)

list-type-nth-lemmamacro

(defmacro list-type-nth-lemma
  (elem-type-fn list-type-fn formals &optional (guard 't))
  (let* ((vars (unique-symbols 1
         (intern-in-package-of-symbol "N" list-type-fn)
         formals)) (var (car vars)))
    `(implies ,(MY-CONJOIN (MY-CONJUNCTS GUARD)
  `((,LIST-TYPE-FN ,@FORMALS) (< (NFIX ,VAR) (LEN L))))
      (,ELEM-TYPE-FN ,@(IF (SYMBOLP ELEM-TYPE-FN)
      (REPLACE-EQUAL 'L `(NTH ,VAR L) FORMALS)
      (LIST `(NTH ,VAR L)))))))

list-type-nth00theorem

(defthm list-type-nth00
  (list-type-nth-lemma elem-type00 list-type00 (l))
  :rule-classes nil
  :hints (("Goal" :induct t :in-theory (enable list-type-cdr00))))

list-type-nth10theorem

(defthm list-type-nth10
  (list-type-nth-lemma elem-type10 list-type10 (l a))
  :rule-classes nil
  :hints (("Goal" :induct t :in-theory (enable list-type-cdr10))))

list-type-nth11theorem

(defthm list-type-nth11
  (list-type-nth-lemma elem-type11 list-type11 (a l))
  :rule-classes nil
  :hints (("Goal" :induct t :in-theory (enable list-type-cdr11))))

pack-intern-namesfunction

(defun pack-intern-names
  (name1 name2)
  (pack-intern name1 name1 "-" name2))

other

(defloop pack-intern-all-names
  (name l)
  (for ((x in l)) (collect (pack-intern-names name x))))

other

(defloop deflist-defthms
  (list-type-fn formals
    elem-type-fn
    guard
    theory
    car-rule-classes
    nth-rule-classes)
  (declare (xargs :guard (and (symbolp list-type-fn)
        (arglistp formals)
        (consp formals)
        (or (symbolp elem-type-fn)
          (and (consp elem-type-fn)
            (eq (car elem-type-fn) 'lambda)
            (<= (len (cadr elem-type-fn)) 2)))
        (symbol-listp theory))
      :mode :program))
  (for ((fn in theory))
    (collect (let ((lemmaname (pack-intern-names list-type-fn fn)) (lemma-macro-name (pack-intern list-type-fn 'list-type- fn '-lemma))
          (rule-classes (case fn
              (car car-rule-classes)
              (nth nth-rule-classes)
              (true-listp '(:forward-chaining))
              (t '(:rewrite))))
          (hints (if (or (consp (my-conjuncts guard)) (> (len formals) 2))
              `(("Goal" :induct t))
              (let* ((numparams (1- (len formals))) (posn (position-equal 'l formals))
                  (numparams-string (coerce (explode-nonnegative-integer numparams 10 nil)
                      'string))
                  (posn-string (coerce (explode-nonnegative-integer posn 10 nil) 'string))
                  (canonical-elem-type-fn (pack-intern list-type-fn
                      'elem-type
                      numparams-string
                      posn-string))
                  (canonical-list-type-fn (pack-intern list-type-fn
                      'list-type
                      numparams-string
                      posn-string))
                  (lemma-name (pack-intern list-type-fn
                      'list-type-
                      fn
                      numparams-string
                      posn-string))
                  (elem-type-instance (cond ((and (consp elem-type-fn) (eq (car elem-type-fn) 'lambda)) elem-type-fn)
                      (t (let ((elem-formals (replace-equal 'l 'x formals)))
                          `(lambda ,ELEM-FORMALS (,ELEM-TYPE-FN ,@ELEM-FORMALS))))))
                  (subst (case (length formals)
                      (2 `((a ,(CAR (REMOVE 'L FORMALS)))))
                      (t nil))))
                `(("Goal" :do-not-induct t
                   :use (:functional-instance (:instance ,LEMMA-NAME ,@SUBST)
                     (,CANONICAL-ELEM-TYPE-FN ,ELEM-TYPE-INSTANCE)
                     (,CANONICAL-LIST-TYPE-FN ,LIST-TYPE-FN))))))))
        `(defthm ,LEMMANAME
          (,LEMMA-MACRO-NAME ,ELEM-TYPE-FN
            ,LIST-TYPE-FN
            ,FORMALS
            ,GUARD)
          :rule-classes ,RULE-CLASSES
          :hints ,HINTS)))))

*deflist-options*constant

(defconst *deflist-options*
  '(:car-rule-classes :nth-rule-classes :theory :omit-defun :theory-name))

*deflist-theory-options*constant

(defconst *deflist-theory-options*
  '((append) (butlast)
    (cons)
    (car)
    (cdr)
    (firstn)
    (initial-sublistp-equal)
    (last)
    (make-list)
    (member-equal)
    (memberp-equal)
    (nth)
    (nth-seg)
    (nthcdr)
    (put-nth)
    (put-seg)
    (remove-duplicates-equal)
    (remove-equal)
    (reverse)
    (subseq)
    (true-listp)
    (update-nth)))

*forward-chaining-elem-types*constant

(defconst *forward-chaining-elem-types*
  '(integerp rationalp
    complex-rationalp
    symbolp
    true-listp
    stringp
    characterp
    alistp
    acl2-numberp))

my-set-differencefunction

(defun my-set-difference
  (l1 l2)
  (cond ((atom l1) nil)
    ((member-equal (car l1) l2) (my-set-difference (cdr l1) l2))
    (t (cons (car l1) (my-set-difference (cdr l1) l2)))))

insert-dependenciesfunction

(defun insert-dependencies
  (l alist already-seen)
  (cond ((atom l) nil)
    ((member (car l) already-seen) (insert-dependencies (cdr l) alist already-seen))
    (t (let ((pair (assoc-equal (car l) alist)))
        (let ((new (my-set-difference (cdr pair) already-seen)))
          (append new
            (list (car l))
            (insert-dependencies (cdr l)
              alist
              (cons (car l) (append new already-seen)))))))))

other

(deftheory minimal-theory-for-deflist
  (union-theories (current-theory 'ground-zero)
    (current-theory 'list-defuns)))

deflist-check-syntaxfunction

(defun deflist-check-syntax
  (name formals body)
  "Return NIL if no errors, otherwise crash."
  (declare (xargs :mode :program))
  (cond ((not (symbolp name)) (bomb 'deflist
        "The function name must be a symbol, but ~p0 is not."
        name))
    ((not (true-listp formals)) (bomb 'deflist
        "The argument list ~p0 is not a true list."
        formals))
    ((not (arglistp formals)) (mv-let (elmt msg)
        (find-first-bad-arg formals)
        (bomb 'deflist
          "The argument list ~p0 is not valid because the ~
                         element ~p1 ~@2."
          formals
          elmt
          msg)))
    ((let* ((formal-strings (mapcar-string formals)) (l-tail (member-equal "L" formal-strings))
         (multiple-ls (member-equal "L" (cdr l-tail))))
       (or (not l-tail) multiple-ls)) (bomb 'deflist
        "The formal argument list to DEFLIST must be a valid ~
                       functional argument list that contains exactly 1 ~
                       symbol whose print-name is "L", but ~p0 is not."
        formals))
    ((null body) (bomb 'deflist "The function body is empty!"))
    (t (let* ((last-form (car (last body))) (options? (and (>= (len body) 2)
              (true-listp last-form)
              (eq (car last-form) :options)))
          (predicate (if options?
              (car (last (butlast body 1)))
              last-form)))
        (cond ((or (symbolp predicate)
             (and (true-listp predicate)
               (equal (len predicate) 3)
               (eq (first predicate) 'lambda)
               (arglistp (second predicate))
               (<= (len (second predicate)) 2))) nil)
          (t (bomb 'deflist
              "The DEFLIST predicate designator must either ~
                             be a symbol, or a 1 or 2-argument LAMBDA function, ~
                             but ~p0 is not."
              predicate)))))))

other

(defsection deflist
  :parents (data-structures)
  :short "Define a new list type, and a theory of the list type."
  :long "<p>Examples</p>

@({
  (deflist integer-listp (l)
    "Recognizes true-lists of integers."
    integerp)

  (deflist bnatural-listp (l lub)
    "Recognizes lists of naturals bounded by lub."
    (lambda (x) (bnaturalp x lub)))

  (deflist symbol-listp (l)
    "Define a list theory for this function which is already defined by
      Acl2."
    symbolp
    (:options :omit-defun))

  (deflist stringp-listp (l)
    "Recognizes lists of strings; produce a minimal theory, and store the NTH
     lemma as a :TYPE-PRESCRIPTION."
    stringp
    (:options (:theory nth put-nth) (:nth-rule-classes :type-prescription)))
})

<p>Syntax:</p>

@({
   DEFLIST name arglist [documentation] {declaration}* predicate [option-list]

   option-list ::= (:OPTIONS <<!options>>)

   options ::= !car-rule-classes-option |
               !nth-rule-classes-option |
               !omit-defun-option |
               !theory-option |
               !theory-name-option

   theory-name-option ::= (:THEORY-NAME theory-name)

   theory-option ::= (:THEORY <<!list-functions>>)

   list-functions ::= APPEND | BUTLAST | CONS | CAR | CDR |
                      FIRSTN | INITIAL-SUBLISTP-EQUAL | LAST |
                      MAKE-LIST | MEMBER-EQUAL | MEMBERP-EQUAL |
                      NTH | NTH-SEG | NTHCDR | PUT-NTH | PUT-SEG |
                      REMOVE-DUPLICATES-EQUAL | REMOVE-EQUAL |
                      REVERSE | SUBSEQ | UPDATE-NTH

   car-rule-classes-option ::= (:CAR-RULE-CLASSES rule-classes)

   nth-rule-classes-option ::= (:NTH-RULE-CLASSES rule-classes)

   omit-defun-option ::= :OMIT-DEFUN
})

<p>Arguments and Values:</p>

@({
   arglist -- an argument list satisfying ACL2::ARGLISTP, and containing
     exactly one symbol whose `print-name' is "L".

   declaration -- any valid declaration.

   documentation -- a string; not evaluated.

   name -- a symbol.

   predicate -- Either a symbol or a one argument LAMBDA function;
     designates a predicate to be applied to each element of the list.

   rule-classes -- any form legal as an argument to the :RULE-CLASSES keyword
    of DEFTHM.

   theory-name -- any symbol that is a legal name for a deftheory event.
})

<p>DEFLIST defines a recognizer for true lists whose elements all satisfy a
given predicate, and by default creates an extensive theory for lists of the
newly defined type.</p>

<p>To define a list type with DEFLIST you must supply a name for the
recognizer, an argument list, and predicate designator.  The name may be any
symbol.  The argument list must be valid as a functional argument list, and
must contain exactly 1 symbol whose `print-name'is "L".  By convention this
is the list argument recognized by the function defined by DEFLIST.</p>

<p>The DEFLIST recognizer will return T only if each element of L
satisfies (returns a non-NIL value) the given predicate, otherwise NIL.  If the
predicate is specified as a symbol, then this is assumed to be the function
symbol of a one argument function (or macro) with which to test the elements of
L.  If the predicate is specified as a single-argument LAMBDA function, then
the given LAMBDA function will be applied to test successive elements of L.</p>

<p>Any number of other arguments to the function may be supplied, but only the
L argument will change in the recursive structure of the recognizer.</p>

<p>Note that DEFLIST does not create any guards for L or any other argument.
Guards may be specified in the usual way since any number of DECLARE forms may
precede the predicate specification in the DEFLIST form.  DO NOT DECLARE GUARDS
FOR THE LIST ARGUMENT L, as this may cause DEFLIST to blindly generate
unprovable conjectures and unusable theorems.  Bear in mind that if you are
defining a function to be used as a guard, then you are advised to consider
what impact guarding the arguments of the function may have on its utility.  In
general the most useful guard functions are those that are guard-free.</p>

<p>Theory:</p>

<p>By default, DEFLIST creates an extensive theory for the recognized lists.
This theory contains appropriate lemmas for all of the list functions appearing
in the `list-functions' syntax description above.  This list of function
symbols is also available as the Acl2 constant *DEFLIST-THEORY-OPTIONS*.</p>

<p>One can select a subset of this theory to be generated by using the :THEORY
option (see below).  DEFLIST always creates a :FORWARD-CHAINING rule from the
recognizer to TRUE-LISTP.  DEFLIST also creates a DEFTHEORY event that lists
all of the lemmas created by the DEFLIST.  The name of the theory is formed by
concatenating the function name and the string "-THEORY", and interning the
resulting string in the package of the function name.</p>

<p>Options:</p>

<p>DEFLIST options are specified with a special :OPTIONS list systax.  If
present, the :OPTIONS list must appear as the last form in the body of the
DEFLIST.</p>

<dl>
<dt>:OMIT-DEFUN</dt>
<dd>If the :OMIT-DEFUN keyword is present then the definition will not be
    created.  Instead, only the list theory for the function is
    generated. Use this option to create a list theory for recognizers
    defined elsewhere.</dd>

<dt>:THEORY</dt>
<dd>This option is used to specify that only a subset of the list theory be
   created.  In the STRINGP-LISTP example above we specify that only lemmas
   about STRINGP-LISTP viz-a-viz NTH and PUT-NTH are to be generated.  By
   default the complete list theory for the recognizer is created.  If the
   option is given as (:THEORY) then the entire theory will be suppressed,
   except for the :FORWARD-CHAINING rule from the recognizer to TRUE-LISTP.</dd>

<dt>:THEORY-NAME</dt>
<dd>This option allows the user to define the name of the deftheory event
   that is automatically generated, and which includes the defthms that
   are generated.</dd>

<dt>:CAR-RULE-CLASSES</dt>
<dt>:NTH-RULE-CLASSES</dt>

<dd>These options specify a value for the :RULE-CLASSES keyword for the
   DEFTHM generated for the CAR and NTH element of a list recognized by the
   DEFLIST recognizer respectively.  The default is :REWRITE.</dd>
</dl>")

deflistmacro

(defmacro deflist
  (name formals &rest body)
  (let* ((syntax-err (deflist-check-syntax name formals body)) (last-form (car (last body)))
      (options? (and (>= (len body) 2)
          (true-listp last-form)
          (eq (car last-form) :options)))
      (option-list (if options?
          (cdr last-form)
          nil))
      (predicate (if options?
          (car (last (butlast body 1)))
          last-form))
      (guard (get-guards-from-body body))
      (ctx 'deflist)
      (option-err (get-option-check-syntax ctx
          option-list
          *deflist-options*
          nil
          nil))
      (omit-defun (get-option-as-flag ctx :omit-defun option-list))
      (theory (insert-dependencies (get-option-subset ctx
            :theory option-list
            (strip-cars *deflist-theory-options*)
            (strip-cars *deflist-theory-options*))
          *deflist-theory-options*
          nil))
      (theory-name (get-option-argument ctx
          :theory-name option-list
          :form (pack-intern name name "-THEORY")
          (pack-intern name name "-THEORY")))
      (car-rule-classes (get-option-argument ctx
          :car-rule-classes option-list
          :form :rewrite :rewrite))
      (nth-rule-classes (get-option-argument ctx
          :nth-rule-classes option-list
          :form :rewrite :rewrite)))
    (or syntax-err
      option-err
      (let ((theory1 (union-equal '(true-listp) theory)))
        `(encapsulate nil
          (local (deflabel deflist-reserved-label))
          (local (in-theory (theory 'minimal-theory-for-deflist)))
          ,@(IF OMIT-DEFUN
      NIL
      (LIST
       `(DEFUN ,NAME ,FORMALS
          ,@(BUTLAST BODY
                     (IF OPTIONS?
                         2
                         1))
          (COND ((ATOM L) (EQ L NIL))
                (T
                 (AND (,PREDICATE ,@(REPLACE-EQUAL 'L '(CAR L) FORMALS))
                      (,NAME ,@(REPLACE-EQUAL 'L '(CDR L) FORMALS))))))))
          (local (in-theory (enable ,NAME)))
          ,@(DEFLIST-DEFTHMS NAME FORMALS PREDICATE GUARD THEORY1 CAR-RULE-CLASSES
   NTH-RULE-CLASSES)
          (deftheory ,THEORY-NAME
            ',(PACK-INTERN-ALL-NAMES NAME THEORY1)))))))