(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))))