permutations: Update.

1 files changed, 141 insertions, 192 deletions

diff --git a/permutations.lisp b/permutations.lisp
index 66ecc74..89b978e 100644
--- a/permutations.lisp
+++ b/permutations.lisp
@@ -1,9 +1,15 @@
-(defun insert (x y)
-  (if (endp y)
-      (list x)
-      (cons (append x y)
-            (insert (cons (car y) x)
-                    (cdr y)))))
+(defun mapcar-cons (e x)
+  (if (endp x)
+      nil
+      (cons (cons e (car x))
+            (mapcar-cons e (cdr x)))))
+
+(defun insert (e x)
+  (if (endp x)
+      (list (list e))
+      (cons (cons e x)
+            (mapcar-cons (car x)
+                         (insert e (cdr x))))))
 
 (defun mappend-insert (x y)
   (if (endp y)
@@ -14,42 +20,13 @@
 (defun permutations (x)
   (if (endp x)
       (list nil)
-      (mappend-insert (list (car x))
+      (mappend-insert (car x)
                       (permutations (cdr x)))))
 
-(defun sum-of-lens (x)
-  (if (endp x)
-      0
-      (+ (len (car x))
-         (sum-of-lens (cdr x)))))
-
-(defun sum-of-1+lens (x)
-  (if (endp x)
-      0
-      (+ (+ 1 (len (car x)))
-         (sum-of-1+lens (cdr x)))))
-
-(defthm sum-of-lens-append
-  (equal (sum-of-lens (append x y))
-         (+ (sum-of-lens x)
-            (sum-of-lens y))))
-
-(defthm len-append
-  (equal (len (append x y))
-         (+ (len x) (len y))))
-
-(defthm sum-of-lens-insert
-  (equal (sum-of-lens (insert x y))
-         (* (+ (len x) (len y))
-            (+ 1 (len y)))))
-
-(defthm len-insert
-  (equal (len (insert x y))
-         (+ 1 (len y))))
-
-(defthm len-mappend-insert
-  (equal (len (mappend-insert (list x) y))
-         (sum-of-1+lens y)))
+(defun factorial (n)
+  (if (zp n)
+      1
+      (* n (factorial (1- n)))))
 
 (defun mapcar-len (x)
   (if (endp x)
@@ -63,198 +40,170 @@
       (+ (car x)
          (sum (cdr x)))))
 
-(defun seq (x n)
-  (if (zp n)
-      nil
-      (cons x (seq x (1- n)))))
-
-(defun mapcar-product (x y)
-  (if (or (endp x) (endp y))
-      nil
-      (cons (* (car x) (car y))
-            (mapcar-product (cdr x) (cdr y)))))
-
 (defun mapcar-sum (x y)
   (if (or (endp x) (endp y))
       nil
       (cons (+ (car x) (car y))
             (mapcar-sum (cdr x) (cdr y)))))
 
-(defthm sum-of-lens-equal-sum-mapcar-len
-  (equal (sum-of-lens x)
-         (sum (mapcar-len x))))
+(defun repeat (x n)
+  (if (zp n)
+      nil
+      (cons x
+            (repeat x (1- n)))))
 
-(defthm sum-of-1+lens-equal-sum-1+-len
-  (equal (sum-of-1+lens x)
-         (sum (mapcar-sum (seq 1 (len x))
-                          (mapcar-len x)))))
+(defun repeatedp (x)
+  (if (or (endp x)
+          (endp (cdr x)))
+      t
+      (and (equal (car x) (cadr x))
+           (repeatedp (cdr x)))))
 
-(defthm nat-listp-mapcar-len
-  (nat-listp (mapcar-len x)))
+;; for len-insert
+(defthm len-mapcar-cons
+  (equal (len (mapcar-cons e x))
+         (len x)))
 
-(defthm sum-mapcar-sum
-  (implies (equal (len x) (len y))
-           (equal (sum (mapcar-sum x y))
-                  (+ (sum x)
-                     (sum y)))))
+;; for len-mappend-insert
+(defthm len-append
+  (equal (len (append x y))
+         (+ (len x)
+            (len y))))
 
-(defthm len-mapcar-len
-  (equal (len (mapcar-len x)) (len x)))
+;; for len-permutations-lemma
+(defthm len-mappend-insert
+  (equal (len (mappend-insert e x))
+         (sum (mapcar-sum (mapcar-len x)
+                          (repeat 1 (len x))))))
 
-(defthm len-mapcar-product
+;; for len-permutations-lemma
+(defthm sum-mapcar-sum
   (implies (equal (len x) (len y))
-           (equal (len (mapcar-product x y))
-                  (len x))))
-
-(defthm mapcar-product-one-seq
-  (implies (acl2-number-listp x)
-           (equal (mapcar-product (seq 1 (len x)) x)
-                  x)))
+           (equal (sum (mapcar-sum x y))
+                  (+ (sum x) (sum y)))))
 
-(defthm len-seq
+;; for len-permutations-lemma
+(defthm len-repeat
   (implies (natp n)
-           (equal (len (seq x n))
+           (equal (len (repeat x n))
                   n)))
 
-(defthm sum-seq
-  (implies (natp n)
-           (equal (sum (seq x n))
-                  (* x n))))
-
-(defthm mapcar-distributivity
-  (equal (* x (sum y))
-         (sum (mapcar-product (seq x (len y))
-                              y))))
+;; for len-permutations-lemma
+(defthm len-mapcar-len
+  (equal (len (mapcar-len x))
+         (len x)))
 
-(defthm len-mapcar-sum
-  (implies (equal (len x) (len y))
-           (equal (len (mapcar-sum x y))
-                  (len x))))
+;; for len-permutations-lemma
+(defthm sum-repeat-1
+  (implies (natp n)
+           (equal (sum (repeat 1 n))
+                  n)))
 
-(defthm mapcar-product-com
-  (implies (equal (len x) (len y))
-           (equal (mapcar-product x y)
-                  (mapcar-product y x))))
+;; 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))))
 
-(defthm mapcar-len-insert
-  (equal (mapcar-len (insert x y))
-         (seq (+ (len x) (len y))
-              (+ 1 (len y)))))
+;; for len-permutations-lemma
+(defthm nat-listp-mapcar-len
+  (nat-listp (mapcar-len x)))
 
-(defun mapcar-len-mappend-insert (x)
-  (if (endp x)
-      nil
-      (append (seq (+ 1 (len (car x)))
-                   (+ 1 (len (car x))))
-              (mapcar-len-mappend-insert (cdr x)))))
 
+;; for repeatedp-mapcar-len-mappend-insert
 (defthm mapcar-len-append
   (equal (mapcar-len (append x y))
          (append (mapcar-len x)
                  (mapcar-len y))))
 
-(defthm theorem-of-mapcar-len-mappend-insert
-  (equal (mapcar-len (mappend-insert (list x) y))
-         (mapcar-len-mappend-insert y)))
-
-(defun sum-mapcar-len-mappend-insert (x)
-  (if (endp x)
-      0
-      (+ (* (+ 1 (len (car x)))
-            (+ 1 (len (car x))))
-         (sum-mapcar-len-mappend-insert (cdr x)))))
-
-(defthm sum-append
-  (equal (sum (append x y))
-         (+ (sum x)
-            (sum y))))
-
-(defthm theorem-of-sum-mapcar-len-mappend-insert
-  (equal (sum (mapcar-len-mappend-insert x))
-         (sum-mapcar-len-mappend-insert x)))
-
-(defun seqp (x)
-  (if (or (endp x)
-          (endp (cdr x)))
-      t
-      (and (equal (car x)
-                  (cadr x))
-           (seqp (cdr x)))))
-
-(defmacro same-len-p (x)
-  `(seqp (mapcar-len ,x)))
-
-(defthm sum-mapcar-len-mappend-insert-permutations
-  (implies (same-len-p x)
-           (equal (sum-mapcar-len-mappend-insert x)
-                  (if (consp x)
-                      (* (+ 1 (len (car x)))
-                         (+ 1 (len (car x)))
-                         (len x))
-                      0))))
-
-(defthm same-len-p-insert
-  (implies (true-listp y)
-           (same-len-p (insert x y))))
-
-(defthm seqp-append
-  (iff (seqp (append x y))
-       (if (consp x)
-           (if (consp y)
-               (and (seqp x)
-                    (seqp y)
-                    (equal (car x) (car y)))
-               (seqp x))
-           (seqp y))))
-
-(defthm car-seq
-  (implies (consp (seq x n))
-           (equal (car (seq x n)) x)))
-
-(defthm car-mapcar-len-mappend-insert
-  (implies (consp (mapcar-len-mappend-insert x))
-           (equal (car (mapcar-len-mappend-insert x))
-                  (+ 1 (len (car x))))))
+;; 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))))
 
-(defthm seqp-seq
-  (seqp (seq x n)))
+;; 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)
-             (car x)
-             (car y))))
+             (+ 1 (len (car x)))
+             nil)))
 
-(defthm seqp-mapcar-len-mappend-insert
-  (implies (same-len-p x)
-           (seqp (mapcar-len-mappend-insert x))))
+;; for len-permutations-lemma
+(defthm repeatedp-mapcar-len-mappend-insert
+  (implies (repeatedp (mapcar-len x))
+           (repeatedp (mapcar-len (mappend-insert e x)))))
 
-(defthm same-len-p-permutations
-  (same-len-p (permutations x)))
+;; for len-permutations-lemma
+(defthm repeatedp-mapcar-len-permutations
+  (repeatedp (mapcar-len (permutations x))))
 
-(defthm len-car-insert
-  (equal (len (car (insert x y)))
-         (+ (len x) (len y))))
+;; 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
-  (implies (and (consp (mappend-insert (list x) y))
-                (same-len-p y))
-           (equal (len (car (mappend-insert (list x) y)))
-                  (+ 1 (len (car y))))))
+  (equal (len (car (mappend-insert e x)))
+         (if (consp x)
+             (+ 1 (len (car x)))
+             0)))
 
+;; for len-permutations-lemma
 (defthm len-car-permutations
-  (implies (consp (permutations x))
-           (equal (len (car (permutations x)))
-                  (len x))))
+  (equal (len (car (permutations x)))
+         (len x)))
 
+;; for len-permutations
 (defthm len-permutations-lemma
-  (equal (sum (mapcar-len (permutations x)))
-         (* (len x) (len (permutations x)))))
-
-(defun factorial (n)
-  (if (zp n)
-      1
-      (* n (factorial (1- n)))))
+  (equal (len (mappend-insert e (permutations x)))
+         (+ (len (permutations x))
+            (* (len x)
+               (len (permutations x))))))
 
 (defthm len-permutations
   (equal (len (permutations x))