# HG changeset patch # User blanchet # Date 1301927316 -7200 # Node ID de9d43c427ae90be535461bc6d6f8caa88eebe91 # Parent 9ca13615c619999ac4aad8b9e9fe61e88d8a0a26 document "nitpick(_params)", "refute(_params)", "try", "sledgehammer(_params)", and "solve_direct" diff -r 9ca13615c619 -r de9d43c427ae doc-src/IsarRef/Thy/HOL_Specific.thy --- 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 \"} \\ + @{command_def (HOL) "try"}@{text "\<^sup>*"} & : & @{text "proof \"} \\ + @{command_def (HOL) "sledgehammer"}@{text "\<^sup>*"} & : & @{text "proof \"} \\ + @{command_def (HOL) "sledgehammer_params"} & : & @{text "theory \ 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 \"} \\ @{command_def (HOL) "quickcheck"}@{text "\<^sup>*"} & : & @{text "proof \"} \\ - @{command_def (HOL) "quickcheck_params"} & : & @{text "theory \ theory"} + @{command_def (HOL) "refute"}@{text "\<^sup>*"} & : & @{text "proof \"} \\ + @{command_def (HOL) "nitpick"}@{text "\<^sup>*"} & : & @{text "proof \"} \\ + @{command_def (HOL) "quickcheck_params"} & : & @{text "theory \ theory"} \\ + @{command_def (HOL) "refute_params"} & : & @{text "theory \ theory"} \\ + @{command_def (HOL) "nitpick_params"} & : & @{text "theory \ 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} *} diff -r 9ca13615c619 -r de9d43c427ae doc-src/IsarRef/Thy/document/HOL_Specific.tex --- 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}% diff -r 9ca13615c619 -r de9d43c427ae doc-src/manual.bib --- 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",