author  lcp 
Mon, 21 Mar 1994 11:02:57 +0100  
changeset 286  e7efbf03562b 
parent 275  933ec96c522e 
child 324  34bc15b546e6 
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 

286  26 
\section{Defining Theories}\label{DefiningTheories} 
104  27 

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

286  29 
\ML{} functions (see \S\ref{BuildingATheory}). Appendix~\ref{app:TheorySyntax} 
30 
presents the concrete syntax for theories. A theory definition consists of 

31 
several different parts: 

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

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

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

37 
is called {\tt Pure}. 

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

38 

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

41 
\S\ref{LoadingTheories} for details. 

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

44 
structures. Isabelle automatically computes the transitive closure of 

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

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

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

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

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

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

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

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

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

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

286  58 
synonym}\indexbold{types!synonyms} is simply an abbreviation 
275  59 
$(\alpha@1,\dots,\alpha@n)name = \mbox{\tt"}\tau\mbox{\tt"}$ and follows 
60 
the same rules as in \ML, except that $name$ can be a string and $\tau$ 

61 
must be enclosed in quotation marks. 

104  62 
\item[$infix$] declares a type or constant to be an infix operator of 
286  63 
priority $nat$ associating to the left ({\tt infixl}) or right ({\tt 
104  64 
infixr}). 
273  65 
\item[$arities$] Each $name$ must be an existing type constructor which is 
66 
given the additional arity $arity$. 

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

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

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

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

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

286  74 
priority of each argument is given by a list of natural numbers, the 
75 
priority of the whole construct by the following natural number; 

76 
priorities are optional. 

104  77 

273  78 
\item Binary constants can be given infix status. 
104  79 

286  80 
\item A constant $f$ {\tt::} $(\tau@1\To\tau@2)\To\tau@3$ can be given {\bf 
81 
binder} status: the declaration {\tt binder} $\cal Q$ $p$ causes 

82 
${\cal Q}\,x.F(x)$ to be treated 

83 
like $f(F)$, where $p$ is the priority. 

273  84 
\end{itemize} 
85 
\item[$trans$] Specifies syntactic translation rules, that is parse 

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

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

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

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

95 

275  96 
\subsection{*Classes and arities} 
286  97 
\index{*classes!context conditions}\index{*arities!context conditions} 
145  98 

286  99 
In order to guarantee principal types~\cite{nipkowprehofer}, 
100 
classes and arities must obey two conditions: 

145  101 
\begin{itemize} 
286  102 
\item There must be no two declarations $ty :: (\vec{r})c$ and $ty :: 
103 
(\vec{s})c$ with $\vec{r} \neq \vec{s}$. For example, the following is 

104 
forbidden: 

145  105 
\begin{ttbox} 
275  106 
types 'a ty 
145  107 
arities ty :: ({\ttlbrace}logic{\ttrbrace}) logic 
108 
ty :: ({\ttlbrace}{\ttrbrace})logic 

109 
\end{ttbox} 

286  110 

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

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

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

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

286  116 
types represented by $s$. For example, the following is forbidden: 
145  117 
\begin{ttbox} 
118 
classes term < logic 

275  119 
types 'a ty 
145  120 
arities ty :: ({\ttlbrace}logic{\ttrbrace})logic 
121 
ty :: ({\ttlbrace}{\ttrbrace})term 

122 
\end{ttbox} 

286  123 

145  124 
\end{itemize} 
125 

104  126 

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

128 
\label{LoadingTheories} 
286  129 
\index{theories!loading} 
130 
\begin{ttbox} 

131 
use_thy : string > unit 

132 
time_use_thy : string > unit 

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

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

135 
\end{ttbox} 

136 

137 
\begin{description} 

138 
\item[\ttindexbold{use_thy} $thyname$] 

139 
reads the theory $thyname$ and creates an \ML{} structure as described below. 

275  140 

286  141 
\item[\ttindexbold{time_use_thy} $thyname$] 
142 
calls {\tt use_thy} $thyname$ and reports the time taken. 

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

143 

286  144 
\item[\ttindexbold{loadpath}] 
145 
contains a list of directories to search when locating the files that 

146 
define a theory. This list is only used if the theory name in {\tt 

147 
use_thy} does not specify the path explicitly. 

148 

149 
\item[\ttindexbold{delete_tmpfiles} \tt:= false;] 

150 
suppresses the deletion of temporary files. 

151 
\end{description} 

152 
% 

104  153 
Each theory definition must reside in a separate file. Let the file {\it 
139  154 
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

155 
theories $TB@1$ \dots $TB@n$. Calling \ttindexbold{use_thy}~{\tt"}{\it 
286  156 
TF\/}{\tt"} reads file {\it tf}{\tt.thy}, writes an intermediate \ML{} 
157 
file {\tt.}{\it tf}{\tt.thy.ML}, and reads the latter file. Recursive {\tt 

158 
use_thy} calls load those parent theories that have not been loaded 

159 
previously; the recursion may continue to any depth. One {\tt use_thy} 

160 
call can read an entire logic if all theories are linked appropriately. 

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

161 

286  162 
The result is an \ML\ structure~$TF$ containing a component {\tt thy} for 
163 
the new theory and components $r@1$ \dots $r@n$ for the rules. The 

164 
structure also contains the definitions of the {\tt ML} section, if 

165 
present. The file {\tt.}{\it tf}{\tt.thy.ML} is then deleted if 

166 
\ttindexbold{delete_tmpfiles} is set to {\tt true} and no errors occurred. 

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

167 

286  168 
Finally the file {\it tf}{\tt.ML} is read, if it exists. This file 
169 
normally contains proofs involving the new theory. It is also possible to 

170 
provide only a {\tt.ML} file, with no {\tt.thy} file. In this case the 

171 
{\tt.ML} file must declare an \ML\ structure having the theory's name. If 

172 
both the {\tt.thy} file and a structure declaration in the {\tt.ML} file 

173 
exist, then the latter declaration is used. See {\tt ZF/ex/llist.ML} for 

174 
an example. 

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

175 

286  176 
\indexbold{theories!names of}\indexbold{files!names of} 
273  177 
\begin{warn} 
286  178 
Case is significant. The argument of \ttindex{use_thy} must be the exact 
179 
theory name. The corresponding filenames are derived by appending 

180 
{\tt.thy} or {\tt.ML} to the theory's name {\it after conversion to lower 

181 
case}. 

273  182 
\end{warn} 
138
9ba8bff1addc
added chapter "Defining Theories" and made changes for new Readthy functions
clasohm
parents:
104
diff
changeset

183 

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

184 

286  185 
\section{Reloading modified theories} 
186 
\indexbold{theories!reloading}\index{*update(} 

187 
\begin{ttbox} 

188 
update : unit > unit 

189 
unlink_thy : string > unit 

190 
\end{ttbox} 

191 
Isabelle keeps track of all loaded theories and their files. If 

192 
\ttindex{use_thy} finds that the theory to be loaded has been read before, 

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

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

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

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

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

198 
marks the children as outofdate. 

199 
\begin{warn} 

200 
Changing a theory on disk often makes it necessary to reload all theories 

201 
descended from it. However, {\tt use_thy} reads only one theory, even if 

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

203 
call {\tt update()}. 

204 
\end{warn} 

205 

206 
\begin{description} 

207 
\item[\ttindexbold{update} ()] 

208 
reloads all modified theories and their descendants in the correct order. 

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

209 

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

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

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

214 
\end{description} 

215 

216 

217 
\subsection{Important note for Poly/ML users}\index{Poly/\ML} 

218 
The theory mechanism depends upon reference variables. At the end of a 

219 
Poly/\ML{} session, the contents of references are lost unless they are 

220 
declared in the current database. Assignments to references in the {\tt 

221 
Pure} database are lost, including all information about loaded theories. 

222 

223 
To avoid losing such information (assuming you have loaded some theories) 

224 
you must declare a new {\tt Readthy} structure in the child database: 

225 
\begin{ttbox} 

226 
structure Readthy = ReadthyFUN (structure ThySyn = ThySyn); 

227 
Readthy.loaded_thys := !loaded_thys; 

228 
open Readthy; 

229 
\end{ttbox} 

230 
This copies into the new reference \verb$loaded_thys$ the contents of the 

231 
original reference, which is the list of already loaded theories. 

232 

233 

234 
\subsection{*Pseudo theories}\indexbold{theories!pseudo} 

275  235 
Any automatic reloading facility requires complete knowledge of all 
286  236 
dependencies. Sometimes theories depend on objects created in \ML{} files 
237 
with no associated {\tt.thy} file. Unless such dependencies are documented, 

238 
{\tt update} fails to reload these \ML{} files and the system is left in a 

275  239 
state where some objects, e.g.\ theorems, still refer to old versions of 
240 
theories. This may lead to the error 

241 
\begin{ttbox} 

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

243 
\end{ttbox} 

286  244 
Therefore there is a way to link theories and {\em orphaned\/} \ML{} files  
245 
those without associated {\tt.thy} file. 

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

246 

286  247 
Let us assume we have an orphaned \ML{} file named {\tt orphan.ML} and a theory 
275  248 
$B$ which depends on {\tt orphan.ML} (for example, {\tt b.ML} uses theorems 
249 
that are proved in {\tt orphan.ML}). Then {\tt b.thy} should mention this 

250 
dependence: 

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

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

253 
\end{ttbox} 
275  254 
Although {\tt orphan} is {\em not\/} used in building the base of theory $B$ 
286  255 
(strings stand for \ML{} files rather than {\tt.thy} files and merely document 
275  256 
additional dependencies), {\tt orphan.ML} is loaded automatically when $B$ is 
257 
(re)built. 

258 

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

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

261 
\begin{ttbox} 

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

263 
\end{ttbox} 

286  264 
The resulting theory is a dummy, but it ensures that {\tt update} reloads 
275  265 
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

266 

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

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

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

270 

286  271 
\index{*update)} 
138
9ba8bff1addc
added chapter "Defining Theories" and made changes for new Readthy functions
clasohm
parents:
104
diff
changeset

272 

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$] 

286  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 and use the resulting theorem like an axiom. 

292 
Actually {\tt assume_ax} returns an assumption; \ttindex{result} 

293 
complains about additional assumptions, but \ttindex{uresult} does not. 

104  294 

295 
For example, if {\it formula} is 

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

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

298 
\end{description} 

299 

286  300 
\subsection{Building a theory} 
301 
\label{BuildingATheory} 

302 
\index{theories!constructingbold} 

303 
\begin{ttbox} 

304 
pure_thy: theory 

305 
merge_theories: theory * theory > theory 

306 
extend_theory: theory > string > \(\cdots\) > theory 

307 
\end{ttbox} 

308 
\begin{description} 

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

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

311 
out by \ML\ functions. 

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

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

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

315 
union of the default sorts of the constituent theories. 

316 
\item [\ttindexbold{extend_theory} $thy$ {\tt"}$T${\tt"} $\cdots$] extends 

317 
the theory $thy$ with new types, constants, etc. $T$ identifies the theory 

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

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

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

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

322 
\begin{ttbox} 

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

324 
\end{ttbox} 

325 
\end{description} 

326 

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

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

286  330 
%is the \ML{} equivalent of the following theory definition: 
275  331 
%\begin{ttbox} 
332 
%\(T\) = \(thy\) + 

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

334 
% \dots 

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

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

337 
% \dots 

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

339 
% \dots 

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

341 
% \dots 

342 
%rules \(name\) \(rule\) 

343 
% \dots 

344 
%end 

345 
%\end{ttbox} 

346 
%where 

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

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

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

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

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

352 
%\\ 

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

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

355 
%\end{tabular} 

356 
% 

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

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

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

360 
%latter case is not documented. 

104  361 

362 

363 
\subsection{Inspecting a theory} 

364 
\index{theories!inspectingbold} 

365 
\begin{ttbox} 

366 
print_theory : theory > unit 

367 
axioms_of : theory > (string*thm)list 

368 
parents_of : theory > theory list 

369 
sign_of : theory > Sign.sg 

370 
stamps_of_thy : theory > string ref list 

371 
\end{ttbox} 

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

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

374 
theory. 

375 
\begin{description} 

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

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

378 

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

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

381 

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

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

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

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

386 

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

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

389 

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

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

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

393 
\end{description} 

394 

395 

396 
\section{Terms} 

397 
\index{termsbold} 

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

401 
type indexname = string * int; 

402 
infix 9 $; 

403 
datatype term = Const of string * typ 

404 
 Free of string * typ 

405 
 Var of indexname * typ 

406 
 Bound of int 

407 
 Abs of string * typ * term 

408 
 op $ of term * term; 

409 
\end{ttbox} 

410 
\begin{description} 

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

286  412 
is the {\bf constant} with name~$a$ and type~$T$. Constants include 
413 
connectives like $\land$ and $\forall$ as well as constants like~0 

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

415 
syntax. 

104  416 

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

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

419 

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

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

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

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

424 
incrementing their subscripts. Scheme variables are essentially free 

425 
variables, but may be instantiated during unification. 

426 

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

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

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

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

431 
information see de Bruijn \cite{debruijn72} or 

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

433 

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

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

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

437 
has no logical significance. 

438 

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

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

441 
\end{description} 

286  442 
Application is written as an infix operator to aid readability. 
443 
Here is an \ML\ pattern to recognize firstorder formula of 

104  444 
the form~$A\imp B$, binding the subformulae to~$A$ and~$B$: 
445 
\begin{ttbox} 

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

447 
\end{ttbox} 

448 

449 

286  450 
\section{Terms and variable binding} 
451 
\begin{ttbox} 

452 
loose_bnos : term > int list 

453 
incr_boundvars : int > term > term 

454 
abstract_over : term*term > term 

455 
variant_abs : string * typ * term > string * term 

456 
aconv : term*term > bool\hfill{\bf infix} 

457 
\end{ttbox} 

458 
These functions are all concerned with the de Bruijn representation of 

459 
bound variables. 

460 
\begin{description} 

461 
\item[\ttindexbold{loose_bnos} $t$] 

462 
returns the list of all dangling bound variable references. In 

463 
particular, {\tt Bound~0} is loose unless it is enclosed in an 

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

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

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

467 

468 
\item[\ttindexbold{incr_boundvars} $j$] 

469 
increases a term's dangling bound variables by the offset~$j$. This 

470 
required when moving a subterm into a context where it is enclosed by a 

471 
different number of abstractions. Bound variables with a matching 

472 
abstraction are unaffected. 

473 

474 
\item[\ttindexbold{abstract_over} $(v,t)$] 

475 
forms the abstraction of~$t$ over~$v$, which may be any wellformed term. 

476 
It replaces every occurrence of \(v\) by a {\tt Bound} variable with the 

477 
correct index. 

478 

479 
\item[\ttindexbold{variant_abs} $(a,T,u)$] 

480 
substitutes into $u$, which should be the body of an abstraction. 

481 
It replaces each occurrence of the outermost bound variable by a free 

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

483 
of~$a$ choosen to be distinct from all constants and from all variables 

484 
free in~$u$. 

485 

486 
\item[$t$ \ttindexbold{aconv} $u$] 

487 
tests whether terms~$t$ and~$u$ are \(\alpha\)convertible: identical up 

488 
to renaming of bound variables. 

489 
\begin{itemize} 

490 
\item 

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

492 
if their names and types are equal. 

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

494 
This confusing situation should be avoided!) 

495 
\item 

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

497 
if they have the same number. 

498 
\item 

499 
Two abstractions are \(\alpha\)convertible 

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

501 
\item 

502 
Two applications are \(\alpha\)convertible 

503 
if the corresponding subterms are. 

504 
\end{itemize} 

505 

506 
\end{description} 

507 

508 
\section{Certified terms}\index{terms!certifiedbold}\index{signatures} 

104  509 
A term $t$ can be {\bf certified} under a signature to ensure that every 
510 
type in~$t$ is declared in the signature and every constant in~$t$ is 

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

286  512 
welltyped and its use of bound variables must be wellformed. Metarules 
513 
such as {\tt forall_elim} take certified terms as arguments. 

104  514 

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

518 

519 
\subsection{Printing terms} 

520 
\index{printing!termsbold} 

521 
\begin{ttbox} 

275  522 
string_of_cterm : cterm > string 
104  523 
Sign.string_of_term : Sign.sg > term > string 
524 
\end{ttbox} 

525 
\begin{description} 

275  526 
\item[\ttindexbold{string_of_cterm} $ct$] 
104  527 
displays $ct$ as a string. 
528 

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

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

531 
\end{description} 

532 

533 
\subsection{Making and inspecting certified terms} 

534 
\begin{ttbox} 

275  535 
cterm_of : Sign.sg > term > cterm 
536 
read_cterm : Sign.sg > string * typ > cterm 

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

104  538 
\end{ttbox} 
539 
\begin{description} 

275  540 
\item[\ttindexbold{cterm_of} $sign$ $t$] \index{signatures} 
104  541 
certifies $t$ with respect to signature~$sign$. 
542 

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

546 
kind of phrase to parse. 

547 

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

551 
subscript are computed during certification. 

552 
\end{description} 

553 

554 

286  555 
\section{Types}\index{typesbold} 
275  556 
Types belong to the \ML\ type \ttindexbold{typ}, which is a concrete 
286  557 
datatype with three constructor functions. These correspond to type 
558 
constructors, free type variables and schematic type variables. Types are 

559 
classified by sorts, which are lists of classes. A class is represented by 

560 
a string. 

104  561 
\begin{ttbox} 
562 
type class = string; 

563 
type sort = class list; 

564 

565 
datatype typ = Type of string * typ list 

566 
 TFree of string * sort 

567 
 TVar of indexname * sort; 

568 

569 
infixr 5 >; 

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

571 
\end{ttbox} 

572 
\begin{description} 

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

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

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

576 
constructor, as well as nullary type constructors such 

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

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

579 
shorthand for function types. 

580 

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

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

583 

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

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

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

587 
during unification. 

588 
\end{description} 

589 

590 

591 
\section{Certified types} 

592 
\index{types!certifiedbold} 

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

275  594 
\ttindexbold{ctyp}. 
104  595 

596 
\subsection{Printing types} 

597 
\index{printing!typesbold} 

598 
\begin{ttbox} 

275  599 
string_of_ctyp : ctyp > string 
104  600 
Sign.string_of_typ : Sign.sg > typ > string 
601 
\end{ttbox} 

602 
\begin{description} 

275  603 
\item[\ttindexbold{string_of_ctyp} $cT$] 
104  604 
displays $cT$ as a string. 
605 

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

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

608 
\end{description} 

609 

610 

611 
\subsection{Making and inspecting certified types} 

612 
\begin{ttbox} 

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

104  615 
\end{ttbox} 
616 
\begin{description} 

275  617 
\item[\ttindexbold{ctyp_of} $sign$ $T$] \index{signatures} 
104  618 
certifies $T$ with respect to signature~$sign$. 
619 

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

623 

624 
\index{theories)} 