added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
authorblanchet
Tue Feb 02 11:38:38 2010 +0100 (2010-02-02)
changeset 349827b8c366e34a2
parent 34981 475aef44d5fb
child 34983 e5cb3a016094
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
doc-src/Nitpick/nitpick.tex
src/HOL/Divides.thy
src/HOL/Nitpick.thy
src/HOL/Nitpick_Examples/Manual_Nits.thy
src/HOL/Nitpick_Examples/Mono_Nits.thy
src/HOL/Tools/Nitpick/HISTORY
src/HOL/Tools/Nitpick/kodkod.ML
src/HOL/Tools/Nitpick/kodkod_sat.ML
src/HOL/Tools/Nitpick/minipick.ML
src/HOL/Tools/Nitpick/nitpick.ML
src/HOL/Tools/Nitpick/nitpick_hol.ML
src/HOL/Tools/Nitpick/nitpick_isar.ML
src/HOL/Tools/Nitpick/nitpick_kodkod.ML
src/HOL/Tools/Nitpick/nitpick_model.ML
src/HOL/Tools/Nitpick/nitpick_mono.ML
src/HOL/Tools/Nitpick/nitpick_nut.ML
src/HOL/Tools/Nitpick/nitpick_peephole.ML
src/HOL/Tools/Nitpick/nitpick_rep.ML
src/HOL/Tools/Nitpick/nitpick_scope.ML
src/HOL/Tools/Nitpick/nitpick_tests.ML
src/HOL/Tools/Nitpick/nitpick_util.ML
src/Pure/Isar/proof_context.ML
     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