removed model checks from Nitpick
authorblanchet
Fri May 29 17:56:43 2015 +0200 (2015-05-29 ago)
changeset 60310932221b62e89
parent 60309 72364a93bcb5
child 60311 599c4a27785c
removed model checks from Nitpick
NEWS
src/Doc/Nitpick/document/root.tex
src/HOL/Nitpick_Examples/Manual_Nits.thy
src/HOL/Tools/Nitpick/nitpick.ML
src/HOL/Tools/Nitpick/nitpick_commands.ML
src/HOL/Tools/Nitpick/nitpick_model.ML
     1.1 --- a/NEWS	Fri May 29 17:17:50 2015 +0200
     1.2 +++ b/NEWS	Fri May 29 17:56:43 2015 +0200
     1.3 @@ -15,6 +15,9 @@
     1.4      cases where Sledgehammer gives a proof that does not work.
     1.5    - Auto Sledgehammer now minimizes and preplays the results.
     1.6  
     1.7 +* Nitpick:
     1.8 +  - Removed "check_potential" and "check_genuine" options.
     1.9 +
    1.10  
    1.11  New in Isabelle2015 (May 2015)
    1.12  ------------------------------
     2.1 --- a/src/Doc/Nitpick/document/root.tex	Fri May 29 17:17:50 2015 +0200
     2.2 +++ b/src/Doc/Nitpick/document/root.tex	Fri May 29 17:56:43 2015 +0200
     2.3 @@ -463,35 +463,26 @@
     2.4  \postw
     2.5  
     2.6  With infinite types, we don't always have the luxury of a genuine counterexample
     2.7 -and must often content ourselves with a potentially spurious one. The tedious
     2.8 -task of finding out whether the potentially spurious counterexample is in fact
     2.9 -genuine can be delegated to \textit{auto} by passing \textit{check\_potential}.
    2.10 +and must often content ourselves with a potentially spurious one.
    2.11  For example:
    2.12  
    2.13  \prew
    2.14  \textbf{lemma} ``$\forall n.\; \textit{Suc}~n \mathbin{\not=} n \,\Longrightarrow\, P$'' \\
    2.15 -\textbf{nitpick} [\textit{card~nat}~= 50, \textit{check\_potential}] \\[2\smallskipamount]
    2.16 +\textbf{nitpick} [\textit{card~nat}~= 50] \\[2\smallskipamount]
    2.17  \slshape Warning: The conjecture either trivially holds for the given scopes or lies outside Nitpick's supported
    2.18  fragment. Only potentially spurious counterexamples may be found. \\[2\smallskipamount]
    2.19  Nitpick found a potentially spurious counterexample: \\[2\smallskipamount]
    2.20  \hbox{}\qquad Free variable: \nopagebreak \\
    2.21 -\hbox{}\qquad\qquad $P = \textit{False}$ \\[2\smallskipamount]
    2.22 -Confirmation by ``\textit{auto}'': The above counterexample is genuine.
    2.23 +\hbox{}\qquad\qquad $P = \textit{False}$
    2.24  \postw
    2.25  
    2.26 -You might wonder why the counterexample is first reported as potentially
    2.27 -spurious. The root of the problem is that the bound variable in $\forall n.\;
    2.28 +The issue is that the bound variable in $\forall n.\;
    2.29  \textit{Suc}~n \mathbin{\not=} n$ ranges over an infinite type. If Nitpick finds
    2.30  an $n$ such that $\textit{Suc}~n \mathbin{=} n$, it evaluates the assumption to
    2.31  \textit{False}; but otherwise, it does not know anything about values of $n \ge
    2.32  \textit{card~nat}$ and must therefore evaluate the assumption to~$\unk$, not
    2.33 -\textit{True}. Since the assumption can never be satisfied, the putative lemma
    2.34 -can never be falsified.
    2.35 -
    2.36 -Incidentally, if you distrust the so-called genuine counterexamples, you can
    2.37 -enable \textit{check\_\allowbreak genuine} to verify them as well. However, be
    2.38 -aware that \textit{auto} will usually fail to prove that the counterexample is
    2.39 -genuine or spurious.
    2.40 +\textit{True}. Since the assumption can never be fully satisfied by Nitpick,
    2.41 +the putative lemma can never be falsified.
    2.42  
    2.43  Some conjectures involving elementary number theory make Nitpick look like a
    2.44  giant with feet of clay:
    2.45 @@ -1746,8 +1737,7 @@
    2.46  
    2.47  The options are categorized as follows:\ mode of operation
    2.48  (\S\ref{mode-of-operation}), scope of search (\S\ref{scope-of-search}), output
    2.49 -format (\S\ref{output-format}), automatic counterexample checks
    2.50 -(\S\ref{authentication}), regression testing (\S\ref{regression-testing}),
    2.51 +format (\S\ref{output-format}), regression testing (\S\ref{regression-testing}),
    2.52  optimizations (\S\ref{optimizations}), and timeouts (\S\ref{timeouts}).
    2.53  
    2.54  If you use Isabelle/jEdit, Nitpick also provides an automatic mode that can
    2.55 @@ -1757,9 +1747,9 @@
    2.56  \textit{assms} (\S\ref{mode-of-operation}), and \textit{mono}
    2.57  (\S\ref{scope-of-search}) are implicitly enabled, \textit{blocking}
    2.58  (\S\ref{mode-of-operation}), \textit{verbose} (\S\ref{output-format}), and
    2.59 -\textit{debug} (\S\ref{output-format}) are disabled, \textit{max\_threads}
    2.60 -(\S\ref{optimizations}) is taken to be 1, \textit{max\_potential}
    2.61 -(\S\ref{output-format}) is taken to be 0, and \textit{timeout}
    2.62 +\textit{debug} (\S\ref{output-format}) are disabled, \textit{max\_potential}
    2.63 +(\S\ref{output-format}) is taken to be 0, \textit{max\_threads}
    2.64 +(\S\ref{optimizations}) is taken to be 1, and \textit{timeout}
    2.65  (\S\ref{timeouts}) is superseded by the ``Auto Time Limit'' in jEdit. Nitpick's
    2.66  output is also more concise.
    2.67  
    2.68 @@ -2112,8 +2102,7 @@
    2.69  the counterexamples may be identical.
    2.70  
    2.71  \nopagebreak
    2.72 -{\small See also \textit{check\_potential} (\S\ref{authentication}) and
    2.73 -\textit{sat\_solver} (\S\ref{optimizations}).}
    2.74 +{\small See also \textit{sat\_solver} (\S\ref{optimizations}).}
    2.75  
    2.76  \opdefault{max\_genuine}{int}{\upshape 1}
    2.77  Specifies the maximum number of genuine counterexamples to display. If you set
    2.78 @@ -2122,8 +2111,7 @@
    2.79  many of the counterexamples may be identical.
    2.80  
    2.81  \nopagebreak
    2.82 -{\small See also \textit{check\_genuine} (\S\ref{authentication}) and
    2.83 -\textit{sat\_solver} (\S\ref{optimizations}).}
    2.84 +{\small See also \textit{sat\_solver} (\S\ref{optimizations}).}
    2.85  
    2.86  \opnodefault{eval}{term\_list}
    2.87  Specifies the list of terms whose values should be displayed along with
    2.88 @@ -2166,31 +2154,10 @@
    2.89  the \textit{format}~\qty{term} option described above.
    2.90  \end{enum}
    2.91  
    2.92 -\subsection{Authentication}
    2.93 -\label{authentication}
    2.94 +\subsection{Regression Testing}
    2.95 +\label{regression-testing}
    2.96  
    2.97  \begin{enum}
    2.98 -\opfalse{check\_potential}{trust\_potential}
    2.99 -Specifies whether potentially spurious counterexamples should be given to
   2.100 -Isabelle's \textit{auto} tactic to assess their validity. If a potentially
   2.101 -spurious counterexample is shown to be genuine, Nitpick displays a message to
   2.102 -this effect and terminates.
   2.103 -
   2.104 -\nopagebreak
   2.105 -{\small See also \textit{max\_potential} (\S\ref{output-format}).}
   2.106 -
   2.107 -\opfalse{check\_genuine}{trust\_genuine}
   2.108 -Specifies whether genuine and quasi genuine counterexamples should be given to
   2.109 -Isabelle's \textit{auto} tactic to assess their validity. If a ``genuine''
   2.110 -counterexample is shown to be spurious, the user is kindly asked to send a bug
   2.111 -report to the author at \authoremail.
   2.112 -
   2.113 -\nopagebreak
   2.114 -{\small See also \textit{max\_genuine} (\S\ref{output-format}).}
   2.115 -
   2.116 -\subsection{Regression Testing}
   2.117 -\label{regression-testing}
   2.118 -
   2.119  \opnodefault{expect}{string}
   2.120  Specifies the expected outcome, which must be one of the following:
   2.121  
   2.122 @@ -2426,15 +2393,12 @@
   2.123  \opdefault{tac\_timeout}{float}{\upshape 0.5}
   2.124  Specifies the maximum number of seconds that should be used by internal
   2.125  tactics---\textit{lexicographic\_order} and \textit{size\_change} when checking
   2.126 -whether a (co)in\-duc\-tive predicate is well-founded, \textit{auto} tactic when
   2.127 -checking a counterexample, or the monotonicity inference. Nitpick tries to honor
   2.128 -this constraint but offers no guarantees.
   2.129 +whether a (co)in\-duc\-tive predicate is well-founded or the monotonicity
   2.130 +inference. Nitpick tries to honor this constraint but offers no guarantees.
   2.131  
   2.132  \nopagebreak
   2.133 -{\small See also \textit{wf} (\S\ref{scope-of-search}),
   2.134 -\textit{mono} (\S\ref{scope-of-search}),
   2.135 -\textit{check\_potential} (\S\ref{authentication}),
   2.136 -and \textit{check\_genuine} (\S\ref{authentication}).}
   2.137 +{\small See also \textit{wf} (\S\ref{scope-of-search}) and
   2.138 +\textit{mono} (\S\ref{scope-of-search}).}
   2.139  \end{enum}
   2.140  
   2.141  \section{Attribute Reference}
   2.142 @@ -2501,7 +2465,7 @@
   2.143  
   2.144  \nopagebreak
   2.145  This attribute specifies the (free-form) specification of a constant defined
   2.146 -using the \hbox{(\textbf{ax\_})}\allowbreak\textbf{specification} command.
   2.147 +using the \textbf{specification} command.
   2.148  \end{enum}
   2.149  
   2.150  When faced with a constant, Nitpick proceeds as follows:
   2.151 @@ -2515,7 +2479,7 @@
   2.152  constant.
   2.153  
   2.154  \item[3.] Otherwise, if the constant was defined using the
   2.155 -\hbox{(\textbf{ax\_})}\allowbreak\textbf{specification} command and the
   2.156 +\allowbreak\textbf{specification} command and the
   2.157  \textit{nitpick\_choice\_spec} set associated with the constant is not empty, it
   2.158  uses these theorems as the specification of the constant.
   2.159  
     3.1 --- a/src/HOL/Nitpick_Examples/Manual_Nits.thy	Fri May 29 17:17:50 2015 +0200
     3.2 +++ b/src/HOL/Nitpick_Examples/Manual_Nits.thy	Fri May 29 17:56:43 2015 +0200
     3.3 @@ -74,7 +74,7 @@
     3.4  oops
     3.5  
     3.6  lemma "\<forall>n. Suc n \<noteq> n \<Longrightarrow> P"
     3.7 -nitpick [card nat = 100, check_potential, tac_timeout = 5, expect = genuine]
     3.8 +nitpick [card nat = 100, expect = potential]
     3.9  oops
    3.10  
    3.11  lemma "P Suc"
     4.1 --- a/src/HOL/Tools/Nitpick/nitpick.ML	Fri May 29 17:17:50 2015 +0200
     4.2 +++ b/src/HOL/Tools/Nitpick/nitpick.ML	Fri May 29 17:56:43 2015 +0200
     4.3 @@ -52,8 +52,6 @@
     4.4       atomss: (typ option * string list) list,
     4.5       max_potential: int,
     4.6       max_genuine: int,
     4.7 -     check_potential: bool,
     4.8 -     check_genuine: bool,
     4.9       batch_size: int,
    4.10       expect: string}
    4.11  
    4.12 @@ -138,8 +136,6 @@
    4.13     atomss: (typ option * string list) list,
    4.14     max_potential: int,
    4.15     max_genuine: int,
    4.16 -   check_potential: bool,
    4.17 -   check_genuine: bool,
    4.18     batch_size: int,
    4.19     expect: string}
    4.20  
    4.21 @@ -234,7 +230,7 @@
    4.22           total_consts, needs, peephole_optim, datatype_sym_break,
    4.23           kodkod_sym_break, tac_timeout, max_threads, show_types, show_skolems,
    4.24           show_consts, evals, formats, atomss, max_potential, max_genuine,
    4.25 -         check_potential, check_genuine, batch_size, ...} = params
    4.26 +         batch_size, ...} = params
    4.27      val outcome = Synchronized.var "Nitpick.outcome" (Queue.empty: string Queue.T)
    4.28      fun pprint print prt =
    4.29        if mode = Auto_Try then
    4.30 @@ -669,25 +665,7 @@
    4.31                Pretty.indent indent_size reconstructed_model]);
    4.32           print_t (K "% SZS output end FiniteModel");
    4.33           if genuine then
    4.34 -           (if check_genuine then
    4.35 -              case prove_hol_model scope tac_timeout free_names sel_names
    4.36 -                                   rel_table bounds (assms_prop ()) of
    4.37 -                SOME true =>
    4.38 -                print ("Confirmation by \"auto\": The above " ^
    4.39 -                       das_wort_model ^ " is really genuine.")
    4.40 -              | SOME false =>
    4.41 -                if genuine_means_genuine then
    4.42 -                  error ("A supposedly genuine " ^ das_wort_model ^ " was \
    4.43 -                         \shown to be spurious by \"auto\".\nThis should never \
    4.44 -                         \happen.\nPlease send a bug report to blanchet\
    4.45 -                         \te@in.tum.de.")
    4.46 -                 else
    4.47 -                   print ("Refutation by \"auto\": The above " ^
    4.48 -                          das_wort_model ^ " is spurious.")
    4.49 -               | NONE => print "No confirmation by \"auto\"."
    4.50 -            else
    4.51 -              ();
    4.52 -            if has_lonely_bool_var orig_t then
    4.53 +           (if has_lonely_bool_var orig_t then
    4.54                print "Hint: Maybe you forgot a colon after the lemma's name?"
    4.55              else if has_syntactic_sorts orig_t then
    4.56                print "Hint: Maybe you forgot a type constraint?"
    4.57 @@ -725,24 +703,7 @@
    4.58              NONE)
    4.59           else
    4.60             if not genuine then
    4.61 -             (Unsynchronized.inc met_potential;
    4.62 -              if check_potential then
    4.63 -                let
    4.64 -                  val status = prove_hol_model scope tac_timeout free_names
    4.65 -                                               sel_names rel_table bounds
    4.66 -                                               (assms_prop ())
    4.67 -                in
    4.68 -                  (case status of
    4.69 -                     SOME true => print ("Confirmation by \"auto\": The \
    4.70 -                                         \above " ^ das_wort_model ^
    4.71 -                                         " is genuine.")
    4.72 -                   | SOME false => print ("Refutation by \"auto\": The above " ^
    4.73 -                                          das_wort_model ^ " is spurious.")
    4.74 -                   | NONE => print "No confirmation by \"auto\".");
    4.75 -                  status
    4.76 -                end
    4.77 -              else
    4.78 -                NONE)
    4.79 +             (Unsynchronized.inc met_potential; NONE)
    4.80             else
    4.81               NONE)
    4.82          |> pair genuine_means_genuine
     5.1 --- a/src/HOL/Tools/Nitpick/nitpick_commands.ML	Fri May 29 17:17:50 2015 +0200
     5.2 +++ b/src/HOL/Tools/Nitpick/nitpick_commands.ML	Fri May 29 17:56:43 2015 +0200
     5.3 @@ -69,9 +69,7 @@
     5.4     ("show_consts", "false"),
     5.5     ("format", "1"),
     5.6     ("max_potential", "1"),
     5.7 -   ("max_genuine", "1"),
     5.8 -   ("check_potential", "false"),
     5.9 -   ("check_genuine", "false")]
    5.10 +   ("max_genuine", "1")]
    5.11  
    5.12  val negated_params =
    5.13    [("dont_box", "box"),
    5.14 @@ -95,9 +93,7 @@
    5.15     ("dont_spy", "spy"),
    5.16     ("hide_types", "show_types"),
    5.17     ("hide_skolems", "show_skolems"),
    5.18 -   ("hide_consts", "show_consts"),
    5.19 -   ("trust_potential", "check_potential"),
    5.20 -   ("trust_genuine", "check_genuine")]
    5.21 +   ("hide_consts", "show_consts")]
    5.22  
    5.23  fun is_known_raw_param s =
    5.24    AList.defined (op =) default_default_params s orelse
    5.25 @@ -270,8 +266,6 @@
    5.26      val max_potential =
    5.27        if mode = Normal then Int.max (0, lookup_int "max_potential") else 0
    5.28      val max_genuine = Int.max (0, lookup_int "max_genuine")
    5.29 -    val check_potential = lookup_bool "check_potential"
    5.30 -    val check_genuine = lookup_bool "check_genuine"
    5.31      val batch_size =
    5.32        case lookup_int_option "batch_size" of
    5.33          SOME n => Int.max (1, n)
    5.34 @@ -294,7 +288,6 @@
    5.35       show_types = show_types, show_skolems = show_skolems,
    5.36       show_consts = show_consts, evals = evals, formats = formats,
    5.37       atomss = atomss, max_potential = max_potential, max_genuine = max_genuine,
    5.38 -     check_potential = check_potential, check_genuine = check_genuine,
    5.39       batch_size = batch_size, expect = expect}
    5.40    end
    5.41  
     6.1 --- a/src/HOL/Tools/Nitpick/nitpick_model.ML	Fri May 29 17:17:50 2015 +0200
     6.2 +++ b/src/HOL/Tools/Nitpick/nitpick_model.ML	Fri May 29 17:56:43 2015 +0200
     6.3 @@ -39,9 +39,6 @@
     6.4      -> (typ option * string list) list -> (string * typ) list ->
     6.5      (string * typ) list -> nut list -> nut list -> nut list ->
     6.6      nut NameTable.table -> Kodkod.raw_bound list -> Pretty.T * bool
     6.7 -  val prove_hol_model :
     6.8 -    scope -> Time.time -> nut list -> nut list -> nut NameTable.table
     6.9 -    -> Kodkod.raw_bound list -> term -> bool option
    6.10  end;
    6.11  
    6.12  structure Nitpick_Model : NITPICK_MODEL =
    6.13 @@ -1036,63 +1033,4 @@
    6.14       forall (is_codatatype_wellformed codatatypes) codatatypes)
    6.15    end
    6.16  
    6.17 -fun term_for_name pool scope atomss sel_names rel_table bounds name =
    6.18 -  let val T = type_of name in
    6.19 -    tuple_list_for_name rel_table bounds name
    6.20 -    |> reconstruct_term (not (is_fully_representable_set name)) false pool
    6.21 -                        (("", ""), ("", "")) scope atomss sel_names rel_table
    6.22 -                        bounds T T (rep_of name)
    6.23 -  end
    6.24 -
    6.25 -fun prove_hol_model (scope as {hol_ctxt = {thy, ctxt, debug, ...},
    6.26 -                               card_assigns, ...})
    6.27 -                    auto_timeout free_names sel_names rel_table bounds prop =
    6.28 -  let
    6.29 -    val pool = Unsynchronized.ref []
    6.30 -    val atomss = [(NONE, [])]
    6.31 -    fun free_type_assm (T, k) =
    6.32 -      let
    6.33 -        fun atom j = nth_atom thy atomss pool true T j
    6.34 -        fun equation_for_atom j = HOLogic.eq_const T $ Bound 0 $ atom j
    6.35 -        val eqs = map equation_for_atom (index_seq 0 k)
    6.36 -        val compreh_assm =
    6.37 -          Const (@{const_name All}, (T --> bool_T) --> bool_T)
    6.38 -              $ Abs ("x", T, foldl1 HOLogic.mk_disj eqs)
    6.39 -        val distinct_assm = distinctness_formula T (map atom (index_seq 0 k))
    6.40 -      in s_conj (compreh_assm, distinct_assm) end
    6.41 -    fun free_name_assm name =
    6.42 -      HOLogic.mk_eq (Free (nickname_of name, type_of name),
    6.43 -                     term_for_name pool scope atomss sel_names rel_table bounds
    6.44 -                                   name)
    6.45 -    val freeT_assms = map free_type_assm (filter (is_TFree o fst) card_assigns)
    6.46 -    val model_assms = map free_name_assm free_names
    6.47 -    val assm = foldr1 s_conj (freeT_assms @ model_assms)
    6.48 -    fun try_out negate =
    6.49 -      let
    6.50 -        val concl = (negate ? curry (op $) @{const Not})
    6.51 -                    (Object_Logic.atomize_term ctxt prop)
    6.52 -        val prop = HOLogic.mk_Trueprop (HOLogic.mk_imp (assm, concl))
    6.53 -                   |> map_types (map_type_tfree
    6.54 -                                     (fn (s, []) => TFree (s, @{sort type})
    6.55 -                                       | x => TFree x))
    6.56 -        val _ =
    6.57 -          if debug then
    6.58 -            (if negate then "Genuineness" else "Spuriousness") ^ " goal: " ^
    6.59 -            Syntax.string_of_term ctxt prop ^ "."
    6.60 -            |> writeln
    6.61 -          else
    6.62 -            ()
    6.63 -        val goal = prop |> Thm.cterm_of ctxt |> Goal.init
    6.64 -      in
    6.65 -        (goal |> SINGLE (DETERM_TIMEOUT auto_timeout (auto_tac ctxt))
    6.66 -              |> the |> Goal.finish ctxt; true)
    6.67 -        handle THM _ => false
    6.68 -             | TimeLimit.TimeOut => false
    6.69 -      end
    6.70 -  in
    6.71 -    if try_out false then SOME true
    6.72 -    else if try_out true then SOME false
    6.73 -    else NONE
    6.74 -  end
    6.75 -
    6.76  end;