reverse-list

other

(in-package "ACL2")

local

(local (include-book "append"))

local

(local (include-book "nth"))

local

(local (include-book "take"))

local

(local (include-book "nthcdr"))

local

(local (include-book "true-list-fix"))

local

(local (include-book "no-duplicatesp-equal"))

local

(local (in-theory (disable reverse revappend)))

reverse-listfunction

(defund reverse-list
  (x)
  (declare (xargs :guard (true-listp x) :verify-guards nil))
  (mbe :logic (if (consp x)
      (append (reverse-list (cdr x)) (list (car x)))
      nil)
    :exec (revappend x nil)))

revappend-becomes-append-of-reverse-listtheorem

(defthmd revappend-becomes-append-of-reverse-list
  (equal (revappend x acc) (append (reverse-list x) acc))
  :hints (("Goal" :in-theory (enable reverse-list revappend append))))

other

(verify-guards reverse-list
  :hints (("Goal" :expand ((reverse-list x))
     :in-theory (e/d (revappend-becomes-append-of-reverse-list)
       (append-of-nil-arg2)))))

reverse-becomes-reverse-listtheorem

(defthm reverse-becomes-reverse-list
  (implies (true-listp x)
    (equal (reverse x) (reverse-list x)))
  :hints (("Goal" :in-theory (enable reverse
       reverse-list
       revappend-becomes-append-of-reverse-list))))

reverse-becomes-reverse-list-gentheorem

(defthm reverse-becomes-reverse-list-gen
  (implies (not (stringp x))
    (equal (reverse x) (reverse-list x)))
  :hints (("Goal" :in-theory (enable reverse
       reverse-list
       revappend-becomes-append-of-reverse-list))))

true-listp-of-reverse-listtheorem

(defthm true-listp-of-reverse-list
  (true-listp (reverse-list x))
  :hints (("Goal" :in-theory (enable reverse-list))))

reverse-list-ifftheorem

(defthm reverse-list-iff
  (iff (reverse-list y) (consp y))
  :hints (("Goal" :in-theory (enable reverse-list))))

len-of-reverse-listtheorem

(defthm len-of-reverse-list
  (equal (len (reverse-list y)) (len y))
  :hints (("Goal" :in-theory (enable reverse-list))))

consp-of-reverse-listtheorem

(defthm consp-of-reverse-list
  (equal (consp (reverse-list x)) (consp x))
  :hints (("Goal" :in-theory (enable reverse-list))))

endp-of-reverse-listtheorem

(defthm endp-of-reverse-list
  (equal (endp (reverse-list x)) (endp x))
  :hints (("Goal" :in-theory (enable reverse-list))))

reverse-list-of-appendtheorem

(defthm reverse-list-of-append
  (equal (reverse-list (append x y))
    (append (reverse-list y) (reverse-list x)))
  :hints (("Goal" :in-theory (enable reverse-list append))))

reverse-list-of-reverse-listtheorem

(defthm reverse-list-of-reverse-list
  (equal (reverse-list (reverse-list x)) (true-list-fix x))
  :hints (("Goal" :in-theory (enable reverse-list append))))

reverse-list-of-constheorem

(defthm reverse-list-of-cons
  (equal (reverse-list (cons a x))
    (append (reverse-list x) (list a)))
  :hints (("Goal" :in-theory (enable reverse-list))))

car-of-reverse-listtheorem

(defthm car-of-reverse-list
  (equal (car (reverse-list x)) (nth (+ -1 (len x)) x))
  :hints (("Goal" :in-theory (enable reverse-list append))))

car-of-reverse-list-2theorem

(defthmd car-of-reverse-list-2
  (equal (car (reverse-list x)) (car (last x))))

reverse-list-of-true-list-fixtheorem

(defthm reverse-list-of-true-list-fix
  (equal (reverse-list (true-list-fix x)) (reverse-list x))
  :hints (("Goal" :in-theory (enable reverse-list))))

member-equal-of-reverse-list-ifftheorem

(defthm member-equal-of-reverse-list-iff
  (iff (member-equal x (reverse-list y)) (member-equal x y))
  :hints (("Goal" :in-theory (enable reverse-list))))

local

(local (defthm nth-of-reverse-list-simple
    (implies (and (natp n) (< n (len x)))
      (equal (nth n (reverse-list x))
        (nth (+ -1 (len x) (- (nfix n))) x)))
    :hints (("Goal" :in-theory (e/d (reverse-list nth) (nth-of-cdr))))))

local

(local (defthm nth-of-reverse-list-helper
    (implies (natp n)
      (equal (nth n (reverse-list x))
        (if (< n (len x))
          (nth (+ -1 (len x) (- (nfix n))) x)
          nil)))
    :hints (("Goal" :in-theory (enable nth-when-<=-len)))))

nth-of-reverse-listtheorem

(defthm nth-of-reverse-list
  (equal (nth n (reverse-list x))
    (if (< (nfix n) (len x))
      (nth (+ -1 (len x) (- (nfix n))) x)
      nil)))

cdr-of-reverse-listtheorem

(defthm cdr-of-reverse-list
  (equal (cdr (reverse-list lst))
    (reverse-list (take (+ -1 (len lst)) lst)))
  :hints (("Goal" :in-theory (enable reverse-list take))))

last-of-reverse-listtheorem

(defthm last-of-reverse-list
  (equal (last (reverse-list x))
    (if (consp x)
      (list (car x))
      nil))
  :hints (("Goal" :in-theory (enable reverse-list))))

take-of-reverse-listtheorem

(defthm take-of-reverse-list
  (implies (and (<= n (len x)) (natp n))
    (equal (take n (reverse-list x))
      (reverse-list (nthcdr (- (len x) n) x))))
  :hints (("Goal" :in-theory (enable reverse-list nthcdr))))

butlast-of-reverse-listtheorem

(defthm butlast-of-reverse-list
  (equal (butlast (reverse-list x) n)
    (reverse-list (nthcdr n x)))
  :hints (("Goal" :in-theory (enable butlast reverse-list nthcdr))))

nthcdr-of-reverse-listtheorem

(defthm nthcdr-of-reverse-list
  (implies (and (<= n (len x)) (natp n))
    (equal (nthcdr n (reverse-list x))
      (reverse-list (take (- (len x) n) x))))
  :hints (("Goal" :in-theory (enable nthcdr reverse-list))))

equal-of-reverse-listtheorem

(defthmd equal-of-reverse-list
  (equal (equal x (reverse-list y))
    (and (true-listp x)
      (equal (true-list-fix y) (reverse-list x))))
  :hints (("Goal" :use (:instance reverse-list-of-true-list-fix (x y))
     :in-theory (disable reverse-list-of-true-list-fix))))

equal-of-reverse-list-and-reverse-listtheorem

(defthm equal-of-reverse-list-and-reverse-list
  (equal (equal (reverse-list x) (reverse-list y))
    (equal (true-list-fix x) (true-list-fix y)))
  :hints (("Goal" :use (:instance equal-of-reverse-list (x (reverse-list x))))))

intersection-equal-of-reverse-list-arg1-ifftheorem

(defthm intersection-equal-of-reverse-list-arg1-iff
  (iff (intersection-equal (reverse-list x) y)
    (intersection-equal x y)))

intersection-equal-of-reverse-list-arg2theorem

(defthm intersection-equal-of-reverse-list-arg2
  (equal (intersection-equal x (reverse-list y))
    (intersection-equal x y)))

no-duplicatesp-equal-of-reverse-listtheorem

(defthm no-duplicatesp-equal-of-reverse-list
  (equal (no-duplicatesp-equal (reverse-list x))
    (no-duplicatesp-equal x))
  :hints (("Goal" :in-theory (enable reverse-list))))

Included Books