author  wenzelm 
Wed, 25 Aug 1999 20:49:02 +0200  
changeset 7357  d0e16da40ea2 
parent 7168  741dc2a434b7 
child 7440  c1829208180f 
permissions  rwrr 
3201  1 

104  2 
%% $Id$ 
145  3 

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

6669  6 
\index{reading!axiomssee{\texttt{assume_ax}}} Theories organize the 
3108  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 

6571  30 
Theories are defined via theory files $name$\texttt{.thy} (there are also 
31 
\MLlevel interfaces which are only intended for people building advanced 

32 
theory definition packages). Appendix~\ref{app:TheorySyntax} presents the 

33 
concrete syntax for theory files; here follows an explanation of the 

34 
constituent parts. 

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

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

3108  38 
theories}\indexbold{theories!parent}, possibly extended with new 
6568  39 
components. \thydx{Pure} and \thydx{CPure} are the basic theories, which 
40 
contain only the metalogic. They differ just in their concrete syntax for 

41 
function applications. 

6571  42 

43 
The new theory begins as a merge of its parents. 

44 
\begin{ttbox} 

45 
Attempt to merge different versions of theories: "\(T@1\)", \(\ldots\), "\(T@n\)" 

46 
\end{ttbox} 

47 
This error may especially occur when a theory is redeclared  say to 

48 
change an inappropriate definition  and bindings to old versions persist. 

49 
Isabelle ensures that old and new theories of the same name are not involved 

50 
in a proof. 

324  51 

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

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

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

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

6669  57 
necessary to declare \texttt{c < e} in addition to \texttt{c < d} and \texttt{d < 
324  58 
e}. 
59 

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

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

61 
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

62 
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

63 
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

64 
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

65 
intersection). 
3108  66 

7168  67 
\item[$sort$] is a finite set of classes. A single class $id$ abbreviates the 
68 
sort $\{id\}$. 

324  69 

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

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

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

74 
indicate the number~$n$. 

75 

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

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

79 

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

80 
\item[$infix$] 
324  81 
declares a type or constant to be an infix operator of priority $nat$ 
6669  82 
associating to the left (\texttt{infixl}) or right (\texttt{infixr}). Only 
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset

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

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

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

89 

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

92 
free grammar. 

93 

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

96 
annotations may attach concrete syntax to the constant. 

97 

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

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

100 
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

101 
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

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

324  105 

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

107 
annotations can take three forms: 

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

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

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

113 
the priority of the whole construct. 

104  114 

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

104  117 

324  118 
\item A constant $f$ of type $(\tau@1\To\tau@2)\To\tau$ can be given {\bf 
6669  119 
binder} status. The declaration \texttt{binder} $\cal Q$ $p$ causes 
286  120 
${\cal Q}\,x.F(x)$ to be treated 
121 
like $f(F)$, where $p$ is the priority. 

273  122 
\end{itemize} 
324  123 

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

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

125 
specifies syntactic translation rules (macros). There are three forms: 
6669  126 
parse rules (\texttt{=>}), print rules (\texttt{<=}), and parse/print rules ({\tt 
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset

127 
==}). 
324  128 

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

130 
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

131 
given by the $string$. Rule names must be distinct within any single 
3108  132 
theory. 
324  133 

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

1650  136 

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

138 
definition. The first $string$ is the type, the second the definition. 
3108  139 

6625  140 
\item[$axclass$] \index{*axclass section} defines an \rmindex{axiomatic type 
141 
class} \cite{Wenzel:1997:TPHOL} as the intersection of existing classes, 

142 
with additional axioms holding. Class axioms may not contain more than one 

143 
type variable. The class axioms (with implicit sort constraints added) are 

144 
bound to the given names. Furthermore a class introduction rule is 

145 
generated, which is automatically employed by $instance$ to prove 

146 
instantiations of this class. 

3108  147 

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

149 
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

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

153 
code $verbatim$. 

1650  154 

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

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

4543  158 

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

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

163 
declared as short base names only. 

164 

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

166 
all following theory sections until changed again explicitly. Also 

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

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

169 
on are handled. 

5369  170 

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

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

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

174 
initialized in this way. 

1846  175 

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

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

180 
Chapters~\ref{DefiningLogics} and \ref{chap:syntax} explain mixfix 
6669  181 
declarations, translation rules and the \texttt{ML} section in more detail. 
145  182 

183 

1905  184 
\subsection{Definitions}\indexbold{definitions} 
185 

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

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

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

1905  190 

191 
Isabelle makes the following checks on definitions: 

192 
\begin{itemize} 

3108  193 
\item Arguments (on the lefthand side) must be distinct variables. 
1905  194 
\item All variables on the righthand side must also appear on the lefthand 
195 
side. 

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

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

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

201 
\end{itemize} 

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

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

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

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

206 

207 

275  208 
\subsection{*Classes and arities} 
324  209 
\index{classes!context conditions}\index{arities!context conditions} 
145  210 

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

216 
excludes the following: 

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

218 
arities 
3108  219 
foo :: ({\ttlbrace}logic{\ttrbrace}) logic 
220 
foo :: ({\ttlbrace}{\ttrbrace})logic 

145  221 
\end{ttbox} 
286  222 

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

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

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

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

229 
following is forbidden: 

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

231 
arities 
3108  232 
foo :: ({\ttlbrace}logic{\ttrbrace})logic 
233 
foo :: ({\ttlbrace}{\ttrbrace})term 

145  234 
\end{ttbox} 
286  235 

145  236 
\end{itemize} 
237 

104  238 

6568  239 
\section{The theory loader}\label{sec:moretheories} 
240 
\index{theories!reading}\index{files!reading} 

241 

242 
Isabelle's theory loader manages dependencies of the internal graph of theory 

243 
nodes (the \emph{theory database}) and the external view of the file system. 

244 
See \S\ref{sec:introtheories} for its most basic commands, such as 

245 
\texttt{use_thy}. There are a few more operations available. 

246 

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

247 
\begin{ttbox} 
6568  248 
use_thy_only : string > unit 
7136  249 
update_thy_only : string > unit 
6568  250 
touch_thy : string > unit 
6658  251 
remove_thy : string > unit 
286  252 
delete_tmpfiles : bool ref \hfill{\bf initially true} 
253 
\end{ttbox} 

254 

324  255 
\begin{ttdescription} 
6569  256 
\item[\ttindexbold{use_thy_only} "$name$";] is similar to \texttt{use_thy}, 
257 
but processes the actual theory file $name$\texttt{.thy} only, ignoring 

6568  258 
$name$\texttt{.ML}. This might be useful in replaying proof scripts by hand 
259 
from the very beginning, starting with the fresh theory. 

260 

7136  261 
\item[\ttindexbold{update_thy_only} "$name$";] is similar to 
262 
\texttt{update_thy}, but processes the actual theory file 

263 
$name$\texttt{.thy} only, ignoring $name$\texttt{.ML}. 

264 

6569  265 
\item[\ttindexbold{touch_thy} "$name$";] marks theory node $name$ of the 
6568  266 
internal graph as outdated. While the theory remains usable, subsequent 
267 
operations such as \texttt{use_thy} may cause a reload. 

268 

6658  269 
\item[\ttindexbold{remove_thy} "$name$";] deletes theory node $name$, 
270 
including \emph{all} of its descendants. Beware! This is a quick way to 

271 
dispose a large number of theories at once. Note that {\ML} bindings to 

272 
theorems etc.\ of removed theories may still persist. 

273 

6568  274 
\item[reset \ttindexbold{delete_tmpfiles};] processing theory files usually 
275 
involves temporary {\ML} files to be created. By default, these are deleted 

276 
afterwards. Resetting the \texttt{delete_tmpfiles} flag inhibits this, 

277 
leaving the generated code for debugging purposes. The basic location for 

278 
temporary files is determined by the \texttt{ISABELLE_TMP} environment 

6571  279 
variable (which is private to the running Isabelle process and may be 
6568  280 
retrieved by \ttindex{getenv} from {\ML}). 
324  281 
\end{ttdescription} 
138
9ba8bff1addc
added chapter "Defining Theories" and made changes for new Readthy functions
clasohm
parents:
104
diff
changeset

282 

6568  283 
\medskip Theory and {\ML} files are located by skimming through the 
284 
directories listed in Isabelle's internal load path, which merely contains the 

285 
current directory ``\texttt{.}'' by default. The load path may be accessed by 

286 
the following operations. 

332  287 

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

288 
\begin{ttbox} 
6568  289 
show_path: unit > string list 
290 
add_path: string > unit 

291 
del_path: string > unit 

292 
reset_path: unit > unit 

286  293 
\end{ttbox} 
294 

324  295 
\begin{ttdescription} 
6568  296 
\item[\ttindexbold{show_path}();] displays the load path components in 
6571  297 
canonical string representation (which is always according to Unix rules). 
6568  298 

6569  299 
\item[\ttindexbold{add_path} "$dir$";] adds component $dir$ to the beginning 
300 
of the load path. 

6568  301 

6569  302 
\item[\ttindexbold{del_path} "$dir$";] removes any occurrences of component 
6568  303 
$dir$ from the load path. 
304 

305 
\item[\ttindexbold{reset_path}();] resets the load path to ``\texttt{.}'' 

306 
(current directory) only. 

324  307 
\end{ttdescription} 
286  308 

6571  309 
In operations referring indirectly to some file, the argument may be prefixed 
7136  310 
by a directory that will be temporarily appended to the load path, e.g.\ 
6571  311 
\texttt{use_thy~"$dir/name$"}. Note that, depending on which parts of the 
312 
ancestry of $name$ are already loaded, the dynamic change of paths might be 

7136  313 
hard to predict. Use this feature with great care only. 
104  314 

315 

6669  316 
\section{Locales} 
317 
\label{Locales} 

318 

319 
Locales \cite{kammuellerlocales} are a concept of local proof contexts. They 

320 
are introduced as named syntactic objects within theories and can be 

321 
opened in any descendant theory. 

322 

323 
\subsection{Declaring Locales} 

324 

325 
A locale is declared in a theory section that starts with the 

326 
keyword \texttt{locale}. It consists typically of three parts, the 

327 
\texttt{fixes} part, the \texttt{assumes} part, and the \texttt{defines} part. 

328 
Appendix \ref{app:TheorySyntax} presents the full syntax. 

329 

330 
\subsubsection{Parts of Locales} 

331 

332 
The subsection introduced by the keyword \texttt{fixes} declares the locale 

333 
constants in a way that closely resembles a global \texttt{consts} 

334 
declaration. In particular, there may be an optional pretty printing syntax 

335 
for the locale constants. 

336 

337 
The subsequent \texttt{assumes} part specifies the locale rules. They are 

338 
defined like \texttt{rules}: by an identifier followed by the rule 

339 
given as a string. Locale rules admit the statement of local assumptions 

340 
about the locale constants. The \texttt{assumes} part is optional. Nonfixed 

341 
variables in locale rules are automatically bound by the universal quantifier 

342 
\texttt{!!} of the metalogic. 

343 

344 
Finally, the \texttt{defines} part introduces the definitions that are 

345 
available in the locale. Locale constants declared in the \texttt{fixes} 

346 
section are defined using the metaequality \texttt{==}. If the 

347 
locale constant is a functiond then its definition can (as usual) have 

348 
variables on the lefthand side acting as formal parameters; they are 

349 
considered as schematic variables and are automatically generalized by 

350 
universal quantification of the metalogic. The right hand side of a 

351 
definition must not contain variables that are not already on the left hand 

352 
side. In so far locale definitions behave like theory level definitions. 

353 
However, the locale concept realizes \emph{dependent definitions}: any variable 

354 
that is fixed as a locale constant can occur on the right hand side of 

355 
definitions. For an illustration of these dependent definitions see the 

356 
occurrence of the locale constant \texttt{G} on the right hand side of the 

357 
definitions of the locale \texttt{group} below. Naturally, definitions can 

358 
already use the syntax of the locale constants in the \texttt{fixes} 

359 
subsection. The \texttt{defines} part is, as the \texttt{assumes} part, 

360 
optional. 

361 

362 
\subsubsection{Example for Definition} 

363 
The concrete syntax of locale definitions is demonstrated by example below. 

364 

365 
Locale \texttt{group} assumes the definition of groups in a theory 

366 
file\footnote{This and other examples are from \texttt{HOL/ex}.}. A locale 

367 
defining a convenient proof environment for group related proofs may be 

368 
added to the theory as follows: 

369 
\begin{ttbox} 

370 
locale group = 

371 
fixes 

372 
G :: "'a grouptype" 

373 
e :: "'a" 

374 
binop :: "'a => 'a => 'a" (infixr "#" 80) 

375 
inv :: "'a => 'a" ("i(_)" [90] 91) 

376 
assumes 

377 
Group_G "G: Group" 

378 
defines 

379 
e_def "e == unit G" 

380 
binop_def "x # y == bin_op G x y" 

381 
inv_def "i(x) == inverse G x" 

382 
\end{ttbox} 

383 

384 
\subsubsection{Polymorphism} 

385 

386 
In contrast to polymorphic definitions in theories, the use of the 

387 
same type variable for the declaration of different locale constants in the 

388 
fixes part means \emph{the same} type. In other words, the scope of the 

389 
polymorphic variables is extended over all constant declarations of a locale. 

390 
In the above example \texttt{'a} refers to the same type which is fixed inside 

391 
the locale. In an exported theorem (see \S\ref{sec:localeexport}) the 

392 
constructors of locale \texttt{group} are polymorphic, yet only simultaneously 

393 
instantiatable. 

394 

395 
\subsubsection{Nested Locales} 

396 

397 
A locale can be defined as the extension of a previously defined 

398 
locale. This operation of extension is optional and is syntactically 

399 
expressed as 

400 
\begin{ttbox} 

401 
locale foo = bar + ... 

402 
\end{ttbox} 

403 
The locale \texttt{foo} builds on the constants and syntax of the locale {\tt 

404 
bar}. That is, all contents of the locale \texttt{bar} can be used in 

405 
definitions and rules of the corresponding parts of the locale {\tt 

406 
foo}. Although locale \texttt{foo} assumes the \texttt{fixes} part of \texttt{bar} it 

407 
does not automatically subsume its rules and definitions. Normally, one 

408 
expects to use locale \texttt{foo} only if locale \texttt{bar} is already 

409 
active. These aspects of use and activation of locales are considered in the 

410 
subsequent section. 

411 

412 

413 
\subsection{Locale Scope} 

414 

415 
Locales are by default inactive, but they can be invoked. The list of 

416 
currently active locales is called \emph{scope}. The process of activating 

417 
them is called \emph{opening}; the reverse is \emph{closing}. 

418 

419 
\subsubsection{Scope} 

420 
The locale scope is part of each theory. It is a dynamic stack containing 

421 
all active locales at a certain point in an interactive session. 

422 
The scope lives until all locales are explicitly closed. At one time there 

423 
can be more than one locale open. The contents of these various active 

424 
locales are all visible in the scope. In case of nested locales for example, 

425 
the nesting is actually reflected to the scope, which contains the nested 

426 
locales as layers. To check the state of the scope during a development the 

427 
function \texttt{Print\_scope} may be used. It displays the names of all open 

428 
locales on the scope. The function \texttt{print\_locales} applied to a theory 

429 
displays all locales contained in that theory and in addition also the 

430 
current scope. 

431 

432 
The scope is manipulated by the commands for opening and closing of locales. 

433 

434 
\subsubsection{Opening} 

435 
Locales can be \emph{opened} at any point during a session where 

436 
we want to prove theorems concerning the locale. Opening a locale means 

437 
making its contents visible by pushing it onto the scope of the current 

438 
theory. Inside a scope of opened locales, theorems can use all definitions and 

439 
rules contained in the locales on the scope. The rules and definitions may 

440 
be accessed individually using the function \ttindex{thm}. This function is 

441 
applied to the names assigned to locale rules and definitions as 

442 
strings. The opening command is called \texttt{Open\_locale} and takes the 

443 
name of the locale to be opened as its argument. 

444 

445 
If one opens a locale \texttt{foo} that is defined by extension from locale 

446 
\texttt{bar}, the function \texttt{Open\_locale} checks if locale \texttt{bar} 

447 
is open. If so, then it just opens \texttt{foo}, if not, then it prints a 

448 
message and opens \texttt{bar} before opening \texttt{foo}. Naturally, this 

449 
carries on, if \texttt{bar} is again an extension. 

450 

451 
\subsubsection{Closing} 

452 

453 
\emph{Closing} means to cancel the last opened locale, pushing it out of the 

454 
scope. Theorems proved during the life cycle of this locale will be disabled, 

455 
unless they have been explicitly exported, as described below. However, when 

456 
the same locale is opened again these theorems may be used again as well, 

457 
provided that they were saved as theorems in the first place, using 

458 
\texttt{qed} or ML assignment. The command \texttt{Close\_locale} takes a 

459 
locale name as a string and checks if this locale is actually the topmost 

460 
locale on the scope. If this is the case, it removes this locale, otherwise 

461 
it prints a warning message and does not change the scope. 

462 

463 
\subsubsection{Export of Theorems} 

464 
\label{sec:localeexport} 

465 

466 
Export of theorems transports theorems out of the scope of locales. Locale 

467 
rules that have been used in the proof of an exported theorem inside the 

468 
locale are carried by the exported form of the theorem as its individual 

469 
metaassumptions. The locale constants are universally quantified variables 

470 
in these theorems, hence such theorems can be instantiated individually. 

471 
Definitions become unfolded; locale constants that were merely used for 

472 
definitions vanish. Logically, exporting corresponds to a combined 

473 
application of introduction rules for implication and universal 

474 
quantification. Exporting forms a kind of normalization of theorems in a 

475 
locale scope. 

476 

477 
According to the possibility of nested locales there are two different forms 

478 
of export. The first one is realized by the function \texttt{export} that 

479 
exports theorems through all layers of opened locales of the scope. Hence, 

480 
the application of export to a theorem yields a theorem of the global level, 

481 
that is, the current theory context without any local assumptions or 

482 
definitions. 

483 

484 
When locales are nested we might want to export a theorem, not to the global 

485 
level of the current theory but just to the previous level. The other export 

486 
function, \texttt{Export}, transports theorems one level up in the scope; the 

487 
theorem still uses locale constants, definitions and rules of the locales 

488 
underneath. 

489 

490 
\subsection{Functions for Locales} 

491 
\label{Syntax} 

492 
\index{locales!functions} 

493 

494 
Here is a quick reference list of locale functions. 

495 
\begin{ttbox} 

496 
Open_locale : xstring > unit 

497 
Close_locale : xstring > unit 

498 
export : thm > thm 

499 
Export : thm > thm 

500 
thm : xstring > thm 

501 
Print_scope : unit > unit 

502 
print_locales: theory > unit 

503 
\end{ttbox} 

504 
\begin{ttdescription} 

505 
\item[\ttindexbold{Open_locale} $xstring$] 

506 
opens the locale {\it xstring}, adding it to the scope of the theory of the 

507 
current context. If the opened locale is built by extension, the ancestors 

508 
are opened automatically. 

509 

510 
\item[\ttindexbold{Close_locale} $xstring$] eliminates the locale {\it 

511 
xstring} from the scope if it is the topmost item on it, otherwise it does 

512 
not change the scope and produces a warning. 

513 

514 
\item[\ttindexbold{export} $thm$] locale definitions become expanded in {\it 

515 
thm} and locale rules that were used in the proof of {\it thm} become part 

516 
of its individual assumptions. This normalization happens with respect to 

517 
\emph{all open locales} on the scope. 

518 

519 
\item[\ttindexbold{Export} $thm$] works like \texttt{export} but normalizes 

520 
theorems only up to the previous level of locales on the scope. 

521 

522 
\item[\ttindexbold{thm} $xstring$] applied to the name of a locale definition 

523 
or rule it returns the definition as a theorem. 

524 

525 
\item[\ttindexbold{Print_scope}()] prints the names of the locales in the 

526 
current scope of the current theory context. 

527 

528 
\item[\ttindexbold{print_locale} $theory$] prints all locales that are 

529 
contained in {\it theory} directly or indirectly. It also displays the 

530 
current scope similar to \texttt{Print\_scope}. 

531 
\end{ttdescription} 

532 

533 

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

534 
\section{Basic operations on theories}\label{BasicOperationsOnTheories} 
4384  535 

536 
\subsection{*Theory inclusion} 

537 
\begin{ttbox} 

538 
subthy : theory * theory > bool 

539 
eq_thy : theory * theory > bool 

540 
transfer : theory > thm > thm 

541 
transfer_sg : Sign.sg > thm > thm 

542 
\end{ttbox} 

543 

544 
Inclusion and equality of theories is determined by unique 

545 
identification stamps that are created when declaring new components. 

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

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

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

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

550 
pretty printing of theorems). 

551 

552 
\begin{ttdescription} 

553 

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

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

556 

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

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

559 

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

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

562 

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

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

565 
signature. 

566 

567 
\end{ttdescription} 

568 

569 

6571  570 
\subsection{*Primitive theories} 
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset

571 
\begin{ttbox} 
4317  572 
ProtoPure.thy : theory 
3108  573 
Pure.thy : theory 
574 
CPure.thy : theory 

286  575 
\end{ttbox} 
3108  576 
\begin{description} 
4317  577 
\item[\ttindexbold{ProtoPure.thy}, \ttindexbold{Pure.thy}, 
578 
\ttindexbold{CPure.thy}] contain the syntax and signature of the 

579 
metalogic. There are basically no axioms: metalevel inferences 

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

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

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

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

584 
containing no syntax for printing prefix applications at all! 

6571  585 

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

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

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

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

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

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

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

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

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

596 
%\end{ttbox} 
3108  597 
\end{description} 
286  598 

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

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

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

286  603 
%is the \ML{} equivalent of the following theory definition: 
275  604 
%\begin{ttbox} 
605 
%\(T\) = \(thy\) + 

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

607 
% \dots 

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

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

610 
% \dots 

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

612 
% \dots 

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

614 
% \dots 

615 
%rules \(name\) \(rule\) 

616 
% \dots 

617 
%end 

618 
%\end{ttbox} 

619 
%where 

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

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

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

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

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

625 
%\\ 

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

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

628 
%\end{tabular} 

104  629 

630 

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

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

633 
\begin{ttbox} 
4317  634 
print_syntax : theory > unit 
635 
print_theory : theory > unit 

636 
parents_of : theory > theory list 

637 
ancestors_of : theory > theory list 

638 
sign_of : theory > Sign.sg 

639 
Sign.stamp_names_of : Sign.sg > string list 

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

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

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

646 

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

648 
$thy$, excluding the syntax. 

4317  649 

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

651 
of~$thy$. 

652 

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

654 
(not including $thy$ itself). 

655 

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

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

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

659 

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

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

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

663 
including that of $sg$ itself. 

104  664 

324  665 
\end{ttdescription} 
104  666 

1369  667 

104  668 
\section{Terms} 
669 
\index{termsbold} 

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

674 
infix 9 $; 

675 
datatype term = Const of string * typ 

676 
 Free of string * typ 

677 
 Var of indexname * typ 

678 
 Bound of int 

679 
 Abs of string * typ * term 

680 
 op $ of term * term; 

681 
\end{ttbox} 

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

686 
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

687 
syntax. 
104  688 

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

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

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

696 
incrementing their subscripts. Scheme variables are essentially free 

697 
variables, but may be instantiated during unification. 

104  698 

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

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

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

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

6592  704 
Paulson~\cite[page~376]{paulsonml2}. 
104  705 

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

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

710 
and printing; it has no logical significance. 

104  711 

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

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

718 
\begin{ttbox} 
104  719 
Const("Trueprop",_) $ (Const("op >",_) $ A $ B) 
720 
\end{ttbox} 

721 

722 

4317  723 
\section{*Variable binding} 
286  724 
\begin{ttbox} 
725 
loose_bnos : term > int list 

726 
incr_boundvars : int > term > term 

727 
abstract_over : term*term > term 

728 
variant_abs : string * typ * term > string * term 

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

732 
bound variables. 

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

734 
\item[\ttindexbold{loose_bnos} $t$] 
286  735 
returns the list of all dangling bound variable references. In 
6669  736 
particular, \texttt{Bound~0} is loose unless it is enclosed in an 
737 
abstraction. Similarly \texttt{Bound~1} is loose unless it is enclosed in 

286  738 
at least two abstractions; if enclosed in just one, the list will contain 
739 
the number 0. A wellformed term does not contain any loose variables. 

740 

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

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

745 
abstraction are unaffected. 

746 

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

747 
\item[\ttindexbold{abstract_over} $(v,t)$] 
286  748 
forms the abstraction of~$t$ over~$v$, which may be any wellformed term. 
6669  749 
It replaces every occurrence of \(v\) by a \texttt{Bound} variable with the 
286  750 
correct index. 
751 

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

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

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

332  756 
of~$a$ chosen to be distinct from all constants and from all variables 
286  757 
free in~$u$. 
758 

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

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

762 
\begin{itemize} 

763 
\item 

6669  764 
Two constants, \texttt{Free}s, or \texttt{Var}s are \(\alpha\)convertible 
286  765 
if their names and types are equal. 
766 
(Variables having the same name but different types are thus distinct. 

767 
This confusing situation should be avoided!) 

768 
\item 

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

770 
if they have the same number. 

771 
\item 

772 
Two abstractions are \(\alpha\)convertible 

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

774 
\item 

775 
Two applications are \(\alpha\)convertible 

776 
if the corresponding subterms are. 

777 
\end{itemize} 

778 

324  779 
\end{ttdescription} 
286  780 

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

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

782 
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

783 
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

784 
constant declared in the signature. The term must be welltyped and its use 
6669  785 
of bound variables must be wellformed. Metarules such as \texttt{forall_elim} 
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset

786 
take certified terms as arguments. 
104  787 

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

791 

792 
\subsection{Printing terms} 

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

794 
\begin{ttbox} 
275  795 
string_of_cterm : cterm > string 
104  796 
Sign.string_of_term : Sign.sg > term > string 
797 
\end{ttbox} 

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

799 
\item[\ttindexbold{string_of_cterm} $ct$] 
104  800 
displays $ct$ as a string. 
801 

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

802 
\item[\ttindexbold{Sign.string_of_term} $sign$ $t$] 
104  803 
displays $t$ as a string, using the syntax of~$sign$. 
324  804 
\end{ttdescription} 
104  805 

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

807 
\begin{ttbox} 
4543  808 
cterm_of : Sign.sg > term > cterm 
809 
read_cterm : Sign.sg > string * typ > cterm 

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

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

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

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

104  814 
\end{ttbox} 
324  815 
\begin{ttdescription} 
4543  816 

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

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

819 

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

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

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

823 
of phrase to parse. 

824 

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

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

827 
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

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

829 
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

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

831 

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

834 
$sign$. 

835 

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

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

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

839 
computed during certification. 

840 

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

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

843 
an abstract \texttt{cterm}. 

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

844 

324  845 
\end{ttdescription} 
104  846 

847 

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

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

849 
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

850 
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

851 
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

852 
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

853 
represented by a string. 
104  854 
\begin{ttbox} 
855 
type class = string; 

856 
type sort = class list; 

857 

858 
datatype typ = Type of string * typ list 

859 
 TFree of string * sort 

860 
 TVar of indexname * sort; 

861 

862 
infixr 5 >; 

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

863 
fun S > T = Type ("fun", [S, T]); 
104  864 
\end{ttbox} 
324  865 
\begin{ttdescription} 
4317  866 
\item[\ttindexbold{Type} ($a$, $Ts$)] \index{type constructorsbold} 
324  867 
applies the {\bf type constructor} named~$a$ to the type operands~$Ts$. 
868 
Type constructors include~\tydx{fun}, the binary function space 

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

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

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

872 
types. 

104  873 

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

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

880 
instantiated during unification. 

881 
\end{ttdescription} 

104  882 

883 

884 
\section{Certified types} 

885 
\index{types!certifiedbold} 

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

886 
Certified types, which are analogous to certified terms, have type 
275  887 
\ttindexbold{ctyp}. 
104  888 

889 
\subsection{Printing types} 

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

891 
\begin{ttbox} 
275  892 
string_of_ctyp : ctyp > string 
104  893 
Sign.string_of_typ : Sign.sg > typ > string 
894 
\end{ttbox} 

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

896 
\item[\ttindexbold{string_of_ctyp} $cT$] 
104  897 
displays $cT$ as a string. 
898 

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

899 
\item[\ttindexbold{Sign.string_of_typ} $sign$ $T$] 
104  900 
displays $T$ as a string, using the syntax of~$sign$. 
324  901 
\end{ttdescription} 
104  902 

903 

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

905 
\begin{ttbox} 
4543  906 
ctyp_of : Sign.sg > typ > ctyp 
907 
rep_ctyp : ctyp > {\ttlbrace}T: typ, sign: Sign.sg\ttrbrace 

908 
Sign.certify_typ : Sign.sg > typ > typ 

104  909 
\end{ttbox} 
324  910 
\begin{ttdescription} 
4543  911 

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

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

914 

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

916 
containing the type itself and its signature. 

917 

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

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

920 
an abstract \texttt{ctyp}. 

104  921 

324  922 
\end{ttdescription} 
104  923 

1846  924 

4317  925 
\section{Oracles: calling trusted external reasoners} 
1846  926 
\label{sec:oracles} 
927 
\index{oracles(} 

928 

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

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

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

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

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

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

935 
depends upon oracle calls. 

936 

937 
\begin{ttbox} 

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

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

940 
> theory 
1846  941 
\end{ttbox} 
942 
\begin{ttdescription} 

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

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

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

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

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

949 
its result is illtyped. 

950 

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

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

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

1846  954 
\end{ttdescription} 
955 

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

6669  957 
The {\ML} type \texttt{exn} is a datatype that can be extended at any time. (See 
1846  958 
my {\em {ML} for the Working Programmer}~\cite{paulsonml2}, especially 
959 
page~136.) The oracle mechanism takes advantage of this to allow an oracle to 

960 
take any information whatever. 

961 

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

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

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

4317  965 
exception object. 
1846  966 
\begin{itemize} 
967 
\item The signature will typically be that of a desendant of the theory 

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

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

970 

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

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

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

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

975 
solve the specified problem. 

976 
\end{itemize} 

977 

6669  978 
A trivial example is provided in theory \texttt{FOL/ex/IffOracle}. This 
4317  979 
oracle generates tautologies of the form $P\bimp\cdots\bimp P$, with 
980 
an even number of $P$s. 

1846  981 

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

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

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

986 
defines the oracle function itself. 

1846  987 
\begin{ttbox} 
4317  988 
exception IffOracleExn of int;\medskip 
989 
fun mk_iff_oracle (sign, IffOracleExn n) = 

990 
if n > 0 andalso n mod 2 = 0 

6669  991 
then Trueprop \$ mk_iff n 
4317  992 
else raise IffOracleExn n; 
1846  993 
\end{ttbox} 
6669  994 
Observe the function's two arguments, the signature \texttt{sign} and the 
4317  995 
exception given as a pattern. The function checks its argument for 
996 
validity. If $n$ is positive and even then it creates a tautology 

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

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

6669  999 
signalled by other means, such as returning the theorem \texttt{True}. 
4317  1000 
Please ensure that the oracle's result is correctly typed; Isabelle 
1001 
will reject illtyped theorems by raising a cryptic exception at top 

1002 
level. 

1846  1003 

6669  1004 
The \texttt{oracle} section of \texttt{IffOracle.thy} installs above 
4317  1005 
\texttt{ML} function as follows: 
1846  1006 
\begin{ttbox} 
4317  1007 
IffOracle = FOL +\medskip 
1008 
oracle 

1009 
iff = mk_iff_oracle\medskip 

1846  1010 
end 
1011 
\end{ttbox} 

1012 

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

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

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

1017 
(sign_of IffOracle.thy, IffOracleExn n); 
4317  1018 
\end{ttbox} 
1019 

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

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

1022 
\begin{ttbox} 

1023 
iff_oracle 10; 

1846  1024 
{\out "P <> P <> P <> P <> P <> P <> P <> P <> P <> P" : thm} 
4317  1025 
iff_oracle 5; 
1846  1026 
{\out Exception IffOracleExn 5 raised} 
1027 
\end{ttbox} 

1028 

1029 
\index{oracles)} 

104  1030 
\index{theories)} 
5369  1031 

1032 

1033 
%%% Local Variables: 

1034 
%%% mode: latex 

1035 
%%% TeXmaster: "ref" 

1036 
%%% End: 