--- 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)
------------------------------
--- 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.
--- 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"
--- 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
--- 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
--- 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;