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

(defthm nat=-symmetric
  (equal (nat= x y)
         (nat= y x)))

(defthm nat=-transitive
  (implies (and (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+-right-cancellative
  (equal (equal (nat+ x k) (nat+ y k))
         (equal x 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" :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)))