peano: Add nat* function and theorems.

1 files changed, 55 insertions, 4 deletions

diff --git a/peano.lisp b/peano.lisp
index 8c7f7d3..5028a13 100644
--- a/peano.lisp
+++ b/peano.lisp
@@ -55,10 +55,12 @@
            (equal (nat+ x y)
                   (nat+ y x))))
 
-(defthm nat+-zero
-  (implies (nat? x)
-           (equal (nat+ nil x)
-                  x)))
+(defthm nat+-left-zero
+  (implies (and (nat? x)
+                (z? x)
+                (nat? y))           
+           (equal (nat+ x y)
+                  y)))
 
 (defthm nat+-right-cancellative
   (equal (equal (nat+ x k) (nat+ y k))
@@ -81,3 +83,52 @@
 (defthm associativity-of-nat+
   (equal (nat+ x (nat+ y z))
          (nat+ (nat+ x y) z)))
+
+(defun nat* (x y)
+  (if (z? y)
+      nil
+      (nat+ x (nat* x (pred y)))))
+
+(defthm nat*-left-one
+  (equal (nat* x (succ nil))
+         x))
+
+(defthm nat*-right-one
+  (equal (nat* x (succ nil))
+         x))
+
+(defthm nat*-commutative
+  (implies (and (nat? x)
+                (nat? y))
+           (equal (nat* x y)
+                  (nat* y x))))
+
+(defthm nat?-nat*
+  (implies (and (nat? x)
+                (nat? y))
+           (nat? (nat* x y))))
+
+(defthm nat*-left-zero
+  (implies (and (z? x)
+                (nat? x))
+           (equal (nat* x y)
+                  nil)))
+
+(defthm distributivity-of-nat*
+  (implies (and (nat? x)
+                (nat? y)
+                (nat? z))
+           (equal (nat* x (nat+ y z))
+                  (nat+ (nat* x y)
+                        (nat* x z)))))
+
+(defthm associativity-of-nat*
+  (implies (and (nat? x)
+                (nat? y)
+                (nat? z))
+           (equal (nat* x (nat* y z))
+                  (nat* (nat* x y) z)))
+  :hints (("Goal" :in-theory (disable nat*-commutative)
+                  :use ((:instance nat*-commutative
+                                   (x (cdr z))
+                                   (y (nat* x y)))))))