1.1 --- a/doc-src/Nitpick/nitpick.tex	Thu Mar 17 14:43:51 2011 +0100
     1.2 +++ b/doc-src/Nitpick/nitpick.tex	Thu Mar 17 14:43:53 2011 +0100
     1.3 @@ -467,25 +467,26 @@
     1.4  \postw
     1.5  
     1.6  With infinite types, we don't always have the luxury of a genuine counterexample
     1.7 -and must often content ourselves with a potential one. The tedious task of
     1.8 -finding out whether the potential counterexample is in fact genuine can be
     1.9 -outsourced to \textit{auto} by passing \textit{check\_potential}. For example:
    1.10 +and must often content ourselves with a potentially spurious one. The tedious
    1.11 +task of finding out whether the potentially spurious counterexample is in fact
    1.12 +genuine can be delegated to \textit{auto} by passing \textit{check\_potential}.
    1.13 +For example:
    1.14  
    1.15  \prew
    1.16  \textbf{lemma} ``$\forall n.\; \textit{Suc}~n \mathbin{\not=} n \,\Longrightarrow\, P$'' \\
    1.17  \textbf{nitpick} [\textit{card~nat}~= 50, \textit{check\_potential}] \\[2\smallskipamount]
    1.18  \slshape Warning: The conjecture either trivially holds for the given scopes or lies outside Nitpick's supported
    1.19 -fragment. Only potential counterexamples may be found. \\[2\smallskipamount]
    1.20 -Nitpick found a potential counterexample: \\[2\smallskipamount]
    1.21 +fragment. Only potentially spurious counterexamples may be found. \\[2\smallskipamount]
    1.22 +Nitpick found a potentially spurious counterexample: \\[2\smallskipamount]
    1.23  \hbox{}\qquad Free variable: \nopagebreak \\
    1.24  \hbox{}\qquad\qquad $P = \textit{False}$ \\[2\smallskipamount]
    1.25  Confirmation by ``\textit{auto}'': The above counterexample is genuine.
    1.26  \postw
    1.27  
    1.28 -You might wonder why the counterexample is first reported as potential. The root
    1.29 -of the problem is that the bound variable in $\forall n.\; \textit{Suc}~n
    1.30 -\mathbin{\not=} n$ ranges over an infinite type. If Nitpick finds an $n$ such
    1.31 -that $\textit{Suc}~n \mathbin{=} n$, it evaluates the assumption to
    1.32 +You might wonder why the counterexample is first reported as potentially
    1.33 +spurious. The root of the problem is that the bound variable in $\forall n.\;
    1.34 +\textit{Suc}~n \mathbin{\not=} n$ ranges over an infinite type. If Nitpick finds
    1.35 +an $n$ such that $\textit{Suc}~n \mathbin{=} n$, it evaluates the assumption to
    1.36  \textit{False}; but otherwise, it does not know anything about values of $n \ge
    1.37  \textit{card~nat}$ and must therefore evaluate the assumption to $\unk$, not
    1.38  \textit{True}. Since the assumption can never be satisfied, the putative lemma
    1.39 @@ -797,9 +798,9 @@
    1.40  Nitpick can compute it efficiently. \\[2\smallskipamount]
    1.41  Trying 1 scope: \\
    1.42  \hbox{}\qquad \textit{card nat}~= 50. \\[2\smallskipamount]
    1.43 -Nitpick found a potential counterexample for \textit{card nat}~= 50: \\[2\smallskipamount]
    1.44 +Nitpick found a potentially spurious counterexample for \textit{card nat}~= 50: \\[2\smallskipamount]
    1.45  \hbox{}\qquad Empty assignment \\[2\smallskipamount]
    1.46 -Nitpick could not find a better counterexample. It checked 0 of 1 scope. \\[2\smallskipamount]
    1.47 +Nitpick could not find a better counterexample. \\[2\smallskipamount]
    1.48  Total time: 1.43 s.
    1.49  \postw
    1.50  
    1.51 @@ -2189,7 +2190,7 @@
    1.52  \opfalse{show\_datatypes}{hide\_datatypes}
    1.53  Specifies whether the subsets used to approximate (co)in\-duc\-tive datatypes should
    1.54  be displayed as part of counterexamples. Such subsets are sometimes helpful when
    1.55 -investigating whether a potential counterexample is genuine or spurious, but
    1.56 +investigating whether a potentially spurious counterexample is genuine, but
    1.57  their potential for clutter is real.
    1.58  
    1.59  \opfalse{show\_consts}{hide\_consts}
    1.60 @@ -2202,10 +2203,10 @@
    1.61  Abbreviation for \textit{show\_datatypes} and \textit{show\_consts}.
    1.62  
    1.63  \opdefault{max\_potential}{int}{\upshape 1}
    1.64 -Specifies the maximum number of potential counterexamples to display. Setting
    1.65 -this option to 0 speeds up the search for a genuine counterexample. This option
    1.66 -is implicitly set to 0 for automatic runs. If you set this option to a value
    1.67 -greater than 1, you will need an incremental SAT solver, such as
    1.68 +Specifies the maximum number of potentially spurious counterexamples to display.
    1.69 +Setting this option to 0 speeds up the search for a genuine counterexample. This
    1.70 +option is implicitly set to 0 for automatic runs. If you set this option to a
    1.71 +value greater than 1, you will need an incremental SAT solver, such as
    1.72  \textit{MiniSat\_JNI} (recommended) and \textit{SAT4J}. Be aware that many of
    1.73  the counterexamples may be identical.
    1.74  
    1.75 @@ -2269,9 +2270,10 @@
    1.76  
    1.77  \begin{enum}
    1.78  \opfalse{check\_potential}{trust\_potential}
    1.79 -Specifies whether potential counterexamples should be given to Isabelle's
    1.80 -\textit{auto} tactic to assess their validity. If a potential counterexample is
    1.81 -shown to be genuine, Nitpick displays a message to this effect and terminates.
    1.82 +Specifies whether potentially spurious counterexamples should be given to
    1.83 +Isabelle's \textit{auto} tactic to assess their validity. If a potentially
    1.84 +spurious counterexample is shown to be genuine, Nitpick displays a message to
    1.85 +this effect and terminates.
    1.86  
    1.87  \nopagebreak
    1.88  {\small See also \textit{max\_potential} (\S\ref{output-format}).}
    1.89 @@ -2294,7 +2296,8 @@
    1.90  \item[$\bullet$] \textbf{\textit{quasi\_genuine}:} Nitpick found a ``quasi
    1.91  genuine'' counterexample (i.e., a counterexample that is genuine unless
    1.92  it contradicts a missing axiom or a dangerous option was used inappropriately).
    1.93 -\item[$\bullet$] \textbf{\textit{potential}:} Nitpick found a potential counterexample.
    1.94 +\item[$\bullet$] \textbf{\textit{potential}:} Nitpick found a potentially
    1.95 +spurious counterexample.
    1.96  \item[$\bullet$] \textbf{\textit{none}:} Nitpick found no counterexample.
    1.97  \item[$\bullet$] \textbf{\textit{unknown}:} Nitpick encountered some problem (e.g.,
    1.98  Kodkod ran out of memory).

     2.1 --- a/src/HOL/Tools/Nitpick/nitpick.ML	Thu Mar 17 14:43:51 2011 +0100
     2.2 +++ b/src/HOL/Tools/Nitpick/nitpick.ML	Thu Mar 17 14:43:53 2011 +0100
     2.3 @@ -605,16 +605,16 @@
     2.4                 NONE
     2.5               else
     2.6                 (Unsynchronized.change too_big_scopes (cons scope);
     2.7 -                print_v (fn () => ("Limit reached: " ^ msg ^
     2.8 -                                   ". Skipping " ^ (if unsound then "potential"
     2.9 -                                                    else "genuine") ^
    2.10 -                                   " component of scope."));
    2.11 +                print_v (fn () =>
    2.12 +                    "Limit reached: " ^ msg ^ ". Skipping " ^
    2.13 +                    (if unsound then "potential component of " else "") ^
    2.14 +                    "scope.");
    2.15                  NONE)
    2.16             | TOO_SMALL (_, msg) =>
    2.17 -             (print_v (fn () => ("Limit reached: " ^ msg ^
    2.18 -                                 ". Skipping " ^ (if unsound then "potential"
    2.19 -                                                  else "genuine") ^
    2.20 -                                 " component of scope."));
    2.21 +             (print_v (fn () =>
    2.22 +                  "Limit reached: " ^ msg ^ ". Skipping " ^
    2.23 +                  (if unsound then "potential component of " else "") ^
    2.24 +                  "scope.");
    2.25                NONE)
    2.26  
    2.27      val das_wort_model =
    2.28 @@ -651,7 +651,7 @@
    2.29          (pprint (Pretty.chunks
    2.30               [Pretty.blk (0,
    2.31                    (pstrs ((if auto then "Auto " else "") ^ "Nitpick found a" ^
    2.32 -                          (if not genuine then " potential "
    2.33 +                          (if not genuine then " potentially spurious "
    2.34                             else if genuine_means_genuine then " "
    2.35                             else " quasi genuine ") ^ das_wort_model) @
    2.36                     (case pretties_for_scope scope verbose of
    2.37 @@ -908,7 +908,8 @@
    2.38                      \fragment." ^
    2.39                      (if exists (not o KK.is_problem_trivially_false o fst)
    2.40                                 unsound_problems then
    2.41 -                       " Only potential " ^ das_wort_model ^ "s may be found."
    2.42 +                       " Only potentially spurious " ^ das_wort_model ^
    2.43 +                       "s may be found."
    2.44                       else
    2.45                         ""))
    2.46                else