21 LPAR'05) for further explanations. |
21 LPAR'05) for further explanations. |
22 *} |
22 *} |
23 |
23 |
24 datatype digit = A ("1") | B ("2") | C ("3") | D ("4") | E ("5") | F ("6") | G ("7") | H ("8") | I ("9") |
24 datatype digit = A ("1") | B ("2") | C ("3") | D ("4") | E ("5") | F ("6") | G ("7") | H ("8") | I ("9") |
25 |
25 |
26 constdefs |
26 definition valid :: "digit => digit => digit => digit => digit => digit => digit => digit => digit => bool" where |
27 valid :: "digit => digit => digit => digit => digit => digit => digit => digit => digit => bool" |
|
28 |
27 |
29 "valid x1 x2 x3 x4 x5 x6 x7 x8 x9 == |
28 "valid x1 x2 x3 x4 x5 x6 x7 x8 x9 == |
30 (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 (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) |
31 \<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> (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) |
32 \<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> (x3 \<noteq> x4) \<and> (x3 \<noteq> x5) \<and> (x3 \<noteq> x6) \<and> (x3 \<noteq> x7) \<and> (x3 \<noteq> x8) \<and> (x3 \<noteq> x9) |
34 \<and> (x5 \<noteq> x6) \<and> (x5 \<noteq> x7) \<and> (x5 \<noteq> x8) \<and> (x5 \<noteq> x9) |
33 \<and> (x5 \<noteq> x6) \<and> (x5 \<noteq> x7) \<and> (x5 \<noteq> x8) \<and> (x5 \<noteq> x9) |
35 \<and> (x6 \<noteq> x7) \<and> (x6 \<noteq> x8) \<and> (x6 \<noteq> x9) |
34 \<and> (x6 \<noteq> x7) \<and> (x6 \<noteq> x8) \<and> (x6 \<noteq> x9) |
36 \<and> (x7 \<noteq> x8) \<and> (x7 \<noteq> x9) |
35 \<and> (x7 \<noteq> x8) \<and> (x7 \<noteq> x9) |
37 \<and> (x8 \<noteq> x9)" |
36 \<and> (x8 \<noteq> x9)" |
38 |
37 |
39 constdefs |
38 definition sudoku :: "digit => digit => digit => digit => digit => digit => digit => digit => digit => |
40 sudoku :: "digit => digit => digit => digit => digit => digit => digit => digit => digit => |
39 digit => digit => digit => digit => digit => digit => digit => digit => digit => |
41 digit => digit => digit => digit => digit => digit => digit => digit => digit => |
40 digit => digit => digit => digit => digit => digit => digit => digit => digit => |
42 digit => digit => digit => digit => digit => digit => digit => digit => digit => |
41 digit => digit => digit => digit => digit => digit => digit => digit => digit => |
43 digit => digit => digit => digit => digit => digit => digit => digit => digit => |
42 digit => digit => digit => digit => digit => digit => digit => digit => digit => |
44 digit => digit => digit => digit => digit => digit => digit => digit => digit => |
43 digit => digit => digit => digit => digit => digit => digit => digit => digit => |
45 digit => digit => digit => digit => digit => digit => digit => digit => digit => |
44 digit => digit => digit => digit => digit => digit => digit => digit => digit => |
46 digit => digit => digit => digit => digit => digit => digit => digit => digit => |
45 digit => digit => digit => digit => digit => digit => digit => digit => digit => |
47 digit => digit => digit => digit => digit => digit => digit => digit => digit => |
46 digit => digit => digit => digit => digit => digit => digit => digit => digit => bool" where |
48 digit => digit => digit => digit => digit => digit => digit => digit => digit => bool" |
|
49 |
47 |
50 "sudoku x11 x12 x13 x14 x15 x16 x17 x18 x19 |
48 "sudoku x11 x12 x13 x14 x15 x16 x17 x18 x19 |
51 x21 x22 x23 x24 x25 x26 x27 x28 x29 |
49 x21 x22 x23 x24 x25 x26 x27 x28 x29 |
52 x31 x32 x33 x34 x35 x36 x37 x38 x39 |
50 x31 x32 x33 x34 x35 x36 x37 x38 x39 |
53 x41 x42 x43 x44 x45 x46 x47 x48 x49 |
51 x41 x42 x43 x44 x45 x46 x47 x48 x49 |