From 279063668f17a09d5f272af1d1614f63cc323cd9 Mon Sep 17 00:00:00 2001
From: Masaya Tojo <masaya@tojo.tokyo>
Date: Wed, 1 Sep 2021 22:19:02 +0900
Subject: Add binary-tree.lisp.

---
 binary-tree.lisp | 178 +++++++++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 178 insertions(+)
 create mode 100644 binary-tree.lisp

diff --git a/binary-tree.lisp b/binary-tree.lisp
new file mode 100644
index 0000000..037da4f
--- /dev/null
+++ b/binary-tree.lisp
@@ -0,0 +1,178 @@
+(defun emptyp (x)
+  (atom x))
+
+(defun val (x)
+  (car 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)
+           (< (val x) e)
+           (lessp (right x) e))))
+
+(defun overp (x e)
+  (if (emptyp x)
+      t
+      (and (overp (left x) e)
+           (< e (val x))
+           (overp (right x) e))))
+
+(defun treep (x)
+  (if (emptyp x)
+      (null x)
+      (and (consp x)
+           (rationalp (car x))
+           (consp (cdr x))
+           (treep (cadr x))
+           (consp (cddr x))
+           (treep (caddr x))
+           (lessp (left x) (val x))
+           (overp (right x) (val x))
+           (null (cdddr x)))))
+
+(defun tree (x l r)
+  (list x l r))
+
+(defthm tree-elim
+  (implies (and (treep x)
+                (not (emptyp x)))
+           (equal (tree (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 rationalp-val
+  (implies (and (treep x)
+                (not (emptyp x)))
+           (rationalp (val x))))
+
+(defthm lessp-left
+  (implies (and (treep x)
+                (not (emptyp x)))
+           (lessp (left x) (val x))))
+
+(defthm overp-right
+  (implies (and (treep x)
+                (not (emptyp x)))
+           (overp (right x) (val x))))
+
+(defthm treep-tree
+  (implies (and (rationalp x)
+                (treep l)
+                (treep r)
+                (lessp l x)
+                (overp r x))
+           (treep (tree x l r)))
+  :rule-classes (:rewrite))
+
+(in-theory (disable emptyp treep val tree left right tree-count))
+
+(defun tree-memberp (e x)
+  (declare (xargs :measure (tree-count x)))
+  (if (emptyp x)
+      nil
+      (if (= (val x) e)
+          t
+          (if (< e (val x))
+              (tree-memberp e (left x))
+              (tree-memberp e (right x))))))
+
+(defthm lessp-not-member
+  (implies (and (treep x)
+                (lessp x e))
+           (not (tree-memberp e x)))
+  :hints (("Goal" :induct (lessp x e))))
+
+(defthm overp-not-member
+  (implies (and (treep x)
+                (overp x e))
+           (not (tree-memberp e x)))
+  :hints (("Goal" :induct (overp x e))))
+
+(defthm not-tree-memberp-lemma-lessp2
+  (implies (and (treep x)
+                (<= e1 e2)
+                (lessp x e1))
+           (lessp x e2))
+  :rule-classes ((:rewrite :match-free :all)))
+
+(defthm not-tree-memberp-lemma-overp2
+  (implies (and (treep x)
+                (< e1 e2)
+                (overp x e2))
+           (overp x e1))
+  :rule-classes ((:rewrite :match-free :all)))
+
+(defthm not-tree-memberp
+  (implies (and (treep x)
+                (not (emptyp x)))
+           (if (= e (val x))
+               t
+               (if (< e (val x))
+                   (not (tree-memberp e (right x)))
+                   (not (tree-memberp e (left x))))))
+  :hints (("Goal" :induct (tree-memberp e x))))
+
+(defun tree-to-list (x)
+  (declare (xargs :measure (tree-count x)))
+  (if (emptyp x)
+      nil
+      (append (tree-to-list (left x))
+              (list (val x))
+              (tree-to-list (right x)))))
+
+(defthm member-append
+  (iff (member e (append x y))
+       (or (member e x)
+           (member e y))))
+
+(defthm tree-memberp-member-tree-to-list
+  (implies (treep x)
+           (iff (tree-memberp e x)
+                (member e (tree-to-list x))))
+  :rule-classes nil)
+
+(defthm member-tree-to-list-tree-memberp
+  (implies (treep x)
+           (iff (member e (tree-to-list x))
+                (tree-memberp e x)))
+  :hints (("Goal" :use (tree-memberp-member-tree-to-list)))
+  :rule-classes nil)
-- 
cgit v1.2.3