4 \chapter{Theories, Terms and Types} \label{theories}
5 \index{theories|(}\index{signatures|bold}
6 \index{reading!axioms|see{{\tt assume_ax}}} Theories organize the
7 syntax, declarations and axioms of a mathematical development. They
8 are built, starting from the {\Pure} or {\CPure} theory, by extending
9 and merging existing theories. They have the \ML\ type
10 \mltydx{theory}. Theory operations signal errors by raising exception
11 \xdx{THEORY}, returning a message and a list of theories.
13 Signatures, which contain information about sorts, types, constants and
14 syntax, have the \ML\ type~\mltydx{Sign.sg}. For identification, each
15 signature carries a unique list of \bfindex{stamps}, which are \ML\
16 references to strings. The strings serve as human-readable names; the
17 references serve as unique identifiers. Each primitive signature has a
18 single stamp. When two signatures are merged, their lists of stamps are
19 also merged. Every theory carries a unique signature.
21 Terms and types are the underlying representation of logical syntax. Their
22 \ML\ definitions are irrelevant to naive Isabelle users. Programmers who
23 wish to extend Isabelle may need to know such details, say to code a tactic
24 that looks for subgoals of a particular form. Terms and types may be
25 `certified' to be well-formed with respect to a given signature.
28 \section{Defining theories}\label{sec:ref-defining-theories}
30 Theories are usually defined using theory definition files (which have a name
31 suffix {\tt .thy}). There is also a low level interface provided by certain
32 \ML{} functions (see \S\ref{BuildingATheory}).
33 Appendix~\ref{app:TheorySyntax} presents the concrete syntax for theory
34 definitions; here is an explanation of the constituent parts:
36 \item[{\it theoryDef}] is the full definition. The new theory is
37 called $id$. It is the union of the named {\bf parent
38 theories}\indexbold{theories!parent}, possibly extended with new
39 components. \thydx{Pure} and \thydx{CPure} are the basic theories,
40 which contain only the meta-logic. They differ just in their
41 concrete syntax for function applications.
43 Normally each {\it name\/} is an identifier, the name of the parent theory.
44 Quoted strings can be used to document additional file dependencies; see
45 \S\ref{LoadingTheories} for details.
48 is a series of class declarations. Declaring {\tt$id$ < $id@1$ \dots\
49 $id@n$} makes $id$ a subclass of the existing classes $id@1\dots
50 id@n$. This rules out cyclic class structures. Isabelle automatically
51 computes the transitive closure of subclass hierarchies; it is not
52 necessary to declare {\tt c < e} in addition to {\tt c < d} and {\tt d <
56 introduces $sort$ as the new default sort for type variables. This applies
57 to unconstrained type variables in an input string but not to type
58 variables created internally. If omitted, the default sort is the listwise
59 union of the default sorts of the parent theories (i.e.\ their logical
62 \item[$sort$] is a finite set of classes. A single class $id$
63 abbreviates the sort $\ttlbrace id\ttrbrace$.
66 is a series of type declarations. Each declares a new type constructor
67 or type synonym. An $n$-place type constructor is specified by
68 $(\alpha@1,\dots,\alpha@n)name$, where the type variables serve only to
69 indicate the number~$n$.
71 A {\bf type synonym}\indexbold{type synonyms} is an abbreviation
72 $(\alpha@1,\dots,\alpha@n)name = \tau$, where $name$ and $\tau$ can
76 declares a type or constant to be an infix operator of priority $nat$
77 associating to the left ({\tt infixl}) or right ({\tt infixr}). Only
78 2-place type constructors can have infix status; an example is {\tt
79 ('a,'b)~"*"~(infixr~20)}, which may express binary product types.
81 \item[$arities$] is a series of type arity declarations. Each assigns
82 arities to type constructors. The $name$ must be an existing type
83 constructor, which is given the additional arity $arity$.
85 \item[$consts$] is a series of constant declarations. Each new
86 constant $name$ is given the specified type. The optional $mixfix$
87 annotations may attach concrete syntax to the constant.
89 \item[$syntax$] \index{*syntax section}\index{print mode} is a variant
90 of $consts$ which adds just syntax without actually declaring
91 logical constants. This gives full control over a theory's context
92 free grammar. The optional $mode$ specifies the print mode where the
93 mixfix productions should be added. If there is no \texttt{output}
94 option given, all productions are also added to the input syntax
95 (regardless of the print mode).
97 \item[$mixfix$] \index{mixfix declarations}
98 annotations can take three forms:
100 \item A mixfix template given as a $string$ of the form
101 {\tt"}\dots{\tt\_}\dots{\tt\_}\dots{\tt"} where the $i$-th underscore
102 indicates the position where the $i$-th argument should go. The list
103 of numbers gives the priority of each argument. The final number gives
104 the priority of the whole construct.
106 \item A constant $f$ of type $\tau@1\To(\tau@2\To\tau)$ can be given {\bf
109 \item A constant $f$ of type $(\tau@1\To\tau@2)\To\tau$ can be given {\bf
110 binder} status. The declaration {\tt binder} $\cal Q$ $p$ causes
111 ${\cal Q}\,x.F(x)$ to be treated
112 like $f(F)$, where $p$ is the priority.
116 specifies syntactic translation rules (macros). There are three forms:
117 parse rules ({\tt =>}), print rules ({\tt <=}), and parse/print rules ({\tt
121 is a series of rule declarations. Each has a name $id$ and the formula is
122 given by the $string$. Rule names must be distinct within any single
125 \item[$defs$] is a series of definitions. They are just like $rules$, except
126 that every $string$ must be a definition (see below for details).
128 \item[$constdefs$] combines the declaration of constants and their
129 definition. The first $string$ is the type, the second the definition.
131 \item[$axclass$] \index{*axclass section} defines an
132 \rmindex{axiomatic type class} as the intersection of existing
133 classes, with additional axioms holding. Class axioms may not
134 contain more than one type variable. The class axioms (with implicit
135 sort constraints added) are bound to the given names. Furthermore a
136 class introduction rule is generated, which is automatically
137 employed by $instance$ to prove instantiations of this class.
139 \item[$instance$] \index{*instance section} proves class inclusions or
140 type arities at the logical level and then transfers these to the
141 type signature. The instantiation is proven and checked properly.
142 The user has to supply sufficient witness information: theorems
143 ($longident$), axioms ($string$), or even arbitrary \ML{} tactic
146 \item[$oracle$] links the theory to a trusted external reasoner. It is
147 allowed to create theorems, but each theorem carries a proof object
148 describing the oracle invocation. See \S\ref{sec:oracles} for details.
150 \item[$ml$] \index{*ML section}
151 consists of \ML\ code, typically for parse and print translation functions.
154 Chapters~\ref{Defining-Logics} and \ref{chap:syntax} explain mixfix
155 declarations, translation rules and the {\tt ML} section in more detail.
158 \subsection{Definitions}\indexbold{definitions}
160 {\bf Definitions} are intended to express abbreviations. The simplest
161 form of a definition is $f \equiv t$, where $f$ is a constant.
162 Isabelle also allows a derived forms where the arguments of~$f$ appear
163 on the left, abbreviating a string of $\lambda$-abstractions.
165 Isabelle makes the following checks on definitions:
167 \item Arguments (on the left-hand side) must be distinct variables.
168 \item All variables on the right-hand side must also appear on the left-hand
170 \item All type variables on the right-hand side must also appear on
171 the left-hand side; this prohibits definitions such as {\tt
172 (zero::nat) == length ([]::'a list)}.
173 \item The definition must not be recursive. Most object-logics provide
174 definitional principles that can be used to express recursion safely.
176 These checks are intended to catch the sort of errors that might be made
177 accidentally. Misspellings, for instance, might result in additional
178 variables appearing on the right-hand side. More elaborate checks could be
179 made, but the cost might be overly strict rules on declaration order, etc.
182 \subsection{*Classes and arities}
183 \index{classes!context conditions}\index{arities!context conditions}
185 In order to guarantee principal types~\cite{nipkow-prehofer},
186 arity declarations must obey two conditions:
188 \item There must not be any two declarations $ty :: (\vec{r})c$ and
189 $ty :: (\vec{s})c$ with $\vec{r} \neq \vec{s}$. For example, this
190 excludes the following:
193 foo :: ({\ttlbrace}logic{\ttrbrace}) logic
194 foo :: ({\ttlbrace}{\ttrbrace})logic
197 \item If there are two declarations $ty :: (s@1,\dots,s@n)c$ and $ty ::
198 (s@1',\dots,s@n')c'$ such that $c' < c$ then $s@i' \preceq s@i$ must hold
199 for $i=1,\dots,n$. The relationship $\preceq$, defined as
200 \[ s' \preceq s \iff \forall c\in s. \exists c'\in s'.~ c'\le c, \]
201 expresses that the set of types represented by $s'$ is a subset of the
202 set of types represented by $s$. Assuming $term \preceq logic$, the
203 following is forbidden:
206 foo :: ({\ttlbrace}logic{\ttrbrace})logic
207 foo :: ({\ttlbrace}{\ttrbrace})term
213 \section{Loading a new theory}\label{LoadingTheories}
214 \index{theories!loading}\index{files!reading}
216 use_thy : string -> unit
217 time_use_thy : string -> unit
218 loadpath : string list ref \hfill{\bf initially {\tt["."]}}
219 delete_tmpfiles : bool ref \hfill{\bf initially true}
222 \begin{ttdescription}
223 \item[\ttindexbold{use_thy} $thyname$]
224 reads the theory $thyname$ and creates an \ML{} structure as described below.
226 \item[\ttindexbold{time_use_thy} $thyname$]
227 calls {\tt use_thy} $thyname$ and reports the time taken.
229 \item[\ttindexbold{loadpath}]
230 contains a list of directories to search when locating the files that
231 define a theory. This list is only used if the theory name in {\tt
232 use_thy} does not specify the path explicitly.
234 \item[reset \ttindexbold{delete_tmpfiles};]
235 suppresses the deletion of temporary files.
238 Each theory definition must reside in a separate file. Let the file
239 {\it T}{\tt.thy} contain the definition of a theory called~$T$, whose
240 parent theories are $TB@1$ \dots $TB@n$. Calling
241 \ttindex{use_thy}~{\tt"{\it T\/}"} reads the file {\it T}{\tt.thy},
242 writes a temporary \ML{} file {\tt.{\it T}.thy.ML}, and reads the
243 latter file. Recursive {\tt use_thy} calls load those parent theories
244 that have not been loaded previously; the recursive calls may continue
245 to any depth. One {\tt use_thy} call can read an entire logic
246 provided all theories are linked appropriately.
248 The result is an \ML\ structure~$T$ containing at least a component
249 {\tt thy} for the new theory and components for each of the rules.
250 The structure also contains the definitions of the {\tt ML} section,
251 if present. The file {\tt.{\it T}.thy.ML} is then deleted if {\tt
252 delete_tmpfiles} is set and no errors occurred.
254 Finally the file {\it T}{\tt.ML} is read, if it exists. The structure
255 $T$ is automatically open in this context. Proof scripts typically
256 refer to its components by unqualified names.
258 Some applications construct theories directly by calling \ML\ functions. In
259 this situation there is no {\tt.thy} file, only an {\tt.ML} file. The
260 {\tt.ML} file must declare an \ML\ structure having the theory's name and a
261 component {\tt thy} containing the new theory object.
262 Section~\ref{sec:pseudo-theories} below describes a way of linking such
263 theories to their parents.
266 Temporary files are written to the current directory, so this must be
267 writable. Isabelle inherits the current directory from the operating
268 system; you can change it within Isabelle by typing {\tt
269 cd"$dir$"}\index{*cd}.
273 \section{Reloading modified theories}\label{sec:reloading-theories}
274 \indexbold{theories!reloading}
276 update : unit -> unit
277 unlink_thy : string -> unit
279 Changing a theory on disk often makes it necessary to reload all theories
280 descended from it. However, {\tt use_thy} reads only one theory, even if
281 some of the parent theories are out of date. In this case you should call
284 Isabelle keeps track of all loaded theories and their files. If
285 \ttindex{use_thy} finds that the theory to be loaded has been read before,
286 it determines whether to reload the theory as follows. First it looks for
287 the theory's files in their previous location. If it finds them, it
288 compares their modification times to the internal data and stops if they
289 are equal. If the files have been moved, {\tt use_thy} searches for them
290 as it would for a new theory. After {\tt use_thy} reloads a theory, it
291 marks the children as out-of-date.
293 \begin{ttdescription}
294 \item[\ttindexbold{update}()]
295 reloads all modified theories and their descendants in the correct order.
297 \item[\ttindexbold{unlink_thy} $thyname$]\indexbold{theories!removing}
298 informs Isabelle that theory $thyname$ no longer exists. If you delete the
299 theory files for $thyname$ then you must execute {\tt unlink_thy};
300 otherwise {\tt update} will complain about a missing file.
304 \subsection{*Pseudo theories}\label{sec:pseudo-theories}
305 \indexbold{theories!pseudo}%
306 Any automatic reloading facility requires complete knowledge of all
307 dependencies. Sometimes theories depend on objects created in \ML{} files
308 with no associated theory definition file. These objects may be theories but
309 they could also be theorems, proof procedures, etc.
311 Unless such dependencies are documented, {\tt update} fails to reload these
312 \ML{} files and the system is left in a state where some objects, such as
313 theorems, still refer to old versions of theories. This may lead to the
316 Attempt to merge different versions of theories: \dots
318 Therefore there is a way to link theories and {\bf orphaned} \ML{} files ---
319 those not associated with a theory definition.
321 Let us assume we have an orphaned \ML{} file named {\tt orphan.ML} and a
322 theory~$B$ that depends on {\tt orphan.ML} --- for example, {\tt B.ML} uses
323 theorems proved in {\tt orphan.ML}. Then {\tt B.thy} should
324 mention this dependency as follows:
326 B = \(\ldots\) + "orphan" + \(\ldots\)
328 Quoted strings stand for theories which have to be loaded before the
329 current theory is read but which are not used in building the base of
330 theory~$B$. Whenever {\tt orphan} changes and is reloaded, Isabelle
331 knows that $B$ has to be updated, too.
333 Note that it's necessary for {\tt orphan} to declare a special ML
334 object of type {\tt theory} which is present in all theories. This is
335 normally achieved by adding the file {\tt orphan.thy} to make {\tt
336 orphan} a {\bf pseudo theory}. A minimum version of {\tt orphan.thy}
343 which uses {\tt Pure} to make a dummy theory. Normally though the
344 orphaned file has its own dependencies. If {\tt orphan.ML} depends on
345 theories or files $A@1$, \ldots, $A@n$, record this by creating the
346 pseudo theory in the following way:
348 orphan = \(A@1\) + \(\ldots\) + \(A@n\)
350 The resulting theory ensures that {\tt update} reloads {\tt orphan}
351 whenever it reloads one of the $A@i$.
353 For an extensive example of how this technique can be used to link
354 lots of theory files and load them by just a few {\tt use_thy} calls
355 see the sources of one of the major object-logics (e.g.\ \ZF).
359 \section{Basic operations on theories}\label{BasicOperationsOnTheories}
360 \subsection{Retrieving axioms and theorems}
361 \index{theories!axioms of}\index{axioms!extracting}
362 \index{theories!theorems of}\index{theorems!extracting}
364 get_axiom : theory -> xstring -> thm
365 get_thm : theory -> xstring -> thm
366 get_thms : theory -> xstring -> thm list
367 axioms_of : theory -> (string * thm) list
368 thms_of : theory -> (string * thm) list
369 assume_ax : theory -> string -> thm
371 \begin{ttdescription}
372 \item[\ttindexbold{get_axiom} $thy$ $name$] returns an axiom with the
373 given $name$ from $thy$ or any of its ancestors, raising exception
374 \xdx{THEORY} if none exists. Merging theories can cause several
375 axioms to have the same name; {\tt get_axiom} returns an arbitrary
376 one. Usually, axioms are also stored as theorems and may be
377 retrieved via \texttt{get_thm} as well.
379 \item[\ttindexbold{get_thm} $thy$ $name$] is analogous to {\tt
380 get_axiom}, but looks for a theorem stored in the theory's
381 database. Like {\tt get_axiom} it searches all parents of a theory
382 if the theorem is not found directly in $thy$.
384 \item[\ttindexbold{get_thms} $thy$ $name$] is like \texttt{get_thm}
385 for retrieving theorem lists stored within the theory. It returns a
386 singleton list if $name$ actually refers to a theorem rather than a
389 \item[\ttindexbold{axioms_of} $thy$] returns the axioms of this theory
390 node, not including the ones of its ancestors.
392 \item[\ttindexbold{thms_of} $thy$] returns all theorems stored within
393 the database of this theory node, not including the ones of its
396 \item[\ttindexbold{assume_ax} $thy$ $formula$] reads the {\it formula}
397 using the syntax of $thy$, following the same conventions as axioms
398 in a theory definition. You can thus pretend that {\it formula} is
399 an axiom and use the resulting theorem like an axiom. Actually {\tt
400 assume_ax} returns an assumption; \ttindex{qed} and
401 \ttindex{result} complain about additional assumptions, but
402 \ttindex{uresult} does not.
404 For example, if {\it formula} is
405 \hbox{\tt a=b ==> b=a} then the resulting theorem has the form
406 \hbox{\verb'?a=?b ==> ?b=?a [!!a b. a=b ==> b=a]'}
409 \subsection{*Building a theory}
410 \label{BuildingATheory}
411 \index{theories!constructing|bold}
413 ProtoPure.thy : theory
416 merge_theories : string -> theory * theory -> theory
419 \item[\ttindexbold{ProtoPure.thy}, \ttindexbold{Pure.thy},
420 \ttindexbold{CPure.thy}] contain the syntax and signature of the
421 meta-logic. There are basically no axioms: meta-level inferences
422 are carried out by \ML\ functions. \texttt{Pure} and \texttt{CPure}
423 just differ in their concrete syntax of prefix function application:
424 $t(u@1, \ldots, u@n)$ in \texttt{Pure} vs.\ $t\,u@1,\ldots\,u@n$ in
425 \texttt{CPure}. \texttt{ProtoPure} is their common parent,
426 containing no syntax for printing prefix applications at all!
428 \item[\ttindexbold{merge_theories} $name$ ($thy@1$, $thy@2$)] merges
429 the two theories $thy@1$ and $thy@2$, creating a new named theory
430 node. The resulting theory contains all of the syntax, signature
431 and axioms of the constituent theories. Merging theories that
432 contain different identification stamps of the same name fails with
433 the following message
435 Attempt to merge different versions of theories: "\(T@1\)", \(\ldots\), "\(T@n\)"
437 This error may especially occur when a theory is redeclared --- say to
438 change an inappropriate definition --- and bindings to old versions
439 persist. Isabelle ensures that old and new theories of the same name
440 are not involved in a proof.
443 %\item [\ttindexbold{extend_theory} $thy$ {\tt"}$T${\tt"} $\cdots$] extends
444 % the theory $thy$ with new types, constants, etc. $T$ identifies the theory
445 % internally. When a theory is redeclared, say to change an incorrect axiom,
446 % bindings to the old axiom may persist. Isabelle ensures that the old and
447 % new theories are not involved in the same proof. Attempting to combine
448 % different theories having the same name $T$ yields the fatal error
449 %extend_theory : theory -> string -> \(\cdots\) -> theory
451 %Attempt to merge different versions of theory: \(T\)
456 %\item [\ttindexbold{extend_theory} $thy$ {\tt"}$T${\tt"}
457 % ($classes$, $default$, $types$, $arities$, $consts$, $sextopt$) $rules$]
458 %\hfill\break %%% include if line is just too short
459 %is the \ML{} equivalent of the following theory definition:
462 %classes \(c\) < \(c@1\),\(\dots\),\(c@m\)
464 %default {\(d@1,\dots,d@r\)}
465 %types \(tycon@1\),\dots,\(tycon@i\) \(n\)
467 %arities \(tycon@1'\),\dots,\(tycon@j'\) :: (\(s@1\),\dots,\(s@n\))\(c\)
469 %consts \(b@1\),\dots,\(b@k\) :: \(\tau\)
471 %rules \(name\) \(rule\)
476 %\begin{tabular}[t]{l@{~=~}l}
477 %$classes$ & \tt[("$c$",["$c@1$",\dots,"$c@m$"]),\dots] \\
478 %$default$ & \tt["$d@1$",\dots,"$d@r$"]\\
479 %$types$ & \tt[([$tycon@1$,\dots,$tycon@i$], $n$),\dots] \\
480 %$arities$ & \tt[([$tycon'@1$,\dots,$tycon'@j$], ([$s@1$,\dots,$s@n$],$c$)),\dots]
482 %$consts$ & \tt[([$b@1$,\dots,$b@k$],$\tau$),\dots] \\
483 %$rules$ & \tt[("$name$",$rule$),\dots]
487 \subsection{Inspecting a theory}\label{sec:inspct-thy}
488 \index{theories!inspecting|bold}
490 print_syntax : theory -> unit
491 print_theory : theory -> unit
492 print_data : theory -> string -> unit
493 parents_of : theory -> theory list
494 ancestors_of : theory -> theory list
495 sign_of : theory -> Sign.sg
496 Sign.stamp_names_of : Sign.sg -> string list
498 These provide means of viewing a theory's components.
499 \begin{ttdescription}
500 \item[\ttindexbold{print_syntax} $thy$] prints the syntax of $thy$
501 (grammar, macros, translation functions etc., see
502 page~\pageref{pg:print_syn} for more details).
504 \item[\ttindexbold{print_theory} $thy$] prints the logical parts of
505 $thy$, excluding the syntax.
507 \item[\ttindexbold{print_data} $thy$ $kind$] prints generic data of
508 $thy$. This invokes the print method associated with $kind$. Refer
509 to the output of \texttt{print_theory} for a list of available data
512 \item[\ttindexbold{parents_of} $thy$] returns the direct ancestors
515 \item[\ttindexbold{ancestors_of} $thy$] returns all ancestors of~$thy$
516 (not including $thy$ itself).
518 \item[\ttindexbold{sign_of} $thy$] returns the signature associated
519 with~$thy$. It is useful with functions like {\tt
520 read_instantiate_sg}, which take a signature as an argument.
522 \item[\ttindexbold{Sign.stamp_names_of} $sg$]\index{signatures}
523 returns the names of the identification \rmindex{stamps} of ax
524 signature. These coincide with the names of its full ancestry
525 including that of $sg$ itself.
532 Terms belong to the \ML\ type \mltydx{term}, which is a concrete datatype
533 with six constructors:
535 type indexname = string * int;
537 datatype term = Const of string * typ
538 | Free of string * typ
539 | Var of indexname * typ
541 | Abs of string * typ * term
542 | op $ of term * term;
544 \begin{ttdescription}
545 \item[\ttindexbold{Const} ($a$, $T$)] \index{constants|bold}
546 is the {\bf constant} with name~$a$ and type~$T$. Constants include
547 connectives like $\land$ and $\forall$ as well as constants like~0
548 and~$Suc$. Other constants may be required to define a logic's concrete
551 \item[\ttindexbold{Free} ($a$, $T$)] \index{variables!free|bold}
552 is the {\bf free variable} with name~$a$ and type~$T$.
554 \item[\ttindexbold{Var} ($v$, $T$)] \index{unknowns|bold}
555 is the {\bf scheme variable} with indexname~$v$ and type~$T$. An
556 \mltydx{indexname} is a string paired with a non-negative index, or
557 subscript; a term's scheme variables can be systematically renamed by
558 incrementing their subscripts. Scheme variables are essentially free
559 variables, but may be instantiated during unification.
561 \item[\ttindexbold{Bound} $i$] \index{variables!bound|bold}
562 is the {\bf bound variable} with de Bruijn index~$i$, which counts the
563 number of lambdas, starting from zero, between a variable's occurrence
564 and its binding. The representation prevents capture of variables. For
565 more information see de Bruijn \cite{debruijn72} or
566 Paulson~\cite[page~336]{paulson91}.
568 \item[\ttindexbold{Abs} ($a$, $T$, $u$)]
569 \index{lambda abs@$\lambda$-abstractions|bold}
570 is the $\lambda$-{\bf abstraction} with body~$u$, and whose bound
571 variable has name~$a$ and type~$T$. The name is used only for parsing
572 and printing; it has no logical significance.
574 \item[$t$ \$ $u$] \index{$@{\tt\$}|bold} \index{function applications|bold}
575 is the {\bf application} of~$t$ to~$u$.
577 Application is written as an infix operator to aid readability.
578 Here is an \ML\ pattern to recognize \FOL{} formulae of
579 the form~$A\imp B$, binding the subformulae to~$A$ and~$B$:
581 Const("Trueprop",_) $ (Const("op -->",_) $ A $ B)
585 \section{*Variable binding}
587 loose_bnos : term -> int list
588 incr_boundvars : int -> term -> term
589 abstract_over : term*term -> term
590 variant_abs : string * typ * term -> string * term
591 aconv : term * term -> bool\hfill{\bf infix}
593 These functions are all concerned with the de Bruijn representation of
595 \begin{ttdescription}
596 \item[\ttindexbold{loose_bnos} $t$]
597 returns the list of all dangling bound variable references. In
598 particular, {\tt Bound~0} is loose unless it is enclosed in an
599 abstraction. Similarly {\tt Bound~1} is loose unless it is enclosed in
600 at least two abstractions; if enclosed in just one, the list will contain
601 the number 0. A well-formed term does not contain any loose variables.
603 \item[\ttindexbold{incr_boundvars} $j$]
604 increases a term's dangling bound variables by the offset~$j$. This is
605 required when moving a subterm into a context where it is enclosed by a
606 different number of abstractions. Bound variables with a matching
607 abstraction are unaffected.
609 \item[\ttindexbold{abstract_over} $(v,t)$]
610 forms the abstraction of~$t$ over~$v$, which may be any well-formed term.
611 It replaces every occurrence of \(v\) by a {\tt Bound} variable with the
614 \item[\ttindexbold{variant_abs} $(a,T,u)$]
615 substitutes into $u$, which should be the body of an abstraction.
616 It replaces each occurrence of the outermost bound variable by a free
617 variable. The free variable has type~$T$ and its name is a variant
618 of~$a$ chosen to be distinct from all constants and from all variables
621 \item[$t$ \ttindexbold{aconv} $u$]
622 tests whether terms~$t$ and~$u$ are \(\alpha\)-convertible: identical up
623 to renaming of bound variables.
626 Two constants, {\tt Free}s, or {\tt Var}s are \(\alpha\)-convertible
627 if their names and types are equal.
628 (Variables having the same name but different types are thus distinct.
629 This confusing situation should be avoided!)
631 Two bound variables are \(\alpha\)-convertible
632 if they have the same number.
634 Two abstractions are \(\alpha\)-convertible
635 if their bodies are, and their bound variables have the same type.
637 Two applications are \(\alpha\)-convertible
638 if the corresponding subterms are.
643 \section{Certified terms}\index{terms!certified|bold}\index{signatures}
644 A term $t$ can be {\bf certified} under a signature to ensure that every type
645 in~$t$ is well-formed and every constant in~$t$ is a type instance of a
646 constant declared in the signature. The term must be well-typed and its use
647 of bound variables must be well-formed. Meta-rules such as {\tt forall_elim}
648 take certified terms as arguments.
650 Certified terms belong to the abstract type \mltydx{cterm}.
651 Elements of the type can only be created through the certification process.
652 In case of error, Isabelle raises exception~\ttindex{TERM}\@.
654 \subsection{Printing terms}
655 \index{terms!printing of}
657 string_of_cterm : cterm -> string
658 Sign.string_of_term : Sign.sg -> term -> string
660 \begin{ttdescription}
661 \item[\ttindexbold{string_of_cterm} $ct$]
662 displays $ct$ as a string.
664 \item[\ttindexbold{Sign.string_of_term} $sign$ $t$]
665 displays $t$ as a string, using the syntax of~$sign$.
668 \subsection{Making and inspecting certified terms}
670 cterm_of : Sign.sg -> term -> cterm
671 read_cterm : Sign.sg -> string * typ -> cterm
672 cert_axm : Sign.sg -> string * term -> string * term
673 read_axm : Sign.sg -> string * string -> string * term
674 rep_cterm : cterm -> {\ttlbrace}T:typ, t:term, sign:Sign.sg, maxidx:int\ttrbrace
676 \begin{ttdescription}
677 \item[\ttindexbold{cterm_of} $sign$ $t$] \index{signatures}
678 certifies $t$ with respect to signature~$sign$.
680 \item[\ttindexbold{read_cterm} $sign$ ($s$, $T$)]
681 reads the string~$s$ using the syntax of~$sign$, creating a certified term.
682 The term is checked to have type~$T$; this type also tells the parser what
683 kind of phrase to parse.
685 \item[\ttindexbold{cert_axm} $sign$ ($name$, $t$)]
686 certifies $t$ with respect to $sign$ as a meta-proposition and converts all
687 exceptions to an error, including the final message
689 The error(s) above occurred in axiom "\(name\)"
692 \item[\ttindexbold{read_axm} $sign$ ($name$, $s$)]
693 similar to {\tt cert_axm}, but first reads the string $s$ using the syntax of
696 \item[\ttindexbold{rep_cterm} $ct$]
697 decomposes $ct$ as a record containing its type, the term itself, its
698 signature, and the maximum subscript of its unknowns. The type and maximum
699 subscript are computed during certification.
703 \section{Types}\index{types|bold}
704 Types belong to the \ML\ type \mltydx{typ}, which is a concrete datatype with
705 three constructor functions. These correspond to type constructors, free
706 type variables and schematic type variables. Types are classified by sorts,
707 which are lists of classes (representing an intersection). A class is
708 represented by a string.
711 type sort = class list;
713 datatype typ = Type of string * typ list
714 | TFree of string * sort
715 | TVar of indexname * sort;
718 fun S --> T = Type ("fun", [S, T]);
720 \begin{ttdescription}
721 \item[\ttindexbold{Type} ($a$, $Ts$)] \index{type constructors|bold}
722 applies the {\bf type constructor} named~$a$ to the type operands~$Ts$.
723 Type constructors include~\tydx{fun}, the binary function space
724 constructor, as well as nullary type constructors such as~\tydx{prop}.
725 Other type constructors may be introduced. In expressions, but not in
726 patterns, \hbox{\tt$S$-->$T$} is a convenient shorthand for function
729 \item[\ttindexbold{TFree} ($a$, $s$)] \index{type variables|bold}
730 is the {\bf type variable} with name~$a$ and sort~$s$.
732 \item[\ttindexbold{TVar} ($v$, $s$)] \index{type unknowns|bold}
733 is the {\bf type unknown} with indexname~$v$ and sort~$s$.
734 Type unknowns are essentially free type variables, but may be
735 instantiated during unification.
739 \section{Certified types}
740 \index{types!certified|bold}
741 Certified types, which are analogous to certified terms, have type
744 \subsection{Printing types}
745 \index{types!printing of}
747 string_of_ctyp : ctyp -> string
748 Sign.string_of_typ : Sign.sg -> typ -> string
750 \begin{ttdescription}
751 \item[\ttindexbold{string_of_ctyp} $cT$]
752 displays $cT$ as a string.
754 \item[\ttindexbold{Sign.string_of_typ} $sign$ $T$]
755 displays $T$ as a string, using the syntax of~$sign$.
759 \subsection{Making and inspecting certified types}
761 ctyp_of : Sign.sg -> typ -> ctyp
762 rep_ctyp : ctyp -> {\ttlbrace}T: typ, sign: Sign.sg\ttrbrace
764 \begin{ttdescription}
765 \item[\ttindexbold{ctyp_of} $sign$ $T$] \index{signatures}
766 certifies $T$ with respect to signature~$sign$.
768 \item[\ttindexbold{rep_ctyp} $cT$]
769 decomposes $cT$ as a record containing the type itself and its signature.
773 \section{Oracles: calling trusted external reasoners}
777 Oracles allow Isabelle to take advantage of external reasoners such as
778 arithmetic decision procedures, model checkers, fast tautology checkers or
779 computer algebra systems. Invoked as an oracle, an external reasoner can
780 create arbitrary Isabelle theorems. It is your responsibility to ensure that
781 the external reasoner is as trustworthy as your application requires.
782 Isabelle's proof objects~(\S\ref{sec:proofObjects}) record how each theorem
783 depends upon oracle calls.
786 invoke_oracle : theory -> xstring -> Sign.sg * object -> thm
787 Theory.add_oracle : bstring * (Sign.sg * object -> term) -> theory -> theory
789 \begin{ttdescription}
790 \item[\ttindexbold{invoke_oracle} $thy$ $name$ ($sign$, $data$)]
791 invokes the oracle $name$ of theory $thy$ passing the information
792 contained in the exception value $data$ and creating a theorem
793 having signature $sign$. Note that type \ttindex{object} is just an
794 abbreviation for \texttt{exn}. Errors arise if $thy$ does not have
795 an oracle called $name$, if the oracle rejects its arguments or if
796 its result is ill-typed.
798 \item[\ttindexbold{Theory.add_oracle} $name$ $fun$ $thy$] extends
799 $thy$ by oracle $fun$ called $name$. It is seldom called
800 explicitly, as there is concrete syntax for oracles in theory files.
803 A curious feature of {\ML} exceptions is that they are ordinary constructors.
804 The {\ML} type {\tt exn} is a datatype that can be extended at any time. (See
805 my {\em {ML} for the Working Programmer}~\cite{paulson-ml2}, especially
806 page~136.) The oracle mechanism takes advantage of this to allow an oracle to
807 take any information whatever.
809 There must be some way of invoking the external reasoner from \ML, either
810 because it is coded in {\ML} or via an operating system interface. Isabelle
811 expects the {\ML} function to take two arguments: a signature and an
814 \item The signature will typically be that of a desendant of the theory
815 declaring the oracle. The oracle will use it to distinguish constants from
816 variables, etc., and it will be attached to the generated theorems.
818 \item The exception is used to pass arbitrary information to the oracle. This
819 information must contain a full description of the problem to be solved by
820 the external reasoner, including any additional information that might be
821 required. The oracle may raise the exception to indicate that it cannot
822 solve the specified problem.
825 A trivial example is provided in theory {\tt FOL/ex/IffOracle}. This
826 oracle generates tautologies of the form $P\bimp\cdots\bimp P$, with
827 an even number of $P$s.
829 The \texttt{ML} section of \texttt{IffOracle.thy} begins by declaring
830 a few auxiliary functions (suppressed below) for creating the
831 tautologies. Then it declares a new exception constructor for the
832 information required by the oracle: here, just an integer. It finally
833 defines the oracle function itself.
835 exception IffOracleExn of int;\medskip
836 fun mk_iff_oracle (sign, IffOracleExn n) =
837 if n > 0 andalso n mod 2 = 0
838 then Trueprop $ mk_iff n
839 else raise IffOracleExn n;
841 Observe the function's two arguments, the signature {\tt sign} and the
842 exception given as a pattern. The function checks its argument for
843 validity. If $n$ is positive and even then it creates a tautology
844 containing $n$ occurrences of~$P$. Otherwise it signals error by
845 raising its own exception (just by happy coincidence). Errors may be
846 signalled by other means, such as returning the theorem {\tt True}.
847 Please ensure that the oracle's result is correctly typed; Isabelle
848 will reject ill-typed theorems by raising a cryptic exception at top
851 The \texttt{oracle} section of {\tt IffOracle.thy} installs above
852 \texttt{ML} function as follows:
854 IffOracle = FOL +\medskip
856 iff = mk_iff_oracle\medskip
860 Now in \texttt{IffOracle.ML} we first define a wrapper for invoking
864 invoke_oracle IffOracle.thy "iff" (sign_of IffOracle.thy, IffOracleExn n);
867 Here are some example applications of the \texttt{iff} oracle. An
868 argument of 10 is allowed, but one of 5 is forbidden:
871 {\out "P <-> P <-> P <-> P <-> P <-> P <-> P <-> P <-> P <-> P" : thm}
873 {\out Exception- IffOracleExn 5 raised}