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