--- 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 "\<infinity>"}.
- \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 "\<infinity>"}.
\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}
*}
--- 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}%