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

     2.1 --- a/src/HOL/Main.thy	Mon Feb 22 14:36:10 2010 +0100
     2.2 +++ b/src/HOL/Main.thy	Mon Feb 22 19:31:00 2010 +0100
     2.3 @@ -1,7 +1,7 @@
     2.4  header {* Main HOL *}
     2.5  
     2.6  theory Main
     2.7 -imports Plain Predicate_Compile Nitpick Quotient
     2.8 +imports Plain Predicate_Compile Nitpick
     2.9  begin
    2.10  
    2.11  text {*

     3.1 --- a/src/HOL/Nitpick.thy	Mon Feb 22 14:36:10 2010 +0100
     3.2 +++ b/src/HOL/Nitpick.thy	Mon Feb 22 19:31:00 2010 +0100
     3.3 @@ -8,7 +8,7 @@
     3.4  header {* Nitpick: Yet Another Counterexample Generator for Isabelle/HOL *}
     3.5  
     3.6  theory Nitpick
     3.7 -imports Map SAT
     3.8 +imports Map Quotient SAT
     3.9  uses ("Tools/Nitpick/kodkod.ML")
    3.10       ("Tools/Nitpick/kodkod_sat.ML")
    3.11       ("Tools/Nitpick/nitpick_util.ML")

     4.1 --- a/src/HOL/Nitpick_Examples/Core_Nits.thy	Mon Feb 22 14:36:10 2010 +0100
     4.2 +++ b/src/HOL/Nitpick_Examples/Core_Nits.thy	Mon Feb 22 19:31:00 2010 +0100
     4.3 @@ -11,82 +11,67 @@
     4.4  imports Main
     4.5  begin
     4.6  
     4.7 -nitpick_params [sat_solver = MiniSat_JNI, max_threads = 1, timeout = 60 s]
     4.8 +nitpick_params [max_potential = 0, sat_solver = MiniSat_JNI, max_threads = 1,
     4.9 +                timeout = 60 s]
    4.10  
    4.11  subsection {* Curry in a Hurry *}
    4.12  
    4.13  lemma "(\<lambda>f x y. (curry o split) f x y) = (\<lambda>f x y. (\<lambda>x. x) f x y)"
    4.14 -nitpick [card = 1\<midarrow>4, expect = none]
    4.15 -nitpick [card = 100, expect = none, timeout = none]
    4.16 +nitpick [card = 1\<midarrow>12, expect = none]
    4.17  by auto
    4.18  
    4.19  lemma "(\<lambda>f p. (split o curry) f p) = (\<lambda>f p. (\<lambda>x. x) f p)"
    4.20 -nitpick [card = 2]
    4.21 -nitpick [card = 1\<midarrow>4, expect = none]
    4.22 -nitpick [card = 10, expect = none]
    4.23 +nitpick [card = 1\<midarrow>12, expect = none]
    4.24  by auto
    4.25  
    4.26  lemma "split (curry f) = f"
    4.27 -nitpick [card = 1\<midarrow>4, expect = none]
    4.28 -nitpick [card = 10, expect = none]
    4.29 -nitpick [card = 40, expect = none]
    4.30 +nitpick [card = 1\<midarrow>12, expect = none]
    4.31  by auto
    4.32  
    4.33  lemma "curry (split f) = f"
    4.34 -nitpick [card = 1\<midarrow>4, expect = none]
    4.35 -nitpick [card = 40, expect = none]
    4.36 +nitpick [card = 1\<midarrow>12, expect = none]
    4.37  by auto
    4.38  
    4.39  lemma "(split o curry) f = f"
    4.40 -nitpick [card = 1\<midarrow>4, expect = none]
    4.41 -nitpick [card = 40, expect = none]
    4.42 +nitpick [card = 1\<midarrow>12, expect = none]
    4.43  by auto
    4.44  
    4.45  lemma "(curry o split) f = f"
    4.46 -nitpick [card = 1\<midarrow>4, expect = none]
    4.47 -nitpick [card = 1000, expect = none]
    4.48 +nitpick [card = 1\<midarrow>12, expect = none]
    4.49  by auto
    4.50  
    4.51  lemma "(split o curry) f = (\<lambda>x. x) f"
    4.52 -nitpick [card = 1\<midarrow>4, expect = none]
    4.53 -nitpick [card = 40, expect = none]
    4.54 +nitpick [card = 1\<midarrow>12, expect = none]
    4.55  by auto
    4.56  
    4.57  lemma "(curry o split) f = (\<lambda>x. x) f"
    4.58 -nitpick [card = 1\<midarrow>4, expect = none]
    4.59 -nitpick [card = 40, expect = none]
    4.60 +nitpick [card = 1\<midarrow>12, expect = none]
    4.61  by auto
    4.62  
    4.63  lemma "((split o curry) f) p = ((\<lambda>x. x) f) p"
    4.64 -nitpick [card = 1\<midarrow>4, expect = none]
    4.65 -nitpick [card = 40, expect = none]
    4.66 +nitpick [card = 1\<midarrow>12, expect = none]
    4.67  by auto
    4.68  
    4.69  lemma "((curry o split) f) x = ((\<lambda>x. x) f) x"
    4.70 -nitpick [card = 1\<midarrow>4, expect = none]
    4.71 -nitpick [card = 1000, expect = none]
    4.72 +nitpick [card = 1\<midarrow>12, expect = none]
    4.73  by auto
    4.74  
    4.75  lemma "((curry o split) f) x y = ((\<lambda>x. x) f) x y"
    4.76 -nitpick [card = 1\<midarrow>4, expect = none]
    4.77 -nitpick [card = 1000, expect = none]
    4.78 +nitpick [card = 1\<midarrow>12, expect = none]
    4.79  by auto
    4.80  
    4.81  lemma "split o curry = (\<lambda>x. x)"
    4.82 -nitpick [card = 1\<midarrow>4, expect = none]
    4.83 -nitpick [card = 40, expect = none]
    4.84 +nitpick [card = 1\<midarrow>12, expect = none]
    4.85  apply (rule ext)+
    4.86  by auto
    4.87  
    4.88  lemma "curry o split = (\<lambda>x. x)"
    4.89 -nitpick [card = 1\<midarrow>4, expect = none]
    4.90 -nitpick [card = 100, expect = none]
    4.91 +nitpick [card = 1\<midarrow>12, expect = none]
    4.92  apply (rule ext)+
    4.93  by auto
    4.94  
    4.95  lemma "split (\<lambda>x y. f (x, y)) = f"
    4.96 -nitpick [card = 1\<midarrow>4, expect = none]
    4.97 -nitpick [card = 40, expect = none]
    4.98 +nitpick [card = 1\<midarrow>12, expect = none]
    4.99  by auto
   4.100  
   4.101  subsection {* Representations *}
   4.102 @@ -96,13 +81,12 @@
   4.103  by auto
   4.104  
   4.105  lemma "(\<exists>g. \<forall>x. g (f x) = x) \<longrightarrow> (\<forall>y. \<exists>x. y = f x)"
   4.106 -nitpick [card 'a = 35, card 'b = 34, expect = genuine]
   4.107 -nitpick [card = 1\<midarrow>15, mono, expect = none]
   4.108 +nitpick [card 'a = 25, card 'b = 24, expect = genuine]
   4.109 +nitpick [card = 1\<midarrow>10, mono, expect = none]
   4.110  oops
   4.111  
   4.112  lemma "\<exists>f. f = (\<lambda>x. x) \<and> f y \<noteq> y"
   4.113  nitpick [card = 1, expect = genuine]
   4.114 -nitpick [card = 2, expect = genuine]
   4.115  nitpick [card = 5, expect = genuine]
   4.116  oops
   4.117  
   4.118 @@ -112,8 +96,7 @@
   4.119  oops
   4.120  
   4.121  lemma "{(a\<Colon>'a\<times>'a, b\<Colon>'b)}^-1 = {(b, a)}"
   4.122 -nitpick [card = 1\<midarrow>6, expect = none]
   4.123 -nitpick [card = 20, expect = none]
   4.124 +nitpick [card = 1\<midarrow>12, expect = none]
   4.125  by auto
   4.126  
   4.127  lemma "fst (a, b) = a"
   4.128 @@ -121,7 +104,7 @@
   4.129  by auto
   4.130  
   4.131  lemma "\<exists>P. P = Id"
   4.132 -nitpick [card = 1\<midarrow>4, expect = none]
   4.133 +nitpick [card = 1\<midarrow>20, expect = none]
   4.134  by auto
   4.135  
   4.136  lemma "(a\<Colon>'a\<Rightarrow>'b, a) \<in> Id\<^sup>*"
   4.137 @@ -129,11 +112,11 @@
   4.138  by auto
   4.139  
   4.140  lemma "(a\<Colon>'a\<times>'a, a) \<in> Id\<^sup>* \<union> {(a, b)}\<^sup>*"
   4.141 -nitpick [card = 1\<midarrow>6, expect = none]
   4.142 +nitpick [card = 1\<midarrow>4, expect = none]
   4.143  by auto
   4.144  
   4.145  lemma "Id (a, a)"
   4.146 -nitpick [card = 1\<midarrow>100, expect = none]
   4.147 +nitpick [card = 1\<midarrow>50, expect = none]
   4.148  by (auto simp: Id_def Collect_def)
   4.149  
   4.150  lemma "Id ((a\<Colon>'a, b\<Colon>'a), (a, b))"
   4.151 @@ -151,7 +134,7 @@
   4.152  lemma "g = Let (A \<or> B)"
   4.153  nitpick [card = 1, expect = none]
   4.154  nitpick [card = 2, expect = genuine]
   4.155 -nitpick [card = 20, expect = genuine]
   4.156 +nitpick [card = 12, expect = genuine]
   4.157  oops
   4.158  
   4.159  lemma "(let a_or_b = A \<or> B in a_or_b \<or> \<not> a_or_b)"
   4.160 @@ -172,37 +155,30 @@
   4.161  
   4.162  lemma "(a\<Colon>'a\<times>'a, a\<Colon>'a\<times>'a) \<in> R"
   4.163  nitpick [card = 1, expect = genuine]
   4.164 -nitpick [card = 2, expect = genuine]
   4.165 -nitpick [card = 4, expect = genuine]
   4.166  nitpick [card = 20, expect = genuine]
   4.167 -nitpick [card = 10, dont_box, expect = genuine]
   4.168 +nitpick [card = 5, dont_box, expect = genuine]
   4.169  oops
   4.170  
   4.171  lemma "f (g\<Colon>'a\<Rightarrow>'a) = x"
   4.172  nitpick [card = 3, expect = genuine]
   4.173  nitpick [card = 3, dont_box, expect = genuine]
   4.174 -nitpick [card = 5, expect = genuine]
   4.175  nitpick [card = 10, expect = genuine]
   4.176  oops
   4.177  
   4.178  lemma "f (a, b) = x"
   4.179 -nitpick [card = 3, expect = genuine]
   4.180 -nitpick [card = 10, expect = genuine]
   4.181 -nitpick [card = 16, expect = genuine]
   4.182 -nitpick [card = 30, expect = genuine]
   4.183 +nitpick [card = 12, expect = genuine]
   4.184  oops
   4.185  
   4.186  lemma "f (a, a) = f (c, d)"
   4.187 -nitpick [card = 4, expect = genuine]
   4.188 -nitpick [card = 20, expect = genuine]
   4.189 +nitpick [card = 12, expect = genuine]
   4.190  oops
   4.191  
   4.192  lemma "(x\<Colon>'a) = (\<lambda>a. \<lambda>b. \<lambda>c. if c then a else b) x x True"
   4.193 -nitpick [card = 2, expect = none]
   4.194 +nitpick [card = 1\<midarrow>12, expect = none]
   4.195  by auto
   4.196  
   4.197  lemma "\<exists>F. F a b = G a b"
   4.198 -nitpick [card = 3, expect = none]
   4.199 +nitpick [card = 2, expect = none]
   4.200  by auto
   4.201  
   4.202  lemma "f = split"
   4.203 @@ -216,12 +192,10 @@
   4.204  
   4.205  lemma "(A, B) \<in> R \<or> (\<exists>C. (A, C) \<in> R \<and> (C, B) \<in> R) \<Longrightarrow> 
   4.206         A = B \<or> (A, B) \<in> R \<or> (\<exists>C. (A, C) \<in> R \<and> (C, B) \<in> R)"
   4.207 -nitpick [card = 1\<midarrow>50, expect = none]
   4.208 +nitpick [card = 1\<midarrow>25, expect = none]
   4.209  by auto
   4.210  
   4.211  lemma "f = (\<lambda>x\<Colon>'a\<times>'b. x)"
   4.212 -nitpick [card = 3, expect = genuine]
   4.213 -nitpick [card = 4, expect = genuine]
   4.214  nitpick [card = 8, expect = genuine]
   4.215  oops
   4.216  
   4.217 @@ -230,30 +204,26 @@
   4.218  lemma "x = y"
   4.219  nitpick [card 'a = 1, expect = none]
   4.220  nitpick [card 'a = 2, expect = genuine]
   4.221 -nitpick [card 'a = 100, expect = genuine]
   4.222 -nitpick [card 'a = 1000, expect = genuine]
   4.223 +nitpick [card 'a = 200, expect = genuine]
   4.224  oops
   4.225  
   4.226  lemma "\<forall>x. x = y"
   4.227  nitpick [card 'a = 1, expect = none]
   4.228  nitpick [card 'a = 2, expect = genuine]
   4.229 -nitpick [card 'a = 100, expect = genuine]
   4.230 -nitpick [card 'a = 1000, expect = genuine]
   4.231 +nitpick [card 'a = 200, expect = genuine]
   4.232  oops
   4.233  
   4.234  lemma "\<forall>x\<Colon>'a \<Rightarrow> bool. x = y"
   4.235  nitpick [card 'a = 1, expect = genuine]
   4.236 -nitpick [card 'a = 2, expect = genuine]
   4.237 -nitpick [card 'a = 100, expect = genuine]
   4.238 -nitpick [card 'a = 1000, expect = genuine]
   4.239 +nitpick [card 'a = 200, expect = genuine]
   4.240  oops
   4.241  
   4.242  lemma "\<exists>x\<Colon>'a \<Rightarrow> bool. x = y"
   4.243 -nitpick [card 'a = 1\<midarrow>10, expect = none]
   4.244 +nitpick [card 'a = 1\<midarrow>20, expect = none]
   4.245  by auto
   4.246  
   4.247  lemma "\<exists>x y\<Colon>'a \<Rightarrow> bool. x = y"
   4.248 -nitpick [card = 1\<midarrow>40, expect = none]
   4.249 +nitpick [card = 1\<midarrow>20, expect = none]
   4.250  by auto
   4.251  
   4.252  lemma "\<forall>x. \<exists>y. f x y = f x (g x)"
   4.253 @@ -261,11 +231,10 @@
   4.254  by auto
   4.255  
   4.256  lemma "\<forall>u. \<exists>v. \<forall>w. \<exists>x. f u v w x = f u (g u) w (h u w)"
   4.257 -nitpick [card = 1\<midarrow>5, expect = none]
   4.258 +nitpick [card = 1\<midarrow>4, expect = none]
   4.259  by auto
   4.260  
   4.261  lemma "\<forall>u. \<exists>v. \<forall>w. \<exists>x. f u v w x = f u (g u w) w (h u)"
   4.262 -nitpick [card = 1\<midarrow>2, expect = genuine]
   4.263  nitpick [card = 3, expect = genuine]
   4.264  oops
   4.265  
   4.266 @@ -273,7 +242,6 @@
   4.267         f u v w x y z = f u (g u) w (h u w) y (k u w y)"
   4.268  nitpick [card = 1\<midarrow>2, expect = none]
   4.269  nitpick [card = 3, expect = none]
   4.270 -nitpick [card = 4, expect = none]
   4.271  sorry
   4.272  
   4.273  lemma "\<forall>u. \<exists>v. \<forall>w. \<exists>x. \<forall>y. \<exists>z.
   4.274 @@ -334,9 +302,6 @@
   4.275  
   4.276  lemma "(\<exists>x\<Colon>'a. \<forall>y. P x y) \<or> (\<exists>x\<Colon>'a \<times> 'a. \<forall>y. P y x)"
   4.277  nitpick [card 'a = 1, expect = genuine]
   4.278 -nitpick [card 'a = 2, expect = genuine]
   4.279 -nitpick [card 'a = 3, expect = genuine]
   4.280 -nitpick [card 'a = 4, expect = genuine]
   4.281  nitpick [card 'a = 5, expect = genuine]
   4.282  oops
   4.283  
   4.284 @@ -390,8 +355,7 @@
   4.285  nitpick [card = 1, expect = genuine]
   4.286  nitpick [card = 1, box "('a \<Rightarrow> prop) \<Rightarrow> prop", expect = genuine]
   4.287  nitpick [card = 2, expect = genuine]
   4.288 -nitpick [card = 8, expect = genuine]
   4.289 -nitpick [card = 10, expect = unknown]
   4.290 +nitpick [card = 6, expect = genuine]
   4.291  oops
   4.292  
   4.293  lemma "\<And>x. f x y = f x y"
   4.294 @@ -416,11 +380,7 @@
   4.295  
   4.296  lemma "x \<equiv> (op \<equiv>) \<Longrightarrow> False"
   4.297  nitpick [card = 1, expect = genuine]
   4.298 -nitpick [card = 2, expect = genuine]
   4.299 -nitpick [card = 3, expect = genuine]
   4.300 -nitpick [card = 4, expect = genuine]
   4.301 -nitpick [card = 5, expect = genuine]
   4.302 -nitpick [card = 100, expect = genuine]
   4.303 +nitpick [card = 20, expect = genuine]
   4.304  oops
   4.305  
   4.306  lemma "I = (\<lambda>x. x) \<Longrightarrow> (op \<equiv> x) \<equiv> (\<lambda>y. (x \<equiv> I y))"
   4.307 @@ -529,7 +489,7 @@
   4.308  lemma "x = Ex \<Longrightarrow> False"
   4.309  nitpick [card = 1, dont_box, expect = genuine]
   4.310  nitpick [card = 2, dont_box, expect = genuine]
   4.311 -nitpick [card = 8, dont_box, expect = genuine]
   4.312 +nitpick [card = 6, dont_box, expect = genuine]
   4.313  nitpick [card = 10, dont_box, expect = unknown]
   4.314  oops
   4.315  
   4.316 @@ -582,8 +542,8 @@
   4.317  nitpick [expect = none]
   4.318  by auto
   4.319  
   4.320 -lemma "I = (\<lambda>x. x) \<Longrightarrow> (op &) = (\<lambda>x. op & (I x))"
   4.321 -      "I = (\<lambda>x. x) \<Longrightarrow> (op &) = (\<lambda>x y. x & (I y))"
   4.322 +lemma "I = (\<lambda>x. x) \<Longrightarrow> (op \<and>) = (\<lambda>x. op \<and> (I x))"
   4.323 +      "I = (\<lambda>x. x) \<Longrightarrow> (op \<and>) = (\<lambda>x y. x \<and> (I y))"
   4.324  nitpick [expect = none]
   4.325  by auto
   4.326  
   4.327 @@ -796,7 +756,7 @@
   4.328  by auto
   4.329  
   4.330  lemma "((x, x), (x, x)) \<in> rtrancl {}"
   4.331 -nitpick [expect = none]
   4.332 +nitpick [card = 1\<midarrow>5, expect = none]
   4.333  by auto
   4.334  
   4.335  lemma "I = (\<lambda>x. x) \<Longrightarrow> op \<union> = (\<lambda>x. op \<union> (I x))"
   4.336 @@ -931,9 +891,8 @@
   4.337  oops
   4.338  
   4.339  lemma "P x \<Longrightarrow> P (The P)"
   4.340 -nitpick [card = 1, expect = none]
   4.341  nitpick [card = 1\<midarrow>2, expect = none]
   4.342 -nitpick [card = 3\<midarrow>5, expect = genuine]
   4.343 +nitpick [card = 3, expect = genuine]
   4.344  nitpick [card = 8, expect = genuine]
   4.345  oops
   4.346  

     5.1 --- a/src/HOL/Nitpick_Examples/Datatype_Nits.thy	Mon Feb 22 14:36:10 2010 +0100
     5.2 +++ b/src/HOL/Nitpick_Examples/Datatype_Nits.thy	Mon Feb 22 19:31:00 2010 +0100
     5.3 @@ -11,7 +11,8 @@
     5.4  imports Main
     5.5  begin
     5.6  
     5.7 -nitpick_params [sat_solver = MiniSat_JNI, max_threads = 1, timeout = 60 s]
     5.8 +nitpick_params [max_potential = 0, sat_solver = MiniSat_JNI, max_threads = 1,
     5.9 +                timeout = 60 s]
    5.10  
    5.11  primrec rot where
    5.12  "rot Nibble0 = Nibble1" | "rot Nibble1 = Nibble2" | "rot Nibble2 = Nibble3" |
    5.13 @@ -27,9 +28,8 @@
    5.14  
    5.15  lemma "rot Nibble2 \<noteq> Nibble3"
    5.16  nitpick [card = 1, expect = none]
    5.17 -nitpick [card = 2, expect = genuine]
    5.18 +nitpick [card = 2, max Nibble4 = 0, expect = genuine]
    5.19  nitpick [card = 2, max Nibble2 = 0, expect = none]
    5.20 -nitpick [card = 2, max Nibble3 = 0, expect = none]
    5.21  oops
    5.22  
    5.23  lemma "(rot ^^ 15) n \<noteq> n"
    5.24 @@ -53,7 +53,7 @@
    5.25  "sn (Pd (_, b)) = b"
    5.26  
    5.27  lemma "fs (Pd p) = fst p"
    5.28 -nitpick [card = 20, expect = none]
    5.29 +nitpick [card = 12, expect = none]
    5.30  sorry
    5.31  
    5.32  lemma "fs (Pd p) = snd p"
    5.33 @@ -61,7 +61,7 @@
    5.34  oops
    5.35  
    5.36  lemma "sn (Pd p) = snd p"
    5.37 -nitpick [card = 20, expect = none]
    5.38 +nitpick [card = 12, expect = none]
    5.39  sorry
    5.40  
    5.41  lemma "sn (Pd p) = fst p"
    5.42 @@ -69,7 +69,7 @@
    5.43  oops
    5.44  
    5.45  lemma "fs (Pd ((a, b), (c, d))) = (a, b)"
    5.46 -nitpick [card = 1\<midarrow>12, expect = none]
    5.47 +nitpick [card = 1\<midarrow>10, expect = none]
    5.48  sorry
    5.49  
    5.50  lemma "fs (Pd ((a, b), (c, d))) = (c, d)"
    5.51 @@ -82,7 +82,7 @@
    5.52  "app (Fn f) x = f x"
    5.53  
    5.54  lemma "app (Fn g) y = g y"
    5.55 -nitpick [card = 1\<midarrow>12, expect = none]
    5.56 +nitpick [card = 1\<midarrow>10, expect = none]
    5.57  sorry
    5.58  
    5.59  lemma "app (Fn g) y = g' y"

     6.1 --- a/src/HOL/Nitpick_Examples/Hotel_Nits.thy	Mon Feb 22 14:36:10 2010 +0100
     6.2 +++ b/src/HOL/Nitpick_Examples/Hotel_Nits.thy	Mon Feb 22 19:31:00 2010 +0100
     6.3 @@ -12,7 +12,8 @@
     6.4  imports Main
     6.5  begin
     6.6  
     6.7 -nitpick_params [sat_solver = MiniSat_JNI, max_threads = 1, timeout = 120 s]
     6.8 +nitpick_params [max_potential = 0, sat_solver = MiniSat_JNI, max_threads = 1,
     6.9 +                timeout = 120 s]
    6.10  
    6.11  typedecl guest
    6.12  typedecl key

     7.1 --- a/src/HOL/Nitpick_Examples/Manual_Nits.thy	Mon Feb 22 14:36:10 2010 +0100
     7.2 +++ b/src/HOL/Nitpick_Examples/Manual_Nits.thy	Mon Feb 22 19:31:00 2010 +0100
     7.3 @@ -8,7 +8,7 @@
     7.4  header {* Examples from the Nitpick Manual *}
     7.5  
     7.6  theory Manual_Nits
     7.7 -imports Main Coinductive_List RealDef
     7.8 +imports Main Coinductive_List Quotient_Product RealDef
     7.9  begin
    7.10  
    7.11  chapter {* 3. First Steps *}
    7.12 @@ -102,6 +102,21 @@
    7.13  nitpick [show_datatypes]
    7.14  oops
    7.15  
    7.16 +fun my_int_rel where
    7.17 +"my_int_rel (x, y) (u, v) = (x + v = u + y)"
    7.18 +
    7.19 +quotient_type my_int = "nat \<times> nat" / my_int_rel
    7.20 +by (auto simp add: equivp_def expand_fun_eq)
    7.21 +
    7.22 +definition add_raw where
    7.23 +"add_raw \<equiv> \<lambda>(x, y) (u, v). (x + (u\<Colon>nat), y + (v\<Colon>nat))"
    7.24 +
    7.25 +quotient_definition "add\<Colon>my_int \<Rightarrow> my_int \<Rightarrow> my_int" is add_raw
    7.26 +
    7.27 +lemma "add x y = add x x"
    7.28 +nitpick [show_datatypes]
    7.29 +oops
    7.30 +
    7.31  record point =
    7.32    Xcoord :: int
    7.33    Ycoord :: int

     8.1 --- a/src/HOL/Nitpick_Examples/Mini_Nits.thy	Mon Feb 22 14:36:10 2010 +0100
     8.2 +++ b/src/HOL/Nitpick_Examples/Mini_Nits.thy	Mon Feb 22 19:31:00 2010 +0100
     8.3 @@ -15,11 +15,9 @@
     8.4  exception FAIL
     8.5  
     8.6  (* int -> term -> string *)
     8.7 -fun minipick 0 _ = "none"
     8.8 -  | minipick n t =
     8.9 -    case minipick (n - 1) t of
    8.10 -      "none" => Minipick.pick_nits_in_term @{context} (K n) t
    8.11 -    | outcome_code => outcome_code
    8.12 +fun minipick n t =
    8.13 +  map (fn k => Minipick.kodkod_problem_from_term @{context} (K k) t) (1 upto n)
    8.14 +  |> Minipick.solve_any_kodkod_problem @{theory}
    8.15  (* int -> term -> bool *)
    8.16  fun none n t = (minipick n t = "none" orelse raise FAIL)
    8.17  fun genuine n t = (minipick n t = "genuine" orelse raise FAIL)
    8.18 @@ -87,11 +85,11 @@
    8.19  ML {* genuine 2 @{prop "(a\<Colon>'a \<times> 'a \<times> 'a, b) \<noteq> (b, a)"} *}
    8.20  ML {* none 5 @{prop "\<exists>a b\<Colon>'a \<Rightarrow> 'a. (a, b) = (b, a)"} *}
    8.21  ML {* genuine 1 @{prop "(a\<Colon>'a \<Rightarrow> 'a, b) \<noteq> (b, a)"} *}
    8.22 -ML {* none 8 @{prop "fst (a, b) = a"} *}
    8.23 +ML {* none 5 @{prop "fst (a, b) = a"} *}
    8.24  ML {* none 1 @{prop "fst (a, b) = b"} *}
    8.25  ML {* genuine 2 @{prop "fst (a, b) = b"} *}
    8.26  ML {* genuine 2 @{prop "fst (a, b) \<noteq> b"} *}
    8.27 -ML {* none 8 @{prop "snd (a, b) = b"} *}
    8.28 +ML {* none 5 @{prop "snd (a, b) = b"} *}
    8.29  ML {* none 1 @{prop "snd (a, b) = a"} *}
    8.30  ML {* genuine 2 @{prop "snd (a, b) = a"} *}
    8.31  ML {* genuine 2 @{prop "snd (a, b) \<noteq> a"} *}

     9.1 --- a/src/HOL/Nitpick_Examples/Pattern_Nits.thy	Mon Feb 22 14:36:10 2010 +0100
     9.2 +++ b/src/HOL/Nitpick_Examples/Pattern_Nits.thy	Mon Feb 22 19:31:00 2010 +0100
     9.3 @@ -11,8 +11,8 @@
     9.4  imports Main
     9.5  begin
     9.6  
     9.7 -nitpick_params [sat_solver = MiniSat_JNI, max_threads = 1, timeout = 60 s,
     9.8 -                card = 14]
     9.9 +nitpick_params [card = 10, max_potential = 0, sat_solver = MiniSat_JNI,
    9.10 +                max_threads = 1, timeout = 60 s]
    9.11  
    9.12  lemma "x = (case u of () \<Rightarrow> y)"
    9.13  nitpick [expect = genuine]
    9.14 @@ -132,7 +132,7 @@
    9.15  nitpick [expect = genuine]
    9.16  oops
    9.17  
    9.18 -lemma "\<exists>y a b zs. x = (y # Some (a, b) # zs)"
    9.19 +lemma "\<exists>y a b zs. x = y # Some (a, b) # zs"
    9.20  nitpick [expect = genuine]
    9.21  oops
    9.22  

    10.1 --- a/src/HOL/Nitpick_Examples/Record_Nits.thy	Mon Feb 22 14:36:10 2010 +0100
    10.2 +++ b/src/HOL/Nitpick_Examples/Record_Nits.thy	Mon Feb 22 19:31:00 2010 +0100
    10.3 @@ -11,7 +11,8 @@
    10.4  imports Main
    10.5  begin
    10.6  
    10.7 -nitpick_params [sat_solver = MiniSat_JNI, max_threads = 1, timeout = 60 s]
    10.8 +nitpick_params [max_potential = 0, sat_solver = MiniSat_JNI, max_threads = 1,
    10.9 +                timeout = 60 s]
   10.10  
   10.11  record point2d =
   10.12    xc :: int

    11.1 --- a/src/HOL/Nitpick_Examples/Refute_Nits.thy	Mon Feb 22 14:36:10 2010 +0100
    11.2 +++ b/src/HOL/Nitpick_Examples/Refute_Nits.thy	Mon Feb 22 19:31:00 2010 +0100
    11.3 @@ -11,7 +11,8 @@
    11.4  imports Main
    11.5  begin
    11.6  
    11.7 -nitpick_params [sat_solver = MiniSat_JNI, max_threads = 1, timeout = 60 s]
    11.8 +nitpick_params [max_potential = 0, sat_solver = MiniSat_JNI, max_threads = 1,
    11.9 +                timeout = 60 s]
   11.10  
   11.11  lemma "P \<and> Q"
   11.12  apply (rule conjI)
   11.13 @@ -174,14 +175,14 @@
   11.14  nitpick [expect = genuine]
   11.15  oops
   11.16  
   11.17 -text {* The "Drinker's theorem" ... *}
   11.18 +text {* The ``Drinker's theorem'' *}
   11.19  
   11.20  lemma "\<exists>x. f x = g x \<longrightarrow> f = g"
   11.21  nitpick [expect = none]
   11.22  apply (auto simp add: ext)
   11.23  done
   11.24  
   11.25 -text {* ... and an incorrect version of it *}
   11.26 +text {* And an incorrect version of it *}
   11.27  
   11.28  lemma "(\<exists>x. f x = g x) \<longrightarrow> f = g"
   11.29  nitpick [expect = genuine]
   11.30 @@ -241,7 +242,7 @@
   11.31  nitpick [expect = genuine]
   11.32  oops
   11.33  
   11.34 -text {* "The transitive closure 'T' of an arbitrary relation 'P' is non-empty." *}
   11.35 +text {* ``The transitive closure of an arbitrary relation is non-empty.'' *}
   11.36  
   11.37  constdefs
   11.38  "trans" :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool"
   11.39 @@ -255,7 +256,7 @@
   11.40  nitpick [expect = genuine]
   11.41  oops
   11.42  
   11.43 -text {* "The union of transitive closures is equal to the transitive closure of unions." *}
   11.44 +text {* ``The union of transitive closures is equal to the transitive closure of unions.'' *}
   11.45  
   11.46  lemma "(\<forall>x y. (P x y \<or> R x y) \<longrightarrow> T x y) \<longrightarrow> trans T \<longrightarrow> (\<forall>Q. (\<forall>x y. (P x y \<or> R x y) \<longrightarrow> Q x y) \<longrightarrow> trans Q \<longrightarrow> subset T Q)
   11.47   \<longrightarrow> trans_closure TP P
   11.48 @@ -264,19 +265,19 @@
   11.49  nitpick [expect = genuine]
   11.50  oops
   11.51  
   11.52 -text {* "Every surjective function is invertible." *}
   11.53 +text {* ``Every surjective function is invertible.'' *}
   11.54  
   11.55  lemma "(\<forall>y. \<exists>x. y = f x) \<longrightarrow> (\<exists>g. \<forall>x. g (f x) = x)"
   11.56  nitpick [expect = genuine]
   11.57  oops
   11.58  
   11.59 -text {* "Every invertible function is surjective." *}
   11.60 +text {* ``Every invertible function is surjective.'' *}
   11.61  
   11.62  lemma "(\<exists>g. \<forall>x. g (f x) = x) \<longrightarrow> (\<forall>y. \<exists>x. y = f x)"
   11.63  nitpick [expect = genuine]
   11.64  oops
   11.65  
   11.66 -text {* Every point is a fixed point of some function. *}
   11.67 +text {* ``Every point is a fixed point of some function.'' *}
   11.68  
   11.69  lemma "\<exists>f. f x = x"
   11.70  nitpick [card = 1\<midarrow>7, expect = none]
   11.71 @@ -284,21 +285,21 @@
   11.72  apply simp
   11.73  done
   11.74  
   11.75 -text {* Axiom of Choice: first an incorrect version ... *}
   11.76 +text {* Axiom of Choice: first an incorrect version *}
   11.77  
   11.78  lemma "(\<forall>x. \<exists>y. P x y) \<longrightarrow> (\<exists>!f. \<forall>x. P x (f x))"
   11.79  nitpick [expect = genuine]
   11.80  oops
   11.81  
   11.82 -text {* ... and now two correct ones *}
   11.83 +text {* And now two correct ones *}
   11.84  
   11.85  lemma "(\<forall>x. \<exists>y. P x y) \<longrightarrow> (\<exists>f. \<forall>x. P x (f x))"
   11.86 -nitpick [card = 1-5, expect = none]
   11.87 +nitpick [card = 1-4, expect = none]
   11.88  apply (simp add: choice)
   11.89  done
   11.90  
   11.91  lemma "(\<forall>x. \<exists>!y. P x y) \<longrightarrow> (\<exists>!f. \<forall>x. P x (f x))"
   11.92 -nitpick [card = 1-4, expect = none]
   11.93 +nitpick [card = 1-3, expect = none]
   11.94  apply auto
   11.95   apply (simp add: ex1_implies_ex choice)
   11.96  apply (fast intro: ext)
   11.97 @@ -807,12 +808,12 @@
   11.98  oops
   11.99  
  11.100  lemma "list_rec nil cons [] = nil"
  11.101 -nitpick [expect = none]
  11.102 +nitpick [card = 1\<midarrow>5, expect = none]
  11.103  apply simp
  11.104  done
  11.105  
  11.106  lemma "list_rec nil cons (x#xs) = cons x xs (list_rec nil cons xs)"
  11.107 -nitpick [expect = none]
  11.108 +nitpick [card = 1\<midarrow>5, expect = none]
  11.109  apply simp
  11.110  done
  11.111  
  11.112 @@ -923,12 +924,12 @@
  11.113  oops
  11.114  
  11.115  lemma "aexp_bexp_rec_1 number ite equal (Number x) = number x"
  11.116 -nitpick [card = 1\<midarrow>4, expect = none]
  11.117 +nitpick [card = 1\<midarrow>3, expect = none]
  11.118  apply simp
  11.119  done
  11.120  
  11.121  lemma "aexp_bexp_rec_1 number ite equal (ITE x y z) = ite x y z (aexp_bexp_rec_2 number ite equal x) (aexp_bexp_rec_1 number ite equal y) (aexp_bexp_rec_1 number ite equal z)"
  11.122 -nitpick [card = 1\<midarrow>4, expect = none]
  11.123 +nitpick [card = 1\<midarrow>3, expect = none]
  11.124  apply simp
  11.125  done
  11.126  
  11.127 @@ -941,7 +942,7 @@
  11.128  oops
  11.129  
  11.130  lemma "aexp_bexp_rec_2 number ite equal (Equal x y) = equal x y (aexp_bexp_rec_1 number ite equal x) (aexp_bexp_rec_1 number ite equal y)"
  11.131 -nitpick [card = 1\<midarrow>4, expect = none]
  11.132 +nitpick [card = 1\<midarrow>3, expect = none]
  11.133  apply simp
  11.134  done
  11.135  
  11.136 @@ -1001,32 +1002,32 @@
  11.137  oops
  11.138  
  11.139  lemma "X_Y_rec_1 a b c d e f A = a"
  11.140 -nitpick [expect = none]
  11.141 +nitpick [card = 1\<midarrow>5, expect = none]
  11.142  apply simp
  11.143  done
  11.144  
  11.145  lemma "X_Y_rec_1 a b c d e f (B x) = b x (X_Y_rec_1 a b c d e f x)"
  11.146 -nitpick [expect = none]
  11.147 +nitpick [card = 1\<midarrow>5, expect = none]
  11.148  apply simp
  11.149  done
  11.150  
  11.151  lemma "X_Y_rec_1 a b c d e f (C y) = c y (X_Y_rec_2 a b c d e f y)"
  11.152 -nitpick [expect = none]
  11.153 +nitpick [card = 1\<midarrow>5, expect = none]
  11.154  apply simp
  11.155  done
  11.156  
  11.157  lemma "X_Y_rec_2 a b c d e f (D x) = d x (X_Y_rec_1 a b c d e f x)"
  11.158 -nitpick [expect = none]
  11.159 +nitpick [card = 1\<midarrow>5, expect = none]
  11.160  apply simp
  11.161  done
  11.162  
  11.163  lemma "X_Y_rec_2 a b c d e f (E y) = e y (X_Y_rec_2 a b c d e f y)"
  11.164 -nitpick [expect = none]
  11.165 +nitpick [card = 1\<midarrow>5, expect = none]
  11.166  apply simp
  11.167  done
  11.168  
  11.169  lemma "X_Y_rec_2 a b c d e f F = f"
  11.170 -nitpick [expect = none]
  11.171 +nitpick [card = 1\<midarrow>5, expect = none]
  11.172  apply simp
  11.173  done
  11.174  
  11.175 @@ -1057,12 +1058,12 @@
  11.176  oops
  11.177  
  11.178  lemma "XOpt_rec_1 cx dx n1 s1 n2 s2 (CX x) = cx x (XOpt_rec_2 cx dx n1 s1 n2 s2 x)"
  11.179 -nitpick [card = 1\<midarrow>6, expect = none]
  11.180 +nitpick [card = 1\<midarrow>5, expect = none]
  11.181  apply simp
  11.182  done
  11.183  
  11.184  lemma "XOpt_rec_1 cx dx n1 s1 n2 s2 (DX x) = dx x (\<lambda>b. XOpt_rec_3 cx dx n1 s1 n2 s2 (x b))"
  11.185 -nitpick [card = 1\<midarrow>4, expect = none]
  11.186 +nitpick [card = 1\<midarrow>3, expect = none]
  11.187  apply simp
  11.188  done
  11.189  
  11.190 @@ -1150,17 +1151,17 @@
  11.191  oops
  11.192  
  11.193  lemma "Trie_rec_1 tr nil cons (TR x) = tr x (Trie_rec_2 tr nil cons x)"
  11.194 -nitpick [card = 1\<midarrow>6, expect = none]
  11.195 +nitpick [card = 1\<midarrow>4, expect = none]
  11.196  apply simp
  11.197  done
  11.198  
  11.199  lemma "Trie_rec_2 tr nil cons [] = nil"
  11.200 -nitpick [card = 1\<midarrow>6, expect = none]
  11.201 +nitpick [card = 1\<midarrow>4, expect = none]
  11.202  apply simp
  11.203  done
  11.204  
  11.205  lemma "Trie_rec_2 tr nil cons (x#xs) = cons x xs (Trie_rec_1 tr nil cons x) (Trie_rec_2 tr nil cons xs)"
  11.206 -nitpick [card = 1\<midarrow>6, expect = none]
  11.207 +nitpick [card = 1\<midarrow>4, expect = none]
  11.208  apply simp
  11.209  done
  11.210  
  11.211 @@ -1365,15 +1366,15 @@
  11.212  oops
  11.213  
  11.214  lemma "f (lfp f) = lfp f"
  11.215 -nitpick [expect = genuine]
  11.216 +nitpick [card = 2, expect = genuine]
  11.217  oops
  11.218  
  11.219  lemma "f (gfp f) = gfp f"
  11.220 -nitpick [expect = genuine]
  11.221 +nitpick [card = 2, expect = genuine]
  11.222  oops
  11.223  
  11.224  lemma "lfp f = gfp f"
  11.225 -nitpick [expect = genuine]
  11.226 +nitpick [card = 2, expect = genuine]
  11.227  oops
  11.228  
  11.229  subsubsection {* Axiomatic Type Classes and Overloading *}

    12.1 --- a/src/HOL/Nitpick_Examples/Special_Nits.thy	Mon Feb 22 14:36:10 2010 +0100
    12.2 +++ b/src/HOL/Nitpick_Examples/Special_Nits.thy	Mon Feb 22 19:31:00 2010 +0100
    12.3 @@ -11,8 +11,8 @@
    12.4  imports Main
    12.5  begin
    12.6  
    12.7 -nitpick_params [sat_solver = MiniSat_JNI, max_threads = 1, timeout = 60 s,
    12.8 -                card = 4]
    12.9 +nitpick_params [card = 4, sat_solver = MiniSat_JNI, max_threads = 1,
   12.10 +                timeout = 60 s]
   12.11  
   12.12  fun f1 :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat" where
   12.13  "f1 a b c d e = a + b + c + d + e"

    13.1 --- a/src/HOL/Nitpick_Examples/Typedef_Nits.thy	Mon Feb 22 14:36:10 2010 +0100
    13.2 +++ b/src/HOL/Nitpick_Examples/Typedef_Nits.thy	Mon Feb 22 19:31:00 2010 +0100
    13.3 @@ -11,8 +11,8 @@
    13.4  imports Main Rational
    13.5  begin
    13.6  
    13.7 -nitpick_params [sat_solver = MiniSat_JNI, max_threads = 1, timeout = 60 s,
    13.8 -                card = 1\<midarrow>4]
    13.9 +nitpick_params [card = 1\<midarrow>4, sat_solver = MiniSat_JNI, max_threads = 1,
   13.10 +                timeout = 60 s]
   13.11  
   13.12  typedef three = "{0\<Colon>nat, 1, 2}"
   13.13  by blast
   13.14 @@ -138,7 +138,8 @@
   13.15  by (rule Inl_Rep_not_Inr_Rep)
   13.16  
   13.17  lemma "Abs_Sum (Rep_Sum a) = a"
   13.18 -nitpick [card = 1\<midarrow>2, timeout = 60 s, expect = none]
   13.19 +nitpick [card = 1, expect = none]
   13.20 +nitpick [card = 2, expect = none]
   13.21  by (rule Rep_Sum_inverse)
   13.22  
   13.23  lemma "0::nat \<equiv> Abs_Nat Zero_Rep"

    14.1 --- a/src/HOL/Tools/Nitpick/minipick.ML	Mon Feb 22 14:36:10 2010 +0100
    14.2 +++ b/src/HOL/Tools/Nitpick/minipick.ML	Mon Feb 22 19:31:00 2010 +0100
    14.3 @@ -19,7 +19,9 @@
    14.4    val true_atom : Kodkod.rel_expr
    14.5    val formula_from_atom : Kodkod.rel_expr -> Kodkod.formula
    14.6    val atom_from_formula : Kodkod.formula -> Kodkod.rel_expr
    14.7 -  val pick_nits_in_term : Proof.context -> (typ -> int) -> term -> string
    14.8 +  val kodkod_problem_from_term :
    14.9 +    Proof.context -> (typ -> int) -> term -> Kodkod.problem
   14.10 +  val solve_any_kodkod_problem : theory -> Kodkod.problem list -> string
   14.11  end;
   14.12  
   14.13  structure Minipick : MINIPICK =
   14.14 @@ -287,11 +289,10 @@
   14.15  fun declarative_axiom_for_free card i (_, T) =
   14.16    declarative_axiom_for_rel_expr card [] T (Rel (arity_of RRep card T, i))
   14.17  
   14.18 -(* Proof.context -> (typ -> int) -> term -> string *)
   14.19 -fun pick_nits_in_term ctxt raw_card t =
   14.20 +(* Proof.context -> (typ -> int) -> term -> problem *)
   14.21 +fun kodkod_problem_from_term ctxt raw_card t =
   14.22    let
   14.23      val thy = ProofContext.theory_of ctxt
   14.24 -    val {overlord, ...} = Nitpick_Isar.default_params thy []
   14.25      (* typ -> int *)
   14.26      fun card (Type ("fun", [T1, T2])) = reasonable_power (card T2) (card T1)
   14.27        | card (Type ("*", [T1, T2])) = card T1 * card T2
   14.28 @@ -306,11 +307,19 @@
   14.29      val formula = kodkod_formula_from_term ctxt card frees neg_t
   14.30                    |> fold_rev (curry And) declarative_axioms
   14.31      val univ_card = univ_card 0 0 0 bounds formula
   14.32 -    val problem =
   14.33 -      {comment = "", settings = [], univ_card = univ_card, tuple_assigns = [],
   14.34 -       bounds = bounds, int_bounds = [], expr_assigns = [], formula = formula}
   14.35    in
   14.36 -    case solve_any_problem overlord NONE 0 1 [problem] of
   14.37 +    {comment = "", settings = [], univ_card = univ_card, tuple_assigns = [],
   14.38 +     bounds = bounds, int_bounds = [], expr_assigns = [], formula = formula}
   14.39 +  end
   14.40 +
   14.41 +(* theory -> problem list -> string *)
   14.42 +fun solve_any_kodkod_problem thy problems =
   14.43 +  let
   14.44 +    val {overlord, ...} = Nitpick_Isar.default_params thy []
   14.45 +    val max_threads = 1
   14.46 +    val max_solutions = 1
   14.47 +  in
   14.48 +    case solve_any_problem overlord NONE max_threads max_solutions problems of
   14.49        NotInstalled => "unknown"
   14.50      | Normal ([], _) => "none"
   14.51      | Normal _ => "genuine"
   14.52 @@ -318,7 +327,5 @@
   14.53      | Interrupted _ => "unknown"
   14.54      | Error (s, _) => error ("Kodkod error: " ^ s)
   14.55    end
   14.56 -  handle NOT_SUPPORTED details =>
   14.57 -         (warning ("Unsupported case: " ^ details ^ "."); "unknown")
   14.58  
   14.59  end;

    15.1 --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Mon Feb 22 14:36:10 2010 +0100
    15.2 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Mon Feb 22 19:31:00 2010 +0100
    15.3 @@ -597,8 +597,8 @@
    15.4  fun unregister_codatatype co_T = register_codatatype co_T "" []
    15.5  
    15.6  (* theory -> typ -> bool *)
    15.7 -fun is_quot_type _ (Type ("IntEx.my_int", _)) = true (* FIXME *)
    15.8 -  | is_quot_type _ (Type ("FSet.fset", _)) = true
    15.9 +fun is_quot_type thy (Type (s, _)) =
   15.10 +    is_some (Quotient_Info.quotdata_lookup_raw thy s)
   15.11    | is_quot_type _ _ = false
   15.12  fun is_codatatype thy (Type (s, _)) =
   15.13      not (null (AList.lookup (op =) (#codatatypes (Data.get thy)) s
   15.14 @@ -666,11 +666,13 @@
   15.15       | NONE => false)
   15.16    | is_rep_fun _ _ = false
   15.17  (* Proof.context -> styp -> bool *)
   15.18 -fun is_quot_abs_fun _ ("IntEx.abs_my_int", _) = true
   15.19 -  | is_quot_abs_fun _ ("FSet.abs_fset", _) = true
   15.20 +fun is_quot_abs_fun ctxt (x as (_, Type ("fun", [_, Type (s', _)]))) =
   15.21 +    (try (Quotient_Term.absrep_const_chk Quotient_Term.AbsF ctxt) s'
   15.22 +     = SOME (Const x))
   15.23    | is_quot_abs_fun _ _ = false
   15.24 -fun is_quot_rep_fun _ ("IntEx.rep_my_int", _) = true
   15.25 -  | is_quot_rep_fun _ ("FSet.rep_fset", _) = true
   15.26 +fun is_quot_rep_fun ctxt (x as (_, Type ("fun", [Type (s', _), _]))) =
   15.27 +    (try (Quotient_Term.absrep_const_chk Quotient_Term.RepF ctxt) s'
   15.28 +     = SOME (Const x))
   15.29    | is_quot_rep_fun _ _ = false
   15.30  
   15.31  (* theory -> styp -> styp *)
   15.32 @@ -680,18 +682,16 @@
   15.33       | NONE => raise TERM ("Nitpick_HOL.mate_of_rep_fun", [Const x]))
   15.34    | mate_of_rep_fun _ x = raise TERM ("Nitpick_HOL.mate_of_rep_fun", [Const x])
   15.35  (* theory -> typ -> typ *)
   15.36 -fun rep_type_for_quot_type _ (Type ("IntEx.my_int", [])) = @{typ "nat * nat"}
   15.37 -  | rep_type_for_quot_type _ (Type ("FSet.fset", [T])) =
   15.38 -    Type (@{type_name list}, [T])
   15.39 -  | rep_type_for_quot_type _ T =
   15.40 -    raise TYPE ("Nitpick_HOL.rep_type_for_quot_type", [T], [])
   15.41 +fun rep_type_for_quot_type thy (T as Type (s, _)) =
   15.42 +  let val {qtyp, rtyp, ...} = Quotient_Info.quotdata_lookup thy s in
   15.43 +    instantiate_type thy qtyp T rtyp
   15.44 +  end
   15.45  (* theory -> typ -> term *)
   15.46 -fun equiv_relation_for_quot_type _ (Type ("IntEx.my_int", [])) =
   15.47 -    Const ("IntEx.intrel", @{typ "(nat * nat) => (nat * nat) => bool"})
   15.48 -  | equiv_relation_for_quot_type _ (Type ("FSet.fset", [T])) =
   15.49 -    Const ("FSet.list_eq",
   15.50 -           Type (@{type_name list}, [T]) --> Type (@{type_name list}, [T])
   15.51 -           --> bool_T)
   15.52 +fun equiv_relation_for_quot_type thy (Type (s, Ts)) =
   15.53 +    let
   15.54 +      val {qtyp, equiv_rel, ...} = Quotient_Info.quotdata_lookup thy s
   15.55 +      val Ts' = qtyp |> dest_Type |> snd
   15.56 +    in subst_atomic_types (Ts' ~~ Ts) equiv_rel end
   15.57    | equiv_relation_for_quot_type _ T =
   15.58      raise TYPE ("Nitpick_HOL.equiv_relation_for_quot_type", [T], [])
   15.59  
   15.60 @@ -1547,7 +1547,7 @@
   15.61  val unfold_max_depth = 255
   15.62  
   15.63  (* hol_context -> term -> term *)
   15.64 -fun unfold_defs_in_term (hol_ctxt as {thy, stds, fast_descrs, case_names,
   15.65 +fun unfold_defs_in_term (hol_ctxt as {thy, ctxt, stds, fast_descrs, case_names,
   15.66                                        def_table, ground_thm_table, ersatz_table,
   15.67                                        ...}) =
   15.68    let
   15.69 @@ -1632,7 +1632,7 @@
   15.70                else if is_stale_constr thy x then
   15.71                  raise NOT_SUPPORTED ("(non-co)constructors of codatatypes \
   15.72                                       \(\"" ^ s ^ "\")")
   15.73 -              else if is_quot_abs_fun thy x then
   15.74 +              else if is_quot_abs_fun ctxt x then
   15.75                  let
   15.76                    val rep_T = domain_type T
   15.77                    val abs_T = range_type T
   15.78 @@ -1642,7 +1642,7 @@
   15.79                                 $ (Const (@{const_name quot_normal},
   15.80                                           rep_T --> rep_T) $ Bound 0)), ts)
   15.81                  end
   15.82 -              else if is_quot_rep_fun thy x then
   15.83 +              else if is_quot_rep_fun ctxt x then
   15.84                  let
   15.85                    val abs_T = domain_type T
   15.86                    val rep_T = range_type T

    16.1 --- a/src/HOL/Tools/Nitpick/nitpick_peephole.ML	Mon Feb 22 14:36:10 2010 +0100
    16.2 +++ b/src/HOL/Tools/Nitpick/nitpick_peephole.ML	Mon Feb 22 19:31:00 2010 +0100
    16.3 @@ -340,24 +340,23 @@
    16.4                 else Project (r, is)
    16.5               end
    16.6  
    16.7 +    (* (rel_expr -> formula) -> rel_expr -> formula *)
    16.8 +    fun s_xone xone r =
    16.9 +      if is_one_rel_expr r then
   16.10 +        True
   16.11 +      else case arity_of_rel_expr r of
   16.12 +        1 => xone r
   16.13 +      | arity => foldl1 And (map (xone o s_project r o single o Num)
   16.14 +                                 (index_seq 0 arity))
   16.15      (* rel_expr -> formula *)
   16.16      fun s_no None = True
   16.17        | s_no (Product (r1, r2)) = s_or (s_no r1) (s_no r2)
   16.18        | s_no (Intersect (Closure (Rel x), Iden)) = Acyclic x
   16.19        | s_no r = if is_one_rel_expr r then False else No r
   16.20      fun s_lone None = True
   16.21 -      | s_lone r = if is_one_rel_expr r then True else Lone r
   16.22 +      | s_lone r = s_xone Lone r
   16.23      fun s_one None = False
   16.24 -      | s_one r =
   16.25 -        if is_one_rel_expr r then
   16.26 -          True
   16.27 -        else if inline_rel_expr r then
   16.28 -          case arity_of_rel_expr r of
   16.29 -            1 => One r
   16.30 -          | arity => foldl1 And (map (One o s_project r o single o Num)
   16.31 -                                     (index_seq 0 arity))
   16.32 -        else
   16.33 -          One r
   16.34 +      | s_one r = s_xone One r
   16.35      fun s_some None = False
   16.36        | s_some (Atom _) = True
   16.37        | s_some (Product (r1, r2)) = s_and (s_some r1) (s_some r2)

    17.1 --- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Mon Feb 22 14:36:10 2010 +0100
    17.2 +++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Mon Feb 22 19:31:00 2010 +0100
    17.3 @@ -293,8 +293,8 @@
    17.4          $ do_term new_Ts old_Ts polar t2
    17.5        | Const (s as @{const_name The}, T) => do_description_operator s T
    17.6        | Const (s as @{const_name Eps}, T) => do_description_operator s T
    17.7 -      | Const (@{const_name quot_normal}, Type ("fun", [_, T2])) =>
    17.8 -        let val T' = box_type hol_ctxt InSel T2 in
    17.9 +      | Const (@{const_name quot_normal}, Type ("fun", [T, _])) =>
   17.10 +        let val T' = box_type hol_ctxt InFunLHS T in
   17.11            Const (@{const_name quot_normal}, T' --> T')
   17.12          end
   17.13        | Const (s as @{const_name Tha}, T) => do_description_operator s T

    18.1 --- a/src/HOL/Tools/Nitpick/nitpick_tests.ML	Mon Feb 22 14:36:10 2010 +0100
    18.2 +++ b/src/HOL/Tools/Nitpick/nitpick_tests.ML	Mon Feb 22 19:31:00 2010 +0100
    18.3 @@ -294,7 +294,8 @@
    18.4  *)
    18.5    ]
    18.6  
    18.7 -fun problem_for_nut ctxt name u =
    18.8 +(* Proof.context -> string * nut -> Kodkod.problem *)
    18.9 +fun problem_for_nut ctxt (name, u) =
   18.10    let
   18.11      val debug = false
   18.12      val peephole_optim = true
   18.13 @@ -320,15 +321,11 @@
   18.14       formula = formula}
   18.15    end
   18.16  
   18.17 -(* string -> unit *)
   18.18 -fun run_test name =
   18.19 +(* unit -> unit *)
   18.20 +fun run_all_tests () =
   18.21    case Kodkod.solve_any_problem false NONE 0 1
   18.22 -           [problem_for_nut @{context} name
   18.23 -                            (the (AList.lookup (op =) tests name))] of
   18.24 +                                (map (problem_for_nut @{context}) tests) of
   18.25      Kodkod.Normal ([], _) => ()
   18.26 -  | _ => warning ("Test " ^ quote name ^ " failed")
   18.27 -
   18.28 -(* unit -> unit *)
   18.29 -fun run_all_tests () = List.app run_test (map fst tests)
   18.30 +  | _ => error "Tests failed"
   18.31  
   18.32  end;