1(*****************************************************************************)
2(* Game of Solitaire (example from Bill Roscoe, but suggested by Tony Hoare) *)
3(*****************************************************************************)
4
5(*****************************************************************************)
6(* State variable numbering:                                                 *)
7(*                                                                           *)
8(*              ----------------                                             *)
9(*              | 07 | 14 | 21 |                                             *)
10(*              ----------------                                             *)
11(*              | 08 | 15 | 22 |                                             *)
12(*    ------------------------------------                                   *)
13(*    | 01 | 04 | 09 | 16 | 23 | 28 | 31 |                                   *)
14(*    ------------------------------------                                   *)
15(*    | 02 | 05 | 10 | 17 | 24 | 29 | 32 |                                   *)
16(*    ------------------------------------                                   *)
17(*    | 03 | 06 | 11 | 18 | 25 | 30 | 33 |                                   *)
18(*    ------------------------------------                                   *)
19(*              | 12 | 19 | 26 |                                             *)
20(*              ----------------                                             *)
21(*              | 13 | 20 | 27 |                                             *)
22(*              ----------------                                             *)
23(*                                                                           *)
24(*****************************************************************************)
25
26(*
27load "HolBddLib";
28load "PrimitiveBddRules";
29load "ListPair";
30*)
31
32open HolKernel Parse boolLib;
33infixr 3 -->;
34infix 9 by;
35infix ++;
36infix ## |-> THEN THENL THENC ORELSE ORELSEC THEN_TCL ORELSE_TCL;
37
38
39open HolBddLib;
40open pairSyntax;
41open bossLib;
42
43val _ = (Globals.priming := SOME "");
44
45val _ = new_theory "Solitaire";
46
47val var_list as
48    [v01,v02,v03,v04,v05,v06,v07,v08,v09,v10,
49     v11,v12,v13,v14,v15,v16,v17,v18,v19,v20,
50     v21,v22,v23,v24,v25,v26,v27,v28,v29,v30,
51     v31,v32,v33] =
52    ["v01","v02","v03","v04","v05",
53     "v06","v07","v08","v09","v10",
54     "v11","v12","v13","v14","v15",
55     "v16","v17","v18","v19","v20",
56     "v21","v22","v23","v24","v25",
57     "v26","v27","v28","v29","v30",
58     "v31","v32","v33"];
59
60val var_list' as
61    [v01',v02',v03',v04',v05',v06',v07',v08',v09',v10',
62     v11',v12',v13',v14',v15',v16',v17',v18',v19',v20',
63     v21',v22',v23',v24',v25',v26',v27',v28',v29',v30',
64     v31',v32',v33'] =
65    map (fn v => v^"'") var_list;
66
67(*****************************************************************************)
68(* Make boolean variables (unprimed and primed)                              *)
69(*****************************************************************************)
70
71fun mk_bool_var s = mk_var(s,bool)
72and mk_primed_bool_var s = mk_bool_var(s^"'");
73
74(*****************************************************************************)
75(* Good variable order is V01 < v01' < v02 < v02' ...                        *)
76(* Function shuffle below used to create it                                  *)
77(*****************************************************************************)
78
79fun shuffle (l1,l2) =
80 ListPair.foldr (fn(x1,x2,l) => x1 :: x2 :: l) [] (l1,l2);
81
82val solitaire_varmap =
83 extendVarmap (map mk_bool_var (shuffle(var_list,var_list'))) empty;
84
85(*****************************************************************************)
86(* State vectors                                                             *)
87(*****************************************************************************)
88
89val st  = list_mk_pair (map mk_bool_var var_list)
90and st' = list_mk_pair (map mk_bool_var var_list');
91
92(*****************************************************************************)
93(* Initial state                                                             *)
94(*****************************************************************************)
95
96val SolitaireInit_def =
97 Define
98   `SolitaireInit ^st =
99     ^(list_mk_conj(map (fn v => if v="v17" then mk_neg(mk_bool_var v)
100                                            else mk_bool_var v) var_list))`;
101
102(*****************************************************************************)
103(* Final goal state                                                          *)
104(*****************************************************************************)
105
106val SolitaireFinal_def =
107 Define
108   `SolitaireFinal ^st =
109     ^(list_mk_conj
110        (map (fn v => if v="v17" then mk_bool_var v
111                                 else mk_neg(mk_bool_var v)) var_list))`;
112
113(*****************************************************************************)
114(* Function to create a formula to represent a move in which a counter at v1 *)
115(* jumps over and takes one at v2 and lands at v3, which must have been      *)
116(* unoccupied.                                                               *)
117(*****************************************************************************)
118
119fun make_move_trans (v1,v2,v3) =
120 let val (_,unchanged) = List.partition (fn v => mem v [v1,v2,v3]) var_list
121 in
122 list_mk_conj
123  ([mk_bool_var v1, mk_bool_var v2, mk_neg(mk_bool_var v3),
124    mk_neg(mk_primed_bool_var v1), mk_neg(mk_primed_bool_var v2), mk_primed_bool_var v3]
125   @
126   (map (fn v => mk_eq(mk_primed_bool_var v,mk_bool_var v)) unchanged))
127 end;
128
129(*****************************************************************************)
130(* List of all possible moves                                                *)
131(*****************************************************************************)
132
133val moves =
134 [(v01,v04,v09), (v01,v02,v03),
135  (v02,v05,v10),
136  (v03,v02,v01), (v03,v06,v11),
137  (v04,v05,v06), (v04,v09,v16),
138  (v05,v10,v17),
139  (v06,v05,v04), (v06,v11,v18),
140  (v07,v08,v09), (v07,v14,v21),
141  (v08,v09,v10), (v08,v15,v22),
142  (v09,v08,v07), (v09,v10,v11), (v09,v04,v01), (v09,v16,v23),
143  (v10,v09,v08), (v10,v11,v12), (v10,v05,v02), (v10,v17,v24),
144  (v11,v10,v09), (v11,v12,v13), (v11,v06,v03), (v11,v18,v25),
145  (v12,v11,v10), (v12,v19,v26),
146  (v13,v12,v11), (v13,v20,v27),
147  (v14,v15,v16),
148  (v15,v16,v17),
149  (v16,v15,v14), (v16,v17,v18), (v16,v09,v04), (v16,v23,v28),
150  (v17,v16,v15), (v17,v18,v19), (v17,v10,v05), (v17,v24,v29),
151  (v18,v17,v16), (v18,v19,v20), (v18,v11,v06), (v18,v25,v30),
152  (v19,v18,v17),
153  (v20,v19,v18),
154  (v21,v22,v23), (v21,v14,v07),
155  (v22,v23,v24), (v22,v15,v08),
156  (v23,v22,v21), (v23,v24,v25), (v23,v16,v09), (v23,v28,v31),
157  (v24,v23,v22), (v24,v25,v26), (v24,v17,v10), (v24,v29,v32),
158  (v25,v24,v23), (v25,v26,v27), (v25,v18,v11), (v25,v30,v33),
159  (v26,v25,v24), (v26,v19,v12),
160  (v27,v26,v25), (v27,v20,v13),
161  (v28,v29,v30), (v28,v23,v16),
162  (v29,v24,v17),
163  (v30,v29,v28), (v30,v25,v18),
164  (v31,v32,v33), (v31,v28,v23),
165  (v32,v29,v24),
166  (v33,v32,v31), (v33,v30,v25)];
167
168(*****************************************************************************)
169(* Define transition relation as disjunction of all moves                    *)
170(*****************************************************************************)
171
172val SolitaireTrans_def =
173 Define
174  `SolitaireTrans(^st,^st') = ^(list_mk_disj(map make_move_trans moves))`;
175
176val (initth,transthl,finalth) =
177 time
178  (findTrace solitaire_varmap SolitaireTrans_def SolitaireInit_def)
179  SolitaireFinal_def;
180
181(*
182val trace_list = ref[];
183
184fun report n tb =
185 (trace_list := append (!trace_list) [tb]; print "Iteration: "; print (Int.toString n);
186  print " Node size: "; print(Int.toString(bdd.nodecount(getBdd tb))); print "\n");
187
188val (in_th0,in_thsuc) =
189 time
190  (REWRITE_RULE[SolitaireInit_def] ## REWRITE_RULE[SolitaireTrans_def])
191  (MkIterThms
192    MachineTransitionTheory.ReachBy_rec
193    (lhs(concl(SPEC_ALL SolitaireTrans_def)))
194    (lhs(concl(SPEC_ALL SolitaireInit_def))));
195
196val (tb,tb') = time (computeFixedpoint report solitaire_varmap) (in_th0,in_thsuc);
197
198val (in_th0,in_thsuc) =
199 time
200  (REWRITE_RULE[SolitaireInit_def] ##
201   simpLib.SIMP_RULE boolSimps.bool_ss [SolitaireTrans_def,LEFT_AND_OVER_OR,EXISTS_OR_THM])
202  (MkIterThms
203    MachineTransitionTheory.ReachBy_rec
204    (lhs(concl(SPEC_ALL SolitaireTrans_def)))
205    (lhs(concl(SPEC_ALL SolitaireInit_def))));
206
207val (tb1,tb1') = time (computeFixedpoint report solitaire_varmap) (in_th0,in_thsuc);
208*)
209
210(*****************************************************************************)
211(* Print out a picture of a Solitaire board from a tuple                     *)
212(*                                                                           *)
213(*   (c1,c2,c3,c4,c5,c6,c7,c8,c9,c10,c11,c12,c13,c14,c15,c16,c17,c18,c19,    *)
214(*   (c21,c22,c23,c24,c25,c26,c27,c28,c29,c30,c31,c32,c3)                    *)
215(*                                                                           *)
216(* where cij is T or F                                                       *)
217(*                                                                           *)
218(* and the printing is                                                       *)
219(*                                                                           *)
220(*      XXX                                                                  *)
221(*      XXX                                                                  *)
222(*    XXXXXXX                                                                *)
223(*    XXXXXXX                                                                *)
224(*    XXXXXXX                                                                *)
225(*      XXX                                                                  *)
226(*      XXX                                                                  *)
227(*****************************************************************************)
228
229fun PrintState tm =
230 let val cl    = strip_pair tm
231     fun p n   = if el n cl = ``T`` then print "1" else print "0"
232     fun sp () = print "   "
233     fun nl () = print"\n"
234 in
235  (print"  ";p 07;p 14;p 21;nl();
236   print"  ";p 08;p 15;p 22;nl();
237   p 01;p 04;p 09;p 16;p 23;p 28;p 31;nl();
238   p 02;p 05;p 10;p 17;p 24;p 29;p 32;nl();
239   p 03;p 06;p 11;p 18;p 25;p 30;p 33;nl();
240   print"  ";p 12;p 19;p 26;nl();
241   print"  ";p 13;p 20;p 22;nl();nl())
242 end;
243
244(*****************************************************************************)
245(* Print out a trace as found by findTrace                                   *)
246(*****************************************************************************)
247
248val _ =
249 List.map
250  PrintState
251  (List.map (fst o dest_pair o rand o concl) transthl @ [rand(concl finalth)]);
252
253val _ = export_theory();
254
255
256(* Reachable state with/without disjunctive partitioning
257
258fun computeSimpReachable vm Rth Bth =
259 let val (by_th0,by_thsuc) =
260          (REWRITE_RULE[Bth,pairTheory.PAIR_EQ] ## REWRITE_RULE[Rth])
261           (MkIterThms
262             MachineTransitionTheory.ReachBy_rec
263             (lhs(concl(SPEC_ALL Rth)))
264             (lhs(concl(SPEC_ALL Bth))))
265     val _ = print "Starting disjunctive partitioning ...\n"
266     val by_thsuc_simp = time MakeSimpRecThm by_thsuc
267     val _ = print "disjunctive partitioning complete.\n"
268     val _ = print "Computing reachable states ...\n"
269 in
270  time (computeFixedpoint (fn n=>fn tb=>print".") vm) (by_th0,by_thsuc_simp)
271 end;
272
273val SimpReachable =
274 computeSimpReachable solitaire_varmap SolitaireTrans_def SolitaireInit_def;
275
276(*
277Starting disjunctive partitioning ...
278runtime: 1112.520s,    gctime: 512.900s,     systime: 1.750s.
279disjunctive partitioning complete.
280Computing reachable states ...
281
282*)
283
284fun computeReachable vm Rth Bth =
285 let val (by_th0,by_thsuc) =
286          (REWRITE_RULE[Bth,pairTheory.PAIR_EQ] ## REWRITE_RULE[Rth])
287           (MkIterThms
288             MachineTransitionTheory.ReachBy_rec
289             (lhs(concl(SPEC_ALL Rth)))
290             (lhs(concl(SPEC_ALL Bth))))
291 in
292  time (computeFixedpoint (fn n=>fn tb=>print".") vm) (by_th0,by_thsuc)
293 end;
294
295val Reachable =
296 computeSimpReachable solitaire_varmap SolitaireTrans_def SolitaireInit_def;
297
298*)
299