diff options
Diffstat (limited to 'peano.lisp')
| -rw-r--r-- | peano.lisp | 61 |
1 files changed, 21 insertions, 40 deletions
@@ -26,23 +26,15 @@ ((or (z? x) (z? y)) nil) (t (nat= (pred x) (pred y))))) +(defthm nat=-reflexive + (nat= x x)) +(defthm nat=-symmetric + (equal (nat= x y) + (nat= y x))) -(defthm nat-reflexive - (implies (nat? x) - (nat= x x))) - -(defthm nat-symmetric - (implies (and (nat? x) - (nat? y)) - (equal (nat= x y) - (nat= y x)))) - -(defthm nat-transitive - (implies (and (nat? x) - (nat? y) - (nat? z) - (nat= x y) +(defthm nat=-transitive + (implies (and (nat= x y) (nat= y z)) (nat= x z))) @@ -68,23 +60,9 @@ (equal (nat+ nil x) x))) -(defthm nat+-left-not-zp - (implies (and (nat? x) - (not (z? x)) - (nat? y)) - (not (equal (nat+ x y) - y)))) - -(defthm nat+-right-not-zp - (implies (and (nat? x) - (nat? y) - (not (z? y))) - (not (equal (nat+ x y) - x))) - :hints (("Goal" :in-theory (disable nat+-commutative) - :use ((:instance nat+-commutative - (x x) - (y y)))))) +(defthm nat+-right-cancellative + (equal (equal (nat+ x k) (nat+ y k)) + (equal x y))) (defthm nat+-left-cancellative (implies (and (nat? x) @@ -92,11 +70,14 @@ (nat? k)) (equal (equal (nat+ k x) (nat+ k y)) (equal x y))) - :hints (("Goal" :induct (nat= x y)))) - -(defthm nat+-right-cancellative - (implies (and (nat? x) - (nat? y) - (nat? k)) - (equal (equal (nat+ x k) (nat+ y k)) - (equal x y)))) + :hints (("Goal" :in-theory (disable nat+-commutative) + :use ((:instance nat+-commutative + (x x) + (y k)) + (:instance nat+-commutative + (x y) + (y k)))))) + +(defthm associativity-of-nat+ + (equal (nat+ x (nat+ y z)) + (nat+ (nat+ x y) z))) |