doc-src/Nitpick/nitpick.tex
 changeset 33191 fe3c65d9c577 child 33193 6f6baa3ef4dd
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Nitpick/nitpick.tex	Thu Oct 22 14:45:20 2009 +0200
@@ -0,0 +1,2484 @@
+\documentclass[a4paper,12pt]{article}
+\usepackage[T1]{fontenc}
+\usepackage{amsmath}
+\usepackage{amssymb}
+\usepackage[french,english]{babel}
+\usepackage{color}
+\usepackage{graphicx}
+%\usepackage{mathpazo}
+\usepackage{multicol}
+\usepackage{stmaryrd}
+%\usepackage[scaled=.85]{beramono}
+\usepackage{../iman,../pdfsetup}
+
+%\oddsidemargin=4.6mm
+%\evensidemargin=4.6mm
+%\textwidth=150mm
+%\topmargin=4.6mm
+%\headheight=0mm
+%\headsep=0mm
+%\textheight=234mm
+
+\def\Colon{\mathord{:\mkern-1.5mu:}}
+%\def\lbrakk{\mathopen{\lbrack\mkern-3.25mu\lbrack}}
+%\def\rbrakk{\mathclose{\rbrack\mkern-3.255mu\rbrack}}
+\def\lparr{\mathopen{(\mkern-4mu\mid}}
+\def\rparr{\mathclose{\mid\mkern-4mu)}}
+
+\def\undef{\textit{undefined}}
+\def\unk{{?}}
+%\def\unr{\textit{others}}
+\def\unr{\ldots}
+\def\Abs#1{\hbox{\rm{\flqq}}{\,#1\,}\hbox{\rm{\frqq}}}
+\def\Q{{\smash{\lower.2ex\hbox{$\scriptstyle?$}}}}
+
+\hyphenation{Mini-Sat size-change First-Steps grand-parent nit-pick
+counter-example counter-examples data-type data-types co-data-type
+co-data-types in-duc-tive co-in-duc-tive}
+
+\urlstyle{tt}
+
+\begin{document}
+
+\title{\includegraphics[scale=0.5]{isabelle_nitpick} \\[4ex]
+Picking Nits \\[\smallskipamount]
+\Large A User's Guide to Nitpick for Isabelle/HOL 2010}
+\author{\hbox{} \\
+Jasmin Christian Blanchette \\
+{\normalsize Fakult\"at f\"ur Informatik, Technische Universit\"at M\"unchen} \\
+\hbox{}}
+
+\maketitle
+
+\tableofcontents
+
+\setlength{\parskip}{.7em plus .2em minus .1em}
+\setlength{\parindent}{0pt}
+\setlength{\abovedisplayskip}{\parskip}
+\setlength{\abovedisplayshortskip}{.9\parskip}
+\setlength{\belowdisplayskip}{\parskip}
+\setlength{\belowdisplayshortskip}{.9\parskip}
+
+% General-purpose enum environment with correct spacing
+\newenvironment{enum}%
+    {\begin{list}{}{%
+        \setlength{\topsep}{.1\parskip}%
+        \setlength{\partopsep}{.1\parskip}%
+        \setlength{\itemsep}{\parskip}%
+        \advance\itemsep by-\parsep}}
+    {\end{list}}
+
+\def\pre{\begingroup\vskip0pt plus1ex\advance\leftskip by\leftmargin
+\advance\rightskip by\leftmargin}
+\def\post{\vskip0pt plus1ex\endgroup}
+
+\def\prew{\pre\advance\rightskip by-\leftmargin}
+\def\postw{\post}
+
+\section{Introduction}
+\label{introduction}
+
+Nitpick \cite{blanchette-nipkow-2009} is a counterexample generator for
+Isabelle/HOL \cite{isa-tutorial} that is designed to handle formulas
+combining (co)in\-duc\-tive datatypes, (co)in\-duc\-tively defined predicates, and
+quantifiers. It builds on Kodkod \cite{torlak-jackson-2007}, a highly optimized
+first-order relational model finder developed by the Software Design Group at
+MIT. It is conceptually similar to Refute \cite{weber-2008}, from which it
+borrows many ideas and code fragments, but it benefits from Kodkod's
+optimizations and a new encoding scheme. The name Nitpick is shamelessly
+appropriated from a now retired Alloy precursor.
+
+Nitpick is easy to use---you simply enter \textbf{nitpick} after a putative
+theorem and wait a few seconds. Nonetheless, there are situations where knowing
+how it works under the hood and how it reacts to various options helps
+increase the test coverage. This manual also explains how to install the tool on
+your workstation. Should the motivation fail you, think of the many hours of
+hard work Nitpick will save you. Proving non-theorems is \textsl{hard work}.
+
+Another common use of Nitpick is to find out whether the axioms of a locale are
+satisfiable, while the locale is being developed. To check this, it suffices to
+write
+
+\prew
+\textbf{lemma}~$\textit{False}$'' \\
+\textbf{nitpick}~[\textit{show\_all}]
+\postw
+
+after the locale's \textbf{begin} keyword. To falsify \textit{False}, Nitpick
+must find a model for the axioms. If it finds no model, we have an indication
+that the axioms might be unsatisfiable.
+
+\newbox\boxA
+\setbox\boxA=\hbox{\texttt{nospam}}
+
+The known bugs and limitations at the time of writing are listed in
+\S\ref{known-bugs-and-limitations}. Comments and bug reports concerning Nitpick
+or this manual should be directed to
+\texttt{blan{\color{white}nospam}\kern-\wd\boxA{}chette@\allowbreak
+in.\allowbreak tum.\allowbreak de}.
+
+\vskip2.5\smallskipamount
+
+\textbf{Acknowledgment.} The author would like to thank Mark Summerfield for
+suggesting several textual improvements.
+% and Perry James for reporting a typo.
+
+\section{First Steps}
+\label{first-steps}
+
+This section introduces Nitpick by presenting small examples. If possible, you
+should try out the examples on your workstation. Your theory file should start
+the standard way:
+
+\prew
+\textbf{theory}~\textit{Scratch} \\
+\textbf{imports}~\textit{Main} \\
+\textbf{begin}
+\postw
+
+The results presented here were obtained using the JNI version of MiniSat and
+with multithreading disabled to reduce nondeterminism. This was done by adding
+the line
+
+\prew
+\textbf{nitpick\_params} [\textit{sat\_solver}~= \textit{MiniSatJNI}, \,\textit{max\_threads}~= 1]
+\postw
+
+after the \textbf{begin} keyword. The JNI version of MiniSat is bundled with
+Kodkodi and is precompiled for the major platforms. Other SAT solvers can also
+be installed, as explained in \S\ref{optimizations}. If you have already
+configured SAT solvers in Isabelle (e.g., for Refute), these will also be
+available to Nitpick.
+
+Throughout this manual, we will explicitly invoke the \textbf{nitpick} command.
+Nitpick also provides an automatic mode that can be enabled by specifying
+
+\prew
+\textbf{nitpick\_params} [\textit{auto}]
+\postw
+
+at the beginning of the theory file. In this mode, Nitpick is run for up to 5
+seconds (by default) on every newly entered theorem, much like Auto Quickcheck.
+
+\subsection{Propositional Logic}
+\label{propositional-logic}
+
+Let's start with a trivial example from propositional logic:
+
+\prew
+\textbf{lemma}~$P \longleftrightarrow Q$'' \\
+\textbf{nitpick}
+\postw
+
+You should get the following output:
+
+\prew
+\slshape
+Nitpick found a counterexample: \\[2\smallskipamount]
+\hbox{}\qquad Free variables: \nopagebreak \\
+\hbox{}\qquad\qquad $P = \textit{True}$ \\
+\hbox{}\qquad\qquad $Q = \textit{False}$
+\postw
+
+Nitpick can also be invoked on individual subgoals, as in the example below:
+
+\prew
+\textbf{apply}~\textit{auto} \\[2\smallskipamount]
+{\slshape goal (2 subgoals): \\
+\ 1. $P\,\Longrightarrow\, Q$ \\
+\ 2. $Q\,\Longrightarrow\, P$} \\[2\smallskipamount]
+\textbf{nitpick}~1 \\[2\smallskipamount]
+{\slshape Nitpick found a counterexample: \\[2\smallskipamount]
+\hbox{}\qquad Free variables: \nopagebreak \\
+\hbox{}\qquad\qquad $P = \textit{True}$ \\
+\hbox{}\qquad\qquad $Q = \textit{False}$} \\[2\smallskipamount]
+\textbf{nitpick}~2 \\[2\smallskipamount]
+{\slshape Nitpick found a counterexample: \\[2\smallskipamount]
+\hbox{}\qquad Free variables: \nopagebreak \\
+\hbox{}\qquad\qquad $P = \textit{False}$ \\
+\hbox{}\qquad\qquad $Q = \textit{True}$} \\[2\smallskipamount]
+\textbf{oops}
+\postw
+
+\subsection{Type Variables}
+\label{type-variables}
+
+If you are left unimpressed by the previous example, don't worry. The next
+one is more mind- and computer-boggling:
+
+\prew
+\textbf{lemma} $P~x\,\Longrightarrow\, P~(\textrm{THE}~y.\;P~y)$''
+\postw
+\pagebreak[2] %% TYPESETTING
+
+The putative lemma involves the definite description operator, {THE}, presented
+in section 5.10.1 of the Isabelle tutorial \cite{isa-tutorial}. The
+operator is defined by the axiom $(\textrm{THE}~x.\; x = a) = a$. The putative
+lemma is merely asserting the indefinite description operator axiom with {THE}
+substituted for {SOME}.
+
+The free variable $x$ and the bound variable $y$ have type $'a$. For formulas
+containing type variables, Nitpick enumerates the possible domains for each type
+variable, up to a given cardinality (8 by default), looking for a finite
+countermodel:
+
+\prew
+\textbf{nitpick} [\textit{verbose}] \\[2\smallskipamount]
+\slshape
+Trying 8 scopes: \nopagebreak \\
+\hbox{}\qquad \textit{card}~$'a$~= 1; \\
+\hbox{}\qquad \textit{card}~$'a$~= 2; \\
+\hbox{}\qquad $\qquad\vdots$ \\[.5\smallskipamount]
+\hbox{}\qquad \textit{card}~$'a$~= 8. \\[2\smallskipamount]
+Nitpick found a counterexample for \textit{card} $'a$~= 3: \\[2\smallskipamount]
+\hbox{}\qquad Free variables: \nopagebreak \\
+\hbox{}\qquad\qquad $P = \{a_2,\, a_3\}$ \\
+\hbox{}\qquad\qquad $x = a_3$ \\[2\smallskipamount]
+Total time: 580 ms.
+\postw
+
+Nitpick found a counterexample in which $'a$ has cardinality 3. (For
+cardinalities 1 and 2, the formula holds.) In the counterexample, the three
+values of type $'a$ are written $a_1$, $a_2$, and $a_3$.
+
+The message Trying $n$ scopes: {\ldots}''\ is shown only if the option
+\textit{verbose} is enabled. You can specify \textit{verbose} each time you
+invoke \textbf{nitpick}, or you can set it globally using the command
+
+\prew
+\textbf{nitpick\_params} [\textit{verbose}]
+\postw
+
+This command also displays the current default values for all of the options
+supported by Nitpick. The options are listed in \S\ref{option-reference}.
+
+\subsection{Constants}
+\label{constants}
+
+By just looking at Nitpick's output, it might not be clear why the
+counterexample in \S\ref{type-variables} is genuine. Let's invoke Nitpick again,
+this time telling it to show the values of the constants that occur in the
+formula:
+
+\prew
+\textbf{lemma}~$P~x\,\Longrightarrow\, P~(\textrm{THE}~y.\;P~y)$'' \\
+\textbf{nitpick}~[\textit{show\_consts}] \\[2\smallskipamount]
+\slshape
+Nitpick found a counterexample for \textit{card} $'a$~= 3: \\[2\smallskipamount]
+\hbox{}\qquad Free variables: \nopagebreak \\
+\hbox{}\qquad\qquad $P = \{a_2,\, a_3\}$ \\
+\hbox{}\qquad\qquad $x = a_3$ \\
+\hbox{}\qquad Constant: \nopagebreak \\
+\hbox{}\qquad\qquad $\textit{The}~\textsl{fallback} = a_1$
+\postw
+
+We can see more clearly now. Since the predicate $P$ isn't true for a unique
+value, $\textrm{THE}~y.\;P~y$ can denote any value of type $'a$, even
+$a_1$. Since $P~a_1$ is false, the entire formula is falsified.
+
+As an optimization, Nitpick's preprocessor introduced the special constant
+\textit{The} fallback'' corresponding to $\textrm{THE}~y.\;P~y$ (i.e.,
+$\mathit{The}~(\lambda y.\;P~y)$) when there doesn't exist a unique $y$
+satisfying $P~y$. We disable this optimization by passing the
+\textit{full\_descrs} option:
+
+\prew
+\textbf{nitpick}~[\textit{full\_descrs},\, \textit{show\_consts}] \\[2\smallskipamount]
+\slshape
+Nitpick found a counterexample for \textit{card} $'a$~= 3: \\[2\smallskipamount]
+\hbox{}\qquad Free variables: \nopagebreak \\
+\hbox{}\qquad\qquad $P = \{a_2,\, a_3\}$ \\
+\hbox{}\qquad\qquad $x = a_3$ \\
+\hbox{}\qquad Constant: \nopagebreak \\
+\hbox{}\qquad\qquad $\hbox{\slshape THE}~y.\;P~y = a_1$
+\postw
+
+As the result of another optimization, Nitpick directly assigned a value to the
+subterm $\textrm{THE}~y.\;P~y$, rather than to the \textit{The} constant. If we
+disable this second optimization by using the command
+
+\prew
+\textbf{nitpick}~[\textit{dont\_specialize},\, \textit{full\_descrs},\,
+\textit{show\_consts}]
+\postw
+
+we finally get \textit{The}:
+
+\prew
+\slshape Constant: \nopagebreak \\
+\hbox{}\qquad \mathit{The} = \undef{} + (\!\begin{aligned}[t]% + & \{\} := a_3,\> \{a_3\} := a_3,\> \{a_2\} := a_2, \\[-2pt] %% TYPESETTING + & \{a_2, a_3\} := a_1,\> \{a_1\} := a_1,\> \{a_1, a_3\} := a_3, \\[-2pt] + & \{a_1, a_2\} := a_3,\> \{a_1, a_2, a_3\} := a_3)\end{aligned}
+\postw
+
+Notice that $\textit{The}~(\lambda y.\;P~y) = \textit{The}~\{a_2, a_3\} = a_1$,
+just like before.\footnote{The \undef{} symbol's presence is explained as
+follows: In higher-order logic, any function can be built from the undefined
+function using repeated applications of the function update operator $f(x := +y)$, just like any list can be built from the empty list using $x \mathbin{\#} +xs$.}
+
+Our misadventures with THE suggest adding $\exists!x{.}$' (there exists a
+unique $x$ such that'') at the front of our putative lemma's assumption:
+
+\prew
+\textbf{lemma}~$\exists {!}x.\; P~x\,\Longrightarrow\, P~(\textrm{THE}~y.\;P~y)$''
+\postw
+
+The fix appears to work:
+
+\prew
+\textbf{nitpick} \\[2\smallskipamount]
+\slshape Nitpick found no counterexample.
+\postw
+
+We can further increase our confidence in the formula by exhausting all
+cardinalities up to 50:
+
+\prew
+\textbf{nitpick} [\textit{card} $'a$~= 1--50]\footnote{The symbol --'
+can be entered as \texttt{-} (hyphen) or
+\texttt{\char\\\char\<midarrow\char\>}.} \\[2\smallskipamount]
+\slshape Nitpick found no counterexample.
+\postw
+
+Let's see if Sledgehammer \cite{sledgehammer-2009} can find a proof:
+
+\prew
+\textbf{sledgehammer} \\[2\smallskipamount]
+{\slshape Sledgehammer: external prover $e$'' for subgoal 1: \\
+$\exists{!}x.\; P~x\,\Longrightarrow\, P~(\hbox{\slshape THE}~y.\; P~y)$ \\
+Try this command: \textrm{apply}~(\textit{metis~the\_equality})} \\[2\smallskipamount]
+\textbf{apply}~(\textit{metis~the\_equality\/}) \nopagebreak \\[2\smallskipamount]
+{\slshape No subgoals!}% \\[2\smallskipamount]
+%\textbf{done}
+\postw
+
+This must be our lucky day.
+
+\subsection{Skolemization}
+\label{skolemization}
+
+Are all invertible functions onto? Let's find out:
+
+\prew
+\textbf{lemma} $\exists g.\; \forall x.~g~(f~x) = x + \,\Longrightarrow\, \forall y.\; \exists x.~y = f~x$'' \\
+\textbf{nitpick} \\[2\smallskipamount]
+\slshape
+Nitpick found a counterexample for \textit{card} $'a$~= 2 and \textit{card} $'b$~=~1: \\[2\smallskipamount]
+\hbox{}\qquad Free variable: \nopagebreak \\
+\hbox{}\qquad\qquad $f = \undef{}(b_1 := a_1)$ \\
+\hbox{}\qquad Skolem constants: \nopagebreak \\
+\hbox{}\qquad\qquad $g = \undef{}(a_1 := b_1,\> a_2 := b_1)$ \\
+\hbox{}\qquad\qquad $y = a_2$
+\postw
+
+Although $f$ is the only free variable occurring in the formula, Nitpick also
+displays values for the bound variables $g$ and $y$. These values are available
+to Nitpick because it performs skolemization as a preprocessing step.
+
+In the previous example, skolemization only affected the outermost quantifiers.
+This is not always the case, as illustrated below:
+
+\prew
+\textbf{lemma} $\exists x.\; \forall f.\; f~x = x$'' \\
+\textbf{nitpick} \\[2\smallskipamount]
+\slshape
+Nitpick found a counterexample for \textit{card} $'a$~= 2: \\[2\smallskipamount]
+\hbox{}\qquad Skolem constant: \nopagebreak \\
+\hbox{}\qquad\qquad \lambda x.\; f = + \undef{}(\!\begin{aligned}[t] + & a_1 := \undef{}(a_1 := a_2,\> a_2 := a_1), \\[-2pt] + & a_2 := \undef{}(a_1 := a_1,\> a_2 := a_1))\end{aligned}
+\postw
+
+The variable $f$ is bound within the scope of $x$; therefore, $f$ depends on
+$x$, as suggested by the notation $\lambda x.\,f$. If $x = a_1$, then $f$ is the
+function that maps $a_1$ to $a_2$ and vice versa; otherwise, $x = a_2$ and $f$
+maps both $a_1$ and $a_2$ to $a_1$. In both cases, $f~x \not= x$.
+
+The source of the Skolem constants is sometimes more obscure:
+
+\prew
+\textbf{lemma} $\mathit{refl}~r\,\Longrightarrow\, \mathit{sym}~r$'' \\
+\textbf{nitpick} \\[2\smallskipamount]
+\slshape
+Nitpick found a counterexample for \textit{card} $'a$~= 2: \\[2\smallskipamount]
+\hbox{}\qquad Free variable: \nopagebreak \\
+\hbox{}\qquad\qquad $r = \{(a_1, a_1),\, (a_2, a_1),\, (a_2, a_2)\}$ \\
+\hbox{}\qquad Skolem constants: \nopagebreak \\
+\hbox{}\qquad\qquad $\mathit{sym}.x = a_2$ \\
+\hbox{}\qquad\qquad $\mathit{sym}.y = a_1$
+\postw
+
+What happened here is that Nitpick expanded the \textit{sym} constant to its
+definition:
+
+\prew
+$\mathit{sym}~r \,\equiv\, + \forall x\> y.\,\> (x, y) \in r \longrightarrow (y, x) \in r.$
+\postw
+
+As their names suggest, the Skolem constants $\mathit{sym}.x$ and
+$\mathit{sym}.y$ are simply the bound variables $x$ and $y$
+from \textit{sym}'s definition.
+
+Although skolemization is a useful optimization, you can disable it by invoking
+Nitpick with \textit{dont\_skolemize}. See \S\ref{optimizations} for details.
+
+\subsection{Natural Numbers and Integers}
+\label{natural-numbers-and-integers}
+
+Because of the axiom of infinity, the type \textit{nat} does not admit any
+finite models. To deal with this, Nitpick considers prefixes $\{0,\, 1,\, +\ldots,\, K - 1\}$ of \textit{nat} (where $K = \textit{card}~\textit{nat}$) and
+maps all other numbers to the undefined value ($\unk$). The type \textit{int} is
+handled in a similar way: If $K = \textit{card}~\textit{int}$, the subset of
+\textit{int} known to Nitpick is $\{-\lceil K/2 \rceil + 1,\, \ldots,\, +\lfloor +K/2 \rfloor\}$. Undefined values lead to a three-valued logic.
+
+Here is an example involving \textit{int}:
+
+\prew
+\textbf{lemma} $\lbrakk i \le j;\> n \le (m{\Colon}\mathit{int})\rbrakk \,\Longrightarrow\, i * n + j * m \le i * m + j * n$'' \\
+\textbf{nitpick} \\[2\smallskipamount]
+\slshape Nitpick found a counterexample: \\[2\smallskipamount]
+\hbox{}\qquad Free variables: \nopagebreak \\
+\hbox{}\qquad\qquad $i = 0$ \\
+\hbox{}\qquad\qquad $j = 1$ \\
+\hbox{}\qquad\qquad $m = 1$ \\
+\hbox{}\qquad\qquad $n = 0$
+\postw
+
+With infinite types, we don't always have the luxury of a genuine counterexample
+and must often content ourselves with a potential one. The tedious task of
+finding out whether the potential counterexample is in fact genuine can be
+outsourced to \textit{auto} by passing the option \textit{check\_potential}. For
+example:
+
+\prew
+\textbf{lemma} $\forall n.\; \textit{Suc}~n \mathbin{\not=} n \,\Longrightarrow\, P$'' \\
+\textbf{nitpick} [\textit{card~nat}~= 100,\, \textit{check\_potential}] \\[2\smallskipamount]
+\slshape Nitpick found a potential counterexample: \\[2\smallskipamount]
+\hbox{}\qquad Free variable: \nopagebreak \\
+\hbox{}\qquad\qquad $P = \textit{False}$ \\[2\smallskipamount]
+Confirmation by \textit{auto}'': The above counterexample is genuine.
+\postw
+
+You might wonder why the counterexample is first reported as potential. The root
+of the problem is that the bound variable in $\forall n.\; \textit{Suc}~n +\mathbin{\not=} n$ ranges over an infinite type. If Nitpick finds an $n$ such
+that $\textit{Suc}~n \mathbin{=} n$, it evaluates the assumption to
+\textit{False}; but otherwise, it does not know anything about values of $n \ge +\textit{card~nat}$ and must therefore evaluate the assumption to $\unk$, not
+\textit{True}. Since the assumption can never be satisfied, the putative lemma
+can never be falsified.
+
+Incidentally, if you distrust the so-called genuine counterexamples, you can
+enable \textit{check\_\allowbreak genuine} to verify them as well. However, be
+aware that \textit{auto} will often fail to prove that the counterexample is
+genuine or spurious.
+
+Some conjectures involving elementary number theory make Nitpick look like a
+giant with feet of clay:
+
+\prew
+\textbf{lemma} $P~\textit{Suc}$'' \\
+\textbf{nitpick} [\textit{card} = 1--6] \\[2\smallskipamount]
+\slshape
+Nitpick found no counterexample.
+\postw
+
+For any cardinality $k$, \textit{Suc} is the partial function $\{0 \mapsto 1,\, +1 \mapsto 2,\, \ldots,\, k - 1 \mapsto \unk\}$, which evaluates to $\unk$ when
+it is passed as argument to $P$. As a result, $P~\textit{Suc}$ is always $\unk$.
+The next example is similar:
+
+\prew
+\textbf{lemma} $P~(\textit{op}~{+}\Colon +\textit{nat}\mathbin{\Rightarrow}\textit{nat}\mathbin{\Rightarrow}\textit{nat})$'' \\
+\textbf{nitpick} [\textit{card nat} = 1] \\[2\smallskipamount]
+{\slshape Nitpick found a counterexample:} \\[2\smallskipamount]
+\hbox{}\qquad Free variable: \nopagebreak \\
+\hbox{}\qquad\qquad $P = \{\}$ \\[2\smallskipamount]
+\textbf{nitpick} [\textit{card nat} = 2] \\[2\smallskipamount]
+{\slshape Nitpick found no counterexample.}
+\postw
+
+The problem here is that \textit{op}~+ is total when \textit{nat} is taken to be
+$\{0\}$ but becomes partial as soon as we add $1$, because $1 + 1 \notin \{0, +1\}$.
+
+Because numbers are infinite and are approximated using a three-valued logic,
+there is usually no need to systematically enumerate domain sizes. If Nitpick
+cannot find a genuine counterexample for \textit{card~nat}~= $k$, it is very
+unlikely that one could be found for smaller domains. (The $P~(\textit{op}~{+})$
+example above is an exception to this principle.) Nitpick nonetheless enumerates
+all cardinalities from 1 to 8 for \textit{nat}, mainly because smaller
+cardinalities are fast to handle and give rise to simpler counterexamples. This
+is explained in more detail in \S\ref{scope-monotonicity}.
+
+\subsection{Inductive Datatypes}
+\label{inductive-datatypes}
+
+Like natural numbers and integers, inductive datatypes with recursive
+constructors admit no finite models and must be approximated by a subterm-closed
+subset. For example, using a cardinality of 10 for ${'}a~\textit{list}$,
+Nitpick looks for all counterexamples that can be built using at most 10
+different lists.
+
+Let's see with an example involving \textit{hd} (which returns the first element
+of a list) and $@$ (which concatenates two lists):
+
+\prew
+\textbf{lemma} $\textit{hd}~(\textit{xs} \mathbin{@} [y, y]) = \textit{hd}~\textit{xs}$'' \\
+\textbf{nitpick} \\[2\smallskipamount]
+\slshape Nitpick found a counterexample for \textit{card} $'a$~= 3: \\[2\smallskipamount]
+\hbox{}\qquad Free variables: \nopagebreak \\
+\hbox{}\qquad\qquad $\textit{xs} = []$ \\
+\hbox{}\qquad\qquad $\textit{y} = a_3$
+\postw
+
+To see why the counterexample is genuine, we enable \textit{show\_consts}
+and \textit{show\_\allowbreak datatypes}:
+
+\prew
+{\slshape Datatype:} \\
+\hbox{}\qquad $'a$~\textit{list}~= $\{[],\, [a_3, a_3],\, [a_3],\, \unr\}$ \\
+{\slshape Constants:} \\
+\hbox{}\qquad $\lambda x_1.\; x_1 \mathbin{@} [y, y] = \undef([] := [a_3, a_3],\> [a_3, a_3] := \unk,\> [a_3] := \unk)$ \\
+\hbox{}\qquad $\textit{hd} = \undef([] := a_2,\> [a_3, a_3] := a_3,\> [a_3] := a_3)$
+\postw
+
+Since $\mathit{hd}~[]$ is undefined in the logic, it may be given any value,
+including $a_2$.
+
+The second constant, $\lambda x_1.\; x_1 \mathbin{@} [y, y]$, is simply the
+append operator whose second argument is fixed to be $[y, y]$. Appending $[a_3, +a_3]$ to $[a_3]$ would normally give $[a_3, a_3, a_3]$, but this value is not
+representable in the subset of $'a$~\textit{list} considered by Nitpick, which
+is shown under the Datatype'' heading; hence the result is $\unk$. Similarly,
+appending $[a_3, a_3]$ to itself gives $\unk$.
+
+Given \textit{card}~$'a = 3$ and \textit{card}~$'a~\textit{list} = 3$, Nitpick
+considers the following subsets:
+
+\kern-.5\smallskipamount %% TYPESETTING
+
+\prew
+\begin{multicols}{3}
+$\{[],\, [a_1],\, [a_2]\}$; \\
+$\{[],\, [a_1],\, [a_3]\}$; \\
+$\{[],\, [a_2],\, [a_3]\}$; \\
+$\{[],\, [a_1],\, [a_1, a_1]\}$; \\
+$\{[],\, [a_1],\, [a_2, a_1]\}$; \\
+$\{[],\, [a_1],\, [a_3, a_1]\}$; \\
+$\{[],\, [a_2],\, [a_1, a_2]\}$; \\
+$\{[],\, [a_2],\, [a_2, a_2]\}$; \\
+$\{[],\, [a_2],\, [a_3, a_2]\}$; \\
+$\{[],\, [a_3],\, [a_1, a_3]\}$; \\
+$\{[],\, [a_3],\, [a_2, a_3]\}$; \\
+$\{[],\, [a_3],\, [a_3, a_3]\}$.
+\end{multicols}
+\postw
+
+\kern-2\smallskipamount %% TYPESETTING
+
+All subterm-closed subsets of $'a~\textit{list}$ consisting of three values
+are listed and only those. As an example of a non-subterm-closed subset,
+consider $\mathcal{S} = \{[],\, [a_1],\,\allowbreak [a_1, a_3]\}$, and observe
+that $[a_1, a_3]$ (i.e., $a_1 \mathbin{\#} [a_3]$) has $[a_3] \notin +\mathcal{S}$ as a subterm.
+
+Here's another m\"ochtegern-lemma that Nitpick can refute without a blink:
+
+\prew
+\textbf{lemma} $\lbrakk \textit{length}~\textit{xs} = 1;\> \textit{length}~\textit{ys} = 1 +\rbrakk \,\Longrightarrow\, \textit{xs} = \textit{ys}$''
+\\
+\textbf{nitpick} [\textit{show\_datatypes}] \\[2\smallskipamount]
+\slshape Nitpick found a counterexample for \textit{card} $'a$~= 3: \\[2\smallskipamount]
+\hbox{}\qquad Free variables: \nopagebreak \\
+\hbox{}\qquad\qquad $\textit{xs} = [a_2]$ \\
+\hbox{}\qquad\qquad $\textit{ys} = [a_3]$ \\
+\hbox{}\qquad Datatypes: \\
+\hbox{}\qquad\qquad $\textit{nat} = \{0,\, 1,\, 2,\, \unr\}$ \\
+\hbox{}\qquad\qquad $'a$~\textit{list} = $\{[],\, [a_3],\, [a_2],\, \unr\}$
+\postw
+
+Because datatypes are approximated using a three-valued logic, there is usually
+no need to systematically enumerate cardinalities: If Nitpick cannot find a
+genuine counterexample for \textit{card}~$'a~\textit{list}$~= 10, it is very
+unlikely that one could be found for smaller cardinalities.
+
+\subsection{Typedefs, Records, Rationals, and Reals}
+\label{typedefs-records-rationals-and-reals}
+
+Nitpick generally treats types declared using \textbf{typedef} as datatypes
+whose single constructor is the corresponding \textit{Abs\_\kern.1ex} function.
+For example:
+
+\prew
+\textbf{typedef}~\textit{three} = $\{0\Colon\textit{nat},\, 1,\, 2\}$'' \\
+\textbf{by}~\textit{blast} \\[2\smallskipamount]
+\textbf{definition}~$A \mathbin{\Colon} \textit{three}$ \textbf{where} \kern-.1em$A \,\equiv\, \textit{Abs\_\allowbreak three}~0$'' \\
+\textbf{definition}~$B \mathbin{\Colon} \textit{three}$ \textbf{where} $B \,\equiv\, \textit{Abs\_three}~1$'' \\
+\textbf{definition}~$C \mathbin{\Colon} \textit{three}$ \textbf{where} $C \,\equiv\, \textit{Abs\_three}~2$'' \\[2\smallskipamount]
+\textbf{lemma} $\lbrakk P~A;\> P~B\rbrakk \,\Longrightarrow\, P~x$'' \\
+\textbf{nitpick} [\textit{show\_datatypes}] \\[2\smallskipamount]
+\slshape Nitpick found a counterexample: \\[2\smallskipamount]
+\hbox{}\qquad Free variables: \nopagebreak \\
+\hbox{}\qquad\qquad $P = \{\Abs{1},\, \Abs{0}\}$ \\
+\hbox{}\qquad\qquad $x = \Abs{2}$ \\
+\hbox{}\qquad Datatypes: \\
+\hbox{}\qquad\qquad $\textit{nat} = \{0,\, 1,\, 2,\, \unr\}$ \\
+\hbox{}\qquad\qquad $\textit{three} = \{\Abs{2},\, \Abs{1},\, \Abs{0},\, \unr\}$
+\postw
+
+%% MARK
+In the output above, $\Abs{n}$ abbreviates $\textit{Abs\_three}~n$.
+
+%% MARK
+Records, which are implemented as \textbf{typedef}s behind the scenes, are
+handled in much the same way:
+
+\prew
+\textbf{record} \textit{point} = \\
+\hbox{}\quad $\textit{Xcoord} \mathbin{\Colon} \textit{int}$ \\
+\hbox{}\quad $\textit{Ycoord} \mathbin{\Colon} \textit{int}$ \\[2\smallskipamount]
+\textbf{lemma} $\textit{Xcoord}~(p\Colon\textit{point}) = \textit{Xcoord}~(q\Colon\textit{point})$'' \\
+\textbf{nitpick} [\textit{show\_datatypes}] \\[2\smallskipamount]
+\slshape Nitpick found a counterexample: \\[2\smallskipamount]
+\hbox{}\qquad Free variables: \nopagebreak \\
+\hbox{}\qquad\qquad $p = \lparr\textit{Xcoord} = 0,\> \textit{Ycoord} = 0\rparr$ \\
+\hbox{}\qquad\qquad $q = \lparr\textit{Xcoord} = 1,\> \textit{Ycoord} = 1\rparr$ \\
+\hbox{}\qquad Datatypes: \\
+\hbox{}\qquad\qquad $\textit{int} = \{0,\, 1,\, \unr\}$ \\
+\hbox{}\qquad\qquad $\textit{point} = \{\lparr\textit{Xcoord} = 1,\> +\textit{Ycoord} = 1\rparr,\> \lparr\textit{Xcoord} = 0,\> \textit{Ycoord} = 0\rparr,\, \unr\}$\kern-1pt %% QUIET
+\postw
+
+Finally, Nitpick provides rudimentary support for rationals and reals using a
+similar approach:
+
+\prew
+\textbf{lemma} $4 * x + 3 * (y\Colon\textit{real}) \not= 1/2$'' \\
+\textbf{nitpick} [\textit{show\_datatypes}] \\[2\smallskipamount]
+\slshape Nitpick found a counterexample: \\[2\smallskipamount]
+\hbox{}\qquad Free variables: \nopagebreak \\
+\hbox{}\qquad\qquad $x = 1/2$ \\
+\hbox{}\qquad\qquad $y = -1/2$ \\
+\hbox{}\qquad Datatypes: \\
+\hbox{}\qquad\qquad $\textit{nat} = \{0,\, 1,\, 2,\, 3,\, 4,\, 5,\, 6,\, 7,\, \unr\}$ \\
+\hbox{}\qquad\qquad $\textit{int} = \{0,\, 1,\, 2,\, 3,\, 4,\, -3,\, -2,\, -1,\, \unr\}$ \\
+\hbox{}\qquad\qquad $\textit{real} = \{1,\, 0,\, 4,\, -3/2,\, 3,\, 2,\, 1/2,\, -1/2,\, \unr\}$
+\postw
+
+\subsection{Inductive and Coinductive Predicates}
+\label{inductive-and-coinductive-predicates}
+
+Inductively defined predicates (and sets) are particularly problematic for
+counterexample generators. They can make Quickcheck~\cite{berghofer-nipkow-2004}
+loop forever and Refute~\cite{weber-2008} run out of resources. The crux of
+the problem is that they are defined using a least fixed point construction.
+
+Nitpick's philosophy is that not all inductive predicates are equal. Consider
+the \textit{even} predicate below:
+
+\prew
+\textbf{inductive}~\textit{even}~\textbf{where} \\
+\textit{even}~0'' $\,\mid$ \\
+\textit{even}~$n\,\Longrightarrow\, \textit{even}~(\textit{Suc}~(\textit{Suc}~n))$''
+\postw
+
+This predicate enjoys the desirable property of being well-founded, which means
+that the introduction rules don't give rise to infinite chains of the form
+
+\prew
+$\cdots\,\Longrightarrow\, \textit{even}~k'' + \,\Longrightarrow\, \textit{even}~k' + \,\Longrightarrow\, \textit{even}~k.$
+\postw
+
+For \textit{even}, this is obvious: Any chain ending at $k$ will be of length
+$k/2 + 1$:
+
+\prew
+$\textit{even}~0\,\Longrightarrow\, \textit{even}~2\,\Longrightarrow\, \cdots + \,\Longrightarrow\, \textit{even}~(k - 2) + \,\Longrightarrow\, \textit{even}~k.$
+\postw
+
+Wellfoundedness is desirable because it enables Nitpick to use a very efficient
+fixed point computation.%
+\footnote{If an inductive predicate is
+well-founded, then it has exactly one fixed point, which is simultaneously the
+least and the greatest fixed point. In these circumstances, the computation of
+the least fixed point amounts to the computation of an arbitrary fixed point,
+which can be performed using a straightforward recursive equation.}
+Moreover, Nitpick can prove wellfoundedness of most well-founded predicates,
+just as Isabelle's \textbf{function} package usually discharges termination
+proof obligations automatically.
+
+Let's try an example:
+
+\prew
+\textbf{lemma} $\exists n.\; \textit{even}~n \mathrel{\land} \textit{even}~(\textit{Suc}~n)$'' \\
+\textbf{nitpick}~[\textit{card nat}~= 100,\, \textit{verbose}] \\[2\smallskipamount]
+\slshape The inductive predicate \textit{even}'' was proved well-founded.
+Nitpick can compute it efficiently. \\[2\smallskipamount]
+Trying 1 scope: \\
+\hbox{}\qquad \textit{card nat}~= 100. \\[2\smallskipamount]
+Nitpick found a potential counterexample for \textit{card nat}~= 100: \\[2\smallskipamount]
+\hbox{}\qquad Empty assignment \\[2\smallskipamount]
+Nitpick could not find a better counterexample. \\[2\smallskipamount]
+Total time: 2274 ms.
+\postw
+
+No genuine counterexample is possible because Nitpick cannot rule out the
+existence of a natural number $n \ge 100$ such that both $\textit{even}~n$ and
+$\textit{even}~(\textit{Suc}~n)$ are true. To help Nitpick, we can bound the
+existential quantifier:
+
+\prew
+\textbf{lemma} $\exists n \mathbin{\le} 99.\; \textit{even}~n \mathrel{\land} \textit{even}~(\textit{Suc}~n)$'' \\
+\textbf{nitpick}~[\textit{card nat}~= 100] \\[2\smallskipamount]
+\slshape Nitpick found a counterexample: \\[2\smallskipamount]
+\hbox{}\qquad Empty assignment
+\postw
+
+So far we were blessed by the wellfoundedness of \textit{even}. What happens if
+we use the following definition instead?
+
+\prew
+\textbf{inductive} $\textit{even}'$ \textbf{where} \\
+$\textit{even}'~(0{\Colon}\textit{nat})$'' $\,\mid$ \\
+$\textit{even}'~2$'' $\,\mid$ \\
+$\lbrakk\textit{even}'~m;\> \textit{even}'~n\rbrakk \,\Longrightarrow\, \textit{even}'~(m + n)$''
+\postw
+
+This definition is not well-founded: From $\textit{even}'~0$ and
+$\textit{even}'~0$, we can derive that $\textit{even}'~0$. Nonetheless, the
+predicates $\textit{even}$ and $\textit{even}'$ are equivalent.
+
+Let's check a property involving $\textit{even}'$. To make up for the
+foreseeable computational hurdles entailed by non-wellfoundedness, we decrease
+\textit{nat}'s cardinality to a mere 10:
+
+\prew
+\textbf{lemma}~$\exists n \in \{0, 2, 4, 6, 8\}.\; +\lnot\;\textit{even}'~n$'' \\
+\textbf{nitpick}~[\textit{card nat}~= 10,\, \textit{verbose},\, \textit{show\_consts}] \\[2\smallskipamount]
+\slshape
+The inductive predicate $\textit{even}'\!$'' could not be proved well-founded.
+Nitpick might need to unroll it. \\[2\smallskipamount]
+Trying 6 scopes: \\
+\hbox{}\qquad \textit{card nat}~= 10 and \textit{iter} $\textit{even}'$~= 0; \\
+\hbox{}\qquad \textit{card nat}~= 10 and \textit{iter} $\textit{even}'$~= 1; \\
+\hbox{}\qquad \textit{card nat}~= 10 and \textit{iter} $\textit{even}'$~= 2; \\
+\hbox{}\qquad \textit{card nat}~= 10 and \textit{iter} $\textit{even}'$~= 4; \\
+\hbox{}\qquad \textit{card nat}~= 10 and \textit{iter} $\textit{even}'$~= 8; \\
+\hbox{}\qquad \textit{card nat}~= 10 and \textit{iter} $\textit{even}'$~= 9. \\[2\smallskipamount]
+Nitpick found a counterexample for \textit{card nat}~= 10 and \textit{iter} $\textit{even}'$~= 2: \\[2\smallskipamount]
+\hbox{}\qquad Constant: \nopagebreak \\
+\hbox{}\qquad\qquad $\lambda i.\; \textit{even}'$ = \undef(\!\begin{aligned}[t] +& 2 := \{0, 2, 4, 6, 8, 1^\Q, 3^\Q, 5^\Q, 7^\Q, 9^\Q\}, \\[-2pt] +& 1 := \{0, 2, 4, 1^\Q, 3^\Q, 5^\Q, 6^\Q, 7^\Q, 8^\Q, 9^\Q\}, \\[-2pt] +& 0 := \{0, 2, 1^\Q, 3^\Q, 4^\Q, 5^\Q, 6^\Q, 7^\Q, 8^\Q, 9^\Q\})\end{aligned} \\[2\smallskipamount]
+Total time: 1140 ms.
+\postw
+
+Nitpick's output is very instructive. First, it tells us that the predicate is
+unrolled, meaning that it is computed iteratively from the empty set. Then it
+lists six scopes specifying different bounds on the numbers of iterations:\ 0,
+1, 2, 4, 8, and~9.
+
+The output also shows how each iteration contributes to $\textit{even}'$. The
+notation $\lambda i.\; \textit{even}'$ indicates that the value of the
+predicate depends on an iteration counter. Iteration 0 provides the basis
+elements, $0$ and $2$. Iteration 1 contributes $4$ ($= 2 + 2$). Iteration 2
+throws $6$ ($= 2 + 4 = 4 + 2$) and $8$ ($= 4 + 4$) into the mix. Further
+iterations would not contribute any new elements.
+
+Some values are marked with superscripted question
+marks~(\lower.2ex\hbox{$^\Q$}'). These are the elements for which the
+predicate evaluates to $\unk$. Thus, $\textit{even}'$ evaluates to either
+\textit{True} or $\unk$, never \textit{False}.
+
+When unrolling a predicate, Nitpick tries 0, 1, 2, 4, 8, 12, 16, and 24
+iterations. However, these numbers are bounded by the cardinality of the
+predicate's domain. With \textit{card~nat}~= 10, no more than 9 iterations are
+ever needed to compute the value of a \textit{nat} predicate. You can specify
+the number of iterations using the \textit{iter} option, as explained in
+\S\ref{scope-of-search}.
+
+In the next formula, $\textit{even}'$ occurs both positively and negatively:
+
+\prew
+\textbf{lemma} $\textit{even}'~(n - 2) \,\Longrightarrow\, \textit{even}'~n$'' \\
+\textbf{nitpick} [\textit{card nat} = 10,\, \textit{show\_consts}] \\[2\smallskipamount]
+\slshape Nitpick found a counterexample: \\[2\smallskipamount]
+\hbox{}\qquad Free variable: \nopagebreak \\
+\hbox{}\qquad\qquad $n = 1$ \\
+\hbox{}\qquad Constants: \nopagebreak \\
+\hbox{}\qquad\qquad $\lambda i.\; \textit{even}'$ = \undef(\!\begin{aligned}[t] +& 0 := \{0, 2, 1^\Q, 3^\Q, 4^\Q, 5^\Q, 6^\Q, 7^\Q, 8^\Q, 9^\Q\})\end{aligned}  \\
+\hbox{}\qquad\qquad $\textit{even}' \subseteq \{0, 2, 4, 6, 8, \unr\}$
+\postw
+
+Notice the special constraint $\textit{even}' \subseteq \{0,\, 2,\, 4,\, 6,\, +8,\, \unr\}$ in the output, whose right-hand side represents an arbitrary
+fixed point (not necessarily the least one). It is used to falsify
+$\textit{even}'~n$. In contrast, the unrolled predicate is used to satisfy
+$\textit{even}'~(n - 2)$.
+
+Coinductive predicates are handled dually. For example:
+
+\prew
+\textbf{coinductive} \textit{nats} \textbf{where} \\
+$\textit{nats}~(x\Colon\textit{nat}) \,\Longrightarrow\, \textit{nats}~x$'' \\[2\smallskipamount]
+\textbf{lemma} $\textit{nats} = \{0, 1, 2, 3, 4\}$'' \\
+\textbf{nitpick}~[\textit{card nat} = 10,\, \textit{show\_consts}] \\[2\smallskipamount]
+\slshape Nitpick found a counterexample:
+\\[2\smallskipamount]
+\hbox{}\qquad Constants: \nopagebreak \\
+\hbox{}\qquad\qquad \lambda i.\; \textit{nats} = \undef(0 := \{\!\begin{aligned}[t] +& 0^\Q, 1^\Q, 2^\Q, 3^\Q, 4^\Q, 5^\Q, 6^\Q, 7^\Q, 8^\Q, 9^\Q, \\[-2pt] +& \unr\})\end{aligned} \\
+\hbox{}\qquad\qquad $nats \supseteq \{9, 5^\Q, 6^\Q, 7^\Q, 8^\Q, \unr\}$
+\postw
+
+As a special case, Nitpick uses Kodkod's transitive closure operator to encode
+negative occurrences of non-well-founded linear inductive predicates,'' i.e.,
+inductive predicates for which each the predicate occurs in at most one
+assumption of each introduction rule. For example:
+
+\prew
+\textbf{inductive} \textit{odd} \textbf{where} \\
+$\textit{odd}~1$'' $\,\mid$ \\
+$\lbrakk \textit{odd}~m;\>\, \textit{even}~n\rbrakk \,\Longrightarrow\, \textit{odd}~(m + n)$'' \\[2\smallskipamount]
+\textbf{lemma}~$\textit{odd}~n \,\Longrightarrow\, \textit{odd}~(n - 2)$'' \\
+\textbf{nitpick}~[\textit{card nat} = 10,\, \textit{show\_consts}] \\[2\smallskipamount]
+\slshape Nitpick found a counterexample:
+\\[2\smallskipamount]
+\hbox{}\qquad Free variable: \nopagebreak \\
+\hbox{}\qquad\qquad $n = 1$ \\
+\hbox{}\qquad Constants: \nopagebreak \\
+\hbox{}\qquad\qquad $\textit{even} = \{0, 2, 4, 6, 8, \unr\}$ \\
+\hbox{}\qquad\qquad $\textit{odd}_{\textsl{base}} = \{1, \unr\}$ \\
+\hbox{}\qquad\qquad \textit{odd}_{\textsl{step}} = \! +\!\begin{aligned}[t] + & \{(0, 0), (0, 2), (0, 4), (0, 6), (0, 8), (1, 1), (1, 3), (1, 5), \\[-2pt] + & \phantom{\{} (1, 7), (1, 9), (2, 2), (2, 4), (2, 6), (2, 8), (3, 3), + (3, 5), \\[-2pt] + & \phantom{\{} (3, 7), (3, 9), (4, 4), (4, 6), (4, 8), (5, 5), (5, 7), (5, 9), \\[-2pt] + & \phantom{\{} (6, 6), (6, 8), (7, 7), (7, 9), (8, 8), (9, 9), \unr\}\end{aligned} \\
+\hbox{}\qquad\qquad $\textit{odd} \subseteq \{1, 3, 5, 7, 9, 8^\Q, \unr\}$
+\postw
+
+\noindent
+In the output, $\textit{odd}_{\textrm{base}}$ represents the base elements and
+$\textit{odd}_{\textrm{step}}$ is a transition relation that computes new
+elements from known ones. The set $\textit{odd}$ consists of all the values
+reachable through the reflexive transitive closure of
+$\textit{odd}_{\textrm{step}}$ starting with any element from
+$\textit{odd}_{\textrm{base}}$, namely 1, 3, 5, 7, and 9. Using Kodkod's
+transitive closure to encode linear predicates is normally either more thorough
+or more efficient than unrolling (depending on the value of \textit{iter}), but
+for those cases where it isn't you can disable it by passing the
+\textit{dont\_star\_linear\_preds} option.
+
+\subsection{Coinductive Datatypes}
+\label{coinductive-datatypes}
+
+While Isabelle regrettably lacks a high-level mechanism for defining coinductive
+datatypes, the \textit{Coinductive\_List} theory provides a coinductive lazy
+list'' datatype, $'a~\textit{llist}$, defined the hard way. Nitpick supports
+these lazy lists seamlessly and provides a hook, described in
+\S\ref{registration-of-coinductive-datatypes}, to register custom coinductive
+datatypes.
+
+(Co)intuitively, a coinductive datatype is similar to an inductive datatype but
+allows infinite objects. Thus, the infinite lists $\textit{ps}$ $=$ $[a, a, a, +\ldots]$, $\textit{qs}$ $=$ $[a, b, a, b, \ldots]$, and $\textit{rs}$ $=$ $[0, +1, 2, 3, \ldots]$ can be defined as lazy lists using the
+$\textit{LNil}\mathbin{\Colon}{'}a~\textit{llist}$ and
+$\textit{LCons}\mathbin{\Colon}{'}a \mathbin{\Rightarrow} {'}a~\textit{llist} +\mathbin{\Rightarrow} {'}a~\textit{llist}$ constructors.
+
+Although it is otherwise no friend of infinity, Nitpick can find counterexamples
+involving cyclic lists such as \textit{ps} and \textit{qs} above as well as
+finite lists:
+
+\prew
+\textbf{lemma} $\textit{xs} \not= \textit{LCons}~a~\textit{xs}$'' \\
+\textbf{nitpick} \\[2\smallskipamount]
+\slshape Nitpick found a counterexample for {\itshape card}~$'a$ = 1: \\[2\smallskipamount]
+\hbox{}\qquad Free variables: \nopagebreak \\
+\hbox{}\qquad\qquad $\textit{a} = a_1$ \\
+\hbox{}\qquad\qquad $\textit{xs} = \textsl{THE}~\omega.\; \omega = \textit{LCons}~a_1~\omega$
+\postw
+
+The notation $\textrm{THE}~\omega.\; \omega = t(\omega)$ stands
+for the infinite term $t(t(t(\ldots)))$. Hence, \textit{xs} is simply the
+infinite list $[a_1, a_1, a_1, \ldots]$.
+
+The next example is more interesting:
+
+\prew
+\textbf{lemma}~$\lbrakk\textit{xs} = \textit{LCons}~a~\textit{xs};\>\, +\textit{ys} = \textit{iterates}~(\lambda b.\> a)~b\rbrakk \,\Longrightarrow\, \textit{xs} = \textit{ys}$'' \\
+\textbf{nitpick} [\textit{verbose}] \\[2\smallskipamount]
+\slshape The type \kern1pt$'a$'' passed the monotonicity test. Nitpick might be able to skip
+some scopes. \\[2\smallskipamount]
+Trying 8 scopes: \\
+\hbox{}\qquad \textit{card} $'a$~= 1, \textit{card} \kern1pt$'a~\textit{list}$''~= 1,
+and \textit{bisim\_depth}~= 0. \\
+\hbox{}\qquad $\qquad\vdots$ \\[.5\smallskipamount]
+\hbox{}\qquad \textit{card} $'a$~= 8, \textit{card} \kern1pt$'a~\textit{list}$''~= 8,
+and \textit{bisim\_depth}~= 7. \\[2\smallskipamount]
+Nitpick found a counterexample for {\itshape card}~$'a$ = 2,
+\textit{card}~\kern1pt$'a~\textit{list}$''~= 2, and \textit{bisim\_\allowbreak
+depth}~= 1:
+\\[2\smallskipamount]
+\hbox{}\qquad Free variables: \nopagebreak \\
+\hbox{}\qquad\qquad $\textit{a} = a_2$ \\
+\hbox{}\qquad\qquad $\textit{b} = a_1$ \\
+\hbox{}\qquad\qquad $\textit{xs} = \textsl{THE}~\omega.\; \omega = \textit{LCons}~a_2~\omega$ \\
+\hbox{}\qquad\qquad $\textit{ys} = \textit{LCons}~a_1~(\textsl{THE}~\omega.\; \omega = \textit{LCons}~a_2~\omega)$ \\[2\smallskipamount]
+Total time: 726 ms.
+\postw
+
+The lazy list $\textit{xs}$ is simply $[a_2, a_2, a_2, \ldots]$, whereas
+$\textit{ys}$ is $[a_1, a_2, a_2, a_2, \ldots]$, i.e., a lasso-shaped list with
+$[a_1]$ as its stem and $[a_2]$ as its cycle. In general, the list segment
+within the scope of the {THE} binder corresponds to the lasso's cycle, whereas
+the segment leading to the binder is the stem.
+
+A salient property of coinductive datatypes is that two objects are considered
+equal if and only if they lead to the same observations. For example, the lazy
+lists $\textrm{THE}~\omega.\; \omega = +\textit{LCons}~a~(\textit{LCons}~b~\omega)$ and
+$\textit{LCons}~a~(\textrm{THE}~\omega.\; \omega = +\textit{LCons}~b~(\textit{LCons}~a~\omega))$ are identical, because both lead
+to the sequence of observations $a$, $b$, $a$, $b$, \hbox{\ldots} (or,
+equivalently, both encode the infinite list $[a, b, a, b, \ldots]$). This
+concept of equality for coinductive datatypes is called bisimulation and is
+defined coinductively.
+
+Internally, Nitpick encodes the coinductive bisimilarity predicate as part of
+the Kodkod problem to ensure that distinct objects lead to different
+observations. This precaution is somewhat expensive and often unnecessary, so it
+can be disabled by setting the \textit{bisim\_depth} option to $-1$. The
+bisimilarity check is then performed \textsl{after} the counterexample has been
+found to ensure correctness. If this after-the-fact check fails, the
+counterexample is tagged as likely genuine'' and Nitpick recommends to try
+again with \textit{bisim\_depth} set to a nonnegative integer. Disabling the
+check for the previous example saves approximately 150~milli\-seconds; the speed
+gains can be more significant for larger scopes.
+
+The next formula illustrates the need for bisimilarity (either as a Kodkod
+predicate or as an after-the-fact check) to prevent spurious counterexamples:
+
+\prew
+\textbf{lemma} $\lbrakk xs = \textit{LCons}~a~\textit{xs};\>\, \textit{ys} = \textit{LCons}~a~\textit{ys}\rbrakk +\,\Longrightarrow\, \textit{xs} = \textit{ys}$'' \\
+\textbf{nitpick} [\textit{bisim\_depth} = $-1$,\, \textit{show\_datatypes}] \\[2\smallskipamount]
+\slshape Nitpick found a likely genuine counterexample for $\textit{card}~'a$ = 2: \\[2\smallskipamount]
+\hbox{}\qquad Free variables: \nopagebreak \\
+\hbox{}\qquad\qquad $a = a_2$ \\
+\hbox{}\qquad\qquad $\textit{xs} = \textsl{THE}~\omega.\; \omega = +\textit{LCons}~a_2~\omega$ \\
+\hbox{}\qquad\qquad $\textit{ys} = \textsl{THE}~\omega.\; \omega = \textit{LCons}~a_2~\omega$ \\
+\hbox{}\qquad Codatatype:\strut \nopagebreak \\
+\hbox{}\qquad\qquad 'a~\textit{llist} = +\{\!\begin{aligned}[t] + & \textsl{THE}~\omega.\; \omega = \textit{LCons}~a_2~\omega, \\[-2pt] + & \textsl{THE}~\omega.\; \omega = \textit{LCons}~a_2~\omega,\> \unr\}\end{aligned}
+\\[2\smallskipamount]
+Try again with \textit{bisim\_depth}'' set to a nonnegative value to confirm
+that the counterexample is genuine. \\[2\smallskipamount]
+{\upshape\textbf{nitpick}} \\[2\smallskipamount]
+\slshape Nitpick found no counterexample.
+\postw
+
+In the first \textbf{nitpick} invocation, the after-the-fact check discovered
+that the two known elements of type $'a~\textit{llist}$ are bisimilar.
+
+A compromise between leaving out the bisimilarity predicate from the Kodkod
+problem and performing the after-the-fact check is to specify a lower
+nonnegative \textit{bisim\_depth} value than the default one provided by
+Nitpick. In general, a value of $K$ means that Nitpick will require all lists to
+be distinguished from each other by their prefixes of length $K$. Be aware that
+setting $K$ to a too low value can overconstrain Nitpick, preventing it from
+finding any counterexamples.
+
+\subsection{Boxing}
+\label{boxing}
+
+Nitpick normally maps function and product types directly to the corresponding
+Kodkod concepts. As a consequence, if $'a$ has cardinality 3 and $'b$ has
+cardinality 4, then $'a \times {'}b$ has cardinality 12 ($= 4 \times 3$) and $'a +\Rightarrow {'}b$ has cardinality 64 ($= 4^3$). In some circumstances, it pays
+off to treat these types in the same way as plain datatypes, by approximating
+them by a subset of a given cardinality. This technique is called boxing'' and
+is particularly useful for functions passed as arguments to other functions, for
+high-arity functions, and for large tuples. Under the hood, boxing involves
+wrapping occurrences of the types $'a \times {'}b$ and $'a \Rightarrow {'}b$ in
+isomorphic datatypes, as can be seen by enabling the \textit{debug} option.
+
+To illustrate boxing, we consider a formalization of $\lambda$-terms represented
+using de Bruijn's notation:
+
+\prew
+\textbf{datatype} \textit{tm} = \textit{Var}~\textit{nat}~$\mid$~\textit{Lam}~\textit{tm} $\mid$ \textit{App~tm~tm}
+\postw
+
+The $\textit{lift}~t~k$ function increments all variables with indices greater
+than or equal to $k$ by one:
+
+\prew
+\textbf{primrec} \textit{lift} \textbf{where} \\
+$\textit{lift}~(\textit{Var}~j)~k = \textit{Var}~(\textrm{if}~j < k~\textrm{then}~j~\textrm{else}~j + 1)$'' $\mid$ \\
+$\textit{lift}~(\textit{Lam}~t)~k = \textit{Lam}~(\textit{lift}~t~(k + 1))$'' $\mid$ \\
+$\textit{lift}~(\textit{App}~t~u)~k = \textit{App}~(\textit{lift}~t~k)~(\textit{lift}~u~k)$''
+\postw
+
+The $\textit{loose}~t~k$ predicate returns \textit{True} if and only if
+term $t$ has a loose variable with index $k$ or more:
+
+\prew
+\textbf{primrec}~\textit{loose} \textbf{where} \\
+$\textit{loose}~(\textit{Var}~j)~k = (j \ge k)$'' $\mid$ \\
+$\textit{loose}~(\textit{Lam}~t)~k = \textit{loose}~t~(\textit{Suc}~k)$'' $\mid$ \\
+$\textit{loose}~(\textit{App}~t~u)~k = (\textit{loose}~t~k \mathrel{\lor} \textit{loose}~u~k)$''
+\postw
+
+Next, the $\textit{subst}~\sigma~t$ function applies the substitution $\sigma$
+on $t$:
+
+\prew
+\textbf{primrec}~\textit{subst} \textbf{where} \\
+$\textit{subst}~\sigma~(\textit{Var}~j) = \sigma~j$'' $\mid$ \\
+$\textit{subst}~\sigma~(\textit{Lam}~t) = {}$\phantom{''} \\
+\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$ \\
+$\textit{subst}~\sigma~(\textit{App}~t~u) = \textit{App}~(\textit{subst}~\sigma~t)~(\textit{subst}~\sigma~u)$''
+\postw
+
+A substitution is a function that maps variable indices to terms. Observe that
+$\sigma$ is a function passed as argument and that Nitpick can't optimize it
+away, because the recursive call for the \textit{Lam} case involves an altered
+version. Also notice the \textit{lift} call, which increments the variable
+indices when moving under a \textit{Lam}.
+
+A reasonable property to expect of substitution is that it should leave closed
+terms unchanged. Alas, even this simple property does not hold:
+
+\pre
+\textbf{lemma}~$\lnot\,\textit{loose}~t~0 \,\Longrightarrow\, \textit{subst}~\sigma~t = t$'' \\
+\textbf{nitpick} [\textit{verbose}] \\[2\smallskipamount]
+\slshape
+Trying 8 scopes: \nopagebreak \\
+\hbox{}\qquad \textit{card~nat}~= 1, \textit{card tm}~= 1, and \textit{card} $\textit{nat} \Rightarrow \textit{tm}$'' = 1; \\
+\hbox{}\qquad \textit{card~nat}~= 2, \textit{card tm}~= 2, and \textit{card} $\textit{nat} \Rightarrow \textit{tm}$'' = 2; \\
+\hbox{}\qquad $\qquad\vdots$ \\[.5\smallskipamount]
+\hbox{}\qquad \textit{card~nat}~= 8, \textit{card tm}~= 8, and \textit{card} $\textit{nat} \Rightarrow \textit{tm}$'' = 8. \\[2\smallskipamount]
+Nitpick found a counterexample for \textit{card~nat}~= 6, \textit{card~tm}~= 6,
+and \textit{card}~$\textit{nat} \Rightarrow \textit{tm}$''~= 6: \\[2\smallskipamount]
+\hbox{}\qquad Free variables: \nopagebreak \\
+\hbox{}\qquad\qquad \sigma = \undef(\!\begin{aligned}[t] +& 0 := \textit{Var}~0,\> + 1 := \textit{Var}~0,\> + 2 := \textit{Var}~0, \\[-2pt] +& 3 := \textit{Var}~0,\> + 4 := \textit{Var}~0,\> + 5 := \textit{Var}~0)\end{aligned} \\
+\hbox{}\qquad\qquad $t = \textit{Lam}~(\textit{Lam}~(\textit{Var}~1))$ \\[2\smallskipamount]
+Total time: $4679$ ms.
+\postw
+
+Using \textit{eval}, we find out that $\textit{subst}~\sigma~t = +\textit{Lam}~(\textit{Lam}~(\textit{Var}~0))$. Using the traditional
+$\lambda$-term notation, $t$~is
+$\lambda x\, y.\> x$ whereas $\textit{subst}~\sigma~t$ is $\lambda x\, y.\> y$.
+The bug is in \textit{subst}: The $\textit{lift}~(\sigma~m)~1$ call should be
+replaced with $\textit{lift}~(\sigma~m)~0$.
+
+An interesting aspect of Nitpick's verbose output is that it assigned inceasing
+cardinalities from 1 to 8 to the type $\textit{nat} \Rightarrow \textit{tm}$.
+For the formula of interest, knowing 6 values of that type was enough to find
+the counterexample. Without boxing, $46\,656$ ($= 6^6$) values must be
+considered, a hopeless undertaking:
+
+\prew
+\textbf{nitpick} [\textit{dont\_box}] \\[2\smallskipamount]
+{\slshape Nitpick ran out of time after checking 4 of 8 scopes.}
+\postw
+
+{\looseness=-1
+Boxing can be enabled or disabled globally or on a per-type basis using the
+\textit{box} option. Moreover, setting the cardinality of a function or
+product type implicitly enables boxing for that type. Nitpick usually performs
+reasonable choices about which types should be boxed, but option tweaking
+sometimes helps.
+
+}
+
+\subsection{Scope Monotonicity}
+\label{scope-monotonicity}
+
+The \textit{card} option (together with \textit{iter}, \textit{bisim\_depth},
+and \textit{max}) controls which scopes are actually tested. In general, to
+exhaust all models below a certain cardinality bound, the number of scopes that
+Nitpick must consider increases exponentially with the number of type variables
+(and \textbf{typedecl}'d types) occurring in the formula. Given the default
+cardinality specification of 1--8, no fewer than $8^4 = 4096$ scopes must be
+considered for a formula involving $'a$, $'b$, $'c$, and $'d$.
+
+Fortunately, many formulas exhibit a property called \textsl{scope
+monotonicity}, meaning that if the formula is falsifiable for a given scope,
+it is also falsifiable for all larger scopes \cite[p.~165]{jackson-2006}.
+
+Consider the formula
+
+\prew
+\textbf{lemma}~$\textit{length~xs} = \textit{length~ys} \,\Longrightarrow\, \textit{rev}~(\textit{zip~xs~ys}) = \textit{zip~xs}~(\textit{rev~ys})$''
+\postw
+
+where \textit{xs} is of type $'a~\textit{list}$ and \textit{ys} is of type
+$'b~\textit{list}$. A priori, Nitpick would need to consider 512 scopes to
+exhaust the specification \textit{card}~= 1--8. However, our intuition tells us
+that any counterexample found with a small scope would still be a counterexample
+in a larger scope---by simply ignoring the fresh $'a$ and $'b$ values provided
+by the larger scope. Nitpick comes to the same conclusion after a careful
+inspection of the formula and the relevant definitions:
+
+\prew
+\textbf{nitpick}~[\textit{verbose}] \\[2\smallskipamount]
+\slshape
+The types \kern1pt$'a$'' and \kern1pt$'b$'' passed the monotonicity test.
+Nitpick might be able to skip some scopes.
+ \\[2\smallskipamount]
+Trying 8 scopes: \\
+\hbox{}\qquad \textit{card} $'a$~= 1, \textit{card} $'b$~= 1,
+\textit{card} \textit{nat}~= 1, \textit{card} $('a \times {'}b)$
+\textit{list}''~= 1, \\
+\hbox{}\qquad\quad \textit{card} \kern1pt$'a$ \textit{list}''~= 1, and
+\textit{card} \kern1pt$'b$ \textit{list}''~= 1. \\
+\hbox{}\qquad \textit{card} $'a$~= 2, \textit{card} $'b$~= 2,
+\textit{card} \textit{nat}~= 2, \textit{card} $('a \times {'}b)$
+\textit{list}''~= 2, \\
+\hbox{}\qquad\quad \textit{card} \kern1pt$'a$ \textit{list}''~= 2, and
+\textit{card} \kern1pt$'b$ \textit{list}''~= 2. \\
+\hbox{}\qquad $\qquad\vdots$ \\[.5\smallskipamount]
+\hbox{}\qquad \textit{card} $'a$~= 8, \textit{card} $'b$~= 8,
+\textit{card} \textit{nat}~= 8, \textit{card} $('a \times {'}b)$
+\textit{list}''~= 8, \\
+\hbox{}\qquad\quad \textit{card} \kern1pt$'a$ \textit{list}''~= 8, and
+\textit{card} \kern1pt$'b$ \textit{list}''~= 8.
+\\[2\smallskipamount]
+Nitpick found a counterexample for
+\textit{card} $'a$~= 5, \textit{card} $'b$~= 5,
+\textit{card} \textit{nat}~= 5, \textit{card} $('a \times {'}b)$
+\textit{list}''~= 5, \textit{card} \kern1pt$'a$ \textit{list}''~= 5, and
+\textit{card} \kern1pt$'b$ \textit{list}''~= 5:
+\\[2\smallskipamount]
+\hbox{}\qquad Free variables: \nopagebreak \\
+\hbox{}\qquad\qquad $\textit{xs} = [a_4, a_5]$ \\
+\hbox{}\qquad\qquad $\textit{ys} = [b_3, b_3]$ \\[2\smallskipamount]
+Total time: 1636 ms.
+\postw
+
+In theory, it should be sufficient to test a single scope:
+
+\prew
+\textbf{nitpick}~[\textit{card}~= 8]
+\postw
+
+However, this is often less efficient in practice and may lead to overly complex
+counterexamples.
+
+If the monotonicity check fails but we believe that the formula is monotonic (or
+we don't mind missing some counterexamples), we can pass the
+\textit{mono} option. To convince yourself that this option is risky,
+simply consider this example from \S\ref{skolemization}:
+
+\prew
+\textbf{lemma} $\exists g.\; \forall x\Colon 'b.~g~(f~x) = x + \,\Longrightarrow\, \forall y\Colon {'}a.\; \exists x.~y = f~x$'' \\
+\textbf{nitpick} [\textit{mono}] \\[2\smallskipamount]
+{\slshape Nitpick found no counterexample.} \\[2\smallskipamount]
+\textbf{nitpick} \\[2\smallskipamount]
+\slshape
+Nitpick found a counterexample for \textit{card} $'a$~= 2 and \textit{card} $'b$~=~1: \\
+\hbox{}\qquad $\vdots$
+\postw
+
+(It turns out the formula holds if and only if $\textit{card}~'a \le +\textit{card}~'b$.) Although this is rarely advisable, the automatic
+monotonicity checks can be disabled by passing \textit{non\_mono}
+(\S\ref{optimizations}).
+
+As insinuated in \S\ref{natural-numbers-and-integers} and
+\S\ref{inductive-datatypes}, \textit{nat}, \textit{int}, and inductive datatypes
+are normally monotonic and treated as such. The same is true for record types,
+\textit{rat}, \textit{real}, and some \textbf{typedef}'d types. Thus, given the
+cardinality specification 1--8, a formula involving \textit{nat}, \textit{int},
+\textit{int~list}, \textit{rat}, and \textit{rat~list} will lead Nitpick to
+consider only 8~scopes instead of $32\,768$.
+
+\section{Case Studies}
+\label{case-studies}
+
+As a didactic device, the previous section focused mostly on toy formulas whose
+validity can easily be assessed just by looking at the formula. We will now
+review two somewhat more realistic case studies that are within Nitpick's
+reach:\ a context-free grammar modeled by mutually inductive sets and a
+functional implementation of AA trees. The results presented in this
+section were produced with the following settings:
+
+\prew
+\textbf{nitpick\_params} [\textit{max\_potential}~= 0,\, \textit{max\_threads} = 2]
+\postw
+
+\subsection{A Context-Free Grammar}
+\label{a-context-free-grammar}
+
+Our first case study is taken from section 7.4 in the Isabelle tutorial
+\cite{isa-tutorial}. The following grammar, originally due to Hopcroft and
+Ullman, produces all strings with an equal number of $a$'s and $b$'s:
+
+\prew
+\begin{tabular}{@{}r@{$\;\,$}c@{$\;\,$}l@{}}
+$S$ & $::=$ & $\epsilon \mid bA \mid aB$ \\
+$A$ & $::=$ & $aS \mid bAA$ \\
+$B$ & $::=$ & $bS \mid aBB$
+\end{tabular}
+\postw
+
+The intuition behind the grammar is that $A$ generates all string with one more
+$a$ than $b$'s and $B$ generates all strings with one more $b$ than $a$'s.
+
+The alphabet consists exclusively of $a$'s and $b$'s:
+
+\prew
+\textbf{datatype} \textit{alphabet}~= $a$ $\mid$ $b$
+\postw
+
+Strings over the alphabet are represented by \textit{alphabet list}s.
+Nonterminals in the grammar become sets of strings. The production rules
+presented above can be expressed as a mutually inductive definition:
+
+\prew
+\textbf{inductive\_set} $S$ \textbf{and} $A$ \textbf{and} $B$ \textbf{where} \\
+\textit{R1}:\kern.4em $[] \in S$'' $\,\mid$ \\
+\textit{R2}:\kern.4em $w \in A\,\Longrightarrow\, b \mathbin{\#} w \in S$'' $\,\mid$ \\
+\textit{R3}:\kern.4em $w \in B\,\Longrightarrow\, a \mathbin{\#} w \in S$'' $\,\mid$ \\
+\textit{R4}:\kern.4em $w \in S\,\Longrightarrow\, a \mathbin{\#} w \in A$'' $\,\mid$ \\
+\textit{R5}:\kern.4em $w \in S\,\Longrightarrow\, b \mathbin{\#} w \in S$'' $\,\mid$ \\
+\textit{R6}:\kern.4em $\lbrakk v \in B;\> v \in B\rbrakk \,\Longrightarrow\, a \mathbin{\#} v \mathbin{@} w \in B$''
+\postw
+
+The conversion of the grammar into the inductive definition was done manually by
+Joe Blow, an underpaid undergraduate student. As a result, some errors might
+have sneaked in.
+
+Debugging faulty specifications is at the heart of Nitpick's \textsl{raison
+d'\^etre}. A good approach is to state desirable properties of the specification
+(here, that $S$ is exactly the set of strings over $\{a, b\}$ with as many $a$'s
+as $b$'s) and check them with Nitpick. If the properties are correctly stated,
+counterexamples will point to bugs in the specification. For our grammar
+example, we will proceed in two steps, separating the soundness and the
+completeness of the set $S$. First, soundness:
+
+\prew
+\textbf{theorem}~\textit{S\_sound}: \\
+$w \in S \longrightarrow \textit{length}~[x\mathbin{\leftarrow} w.\; x = a] = + \textit{length}~[x\mathbin{\leftarrow} w.\; x = b]$'' \\
+\textbf{nitpick} \\[2\smallskipamount]
+\slshape Nitpick found a counterexample: \\[2\smallskipamount]
+\hbox{}\qquad Free variable: \nopagebreak \\
+\hbox{}\qquad\qquad $w = [b]$
+\postw
+
+It would seem that $[b] \in S$. How could this be? An inspection of the
+introduction rules reveals that the only rule with a right-hand side of the form
+$b \mathbin{\#} {\ldots} \in S$ that could have introduced $[b]$ into $S$ is
+\textit{R5}:
+
+\prew
+$w \in S\,\Longrightarrow\, b \mathbin{\#} w \in S$''
+\postw
+
+On closer inspection, we can see that this rule is wrong. To match the
+production $B ::= bS$, the second $S$ should be a $B$. We fix the typo and try
+again:
+
+\prew
+\textbf{nitpick} \\[2\smallskipamount]
+\slshape Nitpick found a counterexample: \\[2\smallskipamount]
+\hbox{}\qquad Free variable: \nopagebreak \\
+\hbox{}\qquad\qquad $w = [a, a, b]$
+\postw
+
+Some detective work is necessary to find out what went wrong here. To get $[a, +a, b] \in S$, we need $[a, b] \in B$ by \textit{R3}, which in turn can only come
+from \textit{R6}:
+
+\prew
+$\lbrakk v \in B;\> v \in B\rbrakk \,\Longrightarrow\, a \mathbin{\#} v \mathbin{@} w \in B$''
+\postw
+
+Now, this formula must be wrong: The same assumption occurs twice, and the
+variable $w$ is unconstrained. Clearly, one of the two occurrences of $v$ in
+the assumptions should have been a $w$.
+
+With the correction made, we don't get any counterexample from Nitpick. Let's
+move on and check completeness:
+
+\prew
+\textbf{theorem}~\textit{S\_complete}: \\
+$\textit{length}~[x\mathbin{\leftarrow} w.\; x = a] = + \textit{length}~[x\mathbin{\leftarrow} w.\; x = b] + \longrightarrow w \in S$'' \\
+\textbf{nitpick} \\[2\smallskipamount]
+\slshape Nitpick found a counterexample: \\[2\smallskipamount]
+\hbox{}\qquad Free variable: \nopagebreak \\
+\hbox{}\qquad\qquad $w = [b, b, a, a]$
+\postw
+
+Apparently, $[b, b, a, a] \notin S$, even though it has the same numbers of
+$a$'s and $b$'s. But since our inductive definition passed the soundness check,
+the introduction rules we have are probably correct. Perhaps we simply lack an
+introduction rule. Comparing the grammar with the inductive definition, our
+suspicion is confirmed: Joe Blow simply forgot the production $A ::= bAA$,
+without which the grammar cannot generate two or more $b$'s in a row. So we add
+the rule
+
+\prew
+$\lbrakk v \in A;\> w \in A\rbrakk \,\Longrightarrow\, b \mathbin{\#} v \mathbin{@} w \in A$''
+\postw
+
+With this last change, we don't get any counterexamples from Nitpick for either
+soundness or completeness. We can even generalize our result to cover $A$ and
+$B$ as well:
+
+\prew
+\textbf{theorem} \textit{S\_A\_B\_sound\_and\_complete}: \\
+$w \in S \longleftrightarrow \textit{length}~[x \mathbin{\leftarrow} w.\; x = a] = \textit{length}~[x \mathbin{\leftarrow} w.\; x = b]$'' \\
+$w \in A \longleftrightarrow \textit{length}~[x \mathbin{\leftarrow} w.\; x = a] = \textit{length}~[x \mathbin{\leftarrow} w.\; x = b] + 1$'' \\
+$w \in B \longleftrightarrow \textit{length}~[x \mathbin{\leftarrow} w.\; x = b] = \textit{length}~[x \mathbin{\leftarrow} w.\; x = a] + 1$'' \\
+\textbf{nitpick} \\[2\smallskipamount]
+\slshape Nitpick found no counterexample.
+\postw
+
+\subsection{AA Trees}
+\label{aa-trees}
+
+AA trees are a kind of balanced trees discovered by Arne Andersson that provide
+similar performance to red-black trees, but with a simpler implementation
+\cite{andersson-1993}. They can be used to store sets of elements equipped with
+a total order $<$. We start by defining the datatype and some basic extractor
+functions:
+
+\prew
+\textbf{datatype} $'a$~\textit{tree} = $\Lambda$ $\mid$ $N$ \kern1pt$'a\Colon \textit{linorder}$'' \textit{nat} \kern1pt$'a$ \textit{tree}'' \kern1pt$'a$ \textit{tree}''  \\[2\smallskipamount]
+\textbf{primrec} \textit{data} \textbf{where} \\
+$\textit{data}~\Lambda = \undef$'' $\,\mid$ \\
+$\textit{data}~(N~x~\_~\_~\_) = x$'' \\[2\smallskipamount]
+\textbf{primrec} \textit{dataset} \textbf{where} \\
+$\textit{dataset}~\Lambda = \{\}$'' $\,\mid$ \\
+$\textit{dataset}~(N~x~\_~t~u) = \{x\} \cup \textit{dataset}~t \mathrel{\cup} \textit{dataset}~u$'' \\[2\smallskipamount]
+\textbf{primrec} \textit{level} \textbf{where} \\
+$\textit{level}~\Lambda = 0$'' $\,\mid$ \\
+$\textit{level}~(N~\_~k~\_~\_) = k$'' \\[2\smallskipamount]
+\textbf{primrec} \textit{left} \textbf{where} \\
+$\textit{left}~\Lambda = \Lambda$'' $\,\mid$ \\
+$\textit{left}~(N~\_~\_~t~\_) = t$'' \\[2\smallskipamount]
+\textbf{primrec} \textit{right} \textbf{where} \\
+$\textit{right}~\Lambda = \Lambda$'' $\,\mid$ \\
+$\textit{right}~(N~\_~\_~\_~u) = u$''
+\postw
+
+The wellformedness criterion for AA trees is fairly complex. Wikipedia states it
+as follows \cite{wikipedia-2009-aa-trees}:
+
+\kern.2\parskip %% TYPESETTING
+
+\pre
+Each node has a level field, and the following invariants must remain true for
+the tree to be valid:
+
+\raggedright
+
+\kern-.4\parskip %% TYPESETTING
+
+\begin{enum}
+\item[]
+\begin{enum}
+\item[1.] The level of a leaf node is one.
+\item[2.] The level of a left child is strictly less than that of its parent.
+\item[3.] The level of a right child is less than or equal to that of its parent.
+\item[4.] The level of a right grandchild is strictly less than that of its grandparent.
+\item[5.] Every node of level greater than one must have two children.
+\end{enum}
+\end{enum}
+\post
+
+\kern.4\parskip %% TYPESETTING
+
+The \textit{wf} predicate formalizes this description:
+
+\prew
+\textbf{primrec} \textit{wf} \textbf{where} \\
+$\textit{wf}~\Lambda = \textit{True}$'' $\,\mid$ \\
+$\textit{wf}~(N~\_~k~t~u) =$ \\
+\phantom{}$(\textrm{if}~t = \Lambda~\textrm{then}$ \\
+\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))$ \\
+\phantom{$($}$\textrm{else}$ \\
+\hbox{\phantom{$(\quad$}$\textit{wf}~t \mathrel{\land} \textit{wf}~u +\mathrel{\land} u \not= \Lambda \mathrel{\land} \textit{level}~t < k +\mathrel{\land} \textit{level}~u \le k \mathrel{\land} +\textit{level}~(\textit{right}~u) < k)$''}\kern-200mm
+\postw
+
+Rebalancing the tree upon insertion and removal of elements is performed by two
+auxiliary functions called \textit{skew} and \textit{split}, defined below:
+
+\prew
+\textbf{primrec} \textit{skew} \textbf{where} \\
+$\textit{skew}~\Lambda = \Lambda$'' $\,\mid$ \\
+$\textit{skew}~(N~x~k~t~u) = {}$ \\
+\phantom{}$(\textrm{if}~t \not= \Lambda \mathrel{\land} k = +\textit{level}~t~\textrm{then}$ \\
+\phantom{(\quad}$N~(\textit{data}~t)~k~(\textit{left}~t)~(N~x~k~ +(\textit{right}~t)~u)$ \\
+\phantom{(}$\textrm{else}$ \\
+\phantom{(\quad}$N~x~k~t~u)$''
+\postw
+
+\prew
+\textbf{primrec} \textit{split} \textbf{where} \\
+$\textit{split}~\Lambda = \Lambda$'' $\,\mid$ \\
+$\textit{split}~(N~x~k~t~u) = {}$ \\
+\phantom{}$(\textrm{if}~u \not= \Lambda \mathrel{\land} k = +\textit{level}~(\textit{right}~u)~\textrm{then}$ \\
+\phantom{(\quad}$N~(\textit{data}~u)~(\textit{Suc}~k)~ +(N~x~k~t~(\textit{left}~u))~(\textit{right}~u)$ \\
+\phantom{(}$\textrm{else}$ \\
+\phantom{(\quad}$N~x~k~t~u)$''
+\postw
+
+Performing a \textit{skew} or a \textit{split} should have no impact on the set
+of elements stored in the tree:
+
+\prew
+\textbf{theorem}~\textit{dataset\_skew\_split}:\\
+$\textit{dataset}~(\textit{skew}~t) = \textit{dataset}~t$'' \\
+$\textit{dataset}~(\textit{split}~t) = \textit{dataset}~t$'' \\
+\textbf{nitpick} \\[2\smallskipamount]
+{\slshape Nitpick ran out of time after checking 7 of 8 scopes.}
+\postw
+
+Furthermore, applying \textit{skew} or \textit{split} to a well-formed tree
+should not alter the tree:
+
+\prew
+\textbf{theorem}~\textit{wf\_skew\_split}:\\
+$\textit{wf}~t\,\Longrightarrow\, \textit{skew}~t = t$'' \\
+$\textit{wf}~t\,\Longrightarrow\, \textit{split}~t = t$'' \\
+\textbf{nitpick} \\[2\smallskipamount]
+{\slshape Nitpick found no counterexample.}
+\postw
+
+Insertion is implemented recursively. It preserves the sort order:
+
+\prew
+\textbf{primrec}~\textit{insort} \textbf{where} \\
+$\textit{insort}~\Lambda~x = N~x~1~\Lambda~\Lambda$'' $\,\mid$ \\
+$\textit{insort}~(N~y~k~t~u)~x =$ \\
+\phantom{}$({*}~(\textit{split} \circ \textit{skew})~{*})~(N~y~k~(\textrm{if}~x < y~\textrm{then}~\textit{insort}~t~x~\textrm{else}~t)$ \\
+\phantom{$({*}~(\textit{split} \circ \textit{skew})~{*})~(N~y~k~$}$(\textrm{if}~x > y~\textrm{then}~\textit{insort}~u~x~\textrm{else}~u))$''
+\postw
+
+Notice that we deliberately commented out the application of \textit{skew} and
+\textit{split}. Let's see if this causes any problems:
+
+\prew
+\textbf{theorem}~\textit{wf\_insort}:\kern.4em $\textit{wf}~t\,\Longrightarrow\, \textit{wf}~(\textit{insort}~t~x)$'' \\
+\textbf{nitpick} \\[2\smallskipamount]
+\slshape Nitpick found a counterexample for \textit{card} $'a$ = 4: \\[2\smallskipamount]
+\hbox{}\qquad Free variables: \nopagebreak \\
+\hbox{}\qquad\qquad $t = N~a_3~1~\Lambda~\Lambda$ \\
+\hbox{}\qquad\qquad $x = a_4$ \\[2\smallskipamount]
+Hint: Maybe you forgot a type constraint?
+\postw
+
+It's hard to see why this is a counterexample. The hint is of no help here. To
+improve readability, we will restrict the theorem to \textit{nat}, so that we
+don't need to look up the value of the $\textit{op}~{<}$ constant to find out
+which element is smaller than the other. In addition, we will tell Nitpick to
+display the value of $\textit{insort}~t~x$ using the \textit{eval} option. This
+gives
+
+\prew
+\textbf{theorem} \textit{wf\_insort\_nat}:\kern.4em $\textit{wf}~t\,\Longrightarrow\, \textit{wf}~(\textit{insort}~t~(x\Colon\textit{nat}))$'' \\
+\textbf{nitpick} [\textit{eval} = $\textit{insort}~t~x$''] \\[2\smallskipamount]
+\slshape Nitpick found a counterexample: \\[2\smallskipamount]
+\hbox{}\qquad Free variables: \nopagebreak \\
+\hbox{}\qquad\qquad $t = N~1~1~\Lambda~\Lambda$ \\
+\hbox{}\qquad\qquad $x = 0$ \\
+\hbox{}\qquad Evaluated term: \\
+\hbox{}\qquad\qquad $\textit{insort}~t~x = N~1~1~(N~0~1~\Lambda~\Lambda)~\Lambda$
+\postw
+
+Nitpick's output reveals that the element $0$ was added as a left child of $1$,
+where both have a level of 1. This violates the second AA tree invariant, which
+states that a left child's level must be less than its parent's. This shouldn't
+come as a surprise, considering that we commented out the tree rebalancing code.
+Reintroducing the code seems to solve the problem:
+
+\prew
+\textbf{theorem}~\textit{wf\_insort}:\kern.4em $\textit{wf}~t\,\Longrightarrow\, \textit{wf}~(\textit{insort}~t~x)$'' \\
+\textbf{nitpick} \\[2\smallskipamount]
+{\slshape Nitpick ran out of time after checking 6 of 8 scopes.}
+\postw
+
+Insertion should transform the set of elements represented by the tree in the
+obvious way:
+
+\prew
+\textbf{theorem} \textit{dataset\_insort}:\kern.4em
+$\textit{dataset}~(\textit{insort}~t~x) = \{x\} \cup \textit{dataset}~t$'' \\
+\textbf{nitpick} \\[2\smallskipamount]
+{\slshape Nitpick ran out of time after checking 5 of 8 scopes.}
+\postw
+
+We could continue like this and sketch a complete theory of AA trees without
+performing a single proof. Once the definitions and main theorems are in place
+and have been thoroughly tested using Nitpick, we could start working on the
+proofs. Developing theories this way usually saves time, because faulty theorems
+and definitions are discovered much earlier in the process.
+
+\section{Option Reference}
+\label{option-reference}
+
+\def\flushitem#1{\item[]\noindent\kern-\leftmargin \textbf{#1}}
+\def\qty#1{$\left<\textit{#1}\right>$}
+\def\qtybf#1{$\mathbf{\left<\textbf{\textit{#1}}\right>}$}
+\def\optrue#1#2{\flushitem{\textit{#1} $\bigl[$= \qtybf{bool}$\bigr]$\quad [\textit{true}]\hfill (neg.: \textit{#2})}\nopagebreak\\[\parskip]}
+\def\opfalse#1#2{\flushitem{\textit{#1} $\bigl[$= \qtybf{bool}$\bigr]$\quad [\textit{false}]\hfill (neg.: \textit{#2})}\nopagebreak\\[\parskip]}
+\def\opsmart#1#2{\flushitem{\textit{#1} $\bigl[$= \qtybf{bool\_or\_smart}$\bigr]$\quad [\textit{smart}]\hfill (neg.: \textit{#2})}\nopagebreak\\[\parskip]}
+\def\ops#1#2{\flushitem{\textit{#1} = \qtybf{#2}} \nopagebreak\\[\parskip]}
+\def\opt#1#2#3{\flushitem{\textit{#1} = \qtybf{#2}\quad [\textit{#3}]} \nopagebreak\\[\parskip]}
+\def\opu#1#2#3{\flushitem{\textit{#1} \qtybf{#2} = \qtybf{#3}} \nopagebreak\\[\parskip]}
+\def\opusmart#1#2#3{\flushitem{\textit{#1} \qtybf{#2} $\bigl[$= \qtybf{bool\_or\_smart}$\bigr]$\hfill (neg.: \textit{#3})}\nopagebreak\\[\parskip]}
+
+Nitpick's behavior can be influenced by various options, which can be specified
+in brackets after the \textbf{nitpick} command. Default values can be set
+using \textbf{nitpick\_\allowbreak params}. For example:
+
+\prew
+\textbf{nitpick\_params} [\textit{verbose}, \,\textit{timeout} = 60$\,s$]
+\postw
+
+The options are categorized as follows:\ mode of operation
+(\S\ref{mode-of-operation}), scope of search (\S\ref{scope-of-search}), output
+format (\S\ref{output-format}), automatic counterexample checks
+(\S\ref{authentication}), optimizations
+(\S\ref{optimizations}), and timeouts (\S\ref{timeouts}).
+
+The number of options can be overwhelming at first glance. Do not let that worry
+you: Nitpick's defaults have been chosen so that it almost always does the right
+thing, and the most important options have been covered in context in
+\S\ref{first-steps}.
+
+The descriptions below refer to the following syntactic quantities:
+
+\begin{enum}
+\item[$\bullet$] \qtybf{string}: A string.
+\item[$\bullet$] \qtybf{bool}: \textit{true} or \textit{false}.
+\item[$\bullet$] \qtybf{bool\_or\_smart}: \textit{true}, \textit{false}, or \textit{smart}.
+\item[$\bullet$] \qtybf{int}: An integer. Negative integers are prefixed with a hyphen.
+\item[$\bullet$] \qtybf{int\_or\_smart}: An integer or \textit{smart}.
+\item[$\bullet$] \qtybf{int\_range}: An integer (e.g., 3) or a range
+of nonnegative integers (e.g., $1$--$4$). The range symbol --' can be entered as \texttt{-} (hyphen) or \texttt{\char\\\char\<midarrow\char\>}.
+
+\item[$\bullet$] \qtybf{int\_seq}: A comma-separated sequence of ranges of integers (e.g.,~1{,}3{,}\allowbreak6--8).
+\item[$\bullet$] \qtybf{time}: An integer followed by $\textit{min}$ (minutes), $s$ (seconds), or \textit{ms}
+(milliseconds), or the keyword \textit{none} ($\infty$ years).
+\item[$\bullet$] \qtybf{const}: The name of a HOL constant.
+\item[$\bullet$] \qtybf{term}: A HOL term (e.g., $f~x$'').
+\item[$\bullet$] \qtybf{term\_list}: A space-separated list of HOL terms (e.g.,
+$f~x$''~$g~y$'').
+\item[$\bullet$] \qtybf{type}: A HOL type.
+\end{enum}
+
+Default values are indicated in square brackets. Boolean options have a negated
+counterpart (e.g., \textit{auto} vs.\ \textit{no\_auto}). When setting Boolean
+options, = \textit{true}'' may be omitted.
+
+\subsection{Mode of Operation}
+\label{mode-of-operation}
+
+\begin{enum}
+\opfalse{auto}{no\_auto}
+Specifies whether Nitpick should be run automatically on newly entered theorems.
+For automatic runs, \textit{user\_axioms} (\S\ref{mode-of-operation}) and
+\textit{assms} (\S\ref{mode-of-operation}) are implicitly enabled,
+\textit{blocking} (\S\ref{mode-of-operation}), \textit{verbose}
+(\S\ref{output-format}), and \textit{debug} (\S\ref{output-format}) are
+disabled, \textit{max\_potential} (\S\ref{output-format}) is taken to be 0, and
+\textit{auto\_timeout} (\S\ref{timeouts}) is used as the time limit instead of
+\textit{timeout} (\S\ref{timeouts}). The output is also more concise.
+
+\nopagebreak
+{\small See also \textit{auto\_timeout} (\S\ref{timeouts}).}
+
+\optrue{blocking}{non\_blocking}
+Specifies whether the \textbf{nitpick} command should operate synchronously.
+The asynchronous (non-blocking) mode lets the user start proving the putative
+theorem while Nitpick looks for a counterexample, but it can also be more
+confusing. For technical reasons, automatic runs currently always block.
+
+\nopagebreak
+{\small See also \textit{auto} (\S\ref{mode-of-operation}).}
+
+\optrue{falsify}{satisfy}
+Specifies whether Nitpick should look for falsifying examples (countermodels) or
+satisfying examples (models). This manual assumes throughout that
+\textit{falsify} is enabled.
+
+\opsmart{user\_axioms}{no\_user\_axioms}
+Specifies whether the user-defined axioms (specified using
+\textbf{axiomatization} and \textbf{axioms}) should be considered. If the option
+is set to \textit{smart}, Nitpick performs an ad hoc axiom selection based on
+the constants that occur in the formula to falsify. The option is implicitly set
+to \textit{true} for automatic runs.
+
+\textbf{Warning:} If the option is set to \textit{true}, Nitpick might
+nonetheless ignore some polymorphic axioms. Counterexamples generated under
+these conditions are tagged as likely genuine.'' The \textit{debug}
+(\S\ref{output-format}) option can be used to find out which axioms were
+considered.
+
+\nopagebreak
+{\small See also \textit{auto} (\S\ref{mode-of-operation}), \textit{assms}
+(\S\ref{mode-of-operation}), and \textit{debug} (\S\ref{output-format}).}
+
+\optrue{assms}{no\_assms}
+Specifies whether the relevant assumptions in structured proof should be
+considered. The option is implicitly enabled for automatic runs.
+
+\nopagebreak
+{\small See also \textit{auto} (\S\ref{mode-of-operation})
+and \textit{user\_axioms} (\S\ref{mode-of-operation}).}
+
+\opfalse{overlord}{no\_overlord}
+Specifies whether Nitpick should put its temporary files in
+\texttt{\$ISABELLE\_\allowbreak HOME\_\allowbreak USER}, which is useful for +debugging Nitpick but also unsafe if several instances of the tool are run +simultaneously. This option is disabled by default unless your home directory +ends with \texttt{blanchet} or \texttt{blanchette}. +%I thought there was only one overlord.'' --- Tobias Nipkow + +\nopagebreak +{\small See also \textit{debug} (\S\ref{output-format}).} +\end{enum} + +\subsection{Scope of Search} +\label{scope-of-search} + +\begin{enum} +\opu{card}{type}{int\_seq} +Specifies the sequence of cardinalities to use for a given type. For +\textit{nat} and \textit{int}, the cardinality fully specifies the subset used +to approximate the type. For example: +% +$$\hbox{\begin{tabular}{@{}rll@{}}% +\textit{card nat} = 4 & induces & \{0,\, 1,\, 2,\, 3\} \\ +\textit{card int} = 4 & induces & \{-1,\, 0,\, +1,\, +2\} \\ +\textit{card int} = 5 & induces & \{-2,\, -1,\, 0,\, +1,\, +2\}.% +\end{tabular}}$$ +% +In general: +% +$$\hbox{\begin{tabular}{@{}rll@{}}% +\textit{card nat} = K & induces & \{0,\, \ldots,\, K - 1\} \\ +\textit{card int} = K & induces & \{-\lceil K/2 \rceil + 1,\, \ldots,\, +\lfloor K/2 \rfloor\}.% +\end{tabular}}$$ +% +For free types, and often also for \textbf{typedecl}'d types, it usually makes +sense to specify cardinalities as a range of the form \textit{$1$--$n$}. +Although function and product types are normally mapped directly to the +corresponding Kodkod concepts, setting +the cardinality of such types is also allowed and implicitly enables boxing'' +for them, as explained in the description of the \textit{box}~\qty{type} +and \textit{box} (\S\ref{scope-of-search}) options. + +\nopagebreak +{\small See also \textit{mono} (\S\ref{scope-of-search}).} + +\opt{card}{int\_seq}{$\mathbf{1}$--$\mathbf{8}$} +Specifies the default sequence of cardinalities to use. This can be overridden +on a per-type basis using the \textit{card}~\qty{type} option described above. + +\opu{max}{const}{int\_seq} +Specifies the sequence of maximum multiplicities to use for a given +(co)in\-duc\-tive datatype constructor. A constructor's multiplicity is the +number of distinct values that it can construct. Nonsensical values (e.g., +\textit{max}~[]~$=$~2) are silently repaired. This option is only available for +datatypes equipped with several constructors. + +\ops{max}{int\_seq} +Specifies the default sequence of maximum multiplicities to use for +(co)in\-duc\-tive datatype constructors. This can be overridden on a per-constructor +basis using the \textit{max}~\qty{const} option described above. + +\opusmart{wf}{const}{non\_wf} +Specifies whether the specified (co)in\-duc\-tively defined predicate is +well-founded. The option can take the following values: + +\begin{enum} +\item[$\bullet$] \textbf{\textit{true}}: Tentatively treat the (co)in\-duc\-tive +predicate as if it were well-founded. Since this is generally not sound when the +predicate is not well-founded, the counterexamples are tagged as likely +genuine.'' + +\item[$\bullet$] \textbf{\textit{false}}: Treat the (co)in\-duc\-tive predicate +as if it were not well-founded. The predicate is then unrolled as prescribed by +the \textit{star\_linear\_preds}, \textit{iter}~\qty{const}, and \textit{iter} +options. + +\item[$\bullet$] \textbf{\textit{smart}}: Try to prove that the inductive +predicate is well-founded using Isabelle's \textit{lexicographic\_order} and +\textit{sizechange} tactics. If this succeeds (or the predicate occurs with an +appropriate polarity in the formula to falsify), use an efficient fixed point +equation as specification of the predicate; otherwise, unroll the predicates +according to the \textit{iter}~\qty{const} and \textit{iter} options. +\end{enum} + +\nopagebreak +{\small See also \textit{iter} (\S\ref{scope-of-search}), +\textit{star\_linear\_preds} (\S\ref{optimizations}), and \textit{tac\_timeout} +(\S\ref{timeouts}).} + +\opsmart{wf}{non\_wf} +Specifies the default wellfoundedness setting to use. This can be overridden on +a per-predicate basis using the \textit{wf}~\qty{const} option above. + +\opu{iter}{const}{int\_seq} +Specifies the sequence of iteration counts to use when unrolling a given +(co)in\-duc\-tive predicate. By default, unrolling is applied for inductive +predicates that occur negatively and coinductive predicates that occur +positively in the formula to falsify and that cannot be proved to be +well-founded, but this behavior is influenced by the \textit{wf} option. The +iteration counts are automatically bounded by the cardinality of the predicate's +domain. + +{\small See also \textit{wf} (\S\ref{scope-of-search}) and +\textit{star\_linear\_preds} (\S\ref{optimizations}).} + +\opt{iter}{int\_seq}{$\mathbf{1{,}2{,}4{,}8{,}12{,}16{,}24{,}32}$} +Specifies the sequence of iteration counts to use when unrolling (co)in\-duc\-tive +predicates. This can be overridden on a per-predicate basis using the +\textit{iter} \qty{const} option above. + +\opt{bisim\_depth}{int\_seq}{$\mathbf{7}$} +Specifies the sequence of iteration counts to use when unrolling the +bisimilarity predicate generated by Nitpick for coinductive datatypes. A value +of$-1$means that no predicate is generated, in which case Nitpick performs an +after-the-fact check to see if the known coinductive datatype values are +bidissimilar. If two values are found to be bisimilar, the counterexample is +tagged as likely genuine.'' The iteration counts are automatically bounded by +the sum of the cardinalities of the coinductive datatypes occurring in the +formula to falsify. + +\opusmart{box}{type}{dont\_box} +Specifies whether Nitpick should attempt to wrap (box'') a given function or +product type in an isomorphic datatype internally. Boxing is an effective mean +to reduce the search space and speed up Nitpick, because the isomorphic datatype +is approximated by a subset of the possible function or pair values; +like other drastic optimizations, it can also prevent the discovery of +counterexamples. The option can take the following values: + +\begin{enum} +\item[$\bullet$] \textbf{\textit{true}}: Box the specified type whenever +practicable. +\item[$\bullet$] \textbf{\textit{false}}: Never box the type. +\item[$\bullet$] \textbf{\textit{smart}}: Box the type only in contexts where it +is likely to help. For example,$n$-tuples where$n > 2$and arguments to +higher-order functions are good candidates for boxing. +\end{enum} + +Setting the \textit{card}~\qty{type} option for a function or product type +implicitly enables boxing for that type. + +\nopagebreak +{\small See also \textit{verbose} (\S\ref{output-format}) +and \textit{debug} (\S\ref{output-format}).} + +\opsmart{box}{dont\_box} +Specifies the default boxing setting to use. This can be overridden on a +per-type basis using the \textit{box}~\qty{type} option described above. + +\opusmart{mono}{type}{non\_mono} +Specifies whether the specified type should be considered monotonic when +enumerating scopes. If the option is set to \textit{smart}, Nitpick performs a +monotonicity check on the type. Setting this option to \textit{true} can reduce +the number of scopes tried, but it also diminishes the theoretical chance of +finding a counterexample, as demonstrated in \S\ref{scope-monotonicity}. + +\nopagebreak +{\small See also \textit{card} (\S\ref{scope-of-search}), +\textit{coalesce\_type\_vars} (\S\ref{scope-of-search}), and \textit{verbose} +(\S\ref{output-format}).} + +\opsmart{mono}{non\_box} +Specifies the default monotonicity setting to use. This can be overridden on a +per-type basis using the \textit{mono}~\qty{type} option described above. + +\opfalse{coalesce\_type\_vars}{dont\_coalesce\_type\_vars} +Specifies whether type variables with the same sort constraints should be +merged. Setting this option to \textit{true} can reduce the number of scopes +tried and the size of the generated Kodkod formulas, but it also diminishes the +theoretical chance of finding a counterexample. + +{\small See also \textit{mono} (\S\ref{scope-of-search}).} +\end{enum} + +\subsection{Output Format} +\label{output-format} + +\begin{enum} +\opfalse{verbose}{quiet} +Specifies whether the \textbf{nitpick} command should explain what it does. This +option is useful to determine which scopes are tried or which SAT solver is +used. This option is implicitly disabled for automatic runs. + +\nopagebreak +{\small See also \textit{auto} (\S\ref{mode-of-operation}).} + +\opfalse{debug}{no\_debug} +Specifies whether Nitpick should display additional debugging information beyond +what \textit{verbose} already displays. Enabling \textit{debug} also enables +\textit{verbose} and \textit{show\_all} behind the scenes. The \textit{debug} +option is implicitly disabled for automatic runs. + +\nopagebreak +{\small See also \textit{auto} (\S\ref{mode-of-operation}), \textit{overlord} +(\S\ref{mode-of-operation}), and \textit{batch\_size} (\S\ref{optimizations}).} + +\optrue{show\_skolems}{hide\_skolem} +Specifies whether the values of Skolem constants should be displayed as part of +counterexamples. Skolem constants correspond to bound variables in the original +formula and usually help us to understand why the counterexample falsifies the +formula. + +\nopagebreak +{\small See also \textit{skolemize} (\S\ref{optimizations}).} + +\opfalse{show\_datatypes}{hide\_datatypes} +Specifies whether the subsets used to approximate (co)in\-duc\-tive datatypes should +be displayed as part of counterexamples. Such subsets are sometimes helpful when +investigating whether a potential counterexample is genuine or spurious, but +their potential for clutter is real. + +\opfalse{show\_consts}{hide\_consts} +Specifies whether the values of constants occurring in the formula (including +its axioms) should be displayed along with any counterexample. These values are +sometimes helpful when investigating why a counterexample is +genuine, but they can clutter the output. + +\opfalse{show\_all}{dont\_show\_all} +Enabling this option effectively enables \textit{show\_skolems}, +\textit{show\_datatypes}, and \textit{show\_consts}. + +\opt{max\_potential}{int}{$\mathbf{1}$} +Specifies the maximum number of potential counterexamples to display. Setting +this option to 0 speeds up the search for a genuine counterexample. This option +is implicitly set to 0 for automatic runs. If you set this option to a value +greater than 1, you will need an incremental SAT solver: For efficiency, it is +recommended to install the JNI version of MiniSat and set \textit{sat\_solver} = +\textit{MiniSatJNI}. Also be aware that many of the counterexamples may look +identical, unless the \textit{show\_all} (\S\ref{output-format}) option is +enabled. + +\nopagebreak +{\small See also \textit{auto} (\S\ref{mode-of-operation}), +\textit{check\_potential} (\S\ref{authentication}), and +\textit{sat\_solver} (\S\ref{optimizations}).} + +\opt{max\_genuine}{int}{$\mathbf{1}$} +Specifies the maximum number of genuine counterexamples to display. If you set +this option to a value greater than 1, you will need an incremental SAT solver: +For efficiency, it is recommended to install the JNI version of MiniSat and set +\textit{sat\_solver} = \textit{MiniSatJNI}. Also be aware that many of the +counterexamples may look identical, unless the \textit{show\_all} +(\S\ref{output-format}) option is enabled. + +\nopagebreak +{\small See also \textit{check\_genuine} (\S\ref{authentication}) and +\textit{sat\_solver} (\S\ref{optimizations}).} + +\ops{eval}{term\_list} +Specifies the list of terms whose values should be displayed along with +counterexamples. This option suffers from an observer effect'': Nitpick might +find different counterexamples for different values of this option. + +\opu{format}{term}{int\_seq} +Specifies how to uncurry the value displayed for a variable or constant. +Uncurrying sometimes increases the readability of the output for high-arity +functions. For example, given the variable$y \mathbin{\Colon} {'a}\Rightarrow
+{'b}\Rightarrow {'c}\Rightarrow {'d}\Rightarrow {'e}\Rightarrow {'f}\Rightarrow
+{'g}$, setting \textit{format}~$y$= 3 tells Nitpick to group the last three +arguments, as if the type had been${'a}\Rightarrow {'b}\Rightarrow
+{'c}\Rightarrow {'d}\times {'e}\times {'f}\Rightarrow {'g}$. In general, a list +of values$n_1,\ldots,n_k$tells Nitpick to show the last$n_k$arguments as an +$n_k$-tuple, the previous$n_{k-1}$arguments as an$n_{k-1}$-tuple, and so on; +arguments that are not accounted for are left alone, as if the specification had +been$1,\ldots,1,n_1,\ldots,n_k$. + +\nopagebreak +{\small See also \textit{uncurry} (\S\ref{optimizations}).} + +\opt{format}{int\_seq}{$\mathbf{1}$} +Specifies the default format to use. Irrespective of the default format, the +extra arguments to a Skolem constant corresponding to the outer bound variables +are kept separated from the remaining arguments, the \textbf{for} arguments of +an inductive definitions are kept separated from the remaining arguments, and +the iteration counter of an unrolled inductive definition is shown alone. The +default format can be overridden on a per-variable or per-constant basis using +the \textit{format}~\qty{term} option described above. +\end{enum} + +%% MARK: Authentication +\subsection{Authentication} +\label{authentication} + +\begin{enum} +\opfalse{check\_potential}{trust\_potential} +Specifies whether potential counterexamples should be given to Isabelle's +\textit{auto} tactic to assess their validity. If a potential counterexample is +shown to be genuine, Nitpick displays a message to this effect and terminates. + +\nopagebreak +{\small See also \textit{max\_potential} (\S\ref{output-format}) and +\textit{auto\_timeout} (\S\ref{timeouts}).} + +\opfalse{check\_genuine}{trust\_genuine} +Specifies whether genuine and likely genuine counterexamples should be given to +Isabelle's \textit{auto} tactic to assess their validity. If a genuine'' +counterexample is shown to be spurious, the user is kindly asked to send a bug +report to the author at +\texttt{blan{\color{white}nospam}\kern-\wd\boxA{}chette@in.tum.de}. + +\nopagebreak +{\small See also \textit{max\_genuine} (\S\ref{output-format}) and +\textit{auto\_timeout} (\S\ref{timeouts}).} + +\ops{expect}{string} +Specifies the expected outcome, which must be one of the following: + +\begin{enum} +\item[$\bullet$] \textbf{\textit{genuine}}: Nitpick found a genuine counterexample. +\item[$\bullet$] \textbf{\textit{likely\_genuine}}: Nitpick found a likely +genuine'' counterexample (i.e., a counterexample that is genuine unless +it contradicts a missing axiom or a dangerous option was used inappropriately). +\item[$\bullet$] \textbf{\textit{potential}}: Nitpick found a potential counterexample. +\item[$\bullet$] \textbf{\textit{none}}: Nitpick found no counterexample. +\item[$\bullet$] \textbf{\textit{unknown}}: Nitpick encountered some problem (e.g., +Kodkod ran out of memory). +\end{enum} + +Nitpick emits an error if the actual outcome differs from the expected outcome. +This option is useful for regression testing. +\end{enum} + +\subsection{Optimizations} +\label{optimizations} + +\def\cpp{C\nobreak\raisebox{.1ex}{+}\nobreak\raisebox{.1ex}{+}} + +\sloppy + +\begin{enum} +\opt{sat\_solver}{string}{smart} +Specifies which SAT solver to use. SAT solvers implemented in C or \cpp{} tend +to be faster than their Java counterparts, but they can be more difficult to +install. Also, if you set the \textit{max\_potential} (\S\ref{output-format}) or +\textit{max\_genuine} (\S\ref{output-format}) option to a value greater than 1, +you will need an incremental SAT solver, such as \textit{MiniSatJNI} +(recommended) or \textit{SAT4J}. + +The supported solvers are listed below: + +\begin{enum} + +\item[$\bullet$] \textbf{\textit{MiniSat}}: MiniSat is an efficient solver +written in \cpp{}. To use MiniSat, set the environment variable +\texttt{MINISAT\_HOME} to the directory that contains the \texttt{minisat} +executable. The \cpp{} sources and executables for MiniSat are available at +\url{http://minisat.se/MiniSat.html}. Nitpick has been tested with versions 1.14 +and 2.0 beta (2007-07-21). + +\item[$\bullet$] \textbf{\textit{MiniSatJNI}}: The JNI (Java Native Interface) +version of MiniSat is bundled in \texttt{nativesolver.\allowbreak tgz}, which +you will find on Kodkod's web site \cite{kodkod-2009}. Unlike the standard +version of MiniSat, the JNI version can be used incrementally. + +\item[$\bullet$] \textbf{\textit{PicoSAT}}: PicoSAT is an efficient solver +written in C. It is bundled with Kodkodi and requires no further installation or +configuration steps. Alternatively, you can install a standard version of +PicoSAT and set the environment variable \texttt{PICOSAT\_HOME} to the directory +that contains the \texttt{picosat} executable. The C sources for PicoSAT are +available at \url{http://fmv.jku.at/picosat/} and are also bundled with Kodkodi. +Nitpick has been tested with version 913. + +\item[$\bullet$] \textbf{\textit{zChaff}}: zChaff is an efficient solver written +in \cpp{}. To use zChaff, set the environment variable \texttt{ZCHAFF\_HOME} to +the directory that contains the \texttt{zchaff} executable. The \cpp{} sources +and executables for zChaff are available at +\url{http://www.princeton.edu/~chaff/zchaff.html}. Nitpick has been tested with +versions 2004-05-13, 2004-11-15, and 2007-03-12. + +\item[$\bullet$] \textbf{\textit{zChaffJNI}}: The JNI version of zChaff is +bundled in \texttt{native\-solver.\allowbreak tgz}, which you will find on +Kodkod's web site \cite{kodkod-2009}. + +\item[$\bullet$] \textbf{\textit{RSat}}: RSat is an efficient solver written in +\cpp{}. To use RSat, set the environment variable \texttt{RSAT\_HOME} to the +directory that contains the \texttt{rsat} executable. The \cpp{} sources for +RSat are available at \url{http://reasoning.cs.ucla.edu/rsat/}. Nitpick has been +tested with version 2.01. + +\item[$\bullet$] \textbf{\textit{BerkMin}}: BerkMin561 is an efficient solver +written in C. To use BerkMin, set the environment variable +\texttt{BERKMIN\_HOME} to the directory that contains the \texttt{BerkMin561} +executable. The BerkMin executables are available at +\url{http://eigold.tripod.com/BerkMin.html}. + +\item[$\bullet$] \textbf{\textit{BerkMinAlloy}}: Variant of BerkMin that is +included with Alloy 4 and calls itself sat56'' in its banner text. To use this +version of BerkMin, set the environment variable +\texttt{BERKMINALLOY\_HOME} to the directory that contains the \texttt{berkmin} +executable. + +\item[$\bullet$] \textbf{\textit{Jerusat}}: Jerusat 1.3 is an efficient solver +written in C. To use Jerusat, set the environment variable +\texttt{JERUSAT\_HOME} to the directory that contains the \texttt{Jerusat1.3} +executable. The C sources for Jerusat are available at +\url{http://www.cs.tau.ac.il/~ale1/Jerusat1.3.tgz}. + +\item[$\bullet$] \textbf{\textit{SAT4J}}: SAT4J is a reasonably efficient solver +written in Java that can be used incrementally. It is bundled with Kodkodi and +requires no further installation or configuration steps. Do not attempt to +install the official SAT4J packages, because their API is incompatible with +Kodkod. + +\item[$\bullet$] \textbf{\textit{SAT4JLight}}: Variant of SAT4J that is +optimized for small problems. It can also be used incrementally. + +\item[$\bullet$] \textbf{\textit{HaifaSat}}: HaifaSat 1.0 beta is an +experimental solver written in \cpp. To use HaifaSat, set the environment +variable \texttt{HAIFASAT\_\allowbreak HOME} to the directory that contains the +\texttt{HaifaSat} executable. The \cpp{} sources for HaifaSat are available at +\url{http://cs.technion.ac.il/~gershman/HaifaSat.htm}. + +\item[$\bullet$] \textbf{\textit{smart}}: If \textit{sat\_solver} is set to +\textit{smart}, Nitpick selects the first solver among MiniSat, PicoSAT, zChaff, +RSat, BerkMin, BerkMinAlloy, and Jerusat that is recognized by Isabelle. If none +is found, it falls back on SAT4J, which should always be available. If +\textit{verbose} is enabled, Nitpick displays which SAT solver was chosen. + +\end{enum} +\fussy + +\opt{batch\_size}{int\_or\_smart}{smart} +Specifies the maximum number of Kodkod problems that should be lumped together +when invoking Kodkodi. Each problem corresponds to one scope. Lumping problems +together ensures that Kodkodi is launched less often, but it makes the verbose +output less readable and is sometimes detrimental to performance. If +\textit{batch\_size} is set to \textit{smart}, the actual value used is 1 if +\textit{debug} (\S\ref{output-format}) is set and 64 otherwise. + +\optrue{destroy\_constrs}{dont\_destroy\_constrs} +Specifies whether formulas involving (co)in\-duc\-tive datatype constructors should +be rewritten to use (automatically generated) discriminators and destructors. +This optimization can drastically reduce the size of the Boolean formulas given +to the SAT solver. + +\nopagebreak +{\small See also \textit{debug} (\S\ref{output-format}).} + +\optrue{specialize}{dont\_specialize} +Specifies whether functions invoked with static arguments should be specialized. +This optimization can drastically reduce the search space, especially for +higher-order functions. + +\nopagebreak +{\small See also \textit{debug} (\S\ref{output-format}) and +\textit{show\_consts} (\S\ref{output-format}).} + +\optrue{skolemize}{dont\_skolemize} +Specifies whether the formula should be skolemized. For performance reasons, +(positive)$\forall$-quanti\-fiers that occur in the scope of a higher-order +(positive)$\exists$-quanti\-fier are left unchanged. + +\nopagebreak +{\small See also \textit{debug} (\S\ref{output-format}) and +\textit{show\_skolems} (\S\ref{output-format}).} + +\optrue{star\_linear\_preds}{dont\_star\_linear\_preds} +Specifies whether Nitpick should use Kodkod's transitive closure operator to +encode non-well-founded linear inductive predicates,'' i.e., inductive +predicates for which each the predicate occurs in at most one assumption of each +introduction rule. Using the reflexive transitive closure is in principle +equivalent to setting \textit{iter} to the cardinality of the predicate's +domain, but it is usually more efficient. + +{\small See also \textit{wf} (\S\ref{scope-of-search}), \textit{debug} +(\S\ref{output-format}), and \textit{iter} (\S\ref{scope-of-search}).} + +\optrue{uncurry}{dont\_uncurry} +Specifies whether Nitpick should uncurry functions. Uncurrying has on its own no +tangible effect on efficiency, but it creates opportunities for the boxing +optimization. + +\nopagebreak +{\small See also \textit{box} (\S\ref{scope-of-search}), \textit{debug} +(\S\ref{output-format}), and \textit{format} (\S\ref{output-format}).} + +\optrue{fast\_descrs}{full\_descrs} +Specifies whether Nitpick should optimize the definite and indefinite +description operators (THE and SOME). The optimized versions usually help +Nitpick generate more counterexamples or at least find them faster, but only the +unoptimized versions are complete when all types occurring in the formula are +finite. + +{\small See also \textit{debug} (\S\ref{output-format}).} + +\optrue{peephole\_optim}{no\_peephole\_optim} +Specifies whether Nitpick should simplify the generated Kodkod formulas using a +peephole optimizer. These optimizations can make a significant difference. +Unless you are tracking down a bug in Nitpick or distrust the peephole +optimizer, you should leave this option enabled. + +\opt{sym\_break}{int}{20} +Specifies an upper bound on the number of relations for which Kodkod generates +symmetry breaking predicates. According to the Kodkod documentation +\cite{kodkod-2009-options}, in general, the higher this value, the more +symmetries will be broken, and the faster the formula will be solved. But, +setting the value too high may have the opposite effect and slow down the +solving.'' + +\opt{sharing\_depth}{int}{3} +Specifies the depth to which Kodkod should check circuits for equivalence during +the translation to SAT. The default of 3 is the same as in Alloy. The minimum +allowed depth is 1. Increasing the sharing may result in a smaller SAT problem, +but can also slow down Kodkod. + +\opfalse{flatten\_props}{dont\_flatten\_props} +Specifies whether Kodkod should try to eliminate intermediate Boolean variables. +Although this might sound like a good idea, in practice it can drastically slow +down Kodkod. + +\opt{max\_threads}{int}{0} +Specifies the maximum number of threads to use in Kodkod. If this option is set +to 0, Kodkod will compute an appropriate value based on the number of processor +cores available. + +\nopagebreak +{\small See also \textit{batch\_size} (\S\ref{optimizations}) and +\textit{timeout} (\S\ref{timeouts}).} +\end{enum} + +\subsection{Timeouts} +\label{timeouts} + +\begin{enum} +\opt{timeout}{time}{$\mathbf{30}$s} +Specifies the maximum amount of time that the \textbf{nitpick} command should +spend looking for a counterexample. Nitpick tries to honor this constraint as +well as it can but offers no guarantees. For automatic runs, +\textit{auto\_timeout} is used instead. + +\nopagebreak +{\small See also \textit{auto} (\S\ref{mode-of-operation}) +and \textit{max\_threads} (\S\ref{optimizations}).} + +\opt{auto\_timeout}{time}{$\mathbf{5}$s} +Specifies the maximum amount of time that Nitpick should use to find a +counterexample when running automatically. Nitpick tries to honor this +constraint as well as it can but offers no guarantees. + +\nopagebreak +{\small See also \textit{auto} (\S\ref{mode-of-operation}).} + +\opt{tac\_timeout}{time}{$\mathbf{500}$ms} +Specifies the maximum amount of time that the \textit{auto} tactic should use +when checking a counterexample, and similarly that \textit{lexicographic\_order} +and \textit{sizechange} should use when checking whether a (co)in\-duc\-tive +predicate is well-founded. Nitpick tries to honor this constraint as well as it +can but offers no guarantees. + +\nopagebreak +{\small See also \textit{wf} (\S\ref{scope-of-search}), +\textit{check\_potential} (\S\ref{authentication}), +and \textit{check\_genuine} (\S\ref{authentication}).} +\end{enum} + +\section{Attribute Reference} +\label{attribute-reference} + +Nitpick needs to consider the definitions of all constants occurring in a +formula in order to falsify it. For constants introduced using the +\textbf{definition} command, the definition is simply the associated +\textit{\_def} axiom. In contrast, instead of using the internal representation +of functions synthesized by Isabelle's \textbf{primrec}, \textbf{function}, and +\textbf{nominal\_primrec} packages, Nitpick relies on the more natural +equational specification entered by the user. + +Behind the scenes, Isabelle's built-in packages and theories rely on the +following attributes to affect Nitpick's behavior: + +\begin{itemize} +\flushitem{\textit{nitpick\_def}} + +\nopagebreak +This attribute specifies an alternative definition of a constant. The +alternative definition should be logically equivalent to the constant's actual +axiomatic definition and should be of the form + +\qquad$c~{?}x_1~\ldots~{?}x_n \,\equiv\, t$, + +where${?}x_1, \ldots, {?}x_n$are distinct variables and$c$does not occur in +$t$. + +\flushitem{\textit{nitpick\_simp}} + +\nopagebreak +This attribute specifies the equations that constitute the specification of a +constant. For functions defined using the \textbf{primrec}, \textbf{function}, +and \textbf{nominal\_\allowbreak primrec} packages, this corresponds to the +\textit{simps} rules. The equations must be of the form + +\qquad$c~t_1~\ldots\ t_n \,=\, u.$+ +\flushitem{\textit{nitpick\_psimp}} + +\nopagebreak +This attribute specifies the equations that constitute the partial specification +of a constant. For functions defined using the \textbf{function} package, this +corresponds to the \textit{psimps} rules. The conditional equations must be of +the form + +\qquad$\lbrakk P_1;\> \ldots;\> P_m\rbrakk \,\Longrightarrow\, c\ t_1\ \ldots\ t_n \,=\, u$. + +\flushitem{\textit{nitpick\_intro}} + +\nopagebreak +This attribute specifies the introduction rules of a (co)in\-duc\-tive predicate. +For predicates defined using the \textbf{inductive} or \textbf{coinductive} +command, this corresponds to the \textit{intros} rules. The introduction rules +must be of the form + +\qquad$\lbrakk P_1;\> \ldots;\> P_m;\> M~(c\ t_{11}\ \ldots\ t_{1n});\>
+\ldots;\> M~(c\ t_{k1}\ \ldots\ t_{kn})\rbrakk \,\Longrightarrow\, c\ u_1\
+\ldots\ u_n$, + +where the$P_i$'s are side conditions that do not involve$c$and$M$is an +optional monotonic operator. The order of the assumptions is irrelevant. + +\end{itemize} + +When faced with a constant, Nitpick proceeds as follows: + +\begin{enum} +\item[1.] If the \textit{nitpick\_simp} set associated with the constant +is not empty, Nitpick uses these rules as the specification of the constant. + +\item[2.] Otherwise, if the \textit{nitpick\_psimp} set associated with +the constant is not empty, it uses these rules as the specification of the +constant. + +\item[3.] Otherwise, it looks up the definition of the constant: + +\begin{enum} +\item[1.] If the \textit{nitpick\_def} set associated with the constant +is not empty, it uses the latest rule added to the set as the definition of the +constant; otherwise it uses the actual definition axiom. +\item[2.] If the definition is of the form + +\qquad$c~{?}x_1~\ldots~{?}x_m \,\equiv\, \lambda y_1~\ldots~y_n.\; \textit{lfp}~(\lambda f.\; t)$, + +then Nitpick assumes that the definition was made using an inductive package and +based on the introduction rules marked with \textit{nitpick\_\allowbreak +ind\_\allowbreak intros} tries to determine whether the definition is +well-founded. +\end{enum} +\end{enum} + +As an illustration, consider the inductive definition + +\prew +\textbf{inductive}~\textit{odd}~\textbf{where} \\ +\textit{odd}~1''$\,\mid$\\ +\textit{odd}~$n\,\Longrightarrow\, \textit{odd}~(\textit{Suc}~(\textit{Suc}~n))$'' +\postw + +Isabelle automatically attaches the \textit{nitpick\_intro} attribute to +the above rules. Nitpick then uses the \textit{lfp}-based definition in +conjunction with these rules. To override this, we can specify an alternative +definition as follows: + +\prew +\textbf{lemma}$\mathit{odd\_def}'$[\textit{nitpick\_def}]: $\textit{odd}~n \,\equiv\, n~\textrm{mod}~2 = 1$'' +\postw + +Nitpick then expands all occurrences of$\mathit{odd}~n$to$n~\textrm{mod}~2
+= 1$. Alternatively, we can specify an equational specification of the constant: + +\prew +\textbf{lemma}$\mathit{odd\_simp}'$[\textit{nitpick\_simp}]: $\textit{odd}~n = (n~\textrm{mod}~2 = 1)$'' +\postw + +Such tweaks should be done with great care, because Nitpick will assume that the +constant is completely defined by its equational specification. For example, if +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 +$\textit{odd}~n$arbitrarily for even values of$n$. The \textit{debug} +(\S\ref{output-format}) option is extremely useful to understand what is going +on when experimenting with \textit{nitpick\_} attributes. + +\section{Standard ML Interface} +\label{standard-ml-interface} + +Nitpick provides a rich Standard ML interface used mainly for internal purposes +and debugging. Among the most interesting functions exported by Nitpick are +those that let you invoke the tool programmatically and those that let you +register and unregister custom coinductive datatypes. + +\subsection{Invocation of Nitpick} +\label{invocation-of-nitpick} + +The \textit{Nitpick} structure offers the following functions for invoking your +favorite counterexample generator: + +\prew +$\textbf{val}\,~\textit{pick\_nits\_in\_term} : \\
+\hbox{}\quad\textit{Proof.state} \rightarrow \textit{params} \rightarrow \textit{bool} \rightarrow \textit{term~list} \rightarrow \textit{term} \\
+\hbox{}\quad{\rightarrow}\; \textit{string} * \textit{Proof.state}$\\ +$\textbf{val}\,~\textit{pick\_nits\_in\_subgoal} : \\
+\hbox{}\quad\textit{Proof.state} \rightarrow \textit{params} \rightarrow \textit{bool} \rightarrow \textit{int} \rightarrow \textit{string} * \textit{Proof.state}$+\postw + +The return value is a new proof state paired with an outcome string +(genuine'', likely\_genuine'', potential'', none'', or unknown''). The +\textit{params} type is a large record that lets you set Nitpick's options. The +current default options can be retrieved by calling the following function +defined in the \textit{NitpickIsar} structure: + +\prew +$\textbf{val}\,~\textit{default\_params} :\,
+\textit{theory} \rightarrow (\textit{string} * \textit{string})~\textit{list} \rightarrow \textit{params}$+\postw + +The second argument lets you override option values before they are parsed and +put into a \textit{params} record. Here is an example: + +\prew +$\textbf{val}\,~\textit{params} = \textit{NitpickIsar.default\_params}~\textit{thy}~[(\textrm{}\textrm{timeout}\textrm{''},\, \textrm{}\textrm{none}\textrm{''})]$\\ +$\textbf{val}\,~(\textit{outcome},\, \textit{state}') = \textit{Nitpick.pick\_nits\_in\_subgoal}~\begin{aligned}[t]
+& \textit{state}~\textit{params}~\textit{false} \\[-2pt]
+& \textit{subgoal}\end{aligned}$+\postw + +\subsection{Registration of Coinductive Datatypes} +\label{registration-of-coinductive-datatypes} + +\let\antiq=\textrm + +If you have defined a custom coinductive datatype, you can tell Nitpick about +it, so that it can use an efficient Kodkod axiomatization similar to the one it +uses for lazy lists. The interface for registering and unregistering coinductive +datatypes consists of the following pair of functions defined in the +\textit{Nitpick} structure: + +\prew +$\textbf{val}\,~\textit{register\_codatatype} :\,
+\textit{typ} \rightarrow \textit{string} \rightarrow \textit{styp~list} \rightarrow \textit{theory} \rightarrow \textit{theory}$\\ +$\textbf{val}\,~\textit{unregister\_codatatype} :\,
+\textit{typ} \rightarrow \textit{theory} \rightarrow \textit{theory}$+\postw + +The type$'a~\textit{llist}$of lazy lists is already registered; had it +not been, you could have told Nitpick about it by adding the following line +to your theory file: + +\prew +$\textbf{setup}~\,\{{*}\,~\!\begin{aligned}[t]
+& \textit{Nitpick.register\_codatatype} \\[-2pt]
+& \qquad @\{\antiq{typ}~\kern1pt'a~\textit{llist}\textrm{''}\}~@\{\antiq{const\_name}~ \textit{llist\_case}\} \\[-2pt] %% TYPESETTING
+& \qquad (\textit{map}~\textit{dest\_Const}~[@\{\antiq{term}~\textit{LNil}\},\, @\{\antiq{term}~\textit{LCons}\}])\,\ {*}\}\end{aligned}$+\postw + +The \textit{register\_codatatype} function takes a coinductive type, its case +function, and the list of its constructors. The case function must take its +arguments in the order that the constructors are listed. If no case function +with the correct signature is available, simply pass the empty string. + +On the other hand, if your goal is to cripple Nitpick, add the following line to +your theory file and try to check a few conjectures about lazy lists: + +\prew +$\textbf{setup}~\,\{{*}\,~\textit{Nitpick.unregister\_codatatype}~@\{\antiq{typ}~
+\kern1pt'a~\textit{list}\textrm{''}\}\ \,{*}\}$+\postw + +\section{Known Bugs and Limitations} +\label{known-bugs-and-limitations} + +Here are the known bugs and limitations in Nitpick at the time of writing: + +\begin{enum} +\item[$\bullet$] Underspecified functions defined using the \textbf{primrec}, +\textbf{function}, or \textbf{nominal\_\allowbreak primrec} packages can lead +Nitpick to generate spurious counterexamples for theorems that refer to values +for which the function is not defined. For example: + +\prew +\textbf{primrec} \textit{prec} \textbf{where} \\ +$\textit{prec}~(\textit{Suc}~n) = n$'' \\[2\smallskipamount] +\textbf{lemma} $\textit{prec}~0 = \undef$'' \\ +\textbf{nitpick} \\[2\smallskipamount] +\quad{\slshape Nitpick found a counterexample for \textit{card nat}~= 2: +\nopagebreak +\\[2\smallskipamount] +\hbox{}\qquad Empty assignment} \nopagebreak\\[2\smallskipamount] +\textbf{by}~(\textit{auto simp}: \textit{prec\_def}) +\postw + +Such theorems are considered bad style because they rely on the internal +representation of functions synthesized by Isabelle, which is an implementation +detail. + +\item[$\bullet$] Nitpick produces spurious counterexamples when invoked after a +\textbf{guess} command in a structured proof. + +\item[$\bullet$] The \textit{nitpick\_} attributes and the +\textit{Nitpick.register\_} functions can cause havoc if used improperly. + +\item[$\bullet$] Local definitions are not supported and result in an error. + +\item[$\bullet\$] All constants and types whose names start with
+\textit{Nitpick}{.} or \textit{NitpickDefs}{.} are reserved for internal use.
+\end{enum}
+
+\let\em=\sl
+\bibliography{../manual}{}
+\bibliographystyle{abbrv}
+
+\end{document}