diff options
| -rw-r--r-- | peano.lisp | 59 |
1 files changed, 55 insertions, 4 deletions
@@ -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))))))) |