(in-package "ACL2")

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

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

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

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

(defun nat? (x)
  (if (z? x)
      (null x)
      (and (equal (car x) (cdr x))
           (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))))

(defmacro nat< (x y)
  `(member-equal ,x ,y))

(defthm nat<-succ
  (nat< x (succ x)))

(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+-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))
         (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)))

(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))))