lcp@104
|
1 |
%% $Id$
|
lcp@104
|
2 |
\chapter{Theories, Terms and Types} \label{theories}
|
lcp@104
|
3 |
\index{theories|(}\index{signatures|bold}
|
lcp@104
|
4 |
\index{reading!axioms|see{{\tt extend_theory} and {\tt assume_ax}}}
|
lcp@104
|
5 |
Theories organize the syntax, declarations and axioms of a mathematical
|
lcp@104
|
6 |
development. They are built, starting from the Pure theory, by extending
|
lcp@104
|
7 |
and merging existing theories. They have the \ML{} type \ttindex{theory}.
|
lcp@104
|
8 |
Theory operations signal errors by raising exception \ttindex{THEORY},
|
lcp@104
|
9 |
returning a message and a list of theories.
|
lcp@104
|
10 |
|
lcp@104
|
11 |
Signatures, which contain information about sorts, types, constants and
|
lcp@104
|
12 |
syntax, have the \ML{} type~\ttindexbold{Sign.sg}. For identification,
|
lcp@104
|
13 |
each signature carries a unique list of {\bf stamps}, which are~\ML{}
|
lcp@104
|
14 |
references (to strings). The strings serve as human-readable names; the
|
lcp@104
|
15 |
references serve as unique identifiers. Each primitive signature has a
|
lcp@104
|
16 |
single stamp. When two signatures are merged, their lists of stamps are
|
lcp@104
|
17 |
also merged. Every theory carries a unique signature.
|
lcp@104
|
18 |
|
lcp@104
|
19 |
Terms and types are the underlying representation of logical syntax. Their
|
lcp@104
|
20 |
\ML{} definitions are irrelevant to naive Isabelle users. Programmers who wish
|
lcp@104
|
21 |
to extend Isabelle may need to know such details, say to code a tactic that
|
lcp@104
|
22 |
looks for subgoals of a particular form. Terms and types may be
|
lcp@104
|
23 |
`certified' to be well-formed with respect to a given signature.
|
lcp@104
|
24 |
|
lcp@104
|
25 |
\section{Defining Theories}
|
lcp@104
|
26 |
\label{DefiningTheories}
|
lcp@104
|
27 |
|
lcp@104
|
28 |
Theories can be defined either using concrete syntax or by calling certain
|
lcp@104
|
29 |
\ML-functions (see \S\ref{BuildingATheory}). Figure~\ref{TheorySyntax}
|
lcp@104
|
30 |
presents the concrete syntax for theories. This grammar employs the
|
lcp@104
|
31 |
following conventions:
|
lcp@104
|
32 |
\begin{itemize}
|
lcp@104
|
33 |
\item Identifiers such as $theoryDef$ denote nonterminal symbols.
|
lcp@104
|
34 |
\item Text in {\tt typewriter font} denotes terminal symbols.
|
lcp@104
|
35 |
\item \ldots{} indicates repetition of a phrase.
|
lcp@104
|
36 |
\item A vertical bar~($|$) separates alternative phrases.
|
lcp@104
|
37 |
\item Square [brackets] enclose optional phrases.
|
lcp@104
|
38 |
\item $id$ stands for an Isabelle identifier.
|
lcp@104
|
39 |
\item $string$ stands for an ML string, with its quotation marks.
|
lcp@104
|
40 |
\item $k$ stands for a natural number.
|
lcp@104
|
41 |
\item $text$ stands for arbitrary ML text.
|
lcp@104
|
42 |
\end{itemize}
|
lcp@104
|
43 |
|
lcp@104
|
44 |
\begin{figure}[hp]
|
lcp@104
|
45 |
\begin{center}
|
lcp@104
|
46 |
\begin{tabular}{rclc}
|
clasohm@138
|
47 |
$theoryDef$ &=& $id$ {\tt=} $name@1$ {\tt+} \dots {\tt+} $name@n$
|
lcp@104
|
48 |
[{\tt+} $extension$]\\\\
|
lcp@104
|
49 |
$extension$ &=& [$classes$] [$default$] [$types$] [$arities$] [$consts$]
|
lcp@104
|
50 |
[$rules$] {\tt end} [$ml$]\\\\
|
lcp@104
|
51 |
$classes$ &=& \ttindex{classes} $class$ \dots $class$ \\\\
|
lcp@104
|
52 |
$class$ &=& $id$ [{\tt<} $id@1${\tt,} \dots{\tt,} $id@n$] \\\\
|
lcp@104
|
53 |
$default$ &=& \ttindex{default} $sort$ \\\\
|
lcp@104
|
54 |
$sort$ &=& $id$ ~~$|$~~ {\tt\{} $id@1${\tt,} \dots{\tt,} $id@n$ {\tt\}} \\\\
|
lcp@104
|
55 |
$name$ &=& $id$ ~~$|$~~ $string$ \\\\
|
lcp@104
|
56 |
$types$ &=& \ttindex{types} $typeDecl$ \dots $typeDecl$ \\\\
|
lcp@104
|
57 |
$typeDecl$ &=& $name${\tt,} \dots{\tt,} $name$ $k$
|
lcp@104
|
58 |
[{\tt(} $infix$ {\tt)}] \\\\
|
lcp@104
|
59 |
$infix$ &=& \ttindex{infixl} $k$ ~~$|$~~ \ttindex{infixr} $k$ \\\\
|
lcp@104
|
60 |
$arities$ &=& \ttindex{arities} $arityDecl$ \dots $arityDecl$ \\\\
|
lcp@104
|
61 |
$arityDecl$ &=& $name${\tt,} \dots{\tt,} $name$ {\tt::} $arity$ \\\\
|
lcp@104
|
62 |
$arity$ &=& [{\tt(} $sort${\tt,} \dots{\tt,} $sort$ {\tt)}] $id$ \\\\
|
lcp@104
|
63 |
$consts$ &=& \ttindex{consts} $constDecl$ \dots $constDecl$ \\\\
|
lcp@104
|
64 |
$constDecl$ &=& $name@1${\tt,} \dots{\tt,} $name@n$ {\tt::} $string$
|
lcp@104
|
65 |
[{\tt(} $mixfix$ {\tt)}] \\\\
|
lcp@104
|
66 |
$mixfix$ &=& $string$
|
lcp@104
|
67 |
[ [\quad{\tt[} $k@1${\tt,} \dots{\tt,} $k@n$ {\tt]}\quad] $k$]\\
|
lcp@104
|
68 |
&$|$& $infix$ \\
|
lcp@104
|
69 |
&$|$& \ttindex{binder} $string$ $k$\\\\
|
lcp@104
|
70 |
$rules$ &=& \ttindex{rules} $rule$ \dots $rule$ \\\\
|
lcp@104
|
71 |
$rule$ &=& $id$ $string$ \\\\
|
lcp@104
|
72 |
$ml$ &=& \ttindex{ML} $text$
|
lcp@104
|
73 |
\end{tabular}
|
lcp@104
|
74 |
\end{center}
|
lcp@104
|
75 |
\caption{Theory Syntax}
|
lcp@104
|
76 |
\label{TheorySyntax}
|
lcp@104
|
77 |
\end{figure}
|
lcp@104
|
78 |
|
lcp@104
|
79 |
The different parts of a theory definition are interpreted as follows:
|
clasohm@138
|
80 |
\begin{description}
|
clasohm@138
|
81 |
\item[$theoryDef$] A theory has a name $id$ and is an
|
clasohm@138
|
82 |
extension of the union of theories $id@1$ \dots $id@n$ with new
|
clasohm@138
|
83 |
classes, types, constants, syntax and axioms. The basic theory, which
|
clasohm@138
|
84 |
contains only the meta-logic, is called {\tt Pure}.
|
clasohm@138
|
85 |
|
clasohm@138
|
86 |
If $name@i$ is a string the theory $name@i$ is {\em not} used in building
|
clasohm@138
|
87 |
the base of theory $id$. The reason for using strings in $theoryDef$ is that
|
clasohm@138
|
88 |
many theories use objects created in a \ML-file that does not belong to a
|
clasohm@138
|
89 |
theory itself. Because $name@1$ \dots $name@n$ are loaded automatically a
|
clasohm@138
|
90 |
string can be used to specify a file that is needed as a series of
|
clasohm@138
|
91 |
\ML{}-declarations but not as a parent for theory $id$. See
|
clasohm@138
|
92 |
Chapter~\ref{LoadingTheories} for details.
|
lcp@104
|
93 |
\item[$class$] The new class $id$ is declared as a subclass of existing
|
lcp@104
|
94 |
classes $id@1$ \dots $id@n$. This rules out cyclic class structures.
|
lcp@104
|
95 |
Isabelle automatically computes the transitive closure of subclass
|
lcp@104
|
96 |
hierarchies. Hence it is not necessary to declare $c@1 < c@3$ in addition
|
lcp@104
|
97 |
to $c@1 < c@2$ and $c@2 < c@3$.
|
lcp@104
|
98 |
\item[$default$] introduces $sort$ as the new default sort for type
|
lcp@104
|
99 |
variables. Unconstrained type variables in an input string are
|
lcp@104
|
100 |
automatically constrained by $sort$; this does not apply to type variables
|
lcp@104
|
101 |
created internally during type inference. If omitted,
|
lcp@104
|
102 |
the default sort is the same as in the parent theory.
|
lcp@104
|
103 |
\item[$sort$] is a finite set $id@1$ \dots $id@n$ of classes; a single class
|
lcp@104
|
104 |
$id$ abbreviates the singleton set {\tt\{}$id${\tt\}}.
|
lcp@104
|
105 |
\item[$name$] is either an alphanumeric identifier or an arbitrary string.
|
lcp@104
|
106 |
\item[$typeDecl$] Each $name$ is declared as a new type constructor with
|
lcp@104
|
107 |
$k$ arguments. Only binary type constructors can have infix status and
|
lcp@104
|
108 |
symbolic names ($string$).
|
lcp@104
|
109 |
\item[$infix$] declares a type or constant to be an infix operator of
|
lcp@104
|
110 |
precedence $k$ associating to the left ({\tt infixl}) or right ({\tt
|
lcp@104
|
111 |
infixr}).
|
lcp@104
|
112 |
\item[$arityDecl$] Each existing type constructor $name@1$ \dots $name@n$
|
lcp@104
|
113 |
is given the additional arity $arity$.
|
lcp@104
|
114 |
\item[$constDecl$] The new constants $name@1$ \dots $name@n$ are declared to
|
lcp@104
|
115 |
be of type $string$. For display purposes they can be annotated with
|
lcp@104
|
116 |
$mixfix$ declarations.
|
lcp@104
|
117 |
\item[$mixfix$] $string$ is a mixfix template of the form {\tt"}\dots{\tt\_}
|
lcp@104
|
118 |
\dots{\tt\_} \dots{\tt"} where the $i$-th underscore indicates the position
|
lcp@104
|
119 |
where the $i$-th argument should go, $k@i$ is the minimum precedence of
|
lcp@104
|
120 |
the $i$-th argument, and $k$ the precedence of the construct. The list
|
lcp@104
|
121 |
\hbox{\tt[$k@1$, \dots, $k@n$]} is optional.
|
lcp@104
|
122 |
|
lcp@104
|
123 |
Binary constants can be given infix status.
|
lcp@104
|
124 |
|
lcp@104
|
125 |
A constant $f$ {\tt::} $(\tau@1\To\tau@2)\To\tau@3$ can be given {\em
|
lcp@104
|
126 |
binder} status: {\tt binder} $Q$ $p$ causes $Q\,x.F(x)$ to be treated
|
lcp@104
|
127 |
like $f(F)$; $p$ is the precedence of the construct.
|
lcp@104
|
128 |
\item[$rule$] A rule consists of a name $id$ and a formula $string$. Rule
|
lcp@104
|
129 |
names must be distinct.
|
lcp@104
|
130 |
\item[$ml$] This final part of a theory consists of ML code,
|
lcp@104
|
131 |
typically for parse and print translations.
|
lcp@104
|
132 |
\end{description}
|
lcp@104
|
133 |
The $mixfix$ and $ml$ sections are explained in more detail in the {\it
|
lcp@104
|
134 |
Defining Logics} chapter of the {\it Logics} manual.
|
lcp@104
|
135 |
|
clasohm@138
|
136 |
\section{Loading Theories}
|
clasohm@138
|
137 |
\label{LoadingTheories}
|
clasohm@138
|
138 |
\subsection{Reading a new theory}
|
clasohm@138
|
139 |
|
lcp@104
|
140 |
\begin{ttbox}
|
lcp@104
|
141 |
use_thy: string -> unit
|
lcp@104
|
142 |
\end{ttbox}
|
clasohm@138
|
143 |
|
lcp@104
|
144 |
Each theory definition must reside in a separate file. Let the file {\it
|
clasohm@138
|
145 |
tf}{\tt.thy} contain the definition of a theory called $TF$ with parent
|
clasohm@138
|
146 |
theories $TB@1$ \dots $TB@n$. Calling \ttindexbold{use_thy}~{\tt"}{\it
|
clasohm@138
|
147 |
TF\/}{\tt"} reads file {\it tf}{\tt.thy}, writes an intermediate {\ML}-file
|
clasohm@138
|
148 |
{\tt.}{\it tf}{\tt.thy.ML}, and reads the latter file. Any of the parent
|
clasohm@138
|
149 |
theories that have not been loaded yet are read now by recursive {\tt use_thy}
|
clasohm@138
|
150 |
calls until either an already loaded theory or {\tt Pure} is reached.
|
clasohm@138
|
151 |
Therefore one can read a complete logic by just one {\tt use_thy} call if all
|
clasohm@138
|
152 |
theories are linked appropriatly. Afterwards an {\ML} structure~$TF$
|
clasohm@138
|
153 |
containing a component {\tt thy} for the new theory and components $r@1$ \dots
|
clasohm@138
|
154 |
$r@n$ for the rules is declared; it also contains the definitions of the {\tt
|
clasohm@138
|
155 |
ML} section if any. (Normally {\tt.}{\it tf}{\tt.thy.ML} is deleted now if
|
clasohm@138
|
156 |
there have occured no errors. In case one wants to have a look at it,
|
clasohm@138
|
157 |
{\tt delete_tmpfiles := false} can be set before calling {\tt use_thy}.)
|
clasohm@138
|
158 |
Finally the file {\it tf}{\tt.ML} is read, if it exists; this file normally
|
clasohm@138
|
159 |
contains proofs involving the new theory.
|
clasohm@138
|
160 |
|
clasohm@138
|
161 |
|
clasohm@138
|
162 |
\subsection{Filenames and paths}
|
clasohm@138
|
163 |
|
clasohm@138
|
164 |
The files the theory definition resides in must have the lower case name of
|
clasohm@138
|
165 |
the theory with ".thy" or ".ML" appended. On the other hand {\tt use_thy}'s
|
clasohm@138
|
166 |
parameter has to be the exact theory name. Optionally the name can be
|
clasohm@138
|
167 |
preceeded by a path to specify the directory where the files can be found. If
|
clasohm@138
|
168 |
no path is provided the reference variable {\tt loadpath} is used which
|
clasohm@138
|
169 |
contains a list of paths that are searched in the given order. After the
|
clasohm@138
|
170 |
".thy"-file for a theory has been found the same path is used to locate the
|
clasohm@138
|
171 |
(optional) ".ML"-file. (You might note that it is also possible to only
|
clasohm@138
|
172 |
provide a ".ML"- but no ".thy"-file. In this case a \ML{} structure with the
|
clasohm@138
|
173 |
theory's name has to be created in the ".ML" file. If both the ".thy"-file
|
clasohm@138
|
174 |
and a structure declaration in the ".ML"-file exist the declaration in the
|
clasohm@138
|
175 |
latter file is used. See {\tt ZF/ex/llist.ML} for an example.)
|
clasohm@138
|
176 |
|
clasohm@138
|
177 |
|
clasohm@138
|
178 |
\subsection{Reloading a theory}
|
clasohm@138
|
179 |
|
clasohm@138
|
180 |
{\tt use_thy} keeps track of all loaded theories and stores information about
|
clasohm@138
|
181 |
their files. If it finds that the theory to be loaded was already read before
|
clasohm@138
|
182 |
the following happens: First the theory's files are searched at the place
|
clasohm@138
|
183 |
they were located at the last time they were read. If they are found their
|
clasohm@138
|
184 |
time of last modification is compared to the internal data and {\tt use_thy}
|
clasohm@138
|
185 |
stops if they are equal. In case the files have been moved, {\tt use_thy}
|
clasohm@138
|
186 |
searches them the same way as a new theory would be searched for. After all
|
clasohm@138
|
187 |
these tests have been passed the theory is reloaded and all theories that
|
clasohm@138
|
188 |
depend on it (i.e. that have its name in their $theoryDef$) are marked as
|
clasohm@138
|
189 |
out-of-date.
|
clasohm@138
|
190 |
|
clasohm@138
|
191 |
As changing a theory often makes it necessary to reload all theories that
|
clasohm@138
|
192 |
(indirectly) depend on it, {\tt update} should be used instead of {\tt
|
clasohm@138
|
193 |
use_thy} to read a modified theory. This function reloads all changed
|
clasohm@138
|
194 |
theories and their descendants in the correct order.
|
clasohm@138
|
195 |
|
clasohm@138
|
196 |
|
clasohm@138
|
197 |
\subsection{Pseudo theories}
|
clasohm@138
|
198 |
|
clasohm@138
|
199 |
There is a problem with {\tt update}: objects created in \ML-files that do not
|
clasohm@138
|
200 |
belong to a theory (see explanation of $theoryDef$ in \ref{DefiningTheories}).
|
clasohm@138
|
201 |
These files are read manually between {\tt use_thy} calls and define objects
|
clasohm@138
|
202 |
used in different theories. As {\tt update} only knows about the
|
clasohm@138
|
203 |
theories there still exist objects with references to the old theory version
|
clasohm@138
|
204 |
after the new one has been read. This (most probably) will produce the fatal
|
clasohm@138
|
205 |
error
|
clasohm@138
|
206 |
\begin{center} \tt
|
clasohm@138
|
207 |
Attempt to merge different versions of theory: $T$
|
clasohm@138
|
208 |
\end{center}
|
clasohm@138
|
209 |
|
clasohm@138
|
210 |
Therefore there is a way to link theories and the $orphaned$ \ML-files. The
|
clasohm@138
|
211 |
link from a theory to a \ML-file has been mentioned in
|
clasohm@138
|
212 |
Chapter~\ref{DefiningTheories} (strings in $theoryDef$). But to make this
|
clasohm@138
|
213 |
work and to establish a link in the opposite direction we need to create a
|
clasohm@138
|
214 |
{\it pseudo theory}. Let's assume we have a \ML-file named {\tt orphan.ML} that
|
clasohm@138
|
215 |
depends on theory $A$ and itself is used in theory $B$. To link the three we
|
clasohm@138
|
216 |
have to create the file {\tt orphan.thy} containing the line
|
clasohm@138
|
217 |
\begin{ttbox}
|
clasohm@138
|
218 |
orphan = A
|
clasohm@138
|
219 |
\end{ttbox}
|
clasohm@138
|
220 |
and add {\tt "orphan"} to theory $B$'s $theoryDef$. Creating {\tt orphan.thy}
|
clasohm@138
|
221 |
is necessary because of two reasons: First it enables automatic loading of
|
clasohm@138
|
222 |
$orphan$'s parents and second it creates the \ML{}-object {\tt orphan} that
|
clasohm@138
|
223 |
is needed by {\tt use_thy} (though it is not added to the base of theory $B$).
|
clasohm@138
|
224 |
If {\tt orphan.ML} depended on no theory then {\tt Pure} would have been used
|
clasohm@138
|
225 |
instead of {\tt A}.
|
clasohm@138
|
226 |
|
clasohm@138
|
227 |
For an extensive example of how this technique can be used to link over 30
|
clasohm@138
|
228 |
files and read them by just two {\tt use_thy} calls have a look at the ZF logic.
|
clasohm@138
|
229 |
|
clasohm@138
|
230 |
|
clasohm@138
|
231 |
\subsection{Removing a theory}
|
clasohm@138
|
232 |
|
clasohm@138
|
233 |
If a previously read file is removed the {\tt update} function will keep
|
clasohm@138
|
234 |
on complaining about a missing file. The theory is not automatically removed
|
clasohm@138
|
235 |
from the internal list to preserve the links to other theories in case one
|
clasohm@138
|
236 |
forgot to adjust the {\tt loadpath} after moving a file. To manually remove a
|
clasohm@138
|
237 |
theory use {\tt unlink_thy}.
|
clasohm@138
|
238 |
|
clasohm@138
|
239 |
|
clasohm@138
|
240 |
\subsection{Using Poly/\ML}
|
clasohm@138
|
241 |
|
clasohm@138
|
242 |
As the functions for reading theories depend on reference variables one has to
|
clasohm@138
|
243 |
take into consideration the way Poly/\ML{} handles them. They are only saved
|
clasohm@138
|
244 |
together with the state if they were declared in the current database. E.g.
|
clasohm@138
|
245 |
changes made to a reference variable declared in the $Pure$ database are $not$
|
clasohm@138
|
246 |
saved if made while using a child database. Therefore a new {\tt Readthy}
|
clasohm@138
|
247 |
structure has to be declared by
|
clasohm@138
|
248 |
\begin{ttbox}
|
clasohm@138
|
249 |
structure Readthy = ReadthyFUN (structure ThySyn = ThySyn);
|
clasohm@138
|
250 |
open Readthy;
|
clasohm@138
|
251 |
\end{ttbox}
|
clasohm@138
|
252 |
in every newly created database. This is not necessary if the database is
|
clasohm@138
|
253 |
created by copying an existent one.
|
clasohm@138
|
254 |
|
clasohm@138
|
255 |
The above declarations are contained in the $Pure$ database, so one could
|
clasohm@138
|
256 |
simply use e.g. {\tt use_thy} if saving of the reference variables is not
|
clasohm@138
|
257 |
needed. Also Standard ML of New Jersey does not have this behaviour.
|
lcp@104
|
258 |
|
lcp@104
|
259 |
|
lcp@104
|
260 |
\section{Basic operations on theories}
|
lcp@104
|
261 |
\subsection{Extracting an axiom from a theory}
|
lcp@104
|
262 |
\index{theories!extracting axioms|bold}\index{axioms}
|
lcp@104
|
263 |
\begin{ttbox}
|
lcp@104
|
264 |
get_axiom: theory -> string -> thm
|
lcp@104
|
265 |
assume_ax: theory -> string -> thm
|
lcp@104
|
266 |
\end{ttbox}
|
lcp@104
|
267 |
\begin{description}
|
lcp@104
|
268 |
\item[\ttindexbold{get_axiom} $thy$ $name$]
|
lcp@104
|
269 |
returns an axiom with the given $name$ from $thy$, raising exception
|
lcp@104
|
270 |
\ttindex{THEORY} if none exists. Merging theories can cause several axioms
|
lcp@104
|
271 |
to have the same name; {\tt get_axiom} returns an arbitrary one.
|
lcp@104
|
272 |
|
lcp@104
|
273 |
\item[\ttindexbold{assume_ax} $thy$ $formula$]
|
lcp@104
|
274 |
reads the {\it formula} using the syntax of $thy$, following the same
|
lcp@104
|
275 |
conventions as axioms in a theory definition. You can thus pretend that
|
lcp@104
|
276 |
{\it formula} is an axiom; in fact, {\tt assume_ax} returns an assumption.
|
lcp@104
|
277 |
You can use the resulting theorem like an axiom. Note that
|
lcp@104
|
278 |
\ttindex{result} complains about additional assumptions, but
|
lcp@104
|
279 |
\ttindex{uresult} does not.
|
lcp@104
|
280 |
|
lcp@104
|
281 |
For example, if {\it formula} is
|
lcp@104
|
282 |
\hbox{\tt a=b ==> b=a} then the resulting theorem might have the form
|
lcp@104
|
283 |
\hbox{\tt\frenchspacing ?a=?b ==> ?b=?a [!!a b. a=b ==> b=a]}
|
lcp@104
|
284 |
\end{description}
|
lcp@104
|
285 |
|
lcp@104
|
286 |
\subsection{Building a theory}
|
lcp@104
|
287 |
\label{BuildingATheory}
|
lcp@104
|
288 |
\index{theories!constructing|bold}
|
lcp@104
|
289 |
\begin{ttbox}
|
lcp@104
|
290 |
pure_thy: theory
|
lcp@104
|
291 |
merge_theories: theory * theory -> theory
|
lcp@104
|
292 |
extend_theory: theory -> string
|
lcp@104
|
293 |
-> (class * class list) list
|
lcp@104
|
294 |
* sort
|
lcp@104
|
295 |
* (string list * int)list
|
lcp@104
|
296 |
* (string list * (sort list * class))list
|
lcp@104
|
297 |
* (string list * string)list * sext option
|
lcp@104
|
298 |
-> (string*string)list -> theory
|
lcp@104
|
299 |
\end{ttbox}
|
lcp@104
|
300 |
Type \ttindex{class} is a synonym for {\tt string}; type \ttindex{sort} is
|
lcp@104
|
301 |
a synonym for \hbox{\tt class list}.
|
lcp@104
|
302 |
\begin{description}
|
lcp@104
|
303 |
\item[\ttindexbold{pure_thy}] contains just the types, constants, and syntax
|
lcp@104
|
304 |
of the meta-logic. There are no axioms: meta-level inferences are carried
|
lcp@104
|
305 |
out by \ML\ functions.
|
lcp@104
|
306 |
\item[\ttindexbold{merge_theories} ($thy@1$, $thy@2$)] merges the two
|
lcp@104
|
307 |
theories $thy@1$ and $thy@2$. The resulting theory contains all types,
|
lcp@104
|
308 |
constants and axioms of the constituent theories; its default sort is the
|
lcp@104
|
309 |
union of the default sorts of the constituent theories.
|
lcp@104
|
310 |
\item [\ttindexbold{extend_theory} $thy$ {\tt"}$T${\tt"}
|
lcp@104
|
311 |
($classes$, $default$, $types$, $arities$, $consts$, $sextopt$) $rules$]
|
lcp@104
|
312 |
\hfill\break %%% include if line is just too short
|
lcp@104
|
313 |
is the \ML-equivalent of the following theory definition:
|
lcp@104
|
314 |
\begin{ttbox}
|
lcp@104
|
315 |
\(T\) = \(thy\) +
|
lcp@104
|
316 |
classes \(c\) < \(c@1\),\(\dots\),\(c@m\)
|
lcp@104
|
317 |
\dots
|
lcp@104
|
318 |
default {\(d@1,\dots,d@r\)}
|
lcp@104
|
319 |
types \(tycon@1\),\dots,\(tycon@i\) \(n\)
|
lcp@104
|
320 |
\dots
|
lcp@104
|
321 |
arities \(tycon@1'\),\dots,\(tycon@j'\) :: (\(s@1\),\dots,\(s@n\))\(c\)
|
lcp@104
|
322 |
\dots
|
lcp@104
|
323 |
consts \(b@1\),\dots,\(b@k\) :: \(\tau\)
|
lcp@104
|
324 |
\dots
|
lcp@104
|
325 |
rules \(name\) \(rule\)
|
lcp@104
|
326 |
\dots
|
lcp@104
|
327 |
end
|
lcp@104
|
328 |
\end{ttbox}
|
lcp@104
|
329 |
where
|
lcp@104
|
330 |
\begin{tabular}[t]{l@{~=~}l}
|
lcp@104
|
331 |
$classes$ & \tt[("$c$",["$c@1$",\dots,"$c@m$"]),\dots] \\
|
lcp@104
|
332 |
$default$ & \tt["$d@1$",\dots,"$d@r$"]\\
|
lcp@104
|
333 |
$types$ & \tt[([$tycon@1$,\dots,$tycon@i$], $n$),\dots] \\
|
lcp@104
|
334 |
$arities$ & \tt[([$tycon'@1$,\dots,$tycon'@j$], ([$s@1$,\dots,$s@n$],$c$)),\dots]
|
lcp@104
|
335 |
\\
|
lcp@104
|
336 |
$consts$ & \tt[([$b@1$,\dots,$b@k$],$\tau$),\dots] \\
|
lcp@104
|
337 |
$rules$ & \tt[("$name$",$rule$),\dots]
|
lcp@104
|
338 |
\end{tabular}
|
lcp@104
|
339 |
|
lcp@104
|
340 |
If theories are defined as in \S\ref{DefiningTheories}, new syntax is added
|
lcp@104
|
341 |
as mixfix annotations to constants. Using {\tt extend_theory}, new syntax can
|
lcp@104
|
342 |
be added via $sextopt$ which is either {\tt None}, or {\tt Some($sext$)}. The
|
lcp@104
|
343 |
latter case is not documented.
|
lcp@104
|
344 |
|
lcp@104
|
345 |
$T$ identifies the theory internally. When a theory is redeclared, say to
|
lcp@104
|
346 |
change an incorrect axiom, bindings to the old axiom may persist. Isabelle
|
lcp@104
|
347 |
ensures that the old and new theories are not involved in the same proof.
|
lcp@104
|
348 |
Attempting to combine different theories having the same name $T$ yields the
|
lcp@104
|
349 |
fatal error
|
lcp@104
|
350 |
\begin{center} \tt
|
lcp@104
|
351 |
Attempt to merge different versions of theory: $T$
|
lcp@104
|
352 |
\end{center}
|
lcp@104
|
353 |
\end{description}
|
lcp@104
|
354 |
|
lcp@104
|
355 |
|
lcp@104
|
356 |
\subsection{Inspecting a theory}
|
lcp@104
|
357 |
\index{theories!inspecting|bold}
|
lcp@104
|
358 |
\begin{ttbox}
|
lcp@104
|
359 |
print_theory : theory -> unit
|
lcp@104
|
360 |
axioms_of : theory -> (string*thm)list
|
lcp@104
|
361 |
parents_of : theory -> theory list
|
lcp@104
|
362 |
sign_of : theory -> Sign.sg
|
lcp@104
|
363 |
stamps_of_thy : theory -> string ref list
|
lcp@104
|
364 |
\end{ttbox}
|
lcp@104
|
365 |
These provide a simple means of viewing a theory's components.
|
lcp@104
|
366 |
Unfortunately, there is no direct connection between a theorem and its
|
lcp@104
|
367 |
theory.
|
lcp@104
|
368 |
\begin{description}
|
lcp@104
|
369 |
\item[\ttindexbold{print_theory} {\it thy}]
|
lcp@104
|
370 |
prints the theory {\it thy\/} at the terminal as a set of identifiers.
|
lcp@104
|
371 |
|
lcp@104
|
372 |
\item[\ttindexbold{axioms_of} $thy$]
|
lcp@104
|
373 |
returns the axioms of~$thy$ and its ancestors.
|
lcp@104
|
374 |
|
lcp@104
|
375 |
\item[\ttindexbold{parents_of} $thy$]
|
lcp@104
|
376 |
returns the parents of~$thy$. This list contains zero, one or two
|
lcp@104
|
377 |
elements, depending upon whether $thy$ is {\tt pure_thy},
|
lcp@104
|
378 |
\hbox{\tt extend_theory $thy$} or \hbox{\tt merge_theories ($thy@1$, $thy@2$)}.
|
lcp@104
|
379 |
|
lcp@104
|
380 |
\item[\ttindexbold{stamps_of_thy} $thy$]\index{signatures}
|
lcp@104
|
381 |
returns the stamps of the signature associated with~$thy$.
|
lcp@104
|
382 |
|
lcp@104
|
383 |
\item[\ttindexbold{sign_of} $thy$]
|
lcp@104
|
384 |
returns the signature associated with~$thy$. It is useful with functions
|
lcp@104
|
385 |
like {\tt read_instantiate_sg}, which take a signature as an argument.
|
lcp@104
|
386 |
\end{description}
|
lcp@104
|
387 |
|
lcp@104
|
388 |
|
lcp@104
|
389 |
\section{Terms}
|
lcp@104
|
390 |
\index{terms|bold}
|
lcp@104
|
391 |
Terms belong to the \ML{} type \ttindexbold{term}, which is a concrete datatype
|
lcp@104
|
392 |
with six constructors: there are six kinds of term.
|
lcp@104
|
393 |
\begin{ttbox}
|
lcp@104
|
394 |
type indexname = string * int;
|
lcp@104
|
395 |
infix 9 $;
|
lcp@104
|
396 |
datatype term = Const of string * typ
|
lcp@104
|
397 |
| Free of string * typ
|
lcp@104
|
398 |
| Var of indexname * typ
|
lcp@104
|
399 |
| Bound of int
|
lcp@104
|
400 |
| Abs of string * typ * term
|
lcp@104
|
401 |
| op $ of term * term;
|
lcp@104
|
402 |
\end{ttbox}
|
lcp@104
|
403 |
\begin{description}
|
lcp@104
|
404 |
\item[\ttindexbold{Const}($a$, $T$)]
|
lcp@104
|
405 |
is the {\bf constant} with name~$a$ and type~$T$. Constants include
|
lcp@104
|
406 |
connectives like $\land$ and $\forall$ (logical constants), as well as
|
lcp@104
|
407 |
constants like~0 and~$Suc$. Other constants may be required to define the
|
lcp@104
|
408 |
concrete syntax of a logic.
|
lcp@104
|
409 |
|
lcp@104
|
410 |
\item[\ttindexbold{Free}($a$, $T$)]
|
lcp@104
|
411 |
is the {\bf free variable} with name~$a$ and type~$T$.
|
lcp@104
|
412 |
|
lcp@104
|
413 |
\item[\ttindexbold{Var}($v$, $T$)]
|
lcp@104
|
414 |
is the {\bf scheme variable} with indexname~$v$ and type~$T$. An
|
lcp@104
|
415 |
\ttindexbold{indexname} is a string paired with a non-negative index, or
|
lcp@104
|
416 |
subscript; a term's scheme variables can be systematically renamed by
|
lcp@104
|
417 |
incrementing their subscripts. Scheme variables are essentially free
|
lcp@104
|
418 |
variables, but may be instantiated during unification.
|
lcp@104
|
419 |
|
lcp@104
|
420 |
\item[\ttindexbold{Bound} $i$]
|
lcp@104
|
421 |
is the {\bf bound variable} with de Bruijn index~$i$, which counts the
|
lcp@104
|
422 |
number of lambdas, starting from zero, between a variable's occurrence and
|
lcp@104
|
423 |
its binding. The representation prevents capture of variables. For more
|
lcp@104
|
424 |
information see de Bruijn \cite{debruijn72} or
|
lcp@104
|
425 |
Paulson~\cite[page~336]{paulson91}.
|
lcp@104
|
426 |
|
lcp@104
|
427 |
\item[\ttindexbold{Abs}($a$, $T$, $u$)]
|
lcp@104
|
428 |
is the {\bf abstraction} with body~$u$, and whose bound variable has
|
lcp@104
|
429 |
name~$a$ and type~$T$. The name is used only for parsing and printing; it
|
lcp@104
|
430 |
has no logical significance.
|
lcp@104
|
431 |
|
lcp@104
|
432 |
\item[\tt $t$ \$ $u$] \index{$@{\tt\$}|bold}
|
lcp@104
|
433 |
is the {\bf application} of~$t$ to~$u$.
|
lcp@104
|
434 |
\end{description}
|
lcp@104
|
435 |
Application is written as an infix operator in order to aid readability.
|
lcp@104
|
436 |
For example, here is an \ML{} pattern to recognize first-order formula of
|
lcp@104
|
437 |
the form~$A\imp B$, binding the subformulae to~$A$ and~$B$:
|
lcp@104
|
438 |
\begin{ttbox}
|
lcp@104
|
439 |
Const("Trueprop",_) $ (Const("op -->",_) $ A $ B)
|
lcp@104
|
440 |
\end{ttbox}
|
lcp@104
|
441 |
|
lcp@104
|
442 |
|
lcp@104
|
443 |
\section{Certified terms}
|
lcp@104
|
444 |
\index{terms!certified|bold}\index{signatures}
|
lcp@104
|
445 |
A term $t$ can be {\bf certified} under a signature to ensure that every
|
lcp@104
|
446 |
type in~$t$ is declared in the signature and every constant in~$t$ is
|
lcp@104
|
447 |
declared as a constant of the same type in the signature. It must be
|
lcp@104
|
448 |
well-typed and must not have any `loose' bound variable
|
lcp@104
|
449 |
references.\footnote{This concerns the internal representation of variable
|
lcp@104
|
450 |
binding using de Bruijn indexes.} Meta-rules such as {\tt forall_elim} take
|
lcp@104
|
451 |
certified terms as arguments.
|
lcp@104
|
452 |
|
lcp@104
|
453 |
Certified terms belong to the abstract type \ttindexbold{Sign.cterm}.
|
lcp@104
|
454 |
Elements of the type can only be created through the certification process.
|
lcp@104
|
455 |
In case of error, Isabelle raises exception~\ttindex{TERM}\@.
|
lcp@104
|
456 |
|
lcp@104
|
457 |
\subsection{Printing terms}
|
lcp@104
|
458 |
\index{printing!terms|bold}
|
lcp@104
|
459 |
\begin{ttbox}
|
lcp@104
|
460 |
Sign.string_of_cterm : Sign.cterm -> string
|
lcp@104
|
461 |
Sign.string_of_term : Sign.sg -> term -> string
|
lcp@104
|
462 |
\end{ttbox}
|
lcp@104
|
463 |
\begin{description}
|
lcp@104
|
464 |
\item[\ttindexbold{Sign.string_of_cterm} $ct$]
|
lcp@104
|
465 |
displays $ct$ as a string.
|
lcp@104
|
466 |
|
lcp@104
|
467 |
\item[\ttindexbold{Sign.string_of_term} $sign$ $t$]
|
lcp@104
|
468 |
displays $t$ as a string, using the syntax of~$sign$.
|
lcp@104
|
469 |
\end{description}
|
lcp@104
|
470 |
|
lcp@104
|
471 |
\subsection{Making and inspecting certified terms}
|
lcp@104
|
472 |
\begin{ttbox}
|
lcp@104
|
473 |
Sign.cterm_of : Sign.sg -> term -> Sign.cterm
|
lcp@104
|
474 |
Sign.read_cterm : Sign.sg -> string * typ -> Sign.cterm
|
lcp@104
|
475 |
Sign.rep_cterm : Sign.cterm -> \{T:typ, t:term,
|
lcp@104
|
476 |
sign: Sign.sg, maxidx:int\}
|
lcp@104
|
477 |
\end{ttbox}
|
lcp@104
|
478 |
\begin{description}
|
lcp@104
|
479 |
\item[\ttindexbold{Sign.cterm_of} $sign$ $t$] \index{signatures}
|
lcp@104
|
480 |
certifies $t$ with respect to signature~$sign$.
|
lcp@104
|
481 |
|
lcp@104
|
482 |
\item[\ttindexbold{Sign.read_cterm} $sign$ ($s$, $T$)]
|
lcp@104
|
483 |
reads the string~$s$ using the syntax of~$sign$, creating a certified term.
|
lcp@104
|
484 |
The term is checked to have type~$T$; this type also tells the parser what
|
lcp@104
|
485 |
kind of phrase to parse.
|
lcp@104
|
486 |
|
lcp@104
|
487 |
\item[\ttindexbold{Sign.rep_cterm} $ct$]
|
lcp@104
|
488 |
decomposes $ct$ as a record containing its type, the term itself, its
|
lcp@104
|
489 |
signature, and the maximum subscript of its unknowns. The type and maximum
|
lcp@104
|
490 |
subscript are computed during certification.
|
lcp@104
|
491 |
\end{description}
|
lcp@104
|
492 |
|
lcp@104
|
493 |
|
lcp@104
|
494 |
\section{Types}
|
lcp@104
|
495 |
\index{types|bold}
|
lcp@104
|
496 |
Types belong to the \ML{} type \ttindexbold{typ}, which is a concrete
|
lcp@104
|
497 |
datatype with three constructors. Types are classified by sorts, which are
|
lcp@104
|
498 |
lists of classes. A class is represented by a string.
|
lcp@104
|
499 |
\begin{ttbox}
|
lcp@104
|
500 |
type class = string;
|
lcp@104
|
501 |
type sort = class list;
|
lcp@104
|
502 |
|
lcp@104
|
503 |
datatype typ = Type of string * typ list
|
lcp@104
|
504 |
| TFree of string * sort
|
lcp@104
|
505 |
| TVar of indexname * sort;
|
lcp@104
|
506 |
|
lcp@104
|
507 |
infixr 5 -->;
|
lcp@104
|
508 |
fun S --> T = Type("fun",[S,T]);
|
lcp@104
|
509 |
\end{ttbox}
|
lcp@104
|
510 |
\begin{description}
|
lcp@104
|
511 |
\item[\ttindexbold{Type}($a$, $Ts$)]
|
lcp@104
|
512 |
applies the {\bf type constructor} named~$a$ to the type operands~$Ts$.
|
lcp@104
|
513 |
Type constructors include~\ttindexbold{fun}, the binary function space
|
lcp@104
|
514 |
constructor, as well as nullary type constructors such
|
lcp@104
|
515 |
as~\ttindexbold{prop}. Other type constructors may be introduced. In
|
lcp@104
|
516 |
expressions, but not in patterns, \hbox{\tt$S$-->$T$} is a convenient
|
lcp@104
|
517 |
shorthand for function types.
|
lcp@104
|
518 |
|
lcp@104
|
519 |
\item[\ttindexbold{TFree}($a$, $s$)]
|
lcp@104
|
520 |
is the {\bf free type variable} with name~$a$ and sort~$s$.
|
lcp@104
|
521 |
|
lcp@104
|
522 |
\item[\ttindexbold{TVar}($v$, $s$)]
|
lcp@104
|
523 |
is the {\bf scheme type variable} with indexname~$v$ and sort~$s$. Scheme
|
lcp@104
|
524 |
type variables are essentially free type variables, but may be instantiated
|
lcp@104
|
525 |
during unification.
|
lcp@104
|
526 |
\end{description}
|
lcp@104
|
527 |
|
lcp@104
|
528 |
|
lcp@104
|
529 |
\section{Certified types}
|
lcp@104
|
530 |
\index{types!certified|bold}
|
lcp@104
|
531 |
Certified types, which are analogous to certified terms, have type
|
lcp@104
|
532 |
\ttindexbold{Sign.ctyp}.
|
lcp@104
|
533 |
|
lcp@104
|
534 |
\subsection{Printing types}
|
lcp@104
|
535 |
\index{printing!types|bold}
|
lcp@104
|
536 |
\begin{ttbox}
|
lcp@104
|
537 |
Sign.string_of_ctyp : Sign.ctyp -> string
|
lcp@104
|
538 |
Sign.string_of_typ : Sign.sg -> typ -> string
|
lcp@104
|
539 |
\end{ttbox}
|
lcp@104
|
540 |
\begin{description}
|
lcp@104
|
541 |
\item[\ttindexbold{Sign.string_of_ctyp} $cT$]
|
lcp@104
|
542 |
displays $cT$ as a string.
|
lcp@104
|
543 |
|
lcp@104
|
544 |
\item[\ttindexbold{Sign.string_of_typ} $sign$ $T$]
|
lcp@104
|
545 |
displays $T$ as a string, using the syntax of~$sign$.
|
lcp@104
|
546 |
\end{description}
|
lcp@104
|
547 |
|
lcp@104
|
548 |
|
lcp@104
|
549 |
\subsection{Making and inspecting certified types}
|
lcp@104
|
550 |
\begin{ttbox}
|
lcp@104
|
551 |
Sign.ctyp_of : Sign.sg -> typ -> Sign.ctyp
|
lcp@104
|
552 |
Sign.rep_ctyp : Sign.ctyp -> \{T: typ, sign: Sign.sg\}
|
lcp@104
|
553 |
\end{ttbox}
|
lcp@104
|
554 |
\begin{description}
|
lcp@104
|
555 |
\item[\ttindexbold{Sign.ctyp_of} $sign$ $T$] \index{signatures}
|
lcp@104
|
556 |
certifies $T$ with respect to signature~$sign$.
|
lcp@104
|
557 |
|
lcp@104
|
558 |
\item[\ttindexbold{Sign.rep_ctyp} $cT$]
|
lcp@104
|
559 |
decomposes $cT$ as a record containing the type itself and its signature.
|
lcp@104
|
560 |
\end{description}
|
lcp@104
|
561 |
|
lcp@104
|
562 |
\index{theories|)}
|