author  wenzelm 
Mon, 08 Dec 1997 20:29:49 +0100  
changeset 4384  429cba89b4c8 
parent 4374  245b64afefe2 
child 4543  82a45bdd0e80 
permissions  rwrr 
3201  1 

104  2 
%% $Id$ 
145  3 

104  4 
\chapter{Theories, Terms and Types} \label{theories} 
5 
\index{theories(}\index{signaturesbold} 

3108  6 
\index{reading!axiomssee{{\tt assume_ax}}} Theories organize the 
7 
syntax, declarations and axioms of a mathematical development. They 

8 
are built, starting from the {\Pure} or {\CPure} theory, by extending 

9 
and merging existing theories. They have the \ML\ type 

10 
\mltydx{theory}. Theory operations signal errors by raising exception 

11 
\xdx{THEORY}, returning a message and a list of theories. 

104  12 

13 
Signatures, which contain information about sorts, types, constants and 

332  14 
syntax, have the \ML\ type~\mltydx{Sign.sg}. For identification, each 
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset

15 
signature carries a unique list of \bfindex{stamps}, which are \ML\ 
324  16 
references to strings. The strings serve as humanreadable names; the 
104  17 
references serve as unique identifiers. Each primitive signature has a 
18 
single stamp. When two signatures are merged, their lists of stamps are 

19 
also merged. Every theory carries a unique signature. 

20 

21 
Terms and types are the underlying representation of logical syntax. Their 

275  22 
\ML\ definitions are irrelevant to naive Isabelle users. Programmers who 
23 
wish to extend Isabelle may need to know such details, say to code a tactic 

24 
that looks for subgoals of a particular form. Terms and types may be 

104  25 
`certified' to be wellformed with respect to a given signature. 
26 

324  27 

28 
\section{Defining theories}\label{sec:refdefiningtheories} 

104  29 

864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset

30 
Theories are usually defined using theory definition files (which have a name 
3485
f27a30a18a17
Now there are TWO spaces after each full stop, so that the Emacs sentence
paulson
parents:
3201
diff
changeset

31 
suffix {\tt .thy}). There is also a low level interface provided by certain 
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset

32 
\ML{} functions (see \S\ref{BuildingATheory}). 
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset

33 
Appendix~\ref{app:TheorySyntax} presents the concrete syntax for theory 
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset

34 
definitions; here is an explanation of the constituent parts: 
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset

35 
\begin{description} 
3108  36 
\item[{\it theoryDef}] is the full definition. The new theory is 
37 
called $id$. It is the union of the named {\bf parent 

38 
theories}\indexbold{theories!parent}, possibly extended with new 

39 
components. \thydx{Pure} and \thydx{CPure} are the basic theories, 

3485
f27a30a18a17
Now there are TWO spaces after each full stop, so that the Emacs sentence
paulson
parents:
3201
diff
changeset

40 
which contain only the metalogic. They differ just in their 
3108  41 
concrete syntax for function applications. 
138
9ba8bff1addc
added chapter "Defining Theories" and made changes for new Readthy functions
clasohm
parents:
104
diff
changeset

42 

864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset

43 
Normally each {\it name\/} is an identifier, the name of the parent theory. 
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset

44 
Quoted strings can be used to document additional file dependencies; see 
275  45 
\S\ref{LoadingTheories} for details. 
324  46 

864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset

47 
\item[$classes$] 
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset

48 
is a series of class declarations. Declaring {\tt$id$ < $id@1$ \dots\ 
324  49 
$id@n$} makes $id$ a subclass of the existing classes $id@1\dots 
50 
id@n$. This rules out cyclic class structures. Isabelle automatically 

51 
computes the transitive closure of subclass hierarchies; it is not 

52 
necessary to declare {\tt c < e} in addition to {\tt c < d} and {\tt d < 

53 
e}. 

54 

864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset

55 
\item[$default$] 
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset

56 
introduces $sort$ as the new default sort for type variables. This applies 
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset

57 
to unconstrained type variables in an input string but not to type 
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset

58 
variables created internally. If omitted, the default sort is the listwise 
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset

59 
union of the default sorts of the parent theories (i.e.\ their logical 
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset

60 
intersection). 
3108  61 

62 
\item[$sort$] is a finite set of classes. A single class $id$ 

63 
abbreviates the sort $\ttlbrace id\ttrbrace$. 

324  64 

864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset

65 
\item[$types$] 
324  66 
is a series of type declarations. Each declares a new type constructor 
67 
or type synonym. An $n$place type constructor is specified by 

68 
$(\alpha@1,\dots,\alpha@n)name$, where the type variables serve only to 

69 
indicate the number~$n$. 

70 

332  71 
A {\bf type synonym}\indexbold{type synonyms} is an abbreviation 
1387  72 
$(\alpha@1,\dots,\alpha@n)name = \tau$, where $name$ and $\tau$ can 
73 
be strings. 

864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset

74 

d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset

75 
\item[$infix$] 
324  76 
declares a type or constant to be an infix operator of priority $nat$ 
3485
f27a30a18a17
Now there are TWO spaces after each full stop, so that the Emacs sentence
paulson
parents:
3201
diff
changeset

77 
associating to the left ({\tt infixl}) or right ({\tt infixr}). Only 
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset

78 
2place type constructors can have infix status; an example is {\tt 
3108  79 
('a,'b)~"*"~(infixr~20)}, which may express binary product types. 
324  80 

3108  81 
\item[$arities$] is a series of type arity declarations. Each assigns 
82 
arities to type constructors. The $name$ must be an existing type 

83 
constructor, which is given the additional arity $arity$. 

84 

85 
\item[$consts$] is a series of constant declarations. Each new 

86 
constant $name$ is given the specified type. The optional $mixfix$ 

87 
annotations may attach concrete syntax to the constant. 

88 

89 
\item[$syntax$] \index{*syntax section}\index{print mode} is a variant 

90 
of $consts$ which adds just syntax without actually declaring 

91 
logical constants. This gives full control over a theory's context 

3485
f27a30a18a17
Now there are TWO spaces after each full stop, so that the Emacs sentence
paulson
parents:
3201
diff
changeset

92 
free grammar. The optional $mode$ specifies the print mode where the 
f27a30a18a17
Now there are TWO spaces after each full stop, so that the Emacs sentence
paulson
parents:
3201
diff
changeset

93 
mixfix productions should be added. If there is no \texttt{output} 
3108  94 
option given, all productions are also added to the input syntax 
95 
(regardless of the print mode). 

324  96 

97 
\item[$mixfix$] \index{mixfix declarations} 

98 
annotations can take three forms: 

273  99 
\begin{itemize} 
100 
\item A mixfix template given as a $string$ of the form 

101 
{\tt"}\dots{\tt\_}\dots{\tt\_}\dots{\tt"} where the $i$th underscore 

324  102 
indicates the position where the $i$th argument should go. The list 
103 
of numbers gives the priority of each argument. The final number gives 

104 
the priority of the whole construct. 

104  105 

324  106 
\item A constant $f$ of type $\tau@1\To(\tau@2\To\tau)$ can be given {\bf 
107 
infix} status. 

104  108 

324  109 
\item A constant $f$ of type $(\tau@1\To\tau@2)\To\tau$ can be given {\bf 
110 
binder} status. The declaration {\tt binder} $\cal Q$ $p$ causes 

286  111 
${\cal Q}\,x.F(x)$ to be treated 
112 
like $f(F)$, where $p$ is the priority. 

273  113 
\end{itemize} 
324  114 

864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset

115 
\item[$trans$] 
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset

116 
specifies syntactic translation rules (macros). There are three forms: 
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset

117 
parse rules ({\tt =>}), print rules ({\tt <=}), and parse/print rules ({\tt 
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset

118 
==}). 
324  119 

1650  120 
\item[$rules$] 
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset

121 
is a series of rule declarations. Each has a name $id$ and the formula is 
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset

122 
given by the $string$. Rule names must be distinct within any single 
3108  123 
theory. 
324  124 

1905  125 
\item[$defs$] is a series of definitions. They are just like $rules$, except 
126 
that every $string$ must be a definition (see below for details). 

1650  127 

128 
\item[$constdefs$] combines the declaration of constants and their 

3485
f27a30a18a17
Now there are TWO spaces after each full stop, so that the Emacs sentence
paulson
parents:
3201
diff
changeset

129 
definition. The first $string$ is the type, the second the definition. 
3108  130 

131 
\item[$axclass$] \index{*axclass section} defines an 

132 
\rmindex{axiomatic type class} as the intersection of existing 

3485
f27a30a18a17
Now there are TWO spaces after each full stop, so that the Emacs sentence
paulson
parents:
3201
diff
changeset

133 
classes, with additional axioms holding. Class axioms may not 
f27a30a18a17
Now there are TWO spaces after each full stop, so that the Emacs sentence
paulson
parents:
3201
diff
changeset

134 
contain more than one type variable. The class axioms (with implicit 
3108  135 
sort constraints added) are bound to the given names. Furthermore a 
136 
class introduction rule is generated, which is automatically 

137 
employed by $instance$ to prove instantiations of this class. 

138 

139 
\item[$instance$] \index{*instance section} proves class inclusions or 

140 
type arities at the logical level and then transfers these to the 

3485
f27a30a18a17
Now there are TWO spaces after each full stop, so that the Emacs sentence
paulson
parents:
3201
diff
changeset

141 
type signature. The instantiation is proven and checked properly. 
3108  142 
The user has to supply sufficient witness information: theorems 
143 
($longident$), axioms ($string$), or even arbitrary \ML{} tactic 

144 
code $verbatim$. 

1650  145 

1846  146 
\item[$oracle$] links the theory to a trusted external reasoner. It is 
147 
allowed to create theorems, but each theorem carries a proof object 

148 
describing the oracle invocation. See \S\ref{sec:oracles} for details. 

149 

324  150 
\item[$ml$] \index{*ML section} 
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset

151 
consists of \ML\ code, typically for parse and print translation functions. 
104  152 
\end{description} 
324  153 
% 
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset

154 
Chapters~\ref{DefiningLogics} and \ref{chap:syntax} explain mixfix 
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset

155 
declarations, translation rules and the {\tt ML} section in more detail. 
145  156 

157 

1905  158 
\subsection{Definitions}\indexbold{definitions} 
159 

3485
f27a30a18a17
Now there are TWO spaces after each full stop, so that the Emacs sentence
paulson
parents:
3201
diff
changeset

160 
{\bf Definitions} are intended to express abbreviations. The simplest 
3108  161 
form of a definition is $f \equiv t$, where $f$ is a constant. 
162 
Isabelle also allows a derived forms where the arguments of~$f$ appear 

163 
on the left, abbreviating a string of $\lambda$abstractions. 

1905  164 

165 
Isabelle makes the following checks on definitions: 

166 
\begin{itemize} 

3108  167 
\item Arguments (on the lefthand side) must be distinct variables. 
1905  168 
\item All variables on the righthand side must also appear on the lefthand 
169 
side. 

3108  170 
\item All type variables on the righthand side must also appear on 
171 
the lefthand side; this prohibits definitions such as {\tt 

172 
(zero::nat) == length ([]::'a list)}. 

1905  173 
\item The definition must not be recursive. Most objectlogics provide 
174 
definitional principles that can be used to express recursion safely. 

175 
\end{itemize} 

176 
These checks are intended to catch the sort of errors that might be made 

177 
accidentally. Misspellings, for instance, might result in additional 

178 
variables appearing on the righthand side. More elaborate checks could be 

179 
made, but the cost might be overly strict rules on declaration order, etc. 

180 

181 

275  182 
\subsection{*Classes and arities} 
324  183 
\index{classes!context conditions}\index{arities!context conditions} 
145  184 

286  185 
In order to guarantee principal types~\cite{nipkowprehofer}, 
324  186 
arity declarations must obey two conditions: 
145  187 
\begin{itemize} 
3108  188 
\item There must not be any two declarations $ty :: (\vec{r})c$ and 
189 
$ty :: (\vec{s})c$ with $\vec{r} \neq \vec{s}$. For example, this 

190 
excludes the following: 

145  191 
\begin{ttbox} 
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset

192 
arities 
3108  193 
foo :: ({\ttlbrace}logic{\ttrbrace}) logic 
194 
foo :: ({\ttlbrace}{\ttrbrace})logic 

145  195 
\end{ttbox} 
286  196 

145  197 
\item If there are two declarations $ty :: (s@1,\dots,s@n)c$ and $ty :: 
198 
(s@1',\dots,s@n')c'$ such that $c' < c$ then $s@i' \preceq s@i$ must hold 

199 
for $i=1,\dots,n$. The relationship $\preceq$, defined as 

200 
\[ s' \preceq s \iff \forall c\in s. \exists c'\in s'.~ c'\le c, \] 

3108  201 
expresses that the set of types represented by $s'$ is a subset of the 
202 
set of types represented by $s$. Assuming $term \preceq logic$, the 

203 
following is forbidden: 

145  204 
\begin{ttbox} 
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset

205 
arities 
3108  206 
foo :: ({\ttlbrace}logic{\ttrbrace})logic 
207 
foo :: ({\ttlbrace}{\ttrbrace})term 

145  208 
\end{ttbox} 
286  209 

145  210 
\end{itemize} 
211 

104  212 

324  213 
\section{Loading a new theory}\label{LoadingTheories} 
214 
\index{theories!loading}\index{files!reading} 

864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset

215 
\begin{ttbox} 
286  216 
use_thy : string > unit 
217 
time_use_thy : string > unit 

218 
loadpath : string list ref \hfill{\bf initially {\tt["."]}} 

219 
delete_tmpfiles : bool ref \hfill{\bf initially true} 

220 
\end{ttbox} 

221 

324  222 
\begin{ttdescription} 
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset

223 
\item[\ttindexbold{use_thy} $thyname$] 
286  224 
reads the theory $thyname$ and creates an \ML{} structure as described below. 
275  225 

864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset

226 
\item[\ttindexbold{time_use_thy} $thyname$] 
286  227 
calls {\tt use_thy} $thyname$ and reports the time taken. 
138
9ba8bff1addc
added chapter "Defining Theories" and made changes for new Readthy functions
clasohm
parents:
104
diff
changeset

228 

864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset

229 
\item[\ttindexbold{loadpath}] 
286  230 
contains a list of directories to search when locating the files that 
231 
define a theory. This list is only used if the theory name in {\tt 

232 
use_thy} does not specify the path explicitly. 

233 

4317  234 
\item[reset \ttindexbold{delete_tmpfiles};] 
286  235 
suppresses the deletion of temporary files. 
324  236 
\end{ttdescription} 
286  237 
% 
3108  238 
Each theory definition must reside in a separate file. Let the file 
239 
{\it T}{\tt.thy} contain the definition of a theory called~$T$, whose 

240 
parent theories are $TB@1$ \dots $TB@n$. Calling 

241 
\ttindex{use_thy}~{\tt"{\it T\/}"} reads the file {\it T}{\tt.thy}, 

242 
writes a temporary \ML{} file {\tt.{\it T}.thy.ML}, and reads the 

243 
latter file. Recursive {\tt use_thy} calls load those parent theories 

244 
that have not been loaded previously; the recursive calls may continue 

245 
to any depth. One {\tt use_thy} call can read an entire logic 

246 
provided all theories are linked appropriately. 

138
9ba8bff1addc
added chapter "Defining Theories" and made changes for new Readthy functions
clasohm
parents:
104
diff
changeset

247 

4317  248 
The result is an \ML\ structure~$T$ containing at least a component 
249 
{\tt thy} for the new theory and components for each of the rules. 

250 
The structure also contains the definitions of the {\tt ML} section, 

251 
if present. The file {\tt.{\it T}.thy.ML} is then deleted if {\tt 

252 
delete_tmpfiles} is set and no errors occurred. 

138
9ba8bff1addc
added chapter "Defining Theories" and made changes for new Readthy functions
clasohm
parents:
104
diff
changeset

253 

4317  254 
Finally the file {\it T}{\tt.ML} is read, if it exists. The structure 
255 
$T$ is automatically open in this context. Proof scripts typically 

256 
refer to its components by unqualified names. 

332  257 

864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset

258 
Some applications construct theories directly by calling \ML\ functions. In 
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset

259 
this situation there is no {\tt.thy} file, only an {\tt.ML} file. The 
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset

260 
{\tt.ML} file must declare an \ML\ structure having the theory's name and a 
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset

261 
component {\tt thy} containing the new theory object. 
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset

262 
Section~\ref{sec:pseudotheories} below describes a way of linking such 
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset

263 
theories to their parents. 
324  264 

265 
\begin{warn} 

864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset

266 
Temporary files are written to the current directory, so this must be 
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset

267 
writable. Isabelle inherits the current directory from the operating 
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset

268 
system; you can change it within Isabelle by typing {\tt 
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset

269 
cd"$dir$"}\index{*cd}. 
273  270 
\end{warn} 
138
9ba8bff1addc
added chapter "Defining Theories" and made changes for new Readthy functions
clasohm
parents:
104
diff
changeset

271 

9ba8bff1addc
added chapter "Defining Theories" and made changes for new Readthy functions
clasohm
parents:
104
diff
changeset

272 

324  273 
\section{Reloading modified theories}\label{sec:reloadingtheories} 
274 
\indexbold{theories!reloading} 

864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset

275 
\begin{ttbox} 
286  276 
update : unit > unit 
277 
unlink_thy : string > unit 

278 
\end{ttbox} 

332  279 
Changing a theory on disk often makes it necessary to reload all theories 
280 
descended from it. However, {\tt use_thy} reads only one theory, even if 

281 
some of the parent theories are out of date. In this case you should call 

282 
{\tt update()}. 

283 

286  284 
Isabelle keeps track of all loaded theories and their files. If 
285 
\ttindex{use_thy} finds that the theory to be loaded has been read before, 

286 
it determines whether to reload the theory as follows. First it looks for 

287 
the theory's files in their previous location. If it finds them, it 

288 
compares their modification times to the internal data and stops if they 

289 
are equal. If the files have been moved, {\tt use_thy} searches for them 

290 
as it would for a new theory. After {\tt use_thy} reloads a theory, it 

291 
marks the children as outofdate. 

292 

324  293 
\begin{ttdescription} 
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset

294 
\item[\ttindexbold{update}()] 
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset

295 
reloads all modified theories and their descendants in the correct order. 
138
9ba8bff1addc
added chapter "Defining Theories" and made changes for new Readthy functions
clasohm
parents:
104
diff
changeset

296 

286  297 
\item[\ttindexbold{unlink_thy} $thyname$]\indexbold{theories!removing} 
298 
informs Isabelle that theory $thyname$ no longer exists. If you delete the 

299 
theory files for $thyname$ then you must execute {\tt unlink_thy}; 

300 
otherwise {\tt update} will complain about a missing file. 

324  301 
\end{ttdescription} 
286  302 

303 

332  304 
\subsection{*Pseudo theories}\label{sec:pseudotheories} 
305 
\indexbold{theories!pseudo}% 

275  306 
Any automatic reloading facility requires complete knowledge of all 
286  307 
dependencies. Sometimes theories depend on objects created in \ML{} files 
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset

308 
with no associated theory definition file. These objects may be theories but 
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset

309 
they could also be theorems, proof procedures, etc. 
332  310 

311 
Unless such dependencies are documented, {\tt update} fails to reload these 

312 
\ML{} files and the system is left in a state where some objects, such as 

313 
theorems, still refer to old versions of theories. This may lead to the 

314 
error 

275  315 
\begin{ttbox} 
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset

316 
Attempt to merge different versions of theories: \dots 
275  317 
\end{ttbox} 
324  318 
Therefore there is a way to link theories and {\bf orphaned} \ML{} files  
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset

319 
those not associated with a theory definition. 
138
9ba8bff1addc
added chapter "Defining Theories" and made changes for new Readthy functions
clasohm
parents:
104
diff
changeset

320 

324  321 
Let us assume we have an orphaned \ML{} file named {\tt orphan.ML} and a 
332  322 
theory~$B$ that depends on {\tt orphan.ML}  for example, {\tt B.ML} uses 
323 
theorems proved in {\tt orphan.ML}. Then {\tt B.thy} should 

864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset

324 
mention this dependency as follows: 
138
9ba8bff1addc
added chapter "Defining Theories" and made changes for new Readthy functions
clasohm
parents:
104
diff
changeset

325 
\begin{ttbox} 
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset

326 
B = \(\ldots\) + "orphan" + \(\ldots\) 
138
9ba8bff1addc
added chapter "Defining Theories" and made changes for new Readthy functions
clasohm
parents:
104
diff
changeset

327 
\end{ttbox} 
1369  328 
Quoted strings stand for theories which have to be loaded before the 
329 
current theory is read but which are not used in building the base of 

3485
f27a30a18a17
Now there are TWO spaces after each full stop, so that the Emacs sentence
paulson
parents:
3201
diff
changeset

330 
theory~$B$. Whenever {\tt orphan} changes and is reloaded, Isabelle 
1369  331 
knows that $B$ has to be updated, too. 
275  332 

1369  333 
Note that it's necessary for {\tt orphan} to declare a special ML 
3485
f27a30a18a17
Now there are TWO spaces after each full stop, so that the Emacs sentence
paulson
parents:
3201
diff
changeset

334 
object of type {\tt theory} which is present in all theories. This is 
1369  335 
normally achieved by adding the file {\tt orphan.thy} to make {\tt 
3485
f27a30a18a17
Now there are TWO spaces after each full stop, so that the Emacs sentence
paulson
parents:
3201
diff
changeset

336 
orphan} a {\bf pseudo theory}. A minimum version of {\tt orphan.thy} 
1369  337 
would be 
338 

339 
\begin{ttbox} 

340 
orphan = Pure 

341 
\end{ttbox} 

342 

3485
f27a30a18a17
Now there are TWO spaces after each full stop, so that the Emacs sentence
paulson
parents:
3201
diff
changeset

343 
which uses {\tt Pure} to make a dummy theory. Normally though the 
1369  344 
orphaned file has its own dependencies. If {\tt orphan.ML} depends on 
345 
theories or files $A@1$, \ldots, $A@n$, record this by creating the 

346 
pseudo theory in the following way: 

275  347 
\begin{ttbox} 
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset

348 
orphan = \(A@1\) + \(\ldots\) + \(A@n\) 
275  349 
\end{ttbox} 
1369  350 
The resulting theory ensures that {\tt update} reloads {\tt orphan} 
351 
whenever it reloads one of the $A@i$. 

138
9ba8bff1addc
added chapter "Defining Theories" and made changes for new Readthy functions
clasohm
parents:
104
diff
changeset

352 

3108  353 
For an extensive example of how this technique can be used to link 
354 
lots of theory files and load them by just a few {\tt use_thy} calls 

355 
see the sources of one of the major objectlogics (e.g.\ \ZF). 

138
9ba8bff1addc
added chapter "Defining Theories" and made changes for new Readthy functions
clasohm
parents:
104
diff
changeset

356 

104  357 

358 

866
2d3d020eef11
added documentation of bind_thm, qed, qed_goal, get_thm, thms_of
clasohm
parents:
864
diff
changeset

359 
\section{Basic operations on theories}\label{BasicOperationsOnTheories} 
4317  360 
\subsection{Retrieving axioms and theorems} 
324  361 
\index{theories!axioms of}\index{axioms!extracting} 
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset

362 
\index{theories!theorems of}\index{theorems!extracting} 
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset

363 
\begin{ttbox} 
4317  364 
get_axiom : theory > xstring > thm 
365 
get_thm : theory > xstring > thm 

366 
get_thms : theory > xstring > thm list 

367 
axioms_of : theory > (string * thm) list 

368 
thms_of : theory > (string * thm) list 

864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset

369 
assume_ax : theory > string > thm 
104  370 
\end{ttbox} 
324  371 
\begin{ttdescription} 
4317  372 
\item[\ttindexbold{get_axiom} $thy$ $name$] returns an axiom with the 
373 
given $name$ from $thy$ or any of its ancestors, raising exception 

374 
\xdx{THEORY} if none exists. Merging theories can cause several 

375 
axioms to have the same name; {\tt get_axiom} returns an arbitrary 

376 
one. Usually, axioms are also stored as theorems and may be 

377 
retrieved via \texttt{get_thm} as well. 

378 

379 
\item[\ttindexbold{get_thm} $thy$ $name$] is analogous to {\tt 

380 
get_axiom}, but looks for a theorem stored in the theory's 

381 
database. Like {\tt get_axiom} it searches all parents of a theory 

382 
if the theorem is not found directly in $thy$. 

383 

384 
\item[\ttindexbold{get_thms} $thy$ $name$] is like \texttt{get_thm} 

385 
for retrieving theorem lists stored within the theory. It returns a 

386 
singleton list if $name$ actually refers to a theorem rather than a 

387 
theorem list. 

388 

389 
\item[\ttindexbold{axioms_of} $thy$] returns the axioms of this theory 

390 
node, not including the ones of its ancestors. 

391 

392 
\item[\ttindexbold{thms_of} $thy$] returns all theorems stored within 

393 
the database of this theory node, not including the ones of its 

394 
ancestors. 

395 

396 
\item[\ttindexbold{assume_ax} $thy$ $formula$] reads the {\it formula} 

397 
using the syntax of $thy$, following the same conventions as axioms 

398 
in a theory definition. You can thus pretend that {\it formula} is 

399 
an axiom and use the resulting theorem like an axiom. Actually {\tt 

400 
assume_ax} returns an assumption; \ttindex{qed} and 

401 
\ttindex{result} complain about additional assumptions, but 

402 
\ttindex{uresult} does not. 

104  403 

404 
For example, if {\it formula} is 

332  405 
\hbox{\tt a=b ==> b=a} then the resulting theorem has the form 
406 
\hbox{\verb'?a=?b ==> ?b=?a [!!a b. a=b ==> b=a]'} 

324  407 
\end{ttdescription} 
104  408 

4384  409 

410 
\subsection{*Theory inclusion} 

411 
\begin{ttbox} 

412 
subthy : theory * theory > bool 

413 
eq_thy : theory * theory > bool 

414 
transfer : theory > thm > thm 

415 
transfer_sg : Sign.sg > thm > thm 

416 
\end{ttbox} 

417 

418 
Inclusion and equality of theories is determined by unique 

419 
identification stamps that are created when declaring new components. 

420 
Theorems contain a reference to the theory (actually to its signature) 

421 
they have been derived in. Transferring theorems to super theories 

422 
has no logical significance, but may affect some operations in subtle 

423 
ways (e.g.\ implicit merges of signatures when applying rules, or 

424 
pretty printing of theorems). 

425 

426 
\begin{ttdescription} 

427 

428 
\item[\ttindexbold{subthy} ($thy@1$, $thy@2$)] determines if $thy@1$ 

429 
is included in $thy@2$ wrt.\ identification stamps. 

430 

431 
\item[\ttindexbold{eq_thy} ($thy@1$, $thy@2$)] determines if $thy@1$ 

432 
is exactly the same as $thy@2$. 

433 

434 
\item[\ttindexbold{transfer} $thy$ $thm$] transfers theorem $thm$ to 

435 
theory $thy$, provided the latter includes the theory of $thm$. 

436 

437 
\item[\ttindexbold{transfer_sg} $sign$ $thm$] is similar to 

438 
\texttt{transfer}, but identifies the super theory via its 

439 
signature. 

440 

441 
\end{ttdescription} 

442 

443 

3108  444 
\subsection{*Building a theory} 
286  445 
\label{BuildingATheory} 
446 
\index{theories!constructingbold} 

864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset

447 
\begin{ttbox} 
4317  448 
ProtoPure.thy : theory 
3108  449 
Pure.thy : theory 
450 
CPure.thy : theory 

4317  451 
merge_theories : string > theory * theory > theory 
286  452 
\end{ttbox} 
3108  453 
\begin{description} 
4317  454 
\item[\ttindexbold{ProtoPure.thy}, \ttindexbold{Pure.thy}, 
455 
\ttindexbold{CPure.thy}] contain the syntax and signature of the 

456 
metalogic. There are basically no axioms: metalevel inferences 

457 
are carried out by \ML\ functions. \texttt{Pure} and \texttt{CPure} 

458 
just differ in their concrete syntax of prefix function application: 

459 
$t(u@1, \ldots, u@n)$ in \texttt{Pure} vs.\ $t\,u@1,\ldots\,u@n$ in 

460 
\texttt{CPure}. \texttt{ProtoPure} is their common parent, 

461 
containing no syntax for printing prefix applications at all! 

462 

463 
\item[\ttindexbold{merge_theories} $name$ ($thy@1$, $thy@2$)] merges 

464 
the two theories $thy@1$ and $thy@2$, creating a new named theory 

465 
node. The resulting theory contains all of the syntax, signature 

466 
and axioms of the constituent theories. Merging theories that 

467 
contain different identification stamps of the same name fails with 

864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset

468 
the following message 
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset

469 
\begin{ttbox} 
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset

470 
Attempt to merge different versions of theories: "\(T@1\)", \(\ldots\), "\(T@n\)" 
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset

471 
\end{ttbox} 
4317  472 
This error may especially occur when a theory is redeclared  say to 
473 
change an inappropriate definition  and bindings to old versions 

474 
persist. Isabelle ensures that old and new theories of the same name 

475 
are not involved in a proof. 

864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset

476 

d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset

477 
%% FIXME 
478  478 
%\item [\ttindexbold{extend_theory} $thy$ {\tt"}$T${\tt"} $\cdots$] extends 
479 
% the theory $thy$ with new types, constants, etc. $T$ identifies the theory 

480 
% internally. When a theory is redeclared, say to change an incorrect axiom, 

481 
% bindings to the old axiom may persist. Isabelle ensures that the old and 

482 
% new theories are not involved in the same proof. Attempting to combine 

483 
% different theories having the same name $T$ yields the fatal error 

484 
%extend_theory : theory > string > \(\cdots\) > theory 

864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset

485 
%\begin{ttbox} 
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset

486 
%Attempt to merge different versions of theory: \(T\) 
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset

487 
%\end{ttbox} 
3108  488 
\end{description} 
286  489 

864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset

490 
%% FIXME 
275  491 
%\item [\ttindexbold{extend_theory} $thy$ {\tt"}$T${\tt"} 
492 
% ($classes$, $default$, $types$, $arities$, $consts$, $sextopt$) $rules$] 

493 
%\hfill\break %%% include if line is just too short 

286  494 
%is the \ML{} equivalent of the following theory definition: 
275  495 
%\begin{ttbox} 
496 
%\(T\) = \(thy\) + 

497 
%classes \(c\) < \(c@1\),\(\dots\),\(c@m\) 

498 
% \dots 

499 
%default {\(d@1,\dots,d@r\)} 

500 
%types \(tycon@1\),\dots,\(tycon@i\) \(n\) 

501 
% \dots 

502 
%arities \(tycon@1'\),\dots,\(tycon@j'\) :: (\(s@1\),\dots,\(s@n\))\(c\) 

503 
% \dots 

504 
%consts \(b@1\),\dots,\(b@k\) :: \(\tau\) 

505 
% \dots 

506 
%rules \(name\) \(rule\) 

507 
% \dots 

508 
%end 

509 
%\end{ttbox} 

510 
%where 

511 
%\begin{tabular}[t]{l@{~=~}l} 

512 
%$classes$ & \tt[("$c$",["$c@1$",\dots,"$c@m$"]),\dots] \\ 

513 
%$default$ & \tt["$d@1$",\dots,"$d@r$"]\\ 

514 
%$types$ & \tt[([$tycon@1$,\dots,$tycon@i$], $n$),\dots] \\ 

515 
%$arities$ & \tt[([$tycon'@1$,\dots,$tycon'@j$], ([$s@1$,\dots,$s@n$],$c$)),\dots] 

516 
%\\ 

517 
%$consts$ & \tt[([$b@1$,\dots,$b@k$],$\tau$),\dots] \\ 

518 
%$rules$ & \tt[("$name$",$rule$),\dots] 

519 
%\end{tabular} 

104  520 

521 

864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset

522 
\subsection{Inspecting a theory}\label{sec:inspctthy} 
104  523 
\index{theories!inspectingbold} 
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset

524 
\begin{ttbox} 
4317  525 
print_syntax : theory > unit 
526 
print_theory : theory > unit 

527 
print_data : theory > string > unit 

528 
parents_of : theory > theory list 

529 
ancestors_of : theory > theory list 

530 
sign_of : theory > Sign.sg 

531 
Sign.stamp_names_of : Sign.sg > string list 

104  532 
\end{ttbox} 
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset

533 
These provide means of viewing a theory's components. 
324  534 
\begin{ttdescription} 
3108  535 
\item[\ttindexbold{print_syntax} $thy$] prints the syntax of $thy$ 
536 
(grammar, macros, translation functions etc., see 

537 
page~\pageref{pg:print_syn} for more details). 

538 

539 
\item[\ttindexbold{print_theory} $thy$] prints the logical parts of 

540 
$thy$, excluding the syntax. 

4317  541 

542 
\item[\ttindexbold{print_data} $thy$ $kind$] prints generic data of 

543 
$thy$. This invokes the print method associated with $kind$. Refer 

544 
to the output of \texttt{print_theory} for a list of available data 

545 
kinds in $thy$. 

546 

547 
\item[\ttindexbold{parents_of} $thy$] returns the direct ancestors 

548 
of~$thy$. 

549 

550 
\item[\ttindexbold{ancestors_of} $thy$] returns all ancestors of~$thy$ 

551 
(not including $thy$ itself). 

552 

553 
\item[\ttindexbold{sign_of} $thy$] returns the signature associated 

554 
with~$thy$. It is useful with functions like {\tt 

555 
read_instantiate_sg}, which take a signature as an argument. 

556 

557 
\item[\ttindexbold{Sign.stamp_names_of} $sg$]\index{signatures} 

558 
returns the names of the identification \rmindex{stamps} of ax 

559 
signature. These coincide with the names of its full ancestry 

560 
including that of $sg$ itself. 

104  561 

324  562 
\end{ttdescription} 
104  563 

1369  564 

104  565 
\section{Terms} 
566 
\index{termsbold} 

324  567 
Terms belong to the \ML\ type \mltydx{term}, which is a concrete datatype 
3108  568 
with six constructors: 
104  569 
\begin{ttbox} 
570 
type indexname = string * int; 

571 
infix 9 $; 

572 
datatype term = Const of string * typ 

573 
 Free of string * typ 

574 
 Var of indexname * typ 

575 
 Bound of int 

576 
 Abs of string * typ * term 

577 
 op $ of term * term; 

578 
\end{ttbox} 

324  579 
\begin{ttdescription} 
4317  580 
\item[\ttindexbold{Const} ($a$, $T$)] \index{constantsbold} 
286  581 
is the {\bf constant} with name~$a$ and type~$T$. Constants include 
582 
connectives like $\land$ and $\forall$ as well as constants like~0 

583 
and~$Suc$. Other constants may be required to define a logic's concrete 

864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset

584 
syntax. 
104  585 

4317  586 
\item[\ttindexbold{Free} ($a$, $T$)] \index{variables!freebold} 
324  587 
is the {\bf free variable} with name~$a$ and type~$T$. 
104  588 

4317  589 
\item[\ttindexbold{Var} ($v$, $T$)] \index{unknownsbold} 
324  590 
is the {\bf scheme variable} with indexname~$v$ and type~$T$. An 
591 
\mltydx{indexname} is a string paired with a nonnegative index, or 

592 
subscript; a term's scheme variables can be systematically renamed by 

593 
incrementing their subscripts. Scheme variables are essentially free 

594 
variables, but may be instantiated during unification. 

104  595 

324  596 
\item[\ttindexbold{Bound} $i$] \index{variables!boundbold} 
597 
is the {\bf bound variable} with de Bruijn index~$i$, which counts the 

598 
number of lambdas, starting from zero, between a variable's occurrence 

599 
and its binding. The representation prevents capture of variables. For 

600 
more information see de Bruijn \cite{debruijn72} or 

601 
Paulson~\cite[page~336]{paulson91}. 

104  602 

4317  603 
\item[\ttindexbold{Abs} ($a$, $T$, $u$)] 
324  604 
\index{lambda abs@$\lambda$abstractionsbold} 
605 
is the $\lambda${\bf abstraction} with body~$u$, and whose bound 

606 
variable has name~$a$ and type~$T$. The name is used only for parsing 

607 
and printing; it has no logical significance. 

104  608 

324  609 
\item[$t$ \$ $u$] \index{$@{\tt\$}bold} \index{function applicationsbold} 
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset

610 
is the {\bf application} of~$t$ to~$u$. 
324  611 
\end{ttdescription} 
286  612 
Application is written as an infix operator to aid readability. 
332  613 
Here is an \ML\ pattern to recognize \FOL{} formulae of 
104  614 
the form~$A\imp B$, binding the subformulae to~$A$ and~$B$: 
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset

615 
\begin{ttbox} 
104  616 
Const("Trueprop",_) $ (Const("op >",_) $ A $ B) 
617 
\end{ttbox} 

618 

619 

4317  620 
\section{*Variable binding} 
286  621 
\begin{ttbox} 
622 
loose_bnos : term > int list 

623 
incr_boundvars : int > term > term 

624 
abstract_over : term*term > term 

625 
variant_abs : string * typ * term > string * term 

4374  626 
aconv : term * term > bool\hfill{\bf infix} 
286  627 
\end{ttbox} 
628 
These functions are all concerned with the de Bruijn representation of 

629 
bound variables. 

324  630 
\begin{ttdescription} 
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset

631 
\item[\ttindexbold{loose_bnos} $t$] 
286  632 
returns the list of all dangling bound variable references. In 
633 
particular, {\tt Bound~0} is loose unless it is enclosed in an 

634 
abstraction. Similarly {\tt Bound~1} is loose unless it is enclosed in 

635 
at least two abstractions; if enclosed in just one, the list will contain 

636 
the number 0. A wellformed term does not contain any loose variables. 

637 

864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset

638 
\item[\ttindexbold{incr_boundvars} $j$] 
332  639 
increases a term's dangling bound variables by the offset~$j$. This is 
286  640 
required when moving a subterm into a context where it is enclosed by a 
641 
different number of abstractions. Bound variables with a matching 

642 
abstraction are unaffected. 

643 

864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset

644 
\item[\ttindexbold{abstract_over} $(v,t)$] 
286  645 
forms the abstraction of~$t$ over~$v$, which may be any wellformed term. 
646 
It replaces every occurrence of \(v\) by a {\tt Bound} variable with the 

647 
correct index. 

648 

864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset

649 
\item[\ttindexbold{variant_abs} $(a,T,u)$] 
286  650 
substitutes into $u$, which should be the body of an abstraction. 
651 
It replaces each occurrence of the outermost bound variable by a free 

652 
variable. The free variable has type~$T$ and its name is a variant 

332  653 
of~$a$ chosen to be distinct from all constants and from all variables 
286  654 
free in~$u$. 
655 

864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset

656 
\item[$t$ \ttindexbold{aconv} $u$] 
286  657 
tests whether terms~$t$ and~$u$ are \(\alpha\)convertible: identical up 
658 
to renaming of bound variables. 

659 
\begin{itemize} 

660 
\item 

661 
Two constants, {\tt Free}s, or {\tt Var}s are \(\alpha\)convertible 

662 
if their names and types are equal. 

663 
(Variables having the same name but different types are thus distinct. 

664 
This confusing situation should be avoided!) 

665 
\item 

666 
Two bound variables are \(\alpha\)convertible 

667 
if they have the same number. 

668 
\item 

669 
Two abstractions are \(\alpha\)convertible 

670 
if their bodies are, and their bound variables have the same type. 

671 
\item 

672 
Two applications are \(\alpha\)convertible 

673 
if the corresponding subterms are. 

674 
\end{itemize} 

675 

324  676 
\end{ttdescription} 
286  677 

864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset

678 
\section{Certified terms}\index{terms!certifiedbold}\index{signatures} 
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset

679 
A term $t$ can be {\bf certified} under a signature to ensure that every type 
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset

680 
in~$t$ is wellformed and every constant in~$t$ is a type instance of a 
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset

681 
constant declared in the signature. The term must be welltyped and its use 
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset

682 
of bound variables must be wellformed. Metarules such as {\tt forall_elim} 
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset

683 
take certified terms as arguments. 
104  684 

324  685 
Certified terms belong to the abstract type \mltydx{cterm}. 
104  686 
Elements of the type can only be created through the certification process. 
687 
In case of error, Isabelle raises exception~\ttindex{TERM}\@. 

688 

689 
\subsection{Printing terms} 

324  690 
\index{terms!printing of} 
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset

691 
\begin{ttbox} 
275  692 
string_of_cterm : cterm > string 
104  693 
Sign.string_of_term : Sign.sg > term > string 
694 
\end{ttbox} 

324  695 
\begin{ttdescription} 
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset

696 
\item[\ttindexbold{string_of_cterm} $ct$] 
104  697 
displays $ct$ as a string. 
698 

864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset

699 
\item[\ttindexbold{Sign.string_of_term} $sign$ $t$] 
104  700 
displays $t$ as a string, using the syntax of~$sign$. 
324  701 
\end{ttdescription} 
104  702 

703 
\subsection{Making and inspecting certified terms} 

864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset

704 
\begin{ttbox} 
275  705 
cterm_of : Sign.sg > term > cterm 
706 
read_cterm : Sign.sg > string * typ > cterm 

864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset

707 
cert_axm : Sign.sg > string * term > string * term 
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset

708 
read_axm : Sign.sg > string * string > string * term 
3108  709 
rep_cterm : cterm > {\ttlbrace}T:typ, t:term, sign:Sign.sg, maxidx:int\ttrbrace 
104  710 
\end{ttbox} 
324  711 
\begin{ttdescription} 
275  712 
\item[\ttindexbold{cterm_of} $sign$ $t$] \index{signatures} 
104  713 
certifies $t$ with respect to signature~$sign$. 
714 

864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset

715 
\item[\ttindexbold{read_cterm} $sign$ ($s$, $T$)] 
104  716 
reads the string~$s$ using the syntax of~$sign$, creating a certified term. 
717 
The term is checked to have type~$T$; this type also tells the parser what 

718 
kind of phrase to parse. 

719 

864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset

720 
\item[\ttindexbold{cert_axm} $sign$ ($name$, $t$)] 
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset

721 
certifies $t$ with respect to $sign$ as a metaproposition and converts all 
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset

722 
exceptions to an error, including the final message 
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset

723 
\begin{ttbox} 
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset

724 
The error(s) above occurred in axiom "\(name\)" 
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset

725 
\end{ttbox} 
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset

726 

d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset

727 
\item[\ttindexbold{read_axm} $sign$ ($name$, $s$)] 
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset

728 
similar to {\tt cert_axm}, but first reads the string $s$ using the syntax of 
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset

729 
$sign$. 
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset

730 

d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset

731 
\item[\ttindexbold{rep_cterm} $ct$] 
104  732 
decomposes $ct$ as a record containing its type, the term itself, its 
733 
signature, and the maximum subscript of its unknowns. The type and maximum 

734 
subscript are computed during certification. 

324  735 
\end{ttdescription} 
104  736 

737 

864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset

738 
\section{Types}\index{typesbold} 
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset

739 
Types belong to the \ML\ type \mltydx{typ}, which is a concrete datatype with 
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset

740 
three constructor functions. These correspond to type constructors, free 
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset

741 
type variables and schematic type variables. Types are classified by sorts, 
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset

742 
which are lists of classes (representing an intersection). A class is 
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset

743 
represented by a string. 
104  744 
\begin{ttbox} 
745 
type class = string; 

746 
type sort = class list; 

747 

748 
datatype typ = Type of string * typ list 

749 
 TFree of string * sort 

750 
 TVar of indexname * sort; 

751 

752 
infixr 5 >; 

864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset

753 
fun S > T = Type ("fun", [S, T]); 
104  754 
\end{ttbox} 
324  755 
\begin{ttdescription} 
4317  756 
\item[\ttindexbold{Type} ($a$, $Ts$)] \index{type constructorsbold} 
324  757 
applies the {\bf type constructor} named~$a$ to the type operands~$Ts$. 
758 
Type constructors include~\tydx{fun}, the binary function space 

759 
constructor, as well as nullary type constructors such as~\tydx{prop}. 

760 
Other type constructors may be introduced. In expressions, but not in 

761 
patterns, \hbox{\tt$S$>$T$} is a convenient shorthand for function 

762 
types. 

104  763 

4317  764 
\item[\ttindexbold{TFree} ($a$, $s$)] \index{type variablesbold} 
324  765 
is the {\bf type variable} with name~$a$ and sort~$s$. 
104  766 

4317  767 
\item[\ttindexbold{TVar} ($v$, $s$)] \index{type unknownsbold} 
324  768 
is the {\bf type unknown} with indexname~$v$ and sort~$s$. 
769 
Type unknowns are essentially free type variables, but may be 

770 
instantiated during unification. 

771 
\end{ttdescription} 

104  772 

773 

774 
\section{Certified types} 

775 
\index{types!certifiedbold} 

864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset

776 
Certified types, which are analogous to certified terms, have type 
275  777 
\ttindexbold{ctyp}. 
104  778 

779 
\subsection{Printing types} 

324  780 
\index{types!printing of} 
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset

781 
\begin{ttbox} 
275  782 
string_of_ctyp : ctyp > string 
104  783 
Sign.string_of_typ : Sign.sg > typ > string 
784 
\end{ttbox} 

324  785 
\begin{ttdescription} 
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset

786 
\item[\ttindexbold{string_of_ctyp} $cT$] 
104  787 
displays $cT$ as a string. 
788 

864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset

789 
\item[\ttindexbold{Sign.string_of_typ} $sign$ $T$] 
104  790 
displays $T$ as a string, using the syntax of~$sign$. 
324  791 
\end{ttdescription} 
104  792 

793 

794 
\subsection{Making and inspecting certified types} 

864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset

795 
\begin{ttbox} 
275  796 
ctyp_of : Sign.sg > typ > ctyp 
3108  797 
rep_ctyp : ctyp > {\ttlbrace}T: typ, sign: Sign.sg\ttrbrace 
104  798 
\end{ttbox} 
324  799 
\begin{ttdescription} 
275  800 
\item[\ttindexbold{ctyp_of} $sign$ $T$] \index{signatures} 
104  801 
certifies $T$ with respect to signature~$sign$. 
802 

864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset

803 
\item[\ttindexbold{rep_ctyp} $cT$] 
104  804 
decomposes $cT$ as a record containing the type itself and its signature. 
324  805 
\end{ttdescription} 
104  806 

1846  807 

4317  808 
\section{Oracles: calling trusted external reasoners} 
1846  809 
\label{sec:oracles} 
810 
\index{oracles(} 

811 

812 
Oracles allow Isabelle to take advantage of external reasoners such as 

813 
arithmetic decision procedures, model checkers, fast tautology checkers or 

814 
computer algebra systems. Invoked as an oracle, an external reasoner can 

815 
create arbitrary Isabelle theorems. It is your responsibility to ensure that 

816 
the external reasoner is as trustworthy as your application requires. 

817 
Isabelle's proof objects~(\S\ref{sec:proofObjects}) record how each theorem 

818 
depends upon oracle calls. 

819 

820 
\begin{ttbox} 

4317  821 
invoke_oracle : theory > xstring > Sign.sg * object > thm 
822 
Theory.add_oracle : bstring * (Sign.sg * object > term) > theory > theory 

1846  823 
\end{ttbox} 
824 
\begin{ttdescription} 

4317  825 
\item[\ttindexbold{invoke_oracle} $thy$ $name$ ($sign$, $data$)] 
826 
invokes the oracle $name$ of theory $thy$ passing the information 

827 
contained in the exception value $data$ and creating a theorem 

828 
having signature $sign$. Note that type \ttindex{object} is just an 

829 
abbreviation for \texttt{exn}. Errors arise if $thy$ does not have 

830 
an oracle called $name$, if the oracle rejects its arguments or if 

831 
its result is illtyped. 

832 

833 
\item[\ttindexbold{Theory.add_oracle} $name$ $fun$ $thy$] extends 

834 
$thy$ by oracle $fun$ called $name$. It is seldom called 

835 
explicitly, as there is concrete syntax for oracles in theory files. 

1846  836 
\end{ttdescription} 
837 

838 
A curious feature of {\ML} exceptions is that they are ordinary constructors. 

839 
The {\ML} type {\tt exn} is a datatype that can be extended at any time. (See 

840 
my {\em {ML} for the Working Programmer}~\cite{paulsonml2}, especially 

841 
page~136.) The oracle mechanism takes advantage of this to allow an oracle to 

842 
take any information whatever. 

843 

844 
There must be some way of invoking the external reasoner from \ML, either 

845 
because it is coded in {\ML} or via an operating system interface. Isabelle 

846 
expects the {\ML} function to take two arguments: a signature and an 

4317  847 
exception object. 
1846  848 
\begin{itemize} 
849 
\item The signature will typically be that of a desendant of the theory 

850 
declaring the oracle. The oracle will use it to distinguish constants from 

851 
variables, etc., and it will be attached to the generated theorems. 

852 

853 
\item The exception is used to pass arbitrary information to the oracle. This 

854 
information must contain a full description of the problem to be solved by 

855 
the external reasoner, including any additional information that might be 

856 
required. The oracle may raise the exception to indicate that it cannot 

857 
solve the specified problem. 

858 
\end{itemize} 

859 

4317  860 
A trivial example is provided in theory {\tt FOL/ex/IffOracle}. This 
861 
oracle generates tautologies of the form $P\bimp\cdots\bimp P$, with 

862 
an even number of $P$s. 

1846  863 

4317  864 
The \texttt{ML} section of \texttt{IffOracle.thy} begins by declaring 
865 
a few auxiliary functions (suppressed below) for creating the 

866 
tautologies. Then it declares a new exception constructor for the 

867 
information required by the oracle: here, just an integer. It finally 

868 
defines the oracle function itself. 

1846  869 
\begin{ttbox} 
4317  870 
exception IffOracleExn of int;\medskip 
871 
fun mk_iff_oracle (sign, IffOracleExn n) = 

872 
if n > 0 andalso n mod 2 = 0 

873 
then Trueprop $ mk_iff n 

874 
else raise IffOracleExn n; 

1846  875 
\end{ttbox} 
4317  876 
Observe the function's two arguments, the signature {\tt sign} and the 
877 
exception given as a pattern. The function checks its argument for 

878 
validity. If $n$ is positive and even then it creates a tautology 

879 
containing $n$ occurrences of~$P$. Otherwise it signals error by 

880 
raising its own exception (just by happy coincidence). Errors may be 

881 
signalled by other means, such as returning the theorem {\tt True}. 

882 
Please ensure that the oracle's result is correctly typed; Isabelle 

883 
will reject illtyped theorems by raising a cryptic exception at top 

884 
level. 

1846  885 

4317  886 
The \texttt{oracle} section of {\tt IffOracle.thy} installs above 
887 
\texttt{ML} function as follows: 

1846  888 
\begin{ttbox} 
4317  889 
IffOracle = FOL +\medskip 
890 
oracle 

891 
iff = mk_iff_oracle\medskip 

1846  892 
end 
893 
\end{ttbox} 

894 

4317  895 
Now in \texttt{IffOracle.ML} we first define a wrapper for invoking 
896 
the oracle: 

1846  897 
\begin{ttbox} 
4317  898 
fun iff_oracle n = 
899 
invoke_oracle IffOracle.thy "iff" (sign_of IffOracle.thy, IffOracleExn n); 

900 
\end{ttbox} 

901 

902 
Here are some example applications of the \texttt{iff} oracle. An 

903 
argument of 10 is allowed, but one of 5 is forbidden: 

904 
\begin{ttbox} 

905 
iff_oracle 10; 

1846  906 
{\out "P <> P <> P <> P <> P <> P <> P <> P <> P <> P" : thm} 
4317  907 
iff_oracle 5; 
1846  908 
{\out Exception IffOracleExn 5 raised} 
909 
\end{ttbox} 

910 

911 
\index{oracles)} 

104  912 
\index{theories)} 