permutations: Remove useless theorems and fucntions.

1 files changed, 24 insertions, 107 deletions

diff --git a/permutations.lisp b/permutations.lisp
index 7c01dc3..66ecc74 100644
--- a/permutations.lisp
+++ b/permutations.lisp
@@ -1,5 +1,3 @@
-(local (include-book "arithmetic/top-with-meta" :dir :system))
-
 (defun insert (x y)
   (if (endp y)
       (list x)
@@ -19,58 +17,39 @@
       (mappend-insert (list (car x))
                       (permutations (cdr x)))))
 
-(defun nat-expt (m n)
-  (cond
-    ((zp n) 1)
-    ((zp (1- n)) m)
-    (t (* m (nat-expt m (1- n))))))
-
-(defun sum-of-nat-expt-lens (x n)
+(defun sum-of-lens (x)
   (if (endp x)
       0
-      (+ (nat-expt (len (car x)) n)
-         (sum-of-nat-expt-lens (cdr x) n))))
-
-(defthm nat-expt-1+
-  (implies (natp n)
-           (equal (nat-expt (+ 1 x) (+ 1 n))
-                  (+ (* x (nat-expt (+ 1 x) n))
-                     (nat-expt (+ 1 x) n)))))
+      (+ (len (car x))
+         (sum-of-lens (cdr x)))))
 
-(defun sum-of-nat-expt-1+lens (x n)
+(defun sum-of-1+lens (x)
   (if (endp x)
       0
-      (+ (nat-expt (+ 1 (len (car x))) n)
-         (sum-of-nat-expt-1+lens (cdr x) n))))
+      (+ (+ 1 (len (car x)))
+         (sum-of-1+lens (cdr x)))))
 
-(defthm sum-of-nat-expt-lens-append
-  (equal (sum-of-nat-expt-lens (append x y) n)
-         (+ (sum-of-nat-expt-lens x n)
-            (sum-of-nat-expt-lens y n))))
+(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-nat-expt-lens-insert
-  (equal (sum-of-nat-expt-lens (insert x y) n)
-         (* (nat-expt (+ (len x) (len y)) n)
+(defthm sum-of-lens-insert
+  (equal (sum-of-lens (insert x y))
+         (* (+ (len x) (len y))
             (+ 1 (len y)))))
 
-(defthm sum-of-nat-expt-lens-mappend-insert
-  (implies (natp n)
-           (equal (sum-of-nat-expt-lens (mappend-insert (list x) y) n)
-                  (sum-of-nat-expt-1+lens y (+ 1 n)))))
-
-(defthm len-sum-of-nextp-lens
-  (equal (len x)
-         (sum-of-nat-expt-lens x 0)))
-(in-theory (disable len-sum-of-nextp-lens))
+(defthm len-insert
+  (equal (len (insert x y))
+         (+ 1 (len y))))
 
 (defthm len-mappend-insert
   (equal (len (mappend-insert (list x) y))
-         (sum-of-nat-expt-1+lens y 1))
-  :hints (("Goal" :in-theory (enable len-sum-of-nextp-lens))))
+         (sum-of-1+lens y)))
 
 (defun mapcar-len (x)
   (if (endp x)
@@ -84,12 +63,6 @@
       (+ (car x)
          (sum (cdr x)))))
 
-(defun mapcar-nat-expt (x i)
-  (if (endp x)
-      nil
-      (cons (nat-expt (car x) i)
-            (mapcar-nat-expt (cdr x) i))))
-
 (defun seq (x n)
   (if (zp n)
       nil
@@ -107,16 +80,14 @@
       (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))))
 
-(defthm sum-of-nat-expt-lens-equal-sum-mapcar-nat-expt-len
-  (equal (sum-of-nat-expt-lens x n)
-         (sum (mapcar-nat-expt (mapcar-len x) n))))
-
-(defthm sum-of-nat-expt-1+lens-equal-sum-mapcar-nat-expt-1+-len
-  (equal (sum-of-nat-expt-1+lens x n)
-         (sum (mapcar-nat-expt (mapcar-sum (seq 1 (len x))
-                                           (mapcar-len x))
-                               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)))))
 
 (defthm nat-listp-mapcar-len
   (nat-listp (mapcar-len x)))
@@ -130,70 +101,16 @@
 (defthm len-mapcar-len
   (equal (len (mapcar-len x)) (len x)))
 
-(defthm len-mapcar-nat-expt
-  (equal (len (mapcar-nat-expt x n)) (len x)))
-
 (defthm len-mapcar-product
   (implies (equal (len x) (len y))
            (equal (len (mapcar-product x y))
                   (len x))))
 
-(defthm mapcar-nat-expt-0-one-seq
-  (equal (mapcar-nat-expt x 0)
-         (seq 1 (len x))))
-
 (defthm mapcar-product-one-seq
   (implies (acl2-number-listp x)
            (equal (mapcar-product (seq 1 (len x)) x)
                   x)))
 
-(defthm mapcar-product-mapcar-nat-expt-0
-  (implies (and (acl2-number-listp x)
-                (equal (len x) (len y)))
-           (equal (mapcar-product (mapcar-nat-expt y 0)
-                                  x)
-                  x)))
-
-(defthm sum-of-nat-expt-lens-equal-sum-mapcar-nat-expt-len/inverse
-  (equal (sum (mapcar-nat-expt (mapcar-len x) n))
-         (sum-of-nat-expt-lens x n)))
-
-(defthm sum-of-nat-expt-1+lens-equal-sum-mapcar-nat-expt-1+-len/inverse
-  (equal (sum (mapcar-nat-expt (mapcar-sum (seq 1 (len x))
-                                           (mapcar-len x))
-                               n))
-         (sum-of-nat-expt-1+lens x n)))
-
-(defthm sum-of-nat-expt-lens-mappend-insert/mapcar
-  (implies (natp n)
-           (equal (sum (mapcar-nat-expt (mapcar-len (mappend-insert (list x)
-                                                                    y))
-                                        n))
-                  (sum (mapcar-nat-expt (mapcar-sum (seq 1 (len y))
-                                                    (mapcar-len y))
-                                        (+ 1 n)))))
-  :hints (("Goal"  :in-theory (disable
-                               sum-of-nat-expt-lens-equal-sum-mapcar-nat-expt-len
-                               sum-of-nat-expt-1+lens-equal-sum-mapcar-nat-expt-1+-len))))
-
-(in-theory (disable sum-of-nat-expt-lens-equal-sum-mapcar-nat-expt-len/inverse
-                    sum-of-nat-expt-1+lens-equal-sum-mapcar-nat-expt-1+-len/inverse))
-
-(defthm nat-expt-1
-  (equal (nat-expt x 1)
-         x))
-
-(defthm mapcar-nat-expt-1
-  (implies (true-listp x)
-           (equal (mapcar-nat-expt x 1)
-                  x)))
-
-(defthm sum-mapcar-len-mappend-insert-lemma
-  (equal (sum (mapcar-len x))
-         (sum (mapcar-nat-expt (mapcar-len x) 1))))
-
-(in-theory (disable sum-mapcar-len-mappend-insert-lemma))
-
 (defthm len-seq
   (implies (natp n)
            (equal (len (seq x n))