Replaced refute with nitpick.
authorwebertj
Mon May 12 00:13:38 2014 +0200 (2014-05-12)
changeset 5694035ce6dab3f5e
parent 56939 c2ddbf327bbd
child 56941 952833323c99
Replaced refute with nitpick.
src/HOL/ROOT
src/HOL/ex/Sudoku.thy
     1.1 --- a/src/HOL/ROOT	Mon May 12 12:38:17 2014 +0200
     1.2 +++ b/src/HOL/ROOT	Mon May 12 00:13:38 2014 +0200
     1.3 @@ -581,13 +581,11 @@
     1.4      Simps_Case_Conv_Examples
     1.5      ML
     1.6      SAT_Examples
     1.7 +    Sudoku
     1.8    theories [skip_proofs = false]
     1.9      Meson_Test
    1.10    theories [condition = SVC_HOME]
    1.11      svc_test
    1.12 -  theories [condition = ZCHAFF_HOME]
    1.13 -    (*requires zChaff (or some other reasonably fast SAT solver)*)
    1.14 -    Sudoku
    1.15    document_files "root.bib" "root.tex"
    1.16  
    1.17  session "HOL-Isar_Examples" in Isar_Examples = HOL +
     2.1 --- a/src/HOL/ex/Sudoku.thy	Mon May 12 12:38:17 2014 +0200
     2.2 +++ b/src/HOL/ex/Sudoku.thy	Mon May 12 00:13:38 2014 +0200
     2.3 @@ -1,24 +1,23 @@
     2.4  (*  Title:      HOL/ex/Sudoku.thy
     2.5      Author:     Tjark Weber
     2.6 -    Copyright   2005-2008
     2.7 +    Copyright   2005-2014
     2.8  *)
     2.9  
    2.10  header {* A SAT-based Sudoku Solver *}
    2.11  
    2.12  theory Sudoku
    2.13 -imports Main "../Library/Refute"
    2.14 +imports Main
    2.15  begin
    2.16  
    2.17  text {*
    2.18 -  Please make sure you are using an efficient SAT solver (e.g., zChaff)
    2.19 -  when loading this theory.  See Isabelle's settings file for details.
    2.20 +  See the paper ``A SAT-based Sudoku Solver'' (Tjark Weber, published at
    2.21 +  LPAR'05) for further explanations.  (The paper describes an older version of
    2.22 +  this theory that used the model finder @{text refute} to find Sudoku
    2.23 +  solutions.  The @{text refute} tool has since been superseded by
    2.24 +  @{text nitpick}, which is used below.)
    2.25 +*}
    2.26  
    2.27 -  Using zChaff, each Sudoku in this theory is solved in less than a
    2.28 -  second.
    2.29 -
    2.30 -  See the paper "A SAT-based Sudoku Solver" (Tjark Weber, published at
    2.31 -  LPAR'05) for further explanations.
    2.32 -*}
    2.33 +no_notation Groups.one_class.one ("1")
    2.34  
    2.35  datatype digit = A ("1") | B ("2") | C ("3") | D ("4") | E ("5") | F ("6") | G ("7") | H ("8") | I ("9")
    2.36  
    2.37 @@ -98,11 +97,11 @@
    2.38      x71 x72 x73 x74 x75 x76 x77 x78 x79
    2.39      x81 x82 x83 x84 x85 x86 x87 x88 x89
    2.40      x91 x92 x93 x94 x95 x96 x97 x98 x99"
    2.41 -  refute
    2.42 +  nitpick [expect=genuine]
    2.43  oops
    2.44  
    2.45  text {*
    2.46 -  An "easy" Sudoku:
    2.47 +  An ``easy'' Sudoku:
    2.48  *}
    2.49  
    2.50  theorem "\<not> sudoku
    2.51 @@ -115,11 +114,11 @@
    2.52      x71  6  x73 x74 x75 x76  2   8  x79
    2.53      x81 x82 x83  4   1   9  x87 x88  5 
    2.54      x91 x92 x93 x94  8  x96 x97  7   9 "
    2.55 -  refute
    2.56 +  nitpick [expect=genuine]
    2.57  oops
    2.58  
    2.59  text {*
    2.60 -  A "hard" Sudoku:
    2.61 +  A ``hard'' Sudoku:
    2.62  *}
    2.63  
    2.64  theorem "\<not> sudoku
    2.65 @@ -132,13 +131,13 @@
    2.66      x71 x72 x73 x74  1  x76  7   8  x79
    2.67       5  x82 x83 x84 x85  9  x87 x88 x89
    2.68      x91 x92 x93 x94 x95 x96 x97  4  x99"
    2.69 -  refute
    2.70 +  nitpick [expect=genuine]
    2.71  oops
    2.72  
    2.73  text {*
    2.74 -  Some "exceptionally difficult" Sudokus, taken from
    2.75 +  Some ``exceptionally difficult'' Sudokus, taken from
    2.76    @{url "http://en.wikipedia.org/w/index.php?title=Algorithmics_of_sudoku&oldid=254685903"}
    2.77 -  (accessed December 2, 2008).
    2.78 +  (accessed December~2, 2008).
    2.79  *}
    2.80  
    2.81  text {*
    2.82 @@ -172,7 +171,7 @@
    2.83       7  x72 x73 x74 x75 x76  6  x78 x79
    2.84      x81  3  x83 x84 x85  9  x87  8  x89
    2.85      x91 x92  2  x94 x95 x96 x97 x98  1 "
    2.86 -  refute
    2.87 +  nitpick [expect=genuine]
    2.88  oops
    2.89  
    2.90  text {*
    2.91 @@ -206,7 +205,7 @@
    2.92       3  x72 x73 x74  8  x76 x77 x78  6 
    2.93      x81 x82  9   2  x85 x86 x87 x88 x89
    2.94      x91  4  x93 x94 x95  1  x97 x98 x99"
    2.95 -  refute
    2.96 +  nitpick [expect=genuine]
    2.97  oops
    2.98  
    2.99  text {*
   2.100 @@ -240,7 +239,7 @@
   2.101      x71 x72  9  x74  8  x76 x77  5  x79
   2.102      x81  2  x83 x84 x85 x86  6  x88 x89
   2.103       4  x92 x93  7  x95 x96 x97 x98 x99"
   2.104 -  refute
   2.105 +  nitpick [expect=genuine]
   2.106  oops
   2.107  
   2.108  text {*
   2.109 @@ -274,7 +273,7 @@
   2.110       5  x72 x73 x74 x75 x76  9  x78 x79
   2.111      x81  3  x83  9  x85 x86 x87 x88  7 
   2.112      x91 x92  1  x94 x95  8   6  x98 x99"
   2.113 -  refute
   2.114 +  nitpick [expect=genuine]
   2.115  oops
   2.116  
   2.117  text {*
   2.118 @@ -308,7 +307,7 @@
   2.119      x71 x72  9  x74  8  x76 x77  5  x79
   2.120      x81  2  x83 x84 x85 x86  6  x88 x89
   2.121       4  x92 x93  7  x95 x96 x97 x98 x99"
   2.122 -  refute
   2.123 +  nitpick [expect=genuine]
   2.124  oops
   2.125  
   2.126  end