lcp@104
|
1 |
%% $Id$
|
wenzelm@145
|
2 |
|
lcp@104
|
3 |
\chapter{Theories, Terms and Types} \label{theories}
|
lcp@104
|
4 |
\index{theories|(}\index{signatures|bold}
|
nipkow@478
|
5 |
\index{reading!axioms|see{{\tt assume_ax}}}
|
lcp@104
|
6 |
Theories organize the syntax, declarations and axioms of a mathematical
|
lcp@104
|
7 |
development. They are built, starting from the Pure theory, by extending
|
lcp@324
|
8 |
and merging existing theories. They have the \ML\ type \mltydx{theory}.
|
lcp@324
|
9 |
Theory operations signal errors by raising exception \xdx{THEORY},
|
lcp@104
|
10 |
returning a message and a list of theories.
|
lcp@104
|
11 |
|
lcp@104
|
12 |
Signatures, which contain information about sorts, types, constants and
|
lcp@332
|
13 |
syntax, have the \ML\ type~\mltydx{Sign.sg}. For identification, each
|
wenzelm@864
|
14 |
signature carries a unique list of \bfindex{stamps}, which are \ML\
|
lcp@324
|
15 |
references to strings. The strings serve as human-readable names; the
|
lcp@104
|
16 |
references serve as unique identifiers. Each primitive signature has a
|
lcp@104
|
17 |
single stamp. When two signatures are merged, their lists of stamps are
|
lcp@104
|
18 |
also merged. Every theory carries a unique signature.
|
lcp@104
|
19 |
|
lcp@104
|
20 |
Terms and types are the underlying representation of logical syntax. Their
|
nipkow@275
|
21 |
\ML\ definitions are irrelevant to naive Isabelle users. Programmers who
|
nipkow@275
|
22 |
wish to extend Isabelle may need to know such details, say to code a tactic
|
nipkow@275
|
23 |
that looks for subgoals of a particular form. Terms and types may be
|
lcp@104
|
24 |
`certified' to be well-formed with respect to a given signature.
|
lcp@104
|
25 |
|
lcp@324
|
26 |
|
lcp@324
|
27 |
\section{Defining theories}\label{sec:ref-defining-theories}
|
lcp@104
|
28 |
|
wenzelm@864
|
29 |
Theories are usually defined using theory definition files (which have a name
|
wenzelm@864
|
30 |
suffix {\tt .thy}). There is also a low level interface provided by certain
|
wenzelm@864
|
31 |
\ML{} functions (see \S\ref{BuildingATheory}).
|
wenzelm@864
|
32 |
Appendix~\ref{app:TheorySyntax} presents the concrete syntax for theory
|
wenzelm@864
|
33 |
definitions; here is an explanation of the constituent parts:
|
wenzelm@864
|
34 |
\begin{description}
|
wenzelm@864
|
35 |
\item[{\it theoryDef}]
|
lcp@324
|
36 |
is the full definition. The new theory is called $id$. It is the union
|
lcp@324
|
37 |
of the named {\bf parent theories}\indexbold{theories!parent}, possibly
|
lcp@324
|
38 |
extended with new classes, etc. The basic theory, which contains only
|
lcp@324
|
39 |
the meta-logic, is called \thydx{Pure}.
|
clasohm@138
|
40 |
|
wenzelm@864
|
41 |
Normally each {\it name\/} is an identifier, the name of the parent theory.
|
wenzelm@864
|
42 |
Quoted strings can be used to document additional file dependencies; see
|
nipkow@275
|
43 |
\S\ref{LoadingTheories} for details.
|
lcp@324
|
44 |
|
wenzelm@864
|
45 |
\item[$classes$]
|
wenzelm@864
|
46 |
is a series of class declarations. Declaring {\tt$id$ < $id@1$ \dots\
|
lcp@324
|
47 |
$id@n$} makes $id$ a subclass of the existing classes $id@1\dots
|
lcp@324
|
48 |
id@n$. This rules out cyclic class structures. Isabelle automatically
|
lcp@324
|
49 |
computes the transitive closure of subclass hierarchies; it is not
|
lcp@324
|
50 |
necessary to declare {\tt c < e} in addition to {\tt c < d} and {\tt d <
|
lcp@324
|
51 |
e}.
|
lcp@324
|
52 |
|
wenzelm@864
|
53 |
\item[$default$]
|
wenzelm@864
|
54 |
introduces $sort$ as the new default sort for type variables. This applies
|
wenzelm@864
|
55 |
to unconstrained type variables in an input string but not to type
|
wenzelm@864
|
56 |
variables created internally. If omitted, the default sort is the listwise
|
wenzelm@864
|
57 |
union of the default sorts of the parent theories (i.e.\ their logical
|
wenzelm@864
|
58 |
intersection).
|
lcp@324
|
59 |
|
wenzelm@864
|
60 |
\item[$sort$]
|
lcp@324
|
61 |
is a finite set of classes. A single class $id$ abbreviates the singleton
|
lcp@324
|
62 |
set {\tt\{}$id${\tt\}}.
|
lcp@324
|
63 |
|
wenzelm@864
|
64 |
\item[$types$]
|
lcp@324
|
65 |
is a series of type declarations. Each declares a new type constructor
|
lcp@324
|
66 |
or type synonym. An $n$-place type constructor is specified by
|
lcp@324
|
67 |
$(\alpha@1,\dots,\alpha@n)name$, where the type variables serve only to
|
lcp@324
|
68 |
indicate the number~$n$.
|
lcp@324
|
69 |
|
lcp@332
|
70 |
A {\bf type synonym}\indexbold{type synonyms} is an abbreviation
|
clasohm@1387
|
71 |
$(\alpha@1,\dots,\alpha@n)name = \tau$, where $name$ and $\tau$ can
|
clasohm@1387
|
72 |
be strings.
|
wenzelm@864
|
73 |
|
wenzelm@864
|
74 |
\item[$infix$]
|
lcp@324
|
75 |
declares a type or constant to be an infix operator of priority $nat$
|
wenzelm@864
|
76 |
associating to the left ({\tt infixl}) or right ({\tt infixr}). Only
|
wenzelm@864
|
77 |
2-place type constructors can have infix status; an example is {\tt
|
wenzelm@864
|
78 |
('a,'b)~"*"~(infixr~20)}, which expresses binary product types.
|
lcp@324
|
79 |
|
wenzelm@864
|
80 |
\item[$arities$]
|
lcp@324
|
81 |
is a series of arity declarations. Each assigns arities to type
|
lcp@324
|
82 |
constructors. The $name$ must be an existing type constructor, which is
|
nipkow@273
|
83 |
given the additional arity $arity$.
|
lcp@324
|
84 |
|
wenzelm@864
|
85 |
\item[$constDecl$]
|
lcp@324
|
86 |
is a series of constant declarations. Each new constant $name$ is given
|
clasohm@1380
|
87 |
the specified type. The optional $mixfix$ annotations may
|
wenzelm@864
|
88 |
attach concrete syntax to the constant. A variant of {\tt consts} is the
|
wenzelm@864
|
89 |
{\tt syntax} section\index{*syntax section}, which adds just syntax without
|
wenzelm@864
|
90 |
declaring logical constants.
|
lcp@324
|
91 |
|
lcp@324
|
92 |
\item[$mixfix$] \index{mixfix declarations}
|
lcp@324
|
93 |
annotations can take three forms:
|
nipkow@273
|
94 |
\begin{itemize}
|
nipkow@273
|
95 |
\item A mixfix template given as a $string$ of the form
|
nipkow@273
|
96 |
{\tt"}\dots{\tt\_}\dots{\tt\_}\dots{\tt"} where the $i$-th underscore
|
lcp@324
|
97 |
indicates the position where the $i$-th argument should go. The list
|
lcp@324
|
98 |
of numbers gives the priority of each argument. The final number gives
|
lcp@324
|
99 |
the priority of the whole construct.
|
lcp@104
|
100 |
|
lcp@324
|
101 |
\item A constant $f$ of type $\tau@1\To(\tau@2\To\tau)$ can be given {\bf
|
lcp@324
|
102 |
infix} status.
|
lcp@104
|
103 |
|
lcp@324
|
104 |
\item A constant $f$ of type $(\tau@1\To\tau@2)\To\tau$ can be given {\bf
|
lcp@324
|
105 |
binder} status. The declaration {\tt binder} $\cal Q$ $p$ causes
|
lcp@286
|
106 |
${\cal Q}\,x.F(x)$ to be treated
|
lcp@286
|
107 |
like $f(F)$, where $p$ is the priority.
|
nipkow@273
|
108 |
\end{itemize}
|
lcp@324
|
109 |
|
wenzelm@864
|
110 |
\item[$trans$]
|
wenzelm@864
|
111 |
specifies syntactic translation rules (macros). There are three forms:
|
wenzelm@864
|
112 |
parse rules ({\tt =>}), print rules ({\tt <=}), and parse/print rules ({\tt
|
wenzelm@864
|
113 |
==}).
|
lcp@324
|
114 |
|
nipkow@1650
|
115 |
\item[$rules$]
|
wenzelm@864
|
116 |
is a series of rule declarations. Each has a name $id$ and the formula is
|
wenzelm@864
|
117 |
given by the $string$. Rule names must be distinct within any single
|
wenzelm@864
|
118 |
theory file.
|
lcp@324
|
119 |
|
nipkow@1650
|
120 |
\item[$defs$]
|
nipkow@1650
|
121 |
is a series of definitions. Just like $rules$, except that every $string$
|
nipkow@1650
|
122 |
must be a definition.
|
nipkow@1650
|
123 |
|
nipkow@1650
|
124 |
\item[$constdefs$] combines the declaration of constants and their
|
nipkow@1650
|
125 |
definition. The first $string$ is the type, the second the definition.
|
nipkow@1650
|
126 |
|
paulson@1846
|
127 |
\item[$oracle$] links the theory to a trusted external reasoner. It is
|
paulson@1846
|
128 |
allowed to create theorems, but each theorem carries a proof object
|
paulson@1846
|
129 |
describing the oracle invocation. See \S\ref{sec:oracles} for details.
|
paulson@1846
|
130 |
|
lcp@324
|
131 |
\item[$ml$] \index{*ML section}
|
wenzelm@864
|
132 |
consists of \ML\ code, typically for parse and print translation functions.
|
lcp@104
|
133 |
\end{description}
|
lcp@324
|
134 |
%
|
wenzelm@864
|
135 |
Chapters~\ref{Defining-Logics} and \ref{chap:syntax} explain mixfix
|
wenzelm@864
|
136 |
declarations, translation rules and the {\tt ML} section in more detail.
|
wenzelm@145
|
137 |
|
wenzelm@145
|
138 |
|
nipkow@275
|
139 |
\subsection{*Classes and arities}
|
lcp@324
|
140 |
\index{classes!context conditions}\index{arities!context conditions}
|
wenzelm@145
|
141 |
|
lcp@286
|
142 |
In order to guarantee principal types~\cite{nipkow-prehofer},
|
lcp@324
|
143 |
arity declarations must obey two conditions:
|
wenzelm@145
|
144 |
\begin{itemize}
|
lcp@286
|
145 |
\item There must be no two declarations $ty :: (\vec{r})c$ and $ty ::
|
lcp@286
|
146 |
(\vec{s})c$ with $\vec{r} \neq \vec{s}$. For example, the following is
|
lcp@286
|
147 |
forbidden:
|
wenzelm@145
|
148 |
\begin{ttbox}
|
wenzelm@864
|
149 |
types
|
wenzelm@864
|
150 |
'a ty
|
wenzelm@864
|
151 |
arities
|
wenzelm@864
|
152 |
ty :: ({\ttlbrace}logic{\ttrbrace}) logic
|
wenzelm@864
|
153 |
ty :: ({\ttlbrace}{\ttrbrace})logic
|
wenzelm@145
|
154 |
\end{ttbox}
|
lcp@286
|
155 |
|
wenzelm@145
|
156 |
\item If there are two declarations $ty :: (s@1,\dots,s@n)c$ and $ty ::
|
wenzelm@145
|
157 |
(s@1',\dots,s@n')c'$ such that $c' < c$ then $s@i' \preceq s@i$ must hold
|
wenzelm@145
|
158 |
for $i=1,\dots,n$. The relationship $\preceq$, defined as
|
wenzelm@145
|
159 |
\[ s' \preceq s \iff \forall c\in s. \exists c'\in s'.~ c'\le c, \]
|
wenzelm@145
|
160 |
expresses that the set of types represented by $s'$ is a subset of the set of
|
lcp@286
|
161 |
types represented by $s$. For example, the following is forbidden:
|
wenzelm@145
|
162 |
\begin{ttbox}
|
wenzelm@864
|
163 |
classes
|
wenzelm@864
|
164 |
term < logic
|
wenzelm@864
|
165 |
types
|
wenzelm@864
|
166 |
'a ty
|
wenzelm@864
|
167 |
arities
|
wenzelm@864
|
168 |
ty :: ({\ttlbrace}logic{\ttrbrace})logic
|
wenzelm@864
|
169 |
ty :: ({\ttlbrace}{\ttrbrace})term
|
wenzelm@145
|
170 |
\end{ttbox}
|
lcp@286
|
171 |
|
wenzelm@145
|
172 |
\end{itemize}
|
wenzelm@145
|
173 |
|
lcp@104
|
174 |
|
lcp@324
|
175 |
\section{Loading a new theory}\label{LoadingTheories}
|
lcp@324
|
176 |
\index{theories!loading}\index{files!reading}
|
wenzelm@864
|
177 |
\begin{ttbox}
|
lcp@286
|
178 |
use_thy : string -> unit
|
lcp@286
|
179 |
time_use_thy : string -> unit
|
lcp@286
|
180 |
loadpath : string list ref \hfill{\bf initially {\tt["."]}}
|
lcp@286
|
181 |
delete_tmpfiles : bool ref \hfill{\bf initially true}
|
lcp@286
|
182 |
\end{ttbox}
|
nipkow@275
|
183 |
|
lcp@324
|
184 |
\begin{ttdescription}
|
wenzelm@864
|
185 |
\item[\ttindexbold{use_thy} $thyname$]
|
lcp@286
|
186 |
reads the theory $thyname$ and creates an \ML{} structure as described below.
|
clasohm@138
|
187 |
|
wenzelm@864
|
188 |
\item[\ttindexbold{time_use_thy} $thyname$]
|
lcp@286
|
189 |
calls {\tt use_thy} $thyname$ and reports the time taken.
|
lcp@286
|
190 |
|
wenzelm@864
|
191 |
\item[\ttindexbold{loadpath}]
|
lcp@286
|
192 |
contains a list of directories to search when locating the files that
|
lcp@286
|
193 |
define a theory. This list is only used if the theory name in {\tt
|
lcp@286
|
194 |
use_thy} does not specify the path explicitly.
|
lcp@286
|
195 |
|
wenzelm@864
|
196 |
\item[\ttindexbold{delete_tmpfiles} := false;]
|
lcp@286
|
197 |
suppresses the deletion of temporary files.
|
lcp@324
|
198 |
\end{ttdescription}
|
lcp@286
|
199 |
%
|
lcp@104
|
200 |
Each theory definition must reside in a separate file. Let the file {\it
|
lcp@332
|
201 |
T}{\tt.thy} contain the definition of a theory called~$T$, whose parent
|
lcp@332
|
202 |
theories are $TB@1$ \dots $TB@n$. Calling \ttindexbold{use_thy}~{\tt"{\it
|
lcp@332
|
203 |
T\/}"} reads the file {\it T}{\tt.thy}, writes a temporary \ML{}
|
lcp@332
|
204 |
file {\tt.{\it T}.thy.ML}, and reads the latter file. Recursive {\tt
|
lcp@286
|
205 |
use_thy} calls load those parent theories that have not been loaded
|
lcp@332
|
206 |
previously; the recursive calls may continue to any depth. One {\tt use_thy}
|
lcp@332
|
207 |
call can read an entire logic provided all theories are linked appropriately.
|
clasohm@138
|
208 |
|
wenzelm@864
|
209 |
The result is an \ML\ structure~$T$ containing at least a component {\tt thy}
|
wenzelm@864
|
210 |
for the new theory and components for each of the rules. The structure also
|
lcp@332
|
211 |
contains the definitions of the {\tt ML} section, if present. The file
|
wenzelm@864
|
212 |
{\tt.{\it T}.thy.ML} is then deleted if {\tt delete_tmpfiles} is set to {\tt
|
wenzelm@864
|
213 |
true} and no errors occurred.
|
clasohm@138
|
214 |
|
lcp@332
|
215 |
Finally the file {\it T}{\tt.ML} is read, if it exists. This file normally
|
lcp@332
|
216 |
begins with the declaration {\tt open~$T$} and contains proofs involving
|
lcp@332
|
217 |
the new theory.
|
clasohm@138
|
218 |
|
wenzelm@864
|
219 |
Some applications construct theories directly by calling \ML\ functions. In
|
wenzelm@864
|
220 |
this situation there is no {\tt.thy} file, only an {\tt.ML} file. The
|
wenzelm@864
|
221 |
{\tt.ML} file must declare an \ML\ structure having the theory's name and a
|
wenzelm@864
|
222 |
component {\tt thy} containing the new theory object.
|
wenzelm@864
|
223 |
Section~\ref{sec:pseudo-theories} below describes a way of linking such
|
wenzelm@864
|
224 |
theories to their parents.
|
lcp@159
|
225 |
|
lcp@324
|
226 |
\begin{warn}
|
wenzelm@864
|
227 |
Temporary files are written to the current directory, so this must be
|
wenzelm@864
|
228 |
writable. Isabelle inherits the current directory from the operating
|
wenzelm@864
|
229 |
system; you can change it within Isabelle by typing {\tt
|
wenzelm@864
|
230 |
cd"$dir$"}\index{*cd}.
|
lcp@324
|
231 |
\end{warn}
|
clasohm@138
|
232 |
|
lcp@324
|
233 |
|
lcp@324
|
234 |
\section{Reloading modified theories}\label{sec:reloading-theories}
|
lcp@324
|
235 |
\indexbold{theories!reloading}
|
wenzelm@864
|
236 |
\begin{ttbox}
|
lcp@286
|
237 |
update : unit -> unit
|
lcp@286
|
238 |
unlink_thy : string -> unit
|
lcp@286
|
239 |
\end{ttbox}
|
lcp@332
|
240 |
Changing a theory on disk often makes it necessary to reload all theories
|
lcp@332
|
241 |
descended from it. However, {\tt use_thy} reads only one theory, even if
|
lcp@332
|
242 |
some of the parent theories are out of date. In this case you should call
|
lcp@332
|
243 |
{\tt update()}.
|
lcp@332
|
244 |
|
lcp@286
|
245 |
Isabelle keeps track of all loaded theories and their files. If
|
lcp@286
|
246 |
\ttindex{use_thy} finds that the theory to be loaded has been read before,
|
lcp@286
|
247 |
it determines whether to reload the theory as follows. First it looks for
|
lcp@286
|
248 |
the theory's files in their previous location. If it finds them, it
|
lcp@286
|
249 |
compares their modification times to the internal data and stops if they
|
lcp@286
|
250 |
are equal. If the files have been moved, {\tt use_thy} searches for them
|
lcp@286
|
251 |
as it would for a new theory. After {\tt use_thy} reloads a theory, it
|
lcp@286
|
252 |
marks the children as out-of-date.
|
clasohm@138
|
253 |
|
lcp@324
|
254 |
\begin{ttdescription}
|
wenzelm@864
|
255 |
\item[\ttindexbold{update}()]
|
wenzelm@864
|
256 |
reloads all modified theories and their descendants in the correct order.
|
clasohm@138
|
257 |
|
lcp@286
|
258 |
\item[\ttindexbold{unlink_thy} $thyname$]\indexbold{theories!removing}
|
lcp@286
|
259 |
informs Isabelle that theory $thyname$ no longer exists. If you delete the
|
lcp@286
|
260 |
theory files for $thyname$ then you must execute {\tt unlink_thy};
|
lcp@286
|
261 |
otherwise {\tt update} will complain about a missing file.
|
lcp@324
|
262 |
\end{ttdescription}
|
clasohm@138
|
263 |
|
lcp@286
|
264 |
|
lcp@332
|
265 |
\goodbreak
|
lcp@324
|
266 |
\subsection{Important note for Poly/ML users}\index{Poly/{\ML} compiler}
|
lcp@286
|
267 |
The theory mechanism depends upon reference variables. At the end of a
|
lcp@286
|
268 |
Poly/\ML{} session, the contents of references are lost unless they are
|
wenzelm@864
|
269 |
declared in the current database. In particular, assignments to references
|
wenzelm@864
|
270 |
of the {\tt Pure} database are lost, including all information about loaded
|
wenzelm@864
|
271 |
theories. To avoid losing this information simply call
|
lcp@286
|
272 |
\begin{ttbox}
|
nipkow@478
|
273 |
init_thy_reader();
|
lcp@286
|
274 |
\end{ttbox}
|
nipkow@478
|
275 |
when building the new database.
|
lcp@286
|
276 |
|
lcp@286
|
277 |
|
lcp@332
|
278 |
\subsection{*Pseudo theories}\label{sec:pseudo-theories}
|
lcp@332
|
279 |
\indexbold{theories!pseudo}%
|
nipkow@275
|
280 |
Any automatic reloading facility requires complete knowledge of all
|
lcp@286
|
281 |
dependencies. Sometimes theories depend on objects created in \ML{} files
|
wenzelm@864
|
282 |
with no associated theory definition file. These objects may be theories but
|
wenzelm@864
|
283 |
they could also be theorems, proof procedures, etc.
|
lcp@332
|
284 |
|
lcp@332
|
285 |
Unless such dependencies are documented, {\tt update} fails to reload these
|
lcp@332
|
286 |
\ML{} files and the system is left in a state where some objects, such as
|
lcp@332
|
287 |
theorems, still refer to old versions of theories. This may lead to the
|
lcp@332
|
288 |
error
|
nipkow@275
|
289 |
\begin{ttbox}
|
wenzelm@864
|
290 |
Attempt to merge different versions of theories: \dots
|
nipkow@275
|
291 |
\end{ttbox}
|
lcp@324
|
292 |
Therefore there is a way to link theories and {\bf orphaned} \ML{} files ---
|
wenzelm@864
|
293 |
those not associated with a theory definition.
|
clasohm@138
|
294 |
|
lcp@324
|
295 |
Let us assume we have an orphaned \ML{} file named {\tt orphan.ML} and a
|
lcp@332
|
296 |
theory~$B$ that depends on {\tt orphan.ML} --- for example, {\tt B.ML} uses
|
lcp@332
|
297 |
theorems proved in {\tt orphan.ML}. Then {\tt B.thy} should
|
wenzelm@864
|
298 |
mention this dependency as follows:
|
clasohm@138
|
299 |
\begin{ttbox}
|
wenzelm@864
|
300 |
B = \(\ldots\) + "orphan" + \(\ldots\)
|
clasohm@138
|
301 |
\end{ttbox}
|
clasohm@1369
|
302 |
Quoted strings stand for theories which have to be loaded before the
|
clasohm@1369
|
303 |
current theory is read but which are not used in building the base of
|
clasohm@1369
|
304 |
theory~$B$. Whenever {\tt orphan} changes and is reloaded, Isabelle
|
clasohm@1369
|
305 |
knows that $B$ has to be updated, too.
|
nipkow@275
|
306 |
|
clasohm@1369
|
307 |
Note that it's necessary for {\tt orphan} to declare a special ML
|
clasohm@1369
|
308 |
object of type {\tt theory} which is present in all theories. This is
|
clasohm@1369
|
309 |
normally achieved by adding the file {\tt orphan.thy} to make {\tt
|
clasohm@1369
|
310 |
orphan} a {\bf pseudo theory}. A minimum version of {\tt orphan.thy}
|
clasohm@1369
|
311 |
would be
|
clasohm@1369
|
312 |
|
clasohm@1369
|
313 |
\begin{ttbox}
|
clasohm@1369
|
314 |
orphan = Pure
|
clasohm@1369
|
315 |
\end{ttbox}
|
clasohm@1369
|
316 |
|
clasohm@1369
|
317 |
which uses {\tt Pure} to make a dummy theory. Normally though the
|
clasohm@1369
|
318 |
orphaned file has its own dependencies. If {\tt orphan.ML} depends on
|
clasohm@1369
|
319 |
theories or files $A@1$, \ldots, $A@n$, record this by creating the
|
clasohm@1369
|
320 |
pseudo theory in the following way:
|
nipkow@275
|
321 |
\begin{ttbox}
|
wenzelm@864
|
322 |
orphan = \(A@1\) + \(\ldots\) + \(A@n\)
|
nipkow@275
|
323 |
\end{ttbox}
|
clasohm@1369
|
324 |
The resulting theory ensures that {\tt update} reloads {\tt orphan}
|
clasohm@1369
|
325 |
whenever it reloads one of the $A@i$.
|
clasohm@138
|
326 |
|
wenzelm@864
|
327 |
For an extensive example of how this technique can be used to link lots of
|
wenzelm@864
|
328 |
theory files and load them by just a few {\tt use_thy} calls, consult the
|
wenzelm@864
|
329 |
sources of \ZF{} set theory.
|
clasohm@138
|
330 |
|
lcp@104
|
331 |
|
lcp@104
|
332 |
|
clasohm@866
|
333 |
\section{Basic operations on theories}\label{BasicOperationsOnTheories}
|
wenzelm@864
|
334 |
\subsection{Extracting an axiom or theorem from a theory}
|
lcp@324
|
335 |
\index{theories!axioms of}\index{axioms!extracting}
|
wenzelm@864
|
336 |
\index{theories!theorems of}\index{theorems!extracting}
|
wenzelm@864
|
337 |
\begin{ttbox}
|
wenzelm@864
|
338 |
get_axiom : theory -> string -> thm
|
wenzelm@864
|
339 |
get_thm : theory -> string -> thm
|
wenzelm@864
|
340 |
assume_ax : theory -> string -> thm
|
lcp@104
|
341 |
\end{ttbox}
|
lcp@324
|
342 |
\begin{ttdescription}
|
wenzelm@864
|
343 |
\item[\ttindexbold{get_axiom} $thy$ $name$]
|
clasohm@866
|
344 |
returns an axiom with the given $name$ from $thy$, raising exception
|
clasohm@866
|
345 |
\xdx{THEORY} if none exists. Merging theories can cause several axioms
|
clasohm@866
|
346 |
to have the same name; {\tt get_axiom} returns an arbitrary one.
|
lcp@104
|
347 |
|
wenzelm@864
|
348 |
\item[\ttindexbold{get_thm} $thy$ $name$]
|
clasohm@866
|
349 |
is analogous to {\tt get_axiom}, but looks for a stored theorem. Like
|
clasohm@866
|
350 |
{\tt get_axiom} it searches all parents of a theory if the theorem
|
clasohm@866
|
351 |
is not associated with $thy$.
|
wenzelm@864
|
352 |
|
wenzelm@864
|
353 |
\item[\ttindexbold{assume_ax} $thy$ $formula$]
|
lcp@286
|
354 |
reads the {\it formula} using the syntax of $thy$, following the same
|
lcp@286
|
355 |
conventions as axioms in a theory definition. You can thus pretend that
|
lcp@286
|
356 |
{\it formula} is an axiom and use the resulting theorem like an axiom.
|
lcp@286
|
357 |
Actually {\tt assume_ax} returns an assumption; \ttindex{result}
|
lcp@286
|
358 |
complains about additional assumptions, but \ttindex{uresult} does not.
|
lcp@104
|
359 |
|
lcp@104
|
360 |
For example, if {\it formula} is
|
lcp@332
|
361 |
\hbox{\tt a=b ==> b=a} then the resulting theorem has the form
|
lcp@332
|
362 |
\hbox{\verb'?a=?b ==> ?b=?a [!!a b. a=b ==> b=a]'}
|
lcp@324
|
363 |
\end{ttdescription}
|
lcp@104
|
364 |
|
lcp@286
|
365 |
\subsection{Building a theory}
|
lcp@286
|
366 |
\label{BuildingATheory}
|
lcp@286
|
367 |
\index{theories!constructing|bold}
|
wenzelm@864
|
368 |
\begin{ttbox}
|
lcp@332
|
369 |
pure_thy : theory
|
lcp@332
|
370 |
merge_theories : theory * theory -> theory
|
lcp@286
|
371 |
\end{ttbox}
|
lcp@324
|
372 |
\begin{ttdescription}
|
wenzelm@864
|
373 |
\item[\ttindexbold{pure_thy}] contains just the syntax and signature
|
lcp@286
|
374 |
of the meta-logic. There are no axioms: meta-level inferences are carried
|
lcp@286
|
375 |
out by \ML\ functions.
|
lcp@286
|
376 |
\item[\ttindexbold{merge_theories} ($thy@1$, $thy@2$)] merges the two
|
wenzelm@864
|
377 |
theories $thy@1$ and $thy@2$. The resulting theory contains all of the
|
wenzelm@864
|
378 |
syntax, signature and axioms of the constituent theories. Merging theories
|
wenzelm@864
|
379 |
that contain different identification stamps of the same name fails with
|
wenzelm@864
|
380 |
the following message
|
wenzelm@864
|
381 |
\begin{ttbox}
|
wenzelm@864
|
382 |
Attempt to merge different versions of theories: "\(T@1\)", \(\ldots\), "\(T@n\)"
|
wenzelm@864
|
383 |
\end{ttbox}
|
wenzelm@864
|
384 |
This error may especially occur when a theory is redeclared --- say to
|
wenzelm@864
|
385 |
change an incorrect axiom --- and bindings to old versions persist.
|
wenzelm@864
|
386 |
Isabelle ensures that old and new theories of the same name are not
|
wenzelm@864
|
387 |
involved in a proof.
|
wenzelm@864
|
388 |
|
wenzelm@864
|
389 |
%% FIXME
|
nipkow@478
|
390 |
%\item [\ttindexbold{extend_theory} $thy$ {\tt"}$T${\tt"} $\cdots$] extends
|
nipkow@478
|
391 |
% the theory $thy$ with new types, constants, etc. $T$ identifies the theory
|
nipkow@478
|
392 |
% internally. When a theory is redeclared, say to change an incorrect axiom,
|
nipkow@478
|
393 |
% bindings to the old axiom may persist. Isabelle ensures that the old and
|
nipkow@478
|
394 |
% new theories are not involved in the same proof. Attempting to combine
|
nipkow@478
|
395 |
% different theories having the same name $T$ yields the fatal error
|
nipkow@478
|
396 |
%extend_theory : theory -> string -> \(\cdots\) -> theory
|
wenzelm@864
|
397 |
%\begin{ttbox}
|
wenzelm@864
|
398 |
%Attempt to merge different versions of theory: \(T\)
|
wenzelm@864
|
399 |
%\end{ttbox}
|
lcp@324
|
400 |
\end{ttdescription}
|
lcp@286
|
401 |
|
wenzelm@864
|
402 |
%% FIXME
|
nipkow@275
|
403 |
%\item [\ttindexbold{extend_theory} $thy$ {\tt"}$T${\tt"}
|
nipkow@275
|
404 |
% ($classes$, $default$, $types$, $arities$, $consts$, $sextopt$) $rules$]
|
nipkow@275
|
405 |
%\hfill\break %%% include if line is just too short
|
lcp@286
|
406 |
%is the \ML{} equivalent of the following theory definition:
|
nipkow@275
|
407 |
%\begin{ttbox}
|
nipkow@275
|
408 |
%\(T\) = \(thy\) +
|
nipkow@275
|
409 |
%classes \(c\) < \(c@1\),\(\dots\),\(c@m\)
|
nipkow@275
|
410 |
% \dots
|
nipkow@275
|
411 |
%default {\(d@1,\dots,d@r\)}
|
nipkow@275
|
412 |
%types \(tycon@1\),\dots,\(tycon@i\) \(n\)
|
nipkow@275
|
413 |
% \dots
|
nipkow@275
|
414 |
%arities \(tycon@1'\),\dots,\(tycon@j'\) :: (\(s@1\),\dots,\(s@n\))\(c\)
|
nipkow@275
|
415 |
% \dots
|
nipkow@275
|
416 |
%consts \(b@1\),\dots,\(b@k\) :: \(\tau\)
|
nipkow@275
|
417 |
% \dots
|
nipkow@275
|
418 |
%rules \(name\) \(rule\)
|
nipkow@275
|
419 |
% \dots
|
nipkow@275
|
420 |
%end
|
nipkow@275
|
421 |
%\end{ttbox}
|
nipkow@275
|
422 |
%where
|
nipkow@275
|
423 |
%\begin{tabular}[t]{l@{~=~}l}
|
nipkow@275
|
424 |
%$classes$ & \tt[("$c$",["$c@1$",\dots,"$c@m$"]),\dots] \\
|
nipkow@275
|
425 |
%$default$ & \tt["$d@1$",\dots,"$d@r$"]\\
|
nipkow@275
|
426 |
%$types$ & \tt[([$tycon@1$,\dots,$tycon@i$], $n$),\dots] \\
|
nipkow@275
|
427 |
%$arities$ & \tt[([$tycon'@1$,\dots,$tycon'@j$], ([$s@1$,\dots,$s@n$],$c$)),\dots]
|
nipkow@275
|
428 |
%\\
|
nipkow@275
|
429 |
%$consts$ & \tt[([$b@1$,\dots,$b@k$],$\tau$),\dots] \\
|
nipkow@275
|
430 |
%$rules$ & \tt[("$name$",$rule$),\dots]
|
nipkow@275
|
431 |
%\end{tabular}
|
lcp@104
|
432 |
|
lcp@104
|
433 |
|
wenzelm@864
|
434 |
\subsection{Inspecting a theory}\label{sec:inspct-thy}
|
lcp@104
|
435 |
\index{theories!inspecting|bold}
|
wenzelm@864
|
436 |
\begin{ttbox}
|
lcp@104
|
437 |
print_theory : theory -> unit
|
wenzelm@864
|
438 |
axioms_of : theory -> (string * thm) list
|
wenzelm@864
|
439 |
thms_of : theory -> (string * thm) list
|
lcp@104
|
440 |
parents_of : theory -> theory list
|
lcp@104
|
441 |
sign_of : theory -> Sign.sg
|
lcp@104
|
442 |
stamps_of_thy : theory -> string ref list
|
lcp@104
|
443 |
\end{ttbox}
|
wenzelm@864
|
444 |
These provide means of viewing a theory's components.
|
lcp@324
|
445 |
\begin{ttdescription}
|
wenzelm@864
|
446 |
\item[\ttindexbold{print_theory} $thy$]
|
wenzelm@864
|
447 |
prints the contents of $thy$ excluding the syntax related parts (which are
|
wenzelm@864
|
448 |
shown by {\tt print_syntax}). The output is quite verbose.
|
lcp@104
|
449 |
|
wenzelm@864
|
450 |
\item[\ttindexbold{axioms_of} $thy$]
|
wenzelm@864
|
451 |
returns the additional axioms of the most recent extend node of~$thy$.
|
lcp@104
|
452 |
|
wenzelm@864
|
453 |
\item[\ttindexbold{thms_of} $thy$]
|
clasohm@866
|
454 |
returns all theorems that are associated with $thy$.
|
wenzelm@864
|
455 |
|
wenzelm@864
|
456 |
\item[\ttindexbold{parents_of} $thy$]
|
wenzelm@864
|
457 |
returns the direct ancestors of~$thy$.
|
wenzelm@864
|
458 |
|
wenzelm@864
|
459 |
\item[\ttindexbold{sign_of} $thy$]
|
wenzelm@864
|
460 |
returns the signature associated with~$thy$. It is useful with functions
|
wenzelm@864
|
461 |
like {\tt read_instantiate_sg}, which take a signature as an argument.
|
lcp@104
|
462 |
|
lcp@104
|
463 |
\item[\ttindexbold{stamps_of_thy} $thy$]\index{signatures}
|
wenzelm@864
|
464 |
returns the identification \rmindex{stamps} of the signature associated
|
wenzelm@864
|
465 |
with~$thy$.
|
lcp@324
|
466 |
\end{ttdescription}
|
lcp@104
|
467 |
|
lcp@104
|
468 |
|
clasohm@1380
|
469 |
\section{Generating HTML documents}
|
clasohm@1369
|
470 |
\index{HTML|bold}
|
clasohm@1369
|
471 |
|
clasohm@1369
|
472 |
Isabelle is able to make HTML documents that show a theory's
|
clasohm@1369
|
473 |
definition, the theorems proved in its ML file and the relationship
|
clasohm@1369
|
474 |
with its ancestors and descendants. HTML stands for Hypertext Markup
|
clasohm@1369
|
475 |
Language and is used in the World Wide Web to represent text
|
clasohm@1380
|
476 |
containing images and links to other documents. Web browsers like
|
clasohm@1380
|
477 |
{\tt xmosaic} or {\tt netscape} are used to view these documents.
|
clasohm@1369
|
478 |
|
clasohm@1369
|
479 |
Besides the three HTML files that are made for every theory
|
clasohm@1369
|
480 |
(definition and theorems, ancestors, descendants), Isabelle stores
|
clasohm@1369
|
481 |
links to all theories in an index file. These indexes are themself
|
clasohm@1380
|
482 |
linked with other indexes to represent the hierarchic structure of
|
clasohm@1380
|
483 |
Isabelle's logics.
|
clasohm@1369
|
484 |
|
clasohm@1369
|
485 |
To make HTML files for logics that are part of the Isabelle
|
clasohm@1380
|
486 |
distribution, simply set the shell environment variable {\tt
|
clasohm@1380
|
487 |
MAKE_HTML} before compiling a logic. This works for single logics as
|
clasohm@1380
|
488 |
well as for the shell script {\tt make-all} (see
|
clasohm@1380
|
489 |
\ref{sec:shell-scripts}). To make HTML files for {\tt FOL} using a
|
clasohm@1380
|
490 |
{\tt csh} style shell, the following commands can be used:
|
clasohm@1380
|
491 |
|
clasohm@1380
|
492 |
\begin{ttbox}
|
clasohm@1380
|
493 |
cd FOL
|
clasohm@1380
|
494 |
setenv MAKE_HTML
|
clasohm@1380
|
495 |
make
|
clasohm@1380
|
496 |
\end{ttbox}
|
clasohm@1380
|
497 |
|
clasohm@1497
|
498 |
The databases made this way do not differ from the ones made with an
|
clasohm@1497
|
499 |
unset {\tt MAKE_HTML}; in particular no HTML files are written if the
|
clasohm@1497
|
500 |
database is used to manually load a theory.
|
clasohm@1497
|
501 |
|
clasohm@1497
|
502 |
As you will see below, the HTML generation is controlled by a boolean
|
clasohm@1497
|
503 |
reference variable. If you want to make databases which define this
|
clasohm@1497
|
504 |
variable's value as {\tt true} and where therefore HTML files are
|
clasohm@1497
|
505 |
written each time {\tt use_thy} is invoked, you have to set {\tt
|
clasohm@1497
|
506 |
MAKE_HTML} to ``{\tt true}'':
|
clasohm@1497
|
507 |
|
clasohm@1497
|
508 |
\begin{ttbox}
|
clasohm@1497
|
509 |
cd FOL
|
clasohm@1497
|
510 |
setenv MAKE_HTML true
|
clasohm@1497
|
511 |
make
|
clasohm@1497
|
512 |
\end{ttbox}
|
clasohm@1497
|
513 |
|
clasohm@1497
|
514 |
All theories loaded from within the {\tt FOL} database and all
|
clasohm@1497
|
515 |
databases derived from it will now cause HTML files to be written.
|
clasohm@1497
|
516 |
This behaviour can be changed by assigning a value of {\tt false} to
|
clasohm@1497
|
517 |
the boolean reference variable {\tt make_html}. Be careful when making
|
clasohm@1520
|
518 |
such databases publicly available since it means that your users will
|
clasohm@1520
|
519 |
generate HTML files though they might not intend to do so.
|
clasohm@1452
|
520 |
|
clasohm@1380
|
521 |
As some of Isabelle's logics are based on others (e.g. {\tt ZF} on
|
clasohm@1380
|
522 |
{\tt FOL}) and because the HTML files list a theory's ancestors, you
|
clasohm@1380
|
523 |
should not make HTML files for a logic if the HTML files for the base
|
clasohm@1380
|
524 |
logic do not exist. Otherwise some of the hypertext links might point
|
clasohm@1380
|
525 |
to non-existing documents.
|
clasohm@1380
|
526 |
|
clasohm@1380
|
527 |
The entry point to all logics is the {\tt index.html} file located in
|
clasohm@1380
|
528 |
Isabelle's main directory. You can also access a HTML version of the
|
clasohm@1380
|
529 |
distribution package at
|
clasohm@1369
|
530 |
|
clasohm@1369
|
531 |
\begin{ttbox}
|
clasohm@1369
|
532 |
http://www4.informatik.tu-muenchen.de/~nipkow/isabelle
|
clasohm@1369
|
533 |
\end{ttbox}
|
clasohm@1369
|
534 |
|
clasohm@1380
|
535 |
|
clasohm@1380
|
536 |
\subsection*{Manual HTML generation}
|
clasohm@1380
|
537 |
|
clasohm@1551
|
538 |
To manually control the generation of HTML files the following
|
clasohm@1551
|
539 |
commands and reference variables are used:
|
clasohm@1369
|
540 |
|
clasohm@1369
|
541 |
\begin{ttbox}
|
clasohm@1369
|
542 |
init_html : unit -> unit
|
clasohm@1369
|
543 |
make_html : bool ref
|
clasohm@1369
|
544 |
finish_html : unit -> unit
|
clasohm@1369
|
545 |
\end{ttbox}
|
clasohm@1369
|
546 |
|
clasohm@1369
|
547 |
\begin{ttdescription}
|
clasohm@1369
|
548 |
\item[\ttindexbold{init_html}]
|
clasohm@1369
|
549 |
activates the HTML facility. It stores the current working directory
|
clasohm@1380
|
550 |
as the place where the {\tt index.html} file for all theories loaded
|
clasohm@1380
|
551 |
afterwards will be stored.
|
clasohm@1369
|
552 |
|
clasohm@1369
|
553 |
\item[\ttindexbold{make_html}]
|
clasohm@1380
|
554 |
is a boolean reference variable read by {\tt use_thy} and other
|
clasohm@1380
|
555 |
functions to decide whether HTML files should be made. After you have
|
clasohm@1380
|
556 |
used {\tt init_html} you can manually change {\tt make_html}'s value
|
clasohm@1380
|
557 |
to temporarily disable HTML generation.
|
clasohm@1369
|
558 |
|
clasohm@1369
|
559 |
\item[\ttindexbold{finish_html}]
|
clasohm@1369
|
560 |
has to be called after all theories have been read that should be
|
clasohm@1380
|
561 |
listed in the current {\tt index.html} file. It reads a temporary
|
clasohm@1369
|
562 |
file with information about the theories read since the last use of
|
clasohm@1369
|
563 |
{\tt init_html} and makes the {\tt index.html} file. If {\tt
|
clasohm@1369
|
564 |
make_html} is {\tt false} nothing is done.
|
clasohm@1369
|
565 |
|
clasohm@1369
|
566 |
The indexes made by this function also contain a link to the {\tt
|
clasohm@1497
|
567 |
README} file if there exists one in the directory where the index is
|
clasohm@1380
|
568 |
stored. If there's a {\tt README.html} file it is used instead of
|
clasohm@1380
|
569 |
{\tt README}.
|
clasohm@1369
|
570 |
|
clasohm@1369
|
571 |
\end{ttdescription}
|
clasohm@1369
|
572 |
|
clasohm@1380
|
573 |
The above functions could be used in the following way:
|
clasohm@1369
|
574 |
|
clasohm@1380
|
575 |
\begin{ttbox}
|
clasohm@1380
|
576 |
init_html();
|
clasohm@1497
|
577 |
{\out Setting path for index.html to "/home/clasohm/isabelle/HOL"}
|
clasohm@1380
|
578 |
use_thy "List";
|
clasohm@1380
|
579 |
\dots
|
clasohm@1380
|
580 |
finish_html();
|
clasohm@1380
|
581 |
\end{ttbox}
|
clasohm@1380
|
582 |
|
clasohm@1380
|
583 |
Please note that HTML files are made only for those theories that are
|
clasohm@1380
|
584 |
read while {\tt make_html} is {\tt true}. These files may contain
|
clasohm@1380
|
585 |
links to theories that were read with a {\tt false} {\tt make_html}
|
clasohm@1380
|
586 |
and therefore point to non-existing files.
|
clasohm@1380
|
587 |
|
clasohm@1380
|
588 |
|
clasohm@1380
|
589 |
\subsection*{Extending or adding a logic}
|
clasohm@1380
|
590 |
|
clasohm@1380
|
591 |
If you add a new subdirectory to Isabelle's logics (or add a completly
|
clasohm@1380
|
592 |
new logic), you would have to call {\tt init_html} at the start of every
|
clasohm@1369
|
593 |
directory's {\tt ROOT.ML} file and {\tt finish_html} at the end of
|
clasohm@1369
|
594 |
it. This is automatically done if you use
|
clasohm@1369
|
595 |
|
clasohm@1380
|
596 |
\begin{ttbox}\index{use_dir}
|
clasohm@1369
|
597 |
use_dir : string -> unit
|
clasohm@1369
|
598 |
\end{ttbox}
|
clasohm@1369
|
599 |
|
clasohm@1369
|
600 |
This function takes a path as its parameter, changes the working
|
clasohm@1369
|
601 |
directory, calls {\tt init_html} if {\tt make_html} is {\tt true},
|
clasohm@1369
|
602 |
executes {\tt ROOT.ML}, and calls {\tt finish_html}. The {\tt
|
clasohm@1369
|
603 |
index.html} file written in this directory will be automatically
|
clasohm@1369
|
604 |
linked to the first index found in the (recursively searched)
|
clasohm@1369
|
605 |
superdirectories.
|
clasohm@1369
|
606 |
|
clasohm@1380
|
607 |
Instead of adding something like
|
clasohm@1380
|
608 |
|
clasohm@1380
|
609 |
\begin{ttbox}
|
clasohm@1380
|
610 |
use"ex/ROOT.ML";
|
clasohm@1380
|
611 |
\end{ttbox}
|
clasohm@1380
|
612 |
|
clasohm@1380
|
613 |
to the logic's makefile you have to use this:
|
clasohm@1380
|
614 |
|
clasohm@1380
|
615 |
\begin{ttbox}
|
clasohm@1380
|
616 |
use_dir"ex";
|
clasohm@1380
|
617 |
\end{ttbox}
|
clasohm@1380
|
618 |
|
clasohm@1380
|
619 |
Since {\tt use_dir} calls {\tt init_html} only if {\tt make_html} is
|
clasohm@1380
|
620 |
{\tt true} the generation of HTML files depends on the value this
|
clasohm@1380
|
621 |
reference variable has. It can either be inherited from the used \ML{}
|
clasohm@1380
|
622 |
database or set in the makefile before {\tt use_dir} is invoked,
|
clasohm@1380
|
623 |
e.g. to set it's value according to the environment variable {\tt
|
clasohm@1380
|
624 |
MAKE_HTML}.
|
clasohm@1380
|
625 |
|
clasohm@1380
|
626 |
The generated HTML files contain all theorems that were proved in the
|
clasohm@1380
|
627 |
theory's \ML{} file with {\tt qed}, {\tt qed_goal} and {\tt qed_goalw},
|
clasohm@1380
|
628 |
or stored with {\tt bind_thm} and {\tt store_thm}. Additionally there
|
clasohm@1380
|
629 |
is a hypertext link to the whole \ML{} file.
|
clasohm@1380
|
630 |
|
clasohm@1551
|
631 |
You can add section headings to the list of theorems by using
|
clasohm@1551
|
632 |
|
clasohm@1551
|
633 |
\begin{ttbox}\index{use_dir}
|
clasohm@1551
|
634 |
section: string -> unit
|
clasohm@1551
|
635 |
\end{ttbox}
|
clasohm@1551
|
636 |
|
clasohm@1551
|
637 |
in a theory's ML file, which converts a plain string to a HTML
|
clasohm@1551
|
638 |
heading and inserts it before the next theorem proved or stored with
|
clasohm@1551
|
639 |
one of the above functions. If {\tt make_html} is {\tt false} nothing
|
clasohm@1551
|
640 |
is done.
|
clasohm@1551
|
641 |
|
clasohm@1380
|
642 |
|
clasohm@1380
|
643 |
\subsection*{Using someone else's database}
|
clasohm@1380
|
644 |
|
clasohm@1380
|
645 |
To make them independent from their storage place, the HTML files only
|
clasohm@1380
|
646 |
contain relative paths which are derived from absolute ones like the
|
clasohm@1380
|
647 |
current working directory, {\tt gif_path} or {\tt base_path}. The
|
clasohm@1380
|
648 |
latter two are reference variables which are initialized at the time
|
clasohm@1380
|
649 |
when the {\tt Pure} database is made. Because you need write access
|
clasohm@1380
|
650 |
for the current directory to make HTML files and therefore (probably)
|
clasohm@1380
|
651 |
generate them in your home directory, the absolute {\tt base_path} is
|
clasohm@1380
|
652 |
not correct if you use someone else's database or a database derived
|
clasohm@1380
|
653 |
from it.
|
clasohm@1380
|
654 |
|
clasohm@1409
|
655 |
In that case you first should set {\tt base_path} to the value of {\em
|
clasohm@1409
|
656 |
your} Isabelle main directory, i.e. the directory that contains the
|
clasohm@1409
|
657 |
subdirectories where standard logics like {\tt FOL} and {\tt HOL} or
|
clasohm@1409
|
658 |
your own logics are stored. If you do not do this, the generated HTML
|
clasohm@1409
|
659 |
files will still be usable but may contain incomplete titles and lack
|
clasohm@1409
|
660 |
some hypertext links.
|
clasohm@1380
|
661 |
|
clasohm@1380
|
662 |
It's also a good idea to set {\tt gif_path} which points to the
|
clasohm@1380
|
663 |
directory containing two GIF images used in the HTML
|
clasohm@1380
|
664 |
documents. Normally this is the {\tt Tools} subdirectory of Isabelle's
|
clasohm@1380
|
665 |
main directory. While its value in general is still valid, your HTML
|
clasohm@1380
|
666 |
files would depend on files not owned by you. This prevents you from
|
clasohm@1380
|
667 |
changing the location of the HTML files (as they contain relative
|
clasohm@1380
|
668 |
paths) and also causes trouble if the database's maker (re)moves the
|
clasohm@1380
|
669 |
GIFs.
|
clasohm@1380
|
670 |
|
clasohm@1409
|
671 |
Here's what you should do before invoking {\tt init_html} using
|
clasohm@1380
|
672 |
someone else's \ML{} database:
|
clasohm@1380
|
673 |
|
clasohm@1380
|
674 |
\begin{ttbox}
|
clasohm@1380
|
675 |
base_path := "/home/smith/isabelle";
|
clasohm@1380
|
676 |
gif_path := "/home/smith/isabelle/Tools";
|
clasohm@1380
|
677 |
init_html();
|
clasohm@1380
|
678 |
\dots
|
clasohm@1380
|
679 |
\end{ttbox}
|
clasohm@1369
|
680 |
|
lcp@104
|
681 |
\section{Terms}
|
lcp@104
|
682 |
\index{terms|bold}
|
lcp@324
|
683 |
Terms belong to the \ML\ type \mltydx{term}, which is a concrete datatype
|
lcp@104
|
684 |
with six constructors: there are six kinds of term.
|
lcp@104
|
685 |
\begin{ttbox}
|
lcp@104
|
686 |
type indexname = string * int;
|
lcp@104
|
687 |
infix 9 $;
|
lcp@104
|
688 |
datatype term = Const of string * typ
|
lcp@104
|
689 |
| Free of string * typ
|
lcp@104
|
690 |
| Var of indexname * typ
|
lcp@104
|
691 |
| Bound of int
|
lcp@104
|
692 |
| Abs of string * typ * term
|
lcp@104
|
693 |
| op $ of term * term;
|
lcp@104
|
694 |
\end{ttbox}
|
lcp@324
|
695 |
\begin{ttdescription}
|
lcp@324
|
696 |
\item[\ttindexbold{Const}($a$, $T$)] \index{constants|bold}
|
lcp@286
|
697 |
is the {\bf constant} with name~$a$ and type~$T$. Constants include
|
lcp@286
|
698 |
connectives like $\land$ and $\forall$ as well as constants like~0
|
lcp@286
|
699 |
and~$Suc$. Other constants may be required to define a logic's concrete
|
wenzelm@864
|
700 |
syntax.
|
lcp@104
|
701 |
|
lcp@324
|
702 |
\item[\ttindexbold{Free}($a$, $T$)] \index{variables!free|bold}
|
lcp@324
|
703 |
is the {\bf free variable} with name~$a$ and type~$T$.
|
lcp@104
|
704 |
|
lcp@324
|
705 |
\item[\ttindexbold{Var}($v$, $T$)] \index{unknowns|bold}
|
lcp@324
|
706 |
is the {\bf scheme variable} with indexname~$v$ and type~$T$. An
|
lcp@324
|
707 |
\mltydx{indexname} is a string paired with a non-negative index, or
|
lcp@324
|
708 |
subscript; a term's scheme variables can be systematically renamed by
|
lcp@324
|
709 |
incrementing their subscripts. Scheme variables are essentially free
|
lcp@324
|
710 |
variables, but may be instantiated during unification.
|
lcp@104
|
711 |
|
lcp@324
|
712 |
\item[\ttindexbold{Bound} $i$] \index{variables!bound|bold}
|
lcp@324
|
713 |
is the {\bf bound variable} with de Bruijn index~$i$, which counts the
|
lcp@324
|
714 |
number of lambdas, starting from zero, between a variable's occurrence
|
lcp@324
|
715 |
and its binding. The representation prevents capture of variables. For
|
lcp@324
|
716 |
more information see de Bruijn \cite{debruijn72} or
|
lcp@324
|
717 |
Paulson~\cite[page~336]{paulson91}.
|
lcp@104
|
718 |
|
lcp@324
|
719 |
\item[\ttindexbold{Abs}($a$, $T$, $u$)]
|
lcp@324
|
720 |
\index{lambda abs@$\lambda$-abstractions|bold}
|
lcp@324
|
721 |
is the $\lambda$-{\bf abstraction} with body~$u$, and whose bound
|
lcp@324
|
722 |
variable has name~$a$ and type~$T$. The name is used only for parsing
|
lcp@324
|
723 |
and printing; it has no logical significance.
|
lcp@104
|
724 |
|
lcp@324
|
725 |
\item[$t$ \$ $u$] \index{$@{\tt\$}|bold} \index{function applications|bold}
|
wenzelm@864
|
726 |
is the {\bf application} of~$t$ to~$u$.
|
lcp@324
|
727 |
\end{ttdescription}
|
lcp@286
|
728 |
Application is written as an infix operator to aid readability.
|
lcp@332
|
729 |
Here is an \ML\ pattern to recognize \FOL{} formulae of
|
lcp@104
|
730 |
the form~$A\imp B$, binding the subformulae to~$A$ and~$B$:
|
wenzelm@864
|
731 |
\begin{ttbox}
|
lcp@104
|
732 |
Const("Trueprop",_) $ (Const("op -->",_) $ A $ B)
|
lcp@104
|
733 |
\end{ttbox}
|
lcp@104
|
734 |
|
lcp@104
|
735 |
|
lcp@324
|
736 |
\section{Variable binding}
|
lcp@286
|
737 |
\begin{ttbox}
|
lcp@286
|
738 |
loose_bnos : term -> int list
|
lcp@286
|
739 |
incr_boundvars : int -> term -> term
|
lcp@286
|
740 |
abstract_over : term*term -> term
|
lcp@286
|
741 |
variant_abs : string * typ * term -> string * term
|
lcp@286
|
742 |
aconv : term*term -> bool\hfill{\bf infix}
|
lcp@286
|
743 |
\end{ttbox}
|
lcp@286
|
744 |
These functions are all concerned with the de Bruijn representation of
|
lcp@286
|
745 |
bound variables.
|
lcp@324
|
746 |
\begin{ttdescription}
|
wenzelm@864
|
747 |
\item[\ttindexbold{loose_bnos} $t$]
|
lcp@286
|
748 |
returns the list of all dangling bound variable references. In
|
lcp@286
|
749 |
particular, {\tt Bound~0} is loose unless it is enclosed in an
|
lcp@286
|
750 |
abstraction. Similarly {\tt Bound~1} is loose unless it is enclosed in
|
lcp@286
|
751 |
at least two abstractions; if enclosed in just one, the list will contain
|
lcp@286
|
752 |
the number 0. A well-formed term does not contain any loose variables.
|
lcp@286
|
753 |
|
wenzelm@864
|
754 |
\item[\ttindexbold{incr_boundvars} $j$]
|
lcp@332
|
755 |
increases a term's dangling bound variables by the offset~$j$. This is
|
lcp@286
|
756 |
required when moving a subterm into a context where it is enclosed by a
|
lcp@286
|
757 |
different number of abstractions. Bound variables with a matching
|
lcp@286
|
758 |
abstraction are unaffected.
|
lcp@286
|
759 |
|
wenzelm@864
|
760 |
\item[\ttindexbold{abstract_over} $(v,t)$]
|
lcp@286
|
761 |
forms the abstraction of~$t$ over~$v$, which may be any well-formed term.
|
lcp@286
|
762 |
It replaces every occurrence of \(v\) by a {\tt Bound} variable with the
|
lcp@286
|
763 |
correct index.
|
lcp@286
|
764 |
|
wenzelm@864
|
765 |
\item[\ttindexbold{variant_abs} $(a,T,u)$]
|
lcp@286
|
766 |
substitutes into $u$, which should be the body of an abstraction.
|
lcp@286
|
767 |
It replaces each occurrence of the outermost bound variable by a free
|
lcp@286
|
768 |
variable. The free variable has type~$T$ and its name is a variant
|
lcp@332
|
769 |
of~$a$ chosen to be distinct from all constants and from all variables
|
lcp@286
|
770 |
free in~$u$.
|
lcp@286
|
771 |
|
wenzelm@864
|
772 |
\item[$t$ \ttindexbold{aconv} $u$]
|
lcp@286
|
773 |
tests whether terms~$t$ and~$u$ are \(\alpha\)-convertible: identical up
|
lcp@286
|
774 |
to renaming of bound variables.
|
lcp@286
|
775 |
\begin{itemize}
|
lcp@286
|
776 |
\item
|
lcp@286
|
777 |
Two constants, {\tt Free}s, or {\tt Var}s are \(\alpha\)-convertible
|
lcp@286
|
778 |
if their names and types are equal.
|
lcp@286
|
779 |
(Variables having the same name but different types are thus distinct.
|
lcp@286
|
780 |
This confusing situation should be avoided!)
|
lcp@286
|
781 |
\item
|
lcp@286
|
782 |
Two bound variables are \(\alpha\)-convertible
|
lcp@286
|
783 |
if they have the same number.
|
lcp@286
|
784 |
\item
|
lcp@286
|
785 |
Two abstractions are \(\alpha\)-convertible
|
lcp@286
|
786 |
if their bodies are, and their bound variables have the same type.
|
lcp@286
|
787 |
\item
|
lcp@286
|
788 |
Two applications are \(\alpha\)-convertible
|
lcp@286
|
789 |
if the corresponding subterms are.
|
lcp@286
|
790 |
\end{itemize}
|
lcp@286
|
791 |
|
lcp@324
|
792 |
\end{ttdescription}
|
lcp@286
|
793 |
|
wenzelm@864
|
794 |
\section{Certified terms}\index{terms!certified|bold}\index{signatures}
|
wenzelm@864
|
795 |
A term $t$ can be {\bf certified} under a signature to ensure that every type
|
wenzelm@864
|
796 |
in~$t$ is well-formed and every constant in~$t$ is a type instance of a
|
wenzelm@864
|
797 |
constant declared in the signature. The term must be well-typed and its use
|
wenzelm@864
|
798 |
of bound variables must be well-formed. Meta-rules such as {\tt forall_elim}
|
wenzelm@864
|
799 |
take certified terms as arguments.
|
lcp@104
|
800 |
|
lcp@324
|
801 |
Certified terms belong to the abstract type \mltydx{cterm}.
|
lcp@104
|
802 |
Elements of the type can only be created through the certification process.
|
lcp@104
|
803 |
In case of error, Isabelle raises exception~\ttindex{TERM}\@.
|
lcp@104
|
804 |
|
lcp@104
|
805 |
\subsection{Printing terms}
|
lcp@324
|
806 |
\index{terms!printing of}
|
wenzelm@864
|
807 |
\begin{ttbox}
|
nipkow@275
|
808 |
string_of_cterm : cterm -> string
|
lcp@104
|
809 |
Sign.string_of_term : Sign.sg -> term -> string
|
lcp@104
|
810 |
\end{ttbox}
|
lcp@324
|
811 |
\begin{ttdescription}
|
wenzelm@864
|
812 |
\item[\ttindexbold{string_of_cterm} $ct$]
|
lcp@104
|
813 |
displays $ct$ as a string.
|
lcp@104
|
814 |
|
wenzelm@864
|
815 |
\item[\ttindexbold{Sign.string_of_term} $sign$ $t$]
|
lcp@104
|
816 |
displays $t$ as a string, using the syntax of~$sign$.
|
lcp@324
|
817 |
\end{ttdescription}
|
lcp@104
|
818 |
|
lcp@104
|
819 |
\subsection{Making and inspecting certified terms}
|
wenzelm@864
|
820 |
\begin{ttbox}
|
nipkow@275
|
821 |
cterm_of : Sign.sg -> term -> cterm
|
nipkow@275
|
822 |
read_cterm : Sign.sg -> string * typ -> cterm
|
wenzelm@864
|
823 |
cert_axm : Sign.sg -> string * term -> string * term
|
wenzelm@864
|
824 |
read_axm : Sign.sg -> string * string -> string * term
|
nipkow@275
|
825 |
rep_cterm : cterm -> \{T:typ, t:term, sign:Sign.sg, maxidx:int\}
|
lcp@104
|
826 |
\end{ttbox}
|
lcp@324
|
827 |
\begin{ttdescription}
|
nipkow@275
|
828 |
\item[\ttindexbold{cterm_of} $sign$ $t$] \index{signatures}
|
lcp@104
|
829 |
certifies $t$ with respect to signature~$sign$.
|
lcp@104
|
830 |
|
wenzelm@864
|
831 |
\item[\ttindexbold{read_cterm} $sign$ ($s$, $T$)]
|
lcp@104
|
832 |
reads the string~$s$ using the syntax of~$sign$, creating a certified term.
|
lcp@104
|
833 |
The term is checked to have type~$T$; this type also tells the parser what
|
lcp@104
|
834 |
kind of phrase to parse.
|
lcp@104
|
835 |
|
wenzelm@864
|
836 |
\item[\ttindexbold{cert_axm} $sign$ ($name$, $t$)]
|
wenzelm@864
|
837 |
certifies $t$ with respect to $sign$ as a meta-proposition and converts all
|
wenzelm@864
|
838 |
exceptions to an error, including the final message
|
wenzelm@864
|
839 |
\begin{ttbox}
|
wenzelm@864
|
840 |
The error(s) above occurred in axiom "\(name\)"
|
wenzelm@864
|
841 |
\end{ttbox}
|
wenzelm@864
|
842 |
|
wenzelm@864
|
843 |
\item[\ttindexbold{read_axm} $sign$ ($name$, $s$)]
|
wenzelm@864
|
844 |
similar to {\tt cert_axm}, but first reads the string $s$ using the syntax of
|
wenzelm@864
|
845 |
$sign$.
|
wenzelm@864
|
846 |
|
wenzelm@864
|
847 |
\item[\ttindexbold{rep_cterm} $ct$]
|
lcp@104
|
848 |
decomposes $ct$ as a record containing its type, the term itself, its
|
lcp@104
|
849 |
signature, and the maximum subscript of its unknowns. The type and maximum
|
lcp@104
|
850 |
subscript are computed during certification.
|
lcp@324
|
851 |
\end{ttdescription}
|
lcp@104
|
852 |
|
lcp@104
|
853 |
|
wenzelm@864
|
854 |
\section{Types}\index{types|bold}
|
wenzelm@864
|
855 |
Types belong to the \ML\ type \mltydx{typ}, which is a concrete datatype with
|
wenzelm@864
|
856 |
three constructor functions. These correspond to type constructors, free
|
wenzelm@864
|
857 |
type variables and schematic type variables. Types are classified by sorts,
|
wenzelm@864
|
858 |
which are lists of classes (representing an intersection). A class is
|
wenzelm@864
|
859 |
represented by a string.
|
lcp@104
|
860 |
\begin{ttbox}
|
lcp@104
|
861 |
type class = string;
|
lcp@104
|
862 |
type sort = class list;
|
lcp@104
|
863 |
|
lcp@104
|
864 |
datatype typ = Type of string * typ list
|
lcp@104
|
865 |
| TFree of string * sort
|
lcp@104
|
866 |
| TVar of indexname * sort;
|
lcp@104
|
867 |
|
lcp@104
|
868 |
infixr 5 -->;
|
wenzelm@864
|
869 |
fun S --> T = Type ("fun", [S, T]);
|
lcp@104
|
870 |
\end{ttbox}
|
lcp@324
|
871 |
\begin{ttdescription}
|
lcp@324
|
872 |
\item[\ttindexbold{Type}($a$, $Ts$)] \index{type constructors|bold}
|
lcp@324
|
873 |
applies the {\bf type constructor} named~$a$ to the type operands~$Ts$.
|
lcp@324
|
874 |
Type constructors include~\tydx{fun}, the binary function space
|
lcp@324
|
875 |
constructor, as well as nullary type constructors such as~\tydx{prop}.
|
lcp@324
|
876 |
Other type constructors may be introduced. In expressions, but not in
|
lcp@324
|
877 |
patterns, \hbox{\tt$S$-->$T$} is a convenient shorthand for function
|
lcp@324
|
878 |
types.
|
lcp@104
|
879 |
|
lcp@324
|
880 |
\item[\ttindexbold{TFree}($a$, $s$)] \index{type variables|bold}
|
lcp@324
|
881 |
is the {\bf type variable} with name~$a$ and sort~$s$.
|
lcp@104
|
882 |
|
lcp@324
|
883 |
\item[\ttindexbold{TVar}($v$, $s$)] \index{type unknowns|bold}
|
lcp@324
|
884 |
is the {\bf type unknown} with indexname~$v$ and sort~$s$.
|
lcp@324
|
885 |
Type unknowns are essentially free type variables, but may be
|
lcp@324
|
886 |
instantiated during unification.
|
lcp@324
|
887 |
\end{ttdescription}
|
lcp@104
|
888 |
|
lcp@104
|
889 |
|
lcp@104
|
890 |
\section{Certified types}
|
lcp@104
|
891 |
\index{types!certified|bold}
|
wenzelm@864
|
892 |
Certified types, which are analogous to certified terms, have type
|
nipkow@275
|
893 |
\ttindexbold{ctyp}.
|
lcp@104
|
894 |
|
lcp@104
|
895 |
\subsection{Printing types}
|
lcp@324
|
896 |
\index{types!printing of}
|
wenzelm@864
|
897 |
\begin{ttbox}
|
nipkow@275
|
898 |
string_of_ctyp : ctyp -> string
|
lcp@104
|
899 |
Sign.string_of_typ : Sign.sg -> typ -> string
|
lcp@104
|
900 |
\end{ttbox}
|
lcp@324
|
901 |
\begin{ttdescription}
|
wenzelm@864
|
902 |
\item[\ttindexbold{string_of_ctyp} $cT$]
|
lcp@104
|
903 |
displays $cT$ as a string.
|
lcp@104
|
904 |
|
wenzelm@864
|
905 |
\item[\ttindexbold{Sign.string_of_typ} $sign$ $T$]
|
lcp@104
|
906 |
displays $T$ as a string, using the syntax of~$sign$.
|
lcp@324
|
907 |
\end{ttdescription}
|
lcp@104
|
908 |
|
lcp@104
|
909 |
|
lcp@104
|
910 |
\subsection{Making and inspecting certified types}
|
wenzelm@864
|
911 |
\begin{ttbox}
|
nipkow@275
|
912 |
ctyp_of : Sign.sg -> typ -> ctyp
|
nipkow@275
|
913 |
rep_ctyp : ctyp -> \{T: typ, sign: Sign.sg\}
|
lcp@104
|
914 |
\end{ttbox}
|
lcp@324
|
915 |
\begin{ttdescription}
|
nipkow@275
|
916 |
\item[\ttindexbold{ctyp_of} $sign$ $T$] \index{signatures}
|
lcp@104
|
917 |
certifies $T$ with respect to signature~$sign$.
|
lcp@104
|
918 |
|
wenzelm@864
|
919 |
\item[\ttindexbold{rep_ctyp} $cT$]
|
lcp@104
|
920 |
decomposes $cT$ as a record containing the type itself and its signature.
|
lcp@324
|
921 |
\end{ttdescription}
|
lcp@104
|
922 |
|
paulson@1846
|
923 |
|
paulson@1846
|
924 |
\section{Oracles: calling external reasoners }
|
paulson@1846
|
925 |
\label{sec:oracles}
|
paulson@1846
|
926 |
\index{oracles|(}
|
paulson@1846
|
927 |
|
paulson@1846
|
928 |
Oracles allow Isabelle to take advantage of external reasoners such as
|
paulson@1846
|
929 |
arithmetic decision procedures, model checkers, fast tautology checkers or
|
paulson@1846
|
930 |
computer algebra systems. Invoked as an oracle, an external reasoner can
|
paulson@1846
|
931 |
create arbitrary Isabelle theorems. It is your responsibility to ensure that
|
paulson@1846
|
932 |
the external reasoner is as trustworthy as your application requires.
|
paulson@1846
|
933 |
Isabelle's proof objects~(\S\ref{sec:proofObjects}) record how each theorem
|
paulson@1846
|
934 |
depends upon oracle calls.
|
paulson@1846
|
935 |
|
paulson@1846
|
936 |
\begin{ttbox}
|
paulson@1846
|
937 |
invoke_oracle : theory * Sign.sg * exn -> thm
|
paulson@1846
|
938 |
set_oracle : Sign.sg -> typ -> string
|
paulson@1846
|
939 |
\end{ttbox}
|
paulson@1846
|
940 |
\begin{ttdescription}
|
paulson@1846
|
941 |
\item[\ttindexbold{invoke_oracle} ($thy$, $sign$, $exn$)] invokes the oracle
|
paulson@1846
|
942 |
of theory $thy$ passing the information contained in the exception value
|
paulson@1846
|
943 |
$exn$ and creating a theorem having signature $sign$. Errors arise if $thy$
|
paulson@1846
|
944 |
does not have an oracle, if the oracle rejects its arguments or if its
|
paulson@1846
|
945 |
result is ill-typed.
|
paulson@1846
|
946 |
|
paulson@1846
|
947 |
\item[\ttindexbold{set_oracle} $fn$ $thy$] sets the oracle of theory $thy$ to
|
paulson@1846
|
948 |
be $fn$. It is seldom called explicitly, as there is syntax for oracles in
|
paulson@1846
|
949 |
theory files. A theory can have at most one oracle.
|
paulson@1846
|
950 |
\end{ttdescription}
|
paulson@1846
|
951 |
|
paulson@1846
|
952 |
A curious feature of {\ML} exceptions is that they are ordinary constructors.
|
paulson@1846
|
953 |
The {\ML} type {\tt exn} is a datatype that can be extended at any time. (See
|
paulson@1846
|
954 |
my {\em {ML} for the Working Programmer}~\cite{paulson-ml2}, especially
|
paulson@1846
|
955 |
page~136.) The oracle mechanism takes advantage of this to allow an oracle to
|
paulson@1846
|
956 |
take any information whatever.
|
paulson@1846
|
957 |
|
paulson@1846
|
958 |
There must be some way of invoking the external reasoner from \ML, either
|
paulson@1846
|
959 |
because it is coded in {\ML} or via an operating system interface. Isabelle
|
paulson@1846
|
960 |
expects the {\ML} function to take two arguments: a signature and an
|
paulson@1846
|
961 |
exception.
|
paulson@1846
|
962 |
\begin{itemize}
|
paulson@1846
|
963 |
\item The signature will typically be that of a desendant of the theory
|
paulson@1846
|
964 |
declaring the oracle. The oracle will use it to distinguish constants from
|
paulson@1846
|
965 |
variables, etc., and it will be attached to the generated theorems.
|
paulson@1846
|
966 |
|
paulson@1846
|
967 |
\item The exception is used to pass arbitrary information to the oracle. This
|
paulson@1846
|
968 |
information must contain a full description of the problem to be solved by
|
paulson@1846
|
969 |
the external reasoner, including any additional information that might be
|
paulson@1846
|
970 |
required. The oracle may raise the exception to indicate that it cannot
|
paulson@1846
|
971 |
solve the specified problem.
|
paulson@1846
|
972 |
\end{itemize}
|
paulson@1846
|
973 |
|
paulson@1846
|
974 |
A trivial example is provided on directory {\tt FOL/ex}. This oracle
|
paulson@1846
|
975 |
generates tautologies of the form $P\bimp\cdots\bimp P$, with an even number
|
paulson@1846
|
976 |
of $P$s.
|
paulson@1846
|
977 |
|
paulson@1846
|
978 |
File {\tt declIffOracle.ML} begins by declaring a new exception constructor
|
paulson@1846
|
979 |
for the oracle the information it requires: here, just an integer. It
|
paulson@1846
|
980 |
contains some code (suppressed below) for creating the tautologies, and
|
paulson@1846
|
981 |
finally declares the oracle function itself:
|
paulson@1846
|
982 |
\begin{ttbox}
|
paulson@1846
|
983 |
exception IffOracleExn of int;
|
paulson@1846
|
984 |
\(\vdots\)
|
paulson@1846
|
985 |
fun mk_iff_oracle (sign, IffOracleExn n) =
|
paulson@1846
|
986 |
if n>0 andalso n mod 2 = 0
|
paulson@1846
|
987 |
then Trueprop $ mk_iff n
|
paulson@1846
|
988 |
else raise IffOracleExn n;
|
paulson@1846
|
989 |
\end{ttbox}
|
paulson@1846
|
990 |
Observe the function two arguments, the signature {\tt sign} and the exception
|
paulson@1846
|
991 |
given as a pattern. The function checks its argument for validity. If $n$ is
|
paulson@1846
|
992 |
positive and even then it creates a tautology containing $n$ occurrences
|
paulson@1846
|
993 |
of~$P$. Otherwise it signals error by raising its own exception. Errors may
|
paulson@1846
|
994 |
be signalled by other means, such as returning the theorem {\tt True}.
|
paulson@1846
|
995 |
Please ensure that the oracle's result is correctly typed; Isabelle will
|
paulson@1846
|
996 |
reject ill-typed theorems by raising a cryptic exception at top level.
|
paulson@1846
|
997 |
|
paulson@1846
|
998 |
The theory file {\tt IffOracle.thy} packages up the function above as an
|
paulson@1846
|
999 |
oracle. The first line indicates that the new theory depends upon the file
|
paulson@1846
|
1000 |
{\tt declIffOracle.ML} (which declares the {\ML} code) as well as on \FOL.
|
paulson@1846
|
1001 |
The second line informs Isabelle that this theory has an oracle given by the
|
paulson@1846
|
1002 |
function {\tt mk_iff_oracle}.
|
paulson@1846
|
1003 |
\begin{ttbox}
|
paulson@1846
|
1004 |
IffOracle = "declIffOracle" + FOL +
|
paulson@1846
|
1005 |
oracle mk_iff_oracle
|
paulson@1846
|
1006 |
end
|
paulson@1846
|
1007 |
\end{ttbox}
|
paulson@1846
|
1008 |
Because a theory can have at most one oracle, the theory itself serves to
|
paulson@1846
|
1009 |
identify the oracle.
|
paulson@1846
|
1010 |
|
paulson@1846
|
1011 |
Here are some examples of invoking the oracle. An argument of 10 is allowed,
|
paulson@1846
|
1012 |
but one of 5 is forbidden:
|
paulson@1846
|
1013 |
\begin{ttbox}
|
paulson@1846
|
1014 |
invoke_oracle (IffOracle.thy, sign_of IffOracle.thy, IffOracleExn 10);
|
paulson@1846
|
1015 |
{\out "P <-> P <-> P <-> P <-> P <-> P <-> P <-> P <-> P <-> P" : thm}
|
paulson@1846
|
1016 |
invoke_oracle (IffOracle.thy, sign_of IffOracle.thy, IffOracleExn 5);
|
paulson@1846
|
1017 |
{\out Exception- IffOracleExn 5 raised}
|
paulson@1846
|
1018 |
\end{ttbox}
|
paulson@1846
|
1019 |
|
paulson@1846
|
1020 |
\index{oracles|)}
|
lcp@104
|
1021 |
\index{theories|)}
|