1.1 --- a/doc-src/Nitpick/nitpick.tex Mon Feb 22 14:36:10 2010 +0100
1.2 +++ b/doc-src/Nitpick/nitpick.tex Mon Feb 22 19:31:00 2010 +0100
1.3 @@ -141,11 +141,11 @@
1.4
1.5 This section introduces Nitpick by presenting small examples. If possible, you
1.6 should try out the examples on your workstation. Your theory file should start
1.7 -the standard way:
1.8 +as follows:
1.9
1.10 \prew
1.11 \textbf{theory}~\textit{Scratch} \\
1.12 -\textbf{imports}~\textit{Main} \\
1.13 +\textbf{imports}~\textit{Main~Coinductive\_List~Quotient\_Product~RealDef} \\
1.14 \textbf{begin}
1.15 \postw
1.16
1.17 @@ -439,7 +439,7 @@
1.18 value (displayed as `$\unk$'). The type \textit{int} is handled similarly.
1.19 Internally, undefined values lead to a three-valued logic.
1.20
1.21 -Here is an example involving \textit{int}:
1.22 +Here is an example involving \textit{int\/}:
1.23
1.24 \prew
1.25 \textbf{lemma} ``$\lbrakk i \le j;\> n \le (m{\Colon}\mathit{int})\rbrakk \,\Longrightarrow\, i * n + j * m \le i * m + j * n$'' \\
1.26 @@ -627,7 +627,7 @@
1.27 genuine counterexample for \textit{card}~$'a~\textit{list}$~= 10, it is very
1.28 unlikely that one could be found for smaller cardinalities.
1.29
1.30 -\subsection{Typedefs, Records, Rationals, and Reals}
1.31 +\subsection{Typedefs, Quotient Types, Records, Rationals, and Reals}
1.32 \label{typedefs-records-rationals-and-reals}
1.33
1.34 Nitpick generally treats types declared using \textbf{typedef} as datatypes
1.35 @@ -651,12 +651,41 @@
1.36 \hbox{}\qquad\qquad $\textit{three} = \{\Abs{0},\, \Abs{1},\, \Abs{2},\, \unr\}$
1.37 \postw
1.38
1.39 -%% MARK
1.40 In the output above, $\Abs{n}$ abbreviates $\textit{Abs\_three}~n$.
1.41
1.42 -%% MARK
1.43 -Records, which are implemented as \textbf{typedef}s behind the scenes, are
1.44 -handled in much the same way:
1.45 +Quotient types are handled in much the same way. The following fragment defines
1.46 +the integer type \textit{my\_int} by encoding the integer $x$ by a pair of
1.47 +natural numbers $(m, n)$ such that $x + n = m$:
1.48 +
1.49 +\prew
1.50 +\textbf{fun} \textit{my\_int\_rel} \textbf{where} \\
1.51 +``$\textit{my\_int\_rel}~(x,\, y)~(u,\, v) = (x + v = u + y)$'' \\[2\smallskipamount]
1.52 +%
1.53 +\textbf{quotient\_type}~\textit{my\_int} = ``$\textit{nat} \times \textit{nat\/}$''$\;{/}\;$\textit{my\_int\_rel} \\
1.54 +\textbf{by}~(\textit{auto simp add\/}:\ \textit{equivp\_def expand\_fun\_eq}) \\[2\smallskipamount]
1.55 +%
1.56 +\textbf{definition}~\textit{add\_raw}~\textbf{where} \\
1.57 +``$\textit{add\_raw} \,\equiv\, \lambda(x,\, y)~(u,\, v).\; (x + (u\Colon\textit{nat}), y + (v\Colon\textit{nat}))$'' \\[2\smallskipamount]
1.58 +%
1.59 +\textbf{quotient\_definition} ``$\textit{add\/}\Colon\textit{my\_int} \Rightarrow \textit{my\_int} \Rightarrow \textit{my\_int\/}$'' \textbf{is} \textit{add\_raw} \\[2\smallskipamount]
1.60 +%
1.61 +\textbf{lemma} ``$\textit{add}~x~y = \textit{add}~x~x$'' \\
1.62 +\textbf{nitpick} [\textit{show\_datatypes}] \\[2\smallskipamount]
1.63 +\slshape Nitpick found a counterexample: \\[2\smallskipamount]
1.64 +\hbox{}\qquad Free variables: \nopagebreak \\
1.65 +\hbox{}\qquad\qquad $x = \Abs{(0,\, 0)}$ \\
1.66 +\hbox{}\qquad\qquad $y = \Abs{(1,\, 0)}$ \\
1.67 +\hbox{}\qquad Datatypes: \\
1.68 +\hbox{}\qquad\qquad $\textit{nat} = \{0,\, 1,\, \unr\}$ \\
1.69 +\hbox{}\qquad\qquad $\textit{nat} \times \textit{nat} = \{(0,\, 0),\> (1,\, 0),\> \unr\}$ \\
1.70 +\hbox{}\qquad\qquad $\textit{my\_int} = \{\Abs{(0,\, 0)},\> \Abs{(1,\, 0)},\> \unr\}$
1.71 +\postw
1.72 +
1.73 +In the counterexample, $\Abs{(0,\, 0)}$ and $\Abs{(1,\, 0)}$ represent the
1.74 +integers $0$ and $1$, respectively. Other representants would have been
1.75 +possible---e.g., $\Abs{(5,\, 5)}$ and $\Abs{(12,\, 11)}$.
1.76 +
1.77 +Records are also handled as datatypes with a single constructor:
1.78
1.79 \prew
1.80 \textbf{record} \textit{point} = \\
1.81 @@ -675,6 +704,8 @@
1.82 & \lparr\textit{Xcoord} = 1,\> \textit{Ycoord} = 1\rparr,\, \unr\}\end{aligned}$
1.83 \postw
1.84
1.85 +
1.86 +
1.87 Finally, Nitpick provides rudimentary support for rationals and reals using a
1.88 similar approach:
1.89
1.90 @@ -949,13 +980,13 @@
1.91 \slshape The type ``\kern1pt$'a$'' passed the monotonicity test. Nitpick might be able to skip
1.92 some scopes. \\[2\smallskipamount]
1.93 Trying 8 scopes: \\
1.94 -\hbox{}\qquad \textit{card} $'a$~= 1, \textit{card} ``\kern1pt$'a~\textit{list}$''~= 1,
1.95 +\hbox{}\qquad \textit{card} $'a$~= 1, \textit{card} ``\kern1pt$'a~\textit{list\/}$''~= 1,
1.96 and \textit{bisim\_depth}~= 0. \\
1.97 \hbox{}\qquad $\qquad\vdots$ \\[.5\smallskipamount]
1.98 -\hbox{}\qquad \textit{card} $'a$~= 8, \textit{card} ``\kern1pt$'a~\textit{list}$''~= 8,
1.99 +\hbox{}\qquad \textit{card} $'a$~= 8, \textit{card} ``\kern1pt$'a~\textit{list\/}$''~= 8,
1.100 and \textit{bisim\_depth}~= 7. \\[2\smallskipamount]
1.101 Nitpick found a counterexample for {\itshape card}~$'a$ = 2,
1.102 -\textit{card}~``\kern1pt$'a~\textit{list}$''~= 2, and \textit{bisim\_\allowbreak
1.103 +\textit{card}~``\kern1pt$'a~\textit{list\/}$''~= 2, and \textit{bisim\_\allowbreak
1.104 depth}~= 1:
1.105 \\[2\smallskipamount]
1.106 \hbox{}\qquad Free variables: \nopagebreak \\
1.107 @@ -1118,7 +1149,7 @@
1.108 \textit{Lam}~(\textit{Lam}~(\textit{Var}~0))$. Using the traditional
1.109 $\lambda$-term notation, $t$~is
1.110 $\lambda x\, y.\> x$ whereas $\textit{subst}~\sigma~t$ is $\lambda x\, y.\> y$.
1.111 -The bug is in \textit{subst}: The $\textit{lift}~(\sigma~m)~1$ call should be
1.112 +The bug is in \textit{subst\/}: The $\textit{lift}~(\sigma~m)~1$ call should be
1.113 replaced with $\textit{lift}~(\sigma~m)~0$.
1.114
1.115 An interesting aspect of Nitpick's verbose output is that it assigned inceasing
1.116 @@ -1509,7 +1540,7 @@
1.117 completeness of the set $S$. First, soundness:
1.118
1.119 \prew
1.120 -\textbf{theorem}~\textit{S\_sound}: \\
1.121 +\textbf{theorem}~\textit{S\_sound\/}: \\
1.122 ``$w \in S \longrightarrow \textit{length}~[x\mathbin{\leftarrow} w.\; x = a] =
1.123 \textit{length}~[x\mathbin{\leftarrow} w.\; x = b]$'' \\
1.124 \textbf{nitpick} \\[2\smallskipamount]
1.125 @@ -1691,7 +1722,7 @@
1.126 of elements stored in the tree:
1.127
1.128 \prew
1.129 -\textbf{theorem}~\textit{dataset\_skew\_split}:\\
1.130 +\textbf{theorem}~\textit{dataset\_skew\_split\/}:\\
1.131 ``$\textit{dataset}~(\textit{skew}~t) = \textit{dataset}~t$'' \\
1.132 ``$\textit{dataset}~(\textit{split}~t) = \textit{dataset}~t$'' \\
1.133 \textbf{nitpick} \\[2\smallskipamount]
1.134 @@ -1702,7 +1733,7 @@
1.135 should not alter the tree:
1.136
1.137 \prew
1.138 -\textbf{theorem}~\textit{wf\_skew\_split}:\\
1.139 +\textbf{theorem}~\textit{wf\_skew\_split\/}:\\
1.140 ``$\textit{wf}~t\,\Longrightarrow\, \textit{skew}~t = t$'' \\
1.141 ``$\textit{wf}~t\,\Longrightarrow\, \textit{split}~t = t$'' \\
1.142 \textbf{nitpick} \\[2\smallskipamount]
1.143 @@ -1723,7 +1754,7 @@
1.144 \textit{split}. Let's see if this causes any problems:
1.145
1.146 \prew
1.147 -\textbf{theorem}~\textit{wf\_insort}:\kern.4em ``$\textit{wf}~t\,\Longrightarrow\, \textit{wf}~(\textit{insort}~t~x)$'' \\
1.148 +\textbf{theorem}~\textit{wf\_insort\/}:\kern.4em ``$\textit{wf}~t\,\Longrightarrow\, \textit{wf}~(\textit{insort}~t~x)$'' \\
1.149 \textbf{nitpick} \\[2\smallskipamount]
1.150 \slshape Nitpick found a counterexample for \textit{card} $'a$ = 4: \\[2\smallskipamount]
1.151 \hbox{}\qquad Free variables: \nopagebreak \\
1.152 @@ -1738,7 +1769,7 @@
1.153 $\textit{insort}~t~x$ using the \textit{eval} option. This gives
1.154
1.155 \prew
1.156 -\textbf{theorem} \textit{wf\_insort\_nat}:\kern.4em ``$\textit{wf}~t\,\Longrightarrow\, \textit{wf}~(\textit{insort}~t~(x\Colon\textit{nat}))$'' \\
1.157 +\textbf{theorem} \textit{wf\_insort\_nat\/}:\kern.4em ``$\textit{wf}~t\,\Longrightarrow\, \textit{wf}~(\textit{insort}~t~(x\Colon\textit{nat}))$'' \\
1.158 \textbf{nitpick} [\textit{eval} = ``$\textit{insort}~t~x$''] \\[2\smallskipamount]
1.159 \slshape Nitpick found a counterexample: \\[2\smallskipamount]
1.160 \hbox{}\qquad Free variables: \nopagebreak \\
1.161 @@ -1755,7 +1786,7 @@
1.162 Reintroducing the code seems to solve the problem:
1.163
1.164 \prew
1.165 -\textbf{theorem}~\textit{wf\_insort}:\kern.4em ``$\textit{wf}~t\,\Longrightarrow\, \textit{wf}~(\textit{insort}~t~x)$'' \\
1.166 +\textbf{theorem}~\textit{wf\_insort\/}:\kern.4em ``$\textit{wf}~t\,\Longrightarrow\, \textit{wf}~(\textit{insort}~t~x)$'' \\
1.167 \textbf{nitpick} \\[2\smallskipamount]
1.168 {\slshape Nitpick ran out of time after checking 7 of 8 scopes.}
1.169 \postw
1.170 @@ -1764,7 +1795,7 @@
1.171 obvious way:
1.172
1.173 \prew
1.174 -\textbf{theorem} \textit{dataset\_insort}:\kern.4em
1.175 +\textbf{theorem} \textit{dataset\_insort\/}:\kern.4em
1.176 ``$\textit{dataset}~(\textit{insort}~t~x) = \{x\} \cup \textit{dataset}~t$'' \\
1.177 \textbf{nitpick} \\[2\smallskipamount]
1.178 {\slshape Nitpick ran out of time after checking 6 of 8 scopes.}
1.179 @@ -1825,19 +1856,19 @@
1.180
1.181 \begin{enum}
1.182 \item[$\bullet$] \qtybf{string}: A string.
1.183 -\item[$\bullet$] \qtybf{bool}: \textit{true} or \textit{false}.
1.184 -\item[$\bullet$] \qtybf{bool\_or\_smart}: \textit{true}, \textit{false}, or \textit{smart}.
1.185 -\item[$\bullet$] \qtybf{int}: An integer. Negative integers are prefixed with a hyphen.
1.186 -\item[$\bullet$] \qtybf{int\_or\_smart}: An integer or \textit{smart}.
1.187 +\item[$\bullet$] \qtybf{bool\/}: \textit{true} or \textit{false}.
1.188 +\item[$\bullet$] \qtybf{bool\_or\_smart\/}: \textit{true}, \textit{false}, or \textit{smart}.
1.189 +\item[$\bullet$] \qtybf{int\/}: An integer. Negative integers are prefixed with a hyphen.
1.190 +\item[$\bullet$] \qtybf{int\_or\_smart\/}: An integer or \textit{smart}.
1.191 \item[$\bullet$] \qtybf{int\_range}: An integer (e.g., 3) or a range
1.192 of nonnegative integers (e.g., $1$--$4$). The range symbol `--' can be entered as \texttt{-} (hyphen) or \texttt{\char`\\\char`\<midarrow\char`\>}.
1.193
1.194 \item[$\bullet$] \qtybf{int\_seq}: A comma-separated sequence of ranges of integers (e.g.,~1{,}3{,}\allowbreak6--8).
1.195 \item[$\bullet$] \qtybf{time}: An integer followed by $\textit{min}$ (minutes), $s$ (seconds), or \textit{ms}
1.196 (milliseconds), or the keyword \textit{none} ($\infty$ years).
1.197 -\item[$\bullet$] \qtybf{const}: The name of a HOL constant.
1.198 +\item[$\bullet$] \qtybf{const\/}: The name of a HOL constant.
1.199 \item[$\bullet$] \qtybf{term}: A HOL term (e.g., ``$f~x$'').
1.200 -\item[$\bullet$] \qtybf{term\_list}: A space-separated list of HOL terms (e.g.,
1.201 +\item[$\bullet$] \qtybf{term\_list\/}: A space-separated list of HOL terms (e.g.,
1.202 ``$f~x$''~``$g~y$'').
1.203 \item[$\bullet$] \qtybf{type}: A HOL type.
1.204 \end{enum}
1.205 @@ -2190,7 +2221,6 @@
1.206 the \textit{format}~\qty{term} option described above.
1.207 \end{enum}
1.208
1.209 -%% MARK: Authentication
1.210 \subsection{Authentication}
1.211 \label{authentication}
1.212
1.213 @@ -2564,14 +2594,14 @@
1.214 definition as follows:
1.215
1.216 \prew
1.217 -\textbf{lemma} $\mathit{odd\_def}'$ [\textit{nitpick\_def}]: ``$\textit{odd}~n \,\equiv\, n~\textrm{mod}~2 = 1$''
1.218 +\textbf{lemma} $\mathit{odd\_def}'$ [\textit{nitpick\_def}]:\kern.4em ``$\textit{odd}~n \,\equiv\, n~\textrm{mod}~2 = 1$''
1.219 \postw
1.220
1.221 Nitpick then expands all occurrences of $\mathit{odd}~n$ to $n~\textrm{mod}~2
1.222 = 1$. Alternatively, we can specify an equational specification of the constant:
1.223
1.224 \prew
1.225 -\textbf{lemma} $\mathit{odd\_simp}'$ [\textit{nitpick\_simp}]: ``$\textit{odd}~n = (n~\textrm{mod}~2 = 1)$''
1.226 +\textbf{lemma} $\mathit{odd\_simp}'$ [\textit{nitpick\_simp}]:\kern.4em ``$\textit{odd}~n = (n~\textrm{mod}~2 = 1)$''
1.227 \postw
1.228
1.229 Such tweaks should be done with great care, because Nitpick will assume that the