doc-src/Ref/theories.tex

first draft of Springer book

%% $Id$

\chapter{Theories, Terms and Types} \label{theories}
\index{theories|(}\index{signatures|bold}
\index{reading!axioms|see{{\tt extend_theory} and {\tt assume_ax}}}
Theories organize the syntax, declarations and axioms of a mathematical
development.  They are built, starting from the Pure theory, by extending
and merging existing theories.  They have the \ML\ type \ttindex{theory}.
Theory operations signal errors by raising exception \ttindex{THEORY},
returning a message and a list of theories.

Signatures, which contain information about sorts, types, constants and
syntax, have the \ML\ type~\ttindexbold{Sign.sg}.  For identification,
each signature carries a unique list of {\bf 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{DefiningTheories}

Theories can be defined either using concrete syntax or by calling certain
\ML{} functions (see \S\ref{BuildingATheory}).  Appendix~\ref{app:TheorySyntax}
presents the concrete syntax for theories.  A theory definition consists of
several different parts: 
\begin{description} 
\item[{\it theoryDef}] A theory has a name $id$ and is an extension of the
  union of theories with name {\it name}, the {\bf parent
    theories}\indexbold{theories!parent}, with new classes, types, constants,
  syntax and axioms.  The basic theory, which contains only the meta-logic,
  is called {\tt Pure}.

  Normally each {\it name\/} is an identifier, the precise name of the parent
  theory. Strings can be used to document additional dependencies; see
  \S\ref{LoadingTheories} for details.
\item[$classes$] {\tt$id$ < $id@1$ \dots\ $id@n$} declares $id$ as a subclass
  of existing classes $id@1\dots id@n$.  This rules out cyclic class
  structures.  Isabelle automatically computes the transitive closure of
  subclass hierarchies.  Hence 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.  Unconstrained type variables in an input string are
  automatically constrained by $sort$; this does not apply to type variables
  created internally during type inference.  If omitted, the default sort is
  the union of the default sorts of the parent theories.
\item[$sort$] is a finite set of classes; a single class $id$ abbreviates the
  singleton set {\tt\{}$id${\tt\}}.
\item[$type$] is either the declaration of a new type (constructor) or type
  synonym $name$. Only binary type constructors can have infix status and
  symbolic names, e.g.\ {\tt ('a,'b)"*"}. Type constructors of $n$ arguments
  are declared by $(\alpha@1,\dots,\alpha@n)name$.  A {\bf type
    synonym}\indexbold{types!synonyms} is simply an abbreviation
  $(\alpha@1,\dots,\alpha@n)name = \mbox{\tt"}\tau\mbox{\tt"}$ and follows
  the same rules as in \ML, except that $name$ can be a string and $\tau$
  must be enclosed in quotation marks.
\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}).
\item[$arities$] Each $name$ must be an existing type constructor which is
  given the additional arity $arity$.
\item[$constDecl$] Each new constant $name$ is declared to be of type
  $string$.  For display purposes $mixfix$ annotations can be attached.
\item[$mixfix$] There are three forms of syntactic annotations:
  \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 minimal
    priority of each argument is given by a list of natural numbers, the
    priority of the whole construct by the following natural number;
    priorities are optional.

  \item Binary constants can be given infix status.

  \item A constant $f$ {\tt::} $(\tau@1\To\tau@2)\To\tau@3$ 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, that is parse 
  rules ({\tt =>}), print rules ({\tt <=}), or both ({\tt ==}).
\item[$rule$] A rule consists of a name $id$ and a formula $string$.  Rule
  names must be distinct.
\item[$ml$] This final part of a theory consists of \ML\ code, 
  typically for parse and print translations.
\end{description}
The $mixfix$, $trans$ and $ml$ sections are explained in more detail in 
the {\it Defining Logics} chapter of {\it Isabelle's Object Logics}.


\subsection{*Classes and arities}
\index{*classes!context conditions}\index{*arities!context conditions}

In order to guarantee principal types~\cite{nipkow-prehofer},
classes and arities must obey two conditions:
\begin{itemize}
\item There must be no two declarations $ty :: (\vec{r})c$ and $ty ::
  (\vec{s})c$ with $\vec{r} \neq \vec{s}$.  For example, the following is
  forbidden:
\begin{ttbox}
types 'a ty
arities ty :: ({\ttlbrace}logic{\ttrbrace}) logic
        ty :: ({\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$.  For example, the following is forbidden:
\begin{ttbox}
classes term < logic
types 'a ty
arities ty :: ({\ttlbrace}logic{\ttrbrace})logic
        ty :: ({\ttlbrace}{\ttrbrace})term
\end{ttbox}

\end{itemize}


\section{Loading a new theory}
\label{LoadingTheories}
\index{theories!loading}
\begin{ttbox} 
use_thy         : string -> unit
time_use_thy    : string -> unit
loadpath        : string list ref \hfill{\bf initially {\tt["."]}}
delete_tmpfiles : bool ref \hfill{\bf initially true}
\end{ttbox}

\begin{description}
\item[\ttindexbold{use_thy} $thyname$] 
  reads the theory $thyname$ and creates an \ML{} structure as described below.

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

\item[\ttindexbold{loadpath}] 
  contains a list of directories to search when locating the files that
  define a theory.  This list is only used if the theory name in {\tt
    use_thy} does not specify the path explicitly.

\item[\ttindexbold{delete_tmpfiles} \tt:= false;] 
suppresses the deletion of temporary files.
\end{description}
%
Each theory definition must reside in a separate file.  Let the file {\it
  tf}{\tt.thy} contain the definition of a theory called $TF$ with parent
theories $TB@1$ \dots $TB@n$.  Calling \ttindexbold{use_thy}~{\tt"}{\it
  TF\/}{\tt"} reads file {\it tf}{\tt.thy}, writes an intermediate \ML{}
file {\tt.}{\it tf}{\tt.thy.ML}, and reads the latter file.  Recursive {\tt
  use_thy} calls load those parent theories that have not been loaded
previously; the recursion may continue to any depth.  One {\tt use_thy}
call can read an entire logic if all theories are linked appropriately.

The result is an \ML\ structure~$TF$ containing a component {\tt thy} for
the new theory and components $r@1$ \dots $r@n$ for the rules.  The
structure also contains the definitions of the {\tt ML} section, if
present.  The file {\tt.}{\it tf}{\tt.thy.ML} is then deleted if
\ttindexbold{delete_tmpfiles} is set to {\tt true} and no errors occurred.

Finally the file {\it tf}{\tt.ML} is read, if it exists.  This file
normally contains proofs involving the new theory.  It is also possible to
provide only a {\tt.ML} file, with no {\tt.thy} file.  In this case the
{\tt.ML} file must declare an \ML\ structure having the theory's name.  If
both the {\tt.thy} file and a structure declaration in the {\tt.ML} file
exist, then the latter declaration is used.  See {\tt ZF/ex/llist.ML} for
an example.

\indexbold{theories!names of}\indexbold{files!names of}
\begin{warn}
  Case is significant.  The argument of \ttindex{use_thy} must be the exact
  theory name.  The corresponding filenames are derived by appending
  {\tt.thy} or {\tt.ML} to the theory's name {\it after conversion to lower
    case}. 
\end{warn}


\section{Reloading modified theories}
\indexbold{theories!reloading}\index{*update|(}
\begin{ttbox} 
update     : unit -> unit
unlink_thy : string -> unit
\end{ttbox}
Isabelle keeps track of all loaded theories and their files.  If
\ttindex{use_thy} finds that the theory to be loaded has been read before,
it determines whether to reload the theory as follows.  First it looks for
the theory's files in their previous location.  If it finds them, it
compares their modification times to the internal data and stops if they
are equal.  If the files have been moved, {\tt use_thy} searches for them
as it would for a new theory.  After {\tt use_thy} reloads a theory, it
marks the children as out-of-date.
\begin{warn}
  Changing a theory on disk often makes it necessary to reload all theories
  descended from it.  However, {\tt use_thy} reads only one theory, even if
  some of the parent theories are out of date.  In this case you should
  call {\tt update()}.
\end{warn}

\begin{description}
\item[\ttindexbold{update} ()] 
  reloads all modified theories and their descendants in the correct order.  

\item[\ttindexbold{unlink_thy} $thyname$]\indexbold{theories!removing}
  informs Isabelle that theory $thyname$ no longer exists.  If you delete the
  theory files for $thyname$ then you must execute {\tt unlink_thy};
  otherwise {\tt update} will complain about a missing file.
\end{description}


\subsection{Important note for Poly/ML users}\index{Poly/\ML}
The theory mechanism depends upon reference variables.  At the end of a
Poly/\ML{} session, the contents of references are lost unless they are
declared in the current database.  Assignments to references in the {\tt
  Pure} database are lost, including all information about loaded theories.

To avoid losing such information (assuming you have loaded some theories)
you must declare a new {\tt Readthy} structure in the child database:
\begin{ttbox}
structure Readthy = ReadthyFUN (structure ThySyn = ThySyn);
Readthy.loaded_thys := !loaded_thys;
open Readthy;
\end{ttbox}
This copies into the new reference \verb$loaded_thys$ the contents of the
original reference, which is the list of already loaded theories.


\subsection{*Pseudo theories}\indexbold{theories!pseudo}
Any automatic reloading facility requires complete knowledge of all
dependencies.  Sometimes theories depend on objects created in \ML{} files
with no associated {\tt.thy} file.  Unless such dependencies are documented,
{\tt update} fails to reload these \ML{} files and the system is left in a
state where some objects, e.g.\ theorems, still refer to old versions of
theories. This may lead to the error
\begin{ttbox}
Attempt to merge different versions of theory: \(T\)
\end{ttbox}
Therefore there is a way to link theories and {\em orphaned\/} \ML{} files ---
those without associated {\tt.thy} file.

Let us assume we have an orphaned \ML{} file named {\tt orphan.ML} and a theory
$B$ which depends on {\tt orphan.ML} (for example, {\tt b.ML} uses theorems
that are proved in {\tt orphan.ML}). Then {\tt b.thy} should mention this
dependence:
\begin{ttbox}
B = ... + "orphan" + ...
\end{ttbox}
Although {\tt orphan} is {\em not\/} used in building the base of theory $B$
(strings stand for \ML{} files rather than {\tt.thy} files and merely document
additional dependencies), {\tt orphan.ML} is loaded automatically when $B$ is
(re)built.

If {\tt orphan.ML} depends on theories $A@1\dots A@n$, this should be recorded
by creating a {\bf pseudo theory} in the file {\tt orphan.thy}:
\begin{ttbox}
orphan = A1 + \(...\) + An
\end{ttbox}
The resulting theory is a dummy, but it ensures that {\tt update} reloads
theory {\it orphan} whenever it reloads one of the $A@i$.

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

\index{*update|)}



\section{Basic operations on theories}
\subsection{Extracting an axiom from a theory}
\index{theories!extracting axioms|bold}\index{axioms}
\begin{ttbox} 
get_axiom: theory -> string -> thm
assume_ax: theory -> string -> thm
\end{ttbox}
\begin{description}
\item[\ttindexbold{get_axiom} $thy$ $name$] 
returns an axiom with the given $name$ from $thy$, raising exception
\ttindex{THEORY} if none exists.  Merging theories can cause several axioms
to have the same name; {\tt get_axiom} returns an arbitrary one.

\item[\ttindexbold{assume_ax} $thy$ $formula$] 
  reads the {\it formula} using the syntax of $thy$, following the same
  conventions as axioms in a theory definition.  You can thus pretend that
  {\it formula} is an axiom and use the resulting theorem like an axiom.
  Actually {\tt assume_ax} returns an assumption;  \ttindex{result}
  complains about additional assumptions, but \ttindex{uresult} does not.

For example, if {\it formula} is
\hbox{\tt a=b ==> b=a} then the resulting theorem might have the form
\hbox{\tt\frenchspacing ?a=?b ==> ?b=?a  [!!a b. a=b ==> b=a]}
\end{description}

\subsection{Building a theory}
\label{BuildingATheory}
\index{theories!constructing|bold}
\begin{ttbox} 
pure_thy: theory
merge_theories: theory * theory -> theory
extend_theory: theory -> string -> \(\cdots\) -> theory
\end{ttbox}
\begin{description}
\item[\ttindexbold{pure_thy}] contains just the types, constants, and syntax
  of the meta-logic.  There are no axioms: meta-level inferences are carried
  out by \ML\ functions.
\item[\ttindexbold{merge_theories} ($thy@1$, $thy@2$)] merges the two
  theories $thy@1$ and $thy@2$.  The resulting theory contains all types,
  constants and axioms of the constituent theories; its default sort is the
  union of the default sorts of the constituent theories.
\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
\begin{ttbox}
Attempt to merge different versions of theory: \(T\)
\end{ttbox}
\end{description}

%\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}
%
%If theories are defined as in \S\ref{DefiningTheories}, new syntax is added
%as mixfix annotations to constants.  Using {\tt extend_theory}, new syntax can
%be added via $sextopt$ which is either {\tt None}, or {\tt Some($sext$)}.  The
%latter case is not documented.


\subsection{Inspecting a theory}
\index{theories!inspecting|bold}
\begin{ttbox} 
print_theory  : theory -> unit
axioms_of     : theory -> (string*thm)list
parents_of    : theory -> theory list
sign_of       : theory -> Sign.sg
stamps_of_thy : theory -> string ref list
\end{ttbox}
These provide a simple means of viewing a theory's components.
Unfortunately, there is no direct connection between a theorem and its
theory.
\begin{description}
\item[\ttindexbold{print_theory} {\it thy}]  
prints the theory {\it thy\/} at the terminal as a set of identifiers.

\item[\ttindexbold{axioms_of} $thy$] 
returns the axioms of~$thy$ and its ancestors.

\item[\ttindexbold{parents_of} $thy$] 
returns the parents of~$thy$.  This list contains zero, one or two
elements, depending upon whether $thy$ is {\tt pure_thy}, 
\hbox{\tt extend_theory $thy$} or \hbox{\tt merge_theories ($thy@1$, $thy@2$)}.

\item[\ttindexbold{stamps_of_thy} $thy$]\index{signatures}
returns the stamps of the signature associated with~$thy$.

\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.
\end{description}


\section{Terms}
\index{terms|bold}
Terms belong to the \ML\ type \ttindexbold{term}, which is a concrete datatype
with six constructors: there are six kinds of term.
\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{description}
\item[\ttindexbold{Const}($a$, $T$)] 
  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$)] 
is the {\bf free variable} with name~$a$ and type~$T$.

\item[\ttindexbold{Var}($v$, $T$)] 
is the {\bf scheme variable} with indexname~$v$ and type~$T$.  An
\ttindexbold{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$] 
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~336]{paulson91}.

\item[\ttindexbold{Abs}($a$, $T$, $u$)] 
is the {\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[\tt $t$ \$ $u$] \index{$@{\tt\$}|bold}
is the {\bf application} of~$t$ to~$u$.  
\end{description}
Application is written as an infix operator to aid readability.
Here is an \ML\ pattern to recognize first-order formula of
the form~$A\imp B$, binding the subformulae to~$A$ and~$B$:
\begin{ttbox} 
Const("Trueprop",_) $ (Const("op -->",_) $ A $ B)
\end{ttbox}


\section{Terms and 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{description}
\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
  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$ choosen 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{description}

\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 declared in the signature and every constant in~$t$ is
declared as a constant of the same type in the signature.  It 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 \ttindexbold{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{printing!terms|bold}
\begin{ttbox} 
     string_of_cterm :           cterm -> string
Sign.string_of_term  : Sign.sg -> term -> string
\end{ttbox}
\begin{description}
\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{description}

\subsection{Making and inspecting certified terms}
\begin{ttbox} 
cterm_of   : Sign.sg -> term -> cterm
read_cterm : Sign.sg -> string * typ -> cterm
rep_cterm  : cterm -> \{T:typ, t:term, sign:Sign.sg, maxidx:int\}
\end{ttbox}
\begin{description}
\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{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.
\end{description}


\section{Types}\index{types|bold} 
Types belong to the \ML\ type \ttindexbold{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.  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{description}
\item[\ttindexbold{Type}($a$, $Ts$)] 
applies the {\bf type constructor} named~$a$ to the type operands~$Ts$.
Type constructors include~\ttindexbold{fun}, the binary function space
constructor, as well as nullary type constructors such
as~\ttindexbold{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$)] 
is the {\bf free type variable} with name~$a$ and sort~$s$.

\item[\ttindexbold{TVar}($v$, $s$)] 
is the {\bf scheme type variable} with indexname~$v$ and sort~$s$.  Scheme
type variables are essentially free type variables, but may be instantiated
during unification.
\end{description}


\section{Certified types}
\index{types!certified|bold}
Certified types, which are analogous to certified terms, have type 
\ttindexbold{ctyp}.

\subsection{Printing types}
\index{printing!types|bold}
\begin{ttbox} 
     string_of_ctyp :           ctyp -> string
Sign.string_of_typ  : Sign.sg -> typ -> string
\end{ttbox}
\begin{description}
\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{description}


\subsection{Making and inspecting certified types}
\begin{ttbox} 
ctyp_of  : Sign.sg -> typ -> ctyp
rep_ctyp : ctyp -> \{T: typ, sign: Sign.sg\}
\end{ttbox}
\begin{description}
\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.
\end{description}

\index{theories|)}