# HG changeset patch
# User blanchet
# Date 1432915003 -7200
# Node ID 932221b62e898e904c1dd7b6dd9209dd0ff3e509
# Parent  72364a93bcb53a260282ca190cff02fc57c68e02
removed model checks from Nitpick

diff -r 72364a93bcb5 -r 932221b62e89 NEWS
--- a/NEWS	Fri May 29 17:17:50 2015 +0200
+++ b/NEWS	Fri May 29 17:56:43 2015 +0200
@@ -15,6 +15,9 @@
     cases where Sledgehammer gives a proof that does not work.
   - Auto Sledgehammer now minimizes and preplays the results.
 
+* Nitpick:
+  - Removed "check_potential" and "check_genuine" options.
+
 
 New in Isabelle2015 (May 2015)
 ------------------------------
diff -r 72364a93bcb5 -r 932221b62e89 src/Doc/Nitpick/document/root.tex
--- a/src/Doc/Nitpick/document/root.tex	Fri May 29 17:17:50 2015 +0200
+++ b/src/Doc/Nitpick/document/root.tex	Fri May 29 17:56:43 2015 +0200
@@ -463,35 +463,26 @@
 \postw
 
 With infinite types, we don't always have the luxury of a genuine counterexample
-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}.
+and must often content ourselves with a potentially spurious one.
 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]
+\textbf{nitpick} [\textit{card~nat}~= 50] \\[2\smallskipamount]
 \slshape Warning: The conjecture either trivially holds for the given scopes or lies outside Nitpick's supported
 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.
+\hbox{}\qquad\qquad $P = \textit{False}$
 \postw
 
-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.\;
+The issue 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
-can never be falsified.
-
-Incidentally, if you distrust the so-called genuine counterexamples, you can
-enable \textit{check\_\allowbreak genuine} to verify them as well. However, be
-aware that \textit{auto} will usually fail to prove that the counterexample is
-genuine or spurious.
+\textit{True}. Since the assumption can never be fully satisfied by Nitpick,
+the putative lemma can never be falsified.
 
 Some conjectures involving elementary number theory make Nitpick look like a
 giant with feet of clay:
@@ -1746,8 +1737,7 @@
 
 The options are categorized as follows:\ mode of operation
 (\S\ref{mode-of-operation}), scope of search (\S\ref{scope-of-search}), output
-format (\S\ref{output-format}), automatic counterexample checks
-(\S\ref{authentication}), regression testing (\S\ref{regression-testing}),
+format (\S\ref{output-format}), regression testing (\S\ref{regression-testing}),
 optimizations (\S\ref{optimizations}), and timeouts (\S\ref{timeouts}).
 
 If you use Isabelle/jEdit, Nitpick also provides an automatic mode that can
@@ -1757,9 +1747,9 @@
 \textit{assms} (\S\ref{mode-of-operation}), and \textit{mono}
 (\S\ref{scope-of-search}) are implicitly enabled, \textit{blocking}
 (\S\ref{mode-of-operation}), \textit{verbose} (\S\ref{output-format}), and
-\textit{debug} (\S\ref{output-format}) are disabled, \textit{max\_threads}
-(\S\ref{optimizations}) is taken to be 1, \textit{max\_potential}
-(\S\ref{output-format}) is taken to be 0, and \textit{timeout}
+\textit{debug} (\S\ref{output-format}) are disabled, \textit{max\_potential}
+(\S\ref{output-format}) is taken to be 0, \textit{max\_threads}
+(\S\ref{optimizations}) is taken to be 1, and \textit{timeout}
 (\S\ref{timeouts}) is superseded by the ``Auto Time Limit'' in jEdit. Nitpick's
 output is also more concise.
 
@@ -2112,8 +2102,7 @@
 the counterexamples may be identical.
 
 \nopagebreak
-{\small See also \textit{check\_potential} (\S\ref{authentication}) and
-\textit{sat\_solver} (\S\ref{optimizations}).}
+{\small See also \textit{sat\_solver} (\S\ref{optimizations}).}
 
 \opdefault{max\_genuine}{int}{\upshape 1}
 Specifies the maximum number of genuine counterexamples to display. If you set
@@ -2122,8 +2111,7 @@
 many of the counterexamples may be identical.
 
 \nopagebreak
-{\small See also \textit{check\_genuine} (\S\ref{authentication}) and
-\textit{sat\_solver} (\S\ref{optimizations}).}
+{\small See also \textit{sat\_solver} (\S\ref{optimizations}).}
 
 \opnodefault{eval}{term\_list}
 Specifies the list of terms whose values should be displayed along with
@@ -2166,31 +2154,10 @@
 the \textit{format}~\qty{term} option described above.
 \end{enum}
 
-\subsection{Authentication}
-\label{authentication}
+\subsection{Regression Testing}
+\label{regression-testing}
 
 \begin{enum}
-\opfalse{check\_potential}{trust\_potential}
-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}).}
-
-\opfalse{check\_genuine}{trust\_genuine}
-Specifies whether genuine and quasi genuine counterexamples should be given to
-Isabelle's \textit{auto} tactic to assess their validity. If a ``genuine''
-counterexample is shown to be spurious, the user is kindly asked to send a bug
-report to the author at \authoremail.
-
-\nopagebreak
-{\small See also \textit{max\_genuine} (\S\ref{output-format}).}
-
-\subsection{Regression Testing}
-\label{regression-testing}
-
 \opnodefault{expect}{string}
 Specifies the expected outcome, which must be one of the following:
 
@@ -2426,15 +2393,12 @@
 \opdefault{tac\_timeout}{float}{\upshape 0.5}
 Specifies the maximum number of seconds that should be used by internal
 tactics---\textit{lexicographic\_order} and \textit{size\_change} when checking
-whether a (co)in\-duc\-tive predicate is well-founded, \textit{auto} tactic when
-checking a counterexample, or the monotonicity inference. Nitpick tries to honor
-this constraint but offers no guarantees.
+whether a (co)in\-duc\-tive predicate is well-founded or the monotonicity
+inference. Nitpick tries to honor this constraint but offers no guarantees.
 
 \nopagebreak
-{\small See also \textit{wf} (\S\ref{scope-of-search}),
-\textit{mono} (\S\ref{scope-of-search}),
-\textit{check\_potential} (\S\ref{authentication}),
-and \textit{check\_genuine} (\S\ref{authentication}).}
+{\small See also \textit{wf} (\S\ref{scope-of-search}) and
+\textit{mono} (\S\ref{scope-of-search}).}
 \end{enum}
 
 \section{Attribute Reference}
@@ -2501,7 +2465,7 @@
 
 \nopagebreak
 This attribute specifies the (free-form) specification of a constant defined
-using the \hbox{(\textbf{ax\_})}\allowbreak\textbf{specification} command.
+using the \textbf{specification} command.
 \end{enum}
 
 When faced with a constant, Nitpick proceeds as follows:
@@ -2515,7 +2479,7 @@
 constant.
 
 \item[3.] Otherwise, if the constant was defined using the
-\hbox{(\textbf{ax\_})}\allowbreak\textbf{specification} command and the
+\allowbreak\textbf{specification} command and the
 \textit{nitpick\_choice\_spec} set associated with the constant is not empty, it
 uses these theorems as the specification of the constant.
 
diff -r 72364a93bcb5 -r 932221b62e89 src/HOL/Nitpick_Examples/Manual_Nits.thy
--- a/src/HOL/Nitpick_Examples/Manual_Nits.thy	Fri May 29 17:17:50 2015 +0200
+++ b/src/HOL/Nitpick_Examples/Manual_Nits.thy	Fri May 29 17:56:43 2015 +0200
@@ -74,7 +74,7 @@
 oops
 
 lemma "\<forall>n. Suc n \<noteq> n \<Longrightarrow> P"
-nitpick [card nat = 100, check_potential, tac_timeout = 5, expect = genuine]
+nitpick [card nat = 100, expect = potential]
 oops
 
 lemma "P Suc"
diff -r 72364a93bcb5 -r 932221b62e89 src/HOL/Tools/Nitpick/nitpick.ML
--- a/src/HOL/Tools/Nitpick/nitpick.ML	Fri May 29 17:17:50 2015 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick.ML	Fri May 29 17:56:43 2015 +0200
@@ -52,8 +52,6 @@
      atomss: (typ option * string list) list,
      max_potential: int,
      max_genuine: int,
-     check_potential: bool,
-     check_genuine: bool,
      batch_size: int,
      expect: string}
 
@@ -138,8 +136,6 @@
    atomss: (typ option * string list) list,
    max_potential: int,
    max_genuine: int,
-   check_potential: bool,
-   check_genuine: bool,
    batch_size: int,
    expect: string}
 
@@ -234,7 +230,7 @@
          total_consts, needs, peephole_optim, datatype_sym_break,
          kodkod_sym_break, tac_timeout, max_threads, show_types, show_skolems,
          show_consts, evals, formats, atomss, max_potential, max_genuine,
-         check_potential, check_genuine, batch_size, ...} = params
+         batch_size, ...} = params
     val outcome = Synchronized.var "Nitpick.outcome" (Queue.empty: string Queue.T)
     fun pprint print prt =
       if mode = Auto_Try then
@@ -669,25 +665,7 @@
               Pretty.indent indent_size reconstructed_model]);
          print_t (K "% SZS output end FiniteModel");
          if genuine then
-           (if check_genuine then
-              case prove_hol_model scope tac_timeout free_names sel_names
-                                   rel_table bounds (assms_prop ()) of
-                SOME true =>
-                print ("Confirmation by \"auto\": The above " ^
-                       das_wort_model ^ " is really genuine.")
-              | SOME false =>
-                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 " ^
-                          das_wort_model ^ " is spurious.")
-               | NONE => print "No confirmation by \"auto\"."
-            else
-              ();
-            if has_lonely_bool_var orig_t then
+           (if has_lonely_bool_var orig_t then
               print "Hint: Maybe you forgot a colon after the lemma's name?"
             else if has_syntactic_sorts orig_t then
               print "Hint: Maybe you forgot a type constraint?"
@@ -725,24 +703,7 @@
             NONE)
          else
            if not genuine then
-             (Unsynchronized.inc met_potential;
-              if check_potential then
-                let
-                  val status = prove_hol_model scope tac_timeout free_names
-                                               sel_names rel_table bounds
-                                               (assms_prop ())
-                in
-                  (case status of
-                     SOME true => print ("Confirmation by \"auto\": The \
-                                         \above " ^ das_wort_model ^
-                                         " is genuine.")
-                   | SOME false => print ("Refutation by \"auto\": The above " ^
-                                          das_wort_model ^ " is spurious.")
-                   | NONE => print "No confirmation by \"auto\".");
-                  status
-                end
-              else
-                NONE)
+             (Unsynchronized.inc met_potential; NONE)
            else
              NONE)
         |> pair genuine_means_genuine
diff -r 72364a93bcb5 -r 932221b62e89 src/HOL/Tools/Nitpick/nitpick_commands.ML
--- a/src/HOL/Tools/Nitpick/nitpick_commands.ML	Fri May 29 17:17:50 2015 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_commands.ML	Fri May 29 17:56:43 2015 +0200
@@ -69,9 +69,7 @@
    ("show_consts", "false"),
    ("format", "1"),
    ("max_potential", "1"),
-   ("max_genuine", "1"),
-   ("check_potential", "false"),
-   ("check_genuine", "false")]
+   ("max_genuine", "1")]
 
 val negated_params =
   [("dont_box", "box"),
@@ -95,9 +93,7 @@
    ("dont_spy", "spy"),
    ("hide_types", "show_types"),
    ("hide_skolems", "show_skolems"),
-   ("hide_consts", "show_consts"),
-   ("trust_potential", "check_potential"),
-   ("trust_genuine", "check_genuine")]
+   ("hide_consts", "show_consts")]
 
 fun is_known_raw_param s =
   AList.defined (op =) default_default_params s orelse
@@ -270,8 +266,6 @@
     val max_potential =
       if mode = Normal then Int.max (0, lookup_int "max_potential") else 0
     val max_genuine = Int.max (0, lookup_int "max_genuine")
-    val check_potential = lookup_bool "check_potential"
-    val check_genuine = lookup_bool "check_genuine"
     val batch_size =
       case lookup_int_option "batch_size" of
         SOME n => Int.max (1, n)
@@ -294,7 +288,6 @@
      show_types = show_types, show_skolems = show_skolems,
      show_consts = show_consts, evals = evals, formats = formats,
      atomss = atomss, max_potential = max_potential, max_genuine = max_genuine,
-     check_potential = check_potential, check_genuine = check_genuine,
      batch_size = batch_size, expect = expect}
   end
 
diff -r 72364a93bcb5 -r 932221b62e89 src/HOL/Tools/Nitpick/nitpick_model.ML
--- a/src/HOL/Tools/Nitpick/nitpick_model.ML	Fri May 29 17:17:50 2015 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_model.ML	Fri May 29 17:56:43 2015 +0200
@@ -39,9 +39,6 @@
     -> (typ option * string list) list -> (string * typ) list ->
     (string * typ) list -> nut list -> nut list -> nut list ->
     nut NameTable.table -> Kodkod.raw_bound list -> Pretty.T * bool
-  val prove_hol_model :
-    scope -> Time.time -> nut list -> nut list -> nut NameTable.table
-    -> Kodkod.raw_bound list -> term -> bool option
 end;
 
 structure Nitpick_Model : NITPICK_MODEL =
@@ -1036,63 +1033,4 @@
      forall (is_codatatype_wellformed codatatypes) codatatypes)
   end
 
-fun term_for_name pool scope atomss sel_names rel_table bounds name =
-  let val T = type_of name in
-    tuple_list_for_name rel_table bounds name
-    |> reconstruct_term (not (is_fully_representable_set name)) false pool
-                        (("", ""), ("", "")) scope atomss sel_names rel_table
-                        bounds T T (rep_of name)
-  end
-
-fun prove_hol_model (scope as {hol_ctxt = {thy, ctxt, debug, ...},
-                               card_assigns, ...})
-                    auto_timeout free_names sel_names rel_table bounds prop =
-  let
-    val pool = Unsynchronized.ref []
-    val atomss = [(NONE, [])]
-    fun free_type_assm (T, k) =
-      let
-        fun atom j = nth_atom thy atomss pool true T j
-        fun equation_for_atom j = HOLogic.eq_const T $ Bound 0 $ atom j
-        val eqs = map equation_for_atom (index_seq 0 k)
-        val compreh_assm =
-          Const (@{const_name All}, (T --> bool_T) --> bool_T)
-              $ Abs ("x", T, foldl1 HOLogic.mk_disj eqs)
-        val distinct_assm = distinctness_formula T (map atom (index_seq 0 k))
-      in s_conj (compreh_assm, distinct_assm) end
-    fun free_name_assm name =
-      HOLogic.mk_eq (Free (nickname_of name, type_of name),
-                     term_for_name pool scope atomss sel_names rel_table bounds
-                                   name)
-    val freeT_assms = map free_type_assm (filter (is_TFree o fst) card_assigns)
-    val model_assms = map free_name_assm free_names
-    val assm = foldr1 s_conj (freeT_assms @ model_assms)
-    fun try_out negate =
-      let
-        val concl = (negate ? curry (op $) @{const Not})
-                    (Object_Logic.atomize_term ctxt prop)
-        val prop = HOLogic.mk_Trueprop (HOLogic.mk_imp (assm, concl))
-                   |> map_types (map_type_tfree
-                                     (fn (s, []) => TFree (s, @{sort type})
-                                       | x => TFree x))
-        val _ =
-          if debug then
-            (if negate then "Genuineness" else "Spuriousness") ^ " goal: " ^
-            Syntax.string_of_term ctxt prop ^ "."
-            |> writeln
-          else
-            ()
-        val goal = prop |> Thm.cterm_of ctxt |> Goal.init
-      in
-        (goal |> SINGLE (DETERM_TIMEOUT auto_timeout (auto_tac ctxt))
-              |> the |> Goal.finish ctxt; true)
-        handle THM _ => false
-             | TimeLimit.TimeOut => false
-      end
-  in
-    if try_out false then SOME true
-    else if try_out true then SOME false
-    else NONE
-  end
-
 end;