# HG changeset patch # User haftmann # Date 1246552348 -7200 # Node ID 9fb31e1a119660562d25e80e3883910968ed357a # Parent b8784cb17a3583752a9716db6c579b1df7faae53# Parent 0bf275fbe93ad0fefc3c6994512385345946349b merged diff -r b8784cb17a35 -r 9fb31e1a1196 doc-src/IsarRef/Thy/HOL_Specific.thy --- a/doc-src/IsarRef/Thy/HOL_Specific.thy Thu Jul 02 14:43:06 2009 +0100 +++ b/doc-src/IsarRef/Thy/HOL_Specific.thy Thu Jul 02 18:32:28 2009 +0200 @@ -81,7 +81,7 @@ \end{matharray} \begin{rail} - 'split\_format' (((name *) + 'and') | ('(' 'complete' ')')) + 'split\_format' ((( name * ) + 'and') | ('(' 'complete' ')')) ; \end{rail} @@ -369,7 +369,7 @@ dtspec: parname? typespec infix? '=' (cons + '|') ; - cons: name (type *) mixfix? + cons: name ( type * ) mixfix? \end{rail} \begin{description} @@ -515,7 +515,7 @@ \begin{rail} 'relation' term ; - 'lexicographic\_order' (clasimpmod *) + 'lexicographic\_order' ( clasimpmod * ) ; \end{rail} @@ -565,7 +565,7 @@ ; recdeftc thmdecl? tc ; - hints: '(' 'hints' (recdefmod *) ')' + hints: '(' 'hints' ( recdefmod * ) ')' ; recdefmod: (('recdef\_simp' | 'recdef\_cong' | 'recdef\_wf') (() | 'add' | 'del') ':' thmrefs) | clasimpmod ; @@ -783,7 +783,7 @@ \end{matharray} \begin{rail} - 'iprover' ('!' ?) (rulemod *) + 'iprover' ('!' ?) ( rulemod * ) ; \end{rail} @@ -824,6 +824,74 @@ *} +section {* Checking and refuting propositions *} + +text {* + Identifying incorrect propositions usually involves evaluation of + particular assignments and systematic counter example search. This + is supported by the following commands. + + \begin{matharray}{rcl} + @{command_def (HOL) "value"}@{text "\<^sup>*"} & : & @{text "context \"} \\ + @{command_def (HOL) "quickcheck"}@{text "\<^sup>*"} & : & @{text "proof \"} \\ + @{command_def (HOL) "quickcheck_params"} & : & @{text "theory \ theory"} + \end{matharray} + + \begin{rail} + 'value' ( ( '[' name ']' ) ? ) modes? term + ; + + 'quickcheck' ( ( '[' args ']' ) ? ) nat? + ; + + 'quickcheck_params' ( ( '[' args ']' ) ? ) + ; + + modes: '(' (name + ) ')' + ; + + args: ( name '=' value + ',' ) + ; + \end{rail} + + \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 also \cite{isabelle-ref}). + 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; available evaluators include @{text nbe} for + \emph{normalization by evaluation} and \emph{code} for code + generation in SML. + + \item @{command (HOL) "quickcheck"} tests the current goal for + counter examples using a series of arbitrary assignments for its + free variables; by default the first subgoal is tested, an other + can be selected explicitly using an optional goal index. + A number of configuration options are supported for + @{command (HOL) "quickcheck"}, notably: + + \begin{description} + + \item[size] specifies the maximum size of the search space for + assignment values. + + \item[iterations] sets how many sets of assignments are + generated for each particular size. + + \end{description} + + These option can be given within square brackets. + + \item @{command (HOL) "quickcheck_params"} changes quickcheck + configuration options persitently. + + \end{description} +*} + + section {* Invoking automated reasoning tools -- The Sledgehammer *} text {* @@ -860,7 +928,7 @@ \end{matharray} \begin{rail} - 'sledgehammer' (nameref *) + 'sledgehammer' ( nameref * ) ; 'atp\_messages' ('(' nat ')')? ; @@ -989,7 +1057,6 @@ (this actually covers the new-style theory format as well). \begin{matharray}{rcl} - @{command_def (HOL) "value"}@{text "\<^sup>*"} & : & @{text "context \"} \\ @{command_def (HOL) "code_module"} & : & @{text "theory \ theory"} \\ @{command_def (HOL) "code_library"} & : & @{text "theory \ theory"} \\ @{command_def (HOL) "consts_code"} & : & @{text "theory \ theory"} \\ @@ -998,9 +1065,6 @@ \end{matharray} \begin{rail} - 'value' term - ; - ( 'code\_module' | 'code\_library' ) modespec ? name ? \\ ( 'file' name ) ? ( 'imports' ( name + ) ) ? \\ 'contains' ( ( name '=' term ) + | term + ) @@ -1034,13 +1098,6 @@ ; \end{rail} - \begin{description} - - \item @{command (HOL) "value"}~@{text t} evaluates and prints a term - using the code generator. - - \end{description} - \medskip The other framework generates code from functional programs (including overloading using type classes) to SML \cite{SML}, OCaml \cite{OCaml} and Haskell \cite{haskell-revised-report}. diff -r b8784cb17a35 -r 9fb31e1a1196 doc-src/IsarRef/Thy/Spec.thy --- a/doc-src/IsarRef/Thy/Spec.thy Thu Jul 02 14:43:06 2009 +0100 +++ b/doc-src/IsarRef/Thy/Spec.thy Thu Jul 02 18:32:28 2009 +0200 @@ -600,7 +600,7 @@ ; 'instance' ; - 'instance' nameref '::' arity + 'instance' (nameref + 'and') '::' arity ; 'subclass' target? nameref ; @@ -644,7 +644,7 @@ concluded by an @{command_ref (local) "end"} command. Note that a list of simultaneous type constructors may be given; - this corresponds nicely to mutual recursive type definitions, e.g.\ + this corresponds nicely to mutually recursive type definitions, e.g.\ in Isabelle/HOL. \item @{command "instance"} in an instantiation target body sets diff -r b8784cb17a35 -r 9fb31e1a1196 doc-src/IsarRef/Thy/document/HOL_Specific.tex --- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex Thu Jul 02 14:43:06 2009 +0100 +++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex Thu Jul 02 18:32:28 2009 +0200 @@ -98,7 +98,7 @@ \end{matharray} \begin{rail} - 'split\_format' (((name *) + 'and') | ('(' 'complete' ')')) + 'split\_format' ((( name * ) + 'and') | ('(' 'complete' ')')) ; \end{rail} @@ -374,7 +374,7 @@ dtspec: parname? typespec infix? '=' (cons + '|') ; - cons: name (type *) mixfix? + cons: name ( type * ) mixfix? \end{rail} \begin{description} @@ -520,7 +520,7 @@ \begin{rail} 'relation' term ; - 'lexicographic\_order' (clasimpmod *) + 'lexicographic\_order' ( clasimpmod * ) ; \end{rail} @@ -570,7 +570,7 @@ ; recdeftc thmdecl? tc ; - hints: '(' 'hints' (recdefmod *) ')' + hints: '(' 'hints' ( recdefmod * ) ')' ; recdefmod: (('recdef\_simp' | 'recdef\_cong' | 'recdef\_wf') (() | 'add' | 'del') ':' thmrefs) | clasimpmod ; @@ -793,7 +793,7 @@ \end{matharray} \begin{rail} - 'iprover' ('!' ?) (rulemod *) + 'iprover' ('!' ?) ( rulemod * ) ; \end{rail} @@ -835,6 +835,76 @@ \end{isamarkuptext}% \isamarkuptrue% % +\isamarkupsection{Checking and refuting propositions% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +Identifying incorrect propositions usually involves evaluation of + particular assignments and systematic counter example search. This + is supported by the following commands. + + \begin{matharray}{rcl} + \indexdef{HOL}{command}{value}\hypertarget{command.HOL.value}{\hyperlink{command.HOL.value}{\mbox{\isa{\isacommand{value}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}context\ {\isasymrightarrow}{\isachardoublequote}} \\ + \indexdef{HOL}{command}{quickcheck}\hypertarget{command.HOL.quickcheck}{\hyperlink{command.HOL.quickcheck}{\mbox{\isa{\isacommand{quickcheck}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}proof\ {\isasymrightarrow}{\isachardoublequote}} \\ + \indexdef{HOL}{command}{quickcheck\_params}\hypertarget{command.HOL.quickcheck-params}{\hyperlink{command.HOL.quickcheck-params}{\mbox{\isa{\isacommand{quickcheck{\isacharunderscore}params}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} + \end{matharray} + + \begin{rail} + 'value' ( ( '[' name ']' ) ? ) modes? term + ; + + 'quickcheck' ( ( '[' args ']' ) ? ) nat? + ; + + 'quickcheck_params' ( ( '[' args ']' ) ? ) + ; + + modes: '(' (name + ) ')' + ; + + args: ( name '=' value + ',' ) + ; + \end{rail} + + \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 also \cite{isabelle-ref}). + 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; available evaluators include \isa{nbe} for + \emph{normalization by evaluation} and \emph{code} for code + generation in SML. + + \item \hyperlink{command.HOL.quickcheck}{\mbox{\isa{\isacommand{quickcheck}}}} tests the current goal for + counter examples using a series of arbitrary assignments for its + free variables; by default the first subgoal is tested, an other + can be selected explicitly using an optional goal index. + A number of configuration options are supported for + \hyperlink{command.HOL.quickcheck}{\mbox{\isa{\isacommand{quickcheck}}}}, notably: + + \begin{description} + + \item[size] specifies the maximum size of the search space for + assignment values. + + \item[iterations] sets how many sets of assignments are + generated for each particular size. + + \end{description} + + These option can be given within square brackets. + + \item \hyperlink{command.HOL.quickcheck-params}{\mbox{\isa{\isacommand{quickcheck{\isacharunderscore}params}}}} changes quickcheck + configuration options persitently. + + \end{description}% +\end{isamarkuptext}% +\isamarkuptrue% +% \isamarkupsection{Invoking automated reasoning tools -- The Sledgehammer% } \isamarkuptrue% @@ -873,7 +943,7 @@ \end{matharray} \begin{rail} - 'sledgehammer' (nameref *) + 'sledgehammer' ( nameref * ) ; 'atp\_messages' ('(' nat ')')? ; @@ -998,7 +1068,6 @@ (this actually covers the new-style theory format as well). \begin{matharray}{rcl} - \indexdef{HOL}{command}{value}\hypertarget{command.HOL.value}{\hyperlink{command.HOL.value}{\mbox{\isa{\isacommand{value}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}context\ {\isasymrightarrow}{\isachardoublequote}} \\ \indexdef{HOL}{command}{code\_module}\hypertarget{command.HOL.code-module}{\hyperlink{command.HOL.code-module}{\mbox{\isa{\isacommand{code{\isacharunderscore}module}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\ \indexdef{HOL}{command}{code\_library}\hypertarget{command.HOL.code-library}{\hyperlink{command.HOL.code-library}{\mbox{\isa{\isacommand{code{\isacharunderscore}library}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\ \indexdef{HOL}{command}{consts\_code}\hypertarget{command.HOL.consts-code}{\hyperlink{command.HOL.consts-code}{\mbox{\isa{\isacommand{consts{\isacharunderscore}code}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\ @@ -1007,9 +1076,6 @@ \end{matharray} \begin{rail} - 'value' term - ; - ( 'code\_module' | 'code\_library' ) modespec ? name ? \\ ( 'file' name ) ? ( 'imports' ( name + ) ) ? \\ 'contains' ( ( name '=' term ) + | term + ) @@ -1043,13 +1109,6 @@ ; \end{rail} - \begin{description} - - \item \hyperlink{command.HOL.value}{\mbox{\isa{\isacommand{value}}}}~\isa{t} evaluates and prints a term - using the code generator. - - \end{description} - \medskip The other framework generates code from functional programs (including overloading using type classes) to SML \cite{SML}, OCaml \cite{OCaml} and Haskell \cite{haskell-revised-report}. diff -r b8784cb17a35 -r 9fb31e1a1196 doc-src/IsarRef/Thy/document/Spec.tex --- a/doc-src/IsarRef/Thy/document/Spec.tex Thu Jul 02 14:43:06 2009 +0100 +++ b/doc-src/IsarRef/Thy/document/Spec.tex Thu Jul 02 18:32:28 2009 +0200 @@ -614,7 +614,7 @@ ; 'instance' ; - 'instance' nameref '::' arity + 'instance' (nameref + 'and') '::' arity ; 'subclass' target? nameref ; @@ -653,7 +653,7 @@ concluded by an \indexref{local}{command}{end}\hyperlink{command.local.end}{\mbox{\isa{\isacommand{end}}}} command. Note that a list of simultaneous type constructors may be given; - this corresponds nicely to mutual recursive type definitions, e.g.\ + this corresponds nicely to mutually recursive type definitions, e.g.\ in Isabelle/HOL. \item \hyperlink{command.instance}{\mbox{\isa{\isacommand{instance}}}} in an instantiation target body sets @@ -733,7 +733,7 @@ \end{matharray} Axiomatic type classes are Isabelle/Pure's primitive - \emph{definitional} interface to type classes. For practical + interface to type classes. For practical applications, you should consider using classes (cf.~\secref{sec:classes}) which provide high level interface.