1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
|
(in-package "ACL2")
(include-book "standard-52-card-deck/standard-52-card-deck")
(defun sum (x)
(declare (xargs :guard (nat-listp x)))
(cond ((endp x) 0)
(t (+ (car x) (sum (cdr x))))))
(defun rank-natp-filter (x)
(declare (xargs :guard (rank-listp x)))
(cond ((endp x) nil)
((natp (car x))
(cons (car x) (rank-natp-filter (cdr x))))
(t (rank-natp-filter (cdr x)))))
(defun rank-facep-filter (x)
(cond ((endp x) nil)
((rank-facep (car x))
(cons (car x) (rank-facep-filter (cdr x))))
(t (rank-facep-filter (cdr x)))))
(defmacro rank-face-list-to-score (x)
`(* 10 (len ,x)))
(defmacro score-without-aces (x)
`(+ (sum (rank-natp-filter ,x))
(rank-face-list-to-score (rank-facep-filter ,x))))
(defthm natp-score-without-aces
(let ((s (score-without-aces x)))
(and (integerp s)
(<= 0 s))))
(defun ace-count (x)
(declare (xargs :guard (rank-listp x)))
(cond ((endp x) 0)
((rank-acep (car x)) (+ 1 (ace-count (cdr x))))
(t (ace-count (cdr x)))))
(defthm natp-ace-count
(and (integerp (ace-count x))
(<= 0 (ace-count x))))
(defmacro add-ace-scores (s ac)
`(cond
((equal ,ac 0) ,s)
((< (+ ,s 10) 21) (+ ,s 11 (- ,ac 1)))
(t (+ ,s 1 (- ,ac 1)))))
(defthm natp-add-ace-scores
(implies (and (integerp x)
(<= 0 x)
(integerp y)
(<= 0 y))
(let ((s (add-ace-scores x y)))
(and (integerp s)
(<= 0 s)))))
(defmacro nat-score (x)
`(add-ace-scores (score-without-aces ,x)
(ace-count ,x)))
(defthm natp-nat-score
(implies (rank-listp x)
(and (integerp (nat-score x))
(<= 0 (nat-score x))))
:rule-classes (:rewrite :forward-chaining))
(defmacro score (x)
`(cond
((and (< 21 (nat-score ,x))) 'BUST)
((and (equal (len ,x) 2) (equal (nat-score ,x) 21))
'NATURAL-BLACKJACK)
(t (nat-score ,x))))
(defmacro scorep (x)
`(or (equal ,x 'bust)
(equal ,x 'natural-blackjack)
(if (integerp ,x)
(if (< ,x 0)
nil
(< ,x 22))
nil)))
(defthm natp-sum
(implies (nat-listp x)
(and (integerp (sum x))
(<= 0 (sum x))))
:rule-classes (:rewrite :forward-chaining))
(defthm nat-listp-rank-natp-filter
(implies (rank-listp x)
(rank-nat-listp (rank-natp-filter x)))
:rule-classes (:rewrite :forward-chaining))
(defthm scorep-score
(implies (rank-listp x)
(scorep (score x))))
(defmacro score-judge (player dealer)
`(cond
((and (equal ,player 'NATURAL-BLACKJACK)
(equal ,dealer 'NATURAL-BLACKJACK))
'PUSH)
((equal ,player 'NATURAL-BLACKJACK) 'WIN)
((equal ,dealer 'NATURAL-BLACKJACK) 'LOSE)
((equal ,player 'BUST) 'LOSE)
((equal ,dealer 'BUST) 'WIN)
((< ,player ,dealer) 'LOSE)
((> ,player ,dealer) 'WIN)
(t 'PUSH)))
(defmacro judge (player dealer)
`(score-judge (score (card-list-to-rank-list ,player))
(score (card-list-to-rank-list ,dealer))))
(defmacro judgementp (x)
`(or (equal ,x 'NATURAL-BLACKJACK)
(equal ,x 'BUST)
(equal ,x 'LOSE)
(equal ,x 'WIN)
(equal ,x 'PUSH)))
(defthm judgementp-score-judge
(judgementp (score-judge p d)))
(defthm if-bust-then-lose
(equal (score-judge 'BUST x) 'LOSE))
(defthm if-draw-a-face-card-and-have-a-ace-card-only-then-natural-blackjack
(implies (and (rank-facep face)
(rank-acep ace))
(equal (score (list ace face))
'NATURAL-BLACKJACK)))
(defun no-rank-acep (x)
(if (endp x)
t
(and (not (rank-acep (car x)))
(no-rank-acep (cdr x)))))
(defthm if-draw-a-face-when-12-then-bust
(implies (and (rank-listp rs)
(no-rank-acep rs)
(rank-facep face)
(equal (nat-score rs) 12))
(equal (score (cons face rs)) 'BUST)))
(defthm safe-to-hit
(implies (and (rank-listp rs)
(rankp new)
(<= (nat-score rs) 11))
(not (equal (score (cons new rs)) 'BUST))))
|
