1.1 --- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex Mon Apr 04 14:44:11 2011 +0200
1.2 +++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex Mon Apr 04 16:28:36 2011 +0200
1.3 @@ -936,29 +936,92 @@
1.4 \end{isamarkuptext}%
1.5 \isamarkuptrue%
1.6 %
1.7 +\isamarkupsection{Proving propositions%
1.8 +}
1.9 +\isamarkuptrue%
1.10 +%
1.11 +\begin{isamarkuptext}%
1.12 +In addition to the standard proof methods, a number of diagnosis
1.13 + tools search for proofs and provide an Isar proof snippet on success.
1.14 + These tools are available via the following commands.
1.15 +
1.16 + \begin{matharray}{rcl}
1.17 + \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}}} \\
1.18 + \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}}} \\
1.19 + \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}}} \\
1.20 + \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}}}
1.21 + \end{matharray}
1.22 +
1.23 + \begin{rail}
1.24 + 'solve_direct'
1.25 + ;
1.26 +
1.27 + 'try' ( ( ( 'simp' | 'intro' | 'elim' | 'dest' ) ':' thmrefs ) + ) ? nat?
1.28 + ;
1.29 +
1.30 + 'sledgehammer' ( '[' args ']' ) ? facts? nat?
1.31 + ;
1.32 +
1.33 + 'sledgehammer_params' ( ( '[' args ']' ) ? )
1.34 + ;
1.35 +
1.36 + args: ( name '=' value + ',' )
1.37 + ;
1.38 +
1.39 + facts: '(' ( ( ( ( 'add' | 'del' ) ':' ) ? thmrefs ) + ) ? ')'
1.40 + ;
1.41 + \end{rail}
1.42 +
1.43 + \begin{description}
1.44 +
1.45 + \item \hyperlink{command.HOL.solve-direct}{\mbox{\isa{\isacommand{solve{\isaliteral{5F}{\isacharunderscore}}direct}}}} checks whether the current subgoals can
1.46 + be solved directly by an existing theorem. Duplicate lemmas can be detected
1.47 + in this way.
1.48 +
1.49 + \item \hyperlink{command.HOL.try}{\mbox{\isa{\isacommand{try}}}} attempts to prove a subgoal using a combination
1.50 + of standard proof methods (\isa{auto}, \isa{simp}, \isa{blast}, etc.).
1.51 + 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}}},
1.52 + \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
1.53 + methods.
1.54 +
1.55 + \item \hyperlink{command.HOL.sledgehammer}{\mbox{\isa{\isacommand{sledgehammer}}}} attempts to prove a subgoal using external
1.56 + automatic provers (resolution provers and SMT solvers). See the Sledgehammer
1.57 + manual \cite{isabelle-sledgehammer} for details.
1.58 +
1.59 + \item \hyperlink{command.HOL.sledgehammer-params}{\mbox{\isa{\isacommand{sledgehammer{\isaliteral{5F}{\isacharunderscore}}params}}}} changes
1.60 + \hyperlink{command.HOL.sledgehammer}{\mbox{\isa{\isacommand{sledgehammer}}}} configuration options persistently.
1.61 +
1.62 + \end{description}%
1.63 +\end{isamarkuptext}%
1.64 +\isamarkuptrue%
1.65 +%
1.66 \isamarkupsection{Checking and refuting propositions%
1.67 }
1.68 \isamarkuptrue%
1.69 %
1.70 \begin{isamarkuptext}%
1.71 Identifying incorrect propositions usually involves evaluation of
1.72 - particular assignments and systematic counter example search. This
1.73 + particular assignments and systematic counterexample search. This
1.74 is supported by the following commands.
1.75
1.76 \begin{matharray}{rcl}
1.77 \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}}} \\
1.78 \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}}} \\
1.79 - \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}}}
1.80 + \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}}} \\
1.81 + \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}}} \\
1.82 + \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}}} \\
1.83 + \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}}} \\
1.84 + \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}}}
1.85 \end{matharray}
1.86
1.87 \begin{rail}
1.88 'value' ( ( '[' name ']' ) ? ) modes? term
1.89 ;
1.90
1.91 - 'quickcheck' ( ( '[' args ']' ) ? ) nat?
1.92 + ('quickcheck' | 'refute' | 'nitpick') ( ( '[' args ']' ) ? ) nat?
1.93 ;
1.94
1.95 - 'quickcheck_params' ( ( '[' args ']' ) ? )
1.96 + ('quickcheck_params' | 'refute_params' | 'nitpick_params') ( ( '[' args ']' ) ? )
1.97 ;
1.98
1.99 modes: '(' (name + ) ')'
1.100 @@ -982,7 +1045,7 @@
1.101 and \emph{code} for code generation in SML.
1.102
1.103 \item \hyperlink{command.HOL.quickcheck}{\mbox{\isa{\isacommand{quickcheck}}}} tests the current goal for
1.104 - counter examples using a series of assignments for its
1.105 + counterexamples using a series of assignments for its
1.106 free variables; by default the first subgoal is tested, an other
1.107 can be selected explicitly using an optional goal index.
1.108 Assignments can be chosen exhausting the search space upto a given
1.109 @@ -1027,8 +1090,49 @@
1.110
1.111 These option can be given within square brackets.
1.112
1.113 - \item \hyperlink{command.HOL.quickcheck-params}{\mbox{\isa{\isacommand{quickcheck{\isaliteral{5F}{\isacharunderscore}}params}}}} changes quickcheck
1.114 - configuration options persitently.
1.115 + \item \hyperlink{command.HOL.quickcheck-params}{\mbox{\isa{\isacommand{quickcheck{\isaliteral{5F}{\isacharunderscore}}params}}}} changes
1.116 + \hyperlink{command.HOL.quickcheck}{\mbox{\isa{\isacommand{quickcheck}}}} configuration options persistently.
1.117 +
1.118 + \item \hyperlink{command.HOL.refute}{\mbox{\isa{\isacommand{refute}}}} tests the current goal for
1.119 + counterexamples using a reduction to SAT. The following configuration
1.120 + options are supported:
1.121 +
1.122 + \begin{description}
1.123 +
1.124 + \item[\isa{minsize}] specifies the minimum size (cardinality) of the
1.125 + models to search for.
1.126 +
1.127 + \item[\isa{maxsize}] specifies the maximum size (cardinality) of the
1.128 + models to search for. Nonpositive values mean $\infty$.
1.129 +
1.130 + \item[\isa{maxvars}] specifies the maximum number of Boolean variables
1.131 + to use when transforming the term into a propositional formula.
1.132 + Nonpositive values mean $\infty$.
1.133 +
1.134 + \item[\isa{satsolver}] specifies the SAT solver to use.
1.135 +
1.136 + \item[\isa{no{\isaliteral{5F}{\isacharunderscore}}assms}] specifies whether assumptions in
1.137 + structured proofs should be ignored.
1.138 +
1.139 + \item[\isa{maxtime}] sets the time limit in seconds.
1.140 +
1.141 + \item[\isa{expect}] can be used to check if the user's
1.142 + expectation was met (\isa{genuine}, \isa{potential},
1.143 + \isa{none}, or \isa{unknown}).
1.144 +
1.145 + \end{description}
1.146 +
1.147 + These option can be given within square brackets.
1.148 +
1.149 + \item \hyperlink{command.HOL.refute-params}{\mbox{\isa{\isacommand{refute{\isaliteral{5F}{\isacharunderscore}}params}}}} changes
1.150 + \hyperlink{command.HOL.refute}{\mbox{\isa{\isacommand{refute}}}} configuration options persistently.
1.151 +
1.152 + \item \hyperlink{command.HOL.nitpick}{\mbox{\isa{\isacommand{nitpick}}}} tests the current goal for counterexamples
1.153 + using a reduction to first-order relational logic. See the Nitpick manual
1.154 + \cite{isabelle-nitpick} for details.
1.155 +
1.156 + \item \hyperlink{command.HOL.nitpick-params}{\mbox{\isa{\isacommand{nitpick{\isaliteral{5F}{\isacharunderscore}}params}}}} changes
1.157 + \hyperlink{command.HOL.nitpick}{\mbox{\isa{\isacommand{nitpick}}}} configuration options persistently.
1.158
1.159 \end{description}%
1.160 \end{isamarkuptext}%