author  haftmann 
Mon, 10 Mar 2008 21:51:43 +0100  
changeset 26245  00cbf41ba625 
parent 25872  69c32d6a88c7 
child 26746  b010007e9d31 
permissions  rwrr 
12621  1 

13048  2 
\chapter{Objectlogic specific elements}\label{ch:logics} 
12621  3 

4 
\section{General logic setup}\label{sec:objectlogic} 

5 

6 
\indexisarcmd{judgment} 

7 
\indexisarmeth{atomize}\indexisaratt{atomize} 

8 
\indexisaratt{ruleformat}\indexisaratt{rulify} 

9 

10 
\begin{matharray}{rcl} 

11 
\isarcmd{judgment} & : & \isartrans{theory}{theory} \\ 

12 
atomize & : & \isarmeth \\ 

13 
atomize & : & \isaratt \\ 

14 
rule_format & : & \isaratt \\ 

15 
rulify & : & \isaratt \\ 

16 
\end{matharray} 

17 

18 
The very starting point for any Isabelle objectlogic is a ``truth judgment'' 

19 
that links objectlevel statements to the metalogic (with its minimal 

20 
language of $prop$ that covers universal quantification $\Forall$ and 

13041  21 
implication $\Imp$). 
22 

23 
Common objectlogics are sufficiently expressive to internalize rule 

24 
statements over $\Forall$ and $\Imp$ within their own language. This is 

25 
useful in certain situations where a rule needs to be viewed as an atomic 

26 
statement from the metalevel perspective, e.g.\ $\All x x \in A \Imp P(x)$ 

27 
versus $\forall x \in A. P(x)$. 

12621  28 

29 
From the following language elements, only the $atomize$ method and 

30 
$rule_format$ attribute are occasionally required by endusers, the rest is 

31 
for those who need to setup their own objectlogic. In the latter case 

32 
existing formulations of Isabelle/FOL or Isabelle/HOL may be taken as 

33 
realistic examples. 

34 

35 
Generic tools may refer to the information provided by objectlogic 

13041  36 
declarations internally. 
37 

38 
\railalias{ruleformat}{rule\_format} 

39 
\railterm{ruleformat} 

12621  40 

41 
\begin{rail} 

42 
'judgment' constdecl 

43 
; 

13041  44 
'atomize' ('(' 'full' ')')? 
13014  45 
; 
46 
ruleformat ('(' 'noasm' ')')? 

12621  47 
; 
48 
\end{rail} 

49 

50 
\begin{descr} 

13041  51 

52 
\item [$\isarkeyword{judgment}~c::\sigma~~(mx)$] declares constant $c$ as the 

12621  53 
truth judgment of the current objectlogic. Its type $\sigma$ should 
54 
specify a coercion of the category of objectlevel propositions to $prop$ of 

13041  55 
the Pure metalogic; the mixfix annotation $(mx)$ would typically just link 
12621  56 
the object language (internally of syntactic category $logic$) with that of 
57 
$prop$. Only one $\isarkeyword{judgment}$ declaration may be given in any 

58 
theory development. 

13041  59 

12621  60 
\item [$atomize$] (as a method) rewrites any nonatomic premises of a 
61 
subgoal, using the metalevel equations declared via $atomize$ (as an 

62 
attribute) beforehand. As a result, heavily nested goals become amenable to 

63 
fundamental operations such as resolution (cf.\ the $rule$ method) and 

13014  64 
proofbyassumption (cf.\ $assumption$). Giving the ``$(full)$'' option 
13041  65 
here means to turn the whole subgoal into an objectstatement (if possible), 
13014  66 
including the outermost parameters and assumptions as well. 
67 

12621  68 
A typical collection of $atomize$ rules for a particular objectlogic would 
69 
provide an internalization for each of the connectives of $\Forall$, $\Imp$, 

70 
and $\equiv$. Metalevel conjunction expressed in the manner of minimal 

71 
higherorder logic as $\All{\PROP\,C} (A \Imp B \Imp \PROP\,C) \Imp PROP\,C$ 

72 
should be covered as well (this is particularly important for locales, see 

73 
\S\ref{sec:locale}). 

13014  74 

12621  75 
\item [$rule_format$] rewrites a theorem by the equalities declared as 
76 
$rulify$ rules in the current objectlogic. By default, the result is fully 

77 
normalized, including assumptions and conclusions at any depth. The 

78 
$no_asm$ option restricts the transformation to the conclusion of a rule. 

13014  79 

12621  80 
In common objectlogics (HOL, FOL, ZF), the effect of $rule_format$ is to 
81 
replace (bounded) universal quantification ($\forall$) and implication 

82 
($\imp$) by the corresponding rule statements over $\Forall$ and $\Imp$. 

83 

84 
\end{descr} 

85 

86 

87 
\section{HOL} 

88 

13039  89 
\subsection{Primitive types}\label{sec:holtypedef} 
12621  90 

91 
\indexisarcmdof{HOL}{typedecl}\indexisarcmdof{HOL}{typedef} 

92 
\begin{matharray}{rcl} 

93 
\isarcmd{typedecl} & : & \isartrans{theory}{theory} \\ 

94 
\isarcmd{typedef} & : & \isartrans{theory}{proof(prove)} \\ 

95 
\end{matharray} 

96 

97 
\begin{rail} 

12879  98 
'typedecl' typespec infix? 
12621  99 
; 
13443  100 
'typedef' altname? abstype '=' repset 
13016  101 
; 
102 

13444  103 
altname: '(' (name  'open'  'open' name) ')' 
13443  104 
; 
13016  105 
abstype: typespec infix? 
106 
; 

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

12621  108 
; 
109 
\end{rail} 

110 

111 
\begin{descr} 

13014  112 

12621  113 
\item [$\isarkeyword{typedecl}~(\vec\alpha)t$] is similar to the original 
114 
$\isarkeyword{typedecl}$ of Isabelle/Pure (see \S\ref{sec:typespure}), but 

13041  115 
also declares type arity $t :: (type, \dots, type) type$, making $t$ an 
12621  116 
actual HOL type constructor. 
13014  117 

12621  118 
\item [$\isarkeyword{typedef}~(\vec\alpha)t = A$] sets up a goal stating 
119 
nonemptiness of the set $A$. After finishing the proof, the theory will be 

13014  120 
augmented by a Gordon/HOLstyle type definition, which establishes a 
121 
bijection between the representing set $A$ and the new type $t$. 

122 

123 
Technically, $\isarkeyword{typedef}$ defines both a type $t$ and a set (term 

13016  124 
constant) of the same name (an alternative base name may be given in 
125 
parentheses). The injection from type to set is called $Rep_t$, its inverse 

126 
$Abs_t$ (this may be changed via an explicit $\isarkeyword{morphisms}$ 

127 
declaration). 

128 

13041  129 
Theorems $Rep_t$, $Rep_t_inverse$, and $Abs_t_inverse$ provide the most 
130 
basic characterization as a corresponding injection/surjection pair (in both 

13016  131 
directions). Rules $Rep_t_inject$ and $Abs_t_inject$ provide a slightly 
13041  132 
more convenient view on the injectivity part, suitable for automated proof 
133 
tools (e.g.\ in $simp$ or $iff$ declarations). Rules 

134 
$Rep_t_cases/Rep_t_induct$, and $Abs_t_cases/Abs_t_induct$ provide 

135 
alternative views on surjectivity; these are already declared as set or type 

136 
rules for the generic $cases$ and $induct$ methods. 

13443  137 

138 
An alternative name may be specified in parentheses; the default is to use 

139 
$t$ as indicated before. The $open$ declaration suppresses a separate 

140 
constant definition for the representing set. 

12621  141 
\end{descr} 
142 

13041  143 
Note that raw type declarations are rarely used in practice; the main 
144 
application is with experimental (or even axiomatic!) theory fragments. 

145 
Instead of primitive HOL type definitions, userlevel theories usually refer 

146 
to higherlevel packages such as $\isarkeyword{record}$ (see 

147 
\S\ref{sec:holrecord}) or $\isarkeyword{datatype}$ (see 

148 
\S\ref{sec:holdatatype}). 

12621  149 

13014  150 

151 
\subsection{Adhoc tuples} 

12621  152 

153 
\indexisarattof{HOL}{splitformat} 

154 
\begin{matharray}{rcl} 

155 
split_format^* & : & \isaratt \\ 

156 
\end{matharray} 

157 

158 
\railalias{splitformat}{split\_format} 

159 
\railterm{splitformat} 

160 

161 
\begin{rail} 

13027  162 
splitformat (((name *) + 'and')  ('(' 'complete' ')')) 
12621  163 
; 
164 
\end{rail} 

165 

166 
\begin{descr} 

13041  167 

12621  168 
\item [$split_format~\vec p@1 \dots \vec p@n$] puts expressions of lowlevel 
169 
tuple types into canonical form as specified by the arguments given; $\vec 

13049  170 
p@i$ refers to occurrences in premise $i$ of the rule. The ``$(complete)$'' 
13041  171 
option causes \emph{all} arguments in function applications to be 
172 
represented canonically according to their tuple type structure. 

13014  173 

12621  174 
Note that these operations tend to invent funny names for new local 
175 
parameters to be introduced. 

176 

177 
\end{descr} 

178 

179 

13039  180 
\subsection{Records}\label{sec:holrecord} 
13014  181 

13041  182 
In principle, records merely generalize the concept of tuples, where 
183 
components may be addressed by labels instead of just position. The logical 

13014  184 
infrastructure of records in Isabelle/HOL is slightly more advanced, though, 
185 
supporting truly extensible record schemes. This admits operations that are 

186 
polymorphic with respect to record extension, yielding ``objectoriented'' 

187 
effects like (single) inheritance. See also \cite{NaraschewskiWTPHOLs98} for 

188 
more details on objectoriented verification and record subtyping in HOL. 

189 

190 

13039  191 
\subsubsection{Basic concepts} 
13014  192 

193 
Isabelle/HOL supports both \emph{fixed} and \emph{schematic} records at the 

194 
level of terms and types. The notation is as follows: 

195 

196 
\begin{center} 

197 
\begin{tabular}{lll} 

198 
& record terms & record types \\ \hline 

199 
fixed & $\record{x = a\fs y = b}$ & $\record{x \ty A\fs y \ty B}$ \\ 

200 
schematic & $\record{x = a\fs y = b\fs \more = m}$ & 

201 
$\record{x \ty A\fs y \ty B\fs \more \ty M}$ \\ 

202 
\end{tabular} 

203 
\end{center} 

204 

205 
\noindent The ASCII representation of $\record{x = a}$ is \texttt{( x = a )}. 

206 

207 
A fixed record $\record{x = a\fs y = b}$ has field $x$ of value $a$ and field 

208 
$y$ of value $b$. The corresponding type is $\record{x \ty A\fs y \ty B}$, 

209 
assuming that $a \ty A$ and $b \ty B$. 

12621  210 

13014  211 
A record scheme like $\record{x = a\fs y = b\fs \more = m}$ contains fields 
212 
$x$ and $y$ as before, but also possibly further fields as indicated by the 

213 
``$\more$'' notation (which is actually part of the syntax). The improper 

214 
field ``$\more$'' of a record scheme is called the \emph{more part}. 

215 
Logically it is just a free variable, which is occasionally referred to as 

13041  216 
``row variable'' in the literature. The more part of a record scheme may be 
217 
instantiated by zero or more further components. For example, the previous 

13014  218 
scheme may get instantiated to $\record{x = a\fs y = b\fs z = c\fs \more = 
219 
m'}$, where $m'$ refers to a different more part. Fixed records are special 

220 
instances of record schemes, where ``$\more$'' is properly terminated by the 

221 
$() :: unit$ element. Actually, $\record{x = a\fs y = b}$ is just an 

222 
abbreviation for $\record{x = a\fs y = b\fs \more = ()}$. 

223 

224 
\medskip 

12621  225 

13014  226 
Two key observations make extensible records in a simply typed language like 
227 
HOL feasible: 

228 
\begin{enumerate} 

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

230 
\item field names are externalized, they cannot be accessed within the logic 

231 
as firstclass values. 

232 
\end{enumerate} 

233 

234 
\medskip 

235 

236 
In Isabelle/HOL record types have to be defined explicitly, fixing their field 

13042  237 
names and types, and their (optional) parent record. Afterwards, records may 
238 
be formed using above syntax, while obeying the canonical order of fields as 

239 
given by their declaration. The record package provides several standard 

240 
operations like selectors and updates. The common setup for various generic 

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

242 
tutorial \cite{isabelleholbook} for further instructions on using records in 

13014  243 
practice. 
244 

245 

13042  246 
\subsubsection{Record specifications} 
12621  247 

248 
\indexisarcmdof{HOL}{record} 

249 
\begin{matharray}{rcl} 

250 
\isarcmd{record} & : & \isartrans{theory}{theory} \\ 

251 
\end{matharray} 

252 

253 
\begin{rail} 

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

255 
; 

256 
\end{rail} 

257 

258 
\begin{descr} 

259 
\item [$\isarkeyword{record}~(\vec\alpha)t = \tau + \vec c :: \vec\sigma$] 

260 
defines extensible record type $(\vec\alpha)t$, derived from the optional 

261 
parent record $\tau$ by adding new field components $\vec c :: \vec\sigma$. 

13014  262 

263 
The type variables of $\tau$ and $\vec\sigma$ need to be covered by the 

264 
(distinct) parameters $\vec\alpha$. Type constructor $t$ has to be new, 

265 
while $\tau$ needs to specify an instance of an existing record type. At 

266 
least one new field $\vec c$ has to be specified. Basically, field names 

267 
need to belong to a unique record. This is not a real restriction in 

268 
practice, since fields are qualified by the record name internally. 

269 

270 
The parent record specification $\tau$ is optional; if omitted $t$ becomes a 

271 
root record. The hierarchy of all records declared within a theory context 

272 
forms a forest structure, i.e.\ a set of trees starting with a root record 

273 
each. There is no way to merge multiple parent records! 

274 

275 
For convenience, $(\vec\alpha) \, t$ is made a type abbreviation for the 

276 
fixed record type $\record{\vec c \ty \vec\sigma}$, likewise is 

277 
$(\vec\alpha, \zeta) \, t_scheme$ made an abbreviation for $\record{\vec c 

278 
\ty \vec\sigma\fs \more \ty \zeta}$. 

279 

12621  280 
\end{descr} 
281 

13042  282 
\subsubsection{Record operations} 
13014  283 

284 
Any record definition of the form presented above produces certain standard 

285 
operations. Selectors and updates are provided for any field, including the 

286 
improper one ``$more$''. There are also cumulative record constructor 

287 
functions. To simplify the presentation below, we assume for now that 

288 
$(\vec\alpha) \, t$ is a root record with fields $\vec c \ty \vec\sigma$. 

289 

290 
\medskip \textbf{Selectors} and \textbf{updates} are available for any field 

291 
(including ``$more$''): 

292 
\begin{matharray}{lll} 

293 
c@i & \ty & \record{\vec c \ty \vec \sigma, \more \ty \zeta} \To \sigma@i \\ 

294 
c@i_update & \ty & \sigma@i \To \record{\vec c \ty \vec\sigma, \more \ty \zeta} \To 

295 
\record{\vec c \ty \vec\sigma, \more \ty \zeta} 

296 
\end{matharray} 

297 

298 
There is special syntax for application of updates: $r \, \record{x \asn a}$ 

299 
abbreviates term $x_update \, a \, r$. Further notation for repeated updates 

300 
is also available: $r \, \record{x \asn a} \, \record{y \asn b} \, \record{z 

301 
\asn c}$ may be written $r \, \record{x \asn a\fs y \asn b\fs z \asn c}$. 

302 
Note that because of postfix notation the order of fields shown here is 

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

304 
applications, fields may be freely permuted in $\record{x \asn a\fs y \asn 

305 
b\fs z \asn c}$, as far as logical equality is concerned. Thus 

13041  306 
commutativity of independent updates can be proven within the logic for any 
307 
two fields, but not as a general theorem. 

13014  308 

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

13041  310 
function: 
13014  311 
\begin{matharray}{lll} 
312 
t{\dtt}make & \ty & \vec\sigma \To \record{\vec c \ty \vec \sigma} \\ 

313 
\end{matharray} 

314 

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

316 
some parent. In general, the latter may depend on another parent as well, 

317 
resulting in a list of \emph{ancestor records}. Appending the lists of fields 

318 
of all ancestors results in a certain field prefix. The record package 

319 
automatically takes care of this by lifting operations over this context of 

320 
ancestor fields. Assuming that $(\vec\alpha) \, t$ has ancestor fields $\vec 

321 
b \ty \vec\rho$, the above record operations will get the following types: 

322 
\begin{matharray}{lll} 

323 
c@i & \ty & \record{\vec b \ty \vec\rho, \vec c \ty \vec\sigma, \more \ty 

324 
\zeta} \To \sigma@i \\ 

325 
c@i_update & \ty & \sigma@i \To 

326 
\record{\vec b \ty \vec\rho, \vec c \ty \vec\sigma, \more \ty \zeta} \To 

327 
\record{\vec b \ty \vec\rho, \vec c \ty \vec\sigma, \more \ty \zeta} \\ 

328 
t{\dtt}make & \ty & \vec\rho \To \vec\sigma \To 

329 
\record{\vec b \ty \vec\rho, \vec c \ty \vec \sigma} \\ 

330 
\end{matharray} 

331 
\noindent 

332 

333 
\medskip Some further operations address the extension aspect of a derived 

334 
record scheme specifically: $fields$ produces a record fragment consisting of 

335 
exactly the new fields introduced here (the result may serve as a more part 

336 
elsewhere); $extend$ takes a fixed record and adds a given more part; 

337 
$truncate$ restricts a record scheme to a fixed record. 

338 

339 
\begin{matharray}{lll} 

340 
t{\dtt}fields & \ty & \vec\sigma \To \record{\vec c \ty \vec \sigma} \\ 

341 
t{\dtt}extend & \ty & \record{\vec d \ty \vec \rho, \vec c \ty \vec\sigma} \To 

342 
\zeta \To \record{\vec d \ty \vec \rho, \vec c \ty \vec\sigma, \more \ty \zeta} \\ 

343 
t{\dtt}truncate & \ty & \record{\vec d \ty \vec \rho, \vec c \ty \vec\sigma, \more \ty \zeta} \To 

344 
\record{\vec d \ty \vec \rho, \vec c \ty \vec\sigma} \\ 

345 
\end{matharray} 

346 

13041  347 
\noindent Note that $t{\dtt}make$ and $t{\dtt}fields$ actually coincide for root records. 
13014  348 

349 

13042  350 
\subsubsection{Derived rules and proof tools} 
13014  351 

352 
The record package proves several results internally, declaring these facts to 

353 
appropriate proof tools. This enables users to reason about record structures 

13041  354 
quite conveniently. Assume that $t$ is a record type as specified above. 
13014  355 

356 
\begin{enumerate} 

13041  357 

13014  358 
\item Standard conversions for selectors or updates applied to record 
359 
constructor terms are made part of the default Simplifier context; thus 

360 
proofs by reduction of basic operations merely require the $simp$ method 

13041  361 
without further arguments. These rules are available as $t{\dtt}simps$, 
362 
too. 

363 

13014  364 
\item Selectors applied to updated records are automatically reduced by an 
13041  365 
internal simplification procedure, which is also part of the standard 
366 
Simplifier setup. 

13014  367 

368 
\item Inject equations of a form analogous to $((x, y) = (x', y')) \equiv x=x' 

369 
\conj y=y'$ are declared to the Simplifier and Classical Reasoner as $iff$ 

370 
rules. These rules are available as $t{\dtt}iffs$. 

371 

372 
\item The introduction rule for record equality analogous to $x~r = x~r' \Imp 

373 
y~r = y~r' \Imp \dots \Imp r = r'$ is declared to the Simplifier, and as the 

374 
basic rule context as ``$intro?$''. The rule is called $t{\dtt}equality$. 

375 

376 
\item Representations of arbitrary record expressions as canonical constructor 

377 
terms are provided both in $cases$ and $induct$ format (cf.\ the generic 

378 
proof methods of the same name, \S\ref{sec:casesinduct}). Several 

379 
variations are available, for fixed records, record schemes, more parts etc. 

13041  380 

13014  381 
The generic proof methods are sufficiently smart to pick the most sensible 
382 
rule according to the type of the indicated record expression: users just 

13041  383 
need to apply something like ``$(cases~r)$'' to a certain proof problem. 
13014  384 

385 
\item The derived record operations $t{\dtt}make$, $t{\dtt}fields$, 

386 
$t{\dtt}extend$, $t{\dtt}truncate$ are \emph{not} treated automatically, but 

387 
usually need to be expanded by hand, using the collective fact 

388 
$t{\dtt}defs$. 

389 

390 
\end{enumerate} 

391 

12621  392 

393 
\subsection{Datatypes}\label{sec:holdatatype} 

394 

395 
\indexisarcmdof{HOL}{datatype}\indexisarcmdof{HOL}{repdatatype} 

396 
\begin{matharray}{rcl} 

397 
\isarcmd{datatype} & : & \isartrans{theory}{theory} \\ 

398 
\isarcmd{rep_datatype} & : & \isartrans{theory}{theory} \\ 

399 
\end{matharray} 

400 

401 
\railalias{repdatatype}{rep\_datatype} 

402 
\railterm{repdatatype} 

403 

404 
\begin{rail} 

405 
'datatype' (dtspec + 'and') 

406 
; 

13024  407 
repdatatype (name *) dtrules 
12621  408 
; 
409 

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

411 
; 

13024  412 
cons: name (type *) mixfix? 
12621  413 
; 
414 
dtrules: 'distinct' thmrefs 'inject' thmrefs 'induction' thmrefs 

415 
\end{rail} 

416 

417 
\begin{descr} 

418 
\item [$\isarkeyword{datatype}$] defines inductive datatypes in HOL. 

419 
\item [$\isarkeyword{rep_datatype}$] represents existing types as inductive 

420 
ones, generating the standard infrastructure of derived concepts (primitive 

421 
recursion etc.). 

422 
\end{descr} 

423 

424 
The induction and exhaustion theorems generated provide case names according 

425 
to the constructors involved, while parameters are named after the types (see 

426 
also \S\ref{sec:casesinduct}). 

427 

13014  428 
See \cite{isabelleHOL} for more details on datatypes, but beware of the 
429 
oldstyle theory syntax being used there! Apart from proper proof methods for 

430 
caseanalysis and induction, there are also emulations of ML tactics 

12621  431 
\texttt{case_tac} and \texttt{induct_tac} available, see 
13042  432 
\S\ref{sec:holinducttac}; these admit to refer directly to the internal 
433 
structure of subgoals (including internally bound parameters). 

12621  434 

435 

436 
\subsection{Recursive functions}\label{sec:recursion} 

437 

25872  438 
\indexisarcmdof{HOL}{primrec}\indexisarcmdof{HOL}{fun}\indexisarcmdof{HOL}{function}\indexisarcmdof{HOL}{termination} 
24524  439 

12621  440 
\begin{matharray}{rcl} 
25872  441 
\isarcmd{primrec} & : & \isarkeep{local{\dsh}theory} \\ 
442 
\isarcmd{fun} & : & \isarkeep{local{\dsh}theory} \\ 

443 
\isarcmd{function} & : & \isartrans{local{\dsh}theory}{proof(prove)} \\ 

444 
\isarcmd{termination} & : & \isartrans{local{\dsh}theory}{proof(prove)} \\ 

24524  445 
\end{matharray} 
446 

447 
\railalias{funopts}{function\_opts} 

448 

449 
\begin{rail} 

25872  450 
'primrec' target? fixes 'where' equations 
24524  451 
; 
25872  452 
equations: (thmdecl? prop + '') 
24524  453 
; 
454 
('fun'  'function') (funopts)? fixes 'where' clauses 

455 
; 

456 
clauses: (thmdecl? prop ('(' 'otherwise' ')')? + '') 

457 
; 

458 
funopts: '(' (('sequential'  'in' name  'domintros'  'tailrec'  

459 
'default' term) + ',') ')' 

460 
; 

461 
'termination' ( term )? 

462 
\end{rail} 

463 

464 
\begin{descr} 

25872  465 

24524  466 
\item [$\isarkeyword{primrec}$] defines primitive recursive functions over 
467 
datatypes, see also \cite{isabelleHOL}. 

25872  468 

24524  469 
\item [$\isarkeyword{function}$] defines functions by general 
470 
wellfounded recursion. A detailed description with examples can be 

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

472 
set of (possibly conditional) recursive equations with arbitrary 

473 
pattern matching. The command generates proof obligations for the 

474 
completeness and the compatibility of patterns. 

475 

476 
The defined function is considered partial, and the resulting 

477 
simplification rules (named $f.psimps$) and induction rule (named 

478 
$f.pinduct$) are guarded by a generated domain predicate $f_dom$. 

479 
The $\isarkeyword{termination}$ command can then be used to establish 

480 
that the function is total. 

481 

482 
\item [$\isarkeyword{fun}$] is a shorthand notation for 

483 
$\isarkeyword{function}~(\textit{sequential})$, followed by automated 

484 
proof attemts regarding pattern matching and termination. For 

485 
details, see \cite{isabellefunction}. 

486 

487 
\item [$\isarkeyword{termination}$~f] commences a termination proof 

488 
for the previously defined function $f$. If no name is given, it 

489 
refers to the most recent function definition. After the proof is 

490 
closed, the recursive equations and the induction principle is established. 

491 
\end{descr} 

492 

493 
Recursive definitions introduced by both the $\isarkeyword{primrec}$ 

494 
and the $\isarkeyword{function}$ command accommodate reasoning by 

495 
induction (cf.\ \S\ref{sec:casesinduct}): rule $c\mathord{.}induct$ 

496 
(where $c$ is the name of the function definition) refers to a 

497 
specific induction rule, with parameters named according to the 

498 
userspecified equations. Case names of $\isarkeyword{primrec}$ are 

499 
that of the datatypes involved, while those of 

500 
$\isarkeyword{function}$ are numbered (starting from $1$). 

501 

502 
The equations provided by these packages may be referred later as theorem list 

503 
$f{\dtt}simps$, where $f$ is the (collective) name of the functions defined. 

504 
Individual equations may be named explicitly as well. 

505 

506 
The $\isarkeyword{function}$ command accepts the following options: 

507 

508 
\begin{descr} 

509 
\item [\emph{sequential}] enables a preprocessor which disambiguates 

510 
overlapping patterns by making them mutually disjoint. Earlier 

511 
equations take precedence over later ones. This allows to give the 

512 
specification in a format very similar to functional programming. 

513 
Note that the resulting simplification and induction rules 

514 
correspond to the transformed specification, not the one given 

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

516 
may result in several theroems. 

517 
Also note that this automatic transformation only works 

518 
for MLstyle datatype patterns. 

519 

520 

521 
\item [\emph{in name}] gives the target for the definition. 

522 

523 
\item [\emph{domintros}] enables the automated generation of 

524 
introduction rules for the domain predicate. While mostly not 

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

526 

527 
\item [\emph{tailrec}] generates the unconstrained recursive equations 

528 
even without a termination proof, provided that the function is 

529 
tailrecursive. This currently only works 

530 

531 
\item [\emph{default d}] allows to specify a default value for a 

532 
(partial) function, which will ensure that $f(x)=d(x)$ whenever $x 

533 
\notin \textit{f\_dom}$. This feature is experimental. 

534 
\end{descr} 

535 

536 
\subsubsection{Proof methods related to recursive definitions} 

537 

538 
\indexisarmethof{HOL}{pat\_completeness} 

539 
\indexisarmethof{HOL}{relation} 

540 
\indexisarmethof{HOL}{lexicographic\_order} 

541 

542 
\begin{matharray}{rcl} 

543 
pat\_completeness & : & \isarmeth \\ 

544 
relation & : & \isarmeth \\ 

545 
lexicographic\_order & : & \isarmeth \\ 

546 
\end{matharray} 

547 

548 
\begin{rail} 

549 
'pat\_completeness' 

550 
; 

551 
'relation' term 

552 
; 

553 
'lexicographic\_order' clasimpmod 

554 
\end{rail} 

555 

556 
\begin{descr} 

557 
\item [\emph{pat\_completeness}] Specialized method to solve goals 

558 
regarding the completeness of pattern matching, as required by the 

559 
$\isarkeyword{function}$ package (cf.~\cite{isabellefunction}). 

560 

561 
\item [\emph{relation R}] Introduces a termination proof using the 

562 
relation $R$. The resulting proof state will contain goals 

563 
expressing that $R$ is wellfounded, and that the arguments 

564 
of recursive calls decrease with respect to $R$. Usually, this 

565 
method is used as the initial proof step of manual termination 

566 
proofs. 

567 

568 
\item [\emph{lexicographic\_order}] Attempts a fully automated 

569 
termination proof by searching for a lexicographic combination of 

570 
size measures on the arguments of the function. The method 

571 
accepts the same arguments as the \emph{auto} method, which it uses 

572 
internally to prove local descents. Hence, modifiers like 

573 
\emph{simp}, \emph{intro} etc.\ can be used to add ``hints'' for the 

574 
automated proofs. In case of failure, extensive information is 

575 
printed, which can help to analyse the failure (cf.~\cite{isabellefunction}). 

576 
\end{descr} 

577 

578 
\subsubsection{Legacy recursion package} 

579 
\indexisarcmdof{HOL}{recdef}\indexisarcmdof{HOL}{recdeftc} 

580 

581 
The use of the legacy $\isarkeyword{recdef}$ command is now deprecated 

582 
in favour of $\isarkeyword{function}$ and $\isarkeyword{fun}$. 

583 

584 
\begin{matharray}{rcl} 

12621  585 
\isarcmd{recdef} & : & \isartrans{theory}{theory} \\ 
586 
\isarcmd{recdef_tc}^* & : & \isartrans{theory}{proof(prove)} \\ 

587 
\end{matharray} 

588 

589 
\railalias{recdefsimp}{recdef\_simp} 

590 
\railterm{recdefsimp} 

591 

592 
\railalias{recdefcong}{recdef\_cong} 

593 
\railterm{recdefcong} 

594 

595 
\railalias{recdefwf}{recdef\_wf} 

596 
\railterm{recdefwf} 

597 

598 
\railalias{recdeftc}{recdef\_tc} 

599 
\railterm{recdeftc} 

600 

601 
\begin{rail} 

13024  602 
'recdef' ('(' 'permissive' ')')? \\ name term (prop +) hints? 
12621  603 
; 
12879  604 
recdeftc thmdecl? tc 
12621  605 
; 
13024  606 
hints: '(' 'hints' (recdefmod *) ')' 
12621  607 
; 
608 
recdefmod: ((recdefsimp  recdefcong  recdefwf) (()  'add'  'del') ':' thmrefs)  clasimpmod 

609 
; 

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

611 
; 

612 
\end{rail} 

613 

614 
\begin{descr} 

13024  615 

12621  616 
\item [$\isarkeyword{recdef}$] defines general wellfounded recursive 
13024  617 
functions (using the TFL package), see also \cite{isabelleHOL}. The 
13041  618 
``$(permissive)$'' option tells TFL to recover from failed proof attempts, 
12621  619 
returning unfinished results. The $recdef_simp$, $recdef_cong$, and 
620 
$recdef_wf$ hints refer to auxiliary rules to be used in the internal 

13024  621 
automated proof process of TFL. Additional $clasimpmod$ declarations (cf.\ 
12621  622 
\S\ref{sec:clasimp}) may be given to tune the context of the Simplifier 
13024  623 
(cf.\ \S\ref{sec:simplifier}) and Classical reasoner (cf.\ 
12621  624 
\S\ref{sec:classical}). 
13024  625 

12621  626 
\item [$\isarkeyword{recdef_tc}~c~(i)$] recommences the proof for leftover 
627 
termination condition number $i$ (default $1$) as generated by a 

628 
$\isarkeyword{recdef}$ definition of constant $c$. 

13024  629 

12621  630 
Note that in most cases, $\isarkeyword{recdef}$ is able to finish its 
631 
internal proofs without manual intervention. 

13024  632 

12621  633 
\end{descr} 
634 

635 
\medskip Hints for $\isarkeyword{recdef}$ may be also declared globally, using 

636 
the following attributes. 

637 

638 
\indexisarattof{HOL}{recdefsimp}\indexisarattof{HOL}{recdefcong}\indexisarattof{HOL}{recdefwf} 

639 
\begin{matharray}{rcl} 

640 
recdef_simp & : & \isaratt \\ 

641 
recdef_cong & : & \isaratt \\ 

642 
recdef_wf & : & \isaratt \\ 

643 
\end{matharray} 

644 

645 
\railalias{recdefsimp}{recdef\_simp} 

646 
\railterm{recdefsimp} 

647 

648 
\railalias{recdefcong}{recdef\_cong} 

649 
\railterm{recdefcong} 

650 

651 
\railalias{recdefwf}{recdef\_wf} 

652 
\railterm{recdefwf} 

653 

654 
\begin{rail} 

655 
(recdefsimp  recdefcong  recdefwf) (()  'add'  'del') 

656 
; 

657 
\end{rail} 

658 

14119  659 
\subsection{Definition by specification}\label{sec:holspecification} 
660 

661 
\indexisarcmdof{HOL}{specification} 

662 
\begin{matharray}{rcl} 

663 
\isarcmd{specification} & : & \isartrans{theory}{proof(prove)} \\ 

14619
8876ad83b1fb
Added documentation for ax_specification, as well as a small comparison of
skalberg
parents:
14165
diff
changeset

664 
\isarcmd{ax_specification} & : & \isartrans{theory}{proof(prove)} \\ 
14119  665 
\end{matharray} 
666 

667 
\begin{rail} 

14619
8876ad83b1fb
Added documentation for ax_specification, as well as a small comparison of
skalberg
parents:
14165
diff
changeset

668 
('specification'  'ax\_specification') '(' (decl +) ')' \\ (thmdecl? prop +) 
14119  669 
; 
14642  670 
decl: ((name ':')? term '(' 'overloaded' ')'?) 
14119  671 
\end{rail} 
672 

673 
\begin{descr} 

14165
67b4c4cdb270
New specification syntax added (the specification may be split over
skalberg
parents:
14119
diff
changeset

674 
\item [$\isarkeyword{specification}~decls~\phi$] sets up a goal stating 
67b4c4cdb270
New specification syntax added (the specification may be split over
skalberg
parents:
14119
diff
changeset

675 
the existence of terms with the properties specified to hold for the 
67b4c4cdb270
New specification syntax added (the specification may be split over
skalberg
parents:
14119
diff
changeset

676 
constants given in $\mathit{decls}$. After finishing the proof, the 
67b4c4cdb270
New specification syntax added (the specification may be split over
skalberg
parents:
14119
diff
changeset

677 
theory will be augmented with definitions for the given constants, 
67b4c4cdb270
New specification syntax added (the specification may be split over
skalberg
parents:
14119
diff
changeset

678 
as well as with theorems stating the properties for these constants. 
14619
8876ad83b1fb
Added documentation for ax_specification, as well as a small comparison of
skalberg
parents:
14165
diff
changeset

679 
\item [$\isarkeyword{ax_specification}~decls~\phi$] sets up a goal stating 
8876ad83b1fb
Added documentation for ax_specification, as well as a small comparison of
skalberg
parents:
14165
diff
changeset

680 
the existence of terms with the properties specified to hold for the 
8876ad83b1fb
Added documentation for ax_specification, as well as a small comparison of
skalberg
parents:
14165
diff
changeset

681 
constants given in $\mathit{decls}$. After finishing the proof, the 
8876ad83b1fb
Added documentation for ax_specification, as well as a small comparison of
skalberg
parents:
14165
diff
changeset

682 
theory will be augmented with axioms expressing the properties given 
8876ad83b1fb
Added documentation for ax_specification, as well as a small comparison of
skalberg
parents:
14165
diff
changeset

683 
in the first place. 
14119  684 
\item[$decl$] declares a constant to be defined by the specification 
685 
given. The definition for the constant $c$ is bound to the name 

686 
$c$\_def unless a theorem name is given in the declaration. 

687 
Overloaded constants should be declared as such. 

688 
\end{descr} 

12621  689 

14619
8876ad83b1fb
Added documentation for ax_specification, as well as a small comparison of
skalberg
parents:
14165
diff
changeset

690 
Whether to use $\isarkeyword{specification}$ or $\isarkeyword{ax_specification}$ 
8876ad83b1fb
Added documentation for ax_specification, as well as a small comparison of
skalberg
parents:
14165
diff
changeset

691 
is to some extent a matter of style. $\isarkeyword{specification}$ introduces no new axioms, 
8876ad83b1fb
Added documentation for ax_specification, as well as a small comparison of
skalberg
parents:
14165
diff
changeset

692 
and so by construction cannot introduce inconsistencies, whereas $\isarkeyword{ax_specification}$ 
8876ad83b1fb
Added documentation for ax_specification, as well as a small comparison of
skalberg
parents:
14165
diff
changeset

693 
does introduce axioms, but only after the user has explicitly proven it to be 
8876ad83b1fb
Added documentation for ax_specification, as well as a small comparison of
skalberg
parents:
14165
diff
changeset

694 
safe. A practical issue must be considered, though: After introducing two constants 
8876ad83b1fb
Added documentation for ax_specification, as well as a small comparison of
skalberg
parents:
14165
diff
changeset

695 
with the same properties using $\isarkeyword{specification}$, one can prove 
8876ad83b1fb
Added documentation for ax_specification, as well as a small comparison of
skalberg
parents:
14165
diff
changeset

696 
that the two constants are, in fact, equal. If this might be a problem, 
8876ad83b1fb
Added documentation for ax_specification, as well as a small comparison of
skalberg
parents:
14165
diff
changeset

697 
one should use $\isarkeyword{ax_specification}$. 
8876ad83b1fb
Added documentation for ax_specification, as well as a small comparison of
skalberg
parents:
14165
diff
changeset

698 

24477  699 
\subsection{Inductive and coinductive definitions}\label{sec:holinductive} 
700 

701 
An {\bf inductive definition} specifies the least predicate (or set) $R$ closed under given 

702 
rules. (Applying a rule to elements of~$R$ yields a result within~$R$.) For 

703 
example, a structural operational semantics is an inductive definition of an 

704 
evaluation relation. Dually, a {\bf coinductive definition} specifies the 

705 
greatest predicate (or set) $R$ consistent with given rules. (Every element of~$R$ can be 

706 
seen as arising by applying a rule to elements of~$R$.) An important example 

707 
is using bisimulation relations to formalise equivalence of processes and 

708 
infinite data structures. 

12621  709 

24477  710 
This package is related to the ZF one, described in a separate 
711 
paper,% 

712 
\footnote{It appeared in CADE~\cite{paulsonCADE}; a longer version is 

713 
distributed with Isabelle.} % 

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

715 
than ZF's thanks to HOL's extralogical automatic typechecking. The types of 

716 
the (co)inductive predicates (or sets) determine the domain of the fixedpoint definition, and 

717 
the package does not have to use inference rules for typechecking. 

718 

719 
\indexisarcmdof{HOL}{inductive}\indexisarcmdof{HOL}{inductiveset}\indexisarcmdof{HOL}{coinductive}\indexisarcmdof{HOL}{coinductiveset}\indexisarattof{HOL}{mono} 

12621  720 
\begin{matharray}{rcl} 
25872  721 
\isarcmd{inductive} & : & \isarkeep{local{\dsh}theory} \\ 
722 
\isarcmd{inductive_set} & : & \isarkeep{local{\dsh}theory} \\ 

723 
\isarcmd{coinductive} & : & \isarkeep{local{\dsh}theory} \\ 

724 
\isarcmd{coinductive_set} & : & \isarkeep{local{\dsh}theory} \\ 

12621  725 
mono & : & \isaratt \\ 
726 
\end{matharray} 

727 

728 
\begin{rail} 

24482  729 
('inductive'  'inductive\_set'  'coinductive'  'coinductive\_set') target? fixes ('for' fixes)? \\ 
730 
('where' clauses)? ('monos' thmrefs)? 

24477  731 
; 
732 
clauses: (thmdecl? prop + '') 

12621  733 
; 
734 
'mono' (()  'add'  'del') 

735 
; 

736 
\end{rail} 

737 

738 
\begin{descr} 

739 
\item [$\isarkeyword{inductive}$ and $\isarkeyword{coinductive}$] define 

24477  740 
(co)inductive predicates from the introduction rules given in the \texttt{where} section. 
24482  741 
The optional \texttt{for} section contains a list of parameters of the (co)inductive 
742 
predicates that remain fixed throughout the definition. 

24477  743 
The optional \texttt{monos} section contains \textit{monotonicity theorems}, 
744 
which are required for each operator applied to a recursive set in the introduction rules. 

745 
There {\bf must} be a theorem of the form $A \leq B \Imp M~A \leq M~B$, for each 

746 
premise $M~R@i~t$ in an introduction rule! 

747 
\item [$\isarkeyword{inductive_set}$ and $\isarkeyword{coinductive_set}$] are wrappers 

748 
for to the previous commands, allowing the definition of (co)inductive sets. 

12621  749 
\item [$mono$] declares monotonicity rules. These rule are involved in the 
750 
automated monotonicity proof of $\isarkeyword{inductive}$. 

751 
\end{descr} 

752 

24477  753 
\subsubsection{Derived rules} 
754 

755 
Each (co)inductive definition $R$ adds definitions to the theory and also 

756 
proves some theorems: 

757 
\begin{description} 

758 
\item[$R{\dtt}intros$] is the list of introduction rules, now proved as theorems, for 

759 
the recursive predicates (or sets). The rules are also available individually, 

760 
using the names given them in the theory file. 

761 
\item[$R{\dtt}cases$] is the case analysis (or elimination) rule. 

762 
\item[$R{\dtt}(co)induct$] is the (co)induction rule. 

763 
\end{description} 

764 
When several predicates $R@1$, $\ldots$, $R@n$ are defined simultaneously, 

765 
the list of introduction rules is called $R@1_\ldots_R@n{\dtt}intros$, the 

766 
case analysis rules are called $R@1{\dtt}cases$, $\ldots$, $R@n{\dtt}cases$, and 

767 
the list of mutual induction rules is called $R@1_\ldots_R@n{\dtt}inducts$. 

768 

769 
\subsubsection{Monotonicity theorems} 

770 

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

772 
proofs. New rules can be added to this set via the $mono$ attribute. 

773 
Theory \texttt{Inductive} shows how this is done. In general, the following 

774 
monotonicity theorems may be added: 

775 
\begin{itemize} 

776 
\item Theorems of the form $A \leq B \Imp M~A \leq M~B$, for proving 

777 
monotonicity of inductive definitions whose introduction rules have premises 

778 
involving terms such as $M~R@i~t$. 

779 
\item Monotonicity theorems for logical operators, which are of the general form 

780 
$\List{\cdots \to \cdots;~\ldots;~\cdots \to \cdots} \Imp 

781 
\cdots \to \cdots$. 

782 
For example, in the case of the operator $\lor$, the corresponding theorem is 

783 
\[ 

784 
\infer{P@1 \lor P@2 \to Q@1 \lor Q@2} 

785 
{P@1 \to Q@1 & P@2 \to Q@2} 

786 
\] 

787 
\item De Morgan style equations for reasoning about the ``polarity'' of expressions, e.g. 

788 
\[ 

789 
(\lnot \lnot P) ~=~ P \qquad\qquad 

790 
(\lnot (P \land Q)) ~=~ (\lnot P \lor \lnot Q) 

791 
\] 

792 
\item Equations for reducing complex operators to more primitive ones whose 

793 
monotonicity can easily be proved, e.g. 

794 
\[ 

795 
(P \to Q) ~=~ (\lnot P \lor Q) \qquad\qquad 

796 
\mathtt{Ball}~A~P ~\equiv~ \forall x.~x \in A \to P~x 

797 
\] 

798 
\end{itemize} 

799 

800 
%FIXME: Example of an inductive definition 

12621  801 

802 

803 
\subsection{Arithmetic proof support} 

804 

805 
\indexisarmethof{HOL}{arith}\indexisarattof{HOL}{arithsplit} 

806 
\begin{matharray}{rcl} 

807 
arith & : & \isarmeth \\ 

808 
arith_split & : & \isaratt \\ 

809 
\end{matharray} 

810 

811 
\begin{rail} 

812 
'arith' '!'? 

813 
; 

814 
\end{rail} 

815 

816 
The $arith$ method decides linear arithmetic problems (on types $nat$, $int$, 

817 
$real$). Any current facts are inserted into the goal before running the 

818 
procedure. The ``!''~argument causes the full context of assumptions to be 

819 
included. The $arith_split$ attribute declares case split rules to be 

820 
expanded before the arithmetic procedure is invoked. 

821 

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

823 
performed by the Simplifier. 

824 

825 

13024  826 
\subsection{Cases and induction: emulating tactic scripts}\label{sec:holinducttac} 
12621  827 

828 
The following important tactical tools of Isabelle/HOL have been ported to 

829 
Isar. These should be never used in proper proof texts! 

830 

831 
\indexisarmethof{HOL}{casetac}\indexisarmethof{HOL}{inducttac} 

832 
\indexisarmethof{HOL}{indcases}\indexisarcmdof{HOL}{inductivecases} 

833 
\begin{matharray}{rcl} 

834 
case_tac^* & : & \isarmeth \\ 

835 
induct_tac^* & : & \isarmeth \\ 

836 
ind_cases^* & : & \isarmeth \\ 

837 
\isarcmd{inductive_cases} & : & \isartrans{theory}{theory} \\ 

838 
\end{matharray} 

839 

840 
\railalias{casetac}{case\_tac} 

841 
\railterm{casetac} 

842 

843 
\railalias{inducttac}{induct\_tac} 

844 
\railterm{inducttac} 

845 

846 
\railalias{indcases}{ind\_cases} 

847 
\railterm{indcases} 

848 

849 
\railalias{inductivecases}{inductive\_cases} 

850 
\railterm{inductivecases} 

851 

852 
\begin{rail} 

853 
casetac goalspec? term rule? 

854 
; 

855 
inducttac goalspec? (insts * 'and') rule? 

856 
; 

24482  857 
indcases (prop +) ('for' (name +)) ? 
12621  858 
; 
13014  859 
inductivecases (thmdecl? (prop +) + 'and') 
12621  860 
; 
861 

862 
rule: ('rule' ':' thmref) 

863 
; 

864 
\end{rail} 

865 

866 
\begin{descr} 

867 
\item [$case_tac$ and $induct_tac$] admit to reason about inductive datatypes 

868 
only (unless an alternative rule is given explicitly). Furthermore, 

869 
$case_tac$ does a classical case split on booleans; $induct_tac$ allows only 

870 
variables to be given as instantiation. These tactic emulations feature 

871 
both goal addressing and dynamic instantiation. Note that named rule cases 

872 
are \emph{not} provided as would be by the proper $induct$ and $cases$ proof 

873 
methods (see \S\ref{sec:casesinduct}). 

13041  874 

12621  875 
\item [$ind_cases$ and $\isarkeyword{inductive_cases}$] provide an interface 
13041  876 
to the internal \texttt{mk_cases} operation. Rules are simplified in an 
877 
unrestricted forward manner. 

13014  878 

12621  879 
While $ind_cases$ is a proof method to apply the result immediately as 
880 
elimination rules, $\isarkeyword{inductive_cases}$ provides case split 

24482  881 
theorems at the theory level for later use. 
882 
The \texttt{for} option of the $ind_cases$ method allows to specify a list 

883 
of variables that should be generalized before applying the resulting rule. 

12621  884 
\end{descr} 
885 

886 

13039  887 
\subsection{Executable code} 
13027  888 

20587  889 
Isabelle/Pure provides two generic frameworks to support code 
890 
generation from executable specifications. Isabelle/HOL 

891 
instantiates these mechanisms in a 

26245  892 
way that is amenable to enduser applications. 
20587  893 

894 
One framework generates code from both functional and 

895 
relational programs to SML. See 

19988  896 
\cite{isabelleHOL} for further information (this actually covers the 
897 
newstyle theory format as well). 

13027  898 

19988  899 
\indexisarcmd{value}\indexisarcmd{codemodule}\indexisarcmd{codelibrary} 
900 
\indexisarcmd{constscode}\indexisarcmd{typescode} 

13027  901 
\indexisaratt{code} 
902 

903 
\begin{matharray}{rcl} 

19988  904 
\isarcmd{value}^* & : & \isarkeep{theory~~proof} \\ 
17659  905 
\isarcmd{code_module} & : & \isartrans{theory}{theory} \\ 
906 
\isarcmd{code_library} & : & \isartrans{theory}{theory} \\ 

13027  907 
\isarcmd{consts_code} & : & \isartrans{theory}{theory} \\ 
908 
\isarcmd{types_code} & : & \isartrans{theory}{theory} \\ 

909 
code & : & \isaratt \\ 

910 
\end{matharray} 

911 

17659  912 
\railalias{verblbrace}{\texttt{\ttlbrace*}} 
913 
\railalias{verbrbrace}{\texttt{*\ttrbrace}} 

914 
\railterm{verblbrace} 

915 
\railterm{verbrbrace} 

916 

19988  917 
\begin{rail} 
918 
'value' term; 

13027  919 

19988  920 
( 'code\_module'  'code\_library' ) modespec ? name ? \\ 
17659  921 
( 'file' name ) ? ( 'imports' ( name + ) ) ? \\ 
922 
'contains' ( ( name '=' term ) +  term + ); 

923 

924 
modespec : '(' ( name * ) ')'; 

925 

19988  926 
'consts\_code' (codespec +); 
17659  927 

22921
475ff421a6a3
consts in consts_code Isar commands are now referred to by usual term syntax
haftmann
parents:
22845
diff
changeset

928 
codespec : const template attachment ?; 
13027  929 

19988  930 
'types\_code' (tycodespec +); 
17659  931 

932 
tycodespec : name template attachment ?; 

933 

22921
475ff421a6a3
consts in consts_code Isar commands are now referred to by usual term syntax
haftmann
parents:
22845
diff
changeset

934 
const: term; 
475ff421a6a3
consts in consts_code Isar commands are now referred to by usual term syntax
haftmann
parents:
22845
diff
changeset

935 

17659  936 
template: '(' string ')'; 
937 

938 
attachment: 'attach' modespec ? verblbrace text verbrbrace; 

939 

940 
'code' (name)?; 

13027  941 
\end{rail} 
942 

19988  943 
\begin{descr} 
944 
\item [$\isarkeyword{value}~t$] reads, evaluates and prints a term 

945 
using the code generator. 

946 
\end{descr} 

947 

20587  948 
The other framework generates code from functional programs 
22291  949 
(including overloading using type classes) to SML \cite{SML}, 
950 
OCaml \cite{OCaml} and Haskell \cite{haskellrevisedreport}. 

20587  951 
Conceptually, code generation is split up in three steps: \emph{selection} 
22752  952 
of code theorems, \emph{translation} into an abstract executable view 
20587  953 
and \emph{serialization} to a specific \emph{target language}. 
21077  954 
See \cite{isabellecodegen} for an introduction on how to use it. 
20587  955 

24992  956 
\indexisarcmd{exportcode} 
22752  957 
\indexisarcmd{codethms} 
958 
\indexisarcmd{codedeps} 

959 
\indexisarcmd{codedatatype} 

21077  960 
\indexisarcmd{codeconst} 
961 
\indexisarcmd{codetype} 

962 
\indexisarcmd{codeclass} 

963 
\indexisarcmd{codeinstance} 

22291  964 
\indexisarcmd{codemonad} 
21077  965 
\indexisarcmd{codereserved} 
24992  966 
\indexisarcmd{codeinclude} 
21077  967 
\indexisarcmd{codemodulename} 
24992  968 
\indexisarcmd{codeexception} 
22291  969 
\indexisarcmd{printcodesetup} 
20587  970 
\indexisaratt{code func} 
971 
\indexisaratt{code inline} 

972 

973 
\begin{matharray}{rcl} 

24348  974 
\isarcmd{export_code}^* & : & \isarkeep{theory~~proof} \\ 
22752  975 
\isarcmd{code_thms}^* & : & \isarkeep{theory~~proof} \\ 
976 
\isarcmd{code_deps}^* & : & \isarkeep{theory~~proof} \\ 

977 
\isarcmd{code_datatype} & : & \isartrans{theory}{theory} \\ 

20587  978 
\isarcmd{code_const} & : & \isartrans{theory}{theory} \\ 
979 
\isarcmd{code_type} & : & \isartrans{theory}{theory} \\ 

980 
\isarcmd{code_class} & : & \isartrans{theory}{theory} \\ 

981 
\isarcmd{code_instance} & : & \isartrans{theory}{theory} \\ 

22291  982 
\isarcmd{code_monad} & : & \isartrans{theory}{theory} \\ 
21077  983 
\isarcmd{code_reserved} & : & \isartrans{theory}{theory} \\ 
24992  984 
\isarcmd{code_include} & : & \isartrans{theory}{theory} \\ 
21077  985 
\isarcmd{code_modulename} & : & \isartrans{theory}{theory} \\ 
24992  986 
\isarcmd{code_exception} & : & \isartrans{theory}{theory} \\ 
22291  987 
\isarcmd{print_codesetup}^* & : & \isarkeep{theory~~proof} \\ 
20587  988 
code\ func & : & \isaratt \\ 
989 
code\ inline & : & \isaratt \\ 

990 
\end{matharray} 

991 

992 
\begin{rail} 

24348  993 
'export\_code' ( constexpr + ) ? \\ 
24482  994 
( ( 'in' target ( 'module\_name' string ) ? \\ 
995 
( 'file' ( string  '' ) ) ? ( '(' args ')' ) ?) + ) ?; 

22752  996 

997 
'code\_thms' ( constexpr + ) ?; 

998 

999 
'code\_deps' ( constexpr + ) ?; 

20587  1000 

1001 
const : term; 

1002 

22752  1003 
constexpr : ( const  'name.*'  '*' ); 
1004 

20587  1005 
typeconstructor : nameref; 
1006 

1007 
class : nameref; 

1008 

22291  1009 
target : 'OCaml'  'SML'  'Haskell'; 
20587  1010 

22752  1011 
'code\_datatype' const +; 
1012 

20587  1013 
'code\_const' (const + 'and') \\ 
22845  1014 
( ( '(' target ( syntax ? + 'and' ) ')' ) + ); 
20587  1015 

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

22845  1017 
( ( '(' target ( syntax ? + 'and' ) ')' ) + ); 
20587  1018 

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

1020 
( ( '(' target \\ 

22845  1021 
( ( string ('where' \\ 
1022 
( const ( '=='  equiv ) string ) + ) ? ) ? + 'and' ) ')' ) + ); 

20587  1023 

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

22845  1025 
( ( '(' target ( '' ? + 'and' ) ')' ) + ); 
20587  1026 

24992  1027 
'code\_monad' const const target; 
22291  1028 

21077  1029 
'code\_reserved' target ( string + ); 
1030 

24992  1031 
'code\_include' target ( string ( string  '') ); 
1032 

21077  1033 
'code\_modulename' target ( ( string string ) + ); 
1034 

24992  1035 
'code\_exception' ( const + ); 
21077  1036 

22291  1037 
syntax : string  ( 'infix'  'infixl'  'infixr' ) nat string; 
20587  1038 

22291  1039 
'print\_codesetup'; 
20587  1040 

22845  1041 
'code\ func' ( 'del' ) ?; 
1042 

1043 
'code\ inline' ( 'del' ) ?; 

20587  1044 
\end{rail} 
1045 

1046 
\begin{descr} 

1047 

24348  1048 
\item [$\isarcmd{export_code}$] is the canonical interface for generating and 
20587  1049 
serializing code: for a given list of constants, code is generated for the specified 
1050 
target language(s). Abstract code is cached incrementally. If no constant is given, 

22845  1051 
the currently cached code is serialized. If no serialization instruction 
20587  1052 
is given, only abstract code is cached. 
1053 

22291  1054 
Constants may be specified by giving them literally, referring 
1055 
to all exeuctable contants within a certain theory named ``name'' 

22752  1056 
by giving (``name.*''), or referring to \emph{all} executable 
22291  1057 
constants currently available (``*''). 
1058 

23807  1059 
By default, for each involved theory one corresponding name space module 
24248  1060 
is generated. Alternativly, a module name may be specified after the 
1061 
(``module_name'') keyword; then \emph{all} code is placed in this module. 

23807  1062 

22845  1063 
For \emph{SML} and \emph{OCaml}, the file specification refers to 
1064 
a single file; for \emph{Haskell}, it refers to a whole directory, 

1065 
where code is generated in multiple files reflecting the module hierarchy. 

1066 
The file specification ``'' denotes standard output. For \emph{SML}, 

1067 
omitting the file specification compiles code internally 

1068 
in the context of the current ML session. 

22291  1069 

22845  1070 
Serializers take an optional list of arguments in parentheses. 
1071 
For \emph{Haskell} a module name prefix may be given using the ``root:'' 

1072 
argument; ``string\_classes'' adds a ``deriving (Read, Show)'' clause 

21090  1073 
to each appropriate datatype declaration. 
20587  1074 

22752  1075 
\item [$\isarcmd{code_thms}$] prints a list of theorems representing the 
1076 
corresponding program containing all given constants; if no constants are 

24248  1077 
given, the currently cached code theorems are printed. 
22752  1078 

1079 
\item [$\isarcmd{code_deps}$] visualizes dependencies of theorems representing the 

1080 
corresponding program containing all given constants; if no constants are 

22845  1081 
given, the currently cached code theorems are visualized. 
22752  1082 

1083 
\item [$\isarcmd{code_datatype}$] specifies a constructor set for a logical type. 

1084 

20587  1085 
\item [$\isarcmd{code_const}$] associates a list of constants 
22845  1086 
with targetspecific serializations; omitting a serialization 
1087 
deletes an existing serialization. 

20587  1088 

1089 
\item [$\isarcmd{code_type}$] associates a list of type constructors 

22845  1090 
with targetspecific serializations; omitting a serialization 
1091 
deletes an existing serialization. 

20587  1092 

1093 
\item [$\isarcmd{code_class}$] associates a list of classes 

1094 
with targetspecific class names; in addition, constants associated 

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

22845  1096 
declarations; omitting a serialization 
1097 
deletes an existing serialization. Applies only to \emph{Haskell}. 

20587  1098 

1099 
\item [$\isarcmd{code_instance}$] declares a list of type constructor / class 

1100 
instance relations as ``already present'' for a given target. 

22845  1101 
Omitting a ``'' deletes an existing ``already present'' declaration. 
20587  1102 
Applies only to \emph{Haskell}. 
1103 

22291  1104 
\item [$\isarcmd{code_monad}$] provides an auxiliary mechanism 
24992  1105 
to generate monadic code. 
22291  1106 

21077  1107 
\item [$\isarcmd{code_reserved}$] declares a list of names 
1108 
as reserved for a given target, preventing it to be shadowed 

1109 
by any generated code. 

1110 

24992  1111 
\item [$\isarcmd{code_include}$] adds arbitrary named content (''include``) 
1112 
to generated code. A as last argument ``'' will remove an already added ''include``. 

1113 

22752  1114 
\item [$\isarcmd{code_modulename}$] declares aliasings from one module name 
1115 
onto another. 

21077  1116 

24992  1117 
\item [$\isarcmd{code_exception}$] declares constants which are not required 
1118 
to have a definition by a defining equations; these are mapped on exceptions 

1119 
instead. 

21077  1120 

22845  1121 
\item [$code\ func$] selects (or with option ''del``, deselects) explicitly 
22291  1122 
a defining equation for code generation. Usually packages introducing 
1123 
defining equations provide a resonable default setup for selection. 

20587  1124 

22845  1125 
\item [$code\ inline$] declares (or with option ''del``, removes) 
1126 
inlining theorems which are applied as rewrite rules to any defining equation 

1127 
during preprocessing. 

20587  1128 

22291  1129 
\item [$\isarcmd{print_codesetup}$] gives an overview on selected 
22845  1130 
defining equations, code generator datatypes and preprocessor setup. 
20587  1131 

1132 
\end{descr} 

13027  1133 

12621  1134 
\section{HOLCF} 
1135 

1136 
\subsection{Mixfix syntax for continuous operations} 

1137 

14682
a5072752114c
HOLCF: discontinued special version of 'constdefs';
wenzelm
parents:
14642
diff
changeset

1138 
\indexisarcmdof{HOLCF}{consts} 
12621  1139 

1140 
\begin{matharray}{rcl} 

1141 
\isarcmd{consts} & : & \isartrans{theory}{theory} \\ 

1142 
\end{matharray} 

1143 

14165
67b4c4cdb270
New specification syntax added (the specification may be split over
skalberg
parents:
14119
diff
changeset

1144 
HOLCF provides a separate type for continuous functions $\alpha \to 
12621  1145 
\beta$, with an explicit application operator $f \cdot x$. Isabelle mixfix 
1146 
syntax normally refers directly to the pure metalevel function type $\alpha 

1147 
\To \beta$, with application $f\,x$. 

1148 

14682
a5072752114c
HOLCF: discontinued special version of 'constdefs';
wenzelm
parents:
14642
diff
changeset

1149 
The HOLCF variant of $\CONSTS$ modifies that of Pure Isabelle (cf.\ 
a5072752114c
HOLCF: discontinued special version of 'constdefs';
wenzelm
parents:
14642
diff
changeset

1150 
\S\ref{sec:consts}) such that declarations involving continuous function types 
a5072752114c
HOLCF: discontinued special version of 'constdefs';
wenzelm
parents:
14642
diff
changeset

1151 
are treated specifically. Any given syntax template is transformed 
a5072752114c
HOLCF: discontinued special version of 'constdefs';
wenzelm
parents:
14642
diff
changeset

1152 
internally, generating translation rules for the abstract and concrete 
a5072752114c
HOLCF: discontinued special version of 'constdefs';
wenzelm
parents:
14642
diff
changeset

1153 
representation of continuous application. Note that mixing of HOLCF and Pure 
14642  1154 
application is \emph{not} supported! 
12621  1155 

1156 
\subsection{Recursive domains} 

1157 

1158 
\indexisarcmdof{HOLCF}{domain} 

1159 
\begin{matharray}{rcl} 

1160 
\isarcmd{domain} & : & \isartrans{theory}{theory} \\ 

1161 
\end{matharray} 

1162 

1163 
\begin{rail} 

1164 
'domain' parname? (dmspec + 'and') 

1165 
; 

1166 

1167 
dmspec: typespec '=' (cons + '') 

1168 
; 

13024  1169 
cons: name (type *) mixfix? 
12621  1170 
; 
1171 
dtrules: 'distinct' thmrefs 'inject' thmrefs 'induction' thmrefs 

1172 
\end{rail} 

1173 

13041  1174 
Recursive domains in HOLCF are analogous to datatypes in classical HOL (cf.\ 
1175 
\S\ref{sec:holdatatype}). Mutual recursion is supported, but no nesting nor 

12621  1176 
arbitrary branching. Domain constructors may be strict (default) or lazy, the 
13041  1177 
latter admits to introduce infinitary objects in the typical LCF manner (e.g.\ 
13014  1178 
lazy lists). See also \cite{MuellerNvOS99} for a general discussion of HOLCF 
1179 
domains. 

12621  1180 

1181 

1182 
\section{ZF} 

1183 

1184 
\subsection{Type checking} 

1185 

13024  1186 
The ZF logic is essentially untyped, so the concept of ``type checking'' is 
1187 
performed as logical reasoning about setmembership statements. A special 

1188 
method assists users in this task; a version of this is already declared as a 

13041  1189 
``solver'' in the standard Simplifier setup. 
13024  1190 

1191 
\indexisarcmd{printtcset}\indexisaratt{typecheck}\indexisaratt{TC} 

1192 

1193 
\begin{matharray}{rcl} 

1194 
\isarcmd{print_tcset}^* & : & \isarkeep{theory~~proof} \\ 

1195 
typecheck & : & \isarmeth \\ 

1196 
TC & : & \isaratt \\ 

1197 
\end{matharray} 

1198 

1199 
\begin{rail} 

1200 
'TC' (()  'add'  'del') 

1201 
; 

1202 
\end{rail} 

1203 

1204 
\begin{descr} 

1205 

1206 
\item [$\isarcmd{print_tcset}$] prints the collection of typechecking rules of 

1207 
the current context. 

1208 

1209 
Note that the component built into the Simplifier only knows about those 

1210 
rules being declared globally in the theory! 

1211 

1212 
\item [$typecheck$] attempts to solve any pending typechecking problems in 

1213 
subgoals. 

1214 

1215 
\item [$TC$] adds or deletes typechecking rules from the context. 

1216 

1217 
\end{descr} 

1218 

1219 

1220 
\subsection{(Co)Inductive sets and datatypes} 

1221 

1222 
\subsubsection{Set definitions} 

1223 

1224 
In ZF everything is a set. The generic inductive package also provides a 

1225 
specific view for ``datatype'' specifications. Coinductive definitions are 

13041  1226 
available in both cases, too. 
13024  1227 

1228 
\indexisarcmdof{ZF}{inductive}\indexisarcmdof{ZF}{coinductive} 

1229 
\indexisarcmdof{ZF}{datatype}\indexisarcmdof{ZF}{codatatype} 

1230 
\begin{matharray}{rcl} 

1231 
\isarcmd{inductive} & : & \isartrans{theory}{theory} \\ 

1232 
\isarcmd{coinductive} & : & \isartrans{theory}{theory} \\ 

1233 
\isarcmd{datatype} & : & \isartrans{theory}{theory} \\ 

1234 
\isarcmd{codatatype} & : & \isartrans{theory}{theory} \\ 

1235 
\end{matharray} 

1236 

1237 
\railalias{CONDEFS}{con\_defs} 

1238 
\railterm{CONDEFS} 

1239 

1240 
\railalias{TYPEINTROS}{type\_intros} 

1241 
\railterm{TYPEINTROS} 

1242 

1243 
\railalias{TYPEELIMS}{type\_elims} 

1244 
\railterm{TYPEELIMS} 

1245 

1246 
\begin{rail} 

1247 
('inductive'  'coinductive') domains intros hints 

1248 
; 

12621  1249 

13024  1250 
domains: 'domains' (term + '+') ('<='  subseteq) term 
1251 
; 

1252 
intros: 'intros' (thmdecl? prop +) 

1253 
; 

1254 
hints: monos? condefs? typeintros? typeelims? 

1255 
; 

1256 
monos: ('monos' thmrefs)? 

1257 
; 

1258 
condefs: (CONDEFS thmrefs)? 

1259 
; 

1260 
typeintros: (TYPEINTROS thmrefs)? 

1261 
; 

1262 
typeelims: (TYPEELIMS thmrefs)? 

1263 
; 

1264 
\end{rail} 

1265 

1266 
In the following diagram $monos$, $typeintros$, and $typeelims$ are the same 

1267 
as above. 

1268 

1269 
\begin{rail} 

1270 
('datatype'  'codatatype') domain? (dtspec + 'and') hints 

1271 
; 

1272 

1273 
domain: ('<='  subseteq) term 

1274 
; 

1275 
dtspec: term '=' (con + '') 

1276 
; 

1277 
con: name ('(' (term ',' +) ')')? 

1278 
; 

1279 
hints: monos? typeintros? typeelims? 

1280 
; 

1281 
\end{rail} 

1282 

1283 
See \cite{isabelleZF} for further information on inductive definitions in 

1284 
HOL, but note that this covers the oldstyle theory format. 

12621  1285 

13024  1286 

1287 
\subsubsection{Primitive recursive functions} 

1288 

1289 
\indexisarcmdof{ZF}{primrec} 

1290 
\begin{matharray}{rcl} 

1291 
\isarcmd{primrec} & : & \isartrans{theory}{theory} \\ 

1292 
\end{matharray} 

1293 

1294 
\begin{rail} 

1295 
'primrec' (thmdecl? prop +) 

1296 
; 

1297 
\end{rail} 

1298 

1299 

13042  1300 
\subsubsection{Cases and induction: emulating tactic scripts} 
13024  1301 

1302 
The following important tactical tools of Isabelle/ZF have been ported to 

1303 
Isar. These should be never used in proper proof texts! 

1304 

1305 
\indexisarmethof{ZF}{casetac}\indexisarmethof{ZF}{inducttac} 

1306 
\indexisarmethof{ZF}{indcases}\indexisarcmdof{ZF}{inductivecases} 

1307 
\begin{matharray}{rcl} 

1308 
case_tac^* & : & \isarmeth \\ 

1309 
induct_tac^* & : & \isarmeth \\ 

1310 
ind_cases^* & : & \isarmeth \\ 

1311 
\isarcmd{inductive_cases} & : & \isartrans{theory}{theory} \\ 

1312 
\end{matharray} 

1313 

1314 
\begin{rail} 

1315 
(casetac  inducttac) goalspec? name 

1316 
; 

1317 
indcases (prop +) 

1318 
; 

1319 
inductivecases (thmdecl? (prop +) + 'and') 

1320 
; 

1321 
\end{rail} 

12621  1322 

13014  1323 
%%% Local Variables: 
12621  1324 
%%% mode: latex 
1325 
%%% TeXmaster: "isarref" 

13014  1326 
%%% End: 