2011 of standard proof methods (\isa{auto}, \isa{simp}, \isa{blast}, etc.). |
2011 of standard proof methods (\isa{auto}, \isa{simp}, \isa{blast}, etc.). |
2012 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}}}, |
2012 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}}}, |
2013 \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 |
2013 \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 |
2014 methods. |
2014 methods. |
2015 |
2015 |
|
2016 \item \hyperlink{command.HOL.try}{\mbox{\isa{\isacommand{try}}}} attempts to prove or disprove a subgoal |
|
2017 using a combination of provers and disprovers (\isa{{\isaliteral{22}{\isachardoublequote}}solve{\isaliteral{5F}{\isacharunderscore}}direct{\isaliteral{22}{\isachardoublequote}}}, |
|
2018 \isa{{\isaliteral{22}{\isachardoublequote}}quickcheck{\isaliteral{22}{\isachardoublequote}}}, \isa{{\isaliteral{22}{\isachardoublequote}}try{\isaliteral{5F}{\isacharunderscore}}methods{\isaliteral{22}{\isachardoublequote}}}, \isa{{\isaliteral{22}{\isachardoublequote}}sledgehammer{\isaliteral{22}{\isachardoublequote}}}, |
|
2019 \isa{{\isaliteral{22}{\isachardoublequote}}nitpick{\isaliteral{22}{\isachardoublequote}}}). |
|
2020 |
2016 \item \hyperlink{command.HOL.sledgehammer}{\mbox{\isa{\isacommand{sledgehammer}}}} attempts to prove a subgoal using external |
2021 \item \hyperlink{command.HOL.sledgehammer}{\mbox{\isa{\isacommand{sledgehammer}}}} attempts to prove a subgoal using external |
2017 automatic provers (resolution provers and SMT solvers). See the Sledgehammer |
2022 automatic provers (resolution provers and SMT solvers). See the Sledgehammer |
2018 manual \cite{isabelle-sledgehammer} for details. |
2023 manual \cite{isabelle-sledgehammer} for details. |
2019 |
2024 |
2020 \item \hyperlink{command.HOL.sledgehammer-params}{\mbox{\isa{\isacommand{sledgehammer{\isaliteral{5F}{\isacharunderscore}}params}}}} changes |
2025 \item \hyperlink{command.HOL.sledgehammer-params}{\mbox{\isa{\isacommand{sledgehammer{\isaliteral{5F}{\isacharunderscore}}params}}}} changes |
2129 \item \hyperlink{command.HOL.quickcheck}{\mbox{\isa{\isacommand{quickcheck}}}} tests the current goal for |
2134 \item \hyperlink{command.HOL.quickcheck}{\mbox{\isa{\isacommand{quickcheck}}}} tests the current goal for |
2130 counterexamples using a series of assignments for its |
2135 counterexamples using a series of assignments for its |
2131 free variables; by default the first subgoal is tested, an other |
2136 free variables; by default the first subgoal is tested, an other |
2132 can be selected explicitly using an optional goal index. |
2137 can be selected explicitly using an optional goal index. |
2133 Assignments can be chosen exhausting the search space upto a given |
2138 Assignments can be chosen exhausting the search space upto a given |
2134 size or using a fixed number of random assignments in the search space. |
2139 size, or using a fixed number of random assignments in the search space, |
|
2140 or exploring the search space symbolically using narrowing. |
2135 By default, quickcheck uses exhaustive testing. |
2141 By default, quickcheck uses exhaustive testing. |
2136 A number of configuration options are supported for |
2142 A number of configuration options are supported for |
2137 \hyperlink{command.HOL.quickcheck}{\mbox{\isa{\isacommand{quickcheck}}}}, notably: |
2143 \hyperlink{command.HOL.quickcheck}{\mbox{\isa{\isacommand{quickcheck}}}}, notably: |
2138 |
2144 |
2139 \begin{description} |
2145 \begin{description} |
2140 |
2146 |
2141 \item[\isa{tester}] specifies how to explore the search space |
2147 \item[\isa{tester}] specifies which testing approach to apply. |
2142 (e.g. exhaustive or random). |
2148 There are three testers, \isa{exhaustive}, |
|
2149 \isa{random}, and \isa{narrowing}. |
2143 An unknown configuration option is treated as an argument to tester, |
2150 An unknown configuration option is treated as an argument to tester, |
2144 making \isa{{\isaliteral{22}{\isachardoublequote}}tester\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{22}{\isachardoublequote}}} optional. |
2151 making \isa{{\isaliteral{22}{\isachardoublequote}}tester\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{22}{\isachardoublequote}}} optional. |
|
2152 When multiple testers are given, these are applied in parallel. |
|
2153 If no tester is specified, quickcheck uses the testers that are |
|
2154 set active, i.e., configurations |
|
2155 \isa{quickcheck{\isaliteral{5F}{\isacharunderscore}}exhaustive{\isaliteral{5F}{\isacharunderscore}}active}, \isa{quickcheck{\isaliteral{5F}{\isacharunderscore}}random{\isaliteral{5F}{\isacharunderscore}}active}, |
|
2156 \isa{quickcheck{\isaliteral{5F}{\isacharunderscore}}narrowing{\isaliteral{5F}{\isacharunderscore}}active} are set to true. |
2145 \item[\isa{size}] specifies the maximum size of the search space |
2157 \item[\isa{size}] specifies the maximum size of the search space |
2146 for assignment values. |
2158 for assignment values. |
2147 |
2159 |
2148 \item[\isa{eval}] takes a term or a list of terms and evaluates |
2160 \item[\isa{eval}] takes a term or a list of terms and evaluates |
2149 these terms under the variable assignment found by quickcheck. |
2161 these terms under the variable assignment found by quickcheck. |