# HG changeset patch
# User blanchet
# Date 1280837088 -7200
# Node ID bc2f9383fd592acb6420e51e7cf0c800f3cee0a5
# Parent  ef644a533265e8530b100f7449af771ac0a5210e
clarify attribute documentation

diff -r ef644a533265 -r bc2f9383fd59 doc-src/Nitpick/nitpick.tex
--- a/doc-src/Nitpick/nitpick.tex	Tue Aug 03 13:40:24 2010 +0200
+++ b/doc-src/Nitpick/nitpick.tex	Tue Aug 03 14:04:48 2010 +0200
@@ -767,7 +767,7 @@
 Inductively defined predicates (and sets) are particularly problematic for
 counterexample generators. They can make Quickcheck~\cite{berghofer-nipkow-2004}
 loop forever and Refute~\cite{weber-2008} run out of resources. The crux of
-the problem is that they are defined using a least fixed point construction.
+the problem is that they are defined using a least fixed-point construction.
 
 Nitpick's philosophy is that not all inductive predicates are equal. Consider
 the \textit{even} predicate below:
@@ -797,7 +797,7 @@
 \postw
 
 Wellfoundedness is desirable because it enables Nitpick to use a very efficient
-fixed point computation.%
+fixed-point computation.%
 \footnote{If an inductive predicate is
 well-founded, then it has exactly one fixed point, which is simultaneously the
 least and the greatest fixed point. In these circumstances, the computation of
@@ -2056,7 +2056,7 @@
 \item[$\bullet$] \textbf{\textit{smart}:} Try to prove that the inductive
 predicate is well-founded using Isabelle's \textit{lexicographic\_order} and
 \textit{size\_change} tactics. If this succeeds (or the predicate occurs with an
-appropriate polarity in the formula to falsify), use an efficient fixed point
+appropriate polarity in the formula to falsify), use an efficient fixed-point
 equation as specification of the predicate; otherwise, unroll the predicates
 according to the \textit{iter}~\qty{const} and \textit{iter} options.
 \end{enum}
@@ -2622,17 +2622,20 @@
 \item[4.] Otherwise, it looks up the definition of the constant:
 
 \begin{enum}
-\item[1.] If the \textit{nitpick\_def} set associated with the constant
-is not empty, it uses the latest rule added to the set as the definition of the
-constant; otherwise it uses the actual definition axiom.
+\item[1.] If the \textit{nitpick\_def} set associated with the constant is not
+empty, it uses the latest rule added to the set as the definition of the
+constant; otherwise it uses the actual definition axiom. In addition, the
+constant is \textsl{unfolded} wherever it appears (as opposed to defined
+equationally).
 \item[2.] If the definition is of the form
 
 \qquad $c~{?}x_1~\ldots~{?}x_m \,\equiv\, \lambda y_1~\ldots~y_n.\; \textit{lfp}~(\lambda f.\; t)$,
 
-then Nitpick assumes that the definition was made using an inductive package and
-based on the introduction rules marked with \textit{nitpick\_\allowbreak
-\allowbreak intros} tries to determine whether the definition is
-well-founded.
+then Nitpick assumes that the definition was made using an inductive package
+based on the introduction rules registered in Isabelle's internal
+\textit{Spec\_Rules} table. It uses the introduction rules to ascertain whether
+the definition is well-founded and the definition to generate a fixed-point
+equation or an unrolled equation.
 \end{enum}
 \end{enum}
 
@@ -2649,7 +2652,7 @@
 definition as follows:
 
 \prew
-\textbf{lemma} $\mathit{odd\_alt_def}$ [\textit{nitpick\_def}]:\kern.4em ``$\textit{odd}~n \,\equiv\, n~\textrm{mod}~2 = 1$''
+\textbf{lemma} $\mathit{odd\_alt\_def}$ [\textit{nitpick\_def}]:\kern.4em ``$\textit{odd}~n \,\equiv\, n~\textrm{mod}~2 = 1$''
 \postw
 
 Nitpick then expands all occurrences of $\mathit{odd}~n$ to $n~\textrm{mod}~2
@@ -2659,12 +2662,18 @@
 \textbf{lemma} $\mathit{odd\_simp}$ [\textit{nitpick\_simp}]:\kern.4em ``$\textit{odd}~n = (n~\textrm{mod}~2 = 1)$''
 \postw
 
-Moreover, because of its internal three-valued logic, Nitpick tends to lose a
+Such tweaks should be done with great care, because Nitpick will assume that the
+constant is completely defined by its equational specification. For example, if
+you make ``$\textit{odd}~(2 * k + 1)$'' a \textit{nitpick\_simp} rule and neglect to provide rules to handle the $2 * k$ case, Nitpick will define
+$\textit{odd}~n$ arbitrarily for even values of $n$. The \textit{debug}
+(\S\ref{output-format}) option is extremely useful to understand what is going
+on when experimenting with \textit{nitpick\_} attributes.
+
+Because of its internal three-valued logic, Nitpick tends to lose a
 lot of precision in the presence of partially specified constants. For example,
 
 \prew
-\textbf{lemma} \textit{odd\_simp} [\textit{nitpick\_simp}]: \\
-``$\textit{odd~x} = \lnot\, \textit{even}~x$''
+\textbf{lemma} \textit{odd\_simp} [\textit{nitpick\_simp}]:\kern.4em ``$\textit{odd~x} = \lnot\, \textit{even}~x$''
 \postw
 
 is superior to
@@ -2675,12 +2684,16 @@
 ``$\lnot\, \textit{even~x} \,\Longrightarrow\, \textit{odd~x} = \textit{True\/}$''
 \postw
 
-Such tweaks should be done with great care, because Nitpick will assume that the
-constant is completely defined by its equational specification. For example, if
-you make ``$\textit{odd}~(2 * k + 1)$'' a \textit{nitpick\_simp} rule and neglect to provide rules to handle the $2 * k$ case, Nitpick will define
-$\textit{odd}~n$ arbitrarily for even values of $n$. The \textit{debug}
-(\S\ref{output-format}) option is extremely useful to understand what is going
-on when experimenting with \textit{nitpick\_} attributes.
+Because Nitpick unfolds definitions but not simplification rules, it often pays
+off to declare long-winded definitions as \textit{nitpick\_simp}. For example:
+
+\prew
+\textbf{definition}~\textit{optimum} \textbf{where} [\textit{nitpick\_simp}]: \\
+``$\textit{optimum}~t =
+     (\forall u.\; \textit{consistent~u} \longrightarrow \textit{alphabet~t} = \textit{alphabet~u}$ \\
+\phantom{``$\textit{optimum}~t = (\forall u.\;$}${\longrightarrow}\; \textit{freq}~t = \textit{freq}~u \longrightarrow
+         \textit{cost~t} \le \textit{cost~u})$''
+\postw
 
 \section{Standard ML Interface}
 \label{standard-ml-interface}