deflist

(in-package "STD")

(include-book "deflist-base")

(include-book "std/osets/element-list" :dir :system)

(include-book "defsort/duplicated-members" :dir :system)

(include-book "std/lists/sets" :dir :system)

(include-book "std/lists/list-fix" :dir :system)

(include-book "std/lists/take" :dir :system)

(include-book "std/lists/repeat" :dir :system)

(include-book "std/lists/rev" :dir :system)

(local (progn (include-book "std/lists/nth" :dir :system)
    (include-book "std/lists/update-nth" :dir :system)
    (include-book "std/lists/butlast" :dir :system)
    (include-book "std/lists/nthcdr" :dir :system)
    (include-book "std/lists/append" :dir :system)
    (include-book "std/lists/last" :dir :system)
    (include-book "std/lists/rcons" :dir :system)
    (include-book "std/lists/remove" :dir :system)
    (include-book "std/lists/revappend" :dir :system)
    (include-book "defredundant")))

(make-event (let ((tab (table-alist 'listp-rules (w state))))
    `(table listp-rules nil ',STD::TAB :clear)))

(make-event (defredundant-fn (strip-cars (table-alist 'listp-rules (w state)))
    nil
    state))

(defsection deflist-lemmas
  (local (include-book "std/osets/under-set-equiv" :dir :system))
  (local (in-theory (enable* definitions expensive-rules)))
  (defthmd deflist-lemma-member-of-car
    (iff (member-equal (car x) x)
      (consp x)))
  (defthmd deflist-lemma-subsetp-of-set-difference-equal
    (subsetp-equal (set-difference-equal x y)
      x))
  (defthmd deflist-lemma-subsetp-of-intersection-equal
    (and (subsetp-equal (intersection-equal x y)
        x)
      (subsetp-equal (intersection-equal x y)
        y)))
  (defthmd deflist-lemma-subsetp-equal-of-duplicated-members
    (subsetp-equal (duplicated-members x) x)
    :hints (("Goal" :in-theory (enable duplicity)))
    :otf-flg t)
  (defthmd deflist-lemma-subsetp-of-nthcdr
    (subsetp-equal (nthcdr n x) x))
  (defthmd deflist-lemma-true-listp-of-nthcdr
    (equal (true-listp (nthcdr n x))
      (or (< (len x) (nfix n))
        (true-listp x)))
    :hints (("Goal" :induct (nthcdr n x))))
  (defthmd deflist-lemma-subsetp-of-last
    (subsetp-equal (last x) x))
  (defthmd deflist-lemma-true-listp-of-last
    (equal (true-listp (last x))
      (true-listp x)))
  (local (include-book "arithmetic/top-with-meta" :dir :system))
  (local (defthmd c0
      (equal (< (+ a b) (+ a c))
        (< b c))))
  (defthmd deflist-lemma-cancel-negative-constant
    (implies (syntaxp (and (quotep a) (< (unquote a) 0)))
      (equal (< (+ a b) c)
        (< b (+ (- a) c))))
    :hints (("Goal" :use ((:instance c0
          (a (- a))
          (b (+ a b))
          (c c))))))
  (defthmd deflist-lemma-len-over-zero
    (equal (< 0 (len x)) (consp x)))
  (defthmd deflist-lemma-nth-when-zp
    (implies (zp n)
      (equal (nth n x) (car x))))
  (defthmd deflist-lemma-nth-when-atom
    (implies (atom x) (equal (nth n x) nil)))
  (defthmd deflist-lemma-nth-of-cons
    (equal (nth n (cons a x))
      (if (zp n)
        a
        (nth (+ -1 n) x))))
  (local (defthm l0
      (implies (and (member a (take n x))
          (<= (nfix n) (len x)))
        (member a x))
      :hints (("Goal" :in-theory (enable take)))))
  (local (defthm l1
      (implies (<= (nfix n) (len x))
        (subsetp-equal (take n x) x))
      :hints (("Goal" :in-theory (enable take)))))
  (defthmd deflist-lemma-subsetp-of-butlast
    (subsetp-equal (butlast x n) x))
  (defthmd deflist-lemma-true-listp-of-butlast
    (true-listp (butlast x n))
    :rule-classes :type-prescription)
  (defthmd deflist-lemma-sfix-when-not-setp
    (implies (not (setp x))
      (equal (sfix x) nil))
    :hints (("Goal" :in-theory (enable sfix emptyp))))
  (defthmd deflist-lemma-sfix-when-setp
    (implies (setp x)
      (equal (sfix x) x))
    :hints (("Goal" :in-theory (enable sfix emptyp))))
  (defthmd deflist-lemma-subsetp-of-difference
    (subsetp-equal (difference x y) x))
  (local (defthm g1
      (implies (member a (sfix x))
        (member a x))
      :hints (("Goal" :do-not-induct t
         :use ((:instance in-to-member
            (a a)
            (x (sfix x))))))))
  (defthmd deflist-lemma-subsetp-of-intersect
    (and (subsetp-equal (intersect x y) x)
      (subsetp-equal (intersect x y) y))
    :hints (("Goal" :do-not-induct t)))
  (defthmd deflist-lemma-true-listp-of-sfix
    (true-listp (sfix x))
    :rule-classes :type-prescription)
  (defthmd deflist-lemma-subsetp-of-union
    (and (subsetp-equal (sfix x)
        (union x y))
      (subsetp-equal (sfix y)
        (union x y))
      (subsetp-equal (union x y)
        (append (sfix x) (sfix y))))))

(deftheory deflist-support-lemmas
  '((:type-prescription intersection-equal) (:type-prescription set-difference-equal)
    (:type-prescription duplicated-members)
    (:t list-fix)
    (:type-prescription rev)
    (:type-prescription len)
    deflist-lemma-member-of-car
    deflist-lemma-subsetp-of-set-difference-equal
    deflist-lemma-subsetp-of-intersection-equal
    deflist-lemma-subsetp-equal-of-duplicated-members
    deflist-lemma-cancel-negative-constant
    deflist-lemma-len-over-zero
    deflist-lemma-nth-when-zp
    deflist-lemma-nth-when-atom
    deflist-lemma-nth-of-cons
    deflist-lemma-sfix-when-not-setp
    deflist-lemma-sfix-when-setp
    deflist-lemma-subsetp-of-nthcdr
    deflist-lemma-subsetp-of-last
    deflist-lemma-subsetp-of-butlast
    deflist-lemma-true-listp-of-last
    deflist-lemma-true-listp-of-butlast
    deflist-lemma-true-listp-of-nthcdr
    deflist-lemma-subsetp-of-difference
    deflist-lemma-subsetp-of-intersect
    deflist-lemma-true-listp-of-sfix
    deflist-lemma-subsetp-of-union
    car-cons
    cdr-cons
    car-cdr-elim
    zp
    len
    natp
    nth
    update-nth
    nfix
    default-+-2
    default-<-1
    default-unary-minus
    unicity-of-0
    take
    list-fix-when-not-consp
    list-fix-when-true-listp
    list-fix-of-cons
    sets-are-true-lists
    mergesort-set
    union-set
    intersect-set
    difference-set
    set-equiv-implies-equal-subsetp-1
    set-equiv-implies-equal-subsetp-2
    subsetp-refl
    list-fix-under-list-equiv
    mergesort-under-set-equiv
    binary-append-without-guard))