From 3e1bdf10c85b5a4aca62349878b1bff786e30938 Mon Sep 17 00:00:00 2001
From: Masaya Tojo <masaya@tojo.tokyo>
Date: Sun, 22 Aug 2021 01:26:52 +0900
Subject: Add functions and theorems about cards.

---
 standard-52-card-deck.lisp | 179 +++++++++++++++++++++++++++++++++++++++++++++
 top.lisp                   |   3 +
 2 files changed, 182 insertions(+)
 create mode 100644 standard-52-card-deck.lisp
 create mode 100644 top.lisp

diff --git a/standard-52-card-deck.lisp b/standard-52-card-deck.lisp
new file mode 100644
index 0000000..70244d3
--- /dev/null
+++ b/standard-52-card-deck.lisp
@@ -0,0 +1,179 @@
+(in-package "ACL2")
+
+(defun suitp (x)
+  (declare (xargs :guard t))
+  (or (equal x 'S)
+      (equal x 'D)
+      (equal x 'C)
+      (equal x 'H)))
+
+(defun rank-acep (x)
+  (declare (xargs :guard t))
+  (equal x 'A))
+
+(defun rank-facep (x)
+  (declare (xargs :guard t))
+  (or (equal x 'J)
+      (equal x 'Q)
+      (equal x 'K)))
+
+(defun rank-natp (x)
+  (declare (xargs :guard t))
+  (and (integerp x)
+       (< 1 x)
+       (< x 11)))
+
+(defun rankp (x)
+  (declare (xargs :guard t))
+  (or (rank-acep x)
+      (rank-facep x)
+      (rank-natp x)))
+
+(defun card (s r)
+  (declare (xargs :guard (and (suitp s)
+                              (rankp r))))
+  (list s r))
+
+(defun cardp (x)
+  (declare (xargs :guard t))
+  (and (consp x)
+       (suitp (car x))
+       (consp (cdr x))
+       (rankp (cadr x))
+       (null (cddr x))))
+
+(defun suit (x)
+  (declare (xargs :guard (cardp x)))
+  (car x))
+
+(defun rank (x)
+  (declare (xargs :guard (cardp x)))
+  (cadr x))
+
+(defthm card-elim
+  (implies (cardp x)
+           (equal (card (suit x) (rank x))
+                  x))
+  :rule-classes :elim)
+
+(defthm suit-card
+  (equal (suit (card s r)) s))
+
+(defthm rank-card
+  (equal (rank (card s r)) r))
+
+(defthm suitp-suit
+  (implies (cardp x)
+           (let ((s (suit x)))
+             (or (equal s 'S)
+                 (equal s 'H)
+                 (equal s 'D)
+                 (equal s 'C))))
+  :rule-classes (:rewrite :forward-chaining))
+
+(defthm rankp-rank
+  (implies (cardp x)
+           (or (equal (rank x) 'A)
+               (equal (rank x) 'J)
+               (equal (rank x) 'Q)
+               (equal (rank x) 'K)
+               (and (integerp (rank x))
+                    (< 1 (rank x))
+                    (< (rank x) 11))))
+  :rule-classes (:rewrite :forward-chaining))
+
+(in-theory (disable card suit rank cardp))
+
+(defun suit-listp (x)
+  (declare (xargs :guard t))
+  (if (atom x)
+      (null x)
+      (and (suitp (car x))
+           (suit-listp (cdr x)))))
+
+(defthm suit-listp-forward-to-symbol-listp
+  (implies (suit-listp x)
+           (symbol-listp x))
+  :rule-classes :forward-chaining)
+
+(defun rank-listp (x)
+  (declare (xargs :guard t))
+  (if (atom x)
+      (null x)
+      (and (rankp (car x))
+           (rank-listp (cdr x)))))
+
+(defthm rank-listp-forward-to-true-listp
+  (implies (rank-listp x)
+           (true-listp x))
+  :rule-classes :forward-chaining)
+
+(defun rank-ace-listp (x)
+  (declare (xargs :guard t))
+  (if (atom x)
+      (null x)
+      (and (rank-acep (car x))
+           (rank-ace-listp (cdr x)))))
+
+(defthm rank-ace-listp-forward-to-true-listp
+  (implies (rank-ace-listp x)
+           (symbol-listp x))
+  :rule-classes :forward-chaining)
+
+(defun rank-face-listp (x)
+  (declare (xargs :guard t))
+  (if (atom x)
+      (null x)
+      (and (rank-facep (car x))
+           (rank-face-listp (cdr x)))))
+
+(defthm rank-face-listp-forward-to-true-listp
+  (implies (rank-face-listp x)
+           (symbol-listp x))
+  :rule-classes :forward-chaining)
+
+(defun rank-nat-listp (x)
+  (declare (xargs :guard t))
+  (if (atom x)
+      (null x)
+      (and (rank-natp (car x))
+           (rank-nat-listp (cdr x)))))
+
+(defthm rank-nat-listp-forward-to-true-listp
+  (implies (rank-nat-listp x)
+           (nat-listp x))
+  :rule-classes :forward-chaining)
+
+(defun card-listp (x)
+  (declare (xargs :guard t))
+  (if (atom x)
+      (null x)
+      (and (cardp (car x))
+           (card-listp (cdr x)))))
+
+(defthm card-listp-forward-to-true-listp
+  (implies (card-listp x)
+           (true-listp x))
+  :rule-classes :forward-chaining)
+
+(defun card-list-to-rank-list (x)
+  (declare (xargs :guard (card-listp x)))
+  (if (endp x)
+      nil
+      (cons (rank (car x))
+            (card-list-to-rank-list (cdr x)))))
+
+(defthm rank-listp-card-list-to-rank-list
+  (implies (card-listp x)
+           (rank-listp (card-list-to-rank-list x))))
+
+(defun card-list-to-suit-list (x)
+  (declare (xargs :guard (card-listp x)))
+  (if (endp x)
+      nil
+      (cons (suit (car x))
+            (card-list-to-suit-list (cdr x)))))
+
+(defthm suit-listp-card-list-to-suit-list
+  (implies (card-listp x)
+           (suit-listp (card-list-to-suit-list x))))
diff --git a/top.lisp b/top.lisp
new file mode 100644
index 0000000..18552e2
--- /dev/null
+++ b/top.lisp
@@ -0,0 +1,3 @@
+(in-package "ACL2")
+
+(include-book "standard-52-card-deck")
-- 
cgit v1.2.3