--- a/doc-src/IsarRef/Thy/HOL_Specific.thy Wed Dec 21 09:41:16 2011 +0100
+++ b/doc-src/IsarRef/Thy/HOL_Specific.thy Wed Dec 21 14:24:29 2011 +0100
@@ -1522,7 +1522,8 @@
@{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"}
+ @{command_def (HOL) "nitpick_params"} & : & @{text "theory \<rightarrow> theory"} \\
+ @{command_def (HOL) "quickcheck_generator"} & : & @{text "theory \<rightarrow> theory"}
\end{matharray}
@{rail "
@@ -1539,6 +1540,9 @@
(@@{command (HOL) quickcheck_params} | @@{command (HOL) refute_params} |
@@{command (HOL) nitpick_params}) ( '[' args ']' )?
;
+ @@{command (HOL) quickcheck_generator} typeconstructor \\
+ 'operations:' ( @{syntax term} +)
+ ;
modes: '(' (@{syntax name} +) ')'
;
@@ -1630,6 +1634,11 @@
\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.
+
\item @{command (HOL) "refute"} tests the current goal for
counterexamples using a reduction to SAT. The following configuration
options are supported:
--- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex Wed Dec 21 09:41:16 2011 +0100
+++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex Wed Dec 21 14:24:29 2011 +0100
@@ -2217,7 +2217,8 @@
\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}}}
+ \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}}} \\
+ \indexdef{HOL}{command}{quickcheck\_generator}\hypertarget{command.HOL.quickcheck-generator}{\hyperlink{command.HOL.quickcheck-generator}{\mbox{\isa{\isacommand{quickcheck{\isaliteral{5F}{\isacharunderscore}}generator}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{22}{\isachardoublequote}}}
\end{matharray}
\begin{railoutput}
@@ -2281,6 +2282,16 @@
\rail@term{\isa{{\isaliteral{5D}{\isacharbrackright}}}}[]
\rail@endbar
\rail@end
+\rail@begin{4}{}
+\rail@term{\hyperlink{command.HOL.quickcheck-generator}{\mbox{\isa{\isacommand{quickcheck{\isaliteral{5F}{\isacharunderscore}}generator}}}}}[]
+\rail@nont{\isa{typeconstructor}}[]
+\rail@cr{2}
+\rail@term{\isa{operations{\isaliteral{3A}{\isacharcolon}}}}[]
+\rail@plus
+\rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[]
+\rail@nextplus{3}
+\rail@endplus
+\rail@end
\rail@begin{2}{\isa{modes}}
\rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[]
\rail@plus
@@ -2383,6 +2394,11 @@
\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.
+
\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: