doc-src/Nitpick/nitpick.tex
author wenzelm
Sun May 01 16:36:34 2011 +0200 (2011-05-01)
changeset 42511 bf89455ccf9d
parent 41993 bd6296de1432
child 42959 ee829022381d
permissions -rw-r--r--
eliminated copies of isabelle style files;
     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`\<midarrow\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: external prover ``$e$'' for subgoal 1: \\
   358 $\exists{!}x.\; P~x\,\Longrightarrow\, P~(\hbox{\slshape THE}~y.\; P~y)$ \\
   359 Try this command: \textrm{apply}~(\textit{metis~the\_equality})} \\[2\smallskipamount]
   360 \textbf{apply}~(\textit{metis~the\_equality\/}) \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\flushitem#1{\item[]\noindent\kern-\leftmargin \textbf{#1}}
  1840 \def\qty#1{$\left<\textit{#1}\right>$}
  1841 \def\qtybf#1{$\mathbf{\left<\textbf{\textit{#1}}\right>}$}
  1842 \def\optrue#1#2{\flushitem{\textit{#1} $\bigl[$= \qtybf{bool}$\bigr]$\quad [\textit{true}]\hfill (neg.: \textit{#2})}\nopagebreak\\[\parskip]}
  1843 \def\opfalse#1#2{\flushitem{\textit{#1} $\bigl[$= \qtybf{bool}$\bigr]$\quad [\textit{false}]\hfill (neg.: \textit{#2})}\nopagebreak\\[\parskip]}
  1844 \def\opsmart#1#2{\flushitem{\textit{#1} $\bigl[$= \qtybf{bool\_or\_smart}$\bigr]$\quad [\textit{smart}]\hfill (neg.: \textit{#2})}\nopagebreak\\[\parskip]}
  1845 \def\opnodefault#1#2{\flushitem{\textit{#1} = \qtybf{#2}} \nopagebreak\\[\parskip]}
  1846 \def\opdefault#1#2#3{\flushitem{\textit{#1} = \qtybf{#2}\quad [\textit{#3}]} \nopagebreak\\[\parskip]}
  1847 \def\oparg#1#2#3{\flushitem{\textit{#1} \qtybf{#2} = \qtybf{#3}} \nopagebreak\\[\parskip]}
  1848 \def\opargbool#1#2#3{\flushitem{\textit{#1} \qtybf{#2} $\bigl[$= \qtybf{bool}$\bigr]$\hfill (neg.: \textit{#3})}\nopagebreak\\[\parskip]}
  1849 \def\opargboolorsmart#1#2#3{\flushitem{\textit{#1} \qtybf{#2} $\bigl[$= \qtybf{bool\_or\_smart}$\bigr]$\hfill (neg.: \textit{#3})}\nopagebreak\\[\parskip]}
  1850 
  1851 Nitpick's behavior can be influenced by various options, which can be specified
  1852 in brackets after the \textbf{nitpick} command. Default values can be set
  1853 using \textbf{nitpick\_\allowbreak params}. For example:
  1854 
  1855 \prew
  1856 \textbf{nitpick\_params} [\textit{verbose}, \,\textit{timeout} = 60]
  1857 \postw
  1858 
  1859 The options are categorized as follows:\ mode of operation
  1860 (\S\ref{mode-of-operation}), scope of search (\S\ref{scope-of-search}), output
  1861 format (\S\ref{output-format}), automatic counterexample checks
  1862 (\S\ref{authentication}), optimizations
  1863 (\S\ref{optimizations}), and timeouts (\S\ref{timeouts}).
  1864 
  1865 You can instruct Nitpick to run automatically on newly entered theorems by
  1866 enabling the ``Auto Nitpick'' option from the ``Isabelle'' menu in Proof
  1867 General. For automatic runs, \textit{user\_axioms} (\S\ref{mode-of-operation}),
  1868 \textit{assms} (\S\ref{mode-of-operation}), and \textit{mono}
  1869 (\S\ref{scope-of-search}) are implicitly enabled, \textit{blocking}
  1870 (\S\ref{mode-of-operation}), \textit{verbose} (\S\ref{output-format}), and
  1871 \textit{debug} (\S\ref{output-format}) are disabled, \textit{max\_threads}
  1872 (\S\ref{optimizations}) is taken to be 1, \textit{max\_potential}
  1873 (\S\ref{output-format}) is taken to be 0, and \textit{timeout}
  1874 (\S\ref{timeouts}) is superseded by the ``Auto Tools Time Limit'' in
  1875 Proof General's ``Isabelle'' menu. Nitpick's output is also more concise.
  1876 
  1877 The number of options can be overwhelming at first glance. Do not let that worry
  1878 you: Nitpick's defaults have been chosen so that it almost always does the right
  1879 thing, and the most important options have been covered in context in
  1880 \S\ref{first-steps}.
  1881 
  1882 The descriptions below refer to the following syntactic quantities:
  1883 
  1884 \begin{enum}
  1885 \item[$\bullet$] \qtybf{string}: A string.
  1886 \item[$\bullet$] \qtybf{string\_list\/}: A space-separated list of strings
  1887 (e.g., ``\textit{ichi ni san}'').
  1888 \item[$\bullet$] \qtybf{bool\/}: \textit{true} or \textit{false}.
  1889 \item[$\bullet$] \qtybf{bool\_or\_smart\/}: \textit{true}, \textit{false}, or \textit{smart}.
  1890 \item[$\bullet$] \qtybf{int\/}: An integer. Negative integers are prefixed with a hyphen.
  1891 \item[$\bullet$] \qtybf{int\_or\_smart\/}: An integer or \textit{smart}.
  1892 \item[$\bullet$] \qtybf{int\_range}: An integer (e.g., 3) or a range
  1893 of nonnegative integers (e.g., $1$--$4$). The range symbol `--' can be entered as \texttt{-} (hyphen) or \texttt{\char`\\\char`\<midarrow\char`\>}.
  1894 \item[$\bullet$] \qtybf{int\_seq}: A comma-separated sequence of ranges of integers (e.g.,~1{,}3{,}\allowbreak6--8).
  1895 \item[$\bullet$] \qtybf{float\_or\_none}: An integer (e.g., 60) or floating-point number
  1896 (e.g., 0.5) expressing a number of seconds, or the keyword \textit{none}
  1897 ($\infty$ seconds).
  1898 \item[$\bullet$] \qtybf{const\/}: The name of a HOL constant.
  1899 \item[$\bullet$] \qtybf{term}: A HOL term (e.g., ``$f~x$'').
  1900 \item[$\bullet$] \qtybf{term\_list\/}: A space-separated list of HOL terms (e.g.,
  1901 ``$f~x$''~``$g~y$'').
  1902 \item[$\bullet$] \qtybf{type}: A HOL type.
  1903 \end{enum}
  1904 
  1905 Default values are indicated in square brackets. Boolean options have a negated
  1906 counterpart (e.g., \textit{blocking} vs.\ \textit{non\_blocking}). When setting
  1907 Boolean options, ``= \textit{true}'' may be omitted.
  1908 
  1909 \subsection{Mode of Operation}
  1910 \label{mode-of-operation}
  1911 
  1912 \begin{enum}
  1913 \optrue{blocking}{non\_blocking}
  1914 Specifies whether the \textbf{nitpick} command should operate synchronously.
  1915 The asynchronous (non-blocking) mode lets the user start proving the putative
  1916 theorem while Nitpick looks for a counterexample, but it can also be more
  1917 confusing. For technical reasons, automatic runs currently always block.
  1918 
  1919 \optrue{falsify}{satisfy}
  1920 Specifies whether Nitpick should look for falsifying examples (countermodels) or
  1921 satisfying examples (models). This manual assumes throughout that
  1922 \textit{falsify} is enabled.
  1923 
  1924 \opsmart{user\_axioms}{no\_user\_axioms}
  1925 Specifies whether the user-defined axioms (specified using 
  1926 \textbf{axiomatization} and \textbf{axioms}) should be considered. If the option
  1927 is set to \textit{smart}, Nitpick performs an ad hoc axiom selection based on
  1928 the constants that occur in the formula to falsify. The option is implicitly set
  1929 to \textit{true} for automatic runs.
  1930 
  1931 \textbf{Warning:} If the option is set to \textit{true}, Nitpick might
  1932 nonetheless ignore some polymorphic axioms. Counterexamples generated under
  1933 these conditions are tagged as ``quasi genuine.'' The \textit{debug}
  1934 (\S\ref{output-format}) option can be used to find out which axioms were
  1935 considered.
  1936 
  1937 \nopagebreak
  1938 {\small See also \textit{assms} (\S\ref{mode-of-operation}) and \textit{debug}
  1939 (\S\ref{output-format}).}
  1940 
  1941 \optrue{assms}{no\_assms}
  1942 Specifies whether the relevant assumptions in structured proofs should be
  1943 considered. The option is implicitly enabled for automatic runs.
  1944 
  1945 \nopagebreak
  1946 {\small See also \textit{user\_axioms} (\S\ref{mode-of-operation}).}
  1947 
  1948 \opfalse{overlord}{no\_overlord}
  1949 Specifies whether Nitpick should put its temporary files in
  1950 \texttt{\$ISABELLE\_\allowbreak HOME\_\allowbreak USER}, which is useful for
  1951 debugging Nitpick but also unsafe if several instances of the tool are run
  1952 simultaneously. The files are identified by the extensions
  1953 \texttt{.kki}, \texttt{.cnf}, \texttt{.out}, and
  1954 \texttt{.err}; you may safely remove them after Nitpick has run.
  1955 
  1956 \nopagebreak
  1957 {\small See also \textit{debug} (\S\ref{output-format}).}
  1958 \end{enum}
  1959 
  1960 \subsection{Scope of Search}
  1961 \label{scope-of-search}
  1962 
  1963 \begin{enum}
  1964 \oparg{card}{type}{int\_seq}
  1965 Specifies the sequence of cardinalities to use for a given type.
  1966 For free types, and often also for \textbf{typedecl}'d types, it usually makes
  1967 sense to specify cardinalities as a range of the form \textit{$1$--$n$}.
  1968 
  1969 \nopagebreak
  1970 {\small See also \textit{box} (\S\ref{scope-of-search}) and \textit{mono}
  1971 (\S\ref{scope-of-search}).}
  1972 
  1973 \opdefault{card}{int\_seq}{\upshape 1--10}
  1974 Specifies the default sequence of cardinalities to use. This can be overridden
  1975 on a per-type basis using the \textit{card}~\qty{type} option described above.
  1976 
  1977 \oparg{max}{const}{int\_seq}
  1978 Specifies the sequence of maximum multiplicities to use for a given
  1979 (co)in\-duc\-tive datatype constructor. A constructor's multiplicity is the
  1980 number of distinct values that it can construct. Nonsensical values (e.g.,
  1981 \textit{max}~[]~$=$~2) are silently repaired. This option is only available for
  1982 datatypes equipped with several constructors.
  1983 
  1984 \opnodefault{max}{int\_seq}
  1985 Specifies the default sequence of maximum multiplicities to use for
  1986 (co)in\-duc\-tive datatype constructors. This can be overridden on a per-constructor
  1987 basis using the \textit{max}~\qty{const} option described above.
  1988 
  1989 \opsmart{binary\_ints}{unary\_ints}
  1990 Specifies whether natural numbers and integers should be encoded using a unary
  1991 or binary notation. In unary mode, the cardinality fully specifies the subset
  1992 used to approximate the type. For example:
  1993 %
  1994 $$\hbox{\begin{tabular}{@{}rll@{}}%
  1995 \textit{card nat} = 4 & induces & $\{0,\, 1,\, 2,\, 3\}$ \\
  1996 \textit{card int} = 4 & induces & $\{-1,\, 0,\, +1,\, +2\}$ \\
  1997 \textit{card int} = 5 & induces & $\{-2,\, -1,\, 0,\, +1,\, +2\}.$%
  1998 \end{tabular}}$$
  1999 %
  2000 In general:
  2001 %
  2002 $$\hbox{\begin{tabular}{@{}rll@{}}%
  2003 \textit{card nat} = $K$ & induces & $\{0,\, \ldots,\, K - 1\}$ \\
  2004 \textit{card int} = $K$ & induces & $\{-\lceil K/2 \rceil + 1,\, \ldots,\, +\lfloor K/2 \rfloor\}.$%
  2005 \end{tabular}}$$
  2006 %
  2007 In binary mode, the cardinality specifies the number of distinct values that can
  2008 be constructed. Each of these value is represented by a bit pattern whose length
  2009 is specified by the \textit{bits} (\S\ref{scope-of-search}) option. By default,
  2010 Nitpick attempts to choose the more appropriate encoding by inspecting the
  2011 formula at hand, preferring the binary notation for problems involving
  2012 multiplicative operators or large constants.
  2013 
  2014 \textbf{Warning:} For technical reasons, Nitpick always reverts to unary for
  2015 problems that refer to the types \textit{rat} or \textit{real} or the constants
  2016 \textit{Suc}, \textit{gcd}, or \textit{lcm}.
  2017 
  2018 {\small See also \textit{bits} (\S\ref{scope-of-search}) and
  2019 \textit{show\_datatypes} (\S\ref{output-format}).}
  2020 
  2021 \opdefault{bits}{int\_seq}{\upshape 1,2,3,4,6,8,10,12,14,16}
  2022 Specifies the number of bits to use to represent natural numbers and integers in
  2023 binary, excluding the sign bit. The minimum is 1 and the maximum is 31.
  2024 
  2025 {\small See also \textit{binary\_ints} (\S\ref{scope-of-search}).}
  2026 
  2027 \opargboolorsmart{wf}{const}{non\_wf}
  2028 Specifies whether the specified (co)in\-duc\-tively defined predicate is
  2029 well-founded. The option can take the following values:
  2030 
  2031 \begin{enum}
  2032 \item[$\bullet$] \textbf{\textit{true}:} Tentatively treat the (co)in\-duc\-tive
  2033 predicate as if it were well-founded. Since this is generally not sound when the
  2034 predicate is not well-founded, the counterexamples are tagged as ``quasi
  2035 genuine.''
  2036 
  2037 \item[$\bullet$] \textbf{\textit{false}:} Treat the (co)in\-duc\-tive predicate
  2038 as if it were not well-founded. The predicate is then unrolled as prescribed by
  2039 the \textit{star\_linear\_preds}, \textit{iter}~\qty{const}, and \textit{iter}
  2040 options.
  2041 
  2042 \item[$\bullet$] \textbf{\textit{smart}:} Try to prove that the inductive
  2043 predicate is well-founded using Isabelle's \textit{lexicographic\_order} and
  2044 \textit{size\_change} tactics. If this succeeds (or the predicate occurs with an
  2045 appropriate polarity in the formula to falsify), use an efficient fixed-point
  2046 equation as specification of the predicate; otherwise, unroll the predicates
  2047 according to the \textit{iter}~\qty{const} and \textit{iter} options.
  2048 \end{enum}
  2049 
  2050 \nopagebreak
  2051 {\small See also \textit{iter} (\S\ref{scope-of-search}),
  2052 \textit{star\_linear\_preds} (\S\ref{optimizations}), and \textit{tac\_timeout}
  2053 (\S\ref{timeouts}).}
  2054 
  2055 \opsmart{wf}{non\_wf}
  2056 Specifies the default wellfoundedness setting to use. This can be overridden on
  2057 a per-predicate basis using the \textit{wf}~\qty{const} option above.
  2058 
  2059 \oparg{iter}{const}{int\_seq}
  2060 Specifies the sequence of iteration counts to use when unrolling a given
  2061 (co)in\-duc\-tive predicate. By default, unrolling is applied for inductive
  2062 predicates that occur negatively and coinductive predicates that occur
  2063 positively in the formula to falsify and that cannot be proved to be
  2064 well-founded, but this behavior is influenced by the \textit{wf} option. The
  2065 iteration counts are automatically bounded by the cardinality of the predicate's
  2066 domain.
  2067 
  2068 {\small See also \textit{wf} (\S\ref{scope-of-search}) and
  2069 \textit{star\_linear\_preds} (\S\ref{optimizations}).}
  2070 
  2071 \opdefault{iter}{int\_seq}{\upshape 0{,}1{,}2{,}4{,}8{,}12{,}16{,}20{,}24{,}28}
  2072 Specifies the sequence of iteration counts to use when unrolling (co)in\-duc\-tive
  2073 predicates. This can be overridden on a per-predicate basis using the
  2074 \textit{iter} \qty{const} option above.
  2075 
  2076 \opdefault{bisim\_depth}{int\_seq}{\upshape 9}
  2077 Specifies the sequence of iteration counts to use when unrolling the
  2078 bisimilarity predicate generated by Nitpick for coinductive datatypes. A value
  2079 of $-1$ means that no predicate is generated, in which case Nitpick performs an
  2080 after-the-fact check to see if the known coinductive datatype values are
  2081 bidissimilar. If two values are found to be bisimilar, the counterexample is
  2082 tagged as ``quasi genuine.'' The iteration counts are automatically bounded by
  2083 the sum of the cardinalities of the coinductive datatypes occurring in the
  2084 formula to falsify.
  2085 
  2086 \opargboolorsmart{box}{type}{dont\_box}
  2087 Specifies whether Nitpick should attempt to wrap (``box'') a given function or
  2088 product type in an isomorphic datatype internally. Boxing is an effective mean
  2089 to reduce the search space and speed up Nitpick, because the isomorphic datatype
  2090 is approximated by a subset of the possible function or pair values.
  2091 Like other drastic optimizations, it can also prevent the discovery of
  2092 counterexamples. The option can take the following values:
  2093 
  2094 \begin{enum}
  2095 \item[$\bullet$] \textbf{\textit{true}:} Box the specified type whenever
  2096 practicable.
  2097 \item[$\bullet$] \textbf{\textit{false}:} Never box the type.
  2098 \item[$\bullet$] \textbf{\textit{smart}:} Box the type only in contexts where it
  2099 is likely to help. For example, $n$-tuples where $n > 2$ and arguments to
  2100 higher-order functions are good candidates for boxing.
  2101 \end{enum}
  2102 
  2103 \nopagebreak
  2104 {\small See also \textit{finitize} (\S\ref{scope-of-search}), \textit{verbose}
  2105 (\S\ref{output-format}), and \textit{debug} (\S\ref{output-format}).}
  2106 
  2107 \opsmart{box}{dont\_box}
  2108 Specifies the default boxing setting to use. This can be overridden on a
  2109 per-type basis using the \textit{box}~\qty{type} option described above.
  2110 
  2111 \opargboolorsmart{finitize}{type}{dont\_finitize}
  2112 Specifies whether Nitpick should attempt to finitize an infinite datatype. The
  2113 option can then take the following values:
  2114 
  2115 \begin{enum}
  2116 \item[$\bullet$] \textbf{\textit{true}:} Finitize the datatype. Since this is
  2117 unsound, counterexamples generated under these conditions are tagged as ``quasi
  2118 genuine.''
  2119 \item[$\bullet$] \textbf{\textit{false}:} Don't attempt to finitize the datatype.
  2120 \item[$\bullet$] \textbf{\textit{smart}:}
  2121 If the datatype's constructors don't appear in the problem, perform a
  2122 monotonicity analysis to detect whether the datatype can be soundly finitized;
  2123 otherwise, don't finitize it.
  2124 \end{enum}
  2125 
  2126 \nopagebreak
  2127 {\small See also \textit{box} (\S\ref{scope-of-search}), \textit{mono}
  2128 (\S\ref{scope-of-search}), \textit{verbose} (\S\ref{output-format}), and
  2129 \textit{debug} (\S\ref{output-format}).}
  2130 
  2131 \opsmart{finitize}{dont\_finitize}
  2132 Specifies the default finitization setting to use. This can be overridden on a
  2133 per-type basis using the \textit{finitize}~\qty{type} option described above.
  2134 
  2135 \opargboolorsmart{mono}{type}{non\_mono}
  2136 Specifies whether the given type should be considered monotonic when enumerating
  2137 scopes and finitizing types. If the option is set to \textit{smart}, Nitpick
  2138 performs a monotonicity check on the type. Setting this option to \textit{true}
  2139 can reduce the number of scopes tried, but it can also diminish the chance of
  2140 finding a counterexample, as demonstrated in \S\ref{scope-monotonicity}. The
  2141 option is implicitly set to \textit{true} for automatic runs.
  2142 
  2143 \nopagebreak
  2144 {\small See also \textit{card} (\S\ref{scope-of-search}),
  2145 \textit{finitize} (\S\ref{scope-of-search}),
  2146 \textit{merge\_type\_vars} (\S\ref{scope-of-search}), and \textit{verbose}
  2147 (\S\ref{output-format}).}
  2148 
  2149 \opsmart{mono}{non\_mono}
  2150 Specifies the default monotonicity setting to use. This can be overridden on a
  2151 per-type basis using the \textit{mono}~\qty{type} option described above.
  2152 
  2153 \opfalse{merge\_type\_vars}{dont\_merge\_type\_vars}
  2154 Specifies whether type variables with the same sort constraints should be
  2155 merged. Setting this option to \textit{true} can reduce the number of scopes
  2156 tried and the size of the generated Kodkod formulas, but it also diminishes the
  2157 theoretical chance of finding a counterexample.
  2158 
  2159 {\small See also \textit{mono} (\S\ref{scope-of-search}).}
  2160 
  2161 \opargbool{std}{type}{non\_std}
  2162 Specifies whether the given (recursive) datatype should be given standard
  2163 models. Nonstandard models are unsound but can help debug structural induction
  2164 proofs, as explained in \S\ref{inductive-properties}.
  2165 
  2166 \optrue{std}{non\_std}
  2167 Specifies the default standardness to use. This can be overridden on a per-type
  2168 basis using the \textit{std}~\qty{type} option described above.
  2169 \end{enum}
  2170 
  2171 \subsection{Output Format}
  2172 \label{output-format}
  2173 
  2174 \begin{enum}
  2175 \opfalse{verbose}{quiet}
  2176 Specifies whether the \textbf{nitpick} command should explain what it does. This
  2177 option is useful to determine which scopes are tried or which SAT solver is
  2178 used. This option is implicitly disabled for automatic runs.
  2179 
  2180 \opfalse{debug}{no\_debug}
  2181 Specifies whether Nitpick should display additional debugging information beyond
  2182 what \textit{verbose} already displays. Enabling \textit{debug} also enables
  2183 \textit{verbose} and \textit{show\_all} behind the scenes. The \textit{debug}
  2184 option is implicitly disabled for automatic runs.
  2185 
  2186 \nopagebreak
  2187 {\small See also \textit{overlord} (\S\ref{mode-of-operation}) and
  2188 \textit{batch\_size} (\S\ref{optimizations}).}
  2189 
  2190 \opfalse{show\_datatypes}{hide\_datatypes}
  2191 Specifies whether the subsets used to approximate (co)in\-duc\-tive datatypes should
  2192 be displayed as part of counterexamples. Such subsets are sometimes helpful when
  2193 investigating whether a potentially spurious counterexample is genuine, but
  2194 their potential for clutter is real.
  2195 
  2196 \optrue{show\_skolems}{hide\_skolem}
  2197 Specifies whether the values of Skolem constants should be displayed as part of
  2198 counterexamples. Skolem constants correspond to bound variables in the original
  2199 formula and usually help us to understand why the counterexample falsifies the
  2200 formula.
  2201 
  2202 \opfalse{show\_consts}{hide\_consts}
  2203 Specifies whether the values of constants occurring in the formula (including
  2204 its axioms) should be displayed along with any counterexample. These values are
  2205 sometimes helpful when investigating why a counterexample is
  2206 genuine, but they can clutter the output.
  2207 
  2208 \opnodefault{show\_all}{bool}
  2209 Abbreviation for \textit{show\_datatypes}, \textit{show\_skolems}, and
  2210 \textit{show\_consts}.
  2211 
  2212 \opdefault{max\_potential}{int}{\upshape 1}
  2213 Specifies the maximum number of potentially spurious counterexamples to display.
  2214 Setting this option to 0 speeds up the search for a genuine counterexample. This
  2215 option is implicitly set to 0 for automatic runs. If you set this option to a
  2216 value greater than 1, you will need an incremental SAT solver, such as
  2217 \textit{MiniSat\_JNI} (recommended) and \textit{SAT4J}. Be aware that many of
  2218 the counterexamples may be identical.
  2219 
  2220 \nopagebreak
  2221 {\small See also \textit{check\_potential} (\S\ref{authentication}) and
  2222 \textit{sat\_solver} (\S\ref{optimizations}).}
  2223 
  2224 \opdefault{max\_genuine}{int}{\upshape 1}
  2225 Specifies the maximum number of genuine counterexamples to display. If you set
  2226 this option to a value greater than 1, you will need an incremental SAT solver,
  2227 such as \textit{MiniSat\_JNI} (recommended) and \textit{SAT4J}. Be aware that
  2228 many of the counterexamples may be identical.
  2229 
  2230 \nopagebreak
  2231 {\small See also \textit{check\_genuine} (\S\ref{authentication}) and
  2232 \textit{sat\_solver} (\S\ref{optimizations}).}
  2233 
  2234 \opnodefault{eval}{term\_list}
  2235 Specifies the list of terms whose values should be displayed along with
  2236 counterexamples. This option suffers from an ``observer effect'': Nitpick might
  2237 find different counterexamples for different values of this option.
  2238 
  2239 \oparg{atoms}{type}{string\_list}
  2240 Specifies the names to use to refer to the atoms of the given type. By default,
  2241 Nitpick generates names of the form $a_1, \ldots, a_n$, where $a$ is the first
  2242 letter of the type's name.
  2243 
  2244 \opnodefault{atoms}{string\_list}
  2245 Specifies the default names to use to refer to atoms of any type. For example,
  2246 to call the three atoms of type ${'}a$ \textit{ichi}, \textit{ni}, and
  2247 \textit{san} instead of $a_1$, $a_2$, $a_3$, specify the option
  2248 ``\textit{atoms}~${'}a$ = \textit{ichi~ni~san}''. The default names can be
  2249 overridden on a per-type basis using the \textit{atoms}~\qty{type} option
  2250 described above.
  2251 
  2252 \oparg{format}{term}{int\_seq}
  2253 Specifies how to uncurry the value displayed for a variable or constant.
  2254 Uncurrying sometimes increases the readability of the output for high-arity
  2255 functions. For example, given the variable $y \mathbin{\Colon} {'a}\Rightarrow
  2256 {'b}\Rightarrow {'c}\Rightarrow {'d}\Rightarrow {'e}\Rightarrow {'f}\Rightarrow
  2257 {'g}$, setting \textit{format}~$y$ = 3 tells Nitpick to group the last three
  2258 arguments, as if the type had been ${'a}\Rightarrow {'b}\Rightarrow
  2259 {'c}\Rightarrow {'d}\times {'e}\times {'f}\Rightarrow {'g}$. In general, a list
  2260 of values $n_1,\ldots,n_k$ tells Nitpick to show the last $n_k$ arguments as an
  2261 $n_k$-tuple, the previous $n_{k-1}$ arguments as an $n_{k-1}$-tuple, and so on;
  2262 arguments that are not accounted for are left alone, as if the specification had
  2263 been $1,\ldots,1,n_1,\ldots,n_k$.
  2264 
  2265 \opdefault{format}{int\_seq}{\upshape 1}
  2266 Specifies the default format to use. Irrespective of the default format, the
  2267 extra arguments to a Skolem constant corresponding to the outer bound variables
  2268 are kept separated from the remaining arguments, the \textbf{for} arguments of
  2269 an inductive definitions are kept separated from the remaining arguments, and
  2270 the iteration counter of an unrolled inductive definition is shown alone. The
  2271 default format can be overridden on a per-variable or per-constant basis using
  2272 the \textit{format}~\qty{term} option described above.
  2273 \end{enum}
  2274 
  2275 \subsection{Authentication}
  2276 \label{authentication}
  2277 
  2278 \begin{enum}
  2279 \opfalse{check\_potential}{trust\_potential}
  2280 Specifies whether potentially spurious counterexamples should be given to
  2281 Isabelle's \textit{auto} tactic to assess their validity. If a potentially
  2282 spurious counterexample is shown to be genuine, Nitpick displays a message to
  2283 this effect and terminates.
  2284 
  2285 \nopagebreak
  2286 {\small See also \textit{max\_potential} (\S\ref{output-format}).}
  2287 
  2288 \opfalse{check\_genuine}{trust\_genuine}
  2289 Specifies whether genuine and quasi genuine counterexamples should be given to
  2290 Isabelle's \textit{auto} tactic to assess their validity. If a ``genuine''
  2291 counterexample is shown to be spurious, the user is kindly asked to send a bug
  2292 report to the author at
  2293 \texttt{blan{\color{white}nospam}\kern-\wd\boxA{}chette@in.tum.de}.
  2294 
  2295 \nopagebreak
  2296 {\small See also \textit{max\_genuine} (\S\ref{output-format}).}
  2297 
  2298 \opnodefault{expect}{string}
  2299 Specifies the expected outcome, which must be one of the following:
  2300 
  2301 \begin{enum}
  2302 \item[$\bullet$] \textbf{\textit{genuine}:} Nitpick found a genuine counterexample.
  2303 \item[$\bullet$] \textbf{\textit{quasi\_genuine}:} Nitpick found a ``quasi
  2304 genuine'' counterexample (i.e., a counterexample that is genuine unless
  2305 it contradicts a missing axiom or a dangerous option was used inappropriately).
  2306 \item[$\bullet$] \textbf{\textit{potential}:} Nitpick found a potentially
  2307 spurious counterexample.
  2308 \item[$\bullet$] \textbf{\textit{none}:} Nitpick found no counterexample.
  2309 \item[$\bullet$] \textbf{\textit{unknown}:} Nitpick encountered some problem (e.g.,
  2310 Kodkod ran out of memory).
  2311 \end{enum}
  2312 
  2313 Nitpick emits an error if the actual outcome differs from the expected outcome.
  2314 This option is useful for regression testing.
  2315 \end{enum}
  2316 
  2317 \subsection{Optimizations}
  2318 \label{optimizations}
  2319 
  2320 \def\cpp{C\nobreak\raisebox{.1ex}{+}\nobreak\raisebox{.1ex}{+}}
  2321 
  2322 \sloppy
  2323 
  2324 \begin{enum}
  2325 \opdefault{sat\_solver}{string}{smart}
  2326 Specifies which SAT solver to use. SAT solvers implemented in C or \cpp{} tend
  2327 to be faster than their Java counterparts, but they can be more difficult to
  2328 install. Also, if you set the \textit{max\_potential} (\S\ref{output-format}) or
  2329 \textit{max\_genuine} (\S\ref{output-format}) option to a value greater than 1,
  2330 you will need an incremental SAT solver, such as \textit{MiniSat\_JNI}
  2331 (recommended) or \textit{SAT4J}.
  2332 
  2333 The supported solvers are listed below:
  2334 
  2335 \begin{enum}
  2336 
  2337 \item[$\bullet$] \textbf{\textit{MiniSat}:} MiniSat is an efficient solver
  2338 written in \cpp{}. To use MiniSat, set the environment variable
  2339 \texttt{MINISAT\_HOME} to the directory that contains the \texttt{minisat}
  2340 executable.%
  2341 \footnote{Important note for Cygwin users: The path must be specified using
  2342 native Windows syntax. Make sure to escape backslashes properly.%
  2343 \label{cygwin-paths}}
  2344 The \cpp{} sources and executables for MiniSat are available at
  2345 \url{http://minisat.se/MiniSat.html}. Nitpick has been tested with versions 1.14
  2346 and 2.0 beta (2007-07-21).
  2347 
  2348 \item[$\bullet$] \textbf{\textit{MiniSat\_JNI}:} The JNI (Java Native Interface)
  2349 version of MiniSat is bundled with Kodkodi and is precompiled for the major
  2350 platforms. It is also available from \texttt{native\-solver.\allowbreak tgz},
  2351 which you will find on Kodkod's web site \cite{kodkod-2009}. Unlike the standard
  2352 version of MiniSat, the JNI version can be used incrementally.
  2353 
  2354 \item[$\bullet$] \textbf{\textit{CryptoMiniSat}:} CryptoMiniSat is the winner of
  2355 the 2010 SAT Race. To use CryptoMiniSat, set the environment variable
  2356 \texttt{CRYPTO\-MINISAT\_}\discretionary{}{}{}\texttt{HOME} to the directory that contains the \texttt{crypto\-minisat}
  2357 executable.%
  2358 \footref{cygwin-paths}
  2359 The \cpp{} sources and executables for Crypto\-Mini\-Sat are available at
  2360 \url{http://planete.inrialpes.fr/~soos/}\allowbreak\url{CryptoMiniSat2/index.php}.
  2361 Nitpick has been tested with version 2.51.
  2362 
  2363 \item[$\bullet$] \textbf{\textit{PicoSAT}:} PicoSAT is an efficient solver
  2364 written in C. You can install a standard version of
  2365 PicoSAT and set the environment variable \texttt{PICOSAT\_HOME} to the directory
  2366 that contains the \texttt{picosat} executable.%
  2367 \footref{cygwin-paths}
  2368 The C sources for PicoSAT are
  2369 available at \url{http://fmv.jku.at/picosat/} and are also bundled with Kodkodi.
  2370 Nitpick has been tested with version 913.
  2371 
  2372 \item[$\bullet$] \textbf{\textit{zChaff}:} zChaff is an efficient solver written
  2373 in \cpp{}. To use zChaff, set the environment variable \texttt{ZCHAFF\_HOME} to
  2374 the directory that contains the \texttt{zchaff} executable.%
  2375 \footref{cygwin-paths}
  2376 The \cpp{} sources and executables for zChaff are available at
  2377 \url{http://www.princeton.edu/~chaff/zchaff.html}. Nitpick has been tested with
  2378 versions 2004-05-13, 2004-11-15, and 2007-03-12.
  2379 
  2380 \item[$\bullet$] \textbf{\textit{zChaff\_JNI}:} The JNI version of zChaff is
  2381 bundled with Kodkodi and is precompiled for the major
  2382 platforms. It is also available from \texttt{native\-solver.\allowbreak tgz},
  2383 which you will find on Kodkod's web site \cite{kodkod-2009}.
  2384 
  2385 \item[$\bullet$] \textbf{\textit{RSat}:} RSat is an efficient solver written in
  2386 \cpp{}. To use RSat, set the environment variable \texttt{RSAT\_HOME} to the
  2387 directory that contains the \texttt{rsat} executable.%
  2388 \footref{cygwin-paths}
  2389 The \cpp{} sources for RSat are available at
  2390 \url{http://reasoning.cs.ucla.edu/rsat/}. Nitpick has been tested with version
  2391 2.01.
  2392 
  2393 \item[$\bullet$] \textbf{\textit{BerkMin}:} BerkMin561 is an efficient solver
  2394 written in C. To use BerkMin, set the environment variable
  2395 \texttt{BERKMIN\_HOME} to the directory that contains the \texttt{BerkMin561}
  2396 executable.\footref{cygwin-paths}
  2397 The BerkMin executables are available at
  2398 \url{http://eigold.tripod.com/BerkMin.html}.
  2399 
  2400 \item[$\bullet$] \textbf{\textit{BerkMin\_Alloy}:} Variant of BerkMin that is
  2401 included with Alloy 4 and calls itself ``sat56'' in its banner text. To use this
  2402 version of BerkMin, set the environment variable
  2403 \texttt{BERKMINALLOY\_HOME} to the directory that contains the \texttt{berkmin}
  2404 executable.%
  2405 \footref{cygwin-paths}
  2406 
  2407 \item[$\bullet$] \textbf{\textit{Jerusat}:} Jerusat 1.3 is an efficient solver
  2408 written in C. To use Jerusat, set the environment variable
  2409 \texttt{JERUSAT\_HOME} to the directory that contains the \texttt{Jerusat1.3}
  2410 executable.%
  2411 \footref{cygwin-paths}
  2412 The C sources for Jerusat are available at
  2413 \url{http://www.cs.tau.ac.il/~ale1/Jerusat1.3.tgz}.
  2414 
  2415 \item[$\bullet$] \textbf{\textit{SAT4J}:} SAT4J is a reasonably efficient solver
  2416 written in Java that can be used incrementally. It is bundled with Kodkodi and
  2417 requires no further installation or configuration steps. Do not attempt to
  2418 install the official SAT4J packages, because their API is incompatible with
  2419 Kodkod.
  2420 
  2421 \item[$\bullet$] \textbf{\textit{SAT4J\_Light}:} Variant of SAT4J that is
  2422 optimized for small problems. It can also be used incrementally.
  2423 
  2424 \item[$\bullet$] \textbf{\textit{smart}:} If \textit{sat\_solver} is set to
  2425 \textit{smart}, Nitpick selects the first solver among the above that is
  2426 recognized by Isabelle. If \textit{verbose} (\S\ref{output-format}) is enabled,
  2427 Nitpick displays which SAT solver was chosen.
  2428 \end{enum}
  2429 \fussy
  2430 
  2431 \opdefault{batch\_size}{int\_or\_smart}{smart}
  2432 Specifies the maximum number of Kodkod problems that should be lumped together
  2433 when invoking Kodkodi. Each problem corresponds to one scope. Lumping problems
  2434 together ensures that Kodkodi is launched less often, but it makes the verbose
  2435 output less readable and is sometimes detrimental to performance. If
  2436 \textit{batch\_size} is set to \textit{smart}, the actual value used is 1 if
  2437 \textit{debug} (\S\ref{output-format}) is set and 50 otherwise.
  2438 
  2439 \optrue{destroy\_constrs}{dont\_destroy\_constrs}
  2440 Specifies whether formulas involving (co)in\-duc\-tive datatype constructors should
  2441 be rewritten to use (automatically generated) discriminators and destructors.
  2442 This optimization can drastically reduce the size of the Boolean formulas given
  2443 to the SAT solver.
  2444 
  2445 \nopagebreak
  2446 {\small See also \textit{debug} (\S\ref{output-format}).}
  2447 
  2448 \optrue{specialize}{dont\_specialize}
  2449 Specifies whether functions invoked with static arguments should be specialized.
  2450 This optimization can drastically reduce the search space, especially for
  2451 higher-order functions.
  2452 
  2453 \nopagebreak
  2454 {\small See also \textit{debug} (\S\ref{output-format}) and
  2455 \textit{show\_consts} (\S\ref{output-format}).}
  2456 
  2457 \optrue{star\_linear\_preds}{dont\_star\_linear\_preds}
  2458 Specifies whether Nitpick should use Kodkod's transitive closure operator to
  2459 encode non-well-founded ``linear inductive predicates,'' i.e., inductive
  2460 predicates for which each the predicate occurs in at most one assumption of each
  2461 introduction rule. Using the reflexive transitive closure is in principle
  2462 equivalent to setting \textit{iter} to the cardinality of the predicate's
  2463 domain, but it is usually more efficient.
  2464 
  2465 {\small See also \textit{wf} (\S\ref{scope-of-search}), \textit{debug}
  2466 (\S\ref{output-format}), and \textit{iter} (\S\ref{scope-of-search}).}
  2467 
  2468 {\small See also \textit{debug} (\S\ref{output-format}).}
  2469 
  2470 \opnodefault{whack}{term\_list}
  2471 Specifies a list of atomic terms (usually constants, but also free and schematic
  2472 variables) that should be taken as being $\unk$ (unknown). This can be useful to
  2473 reduce the size of the Kodkod problem if you can guess in advance that a
  2474 constant might not be needed to find a countermodel.
  2475 
  2476 {\small See also \textit{debug} (\S\ref{output-format}).}
  2477 
  2478 \opnodefault{need}{term\_list}
  2479 Specifies a list of datatype values (normally ground constructor terms) that
  2480 should be part of the subterm-closed subsets used to approximate datatypes. If
  2481 you know that a value must necessarily belong to the subset of representable
  2482 values that approximates a datatype, specifying it can speed up the search,
  2483 especially for high cardinalities.
  2484 %By default, Nitpick inspects the conjecture to infer needed datatype values.
  2485 
  2486 \opsmart{total\_consts}{partial\_consts}
  2487 Specifies whether constants occurring in the problem other than constructors can
  2488 be assumed to be considered total for the representable values that approximate
  2489 a datatype. This option is highly incomplete; it should be used only for
  2490 problems that do not construct datatype values explicitly. Since this option is
  2491 (in rare cases) unsound, counterexamples generated under these conditions are
  2492 tagged as ``quasi genuine.''
  2493 
  2494 \opdefault{datatype\_sym\_break}{int}{\upshape 5}
  2495 Specifies an upper bound on the number of datatypes for which Nitpick generates
  2496 symmetry breaking predicates. Symmetry breaking can speed up the SAT solver
  2497 considerably, especially for unsatisfiable problems, but too much of it can slow
  2498 it down.
  2499 
  2500 \opdefault{kodkod\_sym\_break}{int}{\upshape 15}
  2501 Specifies an upper bound on the number of relations for which Kodkod generates
  2502 symmetry breaking predicates. Symmetry breaking can speed up the SAT solver
  2503 considerably, especially for unsatisfiable problems, but too much of it can slow
  2504 it down.
  2505 
  2506 \optrue{peephole\_optim}{no\_peephole\_optim}
  2507 Specifies whether Nitpick should simplify the generated Kodkod formulas using a
  2508 peephole optimizer. These optimizations can make a significant difference.
  2509 Unless you are tracking down a bug in Nitpick or distrust the peephole
  2510 optimizer, you should leave this option enabled.
  2511 
  2512 \opdefault{max\_threads}{int}{\upshape 0}
  2513 Specifies the maximum number of threads to use in Kodkod. If this option is set
  2514 to 0, Kodkod will compute an appropriate value based on the number of processor
  2515 cores available. The option is implicitly set to 1 for automatic runs.
  2516 
  2517 \nopagebreak
  2518 {\small See also \textit{batch\_size} (\S\ref{optimizations}) and
  2519 \textit{timeout} (\S\ref{timeouts}).}
  2520 \end{enum}
  2521 
  2522 \subsection{Timeouts}
  2523 \label{timeouts}
  2524 
  2525 \begin{enum}
  2526 \opdefault{timeout}{float\_or\_none}{\upshape 30}
  2527 Specifies the maximum number of seconds that the \textbf{nitpick} command should
  2528 spend looking for a counterexample. Nitpick tries to honor this constraint as
  2529 well as it can but offers no guarantees. For automatic runs,
  2530 \textit{timeout} is ignored; instead, Auto Quickcheck and Auto Nitpick share
  2531 a time slot whose length is specified by the ``Auto Counterexample Time
  2532 Limit'' option in Proof General.
  2533 
  2534 \nopagebreak
  2535 {\small See also \textit{max\_threads} (\S\ref{optimizations}).}
  2536 
  2537 \opdefault{tac\_timeout}{float\_or\_none}{\upshape 0.5}
  2538 Specifies the maximum number of seconds that the \textit{auto} tactic should use
  2539 when checking a counterexample, and similarly that \textit{lexicographic\_order}
  2540 and \textit{size\_change} should use when checking whether a (co)in\-duc\-tive
  2541 predicate is well-founded. Nitpick tries to honor this constraint as well as it
  2542 can but offers no guarantees.
  2543 
  2544 \nopagebreak
  2545 {\small See also \textit{wf} (\S\ref{scope-of-search}),
  2546 \textit{check\_potential} (\S\ref{authentication}),
  2547 and \textit{check\_genuine} (\S\ref{authentication}).}
  2548 \end{enum}
  2549 
  2550 \section{Attribute Reference}
  2551 \label{attribute-reference}
  2552 
  2553 Nitpick needs to consider the definitions of all constants occurring in a
  2554 formula in order to falsify it. For constants introduced using the
  2555 \textbf{definition} command, the definition is simply the associated
  2556 \textit{\_def} axiom. In contrast, instead of using the internal representation
  2557 of functions synthesized by Isabelle's \textbf{primrec}, \textbf{function}, and
  2558 \textbf{nominal\_primrec} packages, Nitpick relies on the more natural
  2559 equational specification entered by the user.
  2560 
  2561 Behind the scenes, Isabelle's built-in packages and theories rely on the
  2562 following attributes to affect Nitpick's behavior:
  2563 
  2564 \begin{enum}
  2565 \flushitem{\textit{nitpick\_unfold}}
  2566 
  2567 \nopagebreak
  2568 This attribute specifies an equation that Nitpick should use to expand a
  2569 constant. The equation should be logically equivalent to the constant's actual
  2570 definition and should be of the form
  2571 
  2572 \qquad $c~{?}x_1~\ldots~{?}x_n \,=\, t$,
  2573 
  2574 or
  2575 
  2576 \qquad $c~{?}x_1~\ldots~{?}x_n \,\equiv\, t$,
  2577 
  2578 where ${?}x_1, \ldots, {?}x_n$ are distinct variables and $c$ does not occur in
  2579 $t$. Each occurrence of $c$ in the problem is expanded to $\lambda x_1\,\ldots
  2580 x_n.\; t$.
  2581 
  2582 \flushitem{\textit{nitpick\_simp}}
  2583 
  2584 \nopagebreak
  2585 This attribute specifies the equations that constitute the specification of a
  2586 constant. The \textbf{primrec}, \textbf{function}, and
  2587 \textbf{nominal\_\allowbreak primrec} packages automatically attach this
  2588 attribute to their \textit{simps} rules. The equations must be of the form
  2589 
  2590 \qquad $c~t_1~\ldots\ t_n \;\bigl[{=}\; u\bigr]$
  2591 
  2592 or
  2593 
  2594 \qquad $c~t_1~\ldots\ t_n \,\equiv\, u.$
  2595 
  2596 \flushitem{\textit{nitpick\_psimp}}
  2597 
  2598 \nopagebreak
  2599 This attribute specifies the equations that constitute the partial specification
  2600 of a constant. The \textbf{function} package automatically attaches this
  2601 attribute to its \textit{psimps} rules. The conditional equations must be of the
  2602 form
  2603 
  2604 \qquad $\lbrakk P_1;\> \ldots;\> P_m\rbrakk \,\Longrightarrow\, c\ t_1\ \ldots\ t_n \;\bigl[{=}\; u\bigr]$
  2605 
  2606 or
  2607 
  2608 \qquad $\lbrakk P_1;\> \ldots;\> P_m\rbrakk \,\Longrightarrow\, c\ t_1\ \ldots\ t_n \,\equiv\, u$.
  2609 
  2610 \flushitem{\textit{nitpick\_choice\_spec}}
  2611 
  2612 \nopagebreak
  2613 This attribute specifies the (free-form) specification of a constant defined
  2614 using the \hbox{(\textbf{ax\_})}\allowbreak\textbf{specification} command.
  2615 \end{enum}
  2616 
  2617 When faced with a constant, Nitpick proceeds as follows:
  2618 
  2619 \begin{enum}
  2620 \item[1.] If the \textit{nitpick\_simp} set associated with the constant
  2621 is not empty, Nitpick uses these rules as the specification of the constant.
  2622 
  2623 \item[2.] Otherwise, if the \textit{nitpick\_psimp} set associated with
  2624 the constant is not empty, it uses these rules as the specification of the
  2625 constant.
  2626 
  2627 \item[3.] Otherwise, if the constant was defined using the
  2628 \hbox{(\textbf{ax\_})}\allowbreak\textbf{specification} command and the
  2629 \textit{nitpick\_choice\_spec} set associated with the constant is not empty, it
  2630 uses these theorems as the specification of the constant.
  2631 
  2632 \item[4.] Otherwise, it looks up the definition of the constant. If the
  2633 \textit{nitpick\_unfold} set associated with the constant is not empty, it uses
  2634 the latest rule added to the set as the definition of the constant; otherwise it
  2635 uses the actual definition axiom.
  2636 
  2637 \begin{enum}
  2638 \item[1.] If the definition is of the form
  2639 
  2640 \qquad $c~{?}x_1~\ldots~{?}x_m \,\equiv\, \lambda y_1~\ldots~y_n.\; \textit{lfp}~(\lambda f.\; t)$
  2641 
  2642 or
  2643 
  2644 \qquad $c~{?}x_1~\ldots~{?}x_m \,\equiv\, \lambda y_1~\ldots~y_n.\; \textit{gfp}~(\lambda f.\; t).$
  2645 
  2646 Nitpick assumes that the definition was made using a (co)inductive package
  2647 based on the user-specified introduction rules registered in Isabelle's internal
  2648 \textit{Spec\_Rules} table. The tool uses the introduction rules to ascertain
  2649 whether the definition is well-founded and the definition to generate a
  2650 fixed-point equation or an unrolled equation.
  2651 
  2652 \item[2.] If the definition is compact enough, the constant is \textsl{unfolded}
  2653 wherever it appears; otherwise, it is defined equationally, as with
  2654 the \textit{nitpick\_simp} attribute.
  2655 \end{enum}
  2656 \end{enum}
  2657 
  2658 As an illustration, consider the inductive definition
  2659 
  2660 \prew
  2661 \textbf{inductive}~\textit{odd}~\textbf{where} \\
  2662 ``\textit{odd}~1'' $\,\mid$ \\
  2663 ``\textit{odd}~$n\,\Longrightarrow\, \textit{odd}~(\textit{Suc}~(\textit{Suc}~n))$''
  2664 \postw
  2665 
  2666 By default, Nitpick uses the \textit{lfp}-based definition in conjunction with
  2667 the introduction rules. To override this, you can specify an alternative
  2668 definition as follows:
  2669 
  2670 \prew
  2671 \textbf{lemma} $\mathit{odd\_alt\_unfold}$ [\textit{nitpick\_unfold}]:\kern.4em ``$\textit{odd}~n \,\equiv\, n~\textrm{mod}~2 = 1$''
  2672 \postw
  2673 
  2674 Nitpick then expands all occurrences of $\mathit{odd}~n$ to $n~\textrm{mod}~2
  2675 = 1$. Alternatively, you can specify an equational specification of the constant:
  2676 
  2677 \prew
  2678 \textbf{lemma} $\mathit{odd\_simp}$ [\textit{nitpick\_simp}]:\kern.4em ``$\textit{odd}~n = (n~\textrm{mod}~2 = 1)$''
  2679 \postw
  2680 
  2681 Such tweaks should be done with great care, because Nitpick will assume that the
  2682 constant is completely defined by its equational specification. For example, if
  2683 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
  2684 $\textit{odd}~n$ arbitrarily for even values of $n$. The \textit{debug}
  2685 (\S\ref{output-format}) option is extremely useful to understand what is going
  2686 on when experimenting with \textit{nitpick\_} attributes.
  2687 
  2688 Because of its internal three-valued logic, Nitpick tends to lose a
  2689 lot of precision in the presence of partially specified constants. For example,
  2690 
  2691 \prew
  2692 \textbf{lemma} \textit{odd\_simp} [\textit{nitpick\_simp}]:\kern.4em ``$\textit{odd~x} = \lnot\, \textit{even}~x$''
  2693 \postw
  2694 
  2695 is superior to
  2696 
  2697 \prew
  2698 \textbf{lemma} \textit{odd\_psimps} [\textit{nitpick\_simp}]: \\
  2699 ``$\textit{even~x} \,\Longrightarrow\, \textit{odd~x} = \textit{False\/}$'' \\
  2700 ``$\lnot\, \textit{even~x} \,\Longrightarrow\, \textit{odd~x} = \textit{True\/}$''
  2701 \postw
  2702 
  2703 Because Nitpick sometimes unfolds definitions but never simplification rules,
  2704 you can ensure that a constant is defined explicitly using the
  2705 \textit{nitpick\_simp}. For example:
  2706 
  2707 \prew
  2708 \textbf{definition}~\textit{optimum} \textbf{where} [\textit{nitpick\_simp}]: \\
  2709 ``$\textit{optimum}~t =
  2710      (\forall u.\; \textit{consistent}~u \mathrel{\land} \textit{alphabet}~t = \textit{alphabet}~u$ \\
  2711 \phantom{``$\textit{optimum}~t = (\forall u.\;$}${\mathrel{\land}}\; \textit{freq}~t = \textit{freq}~u \longrightarrow
  2712          \textit{cost}~t \le \textit{cost}~u)$''
  2713 \postw
  2714 
  2715 In some rare occasions, you might want to provide an inductive or coinductive
  2716 view on top of an existing constant $c$. The easiest way to achieve this is to
  2717 define a new constant $c'$ (co)inductively. Then prove that $c$ equals $c'$
  2718 and let Nitpick know about it:
  2719 
  2720 \prew
  2721 \textbf{lemma} \textit{c\_alt\_unfold} [\textit{nitpick\_unfold}]:\kern.4em ``$c \equiv c'$\kern2pt ''
  2722 \postw
  2723 
  2724 This ensures that Nitpick will substitute $c'$ for $c$ and use the (co)inductive
  2725 definition.
  2726 
  2727 \section{Standard ML Interface}
  2728 \label{standard-ml-interface}
  2729 
  2730 Nitpick provides a rich Standard ML interface used mainly for internal purposes
  2731 and debugging. Among the most interesting functions exported by Nitpick are
  2732 those that let you invoke the tool programmatically and those that let you
  2733 register and unregister custom coinductive datatypes as well as term
  2734 postprocessors.
  2735 
  2736 \subsection{Invocation of Nitpick}
  2737 \label{invocation-of-nitpick}
  2738 
  2739 The \textit{Nitpick} structure offers the following functions for invoking your
  2740 favorite counterexample generator:
  2741 
  2742 \prew
  2743 $\textbf{val}\,~\textit{pick\_nits\_in\_term} : \\
  2744 \hbox{}\quad\textit{Proof.state} \rightarrow \textit{params} \rightarrow \textit{bool} \rightarrow \textit{term~list} \rightarrow \textit{term} \\
  2745 \hbox{}\quad{\rightarrow}\; \textit{string} * \textit{Proof.state}$ \\
  2746 $\textbf{val}\,~\textit{pick\_nits\_in\_subgoal} : \\
  2747 \hbox{}\quad\textit{Proof.state} \rightarrow \textit{params} \rightarrow \textit{bool} \rightarrow \textit{int} \rightarrow \textit{string} * \textit{Proof.state}$
  2748 \postw
  2749 
  2750 The return value is a new proof state paired with an outcome string
  2751 (``genuine'', ``quasi\_genuine'', ``potential'', ``none'', or ``unknown''). The
  2752 \textit{params} type is a large record that lets you set Nitpick's options. The
  2753 current default options can be retrieved by calling the following function
  2754 defined in the \textit{Nitpick\_Isar} structure:
  2755 
  2756 \prew
  2757 $\textbf{val}\,~\textit{default\_params} :\,
  2758 \textit{theory} \rightarrow (\textit{string} * \textit{string})~\textit{list} \rightarrow \textit{params}$
  2759 \postw
  2760 
  2761 The second argument lets you override option values before they are parsed and
  2762 put into a \textit{params} record. Here is an example:
  2763 
  2764 \prew
  2765 $\textbf{val}\,~\textit{params} = \textit{Nitpick\_Isar.default\_params}~\textit{thy}~[(\textrm{``}\textrm{timeout\/}\textrm{''},\, \textrm{``}\textrm{none}\textrm{''})]$ \\
  2766 $\textbf{val}\,~(\textit{outcome},\, \textit{state}') = \textit{Nitpick.pick\_nits\_in\_subgoal}~\begin{aligned}[t]
  2767 & \textit{state}~\textit{params}~\textit{false} \\[-2pt]
  2768 & \textit{subgoal}\end{aligned}$
  2769 \postw
  2770 
  2771 \let\antiq=\textrm
  2772 
  2773 \subsection{Registration of Coinductive Datatypes}
  2774 \label{registration-of-coinductive-datatypes}
  2775 
  2776 If you have defined a custom coinductive datatype, you can tell Nitpick about
  2777 it, so that it can use an efficient Kodkod axiomatization similar to the one it
  2778 uses for lazy lists. The interface for registering and unregistering coinductive
  2779 datatypes consists of the following pair of functions defined in the
  2780 \textit{Nitpick\_HOL} structure:
  2781 
  2782 \prew
  2783 $\textbf{val}\,~\textit{register\_codatatype\/} : {}$ \\
  2784 $\hbox{}\quad\textit{morphism} \rightarrow \textit{typ} \rightarrow \textit{string} \rightarrow (\textit{string} \times \textit{typ})\;\textit{list} \rightarrow \textit{Context.generic} {}$ \\
  2785 $\hbox{}\quad{\rightarrow}\; \textit{Context.generic}$ \\
  2786 $\textbf{val}\,~\textit{unregister\_codatatype\/} : {}$ \\
  2787 $\hbox{}\quad\textit{morphism} \rightarrow \textit{typ} \rightarrow \textit{Context.generic} \rightarrow \textit{Context.generic} {}$
  2788 \postw
  2789 
  2790 The type $'a~\textit{llist}$ of lazy lists is already registered; had it
  2791 not been, you could have told Nitpick about it by adding the following line
  2792 to your theory file:
  2793 
  2794 \prew
  2795 $\textbf{declaration}~\,\{{*}$ \\
  2796 $\hbox{}\quad\textit{Nitpick\_HOL.register\_codatatype}~@\{\antiq{typ}~``\kern1pt'a~\textit{llist\/}\textrm{''}\}$ \\
  2797 $\hbox{}\qquad\quad @\{\antiq{const\_name}~ \textit{llist\_case}\}$ \\
  2798 $\hbox{}\qquad\quad (\textit{map}~\textit{dest\_Const}~[@\{\antiq{term}~\textit{LNil}\},\, @\{\antiq{term}~\textit{LCons}\}])$ \\
  2799 ${*}\}$
  2800 \postw
  2801 
  2802 The \textit{register\_codatatype} function takes a coinductive datatype, its
  2803 case function, and the list of its constructors (in addition to the current
  2804 morphism and generic proof context). The case function must take its arguments
  2805 in the order that the constructors are listed. If no case function with the
  2806 correct signature is available, simply pass the empty string.
  2807 
  2808 On the other hand, if your goal is to cripple Nitpick, add the following line to
  2809 your theory file and try to check a few conjectures about lazy lists:
  2810 
  2811 \prew
  2812 $\textbf{declaration}~\,\{{*}$ \\
  2813 $\hbox{}\quad\textit{Nitpick\_HOL.unregister\_codatatype}~@\{\antiq{typ}~``\kern1pt'a~\textit{llist\/}\textrm{''}\}$ \\
  2814 ${*}\}$
  2815 \postw
  2816 
  2817 Inductive datatypes can be registered as coinductive datatypes, given
  2818 appropriate coinductive constructors. However, doing so precludes
  2819 the use of the inductive constructors---Nitpick will generate an error if they
  2820 are needed.
  2821 
  2822 \subsection{Registration of Term Postprocessors}
  2823 \label{registration-of-term-postprocessors}
  2824 
  2825 It is possible to change the output of any term that Nitpick considers a
  2826 datatype by registering a term postprocessor. The interface for registering and
  2827 unregistering postprocessors consists of the following pair of functions defined
  2828 in the \textit{Nitpick\_Model} structure:
  2829 
  2830 \prew
  2831 $\textbf{type}\,~\textit{term\_postprocessor}\,~{=} {}$ \\
  2832 $\hbox{}\quad\textit{Proof.context} \rightarrow \textit{string} \rightarrow (\textit{typ} \rightarrow \textit{term~list\/}) \rightarrow \textit{typ} \rightarrow \textit{term} \rightarrow \textit{term}$ \\
  2833 $\textbf{val}\,~\textit{register\_term\_postprocessor} : {}$ \\
  2834 $\hbox{}\quad\textit{typ} \rightarrow \textit{term\_postprocessor} \rightarrow \textit{morphism} \rightarrow \textit{Context.generic}$ \\
  2835 $\hbox{}\quad{\rightarrow}\; \textit{Context.generic}$ \\
  2836 $\textbf{val}\,~\textit{unregister\_term\_postprocessor} : {}$ \\
  2837 $\hbox{}\quad\textit{typ} \rightarrow \textit{morphism} \rightarrow \textit{Context.generic} \rightarrow \textit{Context.generic}$
  2838 \postw
  2839 
  2840 \S\ref{typedefs-quotient-types-records-rationals-and-reals} and
  2841 \texttt{src/HOL/Library/Multiset.thy} illustrate this feature in context.
  2842 
  2843 \section{Known Bugs and Limitations}
  2844 \label{known-bugs-and-limitations}
  2845 
  2846 Here are the known bugs and limitations in Nitpick at the time of writing:
  2847 
  2848 \begin{enum}
  2849 \item[$\bullet$] Underspecified functions defined using the \textbf{primrec},
  2850 \textbf{function}, or \textbf{nominal\_\allowbreak primrec} packages can lead
  2851 Nitpick to generate spurious counterexamples for theorems that refer to values
  2852 for which the function is not defined. For example:
  2853 
  2854 \prew
  2855 \textbf{primrec} \textit{prec} \textbf{where} \\
  2856 ``$\textit{prec}~(\textit{Suc}~n) = n$'' \\[2\smallskipamount]
  2857 \textbf{lemma} ``$\textit{prec}~0 = \undef$'' \\
  2858 \textbf{nitpick} \\[2\smallskipamount]
  2859 \quad{\slshape Nitpick found a counterexample for \textit{card nat}~= 2: 
  2860 \nopagebreak
  2861 \\[2\smallskipamount]
  2862 \hbox{}\qquad Empty assignment} \nopagebreak\\[2\smallskipamount]
  2863 \textbf{by}~(\textit{auto simp}:~\textit{prec\_def})
  2864 \postw
  2865 
  2866 Such theorems are generally considered bad style because they rely on the
  2867 internal representation of functions synthesized by Isabelle, an implementation
  2868 detail.
  2869 
  2870 \item[$\bullet$] Similarly, Nitpick might find spurious counterexamples for
  2871 theorems that rely on the use of the indefinite description operator internally
  2872 by \textbf{specification} and \textbf{quot\_type}.
  2873 
  2874 \item[$\bullet$] Axioms or definitions that restrict the possible values of the
  2875 \textit{undefined} constant or other partially specified built-in Isabelle
  2876 constants (e.g., \textit{Abs\_} and \textit{Rep\_} constants) are in general
  2877 ignored. Again, such nonconservative extensions are generally considered bad
  2878 style.
  2879 
  2880 \item[$\bullet$] Nitpick maintains a global cache of wellfoundedness conditions,
  2881 which can become invalid if you change the definition of an inductive predicate
  2882 that is registered in the cache. To clear the cache,
  2883 run Nitpick with the \textit{tac\_timeout} option set to a new value (e.g.,
  2884 $0.51$).
  2885 
  2886 \item[$\bullet$] Nitpick produces spurious counterexamples when invoked after a
  2887 \textbf{guess} command in a structured proof.
  2888 
  2889 \item[$\bullet$] The \textit{nitpick\_xxx} attributes and the
  2890 \textit{Nitpick\_xxx.register\_yyy} functions can cause havoc if used
  2891 improperly.
  2892 
  2893 \item[$\bullet$] Although this has never been observed, arbitrary theorem
  2894 morphisms could possibly confuse Nitpick, resulting in spurious counterexamples.
  2895 
  2896 \item[$\bullet$] All constants, types, free variables, and schematic variables
  2897 whose names start with \textit{Nitpick}{.} are reserved for internal use.
  2898 \end{enum}
  2899 
  2900 \let\em=\sl
  2901 \bibliography{../manual}{}
  2902 \bibliographystyle{abbrv}
  2903 
  2904 \end{document}