author  nipkow 
Tue, 01 Mar 1994 17:21:47 +0100  
changeset 275  933ec96c522e 
parent 273  538db1a98ba3 
child 286  e7efbf03562b 
permissions  rwrr 
104  1 
%% $Id$ 
145  2 

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

5 
\index{reading!axiomssee{{\tt extend_theory} and {\tt assume_ax}}} 

6 
Theories organize the syntax, declarations and axioms of a mathematical 

7 
development. They are built, starting from the Pure theory, by extending 

275  8 
and merging existing theories. They have the \ML\ type \ttindex{theory}. 
104  9 
Theory operations signal errors by raising exception \ttindex{THEORY}, 
10 
returning a message and a list of theories. 

11 

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

275  13 
syntax, have the \ML\ type~\ttindexbold{Sign.sg}. For identification, 
14 
each signature carries a unique list of {\bf stamps}, which are \ML\ 

104  15 
references (to strings). The strings serve as humanreadable names; the 
16 
references serve as unique identifiers. Each primitive signature has a 

17 
single stamp. When two signatures are merged, their lists of stamps are 

18 
also merged. Every theory carries a unique signature. 

19 

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

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

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

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

26 
\section{Defining Theories} 

27 
\label{DefiningTheories} 

28 

29 
Theories can be defined either using concrete syntax or by calling certain 

273  30 
\MLfunctions (see \S\ref{BuildingATheory}). Appendix~\ref{TheorySyntax} 
275  31 
presents the concrete syntax for theories following convention that 
104  32 
\begin{itemize} 
275  33 
\item {\tt typewriter font} denotes terminal symbols; 
34 
\item $id$, $tid$, $nat$, $string$ and $text$ are the lexical classes of 

35 
identifiers, type identifiers, natural numbers, \ML\ strings (with their 

36 
quotation marks) and arbitrary \ML\ text. The first three are fully defined 

37 
in the {\it Defining Logics} chapter of {\it Isabelle's Object Logics}. 

104  38 
\end{itemize} 
39 
The different parts of a theory definition are interpreted as follows: 

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

40 
\begin{description} 
273  41 
\item[{\it theoryDef}] A theory has a name $id$ and is an extension of the 
275  42 
union of theories with name {\it name}, the {\bf parent 
43 
theories}\indexbold{theories!parent}, with new classes, types, constants, 

44 
syntax and axioms. The basic theory, which contains only the metalogic, 

45 
is called {\tt Pure}. 

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

46 

275  47 
Normally each {\it name\/} is an identifier, the precise name of the parent 
48 
theory. Strings can be used to document additional dependencies; see 

49 
\S\ref{LoadingTheories} for details. 

273  50 
\item[$classes$] {\tt$id$ < $id@1$ \dots\ $id@n$} declares $id$ as a subclass 
51 
of existing classes $id@1\dots id@n$. This rules out cyclic class 

52 
structures. Isabelle automatically computes the transitive closure of 

53 
subclass hierarchies. Hence it is not necessary to declare {\tt c < e} in 

54 
addition to {\tt c < d} and {\tt d < e}. 

104  55 
\item[$default$] introduces $sort$ as the new default sort for type 
56 
variables. Unconstrained type variables in an input string are 

57 
automatically constrained by $sort$; this does not apply to type variables 

273  58 
created internally during type inference. If omitted, the default sort is 
59 
the union of the default sorts of the parent theories. 

60 
\item[$sort$] is a finite set of classes; a single class $id$ abbreviates the 

61 
singleton set {\tt\{}$id${\tt\}}. 

62 
\item[$type$] is either the declaration of a new type (constructor) or type 

63 
synonym $name$. Only binary type constructors can have infix status and 

275  64 
symbolic names, e.g.\ {\tt ('a,'b)"*"}. Type constructors of $n$ arguments 
65 
are declared by $(\alpha@1,\dots,\alpha@n)name$. A {\bf type 

66 
synonym}\indexbold{type!synonym} is simply an abbreviation 

67 
$(\alpha@1,\dots,\alpha@n)name = \mbox{\tt"}\tau\mbox{\tt"}$ and follows 

68 
the same rules as in \ML, except that $name$ can be a string and $\tau$ 

69 
must be enclosed in quotation marks. 

104  70 
\item[$infix$] declares a type or constant to be an infix operator of 
273  71 
precedence $nat$ associating to the left ({\tt infixl}) or right ({\tt 
104  72 
infixr}). 
273  73 
\item[$arities$] Each $name$ must be an existing type constructor which is 
74 
given the additional arity $arity$. 

75 
\item[$constDecl$] Each new constant $name$ is declared to be of type 

275  76 
$string$. For display purposes $mixfix$ annotations can be attached. 
273  77 
\item[$mixfix$] There are three forms of syntactic annotations: 
78 
\begin{itemize} 

79 
\item A mixfix template given as a $string$ of the form 

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

81 
indicates the position where the $i$th argument should go. The minimal 

82 
precedence of each argument is given by a list of natural numbers, the 

275  83 
precedence of the whole construct by the following natural number; 
84 
precedences are optional. 

104  85 

273  86 
\item Binary constants can be given infix status. 
104  87 

273  88 
\item A constant $f$ {\tt::} $(\tau@1\To\tau@2)\To\tau@3$ can be given {\em 
275  89 
binder\/} status: {\tt binder} $Q$ $p$ causes $Q\,x.F(x)$ to be treated 
104  90 
like $f(F)$; $p$ is the precedence of the construct. 
273  91 
\end{itemize} 
92 
\item[$trans$] Specifies syntactic translation rules, that is parse 

93 
rules ({\tt =>}), print rules ({\tt <=}), or both ({\tt ==}). 

104  94 
\item[$rule$] A rule consists of a name $id$ and a formula $string$. Rule 
95 
names must be distinct. 

275  96 
\item[$ml$] This final part of a theory consists of \ML\ code, 
104  97 
typically for parse and print translations. 
98 
\end{description} 

273  99 
The $mixfix$, $trans$ and $ml$ sections are explained in more detail in 
275  100 
the {\it Defining Logics} chapter of {\it Isabelle's Object Logics}. 
145  101 

102 

275  103 
\subsection{*Classes and arities} 
104 
\index{*classes!context conditions} 

145  105 
\index{*arities!context conditions} 
106 

275  107 
Classes and arities are subject to the following two wellformedness 
145  108 
conditions: 
109 
\begin{itemize} 

110 
\item There are no two declarations $ty :: (\vec{r})c$ and $ty :: (\vec{s})c$ 

111 
with $\vec{r} \neq \vec{s}$. For example 

112 
\begin{ttbox} 

275  113 
types 'a ty 
145  114 
arities ty :: ({\ttlbrace}logic{\ttrbrace}) logic 
115 
ty :: ({\ttlbrace}{\ttrbrace})logic 

116 
\end{ttbox} 

117 
leads to an error message and fails. 

118 
\item If there are two declarations $ty :: (s@1,\dots,s@n)c$ and $ty :: 

119 
(s@1',\dots,s@n')c'$ such that $c' < c$ then $s@i' \preceq s@i$ must hold 

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

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

122 
expresses that the set of types represented by $s'$ is a subset of the set of 

123 
types represented by $s$. For example 

124 
\begin{ttbox} 

125 
classes term < logic 

275  126 
types 'a ty 
145  127 
arities ty :: ({\ttlbrace}logic{\ttrbrace})logic 
128 
ty :: ({\ttlbrace}{\ttrbrace})term 

129 
\end{ttbox} 

130 
leads to an error message and fails. 

131 
\end{itemize} 

132 
These conditions guarantee principal types~\cite{nipkowprehofer}. 

133 

104  134 

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

135 
\section{Loading Theories} 
9ba8bff1addc
added chapter "Defining Theories" and made changes for new Readthy functions
clasohm
parents:
104
diff
changeset

136 
\label{LoadingTheories} 
275  137 
\index{theories!loading(} 
138 

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

139 
\subsection{Reading a new theory} 
9ba8bff1addc
added chapter "Defining Theories" and made changes for new Readthy functions
clasohm
parents:
104
diff
changeset

140 

104  141 
Each theory definition must reside in a separate file. Let the file {\it 
139  142 
tf}{\tt.thy} contain the definition of a theory called $TF$ with parent 
138
9ba8bff1addc
added chapter "Defining Theories" and made changes for new Readthy functions
clasohm
parents:
104
diff
changeset

143 
theories $TB@1$ \dots $TB@n$. Calling \ttindexbold{use_thy}~{\tt"}{\it 
275  144 
TF\/}{\tt"} reads file {\it tf}{\tt.thy}, writes an intermediate \MLfile 
145 
{\tt.}{\it tf}{\tt.thy.ML}, and reads the latter file. Any of the parent 

146 
theories that have not been loaded yet are read now by recursive {\tt 

147 
use_thy} calls until either an already loaded theory or {\tt Pure} is 

148 
reached. Therefore one can read a complete logic by just one {\tt use_thy} 

149 
call if all theories are linked appropriately. Afterwards an \ML\ 

139  150 
structure~$TF$ containing a component {\tt thy} for the new theory and 
151 
components $r@1$ \dots $r@n$ for the rules is declared; it also contains the 

152 
definitions of the {\tt ML} section if any. Unless 

275  153 
\ttindexbold{delete_tmpfiles} is set to {\tt false}, {\tt.}{\it 
154 
tf}{\tt.thy.ML} is deleted if no errors occurred. Finally the file {\it 

155 
tf}{\tt.ML} is read, if it exists; this file normally contains proofs 

156 
involving the new theory. 

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

157 

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

158 

275  159 
\subsection{Theory names, file names and search paths} 
160 
\indexbold{theories!names of} 

161 
\indexbold{files!names of} 

162 
\indexbold{search path} 

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

163 

273  164 
\begin{warn} 
165 
The files defining the theory must have the lower case name of the theory 

275  166 
with {\tt.thy} or {\tt.ML} appended. On the other hand \ttindex{use_thy}'s 
167 
parameter has to be the exact theory name. 

273  168 
\end{warn} 
169 
Optionally the name can be preceded by a path to specify the directory where 

170 
the files can be found. If no path is provided the reference variable 

159  171 
\ttindexbold{loadpath} is used which contains a list of paths that are 
275  172 
searched in the given order. After the {\tt.thy}file for a theory has 
173 
been found, the same path is used to locate the (optional) {\tt.ML}file. 

159  174 

275  175 
It is also possible to provide only a {\tt.ML}file, with no 
176 
{\tt.thy}file. In this case the {\tt.ML}file must declare an \ML\ 

177 
structure having the theory's name. If both the {\tt.thy}file and a 

178 
structure declaration in the {\tt.ML}file exist, then the latter 

159  179 
declaration is used. See {\tt ZF/ex/llist.ML} for an example. 
138
9ba8bff1addc
added chapter "Defining Theories" and made changes for new Readthy functions
clasohm
parents:
104
diff
changeset

180 

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

181 

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

182 
\subsection{Reloading a theory} 
275  183 
\indexbold{theories!reloading} 
184 
\index{*update(} 

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

185 

141
a133921366cb
added index commands, removed last paragraph of "Using Poly/ML"
clasohm
parents:
139
diff
changeset

186 
\ttindex{use_thy} keeps track of all loaded theories and stores information 
a133921366cb
added index commands, removed last paragraph of "Using Poly/ML"
clasohm
parents:
139
diff
changeset

187 
about their files. If it finds that the theory to be loaded was already read 
185  188 
before, the following happens: first the theory's files are searched at the 
273  189 
place they were located the last time they were read. If they are found, 
190 
their time of last modification is compared to the internal data and {\tt 

191 
use_thy} stops if they are equal. In case the files have been moved, {\tt 

192 
use_thy} searches them the same way a new theory would be searched for. 

193 
After all these tests have been passed, the theory is reloaded and all 

275  194 
its children are marked as outofdate. 
273  195 
\begin{warn} 
196 
Changing a theory on disk often makes it necessary to reload all theories 

275  197 
that directly or indirectly depend on it. However, {\tt use_thy} reads only 
198 
one theory, even if some of the parent theories are out of date. In this 

199 
case {\tt update()} should be used. This function reloads {\em all\/} 

273  200 
modified theories and their descendants in the correct order. 
201 
\end{warn} 

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

202 

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

203 

275  204 
\subsection{*Pseudo theories} 
205 
\indexbold{theories!pseudo} 

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

206 

275  207 
Any automatic reloading facility requires complete knowledge of all 
208 
dependencies. Sometimes theories depend on objects created in \MLfiles 

209 
without associated {\tt.thy}file. Unless such dependencies are documented, 

210 
{\tt update} fails to reload these \MLfiles and the system is left in a 

211 
state where some objects, e.g.\ theorems, still refer to old versions of 

212 
theories. This may lead to the error 

213 
\begin{ttbox} 

214 
Attempt to merge different versions of theory: \(T\) 

215 
\end{ttbox} 

216 
Therefore there is a way to link theories and {\em orphaned\/} \MLfiles, 

217 
i.e.\ those without associated {\tt.thy}file. 

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

218 

275  219 
Let us assume we have an orphaned \MLfile named {\tt orphan.ML} and a theory 
220 
$B$ which depends on {\tt orphan.ML} (for example, {\tt b.ML} uses theorems 

221 
that are proved in {\tt orphan.ML}). Then {\tt b.thy} should mention this 

222 
dependence: 

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

223 
\begin{ttbox} 
275  224 
B = ... + "orphan" + ... 
138
9ba8bff1addc
added chapter "Defining Theories" and made changes for new Readthy functions
clasohm
parents:
104
diff
changeset

225 
\end{ttbox} 
275  226 
Although {\tt orphan} is {\em not\/} used in building the base of theory $B$ 
227 
(strings stand for \MLfiles rather than {\tt.thy}files and merely document 

228 
additional dependencies), {\tt orphan.ML} is loaded automatically when $B$ is 

229 
(re)built. 

230 

231 
If {\tt orphan.ML} depends on theories $A@1\dots A@n$, this should be recorded 

232 
by creating a {\bf pseudo theory} in the file {\tt orphan.thy}: 

233 
\begin{ttbox} 

234 
orphan = A1 + \(...\) + An 

235 
\end{ttbox} 

236 
The resulting theory is never used but guarantees that {\tt update} reloads 

237 
theory {\it orphan} 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

238 

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

239 
For an extensive example of how this technique can be used to link over 30 
275  240 
files and load them by just two {\tt use_thy} calls, consult the ZF source 
241 
files. 

242 
\index{theories!loading)} 

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

243 

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

244 

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

245 
\subsection{Removing a theory} 
275  246 
\indexbold{theories!removing} 
138
9ba8bff1addc
added chapter "Defining Theories" and made changes for new Readthy functions
clasohm
parents:
104
diff
changeset

247 

275  248 
If a previously read file is removed, {\tt update} will keep on complaining 
249 
about a missing file. The theory is not automatically removed from the 

250 
internal list to preserve the links to other theories in case one forgot to 

251 
adjust the {\tt loadpath} after moving a file. To remove a theory manually 

252 
use \ttindexbold{unlink_thy}. \index{*update)} 

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

253 

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

254 

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

255 
\subsection{Using Poly/\ML} 
141
a133921366cb
added index commands, removed last paragraph of "Using Poly/ML"
clasohm
parents:
139
diff
changeset

256 
\index{Poly/\ML} 
a133921366cb
added index commands, removed last paragraph of "Using Poly/ML"
clasohm
parents:
139
diff
changeset

257 
\index{reference variables} 
138
9ba8bff1addc
added chapter "Defining Theories" and made changes for new Readthy functions
clasohm
parents:
104
diff
changeset

258 

275  259 
As the functions for reading theories depend on reference variables one has 
260 
to take into account the way Poly/\ML\ handles them. They are only saved 

261 
together with the state if they were declared in the current database. For 

262 
example, changes made to a reference variable declared in the {\tt Pure} 

263 
database are {\em not\/} saved if made while using a child database. 

264 
Therefore a new {\tt Readthy} structure has to be created by 

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

265 
\begin{ttbox} 
9ba8bff1addc
added chapter "Defining Theories" and made changes for new Readthy functions
clasohm
parents:
104
diff
changeset

266 
structure Readthy = ReadthyFUN (structure ThySyn = ThySyn); 
141
a133921366cb
added index commands, removed last paragraph of "Using Poly/ML"
clasohm
parents:
139
diff
changeset

267 
Readthy.loaded_thys := !loaded_thys; 
138
9ba8bff1addc
added chapter "Defining Theories" and made changes for new Readthy functions
clasohm
parents:
104
diff
changeset

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

269 
\end{ttbox} 
141
a133921366cb
added index commands, removed last paragraph of "Using Poly/ML"
clasohm
parents:
139
diff
changeset

270 
in every newly created database. By copying the contents of the old reference 
185  271 
variable \verb$loaded_thys$ the list of already loaded theories is preserved. 
272 
Of course this is not necessary if no theories have been read yet. 

104  273 

274 

275 
\section{Basic operations on theories} 

276 
\subsection{Extracting an axiom from a theory} 

277 
\index{theories!extracting axiomsbold}\index{axioms} 

278 
\begin{ttbox} 

279 
get_axiom: theory > string > thm 

280 
assume_ax: theory > string > thm 

281 
\end{ttbox} 

282 
\begin{description} 

283 
\item[\ttindexbold{get_axiom} $thy$ $name$] 

284 
returns an axiom with the given $name$ from $thy$, raising exception 

285 
\ttindex{THEORY} if none exists. Merging theories can cause several axioms 

286 
to have the same name; {\tt get_axiom} returns an arbitrary one. 

287 

288 
\item[\ttindexbold{assume_ax} $thy$ $formula$] 

289 
reads the {\it formula} using the syntax of $thy$, following the same 

290 
conventions as axioms in a theory definition. You can thus pretend that 

291 
{\it formula} is an axiom; in fact, {\tt assume_ax} returns an assumption. 

292 
You can use the resulting theorem like an axiom. Note that 

293 
\ttindex{result} complains about additional assumptions, but 

294 
\ttindex{uresult} does not. 

295 

296 
For example, if {\it formula} is 

297 
\hbox{\tt a=b ==> b=a} then the resulting theorem might have the form 

298 
\hbox{\tt\frenchspacing ?a=?b ==> ?b=?a [!!a b. a=b ==> b=a]} 

299 
\end{description} 

300 

275  301 
%\subsection{Building a theory} 
302 
%\label{BuildingATheory} 

303 
%\index{theories!constructingbold} 

304 
%\begin{ttbox} 

305 
%pure_thy: theory 

306 
%merge_theories: theory * theory > theory 

307 
%extend_theory: theory > string 

308 
% > (class * class list) list 

309 
% * sort 

310 
% * (string list * int)list 

311 
% * (string list * (sort list * class))list 

312 
% * (string list * string)list * sext option 

313 
% > (string*string)list > theory 

314 
%\end{ttbox} 

315 
%Type \ttindex{class} is a synonym for {\tt string}; type \ttindex{sort} is 

316 
%a synonym for \hbox{\tt class list}. 

317 
%\begin{description} 

318 
%\item[\ttindexbold{pure_thy}] contains just the types, constants, and syntax 

319 
% of the metalogic. There are no axioms: metalevel inferences are carried 

320 
% out by \ML\ functions. 

321 
%\item[\ttindexbold{merge_theories} ($thy@1$, $thy@2$)] merges the two 

322 
% theories $thy@1$ and $thy@2$. The resulting theory contains all types, 

323 
% constants and axioms of the constituent theories; its default sort is the 

324 
% union of the default sorts of the constituent theories. 

325 
%\item [\ttindexbold{extend_theory} $thy$ {\tt"}$T${\tt"} 

326 
% ($classes$, $default$, $types$, $arities$, $consts$, $sextopt$) $rules$] 

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

328 
%is the \MLequivalent of the following theory definition: 

329 
%\begin{ttbox} 

330 
%\(T\) = \(thy\) + 

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

332 
% \dots 

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

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

335 
% \dots 

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

337 
% \dots 

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

339 
% \dots 

340 
%rules \(name\) \(rule\) 

341 
% \dots 

342 
%end 

343 
%\end{ttbox} 

344 
%where 

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

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

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

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

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

350 
%\\ 

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

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

353 
%\end{tabular} 

354 
% 

355 
%If theories are defined as in \S\ref{DefiningTheories}, new syntax is added 

356 
%as mixfix annotations to constants. Using {\tt extend_theory}, new syntax can 

357 
%be added via $sextopt$ which is either {\tt None}, or {\tt Some($sext$)}. The 

358 
%latter case is not documented. 

359 
% 

360 
%$T$ identifies the theory internally. When a theory is redeclared, say to 

361 
%change an incorrect axiom, bindings to the old axiom may persist. Isabelle 

362 
%ensures that the old and new theories are not involved in the same proof. 

363 
%Attempting to combine different theories having the same name $T$ yields the 

364 
%fatal error 

365 
%\begin{ttbox} 

366 
%Attempt to merge different versions of theory: \(T\) 

367 
%\end{ttbox} 

368 
%\end{description} 

369 

104  370 
\subsection{Building a theory} 
371 
\label{BuildingATheory} 

372 
\index{theories!constructingbold} 

373 
\begin{ttbox} 

374 
pure_thy: theory 

375 
merge_theories: theory * theory > theory 

275  376 
extend_theory: theory > string > \(\cdots\) > theory 
104  377 
\end{ttbox} 
378 
\begin{description} 

379 
\item[\ttindexbold{pure_thy}] contains just the types, constants, and syntax 

380 
of the metalogic. There are no axioms: metalevel inferences are carried 

381 
out by \ML\ functions. 

382 
\item[\ttindexbold{merge_theories} ($thy@1$, $thy@2$)] merges the two 

383 
theories $thy@1$ and $thy@2$. The resulting theory contains all types, 

384 
constants and axioms of the constituent theories; its default sort is the 

385 
union of the default sorts of the constituent theories. 

275  386 
\item [\ttindexbold{extend_theory} $thy$ {\tt"}$T${\tt"} $\cdots$] extends 
387 
the theory $thy$ with new types, constants, etc. $T$ identifies the theory 

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

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

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

391 
different theories having the same name $T$ yields the fatal error 

104  392 
\begin{ttbox} 
275  393 
Attempt to merge different versions of theory: \(T\) 
104  394 
\end{ttbox} 
395 
\end{description} 

396 

397 

398 
\subsection{Inspecting a theory} 

399 
\index{theories!inspectingbold} 

400 
\begin{ttbox} 

401 
print_theory : theory > unit 

402 
axioms_of : theory > (string*thm)list 

403 
parents_of : theory > theory list 

404 
sign_of : theory > Sign.sg 

405 
stamps_of_thy : theory > string ref list 

406 
\end{ttbox} 

407 
These provide a simple means of viewing a theory's components. 

408 
Unfortunately, there is no direct connection between a theorem and its 

409 
theory. 

410 
\begin{description} 

411 
\item[\ttindexbold{print_theory} {\it thy}] 

412 
prints the theory {\it thy\/} at the terminal as a set of identifiers. 

413 

414 
\item[\ttindexbold{axioms_of} $thy$] 

415 
returns the axioms of~$thy$ and its ancestors. 

416 

417 
\item[\ttindexbold{parents_of} $thy$] 

418 
returns the parents of~$thy$. This list contains zero, one or two 

419 
elements, depending upon whether $thy$ is {\tt pure_thy}, 

420 
\hbox{\tt extend_theory $thy$} or \hbox{\tt merge_theories ($thy@1$, $thy@2$)}. 

421 

422 
\item[\ttindexbold{stamps_of_thy} $thy$]\index{signatures} 

423 
returns the stamps of the signature associated with~$thy$. 

424 

425 
\item[\ttindexbold{sign_of} $thy$] 

426 
returns the signature associated with~$thy$. It is useful with functions 

427 
like {\tt read_instantiate_sg}, which take a signature as an argument. 

428 
\end{description} 

429 

430 

431 
\section{Terms} 

432 
\index{termsbold} 

275  433 
Terms belong to the \ML\ type \ttindexbold{term}, which is a concrete datatype 
104  434 
with six constructors: there are six kinds of term. 
435 
\begin{ttbox} 

436 
type indexname = string * int; 

437 
infix 9 $; 

438 
datatype term = Const of string * typ 

439 
 Free of string * typ 

440 
 Var of indexname * typ 

441 
 Bound of int 

442 
 Abs of string * typ * term 

443 
 op $ of term * term; 

444 
\end{ttbox} 

445 
\begin{description} 

446 
\item[\ttindexbold{Const}($a$, $T$)] 

447 
is the {\bf constant} with name~$a$ and type~$T$. Constants include 

448 
connectives like $\land$ and $\forall$ (logical constants), as well as 

449 
constants like~0 and~$Suc$. Other constants may be required to define the 

450 
concrete syntax of a logic. 

451 

452 
\item[\ttindexbold{Free}($a$, $T$)] 

453 
is the {\bf free variable} with name~$a$ and type~$T$. 

454 

455 
\item[\ttindexbold{Var}($v$, $T$)] 

456 
is the {\bf scheme variable} with indexname~$v$ and type~$T$. An 

457 
\ttindexbold{indexname} is a string paired with a nonnegative index, or 

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

459 
incrementing their subscripts. Scheme variables are essentially free 

460 
variables, but may be instantiated during unification. 

461 

462 
\item[\ttindexbold{Bound} $i$] 

463 
is the {\bf bound variable} with de Bruijn index~$i$, which counts the 

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

465 
its binding. The representation prevents capture of variables. For more 

466 
information see de Bruijn \cite{debruijn72} or 

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

468 

469 
\item[\ttindexbold{Abs}($a$, $T$, $u$)] 

470 
is the {\bf abstraction} with body~$u$, and whose bound variable has 

471 
name~$a$ and type~$T$. The name is used only for parsing and printing; it 

472 
has no logical significance. 

473 

474 
\item[\tt $t$ \$ $u$] \index{$@{\tt\$}bold} 

475 
is the {\bf application} of~$t$ to~$u$. 

476 
\end{description} 

477 
Application is written as an infix operator in order to aid readability. 

275  478 
For example, here is an \ML\ pattern to recognize firstorder formula of 
104  479 
the form~$A\imp B$, binding the subformulae to~$A$ and~$B$: 
480 
\begin{ttbox} 

481 
Const("Trueprop",_) $ (Const("op >",_) $ A $ B) 

482 
\end{ttbox} 

483 

484 

485 
\section{Certified terms} 

486 
\index{terms!certifiedbold}\index{signatures} 

487 
A term $t$ can be {\bf certified} under a signature to ensure that every 

488 
type in~$t$ is declared in the signature and every constant in~$t$ is 

489 
declared as a constant of the same type in the signature. It must be 

490 
welltyped and must not have any `loose' bound variable 

491 
references.\footnote{This concerns the internal representation of variable 

492 
binding using de Bruijn indexes.} Metarules such as {\tt forall_elim} take 

493 
certified terms as arguments. 

494 

275  495 
Certified terms belong to the abstract type \ttindexbold{cterm}. 
104  496 
Elements of the type can only be created through the certification process. 
497 
In case of error, Isabelle raises exception~\ttindex{TERM}\@. 

498 

499 
\subsection{Printing terms} 

500 
\index{printing!termsbold} 

501 
\begin{ttbox} 

275  502 
string_of_cterm : cterm > string 
104  503 
Sign.string_of_term : Sign.sg > term > string 
504 
\end{ttbox} 

505 
\begin{description} 

275  506 
\item[\ttindexbold{string_of_cterm} $ct$] 
104  507 
displays $ct$ as a string. 
508 

509 
\item[\ttindexbold{Sign.string_of_term} $sign$ $t$] 

510 
displays $t$ as a string, using the syntax of~$sign$. 

511 
\end{description} 

512 

513 
\subsection{Making and inspecting certified terms} 

514 
\begin{ttbox} 

275  515 
cterm_of : Sign.sg > term > cterm 
516 
read_cterm : Sign.sg > string * typ > cterm 

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

104  518 
\end{ttbox} 
519 
\begin{description} 

275  520 
\item[\ttindexbold{cterm_of} $sign$ $t$] \index{signatures} 
104  521 
certifies $t$ with respect to signature~$sign$. 
522 

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

526 
kind of phrase to parse. 

527 

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

531 
subscript are computed during certification. 

532 
\end{description} 

533 

534 

535 
\section{Types} 

536 
\index{typesbold} 

275  537 
Types belong to the \ML\ type \ttindexbold{typ}, which is a concrete 
104  538 
datatype with three constructors. Types are classified by sorts, which are 
539 
lists of classes. A class is represented by a string. 

540 
\begin{ttbox} 

541 
type class = string; 

542 
type sort = class list; 

543 

544 
datatype typ = Type of string * typ list 

545 
 TFree of string * sort 

546 
 TVar of indexname * sort; 

547 

548 
infixr 5 >; 

549 
fun S > T = Type("fun",[S,T]); 

550 
\end{ttbox} 

551 
\begin{description} 

552 
\item[\ttindexbold{Type}($a$, $Ts$)] 

553 
applies the {\bf type constructor} named~$a$ to the type operands~$Ts$. 

554 
Type constructors include~\ttindexbold{fun}, the binary function space 

555 
constructor, as well as nullary type constructors such 

556 
as~\ttindexbold{prop}. Other type constructors may be introduced. In 

557 
expressions, but not in patterns, \hbox{\tt$S$>$T$} is a convenient 

558 
shorthand for function types. 

559 

560 
\item[\ttindexbold{TFree}($a$, $s$)] 

561 
is the {\bf free type variable} with name~$a$ and sort~$s$. 

562 

563 
\item[\ttindexbold{TVar}($v$, $s$)] 

564 
is the {\bf scheme type variable} with indexname~$v$ and sort~$s$. Scheme 

565 
type variables are essentially free type variables, but may be instantiated 

566 
during unification. 

567 
\end{description} 

568 

569 

570 
\section{Certified types} 

571 
\index{types!certifiedbold} 

572 
Certified types, which are analogous to certified terms, have type 

275  573 
\ttindexbold{ctyp}. 
104  574 

575 
\subsection{Printing types} 

576 
\index{printing!typesbold} 

577 
\begin{ttbox} 

275  578 
string_of_ctyp : ctyp > string 
104  579 
Sign.string_of_typ : Sign.sg > typ > string 
580 
\end{ttbox} 

581 
\begin{description} 

275  582 
\item[\ttindexbold{string_of_ctyp} $cT$] 
104  583 
displays $cT$ as a string. 
584 

585 
\item[\ttindexbold{Sign.string_of_typ} $sign$ $T$] 

586 
displays $T$ as a string, using the syntax of~$sign$. 

587 
\end{description} 

588 

589 

590 
\subsection{Making and inspecting certified types} 

591 
\begin{ttbox} 

275  592 
ctyp_of : Sign.sg > typ > ctyp 
593 
rep_ctyp : ctyp > \{T: typ, sign: Sign.sg\} 

104  594 
\end{ttbox} 
595 
\begin{description} 

275  596 
\item[\ttindexbold{ctyp_of} $sign$ $T$] \index{signatures} 
104  597 
certifies $T$ with respect to signature~$sign$. 
598 

275  599 
\item[\ttindexbold{rep_ctyp} $cT$] 
104  600 
decomposes $cT$ as a record containing the type itself and its signature. 
601 
\end{description} 

602 

603 
\index{theories)} 