(in-package "ACL2")

(defun mapcar-cons (e x)
  (declare (xargs :guard (true-listp x)))
  (if (endp x)
      nil
      (cons (cons e (car x))
            (mapcar-cons e (cdr x)))))

(defun insert (e x)
  (declare (xargs :guard (true-listp x)))
  (if (endp x)
      (list (list e))
      (cons (cons e x)
            (mapcar-cons (car x)
                         (insert e (cdr x))))))

(defun mappend-insert (x y)
  (declare (xargs :guard (true-list-listp y)))
  (if (endp y)
      nil
      (append (insert x (car y))
              (mappend-insert x (cdr y)))))

(defun permutations (x)
  (declare (xargs :guard (true-listp x)))
  (if (endp x)
      (list nil)
      (mappend-insert (car x)
                      (permutations (cdr x)))))

(defun factorial (n)
  (declare (xargs :guard (natp n)))
  (if (zp n)
      1
      (* n (factorial (1- n)))))

(defun mapcar-len (x)
  (declare (xargs :guard (true-list-listp x)))
  (if (endp x)
      nil
      (cons (len (car x))
            (mapcar-len (cdr x)))))

(defun sum (x)
  (declare (xargs :guard (nat-listp x)))
  (if (endp x)
      0
      (+ (car x)
         (sum (cdr x)))))

(defun mapcar-sum (x y)
  (declare (xargs :guard (and (nat-listp x)
                              (nat-listp y))))
  (if (or (endp x) (endp y))
      nil
      (cons (+ (car x) (car y))
            (mapcar-sum (cdr x) (cdr y)))))

(defun repeat (x n)
  (declare (xargs :guard (natp n)))
  (if (zp n)
      nil
      (cons x
            (repeat x (1- n)))))

(defun repeatedp (x)
  (declare (xargs :guard (true-listp x)))
  (if (or (endp x)
          (endp (cdr x)))
      t
      (and (equal (car x) (cadr x))
           (repeatedp (cdr x)))))

;; for len-insert
(defthm len-mapcar-cons
  (equal (len (mapcar-cons e x))
         (len x)))

;; for len-mappend-insert
(defthm len-append
  (equal (len (append x y))
         (+ (len x)
            (len y))))

;; for len-permutations-lemma
(defthm len-mappend-insert
  (equal (len (mappend-insert e x))
         (sum (mapcar-sum (mapcar-len x)
                          (repeat 1 (len x))))))

;; for len-permutations-lemma
(defthm sum-mapcar-sum
  (implies (equal (len x) (len y))
           (equal (sum (mapcar-sum x y))
                  (+ (sum x) (sum y)))))

;; for len-permutations-lemma
(defthm len-repeat
  (implies (natp n)
           (equal (len (repeat x n))
                  n)))

;; for len-permutations-lemma
(defthm len-mapcar-len
  (equal (len (mapcar-len x))
         (len x)))

;; for len-permutations-lemma
(defthm sum-repeat-1
  (implies (natp n)
           (equal (sum (repeat 1 n))
                  n)))

;; for len-permutations-lemma
(defthm sum-repeatedp
  (implies (and (nat-listp x)
                (repeatedp x))
           (equal (sum x)
                  (if (consp x)
                      (* (car x)
                         (len x))
                      0))))

;; for len-permutations-lemma
(defthm nat-listp-mapcar-len
  (nat-listp (mapcar-len x)))

;; for repeatedp-mapcar-len-mappend-insert
(defthm mapcar-len-append
  (equal (mapcar-len (append x y))
         (append (mapcar-len x)
                 (mapcar-len y))))

;; for repeatedp-mapcar-len-mappend-insert
(defthm repeatedp-append
  (equal (repeatedp (append x y))
         (cond
           ((endp x) (repeatedp y))
           ((endp y) (repeatedp x))
           (t
            (and (repeatedp x)
                 (repeatedp y)
                 (equal (car x) (car y)))))))

;; for mapcar-len-insert
(defthm mapcar-len-mapcar-cons
  (equal (mapcar-len (mapcar-cons e x))
         (mapcar-sum (mapcar-len x)
                     (repeat 1 (len x)))))

;; mapcar-len-insert
(defthm len-insert
  (equal (len (insert e x))
         (+ 1 (len x))))

;; for repeatedp-mapcar-len-mappend-insert
(defthm mapcar-len-insert
  (equal (mapcar-len (insert e x))
         (repeat (+ 1 (len x))
                 (+ 1 (len x)))))

;; for repeatedp-mapcar-len-mappend-insert
(defthm car-append
  (equal (car (append x y))
         (if (endp x)
             (car y)
             (car x))))

;; for repeatedp-mapcar-len-mappend-insert
(defthm car-repeat
  (equal (car (repeat x n))
         (if (zp n)
             nil
             x)))

;; for repeatedp-mapcar-len-mappend-insert
(defthm repeatedp-repeat
  (repeatedp (repeat x n)))

;; for repeatedp-mapcar-len-mappend-insert
(defthm car-mapcar-len-mappend-insert
  (equal (car (mapcar-len (mappend-insert e x)))
         (if (consp x)
             (+ 1 (len (car x)))
             nil)))

;; for len-permutations-lemma
(defthm repeatedp-mapcar-len-mappend-insert
  (implies (repeatedp (mapcar-len x))
           (repeatedp (mapcar-len (mappend-insert e x)))))

;; for len-permutations-lemma
(defthm repeatedp-mapcar-len-permutations
  (repeatedp (mapcar-len (permutations x))))

;; for len-permutations-lemma
(defthm consp-mapcar-len-mappend-insert
  (consp (mapcar-len (mappend-insert e (permutations x)))))

;; for len-permutations-lemma
(defthm len-car-mappend-insert
  (equal (len (car (mappend-insert e x)))
         (if (consp x)
             (+ 1 (len (car x)))
             0)))

;; for len-permutations-lemma
(defthm len-car-permutations
  (equal (len (car (permutations x)))
         (len x)))

;; for len-permutations
(defthm len-permutations-lemma
  (equal (len (mappend-insert e (permutations x)))
         (+ (len (permutations x))
            (* (len x)
               (len (permutations x))))))

(defthm len-permutations
  (equal (len (permutations x))
         (factorial (len x))))