1.1 --- a/doc-src/IsarRef/Thy/HOL_Specific.thy Wed Dec 21 09:41:16 2011 +0100
1.2 +++ b/doc-src/IsarRef/Thy/HOL_Specific.thy Wed Dec 21 14:24:29 2011 +0100
1.3 @@ -1522,7 +1522,8 @@
1.4 @{command_def (HOL) "nitpick"}@{text "\<^sup>*"} & : & @{text "proof \<rightarrow>"} \\
1.5 @{command_def (HOL) "quickcheck_params"} & : & @{text "theory \<rightarrow> theory"} \\
1.6 @{command_def (HOL) "refute_params"} & : & @{text "theory \<rightarrow> theory"} \\
1.7 - @{command_def (HOL) "nitpick_params"} & : & @{text "theory \<rightarrow> theory"}
1.8 + @{command_def (HOL) "nitpick_params"} & : & @{text "theory \<rightarrow> theory"} \\
1.9 + @{command_def (HOL) "quickcheck_generator"} & : & @{text "theory \<rightarrow> theory"}
1.10 \end{matharray}
1.11
1.12 @{rail "
1.13 @@ -1539,6 +1540,9 @@
1.14 (@@{command (HOL) quickcheck_params} | @@{command (HOL) refute_params} |
1.15 @@{command (HOL) nitpick_params}) ( '[' args ']' )?
1.16 ;
1.17 + @@{command (HOL) quickcheck_generator} typeconstructor \\
1.18 + 'operations:' ( @{syntax term} +)
1.19 + ;
1.20
1.21 modes: '(' (@{syntax name} +) ')'
1.22 ;
1.23 @@ -1630,6 +1634,11 @@
1.24 \item @{command (HOL) "quickcheck_params"} changes
1.25 @{command (HOL) "quickcheck"} configuration options persistently.
1.26
1.27 + \item @{command (HOL) "quickcheck_generator"} creates random and
1.28 + exhaustive value generators for a given type and operations.
1.29 + It generates values by using the operations as if they were
1.30 + constructors of that type.
1.31 +
1.32 \item @{command (HOL) "refute"} tests the current goal for
1.33 counterexamples using a reduction to SAT. The following configuration
1.34 options are supported:
2.1 --- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex Wed Dec 21 09:41:16 2011 +0100
2.2 +++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex Wed Dec 21 14:24:29 2011 +0100
2.3 @@ -2217,7 +2217,8 @@
2.4 \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}}} \\
2.5 \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}}} \\
2.6 \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}}} \\
2.7 - \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}}}
2.8 + \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}}} \\
2.9 + \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}}}
2.10 \end{matharray}
2.11
2.12 \begin{railoutput}
2.13 @@ -2281,6 +2282,16 @@
2.14 \rail@term{\isa{{\isaliteral{5D}{\isacharbrackright}}}}[]
2.15 \rail@endbar
2.16 \rail@end
2.17 +\rail@begin{4}{}
2.18 +\rail@term{\hyperlink{command.HOL.quickcheck-generator}{\mbox{\isa{\isacommand{quickcheck{\isaliteral{5F}{\isacharunderscore}}generator}}}}}[]
2.19 +\rail@nont{\isa{typeconstructor}}[]
2.20 +\rail@cr{2}
2.21 +\rail@term{\isa{operations{\isaliteral{3A}{\isacharcolon}}}}[]
2.22 +\rail@plus
2.23 +\rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[]
2.24 +\rail@nextplus{3}
2.25 +\rail@endplus
2.26 +\rail@end
2.27 \rail@begin{2}{\isa{modes}}
2.28 \rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[]
2.29 \rail@plus
2.30 @@ -2383,6 +2394,11 @@
2.31 \item \hyperlink{command.HOL.quickcheck-params}{\mbox{\isa{\isacommand{quickcheck{\isaliteral{5F}{\isacharunderscore}}params}}}} changes
2.32 \hyperlink{command.HOL.quickcheck}{\mbox{\isa{\isacommand{quickcheck}}}} configuration options persistently.
2.33
2.34 + \item \hyperlink{command.HOL.quickcheck-generator}{\mbox{\isa{\isacommand{quickcheck{\isaliteral{5F}{\isacharunderscore}}generator}}}} creates random and
2.35 + exhaustive value generators for a given type and operations.
2.36 + It generates values by using the operations as if they were
2.37 + constructors of that type.
2.38 +
2.39 \item \hyperlink{command.HOL.refute}{\mbox{\isa{\isacommand{refute}}}} tests the current goal for
2.40 counterexamples using a reduction to SAT. The following configuration
2.41 options are supported: