(defmacro zero? (x)
  `(equal ,x nil))

(defmacro z? (x)
  `(atom ,x))

(defmacro succ (x)
  `(cons nil ,x))

(defmacro pred (x)
  `(cdr ,x))

(defun nat? (x)
  (if (z? x)
      (null x)
      (and (equal (car x) nil)
           (nat? (pred x)))))

(defthm zero-is-nat
  (implies (zero? x)
           (nat? x)))

(defun nat= (x y)
  (cond
    ((and (z? x) (z? y)) t)
    ((or (z? x) (z? y)) nil)
    (t (nat= (pred x) (pred y)))))



(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)
                (nat= y z))
           (nat= x z)))

(defthm nat=-to-equal
  (implies (and (nat? x)
                (nat? y))
           (equal (nat= x y)
                  (equal x y))))

(defun nat+ (x y)
  (if (z? y)
      x
      (succ (nat+ x (pred y)))))

(defthm nat+-commutative
  (implies (and (nat? x)
                (nat? y))
           (equal (nat+ x y)
                  (nat+ y x))))

(defthm nat+-zero
  (implies (nat? x)
           (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+-left-cancellative
  (implies (and (nat? x)
                (nat? y)
                (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))))