(in-package "ACL2")

(defun emptyp (x)
 (atom x))

(defun kv (x)
  (car x))

(defmacro key (x)
  `(car (kv ,x)))

(defmacro val (x)
  `(cdr (kv ,x)))

(defun left (x)
  (cadr x))

(defun right (x)
  (caddr x))

(defun tree-count (x)
  (if (emptyp x)
      0
      (+ 1 (+ (tree-count (left x))
              (tree-count (right x))))))

(defthm natp-tree-count
  (natp (tree-count x)))

(defthm count-tree-count
  (if (emptyp x)
      (equal (tree-count x) 0)
      (equal (tree-count x)
             (+ 1
                (tree-count (left x))
                (tree-count (right x))))))

(defthm tree-count-<
  (implies (not (emptyp x))
           (and (< (tree-count (right x)) (tree-count x))
                (< (tree-count (left x)) (tree-count x)))))

(defun lessp (x e)
  (if (emptyp x)
      t
      (and (lessp (left x) e)
           (< (car (kv x)) e)
           (lessp (right x) e))))

(defun overp (x e)
  (if (emptyp x)
      t
      (and (overp (left x) e)
           (< e (car (kv x)))
           (overp (right x) e))))

(defun treep (x)
  (if (emptyp x)
      (null x)
      (and (consp x)
           (consp (car x))
           (consp (cdr x))
           (consp (cddr x))
           (null (cdddr x))
           (rationalp (key x))
           (treep (left x))
           (treep (right x))
           (lessp (left x) (key x))
           (overp (right x) (key x)))))

(defun tree (k v l r)
  (list (cons k v) l r))

(defthm tree-elim
  (implies (and (treep x)
                (not (emptyp x)))
           (equal (tree (key x) (val x) (left x) (right x))
                  x))
  :rule-classes :elim)

(defthm tree-left
  (implies (and (treep x)
                (not (emptyp x)))
           (treep (left x))))

(defthm tree-right
  (implies (and (treep x)
                (not (emptyp x)))
           (treep (right x))))

(defthm consp-kv
  (implies (and (treep x)
                (not (emptyp x)))
           (consp (kv x))))

(defthm rationalp-key
  (implies (and (treep x)
                (not (emptyp x)))
           (rationalp (key x))))

(defthm lessp-left
  (implies (and (treep x)
                (not (emptyp x)))
           (lessp (left x) (key x))))

(defthm overp-right
  (implies (and (treep x)
                (not (emptyp x)))
           (overp (right x) (key x))))

(defthm treep-tree
  (implies (and (rationalp k)
                (treep l)
                (treep r)
                (lessp l k)
                (overp r k))
           (treep (tree k v l r)))
  :rule-classes (:rewrite))

(in-theory (disable emptyp treep kv tree left right tree-count))

(defun tree-assoc (k x)
  (declare (xargs :measure (tree-count x)))
  (if (emptyp x)
      nil
      (if (= (key x) k)
          (kv x)
          (if (< k (key x))
              (tree-assoc k (left x))
              (tree-assoc k (right x))))))

(defthm lessp-not-assoc
  (implies (and (treep x)
                (lessp x k))
           (not (tree-assoc k x)))
  :hints (("Goal" :induct (lessp x k))))

(defthm overp-not-assoc
  (implies (and (treep x)
                (overp x k))
           (not (tree-assoc k x)))
  :hints (("Goal" :induct (overp x k))))

(defthm not-tree-assoc-lemma-lessp2
  (implies (and (treep x)
                (<= e1 e2)
                (lessp x e1))
           (lessp x e2))
  :rule-classes ((:rewrite :match-free :all)))

(defthm not-tree-assoc-lemma-overp2
  (implies (and (treep x)
                (< e1 e2)
                (overp x e2))
           (overp x e1))
  :rule-classes ((:rewrite :match-free :all)))

(defthm not-tree-assoc
  (implies (and (treep x)
                (not (emptyp x)))
           (if (= k (key x))
               t
               (if (< k (key x))
                   (not (tree-assoc k (right x)))
                   (not (tree-assoc k (left x))))))
  :hints (("Goal" :induct (tree-assoc k x))))

(defun tree-to-alist (x)
  (declare (xargs :measure (tree-count x)))
  (if (emptyp x)
      nil
      (append (tree-to-alist (left x))
              (list (kv x))
              (tree-to-alist (right x)))))

(defthm alistp-append
  (implies (true-listp x)
           (iff (alistp (append x y))
                (and (alistp x)
                     (alistp y)))))

(defthm alistp-tree-to-alist
  (implies (treep x)
           (alistp (tree-to-alist x))))

(defthm assoc-append-nil
  (equal (assoc-equal k (append nil x))
         (assoc-equal k x)))

(defthm assoc-append
  (implies (alistp x)
           (equal (assoc k (append x y))
                  (or (assoc k x)
                      (assoc k y)))))

(defthm tree-assoc-assoc-tree-to-list
  (implies (treep x)
           (equal (tree-assoc k x)
                  (assoc k (tree-to-alist x))))
  :rule-classes nil)

(defthm assoc-tree-to-list-tree-assoc
  (implies (treep x)
           (equal (assoc k (tree-to-alist x))
                  (tree-assoc k x)))
  :hints (("Goal" :use (tree-assoc-assoc-tree-to-list)))
  :rule-classes nil)