document "nitpick(_params)", "refute(_params)", "try", "sledgehammer(_params)", and "solve_direct"

--- a/doc-src/IsarRef/Thy/HOL_Specific.thy	Mon Apr 04 14:44:11 2011 +0200
+++ b/doc-src/IsarRef/Thy/HOL_Specific.thy	Mon Apr 04 16:28:36 2011 +0200
@@ -920,27 +920,88 @@
 *}
 
 
+section {* Proving propositions *}
+
+text {*
+  In addition to the standard proof methods, a number of diagnosis
+  tools search for proofs and provide an Isar proof snippet on success.
+  These tools are available via the following commands.
+
+  \begin{matharray}{rcl}
+    @{command_def (HOL) "solve_direct"}@{text "\<^sup>*"} & : & @{text "proof \<rightarrow>"} \\
+    @{command_def (HOL) "try"}@{text "\<^sup>*"} & : & @{text "proof \<rightarrow>"} \\
+    @{command_def (HOL) "sledgehammer"}@{text "\<^sup>*"} & : & @{text "proof \<rightarrow>"} \\
+    @{command_def (HOL) "sledgehammer_params"} & : & @{text "theory \<rightarrow> theory"}
+  \end{matharray}
+
+  \begin{rail}
+    'solve_direct'
+    ;
+
+    'try' ( ( ( 'simp' | 'intro' | 'elim' | 'dest' ) ':' thmrefs ) + ) ? nat?
+    ;
+
+    'sledgehammer' ( '[' args ']' ) ? facts? nat?
+    ;
+
+    'sledgehammer_params' ( ( '[' args ']' ) ? )
+    ;
+
+    args: ( name '=' value + ',' )
+    ;
+
+    facts: '(' ( ( ( ( 'add' | 'del' ) ':' ) ? thmrefs ) + ) ? ')'
+    ;
+  \end{rail}
+
+  \begin{description}
+
+  \item @{command (HOL) "solve_direct"} checks whether the current subgoals can
+    be solved directly by an existing theorem. Duplicate lemmas can be detected
+    in this way.
+
+  \item @{command (HOL) "try"} attempts to prove a subgoal using a combination
+    of standard proof methods (@{text auto}, @{text simp}, @{text blast}, etc.).
+    Additional facts supplied via @{text "simp:"}, @{text "intro:"},
+    @{text "elim:"}, and @{text "dest:"} are passed to the appropriate proof
+    methods.
+
+  \item @{command (HOL) "sledgehammer"} attempts to prove a subgoal using external
+    automatic provers (resolution provers and SMT solvers). See the Sledgehammer
+    manual \cite{isabelle-sledgehammer} for details.
+
+  \item @{command (HOL) "sledgehammer_params"} changes
+    @{command (HOL) "sledgehammer"} configuration options persistently.
+
+  \end{description}
+*}
+
+
 section {* Checking and refuting propositions *}
 
 text {*
   Identifying incorrect propositions usually involves evaluation of
-  particular assignments and systematic counter example search.  This
+  particular assignments and systematic counterexample search.  This
   is supported by the following commands.
 
   \begin{matharray}{rcl}
     @{command_def (HOL) "value"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
     @{command_def (HOL) "quickcheck"}@{text "\<^sup>*"} & : & @{text "proof \<rightarrow>"} \\
-    @{command_def (HOL) "quickcheck_params"} & : & @{text "theory \<rightarrow> theory"}
+    @{command_def (HOL) "refute"}@{text "\<^sup>*"} & : & @{text "proof \<rightarrow>"} \\
+    @{command_def (HOL) "nitpick"}@{text "\<^sup>*"} & : & @{text "proof \<rightarrow>"} \\
+    @{command_def (HOL) "quickcheck_params"} & : & @{text "theory \<rightarrow> theory"} \\
+    @{command_def (HOL) "refute_params"} & : & @{text "theory \<rightarrow> theory"} \\
+    @{command_def (HOL) "nitpick_params"} & : & @{text "theory \<rightarrow> theory"}
   \end{matharray}
 
   \begin{rail}
     'value' ( ( '[' name ']' ) ? ) modes? term
     ;
 
-    'quickcheck' ( ( '[' args ']' ) ? ) nat?
+    ('quickcheck' | 'refute' | 'nitpick')  ( ( '[' args ']' ) ? ) nat?
     ;
 
-    'quickcheck_params' ( ( '[' args ']' ) ? )
+    ('quickcheck_params' | 'refute_params' | 'nitpick_params') ( ( '[' args ']' ) ? )
     ;
 
     modes: '(' (name + ) ')'
@@ -964,7 +1025,7 @@
     and \emph{code} for code generation in SML.
 
   \item @{command (HOL) "quickcheck"} tests the current goal for
-    counter examples using a series of assignments for its
+    counterexamples using a series of assignments for its
     free variables; by default the first subgoal is tested, an other
     can be selected explicitly using an optional goal index.
     Assignments can be chosen exhausting the search space upto a given
@@ -1010,8 +1071,49 @@
 
     These option can be given within square brackets.
 
-  \item @{command (HOL) "quickcheck_params"} changes quickcheck
-    configuration options persitently.
+  \item @{command (HOL) "quickcheck_params"} changes
+    @{command (HOL) "quickcheck"} configuration options persistently.
+
+  \item @{command (HOL) "refute"} tests the current goal for
+    counterexamples using a reduction to SAT. The following configuration
+    options are supported:
+
+    \begin{description}
+
+    \item[@{text minsize}] specifies the minimum size (cardinality) of the
+      models to search for.
+
+    \item[@{text maxsize}] specifies the maximum size (cardinality) of the
+      models to search for. Nonpositive values mean $\infty$.
+
+    \item[@{text maxvars}] specifies the maximum number of Boolean variables
+    to use when transforming the term into a propositional formula.
+    Nonpositive values mean $\infty$.
+
+    \item[@{text satsolver}] specifies the SAT solver to use.
+
+    \item[@{text no_assms}] specifies whether assumptions in
+    structured proofs should be ignored.
+
+    \item[@{text maxtime}] sets the time limit in seconds.
+
+    \item[@{text expect}] can be used to check if the user's
+    expectation was met (@{text genuine}, @{text potential},
+    @{text none}, or @{text unknown}).
+
+    \end{description}
+
+    These option can be given within square brackets.
+
+  \item @{command (HOL) "refute_params"} changes
+    @{command (HOL) "refute"} configuration options persistently.
+
+  \item @{command (HOL) "nitpick"} tests the current goal for counterexamples
+    using a reduction to first-order relational logic. See the Nitpick manual
+    \cite{isabelle-nitpick} for details.
+
+  \item @{command (HOL) "nitpick_params"} changes
+    @{command (HOL) "nitpick"} configuration options persistently.
 
   \end{description}
 *}

--- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Mon Apr 04 14:44:11 2011 +0200
+++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Mon Apr 04 16:28:36 2011 +0200
@@ -936,29 +936,92 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
+\isamarkupsection{Proving propositions%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+In addition to the standard proof methods, a number of diagnosis
+  tools search for proofs and provide an Isar proof snippet on success.
+  These tools are available via the following commands.
+
+  \begin{matharray}{rcl}
+    \indexdef{HOL}{command}{solve\_direct}\hypertarget{command.HOL.solve-direct}{\hyperlink{command.HOL.solve-direct}{\mbox{\isa{\isacommand{solve{\isaliteral{5F}{\isacharunderscore}}direct}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}proof\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}{\isaliteral{22}{\isachardoublequote}}} \\
+    \indexdef{HOL}{command}{try}\hypertarget{command.HOL.try}{\hyperlink{command.HOL.try}{\mbox{\isa{\isacommand{try}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}proof\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}{\isaliteral{22}{\isachardoublequote}}} \\
+    \indexdef{HOL}{command}{sledgehammer}\hypertarget{command.HOL.sledgehammer}{\hyperlink{command.HOL.sledgehammer}{\mbox{\isa{\isacommand{sledgehammer}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}proof\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}{\isaliteral{22}{\isachardoublequote}}} \\
+    \indexdef{HOL}{command}{sledgehammer\_params}\hypertarget{command.HOL.sledgehammer-params}{\hyperlink{command.HOL.sledgehammer-params}{\mbox{\isa{\isacommand{sledgehammer{\isaliteral{5F}{\isacharunderscore}}params}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{22}{\isachardoublequote}}}
+  \end{matharray}
+
+  \begin{rail}
+    'solve_direct'
+    ;
+
+    'try' ( ( ( 'simp' | 'intro' | 'elim' | 'dest' ) ':' thmrefs ) + ) ? nat?
+    ;
+
+    'sledgehammer' ( '[' args ']' ) ? facts? nat?
+    ;
+
+    'sledgehammer_params' ( ( '[' args ']' ) ? )
+    ;
+
+    args: ( name '=' value + ',' )
+    ;
+
+    facts: '(' ( ( ( ( 'add' | 'del' ) ':' ) ? thmrefs ) + ) ? ')'
+    ;
+  \end{rail}
+
+  \begin{description}
+
+  \item \hyperlink{command.HOL.solve-direct}{\mbox{\isa{\isacommand{solve{\isaliteral{5F}{\isacharunderscore}}direct}}}} checks whether the current subgoals can
+    be solved directly by an existing theorem. Duplicate lemmas can be detected
+    in this way.
+
+  \item \hyperlink{command.HOL.try}{\mbox{\isa{\isacommand{try}}}} attempts to prove a subgoal using a combination
+    of standard proof methods (\isa{auto}, \isa{simp}, \isa{blast}, etc.).
+    Additional facts supplied via \isa{{\isaliteral{22}{\isachardoublequote}}simp{\isaliteral{3A}{\isacharcolon}}{\isaliteral{22}{\isachardoublequote}}}, \isa{{\isaliteral{22}{\isachardoublequote}}intro{\isaliteral{3A}{\isacharcolon}}{\isaliteral{22}{\isachardoublequote}}},
+    \isa{{\isaliteral{22}{\isachardoublequote}}elim{\isaliteral{3A}{\isacharcolon}}{\isaliteral{22}{\isachardoublequote}}}, and \isa{{\isaliteral{22}{\isachardoublequote}}dest{\isaliteral{3A}{\isacharcolon}}{\isaliteral{22}{\isachardoublequote}}} are passed to the appropriate proof
+    methods.
+
+  \item \hyperlink{command.HOL.sledgehammer}{\mbox{\isa{\isacommand{sledgehammer}}}} attempts to prove a subgoal using external
+    automatic provers (resolution provers and SMT solvers). See the Sledgehammer
+    manual \cite{isabelle-sledgehammer} for details.
+
+  \item \hyperlink{command.HOL.sledgehammer-params}{\mbox{\isa{\isacommand{sledgehammer{\isaliteral{5F}{\isacharunderscore}}params}}}} changes
+    \hyperlink{command.HOL.sledgehammer}{\mbox{\isa{\isacommand{sledgehammer}}}} configuration options persistently.
+
+  \end{description}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
 \isamarkupsection{Checking and refuting propositions%
 }
 \isamarkuptrue%
 %
 \begin{isamarkuptext}%
 Identifying incorrect propositions usually involves evaluation of
-  particular assignments and systematic counter example search.  This
+  particular assignments and systematic counterexample search.  This
   is supported by the following commands.
 
   \begin{matharray}{rcl}
     \indexdef{HOL}{command}{value}\hypertarget{command.HOL.value}{\hyperlink{command.HOL.value}{\mbox{\isa{\isacommand{value}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}context\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}{\isaliteral{22}{\isachardoublequote}}} \\
     \indexdef{HOL}{command}{quickcheck}\hypertarget{command.HOL.quickcheck}{\hyperlink{command.HOL.quickcheck}{\mbox{\isa{\isacommand{quickcheck}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}proof\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}{\isaliteral{22}{\isachardoublequote}}} \\
-    \indexdef{HOL}{command}{quickcheck\_params}\hypertarget{command.HOL.quickcheck-params}{\hyperlink{command.HOL.quickcheck-params}{\mbox{\isa{\isacommand{quickcheck{\isaliteral{5F}{\isacharunderscore}}params}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{22}{\isachardoublequote}}}
+    \indexdef{HOL}{command}{refute}\hypertarget{command.HOL.refute}{\hyperlink{command.HOL.refute}{\mbox{\isa{\isacommand{refute}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}proof\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}{\isaliteral{22}{\isachardoublequote}}} \\
+    \indexdef{HOL}{command}{nitpick}\hypertarget{command.HOL.nitpick}{\hyperlink{command.HOL.nitpick}{\mbox{\isa{\isacommand{nitpick}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}proof\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}{\isaliteral{22}{\isachardoublequote}}} \\
+    \indexdef{HOL}{command}{quickcheck\_params}\hypertarget{command.HOL.quickcheck-params}{\hyperlink{command.HOL.quickcheck-params}{\mbox{\isa{\isacommand{quickcheck{\isaliteral{5F}{\isacharunderscore}}params}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{22}{\isachardoublequote}}} \\
+    \indexdef{HOL}{command}{refute\_params}\hypertarget{command.HOL.refute-params}{\hyperlink{command.HOL.refute-params}{\mbox{\isa{\isacommand{refute{\isaliteral{5F}{\isacharunderscore}}params}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{22}{\isachardoublequote}}} \\
+    \indexdef{HOL}{command}{nitpick\_params}\hypertarget{command.HOL.nitpick-params}{\hyperlink{command.HOL.nitpick-params}{\mbox{\isa{\isacommand{nitpick{\isaliteral{5F}{\isacharunderscore}}params}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{22}{\isachardoublequote}}}
   \end{matharray}
 
   \begin{rail}
     'value' ( ( '[' name ']' ) ? ) modes? term
     ;
 
-    'quickcheck' ( ( '[' args ']' ) ? ) nat?
+    ('quickcheck' | 'refute' | 'nitpick')  ( ( '[' args ']' ) ? ) nat?
     ;
 
-    'quickcheck_params' ( ( '[' args ']' ) ? )
+    ('quickcheck_params' | 'refute_params' | 'nitpick_params') ( ( '[' args ']' ) ? )
     ;
 
     modes: '(' (name + ) ')'
@@ -982,7 +1045,7 @@
     and \emph{code} for code generation in SML.
 
   \item \hyperlink{command.HOL.quickcheck}{\mbox{\isa{\isacommand{quickcheck}}}} tests the current goal for
-    counter examples using a series of assignments for its
+    counterexamples using a series of assignments for its
     free variables; by default the first subgoal is tested, an other
     can be selected explicitly using an optional goal index.
     Assignments can be chosen exhausting the search space upto a given
@@ -1027,8 +1090,49 @@
 
     These option can be given within square brackets.
 
-  \item \hyperlink{command.HOL.quickcheck-params}{\mbox{\isa{\isacommand{quickcheck{\isaliteral{5F}{\isacharunderscore}}params}}}} changes quickcheck
-    configuration options persitently.
+  \item \hyperlink{command.HOL.quickcheck-params}{\mbox{\isa{\isacommand{quickcheck{\isaliteral{5F}{\isacharunderscore}}params}}}} changes
+    \hyperlink{command.HOL.quickcheck}{\mbox{\isa{\isacommand{quickcheck}}}} configuration options persistently.
+
+  \item \hyperlink{command.HOL.refute}{\mbox{\isa{\isacommand{refute}}}} tests the current goal for
+    counterexamples using a reduction to SAT. The following configuration
+    options are supported:
+
+    \begin{description}
+
+    \item[\isa{minsize}] specifies the minimum size (cardinality) of the
+      models to search for.
+
+    \item[\isa{maxsize}] specifies the maximum size (cardinality) of the
+      models to search for. Nonpositive values mean $\infty$.
+
+    \item[\isa{maxvars}] specifies the maximum number of Boolean variables
+    to use when transforming the term into a propositional formula.
+    Nonpositive values mean $\infty$.
+
+    \item[\isa{satsolver}] specifies the SAT solver to use.
+
+    \item[\isa{no{\isaliteral{5F}{\isacharunderscore}}assms}] specifies whether assumptions in
+    structured proofs should be ignored.
+
+    \item[\isa{maxtime}] sets the time limit in seconds.
+
+    \item[\isa{expect}] can be used to check if the user's
+    expectation was met (\isa{genuine}, \isa{potential},
+    \isa{none}, or \isa{unknown}).
+
+    \end{description}
+
+    These option can be given within square brackets.
+
+  \item \hyperlink{command.HOL.refute-params}{\mbox{\isa{\isacommand{refute{\isaliteral{5F}{\isacharunderscore}}params}}}} changes
+    \hyperlink{command.HOL.refute}{\mbox{\isa{\isacommand{refute}}}} configuration options persistently.
+
+  \item \hyperlink{command.HOL.nitpick}{\mbox{\isa{\isacommand{nitpick}}}} tests the current goal for counterexamples
+    using a reduction to first-order relational logic. See the Nitpick manual
+    \cite{isabelle-nitpick} for details.
+
+  \item \hyperlink{command.HOL.nitpick-params}{\mbox{\isa{\isacommand{nitpick{\isaliteral{5F}{\isacharunderscore}}params}}}} changes
+    \hyperlink{command.HOL.nitpick}{\mbox{\isa{\isacommand{nitpick}}}} configuration options persistently.
 
   \end{description}%
 \end{isamarkuptext}%

--- a/doc-src/manual.bib	Mon Apr 04 14:44:11 2011 +0200
+++ b/doc-src/manual.bib	Mon Apr 04 16:28:36 2011 +0200
@@ -260,6 +260,20 @@
 title="Introduction to Functional Programming using Haskell",
 publisher=PH,year=1998}
 
+@manual{isabelle-nitpick,
+  author        = {Jasmin Christian Blanchette},
+  title         = {Picking Nits: A User's Guide to {N}itpick for {I}sabelle/{HOL}},
+  institution   = TUM,
+  note          = {\url{http://isabelle.in.tum.de/doc/nitpick.pdf}}
+}
+
+@manual{isabelle-sledgehammer,
+  author        = {Jasmin Christian Blanchette},
+  title         = {Hammering Away: A User's Guide to {S}ledgehammer for {I}sabelle/{HOL}},
+  institution   = TUM,
+  note          = {\url{http://isabelle.in.tum.de/doc/sledgehammer.pdf}}
+}
+
 @inproceedings{blanchette-nipkow-2010,
   title = "Nitpick: A Counterexample Generator for Higher-Order Logic Based on a Relational Model Finder",
   author = "Jasmin Christian Blanchette and Tobias Nipkow",