flist: Add `flist.lisp` file.

1 files changed, 45 insertions, 0 deletions

diff --git a/flist.lisp b/flist.lisp
new file mode 100644
index 0000000..dc6ffe7
--- /dev/null
+++ b/flist.lisp
@@ -0,0 +1,45 @@
+(defun true-flistp (x)
+  (if (endp x)
+      (null x)
+      (and (consp x)
+           (true-flistp (car x)))))
+
+(defun list-to-flist (x)
+  (if (endp x)
+      nil
+      (cons (list-to-flist (cdr x))
+            (car x))))
+
+(defun flist-to-list (x)
+  (if (endp x)
+      nil
+      (cons (cdr x)
+            (flist-to-list (car x)))))
+
+(defthm flist-to-list-to-flist
+  (implies (true-flistp x)
+           (equal (list-to-flist (flist-to-list x))
+                  x)))
+
+(defthm list-to-flist-to-list
+  (implies (true-listp x)
+           (equal (flist-to-list (list-to-flist x))
+                  x)))
+
+
+(defun fappend (x y)
+  (if (endp x)
+      y
+      (cons (fappend (car x) y)
+            (cdr x))))
+
+(defthm assocativity-of-append
+  (equal (fappend (fappend x y) z)
+         (fappend x (fappend y z))))
+
+(defthm fappend-append
+  (implies (and (true-listp x)
+                (true-listp y))
+           (equal (flist-to-list (fappend (list-to-flist x)
+                                          (list-to-flist y)))
+                  (append x y))))