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