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