# HG changeset patch # User wenzelm # Date 1328210804 -3600 # Node ID d90a650a5fb90e76ab90aee018fd737f67c3c7e7 # Parent 83864b045a723494e9052e9bd2dc40c660a1795d misc tuning and reformatting; more antiquotations; diff -r 83864b045a72 -r d90a650a5fb9 doc-src/IsarRef/Thy/HOL_Specific.thy --- a/doc-src/IsarRef/Thy/HOL_Specific.thy Thu Feb 02 18:11:42 2012 +0100 +++ b/doc-src/IsarRef/Thy/HOL_Specific.thy Thu Feb 02 20:26:44 2012 +0100 @@ -546,10 +546,10 @@ accepted (as for @{method auto}). \item @{method (HOL) induction_schema} derives user-specified - induction rules from well-founded induction and completeness of - patterns. This factors out some operations that are done internally - by the function package and makes them available separately. See - @{file "~~/src/HOL/ex/Induction_Schema.thy"} for examples. + induction rules from well-founded induction and completeness of + patterns. This factors out some operations that are done internally + by the function package and makes them available separately. See + @{file "~~/src/HOL/ex/Induction_Schema.thy"} for examples. \end{description} *} @@ -595,12 +595,13 @@ defined: \begin{description} + \item @{text option} defines functions that map into the @{type option} type. Here, the value @{term None} is used to model a non-terminating computation. Monotonicity requires that if @{term - None} is returned by a recursive call, then the overall result - must also be @{term None}. This is best achieved through the use of - the monadic operator @{const "Option.bind"}. + None} is returned by a recursive call, then the overall result must + also be @{term None}. This is best achieved through the use of the + monadic operator @{const "Option.bind"}. \item @{text tailrec} defines functions with an arbitrary result type and uses the slightly degenerated partial order where @{term @@ -610,6 +611,7 @@ only satisfied when each recursive call is a tail call, whose result is directly returned. Thus, this mode of operation allows the definition of arbitrary tail-recursive functions. + \end{description} Experienced users may define new modes by instantiating the locale @@ -1509,27 +1511,29 @@ \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) "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_methods"} 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) "try_methods"} attempts to prove a subgoal + using a combination of standard proof methods (@{method auto}, + @{method simp}, @{method 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) "try"} attempts to prove or disprove a subgoal - using a combination of provers and disprovers (@{text "solve_direct"}, - @{text "quickcheck"}, @{text "try_methods"}, @{text "sledgehammer"}, - @{text "nitpick"}). + using a combination of provers and disprovers (@{command (HOL) + "solve_direct"}, @{command (HOL) "quickcheck"}, @{command (HOL) + "try_methods"}, @{command (HOL) "sledgehammer"}, @{command (HOL) + "nitpick"}). - \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"} 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. + \item @{command (HOL) "sledgehammer_params"} changes @{command (HOL) + "sledgehammer"} configuration options persistently. \end{description} *} @@ -1582,54 +1586,54 @@ \begin{description} \item @{command (HOL) "value"}~@{text t} evaluates and prints a - term; optionally @{text modes} can be specified, which are - appended to the current print mode; see \secref{sec:print-modes}. - Internally, the evaluation is performed by registered evaluators, - which are invoked sequentially until a result is returned. - Alternatively a specific evaluator can be selected using square - brackets; typical evaluators use the current set of code equations - to normalize and include @{text simp} for fully symbolic - evaluation using the simplifier, @{text nbe} for - \emph{normalization by evaluation} and \emph{code} for code - generation in SML. + term; optionally @{text modes} can be specified, which are appended + to the current print mode; see \secref{sec:print-modes}. + Internally, the evaluation is performed by registered evaluators, + which are invoked sequentially until a result is returned. + Alternatively a specific evaluator can be selected using square + brackets; typical evaluators use the current set of code equations + to normalize and include @{text simp} for fully symbolic evaluation + using the simplifier, @{text nbe} for \emph{normalization by + evaluation} and \emph{code} for code generation in SML. - \item @{command (HOL) "values"}~@{text t} enumerates a set comprehension - by evaluation and prints its values up to the given number of solutions; - optionally @{text modes} can be specified, which are - appended to the current print mode; see \secref{sec:print-modes}. + \item @{command (HOL) "values"}~@{text t} enumerates a set + comprehension by evaluation and prints its values up to the given + number of solutions; optionally @{text modes} can be specified, + which are appended to the current print mode; see + \secref{sec:print-modes}. \item @{command (HOL) "quickcheck"} tests the current goal for - 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 - size, or using a fixed number of random assignments in the search space, - or exploring the search space symbolically using narrowing. - By default, quickcheck uses exhaustive testing. - A number of configuration options are supported for - @{command (HOL) "quickcheck"}, notably: + 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 size, or using a + fixed number of random assignments in the search space, or exploring + the search space symbolically using narrowing. By default, + quickcheck uses exhaustive testing. A number of configuration + options are supported for @{command (HOL) "quickcheck"}, notably: \begin{description} \item[@{text tester}] specifies which testing approach to apply. - There are three testers, @{text exhaustive}, - @{text random}, and @{text narrowing}. - An unknown configuration option is treated as an argument to tester, - making @{text "tester ="} optional. - When multiple testers are given, these are applied in parallel. - If no tester is specified, quickcheck uses the testers that are - set active, i.e., configurations - @{text quickcheck_exhaustive_active}, @{text quickcheck_random_active}, - @{text quickcheck_narrowing_active} are set to true. + There are three testers, @{text exhaustive}, @{text random}, and + @{text narrowing}. An unknown configuration option is treated as + an argument to tester, making @{text "tester ="} optional. When + multiple testers are given, these are applied in parallel. If no + tester is specified, quickcheck uses the testers that are set + active, i.e., configurations @{attribute + quickcheck_exhaustive_active}, @{attribute + quickcheck_random_active}, @{attribute + quickcheck_narrowing_active} are set to true. + \item[@{text size}] specifies the maximum size of the search space for assignment values. \item[@{text genuine_only}] sets quickcheck only to return genuine - counterexample, but not potentially spurious counterexamples due - to underspecified functions. + counterexample, but not potentially spurious counterexamples due + to underspecified functions. \item[@{text eval}] takes a term or a list of terms and evaluates - these terms under the variable assignment found by quickcheck. + these terms under the variable assignment found by quickcheck. \item[@{text iterations}] sets how many sets of assignments are generated for each particular size. @@ -1648,8 +1652,8 @@ \item[@{text quiet}] if set quickcheck does not output anything while testing. - \item[@{text verbose}] if set quickcheck informs about the - current size and cardinality while testing. + \item[@{text verbose}] if set quickcheck informs about the current + size and cardinality while testing. \item[@{text expect}] can be used to check if the user's expectation was met (@{text no_expectation}, @{text @@ -1657,31 +1661,31 @@ \end{description} - These option can be given within square brackets. + These option can be given within square brackets. - \item @{command (HOL) "quickcheck_params"} changes - @{command (HOL) "quickcheck"} configuration options persistently. + \item @{command (HOL) "quickcheck_params"} changes @{command (HOL) + "quickcheck"} configuration options persistently. \item @{command (HOL) "quickcheck_generator"} creates random and - exhaustive value generators for a given type and operations. - It generates values by using the operations as if they were - constructors of that type. + exhaustive value generators for a given type and operations. It + generates values by using the operations as if they were + constructors of that type. \item @{command (HOL) "refute"} tests the current goal for - counterexamples using a reduction to SAT. The following configuration - options are supported: + 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 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 maxsize}] specifies the maximum size (cardinality) of + the models to search for. Nonpositive values mean @{text "\"}. - \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 maxvars}] specifies the maximum number of Boolean + variables to use when transforming the term into a propositional + formula. Nonpositive values mean @{text "\"}. \item[@{text satsolver}] specifies the SAT solver to use. @@ -1691,22 +1695,22 @@ \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}). + expectation was met (@{text genuine}, @{text potential}, @{text + none}, or @{text unknown}). \end{description} - These option can be given within square brackets. + These option can be given within square brackets. - \item @{command (HOL) "refute_params"} changes - @{command (HOL) "refute"} configuration options persistently. + \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"} 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. + \item @{command (HOL) "nitpick_params"} changes @{command (HOL) + "nitpick"} configuration options persistently. \end{description} *} diff -r 83864b045a72 -r d90a650a5fb9 doc-src/IsarRef/Thy/document/HOL_Specific.tex --- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex Thu Feb 02 18:11:42 2012 +0100 +++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex Thu Feb 02 20:26:44 2012 +0100 @@ -784,10 +784,10 @@ accepted (as for \hyperlink{method.auto}{\mbox{\isa{auto}}}). \item \hyperlink{method.HOL.induction-schema}{\mbox{\isa{induction{\isaliteral{5F}{\isacharunderscore}}schema}}} derives user-specified - induction rules from well-founded induction and completeness of - patterns. This factors out some operations that are done internally - by the function package and makes them available separately. See - \verb|~~/src/HOL/ex/Induction_Schema.thy| for examples. + induction rules from well-founded induction and completeness of + patterns. This factors out some operations that are done internally + by the function package and makes them available separately. See + \verb|~~/src/HOL/ex/Induction_Schema.thy| for examples. \end{description}% \end{isamarkuptext}% @@ -851,10 +851,11 @@ defined: \begin{description} + \item \isa{option} defines functions that map into the \isa{option} type. Here, the value \isa{None} is used to model a - non-terminating computation. Monotonicity requires that if \isa{None} is returned by a recursive call, then the overall result - must also be \isa{None}. This is best achieved through the use of - the monadic operator \isa{{\isaliteral{22}{\isachardoublequote}}Option{\isaliteral{2E}{\isachardot}}bind{\isaliteral{22}{\isachardoublequote}}}. + non-terminating computation. Monotonicity requires that if \isa{None} is returned by a recursive call, then the overall result must + also be \isa{None}. This is best achieved through the use of the + monadic operator \isa{{\isaliteral{22}{\isachardoublequote}}Option{\isaliteral{2E}{\isachardot}}bind{\isaliteral{22}{\isachardoublequote}}}. \item \isa{tailrec} defines functions with an arbitrary result type and uses the slightly degenerated partial order where \isa{{\isaliteral{22}{\isachardoublequote}}undefined{\isaliteral{22}{\isachardoublequote}}} is the bottom element. Now, monotonicity requires that @@ -863,6 +864,7 @@ only satisfied when each recursive call is a tail call, whose result is directly returned. Thus, this mode of operation allows the definition of arbitrary tail-recursive functions. + \end{description} Experienced users may define new modes by instantiating the locale @@ -2199,27 +2201,24 @@ \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.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-methods}{\mbox{\isa{\isacommand{try{\isaliteral{5F}{\isacharunderscore}}methods}}}} 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.try-methods}{\mbox{\isa{\isacommand{try{\isaliteral{5F}{\isacharunderscore}}methods}}}} attempts to prove a subgoal + using a combination of standard proof methods (\hyperlink{method.auto}{\mbox{\isa{auto}}}, + \hyperlink{method.simp}{\mbox{\isa{simp}}}, \hyperlink{method.blast}{\mbox{\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.try}{\mbox{\isa{\isacommand{try}}}} attempts to prove or disprove a subgoal - using a combination of provers and disprovers (\isa{{\isaliteral{22}{\isachardoublequote}}solve{\isaliteral{5F}{\isacharunderscore}}direct{\isaliteral{22}{\isachardoublequote}}}, - \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}}}, - \isa{{\isaliteral{22}{\isachardoublequote}}nitpick{\isaliteral{22}{\isachardoublequote}}}). + using a combination of provers and disprovers (\hyperlink{command.HOL.solve-direct}{\mbox{\isa{\isacommand{solve{\isaliteral{5F}{\isacharunderscore}}direct}}}}, \hyperlink{command.HOL.quickcheck}{\mbox{\isa{\isacommand{quickcheck}}}}, \hyperlink{command.HOL.try-methods}{\mbox{\isa{\isacommand{try{\isaliteral{5F}{\isacharunderscore}}methods}}}}, \hyperlink{command.HOL.sledgehammer}{\mbox{\isa{\isacommand{sledgehammer}}}}, \hyperlink{command.HOL.nitpick}{\mbox{\isa{\isacommand{nitpick}}}}). - \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}{\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. + \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}% @@ -2340,54 +2339,51 @@ \begin{description} \item \hyperlink{command.HOL.value}{\mbox{\isa{\isacommand{value}}}}~\isa{t} evaluates and prints a - term; optionally \isa{modes} can be specified, which are - appended to the current print mode; see \secref{sec:print-modes}. - Internally, the evaluation is performed by registered evaluators, - which are invoked sequentially until a result is returned. - Alternatively a specific evaluator can be selected using square - brackets; typical evaluators use the current set of code equations - to normalize and include \isa{simp} for fully symbolic - evaluation using the simplifier, \isa{nbe} for - \emph{normalization by evaluation} and \emph{code} for code - generation in SML. + term; optionally \isa{modes} can be specified, which are appended + to the current print mode; see \secref{sec:print-modes}. + Internally, the evaluation is performed by registered evaluators, + which are invoked sequentially until a result is returned. + Alternatively a specific evaluator can be selected using square + brackets; typical evaluators use the current set of code equations + to normalize and include \isa{simp} for fully symbolic evaluation + using the simplifier, \isa{nbe} for \emph{normalization by + evaluation} and \emph{code} for code generation in SML. - \item \hyperlink{command.HOL.values}{\mbox{\isa{\isacommand{values}}}}~\isa{t} enumerates a set comprehension - by evaluation and prints its values up to the given number of solutions; - optionally \isa{modes} can be specified, which are - appended to the current print mode; see \secref{sec:print-modes}. + \item \hyperlink{command.HOL.values}{\mbox{\isa{\isacommand{values}}}}~\isa{t} enumerates a set + comprehension by evaluation and prints its values up to the given + number of solutions; optionally \isa{modes} can be specified, + which are appended to the current print mode; see + \secref{sec:print-modes}. \item \hyperlink{command.HOL.quickcheck}{\mbox{\isa{\isacommand{quickcheck}}}} tests the current goal for - 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 - size, or using a fixed number of random assignments in the search space, - or exploring the search space symbolically using narrowing. - By default, quickcheck uses exhaustive testing. - A number of configuration options are supported for - \hyperlink{command.HOL.quickcheck}{\mbox{\isa{\isacommand{quickcheck}}}}, notably: + 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 size, or using a + fixed number of random assignments in the search space, or exploring + the search space symbolically using narrowing. By default, + quickcheck uses exhaustive testing. A number of configuration + options are supported for \hyperlink{command.HOL.quickcheck}{\mbox{\isa{\isacommand{quickcheck}}}}, notably: \begin{description} \item[\isa{tester}] specifies which testing approach to apply. - There are three testers, \isa{exhaustive}, - \isa{random}, and \isa{narrowing}. - An unknown configuration option is treated as an argument to tester, - making \isa{{\isaliteral{22}{\isachardoublequote}}tester\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{22}{\isachardoublequote}}} optional. - When multiple testers are given, these are applied in parallel. - If no tester is specified, quickcheck uses the testers that are - set active, i.e., configurations - \isa{quickcheck{\isaliteral{5F}{\isacharunderscore}}exhaustive{\isaliteral{5F}{\isacharunderscore}}active}, \isa{quickcheck{\isaliteral{5F}{\isacharunderscore}}random{\isaliteral{5F}{\isacharunderscore}}active}, - \isa{quickcheck{\isaliteral{5F}{\isacharunderscore}}narrowing{\isaliteral{5F}{\isacharunderscore}}active} are set to true. + There are three testers, \isa{exhaustive}, \isa{random}, and + \isa{narrowing}. An unknown configuration option is treated as + an argument to tester, making \isa{{\isaliteral{22}{\isachardoublequote}}tester\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{22}{\isachardoublequote}}} optional. When + multiple testers are given, these are applied in parallel. If no + tester is specified, quickcheck uses the testers that are set + active, i.e., configurations \hyperlink{attribute.quickcheck-exhaustive-active}{\mbox{\isa{quickcheck{\isaliteral{5F}{\isacharunderscore}}exhaustive{\isaliteral{5F}{\isacharunderscore}}active}}}, \hyperlink{attribute.quickcheck-random-active}{\mbox{\isa{quickcheck{\isaliteral{5F}{\isacharunderscore}}random{\isaliteral{5F}{\isacharunderscore}}active}}}, \hyperlink{attribute.quickcheck-narrowing-active}{\mbox{\isa{quickcheck{\isaliteral{5F}{\isacharunderscore}}narrowing{\isaliteral{5F}{\isacharunderscore}}active}}} are set to true. + \item[\isa{size}] specifies the maximum size of the search space for assignment values. \item[\isa{genuine{\isaliteral{5F}{\isacharunderscore}}only}] sets quickcheck only to return genuine - counterexample, but not potentially spurious counterexamples due - to underspecified functions. + counterexample, but not potentially spurious counterexamples due + to underspecified functions. \item[\isa{eval}] takes a term or a list of terms and evaluates - these terms under the variable assignment found by quickcheck. + these terms under the variable assignment found by quickcheck. \item[\isa{iterations}] sets how many sets of assignments are generated for each particular size. @@ -2406,39 +2402,38 @@ \item[\isa{quiet}] if set quickcheck does not output anything while testing. - \item[\isa{verbose}] if set quickcheck informs about the - current size and cardinality while testing. + \item[\isa{verbose}] if set quickcheck informs about the current + size and cardinality while testing. \item[\isa{expect}] can be used to check if the user's expectation was met (\isa{no{\isaliteral{5F}{\isacharunderscore}}expectation}, \isa{no{\isaliteral{5F}{\isacharunderscore}}counterexample}, or \isa{counterexample}). \end{description} - These option can be given within square brackets. + These option can be given within square brackets. - \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.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.quickcheck-generator}{\mbox{\isa{\isacommand{quickcheck{\isaliteral{5F}{\isacharunderscore}}generator}}}} creates random and - exhaustive value generators for a given type and operations. - It generates values by using the operations as if they were - constructors of that type. + exhaustive value generators for a given type and operations. It + generates values by using the operations as if they were + constructors of that type. \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: + 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{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{maxsize}] specifies the maximum size (cardinality) of + the models to search for. Nonpositive values mean \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C696E66696E6974793E}{\isasyminfinity}}{\isaliteral{22}{\isachardoublequote}}}. - \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{maxvars}] specifies the maximum number of Boolean + variables to use when transforming the term into a propositional + formula. Nonpositive values mean \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C696E66696E6974793E}{\isasyminfinity}}{\isaliteral{22}{\isachardoublequote}}}. \item[\isa{satsolver}] specifies the SAT solver to use. @@ -2448,22 +2443,19 @@ \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}). + expectation was met (\isa{genuine}, \isa{potential}, \isa{none}, or \isa{unknown}). \end{description} - These option can be given within square brackets. + 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.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}{\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. + \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}%