added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
1.1 --- a/doc-src/Nitpick/nitpick.tex Mon Feb 01 14:12:12 2010 +0100
1.2 +++ b/doc-src/Nitpick/nitpick.tex Tue Feb 02 11:38:38 2010 +0100
1.3 @@ -25,8 +25,8 @@
1.4 \def\lparr{\mathopen{(\mkern-4mu\mid}}
1.5 \def\rparr{\mathclose{\mid\mkern-4mu)}}
1.6
1.7 -\def\undef{\textit{undefined}}
1.8 \def\unk{{?}}
1.9 +\def\undef{(\lambda x.\; \unk)}
1.10 %\def\unr{\textit{others}}
1.11 \def\unr{\ldots}
1.12 \def\Abs#1{\hbox{\rm{\flqq}}{\,#1\,}\hbox{\rm{\frqq}}}
1.13 @@ -188,8 +188,8 @@
1.14 \prew
1.15 \textbf{apply}~\textit{auto} \\[2\smallskipamount]
1.16 {\slshape goal (2 subgoals): \\
1.17 -\ 1. $P\,\Longrightarrow\, Q$ \\
1.18 -\ 2. $Q\,\Longrightarrow\, P$} \\[2\smallskipamount]
1.19 +\phantom{0}1. $P\,\Longrightarrow\, Q$ \\
1.20 +\phantom{0}2. $Q\,\Longrightarrow\, P$} \\[2\smallskipamount]
1.21 \textbf{nitpick}~1 \\[2\smallskipamount]
1.22 {\slshape Nitpick found a counterexample: \\[2\smallskipamount]
1.23 \hbox{}\qquad Free variables: \nopagebreak \\
1.24 @@ -317,11 +317,9 @@
1.25 \postw
1.26
1.27 Notice that $\textit{The}~(\lambda y.\;P~y) = \textit{The}~\{a_2, a_3\} = a_1$,
1.28 -just like before.\footnote{The \undef{} symbol's presence is explained as
1.29 -follows: In higher-order logic, any function can be built from the undefined
1.30 -function using repeated applications of the function update operator $f(x :=
1.31 -y)$, just like any list can be built from the empty list using $x \mathbin{\#}
1.32 -xs$.}
1.33 +just like before.\footnote{The Isabelle/HOL notation $f(x :=
1.34 +y)$ denotes the function that maps $x$ to $y$ and that otherwise behaves like
1.35 +$f$.}
1.36
1.37 Our misadventures with THE suggest adding `$\exists!x{.}$' (``there exists a
1.38 unique $x$ such that'') at the front of our putative lemma's assumption:
1.39 @@ -562,7 +560,7 @@
1.40 {\slshape Datatype:} \\
1.41 \hbox{}\qquad $'a$~\textit{list}~= $\{[],\, [a_3, a_3],\, [a_3],\, \unr\}$ \\
1.42 {\slshape Constants:} \\
1.43 -\hbox{}\qquad $\lambda x_1.\; x_1 \mathbin{@} [y, y] = \undef([] := [a_3, a_3],\> [a_3, a_3] := \unk,\> [a_3] := \unk)$ \\
1.44 +\hbox{}\qquad $\lambda x_1.\; x_1 \mathbin{@} [y, y] = \undef([] := [a_3, a_3])$ \\
1.45 \hbox{}\qquad $\textit{hd} = \undef([] := a_2,\> [a_3, a_3] := a_3,\> [a_3] := a_3)$
1.46 \postw
1.47
1.48 @@ -1243,6 +1241,208 @@
1.49 \textit{int~list}, \textit{rat}, and \textit{rat~list} will lead Nitpick to
1.50 consider only 8~scopes instead of $32\,768$.
1.51
1.52 +\subsection{Inductive Properties}
1.53 +\label{inductive-properties}
1.54 +
1.55 +Inductive properties are a particular pain to prove, because the failure to
1.56 +establish an induction step can mean several things:
1.57 +%
1.58 +\begin{enumerate}
1.59 +\item The property is invalid.
1.60 +\item The property is valid but is too weak to support the induction step.
1.61 +\item The property is valid and strong enough; it's just that we haven't found
1.62 +the proof yet.
1.63 +\end{enumerate}
1.64 +%
1.65 +Depending on which scenario applies, we would take the appropriate course of
1.66 +action:
1.67 +%
1.68 +\begin{enumerate}
1.69 +\item Repair the statement of the property so that it becomes valid.
1.70 +\item Generalize the property and/or prove auxiliary properties.
1.71 +\item Work harder on a proof.
1.72 +\end{enumerate}
1.73 +%
1.74 +How can we distinguish between the three scenarios? Nitpick's normal mode of
1.75 +operation can often detect scenario 1, and Isabelle's automatic tactics help with
1.76 +scenario 3. Using appropriate techniques, it is also often possible to use
1.77 +Nitpick to identify scenario 2. Consider the following transition system,
1.78 +in which natural numbers represent states:
1.79 +
1.80 +\prew
1.81 +\textbf{inductive\_set}~\textit{reach}~\textbf{where} \\
1.82 +``$(4\Colon\textit{nat}) \in \textit{reach\/}$'' $\mid$ \\
1.83 +``$\lbrakk n < 4;\> n \in \textit{reach\/}\rbrakk \,\Longrightarrow\, 3 * n + 1 \in \textit{reach\/}$'' $\mid$ \\
1.84 +``$n \in \textit{reach} \,\Longrightarrow n + 2 \in \textit{reach\/}$''
1.85 +\postw
1.86 +
1.87 +We will try to prove that only even numbers are reachable:
1.88 +
1.89 +\prew
1.90 +\textbf{lemma}~``$n \in \textit{reach} \,\Longrightarrow\, 2~\textrm{dvd}~n$''
1.91 +\postw
1.92 +
1.93 +Does this property hold? Nitpick cannot find a counterexample within 30 seconds,
1.94 +so let's attempt a proof by induction:
1.95 +
1.96 +\prew
1.97 +\textbf{apply}~(\textit{induct~set}{:}~\textit{reach\/}) \\
1.98 +\textbf{apply}~\textit{auto}
1.99 +\postw
1.100 +
1.101 +This leaves us in the following proof state:
1.102 +
1.103 +\prew
1.104 +{\slshape goal (2 subgoals): \\
1.105 +\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)$ \\
1.106 +\phantom{0}2. ${\bigwedge}n.\;\, \lbrakk n \in \textit{reach\/};\, 2~\textsl{dvd}~n\rbrakk \,\Longrightarrow\, 2~\textsl{dvd}~\textit{Suc}~(\textit{Suc}~n)$
1.107 +}
1.108 +\postw
1.109 +
1.110 +If we run Nitpick on the first subgoal, it still won't find any
1.111 +counterexample; and yet, \textit{auto} fails to go further, and \textit{arith}
1.112 +is helpless. However, notice the $n \in \textit{reach}$ assumption, which
1.113 +strengthens the induction hypothesis but is not immediately usable in the proof.
1.114 +If we remove it and invoke Nitpick, this time we get a counterexample:
1.115 +
1.116 +\prew
1.117 +\textbf{apply}~(\textit{thin\_tac}~``$n \in \textit{reach\/}$'') \\
1.118 +\textbf{nitpick} \\[2\smallskipamount]
1.119 +\slshape Nitpick found a counterexample: \\[2\smallskipamount]
1.120 +\hbox{}\qquad Skolem constant: \nopagebreak \\
1.121 +\hbox{}\qquad\qquad $n = 0$
1.122 +\postw
1.123 +
1.124 +Indeed, 0 < 4, 2 divides 0, but 2 does not divide 1. We can use this information
1.125 +to strength the lemma:
1.126 +
1.127 +\prew
1.128 +\textbf{lemma}~``$n \in \textit{reach} \,\Longrightarrow\, 2~\textrm{dvd}~n \mathrel{\lor} n \not= 0$''
1.129 +\postw
1.130 +
1.131 +Unfortunately, the proof by induction still gets stuck, except that Nitpick now
1.132 +finds the counterexample $n = 2$. We generalize the lemma further to
1.133 +
1.134 +\prew
1.135 +\textbf{lemma}~``$n \in \textit{reach} \,\Longrightarrow\, 2~\textrm{dvd}~n \mathrel{\lor} n \ge 4$''
1.136 +\postw
1.137 +
1.138 +and this time \textit{arith} can finish off the subgoals.
1.139 +
1.140 +A similar technique can be employed for structural induction. The
1.141 +following mini-formalization of full binary trees will serve as illustration:
1.142 +
1.143 +\prew
1.144 +\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]
1.145 +\textbf{primrec}~\textit{labels}~\textbf{where} \\
1.146 +``$\textit{labels}~(\textit{Leaf}~a) = \{a\}$'' $\mid$ \\
1.147 +``$\textit{labels}~(\textit{Branch}~t~u) = \textit{labels}~t \mathrel{\cup} \textit{labels}~u$'' \\[2\smallskipamount]
1.148 +\textbf{primrec}~\textit{swap}~\textbf{where} \\
1.149 +``$\textit{swap}~(\textit{Leaf}~c)~a~b =$ \\
1.150 +\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$ \\
1.151 +``$\textit{swap}~(\textit{Branch}~t~u)~a~b = \textit{Branch}~(\textit{swap}~t~a~b)~(\textit{swap}~u~a~b)$''
1.152 +\postw
1.153 +
1.154 +The \textit{labels} function returns the set of labels occurring on leaves of a
1.155 +tree, and \textit{swap} exchanges two labels. Intuitively, if two distinct
1.156 +labels $a$ and $b$ occur in a tree $t$, they should also occur in the tree
1.157 +obtained by swapping $a$ and $b$:
1.158 +
1.159 +\prew
1.160 +\textbf{lemma} $``\lbrakk a \in \textit{labels}~t;\, b \in \textit{labels}~t;\, a \not= b\rbrakk {}$ \\
1.161 +\phantom{\textbf{lemma} ``}$\,{\Longrightarrow}{\;\,} \textit{labels}~(\textit{swap}~t~a~b) = \textit{labels}~t$''
1.162 +\postw
1.163 +
1.164 +Nitpick can't find any counterexample, so we proceed with induction
1.165 +(this time favoring a more structured style):
1.166 +
1.167 +\prew
1.168 +\textbf{proof}~(\textit{induct}~$t$) \\
1.169 +\hbox{}\quad \textbf{case}~\textit{Leaf}~\textbf{thus}~\textit{?case}~\textbf{by}~\textit{simp} \\
1.170 +\textbf{next} \\
1.171 +\hbox{}\quad \textbf{case}~$(\textit{Branch}~t~u)$~\textbf{thus} \textit{?case}
1.172 +\postw
1.173 +
1.174 +Nitpick can't find any counterexample at this point either, but it makes the
1.175 +following suggestion:
1.176 +
1.177 +\prew
1.178 +\slshape
1.179 +Hint: To check that the induction hypothesis is general enough, try the following command:
1.180 +\textbf{nitpick}~[\textit{non\_std} ``${\kern1pt'a}~\textit{bin\_tree}$'', \textit{show\_consts}].
1.181 +\postw
1.182 +
1.183 +If we follow the hint, we get a ``nonstandard'' counterexample for the step:
1.184 +
1.185 +\prew
1.186 +\slshape Nitpick found a nonstandard counterexample for \textit{card} $'a$ = 4: \\[2\smallskipamount]
1.187 +\hbox{}\qquad Free variables: \nopagebreak \\
1.188 +\hbox{}\qquad\qquad $a = a_4$ \\
1.189 +\hbox{}\qquad\qquad $b = a_3$ \\
1.190 +\hbox{}\qquad\qquad $t = \xi_3$ \\
1.191 +\hbox{}\qquad\qquad $u = \xi_4$ \\
1.192 +\hbox{}\qquad {\slshape Constants:} \nopagebreak \\
1.193 +\hbox{}\qquad\qquad $\textit{labels} = \undef
1.194 + (\!\begin{aligned}[t]%
1.195 + & \xi_3 := \{a_4\},\> \xi_4 := \{a_1, a_3\}, \\[-2pt] %% TYPESETTING
1.196 + & \textit{Branch}~\xi_3~\xi_3 := \{a_4\}, \\[-2pt]
1.197 + & \textit{Branch}~\xi_3~\xi_4 := \{a_1, a_3, a_4\})\end{aligned}$ \\
1.198 +\hbox{}\qquad\qquad $\lambda x_1.\> \textit{swap}~x_1~a~b = \undef
1.199 + (\!\begin{aligned}[t]%
1.200 + & \xi_3 := \xi_3,\> \xi_4 := \xi_3, \\[-2pt]
1.201 + & \textit{Branch}~\xi_3~\xi_3 := \textit{Branch}~\xi_3~\xi_3, \\[-2pt]
1.202 + & \textit{Branch}~\xi_4~\xi_3 := \textit{Branch}~\xi_3~\xi_3)\end{aligned}$ \\[2\smallskipamount]
1.203 +The existence of a nonstandard model suggests that the induction hypothesis is not general enough or perhaps
1.204 +even wrong. See the ``Inductive Properties'' section of the Nitpick manual for details (``\textit{isabelle doc nitpick}'').
1.205 +\postw
1.206 +
1.207 +Reading the Nitpick manual is a most excellent idea.
1.208 +But what's going on? The \textit{non\_std} ``${\kern1pt'a}~\textit{bin\_tree}$''
1.209 +option told the tool to look for nonstandard models of binary trees, which
1.210 +means that new ``nonstandard'' trees $\xi_1, \xi_2, \ldots$, are now allowed in
1.211 +addition to the standard trees generated by the \textit{Leaf} and
1.212 +\textit{Branch} constructors.%
1.213 +\footnote{Notice the similarity between allowing nonstandard trees here and
1.214 +allowing unreachable states in the preceding example (by removing the ``$n \in
1.215 +\textit{reach\/}$'' assumption). In both cases, we effectively enlarge the
1.216 +set of objects over which the induction is performed while doing the step
1.217 +so as to test the induction hypothesis's strength.}
1.218 +The new trees are so nonstandard that we know nothing about them, except what
1.219 +the induction hypothesis states and what can be proved about all trees without
1.220 +relying on induction or case distinction. The key observation is,
1.221 +%
1.222 +\begin{quote}
1.223 +\textsl{If the induction
1.224 +hypothesis is strong enough, the induction step will hold even for nonstandard
1.225 +objects, and Nitpick won't find any nonstandard counterexample.}
1.226 +\end{quote}
1.227 +%
1.228 +But here, Nitpick did find some nonstandard trees $t = \xi_3$
1.229 +and $u = \xi_4$ such that $a \in \textit{labels}~t$, $b \notin
1.230 +\textit{labels}~t$, $a \notin \textit{labels}~u$, and $b \in \textit{labels}~u$.
1.231 +Because neither tree contains both $a$ and $b$, the induction hypothesis tells
1.232 +us nothing about the labels of $\textit{swap}~t~a~b$ and $\textit{swap}~u~a~b$,
1.233 +and as a result we know nothing about the labels of the tree
1.234 +$\textit{swap}~(\textit{Branch}~t~u)~a~b$, which by definition equals
1.235 +$\textit{Branch}$ $(\textit{swap}~t~a~b)$ $(\textit{swap}~u~a~b)$, whose
1.236 +labels are $\textit{labels}$ $(\textit{swap}~t~a~b) \mathrel{\cup}
1.237 +\textit{labels}$ $(\textit{swap}~u~a~b)$.
1.238 +
1.239 +The solution is to ensure that we always know what the labels of the subtrees
1.240 +are in the inductive step, by covering the cases where $a$ and/or~$b$ is not in
1.241 +$t$ in the statement of the lemma:
1.242 +
1.243 +\prew
1.244 +\textbf{lemma} ``$\textit{labels}~(\textit{swap}~t~a~b) = {}$ \\
1.245 +\phantom{\textbf{lemma} ``}$(\textrm{if}~a \in \textit{labels}~t~\textrm{then}$ \nopagebreak \\
1.246 +\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\}$ \\
1.247 +\phantom{\textbf{lemma} ``(}$\textrm{else}$ \\
1.248 +\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)$''
1.249 +\postw
1.250 +
1.251 +This time, Nitpick won't find any nonstandard counterexample, and we can perform
1.252 +the induction step using \textbf{auto}.
1.253 +
1.254 \section{Case Studies}
1.255 \label{case-studies}
1.256
1.257 @@ -1398,7 +1598,8 @@
1.258 functions:
1.259
1.260 \prew
1.261 -\textbf{datatype} $'a$~\textit{tree} = $\Lambda$ $\mid$ $N$ ``\kern1pt$'a\Colon \textit{linorder}$'' \textit{nat} ``\kern1pt$'a$ \textit{tree}'' ``\kern1pt$'a$ \textit{tree}'' \\[2\smallskipamount]
1.262 +\textbf{datatype} $'a$~\textit{aa\_tree} = \\
1.263 +\hbox{}\quad $\Lambda$ $\mid$ $N$ ``\kern1pt$'a\Colon \textit{linorder}$'' \textit{nat} ``\kern1pt$'a$ \textit{aa\_tree}'' ``\kern1pt$'a$ \textit{aa\_tree}'' \\[2\smallskipamount]
1.264 \textbf{primrec} \textit{data} \textbf{where} \\
1.265 ``$\textit{data}~\Lambda = \undef$'' $\,\mid$ \\
1.266 ``$\textit{data}~(N~x~\_~\_~\_) = x$'' \\[2\smallskipamount]
1.267 @@ -1526,7 +1727,7 @@
1.268 \slshape Nitpick found a counterexample for \textit{card} $'a$ = 4: \\[2\smallskipamount]
1.269 \hbox{}\qquad Free variables: \nopagebreak \\
1.270 \hbox{}\qquad\qquad $t = N~a_3~1~\Lambda~\Lambda$ \\
1.271 -\hbox{}\qquad\qquad $x = a_4$ \\[2\smallskipamount]
1.272 +\hbox{}\qquad\qquad $x = a_4$
1.273 \postw
1.274
1.275 It's hard to see why this is a counterexample. To improve readability, we will
1.276 @@ -1583,10 +1784,11 @@
1.277 \def\optrue#1#2{\flushitem{\textit{#1} $\bigl[$= \qtybf{bool}$\bigr]$\quad [\textit{true}]\hfill (neg.: \textit{#2})}\nopagebreak\\[\parskip]}
1.278 \def\opfalse#1#2{\flushitem{\textit{#1} $\bigl[$= \qtybf{bool}$\bigr]$\quad [\textit{false}]\hfill (neg.: \textit{#2})}\nopagebreak\\[\parskip]}
1.279 \def\opsmart#1#2{\flushitem{\textit{#1} $\bigl[$= \qtybf{bool\_or\_smart}$\bigr]$\quad [\textit{smart}]\hfill (neg.: \textit{#2})}\nopagebreak\\[\parskip]}
1.280 -\def\ops#1#2{\flushitem{\textit{#1} = \qtybf{#2}} \nopagebreak\\[\parskip]}
1.281 -\def\opt#1#2#3{\flushitem{\textit{#1} = \qtybf{#2}\quad [\textit{#3}]} \nopagebreak\\[\parskip]}
1.282 -\def\opu#1#2#3{\flushitem{\textit{#1} \qtybf{#2} = \qtybf{#3}} \nopagebreak\\[\parskip]}
1.283 -\def\opusmart#1#2#3{\flushitem{\textit{#1} \qtybf{#2} $\bigl[$= \qtybf{bool\_or\_smart}$\bigr]$\hfill (neg.: \textit{#3})}\nopagebreak\\[\parskip]}
1.284 +\def\opnodefault#1#2{\flushitem{\textit{#1} = \qtybf{#2}} \nopagebreak\\[\parskip]}
1.285 +\def\opdefault#1#2#3{\flushitem{\textit{#1} = \qtybf{#2}\quad [\textit{#3}]} \nopagebreak\\[\parskip]}
1.286 +\def\oparg#1#2#3{\flushitem{\textit{#1} \qtybf{#2} = \qtybf{#3}} \nopagebreak\\[\parskip]}
1.287 +\def\opargbool#1#2#3{\flushitem{\textit{#1} \qtybf{#2} $\bigl[$= \qtybf{bool}$\bigr]$\hfill (neg.: \textit{#3})}\nopagebreak\\[\parskip]}
1.288 +\def\opargboolorsmart#1#2#3{\flushitem{\textit{#1} \qtybf{#2} $\bigl[$= \qtybf{bool\_or\_smart}$\bigr]$\hfill (neg.: \textit{#3})}\nopagebreak\\[\parskip]}
1.289
1.290 Nitpick's behavior can be influenced by various options, which can be specified
1.291 in brackets after the \textbf{nitpick} command. Default values can be set
1.292 @@ -1696,7 +1898,7 @@
1.293 \label{scope-of-search}
1.294
1.295 \begin{enum}
1.296 -\opu{card}{type}{int\_seq}
1.297 +\oparg{card}{type}{int\_seq}
1.298 Specifies the sequence of cardinalities to use for a given type.
1.299 For free types, and often also for \textbf{typedecl}'d types, it usually makes
1.300 sense to specify cardinalities as a range of the form \textit{$1$--$n$}.
1.301 @@ -1709,18 +1911,18 @@
1.302 \nopagebreak
1.303 {\small See also \textit{mono} (\S\ref{scope-of-search}).}
1.304
1.305 -\opt{card}{int\_seq}{$\mathbf{1}$--$\mathbf{8}$}
1.306 +\opdefault{card}{int\_seq}{$\mathbf{1}$--$\mathbf{8}$}
1.307 Specifies the default sequence of cardinalities to use. This can be overridden
1.308 on a per-type basis using the \textit{card}~\qty{type} option described above.
1.309
1.310 -\opu{max}{const}{int\_seq}
1.311 +\oparg{max}{const}{int\_seq}
1.312 Specifies the sequence of maximum multiplicities to use for a given
1.313 (co)in\-duc\-tive datatype constructor. A constructor's multiplicity is the
1.314 number of distinct values that it can construct. Nonsensical values (e.g.,
1.315 \textit{max}~[]~$=$~2) are silently repaired. This option is only available for
1.316 datatypes equipped with several constructors.
1.317
1.318 -\ops{max}{int\_seq}
1.319 +\opnodefault{max}{int\_seq}
1.320 Specifies the default sequence of maximum multiplicities to use for
1.321 (co)in\-duc\-tive datatype constructors. This can be overridden on a per-constructor
1.322 basis using the \textit{max}~\qty{const} option described above.
1.323 @@ -1757,13 +1959,13 @@
1.324 {\small See also \textit{bits} (\S\ref{scope-of-search}) and
1.325 \textit{show\_datatypes} (\S\ref{output-format}).}
1.326
1.327 -\opt{bits}{int\_seq}{$\mathbf{1},\mathbf{2},\mathbf{3},\mathbf{4},\mathbf{6},\mathbf{8},\mathbf{10},\mathbf{12}$}
1.328 +\opdefault{bits}{int\_seq}{$\mathbf{1},\mathbf{2},\mathbf{3},\mathbf{4},\mathbf{6},\mathbf{8},\mathbf{10},\mathbf{12}$}
1.329 Specifies the number of bits to use to represent natural numbers and integers in
1.330 binary, excluding the sign bit. The minimum is 1 and the maximum is 31.
1.331
1.332 {\small See also \textit{binary\_ints} (\S\ref{scope-of-search}).}
1.333
1.334 -\opusmart{wf}{const}{non\_wf}
1.335 +\opargboolorsmart{wf}{const}{non\_wf}
1.336 Specifies whether the specified (co)in\-duc\-tively defined predicate is
1.337 well-founded. The option can take the following values:
1.338
1.339 @@ -1780,7 +1982,7 @@
1.340
1.341 \item[$\bullet$] \textbf{\textit{smart}}: Try to prove that the inductive
1.342 predicate is well-founded using Isabelle's \textit{lexicographic\_order} and
1.343 -\textit{sizechange} tactics. If this succeeds (or the predicate occurs with an
1.344 +\textit{size\_change} tactics. If this succeeds (or the predicate occurs with an
1.345 appropriate polarity in the formula to falsify), use an efficient fixed point
1.346 equation as specification of the predicate; otherwise, unroll the predicates
1.347 according to the \textit{iter}~\qty{const} and \textit{iter} options.
1.348 @@ -1795,7 +1997,7 @@
1.349 Specifies the default wellfoundedness setting to use. This can be overridden on
1.350 a per-predicate basis using the \textit{wf}~\qty{const} option above.
1.351
1.352 -\opu{iter}{const}{int\_seq}
1.353 +\oparg{iter}{const}{int\_seq}
1.354 Specifies the sequence of iteration counts to use when unrolling a given
1.355 (co)in\-duc\-tive predicate. By default, unrolling is applied for inductive
1.356 predicates that occur negatively and coinductive predicates that occur
1.357 @@ -1807,12 +2009,12 @@
1.358 {\small See also \textit{wf} (\S\ref{scope-of-search}) and
1.359 \textit{star\_linear\_preds} (\S\ref{optimizations}).}
1.360
1.361 -\opt{iter}{int\_seq}{$\mathbf{1{,}2{,}4{,}8{,}12{,}16{,}24{,}32}$}
1.362 +\opdefault{iter}{int\_seq}{$\mathbf{1{,}2{,}4{,}8{,}12{,}16{,}24{,}32}$}
1.363 Specifies the sequence of iteration counts to use when unrolling (co)in\-duc\-tive
1.364 predicates. This can be overridden on a per-predicate basis using the
1.365 \textit{iter} \qty{const} option above.
1.366
1.367 -\opt{bisim\_depth}{int\_seq}{$\mathbf{7}$}
1.368 +\opdefault{bisim\_depth}{int\_seq}{$\mathbf{7}$}
1.369 Specifies the sequence of iteration counts to use when unrolling the
1.370 bisimilarity predicate generated by Nitpick for coinductive datatypes. A value
1.371 of $-1$ means that no predicate is generated, in which case Nitpick performs an
1.372 @@ -1822,7 +2024,7 @@
1.373 the sum of the cardinalities of the coinductive datatypes occurring in the
1.374 formula to falsify.
1.375
1.376 -\opusmart{box}{type}{dont\_box}
1.377 +\opargboolorsmart{box}{type}{dont\_box}
1.378 Specifies whether Nitpick should attempt to wrap (``box'') a given function or
1.379 product type in an isomorphic datatype internally. Boxing is an effective mean
1.380 to reduce the search space and speed up Nitpick, because the isomorphic datatype
1.381 @@ -1850,8 +2052,8 @@
1.382 Specifies the default boxing setting to use. This can be overridden on a
1.383 per-type basis using the \textit{box}~\qty{type} option described above.
1.384
1.385 -\opusmart{mono}{type}{non\_mono}
1.386 -Specifies whether the specified type should be considered monotonic when
1.387 +\opargboolorsmart{mono}{type}{non\_mono}
1.388 +Specifies whether the given type should be considered monotonic when
1.389 enumerating scopes. If the option is set to \textit{smart}, Nitpick performs a
1.390 monotonicity check on the type. Setting this option to \textit{true} can reduce
1.391 the number of scopes tried, but it also diminishes the theoretical chance of
1.392 @@ -1873,6 +2075,15 @@
1.393 theoretical chance of finding a counterexample.
1.394
1.395 {\small See also \textit{mono} (\S\ref{scope-of-search}).}
1.396 +
1.397 +\opargbool{std}{type}{non\_std}
1.398 +Specifies whether the given type should be given standard models.
1.399 +Nonstandard models are unsound but can help debug inductive arguments,
1.400 +as explained in \S\ref{inductive-properties}.
1.401 +
1.402 +\optrue{std}{non\_std}
1.403 +Specifies the default standardness to use. This can be overridden on a per-type
1.404 +basis using the \textit{std}~\qty{type} option described above.
1.405 \end{enum}
1.406
1.407 \subsection{Output Format}
1.408 @@ -1919,7 +2130,7 @@
1.409 Enabling this option effectively enables \textit{show\_skolems},
1.410 \textit{show\_datatypes}, and \textit{show\_consts}.
1.411
1.412 -\opt{max\_potential}{int}{$\mathbf{1}$}
1.413 +\opdefault{max\_potential}{int}{$\mathbf{1}$}
1.414 Specifies the maximum number of potential counterexamples to display. Setting
1.415 this option to 0 speeds up the search for a genuine counterexample. This option
1.416 is implicitly set to 0 for automatic runs. If you set this option to a value
1.417 @@ -1933,7 +2144,7 @@
1.418 {\small See also \textit{check\_potential} (\S\ref{authentication}) and
1.419 \textit{sat\_solver} (\S\ref{optimizations}).}
1.420
1.421 -\opt{max\_genuine}{int}{$\mathbf{1}$}
1.422 +\opdefault{max\_genuine}{int}{$\mathbf{1}$}
1.423 Specifies the maximum number of genuine counterexamples to display. If you set
1.424 this option to a value greater than 1, you will need an incremental SAT solver:
1.425 For efficiency, it is recommended to install the JNI version of MiniSat and set
1.426 @@ -1945,12 +2156,12 @@
1.427 {\small See also \textit{check\_genuine} (\S\ref{authentication}) and
1.428 \textit{sat\_solver} (\S\ref{optimizations}).}
1.429
1.430 -\ops{eval}{term\_list}
1.431 +\opnodefault{eval}{term\_list}
1.432 Specifies the list of terms whose values should be displayed along with
1.433 counterexamples. This option suffers from an ``observer effect'': Nitpick might
1.434 find different counterexamples for different values of this option.
1.435
1.436 -\opu{format}{term}{int\_seq}
1.437 +\oparg{format}{term}{int\_seq}
1.438 Specifies how to uncurry the value displayed for a variable or constant.
1.439 Uncurrying sometimes increases the readability of the output for high-arity
1.440 functions. For example, given the variable $y \mathbin{\Colon} {'a}\Rightarrow
1.441 @@ -1966,7 +2177,7 @@
1.442 \nopagebreak
1.443 {\small See also \textit{uncurry} (\S\ref{optimizations}).}
1.444
1.445 -\opt{format}{int\_seq}{$\mathbf{1}$}
1.446 +\opdefault{format}{int\_seq}{$\mathbf{1}$}
1.447 Specifies the default format to use. Irrespective of the default format, the
1.448 extra arguments to a Skolem constant corresponding to the outer bound variables
1.449 are kept separated from the remaining arguments, the \textbf{for} arguments of
1.450 @@ -1999,7 +2210,7 @@
1.451 \nopagebreak
1.452 {\small See also \textit{max\_genuine} (\S\ref{output-format}).}
1.453
1.454 -\ops{expect}{string}
1.455 +\opnodefault{expect}{string}
1.456 Specifies the expected outcome, which must be one of the following:
1.457
1.458 \begin{enum}
1.459 @@ -2025,7 +2236,7 @@
1.460 \sloppy
1.461
1.462 \begin{enum}
1.463 -\opt{sat\_solver}{string}{smart}
1.464 +\opdefault{sat\_solver}{string}{smart}
1.465 Specifies which SAT solver to use. SAT solvers implemented in C or \cpp{} tend
1.466 to be faster than their Java counterparts, but they can be more difficult to
1.467 install. Also, if you set the \textit{max\_potential} (\S\ref{output-format}) or
1.468 @@ -2118,7 +2329,7 @@
1.469 \end{enum}
1.470 \fussy
1.471
1.472 -\opt{batch\_size}{int\_or\_smart}{smart}
1.473 +\opdefault{batch\_size}{int\_or\_smart}{smart}
1.474 Specifies the maximum number of Kodkod problems that should be lumped together
1.475 when invoking Kodkodi. Each problem corresponds to one scope. Lumping problems
1.476 together ensures that Kodkodi is launched less often, but it makes the verbose
1.477 @@ -2188,7 +2399,7 @@
1.478 Unless you are tracking down a bug in Nitpick or distrust the peephole
1.479 optimizer, you should leave this option enabled.
1.480
1.481 -\opt{sym\_break}{int}{20}
1.482 +\opdefault{sym\_break}{int}{20}
1.483 Specifies an upper bound on the number of relations for which Kodkod generates
1.484 symmetry breaking predicates. According to the Kodkod documentation
1.485 \cite{kodkod-2009-options}, ``in general, the higher this value, the more
1.486 @@ -2196,7 +2407,7 @@
1.487 setting the value too high may have the opposite effect and slow down the
1.488 solving.''
1.489
1.490 -\opt{sharing\_depth}{int}{3}
1.491 +\opdefault{sharing\_depth}{int}{3}
1.492 Specifies the depth to which Kodkod should check circuits for equivalence during
1.493 the translation to SAT. The default of 3 is the same as in Alloy. The minimum
1.494 allowed depth is 1. Increasing the sharing may result in a smaller SAT problem,
1.495 @@ -2207,7 +2418,7 @@
1.496 Although this might sound like a good idea, in practice it can drastically slow
1.497 down Kodkod.
1.498
1.499 -\opt{max\_threads}{int}{0}
1.500 +\opdefault{max\_threads}{int}{0}
1.501 Specifies the maximum number of threads to use in Kodkod. If this option is set
1.502 to 0, Kodkod will compute an appropriate value based on the number of processor
1.503 cores available.
1.504 @@ -2221,7 +2432,7 @@
1.505 \label{timeouts}
1.506
1.507 \begin{enum}
1.508 -\opt{timeout}{time}{$\mathbf{30}$ s}
1.509 +\opdefault{timeout}{time}{$\mathbf{30}$ s}
1.510 Specifies the maximum amount of time that the \textbf{nitpick} command should
1.511 spend looking for a counterexample. Nitpick tries to honor this constraint as
1.512 well as it can but offers no guarantees. For automatic runs,
1.513 @@ -2232,10 +2443,10 @@
1.514 \nopagebreak
1.515 {\small See also \textit{max\_threads} (\S\ref{optimizations}).}
1.516
1.517 -\opt{tac\_timeout}{time}{$\mathbf{500}$\,ms}
1.518 +\opdefault{tac\_timeout}{time}{$\mathbf{500}$\,ms}
1.519 Specifies the maximum amount of time that the \textit{auto} tactic should use
1.520 when checking a counterexample, and similarly that \textit{lexicographic\_order}
1.521 -and \textit{sizechange} should use when checking whether a (co)in\-duc\-tive
1.522 +and \textit{size\_change} should use when checking whether a (co)in\-duc\-tive
1.523 predicate is well-founded. Nitpick tries to honor this constraint as well as it
1.524 can but offers no guarantees.
1.525
1.526 @@ -2477,7 +2688,7 @@
1.527 \nopagebreak
1.528 \\[2\smallskipamount]
1.529 \hbox{}\qquad Empty assignment} \nopagebreak\\[2\smallskipamount]
1.530 -\textbf{by}~(\textit{auto simp}: \textit{prec\_def})
1.531 +\textbf{by}~(\textit{auto simp}:~\textit{prec\_def})
1.532 \postw
1.533
1.534 Such theorems are considered bad style because they rely on the internal
2.1 --- a/src/HOL/Divides.thy Mon Feb 01 14:12:12 2010 +0100
2.2 +++ b/src/HOL/Divides.thy Tue Feb 02 11:38:38 2010 +0100
2.3 @@ -2451,7 +2451,8 @@
2.4 in subst [OF mod_div_equality [of _ n]])
2.5 arith
2.6
2.7 -lemmas [nitpick_def] = mod_div_equality' [THEN eq_reflection]
2.8 +lemmas [nitpick_def] = dvd_eq_mod_eq_0 [THEN eq_reflection]
2.9 + mod_div_equality' [THEN eq_reflection]
2.10 zmod_zdiv_equality' [THEN eq_reflection]
2.11
2.12 subsubsection {* Code generation *}
3.1 --- a/src/HOL/Nitpick.thy Mon Feb 01 14:12:12 2010 +0100
3.2 +++ b/src/HOL/Nitpick.thy Tue Feb 02 11:38:38 2010 +0100
3.3 @@ -36,6 +36,7 @@
3.4 and bisim_iterator_max :: bisim_iterator
3.5 and Quot :: "'a \<Rightarrow> 'b"
3.6 and quot_normal :: "'a \<Rightarrow> 'a"
3.7 + and NonStd :: "'a \<Rightarrow> 'b"
3.8 and Tha :: "('a \<Rightarrow> bool) \<Rightarrow> 'a"
3.9
3.10 datatype ('a, 'b) pair_box = PairBox 'a 'b
3.11 @@ -43,6 +44,7 @@
3.12
3.13 typedecl unsigned_bit
3.14 typedecl signed_bit
3.15 +typedecl \<xi>
3.16
3.17 datatype 'a word = Word "('a set)"
3.18
3.19 @@ -250,12 +252,12 @@
3.20 setup {* Nitpick_Isar.setup *}
3.21
3.22 hide (open) const unknown is_unknown undefined_fast_The undefined_fast_Eps bisim
3.23 - bisim_iterator_max Quot quot_normal Tha PairBox FunBox Word refl' wf'
3.24 + bisim_iterator_max Quot quot_normal NonStd Tha PairBox FunBox Word refl' wf'
3.25 wf_wfrec wf_wfrec' wfrec' card' setsum' fold_graph' nat_gcd nat_lcm int_gcd
3.26 int_lcm Frac Abs_Frac Rep_Frac zero_frac one_frac num denom norm_frac frac
3.27 plus_frac times_frac uminus_frac number_of_frac inverse_frac less_eq_frac
3.28 of_frac
3.29 -hide (open) type bisim_iterator pair_box fun_box unsigned_bit signed_bit word
3.30 +hide (open) type bisim_iterator pair_box fun_box unsigned_bit signed_bit \<xi> word
3.31 hide (open) fact If_def Ex1_def rtrancl_def rtranclp_def tranclp_def refl'_def
3.32 wf'_def wf_wfrec'_def wfrec'_def card'_def setsum'_def fold_graph'_def
3.33 The_psimp Eps_psimp unit_case_def nat_case_def list_size_simp nat_gcd_def
4.1 --- a/src/HOL/Nitpick_Examples/Manual_Nits.thy Mon Feb 01 14:12:12 2010 +0100
4.2 +++ b/src/HOL/Nitpick_Examples/Manual_Nits.thy Tue Feb 02 11:38:38 2010 +0100
4.3 @@ -220,6 +220,69 @@
4.4 nitpick
4.5 oops
4.6
4.7 +subsection {* 3.12. Inductive Properties *}
4.8 +
4.9 +inductive_set reach where
4.10 +"(4\<Colon>nat) \<in> reach" |
4.11 +"n \<in> reach \<Longrightarrow> n < 4 \<Longrightarrow> 3 * n + 1 \<in> reach" |
4.12 +"n \<in> reach \<Longrightarrow> n + 2 \<in> reach"
4.13 +
4.14 +lemma "n \<in> reach \<Longrightarrow> 2 dvd n"
4.15 +nitpick
4.16 +apply (induct set: reach)
4.17 + apply auto
4.18 + nitpick
4.19 + apply (thin_tac "n \<in> reach")
4.20 + nitpick
4.21 +oops
4.22 +
4.23 +lemma "n \<in> reach \<Longrightarrow> 2 dvd n \<and> n \<noteq> 0"
4.24 +nitpick
4.25 +apply (induct set: reach)
4.26 + apply auto
4.27 + nitpick
4.28 + apply (thin_tac "n \<in> reach")
4.29 + nitpick
4.30 +oops
4.31 +
4.32 +lemma "n \<in> reach \<Longrightarrow> 2 dvd n \<and> n \<ge> 4"
4.33 +by (induct set: reach) arith+
4.34 +
4.35 +datatype 'a bin_tree = Leaf 'a | Branch "'a bin_tree" "'a bin_tree"
4.36 +
4.37 +primrec labels where
4.38 +"labels (Leaf a) = {a}" |
4.39 +"labels (Branch t u) = labels t \<union> labels u"
4.40 +
4.41 +primrec swap where
4.42 +"swap (Leaf c) a b =
4.43 + (if c = a then Leaf b else if c = b then Leaf a else Leaf c)" |
4.44 +"swap (Branch t u) a b = Branch (swap t a b) (swap u a b)"
4.45 +
4.46 +lemma "\<lbrakk>a \<in> labels t; b \<in> labels t; a \<noteq> b\<rbrakk> \<Longrightarrow> labels (swap t a b) = labels t"
4.47 +nitpick
4.48 +proof (induct t)
4.49 + case Leaf thus ?case by simp
4.50 +next
4.51 + case (Branch t u) thus ?case
4.52 + nitpick
4.53 + nitpick [non_std "'a bin_tree", show_consts]
4.54 +oops
4.55 +
4.56 +lemma "labels (swap t a b) =
4.57 + (if a \<in> labels t then
4.58 + if b \<in> labels t then labels t else (labels t - {a}) \<union> {b}
4.59 + else
4.60 + if b \<in> labels t then (labels t - {b}) \<union> {a} else labels t)"
4.61 +nitpick
4.62 +proof (induct t)
4.63 + case Leaf thus ?case by simp
4.64 +next
4.65 + case (Branch t u) thus ?case
4.66 + nitpick [non_std "'a bin_tree", show_consts]
4.67 + by auto
4.68 +qed
4.69 +
4.70 section {* 4. Case Studies *}
4.71
4.72 nitpick_params [max_potential = 0, max_threads = 2]
4.73 @@ -300,7 +363,7 @@
4.74
4.75 subsection {* 4.2. AA Trees *}
4.76
4.77 -datatype 'a tree = \<Lambda> | N "'a\<Colon>linorder" nat "'a tree" "'a tree"
4.78 +datatype 'a aa_tree = \<Lambda> | N "'a\<Colon>linorder" nat "'a aa_tree" "'a aa_tree"
4.79
4.80 primrec data where
4.81 "data \<Lambda> = undefined" |
5.1 --- a/src/HOL/Nitpick_Examples/Mono_Nits.thy Mon Feb 01 14:12:12 2010 +0100
5.2 +++ b/src/HOL/Nitpick_Examples/Mono_Nits.thy Tue Feb 02 11:38:38 2010 +0100
5.3 @@ -18,18 +18,19 @@
5.4 val def_table = Nitpick_HOL.const_def_table @{context} defs
5.5 val ext_ctxt : Nitpick_HOL.extended_context =
5.6 {thy = @{theory}, ctxt = @{context}, max_bisim_depth = ~1, boxes = [],
5.7 - user_axioms = NONE, debug = false, wfs = [], binary_ints = SOME false,
5.8 - destroy_constrs = false, specialize = false, skolemize = false,
5.9 - star_linear_preds = false, uncurry = false, fast_descrs = false,
5.10 - tac_timeout = NONE, evals = [], case_names = [], def_table = def_table,
5.11 - nondef_table = Symtab.empty, user_nondefs = [],
5.12 + stds = [(NONE, true)], wfs = [], user_axioms = NONE, debug = false,
5.13 + binary_ints = SOME false, destroy_constrs = false, specialize = false,
5.14 + skolemize = false, star_linear_preds = false, uncurry = false,
5.15 + fast_descrs = false, tac_timeout = NONE, evals = [], case_names = [],
5.16 + def_table = def_table, nondef_table = Symtab.empty, user_nondefs = [],
5.17 simp_table = Unsynchronized.ref Symtab.empty, psimp_table = Symtab.empty,
5.18 intro_table = Symtab.empty, ground_thm_table = Inttab.empty,
5.19 ersatz_table = [], skolems = Unsynchronized.ref [],
5.20 special_funs = Unsynchronized.ref [], unrolled_preds = Unsynchronized.ref [],
5.21 wf_cache = Unsynchronized.ref [], constr_cache = Unsynchronized.ref []}
5.22 (* term -> bool *)
5.23 -val is_mono = Nitpick_Mono.formulas_monotonic ext_ctxt @{typ 'a} [] []
5.24 +val is_mono = Nitpick_Mono.formulas_monotonic ext_ctxt @{typ 'a}
5.25 + Nitpick_Mono.Plus [] []
5.26 fun is_const t =
5.27 let val T = fastype_of t in
5.28 is_mono (Logic.mk_implies (Logic.mk_equals (Free ("dummyP", T), t),
6.1 --- a/src/HOL/Tools/Nitpick/HISTORY Mon Feb 01 14:12:12 2010 +0100
6.2 +++ b/src/HOL/Tools/Nitpick/HISTORY Tue Feb 02 11:38:38 2010 +0100
6.3 @@ -1,7 +1,9 @@
6.4 Version 2010
6.5
6.6 * Added and implemented "binary_ints" and "bits" options
6.7 - * Fixed soundness bug in "destroy_constrs" optimization
6.8 + * Added "std" option and implemented support for nonstandard models
6.9 + * Fixed soundness bugs related to "destroy_constrs" optimization and record
6.10 + getters
6.11
6.12 Version 2009-1
6.13
7.1 --- a/src/HOL/Tools/Nitpick/kodkod.ML Mon Feb 01 14:12:12 2010 +0100
7.2 +++ b/src/HOL/Tools/Nitpick/kodkod.ML Tue Feb 02 11:38:38 2010 +0100
7.3 @@ -1,6 +1,6 @@
7.4 (* Title: HOL/Tools/Nitpick/kodkod.ML
7.5 Author: Jasmin Blanchette, TU Muenchen
7.6 - Copyright 2008, 2009
7.7 + Copyright 2008, 2009, 2010
7.8
7.9 ML interface on top of Kodkod.
7.10 *)
8.1 --- a/src/HOL/Tools/Nitpick/kodkod_sat.ML Mon Feb 01 14:12:12 2010 +0100
8.2 +++ b/src/HOL/Tools/Nitpick/kodkod_sat.ML Tue Feb 02 11:38:38 2010 +0100
8.3 @@ -1,6 +1,6 @@
8.4 (* Title: HOL/Tools/Nitpick/kodkod_sat.ML
8.5 Author: Jasmin Blanchette, TU Muenchen
8.6 - Copyright 2009
8.7 + Copyright 2009, 2010
8.8
8.9 Kodkod SAT solver integration.
8.10 *)
9.1 --- a/src/HOL/Tools/Nitpick/minipick.ML Mon Feb 01 14:12:12 2010 +0100
9.2 +++ b/src/HOL/Tools/Nitpick/minipick.ML Tue Feb 02 11:38:38 2010 +0100
9.3 @@ -1,6 +1,6 @@
9.4 (* Title: HOL/Tools/Nitpick/minipick.ML
9.5 Author: Jasmin Blanchette, TU Muenchen
9.6 - Copyright 2009
9.7 + Copyright 2009, 2010
9.8
9.9 Finite model generation for HOL formulas using Kodkod, minimalistic version.
9.10 *)
10.1 --- a/src/HOL/Tools/Nitpick/nitpick.ML Mon Feb 01 14:12:12 2010 +0100
10.2 +++ b/src/HOL/Tools/Nitpick/nitpick.ML Tue Feb 02 11:38:38 2010 +0100
10.3 @@ -1,6 +1,6 @@
10.4 (* Title: HOL/Tools/Nitpick/nitpick.ML
10.5 Author: Jasmin Blanchette, TU Muenchen
10.6 - Copyright 2008, 2009
10.7 + Copyright 2008, 2009, 2010
10.8
10.9 Finite model generation for HOL formulas using Kodkod.
10.10 *)
10.11 @@ -16,6 +16,7 @@
10.12 bisim_depths: int list,
10.13 boxes: (typ option * bool option) list,
10.14 monos: (typ option * bool option) list,
10.15 + stds: (typ option * bool) list,
10.16 wfs: (styp option * bool option) list,
10.17 sat_solver: string,
10.18 blocking: bool,
10.19 @@ -57,9 +58,10 @@
10.20 val register_codatatype : typ -> string -> styp list -> theory -> theory
10.21 val unregister_codatatype : typ -> theory -> theory
10.22 val pick_nits_in_term :
10.23 - Proof.state -> params -> bool -> term list -> term -> string * Proof.state
10.24 + Proof.state -> params -> bool -> int -> int -> int -> term list -> term
10.25 + -> string * Proof.state
10.26 val pick_nits_in_subgoal :
10.27 - Proof.state -> params -> bool -> int -> string * Proof.state
10.28 + Proof.state -> params -> bool -> int -> int -> string * Proof.state
10.29 end;
10.30
10.31 structure Nitpick : NITPICK =
10.32 @@ -85,6 +87,7 @@
10.33 bisim_depths: int list,
10.34 boxes: (typ option * bool option) list,
10.35 monos: (typ option * bool option) list,
10.36 + stds: (typ option * bool) list,
10.37 wfs: (styp option * bool option) list,
10.38 sat_solver: string,
10.39 blocking: bool,
10.40 @@ -183,18 +186,21 @@
10.41 (* (unit -> string) -> Pretty.T *)
10.42 fun plazy f = Pretty.blk (0, pstrs (f ()))
10.43
10.44 -(* Time.time -> Proof.state -> params -> bool -> term -> string * Proof.state *)
10.45 -fun pick_them_nits_in_term deadline state (params : params) auto orig_assm_ts
10.46 - orig_t =
10.47 +(* Time.time -> Proof.state -> params -> bool -> int -> int -> int -> term
10.48 + -> string * Proof.state *)
10.49 +fun pick_them_nits_in_term deadline state (params : params) auto i n step
10.50 + orig_assm_ts orig_t =
10.51 let
10.52 val timer = Timer.startRealTimer ()
10.53 val thy = Proof.theory_of state
10.54 val ctxt = Proof.context_of state
10.55 +(* FIXME: reintroduce code before new release
10.56 val nitpick_thy = ThyInfo.get_theory "Nitpick"
10.57 val _ = Theory.subthy (nitpick_thy, thy) orelse
10.58 error "You must import the theory \"Nitpick\" to use Nitpick"
10.59 +*)
10.60 val {cards_assigns, maxes_assigns, iters_assigns, bitss, bisim_depths,
10.61 - boxes, monos, wfs, sat_solver, blocking, falsify, debug, verbose,
10.62 + boxes, monos, stds, wfs, sat_solver, blocking, falsify, debug, verbose,
10.63 overlord, user_axioms, assms, merge_type_vars, binary_ints,
10.64 destroy_constrs, specialize, skolemize, star_linear_preds, uncurry,
10.65 fast_descrs, peephole_optim, tac_timeout, sym_break, sharing_depth,
10.66 @@ -231,7 +237,16 @@
10.67 if passed_deadline deadline then raise TimeLimit.TimeOut
10.68 else raise Interrupt
10.69
10.70 - val _ = print_m (K "Nitpicking...")
10.71 + val _ =
10.72 + if step = 0 then
10.73 + print_m (fn () => "Nitpicking formula...")
10.74 + else
10.75 + pprint_m (fn () => Pretty.chunks (
10.76 + pretties_for_formulas ctxt ("Nitpicking " ^
10.77 + (if i <> 1 orelse n <> 1 then
10.78 + "subgoal " ^ string_of_int i ^ " of " ^ string_of_int n
10.79 + else
10.80 + "goal")) [orig_t]))
10.81 val neg_t = if falsify then Logic.mk_implies (orig_t, @{prop False})
10.82 else orig_t
10.83 val assms_t = if assms orelse auto then
10.84 @@ -260,7 +275,7 @@
10.85 val ersatz_table = ersatz_table thy
10.86 val (ext_ctxt as {wf_cache, ...}) =
10.87 {thy = thy, ctxt = ctxt, max_bisim_depth = max_bisim_depth, boxes = boxes,
10.88 - user_axioms = user_axioms, debug = debug, wfs = wfs,
10.89 + stds = stds, wfs = wfs, user_axioms = user_axioms, debug = debug,
10.90 binary_ints = binary_ints, destroy_constrs = destroy_constrs,
10.91 specialize = specialize, skolemize = skolemize,
10.92 star_linear_preds = star_linear_preds, uncurry = uncurry,
10.93 @@ -311,7 +326,8 @@
10.94 fold add_free_and_const_names (core_u :: def_us @ nondef_us) ([], [])
10.95 val (sel_names, nonsel_names) =
10.96 List.partition (is_sel o nickname_of) const_names
10.97 - val would_be_genuine = got_all_user_axioms andalso none_true wfs
10.98 + val genuine_means_genuine = got_all_user_axioms andalso none_true wfs
10.99 + val standard = forall snd stds
10.100 (*
10.101 val _ = List.app (priority o string_for_nut ctxt)
10.102 (core_u :: def_us @ nondef_us)
10.103 @@ -322,27 +338,27 @@
10.104 fun is_type_always_monotonic T =
10.105 (is_datatype thy T andalso not (is_quot_type thy T) andalso
10.106 (not (is_pure_typedef thy T) orelse is_univ_typedef thy T)) orelse
10.107 - is_number_type thy T orelse is_bit_type T
10.108 + is_number_type thy T orelse is_bit_type T orelse T = @{typ \<xi>}
10.109 fun is_type_monotonic T =
10.110 unique_scope orelse
10.111 case triple_lookup (type_match thy) monos T of
10.112 SOME (SOME b) => b
10.113 | _ => is_type_always_monotonic T orelse
10.114 - formulas_monotonic ext_ctxt T def_ts nondef_ts core_t
10.115 + formulas_monotonic ext_ctxt T Plus def_ts nondef_ts core_t
10.116 fun is_deep_datatype T =
10.117 is_datatype thy T andalso
10.118 (is_word_type T orelse
10.119 exists (curry (op =) T o domain_type o type_of) sel_names)
10.120 - val Ts = ground_types_in_terms ext_ctxt (core_t :: def_ts @ nondef_ts)
10.121 - |> sort TermOrd.typ_ord
10.122 + val all_Ts = ground_types_in_terms ext_ctxt (core_t :: def_ts @ nondef_ts)
10.123 + |> sort TermOrd.typ_ord
10.124 val _ = if verbose andalso binary_ints = SOME true andalso
10.125 - exists (member (op =) [nat_T, int_T]) Ts then
10.126 + exists (member (op =) [nat_T, int_T]) all_Ts then
10.127 print_v (K "The option \"binary_ints\" will be ignored because \
10.128 \of the presence of rationals, reals, \"Suc\", \
10.129 \\"gcd\", or \"lcm\" in the problem.")
10.130 else
10.131 ()
10.132 - val (mono_Ts, nonmono_Ts) = List.partition is_type_monotonic Ts
10.133 + val (mono_Ts, nonmono_Ts) = List.partition is_type_monotonic all_Ts
10.134 val _ =
10.135 if verbose andalso not unique_scope then
10.136 case filter_out is_type_always_monotonic mono_Ts of
10.137 @@ -364,7 +380,32 @@
10.138 end)
10.139 else
10.140 ()
10.141 - val shallow_dataTs = filter_out is_deep_datatype Ts
10.142 + val deep_dataTs = filter is_deep_datatype all_Ts
10.143 + (* FIXME: Implement proper detection of induction datatypes. *)
10.144 + (* string * (Rule_Cases.T * bool) -> bool *)
10.145 + fun is_inductive_case (_, (Rule_Cases.Case {fixes, assumes, ...}, _)) =
10.146 + false
10.147 +(*
10.148 + not (null fixes) andalso exists (String.isSuffix ".hyps" o fst) assumes
10.149 +*)
10.150 + (* unit -> typ list *)
10.151 + val induct_dataTs =
10.152 + if exists is_inductive_case (ProofContext.cases_of ctxt) then
10.153 + filter (is_datatype thy) all_Ts
10.154 + else
10.155 + []
10.156 + val _ = if standard andalso not (null induct_dataTs) then
10.157 + pprint_m (fn () => Pretty.blk (0,
10.158 + pstrs "Hint: To check that the induction hypothesis is \
10.159 + \general enough, try the following command: " @
10.160 + [Pretty.mark Markup.sendback (Pretty.blk (0,
10.161 + pstrs ("nitpick [" ^
10.162 + commas (map (prefix "non_std " o maybe_quote
10.163 + o unyxml o string_for_type ctxt)
10.164 + induct_dataTs) ^
10.165 + ", show_consts]")))] @ pstrs "."))
10.166 + else
10.167 + ()
10.168 (*
10.169 val _ = priority "Monotonic types:"
10.170 val _ = List.app (priority o string_for_type ctxt) mono_Ts
10.171 @@ -413,7 +454,7 @@
10.172 string_of_int j0))
10.173 (Typtab.dest ofs)
10.174 *)
10.175 - val all_exact = forall (is_exact_type datatypes) Ts
10.176 + val all_exact = forall (is_exact_type datatypes) all_Ts
10.177 (* nut list -> rep NameTable.table -> nut list * rep NameTable.table *)
10.178 val repify_consts = choose_reps_for_consts scope all_exact
10.179 val main_j0 = offset_of_type ofs bool_T
10.180 @@ -536,7 +577,9 @@
10.181 fun tuple_set_for_rel univ_card =
10.182 KK.TupleSet o map (kk_tuple debug univ_card) o the oo AList.lookup (op =)
10.183
10.184 - val word_model = if falsify then "counterexample" else "model"
10.185 + val das_wort_model =
10.186 + (if falsify then "counterexample" else "model")
10.187 + |> not standard ? prefix "nonstandard "
10.188
10.189 val scopes = Unsynchronized.ref []
10.190 val generated_scopes = Unsynchronized.ref []
10.191 @@ -560,42 +603,49 @@
10.192 show_consts = show_consts}
10.193 scope formats frees free_names sel_names nonsel_names rel_table
10.194 bounds
10.195 - val would_be_genuine = would_be_genuine andalso codatatypes_ok
10.196 + val genuine_means_genuine = genuine_means_genuine andalso codatatypes_ok
10.197 in
10.198 pprint (Pretty.chunks
10.199 [Pretty.blk (0,
10.200 (pstrs ("Nitpick found a" ^
10.201 (if not genuine then " potential "
10.202 - else if would_be_genuine then " "
10.203 - else " likely genuine ") ^ word_model) @
10.204 + else if genuine_means_genuine then " "
10.205 + else " likely genuine ") ^ das_wort_model) @
10.206 (case pretties_for_scope scope verbose of
10.207 [] => []
10.208 | pretties => pstrs " for " @ pretties) @
10.209 [Pretty.str ":\n"])),
10.210 Pretty.indent indent_size reconstructed_model]);
10.211 if genuine then
10.212 - (if check_genuine then
10.213 + (if check_genuine andalso standard then
10.214 (case prove_hol_model scope tac_timeout free_names sel_names
10.215 rel_table bounds assms_t of
10.216 SOME true => print ("Confirmation by \"auto\": The above " ^
10.217 - word_model ^ " is really genuine.")
10.218 + das_wort_model ^ " is really genuine.")
10.219 | SOME false =>
10.220 - if would_be_genuine then
10.221 - error ("A supposedly genuine " ^ word_model ^ " was shown to\
10.222 - \be spurious by \"auto\".\nThis should never happen.\n\
10.223 - \Please send a bug report to blanchet\
10.224 + if genuine_means_genuine then
10.225 + error ("A supposedly genuine " ^ das_wort_model ^ " was \
10.226 + \shown to be spurious by \"auto\".\nThis should never \
10.227 + \happen.\nPlease send a bug report to blanchet\
10.228 \te@in.tum.de.")
10.229 else
10.230 - print ("Refutation by \"auto\": The above " ^ word_model ^
10.231 + print ("Refutation by \"auto\": The above " ^ das_wort_model ^
10.232 " is spurious.")
10.233 | NONE => print "No confirmation by \"auto\".")
10.234 else
10.235 ();
10.236 + if not standard andalso not (null induct_dataTs) then
10.237 + print "The existence of a nonstandard model suggests that the \
10.238 + \induction hypothesis is not general enough or perhaps even \
10.239 + \wrong. See the \"Inductive Properties\" section of the \
10.240 + \Nitpick manual for details (\"isabelle doc nitpick\")."
10.241 + else
10.242 + ();
10.243 if has_syntactic_sorts orig_t then
10.244 print "Hint: Maybe you forgot a type constraint?"
10.245 else
10.246 ();
10.247 - if not would_be_genuine then
10.248 + if not genuine_means_genuine then
10.249 if no_poly_user_axioms then
10.250 let
10.251 val options =
10.252 @@ -611,12 +661,13 @@
10.253 in
10.254 print ("Try again with " ^
10.255 space_implode " " (serial_commas "and" ss) ^
10.256 - " to confirm that the " ^ word_model ^ " is genuine.")
10.257 + " to confirm that the " ^ das_wort_model ^
10.258 + " is genuine.")
10.259 end
10.260 else
10.261 print ("Nitpick is unable to guarantee the authenticity of \
10.262 - \the " ^ word_model ^ " in the presence of polymorphic \
10.263 - \axioms.")
10.264 + \the " ^ das_wort_model ^ " in the presence of \
10.265 + \polymorphic axioms.")
10.266 else
10.267 ();
10.268 NONE)
10.269 @@ -630,9 +681,9 @@
10.270 in
10.271 (case status of
10.272 SOME true => print ("Confirmation by \"auto\": The above " ^
10.273 - word_model ^ " is genuine.")
10.274 + das_wort_model ^ " is genuine.")
10.275 | SOME false => print ("Refutation by \"auto\": The above " ^
10.276 - word_model ^ " is spurious.")
10.277 + das_wort_model ^ " is spurious.")
10.278 | NONE => print "No confirmation by \"auto\".");
10.279 status
10.280 end
10.281 @@ -820,14 +871,20 @@
10.282 (print_m (fn () => excipit "ran out of some resource"); "unknown")
10.283 else if max_genuine = original_max_genuine then
10.284 if max_potential = original_max_potential then
10.285 - (print_m (K ("Nitpick found no " ^ word_model ^ ".")); "none")
10.286 + (print_m (fn () =>
10.287 + "Nitpick found no " ^ das_wort_model ^ "." ^
10.288 + (if not standard andalso not (null induct_dataTs) then
10.289 + " This suggests that the induction hypothesis might be \
10.290 + \general enough to prove this subgoal."
10.291 + else
10.292 + "")); "none")
10.293 else
10.294 - (print_m (K ("Nitpick could not find " ^
10.295 - (if max_genuine = 1 then "a better " ^ word_model ^ "."
10.296 - else "any better " ^ word_model ^ "s.")));
10.297 - "potential")
10.298 + (print_m (fn () =>
10.299 + "Nitpick could not find a" ^
10.300 + (if max_genuine = 1 then " better " ^ das_wort_model ^ "."
10.301 + else "ny better " ^ das_wort_model ^ "s.")); "potential")
10.302 else
10.303 - if would_be_genuine then "genuine" else "likely_genuine"
10.304 + if genuine_means_genuine then "genuine" else "likely_genuine"
10.305 | run_batches j n (batch :: batches) z =
10.306 let val (z as (_, max_genuine, _)) = run_batch j n batch z in
10.307 run_batches (j + 1) n (if max_genuine > 0 then batches else []) z
10.308 @@ -835,7 +892,7 @@
10.309
10.310 val (skipped, the_scopes) =
10.311 all_scopes ext_ctxt sym_break cards_assigns maxes_assigns iters_assigns
10.312 - bitss bisim_depths mono_Ts nonmono_Ts shallow_dataTs
10.313 + bitss bisim_depths mono_Ts nonmono_Ts deep_dataTs
10.314 val _ = if skipped > 0 then
10.315 print_m (fn () => "Too many scopes. Skipping " ^
10.316 string_of_int skipped ^ " scope" ^
10.317 @@ -868,9 +925,10 @@
10.318 else
10.319 error "Nitpick was interrupted."
10.320
10.321 -(* Proof.state -> params -> bool -> term -> string * Proof.state *)
10.322 -fun pick_nits_in_term state (params as {debug, timeout, expect, ...}) auto
10.323 - orig_assm_ts orig_t =
10.324 +(* Proof.state -> params -> bool -> int -> int -> int -> term
10.325 + -> string * Proof.state *)
10.326 +fun pick_nits_in_term state (params as {debug, timeout, expect, ...}) auto i n
10.327 + step orig_assm_ts orig_t =
10.328 if getenv "KODKODI" = "" then
10.329 (if auto then ()
10.330 else warning (Pretty.string_of (plazy install_kodkodi_message));
10.331 @@ -880,26 +938,29 @@
10.332 val deadline = Option.map (curry Time.+ (Time.now ())) timeout
10.333 val outcome as (outcome_code, _) =
10.334 time_limit (if debug then NONE else timeout)
10.335 - (pick_them_nits_in_term deadline state params auto orig_assm_ts)
10.336 - orig_t
10.337 + (pick_them_nits_in_term deadline state params auto i n step
10.338 + orig_assm_ts) orig_t
10.339 in
10.340 if expect = "" orelse outcome_code = expect then outcome
10.341 else error ("Unexpected outcome: " ^ quote outcome_code ^ ".")
10.342 end
10.343
10.344 -(* Proof.state -> params -> thm -> int -> string * Proof.state *)
10.345 -fun pick_nits_in_subgoal state params auto i =
10.346 +(* Proof.state -> params -> bool -> int -> int -> string * Proof.state *)
10.347 +fun pick_nits_in_subgoal state params auto i step =
10.348 let
10.349 val ctxt = Proof.context_of state
10.350 val t = state |> Proof.raw_goal |> #goal |> prop_of
10.351 in
10.352 - if Logic.count_prems t = 0 then
10.353 - (priority "No subgoal!"; ("none", state))
10.354 - else
10.355 + case Logic.count_prems t of
10.356 + 0 => (priority "No subgoal!"; ("none", state))
10.357 + | n =>
10.358 let
10.359 val assms = map term_of (Assumption.all_assms_of ctxt)
10.360 val (t, frees) = Logic.goal_params t i
10.361 - in pick_nits_in_term state params auto assms (subst_bounds (frees, t)) end
10.362 + in
10.363 + pick_nits_in_term state params auto i n step assms
10.364 + (subst_bounds (frees, t))
10.365 + end
10.366 end
10.367
10.368 end;
11.1 --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Mon Feb 01 14:12:12 2010 +0100
11.2 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Tue Feb 02 11:38:38 2010 +0100
11.3 @@ -1,6 +1,6 @@
11.4 (* Title: HOL/Tools/Nitpick/nitpick_hol.ML
11.5 Author: Jasmin Blanchette, TU Muenchen
11.6 - Copyright 2008, 2009
11.7 + Copyright 2008, 2009, 2010
11.8
11.9 Auxiliary HOL-related functions used by Nitpick.
11.10 *)
11.11 @@ -18,6 +18,7 @@
11.12 ctxt: Proof.context,
11.13 max_bisim_depth: int,
11.14 boxes: (typ option * bool option) list,
11.15 + stds: (typ option * bool) list,
11.16 wfs: (styp option * bool option) list,
11.17 user_axioms: bool option,
11.18 debug: bool,
11.19 @@ -165,6 +166,7 @@
11.20 ctxt: Proof.context,
11.21 max_bisim_depth: int,
11.22 boxes: (typ option * bool option) list,
11.23 + stds: (typ option * bool) list,
11.24 wfs: (styp option * bool option) list,
11.25 user_axioms: bool option,
11.26 debug: bool,
11.27 @@ -548,7 +550,7 @@
11.28 val is_typedef = is_some oo typedef_info
11.29 val is_real_datatype = is_some oo Datatype.get_info
11.30 (* theory -> typ -> bool *)
11.31 -fun is_quot_type _ (Type ("IntEx.my_int", _)) = true (* ### *)
11.32 +fun is_quot_type _ (Type ("IntEx.my_int", _)) = true (* FIXME *)
11.33 | is_quot_type _ _ = false
11.34 fun is_codatatype thy (T as Type (s, _)) =
11.35 not (null (AList.lookup (op =) (#codatatypes (Data.get thy)) s
11.36 @@ -615,9 +617,9 @@
11.37 | NONE => false)
11.38 | is_rep_fun _ _ = false
11.39 (* Proof.context -> styp -> bool *)
11.40 -fun is_quot_abs_fun _ ("IntEx.abs_my_int", _) = true (* ### *)
11.41 +fun is_quot_abs_fun _ ("IntEx.abs_my_int", _) = true (* FIXME *)
11.42 | is_quot_abs_fun _ _ = false
11.43 -fun is_quot_rep_fun _ ("IntEx.rep_my_int", _) = true (* ### *)
11.44 +fun is_quot_rep_fun _ ("IntEx.rep_my_int", _) = true (* FIXME *)
11.45 | is_quot_rep_fun _ _ = false
11.46
11.47 (* theory -> styp -> styp *)
11.48 @@ -648,12 +650,12 @@
11.49 end
11.50 handle TYPE ("dest_Type", _, _) => false
11.51 fun is_constr_like thy (s, T) =
11.52 - s = @{const_name FunBox} orelse s = @{const_name PairBox} orelse
11.53 + member (op =) [@{const_name FunBox}, @{const_name PairBox},
11.54 + @{const_name Quot}, @{const_name Zero_Rep},
11.55 + @{const_name Suc_Rep}] s orelse
11.56 let val (x as (s, T)) = (s, unbit_and_unbox_type T) in
11.57 Refute.is_IDT_constructor thy x orelse is_record_constr x orelse
11.58 (is_abs_fun thy x andalso is_pure_typedef thy (range_type T)) orelse
11.59 - s = @{const_name Quot} orelse
11.60 - s = @{const_name Zero_Rep} orelse s = @{const_name Suc_Rep} orelse
11.61 x = (@{const_name zero_nat_inst.zero_nat}, nat_T) orelse
11.62 is_coconstr thy x
11.63 end
11.64 @@ -710,7 +712,8 @@
11.65 box_type ext_ctxt (in_fun_lhs_for boxy) T1
11.66 --> box_type ext_ctxt (in_fun_rhs_for boxy) T2
11.67 | Type (z as ("*", Ts)) =>
11.68 - if should_box_type ext_ctxt boxy z then
11.69 + if boxy <> InConstr andalso boxy <> InSel
11.70 + andalso should_box_type ext_ctxt boxy z then
11.71 Type (@{type_name pair_box}, map (box_type ext_ctxt InSel) Ts)
11.72 else
11.73 Type ("*", map (box_type ext_ctxt
11.74 @@ -778,11 +781,11 @@
11.75 fun zero_const T = Const (@{const_name zero_nat_inst.zero_nat}, T)
11.76 fun suc_const T = Const (@{const_name Suc}, T --> T)
11.77
11.78 -(* theory -> typ -> styp list *)
11.79 -fun uncached_datatype_constrs thy (T as Type (s, Ts)) =
11.80 +(* extended_context -> typ -> styp list *)
11.81 +fun uncached_datatype_constrs ({thy, stds, ...} : extended_context)
11.82 + (T as Type (s, Ts)) =
11.83 (case AList.lookup (op =) (#codatatypes (Data.get thy)) s of
11.84 - SOME (_, xs' as (_ :: _)) =>
11.85 - map (apsnd (repair_constr_type thy T)) xs'
11.86 + SOME (_, xs' as (_ :: _)) => map (apsnd (repair_constr_type thy T)) xs'
11.87 | _ =>
11.88 if is_datatype thy T then
11.89 case Datatype.get_info thy s of
11.90 @@ -793,6 +796,8 @@
11.91 map (fn (s', Us) =>
11.92 (s', map (Refute.typ_of_dtyp descr (dtyps ~~ Ts)) Us
11.93 ---> T)) constrs
11.94 + |> (triple_lookup (type_match thy) stds T |> the |> not) ?
11.95 + cons (@{const_name NonStd}, @{typ \<xi>} --> T)
11.96 end
11.97 | NONE =>
11.98 if is_record_type T then
11.99 @@ -815,12 +820,11 @@
11.100 [])
11.101 | uncached_datatype_constrs _ _ = []
11.102 (* extended_context -> typ -> styp list *)
11.103 -fun datatype_constrs (ext_ctxt as {thy, constr_cache, ...} : extended_context)
11.104 - T =
11.105 +fun datatype_constrs (ext_ctxt as {constr_cache, ...}) T =
11.106 case AList.lookup (op =) (!constr_cache) T of
11.107 SOME xs => xs
11.108 | NONE =>
11.109 - let val xs = uncached_datatype_constrs thy T in
11.110 + let val xs = uncached_datatype_constrs ext_ctxt T in
11.111 (Unsynchronized.change constr_cache (cons (T, xs)); xs)
11.112 end
11.113 fun boxed_datatype_constrs ext_ctxt =
11.114 @@ -838,6 +842,7 @@
11.115 AList.lookup (op =) (boxed_datatype_constrs ext_ctxt (domain_type T')) s
11.116 |> the |> pair s
11.117 end
11.118 +
11.119 (* extended_context -> styp -> term *)
11.120 fun discr_term_for_constr ext_ctxt (x as (s, T)) =
11.121 let val dataT = body_type T in
11.122 @@ -849,7 +854,6 @@
11.123 else
11.124 Abs (Name.uu, dataT, @{const True})
11.125 end
11.126 -
11.127 (* extended_context -> styp -> term -> term *)
11.128 fun discriminate_value (ext_ctxt as {thy, ...}) (x as (_, T)) t =
11.129 case strip_comb t of
11.130 @@ -919,7 +923,7 @@
11.131 (@{const_name Pair}, T1 --> T2 --> T)
11.132 end
11.133 else
11.134 - datatype_constrs ext_ctxt T |> the_single
11.135 + datatype_constrs ext_ctxt T |> hd
11.136 val arg_Ts = binder_types T'
11.137 in
11.138 list_comb (Const x', map2 (select_nth_constr_arg thy x' t)
11.139 @@ -1361,10 +1365,9 @@
11.140 val normal_y = normal_t $ y_var
11.141 val is_unknown_t = Const (@{const_name is_unknown}, rep_T --> bool_T)
11.142 in
11.143 - [Logic.mk_equals (sel_a_t, normal_t $ sel_a_t),
11.144 + [Logic.mk_equals (normal_t $ sel_a_t, sel_a_t),
11.145 Logic.list_implies
11.146 - ([@{const Not} $ (HOLogic.mk_eq (x_var, y_var)),
11.147 - @{const Not} $ (is_unknown_t $ normal_x),
11.148 + ([@{const Not} $ (is_unknown_t $ normal_x),
11.149 @{const Not} $ (is_unknown_t $ normal_y),
11.150 equiv_rel $ x_var $ y_var] |> map HOLogic.mk_Trueprop,
11.151 Logic.mk_equals (normal_x, normal_y)),
11.152 @@ -1388,17 +1391,27 @@
11.153 fun optimized_case_def (ext_ctxt as {thy, ...}) dataT res_T =
11.154 let
11.155 val xs = datatype_constrs ext_ctxt dataT
11.156 - val func_Ts = map ((fn T => binder_types T ---> res_T) o snd) xs
11.157 - val (xs', x) = split_last xs
11.158 + val xs' = filter_out (fn (s, _) => s = @{const_name NonStd}) xs
11.159 + val func_Ts = map ((fn T => binder_types T ---> res_T) o snd) xs'
11.160 in
11.161 - constr_case_body thy (1, x)
11.162 - |> fold_rev (add_constr_case ext_ctxt res_T) (length xs downto 2 ~~ xs')
11.163 + (if length xs = length xs' then
11.164 + let
11.165 + val (xs'', x) = split_last xs'
11.166 + in
11.167 + constr_case_body thy (1, x)
11.168 + |> fold_rev (add_constr_case ext_ctxt res_T)
11.169 + (length xs' downto 2 ~~ xs'')
11.170 + end
11.171 + else
11.172 + Const (@{const_name undefined}, dataT --> res_T) $ Bound 0
11.173 + |> fold_rev (add_constr_case ext_ctxt res_T)
11.174 + (length xs' downto 1 ~~ xs'))
11.175 |> fold_rev (curry absdummy) (func_Ts @ [dataT])
11.176 end
11.177
11.178 (* extended_context -> string -> typ -> typ -> term -> term *)
11.179 fun optimized_record_get (ext_ctxt as {thy, ...}) s rec_T res_T t =
11.180 - let val constr_x = the_single (datatype_constrs ext_ctxt rec_T) in
11.181 + let val constr_x = hd (datatype_constrs ext_ctxt rec_T) in
11.182 case no_of_record_field thy s rec_T of
11.183 ~1 => (case rec_T of
11.184 Type (_, Ts as _ :: _) =>
11.185 @@ -1416,7 +1429,7 @@
11.186 (* extended_context -> string -> typ -> term -> term -> term *)
11.187 fun optimized_record_update (ext_ctxt as {thy, ...}) s rec_T fun_t rec_t =
11.188 let
11.189 - val constr_x as (_, constr_T) = the_single (datatype_constrs ext_ctxt rec_T)
11.190 + val constr_x as (_, constr_T) = hd (datatype_constrs ext_ctxt rec_T)
11.191 val Ts = binder_types constr_T
11.192 val n = length Ts
11.193 val special_j = no_of_record_field thy s rec_T
11.194 @@ -1606,7 +1619,7 @@
11.195 case length ts of
11.196 0 => (do_term depth Ts (eta_expand Ts t 1), [])
11.197 | _ => (optimized_record_get ext_ctxt s (domain_type T)
11.198 - (range_type T) (hd ts), tl ts)
11.199 + (range_type T) (do_term depth Ts (hd ts)), tl ts)
11.200 else if is_record_update thy x then
11.201 case length ts of
11.202 2 => (optimized_record_update ext_ctxt
11.203 @@ -2077,7 +2090,7 @@
11.204 (t0 as Const (@{const_name "=="}, _)) $ t1 $ t2 =>
11.205 do_eq_or_imp Ts true def t0 t1 t2 seen
11.206 | (t0 as @{const "==>"}) $ t1 $ t2 =>
11.207 - do_eq_or_imp Ts false def t0 t1 t2 seen
11.208 + if def then (t, []) else do_eq_or_imp Ts false def t0 t1 t2 seen
11.209 | (t0 as Const (@{const_name "op ="}, _)) $ t1 $ t2 =>
11.210 do_eq_or_imp Ts true def t0 t1 t2 seen
11.211 | (t0 as @{const "op -->"}) $ t1 $ t2 =>
11.212 @@ -2126,27 +2139,33 @@
11.213 | aux _ t = t
11.214 (* bool -> bool -> term -> term -> term -> term *)
11.215 and aux_eq careful pass1 t0 t1 t2 =
11.216 - (if careful then
11.217 - raise SAME ()
11.218 - else if axiom andalso is_Var t2 andalso
11.219 - num_occs_of_var (dest_Var t2) = 1 then
11.220 - @{const True}
11.221 - else case strip_comb t2 of
11.222 - (Const (x as (s, T)), args) =>
11.223 - let val arg_Ts = binder_types T in
11.224 - if length arg_Ts = length args andalso
11.225 - (is_constr thy x orelse s = @{const_name Pair} orelse
11.226 - x = (@{const_name Suc}, nat_T --> nat_T)) andalso
11.227 - (not careful orelse not (is_Var t1) orelse
11.228 - String.isPrefix val_var_prefix (fst (fst (dest_Var t1)))) then
11.229 - discriminate_value ext_ctxt x t1 ::
11.230 - map3 (sel_eq x t1) (index_seq 0 (length args)) arg_Ts args
11.231 - |> foldr1 s_conj
11.232 - |> body_type (type_of t0) = prop_T ? HOLogic.mk_Trueprop
11.233 - else
11.234 - raise SAME ()
11.235 - end
11.236 - | _ => raise SAME ())
11.237 + ((if careful then
11.238 + raise SAME ()
11.239 + else if axiom andalso is_Var t2 andalso
11.240 + num_occs_of_var (dest_Var t2) = 1 then
11.241 + @{const True}
11.242 + else case strip_comb t2 of
11.243 + (* The first case is not as general as it could be. *)
11.244 + (Const (@{const_name PairBox}, _),
11.245 + [Const (@{const_name fst}, _) $ Var z1,
11.246 + Const (@{const_name snd}, _) $ Var z2]) =>
11.247 + if z1 = z2 andalso num_occs_of_var z1 = 2 then @{const True}
11.248 + else raise SAME ()
11.249 + | (Const (x as (s, T)), args) =>
11.250 + let val arg_Ts = binder_types T in
11.251 + if length arg_Ts = length args andalso
11.252 + (is_constr thy x orelse s = @{const_name Pair} orelse
11.253 + x = (@{const_name Suc}, nat_T --> nat_T)) andalso
11.254 + (not careful orelse not (is_Var t1) orelse
11.255 + String.isPrefix val_var_prefix (fst (fst (dest_Var t1)))) then
11.256 + discriminate_value ext_ctxt x t1 ::
11.257 + map3 (sel_eq x t1) (index_seq 0 (length args)) arg_Ts args
11.258 + |> foldr1 s_conj
11.259 + else
11.260 + raise SAME ()
11.261 + end
11.262 + | _ => raise SAME ())
11.263 + |> body_type (type_of t0) = prop_T ? HOLogic.mk_Trueprop)
11.264 handle SAME () => if pass1 then aux_eq careful false t0 t2 t1
11.265 else t0 $ aux false t2 $ aux false t1
11.266 (* styp -> term -> int -> typ -> term -> term *)
11.267 @@ -2947,7 +2966,7 @@
11.268 | Const (s as @{const_name The}, T) => do_description_operator s T
11.269 | Const (s as @{const_name Eps}, T) => do_description_operator s T
11.270 | Const (@{const_name quot_normal}, Type ("fun", [_, T2])) =>
11.271 - let val T' = box_type ext_ctxt InFunRHS1 T2 in
11.272 + let val T' = box_type ext_ctxt InSel T2 in
11.273 Const (@{const_name quot_normal}, T' --> T')
11.274 end
11.275 | Const (s as @{const_name Tha}, T) => do_description_operator s T
11.276 @@ -2960,7 +2979,8 @@
11.277 T
11.278 else if is_constr_like thy x then
11.279 box_type ext_ctxt InConstr T
11.280 - else if is_sel s orelse is_rep_fun thy x then
11.281 + else if is_sel s
11.282 + orelse is_rep_fun thy x then
11.283 box_type ext_ctxt InSel T
11.284 else
11.285 box_type ext_ctxt InExpr T)
11.286 @@ -3495,6 +3515,7 @@
11.287 #> simplify_constrs_and_sels thy
11.288 #> distribute_quantifiers
11.289 #> push_quantifiers_inward thy
11.290 + #> Envir.eta_contract
11.291 #> not core ? Refute.close_form
11.292 #> shorten_abs_vars
11.293 in
12.1 --- a/src/HOL/Tools/Nitpick/nitpick_isar.ML Mon Feb 01 14:12:12 2010 +0100
12.2 +++ b/src/HOL/Tools/Nitpick/nitpick_isar.ML Tue Feb 02 11:38:38 2010 +0100
12.3 @@ -1,6 +1,6 @@
12.4 (* Title: HOL/Tools/Nitpick/nitpick_isar.ML
12.5 Author: Jasmin Blanchette, TU Muenchen
12.6 - Copyright 2008, 2009
12.7 + Copyright 2008, 2009, 2010
12.8
12.9 Adds the "nitpick" and "nitpick_params" commands to Isabelle/Isar's outer
12.10 syntax.
12.11 @@ -28,9 +28,8 @@
12.12
12.13 val _ =
12.14 ProofGeneralPgip.add_preference Preferences.category_tracing
12.15 - (Preferences.bool_pref auto
12.16 - "auto-nitpick"
12.17 - "Whether to run Nitpick automatically.")
12.18 + (Preferences.bool_pref auto "auto-nitpick"
12.19 + "Whether to run Nitpick automatically.")
12.20
12.21 type raw_param = string * string list
12.22
12.23 @@ -41,6 +40,7 @@
12.24 ("bisim_depth", ["7"]),
12.25 ("box", ["smart"]),
12.26 ("mono", ["smart"]),
12.27 + ("std", ["true"]),
12.28 ("wf", ["smart"]),
12.29 ("sat_solver", ["smart"]),
12.30 ("batch_size", ["smart"]),
12.31 @@ -79,6 +79,7 @@
12.32 val negated_params =
12.33 [("dont_box", "box"),
12.34 ("non_mono", "mono"),
12.35 + ("non_std", "std"),
12.36 ("non_wf", "wf"),
12.37 ("non_blocking", "blocking"),
12.38 ("satisfy", "falsify"),
12.39 @@ -110,8 +111,8 @@
12.40 AList.defined (op =) negated_params s orelse
12.41 s = "max" orelse s = "eval" orelse s = "expect" orelse
12.42 exists (fn p => String.isPrefix (p ^ " ") s)
12.43 - ["card", "max", "iter", "box", "dont_box", "mono", "non_mono", "wf",
12.44 - "non_wf", "format"]
12.45 + ["card", "max", "iter", "box", "dont_box", "mono", "non_mono", "std",
12.46 + "non_std", "wf", "non_wf", "format"]
12.47
12.48 (* string * 'a -> unit *)
12.49 fun check_raw_param (s, _) =
12.50 @@ -244,6 +245,14 @@
12.51 value |> stringify_raw_param_value
12.52 |> int_seq_from_string name min_int))
12.53 (filter (String.isPrefix (prefix ^ " ") o fst) raw_params)
12.54 + (* (string -> 'a) -> string -> ('a option * bool) list *)
12.55 + fun lookup_bool_assigns read prefix =
12.56 + (NONE, lookup_bool prefix)
12.57 + :: map (fn (name, value) =>
12.58 + (SOME (read (String.extract (name, size prefix + 1, NONE))),
12.59 + value |> stringify_raw_param_value
12.60 + |> bool_option_from_string false name |> the))
12.61 + (filter (String.isPrefix (prefix ^ " ") o fst) raw_params)
12.62 (* (string -> 'a) -> string -> ('a option * bool option) list *)
12.63 fun lookup_bool_option_assigns read prefix =
12.64 (NONE, lookup_bool_option prefix)
12.65 @@ -297,6 +306,7 @@
12.66 NONE
12.67 | (NONE, _) => NONE) cards_assigns
12.68 val monos = lookup_bool_option_assigns read_type_polymorphic "mono"
12.69 + val stds = lookup_bool_assigns read_type_polymorphic "std"
12.70 val wfs = lookup_bool_option_assigns read_const_polymorphic "wf"
12.71 val sat_solver = lookup_string "sat_solver"
12.72 val blocking = not auto andalso lookup_bool "blocking"
12.73 @@ -339,9 +349,10 @@
12.74 in
12.75 {cards_assigns = cards_assigns, maxes_assigns = maxes_assigns,
12.76 iters_assigns = iters_assigns, bitss = bitss, bisim_depths = bisim_depths,
12.77 - boxes = boxes, monos = monos, wfs = wfs, sat_solver = sat_solver,
12.78 - blocking = blocking, falsify = falsify, debug = debug, verbose = verbose,
12.79 - overlord = overlord, user_axioms = user_axioms, assms = assms,
12.80 + boxes = boxes, monos = monos, stds = stds, wfs = wfs,
12.81 + sat_solver = sat_solver, blocking = blocking, falsify = falsify,
12.82 + debug = debug, verbose = verbose, overlord = overlord,
12.83 + user_axioms = user_axioms, assms = assms,
12.84 merge_type_vars = merge_type_vars, binary_ints = binary_ints,
12.85 destroy_constrs = destroy_constrs, specialize = specialize,
12.86 skolemize = skolemize, star_linear_preds = star_linear_preds,
12.87 @@ -416,8 +427,9 @@
12.88 | Refute.REFUTE (loc, details) =>
12.89 error ("Unhandled Refute error (" ^ quote loc ^ "): " ^ details ^ ".")
12.90
12.91 -(* raw_param list -> bool -> int -> Proof.state -> bool * Proof.state *)
12.92 -fun pick_nits override_params auto i state =
12.93 +
12.94 +(* raw_param list -> bool -> int -> int -> Proof.state -> bool * Proof.state *)
12.95 +fun pick_nits override_params auto i step state =
12.96 let
12.97 val thy = Proof.theory_of state
12.98 val ctxt = Proof.context_of state
12.99 @@ -431,7 +443,7 @@
12.100 |> (if auto then perhaps o try
12.101 else if debug then fn f => fn x => f x
12.102 else handle_exceptions ctxt)
12.103 - (fn (_, state) => pick_nits_in_subgoal state params auto i
12.104 + (fn (_, state) => pick_nits_in_subgoal state params auto i step
12.105 |>> curry (op =) "genuine")
12.106 in
12.107 if auto orelse blocking then go ()
12.108 @@ -441,9 +453,9 @@
12.109 (* raw_param list option * int option -> Toplevel.transition
12.110 -> Toplevel.transition *)
12.111 fun nitpick_trans (opt_params, opt_i) =
12.112 - Toplevel.keep (K ()
12.113 - o snd o pick_nits (these opt_params) false (the_default 1 opt_i)
12.114 - o Toplevel.proof_of)
12.115 + Toplevel.keep (fn st =>
12.116 + (pick_nits (these opt_params) false (the_default 1 opt_i)
12.117 + (Toplevel.proof_position_of st) (Toplevel.proof_of st); ()))
12.118
12.119 (* raw_param -> string *)
12.120 fun string_for_raw_param (name, value) =
12.121 @@ -477,7 +489,7 @@
12.122
12.123 (* Proof.state -> bool * Proof.state *)
12.124 fun auto_nitpick state =
12.125 - if not (!auto) then (false, state) else pick_nits [] true 1 state
12.126 + if not (!auto) then (false, state) else pick_nits [] true 1 0 state
12.127
12.128 val setup = Auto_Counterexample.register_tool ("nitpick", auto_nitpick)
12.129
13.1 --- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Mon Feb 01 14:12:12 2010 +0100
13.2 +++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Tue Feb 02 11:38:38 2010 +0100
13.3 @@ -1,6 +1,6 @@
13.4 (* Title: HOL/Tools/Nitpick/nitpick_kodkod.ML
13.5 Author: Jasmin Blanchette, TU Muenchen
13.6 - Copyright 2008, 2009
13.7 + Copyright 2008, 2009, 2010
13.8
13.9 Kodkod problem generator part of Kodkod.
13.10 *)
13.11 @@ -285,8 +285,8 @@
13.12 (* Proof.context -> bool -> string -> typ -> rep -> string *)
13.13 fun bound_comment ctxt debug nick T R =
13.14 short_name nick ^
13.15 - (if debug then " :: " ^ plain_string_from_yxml (Syntax.string_of_typ ctxt T)
13.16 - else "") ^ " : " ^ string_for_rep R
13.17 + (if debug then " :: " ^ unyxml (Syntax.string_of_typ ctxt T) else "") ^
13.18 + " : " ^ string_for_rep R
13.19
13.20 (* Proof.context -> bool -> nut -> KK.bound *)
13.21 fun bound_for_plain_rel ctxt debug (u as FreeRel (x, T, R, nick)) =
13.22 @@ -754,7 +754,7 @@
13.23 (* extended_context -> kodkod_constrs -> nut NameTable.table -> dtype_spec list
13.24 -> dtype_spec -> nfa_entry option *)
13.25 fun nfa_entry_for_datatype _ _ _ _ ({co = true, ...} : dtype_spec) = NONE
13.26 - | nfa_entry_for_datatype _ _ _ _ {shallow = true, ...} = NONE
13.27 + | nfa_entry_for_datatype _ _ _ _ {deep = false, ...} = NONE
13.28 | nfa_entry_for_datatype ext_ctxt kk rel_table dtypes {typ, constrs, ...} =
13.29 SOME (typ, maps (nfa_transitions_for_constr ext_ctxt kk rel_table dtypes
13.30 o #const) constrs)
13.31 @@ -926,7 +926,7 @@
13.32
13.33 (* extended_context -> int -> int Typtab.table -> kodkod_constrs
13.34 -> nut NameTable.table -> dtype_spec -> KK.formula list *)
13.35 -fun other_axioms_for_datatype _ _ _ _ _ {shallow = true, ...} = []
13.36 +fun other_axioms_for_datatype _ _ _ _ _ {deep = false, ...} = []
13.37 | other_axioms_for_datatype ext_ctxt bits ofs kk rel_table
13.38 (dtype as {typ, ...}) =
13.39 let val j0 = offset_of_type ofs typ in
14.1 --- a/src/HOL/Tools/Nitpick/nitpick_model.ML Mon Feb 01 14:12:12 2010 +0100
14.2 +++ b/src/HOL/Tools/Nitpick/nitpick_model.ML Tue Feb 02 11:38:38 2010 +0100
14.3 @@ -1,6 +1,6 @@
14.4 (* Title: HOL/Tools/Nitpick/nitpick_model.ML
14.5 Author: Jasmin Blanchette, TU Muenchen
14.6 - Copyright 2009
14.7 + Copyright 2009, 2010
14.8
14.9 Model reconstruction for Nitpick.
14.10 *)
14.11 @@ -53,7 +53,8 @@
14.12 val base_mixfix = "_\<^bsub>base\<^esub>"
14.13 val step_mixfix = "_\<^bsub>step\<^esub>"
14.14 val abs_mixfix = "\<guillemotleft>_\<guillemotright>"
14.15 -val non_opt_name = nitpick_prefix ^ "non_opt"
14.16 +val opt_flag = nitpick_prefix ^ "opt"
14.17 +val non_opt_flag = nitpick_prefix ^ "non_opt"
14.18
14.19 (* string -> int -> string *)
14.20 fun atom_suffix s j =
14.21 @@ -62,7 +63,10 @@
14.22 ? prefix "\<^isub>,"
14.23 (* string -> typ -> int -> string *)
14.24 fun atom_name prefix (T as Type (s, _)) j =
14.25 - prefix ^ substring (shortest_name s, 0, 1) ^ atom_suffix s j
14.26 + let val s' = shortest_name s in
14.27 + prefix ^ (if String.isPrefix "\\" s' then s' else substring (s', 0, 1)) ^
14.28 + atom_suffix s j
14.29 + end
14.30 | atom_name prefix (T as TFree (s, _)) j =
14.31 prefix ^ perhaps (try (unprefix "'")) s ^ atom_suffix s j
14.32 | atom_name _ T _ = raise TYPE ("Nitpick_Model.atom_name", [T], [])
14.33 @@ -139,23 +143,21 @@
14.34 let
14.35 (* typ -> typ -> (term * term) list -> term *)
14.36 fun aux T1 T2 [] =
14.37 - Const (if maybe_opt orelse T2 <> bool_T then @{const_name undefined}
14.38 - else non_opt_name, T1 --> T2)
14.39 + Const (if maybe_opt then opt_flag else non_opt_flag, T1 --> T2)
14.40 | aux T1 T2 ((t1, t2) :: ps) =
14.41 Const (@{const_name fun_upd}, (T1 --> T2) --> T1 --> T2 --> T1 --> T2)
14.42 $ aux T1 T2 ps $ t1 $ t2
14.43 in aux T1 T2 o rev end
14.44 (* term -> bool *)
14.45 -fun is_plain_fun (Const (s, _)) =
14.46 - (s = @{const_name undefined} orelse s = non_opt_name)
14.47 +fun is_plain_fun (Const (s, _)) = (s = opt_flag orelse s = non_opt_flag)
14.48 | is_plain_fun (Const (@{const_name fun_upd}, _) $ t0 $ _ $ _) =
14.49 is_plain_fun t0
14.50 | is_plain_fun _ = false
14.51 (* term -> bool * (term list * term list) *)
14.52 val dest_plain_fun =
14.53 let
14.54 - (* term -> term list * term list *)
14.55 - fun aux (Const (s, _)) = (s <> non_opt_name, ([], []))
14.56 + (* term -> bool * (term list * term list) *)
14.57 + fun aux (Const (s, _)) = (s <> non_opt_flag, ([], []))
14.58 | aux (Const (@{const_name fun_upd}, _) $ t0 $ t1 $ t2) =
14.59 let val (s, (ts1, ts2)) = aux t0 in (s, (t1 :: ts1, t2 :: ts2)) end
14.60 | aux t = raise TERM ("Nitpick_Model.dest_plain_fun", [t])
14.61 @@ -300,7 +302,7 @@
14.62 aux' ps
14.63 in aux end
14.64 (* typ list -> term -> term *)
14.65 - fun setify_mapify_funs Ts t =
14.66 + fun polish_funs Ts t =
14.67 (case fastype_of1 (Ts, t) of
14.68 Type ("fun", [T1, T2]) =>
14.69 if is_plain_fun t then
14.70 @@ -308,7 +310,7 @@
14.71 @{typ bool} =>
14.72 let
14.73 val (maybe_opt, ts_pair) =
14.74 - dest_plain_fun t ||> pairself (map (setify_mapify_funs Ts))
14.75 + dest_plain_fun t ||> pairself (map (polish_funs Ts))
14.76 in
14.77 make_set maybe_opt T1 T2
14.78 (sort_wrt (truth_const_sort_key o snd) (op ~~ ts_pair))
14.79 @@ -316,7 +318,7 @@
14.80 | Type (@{type_name option}, [T2']) =>
14.81 let
14.82 val ts_pair = snd (dest_plain_fun t)
14.83 - |> pairself (map (setify_mapify_funs Ts))
14.84 + |> pairself (map (polish_funs Ts))
14.85 in make_map T1 T2 T2' (rev (op ~~ ts_pair)) end
14.86 | _ => raise SAME ()
14.87 else
14.88 @@ -324,9 +326,18 @@
14.89 | _ => raise SAME ())
14.90 handle SAME () =>
14.91 case t of
14.92 - t1 $ t2 => setify_mapify_funs Ts t1 $ setify_mapify_funs Ts t2
14.93 - | Abs (s, T, t') => Abs (s, T, setify_mapify_funs (T :: Ts) t')
14.94 - | _ => t
14.95 + (t1 as Const (@{const_name fun_upd}, _) $ t11 $ _)
14.96 + $ (t2 as Const (s, _)) =>
14.97 + if s = unknown then polish_funs Ts t11
14.98 + else polish_funs Ts t1 $ polish_funs Ts t2
14.99 + | t1 $ t2 => polish_funs Ts t1 $ polish_funs Ts t2
14.100 + | Abs (s, T, t') => Abs (s, T, polish_funs (T :: Ts) t')
14.101 + | Const (s, Type ("fun", [T1, T2])) =>
14.102 + if s = opt_flag orelse s = non_opt_flag then
14.103 + Abs ("x", T1, Const (unknown, T2))
14.104 + else
14.105 + t
14.106 + | t => t
14.107 (* bool -> typ -> typ -> typ -> term list -> term list -> term *)
14.108 fun make_fun maybe_opt T1 T2 T' ts1 ts2 =
14.109 ts1 ~~ ts2 |> sort (nice_term_ord o pairself fst)
14.110 @@ -371,7 +382,7 @@
14.111 HOLogic.mk_number nat_T j
14.112 else case datatype_spec datatypes T of
14.113 NONE => atom for_auto T j
14.114 - | SOME {shallow = true, ...} => atom for_auto T j
14.115 + | SOME {deep = false, ...} => atom for_auto T j
14.116 | SOME {co, constrs, ...} =>
14.117 let
14.118 (* styp -> int list *)
14.119 @@ -437,13 +448,16 @@
14.120 | n2 => Const (@{const_name Algebras.divide},
14.121 num_T --> num_T --> num_T)
14.122 $ mk_num n1 $ mk_num n2)
14.123 - | _ => raise TERM ("Nitpick_Model.reconstruct_term.term_\
14.124 - \for_atom (Abs_Frac)", ts)
14.125 + | _ => raise TERM ("Nitpick_Model.reconstruct_term.\
14.126 + \term_for_atom (Abs_Frac)", ts)
14.127 end
14.128 else if not for_auto andalso
14.129 (is_abs_fun thy constr_x orelse
14.130 constr_s = @{const_name Quot}) then
14.131 Const (abs_name, constr_T) $ the_single ts
14.132 + else if not for_auto andalso
14.133 + constr_s = @{const_name NonStd} then
14.134 + Const (fst (dest_Const (the_single ts)), T)
14.135 else
14.136 list_comb (Const constr_x, ts)
14.137 in
14.138 @@ -509,8 +523,7 @@
14.139 Refute.string_of_typ T ^ " " ^ string_for_rep R ^ " " ^
14.140 string_of_int (length jss))
14.141 in
14.142 - (not for_auto ? setify_mapify_funs []) o unbit_and_unbox_term
14.143 - oooo term_for_rep []
14.144 + (not for_auto ? polish_funs []) o unbit_and_unbox_term oooo term_for_rep []
14.145 end
14.146
14.147 (* scope -> nut list -> nut NameTable.table -> KK.raw_bound list -> nut
14.148 @@ -522,8 +535,7 @@
14.149 (rep_of name)
14.150 end
14.151
14.152 -(* Proof.context
14.153 - -> (string * string * string * string * string) * Proof.context *)
14.154 +(* Proof.context -> (string * string * string * string) * Proof.context *)
14.155 fun add_wacky_syntax ctxt =
14.156 let
14.157 (* term -> string *)
14.158 @@ -573,13 +585,13 @@
14.159 -> nut list -> nut list -> nut NameTable.table -> KK.raw_bound list
14.160 -> Pretty.T * bool *)
14.161 fun reconstruct_hol_model {show_skolems, show_datatypes, show_consts}
14.162 - ({ext_ctxt as {thy, ctxt, max_bisim_depth, boxes, wfs, user_axioms,
14.163 - debug, binary_ints, destroy_constrs, specialize,
14.164 - skolemize, star_linear_preds, uncurry, fast_descrs,
14.165 - tac_timeout, evals, case_names, def_table, nondef_table,
14.166 - user_nondefs, simp_table, psimp_table, intro_table,
14.167 - ground_thm_table, ersatz_table, skolems, special_funs,
14.168 - unrolled_preds, wf_cache, constr_cache},
14.169 + ({ext_ctxt as {thy, ctxt, max_bisim_depth, boxes, stds, wfs,
14.170 + user_axioms, debug, binary_ints, destroy_constrs,
14.171 + specialize, skolemize, star_linear_preds, uncurry,
14.172 + fast_descrs, tac_timeout, evals, case_names, def_table,
14.173 + nondef_table, user_nondefs, simp_table, psimp_table,
14.174 + intro_table, ground_thm_table, ersatz_table, skolems,
14.175 + special_funs, unrolled_preds, wf_cache, constr_cache},
14.176 card_assigns, bits, bisim_depth, datatypes, ofs} : scope)
14.177 formats all_frees free_names sel_names nonsel_names rel_table bounds =
14.178 let
14.179 @@ -587,7 +599,7 @@
14.180 add_wacky_syntax ctxt
14.181 val ext_ctxt =
14.182 {thy = thy, ctxt = ctxt, max_bisim_depth = max_bisim_depth, boxes = boxes,
14.183 - wfs = wfs, user_axioms = user_axioms, debug = debug,
14.184 + stds = stds, wfs = wfs, user_axioms = user_axioms, debug = debug,
14.185 binary_ints = binary_ints, destroy_constrs = destroy_constrs,
14.186 specialize = specialize, skolemize = skolemize,
14.187 star_linear_preds = star_linear_preds, uncurry = uncurry,
14.188 @@ -650,16 +662,15 @@
14.189 Pretty.block (Pretty.breaks
14.190 [Syntax.pretty_typ ctxt (unbit_and_unbox_type typ), Pretty.str "=",
14.191 Pretty.enum "," "{" "}"
14.192 - (map (Syntax.pretty_term ctxt) (all_values_of_type card typ)
14.193 - @ (if complete then [] else [Pretty.str unrep]))])
14.194 + (map (Syntax.pretty_term ctxt) (all_values_of_type card typ) @
14.195 + (if complete then [] else [Pretty.str unrep]))])
14.196 (* typ -> dtype_spec list *)
14.197 fun integer_datatype T =
14.198 [{typ = T, card = card_of_type card_assigns T, co = false,
14.199 - complete = false, concrete = true, shallow = false, constrs = []}]
14.200 + complete = false, concrete = true, deep = true, constrs = []}]
14.201 handle TYPE ("Nitpick_HOL.card_of_type", _, _) => []
14.202 val (codatatypes, datatypes) =
14.203 - datatypes |> filter_out #shallow
14.204 - |> List.partition #co
14.205 + datatypes |> filter #deep |> List.partition #co
14.206 ||> append (integer_datatype nat_T @ integer_datatype int_T)
14.207 val block_of_datatypes =
14.208 if show_datatypes andalso not (null datatypes) then
15.1 --- a/src/HOL/Tools/Nitpick/nitpick_mono.ML Mon Feb 01 14:12:12 2010 +0100
15.2 +++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML Tue Feb 02 11:38:38 2010 +0100
15.3 @@ -1,16 +1,17 @@
15.4 (* Title: HOL/Tools/Nitpick/nitpick_mono.ML
15.5 Author: Jasmin Blanchette, TU Muenchen
15.6 - Copyright 2009
15.7 + Copyright 2009, 2010
15.8
15.9 Monotonicity predicate for higher-order logic.
15.10 *)
15.11
15.12 signature NITPICK_MONO =
15.13 sig
15.14 + datatype sign = Plus | Minus
15.15 type extended_context = Nitpick_HOL.extended_context
15.16
15.17 val formulas_monotonic :
15.18 - extended_context -> typ -> term list -> term list -> term -> bool
15.19 + extended_context -> typ -> sign -> term list -> term list -> term -> bool
15.20 end;
15.21
15.22 structure Nitpick_Mono : NITPICK_MONO =
15.23 @@ -21,7 +22,7 @@
15.24
15.25 type var = int
15.26
15.27 -datatype sign = Pos | Neg
15.28 +datatype sign = Plus | Minus
15.29 datatype sign_atom = S of sign | V of var
15.30
15.31 type literal = var * sign
15.32 @@ -54,13 +55,13 @@
15.33 if null xs then "" else "\<^bsub>" ^ string_for_vars sep xs ^ "\<^esub>"
15.34
15.35 (* sign -> string *)
15.36 -fun string_for_sign Pos = "+"
15.37 - | string_for_sign Neg = "-"
15.38 +fun string_for_sign Plus = "+"
15.39 + | string_for_sign Minus = "-"
15.40
15.41 (* sign -> sign -> sign *)
15.42 -fun xor sn1 sn2 = if sn1 = sn2 then Pos else Neg
15.43 +fun xor sn1 sn2 = if sn1 = sn2 then Plus else Minus
15.44 (* sign -> sign *)
15.45 -val negate = xor Neg
15.46 +val negate = xor Minus
15.47
15.48 (* sign_atom -> string *)
15.49 fun string_for_sign_atom (S sn) = string_for_sign sn
15.50 @@ -152,7 +153,7 @@
15.51
15.52 (* string * typ list -> ctype list -> ctype *)
15.53 fun constr_ctype_for_binders z Cs =
15.54 - fold_rev (fn C => curry3 CFun C (S Neg)) Cs (CRec z)
15.55 + fold_rev (fn C => curry3 CFun C (S Minus)) Cs (CRec z)
15.56
15.57 (* ((string * typ list) * ctype) list -> ctype list -> ctype -> ctype *)
15.58 fun repair_ctype _ _ CAlpha = CAlpha
15.59 @@ -199,7 +200,7 @@
15.60 exists_alpha_sub_ctype_fresh C1 then
15.61 V (Unsynchronized.inc max_fresh)
15.62 else
15.63 - S Neg
15.64 + S Minus
15.65 in CFun (C1, a, C2) end
15.66 (* typ -> ctype *)
15.67 and do_type T =
15.68 @@ -252,13 +253,13 @@
15.69 fun prodC_factors (CPair (C1, C2)) = maps prodC_factors [C1, C2]
15.70 | prodC_factors C = [C]
15.71 (* ctype -> ctype list * ctype *)
15.72 -fun curried_strip_ctype (CFun (C1, S Neg, C2)) =
15.73 +fun curried_strip_ctype (CFun (C1, S Minus, C2)) =
15.74 curried_strip_ctype C2 |>> append (prodC_factors C1)
15.75 | curried_strip_ctype C = ([], C)
15.76 (* string -> ctype -> ctype *)
15.77 fun sel_ctype_from_constr_ctype s C =
15.78 let val (arg_Cs, dataC) = curried_strip_ctype C in
15.79 - CFun (dataC, S Neg,
15.80 + CFun (dataC, S Minus,
15.81 case sel_no_from_name s of ~1 => bool_C | n => nth arg_Cs n)
15.82 end
15.83
15.84 @@ -268,8 +269,13 @@
15.85 if could_exist_alpha_sub_ctype thy alpha_T T then
15.86 case AList.lookup (op =) (!constr_cache) x of
15.87 SOME C => C
15.88 - | NONE => (fresh_ctype_for_type cdata (body_type T);
15.89 - AList.lookup (op =) (!constr_cache) x |> the)
15.90 + | NONE => if T = alpha_T then
15.91 + let val C = fresh_ctype_for_type cdata T in
15.92 + (Unsynchronized.change constr_cache (cons (x, C)); C)
15.93 + end
15.94 + else
15.95 + (fresh_ctype_for_type cdata (body_type T);
15.96 + AList.lookup (op =) (!constr_cache) x |> the)
15.97 else
15.98 fresh_ctype_for_type cdata T
15.99 fun ctype_for_sel (cdata as {ext_ctxt, ...}) (x as (s, _)) =
15.100 @@ -332,9 +338,9 @@
15.101 | _ => do_sign_atom_comp Eq [] a2 a1 accum)
15.102 | do_sign_atom_comp Leq [] a1 a2 (accum as (lits, comps)) =
15.103 (case (a1, a2) of
15.104 - (_, S Neg) => SOME accum
15.105 - | (S Pos, _) => SOME accum
15.106 - | (S Neg, S Pos) => NONE
15.107 + (_, S Minus) => SOME accum
15.108 + | (S Plus, _) => SOME accum
15.109 + | (S Minus, S Plus) => NONE
15.110 | (V _, V _) => SOME (lits, insert (op =) (a1, a2, Leq, []) comps)
15.111 | _ => do_sign_atom_comp Eq [] a1 a2 accum)
15.112 | do_sign_atom_comp cmp xs a1 a2 (accum as (lits, comps)) =
15.113 @@ -354,8 +360,8 @@
15.114 accum |> do_sign_atom_comp Leq xs a1 a2
15.115 |> do_ctype_comp Leq xs C21 C11
15.116 |> (case a2 of
15.117 - S Neg => I
15.118 - | S Pos => do_ctype_comp Leq xs C11 C21
15.119 + S Minus => I
15.120 + | S Plus => do_ctype_comp Leq xs C11 C21
15.121 | V x => do_ctype_comp Leq (x :: xs) C11 C21)
15.122 else
15.123 SOME accum)
15.124 @@ -386,29 +392,33 @@
15.125 (* sign -> sign_expr -> ctype -> (literal list * sign_expr list) option
15.126 -> (literal list * sign_expr list) option *)
15.127 fun do_notin_ctype_fv _ _ _ NONE = NONE
15.128 - | do_notin_ctype_fv Neg _ CAlpha accum = accum
15.129 - | do_notin_ctype_fv Pos [] CAlpha _ = NONE
15.130 - | do_notin_ctype_fv Pos [(x, sn)] CAlpha (SOME (lits, sexps)) =
15.131 + | do_notin_ctype_fv Minus _ CAlpha accum = accum
15.132 + | do_notin_ctype_fv Plus [] CAlpha _ = NONE
15.133 + | do_notin_ctype_fv Plus [(x, sn)] CAlpha (SOME (lits, sexps)) =
15.134 SOME lits |> do_literal (x, sn) |> Option.map (rpair sexps)
15.135 - | do_notin_ctype_fv Pos sexp CAlpha (SOME (lits, sexps)) =
15.136 + | do_notin_ctype_fv Plus sexp CAlpha (SOME (lits, sexps)) =
15.137 SOME (lits, insert (op =) sexp sexps)
15.138 | do_notin_ctype_fv sn sexp (CFun (C1, S sn', C2)) accum =
15.139 - accum |> (if sn' = Pos andalso sn = Pos then do_notin_ctype_fv Pos sexp C1
15.140 - else I)
15.141 - |> (if sn' = Neg orelse sn = Pos then do_notin_ctype_fv Neg sexp C1
15.142 - else I)
15.143 + accum |> (if sn' = Plus andalso sn = Plus then
15.144 + do_notin_ctype_fv Plus sexp C1
15.145 + else
15.146 + I)
15.147 + |> (if sn' = Minus orelse sn = Plus then
15.148 + do_notin_ctype_fv Minus sexp C1
15.149 + else
15.150 + I)
15.151 |> do_notin_ctype_fv sn sexp C2
15.152 - | do_notin_ctype_fv Pos sexp (CFun (C1, V x, C2)) accum =
15.153 - accum |> (case do_literal (x, Neg) (SOME sexp) of
15.154 + | do_notin_ctype_fv Plus sexp (CFun (C1, V x, C2)) accum =
15.155 + accum |> (case do_literal (x, Minus) (SOME sexp) of
15.156 NONE => I
15.157 - | SOME sexp' => do_notin_ctype_fv Pos sexp' C1)
15.158 - |> do_notin_ctype_fv Neg sexp C1
15.159 - |> do_notin_ctype_fv Pos sexp C2
15.160 - | do_notin_ctype_fv Neg sexp (CFun (C1, V x, C2)) accum =
15.161 - accum |> (case do_literal (x, Pos) (SOME sexp) of
15.162 + | SOME sexp' => do_notin_ctype_fv Plus sexp' C1)
15.163 + |> do_notin_ctype_fv Minus sexp C1
15.164 + |> do_notin_ctype_fv Plus sexp C2
15.165 + | do_notin_ctype_fv Minus sexp (CFun (C1, V x, C2)) accum =
15.166 + accum |> (case do_literal (x, Plus) (SOME sexp) of
15.167 NONE => I
15.168 - | SOME sexp' => do_notin_ctype_fv Pos sexp' C1)
15.169 - |> do_notin_ctype_fv Neg sexp C2
15.170 + | SOME sexp' => do_notin_ctype_fv Plus sexp' C1)
15.171 + |> do_notin_ctype_fv Minus sexp C2
15.172 | do_notin_ctype_fv sn sexp (CPair (C1, C2)) accum =
15.173 accum |> fold (do_notin_ctype_fv sn sexp) [C1, C2]
15.174 | do_notin_ctype_fv sn sexp (CType (_, Cs)) accum =
15.175 @@ -420,14 +430,14 @@
15.176 fun add_notin_ctype_fv _ _ UnsolvableCSet = UnsolvableCSet
15.177 | add_notin_ctype_fv sn C (CSet (lits, comps, sexps)) =
15.178 (print_g ("*** Add " ^ string_for_ctype C ^ " is right-" ^
15.179 - (case sn of Neg => "unique" | Pos => "total") ^ ".");
15.180 + (case sn of Minus => "unique" | Plus => "total") ^ ".");
15.181 case do_notin_ctype_fv sn [] C (SOME (lits, sexps)) of
15.182 NONE => (print_g "**** Unsolvable"; UnsolvableCSet)
15.183 | SOME (lits, sexps) => CSet (lits, comps, sexps))
15.184
15.185 (* ctype -> constraint_set -> constraint_set *)
15.186 -val add_ctype_is_right_unique = add_notin_ctype_fv Neg
15.187 -val add_ctype_is_right_total = add_notin_ctype_fv Pos
15.188 +val add_ctype_is_right_unique = add_notin_ctype_fv Minus
15.189 +val add_ctype_is_right_total = add_notin_ctype_fv Plus
15.190
15.191 (* constraint_set -> constraint_set -> constraint_set *)
15.192 fun unite (CSet (lits1, comps1, sexps1)) (CSet (lits2, comps2, sexps2)) =
15.193 @@ -437,11 +447,11 @@
15.194 | unite _ _ = UnsolvableCSet
15.195
15.196 (* sign -> bool *)
15.197 -fun bool_from_sign Pos = false
15.198 - | bool_from_sign Neg = true
15.199 +fun bool_from_sign Plus = false
15.200 + | bool_from_sign Minus = true
15.201 (* bool -> sign *)
15.202 -fun sign_from_bool false = Pos
15.203 - | sign_from_bool true = Neg
15.204 +fun sign_from_bool false = Plus
15.205 + | sign_from_bool true = Minus
15.206
15.207 (* literal -> PropLogic.prop_formula *)
15.208 fun prop_for_literal (x, sn) =
15.209 @@ -460,10 +470,10 @@
15.210 PropLogic.SAnd (prop_for_comp (a1, a2, Leq, []),
15.211 prop_for_comp (a2, a1, Leq, []))
15.212 | prop_for_comp (a1, a2, Leq, []) =
15.213 - PropLogic.SOr (prop_for_sign_atom_eq (a1, Pos),
15.214 - prop_for_sign_atom_eq (a2, Neg))
15.215 + PropLogic.SOr (prop_for_sign_atom_eq (a1, Plus),
15.216 + prop_for_sign_atom_eq (a2, Minus))
15.217 | prop_for_comp (a1, a2, cmp, xs) =
15.218 - PropLogic.SOr (prop_for_exists_eq xs Neg, prop_for_comp (a1, a2, cmp, []))
15.219 + PropLogic.SOr (prop_for_exists_eq xs Minus, prop_for_comp (a1, a2, cmp, []))
15.220
15.221 (* var -> (int -> bool option) -> literal list -> literal list *)
15.222 fun literals_from_assignments max_var assigns lits =
15.223 @@ -491,7 +501,7 @@
15.224
15.225 (* literal list -> unit *)
15.226 fun print_solution lits =
15.227 - let val (pos, neg) = List.partition (curry (op =) Pos o snd) lits in
15.228 + let val (pos, neg) = List.partition (curry (op =) Plus o snd) lits in
15.229 print_g ("*** Solution:\n" ^
15.230 "+: " ^ commas (map (string_for_var o fst) pos) ^ "\n" ^
15.231 "-: " ^ commas (map (string_for_var o fst) neg))
15.232 @@ -523,7 +533,7 @@
15.233 type ctype_context =
15.234 {bounds: ctype list,
15.235 frees: (styp * ctype) list,
15.236 - consts: (styp * ctype_schema) list}
15.237 + consts: (styp * ctype) list}
15.238
15.239 type accumulator = ctype_context * constraint_set
15.240
15.241 @@ -546,20 +556,20 @@
15.242 val ctype_for = fresh_ctype_for_type cdata
15.243 (* ctype -> ctype *)
15.244 fun pos_set_ctype_for_dom C =
15.245 - CFun (C, S (if exists_alpha_sub_ctype C then Pos else Neg), bool_C)
15.246 + CFun (C, S (if exists_alpha_sub_ctype C then Plus else Minus), bool_C)
15.247 (* typ -> accumulator -> ctype * accumulator *)
15.248 fun do_quantifier T (gamma, cset) =
15.249 let
15.250 val abs_C = ctype_for (domain_type (domain_type T))
15.251 val body_C = ctype_for (range_type T)
15.252 in
15.253 - (CFun (CFun (abs_C, S Neg, body_C), S Neg, body_C),
15.254 + (CFun (CFun (abs_C, S Minus, body_C), S Minus, body_C),
15.255 (gamma, cset |> add_ctype_is_right_total abs_C))
15.256 end
15.257 fun do_equals T (gamma, cset) =
15.258 let val C = ctype_for (domain_type T) in
15.259 - (CFun (C, S Neg, CFun (C, V (Unsynchronized.inc max_fresh),
15.260 - ctype_for (nth_range_type 2 T))),
15.261 + (CFun (C, S Minus, CFun (C, V (Unsynchronized.inc max_fresh),
15.262 + ctype_for (nth_range_type 2 T))),
15.263 (gamma, cset |> add_ctype_is_right_unique C))
15.264 end
15.265 fun do_robust_set_operation T (gamma, cset) =
15.266 @@ -569,7 +579,7 @@
15.267 val C2 = ctype_for set_T
15.268 val C3 = ctype_for set_T
15.269 in
15.270 - (CFun (C1, S Neg, CFun (C2, S Neg, C3)),
15.271 + (CFun (C1, S Minus, CFun (C2, S Minus, C3)),
15.272 (gamma, cset |> add_is_sub_ctype C1 C3 |> add_is_sub_ctype C2 C3))
15.273 end
15.274 fun do_fragile_set_operation T (gamma, cset) =
15.275 @@ -579,7 +589,7 @@
15.276 (* typ -> ctype *)
15.277 fun custom_ctype_for (T as Type ("fun", [T1, T2])) =
15.278 if T = set_T then set_C
15.279 - else CFun (custom_ctype_for T1, S Neg, custom_ctype_for T2)
15.280 + else CFun (custom_ctype_for T1, S Minus, custom_ctype_for T2)
15.281 | custom_ctype_for T = ctype_for T
15.282 in
15.283 (custom_ctype_for T, (gamma, cset |> add_ctype_is_right_unique set_C))
15.284 @@ -588,13 +598,13 @@
15.285 fun do_pair_constr T accum =
15.286 case ctype_for (nth_range_type 2 T) of
15.287 C as CPair (a_C, b_C) =>
15.288 - (CFun (a_C, S Neg, CFun (b_C, S Neg, C)), accum)
15.289 + (CFun (a_C, S Minus, CFun (b_C, S Minus, C)), accum)
15.290 | C => raise CTYPE ("Nitpick_Mono.consider_term.do_pair_constr", [C])
15.291 (* int -> typ -> accumulator -> ctype * accumulator *)
15.292 fun do_nth_pair_sel n T =
15.293 case ctype_for (domain_type T) of
15.294 C as CPair (a_C, b_C) =>
15.295 - pair (CFun (C, S Neg, if n = 0 then a_C else b_C))
15.296 + pair (CFun (C, S Minus, if n = 0 then a_C else b_C))
15.297 | C => raise CTYPE ("Nitpick_Mono.consider_term.do_nth_pair_sel", [C])
15.298 val unsolvable = (CType ("unsolvable", []), unsolvable_accum)
15.299 (* typ -> term -> accumulator -> ctype * accumulator *)
15.300 @@ -613,7 +623,7 @@
15.301 (case t of
15.302 Const (x as (s, T)) =>
15.303 (case AList.lookup (op =) consts x of
15.304 - SOME (C, cset') => (C, (gamma, cset |> unite cset'))
15.305 + SOME C => (C, accum)
15.306 | NONE =>
15.307 if not (could_exist_alpha_subtype alpha_T T) then
15.308 (ctype_for T, accum)
15.309 @@ -627,12 +637,12 @@
15.310 | @{const_name Eps} => (print_g "*** Eps"; unsolvable)
15.311 | @{const_name If} =>
15.312 do_robust_set_operation (range_type T) accum
15.313 - |>> curry3 CFun bool_C (S Neg)
15.314 + |>> curry3 CFun bool_C (S Minus)
15.315 | @{const_name Pair} => do_pair_constr T accum
15.316 | @{const_name fst} => do_nth_pair_sel 0 T accum
15.317 | @{const_name snd} => do_nth_pair_sel 1 T accum
15.318 | @{const_name Id} =>
15.319 - (CFun (ctype_for (domain_type T), S Neg, bool_C), accum)
15.320 + (CFun (ctype_for (domain_type T), S Minus, bool_C), accum)
15.321 | @{const_name insert} =>
15.322 let
15.323 val set_T = domain_type (range_type T)
15.324 @@ -641,7 +651,7 @@
15.325 val C2 = ctype_for set_T
15.326 val C3 = ctype_for set_T
15.327 in
15.328 - (CFun (C1, S Neg, CFun (C2, S Neg, C3)),
15.329 + (CFun (C1, S Minus, CFun (C2, S Minus, C3)),
15.330 (gamma, cset |> add_ctype_is_right_unique C1
15.331 |> add_is_sub_ctype C1' C3
15.332 |> add_is_sub_ctype C2 C3))
15.333 @@ -654,7 +664,7 @@
15.334 CFun (ctype_for (domain_type T), V x, bool_C)
15.335 val ab_set_C = domain_type T |> ctype_for_set
15.336 val ba_set_C = range_type T |> ctype_for_set
15.337 - in (CFun (ab_set_C, S Neg, ba_set_C), accum) end
15.338 + in (CFun (ab_set_C, S Minus, ba_set_C), accum) end
15.339 | @{const_name trancl} => do_fragile_set_operation T accum
15.340 | @{const_name rtrancl} => (print_g "*** rtrancl"; unsolvable)
15.341 | @{const_name lower_semilattice_fun_inst.inf_fun} =>
15.342 @@ -663,7 +673,7 @@
15.343 do_robust_set_operation T accum
15.344 | @{const_name finite} =>
15.345 let val C1 = ctype_for (domain_type (domain_type T)) in
15.346 - (CFun (pos_set_ctype_for_dom C1, S Neg, bool_C), accum)
15.347 + (CFun (pos_set_ctype_for_dom C1, S Minus, bool_C), accum)
15.348 end
15.349 | @{const_name rel_comp} =>
15.350 let
15.351 @@ -675,7 +685,7 @@
15.352 val ab_set_C = domain_type (range_type T) |> ctype_for_set
15.353 val ac_set_C = nth_range_type 2 T |> ctype_for_set
15.354 in
15.355 - (CFun (bc_set_C, S Neg, CFun (ab_set_C, S Neg, ac_set_C)),
15.356 + (CFun (bc_set_C, S Minus, CFun (ab_set_C, S Minus, ac_set_C)),
15.357 accum)
15.358 end
15.359 | @{const_name image} =>
15.360 @@ -683,8 +693,8 @@
15.361 val a_C = ctype_for (domain_type (domain_type T))
15.362 val b_C = ctype_for (range_type (domain_type T))
15.363 in
15.364 - (CFun (CFun (a_C, S Neg, b_C), S Neg,
15.365 - CFun (pos_set_ctype_for_dom a_C, S Neg,
15.366 + (CFun (CFun (a_C, S Minus, b_C), S Minus,
15.367 + CFun (pos_set_ctype_for_dom a_C, S Minus,
15.368 pos_set_ctype_for_dom b_C)), accum)
15.369 end
15.370 | @{const_name Sigma} =>
15.371 @@ -698,11 +708,11 @@
15.372 val b_set_C = ctype_for_set (range_type (domain_type
15.373 (range_type T)))
15.374 val a_set_C = ctype_for_set a_set_T
15.375 - val a_to_b_set_C = CFun (a_C, S Neg, b_set_C)
15.376 + val a_to_b_set_C = CFun (a_C, S Minus, b_set_C)
15.377 val ab_set_C = ctype_for_set (nth_range_type 2 T)
15.378 in
15.379 - (CFun (a_set_C, S Neg, CFun (a_to_b_set_C, S Neg, ab_set_C)),
15.380 - accum)
15.381 + (CFun (a_set_C, S Minus,
15.382 + CFun (a_to_b_set_C, S Minus, ab_set_C)), accum)
15.383 end
15.384 | @{const_name minus_fun_inst.minus_fun} =>
15.385 let
15.386 @@ -710,8 +720,8 @@
15.387 val left_set_C = ctype_for set_T
15.388 val right_set_C = ctype_for set_T
15.389 in
15.390 - (CFun (left_set_C, S Neg,
15.391 - CFun (right_set_C, S Neg, left_set_C)),
15.392 + (CFun (left_set_C, S Minus,
15.393 + CFun (right_set_C, S Minus, left_set_C)),
15.394 (gamma, cset |> add_ctype_is_right_unique right_set_C
15.395 |> add_is_sub_ctype right_set_C left_set_C))
15.396 end
15.397 @@ -721,15 +731,15 @@
15.398 let
15.399 val a_C = ctype_for (domain_type (domain_type T))
15.400 val a_set_C = pos_set_ctype_for_dom a_C
15.401 - in (CFun (a_set_C, S Neg, a_C), accum) end
15.402 + in (CFun (a_set_C, S Minus, a_C), accum) end
15.403 | @{const_name FunBox} =>
15.404 let val dom_C = ctype_for (domain_type T) in
15.405 - (CFun (dom_C, S Neg, dom_C), accum)
15.406 + (CFun (dom_C, S Minus, dom_C), accum)
15.407 end
15.408 | _ => if is_sel s then
15.409 if constr_name_for_sel_like s = @{const_name FunBox} then
15.410 let val dom_C = ctype_for (domain_type T) in
15.411 - (CFun (dom_C, S Neg, dom_C), accum)
15.412 + (CFun (dom_C, S Minus, dom_C), accum)
15.413 end
15.414 else
15.415 (ctype_for_sel cdata x, accum)
15.416 @@ -740,7 +750,10 @@
15.417 SOME t' => do_term t' accum
15.418 | NONE => (print_g ("*** built-in " ^ s); unsolvable)
15.419 else
15.420 - (ctype_for T, accum))
15.421 + let val C = ctype_for T in
15.422 + (C, ({bounds = bounds, frees = frees,
15.423 + consts = (x, C) :: consts}, cset))
15.424 + end)
15.425 | Free (x as (_, T)) =>
15.426 (case AList.lookup (op =) frees x of
15.427 SOME C => (C, accum)
15.428 @@ -756,7 +769,7 @@
15.429 let
15.430 val C = ctype_for T
15.431 val (C', accum) = do_term t' (accum |>> push_bound C)
15.432 - in (CFun (C, S Neg, C'), accum |>> pop_bound) end
15.433 + in (CFun (C, S Minus, C'), accum |>> pop_bound) end
15.434 | Const (@{const_name All}, _)
15.435 $ Abs (_, T', @{const "op -->"} $ (t1 $ Bound 0) $ t2) =>
15.436 do_bounded_quantifier T' t1 t2 accum
15.437 @@ -802,7 +815,7 @@
15.438 fun do_quantifier quant_s abs_T body_t =
15.439 let
15.440 val abs_C = ctype_for abs_T
15.441 - val side_cond = ((sn = Neg) = (quant_s = @{const_name Ex}))
15.442 + val side_cond = ((sn = Minus) = (quant_s = @{const_name Ex}))
15.443 val cset = cset |> side_cond ? add_ctype_is_right_total abs_C
15.444 in
15.445 (gamma |> push_bound abs_C, cset) |> do_co_formula body_t
15.446 @@ -815,11 +828,11 @@
15.447 (* term -> term -> accumulator *)
15.448 fun do_equals t1 t2 =
15.449 case sn of
15.450 - Pos => do_term t accum |> snd
15.451 - | Neg => let
15.452 - val (C1, accum) = do_term t1 accum
15.453 - val (C2, accum) = do_term t2 accum
15.454 - in accum ||> add_ctypes_equal C1 C2 end
15.455 + Plus => do_term t accum |> snd
15.456 + | Minus => let
15.457 + val (C1, accum) = do_term t1 accum
15.458 + val (C2, accum) = do_term t2 accum
15.459 + in accum ||> add_ctypes_equal C1 C2 end
15.460 in
15.461 case t of
15.462 Const (s0 as @{const_name all}, _) $ Abs (_, T1, t1) =>
15.463 @@ -876,7 +889,7 @@
15.464 (* cdata -> term -> accumulator -> accumulator *)
15.465 fun consider_definitional_axiom (cdata as {ext_ctxt as {thy, ...}, ...}) t =
15.466 if not (is_constr_pattern_formula thy t) then
15.467 - consider_nondefinitional_axiom cdata Pos t
15.468 + consider_nondefinitional_axiom cdata Plus t
15.469 else if is_harmless_axiom t then
15.470 I
15.471 else
15.472 @@ -921,11 +934,11 @@
15.473 (* theory -> literal list -> ctype_context -> unit *)
15.474 fun print_ctype_context ctxt lits ({frees, consts, ...} : ctype_context) =
15.475 map (fn (x, C) => string_for_ctype_of_term ctxt lits (Free x) C) frees @
15.476 - map (fn (x, (C, _)) => string_for_ctype_of_term ctxt lits (Const x) C) consts
15.477 + map (fn (x, C) => string_for_ctype_of_term ctxt lits (Const x) C) consts
15.478 |> cat_lines |> print_g
15.479
15.480 -(* extended_context -> typ -> term list -> term list -> term -> bool *)
15.481 -fun formulas_monotonic (ext_ctxt as {ctxt, ...}) alpha_T def_ts nondef_ts
15.482 +(* extended_context -> typ -> sign -> term list -> term list -> term -> bool *)
15.483 +fun formulas_monotonic (ext_ctxt as {ctxt, ...}) alpha_T sn def_ts nondef_ts
15.484 core_t =
15.485 let
15.486 val _ = print_g ("****** " ^ string_for_ctype CAlpha ^ " is " ^
15.487 @@ -934,8 +947,8 @@
15.488 val (gamma, cset) =
15.489 (initial_gamma, slack)
15.490 |> fold (consider_definitional_axiom cdata) def_ts
15.491 - |> fold (consider_nondefinitional_axiom cdata Pos) nondef_ts
15.492 - |> consider_general_formula cdata Pos core_t
15.493 + |> fold (consider_nondefinitional_axiom cdata Plus) nondef_ts
15.494 + |> consider_general_formula cdata sn core_t
15.495 in
15.496 case solve (!max_fresh) cset of
15.497 SOME lits => (print_ctype_context ctxt lits gamma; true)
16.1 --- a/src/HOL/Tools/Nitpick/nitpick_nut.ML Mon Feb 01 14:12:12 2010 +0100
16.2 +++ b/src/HOL/Tools/Nitpick/nitpick_nut.ML Tue Feb 02 11:38:38 2010 +0100
16.3 @@ -1,6 +1,6 @@
16.4 (* Title: HOL/Tools/Nitpick/nitpick_nut.ML
16.5 Author: Jasmin Blanchette, TU Muenchen
16.6 - Copyright 2008, 2009
16.7 + Copyright 2008, 2009, 2010
16.8
16.9 Nitpick underlying terms (nuts).
16.10 *)
16.11 @@ -766,7 +766,7 @@
16.12 (~1 upto num_sels_for_constr_type T - 1)
16.13 (* scope -> dtype_spec -> nut list * rep NameTable.table
16.14 -> nut list * rep NameTable.table *)
16.15 -fun choose_rep_for_sels_of_datatype _ ({shallow = true, ...} : dtype_spec) = I
16.16 +fun choose_rep_for_sels_of_datatype _ ({deep = false, ...} : dtype_spec) = I
16.17 | choose_rep_for_sels_of_datatype scope {constrs, ...} =
16.18 fold_rev (choose_rep_for_sels_for_constr scope o #const) constrs
16.19 (* scope -> rep NameTable.table -> nut list * rep NameTable.table *)
17.1 --- a/src/HOL/Tools/Nitpick/nitpick_peephole.ML Mon Feb 01 14:12:12 2010 +0100
17.2 +++ b/src/HOL/Tools/Nitpick/nitpick_peephole.ML Tue Feb 02 11:38:38 2010 +0100
17.3 @@ -1,6 +1,6 @@
17.4 (* Title: HOL/Tools/Nitpick/nitpick_peephole.ML
17.5 Author: Jasmin Blanchette, TU Muenchen
17.6 - Copyright 2008, 2009
17.7 + Copyright 2008, 2009, 2010
17.8
17.9 Peephole optimizer for Nitpick.
17.10 *)
18.1 --- a/src/HOL/Tools/Nitpick/nitpick_rep.ML Mon Feb 01 14:12:12 2010 +0100
18.2 +++ b/src/HOL/Tools/Nitpick/nitpick_rep.ML Tue Feb 02 11:38:38 2010 +0100
18.3 @@ -1,6 +1,6 @@
18.4 (* Title: HOL/Tools/Nitpick/nitpick_rep.ML
18.5 Author: Jasmin Blanchette, TU Muenchen
18.6 - Copyright 2008, 2009
18.7 + Copyright 2008, 2009, 2010
18.8
18.9 Kodkod representations of Nitpick terms.
18.10 *)
19.1 --- a/src/HOL/Tools/Nitpick/nitpick_scope.ML Mon Feb 01 14:12:12 2010 +0100
19.2 +++ b/src/HOL/Tools/Nitpick/nitpick_scope.ML Tue Feb 02 11:38:38 2010 +0100
19.3 @@ -1,6 +1,6 @@
19.4 (* Title: HOL/Tools/Nitpick/nitpick_scope.ML
19.5 Author: Jasmin Blanchette, TU Muenchen
19.6 - Copyright 2008, 2009
19.7 + Copyright 2008, 2009, 2010
19.8
19.9 Scope enumerator for Nitpick.
19.10 *)
19.11 @@ -24,7 +24,7 @@
19.12 co: bool,
19.13 complete: bool,
19.14 concrete: bool,
19.15 - shallow: bool,
19.16 + deep: bool,
19.17 constrs: constr_spec list}
19.18
19.19 type scope = {
19.20 @@ -73,7 +73,7 @@
19.21 co: bool,
19.22 complete: bool,
19.23 concrete: bool,
19.24 - shallow: bool,
19.25 + deep: bool,
19.26 constrs: constr_spec list}
19.27
19.28 type scope = {
19.29 @@ -134,7 +134,7 @@
19.30 fun quintuple_for_scope quote ({ext_ctxt as {thy, ctxt, ...}, card_assigns,
19.31 bits, bisim_depth, datatypes, ...} : scope) =
19.32 let
19.33 - val boring_Ts = [@{typ unsigned_bit}, @{typ signed_bit},
19.34 + val boring_Ts = [@{typ unsigned_bit}, @{typ signed_bit}, @{typ \<xi>},
19.35 @{typ bisim_iterator}]
19.36 val (iter_assigns, card_assigns) =
19.37 card_assigns |> filter_out (member (op =) boring_Ts o fst)
19.38 @@ -429,9 +429,10 @@
19.39 else if not co andalso num_self_recs > 0 then
19.40 if not self_rec andalso num_non_self_recs = 1 andalso
19.41 domain_card 2 card_assigns T = 1 then
19.42 - {delta = 0, epsilon = 1, exclusive = (s = @{const_name Nil}),
19.43 + {delta = 0, epsilon = 1,
19.44 + exclusive = (s = @{const_name Nil} andalso length constrs = 2),
19.45 total = true}
19.46 - else if s = @{const_name Cons} then
19.47 + else if s = @{const_name Cons} andalso length constrs = 2 then
19.48 {delta = 1, epsilon = card, exclusive = true, total = false}
19.49 else
19.50 {delta = 0, epsilon = card, exclusive = false, total = false}
19.51 @@ -455,10 +456,10 @@
19.52 end
19.53
19.54 (* extended_context -> typ list -> scope_desc -> typ * int -> dtype_spec *)
19.55 -fun datatype_spec_from_scope_descriptor (ext_ctxt as {thy, ...}) shallow_dataTs
19.56 +fun datatype_spec_from_scope_descriptor (ext_ctxt as {thy, ...}) deep_dataTs
19.57 (desc as (card_assigns, _)) (T, card) =
19.58 let
19.59 - val shallow = member (op =) shallow_dataTs T
19.60 + val deep = member (op =) deep_dataTs T
19.61 val co = is_codatatype thy T
19.62 val xs = boxed_datatype_constrs ext_ctxt T
19.63 val self_recs = map (is_self_recursive_constr_type o snd) xs
19.64 @@ -475,7 +476,7 @@
19.65 num_non_self_recs) (self_recs ~~ xs) []
19.66 in
19.67 {typ = T, card = card, co = co, complete = complete, concrete = concrete,
19.68 - shallow = shallow, constrs = constrs}
19.69 + deep = deep, constrs = constrs}
19.70 end
19.71
19.72 (* int -> int *)
19.73 @@ -487,11 +488,11 @@
19.74 (map snd card_assigns @ map snd max_assigns) 0)
19.75
19.76 (* extended_context -> int -> typ list -> scope_desc -> scope *)
19.77 -fun scope_from_descriptor (ext_ctxt as {thy, ...}) sym_break shallow_dataTs
19.78 +fun scope_from_descriptor (ext_ctxt as {thy, ...}) sym_break deep_dataTs
19.79 (desc as (card_assigns, _)) =
19.80 let
19.81 val datatypes =
19.82 - map (datatype_spec_from_scope_descriptor ext_ctxt shallow_dataTs desc)
19.83 + map (datatype_spec_from_scope_descriptor ext_ctxt deep_dataTs desc)
19.84 (filter (is_datatype thy o fst) card_assigns)
19.85 val bits = card_of_type card_assigns @{typ signed_bit} - 1
19.86 handle TYPE ("Nitpick_HOL.card_of_type", _, _) =>
19.87 @@ -524,8 +525,7 @@
19.88 -> (styp option * int list) list -> (styp option * int list) list -> int list
19.89 -> typ list -> typ list -> typ list -> int * scope list *)
19.90 fun all_scopes (ext_ctxt as {thy, ...}) sym_break cards_assigns maxes_assigns
19.91 - iters_assigns bitss bisim_depths mono_Ts nonmono_Ts
19.92 - shallow_dataTs =
19.93 + iters_assigns bitss bisim_depths mono_Ts nonmono_Ts deep_dataTs =
19.94 let
19.95 val cards_assigns = repair_cards_assigns_wrt_boxing thy mono_Ts
19.96 cards_assigns
19.97 @@ -540,7 +540,7 @@
19.98 in
19.99 (length all - length head,
19.100 descs |> length descs <= distinct_threshold ? distinct (op =)
19.101 - |> map (scope_from_descriptor ext_ctxt sym_break shallow_dataTs))
19.102 + |> map (scope_from_descriptor ext_ctxt sym_break deep_dataTs))
19.103 end
19.104
19.105 end;
20.1 --- a/src/HOL/Tools/Nitpick/nitpick_tests.ML Mon Feb 01 14:12:12 2010 +0100
20.2 +++ b/src/HOL/Tools/Nitpick/nitpick_tests.ML Tue Feb 02 11:38:38 2010 +0100
20.3 @@ -1,6 +1,6 @@
20.4 (* Title: HOL/Tools/Nitpick/nitpick_tests.ML
20.5 Author: Jasmin Blanchette, TU Muenchen
20.6 - Copyright 2008, 2009
20.7 + Copyright 2008, 2009, 2010
20.8
20.9 Unit tests for Nitpick.
20.10 *)
21.1 --- a/src/HOL/Tools/Nitpick/nitpick_util.ML Mon Feb 01 14:12:12 2010 +0100
21.2 +++ b/src/HOL/Tools/Nitpick/nitpick_util.ML Tue Feb 02 11:38:38 2010 +0100
21.3 @@ -1,6 +1,6 @@
21.4 (* Title: HOL/Tools/Nitpick/nitpick_util.ML
21.5 Author: Jasmin Blanchette, TU Muenchen
21.6 - Copyright 2008, 2009
21.7 + Copyright 2008, 2009, 2010
21.8
21.9 General-purpose functions used by the Nitpick modules.
21.10 *)
21.11 @@ -58,7 +58,7 @@
21.12 val setmp_show_all_types : ('a -> 'b) -> 'a -> 'b
21.13 val indent_size : int
21.14 val pstrs : string -> Pretty.T list
21.15 - val plain_string_from_yxml : string -> string
21.16 + val unyxml : string -> string
21.17 val maybe_quote : string -> string
21.18 end
21.19
21.20 @@ -278,13 +278,13 @@
21.21 fun plain_string_from_xml_tree t =
21.22 Buffer.empty |> XML.add_content t |> Buffer.content
21.23 (* string -> string *)
21.24 -val plain_string_from_yxml = plain_string_from_xml_tree o YXML.parse
21.25 +val unyxml = plain_string_from_xml_tree o YXML.parse
21.26
21.27 (* string -> bool *)
21.28 val is_long_identifier = forall Syntax.is_identifier o space_explode "."
21.29 (* string -> string *)
21.30 fun maybe_quote y =
21.31 - let val s = plain_string_from_yxml y in
21.32 + let val s = unyxml y in
21.33 y |> (not (is_long_identifier (perhaps (try (unprefix "'")) s)) orelse
21.34 OuterKeyword.is_keyword s) ? quote
21.35 end
22.1 --- a/src/Pure/Isar/proof_context.ML Mon Feb 01 14:12:12 2010 +0100
22.2 +++ b/src/Pure/Isar/proof_context.ML Tue Feb 02 11:38:38 2010 +0100
22.3 @@ -33,6 +33,7 @@
22.4 val set_syntax_mode: Syntax.mode -> Proof.context -> Proof.context
22.5 val restore_syntax_mode: Proof.context -> Proof.context -> Proof.context
22.6 val facts_of: Proof.context -> Facts.T
22.7 + val cases_of: Proof.context -> (string * (Rule_Cases.T * bool)) list
22.8 val transfer_syntax: theory -> Proof.context -> Proof.context
22.9 val transfer: theory -> Proof.context -> Proof.context
22.10 val theory: (theory -> theory) -> Proof.context -> Proof.context