added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
--- a/doc-src/Nitpick/nitpick.tex Mon Feb 01 14:12:12 2010 +0100
+++ b/doc-src/Nitpick/nitpick.tex Tue Feb 02 11:38:38 2010 +0100
@@ -25,8 +25,8 @@
\def\lparr{\mathopen{(\mkern-4mu\mid}}
\def\rparr{\mathclose{\mid\mkern-4mu)}}
-\def\undef{\textit{undefined}}
\def\unk{{?}}
+\def\undef{(\lambda x.\; \unk)}
%\def\unr{\textit{others}}
\def\unr{\ldots}
\def\Abs#1{\hbox{\rm{\flqq}}{\,#1\,}\hbox{\rm{\frqq}}}
@@ -188,8 +188,8 @@
\prew
\textbf{apply}~\textit{auto} \\[2\smallskipamount]
{\slshape goal (2 subgoals): \\
-\ 1. $P\,\Longrightarrow\, Q$ \\
-\ 2. $Q\,\Longrightarrow\, P$} \\[2\smallskipamount]
+\phantom{0}1. $P\,\Longrightarrow\, Q$ \\
+\phantom{0}2. $Q\,\Longrightarrow\, P$} \\[2\smallskipamount]
\textbf{nitpick}~1 \\[2\smallskipamount]
{\slshape Nitpick found a counterexample: \\[2\smallskipamount]
\hbox{}\qquad Free variables: \nopagebreak \\
@@ -317,11 +317,9 @@
\postw
Notice that $\textit{The}~(\lambda y.\;P~y) = \textit{The}~\{a_2, a_3\} = a_1$,
-just like before.\footnote{The \undef{} symbol's presence is explained as
-follows: In higher-order logic, any function can be built from the undefined
-function using repeated applications of the function update operator $f(x :=
-y)$, just like any list can be built from the empty list using $x \mathbin{\#}
-xs$.}
+just like before.\footnote{The Isabelle/HOL notation $f(x :=
+y)$ denotes the function that maps $x$ to $y$ and that otherwise behaves like
+$f$.}
Our misadventures with THE suggest adding `$\exists!x{.}$' (``there exists a
unique $x$ such that'') at the front of our putative lemma's assumption:
@@ -562,7 +560,7 @@
{\slshape Datatype:} \\
\hbox{}\qquad $'a$~\textit{list}~= $\{[],\, [a_3, a_3],\, [a_3],\, \unr\}$ \\
{\slshape Constants:} \\
-\hbox{}\qquad $\lambda x_1.\; x_1 \mathbin{@} [y, y] = \undef([] := [a_3, a_3],\> [a_3, a_3] := \unk,\> [a_3] := \unk)$ \\
+\hbox{}\qquad $\lambda x_1.\; x_1 \mathbin{@} [y, y] = \undef([] := [a_3, a_3])$ \\
\hbox{}\qquad $\textit{hd} = \undef([] := a_2,\> [a_3, a_3] := a_3,\> [a_3] := a_3)$
\postw
@@ -1243,6 +1241,208 @@
\textit{int~list}, \textit{rat}, and \textit{rat~list} will lead Nitpick to
consider only 8~scopes instead of $32\,768$.
+\subsection{Inductive Properties}
+\label{inductive-properties}
+
+Inductive properties are a particular pain to prove, because the failure to
+establish an induction step can mean several things:
+%
+\begin{enumerate}
+\item The property is invalid.
+\item The property is valid but is too weak to support the induction step.
+\item The property is valid and strong enough; it's just that we haven't found
+the proof yet.
+\end{enumerate}
+%
+Depending on which scenario applies, we would take the appropriate course of
+action:
+%
+\begin{enumerate}
+\item Repair the statement of the property so that it becomes valid.
+\item Generalize the property and/or prove auxiliary properties.
+\item Work harder on a proof.
+\end{enumerate}
+%
+How can we distinguish between the three scenarios? Nitpick's normal mode of
+operation can often detect scenario 1, and Isabelle's automatic tactics help with
+scenario 3. Using appropriate techniques, it is also often possible to use
+Nitpick to identify scenario 2. Consider the following transition system,
+in which natural numbers represent states:
+
+\prew
+\textbf{inductive\_set}~\textit{reach}~\textbf{where} \\
+``$(4\Colon\textit{nat}) \in \textit{reach\/}$'' $\mid$ \\
+``$\lbrakk n < 4;\> n \in \textit{reach\/}\rbrakk \,\Longrightarrow\, 3 * n + 1 \in \textit{reach\/}$'' $\mid$ \\
+``$n \in \textit{reach} \,\Longrightarrow n + 2 \in \textit{reach\/}$''
+\postw
+
+We will try to prove that only even numbers are reachable:
+
+\prew
+\textbf{lemma}~``$n \in \textit{reach} \,\Longrightarrow\, 2~\textrm{dvd}~n$''
+\postw
+
+Does this property hold? Nitpick cannot find a counterexample within 30 seconds,
+so let's attempt a proof by induction:
+
+\prew
+\textbf{apply}~(\textit{induct~set}{:}~\textit{reach\/}) \\
+\textbf{apply}~\textit{auto}
+\postw
+
+This leaves us in the following proof state:
+
+\prew
+{\slshape goal (2 subgoals): \\
+\phantom{0}1. ${\bigwedge}n.\;\, \lbrakk n \in \textit{reach\/};\, n < 4;\, 2~\textsl{dvd}~n\rbrakk \,\Longrightarrow\, 2~\textsl{dvd}~\textit{Suc}~(3 * n)$ \\
+\phantom{0}2. ${\bigwedge}n.\;\, \lbrakk n \in \textit{reach\/};\, 2~\textsl{dvd}~n\rbrakk \,\Longrightarrow\, 2~\textsl{dvd}~\textit{Suc}~(\textit{Suc}~n)$
+}
+\postw
+
+If we run Nitpick on the first subgoal, it still won't find any
+counterexample; and yet, \textit{auto} fails to go further, and \textit{arith}
+is helpless. However, notice the $n \in \textit{reach}$ assumption, which
+strengthens the induction hypothesis but is not immediately usable in the proof.
+If we remove it and invoke Nitpick, this time we get a counterexample:
+
+\prew
+\textbf{apply}~(\textit{thin\_tac}~``$n \in \textit{reach\/}$'') \\
+\textbf{nitpick} \\[2\smallskipamount]
+\slshape Nitpick found a counterexample: \\[2\smallskipamount]
+\hbox{}\qquad Skolem constant: \nopagebreak \\
+\hbox{}\qquad\qquad $n = 0$
+\postw
+
+Indeed, 0 < 4, 2 divides 0, but 2 does not divide 1. We can use this information
+to strength the lemma:
+
+\prew
+\textbf{lemma}~``$n \in \textit{reach} \,\Longrightarrow\, 2~\textrm{dvd}~n \mathrel{\lor} n \not= 0$''
+\postw
+
+Unfortunately, the proof by induction still gets stuck, except that Nitpick now
+finds the counterexample $n = 2$. We generalize the lemma further to
+
+\prew
+\textbf{lemma}~``$n \in \textit{reach} \,\Longrightarrow\, 2~\textrm{dvd}~n \mathrel{\lor} n \ge 4$''
+\postw
+
+and this time \textit{arith} can finish off the subgoals.
+
+A similar technique can be employed for structural induction. The
+following mini-formalization of full binary trees will serve as illustration:
+
+\prew
+\textbf{datatype} $\kern1pt'a$~\textit{bin\_tree} = $\textit{Leaf}~{\kern1pt'a}$ $\mid$ $\textit{Branch}$ ``\kern1pt$'a$ \textit{bin\_tree}'' ``\kern1pt$'a$ \textit{bin\_tree}'' \\[2\smallskipamount]
+\textbf{primrec}~\textit{labels}~\textbf{where} \\
+``$\textit{labels}~(\textit{Leaf}~a) = \{a\}$'' $\mid$ \\
+``$\textit{labels}~(\textit{Branch}~t~u) = \textit{labels}~t \mathrel{\cup} \textit{labels}~u$'' \\[2\smallskipamount]
+\textbf{primrec}~\textit{swap}~\textbf{where} \\
+``$\textit{swap}~(\textit{Leaf}~c)~a~b =$ \\
+\phantom{``}$(\textrm{if}~c = a~\textrm{then}~\textit{Leaf}~b~\textrm{else~if}~c = b~\textrm{then}~\textit{Leaf}~a~\textrm{else}~\textit{Leaf}~c)$'' $\mid$ \\
+``$\textit{swap}~(\textit{Branch}~t~u)~a~b = \textit{Branch}~(\textit{swap}~t~a~b)~(\textit{swap}~u~a~b)$''
+\postw
+
+The \textit{labels} function returns the set of labels occurring on leaves of a
+tree, and \textit{swap} exchanges two labels. Intuitively, if two distinct
+labels $a$ and $b$ occur in a tree $t$, they should also occur in the tree
+obtained by swapping $a$ and $b$:
+
+\prew
+\textbf{lemma} $``\lbrakk a \in \textit{labels}~t;\, b \in \textit{labels}~t;\, a \not= b\rbrakk {}$ \\
+\phantom{\textbf{lemma} ``}$\,{\Longrightarrow}{\;\,} \textit{labels}~(\textit{swap}~t~a~b) = \textit{labels}~t$''
+\postw
+
+Nitpick can't find any counterexample, so we proceed with induction
+(this time favoring a more structured style):
+
+\prew
+\textbf{proof}~(\textit{induct}~$t$) \\
+\hbox{}\quad \textbf{case}~\textit{Leaf}~\textbf{thus}~\textit{?case}~\textbf{by}~\textit{simp} \\
+\textbf{next} \\
+\hbox{}\quad \textbf{case}~$(\textit{Branch}~t~u)$~\textbf{thus} \textit{?case}
+\postw
+
+Nitpick can't find any counterexample at this point either, but it makes the
+following suggestion:
+
+\prew
+\slshape
+Hint: To check that the induction hypothesis is general enough, try the following command:
+\textbf{nitpick}~[\textit{non\_std} ``${\kern1pt'a}~\textit{bin\_tree}$'', \textit{show\_consts}].
+\postw
+
+If we follow the hint, we get a ``nonstandard'' counterexample for the step:
+
+\prew
+\slshape Nitpick found a nonstandard counterexample for \textit{card} $'a$ = 4: \\[2\smallskipamount]
+\hbox{}\qquad Free variables: \nopagebreak \\
+\hbox{}\qquad\qquad $a = a_4$ \\
+\hbox{}\qquad\qquad $b = a_3$ \\
+\hbox{}\qquad\qquad $t = \xi_3$ \\
+\hbox{}\qquad\qquad $u = \xi_4$ \\
+\hbox{}\qquad {\slshape Constants:} \nopagebreak \\
+\hbox{}\qquad\qquad $\textit{labels} = \undef
+ (\!\begin{aligned}[t]%
+ & \xi_3 := \{a_4\},\> \xi_4 := \{a_1, a_3\}, \\[-2pt] %% TYPESETTING
+ & \textit{Branch}~\xi_3~\xi_3 := \{a_4\}, \\[-2pt]
+ & \textit{Branch}~\xi_3~\xi_4 := \{a_1, a_3, a_4\})\end{aligned}$ \\
+\hbox{}\qquad\qquad $\lambda x_1.\> \textit{swap}~x_1~a~b = \undef
+ (\!\begin{aligned}[t]%
+ & \xi_3 := \xi_3,\> \xi_4 := \xi_3, \\[-2pt]
+ & \textit{Branch}~\xi_3~\xi_3 := \textit{Branch}~\xi_3~\xi_3, \\[-2pt]
+ & \textit{Branch}~\xi_4~\xi_3 := \textit{Branch}~\xi_3~\xi_3)\end{aligned}$ \\[2\smallskipamount]
+The existence of a nonstandard model suggests that the induction hypothesis is not general enough or perhaps
+even wrong. See the ``Inductive Properties'' section of the Nitpick manual for details (``\textit{isabelle doc nitpick}'').
+\postw
+
+Reading the Nitpick manual is a most excellent idea.
+But what's going on? The \textit{non\_std} ``${\kern1pt'a}~\textit{bin\_tree}$''
+option told the tool to look for nonstandard models of binary trees, which
+means that new ``nonstandard'' trees $\xi_1, \xi_2, \ldots$, are now allowed in
+addition to the standard trees generated by the \textit{Leaf} and
+\textit{Branch} constructors.%
+\footnote{Notice the similarity between allowing nonstandard trees here and
+allowing unreachable states in the preceding example (by removing the ``$n \in
+\textit{reach\/}$'' assumption). In both cases, we effectively enlarge the
+set of objects over which the induction is performed while doing the step
+so as to test the induction hypothesis's strength.}
+The new trees are so nonstandard that we know nothing about them, except what
+the induction hypothesis states and what can be proved about all trees without
+relying on induction or case distinction. The key observation is,
+%
+\begin{quote}
+\textsl{If the induction
+hypothesis is strong enough, the induction step will hold even for nonstandard
+objects, and Nitpick won't find any nonstandard counterexample.}
+\end{quote}
+%
+But here, Nitpick did find some nonstandard trees $t = \xi_3$
+and $u = \xi_4$ such that $a \in \textit{labels}~t$, $b \notin
+\textit{labels}~t$, $a \notin \textit{labels}~u$, and $b \in \textit{labels}~u$.
+Because neither tree contains both $a$ and $b$, the induction hypothesis tells
+us nothing about the labels of $\textit{swap}~t~a~b$ and $\textit{swap}~u~a~b$,
+and as a result we know nothing about the labels of the tree
+$\textit{swap}~(\textit{Branch}~t~u)~a~b$, which by definition equals
+$\textit{Branch}$ $(\textit{swap}~t~a~b)$ $(\textit{swap}~u~a~b)$, whose
+labels are $\textit{labels}$ $(\textit{swap}~t~a~b) \mathrel{\cup}
+\textit{labels}$ $(\textit{swap}~u~a~b)$.
+
+The solution is to ensure that we always know what the labels of the subtrees
+are in the inductive step, by covering the cases where $a$ and/or~$b$ is not in
+$t$ in the statement of the lemma:
+
+\prew
+\textbf{lemma} ``$\textit{labels}~(\textit{swap}~t~a~b) = {}$ \\
+\phantom{\textbf{lemma} ``}$(\textrm{if}~a \in \textit{labels}~t~\textrm{then}$ \nopagebreak \\
+\phantom{\textbf{lemma} ``(\quad}$\textrm{if}~b \in \textit{labels}~t~\textrm{then}~\textit{labels}~t~\textrm{else}~(\textit{labels}~t - \{a\}) \mathrel{\cup} \{b\}$ \\
+\phantom{\textbf{lemma} ``(}$\textrm{else}$ \\
+\phantom{\textbf{lemma} ``(\quad}$\textrm{if}~b \in \textit{labels}~t~\textrm{then}~(\textit{labels}~t - \{b\}) \mathrel{\cup} \{a\}~\textrm{else}~\textit{labels}~t)$''
+\postw
+
+This time, Nitpick won't find any nonstandard counterexample, and we can perform
+the induction step using \textbf{auto}.
+
\section{Case Studies}
\label{case-studies}
@@ -1398,7 +1598,8 @@
functions:
\prew
-\textbf{datatype} $'a$~\textit{tree} = $\Lambda$ $\mid$ $N$ ``\kern1pt$'a\Colon \textit{linorder}$'' \textit{nat} ``\kern1pt$'a$ \textit{tree}'' ``\kern1pt$'a$ \textit{tree}'' \\[2\smallskipamount]
+\textbf{datatype} $'a$~\textit{aa\_tree} = \\
+\hbox{}\quad $\Lambda$ $\mid$ $N$ ``\kern1pt$'a\Colon \textit{linorder}$'' \textit{nat} ``\kern1pt$'a$ \textit{aa\_tree}'' ``\kern1pt$'a$ \textit{aa\_tree}'' \\[2\smallskipamount]
\textbf{primrec} \textit{data} \textbf{where} \\
``$\textit{data}~\Lambda = \undef$'' $\,\mid$ \\
``$\textit{data}~(N~x~\_~\_~\_) = x$'' \\[2\smallskipamount]
@@ -1526,7 +1727,7 @@
\slshape Nitpick found a counterexample for \textit{card} $'a$ = 4: \\[2\smallskipamount]
\hbox{}\qquad Free variables: \nopagebreak \\
\hbox{}\qquad\qquad $t = N~a_3~1~\Lambda~\Lambda$ \\
-\hbox{}\qquad\qquad $x = a_4$ \\[2\smallskipamount]
+\hbox{}\qquad\qquad $x = a_4$
\postw
It's hard to see why this is a counterexample. To improve readability, we will
@@ -1583,10 +1784,11 @@
\def\optrue#1#2{\flushitem{\textit{#1} $\bigl[$= \qtybf{bool}$\bigr]$\quad [\textit{true}]\hfill (neg.: \textit{#2})}\nopagebreak\\[\parskip]}
\def\opfalse#1#2{\flushitem{\textit{#1} $\bigl[$= \qtybf{bool}$\bigr]$\quad [\textit{false}]\hfill (neg.: \textit{#2})}\nopagebreak\\[\parskip]}
\def\opsmart#1#2{\flushitem{\textit{#1} $\bigl[$= \qtybf{bool\_or\_smart}$\bigr]$\quad [\textit{smart}]\hfill (neg.: \textit{#2})}\nopagebreak\\[\parskip]}
-\def\ops#1#2{\flushitem{\textit{#1} = \qtybf{#2}} \nopagebreak\\[\parskip]}
-\def\opt#1#2#3{\flushitem{\textit{#1} = \qtybf{#2}\quad [\textit{#3}]} \nopagebreak\\[\parskip]}
-\def\opu#1#2#3{\flushitem{\textit{#1} \qtybf{#2} = \qtybf{#3}} \nopagebreak\\[\parskip]}
-\def\opusmart#1#2#3{\flushitem{\textit{#1} \qtybf{#2} $\bigl[$= \qtybf{bool\_or\_smart}$\bigr]$\hfill (neg.: \textit{#3})}\nopagebreak\\[\parskip]}
+\def\opnodefault#1#2{\flushitem{\textit{#1} = \qtybf{#2}} \nopagebreak\\[\parskip]}
+\def\opdefault#1#2#3{\flushitem{\textit{#1} = \qtybf{#2}\quad [\textit{#3}]} \nopagebreak\\[\parskip]}
+\def\oparg#1#2#3{\flushitem{\textit{#1} \qtybf{#2} = \qtybf{#3}} \nopagebreak\\[\parskip]}
+\def\opargbool#1#2#3{\flushitem{\textit{#1} \qtybf{#2} $\bigl[$= \qtybf{bool}$\bigr]$\hfill (neg.: \textit{#3})}\nopagebreak\\[\parskip]}
+\def\opargboolorsmart#1#2#3{\flushitem{\textit{#1} \qtybf{#2} $\bigl[$= \qtybf{bool\_or\_smart}$\bigr]$\hfill (neg.: \textit{#3})}\nopagebreak\\[\parskip]}
Nitpick's behavior can be influenced by various options, which can be specified
in brackets after the \textbf{nitpick} command. Default values can be set
@@ -1696,7 +1898,7 @@
\label{scope-of-search}
\begin{enum}
-\opu{card}{type}{int\_seq}
+\oparg{card}{type}{int\_seq}
Specifies the sequence of cardinalities to use for a given type.
For free types, and often also for \textbf{typedecl}'d types, it usually makes
sense to specify cardinalities as a range of the form \textit{$1$--$n$}.
@@ -1709,18 +1911,18 @@
\nopagebreak
{\small See also \textit{mono} (\S\ref{scope-of-search}).}
-\opt{card}{int\_seq}{$\mathbf{1}$--$\mathbf{8}$}
+\opdefault{card}{int\_seq}{$\mathbf{1}$--$\mathbf{8}$}
Specifies the default sequence of cardinalities to use. This can be overridden
on a per-type basis using the \textit{card}~\qty{type} option described above.
-\opu{max}{const}{int\_seq}
+\oparg{max}{const}{int\_seq}
Specifies the sequence of maximum multiplicities to use for a given
(co)in\-duc\-tive datatype constructor. A constructor's multiplicity is the
number of distinct values that it can construct. Nonsensical values (e.g.,
\textit{max}~[]~$=$~2) are silently repaired. This option is only available for
datatypes equipped with several constructors.
-\ops{max}{int\_seq}
+\opnodefault{max}{int\_seq}
Specifies the default sequence of maximum multiplicities to use for
(co)in\-duc\-tive datatype constructors. This can be overridden on a per-constructor
basis using the \textit{max}~\qty{const} option described above.
@@ -1757,13 +1959,13 @@
{\small See also \textit{bits} (\S\ref{scope-of-search}) and
\textit{show\_datatypes} (\S\ref{output-format}).}
-\opt{bits}{int\_seq}{$\mathbf{1},\mathbf{2},\mathbf{3},\mathbf{4},\mathbf{6},\mathbf{8},\mathbf{10},\mathbf{12}$}
+\opdefault{bits}{int\_seq}{$\mathbf{1},\mathbf{2},\mathbf{3},\mathbf{4},\mathbf{6},\mathbf{8},\mathbf{10},\mathbf{12}$}
Specifies the number of bits to use to represent natural numbers and integers in
binary, excluding the sign bit. The minimum is 1 and the maximum is 31.
{\small See also \textit{binary\_ints} (\S\ref{scope-of-search}).}
-\opusmart{wf}{const}{non\_wf}
+\opargboolorsmart{wf}{const}{non\_wf}
Specifies whether the specified (co)in\-duc\-tively defined predicate is
well-founded. The option can take the following values:
@@ -1780,7 +1982,7 @@
\item[$\bullet$] \textbf{\textit{smart}}: Try to prove that the inductive
predicate is well-founded using Isabelle's \textit{lexicographic\_order} and
-\textit{sizechange} tactics. If this succeeds (or the predicate occurs with an
+\textit{size\_change} tactics. If this succeeds (or the predicate occurs with an
appropriate polarity in the formula to falsify), use an efficient fixed point
equation as specification of the predicate; otherwise, unroll the predicates
according to the \textit{iter}~\qty{const} and \textit{iter} options.
@@ -1795,7 +1997,7 @@
Specifies the default wellfoundedness setting to use. This can be overridden on
a per-predicate basis using the \textit{wf}~\qty{const} option above.
-\opu{iter}{const}{int\_seq}
+\oparg{iter}{const}{int\_seq}
Specifies the sequence of iteration counts to use when unrolling a given
(co)in\-duc\-tive predicate. By default, unrolling is applied for inductive
predicates that occur negatively and coinductive predicates that occur
@@ -1807,12 +2009,12 @@
{\small See also \textit{wf} (\S\ref{scope-of-search}) and
\textit{star\_linear\_preds} (\S\ref{optimizations}).}
-\opt{iter}{int\_seq}{$\mathbf{1{,}2{,}4{,}8{,}12{,}16{,}24{,}32}$}
+\opdefault{iter}{int\_seq}{$\mathbf{1{,}2{,}4{,}8{,}12{,}16{,}24{,}32}$}
Specifies the sequence of iteration counts to use when unrolling (co)in\-duc\-tive
predicates. This can be overridden on a per-predicate basis using the
\textit{iter} \qty{const} option above.
-\opt{bisim\_depth}{int\_seq}{$\mathbf{7}$}
+\opdefault{bisim\_depth}{int\_seq}{$\mathbf{7}$}
Specifies the sequence of iteration counts to use when unrolling the
bisimilarity predicate generated by Nitpick for coinductive datatypes. A value
of $-1$ means that no predicate is generated, in which case Nitpick performs an
@@ -1822,7 +2024,7 @@
the sum of the cardinalities of the coinductive datatypes occurring in the
formula to falsify.
-\opusmart{box}{type}{dont\_box}
+\opargboolorsmart{box}{type}{dont\_box}
Specifies whether Nitpick should attempt to wrap (``box'') a given function or
product type in an isomorphic datatype internally. Boxing is an effective mean
to reduce the search space and speed up Nitpick, because the isomorphic datatype
@@ -1850,8 +2052,8 @@
Specifies the default boxing setting to use. This can be overridden on a
per-type basis using the \textit{box}~\qty{type} option described above.
-\opusmart{mono}{type}{non\_mono}
-Specifies whether the specified type should be considered monotonic when
+\opargboolorsmart{mono}{type}{non\_mono}
+Specifies whether the given type should be considered monotonic when
enumerating scopes. If the option is set to \textit{smart}, Nitpick performs a
monotonicity check on the type. Setting this option to \textit{true} can reduce
the number of scopes tried, but it also diminishes the theoretical chance of
@@ -1873,6 +2075,15 @@
theoretical chance of finding a counterexample.
{\small See also \textit{mono} (\S\ref{scope-of-search}).}
+
+\opargbool{std}{type}{non\_std}
+Specifies whether the given type should be given standard models.
+Nonstandard models are unsound but can help debug inductive arguments,
+as explained in \S\ref{inductive-properties}.
+
+\optrue{std}{non\_std}
+Specifies the default standardness to use. This can be overridden on a per-type
+basis using the \textit{std}~\qty{type} option described above.
\end{enum}
\subsection{Output Format}
@@ -1919,7 +2130,7 @@
Enabling this option effectively enables \textit{show\_skolems},
\textit{show\_datatypes}, and \textit{show\_consts}.
-\opt{max\_potential}{int}{$\mathbf{1}$}
+\opdefault{max\_potential}{int}{$\mathbf{1}$}
Specifies the maximum number of potential counterexamples to display. Setting
this option to 0 speeds up the search for a genuine counterexample. This option
is implicitly set to 0 for automatic runs. If you set this option to a value
@@ -1933,7 +2144,7 @@
{\small See also \textit{check\_potential} (\S\ref{authentication}) and
\textit{sat\_solver} (\S\ref{optimizations}).}
-\opt{max\_genuine}{int}{$\mathbf{1}$}
+\opdefault{max\_genuine}{int}{$\mathbf{1}$}
Specifies the maximum number of genuine counterexamples to display. If you set
this option to a value greater than 1, you will need an incremental SAT solver:
For efficiency, it is recommended to install the JNI version of MiniSat and set
@@ -1945,12 +2156,12 @@
{\small See also \textit{check\_genuine} (\S\ref{authentication}) and
\textit{sat\_solver} (\S\ref{optimizations}).}
-\ops{eval}{term\_list}
+\opnodefault{eval}{term\_list}
Specifies the list of terms whose values should be displayed along with
counterexamples. This option suffers from an ``observer effect'': Nitpick might
find different counterexamples for different values of this option.
-\opu{format}{term}{int\_seq}
+\oparg{format}{term}{int\_seq}
Specifies how to uncurry the value displayed for a variable or constant.
Uncurrying sometimes increases the readability of the output for high-arity
functions. For example, given the variable $y \mathbin{\Colon} {'a}\Rightarrow
@@ -1966,7 +2177,7 @@
\nopagebreak
{\small See also \textit{uncurry} (\S\ref{optimizations}).}
-\opt{format}{int\_seq}{$\mathbf{1}$}
+\opdefault{format}{int\_seq}{$\mathbf{1}$}
Specifies the default format to use. Irrespective of the default format, the
extra arguments to a Skolem constant corresponding to the outer bound variables
are kept separated from the remaining arguments, the \textbf{for} arguments of
@@ -1999,7 +2210,7 @@
\nopagebreak
{\small See also \textit{max\_genuine} (\S\ref{output-format}).}
-\ops{expect}{string}
+\opnodefault{expect}{string}
Specifies the expected outcome, which must be one of the following:
\begin{enum}
@@ -2025,7 +2236,7 @@
\sloppy
\begin{enum}
-\opt{sat\_solver}{string}{smart}
+\opdefault{sat\_solver}{string}{smart}
Specifies which SAT solver to use. SAT solvers implemented in C or \cpp{} tend
to be faster than their Java counterparts, but they can be more difficult to
install. Also, if you set the \textit{max\_potential} (\S\ref{output-format}) or
@@ -2118,7 +2329,7 @@
\end{enum}
\fussy
-\opt{batch\_size}{int\_or\_smart}{smart}
+\opdefault{batch\_size}{int\_or\_smart}{smart}
Specifies the maximum number of Kodkod problems that should be lumped together
when invoking Kodkodi. Each problem corresponds to one scope. Lumping problems
together ensures that Kodkodi is launched less often, but it makes the verbose
@@ -2188,7 +2399,7 @@
Unless you are tracking down a bug in Nitpick or distrust the peephole
optimizer, you should leave this option enabled.
-\opt{sym\_break}{int}{20}
+\opdefault{sym\_break}{int}{20}
Specifies an upper bound on the number of relations for which Kodkod generates
symmetry breaking predicates. According to the Kodkod documentation
\cite{kodkod-2009-options}, ``in general, the higher this value, the more
@@ -2196,7 +2407,7 @@
setting the value too high may have the opposite effect and slow down the
solving.''
-\opt{sharing\_depth}{int}{3}
+\opdefault{sharing\_depth}{int}{3}
Specifies the depth to which Kodkod should check circuits for equivalence during
the translation to SAT. The default of 3 is the same as in Alloy. The minimum
allowed depth is 1. Increasing the sharing may result in a smaller SAT problem,
@@ -2207,7 +2418,7 @@
Although this might sound like a good idea, in practice it can drastically slow
down Kodkod.
-\opt{max\_threads}{int}{0}
+\opdefault{max\_threads}{int}{0}
Specifies the maximum number of threads to use in Kodkod. If this option is set
to 0, Kodkod will compute an appropriate value based on the number of processor
cores available.
@@ -2221,7 +2432,7 @@
\label{timeouts}
\begin{enum}
-\opt{timeout}{time}{$\mathbf{30}$ s}
+\opdefault{timeout}{time}{$\mathbf{30}$ s}
Specifies the maximum amount of time that the \textbf{nitpick} command should
spend looking for a counterexample. Nitpick tries to honor this constraint as
well as it can but offers no guarantees. For automatic runs,
@@ -2232,10 +2443,10 @@
\nopagebreak
{\small See also \textit{max\_threads} (\S\ref{optimizations}).}
-\opt{tac\_timeout}{time}{$\mathbf{500}$\,ms}
+\opdefault{tac\_timeout}{time}{$\mathbf{500}$\,ms}
Specifies the maximum amount of time that the \textit{auto} tactic should use
when checking a counterexample, and similarly that \textit{lexicographic\_order}
-and \textit{sizechange} should use when checking whether a (co)in\-duc\-tive
+and \textit{size\_change} should use when checking whether a (co)in\-duc\-tive
predicate is well-founded. Nitpick tries to honor this constraint as well as it
can but offers no guarantees.
@@ -2477,7 +2688,7 @@
\nopagebreak
\\[2\smallskipamount]
\hbox{}\qquad Empty assignment} \nopagebreak\\[2\smallskipamount]
-\textbf{by}~(\textit{auto simp}: \textit{prec\_def})
+\textbf{by}~(\textit{auto simp}:~\textit{prec\_def})
\postw
Such theorems are considered bad style because they rely on the internal
--- a/src/HOL/Divides.thy Mon Feb 01 14:12:12 2010 +0100
+++ b/src/HOL/Divides.thy Tue Feb 02 11:38:38 2010 +0100
@@ -2451,7 +2451,8 @@
in subst [OF mod_div_equality [of _ n]])
arith
-lemmas [nitpick_def] = mod_div_equality' [THEN eq_reflection]
+lemmas [nitpick_def] = dvd_eq_mod_eq_0 [THEN eq_reflection]
+ mod_div_equality' [THEN eq_reflection]
zmod_zdiv_equality' [THEN eq_reflection]
subsubsection {* Code generation *}
--- a/src/HOL/Nitpick.thy Mon Feb 01 14:12:12 2010 +0100
+++ b/src/HOL/Nitpick.thy Tue Feb 02 11:38:38 2010 +0100
@@ -36,6 +36,7 @@
and bisim_iterator_max :: bisim_iterator
and Quot :: "'a \<Rightarrow> 'b"
and quot_normal :: "'a \<Rightarrow> 'a"
+ and NonStd :: "'a \<Rightarrow> 'b"
and Tha :: "('a \<Rightarrow> bool) \<Rightarrow> 'a"
datatype ('a, 'b) pair_box = PairBox 'a 'b
@@ -43,6 +44,7 @@
typedecl unsigned_bit
typedecl signed_bit
+typedecl \<xi>
datatype 'a word = Word "('a set)"
@@ -250,12 +252,12 @@
setup {* Nitpick_Isar.setup *}
hide (open) const unknown is_unknown undefined_fast_The undefined_fast_Eps bisim
- bisim_iterator_max Quot quot_normal Tha PairBox FunBox Word refl' wf'
+ bisim_iterator_max Quot quot_normal NonStd Tha PairBox FunBox Word refl' wf'
wf_wfrec wf_wfrec' wfrec' card' setsum' fold_graph' nat_gcd nat_lcm int_gcd
int_lcm Frac Abs_Frac Rep_Frac zero_frac one_frac num denom norm_frac frac
plus_frac times_frac uminus_frac number_of_frac inverse_frac less_eq_frac
of_frac
-hide (open) type bisim_iterator pair_box fun_box unsigned_bit signed_bit word
+hide (open) type bisim_iterator pair_box fun_box unsigned_bit signed_bit \<xi> word
hide (open) fact If_def Ex1_def rtrancl_def rtranclp_def tranclp_def refl'_def
wf'_def wf_wfrec'_def wfrec'_def card'_def setsum'_def fold_graph'_def
The_psimp Eps_psimp unit_case_def nat_case_def list_size_simp nat_gcd_def
--- a/src/HOL/Nitpick_Examples/Manual_Nits.thy Mon Feb 01 14:12:12 2010 +0100
+++ b/src/HOL/Nitpick_Examples/Manual_Nits.thy Tue Feb 02 11:38:38 2010 +0100
@@ -220,6 +220,69 @@
nitpick
oops
+subsection {* 3.12. Inductive Properties *}
+
+inductive_set reach where
+"(4\<Colon>nat) \<in> reach" |
+"n \<in> reach \<Longrightarrow> n < 4 \<Longrightarrow> 3 * n + 1 \<in> reach" |
+"n \<in> reach \<Longrightarrow> n + 2 \<in> reach"
+
+lemma "n \<in> reach \<Longrightarrow> 2 dvd n"
+nitpick
+apply (induct set: reach)
+ apply auto
+ nitpick
+ apply (thin_tac "n \<in> reach")
+ nitpick
+oops
+
+lemma "n \<in> reach \<Longrightarrow> 2 dvd n \<and> n \<noteq> 0"
+nitpick
+apply (induct set: reach)
+ apply auto
+ nitpick
+ apply (thin_tac "n \<in> reach")
+ nitpick
+oops
+
+lemma "n \<in> reach \<Longrightarrow> 2 dvd n \<and> n \<ge> 4"
+by (induct set: reach) arith+
+
+datatype 'a bin_tree = Leaf 'a | Branch "'a bin_tree" "'a bin_tree"
+
+primrec labels where
+"labels (Leaf a) = {a}" |
+"labels (Branch t u) = labels t \<union> labels u"
+
+primrec swap where
+"swap (Leaf c) a b =
+ (if c = a then Leaf b else if c = b then Leaf a else Leaf c)" |
+"swap (Branch t u) a b = Branch (swap t a b) (swap u a b)"
+
+lemma "\<lbrakk>a \<in> labels t; b \<in> labels t; a \<noteq> b\<rbrakk> \<Longrightarrow> labels (swap t a b) = labels t"
+nitpick
+proof (induct t)
+ case Leaf thus ?case by simp
+next
+ case (Branch t u) thus ?case
+ nitpick
+ nitpick [non_std "'a bin_tree", show_consts]
+oops
+
+lemma "labels (swap t a b) =
+ (if a \<in> labels t then
+ if b \<in> labels t then labels t else (labels t - {a}) \<union> {b}
+ else
+ if b \<in> labels t then (labels t - {b}) \<union> {a} else labels t)"
+nitpick
+proof (induct t)
+ case Leaf thus ?case by simp
+next
+ case (Branch t u) thus ?case
+ nitpick [non_std "'a bin_tree", show_consts]
+ by auto
+qed
+
section {* 4. Case Studies *}
nitpick_params [max_potential = 0, max_threads = 2]
@@ -300,7 +363,7 @@
subsection {* 4.2. AA Trees *}
-datatype 'a tree = \<Lambda> | N "'a\<Colon>linorder" nat "'a tree" "'a tree"
+datatype 'a aa_tree = \<Lambda> | N "'a\<Colon>linorder" nat "'a aa_tree" "'a aa_tree"
primrec data where
"data \<Lambda> = undefined" |
--- a/src/HOL/Nitpick_Examples/Mono_Nits.thy Mon Feb 01 14:12:12 2010 +0100
+++ b/src/HOL/Nitpick_Examples/Mono_Nits.thy Tue Feb 02 11:38:38 2010 +0100
@@ -18,18 +18,19 @@
val def_table = Nitpick_HOL.const_def_table @{context} defs
val ext_ctxt : Nitpick_HOL.extended_context =
{thy = @{theory}, ctxt = @{context}, max_bisim_depth = ~1, boxes = [],
- user_axioms = NONE, debug = false, wfs = [], binary_ints = SOME false,
- destroy_constrs = false, specialize = false, skolemize = false,
- star_linear_preds = false, uncurry = false, fast_descrs = false,
- tac_timeout = NONE, evals = [], case_names = [], def_table = def_table,
- nondef_table = Symtab.empty, user_nondefs = [],
+ stds = [(NONE, true)], wfs = [], user_axioms = NONE, debug = false,
+ binary_ints = SOME false, destroy_constrs = false, specialize = false,
+ skolemize = false, star_linear_preds = false, uncurry = false,
+ fast_descrs = false, tac_timeout = NONE, evals = [], case_names = [],
+ def_table = def_table, nondef_table = Symtab.empty, user_nondefs = [],
simp_table = Unsynchronized.ref Symtab.empty, psimp_table = Symtab.empty,
intro_table = Symtab.empty, ground_thm_table = Inttab.empty,
ersatz_table = [], skolems = Unsynchronized.ref [],
special_funs = Unsynchronized.ref [], unrolled_preds = Unsynchronized.ref [],
wf_cache = Unsynchronized.ref [], constr_cache = Unsynchronized.ref []}
(* term -> bool *)
-val is_mono = Nitpick_Mono.formulas_monotonic ext_ctxt @{typ 'a} [] []
+val is_mono = Nitpick_Mono.formulas_monotonic ext_ctxt @{typ 'a}
+ Nitpick_Mono.Plus [] []
fun is_const t =
let val T = fastype_of t in
is_mono (Logic.mk_implies (Logic.mk_equals (Free ("dummyP", T), t),
--- a/src/HOL/Tools/Nitpick/HISTORY Mon Feb 01 14:12:12 2010 +0100
+++ b/src/HOL/Tools/Nitpick/HISTORY Tue Feb 02 11:38:38 2010 +0100
@@ -1,7 +1,9 @@
Version 2010
* Added and implemented "binary_ints" and "bits" options
- * Fixed soundness bug in "destroy_constrs" optimization
+ * Added "std" option and implemented support for nonstandard models
+ * Fixed soundness bugs related to "destroy_constrs" optimization and record
+ getters
Version 2009-1
--- a/src/HOL/Tools/Nitpick/kodkod.ML Mon Feb 01 14:12:12 2010 +0100
+++ b/src/HOL/Tools/Nitpick/kodkod.ML Tue Feb 02 11:38:38 2010 +0100
@@ -1,6 +1,6 @@
(* Title: HOL/Tools/Nitpick/kodkod.ML
Author: Jasmin Blanchette, TU Muenchen
- Copyright 2008, 2009
+ Copyright 2008, 2009, 2010
ML interface on top of Kodkod.
*)
--- a/src/HOL/Tools/Nitpick/kodkod_sat.ML Mon Feb 01 14:12:12 2010 +0100
+++ b/src/HOL/Tools/Nitpick/kodkod_sat.ML Tue Feb 02 11:38:38 2010 +0100
@@ -1,6 +1,6 @@
(* Title: HOL/Tools/Nitpick/kodkod_sat.ML
Author: Jasmin Blanchette, TU Muenchen
- Copyright 2009
+ Copyright 2009, 2010
Kodkod SAT solver integration.
*)
--- a/src/HOL/Tools/Nitpick/minipick.ML Mon Feb 01 14:12:12 2010 +0100
+++ b/src/HOL/Tools/Nitpick/minipick.ML Tue Feb 02 11:38:38 2010 +0100
@@ -1,6 +1,6 @@
(* Title: HOL/Tools/Nitpick/minipick.ML
Author: Jasmin Blanchette, TU Muenchen
- Copyright 2009
+ Copyright 2009, 2010
Finite model generation for HOL formulas using Kodkod, minimalistic version.
*)
--- a/src/HOL/Tools/Nitpick/nitpick.ML Mon Feb 01 14:12:12 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick.ML Tue Feb 02 11:38:38 2010 +0100
@@ -1,6 +1,6 @@
(* Title: HOL/Tools/Nitpick/nitpick.ML
Author: Jasmin Blanchette, TU Muenchen
- Copyright 2008, 2009
+ Copyright 2008, 2009, 2010
Finite model generation for HOL formulas using Kodkod.
*)
@@ -16,6 +16,7 @@
bisim_depths: int list,
boxes: (typ option * bool option) list,
monos: (typ option * bool option) list,
+ stds: (typ option * bool) list,
wfs: (styp option * bool option) list,
sat_solver: string,
blocking: bool,
@@ -57,9 +58,10 @@
val register_codatatype : typ -> string -> styp list -> theory -> theory
val unregister_codatatype : typ -> theory -> theory
val pick_nits_in_term :
- Proof.state -> params -> bool -> term list -> term -> string * Proof.state
+ Proof.state -> params -> bool -> int -> int -> int -> term list -> term
+ -> string * Proof.state
val pick_nits_in_subgoal :
- Proof.state -> params -> bool -> int -> string * Proof.state
+ Proof.state -> params -> bool -> int -> int -> string * Proof.state
end;
structure Nitpick : NITPICK =
@@ -85,6 +87,7 @@
bisim_depths: int list,
boxes: (typ option * bool option) list,
monos: (typ option * bool option) list,
+ stds: (typ option * bool) list,
wfs: (styp option * bool option) list,
sat_solver: string,
blocking: bool,
@@ -183,18 +186,21 @@
(* (unit -> string) -> Pretty.T *)
fun plazy f = Pretty.blk (0, pstrs (f ()))
-(* Time.time -> Proof.state -> params -> bool -> term -> string * Proof.state *)
-fun pick_them_nits_in_term deadline state (params : params) auto orig_assm_ts
- orig_t =
+(* Time.time -> Proof.state -> params -> bool -> int -> int -> int -> term
+ -> string * Proof.state *)
+fun pick_them_nits_in_term deadline state (params : params) auto i n step
+ orig_assm_ts orig_t =
let
val timer = Timer.startRealTimer ()
val thy = Proof.theory_of state
val ctxt = Proof.context_of state
+(* FIXME: reintroduce code before new release
val nitpick_thy = ThyInfo.get_theory "Nitpick"
val _ = Theory.subthy (nitpick_thy, thy) orelse
error "You must import the theory \"Nitpick\" to use Nitpick"
+*)
val {cards_assigns, maxes_assigns, iters_assigns, bitss, bisim_depths,
- boxes, monos, wfs, sat_solver, blocking, falsify, debug, verbose,
+ boxes, monos, stds, wfs, sat_solver, blocking, falsify, debug, verbose,
overlord, user_axioms, assms, merge_type_vars, binary_ints,
destroy_constrs, specialize, skolemize, star_linear_preds, uncurry,
fast_descrs, peephole_optim, tac_timeout, sym_break, sharing_depth,
@@ -231,7 +237,16 @@
if passed_deadline deadline then raise TimeLimit.TimeOut
else raise Interrupt
- val _ = print_m (K "Nitpicking...")
+ val _ =
+ if step = 0 then
+ print_m (fn () => "Nitpicking formula...")
+ else
+ pprint_m (fn () => Pretty.chunks (
+ pretties_for_formulas ctxt ("Nitpicking " ^
+ (if i <> 1 orelse n <> 1 then
+ "subgoal " ^ string_of_int i ^ " of " ^ string_of_int n
+ else
+ "goal")) [orig_t]))
val neg_t = if falsify then Logic.mk_implies (orig_t, @{prop False})
else orig_t
val assms_t = if assms orelse auto then
@@ -260,7 +275,7 @@
val ersatz_table = ersatz_table thy
val (ext_ctxt as {wf_cache, ...}) =
{thy = thy, ctxt = ctxt, max_bisim_depth = max_bisim_depth, boxes = boxes,
- user_axioms = user_axioms, debug = debug, wfs = wfs,
+ stds = stds, wfs = wfs, user_axioms = user_axioms, debug = debug,
binary_ints = binary_ints, destroy_constrs = destroy_constrs,
specialize = specialize, skolemize = skolemize,
star_linear_preds = star_linear_preds, uncurry = uncurry,
@@ -311,7 +326,8 @@
fold add_free_and_const_names (core_u :: def_us @ nondef_us) ([], [])
val (sel_names, nonsel_names) =
List.partition (is_sel o nickname_of) const_names
- val would_be_genuine = got_all_user_axioms andalso none_true wfs
+ val genuine_means_genuine = got_all_user_axioms andalso none_true wfs
+ val standard = forall snd stds
(*
val _ = List.app (priority o string_for_nut ctxt)
(core_u :: def_us @ nondef_us)
@@ -322,27 +338,27 @@
fun is_type_always_monotonic T =
(is_datatype thy T andalso not (is_quot_type thy T) andalso
(not (is_pure_typedef thy T) orelse is_univ_typedef thy T)) orelse
- is_number_type thy T orelse is_bit_type T
+ is_number_type thy T orelse is_bit_type T orelse T = @{typ \<xi>}
fun is_type_monotonic T =
unique_scope orelse
case triple_lookup (type_match thy) monos T of
SOME (SOME b) => b
| _ => is_type_always_monotonic T orelse
- formulas_monotonic ext_ctxt T def_ts nondef_ts core_t
+ formulas_monotonic ext_ctxt T Plus def_ts nondef_ts core_t
fun is_deep_datatype T =
is_datatype thy T andalso
(is_word_type T orelse
exists (curry (op =) T o domain_type o type_of) sel_names)
- val Ts = ground_types_in_terms ext_ctxt (core_t :: def_ts @ nondef_ts)
- |> sort TermOrd.typ_ord
+ val all_Ts = ground_types_in_terms ext_ctxt (core_t :: def_ts @ nondef_ts)
+ |> sort TermOrd.typ_ord
val _ = if verbose andalso binary_ints = SOME true andalso
- exists (member (op =) [nat_T, int_T]) Ts then
+ exists (member (op =) [nat_T, int_T]) all_Ts then
print_v (K "The option \"binary_ints\" will be ignored because \
\of the presence of rationals, reals, \"Suc\", \
\\"gcd\", or \"lcm\" in the problem.")
else
()
- val (mono_Ts, nonmono_Ts) = List.partition is_type_monotonic Ts
+ val (mono_Ts, nonmono_Ts) = List.partition is_type_monotonic all_Ts
val _ =
if verbose andalso not unique_scope then
case filter_out is_type_always_monotonic mono_Ts of
@@ -364,7 +380,32 @@
end)
else
()
- val shallow_dataTs = filter_out is_deep_datatype Ts
+ val deep_dataTs = filter is_deep_datatype all_Ts
+ (* FIXME: Implement proper detection of induction datatypes. *)
+ (* string * (Rule_Cases.T * bool) -> bool *)
+ fun is_inductive_case (_, (Rule_Cases.Case {fixes, assumes, ...}, _)) =
+ false
+(*
+ not (null fixes) andalso exists (String.isSuffix ".hyps" o fst) assumes
+*)
+ (* unit -> typ list *)
+ val induct_dataTs =
+ if exists is_inductive_case (ProofContext.cases_of ctxt) then
+ filter (is_datatype thy) all_Ts
+ else
+ []
+ val _ = if standard andalso not (null induct_dataTs) then
+ pprint_m (fn () => Pretty.blk (0,
+ pstrs "Hint: To check that the induction hypothesis is \
+ \general enough, try the following command: " @
+ [Pretty.mark Markup.sendback (Pretty.blk (0,
+ pstrs ("nitpick [" ^
+ commas (map (prefix "non_std " o maybe_quote
+ o unyxml o string_for_type ctxt)
+ induct_dataTs) ^
+ ", show_consts]")))] @ pstrs "."))
+ else
+ ()
(*
val _ = priority "Monotonic types:"
val _ = List.app (priority o string_for_type ctxt) mono_Ts
@@ -413,7 +454,7 @@
string_of_int j0))
(Typtab.dest ofs)
*)
- val all_exact = forall (is_exact_type datatypes) Ts
+ val all_exact = forall (is_exact_type datatypes) all_Ts
(* nut list -> rep NameTable.table -> nut list * rep NameTable.table *)
val repify_consts = choose_reps_for_consts scope all_exact
val main_j0 = offset_of_type ofs bool_T
@@ -536,7 +577,9 @@
fun tuple_set_for_rel univ_card =
KK.TupleSet o map (kk_tuple debug univ_card) o the oo AList.lookup (op =)
- val word_model = if falsify then "counterexample" else "model"
+ val das_wort_model =
+ (if falsify then "counterexample" else "model")
+ |> not standard ? prefix "nonstandard "
val scopes = Unsynchronized.ref []
val generated_scopes = Unsynchronized.ref []
@@ -560,42 +603,49 @@
show_consts = show_consts}
scope formats frees free_names sel_names nonsel_names rel_table
bounds
- val would_be_genuine = would_be_genuine andalso codatatypes_ok
+ val genuine_means_genuine = genuine_means_genuine andalso codatatypes_ok
in
pprint (Pretty.chunks
[Pretty.blk (0,
(pstrs ("Nitpick found a" ^
(if not genuine then " potential "
- else if would_be_genuine then " "
- else " likely genuine ") ^ word_model) @
+ else if genuine_means_genuine then " "
+ else " likely genuine ") ^ das_wort_model) @
(case pretties_for_scope scope verbose of
[] => []
| pretties => pstrs " for " @ pretties) @
[Pretty.str ":\n"])),
Pretty.indent indent_size reconstructed_model]);
if genuine then
- (if check_genuine then
+ (if check_genuine andalso standard then
(case prove_hol_model scope tac_timeout free_names sel_names
rel_table bounds assms_t of
SOME true => print ("Confirmation by \"auto\": The above " ^
- word_model ^ " is really genuine.")
+ das_wort_model ^ " is really genuine.")
| SOME false =>
- if would_be_genuine then
- error ("A supposedly genuine " ^ word_model ^ " was shown to\
- \be spurious by \"auto\".\nThis should never happen.\n\
- \Please send a bug report to blanchet\
+ if genuine_means_genuine then
+ error ("A supposedly genuine " ^ das_wort_model ^ " was \
+ \shown to be spurious by \"auto\".\nThis should never \
+ \happen.\nPlease send a bug report to blanchet\
\te@in.tum.de.")
else
- print ("Refutation by \"auto\": The above " ^ word_model ^
+ print ("Refutation by \"auto\": The above " ^ das_wort_model ^
" is spurious.")
| NONE => print "No confirmation by \"auto\".")
else
();
+ if not standard andalso not (null induct_dataTs) then
+ print "The existence of a nonstandard model suggests that the \
+ \induction hypothesis is not general enough or perhaps even \
+ \wrong. See the \"Inductive Properties\" section of the \
+ \Nitpick manual for details (\"isabelle doc nitpick\")."
+ else
+ ();
if has_syntactic_sorts orig_t then
print "Hint: Maybe you forgot a type constraint?"
else
();
- if not would_be_genuine then
+ if not genuine_means_genuine then
if no_poly_user_axioms then
let
val options =
@@ -611,12 +661,13 @@
in
print ("Try again with " ^
space_implode " " (serial_commas "and" ss) ^
- " to confirm that the " ^ word_model ^ " is genuine.")
+ " to confirm that the " ^ das_wort_model ^
+ " is genuine.")
end
else
print ("Nitpick is unable to guarantee the authenticity of \
- \the " ^ word_model ^ " in the presence of polymorphic \
- \axioms.")
+ \the " ^ das_wort_model ^ " in the presence of \
+ \polymorphic axioms.")
else
();
NONE)
@@ -630,9 +681,9 @@
in
(case status of
SOME true => print ("Confirmation by \"auto\": The above " ^
- word_model ^ " is genuine.")
+ das_wort_model ^ " is genuine.")
| SOME false => print ("Refutation by \"auto\": The above " ^
- word_model ^ " is spurious.")
+ das_wort_model ^ " is spurious.")
| NONE => print "No confirmation by \"auto\".");
status
end
@@ -820,14 +871,20 @@
(print_m (fn () => excipit "ran out of some resource"); "unknown")
else if max_genuine = original_max_genuine then
if max_potential = original_max_potential then
- (print_m (K ("Nitpick found no " ^ word_model ^ ".")); "none")
+ (print_m (fn () =>
+ "Nitpick found no " ^ das_wort_model ^ "." ^
+ (if not standard andalso not (null induct_dataTs) then
+ " This suggests that the induction hypothesis might be \
+ \general enough to prove this subgoal."
+ else
+ "")); "none")
else
- (print_m (K ("Nitpick could not find " ^
- (if max_genuine = 1 then "a better " ^ word_model ^ "."
- else "any better " ^ word_model ^ "s.")));
- "potential")
+ (print_m (fn () =>
+ "Nitpick could not find a" ^
+ (if max_genuine = 1 then " better " ^ das_wort_model ^ "."
+ else "ny better " ^ das_wort_model ^ "s.")); "potential")
else
- if would_be_genuine then "genuine" else "likely_genuine"
+ if genuine_means_genuine then "genuine" else "likely_genuine"
| run_batches j n (batch :: batches) z =
let val (z as (_, max_genuine, _)) = run_batch j n batch z in
run_batches (j + 1) n (if max_genuine > 0 then batches else []) z
@@ -835,7 +892,7 @@
val (skipped, the_scopes) =
all_scopes ext_ctxt sym_break cards_assigns maxes_assigns iters_assigns
- bitss bisim_depths mono_Ts nonmono_Ts shallow_dataTs
+ bitss bisim_depths mono_Ts nonmono_Ts deep_dataTs
val _ = if skipped > 0 then
print_m (fn () => "Too many scopes. Skipping " ^
string_of_int skipped ^ " scope" ^
@@ -868,9 +925,10 @@
else
error "Nitpick was interrupted."
-(* Proof.state -> params -> bool -> term -> string * Proof.state *)
-fun pick_nits_in_term state (params as {debug, timeout, expect, ...}) auto
- orig_assm_ts orig_t =
+(* Proof.state -> params -> bool -> int -> int -> int -> term
+ -> string * Proof.state *)
+fun pick_nits_in_term state (params as {debug, timeout, expect, ...}) auto i n
+ step orig_assm_ts orig_t =
if getenv "KODKODI" = "" then
(if auto then ()
else warning (Pretty.string_of (plazy install_kodkodi_message));
@@ -880,26 +938,29 @@
val deadline = Option.map (curry Time.+ (Time.now ())) timeout
val outcome as (outcome_code, _) =
time_limit (if debug then NONE else timeout)
- (pick_them_nits_in_term deadline state params auto orig_assm_ts)
- orig_t
+ (pick_them_nits_in_term deadline state params auto i n step
+ orig_assm_ts) orig_t
in
if expect = "" orelse outcome_code = expect then outcome
else error ("Unexpected outcome: " ^ quote outcome_code ^ ".")
end
-(* Proof.state -> params -> thm -> int -> string * Proof.state *)
-fun pick_nits_in_subgoal state params auto i =
+(* Proof.state -> params -> bool -> int -> int -> string * Proof.state *)
+fun pick_nits_in_subgoal state params auto i step =
let
val ctxt = Proof.context_of state
val t = state |> Proof.raw_goal |> #goal |> prop_of
in
- if Logic.count_prems t = 0 then
- (priority "No subgoal!"; ("none", state))
- else
+ case Logic.count_prems t of
+ 0 => (priority "No subgoal!"; ("none", state))
+ | n =>
let
val assms = map term_of (Assumption.all_assms_of ctxt)
val (t, frees) = Logic.goal_params t i
- in pick_nits_in_term state params auto assms (subst_bounds (frees, t)) end
+ in
+ pick_nits_in_term state params auto i n step assms
+ (subst_bounds (frees, t))
+ end
end
end;
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Mon Feb 01 14:12:12 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Tue Feb 02 11:38:38 2010 +0100
@@ -1,6 +1,6 @@
(* Title: HOL/Tools/Nitpick/nitpick_hol.ML
Author: Jasmin Blanchette, TU Muenchen
- Copyright 2008, 2009
+ Copyright 2008, 2009, 2010
Auxiliary HOL-related functions used by Nitpick.
*)
@@ -18,6 +18,7 @@
ctxt: Proof.context,
max_bisim_depth: int,
boxes: (typ option * bool option) list,
+ stds: (typ option * bool) list,
wfs: (styp option * bool option) list,
user_axioms: bool option,
debug: bool,
@@ -165,6 +166,7 @@
ctxt: Proof.context,
max_bisim_depth: int,
boxes: (typ option * bool option) list,
+ stds: (typ option * bool) list,
wfs: (styp option * bool option) list,
user_axioms: bool option,
debug: bool,
@@ -548,7 +550,7 @@
val is_typedef = is_some oo typedef_info
val is_real_datatype = is_some oo Datatype.get_info
(* theory -> typ -> bool *)
-fun is_quot_type _ (Type ("IntEx.my_int", _)) = true (* ### *)
+fun is_quot_type _ (Type ("IntEx.my_int", _)) = true (* FIXME *)
| is_quot_type _ _ = false
fun is_codatatype thy (T as Type (s, _)) =
not (null (AList.lookup (op =) (#codatatypes (Data.get thy)) s
@@ -615,9 +617,9 @@
| NONE => false)
| is_rep_fun _ _ = false
(* Proof.context -> styp -> bool *)
-fun is_quot_abs_fun _ ("IntEx.abs_my_int", _) = true (* ### *)
+fun is_quot_abs_fun _ ("IntEx.abs_my_int", _) = true (* FIXME *)
| is_quot_abs_fun _ _ = false
-fun is_quot_rep_fun _ ("IntEx.rep_my_int", _) = true (* ### *)
+fun is_quot_rep_fun _ ("IntEx.rep_my_int", _) = true (* FIXME *)
| is_quot_rep_fun _ _ = false
(* theory -> styp -> styp *)
@@ -648,12 +650,12 @@
end
handle TYPE ("dest_Type", _, _) => false
fun is_constr_like thy (s, T) =
- s = @{const_name FunBox} orelse s = @{const_name PairBox} orelse
+ member (op =) [@{const_name FunBox}, @{const_name PairBox},
+ @{const_name Quot}, @{const_name Zero_Rep},
+ @{const_name Suc_Rep}] s orelse
let val (x as (s, T)) = (s, unbit_and_unbox_type T) in
Refute.is_IDT_constructor thy x orelse is_record_constr x orelse
(is_abs_fun thy x andalso is_pure_typedef thy (range_type T)) orelse
- s = @{const_name Quot} orelse
- s = @{const_name Zero_Rep} orelse s = @{const_name Suc_Rep} orelse
x = (@{const_name zero_nat_inst.zero_nat}, nat_T) orelse
is_coconstr thy x
end
@@ -710,7 +712,8 @@
box_type ext_ctxt (in_fun_lhs_for boxy) T1
--> box_type ext_ctxt (in_fun_rhs_for boxy) T2
| Type (z as ("*", Ts)) =>
- if should_box_type ext_ctxt boxy z then
+ if boxy <> InConstr andalso boxy <> InSel
+ andalso should_box_type ext_ctxt boxy z then
Type (@{type_name pair_box}, map (box_type ext_ctxt InSel) Ts)
else
Type ("*", map (box_type ext_ctxt
@@ -778,11 +781,11 @@
fun zero_const T = Const (@{const_name zero_nat_inst.zero_nat}, T)
fun suc_const T = Const (@{const_name Suc}, T --> T)
-(* theory -> typ -> styp list *)
-fun uncached_datatype_constrs thy (T as Type (s, Ts)) =
+(* extended_context -> typ -> styp list *)
+fun uncached_datatype_constrs ({thy, stds, ...} : extended_context)
+ (T as Type (s, Ts)) =
(case AList.lookup (op =) (#codatatypes (Data.get thy)) s of
- SOME (_, xs' as (_ :: _)) =>
- map (apsnd (repair_constr_type thy T)) xs'
+ SOME (_, xs' as (_ :: _)) => map (apsnd (repair_constr_type thy T)) xs'
| _ =>
if is_datatype thy T then
case Datatype.get_info thy s of
@@ -793,6 +796,8 @@
map (fn (s', Us) =>
(s', map (Refute.typ_of_dtyp descr (dtyps ~~ Ts)) Us
---> T)) constrs
+ |> (triple_lookup (type_match thy) stds T |> the |> not) ?
+ cons (@{const_name NonStd}, @{typ \<xi>} --> T)
end
| NONE =>
if is_record_type T then
@@ -815,12 +820,11 @@
[])
| uncached_datatype_constrs _ _ = []
(* extended_context -> typ -> styp list *)
-fun datatype_constrs (ext_ctxt as {thy, constr_cache, ...} : extended_context)
- T =
+fun datatype_constrs (ext_ctxt as {constr_cache, ...}) T =
case AList.lookup (op =) (!constr_cache) T of
SOME xs => xs
| NONE =>
- let val xs = uncached_datatype_constrs thy T in
+ let val xs = uncached_datatype_constrs ext_ctxt T in
(Unsynchronized.change constr_cache (cons (T, xs)); xs)
end
fun boxed_datatype_constrs ext_ctxt =
@@ -838,6 +842,7 @@
AList.lookup (op =) (boxed_datatype_constrs ext_ctxt (domain_type T')) s
|> the |> pair s
end
+
(* extended_context -> styp -> term *)
fun discr_term_for_constr ext_ctxt (x as (s, T)) =
let val dataT = body_type T in
@@ -849,7 +854,6 @@
else
Abs (Name.uu, dataT, @{const True})
end
-
(* extended_context -> styp -> term -> term *)
fun discriminate_value (ext_ctxt as {thy, ...}) (x as (_, T)) t =
case strip_comb t of
@@ -919,7 +923,7 @@
(@{const_name Pair}, T1 --> T2 --> T)
end
else
- datatype_constrs ext_ctxt T |> the_single
+ datatype_constrs ext_ctxt T |> hd
val arg_Ts = binder_types T'
in
list_comb (Const x', map2 (select_nth_constr_arg thy x' t)
@@ -1361,10 +1365,9 @@
val normal_y = normal_t $ y_var
val is_unknown_t = Const (@{const_name is_unknown}, rep_T --> bool_T)
in
- [Logic.mk_equals (sel_a_t, normal_t $ sel_a_t),
+ [Logic.mk_equals (normal_t $ sel_a_t, sel_a_t),
Logic.list_implies
- ([@{const Not} $ (HOLogic.mk_eq (x_var, y_var)),
- @{const Not} $ (is_unknown_t $ normal_x),
+ ([@{const Not} $ (is_unknown_t $ normal_x),
@{const Not} $ (is_unknown_t $ normal_y),
equiv_rel $ x_var $ y_var] |> map HOLogic.mk_Trueprop,
Logic.mk_equals (normal_x, normal_y)),
@@ -1388,17 +1391,27 @@
fun optimized_case_def (ext_ctxt as {thy, ...}) dataT res_T =
let
val xs = datatype_constrs ext_ctxt dataT
- val func_Ts = map ((fn T => binder_types T ---> res_T) o snd) xs
- val (xs', x) = split_last xs
+ val xs' = filter_out (fn (s, _) => s = @{const_name NonStd}) xs
+ val func_Ts = map ((fn T => binder_types T ---> res_T) o snd) xs'
in
- constr_case_body thy (1, x)
- |> fold_rev (add_constr_case ext_ctxt res_T) (length xs downto 2 ~~ xs')
+ (if length xs = length xs' then
+ let
+ val (xs'', x) = split_last xs'
+ in
+ constr_case_body thy (1, x)
+ |> fold_rev (add_constr_case ext_ctxt res_T)
+ (length xs' downto 2 ~~ xs'')
+ end
+ else
+ Const (@{const_name undefined}, dataT --> res_T) $ Bound 0
+ |> fold_rev (add_constr_case ext_ctxt res_T)
+ (length xs' downto 1 ~~ xs'))
|> fold_rev (curry absdummy) (func_Ts @ [dataT])
end
(* extended_context -> string -> typ -> typ -> term -> term *)
fun optimized_record_get (ext_ctxt as {thy, ...}) s rec_T res_T t =
- let val constr_x = the_single (datatype_constrs ext_ctxt rec_T) in
+ let val constr_x = hd (datatype_constrs ext_ctxt rec_T) in
case no_of_record_field thy s rec_T of
~1 => (case rec_T of
Type (_, Ts as _ :: _) =>
@@ -1416,7 +1429,7 @@
(* extended_context -> string -> typ -> term -> term -> term *)
fun optimized_record_update (ext_ctxt as {thy, ...}) s rec_T fun_t rec_t =
let
- val constr_x as (_, constr_T) = the_single (datatype_constrs ext_ctxt rec_T)
+ val constr_x as (_, constr_T) = hd (datatype_constrs ext_ctxt rec_T)
val Ts = binder_types constr_T
val n = length Ts
val special_j = no_of_record_field thy s rec_T
@@ -1606,7 +1619,7 @@
case length ts of
0 => (do_term depth Ts (eta_expand Ts t 1), [])
| _ => (optimized_record_get ext_ctxt s (domain_type T)
- (range_type T) (hd ts), tl ts)
+ (range_type T) (do_term depth Ts (hd ts)), tl ts)
else if is_record_update thy x then
case length ts of
2 => (optimized_record_update ext_ctxt
@@ -2077,7 +2090,7 @@
(t0 as Const (@{const_name "=="}, _)) $ t1 $ t2 =>
do_eq_or_imp Ts true def t0 t1 t2 seen
| (t0 as @{const "==>"}) $ t1 $ t2 =>
- do_eq_or_imp Ts false def t0 t1 t2 seen
+ if def then (t, []) else do_eq_or_imp Ts false def t0 t1 t2 seen
| (t0 as Const (@{const_name "op ="}, _)) $ t1 $ t2 =>
do_eq_or_imp Ts true def t0 t1 t2 seen
| (t0 as @{const "op -->"}) $ t1 $ t2 =>
@@ -2126,27 +2139,33 @@
| aux _ t = t
(* bool -> bool -> term -> term -> term -> term *)
and aux_eq careful pass1 t0 t1 t2 =
- (if careful then
- raise SAME ()
- else if axiom andalso is_Var t2 andalso
- num_occs_of_var (dest_Var t2) = 1 then
- @{const True}
- else case strip_comb t2 of
- (Const (x as (s, T)), args) =>
- let val arg_Ts = binder_types T in
- if length arg_Ts = length args andalso
- (is_constr thy x orelse s = @{const_name Pair} orelse
- x = (@{const_name Suc}, nat_T --> nat_T)) andalso
- (not careful orelse not (is_Var t1) orelse
- String.isPrefix val_var_prefix (fst (fst (dest_Var t1)))) then
- discriminate_value ext_ctxt x t1 ::
- map3 (sel_eq x t1) (index_seq 0 (length args)) arg_Ts args
- |> foldr1 s_conj
- |> body_type (type_of t0) = prop_T ? HOLogic.mk_Trueprop
- else
- raise SAME ()
- end
- | _ => raise SAME ())
+ ((if careful then
+ raise SAME ()
+ else if axiom andalso is_Var t2 andalso
+ num_occs_of_var (dest_Var t2) = 1 then
+ @{const True}
+ else case strip_comb t2 of
+ (* The first case is not as general as it could be. *)
+ (Const (@{const_name PairBox}, _),
+ [Const (@{const_name fst}, _) $ Var z1,
+ Const (@{const_name snd}, _) $ Var z2]) =>
+ if z1 = z2 andalso num_occs_of_var z1 = 2 then @{const True}
+ else raise SAME ()
+ | (Const (x as (s, T)), args) =>
+ let val arg_Ts = binder_types T in
+ if length arg_Ts = length args andalso
+ (is_constr thy x orelse s = @{const_name Pair} orelse
+ x = (@{const_name Suc}, nat_T --> nat_T)) andalso
+ (not careful orelse not (is_Var t1) orelse
+ String.isPrefix val_var_prefix (fst (fst (dest_Var t1)))) then
+ discriminate_value ext_ctxt x t1 ::
+ map3 (sel_eq x t1) (index_seq 0 (length args)) arg_Ts args
+ |> foldr1 s_conj
+ else
+ raise SAME ()
+ end
+ | _ => raise SAME ())
+ |> body_type (type_of t0) = prop_T ? HOLogic.mk_Trueprop)
handle SAME () => if pass1 then aux_eq careful false t0 t2 t1
else t0 $ aux false t2 $ aux false t1
(* styp -> term -> int -> typ -> term -> term *)
@@ -2947,7 +2966,7 @@
| 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 ext_ctxt InFunRHS1 T2 in
+ let val T' = box_type ext_ctxt InSel T2 in
Const (@{const_name quot_normal}, T' --> T')
end
| Const (s as @{const_name Tha}, T) => do_description_operator s T
@@ -2960,7 +2979,8 @@
T
else if is_constr_like thy x then
box_type ext_ctxt InConstr T
- else if is_sel s orelse is_rep_fun thy x then
+ else if is_sel s
+ orelse is_rep_fun thy x then
box_type ext_ctxt InSel T
else
box_type ext_ctxt InExpr T)
@@ -3495,6 +3515,7 @@
#> simplify_constrs_and_sels thy
#> distribute_quantifiers
#> push_quantifiers_inward thy
+ #> Envir.eta_contract
#> not core ? Refute.close_form
#> shorten_abs_vars
in
--- a/src/HOL/Tools/Nitpick/nitpick_isar.ML Mon Feb 01 14:12:12 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_isar.ML Tue Feb 02 11:38:38 2010 +0100
@@ -1,6 +1,6 @@
(* Title: HOL/Tools/Nitpick/nitpick_isar.ML
Author: Jasmin Blanchette, TU Muenchen
- Copyright 2008, 2009
+ Copyright 2008, 2009, 2010
Adds the "nitpick" and "nitpick_params" commands to Isabelle/Isar's outer
syntax.
@@ -28,9 +28,8 @@
val _ =
ProofGeneralPgip.add_preference Preferences.category_tracing
- (Preferences.bool_pref auto
- "auto-nitpick"
- "Whether to run Nitpick automatically.")
+ (Preferences.bool_pref auto "auto-nitpick"
+ "Whether to run Nitpick automatically.")
type raw_param = string * string list
@@ -41,6 +40,7 @@
("bisim_depth", ["7"]),
("box", ["smart"]),
("mono", ["smart"]),
+ ("std", ["true"]),
("wf", ["smart"]),
("sat_solver", ["smart"]),
("batch_size", ["smart"]),
@@ -79,6 +79,7 @@
val negated_params =
[("dont_box", "box"),
("non_mono", "mono"),
+ ("non_std", "std"),
("non_wf", "wf"),
("non_blocking", "blocking"),
("satisfy", "falsify"),
@@ -110,8 +111,8 @@
AList.defined (op =) negated_params s orelse
s = "max" orelse s = "eval" orelse s = "expect" orelse
exists (fn p => String.isPrefix (p ^ " ") s)
- ["card", "max", "iter", "box", "dont_box", "mono", "non_mono", "wf",
- "non_wf", "format"]
+ ["card", "max", "iter", "box", "dont_box", "mono", "non_mono", "std",
+ "non_std", "wf", "non_wf", "format"]
(* string * 'a -> unit *)
fun check_raw_param (s, _) =
@@ -244,6 +245,14 @@
value |> stringify_raw_param_value
|> int_seq_from_string name min_int))
(filter (String.isPrefix (prefix ^ " ") o fst) raw_params)
+ (* (string -> 'a) -> string -> ('a option * bool) list *)
+ fun lookup_bool_assigns read prefix =
+ (NONE, lookup_bool prefix)
+ :: map (fn (name, value) =>
+ (SOME (read (String.extract (name, size prefix + 1, NONE))),
+ value |> stringify_raw_param_value
+ |> bool_option_from_string false name |> the))
+ (filter (String.isPrefix (prefix ^ " ") o fst) raw_params)
(* (string -> 'a) -> string -> ('a option * bool option) list *)
fun lookup_bool_option_assigns read prefix =
(NONE, lookup_bool_option prefix)
@@ -297,6 +306,7 @@
NONE
| (NONE, _) => NONE) cards_assigns
val monos = lookup_bool_option_assigns read_type_polymorphic "mono"
+ val stds = lookup_bool_assigns read_type_polymorphic "std"
val wfs = lookup_bool_option_assigns read_const_polymorphic "wf"
val sat_solver = lookup_string "sat_solver"
val blocking = not auto andalso lookup_bool "blocking"
@@ -339,9 +349,10 @@
in
{cards_assigns = cards_assigns, maxes_assigns = maxes_assigns,
iters_assigns = iters_assigns, bitss = bitss, bisim_depths = bisim_depths,
- boxes = boxes, monos = monos, wfs = wfs, sat_solver = sat_solver,
- blocking = blocking, falsify = falsify, debug = debug, verbose = verbose,
- overlord = overlord, user_axioms = user_axioms, assms = assms,
+ boxes = boxes, monos = monos, stds = stds, wfs = wfs,
+ sat_solver = sat_solver, blocking = blocking, falsify = falsify,
+ debug = debug, verbose = verbose, overlord = overlord,
+ user_axioms = user_axioms, assms = assms,
merge_type_vars = merge_type_vars, binary_ints = binary_ints,
destroy_constrs = destroy_constrs, specialize = specialize,
skolemize = skolemize, star_linear_preds = star_linear_preds,
@@ -416,8 +427,9 @@
| Refute.REFUTE (loc, details) =>
error ("Unhandled Refute error (" ^ quote loc ^ "): " ^ details ^ ".")
-(* raw_param list -> bool -> int -> Proof.state -> bool * Proof.state *)
-fun pick_nits override_params auto i state =
+
+(* raw_param list -> bool -> int -> int -> Proof.state -> bool * Proof.state *)
+fun pick_nits override_params auto i step state =
let
val thy = Proof.theory_of state
val ctxt = Proof.context_of state
@@ -431,7 +443,7 @@
|> (if auto then perhaps o try
else if debug then fn f => fn x => f x
else handle_exceptions ctxt)
- (fn (_, state) => pick_nits_in_subgoal state params auto i
+ (fn (_, state) => pick_nits_in_subgoal state params auto i step
|>> curry (op =) "genuine")
in
if auto orelse blocking then go ()
@@ -441,9 +453,9 @@
(* raw_param list option * int option -> Toplevel.transition
-> Toplevel.transition *)
fun nitpick_trans (opt_params, opt_i) =
- Toplevel.keep (K ()
- o snd o pick_nits (these opt_params) false (the_default 1 opt_i)
- o Toplevel.proof_of)
+ Toplevel.keep (fn st =>
+ (pick_nits (these opt_params) false (the_default 1 opt_i)
+ (Toplevel.proof_position_of st) (Toplevel.proof_of st); ()))
(* raw_param -> string *)
fun string_for_raw_param (name, value) =
@@ -477,7 +489,7 @@
(* Proof.state -> bool * Proof.state *)
fun auto_nitpick state =
- if not (!auto) then (false, state) else pick_nits [] true 1 state
+ if not (!auto) then (false, state) else pick_nits [] true 1 0 state
val setup = Auto_Counterexample.register_tool ("nitpick", auto_nitpick)
--- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Mon Feb 01 14:12:12 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Tue Feb 02 11:38:38 2010 +0100
@@ -1,6 +1,6 @@
(* Title: HOL/Tools/Nitpick/nitpick_kodkod.ML
Author: Jasmin Blanchette, TU Muenchen
- Copyright 2008, 2009
+ Copyright 2008, 2009, 2010
Kodkod problem generator part of Kodkod.
*)
@@ -285,8 +285,8 @@
(* Proof.context -> bool -> string -> typ -> rep -> string *)
fun bound_comment ctxt debug nick T R =
short_name nick ^
- (if debug then " :: " ^ plain_string_from_yxml (Syntax.string_of_typ ctxt T)
- else "") ^ " : " ^ string_for_rep R
+ (if debug then " :: " ^ unyxml (Syntax.string_of_typ ctxt T) else "") ^
+ " : " ^ string_for_rep R
(* Proof.context -> bool -> nut -> KK.bound *)
fun bound_for_plain_rel ctxt debug (u as FreeRel (x, T, R, nick)) =
@@ -754,7 +754,7 @@
(* extended_context -> kodkod_constrs -> nut NameTable.table -> dtype_spec list
-> dtype_spec -> nfa_entry option *)
fun nfa_entry_for_datatype _ _ _ _ ({co = true, ...} : dtype_spec) = NONE
- | nfa_entry_for_datatype _ _ _ _ {shallow = true, ...} = NONE
+ | nfa_entry_for_datatype _ _ _ _ {deep = false, ...} = NONE
| nfa_entry_for_datatype ext_ctxt kk rel_table dtypes {typ, constrs, ...} =
SOME (typ, maps (nfa_transitions_for_constr ext_ctxt kk rel_table dtypes
o #const) constrs)
@@ -926,7 +926,7 @@
(* extended_context -> int -> int Typtab.table -> kodkod_constrs
-> nut NameTable.table -> dtype_spec -> KK.formula list *)
-fun other_axioms_for_datatype _ _ _ _ _ {shallow = true, ...} = []
+fun other_axioms_for_datatype _ _ _ _ _ {deep = false, ...} = []
| other_axioms_for_datatype ext_ctxt bits ofs kk rel_table
(dtype as {typ, ...}) =
let val j0 = offset_of_type ofs typ in
--- a/src/HOL/Tools/Nitpick/nitpick_model.ML Mon Feb 01 14:12:12 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_model.ML Tue Feb 02 11:38:38 2010 +0100
@@ -1,6 +1,6 @@
(* Title: HOL/Tools/Nitpick/nitpick_model.ML
Author: Jasmin Blanchette, TU Muenchen
- Copyright 2009
+ Copyright 2009, 2010
Model reconstruction for Nitpick.
*)
@@ -53,7 +53,8 @@
val base_mixfix = "_\<^bsub>base\<^esub>"
val step_mixfix = "_\<^bsub>step\<^esub>"
val abs_mixfix = "\<guillemotleft>_\<guillemotright>"
-val non_opt_name = nitpick_prefix ^ "non_opt"
+val opt_flag = nitpick_prefix ^ "opt"
+val non_opt_flag = nitpick_prefix ^ "non_opt"
(* string -> int -> string *)
fun atom_suffix s j =
@@ -62,7 +63,10 @@
? prefix "\<^isub>,"
(* string -> typ -> int -> string *)
fun atom_name prefix (T as Type (s, _)) j =
- prefix ^ substring (shortest_name s, 0, 1) ^ atom_suffix s j
+ let val s' = shortest_name s in
+ prefix ^ (if String.isPrefix "\\" s' then s' else substring (s', 0, 1)) ^
+ atom_suffix s j
+ end
| atom_name prefix (T as TFree (s, _)) j =
prefix ^ perhaps (try (unprefix "'")) s ^ atom_suffix s j
| atom_name _ T _ = raise TYPE ("Nitpick_Model.atom_name", [T], [])
@@ -139,23 +143,21 @@
let
(* typ -> typ -> (term * term) list -> term *)
fun aux T1 T2 [] =
- Const (if maybe_opt orelse T2 <> bool_T then @{const_name undefined}
- else non_opt_name, T1 --> T2)
+ Const (if maybe_opt then opt_flag else non_opt_flag, T1 --> T2)
| aux T1 T2 ((t1, t2) :: ps) =
Const (@{const_name fun_upd}, (T1 --> T2) --> T1 --> T2 --> T1 --> T2)
$ aux T1 T2 ps $ t1 $ t2
in aux T1 T2 o rev end
(* term -> bool *)
-fun is_plain_fun (Const (s, _)) =
- (s = @{const_name undefined} orelse s = non_opt_name)
+fun is_plain_fun (Const (s, _)) = (s = opt_flag orelse s = non_opt_flag)
| is_plain_fun (Const (@{const_name fun_upd}, _) $ t0 $ _ $ _) =
is_plain_fun t0
| is_plain_fun _ = false
(* term -> bool * (term list * term list) *)
val dest_plain_fun =
let
- (* term -> term list * term list *)
- fun aux (Const (s, _)) = (s <> non_opt_name, ([], []))
+ (* term -> bool * (term list * term list) *)
+ fun aux (Const (s, _)) = (s <> non_opt_flag, ([], []))
| aux (Const (@{const_name fun_upd}, _) $ t0 $ t1 $ t2) =
let val (s, (ts1, ts2)) = aux t0 in (s, (t1 :: ts1, t2 :: ts2)) end
| aux t = raise TERM ("Nitpick_Model.dest_plain_fun", [t])
@@ -300,7 +302,7 @@
aux' ps
in aux end
(* typ list -> term -> term *)
- fun setify_mapify_funs Ts t =
+ fun polish_funs Ts t =
(case fastype_of1 (Ts, t) of
Type ("fun", [T1, T2]) =>
if is_plain_fun t then
@@ -308,7 +310,7 @@
@{typ bool} =>
let
val (maybe_opt, ts_pair) =
- dest_plain_fun t ||> pairself (map (setify_mapify_funs Ts))
+ dest_plain_fun t ||> pairself (map (polish_funs Ts))
in
make_set maybe_opt T1 T2
(sort_wrt (truth_const_sort_key o snd) (op ~~ ts_pair))
@@ -316,7 +318,7 @@
| Type (@{type_name option}, [T2']) =>
let
val ts_pair = snd (dest_plain_fun t)
- |> pairself (map (setify_mapify_funs Ts))
+ |> pairself (map (polish_funs Ts))
in make_map T1 T2 T2' (rev (op ~~ ts_pair)) end
| _ => raise SAME ()
else
@@ -324,9 +326,18 @@
| _ => raise SAME ())
handle SAME () =>
case t of
- t1 $ t2 => setify_mapify_funs Ts t1 $ setify_mapify_funs Ts t2
- | Abs (s, T, t') => Abs (s, T, setify_mapify_funs (T :: Ts) t')
- | _ => t
+ (t1 as Const (@{const_name fun_upd}, _) $ t11 $ _)
+ $ (t2 as Const (s, _)) =>
+ if s = unknown then polish_funs Ts t11
+ else polish_funs Ts t1 $ polish_funs Ts t2
+ | t1 $ t2 => polish_funs Ts t1 $ polish_funs Ts t2
+ | Abs (s, T, t') => Abs (s, T, polish_funs (T :: Ts) t')
+ | Const (s, Type ("fun", [T1, T2])) =>
+ if s = opt_flag orelse s = non_opt_flag then
+ Abs ("x", T1, Const (unknown, T2))
+ else
+ t
+ | t => t
(* bool -> typ -> typ -> typ -> term list -> term list -> term *)
fun make_fun maybe_opt T1 T2 T' ts1 ts2 =
ts1 ~~ ts2 |> sort (nice_term_ord o pairself fst)
@@ -371,7 +382,7 @@
HOLogic.mk_number nat_T j
else case datatype_spec datatypes T of
NONE => atom for_auto T j
- | SOME {shallow = true, ...} => atom for_auto T j
+ | SOME {deep = false, ...} => atom for_auto T j
| SOME {co, constrs, ...} =>
let
(* styp -> int list *)
@@ -437,13 +448,16 @@
| n2 => Const (@{const_name Algebras.divide},
num_T --> num_T --> num_T)
$ mk_num n1 $ mk_num n2)
- | _ => raise TERM ("Nitpick_Model.reconstruct_term.term_\
- \for_atom (Abs_Frac)", ts)
+ | _ => raise TERM ("Nitpick_Model.reconstruct_term.\
+ \term_for_atom (Abs_Frac)", ts)
end
else if not for_auto andalso
(is_abs_fun thy constr_x orelse
constr_s = @{const_name Quot}) then
Const (abs_name, constr_T) $ the_single ts
+ else if not for_auto andalso
+ constr_s = @{const_name NonStd} then
+ Const (fst (dest_Const (the_single ts)), T)
else
list_comb (Const constr_x, ts)
in
@@ -509,8 +523,7 @@
Refute.string_of_typ T ^ " " ^ string_for_rep R ^ " " ^
string_of_int (length jss))
in
- (not for_auto ? setify_mapify_funs []) o unbit_and_unbox_term
- oooo term_for_rep []
+ (not for_auto ? polish_funs []) o unbit_and_unbox_term oooo term_for_rep []
end
(* scope -> nut list -> nut NameTable.table -> KK.raw_bound list -> nut
@@ -522,8 +535,7 @@
(rep_of name)
end
-(* Proof.context
- -> (string * string * string * string * string) * Proof.context *)
+(* Proof.context -> (string * string * string * string) * Proof.context *)
fun add_wacky_syntax ctxt =
let
(* term -> string *)
@@ -573,13 +585,13 @@
-> nut list -> nut list -> nut NameTable.table -> KK.raw_bound list
-> Pretty.T * bool *)
fun reconstruct_hol_model {show_skolems, show_datatypes, show_consts}
- ({ext_ctxt as {thy, ctxt, max_bisim_depth, boxes, wfs, user_axioms,
- debug, binary_ints, destroy_constrs, specialize,
- skolemize, star_linear_preds, uncurry, fast_descrs,
- tac_timeout, evals, case_names, def_table, nondef_table,
- user_nondefs, simp_table, psimp_table, intro_table,
- ground_thm_table, ersatz_table, skolems, special_funs,
- unrolled_preds, wf_cache, constr_cache},
+ ({ext_ctxt as {thy, ctxt, max_bisim_depth, boxes, stds, wfs,
+ user_axioms, debug, binary_ints, destroy_constrs,
+ specialize, skolemize, star_linear_preds, uncurry,
+ fast_descrs, tac_timeout, evals, case_names, def_table,
+ nondef_table, user_nondefs, simp_table, psimp_table,
+ intro_table, ground_thm_table, ersatz_table, skolems,
+ special_funs, unrolled_preds, wf_cache, constr_cache},
card_assigns, bits, bisim_depth, datatypes, ofs} : scope)
formats all_frees free_names sel_names nonsel_names rel_table bounds =
let
@@ -587,7 +599,7 @@
add_wacky_syntax ctxt
val ext_ctxt =
{thy = thy, ctxt = ctxt, max_bisim_depth = max_bisim_depth, boxes = boxes,
- wfs = wfs, user_axioms = user_axioms, debug = debug,
+ stds = stds, wfs = wfs, user_axioms = user_axioms, debug = debug,
binary_ints = binary_ints, destroy_constrs = destroy_constrs,
specialize = specialize, skolemize = skolemize,
star_linear_preds = star_linear_preds, uncurry = uncurry,
@@ -650,16 +662,15 @@
Pretty.block (Pretty.breaks
[Syntax.pretty_typ ctxt (unbit_and_unbox_type typ), Pretty.str "=",
Pretty.enum "," "{" "}"
- (map (Syntax.pretty_term ctxt) (all_values_of_type card typ)
- @ (if complete then [] else [Pretty.str unrep]))])
+ (map (Syntax.pretty_term ctxt) (all_values_of_type card typ) @
+ (if complete then [] else [Pretty.str unrep]))])
(* typ -> dtype_spec list *)
fun integer_datatype T =
[{typ = T, card = card_of_type card_assigns T, co = false,
- complete = false, concrete = true, shallow = false, constrs = []}]
+ complete = false, concrete = true, deep = true, constrs = []}]
handle TYPE ("Nitpick_HOL.card_of_type", _, _) => []
val (codatatypes, datatypes) =
- datatypes |> filter_out #shallow
- |> List.partition #co
+ datatypes |> filter #deep |> List.partition #co
||> append (integer_datatype nat_T @ integer_datatype int_T)
val block_of_datatypes =
if show_datatypes andalso not (null datatypes) then
--- a/src/HOL/Tools/Nitpick/nitpick_mono.ML Mon Feb 01 14:12:12 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML Tue Feb 02 11:38:38 2010 +0100
@@ -1,16 +1,17 @@
(* Title: HOL/Tools/Nitpick/nitpick_mono.ML
Author: Jasmin Blanchette, TU Muenchen
- Copyright 2009
+ Copyright 2009, 2010
Monotonicity predicate for higher-order logic.
*)
signature NITPICK_MONO =
sig
+ datatype sign = Plus | Minus
type extended_context = Nitpick_HOL.extended_context
val formulas_monotonic :
- extended_context -> typ -> term list -> term list -> term -> bool
+ extended_context -> typ -> sign -> term list -> term list -> term -> bool
end;
structure Nitpick_Mono : NITPICK_MONO =
@@ -21,7 +22,7 @@
type var = int
-datatype sign = Pos | Neg
+datatype sign = Plus | Minus
datatype sign_atom = S of sign | V of var
type literal = var * sign
@@ -54,13 +55,13 @@
if null xs then "" else "\<^bsub>" ^ string_for_vars sep xs ^ "\<^esub>"
(* sign -> string *)
-fun string_for_sign Pos = "+"
- | string_for_sign Neg = "-"
+fun string_for_sign Plus = "+"
+ | string_for_sign Minus = "-"
(* sign -> sign -> sign *)
-fun xor sn1 sn2 = if sn1 = sn2 then Pos else Neg
+fun xor sn1 sn2 = if sn1 = sn2 then Plus else Minus
(* sign -> sign *)
-val negate = xor Neg
+val negate = xor Minus
(* sign_atom -> string *)
fun string_for_sign_atom (S sn) = string_for_sign sn
@@ -152,7 +153,7 @@
(* string * typ list -> ctype list -> ctype *)
fun constr_ctype_for_binders z Cs =
- fold_rev (fn C => curry3 CFun C (S Neg)) Cs (CRec z)
+ fold_rev (fn C => curry3 CFun C (S Minus)) Cs (CRec z)
(* ((string * typ list) * ctype) list -> ctype list -> ctype -> ctype *)
fun repair_ctype _ _ CAlpha = CAlpha
@@ -199,7 +200,7 @@
exists_alpha_sub_ctype_fresh C1 then
V (Unsynchronized.inc max_fresh)
else
- S Neg
+ S Minus
in CFun (C1, a, C2) end
(* typ -> ctype *)
and do_type T =
@@ -252,13 +253,13 @@
fun prodC_factors (CPair (C1, C2)) = maps prodC_factors [C1, C2]
| prodC_factors C = [C]
(* ctype -> ctype list * ctype *)
-fun curried_strip_ctype (CFun (C1, S Neg, C2)) =
+fun curried_strip_ctype (CFun (C1, S Minus, C2)) =
curried_strip_ctype C2 |>> append (prodC_factors C1)
| curried_strip_ctype C = ([], C)
(* string -> ctype -> ctype *)
fun sel_ctype_from_constr_ctype s C =
let val (arg_Cs, dataC) = curried_strip_ctype C in
- CFun (dataC, S Neg,
+ CFun (dataC, S Minus,
case sel_no_from_name s of ~1 => bool_C | n => nth arg_Cs n)
end
@@ -268,8 +269,13 @@
if could_exist_alpha_sub_ctype thy alpha_T T then
case AList.lookup (op =) (!constr_cache) x of
SOME C => C
- | NONE => (fresh_ctype_for_type cdata (body_type T);
- AList.lookup (op =) (!constr_cache) x |> the)
+ | NONE => if T = alpha_T then
+ let val C = fresh_ctype_for_type cdata T in
+ (Unsynchronized.change constr_cache (cons (x, C)); C)
+ end
+ else
+ (fresh_ctype_for_type cdata (body_type T);
+ AList.lookup (op =) (!constr_cache) x |> the)
else
fresh_ctype_for_type cdata T
fun ctype_for_sel (cdata as {ext_ctxt, ...}) (x as (s, _)) =
@@ -332,9 +338,9 @@
| _ => do_sign_atom_comp Eq [] a2 a1 accum)
| do_sign_atom_comp Leq [] a1 a2 (accum as (lits, comps)) =
(case (a1, a2) of
- (_, S Neg) => SOME accum
- | (S Pos, _) => SOME accum
- | (S Neg, S Pos) => NONE
+ (_, S Minus) => SOME accum
+ | (S Plus, _) => SOME accum
+ | (S Minus, S Plus) => NONE
| (V _, V _) => SOME (lits, insert (op =) (a1, a2, Leq, []) comps)
| _ => do_sign_atom_comp Eq [] a1 a2 accum)
| do_sign_atom_comp cmp xs a1 a2 (accum as (lits, comps)) =
@@ -354,8 +360,8 @@
accum |> do_sign_atom_comp Leq xs a1 a2
|> do_ctype_comp Leq xs C21 C11
|> (case a2 of
- S Neg => I
- | S Pos => do_ctype_comp Leq xs C11 C21
+ S Minus => I
+ | S Plus => do_ctype_comp Leq xs C11 C21
| V x => do_ctype_comp Leq (x :: xs) C11 C21)
else
SOME accum)
@@ -386,29 +392,33 @@
(* sign -> sign_expr -> ctype -> (literal list * sign_expr list) option
-> (literal list * sign_expr list) option *)
fun do_notin_ctype_fv _ _ _ NONE = NONE
- | do_notin_ctype_fv Neg _ CAlpha accum = accum
- | do_notin_ctype_fv Pos [] CAlpha _ = NONE
- | do_notin_ctype_fv Pos [(x, sn)] CAlpha (SOME (lits, sexps)) =
+ | do_notin_ctype_fv Minus _ CAlpha accum = accum
+ | do_notin_ctype_fv Plus [] CAlpha _ = NONE
+ | do_notin_ctype_fv Plus [(x, sn)] CAlpha (SOME (lits, sexps)) =
SOME lits |> do_literal (x, sn) |> Option.map (rpair sexps)
- | do_notin_ctype_fv Pos sexp CAlpha (SOME (lits, sexps)) =
+ | do_notin_ctype_fv Plus sexp CAlpha (SOME (lits, sexps)) =
SOME (lits, insert (op =) sexp sexps)
| do_notin_ctype_fv sn sexp (CFun (C1, S sn', C2)) accum =
- accum |> (if sn' = Pos andalso sn = Pos then do_notin_ctype_fv Pos sexp C1
- else I)
- |> (if sn' = Neg orelse sn = Pos then do_notin_ctype_fv Neg sexp C1
- else I)
+ accum |> (if sn' = Plus andalso sn = Plus then
+ do_notin_ctype_fv Plus sexp C1
+ else
+ I)
+ |> (if sn' = Minus orelse sn = Plus then
+ do_notin_ctype_fv Minus sexp C1
+ else
+ I)
|> do_notin_ctype_fv sn sexp C2
- | do_notin_ctype_fv Pos sexp (CFun (C1, V x, C2)) accum =
- accum |> (case do_literal (x, Neg) (SOME sexp) of
+ | do_notin_ctype_fv Plus sexp (CFun (C1, V x, C2)) accum =
+ accum |> (case do_literal (x, Minus) (SOME sexp) of
NONE => I
- | SOME sexp' => do_notin_ctype_fv Pos sexp' C1)
- |> do_notin_ctype_fv Neg sexp C1
- |> do_notin_ctype_fv Pos sexp C2
- | do_notin_ctype_fv Neg sexp (CFun (C1, V x, C2)) accum =
- accum |> (case do_literal (x, Pos) (SOME sexp) of
+ | SOME sexp' => do_notin_ctype_fv Plus sexp' C1)
+ |> do_notin_ctype_fv Minus sexp C1
+ |> do_notin_ctype_fv Plus sexp C2
+ | do_notin_ctype_fv Minus sexp (CFun (C1, V x, C2)) accum =
+ accum |> (case do_literal (x, Plus) (SOME sexp) of
NONE => I
- | SOME sexp' => do_notin_ctype_fv Pos sexp' C1)
- |> do_notin_ctype_fv Neg sexp C2
+ | SOME sexp' => do_notin_ctype_fv Plus sexp' C1)
+ |> do_notin_ctype_fv Minus sexp C2
| do_notin_ctype_fv sn sexp (CPair (C1, C2)) accum =
accum |> fold (do_notin_ctype_fv sn sexp) [C1, C2]
| do_notin_ctype_fv sn sexp (CType (_, Cs)) accum =
@@ -420,14 +430,14 @@
fun add_notin_ctype_fv _ _ UnsolvableCSet = UnsolvableCSet
| add_notin_ctype_fv sn C (CSet (lits, comps, sexps)) =
(print_g ("*** Add " ^ string_for_ctype C ^ " is right-" ^
- (case sn of Neg => "unique" | Pos => "total") ^ ".");
+ (case sn of Minus => "unique" | Plus => "total") ^ ".");
case do_notin_ctype_fv sn [] C (SOME (lits, sexps)) of
NONE => (print_g "**** Unsolvable"; UnsolvableCSet)
| SOME (lits, sexps) => CSet (lits, comps, sexps))
(* ctype -> constraint_set -> constraint_set *)
-val add_ctype_is_right_unique = add_notin_ctype_fv Neg
-val add_ctype_is_right_total = add_notin_ctype_fv Pos
+val add_ctype_is_right_unique = add_notin_ctype_fv Minus
+val add_ctype_is_right_total = add_notin_ctype_fv Plus
(* constraint_set -> constraint_set -> constraint_set *)
fun unite (CSet (lits1, comps1, sexps1)) (CSet (lits2, comps2, sexps2)) =
@@ -437,11 +447,11 @@
| unite _ _ = UnsolvableCSet
(* sign -> bool *)
-fun bool_from_sign Pos = false
- | bool_from_sign Neg = true
+fun bool_from_sign Plus = false
+ | bool_from_sign Minus = true
(* bool -> sign *)
-fun sign_from_bool false = Pos
- | sign_from_bool true = Neg
+fun sign_from_bool false = Plus
+ | sign_from_bool true = Minus
(* literal -> PropLogic.prop_formula *)
fun prop_for_literal (x, sn) =
@@ -460,10 +470,10 @@
PropLogic.SAnd (prop_for_comp (a1, a2, Leq, []),
prop_for_comp (a2, a1, Leq, []))
| prop_for_comp (a1, a2, Leq, []) =
- PropLogic.SOr (prop_for_sign_atom_eq (a1, Pos),
- prop_for_sign_atom_eq (a2, Neg))
+ PropLogic.SOr (prop_for_sign_atom_eq (a1, Plus),
+ prop_for_sign_atom_eq (a2, Minus))
| prop_for_comp (a1, a2, cmp, xs) =
- PropLogic.SOr (prop_for_exists_eq xs Neg, prop_for_comp (a1, a2, cmp, []))
+ PropLogic.SOr (prop_for_exists_eq xs Minus, prop_for_comp (a1, a2, cmp, []))
(* var -> (int -> bool option) -> literal list -> literal list *)
fun literals_from_assignments max_var assigns lits =
@@ -491,7 +501,7 @@
(* literal list -> unit *)
fun print_solution lits =
- let val (pos, neg) = List.partition (curry (op =) Pos o snd) lits in
+ let val (pos, neg) = List.partition (curry (op =) Plus o snd) lits in
print_g ("*** Solution:\n" ^
"+: " ^ commas (map (string_for_var o fst) pos) ^ "\n" ^
"-: " ^ commas (map (string_for_var o fst) neg))
@@ -523,7 +533,7 @@
type ctype_context =
{bounds: ctype list,
frees: (styp * ctype) list,
- consts: (styp * ctype_schema) list}
+ consts: (styp * ctype) list}
type accumulator = ctype_context * constraint_set
@@ -546,20 +556,20 @@
val ctype_for = fresh_ctype_for_type cdata
(* ctype -> ctype *)
fun pos_set_ctype_for_dom C =
- CFun (C, S (if exists_alpha_sub_ctype C then Pos else Neg), bool_C)
+ CFun (C, S (if exists_alpha_sub_ctype C then Plus else Minus), bool_C)
(* typ -> accumulator -> ctype * accumulator *)
fun do_quantifier T (gamma, cset) =
let
val abs_C = ctype_for (domain_type (domain_type T))
val body_C = ctype_for (range_type T)
in
- (CFun (CFun (abs_C, S Neg, body_C), S Neg, body_C),
+ (CFun (CFun (abs_C, S Minus, body_C), S Minus, body_C),
(gamma, cset |> add_ctype_is_right_total abs_C))
end
fun do_equals T (gamma, cset) =
let val C = ctype_for (domain_type T) in
- (CFun (C, S Neg, CFun (C, V (Unsynchronized.inc max_fresh),
- ctype_for (nth_range_type 2 T))),
+ (CFun (C, S Minus, CFun (C, V (Unsynchronized.inc max_fresh),
+ ctype_for (nth_range_type 2 T))),
(gamma, cset |> add_ctype_is_right_unique C))
end
fun do_robust_set_operation T (gamma, cset) =
@@ -569,7 +579,7 @@
val C2 = ctype_for set_T
val C3 = ctype_for set_T
in
- (CFun (C1, S Neg, CFun (C2, S Neg, C3)),
+ (CFun (C1, S Minus, CFun (C2, S Minus, C3)),
(gamma, cset |> add_is_sub_ctype C1 C3 |> add_is_sub_ctype C2 C3))
end
fun do_fragile_set_operation T (gamma, cset) =
@@ -579,7 +589,7 @@
(* typ -> ctype *)
fun custom_ctype_for (T as Type ("fun", [T1, T2])) =
if T = set_T then set_C
- else CFun (custom_ctype_for T1, S Neg, custom_ctype_for T2)
+ else CFun (custom_ctype_for T1, S Minus, custom_ctype_for T2)
| custom_ctype_for T = ctype_for T
in
(custom_ctype_for T, (gamma, cset |> add_ctype_is_right_unique set_C))
@@ -588,13 +598,13 @@
fun do_pair_constr T accum =
case ctype_for (nth_range_type 2 T) of
C as CPair (a_C, b_C) =>
- (CFun (a_C, S Neg, CFun (b_C, S Neg, C)), accum)
+ (CFun (a_C, S Minus, CFun (b_C, S Minus, C)), accum)
| C => raise CTYPE ("Nitpick_Mono.consider_term.do_pair_constr", [C])
(* int -> typ -> accumulator -> ctype * accumulator *)
fun do_nth_pair_sel n T =
case ctype_for (domain_type T) of
C as CPair (a_C, b_C) =>
- pair (CFun (C, S Neg, if n = 0 then a_C else b_C))
+ pair (CFun (C, S Minus, if n = 0 then a_C else b_C))
| C => raise CTYPE ("Nitpick_Mono.consider_term.do_nth_pair_sel", [C])
val unsolvable = (CType ("unsolvable", []), unsolvable_accum)
(* typ -> term -> accumulator -> ctype * accumulator *)
@@ -613,7 +623,7 @@
(case t of
Const (x as (s, T)) =>
(case AList.lookup (op =) consts x of
- SOME (C, cset') => (C, (gamma, cset |> unite cset'))
+ SOME C => (C, accum)
| NONE =>
if not (could_exist_alpha_subtype alpha_T T) then
(ctype_for T, accum)
@@ -627,12 +637,12 @@
| @{const_name Eps} => (print_g "*** Eps"; unsolvable)
| @{const_name If} =>
do_robust_set_operation (range_type T) accum
- |>> curry3 CFun bool_C (S Neg)
+ |>> curry3 CFun bool_C (S Minus)
| @{const_name Pair} => do_pair_constr T accum
| @{const_name fst} => do_nth_pair_sel 0 T accum
| @{const_name snd} => do_nth_pair_sel 1 T accum
| @{const_name Id} =>
- (CFun (ctype_for (domain_type T), S Neg, bool_C), accum)
+ (CFun (ctype_for (domain_type T), S Minus, bool_C), accum)
| @{const_name insert} =>
let
val set_T = domain_type (range_type T)
@@ -641,7 +651,7 @@
val C2 = ctype_for set_T
val C3 = ctype_for set_T
in
- (CFun (C1, S Neg, CFun (C2, S Neg, C3)),
+ (CFun (C1, S Minus, CFun (C2, S Minus, C3)),
(gamma, cset |> add_ctype_is_right_unique C1
|> add_is_sub_ctype C1' C3
|> add_is_sub_ctype C2 C3))
@@ -654,7 +664,7 @@
CFun (ctype_for (domain_type T), V x, bool_C)
val ab_set_C = domain_type T |> ctype_for_set
val ba_set_C = range_type T |> ctype_for_set
- in (CFun (ab_set_C, S Neg, ba_set_C), accum) end
+ in (CFun (ab_set_C, S Minus, ba_set_C), accum) end
| @{const_name trancl} => do_fragile_set_operation T accum
| @{const_name rtrancl} => (print_g "*** rtrancl"; unsolvable)
| @{const_name lower_semilattice_fun_inst.inf_fun} =>
@@ -663,7 +673,7 @@
do_robust_set_operation T accum
| @{const_name finite} =>
let val C1 = ctype_for (domain_type (domain_type T)) in
- (CFun (pos_set_ctype_for_dom C1, S Neg, bool_C), accum)
+ (CFun (pos_set_ctype_for_dom C1, S Minus, bool_C), accum)
end
| @{const_name rel_comp} =>
let
@@ -675,7 +685,7 @@
val ab_set_C = domain_type (range_type T) |> ctype_for_set
val ac_set_C = nth_range_type 2 T |> ctype_for_set
in
- (CFun (bc_set_C, S Neg, CFun (ab_set_C, S Neg, ac_set_C)),
+ (CFun (bc_set_C, S Minus, CFun (ab_set_C, S Minus, ac_set_C)),
accum)
end
| @{const_name image} =>
@@ -683,8 +693,8 @@
val a_C = ctype_for (domain_type (domain_type T))
val b_C = ctype_for (range_type (domain_type T))
in
- (CFun (CFun (a_C, S Neg, b_C), S Neg,
- CFun (pos_set_ctype_for_dom a_C, S Neg,
+ (CFun (CFun (a_C, S Minus, b_C), S Minus,
+ CFun (pos_set_ctype_for_dom a_C, S Minus,
pos_set_ctype_for_dom b_C)), accum)
end
| @{const_name Sigma} =>
@@ -698,11 +708,11 @@
val b_set_C = ctype_for_set (range_type (domain_type
(range_type T)))
val a_set_C = ctype_for_set a_set_T
- val a_to_b_set_C = CFun (a_C, S Neg, b_set_C)
+ val a_to_b_set_C = CFun (a_C, S Minus, b_set_C)
val ab_set_C = ctype_for_set (nth_range_type 2 T)
in
- (CFun (a_set_C, S Neg, CFun (a_to_b_set_C, S Neg, ab_set_C)),
- accum)
+ (CFun (a_set_C, S Minus,
+ CFun (a_to_b_set_C, S Minus, ab_set_C)), accum)
end
| @{const_name minus_fun_inst.minus_fun} =>
let
@@ -710,8 +720,8 @@
val left_set_C = ctype_for set_T
val right_set_C = ctype_for set_T
in
- (CFun (left_set_C, S Neg,
- CFun (right_set_C, S Neg, left_set_C)),
+ (CFun (left_set_C, S Minus,
+ CFun (right_set_C, S Minus, left_set_C)),
(gamma, cset |> add_ctype_is_right_unique right_set_C
|> add_is_sub_ctype right_set_C left_set_C))
end
@@ -721,15 +731,15 @@
let
val a_C = ctype_for (domain_type (domain_type T))
val a_set_C = pos_set_ctype_for_dom a_C
- in (CFun (a_set_C, S Neg, a_C), accum) end
+ in (CFun (a_set_C, S Minus, a_C), accum) end
| @{const_name FunBox} =>
let val dom_C = ctype_for (domain_type T) in
- (CFun (dom_C, S Neg, dom_C), accum)
+ (CFun (dom_C, S Minus, dom_C), accum)
end
| _ => if is_sel s then
if constr_name_for_sel_like s = @{const_name FunBox} then
let val dom_C = ctype_for (domain_type T) in
- (CFun (dom_C, S Neg, dom_C), accum)
+ (CFun (dom_C, S Minus, dom_C), accum)
end
else
(ctype_for_sel cdata x, accum)
@@ -740,7 +750,10 @@
SOME t' => do_term t' accum
| NONE => (print_g ("*** built-in " ^ s); unsolvable)
else
- (ctype_for T, accum))
+ let val C = ctype_for T in
+ (C, ({bounds = bounds, frees = frees,
+ consts = (x, C) :: consts}, cset))
+ end)
| Free (x as (_, T)) =>
(case AList.lookup (op =) frees x of
SOME C => (C, accum)
@@ -756,7 +769,7 @@
let
val C = ctype_for T
val (C', accum) = do_term t' (accum |>> push_bound C)
- in (CFun (C, S Neg, C'), accum |>> pop_bound) end
+ in (CFun (C, S Minus, C'), accum |>> pop_bound) end
| Const (@{const_name All}, _)
$ Abs (_, T', @{const "op -->"} $ (t1 $ Bound 0) $ t2) =>
do_bounded_quantifier T' t1 t2 accum
@@ -802,7 +815,7 @@
fun do_quantifier quant_s abs_T body_t =
let
val abs_C = ctype_for abs_T
- val side_cond = ((sn = Neg) = (quant_s = @{const_name Ex}))
+ val side_cond = ((sn = Minus) = (quant_s = @{const_name Ex}))
val cset = cset |> side_cond ? add_ctype_is_right_total abs_C
in
(gamma |> push_bound abs_C, cset) |> do_co_formula body_t
@@ -815,11 +828,11 @@
(* term -> term -> accumulator *)
fun do_equals t1 t2 =
case sn of
- Pos => do_term t accum |> snd
- | Neg => let
- val (C1, accum) = do_term t1 accum
- val (C2, accum) = do_term t2 accum
- in accum ||> add_ctypes_equal C1 C2 end
+ Plus => do_term t accum |> snd
+ | Minus => let
+ val (C1, accum) = do_term t1 accum
+ val (C2, accum) = do_term t2 accum
+ in accum ||> add_ctypes_equal C1 C2 end
in
case t of
Const (s0 as @{const_name all}, _) $ Abs (_, T1, t1) =>
@@ -876,7 +889,7 @@
(* cdata -> term -> accumulator -> accumulator *)
fun consider_definitional_axiom (cdata as {ext_ctxt as {thy, ...}, ...}) t =
if not (is_constr_pattern_formula thy t) then
- consider_nondefinitional_axiom cdata Pos t
+ consider_nondefinitional_axiom cdata Plus t
else if is_harmless_axiom t then
I
else
@@ -921,11 +934,11 @@
(* theory -> literal list -> ctype_context -> unit *)
fun print_ctype_context ctxt lits ({frees, consts, ...} : ctype_context) =
map (fn (x, C) => string_for_ctype_of_term ctxt lits (Free x) C) frees @
- map (fn (x, (C, _)) => string_for_ctype_of_term ctxt lits (Const x) C) consts
+ map (fn (x, C) => string_for_ctype_of_term ctxt lits (Const x) C) consts
|> cat_lines |> print_g
-(* extended_context -> typ -> term list -> term list -> term -> bool *)
-fun formulas_monotonic (ext_ctxt as {ctxt, ...}) alpha_T def_ts nondef_ts
+(* extended_context -> typ -> sign -> term list -> term list -> term -> bool *)
+fun formulas_monotonic (ext_ctxt as {ctxt, ...}) alpha_T sn def_ts nondef_ts
core_t =
let
val _ = print_g ("****** " ^ string_for_ctype CAlpha ^ " is " ^
@@ -934,8 +947,8 @@
val (gamma, cset) =
(initial_gamma, slack)
|> fold (consider_definitional_axiom cdata) def_ts
- |> fold (consider_nondefinitional_axiom cdata Pos) nondef_ts
- |> consider_general_formula cdata Pos core_t
+ |> fold (consider_nondefinitional_axiom cdata Plus) nondef_ts
+ |> consider_general_formula cdata sn core_t
in
case solve (!max_fresh) cset of
SOME lits => (print_ctype_context ctxt lits gamma; true)
--- a/src/HOL/Tools/Nitpick/nitpick_nut.ML Mon Feb 01 14:12:12 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_nut.ML Tue Feb 02 11:38:38 2010 +0100
@@ -1,6 +1,6 @@
(* Title: HOL/Tools/Nitpick/nitpick_nut.ML
Author: Jasmin Blanchette, TU Muenchen
- Copyright 2008, 2009
+ Copyright 2008, 2009, 2010
Nitpick underlying terms (nuts).
*)
@@ -766,7 +766,7 @@
(~1 upto num_sels_for_constr_type T - 1)
(* scope -> dtype_spec -> nut list * rep NameTable.table
-> nut list * rep NameTable.table *)
-fun choose_rep_for_sels_of_datatype _ ({shallow = true, ...} : dtype_spec) = I
+fun choose_rep_for_sels_of_datatype _ ({deep = false, ...} : dtype_spec) = I
| choose_rep_for_sels_of_datatype scope {constrs, ...} =
fold_rev (choose_rep_for_sels_for_constr scope o #const) constrs
(* scope -> rep NameTable.table -> nut list * rep NameTable.table *)
--- a/src/HOL/Tools/Nitpick/nitpick_peephole.ML Mon Feb 01 14:12:12 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_peephole.ML Tue Feb 02 11:38:38 2010 +0100
@@ -1,6 +1,6 @@
(* Title: HOL/Tools/Nitpick/nitpick_peephole.ML
Author: Jasmin Blanchette, TU Muenchen
- Copyright 2008, 2009
+ Copyright 2008, 2009, 2010
Peephole optimizer for Nitpick.
*)
--- a/src/HOL/Tools/Nitpick/nitpick_rep.ML Mon Feb 01 14:12:12 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_rep.ML Tue Feb 02 11:38:38 2010 +0100
@@ -1,6 +1,6 @@
(* Title: HOL/Tools/Nitpick/nitpick_rep.ML
Author: Jasmin Blanchette, TU Muenchen
- Copyright 2008, 2009
+ Copyright 2008, 2009, 2010
Kodkod representations of Nitpick terms.
*)
--- a/src/HOL/Tools/Nitpick/nitpick_scope.ML Mon Feb 01 14:12:12 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_scope.ML Tue Feb 02 11:38:38 2010 +0100
@@ -1,6 +1,6 @@
(* Title: HOL/Tools/Nitpick/nitpick_scope.ML
Author: Jasmin Blanchette, TU Muenchen
- Copyright 2008, 2009
+ Copyright 2008, 2009, 2010
Scope enumerator for Nitpick.
*)
@@ -24,7 +24,7 @@
co: bool,
complete: bool,
concrete: bool,
- shallow: bool,
+ deep: bool,
constrs: constr_spec list}
type scope = {
@@ -73,7 +73,7 @@
co: bool,
complete: bool,
concrete: bool,
- shallow: bool,
+ deep: bool,
constrs: constr_spec list}
type scope = {
@@ -134,7 +134,7 @@
fun quintuple_for_scope quote ({ext_ctxt as {thy, ctxt, ...}, card_assigns,
bits, bisim_depth, datatypes, ...} : scope) =
let
- val boring_Ts = [@{typ unsigned_bit}, @{typ signed_bit},
+ val boring_Ts = [@{typ unsigned_bit}, @{typ signed_bit}, @{typ \<xi>},
@{typ bisim_iterator}]
val (iter_assigns, card_assigns) =
card_assigns |> filter_out (member (op =) boring_Ts o fst)
@@ -429,9 +429,10 @@
else if not co andalso num_self_recs > 0 then
if not self_rec andalso num_non_self_recs = 1 andalso
domain_card 2 card_assigns T = 1 then
- {delta = 0, epsilon = 1, exclusive = (s = @{const_name Nil}),
+ {delta = 0, epsilon = 1,
+ exclusive = (s = @{const_name Nil} andalso length constrs = 2),
total = true}
- else if s = @{const_name Cons} then
+ else if s = @{const_name Cons} andalso length constrs = 2 then
{delta = 1, epsilon = card, exclusive = true, total = false}
else
{delta = 0, epsilon = card, exclusive = false, total = false}
@@ -455,10 +456,10 @@
end
(* extended_context -> typ list -> scope_desc -> typ * int -> dtype_spec *)
-fun datatype_spec_from_scope_descriptor (ext_ctxt as {thy, ...}) shallow_dataTs
+fun datatype_spec_from_scope_descriptor (ext_ctxt as {thy, ...}) deep_dataTs
(desc as (card_assigns, _)) (T, card) =
let
- val shallow = member (op =) shallow_dataTs T
+ val deep = member (op =) deep_dataTs T
val co = is_codatatype thy T
val xs = boxed_datatype_constrs ext_ctxt T
val self_recs = map (is_self_recursive_constr_type o snd) xs
@@ -475,7 +476,7 @@
num_non_self_recs) (self_recs ~~ xs) []
in
{typ = T, card = card, co = co, complete = complete, concrete = concrete,
- shallow = shallow, constrs = constrs}
+ deep = deep, constrs = constrs}
end
(* int -> int *)
@@ -487,11 +488,11 @@
(map snd card_assigns @ map snd max_assigns) 0)
(* extended_context -> int -> typ list -> scope_desc -> scope *)
-fun scope_from_descriptor (ext_ctxt as {thy, ...}) sym_break shallow_dataTs
+fun scope_from_descriptor (ext_ctxt as {thy, ...}) sym_break deep_dataTs
(desc as (card_assigns, _)) =
let
val datatypes =
- map (datatype_spec_from_scope_descriptor ext_ctxt shallow_dataTs desc)
+ map (datatype_spec_from_scope_descriptor ext_ctxt deep_dataTs desc)
(filter (is_datatype thy o fst) card_assigns)
val bits = card_of_type card_assigns @{typ signed_bit} - 1
handle TYPE ("Nitpick_HOL.card_of_type", _, _) =>
@@ -524,8 +525,7 @@
-> (styp option * int list) list -> (styp option * int list) list -> int list
-> typ list -> typ list -> typ list -> int * scope list *)
fun all_scopes (ext_ctxt as {thy, ...}) sym_break cards_assigns maxes_assigns
- iters_assigns bitss bisim_depths mono_Ts nonmono_Ts
- shallow_dataTs =
+ iters_assigns bitss bisim_depths mono_Ts nonmono_Ts deep_dataTs =
let
val cards_assigns = repair_cards_assigns_wrt_boxing thy mono_Ts
cards_assigns
@@ -540,7 +540,7 @@
in
(length all - length head,
descs |> length descs <= distinct_threshold ? distinct (op =)
- |> map (scope_from_descriptor ext_ctxt sym_break shallow_dataTs))
+ |> map (scope_from_descriptor ext_ctxt sym_break deep_dataTs))
end
end;
--- a/src/HOL/Tools/Nitpick/nitpick_tests.ML Mon Feb 01 14:12:12 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_tests.ML Tue Feb 02 11:38:38 2010 +0100
@@ -1,6 +1,6 @@
(* Title: HOL/Tools/Nitpick/nitpick_tests.ML
Author: Jasmin Blanchette, TU Muenchen
- Copyright 2008, 2009
+ Copyright 2008, 2009, 2010
Unit tests for Nitpick.
*)
--- a/src/HOL/Tools/Nitpick/nitpick_util.ML Mon Feb 01 14:12:12 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_util.ML Tue Feb 02 11:38:38 2010 +0100
@@ -1,6 +1,6 @@
(* Title: HOL/Tools/Nitpick/nitpick_util.ML
Author: Jasmin Blanchette, TU Muenchen
- Copyright 2008, 2009
+ Copyright 2008, 2009, 2010
General-purpose functions used by the Nitpick modules.
*)
@@ -58,7 +58,7 @@
val setmp_show_all_types : ('a -> 'b) -> 'a -> 'b
val indent_size : int
val pstrs : string -> Pretty.T list
- val plain_string_from_yxml : string -> string
+ val unyxml : string -> string
val maybe_quote : string -> string
end
@@ -278,13 +278,13 @@
fun plain_string_from_xml_tree t =
Buffer.empty |> XML.add_content t |> Buffer.content
(* string -> string *)
-val plain_string_from_yxml = plain_string_from_xml_tree o YXML.parse
+val unyxml = plain_string_from_xml_tree o YXML.parse
(* string -> bool *)
val is_long_identifier = forall Syntax.is_identifier o space_explode "."
(* string -> string *)
fun maybe_quote y =
- let val s = plain_string_from_yxml y in
+ let val s = unyxml y in
y |> (not (is_long_identifier (perhaps (try (unprefix "'")) s)) orelse
OuterKeyword.is_keyword s) ? quote
end
--- a/src/Pure/Isar/proof_context.ML Mon Feb 01 14:12:12 2010 +0100
+++ b/src/Pure/Isar/proof_context.ML Tue Feb 02 11:38:38 2010 +0100
@@ -33,6 +33,7 @@
val set_syntax_mode: Syntax.mode -> Proof.context -> Proof.context
val restore_syntax_mode: Proof.context -> Proof.context -> Proof.context
val facts_of: Proof.context -> Facts.T
+ val cases_of: Proof.context -> (string * (Rule_Cases.T * bool)) list
val transfer_syntax: theory -> Proof.context -> Proof.context
val transfer: theory -> Proof.context -> Proof.context
val theory: (theory -> theory) -> Proof.context -> Proof.context