doc-src/IsarRef/Thy/HOL_Specific.thy

   \begin{matharray}{rcl}
     @{attribute (HOL) split_format}@{text "\<^sup>*"} & : & @{text attribute} \\
   \end{matharray}
 
   \begin{rail}
-    'split\_format' (((name *) + 'and') | ('(' 'complete' ')'))
+    'split\_format' ((( name * ) + 'and') | ('(' 'complete' ')'))
     ;
   \end{rail}
 
   \begin{description}
   

     'rep\_datatype' ('(' (name +) ')')? (term +)
     ;
 
     dtspec: parname? typespec infix? '=' (cons + '|')
     ;
-    cons: name (type *) mixfix?
+    cons: name ( type * ) mixfix?
   \end{rail}
 
   \begin{description}
 
   \item @{command (HOL) "datatype"} defines inductive datatypes in

   \end{matharray}
 
   \begin{rail}
     'relation' term
     ;
-    'lexicographic\_order' (clasimpmod *)
+    'lexicographic\_order' ( clasimpmod * )
     ;
   \end{rail}
 
   \begin{description}
 

   \begin{rail}
     'recdef' ('(' 'permissive' ')')? \\ name term (prop +) hints?
     ;
     recdeftc thmdecl? tc
     ;
-    hints: '(' 'hints' (recdefmod *) ')'
+    hints: '(' 'hints' ( recdefmod * ) ')'
     ;
     recdefmod: (('recdef\_simp' | 'recdef\_cong' | 'recdef\_wf') (() | 'add' | 'del') ':' thmrefs) | clasimpmod
     ;
     tc: nameref ('(' nat ')')?
     ;

   \begin{matharray}{rcl}
     @{method_def (HOL) iprover} & : & @{text method} \\
   \end{matharray}
 
   \begin{rail}
-    'iprover' ('!' ?) (rulemod *)
+    'iprover' ('!' ?) ( rulemod * )
     ;
   \end{rail}
 
   The @{method (HOL) iprover} method performs intuitionistic proof
   search, depending on specifically declared rules from the context,

   geometry.  See @{"file" "~~/src/HOL/ex/Coherent.thy"} for some
   examples.
 *}
 
 
+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 \<rightarrow>"} \\
+    @{command_def (HOL) "quickcheck"}@{text "\<^sup>*"} & : & @{text "proof \<rightarrow>"} \\
+    @{command_def (HOL) "quickcheck_params"} & : & @{text "theory \<rightarrow> 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 {*
   Isabelle/HOL includes a generic \emph{ATP manager} that allows
   external automated reasoning tools to crunch a pending goal.

     @{command_def (HOL) "atp_messages"}@{text "\<^sup>*"} & : & @{text "any \<rightarrow>"} \\
     @{method_def (HOL) metis} & : & @{text method} \\
   \end{matharray}
 
   \begin{rail}
-  'sledgehammer' (nameref *)
+  'sledgehammer' ( nameref * )
   ;
   'atp\_messages' ('(' nat ')')?
   ;
 
   'metis' thmrefs

   One framework generates code from both functional and relational
   programs to SML.  See \cite{isabelle-HOL} for further information
   (this actually covers the new-style theory format as well).
 
   \begin{matharray}{rcl}
-    @{command_def (HOL) "value"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
     @{command_def (HOL) "code_module"} & : & @{text "theory \<rightarrow> theory"} \\
     @{command_def (HOL) "code_library"} & : & @{text "theory \<rightarrow> theory"} \\
     @{command_def (HOL) "consts_code"} & : & @{text "theory \<rightarrow> theory"} \\
     @{command_def (HOL) "types_code"} & : & @{text "theory \<rightarrow> theory"} \\  
     @{attribute_def (HOL) code} & : & @{text attribute} \\
   \end{matharray}
 
   \begin{rail}
-  'value' term
-  ;
-
   ( 'code\_module' | 'code\_library' ) modespec ? name ? \\
     ( 'file' name ) ? ( 'imports' ( name + ) ) ? \\
     'contains' ( ( name '=' term ) + | term + )
   ;
 

   ;
 
   'code' (name)?
   ;
   \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}.
   Conceptually, code generation is split up in three steps: