(in-package "ACL2")

(defun app (x y)
  (cond ((endp x) y)
        (t (cons (car x) (app (cdr x) y)))))

(defun rotate (n x)
  (cond ((zp n) x)
        (t (rotate (1- n)
                   (app (cdr x)
                        (list (car x)))))))

(include-book "arithmetic-5/top" :dir :system)

(defun firstn (n x)
  (if (zp n)
      nil
    (cons (car x)
          (firstn (1- n) (cdr x)))))

(defun dropn (n x)
  (if (zp n)
      x
    (dropn (1- n) (cdr x))))

(defthm app-x-nil
  (implies (true-listp x)
           (equal (app x nil) x)))

(defthm dropn-app
  (implies (and (natp n)
                (<= n (len x)))
           (equal (dropn n (app x y))
                  (app (dropn n x) y))))

(defthm app-assoc
  (equal (app (app x y) z)
         (app x (app y z))))

(defthm firstn-app
  (implies (and (natp n)
                (<= n (len x)))
           (equal (firstn n (app x y))
                  (firstn n x))))

(defthm len-app
  (equal (len (app a b))
         (+ (len a) (len b))))

; A better (unconditional) version follows:
;(defthm true-listp-app
;  (implies (true-listp y)
;           (true-listp (app x y))))

(defthm true-listp-app
  (equal (true-listp (app x y))
         (true-listp y)))

(defthm rotate-len-generalization
  (implies (and (true-listp x)
                (<= n (len x)))
           (equal (rotate n x)
                  (app (dropn n x) (firstn n x)))))

(defthm dropn-len
  (implies (true-listp x)
           (equal (dropn (len x) x)
                  nil)))

(defthm firstn-len
  (implies (true-listp x)
           (equal (firstn (len x) x)
                  x)))

(defthm rotate-len
  (implies (true-listp x)
           (equal (rotate (len x) x)
                  x)))