--- a/doc-src/Nitpick/nitpick.tex Wed Feb 17 10:28:37 2010 +0100
+++ b/doc-src/Nitpick/nitpick.tex Wed Feb 17 11:19:48 2010 +0100
@@ -1369,7 +1369,7 @@
\prew
\slshape
Hint: To check that the induction hypothesis is general enough, try this command:
-\textbf{nitpick}~[\textit{non\_std} ``${\kern1pt'a}~\textit{bin\_tree}$'', \textit{show\_all}].
+\textbf{nitpick}~[\textit{non\_std}, \textit{show\_all}].
\postw
If we follow the hint, we get a ``nonstandard'' counterexample for the step:
@@ -1397,11 +1397,10 @@
\postw
Reading the Nitpick manual is a most excellent idea.
-But what's going on? The \textit{non\_std} ``${\kern1pt'a}~\textit{bin\_tree}$''
-option told the tool to look for nonstandard models of binary trees, which
-means that new ``nonstandard'' trees $\xi_1, \xi_2, \ldots$, are now allowed in
-addition to the standard trees generated by the \textit{Leaf} and
-\textit{Branch} constructors.%
+But what's going on? The \textit{non\_std} option told the tool to look for
+nonstandard models of binary trees, which means that new ``nonstandard'' trees
+$\xi_1, \xi_2, \ldots$, are now allowed in addition to the standard trees
+generated by the \textit{Leaf} and \textit{Branch} constructors.%
\footnote{Notice the similarity between allowing nonstandard trees here and
allowing unreachable states in the preceding example (by removing the ``$n \in
\textit{reach\/}$'' assumption). In both cases, we effectively enlarge the
--- a/src/HOL/Tools/Nitpick/nitpick.ML Wed Feb 17 10:28:37 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick.ML Wed Feb 17 11:19:48 2010 +0100
@@ -382,29 +382,22 @@
else
()
val deep_dataTs = filter is_deep_datatype all_Ts
- (* FIXME: Implement proper detection of induction datatypes. *)
+ (* This detection code is an ugly hack. Fortunately, it is used only to
+ provide a hint to the user. *)
(* string * (Rule_Cases.T * bool) -> bool *)
- fun is_inductive_case (_, (Rule_Cases.Case {fixes, assumes, ...}, _)) =
- false
-(*
- not (null fixes) andalso exists (String.isSuffix ".hyps" o fst) assumes
-*)
- (* unit -> typ list *)
- val induct_dataTs =
- if exists is_inductive_case (ProofContext.cases_of ctxt) then
- filter (is_datatype thy) all_Ts
- else
- []
- val _ = if standard andalso not (null induct_dataTs) then
+ fun is_struct_induct_step (name, (Rule_Cases.Case {fixes, assumes, ...}, _)) =
+ not (null fixes) andalso
+ exists (String.isSuffix ".hyps" o fst) assumes andalso
+ exists (exists (curry (op =) name o shortest_name o fst)
+ o datatype_constrs hol_ctxt) deep_dataTs
+ val likely_in_struct_induct_step =
+ exists is_struct_induct_step (ProofContext.cases_of ctxt)
+ val _ = if standard andalso likely_in_struct_induct_step then
pprint_m (fn () => Pretty.blk (0,
pstrs "Hint: To check that the induction hypothesis is \
\general enough, try this command: " @
[Pretty.mark Markup.sendback (Pretty.blk (0,
- pstrs ("nitpick [" ^
- commas (map (prefix "non_std " o maybe_quote
- o unyxml o string_for_type ctxt)
- induct_dataTs) ^
- ", show_consts]")))] @ pstrs "."))
+ pstrs ("nitpick [non_std, show_all]")))] @ pstrs "."))
else
()
(*
@@ -635,7 +628,7 @@
| NONE => print "No confirmation by \"auto\".")
else
();
- if not standard andalso not (null induct_dataTs) then
+ if not standard andalso likely_in_struct_induct_step then
print "The existence of a nonstandard model suggests that the \
\induction hypothesis is not general enough or perhaps even \
\wrong. See the \"Inductive Properties\" section of the \
@@ -874,7 +867,7 @@
if max_potential = original_max_potential then
(print_m (fn () =>
"Nitpick found no " ^ das_wort_model ^ "." ^
- (if not standard andalso not (null induct_dataTs) then
+ (if not standard andalso likely_in_struct_induct_step then
" This suggests that the induction hypothesis might be \
\general enough to prove this subgoal."
else