# HG changeset patch
# User blanchet
# Date 1266401988 -3600
# Node ID 8580ba6514896d5c4dc2a167d677b8722d8e73fa
# Parent  4c39632b811f3e15e3d510baba87eed20dc5a3b1
reintroduce structural induction hint in Nitpick

diff -r 4c39632b811f -r 8580ba651489 doc-src/Nitpick/nitpick.tex
--- 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
diff -r 4c39632b811f -r 8580ba651489 src/HOL/Tools/Nitpick/nitpick.ML
--- 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