%% $Id$
\chapter{Theories, Terms and Types} \label{theories}
\index{theories|(}\index{signatures|bold}
\index{reading!axioms|see{{\tt assume_ax}}} Theories organize the
syntax, declarations and axioms of a mathematical development. They
are built, starting from the {\Pure} or {\CPure} theory, by extending
and merging existing theories. They have the \ML\ type
\mltydx{theory}. Theory operations signal errors by raising exception
\xdx{THEORY}, returning a message and a list of theories.
Signatures, which contain information about sorts, types, constants and
syntax, have the \ML\ type~\mltydx{Sign.sg}. For identification, each
signature carries a unique list of \bfindex{stamps}, which are \ML\
references to strings. The strings serve as human-readable names; the
references serve as unique identifiers. Each primitive signature has a
single stamp. When two signatures are merged, their lists of stamps are
also merged. Every theory carries a unique signature.
Terms and types are the underlying representation of logical syntax. Their
\ML\ definitions are irrelevant to naive Isabelle users. Programmers who
wish to extend Isabelle may need to know such details, say to code a tactic
that looks for subgoals of a particular form. Terms and types may be
`certified' to be well-formed with respect to a given signature.
\section{Defining theories}\label{sec:ref-defining-theories}
Theories are defined via theory files $name$\texttt{.thy} (there are also
\ML-level interfaces which are only intended for people building advanced
theory definition packages). Appendix~\ref{app:TheorySyntax} presents the
concrete syntax for theory files; here follows an explanation of the
constituent parts.
\begin{description}
\item[{\it theoryDef}] is the full definition. The new theory is called $id$.
It is the union of the named {\bf parent
theories}\indexbold{theories!parent}, possibly extended with new
components. \thydx{Pure} and \thydx{CPure} are the basic theories, which
contain only the meta-logic. They differ just in their concrete syntax for
function applications.
The new theory begins as a merge of its parents.
\begin{ttbox}
Attempt to merge different versions of theories: "\(T@1\)", \(\ldots\), "\(T@n\)"
\end{ttbox}
This error may especially occur when a theory is redeclared --- say to
change an inappropriate definition --- and bindings to old versions persist.
Isabelle ensures that old and new theories of the same name are not involved
in a proof.
\item[$classes$]
is a series of class declarations. Declaring {\tt$id$ < $id@1$ \dots\
$id@n$} makes $id$ a subclass of the existing classes $id@1\dots
id@n$. This rules out cyclic class structures. Isabelle automatically
computes the transitive closure of subclass hierarchies; it is not
necessary to declare {\tt c < e} in addition to {\tt c < d} and {\tt d <
e}.
\item[$default$]
introduces $sort$ as the new default sort for type variables. This applies
to unconstrained type variables in an input string but not to type
variables created internally. If omitted, the default sort is the listwise
union of the default sorts of the parent theories (i.e.\ their logical
intersection).
\item[$sort$] is a finite set of classes. A single class $id$
abbreviates the sort $\ttlbrace id\ttrbrace$.
\item[$types$]
is a series of type declarations. Each declares a new type constructor
or type synonym. An $n$-place type constructor is specified by
$(\alpha@1,\dots,\alpha@n)name$, where the type variables serve only to
indicate the number~$n$.
A {\bf type synonym}\indexbold{type synonyms} is an abbreviation
$(\alpha@1,\dots,\alpha@n)name = \tau$, where $name$ and $\tau$ can
be strings.
\item[$infix$]
declares a type or constant to be an infix operator of priority $nat$
associating to the left ({\tt infixl}) or right ({\tt infixr}). Only
2-place type constructors can have infix status; an example is {\tt
('a,'b)~"*"~(infixr~20)}, which may express binary product types.
\item[$arities$] is a series of type arity declarations. Each assigns
arities to type constructors. The $name$ must be an existing type
constructor, which is given the additional arity $arity$.
\item[$nonterminals$]\index{*nonterminal symbols} declares purely
syntactic types to be used as nonterminal symbols of the context
free grammar.
\item[$consts$] is a series of constant declarations. Each new
constant $name$ is given the specified type. The optional $mixfix$
annotations may attach concrete syntax to the constant.
\item[$syntax$] \index{*syntax section}\index{print mode} is a variant
of $consts$ which adds just syntax without actually declaring
logical constants. This gives full control over a theory's context
free grammar. The optional $mode$ specifies the print mode where the
mixfix productions should be added. If there is no \texttt{output}
option given, all productions are also added to the input syntax
(regardless of the print mode).
\item[$mixfix$] \index{mixfix declarations}
annotations can take three forms:
\begin{itemize}
\item A mixfix template given as a $string$ of the form
{\tt"}\dots{\tt\_}\dots{\tt\_}\dots{\tt"} where the $i$-th underscore
indicates the position where the $i$-th argument should go. The list
of numbers gives the priority of each argument. The final number gives
the priority of the whole construct.
\item A constant $f$ of type $\tau@1\To(\tau@2\To\tau)$ can be given {\bf
infix} status.
\item A constant $f$ of type $(\tau@1\To\tau@2)\To\tau$ can be given {\bf
binder} status. The declaration {\tt binder} $\cal Q$ $p$ causes
${\cal Q}\,x.F(x)$ to be treated
like $f(F)$, where $p$ is the priority.
\end{itemize}
\item[$trans$]
specifies syntactic translation rules (macros). There are three forms:
parse rules ({\tt =>}), print rules ({\tt <=}), and parse/print rules ({\tt
==}).
\item[$rules$]
is a series of rule declarations. Each has a name $id$ and the formula is
given by the $string$. Rule names must be distinct within any single
theory.
\item[$defs$] is a series of definitions. They are just like $rules$, except
that every $string$ must be a definition (see below for details).
\item[$constdefs$] combines the declaration of constants and their
definition. The first $string$ is the type, the second the definition.
\item[$axclass$] \index{*axclass section} defines an
\rmindex{axiomatic type class} as the intersection of existing
classes, with additional axioms holding. Class axioms may not
contain more than one type variable. The class axioms (with implicit
sort constraints added) are bound to the given names. Furthermore a
class introduction rule is generated, which is automatically
employed by $instance$ to prove instantiations of this class.
\item[$instance$] \index{*instance section} proves class inclusions or
type arities at the logical level and then transfers these to the
type signature. The instantiation is proven and checked properly.
The user has to supply sufficient witness information: theorems
($longident$), axioms ($string$), or even arbitrary \ML{} tactic
code $verbatim$.
\item[$oracle$] links the theory to a trusted external reasoner. It is
allowed to create theorems, but each theorem carries a proof object
describing the oracle invocation. See \S\ref{sec:oracles} for details.
\item[$local$, $global$] change the current name declaration mode.
Initially, theories start in $local$ mode, causing all names of
types, constants, axioms etc.\ to be automatically qualified by the
theory name. Changing this to $global$ causes all names to be
declared as short base names only.
The $local$ and $global$ declarations act like switches, affecting
all following theory sections until changed again explicitly. Also
note that the final state at the end of the theory will persist. In
particular, this determines how the names of theorems stored later
on are handled.
\item[$setup$]\index{*setup!theory} applies a list of ML functions to
the theory. The argument should denote a value of type
\texttt{(theory -> theory) list}. Typically, ML packages are
initialized in this way.
\item[$ml$] \index{*ML section}
consists of \ML\ code, typically for parse and print translation functions.
\end{description}
%
Chapters~\ref{Defining-Logics} and \ref{chap:syntax} explain mixfix
declarations, translation rules and the {\tt ML} section in more detail.
\subsection{Definitions}\indexbold{definitions}
{\bf Definitions} are intended to express abbreviations. The simplest
form of a definition is $f \equiv t$, where $f$ is a constant.
Isabelle also allows a derived forms where the arguments of~$f$ appear
on the left, abbreviating a string of $\lambda$-abstractions.
Isabelle makes the following checks on definitions:
\begin{itemize}
\item Arguments (on the left-hand side) must be distinct variables.
\item All variables on the right-hand side must also appear on the left-hand
side.
\item All type variables on the right-hand side must also appear on
the left-hand side; this prohibits definitions such as {\tt
(zero::nat) == length ([]::'a list)}.
\item The definition must not be recursive. Most object-logics provide
definitional principles that can be used to express recursion safely.
\end{itemize}
These checks are intended to catch the sort of errors that might be made
accidentally. Misspellings, for instance, might result in additional
variables appearing on the right-hand side. More elaborate checks could be
made, but the cost might be overly strict rules on declaration order, etc.
\subsection{*Classes and arities}
\index{classes!context conditions}\index{arities!context conditions}
In order to guarantee principal types~\cite{nipkow-prehofer},
arity declarations must obey two conditions:
\begin{itemize}
\item There must not be any two declarations $ty :: (\vec{r})c$ and
$ty :: (\vec{s})c$ with $\vec{r} \neq \vec{s}$. For example, this
excludes the following:
\begin{ttbox}
arities
foo :: ({\ttlbrace}logic{\ttrbrace}) logic
foo :: ({\ttlbrace}{\ttrbrace})logic
\end{ttbox}
\item If there are two declarations $ty :: (s@1,\dots,s@n)c$ and $ty ::
(s@1',\dots,s@n')c'$ such that $c' < c$ then $s@i' \preceq s@i$ must hold
for $i=1,\dots,n$. The relationship $\preceq$, defined as
\[ s' \preceq s \iff \forall c\in s. \exists c'\in s'.~ c'\le c, \]
expresses that the set of types represented by $s'$ is a subset of the
set of types represented by $s$. Assuming $term \preceq logic$, the
following is forbidden:
\begin{ttbox}
arities
foo :: ({\ttlbrace}logic{\ttrbrace})logic
foo :: ({\ttlbrace}{\ttrbrace})term
\end{ttbox}
\end{itemize}
\section{The theory loader}\label{sec:more-theories}
\index{theories!reading}\index{files!reading}
Isabelle's theory loader manages dependencies of the internal graph of theory
nodes (the \emph{theory database}) and the external view of the file system.
See \S\ref{sec:intro-theories} for its most basic commands, such as
\texttt{use_thy}. There are a few more operations available.
\begin{ttbox}
use_thy_only : string -> unit
update_thy : string -> unit
touch_thy : string -> unit
delete_tmpfiles : bool ref \hfill{\bf initially true}
\end{ttbox}
\begin{ttdescription}
\item[\ttindexbold{use_thy_only} "$name$";] is similar to \texttt{use_thy},
but processes the actual theory file $name$\texttt{.thy} only, ignoring
$name$\texttt{.ML}. This might be useful in replaying proof scripts by hand
from the very beginning, starting with the fresh theory.
\item[\ttindexbold{update_thy} "$name$";] is similar to \texttt{use_thy}, but
ensures that theory $name$ is fully up-to-date with respect to the file
system --- apart from $name$ itself any of its ancestors may be reloaded as
well.
\item[\ttindexbold{touch_thy} "$name$";] marks theory node $name$ of the
internal graph as outdated. While the theory remains usable, subsequent
operations such as \texttt{use_thy} may cause a reload.
\item[reset \ttindexbold{delete_tmpfiles};] processing theory files usually
involves temporary {\ML} files to be created. By default, these are deleted
afterwards. Resetting the \texttt{delete_tmpfiles} flag inhibits this,
leaving the generated code for debugging purposes. The basic location for
temporary files is determined by the \texttt{ISABELLE_TMP} environment
variable (which is private to the running Isabelle process and may be
retrieved by \ttindex{getenv} from {\ML}).
\end{ttdescription}
\medskip Theory and {\ML} files are located by skimming through the
directories listed in Isabelle's internal load path, which merely contains the
current directory ``\texttt{.}'' by default. The load path may be accessed by
the following operations.
\begin{ttbox}
show_path: unit -> string list
add_path: string -> unit
del_path: string -> unit
reset_path: unit -> unit
\end{ttbox}
\begin{ttdescription}
\item[\ttindexbold{show_path}();] displays the load path components in
canonical string representation (which is always according to Unix rules).
\item[\ttindexbold{add_path} "$dir$";] adds component $dir$ to the beginning
of the load path.
\item[\ttindexbold{del_path} "$dir$";] removes any occurrences of component
$dir$ from the load path.
\item[\ttindexbold{reset_path}();] resets the load path to ``\texttt{.}''
(current directory) only.
\end{ttdescription}
In operations referring indirectly to some file, the argument may be prefixed
by a directory that will be used as temporary load path, e.g.\
\texttt{use_thy~"$dir/name$"}. Note that, depending on which parts of the
ancestry of $name$ are already loaded, the dynamic change of paths might be
hard to predict. Use this feature with care only.
\section{Basic operations on theories}\label{BasicOperationsOnTheories}
\subsection{*Theory inclusion}
\begin{ttbox}
subthy : theory * theory -> bool
eq_thy : theory * theory -> bool
transfer : theory -> thm -> thm
transfer_sg : Sign.sg -> thm -> thm
\end{ttbox}
Inclusion and equality of theories is determined by unique
identification stamps that are created when declaring new components.
Theorems contain a reference to the theory (actually to its signature)
they have been derived in. Transferring theorems to super theories
has no logical significance, but may affect some operations in subtle
ways (e.g.\ implicit merges of signatures when applying rules, or
pretty printing of theorems).
\begin{ttdescription}
\item[\ttindexbold{subthy} ($thy@1$, $thy@2$)] determines if $thy@1$
is included in $thy@2$ wrt.\ identification stamps.
\item[\ttindexbold{eq_thy} ($thy@1$, $thy@2$)] determines if $thy@1$
is exactly the same as $thy@2$.
\item[\ttindexbold{transfer} $thy$ $thm$] transfers theorem $thm$ to
theory $thy$, provided the latter includes the theory of $thm$.
\item[\ttindexbold{transfer_sg} $sign$ $thm$] is similar to
\texttt{transfer}, but identifies the super theory via its
signature.
\end{ttdescription}
\subsection{*Primitive theories}
\begin{ttbox}
ProtoPure.thy : theory
Pure.thy : theory
CPure.thy : theory
\end{ttbox}
\begin{description}
\item[\ttindexbold{ProtoPure.thy}, \ttindexbold{Pure.thy},
\ttindexbold{CPure.thy}] contain the syntax and signature of the
meta-logic. There are basically no axioms: meta-level inferences
are carried out by \ML\ functions. \texttt{Pure} and \texttt{CPure}
just differ in their concrete syntax of prefix function application:
$t(u@1, \ldots, u@n)$ in \texttt{Pure} vs.\ $t\,u@1,\ldots\,u@n$ in
\texttt{CPure}. \texttt{ProtoPure} is their common parent,
containing no syntax for printing prefix applications at all!
%%FIXME
%\item[\ttindexbold{merge_theories} $name$ ($thy@1$, $thy@2$)] merges
% the two theories $thy@1$ and $thy@2$, creating a new named theory
% node. The resulting theory contains all of the syntax, signature
% and axioms of the constituent theories. Merging theories that
% contain different identification stamps of the same name fails with
% the following message
%% FIXME
%\item [\ttindexbold{extend_theory} $thy$ {\tt"}$T${\tt"} $\cdots$] extends
% the theory $thy$ with new types, constants, etc. $T$ identifies the theory
% internally. When a theory is redeclared, say to change an incorrect axiom,
% bindings to the old axiom may persist. Isabelle ensures that the old and
% new theories are not involved in the same proof. Attempting to combine
% different theories having the same name $T$ yields the fatal error
%extend_theory : theory -> string -> \(\cdots\) -> theory
%\begin{ttbox}
%Attempt to merge different versions of theory: \(T\)
%\end{ttbox}
\end{description}
%% FIXME
%\item [\ttindexbold{extend_theory} $thy$ {\tt"}$T${\tt"}
% ($classes$, $default$, $types$, $arities$, $consts$, $sextopt$) $rules$]
%\hfill\break %%% include if line is just too short
%is the \ML{} equivalent of the following theory definition:
%\begin{ttbox}
%\(T\) = \(thy\) +
%classes \(c\) < \(c@1\),\(\dots\),\(c@m\)
% \dots
%default {\(d@1,\dots,d@r\)}
%types \(tycon@1\),\dots,\(tycon@i\) \(n\)
% \dots
%arities \(tycon@1'\),\dots,\(tycon@j'\) :: (\(s@1\),\dots,\(s@n\))\(c\)
% \dots
%consts \(b@1\),\dots,\(b@k\) :: \(\tau\)
% \dots
%rules \(name\) \(rule\)
% \dots
%end
%\end{ttbox}
%where
%\begin{tabular}[t]{l@{~=~}l}
%$classes$ & \tt[("$c$",["$c@1$",\dots,"$c@m$"]),\dots] \\
%$default$ & \tt["$d@1$",\dots,"$d@r$"]\\
%$types$ & \tt[([$tycon@1$,\dots,$tycon@i$], $n$),\dots] \\
%$arities$ & \tt[([$tycon'@1$,\dots,$tycon'@j$], ([$s@1$,\dots,$s@n$],$c$)),\dots]
%\\
%$consts$ & \tt[([$b@1$,\dots,$b@k$],$\tau$),\dots] \\
%$rules$ & \tt[("$name$",$rule$),\dots]
%\end{tabular}
\subsection{Inspecting a theory}\label{sec:inspct-thy}
\index{theories!inspecting|bold}
\begin{ttbox}
print_syntax : theory -> unit
print_theory : theory -> unit
parents_of : theory -> theory list
ancestors_of : theory -> theory list
sign_of : theory -> Sign.sg
Sign.stamp_names_of : Sign.sg -> string list
\end{ttbox}
These provide means of viewing a theory's components.
\begin{ttdescription}
\item[\ttindexbold{print_syntax} $thy$] prints the syntax of $thy$
(grammar, macros, translation functions etc., see
page~\pageref{pg:print_syn} for more details).
\item[\ttindexbold{print_theory} $thy$] prints the logical parts of
$thy$, excluding the syntax.
\item[\ttindexbold{parents_of} $thy$] returns the direct ancestors
of~$thy$.
\item[\ttindexbold{ancestors_of} $thy$] returns all ancestors of~$thy$
(not including $thy$ itself).
\item[\ttindexbold{sign_of} $thy$] returns the signature associated
with~$thy$. It is useful with functions like {\tt
read_instantiate_sg}, which take a signature as an argument.
\item[\ttindexbold{Sign.stamp_names_of} $sg$]\index{signatures}
returns the names of the identification \rmindex{stamps} of ax
signature. These coincide with the names of its full ancestry
including that of $sg$ itself.
\end{ttdescription}
\section{Terms}
\index{terms|bold}
Terms belong to the \ML\ type \mltydx{term}, which is a concrete datatype
with six constructors:
\begin{ttbox}
type indexname = string * int;
infix 9 $;
datatype term = Const of string * typ
| Free of string * typ
| Var of indexname * typ
| Bound of int
| Abs of string * typ * term
| op $ of term * term;
\end{ttbox}
\begin{ttdescription}
\item[\ttindexbold{Const} ($a$, $T$)] \index{constants|bold}
is the {\bf constant} with name~$a$ and type~$T$. Constants include
connectives like $\land$ and $\forall$ as well as constants like~0
and~$Suc$. Other constants may be required to define a logic's concrete
syntax.
\item[\ttindexbold{Free} ($a$, $T$)] \index{variables!free|bold}
is the {\bf free variable} with name~$a$ and type~$T$.
\item[\ttindexbold{Var} ($v$, $T$)] \index{unknowns|bold}
is the {\bf scheme variable} with indexname~$v$ and type~$T$. An
\mltydx{indexname} is a string paired with a non-negative index, or
subscript; a term's scheme variables can be systematically renamed by
incrementing their subscripts. Scheme variables are essentially free
variables, but may be instantiated during unification.
\item[\ttindexbold{Bound} $i$] \index{variables!bound|bold}
is the {\bf bound variable} with de Bruijn index~$i$, which counts the
number of lambdas, starting from zero, between a variable's occurrence
and its binding. The representation prevents capture of variables. For
more information see de Bruijn \cite{debruijn72} or
Paulson~\cite[page~376]{paulson-ml2}.
\item[\ttindexbold{Abs} ($a$, $T$, $u$)]
\index{lambda abs@$\lambda$-abstractions|bold}
is the $\lambda$-{\bf abstraction} with body~$u$, and whose bound
variable has name~$a$ and type~$T$. The name is used only for parsing
and printing; it has no logical significance.
\item[$t$ \$ $u$] \index{$@{\tt\$}|bold} \index{function applications|bold}
is the {\bf application} of~$t$ to~$u$.
\end{ttdescription}
Application is written as an infix operator to aid readability.
Here is an \ML\ pattern to recognize \FOL{} formulae of
the form~$A\imp B$, binding the subformulae to~$A$ and~$B$:
\begin{ttbox}
Const("Trueprop",_) $ (Const("op -->",_) $ A $ B)
\end{ttbox}
\section{*Variable binding}
\begin{ttbox}
loose_bnos : term -> int list
incr_boundvars : int -> term -> term
abstract_over : term*term -> term
variant_abs : string * typ * term -> string * term
aconv : term * term -> bool\hfill{\bf infix}
\end{ttbox}
These functions are all concerned with the de Bruijn representation of
bound variables.
\begin{ttdescription}
\item[\ttindexbold{loose_bnos} $t$]
returns the list of all dangling bound variable references. In
particular, {\tt Bound~0} is loose unless it is enclosed in an
abstraction. Similarly {\tt Bound~1} is loose unless it is enclosed in
at least two abstractions; if enclosed in just one, the list will contain
the number 0. A well-formed term does not contain any loose variables.
\item[\ttindexbold{incr_boundvars} $j$]
increases a term's dangling bound variables by the offset~$j$. This is
required when moving a subterm into a context where it is enclosed by a
different number of abstractions. Bound variables with a matching
abstraction are unaffected.
\item[\ttindexbold{abstract_over} $(v,t)$]
forms the abstraction of~$t$ over~$v$, which may be any well-formed term.
It replaces every occurrence of \(v\) by a {\tt Bound} variable with the
correct index.
\item[\ttindexbold{variant_abs} $(a,T,u)$]
substitutes into $u$, which should be the body of an abstraction.
It replaces each occurrence of the outermost bound variable by a free
variable. The free variable has type~$T$ and its name is a variant
of~$a$ chosen to be distinct from all constants and from all variables
free in~$u$.
\item[$t$ \ttindexbold{aconv} $u$]
tests whether terms~$t$ and~$u$ are \(\alpha\)-convertible: identical up
to renaming of bound variables.
\begin{itemize}
\item
Two constants, {\tt Free}s, or {\tt Var}s are \(\alpha\)-convertible
if their names and types are equal.
(Variables having the same name but different types are thus distinct.
This confusing situation should be avoided!)
\item
Two bound variables are \(\alpha\)-convertible
if they have the same number.
\item
Two abstractions are \(\alpha\)-convertible
if their bodies are, and their bound variables have the same type.
\item
Two applications are \(\alpha\)-convertible
if the corresponding subterms are.
\end{itemize}
\end{ttdescription}
\section{Certified terms}\index{terms!certified|bold}\index{signatures}
A term $t$ can be {\bf certified} under a signature to ensure that every type
in~$t$ is well-formed and every constant in~$t$ is a type instance of a
constant declared in the signature. The term must be well-typed and its use
of bound variables must be well-formed. Meta-rules such as {\tt forall_elim}
take certified terms as arguments.
Certified terms belong to the abstract type \mltydx{cterm}.
Elements of the type can only be created through the certification process.
In case of error, Isabelle raises exception~\ttindex{TERM}\@.
\subsection{Printing terms}
\index{terms!printing of}
\begin{ttbox}
string_of_cterm : cterm -> string
Sign.string_of_term : Sign.sg -> term -> string
\end{ttbox}
\begin{ttdescription}
\item[\ttindexbold{string_of_cterm} $ct$]
displays $ct$ as a string.
\item[\ttindexbold{Sign.string_of_term} $sign$ $t$]
displays $t$ as a string, using the syntax of~$sign$.
\end{ttdescription}
\subsection{Making and inspecting certified terms}
\begin{ttbox}
cterm_of : Sign.sg -> term -> cterm
read_cterm : Sign.sg -> string * typ -> cterm
cert_axm : Sign.sg -> string * term -> string * term
read_axm : Sign.sg -> string * string -> string * term
rep_cterm : cterm -> {\ttlbrace}T:typ, t:term, sign:Sign.sg, maxidx:int\ttrbrace
Sign.certify_term : Sign.sg -> term -> term * typ * int
\end{ttbox}
\begin{ttdescription}
\item[\ttindexbold{cterm_of} $sign$ $t$] \index{signatures} certifies
$t$ with respect to signature~$sign$.
\item[\ttindexbold{read_cterm} $sign$ ($s$, $T$)] reads the string~$s$
using the syntax of~$sign$, creating a certified term. The term is
checked to have type~$T$; this type also tells the parser what kind
of phrase to parse.
\item[\ttindexbold{cert_axm} $sign$ ($name$, $t$)] certifies $t$ with
respect to $sign$ as a meta-proposition and converts all exceptions
to an error, including the final message
\begin{ttbox}
The error(s) above occurred in axiom "\(name\)"
\end{ttbox}
\item[\ttindexbold{read_axm} $sign$ ($name$, $s$)] similar to {\tt
cert_axm}, but first reads the string $s$ using the syntax of
$sign$.
\item[\ttindexbold{rep_cterm} $ct$] decomposes $ct$ as a record
containing its type, the term itself, its signature, and the maximum
subscript of its unknowns. The type and maximum subscript are
computed during certification.
\item[\ttindexbold{Sign.certify_term}] is a more primitive version of
\texttt{cterm_of}, returning the internal representation instead of
an abstract \texttt{cterm}.
\end{ttdescription}
\section{Types}\index{types|bold}
Types belong to the \ML\ type \mltydx{typ}, which is a concrete datatype with
three constructor functions. These correspond to type constructors, free
type variables and schematic type variables. Types are classified by sorts,
which are lists of classes (representing an intersection). A class is
represented by a string.
\begin{ttbox}
type class = string;
type sort = class list;
datatype typ = Type of string * typ list
| TFree of string * sort
| TVar of indexname * sort;
infixr 5 -->;
fun S --> T = Type ("fun", [S, T]);
\end{ttbox}
\begin{ttdescription}
\item[\ttindexbold{Type} ($a$, $Ts$)] \index{type constructors|bold}
applies the {\bf type constructor} named~$a$ to the type operands~$Ts$.
Type constructors include~\tydx{fun}, the binary function space
constructor, as well as nullary type constructors such as~\tydx{prop}.
Other type constructors may be introduced. In expressions, but not in
patterns, \hbox{\tt$S$-->$T$} is a convenient shorthand for function
types.
\item[\ttindexbold{TFree} ($a$, $s$)] \index{type variables|bold}
is the {\bf type variable} with name~$a$ and sort~$s$.
\item[\ttindexbold{TVar} ($v$, $s$)] \index{type unknowns|bold}
is the {\bf type unknown} with indexname~$v$ and sort~$s$.
Type unknowns are essentially free type variables, but may be
instantiated during unification.
\end{ttdescription}
\section{Certified types}
\index{types!certified|bold}
Certified types, which are analogous to certified terms, have type
\ttindexbold{ctyp}.
\subsection{Printing types}
\index{types!printing of}
\begin{ttbox}
string_of_ctyp : ctyp -> string
Sign.string_of_typ : Sign.sg -> typ -> string
\end{ttbox}
\begin{ttdescription}
\item[\ttindexbold{string_of_ctyp} $cT$]
displays $cT$ as a string.
\item[\ttindexbold{Sign.string_of_typ} $sign$ $T$]
displays $T$ as a string, using the syntax of~$sign$.
\end{ttdescription}
\subsection{Making and inspecting certified types}
\begin{ttbox}
ctyp_of : Sign.sg -> typ -> ctyp
rep_ctyp : ctyp -> {\ttlbrace}T: typ, sign: Sign.sg\ttrbrace
Sign.certify_typ : Sign.sg -> typ -> typ
\end{ttbox}
\begin{ttdescription}
\item[\ttindexbold{ctyp_of} $sign$ $T$] \index{signatures} certifies
$T$ with respect to signature~$sign$.
\item[\ttindexbold{rep_ctyp} $cT$] decomposes $cT$ as a record
containing the type itself and its signature.
\item[\ttindexbold{Sign.certify_typ}] is a more primitive version of
\texttt{ctyp_of}, returning the internal representation instead of
an abstract \texttt{ctyp}.
\end{ttdescription}
\section{Oracles: calling trusted external reasoners}
\label{sec:oracles}
\index{oracles|(}
Oracles allow Isabelle to take advantage of external reasoners such as
arithmetic decision procedures, model checkers, fast tautology checkers or
computer algebra systems. Invoked as an oracle, an external reasoner can
create arbitrary Isabelle theorems. It is your responsibility to ensure that
the external reasoner is as trustworthy as your application requires.
Isabelle's proof objects~(\S\ref{sec:proofObjects}) record how each theorem
depends upon oracle calls.
\begin{ttbox}
invoke_oracle : theory -> xstring -> Sign.sg * object -> thm
Theory.add_oracle : bstring * (Sign.sg * object -> term) -> theory
-> theory
\end{ttbox}
\begin{ttdescription}
\item[\ttindexbold{invoke_oracle} $thy$ $name$ ($sign$, $data$)]
invokes the oracle $name$ of theory $thy$ passing the information
contained in the exception value $data$ and creating a theorem
having signature $sign$. Note that type \ttindex{object} is just an
abbreviation for \texttt{exn}. Errors arise if $thy$ does not have
an oracle called $name$, if the oracle rejects its arguments or if
its result is ill-typed.
\item[\ttindexbold{Theory.add_oracle} $name$ $fun$ $thy$] extends
$thy$ by oracle $fun$ called $name$. It is seldom called
explicitly, as there is concrete syntax for oracles in theory files.
\end{ttdescription}
A curious feature of {\ML} exceptions is that they are ordinary constructors.
The {\ML} type {\tt exn} is a datatype that can be extended at any time. (See
my {\em {ML} for the Working Programmer}~\cite{paulson-ml2}, especially
page~136.) The oracle mechanism takes advantage of this to allow an oracle to
take any information whatever.
There must be some way of invoking the external reasoner from \ML, either
because it is coded in {\ML} or via an operating system interface. Isabelle
expects the {\ML} function to take two arguments: a signature and an
exception object.
\begin{itemize}
\item The signature will typically be that of a desendant of the theory
declaring the oracle. The oracle will use it to distinguish constants from
variables, etc., and it will be attached to the generated theorems.
\item The exception is used to pass arbitrary information to the oracle. This
information must contain a full description of the problem to be solved by
the external reasoner, including any additional information that might be
required. The oracle may raise the exception to indicate that it cannot
solve the specified problem.
\end{itemize}
A trivial example is provided in theory {\tt FOL/ex/IffOracle}. This
oracle generates tautologies of the form $P\bimp\cdots\bimp P$, with
an even number of $P$s.
The \texttt{ML} section of \texttt{IffOracle.thy} begins by declaring
a few auxiliary functions (suppressed below) for creating the
tautologies. Then it declares a new exception constructor for the
information required by the oracle: here, just an integer. It finally
defines the oracle function itself.
\begin{ttbox}
exception IffOracleExn of int;\medskip
fun mk_iff_oracle (sign, IffOracleExn n) =
if n > 0 andalso n mod 2 = 0
then Trueprop $ mk_iff n
else raise IffOracleExn n;
\end{ttbox}
Observe the function's two arguments, the signature {\tt sign} and the
exception given as a pattern. The function checks its argument for
validity. If $n$ is positive and even then it creates a tautology
containing $n$ occurrences of~$P$. Otherwise it signals error by
raising its own exception (just by happy coincidence). Errors may be
signalled by other means, such as returning the theorem {\tt True}.
Please ensure that the oracle's result is correctly typed; Isabelle
will reject ill-typed theorems by raising a cryptic exception at top
level.
The \texttt{oracle} section of {\tt IffOracle.thy} installs above
\texttt{ML} function as follows:
\begin{ttbox}
IffOracle = FOL +\medskip
oracle
iff = mk_iff_oracle\medskip
end
\end{ttbox}
Now in \texttt{IffOracle.ML} we first define a wrapper for invoking
the oracle:
\begin{ttbox}
fun iff_oracle n = invoke_oracle IffOracle.thy "iff"
(sign_of IffOracle.thy, IffOracleExn n);
\end{ttbox}
Here are some example applications of the \texttt{iff} oracle. An
argument of 10 is allowed, but one of 5 is forbidden:
\begin{ttbox}
iff_oracle 10;
{\out "P <-> P <-> P <-> P <-> P <-> P <-> P <-> P <-> P <-> P" : thm}
iff_oracle 5;
{\out Exception- IffOracleExn 5 raised}
\end{ttbox}
\index{oracles|)}
\index{theories|)}
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "ref"
%%% End: