770 The @{attribute (HOL) arith_split} attribute declares case split |
770 The @{attribute (HOL) arith_split} attribute declares case split |
771 rules to be expanded before the arithmetic procedure is invoked. |
771 rules to be expanded before the arithmetic procedure is invoked. |
772 |
772 |
773 Note that a simpler (but faster) version of arithmetic reasoning is |
773 Note that a simpler (but faster) version of arithmetic reasoning is |
774 already performed by the Simplifier. |
774 already performed by the Simplifier. |
|
775 *} |
|
776 |
|
777 |
|
778 section {* Invoking automated reasoning tools -- The Sledgehammer *} |
|
779 |
|
780 text {* |
|
781 Isabelle/HOL includes a generic \emph{ATP manager} that allows |
|
782 external automated reasoning tools to crunch a pending goal. |
|
783 Supported provers include E\footnote{\url{http://www.eprover.org}}, |
|
784 SPASS\footnote{\url{http://www.spass-prover.org/}}, and Vampire. |
|
785 There is also a wrapper to invoke provers remotely via the |
|
786 SystemOnTPTP\footnote{\url{http://www.cs.miami.edu/~tptp/cgi-bin/SystemOnTPTP}} |
|
787 web service. |
|
788 |
|
789 The problem passed to external provers consists of the goal together |
|
790 with a smart selection of lemmas from the current theory context. |
|
791 The result of a successful proof search is some source text that |
|
792 usually reconstructs the proof within Isabelle, without requiring |
|
793 external provers again. The Metis |
|
794 prover\footnote{\url{http://www.gilith.com/software/metis/}} that is |
|
795 integrated into Isabelle/HOL is being used here. |
|
796 |
|
797 In this mode of operation, heavy means of automated reasoning are |
|
798 used as a strong relevance filter, while the main proof checking |
|
799 works via explicit inferences going through the Isabelle kernel. |
|
800 Moreover, rechecking Isabelle proof texts with already specified |
|
801 auxiliary facts is much faster than performing fully automated |
|
802 search over and over again. |
|
803 |
|
804 \begin{matharray}{rcl} |
|
805 @{command_def (HOL) "sledgehammer"}@{text "\<^sup>*"} & : & \isarkeep{proof} \\ |
|
806 @{command_def (HOL) "print_atps"}@{text "\<^sup>*"} & : & \isarkeep{theory~|~proof} \\ |
|
807 @{command_def (HOL) "atp_info"}@{text "\<^sup>*"} & : & \isarkeep{\cdot} \\ |
|
808 @{command_def (HOL) "atp_kill"}@{text "\<^sup>*"} & : & \isarkeep{\cdot} \\ |
|
809 @{method_def (HOL) metis} & : & \isarmeth \\ |
|
810 \end{matharray} |
|
811 |
|
812 \begin{rail} |
|
813 'sledgehammer' (nameref *) |
|
814 ; |
|
815 |
|
816 'metis' thmrefs |
|
817 ; |
|
818 \end{rail} |
|
819 |
|
820 \begin{descr} |
|
821 |
|
822 \item [@{command (HOL) sledgehammer}~@{text "prover\<^sub>1 \<dots> |
|
823 prover\<^sub>n"}] invokes the specified automated theorem provers on |
|
824 the first subgoal. Provers are run in parallel, the first |
|
825 successful result is displayed, and the other attempts are |
|
826 terminated. |
|
827 |
|
828 Provers are defined in the theory context, see also @{command (HOL) |
|
829 print_atps}. If no provers are given as arguments to @{command |
|
830 (HOL) sledgehammer}, the system refers to the default defined as |
|
831 ``ATP provers'' preference by the user interface. |
|
832 |
|
833 There are additional preferences for timeout (default: 60 seconds), |
|
834 and the maximum number of independent prover processes (default: 5); |
|
835 excessive provers are automatically terminated. |
|
836 |
|
837 \item [@{command (HOL) print_atps}] prints the list of automated |
|
838 theorem provers available to the @{command (HOL) sledgehammer} |
|
839 command. |
|
840 |
|
841 \item [@{command (HOL) atp_info}] prints information about presently |
|
842 running provers, including elapsed runtime, and the remaining time |
|
843 until timeout. |
|
844 |
|
845 \item [@{command (HOL) atp_kill}] terminates all presently running |
|
846 provers. |
|
847 |
|
848 \item [@{method (HOL) metis}~@{text "facts"}] invokes the Metis |
|
849 prover with the given facts. Metis is an automated proof tool of |
|
850 medium strength, but is fully integrated into Isabelle/HOL, with |
|
851 explicit inferences going through the kernel. Thus its results are |
|
852 guaranteed to be ``correct by construction''. |
|
853 |
|
854 Note that all facts used with Metis need to be specified as explicit |
|
855 arguments. There are no rule declarations as for other Isabelle |
|
856 provers, like @{method blast} or @{method fast}. |
|
857 |
|
858 \end{descr} |
775 *} |
859 *} |
776 |
860 |
777 |
861 |
778 section {* Unstructured cases analysis and induction \label{sec:hol-induct-tac} *} |
862 section {* Unstructured cases analysis and induction \label{sec:hol-induct-tac} *} |
779 |
863 |