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[$local, global$] changes the current name declaration mode.
151 Initially, theories start in $local$ mode, causing all names of
152 types, constants, axioms etc.\ to be automatically qualified by the
153 theory name. Changing this to $global$ causes all names to be
154 declared as short base names only.
156 The $local$ and $global$ declarations act like switches, affecting
157 all following theory sections until changed again explicitly. Also
158 note that the final state at the end of the theory will persist. In
159 particular, this determines how the names of theorems stored later
162 \item[$ml$] \index{*ML section}
163 consists of \ML\ code, typically for parse and print translation functions.
166 Chapters~\ref{Defining-Logics} and \ref{chap:syntax} explain mixfix
167 declarations, translation rules and the {\tt ML} section in more detail.
170 \subsection{Definitions}\indexbold{definitions}
172 {\bf Definitions} are intended to express abbreviations. The simplest
173 form of a definition is $f \equiv t$, where $f$ is a constant.
174 Isabelle also allows a derived forms where the arguments of~$f$ appear
175 on the left, abbreviating a string of $\lambda$-abstractions.
177 Isabelle makes the following checks on definitions:
179 \item Arguments (on the left-hand side) must be distinct variables.
180 \item All variables on the right-hand side must also appear on the left-hand
182 \item All type variables on the right-hand side must also appear on
183 the left-hand side; this prohibits definitions such as {\tt
184 (zero::nat) == length ([]::'a list)}.
185 \item The definition must not be recursive. Most object-logics provide
186 definitional principles that can be used to express recursion safely.
188 These checks are intended to catch the sort of errors that might be made
189 accidentally. Misspellings, for instance, might result in additional
190 variables appearing on the right-hand side. More elaborate checks could be
191 made, but the cost might be overly strict rules on declaration order, etc.
194 \subsection{*Classes and arities}
195 \index{classes!context conditions}\index{arities!context conditions}
197 In order to guarantee principal types~\cite{nipkow-prehofer},
198 arity declarations must obey two conditions:
200 \item There must not be any two declarations $ty :: (\vec{r})c$ and
201 $ty :: (\vec{s})c$ with $\vec{r} \neq \vec{s}$. For example, this
202 excludes the following:
205 foo :: ({\ttlbrace}logic{\ttrbrace}) logic
206 foo :: ({\ttlbrace}{\ttrbrace})logic
209 \item If there are two declarations $ty :: (s@1,\dots,s@n)c$ and $ty ::
210 (s@1',\dots,s@n')c'$ such that $c' < c$ then $s@i' \preceq s@i$ must hold
211 for $i=1,\dots,n$. The relationship $\preceq$, defined as
212 \[ s' \preceq s \iff \forall c\in s. \exists c'\in s'.~ c'\le c, \]
213 expresses that the set of types represented by $s'$ is a subset of the
214 set of types represented by $s$. Assuming $term \preceq logic$, the
215 following is forbidden:
218 foo :: ({\ttlbrace}logic{\ttrbrace})logic
219 foo :: ({\ttlbrace}{\ttrbrace})term
225 \section{Loading a new theory}\label{LoadingTheories}
226 \index{theories!loading}\index{files!reading}
228 use_thy : string -> unit
229 time_use_thy : string -> unit
230 loadpath : string list ref \hfill{\bf initially {\tt["."]}}
231 delete_tmpfiles : bool ref \hfill{\bf initially true}
234 \begin{ttdescription}
235 \item[\ttindexbold{use_thy} $thyname$]
236 reads the theory $thyname$ and creates an \ML{} structure as described below.
238 \item[\ttindexbold{time_use_thy} $thyname$]
239 calls {\tt use_thy} $thyname$ and reports the time taken.
241 \item[\ttindexbold{loadpath}]
242 contains a list of directories to search when locating the files that
243 define a theory. This list is only used if the theory name in {\tt
244 use_thy} does not specify the path explicitly.
246 \item[reset \ttindexbold{delete_tmpfiles};]
247 suppresses the deletion of temporary files.
250 Each theory definition must reside in a separate file. Let the file
251 {\it T}{\tt.thy} contain the definition of a theory called~$T$, whose
252 parent theories are $TB@1$ \dots $TB@n$. Calling
253 \texttt{use_thy}~{\tt"{\it T\/}"} reads the file {\it T}{\tt.thy},
254 writes a temporary \ML{} file {\tt.{\it T}.thy.ML}, and reads the
255 latter file. Recursive {\tt use_thy} calls load those parent theories
256 that have not been loaded previously; the recursive calls may continue
257 to any depth. One {\tt use_thy} call can read an entire logic
258 provided all theories are linked appropriately.
260 The result is an \ML\ structure~$T$ containing at least a component
261 {\tt thy} for the new theory and components for each of the rules.
262 The structure also contains the definitions of the {\tt ML} section,
263 if present. The file {\tt.{\it T}.thy.ML} is then deleted if {\tt
264 delete_tmpfiles} is set and no errors occurred.
266 Finally the file {\it T}{\tt.ML} is read, if it exists. The structure
267 $T$ is automatically open in this context. Proof scripts typically
268 refer to its components by unqualified names.
270 Some applications construct theories directly by calling \ML\ functions. In
271 this situation there is no {\tt.thy} file, only an {\tt.ML} file. The
272 {\tt.ML} file must declare an \ML\ structure having the theory's name and a
273 component {\tt thy} containing the new theory object.
274 Section~\ref{sec:pseudo-theories} below describes a way of linking such
275 theories to their parents.
278 \section{Reloading modified theories}\label{sec:reloading-theories}
279 \indexbold{theories!reloading}
281 update : unit -> unit
282 unlink_thy : string -> unit
284 Changing a theory on disk often makes it necessary to reload all theories
285 descended from it. However, {\tt use_thy} reads only one theory, even if
286 some of the parent theories are out of date. In this case you should call
289 Isabelle keeps track of all loaded theories and their files. If
290 \texttt{use_thy} finds that the theory to be loaded has been read
291 before, it determines whether to reload the theory as follows. First
292 it looks for the theory's files in their previous location. If it
293 finds them, it compares their modification times to the internal data
294 and stops if they are equal. If the files have been moved, {\tt
295 use_thy} searches for them as it would for a new theory. After {\tt
296 use_thy} reloads a theory, it marks the children as out-of-date.
298 \begin{ttdescription}
299 \item[\ttindexbold{update}()]
300 reloads all modified theories and their descendants in the correct order.
302 \item[\ttindexbold{unlink_thy} $thyname$]\indexbold{theories!removing}
303 informs Isabelle that theory $thyname$ no longer exists. If you delete the
304 theory files for $thyname$ then you must execute {\tt unlink_thy};
305 otherwise {\tt update} will complain about a missing file.
309 \subsection{*Pseudo theories}\label{sec:pseudo-theories}
310 \indexbold{theories!pseudo}%
311 Any automatic reloading facility requires complete knowledge of all
312 dependencies. Sometimes theories depend on objects created in \ML{} files
313 with no associated theory definition file. These objects may be theories but
314 they could also be theorems, proof procedures, etc.
316 Unless such dependencies are documented, {\tt update} fails to reload these
317 \ML{} files and the system is left in a state where some objects, such as
318 theorems, still refer to old versions of theories. This may lead to the
321 Attempt to merge different versions of theories: \dots
323 Therefore there is a way to link theories and {\bf orphaned} \ML{} files ---
324 those not associated with a theory definition.
326 Let us assume we have an orphaned \ML{} file named {\tt orphan.ML} and a
327 theory~$B$ that depends on {\tt orphan.ML} --- for example, {\tt B.ML} uses
328 theorems proved in {\tt orphan.ML}. Then {\tt B.thy} should
329 mention this dependency as follows:
331 B = \(\ldots\) + "orphan" + \(\ldots\)
333 Quoted strings stand for theories which have to be loaded before the
334 current theory is read but which are not used in building the base of
335 theory~$B$. Whenever {\tt orphan} changes and is reloaded, Isabelle
336 knows that $B$ has to be updated, too.
338 Note that it's necessary for {\tt orphan} to declare a special ML
339 object of type {\tt theory} which is present in all theories. This is
340 normally achieved by adding the file {\tt orphan.thy} to make {\tt
341 orphan} a {\bf pseudo theory}. A minimum version of {\tt orphan.thy}
348 which uses {\tt Pure} to make a dummy theory. Normally though the
349 orphaned file has its own dependencies. If {\tt orphan.ML} depends on
350 theories or files $A@1$, \ldots, $A@n$, record this by creating the
351 pseudo theory in the following way:
353 orphan = \(A@1\) + \(\ldots\) + \(A@n\)
355 The resulting theory ensures that {\tt update} reloads {\tt orphan}
356 whenever it reloads one of the $A@i$.
358 For an extensive example of how this technique can be used to link
359 lots of theory files and load them by just a few {\tt use_thy} calls
360 see the sources of one of the major object-logics (e.g.\ \ZF).
364 \section{Basic operations on theories}\label{BasicOperationsOnTheories}
365 \subsection{Retrieving axioms and theorems}
366 \index{theories!axioms of}\index{axioms!extracting}
367 \index{theories!theorems of}\index{theorems!extracting}
369 get_axiom : theory -> xstring -> thm
370 get_thm : theory -> xstring -> thm
371 get_thms : theory -> xstring -> thm list
372 axioms_of : theory -> (string * thm) list
373 thms_of : theory -> (string * thm) list
374 assume_ax : theory -> string -> thm
376 \begin{ttdescription}
377 \item[\ttindexbold{get_axiom} $thy$ $name$] returns an axiom with the
378 given $name$ from $thy$ or any of its ancestors, raising exception
379 \xdx{THEORY} if none exists. Merging theories can cause several
380 axioms to have the same name; {\tt get_axiom} returns an arbitrary
381 one. Usually, axioms are also stored as theorems and may be
382 retrieved via \texttt{get_thm} as well.
384 \item[\ttindexbold{get_thm} $thy$ $name$] is analogous to {\tt
385 get_axiom}, but looks for a theorem stored in the theory's
386 database. Like {\tt get_axiom} it searches all parents of a theory
387 if the theorem is not found directly in $thy$.
389 \item[\ttindexbold{get_thms} $thy$ $name$] is like \texttt{get_thm}
390 for retrieving theorem lists stored within the theory. It returns a
391 singleton list if $name$ actually refers to a theorem rather than a
394 \item[\ttindexbold{axioms_of} $thy$] returns the axioms of this theory
395 node, not including the ones of its ancestors.
397 \item[\ttindexbold{thms_of} $thy$] returns all theorems stored within
398 the database of this theory node, not including the ones of its
401 \item[\ttindexbold{assume_ax} $thy$ $formula$] reads the {\it formula}
402 using the syntax of $thy$, following the same conventions as axioms
403 in a theory definition. You can thus pretend that {\it formula} is
404 an axiom and use the resulting theorem like an axiom. Actually {\tt
405 assume_ax} returns an assumption; \ttindex{qed} and
406 \ttindex{result} complain about additional assumptions, but
407 \ttindex{uresult} does not.
409 For example, if {\it formula} is
410 \hbox{\tt a=b ==> b=a} then the resulting theorem has the form
411 \hbox{\verb'?a=?b ==> ?b=?a [!!a b. a=b ==> b=a]'}
415 \subsection{*Theory inclusion}
417 subthy : theory * theory -> bool
418 eq_thy : theory * theory -> bool
419 transfer : theory -> thm -> thm
420 transfer_sg : Sign.sg -> thm -> thm
423 Inclusion and equality of theories is determined by unique
424 identification stamps that are created when declaring new components.
425 Theorems contain a reference to the theory (actually to its signature)
426 they have been derived in. Transferring theorems to super theories
427 has no logical significance, but may affect some operations in subtle
428 ways (e.g.\ implicit merges of signatures when applying rules, or
429 pretty printing of theorems).
431 \begin{ttdescription}
433 \item[\ttindexbold{subthy} ($thy@1$, $thy@2$)] determines if $thy@1$
434 is included in $thy@2$ wrt.\ identification stamps.
436 \item[\ttindexbold{eq_thy} ($thy@1$, $thy@2$)] determines if $thy@1$
437 is exactly the same as $thy@2$.
439 \item[\ttindexbold{transfer} $thy$ $thm$] transfers theorem $thm$ to
440 theory $thy$, provided the latter includes the theory of $thm$.
442 \item[\ttindexbold{transfer_sg} $sign$ $thm$] is similar to
443 \texttt{transfer}, but identifies the super theory via its
449 \subsection{*Building a theory}
450 \label{BuildingATheory}
451 \index{theories!constructing|bold}
453 ProtoPure.thy : theory
456 merge_theories : string -> theory * theory -> theory
459 \item[\ttindexbold{ProtoPure.thy}, \ttindexbold{Pure.thy},
460 \ttindexbold{CPure.thy}] contain the syntax and signature of the
461 meta-logic. There are basically no axioms: meta-level inferences
462 are carried out by \ML\ functions. \texttt{Pure} and \texttt{CPure}
463 just differ in their concrete syntax of prefix function application:
464 $t(u@1, \ldots, u@n)$ in \texttt{Pure} vs.\ $t\,u@1,\ldots\,u@n$ in
465 \texttt{CPure}. \texttt{ProtoPure} is their common parent,
466 containing no syntax for printing prefix applications at all!
468 \item[\ttindexbold{merge_theories} $name$ ($thy@1$, $thy@2$)] merges
469 the two theories $thy@1$ and $thy@2$, creating a new named theory
470 node. The resulting theory contains all of the syntax, signature
471 and axioms of the constituent theories. Merging theories that
472 contain different identification stamps of the same name fails with
473 the following message
475 Attempt to merge different versions of theories: "\(T@1\)", \(\ldots\), "\(T@n\)"
477 This error may especially occur when a theory is redeclared --- say to
478 change an inappropriate definition --- and bindings to old versions
479 persist. Isabelle ensures that old and new theories of the same name
480 are not involved in a proof.
483 %\item [\ttindexbold{extend_theory} $thy$ {\tt"}$T${\tt"} $\cdots$] extends
484 % the theory $thy$ with new types, constants, etc. $T$ identifies the theory
485 % internally. When a theory is redeclared, say to change an incorrect axiom,
486 % bindings to the old axiom may persist. Isabelle ensures that the old and
487 % new theories are not involved in the same proof. Attempting to combine
488 % different theories having the same name $T$ yields the fatal error
489 %extend_theory : theory -> string -> \(\cdots\) -> theory
491 %Attempt to merge different versions of theory: \(T\)
496 %\item [\ttindexbold{extend_theory} $thy$ {\tt"}$T${\tt"}
497 % ($classes$, $default$, $types$, $arities$, $consts$, $sextopt$) $rules$]
498 %\hfill\break %%% include if line is just too short
499 %is the \ML{} equivalent of the following theory definition:
502 %classes \(c\) < \(c@1\),\(\dots\),\(c@m\)
504 %default {\(d@1,\dots,d@r\)}
505 %types \(tycon@1\),\dots,\(tycon@i\) \(n\)
507 %arities \(tycon@1'\),\dots,\(tycon@j'\) :: (\(s@1\),\dots,\(s@n\))\(c\)
509 %consts \(b@1\),\dots,\(b@k\) :: \(\tau\)
511 %rules \(name\) \(rule\)
516 %\begin{tabular}[t]{l@{~=~}l}
517 %$classes$ & \tt[("$c$",["$c@1$",\dots,"$c@m$"]),\dots] \\
518 %$default$ & \tt["$d@1$",\dots,"$d@r$"]\\
519 %$types$ & \tt[([$tycon@1$,\dots,$tycon@i$], $n$),\dots] \\
520 %$arities$ & \tt[([$tycon'@1$,\dots,$tycon'@j$], ([$s@1$,\dots,$s@n$],$c$)),\dots]
522 %$consts$ & \tt[([$b@1$,\dots,$b@k$],$\tau$),\dots] \\
523 %$rules$ & \tt[("$name$",$rule$),\dots]
527 \subsection{Inspecting a theory}\label{sec:inspct-thy}
528 \index{theories!inspecting|bold}
530 print_syntax : theory -> unit
531 print_theory : theory -> unit
532 print_data : theory -> string -> unit
533 parents_of : theory -> theory list
534 ancestors_of : theory -> theory list
535 sign_of : theory -> Sign.sg
536 Sign.stamp_names_of : Sign.sg -> string list
538 These provide means of viewing a theory's components.
539 \begin{ttdescription}
540 \item[\ttindexbold{print_syntax} $thy$] prints the syntax of $thy$
541 (grammar, macros, translation functions etc., see
542 page~\pageref{pg:print_syn} for more details).
544 \item[\ttindexbold{print_theory} $thy$] prints the logical parts of
545 $thy$, excluding the syntax.
547 \item[\ttindexbold{print_data} $thy$ $kind$] prints generic data of
548 $thy$. This invokes the print method associated with $kind$. Refer
549 to the output of \texttt{print_theory} for a list of available data
552 \item[\ttindexbold{parents_of} $thy$] returns the direct ancestors
555 \item[\ttindexbold{ancestors_of} $thy$] returns all ancestors of~$thy$
556 (not including $thy$ itself).
558 \item[\ttindexbold{sign_of} $thy$] returns the signature associated
559 with~$thy$. It is useful with functions like {\tt
560 read_instantiate_sg}, which take a signature as an argument.
562 \item[\ttindexbold{Sign.stamp_names_of} $sg$]\index{signatures}
563 returns the names of the identification \rmindex{stamps} of ax
564 signature. These coincide with the names of its full ancestry
565 including that of $sg$ itself.
572 Terms belong to the \ML\ type \mltydx{term}, which is a concrete datatype
573 with six constructors:
575 type indexname = string * int;
577 datatype term = Const of string * typ
578 | Free of string * typ
579 | Var of indexname * typ
581 | Abs of string * typ * term
582 | op $ of term * term;
584 \begin{ttdescription}
585 \item[\ttindexbold{Const} ($a$, $T$)] \index{constants|bold}
586 is the {\bf constant} with name~$a$ and type~$T$. Constants include
587 connectives like $\land$ and $\forall$ as well as constants like~0
588 and~$Suc$. Other constants may be required to define a logic's concrete
591 \item[\ttindexbold{Free} ($a$, $T$)] \index{variables!free|bold}
592 is the {\bf free variable} with name~$a$ and type~$T$.
594 \item[\ttindexbold{Var} ($v$, $T$)] \index{unknowns|bold}
595 is the {\bf scheme variable} with indexname~$v$ and type~$T$. An
596 \mltydx{indexname} is a string paired with a non-negative index, or
597 subscript; a term's scheme variables can be systematically renamed by
598 incrementing their subscripts. Scheme variables are essentially free
599 variables, but may be instantiated during unification.
601 \item[\ttindexbold{Bound} $i$] \index{variables!bound|bold}
602 is the {\bf bound variable} with de Bruijn index~$i$, which counts the
603 number of lambdas, starting from zero, between a variable's occurrence
604 and its binding. The representation prevents capture of variables. For
605 more information see de Bruijn \cite{debruijn72} or
606 Paulson~\cite[page~336]{paulson91}.
608 \item[\ttindexbold{Abs} ($a$, $T$, $u$)]
609 \index{lambda abs@$\lambda$-abstractions|bold}
610 is the $\lambda$-{\bf abstraction} with body~$u$, and whose bound
611 variable has name~$a$ and type~$T$. The name is used only for parsing
612 and printing; it has no logical significance.
614 \item[$t$ \$ $u$] \index{$@{\tt\$}|bold} \index{function applications|bold}
615 is the {\bf application} of~$t$ to~$u$.
617 Application is written as an infix operator to aid readability.
618 Here is an \ML\ pattern to recognize \FOL{} formulae of
619 the form~$A\imp B$, binding the subformulae to~$A$ and~$B$:
621 Const("Trueprop",_) $ (Const("op -->",_) $ A $ B)
625 \section{*Variable binding}
627 loose_bnos : term -> int list
628 incr_boundvars : int -> term -> term
629 abstract_over : term*term -> term
630 variant_abs : string * typ * term -> string * term
631 aconv : term * term -> bool\hfill{\bf infix}
633 These functions are all concerned with the de Bruijn representation of
635 \begin{ttdescription}
636 \item[\ttindexbold{loose_bnos} $t$]
637 returns the list of all dangling bound variable references. In
638 particular, {\tt Bound~0} is loose unless it is enclosed in an
639 abstraction. Similarly {\tt Bound~1} is loose unless it is enclosed in
640 at least two abstractions; if enclosed in just one, the list will contain
641 the number 0. A well-formed term does not contain any loose variables.
643 \item[\ttindexbold{incr_boundvars} $j$]
644 increases a term's dangling bound variables by the offset~$j$. This is
645 required when moving a subterm into a context where it is enclosed by a
646 different number of abstractions. Bound variables with a matching
647 abstraction are unaffected.
649 \item[\ttindexbold{abstract_over} $(v,t)$]
650 forms the abstraction of~$t$ over~$v$, which may be any well-formed term.
651 It replaces every occurrence of \(v\) by a {\tt Bound} variable with the
654 \item[\ttindexbold{variant_abs} $(a,T,u)$]
655 substitutes into $u$, which should be the body of an abstraction.
656 It replaces each occurrence of the outermost bound variable by a free
657 variable. The free variable has type~$T$ and its name is a variant
658 of~$a$ chosen to be distinct from all constants and from all variables
661 \item[$t$ \ttindexbold{aconv} $u$]
662 tests whether terms~$t$ and~$u$ are \(\alpha\)-convertible: identical up
663 to renaming of bound variables.
666 Two constants, {\tt Free}s, or {\tt Var}s are \(\alpha\)-convertible
667 if their names and types are equal.
668 (Variables having the same name but different types are thus distinct.
669 This confusing situation should be avoided!)
671 Two bound variables are \(\alpha\)-convertible
672 if they have the same number.
674 Two abstractions are \(\alpha\)-convertible
675 if their bodies are, and their bound variables have the same type.
677 Two applications are \(\alpha\)-convertible
678 if the corresponding subterms are.
683 \section{Certified terms}\index{terms!certified|bold}\index{signatures}
684 A term $t$ can be {\bf certified} under a signature to ensure that every type
685 in~$t$ is well-formed and every constant in~$t$ is a type instance of a
686 constant declared in the signature. The term must be well-typed and its use
687 of bound variables must be well-formed. Meta-rules such as {\tt forall_elim}
688 take certified terms as arguments.
690 Certified terms belong to the abstract type \mltydx{cterm}.
691 Elements of the type can only be created through the certification process.
692 In case of error, Isabelle raises exception~\ttindex{TERM}\@.
694 \subsection{Printing terms}
695 \index{terms!printing of}
697 string_of_cterm : cterm -> string
698 Sign.string_of_term : Sign.sg -> term -> string
700 \begin{ttdescription}
701 \item[\ttindexbold{string_of_cterm} $ct$]
702 displays $ct$ as a string.
704 \item[\ttindexbold{Sign.string_of_term} $sign$ $t$]
705 displays $t$ as a string, using the syntax of~$sign$.
708 \subsection{Making and inspecting certified terms}
710 cterm_of : Sign.sg -> term -> cterm
711 read_cterm : Sign.sg -> string * typ -> cterm
712 cert_axm : Sign.sg -> string * term -> string * term
713 read_axm : Sign.sg -> string * string -> string * term
714 rep_cterm : cterm -> {\ttlbrace}T:typ, t:term, sign:Sign.sg, maxidx:int\ttrbrace
715 Sign.certify_term : Sign.sg -> term -> term * typ * int
717 \begin{ttdescription}
719 \item[\ttindexbold{cterm_of} $sign$ $t$] \index{signatures} certifies
720 $t$ with respect to signature~$sign$.
722 \item[\ttindexbold{read_cterm} $sign$ ($s$, $T$)] reads the string~$s$
723 using the syntax of~$sign$, creating a certified term. The term is
724 checked to have type~$T$; this type also tells the parser what kind
727 \item[\ttindexbold{cert_axm} $sign$ ($name$, $t$)] certifies $t$ with
728 respect to $sign$ as a meta-proposition and converts all exceptions
729 to an error, including the final message
731 The error(s) above occurred in axiom "\(name\)"
734 \item[\ttindexbold{read_axm} $sign$ ($name$, $s$)] similar to {\tt
735 cert_axm}, but first reads the string $s$ using the syntax of
738 \item[\ttindexbold{rep_cterm} $ct$] decomposes $ct$ as a record
739 containing its type, the term itself, its signature, and the maximum
740 subscript of its unknowns. The type and maximum subscript are
741 computed during certification.
743 \item[\ttindexbold{Sign.certify_term}] is a more primitive version of
744 \texttt{cterm_of}, returning the internal representation instead of
745 an abstract \texttt{cterm}.
750 \section{Types}\index{types|bold}
751 Types belong to the \ML\ type \mltydx{typ}, which is a concrete datatype with
752 three constructor functions. These correspond to type constructors, free
753 type variables and schematic type variables. Types are classified by sorts,
754 which are lists of classes (representing an intersection). A class is
755 represented by a string.
758 type sort = class list;
760 datatype typ = Type of string * typ list
761 | TFree of string * sort
762 | TVar of indexname * sort;
765 fun S --> T = Type ("fun", [S, T]);
767 \begin{ttdescription}
768 \item[\ttindexbold{Type} ($a$, $Ts$)] \index{type constructors|bold}
769 applies the {\bf type constructor} named~$a$ to the type operands~$Ts$.
770 Type constructors include~\tydx{fun}, the binary function space
771 constructor, as well as nullary type constructors such as~\tydx{prop}.
772 Other type constructors may be introduced. In expressions, but not in
773 patterns, \hbox{\tt$S$-->$T$} is a convenient shorthand for function
776 \item[\ttindexbold{TFree} ($a$, $s$)] \index{type variables|bold}
777 is the {\bf type variable} with name~$a$ and sort~$s$.
779 \item[\ttindexbold{TVar} ($v$, $s$)] \index{type unknowns|bold}
780 is the {\bf type unknown} with indexname~$v$ and sort~$s$.
781 Type unknowns are essentially free type variables, but may be
782 instantiated during unification.
786 \section{Certified types}
787 \index{types!certified|bold}
788 Certified types, which are analogous to certified terms, have type
791 \subsection{Printing types}
792 \index{types!printing of}
794 string_of_ctyp : ctyp -> string
795 Sign.string_of_typ : Sign.sg -> typ -> string
797 \begin{ttdescription}
798 \item[\ttindexbold{string_of_ctyp} $cT$]
799 displays $cT$ as a string.
801 \item[\ttindexbold{Sign.string_of_typ} $sign$ $T$]
802 displays $T$ as a string, using the syntax of~$sign$.
806 \subsection{Making and inspecting certified types}
808 ctyp_of : Sign.sg -> typ -> ctyp
809 rep_ctyp : ctyp -> {\ttlbrace}T: typ, sign: Sign.sg\ttrbrace
810 Sign.certify_typ : Sign.sg -> typ -> typ
812 \begin{ttdescription}
814 \item[\ttindexbold{ctyp_of} $sign$ $T$] \index{signatures} certifies
815 $T$ with respect to signature~$sign$.
817 \item[\ttindexbold{rep_ctyp} $cT$] decomposes $cT$ as a record
818 containing the type itself and its signature.
820 \item[\ttindexbold{Sign.certify_typ}] is a more primitive version of
821 \texttt{ctyp_of}, returning the internal representation instead of
822 an abstract \texttt{ctyp}.
827 \section{Oracles: calling trusted external reasoners}
831 Oracles allow Isabelle to take advantage of external reasoners such as
832 arithmetic decision procedures, model checkers, fast tautology checkers or
833 computer algebra systems. Invoked as an oracle, an external reasoner can
834 create arbitrary Isabelle theorems. It is your responsibility to ensure that
835 the external reasoner is as trustworthy as your application requires.
836 Isabelle's proof objects~(\S\ref{sec:proofObjects}) record how each theorem
837 depends upon oracle calls.
840 invoke_oracle : theory -> xstring -> Sign.sg * object -> thm
841 Theory.add_oracle : bstring * (Sign.sg * object -> term) -> theory
844 \begin{ttdescription}
845 \item[\ttindexbold{invoke_oracle} $thy$ $name$ ($sign$, $data$)]
846 invokes the oracle $name$ of theory $thy$ passing the information
847 contained in the exception value $data$ and creating a theorem
848 having signature $sign$. Note that type \ttindex{object} is just an
849 abbreviation for \texttt{exn}. Errors arise if $thy$ does not have
850 an oracle called $name$, if the oracle rejects its arguments or if
851 its result is ill-typed.
853 \item[\ttindexbold{Theory.add_oracle} $name$ $fun$ $thy$] extends
854 $thy$ by oracle $fun$ called $name$. It is seldom called
855 explicitly, as there is concrete syntax for oracles in theory files.
858 A curious feature of {\ML} exceptions is that they are ordinary constructors.
859 The {\ML} type {\tt exn} is a datatype that can be extended at any time. (See
860 my {\em {ML} for the Working Programmer}~\cite{paulson-ml2}, especially
861 page~136.) The oracle mechanism takes advantage of this to allow an oracle to
862 take any information whatever.
864 There must be some way of invoking the external reasoner from \ML, either
865 because it is coded in {\ML} or via an operating system interface. Isabelle
866 expects the {\ML} function to take two arguments: a signature and an
869 \item The signature will typically be that of a desendant of the theory
870 declaring the oracle. The oracle will use it to distinguish constants from
871 variables, etc., and it will be attached to the generated theorems.
873 \item The exception is used to pass arbitrary information to the oracle. This
874 information must contain a full description of the problem to be solved by
875 the external reasoner, including any additional information that might be
876 required. The oracle may raise the exception to indicate that it cannot
877 solve the specified problem.
880 A trivial example is provided in theory {\tt FOL/ex/IffOracle}. This
881 oracle generates tautologies of the form $P\bimp\cdots\bimp P$, with
882 an even number of $P$s.
884 The \texttt{ML} section of \texttt{IffOracle.thy} begins by declaring
885 a few auxiliary functions (suppressed below) for creating the
886 tautologies. Then it declares a new exception constructor for the
887 information required by the oracle: here, just an integer. It finally
888 defines the oracle function itself.
890 exception IffOracleExn of int;\medskip
891 fun mk_iff_oracle (sign, IffOracleExn n) =
892 if n > 0 andalso n mod 2 = 0
893 then Trueprop $ mk_iff n
894 else raise IffOracleExn n;
896 Observe the function's two arguments, the signature {\tt sign} and the
897 exception given as a pattern. The function checks its argument for
898 validity. If $n$ is positive and even then it creates a tautology
899 containing $n$ occurrences of~$P$. Otherwise it signals error by
900 raising its own exception (just by happy coincidence). Errors may be
901 signalled by other means, such as returning the theorem {\tt True}.
902 Please ensure that the oracle's result is correctly typed; Isabelle
903 will reject ill-typed theorems by raising a cryptic exception at top
906 The \texttt{oracle} section of {\tt IffOracle.thy} installs above
907 \texttt{ML} function as follows:
909 IffOracle = FOL +\medskip
911 iff = mk_iff_oracle\medskip
915 Now in \texttt{IffOracle.ML} we first define a wrapper for invoking
918 fun iff_oracle n = invoke_oracle IffOracle.thy "iff"
919 (sign_of IffOracle.thy, IffOracleExn n);
922 Here are some example applications of the \texttt{iff} oracle. An
923 argument of 10 is allowed, but one of 5 is forbidden:
926 {\out "P <-> P <-> P <-> P <-> P <-> P <-> P <-> P <-> P <-> P" : thm}
928 {\out Exception- IffOracleExn 5 raised}