Cookies disclaimer

I agree Our site saves small pieces of text information (cookies) on your device in order to deliver better content and for statistical purposes. You can disable the usage of cookies by changing the settings of your browser. By browsing our website without changing the browser settings you grant us permission to store that information on your device.

[2018-Oct] Sudoku

Isabelle is trying do solve a Sudoku, but she somehow got stuck and now she wonders whether there is actually a solution.

Can you help her out? 

+-----------+-----------+-----------+
|     9     | 7         |      6    |
|           | 2   3     | 1         |
| 3   1   5 |           |           |
+-----------+-----------+-----------+
|         6 |     1     |     3     |
| 8       2 |           |         9 |
| 9         |         3 |         4 |
+-----------+-----------+-----------+
|         8 |         6 | 7         |
|     4     |     7     | 8   2     |
|           | 8   4     |           |
+-----------+-----------+-----------+

Resources

Download Files

Definitions File 

theory Defs
  imports Main
begin
 

no_notation Groups.one_class.one ("1")

datatype digit = A ("1") | B ("2") | C ("3") | D ("4") | E ("5") | F ("6") | G ("7") | H ("8") | I ("9")

definition valid :: "digit => digit => digit => digit => digit => digit => digit => digit => digit => bool" where

  "valid x1 x2 x3 x4 x5 x6 x7 x8 x9 ==
    (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)
    \<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)
    \<and> (x3 \<noteq> x4) \<and> (x3 \<noteq> x5) \<and> (x3 \<noteq> x6) \<and> (x3 \<noteq> x7) \<and> (x3 \<noteq> x8) \<and> (x3 \<noteq> x9)
    \<and> (x4 \<noteq> x5) \<and> (x4 \<noteq> x6) \<and> (x4 \<noteq> x7) \<and> (x4 \<noteq> x8) \<and> (x4 \<noteq> x9)
    \<and> (x5 \<noteq> x6) \<and> (x5 \<noteq> x7) \<and> (x5 \<noteq> x8) \<and> (x5 \<noteq> x9)
    \<and> (x6 \<noteq> x7) \<and> (x6 \<noteq> x8) \<and> (x6 \<noteq> x9)
    \<and> (x7 \<noteq> x8) \<and> (x7 \<noteq> x9)
    \<and> (x8 \<noteq> x9)"

definition sudoku :: "digit => digit => digit => digit => digit => digit => digit => digit => digit =>
    digit => digit => digit => digit => digit => digit => digit => digit => digit =>
    digit => digit => digit => digit => digit => digit => digit => digit => digit =>
    digit => digit => digit => digit => digit => digit => digit => digit => digit =>
    digit => digit => digit => digit => digit => digit => digit => digit => digit =>
    digit => digit => digit => digit => digit => digit => digit => digit => digit =>
    digit => digit => digit => digit => digit => digit => digit => digit => digit =>
    digit => digit => digit => digit => digit => digit => digit => digit => digit =>
    digit => digit => digit => digit => digit => digit => digit => digit => digit => bool" where

  "sudoku x11 x12 x13 x14 x15 x16 x17 x18 x19
          x21 x22 x23 x24 x25 x26 x27 x28 x29
          x31 x32 x33 x34 x35 x36 x37 x38 x39
          x41 x42 x43 x44 x45 x46 x47 x48 x49
          x51 x52 x53 x54 x55 x56 x57 x58 x59
          x61 x62 x63 x64 x65 x66 x67 x68 x69
          x71 x72 x73 x74 x75 x76 x77 x78 x79
          x81 x82 x83 x84 x85 x86 x87 x88 x89
          x91 x92 x93 x94 x95 x96 x97 x98 x99 ==

       valid x11 x12 x13 x14 x15 x16 x17 x18 x19
     \<and> valid x21 x22 x23 x24 x25 x26 x27 x28 x29
     \<and> valid x31 x32 x33 x34 x35 x36 x37 x38 x39
     \<and> valid x41 x42 x43 x44 x45 x46 x47 x48 x49
     \<and> valid x51 x52 x53 x54 x55 x56 x57 x58 x59
     \<and> valid x61 x62 x63 x64 x65 x66 x67 x68 x69
     \<and> valid x71 x72 x73 x74 x75 x76 x77 x78 x79
     \<and> valid x81 x82 x83 x84 x85 x86 x87 x88 x89
     \<and> valid x91 x92 x93 x94 x95 x96 x97 x98 x99

     \<and> valid x11 x21 x31 x41 x51 x61 x71 x81 x91
     \<and> valid x12 x22 x32 x42 x52 x62 x72 x82 x92
     \<and> valid x13 x23 x33 x43 x53 x63 x73 x83 x93
     \<and> valid x14 x24 x34 x44 x54 x64 x74 x84 x94
     \<and> valid x15 x25 x35 x45 x55 x65 x75 x85 x95
     \<and> valid x16 x26 x36 x46 x56 x66 x76 x86 x96
     \<and> valid x17 x27 x37 x47 x57 x67 x77 x87 x97
     \<and> valid x18 x28 x38 x48 x58 x68 x78 x88 x98
     \<and> valid x19 x29 x39 x49 x59 x69 x79 x89 x99

     \<and> valid x11 x12 x13 x21 x22 x23 x31 x32 x33
     \<and> valid x14 x15 x16 x24 x25 x26 x34 x35 x36
     \<and> valid x17 x18 x19 x27 x28 x29 x37 x38 x39
     \<and> valid x41 x42 x43 x51 x52 x53 x61 x62 x63
     \<and> valid x44 x45 x46 x54 x55 x56 x64 x65 x66
     \<and> valid x47 x48 x49 x57 x58 x59 x67 x68 x69
     \<and> valid x71 x72 x73 x81 x82 x83 x91 x92 x93
     \<and> valid x74 x75 x76 x84 x85 x86 x94 x95 x96
     \<and> valid x77 x78 x79 x87 x88 x89 x97 x98 x99"


end

Template File 

theory Submission
imports Defs
begin
  
theorem solvesudoku: "\<exists>x11     x13     x15 x16 x17     x19
          x21 x22 x23         x26     x28 x29
                      x34 x35 x36 x37 x38 x39
          x41 x42     x44     x46 x47     x49
              x52     x54 x55 x56 x57 x58    
              x62 x63 x64 x65     x67 x68    
          x71 x72     x74 x75         x78 x79
          x81     x83 x84     x86         x89
          x91 x92 x93         x96 x97 x98 x99.
    sudoku x11  9  x13  7  x15 x16 x17  6  x19
           x21 x22 x23  2   3  x26  1  x28 x29
            3   1   5  x34 x35 x36 x37 x38 x39
           x41 x42  6  x44  1  x46 x47  3  x49
            8  x52  2  x54 x55 x56 x57 x58  9 
            9  x62 x63 x64 x65  3  x67 x68  4 
           x71 x72  8  x74 x75  6   7  x78 x79
           x81  4  x83 x84  7  x86  8   2  x89
           x91 x92 x93  8   4  x96 x97 x98 x99" sorry


end

Check File 

theory Check
imports Submission
begin

theorem "\<exists>x11     x13     x15 x16 x17     x19
          x21 x22 x23         x26     x28 x29
                      x34 x35 x36 x37 x38 x39
          x41 x42     x44     x46 x47     x49
              x52     x54 x55 x56 x57 x58    
              x62 x63 x64 x65     x67 x68    
          x71 x72     x74 x75         x78 x79
          x81     x83 x84     x86         x89
          x91 x92 x93         x96 x97 x98 x99.
    sudoku x11  9  x13  7  x15 x16 x17  6  x19
           x21 x22 x23  2   3  x26  1  x28 x29
            3   1   5  x34 x35 x36 x37 x38 x39
           x41 x42  6  x44  1  x46 x47  3  x49
            8  x52  2  x54 x55 x56 x57 x58  9 
            9  x62 x63 x64 x65  3  x67 x68  4 
           x71 x72  8  x74 x75  6   7  x78 x79
           x81  4  x83 x84  7  x86  8   2  x89
           x91 x92 x93  8   4  x96 x97 x98 x99"
by(rule Submission.solvesudoku)


end
Download Files

Definitions File 

theory Defs
  imports Main
begin
 

no_notation Groups.one_class.one ("1")

datatype digit = A ("1") | B ("2") | C ("3") | D ("4") | E ("5") | F ("6") | G ("7") | H ("8") | I ("9")

definition valid :: "digit => digit => digit => digit => digit => digit => digit => digit => digit => bool" where

  "valid x1 x2 x3 x4 x5 x6 x7 x8 x9 ==
    (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)
    \<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)
    \<and> (x3 \<noteq> x4) \<and> (x3 \<noteq> x5) \<and> (x3 \<noteq> x6) \<and> (x3 \<noteq> x7) \<and> (x3 \<noteq> x8) \<and> (x3 \<noteq> x9)
    \<and> (x4 \<noteq> x5) \<and> (x4 \<noteq> x6) \<and> (x4 \<noteq> x7) \<and> (x4 \<noteq> x8) \<and> (x4 \<noteq> x9)
    \<and> (x5 \<noteq> x6) \<and> (x5 \<noteq> x7) \<and> (x5 \<noteq> x8) \<and> (x5 \<noteq> x9)
    \<and> (x6 \<noteq> x7) \<and> (x6 \<noteq> x8) \<and> (x6 \<noteq> x9)
    \<and> (x7 \<noteq> x8) \<and> (x7 \<noteq> x9)
    \<and> (x8 \<noteq> x9)"

definition sudoku :: "digit => digit => digit => digit => digit => digit => digit => digit => digit =>
    digit => digit => digit => digit => digit => digit => digit => digit => digit =>
    digit => digit => digit => digit => digit => digit => digit => digit => digit =>
    digit => digit => digit => digit => digit => digit => digit => digit => digit =>
    digit => digit => digit => digit => digit => digit => digit => digit => digit =>
    digit => digit => digit => digit => digit => digit => digit => digit => digit =>
    digit => digit => digit => digit => digit => digit => digit => digit => digit =>
    digit => digit => digit => digit => digit => digit => digit => digit => digit =>
    digit => digit => digit => digit => digit => digit => digit => digit => digit => bool" where

  "sudoku x11 x12 x13 x14 x15 x16 x17 x18 x19
          x21 x22 x23 x24 x25 x26 x27 x28 x29
          x31 x32 x33 x34 x35 x36 x37 x38 x39
          x41 x42 x43 x44 x45 x46 x47 x48 x49
          x51 x52 x53 x54 x55 x56 x57 x58 x59
          x61 x62 x63 x64 x65 x66 x67 x68 x69
          x71 x72 x73 x74 x75 x76 x77 x78 x79
          x81 x82 x83 x84 x85 x86 x87 x88 x89
          x91 x92 x93 x94 x95 x96 x97 x98 x99 ==

       valid x11 x12 x13 x14 x15 x16 x17 x18 x19
     \<and> valid x21 x22 x23 x24 x25 x26 x27 x28 x29
     \<and> valid x31 x32 x33 x34 x35 x36 x37 x38 x39
     \<and> valid x41 x42 x43 x44 x45 x46 x47 x48 x49
     \<and> valid x51 x52 x53 x54 x55 x56 x57 x58 x59
     \<and> valid x61 x62 x63 x64 x65 x66 x67 x68 x69
     \<and> valid x71 x72 x73 x74 x75 x76 x77 x78 x79
     \<and> valid x81 x82 x83 x84 x85 x86 x87 x88 x89
     \<and> valid x91 x92 x93 x94 x95 x96 x97 x98 x99

     \<and> valid x11 x21 x31 x41 x51 x61 x71 x81 x91
     \<and> valid x12 x22 x32 x42 x52 x62 x72 x82 x92
     \<and> valid x13 x23 x33 x43 x53 x63 x73 x83 x93
     \<and> valid x14 x24 x34 x44 x54 x64 x74 x84 x94
     \<and> valid x15 x25 x35 x45 x55 x65 x75 x85 x95
     \<and> valid x16 x26 x36 x46 x56 x66 x76 x86 x96
     \<and> valid x17 x27 x37 x47 x57 x67 x77 x87 x97
     \<and> valid x18 x28 x38 x48 x58 x68 x78 x88 x98
     \<and> valid x19 x29 x39 x49 x59 x69 x79 x89 x99

     \<and> valid x11 x12 x13 x21 x22 x23 x31 x32 x33
     \<and> valid x14 x15 x16 x24 x25 x26 x34 x35 x36
     \<and> valid x17 x18 x19 x27 x28 x29 x37 x38 x39
     \<and> valid x41 x42 x43 x51 x52 x53 x61 x62 x63
     \<and> valid x44 x45 x46 x54 x55 x56 x64 x65 x66
     \<and> valid x47 x48 x49 x57 x58 x59 x67 x68 x69
     \<and> valid x71 x72 x73 x81 x82 x83 x91 x92 x93
     \<and> valid x74 x75 x76 x84 x85 x86 x94 x95 x96
     \<and> valid x77 x78 x79 x87 x88 x89 x97 x98 x99"


end

Template File 

theory Submission
imports Defs
begin
  
theorem solvesudoku: "\<exists>x11     x13     x15 x16 x17     x19
          x21 x22 x23         x26     x28 x29
                      x34 x35 x36 x37 x38 x39
          x41 x42     x44     x46 x47     x49
              x52     x54 x55 x56 x57 x58    
              x62 x63 x64 x65     x67 x68    
          x71 x72     x74 x75         x78 x79
          x81     x83 x84     x86         x89
          x91 x92 x93         x96 x97 x98 x99.
    sudoku x11  9  x13  7  x15 x16 x17  6  x19
           x21 x22 x23  2   3  x26  1  x28 x29
            3   1   5  x34 x35 x36 x37 x38 x39
           x41 x42  6  x44  1  x46 x47  3  x49
            8  x52  2  x54 x55 x56 x57 x58  9 
            9  x62 x63 x64 x65  3  x67 x68  4 
           x71 x72  8  x74 x75  6   7  x78 x79
           x81  4  x83 x84  7  x86  8   2  x89
           x91 x92 x93  8   4  x96 x97 x98 x99" sorry


end

Check File 

theory Check
imports Submission
begin

theorem "\<exists>x11     x13     x15 x16 x17     x19
          x21 x22 x23         x26     x28 x29
                      x34 x35 x36 x37 x38 x39
          x41 x42     x44     x46 x47     x49
              x52     x54 x55 x56 x57 x58    
              x62 x63 x64 x65     x67 x68    
          x71 x72     x74 x75         x78 x79
          x81     x83 x84     x86         x89
          x91 x92 x93         x96 x97 x98 x99.
    sudoku x11  9  x13  7  x15 x16 x17  6  x19
           x21 x22 x23  2   3  x26  1  x28 x29
            3   1   5  x34 x35 x36 x37 x38 x39
           x41 x42  6  x44  1  x46 x47  3  x49
            8  x52  2  x54 x55 x56 x57 x58  9 
            9  x62 x63 x64 x65  3  x67 x68  4 
           x71 x72  8  x74 x75  6   7  x78 x79
           x81  4  x83 x84  7  x86  8   2  x89
           x91 x92 x93  8   4  x96 x97 x98 x99"
by(rule Submission.solvesudoku)


end
Terms and Conditions