# HG changeset patch # User blanchet # Date 1266863478 -3600 # Node ID 40da65ef68e3e7b4a13aeccae0261f4b85a69bd7 # Parent 9edc2bd6d2bdc2aadccdc0185793776d3abdbc09# Parent 8fd9d555d04dbb2f0acfe8407c9593367ac061f8 merge diff -r 8fd9d555d04d -r 40da65ef68e3 doc-src/Nitpick/nitpick.tex --- a/doc-src/Nitpick/nitpick.tex Mon Feb 22 17:02:39 2010 +0100 +++ b/doc-src/Nitpick/nitpick.tex Mon Feb 22 19:31:18 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`\}. \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 diff -r 8fd9d555d04d -r 40da65ef68e3 src/HOL/Main.thy --- a/src/HOL/Main.thy Mon Feb 22 17:02:39 2010 +0100 +++ b/src/HOL/Main.thy Mon Feb 22 19:31:18 2010 +0100 @@ -1,7 +1,7 @@ header {* Main HOL *} theory Main -imports Plain Predicate_Compile Nitpick Quotient +imports Plain Predicate_Compile Nitpick begin text {* diff -r 8fd9d555d04d -r 40da65ef68e3 src/HOL/Nitpick.thy --- a/src/HOL/Nitpick.thy Mon Feb 22 17:02:39 2010 +0100 +++ b/src/HOL/Nitpick.thy Mon Feb 22 19:31:18 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") diff -r 8fd9d555d04d -r 40da65ef68e3 src/HOL/Nitpick_Examples/Core_Nits.thy --- a/src/HOL/Nitpick_Examples/Core_Nits.thy Mon Feb 22 17:02:39 2010 +0100 +++ b/src/HOL/Nitpick_Examples/Core_Nits.thy Mon Feb 22 19:31:18 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 "(\f x y. (curry o split) f x y) = (\f x y. (\x. x) f x y)" -nitpick [card = 1\4, expect = none] -nitpick [card = 100, expect = none, timeout = none] +nitpick [card = 1\12, expect = none] by auto lemma "(\f p. (split o curry) f p) = (\f p. (\x. x) f p)" -nitpick [card = 2] -nitpick [card = 1\4, expect = none] -nitpick [card = 10, expect = none] +nitpick [card = 1\12, expect = none] by auto lemma "split (curry f) = f" -nitpick [card = 1\4, expect = none] -nitpick [card = 10, expect = none] -nitpick [card = 40, expect = none] +nitpick [card = 1\12, expect = none] by auto lemma "curry (split f) = f" -nitpick [card = 1\4, expect = none] -nitpick [card = 40, expect = none] +nitpick [card = 1\12, expect = none] by auto lemma "(split o curry) f = f" -nitpick [card = 1\4, expect = none] -nitpick [card = 40, expect = none] +nitpick [card = 1\12, expect = none] by auto lemma "(curry o split) f = f" -nitpick [card = 1\4, expect = none] -nitpick [card = 1000, expect = none] +nitpick [card = 1\12, expect = none] by auto lemma "(split o curry) f = (\x. x) f" -nitpick [card = 1\4, expect = none] -nitpick [card = 40, expect = none] +nitpick [card = 1\12, expect = none] by auto lemma "(curry o split) f = (\x. x) f" -nitpick [card = 1\4, expect = none] -nitpick [card = 40, expect = none] +nitpick [card = 1\12, expect = none] by auto lemma "((split o curry) f) p = ((\x. x) f) p" -nitpick [card = 1\4, expect = none] -nitpick [card = 40, expect = none] +nitpick [card = 1\12, expect = none] by auto lemma "((curry o split) f) x = ((\x. x) f) x" -nitpick [card = 1\4, expect = none] -nitpick [card = 1000, expect = none] +nitpick [card = 1\12, expect = none] by auto lemma "((curry o split) f) x y = ((\x. x) f) x y" -nitpick [card = 1\4, expect = none] -nitpick [card = 1000, expect = none] +nitpick [card = 1\12, expect = none] by auto lemma "split o curry = (\x. x)" -nitpick [card = 1\4, expect = none] -nitpick [card = 40, expect = none] +nitpick [card = 1\12, expect = none] apply (rule ext)+ by auto lemma "curry o split = (\x. x)" -nitpick [card = 1\4, expect = none] -nitpick [card = 100, expect = none] +nitpick [card = 1\12, expect = none] apply (rule ext)+ by auto lemma "split (\x y. f (x, y)) = f" -nitpick [card = 1\4, expect = none] -nitpick [card = 40, expect = none] +nitpick [card = 1\12, expect = none] by auto subsection {* Representations *} @@ -96,13 +81,12 @@ by auto lemma "(\g. \x. g (f x) = x) \ (\y. \x. y = f x)" -nitpick [card 'a = 35, card 'b = 34, expect = genuine] -nitpick [card = 1\15, mono, expect = none] +nitpick [card 'a = 25, card 'b = 24, expect = genuine] +nitpick [card = 1\10, mono, expect = none] oops lemma "\f. f = (\x. x) \ f y \ y" nitpick [card = 1, expect = genuine] -nitpick [card = 2, expect = genuine] nitpick [card = 5, expect = genuine] oops @@ -112,8 +96,7 @@ oops lemma "{(a\'a\'a, b\'b)}^-1 = {(b, a)}" -nitpick [card = 1\6, expect = none] -nitpick [card = 20, expect = none] +nitpick [card = 1\12, expect = none] by auto lemma "fst (a, b) = a" @@ -121,7 +104,7 @@ by auto lemma "\P. P = Id" -nitpick [card = 1\4, expect = none] +nitpick [card = 1\20, expect = none] by auto lemma "(a\'a\'b, a) \ Id\<^sup>*" @@ -129,11 +112,11 @@ by auto lemma "(a\'a\'a, a) \ Id\<^sup>* \ {(a, b)}\<^sup>*" -nitpick [card = 1\6, expect = none] +nitpick [card = 1\4, expect = none] by auto lemma "Id (a, a)" -nitpick [card = 1\100, expect = none] +nitpick [card = 1\50, expect = none] by (auto simp: Id_def Collect_def) lemma "Id ((a\'a, b\'a), (a, b))" @@ -151,7 +134,7 @@ lemma "g = Let (A \ 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 \ B in a_or_b \ \ a_or_b)" @@ -172,37 +155,30 @@ lemma "(a\'a\'a, a\'a\'a) \ 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\'a\'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\'a) = (\a. \b. \c. if c then a else b) x x True" -nitpick [card = 2, expect = none] +nitpick [card = 1\12, expect = none] by auto lemma "\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) \ R \ (\C. (A, C) \ R \ (C, B) \ R) \ A = B \ (A, B) \ R \ (\C. (A, C) \ R \ (C, B) \ R)" -nitpick [card = 1\50, expect = none] +nitpick [card = 1\25, expect = none] by auto lemma "f = (\x\'a\'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 "\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 "\x\'a \ 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 "\x\'a \ bool. x = y" -nitpick [card 'a = 1\10, expect = none] +nitpick [card 'a = 1\20, expect = none] by auto lemma "\x y\'a \ bool. x = y" -nitpick [card = 1\40, expect = none] +nitpick [card = 1\20, expect = none] by auto lemma "\x. \y. f x y = f x (g x)" @@ -261,11 +231,10 @@ by auto lemma "\u. \v. \w. \x. f u v w x = f u (g u) w (h u w)" -nitpick [card = 1\5, expect = none] +nitpick [card = 1\4, expect = none] by auto lemma "\u. \v. \w. \x. f u v w x = f u (g u w) w (h u)" -nitpick [card = 1\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\2, expect = none] nitpick [card = 3, expect = none] -nitpick [card = 4, expect = none] sorry lemma "\u. \v. \w. \x. \y. \z. @@ -334,9 +302,6 @@ lemma "(\x\'a. \y. P x y) \ (\x\'a \ 'a. \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 \ prop) \ 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 "\x. f x y = f x y" @@ -416,11 +380,7 @@ lemma "x \ (op \) \ 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 = (\x. x) \ (op \ x) \ (\y. (x \ I y))" @@ -529,7 +489,7 @@ lemma "x = Ex \ 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 = (\x. x) \ (op &) = (\x. op & (I x))" - "I = (\x. x) \ (op &) = (\x y. x & (I y))" +lemma "I = (\x. x) \ (op \) = (\x. op \ (I x))" + "I = (\x. x) \ (op \) = (\x y. x \ (I y))" nitpick [expect = none] by auto @@ -796,7 +756,7 @@ by auto lemma "((x, x), (x, x)) \ rtrancl {}" -nitpick [expect = none] +nitpick [card = 1\5, expect = none] by auto lemma "I = (\x. x) \ op \ = (\x. op \ (I x))" @@ -931,9 +891,8 @@ oops lemma "P x \ P (The P)" -nitpick [card = 1, expect = none] nitpick [card = 1\2, expect = none] -nitpick [card = 3\5, expect = genuine] +nitpick [card = 3, expect = genuine] nitpick [card = 8, expect = genuine] oops diff -r 8fd9d555d04d -r 40da65ef68e3 src/HOL/Nitpick_Examples/Datatype_Nits.thy --- a/src/HOL/Nitpick_Examples/Datatype_Nits.thy Mon Feb 22 17:02:39 2010 +0100 +++ b/src/HOL/Nitpick_Examples/Datatype_Nits.thy Mon Feb 22 19:31:18 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 \ 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 \ 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\12, expect = none] +nitpick [card = 1\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\12, expect = none] +nitpick [card = 1\10, expect = none] sorry lemma "app (Fn g) y = g' y" diff -r 8fd9d555d04d -r 40da65ef68e3 src/HOL/Nitpick_Examples/Hotel_Nits.thy --- a/src/HOL/Nitpick_Examples/Hotel_Nits.thy Mon Feb 22 17:02:39 2010 +0100 +++ b/src/HOL/Nitpick_Examples/Hotel_Nits.thy Mon Feb 22 19:31:18 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 diff -r 8fd9d555d04d -r 40da65ef68e3 src/HOL/Nitpick_Examples/Manual_Nits.thy --- a/src/HOL/Nitpick_Examples/Manual_Nits.thy Mon Feb 22 17:02:39 2010 +0100 +++ b/src/HOL/Nitpick_Examples/Manual_Nits.thy Mon Feb 22 19:31:18 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 \ nat" / my_int_rel +by (auto simp add: equivp_def expand_fun_eq) + +definition add_raw where +"add_raw \ \(x, y) (u, v). (x + (u\nat), y + (v\nat))" + +quotient_definition "add\my_int \ my_int \ my_int" is add_raw + +lemma "add x y = add x x" +nitpick [show_datatypes] +oops + record point = Xcoord :: int Ycoord :: int diff -r 8fd9d555d04d -r 40da65ef68e3 src/HOL/Nitpick_Examples/Mini_Nits.thy --- a/src/HOL/Nitpick_Examples/Mini_Nits.thy Mon Feb 22 17:02:39 2010 +0100 +++ b/src/HOL/Nitpick_Examples/Mini_Nits.thy Mon Feb 22 19:31:18 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\'a \ 'a \ 'a, b) \ (b, a)"} *} ML {* none 5 @{prop "\a b\'a \ 'a. (a, b) = (b, a)"} *} ML {* genuine 1 @{prop "(a\'a \ 'a, b) \ (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) \ 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) \ a"} *} diff -r 8fd9d555d04d -r 40da65ef68e3 src/HOL/Nitpick_Examples/Pattern_Nits.thy --- a/src/HOL/Nitpick_Examples/Pattern_Nits.thy Mon Feb 22 17:02:39 2010 +0100 +++ b/src/HOL/Nitpick_Examples/Pattern_Nits.thy Mon Feb 22 19:31:18 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 () \ y)" nitpick [expect = genuine] @@ -132,7 +132,7 @@ nitpick [expect = genuine] oops -lemma "\y a b zs. x = (y # Some (a, b) # zs)" +lemma "\y a b zs. x = y # Some (a, b) # zs" nitpick [expect = genuine] oops diff -r 8fd9d555d04d -r 40da65ef68e3 src/HOL/Nitpick_Examples/Record_Nits.thy --- a/src/HOL/Nitpick_Examples/Record_Nits.thy Mon Feb 22 17:02:39 2010 +0100 +++ b/src/HOL/Nitpick_Examples/Record_Nits.thy Mon Feb 22 19:31:18 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 diff -r 8fd9d555d04d -r 40da65ef68e3 src/HOL/Nitpick_Examples/Refute_Nits.thy --- a/src/HOL/Nitpick_Examples/Refute_Nits.thy Mon Feb 22 17:02:39 2010 +0100 +++ b/src/HOL/Nitpick_Examples/Refute_Nits.thy Mon Feb 22 19:31:18 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 \ Q" apply (rule conjI) @@ -174,14 +175,14 @@ nitpick [expect = genuine] oops -text {* The "Drinker's theorem" ... *} +text {* The ``Drinker's theorem'' *} lemma "\x. f x = g x \ 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 "(\x. f x = g x) \ 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 \ 'a \ bool) \ 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 "(\x y. (P x y \ R x y) \ T x y) \ trans T \ (\Q. (\x y. (P x y \ R x y) \ Q x y) \ trans Q \ subset T Q) \ 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 "(\y. \x. y = f x) \ (\g. \x. g (f x) = x)" nitpick [expect = genuine] oops -text {* "Every invertible function is surjective." *} +text {* ``Every invertible function is surjective.'' *} lemma "(\g. \x. g (f x) = x) \ (\y. \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 "\f. f x = x" nitpick [card = 1\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 "(\x. \y. P x y) \ (\!f. \x. P x (f x))" nitpick [expect = genuine] oops -text {* ... and now two correct ones *} +text {* And now two correct ones *} lemma "(\x. \y. P x y) \ (\f. \x. P x (f x))" -nitpick [card = 1-5, expect = none] +nitpick [card = 1-4, expect = none] apply (simp add: choice) done lemma "(\x. \!y. P x y) \ (\!f. \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\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\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\4, expect = none] +nitpick [card = 1\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\4, expect = none] +nitpick [card = 1\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\4, expect = none] +nitpick [card = 1\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\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\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\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\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\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\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\6, expect = none] +nitpick [card = 1\5, expect = none] apply simp done lemma "XOpt_rec_1 cx dx n1 s1 n2 s2 (DX x) = dx x (\b. XOpt_rec_3 cx dx n1 s1 n2 s2 (x b))" -nitpick [card = 1\4, expect = none] +nitpick [card = 1\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\6, expect = none] +nitpick [card = 1\4, expect = none] apply simp done lemma "Trie_rec_2 tr nil cons [] = nil" -nitpick [card = 1\6, expect = none] +nitpick [card = 1\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\6, expect = none] +nitpick [card = 1\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 *} diff -r 8fd9d555d04d -r 40da65ef68e3 src/HOL/Nitpick_Examples/Special_Nits.thy --- a/src/HOL/Nitpick_Examples/Special_Nits.thy Mon Feb 22 17:02:39 2010 +0100 +++ b/src/HOL/Nitpick_Examples/Special_Nits.thy Mon Feb 22 19:31:18 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 \ nat \ nat \ nat \ nat \ nat" where "f1 a b c d e = a + b + c + d + e" diff -r 8fd9d555d04d -r 40da65ef68e3 src/HOL/Nitpick_Examples/Typedef_Nits.thy --- a/src/HOL/Nitpick_Examples/Typedef_Nits.thy Mon Feb 22 17:02:39 2010 +0100 +++ b/src/HOL/Nitpick_Examples/Typedef_Nits.thy Mon Feb 22 19:31:18 2010 +0100 @@ -11,8 +11,8 @@ imports Main Rational begin -nitpick_params [sat_solver = MiniSat_JNI, max_threads = 1, timeout = 60 s, - card = 1\4] +nitpick_params [card = 1\4, sat_solver = MiniSat_JNI, max_threads = 1, + timeout = 60 s] typedef three = "{0\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\2, timeout = 60 s, expect = none] +nitpick [card = 1, expect = none] +nitpick [card = 2, expect = none] by (rule Rep_Sum_inverse) lemma "0::nat \ Abs_Nat Zero_Rep" diff -r 8fd9d555d04d -r 40da65ef68e3 src/HOL/Tools/Nitpick/minipick.ML --- a/src/HOL/Tools/Nitpick/minipick.ML Mon Feb 22 17:02:39 2010 +0100 +++ b/src/HOL/Tools/Nitpick/minipick.ML Mon Feb 22 19:31:18 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; diff -r 8fd9d555d04d -r 40da65ef68e3 src/HOL/Tools/Nitpick/nitpick_hol.ML --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Mon Feb 22 17:02:39 2010 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Mon Feb 22 19:31:18 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], []) @@ -1143,6 +1143,8 @@ fun is_built_in_theory thy = Theory.subthy (thy, @{theory Refute}) (* term -> bool *) +val is_trivial_definition = + the_default false o try (op aconv o Logic.dest_equals) val is_plain_definition = let (* term -> bool *) @@ -1180,7 +1182,9 @@ val defs = (thy |> PureThy.all_thms_of |> filter (curry (op =) Thm.definitionK o Thm.get_kind o snd) - |> map (prop_of o snd) |> filter is_plain_definition) @ + |> map (prop_of o snd) + |> filter_out is_trivial_definition + |> filter is_plain_definition) @ user_defs @ built_in_defs in (defs, built_in_nondefs, user_nondefs) end @@ -1543,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 @@ -1628,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 @@ -1638,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 diff -r 8fd9d555d04d -r 40da65ef68e3 src/HOL/Tools/Nitpick/nitpick_peephole.ML --- a/src/HOL/Tools/Nitpick/nitpick_peephole.ML Mon Feb 22 17:02:39 2010 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_peephole.ML Mon Feb 22 19:31:18 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) diff -r 8fd9d555d04d -r 40da65ef68e3 src/HOL/Tools/Nitpick/nitpick_preproc.ML --- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML Mon Feb 22 17:02:39 2010 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML Mon Feb 22 19:31:18 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 diff -r 8fd9d555d04d -r 40da65ef68e3 src/HOL/Tools/Nitpick/nitpick_tests.ML --- a/src/HOL/Tools/Nitpick/nitpick_tests.ML Mon Feb 22 17:02:39 2010 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_tests.ML Mon Feb 22 19:31:18 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;