--- a/doc-src/IsarRef/Thy/HOL_Specific.thy Mon Apr 04 15:51:45 2011 +0200
+++ b/doc-src/IsarRef/Thy/HOL_Specific.thy Mon Apr 04 16:35:46 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 15:51:45 2011 +0200
+++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex Mon Apr 04 16:35:46 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/TutorialI/Rules/Basic.thy Mon Apr 04 15:51:45 2011 +0200
+++ b/doc-src/TutorialI/Rules/Basic.thy Mon Apr 04 16:35:46 2011 +0200
@@ -52,14 +52,14 @@
@{thm[display] ssubst}
\rulename{ssubst}
-*};
+*}
lemma "\<lbrakk> x = f x; P(f x) \<rbrakk> \<Longrightarrow> P x"
by (erule ssubst)
text {*
also provable by simp (re-orients)
-*};
+*}
text {*
the subst method
@@ -69,17 +69,17 @@
this would fail:
apply (simp add: mult_commute)
-*};
+*}
lemma "\<lbrakk>P x y z; Suc x < y\<rbrakk> \<Longrightarrow> f z = x*y"
txt{*
@{subgoals[display,indent=0,margin=65]}
-*};
+*}
apply (subst mult_commute)
txt{*
@{subgoals[display,indent=0,margin=65]}
-*};
+*}
oops
(*exercise involving THEN*)
@@ -143,7 +143,7 @@
@{thm[display] contrapos_nn}
\rulename{contrapos_nn}
-*};
+*}
lemma "\<lbrakk>\<not>(P\<longrightarrow>Q); \<not>(R\<longrightarrow>Q)\<rbrakk> \<Longrightarrow> R"
@@ -156,7 +156,7 @@
text {*
@{thm[display] disjCI}
\rulename{disjCI}
-*};
+*}
lemma "(P \<or> Q) \<and> R \<Longrightarrow> P \<or> Q \<and> R"
apply (intro disjCI conjI)
@@ -226,7 +226,7 @@
@{thm[display] spec}
\rulename{spec}
-*};
+*}
lemma "\<forall>x. P x \<longrightarrow> P x"
apply (rule allI)
@@ -267,7 +267,7 @@
@{thm[display]"exE"}
\rulename{exE}
-*};
+*}
text{*
@@ -285,7 +285,7 @@
text {*
@{thm[display]"dvd_def"}
\rulename{dvd_def}
-*};
+*}
lemma mult_dvd_mono: "\<lbrakk>i dvd m; j dvd n\<rbrakk> \<Longrightarrow> i*j dvd (m*n :: nat)"
apply (simp add: dvd_def)
@@ -344,7 +344,7 @@
txt{*
@{subgoals[display,indent=0,margin=65]}
-*};
+*}
apply (rule the_equality)
@@ -352,7 +352,7 @@
@{subgoals[display,indent=0,margin=65]}
first subgoal is existence; second is uniqueness
-*};
+*}
by (auto intro: order_antisym)
@@ -364,7 +364,7 @@
@{subgoals[display,indent=0,margin=65]}
state after intro rules
-*};
+*}
apply (drule spec, erule exE)
txt{*
@@ -372,18 +372,18 @@
applying @text{someI} automatically instantiates
@{term f} to @{term "\<lambda>x. SOME y. P x y"}
-*};
+*}
by (rule someI)
(*both can be done by blast, which however hasn't been introduced yet*)
-lemma "[| P (k::nat); \<forall>x. P x \<longrightarrow> k \<le> x |] ==> (LEAST x. P(x)) = k";
+lemma "[| P (k::nat); \<forall>x. P x \<longrightarrow> k \<le> x |] ==> (LEAST x. P(x)) = k"
apply (simp add: Least_def LeastM_def)
-by (blast intro: some_equality order_antisym);
+by (blast intro: some_equality order_antisym)
theorem axiom_of_choice': "(\<forall>x. \<exists>y. P x y) \<Longrightarrow> \<exists>f. \<forall>x. P x (f x)"
apply (rule exI [of _ "\<lambda>x. SOME y. P x y"])
-by (blast intro: someI);
+by (blast intro: someI)
text{*end of Epsilon section*}
--- a/doc-src/manual.bib Mon Apr 04 15:51:45 2011 +0200
+++ b/doc-src/manual.bib Mon Apr 04 16:35:46 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",
--- a/src/HOL/Finite_Set.thy Mon Apr 04 15:51:45 2011 +0200
+++ b/src/HOL/Finite_Set.thy Mon Apr 04 16:35:46 2011 +0200
@@ -246,24 +246,20 @@
by (simp add: image_Collect [symmetric])
lemma finite_imageD:
- "finite (f ` A) \<Longrightarrow> inj_on f A \<Longrightarrow> finite A"
-proof -
- have aux: "!!A. finite (A - {}) = finite A" by simp
- fix B :: "'a set"
- assume "finite B"
- thus "!!A. f`A = B ==> inj_on f A ==> finite A"
- apply induct
- apply simp
- apply (subgoal_tac "EX y:A. f y = x & F = f ` (A - {y})")
- apply clarify
- apply (simp (no_asm_use) add: inj_on_def)
- apply (blast dest!: aux [THEN iffD1], atomize)
- apply (erule_tac V = "ALL A. ?PP (A)" in thin_rl)
- apply (frule subsetD [OF equalityD2 insertI1], clarify)
- apply (rule_tac x = xa in bexI)
- apply (simp_all add: inj_on_image_set_diff)
- done
-qed (rule refl)
+ assumes "finite (f ` A)" and "inj_on f A"
+ shows "finite A"
+using assms proof (induct "f ` A" arbitrary: A)
+ case empty then show ?case by simp
+next
+ case (insert x B)
+ then have B_A: "insert x B = f ` A" by simp
+ then obtain y where "x = f y" and "y \<in> A" by blast
+ from B_A `x \<notin> B` have "B = f ` A - {x}" by blast
+ with B_A `x \<notin> B` `x = f y` `inj_on f A` `y \<in> A` have "B = f ` (A - {y})" by (simp add: inj_on_image_set_diff)
+ moreover from `inj_on f A` have "inj_on f (A - {y})" by (rule inj_on_diff)
+ ultimately have "finite (A - {y})" by (rule insert.hyps)
+ then show "finite A" by simp
+qed
lemma finite_surj:
"finite A \<Longrightarrow> B \<subseteq> f ` A \<Longrightarrow> finite B"
@@ -359,34 +355,32 @@
by (simp only: UNIV_Times_UNIV [symmetric] finite_cartesian_product)
lemma finite_cartesian_productD1:
- "finite (A \<times> B) \<Longrightarrow> B \<noteq> {} \<Longrightarrow> finite A"
-apply (auto simp add: finite_conv_nat_seg_image)
-apply (drule_tac x=n in spec)
-apply (drule_tac x="fst o f" in spec)
-apply (auto simp add: o_def)
- prefer 2 apply (force dest!: equalityD2)
-apply (drule equalityD1)
-apply (rename_tac y x)
-apply (subgoal_tac "\<exists>k. k<n & f k = (x,y)")
- prefer 2 apply force
-apply clarify
-apply (rule_tac x=k in image_eqI, auto)
-done
+ assumes "finite (A \<times> B)" and "B \<noteq> {}"
+ shows "finite A"
+proof -
+ from assms obtain n f where "A \<times> B = f ` {i::nat. i < n}"
+ by (auto simp add: finite_conv_nat_seg_image)
+ then have "fst ` (A \<times> B) = fst ` f ` {i::nat. i < n}" by simp
+ with `B \<noteq> {}` have "A = (fst \<circ> f) ` {i::nat. i < n}"
+ by (simp add: image_compose)
+ then have "\<exists>n f. A = f ` {i::nat. i < n}" by blast
+ then show ?thesis
+ by (auto simp add: finite_conv_nat_seg_image)
+qed
lemma finite_cartesian_productD2:
- "[| finite (A <*> B); A \<noteq> {} |] ==> finite B"
-apply (auto simp add: finite_conv_nat_seg_image)
-apply (drule_tac x=n in spec)
-apply (drule_tac x="snd o f" in spec)
-apply (auto simp add: o_def)
- prefer 2 apply (force dest!: equalityD2)
-apply (drule equalityD1)
-apply (rename_tac x y)
-apply (subgoal_tac "\<exists>k. k<n & f k = (x,y)")
- prefer 2 apply force
-apply clarify
-apply (rule_tac x=k in image_eqI, auto)
-done
+ assumes "finite (A \<times> B)" and "A \<noteq> {}"
+ shows "finite B"
+proof -
+ from assms obtain n f where "A \<times> B = f ` {i::nat. i < n}"
+ by (auto simp add: finite_conv_nat_seg_image)
+ then have "snd ` (A \<times> B) = snd ` f ` {i::nat. i < n}" by simp
+ with `A \<noteq> {}` have "B = (snd \<circ> f) ` {i::nat. i < n}"
+ by (simp add: image_compose)
+ then have "\<exists>n f. B = f ` {i::nat. i < n}" by blast
+ then show ?thesis
+ by (auto simp add: finite_conv_nat_seg_image)
+qed
lemma finite_Pow_iff [iff]:
"finite (Pow A) \<longleftrightarrow> finite A"
--- a/src/HOL/Nitpick_Examples/Core_Nits.thy Mon Apr 04 15:51:45 2011 +0200
+++ b/src/HOL/Nitpick_Examples/Core_Nits.thy Mon Apr 04 16:35:46 2011 +0200
@@ -12,7 +12,7 @@
begin
nitpick_params [verbose, card = 1\<midarrow>6, unary_ints, max_potential = 0,
- sat_solver = MiniSat_JNI, max_threads = 1, timeout = 60]
+ sat_solver = MiniSat_JNI, max_threads = 1, timeout = 240]
subsection {* Curry in a Hurry *}
--- a/src/HOL/Nitpick_Examples/Datatype_Nits.thy Mon Apr 04 15:51:45 2011 +0200
+++ b/src/HOL/Nitpick_Examples/Datatype_Nits.thy Mon Apr 04 16:35:46 2011 +0200
@@ -12,7 +12,7 @@
begin
nitpick_params [verbose, card = 1\<midarrow>8, max_potential = 0,
- sat_solver = MiniSat_JNI, max_threads = 1, timeout = 60]
+ sat_solver = MiniSat_JNI, max_threads = 1, timeout = 240]
primrec rot where
"rot Nibble0 = Nibble1" | "rot Nibble1 = Nibble2" | "rot Nibble2 = Nibble3" |
--- a/src/HOL/Nitpick_Examples/Hotel_Nits.thy Mon Apr 04 15:51:45 2011 +0200
+++ b/src/HOL/Nitpick_Examples/Hotel_Nits.thy Mon Apr 04 16:35:46 2011 +0200
@@ -13,7 +13,7 @@
begin
nitpick_params [verbose, max_potential = 0, sat_solver = MiniSat_JNI,
- max_threads = 1, timeout = 120]
+ max_threads = 1, timeout = 240]
typedecl guest
typedecl key
--- a/src/HOL/Nitpick_Examples/Induct_Nits.thy Mon Apr 04 15:51:45 2011 +0200
+++ b/src/HOL/Nitpick_Examples/Induct_Nits.thy Mon Apr 04 16:35:46 2011 +0200
@@ -12,7 +12,7 @@
begin
nitpick_params [verbose, card = 1\<midarrow>8, unary_ints,
- sat_solver = MiniSat_JNI, max_threads = 1, timeout = 60]
+ sat_solver = MiniSat_JNI, max_threads = 1, timeout = 240]
inductive p1 :: "nat \<Rightarrow> bool" where
"p1 0" |
--- a/src/HOL/Nitpick_Examples/Integer_Nits.thy Mon Apr 04 15:51:45 2011 +0200
+++ b/src/HOL/Nitpick_Examples/Integer_Nits.thy Mon Apr 04 16:35:46 2011 +0200
@@ -12,7 +12,7 @@
begin
nitpick_params [verbose, card = 1\<midarrow>5, bits = 1,2,3,4,6,
- sat_solver = MiniSat_JNI, max_threads = 1, timeout = 60]
+ sat_solver = MiniSat_JNI, max_threads = 1, timeout = 240]
lemma "Suc x = x + 1"
nitpick [unary_ints, expect = none]
--- a/src/HOL/Nitpick_Examples/Manual_Nits.thy Mon Apr 04 15:51:45 2011 +0200
+++ b/src/HOL/Nitpick_Examples/Manual_Nits.thy Mon Apr 04 16:35:46 2011 +0200
@@ -18,7 +18,7 @@
chapter {* 3. First Steps *}
nitpick_params [verbose, sat_solver = MiniSat_JNI, max_threads = 1,
- timeout = 60]
+ timeout = 240]
subsection {* 3.1. Propositional Logic *}
--- a/src/HOL/Nitpick_Examples/Pattern_Nits.thy Mon Apr 04 15:51:45 2011 +0200
+++ b/src/HOL/Nitpick_Examples/Pattern_Nits.thy Mon Apr 04 16:35:46 2011 +0200
@@ -12,7 +12,7 @@
begin
nitpick_params [verbose, card = 10, max_potential = 0, sat_solver = MiniSat_JNI,
- max_threads = 1, timeout = 60]
+ max_threads = 1, timeout = 240]
lemma "x = (case u of () \<Rightarrow> y)"
nitpick [expect = genuine]
--- a/src/HOL/Nitpick_Examples/Record_Nits.thy Mon Apr 04 15:51:45 2011 +0200
+++ b/src/HOL/Nitpick_Examples/Record_Nits.thy Mon Apr 04 16:35:46 2011 +0200
@@ -12,7 +12,7 @@
begin
nitpick_params [verbose, card = 1\<midarrow>6, max_potential = 0,
- sat_solver = MiniSat_JNI, max_threads = 1, timeout = 60]
+ sat_solver = MiniSat_JNI, max_threads = 1, timeout = 240]
record point2d =
xc :: int
--- a/src/HOL/Nitpick_Examples/Refute_Nits.thy Mon Apr 04 15:51:45 2011 +0200
+++ b/src/HOL/Nitpick_Examples/Refute_Nits.thy Mon Apr 04 16:35:46 2011 +0200
@@ -12,7 +12,7 @@
begin
nitpick_params [verbose, card = 1\<midarrow>6, max_potential = 0,
- sat_solver = MiniSat_JNI, max_threads = 1, timeout = 60]
+ sat_solver = MiniSat_JNI, max_threads = 1, timeout = 240]
lemma "P \<and> Q"
apply (rule conjI)
--- a/src/HOL/Nitpick_Examples/Special_Nits.thy Mon Apr 04 15:51:45 2011 +0200
+++ b/src/HOL/Nitpick_Examples/Special_Nits.thy Mon Apr 04 16:35:46 2011 +0200
@@ -12,7 +12,7 @@
begin
nitpick_params [verbose, card = 4, sat_solver = MiniSat_JNI, max_threads = 1,
- timeout = 60]
+ timeout = 240]
fun f1 :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat" where
"f1 a b c d e = a + b + c + d + e"
--- a/src/HOL/Nitpick_Examples/Typedef_Nits.thy Mon Apr 04 15:51:45 2011 +0200
+++ b/src/HOL/Nitpick_Examples/Typedef_Nits.thy Mon Apr 04 16:35:46 2011 +0200
@@ -12,7 +12,7 @@
begin
nitpick_params [verbose, card = 1\<midarrow>4, sat_solver = MiniSat_JNI, max_threads = 1,
- timeout = 60]
+ timeout = 240]
typedef three = "{0\<Colon>nat, 1, 2}"
by blast
@@ -159,7 +159,7 @@
by (rule Rep_Nat_inverse)
lemma "0 \<equiv> Abs_Integ (intrel `` {(0, 0)})"
-nitpick [card = 1, unary_ints, max_potential = 0, timeout = 240, expect = none]
+nitpick [card = 1, unary_ints, max_potential = 0, expect = none]
by (rule Zero_int_def_raw)
lemma "Abs_list (Rep_list a) = a"
--- a/src/HOL/Predicate_Compile_Examples/Examples.thy Mon Apr 04 15:51:45 2011 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Examples.thy Mon Apr 04 16:35:46 2011 +0200
@@ -2,7 +2,7 @@
imports Main "~~/src/HOL/Library/Predicate_Compile_Alternative_Defs"
begin
-declare [[values_timeout = 240.0]]
+declare [[values_timeout = 480.0]]
section {* Formal Languages *}
--- a/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy Mon Apr 04 15:51:45 2011 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy Mon Apr 04 16:35:46 2011 +0200
@@ -2,7 +2,7 @@
imports "~~/src/HOL/Library/Predicate_Compile_Alternative_Defs"
begin
-declare [[values_timeout = 240.0]]
+declare [[values_timeout = 480.0]]
subsection {* Basic predicates *}
--- a/src/HOL/Tools/Quickcheck/exhaustive_generators.ML Mon Apr 04 15:51:45 2011 +0200
+++ b/src/HOL/Tools/Quickcheck/exhaustive_generators.ML Mon Apr 04 16:35:46 2011 +0200
@@ -23,10 +23,6 @@
structure Exhaustive_Generators : EXHAUSTIVE_GENERATORS =
struct
-(* static options *)
-
-val define_foundationally = false
-
(* dynamic options *)
val (smart_quantifier, setup_smart_quantifier) =
@@ -71,8 +67,7 @@
let
val (T as Type(@{type_name "option"}, [T'])) = fastype_of x
in
- Const (@{const_name "Quickcheck_Exhaustive.orelse"}, T --> T --> T)
- $ x $ y
+ Const (@{const_name "Quickcheck_Exhaustive.orelse"}, T --> T --> T) $ x $ y
end
(** datatypes **)
@@ -157,11 +152,6 @@
(HOL_basic_ss addsimps [@{thm in_measure}, @{thm o_def}, @{thm snd_conv},
@{thm nat_mono_iff}, less_int_pred] @ @{thms sum.cases}) 1))
-fun pat_completeness_auto ctxt =
- Pat_Completeness.pat_completeness_tac ctxt 1
- THEN auto_tac (clasimpset_of ctxt)
-
-
(* creating the instances *)
fun instantiate_exhaustive_datatype config descr vs tycos prfx (names, auxnames) (Ts, Us) thy =
@@ -171,39 +161,9 @@
in
thy
|> Class.instantiation (tycos, vs, @{sort exhaustive})
- |> (if define_foundationally then
- let
- val exhaustives = map2 (fn name => fn T => Free (name, exhaustiveT T)) exhaustivesN (Ts @ Us)
- val eqs = mk_equations descr vs tycos exhaustives (Ts, Us)
- in
- Function.add_function
- (map (fn (name, T) =>
- Syntax.no_syn (Binding.conceal (Binding.name name), SOME (exhaustiveT T)))
- (exhaustivesN ~~ (Ts @ Us)))
- (map (pair (apfst Binding.conceal Attrib.empty_binding)) eqs)
- Function_Common.default_config pat_completeness_auto
- #> snd
- #> Local_Theory.restore
- #> (fn lthy => Function.prove_termination NONE (termination_tac lthy) lthy)
- #> snd
- end
- else
- fold_map (fn (name, T) => Local_Theory.define
- ((Binding.conceal (Binding.name name), NoSyn),
- (apfst Binding.conceal Attrib.empty_binding, mk_undefined (exhaustiveT T)))
- #> apfst fst) (exhaustivesN ~~ (Ts @ Us))
- #> (fn (exhaustives, lthy) =>
- let
- val eqs_t = mk_equations descr vs tycos exhaustives (Ts, Us)
- val eqs = map (fn eq => Goal.prove lthy ["f", "i"] [] eq
- (fn _ => Skip_Proof.cheat_tac (ProofContext.theory_of lthy))) eqs_t
- in
- fold (fn (name, eq) => Local_Theory.note
- ((Binding.conceal (Binding.qualify true prfx
- (Binding.qualify true name (Binding.name "simps"))),
- Code.add_default_eqn_attrib :: map (Attrib.internal o K)
- [Simplifier.simp_add, Nitpick_Simps.add]), [eq]) #> snd) (exhaustivesN ~~ eqs) lthy
- end))
+ |> Quickcheck_Common.define_functions
+ (fn exhaustives => mk_equations descr vs tycos exhaustives (Ts, Us), SOME termination_tac)
+ prfx ["f", "i"] exhaustivesN (map exhaustiveT (Ts @ Us))
|> Class.prove_instantiation_exit (K (Class.intro_classes_tac []))
end handle FUNCTION_TYPE =>
(Datatype_Aux.message config
--- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML Mon Apr 04 15:51:45 2011 +0200
+++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML Mon Apr 04 16:35:46 2011 +0200
@@ -21,9 +21,6 @@
val (finite_functions, setup_finite_functions) =
Attrib.config_bool "quickcheck_finite_functions" (K true)
-
-fun mk_undefined T = Const(@{const_name undefined}, T)
-
(* narrowing specific names and types *)
exception FUNCTION_TYPE;
@@ -57,12 +54,7 @@
fun mk_equations descr vs tycos narrowings (Ts, Us) =
let
fun mk_call T =
- let
- val narrowing =
- Const (@{const_name "Quickcheck_Narrowing.narrowing_class.narrowing"}, narrowingT T)
- in
- (T, narrowing)
- end
+ (T, Const (@{const_name "Quickcheck_Narrowing.narrowing_class.narrowing"}, narrowingT T))
fun mk_aux_call fTs (k, _) (tyco, Ts) =
let
val T = Type (tyco, Ts)
@@ -86,8 +78,7 @@
in
eqs
end
-
-
+
fun instantiate_narrowing_datatype config descr vs tycos prfx (names, auxnames) (Ts, Us) thy =
let
val _ = Datatype_Aux.message config "Creating narrowing generators ...";
@@ -95,22 +86,9 @@
in
thy
|> Class.instantiation (tycos, vs, @{sort narrowing})
- |> (fold_map (fn (name, T) => Local_Theory.define
- ((Binding.conceal (Binding.name name), NoSyn),
- (apfst Binding.conceal Attrib.empty_binding, mk_undefined (narrowingT T)))
- #> apfst fst) (narrowingsN ~~ (Ts @ Us))
- #> (fn (narrowings, lthy) =>
- let
- val eqs_t = mk_equations descr vs tycos narrowings (Ts, Us)
- val eqs = map (fn eq => Goal.prove lthy ["f", "i"] [] eq
- (fn _ => Skip_Proof.cheat_tac (ProofContext.theory_of lthy))) eqs_t
- in
- fold (fn (name, eq) => Local_Theory.note
- ((Binding.conceal (Binding.qualify true prfx
- (Binding.qualify true name (Binding.name "simps"))),
- Code.add_default_eqn_attrib :: map (Attrib.internal o K)
- [Simplifier.simp_add, Nitpick_Simps.add]), [eq]) #> snd) (narrowingsN ~~ eqs) lthy
- end))
+ |> Quickcheck_Common.define_functions
+ (fn narrowings => mk_equations descr vs tycos narrowings (Ts, Us), NONE)
+ prfx [] narrowingsN (map narrowingT (Ts @ Us))
|> Class.prove_instantiation_exit (K (Class.intro_classes_tac []))
end;
--- a/src/HOL/Tools/Quickcheck/quickcheck_common.ML Mon Apr 04 15:51:45 2011 +0200
+++ b/src/HOL/Tools/Quickcheck/quickcheck_common.ML Mon Apr 04 16:35:46 2011 +0200
@@ -7,6 +7,8 @@
signature QUICKCHECK_COMMON =
sig
val strip_imp : term -> (term list * term)
+ val define_functions : ((term list -> term list) * (Proof.context -> tactic) option)
+ -> string -> string list -> string list -> typ list -> Proof.context -> Proof.context
val perhaps_constrain: theory -> (typ * sort) list -> (string * sort) list
-> (string * sort -> string * sort) option
val ensure_sort_datatype:
@@ -21,11 +23,57 @@
structure Quickcheck_Common : QUICKCHECK_COMMON =
struct
+(* static options *)
+
+val define_foundationally = false
+
(* HOLogic's term functions *)
fun strip_imp (Const(@{const_name HOL.implies},_) $ A $ B) = apfst (cons A) (strip_imp B)
| strip_imp A = ([], A)
+fun mk_undefined T = Const(@{const_name undefined}, T)
+
+(* defining functions *)
+
+fun pat_completeness_auto ctxt =
+ Pat_Completeness.pat_completeness_tac ctxt 1
+ THEN auto_tac (clasimpset_of ctxt)
+
+fun define_functions (mk_equations, termination_tac) prfx argnames names Ts =
+ if define_foundationally andalso is_some termination_tac then
+ let
+ val eqs_t = mk_equations (map2 (fn name => fn T => Free (name, T)) names Ts)
+ in
+ Function.add_function
+ (map (fn (name, T) =>
+ Syntax.no_syn (Binding.conceal (Binding.name name), SOME T))
+ (names ~~ Ts))
+ (map (pair (apfst Binding.conceal Attrib.empty_binding)) eqs_t)
+ Function_Common.default_config pat_completeness_auto
+ #> snd
+ #> Local_Theory.restore
+ #> (fn lthy => Function.prove_termination NONE (the termination_tac lthy) lthy)
+ #> snd
+ end
+ else
+ fold_map (fn (name, T) => Local_Theory.define
+ ((Binding.conceal (Binding.name name), NoSyn),
+ (apfst Binding.conceal Attrib.empty_binding, mk_undefined T))
+ #> apfst fst) (names ~~ Ts)
+ #> (fn (consts, lthy) =>
+ let
+ val eqs_t = mk_equations consts
+ val eqs = map (fn eq => Goal.prove lthy argnames [] eq
+ (fn _ => Skip_Proof.cheat_tac (ProofContext.theory_of lthy))) eqs_t
+ in
+ fold (fn (name, eq) => Local_Theory.note
+ ((Binding.conceal (Binding.qualify true prfx
+ (Binding.qualify true name (Binding.name "simps"))),
+ Code.add_default_eqn_attrib :: map (Attrib.internal o K)
+ [Simplifier.simp_add, Nitpick_Simps.add]), [eq]) #> snd) (names ~~ eqs) lthy
+ end)
+
(** ensuring sort constraints **)
fun perhaps_constrain thy insts raw_vs =
--- a/src/HOL/ex/TPTP.thy Mon Apr 04 15:51:45 2011 +0200
+++ b/src/HOL/ex/TPTP.thy Mon Apr 04 16:35:46 2011 +0200
@@ -16,7 +16,7 @@
refute_params [maxtime = 10000, no_assms, expect = genuine]
nitpick_params [timeout = none, card = 1-50, verbose, dont_box, no_assms,
- expect = genuine]
+ batch_size = 1, expect = genuine]
ML {* Proofterm.proofs := 0 *}
@@ -30,32 +30,34 @@
| ERROR _ => NONE
in
(case result of
- NONE => (writeln ("FAILURE: " ^ name); Seq.empty)
- | SOME st' => (writeln ("SUCCESS: " ^ name); Seq.single st'))
+ NONE => (warning ("FAILURE: " ^ name); Seq.empty)
+ | SOME st' => (warning ("SUCCESS: " ^ name); Seq.single st'))
end
*}
ML {*
-fun isabellep_tac max_secs =
- SOLVE_TIMEOUT (max_secs div 5) "sledgehammer"
- (ALLGOALS (Sledgehammer_Tactics.sledgehammer_as_oracle_tac @{context}))
+fun isabellep_tac ctxt cs ss css max_secs =
+ SOLVE_TIMEOUT (max_secs div 10) "smt" (ALLGOALS (SMT_Solver.smt_tac ctxt []))
ORELSE
- SOLVE_TIMEOUT (max_secs div 10) "simp" (ALLGOALS (asm_full_simp_tac @{simpset}))
+ SOLVE_TIMEOUT (max_secs div 5) "sledgehammer"
+ (ALLGOALS (Sledgehammer_Tactics.sledgehammer_as_oracle_tac ctxt))
ORELSE
- SOLVE_TIMEOUT (max_secs div 20) "blast" (ALLGOALS (blast_tac @{claset}))
+ SOLVE_TIMEOUT (max_secs div 10) "simp" (ALLGOALS (asm_full_simp_tac ss))
+ ORELSE
+ SOLVE_TIMEOUT (max_secs div 20) "blast" (ALLGOALS (blast_tac cs))
ORELSE
- SOLVE_TIMEOUT (max_secs div 10) "auto" (auto_tac @{clasimpset}
- THEN ALLGOALS (Sledgehammer_Tactics.sledgehammer_as_oracle_tac @{context}))
+ SOLVE_TIMEOUT (max_secs div 10) "auto" (auto_tac css
+ THEN ALLGOALS (Sledgehammer_Tactics.sledgehammer_as_oracle_tac ctxt))
ORELSE
- SOLVE_TIMEOUT (max_secs div 10) "metis" (ALLGOALS (Metis_Tactics.metis_tac @{context} []))
+ SOLVE_TIMEOUT (max_secs div 10) "metis" (ALLGOALS (Metis_Tactics.metis_tac ctxt []))
ORELSE
- SOLVE_TIMEOUT (max_secs div 5) "fast" (ALLGOALS (fast_tac @{claset}))
+ SOLVE_TIMEOUT (max_secs div 10) "fast" (ALLGOALS (fast_tac cs))
ORELSE
- SOLVE_TIMEOUT (max_secs div 10) "best" (ALLGOALS (best_tac @{claset}))
+ SOLVE_TIMEOUT (max_secs div 10) "best" (ALLGOALS (best_tac cs))
ORELSE
- SOLVE_TIMEOUT (max_secs div 10) "force" (ALLGOALS (force_tac @{clasimpset}))
+ SOLVE_TIMEOUT (max_secs div 10) "force" (ALLGOALS (force_tac css))
ORELSE
- SOLVE_TIMEOUT max_secs "fastsimp" (ALLGOALS (fast_simp_tac @{clasimpset}))
+ SOLVE_TIMEOUT max_secs "fastsimp" (ALLGOALS (fast_simp_tac css))
*}
end