3 \chapter{Theories, Terms and Types} \label{theories}
4 \index{theories|(}\index{signatures|bold}
5 \index{reading!axioms|see{{\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
8 and merging existing theories. They have the \ML\ type \mltydx{theory}.
9 Theory operations signal errors by raising exception \xdx{THEORY},
10 returning a message and a list of theories.
12 Signatures, which contain information about sorts, types, constants and
13 syntax, have the \ML\ type~\mltydx{Sign.sg}. For identification, each
14 signature carries a unique list of \bfindex{stamps}, which are \ML\
15 references to strings. The strings serve as human-readable 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.
20 Terms and types are the underlying representation of logical syntax. Their
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
24 `certified' to be well-formed with respect to a given signature.
27 \section{Defining theories}\label{sec:ref-defining-theories}
29 Theories are usually defined using theory definition files (which have a name
30 suffix {\tt .thy}). There is also a low level interface provided by certain
31 \ML{} functions (see \S\ref{BuildingATheory}).
32 Appendix~\ref{app:TheorySyntax} presents the concrete syntax for theory
33 definitions; here is an explanation of the constituent parts:
35 \item[{\it theoryDef}]
36 is the full definition. The new theory is called $id$. It is the union
37 of the named {\bf parent theories}\indexbold{theories!parent}, possibly
38 extended with new classes, etc. The basic theory, which contains only
39 the meta-logic, is called \thydx{Pure}.
41 Normally each {\it name\/} is an identifier, the name of the parent theory.
42 Quoted strings can be used to document additional file dependencies; see
43 \S\ref{LoadingTheories} for details.
46 is a series of class declarations. Declaring {\tt$id$ < $id@1$ \dots\
47 $id@n$} makes $id$ a subclass of the existing classes $id@1\dots
48 id@n$. This rules out cyclic class structures. Isabelle automatically
49 computes the transitive closure of subclass hierarchies; it is not
50 necessary to declare {\tt c < e} in addition to {\tt c < d} and {\tt d <
54 introduces $sort$ as the new default sort for type variables. This applies
55 to unconstrained type variables in an input string but not to type
56 variables created internally. If omitted, the default sort is the listwise
57 union of the default sorts of the parent theories (i.e.\ their logical
61 is a finite set of classes. A single class $id$ abbreviates the singleton
62 set {\tt\{}$id${\tt\}}.
65 is a series of type declarations. Each declares a new type constructor
66 or type synonym. An $n$-place type constructor is specified by
67 $(\alpha@1,\dots,\alpha@n)name$, where the type variables serve only to
68 indicate the number~$n$.
70 A {\bf type synonym}\indexbold{type synonyms} is an abbreviation
71 $(\alpha@1,\dots,\alpha@n)name = \mbox{\tt"}\tau\mbox{\tt"}$, where
72 $name$ can be a string and $\tau$ must be enclosed in quotation marks.
75 declares a type or constant to be an infix operator of priority $nat$
76 associating to the left ({\tt infixl}) or right ({\tt infixr}). Only
77 2-place type constructors can have infix status; an example is {\tt
78 ('a,'b)~"*"~(infixr~20)}, which expresses binary product types.
81 is a series of arity declarations. Each assigns arities to type
82 constructors. The $name$ must be an existing type constructor, which is
83 given the additional arity $arity$.
86 is a series of constant declarations. Each new constant $name$ is given
87 the type specified by the $string$. The optional $mixfix$ annotations may
88 attach concrete syntax to the constant. A variant of {\tt consts} is the
89 {\tt syntax} section\index{*syntax section}, which adds just syntax without
90 declaring logical constants.
92 \item[$mixfix$] \index{mixfix declarations}
93 annotations can take three forms:
95 \item A mixfix template given as a $string$ of the form
96 {\tt"}\dots{\tt\_}\dots{\tt\_}\dots{\tt"} where the $i$-th underscore
97 indicates the position where the $i$-th argument should go. The list
98 of numbers gives the priority of each argument. The final number gives
99 the priority of the whole construct.
101 \item A constant $f$ of type $\tau@1\To(\tau@2\To\tau)$ can be given {\bf
104 \item A constant $f$ of type $(\tau@1\To\tau@2)\To\tau$ can be given {\bf
105 binder} status. The declaration {\tt binder} $\cal Q$ $p$ causes
106 ${\cal Q}\,x.F(x)$ to be treated
107 like $f(F)$, where $p$ is the priority.
111 specifies syntactic translation rules (macros). There are three forms:
112 parse rules ({\tt =>}), print rules ({\tt <=}), and parse/print rules ({\tt
116 is a series of rule declarations. Each has a name $id$ and the formula is
117 given by the $string$. Rule names must be distinct within any single
120 \item[$ml$] \index{*ML section}
121 consists of \ML\ code, typically for parse and print translation functions.
124 Chapters~\ref{Defining-Logics} and \ref{chap:syntax} explain mixfix
125 declarations, translation rules and the {\tt ML} section in more detail.
128 \subsection{*Classes and arities}
129 \index{classes!context conditions}\index{arities!context conditions}
131 In order to guarantee principal types~\cite{nipkow-prehofer},
132 arity declarations must obey two conditions:
134 \item There must be no two declarations $ty :: (\vec{r})c$ and $ty ::
135 (\vec{s})c$ with $\vec{r} \neq \vec{s}$. For example, the following is
141 ty :: ({\ttlbrace}logic{\ttrbrace}) logic
142 ty :: ({\ttlbrace}{\ttrbrace})logic
145 \item If there are two declarations $ty :: (s@1,\dots,s@n)c$ and $ty ::
146 (s@1',\dots,s@n')c'$ such that $c' < c$ then $s@i' \preceq s@i$ must hold
147 for $i=1,\dots,n$. The relationship $\preceq$, defined as
148 \[ s' \preceq s \iff \forall c\in s. \exists c'\in s'.~ c'\le c, \]
149 expresses that the set of types represented by $s'$ is a subset of the set of
150 types represented by $s$. For example, the following is forbidden:
157 ty :: ({\ttlbrace}logic{\ttrbrace})logic
158 ty :: ({\ttlbrace}{\ttrbrace})term
164 \section{Loading a new theory}\label{LoadingTheories}
165 \index{theories!loading}\index{files!reading}
167 use_thy : string -> unit
168 time_use_thy : string -> unit
169 loadpath : string list ref \hfill{\bf initially {\tt["."]}}
170 delete_tmpfiles : bool ref \hfill{\bf initially true}
173 \begin{ttdescription}
174 \item[\ttindexbold{use_thy} $thyname$]
175 reads the theory $thyname$ and creates an \ML{} structure as described below.
177 \item[\ttindexbold{time_use_thy} $thyname$]
178 calls {\tt use_thy} $thyname$ and reports the time taken.
180 \item[\ttindexbold{loadpath}]
181 contains a list of directories to search when locating the files that
182 define a theory. This list is only used if the theory name in {\tt
183 use_thy} does not specify the path explicitly.
185 \item[\ttindexbold{delete_tmpfiles} := false;]
186 suppresses the deletion of temporary files.
189 Each theory definition must reside in a separate file. Let the file {\it
190 T}{\tt.thy} contain the definition of a theory called~$T$, whose parent
191 theories are $TB@1$ \dots $TB@n$. Calling \ttindexbold{use_thy}~{\tt"{\it
192 T\/}"} reads the file {\it T}{\tt.thy}, writes a temporary \ML{}
193 file {\tt.{\it T}.thy.ML}, and reads the latter file. Recursive {\tt
194 use_thy} calls load those parent theories that have not been loaded
195 previously; the recursive calls may continue to any depth. One {\tt use_thy}
196 call can read an entire logic provided all theories are linked appropriately.
198 The result is an \ML\ structure~$T$ containing at least a component {\tt thy}
199 for the new theory and components for each of the rules. The structure also
200 contains the definitions of the {\tt ML} section, if present. The file
201 {\tt.{\it T}.thy.ML} is then deleted if {\tt delete_tmpfiles} is set to {\tt
202 true} and no errors occurred.
204 Finally the file {\it T}{\tt.ML} is read, if it exists. This file normally
205 begins with the declaration {\tt open~$T$} and contains proofs involving
208 Some applications construct theories directly by calling \ML\ functions. In
209 this situation there is no {\tt.thy} file, only an {\tt.ML} file. The
210 {\tt.ML} file must declare an \ML\ structure having the theory's name and a
211 component {\tt thy} containing the new theory object.
212 Section~\ref{sec:pseudo-theories} below describes a way of linking such
213 theories to their parents.
216 Temporary files are written to the current directory, so this must be
217 writable. Isabelle inherits the current directory from the operating
218 system; you can change it within Isabelle by typing {\tt
219 cd"$dir$"}\index{*cd}.
223 \section{Reloading modified theories}\label{sec:reloading-theories}
224 \indexbold{theories!reloading}
226 update : unit -> unit
227 unlink_thy : string -> unit
229 Changing a theory on disk often makes it necessary to reload all theories
230 descended from it. However, {\tt use_thy} reads only one theory, even if
231 some of the parent theories are out of date. In this case you should call
234 Isabelle keeps track of all loaded theories and their files. If
235 \ttindex{use_thy} finds that the theory to be loaded has been read before,
236 it determines whether to reload the theory as follows. First it looks for
237 the theory's files in their previous location. If it finds them, it
238 compares their modification times to the internal data and stops if they
239 are equal. If the files have been moved, {\tt use_thy} searches for them
240 as it would for a new theory. After {\tt use_thy} reloads a theory, it
241 marks the children as out-of-date.
243 \begin{ttdescription}
244 \item[\ttindexbold{update}()]
245 reloads all modified theories and their descendants in the correct order.
247 \item[\ttindexbold{unlink_thy} $thyname$]\indexbold{theories!removing}
248 informs Isabelle that theory $thyname$ no longer exists. If you delete the
249 theory files for $thyname$ then you must execute {\tt unlink_thy};
250 otherwise {\tt update} will complain about a missing file.
255 \subsection{Important note for Poly/ML users}\index{Poly/{\ML} compiler}
256 The theory mechanism depends upon reference variables. At the end of a
257 Poly/\ML{} session, the contents of references are lost unless they are
258 declared in the current database. In particular, assignments to references
259 of the {\tt Pure} database are lost, including all information about loaded
260 theories. To avoid losing this information simply call
264 when building the new database.
267 \subsection{*Pseudo theories}\label{sec:pseudo-theories}
268 \indexbold{theories!pseudo}%
269 Any automatic reloading facility requires complete knowledge of all
270 dependencies. Sometimes theories depend on objects created in \ML{} files
271 with no associated theory definition file. These objects may be theories but
272 they could also be theorems, proof procedures, etc.
274 Unless such dependencies are documented, {\tt update} fails to reload these
275 \ML{} files and the system is left in a state where some objects, such as
276 theorems, still refer to old versions of theories. This may lead to the
279 Attempt to merge different versions of theories: \dots
281 Therefore there is a way to link theories and {\bf orphaned} \ML{} files ---
282 those not associated with a theory definition.
284 Let us assume we have an orphaned \ML{} file named {\tt orphan.ML} and a
285 theory~$B$ that depends on {\tt orphan.ML} --- for example, {\tt B.ML} uses
286 theorems proved in {\tt orphan.ML}. Then {\tt B.thy} should
287 mention this dependency as follows:
289 B = \(\ldots\) + "orphan" + \(\ldots\)
291 Quoted strings stand for theories which have to be loaded before the
292 current theory is read but which are not used in building the base of
293 theory~$B$. Whenever {\tt orphan} changes and is reloaded, Isabelle
294 knows that $B$ has to be updated, too.
296 Note that it's necessary for {\tt orphan} to declare a special ML
297 object of type {\tt theory} which is present in all theories. This is
298 normally achieved by adding the file {\tt orphan.thy} to make {\tt
299 orphan} a {\bf pseudo theory}. A minimum version of {\tt orphan.thy}
306 which uses {\tt Pure} to make a dummy theory. Normally though the
307 orphaned file has its own dependencies. If {\tt orphan.ML} depends on
308 theories or files $A@1$, \ldots, $A@n$, record this by creating the
309 pseudo theory in the following way:
311 orphan = \(A@1\) + \(\ldots\) + \(A@n\)
313 The resulting theory ensures that {\tt update} reloads {\tt orphan}
314 whenever it reloads one of the $A@i$.
316 For an extensive example of how this technique can be used to link lots of
317 theory files and load them by just a few {\tt use_thy} calls, consult the
318 sources of \ZF{} set theory.
322 \section{Basic operations on theories}\label{BasicOperationsOnTheories}
323 \subsection{Extracting an axiom or theorem from a theory}
324 \index{theories!axioms of}\index{axioms!extracting}
325 \index{theories!theorems of}\index{theorems!extracting}
327 get_axiom : theory -> string -> thm
328 get_thm : theory -> string -> thm
329 assume_ax : theory -> string -> thm
331 \begin{ttdescription}
332 \item[\ttindexbold{get_axiom} $thy$ $name$]
333 returns an axiom with the given $name$ from $thy$, raising exception
334 \xdx{THEORY} if none exists. Merging theories can cause several axioms
335 to have the same name; {\tt get_axiom} returns an arbitrary one.
337 \item[\ttindexbold{get_thm} $thy$ $name$]
338 is analogous to {\tt get_axiom}, but looks for a stored theorem. Like
339 {\tt get_axiom} it searches all parents of a theory if the theorem
340 is not associated with $thy$.
342 \item[\ttindexbold{assume_ax} $thy$ $formula$]
343 reads the {\it formula} using the syntax of $thy$, following the same
344 conventions as axioms in a theory definition. You can thus pretend that
345 {\it formula} is an axiom and use the resulting theorem like an axiom.
346 Actually {\tt assume_ax} returns an assumption; \ttindex{result}
347 complains about additional assumptions, but \ttindex{uresult} does not.
349 For example, if {\it formula} is
350 \hbox{\tt a=b ==> b=a} then the resulting theorem has the form
351 \hbox{\verb'?a=?b ==> ?b=?a [!!a b. a=b ==> b=a]'}
354 \subsection{Building a theory}
355 \label{BuildingATheory}
356 \index{theories!constructing|bold}
359 merge_theories : theory * theory -> theory
361 \begin{ttdescription}
362 \item[\ttindexbold{pure_thy}] contains just the syntax and signature
363 of the meta-logic. There are no axioms: meta-level inferences are carried
364 out by \ML\ functions.
365 \item[\ttindexbold{merge_theories} ($thy@1$, $thy@2$)] merges the two
366 theories $thy@1$ and $thy@2$. The resulting theory contains all of the
367 syntax, signature and axioms of the constituent theories. Merging theories
368 that contain different identification stamps of the same name fails with
369 the following message
371 Attempt to merge different versions of theories: "\(T@1\)", \(\ldots\), "\(T@n\)"
373 This error may especially occur when a theory is redeclared --- say to
374 change an incorrect axiom --- and bindings to old versions persist.
375 Isabelle ensures that old and new theories of the same name are not
379 %\item [\ttindexbold{extend_theory} $thy$ {\tt"}$T${\tt"} $\cdots$] extends
380 % the theory $thy$ with new types, constants, etc. $T$ identifies the theory
381 % internally. When a theory is redeclared, say to change an incorrect axiom,
382 % bindings to the old axiom may persist. Isabelle ensures that the old and
383 % new theories are not involved in the same proof. Attempting to combine
384 % different theories having the same name $T$ yields the fatal error
385 %extend_theory : theory -> string -> \(\cdots\) -> theory
387 %Attempt to merge different versions of theory: \(T\)
392 %\item [\ttindexbold{extend_theory} $thy$ {\tt"}$T${\tt"}
393 % ($classes$, $default$, $types$, $arities$, $consts$, $sextopt$) $rules$]
394 %\hfill\break %%% include if line is just too short
395 %is the \ML{} equivalent of the following theory definition:
398 %classes \(c\) < \(c@1\),\(\dots\),\(c@m\)
400 %default {\(d@1,\dots,d@r\)}
401 %types \(tycon@1\),\dots,\(tycon@i\) \(n\)
403 %arities \(tycon@1'\),\dots,\(tycon@j'\) :: (\(s@1\),\dots,\(s@n\))\(c\)
405 %consts \(b@1\),\dots,\(b@k\) :: \(\tau\)
407 %rules \(name\) \(rule\)
412 %\begin{tabular}[t]{l@{~=~}l}
413 %$classes$ & \tt[("$c$",["$c@1$",\dots,"$c@m$"]),\dots] \\
414 %$default$ & \tt["$d@1$",\dots,"$d@r$"]\\
415 %$types$ & \tt[([$tycon@1$,\dots,$tycon@i$], $n$),\dots] \\
416 %$arities$ & \tt[([$tycon'@1$,\dots,$tycon'@j$], ([$s@1$,\dots,$s@n$],$c$)),\dots]
418 %$consts$ & \tt[([$b@1$,\dots,$b@k$],$\tau$),\dots] \\
419 %$rules$ & \tt[("$name$",$rule$),\dots]
423 \subsection{Inspecting a theory}\label{sec:inspct-thy}
424 \index{theories!inspecting|bold}
426 print_theory : theory -> unit
427 axioms_of : theory -> (string * thm) list
428 thms_of : theory -> (string * thm) list
429 parents_of : theory -> theory list
430 sign_of : theory -> Sign.sg
431 stamps_of_thy : theory -> string ref list
433 These provide means of viewing a theory's components.
434 \begin{ttdescription}
435 \item[\ttindexbold{print_theory} $thy$]
436 prints the contents of $thy$ excluding the syntax related parts (which are
437 shown by {\tt print_syntax}). The output is quite verbose.
439 \item[\ttindexbold{axioms_of} $thy$]
440 returns the additional axioms of the most recent extend node of~$thy$.
442 \item[\ttindexbold{thms_of} $thy$]
443 returns all theorems that are associated with $thy$.
445 \item[\ttindexbold{parents_of} $thy$]
446 returns the direct ancestors of~$thy$.
448 \item[\ttindexbold{sign_of} $thy$]
449 returns the signature associated with~$thy$. It is useful with functions
450 like {\tt read_instantiate_sg}, which take a signature as an argument.
452 \item[\ttindexbold{stamps_of_thy} $thy$]\index{signatures}
453 returns the identification \rmindex{stamps} of the signature associated
458 \section{Viewing theories as HTML documents}
461 Isabelle is able to make HTML documents that show a theory's
462 definition, the theorems proved in its ML file and the relationship
463 with its ancestors and descendants. HTML stands for Hypertext Markup
464 Language and is used in the World Wide Web to represent text
465 containing images and links to other documents. Web browsers like the
466 ones from Mosaic or Netscape are used to view these documents.
468 Besides the three HTML files that are made for every theory
469 (definition and theorems, ancestors, descendants), Isabelle stores
470 links to all theories in an index file. These indexes are themself
471 linked with other indexes.
473 To make HTML files for logics that are part of the Isabelle
474 distribution, simply set the environment variable {\tt MAKE_HTML}
475 before compiling a logic. The entry point to all logics is the {\tt
476 index.html} file located in Isabelle's main directory. You also can
477 access a HTML version of the Isabelle distribution package at
480 http://www4.informatik.tu-muenchen.de/~nipkow/isabelle
483 Internally the HTML generation is controlled by
486 index_path : string ref
487 gif_path : string ref
488 base_path : string ref
489 init_html : unit -> unit
491 finish_html : unit -> unit
494 \begin{ttdescription}
495 \item[\ttindexbold{base_path}]
496 contains the absolute path of Isabelle's main directory. To make them
497 independent from their storage place, the HTML files only contain
498 relative paths which are derived from absolute ones like the current
499 working directory, {\tt index_path} or {\tt base_path}.
501 As {\tt base_path} and {\tt gif_path} are set at the time when the
502 {\tt Pure} database is made, they are not valid if you use someone
503 else's database to read theories stored in your private directory. In
504 that case you first have to set {\tt base_path} to the value of {\em
505 your} Isabelle main directory, i.e. the directory that contains the
506 subdirectories where logics like {\tt FOL}, {\tt HOL} etc. are
507 stored. Besides you have to set the next variable:
509 \item[\ttindexbold{gif_path}]
510 contains the absolute path of two GIF images used in the HTML
511 documents. Normally it points to the {\tt Tools} subdirectory of
512 Isabelle's main directory. As with {\tt base_path} you have to set it
513 manually if you use someone else's database.
515 \item[\ttindexbold{init_html}]
516 activates the HTML facility. It stores the current working directory
517 in {\tt index_path} which is were the {\tt index.html} file for all
518 theories loaded afterwards will be placed.
520 \item[\ttindexbold{make_html}]
521 is a variable read by {\tt use_thy} to decide whether HTML files
522 should be made or not. After you have used {\tt init_html} you can
523 manually change {\tt make_html}'s value to temporarily disable HTML
526 \item[\ttindexbold{finish_html}]
527 has to be called after all theories have been read that should be
528 contained in the current {\tt index.html} file. It reads a temporary
529 file with information about the theories read since the last use of
530 {\tt init_html} and makes the {\tt index.html} file. If {\tt
531 make_html} is {\tt false} nothing is done.
533 The indexes made by this function also contain a link to the {\tt
534 README} file if there exists one in the directory were the index is
535 stored. If there's a {\tt README.html} file it's used instead of the
540 Please note that the HTML facility was developed to make HTML
541 documents for a stable version of a logic. It is not intended to make
542 these documents for a logic were theories are changed and only a part
543 of the logic is reread.
545 If you add new subdirectories to Isabelle's logics (or add a completly
546 new logic), you would have to call {\tt init_html} at the start of the
547 directory's {\tt ROOT.ML} file and {\tt finish_html} at the end of
548 it. This is automatically done if you use
551 use_dir : string -> unit
554 This function takes a path as its parameter, changes the working
555 directory, calls {\tt init_html} if {\tt make_html} is {\tt true},
556 executes {\tt ROOT.ML}, and calls {\tt finish_html}. The {\tt
557 index.html} file written in this directory will be automatically
558 linked to the first index found in the (recursively searched)
564 Terms belong to the \ML\ type \mltydx{term}, which is a concrete datatype
565 with six constructors: there are six kinds of term.
567 type indexname = string * int;
569 datatype term = Const of string * typ
570 | Free of string * typ
571 | Var of indexname * typ
573 | Abs of string * typ * term
574 | op $ of term * term;
576 \begin{ttdescription}
577 \item[\ttindexbold{Const}($a$, $T$)] \index{constants|bold}
578 is the {\bf constant} with name~$a$ and type~$T$. Constants include
579 connectives like $\land$ and $\forall$ as well as constants like~0
580 and~$Suc$. Other constants may be required to define a logic's concrete
583 \item[\ttindexbold{Free}($a$, $T$)] \index{variables!free|bold}
584 is the {\bf free variable} with name~$a$ and type~$T$.
586 \item[\ttindexbold{Var}($v$, $T$)] \index{unknowns|bold}
587 is the {\bf scheme variable} with indexname~$v$ and type~$T$. An
588 \mltydx{indexname} is a string paired with a non-negative index, or
589 subscript; a term's scheme variables can be systematically renamed by
590 incrementing their subscripts. Scheme variables are essentially free
591 variables, but may be instantiated during unification.
593 \item[\ttindexbold{Bound} $i$] \index{variables!bound|bold}
594 is the {\bf bound variable} with de Bruijn index~$i$, which counts the
595 number of lambdas, starting from zero, between a variable's occurrence
596 and its binding. The representation prevents capture of variables. For
597 more information see de Bruijn \cite{debruijn72} or
598 Paulson~\cite[page~336]{paulson91}.
600 \item[\ttindexbold{Abs}($a$, $T$, $u$)]
601 \index{lambda abs@$\lambda$-abstractions|bold}
602 is the $\lambda$-{\bf abstraction} with body~$u$, and whose bound
603 variable has name~$a$ and type~$T$. The name is used only for parsing
604 and printing; it has no logical significance.
606 \item[$t$ \$ $u$] \index{$@{\tt\$}|bold} \index{function applications|bold}
607 is the {\bf application} of~$t$ to~$u$.
609 Application is written as an infix operator to aid readability.
610 Here is an \ML\ pattern to recognize \FOL{} formulae of
611 the form~$A\imp B$, binding the subformulae to~$A$ and~$B$:
613 Const("Trueprop",_) $ (Const("op -->",_) $ A $ B)
617 \section{Variable binding}
619 loose_bnos : term -> int list
620 incr_boundvars : int -> term -> term
621 abstract_over : term*term -> term
622 variant_abs : string * typ * term -> string * term
623 aconv : term*term -> bool\hfill{\bf infix}
625 These functions are all concerned with the de Bruijn representation of
627 \begin{ttdescription}
628 \item[\ttindexbold{loose_bnos} $t$]
629 returns the list of all dangling bound variable references. In
630 particular, {\tt Bound~0} is loose unless it is enclosed in an
631 abstraction. Similarly {\tt Bound~1} is loose unless it is enclosed in
632 at least two abstractions; if enclosed in just one, the list will contain
633 the number 0. A well-formed term does not contain any loose variables.
635 \item[\ttindexbold{incr_boundvars} $j$]
636 increases a term's dangling bound variables by the offset~$j$. This is
637 required when moving a subterm into a context where it is enclosed by a
638 different number of abstractions. Bound variables with a matching
639 abstraction are unaffected.
641 \item[\ttindexbold{abstract_over} $(v,t)$]
642 forms the abstraction of~$t$ over~$v$, which may be any well-formed term.
643 It replaces every occurrence of \(v\) by a {\tt Bound} variable with the
646 \item[\ttindexbold{variant_abs} $(a,T,u)$]
647 substitutes into $u$, which should be the body of an abstraction.
648 It replaces each occurrence of the outermost bound variable by a free
649 variable. The free variable has type~$T$ and its name is a variant
650 of~$a$ chosen to be distinct from all constants and from all variables
653 \item[$t$ \ttindexbold{aconv} $u$]
654 tests whether terms~$t$ and~$u$ are \(\alpha\)-convertible: identical up
655 to renaming of bound variables.
658 Two constants, {\tt Free}s, or {\tt Var}s are \(\alpha\)-convertible
659 if their names and types are equal.
660 (Variables having the same name but different types are thus distinct.
661 This confusing situation should be avoided!)
663 Two bound variables are \(\alpha\)-convertible
664 if they have the same number.
666 Two abstractions are \(\alpha\)-convertible
667 if their bodies are, and their bound variables have the same type.
669 Two applications are \(\alpha\)-convertible
670 if the corresponding subterms are.
675 \section{Certified terms}\index{terms!certified|bold}\index{signatures}
676 A term $t$ can be {\bf certified} under a signature to ensure that every type
677 in~$t$ is well-formed and every constant in~$t$ is a type instance of a
678 constant declared in the signature. The term must be well-typed and its use
679 of bound variables must be well-formed. Meta-rules such as {\tt forall_elim}
680 take certified terms as arguments.
682 Certified terms belong to the abstract type \mltydx{cterm}.
683 Elements of the type can only be created through the certification process.
684 In case of error, Isabelle raises exception~\ttindex{TERM}\@.
686 \subsection{Printing terms}
687 \index{terms!printing of}
689 string_of_cterm : cterm -> string
690 Sign.string_of_term : Sign.sg -> term -> string
692 \begin{ttdescription}
693 \item[\ttindexbold{string_of_cterm} $ct$]
694 displays $ct$ as a string.
696 \item[\ttindexbold{Sign.string_of_term} $sign$ $t$]
697 displays $t$ as a string, using the syntax of~$sign$.
700 \subsection{Making and inspecting certified terms}
702 cterm_of : Sign.sg -> term -> cterm
703 read_cterm : Sign.sg -> string * typ -> cterm
704 cert_axm : Sign.sg -> string * term -> string * term
705 read_axm : Sign.sg -> string * string -> string * term
706 rep_cterm : cterm -> \{T:typ, t:term, sign:Sign.sg, maxidx:int\}
708 \begin{ttdescription}
709 \item[\ttindexbold{cterm_of} $sign$ $t$] \index{signatures}
710 certifies $t$ with respect to signature~$sign$.
712 \item[\ttindexbold{read_cterm} $sign$ ($s$, $T$)]
713 reads the string~$s$ using the syntax of~$sign$, creating a certified term.
714 The term is checked to have type~$T$; this type also tells the parser what
715 kind of phrase to parse.
717 \item[\ttindexbold{cert_axm} $sign$ ($name$, $t$)]
718 certifies $t$ with respect to $sign$ as a meta-proposition and converts all
719 exceptions to an error, including the final message
721 The error(s) above occurred in axiom "\(name\)"
724 \item[\ttindexbold{read_axm} $sign$ ($name$, $s$)]
725 similar to {\tt cert_axm}, but first reads the string $s$ using the syntax of
728 \item[\ttindexbold{rep_cterm} $ct$]
729 decomposes $ct$ as a record containing its type, the term itself, its
730 signature, and the maximum subscript of its unknowns. The type and maximum
731 subscript are computed during certification.
735 \section{Types}\index{types|bold}
736 Types belong to the \ML\ type \mltydx{typ}, which is a concrete datatype with
737 three constructor functions. These correspond to type constructors, free
738 type variables and schematic type variables. Types are classified by sorts,
739 which are lists of classes (representing an intersection). A class is
740 represented by a string.
743 type sort = class list;
745 datatype typ = Type of string * typ list
746 | TFree of string * sort
747 | TVar of indexname * sort;
750 fun S --> T = Type ("fun", [S, T]);
752 \begin{ttdescription}
753 \item[\ttindexbold{Type}($a$, $Ts$)] \index{type constructors|bold}
754 applies the {\bf type constructor} named~$a$ to the type operands~$Ts$.
755 Type constructors include~\tydx{fun}, the binary function space
756 constructor, as well as nullary type constructors such as~\tydx{prop}.
757 Other type constructors may be introduced. In expressions, but not in
758 patterns, \hbox{\tt$S$-->$T$} is a convenient shorthand for function
761 \item[\ttindexbold{TFree}($a$, $s$)] \index{type variables|bold}
762 is the {\bf type variable} with name~$a$ and sort~$s$.
764 \item[\ttindexbold{TVar}($v$, $s$)] \index{type unknowns|bold}
765 is the {\bf type unknown} with indexname~$v$ and sort~$s$.
766 Type unknowns are essentially free type variables, but may be
767 instantiated during unification.
771 \section{Certified types}
772 \index{types!certified|bold}
773 Certified types, which are analogous to certified terms, have type
776 \subsection{Printing types}
777 \index{types!printing of}
779 string_of_ctyp : ctyp -> string
780 Sign.string_of_typ : Sign.sg -> typ -> string
782 \begin{ttdescription}
783 \item[\ttindexbold{string_of_ctyp} $cT$]
784 displays $cT$ as a string.
786 \item[\ttindexbold{Sign.string_of_typ} $sign$ $T$]
787 displays $T$ as a string, using the syntax of~$sign$.
791 \subsection{Making and inspecting certified types}
793 ctyp_of : Sign.sg -> typ -> ctyp
794 rep_ctyp : ctyp -> \{T: typ, sign: Sign.sg\}
796 \begin{ttdescription}
797 \item[\ttindexbold{ctyp_of} $sign$ $T$] \index{signatures}
798 certifies $T$ with respect to signature~$sign$.
800 \item[\ttindexbold{rep_ctyp} $cT$]
801 decomposes $cT$ as a record containing the type itself and its signature.