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}.