author | berghofe |
Thu, 30 Aug 2007 11:46:37 +0200 | |
changeset 24482 | 5edb9a54900f |
parent 24477 | f45e301b9e5c |
child 24524 | 6892fdc7e9f8 |
permissions | -rw-r--r-- |
12621 | 1 |
|
13048 | 2 |
\chapter{Object-logic specific elements}\label{ch:logics} |
12621 | 3 |
|
4 |
\section{General logic setup}\label{sec:object-logic} |
|
5 |
||
6 |
\indexisarcmd{judgment} |
|
7 |
\indexisarmeth{atomize}\indexisaratt{atomize} |
|
8 |
\indexisaratt{rule-format}\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 object-logic is a ``truth judgment'' |
|
19 |
that links object-level statements to the meta-logic (with its minimal |
|
20 |
language of $prop$ that covers universal quantification $\Forall$ and |
|
13041 | 21 |
implication $\Imp$). |
22 |
||
23 |
Common object-logics 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 meta-level 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 end-users, the rest is |
|
31 |
for those who need to setup their own object-logic. 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 object-logic |
|
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 object-logic. Its type $\sigma$ should |
54 |
specify a coercion of the category of object-level propositions to $prop$ of |
|
13041 | 55 |
the Pure meta-logic; 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 non-atomic premises of a |
61 |
sub-goal, using the meta-level 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 |
proof-by-assumption (cf.\ $assumption$). Giving the ``$(full)$'' option |
13041 | 65 |
here means to turn the whole subgoal into an object-statement (if possible), |
13014 | 66 |
including the outermost parameters and assumptions as well. |
67 |
||
12621 | 68 |
A typical collection of $atomize$ rules for a particular object-logic would |
69 |
provide an internalization for each of the connectives of $\Forall$, $\Imp$, |
|
70 |
and $\equiv$. Meta-level conjunction expressed in the manner of minimal |
|
71 |
higher-order 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 object-logic. 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 object-logics (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:hol-typedef} |
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:types-pure}), 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 |
non-emptiness of the set $A$. After finishing the proof, the theory will be |
|
13014 | 120 |
augmented by a Gordon/HOL-style 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, user-level theories usually refer |
|
146 |
to higher-level packages such as $\isarkeyword{record}$ (see |
|
147 |
\S\ref{sec:hol-record}) or $\isarkeyword{datatype}$ (see |
|
148 |
\S\ref{sec:hol-datatype}). |
|
12621 | 149 |
|
13014 | 150 |
|
151 |
\subsection{Adhoc tuples} |
|
12621 | 152 |
|
153 |
\indexisarattof{HOL}{split-format} |
|
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 low-level |
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:hol-record} |
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 ``object-oriented'' |
|
187 |
effects like (single) inheritance. See also \cite{NaraschewskiW-TPHOLs98} for |
|
188 |
more details on object-oriented 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}{l|l|l} |
|
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 first-class 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{isabelle-hol-book} 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 non-root 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:cases-induct}). 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:hol-datatype} |
|
394 |
||
395 |
\indexisarcmdof{HOL}{datatype}\indexisarcmdof{HOL}{rep-datatype} |
|
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:cases-induct}). |
|
427 |
||
13014 | 428 |
See \cite{isabelle-HOL} for more details on datatypes, but beware of the |
429 |
old-style theory syntax being used there! Apart from proper proof methods for |
|
430 |
case-analysis 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:hol-induct-tac}; 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 |
||
438 |
\indexisarcmdof{HOL}{primrec}\indexisarcmdof{HOL}{recdef}\indexisarcmdof{HOL}{recdef-tc} |
|
439 |
\begin{matharray}{rcl} |
|
440 |
\isarcmd{primrec} & : & \isartrans{theory}{theory} \\ |
|
441 |
\isarcmd{recdef} & : & \isartrans{theory}{theory} \\ |
|
442 |
\isarcmd{recdef_tc}^* & : & \isartrans{theory}{proof(prove)} \\ |
|
443 |
\end{matharray} |
|
444 |
||
445 |
\railalias{recdefsimp}{recdef\_simp} |
|
446 |
\railterm{recdefsimp} |
|
447 |
||
448 |
\railalias{recdefcong}{recdef\_cong} |
|
449 |
\railterm{recdefcong} |
|
450 |
||
451 |
\railalias{recdefwf}{recdef\_wf} |
|
452 |
\railterm{recdefwf} |
|
453 |
||
454 |
\railalias{recdeftc}{recdef\_tc} |
|
455 |
\railterm{recdeftc} |
|
456 |
||
457 |
\begin{rail} |
|
13024 | 458 |
'primrec' parname? (equation +) |
12621 | 459 |
; |
13024 | 460 |
'recdef' ('(' 'permissive' ')')? \\ name term (prop +) hints? |
12621 | 461 |
; |
12879 | 462 |
recdeftc thmdecl? tc |
12621 | 463 |
; |
464 |
||
12879 | 465 |
equation: thmdecl? prop |
12621 | 466 |
; |
13024 | 467 |
hints: '(' 'hints' (recdefmod *) ')' |
12621 | 468 |
; |
469 |
recdefmod: ((recdefsimp | recdefcong | recdefwf) (() | 'add' | 'del') ':' thmrefs) | clasimpmod |
|
470 |
; |
|
471 |
tc: nameref ('(' nat ')')? |
|
472 |
; |
|
473 |
\end{rail} |
|
474 |
||
475 |
\begin{descr} |
|
13024 | 476 |
|
12621 | 477 |
\item [$\isarkeyword{primrec}$] defines primitive recursive functions over |
13024 | 478 |
datatypes, see also \cite{isabelle-HOL}. |
479 |
||
12621 | 480 |
\item [$\isarkeyword{recdef}$] defines general well-founded recursive |
13024 | 481 |
functions (using the TFL package), see also \cite{isabelle-HOL}. The |
13041 | 482 |
``$(permissive)$'' option tells TFL to recover from failed proof attempts, |
12621 | 483 |
returning unfinished results. The $recdef_simp$, $recdef_cong$, and |
484 |
$recdef_wf$ hints refer to auxiliary rules to be used in the internal |
|
13024 | 485 |
automated proof process of TFL. Additional $clasimpmod$ declarations (cf.\ |
12621 | 486 |
\S\ref{sec:clasimp}) may be given to tune the context of the Simplifier |
13024 | 487 |
(cf.\ \S\ref{sec:simplifier}) and Classical reasoner (cf.\ |
12621 | 488 |
\S\ref{sec:classical}). |
13024 | 489 |
|
12621 | 490 |
\item [$\isarkeyword{recdef_tc}~c~(i)$] recommences the proof for leftover |
491 |
termination condition number $i$ (default $1$) as generated by a |
|
492 |
$\isarkeyword{recdef}$ definition of constant $c$. |
|
13024 | 493 |
|
12621 | 494 |
Note that in most cases, $\isarkeyword{recdef}$ is able to finish its |
495 |
internal proofs without manual intervention. |
|
13024 | 496 |
|
12621 | 497 |
\end{descr} |
498 |
||
13014 | 499 |
Both kinds of recursive definitions accommodate reasoning by induction (cf.\ |
12621 | 500 |
\S\ref{sec:cases-induct}): rule $c\mathord{.}induct$ (where $c$ is the name of |
501 |
the function definition) refers to a specific induction rule, with parameters |
|
502 |
named according to the user-specified equations. Case names of |
|
503 |
$\isarkeyword{primrec}$ are that of the datatypes involved, while those of |
|
504 |
$\isarkeyword{recdef}$ are numbered (starting from $1$). |
|
505 |
||
506 |
The equations provided by these packages may be referred later as theorem list |
|
13041 | 507 |
$f{\dtt}simps$, where $f$ is the (collective) name of the functions defined. |
508 |
Individual equations may be named explicitly as well; note that for |
|
12621 | 509 |
$\isarkeyword{recdef}$ each specification given by the user may result in |
510 |
several theorems. |
|
511 |
||
512 |
\medskip Hints for $\isarkeyword{recdef}$ may be also declared globally, using |
|
513 |
the following attributes. |
|
514 |
||
515 |
\indexisarattof{HOL}{recdef-simp}\indexisarattof{HOL}{recdef-cong}\indexisarattof{HOL}{recdef-wf} |
|
516 |
\begin{matharray}{rcl} |
|
517 |
recdef_simp & : & \isaratt \\ |
|
518 |
recdef_cong & : & \isaratt \\ |
|
519 |
recdef_wf & : & \isaratt \\ |
|
520 |
\end{matharray} |
|
521 |
||
522 |
\railalias{recdefsimp}{recdef\_simp} |
|
523 |
\railterm{recdefsimp} |
|
524 |
||
525 |
\railalias{recdefcong}{recdef\_cong} |
|
526 |
\railterm{recdefcong} |
|
527 |
||
528 |
\railalias{recdefwf}{recdef\_wf} |
|
529 |
\railterm{recdefwf} |
|
530 |
||
531 |
\begin{rail} |
|
532 |
(recdefsimp | recdefcong | recdefwf) (() | 'add' | 'del') |
|
533 |
; |
|
534 |
\end{rail} |
|
535 |
||
14119 | 536 |
\subsection{Definition by specification}\label{sec:hol-specification} |
537 |
||
538 |
\indexisarcmdof{HOL}{specification} |
|
539 |
\begin{matharray}{rcl} |
|
540 |
\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
|
541 |
\isarcmd{ax_specification} & : & \isartrans{theory}{proof(prove)} \\ |
14119 | 542 |
\end{matharray} |
543 |
||
544 |
\begin{rail} |
|
14619
8876ad83b1fb
Added documentation for ax_specification, as well as a small comparison of
skalberg
parents:
14165
diff
changeset
|
545 |
('specification' | 'ax\_specification') '(' (decl +) ')' \\ (thmdecl? prop +) |
14119 | 546 |
; |
14642 | 547 |
decl: ((name ':')? term '(' 'overloaded' ')'?) |
14119 | 548 |
\end{rail} |
549 |
||
550 |
\begin{descr} |
|
14165
67b4c4cdb270
New specification syntax added (the specification may be split over
skalberg
parents:
14119
diff
changeset
|
551 |
\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
|
552 |
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
|
553 |
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
|
554 |
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
|
555 |
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
|
556 |
\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
|
557 |
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
|
558 |
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
|
559 |
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
|
560 |
in the first place. |
14119 | 561 |
\item[$decl$] declares a constant to be defined by the specification |
562 |
given. The definition for the constant $c$ is bound to the name |
|
563 |
$c$\_def unless a theorem name is given in the declaration. |
|
564 |
Overloaded constants should be declared as such. |
|
565 |
\end{descr} |
|
12621 | 566 |
|
14619
8876ad83b1fb
Added documentation for ax_specification, as well as a small comparison of
skalberg
parents:
14165
diff
changeset
|
567 |
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
|
568 |
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
|
569 |
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
|
570 |
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
|
571 |
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
|
572 |
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
|
573 |
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
|
574 |
one should use $\isarkeyword{ax_specification}$. |
8876ad83b1fb
Added documentation for ax_specification, as well as a small comparison of
skalberg
parents:
14165
diff
changeset
|
575 |
|
24477 | 576 |
\subsection{Inductive and coinductive definitions}\label{sec:hol-inductive} |
577 |
||
578 |
An {\bf inductive definition} specifies the least predicate (or set) $R$ closed under given |
|
579 |
rules. (Applying a rule to elements of~$R$ yields a result within~$R$.) For |
|
580 |
example, a structural operational semantics is an inductive definition of an |
|
581 |
evaluation relation. Dually, a {\bf coinductive definition} specifies the |
|
582 |
greatest predicate (or set) $R$ consistent with given rules. (Every element of~$R$ can be |
|
583 |
seen as arising by applying a rule to elements of~$R$.) An important example |
|
584 |
is using bisimulation relations to formalise equivalence of processes and |
|
585 |
infinite data structures. |
|
12621 | 586 |
|
24477 | 587 |
This package is related to the ZF one, described in a separate |
588 |
paper,% |
|
589 |
\footnote{It appeared in CADE~\cite{paulson-CADE}; a longer version is |
|
590 |
distributed with Isabelle.} % |
|
591 |
which you should refer to in case of difficulties. The package is simpler |
|
592 |
than ZF's thanks to HOL's extra-logical automatic type-checking. The types of |
|
593 |
the (co)inductive predicates (or sets) determine the domain of the fixedpoint definition, and |
|
594 |
the package does not have to use inference rules for type-checking. |
|
595 |
||
596 |
\indexisarcmdof{HOL}{inductive}\indexisarcmdof{HOL}{inductive-set}\indexisarcmdof{HOL}{coinductive}\indexisarcmdof{HOL}{coinductive-set}\indexisarattof{HOL}{mono} |
|
12621 | 597 |
\begin{matharray}{rcl} |
598 |
\isarcmd{inductive} & : & \isartrans{theory}{theory} \\ |
|
24477 | 599 |
\isarcmd{inductive_set} & : & \isartrans{theory}{theory} \\ |
12621 | 600 |
\isarcmd{coinductive} & : & \isartrans{theory}{theory} \\ |
24477 | 601 |
\isarcmd{coinductive_set} & : & \isartrans{theory}{theory} \\ |
12621 | 602 |
mono & : & \isaratt \\ |
603 |
\end{matharray} |
|
604 |
||
605 |
\begin{rail} |
|
24482 | 606 |
('inductive' | 'inductive\_set' | 'coinductive' | 'coinductive\_set') target? fixes ('for' fixes)? \\ |
607 |
('where' clauses)? ('monos' thmrefs)? |
|
24477 | 608 |
; |
609 |
clauses: (thmdecl? prop + '|') |
|
12621 | 610 |
; |
611 |
'mono' (() | 'add' | 'del') |
|
612 |
; |
|
613 |
\end{rail} |
|
614 |
||
615 |
\begin{descr} |
|
616 |
\item [$\isarkeyword{inductive}$ and $\isarkeyword{coinductive}$] define |
|
24477 | 617 |
(co)inductive predicates from the introduction rules given in the \texttt{where} section. |
24482 | 618 |
The optional \texttt{for} section contains a list of parameters of the (co)inductive |
619 |
predicates that remain fixed throughout the definition. |
|
24477 | 620 |
The optional \texttt{monos} section contains \textit{monotonicity theorems}, |
621 |
which are required for each operator applied to a recursive set in the introduction rules. |
|
622 |
There {\bf must} be a theorem of the form $A \leq B \Imp M~A \leq M~B$, for each |
|
623 |
premise $M~R@i~t$ in an introduction rule! |
|
624 |
\item [$\isarkeyword{inductive_set}$ and $\isarkeyword{coinductive_set}$] are wrappers |
|
625 |
for to the previous commands, allowing the definition of (co)inductive sets. |
|
12621 | 626 |
\item [$mono$] declares monotonicity rules. These rule are involved in the |
627 |
automated monotonicity proof of $\isarkeyword{inductive}$. |
|
628 |
\end{descr} |
|
629 |
||
24477 | 630 |
\subsubsection{Derived rules} |
631 |
||
632 |
Each (co)inductive definition $R$ adds definitions to the theory and also |
|
633 |
proves some theorems: |
|
634 |
\begin{description} |
|
635 |
\item[$R{\dtt}intros$] is the list of introduction rules, now proved as theorems, for |
|
636 |
the recursive predicates (or sets). The rules are also available individually, |
|
637 |
using the names given them in the theory file. |
|
638 |
\item[$R{\dtt}cases$] is the case analysis (or elimination) rule. |
|
639 |
\item[$R{\dtt}(co)induct$] is the (co)induction rule. |
|
640 |
\end{description} |
|
641 |
When several predicates $R@1$, $\ldots$, $R@n$ are defined simultaneously, |
|
642 |
the list of introduction rules is called $R@1_\ldots_R@n{\dtt}intros$, the |
|
643 |
case analysis rules are called $R@1{\dtt}cases$, $\ldots$, $R@n{\dtt}cases$, and |
|
644 |
the list of mutual induction rules is called $R@1_\ldots_R@n{\dtt}inducts$. |
|
645 |
||
646 |
\subsubsection{Monotonicity theorems} |
|
647 |
||
648 |
Each theory contains a default set of theorems that are used in monotonicity |
|
649 |
proofs. New rules can be added to this set via the $mono$ attribute. |
|
650 |
Theory \texttt{Inductive} shows how this is done. In general, the following |
|
651 |
monotonicity theorems may be added: |
|
652 |
\begin{itemize} |
|
653 |
\item Theorems of the form $A \leq B \Imp M~A \leq M~B$, for proving |
|
654 |
monotonicity of inductive definitions whose introduction rules have premises |
|
655 |
involving terms such as $M~R@i~t$. |
|
656 |
\item Monotonicity theorems for logical operators, which are of the general form |
|
657 |
$\List{\cdots \to \cdots;~\ldots;~\cdots \to \cdots} \Imp |
|
658 |
\cdots \to \cdots$. |
|
659 |
For example, in the case of the operator $\lor$, the corresponding theorem is |
|
660 |
\[ |
|
661 |
\infer{P@1 \lor P@2 \to Q@1 \lor Q@2} |
|
662 |
{P@1 \to Q@1 & P@2 \to Q@2} |
|
663 |
\] |
|
664 |
\item De Morgan style equations for reasoning about the ``polarity'' of expressions, e.g. |
|
665 |
\[ |
|
666 |
(\lnot \lnot P) ~=~ P \qquad\qquad |
|
667 |
(\lnot (P \land Q)) ~=~ (\lnot P \lor \lnot Q) |
|
668 |
\] |
|
669 |
\item Equations for reducing complex operators to more primitive ones whose |
|
670 |
monotonicity can easily be proved, e.g. |
|
671 |
\[ |
|
672 |
(P \to Q) ~=~ (\lnot P \lor Q) \qquad\qquad |
|
673 |
\mathtt{Ball}~A~P ~\equiv~ \forall x.~x \in A \to P~x |
|
674 |
\] |
|
675 |
\end{itemize} |
|
676 |
||
677 |
%FIXME: Example of an inductive definition |
|
12621 | 678 |
|
679 |
||
680 |
\subsection{Arithmetic proof support} |
|
681 |
||
682 |
\indexisarmethof{HOL}{arith}\indexisarattof{HOL}{arith-split} |
|
683 |
\begin{matharray}{rcl} |
|
684 |
arith & : & \isarmeth \\ |
|
685 |
arith_split & : & \isaratt \\ |
|
686 |
\end{matharray} |
|
687 |
||
688 |
\begin{rail} |
|
689 |
'arith' '!'? |
|
690 |
; |
|
691 |
\end{rail} |
|
692 |
||
693 |
The $arith$ method decides linear arithmetic problems (on types $nat$, $int$, |
|
694 |
$real$). Any current facts are inserted into the goal before running the |
|
695 |
procedure. The ``!''~argument causes the full context of assumptions to be |
|
696 |
included. The $arith_split$ attribute declares case split rules to be |
|
697 |
expanded before the arithmetic procedure is invoked. |
|
698 |
||
699 |
Note that a simpler (but faster) version of arithmetic reasoning is already |
|
700 |
performed by the Simplifier. |
|
701 |
||
702 |
||
13024 | 703 |
\subsection{Cases and induction: emulating tactic scripts}\label{sec:hol-induct-tac} |
12621 | 704 |
|
705 |
The following important tactical tools of Isabelle/HOL have been ported to |
|
706 |
Isar. These should be never used in proper proof texts! |
|
707 |
||
708 |
\indexisarmethof{HOL}{case-tac}\indexisarmethof{HOL}{induct-tac} |
|
709 |
\indexisarmethof{HOL}{ind-cases}\indexisarcmdof{HOL}{inductive-cases} |
|
710 |
\begin{matharray}{rcl} |
|
711 |
case_tac^* & : & \isarmeth \\ |
|
712 |
induct_tac^* & : & \isarmeth \\ |
|
713 |
ind_cases^* & : & \isarmeth \\ |
|
714 |
\isarcmd{inductive_cases} & : & \isartrans{theory}{theory} \\ |
|
715 |
\end{matharray} |
|
716 |
||
717 |
\railalias{casetac}{case\_tac} |
|
718 |
\railterm{casetac} |
|
719 |
||
720 |
\railalias{inducttac}{induct\_tac} |
|
721 |
\railterm{inducttac} |
|
722 |
||
723 |
\railalias{indcases}{ind\_cases} |
|
724 |
\railterm{indcases} |
|
725 |
||
726 |
\railalias{inductivecases}{inductive\_cases} |
|
727 |
\railterm{inductivecases} |
|
728 |
||
729 |
\begin{rail} |
|
730 |
casetac goalspec? term rule? |
|
731 |
; |
|
732 |
inducttac goalspec? (insts * 'and') rule? |
|
733 |
; |
|
24482 | 734 |
indcases (prop +) ('for' (name +)) ? |
12621 | 735 |
; |
13014 | 736 |
inductivecases (thmdecl? (prop +) + 'and') |
12621 | 737 |
; |
738 |
||
739 |
rule: ('rule' ':' thmref) |
|
740 |
; |
|
741 |
\end{rail} |
|
742 |
||
743 |
\begin{descr} |
|
744 |
\item [$case_tac$ and $induct_tac$] admit to reason about inductive datatypes |
|
745 |
only (unless an alternative rule is given explicitly). Furthermore, |
|
746 |
$case_tac$ does a classical case split on booleans; $induct_tac$ allows only |
|
747 |
variables to be given as instantiation. These tactic emulations feature |
|
748 |
both goal addressing and dynamic instantiation. Note that named rule cases |
|
749 |
are \emph{not} provided as would be by the proper $induct$ and $cases$ proof |
|
750 |
methods (see \S\ref{sec:cases-induct}). |
|
13041 | 751 |
|
12621 | 752 |
\item [$ind_cases$ and $\isarkeyword{inductive_cases}$] provide an interface |
13041 | 753 |
to the internal \texttt{mk_cases} operation. Rules are simplified in an |
754 |
unrestricted forward manner. |
|
13014 | 755 |
|
12621 | 756 |
While $ind_cases$ is a proof method to apply the result immediately as |
757 |
elimination rules, $\isarkeyword{inductive_cases}$ provides case split |
|
24482 | 758 |
theorems at the theory level for later use. |
759 |
The \texttt{for} option of the $ind_cases$ method allows to specify a list |
|
760 |
of variables that should be generalized before applying the resulting rule. |
|
12621 | 761 |
\end{descr} |
762 |
||
763 |
||
13039 | 764 |
\subsection{Executable code} |
13027 | 765 |
|
20587 | 766 |
Isabelle/Pure provides two generic frameworks to support code |
767 |
generation from executable specifications. Isabelle/HOL |
|
768 |
instantiates these mechanisms in a |
|
769 |
way that is amenable to end-user applications |
|
770 |
||
771 |
One framework generates code from both functional and |
|
772 |
relational programs to SML. See |
|
19988 | 773 |
\cite{isabelle-HOL} for further information (this actually covers the |
774 |
new-style theory format as well). |
|
13027 | 775 |
|
19988 | 776 |
\indexisarcmd{value}\indexisarcmd{code-module}\indexisarcmd{code-library} |
777 |
\indexisarcmd{consts-code}\indexisarcmd{types-code} |
|
13027 | 778 |
\indexisaratt{code} |
779 |
||
780 |
\begin{matharray}{rcl} |
|
19988 | 781 |
\isarcmd{value}^* & : & \isarkeep{theory~|~proof} \\ |
17659 | 782 |
\isarcmd{code_module} & : & \isartrans{theory}{theory} \\ |
783 |
\isarcmd{code_library} & : & \isartrans{theory}{theory} \\ |
|
13027 | 784 |
\isarcmd{consts_code} & : & \isartrans{theory}{theory} \\ |
785 |
\isarcmd{types_code} & : & \isartrans{theory}{theory} \\ |
|
786 |
code & : & \isaratt \\ |
|
787 |
\end{matharray} |
|
788 |
||
17659 | 789 |
\railalias{verblbrace}{\texttt{\ttlbrace*}} |
790 |
\railalias{verbrbrace}{\texttt{*\ttrbrace}} |
|
791 |
\railterm{verblbrace} |
|
792 |
\railterm{verbrbrace} |
|
793 |
||
19988 | 794 |
\begin{rail} |
795 |
'value' term; |
|
13027 | 796 |
|
19988 | 797 |
( 'code\_module' | 'code\_library' ) modespec ? name ? \\ |
17659 | 798 |
( 'file' name ) ? ( 'imports' ( name + ) ) ? \\ |
799 |
'contains' ( ( name '=' term ) + | term + ); |
|
800 |
||
801 |
modespec : '(' ( name * ) ')'; |
|
802 |
||
19988 | 803 |
'consts\_code' (codespec +); |
17659 | 804 |
|
22921
475ff421a6a3
consts in consts_code Isar commands are now referred to by usual term syntax
haftmann
parents:
22845
diff
changeset
|
805 |
codespec : const template attachment ?; |
13027 | 806 |
|
19988 | 807 |
'types\_code' (tycodespec +); |
17659 | 808 |
|
809 |
tycodespec : name template attachment ?; |
|
810 |
||
22921
475ff421a6a3
consts in consts_code Isar commands are now referred to by usual term syntax
haftmann
parents:
22845
diff
changeset
|
811 |
const: term; |
475ff421a6a3
consts in consts_code Isar commands are now referred to by usual term syntax
haftmann
parents:
22845
diff
changeset
|
812 |
|
17659 | 813 |
template: '(' string ')'; |
814 |
||
815 |
attachment: 'attach' modespec ? verblbrace text verbrbrace; |
|
816 |
||
817 |
'code' (name)?; |
|
13027 | 818 |
\end{rail} |
819 |
||
19988 | 820 |
\begin{descr} |
821 |
\item [$\isarkeyword{value}~t$] reads, evaluates and prints a term |
|
822 |
using the code generator. |
|
823 |
\end{descr} |
|
824 |
||
20587 | 825 |
The other framework generates code from functional programs |
22291 | 826 |
(including overloading using type classes) to SML \cite{SML}, |
827 |
OCaml \cite{OCaml} and Haskell \cite{haskell-revised-report}. |
|
20587 | 828 |
Conceptually, code generation is split up in three steps: \emph{selection} |
22752 | 829 |
of code theorems, \emph{translation} into an abstract executable view |
20587 | 830 |
and \emph{serialization} to a specific \emph{target language}. |
21077 | 831 |
See \cite{isabelle-codegen} for an introduction on how to use it. |
20587 | 832 |
|
833 |
\indexisarcmd{code-gen} |
|
22752 | 834 |
\indexisarcmd{code-thms} |
835 |
\indexisarcmd{code-deps} |
|
836 |
\indexisarcmd{code-datatype} |
|
21077 | 837 |
\indexisarcmd{code-const} |
838 |
\indexisarcmd{code-type} |
|
839 |
\indexisarcmd{code-class} |
|
840 |
\indexisarcmd{code-instance} |
|
22291 | 841 |
\indexisarcmd{code-monad} |
21077 | 842 |
\indexisarcmd{code-reserved} |
843 |
\indexisarcmd{code-modulename} |
|
844 |
\indexisarcmd{code-moduleprolog} |
|
845 |
\indexisarcmd{code-abstype} |
|
22291 | 846 |
\indexisarcmd{print-codesetup} |
20587 | 847 |
\indexisaratt{code func} |
848 |
\indexisaratt{code inline} |
|
849 |
||
850 |
\begin{matharray}{rcl} |
|
24348 | 851 |
\isarcmd{export_code}^* & : & \isarkeep{theory~|~proof} \\ |
22752 | 852 |
\isarcmd{code_thms}^* & : & \isarkeep{theory~|~proof} \\ |
853 |
\isarcmd{code_deps}^* & : & \isarkeep{theory~|~proof} \\ |
|
854 |
\isarcmd{code_datatype} & : & \isartrans{theory}{theory} \\ |
|
20587 | 855 |
\isarcmd{code_const} & : & \isartrans{theory}{theory} \\ |
856 |
\isarcmd{code_type} & : & \isartrans{theory}{theory} \\ |
|
857 |
\isarcmd{code_class} & : & \isartrans{theory}{theory} \\ |
|
858 |
\isarcmd{code_instance} & : & \isartrans{theory}{theory} \\ |
|
22291 | 859 |
\isarcmd{code_monad} & : & \isartrans{theory}{theory} \\ |
21077 | 860 |
\isarcmd{code_reserved} & : & \isartrans{theory}{theory} \\ |
861 |
\isarcmd{code_modulename} & : & \isartrans{theory}{theory} \\ |
|
862 |
\isarcmd{code_moduleprolog} & : & \isartrans{theory}{theory} \\ |
|
863 |
\isarcmd{code_abstype} & : & \isartrans{theory}{theory} \\ |
|
22291 | 864 |
\isarcmd{print_codesetup}^* & : & \isarkeep{theory~|~proof} \\ |
20587 | 865 |
code\ func & : & \isaratt \\ |
866 |
code\ inline & : & \isaratt \\ |
|
867 |
\end{matharray} |
|
868 |
||
869 |
\begin{rail} |
|
24348 | 870 |
'export\_code' ( constexpr + ) ? \\ |
24482 | 871 |
( ( 'in' target ( 'module\_name' string ) ? \\ |
872 |
( 'file' ( string | '-' ) ) ? ( '(' args ')' ) ?) + ) ?; |
|
22752 | 873 |
|
874 |
'code\_thms' ( constexpr + ) ?; |
|
875 |
||
876 |
'code\_deps' ( constexpr + ) ?; |
|
20587 | 877 |
|
878 |
const : term; |
|
879 |
||
22752 | 880 |
constexpr : ( const | 'name.*' | '*' ); |
881 |
||
20587 | 882 |
typeconstructor : nameref; |
883 |
||
884 |
class : nameref; |
|
885 |
||
22291 | 886 |
target : 'OCaml' | 'SML' | 'Haskell'; |
20587 | 887 |
|
22752 | 888 |
'code\_datatype' const +; |
889 |
||
20587 | 890 |
'code\_const' (const + 'and') \\ |
22845 | 891 |
( ( '(' target ( syntax ? + 'and' ) ')' ) + ); |
20587 | 892 |
|
893 |
'code\_type' (typeconstructor + 'and') \\ |
|
22845 | 894 |
( ( '(' target ( syntax ? + 'and' ) ')' ) + ); |
20587 | 895 |
|
896 |
'code\_class' (class + 'and') \\ |
|
897 |
( ( '(' target \\ |
|
22845 | 898 |
( ( string ('where' \\ |
899 |
( const ( '==' | equiv ) string ) + ) ? ) ? + 'and' ) ')' ) + ); |
|
20587 | 900 |
|
901 |
'code\_instance' (( typeconstructor '::' class ) + 'and') \\ |
|
22845 | 902 |
( ( '(' target ( '-' ? + 'and' ) ')' ) + ); |
20587 | 903 |
|
22291 | 904 |
'code\_monad' term term term; |
905 |
||
21077 | 906 |
'code\_reserved' target ( string + ); |
907 |
||
908 |
'code\_modulename' target ( ( string string ) + ); |
|
909 |
||
910 |
'code\_moduleprolog' target ( ( string ( string | '-') ) + ); |
|
911 |
||
912 |
'code\_abstype' typ typ 'where' ( const ( '==' | equiv ) const + ); |
|
913 |
||
22291 | 914 |
syntax : string | ( 'infix' | 'infixl' | 'infixr' ) nat string; |
20587 | 915 |
|
22291 | 916 |
'print\_codesetup'; |
20587 | 917 |
|
22845 | 918 |
'code\ func' ( 'del' ) ?; |
919 |
||
920 |
'code\ inline' ( 'del' ) ?; |
|
20587 | 921 |
\end{rail} |
922 |
||
923 |
\begin{descr} |
|
924 |
||
24348 | 925 |
\item [$\isarcmd{export_code}$] is the canonical interface for generating and |
20587 | 926 |
serializing code: for a given list of constants, code is generated for the specified |
927 |
target language(s). Abstract code is cached incrementally. If no constant is given, |
|
22845 | 928 |
the currently cached code is serialized. If no serialization instruction |
20587 | 929 |
is given, only abstract code is cached. |
930 |
||
22291 | 931 |
Constants may be specified by giving them literally, referring |
932 |
to all exeuctable contants within a certain theory named ``name'' |
|
22752 | 933 |
by giving (``name.*''), or referring to \emph{all} executable |
22291 | 934 |
constants currently available (``*''). |
935 |
||
23807 | 936 |
By default, for each involved theory one corresponding name space module |
24248 | 937 |
is generated. Alternativly, a module name may be specified after the |
938 |
(``module_name'') keyword; then \emph{all} code is placed in this module. |
|
23807 | 939 |
|
22845 | 940 |
For \emph{SML} and \emph{OCaml}, the file specification refers to |
941 |
a single file; for \emph{Haskell}, it refers to a whole directory, |
|
942 |
where code is generated in multiple files reflecting the module hierarchy. |
|
943 |
The file specification ``-'' denotes standard output. For \emph{SML}, |
|
944 |
omitting the file specification compiles code internally |
|
945 |
in the context of the current ML session. |
|
22291 | 946 |
|
22845 | 947 |
Serializers take an optional list of arguments in parentheses. |
948 |
For \emph{Haskell} a module name prefix may be given using the ``root:'' |
|
949 |
argument; ``string\_classes'' adds a ``deriving (Read, Show)'' clause |
|
21090 | 950 |
to each appropriate datatype declaration. |
20587 | 951 |
|
22752 | 952 |
\item [$\isarcmd{code_thms}$] prints a list of theorems representing the |
953 |
corresponding program containing all given constants; if no constants are |
|
24248 | 954 |
given, the currently cached code theorems are printed. |
22752 | 955 |
|
956 |
\item [$\isarcmd{code_deps}$] visualizes dependencies of theorems representing the |
|
957 |
corresponding program containing all given constants; if no constants are |
|
22845 | 958 |
given, the currently cached code theorems are visualized. |
22752 | 959 |
|
960 |
\item [$\isarcmd{code_datatype}$] specifies a constructor set for a logical type. |
|
961 |
||
20587 | 962 |
\item [$\isarcmd{code_const}$] associates a list of constants |
22845 | 963 |
with target-specific serializations; omitting a serialization |
964 |
deletes an existing serialization. |
|
20587 | 965 |
|
966 |
\item [$\isarcmd{code_type}$] associates a list of type constructors |
|
22845 | 967 |
with target-specific serializations; omitting a serialization |
968 |
deletes an existing serialization. |
|
20587 | 969 |
|
970 |
\item [$\isarcmd{code_class}$] associates a list of classes |
|
971 |
with target-specific class names; in addition, constants associated |
|
972 |
with this class may be given target-specific names used for instance |
|
22845 | 973 |
declarations; omitting a serialization |
974 |
deletes an existing serialization. Applies only to \emph{Haskell}. |
|
20587 | 975 |
|
976 |
\item [$\isarcmd{code_instance}$] declares a list of type constructor / class |
|
977 |
instance relations as ``already present'' for a given target. |
|
22845 | 978 |
Omitting a ``-'' deletes an existing ``already present'' declaration. |
20587 | 979 |
Applies only to \emph{Haskell}. |
980 |
||
22291 | 981 |
\item [$\isarcmd{code_monad}$] provides an auxiliary mechanism |
982 |
to generate monad code in \emph{Haskell}. |
|
983 |
||
21077 | 984 |
\item [$\isarcmd{code_reserved}$] declares a list of names |
985 |
as reserved for a given target, preventing it to be shadowed |
|
986 |
by any generated code. |
|
987 |
||
22752 | 988 |
\item [$\isarcmd{code_modulename}$] declares aliasings from one module name |
989 |
onto another. |
|
21077 | 990 |
|
24248 | 991 |
\item [$\isarcmd{code_moduleprolog}$] adds an arbitrary content (''prolog``) |
22752 | 992 |
to a specified module. A ``-'' will remove an already given prolog. |
21077 | 993 |
|
994 |
\item [$\isarcmd{code_abstype}$] offers an interface for implementing |
|
995 |
an abstract type plus operations by executable counterparts. |
|
996 |
||
22845 | 997 |
\item [$code\ func$] selects (or with option ''del``, deselects) explicitly |
22291 | 998 |
a defining equation for code generation. Usually packages introducing |
999 |
defining equations provide a resonable default setup for selection. |
|
20587 | 1000 |
|
22845 | 1001 |
\item [$code\ inline$] declares (or with option ''del``, removes) |
1002 |
inlining theorems which are applied as rewrite rules to any defining equation |
|
1003 |
during preprocessing. |
|
20587 | 1004 |
|
22291 | 1005 |
\item [$\isarcmd{print_codesetup}$] gives an overview on selected |
22845 | 1006 |
defining equations, code generator datatypes and preprocessor setup. |
20587 | 1007 |
|
1008 |
\end{descr} |
|
13027 | 1009 |
|
12621 | 1010 |
\section{HOLCF} |
1011 |
||
1012 |
\subsection{Mixfix syntax for continuous operations} |
|
1013 |
||
14682
a5072752114c
HOLCF: discontinued special version of 'constdefs';
wenzelm
parents:
14642
diff
changeset
|
1014 |
\indexisarcmdof{HOLCF}{consts} |
12621 | 1015 |
|
1016 |
\begin{matharray}{rcl} |
|
1017 |
\isarcmd{consts} & : & \isartrans{theory}{theory} \\ |
|
1018 |
\end{matharray} |
|
1019 |
||
14165
67b4c4cdb270
New specification syntax added (the specification may be split over
skalberg
parents:
14119
diff
changeset
|
1020 |
HOLCF provides a separate type for continuous functions $\alpha \to |
12621 | 1021 |
\beta$, with an explicit application operator $f \cdot x$. Isabelle mixfix |
1022 |
syntax normally refers directly to the pure meta-level function type $\alpha |
|
1023 |
\To \beta$, with application $f\,x$. |
|
1024 |
||
14682
a5072752114c
HOLCF: discontinued special version of 'constdefs';
wenzelm
parents:
14642
diff
changeset
|
1025 |
The HOLCF variant of $\CONSTS$ modifies that of Pure Isabelle (cf.\ |
a5072752114c
HOLCF: discontinued special version of 'constdefs';
wenzelm
parents:
14642
diff
changeset
|
1026 |
\S\ref{sec:consts}) such that declarations involving continuous function types |
a5072752114c
HOLCF: discontinued special version of 'constdefs';
wenzelm
parents:
14642
diff
changeset
|
1027 |
are treated specifically. Any given syntax template is transformed |
a5072752114c
HOLCF: discontinued special version of 'constdefs';
wenzelm
parents:
14642
diff
changeset
|
1028 |
internally, generating translation rules for the abstract and concrete |
a5072752114c
HOLCF: discontinued special version of 'constdefs';
wenzelm
parents:
14642
diff
changeset
|
1029 |
representation of continuous application. Note that mixing of HOLCF and Pure |
14642 | 1030 |
application is \emph{not} supported! |
12621 | 1031 |
|
1032 |
\subsection{Recursive domains} |
|
1033 |
||
1034 |
\indexisarcmdof{HOLCF}{domain} |
|
1035 |
\begin{matharray}{rcl} |
|
1036 |
\isarcmd{domain} & : & \isartrans{theory}{theory} \\ |
|
1037 |
\end{matharray} |
|
1038 |
||
1039 |
\begin{rail} |
|
1040 |
'domain' parname? (dmspec + 'and') |
|
1041 |
; |
|
1042 |
||
1043 |
dmspec: typespec '=' (cons + '|') |
|
1044 |
; |
|
13024 | 1045 |
cons: name (type *) mixfix? |
12621 | 1046 |
; |
1047 |
dtrules: 'distinct' thmrefs 'inject' thmrefs 'induction' thmrefs |
|
1048 |
\end{rail} |
|
1049 |
||
13041 | 1050 |
Recursive domains in HOLCF are analogous to datatypes in classical HOL (cf.\ |
1051 |
\S\ref{sec:hol-datatype}). Mutual recursion is supported, but no nesting nor |
|
12621 | 1052 |
arbitrary branching. Domain constructors may be strict (default) or lazy, the |
13041 | 1053 |
latter admits to introduce infinitary objects in the typical LCF manner (e.g.\ |
13014 | 1054 |
lazy lists). See also \cite{MuellerNvOS99} for a general discussion of HOLCF |
1055 |
domains. |
|
12621 | 1056 |
|
1057 |
||
1058 |
\section{ZF} |
|
1059 |
||
1060 |
\subsection{Type checking} |
|
1061 |
||
13024 | 1062 |
The ZF logic is essentially untyped, so the concept of ``type checking'' is |
1063 |
performed as logical reasoning about set-membership statements. A special |
|
1064 |
method assists users in this task; a version of this is already declared as a |
|
13041 | 1065 |
``solver'' in the standard Simplifier setup. |
13024 | 1066 |
|
1067 |
\indexisarcmd{print-tcset}\indexisaratt{typecheck}\indexisaratt{TC} |
|
1068 |
||
1069 |
\begin{matharray}{rcl} |
|
1070 |
\isarcmd{print_tcset}^* & : & \isarkeep{theory~|~proof} \\ |
|
1071 |
typecheck & : & \isarmeth \\ |
|
1072 |
TC & : & \isaratt \\ |
|
1073 |
\end{matharray} |
|
1074 |
||
1075 |
\begin{rail} |
|
1076 |
'TC' (() | 'add' | 'del') |
|
1077 |
; |
|
1078 |
\end{rail} |
|
1079 |
||
1080 |
\begin{descr} |
|
1081 |
||
1082 |
\item [$\isarcmd{print_tcset}$] prints the collection of typechecking rules of |
|
1083 |
the current context. |
|
1084 |
||
1085 |
Note that the component built into the Simplifier only knows about those |
|
1086 |
rules being declared globally in the theory! |
|
1087 |
||
1088 |
\item [$typecheck$] attempts to solve any pending type-checking problems in |
|
1089 |
subgoals. |
|
1090 |
||
1091 |
\item [$TC$] adds or deletes type-checking rules from the context. |
|
1092 |
||
1093 |
\end{descr} |
|
1094 |
||
1095 |
||
1096 |
\subsection{(Co)Inductive sets and datatypes} |
|
1097 |
||
1098 |
\subsubsection{Set definitions} |
|
1099 |
||
1100 |
In ZF everything is a set. The generic inductive package also provides a |
|
1101 |
specific view for ``datatype'' specifications. Coinductive definitions are |
|
13041 | 1102 |
available in both cases, too. |
13024 | 1103 |
|
1104 |
\indexisarcmdof{ZF}{inductive}\indexisarcmdof{ZF}{coinductive} |
|
1105 |
\indexisarcmdof{ZF}{datatype}\indexisarcmdof{ZF}{codatatype} |
|
1106 |
\begin{matharray}{rcl} |
|
1107 |
\isarcmd{inductive} & : & \isartrans{theory}{theory} \\ |
|
1108 |
\isarcmd{coinductive} & : & \isartrans{theory}{theory} \\ |
|
1109 |
\isarcmd{datatype} & : & \isartrans{theory}{theory} \\ |
|
1110 |
\isarcmd{codatatype} & : & \isartrans{theory}{theory} \\ |
|
1111 |
\end{matharray} |
|
1112 |
||
1113 |
\railalias{CONDEFS}{con\_defs} |
|
1114 |
\railterm{CONDEFS} |
|
1115 |
||
1116 |
\railalias{TYPEINTROS}{type\_intros} |
|
1117 |
\railterm{TYPEINTROS} |
|
1118 |
||
1119 |
\railalias{TYPEELIMS}{type\_elims} |
|
1120 |
\railterm{TYPEELIMS} |
|
1121 |
||
1122 |
\begin{rail} |
|
1123 |
('inductive' | 'coinductive') domains intros hints |
|
1124 |
; |
|
12621 | 1125 |
|
13024 | 1126 |
domains: 'domains' (term + '+') ('<=' | subseteq) term |
1127 |
; |
|
1128 |
intros: 'intros' (thmdecl? prop +) |
|
1129 |
; |
|
1130 |
hints: monos? condefs? typeintros? typeelims? |
|
1131 |
; |
|
1132 |
monos: ('monos' thmrefs)? |
|
1133 |
; |
|
1134 |
condefs: (CONDEFS thmrefs)? |
|
1135 |
; |
|
1136 |
typeintros: (TYPEINTROS thmrefs)? |
|
1137 |
; |
|
1138 |
typeelims: (TYPEELIMS thmrefs)? |
|
1139 |
; |
|
1140 |
\end{rail} |
|
1141 |
||
1142 |
In the following diagram $monos$, $typeintros$, and $typeelims$ are the same |
|
1143 |
as above. |
|
1144 |
||
1145 |
\begin{rail} |
|
1146 |
('datatype' | 'codatatype') domain? (dtspec + 'and') hints |
|
1147 |
; |
|
1148 |
||
1149 |
domain: ('<=' | subseteq) term |
|
1150 |
; |
|
1151 |
dtspec: term '=' (con + '|') |
|
1152 |
; |
|
1153 |
con: name ('(' (term ',' +) ')')? |
|
1154 |
; |
|
1155 |
hints: monos? typeintros? typeelims? |
|
1156 |
; |
|
1157 |
\end{rail} |
|
1158 |
||
1159 |
See \cite{isabelle-ZF} for further information on inductive definitions in |
|
1160 |
HOL, but note that this covers the old-style theory format. |
|
12621 | 1161 |
|
13024 | 1162 |
|
1163 |
\subsubsection{Primitive recursive functions} |
|
1164 |
||
1165 |
\indexisarcmdof{ZF}{primrec} |
|
1166 |
\begin{matharray}{rcl} |
|
1167 |
\isarcmd{primrec} & : & \isartrans{theory}{theory} \\ |
|
1168 |
\end{matharray} |
|
1169 |
||
1170 |
\begin{rail} |
|
1171 |
'primrec' (thmdecl? prop +) |
|
1172 |
; |
|
1173 |
\end{rail} |
|
1174 |
||
1175 |
||
13042 | 1176 |
\subsubsection{Cases and induction: emulating tactic scripts} |
13024 | 1177 |
|
1178 |
The following important tactical tools of Isabelle/ZF have been ported to |
|
1179 |
Isar. These should be never used in proper proof texts! |
|
1180 |
||
1181 |
\indexisarmethof{ZF}{case-tac}\indexisarmethof{ZF}{induct-tac} |
|
1182 |
\indexisarmethof{ZF}{ind-cases}\indexisarcmdof{ZF}{inductive-cases} |
|
1183 |
\begin{matharray}{rcl} |
|
1184 |
case_tac^* & : & \isarmeth \\ |
|
1185 |
induct_tac^* & : & \isarmeth \\ |
|
1186 |
ind_cases^* & : & \isarmeth \\ |
|
1187 |
\isarcmd{inductive_cases} & : & \isartrans{theory}{theory} \\ |
|
1188 |
\end{matharray} |
|
1189 |
||
1190 |
\begin{rail} |
|
1191 |
(casetac | inducttac) goalspec? name |
|
1192 |
; |
|
1193 |
indcases (prop +) |
|
1194 |
; |
|
1195 |
inductivecases (thmdecl? (prop +) + 'and') |
|
1196 |
; |
|
1197 |
\end{rail} |
|
12621 | 1198 |
|
13014 | 1199 |
%%% Local Variables: |
12621 | 1200 |
%%% mode: latex |
1201 |
%%% TeX-master: "isar-ref" |
|
13014 | 1202 |
%%% End: |