author  wenzelm 
Mon, 15 Dec 2008 21:54:37 +0100  
changeset 29114  715178f6ae31 
parent 29112  f2b45eea6dac 
child 29560  fa6c5d62adf5 
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} 

28761
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset

13 
@{command_def (HOL) "typedecl"} & : & @{text "theory \<rightarrow> theory"} \\ 
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset

14 
@{command_def (HOL) "typedef"} & : & @{text "theory \<rightarrow> proof(prove)"} \\ 
26849  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 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28752
diff
changeset

31 
\begin{description} 
26849  32 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28752
diff
changeset

33 
\item @{command (HOL) "typedecl"}~@{text "(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>n) t"} is similar 
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28752
diff
changeset

34 
to the original @{command "typedecl"} of Isabelle/Pure (see 
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28752
diff
changeset

35 
\secref{sec:typespure}), but also declares type arity @{text "t :: 
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28752
diff
changeset

36 
(type, \<dots>, type) type"}, making @{text t} an actual HOL type 
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28752
diff
changeset

37 
constructor. %FIXME check, update 
26849  38 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28752
diff
changeset

39 
\item @{command (HOL) "typedef"}~@{text "(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>n) t = A"} sets up 
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28752
diff
changeset

40 
a goal stating nonemptiness of the set @{text A}. After finishing 
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28752
diff
changeset

41 
the proof, the theory will be augmented by a Gordon/HOLstyle type 
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28752
diff
changeset

42 
definition, which establishes a bijection between the representing 
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28752
diff
changeset

43 
set @{text A} and the new type @{text t}. 
26849  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 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28752
diff
changeset

67 
\end{description} 
26849  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} 

28761
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset

82 
@{attribute (HOL) split_format}@{text "\<^sup>*"} & : & @{text attribute} \\ 
26849  83 
\end{matharray} 
84 

85 
\begin{rail} 

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

87 
; 

88 
\end{rail} 

89 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28752
diff
changeset

90 
\begin{description} 
26849  91 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28752
diff
changeset

92 
\item @{attribute (HOL) split_format}~@{text "p\<^sub>1 \<dots> p\<^sub>m \<AND> \<dots> 
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28752
diff
changeset

93 
\<AND> q\<^sub>1 \<dots> q\<^sub>n"} puts expressions of lowlevel tuple types into 
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28752
diff
changeset

94 
canonical form as specified by the arguments given; the @{text i}th 
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28752
diff
changeset

95 
collection of arguments refers to occurrences in premise @{text i} 
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28752
diff
changeset

96 
of the rule. The ``@{text "(complete)"}'' option causes \emph{all} 
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28752
diff
changeset

97 
arguments in function applications to be represented canonically 
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28752
diff
changeset

98 
according to their tuple type structure. 
26849  99 

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

101 
parameters to be introduced. 

102 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28752
diff
changeset

103 
\end{description} 
26849  104 
*} 
105 

106 

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

108 

109 
text {* 

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

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

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

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

114 
admits operations that are polymorphic with respect to record 

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

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

117 
details on objectoriented verification and record subtyping in HOL. 

118 
*} 

119 

120 

121 
subsection {* Basic concepts *} 

122 

123 
text {* 

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

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

126 

127 
\begin{center} 

128 
\begin{tabular}{lll} 

129 
& record terms & record types \\ \hline 

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

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

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

133 
\end{tabular} 

134 
\end{center} 

135 

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

137 
"( x = a )"}. 

138 

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

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

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

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

143 

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

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

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

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

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

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

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

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

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

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

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

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

158 

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

160 
typed language like HOL work out: 

161 

162 
\begin{enumerate} 

163 

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

165 
variable, 

166 

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

26849  169 

170 
\end{enumerate} 

171 

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

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

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

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

176 
The record package provides several standard operations like 

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

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

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

180 
records in practice. 

181 
*} 

182 

183 

184 
subsection {* Record specifications *} 

185 

186 
text {* 

187 
\begin{matharray}{rcl} 

28761
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset

188 
@{command_def (HOL) "record"} & : & @{text "theory \<rightarrow> theory"} \\ 
26849  189 
\end{matharray} 
190 

191 
\begin{rail} 

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

193 
; 

194 
\end{rail} 

195 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28752
diff
changeset

196 
\begin{description} 
26849  197 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28752
diff
changeset

198 
\item @{command (HOL) "record"}~@{text "(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>m) t = \<tau> + c\<^sub>1 :: \<sigma>\<^sub>1 
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28752
diff
changeset

199 
\<dots> c\<^sub>n :: \<sigma>\<^sub>n"} defines extensible record type @{text "(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>m) t"}, 
26849  200 
derived from the optional parent record @{text "\<tau>"} by adding new 
201 
field components @{text "c\<^sub>i :: \<sigma>\<^sub>i"} etc. 

202 

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

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

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

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

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

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

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

210 
the record name internally. 

211 

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

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

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

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

216 
merge multiple parent records! 

217 

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

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

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

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

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

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

224 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28752
diff
changeset

225 
\end{description} 
26849  226 
*} 
227 

228 

229 
subsection {* Record operations *} 

230 

231 
text {* 

232 
Any record definition of the form presented above produces certain 

233 
standard operations. Selectors and updates are provided for any 

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

235 
cumulative record constructor functions. To simplify the 

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

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

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

239 

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

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

242 

243 
\begin{matharray}{lll} 

26852  244 
@{text "c\<^sub>i"} & @{text "::"} & @{text "\<lparr>\<^vec>c :: \<^vec>\<sigma>, \<dots> :: \<zeta>\<rparr> \<Rightarrow> \<sigma>\<^sub>i"} \\ 
245 
@{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  246 
\end{matharray} 
247 

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

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

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

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

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

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

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

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

256 
Thus commutativity of independent updates can be proven within the 

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

258 

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

260 
constructor function: 

261 

262 
\begin{matharray}{lll} 

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

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

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

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

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

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

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

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

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

274 
the above record operations will get the following types: 

275 

26852  276 
\medskip 
277 
\begin{tabular}{lll} 

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

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

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

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

284 
\end{tabular} 

285 
\medskip 

26849  286 

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

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

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

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

293 

26852  294 
\medskip 
295 
\begin{tabular}{lll} 

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

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

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

299 
@{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>"} \\ 

300 
\end{tabular} 

301 
\medskip 

26849  302 

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

304 
for root records. 

305 
*} 

306 

307 

308 
subsection {* Derived rules and proof tools *} 

309 

310 
text {* 

311 
The record package proves several results internally, declaring 

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

313 
reason about record structures quite conveniently. Assume that 

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

315 

316 
\begin{enumerate} 

317 

318 
\item Standard conversions for selectors or updates applied to 

319 
record constructor terms are made part of the default Simplifier 

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

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

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

323 

324 
\item Selectors applied to updated records are automatically reduced 

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

326 
standard Simplifier setup. 

327 

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

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

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

331 
@{text "t.iffs"}. 

332 

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

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

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

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

337 

338 
\item Representations of arbitrary record expressions as canonical 

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

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

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

342 
fixed records, record schemes, more parts etc. 

343 

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

345 
sensible rule according to the type of the indicated record 

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

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

348 

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

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

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

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

353 

354 
\end{enumerate} 

355 
*} 

356 

357 

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

359 

360 
text {* 

361 
\begin{matharray}{rcl} 

28761
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset

362 
@{command_def (HOL) "datatype"} & : & @{text "theory \<rightarrow> theory"} \\ 
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset

363 
@{command_def (HOL) "rep_datatype"} & : & @{text "theory \<rightarrow> proof(prove)"} \\ 
26849  364 
\end{matharray} 
365 

366 
\begin{rail} 

367 
'datatype' (dtspec + 'and') 

368 
; 

27452  369 
'rep\_datatype' ('(' (name +) ')')? (term +) 
26849  370 
; 
371 

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

373 
; 

374 
cons: name (type *) mixfix? 

375 
\end{rail} 

376 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28752
diff
changeset

377 
\begin{description} 
26849  378 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28752
diff
changeset

379 
\item @{command (HOL) "datatype"} defines inductive datatypes in 
26849  380 
HOL. 
381 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28752
diff
changeset

382 
\item @{command (HOL) "rep_datatype"} represents existing types as 
26849  383 
inductive ones, generating the standard infrastructure of derived 
384 
concepts (primitive recursion etc.). 

385 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28752
diff
changeset

386 
\end{description} 
26849  387 

388 
The induction and exhaustion theorems generated provide case names 

389 
according to the constructors involved, while parameters are named 

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

391 

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

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

394 
proof methods for caseanalysis and induction, there are also 

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

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

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

398 
internally bound parameters). 

399 
*} 

400 

401 

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

403 

404 
text {* 

405 
\begin{matharray}{rcl} 

28761
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset

406 
@{command_def (HOL) "primrec"} & : & @{text "local_theory \<rightarrow> local_theory"} \\ 
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset

407 
@{command_def (HOL) "fun"} & : & @{text "local_theory \<rightarrow> local_theory"} \\ 
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset

408 
@{command_def (HOL) "function"} & : & @{text "local_theory \<rightarrow> proof(prove)"} \\ 
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset

409 
@{command_def (HOL) "termination"} & : & @{text "local_theory \<rightarrow> proof(prove)"} \\ 
26849  410 
\end{matharray} 
411 

412 
\begin{rail} 

413 
'primrec' target? fixes 'where' equations 

414 
; 

415 
equations: (thmdecl? prop + '') 

416 
; 

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

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

420 
; 

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

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

424 
\end{rail} 

425 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28752
diff
changeset

426 
\begin{description} 
26849  427 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28752
diff
changeset

428 
\item @{command (HOL) "primrec"} defines primitive recursive 
26849  429 
functions over datatypes, see also \cite{isabelleHOL}. 
430 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28752
diff
changeset

431 
\item @{command (HOL) "function"} defines functions by general 
26849  432 
wellfounded recursion. A detailed description with examples can be 
433 
found in \cite{isabellefunction}. The function is specified by a 

434 
set of (possibly conditional) recursive equations with arbitrary 

435 
pattern matching. The command generates proof obligations for the 

436 
completeness and the compatibility of patterns. 

437 

438 
The defined function is considered partial, and the resulting 

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

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

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

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

443 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28752
diff
changeset

444 
\item @{command (HOL) "fun"} is a shorthand notation for ``@{command 
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28752
diff
changeset

445 
(HOL) "function"}~@{text "(sequential)"}, followed by automated 
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28752
diff
changeset

446 
proof attempts regarding pattern matching and termination. See 
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28752
diff
changeset

447 
\cite{isabellefunction} for further details. 
26849  448 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28752
diff
changeset

449 
\item @{command (HOL) "termination"}~@{text f} commences a 
26849  450 
termination proof for the previously defined function @{text f}. If 
451 
this is omitted, the command refers to the most recent function 

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

453 
the induction principle is established. 

454 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28752
diff
changeset

455 
\end{description} 
26849  456 

457 
%FIXME check 

458 

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

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

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

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

466 
with structural recursion on the datatype the recursion is carried 

467 
out. 

468 
Case names of @{command (HOL) 

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

471 

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

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

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

475 
explicitly as well. 

476 

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

478 
options. 

479 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28752
diff
changeset

480 
\begin{description} 
26849  481 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28752
diff
changeset

482 
\item @{text sequential} enables a preprocessor which disambiguates 
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28752
diff
changeset

483 
overlapping patterns by making them mutually disjoint. Earlier 
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28752
diff
changeset

484 
equations take precedence over later ones. This allows to give the 
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28752
diff
changeset

485 
specification in a format very similar to functional programming. 
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28752
diff
changeset

486 
Note that the resulting simplification and induction rules 
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28752
diff
changeset

487 
correspond to the transformed specification, not the one given 
26849  488 
originally. This usually means that each equation given by the user 
489 
may result in several theroems. Also note that this automatic 

490 
transformation only works for MLstyle datatype patterns. 

491 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28752
diff
changeset

492 
\item @{text domintros} enables the automated generation of 
26849  493 
introduction rules for the domain predicate. While mostly not 
494 
needed, they can be helpful in some proofs about partial functions. 

495 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28752
diff
changeset

496 
\item @{text tailrec} generates the unconstrained recursive 
26849  497 
equations even without a termination proof, provided that the 
498 
function is tailrecursive. This currently only works 

499 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28752
diff
changeset

500 
\item @{text "default d"} allows to specify a default value for a 
26849  501 
(partial) function, which will ensure that @{text "f x = d x"} 
502 
whenever @{text "x \<notin> f_dom"}. 

503 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28752
diff
changeset

504 
\end{description} 
26849  505 
*} 
506 

507 

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

509 

510 
text {* 

511 
\begin{matharray}{rcl} 

28761
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset

512 
@{method_def (HOL) pat_completeness} & : & @{text method} \\ 
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset

513 
@{method_def (HOL) relation} & : & @{text method} \\ 
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset

514 
@{method_def (HOL) lexicographic_order} & : & @{text method} \\ 
26849  515 
\end{matharray} 
516 

517 
\begin{rail} 

518 
'relation' term 

519 
; 

520 
'lexicographic\_order' (clasimpmod *) 

521 
; 

522 
\end{rail} 

523 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28752
diff
changeset

524 
\begin{description} 
26849  525 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28752
diff
changeset

526 
\item @{method (HOL) pat_completeness} is a specialized method to 
26849  527 
solve goals regarding the completeness of pattern matching, as 
528 
required by the @{command (HOL) "function"} package (cf.\ 

529 
\cite{isabellefunction}). 

530 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28752
diff
changeset

531 
\item @{method (HOL) relation}~@{text R} introduces a termination 
26849  532 
proof using the relation @{text R}. The resulting proof state will 
533 
contain goals expressing that @{text R} is wellfounded, and that the 

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

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

536 
termination proofs. 

537 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28752
diff
changeset

538 
\item @{method (HOL) "lexicographic_order"} attempts a fully 
26849  539 
automated termination proof by searching for a lexicographic 
540 
combination of size measures on the arguments of the function. The 

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

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

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

544 
\secref{sec:clasimp}. 

545 

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

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

548 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28752
diff
changeset

549 
\end{description} 
26849  550 
*} 
551 

552 

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

554 

555 
text {* 

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

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

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

559 

560 
\begin{matharray}{rcl} 

28761
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset

561 
@{command_def (HOL) "recdef"} & : & @{text "theory \<rightarrow> theory)"} \\ 
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset

562 
@{command_def (HOL) "recdef_tc"}@{text "\<^sup>*"} & : & @{text "theory \<rightarrow> proof(prove)"} \\ 
26849  563 
\end{matharray} 
564 

565 
\begin{rail} 

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

567 
; 

568 
recdeftc thmdecl? tc 

569 
; 

570 
hints: '(' 'hints' (recdefmod *) ')' 

571 
; 

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

573 
; 

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

575 
; 

576 
\end{rail} 

577 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28752
diff
changeset

578 
\begin{description} 
26849  579 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28752
diff
changeset

580 
\item @{command (HOL) "recdef"} defines general wellfounded 
26849  581 
recursive functions (using the TFL package), see also 
582 
\cite{isabelleHOL}. The ``@{text "(permissive)"}'' option tells 

583 
TFL to recover from failed proof attempts, returning unfinished 

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

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

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

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

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

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

590 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28752
diff
changeset

591 
\item @{command (HOL) "recdef_tc"}~@{text "c (i)"} recommences the 
26849  592 
proof for leftover termination condition number @{text i} (default 
593 
1) as generated by a @{command (HOL) "recdef"} definition of 

594 
constant @{text c}. 

595 

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

597 
its internal proofs without manual intervention. 

598 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28752
diff
changeset

599 
\end{description} 
26849  600 

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

602 
globally, using the following attributes. 

603 

604 
\begin{matharray}{rcl} 

28761
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset

605 
@{attribute_def (HOL) recdef_simp} & : & @{text attribute} \\ 
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset

606 
@{attribute_def (HOL) recdef_cong} & : & @{text attribute} \\ 
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset

607 
@{attribute_def (HOL) recdef_wf} & : & @{text attribute} \\ 
26849  608 
\end{matharray} 
609 

610 
\begin{rail} 

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

612 
; 

613 
\end{rail} 

614 
*} 

615 

616 

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

618 

619 
text {* 

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

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

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

623 
structural operational semantics is an inductive definition of an 

624 
evaluation relation. 

625 

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

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

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

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

630 
relations to formalise equivalence of processes and infinite data 

631 
structures. 

632 

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

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

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

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

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

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

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

640 
to use inference rules for typechecking. 

641 

642 
\begin{matharray}{rcl} 

28761
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset

643 
@{command_def (HOL) "inductive"} & : & @{text "local_theory \<rightarrow> local_theory"} \\ 
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset

644 
@{command_def (HOL) "inductive_set"} & : & @{text "local_theory \<rightarrow> local_theory"} \\ 
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset

645 
@{command_def (HOL) "coinductive"} & : & @{text "local_theory \<rightarrow> local_theory"} \\ 
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset

646 
@{command_def (HOL) "coinductive_set"} & : & @{text "local_theory \<rightarrow> local_theory"} \\ 
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset

647 
@{attribute_def (HOL) mono} & : & @{text attribute} \\ 
26849  648 
\end{matharray} 
649 

650 
\begin{rail} 

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

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

653 
; 

654 
clauses: (thmdecl? prop + '') 

655 
; 

656 
'mono' (()  'add'  'del') 

657 
; 

658 
\end{rail} 

659 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28752
diff
changeset

660 
\begin{description} 
26849  661 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28752
diff
changeset

662 
\item @{command (HOL) "inductive"} and @{command (HOL) 
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28752
diff
changeset

663 
"coinductive"} define (co)inductive predicates from the 
26849  664 
introduction rules given in the @{keyword "where"} part. The 
665 
optional @{keyword "for"} part contains a list of parameters of the 

666 
(co)inductive predicates that remain fixed throughout the 

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

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

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

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

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

672 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28752
diff
changeset

673 
\item @{command (HOL) "inductive_set"} and @{command (HOL) 
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28752
diff
changeset

674 
"coinductive_set"} are wrappers for to the previous commands, 
26849  675 
allowing the definition of (co)inductive sets. 
676 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28752
diff
changeset

677 
\item @{attribute (HOL) mono} declares monotonicity rules. These 
26849  678 
rule are involved in the automated monotonicity proof of @{command 
679 
(HOL) "inductive"}. 

680 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28752
diff
changeset

681 
\end{description} 
26849  682 
*} 
683 

684 

685 
subsection {* Derived rules *} 

686 

687 
text {* 

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

689 
theory and also proves some theorems: 

690 

691 
\begin{description} 

692 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28752
diff
changeset

693 
\item @{text R.intros} is the list of introduction rules as proven 
26849  694 
theorems, for the recursive predicates (or sets). The rules are 
695 
also available individually, using the names given them in the 

696 
theory file; 

697 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28752
diff
changeset

698 
\item @{text R.cases} is the case analysis (or elimination) rule; 
26849  699 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28752
diff
changeset

700 
\item @{text R.induct} or @{text R.coinduct} is the (co)induction 
26849  701 
rule. 
702 

703 
\end{description} 

704 

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

706 
defined simultaneously, the list of introduction rules is called 

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

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

709 
of mutual induction rules is called @{text 

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

711 
*} 

712 

713 

714 
subsection {* Monotonicity theorems *} 

715 

716 
text {* 

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

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

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

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

721 
theorems may be added: 

722 

723 
\begin{itemize} 

724 

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

726 
monotonicity of inductive definitions whose introduction rules have 

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

728 

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

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

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

732 
\[ 

733 
\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"}} 

734 
\] 

735 

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

737 
of expressions, e.g. 

738 
\[ 

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

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

741 
\] 

742 

743 
\item Equations for reducing complex operators to more primitive 

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

745 
\[ 

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

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

748 
\] 

749 

750 
\end{itemize} 

751 

752 
%FIXME: Example of an inductive definition 

753 
*} 

754 

755 

756 
section {* Arithmetic proof support *} 

757 

758 
text {* 

759 
\begin{matharray}{rcl} 

28761
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset

760 
@{method_def (HOL) arith} & : & @{text method} \\ 
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset

761 
@{attribute_def (HOL) arith_split} & : & @{text attribute} \\ 
26849  762 
\end{matharray} 
763 

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

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

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

767 

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

26849  770 

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

772 
already performed by the Simplifier. 

773 
*} 

774 

775 

28603  776 
section {* Invoking automated reasoning tools  The Sledgehammer *} 
777 

778 
text {* 

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

780 
external automated reasoning tools to crunch a pending goal. 

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

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

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

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

785 
web service. 

786 

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

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

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

790 
usually reconstructs the proof within Isabelle, without requiring 

791 
external provers again. The Metis 

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

793 
integrated into Isabelle/HOL is being used here. 

794 

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

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

797 
works via explicit inferences going through the Isabelle kernel. 

798 
Moreover, rechecking Isabelle proof texts with already specified 

799 
auxiliary facts is much faster than performing fully automated 

800 
search over and over again. 

801 

802 
\begin{matharray}{rcl} 

28761
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset

803 
@{command_def (HOL) "sledgehammer"}@{text "\<^sup>*"} & : & @{text "proof \<rightarrow>"} \\ 
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset

804 
@{command_def (HOL) "print_atps"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\ 
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset

805 
@{command_def (HOL) "atp_info"}@{text "\<^sup>*"} & : & @{text "any \<rightarrow>"} \\ 
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset

806 
@{command_def (HOL) "atp_kill"}@{text "\<^sup>*"} & : & @{text "any \<rightarrow>"} \\ 
29112
f2b45eea6dac
added 'atp_messages' command, which displays recent messages synchronously;
wenzelm
parents:
28761
diff
changeset

807 
@{command_def (HOL) "atp_messages"}@{text "\<^sup>*"} & : & @{text "any \<rightarrow>"} \\ 
28761
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset

808 
@{method_def (HOL) metis} & : & @{text method} \\ 
28603  809 
\end{matharray} 
810 

811 
\begin{rail} 

812 
'sledgehammer' (nameref *) 

813 
; 

29112
f2b45eea6dac
added 'atp_messages' command, which displays recent messages synchronously;
wenzelm
parents:
28761
diff
changeset

814 
'atp\_messages' ('(' nat ')')? 
29114  815 
; 
28603  816 

817 
'metis' thmrefs 

818 
; 

819 
\end{rail} 

820 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28752
diff
changeset

821 
\begin{description} 
28603  822 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28752
diff
changeset

823 
\item @{command (HOL) sledgehammer}~@{text "prover\<^sub>1 \<dots> prover\<^sub>n"} 
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28752
diff
changeset

824 
invokes the specified automated theorem provers on the first 
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28752
diff
changeset

825 
subgoal. Provers are run in parallel, the first successful result 
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28752
diff
changeset

826 
is displayed, and the other attempts are terminated. 
28603  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 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28752
diff
changeset

837 
\item @{command (HOL) print_atps} prints the list of automated 
28603  838 
theorem provers available to the @{command (HOL) sledgehammer} 
839 
command. 

840 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28752
diff
changeset

841 
\item @{command (HOL) atp_info} prints information about presently 
28603  842 
running provers, including elapsed runtime, and the remaining time 
843 
until timeout. 

844 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28752
diff
changeset

845 
\item @{command (HOL) atp_kill} terminates all presently running 
28603  846 
provers. 
847 

29112
f2b45eea6dac
added 'atp_messages' command, which displays recent messages synchronously;
wenzelm
parents:
28761
diff
changeset

848 
\item @{command (HOL) atp_messages} displays recent messages issued 
f2b45eea6dac
added 'atp_messages' command, which displays recent messages synchronously;
wenzelm
parents:
28761
diff
changeset

849 
by automated theorem provers. This allows to examine results that 
f2b45eea6dac
added 'atp_messages' command, which displays recent messages synchronously;
wenzelm
parents:
28761
diff
changeset

850 
might have got lost due to the asynchronous nature of default 
f2b45eea6dac
added 'atp_messages' command, which displays recent messages synchronously;
wenzelm
parents:
28761
diff
changeset

851 
@{command (HOL) sledgehammer} output. An optional message limit may 
f2b45eea6dac
added 'atp_messages' command, which displays recent messages synchronously;
wenzelm
parents:
28761
diff
changeset

852 
be specified (default 5). 
f2b45eea6dac
added 'atp_messages' command, which displays recent messages synchronously;
wenzelm
parents:
28761
diff
changeset

853 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28752
diff
changeset

854 
\item @{method (HOL) metis}~@{text "facts"} invokes the Metis prover 
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28752
diff
changeset

855 
with the given facts. Metis is an automated proof tool of medium 
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28752
diff
changeset

856 
strength, but is fully integrated into Isabelle/HOL, with explicit 
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28752
diff
changeset

857 
inferences going through the kernel. Thus its results are 
28603  858 
guaranteed to be ``correct by construction''. 
859 

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

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

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

863 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28752
diff
changeset

864 
\end{description} 
28603  865 
*} 
866 

867 

28752  868 
section {* Unstructured case analysis and induction \label{sec:holinducttac} *} 
26849  869 

870 
text {* 

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

871 
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

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

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

875 
\begin{matharray}{rcl} 

28761
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset

876 
@{method_def (HOL) case_tac}@{text "\<^sup>*"} & : & @{text method} \\ 
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset

877 
@{method_def (HOL) induct_tac}@{text "\<^sup>*"} & : & @{text method} \\ 
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset

878 
@{method_def (HOL) ind_cases}@{text "\<^sup>*"} & : & @{text method} \\ 
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset

879 
@{command_def (HOL) "inductive_cases"}@{text "\<^sup>*"} & : & @{text "local_theory \<rightarrow> local_theory"} \\ 
26849  880 
\end{matharray} 
881 

882 
\begin{rail} 

883 
'case\_tac' goalspec? term rule? 

884 
; 

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

886 
; 

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

888 
; 

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

890 
; 

891 

892 
rule: ('rule' ':' thmref) 

893 
; 

894 
\end{rail} 

895 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28752
diff
changeset

896 
\begin{description} 
26849  897 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28752
diff
changeset

898 
\item @{method (HOL) case_tac} and @{method (HOL) induct_tac} admit 
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28752
diff
changeset

899 
to reason about inductive types. Rules are selected according to 
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28752
diff
changeset

900 
the declarations by the @{attribute cases} and @{attribute induct} 
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28752
diff
changeset

901 
attributes, cf.\ \secref{sec:casesinduct}. The @{command (HOL) 
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28752
diff
changeset

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

903 

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

904 
These unstructured tactics feature both goal addressing and dynamic 
26849  905 
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

906 
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

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

908 
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

909 
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

910 
being addressed. 
26849  911 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28752
diff
changeset

912 
\item @{method (HOL) ind_cases} and @{command (HOL) 
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28752
diff
changeset

913 
"inductive_cases"} provide an interface to the internal @{ML_text 
26860  914 
mk_cases} operation. Rules are simplified in an unrestricted 
915 
forward manner. 

26849  916 

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

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

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

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

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

922 
be generalized before applying the resulting rule. 

923 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28752
diff
changeset

924 
\end{description} 
26849  925 
*} 
926 

927 

928 
section {* Executable code *} 

929 

930 
text {* 

931 
Isabelle/Pure provides two generic frameworks to support code 

932 
generation from executable specifications. Isabelle/HOL 

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

934 
applications. 

935 

936 
One framework generates code from both functional and relational 

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

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

939 

940 
\begin{matharray}{rcl} 

28761
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset

941 
@{command_def (HOL) "value"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\ 
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset

942 
@{command_def (HOL) "code_module"} & : & @{text "theory \<rightarrow> theory"} \\ 
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset

943 
@{command_def (HOL) "code_library"} & : & @{text "theory \<rightarrow> theory"} \\ 
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset

944 
@{command_def (HOL) "consts_code"} & : & @{text "theory \<rightarrow> theory"} \\ 
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset

945 
@{command_def (HOL) "types_code"} & : & @{text "theory \<rightarrow> theory"} \\ 
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset

946 
@{attribute_def (HOL) code} & : & @{text attribute} \\ 
26849  947 
\end{matharray} 
948 

949 
\begin{rail} 

950 
'value' term 

951 
; 

952 

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

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

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

956 
; 

957 

958 
modespec: '(' ( name * ) ')' 

959 
; 

960 

961 
'consts\_code' (codespec +) 

962 
; 

963 

964 
codespec: const template attachment ? 

965 
; 

966 

967 
'types\_code' (tycodespec +) 

968 
; 

969 

970 
tycodespec: name template attachment ? 

971 
; 

972 

973 
const: term 

974 
; 

975 

976 
template: '(' string ')' 

977 
; 

978 

979 
attachment: 'attach' modespec ? verblbrace text verbrbrace 

980 
; 

981 

982 
'code' (name)? 

983 
; 

984 
\end{rail} 

985 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28752
diff
changeset

986 
\begin{description} 
26849  987 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28752
diff
changeset

988 
\item @{command (HOL) "value"}~@{text t} evaluates and prints a term 
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28752
diff
changeset

989 
using the code generator. 
26849  990 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28752
diff
changeset

991 
\end{description} 
26849  992 

993 
\medskip The other framework generates code from functional programs 

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

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

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

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

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

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

1000 
introduction on how to use it. 

1001 

1002 
\begin{matharray}{rcl} 

28761
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset

1003 
@{command_def (HOL) "export_code"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\ 
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset

1004 
@{command_def (HOL) "code_thms"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\ 
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset

1005 
@{command_def (HOL) "code_deps"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\ 
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset

1006 
@{command_def (HOL) "code_datatype"} & : & @{text "theory \<rightarrow> theory"} \\ 
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset

1007 
@{command_def (HOL) "code_const"} & : & @{text "theory \<rightarrow> theory"} \\ 
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset

1008 
@{command_def (HOL) "code_type"} & : & @{text "theory \<rightarrow> theory"} \\ 
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset

1009 
@{command_def (HOL) "code_class"} & : & @{text "theory \<rightarrow> theory"} \\ 
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset

1010 
@{command_def (HOL) "code_instance"} & : & @{text "theory \<rightarrow> theory"} \\ 
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset

1011 
@{command_def (HOL) "code_monad"} & : & @{text "theory \<rightarrow> theory"} \\ 
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset

1012 
@{command_def (HOL) "code_reserved"} & : & @{text "theory \<rightarrow> theory"} \\ 
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset

1013 
@{command_def (HOL) "code_include"} & : & @{text "theory \<rightarrow> theory"} \\ 
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset

1014 
@{command_def (HOL) "code_modulename"} & : & @{text "theory \<rightarrow> theory"} \\ 
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset

1015 
@{command_def (HOL) "code_abort"} & : & @{text "theory \<rightarrow> theory"} \\ 
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset

1016 
@{command_def (HOL) "print_codesetup"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\ 
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset

1017 
@{attribute_def (HOL) code} & : & @{text attribute} \\ 
26849  1018 
\end{matharray} 
1019 

1020 
\begin{rail} 

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

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

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

1024 
; 

1025 

1026 
'code\_thms' ( constexpr + ) ? 

1027 
; 

1028 

1029 
'code\_deps' ( constexpr + ) ? 

1030 
; 

1031 

1032 
const: term 

1033 
; 

1034 

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

1036 
; 

1037 

1038 
typeconstructor: nameref 

1039 
; 

1040 

1041 
class: nameref 

1042 
; 

1043 

1044 
target: 'OCaml'  'SML'  'Haskell' 

1045 
; 

1046 

1047 
'code\_datatype' const + 

1048 
; 

1049 

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

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

1052 
; 

1053 

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

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

1056 
; 

1057 

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

28687  1059 
( ( '(' target \\ ( string ? + 'and' ) ')' ) + ) 
26849  1060 
; 
1061 

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

1063 
( ( '(' target ( '' ? + 'and' ) ')' ) + ) 

1064 
; 

1065 

1066 
'code\_monad' const const target 

1067 
; 

1068 

1069 
'code\_reserved' target ( string + ) 

1070 
; 

1071 

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

1073 
; 

1074 

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

1076 
; 

1077 

27452  1078 
'code\_abort' ( const + ) 
26849  1079 
; 
1080 

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

1082 
; 

1083 

28562  1084 
'code' ( 'inline' ) ? ( 'del' ) ? 
26849  1085 
; 
1086 
\end{rail} 

1087 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28752
diff
changeset

1088 
\begin{description} 
26849  1089 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28752
diff
changeset

1090 
\item @{command (HOL) "export_code"} is the canonical interface for 
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28752
diff
changeset

1091 
generating and serializing code: for a given list of constants, code 
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28752
diff
changeset

1092 
is generated for the specified target languages. Abstract code is 
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28752
diff
changeset

1093 
cached incrementally. If no constant is given, the currently cached 
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28752
diff
changeset

1094 
code is serialized. If no serialization instruction is given, only 
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28752
diff
changeset

1095 
abstract code is cached. 
26849  1096 

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

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

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

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

1101 

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

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

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

1105 
placed in this module. 

1106 

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

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

1109 
where code is generated in multiple files reflecting the module 

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

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

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

1113 

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

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

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

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

1118 
declaration. 

1119 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28752
diff
changeset

1120 
\item @{command (HOL) "code_thms"} prints a list of theorems 
26849  1121 
representing the corresponding program containing all given 
1122 
constants; if no constants are given, the currently cached code 

1123 
theorems are printed. 

1124 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28752
diff
changeset

1125 
\item @{command (HOL) "code_deps"} visualizes dependencies of 
26849  1126 
theorems representing the corresponding program containing all given 
1127 
constants; if no constants are given, the currently cached code 

1128 
theorems are visualized. 

1129 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28752
diff
changeset

1130 
\item @{command (HOL) "code_datatype"} specifies a constructor set 
26849  1131 
for a logical type. 
1132 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28752
diff
changeset

1133 
\item @{command (HOL) "code_const"} associates a list of constants 
26849  1134 
with targetspecific serializations; omitting a serialization 
1135 
deletes an existing serialization. 

1136 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28752
diff
changeset

1137 
\item @{command (HOL) "code_type"} associates a list of type 
26849  1138 
constructors with targetspecific serializations; omitting a 
1139 
serialization deletes an existing serialization. 

1140 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28752
diff
changeset

1141 
\item @{command (HOL) "code_class"} associates a list of classes 
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28752
diff
changeset

1142 
with targetspecific class names; omitting a serialization deletes 
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28752
diff
changeset

1143 
an existing serialization. This applies only to \emph{Haskell}. 
26849  1144 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28752
diff
changeset

1145 
\item @{command (HOL) "code_instance"} declares a list of type 
26849  1146 
constructor / class instance relations as ``already present'' for a 
1147 
given target. Omitting a ``@{text ""}'' deletes an existing 

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

1149 
\emph{Haskell}. 

1150 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28752
diff
changeset

1151 
\item @{command (HOL) "code_monad"} provides an auxiliary mechanism 
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28752
diff
changeset

1152 
to generate monadic code for Haskell. 
26849  1153 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28752
diff
changeset

1154 
\item @{command (HOL) "code_reserved"} declares a list of names as 
26849  1155 
reserved for a given target, preventing it to be shadowed by any 
1156 
generated code. 

1157 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28752
diff
changeset

1158 
\item @{command (HOL) "code_include"} adds arbitrary named content 
27706  1159 
(``include'') to generated code. A ``@{text ""}'' as last argument 
26849  1160 
will remove an already added ``include''. 
1161 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28752
diff
changeset

1162 
\item @{command (HOL) "code_modulename"} declares aliasings from one 
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28752
diff
changeset

1163 
module name onto another. 
26849  1164 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28752
diff
changeset

1165 
\item @{command (HOL) "code_abort"} declares constants which are not 
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28752
diff
changeset

1166 
required to have a definition by means of defining equations; if 
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28752
diff
changeset

1167 
needed these are implemented by program abort instead. 
26849  1168 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28752
diff
changeset

1169 
\item @{attribute (HOL) code} explicitly selects (or with option 
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28752
diff
changeset

1170 
``@{text "del"}'' deselects) a defining equation for code 
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28752
diff
changeset

1171 
generation. Usually packages introducing defining equations provide 
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28752
diff
changeset

1172 
a reasonable default setup for selection. 
26849  1173 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28752
diff
changeset

1174 
\item @{attribute (HOL) code}~@{text inline} declares (or with 
28562  1175 
option ``@{text "del"}'' removes) inlining theorems which are 
26849  1176 
applied as rewrite rules to any defining equation during 
1177 
preprocessing. 

1178 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28752
diff
changeset

1179 
\item @{command (HOL) "print_codesetup"} gives an overview on 
26849  1180 
selected defining equations, code generator datatypes and 
1181 
preprocessor setup. 

1182 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28752
diff
changeset

1183 
\end{description} 
26849  1184 
*} 
1185 

27045  1186 

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

1188 

1189 
text {* 

1190 
\begin{matharray}{rcl} 

28761
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset

1191 
@{command_def (HOL) "specification"} & : & @{text "theory \<rightarrow> proof(prove)"} \\ 
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset

1192 
@{command_def (HOL) "ax_specification"} & : & @{text "theory \<rightarrow> proof(prove)"} \\ 
27045  1193 
\end{matharray} 
1194 

1195 
\begin{rail} 

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

1197 
; 

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

1199 
\end{rail} 

1200 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28752
diff
changeset

1201 
\begin{description} 
27045  1202 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28752
diff
changeset

1203 
\item @{command (HOL) "specification"}~@{text "decls \<phi>"} sets up a 
27045  1204 
goal stating the existence of terms with the properties specified to 
1205 
hold for the constants given in @{text decls}. After finishing the 

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

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

1208 
constants. 

1209 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28752
diff
changeset

1210 
\item @{command (HOL) "ax_specification"}~@{text "decls \<phi>"} sets up 
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28752
diff
changeset

1211 
a goal stating the existence of terms with the properties specified 
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28752
diff
changeset

1212 
to hold for the constants given in @{text decls}. After finishing 
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28752
diff
changeset

1213 
the proof, the theory will be augmented with axioms expressing the 
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28752
diff
changeset

1214 
properties given in the first place. 
27045  1215 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28752
diff
changeset

1216 
\item @{text decl} declares a constant to be defined by the 
27045  1217 
specification given. The definition for the constant @{text c} is 
1218 
bound to the name @{text c_def} unless a theorem name is given in 

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

1220 

28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28752
diff
changeset

1221 
\end{description} 
27045  1222 

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

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

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

1226 
construction cannot introduce inconsistencies, whereas @{command 

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

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

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

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

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

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

1233 
*} 

1234 

26840  1235 
end 