changeset 3108 | 335efc3f5632 |
parent 1905 | 81061bd61ad3 |
child 3201 | 7c3cbf675e85 |
3107:492a3d5d2b17 | 3108:335efc3f5632 |
---|---|
1 %% $Id$ |
1 %% $Id$ |
2 |
2 |
3 \chapter{Theories, Terms and Types} \label{theories} |
3 \chapter{Theories, Terms and Types} \label{theories} |
4 \index{theories|(}\index{signatures|bold} |
4 \index{theories|(}\index{signatures|bold} |
5 \index{reading!axioms|see{{\tt assume_ax}}} |
5 \index{reading!axioms|see{{\tt assume_ax}}} Theories organize the |
6 Theories organize the syntax, declarations and axioms of a mathematical |
6 syntax, declarations and axioms of a mathematical development. They |
7 development. They are built, starting from the Pure theory, by extending |
7 are built, starting from the {\Pure} or {\CPure} theory, by extending |
8 and merging existing theories. They have the \ML\ type \mltydx{theory}. |
8 and merging existing theories. They have the \ML\ type |
9 Theory operations signal errors by raising exception \xdx{THEORY}, |
9 \mltydx{theory}. Theory operations signal errors by raising exception |
10 returning a message and a list of theories. |
10 \xdx{THEORY}, returning a message and a list of theories. |
11 |
11 |
12 Signatures, which contain information about sorts, types, constants and |
12 Signatures, which contain information about sorts, types, constants and |
13 syntax, have the \ML\ type~\mltydx{Sign.sg}. For identification, each |
13 syntax, have the \ML\ type~\mltydx{Sign.sg}. For identification, each |
14 signature carries a unique list of \bfindex{stamps}, which are \ML\ |
14 signature carries a unique list of \bfindex{stamps}, which are \ML\ |
15 references to strings. The strings serve as human-readable names; the |
15 references to strings. The strings serve as human-readable names; the |
30 suffix {\tt .thy}). There is also a low level interface provided by certain |
30 suffix {\tt .thy}). There is also a low level interface provided by certain |
31 \ML{} functions (see \S\ref{BuildingATheory}). |
31 \ML{} functions (see \S\ref{BuildingATheory}). |
32 Appendix~\ref{app:TheorySyntax} presents the concrete syntax for theory |
32 Appendix~\ref{app:TheorySyntax} presents the concrete syntax for theory |
33 definitions; here is an explanation of the constituent parts: |
33 definitions; here is an explanation of the constituent parts: |
34 \begin{description} |
34 \begin{description} |
35 \item[{\it theoryDef}] |
35 \item[{\it theoryDef}] is the full definition. The new theory is |
36 is the full definition. The new theory is called $id$. It is the union |
36 called $id$. It is the union of the named {\bf parent |
37 of the named {\bf parent theories}\indexbold{theories!parent}, possibly |
37 theories}\indexbold{theories!parent}, possibly extended with new |
38 extended with new classes, etc. The basic theory, which contains only |
38 components. \thydx{Pure} and \thydx{CPure} are the basic theories, |
39 the meta-logic, is called \thydx{Pure}. |
39 which contain only the meta-logic. They differ just in their |
40 concrete syntax for function applications. |
|
40 |
41 |
41 Normally each {\it name\/} is an identifier, the name of the parent theory. |
42 Normally each {\it name\/} is an identifier, the name of the parent theory. |
42 Quoted strings can be used to document additional file dependencies; see |
43 Quoted strings can be used to document additional file dependencies; see |
43 \S\ref{LoadingTheories} for details. |
44 \S\ref{LoadingTheories} for details. |
44 |
45 |
54 introduces $sort$ as the new default sort for type variables. This applies |
55 introduces $sort$ as the new default sort for type variables. This applies |
55 to unconstrained type variables in an input string but not to type |
56 to unconstrained type variables in an input string but not to type |
56 variables created internally. If omitted, the default sort is the listwise |
57 variables created internally. If omitted, the default sort is the listwise |
57 union of the default sorts of the parent theories (i.e.\ their logical |
58 union of the default sorts of the parent theories (i.e.\ their logical |
58 intersection). |
59 intersection). |
59 |
60 |
60 \item[$sort$] |
61 \item[$sort$] is a finite set of classes. A single class $id$ |
61 is a finite set of classes. A single class $id$ abbreviates the singleton |
62 abbreviates the sort $\ttlbrace id\ttrbrace$. |
62 set {\tt\{}$id${\tt\}}. |
|
63 |
63 |
64 \item[$types$] |
64 \item[$types$] |
65 is a series of type declarations. Each declares a new type constructor |
65 is a series of type declarations. Each declares a new type constructor |
66 or type synonym. An $n$-place type constructor is specified by |
66 or type synonym. An $n$-place type constructor is specified by |
67 $(\alpha@1,\dots,\alpha@n)name$, where the type variables serve only to |
67 $(\alpha@1,\dots,\alpha@n)name$, where the type variables serve only to |
73 |
73 |
74 \item[$infix$] |
74 \item[$infix$] |
75 declares a type or constant to be an infix operator of priority $nat$ |
75 declares a type or constant to be an infix operator of priority $nat$ |
76 associating to the left ({\tt infixl}) or right ({\tt infixr}). Only |
76 associating to the left ({\tt infixl}) or right ({\tt infixr}). Only |
77 2-place type constructors can have infix status; an example is {\tt |
77 2-place type constructors can have infix status; an example is {\tt |
78 ('a,'b)~"*"~(infixr~20)}, which expresses binary product types. |
78 ('a,'b)~"*"~(infixr~20)}, which may express binary product types. |
79 |
79 |
80 \item[$arities$] |
80 \item[$arities$] is a series of type arity declarations. Each assigns |
81 is a series of arity declarations. Each assigns arities to type |
81 arities to type constructors. The $name$ must be an existing type |
82 constructors. The $name$ must be an existing type constructor, which is |
82 constructor, which is given the additional arity $arity$. |
83 given the additional arity $arity$. |
83 |
84 |
84 \item[$consts$] is a series of constant declarations. Each new |
85 \item[$constDecl$] |
85 constant $name$ is given the specified type. The optional $mixfix$ |
86 is a series of constant declarations. Each new constant $name$ is given |
86 annotations may attach concrete syntax to the constant. |
87 the specified type. The optional $mixfix$ annotations may |
87 |
88 attach concrete syntax to the constant. A variant of {\tt consts} is the |
88 \item[$syntax$] \index{*syntax section}\index{print mode} is a variant |
89 {\tt syntax} section\index{*syntax section}, which adds just syntax without |
89 of $consts$ which adds just syntax without actually declaring |
90 declaring logical constants. |
90 logical constants. This gives full control over a theory's context |
91 free grammar. The optional $mode$ specifies the print mode where the |
|
92 mixfix productions should be added. If there is no \texttt{output} |
|
93 option given, all productions are also added to the input syntax |
|
94 (regardless of the print mode). |
|
91 |
95 |
92 \item[$mixfix$] \index{mixfix declarations} |
96 \item[$mixfix$] \index{mixfix declarations} |
93 annotations can take three forms: |
97 annotations can take three forms: |
94 \begin{itemize} |
98 \begin{itemize} |
95 \item A mixfix template given as a $string$ of the form |
99 \item A mixfix template given as a $string$ of the form |
113 ==}). |
117 ==}). |
114 |
118 |
115 \item[$rules$] |
119 \item[$rules$] |
116 is a series of rule declarations. Each has a name $id$ and the formula is |
120 is a series of rule declarations. Each has a name $id$ and the formula is |
117 given by the $string$. Rule names must be distinct within any single |
121 given by the $string$. Rule names must be distinct within any single |
118 theory file. |
122 theory. |
119 |
123 |
120 \item[$defs$] is a series of definitions. They are just like $rules$, except |
124 \item[$defs$] is a series of definitions. They are just like $rules$, except |
121 that every $string$ must be a definition (see below for details). |
125 that every $string$ must be a definition (see below for details). |
122 |
126 |
123 \item[$constdefs$] combines the declaration of constants and their |
127 \item[$constdefs$] combines the declaration of constants and their |
124 definition. The first $string$ is the type, the second the definition. |
128 definition. The first $string$ is the type, the second the definition. |
129 |
|
130 \item[$axclass$] \index{*axclass section} defines an |
|
131 \rmindex{axiomatic type class} as the intersection of existing |
|
132 classes, with additional axioms holding. Class axioms may not |
|
133 contain more than one type variable. The class axioms (with implicit |
|
134 sort constraints added) are bound to the given names. Furthermore a |
|
135 class introduction rule is generated, which is automatically |
|
136 employed by $instance$ to prove instantiations of this class. |
|
137 |
|
138 \item[$instance$] \index{*instance section} proves class inclusions or |
|
139 type arities at the logical level and then transfers these to the |
|
140 type signature. The instantiation is proven and checked properly. |
|
141 The user has to supply sufficient witness information: theorems |
|
142 ($longident$), axioms ($string$), or even arbitrary \ML{} tactic |
|
143 code $verbatim$. |
|
125 |
144 |
126 \item[$oracle$] links the theory to a trusted external reasoner. It is |
145 \item[$oracle$] links the theory to a trusted external reasoner. It is |
127 allowed to create theorems, but each theorem carries a proof object |
146 allowed to create theorems, but each theorem carries a proof object |
128 describing the oracle invocation. See \S\ref{sec:oracles} for details. |
147 describing the oracle invocation. See \S\ref{sec:oracles} for details. |
129 |
148 |
135 declarations, translation rules and the {\tt ML} section in more detail. |
154 declarations, translation rules and the {\tt ML} section in more detail. |
136 |
155 |
137 |
156 |
138 \subsection{Definitions}\indexbold{definitions} |
157 \subsection{Definitions}\indexbold{definitions} |
139 |
158 |
140 {\bf Definitions} are intended to express abbreviations. The simplest form of |
159 {\bf Definitions} are intended to express abbreviations. The simplest |
141 a definition is $f \equiv t$, where $f$ is a constant. Isabelle also allows a |
160 form of a definition is $f \equiv t$, where $f$ is a constant. |
142 derived form where the arguments of~$f$ appear on the left, abbreviating a |
161 Isabelle also allows a derived forms where the arguments of~$f$ appear |
143 string of $\lambda$-abstractions. |
162 on the left, abbreviating a string of $\lambda$-abstractions. |
144 |
163 |
145 Isabelle makes the following checks on definitions: |
164 Isabelle makes the following checks on definitions: |
146 \begin{itemize} |
165 \begin{itemize} |
147 \item Arguments (on the left-hand side) must be distinct variables |
166 \item Arguments (on the left-hand side) must be distinct variables. |
148 \item All variables on the right-hand side must also appear on the left-hand |
167 \item All variables on the right-hand side must also appear on the left-hand |
149 side. |
168 side. |
150 \item All type variables on the right-hand side must also appear on the |
169 \item All type variables on the right-hand side must also appear on |
151 left-hand side; this prohibits definitions such as {\tt zero == length []}. |
170 the left-hand side; this prohibits definitions such as {\tt |
171 (zero::nat) == length ([]::'a list)}. |
|
152 \item The definition must not be recursive. Most object-logics provide |
172 \item The definition must not be recursive. Most object-logics provide |
153 definitional principles that can be used to express recursion safely. |
173 definitional principles that can be used to express recursion safely. |
154 \end{itemize} |
174 \end{itemize} |
155 These checks are intended to catch the sort of errors that might be made |
175 These checks are intended to catch the sort of errors that might be made |
156 accidentally. Misspellings, for instance, might result in additional |
176 accidentally. Misspellings, for instance, might result in additional |
162 \index{classes!context conditions}\index{arities!context conditions} |
182 \index{classes!context conditions}\index{arities!context conditions} |
163 |
183 |
164 In order to guarantee principal types~\cite{nipkow-prehofer}, |
184 In order to guarantee principal types~\cite{nipkow-prehofer}, |
165 arity declarations must obey two conditions: |
185 arity declarations must obey two conditions: |
166 \begin{itemize} |
186 \begin{itemize} |
167 \item There must be no two declarations $ty :: (\vec{r})c$ and $ty :: |
187 \item There must not be any two declarations $ty :: (\vec{r})c$ and |
168 (\vec{s})c$ with $\vec{r} \neq \vec{s}$. For example, the following is |
188 $ty :: (\vec{s})c$ with $\vec{r} \neq \vec{s}$. For example, this |
169 forbidden: |
189 excludes the following: |
170 \begin{ttbox} |
190 \begin{ttbox} |
171 types |
|
172 'a ty |
|
173 arities |
191 arities |
174 ty :: ({\ttlbrace}logic{\ttrbrace}) logic |
192 foo :: ({\ttlbrace}logic{\ttrbrace}) logic |
175 ty :: ({\ttlbrace}{\ttrbrace})logic |
193 foo :: ({\ttlbrace}{\ttrbrace})logic |
176 \end{ttbox} |
194 \end{ttbox} |
177 |
195 |
178 \item If there are two declarations $ty :: (s@1,\dots,s@n)c$ and $ty :: |
196 \item If there are two declarations $ty :: (s@1,\dots,s@n)c$ and $ty :: |
179 (s@1',\dots,s@n')c'$ such that $c' < c$ then $s@i' \preceq s@i$ must hold |
197 (s@1',\dots,s@n')c'$ such that $c' < c$ then $s@i' \preceq s@i$ must hold |
180 for $i=1,\dots,n$. The relationship $\preceq$, defined as |
198 for $i=1,\dots,n$. The relationship $\preceq$, defined as |
181 \[ s' \preceq s \iff \forall c\in s. \exists c'\in s'.~ c'\le c, \] |
199 \[ s' \preceq s \iff \forall c\in s. \exists c'\in s'.~ c'\le c, \] |
182 expresses that the set of types represented by $s'$ is a subset of the set of |
200 expresses that the set of types represented by $s'$ is a subset of the |
183 types represented by $s$. For example, the following is forbidden: |
201 set of types represented by $s$. Assuming $term \preceq logic$, the |
184 \begin{ttbox} |
202 following is forbidden: |
185 classes |
203 \begin{ttbox} |
186 term < logic |
|
187 types |
|
188 'a ty |
|
189 arities |
204 arities |
190 ty :: ({\ttlbrace}logic{\ttrbrace})logic |
205 foo :: ({\ttlbrace}logic{\ttrbrace})logic |
191 ty :: ({\ttlbrace}{\ttrbrace})term |
206 foo :: ({\ttlbrace}{\ttrbrace})term |
192 \end{ttbox} |
207 \end{ttbox} |
193 |
208 |
194 \end{itemize} |
209 \end{itemize} |
195 |
210 |
196 |
211 |
217 |
232 |
218 \item[\ttindexbold{delete_tmpfiles} := false;] |
233 \item[\ttindexbold{delete_tmpfiles} := false;] |
219 suppresses the deletion of temporary files. |
234 suppresses the deletion of temporary files. |
220 \end{ttdescription} |
235 \end{ttdescription} |
221 % |
236 % |
222 Each theory definition must reside in a separate file. Let the file {\it |
237 Each theory definition must reside in a separate file. Let the file |
223 T}{\tt.thy} contain the definition of a theory called~$T$, whose parent |
238 {\it T}{\tt.thy} contain the definition of a theory called~$T$, whose |
224 theories are $TB@1$ \dots $TB@n$. Calling \ttindexbold{use_thy}~{\tt"{\it |
239 parent theories are $TB@1$ \dots $TB@n$. Calling |
225 T\/}"} reads the file {\it T}{\tt.thy}, writes a temporary \ML{} |
240 \ttindex{use_thy}~{\tt"{\it T\/}"} reads the file {\it T}{\tt.thy}, |
226 file {\tt.{\it T}.thy.ML}, and reads the latter file. Recursive {\tt |
241 writes a temporary \ML{} file {\tt.{\it T}.thy.ML}, and reads the |
227 use_thy} calls load those parent theories that have not been loaded |
242 latter file. Recursive {\tt use_thy} calls load those parent theories |
228 previously; the recursive calls may continue to any depth. One {\tt use_thy} |
243 that have not been loaded previously; the recursive calls may continue |
229 call can read an entire logic provided all theories are linked appropriately. |
244 to any depth. One {\tt use_thy} call can read an entire logic |
245 provided all theories are linked appropriately. |
|
230 |
246 |
231 The result is an \ML\ structure~$T$ containing at least a component {\tt thy} |
247 The result is an \ML\ structure~$T$ containing at least a component {\tt thy} |
232 for the new theory and components for each of the rules. The structure also |
248 for the new theory and components for each of the rules. The structure also |
233 contains the definitions of the {\tt ML} section, if present. The file |
249 contains the definitions of the {\tt ML} section, if present. The file |
234 {\tt.{\it T}.thy.ML} is then deleted if {\tt delete_tmpfiles} is set to {\tt |
250 {\tt.{\it T}.thy.ML} is then deleted if {\tt delete_tmpfiles} is set to {\tt |
235 true} and no errors occurred. |
251 true} and no errors occurred. |
236 |
252 |
237 Finally the file {\it T}{\tt.ML} is read, if it exists. This file normally |
253 Finally the file {\it T}{\tt.ML} is read, if it exists. Since the |
238 begins with the declaration {\tt open~$T$} and contains proofs involving |
254 structure $T$ is automatically open in this context, proof scripts may |
239 the new theory. |
255 (or even should) refer to its components by unqualified names. |
240 |
256 |
241 Some applications construct theories directly by calling \ML\ functions. In |
257 Some applications construct theories directly by calling \ML\ functions. In |
242 this situation there is no {\tt.thy} file, only an {\tt.ML} file. The |
258 this situation there is no {\tt.thy} file, only an {\tt.ML} file. The |
243 {\tt.ML} file must declare an \ML\ structure having the theory's name and a |
259 {\tt.ML} file must declare an \ML\ structure having the theory's name and a |
244 component {\tt thy} containing the new theory object. |
260 component {\tt thy} containing the new theory object. |
282 theory files for $thyname$ then you must execute {\tt unlink_thy}; |
298 theory files for $thyname$ then you must execute {\tt unlink_thy}; |
283 otherwise {\tt update} will complain about a missing file. |
299 otherwise {\tt update} will complain about a missing file. |
284 \end{ttdescription} |
300 \end{ttdescription} |
285 |
301 |
286 |
302 |
287 \goodbreak |
303 %FIXME remove |
288 \subsection{Important note for Poly/ML users}\index{Poly/{\ML} compiler} |
304 %\goodbreak |
289 The theory mechanism depends upon reference variables. At the end of a |
305 %\subsection{Important note for Poly/ML users}\index{Poly/{\ML} compiler} |
290 Poly/\ML{} session, the contents of references are lost unless they are |
306 %The theory mechanism depends upon reference variables. At the end of a |
291 declared in the current database. In particular, assignments to references |
307 %Poly/\ML{} session, the contents of references are lost unless they are |
292 of the {\tt Pure} database are lost, including all information about loaded |
308 %declared in the current database. In particular, assignments to references |
293 theories. To avoid losing this information simply call |
309 %of the {\tt Pure} database are lost, including all information about loaded |
294 \begin{ttbox} |
310 %theories. To avoid losing this information simply call |
295 init_thy_reader(); |
311 %\begin{ttbox} |
296 \end{ttbox} |
312 %init_thy_reader(); |
297 when building the new database. |
313 %\end{ttbox} |
314 %when building the new database. |
|
298 |
315 |
299 |
316 |
300 \subsection{*Pseudo theories}\label{sec:pseudo-theories} |
317 \subsection{*Pseudo theories}\label{sec:pseudo-theories} |
301 \indexbold{theories!pseudo}% |
318 \indexbold{theories!pseudo}% |
302 Any automatic reloading facility requires complete knowledge of all |
319 Any automatic reloading facility requires complete knowledge of all |
344 orphan = \(A@1\) + \(\ldots\) + \(A@n\) |
361 orphan = \(A@1\) + \(\ldots\) + \(A@n\) |
345 \end{ttbox} |
362 \end{ttbox} |
346 The resulting theory ensures that {\tt update} reloads {\tt orphan} |
363 The resulting theory ensures that {\tt update} reloads {\tt orphan} |
347 whenever it reloads one of the $A@i$. |
364 whenever it reloads one of the $A@i$. |
348 |
365 |
349 For an extensive example of how this technique can be used to link lots of |
366 For an extensive example of how this technique can be used to link |
350 theory files and load them by just a few {\tt use_thy} calls, consult the |
367 lots of theory files and load them by just a few {\tt use_thy} calls |
351 sources of \ZF{} set theory. |
368 see the sources of one of the major object-logics (e.g.\ \ZF). |
352 |
369 |
353 |
370 |
354 |
371 |
355 \section{Basic operations on theories}\label{BasicOperationsOnTheories} |
372 \section{Basic operations on theories}\label{BasicOperationsOnTheories} |
356 \subsection{Extracting an axiom or theorem from a theory} |
373 \subsection{Extracting an axiom or theorem from a theory} |
382 For example, if {\it formula} is |
399 For example, if {\it formula} is |
383 \hbox{\tt a=b ==> b=a} then the resulting theorem has the form |
400 \hbox{\tt a=b ==> b=a} then the resulting theorem has the form |
384 \hbox{\verb'?a=?b ==> ?b=?a [!!a b. a=b ==> b=a]'} |
401 \hbox{\verb'?a=?b ==> ?b=?a [!!a b. a=b ==> b=a]'} |
385 \end{ttdescription} |
402 \end{ttdescription} |
386 |
403 |
387 \subsection{Building a theory} |
404 \subsection{*Building a theory} |
388 \label{BuildingATheory} |
405 \label{BuildingATheory} |
389 \index{theories!constructing|bold} |
406 \index{theories!constructing|bold} |
390 \begin{ttbox} |
407 \begin{ttbox} |
391 pure_thy : theory |
408 Pure.thy : theory |
409 CPure.thy : theory |
|
392 merge_theories : theory * theory -> theory |
410 merge_theories : theory * theory -> theory |
393 \end{ttbox} |
411 \end{ttbox} |
394 \begin{ttdescription} |
412 \begin{description} |
395 \item[\ttindexbold{pure_thy}] contains just the syntax and signature |
413 \item[\ttindexbold{Pure.thy}, \ttindexbold{CPure.thy}] contain the |
396 of the meta-logic. There are no axioms: meta-level inferences are carried |
414 syntax and signature of the meta-logic. There are no axioms: |
397 out by \ML\ functions. |
415 meta-level inferences are carried out by \ML\ functions. The two |
416 \Pure s just differ in their concrete syntax of function |
|
417 application: $t(u@1, \ldots, u@n)$ vs.\ $t\,u@1,\ldots\,u@n$. |
|
418 |
|
398 \item[\ttindexbold{merge_theories} ($thy@1$, $thy@2$)] merges the two |
419 \item[\ttindexbold{merge_theories} ($thy@1$, $thy@2$)] merges the two |
399 theories $thy@1$ and $thy@2$. The resulting theory contains all of the |
420 theories $thy@1$ and $thy@2$. The resulting theory contains all of the |
400 syntax, signature and axioms of the constituent theories. Merging theories |
421 syntax, signature and axioms of the constituent theories. Merging theories |
401 that contain different identification stamps of the same name fails with |
422 that contain different identification stamps of the same name fails with |
402 the following message |
423 the following message |
417 % different theories having the same name $T$ yields the fatal error |
438 % different theories having the same name $T$ yields the fatal error |
418 %extend_theory : theory -> string -> \(\cdots\) -> theory |
439 %extend_theory : theory -> string -> \(\cdots\) -> theory |
419 %\begin{ttbox} |
440 %\begin{ttbox} |
420 %Attempt to merge different versions of theory: \(T\) |
441 %Attempt to merge different versions of theory: \(T\) |
421 %\end{ttbox} |
442 %\end{ttbox} |
422 \end{ttdescription} |
443 \end{description} |
423 |
444 |
424 %% FIXME |
445 %% FIXME |
425 %\item [\ttindexbold{extend_theory} $thy$ {\tt"}$T${\tt"} |
446 %\item [\ttindexbold{extend_theory} $thy$ {\tt"}$T${\tt"} |
426 % ($classes$, $default$, $types$, $arities$, $consts$, $sextopt$) $rules$] |
447 % ($classes$, $default$, $types$, $arities$, $consts$, $sextopt$) $rules$] |
427 %\hfill\break %%% include if line is just too short |
448 %\hfill\break %%% include if line is just too short |
454 |
475 |
455 |
476 |
456 \subsection{Inspecting a theory}\label{sec:inspct-thy} |
477 \subsection{Inspecting a theory}\label{sec:inspct-thy} |
457 \index{theories!inspecting|bold} |
478 \index{theories!inspecting|bold} |
458 \begin{ttbox} |
479 \begin{ttbox} |
480 print_syntax : theory -> unit |
|
459 print_theory : theory -> unit |
481 print_theory : theory -> unit |
460 axioms_of : theory -> (string * thm) list |
482 axioms_of : theory -> (string * thm) list |
461 thms_of : theory -> (string * thm) list |
483 thms_of : theory -> (string * thm) list |
462 parents_of : theory -> theory list |
484 parents_of : theory -> theory list |
463 sign_of : theory -> Sign.sg |
485 sign_of : theory -> Sign.sg |
464 stamps_of_thy : theory -> string ref list |
486 stamps_of_thy : theory -> string ref list |
465 \end{ttbox} |
487 \end{ttbox} |
466 These provide means of viewing a theory's components. |
488 These provide means of viewing a theory's components. |
467 \begin{ttdescription} |
489 \begin{ttdescription} |
468 \item[\ttindexbold{print_theory} $thy$] |
490 \item[\ttindexbold{print_syntax} $thy$] prints the syntax of $thy$ |
469 prints the contents of $thy$ excluding the syntax related parts (which are |
491 (grammar, macros, translation functions etc., see |
470 shown by {\tt print_syntax}). The output is quite verbose. |
492 page~\pageref{pg:print_syn} for more details). |
493 |
|
494 \item[\ttindexbold{print_theory} $thy$] prints the logical parts of |
|
495 $thy$, excluding the syntax. |
|
471 |
496 |
472 \item[\ttindexbold{axioms_of} $thy$] |
497 \item[\ttindexbold{axioms_of} $thy$] |
473 returns the additional axioms of the most recent extend node of~$thy$. |
498 returns the additional axioms of the most recent extend node of~$thy$. |
474 |
499 |
475 \item[\ttindexbold{thms_of} $thy$] |
500 \item[\ttindexbold{thms_of} $thy$] |
485 \item[\ttindexbold{stamps_of_thy} $thy$]\index{signatures} |
510 \item[\ttindexbold{stamps_of_thy} $thy$]\index{signatures} |
486 returns the identification \rmindex{stamps} of the signature associated |
511 returns the identification \rmindex{stamps} of the signature associated |
487 with~$thy$. |
512 with~$thy$. |
488 \end{ttdescription} |
513 \end{ttdescription} |
489 |
514 |
490 |
515 %FIXME move to sysman! |
491 \section{Generating HTML documents} |
516 %\section{Generating HTML documents} |
492 \index{HTML|bold} |
517 %\index{HTML|bold} |
493 |
518 % |
494 Isabelle is able to make HTML documents that show a theory's |
519 %Isabelle is able to make HTML documents that show a theory's |
495 definition, the theorems proved in its ML file and the relationship |
520 %definition, the theorems proved in its ML file and the relationship |
496 with its ancestors and descendants. HTML stands for Hypertext Markup |
521 %with its ancestors and descendants. HTML stands for Hypertext Markup |
497 Language and is used in the World Wide Web to represent text |
522 %Language and is used in the World Wide Web to represent text |
498 containing images and links to other documents. Web browsers like |
523 %containing images and links to other documents. Web browsers like |
499 {\tt xmosaic} or {\tt netscape} are used to view these documents. |
524 %{\tt xmosaic} or {\tt netscape} are used to view these documents. |
500 |
525 % |
501 Besides the three HTML files that are made for every theory |
526 %Besides the three HTML files that are made for every theory |
502 (definition and theorems, ancestors, descendants), Isabelle stores |
527 %(definition and theorems, ancestors, descendants), Isabelle stores |
503 links to all theories in an index file. These indexes are themself |
528 %links to all theories in an index file. These indexes are themself |
504 linked with other indexes to represent the hierarchic structure of |
529 %linked with other indexes to represent the hierarchic structure of |
505 Isabelle's logics. |
530 %Isabelle's logics. |
506 |
531 % |
507 To make HTML files for logics that are part of the Isabelle |
532 %To make HTML files for logics that are part of the Isabelle |
508 distribution, simply set the shell environment variable {\tt |
533 %distribution, simply set the shell environment variable {\tt |
509 MAKE_HTML} before compiling a logic. This works for single logics as |
534 %MAKE_HTML} before compiling a logic. This works for single logics as |
510 well as for the shell script {\tt make-all} (see |
535 %well as for the shell script {\tt make-all} (see |
511 \ref{sec:shell-scripts}). To make HTML files for {\tt FOL} using a |
536 %\ref{sec:shell-scripts}). To make HTML files for {\tt FOL} using a |
512 {\tt csh} style shell, the following commands can be used: |
537 %{\tt csh} style shell, the following commands can be used: |
513 |
538 % |
514 \begin{ttbox} |
539 %\begin{ttbox} |
515 cd FOL |
540 %cd FOL |
516 setenv MAKE_HTML |
541 %setenv MAKE_HTML |
517 make |
542 %make |
518 \end{ttbox} |
543 %\end{ttbox} |
519 |
544 % |
520 The databases made this way do not differ from the ones made with an |
545 %The databases made this way do not differ from the ones made with an |
521 unset {\tt MAKE_HTML}; in particular no HTML files are written if the |
546 %unset {\tt MAKE_HTML}; in particular no HTML files are written if the |
522 database is used to manually load a theory. |
547 %database is used to manually load a theory. |
523 |
548 % |
524 As you will see below, the HTML generation is controlled by a boolean |
549 %As you will see below, the HTML generation is controlled by a boolean |
525 reference variable. If you want to make databases which define this |
550 %reference variable. If you want to make databases which define this |
526 variable's value as {\tt true} and where therefore HTML files are |
551 %variable's value as {\tt true} and where therefore HTML files are |
527 written each time {\tt use_thy} is invoked, you have to set {\tt |
552 %written each time {\tt use_thy} is invoked, you have to set {\tt |
528 MAKE_HTML} to ``{\tt true}'': |
553 %MAKE_HTML} to ``{\tt true}'': |
529 |
554 % |
530 \begin{ttbox} |
555 %\begin{ttbox} |
531 cd FOL |
556 %cd FOL |
532 setenv MAKE_HTML true |
557 %setenv MAKE_HTML true |
533 make |
558 %make |
534 \end{ttbox} |
559 %\end{ttbox} |
535 |
560 % |
536 All theories loaded from within the {\tt FOL} database and all |
561 %All theories loaded from within the {\tt FOL} database and all |
537 databases derived from it will now cause HTML files to be written. |
562 %databases derived from it will now cause HTML files to be written. |
538 This behaviour can be changed by assigning a value of {\tt false} to |
563 %This behaviour can be changed by assigning a value of {\tt false} to |
539 the boolean reference variable {\tt make_html}. Be careful when making |
564 %the boolean reference variable {\tt make_html}. Be careful when making |
540 such databases publicly available since it means that your users will |
565 %such databases publicly available since it means that your users will |
541 generate HTML files though they might not intend to do so. |
566 %generate HTML files though they might not intend to do so. |
542 |
567 % |
543 As some of Isabelle's logics are based on others (e.g. {\tt ZF} on |
568 %As some of Isabelle's logics are based on others (e.g. {\tt ZF} on |
544 {\tt FOL}) and because the HTML files list a theory's ancestors, you |
569 %{\tt FOL}) and because the HTML files list a theory's ancestors, you |
545 should not make HTML files for a logic if the HTML files for the base |
570 %should not make HTML files for a logic if the HTML files for the base |
546 logic do not exist. Otherwise some of the hypertext links might point |
571 %logic do not exist. Otherwise some of the hypertext links might point |
547 to non-existing documents. |
572 %to non-existing documents. |
548 |
573 % |
549 The entry point to all logics is the {\tt index.html} file located in |
574 %The entry point to all logics is the {\tt index.html} file located in |
550 Isabelle's main directory. You can also access a HTML version of the |
575 %Isabelle's main directory. You can also access a HTML version of the |
551 distribution package at |
576 %distribution package at |
552 |
577 % |
553 \begin{ttbox} |
578 %\begin{ttbox} |
554 http://www4.informatik.tu-muenchen.de/~nipkow/isabelle |
579 %http://www4.informatik.tu-muenchen.de/~nipkow/isabelle/ |
555 \end{ttbox} |
580 %\end{ttbox} |
556 |
581 % |
557 |
582 % |
558 \subsection*{Manual HTML generation} |
583 %\subsection*{Manual HTML generation} |
559 |
584 % |
560 To manually control the generation of HTML files the following |
585 %To manually control the generation of HTML files the following |
561 commands and reference variables are used: |
586 %commands and reference variables are used: |
562 |
587 % |
563 \begin{ttbox} |
588 %\begin{ttbox} |
564 init_html : unit -> unit |
589 %init_html : unit -> unit |
565 make_html : bool ref |
590 %make_html : bool ref |
566 finish_html : unit -> unit |
591 %finish_html : unit -> unit |
567 \end{ttbox} |
592 %\end{ttbox} |
568 |
593 % |
569 \begin{ttdescription} |
594 %\begin{ttdescription} |
570 \item[\ttindexbold{init_html}] |
595 %\item[\ttindexbold{init_html}] |
571 activates the HTML facility. It stores the current working directory |
596 %activates the HTML facility. It stores the current working directory |
572 as the place where the {\tt index.html} file for all theories loaded |
597 %as the place where the {\tt index.html} file for all theories loaded |
573 afterwards will be stored. |
598 %afterwards will be stored. |
574 |
599 % |
575 \item[\ttindexbold{make_html}] |
600 %\item[\ttindexbold{make_html}] |
576 is a boolean reference variable read by {\tt use_thy} and other |
601 %is a boolean reference variable read by {\tt use_thy} and other |
577 functions to decide whether HTML files should be made. After you have |
602 %functions to decide whether HTML files should be made. After you have |
578 used {\tt init_html} you can manually change {\tt make_html}'s value |
603 %used {\tt init_html} you can manually change {\tt make_html}'s value |
579 to temporarily disable HTML generation. |
604 %to temporarily disable HTML generation. |
580 |
605 % |
581 \item[\ttindexbold{finish_html}] |
606 %\item[\ttindexbold{finish_html}] |
582 has to be called after all theories have been read that should be |
607 %has to be called after all theories have been read that should be |
583 listed in the current {\tt index.html} file. It reads a temporary |
608 %listed in the current {\tt index.html} file. It reads a temporary |
584 file with information about the theories read since the last use of |
609 %file with information about the theories read since the last use of |
585 {\tt init_html} and makes the {\tt index.html} file. If {\tt |
610 %{\tt init_html} and makes the {\tt index.html} file. If {\tt |
586 make_html} is {\tt false} nothing is done. |
611 %make_html} is {\tt false} nothing is done. |
587 |
612 % |
588 The indexes made by this function also contain a link to the {\tt |
613 %The indexes made by this function also contain a link to the {\tt |
589 README} file if there exists one in the directory where the index is |
614 %README} file if there exists one in the directory where the index is |
590 stored. If there's a {\tt README.html} file it is used instead of |
615 %stored. If there's a {\tt README.html} file it is used instead of |
591 {\tt README}. |
616 %{\tt README}. |
592 |
617 % |
593 \end{ttdescription} |
618 %\end{ttdescription} |
594 |
619 % |
595 The above functions could be used in the following way: |
620 %The above functions could be used in the following way: |
596 |
621 % |
597 \begin{ttbox} |
622 %\begin{ttbox} |
598 init_html(); |
623 %init_html(); |
599 {\out Setting path for index.html to "/home/clasohm/isabelle/HOL"} |
624 %{\out Setting path for index.html to "/home/clasohm/isabelle/HOL"} |
600 use_thy "List"; |
625 %use_thy "List"; |
601 \dots |
626 %\dots |
602 finish_html(); |
627 %finish_html(); |
603 \end{ttbox} |
628 %\end{ttbox} |
604 |
629 % |
605 Please note that HTML files are made only for those theories that are |
630 %Please note that HTML files are made only for those theories that are |
606 read while {\tt make_html} is {\tt true}. These files may contain |
631 %read while {\tt make_html} is {\tt true}. These files may contain |
607 links to theories that were read with a {\tt false} {\tt make_html} |
632 %links to theories that were read with a {\tt false} {\tt make_html} |
608 and therefore point to non-existing files. |
633 %and therefore point to non-existing files. |
609 |
634 % |
610 |
635 % |
611 \subsection*{Extending or adding a logic} |
636 %\subsection*{Extending or adding a logic} |
612 |
637 % |
613 If you add a new subdirectory to Isabelle's logics (or add a completly |
638 %If you add a new subdirectory to Isabelle's logics (or add a completly |
614 new logic), you would have to call {\tt init_html} at the start of every |
639 %new logic), you would have to call {\tt init_html} at the start of every |
615 directory's {\tt ROOT.ML} file and {\tt finish_html} at the end of |
640 %directory's {\tt ROOT.ML} file and {\tt finish_html} at the end of |
616 it. This is automatically done if you use |
641 %it. This is automatically done if you use |
617 |
642 % |
618 \begin{ttbox}\index{use_dir} |
643 %\begin{ttbox}\index{use_dir} |
619 use_dir : string -> unit |
644 %use_dir : string -> unit |
620 \end{ttbox} |
645 %\end{ttbox} |
621 |
646 % |
622 This function takes a path as its parameter, changes the working |
647 %This function takes a path as its parameter, changes the working |
623 directory, calls {\tt init_html} if {\tt make_html} is {\tt true}, |
648 %directory, calls {\tt init_html} if {\tt make_html} is {\tt true}, |
624 executes {\tt ROOT.ML}, and calls {\tt finish_html}. The {\tt |
649 %executes {\tt ROOT.ML}, and calls {\tt finish_html}. The {\tt |
625 index.html} file written in this directory will be automatically |
650 %index.html} file written in this directory will be automatically |
626 linked to the first index found in the (recursively searched) |
651 %linked to the first index found in the (recursively searched) |
627 superdirectories. |
652 %superdirectories. |
628 |
653 % |
629 Instead of adding something like |
654 %Instead of adding something like |
630 |
655 % |
631 \begin{ttbox} |
656 %\begin{ttbox} |
632 use"ex/ROOT.ML"; |
657 %use"ex/ROOT.ML"; |
633 \end{ttbox} |
658 %\end{ttbox} |
634 |
659 % |
635 to the logic's makefile you have to use this: |
660 %to the logic's makefile you have to use this: |
636 |
661 % |
637 \begin{ttbox} |
662 %\begin{ttbox} |
638 use_dir"ex"; |
663 %use_dir"ex"; |
639 \end{ttbox} |
664 %\end{ttbox} |
640 |
665 % |
641 Since {\tt use_dir} calls {\tt init_html} only if {\tt make_html} is |
666 %Since {\tt use_dir} calls {\tt init_html} only if {\tt make_html} is |
642 {\tt true} the generation of HTML files depends on the value this |
667 %{\tt true} the generation of HTML files depends on the value this |
643 reference variable has. It can either be inherited from the used \ML{} |
668 %reference variable has. It can either be inherited from the used \ML{} |
644 database or set in the makefile before {\tt use_dir} is invoked, |
669 %database or set in the makefile before {\tt use_dir} is invoked, |
645 e.g. to set it's value according to the environment variable {\tt |
670 %e.g. to set it's value according to the environment variable {\tt |
646 MAKE_HTML}. |
671 %MAKE_HTML}. |
647 |
672 % |
648 The generated HTML files contain all theorems that were proved in the |
673 %The generated HTML files contain all theorems that were proved in the |
649 theory's \ML{} file with {\tt qed}, {\tt qed_goal} and {\tt qed_goalw}, |
674 %theory's \ML{} file with {\tt qed}, {\tt qed_goal} and {\tt qed_goalw}, |
650 or stored with {\tt bind_thm} and {\tt store_thm}. Additionally there |
675 %or stored with {\tt bind_thm} and {\tt store_thm}. Additionally there |
651 is a hypertext link to the whole \ML{} file. |
676 %is a hypertext link to the whole \ML{} file. |
652 |
677 % |
653 You can add section headings to the list of theorems by using |
678 %You can add section headings to the list of theorems by using |
654 |
679 % |
655 \begin{ttbox}\index{use_dir} |
680 %\begin{ttbox}\index{use_dir} |
656 section: string -> unit |
681 %section: string -> unit |
657 \end{ttbox} |
682 %\end{ttbox} |
658 |
683 % |
659 in a theory's ML file, which converts a plain string to a HTML |
684 %in a theory's ML file, which converts a plain string to a HTML |
660 heading and inserts it before the next theorem proved or stored with |
685 %heading and inserts it before the next theorem proved or stored with |
661 one of the above functions. If {\tt make_html} is {\tt false} nothing |
686 %one of the above functions. If {\tt make_html} is {\tt false} nothing |
662 is done. |
687 %is done. |
663 |
688 % |
664 |
689 % |
665 \subsection*{Using someone else's database} |
690 %\subsection*{Using someone else's database} |
666 |
691 % |
667 To make them independent from their storage place, the HTML files only |
692 %To make them independent from their storage place, the HTML files only |
668 contain relative paths which are derived from absolute ones like the |
693 %contain relative paths which are derived from absolute ones like the |
669 current working directory, {\tt gif_path} or {\tt base_path}. The |
694 %current working directory, {\tt gif_path} or {\tt base_path}. The |
670 latter two are reference variables which are initialized at the time |
695 %latter two are reference variables which are initialized at the time |
671 when the {\tt Pure} database is made. Because you need write access |
696 %when the {\tt Pure} database is made. Because you need write access |
672 for the current directory to make HTML files and therefore (probably) |
697 %for the current directory to make HTML files and therefore (probably) |
673 generate them in your home directory, the absolute {\tt base_path} is |
698 %generate them in your home directory, the absolute {\tt base_path} is |
674 not correct if you use someone else's database or a database derived |
699 %not correct if you use someone else's database or a database derived |
675 from it. |
700 %from it. |
676 |
701 % |
677 In that case you first should set {\tt base_path} to the value of {\em |
702 %In that case you first should set {\tt base_path} to the value of {\em |
678 your} Isabelle main directory, i.e. the directory that contains the |
703 %your} Isabelle main directory, i.e. the directory that contains the |
679 subdirectories where standard logics like {\tt FOL} and {\tt HOL} or |
704 %subdirectories where standard logics like {\tt FOL} and {\tt HOL} or |
680 your own logics are stored. If you do not do this, the generated HTML |
705 %your own logics are stored. If you do not do this, the generated HTML |
681 files will still be usable but may contain incomplete titles and lack |
706 %files will still be usable but may contain incomplete titles and lack |
682 some hypertext links. |
707 %some hypertext links. |
683 |
708 % |
684 It's also a good idea to set {\tt gif_path} which points to the |
709 %It's also a good idea to set {\tt gif_path} which points to the |
685 directory containing two GIF images used in the HTML |
710 %directory containing two GIF images used in the HTML |
686 documents. Normally this is the {\tt Tools} subdirectory of Isabelle's |
711 %documents. Normally this is the {\tt Tools} subdirectory of Isabelle's |
687 main directory. While its value in general is still valid, your HTML |
712 %main directory. While its value in general is still valid, your HTML |
688 files would depend on files not owned by you. This prevents you from |
713 %files would depend on files not owned by you. This prevents you from |
689 changing the location of the HTML files (as they contain relative |
714 %changing the location of the HTML files (as they contain relative |
690 paths) and also causes trouble if the database's maker (re)moves the |
715 %paths) and also causes trouble if the database's maker (re)moves the |
691 GIFs. |
716 %GIFs. |
692 |
717 % |
693 Here's what you should do before invoking {\tt init_html} using |
718 %Here's what you should do before invoking {\tt init_html} using |
694 someone else's \ML{} database: |
719 %someone else's \ML{} database: |
695 |
720 % |
696 \begin{ttbox} |
721 %\begin{ttbox} |
697 base_path := "/home/smith/isabelle"; |
722 %base_path := "/home/smith/isabelle"; |
698 gif_path := "/home/smith/isabelle/Tools"; |
723 %gif_path := "/home/smith/isabelle/Tools"; |
699 init_html(); |
724 %init_html(); |
700 \dots |
725 %\dots |
701 \end{ttbox} |
726 %\end{ttbox} |
727 |
|
702 |
728 |
703 \section{Terms} |
729 \section{Terms} |
704 \index{terms|bold} |
730 \index{terms|bold} |
705 Terms belong to the \ML\ type \mltydx{term}, which is a concrete datatype |
731 Terms belong to the \ML\ type \mltydx{term}, which is a concrete datatype |
706 with six constructors: there are six kinds of term. |
732 with six constructors: |
707 \begin{ttbox} |
733 \begin{ttbox} |
708 type indexname = string * int; |
734 type indexname = string * int; |
709 infix 9 $; |
735 infix 9 $; |
710 datatype term = Const of string * typ |
736 datatype term = Const of string * typ |
711 | Free of string * typ |
737 | Free of string * typ |
842 \begin{ttbox} |
868 \begin{ttbox} |
843 cterm_of : Sign.sg -> term -> cterm |
869 cterm_of : Sign.sg -> term -> cterm |
844 read_cterm : Sign.sg -> string * typ -> cterm |
870 read_cterm : Sign.sg -> string * typ -> cterm |
845 cert_axm : Sign.sg -> string * term -> string * term |
871 cert_axm : Sign.sg -> string * term -> string * term |
846 read_axm : Sign.sg -> string * string -> string * term |
872 read_axm : Sign.sg -> string * string -> string * term |
847 rep_cterm : cterm -> \{T:typ, t:term, sign:Sign.sg, maxidx:int\} |
873 rep_cterm : cterm -> {\ttlbrace}T:typ, t:term, sign:Sign.sg, maxidx:int\ttrbrace |
848 \end{ttbox} |
874 \end{ttbox} |
849 \begin{ttdescription} |
875 \begin{ttdescription} |
850 \item[\ttindexbold{cterm_of} $sign$ $t$] \index{signatures} |
876 \item[\ttindexbold{cterm_of} $sign$ $t$] \index{signatures} |
851 certifies $t$ with respect to signature~$sign$. |
877 certifies $t$ with respect to signature~$sign$. |
852 |
878 |
930 |
956 |
931 |
957 |
932 \subsection{Making and inspecting certified types} |
958 \subsection{Making and inspecting certified types} |
933 \begin{ttbox} |
959 \begin{ttbox} |
934 ctyp_of : Sign.sg -> typ -> ctyp |
960 ctyp_of : Sign.sg -> typ -> ctyp |
935 rep_ctyp : ctyp -> \{T: typ, sign: Sign.sg\} |
961 rep_ctyp : ctyp -> {\ttlbrace}T: typ, sign: Sign.sg\ttrbrace |
936 \end{ttbox} |
962 \end{ttbox} |
937 \begin{ttdescription} |
963 \begin{ttdescription} |
938 \item[\ttindexbold{ctyp_of} $sign$ $T$] \index{signatures} |
964 \item[\ttindexbold{ctyp_of} $sign$ $T$] \index{signatures} |
939 certifies $T$ with respect to signature~$sign$. |
965 certifies $T$ with respect to signature~$sign$. |
940 |
966 |
966 does not have an oracle, if the oracle rejects its arguments or if its |
992 does not have an oracle, if the oracle rejects its arguments or if its |
967 result is ill-typed. |
993 result is ill-typed. |
968 |
994 |
969 \item[\ttindexbold{set_oracle} $fn$ $thy$] sets the oracle of theory $thy$ to |
995 \item[\ttindexbold{set_oracle} $fn$ $thy$] sets the oracle of theory $thy$ to |
970 be $fn$. It is seldom called explicitly, as there is syntax for oracles in |
996 be $fn$. It is seldom called explicitly, as there is syntax for oracles in |
971 theory files. A theory can have at most one oracle. |
997 theory files. Any theory node can have at most one oracle. |
972 \end{ttdescription} |
998 \end{ttdescription} |
973 |
999 |
974 A curious feature of {\ML} exceptions is that they are ordinary constructors. |
1000 A curious feature of {\ML} exceptions is that they are ordinary constructors. |
975 The {\ML} type {\tt exn} is a datatype that can be extended at any time. (See |
1001 The {\ML} type {\tt exn} is a datatype that can be extended at any time. (See |
976 my {\em {ML} for the Working Programmer}~\cite{paulson-ml2}, especially |
1002 my {\em {ML} for the Working Programmer}~\cite{paulson-ml2}, especially |