1.1 --- a/doc-src/Nitpick/nitpick.tex	Tue Feb 09 16:05:49 2010 +0100
     1.2 +++ b/doc-src/Nitpick/nitpick.tex	Tue Feb 09 16:07:51 2010 +0100
     1.3 @@ -154,7 +154,7 @@
     1.4  the line
     1.5  
     1.6  \prew
     1.7 -\textbf{nitpick\_params} [\textit{sat\_solver}~= \textit{MiniSatJNI}, \,\textit{max\_threads}~= 1]
     1.8 +\textbf{nitpick\_params} [\textit{sat\_solver}~= \textit{MiniSat\_JNI}, \,\textit{max\_threads}~= 1]
     1.9  \postw
    1.10  
    1.11  after the \textbf{begin} keyword. The JNI version of MiniSat is bundled with
    1.12 @@ -311,9 +311,9 @@
    1.13  \slshape Constant: \nopagebreak \\
    1.14  \hbox{}\qquad $\mathit{The} = \undef{}
    1.15      (\!\begin{aligned}[t]%
    1.16 -    & \{\} := a_3,\> \{a_3\} := a_3,\> \{a_2\} := a_2, \\[-2pt] %% TYPESETTING
    1.17 -    & \{a_2, a_3\} := a_1,\> \{a_1\} := a_1,\> \{a_1, a_3\} := a_3, \\[-2pt]
    1.18 -    & \{a_1, a_2\} := a_3,\> \{a_1, a_2, a_3\} := a_3)\end{aligned}$
    1.19 +    & \{a_1, a_2, a_3\} := a_3,\> \{a_1, a_2\} := a_3,\> \{a_1, a_3\} := a_3, \\[-2pt] %% TYPESETTING
    1.20 +    & \{a_1\} := a_1,\> \{a_2, a_3\} := a_1,\> \{a_2\} := a_2, \\[-2pt]
    1.21 +    & \{a_3\} := a_3,\> \{\} := a_3)\end{aligned}$
    1.22  \postw
    1.23  
    1.24  Notice that $\textit{The}~(\lambda y.\;P~y) = \textit{The}~\{a_2, a_3\} = a_1$,
    1.25 @@ -550,7 +550,7 @@
    1.26  \slshape Nitpick found a counterexample for \textit{card} $'a$~= 3: \\[2\smallskipamount]
    1.27  \hbox{}\qquad Free variables: \nopagebreak \\
    1.28  \hbox{}\qquad\qquad $\textit{xs} = []$ \\
    1.29 -\hbox{}\qquad\qquad $\textit{y} = a_3$
    1.30 +\hbox{}\qquad\qquad $\textit{y} = a_1$
    1.31  \postw
    1.32  
    1.33  To see why the counterexample is genuine, we enable \textit{show\_consts}
    1.34 @@ -558,21 +558,21 @@
    1.35  
    1.36  \prew
    1.37  {\slshape Datatype:} \\
    1.38 -\hbox{}\qquad $'a$~\textit{list}~= $\{[],\, [a_3, a_3],\, [a_3],\, \unr\}$ \\
    1.39 +\hbox{}\qquad $'a$~\textit{list}~= $\{[],\, [a_1],\, [a_1, a_1],\, \unr\}$ \\
    1.40  {\slshape Constants:} \\
    1.41 -\hbox{}\qquad $\lambda x_1.\; x_1 \mathbin{@} [y, y] = \undef([] := [a_3, a_3])$ \\
    1.42 -\hbox{}\qquad $\textit{hd} = \undef([] := a_2,\> [a_3, a_3] := a_3,\> [a_3] := a_3)$
    1.43 +\hbox{}\qquad $\lambda x_1.\; x_1 \mathbin{@} [y, y] = \undef([] := [a_1, a_1])$ \\
    1.44 +\hbox{}\qquad $\textit{hd} = \undef([] := a_2,\> [a_1] := a_1,\> [a_1, a_1] := a_1)$
    1.45  \postw
    1.46  
    1.47  Since $\mathit{hd}~[]$ is undefined in the logic, it may be given any value,
    1.48  including $a_2$.
    1.49  
    1.50  The second constant, $\lambda x_1.\; x_1 \mathbin{@} [y, y]$, is simply the
    1.51 -append operator whose second argument is fixed to be $[y, y]$. Appending $[a_3,
    1.52 -a_3]$ to $[a_3]$ would normally give $[a_3, a_3, a_3]$, but this value is not
    1.53 +append operator whose second argument is fixed to be $[y, y]$. Appending $[a_1,
    1.54 +a_1]$ to $[a_1]$ would normally give $[a_1, a_1, a_1]$, but this value is not
    1.55  representable in the subset of $'a$~\textit{list} considered by Nitpick, which
    1.56  is shown under the ``Datatype'' heading; hence the result is $\unk$. Similarly,
    1.57 -appending $[a_3, a_3]$ to itself gives $\unk$.
    1.58 +appending $[a_1, a_1]$ to itself gives $\unk$.
    1.59  
    1.60  Given \textit{card}~$'a = 3$ and \textit{card}~$'a~\textit{list} = 3$, Nitpick
    1.61  considers the following subsets:
    1.62 @@ -600,8 +600,8 @@
    1.63  
    1.64  All subterm-closed subsets of $'a~\textit{list}$ consisting of three values
    1.65  are listed and only those. As an example of a non-subterm-closed subset,
    1.66 -consider $\mathcal{S} = \{[],\, [a_1],\,\allowbreak [a_1, a_3]\}$, and observe
    1.67 -that $[a_1, a_3]$ (i.e., $a_1 \mathbin{\#} [a_3]$) has $[a_3] \notin
    1.68 +consider $\mathcal{S} = \{[],\, [a_1],\,\allowbreak [a_1, a_2]\}$, and observe
    1.69 +that $[a_1, a_2]$ (i.e., $a_1 \mathbin{\#} [a_2]$) has $[a_2] \notin
    1.70  \mathcal{S}$ as a subterm.
    1.71  
    1.72  Here's another m\"ochtegern-lemma that Nitpick can refute without a blink:
    1.73 @@ -613,11 +613,11 @@
    1.74  \textbf{nitpick} [\textit{show\_datatypes}] \\[2\smallskipamount]
    1.75  \slshape Nitpick found a counterexample for \textit{card} $'a$~= 3: \\[2\smallskipamount]
    1.76  \hbox{}\qquad Free variables: \nopagebreak \\
    1.77 -\hbox{}\qquad\qquad $\textit{xs} = [a_2]$ \\
    1.78 -\hbox{}\qquad\qquad $\textit{ys} = [a_3]$ \\
    1.79 +\hbox{}\qquad\qquad $\textit{xs} = [a_1]$ \\
    1.80 +\hbox{}\qquad\qquad $\textit{ys} = [a_2]$ \\
    1.81  \hbox{}\qquad Datatypes: \\
    1.82  \hbox{}\qquad\qquad $\textit{nat} = \{0,\, 1,\, 2,\, \unr\}$ \\
    1.83 -\hbox{}\qquad\qquad $'a$~\textit{list} = $\{[],\, [a_3],\, [a_2],\, \unr\}$
    1.84 +\hbox{}\qquad\qquad $'a$~\textit{list} = $\{[],\, [a_1],\, [a_2],\, \unr\}$
    1.85  \postw
    1.86  
    1.87  Because datatypes are approximated using a three-valued logic, there is usually
    1.88 @@ -642,11 +642,11 @@
    1.89  \textbf{nitpick} [\textit{show\_datatypes}] \\[2\smallskipamount]
    1.90  \slshape Nitpick found a counterexample: \\[2\smallskipamount]
    1.91  \hbox{}\qquad Free variables: \nopagebreak \\
    1.92 -\hbox{}\qquad\qquad $P = \{\Abs{1},\, \Abs{0}\}$ \\
    1.93 +\hbox{}\qquad\qquad $P = \{\Abs{0},\, \Abs{1}\}$ \\
    1.94  \hbox{}\qquad\qquad $x = \Abs{2}$ \\
    1.95  \hbox{}\qquad Datatypes: \\
    1.96  \hbox{}\qquad\qquad $\textit{nat} = \{0,\, 1,\, 2,\, \unr\}$ \\
    1.97 -\hbox{}\qquad\qquad $\textit{three} = \{\Abs{2},\, \Abs{1},\, \Abs{0},\, \unr\}$
    1.98 +\hbox{}\qquad\qquad $\textit{three} = \{\Abs{0},\, \Abs{1},\, \Abs{2},\, \unr\}$
    1.99  \postw
   1.100  
   1.101  %% MARK
   1.102 @@ -664,12 +664,13 @@
   1.103  \textbf{nitpick} [\textit{show\_datatypes}] \\[2\smallskipamount]
   1.104  \slshape Nitpick found a counterexample: \\[2\smallskipamount]
   1.105  \hbox{}\qquad Free variables: \nopagebreak \\
   1.106 -\hbox{}\qquad\qquad $p = \lparr\textit{Xcoord} = 0,\> \textit{Ycoord} = 0\rparr$ \\
   1.107 -\hbox{}\qquad\qquad $q = \lparr\textit{Xcoord} = 1,\> \textit{Ycoord} = 1\rparr$ \\
   1.108 +\hbox{}\qquad\qquad $p = \lparr\textit{Xcoord} = 1,\> \textit{Ycoord} = 1\rparr$ \\
   1.109 +\hbox{}\qquad\qquad $q = \lparr\textit{Xcoord} = 0,\> \textit{Ycoord} = 0\rparr$ \\
   1.110  \hbox{}\qquad Datatypes: \\
   1.111  \hbox{}\qquad\qquad $\textit{int} = \{0,\, 1,\, \unr\}$ \\
   1.112 -\hbox{}\qquad\qquad $\textit{point} = \{\lparr\textit{Xcoord} = 1,\>
   1.113 -\textit{Ycoord} = 1\rparr,\> \lparr\textit{Xcoord} = 0,\> \textit{Ycoord} = 0\rparr,\, \unr\}$\kern-1pt %% QUIET
   1.114 +\hbox{}\qquad\qquad $\textit{point} = \{\!\begin{aligned}[t]
   1.115 +& \lparr\textit{Xcoord} = 0,\> \textit{Ycoord} = 0\rparr, \\[-2pt] %% TYPESETTING
   1.116 +& \lparr\textit{Xcoord} = 1,\> \textit{Ycoord} = 1\rparr,\, \unr\}\end{aligned}$
   1.117  \postw
   1.118  
   1.119  Finally, Nitpick provides rudimentary support for rationals and reals using a
   1.120 @@ -956,16 +957,16 @@
   1.121  depth}~= 1:
   1.122  \\[2\smallskipamount]
   1.123  \hbox{}\qquad Free variables: \nopagebreak \\
   1.124 -\hbox{}\qquad\qquad $\textit{a} = a_2$ \\
   1.125 -\hbox{}\qquad\qquad $\textit{b} = a_1$ \\
   1.126 -\hbox{}\qquad\qquad $\textit{xs} = \textsl{THE}~\omega.\; \omega = \textit{LCons}~a_2~\omega$ \\
   1.127 -\hbox{}\qquad\qquad $\textit{ys} = \textit{LCons}~a_1~(\textsl{THE}~\omega.\; \omega = \textit{LCons}~a_2~\omega)$ \\[2\smallskipamount]
   1.128 +\hbox{}\qquad\qquad $\textit{a} = a_1$ \\
   1.129 +\hbox{}\qquad\qquad $\textit{b} = a_2$ \\
   1.130 +\hbox{}\qquad\qquad $\textit{xs} = \textsl{THE}~\omega.\; \omega = \textit{LCons}~a_1~\omega$ \\
   1.131 +\hbox{}\qquad\qquad $\textit{ys} = \textit{LCons}~a_2~(\textsl{THE}~\omega.\; \omega = \textit{LCons}~a_1~\omega)$ \\[2\smallskipamount]
   1.132  Total time: 726 ms.
   1.133  \postw
   1.134  
   1.135 -The lazy list $\textit{xs}$ is simply $[a_2, a_2, a_2, \ldots]$, whereas
   1.136 -$\textit{ys}$ is $[a_1, a_2, a_2, a_2, \ldots]$, i.e., a lasso-shaped list with
   1.137 -$[a_1]$ as its stem and $[a_2]$ as its cycle. In general, the list segment
   1.138 +The lazy list $\textit{xs}$ is simply $[a_1, a_1, a_1, \ldots]$, whereas
   1.139 +$\textit{ys}$ is $[a_2, a_1, a_1, a_1, \ldots]$, i.e., a lasso-shaped list with
   1.140 +$[a_2]$ as its stem and $[a_1]$ as its cycle. In general, the list segment
   1.141  within the scope of the {THE} binder corresponds to the lasso's cycle, whereas
   1.142  the segment leading to the binder is the stem.
   1.143  
   1.144 @@ -1000,15 +1001,15 @@
   1.145  \textbf{nitpick} [\textit{bisim\_depth} = $-1$, \textit{show\_datatypes}] \\[2\smallskipamount]
   1.146  \slshape Nitpick found a likely genuine counterexample for $\textit{card}~'a$ = 2: \\[2\smallskipamount]
   1.147  \hbox{}\qquad Free variables: \nopagebreak \\
   1.148 -\hbox{}\qquad\qquad $a = a_2$ \\
   1.149 +\hbox{}\qquad\qquad $a = a_1$ \\
   1.150  \hbox{}\qquad\qquad $\textit{xs} = \textsl{THE}~\omega.\; \omega =
   1.151 -\textit{LCons}~a_2~\omega$ \\
   1.152 -\hbox{}\qquad\qquad $\textit{ys} = \textsl{THE}~\omega.\; \omega = \textit{LCons}~a_2~\omega$ \\
   1.153 +\textit{LCons}~a_1~\omega$ \\
   1.154 +\hbox{}\qquad\qquad $\textit{ys} = \textsl{THE}~\omega.\; \omega = \textit{LCons}~a_1~\omega$ \\
   1.155  \hbox{}\qquad Codatatype:\strut \nopagebreak \\
   1.156  \hbox{}\qquad\qquad $'a~\textit{llist} =
   1.157  \{\!\begin{aligned}[t]
   1.158 -  & \textsl{THE}~\omega.\; \omega = \textit{LCons}~a_2~\omega, \\[-2pt]
   1.159 -  & \textsl{THE}~\omega.\; \omega = \textit{LCons}~a_2~\omega,\> \unr\}\end{aligned}$
   1.160 +  & \textsl{THE}~\omega.\; \omega = \textit{LCons}~a_1~\omega, \\[-2pt]
   1.161 +  & \textsl{THE}~\omega.\; \omega = \textit{LCons}~a_1~\omega,\> \unr\}\end{aligned}$
   1.162  \\[2\smallskipamount]
   1.163  Try again with ``\textit{bisim\_depth}'' set to a nonnegative value to confirm
   1.164  that the counterexample is genuine. \\[2\smallskipamount]
   1.165 @@ -1198,8 +1199,8 @@
   1.166  \textit{card} ``\kern1pt$'b$ \textit{list}''~= 5:
   1.167  \\[2\smallskipamount]
   1.168  \hbox{}\qquad Free variables: \nopagebreak \\
   1.169 -\hbox{}\qquad\qquad $\textit{xs} = [a_4, a_5]$ \\
   1.170 -\hbox{}\qquad\qquad $\textit{ys} = [b_3, b_3]$ \\[2\smallskipamount]
   1.171 +\hbox{}\qquad\qquad $\textit{xs} = [a_1, a_2]$ \\
   1.172 +\hbox{}\qquad\qquad $\textit{ys} = [b_1, b_1]$ \\[2\smallskipamount]
   1.173  Total time: 1636 ms.
   1.174  \postw
   1.175  
   1.176 @@ -1377,21 +1378,21 @@
   1.177  \prew
   1.178  \slshape Nitpick found a nonstandard counterexample for \textit{card} $'a$ = 4: \\[2\smallskipamount]
   1.179  \hbox{}\qquad Free variables: \nopagebreak \\
   1.180 -\hbox{}\qquad\qquad $a = a_4$ \\
   1.181 -\hbox{}\qquad\qquad $b = a_3$ \\
   1.182 -\hbox{}\qquad\qquad $t = \xi_3$ \\
   1.183 -\hbox{}\qquad\qquad $u = \xi_4$ \\
   1.184 +\hbox{}\qquad\qquad $a = a_1$ \\
   1.185 +\hbox{}\qquad\qquad $b = a_2$ \\
   1.186 +\hbox{}\qquad\qquad $t = \xi_1$ \\
   1.187 +\hbox{}\qquad\qquad $u = \xi_2$ \\
   1.188  \hbox{}\qquad {\slshape Constants:} \nopagebreak \\
   1.189  \hbox{}\qquad\qquad $\textit{labels} = \undef
   1.190      (\!\begin{aligned}[t]%
   1.191 -    & \xi_3 := \{a_4\},\> \xi_4 := \{a_1, a_3\}, \\[-2pt] %% TYPESETTING
   1.192 -    & \textit{Branch}~\xi_3~\xi_3 := \{a_4\}, \\[-2pt]
   1.193 -    & \textit{Branch}~\xi_3~\xi_4 := \{a_1, a_3, a_4\})\end{aligned}$ \\
   1.194 +    & \xi_1 := \{a_1, a_4, a_3^\Q\},\> \xi_2 := \{a_2, a_3^\Q\}, \\[-2pt] %% TYPESETTING
   1.195 +    & \textit{Branch}~\xi_1~\xi_2 := \{a_1, a_2, a_4, a_3^\Q\}, \\[-2pt]
   1.196 +    & \textit{Branch}~\xi_2~\xi_2 := \{a_2, a_3^\Q\})\end{aligned}$ \\
   1.197  \hbox{}\qquad\qquad $\lambda x_1.\> \textit{swap}~x_1~a~b = \undef
   1.198      (\!\begin{aligned}[t]%
   1.199 -    & \xi_3 := \xi_3,\> \xi_4 := \xi_3, \\[-2pt]
   1.200 -    & \textit{Branch}~\xi_3~\xi_3 := \textit{Branch}~\xi_3~\xi_3, \\[-2pt]
   1.201 -    & \textit{Branch}~\xi_4~\xi_3 := \textit{Branch}~\xi_3~\xi_3)\end{aligned}$ \\[2\smallskipamount]
   1.202 +    & \xi_1 := \xi_2,\> \xi_2 := \xi_2, \\[-2pt]
   1.203 +    & \textit{Branch}~\xi_1~\xi_2 := \textit{Branch}~\xi_2~\xi_2, \\[-2pt]
   1.204 +    & \textit{Branch}~\xi_2~\xi_2 := \textit{Branch}~\xi_2~\xi_2)\end{aligned}$ \\[2\smallskipamount]
   1.205  The existence of a nonstandard model suggests that the induction hypothesis is not general enough or perhaps
   1.206  even wrong. See the ``Inductive Properties'' section of the Nitpick manual for details (``\textit{isabelle doc nitpick}'').
   1.207  \postw
   1.208 @@ -1406,7 +1407,7 @@
   1.209  allowing unreachable states in the preceding example (by removing the ``$n \in
   1.210  \textit{reach\/}$'' assumption). In both cases, we effectively enlarge the
   1.211  set of objects over which the induction is performed while doing the step
   1.212 -so as to test the induction hypothesis's strength.}
   1.213 +in order to test the induction hypothesis's strength.}
   1.214  The new trees are so nonstandard that we know nothing about them, except what
   1.215  the induction hypothesis states and what can be proved about all trees without
   1.216  relying on induction or case distinction. The key observation is,
   1.217 @@ -1417,8 +1418,8 @@
   1.218  objects, and Nitpick won't find any nonstandard counterexample.}
   1.219  \end{quote}
   1.220  %
   1.221 -But here, Nitpick did find some nonstandard trees $t = \xi_3$
   1.222 -and $u = \xi_4$ such that $a \in \textit{labels}~t$, $b \notin
   1.223 +But here, Nitpick did find some nonstandard trees $t = \xi_1$
   1.224 +and $u = \xi_2$ such that $a \in \textit{labels}~t$, $b \notin
   1.225  \textit{labels}~t$, $a \notin \textit{labels}~u$, and $b \in \textit{labels}~u$.
   1.226  Because neither tree contains both $a$ and $b$, the induction hypothesis tells
   1.227  us nothing about the labels of $\textit{swap}~t~a~b$ and $\textit{swap}~u~a~b$,
   1.228 @@ -1441,7 +1442,7 @@
   1.229  \postw
   1.230  
   1.231  This time, Nitpick won't find any nonstandard counterexample, and we can perform
   1.232 -the induction step using \textbf{auto}.
   1.233 +the induction step using \textit{auto}.
   1.234  
   1.235  \section{Case Studies}
   1.236  \label{case-studies}
   1.237 @@ -1726,8 +1727,8 @@
   1.238  \textbf{nitpick} \\[2\smallskipamount]
   1.239  \slshape Nitpick found a counterexample for \textit{card} $'a$ = 4: \\[2\smallskipamount]
   1.240  \hbox{}\qquad Free variables: \nopagebreak \\
   1.241 -\hbox{}\qquad\qquad $t = N~a_3~1~\Lambda~\Lambda$ \\
   1.242 -\hbox{}\qquad\qquad $x = a_4$
   1.243 +\hbox{}\qquad\qquad $t = N~a_1~1~\Lambda~\Lambda$ \\
   1.244 +\hbox{}\qquad\qquad $x = a_2$
   1.245  \postw
   1.246  
   1.247  It's hard to see why this is a counterexample. To improve readability, we will
   1.248 @@ -2138,7 +2139,7 @@
   1.249  is implicitly set to 0 for automatic runs. If you set this option to a value
   1.250  greater than 1, you will need an incremental SAT solver: For efficiency, it is
   1.251  recommended to install the JNI version of MiniSat and set \textit{sat\_solver} =
   1.252 -\textit{MiniSatJNI}. Also be aware that many of the counterexamples may look
   1.253 +\textit{MiniSat\_JNI}. Also be aware that many of the counterexamples may look
   1.254  identical, unless the \textit{show\_all} (\S\ref{output-format}) option is
   1.255  enabled.
   1.256  
   1.257 @@ -2150,7 +2151,7 @@
   1.258  Specifies the maximum number of genuine counterexamples to display. If you set
   1.259  this option to a value greater than 1, you will need an incremental SAT solver:
   1.260  For efficiency, it is recommended to install the JNI version of MiniSat and set
   1.261 -\textit{sat\_solver} = \textit{MiniSatJNI}. Also be aware that many of the
   1.262 +\textit{sat\_solver} = \textit{MiniSat\_JNI}. Also be aware that many of the
   1.263  counterexamples may look identical, unless the \textit{show\_all}
   1.264  (\S\ref{output-format}) option is enabled.
   1.265  
   1.266 @@ -2243,7 +2244,7 @@
   1.267  to be faster than their Java counterparts, but they can be more difficult to
   1.268  install. Also, if you set the \textit{max\_potential} (\S\ref{output-format}) or
   1.269  \textit{max\_genuine} (\S\ref{output-format}) option to a value greater than 1,
   1.270 -you will need an incremental SAT solver, such as \textit{MiniSatJNI}
   1.271 +you will need an incremental SAT solver, such as \textit{MiniSat\_JNI}
   1.272  (recommended) or \textit{SAT4J}.
   1.273  
   1.274  The supported solvers are listed below:
   1.275 @@ -2257,7 +2258,7 @@
   1.276  \url{http://minisat.se/MiniSat.html}. Nitpick has been tested with versions 1.14
   1.277  and 2.0 beta (2007-07-21).
   1.278  
   1.279 -\item[$\bullet$] \textbf{\textit{MiniSatJNI}}: The JNI (Java Native Interface)
   1.280 +\item[$\bullet$] \textbf{\textit{MiniSat\_JNI}}: The JNI (Java Native Interface)
   1.281  version of MiniSat is bundled in \texttt{nativesolver.\allowbreak tgz}, which
   1.282  you will find on Kodkod's web site \cite{kodkod-2009}. Unlike the standard
   1.283  version of MiniSat, the JNI version can be used incrementally.
   1.284 @@ -2279,7 +2280,7 @@
   1.285  \url{http://www.princeton.edu/~chaff/zchaff.html}. Nitpick has been tested with
   1.286  versions 2004-05-13, 2004-11-15, and 2007-03-12.
   1.287  
   1.288 -\item[$\bullet$] \textbf{\textit{zChaffJNI}}: The JNI version of zChaff is
   1.289 +\item[$\bullet$] \textbf{\textit{zChaff\_JNI}}: The JNI version of zChaff is
   1.290  bundled in \texttt{native\-solver.\allowbreak tgz}, which you will find on
   1.291  Kodkod's web site \cite{kodkod-2009}.
   1.292  
   1.293 @@ -2295,7 +2296,7 @@
   1.294  executable. The BerkMin executables are available at
   1.295  \url{http://eigold.tripod.com/BerkMin.html}.
   1.296  
   1.297 -\item[$\bullet$] \textbf{\textit{BerkMinAlloy}}: Variant of BerkMin that is
   1.298 +\item[$\bullet$] \textbf{\textit{BerkMin\_Alloy}}: Variant of BerkMin that is
   1.299  included with Alloy 4 and calls itself ``sat56'' in its banner text. To use this
   1.300  version of BerkMin, set the environment variable
   1.301  \texttt{BERKMINALLOY\_HOME} to the directory that contains the \texttt{berkmin}
   1.302 @@ -2313,7 +2314,7 @@
   1.303  install the official SAT4J packages, because their API is incompatible with
   1.304  Kodkod.
   1.305  
   1.306 -\item[$\bullet$] \textbf{\textit{SAT4JLight}}: Variant of SAT4J that is
   1.307 +\item[$\bullet$] \textbf{\textit{SAT4J\_Light}}: Variant of SAT4J that is
   1.308  optimized for small problems. It can also be used incrementally.
   1.309  
   1.310  \item[$\bullet$] \textbf{\textit{HaifaSat}}: HaifaSat 1.0 beta is an
   1.311 @@ -2324,7 +2325,7 @@
   1.312  
   1.313  \item[$\bullet$] \textbf{\textit{smart}}: If \textit{sat\_solver} is set to
   1.314  \textit{smart}, Nitpick selects the first solver among MiniSat,
   1.315 -PicoSAT, zChaff, RSat, BerkMin, BerkMinAlloy, Jerusat, MiniSatJNI, and zChaffJNI
   1.316 +PicoSAT, zChaff, RSat, BerkMin, BerkMin\_Alloy, Jerusat, MiniSat\_JNI, and zChaff\_JNI
   1.317  that is recognized by Isabelle. If none is found, it falls back on SAT4J, which
   1.318  should always be available. If \textit{verbose} (\S\ref{output-format}) is
   1.319  enabled, Nitpick displays which SAT solver was chosen.

     2.1 --- a/doc-src/manual.bib	Tue Feb 09 16:05:49 2010 +0100
     2.2 +++ b/doc-src/manual.bib	Tue Feb 09 16:07:51 2010 +0100
     2.3 @@ -3,7 +3,7 @@
     2.4  %publishers
     2.5  @string{AP="Academic Press"}
     2.6  @string{CUP="Cambridge University Press"}
     2.7 -@string{IEEE="{\sc ieee} Computer Society Press"}
     2.8 +@string{IEEE="IEEE Computer Society Press"}
     2.9  @string{LNCS="Lecture Notes in Computer Science"}
    2.10  @string{MIT="MIT Press"}
    2.11  @string{NH="North-Holland"}

     3.1 --- a/src/HOL/Nitpick_Examples/Core_Nits.thy	Tue Feb 09 16:05:49 2010 +0100
     3.2 +++ b/src/HOL/Nitpick_Examples/Core_Nits.thy	Tue Feb 09 16:07:51 2010 +0100
     3.3 @@ -11,7 +11,7 @@
     3.4  imports Main
     3.5  begin
     3.6  
     3.7 -nitpick_params [sat_solver = MiniSatJNI, max_threads = 1, timeout = 60 s]
     3.8 +nitpick_params [sat_solver = MiniSat_JNI, max_threads = 1, timeout = 60 s]
     3.9  
    3.10  subsection {* Curry in a Hurry *}
    3.11  

     4.1 --- a/src/HOL/Nitpick_Examples/Datatype_Nits.thy	Tue Feb 09 16:05:49 2010 +0100
     4.2 +++ b/src/HOL/Nitpick_Examples/Datatype_Nits.thy	Tue Feb 09 16:07:51 2010 +0100
     4.3 @@ -11,7 +11,7 @@
     4.4  imports Main
     4.5  begin
     4.6  
     4.7 -nitpick_params [sat_solver = MiniSatJNI, max_threads = 1, timeout = 60 s]
     4.8 +nitpick_params [sat_solver = MiniSat_JNI, max_threads = 1, timeout = 60 s]
     4.9  
    4.10  primrec rot where
    4.11  "rot Nibble0 = Nibble1" | "rot Nibble1 = Nibble2" | "rot Nibble2 = Nibble3" |

     5.1 --- a/src/HOL/Nitpick_Examples/Hotel_Nits.thy	Tue Feb 09 16:05:49 2010 +0100
     5.2 +++ b/src/HOL/Nitpick_Examples/Hotel_Nits.thy	Tue Feb 09 16:07:51 2010 +0100
     5.3 @@ -12,7 +12,7 @@
     5.4  imports Main
     5.5  begin
     5.6  
     5.7 -nitpick_params [sat_solver = MiniSatJNI, max_threads = 1, timeout = 120 s]
     5.8 +nitpick_params [sat_solver = MiniSat_JNI, max_threads = 1, timeout = 120 s]
     5.9  
    5.10  typedecl guest
    5.11  typedecl key

     6.1 --- a/src/HOL/Nitpick_Examples/Induct_Nits.thy	Tue Feb 09 16:05:49 2010 +0100
     6.2 +++ b/src/HOL/Nitpick_Examples/Induct_Nits.thy	Tue Feb 09 16:07:51 2010 +0100
     6.3 @@ -11,7 +11,7 @@
     6.4  imports Main
     6.5  begin
     6.6  
     6.7 -nitpick_params [sat_solver = MiniSatJNI, max_threads = 1, timeout = 60 s]
     6.8 +nitpick_params [sat_solver = MiniSat_JNI, max_threads = 1, timeout = 60 s]
     6.9  
    6.10  inductive p1 :: "nat \<Rightarrow> bool" where
    6.11  "p1 0" |

     7.1 --- a/src/HOL/Nitpick_Examples/Integer_Nits.thy	Tue Feb 09 16:05:49 2010 +0100
     7.2 +++ b/src/HOL/Nitpick_Examples/Integer_Nits.thy	Tue Feb 09 16:07:51 2010 +0100
     7.3 @@ -11,7 +11,7 @@
     7.4  imports Nitpick
     7.5  begin
     7.6  
     7.7 -nitpick_params [sat_solver = MiniSatJNI, max_threads = 1, timeout = 60 s,
     7.8 +nitpick_params [sat_solver = MiniSat_JNI, max_threads = 1, timeout = 60 s,
     7.9                  card = 1\<midarrow>6, bits = 1,2,3,4,6,8]
    7.10  
    7.11  lemma "Suc x = x + 1"

     8.1 --- a/src/HOL/Nitpick_Examples/Manual_Nits.thy	Tue Feb 09 16:05:49 2010 +0100
     8.2 +++ b/src/HOL/Nitpick_Examples/Manual_Nits.thy	Tue Feb 09 16:07:51 2010 +0100
     8.3 @@ -13,7 +13,7 @@
     8.4  
     8.5  chapter {* 3. First Steps *}
     8.6  
     8.7 -nitpick_params [sat_solver = MiniSatJNI, max_threads = 1]
     8.8 +nitpick_params [sat_solver = MiniSat_JNI, max_threads = 1]
     8.9  
    8.10  subsection {* 3.1. Propositional Logic *}
    8.11  

     9.1 --- a/src/HOL/Nitpick_Examples/Pattern_Nits.thy	Tue Feb 09 16:05:49 2010 +0100
     9.2 +++ b/src/HOL/Nitpick_Examples/Pattern_Nits.thy	Tue Feb 09 16:07:51 2010 +0100
     9.3 @@ -11,7 +11,7 @@
     9.4  imports Main
     9.5  begin
     9.6  
     9.7 -nitpick_params [sat_solver = MiniSatJNI, max_threads = 1, timeout = 60 s,
     9.8 +nitpick_params [sat_solver = MiniSat_JNI, max_threads = 1, timeout = 60 s,
     9.9                  card = 14]
    9.10  
    9.11  lemma "x = (case u of () \<Rightarrow> y)"

    10.1 --- a/src/HOL/Nitpick_Examples/Record_Nits.thy	Tue Feb 09 16:05:49 2010 +0100
    10.2 +++ b/src/HOL/Nitpick_Examples/Record_Nits.thy	Tue Feb 09 16:07:51 2010 +0100
    10.3 @@ -11,7 +11,7 @@
    10.4  imports Main
    10.5  begin
    10.6  
    10.7 -nitpick_params [sat_solver = MiniSatJNI, max_threads = 1, timeout = 60 s]
    10.8 +nitpick_params [sat_solver = MiniSat_JNI, max_threads = 1, timeout = 60 s]
    10.9  
   10.10  record point2d =
   10.11    xc :: int

    11.1 --- a/src/HOL/Nitpick_Examples/Refute_Nits.thy	Tue Feb 09 16:05:49 2010 +0100
    11.2 +++ b/src/HOL/Nitpick_Examples/Refute_Nits.thy	Tue Feb 09 16:07:51 2010 +0100
    11.3 @@ -11,7 +11,7 @@
    11.4  imports Main
    11.5  begin
    11.6  
    11.7 -nitpick_params [sat_solver = MiniSatJNI, max_threads = 1, timeout = 60 s]
    11.8 +nitpick_params [sat_solver = MiniSat_JNI, max_threads = 1, timeout = 60 s]
    11.9  
   11.10  lemma "P \<and> Q"
   11.11  apply (rule conjI)

    12.1 --- a/src/HOL/Nitpick_Examples/Special_Nits.thy	Tue Feb 09 16:05:49 2010 +0100
    12.2 +++ b/src/HOL/Nitpick_Examples/Special_Nits.thy	Tue Feb 09 16:07:51 2010 +0100
    12.3 @@ -11,7 +11,7 @@
    12.4  imports Main
    12.5  begin
    12.6  
    12.7 -nitpick_params [sat_solver = MiniSatJNI, max_threads = 1, timeout = 60 s,
    12.8 +nitpick_params [sat_solver = MiniSat_JNI, max_threads = 1, timeout = 60 s,
    12.9                  card = 4]
   12.10  
   12.11  fun f1 :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat" where

    13.1 --- a/src/HOL/Nitpick_Examples/Typedef_Nits.thy	Tue Feb 09 16:05:49 2010 +0100
    13.2 +++ b/src/HOL/Nitpick_Examples/Typedef_Nits.thy	Tue Feb 09 16:07:51 2010 +0100
    13.3 @@ -11,7 +11,8 @@
    13.4  imports Main Rational
    13.5  begin
    13.6  
    13.7 -nitpick_params [card = 1\<midarrow>4, timeout = 30 s]
    13.8 +nitpick_params [sat_solver = MiniSat_JNI, max_threads = 1, timeout = 60 s,
    13.9 +                card = 1\<midarrow>4]
   13.10  
   13.11  typedef three = "{0\<Colon>nat, 1, 2}"
   13.12  by blast

    14.1 --- a/src/HOL/Tools/Nitpick/HISTORY	Tue Feb 09 16:05:49 2010 +0100
    14.2 +++ b/src/HOL/Tools/Nitpick/HISTORY	Tue Feb 09 16:07:51 2010 +0100
    14.3 @@ -4,6 +4,8 @@
    14.4    * Added "std" option and implemented support for nonstandard models
    14.5    * Fixed soundness bugs related to "destroy_constrs" optimization and record
    14.6      getters
    14.7 +  * Renamed "MiniSatJNI", "zChaffJNI", "BerkMinAlloy", and "SAT4JLight" to
    14.8 + 	"MiniSat_JNI", "zChaff_JNI", "BerkMin_Alloy", and "SAT4J_Light"
    14.9  
   14.10  Version 2009-1
   14.11  

    15.1 --- a/src/HOL/Tools/Nitpick/kodkod_sat.ML	Tue Feb 09 16:05:49 2010 +0100
    15.2 +++ b/src/HOL/Tools/Nitpick/kodkod_sat.ML	Tue Feb 09 16:07:51 2010 +0100
    15.3 @@ -42,12 +42,12 @@
    15.4                             if berkmin_exec = "" then "BerkMin561"
    15.5                             else berkmin_exec, [], "Satisfiable          !!",
    15.6                             "solution =", "UNSATISFIABLE          !!")),
    15.7 -   ("BerkMinAlloy", External (ToStdout, "BERKMINALLOY_HOME", "berkmin", [])),
    15.8 +   ("BerkMin_Alloy", External (ToStdout, "BERKMINALLOY_HOME", "berkmin", [])),
    15.9     ("Jerusat", External (ToStdout, "JERUSAT_HOME", "Jerusat1.3", [])),
   15.10 -   ("MiniSatJNI", Internal (JNI, Incremental, ["MiniSat"])),
   15.11 -   ("zChaffJNI", Internal (JNI, Batch, ["zChaff"])),
   15.12 +   ("MiniSat_JNI", Internal (JNI, Incremental, ["MiniSat"])),
   15.13 +   ("zChaff_JNI", Internal (JNI, Batch, ["zChaff"])),
   15.14     ("SAT4J", Internal (Java, Incremental, ["DefaultSAT4J"])),
   15.15 -   ("SAT4JLight", Internal (Java, Incremental, ["LightSAT4J"])),
   15.16 +   ("SAT4J_Light", Internal (Java, Incremental, ["LightSAT4J"])),
   15.17     ("HaifaSat", ExternalV2 (ToStdout, "HAIFASAT_HOME", "HaifaSat", ["-p", "1"],
   15.18                              "s SATISFIABLE", "v ", "s UNSATISFIABLE"))]
   15.19  

    16.1 --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Tue Feb 09 16:05:49 2010 +0100
    16.2 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Tue Feb 09 16:07:51 2010 +0100
    16.3 @@ -122,6 +122,7 @@
    16.4    val nth_sel_for_constr : styp -> int -> styp
    16.5    val boxed_nth_sel_for_constr : hol_context -> styp -> int -> styp
    16.6    val sel_no_from_name : string -> int
    16.7 +  val close_form : term -> term
    16.8    val eta_expand : typ list -> term -> int -> term
    16.9    val extensionalize : term -> term
   16.10    val distinctness_formula : typ -> term list -> term
   16.11 @@ -782,6 +783,22 @@
   16.12    else
   16.13      0
   16.14  
   16.15 +(* term -> term *)
   16.16 +val close_form =
   16.17 +  let
   16.18 +    (* (indexname * typ) list -> (indexname * typ) list -> term -> term *)
   16.19 +    fun close_up zs zs' =
   16.20 +      fold (fn (z as ((s, _), T)) => fn t' =>
   16.21 +               Term.all T $ Abs (s, T, abstract_over (Var z, t')))
   16.22 +           (take (length zs' - length zs) zs')
   16.23 +    (* (indexname * typ) list -> term -> term *)
   16.24 +    fun aux zs (@{const "==>"} $ t1 $ t2) =
   16.25 +        let val zs' = Term.add_vars t1 zs in
   16.26 +          close_up zs zs' (Logic.mk_implies (t1, aux zs' t2))
   16.27 +        end
   16.28 +      | aux zs t = close_up zs (Term.add_vars t zs) t
   16.29 +  in aux [] end
   16.30 +
   16.31  (* typ list -> term -> int -> term *)
   16.32  fun eta_expand _ t 0 = t
   16.33    | eta_expand Ts (Abs (s, T, t')) n =

    17.1 --- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Tue Feb 09 16:05:49 2010 +0100
    17.2 +++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Tue Feb 09 16:07:51 2010 +0100
    17.3 @@ -317,7 +317,7 @@
    17.4               [ts] |> not exclusive ? cons (KK.TupleSet [])
    17.5             else
    17.6               [KK.TupleSet [],
    17.7 -              if exclusive andalso T1 = T2 andalso epsilon > delta then
    17.8 +              if (* ### exclusive andalso*) T1 = T2 andalso epsilon > delta then
    17.9                  index_seq delta (epsilon - delta)
   17.10                  |> map (fn j =>
   17.11                             KK.TupleProduct (KK.TupleSet [Kodkod.Tuple [j + j0]],

    18.1 --- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Tue Feb 09 16:05:49 2010 +0100
    18.2 +++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Tue Feb 09 16:07:51 2010 +0100
    18.3 @@ -943,7 +943,7 @@
    18.4                              |> map Logic.mk_equals,
    18.5                          Logic.mk_equals (list_comb (Const x1, bounds1 @ args1),
    18.6                                           list_comb (Const x2, bounds2 @ args2)))
    18.7 -    |> Refute.close_form (* TODO: needed? *)
    18.8 +    |> close_form (* TODO: needed? *)
    18.9    end
   18.10  
   18.11  (* hol_context -> styp list -> term list *)
   18.12 @@ -1391,7 +1391,7 @@
   18.13      val skolem_depth = if skolemize then 4 else ~1
   18.14      val (((def_ts, nondef_ts), (got_all_mono_user_axioms, no_poly_user_axioms)),
   18.15           core_t) = t |> unfold_defs_in_term hol_ctxt
   18.16 -                     |> Refute.close_form
   18.17 +                     |> close_form
   18.18                       |> skolemize_term_and_more hol_ctxt skolem_depth
   18.19                       |> specialize_consts_in_term hol_ctxt 0
   18.20                       |> `(axioms_for_term hol_ctxt)
   18.21 @@ -1420,7 +1420,7 @@
   18.22        #> simplify_constrs_and_sels thy
   18.23        #> distribute_quantifiers
   18.24        #> push_quantifiers_inward thy
   18.25 -      #> not core ? Refute.close_form
   18.26 +      #> close_form
   18.27        #> Term.map_abs_vars shortest_name
   18.28    in
   18.29      (((map (do_rest true false) def_ts, map (do_rest false false) nondef_ts),