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 67val _ = Globals.priming := SOME ""; 68 69(*****************************************************************************) 70(* Varmap (i.e. variable ordering) for later use *) 71(*****************************************************************************) 72 73val basic_varmap = 74 extendVarmap 75 (map 76 (fn s => mk_var(s,bool)) 77 ["v0","v1","v2","v3","v4","v5","v6","v7","v8", 78 "v0'","v1'","v2'","v3'","v4'","v5'","v6'","v7'","v8'", 79 "c0","c1","c2","c3", 80 "c0'","c1'","c2'","c3'"]) 81 empty; 82 83(*****************************************************************************) 84(* Initial state *) 85(*****************************************************************************) 86 87val Init_def = 88 Define 89 `Init(v0,v1,v2,v3,v4,v5,v6,v7,v8,c0:bool,c1:bool,c2:bool,c3:bool) = 90 ~v0 /\ v1 /\ ~v2 /\ v3 /\ ~v4 /\ v5 /\ ~v6 /\ v7 /\ ~v8`; 91 92(*****************************************************************************) 93(* Transition relation *) 94(*****************************************************************************) 95 96val Trans_def = 97 Define 98 `Trans((v0,v1,v2,v3,v4,v5,v6,v7,v8,c0:bool,c1:bool,c2:bool,c3:bool), 99 (v0',v1',v2',v3',v4',v5',v6',v7',v8',c0',c1',c2',c3')) = 100 ((v0'=~v0)/\(v1'=~v1)/\(v2'=v2)/\(v3'=~v3)/\(v4'=v4)/\ (* toggle 0 *) 101 (v5'=v5)/\(v6'=v6)/\(v7'=v7)/\(v8'=v8) /\ ~c3' /\ ~c2' /\ ~c1' /\~c0') 102 \/ 103 ((v0'=~v0)/\(v1'=~v1)/\(v2'=~v2)/\(v3'=v3)/\(v4'=~v4)/\ (* toggle 1 *) 104 (v5'=v5)/\(v6'=v6)/\(v7'=v7)/\(v8'=v8) /\ ~c3' /\ ~c2' /\ ~c1' /\ c0') 105 \/ 106 ((v0'=v0)/\(v1'=~v1)/\(v2'=~v2)/\(v3'=v3)/\(v4'=v4)/\ (* toggle 2 *) 107 (v5'=~v5)/\(v6'=v6)/\(v7'=v7)/\(v8'=v8) /\ ~c3' /\ ~c2' /\ c1' /\ ~c0') 108 \/ 109 ((v0'=~v0)/\(v1'=v1)/\(v2'=v2)/\(v3'=~v3)/\(v4'=~v4)/\ (* toggle 3 *) 110 (v5'=v5)/\(v6'=~v6)/\(v7'=v7)/\(v8'=v8) /\ ~c3' /\ ~c2' /\ c1' /\ c0') 111 \/ 112 ((v0'=v0)/\(v1'=~v1)/\(v2'=v2)/\(v3'=~v3)/\(v4'=~v4)/\ (* toggle 4 *) 113 (v5'=~v5)/\(v6'=v6)/\(v7'=~v7)/\(v8'=v8) /\ ~c3' /\ c2' /\ ~c1' /\ ~c0') 114 \/ 115 ((v0'=v0)/\(v1'=v1)/\(v2'=~v2)/\(v3'=v3)/\(v4'=~v4)/\ (* toggle 5 *) 116 (v5'=~v5)/\(v6'=v6)/\(v7'=v7)/\(v8'=~v8) /\ ~c3' /\ c2' /\ ~c1' /\ c0') 117 \/ 118 ((v0'=v0)/\(v1'=v1)/\(v2'=v2)/\(v3'=~v3)/\(v4'=v4)/\ (* toggle 6 *) 119 (v5'=v5)/\(v6'=~v6)/\(v7'=~v7)/\(v8'=v8) /\ ~c3' /\ c2' /\ c1' /\ ~c0') 120 \/ 121 ((v0'=v0)/\(v1'=v1)/\(v2'=v2)/\(v3'=v3)/\(v4'=~v4)/\ (* toggle 7 *) 122 (v5'=v5)/\(v6'=~v6)/\(v7'=~v7)/\(v8'=~v8) /\ ~c3' /\ c2' /\ c1' /\ c0') 123 \/ 124 ((v0'=v0)/\(v1'=v1)/\(v2'=v2)/\(v3'=v3)/\(v4'=v4)/\ (* toggle 8 *) 125 (v5'=~v5)/\(v6'=v6)/\(v7'=~v7)/\(v8'=~v8) /\ c3' /\ ~c2' /\ ~c1' /\ ~c0')`; 126 127(*****************************************************************************) 128(* Final state *) 129(*****************************************************************************) 130 131val Final_def = 132 Define 133 `Final(v0,v1,v2,v3,v4,v5,v6,v7,v8,c0:bool,c1:bool,c2:bool,c3:bool) = 134 ~v0 /\ ~v1 /\ ~v2 /\ ~v3 /\ ~v4 /\ ~v5 /\ ~v6 /\ ~v7 /\ ~v8`; 135 136val (_,thl,thfin) = findTrace basic_varmap Trans_def Init_def Final_def; 137 138(****************************************************************************** 139Stuff commented out here superceded by findTrace 140 141val s = 142 ``(v0:bool,v1:bool,v2:bool,v3:bool,v4:bool,v5:bool,v6:bool,v7:bool,v8:bool, 143 c0:bool,c1:bool,c2:bool,c3:bool)``; 144 145val (by_th0,by_thsuc) = 146 time 147 (REWRITE_RULE[Eq_def,pairTheory.PAIR_EQ] ## REWRITE_RULE[Trans_def]) 148 (MkIterThms 149 MachineTransitionTheory.ReachBy_rec 150 (lhs(concl(SPEC_ALL Trans_def))) 151 (lhs(concl(ISPECL[``(F,T,F,T,F,T,F,T,F,F,F,F,F)``,s]Eq_def)))); 152 153val (FinalTb,FinalTb') = 154 computeFixedpoint 155 (fn n => fn tb => print ".") 156 basic_varmap 157 (by_th0,by_thsuc); 158 159val ReachTb = 160 BddEqMp 161 (SYM 162 (AP_THM 163 (MATCH_MP 164 ReachBy_fixedpoint 165 (EXT 166 (PGEN 167 (mk_var("s",type_of s)) 168 s 169 (BddThmOracle(BddOp(Biimp,FinalTb,FinalTb')))))) 170 s)) 171 FinalTb; 172 173val Trace = 174 computeTrace 175 (fn n => fn tb => print".") 176 basic_varmap 177 Final_def 178 (by_th0,by_thsuc); 179 180val Solution = traceBack basic_varmap Trace Final_def Trans_def; 181******************************************************************************) 182 183(*****************************************************************************) 184(* Print out a picture of a puzzle state from a tuple *) 185(* *) 186(* (v0,v1,v2,v3,v4,v5,v6,v7,v8,c0,c1,c2,c3) *) 187(* *) 188(* where vi is T or F, and if n is V[c3,c2,c1,c0] the printing is *) 189(* *) 190(* n *) 191(* 0 --- 1 --- 2 *) 192(* | | | *) 193(* | | | *) 194(* 3 --- 4 --- 5 *) 195(* | | | *) 196(* | | | *) 197(* 6 --- 7 --- 8 *) 198(* *) 199(* (number is omitted if flag is false) *) 200(*****************************************************************************) 201 202fun PrintState flag tm = 203 let val cl = strip_pair tm 204 fun s n = el (n+1) cl 205 fun p n = print_term(s n) 206 fun sp () = print " --- " 207 fun nl () = print"\n" 208 fun bv b = if b=T then 1 else 0 209 fun pb(c3,c2,c1,c0) = print_term(intToTerm(8*(bv c3) + 4*(bv c2) + 2*(bv c1) + (bv c0))) 210 in 211 (nl(); 212 (if flag then (print" "; pb(s 12, s 11, s 10, s 9) ; nl()) else ()); 213 print" " ;p 0 ;sp();p 1 ;sp();p 2 ;nl(); 214 print" | | |"; nl(); 215 print" " ;p 3 ;sp();p 4 ;sp();p 5 ;nl(); 216 print" | | |"; nl(); 217 print" " ;p 6 ;sp();p 7 ;sp();p 8 ;nl(); nl(); nl()) 218 end; 219 220(*****************************************************************************) 221(* Print out a trace as found by traceBack *) 222(*****************************************************************************) 223 224fun PrintTrace cl = 225 (print "\nThe number shows the position toggled to get to the following state\n\n"; 226 PrintState false (hd cl); 227 map (PrintState true) (tl cl)); 228 229val _ = PrintTrace 230 (List.map (fst o dest_pair o rand o concl) thl @ [rand(concl thfin)]) 231 232(* Solution found 233 234The number shows the position toggled to get to the following state 235 236 237 F --- T --- F 238 | | | 239 T --- F --- T 240 | | | 241 F --- T --- F 242 243 244 245 1 246 T --- F --- T 247 | | | 248 T --- T --- T 249 | | | 250 F --- T --- F 251 252 253 254 3 255 F --- F --- T 256 | | | 257 F --- F --- T 258 | | | 259 T --- T --- F 260 261 262 263 5 264 F --- F --- F 265 | | | 266 F --- T --- F 267 | | | 268 T --- T --- T 269 270 271 272 7 273 F --- F --- F 274 | | | 275 F --- F --- F 276 | | | 277 F --- F --- F 278 279*) 280 281 282val _ = export_theory(); 283