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