author  paulson 
Wed, 07 Oct 1998 10:31:30 +0200  
changeset 5619  76a8c72e3fd4 
parent 5390  0c9e6d860485 
child 6568  b38bc78d9a9d 
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 

5369  85 
\item[$nonterminals$]\index{*nonterminal symbols} declares purely 
86 
syntactic types to be used as nonterminal symbols of the context 

87 
free grammar. 

88 

3108  89 
\item[$consts$] is a series of constant declarations. Each new 
90 
constant $name$ is given the specified type. The optional $mixfix$ 

91 
annotations may attach concrete syntax to the constant. 

92 

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

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

95 
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

96 
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

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

324  100 

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

102 
annotations can take three forms: 

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

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

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

108 
the priority of the whole construct. 

104  109 

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

104  112 

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

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

273  117 
\end{itemize} 
324  118 

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

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

120 
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

121 
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

122 
==}). 
324  123 

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

125 
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

126 
given by the $string$. Rule names must be distinct within any single 
3108  127 
theory. 
324  128 

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

1650  131 

132 
\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

133 
definition. The first $string$ is the type, the second the definition. 
3108  134 

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

136 
\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

137 
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

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

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

142 

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

144 
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

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

148 
code $verbatim$. 

1650  149 

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

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

4543  153 

5369  154 
\item[$local$, $global$] change the current name declaration mode. 
4543  155 
Initially, theories start in $local$ mode, causing all names of 
156 
types, constants, axioms etc.\ to be automatically qualified by the 

157 
theory name. Changing this to $global$ causes all names to be 

158 
declared as short base names only. 

159 

160 
The $local$ and $global$ declarations act like switches, affecting 

161 
all following theory sections until changed again explicitly. Also 

162 
note that the final state at the end of the theory will persist. In 

163 
particular, this determines how the names of theorems stored later 

164 
on are handled. 

5369  165 

166 
\item[$setup$]\index{*setup!theory} applies a list of ML functions to 

167 
the theory. The argument should denote a value of type 

168 
\texttt{(theory > theory) list}. Typically, ML packages are 

169 
initialized in this way. 

1846  170 

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

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

175 
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

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

178 

1905  179 
\subsection{Definitions}\indexbold{definitions} 
180 

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

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

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

1905  185 

186 
Isabelle makes the following checks on definitions: 

187 
\begin{itemize} 

3108  188 
\item Arguments (on the lefthand side) must be distinct variables. 
1905  189 
\item All variables on the righthand side must also appear on the lefthand 
190 
side. 

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

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

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

196 
\end{itemize} 

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

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

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

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

201 

202 

275  203 
\subsection{*Classes and arities} 
324  204 
\index{classes!context conditions}\index{arities!context conditions} 
145  205 

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

211 
excludes the following: 

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

213 
arities 
3108  214 
foo :: ({\ttlbrace}logic{\ttrbrace}) logic 
215 
foo :: ({\ttlbrace}{\ttrbrace})logic 

145  216 
\end{ttbox} 
286  217 

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

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

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

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

224 
following is forbidden: 

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

226 
arities 
3108  227 
foo :: ({\ttlbrace}logic{\ttrbrace})logic 
228 
foo :: ({\ttlbrace}{\ttrbrace})term 

145  229 
\end{ttbox} 
286  230 

145  231 
\end{itemize} 
232 

104  233 

324  234 
\section{Loading a new theory}\label{LoadingTheories} 
235 
\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

236 
\begin{ttbox} 
286  237 
use_thy : string > unit 
238 
time_use_thy : string > unit 

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

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

241 
\end{ttbox} 

242 

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

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

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

247 
\item[\ttindexbold{time_use_thy} $thyname$] 
286  248 
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

249 

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

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

253 
use_thy} does not specify the path explicitly. 

254 

4317  255 
\item[reset \ttindexbold{delete_tmpfiles};] 
286  256 
suppresses the deletion of temporary files. 
324  257 
\end{ttdescription} 
286  258 
% 
3108  259 
Each theory definition must reside in a separate file. Let the file 
260 
{\it T}{\tt.thy} contain the definition of a theory called~$T$, whose 

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

4543  262 
\texttt{use_thy}~{\tt"{\it T\/}"} reads the file {\it T}{\tt.thy}, 
3108  263 
writes a temporary \ML{} file {\tt.{\it T}.thy.ML}, and reads the 
264 
latter file. Recursive {\tt use_thy} calls load those parent theories 

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

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

267 
provided all theories are linked appropriately. 

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

268 

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

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

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

273 
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

274 

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

277 
refer to its components by unqualified names. 

332  278 

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

279 
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

280 
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

281 
{\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

282 
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

283 
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

284 
theories to their parents. 
324  285 

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

286 

324  287 
\section{Reloading modified theories}\label{sec:reloadingtheories} 
288 
\indexbold{theories!reloading} 

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

289 
\begin{ttbox} 
286  290 
update : unit > unit 
291 
unlink_thy : string > unit 

292 
\end{ttbox} 

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

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

296 
{\tt update()}. 

297 

286  298 
Isabelle keeps track of all loaded theories and their files. If 
4543  299 
\texttt{use_thy} finds that the theory to be loaded has been read 
300 
before, it determines whether to reload the theory as follows. First 

301 
it looks for the theory's files in their previous location. If it 

302 
finds them, it compares their modification times to the internal data 

303 
and stops if they are equal. If the files have been moved, {\tt 

304 
use_thy} searches for them as it would for a new theory. After {\tt 

305 
use_thy} reloads a theory, it marks the children as outofdate. 

286  306 

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

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

309 
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

310 

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

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

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

324  315 
\end{ttdescription} 
286  316 

317 

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

275  320 
Any automatic reloading facility requires complete knowledge of all 
286  321 
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

322 
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

323 
they could also be theorems, proof procedures, etc. 
332  324 

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

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

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

328 
error 

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

330 
Attempt to merge different versions of theories: \dots 
275  331 
\end{ttbox} 
324  332 
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

333 
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

334 

324  335 
Let us assume we have an orphaned \ML{} file named {\tt orphan.ML} and a 
332  336 
theory~$B$ that depends on {\tt orphan.ML}  for example, {\tt B.ML} uses 
337 
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

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

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

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

341 
\end{ttbox} 
1369  342 
Quoted strings stand for theories which have to be loaded before the 
343 
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

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

1369  347 
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

348 
object of type {\tt theory} which is present in all theories. This is 
1369  349 
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

350 
orphan} a {\bf pseudo theory}. A minimum version of {\tt orphan.thy} 
1369  351 
would be 
352 

353 
\begin{ttbox} 

354 
orphan = Pure 

355 
\end{ttbox} 

356 

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

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

360 
pseudo theory in the following way: 

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

362 
orphan = \(A@1\) + \(\ldots\) + \(A@n\) 
275  363 
\end{ttbox} 
1369  364 
The resulting theory ensures that {\tt update} reloads {\tt orphan} 
365 
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

366 

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

369 
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

370 

104  371 

372 

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

373 
\section{Basic operations on theories}\label{BasicOperationsOnTheories} 
4384  374 

375 
\subsection{*Theory inclusion} 

376 
\begin{ttbox} 

377 
subthy : theory * theory > bool 

378 
eq_thy : theory * theory > bool 

379 
transfer : theory > thm > thm 

380 
transfer_sg : Sign.sg > thm > thm 

381 
\end{ttbox} 

382 

383 
Inclusion and equality of theories is determined by unique 

384 
identification stamps that are created when declaring new components. 

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

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

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

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

389 
pretty printing of theorems). 

390 

391 
\begin{ttdescription} 

392 

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

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

395 

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

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

398 

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

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

401 

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

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

404 
signature. 

405 

406 
\end{ttdescription} 

407 

408 

3108  409 
\subsection{*Building a theory} 
286  410 
\label{BuildingATheory} 
411 
\index{theories!constructingbold} 

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

412 
\begin{ttbox} 
4317  413 
ProtoPure.thy : theory 
3108  414 
Pure.thy : theory 
415 
CPure.thy : theory 

4317  416 
merge_theories : string > theory * theory > theory 
286  417 
\end{ttbox} 
3108  418 
\begin{description} 
4317  419 
\item[\ttindexbold{ProtoPure.thy}, \ttindexbold{Pure.thy}, 
420 
\ttindexbold{CPure.thy}] contain the syntax and signature of the 

421 
metalogic. There are basically no axioms: metalevel inferences 

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

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

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

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

426 
containing no syntax for printing prefix applications at all! 

427 

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

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

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

431 
and axioms of the constituent theories. Merging theories that 

432 
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

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

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

435 
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

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

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

440 
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

441 

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

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

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

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

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

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

449 
%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

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

451 
%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

452 
%\end{ttbox} 
3108  453 
\end{description} 
286  454 

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

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

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

286  459 
%is the \ML{} equivalent of the following theory definition: 
275  460 
%\begin{ttbox} 
461 
%\(T\) = \(thy\) + 

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

463 
% \dots 

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

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

466 
% \dots 

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

468 
% \dots 

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

470 
% \dots 

471 
%rules \(name\) \(rule\) 

472 
% \dots 

473 
%end 

474 
%\end{ttbox} 

475 
%where 

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

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

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

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

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

481 
%\\ 

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

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

484 
%\end{tabular} 

104  485 

486 

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

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

489 
\begin{ttbox} 
4317  490 
print_syntax : theory > unit 
491 
print_theory : theory > unit 

492 
parents_of : theory > theory list 

493 
ancestors_of : theory > theory list 

494 
sign_of : theory > Sign.sg 

495 
Sign.stamp_names_of : Sign.sg > string list 

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

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

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

502 

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

504 
$thy$, excluding the syntax. 

4317  505 

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

507 
of~$thy$. 

508 

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

510 
(not including $thy$ itself). 

511 

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

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

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

515 

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

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

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

519 
including that of $sg$ itself. 

104  520 

324  521 
\end{ttdescription} 
104  522 

1369  523 

104  524 
\section{Terms} 
525 
\index{termsbold} 

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

530 
infix 9 $; 

531 
datatype term = Const of string * typ 

532 
 Free of string * typ 

533 
 Var of indexname * typ 

534 
 Bound of int 

535 
 Abs of string * typ * term 

536 
 op $ of term * term; 

537 
\end{ttbox} 

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

542 
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

543 
syntax. 
104  544 

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

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

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

552 
incrementing their subscripts. Scheme variables are essentially free 

553 
variables, but may be instantiated during unification. 

104  554 

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

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

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

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

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

104  561 

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

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

566 
and printing; it has no logical significance. 

104  567 

324  568 
\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

569 
is the {\bf application} of~$t$ to~$u$. 
324  570 
\end{ttdescription} 
286  571 
Application is written as an infix operator to aid readability. 
332  572 
Here is an \ML\ pattern to recognize \FOL{} formulae of 
104  573 
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

574 
\begin{ttbox} 
104  575 
Const("Trueprop",_) $ (Const("op >",_) $ A $ B) 
576 
\end{ttbox} 

577 

578 

4317  579 
\section{*Variable binding} 
286  580 
\begin{ttbox} 
581 
loose_bnos : term > int list 

582 
incr_boundvars : int > term > term 

583 
abstract_over : term*term > term 

584 
variant_abs : string * typ * term > string * term 

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

588 
bound variables. 

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

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

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

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

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

596 

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

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

601 
abstraction are unaffected. 

602 

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

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

606 
correct index. 

607 

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

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

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

332  612 
of~$a$ chosen to be distinct from all constants and from all variables 
286  613 
free in~$u$. 
614 

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

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

618 
\begin{itemize} 

619 
\item 

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

621 
if their names and types are equal. 

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

623 
This confusing situation should be avoided!) 

624 
\item 

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

626 
if they have the same number. 

627 
\item 

628 
Two abstractions are \(\alpha\)convertible 

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

630 
\item 

631 
Two applications are \(\alpha\)convertible 

632 
if the corresponding subterms are. 

633 
\end{itemize} 

634 

324  635 
\end{ttdescription} 
286  636 

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

637 
\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

638 
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

639 
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

640 
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

641 
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

642 
take certified terms as arguments. 
104  643 

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

647 

648 
\subsection{Printing terms} 

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

650 
\begin{ttbox} 
275  651 
string_of_cterm : cterm > string 
104  652 
Sign.string_of_term : Sign.sg > term > string 
653 
\end{ttbox} 

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

655 
\item[\ttindexbold{string_of_cterm} $ct$] 
104  656 
displays $ct$ as a string. 
657 

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

658 
\item[\ttindexbold{Sign.string_of_term} $sign$ $t$] 
104  659 
displays $t$ as a string, using the syntax of~$sign$. 
324  660 
\end{ttdescription} 
104  661 

662 
\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

663 
\begin{ttbox} 
4543  664 
cterm_of : Sign.sg > term > cterm 
665 
read_cterm : Sign.sg > string * typ > cterm 

666 
cert_axm : Sign.sg > string * term > string * term 

667 
read_axm : Sign.sg > string * string > string * term 

668 
rep_cterm : cterm > {\ttlbrace}T:typ, t:term, sign:Sign.sg, maxidx:int\ttrbrace 

669 
Sign.certify_term : Sign.sg > term > term * typ * int 

104  670 
\end{ttbox} 
324  671 
\begin{ttdescription} 
4543  672 

673 
\item[\ttindexbold{cterm_of} $sign$ $t$] \index{signatures} certifies 

674 
$t$ with respect to signature~$sign$. 

675 

676 
\item[\ttindexbold{read_cterm} $sign$ ($s$, $T$)] reads the string~$s$ 

677 
using the syntax of~$sign$, creating a certified term. The term is 

678 
checked to have type~$T$; this type also tells the parser what kind 

679 
of phrase to parse. 

680 

681 
\item[\ttindexbold{cert_axm} $sign$ ($name$, $t$)] certifies $t$ with 

682 
respect to $sign$ as a metaproposition and converts all exceptions 

683 
to an error, including the final message 

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

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

685 
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

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

687 

4543  688 
\item[\ttindexbold{read_axm} $sign$ ($name$, $s$)] similar to {\tt 
689 
cert_axm}, but first reads the string $s$ using the syntax of 

690 
$sign$. 

691 

692 
\item[\ttindexbold{rep_cterm} $ct$] decomposes $ct$ as a record 

693 
containing its type, the term itself, its signature, and the maximum 

694 
subscript of its unknowns. The type and maximum subscript are 

695 
computed during certification. 

696 

697 
\item[\ttindexbold{Sign.certify_term}] is a more primitive version of 

698 
\texttt{cterm_of}, returning the internal representation instead of 

699 
an abstract \texttt{cterm}. 

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

700 

324  701 
\end{ttdescription} 
104  702 

703 

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

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

705 
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

706 
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

707 
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

708 
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

709 
represented by a string. 
104  710 
\begin{ttbox} 
711 
type class = string; 

712 
type sort = class list; 

713 

714 
datatype typ = Type of string * typ list 

715 
 TFree of string * sort 

716 
 TVar of indexname * sort; 

717 

718 
infixr 5 >; 

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

719 
fun S > T = Type ("fun", [S, T]); 
104  720 
\end{ttbox} 
324  721 
\begin{ttdescription} 
4317  722 
\item[\ttindexbold{Type} ($a$, $Ts$)] \index{type constructorsbold} 
324  723 
applies the {\bf type constructor} named~$a$ to the type operands~$Ts$. 
724 
Type constructors include~\tydx{fun}, the binary function space 

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

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

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

728 
types. 

104  729 

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

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

736 
instantiated during unification. 

737 
\end{ttdescription} 

104  738 

739 

740 
\section{Certified types} 

741 
\index{types!certifiedbold} 

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

742 
Certified types, which are analogous to certified terms, have type 
275  743 
\ttindexbold{ctyp}. 
104  744 

745 
\subsection{Printing types} 

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

747 
\begin{ttbox} 
275  748 
string_of_ctyp : ctyp > string 
104  749 
Sign.string_of_typ : Sign.sg > typ > string 
750 
\end{ttbox} 

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

752 
\item[\ttindexbold{string_of_ctyp} $cT$] 
104  753 
displays $cT$ as a string. 
754 

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

755 
\item[\ttindexbold{Sign.string_of_typ} $sign$ $T$] 
104  756 
displays $T$ as a string, using the syntax of~$sign$. 
324  757 
\end{ttdescription} 
104  758 

759 

760 
\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

761 
\begin{ttbox} 
4543  762 
ctyp_of : Sign.sg > typ > ctyp 
763 
rep_ctyp : ctyp > {\ttlbrace}T: typ, sign: Sign.sg\ttrbrace 

764 
Sign.certify_typ : Sign.sg > typ > typ 

104  765 
\end{ttbox} 
324  766 
\begin{ttdescription} 
4543  767 

768 
\item[\ttindexbold{ctyp_of} $sign$ $T$] \index{signatures} certifies 

769 
$T$ with respect to signature~$sign$. 

770 

771 
\item[\ttindexbold{rep_ctyp} $cT$] decomposes $cT$ as a record 

772 
containing the type itself and its signature. 

773 

774 
\item[\ttindexbold{Sign.certify_typ}] is a more primitive version of 

775 
\texttt{ctyp_of}, returning the internal representation instead of 

776 
an abstract \texttt{ctyp}. 

104  777 

324  778 
\end{ttdescription} 
104  779 

1846  780 

4317  781 
\section{Oracles: calling trusted external reasoners} 
1846  782 
\label{sec:oracles} 
783 
\index{oracles(} 

784 

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

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

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

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

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

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

791 
depends upon oracle calls. 

792 

793 
\begin{ttbox} 

4317  794 
invoke_oracle : theory > xstring > Sign.sg * object > thm 
4597
a0bdee64194c
Fixed a lot of overfull and underfull lines (hboxes)
paulson
parents:
4543
diff
changeset

795 
Theory.add_oracle : bstring * (Sign.sg * object > term) > theory 
a0bdee64194c
Fixed a lot of overfull and underfull lines (hboxes)
paulson
parents:
4543
diff
changeset

796 
> theory 
1846  797 
\end{ttbox} 
798 
\begin{ttdescription} 

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

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

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

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

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

805 
its result is illtyped. 

806 

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

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

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

1846  810 
\end{ttdescription} 
811 

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

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

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

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

816 
take any information whatever. 

817 

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

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

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

4317  821 
exception object. 
1846  822 
\begin{itemize} 
823 
\item The signature will typically be that of a desendant of the theory 

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

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

826 

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

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

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

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

831 
solve the specified problem. 

832 
\end{itemize} 

833 

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

836 
an even number of $P$s. 

1846  837 

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

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

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

842 
defines the oracle function itself. 

1846  843 
\begin{ttbox} 
4317  844 
exception IffOracleExn of int;\medskip 
845 
fun mk_iff_oracle (sign, IffOracleExn n) = 

846 
if n > 0 andalso n mod 2 = 0 

847 
then Trueprop $ mk_iff n 

848 
else raise IffOracleExn n; 

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

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

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

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

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

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

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

858 
level. 

1846  859 

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

1846  862 
\begin{ttbox} 
4317  863 
IffOracle = FOL +\medskip 
864 
oracle 

865 
iff = mk_iff_oracle\medskip 

1846  866 
end 
867 
\end{ttbox} 

868 

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

1846  871 
\begin{ttbox} 
4597
a0bdee64194c
Fixed a lot of overfull and underfull lines (hboxes)
paulson
parents:
4543
diff
changeset

872 
fun iff_oracle n = invoke_oracle IffOracle.thy "iff" 
a0bdee64194c
Fixed a lot of overfull and underfull lines (hboxes)
paulson
parents:
4543
diff
changeset

873 
(sign_of IffOracle.thy, IffOracleExn n); 
4317  874 
\end{ttbox} 
875 

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

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

878 
\begin{ttbox} 

879 
iff_oracle 10; 

1846  880 
{\out "P <> P <> P <> P <> P <> P <> P <> P <> P <> P" : thm} 
4317  881 
iff_oracle 5; 
1846  882 
{\out Exception IffOracleExn 5 raised} 
883 
\end{ttbox} 

884 

885 
\index{oracles)} 

104  886 
\index{theories)} 
5369  887 

888 

889 
%%% Local Variables: 

890 
%%% mode: latex 

891 
%%% TeXmaster: "ref" 

892 
%%% End: 