1 2(*****************************************************************************) 3(* Puzzle from http://www.lego.com/matanui *) 4(*****************************************************************************) 5 6(*****************************************************************************) 7(* Nine boolean state variables *) 8(* *) 9(* 0 --- 1 --- 2 *) 10(* | | | *) 11(* | | | *) 12(* 3 --- 4 --- 5 *) 13(* | | | *) 14(* | | | *) 15(* 6 --- 7 --- 8 *) 16(* *) 17(* A transition consists of complementing a variable and all its *) 18(* immediate neighbours. *) 19(* *) 20(* Problem is whether one can get from *) 21(* *) 22(* *) 23(* F --- T --- F *) 24(* | | | *) 25(* | | | *) 26(* T --- F --- T *) 27(* | | | *) 28(* | | | *) 29(* F --- T --- F *) 30(* *) 31(* to *) 32(* *) 33(* *) 34(* F --- F --- F *) 35(* | | | *) 36(* | | | *) 37(* F --- F --- F *) 38(* | | | *) 39(* | | | *) 40(* F --- F --- F *) 41(* *) 42(*****************************************************************************) 43 44(* Comment out for compilation 45load "HolBddLib"; 46load "PrimitiveBddRules"; 47load "ListPair"; 48*) 49 50(* Needed for compilation *) 51open HolKernel Parse boolLib; 52infixr 3 -->; 53infix 9 by; 54infix ++; 55infix ## |-> THEN THENL THENC ORELSE ORELSEC THEN_TCL ORELSE_TCL; 56(**) 57 58open bossLib; 59open HolBddLib; 60open bdd; 61open pairSyntax; 62open pairTools; 63open pairTheory; 64 65val _ = new_theory "KatiPuzzle"; 66 67(*****************************************************************************) 68(* Varmap (i.e. variable ordering) for later use *) 69(*****************************************************************************) 70 71val basic_varmap = 72 extendVarmap 73 (map 74 (fn s => mk_var(s,bool)) 75 ["v0","v1","v2","v3","v4","v5","v6","v7","v8", 76 "v0'","v1'","v2'","v3'","v4'","v5'","v6'","v7'","v8'", 77 "c0","c1","c2","c3", 78 "c0'","c1'","c2'","c3'"]) 79 empty; 80 81(*****************************************************************************) 82(* Initial state *) 83(*****************************************************************************) 84 85val Init_def = 86 Define 87 `Init(v0,v1,v2,v3,v4,v5,v6,v7,v8,c0:bool,c1:bool,c2:bool,c3:bool) = 88 (~v0 /\ v1 /\ ~v2 /\ v3 /\ ~v4 /\ v5 /\ ~v6 /\ v7 /\ ~v8)`; 89 90(*****************************************************************************) 91(* Transition relation *) 92(*****************************************************************************) 93 94val Trans_def = 95 Define 96 `Trans((v0,v1,v2,v3,v4,v5,v6,v7,v8,c0:bool,c1:bool,c2:bool,c3:bool), 97 (v0',v1',v2',v3',v4',v5',v6',v7',v8',c0',c1',c2',c3')) = 98 (((v0'=~v0)/\(v1'=~v1)/\(v2'=v2)/\(v3'=~v3)/\(v4'=v4)/\ (* toggle 0 *) 99 (v5'=v5)/\(v6'=v6)/\(v7'=v7)/\(v8'=v8) /\ ~c3' /\ ~c2' /\ ~c1' /\~c0') 100 \/ 101 ((v0'=~v0)/\(v1'=~v1)/\(v2'=~v2)/\(v3'=v3)/\(v4'=~v4)/\ (* toggle 1 *) 102 (v5'=v5)/\(v6'=v6)/\(v7'=v7)/\(v8'=v8) /\ ~c3' /\ ~c2' /\ ~c1' /\ c0') 103 \/ 104 ((v0'=v0)/\(v1'=~v1)/\(v2'=~v2)/\(v3'=v3)/\(v4'=v4)/\ (* toggle 2 *) 105 (v5'=~v5)/\(v6'=v6)/\(v7'=v7)/\(v8'=v8) /\ ~c3' /\ ~c2' /\ c1' /\ ~c0') 106 \/ 107 ((v0'=~v0)/\(v1'=v1)/\(v2'=v2)/\(v3'=~v3)/\(v4'=~v4)/\ (* toggle 3 *) 108 (v5'=v5)/\(v6'=~v6)/\(v7'=v7)/\(v8'=v8) /\ ~c3' /\ ~c2' /\ c1' /\ c0') 109 \/ 110 ((v0'=v0)/\(v1'=~v1)/\(v2'=v2)/\(v3'=~v3)/\(v4'=~v4)/\ (* toggle 4 *) 111 (v5'=~v5)/\(v6'=v6)/\(v7'=~v7)/\(v8'=v8) /\ ~c3' /\ c2' /\ ~c1' /\ ~c0') 112 \/ 113 ((v0'=v0)/\(v1'=v1)/\(v2'=~v2)/\(v3'=v3)/\(v4'=~v4)/\ (* toggle 5 *) 114 (v5'=~v5)/\(v6'=v6)/\(v7'=v7)/\(v8'=~v8) /\ ~c3' /\ c2' /\ ~c1' /\ c0') 115 \/ 116 ((v0'=v0)/\(v1'=v1)/\(v2'=v2)/\(v3'=~v3)/\(v4'=v4)/\ (* toggle 6 *) 117 (v5'=v5)/\(v6'=~v6)/\(v7'=~v7)/\(v8'=v8) /\ ~c3' /\ c2' /\ c1' /\ ~c0') 118 \/ 119 ((v0'=v0)/\(v1'=v1)/\(v2'=v2)/\(v3'=v3)/\(v4'=~v4)/\ (* toggle 7 *) 120 (v5'=v5)/\(v6'=~v6)/\(v7'=~v7)/\(v8'=~v8) /\ ~c3' /\ c2' /\ c1' /\ c0') 121 \/ 122 ((v0'=v0)/\(v1'=v1)/\(v2'=v2)/\(v3'=v3)/\(v4'=v4)/\ (* toggle 8 *) 123 (v5'=~v5)/\(v6'=v6)/\(v7'=~v7)/\(v8'=~v8) /\ c3' /\ ~c2' /\ ~c1' /\ ~c0'))`; 124 125(*****************************************************************************) 126(* Final state *) 127(*****************************************************************************) 128 129val Final_def = 130 Define 131 `Final(v0,v1,v2,v3,v4,v5,v6,v7,v8,c0:bool,c1:bool,c2:bool,c3:bool) = 132 (~v0 /\ ~v1 /\ ~v2 /\ ~v3 /\ ~v4 /\ ~v5 /\ ~v6 /\ ~v7 /\ ~v8)`; 133 134val (_,thl,thfin) = findTrace basic_varmap Trans_def Init_def Final_def; 135 136(****************************************************************************** 137Stuff commented out here superceded by findTrace 138 139val s = 140 ``(v0:bool,v1:bool,v2:bool,v3:bool,v4:bool,v5:bool,v6:bool,v7:bool,v8:bool, 141 c0:bool,c1:bool,c2:bool,c3:bool)``; 142 143val (by_th0,by_thsuc) = 144 time 145 (REWRITE_RULE[Eq_def,pairTheory.PAIR_EQ] ## REWRITE_RULE[Trans_def]) 146 (MkIterThms 147 MachineTransitionTheory.ReachBy_rec 148 (lhs(concl(SPEC_ALL Trans_def))) 149 (lhs(concl(ISPECL[``(F,T,F,T,F,T,F,T,F,F,F,F,F)``,s]Eq_def)))); 150 151val (FinalTb,FinalTb') = 152 computeFixedpoint 153 (fn n => fn tb => print ".") 154 basic_varmap 155 (by_th0,by_thsuc); 156 157val ReachTb = 158 BddEqMp 159 (SYM 160 (AP_THM 161 (MATCH_MP 162 ReachBy_fixedpoint 163 (EXT 164 (PGEN 165 (mk_var("s",type_of s)) 166 s 167 (BddThmOracle(BddOp(Biimp,FinalTb,FinalTb')))))) 168 s)) 169 FinalTb; 170 171val Trace = 172 computeTrace 173 (fn n => fn tb => print".") 174 basic_varmap 175 Final_def 176 (by_th0,by_thsuc); 177 178val Solution = traceBack basic_varmap Trace Final_def Trans_def; 179******************************************************************************) 180 181(*****************************************************************************) 182(* Print out a picture of a puzzle state from a tuple *) 183(* *) 184(* (v0,v1,v2,v3,v4,v5,v6,v7,v8,c0,c1,c2,c3) *) 185(* *) 186(* where vi is T or F, and if n is V[c3,c2,c1,c0] the printing is *) 187(* *) 188(* n *) 189(* 0 --- 1 --- 2 *) 190(* | | | *) 191(* | | | *) 192(* 3 --- 4 --- 5 *) 193(* | | | *) 194(* | | | *) 195(* 6 --- 7 --- 8 *) 196(* *) 197(* (number is omitted if flag is false) *) 198(*****************************************************************************) 199 200fun PrintState flag tm = 201 let val cl = strip_pair tm 202 fun s n = el (n+1) cl 203 fun p n = print_term(s n) 204 fun sp () = print " --- " 205 fun nl () = print"\n" 206 fun bv b = if b ~~ T then 1 else 0 207 fun pb(c3,c2,c1,c0) = print_term(intToTerm(8*(bv c3) + 4*(bv c2) + 2*(bv c1) + (bv c0))) 208 in 209 (nl(); 210 (if flag then (print" "; pb(s 12, s 11, s 10, s 9) ; nl()) else ()); 211 print" " ;p 0 ;sp();p 1 ;sp();p 2 ;nl(); 212 print" | | |"; nl(); 213 print" " ;p 3 ;sp();p 4 ;sp();p 5 ;nl(); 214 print" | | |"; nl(); 215 print" " ;p 6 ;sp();p 7 ;sp();p 8 ;nl(); nl(); nl()) 216 end; 217 218(*****************************************************************************) 219(* Print out a trace as found by traceBack *) 220(*****************************************************************************) 221 222fun PrintTrace cl = 223 (print "\nThe number shows the position toggled to get to the following state\n\n"; 224 PrintState false (hd cl); 225 map (PrintState true) (tl cl)); 226 227val _ = PrintTrace 228 (List.map (fst o dest_pair o rand o concl) thl @ [rand(concl thfin)]) 229 230(* Solution found 231 232The number shows the position toggled to get to the following state 233 234 235 F --- T --- F 236 | | | 237 T --- F --- T 238 | | | 239 F --- T --- F 240 241 242 243 1 244 T --- F --- T 245 | | | 246 T --- T --- T 247 | | | 248 F --- T --- F 249 250 251 252 3 253 F --- F --- T 254 | | | 255 F --- F --- T 256 | | | 257 T --- T --- F 258 259 260 261 5 262 F --- F --- F 263 | | | 264 F --- T --- F 265 | | | 266 T --- T --- T 267 268 269 270 7 271 F --- F --- F 272 | | | 273 F --- F --- F 274 | | | 275 F --- F --- F 276 277*) 278 279 280val _ = export_theory(); 281