# HG changeset patch
# User blanchet
# Date 1300369433 -3600
# Node ID 0e4716fa330a7f24a8d03c6af3b6774ceb3ae184
# Parent  ea02b9ee30854b73c27ef8dc3c066d5009bc676c
reword Nitpick's wording concerning potential counterexamples

diff -r ea02b9ee3085 -r 0e4716fa330a doc-src/Nitpick/nitpick.tex
--- 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).
diff -r ea02b9ee3085 -r 0e4716fa330a src/HOL/Tools/Nitpick/nitpick.ML
--- 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