doc-src/Nitpick/nitpick.tex
author blanchet
Fri May 14 22:43:00 2010 +0200 (2010-05-14)
changeset 36926 90bb12cf8e36
parent 36390 eee4ee6a5cbe
child 37169 f69efa106feb
permissions -rw-r--r--
added Sledgehammer manual;
some material was recovered from the Isar material, the rest is new
     1 \documentclass[a4paper,12pt]{article}
     2 \usepackage[T1]{fontenc}
     3 \usepackage{amsmath}
     4 \usepackage{amssymb}
     5 \usepackage[english,french]{babel}
     6 \usepackage{color}
     7 \usepackage{footmisc}
     8 \usepackage{graphicx}
     9 %\usepackage{mathpazo}
    10 \usepackage{multicol}
    11 \usepackage{stmaryrd}
    12 %\usepackage[scaled=.85]{beramono}
    13 \usepackage{../iman,../pdfsetup}
    14 
    15 %\oddsidemargin=4.6mm
    16 %\evensidemargin=4.6mm
    17 %\textwidth=150mm
    18 %\topmargin=4.6mm
    19 %\headheight=0mm
    20 %\headsep=0mm
    21 %\textheight=234mm
    22 
    23 \def\Colon{\mathord{:\mkern-1.5mu:}}
    24 %\def\lbrakk{\mathopen{\lbrack\mkern-3.25mu\lbrack}}
    25 %\def\rbrakk{\mathclose{\rbrack\mkern-3.255mu\rbrack}}
    26 \def\lparr{\mathopen{(\mkern-4mu\mid}}
    27 \def\rparr{\mathclose{\mid\mkern-4mu)}}
    28 
    29 \def\unk{{?}}
    30 \def\undef{(\lambda x.\; \unk)}
    31 %\def\unr{\textit{others}}
    32 \def\unr{\ldots}
    33 \def\Abs#1{\hbox{\rm{\flqq}}{\,#1\,}\hbox{\rm{\frqq}}}
    34 \def\Q{{\smash{\lower.2ex\hbox{$\scriptstyle?$}}}}
    35 
    36 \hyphenation{Mini-Sat size-change First-Steps grand-parent nit-pick
    37 counter-example counter-examples data-type data-types co-data-type 
    38 co-data-types in-duc-tive co-in-duc-tive}
    39 
    40 \urlstyle{tt}
    41 
    42 \begin{document}
    43 
    44 \selectlanguage{english}
    45 
    46 \title{\includegraphics[scale=0.5]{isabelle_nitpick} \\[4ex]
    47 Picking Nits \\[\smallskipamount]
    48 \Large A User's Guide to Nitpick for Isabelle/HOL}
    49 \author{\hbox{} \\
    50 Jasmin Christian Blanchette \\
    51 {\normalsize Institut f\"ur Informatik, Technische Universit\"at M\"unchen} \\
    52 \hbox{}}
    53 
    54 \maketitle
    55 
    56 \tableofcontents
    57 
    58 \setlength{\parskip}{.7em plus .2em minus .1em}
    59 \setlength{\parindent}{0pt}
    60 \setlength{\abovedisplayskip}{\parskip}
    61 \setlength{\abovedisplayshortskip}{.9\parskip}
    62 \setlength{\belowdisplayskip}{\parskip}
    63 \setlength{\belowdisplayshortskip}{.9\parskip}
    64 
    65 % General-purpose enum environment with correct spacing
    66 \newenvironment{enum}%
    67     {\begin{list}{}{%
    68         \setlength{\topsep}{.1\parskip}%
    69         \setlength{\partopsep}{.1\parskip}%
    70         \setlength{\itemsep}{\parskip}%
    71         \advance\itemsep by-\parsep}}
    72     {\end{list}}
    73 
    74 \def\pre{\begingroup\vskip0pt plus1ex\advance\leftskip by\leftmargin
    75 \advance\rightskip by\leftmargin}
    76 \def\post{\vskip0pt plus1ex\endgroup}
    77 
    78 \def\prew{\pre\advance\rightskip by-\leftmargin}
    79 \def\postw{\post}
    80 
    81 \section{Introduction}
    82 \label{introduction}
    83 
    84 Nitpick \cite{blanchette-nipkow-2010} is a counterexample generator for
    85 Isabelle/HOL \cite{isa-tutorial} that is designed to handle formulas
    86 combining (co)in\-duc\-tive datatypes, (co)in\-duc\-tively defined predicates, and
    87 quantifiers. It builds on Kodkod \cite{torlak-jackson-2007}, a highly optimized
    88 first-order relational model finder developed by the Software Design Group at
    89 MIT. It is conceptually similar to Refute \cite{weber-2008}, from which it
    90 borrows many ideas and code fragments, but it benefits from Kodkod's
    91 optimizations and a new encoding scheme. The name Nitpick is shamelessly
    92 appropriated from a now retired Alloy precursor.
    93 
    94 Nitpick is easy to use---you simply enter \textbf{nitpick} after a putative
    95 theorem and wait a few seconds. Nonetheless, there are situations where knowing
    96 how it works under the hood and how it reacts to various options helps
    97 increase the test coverage. This manual also explains how to install the tool on
    98 your workstation. Should the motivation fail you, think of the many hours of
    99 hard work Nitpick will save you. Proving non-theorems is \textsl{hard work}.
   100 
   101 Another common use of Nitpick is to find out whether the axioms of a locale are
   102 satisfiable, while the locale is being developed. To check this, it suffices to
   103 write
   104 
   105 \prew
   106 \textbf{lemma}~``$\textit{False}$'' \\
   107 \textbf{nitpick}~[\textit{show\_all}]
   108 \postw
   109 
   110 after the locale's \textbf{begin} keyword. To falsify \textit{False}, Nitpick
   111 must find a model for the axioms. If it finds no model, we have an indication
   112 that the axioms might be unsatisfiable.
   113 
   114 You can also invoke Nitpick from the ``Commands'' submenu of the
   115 ``Isabelle'' menu in Proof General or by pressing the Emacs key sequence C-c C-a
   116 C-n. This is equivalent to entering the \textbf{nitpick} command with no
   117 arguments in the theory text.
   118 
   119 Nitpick requires the Kodkodi package for Isabelle as well as a Java 1.5 virtual
   120 machine called \texttt{java}. The examples presented in this manual can be found
   121 in Isabelle's \texttt{src/HOL/Nitpick\_Examples/Manual\_Nits.thy} theory.
   122 
   123 Throughout this manual, we will explicitly invoke the \textbf{nitpick} command.
   124 Nitpick also provides an automatic mode that can be enabled using the
   125 ``Auto Nitpick'' option from the ``Isabelle'' menu in Proof General. In this
   126 mode, Nitpick is run on every newly entered theorem, much like Auto Quickcheck.
   127 The collective time limit for Auto Nitpick and Auto Quickcheck can be set using
   128 the ``Auto Counterexample Time Limit'' option.
   129 
   130 \newbox\boxA
   131 \setbox\boxA=\hbox{\texttt{nospam}}
   132 
   133 The known bugs and limitations at the time of writing are listed in
   134 \S\ref{known-bugs-and-limitations}. Comments and bug reports concerning Nitpick
   135 or this manual should be directed to
   136 \texttt{blan{\color{white}nospam}\kern-\wd\boxA{}chette@\allowbreak
   137 in.\allowbreak tum.\allowbreak de}.
   138 
   139 \vskip2.5\smallskipamount
   140 
   141 \textbf{Acknowledgment.} The author would like to thank Mark Summerfield for
   142 suggesting several textual improvements.
   143 % and Perry James for reporting a typo.
   144 
   145 %\section{Installation}
   146 %\label{installation}
   147 %
   148 %MISSING:
   149 %
   150 %  * Nitpick is part of Isabelle/HOL
   151 %  * but it relies on an external tool called Kodkodi (Kodkod wrapper)
   152 %  * Two options:
   153 %    * if you use a prebuilt Isabelle package, Kodkodi is automatically there
   154 %    * if you work from sources, the latest Kodkodi can be obtained from ...
   155 %      download it, install it in some directory of your choice (e.g.,
   156 %      $ISABELLE_HOME/contrib/kodkodi), and add the absolute path to Kodkodi
   157 %      in your .isabelle/etc/components file
   158 %
   159 %  * If you're not sure, just try the example in the next section
   160 
   161 \section{First Steps}
   162 \label{first-steps}
   163 
   164 This section introduces Nitpick by presenting small examples. If possible, you
   165 should try out the examples on your workstation. Your theory file should start
   166 as follows:
   167 
   168 \prew
   169 \textbf{theory}~\textit{Scratch} \\
   170 \textbf{imports}~\textit{Main~Quotient\_Product~RealDef} \\
   171 \textbf{begin}
   172 \postw
   173 
   174 The results presented here were obtained using the JNI (Java Native Interface)
   175 version of MiniSat and with multithreading disabled to reduce nondeterminism.
   176 This was done by adding the line
   177 
   178 \prew
   179 \textbf{nitpick\_params} [\textit{sat\_solver}~= \textit{MiniSat\_JNI}, \,\textit{max\_threads}~= 1]
   180 \postw
   181 
   182 after the \textbf{begin} keyword. The JNI version of MiniSat is bundled with
   183 Kodkodi and is precompiled for the major platforms. Other SAT solvers can also
   184 be installed, as explained in \S\ref{optimizations}. If you have already
   185 configured SAT solvers in Isabelle (e.g., for Refute), these will also be
   186 available to Nitpick.
   187 
   188 \subsection{Propositional Logic}
   189 \label{propositional-logic}
   190 
   191 Let's start with a trivial example from propositional logic:
   192 
   193 \prew
   194 \textbf{lemma}~``$P \longleftrightarrow Q$'' \\
   195 \textbf{nitpick}
   196 \postw
   197 
   198 You should get the following output:
   199 
   200 \prew
   201 \slshape
   202 Nitpick found a counterexample: \\[2\smallskipamount]
   203 \hbox{}\qquad Free variables: \nopagebreak \\
   204 \hbox{}\qquad\qquad $P = \textit{True}$ \\
   205 \hbox{}\qquad\qquad $Q = \textit{False}$
   206 \postw
   207 
   208 %FIXME: If you get the output:...
   209 %Then do such-and-such.
   210 
   211 Nitpick can also be invoked on individual subgoals, as in the example below:
   212 
   213 \prew
   214 \textbf{apply}~\textit{auto} \\[2\smallskipamount]
   215 {\slshape goal (2 subgoals): \\
   216 \phantom{0}1. $P\,\Longrightarrow\, Q$ \\
   217 \phantom{0}2. $Q\,\Longrightarrow\, P$} \\[2\smallskipamount]
   218 \textbf{nitpick}~1 \\[2\smallskipamount]
   219 {\slshape Nitpick found a counterexample: \\[2\smallskipamount]
   220 \hbox{}\qquad Free variables: \nopagebreak \\
   221 \hbox{}\qquad\qquad $P = \textit{True}$ \\
   222 \hbox{}\qquad\qquad $Q = \textit{False}$} \\[2\smallskipamount]
   223 \textbf{nitpick}~2 \\[2\smallskipamount]
   224 {\slshape Nitpick found a counterexample: \\[2\smallskipamount]
   225 \hbox{}\qquad Free variables: \nopagebreak \\
   226 \hbox{}\qquad\qquad $P = \textit{False}$ \\
   227 \hbox{}\qquad\qquad $Q = \textit{True}$} \\[2\smallskipamount]
   228 \textbf{oops}
   229 \postw
   230 
   231 \subsection{Type Variables}
   232 \label{type-variables}
   233 
   234 If you are left unimpressed by the previous example, don't worry. The next
   235 one is more mind- and computer-boggling:
   236 
   237 \prew
   238 \textbf{lemma} ``$P~x\,\Longrightarrow\, P~(\textrm{THE}~y.\;P~y)$''
   239 \postw
   240 \pagebreak[2] %% TYPESETTING
   241 
   242 The putative lemma involves the definite description operator, {THE}, presented
   243 in section 5.10.1 of the Isabelle tutorial \cite{isa-tutorial}. The
   244 operator is defined by the axiom $(\textrm{THE}~x.\; x = a) = a$. The putative
   245 lemma is merely asserting the indefinite description operator axiom with {THE}
   246 substituted for {SOME}.
   247 
   248 The free variable $x$ and the bound variable $y$ have type $'a$. For formulas
   249 containing type variables, Nitpick enumerates the possible domains for each type
   250 variable, up to a given cardinality (8 by default), looking for a finite
   251 countermodel:
   252 
   253 \prew
   254 \textbf{nitpick} [\textit{verbose}] \\[2\smallskipamount]
   255 \slshape
   256 Trying 8 scopes: \nopagebreak \\
   257 \hbox{}\qquad \textit{card}~$'a$~= 1; \\
   258 \hbox{}\qquad \textit{card}~$'a$~= 2; \\
   259 \hbox{}\qquad $\qquad\vdots$ \\[.5\smallskipamount]
   260 \hbox{}\qquad \textit{card}~$'a$~= 8. \\[2\smallskipamount]
   261 Nitpick found a counterexample for \textit{card} $'a$~= 3: \\[2\smallskipamount]
   262 \hbox{}\qquad Free variables: \nopagebreak \\
   263 \hbox{}\qquad\qquad $P = \{a_2,\, a_3\}$ \\
   264 \hbox{}\qquad\qquad $x = a_3$ \\[2\smallskipamount]
   265 Total time: 580 ms.
   266 \postw
   267 
   268 Nitpick found a counterexample in which $'a$ has cardinality 3. (For
   269 cardinalities 1 and 2, the formula holds.) In the counterexample, the three
   270 values of type $'a$ are written $a_1$, $a_2$, and $a_3$.
   271 
   272 The message ``Trying $n$ scopes: {\ldots}''\ is shown only if the option
   273 \textit{verbose} is enabled. You can specify \textit{verbose} each time you
   274 invoke \textbf{nitpick}, or you can set it globally using the command
   275 
   276 \prew
   277 \textbf{nitpick\_params} [\textit{verbose}]
   278 \postw
   279 
   280 This command also displays the current default values for all of the options
   281 supported by Nitpick. The options are listed in \S\ref{option-reference}.
   282 
   283 \subsection{Constants}
   284 \label{constants}
   285 
   286 By just looking at Nitpick's output, it might not be clear why the
   287 counterexample in \S\ref{type-variables} is genuine. Let's invoke Nitpick again,
   288 this time telling it to show the values of the constants that occur in the
   289 formula:
   290 
   291 \prew
   292 \textbf{lemma}~``$P~x\,\Longrightarrow\, P~(\textrm{THE}~y.\;P~y)$'' \\
   293 \textbf{nitpick}~[\textit{show\_consts}] \\[2\smallskipamount]
   294 \slshape
   295 Nitpick found a counterexample for \textit{card} $'a$~= 3: \\[2\smallskipamount]
   296 \hbox{}\qquad Free variables: \nopagebreak \\
   297 \hbox{}\qquad\qquad $P = \{a_2,\, a_3\}$ \\
   298 \hbox{}\qquad\qquad $x = a_3$ \\
   299 \hbox{}\qquad Constant: \nopagebreak \\
   300 \hbox{}\qquad\qquad $\textit{The}~\textsl{fallback} = a_1$
   301 \postw
   302 
   303 We can see more clearly now. Since the predicate $P$ isn't true for a unique
   304 value, $\textrm{THE}~y.\;P~y$ can denote any value of type $'a$, even
   305 $a_1$. Since $P~a_1$ is false, the entire formula is falsified.
   306 
   307 As an optimization, Nitpick's preprocessor introduced the special constant
   308 ``\textit{The} fallback'' corresponding to $\textrm{THE}~y.\;P~y$ (i.e.,
   309 $\mathit{The}~(\lambda y.\;P~y)$) when there doesn't exist a unique $y$
   310 satisfying $P~y$. We disable this optimization by passing the
   311 \textit{full\_descrs} option:
   312 
   313 \prew
   314 \textbf{nitpick}~[\textit{full\_descrs},\, \textit{show\_consts}] \\[2\smallskipamount]
   315 \slshape
   316 Nitpick found a counterexample for \textit{card} $'a$~= 3: \\[2\smallskipamount]
   317 \hbox{}\qquad Free variables: \nopagebreak \\
   318 \hbox{}\qquad\qquad $P = \{a_2,\, a_3\}$ \\
   319 \hbox{}\qquad\qquad $x = a_3$ \\
   320 \hbox{}\qquad Constant: \nopagebreak \\
   321 \hbox{}\qquad\qquad $\hbox{\slshape THE}~y.\;P~y = a_1$
   322 \postw
   323 
   324 As the result of another optimization, Nitpick directly assigned a value to the
   325 subterm $\textrm{THE}~y.\;P~y$, rather than to the \textit{The} constant. If we
   326 disable this second optimization by using the command
   327 
   328 \prew
   329 \textbf{nitpick}~[\textit{dont\_specialize},\, \textit{full\_descrs},\,
   330 \textit{show\_consts}]
   331 \postw
   332 
   333 we finally get \textit{The}:
   334 
   335 \prew
   336 \slshape Constant: \nopagebreak \\
   337 \hbox{}\qquad $\mathit{The} = \undef{}
   338     (\!\begin{aligned}[t]%
   339     & \{a_1, a_2, a_3\} := a_3,\> \{a_1, a_2\} := a_3,\> \{a_1, a_3\} := a_3, \\[-2pt] %% TYPESETTING
   340     & \{a_1\} := a_1,\> \{a_2, a_3\} := a_1,\> \{a_2\} := a_2, \\[-2pt]
   341     & \{a_3\} := a_3,\> \{\} := a_3)\end{aligned}$
   342 \postw
   343 
   344 Notice that $\textit{The}~(\lambda y.\;P~y) = \textit{The}~\{a_2, a_3\} = a_1$,
   345 just like before.\footnote{The Isabelle/HOL notation $f(x :=
   346 y)$ denotes the function that maps $x$ to $y$ and that otherwise behaves like
   347 $f$.}
   348 
   349 Our misadventures with THE suggest adding `$\exists!x{.}$' (``there exists a
   350 unique $x$ such that'') at the front of our putative lemma's assumption:
   351 
   352 \prew
   353 \textbf{lemma}~``$\exists {!}x.\; P~x\,\Longrightarrow\, P~(\textrm{THE}~y.\;P~y)$''
   354 \postw
   355 
   356 The fix appears to work:
   357 
   358 \prew
   359 \textbf{nitpick} \\[2\smallskipamount]
   360 \slshape Nitpick found no counterexample.
   361 \postw
   362 
   363 We can further increase our confidence in the formula by exhausting all
   364 cardinalities up to 50:
   365 
   366 \prew
   367 \textbf{nitpick} [\textit{card} $'a$~= 1--50]\footnote{The symbol `--'
   368 can be entered as \texttt{-} (hyphen) or
   369 \texttt{\char`\\\char`\<midarrow\char`\>}.} \\[2\smallskipamount]
   370 \slshape Nitpick found no counterexample.
   371 \postw
   372 
   373 Let's see if Sledgehammer \cite{sledgehammer-2009} can find a proof:
   374 
   375 \prew
   376 \textbf{sledgehammer} \\[2\smallskipamount]
   377 {\slshape Sledgehammer: external prover ``$e$'' for subgoal 1: \\
   378 $\exists{!}x.\; P~x\,\Longrightarrow\, P~(\hbox{\slshape THE}~y.\; P~y)$ \\
   379 Try this command: \textrm{apply}~(\textit{metis~the\_equality})} \\[2\smallskipamount]
   380 \textbf{apply}~(\textit{metis~the\_equality\/}) \nopagebreak \\[2\smallskipamount]
   381 {\slshape No subgoals!}% \\[2\smallskipamount]
   382 %\textbf{done}
   383 \postw
   384 
   385 This must be our lucky day.
   386 
   387 \subsection{Skolemization}
   388 \label{skolemization}
   389 
   390 Are all invertible functions onto? Let's find out:
   391 
   392 \prew
   393 \textbf{lemma} ``$\exists g.\; \forall x.~g~(f~x) = x
   394  \,\Longrightarrow\, \forall y.\; \exists x.~y = f~x$'' \\
   395 \textbf{nitpick} \\[2\smallskipamount]
   396 \slshape
   397 Nitpick found a counterexample for \textit{card} $'a$~= 2 and \textit{card} $'b$~=~1: \\[2\smallskipamount]
   398 \hbox{}\qquad Free variable: \nopagebreak \\
   399 \hbox{}\qquad\qquad $f = \undef{}(b_1 := a_1)$ \\
   400 \hbox{}\qquad Skolem constants: \nopagebreak \\
   401 \hbox{}\qquad\qquad $g = \undef{}(a_1 := b_1,\> a_2 := b_1)$ \\
   402 \hbox{}\qquad\qquad $y = a_2$
   403 \postw
   404 
   405 Although $f$ is the only free variable occurring in the formula, Nitpick also
   406 displays values for the bound variables $g$ and $y$. These values are available
   407 to Nitpick because it performs skolemization as a preprocessing step.
   408 
   409 In the previous example, skolemization only affected the outermost quantifiers.
   410 This is not always the case, as illustrated below:
   411 
   412 \prew
   413 \textbf{lemma} ``$\exists x.\; \forall f.\; f~x = x$'' \\
   414 \textbf{nitpick} \\[2\smallskipamount]
   415 \slshape
   416 Nitpick found a counterexample for \textit{card} $'a$~= 2: \\[2\smallskipamount]
   417 \hbox{}\qquad Skolem constant: \nopagebreak \\
   418 \hbox{}\qquad\qquad $\lambda x.\; f =
   419     \undef{}(\!\begin{aligned}[t]
   420     & a_1 := \undef{}(a_1 := a_2,\> a_2 := a_1), \\[-2pt]
   421     & a_2 := \undef{}(a_1 := a_1,\> a_2 := a_1))\end{aligned}$
   422 \postw
   423 
   424 The variable $f$ is bound within the scope of $x$; therefore, $f$ depends on
   425 $x$, as suggested by the notation $\lambda x.\,f$. If $x = a_1$, then $f$ is the
   426 function that maps $a_1$ to $a_2$ and vice versa; otherwise, $x = a_2$ and $f$
   427 maps both $a_1$ and $a_2$ to $a_1$. In both cases, $f~x \not= x$.
   428 
   429 The source of the Skolem constants is sometimes more obscure:
   430 
   431 \prew
   432 \textbf{lemma} ``$\mathit{refl}~r\,\Longrightarrow\, \mathit{sym}~r$'' \\
   433 \textbf{nitpick} \\[2\smallskipamount]
   434 \slshape
   435 Nitpick found a counterexample for \textit{card} $'a$~= 2: \\[2\smallskipamount]
   436 \hbox{}\qquad Free variable: \nopagebreak \\
   437 \hbox{}\qquad\qquad $r = \{(a_1, a_1),\, (a_2, a_1),\, (a_2, a_2)\}$ \\
   438 \hbox{}\qquad Skolem constants: \nopagebreak \\
   439 \hbox{}\qquad\qquad $\mathit{sym}.x = a_2$ \\
   440 \hbox{}\qquad\qquad $\mathit{sym}.y = a_1$
   441 \postw
   442 
   443 What happened here is that Nitpick expanded the \textit{sym} constant to its
   444 definition:
   445 
   446 \prew
   447 $\mathit{sym}~r \,\equiv\,
   448  \forall x\> y.\,\> (x, y) \in r \longrightarrow (y, x) \in r.$
   449 \postw
   450 
   451 As their names suggest, the Skolem constants $\mathit{sym}.x$ and
   452 $\mathit{sym}.y$ are simply the bound variables $x$ and $y$
   453 from \textit{sym}'s definition.
   454 
   455 \subsection{Natural Numbers and Integers}
   456 \label{natural-numbers-and-integers}
   457 
   458 Because of the axiom of infinity, the type \textit{nat} does not admit any
   459 finite models. To deal with this, Nitpick's approach is to consider finite
   460 subsets $N$ of \textit{nat} and maps all numbers $\notin N$ to the undefined
   461 value (displayed as `$\unk$'). The type \textit{int} is handled similarly.
   462 Internally, undefined values lead to a three-valued logic.
   463 
   464 Here is an example involving \textit{int\/}:
   465 
   466 \prew
   467 \textbf{lemma} ``$\lbrakk i \le j;\> n \le (m{\Colon}\mathit{int})\rbrakk \,\Longrightarrow\, i * n + j * m \le i * m + j * n$'' \\
   468 \textbf{nitpick} \\[2\smallskipamount]
   469 \slshape Nitpick found a counterexample: \\[2\smallskipamount]
   470 \hbox{}\qquad Free variables: \nopagebreak \\
   471 \hbox{}\qquad\qquad $i = 0$ \\
   472 \hbox{}\qquad\qquad $j = 1$ \\
   473 \hbox{}\qquad\qquad $m = 1$ \\
   474 \hbox{}\qquad\qquad $n = 0$
   475 \postw
   476 
   477 Internally, Nitpick uses either a unary or a binary representation of numbers.
   478 The unary representation is more efficient but only suitable for numbers very
   479 close to zero. By default, Nitpick attempts to choose the more appropriate
   480 encoding by inspecting the formula at hand. This behavior can be overridden by
   481 passing either \textit{unary\_ints} or \textit{binary\_ints} as option. For
   482 binary notation, the number of bits to use can be specified using
   483 the \textit{bits} option. For example:
   484 
   485 \prew
   486 \textbf{nitpick} [\textit{binary\_ints}, \textit{bits}${} = 16$]
   487 \postw
   488 
   489 With infinite types, we don't always have the luxury of a genuine counterexample
   490 and must often content ourselves with a potential one. The tedious task of
   491 finding out whether the potential counterexample is in fact genuine can be
   492 outsourced to \textit{auto} by passing \textit{check\_potential}. For example:
   493 
   494 \prew
   495 \textbf{lemma} ``$\forall n.\; \textit{Suc}~n \mathbin{\not=} n \,\Longrightarrow\, P$'' \\
   496 \textbf{nitpick} [\textit{card~nat}~= 50, \textit{check\_potential}] \\[2\smallskipamount]
   497 \slshape Warning: The conjecture either trivially holds for the given scopes or lies outside Nitpick's supported
   498 fragment. Only potential counterexamples may be found. \\[2\smallskipamount]
   499 Nitpick found a potential counterexample: \\[2\smallskipamount]
   500 \hbox{}\qquad Free variable: \nopagebreak \\
   501 \hbox{}\qquad\qquad $P = \textit{False}$ \\[2\smallskipamount]
   502 Confirmation by ``\textit{auto}'': The above counterexample is genuine.
   503 \postw
   504 
   505 You might wonder why the counterexample is first reported as potential. The root
   506 of the problem is that the bound variable in $\forall n.\; \textit{Suc}~n
   507 \mathbin{\not=} n$ ranges over an infinite type. If Nitpick finds an $n$ such
   508 that $\textit{Suc}~n \mathbin{=} n$, it evaluates the assumption to
   509 \textit{False}; but otherwise, it does not know anything about values of $n \ge
   510 \textit{card~nat}$ and must therefore evaluate the assumption to $\unk$, not
   511 \textit{True}. Since the assumption can never be satisfied, the putative lemma
   512 can never be falsified.
   513 
   514 Incidentally, if you distrust the so-called genuine counterexamples, you can
   515 enable \textit{check\_\allowbreak genuine} to verify them as well. However, be
   516 aware that \textit{auto} will usually fail to prove that the counterexample is
   517 genuine or spurious.
   518 
   519 Some conjectures involving elementary number theory make Nitpick look like a
   520 giant with feet of clay:
   521 
   522 \prew
   523 \textbf{lemma} ``$P~\textit{Suc}$'' \\
   524 \textbf{nitpick} \\[2\smallskipamount]
   525 \slshape
   526 Nitpick found no counterexample.
   527 \postw
   528 
   529 On any finite set $N$, \textit{Suc} is a partial function; for example, if $N =
   530 \{0, 1, \ldots, k\}$, then \textit{Suc} is $\{0 \mapsto 1,\, 1 \mapsto 2,\,
   531 \ldots,\, k \mapsto \unk\}$, which evaluates to $\unk$ when passed as
   532 argument to $P$. As a result, $P~\textit{Suc}$ is always $\unk$. The next
   533 example is similar:
   534 
   535 \prew
   536 \textbf{lemma} ``$P~(\textit{op}~{+}\Colon
   537 \textit{nat}\mathbin{\Rightarrow}\textit{nat}\mathbin{\Rightarrow}\textit{nat})$'' \\
   538 \textbf{nitpick} [\textit{card nat} = 1] \\[2\smallskipamount]
   539 {\slshape Nitpick found a counterexample:} \\[2\smallskipamount]
   540 \hbox{}\qquad Free variable: \nopagebreak \\
   541 \hbox{}\qquad\qquad $P = \{\}$ \\[2\smallskipamount]
   542 \textbf{nitpick} [\textit{card nat} = 2] \\[2\smallskipamount]
   543 {\slshape Nitpick found no counterexample.}
   544 \postw
   545 
   546 The problem here is that \textit{op}~+ is total when \textit{nat} is taken to be
   547 $\{0\}$ but becomes partial as soon as we add $1$, because $1 + 1 \notin \{0,
   548 1\}$.
   549 
   550 Because numbers are infinite and are approximated using a three-valued logic,
   551 there is usually no need to systematically enumerate domain sizes. If Nitpick
   552 cannot find a genuine counterexample for \textit{card~nat}~= $k$, it is very
   553 unlikely that one could be found for smaller domains. (The $P~(\textit{op}~{+})$
   554 example above is an exception to this principle.) Nitpick nonetheless enumerates
   555 all cardinalities from 1 to 8 for \textit{nat}, mainly because smaller
   556 cardinalities are fast to handle and give rise to simpler counterexamples. This
   557 is explained in more detail in \S\ref{scope-monotonicity}.
   558 
   559 \subsection{Inductive Datatypes}
   560 \label{inductive-datatypes}
   561 
   562 Like natural numbers and integers, inductive datatypes with recursive
   563 constructors admit no finite models and must be approximated by a subterm-closed
   564 subset. For example, using a cardinality of 10 for ${'}a~\textit{list}$,
   565 Nitpick looks for all counterexamples that can be built using at most 10
   566 different lists.
   567 
   568 Let's see with an example involving \textit{hd} (which returns the first element
   569 of a list) and $@$ (which concatenates two lists):
   570 
   571 \prew
   572 \textbf{lemma} ``$\textit{hd}~(\textit{xs} \mathbin{@} [y, y]) = \textit{hd}~\textit{xs}$'' \\
   573 \textbf{nitpick} \\[2\smallskipamount]
   574 \slshape Nitpick found a counterexample for \textit{card} $'a$~= 3: \\[2\smallskipamount]
   575 \hbox{}\qquad Free variables: \nopagebreak \\
   576 \hbox{}\qquad\qquad $\textit{xs} = []$ \\
   577 \hbox{}\qquad\qquad $\textit{y} = a_1$
   578 \postw
   579 
   580 To see why the counterexample is genuine, we enable \textit{show\_consts}
   581 and \textit{show\_\allowbreak datatypes}:
   582 
   583 \prew
   584 {\slshape Datatype:} \\
   585 \hbox{}\qquad $'a$~\textit{list}~= $\{[],\, [a_1],\, [a_1, a_1],\, \unr\}$ \\
   586 {\slshape Constants:} \\
   587 \hbox{}\qquad $\lambda x_1.\; x_1 \mathbin{@} [y, y] = \undef([] := [a_1, a_1])$ \\
   588 \hbox{}\qquad $\textit{hd} = \undef([] := a_2,\> [a_1] := a_1,\> [a_1, a_1] := a_1)$
   589 \postw
   590 
   591 Since $\mathit{hd}~[]$ is undefined in the logic, it may be given any value,
   592 including $a_2$.
   593 
   594 The second constant, $\lambda x_1.\; x_1 \mathbin{@} [y, y]$, is simply the
   595 append operator whose second argument is fixed to be $[y, y]$. Appending $[a_1,
   596 a_1]$ to $[a_1]$ would normally give $[a_1, a_1, a_1]$, but this value is not
   597 representable in the subset of $'a$~\textit{list} considered by Nitpick, which
   598 is shown under the ``Datatype'' heading; hence the result is $\unk$. Similarly,
   599 appending $[a_1, a_1]$ to itself gives $\unk$.
   600 
   601 Given \textit{card}~$'a = 3$ and \textit{card}~$'a~\textit{list} = 3$, Nitpick
   602 considers the following subsets:
   603 
   604 \kern-.5\smallskipamount %% TYPESETTING
   605 
   606 \prew
   607 \begin{multicols}{3}
   608 $\{[],\, [a_1],\, [a_2]\}$; \\
   609 $\{[],\, [a_1],\, [a_3]\}$; \\
   610 $\{[],\, [a_2],\, [a_3]\}$; \\
   611 $\{[],\, [a_1],\, [a_1, a_1]\}$; \\
   612 $\{[],\, [a_1],\, [a_2, a_1]\}$; \\
   613 $\{[],\, [a_1],\, [a_3, a_1]\}$; \\
   614 $\{[],\, [a_2],\, [a_1, a_2]\}$; \\
   615 $\{[],\, [a_2],\, [a_2, a_2]\}$; \\
   616 $\{[],\, [a_2],\, [a_3, a_2]\}$; \\
   617 $\{[],\, [a_3],\, [a_1, a_3]\}$; \\
   618 $\{[],\, [a_3],\, [a_2, a_3]\}$; \\
   619 $\{[],\, [a_3],\, [a_3, a_3]\}$.
   620 \end{multicols}
   621 \postw
   622 
   623 \kern-2\smallskipamount %% TYPESETTING
   624 
   625 All subterm-closed subsets of $'a~\textit{list}$ consisting of three values
   626 are listed and only those. As an example of a non-subterm-closed subset,
   627 consider $\mathcal{S} = \{[],\, [a_1],\,\allowbreak [a_1, a_2]\}$, and observe
   628 that $[a_1, a_2]$ (i.e., $a_1 \mathbin{\#} [a_2]$) has $[a_2] \notin
   629 \mathcal{S}$ as a subterm.
   630 
   631 Here's another m\"ochtegern-lemma that Nitpick can refute without a blink:
   632 
   633 \prew
   634 \textbf{lemma} ``$\lbrakk \textit{length}~\textit{xs} = 1;\> \textit{length}~\textit{ys} = 1
   635 \rbrakk \,\Longrightarrow\, \textit{xs} = \textit{ys}$''
   636 \\
   637 \textbf{nitpick} [\textit{show\_datatypes}] \\[2\smallskipamount]
   638 \slshape Nitpick found a counterexample for \textit{card} $'a$~= 3: \\[2\smallskipamount]
   639 \hbox{}\qquad Free variables: \nopagebreak \\
   640 \hbox{}\qquad\qquad $\textit{xs} = [a_1]$ \\
   641 \hbox{}\qquad\qquad $\textit{ys} = [a_2]$ \\
   642 \hbox{}\qquad Datatypes: \\
   643 \hbox{}\qquad\qquad $\textit{nat} = \{0,\, 1,\, 2,\, \unr\}$ \\
   644 \hbox{}\qquad\qquad $'a$~\textit{list} = $\{[],\, [a_1],\, [a_2],\, \unr\}$
   645 \postw
   646 
   647 Because datatypes are approximated using a three-valued logic, there is usually
   648 no need to systematically enumerate cardinalities: If Nitpick cannot find a
   649 genuine counterexample for \textit{card}~$'a~\textit{list}$~= 10, it is very
   650 unlikely that one could be found for smaller cardinalities.
   651 
   652 \subsection{Typedefs, Quotient Types, Records, Rationals, and Reals}
   653 \label{typedefs-quotient-types-records-rationals-and-reals}
   654 
   655 Nitpick generally treats types declared using \textbf{typedef} as datatypes
   656 whose single constructor is the corresponding \textit{Abs\_\kern.1ex} function.
   657 For example:
   658 
   659 \prew
   660 \textbf{typedef}~\textit{three} = ``$\{0\Colon\textit{nat},\, 1,\, 2\}$'' \\
   661 \textbf{by}~\textit{blast} \\[2\smallskipamount]
   662 \textbf{definition}~$A \mathbin{\Colon} \textit{three}$ \textbf{where} ``\kern-.1em$A \,\equiv\, \textit{Abs\_\allowbreak three}~0$'' \\
   663 \textbf{definition}~$B \mathbin{\Colon} \textit{three}$ \textbf{where} ``$B \,\equiv\, \textit{Abs\_three}~1$'' \\
   664 \textbf{definition}~$C \mathbin{\Colon} \textit{three}$ \textbf{where} ``$C \,\equiv\, \textit{Abs\_three}~2$'' \\[2\smallskipamount]
   665 \textbf{lemma} ``$\lbrakk P~A;\> P~B\rbrakk \,\Longrightarrow\, P~x$'' \\
   666 \textbf{nitpick} [\textit{show\_datatypes}] \\[2\smallskipamount]
   667 \slshape Nitpick found a counterexample: \\[2\smallskipamount]
   668 \hbox{}\qquad Free variables: \nopagebreak \\
   669 \hbox{}\qquad\qquad $P = \{\Abs{0},\, \Abs{1}\}$ \\
   670 \hbox{}\qquad\qquad $x = \Abs{2}$ \\
   671 \hbox{}\qquad Datatypes: \\
   672 \hbox{}\qquad\qquad $\textit{nat} = \{0,\, 1,\, 2,\, \unr\}$ \\
   673 \hbox{}\qquad\qquad $\textit{three} = \{\Abs{0},\, \Abs{1},\, \Abs{2},\, \unr\}$
   674 \postw
   675 
   676 In the output above, $\Abs{n}$ abbreviates $\textit{Abs\_three}~n$.
   677 
   678 Quotient types are handled in much the same way. The following fragment defines
   679 the integer type \textit{my\_int} by encoding the integer $x$ by a pair of
   680 natural numbers $(m, n)$ such that $x + n = m$:
   681 
   682 \prew
   683 \textbf{fun} \textit{my\_int\_rel} \textbf{where} \\
   684 ``$\textit{my\_int\_rel}~(x,\, y)~(u,\, v) = (x + v = u + y)$'' \\[2\smallskipamount]
   685 %
   686 \textbf{quotient\_type}~\textit{my\_int} = ``$\textit{nat} \times \textit{nat\/}$''$\;{/}\;$\textit{my\_int\_rel} \\
   687 \textbf{by}~(\textit{auto simp add\/}:\ \textit{equivp\_def expand\_fun\_eq}) \\[2\smallskipamount]
   688 %
   689 \textbf{definition}~\textit{add\_raw}~\textbf{where} \\
   690 ``$\textit{add\_raw} \,\equiv\, \lambda(x,\, y)~(u,\, v).\; (x + (u\Colon\textit{nat}), y + (v\Colon\textit{nat}))$'' \\[2\smallskipamount]
   691 %
   692 \textbf{quotient\_definition} ``$\textit{add\/}\Colon\textit{my\_int} \Rightarrow \textit{my\_int} \Rightarrow \textit{my\_int\/}$'' \textbf{is} \textit{add\_raw} \\[2\smallskipamount]
   693 %
   694 \textbf{lemma} ``$\textit{add}~x~y = \textit{add}~x~x$'' \\
   695 \textbf{nitpick} [\textit{show\_datatypes}] \\[2\smallskipamount]
   696 \slshape Nitpick found a counterexample: \\[2\smallskipamount]
   697 \hbox{}\qquad Free variables: \nopagebreak \\
   698 \hbox{}\qquad\qquad $x = \Abs{(0,\, 0)}$ \\
   699 \hbox{}\qquad\qquad $y = \Abs{(1,\, 0)}$ \\
   700 \hbox{}\qquad Datatypes: \\
   701 \hbox{}\qquad\qquad $\textit{nat} = \{0,\, 1,\, \unr\}$ \\
   702 \hbox{}\qquad\qquad $\textit{nat} \times \textit{nat}~[\textsl{boxed\/}] = \{(0,\, 0),\> (1,\, 0),\> \unr\}$ \\
   703 \hbox{}\qquad\qquad $\textit{my\_int} = \{\Abs{(0,\, 0)},\> \Abs{(1,\, 0)},\> \unr\}$
   704 \postw
   705 
   706 In the counterexample, $\Abs{(0,\, 0)}$ and $\Abs{(1,\, 0)}$ represent the
   707 integers $0$ and $1$, respectively. Other representants would have been
   708 possible---e.g., $\Abs{(5,\, 5)}$ and $\Abs{(12,\, 11)}$. If we are going to
   709 use \textit{my\_int} extensively, it pays off to install a term postprocessor
   710 that converts the pair notation to the standard mathematical notation:
   711 
   712 \prew
   713 $\textbf{ML}~\,\{{*} \\
   714 \!\begin{aligned}[t]
   715 %& ({*}~\,\textit{Proof.context} \rightarrow \textit{string} \rightarrow (\textit{typ} \rightarrow \textit{term~list\/}) \rightarrow \textit{typ} \rightarrow \textit{term} \\[-2pt]
   716 %& \phantom{(*}~\,{\rightarrow}\;\textit{term}~\,{*}) \\[-2pt]
   717 & \textbf{fun}\,~\textit{my\_int\_postproc}~\_~\_~\_~T~(\textit{Const}~\_~\$~(\textit{Const}~\_~\$~\textit{t1}~\$~\textit{t2\/})) = {} \\[-2pt]
   718 & \phantom{fun}\,~\textit{HOLogic.mk\_number}~T~(\textit{snd}~(\textit{HOLogic.dest\_number~t1}) \\[-2pt]
   719 & \phantom{fun\,~\textit{HOLogic.mk\_number}~T~(}{-}~\textit{snd}~(\textit{HOLogic.dest\_number~t2\/})) \\[-2pt]
   720 & \phantom{fun}\!{\mid}\,~\textit{my\_int\_postproc}~\_~\_~\_~\_~t = t \\[-2pt]
   721 {*}\}\end{aligned}$ \\[2\smallskipamount]
   722 $\textbf{setup}~\,\{{*} \\
   723 \!\begin{aligned}[t]
   724 & \textit{Nitpick.register\_term\_postprocessor}~\!\begin{aligned}[t]
   725   & @\{\textrm{typ}~\textit{my\_int}\}~\textit{my\_int\_postproc}\end{aligned} \\[-2pt]
   726 {*}\}\end{aligned}$
   727 \postw
   728 
   729 Records are also handled as datatypes with a single constructor:
   730 
   731 \prew
   732 \textbf{record} \textit{point} = \\
   733 \hbox{}\quad $\textit{Xcoord} \mathbin{\Colon} \textit{int}$ \\
   734 \hbox{}\quad $\textit{Ycoord} \mathbin{\Colon} \textit{int}$ \\[2\smallskipamount]
   735 \textbf{lemma} ``$\textit{Xcoord}~(p\Colon\textit{point}) = \textit{Xcoord}~(q\Colon\textit{point})$'' \\
   736 \textbf{nitpick} [\textit{show\_datatypes}] \\[2\smallskipamount]
   737 \slshape Nitpick found a counterexample: \\[2\smallskipamount]
   738 \hbox{}\qquad Free variables: \nopagebreak \\
   739 \hbox{}\qquad\qquad $p = \lparr\textit{Xcoord} = 1,\> \textit{Ycoord} = 1\rparr$ \\
   740 \hbox{}\qquad\qquad $q = \lparr\textit{Xcoord} = 0,\> \textit{Ycoord} = 0\rparr$ \\
   741 \hbox{}\qquad Datatypes: \\
   742 \hbox{}\qquad\qquad $\textit{int} = \{0,\, 1,\, \unr\}$ \\
   743 \hbox{}\qquad\qquad $\textit{point} = \{\!\begin{aligned}[t]
   744 & \lparr\textit{Xcoord} = 0,\> \textit{Ycoord} = 0\rparr, \\[-2pt] %% TYPESETTING
   745 & \lparr\textit{Xcoord} = 1,\> \textit{Ycoord} = 1\rparr,\, \unr\}\end{aligned}$
   746 \postw
   747 
   748 Finally, Nitpick provides rudimentary support for rationals and reals using a
   749 similar approach:
   750 
   751 \prew
   752 \textbf{lemma} ``$4 * x + 3 * (y\Colon\textit{real}) \not= 1/2$'' \\
   753 \textbf{nitpick} [\textit{show\_datatypes}] \\[2\smallskipamount]
   754 \slshape Nitpick found a counterexample: \\[2\smallskipamount]
   755 \hbox{}\qquad Free variables: \nopagebreak \\
   756 \hbox{}\qquad\qquad $x = 1/2$ \\
   757 \hbox{}\qquad\qquad $y = -1/2$ \\
   758 \hbox{}\qquad Datatypes: \\
   759 \hbox{}\qquad\qquad $\textit{nat} = \{0,\, 1,\, 2,\, 3,\, 4,\, 5,\, 6,\, 7,\, \unr\}$ \\
   760 \hbox{}\qquad\qquad $\textit{int} = \{0,\, 1,\, 2,\, 3,\, 4,\, -3,\, -2,\, -1,\, \unr\}$ \\
   761 \hbox{}\qquad\qquad $\textit{real} = \{1,\, 0,\, 4,\, -3/2,\, 3,\, 2,\, 1/2,\, -1/2,\, \unr\}$
   762 \postw
   763 
   764 \subsection{Inductive and Coinductive Predicates}
   765 \label{inductive-and-coinductive-predicates}
   766 
   767 Inductively defined predicates (and sets) are particularly problematic for
   768 counterexample generators. They can make Quickcheck~\cite{berghofer-nipkow-2004}
   769 loop forever and Refute~\cite{weber-2008} run out of resources. The crux of
   770 the problem is that they are defined using a least fixed point construction.
   771 
   772 Nitpick's philosophy is that not all inductive predicates are equal. Consider
   773 the \textit{even} predicate below:
   774 
   775 \prew
   776 \textbf{inductive}~\textit{even}~\textbf{where} \\
   777 ``\textit{even}~0'' $\,\mid$ \\
   778 ``\textit{even}~$n\,\Longrightarrow\, \textit{even}~(\textit{Suc}~(\textit{Suc}~n))$''
   779 \postw
   780 
   781 This predicate enjoys the desirable property of being well-founded, which means
   782 that the introduction rules don't give rise to infinite chains of the form
   783 
   784 \prew
   785 $\cdots\,\Longrightarrow\, \textit{even}~k''
   786        \,\Longrightarrow\, \textit{even}~k'
   787        \,\Longrightarrow\, \textit{even}~k.$
   788 \postw
   789 
   790 For \textit{even}, this is obvious: Any chain ending at $k$ will be of length
   791 $k/2 + 1$:
   792 
   793 \prew
   794 $\textit{even}~0\,\Longrightarrow\, \textit{even}~2\,\Longrightarrow\, \cdots
   795        \,\Longrightarrow\, \textit{even}~(k - 2)
   796        \,\Longrightarrow\, \textit{even}~k.$
   797 \postw
   798 
   799 Wellfoundedness is desirable because it enables Nitpick to use a very efficient
   800 fixed point computation.%
   801 \footnote{If an inductive predicate is
   802 well-founded, then it has exactly one fixed point, which is simultaneously the
   803 least and the greatest fixed point. In these circumstances, the computation of
   804 the least fixed point amounts to the computation of an arbitrary fixed point,
   805 which can be performed using a straightforward recursive equation.}
   806 Moreover, Nitpick can prove wellfoundedness of most well-founded predicates,
   807 just as Isabelle's \textbf{function} package usually discharges termination
   808 proof obligations automatically.
   809 
   810 Let's try an example:
   811 
   812 \prew
   813 \textbf{lemma} ``$\exists n.\; \textit{even}~n \mathrel{\land} \textit{even}~(\textit{Suc}~n)$'' \\
   814 \textbf{nitpick}~[\textit{card nat}~= 50, \textit{unary\_ints}, \textit{verbose}] \\[2\smallskipamount]
   815 \slshape The inductive predicate ``\textit{even}'' was proved well-founded.
   816 Nitpick can compute it efficiently. \\[2\smallskipamount]
   817 Trying 1 scope: \\
   818 \hbox{}\qquad \textit{card nat}~= 50. \\[2\smallskipamount]
   819 Nitpick found a potential counterexample for \textit{card nat}~= 50: \\[2\smallskipamount]
   820 \hbox{}\qquad Empty assignment \\[2\smallskipamount]
   821 Nitpick could not find a better counterexample. \\[2\smallskipamount]
   822 Total time: 2274 ms.
   823 \postw
   824 
   825 No genuine counterexample is possible because Nitpick cannot rule out the
   826 existence of a natural number $n \ge 50$ such that both $\textit{even}~n$ and
   827 $\textit{even}~(\textit{Suc}~n)$ are true. To help Nitpick, we can bound the
   828 existential quantifier:
   829 
   830 \prew
   831 \textbf{lemma} ``$\exists n \mathbin{\le} 49.\; \textit{even}~n \mathrel{\land} \textit{even}~(\textit{Suc}~n)$'' \\
   832 \textbf{nitpick}~[\textit{card nat}~= 50, \textit{unary\_ints}] \\[2\smallskipamount]
   833 \slshape Nitpick found a counterexample: \\[2\smallskipamount]
   834 \hbox{}\qquad Empty assignment
   835 \postw
   836 
   837 So far we were blessed by the wellfoundedness of \textit{even}. What happens if
   838 we use the following definition instead?
   839 
   840 \prew
   841 \textbf{inductive} $\textit{even}'$ \textbf{where} \\
   842 ``$\textit{even}'~(0{\Colon}\textit{nat})$'' $\,\mid$ \\
   843 ``$\textit{even}'~2$'' $\,\mid$ \\
   844 ``$\lbrakk\textit{even}'~m;\> \textit{even}'~n\rbrakk \,\Longrightarrow\, \textit{even}'~(m + n)$''
   845 \postw
   846 
   847 This definition is not well-founded: From $\textit{even}'~0$ and
   848 $\textit{even}'~0$, we can derive that $\textit{even}'~0$. Nonetheless, the
   849 predicates $\textit{even}$ and $\textit{even}'$ are equivalent.
   850 
   851 Let's check a property involving $\textit{even}'$. To make up for the
   852 foreseeable computational hurdles entailed by non-wellfoundedness, we decrease
   853 \textit{nat}'s cardinality to a mere 10:
   854 
   855 \prew
   856 \textbf{lemma}~``$\exists n \in \{0, 2, 4, 6, 8\}.\;
   857 \lnot\;\textit{even}'~n$'' \\
   858 \textbf{nitpick}~[\textit{card nat}~= 10,\, \textit{verbose},\, \textit{show\_consts}] \\[2\smallskipamount]
   859 \slshape
   860 The inductive predicate ``$\textit{even}'\!$'' could not be proved well-founded.
   861 Nitpick might need to unroll it. \\[2\smallskipamount]
   862 Trying 6 scopes: \\
   863 \hbox{}\qquad \textit{card nat}~= 10 and \textit{iter} $\textit{even}'$~= 0; \\
   864 \hbox{}\qquad \textit{card nat}~= 10 and \textit{iter} $\textit{even}'$~= 1; \\
   865 \hbox{}\qquad \textit{card nat}~= 10 and \textit{iter} $\textit{even}'$~= 2; \\
   866 \hbox{}\qquad \textit{card nat}~= 10 and \textit{iter} $\textit{even}'$~= 4; \\
   867 \hbox{}\qquad \textit{card nat}~= 10 and \textit{iter} $\textit{even}'$~= 8; \\
   868 \hbox{}\qquad \textit{card nat}~= 10 and \textit{iter} $\textit{even}'$~= 9. \\[2\smallskipamount]
   869 Nitpick found a counterexample for \textit{card nat}~= 10 and \textit{iter} $\textit{even}'$~= 2: \\[2\smallskipamount]
   870 \hbox{}\qquad Constant: \nopagebreak \\
   871 \hbox{}\qquad\qquad $\lambda i.\; \textit{even}'$ = $\undef(\!\begin{aligned}[t]
   872 & 2 := \{0, 2, 4, 6, 8, 1^\Q, 3^\Q, 5^\Q, 7^\Q, 9^\Q\}, \\[-2pt]
   873 & 1 := \{0, 2, 4, 1^\Q, 3^\Q, 5^\Q, 6^\Q, 7^\Q, 8^\Q, 9^\Q\}, \\[-2pt]
   874 & 0 := \{0, 2, 1^\Q, 3^\Q, 4^\Q, 5^\Q, 6^\Q, 7^\Q, 8^\Q, 9^\Q\})\end{aligned}$ \\[2\smallskipamount]
   875 Total time: 1140 ms.
   876 \postw
   877 
   878 Nitpick's output is very instructive. First, it tells us that the predicate is
   879 unrolled, meaning that it is computed iteratively from the empty set. Then it
   880 lists six scopes specifying different bounds on the numbers of iterations:\ 0,
   881 1, 2, 4, 8, and~9.
   882 
   883 The output also shows how each iteration contributes to $\textit{even}'$. The
   884 notation $\lambda i.\; \textit{even}'$ indicates that the value of the
   885 predicate depends on an iteration counter. Iteration 0 provides the basis
   886 elements, $0$ and $2$. Iteration 1 contributes $4$ ($= 2 + 2$). Iteration 2
   887 throws $6$ ($= 2 + 4 = 4 + 2$) and $8$ ($= 4 + 4$) into the mix. Further
   888 iterations would not contribute any new elements.
   889 
   890 Some values are marked with superscripted question
   891 marks~(`\lower.2ex\hbox{$^\Q$}'). These are the elements for which the
   892 predicate evaluates to $\unk$. Thus, $\textit{even}'$ evaluates to either
   893 \textit{True} or $\unk$, never \textit{False}.
   894 
   895 When unrolling a predicate, Nitpick tries 0, 1, 2, 4, 8, 12, 16, and 24
   896 iterations. However, these numbers are bounded by the cardinality of the
   897 predicate's domain. With \textit{card~nat}~= 10, no more than 9 iterations are
   898 ever needed to compute the value of a \textit{nat} predicate. You can specify
   899 the number of iterations using the \textit{iter} option, as explained in
   900 \S\ref{scope-of-search}.
   901 
   902 In the next formula, $\textit{even}'$ occurs both positively and negatively:
   903 
   904 \prew
   905 \textbf{lemma} ``$\textit{even}'~(n - 2) \,\Longrightarrow\, \textit{even}'~n$'' \\
   906 \textbf{nitpick} [\textit{card nat} = 10, \textit{show\_consts}] \\[2\smallskipamount]
   907 \slshape Nitpick found a counterexample: \\[2\smallskipamount]
   908 \hbox{}\qquad Free variable: \nopagebreak \\
   909 \hbox{}\qquad\qquad $n = 1$ \\
   910 \hbox{}\qquad Constants: \nopagebreak \\
   911 \hbox{}\qquad\qquad $\lambda i.\; \textit{even}'$ = $\undef(\!\begin{aligned}[t]
   912 & 0 := \{0, 2, 1^\Q, 3^\Q, 4^\Q, 5^\Q, 6^\Q, 7^\Q, 8^\Q, 9^\Q\})\end{aligned}$  \\
   913 \hbox{}\qquad\qquad $\textit{even}' \subseteq \{0, 2, 4, 6, 8, \unr\}$
   914 \postw
   915 
   916 Notice the special constraint $\textit{even}' \subseteq \{0,\, 2,\, 4,\, 6,\,
   917 8,\, \unr\}$ in the output, whose right-hand side represents an arbitrary
   918 fixed point (not necessarily the least one). It is used to falsify
   919 $\textit{even}'~n$. In contrast, the unrolled predicate is used to satisfy
   920 $\textit{even}'~(n - 2)$.
   921 
   922 Coinductive predicates are handled dually. For example:
   923 
   924 \prew
   925 \textbf{coinductive} \textit{nats} \textbf{where} \\
   926 ``$\textit{nats}~(x\Colon\textit{nat}) \,\Longrightarrow\, \textit{nats}~x$'' \\[2\smallskipamount]
   927 \textbf{lemma} ``$\textit{nats} = \{0, 1, 2, 3, 4\}$'' \\
   928 \textbf{nitpick}~[\textit{card nat} = 10,\, \textit{show\_consts}] \\[2\smallskipamount]
   929 \slshape Nitpick found a counterexample:
   930 \\[2\smallskipamount]
   931 \hbox{}\qquad Constants: \nopagebreak \\
   932 \hbox{}\qquad\qquad $\lambda i.\; \textit{nats} = \undef(0 := \{\!\begin{aligned}[t]
   933 & 0^\Q, 1^\Q, 2^\Q, 3^\Q, 4^\Q, 5^\Q, 6^\Q, 7^\Q, 8^\Q, 9^\Q, \\[-2pt]
   934 & \unr\})\end{aligned}$ \\
   935 \hbox{}\qquad\qquad $nats \supseteq \{9, 5^\Q, 6^\Q, 7^\Q, 8^\Q, \unr\}$
   936 \postw
   937 
   938 As a special case, Nitpick uses Kodkod's transitive closure operator to encode
   939 negative occurrences of non-well-founded ``linear inductive predicates,'' i.e.,
   940 inductive predicates for which each the predicate occurs in at most one
   941 assumption of each introduction rule. For example:
   942 
   943 \prew
   944 \textbf{inductive} \textit{odd} \textbf{where} \\
   945 ``$\textit{odd}~1$'' $\,\mid$ \\
   946 ``$\lbrakk \textit{odd}~m;\>\, \textit{even}~n\rbrakk \,\Longrightarrow\, \textit{odd}~(m + n)$'' \\[2\smallskipamount]
   947 \textbf{lemma}~``$\textit{odd}~n \,\Longrightarrow\, \textit{odd}~(n - 2)$'' \\
   948 \textbf{nitpick}~[\textit{card nat} = 10,\, \textit{show\_consts}] \\[2\smallskipamount]
   949 \slshape Nitpick found a counterexample:
   950 \\[2\smallskipamount]
   951 \hbox{}\qquad Free variable: \nopagebreak \\
   952 \hbox{}\qquad\qquad $n = 1$ \\
   953 \hbox{}\qquad Constants: \nopagebreak \\
   954 \hbox{}\qquad\qquad $\textit{even} = \{0, 2, 4, 6, 8, \unr\}$ \\
   955 \hbox{}\qquad\qquad $\textit{odd}_{\textsl{base}} = \{1, \unr\}$ \\
   956 \hbox{}\qquad\qquad $\textit{odd}_{\textsl{step}} = \!
   957 \!\begin{aligned}[t]
   958   & \{(0, 0), (0, 2), (0, 4), (0, 6), (0, 8), (1, 1), (1, 3), (1, 5), \\[-2pt]
   959   & \phantom{\{} (1, 7), (1, 9), (2, 2), (2, 4), (2, 6), (2, 8), (3, 3),
   960        (3, 5), \\[-2pt]
   961   & \phantom{\{} (3, 7), (3, 9), (4, 4), (4, 6), (4, 8), (5, 5), (5, 7), (5, 9), \\[-2pt]
   962   & \phantom{\{} (6, 6), (6, 8), (7, 7), (7, 9), (8, 8), (9, 9), \unr\}\end{aligned}$ \\
   963 \hbox{}\qquad\qquad $\textit{odd} \subseteq \{1, 3, 5, 7, 9, 8^\Q, \unr\}$
   964 \postw
   965 
   966 \noindent
   967 In the output, $\textit{odd}_{\textrm{base}}$ represents the base elements and
   968 $\textit{odd}_{\textrm{step}}$ is a transition relation that computes new
   969 elements from known ones. The set $\textit{odd}$ consists of all the values
   970 reachable through the reflexive transitive closure of
   971 $\textit{odd}_{\textrm{step}}$ starting with any element from
   972 $\textit{odd}_{\textrm{base}}$, namely 1, 3, 5, 7, and 9. Using Kodkod's
   973 transitive closure to encode linear predicates is normally either more thorough
   974 or more efficient than unrolling (depending on the value of \textit{iter}), but
   975 for those cases where it isn't you can disable it by passing the
   976 \textit{dont\_star\_linear\_preds} option.
   977 
   978 \subsection{Coinductive Datatypes}
   979 \label{coinductive-datatypes}
   980 
   981 While Isabelle regrettably lacks a high-level mechanism for defining coinductive
   982 datatypes, the \textit{Coinductive\_List} theory from Andreas Lochbihler's
   983 \textit{Coinductive} AFP entry \cite{lochbihler-2010} provides a coinductive
   984 ``lazy list'' datatype, $'a~\textit{llist}$, defined the hard way. Nitpick
   985 supports these lazy lists seamlessly and provides a hook, described in
   986 \S\ref{registration-of-coinductive-datatypes}, to register custom coinductive
   987 datatypes.
   988 
   989 (Co)intuitively, a coinductive datatype is similar to an inductive datatype but
   990 allows infinite objects. Thus, the infinite lists $\textit{ps}$ $=$ $[a, a, a,
   991 \ldots]$, $\textit{qs}$ $=$ $[a, b, a, b, \ldots]$, and $\textit{rs}$ $=$ $[0,
   992 1, 2, 3, \ldots]$ can be defined as lazy lists using the
   993 $\textit{LNil}\mathbin{\Colon}{'}a~\textit{llist}$ and
   994 $\textit{LCons}\mathbin{\Colon}{'}a \mathbin{\Rightarrow} {'}a~\textit{llist}
   995 \mathbin{\Rightarrow} {'}a~\textit{llist}$ constructors.
   996 
   997 Although it is otherwise no friend of infinity, Nitpick can find counterexamples
   998 involving cyclic lists such as \textit{ps} and \textit{qs} above as well as
   999 finite lists:
  1000 
  1001 \prew
  1002 \textbf{lemma} ``$\textit{xs} \not= \textit{LCons}~a~\textit{xs}$'' \\
  1003 \textbf{nitpick} \\[2\smallskipamount]
  1004 \slshape Nitpick found a counterexample for {\itshape card}~$'a$ = 1: \\[2\smallskipamount]
  1005 \hbox{}\qquad Free variables: \nopagebreak \\
  1006 \hbox{}\qquad\qquad $\textit{a} = a_1$ \\
  1007 \hbox{}\qquad\qquad $\textit{xs} = \textsl{THE}~\omega.\; \omega = \textit{LCons}~a_1~\omega$
  1008 \postw
  1009 
  1010 The notation $\textrm{THE}~\omega.\; \omega = t(\omega)$ stands
  1011 for the infinite term $t(t(t(\ldots)))$. Hence, \textit{xs} is simply the
  1012 infinite list $[a_1, a_1, a_1, \ldots]$.
  1013 
  1014 The next example is more interesting:
  1015 
  1016 \prew
  1017 \textbf{lemma}~``$\lbrakk\textit{xs} = \textit{LCons}~a~\textit{xs};\>\,
  1018 \textit{ys} = \textit{iterates}~(\lambda b.\> a)~b\rbrakk \,\Longrightarrow\, \textit{xs} = \textit{ys}$'' \\
  1019 \textbf{nitpick} [\textit{verbose}] \\[2\smallskipamount]
  1020 \slshape The type ``\kern1pt$'a$'' passed the monotonicity test. Nitpick might be able to skip
  1021 some scopes. \\[2\smallskipamount]
  1022 Trying 8 scopes: \\
  1023 \hbox{}\qquad \textit{card} $'a$~= 1, \textit{card} ``\kern1pt$'a~\textit{list\/}$''~= 1,
  1024 and \textit{bisim\_depth}~= 0. \\
  1025 \hbox{}\qquad $\qquad\vdots$ \\[.5\smallskipamount]
  1026 \hbox{}\qquad \textit{card} $'a$~= 8, \textit{card} ``\kern1pt$'a~\textit{list\/}$''~= 8,
  1027 and \textit{bisim\_depth}~= 7. \\[2\smallskipamount]
  1028 Nitpick found a counterexample for {\itshape card}~$'a$ = 2,
  1029 \textit{card}~``\kern1pt$'a~\textit{list\/}$''~= 2, and \textit{bisim\_\allowbreak
  1030 depth}~= 1:
  1031 \\[2\smallskipamount]
  1032 \hbox{}\qquad Free variables: \nopagebreak \\
  1033 \hbox{}\qquad\qquad $\textit{a} = a_1$ \\
  1034 \hbox{}\qquad\qquad $\textit{b} = a_2$ \\
  1035 \hbox{}\qquad\qquad $\textit{xs} = \textsl{THE}~\omega.\; \omega = \textit{LCons}~a_1~\omega$ \\
  1036 \hbox{}\qquad\qquad $\textit{ys} = \textit{LCons}~a_2~(\textsl{THE}~\omega.\; \omega = \textit{LCons}~a_1~\omega)$ \\[2\smallskipamount]
  1037 Total time: 726 ms.
  1038 \postw
  1039 
  1040 The lazy list $\textit{xs}$ is simply $[a_1, a_1, a_1, \ldots]$, whereas
  1041 $\textit{ys}$ is $[a_2, a_1, a_1, a_1, \ldots]$, i.e., a lasso-shaped list with
  1042 $[a_2]$ as its stem and $[a_1]$ as its cycle. In general, the list segment
  1043 within the scope of the {THE} binder corresponds to the lasso's cycle, whereas
  1044 the segment leading to the binder is the stem.
  1045 
  1046 A salient property of coinductive datatypes is that two objects are considered
  1047 equal if and only if they lead to the same observations. For example, the lazy
  1048 lists $\textrm{THE}~\omega.\; \omega =
  1049 \textit{LCons}~a~(\textit{LCons}~b~\omega)$ and
  1050 $\textit{LCons}~a~(\textrm{THE}~\omega.\; \omega =
  1051 \textit{LCons}~b~(\textit{LCons}~a~\omega))$ are identical, because both lead
  1052 to the sequence of observations $a$, $b$, $a$, $b$, \hbox{\ldots} (or,
  1053 equivalently, both encode the infinite list $[a, b, a, b, \ldots]$). This
  1054 concept of equality for coinductive datatypes is called bisimulation and is
  1055 defined coinductively.
  1056 
  1057 Internally, Nitpick encodes the coinductive bisimilarity predicate as part of
  1058 the Kodkod problem to ensure that distinct objects lead to different
  1059 observations. This precaution is somewhat expensive and often unnecessary, so it
  1060 can be disabled by setting the \textit{bisim\_depth} option to $-1$. The
  1061 bisimilarity check is then performed \textsl{after} the counterexample has been
  1062 found to ensure correctness. If this after-the-fact check fails, the
  1063 counterexample is tagged as ``quasi genuine'' and Nitpick recommends to try
  1064 again with \textit{bisim\_depth} set to a nonnegative integer. Disabling the
  1065 check for the previous example saves approximately 150~milli\-seconds; the speed
  1066 gains can be more significant for larger scopes.
  1067 
  1068 The next formula illustrates the need for bisimilarity (either as a Kodkod
  1069 predicate or as an after-the-fact check) to prevent spurious counterexamples:
  1070 
  1071 \prew
  1072 \textbf{lemma} ``$\lbrakk xs = \textit{LCons}~a~\textit{xs};\>\, \textit{ys} = \textit{LCons}~a~\textit{ys}\rbrakk
  1073 \,\Longrightarrow\, \textit{xs} = \textit{ys}$'' \\
  1074 \textbf{nitpick} [\textit{bisim\_depth} = $-1$, \textit{show\_datatypes}] \\[2\smallskipamount]
  1075 \slshape Nitpick found a quasi genuine counterexample for $\textit{card}~'a$ = 2: \\[2\smallskipamount]
  1076 \hbox{}\qquad Free variables: \nopagebreak \\
  1077 \hbox{}\qquad\qquad $a = a_1$ \\
  1078 \hbox{}\qquad\qquad $\textit{xs} = \textsl{THE}~\omega.\; \omega =
  1079 \textit{LCons}~a_1~\omega$ \\
  1080 \hbox{}\qquad\qquad $\textit{ys} = \textsl{THE}~\omega.\; \omega = \textit{LCons}~a_1~\omega$ \\
  1081 \hbox{}\qquad Codatatype:\strut \nopagebreak \\
  1082 \hbox{}\qquad\qquad $'a~\textit{llist} =
  1083 \{\!\begin{aligned}[t]
  1084   & \textsl{THE}~\omega.\; \omega = \textit{LCons}~a_1~\omega, \\[-2pt]
  1085   & \textsl{THE}~\omega.\; \omega = \textit{LCons}~a_1~\omega,\> \unr\}\end{aligned}$
  1086 \\[2\smallskipamount]
  1087 Try again with ``\textit{bisim\_depth}'' set to a nonnegative value to confirm
  1088 that the counterexample is genuine. \\[2\smallskipamount]
  1089 {\upshape\textbf{nitpick}} \\[2\smallskipamount]
  1090 \slshape Nitpick found no counterexample.
  1091 \postw
  1092 
  1093 In the first \textbf{nitpick} invocation, the after-the-fact check discovered 
  1094 that the two known elements of type $'a~\textit{llist}$ are bisimilar.
  1095 
  1096 A compromise between leaving out the bisimilarity predicate from the Kodkod
  1097 problem and performing the after-the-fact check is to specify a lower
  1098 nonnegative \textit{bisim\_depth} value than the default one provided by
  1099 Nitpick. In general, a value of $K$ means that Nitpick will require all lists to
  1100 be distinguished from each other by their prefixes of length $K$. Be aware that
  1101 setting $K$ to a too low value can overconstrain Nitpick, preventing it from
  1102 finding any counterexamples.
  1103 
  1104 \subsection{Boxing}
  1105 \label{boxing}
  1106 
  1107 Nitpick normally maps function and product types directly to the corresponding
  1108 Kodkod concepts. As a consequence, if $'a$ has cardinality 3 and $'b$ has
  1109 cardinality 4, then $'a \times {'}b$ has cardinality 12 ($= 4 \times 3$) and $'a
  1110 \Rightarrow {'}b$ has cardinality 64 ($= 4^3$). In some circumstances, it pays
  1111 off to treat these types in the same way as plain datatypes, by approximating
  1112 them by a subset of a given cardinality. This technique is called ``boxing'' and
  1113 is particularly useful for functions passed as arguments to other functions, for
  1114 high-arity functions, and for large tuples. Under the hood, boxing involves
  1115 wrapping occurrences of the types $'a \times {'}b$ and $'a \Rightarrow {'}b$ in
  1116 isomorphic datatypes, as can be seen by enabling the \textit{debug} option.
  1117 
  1118 To illustrate boxing, we consider a formalization of $\lambda$-terms represented
  1119 using de Bruijn's notation:
  1120 
  1121 \prew
  1122 \textbf{datatype} \textit{tm} = \textit{Var}~\textit{nat}~$\mid$~\textit{Lam}~\textit{tm} $\mid$ \textit{App~tm~tm}
  1123 \postw
  1124 
  1125 The $\textit{lift}~t~k$ function increments all variables with indices greater
  1126 than or equal to $k$ by one:
  1127 
  1128 \prew
  1129 \textbf{primrec} \textit{lift} \textbf{where} \\
  1130 ``$\textit{lift}~(\textit{Var}~j)~k = \textit{Var}~(\textrm{if}~j < k~\textrm{then}~j~\textrm{else}~j + 1)$'' $\mid$ \\
  1131 ``$\textit{lift}~(\textit{Lam}~t)~k = \textit{Lam}~(\textit{lift}~t~(k + 1))$'' $\mid$ \\
  1132 ``$\textit{lift}~(\textit{App}~t~u)~k = \textit{App}~(\textit{lift}~t~k)~(\textit{lift}~u~k)$''
  1133 \postw
  1134 
  1135 The $\textit{loose}~t~k$ predicate returns \textit{True} if and only if
  1136 term $t$ has a loose variable with index $k$ or more:
  1137 
  1138 \prew
  1139 \textbf{primrec}~\textit{loose} \textbf{where} \\
  1140 ``$\textit{loose}~(\textit{Var}~j)~k = (j \ge k)$'' $\mid$ \\
  1141 ``$\textit{loose}~(\textit{Lam}~t)~k = \textit{loose}~t~(\textit{Suc}~k)$'' $\mid$ \\
  1142 ``$\textit{loose}~(\textit{App}~t~u)~k = (\textit{loose}~t~k \mathrel{\lor} \textit{loose}~u~k)$''
  1143 \postw
  1144 
  1145 Next, the $\textit{subst}~\sigma~t$ function applies the substitution $\sigma$
  1146 on $t$:
  1147 
  1148 \prew
  1149 \textbf{primrec}~\textit{subst} \textbf{where} \\
  1150 ``$\textit{subst}~\sigma~(\textit{Var}~j) = \sigma~j$'' $\mid$ \\
  1151 ``$\textit{subst}~\sigma~(\textit{Lam}~t) = {}$\phantom{''} \\
  1152 \phantom{``}$\textit{Lam}~(\textit{subst}~(\lambda n.\> \textrm{case}~n~\textrm{of}~0 \Rightarrow \textit{Var}~0 \mid \textit{Suc}~m \Rightarrow \textit{lift}~(\sigma~m)~1)~t)$'' $\mid$ \\
  1153 ``$\textit{subst}~\sigma~(\textit{App}~t~u) = \textit{App}~(\textit{subst}~\sigma~t)~(\textit{subst}~\sigma~u)$''
  1154 \postw
  1155 
  1156 A substitution is a function that maps variable indices to terms. Observe that
  1157 $\sigma$ is a function passed as argument and that Nitpick can't optimize it
  1158 away, because the recursive call for the \textit{Lam} case involves an altered
  1159 version. Also notice the \textit{lift} call, which increments the variable
  1160 indices when moving under a \textit{Lam}.
  1161 
  1162 A reasonable property to expect of substitution is that it should leave closed
  1163 terms unchanged. Alas, even this simple property does not hold:
  1164 
  1165 \pre
  1166 \textbf{lemma}~``$\lnot\,\textit{loose}~t~0 \,\Longrightarrow\, \textit{subst}~\sigma~t = t$'' \\
  1167 \textbf{nitpick} [\textit{verbose}] \\[2\smallskipamount]
  1168 \slshape
  1169 Trying 8 scopes: \nopagebreak \\
  1170 \hbox{}\qquad \textit{card~nat}~= 1, \textit{card tm}~= 1, and \textit{card} ``$\textit{nat} \Rightarrow \textit{tm}$'' = 1; \\
  1171 \hbox{}\qquad \textit{card~nat}~= 2, \textit{card tm}~= 2, and \textit{card} ``$\textit{nat} \Rightarrow \textit{tm}$'' = 2; \\
  1172 \hbox{}\qquad $\qquad\vdots$ \\[.5\smallskipamount]
  1173 \hbox{}\qquad \textit{card~nat}~= 8, \textit{card tm}~= 8, and \textit{card} ``$\textit{nat} \Rightarrow \textit{tm}$'' = 8. \\[2\smallskipamount]
  1174 Nitpick found a counterexample for \textit{card~nat}~= 6, \textit{card~tm}~= 6,
  1175 and \textit{card}~``$\textit{nat} \Rightarrow \textit{tm}$''~= 6: \\[2\smallskipamount]
  1176 \hbox{}\qquad Free variables: \nopagebreak \\
  1177 \hbox{}\qquad\qquad $\sigma = \undef(\!\begin{aligned}[t]
  1178 & 0 := \textit{Var}~0,\>
  1179   1 := \textit{Var}~0,\>
  1180   2 := \textit{Var}~0, \\[-2pt]
  1181 & 3 := \textit{Var}~0,\>
  1182   4 := \textit{Var}~0,\>
  1183   5 := \textit{Var}~0)\end{aligned}$ \\
  1184 \hbox{}\qquad\qquad $t = \textit{Lam}~(\textit{Lam}~(\textit{Var}~1))$ \\[2\smallskipamount]
  1185 Total time: $4679$ ms.
  1186 \postw
  1187 
  1188 Using \textit{eval}, we find out that $\textit{subst}~\sigma~t =
  1189 \textit{Lam}~(\textit{Lam}~(\textit{Var}~0))$. Using the traditional
  1190 $\lambda$-term notation, $t$~is
  1191 $\lambda x\, y.\> x$ whereas $\textit{subst}~\sigma~t$ is $\lambda x\, y.\> y$.
  1192 The bug is in \textit{subst\/}: The $\textit{lift}~(\sigma~m)~1$ call should be
  1193 replaced with $\textit{lift}~(\sigma~m)~0$.
  1194 
  1195 An interesting aspect of Nitpick's verbose output is that it assigned inceasing
  1196 cardinalities from 1 to 8 to the type $\textit{nat} \Rightarrow \textit{tm}$.
  1197 For the formula of interest, knowing 6 values of that type was enough to find
  1198 the counterexample. Without boxing, $46\,656$ ($= 6^6$) values must be
  1199 considered, a hopeless undertaking:
  1200 
  1201 \prew
  1202 \textbf{nitpick} [\textit{dont\_box}] \\[2\smallskipamount]
  1203 {\slshape Nitpick ran out of time after checking 4 of 8 scopes.}
  1204 \postw
  1205 
  1206 {\looseness=-1
  1207 Boxing can be enabled or disabled globally or on a per-type basis using the
  1208 \textit{box} option. Nitpick usually performs reasonable choices about which
  1209 types should be boxed, but option tweaking sometimes helps. A related optimization,
  1210 ``finalization,'' attempts to wrap functions that constant at all but finitely
  1211 many points (e.g., finite sets); see the documentation for the \textit{finalize}
  1212 option in \S\ref{scope-of-search} for details.
  1213 
  1214 }
  1215 
  1216 \subsection{Scope Monotonicity}
  1217 \label{scope-monotonicity}
  1218 
  1219 The \textit{card} option (together with \textit{iter}, \textit{bisim\_depth},
  1220 and \textit{max}) controls which scopes are actually tested. In general, to
  1221 exhaust all models below a certain cardinality bound, the number of scopes that
  1222 Nitpick must consider increases exponentially with the number of type variables
  1223 (and \textbf{typedecl}'d types) occurring in the formula. Given the default
  1224 cardinality specification of 1--8, no fewer than $8^4 = 4096$ scopes must be
  1225 considered for a formula involving $'a$, $'b$, $'c$, and $'d$.
  1226 
  1227 Fortunately, many formulas exhibit a property called \textsl{scope
  1228 monotonicity}, meaning that if the formula is falsifiable for a given scope,
  1229 it is also falsifiable for all larger scopes \cite[p.~165]{jackson-2006}.
  1230 
  1231 Consider the formula
  1232 
  1233 \prew
  1234 \textbf{lemma}~``$\textit{length~xs} = \textit{length~ys} \,\Longrightarrow\, \textit{rev}~(\textit{zip~xs~ys}) = \textit{zip~xs}~(\textit{rev~ys})$''
  1235 \postw
  1236 
  1237 where \textit{xs} is of type $'a~\textit{list}$ and \textit{ys} is of type
  1238 $'b~\textit{list}$. A priori, Nitpick would need to consider 512 scopes to
  1239 exhaust the specification \textit{card}~= 1--8. However, our intuition tells us
  1240 that any counterexample found with a small scope would still be a counterexample
  1241 in a larger scope---by simply ignoring the fresh $'a$ and $'b$ values provided
  1242 by the larger scope. Nitpick comes to the same conclusion after a careful
  1243 inspection of the formula and the relevant definitions:
  1244 
  1245 \prew
  1246 \textbf{nitpick}~[\textit{verbose}] \\[2\smallskipamount]
  1247 \slshape
  1248 The types ``\kern1pt$'a$'' and ``\kern1pt$'b$'' passed the monotonicity test.
  1249 Nitpick might be able to skip some scopes.
  1250  \\[2\smallskipamount]
  1251 Trying 8 scopes: \\
  1252 \hbox{}\qquad \textit{card} $'a$~= 1, \textit{card} $'b$~= 1,
  1253 \textit{card} \textit{nat}~= 1, \textit{card} ``$('a \times {'}b)$
  1254 \textit{list\/}''~= 1, \\
  1255 \hbox{}\qquad\quad \textit{card} ``\kern1pt$'a$ \textit{list\/}''~= 1, and
  1256 \textit{card} ``\kern1pt$'b$ \textit{list\/}''~= 1. \\
  1257 \hbox{}\qquad \textit{card} $'a$~= 2, \textit{card} $'b$~= 2,
  1258 \textit{card} \textit{nat}~= 2, \textit{card} ``$('a \times {'}b)$
  1259 \textit{list\/}''~= 2, \\
  1260 \hbox{}\qquad\quad \textit{card} ``\kern1pt$'a$ \textit{list\/}''~= 2, and
  1261 \textit{card} ``\kern1pt$'b$ \textit{list\/}''~= 2. \\
  1262 \hbox{}\qquad $\qquad\vdots$ \\[.5\smallskipamount]
  1263 \hbox{}\qquad \textit{card} $'a$~= 8, \textit{card} $'b$~= 8,
  1264 \textit{card} \textit{nat}~= 8, \textit{card} ``$('a \times {'}b)$
  1265 \textit{list\/}''~= 8, \\
  1266 \hbox{}\qquad\quad \textit{card} ``\kern1pt$'a$ \textit{list\/}''~= 8, and
  1267 \textit{card} ``\kern1pt$'b$ \textit{list\/}''~= 8.
  1268 \\[2\smallskipamount]
  1269 Nitpick found a counterexample for
  1270 \textit{card} $'a$~= 5, \textit{card} $'b$~= 5,
  1271 \textit{card} \textit{nat}~= 5, \textit{card} ``$('a \times {'}b)$
  1272 \textit{list\/}''~= 5, \textit{card} ``\kern1pt$'a$ \textit{list\/}''~= 5, and
  1273 \textit{card} ``\kern1pt$'b$ \textit{list\/}''~= 5:
  1274 \\[2\smallskipamount]
  1275 \hbox{}\qquad Free variables: \nopagebreak \\
  1276 \hbox{}\qquad\qquad $\textit{xs} = [a_1, a_2]$ \\
  1277 \hbox{}\qquad\qquad $\textit{ys} = [b_1, b_1]$ \\[2\smallskipamount]
  1278 Total time: 1636 ms.
  1279 \postw
  1280 
  1281 In theory, it should be sufficient to test a single scope:
  1282 
  1283 \prew
  1284 \textbf{nitpick}~[\textit{card}~= 8]
  1285 \postw
  1286 
  1287 However, this is often less efficient in practice and may lead to overly complex
  1288 counterexamples.
  1289 
  1290 If the monotonicity check fails but we believe that the formula is monotonic (or
  1291 we don't mind missing some counterexamples), we can pass the
  1292 \textit{mono} option. To convince yourself that this option is risky,
  1293 simply consider this example from \S\ref{skolemization}:
  1294 
  1295 \prew
  1296 \textbf{lemma} ``$\exists g.\; \forall x\Colon 'b.~g~(f~x) = x
  1297  \,\Longrightarrow\, \forall y\Colon {'}a.\; \exists x.~y = f~x$'' \\
  1298 \textbf{nitpick} [\textit{mono}] \\[2\smallskipamount]
  1299 {\slshape Nitpick found no counterexample.} \\[2\smallskipamount]
  1300 \textbf{nitpick} \\[2\smallskipamount]
  1301 \slshape
  1302 Nitpick found a counterexample for \textit{card} $'a$~= 2 and \textit{card} $'b$~=~1: \\
  1303 \hbox{}\qquad $\vdots$
  1304 \postw
  1305 
  1306 (It turns out the formula holds if and only if $\textit{card}~'a \le
  1307 \textit{card}~'b$.) Although this is rarely advisable, the automatic
  1308 monotonicity checks can be disabled by passing \textit{non\_mono}
  1309 (\S\ref{optimizations}).
  1310 
  1311 As insinuated in \S\ref{natural-numbers-and-integers} and
  1312 \S\ref{inductive-datatypes}, \textit{nat}, \textit{int}, and inductive datatypes
  1313 are normally monotonic and treated as such. The same is true for record types,
  1314 \textit{rat}, \textit{real}, and some \textbf{typedef}'d types. Thus, given the
  1315 cardinality specification 1--8, a formula involving \textit{nat}, \textit{int},
  1316 \textit{int~list}, \textit{rat}, and \textit{rat~list} will lead Nitpick to
  1317 consider only 8~scopes instead of $32\,768$.
  1318 
  1319 \subsection{Inductive Properties}
  1320 \label{inductive-properties}
  1321 
  1322 Inductive properties are a particular pain to prove, because the failure to
  1323 establish an induction step can mean several things:
  1324 %
  1325 \begin{enumerate}
  1326 \item The property is invalid.
  1327 \item The property is valid but is too weak to support the induction step.
  1328 \item The property is valid and strong enough; it's just that we haven't found
  1329 the proof yet.
  1330 \end{enumerate}
  1331 %
  1332 Depending on which scenario applies, we would take the appropriate course of
  1333 action:
  1334 %
  1335 \begin{enumerate}
  1336 \item Repair the statement of the property so that it becomes valid.
  1337 \item Generalize the property and/or prove auxiliary properties.
  1338 \item Work harder on a proof.
  1339 \end{enumerate}
  1340 %
  1341 How can we distinguish between the three scenarios? Nitpick's normal mode of
  1342 operation can often detect scenario 1, and Isabelle's automatic tactics help with
  1343 scenario 3. Using appropriate techniques, it is also often possible to use
  1344 Nitpick to identify scenario 2. Consider the following transition system,
  1345 in which natural numbers represent states:
  1346 
  1347 \prew
  1348 \textbf{inductive\_set}~\textit{reach}~\textbf{where} \\
  1349 ``$(4\Colon\textit{nat}) \in \textit{reach\/}$'' $\mid$ \\
  1350 ``$\lbrakk n < 4;\> n \in \textit{reach\/}\rbrakk \,\Longrightarrow\, 3 * n + 1 \in \textit{reach\/}$'' $\mid$ \\
  1351 ``$n \in \textit{reach} \,\Longrightarrow n + 2 \in \textit{reach\/}$''
  1352 \postw
  1353 
  1354 We will try to prove that only even numbers are reachable:
  1355 
  1356 \prew
  1357 \textbf{lemma}~``$n \in \textit{reach} \,\Longrightarrow\, 2~\textrm{dvd}~n$''
  1358 \postw
  1359 
  1360 Does this property hold? Nitpick cannot find a counterexample within 30 seconds,
  1361 so let's attempt a proof by induction:
  1362 
  1363 \prew
  1364 \textbf{apply}~(\textit{induct~set}{:}~\textit{reach\/}) \\
  1365 \textbf{apply}~\textit{auto}
  1366 \postw
  1367 
  1368 This leaves us in the following proof state:
  1369 
  1370 \prew
  1371 {\slshape goal (2 subgoals): \\
  1372 \phantom{0}1. ${\bigwedge}n.\;\, \lbrakk n \in \textit{reach\/};\, n < 4;\, 2~\textsl{dvd}~n\rbrakk \,\Longrightarrow\, 2~\textsl{dvd}~\textit{Suc}~(3 * n)$ \\
  1373 \phantom{0}2. ${\bigwedge}n.\;\, \lbrakk n \in \textit{reach\/};\, 2~\textsl{dvd}~n\rbrakk \,\Longrightarrow\, 2~\textsl{dvd}~\textit{Suc}~(\textit{Suc}~n)$
  1374 }
  1375 \postw
  1376 
  1377 If we run Nitpick on the first subgoal, it still won't find any
  1378 counterexample; and yet, \textit{auto} fails to go further, and \textit{arith}
  1379 is helpless. However, notice the $n \in \textit{reach}$ assumption, which
  1380 strengthens the induction hypothesis but is not immediately usable in the proof.
  1381 If we remove it and invoke Nitpick, this time we get a counterexample:
  1382 
  1383 \prew
  1384 \textbf{apply}~(\textit{thin\_tac}~``$n \in \textit{reach\/}$'') \\
  1385 \textbf{nitpick} \\[2\smallskipamount]
  1386 \slshape Nitpick found a counterexample: \\[2\smallskipamount]
  1387 \hbox{}\qquad Skolem constant: \nopagebreak \\
  1388 \hbox{}\qquad\qquad $n = 0$
  1389 \postw
  1390 
  1391 Indeed, 0 < 4, 2 divides 0, but 2 does not divide 1. We can use this information
  1392 to strength the lemma:
  1393 
  1394 \prew
  1395 \textbf{lemma}~``$n \in \textit{reach} \,\Longrightarrow\, 2~\textrm{dvd}~n \mathrel{\lor} n \not= 0$''
  1396 \postw
  1397 
  1398 Unfortunately, the proof by induction still gets stuck, except that Nitpick now
  1399 finds the counterexample $n = 2$. We generalize the lemma further to
  1400 
  1401 \prew
  1402 \textbf{lemma}~``$n \in \textit{reach} \,\Longrightarrow\, 2~\textrm{dvd}~n \mathrel{\lor} n \ge 4$''
  1403 \postw
  1404 
  1405 and this time \textit{arith} can finish off the subgoals.
  1406 
  1407 A similar technique can be employed for structural induction. The
  1408 following mini formalization of full binary trees will serve as illustration:
  1409 
  1410 \prew
  1411 \textbf{datatype} $\kern1pt'a$~\textit{bin\_tree} = $\textit{Leaf}~{\kern1pt'a}$ $\mid$ $\textit{Branch}$ ``\kern1pt$'a$ \textit{bin\_tree}'' ``\kern1pt$'a$ \textit{bin\_tree}'' \\[2\smallskipamount]
  1412 \textbf{primrec}~\textit{labels}~\textbf{where} \\
  1413 ``$\textit{labels}~(\textit{Leaf}~a) = \{a\}$'' $\mid$ \\
  1414 ``$\textit{labels}~(\textit{Branch}~t~u) = \textit{labels}~t \mathrel{\cup} \textit{labels}~u$'' \\[2\smallskipamount]
  1415 \textbf{primrec}~\textit{swap}~\textbf{where} \\
  1416 ``$\textit{swap}~(\textit{Leaf}~c)~a~b =$ \\
  1417 \phantom{``}$(\textrm{if}~c = a~\textrm{then}~\textit{Leaf}~b~\textrm{else~if}~c = b~\textrm{then}~\textit{Leaf}~a~\textrm{else}~\textit{Leaf}~c)$'' $\mid$ \\
  1418 ``$\textit{swap}~(\textit{Branch}~t~u)~a~b = \textit{Branch}~(\textit{swap}~t~a~b)~(\textit{swap}~u~a~b)$''
  1419 \postw
  1420 
  1421 The \textit{labels} function returns the set of labels occurring on leaves of a
  1422 tree, and \textit{swap} exchanges two labels. Intuitively, if two distinct
  1423 labels $a$ and $b$ occur in a tree $t$, they should also occur in the tree
  1424 obtained by swapping $a$ and $b$:
  1425 
  1426 \prew
  1427 \textbf{lemma} $``\{a, b\} \subseteq \textit{labels}~t \,\Longrightarrow\, \textit{labels}~(\textit{swap}~t~a~b) = \textit{labels}~t$''
  1428 \postw
  1429 
  1430 Nitpick can't find any counterexample, so we proceed with induction
  1431 (this time favoring a more structured style):
  1432 
  1433 \prew
  1434 \textbf{proof}~(\textit{induct}~$t$) \\
  1435 \hbox{}\quad \textbf{case}~\textit{Leaf}~\textbf{thus}~\textit{?case}~\textbf{by}~\textit{simp} \\
  1436 \textbf{next} \\
  1437 \hbox{}\quad \textbf{case}~$(\textit{Branch}~t~u)$~\textbf{thus} \textit{?case}
  1438 \postw
  1439 
  1440 Nitpick can't find any counterexample at this point either, but it makes the
  1441 following suggestion:
  1442 
  1443 \prew
  1444 \slshape
  1445 Hint: To check that the induction hypothesis is general enough, try this command:
  1446 \textbf{nitpick}~[\textit{non\_std}, \textit{show\_all}].
  1447 \postw
  1448 
  1449 If we follow the hint, we get a ``nonstandard'' counterexample for the step:
  1450 
  1451 \prew
  1452 \slshape Nitpick found a nonstandard counterexample for \textit{card} $'a$ = 3: \\[2\smallskipamount]
  1453 \hbox{}\qquad Free variables: \nopagebreak \\
  1454 \hbox{}\qquad\qquad $a = a_1$ \\
  1455 \hbox{}\qquad\qquad $b = a_2$ \\
  1456 \hbox{}\qquad\qquad $t = \xi_1$ \\
  1457 \hbox{}\qquad\qquad $u = \xi_2$ \\
  1458 \hbox{}\qquad Datatype: \nopagebreak \\
  1459 \hbox{}\qquad\qquad $\alpha~\textit{btree} = \{\xi_1 \mathbin{=} \textit{Branch}~\xi_1~\xi_1,\> \xi_2 \mathbin{=} \textit{Branch}~\xi_2~\xi_2,\> \textit{Branch}~\xi_1~\xi_2\}$ \\
  1460 \hbox{}\qquad {\slshape Constants:} \nopagebreak \\
  1461 \hbox{}\qquad\qquad $\textit{labels} = \undef
  1462     (\!\begin{aligned}[t]%
  1463     & \xi_1 := \{a_2, a_3\},\> \xi_2 := \{a_1\},\> \\[-2pt]
  1464     & \textit{Branch}~\xi_1~\xi_2 := \{a_1, a_2, a_3\})\end{aligned}$ \\
  1465 \hbox{}\qquad\qquad $\lambda x_1.\> \textit{swap}~x_1~a~b = \undef
  1466     (\!\begin{aligned}[t]%
  1467     & \xi_1 := \xi_2,\> \xi_2 := \xi_2, \\[-2pt]
  1468     & \textit{Branch}~\xi_1~\xi_2 := \xi_2)\end{aligned}$ \\[2\smallskipamount]
  1469 The existence of a nonstandard model suggests that the induction hypothesis is not general enough or may even
  1470 be wrong. See the Nitpick manual's ``Inductive Properties'' section for details (``\textit{isabelle doc nitpick}'').
  1471 \postw
  1472 
  1473 Reading the Nitpick manual is a most excellent idea.
  1474 But what's going on? The \textit{non\_std} option told the tool to look for
  1475 nonstandard models of binary trees, which means that new ``nonstandard'' trees
  1476 $\xi_1, \xi_2, \ldots$, are now allowed in addition to the standard trees
  1477 generated by the \textit{Leaf} and \textit{Branch} constructors.%
  1478 \footnote{Notice the similarity between allowing nonstandard trees here and
  1479 allowing unreachable states in the preceding example (by removing the ``$n \in
  1480 \textit{reach\/}$'' assumption). In both cases, we effectively enlarge the
  1481 set of objects over which the induction is performed while doing the step
  1482 in order to test the induction hypothesis's strength.}
  1483 Unlike standard trees, these new trees contain cycles. We will see later that
  1484 every property of acyclic trees that can be proved without using induction also
  1485 holds for cyclic trees. Hence,
  1486 %
  1487 \begin{quote}
  1488 \textsl{If the induction
  1489 hypothesis is strong enough, the induction step will hold even for nonstandard
  1490 objects, and Nitpick won't find any nonstandard counterexample.}
  1491 \end{quote}
  1492 %
  1493 But here the tool find some nonstandard trees $t = \xi_1$
  1494 and $u = \xi_2$ such that $a \notin \textit{labels}~t$, $b \in
  1495 \textit{labels}~t$, $a \in \textit{labels}~u$, and $b \notin \textit{labels}~u$.
  1496 Because neither tree contains both $a$ and $b$, the induction hypothesis tells
  1497 us nothing about the labels of $\textit{swap}~t~a~b$ and $\textit{swap}~u~a~b$,
  1498 and as a result we know nothing about the labels of the tree
  1499 $\textit{swap}~(\textit{Branch}~t~u)~a~b$, which by definition equals
  1500 $\textit{Branch}$ $(\textit{swap}~t~a~b)$ $(\textit{swap}~u~a~b)$, whose
  1501 labels are $\textit{labels}$ $(\textit{swap}~t~a~b) \mathrel{\cup}
  1502 \textit{labels}$ $(\textit{swap}~u~a~b)$.
  1503 
  1504 The solution is to ensure that we always know what the labels of the subtrees
  1505 are in the inductive step, by covering the cases where $a$ and/or~$b$ is not in
  1506 $t$ in the statement of the lemma:
  1507 
  1508 \prew
  1509 \textbf{lemma} ``$\textit{labels}~(\textit{swap}~t~a~b) = {}$ \\
  1510 \phantom{\textbf{lemma} ``}$(\textrm{if}~a \in \textit{labels}~t~\textrm{then}$ \nopagebreak \\
  1511 \phantom{\textbf{lemma} ``(\quad}$\textrm{if}~b \in \textit{labels}~t~\textrm{then}~\textit{labels}~t~\textrm{else}~(\textit{labels}~t - \{a\}) \mathrel{\cup} \{b\}$ \\
  1512 \phantom{\textbf{lemma} ``(}$\textrm{else}$ \\
  1513 \phantom{\textbf{lemma} ``(\quad}$\textrm{if}~b \in \textit{labels}~t~\textrm{then}~(\textit{labels}~t - \{b\}) \mathrel{\cup} \{a\}~\textrm{else}~\textit{labels}~t)$''
  1514 \postw
  1515 
  1516 This time, Nitpick won't find any nonstandard counterexample, and we can perform
  1517 the induction step using \textit{auto}.
  1518 
  1519 \section{Case Studies}
  1520 \label{case-studies}
  1521 
  1522 As a didactic device, the previous section focused mostly on toy formulas whose
  1523 validity can easily be assessed just by looking at the formula. We will now
  1524 review two somewhat more realistic case studies that are within Nitpick's
  1525 reach:\ a context-free grammar modeled by mutually inductive sets and a
  1526 functional implementation of AA trees. The results presented in this
  1527 section were produced with the following settings:
  1528 
  1529 \prew
  1530 \textbf{nitpick\_params} [\textit{max\_potential}~= 0]
  1531 \postw
  1532 
  1533 \subsection{A Context-Free Grammar}
  1534 \label{a-context-free-grammar}
  1535 
  1536 Our first case study is taken from section 7.4 in the Isabelle tutorial
  1537 \cite{isa-tutorial}. The following grammar, originally due to Hopcroft and
  1538 Ullman, produces all strings with an equal number of $a$'s and $b$'s:
  1539 
  1540 \prew
  1541 \begin{tabular}{@{}r@{$\;\,$}c@{$\;\,$}l@{}}
  1542 $S$ & $::=$ & $\epsilon \mid bA \mid aB$ \\
  1543 $A$ & $::=$ & $aS \mid bAA$ \\
  1544 $B$ & $::=$ & $bS \mid aBB$
  1545 \end{tabular}
  1546 \postw
  1547 
  1548 The intuition behind the grammar is that $A$ generates all string with one more
  1549 $a$ than $b$'s and $B$ generates all strings with one more $b$ than $a$'s.
  1550 
  1551 The alphabet consists exclusively of $a$'s and $b$'s:
  1552 
  1553 \prew
  1554 \textbf{datatype} \textit{alphabet}~= $a$ $\mid$ $b$
  1555 \postw
  1556 
  1557 Strings over the alphabet are represented by \textit{alphabet list}s.
  1558 Nonterminals in the grammar become sets of strings. The production rules
  1559 presented above can be expressed as a mutually inductive definition:
  1560 
  1561 \prew
  1562 \textbf{inductive\_set} $S$ \textbf{and} $A$ \textbf{and} $B$ \textbf{where} \\
  1563 \textit{R1}:\kern.4em ``$[] \in S$'' $\,\mid$ \\
  1564 \textit{R2}:\kern.4em ``$w \in A\,\Longrightarrow\, b \mathbin{\#} w \in S$'' $\,\mid$ \\
  1565 \textit{R3}:\kern.4em ``$w \in B\,\Longrightarrow\, a \mathbin{\#} w \in S$'' $\,\mid$ \\
  1566 \textit{R4}:\kern.4em ``$w \in S\,\Longrightarrow\, a \mathbin{\#} w \in A$'' $\,\mid$ \\
  1567 \textit{R5}:\kern.4em ``$w \in S\,\Longrightarrow\, b \mathbin{\#} w \in S$'' $\,\mid$ \\
  1568 \textit{R6}:\kern.4em ``$\lbrakk v \in B;\> v \in B\rbrakk \,\Longrightarrow\, a \mathbin{\#} v \mathbin{@} w \in B$''
  1569 \postw
  1570 
  1571 The conversion of the grammar into the inductive definition was done manually by
  1572 Joe Blow, an underpaid undergraduate student. As a result, some errors might
  1573 have sneaked in.
  1574 
  1575 Debugging faulty specifications is at the heart of Nitpick's \textsl{raison
  1576 d'\^etre}. A good approach is to state desirable properties of the specification
  1577 (here, that $S$ is exactly the set of strings over $\{a, b\}$ with as many $a$'s
  1578 as $b$'s) and check them with Nitpick. If the properties are correctly stated,
  1579 counterexamples will point to bugs in the specification. For our grammar
  1580 example, we will proceed in two steps, separating the soundness and the
  1581 completeness of the set $S$. First, soundness:
  1582 
  1583 \prew
  1584 \textbf{theorem}~\textit{S\_sound\/}: \\
  1585 ``$w \in S \longrightarrow \textit{length}~[x\mathbin{\leftarrow} w.\; x = a] =
  1586   \textit{length}~[x\mathbin{\leftarrow} w.\; x = b]$'' \\
  1587 \textbf{nitpick} \\[2\smallskipamount]
  1588 \slshape Nitpick found a counterexample: \\[2\smallskipamount]
  1589 \hbox{}\qquad Free variable: \nopagebreak \\
  1590 \hbox{}\qquad\qquad $w = [b]$
  1591 \postw
  1592 
  1593 It would seem that $[b] \in S$. How could this be? An inspection of the
  1594 introduction rules reveals that the only rule with a right-hand side of the form
  1595 $b \mathbin{\#} {\ldots} \in S$ that could have introduced $[b]$ into $S$ is
  1596 \textit{R5}:
  1597 
  1598 \prew
  1599 ``$w \in S\,\Longrightarrow\, b \mathbin{\#} w \in S$''
  1600 \postw
  1601 
  1602 On closer inspection, we can see that this rule is wrong. To match the
  1603 production $B ::= bS$, the second $S$ should be a $B$. We fix the typo and try
  1604 again:
  1605 
  1606 \prew
  1607 \textbf{nitpick} \\[2\smallskipamount]
  1608 \slshape Nitpick found a counterexample: \\[2\smallskipamount]
  1609 \hbox{}\qquad Free variable: \nopagebreak \\
  1610 \hbox{}\qquad\qquad $w = [a, a, b]$
  1611 \postw
  1612 
  1613 Some detective work is necessary to find out what went wrong here. To get $[a,
  1614 a, b] \in S$, we need $[a, b] \in B$ by \textit{R3}, which in turn can only come
  1615 from \textit{R6}:
  1616 
  1617 \prew
  1618 ``$\lbrakk v \in B;\> v \in B\rbrakk \,\Longrightarrow\, a \mathbin{\#} v \mathbin{@} w \in B$''
  1619 \postw
  1620 
  1621 Now, this formula must be wrong: The same assumption occurs twice, and the
  1622 variable $w$ is unconstrained. Clearly, one of the two occurrences of $v$ in
  1623 the assumptions should have been a $w$.
  1624 
  1625 With the correction made, we don't get any counterexample from Nitpick. Let's
  1626 move on and check completeness:
  1627 
  1628 \prew
  1629 \textbf{theorem}~\textit{S\_complete}: \\
  1630 ``$\textit{length}~[x\mathbin{\leftarrow} w.\; x = a] =
  1631    \textit{length}~[x\mathbin{\leftarrow} w.\; x = b]
  1632   \longrightarrow w \in S$'' \\
  1633 \textbf{nitpick} \\[2\smallskipamount]
  1634 \slshape Nitpick found a counterexample: \\[2\smallskipamount]
  1635 \hbox{}\qquad Free variable: \nopagebreak \\
  1636 \hbox{}\qquad\qquad $w = [b, b, a, a]$
  1637 \postw
  1638 
  1639 Apparently, $[b, b, a, a] \notin S$, even though it has the same numbers of
  1640 $a$'s and $b$'s. But since our inductive definition passed the soundness check,
  1641 the introduction rules we have are probably correct. Perhaps we simply lack an
  1642 introduction rule. Comparing the grammar with the inductive definition, our
  1643 suspicion is confirmed: Joe Blow simply forgot the production $A ::= bAA$,
  1644 without which the grammar cannot generate two or more $b$'s in a row. So we add
  1645 the rule
  1646 
  1647 \prew
  1648 ``$\lbrakk v \in A;\> w \in A\rbrakk \,\Longrightarrow\, b \mathbin{\#} v \mathbin{@} w \in A$''
  1649 \postw
  1650 
  1651 With this last change, we don't get any counterexamples from Nitpick for either
  1652 soundness or completeness. We can even generalize our result to cover $A$ and
  1653 $B$ as well:
  1654 
  1655 \prew
  1656 \textbf{theorem} \textit{S\_A\_B\_sound\_and\_complete}: \\
  1657 ``$w \in S \longleftrightarrow \textit{length}~[x \mathbin{\leftarrow} w.\; x = a] = \textit{length}~[x \mathbin{\leftarrow} w.\; x = b]$'' \\
  1658 ``$w \in A \longleftrightarrow \textit{length}~[x \mathbin{\leftarrow} w.\; x = a] = \textit{length}~[x \mathbin{\leftarrow} w.\; x = b] + 1$'' \\
  1659 ``$w \in B \longleftrightarrow \textit{length}~[x \mathbin{\leftarrow} w.\; x = b] = \textit{length}~[x \mathbin{\leftarrow} w.\; x = a] + 1$'' \\
  1660 \textbf{nitpick} \\[2\smallskipamount]
  1661 \slshape Nitpick ran out of time after checking 7 of 8 scopes.
  1662 \postw
  1663 
  1664 \subsection{AA Trees}
  1665 \label{aa-trees}
  1666 
  1667 AA trees are a kind of balanced trees discovered by Arne Andersson that provide
  1668 similar performance to red-black trees, but with a simpler implementation
  1669 \cite{andersson-1993}. They can be used to store sets of elements equipped with
  1670 a total order $<$. We start by defining the datatype and some basic extractor
  1671 functions:
  1672 
  1673 \prew
  1674 \textbf{datatype} $'a$~\textit{aa\_tree} = \\
  1675 \hbox{}\quad $\Lambda$ $\mid$ $N$ ``\kern1pt$'a\Colon \textit{linorder}$'' \textit{nat} ``\kern1pt$'a$ \textit{aa\_tree}'' ``\kern1pt$'a$ \textit{aa\_tree}''  \\[2\smallskipamount]
  1676 \textbf{primrec} \textit{data} \textbf{where} \\
  1677 ``$\textit{data}~\Lambda = \undef$'' $\,\mid$ \\
  1678 ``$\textit{data}~(N~x~\_~\_~\_) = x$'' \\[2\smallskipamount]
  1679 \textbf{primrec} \textit{dataset} \textbf{where} \\
  1680 ``$\textit{dataset}~\Lambda = \{\}$'' $\,\mid$ \\
  1681 ``$\textit{dataset}~(N~x~\_~t~u) = \{x\} \cup \textit{dataset}~t \mathrel{\cup} \textit{dataset}~u$'' \\[2\smallskipamount]
  1682 \textbf{primrec} \textit{level} \textbf{where} \\
  1683 ``$\textit{level}~\Lambda = 0$'' $\,\mid$ \\
  1684 ``$\textit{level}~(N~\_~k~\_~\_) = k$'' \\[2\smallskipamount]
  1685 \textbf{primrec} \textit{left} \textbf{where} \\
  1686 ``$\textit{left}~\Lambda = \Lambda$'' $\,\mid$ \\
  1687 ``$\textit{left}~(N~\_~\_~t~\_) = t$'' \\[2\smallskipamount]
  1688 \textbf{primrec} \textit{right} \textbf{where} \\
  1689 ``$\textit{right}~\Lambda = \Lambda$'' $\,\mid$ \\
  1690 ``$\textit{right}~(N~\_~\_~\_~u) = u$''
  1691 \postw
  1692 
  1693 The wellformedness criterion for AA trees is fairly complex. Wikipedia states it
  1694 as follows \cite{wikipedia-2009-aa-trees}:
  1695 
  1696 \kern.2\parskip %% TYPESETTING
  1697 
  1698 \pre
  1699 Each node has a level field, and the following invariants must remain true for
  1700 the tree to be valid:
  1701 
  1702 \raggedright
  1703 
  1704 \kern-.4\parskip %% TYPESETTING
  1705 
  1706 \begin{enum}
  1707 \item[]
  1708 \begin{enum}
  1709 \item[1.] The level of a leaf node is one.
  1710 \item[2.] The level of a left child is strictly less than that of its parent.
  1711 \item[3.] The level of a right child is less than or equal to that of its parent.
  1712 \item[4.] The level of a right grandchild is strictly less than that of its grandparent.
  1713 \item[5.] Every node of level greater than one must have two children.
  1714 \end{enum}
  1715 \end{enum}
  1716 \post
  1717 
  1718 \kern.4\parskip %% TYPESETTING
  1719 
  1720 The \textit{wf} predicate formalizes this description:
  1721 
  1722 \prew
  1723 \textbf{primrec} \textit{wf} \textbf{where} \\
  1724 ``$\textit{wf}~\Lambda = \textit{True}$'' $\,\mid$ \\
  1725 ``$\textit{wf}~(N~\_~k~t~u) =$ \\
  1726 \phantom{``}$(\textrm{if}~t = \Lambda~\textrm{then}$ \\
  1727 \phantom{``$(\quad$}$k = 1 \mathrel{\land} (u = \Lambda \mathrel{\lor} (\textit{level}~u = 1 \mathrel{\land} \textit{left}~u = \Lambda \mathrel{\land} \textit{right}~u = \Lambda))$ \\
  1728 \phantom{``$($}$\textrm{else}$ \\
  1729 \hbox{}\phantom{``$(\quad$}$\textit{wf}~t \mathrel{\land} \textit{wf}~u
  1730 \mathrel{\land} u \not= \Lambda \mathrel{\land} \textit{level}~t < k
  1731 \mathrel{\land} \textit{level}~u \le k$ \\
  1732 \hbox{}\phantom{``$(\quad$}${\land}\; \textit{level}~(\textit{right}~u) < k)$''
  1733 \postw
  1734 
  1735 Rebalancing the tree upon insertion and removal of elements is performed by two
  1736 auxiliary functions called \textit{skew} and \textit{split}, defined below:
  1737 
  1738 \prew
  1739 \textbf{primrec} \textit{skew} \textbf{where} \\
  1740 ``$\textit{skew}~\Lambda = \Lambda$'' $\,\mid$ \\
  1741 ``$\textit{skew}~(N~x~k~t~u) = {}$ \\
  1742 \phantom{``}$(\textrm{if}~t \not= \Lambda \mathrel{\land} k =
  1743 \textit{level}~t~\textrm{then}$ \\
  1744 \phantom{``(\quad}$N~(\textit{data}~t)~k~(\textit{left}~t)~(N~x~k~
  1745 (\textit{right}~t)~u)$ \\
  1746 \phantom{``(}$\textrm{else}$ \\
  1747 \phantom{``(\quad}$N~x~k~t~u)$''
  1748 \postw
  1749 
  1750 \prew
  1751 \textbf{primrec} \textit{split} \textbf{where} \\
  1752 ``$\textit{split}~\Lambda = \Lambda$'' $\,\mid$ \\
  1753 ``$\textit{split}~(N~x~k~t~u) = {}$ \\
  1754 \phantom{``}$(\textrm{if}~u \not= \Lambda \mathrel{\land} k =
  1755 \textit{level}~(\textit{right}~u)~\textrm{then}$ \\
  1756 \phantom{``(\quad}$N~(\textit{data}~u)~(\textit{Suc}~k)~
  1757 (N~x~k~t~(\textit{left}~u))~(\textit{right}~u)$ \\
  1758 \phantom{``(}$\textrm{else}$ \\
  1759 \phantom{``(\quad}$N~x~k~t~u)$''
  1760 \postw
  1761 
  1762 Performing a \textit{skew} or a \textit{split} should have no impact on the set
  1763 of elements stored in the tree:
  1764 
  1765 \prew
  1766 \textbf{theorem}~\textit{dataset\_skew\_split\/}:\\
  1767 ``$\textit{dataset}~(\textit{skew}~t) = \textit{dataset}~t$'' \\
  1768 ``$\textit{dataset}~(\textit{split}~t) = \textit{dataset}~t$'' \\
  1769 \textbf{nitpick} \\[2\smallskipamount]
  1770 {\slshape Nitpick ran out of time after checking 7 of 8 scopes.}
  1771 \postw
  1772 
  1773 Furthermore, applying \textit{skew} or \textit{split} to a well-formed tree
  1774 should not alter the tree:
  1775 
  1776 \prew
  1777 \textbf{theorem}~\textit{wf\_skew\_split\/}:\\
  1778 ``$\textit{wf}~t\,\Longrightarrow\, \textit{skew}~t = t$'' \\
  1779 ``$\textit{wf}~t\,\Longrightarrow\, \textit{split}~t = t$'' \\
  1780 \textbf{nitpick} \\[2\smallskipamount]
  1781 {\slshape Nitpick found no counterexample.}
  1782 \postw
  1783 
  1784 Insertion is implemented recursively. It preserves the sort order:
  1785 
  1786 \prew
  1787 \textbf{primrec}~\textit{insort} \textbf{where} \\
  1788 ``$\textit{insort}~\Lambda~x = N~x~1~\Lambda~\Lambda$'' $\,\mid$ \\
  1789 ``$\textit{insort}~(N~y~k~t~u)~x =$ \\
  1790 \phantom{``}$({*}~(\textit{split} \circ \textit{skew})~{*})~(N~y~k~(\textrm{if}~x < y~\textrm{then}~\textit{insort}~t~x~\textrm{else}~t)$ \\
  1791 \phantom{``$({*}~(\textit{split} \circ \textit{skew})~{*})~(N~y~k~$}$(\textrm{if}~x > y~\textrm{then}~\textit{insort}~u~x~\textrm{else}~u))$''
  1792 \postw
  1793 
  1794 Notice that we deliberately commented out the application of \textit{skew} and
  1795 \textit{split}. Let's see if this causes any problems:
  1796 
  1797 \prew
  1798 \textbf{theorem}~\textit{wf\_insort\/}:\kern.4em ``$\textit{wf}~t\,\Longrightarrow\, \textit{wf}~(\textit{insort}~t~x)$'' \\
  1799 \textbf{nitpick} \\[2\smallskipamount]
  1800 \slshape Nitpick found a counterexample for \textit{card} $'a$ = 4: \\[2\smallskipamount]
  1801 \hbox{}\qquad Free variables: \nopagebreak \\
  1802 \hbox{}\qquad\qquad $t = N~a_1~1~\Lambda~\Lambda$ \\
  1803 \hbox{}\qquad\qquad $x = a_2$
  1804 \postw
  1805 
  1806 It's hard to see why this is a counterexample. To improve readability, we will
  1807 restrict the theorem to \textit{nat}, so that we don't need to look up the value
  1808 of the $\textit{op}~{<}$ constant to find out which element is smaller than the
  1809 other. In addition, we will tell Nitpick to display the value of
  1810 $\textit{insort}~t~x$ using the \textit{eval} option. This gives
  1811 
  1812 \prew
  1813 \textbf{theorem} \textit{wf\_insort\_nat\/}:\kern.4em ``$\textit{wf}~t\,\Longrightarrow\, \textit{wf}~(\textit{insort}~t~(x\Colon\textit{nat}))$'' \\
  1814 \textbf{nitpick} [\textit{eval} = ``$\textit{insort}~t~x$''] \\[2\smallskipamount]
  1815 \slshape Nitpick found a counterexample: \\[2\smallskipamount]
  1816 \hbox{}\qquad Free variables: \nopagebreak \\
  1817 \hbox{}\qquad\qquad $t = N~1~1~\Lambda~\Lambda$ \\
  1818 \hbox{}\qquad\qquad $x = 0$ \\
  1819 \hbox{}\qquad Evaluated term: \\
  1820 \hbox{}\qquad\qquad $\textit{insort}~t~x = N~1~1~(N~0~1~\Lambda~\Lambda)~\Lambda$
  1821 \postw
  1822 
  1823 Nitpick's output reveals that the element $0$ was added as a left child of $1$,
  1824 where both have a level of 1. This violates the second AA tree invariant, which
  1825 states that a left child's level must be less than its parent's. This shouldn't
  1826 come as a surprise, considering that we commented out the tree rebalancing code.
  1827 Reintroducing the code seems to solve the problem:
  1828 
  1829 \prew
  1830 \textbf{theorem}~\textit{wf\_insort\/}:\kern.4em ``$\textit{wf}~t\,\Longrightarrow\, \textit{wf}~(\textit{insort}~t~x)$'' \\
  1831 \textbf{nitpick} \\[2\smallskipamount]
  1832 {\slshape Nitpick ran out of time after checking 7 of 8 scopes.}
  1833 \postw
  1834 
  1835 Insertion should transform the set of elements represented by the tree in the
  1836 obvious way:
  1837 
  1838 \prew
  1839 \textbf{theorem} \textit{dataset\_insort\/}:\kern.4em
  1840 ``$\textit{dataset}~(\textit{insort}~t~x) = \{x\} \cup \textit{dataset}~t$'' \\
  1841 \textbf{nitpick} \\[2\smallskipamount]
  1842 {\slshape Nitpick ran out of time after checking 6 of 8 scopes.}
  1843 \postw
  1844 
  1845 We could continue like this and sketch a complete theory of AA trees. Once the
  1846 definitions and main theorems are in place and have been thoroughly tested using
  1847 Nitpick, we could start working on the proofs. Developing theories this way
  1848 usually saves time, because faulty theorems and definitions are discovered much
  1849 earlier in the process.
  1850 
  1851 \section{Option Reference}
  1852 \label{option-reference}
  1853 
  1854 \def\flushitem#1{\item[]\noindent\kern-\leftmargin \textbf{#1}}
  1855 \def\qty#1{$\left<\textit{#1}\right>$}
  1856 \def\qtybf#1{$\mathbf{\left<\textbf{\textit{#1}}\right>}$}
  1857 \def\optrue#1#2{\flushitem{\textit{#1} $\bigl[$= \qtybf{bool}$\bigr]$\quad [\textit{true}]\hfill (neg.: \textit{#2})}\nopagebreak\\[\parskip]}
  1858 \def\opfalse#1#2{\flushitem{\textit{#1} $\bigl[$= \qtybf{bool}$\bigr]$\quad [\textit{false}]\hfill (neg.: \textit{#2})}\nopagebreak\\[\parskip]}
  1859 \def\opsmart#1#2{\flushitem{\textit{#1} $\bigl[$= \qtybf{bool\_or\_smart}$\bigr]$\quad [\textit{smart}]\hfill (neg.: \textit{#2})}\nopagebreak\\[\parskip]}
  1860 \def\opnodefault#1#2{\flushitem{\textit{#1} = \qtybf{#2}} \nopagebreak\\[\parskip]}
  1861 \def\opdefault#1#2#3{\flushitem{\textit{#1} = \qtybf{#2}\quad [\textit{#3}]} \nopagebreak\\[\parskip]}
  1862 \def\oparg#1#2#3{\flushitem{\textit{#1} \qtybf{#2} = \qtybf{#3}} \nopagebreak\\[\parskip]}
  1863 \def\opargbool#1#2#3{\flushitem{\textit{#1} \qtybf{#2} $\bigl[$= \qtybf{bool}$\bigr]$\hfill (neg.: \textit{#3})}\nopagebreak\\[\parskip]}
  1864 \def\opargboolorsmart#1#2#3{\flushitem{\textit{#1} \qtybf{#2} $\bigl[$= \qtybf{bool\_or\_smart}$\bigr]$\hfill (neg.: \textit{#3})}\nopagebreak\\[\parskip]}
  1865 
  1866 Nitpick's behavior can be influenced by various options, which can be specified
  1867 in brackets after the \textbf{nitpick} command. Default values can be set
  1868 using \textbf{nitpick\_\allowbreak params}. For example:
  1869 
  1870 \prew
  1871 \textbf{nitpick\_params} [\textit{verbose}, \,\textit{timeout} = 60$\,s$]
  1872 \postw
  1873 
  1874 The options are categorized as follows:\ mode of operation
  1875 (\S\ref{mode-of-operation}), scope of search (\S\ref{scope-of-search}), output
  1876 format (\S\ref{output-format}), automatic counterexample checks
  1877 (\S\ref{authentication}), optimizations
  1878 (\S\ref{optimizations}), and timeouts (\S\ref{timeouts}).
  1879 
  1880 You can instruct Nitpick to run automatically on newly entered theorems by
  1881 enabling the ``Auto Nitpick'' option from the ``Isabelle'' menu in Proof
  1882 General. For automatic runs, \textit{user\_axioms} (\S\ref{mode-of-operation})
  1883 and \textit{assms} (\S\ref{mode-of-operation}) are implicitly enabled,
  1884 \textit{blocking} (\S\ref{mode-of-operation}), \textit{verbose}
  1885 (\S\ref{output-format}), and \textit{debug} (\S\ref{output-format}) are
  1886 disabled, \textit{max\_potential} (\S\ref{output-format}) is taken to be 0, and
  1887 \textit{timeout} (\S\ref{timeouts}) is superseded by the ``Auto Counterexample
  1888 Time Limit'' in Proof General's ``Isabelle'' menu. Nitpick's output is also more
  1889 concise.
  1890 
  1891 The number of options can be overwhelming at first glance. Do not let that worry
  1892 you: Nitpick's defaults have been chosen so that it almost always does the right
  1893 thing, and the most important options have been covered in context in
  1894 \S\ref{first-steps}.
  1895 
  1896 The descriptions below refer to the following syntactic quantities:
  1897 
  1898 \begin{enum}
  1899 \item[$\bullet$] \qtybf{string}: A string.
  1900 \item[$\bullet$] \qtybf{bool\/}: \textit{true} or \textit{false}.
  1901 \item[$\bullet$] \qtybf{bool\_or\_smart\/}: \textit{true}, \textit{false}, or \textit{smart}.
  1902 \item[$\bullet$] \qtybf{int\/}: An integer. Negative integers are prefixed with a hyphen.
  1903 \item[$\bullet$] \qtybf{int\_or\_smart\/}: An integer or \textit{smart}.
  1904 \item[$\bullet$] \qtybf{int\_range}: An integer (e.g., 3) or a range
  1905 of nonnegative integers (e.g., $1$--$4$). The range symbol `--' can be entered as \texttt{-} (hyphen) or \texttt{\char`\\\char`\<midarrow\char`\>}.
  1906 
  1907 \item[$\bullet$] \qtybf{int\_seq}: A comma-separated sequence of ranges of integers (e.g.,~1{,}3{,}\allowbreak6--8).
  1908 \item[$\bullet$] \qtybf{time}: An integer followed by $\textit{min}$ (minutes), $s$ (seconds), or \textit{ms}
  1909 (milliseconds), or the keyword \textit{none} ($\infty$ years).
  1910 \item[$\bullet$] \qtybf{const\/}: The name of a HOL constant.
  1911 \item[$\bullet$] \qtybf{term}: A HOL term (e.g., ``$f~x$'').
  1912 \item[$\bullet$] \qtybf{term\_list\/}: A space-separated list of HOL terms (e.g.,
  1913 ``$f~x$''~``$g~y$'').
  1914 \item[$\bullet$] \qtybf{type}: A HOL type.
  1915 \end{enum}
  1916 
  1917 Default values are indicated in square brackets. Boolean options have a negated
  1918 counterpart (e.g., \textit{blocking} vs.\ \textit{no\_blocking}). When setting
  1919 Boolean options, ``= \textit{true}'' may be omitted.
  1920 
  1921 \subsection{Mode of Operation}
  1922 \label{mode-of-operation}
  1923 
  1924 \begin{enum}
  1925 \optrue{blocking}{non\_blocking}
  1926 Specifies whether the \textbf{nitpick} command should operate synchronously.
  1927 The asynchronous (non-blocking) mode lets the user start proving the putative
  1928 theorem while Nitpick looks for a counterexample, but it can also be more
  1929 confusing. For technical reasons, automatic runs currently always block.
  1930 
  1931 \optrue{falsify}{satisfy}
  1932 Specifies whether Nitpick should look for falsifying examples (countermodels) or
  1933 satisfying examples (models). This manual assumes throughout that
  1934 \textit{falsify} is enabled.
  1935 
  1936 \opsmart{user\_axioms}{no\_user\_axioms}
  1937 Specifies whether the user-defined axioms (specified using 
  1938 \textbf{axiomatization} and \textbf{axioms}) should be considered. If the option
  1939 is set to \textit{smart}, Nitpick performs an ad hoc axiom selection based on
  1940 the constants that occur in the formula to falsify. The option is implicitly set
  1941 to \textit{true} for automatic runs.
  1942 
  1943 \textbf{Warning:} If the option is set to \textit{true}, Nitpick might
  1944 nonetheless ignore some polymorphic axioms. Counterexamples generated under
  1945 these conditions are tagged as ``quasi genuine.'' The \textit{debug}
  1946 (\S\ref{output-format}) option can be used to find out which axioms were
  1947 considered.
  1948 
  1949 \nopagebreak
  1950 {\small See also \textit{assms} (\S\ref{mode-of-operation}) and \textit{debug}
  1951 (\S\ref{output-format}).}
  1952 
  1953 \optrue{assms}{no\_assms}
  1954 Specifies whether the relevant assumptions in structured proofs should be
  1955 considered. The option is implicitly enabled for automatic runs.
  1956 
  1957 \nopagebreak
  1958 {\small See also \textit{user\_axioms} (\S\ref{mode-of-operation}).}
  1959 
  1960 \opfalse{overlord}{no\_overlord}
  1961 Specifies whether Nitpick should put its temporary files in
  1962 \texttt{\$ISABELLE\_\allowbreak HOME\_\allowbreak USER}, which is useful for
  1963 debugging Nitpick but also unsafe if several instances of the tool are run
  1964 simultaneously. The files are identified by the extensions
  1965 \texttt{.kki}, \texttt{.cnf}, \texttt{.out}, and
  1966 \texttt{.err}; you may safely remove them after Nitpick has run.
  1967 
  1968 \nopagebreak
  1969 {\small See also \textit{debug} (\S\ref{output-format}).}
  1970 \end{enum}
  1971 
  1972 \subsection{Scope of Search}
  1973 \label{scope-of-search}
  1974 
  1975 \begin{enum}
  1976 \oparg{card}{type}{int\_seq}
  1977 Specifies the sequence of cardinalities to use for a given type.
  1978 For free types, and often also for \textbf{typedecl}'d types, it usually makes
  1979 sense to specify cardinalities as a range of the form \textit{$1$--$n$}.
  1980 
  1981 \nopagebreak
  1982 {\small See also \textit{box} (\S\ref{scope-of-search}) and \textit{mono}
  1983 (\S\ref{scope-of-search}).}
  1984 
  1985 \opdefault{card}{int\_seq}{$\mathbf{1}$--$\mathbf{8}$}
  1986 Specifies the default sequence of cardinalities to use. This can be overridden
  1987 on a per-type basis using the \textit{card}~\qty{type} option described above.
  1988 
  1989 \oparg{max}{const}{int\_seq}
  1990 Specifies the sequence of maximum multiplicities to use for a given
  1991 (co)in\-duc\-tive datatype constructor. A constructor's multiplicity is the
  1992 number of distinct values that it can construct. Nonsensical values (e.g.,
  1993 \textit{max}~[]~$=$~2) are silently repaired. This option is only available for
  1994 datatypes equipped with several constructors.
  1995 
  1996 \opnodefault{max}{int\_seq}
  1997 Specifies the default sequence of maximum multiplicities to use for
  1998 (co)in\-duc\-tive datatype constructors. This can be overridden on a per-constructor
  1999 basis using the \textit{max}~\qty{const} option described above.
  2000 
  2001 \opsmart{binary\_ints}{unary\_ints}
  2002 Specifies whether natural numbers and integers should be encoded using a unary
  2003 or binary notation. In unary mode, the cardinality fully specifies the subset
  2004 used to approximate the type. For example:
  2005 %
  2006 $$\hbox{\begin{tabular}{@{}rll@{}}%
  2007 \textit{card nat} = 4 & induces & $\{0,\, 1,\, 2,\, 3\}$ \\
  2008 \textit{card int} = 4 & induces & $\{-1,\, 0,\, +1,\, +2\}$ \\
  2009 \textit{card int} = 5 & induces & $\{-2,\, -1,\, 0,\, +1,\, +2\}.$%
  2010 \end{tabular}}$$
  2011 %
  2012 In general:
  2013 %
  2014 $$\hbox{\begin{tabular}{@{}rll@{}}%
  2015 \textit{card nat} = $K$ & induces & $\{0,\, \ldots,\, K - 1\}$ \\
  2016 \textit{card int} = $K$ & induces & $\{-\lceil K/2 \rceil + 1,\, \ldots,\, +\lfloor K/2 \rfloor\}.$%
  2017 \end{tabular}}$$
  2018 %
  2019 In binary mode, the cardinality specifies the number of distinct values that can
  2020 be constructed. Each of these value is represented by a bit pattern whose length
  2021 is specified by the \textit{bits} (\S\ref{scope-of-search}) option. By default,
  2022 Nitpick attempts to choose the more appropriate encoding by inspecting the
  2023 formula at hand, preferring the binary notation for problems involving
  2024 multiplicative operators or large constants.
  2025 
  2026 \textbf{Warning:} For technical reasons, Nitpick always reverts to unary for
  2027 problems that refer to the types \textit{rat} or \textit{real} or the constants
  2028 \textit{Suc}, \textit{gcd}, or \textit{lcm}.
  2029 
  2030 {\small See also \textit{bits} (\S\ref{scope-of-search}) and
  2031 \textit{show\_datatypes} (\S\ref{output-format}).}
  2032 
  2033 \opdefault{bits}{int\_seq}{$\mathbf{1},\mathbf{2},\mathbf{3},\mathbf{4},\mathbf{6},\mathbf{8},\mathbf{10},\mathbf{12}$}
  2034 Specifies the number of bits to use to represent natural numbers and integers in
  2035 binary, excluding the sign bit. The minimum is 1 and the maximum is 31.
  2036 
  2037 {\small See also \textit{binary\_ints} (\S\ref{scope-of-search}).}
  2038 
  2039 \opargboolorsmart{wf}{const}{non\_wf}
  2040 Specifies whether the specified (co)in\-duc\-tively defined predicate is
  2041 well-founded. The option can take the following values:
  2042 
  2043 \begin{enum}
  2044 \item[$\bullet$] \textbf{\textit{true}:} Tentatively treat the (co)in\-duc\-tive
  2045 predicate as if it were well-founded. Since this is generally not sound when the
  2046 predicate is not well-founded, the counterexamples are tagged as ``quasi
  2047 genuine.''
  2048 
  2049 \item[$\bullet$] \textbf{\textit{false}:} Treat the (co)in\-duc\-tive predicate
  2050 as if it were not well-founded. The predicate is then unrolled as prescribed by
  2051 the \textit{star\_linear\_preds}, \textit{iter}~\qty{const}, and \textit{iter}
  2052 options.
  2053 
  2054 \item[$\bullet$] \textbf{\textit{smart}:} Try to prove that the inductive
  2055 predicate is well-founded using Isabelle's \textit{lexicographic\_order} and
  2056 \textit{size\_change} tactics. If this succeeds (or the predicate occurs with an
  2057 appropriate polarity in the formula to falsify), use an efficient fixed point
  2058 equation as specification of the predicate; otherwise, unroll the predicates
  2059 according to the \textit{iter}~\qty{const} and \textit{iter} options.
  2060 \end{enum}
  2061 
  2062 \nopagebreak
  2063 {\small See also \textit{iter} (\S\ref{scope-of-search}),
  2064 \textit{star\_linear\_preds} (\S\ref{optimizations}), and \textit{tac\_timeout}
  2065 (\S\ref{timeouts}).}
  2066 
  2067 \opsmart{wf}{non\_wf}
  2068 Specifies the default wellfoundedness setting to use. This can be overridden on
  2069 a per-predicate basis using the \textit{wf}~\qty{const} option above.
  2070 
  2071 \oparg{iter}{const}{int\_seq}
  2072 Specifies the sequence of iteration counts to use when unrolling a given
  2073 (co)in\-duc\-tive predicate. By default, unrolling is applied for inductive
  2074 predicates that occur negatively and coinductive predicates that occur
  2075 positively in the formula to falsify and that cannot be proved to be
  2076 well-founded, but this behavior is influenced by the \textit{wf} option. The
  2077 iteration counts are automatically bounded by the cardinality of the predicate's
  2078 domain.
  2079 
  2080 {\small See also \textit{wf} (\S\ref{scope-of-search}) and
  2081 \textit{star\_linear\_preds} (\S\ref{optimizations}).}
  2082 
  2083 \opdefault{iter}{int\_seq}{$\mathbf{1{,}2{,}4{,}8{,}12{,}16{,}24{,}32}$}
  2084 Specifies the sequence of iteration counts to use when unrolling (co)in\-duc\-tive
  2085 predicates. This can be overridden on a per-predicate basis using the
  2086 \textit{iter} \qty{const} option above.
  2087 
  2088 \opdefault{bisim\_depth}{int\_seq}{$\mathbf{7}$}
  2089 Specifies the sequence of iteration counts to use when unrolling the
  2090 bisimilarity predicate generated by Nitpick for coinductive datatypes. A value
  2091 of $-1$ means that no predicate is generated, in which case Nitpick performs an
  2092 after-the-fact check to see if the known coinductive datatype values are
  2093 bidissimilar. If two values are found to be bisimilar, the counterexample is
  2094 tagged as ``quasi genuine.'' The iteration counts are automatically bounded by
  2095 the sum of the cardinalities of the coinductive datatypes occurring in the
  2096 formula to falsify.
  2097 
  2098 \opargboolorsmart{box}{type}{dont\_box}
  2099 Specifies whether Nitpick should attempt to wrap (``box'') a given function or
  2100 product type in an isomorphic datatype internally. Boxing is an effective mean
  2101 to reduce the search space and speed up Nitpick, because the isomorphic datatype
  2102 is approximated by a subset of the possible function or pair values.
  2103 Like other drastic optimizations, it can also prevent the discovery of
  2104 counterexamples. The option can take the following values:
  2105 
  2106 \begin{enum}
  2107 \item[$\bullet$] \textbf{\textit{true}:} Box the specified type whenever
  2108 practicable.
  2109 \item[$\bullet$] \textbf{\textit{false}:} Never box the type.
  2110 \item[$\bullet$] \textbf{\textit{smart}:} Box the type only in contexts where it
  2111 is likely to help. For example, $n$-tuples where $n > 2$ and arguments to
  2112 higher-order functions are good candidates for boxing.
  2113 \end{enum}
  2114 
  2115 \nopagebreak
  2116 {\small See also \textit{finitize} (\S\ref{scope-of-search}), \textit{verbose}
  2117 (\S\ref{output-format}), and \textit{debug} (\S\ref{output-format}).}
  2118 
  2119 \opsmart{box}{dont\_box}
  2120 Specifies the default boxing setting to use. This can be overridden on a
  2121 per-type basis using the \textit{box}~\qty{type} option described above.
  2122 
  2123 \opargboolorsmart{finitize}{type}{dont\_finitize}
  2124 Specifies whether Nitpick should attempt to finitize a given type, which can be
  2125 a function type or an infinite ``shallow datatype'' (an infinite datatype whose
  2126 constructors don't appear in the problem).
  2127 
  2128 For function types, Nitpick performs a monotonicity analysis to detect functions
  2129 that are constant at all but finitely many points (e.g., finite sets) and treats
  2130 such occurrences specially, thereby increasing the precision. The option can
  2131 then take the following values:
  2132 
  2133 \begin{enum}
  2134 \item[$\bullet$] \textbf{\textit{false}:} Don't attempt to finitize the type.
  2135 \item[$\bullet$] \textbf{\textit{true}} or \textbf{\textit{smart}:} Finitize the
  2136 type wherever possible.
  2137 \end{enum}
  2138 
  2139 The semantics of the option is somewhat different for infinite shallow
  2140 datatypes:
  2141 
  2142 \begin{enum}
  2143 \item[$\bullet$] \textbf{\textit{true}:} Finitize the datatype. Since this is
  2144 unsound, counterexamples generated under these conditions are tagged as ``quasi
  2145 genuine.''
  2146 \item[$\bullet$] \textbf{\textit{false}:} Don't attempt to finitize the datatype.
  2147 \item[$\bullet$] \textbf{\textit{smart}:} Perform a monotonicity analysis to
  2148 detect whether the datatype can be safely finitized before finitizing it.
  2149 \end{enum}
  2150 
  2151 Like other drastic optimizations, finitization can sometimes prevent the
  2152 discovery of counterexamples.
  2153 
  2154 \nopagebreak
  2155 {\small See also \textit{box} (\S\ref{scope-of-search}), \textit{mono}
  2156 (\S\ref{scope-of-search}), \textit{verbose} (\S\ref{output-format}), and
  2157 \textit{debug} (\S\ref{output-format}).}
  2158 
  2159 \opsmart{finitize}{dont\_finitize}
  2160 Specifies the default finitization setting to use. This can be overridden on a
  2161 per-type basis using the \textit{finitize}~\qty{type} option described above.
  2162 
  2163 \opargboolorsmart{mono}{type}{non\_mono}
  2164 Specifies whether the given type should be considered monotonic when enumerating
  2165 scopes and finitizing types. If the option is set to \textit{smart}, Nitpick
  2166 performs a monotonicity check on the type. Setting this option to \textit{true}
  2167 can reduce the number of scopes tried, but it can also diminish the chance of
  2168 finding a counterexample, as demonstrated in \S\ref{scope-monotonicity}.
  2169 
  2170 \nopagebreak
  2171 {\small See also \textit{card} (\S\ref{scope-of-search}),
  2172 \textit{finitize} (\S\ref{scope-of-search}),
  2173 \textit{merge\_type\_vars} (\S\ref{scope-of-search}), and \textit{verbose}
  2174 (\S\ref{output-format}).}
  2175 
  2176 \opsmart{mono}{non\_mono}
  2177 Specifies the default monotonicity setting to use. This can be overridden on a
  2178 per-type basis using the \textit{mono}~\qty{type} option described above.
  2179 
  2180 \opfalse{merge\_type\_vars}{dont\_merge\_type\_vars}
  2181 Specifies whether type variables with the same sort constraints should be
  2182 merged. Setting this option to \textit{true} can reduce the number of scopes
  2183 tried and the size of the generated Kodkod formulas, but it also diminishes the
  2184 theoretical chance of finding a counterexample.
  2185 
  2186 {\small See also \textit{mono} (\S\ref{scope-of-search}).}
  2187 
  2188 \opargbool{std}{type}{non\_std}
  2189 Specifies whether the given (recursive) datatype should be given standard
  2190 models. Nonstandard models are unsound but can help debug structural induction
  2191 proofs, as explained in \S\ref{inductive-properties}.
  2192 
  2193 \optrue{std}{non\_std}
  2194 Specifies the default standardness to use. This can be overridden on a per-type
  2195 basis using the \textit{std}~\qty{type} option described above.
  2196 \end{enum}
  2197 
  2198 \subsection{Output Format}
  2199 \label{output-format}
  2200 
  2201 \begin{enum}
  2202 \opfalse{verbose}{quiet}
  2203 Specifies whether the \textbf{nitpick} command should explain what it does. This
  2204 option is useful to determine which scopes are tried or which SAT solver is
  2205 used. This option is implicitly disabled for automatic runs.
  2206 
  2207 \opfalse{debug}{no\_debug}
  2208 Specifies whether Nitpick should display additional debugging information beyond
  2209 what \textit{verbose} already displays. Enabling \textit{debug} also enables
  2210 \textit{verbose} and \textit{show\_all} behind the scenes. The \textit{debug}
  2211 option is implicitly disabled for automatic runs.
  2212 
  2213 \nopagebreak
  2214 {\small See also \textit{overlord} (\S\ref{mode-of-operation}) and
  2215 \textit{batch\_size} (\S\ref{optimizations}).}
  2216 
  2217 \opfalse{show\_datatypes}{hide\_datatypes}
  2218 Specifies whether the subsets used to approximate (co)in\-duc\-tive datatypes should
  2219 be displayed as part of counterexamples. Such subsets are sometimes helpful when
  2220 investigating whether a potential counterexample is genuine or spurious, but
  2221 their potential for clutter is real.
  2222 
  2223 \opfalse{show\_consts}{hide\_consts}
  2224 Specifies whether the values of constants occurring in the formula (including
  2225 its axioms) should be displayed along with any counterexample. These values are
  2226 sometimes helpful when investigating why a counterexample is
  2227 genuine, but they can clutter the output.
  2228 
  2229 \opfalse{show\_all}{dont\_show\_all}
  2230 Enabling this option effectively enables \textit{show\_datatypes} and
  2231 \textit{show\_consts}.
  2232 
  2233 \opdefault{max\_potential}{int}{$\mathbf{1}$}
  2234 Specifies the maximum number of potential counterexamples to display. Setting
  2235 this option to 0 speeds up the search for a genuine counterexample. This option
  2236 is implicitly set to 0 for automatic runs. If you set this option to a value
  2237 greater than 1, you will need an incremental SAT solver, such as
  2238 \textit{MiniSat\_JNI} (recommended) and \textit{SAT4J}. Be aware that many of
  2239 the counterexamples may be identical.
  2240 
  2241 \nopagebreak
  2242 {\small See also \textit{check\_potential} (\S\ref{authentication}) and
  2243 \textit{sat\_solver} (\S\ref{optimizations}).}
  2244 
  2245 \opdefault{max\_genuine}{int}{$\mathbf{1}$}
  2246 Specifies the maximum number of genuine counterexamples to display. If you set
  2247 this option to a value greater than 1, you will need an incremental SAT solver,
  2248 such as \textit{MiniSat\_JNI} (recommended) and \textit{SAT4J}. Be aware that
  2249 many of the counterexamples may be identical.
  2250 
  2251 \nopagebreak
  2252 {\small See also \textit{check\_genuine} (\S\ref{authentication}) and
  2253 \textit{sat\_solver} (\S\ref{optimizations}).}
  2254 
  2255 \opnodefault{eval}{term\_list}
  2256 Specifies the list of terms whose values should be displayed along with
  2257 counterexamples. This option suffers from an ``observer effect'': Nitpick might
  2258 find different counterexamples for different values of this option.
  2259 
  2260 \oparg{format}{term}{int\_seq}
  2261 Specifies how to uncurry the value displayed for a variable or constant.
  2262 Uncurrying sometimes increases the readability of the output for high-arity
  2263 functions. For example, given the variable $y \mathbin{\Colon} {'a}\Rightarrow
  2264 {'b}\Rightarrow {'c}\Rightarrow {'d}\Rightarrow {'e}\Rightarrow {'f}\Rightarrow
  2265 {'g}$, setting \textit{format}~$y$ = 3 tells Nitpick to group the last three
  2266 arguments, as if the type had been ${'a}\Rightarrow {'b}\Rightarrow
  2267 {'c}\Rightarrow {'d}\times {'e}\times {'f}\Rightarrow {'g}$. In general, a list
  2268 of values $n_1,\ldots,n_k$ tells Nitpick to show the last $n_k$ arguments as an
  2269 $n_k$-tuple, the previous $n_{k-1}$ arguments as an $n_{k-1}$-tuple, and so on;
  2270 arguments that are not accounted for are left alone, as if the specification had
  2271 been $1,\ldots,1,n_1,\ldots,n_k$.
  2272 
  2273 \opdefault{format}{int\_seq}{$\mathbf{1}$}
  2274 Specifies the default format to use. Irrespective of the default format, the
  2275 extra arguments to a Skolem constant corresponding to the outer bound variables
  2276 are kept separated from the remaining arguments, the \textbf{for} arguments of
  2277 an inductive definitions are kept separated from the remaining arguments, and
  2278 the iteration counter of an unrolled inductive definition is shown alone. The
  2279 default format can be overridden on a per-variable or per-constant basis using
  2280 the \textit{format}~\qty{term} option described above.
  2281 \end{enum}
  2282 
  2283 \subsection{Authentication}
  2284 \label{authentication}
  2285 
  2286 \begin{enum}
  2287 \opfalse{check\_potential}{trust\_potential}
  2288 Specifies whether potential counterexamples should be given to Isabelle's
  2289 \textit{auto} tactic to assess their validity. If a potential counterexample is
  2290 shown to be genuine, Nitpick displays a message to this effect and terminates.
  2291 
  2292 \nopagebreak
  2293 {\small See also \textit{max\_potential} (\S\ref{output-format}).}
  2294 
  2295 \opfalse{check\_genuine}{trust\_genuine}
  2296 Specifies whether genuine and quasi genuine counterexamples should be given to
  2297 Isabelle's \textit{auto} tactic to assess their validity. If a ``genuine''
  2298 counterexample is shown to be spurious, the user is kindly asked to send a bug
  2299 report to the author at
  2300 \texttt{blan{\color{white}nospam}\kern-\wd\boxA{}chette@in.tum.de}.
  2301 
  2302 \nopagebreak
  2303 {\small See also \textit{max\_genuine} (\S\ref{output-format}).}
  2304 
  2305 \opnodefault{expect}{string}
  2306 Specifies the expected outcome, which must be one of the following:
  2307 
  2308 \begin{enum}
  2309 \item[$\bullet$] \textbf{\textit{genuine}:} Nitpick found a genuine counterexample.
  2310 \item[$\bullet$] \textbf{\textit{quasi\_genuine}:} Nitpick found a ``quasi
  2311 genuine'' counterexample (i.e., a counterexample that is genuine unless
  2312 it contradicts a missing axiom or a dangerous option was used inappropriately).
  2313 \item[$\bullet$] \textbf{\textit{potential}:} Nitpick found a potential counterexample.
  2314 \item[$\bullet$] \textbf{\textit{none}:} Nitpick found no counterexample.
  2315 \item[$\bullet$] \textbf{\textit{unknown}:} Nitpick encountered some problem (e.g.,
  2316 Kodkod ran out of memory).
  2317 \end{enum}
  2318 
  2319 Nitpick emits an error if the actual outcome differs from the expected outcome.
  2320 This option is useful for regression testing.
  2321 \end{enum}
  2322 
  2323 \subsection{Optimizations}
  2324 \label{optimizations}
  2325 
  2326 \def\cpp{C\nobreak\raisebox{.1ex}{+}\nobreak\raisebox{.1ex}{+}}
  2327 
  2328 \sloppy
  2329 
  2330 \begin{enum}
  2331 \opdefault{sat\_solver}{string}{smart}
  2332 Specifies which SAT solver to use. SAT solvers implemented in C or \cpp{} tend
  2333 to be faster than their Java counterparts, but they can be more difficult to
  2334 install. Also, if you set the \textit{max\_potential} (\S\ref{output-format}) or
  2335 \textit{max\_genuine} (\S\ref{output-format}) option to a value greater than 1,
  2336 you will need an incremental SAT solver, such as \textit{MiniSat\_JNI}
  2337 (recommended) or \textit{SAT4J}.
  2338 
  2339 The supported solvers are listed below:
  2340 
  2341 \begin{enum}
  2342 
  2343 \item[$\bullet$] \textbf{\textit{MiniSat}:} MiniSat is an efficient solver
  2344 written in \cpp{}. To use MiniSat, set the environment variable
  2345 \texttt{MINISAT\_HOME} to the directory that contains the \texttt{minisat}
  2346 executable.%
  2347 \footnote{Important note for Cygwin users: The path must be specified using
  2348 native Windows syntax. Make sure to escape backslashes properly.%
  2349 \label{cygwin-paths}}
  2350 The \cpp{} sources and executables for MiniSat are available at
  2351 \url{http://minisat.se/MiniSat.html}. Nitpick has been tested with versions 1.14
  2352 and 2.0 beta (2007-07-21).
  2353 
  2354 \item[$\bullet$] \textbf{\textit{MiniSat\_JNI}:} The JNI (Java Native Interface)
  2355 version of MiniSat is bundled with Kodkodi and is precompiled for the major
  2356 platforms. It is also available from \texttt{native\-solver.\allowbreak tgz},
  2357 which you will find on Kodkod's web site \cite{kodkod-2009}. Unlike the standard
  2358 version of MiniSat, the JNI version can be used incrementally.
  2359 
  2360 \item[$\bullet$] \textbf{\textit{PicoSAT}:} PicoSAT is an efficient solver
  2361 written in C. You can install a standard version of
  2362 PicoSAT and set the environment variable \texttt{PICOSAT\_HOME} to the directory
  2363 that contains the \texttt{picosat} executable.%
  2364 \footref{cygwin-paths}
  2365 The C sources for PicoSAT are
  2366 available at \url{http://fmv.jku.at/picosat/} and are also bundled with Kodkodi.
  2367 Nitpick has been tested with version 913.
  2368 
  2369 \item[$\bullet$] \textbf{\textit{zChaff}:} zChaff is an efficient solver written
  2370 in \cpp{}. To use zChaff, set the environment variable \texttt{ZCHAFF\_HOME} to
  2371 the directory that contains the \texttt{zchaff} executable.%
  2372 \footref{cygwin-paths}
  2373 The \cpp{} sources and executables for zChaff are available at
  2374 \url{http://www.princeton.edu/~chaff/zchaff.html}. Nitpick has been tested with
  2375 versions 2004-05-13, 2004-11-15, and 2007-03-12.
  2376 
  2377 \item[$\bullet$] \textbf{\textit{zChaff\_JNI}:} The JNI version of zChaff is
  2378 bundled with Kodkodi and is precompiled for the major
  2379 platforms. It is also available from \texttt{native\-solver.\allowbreak tgz},
  2380 which you will find on Kodkod's web site \cite{kodkod-2009}.
  2381 
  2382 \item[$\bullet$] \textbf{\textit{RSat}:} RSat is an efficient solver written in
  2383 \cpp{}. To use RSat, set the environment variable \texttt{RSAT\_HOME} to the
  2384 directory that contains the \texttt{rsat} executable.%
  2385 \footref{cygwin-paths}
  2386 The \cpp{} sources for RSat are available at
  2387 \url{http://reasoning.cs.ucla.edu/rsat/}. Nitpick has been tested with version
  2388 2.01.
  2389 
  2390 \item[$\bullet$] \textbf{\textit{BerkMin}:} BerkMin561 is an efficient solver
  2391 written in C. To use BerkMin, set the environment variable
  2392 \texttt{BERKMIN\_HOME} to the directory that contains the \texttt{BerkMin561}
  2393 executable.\footref{cygwin-paths}
  2394 The BerkMin executables are available at
  2395 \url{http://eigold.tripod.com/BerkMin.html}.
  2396 
  2397 \item[$\bullet$] \textbf{\textit{BerkMin\_Alloy}:} Variant of BerkMin that is
  2398 included with Alloy 4 and calls itself ``sat56'' in its banner text. To use this
  2399 version of BerkMin, set the environment variable
  2400 \texttt{BERKMINALLOY\_HOME} to the directory that contains the \texttt{berkmin}
  2401 executable.%
  2402 \footref{cygwin-paths}
  2403 
  2404 \item[$\bullet$] \textbf{\textit{Jerusat}:} Jerusat 1.3 is an efficient solver
  2405 written in C. To use Jerusat, set the environment variable
  2406 \texttt{JERUSAT\_HOME} to the directory that contains the \texttt{Jerusat1.3}
  2407 executable.%
  2408 \footref{cygwin-paths}
  2409 The C sources for Jerusat are available at
  2410 \url{http://www.cs.tau.ac.il/~ale1/Jerusat1.3.tgz}.
  2411 
  2412 \item[$\bullet$] \textbf{\textit{SAT4J}:} SAT4J is a reasonably efficient solver
  2413 written in Java that can be used incrementally. It is bundled with Kodkodi and
  2414 requires no further installation or configuration steps. Do not attempt to
  2415 install the official SAT4J packages, because their API is incompatible with
  2416 Kodkod.
  2417 
  2418 \item[$\bullet$] \textbf{\textit{SAT4J\_Light}:} Variant of SAT4J that is
  2419 optimized for small problems. It can also be used incrementally.
  2420 
  2421 \item[$\bullet$] \textbf{\textit{smart}:} If \textit{sat\_solver} is set to
  2422 \textit{smart}, Nitpick selects the first solver among MiniSat,
  2423 PicoSAT, zChaff, RSat, BerkMin, BerkMin\_Alloy, Jerusat, MiniSat\_JNI, and zChaff\_JNI
  2424 that is recognized by Isabelle. If none is found, it falls back on SAT4J, which
  2425 should always be available. If \textit{verbose} (\S\ref{output-format}) is
  2426 enabled, Nitpick displays which SAT solver was chosen.
  2427 \end{enum}
  2428 \fussy
  2429 
  2430 \opdefault{batch\_size}{int\_or\_smart}{smart}
  2431 Specifies the maximum number of Kodkod problems that should be lumped together
  2432 when invoking Kodkodi. Each problem corresponds to one scope. Lumping problems
  2433 together ensures that Kodkodi is launched less often, but it makes the verbose
  2434 output less readable and is sometimes detrimental to performance. If
  2435 \textit{batch\_size} is set to \textit{smart}, the actual value used is 1 if
  2436 \textit{debug} (\S\ref{output-format}) is set and 64 otherwise.
  2437 
  2438 \optrue{destroy\_constrs}{dont\_destroy\_constrs}
  2439 Specifies whether formulas involving (co)in\-duc\-tive datatype constructors should
  2440 be rewritten to use (automatically generated) discriminators and destructors.
  2441 This optimization can drastically reduce the size of the Boolean formulas given
  2442 to the SAT solver.
  2443 
  2444 \nopagebreak
  2445 {\small See also \textit{debug} (\S\ref{output-format}).}
  2446 
  2447 \optrue{specialize}{dont\_specialize}
  2448 Specifies whether functions invoked with static arguments should be specialized.
  2449 This optimization can drastically reduce the search space, especially for
  2450 higher-order functions.
  2451 
  2452 \nopagebreak
  2453 {\small See also \textit{debug} (\S\ref{output-format}) and
  2454 \textit{show\_consts} (\S\ref{output-format}).}
  2455 
  2456 \optrue{star\_linear\_preds}{dont\_star\_linear\_preds}
  2457 Specifies whether Nitpick should use Kodkod's transitive closure operator to
  2458 encode non-well-founded ``linear inductive predicates,'' i.e., inductive
  2459 predicates for which each the predicate occurs in at most one assumption of each
  2460 introduction rule. Using the reflexive transitive closure is in principle
  2461 equivalent to setting \textit{iter} to the cardinality of the predicate's
  2462 domain, but it is usually more efficient.
  2463 
  2464 {\small See also \textit{wf} (\S\ref{scope-of-search}), \textit{debug}
  2465 (\S\ref{output-format}), and \textit{iter} (\S\ref{scope-of-search}).}
  2466 
  2467 \optrue{fast\_descrs}{full\_descrs}
  2468 Specifies whether Nitpick should optimize the definite and indefinite
  2469 description operators (THE and SOME). The optimized versions usually help
  2470 Nitpick generate more counterexamples or at least find them faster, but only the
  2471 unoptimized versions are complete when all types occurring in the formula are
  2472 finite.
  2473 
  2474 {\small See also \textit{debug} (\S\ref{output-format}).}
  2475 
  2476 \optrue{peephole\_optim}{no\_peephole\_optim}
  2477 Specifies whether Nitpick should simplify the generated Kodkod formulas using a
  2478 peephole optimizer. These optimizations can make a significant difference.
  2479 Unless you are tracking down a bug in Nitpick or distrust the peephole
  2480 optimizer, you should leave this option enabled.
  2481 
  2482 \opdefault{max\_threads}{int}{0}
  2483 Specifies the maximum number of threads to use in Kodkod. If this option is set
  2484 to 0, Kodkod will compute an appropriate value based on the number of processor
  2485 cores available.
  2486 
  2487 \nopagebreak
  2488 {\small See also \textit{batch\_size} (\S\ref{optimizations}) and
  2489 \textit{timeout} (\S\ref{timeouts}).}
  2490 \end{enum}
  2491 
  2492 \subsection{Timeouts}
  2493 \label{timeouts}
  2494 
  2495 \begin{enum}
  2496 \opdefault{timeout}{time}{$\mathbf{30}$ s}
  2497 Specifies the maximum amount of time that the \textbf{nitpick} command should
  2498 spend looking for a counterexample. Nitpick tries to honor this constraint as
  2499 well as it can but offers no guarantees. For automatic runs,
  2500 \textit{timeout} is ignored; instead, Auto Quickcheck and Auto Nitpick share
  2501 a time slot whose length is specified by the ``Auto Counterexample Time
  2502 Limit'' option in Proof General.
  2503 
  2504 \nopagebreak
  2505 {\small See also \textit{max\_threads} (\S\ref{optimizations}).}
  2506 
  2507 \opdefault{tac\_timeout}{time}{$\mathbf{500}$\,ms}
  2508 Specifies the maximum amount of time that the \textit{auto} tactic should use
  2509 when checking a counterexample, and similarly that \textit{lexicographic\_order}
  2510 and \textit{size\_change} should use when checking whether a (co)in\-duc\-tive
  2511 predicate is well-founded. Nitpick tries to honor this constraint as well as it
  2512 can but offers no guarantees.
  2513 
  2514 \nopagebreak
  2515 {\small See also \textit{wf} (\S\ref{scope-of-search}),
  2516 \textit{check\_potential} (\S\ref{authentication}),
  2517 and \textit{check\_genuine} (\S\ref{authentication}).}
  2518 \end{enum}
  2519 
  2520 \section{Attribute Reference}
  2521 \label{attribute-reference}
  2522 
  2523 Nitpick needs to consider the definitions of all constants occurring in a
  2524 formula in order to falsify it. For constants introduced using the
  2525 \textbf{definition} command, the definition is simply the associated
  2526 \textit{\_def} axiom. In contrast, instead of using the internal representation
  2527 of functions synthesized by Isabelle's \textbf{primrec}, \textbf{function}, and
  2528 \textbf{nominal\_primrec} packages, Nitpick relies on the more natural
  2529 equational specification entered by the user.
  2530 
  2531 Behind the scenes, Isabelle's built-in packages and theories rely on the
  2532 following attributes to affect Nitpick's behavior:
  2533 
  2534 \begin{enum}
  2535 \flushitem{\textit{nitpick\_def}}
  2536 
  2537 \nopagebreak
  2538 This attribute specifies an alternative definition of a constant. The
  2539 alternative definition should be logically equivalent to the constant's actual
  2540 axiomatic definition and should be of the form
  2541 
  2542 \qquad $c~{?}x_1~\ldots~{?}x_n \,\equiv\, t$,
  2543 
  2544 where ${?}x_1, \ldots, {?}x_n$ are distinct variables and $c$ does not occur in
  2545 $t$.
  2546 
  2547 \flushitem{\textit{nitpick\_simp}}
  2548 
  2549 \nopagebreak
  2550 This attribute specifies the equations that constitute the specification of a
  2551 constant. For functions defined using the \textbf{primrec}, \textbf{function},
  2552 and \textbf{nominal\_\allowbreak primrec} packages, this corresponds to the
  2553 \textit{simps} rules. The equations must be of the form
  2554 
  2555 \qquad $c~t_1~\ldots\ t_n \,=\, u.$
  2556 
  2557 \flushitem{\textit{nitpick\_psimp}}
  2558 
  2559 \nopagebreak
  2560 This attribute specifies the equations that constitute the partial specification
  2561 of a constant. For functions defined using the \textbf{function} package, this
  2562 corresponds to the \textit{psimps} rules. The conditional equations must be of
  2563 the form
  2564 
  2565 \qquad $\lbrakk P_1;\> \ldots;\> P_m\rbrakk \,\Longrightarrow\, c\ t_1\ \ldots\ t_n \,=\, u$.
  2566 
  2567 \flushitem{\textit{nitpick\_intro}}
  2568 
  2569 \nopagebreak
  2570 This attribute specifies the introduction rules of a (co)in\-duc\-tive predicate.
  2571 For predicates defined using the \textbf{inductive} or \textbf{coinductive}
  2572 command, this corresponds to the \textit{intros} rules. The introduction rules
  2573 must be of the form
  2574 
  2575 \qquad $\lbrakk P_1;\> \ldots;\> P_m;\> M~(c\ t_{11}\ \ldots\ t_{1n});\>
  2576 \ldots;\> M~(c\ t_{k1}\ \ldots\ t_{kn})\rbrakk$ \\
  2577 \hbox{}\qquad ${\Longrightarrow}\;\, c\ u_1\ \ldots\ u_n$,
  2578 
  2579 where the $P_i$'s are side conditions that do not involve $c$ and $M$ is an
  2580 optional monotonic operator. The order of the assumptions is irrelevant.
  2581 
  2582 \flushitem{\textit{nitpick\_choice\_spec}}
  2583 
  2584 \nopagebreak
  2585 This attribute specifies the (free-form) specification of a constant defined
  2586 using the \hbox{(\textbf{ax\_})}\allowbreak\textbf{specification} command.
  2587 
  2588 \end{enum}
  2589 
  2590 When faced with a constant, Nitpick proceeds as follows:
  2591 
  2592 \begin{enum}
  2593 \item[1.] If the \textit{nitpick\_simp} set associated with the constant
  2594 is not empty, Nitpick uses these rules as the specification of the constant.
  2595 
  2596 \item[2.] Otherwise, if the \textit{nitpick\_psimp} set associated with
  2597 the constant is not empty, it uses these rules as the specification of the
  2598 constant.
  2599 
  2600 \item[3.] Otherwise, if the constant was defined using the
  2601 \hbox{(\textbf{ax\_})}\allowbreak\textbf{specification} command and the
  2602 \textit{nitpick\_choice\_spec} set associated with the constant is not empty, it
  2603 uses these theorems as the specification of the constant.
  2604 
  2605 \item[4.] Otherwise, it looks up the definition of the constant:
  2606 
  2607 \begin{enum}
  2608 \item[1.] If the \textit{nitpick\_def} set associated with the constant
  2609 is not empty, it uses the latest rule added to the set as the definition of the
  2610 constant; otherwise it uses the actual definition axiom.
  2611 \item[2.] If the definition is of the form
  2612 
  2613 \qquad $c~{?}x_1~\ldots~{?}x_m \,\equiv\, \lambda y_1~\ldots~y_n.\; \textit{lfp}~(\lambda f.\; t)$,
  2614 
  2615 then Nitpick assumes that the definition was made using an inductive package and
  2616 based on the introduction rules marked with \textit{nitpick\_\allowbreak
  2617 \allowbreak intros} tries to determine whether the definition is
  2618 well-founded.
  2619 \end{enum}
  2620 \end{enum}
  2621 
  2622 As an illustration, consider the inductive definition
  2623 
  2624 \prew
  2625 \textbf{inductive}~\textit{odd}~\textbf{where} \\
  2626 ``\textit{odd}~1'' $\,\mid$ \\
  2627 ``\textit{odd}~$n\,\Longrightarrow\, \textit{odd}~(\textit{Suc}~(\textit{Suc}~n))$''
  2628 \postw
  2629 
  2630 Isabelle automatically attaches the \textit{nitpick\_intro} attribute to
  2631 the above rules. Nitpick then uses the \textit{lfp}-based definition in
  2632 conjunction with these rules. To override this, we can specify an alternative
  2633 definition as follows:
  2634 
  2635 \prew
  2636 \textbf{lemma} $\mathit{odd\_def}'$ [\textit{nitpick\_def}]:\kern.4em ``$\textit{odd}~n \,\equiv\, n~\textrm{mod}~2 = 1$''
  2637 \postw
  2638 
  2639 Nitpick then expands all occurrences of $\mathit{odd}~n$ to $n~\textrm{mod}~2
  2640 = 1$. Alternatively, we can specify an equational specification of the constant:
  2641 
  2642 \prew
  2643 \textbf{lemma} $\mathit{odd\_simp}'$ [\textit{nitpick\_simp}]:\kern.4em ``$\textit{odd}~n = (n~\textrm{mod}~2 = 1)$''
  2644 \postw
  2645 
  2646 Such tweaks should be done with great care, because Nitpick will assume that the
  2647 constant is completely defined by its equational specification. For example, if
  2648 you make ``$\textit{odd}~(2 * k + 1)$'' a \textit{nitpick\_simp} rule and neglect to provide rules to handle the $2 * k$ case, Nitpick will define
  2649 $\textit{odd}~n$ arbitrarily for even values of $n$. The \textit{debug}
  2650 (\S\ref{output-format}) option is extremely useful to understand what is going
  2651 on when experimenting with \textit{nitpick\_} attributes.
  2652 
  2653 \section{Standard ML Interface}
  2654 \label{standard-ml-interface}
  2655 
  2656 Nitpick provides a rich Standard ML interface used mainly for internal purposes
  2657 and debugging. Among the most interesting functions exported by Nitpick are
  2658 those that let you invoke the tool programmatically and those that let you
  2659 register and unregister custom coinductive datatypes as well as term
  2660 postprocessors.
  2661 
  2662 \subsection{Invocation of Nitpick}
  2663 \label{invocation-of-nitpick}
  2664 
  2665 The \textit{Nitpick} structure offers the following functions for invoking your
  2666 favorite counterexample generator:
  2667 
  2668 \prew
  2669 $\textbf{val}\,~\textit{pick\_nits\_in\_term} : \\
  2670 \hbox{}\quad\textit{Proof.state} \rightarrow \textit{params} \rightarrow \textit{bool} \rightarrow \textit{term~list} \rightarrow \textit{term} \\
  2671 \hbox{}\quad{\rightarrow}\; \textit{string} * \textit{Proof.state}$ \\
  2672 $\textbf{val}\,~\textit{pick\_nits\_in\_subgoal} : \\
  2673 \hbox{}\quad\textit{Proof.state} \rightarrow \textit{params} \rightarrow \textit{bool} \rightarrow \textit{int} \rightarrow \textit{string} * \textit{Proof.state}$
  2674 \postw
  2675 
  2676 The return value is a new proof state paired with an outcome string
  2677 (``genuine'', ``quasi\_genuine'', ``potential'', ``none'', or ``unknown''). The
  2678 \textit{params} type is a large record that lets you set Nitpick's options. The
  2679 current default options can be retrieved by calling the following function
  2680 defined in the \textit{Nitpick\_Isar} structure:
  2681 
  2682 \prew
  2683 $\textbf{val}\,~\textit{default\_params} :\,
  2684 \textit{theory} \rightarrow (\textit{string} * \textit{string})~\textit{list} \rightarrow \textit{params}$
  2685 \postw
  2686 
  2687 The second argument lets you override option values before they are parsed and
  2688 put into a \textit{params} record. Here is an example:
  2689 
  2690 \prew
  2691 $\textbf{val}\,~\textit{params} = \textit{Nitpick\_Isar.default\_params}~\textit{thy}~[(\textrm{``}\textrm{timeout\/}\textrm{''},\, \textrm{``}\textrm{none}\textrm{''})]$ \\
  2692 $\textbf{val}\,~(\textit{outcome},\, \textit{state}') = \textit{Nitpick.pick\_nits\_in\_subgoal}~\begin{aligned}[t]
  2693 & \textit{state}~\textit{params}~\textit{false} \\[-2pt]
  2694 & \textit{subgoal}\end{aligned}$
  2695 \postw
  2696 
  2697 \let\antiq=\textrm
  2698 
  2699 \subsection{Registration of Coinductive Datatypes}
  2700 \label{registration-of-coinductive-datatypes}
  2701 
  2702 If you have defined a custom coinductive datatype, you can tell Nitpick about
  2703 it, so that it can use an efficient Kodkod axiomatization similar to the one it
  2704 uses for lazy lists. The interface for registering and unregistering coinductive
  2705 datatypes consists of the following pair of functions defined in the
  2706 \textit{Nitpick} structure:
  2707 
  2708 \prew
  2709 $\textbf{val}\,~\textit{register\_codatatype} :\,
  2710 \textit{typ} \rightarrow \textit{string} \rightarrow \textit{styp~list} \rightarrow \textit{theory} \rightarrow \textit{theory}$ \\
  2711 $\textbf{val}\,~\textit{unregister\_codatatype} :\,
  2712 \textit{typ} \rightarrow \textit{theory} \rightarrow \textit{theory}$
  2713 \postw
  2714 
  2715 The type $'a~\textit{llist}$ of lazy lists is already registered; had it
  2716 not been, you could have told Nitpick about it by adding the following line
  2717 to your theory file:
  2718 
  2719 \prew
  2720 $\textbf{setup}~\,\{{*}\,~\!\begin{aligned}[t]
  2721 & \textit{Nitpick.register\_codatatype} \\[-2pt]
  2722 & \qquad @\{\antiq{typ}~``\kern1pt'a~\textit{llist\/}\textrm{''}\}~@\{\antiq{const\_name}~ \textit{llist\_case}\} \\[-2pt] %% TYPESETTING
  2723 & \qquad (\textit{map}~\textit{dest\_Const}~[@\{\antiq{term}~\textit{LNil}\},\, @\{\antiq{term}~\textit{LCons}\}])\,\ {*}\}\end{aligned}$
  2724 \postw
  2725 
  2726 The \textit{register\_codatatype} function takes a coinductive type, its case
  2727 function, and the list of its constructors. The case function must take its
  2728 arguments in the order that the constructors are listed. If no case function
  2729 with the correct signature is available, simply pass the empty string.
  2730 
  2731 On the other hand, if your goal is to cripple Nitpick, add the following line to
  2732 your theory file and try to check a few conjectures about lazy lists:
  2733 
  2734 \prew
  2735 $\textbf{setup}~\,\{{*}\,~\textit{Nitpick.unregister\_codatatype}~@\{\antiq{typ}~``
  2736 \kern1pt'a~\textit{list\/}\textrm{''}\}\ \,{*}\}$
  2737 \postw
  2738 
  2739 Inductive datatypes can be registered as coinductive datatypes, given
  2740 appropriate coinductive constructors. However, doing so precludes
  2741 the use of the inductive constructors---Nitpick will generate an error if they
  2742 are needed.
  2743 
  2744 \subsection{Registration of Term Postprocessors}
  2745 \label{registration-of-term-postprocessors}
  2746 
  2747 It is possible to change the output of any term that Nitpick considers a
  2748 datatype by registering a term postprocessor. The interface for registering and
  2749 unregistering postprocessors consists of the following pair of functions defined
  2750 in the \textit{Nitpick} structure:
  2751 
  2752 \prew
  2753 $\textbf{type}\,~\textit{term\_postprocessor}\,~{=} {}$ \\
  2754 $\hbox{}\quad\textit{Proof.context} \rightarrow \textit{string} \rightarrow (\textit{typ} \rightarrow \textit{term~list\/}) \rightarrow \textit{typ} \rightarrow \textit{term} \rightarrow \textit{term}$ \\
  2755 $\textbf{val}\,~\textit{register\_term\_postprocessors} : {}$ \\
  2756 $\hbox{}\quad\textit{typ} \rightarrow \textit{term\_postprocessor} \rightarrow \textit{theory} \rightarrow \textit{theory}$ \\
  2757 $\textbf{val}\,~\textit{unregister\_term\_postprocessors} :\,
  2758 \textit{typ} \rightarrow \textit{theory} \rightarrow \textit{theory}$
  2759 \postw
  2760 
  2761 \S\ref{typedefs-quotient-types-records-rationals-and-reals} and
  2762 \texttt{src/HOL/Library/Multiset.thy} illustrate this feature in context.
  2763 
  2764 \section{Known Bugs and Limitations}
  2765 \label{known-bugs-and-limitations}
  2766 
  2767 Here are the known bugs and limitations in Nitpick at the time of writing:
  2768 
  2769 \begin{enum}
  2770 \item[$\bullet$] Underspecified functions defined using the \textbf{primrec},
  2771 \textbf{function}, or \textbf{nominal\_\allowbreak primrec} packages can lead
  2772 Nitpick to generate spurious counterexamples for theorems that refer to values
  2773 for which the function is not defined. For example:
  2774 
  2775 \prew
  2776 \textbf{primrec} \textit{prec} \textbf{where} \\
  2777 ``$\textit{prec}~(\textit{Suc}~n) = n$'' \\[2\smallskipamount]
  2778 \textbf{lemma} ``$\textit{prec}~0 = \undef$'' \\
  2779 \textbf{nitpick} \\[2\smallskipamount]
  2780 \quad{\slshape Nitpick found a counterexample for \textit{card nat}~= 2: 
  2781 \nopagebreak
  2782 \\[2\smallskipamount]
  2783 \hbox{}\qquad Empty assignment} \nopagebreak\\[2\smallskipamount]
  2784 \textbf{by}~(\textit{auto simp}:~\textit{prec\_def})
  2785 \postw
  2786 
  2787 Such theorems are considered bad style because they rely on the internal
  2788 representation of functions synthesized by Isabelle, which is an implementation
  2789 detail.
  2790 
  2791 \item[$\bullet$] Axioms that restrict the possible values of the
  2792 \textit{undefined} constant are in general ignored.
  2793 
  2794 \item[$\bullet$] Nitpick maintains a global cache of wellfoundedness conditions,
  2795 which can become invalid if you change the definition of an inductive predicate
  2796 that is registered in the cache. To clear the cache,
  2797 run Nitpick with the \textit{tac\_timeout} option set to a new value (e.g.,
  2798 501$\,\textit{ms}$).
  2799 
  2800 \item[$\bullet$] Nitpick produces spurious counterexamples when invoked after a
  2801 \textbf{guess} command in a structured proof.
  2802 
  2803 \item[$\bullet$] The \textit{nitpick\_} attributes and the
  2804 \textit{Nitpick.register\_} functions can cause havoc if used improperly.
  2805 
  2806 \item[$\bullet$] Although this has never been observed, arbitrary theorem
  2807 morphisms could possibly confuse Nitpick, resulting in spurious counterexamples.
  2808 
  2809 \item[$\bullet$] All constants, types, free variables, and schematic variables
  2810 whose names start with \textit{Nitpick}{.} are reserved for internal use.
  2811 \end{enum}
  2812 
  2813 \let\em=\sl
  2814 \bibliography{../manual}{}
  2815 \bibliographystyle{abbrv}
  2816 
  2817 \end{document}