1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/doc-src/Ref/theories.tex Wed Nov 10 05:00:57 1993 +0100
1.3 @@ -0,0 +1,445 @@
1.4 +%% $Id$
1.5 +\chapter{Theories, Terms and Types} \label{theories}
1.6 +\index{theories|(}\index{signatures|bold}
1.7 +\index{reading!axioms|see{{\tt extend_theory} and {\tt assume_ax}}}
1.8 +Theories organize the syntax, declarations and axioms of a mathematical
1.9 +development. They are built, starting from the Pure theory, by extending
1.10 +and merging existing theories. They have the \ML{} type \ttindex{theory}.
1.11 +Theory operations signal errors by raising exception \ttindex{THEORY},
1.12 +returning a message and a list of theories.
1.13 +
1.14 +Signatures, which contain information about sorts, types, constants and
1.15 +syntax, have the \ML{} type~\ttindexbold{Sign.sg}. For identification,
1.16 +each signature carries a unique list of {\bf stamps}, which are~\ML{}
1.17 +references (to strings). The strings serve as human-readable names; the
1.18 +references serve as unique identifiers. Each primitive signature has a
1.19 +single stamp. When two signatures are merged, their lists of stamps are
1.20 +also merged. Every theory carries a unique signature.
1.21 +
1.22 +Terms and types are the underlying representation of logical syntax. Their
1.23 +\ML{} definitions are irrelevant to naive Isabelle users. Programmers who wish
1.24 +to extend Isabelle may need to know such details, say to code a tactic that
1.25 +looks for subgoals of a particular form. Terms and types may be
1.26 +`certified' to be well-formed with respect to a given signature.
1.27 +
1.28 +\section{Defining Theories}
1.29 +\label{DefiningTheories}
1.30 +
1.31 +Theories can be defined either using concrete syntax or by calling certain
1.32 +\ML-functions (see \S\ref{BuildingATheory}). Figure~\ref{TheorySyntax}
1.33 +presents the concrete syntax for theories. This grammar employs the
1.34 +following conventions:
1.35 +\begin{itemize}
1.36 +\item Identifiers such as $theoryDef$ denote nonterminal symbols.
1.37 +\item Text in {\tt typewriter font} denotes terminal symbols.
1.38 +\item \ldots{} indicates repetition of a phrase.
1.39 +\item A vertical bar~($|$) separates alternative phrases.
1.40 +\item Square [brackets] enclose optional phrases.
1.41 +\item $id$ stands for an Isabelle identifier.
1.42 +\item $string$ stands for an ML string, with its quotation marks.
1.43 +\item $k$ stands for a natural number.
1.44 +\item $text$ stands for arbitrary ML text.
1.45 +\end{itemize}
1.46 +
1.47 +\begin{figure}[hp]
1.48 +\begin{center}
1.49 +\begin{tabular}{rclc}
1.50 +$theoryDef$ &=& $id$ {\tt=} $id@1$ {\tt+} \dots {\tt+} $id@n$
1.51 + [{\tt+} $extension$]\\\\
1.52 +$extension$ &=& [$classes$] [$default$] [$types$] [$arities$] [$consts$]
1.53 + [$rules$] {\tt end} [$ml$]\\\\
1.54 +$classes$ &=& \ttindex{classes} $class$ \dots $class$ \\\\
1.55 +$class$ &=& $id$ [{\tt<} $id@1${\tt,} \dots{\tt,} $id@n$] \\\\
1.56 +$default$ &=& \ttindex{default} $sort$ \\\\
1.57 +$sort$ &=& $id$ ~~$|$~~ {\tt\{} $id@1${\tt,} \dots{\tt,} $id@n$ {\tt\}} \\\\
1.58 +$name$ &=& $id$ ~~$|$~~ $string$ \\\\
1.59 +$types$ &=& \ttindex{types} $typeDecl$ \dots $typeDecl$ \\\\
1.60 +$typeDecl$ &=& $name${\tt,} \dots{\tt,} $name$ $k$
1.61 + [{\tt(} $infix$ {\tt)}] \\\\
1.62 +$infix$ &=& \ttindex{infixl} $k$ ~~$|$~~ \ttindex{infixr} $k$ \\\\
1.63 +$arities$ &=& \ttindex{arities} $arityDecl$ \dots $arityDecl$ \\\\
1.64 +$arityDecl$ &=& $name${\tt,} \dots{\tt,} $name$ {\tt::} $arity$ \\\\
1.65 +$arity$ &=& [{\tt(} $sort${\tt,} \dots{\tt,} $sort$ {\tt)}] $id$ \\\\
1.66 +$consts$ &=& \ttindex{consts} $constDecl$ \dots $constDecl$ \\\\
1.67 +$constDecl$ &=& $name@1${\tt,} \dots{\tt,} $name@n$ {\tt::} $string$
1.68 + [{\tt(} $mixfix$ {\tt)}] \\\\
1.69 +$mixfix$ &=& $string$
1.70 + [ [\quad{\tt[} $k@1${\tt,} \dots{\tt,} $k@n$ {\tt]}\quad] $k$]\\
1.71 + &$|$& $infix$ \\
1.72 + &$|$& \ttindex{binder} $string$ $k$\\\\
1.73 +$rules$ &=& \ttindex{rules} $rule$ \dots $rule$ \\\\
1.74 +$rule$ &=& $id$ $string$ \\\\
1.75 +$ml$ &=& \ttindex{ML} $text$
1.76 +\end{tabular}
1.77 +\end{center}
1.78 +\caption{Theory Syntax}
1.79 +\label{TheorySyntax}
1.80 +\end{figure}
1.81 +
1.82 +The different parts of a theory definition are interpreted as follows:
1.83 +\begin{description}
1.84 +\item[$theoryDef$] A theory has a name $id$ and is an extension of the union
1.85 + of existing theories $id@1$ \dots $id@n$ with new classes, types,
1.86 + constants, syntax and axioms. The basic theory, which contains only the
1.87 + meta-logic, is called {\tt Pure}.
1.88 +\item[$class$] The new class $id$ is declared as a subclass of existing
1.89 + classes $id@1$ \dots $id@n$. This rules out cyclic class structures.
1.90 + Isabelle automatically computes the transitive closure of subclass
1.91 + hierarchies. Hence it is not necessary to declare $c@1 < c@3$ in addition
1.92 + to $c@1 < c@2$ and $c@2 < c@3$.
1.93 +\item[$default$] introduces $sort$ as the new default sort for type
1.94 + variables. Unconstrained type variables in an input string are
1.95 + automatically constrained by $sort$; this does not apply to type variables
1.96 + created internally during type inference. If omitted,
1.97 + the default sort is the same as in the parent theory.
1.98 +\item[$sort$] is a finite set $id@1$ \dots $id@n$ of classes; a single class
1.99 + $id$ abbreviates the singleton set {\tt\{}$id${\tt\}}.
1.100 +\item[$name$] is either an alphanumeric identifier or an arbitrary string.
1.101 +\item[$typeDecl$] Each $name$ is declared as a new type constructor with
1.102 + $k$ arguments. Only binary type constructors can have infix status and
1.103 + symbolic names ($string$).
1.104 +\item[$infix$] declares a type or constant to be an infix operator of
1.105 + precedence $k$ associating to the left ({\tt infixl}) or right ({\tt
1.106 + infixr}).
1.107 +\item[$arityDecl$] Each existing type constructor $name@1$ \dots $name@n$
1.108 + is given the additional arity $arity$.
1.109 +\item[$constDecl$] The new constants $name@1$ \dots $name@n$ are declared to
1.110 + be of type $string$. For display purposes they can be annotated with
1.111 + $mixfix$ declarations.
1.112 +\item[$mixfix$] $string$ is a mixfix template of the form {\tt"}\dots{\tt\_}
1.113 + \dots{\tt\_} \dots{\tt"} where the $i$-th underscore indicates the position
1.114 + where the $i$-th argument should go, $k@i$ is the minimum precedence of
1.115 + the $i$-th argument, and $k$ the precedence of the construct. The list
1.116 + \hbox{\tt[$k@1$, \dots, $k@n$]} is optional.
1.117 +
1.118 + Binary constants can be given infix status.
1.119 +
1.120 + A constant $f$ {\tt::} $(\tau@1\To\tau@2)\To\tau@3$ can be given {\em
1.121 + binder} status: {\tt binder} $Q$ $p$ causes $Q\,x.F(x)$ to be treated
1.122 + like $f(F)$; $p$ is the precedence of the construct.
1.123 +\item[$rule$] A rule consists of a name $id$ and a formula $string$. Rule
1.124 + names must be distinct.
1.125 +\item[$ml$] This final part of a theory consists of ML code,
1.126 + typically for parse and print translations.
1.127 +\end{description}
1.128 +The $mixfix$ and $ml$ sections are explained in more detail in the {\it
1.129 +Defining Logics} chapter of the {\it Logics} manual.
1.130 +
1.131 +\begin{ttbox}
1.132 +use_thy: string -> unit
1.133 +\end{ttbox}
1.134 +Each theory definition must reside in a separate file. Let the file {\it
1.135 + tf}{\tt.thy} contain the definition of a theory called $TF$ with rules named
1.136 +$r@1$ \dots $r@n$. Calling \ttindexbold{use_thy}~{\tt"}{\it tf\/}{\tt"} reads
1.137 +file {\it tf}{\tt.thy}, writes an intermediate {\ML}-file {\tt.}{\it
1.138 + tf}{\tt.thy.ML}, and reads the latter file. This declares an {\ML}
1.139 +structure~$TF$ containing a component {\tt thy} for the new theory
1.140 +and components $r@1$ \dots $r@n$ for the rules; it also contains the
1.141 +definitions of the {\tt ML} section if any. Then {\tt use_thy}
1.142 +reads the file {\it tf}{\tt.ML}, if it exists; this file normally contains
1.143 +proofs involving the new theory.
1.144 +
1.145 +
1.146 +\section{Basic operations on theories}
1.147 +\subsection{Extracting an axiom from a theory}
1.148 +\index{theories!extracting axioms|bold}\index{axioms}
1.149 +\begin{ttbox}
1.150 +get_axiom: theory -> string -> thm
1.151 +assume_ax: theory -> string -> thm
1.152 +\end{ttbox}
1.153 +\begin{description}
1.154 +\item[\ttindexbold{get_axiom} $thy$ $name$]
1.155 +returns an axiom with the given $name$ from $thy$, raising exception
1.156 +\ttindex{THEORY} if none exists. Merging theories can cause several axioms
1.157 +to have the same name; {\tt get_axiom} returns an arbitrary one.
1.158 +
1.159 +\item[\ttindexbold{assume_ax} $thy$ $formula$]
1.160 +reads the {\it formula} using the syntax of $thy$, following the same
1.161 +conventions as axioms in a theory definition. You can thus pretend that
1.162 +{\it formula} is an axiom; in fact, {\tt assume_ax} returns an assumption.
1.163 +You can use the resulting theorem like an axiom. Note that
1.164 +\ttindex{result} complains about additional assumptions, but
1.165 +\ttindex{uresult} does not.
1.166 +
1.167 +For example, if {\it formula} is
1.168 +\hbox{\tt a=b ==> b=a} then the resulting theorem might have the form
1.169 +\hbox{\tt\frenchspacing ?a=?b ==> ?b=?a [!!a b. a=b ==> b=a]}
1.170 +\end{description}
1.171 +
1.172 +\subsection{Building a theory}
1.173 +\label{BuildingATheory}
1.174 +\index{theories!constructing|bold}
1.175 +\begin{ttbox}
1.176 +pure_thy: theory
1.177 +merge_theories: theory * theory -> theory
1.178 +extend_theory: theory -> string
1.179 + -> (class * class list) list
1.180 + * sort
1.181 + * (string list * int)list
1.182 + * (string list * (sort list * class))list
1.183 + * (string list * string)list * sext option
1.184 + -> (string*string)list -> theory
1.185 +\end{ttbox}
1.186 +Type \ttindex{class} is a synonym for {\tt string}; type \ttindex{sort} is
1.187 +a synonym for \hbox{\tt class list}.
1.188 +\begin{description}
1.189 +\item[\ttindexbold{pure_thy}] contains just the types, constants, and syntax
1.190 + of the meta-logic. There are no axioms: meta-level inferences are carried
1.191 + out by \ML\ functions.
1.192 +\item[\ttindexbold{merge_theories} ($thy@1$, $thy@2$)] merges the two
1.193 + theories $thy@1$ and $thy@2$. The resulting theory contains all types,
1.194 + constants and axioms of the constituent theories; its default sort is the
1.195 + union of the default sorts of the constituent theories.
1.196 +\item [\ttindexbold{extend_theory} $thy$ {\tt"}$T${\tt"}
1.197 + ($classes$, $default$, $types$, $arities$, $consts$, $sextopt$) $rules$]
1.198 +\hfill\break %%% include if line is just too short
1.199 +is the \ML-equivalent of the following theory definition:
1.200 +\begin{ttbox}
1.201 +\(T\) = \(thy\) +
1.202 +classes \(c\) < \(c@1\),\(\dots\),\(c@m\)
1.203 + \dots
1.204 +default {\(d@1,\dots,d@r\)}
1.205 +types \(tycon@1\),\dots,\(tycon@i\) \(n\)
1.206 + \dots
1.207 +arities \(tycon@1'\),\dots,\(tycon@j'\) :: (\(s@1\),\dots,\(s@n\))\(c\)
1.208 + \dots
1.209 +consts \(b@1\),\dots,\(b@k\) :: \(\tau\)
1.210 + \dots
1.211 +rules \(name\) \(rule\)
1.212 + \dots
1.213 +end
1.214 +\end{ttbox}
1.215 +where
1.216 +\begin{tabular}[t]{l@{~=~}l}
1.217 +$classes$ & \tt[("$c$",["$c@1$",\dots,"$c@m$"]),\dots] \\
1.218 +$default$ & \tt["$d@1$",\dots,"$d@r$"]\\
1.219 +$types$ & \tt[([$tycon@1$,\dots,$tycon@i$], $n$),\dots] \\
1.220 +$arities$ & \tt[([$tycon'@1$,\dots,$tycon'@j$], ([$s@1$,\dots,$s@n$],$c$)),\dots]
1.221 +\\
1.222 +$consts$ & \tt[([$b@1$,\dots,$b@k$],$\tau$),\dots] \\
1.223 +$rules$ & \tt[("$name$",$rule$),\dots]
1.224 +\end{tabular}
1.225 +
1.226 +If theories are defined as in \S\ref{DefiningTheories}, new syntax is added
1.227 +as mixfix annotations to constants. Using {\tt extend_theory}, new syntax can
1.228 +be added via $sextopt$ which is either {\tt None}, or {\tt Some($sext$)}. The
1.229 +latter case is not documented.
1.230 +
1.231 +$T$ identifies the theory internally. When a theory is redeclared, say to
1.232 +change an incorrect axiom, bindings to the old axiom may persist. Isabelle
1.233 +ensures that the old and new theories are not involved in the same proof.
1.234 +Attempting to combine different theories having the same name $T$ yields the
1.235 +fatal error
1.236 +\begin{center} \tt
1.237 +Attempt to merge different versions of theory: $T$
1.238 +\end{center}
1.239 +\end{description}
1.240 +
1.241 +
1.242 +\subsection{Inspecting a theory}
1.243 +\index{theories!inspecting|bold}
1.244 +\begin{ttbox}
1.245 +print_theory : theory -> unit
1.246 +axioms_of : theory -> (string*thm)list
1.247 +parents_of : theory -> theory list
1.248 +sign_of : theory -> Sign.sg
1.249 +stamps_of_thy : theory -> string ref list
1.250 +\end{ttbox}
1.251 +These provide a simple means of viewing a theory's components.
1.252 +Unfortunately, there is no direct connection between a theorem and its
1.253 +theory.
1.254 +\begin{description}
1.255 +\item[\ttindexbold{print_theory} {\it thy}]
1.256 +prints the theory {\it thy\/} at the terminal as a set of identifiers.
1.257 +
1.258 +\item[\ttindexbold{axioms_of} $thy$]
1.259 +returns the axioms of~$thy$ and its ancestors.
1.260 +
1.261 +\item[\ttindexbold{parents_of} $thy$]
1.262 +returns the parents of~$thy$. This list contains zero, one or two
1.263 +elements, depending upon whether $thy$ is {\tt pure_thy},
1.264 +\hbox{\tt extend_theory $thy$} or \hbox{\tt merge_theories ($thy@1$, $thy@2$)}.
1.265 +
1.266 +\item[\ttindexbold{stamps_of_thy} $thy$]\index{signatures}
1.267 +returns the stamps of the signature associated with~$thy$.
1.268 +
1.269 +\item[\ttindexbold{sign_of} $thy$]
1.270 +returns the signature associated with~$thy$. It is useful with functions
1.271 +like {\tt read_instantiate_sg}, which take a signature as an argument.
1.272 +\end{description}
1.273 +
1.274 +
1.275 +\section{Terms}
1.276 +\index{terms|bold}
1.277 +Terms belong to the \ML{} type \ttindexbold{term}, which is a concrete datatype
1.278 +with six constructors: there are six kinds of term.
1.279 +\begin{ttbox}
1.280 +type indexname = string * int;
1.281 +infix 9 $;
1.282 +datatype term = Const of string * typ
1.283 + | Free of string * typ
1.284 + | Var of indexname * typ
1.285 + | Bound of int
1.286 + | Abs of string * typ * term
1.287 + | op $ of term * term;
1.288 +\end{ttbox}
1.289 +\begin{description}
1.290 +\item[\ttindexbold{Const}($a$, $T$)]
1.291 +is the {\bf constant} with name~$a$ and type~$T$. Constants include
1.292 +connectives like $\land$ and $\forall$ (logical constants), as well as
1.293 +constants like~0 and~$Suc$. Other constants may be required to define the
1.294 +concrete syntax of a logic.
1.295 +
1.296 +\item[\ttindexbold{Free}($a$, $T$)]
1.297 +is the {\bf free variable} with name~$a$ and type~$T$.
1.298 +
1.299 +\item[\ttindexbold{Var}($v$, $T$)]
1.300 +is the {\bf scheme variable} with indexname~$v$ and type~$T$. An
1.301 +\ttindexbold{indexname} is a string paired with a non-negative index, or
1.302 +subscript; a term's scheme variables can be systematically renamed by
1.303 +incrementing their subscripts. Scheme variables are essentially free
1.304 +variables, but may be instantiated during unification.
1.305 +
1.306 +\item[\ttindexbold{Bound} $i$]
1.307 +is the {\bf bound variable} with de Bruijn index~$i$, which counts the
1.308 +number of lambdas, starting from zero, between a variable's occurrence and
1.309 +its binding. The representation prevents capture of variables. For more
1.310 +information see de Bruijn \cite{debruijn72} or
1.311 +Paulson~\cite[page~336]{paulson91}.
1.312 +
1.313 +\item[\ttindexbold{Abs}($a$, $T$, $u$)]
1.314 +is the {\bf abstraction} with body~$u$, and whose bound variable has
1.315 +name~$a$ and type~$T$. The name is used only for parsing and printing; it
1.316 +has no logical significance.
1.317 +
1.318 +\item[\tt $t$ \$ $u$] \index{$@{\tt\$}|bold}
1.319 +is the {\bf application} of~$t$ to~$u$.
1.320 +\end{description}
1.321 +Application is written as an infix operator in order to aid readability.
1.322 +For example, here is an \ML{} pattern to recognize first-order formula of
1.323 +the form~$A\imp B$, binding the subformulae to~$A$ and~$B$:
1.324 +\begin{ttbox}
1.325 +Const("Trueprop",_) $ (Const("op -->",_) $ A $ B)
1.326 +\end{ttbox}
1.327 +
1.328 +
1.329 +\section{Certified terms}
1.330 +\index{terms!certified|bold}\index{signatures}
1.331 +A term $t$ can be {\bf certified} under a signature to ensure that every
1.332 +type in~$t$ is declared in the signature and every constant in~$t$ is
1.333 +declared as a constant of the same type in the signature. It must be
1.334 +well-typed and must not have any `loose' bound variable
1.335 +references.\footnote{This concerns the internal representation of variable
1.336 +binding using de Bruijn indexes.} Meta-rules such as {\tt forall_elim} take
1.337 +certified terms as arguments.
1.338 +
1.339 +Certified terms belong to the abstract type \ttindexbold{Sign.cterm}.
1.340 +Elements of the type can only be created through the certification process.
1.341 +In case of error, Isabelle raises exception~\ttindex{TERM}\@.
1.342 +
1.343 +\subsection{Printing terms}
1.344 +\index{printing!terms|bold}
1.345 +\begin{ttbox}
1.346 +Sign.string_of_cterm : Sign.cterm -> string
1.347 +Sign.string_of_term : Sign.sg -> term -> string
1.348 +\end{ttbox}
1.349 +\begin{description}
1.350 +\item[\ttindexbold{Sign.string_of_cterm} $ct$]
1.351 +displays $ct$ as a string.
1.352 +
1.353 +\item[\ttindexbold{Sign.string_of_term} $sign$ $t$]
1.354 +displays $t$ as a string, using the syntax of~$sign$.
1.355 +\end{description}
1.356 +
1.357 +\subsection{Making and inspecting certified terms}
1.358 +\begin{ttbox}
1.359 +Sign.cterm_of : Sign.sg -> term -> Sign.cterm
1.360 +Sign.read_cterm : Sign.sg -> string * typ -> Sign.cterm
1.361 +Sign.rep_cterm : Sign.cterm -> \{T:typ, t:term,
1.362 + sign: Sign.sg, maxidx:int\}
1.363 +\end{ttbox}
1.364 +\begin{description}
1.365 +\item[\ttindexbold{Sign.cterm_of} $sign$ $t$] \index{signatures}
1.366 +certifies $t$ with respect to signature~$sign$.
1.367 +
1.368 +\item[\ttindexbold{Sign.read_cterm} $sign$ ($s$, $T$)]
1.369 +reads the string~$s$ using the syntax of~$sign$, creating a certified term.
1.370 +The term is checked to have type~$T$; this type also tells the parser what
1.371 +kind of phrase to parse.
1.372 +
1.373 +\item[\ttindexbold{Sign.rep_cterm} $ct$]
1.374 +decomposes $ct$ as a record containing its type, the term itself, its
1.375 +signature, and the maximum subscript of its unknowns. The type and maximum
1.376 +subscript are computed during certification.
1.377 +\end{description}
1.378 +
1.379 +
1.380 +\section{Types}
1.381 +\index{types|bold}
1.382 +Types belong to the \ML{} type \ttindexbold{typ}, which is a concrete
1.383 +datatype with three constructors. Types are classified by sorts, which are
1.384 +lists of classes. A class is represented by a string.
1.385 +\begin{ttbox}
1.386 +type class = string;
1.387 +type sort = class list;
1.388 +
1.389 +datatype typ = Type of string * typ list
1.390 + | TFree of string * sort
1.391 + | TVar of indexname * sort;
1.392 +
1.393 +infixr 5 -->;
1.394 +fun S --> T = Type("fun",[S,T]);
1.395 +\end{ttbox}
1.396 +\begin{description}
1.397 +\item[\ttindexbold{Type}($a$, $Ts$)]
1.398 +applies the {\bf type constructor} named~$a$ to the type operands~$Ts$.
1.399 +Type constructors include~\ttindexbold{fun}, the binary function space
1.400 +constructor, as well as nullary type constructors such
1.401 +as~\ttindexbold{prop}. Other type constructors may be introduced. In
1.402 +expressions, but not in patterns, \hbox{\tt$S$-->$T$} is a convenient
1.403 +shorthand for function types.
1.404 +
1.405 +\item[\ttindexbold{TFree}($a$, $s$)]
1.406 +is the {\bf free type variable} with name~$a$ and sort~$s$.
1.407 +
1.408 +\item[\ttindexbold{TVar}($v$, $s$)]
1.409 +is the {\bf scheme type variable} with indexname~$v$ and sort~$s$. Scheme
1.410 +type variables are essentially free type variables, but may be instantiated
1.411 +during unification.
1.412 +\end{description}
1.413 +
1.414 +
1.415 +\section{Certified types}
1.416 +\index{types!certified|bold}
1.417 +Certified types, which are analogous to certified terms, have type
1.418 +\ttindexbold{Sign.ctyp}.
1.419 +
1.420 +\subsection{Printing types}
1.421 +\index{printing!types|bold}
1.422 +\begin{ttbox}
1.423 +Sign.string_of_ctyp : Sign.ctyp -> string
1.424 +Sign.string_of_typ : Sign.sg -> typ -> string
1.425 +\end{ttbox}
1.426 +\begin{description}
1.427 +\item[\ttindexbold{Sign.string_of_ctyp} $cT$]
1.428 +displays $cT$ as a string.
1.429 +
1.430 +\item[\ttindexbold{Sign.string_of_typ} $sign$ $T$]
1.431 +displays $T$ as a string, using the syntax of~$sign$.
1.432 +\end{description}
1.433 +
1.434 +
1.435 +\subsection{Making and inspecting certified types}
1.436 +\begin{ttbox}
1.437 +Sign.ctyp_of : Sign.sg -> typ -> Sign.ctyp
1.438 +Sign.rep_ctyp : Sign.ctyp -> \{T: typ, sign: Sign.sg\}
1.439 +\end{ttbox}
1.440 +\begin{description}
1.441 +\item[\ttindexbold{Sign.ctyp_of} $sign$ $T$] \index{signatures}
1.442 +certifies $T$ with respect to signature~$sign$.
1.443 +
1.444 +\item[\ttindexbold{Sign.rep_ctyp} $cT$]
1.445 +decomposes $cT$ as a record containing the type itself and its signature.
1.446 +\end{description}
1.447 +
1.448 +\index{theories|)}