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