--- a/doc-src/Nitpick/nitpick.tex Mon Feb 22 14:36:10 2010 +0100
+++ b/doc-src/Nitpick/nitpick.tex Mon Feb 22 19:31:00 2010 +0100
@@ -141,11 +141,11 @@
This section introduces Nitpick by presenting small examples. If possible, you
should try out the examples on your workstation. Your theory file should start
-the standard way:
+as follows:
\prew
\textbf{theory}~\textit{Scratch} \\
-\textbf{imports}~\textit{Main} \\
+\textbf{imports}~\textit{Main~Coinductive\_List~Quotient\_Product~RealDef} \\
\textbf{begin}
\postw
@@ -439,7 +439,7 @@
value (displayed as `$\unk$'). The type \textit{int} is handled similarly.
Internally, undefined values lead to a three-valued logic.
-Here is an example involving \textit{int}:
+Here is an example involving \textit{int\/}:
\prew
\textbf{lemma} ``$\lbrakk i \le j;\> n \le (m{\Colon}\mathit{int})\rbrakk \,\Longrightarrow\, i * n + j * m \le i * m + j * n$'' \\
@@ -627,7 +627,7 @@
genuine counterexample for \textit{card}~$'a~\textit{list}$~= 10, it is very
unlikely that one could be found for smaller cardinalities.
-\subsection{Typedefs, Records, Rationals, and Reals}
+\subsection{Typedefs, Quotient Types, Records, Rationals, and Reals}
\label{typedefs-records-rationals-and-reals}
Nitpick generally treats types declared using \textbf{typedef} as datatypes
@@ -651,12 +651,41 @@
\hbox{}\qquad\qquad $\textit{three} = \{\Abs{0},\, \Abs{1},\, \Abs{2},\, \unr\}$
\postw
-%% MARK
In the output above, $\Abs{n}$ abbreviates $\textit{Abs\_three}~n$.
-%% MARK
-Records, which are implemented as \textbf{typedef}s behind the scenes, are
-handled in much the same way:
+Quotient types are handled in much the same way. The following fragment defines
+the integer type \textit{my\_int} by encoding the integer $x$ by a pair of
+natural numbers $(m, n)$ such that $x + n = m$:
+
+\prew
+\textbf{fun} \textit{my\_int\_rel} \textbf{where} \\
+``$\textit{my\_int\_rel}~(x,\, y)~(u,\, v) = (x + v = u + y)$'' \\[2\smallskipamount]
+%
+\textbf{quotient\_type}~\textit{my\_int} = ``$\textit{nat} \times \textit{nat\/}$''$\;{/}\;$\textit{my\_int\_rel} \\
+\textbf{by}~(\textit{auto simp add\/}:\ \textit{equivp\_def expand\_fun\_eq}) \\[2\smallskipamount]
+%
+\textbf{definition}~\textit{add\_raw}~\textbf{where} \\
+``$\textit{add\_raw} \,\equiv\, \lambda(x,\, y)~(u,\, v).\; (x + (u\Colon\textit{nat}), y + (v\Colon\textit{nat}))$'' \\[2\smallskipamount]
+%
+\textbf{quotient\_definition} ``$\textit{add\/}\Colon\textit{my\_int} \Rightarrow \textit{my\_int} \Rightarrow \textit{my\_int\/}$'' \textbf{is} \textit{add\_raw} \\[2\smallskipamount]
+%
+\textbf{lemma} ``$\textit{add}~x~y = \textit{add}~x~x$'' \\
+\textbf{nitpick} [\textit{show\_datatypes}] \\[2\smallskipamount]
+\slshape Nitpick found a counterexample: \\[2\smallskipamount]
+\hbox{}\qquad Free variables: \nopagebreak \\
+\hbox{}\qquad\qquad $x = \Abs{(0,\, 0)}$ \\
+\hbox{}\qquad\qquad $y = \Abs{(1,\, 0)}$ \\
+\hbox{}\qquad Datatypes: \\
+\hbox{}\qquad\qquad $\textit{nat} = \{0,\, 1,\, \unr\}$ \\
+\hbox{}\qquad\qquad $\textit{nat} \times \textit{nat} = \{(0,\, 0),\> (1,\, 0),\> \unr\}$ \\
+\hbox{}\qquad\qquad $\textit{my\_int} = \{\Abs{(0,\, 0)},\> \Abs{(1,\, 0)},\> \unr\}$
+\postw
+
+In the counterexample, $\Abs{(0,\, 0)}$ and $\Abs{(1,\, 0)}$ represent the
+integers $0$ and $1$, respectively. Other representants would have been
+possible---e.g., $\Abs{(5,\, 5)}$ and $\Abs{(12,\, 11)}$.
+
+Records are also handled as datatypes with a single constructor:
\prew
\textbf{record} \textit{point} = \\
@@ -675,6 +704,8 @@
& \lparr\textit{Xcoord} = 1,\> \textit{Ycoord} = 1\rparr,\, \unr\}\end{aligned}$
\postw
+
+
Finally, Nitpick provides rudimentary support for rationals and reals using a
similar approach:
@@ -949,13 +980,13 @@
\slshape The type ``\kern1pt$'a$'' passed the monotonicity test. Nitpick might be able to skip
some scopes. \\[2\smallskipamount]
Trying 8 scopes: \\
-\hbox{}\qquad \textit{card} $'a$~= 1, \textit{card} ``\kern1pt$'a~\textit{list}$''~= 1,
+\hbox{}\qquad \textit{card} $'a$~= 1, \textit{card} ``\kern1pt$'a~\textit{list\/}$''~= 1,
and \textit{bisim\_depth}~= 0. \\
\hbox{}\qquad $\qquad\vdots$ \\[.5\smallskipamount]
-\hbox{}\qquad \textit{card} $'a$~= 8, \textit{card} ``\kern1pt$'a~\textit{list}$''~= 8,
+\hbox{}\qquad \textit{card} $'a$~= 8, \textit{card} ``\kern1pt$'a~\textit{list\/}$''~= 8,
and \textit{bisim\_depth}~= 7. \\[2\smallskipamount]
Nitpick found a counterexample for {\itshape card}~$'a$ = 2,
-\textit{card}~``\kern1pt$'a~\textit{list}$''~= 2, and \textit{bisim\_\allowbreak
+\textit{card}~``\kern1pt$'a~\textit{list\/}$''~= 2, and \textit{bisim\_\allowbreak
depth}~= 1:
\\[2\smallskipamount]
\hbox{}\qquad Free variables: \nopagebreak \\
@@ -1118,7 +1149,7 @@
\textit{Lam}~(\textit{Lam}~(\textit{Var}~0))$. Using the traditional
$\lambda$-term notation, $t$~is
$\lambda x\, y.\> x$ whereas $\textit{subst}~\sigma~t$ is $\lambda x\, y.\> y$.
-The bug is in \textit{subst}: The $\textit{lift}~(\sigma~m)~1$ call should be
+The bug is in \textit{subst\/}: The $\textit{lift}~(\sigma~m)~1$ call should be
replaced with $\textit{lift}~(\sigma~m)~0$.
An interesting aspect of Nitpick's verbose output is that it assigned inceasing
@@ -1509,7 +1540,7 @@
completeness of the set $S$. First, soundness:
\prew
-\textbf{theorem}~\textit{S\_sound}: \\
+\textbf{theorem}~\textit{S\_sound\/}: \\
``$w \in S \longrightarrow \textit{length}~[x\mathbin{\leftarrow} w.\; x = a] =
\textit{length}~[x\mathbin{\leftarrow} w.\; x = b]$'' \\
\textbf{nitpick} \\[2\smallskipamount]
@@ -1691,7 +1722,7 @@
of elements stored in the tree:
\prew
-\textbf{theorem}~\textit{dataset\_skew\_split}:\\
+\textbf{theorem}~\textit{dataset\_skew\_split\/}:\\
``$\textit{dataset}~(\textit{skew}~t) = \textit{dataset}~t$'' \\
``$\textit{dataset}~(\textit{split}~t) = \textit{dataset}~t$'' \\
\textbf{nitpick} \\[2\smallskipamount]
@@ -1702,7 +1733,7 @@
should not alter the tree:
\prew
-\textbf{theorem}~\textit{wf\_skew\_split}:\\
+\textbf{theorem}~\textit{wf\_skew\_split\/}:\\
``$\textit{wf}~t\,\Longrightarrow\, \textit{skew}~t = t$'' \\
``$\textit{wf}~t\,\Longrightarrow\, \textit{split}~t = t$'' \\
\textbf{nitpick} \\[2\smallskipamount]
@@ -1723,7 +1754,7 @@
\textit{split}. Let's see if this causes any problems:
\prew
-\textbf{theorem}~\textit{wf\_insort}:\kern.4em ``$\textit{wf}~t\,\Longrightarrow\, \textit{wf}~(\textit{insort}~t~x)$'' \\
+\textbf{theorem}~\textit{wf\_insort\/}:\kern.4em ``$\textit{wf}~t\,\Longrightarrow\, \textit{wf}~(\textit{insort}~t~x)$'' \\
\textbf{nitpick} \\[2\smallskipamount]
\slshape Nitpick found a counterexample for \textit{card} $'a$ = 4: \\[2\smallskipamount]
\hbox{}\qquad Free variables: \nopagebreak \\
@@ -1738,7 +1769,7 @@
$\textit{insort}~t~x$ using the \textit{eval} option. This gives
\prew
-\textbf{theorem} \textit{wf\_insort\_nat}:\kern.4em ``$\textit{wf}~t\,\Longrightarrow\, \textit{wf}~(\textit{insort}~t~(x\Colon\textit{nat}))$'' \\
+\textbf{theorem} \textit{wf\_insort\_nat\/}:\kern.4em ``$\textit{wf}~t\,\Longrightarrow\, \textit{wf}~(\textit{insort}~t~(x\Colon\textit{nat}))$'' \\
\textbf{nitpick} [\textit{eval} = ``$\textit{insort}~t~x$''] \\[2\smallskipamount]
\slshape Nitpick found a counterexample: \\[2\smallskipamount]
\hbox{}\qquad Free variables: \nopagebreak \\
@@ -1755,7 +1786,7 @@
Reintroducing the code seems to solve the problem:
\prew
-\textbf{theorem}~\textit{wf\_insort}:\kern.4em ``$\textit{wf}~t\,\Longrightarrow\, \textit{wf}~(\textit{insort}~t~x)$'' \\
+\textbf{theorem}~\textit{wf\_insort\/}:\kern.4em ``$\textit{wf}~t\,\Longrightarrow\, \textit{wf}~(\textit{insort}~t~x)$'' \\
\textbf{nitpick} \\[2\smallskipamount]
{\slshape Nitpick ran out of time after checking 7 of 8 scopes.}
\postw
@@ -1764,7 +1795,7 @@
obvious way:
\prew
-\textbf{theorem} \textit{dataset\_insort}:\kern.4em
+\textbf{theorem} \textit{dataset\_insort\/}:\kern.4em
``$\textit{dataset}~(\textit{insort}~t~x) = \{x\} \cup \textit{dataset}~t$'' \\
\textbf{nitpick} \\[2\smallskipamount]
{\slshape Nitpick ran out of time after checking 6 of 8 scopes.}
@@ -1825,19 +1856,19 @@
\begin{enum}
\item[$\bullet$] \qtybf{string}: A string.
-\item[$\bullet$] \qtybf{bool}: \textit{true} or \textit{false}.
-\item[$\bullet$] \qtybf{bool\_or\_smart}: \textit{true}, \textit{false}, or \textit{smart}.
-\item[$\bullet$] \qtybf{int}: An integer. Negative integers are prefixed with a hyphen.
-\item[$\bullet$] \qtybf{int\_or\_smart}: An integer or \textit{smart}.
+\item[$\bullet$] \qtybf{bool\/}: \textit{true} or \textit{false}.
+\item[$\bullet$] \qtybf{bool\_or\_smart\/}: \textit{true}, \textit{false}, or \textit{smart}.
+\item[$\bullet$] \qtybf{int\/}: An integer. Negative integers are prefixed with a hyphen.
+\item[$\bullet$] \qtybf{int\_or\_smart\/}: An integer or \textit{smart}.
\item[$\bullet$] \qtybf{int\_range}: An integer (e.g., 3) or a range
of nonnegative integers (e.g., $1$--$4$). The range symbol `--' can be entered as \texttt{-} (hyphen) or \texttt{\char`\\\char`\<midarrow\char`\>}.
\item[$\bullet$] \qtybf{int\_seq}: A comma-separated sequence of ranges of integers (e.g.,~1{,}3{,}\allowbreak6--8).
\item[$\bullet$] \qtybf{time}: An integer followed by $\textit{min}$ (minutes), $s$ (seconds), or \textit{ms}
(milliseconds), or the keyword \textit{none} ($\infty$ years).
-\item[$\bullet$] \qtybf{const}: The name of a HOL constant.
+\item[$\bullet$] \qtybf{const\/}: The name of a HOL constant.
\item[$\bullet$] \qtybf{term}: A HOL term (e.g., ``$f~x$'').
-\item[$\bullet$] \qtybf{term\_list}: A space-separated list of HOL terms (e.g.,
+\item[$\bullet$] \qtybf{term\_list\/}: A space-separated list of HOL terms (e.g.,
``$f~x$''~``$g~y$'').
\item[$\bullet$] \qtybf{type}: A HOL type.
\end{enum}
@@ -2190,7 +2221,6 @@
the \textit{format}~\qty{term} option described above.
\end{enum}
-%% MARK: Authentication
\subsection{Authentication}
\label{authentication}
@@ -2564,14 +2594,14 @@
definition as follows:
\prew
-\textbf{lemma} $\mathit{odd\_def}'$ [\textit{nitpick\_def}]: ``$\textit{odd}~n \,\equiv\, n~\textrm{mod}~2 = 1$''
+\textbf{lemma} $\mathit{odd\_def}'$ [\textit{nitpick\_def}]:\kern.4em ``$\textit{odd}~n \,\equiv\, n~\textrm{mod}~2 = 1$''
\postw
Nitpick then expands all occurrences of $\mathit{odd}~n$ to $n~\textrm{mod}~2
= 1$. Alternatively, we can specify an equational specification of the constant:
\prew
-\textbf{lemma} $\mathit{odd\_simp}'$ [\textit{nitpick\_simp}]: ``$\textit{odd}~n = (n~\textrm{mod}~2 = 1)$''
+\textbf{lemma} $\mathit{odd\_simp}'$ [\textit{nitpick\_simp}]:\kern.4em ``$\textit{odd}~n = (n~\textrm{mod}~2 = 1)$''
\postw
Such tweaks should be done with great care, because Nitpick will assume that the
--- a/src/HOL/Main.thy Mon Feb 22 14:36:10 2010 +0100
+++ b/src/HOL/Main.thy Mon Feb 22 19:31:00 2010 +0100
@@ -1,7 +1,7 @@
header {* Main HOL *}
theory Main
-imports Plain Predicate_Compile Nitpick Quotient
+imports Plain Predicate_Compile Nitpick
begin
text {*
--- a/src/HOL/Nitpick.thy Mon Feb 22 14:36:10 2010 +0100
+++ b/src/HOL/Nitpick.thy Mon Feb 22 19:31:00 2010 +0100
@@ -8,7 +8,7 @@
header {* Nitpick: Yet Another Counterexample Generator for Isabelle/HOL *}
theory Nitpick
-imports Map SAT
+imports Map Quotient SAT
uses ("Tools/Nitpick/kodkod.ML")
("Tools/Nitpick/kodkod_sat.ML")
("Tools/Nitpick/nitpick_util.ML")
--- a/src/HOL/Nitpick_Examples/Core_Nits.thy Mon Feb 22 14:36:10 2010 +0100
+++ b/src/HOL/Nitpick_Examples/Core_Nits.thy Mon Feb 22 19:31:00 2010 +0100
@@ -11,82 +11,67 @@
imports Main
begin
-nitpick_params [sat_solver = MiniSat_JNI, max_threads = 1, timeout = 60 s]
+nitpick_params [max_potential = 0, sat_solver = MiniSat_JNI, max_threads = 1,
+ timeout = 60 s]
subsection {* Curry in a Hurry *}
lemma "(\<lambda>f x y. (curry o split) f x y) = (\<lambda>f x y. (\<lambda>x. x) f x y)"
-nitpick [card = 1\<midarrow>4, expect = none]
-nitpick [card = 100, expect = none, timeout = none]
+nitpick [card = 1\<midarrow>12, expect = none]
by auto
lemma "(\<lambda>f p. (split o curry) f p) = (\<lambda>f p. (\<lambda>x. x) f p)"
-nitpick [card = 2]
-nitpick [card = 1\<midarrow>4, expect = none]
-nitpick [card = 10, expect = none]
+nitpick [card = 1\<midarrow>12, expect = none]
by auto
lemma "split (curry f) = f"
-nitpick [card = 1\<midarrow>4, expect = none]
-nitpick [card = 10, expect = none]
-nitpick [card = 40, expect = none]
+nitpick [card = 1\<midarrow>12, expect = none]
by auto
lemma "curry (split f) = f"
-nitpick [card = 1\<midarrow>4, expect = none]
-nitpick [card = 40, expect = none]
+nitpick [card = 1\<midarrow>12, expect = none]
by auto
lemma "(split o curry) f = f"
-nitpick [card = 1\<midarrow>4, expect = none]
-nitpick [card = 40, expect = none]
+nitpick [card = 1\<midarrow>12, expect = none]
by auto
lemma "(curry o split) f = f"
-nitpick [card = 1\<midarrow>4, expect = none]
-nitpick [card = 1000, expect = none]
+nitpick [card = 1\<midarrow>12, expect = none]
by auto
lemma "(split o curry) f = (\<lambda>x. x) f"
-nitpick [card = 1\<midarrow>4, expect = none]
-nitpick [card = 40, expect = none]
+nitpick [card = 1\<midarrow>12, expect = none]
by auto
lemma "(curry o split) f = (\<lambda>x. x) f"
-nitpick [card = 1\<midarrow>4, expect = none]
-nitpick [card = 40, expect = none]
+nitpick [card = 1\<midarrow>12, expect = none]
by auto
lemma "((split o curry) f) p = ((\<lambda>x. x) f) p"
-nitpick [card = 1\<midarrow>4, expect = none]
-nitpick [card = 40, expect = none]
+nitpick [card = 1\<midarrow>12, expect = none]
by auto
lemma "((curry o split) f) x = ((\<lambda>x. x) f) x"
-nitpick [card = 1\<midarrow>4, expect = none]
-nitpick [card = 1000, expect = none]
+nitpick [card = 1\<midarrow>12, expect = none]
by auto
lemma "((curry o split) f) x y = ((\<lambda>x. x) f) x y"
-nitpick [card = 1\<midarrow>4, expect = none]
-nitpick [card = 1000, expect = none]
+nitpick [card = 1\<midarrow>12, expect = none]
by auto
lemma "split o curry = (\<lambda>x. x)"
-nitpick [card = 1\<midarrow>4, expect = none]
-nitpick [card = 40, expect = none]
+nitpick [card = 1\<midarrow>12, expect = none]
apply (rule ext)+
by auto
lemma "curry o split = (\<lambda>x. x)"
-nitpick [card = 1\<midarrow>4, expect = none]
-nitpick [card = 100, expect = none]
+nitpick [card = 1\<midarrow>12, expect = none]
apply (rule ext)+
by auto
lemma "split (\<lambda>x y. f (x, y)) = f"
-nitpick [card = 1\<midarrow>4, expect = none]
-nitpick [card = 40, expect = none]
+nitpick [card = 1\<midarrow>12, expect = none]
by auto
subsection {* Representations *}
@@ -96,13 +81,12 @@
by auto
lemma "(\<exists>g. \<forall>x. g (f x) = x) \<longrightarrow> (\<forall>y. \<exists>x. y = f x)"
-nitpick [card 'a = 35, card 'b = 34, expect = genuine]
-nitpick [card = 1\<midarrow>15, mono, expect = none]
+nitpick [card 'a = 25, card 'b = 24, expect = genuine]
+nitpick [card = 1\<midarrow>10, mono, expect = none]
oops
lemma "\<exists>f. f = (\<lambda>x. x) \<and> f y \<noteq> y"
nitpick [card = 1, expect = genuine]
-nitpick [card = 2, expect = genuine]
nitpick [card = 5, expect = genuine]
oops
@@ -112,8 +96,7 @@
oops
lemma "{(a\<Colon>'a\<times>'a, b\<Colon>'b)}^-1 = {(b, a)}"
-nitpick [card = 1\<midarrow>6, expect = none]
-nitpick [card = 20, expect = none]
+nitpick [card = 1\<midarrow>12, expect = none]
by auto
lemma "fst (a, b) = a"
@@ -121,7 +104,7 @@
by auto
lemma "\<exists>P. P = Id"
-nitpick [card = 1\<midarrow>4, expect = none]
+nitpick [card = 1\<midarrow>20, expect = none]
by auto
lemma "(a\<Colon>'a\<Rightarrow>'b, a) \<in> Id\<^sup>*"
@@ -129,11 +112,11 @@
by auto
lemma "(a\<Colon>'a\<times>'a, a) \<in> Id\<^sup>* \<union> {(a, b)}\<^sup>*"
-nitpick [card = 1\<midarrow>6, expect = none]
+nitpick [card = 1\<midarrow>4, expect = none]
by auto
lemma "Id (a, a)"
-nitpick [card = 1\<midarrow>100, expect = none]
+nitpick [card = 1\<midarrow>50, expect = none]
by (auto simp: Id_def Collect_def)
lemma "Id ((a\<Colon>'a, b\<Colon>'a), (a, b))"
@@ -151,7 +134,7 @@
lemma "g = Let (A \<or> B)"
nitpick [card = 1, expect = none]
nitpick [card = 2, expect = genuine]
-nitpick [card = 20, expect = genuine]
+nitpick [card = 12, expect = genuine]
oops
lemma "(let a_or_b = A \<or> B in a_or_b \<or> \<not> a_or_b)"
@@ -172,37 +155,30 @@
lemma "(a\<Colon>'a\<times>'a, a\<Colon>'a\<times>'a) \<in> R"
nitpick [card = 1, expect = genuine]
-nitpick [card = 2, expect = genuine]
-nitpick [card = 4, expect = genuine]
nitpick [card = 20, expect = genuine]
-nitpick [card = 10, dont_box, expect = genuine]
+nitpick [card = 5, dont_box, expect = genuine]
oops
lemma "f (g\<Colon>'a\<Rightarrow>'a) = x"
nitpick [card = 3, expect = genuine]
nitpick [card = 3, dont_box, expect = genuine]
-nitpick [card = 5, expect = genuine]
nitpick [card = 10, expect = genuine]
oops
lemma "f (a, b) = x"
-nitpick [card = 3, expect = genuine]
-nitpick [card = 10, expect = genuine]
-nitpick [card = 16, expect = genuine]
-nitpick [card = 30, expect = genuine]
+nitpick [card = 12, expect = genuine]
oops
lemma "f (a, a) = f (c, d)"
-nitpick [card = 4, expect = genuine]
-nitpick [card = 20, expect = genuine]
+nitpick [card = 12, expect = genuine]
oops
lemma "(x\<Colon>'a) = (\<lambda>a. \<lambda>b. \<lambda>c. if c then a else b) x x True"
-nitpick [card = 2, expect = none]
+nitpick [card = 1\<midarrow>12, expect = none]
by auto
lemma "\<exists>F. F a b = G a b"
-nitpick [card = 3, expect = none]
+nitpick [card = 2, expect = none]
by auto
lemma "f = split"
@@ -216,12 +192,10 @@
lemma "(A, B) \<in> R \<or> (\<exists>C. (A, C) \<in> R \<and> (C, B) \<in> R) \<Longrightarrow>
A = B \<or> (A, B) \<in> R \<or> (\<exists>C. (A, C) \<in> R \<and> (C, B) \<in> R)"
-nitpick [card = 1\<midarrow>50, expect = none]
+nitpick [card = 1\<midarrow>25, expect = none]
by auto
lemma "f = (\<lambda>x\<Colon>'a\<times>'b. x)"
-nitpick [card = 3, expect = genuine]
-nitpick [card = 4, expect = genuine]
nitpick [card = 8, expect = genuine]
oops
@@ -230,30 +204,26 @@
lemma "x = y"
nitpick [card 'a = 1, expect = none]
nitpick [card 'a = 2, expect = genuine]
-nitpick [card 'a = 100, expect = genuine]
-nitpick [card 'a = 1000, expect = genuine]
+nitpick [card 'a = 200, expect = genuine]
oops
lemma "\<forall>x. x = y"
nitpick [card 'a = 1, expect = none]
nitpick [card 'a = 2, expect = genuine]
-nitpick [card 'a = 100, expect = genuine]
-nitpick [card 'a = 1000, expect = genuine]
+nitpick [card 'a = 200, expect = genuine]
oops
lemma "\<forall>x\<Colon>'a \<Rightarrow> bool. x = y"
nitpick [card 'a = 1, expect = genuine]
-nitpick [card 'a = 2, expect = genuine]
-nitpick [card 'a = 100, expect = genuine]
-nitpick [card 'a = 1000, expect = genuine]
+nitpick [card 'a = 200, expect = genuine]
oops
lemma "\<exists>x\<Colon>'a \<Rightarrow> bool. x = y"
-nitpick [card 'a = 1\<midarrow>10, expect = none]
+nitpick [card 'a = 1\<midarrow>20, expect = none]
by auto
lemma "\<exists>x y\<Colon>'a \<Rightarrow> bool. x = y"
-nitpick [card = 1\<midarrow>40, expect = none]
+nitpick [card = 1\<midarrow>20, expect = none]
by auto
lemma "\<forall>x. \<exists>y. f x y = f x (g x)"
@@ -261,11 +231,10 @@
by auto
lemma "\<forall>u. \<exists>v. \<forall>w. \<exists>x. f u v w x = f u (g u) w (h u w)"
-nitpick [card = 1\<midarrow>5, expect = none]
+nitpick [card = 1\<midarrow>4, expect = none]
by auto
lemma "\<forall>u. \<exists>v. \<forall>w. \<exists>x. f u v w x = f u (g u w) w (h u)"
-nitpick [card = 1\<midarrow>2, expect = genuine]
nitpick [card = 3, expect = genuine]
oops
@@ -273,7 +242,6 @@
f u v w x y z = f u (g u) w (h u w) y (k u w y)"
nitpick [card = 1\<midarrow>2, expect = none]
nitpick [card = 3, expect = none]
-nitpick [card = 4, expect = none]
sorry
lemma "\<forall>u. \<exists>v. \<forall>w. \<exists>x. \<forall>y. \<exists>z.
@@ -334,9 +302,6 @@
lemma "(\<exists>x\<Colon>'a. \<forall>y. P x y) \<or> (\<exists>x\<Colon>'a \<times> 'a. \<forall>y. P y x)"
nitpick [card 'a = 1, expect = genuine]
-nitpick [card 'a = 2, expect = genuine]
-nitpick [card 'a = 3, expect = genuine]
-nitpick [card 'a = 4, expect = genuine]
nitpick [card 'a = 5, expect = genuine]
oops
@@ -390,8 +355,7 @@
nitpick [card = 1, expect = genuine]
nitpick [card = 1, box "('a \<Rightarrow> prop) \<Rightarrow> prop", expect = genuine]
nitpick [card = 2, expect = genuine]
-nitpick [card = 8, expect = genuine]
-nitpick [card = 10, expect = unknown]
+nitpick [card = 6, expect = genuine]
oops
lemma "\<And>x. f x y = f x y"
@@ -416,11 +380,7 @@
lemma "x \<equiv> (op \<equiv>) \<Longrightarrow> False"
nitpick [card = 1, expect = genuine]
-nitpick [card = 2, expect = genuine]
-nitpick [card = 3, expect = genuine]
-nitpick [card = 4, expect = genuine]
-nitpick [card = 5, expect = genuine]
-nitpick [card = 100, expect = genuine]
+nitpick [card = 20, expect = genuine]
oops
lemma "I = (\<lambda>x. x) \<Longrightarrow> (op \<equiv> x) \<equiv> (\<lambda>y. (x \<equiv> I y))"
@@ -529,7 +489,7 @@
lemma "x = Ex \<Longrightarrow> False"
nitpick [card = 1, dont_box, expect = genuine]
nitpick [card = 2, dont_box, expect = genuine]
-nitpick [card = 8, dont_box, expect = genuine]
+nitpick [card = 6, dont_box, expect = genuine]
nitpick [card = 10, dont_box, expect = unknown]
oops
@@ -582,8 +542,8 @@
nitpick [expect = none]
by auto
-lemma "I = (\<lambda>x. x) \<Longrightarrow> (op &) = (\<lambda>x. op & (I x))"
- "I = (\<lambda>x. x) \<Longrightarrow> (op &) = (\<lambda>x y. x & (I y))"
+lemma "I = (\<lambda>x. x) \<Longrightarrow> (op \<and>) = (\<lambda>x. op \<and> (I x))"
+ "I = (\<lambda>x. x) \<Longrightarrow> (op \<and>) = (\<lambda>x y. x \<and> (I y))"
nitpick [expect = none]
by auto
@@ -796,7 +756,7 @@
by auto
lemma "((x, x), (x, x)) \<in> rtrancl {}"
-nitpick [expect = none]
+nitpick [card = 1\<midarrow>5, expect = none]
by auto
lemma "I = (\<lambda>x. x) \<Longrightarrow> op \<union> = (\<lambda>x. op \<union> (I x))"
@@ -931,9 +891,8 @@
oops
lemma "P x \<Longrightarrow> P (The P)"
-nitpick [card = 1, expect = none]
nitpick [card = 1\<midarrow>2, expect = none]
-nitpick [card = 3\<midarrow>5, expect = genuine]
+nitpick [card = 3, expect = genuine]
nitpick [card = 8, expect = genuine]
oops
--- a/src/HOL/Nitpick_Examples/Datatype_Nits.thy Mon Feb 22 14:36:10 2010 +0100
+++ b/src/HOL/Nitpick_Examples/Datatype_Nits.thy Mon Feb 22 19:31:00 2010 +0100
@@ -11,7 +11,8 @@
imports Main
begin
-nitpick_params [sat_solver = MiniSat_JNI, max_threads = 1, timeout = 60 s]
+nitpick_params [max_potential = 0, sat_solver = MiniSat_JNI, max_threads = 1,
+ timeout = 60 s]
primrec rot where
"rot Nibble0 = Nibble1" | "rot Nibble1 = Nibble2" | "rot Nibble2 = Nibble3" |
@@ -27,9 +28,8 @@
lemma "rot Nibble2 \<noteq> Nibble3"
nitpick [card = 1, expect = none]
-nitpick [card = 2, expect = genuine]
+nitpick [card = 2, max Nibble4 = 0, expect = genuine]
nitpick [card = 2, max Nibble2 = 0, expect = none]
-nitpick [card = 2, max Nibble3 = 0, expect = none]
oops
lemma "(rot ^^ 15) n \<noteq> n"
@@ -53,7 +53,7 @@
"sn (Pd (_, b)) = b"
lemma "fs (Pd p) = fst p"
-nitpick [card = 20, expect = none]
+nitpick [card = 12, expect = none]
sorry
lemma "fs (Pd p) = snd p"
@@ -61,7 +61,7 @@
oops
lemma "sn (Pd p) = snd p"
-nitpick [card = 20, expect = none]
+nitpick [card = 12, expect = none]
sorry
lemma "sn (Pd p) = fst p"
@@ -69,7 +69,7 @@
oops
lemma "fs (Pd ((a, b), (c, d))) = (a, b)"
-nitpick [card = 1\<midarrow>12, expect = none]
+nitpick [card = 1\<midarrow>10, expect = none]
sorry
lemma "fs (Pd ((a, b), (c, d))) = (c, d)"
@@ -82,7 +82,7 @@
"app (Fn f) x = f x"
lemma "app (Fn g) y = g y"
-nitpick [card = 1\<midarrow>12, expect = none]
+nitpick [card = 1\<midarrow>10, expect = none]
sorry
lemma "app (Fn g) y = g' y"
--- a/src/HOL/Nitpick_Examples/Hotel_Nits.thy Mon Feb 22 14:36:10 2010 +0100
+++ b/src/HOL/Nitpick_Examples/Hotel_Nits.thy Mon Feb 22 19:31:00 2010 +0100
@@ -12,7 +12,8 @@
imports Main
begin
-nitpick_params [sat_solver = MiniSat_JNI, max_threads = 1, timeout = 120 s]
+nitpick_params [max_potential = 0, sat_solver = MiniSat_JNI, max_threads = 1,
+ timeout = 120 s]
typedecl guest
typedecl key
--- a/src/HOL/Nitpick_Examples/Manual_Nits.thy Mon Feb 22 14:36:10 2010 +0100
+++ b/src/HOL/Nitpick_Examples/Manual_Nits.thy Mon Feb 22 19:31:00 2010 +0100
@@ -8,7 +8,7 @@
header {* Examples from the Nitpick Manual *}
theory Manual_Nits
-imports Main Coinductive_List RealDef
+imports Main Coinductive_List Quotient_Product RealDef
begin
chapter {* 3. First Steps *}
@@ -102,6 +102,21 @@
nitpick [show_datatypes]
oops
+fun my_int_rel where
+"my_int_rel (x, y) (u, v) = (x + v = u + y)"
+
+quotient_type my_int = "nat \<times> nat" / my_int_rel
+by (auto simp add: equivp_def expand_fun_eq)
+
+definition add_raw where
+"add_raw \<equiv> \<lambda>(x, y) (u, v). (x + (u\<Colon>nat), y + (v\<Colon>nat))"
+
+quotient_definition "add\<Colon>my_int \<Rightarrow> my_int \<Rightarrow> my_int" is add_raw
+
+lemma "add x y = add x x"
+nitpick [show_datatypes]
+oops
+
record point =
Xcoord :: int
Ycoord :: int
--- a/src/HOL/Nitpick_Examples/Mini_Nits.thy Mon Feb 22 14:36:10 2010 +0100
+++ b/src/HOL/Nitpick_Examples/Mini_Nits.thy Mon Feb 22 19:31:00 2010 +0100
@@ -15,11 +15,9 @@
exception FAIL
(* int -> term -> string *)
-fun minipick 0 _ = "none"
- | minipick n t =
- case minipick (n - 1) t of
- "none" => Minipick.pick_nits_in_term @{context} (K n) t
- | outcome_code => outcome_code
+fun minipick n t =
+ map (fn k => Minipick.kodkod_problem_from_term @{context} (K k) t) (1 upto n)
+ |> Minipick.solve_any_kodkod_problem @{theory}
(* int -> term -> bool *)
fun none n t = (minipick n t = "none" orelse raise FAIL)
fun genuine n t = (minipick n t = "genuine" orelse raise FAIL)
@@ -87,11 +85,11 @@
ML {* genuine 2 @{prop "(a\<Colon>'a \<times> 'a \<times> 'a, b) \<noteq> (b, a)"} *}
ML {* none 5 @{prop "\<exists>a b\<Colon>'a \<Rightarrow> 'a. (a, b) = (b, a)"} *}
ML {* genuine 1 @{prop "(a\<Colon>'a \<Rightarrow> 'a, b) \<noteq> (b, a)"} *}
-ML {* none 8 @{prop "fst (a, b) = a"} *}
+ML {* none 5 @{prop "fst (a, b) = a"} *}
ML {* none 1 @{prop "fst (a, b) = b"} *}
ML {* genuine 2 @{prop "fst (a, b) = b"} *}
ML {* genuine 2 @{prop "fst (a, b) \<noteq> b"} *}
-ML {* none 8 @{prop "snd (a, b) = b"} *}
+ML {* none 5 @{prop "snd (a, b) = b"} *}
ML {* none 1 @{prop "snd (a, b) = a"} *}
ML {* genuine 2 @{prop "snd (a, b) = a"} *}
ML {* genuine 2 @{prop "snd (a, b) \<noteq> a"} *}
--- a/src/HOL/Nitpick_Examples/Pattern_Nits.thy Mon Feb 22 14:36:10 2010 +0100
+++ b/src/HOL/Nitpick_Examples/Pattern_Nits.thy Mon Feb 22 19:31:00 2010 +0100
@@ -11,8 +11,8 @@
imports Main
begin
-nitpick_params [sat_solver = MiniSat_JNI, max_threads = 1, timeout = 60 s,
- card = 14]
+nitpick_params [card = 10, max_potential = 0, sat_solver = MiniSat_JNI,
+ max_threads = 1, timeout = 60 s]
lemma "x = (case u of () \<Rightarrow> y)"
nitpick [expect = genuine]
@@ -132,7 +132,7 @@
nitpick [expect = genuine]
oops
-lemma "\<exists>y a b zs. x = (y # Some (a, b) # zs)"
+lemma "\<exists>y a b zs. x = y # Some (a, b) # zs"
nitpick [expect = genuine]
oops
--- a/src/HOL/Nitpick_Examples/Record_Nits.thy Mon Feb 22 14:36:10 2010 +0100
+++ b/src/HOL/Nitpick_Examples/Record_Nits.thy Mon Feb 22 19:31:00 2010 +0100
@@ -11,7 +11,8 @@
imports Main
begin
-nitpick_params [sat_solver = MiniSat_JNI, max_threads = 1, timeout = 60 s]
+nitpick_params [max_potential = 0, sat_solver = MiniSat_JNI, max_threads = 1,
+ timeout = 60 s]
record point2d =
xc :: int
--- a/src/HOL/Nitpick_Examples/Refute_Nits.thy Mon Feb 22 14:36:10 2010 +0100
+++ b/src/HOL/Nitpick_Examples/Refute_Nits.thy Mon Feb 22 19:31:00 2010 +0100
@@ -11,7 +11,8 @@
imports Main
begin
-nitpick_params [sat_solver = MiniSat_JNI, max_threads = 1, timeout = 60 s]
+nitpick_params [max_potential = 0, sat_solver = MiniSat_JNI, max_threads = 1,
+ timeout = 60 s]
lemma "P \<and> Q"
apply (rule conjI)
@@ -174,14 +175,14 @@
nitpick [expect = genuine]
oops
-text {* The "Drinker's theorem" ... *}
+text {* The ``Drinker's theorem'' *}
lemma "\<exists>x. f x = g x \<longrightarrow> f = g"
nitpick [expect = none]
apply (auto simp add: ext)
done
-text {* ... and an incorrect version of it *}
+text {* And an incorrect version of it *}
lemma "(\<exists>x. f x = g x) \<longrightarrow> f = g"
nitpick [expect = genuine]
@@ -241,7 +242,7 @@
nitpick [expect = genuine]
oops
-text {* "The transitive closure 'T' of an arbitrary relation 'P' is non-empty." *}
+text {* ``The transitive closure of an arbitrary relation is non-empty.'' *}
constdefs
"trans" :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool"
@@ -255,7 +256,7 @@
nitpick [expect = genuine]
oops
-text {* "The union of transitive closures is equal to the transitive closure of unions." *}
+text {* ``The union of transitive closures is equal to the transitive closure of unions.'' *}
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)
\<longrightarrow> trans_closure TP P
@@ -264,19 +265,19 @@
nitpick [expect = genuine]
oops
-text {* "Every surjective function is invertible." *}
+text {* ``Every surjective function is invertible.'' *}
lemma "(\<forall>y. \<exists>x. y = f x) \<longrightarrow> (\<exists>g. \<forall>x. g (f x) = x)"
nitpick [expect = genuine]
oops
-text {* "Every invertible function is surjective." *}
+text {* ``Every invertible function is surjective.'' *}
lemma "(\<exists>g. \<forall>x. g (f x) = x) \<longrightarrow> (\<forall>y. \<exists>x. y = f x)"
nitpick [expect = genuine]
oops
-text {* Every point is a fixed point of some function. *}
+text {* ``Every point is a fixed point of some function.'' *}
lemma "\<exists>f. f x = x"
nitpick [card = 1\<midarrow>7, expect = none]
@@ -284,21 +285,21 @@
apply simp
done
-text {* Axiom of Choice: first an incorrect version ... *}
+text {* Axiom of Choice: first an incorrect version *}
lemma "(\<forall>x. \<exists>y. P x y) \<longrightarrow> (\<exists>!f. \<forall>x. P x (f x))"
nitpick [expect = genuine]
oops
-text {* ... and now two correct ones *}
+text {* And now two correct ones *}
lemma "(\<forall>x. \<exists>y. P x y) \<longrightarrow> (\<exists>f. \<forall>x. P x (f x))"
-nitpick [card = 1-5, expect = none]
+nitpick [card = 1-4, expect = none]
apply (simp add: choice)
done
lemma "(\<forall>x. \<exists>!y. P x y) \<longrightarrow> (\<exists>!f. \<forall>x. P x (f x))"
-nitpick [card = 1-4, expect = none]
+nitpick [card = 1-3, expect = none]
apply auto
apply (simp add: ex1_implies_ex choice)
apply (fast intro: ext)
@@ -807,12 +808,12 @@
oops
lemma "list_rec nil cons [] = nil"
-nitpick [expect = none]
+nitpick [card = 1\<midarrow>5, expect = none]
apply simp
done
lemma "list_rec nil cons (x#xs) = cons x xs (list_rec nil cons xs)"
-nitpick [expect = none]
+nitpick [card = 1\<midarrow>5, expect = none]
apply simp
done
@@ -923,12 +924,12 @@
oops
lemma "aexp_bexp_rec_1 number ite equal (Number x) = number x"
-nitpick [card = 1\<midarrow>4, expect = none]
+nitpick [card = 1\<midarrow>3, expect = none]
apply simp
done
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)"
-nitpick [card = 1\<midarrow>4, expect = none]
+nitpick [card = 1\<midarrow>3, expect = none]
apply simp
done
@@ -941,7 +942,7 @@
oops
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)"
-nitpick [card = 1\<midarrow>4, expect = none]
+nitpick [card = 1\<midarrow>3, expect = none]
apply simp
done
@@ -1001,32 +1002,32 @@
oops
lemma "X_Y_rec_1 a b c d e f A = a"
-nitpick [expect = none]
+nitpick [card = 1\<midarrow>5, expect = none]
apply simp
done
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)"
-nitpick [expect = none]
+nitpick [card = 1\<midarrow>5, expect = none]
apply simp
done
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)"
-nitpick [expect = none]
+nitpick [card = 1\<midarrow>5, expect = none]
apply simp
done
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)"
-nitpick [expect = none]
+nitpick [card = 1\<midarrow>5, expect = none]
apply simp
done
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)"
-nitpick [expect = none]
+nitpick [card = 1\<midarrow>5, expect = none]
apply simp
done
lemma "X_Y_rec_2 a b c d e f F = f"
-nitpick [expect = none]
+nitpick [card = 1\<midarrow>5, expect = none]
apply simp
done
@@ -1057,12 +1058,12 @@
oops
lemma "XOpt_rec_1 cx dx n1 s1 n2 s2 (CX x) = cx x (XOpt_rec_2 cx dx n1 s1 n2 s2 x)"
-nitpick [card = 1\<midarrow>6, expect = none]
+nitpick [card = 1\<midarrow>5, expect = none]
apply simp
done
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))"
-nitpick [card = 1\<midarrow>4, expect = none]
+nitpick [card = 1\<midarrow>3, expect = none]
apply simp
done
@@ -1150,17 +1151,17 @@
oops
lemma "Trie_rec_1 tr nil cons (TR x) = tr x (Trie_rec_2 tr nil cons x)"
-nitpick [card = 1\<midarrow>6, expect = none]
+nitpick [card = 1\<midarrow>4, expect = none]
apply simp
done
lemma "Trie_rec_2 tr nil cons [] = nil"
-nitpick [card = 1\<midarrow>6, expect = none]
+nitpick [card = 1\<midarrow>4, expect = none]
apply simp
done
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)"
-nitpick [card = 1\<midarrow>6, expect = none]
+nitpick [card = 1\<midarrow>4, expect = none]
apply simp
done
@@ -1365,15 +1366,15 @@
oops
lemma "f (lfp f) = lfp f"
-nitpick [expect = genuine]
+nitpick [card = 2, expect = genuine]
oops
lemma "f (gfp f) = gfp f"
-nitpick [expect = genuine]
+nitpick [card = 2, expect = genuine]
oops
lemma "lfp f = gfp f"
-nitpick [expect = genuine]
+nitpick [card = 2, expect = genuine]
oops
subsubsection {* Axiomatic Type Classes and Overloading *}
--- a/src/HOL/Nitpick_Examples/Special_Nits.thy Mon Feb 22 14:36:10 2010 +0100
+++ b/src/HOL/Nitpick_Examples/Special_Nits.thy Mon Feb 22 19:31:00 2010 +0100
@@ -11,8 +11,8 @@
imports Main
begin
-nitpick_params [sat_solver = MiniSat_JNI, max_threads = 1, timeout = 60 s,
- card = 4]
+nitpick_params [card = 4, sat_solver = MiniSat_JNI, max_threads = 1,
+ timeout = 60 s]
fun f1 :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat" where
"f1 a b c d e = a + b + c + d + e"
--- a/src/HOL/Nitpick_Examples/Typedef_Nits.thy Mon Feb 22 14:36:10 2010 +0100
+++ b/src/HOL/Nitpick_Examples/Typedef_Nits.thy Mon Feb 22 19:31:00 2010 +0100
@@ -11,8 +11,8 @@
imports Main Rational
begin
-nitpick_params [sat_solver = MiniSat_JNI, max_threads = 1, timeout = 60 s,
- card = 1\<midarrow>4]
+nitpick_params [card = 1\<midarrow>4, sat_solver = MiniSat_JNI, max_threads = 1,
+ timeout = 60 s]
typedef three = "{0\<Colon>nat, 1, 2}"
by blast
@@ -138,7 +138,8 @@
by (rule Inl_Rep_not_Inr_Rep)
lemma "Abs_Sum (Rep_Sum a) = a"
-nitpick [card = 1\<midarrow>2, timeout = 60 s, expect = none]
+nitpick [card = 1, expect = none]
+nitpick [card = 2, expect = none]
by (rule Rep_Sum_inverse)
lemma "0::nat \<equiv> Abs_Nat Zero_Rep"
--- a/src/HOL/Tools/Nitpick/minipick.ML Mon Feb 22 14:36:10 2010 +0100
+++ b/src/HOL/Tools/Nitpick/minipick.ML Mon Feb 22 19:31:00 2010 +0100
@@ -19,7 +19,9 @@
val true_atom : Kodkod.rel_expr
val formula_from_atom : Kodkod.rel_expr -> Kodkod.formula
val atom_from_formula : Kodkod.formula -> Kodkod.rel_expr
- val pick_nits_in_term : Proof.context -> (typ -> int) -> term -> string
+ val kodkod_problem_from_term :
+ Proof.context -> (typ -> int) -> term -> Kodkod.problem
+ val solve_any_kodkod_problem : theory -> Kodkod.problem list -> string
end;
structure Minipick : MINIPICK =
@@ -287,11 +289,10 @@
fun declarative_axiom_for_free card i (_, T) =
declarative_axiom_for_rel_expr card [] T (Rel (arity_of RRep card T, i))
-(* Proof.context -> (typ -> int) -> term -> string *)
-fun pick_nits_in_term ctxt raw_card t =
+(* Proof.context -> (typ -> int) -> term -> problem *)
+fun kodkod_problem_from_term ctxt raw_card t =
let
val thy = ProofContext.theory_of ctxt
- val {overlord, ...} = Nitpick_Isar.default_params thy []
(* typ -> int *)
fun card (Type ("fun", [T1, T2])) = reasonable_power (card T2) (card T1)
| card (Type ("*", [T1, T2])) = card T1 * card T2
@@ -306,11 +307,19 @@
val formula = kodkod_formula_from_term ctxt card frees neg_t
|> fold_rev (curry And) declarative_axioms
val univ_card = univ_card 0 0 0 bounds formula
- val problem =
- {comment = "", settings = [], univ_card = univ_card, tuple_assigns = [],
- bounds = bounds, int_bounds = [], expr_assigns = [], formula = formula}
in
- case solve_any_problem overlord NONE 0 1 [problem] of
+ {comment = "", settings = [], univ_card = univ_card, tuple_assigns = [],
+ bounds = bounds, int_bounds = [], expr_assigns = [], formula = formula}
+ end
+
+(* theory -> problem list -> string *)
+fun solve_any_kodkod_problem thy problems =
+ let
+ val {overlord, ...} = Nitpick_Isar.default_params thy []
+ val max_threads = 1
+ val max_solutions = 1
+ in
+ case solve_any_problem overlord NONE max_threads max_solutions problems of
NotInstalled => "unknown"
| Normal ([], _) => "none"
| Normal _ => "genuine"
@@ -318,7 +327,5 @@
| Interrupted _ => "unknown"
| Error (s, _) => error ("Kodkod error: " ^ s)
end
- handle NOT_SUPPORTED details =>
- (warning ("Unsupported case: " ^ details ^ "."); "unknown")
end;
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Mon Feb 22 14:36:10 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Mon Feb 22 19:31:00 2010 +0100
@@ -597,8 +597,8 @@
fun unregister_codatatype co_T = register_codatatype co_T "" []
(* theory -> typ -> bool *)
-fun is_quot_type _ (Type ("IntEx.my_int", _)) = true (* FIXME *)
- | is_quot_type _ (Type ("FSet.fset", _)) = true
+fun is_quot_type thy (Type (s, _)) =
+ is_some (Quotient_Info.quotdata_lookup_raw thy s)
| is_quot_type _ _ = false
fun is_codatatype thy (Type (s, _)) =
not (null (AList.lookup (op =) (#codatatypes (Data.get thy)) s
@@ -666,11 +666,13 @@
| NONE => false)
| is_rep_fun _ _ = false
(* Proof.context -> styp -> bool *)
-fun is_quot_abs_fun _ ("IntEx.abs_my_int", _) = true
- | is_quot_abs_fun _ ("FSet.abs_fset", _) = true
+fun is_quot_abs_fun ctxt (x as (_, Type ("fun", [_, Type (s', _)]))) =
+ (try (Quotient_Term.absrep_const_chk Quotient_Term.AbsF ctxt) s'
+ = SOME (Const x))
| is_quot_abs_fun _ _ = false
-fun is_quot_rep_fun _ ("IntEx.rep_my_int", _) = true
- | is_quot_rep_fun _ ("FSet.rep_fset", _) = true
+fun is_quot_rep_fun ctxt (x as (_, Type ("fun", [Type (s', _), _]))) =
+ (try (Quotient_Term.absrep_const_chk Quotient_Term.RepF ctxt) s'
+ = SOME (Const x))
| is_quot_rep_fun _ _ = false
(* theory -> styp -> styp *)
@@ -680,18 +682,16 @@
| NONE => raise TERM ("Nitpick_HOL.mate_of_rep_fun", [Const x]))
| mate_of_rep_fun _ x = raise TERM ("Nitpick_HOL.mate_of_rep_fun", [Const x])
(* theory -> typ -> typ *)
-fun rep_type_for_quot_type _ (Type ("IntEx.my_int", [])) = @{typ "nat * nat"}
- | rep_type_for_quot_type _ (Type ("FSet.fset", [T])) =
- Type (@{type_name list}, [T])
- | rep_type_for_quot_type _ T =
- raise TYPE ("Nitpick_HOL.rep_type_for_quot_type", [T], [])
+fun rep_type_for_quot_type thy (T as Type (s, _)) =
+ let val {qtyp, rtyp, ...} = Quotient_Info.quotdata_lookup thy s in
+ instantiate_type thy qtyp T rtyp
+ end
(* theory -> typ -> term *)
-fun equiv_relation_for_quot_type _ (Type ("IntEx.my_int", [])) =
- Const ("IntEx.intrel", @{typ "(nat * nat) => (nat * nat) => bool"})
- | equiv_relation_for_quot_type _ (Type ("FSet.fset", [T])) =
- Const ("FSet.list_eq",
- Type (@{type_name list}, [T]) --> Type (@{type_name list}, [T])
- --> bool_T)
+fun equiv_relation_for_quot_type thy (Type (s, Ts)) =
+ let
+ val {qtyp, equiv_rel, ...} = Quotient_Info.quotdata_lookup thy s
+ val Ts' = qtyp |> dest_Type |> snd
+ in subst_atomic_types (Ts' ~~ Ts) equiv_rel end
| equiv_relation_for_quot_type _ T =
raise TYPE ("Nitpick_HOL.equiv_relation_for_quot_type", [T], [])
@@ -1547,7 +1547,7 @@
val unfold_max_depth = 255
(* hol_context -> term -> term *)
-fun unfold_defs_in_term (hol_ctxt as {thy, stds, fast_descrs, case_names,
+fun unfold_defs_in_term (hol_ctxt as {thy, ctxt, stds, fast_descrs, case_names,
def_table, ground_thm_table, ersatz_table,
...}) =
let
@@ -1632,7 +1632,7 @@
else if is_stale_constr thy x then
raise NOT_SUPPORTED ("(non-co)constructors of codatatypes \
\(\"" ^ s ^ "\")")
- else if is_quot_abs_fun thy x then
+ else if is_quot_abs_fun ctxt x then
let
val rep_T = domain_type T
val abs_T = range_type T
@@ -1642,7 +1642,7 @@
$ (Const (@{const_name quot_normal},
rep_T --> rep_T) $ Bound 0)), ts)
end
- else if is_quot_rep_fun thy x then
+ else if is_quot_rep_fun ctxt x then
let
val abs_T = domain_type T
val rep_T = range_type T
--- a/src/HOL/Tools/Nitpick/nitpick_peephole.ML Mon Feb 22 14:36:10 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_peephole.ML Mon Feb 22 19:31:00 2010 +0100
@@ -340,24 +340,23 @@
else Project (r, is)
end
+ (* (rel_expr -> formula) -> rel_expr -> formula *)
+ fun s_xone xone r =
+ if is_one_rel_expr r then
+ True
+ else case arity_of_rel_expr r of
+ 1 => xone r
+ | arity => foldl1 And (map (xone o s_project r o single o Num)
+ (index_seq 0 arity))
(* rel_expr -> formula *)
fun s_no None = True
| s_no (Product (r1, r2)) = s_or (s_no r1) (s_no r2)
| s_no (Intersect (Closure (Rel x), Iden)) = Acyclic x
| s_no r = if is_one_rel_expr r then False else No r
fun s_lone None = True
- | s_lone r = if is_one_rel_expr r then True else Lone r
+ | s_lone r = s_xone Lone r
fun s_one None = False
- | s_one r =
- if is_one_rel_expr r then
- True
- else if inline_rel_expr r then
- case arity_of_rel_expr r of
- 1 => One r
- | arity => foldl1 And (map (One o s_project r o single o Num)
- (index_seq 0 arity))
- else
- One r
+ | s_one r = s_xone One r
fun s_some None = False
| s_some (Atom _) = True
| s_some (Product (r1, r2)) = s_and (s_some r1) (s_some r2)
--- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML Mon Feb 22 14:36:10 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML Mon Feb 22 19:31:00 2010 +0100
@@ -293,8 +293,8 @@
$ do_term new_Ts old_Ts polar t2
| Const (s as @{const_name The}, T) => do_description_operator s T
| Const (s as @{const_name Eps}, T) => do_description_operator s T
- | Const (@{const_name quot_normal}, Type ("fun", [_, T2])) =>
- let val T' = box_type hol_ctxt InSel T2 in
+ | Const (@{const_name quot_normal}, Type ("fun", [T, _])) =>
+ let val T' = box_type hol_ctxt InFunLHS T in
Const (@{const_name quot_normal}, T' --> T')
end
| Const (s as @{const_name Tha}, T) => do_description_operator s T
--- a/src/HOL/Tools/Nitpick/nitpick_tests.ML Mon Feb 22 14:36:10 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_tests.ML Mon Feb 22 19:31:00 2010 +0100
@@ -294,7 +294,8 @@
*)
]
-fun problem_for_nut ctxt name u =
+(* Proof.context -> string * nut -> Kodkod.problem *)
+fun problem_for_nut ctxt (name, u) =
let
val debug = false
val peephole_optim = true
@@ -320,15 +321,11 @@
formula = formula}
end
-(* string -> unit *)
-fun run_test name =
+(* unit -> unit *)
+fun run_all_tests () =
case Kodkod.solve_any_problem false NONE 0 1
- [problem_for_nut @{context} name
- (the (AList.lookup (op =) tests name))] of
+ (map (problem_for_nut @{context}) tests) of
Kodkod.Normal ([], _) => ()
- | _ => warning ("Test " ^ quote name ^ " failed")
-
-(* unit -> unit *)
-fun run_all_tests () = List.app run_test (map fst tests)
+ | _ => error "Tests failed"
end;