src/HOL/ex/Sudoku.thy
 author bulwahn Fri Oct 21 11:17:14 2011 +0200 (2011-10-21) changeset 45231 d85a2fdc586c parent 41589 bbd861837ebc child 54703 499f92dc6e45 permissions -rw-r--r--
replacing code_inline by code_unfold, removing obsolete code_unfold, code_inline del now that the ancient code generator is removed
 wenzelm@41589  1 (* Title: HOL/ex/Sudoku.thy  webertj@18408  2  Author: Tjark Weber  webertj@28949  3  Copyright 2005-2008  webertj@18408  4 *)  webertj@18408  5 webertj@18408  6 header {* A SAT-based Sudoku Solver *}  webertj@18408  7 webertj@18408  8 theory Sudoku  webertj@18408  9 imports Main  webertj@18408  10 begin  webertj@18408  11 webertj@18408  12 text {*  webertj@28949  13  Please make sure you are using an efficient SAT solver (e.g., zChaff)  webertj@18408  14  when loading this theory. See Isabelle's settings file for details.  webertj@18408  15 webertj@28949  16  Using zChaff, each Sudoku in this theory is solved in less than a  webertj@28949  17  second.  webertj@28949  18 webertj@18408  19  See the paper "A SAT-based Sudoku Solver" (Tjark Weber, published at  webertj@18408  20  LPAR'05) for further explanations.  webertj@18408  21 *}  webertj@18408  22 webertj@18408  23 datatype digit = A ("1") | B ("2") | C ("3") | D ("4") | E ("5") | F ("6") | G ("7") | H ("8") | I ("9")  webertj@18408  24 haftmann@35416  25 definition valid :: "digit => digit => digit => digit => digit => digit => digit => digit => digit => bool" where  webertj@18408  26 webertj@18408  27  "valid x1 x2 x3 x4 x5 x6 x7 x8 x9 ==  webertj@18408  28  (x1 \ x2) \ (x1 \ x3) \ (x1 \ x4) \ (x1 \ x5) \ (x1 \ x6) \ (x1 \ x7) \ (x1 \ x8) \ (x1 \ x9)  webertj@18408  29  \ (x2 \ x3) \ (x2 \ x4) \ (x2 \ x5) \ (x2 \ x6) \ (x2 \ x7) \ (x2 \ x8) \ (x2 \ x9)  webertj@18408  30  \ (x3 \ x4) \ (x3 \ x5) \ (x3 \ x6) \ (x3 \ x7) \ (x3 \ x8) \ (x3 \ x9)  webertj@18408  31  \ (x4 \ x5) \ (x4 \ x6) \ (x4 \ x7) \ (x4 \ x8) \ (x4 \ x9)  webertj@18408  32  \ (x5 \ x6) \ (x5 \ x7) \ (x5 \ x8) \ (x5 \ x9)  webertj@18408  33  \ (x6 \ x7) \ (x6 \ x8) \ (x6 \ x9)  webertj@18408  34  \ (x7 \ x8) \ (x7 \ x9)  webertj@18408  35  \ (x8 \ x9)"  webertj@18408  36 haftmann@35416  37 definition sudoku :: "digit => digit => digit => digit => digit => digit => digit => digit => digit =>  webertj@18408  38  digit => digit => digit => digit => digit => digit => digit => digit => digit =>  webertj@18408  39  digit => digit => digit => digit => digit => digit => digit => digit => digit =>  webertj@18408  40  digit => digit => digit => digit => digit => digit => digit => digit => digit =>  webertj@18408  41  digit => digit => digit => digit => digit => digit => digit => digit => digit =>  webertj@18408  42  digit => digit => digit => digit => digit => digit => digit => digit => digit =>  webertj@18408  43  digit => digit => digit => digit => digit => digit => digit => digit => digit =>  webertj@18408  44  digit => digit => digit => digit => digit => digit => digit => digit => digit =>  haftmann@35416  45  digit => digit => digit => digit => digit => digit => digit => digit => digit => bool" where  webertj@18408  46 webertj@18408  47  "sudoku x11 x12 x13 x14 x15 x16 x17 x18 x19  webertj@18408  48  x21 x22 x23 x24 x25 x26 x27 x28 x29  webertj@18408  49  x31 x32 x33 x34 x35 x36 x37 x38 x39  webertj@18408  50  x41 x42 x43 x44 x45 x46 x47 x48 x49  webertj@18408  51  x51 x52 x53 x54 x55 x56 x57 x58 x59  webertj@18408  52  x61 x62 x63 x64 x65 x66 x67 x68 x69  webertj@18408  53  x71 x72 x73 x74 x75 x76 x77 x78 x79  webertj@18408  54  x81 x82 x83 x84 x85 x86 x87 x88 x89  webertj@18408  55  x91 x92 x93 x94 x95 x96 x97 x98 x99 ==  webertj@18408  56 webertj@18408  57  valid x11 x12 x13 x14 x15 x16 x17 x18 x19  webertj@18408  58  \ valid x21 x22 x23 x24 x25 x26 x27 x28 x29  webertj@18408  59  \ valid x31 x32 x33 x34 x35 x36 x37 x38 x39  webertj@18408  60  \ valid x41 x42 x43 x44 x45 x46 x47 x48 x49  webertj@18408  61  \ valid x51 x52 x53 x54 x55 x56 x57 x58 x59  webertj@18408  62  \ valid x61 x62 x63 x64 x65 x66 x67 x68 x69  webertj@18408  63  \ valid x71 x72 x73 x74 x75 x76 x77 x78 x79  webertj@18408  64  \ valid x81 x82 x83 x84 x85 x86 x87 x88 x89  webertj@18408  65  \ valid x91 x92 x93 x94 x95 x96 x97 x98 x99  webertj@18408  66 webertj@18408  67  \ valid x11 x21 x31 x41 x51 x61 x71 x81 x91  webertj@18408  68  \ valid x12 x22 x32 x42 x52 x62 x72 x82 x92  webertj@18408  69  \ valid x13 x23 x33 x43 x53 x63 x73 x83 x93  webertj@18408  70  \ valid x14 x24 x34 x44 x54 x64 x74 x84 x94  webertj@18408  71  \ valid x15 x25 x35 x45 x55 x65 x75 x85 x95  webertj@18408  72  \ valid x16 x26 x36 x46 x56 x66 x76 x86 x96  webertj@18408  73  \ valid x17 x27 x37 x47 x57 x67 x77 x87 x97  webertj@18408  74  \ valid x18 x28 x38 x48 x58 x68 x78 x88 x98  webertj@18408  75  \ valid x19 x29 x39 x49 x59 x69 x79 x89 x99  webertj@18408  76 webertj@18408  77  \ valid x11 x12 x13 x21 x22 x23 x31 x32 x33  webertj@18408  78  \ valid x14 x15 x16 x24 x25 x26 x34 x35 x36  webertj@18408  79  \ valid x17 x18 x19 x27 x28 x29 x37 x38 x39  webertj@18408  80  \ valid x41 x42 x43 x51 x52 x53 x61 x62 x63  webertj@18408  81  \ valid x44 x45 x46 x54 x55 x56 x64 x65 x66  webertj@18408  82  \ valid x47 x48 x49 x57 x58 x59 x67 x68 x69  webertj@18408  83  \ valid x71 x72 x73 x81 x82 x83 x91 x92 x93  webertj@18408  84  \ valid x74 x75 x76 x84 x85 x86 x94 x95 x96  webertj@18408  85  \ valid x77 x78 x79 x87 x88 x89 x97 x98 x99"  webertj@18408  86 webertj@18408  87 text {*  webertj@18408  88  Just an arbitrary Sudoku grid:  webertj@18408  89 *}  webertj@18408  90 webertj@18408  91 theorem "\ sudoku  webertj@18408  92  x11 x12 x13 x14 x15 x16 x17 x18 x19  webertj@18408  93  x21 x22 x23 x24 x25 x26 x27 x28 x29  webertj@18408  94  x31 x32 x33 x34 x35 x36 x37 x38 x39  webertj@18408  95  x41 x42 x43 x44 x45 x46 x47 x48 x49  webertj@18408  96  x51 x52 x53 x54 x55 x56 x57 x58 x59  webertj@18408  97  x61 x62 x63 x64 x65 x66 x67 x68 x69  webertj@18408  98  x71 x72 x73 x74 x75 x76 x77 x78 x79  webertj@18408  99  x81 x82 x83 x84 x85 x86 x87 x88 x89  webertj@18408  100  x91 x92 x93 x94 x95 x96 x97 x98 x99"  webertj@18408  101  refute  webertj@18408  102 oops  webertj@18408  103 webertj@18408  104 text {*  webertj@18408  105  An "easy" Sudoku:  webertj@18408  106 *}  webertj@18408  107 webertj@18408  108 theorem "\ sudoku  webertj@18408  109  5 3 x13 x14 7 x16 x17 x18 x19  webertj@18408  110  6 x22 x23 1 9 5 x27 x28 x29  webertj@18408  111  x31 9 8 x34 x35 x36 x37 6 x39  webertj@18408  112  8 x42 x43 x44 6 x46 x47 x48 3  webertj@18408  113  4 x52 x53 8 x55 3 x57 x58 1  webertj@18408  114  7 x62 x63 x64 2 x66 x67 x68 6  webertj@18408  115  x71 6 x73 x74 x75 x76 2 8 x79  webertj@18408  116  x81 x82 x83 4 1 9 x87 x88 5  webertj@18408  117  x91 x92 x93 x94 8 x96 x97 7 9 "  webertj@18408  118  refute  webertj@18408  119 oops  webertj@18408  120 webertj@18408  121 text {*  webertj@18408  122  A "hard" Sudoku:  webertj@18408  123 *}  webertj@18408  124 webertj@18408  125 theorem "\ sudoku  webertj@18408  126  x11 2 x13 x14 x15 x16 x17 x18 x19  webertj@18408  127  x21 x22 x23 6 x25 x26 x27 x28 3  webertj@18408  128  x31 7 4 x34 8 x36 x37 x38 x39  webertj@18408  129  x41 x42 x43 x44 x45 3 x47 x48 2  webertj@18408  130  x51 8 x53 x54 4 x56 x57 1 x59  webertj@18408  131  6 x62 x63 5 x65 x66 x67 x68 x69  webertj@18408  132  x71 x72 x73 x74 1 x76 7 8 x79  webertj@18408  133  5 x82 x83 x84 x85 9 x87 x88 x89  webertj@18408  134  x91 x92 x93 x94 x95 x96 x97 4 x99"  webertj@18408  135  refute  webertj@18408  136 oops  webertj@18408  137 webertj@28949  138 text {*  webertj@28949  139  Some "exceptionally difficult" Sudokus, taken from  webertj@28949  140  \url{http://en.wikipedia.org/w/index.php?title=Algorithmics_of_sudoku&oldid=254685903}  webertj@28949  141  (accessed December 2, 2008).  webertj@28949  142 *}  webertj@28949  143 webertj@28949  144 text {*  webertj@28949  145 \begin{verbatim}  webertj@28949  146 Rating Program: gsf's sudoku q1 (rating)  webertj@28949  147 Rating: 99408  webertj@28949  148 Poster: JPF  webertj@28949  149 Label: Easter Monster  webertj@28949  150 1.......2.9.4...5...6...7...5.9.3.......7.......85..4.7.....6...3...9.8...2.....1  webertj@28949  151 1 . . | . . . | . . 2  webertj@28949  152 . 9 . | 4 . . | . 5 .  webertj@28949  153 . . 6 | . . . | 7 . .  webertj@28949  154 ------+-------+------  webertj@28949  155 . 5 . | 9 . 3 | . . .  webertj@28949  156 . . . | . 7 . | . . .  webertj@28949  157 . . . | 8 5 . | . 4 .  webertj@28949  158 ------+-------+------  webertj@28949  159 7 . . | . . . | 6 . .  webertj@28949  160 . 3 . | . . 9 | . 8 .  webertj@28949  161 . . 2 | . . . | . . 1  webertj@28949  162 \end{verbatim}  webertj@28949  163 *}  webertj@28949  164 webertj@28949  165 theorem "\ sudoku  webertj@28949  166  1 x12 x13 x14 x15 x16 x17 x18 2  webertj@28949  167  x21 9 x23 4 x25 x26 x27 5 x29  webertj@28949  168  x31 x32 6 x34 x35 x36 7 x38 x39  webertj@28949  169  x41 5 x43 9 x45 3 x47 x48 x49  webertj@28949  170  x51 x52 x53 x54 7 x56 x57 x58 x59  webertj@28949  171  x61 x62 x63 8 5 x66 x67 4 x69  webertj@28949  172  7 x72 x73 x74 x75 x76 6 x78 x79  webertj@28949  173  x81 3 x83 x84 x85 9 x87 8 x89  webertj@28949  174  x91 x92 2 x94 x95 x96 x97 x98 1 "  webertj@28949  175  refute  webertj@28949  176 oops  webertj@28949  177 webertj@28949  178 text {*  webertj@28949  179 \begin{verbatim}  webertj@28949  180 Rating Program: gsf's sudoku q1 (Processing time)  webertj@28949  181 Rating: 4m19s@2 GHz  webertj@28949  182 Poster: tarek  webertj@28949  183 Label: tarek071223170000-052  webertj@28949  184 ..1..4.......6.3.5...9.....8.....7.3.......285...7.6..3...8...6..92......4...1...  webertj@28949  185 . . 1 | . . 4 | . . .  webertj@28949  186 . . . | . 6 . | 3 . 5  webertj@28949  187 . . . | 9 . . | . . .  webertj@28949  188 ------+-------+------  webertj@28949  189 8 . . | . . . | 7 . 3  webertj@28949  190 . . . | . . . | . 2 8  webertj@28949  191 5 . . | . 7 . | 6 . .  webertj@28949  192 ------+-------+------  webertj@28949  193 3 . . | . 8 . | . . 6  webertj@28949  194 . . 9 | 2 . . | . . .  webertj@28949  195 . 4 . | . . 1 | . . .  webertj@28949  196 \end{verbatim}  webertj@28949  197 *}  webertj@28949  198 webertj@28949  199 theorem "\ sudoku  webertj@28949  200  x11 x12 1 x14 x15 4 x17 x18 x19  webertj@28949  201  x21 x22 x23 x24 6 x26 3 x28 5  webertj@28949  202  x31 x32 x33 9 x35 x36 x37 x38 x39  webertj@28949  203  8 x42 x43 x44 x45 x46 7 x48 3  webertj@28949  204  x51 x52 x53 x54 x55 x56 x57 2 8  webertj@28949  205  5 x62 x63 x64 7 x66 6 x68 x69  webertj@28949  206  3 x72 x73 x74 8 x76 x77 x78 6  webertj@28949  207  x81 x82 9 2 x85 x86 x87 x88 x89  webertj@28949  208  x91 4 x93 x94 x95 1 x97 x98 x99"  webertj@28949  209  refute  webertj@28949  210 oops  webertj@28949  211 webertj@28949  212 text {*  webertj@28949  213 \begin{verbatim}  webertj@28949  214 Rating Program: Nicolas Juillerat's Sudoku explainer 1.2.1  webertj@28949  215 Rating: 11.9  webertj@28949  216 Poster: tarek  webertj@28949  217 Label: golden nugget  webertj@28949  218 .......39.....1..5..3.5.8....8.9...6.7...2...1..4.......9.8..5..2....6..4..7.....  webertj@28949  219 . . . | . . . | . 3 9  webertj@28949  220 . . . | . . 1 | . . 5  webertj@28949  221 . . 3 | . 5 . | 8 . .  webertj@28949  222 ------+-------+------  webertj@28949  223 . . 8 | . 9 . | . . 6  webertj@28949  224 . 7 . | . . 2 | . . .  webertj@28949  225 1 . . | 4 . . | . . .  webertj@28949  226 ------+-------+------  webertj@28949  227 . . 9 | . 8 . | . 5 .  webertj@28949  228 . 2 . | . . . | 6 . .  webertj@28949  229 4 . . | 7 . . | . . .  webertj@28949  230 \end{verbatim}  webertj@28949  231 *}  webertj@28949  232 webertj@28949  233 theorem "\ sudoku  webertj@28949  234  x11 x12 x13 x14 x15 x16 x17 3 9  webertj@28949  235  x21 x22 x23 x24 x25 1 x27 x28 5  webertj@28949  236  x31 x32 3 x34 5 x36 8 x38 x39  webertj@28949  237  x41 x42 8 x44 9 x46 x47 x48 6  webertj@28949  238  x51 7 x53 x54 x55 2 x57 x58 x59  webertj@28949  239  1 x62 x63 4 x65 x66 x67 x68 x69  webertj@28949  240  x71 x72 9 x74 8 x76 x77 5 x79  webertj@28949  241  x81 2 x83 x84 x85 x86 6 x88 x89  webertj@28949  242  4 x92 x93 7 x95 x96 x97 x98 x99"  webertj@28949  243  refute  webertj@28949  244 oops  webertj@28949  245 webertj@28949  246 text {*  webertj@28949  247 \begin{verbatim}  webertj@28949  248 Rating Program: dukuso's suexrat9  webertj@28949  249 Rating: 4483  webertj@28949  250 Poster: coloin  webertj@28949  251 Label: col-02-08-071  webertj@28949  252 .2.4.37.........32........4.4.2...7.8...5.........1...5.....9...3.9....7..1..86..  webertj@28949  253 . 2 . | 4 . 3 | 7 . .  webertj@28949  254 . . . | . . . | . 3 2  webertj@28949  255 . . . | . . . | . . 4  webertj@28949  256 ------+-------+------  webertj@28949  257 . 4 . | 2 . . | . 7 .  webertj@28949  258 8 . . | . 5 . | . . .  webertj@28949  259 . . . | . . 1 | . . .  webertj@28949  260 ------+-------+------  webertj@28949  261 5 . . | . . . | 9 . .  webertj@28949  262 . 3 . | 9 . . | . . 7  webertj@28949  263 . . 1 | . . 8 | 6 . .  webertj@28949  264 \end{verbatim}  webertj@28949  265 *}  webertj@28949  266 webertj@28949  267 theorem "\ sudoku  webertj@28949  268  x11 2 x13 4 x15 3 7 x18 x19  webertj@28949  269  x21 x22 x23 x24 x25 x26 x27 3 2  webertj@28949  270  x31 x32 x33 x34 x35 x36 x37 x38 4  webertj@28949  271  x41 4 x43 2 x45 x46 x47 7 x49  webertj@28949  272  8 x52 x53 x54 5 x56 x57 x58 x59  webertj@28949  273  x61 x62 x63 x64 x65 1 x67 x68 x69  webertj@28949  274  5 x72 x73 x74 x75 x76 9 x78 x79  webertj@28949  275  x81 3 x83 9 x85 x86 x87 x88 7  webertj@28949  276  x91 x92 1 x94 x95 8 6 x98 x99"  webertj@28949  277  refute  webertj@28949  278 oops  webertj@28949  279 webertj@28949  280 text {*  webertj@28949  281 \begin{verbatim}  webertj@28949  282 Rating Program: dukuso's suexratt (10000 2 option)  webertj@28949  283 Rating: 2141  webertj@28949  284 Poster: tarek  webertj@28949  285 Label: golden nugget  webertj@28949  286 .......39.....1..5..3.5.8....8.9...6.7...2...1..4.......9.8..5..2....6..4..7.....  webertj@28949  287 . . . | . . . | . 3 9  webertj@28949  288 . . . | . . 1 | . . 5  webertj@28949  289 . . 3 | . 5 . | 8 . .  webertj@28949  290 ------+-------+------  webertj@28949  291 . . 8 | . 9 . | . . 6  webertj@28949  292 . 7 . | . . 2 | . . .  webertj@28949  293 1 . . | 4 . . | . . .  webertj@28949  294 ------+-------+------  webertj@28949  295 . . 9 | . 8 . | . 5 .  webertj@28949  296 . 2 . | . . . | 6 . .  webertj@28949  297 4 . . | 7 . . | . . .  webertj@28949  298 \end{verbatim}  webertj@28949  299 *}  webertj@28949  300 webertj@28949  301 theorem "\ sudoku  webertj@28949  302  x11 x12 x13 x14 x15 x16 x17 3 9  webertj@28949  303  x21 x22 x23 x24 x25 1 x27 x28 5  webertj@28949  304  x31 x32 3 x34 5 x36 8 x38 x39  webertj@28949  305  x41 x42 8 x44 9 x46 x47 x48 6  webertj@28949  306  x51 7 x53 x54 x55 2 x57 x58 x59  webertj@28949  307  1 x62 x63 4 x65 x66 x67 x68 x69  webertj@28949  308  x71 x72 9 x74 8 x76 x77 5 x79  webertj@28949  309  x81 2 x83 x84 x85 x86 6 x88 x89  webertj@28949  310  4 x92 x93 7 x95 x96 x97 x98 x99"  webertj@28949  311  refute  webertj@28949  312 oops  webertj@28949  313 webertj@18408  314 end