104

1 
%% $Id$


2 
\chapter{Theories, Terms and Types} \label{theories}


3 
\index{theories(}\index{signaturesbold}


4 
\index{reading!axiomssee{{\tt extend_theory} and {\tt assume_ax}}}


5 
Theories organize the syntax, declarations and axioms of a mathematical


6 
development. They are built, starting from the Pure theory, by extending


7 
and merging existing theories. They have the \ML{} type \ttindex{theory}.


8 
Theory operations signal errors by raising exception \ttindex{THEORY},


9 
returning a message and a list of theories.


10 


11 
Signatures, which contain information about sorts, types, constants and


12 
syntax, have the \ML{} type~\ttindexbold{Sign.sg}. For identification,


13 
each signature carries a unique list of {\bf stamps}, which are~\ML{}


14 
references (to strings). The strings serve as humanreadable names; the


15 
references serve as unique identifiers. Each primitive signature has a


16 
single stamp. When two signatures are merged, their lists of stamps are


17 
also merged. Every theory carries a unique signature.


18 


19 
Terms and types are the underlying representation of logical syntax. Their


20 
\ML{} definitions are irrelevant to naive Isabelle users. Programmers who wish


21 
to extend Isabelle may need to know such details, say to code a tactic that


22 
looks for subgoals of a particular form. Terms and types may be


23 
`certified' to be wellformed with respect to a given signature.


24 


25 
\section{Defining Theories}


26 
\label{DefiningTheories}


27 


28 
Theories can be defined either using concrete syntax or by calling certain


29 
\MLfunctions (see \S\ref{BuildingATheory}). Figure~\ref{TheorySyntax}


30 
presents the concrete syntax for theories. This grammar employs the


31 
following conventions:


32 
\begin{itemize}


33 
\item Identifiers such as $theoryDef$ denote nonterminal symbols.


34 
\item Text in {\tt typewriter font} denotes terminal symbols.


35 
\item \ldots{} indicates repetition of a phrase.


36 
\item A vertical bar~($$) separates alternative phrases.


37 
\item Square [brackets] enclose optional phrases.


38 
\item $id$ stands for an Isabelle identifier.


39 
\item $string$ stands for an ML string, with its quotation marks.


40 
\item $k$ stands for a natural number.


41 
\item $text$ stands for arbitrary ML text.


42 
\end{itemize}


43 


44 
\begin{figure}[hp]


45 
\begin{center}


46 
\begin{tabular}{rclc}


47 
$theoryDef$ &=& $id$ {\tt=} $id@1$ {\tt+} \dots {\tt+} $id@n$


48 
[{\tt+} $extension$]\\\\


49 
$extension$ &=& [$classes$] [$default$] [$types$] [$arities$] [$consts$]


50 
[$rules$] {\tt end} [$ml$]\\\\


51 
$classes$ &=& \ttindex{classes} $class$ \dots $class$ \\\\


52 
$class$ &=& $id$ [{\tt<} $id@1${\tt,} \dots{\tt,} $id@n$] \\\\


53 
$default$ &=& \ttindex{default} $sort$ \\\\


54 
$sort$ &=& $id$ ~~$$~~ {\tt\{} $id@1${\tt,} \dots{\tt,} $id@n$ {\tt\}} \\\\


55 
$name$ &=& $id$ ~~$$~~ $string$ \\\\


56 
$types$ &=& \ttindex{types} $typeDecl$ \dots $typeDecl$ \\\\


57 
$typeDecl$ &=& $name${\tt,} \dots{\tt,} $name$ $k$


58 
[{\tt(} $infix$ {\tt)}] \\\\


59 
$infix$ &=& \ttindex{infixl} $k$ ~~$$~~ \ttindex{infixr} $k$ \\\\


60 
$arities$ &=& \ttindex{arities} $arityDecl$ \dots $arityDecl$ \\\\


61 
$arityDecl$ &=& $name${\tt,} \dots{\tt,} $name$ {\tt::} $arity$ \\\\


62 
$arity$ &=& [{\tt(} $sort${\tt,} \dots{\tt,} $sort$ {\tt)}] $id$ \\\\


63 
$consts$ &=& \ttindex{consts} $constDecl$ \dots $constDecl$ \\\\


64 
$constDecl$ &=& $name@1${\tt,} \dots{\tt,} $name@n$ {\tt::} $string$


65 
[{\tt(} $mixfix$ {\tt)}] \\\\


66 
$mixfix$ &=& $string$


67 
[ [\quad{\tt[} $k@1${\tt,} \dots{\tt,} $k@n$ {\tt]}\quad] $k$]\\


68 
&$$& $infix$ \\


69 
&$$& \ttindex{binder} $string$ $k$\\\\


70 
$rules$ &=& \ttindex{rules} $rule$ \dots $rule$ \\\\


71 
$rule$ &=& $id$ $string$ \\\\


72 
$ml$ &=& \ttindex{ML} $text$


73 
\end{tabular}


74 
\end{center}


75 
\caption{Theory Syntax}


76 
\label{TheorySyntax}


77 
\end{figure}


78 


79 
The different parts of a theory definition are interpreted as follows:


80 
\begin{description}


81 
\item[$theoryDef$] A theory has a name $id$ and is an extension of the union


82 
of existing theories $id@1$ \dots $id@n$ with new classes, types,


83 
constants, syntax and axioms. The basic theory, which contains only the


84 
metalogic, is called {\tt Pure}.


85 
\item[$class$] The new class $id$ is declared as a subclass of existing


86 
classes $id@1$ \dots $id@n$. This rules out cyclic class structures.


87 
Isabelle automatically computes the transitive closure of subclass


88 
hierarchies. Hence it is not necessary to declare $c@1 < c@3$ in addition


89 
to $c@1 < c@2$ and $c@2 < c@3$.


90 
\item[$default$] introduces $sort$ as the new default sort for type


91 
variables. Unconstrained type variables in an input string are


92 
automatically constrained by $sort$; this does not apply to type variables


93 
created internally during type inference. If omitted,


94 
the default sort is the same as in the parent theory.


95 
\item[$sort$] is a finite set $id@1$ \dots $id@n$ of classes; a single class


96 
$id$ abbreviates the singleton set {\tt\{}$id${\tt\}}.


97 
\item[$name$] is either an alphanumeric identifier or an arbitrary string.


98 
\item[$typeDecl$] Each $name$ is declared as a new type constructor with


99 
$k$ arguments. Only binary type constructors can have infix status and


100 
symbolic names ($string$).


101 
\item[$infix$] declares a type or constant to be an infix operator of


102 
precedence $k$ associating to the left ({\tt infixl}) or right ({\tt


103 
infixr}).


104 
\item[$arityDecl$] Each existing type constructor $name@1$ \dots $name@n$


105 
is given the additional arity $arity$.


106 
\item[$constDecl$] The new constants $name@1$ \dots $name@n$ are declared to


107 
be of type $string$. For display purposes they can be annotated with


108 
$mixfix$ declarations.


109 
\item[$mixfix$] $string$ is a mixfix template of the form {\tt"}\dots{\tt\_}


110 
\dots{\tt\_} \dots{\tt"} where the $i$th underscore indicates the position


111 
where the $i$th argument should go, $k@i$ is the minimum precedence of


112 
the $i$th argument, and $k$ the precedence of the construct. The list


113 
\hbox{\tt[$k@1$, \dots, $k@n$]} is optional.


114 


115 
Binary constants can be given infix status.


116 


117 
A constant $f$ {\tt::} $(\tau@1\To\tau@2)\To\tau@3$ can be given {\em


118 
binder} status: {\tt binder} $Q$ $p$ causes $Q\,x.F(x)$ to be treated


119 
like $f(F)$; $p$ is the precedence of the construct.


120 
\item[$rule$] A rule consists of a name $id$ and a formula $string$. Rule


121 
names must be distinct.


122 
\item[$ml$] This final part of a theory consists of ML code,


123 
typically for parse and print translations.


124 
\end{description}


125 
The $mixfix$ and $ml$ sections are explained in more detail in the {\it


126 
Defining Logics} chapter of the {\it Logics} manual.


127 


128 
\begin{ttbox}


129 
use_thy: string > unit


130 
\end{ttbox}


131 
Each theory definition must reside in a separate file. Let the file {\it


132 
tf}{\tt.thy} contain the definition of a theory called $TF$ with rules named


133 
$r@1$ \dots $r@n$. Calling \ttindexbold{use_thy}~{\tt"}{\it tf\/}{\tt"} reads


134 
file {\it tf}{\tt.thy}, writes an intermediate {\ML}file {\tt.}{\it


135 
tf}{\tt.thy.ML}, and reads the latter file. This declares an {\ML}


136 
structure~$TF$ containing a component {\tt thy} for the new theory


137 
and components $r@1$ \dots $r@n$ for the rules; it also contains the


138 
definitions of the {\tt ML} section if any. Then {\tt use_thy}


139 
reads the file {\it tf}{\tt.ML}, if it exists; this file normally contains


140 
proofs involving the new theory.


141 


142 


143 
\section{Basic operations on theories}


144 
\subsection{Extracting an axiom from a theory}


145 
\index{theories!extracting axiomsbold}\index{axioms}


146 
\begin{ttbox}


147 
get_axiom: theory > string > thm


148 
assume_ax: theory > string > thm


149 
\end{ttbox}


150 
\begin{description}


151 
\item[\ttindexbold{get_axiom} $thy$ $name$]


152 
returns an axiom with the given $name$ from $thy$, raising exception


153 
\ttindex{THEORY} if none exists. Merging theories can cause several axioms


154 
to have the same name; {\tt get_axiom} returns an arbitrary one.


155 


156 
\item[\ttindexbold{assume_ax} $thy$ $formula$]


157 
reads the {\it formula} using the syntax of $thy$, following the same


158 
conventions as axioms in a theory definition. You can thus pretend that


159 
{\it formula} is an axiom; in fact, {\tt assume_ax} returns an assumption.


160 
You can use the resulting theorem like an axiom. Note that


161 
\ttindex{result} complains about additional assumptions, but


162 
\ttindex{uresult} does not.


163 


164 
For example, if {\it formula} is


165 
\hbox{\tt a=b ==> b=a} then the resulting theorem might have the form


166 
\hbox{\tt\frenchspacing ?a=?b ==> ?b=?a [!!a b. a=b ==> b=a]}


167 
\end{description}


168 


169 
\subsection{Building a theory}


170 
\label{BuildingATheory}


171 
\index{theories!constructingbold}


172 
\begin{ttbox}


173 
pure_thy: theory


174 
merge_theories: theory * theory > theory


175 
extend_theory: theory > string


176 
> (class * class list) list


177 
* sort


178 
* (string list * int)list


179 
* (string list * (sort list * class))list


180 
* (string list * string)list * sext option


181 
> (string*string)list > theory


182 
\end{ttbox}


183 
Type \ttindex{class} is a synonym for {\tt string}; type \ttindex{sort} is


184 
a synonym for \hbox{\tt class list}.


185 
\begin{description}


186 
\item[\ttindexbold{pure_thy}] contains just the types, constants, and syntax


187 
of the metalogic. There are no axioms: metalevel inferences are carried


188 
out by \ML\ functions.


189 
\item[\ttindexbold{merge_theories} ($thy@1$, $thy@2$)] merges the two


190 
theories $thy@1$ and $thy@2$. The resulting theory contains all types,


191 
constants and axioms of the constituent theories; its default sort is the


192 
union of the default sorts of the constituent theories.


193 
\item [\ttindexbold{extend_theory} $thy$ {\tt"}$T${\tt"}


194 
($classes$, $default$, $types$, $arities$, $consts$, $sextopt$) $rules$]


195 
\hfill\break %%% include if line is just too short


196 
is the \MLequivalent of the following theory definition:


197 
\begin{ttbox}


198 
\(T\) = \(thy\) +


199 
classes \(c\) < \(c@1\),\(\dots\),\(c@m\)


200 
\dots


201 
default {\(d@1,\dots,d@r\)}


202 
types \(tycon@1\),\dots,\(tycon@i\) \(n\)


203 
\dots


204 
arities \(tycon@1'\),\dots,\(tycon@j'\) :: (\(s@1\),\dots,\(s@n\))\(c\)


205 
\dots


206 
consts \(b@1\),\dots,\(b@k\) :: \(\tau\)


207 
\dots


208 
rules \(name\) \(rule\)


209 
\dots


210 
end


211 
\end{ttbox}


212 
where


213 
\begin{tabular}[t]{l@{~=~}l}


214 
$classes$ & \tt[("$c$",["$c@1$",\dots,"$c@m$"]),\dots] \\


215 
$default$ & \tt["$d@1$",\dots,"$d@r$"]\\


216 
$types$ & \tt[([$tycon@1$,\dots,$tycon@i$], $n$),\dots] \\


217 
$arities$ & \tt[([$tycon'@1$,\dots,$tycon'@j$], ([$s@1$,\dots,$s@n$],$c$)),\dots]


218 
\\


219 
$consts$ & \tt[([$b@1$,\dots,$b@k$],$\tau$),\dots] \\


220 
$rules$ & \tt[("$name$",$rule$),\dots]


221 
\end{tabular}


222 


223 
If theories are defined as in \S\ref{DefiningTheories}, new syntax is added


224 
as mixfix annotations to constants. Using {\tt extend_theory}, new syntax can


225 
be added via $sextopt$ which is either {\tt None}, or {\tt Some($sext$)}. The


226 
latter case is not documented.


227 


228 
$T$ identifies the theory internally. When a theory is redeclared, say to


229 
change an incorrect axiom, bindings to the old axiom may persist. Isabelle


230 
ensures that the old and new theories are not involved in the same proof.


231 
Attempting to combine different theories having the same name $T$ yields the


232 
fatal error


233 
\begin{center} \tt


234 
Attempt to merge different versions of theory: $T$


235 
\end{center}


236 
\end{description}


237 


238 


239 
\subsection{Inspecting a theory}


240 
\index{theories!inspectingbold}


241 
\begin{ttbox}


242 
print_theory : theory > unit


243 
axioms_of : theory > (string*thm)list


244 
parents_of : theory > theory list


245 
sign_of : theory > Sign.sg


246 
stamps_of_thy : theory > string ref list


247 
\end{ttbox}


248 
These provide a simple means of viewing a theory's components.


249 
Unfortunately, there is no direct connection between a theorem and its


250 
theory.


251 
\begin{description}


252 
\item[\ttindexbold{print_theory} {\it thy}]


253 
prints the theory {\it thy\/} at the terminal as a set of identifiers.


254 


255 
\item[\ttindexbold{axioms_of} $thy$]


256 
returns the axioms of~$thy$ and its ancestors.


257 


258 
\item[\ttindexbold{parents_of} $thy$]


259 
returns the parents of~$thy$. This list contains zero, one or two


260 
elements, depending upon whether $thy$ is {\tt pure_thy},


261 
\hbox{\tt extend_theory $thy$} or \hbox{\tt merge_theories ($thy@1$, $thy@2$)}.


262 


263 
\item[\ttindexbold{stamps_of_thy} $thy$]\index{signatures}


264 
returns the stamps of the signature associated with~$thy$.


265 


266 
\item[\ttindexbold{sign_of} $thy$]


267 
returns the signature associated with~$thy$. It is useful with functions


268 
like {\tt read_instantiate_sg}, which take a signature as an argument.


269 
\end{description}


270 


271 


272 
\section{Terms}


273 
\index{termsbold}


274 
Terms belong to the \ML{} type \ttindexbold{term}, which is a concrete datatype


275 
with six constructors: there are six kinds of term.


276 
\begin{ttbox}


277 
type indexname = string * int;


278 
infix 9 $;


279 
datatype term = Const of string * typ


280 
 Free of string * typ


281 
 Var of indexname * typ


282 
 Bound of int


283 
 Abs of string * typ * term


284 
 op $ of term * term;


285 
\end{ttbox}


286 
\begin{description}


287 
\item[\ttindexbold{Const}($a$, $T$)]


288 
is the {\bf constant} with name~$a$ and type~$T$. Constants include


289 
connectives like $\land$ and $\forall$ (logical constants), as well as


290 
constants like~0 and~$Suc$. Other constants may be required to define the


291 
concrete syntax of a logic.


292 


293 
\item[\ttindexbold{Free}($a$, $T$)]


294 
is the {\bf free variable} with name~$a$ and type~$T$.


295 


296 
\item[\ttindexbold{Var}($v$, $T$)]


297 
is the {\bf scheme variable} with indexname~$v$ and type~$T$. An


298 
\ttindexbold{indexname} is a string paired with a nonnegative index, or


299 
subscript; a term's scheme variables can be systematically renamed by


300 
incrementing their subscripts. Scheme variables are essentially free


301 
variables, but may be instantiated during unification.


302 


303 
\item[\ttindexbold{Bound} $i$]


304 
is the {\bf bound variable} with de Bruijn index~$i$, which counts the


305 
number of lambdas, starting from zero, between a variable's occurrence and


306 
its binding. The representation prevents capture of variables. For more


307 
information see de Bruijn \cite{debruijn72} or


308 
Paulson~\cite[page~336]{paulson91}.


309 


310 
\item[\ttindexbold{Abs}($a$, $T$, $u$)]


311 
is the {\bf abstraction} with body~$u$, and whose bound variable has


312 
name~$a$ and type~$T$. The name is used only for parsing and printing; it


313 
has no logical significance.


314 


315 
\item[\tt $t$ \$ $u$] \index{$@{\tt\$}bold}


316 
is the {\bf application} of~$t$ to~$u$.


317 
\end{description}


318 
Application is written as an infix operator in order to aid readability.


319 
For example, here is an \ML{} pattern to recognize firstorder formula of


320 
the form~$A\imp B$, binding the subformulae to~$A$ and~$B$:


321 
\begin{ttbox}


322 
Const("Trueprop",_) $ (Const("op >",_) $ A $ B)


323 
\end{ttbox}


324 


325 


326 
\section{Certified terms}


327 
\index{terms!certifiedbold}\index{signatures}


328 
A term $t$ can be {\bf certified} under a signature to ensure that every


329 
type in~$t$ is declared in the signature and every constant in~$t$ is


330 
declared as a constant of the same type in the signature. It must be


331 
welltyped and must not have any `loose' bound variable


332 
references.\footnote{This concerns the internal representation of variable


333 
binding using de Bruijn indexes.} Metarules such as {\tt forall_elim} take


334 
certified terms as arguments.


335 


336 
Certified terms belong to the abstract type \ttindexbold{Sign.cterm}.


337 
Elements of the type can only be created through the certification process.


338 
In case of error, Isabelle raises exception~\ttindex{TERM}\@.


339 


340 
\subsection{Printing terms}


341 
\index{printing!termsbold}


342 
\begin{ttbox}


343 
Sign.string_of_cterm : Sign.cterm > string


344 
Sign.string_of_term : Sign.sg > term > string


345 
\end{ttbox}


346 
\begin{description}


347 
\item[\ttindexbold{Sign.string_of_cterm} $ct$]


348 
displays $ct$ as a string.


349 


350 
\item[\ttindexbold{Sign.string_of_term} $sign$ $t$]


351 
displays $t$ as a string, using the syntax of~$sign$.


352 
\end{description}


353 


354 
\subsection{Making and inspecting certified terms}


355 
\begin{ttbox}


356 
Sign.cterm_of : Sign.sg > term > Sign.cterm


357 
Sign.read_cterm : Sign.sg > string * typ > Sign.cterm


358 
Sign.rep_cterm : Sign.cterm > \{T:typ, t:term,


359 
sign: Sign.sg, maxidx:int\}


360 
\end{ttbox}


361 
\begin{description}


362 
\item[\ttindexbold{Sign.cterm_of} $sign$ $t$] \index{signatures}


363 
certifies $t$ with respect to signature~$sign$.


364 


365 
\item[\ttindexbold{Sign.read_cterm} $sign$ ($s$, $T$)]


366 
reads the string~$s$ using the syntax of~$sign$, creating a certified term.


367 
The term is checked to have type~$T$; this type also tells the parser what


368 
kind of phrase to parse.


369 


370 
\item[\ttindexbold{Sign.rep_cterm} $ct$]


371 
decomposes $ct$ as a record containing its type, the term itself, its


372 
signature, and the maximum subscript of its unknowns. The type and maximum


373 
subscript are computed during certification.


374 
\end{description}


375 


376 


377 
\section{Types}


378 
\index{typesbold}


379 
Types belong to the \ML{} type \ttindexbold{typ}, which is a concrete


380 
datatype with three constructors. Types are classified by sorts, which are


381 
lists of classes. A class is represented by a string.


382 
\begin{ttbox}


383 
type class = string;


384 
type sort = class list;


385 


386 
datatype typ = Type of string * typ list


387 
 TFree of string * sort


388 
 TVar of indexname * sort;


389 


390 
infixr 5 >;


391 
fun S > T = Type("fun",[S,T]);


392 
\end{ttbox}


393 
\begin{description}


394 
\item[\ttindexbold{Type}($a$, $Ts$)]


395 
applies the {\bf type constructor} named~$a$ to the type operands~$Ts$.


396 
Type constructors include~\ttindexbold{fun}, the binary function space


397 
constructor, as well as nullary type constructors such


398 
as~\ttindexbold{prop}. Other type constructors may be introduced. In


399 
expressions, but not in patterns, \hbox{\tt$S$>$T$} is a convenient


400 
shorthand for function types.


401 


402 
\item[\ttindexbold{TFree}($a$, $s$)]


403 
is the {\bf free type variable} with name~$a$ and sort~$s$.


404 


405 
\item[\ttindexbold{TVar}($v$, $s$)]


406 
is the {\bf scheme type variable} with indexname~$v$ and sort~$s$. Scheme


407 
type variables are essentially free type variables, but may be instantiated


408 
during unification.


409 
\end{description}


410 


411 


412 
\section{Certified types}


413 
\index{types!certifiedbold}


414 
Certified types, which are analogous to certified terms, have type


415 
\ttindexbold{Sign.ctyp}.


416 


417 
\subsection{Printing types}


418 
\index{printing!typesbold}


419 
\begin{ttbox}


420 
Sign.string_of_ctyp : Sign.ctyp > string


421 
Sign.string_of_typ : Sign.sg > typ > string


422 
\end{ttbox}


423 
\begin{description}


424 
\item[\ttindexbold{Sign.string_of_ctyp} $cT$]


425 
displays $cT$ as a string.


426 


427 
\item[\ttindexbold{Sign.string_of_typ} $sign$ $T$]


428 
displays $T$ as a string, using the syntax of~$sign$.


429 
\end{description}


430 


431 


432 
\subsection{Making and inspecting certified types}


433 
\begin{ttbox}


434 
Sign.ctyp_of : Sign.sg > typ > Sign.ctyp


435 
Sign.rep_ctyp : Sign.ctyp > \{T: typ, sign: Sign.sg\}


436 
\end{ttbox}


437 
\begin{description}


438 
\item[\ttindexbold{Sign.ctyp_of} $sign$ $T$] \index{signatures}


439 
certifies $T$ with respect to signature~$sign$.


440 


441 
\item[\ttindexbold{Sign.rep_ctyp} $cT$]


442 
decomposes $cT$ as a record containing the type itself and its signature.


443 
\end{description}


444 


445 
\index{theories)}
