--- a/doc-src/Nitpick/nitpick.tex Thu Mar 17 14:43:51 2011 +0100
+++ b/doc-src/Nitpick/nitpick.tex Thu Mar 17 14:43:53 2011 +0100
@@ -467,25 +467,26 @@
\postw
With infinite types, we don't always have the luxury of a genuine counterexample
-and must often content ourselves with a potential one. The tedious task of
-finding out whether the potential counterexample is in fact genuine can be
-outsourced to \textit{auto} by passing \textit{check\_potential}. For example:
+and must often content ourselves with a potentially spurious one. The tedious
+task of finding out whether the potentially spurious counterexample is in fact
+genuine can be delegated to \textit{auto} by passing \textit{check\_potential}.
+For example:
\prew
\textbf{lemma} ``$\forall n.\; \textit{Suc}~n \mathbin{\not=} n \,\Longrightarrow\, P$'' \\
\textbf{nitpick} [\textit{card~nat}~= 50, \textit{check\_potential}] \\[2\smallskipamount]
\slshape Warning: The conjecture either trivially holds for the given scopes or lies outside Nitpick's supported
-fragment. Only potential counterexamples may be found. \\[2\smallskipamount]
-Nitpick found a potential counterexample: \\[2\smallskipamount]
+fragment. Only potentially spurious counterexamples may be found. \\[2\smallskipamount]
+Nitpick found a potentially spurious counterexample: \\[2\smallskipamount]
\hbox{}\qquad Free variable: \nopagebreak \\
\hbox{}\qquad\qquad $P = \textit{False}$ \\[2\smallskipamount]
Confirmation by ``\textit{auto}'': The above counterexample is genuine.
\postw
-You might wonder why the counterexample is first reported as potential. The root
-of the problem is that the bound variable in $\forall n.\; \textit{Suc}~n
-\mathbin{\not=} n$ ranges over an infinite type. If Nitpick finds an $n$ such
-that $\textit{Suc}~n \mathbin{=} n$, it evaluates the assumption to
+You might wonder why the counterexample is first reported as potentially
+spurious. The root of the problem is that the bound variable in $\forall n.\;
+\textit{Suc}~n \mathbin{\not=} n$ ranges over an infinite type. If Nitpick finds
+an $n$ such that $\textit{Suc}~n \mathbin{=} n$, it evaluates the assumption to
\textit{False}; but otherwise, it does not know anything about values of $n \ge
\textit{card~nat}$ and must therefore evaluate the assumption to $\unk$, not
\textit{True}. Since the assumption can never be satisfied, the putative lemma
@@ -797,9 +798,9 @@
Nitpick can compute it efficiently. \\[2\smallskipamount]
Trying 1 scope: \\
\hbox{}\qquad \textit{card nat}~= 50. \\[2\smallskipamount]
-Nitpick found a potential counterexample for \textit{card nat}~= 50: \\[2\smallskipamount]
+Nitpick found a potentially spurious counterexample for \textit{card nat}~= 50: \\[2\smallskipamount]
\hbox{}\qquad Empty assignment \\[2\smallskipamount]
-Nitpick could not find a better counterexample. It checked 0 of 1 scope. \\[2\smallskipamount]
+Nitpick could not find a better counterexample. \\[2\smallskipamount]
Total time: 1.43 s.
\postw
@@ -2189,7 +2190,7 @@
\opfalse{show\_datatypes}{hide\_datatypes}
Specifies whether the subsets used to approximate (co)in\-duc\-tive datatypes should
be displayed as part of counterexamples. Such subsets are sometimes helpful when
-investigating whether a potential counterexample is genuine or spurious, but
+investigating whether a potentially spurious counterexample is genuine, but
their potential for clutter is real.
\opfalse{show\_consts}{hide\_consts}
@@ -2202,10 +2203,10 @@
Abbreviation for \textit{show\_datatypes} and \textit{show\_consts}.
\opdefault{max\_potential}{int}{\upshape 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
-greater than 1, you will need an incremental SAT solver, such as
+Specifies the maximum number of potentially spurious 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 greater than 1, you will need an incremental SAT solver, such as
\textit{MiniSat\_JNI} (recommended) and \textit{SAT4J}. Be aware that many of
the counterexamples may be identical.
@@ -2269,9 +2270,10 @@
\begin{enum}
\opfalse{check\_potential}{trust\_potential}
-Specifies whether potential counterexamples should be given to Isabelle's
-\textit{auto} tactic to assess their validity. If a potential counterexample is
-shown to be genuine, Nitpick displays a message to this effect and terminates.
+Specifies whether potentially spurious counterexamples should be given to
+Isabelle's \textit{auto} tactic to assess their validity. If a potentially
+spurious counterexample is shown to be genuine, Nitpick displays a message to
+this effect and terminates.
\nopagebreak
{\small See also \textit{max\_potential} (\S\ref{output-format}).}
@@ -2294,7 +2296,8 @@
\item[$\bullet$] \textbf{\textit{quasi\_genuine}:} Nitpick found a ``quasi
genuine'' counterexample (i.e., a counterexample that is genuine unless
it contradicts a missing axiom or a dangerous option was used inappropriately).
-\item[$\bullet$] \textbf{\textit{potential}:} Nitpick found a potential counterexample.
+\item[$\bullet$] \textbf{\textit{potential}:} Nitpick found a potentially
+spurious counterexample.
\item[$\bullet$] \textbf{\textit{none}:} Nitpick found no counterexample.
\item[$\bullet$] \textbf{\textit{unknown}:} Nitpick encountered some problem (e.g.,
Kodkod ran out of memory).
--- a/src/HOL/Tools/Nitpick/nitpick.ML Thu Mar 17 14:43:51 2011 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick.ML Thu Mar 17 14:43:53 2011 +0100
@@ -605,16 +605,16 @@
NONE
else
(Unsynchronized.change too_big_scopes (cons scope);
- print_v (fn () => ("Limit reached: " ^ msg ^
- ". Skipping " ^ (if unsound then "potential"
- else "genuine") ^
- " component of scope."));
+ print_v (fn () =>
+ "Limit reached: " ^ msg ^ ". Skipping " ^
+ (if unsound then "potential component of " else "") ^
+ "scope.");
NONE)
| TOO_SMALL (_, msg) =>
- (print_v (fn () => ("Limit reached: " ^ msg ^
- ". Skipping " ^ (if unsound then "potential"
- else "genuine") ^
- " component of scope."));
+ (print_v (fn () =>
+ "Limit reached: " ^ msg ^ ". Skipping " ^
+ (if unsound then "potential component of " else "") ^
+ "scope.");
NONE)
val das_wort_model =
@@ -651,7 +651,7 @@
(pprint (Pretty.chunks
[Pretty.blk (0,
(pstrs ((if auto then "Auto " else "") ^ "Nitpick found a" ^
- (if not genuine then " potential "
+ (if not genuine then " potentially spurious "
else if genuine_means_genuine then " "
else " quasi genuine ") ^ das_wort_model) @
(case pretties_for_scope scope verbose of
@@ -908,7 +908,8 @@
\fragment." ^
(if exists (not o KK.is_problem_trivially_false o fst)
unsound_problems then
- " Only potential " ^ das_wort_model ^ "s may be found."
+ " Only potentially spurious " ^ das_wort_model ^
+ "s may be found."
else
""))
else