From a51be68a1b9c1c2c4e720b49190fdd89a86885bb Mon Sep 17 00:00:00 2001 From: Masaya Tojo Date: Thu, 9 Sep 2021 15:49:44 +0900 Subject: flist: Add `flist.lisp` file. --- flist.lisp | 45 +++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 45 insertions(+) create mode 100644 flist.lisp 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)))) -- cgit v1.2.3