1 |
|
2 \chapter{Object-logic specific elements}\label{ch:logics} |
|
3 |
|
4 \section{HOL} |
|
5 |
|
6 \subsection{Primitive types}\label{sec:hol-typedef} |
|
7 |
|
8 \indexisarcmdof{HOL}{typedecl}\indexisarcmdof{HOL}{typedef} |
|
9 \begin{matharray}{rcl} |
|
10 \isarcmd{typedecl} & : & \isartrans{theory}{theory} \\ |
|
11 \isarcmd{typedef} & : & \isartrans{theory}{proof(prove)} \\ |
|
12 \end{matharray} |
|
13 |
|
14 \begin{rail} |
|
15 'typedecl' typespec infix? |
|
16 ; |
|
17 'typedef' altname? abstype '=' repset |
|
18 ; |
|
19 |
|
20 altname: '(' (name | 'open' | 'open' name) ')' |
|
21 ; |
|
22 abstype: typespec infix? |
|
23 ; |
|
24 repset: term ('morphisms' name name)? |
|
25 ; |
|
26 \end{rail} |
|
27 |
|
28 \begin{descr} |
|
29 |
|
30 \item [$\isarkeyword{typedecl}~(\vec\alpha)t$] is similar to the original |
|
31 $\isarkeyword{typedecl}$ of Isabelle/Pure (see \S\ref{sec:types-pure}), but |
|
32 also declares type arity $t :: (type, \dots, type) type$, making $t$ an |
|
33 actual HOL type constructor. |
|
34 |
|
35 \item [$\isarkeyword{typedef}~(\vec\alpha)t = A$] sets up a goal stating |
|
36 non-emptiness of the set $A$. After finishing the proof, the theory will be |
|
37 augmented by a Gordon/HOL-style type definition, which establishes a |
|
38 bijection between the representing set $A$ and the new type $t$. |
|
39 |
|
40 Technically, $\isarkeyword{typedef}$ defines both a type $t$ and a set (term |
|
41 constant) of the same name (an alternative base name may be given in |
|
42 parentheses). The injection from type to set is called $Rep_t$, its inverse |
|
43 $Abs_t$ (this may be changed via an explicit $\isarkeyword{morphisms}$ |
|
44 declaration). |
|
45 |
|
46 Theorems $Rep_t$, $Rep_t_inverse$, and $Abs_t_inverse$ provide the most |
|
47 basic characterization as a corresponding injection/surjection pair (in both |
|
48 directions). Rules $Rep_t_inject$ and $Abs_t_inject$ provide a slightly |
|
49 more convenient view on the injectivity part, suitable for automated proof |
|
50 tools (e.g.\ in $simp$ or $iff$ declarations). Rules |
|
51 $Rep_t_cases/Rep_t_induct$, and $Abs_t_cases/Abs_t_induct$ provide |
|
52 alternative views on surjectivity; these are already declared as set or type |
|
53 rules for the generic $cases$ and $induct$ methods. |
|
54 |
|
55 An alternative name may be specified in parentheses; the default is to use |
|
56 $t$ as indicated before. The $open$ declaration suppresses a separate |
|
57 constant definition for the representing set. |
|
58 \end{descr} |
|
59 |
|
60 Note that raw type declarations are rarely used in practice; the main |
|
61 application is with experimental (or even axiomatic!) theory fragments. |
|
62 Instead of primitive HOL type definitions, user-level theories usually refer |
|
63 to higher-level packages such as $\isarkeyword{record}$ (see |
|
64 \S\ref{sec:hol-record}) or $\isarkeyword{datatype}$ (see |
|
65 \S\ref{sec:hol-datatype}). |
|
66 |
|
67 |
|
68 \subsection{Adhoc tuples} |
|
69 |
|
70 \indexisarattof{HOL}{split-format} |
|
71 \begin{matharray}{rcl} |
|
72 split_format^* & : & \isaratt \\ |
|
73 \end{matharray} |
|
74 |
|
75 \railalias{splitformat}{split\_format} |
|
76 \railterm{splitformat} |
|
77 |
|
78 \begin{rail} |
|
79 splitformat (((name *) + 'and') | ('(' 'complete' ')')) |
|
80 ; |
|
81 \end{rail} |
|
82 |
|
83 \begin{descr} |
|
84 |
|
85 \item [$split_format~\vec p@1 \dots \vec p@n$] puts expressions of low-level |
|
86 tuple types into canonical form as specified by the arguments given; $\vec |
|
87 p@i$ refers to occurrences in premise $i$ of the rule. The ``$(complete)$'' |
|
88 option causes \emph{all} arguments in function applications to be |
|
89 represented canonically according to their tuple type structure. |
|
90 |
|
91 Note that these operations tend to invent funny names for new local |
|
92 parameters to be introduced. |
|
93 |
|
94 \end{descr} |
|
95 |
|
96 |
|
97 \subsection{Records}\label{sec:hol-record} |
|
98 |
|
99 In principle, records merely generalize the concept of tuples, where |
|
100 components may be addressed by labels instead of just position. The logical |
|
101 infrastructure of records in Isabelle/HOL is slightly more advanced, though, |
|
102 supporting truly extensible record schemes. This admits operations that are |
|
103 polymorphic with respect to record extension, yielding ``object-oriented'' |
|
104 effects like (single) inheritance. See also \cite{NaraschewskiW-TPHOLs98} for |
|
105 more details on object-oriented verification and record subtyping in HOL. |
|
106 |
|
107 |
|
108 \subsubsection{Basic concepts} |
|
109 |
|
110 Isabelle/HOL supports both \emph{fixed} and \emph{schematic} records at the |
|
111 level of terms and types. The notation is as follows: |
|
112 |
|
113 \begin{center} |
|
114 \begin{tabular}{l|l|l} |
|
115 & record terms & record types \\ \hline |
|
116 fixed & $\record{x = a\fs y = b}$ & $\record{x \ty A\fs y \ty B}$ \\ |
|
117 schematic & $\record{x = a\fs y = b\fs \more = m}$ & |
|
118 $\record{x \ty A\fs y \ty B\fs \more \ty M}$ \\ |
|
119 \end{tabular} |
|
120 \end{center} |
|
121 |
|
122 \noindent The ASCII representation of $\record{x = a}$ is \texttt{(| x = a |)}. |
|
123 |
|
124 A fixed record $\record{x = a\fs y = b}$ has field $x$ of value $a$ and field |
|
125 $y$ of value $b$. The corresponding type is $\record{x \ty A\fs y \ty B}$, |
|
126 assuming that $a \ty A$ and $b \ty B$. |
|
127 |
|
128 A record scheme like $\record{x = a\fs y = b\fs \more = m}$ contains fields |
|
129 $x$ and $y$ as before, but also possibly further fields as indicated by the |
|
130 ``$\more$'' notation (which is actually part of the syntax). The improper |
|
131 field ``$\more$'' of a record scheme is called the \emph{more part}. |
|
132 Logically it is just a free variable, which is occasionally referred to as |
|
133 ``row variable'' in the literature. The more part of a record scheme may be |
|
134 instantiated by zero or more further components. For example, the previous |
|
135 scheme may get instantiated to $\record{x = a\fs y = b\fs z = c\fs \more = |
|
136 m'}$, where $m'$ refers to a different more part. Fixed records are special |
|
137 instances of record schemes, where ``$\more$'' is properly terminated by the |
|
138 $() :: unit$ element. Actually, $\record{x = a\fs y = b}$ is just an |
|
139 abbreviation for $\record{x = a\fs y = b\fs \more = ()}$. |
|
140 |
|
141 \medskip |
|
142 |
|
143 Two key observations make extensible records in a simply typed language like |
|
144 HOL feasible: |
|
145 \begin{enumerate} |
|
146 \item the more part is internalized, as a free term or type variable, |
|
147 \item field names are externalized, they cannot be accessed within the logic |
|
148 as first-class values. |
|
149 \end{enumerate} |
|
150 |
|
151 \medskip |
|
152 |
|
153 In Isabelle/HOL record types have to be defined explicitly, fixing their field |
|
154 names and types, and their (optional) parent record. Afterwards, records may |
|
155 be formed using above syntax, while obeying the canonical order of fields as |
|
156 given by their declaration. The record package provides several standard |
|
157 operations like selectors and updates. The common setup for various generic |
|
158 proof tools enable succinct reasoning patterns. See also the Isabelle/HOL |
|
159 tutorial \cite{isabelle-hol-book} for further instructions on using records in |
|
160 practice. |
|
161 |
|
162 |
|
163 \subsubsection{Record specifications} |
|
164 |
|
165 \indexisarcmdof{HOL}{record} |
|
166 \begin{matharray}{rcl} |
|
167 \isarcmd{record} & : & \isartrans{theory}{theory} \\ |
|
168 \end{matharray} |
|
169 |
|
170 \begin{rail} |
|
171 'record' typespec '=' (type '+')? (constdecl +) |
|
172 ; |
|
173 \end{rail} |
|
174 |
|
175 \begin{descr} |
|
176 \item [$\isarkeyword{record}~(\vec\alpha)t = \tau + \vec c :: \vec\sigma$] |
|
177 defines extensible record type $(\vec\alpha)t$, derived from the optional |
|
178 parent record $\tau$ by adding new field components $\vec c :: \vec\sigma$. |
|
179 |
|
180 The type variables of $\tau$ and $\vec\sigma$ need to be covered by the |
|
181 (distinct) parameters $\vec\alpha$. Type constructor $t$ has to be new, |
|
182 while $\tau$ needs to specify an instance of an existing record type. At |
|
183 least one new field $\vec c$ has to be specified. Basically, field names |
|
184 need to belong to a unique record. This is not a real restriction in |
|
185 practice, since fields are qualified by the record name internally. |
|
186 |
|
187 The parent record specification $\tau$ is optional; if omitted $t$ becomes a |
|
188 root record. The hierarchy of all records declared within a theory context |
|
189 forms a forest structure, i.e.\ a set of trees starting with a root record |
|
190 each. There is no way to merge multiple parent records! |
|
191 |
|
192 For convenience, $(\vec\alpha) \, t$ is made a type abbreviation for the |
|
193 fixed record type $\record{\vec c \ty \vec\sigma}$, likewise is |
|
194 $(\vec\alpha, \zeta) \, t_scheme$ made an abbreviation for $\record{\vec c |
|
195 \ty \vec\sigma\fs \more \ty \zeta}$. |
|
196 |
|
197 \end{descr} |
|
198 |
|
199 \subsubsection{Record operations} |
|
200 |
|
201 Any record definition of the form presented above produces certain standard |
|
202 operations. Selectors and updates are provided for any field, including the |
|
203 improper one ``$more$''. There are also cumulative record constructor |
|
204 functions. To simplify the presentation below, we assume for now that |
|
205 $(\vec\alpha) \, t$ is a root record with fields $\vec c \ty \vec\sigma$. |
|
206 |
|
207 \medskip \textbf{Selectors} and \textbf{updates} are available for any field |
|
208 (including ``$more$''): |
|
209 \begin{matharray}{lll} |
|
210 c@i & \ty & \record{\vec c \ty \vec \sigma, \more \ty \zeta} \To \sigma@i \\ |
|
211 c@i_update & \ty & \sigma@i \To \record{\vec c \ty \vec\sigma, \more \ty \zeta} \To |
|
212 \record{\vec c \ty \vec\sigma, \more \ty \zeta} |
|
213 \end{matharray} |
|
214 |
|
215 There is special syntax for application of updates: $r \, \record{x \asn a}$ |
|
216 abbreviates term $x_update \, a \, r$. Further notation for repeated updates |
|
217 is also available: $r \, \record{x \asn a} \, \record{y \asn b} \, \record{z |
|
218 \asn c}$ may be written $r \, \record{x \asn a\fs y \asn b\fs z \asn c}$. |
|
219 Note that because of postfix notation the order of fields shown here is |
|
220 reverse than in the actual term. Since repeated updates are just function |
|
221 applications, fields may be freely permuted in $\record{x \asn a\fs y \asn |
|
222 b\fs z \asn c}$, as far as logical equality is concerned. Thus |
|
223 commutativity of independent updates can be proven within the logic for any |
|
224 two fields, but not as a general theorem. |
|
225 |
|
226 \medskip The \textbf{make} operation provides a cumulative record constructor |
|
227 function: |
|
228 \begin{matharray}{lll} |
|
229 t{\dtt}make & \ty & \vec\sigma \To \record{\vec c \ty \vec \sigma} \\ |
|
230 \end{matharray} |
|
231 |
|
232 \medskip We now reconsider the case of non-root records, which are derived of |
|
233 some parent. In general, the latter may depend on another parent as well, |
|
234 resulting in a list of \emph{ancestor records}. Appending the lists of fields |
|
235 of all ancestors results in a certain field prefix. The record package |
|
236 automatically takes care of this by lifting operations over this context of |
|
237 ancestor fields. Assuming that $(\vec\alpha) \, t$ has ancestor fields $\vec |
|
238 b \ty \vec\rho$, the above record operations will get the following types: |
|
239 \begin{matharray}{lll} |
|
240 c@i & \ty & \record{\vec b \ty \vec\rho, \vec c \ty \vec\sigma, \more \ty |
|
241 \zeta} \To \sigma@i \\ |
|
242 c@i_update & \ty & \sigma@i \To |
|
243 \record{\vec b \ty \vec\rho, \vec c \ty \vec\sigma, \more \ty \zeta} \To |
|
244 \record{\vec b \ty \vec\rho, \vec c \ty \vec\sigma, \more \ty \zeta} \\ |
|
245 t{\dtt}make & \ty & \vec\rho \To \vec\sigma \To |
|
246 \record{\vec b \ty \vec\rho, \vec c \ty \vec \sigma} \\ |
|
247 \end{matharray} |
|
248 \noindent |
|
249 |
|
250 \medskip Some further operations address the extension aspect of a derived |
|
251 record scheme specifically: $fields$ produces a record fragment consisting of |
|
252 exactly the new fields introduced here (the result may serve as a more part |
|
253 elsewhere); $extend$ takes a fixed record and adds a given more part; |
|
254 $truncate$ restricts a record scheme to a fixed record. |
|
255 |
|
256 \begin{matharray}{lll} |
|
257 t{\dtt}fields & \ty & \vec\sigma \To \record{\vec c \ty \vec \sigma} \\ |
|
258 t{\dtt}extend & \ty & \record{\vec d \ty \vec \rho, \vec c \ty \vec\sigma} \To |
|
259 \zeta \To \record{\vec d \ty \vec \rho, \vec c \ty \vec\sigma, \more \ty \zeta} \\ |
|
260 t{\dtt}truncate & \ty & \record{\vec d \ty \vec \rho, \vec c \ty \vec\sigma, \more \ty \zeta} \To |
|
261 \record{\vec d \ty \vec \rho, \vec c \ty \vec\sigma} \\ |
|
262 \end{matharray} |
|
263 |
|
264 \noindent Note that $t{\dtt}make$ and $t{\dtt}fields$ actually coincide for root records. |
|
265 |
|
266 |
|
267 \subsubsection{Derived rules and proof tools} |
|
268 |
|
269 The record package proves several results internally, declaring these facts to |
|
270 appropriate proof tools. This enables users to reason about record structures |
|
271 quite conveniently. Assume that $t$ is a record type as specified above. |
|
272 |
|
273 \begin{enumerate} |
|
274 |
|
275 \item Standard conversions for selectors or updates applied to record |
|
276 constructor terms are made part of the default Simplifier context; thus |
|
277 proofs by reduction of basic operations merely require the $simp$ method |
|
278 without further arguments. These rules are available as $t{\dtt}simps$, |
|
279 too. |
|
280 |
|
281 \item Selectors applied to updated records are automatically reduced by an |
|
282 internal simplification procedure, which is also part of the standard |
|
283 Simplifier setup. |
|
284 |
|
285 \item Inject equations of a form analogous to $((x, y) = (x', y')) \equiv x=x' |
|
286 \conj y=y'$ are declared to the Simplifier and Classical Reasoner as $iff$ |
|
287 rules. These rules are available as $t{\dtt}iffs$. |
|
288 |
|
289 \item The introduction rule for record equality analogous to $x~r = x~r' \Imp |
|
290 y~r = y~r' \Imp \dots \Imp r = r'$ is declared to the Simplifier, and as the |
|
291 basic rule context as ``$intro?$''. The rule is called $t{\dtt}equality$. |
|
292 |
|
293 \item Representations of arbitrary record expressions as canonical constructor |
|
294 terms are provided both in $cases$ and $induct$ format (cf.\ the generic |
|
295 proof methods of the same name, \S\ref{sec:cases-induct}). Several |
|
296 variations are available, for fixed records, record schemes, more parts etc. |
|
297 |
|
298 The generic proof methods are sufficiently smart to pick the most sensible |
|
299 rule according to the type of the indicated record expression: users just |
|
300 need to apply something like ``$(cases~r)$'' to a certain proof problem. |
|
301 |
|
302 \item The derived record operations $t{\dtt}make$, $t{\dtt}fields$, |
|
303 $t{\dtt}extend$, $t{\dtt}truncate$ are \emph{not} treated automatically, but |
|
304 usually need to be expanded by hand, using the collective fact |
|
305 $t{\dtt}defs$. |
|
306 |
|
307 \end{enumerate} |
|
308 |
|
309 |
|
310 \subsection{Datatypes}\label{sec:hol-datatype} |
|
311 |
|
312 \indexisarcmdof{HOL}{datatype}\indexisarcmdof{HOL}{rep-datatype} |
|
313 \begin{matharray}{rcl} |
|
314 \isarcmd{datatype} & : & \isartrans{theory}{theory} \\ |
|
315 \isarcmd{rep_datatype} & : & \isartrans{theory}{theory} \\ |
|
316 \end{matharray} |
|
317 |
|
318 \railalias{repdatatype}{rep\_datatype} |
|
319 \railterm{repdatatype} |
|
320 |
|
321 \begin{rail} |
|
322 'datatype' (dtspec + 'and') |
|
323 ; |
|
324 repdatatype (name *) dtrules |
|
325 ; |
|
326 |
|
327 dtspec: parname? typespec infix? '=' (cons + '|') |
|
328 ; |
|
329 cons: name (type *) mixfix? |
|
330 ; |
|
331 dtrules: 'distinct' thmrefs 'inject' thmrefs 'induction' thmrefs |
|
332 \end{rail} |
|
333 |
|
334 \begin{descr} |
|
335 \item [$\isarkeyword{datatype}$] defines inductive datatypes in HOL. |
|
336 \item [$\isarkeyword{rep_datatype}$] represents existing types as inductive |
|
337 ones, generating the standard infrastructure of derived concepts (primitive |
|
338 recursion etc.). |
|
339 \end{descr} |
|
340 |
|
341 The induction and exhaustion theorems generated provide case names according |
|
342 to the constructors involved, while parameters are named after the types (see |
|
343 also \S\ref{sec:cases-induct}). |
|
344 |
|
345 See \cite{isabelle-HOL} for more details on datatypes, but beware of the |
|
346 old-style theory syntax being used there! Apart from proper proof methods for |
|
347 case-analysis and induction, there are also emulations of ML tactics |
|
348 \texttt{case_tac} and \texttt{induct_tac} available, see |
|
349 \S\ref{sec:hol-induct-tac}; these admit to refer directly to the internal |
|
350 structure of subgoals (including internally bound parameters). |
|
351 |
|
352 |
|
353 \subsection{Recursive functions}\label{sec:recursion} |
|
354 |
|
355 \indexisarcmdof{HOL}{primrec}\indexisarcmdof{HOL}{fun}\indexisarcmdof{HOL}{function}\indexisarcmdof{HOL}{termination} |
|
356 |
|
357 \begin{matharray}{rcl} |
|
358 \isarcmd{primrec} & : & \isarkeep{local{\dsh}theory} \\ |
|
359 \isarcmd{fun} & : & \isarkeep{local{\dsh}theory} \\ |
|
360 \isarcmd{function} & : & \isartrans{local{\dsh}theory}{proof(prove)} \\ |
|
361 \isarcmd{termination} & : & \isartrans{local{\dsh}theory}{proof(prove)} \\ |
|
362 \end{matharray} |
|
363 |
|
364 \railalias{funopts}{function\_opts} |
|
365 |
|
366 \begin{rail} |
|
367 'primrec' target? fixes 'where' equations |
|
368 ; |
|
369 equations: (thmdecl? prop + '|') |
|
370 ; |
|
371 ('fun' | 'function') (funopts)? fixes 'where' clauses |
|
372 ; |
|
373 clauses: (thmdecl? prop ('(' 'otherwise' ')')? + '|') |
|
374 ; |
|
375 funopts: '(' (('sequential' | 'in' name | 'domintros' | 'tailrec' | |
|
376 'default' term) + ',') ')' |
|
377 ; |
|
378 'termination' ( term )? |
|
379 \end{rail} |
|
380 |
|
381 \begin{descr} |
|
382 |
|
383 \item [$\isarkeyword{primrec}$] defines primitive recursive functions over |
|
384 datatypes, see also \cite{isabelle-HOL}. |
|
385 |
|
386 \item [$\isarkeyword{function}$] defines functions by general |
|
387 wellfounded recursion. A detailed description with examples can be |
|
388 found in \cite{isabelle-function}. The function is specified by a |
|
389 set of (possibly conditional) recursive equations with arbitrary |
|
390 pattern matching. The command generates proof obligations for the |
|
391 completeness and the compatibility of patterns. |
|
392 |
|
393 The defined function is considered partial, and the resulting |
|
394 simplification rules (named $f.psimps$) and induction rule (named |
|
395 $f.pinduct$) are guarded by a generated domain predicate $f_dom$. |
|
396 The $\isarkeyword{termination}$ command can then be used to establish |
|
397 that the function is total. |
|
398 |
|
399 \item [$\isarkeyword{fun}$] is a shorthand notation for |
|
400 $\isarkeyword{function}~(\textit{sequential})$, followed by automated |
|
401 proof attemts regarding pattern matching and termination. For |
|
402 details, see \cite{isabelle-function}. |
|
403 |
|
404 \item [$\isarkeyword{termination}$~f] commences a termination proof |
|
405 for the previously defined function $f$. If no name is given, it |
|
406 refers to the most recent function definition. After the proof is |
|
407 closed, the recursive equations and the induction principle is established. |
|
408 \end{descr} |
|
409 |
|
410 Recursive definitions introduced by both the $\isarkeyword{primrec}$ |
|
411 and the $\isarkeyword{function}$ command accommodate reasoning by |
|
412 induction (cf.\ \S\ref{sec:cases-induct}): rule $c\mathord{.}induct$ |
|
413 (where $c$ is the name of the function definition) refers to a |
|
414 specific induction rule, with parameters named according to the |
|
415 user-specified equations. Case names of $\isarkeyword{primrec}$ are |
|
416 that of the datatypes involved, while those of |
|
417 $\isarkeyword{function}$ are numbered (starting from $1$). |
|
418 |
|
419 The equations provided by these packages may be referred later as theorem list |
|
420 $f{\dtt}simps$, where $f$ is the (collective) name of the functions defined. |
|
421 Individual equations may be named explicitly as well. |
|
422 |
|
423 The $\isarkeyword{function}$ command accepts the following options: |
|
424 |
|
425 \begin{descr} |
|
426 \item [\emph{sequential}] enables a preprocessor which disambiguates |
|
427 overlapping patterns by making them mutually disjoint. Earlier |
|
428 equations take precedence over later ones. This allows to give the |
|
429 specification in a format very similar to functional programming. |
|
430 Note that the resulting simplification and induction rules |
|
431 correspond to the transformed specification, not the one given |
|
432 originally. This usually means that each equation given by the user |
|
433 may result in several theroems. |
|
434 Also note that this automatic transformation only works |
|
435 for ML-style datatype patterns. |
|
436 |
|
437 |
|
438 \item [\emph{in name}] gives the target for the definition. |
|
439 |
|
440 \item [\emph{domintros}] enables the automated generation of |
|
441 introduction rules for the domain predicate. While mostly not |
|
442 needed, they can be helpful in some proofs about partial functions. |
|
443 |
|
444 \item [\emph{tailrec}] generates the unconstrained recursive equations |
|
445 even without a termination proof, provided that the function is |
|
446 tail-recursive. This currently only works |
|
447 |
|
448 \item [\emph{default d}] allows to specify a default value for a |
|
449 (partial) function, which will ensure that $f(x)=d(x)$ whenever $x |
|
450 \notin \textit{f\_dom}$. This feature is experimental. |
|
451 \end{descr} |
|
452 |
|
453 \subsubsection{Proof methods related to recursive definitions} |
|
454 |
|
455 \indexisarmethof{HOL}{pat-completeness} |
|
456 \indexisarmethof{HOL}{relation} |
|
457 \indexisarmethof{HOL}{lexicographic-order} |
|
458 |
|
459 \begin{matharray}{rcl} |
|
460 pat\_completeness & : & \isarmeth \\ |
|
461 relation & : & \isarmeth \\ |
|
462 lexicographic\_order & : & \isarmeth \\ |
|
463 \end{matharray} |
|
464 |
|
465 \begin{rail} |
|
466 'pat\_completeness' |
|
467 ; |
|
468 'relation' term |
|
469 ; |
|
470 'lexicographic\_order' clasimpmod |
|
471 \end{rail} |
|
472 |
|
473 \begin{descr} |
|
474 \item [\emph{pat\_completeness}] Specialized method to solve goals |
|
475 regarding the completeness of pattern matching, as required by the |
|
476 $\isarkeyword{function}$ package (cf.~\cite{isabelle-function}). |
|
477 |
|
478 \item [\emph{relation R}] Introduces a termination proof using the |
|
479 relation $R$. The resulting proof state will contain goals |
|
480 expressing that $R$ is wellfounded, and that the arguments |
|
481 of recursive calls decrease with respect to $R$. Usually, this |
|
482 method is used as the initial proof step of manual termination |
|
483 proofs. |
|
484 |
|
485 \item [\emph{lexicographic\_order}] Attempts a fully automated |
|
486 termination proof by searching for a lexicographic combination of |
|
487 size measures on the arguments of the function. The method |
|
488 accepts the same arguments as the \emph{auto} method, which it uses |
|
489 internally to prove local descents. Hence, modifiers like |
|
490 \emph{simp}, \emph{intro} etc.\ can be used to add ``hints'' for the |
|
491 automated proofs. In case of failure, extensive information is |
|
492 printed, which can help to analyse the failure (cf.~\cite{isabelle-function}). |
|
493 \end{descr} |
|
494 |
|
495 \subsubsection{Legacy recursion package} |
|
496 \indexisarcmdof{HOL}{recdef}\indexisarcmdof{HOL}{recdef-tc} |
|
497 |
|
498 The use of the legacy $\isarkeyword{recdef}$ command is now deprecated |
|
499 in favour of $\isarkeyword{function}$ and $\isarkeyword{fun}$. |
|
500 |
|
501 \begin{matharray}{rcl} |
|
502 \isarcmd{recdef} & : & \isartrans{theory}{theory} \\ |
|
503 \isarcmd{recdef_tc}^* & : & \isartrans{theory}{proof(prove)} \\ |
|
504 \end{matharray} |
|
505 |
|
506 \railalias{recdefsimp}{recdef\_simp} |
|
507 \railterm{recdefsimp} |
|
508 |
|
509 \railalias{recdefcong}{recdef\_cong} |
|
510 \railterm{recdefcong} |
|
511 |
|
512 \railalias{recdefwf}{recdef\_wf} |
|
513 \railterm{recdefwf} |
|
514 |
|
515 \railalias{recdeftc}{recdef\_tc} |
|
516 \railterm{recdeftc} |
|
517 |
|
518 \begin{rail} |
|
519 'recdef' ('(' 'permissive' ')')? \\ name term (prop +) hints? |
|
520 ; |
|
521 recdeftc thmdecl? tc |
|
522 ; |
|
523 hints: '(' 'hints' (recdefmod *) ')' |
|
524 ; |
|
525 recdefmod: ((recdefsimp | recdefcong | recdefwf) (() | 'add' | 'del') ':' thmrefs) | clasimpmod |
|
526 ; |
|
527 tc: nameref ('(' nat ')')? |
|
528 ; |
|
529 \end{rail} |
|
530 |
|
531 \begin{descr} |
|
532 |
|
533 \item [$\isarkeyword{recdef}$] defines general well-founded recursive |
|
534 functions (using the TFL package), see also \cite{isabelle-HOL}. The |
|
535 ``$(permissive)$'' option tells TFL to recover from failed proof attempts, |
|
536 returning unfinished results. The $recdef_simp$, $recdef_cong$, and |
|
537 $recdef_wf$ hints refer to auxiliary rules to be used in the internal |
|
538 automated proof process of TFL. Additional $clasimpmod$ declarations (cf.\ |
|
539 \S\ref{sec:clasimp}) may be given to tune the context of the Simplifier |
|
540 (cf.\ \S\ref{sec:simplifier}) and Classical reasoner (cf.\ |
|
541 \S\ref{sec:classical}). |
|
542 |
|
543 \item [$\isarkeyword{recdef_tc}~c~(i)$] recommences the proof for leftover |
|
544 termination condition number $i$ (default $1$) as generated by a |
|
545 $\isarkeyword{recdef}$ definition of constant $c$. |
|
546 |
|
547 Note that in most cases, $\isarkeyword{recdef}$ is able to finish its |
|
548 internal proofs without manual intervention. |
|
549 |
|
550 \end{descr} |
|
551 |
|
552 \medskip Hints for $\isarkeyword{recdef}$ may be also declared globally, using |
|
553 the following attributes. |
|
554 |
|
555 \indexisarattof{HOL}{recdef-simp}\indexisarattof{HOL}{recdef-cong}\indexisarattof{HOL}{recdef-wf} |
|
556 \begin{matharray}{rcl} |
|
557 recdef_simp & : & \isaratt \\ |
|
558 recdef_cong & : & \isaratt \\ |
|
559 recdef_wf & : & \isaratt \\ |
|
560 \end{matharray} |
|
561 |
|
562 \railalias{recdefsimp}{recdef\_simp} |
|
563 \railterm{recdefsimp} |
|
564 |
|
565 \railalias{recdefcong}{recdef\_cong} |
|
566 \railterm{recdefcong} |
|
567 |
|
568 \railalias{recdefwf}{recdef\_wf} |
|
569 \railterm{recdefwf} |
|
570 |
|
571 \begin{rail} |
|
572 (recdefsimp | recdefcong | recdefwf) (() | 'add' | 'del') |
|
573 ; |
|
574 \end{rail} |
|
575 |
|
576 \subsection{Definition by specification}\label{sec:hol-specification} |
|
577 |
|
578 \indexisarcmdof{HOL}{specification} |
|
579 \begin{matharray}{rcl} |
|
580 \isarcmd{specification} & : & \isartrans{theory}{proof(prove)} \\ |
|
581 \isarcmd{ax_specification} & : & \isartrans{theory}{proof(prove)} \\ |
|
582 \end{matharray} |
|
583 |
|
584 \begin{rail} |
|
585 ('specification' | 'ax\_specification') '(' (decl +) ')' \\ (thmdecl? prop +) |
|
586 ; |
|
587 decl: ((name ':')? term '(' 'overloaded' ')'?) |
|
588 \end{rail} |
|
589 |
|
590 \begin{descr} |
|
591 \item [$\isarkeyword{specification}~decls~\phi$] sets up a goal stating |
|
592 the existence of terms with the properties specified to hold for the |
|
593 constants given in $\mathit{decls}$. After finishing the proof, the |
|
594 theory will be augmented with definitions for the given constants, |
|
595 as well as with theorems stating the properties for these constants. |
|
596 \item [$\isarkeyword{ax_specification}~decls~\phi$] sets up a goal stating |
|
597 the existence of terms with the properties specified to hold for the |
|
598 constants given in $\mathit{decls}$. After finishing the proof, the |
|
599 theory will be augmented with axioms expressing the properties given |
|
600 in the first place. |
|
601 \item[$decl$] declares a constant to be defined by the specification |
|
602 given. The definition for the constant $c$ is bound to the name |
|
603 $c$\_def unless a theorem name is given in the declaration. |
|
604 Overloaded constants should be declared as such. |
|
605 \end{descr} |
|
606 |
|
607 Whether to use $\isarkeyword{specification}$ or $\isarkeyword{ax_specification}$ |
|
608 is to some extent a matter of style. $\isarkeyword{specification}$ introduces no new axioms, |
|
609 and so by construction cannot introduce inconsistencies, whereas $\isarkeyword{ax_specification}$ |
|
610 does introduce axioms, but only after the user has explicitly proven it to be |
|
611 safe. A practical issue must be considered, though: After introducing two constants |
|
612 with the same properties using $\isarkeyword{specification}$, one can prove |
|
613 that the two constants are, in fact, equal. If this might be a problem, |
|
614 one should use $\isarkeyword{ax_specification}$. |
|
615 |
|
616 \subsection{Inductive and coinductive definitions}\label{sec:hol-inductive} |
|
617 |
|
618 An {\bf inductive definition} specifies the least predicate (or set) $R$ closed under given |
|
619 rules. (Applying a rule to elements of~$R$ yields a result within~$R$.) For |
|
620 example, a structural operational semantics is an inductive definition of an |
|
621 evaluation relation. Dually, a {\bf coinductive definition} specifies the |
|
622 greatest predicate (or set) $R$ consistent with given rules. (Every element of~$R$ can be |
|
623 seen as arising by applying a rule to elements of~$R$.) An important example |
|
624 is using bisimulation relations to formalise equivalence of processes and |
|
625 infinite data structures. |
|
626 |
|
627 This package is related to the ZF one, described in a separate |
|
628 paper,% |
|
629 \footnote{It appeared in CADE~\cite{paulson-CADE}; a longer version is |
|
630 distributed with Isabelle.} % |
|
631 which you should refer to in case of difficulties. The package is simpler |
|
632 than ZF's thanks to HOL's extra-logical automatic type-checking. The types of |
|
633 the (co)inductive predicates (or sets) determine the domain of the fixedpoint definition, and |
|
634 the package does not have to use inference rules for type-checking. |
|
635 |
|
636 \indexisarcmdof{HOL}{inductive}\indexisarcmdof{HOL}{inductive-set}\indexisarcmdof{HOL}{coinductive}\indexisarcmdof{HOL}{coinductive-set}\indexisarattof{HOL}{mono} |
|
637 \begin{matharray}{rcl} |
|
638 \isarcmd{inductive} & : & \isarkeep{local{\dsh}theory} \\ |
|
639 \isarcmd{inductive_set} & : & \isarkeep{local{\dsh}theory} \\ |
|
640 \isarcmd{coinductive} & : & \isarkeep{local{\dsh}theory} \\ |
|
641 \isarcmd{coinductive_set} & : & \isarkeep{local{\dsh}theory} \\ |
|
642 mono & : & \isaratt \\ |
|
643 \end{matharray} |
|
644 |
|
645 \begin{rail} |
|
646 ('inductive' | 'inductive\_set' | 'coinductive' | 'coinductive\_set') target? fixes ('for' fixes)? \\ |
|
647 ('where' clauses)? ('monos' thmrefs)? |
|
648 ; |
|
649 clauses: (thmdecl? prop + '|') |
|
650 ; |
|
651 'mono' (() | 'add' | 'del') |
|
652 ; |
|
653 \end{rail} |
|
654 |
|
655 \begin{descr} |
|
656 \item [$\isarkeyword{inductive}$ and $\isarkeyword{coinductive}$] define |
|
657 (co)inductive predicates from the introduction rules given in the \texttt{where} section. |
|
658 The optional \texttt{for} section contains a list of parameters of the (co)inductive |
|
659 predicates that remain fixed throughout the definition. |
|
660 The optional \texttt{monos} section contains \textit{monotonicity theorems}, |
|
661 which are required for each operator applied to a recursive set in the introduction rules. |
|
662 There {\bf must} be a theorem of the form $A \leq B \Imp M~A \leq M~B$, for each |
|
663 premise $M~R@i~t$ in an introduction rule! |
|
664 \item [$\isarkeyword{inductive_set}$ and $\isarkeyword{coinductive_set}$] are wrappers |
|
665 for to the previous commands, allowing the definition of (co)inductive sets. |
|
666 \item [$mono$] declares monotonicity rules. These rule are involved in the |
|
667 automated monotonicity proof of $\isarkeyword{inductive}$. |
|
668 \end{descr} |
|
669 |
|
670 \subsubsection{Derived rules} |
|
671 |
|
672 Each (co)inductive definition $R$ adds definitions to the theory and also |
|
673 proves some theorems: |
|
674 \begin{description} |
|
675 \item[$R{\dtt}intros$] is the list of introduction rules, now proved as theorems, for |
|
676 the recursive predicates (or sets). The rules are also available individually, |
|
677 using the names given them in the theory file. |
|
678 \item[$R{\dtt}cases$] is the case analysis (or elimination) rule. |
|
679 \item[$R{\dtt}(co)induct$] is the (co)induction rule. |
|
680 \end{description} |
|
681 When several predicates $R@1$, $\ldots$, $R@n$ are defined simultaneously, |
|
682 the list of introduction rules is called $R@1_\ldots_R@n{\dtt}intros$, the |
|
683 case analysis rules are called $R@1{\dtt}cases$, $\ldots$, $R@n{\dtt}cases$, and |
|
684 the list of mutual induction rules is called $R@1_\ldots_R@n{\dtt}inducts$. |
|
685 |
|
686 \subsubsection{Monotonicity theorems} |
|
687 |
|
688 Each theory contains a default set of theorems that are used in monotonicity |
|
689 proofs. New rules can be added to this set via the $mono$ attribute. |
|
690 Theory \texttt{Inductive} shows how this is done. In general, the following |
|
691 monotonicity theorems may be added: |
|
692 \begin{itemize} |
|
693 \item Theorems of the form $A \leq B \Imp M~A \leq M~B$, for proving |
|
694 monotonicity of inductive definitions whose introduction rules have premises |
|
695 involving terms such as $M~R@i~t$. |
|
696 \item Monotonicity theorems for logical operators, which are of the general form |
|
697 $\List{\cdots \to \cdots;~\ldots;~\cdots \to \cdots} \Imp |
|
698 \cdots \to \cdots$. |
|
699 For example, in the case of the operator $\lor$, the corresponding theorem is |
|
700 \[ |
|
701 \infer{P@1 \lor P@2 \to Q@1 \lor Q@2} |
|
702 {P@1 \to Q@1 & P@2 \to Q@2} |
|
703 \] |
|
704 \item De Morgan style equations for reasoning about the ``polarity'' of expressions, e.g. |
|
705 \[ |
|
706 (\lnot \lnot P) ~=~ P \qquad\qquad |
|
707 (\lnot (P \land Q)) ~=~ (\lnot P \lor \lnot Q) |
|
708 \] |
|
709 \item Equations for reducing complex operators to more primitive ones whose |
|
710 monotonicity can easily be proved, e.g. |
|
711 \[ |
|
712 (P \to Q) ~=~ (\lnot P \lor Q) \qquad\qquad |
|
713 \mathtt{Ball}~A~P ~\equiv~ \forall x.~x \in A \to P~x |
|
714 \] |
|
715 \end{itemize} |
|
716 |
|
717 %FIXME: Example of an inductive definition |
|
718 |
|
719 |
|
720 \subsection{Arithmetic proof support} |
|
721 |
|
722 \indexisarmethof{HOL}{arith}\indexisarattof{HOL}{arith-split} |
|
723 \begin{matharray}{rcl} |
|
724 arith & : & \isarmeth \\ |
|
725 arith_split & : & \isaratt \\ |
|
726 \end{matharray} |
|
727 |
|
728 \begin{rail} |
|
729 'arith' '!'? |
|
730 ; |
|
731 \end{rail} |
|
732 |
|
733 The $arith$ method decides linear arithmetic problems (on types $nat$, $int$, |
|
734 $real$). Any current facts are inserted into the goal before running the |
|
735 procedure. The ``!''~argument causes the full context of assumptions to be |
|
736 included. The $arith_split$ attribute declares case split rules to be |
|
737 expanded before the arithmetic procedure is invoked. |
|
738 |
|
739 Note that a simpler (but faster) version of arithmetic reasoning is already |
|
740 performed by the Simplifier. |
|
741 |
|
742 |
|
743 \subsection{Cases and induction: emulating tactic scripts}\label{sec:hol-induct-tac} |
|
744 |
|
745 The following important tactical tools of Isabelle/HOL have been ported to |
|
746 Isar. These should be never used in proper proof texts! |
|
747 |
|
748 \indexisarmethof{HOL}{case-tac}\indexisarmethof{HOL}{induct-tac} |
|
749 \indexisarmethof{HOL}{ind-cases}\indexisarcmdof{HOL}{inductive-cases} |
|
750 \begin{matharray}{rcl} |
|
751 case_tac^* & : & \isarmeth \\ |
|
752 induct_tac^* & : & \isarmeth \\ |
|
753 ind_cases^* & : & \isarmeth \\ |
|
754 \isarcmd{inductive_cases} & : & \isartrans{theory}{theory} \\ |
|
755 \end{matharray} |
|
756 |
|
757 \railalias{casetac}{case\_tac} |
|
758 \railterm{casetac} |
|
759 |
|
760 \railalias{inducttac}{induct\_tac} |
|
761 \railterm{inducttac} |
|
762 |
|
763 \railalias{indcases}{ind\_cases} |
|
764 \railterm{indcases} |
|
765 |
|
766 \railalias{inductivecases}{inductive\_cases} |
|
767 \railterm{inductivecases} |
|
768 |
|
769 \begin{rail} |
|
770 casetac goalspec? term rule? |
|
771 ; |
|
772 inducttac goalspec? (insts * 'and') rule? |
|
773 ; |
|
774 indcases (prop +) ('for' (name +)) ? |
|
775 ; |
|
776 inductivecases (thmdecl? (prop +) + 'and') |
|
777 ; |
|
778 |
|
779 rule: ('rule' ':' thmref) |
|
780 ; |
|
781 \end{rail} |
|
782 |
|
783 \begin{descr} |
|
784 \item [$case_tac$ and $induct_tac$] admit to reason about inductive datatypes |
|
785 only (unless an alternative rule is given explicitly). Furthermore, |
|
786 $case_tac$ does a classical case split on booleans; $induct_tac$ allows only |
|
787 variables to be given as instantiation. These tactic emulations feature |
|
788 both goal addressing and dynamic instantiation. Note that named rule cases |
|
789 are \emph{not} provided as would be by the proper $induct$ and $cases$ proof |
|
790 methods (see \S\ref{sec:cases-induct}). |
|
791 |
|
792 \item [$ind_cases$ and $\isarkeyword{inductive_cases}$] provide an interface |
|
793 to the internal \texttt{mk_cases} operation. Rules are simplified in an |
|
794 unrestricted forward manner. |
|
795 |
|
796 While $ind_cases$ is a proof method to apply the result immediately as |
|
797 elimination rules, $\isarkeyword{inductive_cases}$ provides case split |
|
798 theorems at the theory level for later use. |
|
799 The \texttt{for} option of the $ind_cases$ method allows to specify a list |
|
800 of variables that should be generalized before applying the resulting rule. |
|
801 \end{descr} |
|
802 |
|
803 |
|
804 \subsection{Executable code} |
|
805 |
|
806 Isabelle/Pure provides two generic frameworks to support code |
|
807 generation from executable specifications. Isabelle/HOL |
|
808 instantiates these mechanisms in a |
|
809 way that is amenable to end-user applications. |
|
810 |
|
811 One framework generates code from both functional and |
|
812 relational programs to SML. See |
|
813 \cite{isabelle-HOL} for further information (this actually covers the |
|
814 new-style theory format as well). |
|
815 |
|
816 \indexisarcmd{value}\indexisarcmd{code-module}\indexisarcmd{code-library} |
|
817 \indexisarcmd{consts-code}\indexisarcmd{types-code} |
|
818 \indexisaratt{code} |
|
819 |
|
820 \begin{matharray}{rcl} |
|
821 \isarcmd{value}^* & : & \isarkeep{theory~|~proof} \\ |
|
822 \isarcmd{code_module} & : & \isartrans{theory}{theory} \\ |
|
823 \isarcmd{code_library} & : & \isartrans{theory}{theory} \\ |
|
824 \isarcmd{consts_code} & : & \isartrans{theory}{theory} \\ |
|
825 \isarcmd{types_code} & : & \isartrans{theory}{theory} \\ |
|
826 code & : & \isaratt \\ |
|
827 \end{matharray} |
|
828 |
|
829 \railalias{verblbrace}{\texttt{\ttlbrace*}} |
|
830 \railalias{verbrbrace}{\texttt{*\ttrbrace}} |
|
831 \railterm{verblbrace} |
|
832 \railterm{verbrbrace} |
|
833 |
|
834 \begin{rail} |
|
835 'value' term; |
|
836 |
|
837 ( 'code\_module' | 'code\_library' ) modespec ? name ? \\ |
|
838 ( 'file' name ) ? ( 'imports' ( name + ) ) ? \\ |
|
839 'contains' ( ( name '=' term ) + | term + ); |
|
840 |
|
841 modespec : '(' ( name * ) ')'; |
|
842 |
|
843 'consts\_code' (codespec +); |
|
844 |
|
845 codespec : const template attachment ?; |
|
846 |
|
847 'types\_code' (tycodespec +); |
|
848 |
|
849 tycodespec : name template attachment ?; |
|
850 |
|
851 const: term; |
|
852 |
|
853 template: '(' string ')'; |
|
854 |
|
855 attachment: 'attach' modespec ? verblbrace text verbrbrace; |
|
856 |
|
857 'code' (name)?; |
|
858 \end{rail} |
|
859 |
|
860 \begin{descr} |
|
861 \item [$\isarkeyword{value}~t$] reads, evaluates and prints a term |
|
862 using the code generator. |
|
863 \end{descr} |
|
864 |
|
865 The other framework generates code from functional programs |
|
866 (including overloading using type classes) to SML \cite{SML}, |
|
867 OCaml \cite{OCaml} and Haskell \cite{haskell-revised-report}. |
|
868 Conceptually, code generation is split up in three steps: \emph{selection} |
|
869 of code theorems, \emph{translation} into an abstract executable view |
|
870 and \emph{serialization} to a specific \emph{target language}. |
|
871 See \cite{isabelle-codegen} for an introduction on how to use it. |
|
872 |
|
873 \indexisarcmd{export-code} |
|
874 \indexisarcmd{code-thms} |
|
875 \indexisarcmd{code-deps} |
|
876 \indexisarcmd{code-datatype} |
|
877 \indexisarcmd{code-const} |
|
878 \indexisarcmd{code-type} |
|
879 \indexisarcmd{code-class} |
|
880 \indexisarcmd{code-instance} |
|
881 \indexisarcmd{code-monad} |
|
882 \indexisarcmd{code-reserved} |
|
883 \indexisarcmd{code-include} |
|
884 \indexisarcmd{code-modulename} |
|
885 \indexisarcmd{code-exception} |
|
886 \indexisarcmd{print-codesetup} |
|
887 \indexisaratt{code func} |
|
888 \indexisaratt{code inline} |
|
889 |
|
890 \begin{matharray}{rcl} |
|
891 \isarcmd{export_code}^* & : & \isarkeep{theory~|~proof} \\ |
|
892 \isarcmd{code_thms}^* & : & \isarkeep{theory~|~proof} \\ |
|
893 \isarcmd{code_deps}^* & : & \isarkeep{theory~|~proof} \\ |
|
894 \isarcmd{code_datatype} & : & \isartrans{theory}{theory} \\ |
|
895 \isarcmd{code_const} & : & \isartrans{theory}{theory} \\ |
|
896 \isarcmd{code_type} & : & \isartrans{theory}{theory} \\ |
|
897 \isarcmd{code_class} & : & \isartrans{theory}{theory} \\ |
|
898 \isarcmd{code_instance} & : & \isartrans{theory}{theory} \\ |
|
899 \isarcmd{code_monad} & : & \isartrans{theory}{theory} \\ |
|
900 \isarcmd{code_reserved} & : & \isartrans{theory}{theory} \\ |
|
901 \isarcmd{code_include} & : & \isartrans{theory}{theory} \\ |
|
902 \isarcmd{code_modulename} & : & \isartrans{theory}{theory} \\ |
|
903 \isarcmd{code_exception} & : & \isartrans{theory}{theory} \\ |
|
904 \isarcmd{print_codesetup}^* & : & \isarkeep{theory~|~proof} \\ |
|
905 code\ func & : & \isaratt \\ |
|
906 code\ inline & : & \isaratt \\ |
|
907 \end{matharray} |
|
908 |
|
909 \begin{rail} |
|
910 'export\_code' ( constexpr + ) ? \\ |
|
911 ( ( 'in' target ( 'module\_name' string ) ? \\ |
|
912 ( 'file' ( string | '-' ) ) ? ( '(' args ')' ) ?) + ) ?; |
|
913 |
|
914 'code\_thms' ( constexpr + ) ?; |
|
915 |
|
916 'code\_deps' ( constexpr + ) ?; |
|
917 |
|
918 const : term; |
|
919 |
|
920 constexpr : ( const | 'name.*' | '*' ); |
|
921 |
|
922 typeconstructor : nameref; |
|
923 |
|
924 class : nameref; |
|
925 |
|
926 target : 'OCaml' | 'SML' | 'Haskell'; |
|
927 |
|
928 'code\_datatype' const +; |
|
929 |
|
930 'code\_const' (const + 'and') \\ |
|
931 ( ( '(' target ( syntax ? + 'and' ) ')' ) + ); |
|
932 |
|
933 'code\_type' (typeconstructor + 'and') \\ |
|
934 ( ( '(' target ( syntax ? + 'and' ) ')' ) + ); |
|
935 |
|
936 'code\_class' (class + 'and') \\ |
|
937 ( ( '(' target \\ |
|
938 ( ( string ('where' \\ |
|
939 ( const ( '==' | equiv ) string ) + ) ? ) ? + 'and' ) ')' ) + ); |
|
940 |
|
941 'code\_instance' (( typeconstructor '::' class ) + 'and') \\ |
|
942 ( ( '(' target ( '-' ? + 'and' ) ')' ) + ); |
|
943 |
|
944 'code\_monad' const const target; |
|
945 |
|
946 'code\_reserved' target ( string + ); |
|
947 |
|
948 'code\_include' target ( string ( string | '-') ); |
|
949 |
|
950 'code\_modulename' target ( ( string string ) + ); |
|
951 |
|
952 'code\_exception' ( const + ); |
|
953 |
|
954 syntax : string | ( 'infix' | 'infixl' | 'infixr' ) nat string; |
|
955 |
|
956 'print\_codesetup'; |
|
957 |
|
958 'code\ func' ( 'del' ) ?; |
|
959 |
|
960 'code\ inline' ( 'del' ) ?; |
|
961 \end{rail} |
|
962 |
|
963 \begin{descr} |
|
964 |
|
965 \item [$\isarcmd{export_code}$] is the canonical interface for generating and |
|
966 serializing code: for a given list of constants, code is generated for the specified |
|
967 target language(s). Abstract code is cached incrementally. If no constant is given, |
|
968 the currently cached code is serialized. If no serialization instruction |
|
969 is given, only abstract code is cached. |
|
970 |
|
971 Constants may be specified by giving them literally, referring |
|
972 to all exeuctable contants within a certain theory named ``name'' |
|
973 by giving (``name.*''), or referring to \emph{all} executable |
|
974 constants currently available (``*''). |
|
975 |
|
976 By default, for each involved theory one corresponding name space module |
|
977 is generated. Alternativly, a module name may be specified after the |
|
978 (``module_name'') keyword; then \emph{all} code is placed in this module. |
|
979 |
|
980 For \emph{SML} and \emph{OCaml}, the file specification refers to |
|
981 a single file; for \emph{Haskell}, it refers to a whole directory, |
|
982 where code is generated in multiple files reflecting the module hierarchy. |
|
983 The file specification ``-'' denotes standard output. For \emph{SML}, |
|
984 omitting the file specification compiles code internally |
|
985 in the context of the current ML session. |
|
986 |
|
987 Serializers take an optional list of arguments in parentheses. |
|
988 For \emph{Haskell} a module name prefix may be given using the ``root:'' |
|
989 argument; ``string\_classes'' adds a ``deriving (Read, Show)'' clause |
|
990 to each appropriate datatype declaration. |
|
991 |
|
992 \item [$\isarcmd{code_thms}$] prints a list of theorems representing the |
|
993 corresponding program containing all given constants; if no constants are |
|
994 given, the currently cached code theorems are printed. |
|
995 |
|
996 \item [$\isarcmd{code_deps}$] visualizes dependencies of theorems representing the |
|
997 corresponding program containing all given constants; if no constants are |
|
998 given, the currently cached code theorems are visualized. |
|
999 |
|
1000 \item [$\isarcmd{code_datatype}$] specifies a constructor set for a logical type. |
|
1001 |
|
1002 \item [$\isarcmd{code_const}$] associates a list of constants |
|
1003 with target-specific serializations; omitting a serialization |
|
1004 deletes an existing serialization. |
|
1005 |
|
1006 \item [$\isarcmd{code_type}$] associates a list of type constructors |
|
1007 with target-specific serializations; omitting a serialization |
|
1008 deletes an existing serialization. |
|
1009 |
|
1010 \item [$\isarcmd{code_class}$] associates a list of classes |
|
1011 with target-specific class names; in addition, constants associated |
|
1012 with this class may be given target-specific names used for instance |
|
1013 declarations; omitting a serialization |
|
1014 deletes an existing serialization. Applies only to \emph{Haskell}. |
|
1015 |
|
1016 \item [$\isarcmd{code_instance}$] declares a list of type constructor / class |
|
1017 instance relations as ``already present'' for a given target. |
|
1018 Omitting a ``-'' deletes an existing ``already present'' declaration. |
|
1019 Applies only to \emph{Haskell}. |
|
1020 |
|
1021 \item [$\isarcmd{code_monad}$] provides an auxiliary mechanism |
|
1022 to generate monadic code. |
|
1023 |
|
1024 \item [$\isarcmd{code_reserved}$] declares a list of names |
|
1025 as reserved for a given target, preventing it to be shadowed |
|
1026 by any generated code. |
|
1027 |
|
1028 \item [$\isarcmd{code_include}$] adds arbitrary named content (''include``) |
|
1029 to generated code. A as last argument ``-'' will remove an already added ''include``. |
|
1030 |
|
1031 \item [$\isarcmd{code_modulename}$] declares aliasings from one module name |
|
1032 onto another. |
|
1033 |
|
1034 \item [$\isarcmd{code_exception}$] declares constants which are not required |
|
1035 to have a definition by a defining equations; these are mapped on exceptions |
|
1036 instead. |
|
1037 |
|
1038 \item [$code\ func$] selects (or with option ''del``, deselects) explicitly |
|
1039 a defining equation for code generation. Usually packages introducing |
|
1040 defining equations provide a resonable default setup for selection. |
|
1041 |
|
1042 \item [$code\ inline$] declares (or with option ''del``, removes) |
|
1043 inlining theorems which are applied as rewrite rules to any defining equation |
|
1044 during preprocessing. |
|
1045 |
|
1046 \item [$\isarcmd{print_codesetup}$] gives an overview on selected |
|
1047 defining equations, code generator datatypes and preprocessor setup. |
|
1048 |
|
1049 \end{descr} |
|
1050 |
|
1051 |
|
1052 %%% Local Variables: |
|
1053 %%% mode: latex |
|
1054 %%% TeX-master: "isar-ref" |
|
1055 %%% End: |
|