diff -r 548d3f16404b -r 77aa29bf14ee doc-src/Nitpick/nitpick.tex --- a/doc-src/Nitpick/nitpick.tex Thu Mar 11 12:22:11 2010 +0100 +++ b/doc-src/Nitpick/nitpick.tex Thu Mar 11 15:33:45 2010 +0100 @@ -137,8 +137,8 @@ suggesting several textual improvements. % and Perry James for reporting a typo. -\section{Overview} -\label{overview} +\section{First Steps} +\label{first-steps} This section introduces Nitpick by presenting small examples. If possible, you should try out the examples on your workstation. Your theory file should start @@ -472,7 +472,7 @@ \prew \textbf{lemma} ``$\forall n.\; \textit{Suc}~n \mathbin{\not=} n \,\Longrightarrow\, P$'' \\ -\textbf{nitpick} [\textit{card~nat}~= 100, \textit{check\_potential}] \\[2\smallskipamount] +\textbf{nitpick} [\textit{card~nat}~= 50, \textit{check\_potential}] \\[2\smallskipamount] \slshape Warning: The conjecture either trivially holds for the given scopes or lies outside Nitpick's supported fragment. Only potential counterexamples may be found. \\[2\smallskipamount] Nitpick found a potential counterexample: \\[2\smallskipamount] @@ -629,7 +629,7 @@ unlikely that one could be found for smaller cardinalities. \subsection{Typedefs, Quotient Types, Records, Rationals, and Reals} -\label{typedefs-records-rationals-and-reals} +\label{typedefs-quotient-types-records-rationals-and-reals} Nitpick generally treats types declared using \textbf{typedef} as datatypes whose single constructor is the corresponding \textit{Abs\_\kern.1ex} function. @@ -684,7 +684,26 @@ In the counterexample, $\Abs{(0,\, 0)}$ and $\Abs{(1,\, 0)}$ represent the integers $0$ and $1$, respectively. Other representants would have been -possible---e.g., $\Abs{(5,\, 5)}$ and $\Abs{(12,\, 11)}$. +possible---e.g., $\Abs{(5,\, 5)}$ and $\Abs{(12,\, 11)}$. If we are going to +use \textit{my\_int} extensively, it pays off to install a term postprocessor +that converts the pair notation to the standard mathematical notation: + +\prew +$\textbf{ML}~\,\{{*} \\ +\!\begin{aligned}[t] +%& ({*}~\,\textit{Proof.context} \rightarrow \textit{string} \rightarrow (\textit{typ} \rightarrow \textit{term~list\/}) \rightarrow \textit{typ} \rightarrow \textit{term} \\[-2pt] +%& \phantom{(*}~\,{\rightarrow}\;\textit{term}~\,{*}) \\[-2pt] +& \textbf{fun}\,~\textit{my\_int\_postproc}~\_~\_~\_~T~(\textit{Const}~\_~\$~(\textit{Const}~\_~\$~\textit{t1}~\$~\textit{t2\/})) = {} \\[-2pt] +& \phantom{fun}\,~\textit{HOLogic.mk\_number}~T~(\textit{snd}~(\textit{HOLogic.dest\_number~t1}) \\[-2pt] +& \phantom{fun\,~\textit{HOLogic.mk\_number}~T~(}{-}~\textit{snd}~(\textit{HOLogic.dest\_number~t2\/})) \\[-2pt] +& \phantom{fun}\!{\mid}\,~\textit{my\_int\_postproc}~\_~\_~\_~\_~t = t \\[-2pt] +{*}\}\end{aligned}$ \\[2\smallskipamount] +$\textbf{setup}~\,\{{*} \\ +\!\begin{aligned}[t] +& \textit{Nitpick.register\_term\_postprocessor}~\!\begin{aligned}[t] + & @\{\textrm{typ}~\textit{my\_int}\}~\textit{my\_int\_postproc}\end{aligned} \\[-2pt] +{*}\}\end{aligned}$ +\postw Records are also handled as datatypes with a single constructor: @@ -771,25 +790,25 @@ \prew \textbf{lemma} ``$\exists n.\; \textit{even}~n \mathrel{\land} \textit{even}~(\textit{Suc}~n)$'' \\ -\textbf{nitpick}~[\textit{card nat}~= 100, \textit{unary\_ints}, \textit{verbose}] \\[2\smallskipamount] +\textbf{nitpick}~[\textit{card nat}~= 50, \textit{unary\_ints}, \textit{verbose}] \\[2\smallskipamount] \slshape The inductive predicate ``\textit{even}'' was proved well-founded. Nitpick can compute it efficiently. \\[2\smallskipamount] Trying 1 scope: \\ -\hbox{}\qquad \textit{card nat}~= 100. \\[2\smallskipamount] -Nitpick found a potential counterexample for \textit{card nat}~= 100: \\[2\smallskipamount] +\hbox{}\qquad \textit{card nat}~= 50. \\[2\smallskipamount] +Nitpick found a potential counterexample for \textit{card nat}~= 50: \\[2\smallskipamount] \hbox{}\qquad Empty assignment \\[2\smallskipamount] Nitpick could not find a better counterexample. \\[2\smallskipamount] Total time: 2274 ms. \postw No genuine counterexample is possible because Nitpick cannot rule out the -existence of a natural number $n \ge 100$ such that both $\textit{even}~n$ and +existence of a natural number $n \ge 50$ such that both $\textit{even}~n$ and $\textit{even}~(\textit{Suc}~n)$ are true. To help Nitpick, we can bound the existential quantifier: \prew -\textbf{lemma} ``$\exists n \mathbin{\le} 99.\; \textit{even}~n \mathrel{\land} \textit{even}~(\textit{Suc}~n)$'' \\ -\textbf{nitpick}~[\textit{card nat}~= 100, \textit{unary\_ints}] \\[2\smallskipamount] +\textbf{lemma} ``$\exists n \mathbin{\le} 49.\; \textit{even}~n \mathrel{\land} \textit{even}~(\textit{Suc}~n)$'' \\ +\textbf{nitpick}~[\textit{card nat}~= 50, \textit{unary\_ints}] \\[2\smallskipamount] \slshape Nitpick found a counterexample: \\[2\smallskipamount] \hbox{}\qquad Empty assignment \postw @@ -1211,26 +1230,26 @@ Trying 8 scopes: \\ \hbox{}\qquad \textit{card} $'a$~= 1, \textit{card} $'b$~= 1, \textit{card} \textit{nat}~= 1, \textit{card} ``$('a \times {'}b)$ -\textit{list}''~= 1, \\ -\hbox{}\qquad\quad \textit{card} ``\kern1pt$'a$ \textit{list}''~= 1, and -\textit{card} ``\kern1pt$'b$ \textit{list}''~= 1. \\ +\textit{list\/}''~= 1, \\ +\hbox{}\qquad\quad \textit{card} ``\kern1pt$'a$ \textit{list\/}''~= 1, and +\textit{card} ``\kern1pt$'b$ \textit{list\/}''~= 1. \\ \hbox{}\qquad \textit{card} $'a$~= 2, \textit{card} $'b$~= 2, \textit{card} \textit{nat}~= 2, \textit{card} ``$('a \times {'}b)$ -\textit{list}''~= 2, \\ -\hbox{}\qquad\quad \textit{card} ``\kern1pt$'a$ \textit{list}''~= 2, and -\textit{card} ``\kern1pt$'b$ \textit{list}''~= 2. \\ +\textit{list\/}''~= 2, \\ +\hbox{}\qquad\quad \textit{card} ``\kern1pt$'a$ \textit{list\/}''~= 2, and +\textit{card} ``\kern1pt$'b$ \textit{list\/}''~= 2. \\ \hbox{}\qquad $\qquad\vdots$ \\[.5\smallskipamount] \hbox{}\qquad \textit{card} $'a$~= 8, \textit{card} $'b$~= 8, \textit{card} \textit{nat}~= 8, \textit{card} ``$('a \times {'}b)$ -\textit{list}''~= 8, \\ -\hbox{}\qquad\quad \textit{card} ``\kern1pt$'a$ \textit{list}''~= 8, and -\textit{card} ``\kern1pt$'b$ \textit{list}''~= 8. +\textit{list\/}''~= 8, \\ +\hbox{}\qquad\quad \textit{card} ``\kern1pt$'a$ \textit{list\/}''~= 8, and +\textit{card} ``\kern1pt$'b$ \textit{list\/}''~= 8. \\[2\smallskipamount] Nitpick found a counterexample for \textit{card} $'a$~= 5, \textit{card} $'b$~= 5, \textit{card} \textit{nat}~= 5, \textit{card} ``$('a \times {'}b)$ -\textit{list}''~= 5, \textit{card} ``\kern1pt$'a$ \textit{list}''~= 5, and -\textit{card} ``\kern1pt$'b$ \textit{list}''~= 5: +\textit{list\/}''~= 5, \textit{card} ``\kern1pt$'a$ \textit{list\/}''~= 5, and +\textit{card} ``\kern1pt$'b$ \textit{list\/}''~= 5: \\[2\smallskipamount] \hbox{}\qquad Free variables: \nopagebreak \\ \hbox{}\qquad\qquad $\textit{xs} = [a_1, a_2]$ \\ @@ -1851,7 +1870,7 @@ The number of options can be overwhelming at first glance. Do not let that worry you: Nitpick's defaults have been chosen so that it almost always does the right thing, and the most important options have been covered in context in -\S\ref{overview}. +\S\ref{first-steps}. The descriptions below refer to the following syntactic quantities: @@ -2622,7 +2641,7 @@ then Nitpick assumes that the definition was made using an inductive package and based on the introduction rules marked with \textit{nitpick\_\allowbreak -ind\_\allowbreak intros} tries to determine whether the definition is +\allowbreak intros} tries to determine whether the definition is well-founded. \end{enum} \end{enum} @@ -2664,7 +2683,8 @@ Nitpick provides a rich Standard ML interface used mainly for internal purposes and debugging. Among the most interesting functions exported by Nitpick are those that let you invoke the tool programmatically and those that let you -register and unregister custom coinductive datatypes. +register and unregister custom coinductive datatypes as well as term +postprocessors. \subsection{Invocation of Nitpick} \label{invocation-of-nitpick} @@ -2695,7 +2715,7 @@ put into a \textit{params} record. Here is an example: \prew -$\textbf{val}\,~\textit{params} = \textit{Nitpick\_Isar.default\_params}~\textit{thy}~[(\textrm{``}\textrm{timeout}\textrm{''},\, \textrm{``}\textrm{none}\textrm{''})]$ \\ +$\textbf{val}\,~\textit{params} = \textit{Nitpick\_Isar.default\_params}~\textit{thy}~[(\textrm{``}\textrm{timeout\/}\textrm{''},\, \textrm{``}\textrm{none}\textrm{''})]$ \\ $\textbf{val}\,~(\textit{outcome},\, \textit{state}') = \textit{Nitpick.pick\_nits\_in\_subgoal}~\begin{aligned}[t] & \textit{state}~\textit{params}~\textit{false} \\[-2pt] & \textit{subgoal}\end{aligned}$ @@ -2726,7 +2746,7 @@ \prew $\textbf{setup}~\,\{{*}\,~\!\begin{aligned}[t] & \textit{Nitpick.register\_codatatype} \\[-2pt] -& \qquad @\{\antiq{typ}~``\kern1pt'a~\textit{llist}\textrm{''}\}~@\{\antiq{const\_name}~ \textit{llist\_case}\} \\[-2pt] %% TYPESETTING +& \qquad @\{\antiq{typ}~``\kern1pt'a~\textit{llist\/}\textrm{''}\}~@\{\antiq{const\_name}~ \textit{llist\_case}\} \\[-2pt] %% TYPESETTING & \qquad (\textit{map}~\textit{dest\_Const}~[@\{\antiq{term}~\textit{LNil}\},\, @\{\antiq{term}~\textit{LCons}\}])\,\ {*}\}\end{aligned}$ \postw @@ -2740,7 +2760,7 @@ \prew $\textbf{setup}~\,\{{*}\,~\textit{Nitpick.unregister\_codatatype}~@\{\antiq{typ}~`` -\kern1pt'a~\textit{list}\textrm{''}\}\ \,{*}\}$ +\kern1pt'a~\textit{list\/}\textrm{''}\}\ \,{*}\}$ \postw Inductive datatypes can be registered as coinductive datatypes, given @@ -2748,6 +2768,26 @@ the use of the inductive constructors---Nitpick will generate an error if they are needed. +\subsection{Registration of Term Postprocessors} +\label{registration-of-term-postprocessors} + +It is possible to change the output of any term that Nitpick considers a +datatype by registering a term postprocessor. The interface for registering and +unregistering postprocessors consists of the following pair of functions defined +in the \textit{Nitpick} structure: + +\prew +$\textbf{type}\,~\textit{term\_postprocessor}\,~{=} {}$ \\ +$\hbox{}\quad\textit{Proof.context} \rightarrow \textit{string} \rightarrow (\textit{typ} \rightarrow \textit{term~list\/}) \rightarrow \textit{typ} \rightarrow \textit{term} \rightarrow \textit{term}$ \\ +$\textbf{val}\,~\textit{register\_term\_postprocessors} : {}$ \\ +$\hbox{}\quad\textit{typ} \rightarrow \textit{term\_postprocessor} \rightarrow \textit{theory} \rightarrow \textit{theory}$ \\ +$\textbf{val}\,~\textit{unregister\_term\_postprocessors} :\, +\textit{typ} \rightarrow \textit{theory} \rightarrow \textit{theory}$ +\postw + +\S\ref{typedefs-quotient-types-records-rationals-and-reals} and +\texttt{src/HOL/Library/Multiset.thy} illustrate this feature in context. + \section{Known Bugs and Limitations} \label{known-bugs-and-limitations}