author  wenzelm 
Wed, 15 Oct 2008 21:06:15 +0200  
changeset 28603  b40800eef8a7 
parent 28562  4e74209f113e 
child 28687  150a8a1eae1a 
permissions  rwrr 
26840  1 
(* $Id$ *) 
2 

3 
theory HOL_Specific 

26849  4 
imports Main 
26840  5 
begin 
6 

26852  7 
chapter {* Isabelle/HOL \label{ch:hol} *} 
26849  8 

9 
section {* Primitive types \label{sec:holtypedef} *} 

10 

11 
text {* 

12 
\begin{matharray}{rcl} 

13 
@{command_def (HOL) "typedecl"} & : & \isartrans{theory}{theory} \\ 

14 
@{command_def (HOL) "typedef"} & : & \isartrans{theory}{proof(prove)} \\ 

15 
\end{matharray} 

16 

17 
\begin{rail} 

18 
'typedecl' typespec infix? 

19 
; 

20 
'typedef' altname? abstype '=' repset 

21 
; 

22 

23 
altname: '(' (name  'open'  'open' name) ')' 

24 
; 

25 
abstype: typespec infix? 

26 
; 

27 
repset: term ('morphisms' name name)? 

28 
; 

29 
\end{rail} 

30 

31 
\begin{descr} 

32 

33 
\item [@{command (HOL) "typedecl"}~@{text "(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>n) 

34 
t"}] is similar to the original @{command "typedecl"} of 

35 
Isabelle/Pure (see \secref{sec:typespure}), but also declares type 

36 
arity @{text "t :: (type, \<dots>, type) type"}, making @{text t} an 

37 
actual HOL type constructor. %FIXME check, update 

38 

39 
\item [@{command (HOL) "typedef"}~@{text "(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>n) 

40 
t = A"}] sets up a goal stating nonemptiness of the set @{text A}. 

41 
After finishing the proof, the theory will be augmented by a 

42 
Gordon/HOLstyle type definition, which establishes a bijection 

43 
between the representing set @{text A} and the new type @{text t}. 

44 

45 
Technically, @{command (HOL) "typedef"} defines both a type @{text 

46 
t} and a set (term constant) of the same name (an alternative base 

47 
name may be given in parentheses). The injection from type to set 

48 
is called @{text Rep_t}, its inverse @{text Abs_t} (this may be 

49 
changed via an explicit @{keyword (HOL) "morphisms"} declaration). 

50 

51 
Theorems @{text Rep_t}, @{text Rep_t_inverse}, and @{text 

52 
Abs_t_inverse} provide the most basic characterization as a 

53 
corresponding injection/surjection pair (in both directions). Rules 

54 
@{text Rep_t_inject} and @{text Abs_t_inject} provide a slightly 

55 
more convenient view on the injectivity part, suitable for automated 

26894  56 
proof tools (e.g.\ in @{attribute simp} or @{attribute iff} 
57 
declarations). Rules @{text Rep_t_cases}/@{text Rep_t_induct}, and 

58 
@{text Abs_t_cases}/@{text Abs_t_induct} provide alternative views 

59 
on surjectivity; these are already declared as set or type rules for 

26849  60 
the generic @{method cases} and @{method induct} methods. 
61 

62 
An alternative name may be specified in parentheses; the default is 

63 
to use @{text t} as indicated before. The ``@{text "(open)"}'' 

64 
declaration suppresses a separate constant definition for the 

65 
representing set. 

66 

67 
\end{descr} 

68 

69 
Note that raw type declarations are rarely used in practice; the 

70 
main application is with experimental (or even axiomatic!) theory 

71 
fragments. Instead of primitive HOL type definitions, userlevel 

72 
theories usually refer to higherlevel packages such as @{command 

73 
(HOL) "record"} (see \secref{sec:holrecord}) or @{command (HOL) 

74 
"datatype"} (see \secref{sec:holdatatype}). 

75 
*} 

76 

77 

78 
section {* Adhoc tuples *} 

79 

80 
text {* 

81 
\begin{matharray}{rcl} 

82 
@{attribute (HOL) split_format}@{text "\<^sup>*"} & : & \isaratt \\ 

83 
\end{matharray} 

84 

85 
\begin{rail} 

86 
'split\_format' (((name *) + 'and')  ('(' 'complete' ')')) 

87 
; 

88 
\end{rail} 

89 

90 
\begin{descr} 

91 

26894  92 
\item [@{attribute (HOL) split_format}~@{text "p\<^sub>1 \<dots> p\<^sub>m 
26849  93 
\<AND> \<dots> \<AND> q\<^sub>1 \<dots> q\<^sub>n"}] puts expressions of 
94 
lowlevel tuple types into canonical form as specified by the 

95 
arguments given; the @{text i}th collection of arguments refers to 

96 
occurrences in premise @{text i} of the rule. The ``@{text 

97 
"(complete)"}'' option causes \emph{all} arguments in function 

98 
applications to be represented canonically according to their tuple 

99 
type structure. 

100 

101 
Note that these operations tend to invent funny names for new local 

102 
parameters to be introduced. 

103 

104 
\end{descr} 

105 
*} 

106 

107 

108 
section {* Records \label{sec:holrecord} *} 

109 

110 
text {* 

111 
In principle, records merely generalize the concept of tuples, where 

112 
components may be addressed by labels instead of just position. The 

113 
logical infrastructure of records in Isabelle/HOL is slightly more 

114 
advanced, though, supporting truly extensible record schemes. This 

115 
admits operations that are polymorphic with respect to record 

116 
extension, yielding ``objectoriented'' effects like (single) 

117 
inheritance. See also \cite{NaraschewskiWTPHOLs98} for more 

118 
details on objectoriented verification and record subtyping in HOL. 

119 
*} 

120 

121 

122 
subsection {* Basic concepts *} 

123 

124 
text {* 

125 
Isabelle/HOL supports both \emph{fixed} and \emph{schematic} records 

126 
at the level of terms and types. The notation is as follows: 

127 

128 
\begin{center} 

129 
\begin{tabular}{lll} 

130 
& record terms & record types \\ \hline 

131 
fixed & @{text "\<lparr>x = a, y = b\<rparr>"} & @{text "\<lparr>x :: A, y :: B\<rparr>"} \\ 

132 
schematic & @{text "\<lparr>x = a, y = b, \<dots> = m\<rparr>"} & 

133 
@{text "\<lparr>x :: A, y :: B, \<dots> :: M\<rparr>"} \\ 

134 
\end{tabular} 

135 
\end{center} 

136 

137 
\noindent The ASCII representation of @{text "\<lparr>x = a\<rparr>"} is @{text 

138 
"( x = a )"}. 

139 

140 
A fixed record @{text "\<lparr>x = a, y = b\<rparr>"} has field @{text x} of value 

141 
@{text a} and field @{text y} of value @{text b}. The corresponding 

142 
type is @{text "\<lparr>x :: A, y :: B\<rparr>"}, assuming that @{text "a :: A"} 

143 
and @{text "b :: B"}. 

144 

145 
A record scheme like @{text "\<lparr>x = a, y = b, \<dots> = m\<rparr>"} contains fields 

146 
@{text x} and @{text y} as before, but also possibly further fields 

147 
as indicated by the ``@{text "\<dots>"}'' notation (which is actually part 

148 
of the syntax). The improper field ``@{text "\<dots>"}'' of a record 

149 
scheme is called the \emph{more part}. Logically it is just a free 

150 
variable, which is occasionally referred to as ``row variable'' in 

151 
the literature. The more part of a record scheme may be 

152 
instantiated by zero or more further components. For example, the 

153 
previous scheme may get instantiated to @{text "\<lparr>x = a, y = b, z = 

26852  154 
c, \<dots> = m'\<rparr>"}, where @{text m'} refers to a different more part. 
26849  155 
Fixed records are special instances of record schemes, where 
156 
``@{text "\<dots>"}'' is properly terminated by the @{text "() :: unit"} 

157 
element. In fact, @{text "\<lparr>x = a, y = b\<rparr>"} is just an abbreviation 

158 
for @{text "\<lparr>x = a, y = b, \<dots> = ()\<rparr>"}. 

159 

160 
\medskip Two key observations make extensible records in a simply 

161 
typed language like HOL work out: 

162 

163 
\begin{enumerate} 

164 

165 
\item the more part is internalized, as a free term or type 

166 
variable, 

167 

26852  168 
\item field names are externalized, they cannot be accessed within 
169 
the logic as firstclass values. 

26849  170 

171 
\end{enumerate} 

172 

173 
\medskip In Isabelle/HOL record types have to be defined explicitly, 

174 
fixing their field names and types, and their (optional) parent 

175 
record. Afterwards, records may be formed using above syntax, while 

176 
obeying the canonical order of fields as given by their declaration. 

177 
The record package provides several standard operations like 

178 
selectors and updates. The common setup for various generic proof 

179 
tools enable succinct reasoning patterns. See also the Isabelle/HOL 

180 
tutorial \cite{isabelleholbook} for further instructions on using 

181 
records in practice. 

182 
*} 

183 

184 

185 
subsection {* Record specifications *} 

186 

187 
text {* 

188 
\begin{matharray}{rcl} 

189 
@{command_def (HOL) "record"} & : & \isartrans{theory}{theory} \\ 

190 
\end{matharray} 

191 

192 
\begin{rail} 

193 
'record' typespec '=' (type '+')? (constdecl +) 

194 
; 

195 
\end{rail} 

196 

197 
\begin{descr} 

198 

199 
\item [@{command (HOL) "record"}~@{text "(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>m) t 

200 
= \<tau> + c\<^sub>1 :: \<sigma>\<^sub>1 \<dots> c\<^sub>n :: \<sigma>\<^sub>n"}] defines 

201 
extensible record type @{text "(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>m) t"}, 

202 
derived from the optional parent record @{text "\<tau>"} by adding new 

203 
field components @{text "c\<^sub>i :: \<sigma>\<^sub>i"} etc. 

204 

205 
The type variables of @{text "\<tau>"} and @{text "\<sigma>\<^sub>i"} need to be 

206 
covered by the (distinct) parameters @{text "\<alpha>\<^sub>1, \<dots>, 

207 
\<alpha>\<^sub>m"}. Type constructor @{text t} has to be new, while @{text 

208 
\<tau>} needs to specify an instance of an existing record type. At 

209 
least one new field @{text "c\<^sub>i"} has to be specified. 

210 
Basically, field names need to belong to a unique record. This is 

211 
not a real restriction in practice, since fields are qualified by 

212 
the record name internally. 

213 

214 
The parent record specification @{text \<tau>} is optional; if omitted 

215 
@{text t} becomes a root record. The hierarchy of all records 

216 
declared within a theory context forms a forest structure, i.e.\ a 

217 
set of trees starting with a root record each. There is no way to 

218 
merge multiple parent records! 

219 

220 
For convenience, @{text "(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>m) t"} is made a 

221 
type abbreviation for the fixed record type @{text "\<lparr>c\<^sub>1 :: 

222 
\<sigma>\<^sub>1, \<dots>, c\<^sub>n :: \<sigma>\<^sub>n\<rparr>"}, likewise is @{text 

223 
"(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>m, \<zeta>) t_scheme"} made an abbreviation for 

224 
@{text "\<lparr>c\<^sub>1 :: \<sigma>\<^sub>1, \<dots>, c\<^sub>n :: \<sigma>\<^sub>n, \<dots> :: 

225 
\<zeta>\<rparr>"}. 

226 

227 
\end{descr} 

228 
*} 

229 

230 

231 
subsection {* Record operations *} 

232 

233 
text {* 

234 
Any record definition of the form presented above produces certain 

235 
standard operations. Selectors and updates are provided for any 

236 
field, including the improper one ``@{text more}''. There are also 

237 
cumulative record constructor functions. To simplify the 

238 
presentation below, we assume for now that @{text "(\<alpha>\<^sub>1, \<dots>, 

239 
\<alpha>\<^sub>m) t"} is a root record with fields @{text "c\<^sub>1 :: 

240 
\<sigma>\<^sub>1, \<dots>, c\<^sub>n :: \<sigma>\<^sub>n"}. 

241 

242 
\medskip \textbf{Selectors} and \textbf{updates} are available for 

243 
any field (including ``@{text more}''): 

244 

245 
\begin{matharray}{lll} 

26852  246 
@{text "c\<^sub>i"} & @{text "::"} & @{text "\<lparr>\<^vec>c :: \<^vec>\<sigma>, \<dots> :: \<zeta>\<rparr> \<Rightarrow> \<sigma>\<^sub>i"} \\ 
247 
@{text "c\<^sub>i_update"} & @{text "::"} & @{text "\<sigma>\<^sub>i \<Rightarrow> \<lparr>\<^vec>c :: \<^vec>\<sigma>, \<dots> :: \<zeta>\<rparr> \<Rightarrow> \<lparr>\<^vec>c :: \<^vec>\<sigma>, \<dots> :: \<zeta>\<rparr>"} \\ 

26849  248 
\end{matharray} 
249 

250 
There is special syntax for application of updates: @{text "r\<lparr>x := 

251 
a\<rparr>"} abbreviates term @{text "x_update a r"}. Further notation for 

252 
repeated updates is also available: @{text "r\<lparr>x := a\<rparr>\<lparr>y := b\<rparr>\<lparr>z := 

253 
c\<rparr>"} may be written @{text "r\<lparr>x := a, y := b, z := c\<rparr>"}. Note that 

254 
because of postfix notation the order of fields shown here is 

255 
reverse than in the actual term. Since repeated updates are just 

256 
function applications, fields may be freely permuted in @{text "\<lparr>x 

257 
:= a, y := b, z := c\<rparr>"}, as far as logical equality is concerned. 

258 
Thus commutativity of independent updates can be proven within the 

259 
logic for any two fields, but not as a general theorem. 

260 

261 
\medskip The \textbf{make} operation provides a cumulative record 

262 
constructor function: 

263 

264 
\begin{matharray}{lll} 

26852  265 
@{text "t.make"} & @{text "::"} & @{text "\<sigma>\<^sub>1 \<Rightarrow> \<dots> \<sigma>\<^sub>n \<Rightarrow> \<lparr>\<^vec>c :: \<^vec>\<sigma>\<rparr>"} \\ 
26849  266 
\end{matharray} 
267 

268 
\medskip We now reconsider the case of nonroot records, which are 

269 
derived of some parent. In general, the latter may depend on 

270 
another parent as well, resulting in a list of \emph{ancestor 

271 
records}. Appending the lists of fields of all ancestors results in 

272 
a certain field prefix. The record package automatically takes care 

273 
of this by lifting operations over this context of ancestor fields. 

274 
Assuming that @{text "(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>m) t"} has ancestor 

275 
fields @{text "b\<^sub>1 :: \<rho>\<^sub>1, \<dots>, b\<^sub>k :: \<rho>\<^sub>k"}, 

276 
the above record operations will get the following types: 

277 

26852  278 
\medskip 
279 
\begin{tabular}{lll} 

280 
@{text "c\<^sub>i"} & @{text "::"} & @{text "\<lparr>\<^vec>b :: \<^vec>\<rho>, \<^vec>c :: \<^vec>\<sigma>, \<dots> :: \<zeta>\<rparr> \<Rightarrow> \<sigma>\<^sub>i"} \\ 

26849  281 
@{text "c\<^sub>i_update"} & @{text "::"} & @{text "\<sigma>\<^sub>i \<Rightarrow> 
26852  282 
\<lparr>\<^vec>b :: \<^vec>\<rho>, \<^vec>c :: \<^vec>\<sigma>, \<dots> :: \<zeta>\<rparr> \<Rightarrow> 
283 
\<lparr>\<^vec>b :: \<^vec>\<rho>, \<^vec>c :: \<^vec>\<sigma>, \<dots> :: \<zeta>\<rparr>"} \\ 

284 
@{text "t.make"} & @{text "::"} & @{text "\<rho>\<^sub>1 \<Rightarrow> \<dots> \<rho>\<^sub>k \<Rightarrow> \<sigma>\<^sub>1 \<Rightarrow> \<dots> \<sigma>\<^sub>n \<Rightarrow> 

285 
\<lparr>\<^vec>b :: \<^vec>\<rho>, \<^vec>c :: \<^vec>\<sigma>\<rparr>"} \\ 

286 
\end{tabular} 

287 
\medskip 

26849  288 

26852  289 
\noindent Some further operations address the extension aspect of a 
26849  290 
derived record scheme specifically: @{text "t.fields"} produces a 
291 
record fragment consisting of exactly the new fields introduced here 

292 
(the result may serve as a more part elsewhere); @{text "t.extend"} 

293 
takes a fixed record and adds a given more part; @{text 

294 
"t.truncate"} restricts a record scheme to a fixed record. 

295 

26852  296 
\medskip 
297 
\begin{tabular}{lll} 

298 
@{text "t.fields"} & @{text "::"} & @{text "\<sigma>\<^sub>1 \<Rightarrow> \<dots> \<sigma>\<^sub>n \<Rightarrow> \<lparr>\<^vec>c :: \<^vec>\<sigma>\<rparr>"} \\ 

299 
@{text "t.extend"} & @{text "::"} & @{text "\<lparr>\<^vec>b :: \<^vec>\<rho>, \<^vec>c :: \<^vec>\<sigma>\<rparr> \<Rightarrow> 

300 
\<zeta> \<Rightarrow> \<lparr>\<^vec>b :: \<^vec>\<rho>, \<^vec>c :: \<^vec>\<sigma>, \<dots> :: \<zeta>\<rparr>"} \\ 

301 
@{text "t.truncate"} & @{text "::"} & @{text "\<lparr>\<^vec>b :: \<^vec>\<rho>, \<^vec>c :: \<^vec>\<sigma>, \<dots> :: \<zeta>\<rparr> \<Rightarrow> \<lparr>\<^vec>b :: \<^vec>\<rho>, \<^vec>c :: \<^vec>\<sigma>\<rparr>"} \\ 

302 
\end{tabular} 

303 
\medskip 

26849  304 

305 
\noindent Note that @{text "t.make"} and @{text "t.fields"} coincide 

306 
for root records. 

307 
*} 

308 

309 

310 
subsection {* Derived rules and proof tools *} 

311 

312 
text {* 

313 
The record package proves several results internally, declaring 

314 
these facts to appropriate proof tools. This enables users to 

315 
reason about record structures quite conveniently. Assume that 

316 
@{text t} is a record type as specified above. 

317 

318 
\begin{enumerate} 

319 

320 
\item Standard conversions for selectors or updates applied to 

321 
record constructor terms are made part of the default Simplifier 

322 
context; thus proofs by reduction of basic operations merely require 

323 
the @{method simp} method without further arguments. These rules 

324 
are available as @{text "t.simps"}, too. 

325 

326 
\item Selectors applied to updated records are automatically reduced 

327 
by an internal simplification procedure, which is also part of the 

328 
standard Simplifier setup. 

329 

330 
\item Inject equations of a form analogous to @{prop "(x, y) = (x', 

331 
y') \<equiv> x = x' \<and> y = y'"} are declared to the Simplifier and Classical 

332 
Reasoner as @{attribute iff} rules. These rules are available as 

333 
@{text "t.iffs"}. 

334 

335 
\item The introduction rule for record equality analogous to @{text 

336 
"x r = x r' \<Longrightarrow> y r = y r' \<dots> \<Longrightarrow> r = r'"} is declared to the Simplifier, 

337 
and as the basic rule context as ``@{attribute intro}@{text "?"}''. 

338 
The rule is called @{text "t.equality"}. 

339 

340 
\item Representations of arbitrary record expressions as canonical 

341 
constructor terms are provided both in @{method cases} and @{method 

342 
induct} format (cf.\ the generic proof methods of the same name, 

343 
\secref{sec:casesinduct}). Several variations are available, for 

344 
fixed records, record schemes, more parts etc. 

345 

346 
The generic proof methods are sufficiently smart to pick the most 

347 
sensible rule according to the type of the indicated record 

348 
expression: users just need to apply something like ``@{text "(cases 

349 
r)"}'' to a certain proof problem. 

350 

351 
\item The derived record operations @{text "t.make"}, @{text 

352 
"t.fields"}, @{text "t.extend"}, @{text "t.truncate"} are \emph{not} 

353 
treated automatically, but usually need to be expanded by hand, 

354 
using the collective fact @{text "t.defs"}. 

355 

356 
\end{enumerate} 

357 
*} 

358 

359 

360 
section {* Datatypes \label{sec:holdatatype} *} 

361 

362 
text {* 

363 
\begin{matharray}{rcl} 

364 
@{command_def (HOL) "datatype"} & : & \isartrans{theory}{theory} \\ 

27452  365 
@{command_def (HOL) "rep_datatype"} & : & \isartrans{theory}{proof} \\ 
26849  366 
\end{matharray} 
367 

368 
\begin{rail} 

369 
'datatype' (dtspec + 'and') 

370 
; 

27452  371 
'rep\_datatype' ('(' (name +) ')')? (term +) 
26849  372 
; 
373 

374 
dtspec: parname? typespec infix? '=' (cons + '') 

375 
; 

376 
cons: name (type *) mixfix? 

377 
\end{rail} 

378 

379 
\begin{descr} 

380 

381 
\item [@{command (HOL) "datatype"}] defines inductive datatypes in 

382 
HOL. 

383 

384 
\item [@{command (HOL) "rep_datatype"}] represents existing types as 

385 
inductive ones, generating the standard infrastructure of derived 

386 
concepts (primitive recursion etc.). 

387 

388 
\end{descr} 

389 

390 
The induction and exhaustion theorems generated provide case names 

391 
according to the constructors involved, while parameters are named 

392 
after the types (see also \secref{sec:casesinduct}). 

393 

394 
See \cite{isabelleHOL} for more details on datatypes, but beware of 

395 
the oldstyle theory syntax being used there! Apart from proper 

396 
proof methods for caseanalysis and induction, there are also 

397 
emulations of ML tactics @{method (HOL) case_tac} and @{method (HOL) 

398 
induct_tac} available, see \secref{sec:holinducttac}; these admit 

399 
to refer directly to the internal structure of subgoals (including 

400 
internally bound parameters). 

401 
*} 

402 

403 

404 
section {* Recursive functions \label{sec:recursion} *} 

405 

406 
text {* 

407 
\begin{matharray}{rcl} 

408 
@{command_def (HOL) "primrec"} & : & \isarkeep{local{\dsh}theory} \\ 

409 
@{command_def (HOL) "fun"} & : & \isarkeep{local{\dsh}theory} \\ 

410 
@{command_def (HOL) "function"} & : & \isartrans{local{\dsh}theory}{proof(prove)} \\ 

411 
@{command_def (HOL) "termination"} & : & \isartrans{local{\dsh}theory}{proof(prove)} \\ 

412 
\end{matharray} 

413 

414 
\begin{rail} 

415 
'primrec' target? fixes 'where' equations 

416 
; 

417 
equations: (thmdecl? prop + '') 

418 
; 

26985
51c5acd57b75
function: uniform treatment of target, not as config;
wenzelm
parents:
26894
diff
changeset

419 
('fun'  'function') target? functionopts? fixes 'where' clauses 
26849  420 
; 
421 
clauses: (thmdecl? prop ('(' 'otherwise' ')')? + '') 

422 
; 

26985
51c5acd57b75
function: uniform treatment of target, not as config;
wenzelm
parents:
26894
diff
changeset

423 
functionopts: '(' (('sequential'  'domintros'  'tailrec'  'default' term) + ',') ')' 
26849  424 
; 
425 
'termination' ( term )? 

426 
\end{rail} 

427 

428 
\begin{descr} 

429 

430 
\item [@{command (HOL) "primrec"}] defines primitive recursive 

431 
functions over datatypes, see also \cite{isabelleHOL}. 

432 

433 
\item [@{command (HOL) "function"}] defines functions by general 

434 
wellfounded recursion. A detailed description with examples can be 

435 
found in \cite{isabellefunction}. The function is specified by a 

436 
set of (possibly conditional) recursive equations with arbitrary 

437 
pattern matching. The command generates proof obligations for the 

438 
completeness and the compatibility of patterns. 

439 

440 
The defined function is considered partial, and the resulting 

441 
simplification rules (named @{text "f.psimps"}) and induction rule 

442 
(named @{text "f.pinduct"}) are guarded by a generated domain 

443 
predicate @{text "f_dom"}. The @{command (HOL) "termination"} 

444 
command can then be used to establish that the function is total. 

445 

446 
\item [@{command (HOL) "fun"}] is a shorthand notation for 

447 
``@{command (HOL) "function"}~@{text "(sequential)"}, followed by 

448 
automated proof attempts regarding pattern matching and termination. 

449 
See \cite{isabellefunction} for further details. 

450 

451 
\item [@{command (HOL) "termination"}~@{text f}] commences a 

452 
termination proof for the previously defined function @{text f}. If 

453 
this is omitted, the command refers to the most recent function 

454 
definition. After the proof is closed, the recursive equations and 

455 
the induction principle is established. 

456 

457 
\end{descr} 

458 

459 
%FIXME check 

460 

27452  461 
Recursive definitions introduced by the @{command (HOL) "function"} 
462 
command accommodate 

26849  463 
reasoning by induction (cf.\ \secref{sec:casesinduct}): rule @{text 
464 
"c.induct"} (where @{text c} is the name of the function definition) 

465 
refers to a specific induction rule, with parameters named according 

27452  466 
to the userspecified equations. 
467 
For the @{command (HOL) "primrec"} the induction principle coincides 

468 
with structural recursion on the datatype the recursion is carried 

469 
out. 

470 
Case names of @{command (HOL) 

26849  471 
"primrec"} are that of the datatypes involved, while those of 
472 
@{command (HOL) "function"} are numbered (starting from 1). 

473 

474 
The equations provided by these packages may be referred later as 

475 
theorem list @{text "f.simps"}, where @{text f} is the (collective) 

476 
name of the functions defined. Individual equations may be named 

477 
explicitly as well. 

478 

479 
The @{command (HOL) "function"} command accepts the following 

480 
options. 

481 

482 
\begin{descr} 

483 

484 
\item [@{text sequential}] enables a preprocessor which 

485 
disambiguates overlapping patterns by making them mutually disjoint. 

486 
Earlier equations take precedence over later ones. This allows to 

487 
give the specification in a format very similar to functional 

488 
programming. Note that the resulting simplification and induction 

489 
rules correspond to the transformed specification, not the one given 

490 
originally. This usually means that each equation given by the user 

491 
may result in several theroems. Also note that this automatic 

492 
transformation only works for MLstyle datatype patterns. 

493 

494 
\item [@{text domintros}] enables the automated generation of 

495 
introduction rules for the domain predicate. While mostly not 

496 
needed, they can be helpful in some proofs about partial functions. 

497 

498 
\item [@{text tailrec}] generates the unconstrained recursive 

499 
equations even without a termination proof, provided that the 

500 
function is tailrecursive. This currently only works 

501 

502 
\item [@{text "default d"}] allows to specify a default value for a 

503 
(partial) function, which will ensure that @{text "f x = d x"} 

504 
whenever @{text "x \<notin> f_dom"}. 

505 

506 
\end{descr} 

507 
*} 

508 

509 

510 
subsection {* Proof methods related to recursive definitions *} 

511 

512 
text {* 

513 
\begin{matharray}{rcl} 

514 
@{method_def (HOL) pat_completeness} & : & \isarmeth \\ 

515 
@{method_def (HOL) relation} & : & \isarmeth \\ 

516 
@{method_def (HOL) lexicographic_order} & : & \isarmeth \\ 

517 
\end{matharray} 

518 

519 
\begin{rail} 

520 
'relation' term 

521 
; 

522 
'lexicographic\_order' (clasimpmod *) 

523 
; 

524 
\end{rail} 

525 

526 
\begin{descr} 

527 

528 
\item [@{method (HOL) pat_completeness}] is a specialized method to 

529 
solve goals regarding the completeness of pattern matching, as 

530 
required by the @{command (HOL) "function"} package (cf.\ 

531 
\cite{isabellefunction}). 

532 

533 
\item [@{method (HOL) relation}~@{text R}] introduces a termination 

534 
proof using the relation @{text R}. The resulting proof state will 

535 
contain goals expressing that @{text R} is wellfounded, and that the 

536 
arguments of recursive calls decrease with respect to @{text R}. 

537 
Usually, this method is used as the initial proof step of manual 

538 
termination proofs. 

539 

540 
\item [@{method (HOL) "lexicographic_order"}] attempts a fully 

541 
automated termination proof by searching for a lexicographic 

542 
combination of size measures on the arguments of the function. The 

543 
method accepts the same arguments as the @{method auto} method, 

544 
which it uses internally to prove local descents. The same context 

545 
modifiers as for @{method auto} are accepted, see 

546 
\secref{sec:clasimp}. 

547 

548 
In case of failure, extensive information is printed, which can help 

549 
to analyse the situation (cf.\ \cite{isabellefunction}). 

550 

551 
\end{descr} 

552 
*} 

553 

554 

555 
subsection {* Oldstyle recursive function definitions (TFL) *} 

556 

557 
text {* 

558 
The old TFL commands @{command (HOL) "recdef"} and @{command (HOL) 

559 
"recdef_tc"} for defining recursive are mostly obsolete; @{command 

560 
(HOL) "function"} or @{command (HOL) "fun"} should be used instead. 

561 

562 
\begin{matharray}{rcl} 

563 
@{command_def (HOL) "recdef"} & : & \isartrans{theory}{theory} \\ 

564 
@{command_def (HOL) "recdef_tc"}@{text "\<^sup>*"} & : & \isartrans{theory}{proof(prove)} \\ 

565 
\end{matharray} 

566 

567 
\begin{rail} 

568 
'recdef' ('(' 'permissive' ')')? \\ name term (prop +) hints? 

569 
; 

570 
recdeftc thmdecl? tc 

571 
; 

572 
hints: '(' 'hints' (recdefmod *) ')' 

573 
; 

574 
recdefmod: (('recdef\_simp'  'recdef\_cong'  'recdef\_wf') (()  'add'  'del') ':' thmrefs)  clasimpmod 

575 
; 

576 
tc: nameref ('(' nat ')')? 

577 
; 

578 
\end{rail} 

579 

580 
\begin{descr} 

581 

582 
\item [@{command (HOL) "recdef"}] defines general wellfounded 

583 
recursive functions (using the TFL package), see also 

584 
\cite{isabelleHOL}. The ``@{text "(permissive)"}'' option tells 

585 
TFL to recover from failed proof attempts, returning unfinished 

586 
results. The @{text recdef_simp}, @{text recdef_cong}, and @{text 

587 
recdef_wf} hints refer to auxiliary rules to be used in the internal 

588 
automated proof process of TFL. Additional @{syntax clasimpmod} 

589 
declarations (cf.\ \secref{sec:clasimp}) may be given to tune the 

590 
context of the Simplifier (cf.\ \secref{sec:simplifier}) and 

591 
Classical reasoner (cf.\ \secref{sec:classical}). 

592 

593 
\item [@{command (HOL) "recdef_tc"}~@{text "c (i)"}] recommences the 

594 
proof for leftover termination condition number @{text i} (default 

595 
1) as generated by a @{command (HOL) "recdef"} definition of 

596 
constant @{text c}. 

597 

598 
Note that in most cases, @{command (HOL) "recdef"} is able to finish 

599 
its internal proofs without manual intervention. 

600 

601 
\end{descr} 

602 

603 
\medskip Hints for @{command (HOL) "recdef"} may be also declared 

604 
globally, using the following attributes. 

605 

606 
\begin{matharray}{rcl} 

607 
@{attribute_def (HOL) recdef_simp} & : & \isaratt \\ 

608 
@{attribute_def (HOL) recdef_cong} & : & \isaratt \\ 

609 
@{attribute_def (HOL) recdef_wf} & : & \isaratt \\ 

610 
\end{matharray} 

611 

612 
\begin{rail} 

613 
('recdef\_simp'  'recdef\_cong'  'recdef\_wf') (()  'add'  'del') 

614 
; 

615 
\end{rail} 

616 
*} 

617 

618 

619 
section {* Inductive and coinductive definitions \label{sec:holinductive} *} 

620 

621 
text {* 

622 
An \textbf{inductive definition} specifies the least predicate (or 

623 
set) @{text R} closed under given rules: applying a rule to elements 

624 
of @{text R} yields a result within @{text R}. For example, a 

625 
structural operational semantics is an inductive definition of an 

626 
evaluation relation. 

627 

628 
Dually, a \textbf{coinductive definition} specifies the greatest 

629 
predicate~/ set @{text R} that is consistent with given rules: every 

630 
element of @{text R} can be seen as arising by applying a rule to 

631 
elements of @{text R}. An important example is using bisimulation 

632 
relations to formalise equivalence of processes and infinite data 

633 
structures. 

634 

635 
\medskip The HOL package is related to the ZF one, which is 

636 
described in a separate paper,\footnote{It appeared in CADE 

637 
\cite{paulsonCADE}; a longer version is distributed with Isabelle.} 

638 
which you should refer to in case of difficulties. The package is 

639 
simpler than that of ZF thanks to implicit typechecking in HOL. 

640 
The types of the (co)inductive predicates (or sets) determine the 

641 
domain of the fixedpoint definition, and the package does not have 

642 
to use inference rules for typechecking. 

643 

644 
\begin{matharray}{rcl} 

645 
@{command_def (HOL) "inductive"} & : & \isarkeep{local{\dsh}theory} \\ 

646 
@{command_def (HOL) "inductive_set"} & : & \isarkeep{local{\dsh}theory} \\ 

647 
@{command_def (HOL) "coinductive"} & : & \isarkeep{local{\dsh}theory} \\ 

648 
@{command_def (HOL) "coinductive_set"} & : & \isarkeep{local{\dsh}theory} \\ 

649 
@{attribute_def (HOL) mono} & : & \isaratt \\ 

650 
\end{matharray} 

651 

652 
\begin{rail} 

653 
('inductive'  'inductive\_set'  'coinductive'  'coinductive\_set') target? fixes ('for' fixes)? \\ 

654 
('where' clauses)? ('monos' thmrefs)? 

655 
; 

656 
clauses: (thmdecl? prop + '') 

657 
; 

658 
'mono' (()  'add'  'del') 

659 
; 

660 
\end{rail} 

661 

662 
\begin{descr} 

663 

664 
\item [@{command (HOL) "inductive"} and @{command (HOL) 

665 
"coinductive"}] define (co)inductive predicates from the 

666 
introduction rules given in the @{keyword "where"} part. The 

667 
optional @{keyword "for"} part contains a list of parameters of the 

668 
(co)inductive predicates that remain fixed throughout the 

669 
definition. The optional @{keyword "monos"} section contains 

670 
\emph{monotonicity theorems}, which are required for each operator 

671 
applied to a recursive set in the introduction rules. There 

672 
\emph{must} be a theorem of the form @{text "A \<le> B \<Longrightarrow> M A \<le> M B"}, 

673 
for each premise @{text "M R\<^sub>i t"} in an introduction rule! 

674 

675 
\item [@{command (HOL) "inductive_set"} and @{command (HOL) 

676 
"coinductive_set"}] are wrappers for to the previous commands, 

677 
allowing the definition of (co)inductive sets. 

678 

679 
\item [@{attribute (HOL) mono}] declares monotonicity rules. These 

680 
rule are involved in the automated monotonicity proof of @{command 

681 
(HOL) "inductive"}. 

682 

683 
\end{descr} 

684 
*} 

685 

686 

687 
subsection {* Derived rules *} 

688 

689 
text {* 

690 
Each (co)inductive definition @{text R} adds definitions to the 

691 
theory and also proves some theorems: 

692 

693 
\begin{description} 

694 

695 
\item [@{text R.intros}] is the list of introduction rules as proven 

696 
theorems, for the recursive predicates (or sets). The rules are 

697 
also available individually, using the names given them in the 

698 
theory file; 

699 

700 
\item [@{text R.cases}] is the case analysis (or elimination) rule; 

701 

702 
\item [@{text R.induct} or @{text R.coinduct}] is the (co)induction 

703 
rule. 

704 

705 
\end{description} 

706 

707 
When several predicates @{text "R\<^sub>1, \<dots>, R\<^sub>n"} are 

708 
defined simultaneously, the list of introduction rules is called 

709 
@{text "R\<^sub>1_\<dots>_R\<^sub>n.intros"}, the case analysis rules are 

710 
called @{text "R\<^sub>1.cases, \<dots>, R\<^sub>n.cases"}, and the list 

711 
of mutual induction rules is called @{text 

712 
"R\<^sub>1_\<dots>_R\<^sub>n.inducts"}. 

713 
*} 

714 

715 

716 
subsection {* Monotonicity theorems *} 

717 

718 
text {* 

719 
Each theory contains a default set of theorems that are used in 

720 
monotonicity proofs. New rules can be added to this set via the 

721 
@{attribute (HOL) mono} attribute. The HOL theory @{text Inductive} 

722 
shows how this is done. In general, the following monotonicity 

723 
theorems may be added: 

724 

725 
\begin{itemize} 

726 

727 
\item Theorems of the form @{text "A \<le> B \<Longrightarrow> M A \<le> M B"}, for proving 

728 
monotonicity of inductive definitions whose introduction rules have 

729 
premises involving terms such as @{text "M R\<^sub>i t"}. 

730 

731 
\item Monotonicity theorems for logical operators, which are of the 

732 
general form @{text "(\<dots> \<longrightarrow> \<dots>) \<Longrightarrow> \<dots> (\<dots> \<longrightarrow> \<dots>) \<Longrightarrow> \<dots> \<longrightarrow> \<dots>"}. For example, in 

733 
the case of the operator @{text "\<or>"}, the corresponding theorem is 

734 
\[ 

735 
\infer{@{text "P\<^sub>1 \<or> P\<^sub>2 \<longrightarrow> Q\<^sub>1 \<or> Q\<^sub>2"}}{@{text "P\<^sub>1 \<longrightarrow> Q\<^sub>1"} & @{text "P\<^sub>2 \<longrightarrow> Q\<^sub>2"}} 

736 
\] 

737 

738 
\item De Morgan style equations for reasoning about the ``polarity'' 

739 
of expressions, e.g. 

740 
\[ 

741 
@{prop "\<not> \<not> P \<longleftrightarrow> P"} \qquad\qquad 

742 
@{prop "\<not> (P \<and> Q) \<longleftrightarrow> \<not> P \<or> \<not> Q"} 

743 
\] 

744 

745 
\item Equations for reducing complex operators to more primitive 

746 
ones whose monotonicity can easily be proved, e.g. 

747 
\[ 

748 
@{prop "(P \<longrightarrow> Q) \<longleftrightarrow> \<not> P \<or> Q"} \qquad\qquad 

749 
@{prop "Ball A P \<equiv> \<forall>x. x \<in> A \<longrightarrow> P x"} 

750 
\] 

751 

752 
\end{itemize} 

753 

754 
%FIXME: Example of an inductive definition 

755 
*} 

756 

757 

758 
section {* Arithmetic proof support *} 

759 

760 
text {* 

761 
\begin{matharray}{rcl} 

762 
@{method_def (HOL) arith} & : & \isarmeth \\ 

26894  763 
@{attribute_def (HOL) arith_split} & : & \isaratt \\ 
26849  764 
\end{matharray} 
765 

766 
The @{method (HOL) arith} method decides linear arithmetic problems 

767 
(on types @{text nat}, @{text int}, @{text real}). Any current 

768 
facts are inserted into the goal before running the procedure. 

769 

26894  770 
The @{attribute (HOL) arith_split} attribute declares case split 
771 
rules to be expanded before the arithmetic procedure is invoked. 

26849  772 

773 
Note that a simpler (but faster) version of arithmetic reasoning is 

774 
already performed by the Simplifier. 

775 
*} 

776 

777 

28603  778 
section {* Invoking automated reasoning tools  The Sledgehammer *} 
779 

780 
text {* 

781 
Isabelle/HOL includes a generic \emph{ATP manager} that allows 

782 
external automated reasoning tools to crunch a pending goal. 

783 
Supported provers include E\footnote{\url{http://www.eprover.org}}, 

784 
SPASS\footnote{\url{http://www.spassprover.org/}}, and Vampire. 

785 
There is also a wrapper to invoke provers remotely via the 

786 
SystemOnTPTP\footnote{\url{http://www.cs.miami.edu/~tptp/cgibin/SystemOnTPTP}} 

787 
web service. 

788 

789 
The problem passed to external provers consists of the goal together 

790 
with a smart selection of lemmas from the current theory context. 

791 
The result of a successful proof search is some source text that 

792 
usually reconstructs the proof within Isabelle, without requiring 

793 
external provers again. The Metis 

794 
prover\footnote{\url{http://www.gilith.com/software/metis/}} that is 

795 
integrated into Isabelle/HOL is being used here. 

796 

797 
In this mode of operation, heavy means of automated reasoning are 

798 
used as a strong relevance filter, while the main proof checking 

799 
works via explicit inferences going through the Isabelle kernel. 

800 
Moreover, rechecking Isabelle proof texts with already specified 

801 
auxiliary facts is much faster than performing fully automated 

802 
search over and over again. 

803 

804 
\begin{matharray}{rcl} 

805 
@{command_def (HOL) "sledgehammer"}@{text "\<^sup>*"} & : & \isarkeep{proof} \\ 

806 
@{command_def (HOL) "print_atps"}@{text "\<^sup>*"} & : & \isarkeep{theory~~proof} \\ 

807 
@{command_def (HOL) "atp_info"}@{text "\<^sup>*"} & : & \isarkeep{\cdot} \\ 

808 
@{command_def (HOL) "atp_kill"}@{text "\<^sup>*"} & : & \isarkeep{\cdot} \\ 

809 
@{method_def (HOL) metis} & : & \isarmeth \\ 

810 
\end{matharray} 

811 

812 
\begin{rail} 

813 
'sledgehammer' (nameref *) 

814 
; 

815 

816 
'metis' thmrefs 

817 
; 

818 
\end{rail} 

819 

820 
\begin{descr} 

821 

822 
\item [@{command (HOL) sledgehammer}~@{text "prover\<^sub>1 \<dots> 

823 
prover\<^sub>n"}] invokes the specified automated theorem provers on 

824 
the first subgoal. Provers are run in parallel, the first 

825 
successful result is displayed, and the other attempts are 

826 
terminated. 

827 

828 
Provers are defined in the theory context, see also @{command (HOL) 

829 
print_atps}. If no provers are given as arguments to @{command 

830 
(HOL) sledgehammer}, the system refers to the default defined as 

831 
``ATP provers'' preference by the user interface. 

832 

833 
There are additional preferences for timeout (default: 60 seconds), 

834 
and the maximum number of independent prover processes (default: 5); 

835 
excessive provers are automatically terminated. 

836 

837 
\item [@{command (HOL) print_atps}] prints the list of automated 

838 
theorem provers available to the @{command (HOL) sledgehammer} 

839 
command. 

840 

841 
\item [@{command (HOL) atp_info}] prints information about presently 

842 
running provers, including elapsed runtime, and the remaining time 

843 
until timeout. 

844 

845 
\item [@{command (HOL) atp_kill}] terminates all presently running 

846 
provers. 

847 

848 
\item [@{method (HOL) metis}~@{text "facts"}] invokes the Metis 

849 
prover with the given facts. Metis is an automated proof tool of 

850 
medium strength, but is fully integrated into Isabelle/HOL, with 

851 
explicit inferences going through the kernel. Thus its results are 

852 
guaranteed to be ``correct by construction''. 

853 

854 
Note that all facts used with Metis need to be specified as explicit 

855 
arguments. There are no rule declarations as for other Isabelle 

856 
provers, like @{method blast} or @{method fast}. 

857 

858 
\end{descr} 

859 
*} 

860 

861 

27123
11fcdd5897dd
case_tac/induct_tac: use same declarations as cases/induct;
wenzelm
parents:
27103
diff
changeset

862 
section {* Unstructured cases analysis and induction \label{sec:holinducttac} *} 
26849  863 

864 
text {* 

27123
11fcdd5897dd
case_tac/induct_tac: use same declarations as cases/induct;
wenzelm
parents:
27103
diff
changeset

865 
The following tools of Isabelle/HOL support cases analysis and 
11fcdd5897dd
case_tac/induct_tac: use same declarations as cases/induct;
wenzelm
parents:
27103
diff
changeset

866 
induction in unstructured tactic scripts; see also 
11fcdd5897dd
case_tac/induct_tac: use same declarations as cases/induct;
wenzelm
parents:
27103
diff
changeset

867 
\secref{sec:casesinduct} for proper Isar versions of similar ideas. 
26849  868 

869 
\begin{matharray}{rcl} 

870 
@{method_def (HOL) case_tac}@{text "\<^sup>*"} & : & \isarmeth \\ 

871 
@{method_def (HOL) induct_tac}@{text "\<^sup>*"} & : & \isarmeth \\ 

872 
@{method_def (HOL) ind_cases}@{text "\<^sup>*"} & : & \isarmeth \\ 

27123
11fcdd5897dd
case_tac/induct_tac: use same declarations as cases/induct;
wenzelm
parents:
27103
diff
changeset

873 
@{command_def (HOL) "inductive_cases"}@{text "\<^sup>*"} & : & \isartrans{theory}{theory} \\ 
26849  874 
\end{matharray} 
875 

876 
\begin{rail} 

877 
'case\_tac' goalspec? term rule? 

878 
; 

879 
'induct\_tac' goalspec? (insts * 'and') rule? 

880 
; 

881 
'ind\_cases' (prop +) ('for' (name +)) ? 

882 
; 

883 
'inductive\_cases' (thmdecl? (prop +) + 'and') 

884 
; 

885 

886 
rule: ('rule' ':' thmref) 

887 
; 

888 
\end{rail} 

889 

890 
\begin{descr} 

891 

892 
\item [@{method (HOL) case_tac} and @{method (HOL) induct_tac}] 

27123
11fcdd5897dd
case_tac/induct_tac: use same declarations as cases/induct;
wenzelm
parents:
27103
diff
changeset

893 
admit to reason about inductive types. Rules are selected according 
11fcdd5897dd
case_tac/induct_tac: use same declarations as cases/induct;
wenzelm
parents:
27103
diff
changeset

894 
to the declarations by the @{attribute cases} and @{attribute 
11fcdd5897dd
case_tac/induct_tac: use same declarations as cases/induct;
wenzelm
parents:
27103
diff
changeset

895 
induct} attributes, cf.\ \secref{sec:casesinduct}. The @{command 
11fcdd5897dd
case_tac/induct_tac: use same declarations as cases/induct;
wenzelm
parents:
27103
diff
changeset

896 
(HOL) datatype} package already takes care of this. 
11fcdd5897dd
case_tac/induct_tac: use same declarations as cases/induct;
wenzelm
parents:
27103
diff
changeset

897 

11fcdd5897dd
case_tac/induct_tac: use same declarations as cases/induct;
wenzelm
parents:
27103
diff
changeset

898 
These unstructured tactics feature both goal addressing and dynamic 
26849  899 
instantiation. Note that named rule cases are \emph{not} provided 
27123
11fcdd5897dd
case_tac/induct_tac: use same declarations as cases/induct;
wenzelm
parents:
27103
diff
changeset

900 
as would be by the proper @{method cases} and @{method induct} proof 
11fcdd5897dd
case_tac/induct_tac: use same declarations as cases/induct;
wenzelm
parents:
27103
diff
changeset

901 
methods (see \secref{sec:casesinduct}). Unlike the @{method 
11fcdd5897dd
case_tac/induct_tac: use same declarations as cases/induct;
wenzelm
parents:
27103
diff
changeset

902 
induct} method, @{method induct_tac} does not handle structured rule 
11fcdd5897dd
case_tac/induct_tac: use same declarations as cases/induct;
wenzelm
parents:
27103
diff
changeset

903 
statements, only the compact objectlogic conclusion of the subgoal 
11fcdd5897dd
case_tac/induct_tac: use same declarations as cases/induct;
wenzelm
parents:
27103
diff
changeset

904 
being addressed. 
26849  905 

906 
\item [@{method (HOL) ind_cases} and @{command (HOL) 

26860  907 
"inductive_cases"}] provide an interface to the internal @{ML_text 
908 
mk_cases} operation. Rules are simplified in an unrestricted 

909 
forward manner. 

26849  910 

911 
While @{method (HOL) ind_cases} is a proof method to apply the 

912 
result immediately as elimination rules, @{command (HOL) 

913 
"inductive_cases"} provides case split theorems at the theory level 

914 
for later use. The @{keyword "for"} argument of the @{method (HOL) 

915 
ind_cases} method allows to specify a list of variables that should 

916 
be generalized before applying the resulting rule. 

917 

918 
\end{descr} 

919 
*} 

920 

921 

922 
section {* Executable code *} 

923 

924 
text {* 

925 
Isabelle/Pure provides two generic frameworks to support code 

926 
generation from executable specifications. Isabelle/HOL 

927 
instantiates these mechanisms in a way that is amenable to enduser 

928 
applications. 

929 

930 
One framework generates code from both functional and relational 

931 
programs to SML. See \cite{isabelleHOL} for further information 

932 
(this actually covers the newstyle theory format as well). 

933 

934 
\begin{matharray}{rcl} 

935 
@{command_def (HOL) "value"}@{text "\<^sup>*"} & : & \isarkeep{theory~~proof} \\ 

936 
@{command_def (HOL) "code_module"} & : & \isartrans{theory}{theory} \\ 

937 
@{command_def (HOL) "code_library"} & : & \isartrans{theory}{theory} \\ 

938 
@{command_def (HOL) "consts_code"} & : & \isartrans{theory}{theory} \\ 

939 
@{command_def (HOL) "types_code"} & : & \isartrans{theory}{theory} \\ 

940 
@{attribute_def (HOL) code} & : & \isaratt \\ 

941 
\end{matharray} 

942 

943 
\begin{rail} 

944 
'value' term 

945 
; 

946 

947 
( 'code\_module'  'code\_library' ) modespec ? name ? \\ 

948 
( 'file' name ) ? ( 'imports' ( name + ) ) ? \\ 

949 
'contains' ( ( name '=' term ) +  term + ) 

950 
; 

951 

952 
modespec: '(' ( name * ) ')' 

953 
; 

954 

955 
'consts\_code' (codespec +) 

956 
; 

957 

958 
codespec: const template attachment ? 

959 
; 

960 

961 
'types\_code' (tycodespec +) 

962 
; 

963 

964 
tycodespec: name template attachment ? 

965 
; 

966 

967 
const: term 

968 
; 

969 

970 
template: '(' string ')' 

971 
; 

972 

973 
attachment: 'attach' modespec ? verblbrace text verbrbrace 

974 
; 

975 

976 
'code' (name)? 

977 
; 

978 
\end{rail} 

979 

980 
\begin{descr} 

981 

982 
\item [@{command (HOL) "value"}~@{text t}] evaluates and prints a 

983 
term using the code generator. 

984 

985 
\end{descr} 

986 

987 
\medskip The other framework generates code from functional programs 

988 
(including overloading using type classes) to SML \cite{SML}, OCaml 

989 
\cite{OCaml} and Haskell \cite{haskellrevisedreport}. 

990 
Conceptually, code generation is split up in three steps: 

991 
\emph{selection} of code theorems, \emph{translation} into an 

992 
abstract executable view and \emph{serialization} to a specific 

993 
\emph{target language}. See \cite{isabellecodegen} for an 

994 
introduction on how to use it. 

995 

996 
\begin{matharray}{rcl} 

997 
@{command_def (HOL) "export_code"}@{text "\<^sup>*"} & : & \isarkeep{theory~~proof} \\ 

998 
@{command_def (HOL) "code_thms"}@{text "\<^sup>*"} & : & \isarkeep{theory~~proof} \\ 

999 
@{command_def (HOL) "code_deps"}@{text "\<^sup>*"} & : & \isarkeep{theory~~proof} \\ 

1000 
@{command_def (HOL) "code_datatype"} & : & \isartrans{theory}{theory} \\ 

1001 
@{command_def (HOL) "code_const"} & : & \isartrans{theory}{theory} \\ 

1002 
@{command_def (HOL) "code_type"} & : & \isartrans{theory}{theory} \\ 

1003 
@{command_def (HOL) "code_class"} & : & \isartrans{theory}{theory} \\ 

1004 
@{command_def (HOL) "code_instance"} & : & \isartrans{theory}{theory} \\ 

1005 
@{command_def (HOL) "code_monad"} & : & \isartrans{theory}{theory} \\ 

1006 
@{command_def (HOL) "code_reserved"} & : & \isartrans{theory}{theory} \\ 

1007 
@{command_def (HOL) "code_include"} & : & \isartrans{theory}{theory} \\ 

1008 
@{command_def (HOL) "code_modulename"} & : & \isartrans{theory}{theory} \\ 

27103  1009 
@{command_def (HOL) "code_abort"} & : & \isartrans{theory}{theory} \\ 
26849  1010 
@{command_def (HOL) "print_codesetup"}@{text "\<^sup>*"} & : & \isarkeep{theory~~proof} \\ 
1011 
@{attribute_def (HOL) code} & : & \isaratt \\ 

1012 
\end{matharray} 

1013 

1014 
\begin{rail} 

1015 
'export\_code' ( constexpr + ) ? \\ 

1016 
( ( 'in' target ( 'module\_name' string ) ? \\ 

1017 
( 'file' ( string  '' ) ) ? ( '(' args ')' ) ?) + ) ? 

1018 
; 

1019 

1020 
'code\_thms' ( constexpr + ) ? 

1021 
; 

1022 

1023 
'code\_deps' ( constexpr + ) ? 

1024 
; 

1025 

1026 
const: term 

1027 
; 

1028 

1029 
constexpr: ( const  'name.*'  '*' ) 

1030 
; 

1031 

1032 
typeconstructor: nameref 

1033 
; 

1034 

1035 
class: nameref 

1036 
; 

1037 

1038 
target: 'OCaml'  'SML'  'Haskell' 

1039 
; 

1040 

1041 
'code\_datatype' const + 

1042 
; 

1043 

1044 
'code\_const' (const + 'and') \\ 

1045 
( ( '(' target ( syntax ? + 'and' ) ')' ) + ) 

1046 
; 

1047 

1048 
'code\_type' (typeconstructor + 'and') \\ 

1049 
( ( '(' target ( syntax ? + 'and' ) ')' ) + ) 

1050 
; 

1051 

1052 
'code\_class' (class + 'and') \\ 

1053 
( ( '(' target \\ 

1054 
( ( string ('where' \\ 

1055 
( const ( '=='  equiv ) string ) + ) ? ) ? + 'and' ) ')' ) + ) 

1056 
; 

1057 

1058 
'code\_instance' (( typeconstructor '::' class ) + 'and') \\ 

1059 
( ( '(' target ( '' ? + 'and' ) ')' ) + ) 

1060 
; 

1061 

1062 
'code\_monad' const const target 

1063 
; 

1064 

1065 
'code\_reserved' target ( string + ) 

1066 
; 

1067 

1068 
'code\_include' target ( string ( string  '') ) 

1069 
; 

1070 

1071 
'code\_modulename' target ( ( string string ) + ) 

1072 
; 

1073 

27452  1074 
'code\_abort' ( const + ) 
26849  1075 
; 
1076 

1077 
syntax: string  ( 'infix'  'infixl'  'infixr' ) nat string 

1078 
; 

1079 

28562  1080 
'code' ( 'inline' ) ? ( 'del' ) ? 
26849  1081 
; 
1082 
\end{rail} 

1083 

1084 
\begin{descr} 

1085 

1086 
\item [@{command (HOL) "export_code"}] is the canonical interface 

1087 
for generating and serializing code: for a given list of constants, 

1088 
code is generated for the specified target languages. Abstract code 

1089 
is cached incrementally. If no constant is given, the currently 

1090 
cached code is serialized. If no serialization instruction is 

1091 
given, only abstract code is cached. 

1092 

1093 
Constants may be specified by giving them literally, referring to 

1094 
all executable contants within a certain theory by giving @{text 

1095 
"name.*"}, or referring to \emph{all} executable constants currently 

1096 
available by giving @{text "*"}. 

1097 

1098 
By default, for each involved theory one corresponding name space 

1099 
module is generated. Alternativly, a module name may be specified 

1100 
after the @{keyword "module_name"} keyword; then \emph{all} code is 

1101 
placed in this module. 

1102 

1103 
For \emph{SML} and \emph{OCaml}, the file specification refers to a 

1104 
single file; for \emph{Haskell}, it refers to a whole directory, 

1105 
where code is generated in multiple files reflecting the module 

1106 
hierarchy. The file specification ``@{text ""}'' denotes standard 

1107 
output. For \emph{SML}, omitting the file specification compiles 

1108 
code internally in the context of the current ML session. 

1109 

1110 
Serializers take an optional list of arguments in parentheses. For 

1111 
\emph{Haskell} a module name prefix may be given using the ``@{text 

1112 
"root:"}'' argument; ``@{text string_classes}'' adds a ``@{verbatim 

1113 
"deriving (Read, Show)"}'' clause to each appropriate datatype 

1114 
declaration. 

1115 

1116 
\item [@{command (HOL) "code_thms"}] prints a list of theorems 

1117 
representing the corresponding program containing all given 

1118 
constants; if no constants are given, the currently cached code 

1119 
theorems are printed. 

1120 

1121 
\item [@{command (HOL) "code_deps"}] visualizes dependencies of 

1122 
theorems representing the corresponding program containing all given 

1123 
constants; if no constants are given, the currently cached code 

1124 
theorems are visualized. 

1125 

1126 
\item [@{command (HOL) "code_datatype"}] specifies a constructor set 

1127 
for a logical type. 

1128 

1129 
\item [@{command (HOL) "code_const"}] associates a list of constants 

1130 
with targetspecific serializations; omitting a serialization 

1131 
deletes an existing serialization. 

1132 

1133 
\item [@{command (HOL) "code_type"}] associates a list of type 

1134 
constructors with targetspecific serializations; omitting a 

1135 
serialization deletes an existing serialization. 

1136 

1137 
\item [@{command (HOL) "code_class"}] associates a list of classes 

1138 
with targetspecific class names; in addition, constants associated 

1139 
with this class may be given targetspecific names used for instance 

1140 
declarations; omitting a serialization deletes an existing 

1141 
serialization. This applies only to \emph{Haskell}. 

1142 

1143 
\item [@{command (HOL) "code_instance"}] declares a list of type 

1144 
constructor / class instance relations as ``already present'' for a 

1145 
given target. Omitting a ``@{text ""}'' deletes an existing 

1146 
``already present'' declaration. This applies only to 

1147 
\emph{Haskell}. 

1148 

1149 
\item [@{command (HOL) "code_monad"}] provides an auxiliary 

27706  1150 
mechanism to generate monadic code for Haskell. 
26849  1151 

1152 
\item [@{command (HOL) "code_reserved"}] declares a list of names as 

1153 
reserved for a given target, preventing it to be shadowed by any 

1154 
generated code. 

1155 

1156 
\item [@{command (HOL) "code_include"}] adds arbitrary named content 

27706  1157 
(``include'') to generated code. A ``@{text ""}'' as last argument 
26849  1158 
will remove an already added ``include''. 
1159 

1160 
\item [@{command (HOL) "code_modulename"}] declares aliasings from 

1161 
one module name onto another. 

1162 

27103  1163 
\item [@{command (HOL) "code_abort"}] declares constants which 
27452  1164 
are not required to have a definition by means of defining equations; 
27103  1165 
if needed these are implemented by program abort instead. 
26849  1166 

28562  1167 
\item [@{attribute (HOL) code}] explicitly selects (or 
1168 
with option ``@{text "del"}'' deselects) a defining equation for 

26849  1169 
code generation. Usually packages introducing defining equations 
27452  1170 
provide a reasonable default setup for selection. 
26849  1171 

1172 
\item [@{attribute (HOL) code}@{text inline}] declares (or with 

28562  1173 
option ``@{text "del"}'' removes) inlining theorems which are 
26849  1174 
applied as rewrite rules to any defining equation during 
1175 
preprocessing. 

1176 

1177 
\item [@{command (HOL) "print_codesetup"}] gives an overview on 

1178 
selected defining equations, code generator datatypes and 

1179 
preprocessor setup. 

1180 

1181 
\end{descr} 

1182 
*} 

1183 

27045  1184 

1185 
section {* Definition by specification \label{sec:holspecification} *} 

1186 

1187 
text {* 

1188 
\begin{matharray}{rcl} 

1189 
@{command_def (HOL) "specification"} & : & \isartrans{theory}{proof(prove)} \\ 

1190 
@{command_def (HOL) "ax_specification"} & : & \isartrans{theory}{proof(prove)} \\ 

1191 
\end{matharray} 

1192 

1193 
\begin{rail} 

1194 
('specification'  'ax\_specification') '(' (decl +) ')' \\ (thmdecl? prop +) 

1195 
; 

1196 
decl: ((name ':')? term '(' 'overloaded' ')'?) 

1197 
\end{rail} 

1198 

1199 
\begin{descr} 

1200 

1201 
\item [@{command (HOL) "specification"}~@{text "decls \<phi>"}] sets up a 

1202 
goal stating the existence of terms with the properties specified to 

1203 
hold for the constants given in @{text decls}. After finishing the 

1204 
proof, the theory will be augmented with definitions for the given 

1205 
constants, as well as with theorems stating the properties for these 

1206 
constants. 

1207 

1208 
\item [@{command (HOL) "ax_specification"}~@{text "decls \<phi>"}] sets 

1209 
up a goal stating the existence of terms with the properties 

1210 
specified to hold for the constants given in @{text decls}. After 

1211 
finishing the proof, the theory will be augmented with axioms 

1212 
expressing the properties given in the first place. 

1213 

1214 
\item [@{text decl}] declares a constant to be defined by the 

1215 
specification given. The definition for the constant @{text c} is 

1216 
bound to the name @{text c_def} unless a theorem name is given in 

1217 
the declaration. Overloaded constants should be declared as such. 

1218 

1219 
\end{descr} 

1220 

1221 
Whether to use @{command (HOL) "specification"} or @{command (HOL) 

1222 
"ax_specification"} is to some extent a matter of style. @{command 

1223 
(HOL) "specification"} introduces no new axioms, and so by 

1224 
construction cannot introduce inconsistencies, whereas @{command 

1225 
(HOL) "ax_specification"} does introduce axioms, but only after the 

1226 
user has explicitly proven it to be safe. A practical issue must be 

1227 
considered, though: After introducing two constants with the same 

1228 
properties using @{command (HOL) "specification"}, one can prove 

1229 
that the two constants are, in fact, equal. If this might be a 

1230 
problem, one should use @{command (HOL) "ax_specification"}. 

1231 
*} 

1232 

26840  1233 
end 