doc-src/IsarRef/Thy/HOL_Specific.thy
changeset 31912 f5bd306f5e9d
parent 31254 03a35fbc9dc6
child 31998 2c7a24f74db9
     1.1 --- a/doc-src/IsarRef/Thy/HOL_Specific.thy	Sun Jun 28 22:51:29 2009 +0200
     1.2 +++ b/doc-src/IsarRef/Thy/HOL_Specific.thy	Thu Jul 02 16:00:27 2009 +0200
     1.3 @@ -81,7 +81,7 @@
     1.4    \end{matharray}
     1.5  
     1.6    \begin{rail}
     1.7 -    'split\_format' (((name *) + 'and') | ('(' 'complete' ')'))
     1.8 +    'split\_format' ((( name * ) + 'and') | ('(' 'complete' ')'))
     1.9      ;
    1.10    \end{rail}
    1.11  
    1.12 @@ -369,7 +369,7 @@
    1.13  
    1.14      dtspec: parname? typespec infix? '=' (cons + '|')
    1.15      ;
    1.16 -    cons: name (type *) mixfix?
    1.17 +    cons: name ( type * ) mixfix?
    1.18    \end{rail}
    1.19  
    1.20    \begin{description}
    1.21 @@ -515,7 +515,7 @@
    1.22    \begin{rail}
    1.23      'relation' term
    1.24      ;
    1.25 -    'lexicographic\_order' (clasimpmod *)
    1.26 +    'lexicographic\_order' ( clasimpmod * )
    1.27      ;
    1.28    \end{rail}
    1.29  
    1.30 @@ -565,7 +565,7 @@
    1.31      ;
    1.32      recdeftc thmdecl? tc
    1.33      ;
    1.34 -    hints: '(' 'hints' (recdefmod *) ')'
    1.35 +    hints: '(' 'hints' ( recdefmod * ) ')'
    1.36      ;
    1.37      recdefmod: (('recdef\_simp' | 'recdef\_cong' | 'recdef\_wf') (() | 'add' | 'del') ':' thmrefs) | clasimpmod
    1.38      ;
    1.39 @@ -783,7 +783,7 @@
    1.40    \end{matharray}
    1.41  
    1.42    \begin{rail}
    1.43 -    'iprover' ('!' ?) (rulemod *)
    1.44 +    'iprover' ('!' ?) ( rulemod * )
    1.45      ;
    1.46    \end{rail}
    1.47  
    1.48 @@ -824,6 +824,74 @@
    1.49  *}
    1.50  
    1.51  
    1.52 +section {* Checking and refuting propositions *}
    1.53 +
    1.54 +text {*
    1.55 +  Identifying incorrect propositions usually involves evaluation of
    1.56 +  particular assignments and systematic counter example search.  This
    1.57 +  is supported by the following commands.
    1.58 +
    1.59 +  \begin{matharray}{rcl}
    1.60 +    @{command_def (HOL) "value"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
    1.61 +    @{command_def (HOL) "quickcheck"}@{text "\<^sup>*"} & : & @{text "proof \<rightarrow>"} \\
    1.62 +    @{command_def (HOL) "quickcheck_params"} & : & @{text "theory \<rightarrow> theory"}
    1.63 +  \end{matharray}
    1.64 +
    1.65 +  \begin{rail}
    1.66 +    'value' ( ( '[' name ']' ) ? ) modes? term
    1.67 +    ;
    1.68 +
    1.69 +    'quickcheck' ( ( '[' args ']' ) ? ) nat?
    1.70 +    ;
    1.71 +
    1.72 +    'quickcheck_params' ( ( '[' args ']' ) ? )
    1.73 +    ;
    1.74 +
    1.75 +    modes: '(' (name + ) ')'
    1.76 +    ;
    1.77 +
    1.78 +    args: ( name '=' value + ',' )
    1.79 +    ;
    1.80 +  \end{rail}
    1.81 +
    1.82 +  \begin{description}
    1.83 +
    1.84 +  \item @{command (HOL) "value"}~@{text t} evaluates and prints a
    1.85 +    term; optionally @{text modes} can be specified, which are
    1.86 +    appended to the current print mode (see also \cite{isabelle-ref}).
    1.87 +    Internally, the evaluation is performed by registered evaluators,
    1.88 +    which are invoked sequentially until a result is returned.
    1.89 +    Alternatively a specific evaluator can be selected using square
    1.90 +    brackets; available evaluators include @{text nbe} for
    1.91 +    \emph{normalization by evaluation} and \emph{code} for code
    1.92 +    generation in SML.
    1.93 +
    1.94 +  \item @{command (HOL) "quickcheck"} tests the current goal for
    1.95 +    counter examples using a series of arbitrary assignments for its
    1.96 +    free variables; by default the first subgoal is tested, an other
    1.97 +    can be selected explicitly using an optional goal index.
    1.98 +    A number of configuration options are supported for
    1.99 +    @{command (HOL) "quickcheck"}, notably:
   1.100 +
   1.101 +    \begin{description}
   1.102 +
   1.103 +      \item[size] specifies the maximum size of the search space for
   1.104 +        assignment values.
   1.105 +
   1.106 +      \item[iterations] sets how many sets of assignments are
   1.107 +        generated for each particular size.
   1.108 +
   1.109 +    \end{description}
   1.110 +
   1.111 +    These option can be given within square brackets.
   1.112 +
   1.113 +  \item @{command (HOL) "quickcheck_params"} changes quickcheck
   1.114 +    configuration options persitently.
   1.115 +
   1.116 +  \end{description}
   1.117 +*}
   1.118 +
   1.119 +
   1.120  section {* Invoking automated reasoning tools -- The Sledgehammer *}
   1.121  
   1.122  text {*
   1.123 @@ -860,7 +928,7 @@
   1.124    \end{matharray}
   1.125  
   1.126    \begin{rail}
   1.127 -  'sledgehammer' (nameref *)
   1.128 +  'sledgehammer' ( nameref * )
   1.129    ;
   1.130    'atp\_messages' ('(' nat ')')?
   1.131    ;
   1.132 @@ -989,7 +1057,6 @@
   1.133    (this actually covers the new-style theory format as well).
   1.134  
   1.135    \begin{matharray}{rcl}
   1.136 -    @{command_def (HOL) "value"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
   1.137      @{command_def (HOL) "code_module"} & : & @{text "theory \<rightarrow> theory"} \\
   1.138      @{command_def (HOL) "code_library"} & : & @{text "theory \<rightarrow> theory"} \\
   1.139      @{command_def (HOL) "consts_code"} & : & @{text "theory \<rightarrow> theory"} \\
   1.140 @@ -998,9 +1065,6 @@
   1.141    \end{matharray}
   1.142  
   1.143    \begin{rail}
   1.144 -  'value' term
   1.145 -  ;
   1.146 -
   1.147    ( 'code\_module' | 'code\_library' ) modespec ? name ? \\
   1.148      ( 'file' name ) ? ( 'imports' ( name + ) ) ? \\
   1.149      'contains' ( ( name '=' term ) + | term + )
   1.150 @@ -1034,13 +1098,6 @@
   1.151    ;
   1.152    \end{rail}
   1.153  
   1.154 -  \begin{description}
   1.155 -
   1.156 -  \item @{command (HOL) "value"}~@{text t} evaluates and prints a term
   1.157 -  using the code generator.
   1.158 -
   1.159 -  \end{description}
   1.160 -
   1.161    \medskip The other framework generates code from functional programs
   1.162    (including overloading using type classes) to SML \cite{SML}, OCaml
   1.163    \cite{OCaml} and Haskell \cite{haskell-revised-report}.