1.1 --- a/doc-src/Nitpick/nitpick.tex Thu Mar 11 12:22:11 2010 +0100
1.2 +++ b/doc-src/Nitpick/nitpick.tex Thu Mar 11 15:33:45 2010 +0100
1.3 @@ -137,8 +137,8 @@
1.4 suggesting several textual improvements.
1.5 % and Perry James for reporting a typo.
1.6
1.7 -\section{Overview}
1.8 -\label{overview}
1.9 +\section{First Steps}
1.10 +\label{first-steps}
1.11
1.12 This section introduces Nitpick by presenting small examples. If possible, you
1.13 should try out the examples on your workstation. Your theory file should start
1.14 @@ -472,7 +472,7 @@
1.15
1.16 \prew
1.17 \textbf{lemma} ``$\forall n.\; \textit{Suc}~n \mathbin{\not=} n \,\Longrightarrow\, P$'' \\
1.18 -\textbf{nitpick} [\textit{card~nat}~= 100, \textit{check\_potential}] \\[2\smallskipamount]
1.19 +\textbf{nitpick} [\textit{card~nat}~= 50, \textit{check\_potential}] \\[2\smallskipamount]
1.20 \slshape Warning: The conjecture either trivially holds for the given scopes or lies outside Nitpick's supported
1.21 fragment. Only potential counterexamples may be found. \\[2\smallskipamount]
1.22 Nitpick found a potential counterexample: \\[2\smallskipamount]
1.23 @@ -629,7 +629,7 @@
1.24 unlikely that one could be found for smaller cardinalities.
1.25
1.26 \subsection{Typedefs, Quotient Types, Records, Rationals, and Reals}
1.27 -\label{typedefs-records-rationals-and-reals}
1.28 +\label{typedefs-quotient-types-records-rationals-and-reals}
1.29
1.30 Nitpick generally treats types declared using \textbf{typedef} as datatypes
1.31 whose single constructor is the corresponding \textit{Abs\_\kern.1ex} function.
1.32 @@ -684,7 +684,26 @@
1.33
1.34 In the counterexample, $\Abs{(0,\, 0)}$ and $\Abs{(1,\, 0)}$ represent the
1.35 integers $0$ and $1$, respectively. Other representants would have been
1.36 -possible---e.g., $\Abs{(5,\, 5)}$ and $\Abs{(12,\, 11)}$.
1.37 +possible---e.g., $\Abs{(5,\, 5)}$ and $\Abs{(12,\, 11)}$. If we are going to
1.38 +use \textit{my\_int} extensively, it pays off to install a term postprocessor
1.39 +that converts the pair notation to the standard mathematical notation:
1.40 +
1.41 +\prew
1.42 +$\textbf{ML}~\,\{{*} \\
1.43 +\!\begin{aligned}[t]
1.44 +%& ({*}~\,\textit{Proof.context} \rightarrow \textit{string} \rightarrow (\textit{typ} \rightarrow \textit{term~list\/}) \rightarrow \textit{typ} \rightarrow \textit{term} \\[-2pt]
1.45 +%& \phantom{(*}~\,{\rightarrow}\;\textit{term}~\,{*}) \\[-2pt]
1.46 +& \textbf{fun}\,~\textit{my\_int\_postproc}~\_~\_~\_~T~(\textit{Const}~\_~\$~(\textit{Const}~\_~\$~\textit{t1}~\$~\textit{t2\/})) = {} \\[-2pt]
1.47 +& \phantom{fun}\,~\textit{HOLogic.mk\_number}~T~(\textit{snd}~(\textit{HOLogic.dest\_number~t1}) \\[-2pt]
1.48 +& \phantom{fun\,~\textit{HOLogic.mk\_number}~T~(}{-}~\textit{snd}~(\textit{HOLogic.dest\_number~t2\/})) \\[-2pt]
1.49 +& \phantom{fun}\!{\mid}\,~\textit{my\_int\_postproc}~\_~\_~\_~\_~t = t \\[-2pt]
1.50 +{*}\}\end{aligned}$ \\[2\smallskipamount]
1.51 +$\textbf{setup}~\,\{{*} \\
1.52 +\!\begin{aligned}[t]
1.53 +& \textit{Nitpick.register\_term\_postprocessor}~\!\begin{aligned}[t]
1.54 + & @\{\textrm{typ}~\textit{my\_int}\}~\textit{my\_int\_postproc}\end{aligned} \\[-2pt]
1.55 +{*}\}\end{aligned}$
1.56 +\postw
1.57
1.58 Records are also handled as datatypes with a single constructor:
1.59
1.60 @@ -771,25 +790,25 @@
1.61
1.62 \prew
1.63 \textbf{lemma} ``$\exists n.\; \textit{even}~n \mathrel{\land} \textit{even}~(\textit{Suc}~n)$'' \\
1.64 -\textbf{nitpick}~[\textit{card nat}~= 100, \textit{unary\_ints}, \textit{verbose}] \\[2\smallskipamount]
1.65 +\textbf{nitpick}~[\textit{card nat}~= 50, \textit{unary\_ints}, \textit{verbose}] \\[2\smallskipamount]
1.66 \slshape The inductive predicate ``\textit{even}'' was proved well-founded.
1.67 Nitpick can compute it efficiently. \\[2\smallskipamount]
1.68 Trying 1 scope: \\
1.69 -\hbox{}\qquad \textit{card nat}~= 100. \\[2\smallskipamount]
1.70 -Nitpick found a potential counterexample for \textit{card nat}~= 100: \\[2\smallskipamount]
1.71 +\hbox{}\qquad \textit{card nat}~= 50. \\[2\smallskipamount]
1.72 +Nitpick found a potential counterexample for \textit{card nat}~= 50: \\[2\smallskipamount]
1.73 \hbox{}\qquad Empty assignment \\[2\smallskipamount]
1.74 Nitpick could not find a better counterexample. \\[2\smallskipamount]
1.75 Total time: 2274 ms.
1.76 \postw
1.77
1.78 No genuine counterexample is possible because Nitpick cannot rule out the
1.79 -existence of a natural number $n \ge 100$ such that both $\textit{even}~n$ and
1.80 +existence of a natural number $n \ge 50$ such that both $\textit{even}~n$ and
1.81 $\textit{even}~(\textit{Suc}~n)$ are true. To help Nitpick, we can bound the
1.82 existential quantifier:
1.83
1.84 \prew
1.85 -\textbf{lemma} ``$\exists n \mathbin{\le} 99.\; \textit{even}~n \mathrel{\land} \textit{even}~(\textit{Suc}~n)$'' \\
1.86 -\textbf{nitpick}~[\textit{card nat}~= 100, \textit{unary\_ints}] \\[2\smallskipamount]
1.87 +\textbf{lemma} ``$\exists n \mathbin{\le} 49.\; \textit{even}~n \mathrel{\land} \textit{even}~(\textit{Suc}~n)$'' \\
1.88 +\textbf{nitpick}~[\textit{card nat}~= 50, \textit{unary\_ints}] \\[2\smallskipamount]
1.89 \slshape Nitpick found a counterexample: \\[2\smallskipamount]
1.90 \hbox{}\qquad Empty assignment
1.91 \postw
1.92 @@ -1211,26 +1230,26 @@
1.93 Trying 8 scopes: \\
1.94 \hbox{}\qquad \textit{card} $'a$~= 1, \textit{card} $'b$~= 1,
1.95 \textit{card} \textit{nat}~= 1, \textit{card} ``$('a \times {'}b)$
1.96 -\textit{list}''~= 1, \\
1.97 -\hbox{}\qquad\quad \textit{card} ``\kern1pt$'a$ \textit{list}''~= 1, and
1.98 -\textit{card} ``\kern1pt$'b$ \textit{list}''~= 1. \\
1.99 +\textit{list\/}''~= 1, \\
1.100 +\hbox{}\qquad\quad \textit{card} ``\kern1pt$'a$ \textit{list\/}''~= 1, and
1.101 +\textit{card} ``\kern1pt$'b$ \textit{list\/}''~= 1. \\
1.102 \hbox{}\qquad \textit{card} $'a$~= 2, \textit{card} $'b$~= 2,
1.103 \textit{card} \textit{nat}~= 2, \textit{card} ``$('a \times {'}b)$
1.104 -\textit{list}''~= 2, \\
1.105 -\hbox{}\qquad\quad \textit{card} ``\kern1pt$'a$ \textit{list}''~= 2, and
1.106 -\textit{card} ``\kern1pt$'b$ \textit{list}''~= 2. \\
1.107 +\textit{list\/}''~= 2, \\
1.108 +\hbox{}\qquad\quad \textit{card} ``\kern1pt$'a$ \textit{list\/}''~= 2, and
1.109 +\textit{card} ``\kern1pt$'b$ \textit{list\/}''~= 2. \\
1.110 \hbox{}\qquad $\qquad\vdots$ \\[.5\smallskipamount]
1.111 \hbox{}\qquad \textit{card} $'a$~= 8, \textit{card} $'b$~= 8,
1.112 \textit{card} \textit{nat}~= 8, \textit{card} ``$('a \times {'}b)$
1.113 -\textit{list}''~= 8, \\
1.114 -\hbox{}\qquad\quad \textit{card} ``\kern1pt$'a$ \textit{list}''~= 8, and
1.115 -\textit{card} ``\kern1pt$'b$ \textit{list}''~= 8.
1.116 +\textit{list\/}''~= 8, \\
1.117 +\hbox{}\qquad\quad \textit{card} ``\kern1pt$'a$ \textit{list\/}''~= 8, and
1.118 +\textit{card} ``\kern1pt$'b$ \textit{list\/}''~= 8.
1.119 \\[2\smallskipamount]
1.120 Nitpick found a counterexample for
1.121 \textit{card} $'a$~= 5, \textit{card} $'b$~= 5,
1.122 \textit{card} \textit{nat}~= 5, \textit{card} ``$('a \times {'}b)$
1.123 -\textit{list}''~= 5, \textit{card} ``\kern1pt$'a$ \textit{list}''~= 5, and
1.124 -\textit{card} ``\kern1pt$'b$ \textit{list}''~= 5:
1.125 +\textit{list\/}''~= 5, \textit{card} ``\kern1pt$'a$ \textit{list\/}''~= 5, and
1.126 +\textit{card} ``\kern1pt$'b$ \textit{list\/}''~= 5:
1.127 \\[2\smallskipamount]
1.128 \hbox{}\qquad Free variables: \nopagebreak \\
1.129 \hbox{}\qquad\qquad $\textit{xs} = [a_1, a_2]$ \\
1.130 @@ -1851,7 +1870,7 @@
1.131 The number of options can be overwhelming at first glance. Do not let that worry
1.132 you: Nitpick's defaults have been chosen so that it almost always does the right
1.133 thing, and the most important options have been covered in context in
1.134 -\S\ref{overview}.
1.135 +\S\ref{first-steps}.
1.136
1.137 The descriptions below refer to the following syntactic quantities:
1.138
1.139 @@ -2622,7 +2641,7 @@
1.140
1.141 then Nitpick assumes that the definition was made using an inductive package and
1.142 based on the introduction rules marked with \textit{nitpick\_\allowbreak
1.143 -ind\_\allowbreak intros} tries to determine whether the definition is
1.144 +\allowbreak intros} tries to determine whether the definition is
1.145 well-founded.
1.146 \end{enum}
1.147 \end{enum}
1.148 @@ -2664,7 +2683,8 @@
1.149 Nitpick provides a rich Standard ML interface used mainly for internal purposes
1.150 and debugging. Among the most interesting functions exported by Nitpick are
1.151 those that let you invoke the tool programmatically and those that let you
1.152 -register and unregister custom coinductive datatypes.
1.153 +register and unregister custom coinductive datatypes as well as term
1.154 +postprocessors.
1.155
1.156 \subsection{Invocation of Nitpick}
1.157 \label{invocation-of-nitpick}
1.158 @@ -2695,7 +2715,7 @@
1.159 put into a \textit{params} record. Here is an example:
1.160
1.161 \prew
1.162 -$\textbf{val}\,~\textit{params} = \textit{Nitpick\_Isar.default\_params}~\textit{thy}~[(\textrm{``}\textrm{timeout}\textrm{''},\, \textrm{``}\textrm{none}\textrm{''})]$ \\
1.163 +$\textbf{val}\,~\textit{params} = \textit{Nitpick\_Isar.default\_params}~\textit{thy}~[(\textrm{``}\textrm{timeout\/}\textrm{''},\, \textrm{``}\textrm{none}\textrm{''})]$ \\
1.164 $\textbf{val}\,~(\textit{outcome},\, \textit{state}') = \textit{Nitpick.pick\_nits\_in\_subgoal}~\begin{aligned}[t]
1.165 & \textit{state}~\textit{params}~\textit{false} \\[-2pt]
1.166 & \textit{subgoal}\end{aligned}$
1.167 @@ -2726,7 +2746,7 @@
1.168 \prew
1.169 $\textbf{setup}~\,\{{*}\,~\!\begin{aligned}[t]
1.170 & \textit{Nitpick.register\_codatatype} \\[-2pt]
1.171 -& \qquad @\{\antiq{typ}~``\kern1pt'a~\textit{llist}\textrm{''}\}~@\{\antiq{const\_name}~ \textit{llist\_case}\} \\[-2pt] %% TYPESETTING
1.172 +& \qquad @\{\antiq{typ}~``\kern1pt'a~\textit{llist\/}\textrm{''}\}~@\{\antiq{const\_name}~ \textit{llist\_case}\} \\[-2pt] %% TYPESETTING
1.173 & \qquad (\textit{map}~\textit{dest\_Const}~[@\{\antiq{term}~\textit{LNil}\},\, @\{\antiq{term}~\textit{LCons}\}])\,\ {*}\}\end{aligned}$
1.174 \postw
1.175
1.176 @@ -2740,7 +2760,7 @@
1.177
1.178 \prew
1.179 $\textbf{setup}~\,\{{*}\,~\textit{Nitpick.unregister\_codatatype}~@\{\antiq{typ}~``
1.180 -\kern1pt'a~\textit{list}\textrm{''}\}\ \,{*}\}$
1.181 +\kern1pt'a~\textit{list\/}\textrm{''}\}\ \,{*}\}$
1.182 \postw
1.183
1.184 Inductive datatypes can be registered as coinductive datatypes, given
1.185 @@ -2748,6 +2768,26 @@
1.186 the use of the inductive constructors---Nitpick will generate an error if they
1.187 are needed.
1.188
1.189 +\subsection{Registration of Term Postprocessors}
1.190 +\label{registration-of-term-postprocessors}
1.191 +
1.192 +It is possible to change the output of any term that Nitpick considers a
1.193 +datatype by registering a term postprocessor. The interface for registering and
1.194 +unregistering postprocessors consists of the following pair of functions defined
1.195 +in the \textit{Nitpick} structure:
1.196 +
1.197 +\prew
1.198 +$\textbf{type}\,~\textit{term\_postprocessor}\,~{=} {}$ \\
1.199 +$\hbox{}\quad\textit{Proof.context} \rightarrow \textit{string} \rightarrow (\textit{typ} \rightarrow \textit{term~list\/}) \rightarrow \textit{typ} \rightarrow \textit{term} \rightarrow \textit{term}$ \\
1.200 +$\textbf{val}\,~\textit{register\_term\_postprocessors} : {}$ \\
1.201 +$\hbox{}\quad\textit{typ} \rightarrow \textit{term\_postprocessor} \rightarrow \textit{theory} \rightarrow \textit{theory}$ \\
1.202 +$\textbf{val}\,~\textit{unregister\_term\_postprocessors} :\,
1.203 +\textit{typ} \rightarrow \textit{theory} \rightarrow \textit{theory}$
1.204 +\postw
1.205 +
1.206 +\S\ref{typedefs-quotient-types-records-rationals-and-reals} and
1.207 +\texttt{src/HOL/Library/Multiset.thy} illustrate this feature in context.
1.208 +
1.209 \section{Known Bugs and Limitations}
1.210 \label{known-bugs-and-limitations}
1.211