author | clasohm |
Thu, 25 Nov 1993 14:32:54 +0100 | |
changeset 150 | 919a03a587eb |
parent 145 | 422197c5a078 |
child 159 | 3d0324f9417b |
permissions | -rw-r--r-- |
104 | 1 |
%% $Id$ |
145 | 2 |
|
104 | 3 |
\chapter{Theories, Terms and Types} \label{theories} |
4 |
\index{theories|(}\index{signatures|bold} |
|
5 |
\index{reading!axioms|see{{\tt extend_theory} and {\tt assume_ax}}} |
|
6 |
Theories organize the syntax, declarations and axioms of a mathematical |
|
7 |
development. They are built, starting from the Pure theory, by extending |
|
8 |
and merging existing theories. They have the \ML{} type \ttindex{theory}. |
|
9 |
Theory operations signal errors by raising exception \ttindex{THEORY}, |
|
10 |
returning a message and a list of theories. |
|
11 |
||
12 |
Signatures, which contain information about sorts, types, constants and |
|
13 |
syntax, have the \ML{} type~\ttindexbold{Sign.sg}. For identification, |
|
14 |
each signature carries a unique list of {\bf stamps}, which are~\ML{} |
|
15 |
references (to strings). The strings serve as human-readable names; the |
|
16 |
references serve as unique identifiers. Each primitive signature has a |
|
17 |
single stamp. When two signatures are merged, their lists of stamps are |
|
18 |
also merged. Every theory carries a unique signature. |
|
19 |
||
20 |
Terms and types are the underlying representation of logical syntax. Their |
|
21 |
\ML{} definitions are irrelevant to naive Isabelle users. Programmers who wish |
|
22 |
to extend Isabelle may need to know such details, say to code a tactic that |
|
23 |
looks for subgoals of a particular form. Terms and types may be |
|
24 |
`certified' to be well-formed with respect to a given signature. |
|
25 |
||
26 |
\section{Defining Theories} |
|
27 |
\label{DefiningTheories} |
|
28 |
||
29 |
Theories can be defined either using concrete syntax or by calling certain |
|
30 |
\ML-functions (see \S\ref{BuildingATheory}). Figure~\ref{TheorySyntax} |
|
31 |
presents the concrete syntax for theories. This grammar employs the |
|
32 |
following conventions: |
|
33 |
\begin{itemize} |
|
34 |
\item Identifiers such as $theoryDef$ denote nonterminal symbols. |
|
35 |
\item Text in {\tt typewriter font} denotes terminal symbols. |
|
36 |
\item \ldots{} indicates repetition of a phrase. |
|
37 |
\item A vertical bar~($|$) separates alternative phrases. |
|
38 |
\item Square [brackets] enclose optional phrases. |
|
39 |
\item $id$ stands for an Isabelle identifier. |
|
40 |
\item $string$ stands for an ML string, with its quotation marks. |
|
41 |
\item $k$ stands for a natural number. |
|
42 |
\item $text$ stands for arbitrary ML text. |
|
43 |
\end{itemize} |
|
44 |
||
45 |
\begin{figure}[hp] |
|
46 |
\begin{center} |
|
47 |
\begin{tabular}{rclc} |
|
138
9ba8bff1addc
added chapter "Defining Theories" and made changes for new Readthy functions
clasohm
parents:
104
diff
changeset
|
48 |
$theoryDef$ &=& $id$ {\tt=} $name@1$ {\tt+} \dots {\tt+} $name@n$ |
104 | 49 |
[{\tt+} $extension$]\\\\ |
50 |
$extension$ &=& [$classes$] [$default$] [$types$] [$arities$] [$consts$] |
|
145 | 51 |
[$trans$] [$rules$] {\tt end} [$ml$]\\\\ |
104 | 52 |
$classes$ &=& \ttindex{classes} $class$ \dots $class$ \\\\ |
53 |
$class$ &=& $id$ [{\tt<} $id@1${\tt,} \dots{\tt,} $id@n$] \\\\ |
|
54 |
$default$ &=& \ttindex{default} $sort$ \\\\ |
|
55 |
$sort$ &=& $id$ ~~$|$~~ {\tt\{} $id@1${\tt,} \dots{\tt,} $id@n$ {\tt\}} \\\\ |
|
56 |
$name$ &=& $id$ ~~$|$~~ $string$ \\\\ |
|
57 |
$types$ &=& \ttindex{types} $typeDecl$ \dots $typeDecl$ \\\\ |
|
58 |
$typeDecl$ &=& $name${\tt,} \dots{\tt,} $name$ $k$ |
|
59 |
[{\tt(} $infix$ {\tt)}] \\\\ |
|
60 |
$infix$ &=& \ttindex{infixl} $k$ ~~$|$~~ \ttindex{infixr} $k$ \\\\ |
|
61 |
$arities$ &=& \ttindex{arities} $arityDecl$ \dots $arityDecl$ \\\\ |
|
62 |
$arityDecl$ &=& $name${\tt,} \dots{\tt,} $name$ {\tt::} $arity$ \\\\ |
|
63 |
$arity$ &=& [{\tt(} $sort${\tt,} \dots{\tt,} $sort$ {\tt)}] $id$ \\\\ |
|
64 |
$consts$ &=& \ttindex{consts} $constDecl$ \dots $constDecl$ \\\\ |
|
65 |
$constDecl$ &=& $name@1${\tt,} \dots{\tt,} $name@n$ {\tt::} $string$ |
|
66 |
[{\tt(} $mixfix$ {\tt)}] \\\\ |
|
67 |
$mixfix$ &=& $string$ |
|
68 |
[ [\quad{\tt[} $k@1${\tt,} \dots{\tt,} $k@n$ {\tt]}\quad] $k$]\\ |
|
69 |
&$|$& $infix$ \\ |
|
70 |
&$|$& \ttindex{binder} $string$ $k$\\\\ |
|
145 | 71 |
$trans$ &=& \ttindex{translations} $transDecl$ \dots $transDecl$ \\\\ |
72 |
$transDecl$ &=& [ {\tt(}$string${\tt)} ] $string$ |
|
73 |
[ {\tt=>} $|$ {\tt<=} $|$ {\tt==} ] [ ($string$) ] $string$ \\\\ |
|
104 | 74 |
$rules$ &=& \ttindex{rules} $rule$ \dots $rule$ \\\\ |
75 |
$rule$ &=& $id$ $string$ \\\\ |
|
76 |
$ml$ &=& \ttindex{ML} $text$ |
|
77 |
\end{tabular} |
|
78 |
\end{center} |
|
79 |
\caption{Theory Syntax} |
|
80 |
\label{TheorySyntax} |
|
81 |
\end{figure} |
|
82 |
||
83 |
The different parts of a theory definition are interpreted as follows: |
|
138
9ba8bff1addc
added chapter "Defining Theories" and made changes for new Readthy functions
clasohm
parents:
104
diff
changeset
|
84 |
\begin{description} |
9ba8bff1addc
added chapter "Defining Theories" and made changes for new Readthy functions
clasohm
parents:
104
diff
changeset
|
85 |
\item[$theoryDef$] A theory has a name $id$ and is an |
139 | 86 |
extension of the union of theories $name@1$ \dots $name@n$ with new |
138
9ba8bff1addc
added chapter "Defining Theories" and made changes for new Readthy functions
clasohm
parents:
104
diff
changeset
|
87 |
classes, types, constants, syntax and axioms. The basic theory, which |
9ba8bff1addc
added chapter "Defining Theories" and made changes for new Readthy functions
clasohm
parents:
104
diff
changeset
|
88 |
contains only the meta-logic, is called {\tt Pure}. |
9ba8bff1addc
added chapter "Defining Theories" and made changes for new Readthy functions
clasohm
parents:
104
diff
changeset
|
89 |
|
139 | 90 |
If $name@i$ is a string, then theory $name@i$ is {\em not} used in building |
91 |
the base of theory $id$. Strings stand for ML-files rather than |
|
92 |
theory-files and document the dependence if $id$ on additional files. This |
|
93 |
is required because $name@1$ \dots $name@n$ are loaded automatically when |
|
94 |
theory $id$ is (re)built. See Chapter~\ref{LoadingTheories} for details. |
|
104 | 95 |
\item[$class$] The new class $id$ is declared as a subclass of existing |
96 |
classes $id@1$ \dots $id@n$. This rules out cyclic class structures. |
|
97 |
Isabelle automatically computes the transitive closure of subclass |
|
98 |
hierarchies. Hence it is not necessary to declare $c@1 < c@3$ in addition |
|
99 |
to $c@1 < c@2$ and $c@2 < c@3$. |
|
100 |
\item[$default$] introduces $sort$ as the new default sort for type |
|
101 |
variables. Unconstrained type variables in an input string are |
|
102 |
automatically constrained by $sort$; this does not apply to type variables |
|
103 |
created internally during type inference. If omitted, |
|
104 |
the default sort is the same as in the parent theory. |
|
105 |
\item[$sort$] is a finite set $id@1$ \dots $id@n$ of classes; a single class |
|
106 |
$id$ abbreviates the singleton set {\tt\{}$id${\tt\}}. |
|
107 |
\item[$name$] is either an alphanumeric identifier or an arbitrary string. |
|
108 |
\item[$typeDecl$] Each $name$ is declared as a new type constructor with |
|
109 |
$k$ arguments. Only binary type constructors can have infix status and |
|
110 |
symbolic names ($string$). |
|
111 |
\item[$infix$] declares a type or constant to be an infix operator of |
|
112 |
precedence $k$ associating to the left ({\tt infixl}) or right ({\tt |
|
113 |
infixr}). |
|
114 |
\item[$arityDecl$] Each existing type constructor $name@1$ \dots $name@n$ |
|
115 |
is given the additional arity $arity$. |
|
116 |
\item[$constDecl$] The new constants $name@1$ \dots $name@n$ are declared to |
|
117 |
be of type $string$. For display purposes they can be annotated with |
|
118 |
$mixfix$ declarations. |
|
119 |
\item[$mixfix$] $string$ is a mixfix template of the form {\tt"}\dots{\tt\_} |
|
120 |
\dots{\tt\_} \dots{\tt"} where the $i$-th underscore indicates the position |
|
121 |
where the $i$-th argument should go, $k@i$ is the minimum precedence of |
|
122 |
the $i$-th argument, and $k$ the precedence of the construct. The list |
|
123 |
\hbox{\tt[$k@1$, \dots, $k@n$]} is optional. |
|
124 |
||
125 |
Binary constants can be given infix status. |
|
126 |
||
127 |
A constant $f$ {\tt::} $(\tau@1\To\tau@2)\To\tau@3$ can be given {\em |
|
128 |
binder} status: {\tt binder} $Q$ $p$ causes $Q\,x.F(x)$ to be treated |
|
129 |
like $f(F)$; $p$ is the precedence of the construct. |
|
145 | 130 |
\item[$transDecl$] Specifies a syntactic translation rule, that is a parse |
131 |
rule ({\tt =>}), a print rule ({\tt <=}), or both ({\tt ==}). |
|
104 | 132 |
\item[$rule$] A rule consists of a name $id$ and a formula $string$. Rule |
133 |
names must be distinct. |
|
134 |
\item[$ml$] This final part of a theory consists of ML code, |
|
135 |
typically for parse and print translations. |
|
136 |
\end{description} |
|
145 | 137 |
The $mixfix$, $transDecl$ and $ml$ sections are explained in more detail in |
138 |
the {\it Defining Logics} chapter of the {\it Logics} manual. |
|
139 |
||
140 |
||
141 |
\subsection{Classes and types} |
|
142 |
\index{*arities!context conditions} |
|
143 |
||
144 |
Type declarations are subject to the following two well-formedness |
|
145 |
conditions: |
|
146 |
\begin{itemize} |
|
147 |
\item There are no two declarations $ty :: (\vec{r})c$ and $ty :: (\vec{s})c$ |
|
148 |
with $\vec{r} \neq \vec{s}$. For example |
|
149 |
\begin{ttbox} |
|
150 |
types ty 1 |
|
151 |
arities ty :: ({\ttlbrace}logic{\ttrbrace}) logic |
|
152 |
ty :: ({\ttlbrace}{\ttrbrace})logic |
|
153 |
\end{ttbox} |
|
154 |
leads to an error message and fails. |
|
155 |
\item If there are two declarations $ty :: (s@1,\dots,s@n)c$ and $ty :: |
|
156 |
(s@1',\dots,s@n')c'$ such that $c' < c$ then $s@i' \preceq s@i$ must hold |
|
157 |
for $i=1,\dots,n$. The relationship $\preceq$, defined as |
|
158 |
\[ s' \preceq s \iff \forall c\in s. \exists c'\in s'.~ c'\le c, \] |
|
159 |
expresses that the set of types represented by $s'$ is a subset of the set of |
|
160 |
types represented by $s$. For example |
|
161 |
\begin{ttbox} |
|
162 |
classes term < logic |
|
163 |
types ty 1 |
|
164 |
arities ty :: ({\ttlbrace}logic{\ttrbrace})logic |
|
165 |
ty :: ({\ttlbrace}{\ttrbrace})term |
|
166 |
\end{ttbox} |
|
167 |
leads to an error message and fails. |
|
168 |
\end{itemize} |
|
169 |
These conditions guarantee principal types~\cite{nipkow-prehofer}. |
|
170 |
||
104 | 171 |
|
138
9ba8bff1addc
added chapter "Defining Theories" and made changes for new Readthy functions
clasohm
parents:
104
diff
changeset
|
172 |
\section{Loading Theories} |
9ba8bff1addc
added chapter "Defining Theories" and made changes for new Readthy functions
clasohm
parents:
104
diff
changeset
|
173 |
\label{LoadingTheories} |
9ba8bff1addc
added chapter "Defining Theories" and made changes for new Readthy functions
clasohm
parents:
104
diff
changeset
|
174 |
\subsection{Reading a new theory} |
9ba8bff1addc
added chapter "Defining Theories" and made changes for new Readthy functions
clasohm
parents:
104
diff
changeset
|
175 |
|
104 | 176 |
Each theory definition must reside in a separate file. Let the file {\it |
139 | 177 |
tf}{\tt.thy} contain the definition of a theory called $TF$ with parent |
138
9ba8bff1addc
added chapter "Defining Theories" and made changes for new Readthy functions
clasohm
parents:
104
diff
changeset
|
178 |
theories $TB@1$ \dots $TB@n$. Calling \ttindexbold{use_thy}~{\tt"}{\it |
139 | 179 |
TF\/}{\tt"} reads file {\it tf}{\tt.thy}, writes an intermediate {\ML}-file |
150
919a03a587eb
changed beginning of "Reading a new theory", added index "automatic loading"
clasohm
parents:
145
diff
changeset
|
180 |
{\tt.}{\it tf}{\tt.thy.ML}, and reads the latter file. \indexbold{automatic |
919a03a587eb
changed beginning of "Reading a new theory", added index "automatic loading"
clasohm
parents:
145
diff
changeset
|
181 |
loading} Any of the parent theories that have not been loaded yet are read now |
919a03a587eb
changed beginning of "Reading a new theory", added index "automatic loading"
clasohm
parents:
145
diff
changeset
|
182 |
by recursive {\tt use_thy} calls until either an already loaded theory or {\tt |
919a03a587eb
changed beginning of "Reading a new theory", added index "automatic loading"
clasohm
parents:
145
diff
changeset
|
183 |
Pure} is reached. Therefore one can read a complete logic by just one {\tt |
919a03a587eb
changed beginning of "Reading a new theory", added index "automatic loading"
clasohm
parents:
145
diff
changeset
|
184 |
use_thy} call if all theories are linked appropriatly. Afterwards an {\ML} |
139 | 185 |
structure~$TF$ containing a component {\tt thy} for the new theory and |
186 |
components $r@1$ \dots $r@n$ for the rules is declared; it also contains the |
|
187 |
definitions of the {\tt ML} section if any. Unless |
|
150
919a03a587eb
changed beginning of "Reading a new theory", added index "automatic loading"
clasohm
parents:
145
diff
changeset
|
188 |
\ttindexbold{delete_tmpfiles} is set to {\tt false}, {\tt.}{\it tf}{\tt.thy.ML} |
919a03a587eb
changed beginning of "Reading a new theory", added index "automatic loading"
clasohm
parents:
145
diff
changeset
|
189 |
is deleted if no errors occured. Finally the file {\it tf}{\tt.ML} is read, if |
919a03a587eb
changed beginning of "Reading a new theory", added index "automatic loading"
clasohm
parents:
145
diff
changeset
|
190 |
it exists; this file normally contains proofs involving the new theory. |
138
9ba8bff1addc
added chapter "Defining Theories" and made changes for new Readthy functions
clasohm
parents:
104
diff
changeset
|
191 |
|
9ba8bff1addc
added chapter "Defining Theories" and made changes for new Readthy functions
clasohm
parents:
104
diff
changeset
|
192 |
|
9ba8bff1addc
added chapter "Defining Theories" and made changes for new Readthy functions
clasohm
parents:
104
diff
changeset
|
193 |
\subsection{Filenames and paths} |
141
a133921366cb
added index commands, removed last paragraph of "Using Poly/ML"
clasohm
parents:
139
diff
changeset
|
194 |
\indexbold{filenames} |
138
9ba8bff1addc
added chapter "Defining Theories" and made changes for new Readthy functions
clasohm
parents:
104
diff
changeset
|
195 |
|
9ba8bff1addc
added chapter "Defining Theories" and made changes for new Readthy functions
clasohm
parents:
104
diff
changeset
|
196 |
The files the theory definition resides in must have the lower case name of |
141
a133921366cb
added index commands, removed last paragraph of "Using Poly/ML"
clasohm
parents:
139
diff
changeset
|
197 |
the theory with ".thy" or ".ML" appended. On the other hand \ttindex{use_thy}'s |
138
9ba8bff1addc
added chapter "Defining Theories" and made changes for new Readthy functions
clasohm
parents:
104
diff
changeset
|
198 |
parameter has to be the exact theory name. Optionally the name can be |
9ba8bff1addc
added chapter "Defining Theories" and made changes for new Readthy functions
clasohm
parents:
104
diff
changeset
|
199 |
preceeded by a path to specify the directory where the files can be found. If |
141
a133921366cb
added index commands, removed last paragraph of "Using Poly/ML"
clasohm
parents:
139
diff
changeset
|
200 |
no path is provided the reference variable \ttindexbold{loadpath} is used which |
138
9ba8bff1addc
added chapter "Defining Theories" and made changes for new Readthy functions
clasohm
parents:
104
diff
changeset
|
201 |
contains a list of paths that are searched in the given order. After the |
139 | 202 |
".thy"-file for a theory has been found, the same path is used to locate the |
138
9ba8bff1addc
added chapter "Defining Theories" and made changes for new Readthy functions
clasohm
parents:
104
diff
changeset
|
203 |
(optional) ".ML"-file. (You might note that it is also possible to only |
139 | 204 |
provide a ".ML"- but no ".thy"-file. In this case an \ML{} structure with the |
138
9ba8bff1addc
added chapter "Defining Theories" and made changes for new Readthy functions
clasohm
parents:
104
diff
changeset
|
205 |
theory's name has to be created in the ".ML" file. If both the ".thy"-file |
9ba8bff1addc
added chapter "Defining Theories" and made changes for new Readthy functions
clasohm
parents:
104
diff
changeset
|
206 |
and a structure declaration in the ".ML"-file exist the declaration in the |
9ba8bff1addc
added chapter "Defining Theories" and made changes for new Readthy functions
clasohm
parents:
104
diff
changeset
|
207 |
latter file is used. See {\tt ZF/ex/llist.ML} for an example.) |
9ba8bff1addc
added chapter "Defining Theories" and made changes for new Readthy functions
clasohm
parents:
104
diff
changeset
|
208 |
|
9ba8bff1addc
added chapter "Defining Theories" and made changes for new Readthy functions
clasohm
parents:
104
diff
changeset
|
209 |
|
9ba8bff1addc
added chapter "Defining Theories" and made changes for new Readthy functions
clasohm
parents:
104
diff
changeset
|
210 |
\subsection{Reloading a theory} |
141
a133921366cb
added index commands, removed last paragraph of "Using Poly/ML"
clasohm
parents:
139
diff
changeset
|
211 |
\index{reloading a theory} |
138
9ba8bff1addc
added chapter "Defining Theories" and made changes for new Readthy functions
clasohm
parents:
104
diff
changeset
|
212 |
|
141
a133921366cb
added index commands, removed last paragraph of "Using Poly/ML"
clasohm
parents:
139
diff
changeset
|
213 |
\ttindex{use_thy} keeps track of all loaded theories and stores information |
a133921366cb
added index commands, removed last paragraph of "Using Poly/ML"
clasohm
parents:
139
diff
changeset
|
214 |
about their files. If it finds that the theory to be loaded was already read |
139 | 215 |
before, the following happens: First the theory's files are searched at the |
141
a133921366cb
added index commands, removed last paragraph of "Using Poly/ML"
clasohm
parents:
139
diff
changeset
|
216 |
place they were located the last time they were read. If they are found, their |
a133921366cb
added index commands, removed last paragraph of "Using Poly/ML"
clasohm
parents:
139
diff
changeset
|
217 |
time of last modification is compared to the internal data and {\tt use_thy} |
a133921366cb
added index commands, removed last paragraph of "Using Poly/ML"
clasohm
parents:
139
diff
changeset
|
218 |
stops if they are equal. In case the files have been moved, {\tt use_thy} |
a133921366cb
added index commands, removed last paragraph of "Using Poly/ML"
clasohm
parents:
139
diff
changeset
|
219 |
searches them the same way a new theory would be searched for. After all these |
a133921366cb
added index commands, removed last paragraph of "Using Poly/ML"
clasohm
parents:
139
diff
changeset
|
220 |
tests have been passed, the theory is reloaded and all theories that depend on |
a133921366cb
added index commands, removed last paragraph of "Using Poly/ML"
clasohm
parents:
139
diff
changeset
|
221 |
it (i.e. that have its name in their $theoryDef$) are marked as out-of-date. |
138
9ba8bff1addc
added chapter "Defining Theories" and made changes for new Readthy functions
clasohm
parents:
104
diff
changeset
|
222 |
|
9ba8bff1addc
added chapter "Defining Theories" and made changes for new Readthy functions
clasohm
parents:
104
diff
changeset
|
223 |
As changing a theory often makes it necessary to reload all theories that |
141
a133921366cb
added index commands, removed last paragraph of "Using Poly/ML"
clasohm
parents:
139
diff
changeset
|
224 |
(indirectly) depend on it, \ttindexbold{update} should be used instead of {\tt |
138
9ba8bff1addc
added chapter "Defining Theories" and made changes for new Readthy functions
clasohm
parents:
104
diff
changeset
|
225 |
use_thy} to read a modified theory. This function reloads all changed |
9ba8bff1addc
added chapter "Defining Theories" and made changes for new Readthy functions
clasohm
parents:
104
diff
changeset
|
226 |
theories and their descendants in the correct order. |
9ba8bff1addc
added chapter "Defining Theories" and made changes for new Readthy functions
clasohm
parents:
104
diff
changeset
|
227 |
|
9ba8bff1addc
added chapter "Defining Theories" and made changes for new Readthy functions
clasohm
parents:
104
diff
changeset
|
228 |
|
9ba8bff1addc
added chapter "Defining Theories" and made changes for new Readthy functions
clasohm
parents:
104
diff
changeset
|
229 |
\subsection{Pseudo theories} |
141
a133921366cb
added index commands, removed last paragraph of "Using Poly/ML"
clasohm
parents:
139
diff
changeset
|
230 |
\indexbold{pseudo theories} |
138
9ba8bff1addc
added chapter "Defining Theories" and made changes for new Readthy functions
clasohm
parents:
104
diff
changeset
|
231 |
|
141
a133921366cb
added index commands, removed last paragraph of "Using Poly/ML"
clasohm
parents:
139
diff
changeset
|
232 |
There is a problem with \ttindex{update}: objects created in \ML-files that do |
a133921366cb
added index commands, removed last paragraph of "Using Poly/ML"
clasohm
parents:
139
diff
changeset
|
233 |
not belong to a theory (see explanation of $theoryDef$ in |
a133921366cb
added index commands, removed last paragraph of "Using Poly/ML"
clasohm
parents:
139
diff
changeset
|
234 |
\ref{DefiningTheories}). These files are read manually between {\tt use_thy} |
a133921366cb
added index commands, removed last paragraph of "Using Poly/ML"
clasohm
parents:
139
diff
changeset
|
235 |
calls and define objects used in different theories. As {\tt update} only |
a133921366cb
added index commands, removed last paragraph of "Using Poly/ML"
clasohm
parents:
139
diff
changeset
|
236 |
knows about the theories there still exist objects with references to the old |
a133921366cb
added index commands, removed last paragraph of "Using Poly/ML"
clasohm
parents:
139
diff
changeset
|
237 |
theory version after the new one has been read. This (most probably) will |
a133921366cb
added index commands, removed last paragraph of "Using Poly/ML"
clasohm
parents:
139
diff
changeset
|
238 |
produce the fatal error |
138
9ba8bff1addc
added chapter "Defining Theories" and made changes for new Readthy functions
clasohm
parents:
104
diff
changeset
|
239 |
\begin{center} \tt |
9ba8bff1addc
added chapter "Defining Theories" and made changes for new Readthy functions
clasohm
parents:
104
diff
changeset
|
240 |
Attempt to merge different versions of theory: $T$ |
9ba8bff1addc
added chapter "Defining Theories" and made changes for new Readthy functions
clasohm
parents:
104
diff
changeset
|
241 |
\end{center} |
9ba8bff1addc
added chapter "Defining Theories" and made changes for new Readthy functions
clasohm
parents:
104
diff
changeset
|
242 |
|
9ba8bff1addc
added chapter "Defining Theories" and made changes for new Readthy functions
clasohm
parents:
104
diff
changeset
|
243 |
Therefore there is a way to link theories and the $orphaned$ \ML-files. The |
139 | 244 |
link from a theory to an \ML-file has been mentioned in |
138
9ba8bff1addc
added chapter "Defining Theories" and made changes for new Readthy functions
clasohm
parents:
104
diff
changeset
|
245 |
Chapter~\ref{DefiningTheories} (strings in $theoryDef$). But to make this |
9ba8bff1addc
added chapter "Defining Theories" and made changes for new Readthy functions
clasohm
parents:
104
diff
changeset
|
246 |
work and to establish a link in the opposite direction we need to create a |
139 | 247 |
{\it pseudo theory}. Let's assume we have an \ML-file named {\tt orphan.ML} |
248 |
that depends on theory $A$ and is itself used in theory $B$. To link the |
|
249 |
three we have to create the file {\tt orphan.thy} containing the line |
|
138
9ba8bff1addc
added chapter "Defining Theories" and made changes for new Readthy functions
clasohm
parents:
104
diff
changeset
|
250 |
\begin{ttbox} |
9ba8bff1addc
added chapter "Defining Theories" and made changes for new Readthy functions
clasohm
parents:
104
diff
changeset
|
251 |
orphan = A |
9ba8bff1addc
added chapter "Defining Theories" and made changes for new Readthy functions
clasohm
parents:
104
diff
changeset
|
252 |
\end{ttbox} |
139 | 253 |
and add {\tt "orphan"} to the list of $B$'s parents. Creating {\tt |
254 |
orphan.thy} is necessary because of two reasons: First it enables automatic |
|
255 |
loading of $orphan$'s parents and second it creates the \ML{}-object {\tt |
|
256 |
orphan} that is needed by {\tt use_thy} (though it is not added to the base |
|
257 |
of theory $B$). If {\tt orphan.ML} depended on no theory then {\tt Pure} |
|
258 |
would have been used instead of {\tt A}. |
|
138
9ba8bff1addc
added chapter "Defining Theories" and made changes for new Readthy functions
clasohm
parents:
104
diff
changeset
|
259 |
|
9ba8bff1addc
added chapter "Defining Theories" and made changes for new Readthy functions
clasohm
parents:
104
diff
changeset
|
260 |
For an extensive example of how this technique can be used to link over 30 |
139 | 261 |
files and read them by just two {\tt use_thy} calls have a look at the ZF |
262 |
logic. |
|
138
9ba8bff1addc
added chapter "Defining Theories" and made changes for new Readthy functions
clasohm
parents:
104
diff
changeset
|
263 |
|
9ba8bff1addc
added chapter "Defining Theories" and made changes for new Readthy functions
clasohm
parents:
104
diff
changeset
|
264 |
|
9ba8bff1addc
added chapter "Defining Theories" and made changes for new Readthy functions
clasohm
parents:
104
diff
changeset
|
265 |
\subsection{Removing a theory} |
141
a133921366cb
added index commands, removed last paragraph of "Using Poly/ML"
clasohm
parents:
139
diff
changeset
|
266 |
\index{removing theories} |
138
9ba8bff1addc
added chapter "Defining Theories" and made changes for new Readthy functions
clasohm
parents:
104
diff
changeset
|
267 |
|
141
a133921366cb
added index commands, removed last paragraph of "Using Poly/ML"
clasohm
parents:
139
diff
changeset
|
268 |
If a previously read file is removed the \ttindex{update} function will keep |
138
9ba8bff1addc
added chapter "Defining Theories" and made changes for new Readthy functions
clasohm
parents:
104
diff
changeset
|
269 |
on complaining about a missing file. The theory is not automatically removed |
9ba8bff1addc
added chapter "Defining Theories" and made changes for new Readthy functions
clasohm
parents:
104
diff
changeset
|
270 |
from the internal list to preserve the links to other theories in case one |
9ba8bff1addc
added chapter "Defining Theories" and made changes for new Readthy functions
clasohm
parents:
104
diff
changeset
|
271 |
forgot to adjust the {\tt loadpath} after moving a file. To manually remove a |
141
a133921366cb
added index commands, removed last paragraph of "Using Poly/ML"
clasohm
parents:
139
diff
changeset
|
272 |
theory use \ttindexbold{unlink_thy}. |
138
9ba8bff1addc
added chapter "Defining Theories" and made changes for new Readthy functions
clasohm
parents:
104
diff
changeset
|
273 |
|
9ba8bff1addc
added chapter "Defining Theories" and made changes for new Readthy functions
clasohm
parents:
104
diff
changeset
|
274 |
|
9ba8bff1addc
added chapter "Defining Theories" and made changes for new Readthy functions
clasohm
parents:
104
diff
changeset
|
275 |
\subsection{Using Poly/\ML} |
141
a133921366cb
added index commands, removed last paragraph of "Using Poly/ML"
clasohm
parents:
139
diff
changeset
|
276 |
\index{Poly/\ML} |
a133921366cb
added index commands, removed last paragraph of "Using Poly/ML"
clasohm
parents:
139
diff
changeset
|
277 |
\index{reference variables} |
138
9ba8bff1addc
added chapter "Defining Theories" and made changes for new Readthy functions
clasohm
parents:
104
diff
changeset
|
278 |
|
9ba8bff1addc
added chapter "Defining Theories" and made changes for new Readthy functions
clasohm
parents:
104
diff
changeset
|
279 |
As the functions for reading theories depend on reference variables one has to |
9ba8bff1addc
added chapter "Defining Theories" and made changes for new Readthy functions
clasohm
parents:
104
diff
changeset
|
280 |
take into consideration the way Poly/\ML{} handles them. They are only saved |
9ba8bff1addc
added chapter "Defining Theories" and made changes for new Readthy functions
clasohm
parents:
104
diff
changeset
|
281 |
together with the state if they were declared in the current database. E.g. |
9ba8bff1addc
added chapter "Defining Theories" and made changes for new Readthy functions
clasohm
parents:
104
diff
changeset
|
282 |
changes made to a reference variable declared in the $Pure$ database are $not$ |
9ba8bff1addc
added chapter "Defining Theories" and made changes for new Readthy functions
clasohm
parents:
104
diff
changeset
|
283 |
saved if made while using a child database. Therefore a new {\tt Readthy} |
9ba8bff1addc
added chapter "Defining Theories" and made changes for new Readthy functions
clasohm
parents:
104
diff
changeset
|
284 |
structure has to be declared by |
9ba8bff1addc
added chapter "Defining Theories" and made changes for new Readthy functions
clasohm
parents:
104
diff
changeset
|
285 |
\begin{ttbox} |
9ba8bff1addc
added chapter "Defining Theories" and made changes for new Readthy functions
clasohm
parents:
104
diff
changeset
|
286 |
structure Readthy = ReadthyFUN (structure ThySyn = ThySyn); |
141
a133921366cb
added index commands, removed last paragraph of "Using Poly/ML"
clasohm
parents:
139
diff
changeset
|
287 |
Readthy.loaded_thys := !loaded_thys; |
138
9ba8bff1addc
added chapter "Defining Theories" and made changes for new Readthy functions
clasohm
parents:
104
diff
changeset
|
288 |
open Readthy; |
9ba8bff1addc
added chapter "Defining Theories" and made changes for new Readthy functions
clasohm
parents:
104
diff
changeset
|
289 |
\end{ttbox} |
141
a133921366cb
added index commands, removed last paragraph of "Using Poly/ML"
clasohm
parents:
139
diff
changeset
|
290 |
in every newly created database. By copying the contents of the old reference |
a133921366cb
added index commands, removed last paragraph of "Using Poly/ML"
clasohm
parents:
139
diff
changeset
|
291 |
variable loaded_thys the list of already loaded theories is preserved. Of |
a133921366cb
added index commands, removed last paragraph of "Using Poly/ML"
clasohm
parents:
139
diff
changeset
|
292 |
course this is not necessary if no theories have been read yet. |
104 | 293 |
|
294 |
||
295 |
\section{Basic operations on theories} |
|
296 |
\subsection{Extracting an axiom from a theory} |
|
297 |
\index{theories!extracting axioms|bold}\index{axioms} |
|
298 |
\begin{ttbox} |
|
299 |
get_axiom: theory -> string -> thm |
|
300 |
assume_ax: theory -> string -> thm |
|
301 |
\end{ttbox} |
|
302 |
\begin{description} |
|
303 |
\item[\ttindexbold{get_axiom} $thy$ $name$] |
|
304 |
returns an axiom with the given $name$ from $thy$, raising exception |
|
305 |
\ttindex{THEORY} if none exists. Merging theories can cause several axioms |
|
306 |
to have the same name; {\tt get_axiom} returns an arbitrary one. |
|
307 |
||
308 |
\item[\ttindexbold{assume_ax} $thy$ $formula$] |
|
309 |
reads the {\it formula} using the syntax of $thy$, following the same |
|
310 |
conventions as axioms in a theory definition. You can thus pretend that |
|
311 |
{\it formula} is an axiom; in fact, {\tt assume_ax} returns an assumption. |
|
312 |
You can use the resulting theorem like an axiom. Note that |
|
313 |
\ttindex{result} complains about additional assumptions, but |
|
314 |
\ttindex{uresult} does not. |
|
315 |
||
316 |
For example, if {\it formula} is |
|
317 |
\hbox{\tt a=b ==> b=a} then the resulting theorem might have the form |
|
318 |
\hbox{\tt\frenchspacing ?a=?b ==> ?b=?a [!!a b. a=b ==> b=a]} |
|
319 |
\end{description} |
|
320 |
||
321 |
\subsection{Building a theory} |
|
322 |
\label{BuildingATheory} |
|
323 |
\index{theories!constructing|bold} |
|
324 |
\begin{ttbox} |
|
325 |
pure_thy: theory |
|
326 |
merge_theories: theory * theory -> theory |
|
327 |
extend_theory: theory -> string |
|
328 |
-> (class * class list) list |
|
329 |
* sort |
|
330 |
* (string list * int)list |
|
331 |
* (string list * (sort list * class))list |
|
332 |
* (string list * string)list * sext option |
|
333 |
-> (string*string)list -> theory |
|
334 |
\end{ttbox} |
|
335 |
Type \ttindex{class} is a synonym for {\tt string}; type \ttindex{sort} is |
|
336 |
a synonym for \hbox{\tt class list}. |
|
337 |
\begin{description} |
|
338 |
\item[\ttindexbold{pure_thy}] contains just the types, constants, and syntax |
|
339 |
of the meta-logic. There are no axioms: meta-level inferences are carried |
|
340 |
out by \ML\ functions. |
|
341 |
\item[\ttindexbold{merge_theories} ($thy@1$, $thy@2$)] merges the two |
|
342 |
theories $thy@1$ and $thy@2$. The resulting theory contains all types, |
|
343 |
constants and axioms of the constituent theories; its default sort is the |
|
344 |
union of the default sorts of the constituent theories. |
|
345 |
\item [\ttindexbold{extend_theory} $thy$ {\tt"}$T${\tt"} |
|
346 |
($classes$, $default$, $types$, $arities$, $consts$, $sextopt$) $rules$] |
|
347 |
\hfill\break %%% include if line is just too short |
|
348 |
is the \ML-equivalent of the following theory definition: |
|
349 |
\begin{ttbox} |
|
350 |
\(T\) = \(thy\) + |
|
351 |
classes \(c\) < \(c@1\),\(\dots\),\(c@m\) |
|
352 |
\dots |
|
353 |
default {\(d@1,\dots,d@r\)} |
|
354 |
types \(tycon@1\),\dots,\(tycon@i\) \(n\) |
|
355 |
\dots |
|
356 |
arities \(tycon@1'\),\dots,\(tycon@j'\) :: (\(s@1\),\dots,\(s@n\))\(c\) |
|
357 |
\dots |
|
358 |
consts \(b@1\),\dots,\(b@k\) :: \(\tau\) |
|
359 |
\dots |
|
360 |
rules \(name\) \(rule\) |
|
361 |
\dots |
|
362 |
end |
|
363 |
\end{ttbox} |
|
364 |
where |
|
365 |
\begin{tabular}[t]{l@{~=~}l} |
|
366 |
$classes$ & \tt[("$c$",["$c@1$",\dots,"$c@m$"]),\dots] \\ |
|
367 |
$default$ & \tt["$d@1$",\dots,"$d@r$"]\\ |
|
368 |
$types$ & \tt[([$tycon@1$,\dots,$tycon@i$], $n$),\dots] \\ |
|
369 |
$arities$ & \tt[([$tycon'@1$,\dots,$tycon'@j$], ([$s@1$,\dots,$s@n$],$c$)),\dots] |
|
370 |
\\ |
|
371 |
$consts$ & \tt[([$b@1$,\dots,$b@k$],$\tau$),\dots] \\ |
|
372 |
$rules$ & \tt[("$name$",$rule$),\dots] |
|
373 |
\end{tabular} |
|
374 |
||
375 |
If theories are defined as in \S\ref{DefiningTheories}, new syntax is added |
|
376 |
as mixfix annotations to constants. Using {\tt extend_theory}, new syntax can |
|
377 |
be added via $sextopt$ which is either {\tt None}, or {\tt Some($sext$)}. The |
|
378 |
latter case is not documented. |
|
379 |
||
380 |
$T$ identifies the theory internally. When a theory is redeclared, say to |
|
381 |
change an incorrect axiom, bindings to the old axiom may persist. Isabelle |
|
382 |
ensures that the old and new theories are not involved in the same proof. |
|
383 |
Attempting to combine different theories having the same name $T$ yields the |
|
384 |
fatal error |
|
385 |
\begin{center} \tt |
|
386 |
Attempt to merge different versions of theory: $T$ |
|
387 |
\end{center} |
|
388 |
\end{description} |
|
389 |
||
390 |
||
391 |
\subsection{Inspecting a theory} |
|
392 |
\index{theories!inspecting|bold} |
|
393 |
\begin{ttbox} |
|
394 |
print_theory : theory -> unit |
|
395 |
axioms_of : theory -> (string*thm)list |
|
396 |
parents_of : theory -> theory list |
|
397 |
sign_of : theory -> Sign.sg |
|
398 |
stamps_of_thy : theory -> string ref list |
|
399 |
\end{ttbox} |
|
400 |
These provide a simple means of viewing a theory's components. |
|
401 |
Unfortunately, there is no direct connection between a theorem and its |
|
402 |
theory. |
|
403 |
\begin{description} |
|
404 |
\item[\ttindexbold{print_theory} {\it thy}] |
|
405 |
prints the theory {\it thy\/} at the terminal as a set of identifiers. |
|
406 |
||
407 |
\item[\ttindexbold{axioms_of} $thy$] |
|
408 |
returns the axioms of~$thy$ and its ancestors. |
|
409 |
||
410 |
\item[\ttindexbold{parents_of} $thy$] |
|
411 |
returns the parents of~$thy$. This list contains zero, one or two |
|
412 |
elements, depending upon whether $thy$ is {\tt pure_thy}, |
|
413 |
\hbox{\tt extend_theory $thy$} or \hbox{\tt merge_theories ($thy@1$, $thy@2$)}. |
|
414 |
||
415 |
\item[\ttindexbold{stamps_of_thy} $thy$]\index{signatures} |
|
416 |
returns the stamps of the signature associated with~$thy$. |
|
417 |
||
418 |
\item[\ttindexbold{sign_of} $thy$] |
|
419 |
returns the signature associated with~$thy$. It is useful with functions |
|
420 |
like {\tt read_instantiate_sg}, which take a signature as an argument. |
|
421 |
\end{description} |
|
422 |
||
423 |
||
424 |
\section{Terms} |
|
425 |
\index{terms|bold} |
|
426 |
Terms belong to the \ML{} type \ttindexbold{term}, which is a concrete datatype |
|
427 |
with six constructors: there are six kinds of term. |
|
428 |
\begin{ttbox} |
|
429 |
type indexname = string * int; |
|
430 |
infix 9 $; |
|
431 |
datatype term = Const of string * typ |
|
432 |
| Free of string * typ |
|
433 |
| Var of indexname * typ |
|
434 |
| Bound of int |
|
435 |
| Abs of string * typ * term |
|
436 |
| op $ of term * term; |
|
437 |
\end{ttbox} |
|
438 |
\begin{description} |
|
439 |
\item[\ttindexbold{Const}($a$, $T$)] |
|
440 |
is the {\bf constant} with name~$a$ and type~$T$. Constants include |
|
441 |
connectives like $\land$ and $\forall$ (logical constants), as well as |
|
442 |
constants like~0 and~$Suc$. Other constants may be required to define the |
|
443 |
concrete syntax of a logic. |
|
444 |
||
445 |
\item[\ttindexbold{Free}($a$, $T$)] |
|
446 |
is the {\bf free variable} with name~$a$ and type~$T$. |
|
447 |
||
448 |
\item[\ttindexbold{Var}($v$, $T$)] |
|
449 |
is the {\bf scheme variable} with indexname~$v$ and type~$T$. An |
|
450 |
\ttindexbold{indexname} is a string paired with a non-negative index, or |
|
451 |
subscript; a term's scheme variables can be systematically renamed by |
|
452 |
incrementing their subscripts. Scheme variables are essentially free |
|
453 |
variables, but may be instantiated during unification. |
|
454 |
||
455 |
\item[\ttindexbold{Bound} $i$] |
|
456 |
is the {\bf bound variable} with de Bruijn index~$i$, which counts the |
|
457 |
number of lambdas, starting from zero, between a variable's occurrence and |
|
458 |
its binding. The representation prevents capture of variables. For more |
|
459 |
information see de Bruijn \cite{debruijn72} or |
|
460 |
Paulson~\cite[page~336]{paulson91}. |
|
461 |
||
462 |
\item[\ttindexbold{Abs}($a$, $T$, $u$)] |
|
463 |
is the {\bf abstraction} with body~$u$, and whose bound variable has |
|
464 |
name~$a$ and type~$T$. The name is used only for parsing and printing; it |
|
465 |
has no logical significance. |
|
466 |
||
467 |
\item[\tt $t$ \$ $u$] \index{$@{\tt\$}|bold} |
|
468 |
is the {\bf application} of~$t$ to~$u$. |
|
469 |
\end{description} |
|
470 |
Application is written as an infix operator in order to aid readability. |
|
471 |
For example, here is an \ML{} pattern to recognize first-order formula of |
|
472 |
the form~$A\imp B$, binding the subformulae to~$A$ and~$B$: |
|
473 |
\begin{ttbox} |
|
474 |
Const("Trueprop",_) $ (Const("op -->",_) $ A $ B) |
|
475 |
\end{ttbox} |
|
476 |
||
477 |
||
478 |
\section{Certified terms} |
|
479 |
\index{terms!certified|bold}\index{signatures} |
|
480 |
A term $t$ can be {\bf certified} under a signature to ensure that every |
|
481 |
type in~$t$ is declared in the signature and every constant in~$t$ is |
|
482 |
declared as a constant of the same type in the signature. It must be |
|
483 |
well-typed and must not have any `loose' bound variable |
|
484 |
references.\footnote{This concerns the internal representation of variable |
|
485 |
binding using de Bruijn indexes.} Meta-rules such as {\tt forall_elim} take |
|
486 |
certified terms as arguments. |
|
487 |
||
488 |
Certified terms belong to the abstract type \ttindexbold{Sign.cterm}. |
|
489 |
Elements of the type can only be created through the certification process. |
|
490 |
In case of error, Isabelle raises exception~\ttindex{TERM}\@. |
|
491 |
||
492 |
\subsection{Printing terms} |
|
493 |
\index{printing!terms|bold} |
|
494 |
\begin{ttbox} |
|
495 |
Sign.string_of_cterm : Sign.cterm -> string |
|
496 |
Sign.string_of_term : Sign.sg -> term -> string |
|
497 |
\end{ttbox} |
|
498 |
\begin{description} |
|
499 |
\item[\ttindexbold{Sign.string_of_cterm} $ct$] |
|
500 |
displays $ct$ as a string. |
|
501 |
||
502 |
\item[\ttindexbold{Sign.string_of_term} $sign$ $t$] |
|
503 |
displays $t$ as a string, using the syntax of~$sign$. |
|
504 |
\end{description} |
|
505 |
||
506 |
\subsection{Making and inspecting certified terms} |
|
507 |
\begin{ttbox} |
|
508 |
Sign.cterm_of : Sign.sg -> term -> Sign.cterm |
|
509 |
Sign.read_cterm : Sign.sg -> string * typ -> Sign.cterm |
|
510 |
Sign.rep_cterm : Sign.cterm -> \{T:typ, t:term, |
|
511 |
sign: Sign.sg, maxidx:int\} |
|
512 |
\end{ttbox} |
|
513 |
\begin{description} |
|
514 |
\item[\ttindexbold{Sign.cterm_of} $sign$ $t$] \index{signatures} |
|
515 |
certifies $t$ with respect to signature~$sign$. |
|
516 |
||
517 |
\item[\ttindexbold{Sign.read_cterm} $sign$ ($s$, $T$)] |
|
518 |
reads the string~$s$ using the syntax of~$sign$, creating a certified term. |
|
519 |
The term is checked to have type~$T$; this type also tells the parser what |
|
520 |
kind of phrase to parse. |
|
521 |
||
522 |
\item[\ttindexbold{Sign.rep_cterm} $ct$] |
|
523 |
decomposes $ct$ as a record containing its type, the term itself, its |
|
524 |
signature, and the maximum subscript of its unknowns. The type and maximum |
|
525 |
subscript are computed during certification. |
|
526 |
\end{description} |
|
527 |
||
528 |
||
529 |
\section{Types} |
|
530 |
\index{types|bold} |
|
531 |
Types belong to the \ML{} type \ttindexbold{typ}, which is a concrete |
|
532 |
datatype with three constructors. Types are classified by sorts, which are |
|
533 |
lists of classes. A class is represented by a string. |
|
534 |
\begin{ttbox} |
|
535 |
type class = string; |
|
536 |
type sort = class list; |
|
537 |
||
538 |
datatype typ = Type of string * typ list |
|
539 |
| TFree of string * sort |
|
540 |
| TVar of indexname * sort; |
|
541 |
||
542 |
infixr 5 -->; |
|
543 |
fun S --> T = Type("fun",[S,T]); |
|
544 |
\end{ttbox} |
|
545 |
\begin{description} |
|
546 |
\item[\ttindexbold{Type}($a$, $Ts$)] |
|
547 |
applies the {\bf type constructor} named~$a$ to the type operands~$Ts$. |
|
548 |
Type constructors include~\ttindexbold{fun}, the binary function space |
|
549 |
constructor, as well as nullary type constructors such |
|
550 |
as~\ttindexbold{prop}. Other type constructors may be introduced. In |
|
551 |
expressions, but not in patterns, \hbox{\tt$S$-->$T$} is a convenient |
|
552 |
shorthand for function types. |
|
553 |
||
554 |
\item[\ttindexbold{TFree}($a$, $s$)] |
|
555 |
is the {\bf free type variable} with name~$a$ and sort~$s$. |
|
556 |
||
557 |
\item[\ttindexbold{TVar}($v$, $s$)] |
|
558 |
is the {\bf scheme type variable} with indexname~$v$ and sort~$s$. Scheme |
|
559 |
type variables are essentially free type variables, but may be instantiated |
|
560 |
during unification. |
|
561 |
\end{description} |
|
562 |
||
563 |
||
564 |
\section{Certified types} |
|
565 |
\index{types!certified|bold} |
|
566 |
Certified types, which are analogous to certified terms, have type |
|
567 |
\ttindexbold{Sign.ctyp}. |
|
568 |
||
569 |
\subsection{Printing types} |
|
570 |
\index{printing!types|bold} |
|
571 |
\begin{ttbox} |
|
572 |
Sign.string_of_ctyp : Sign.ctyp -> string |
|
573 |
Sign.string_of_typ : Sign.sg -> typ -> string |
|
574 |
\end{ttbox} |
|
575 |
\begin{description} |
|
576 |
\item[\ttindexbold{Sign.string_of_ctyp} $cT$] |
|
577 |
displays $cT$ as a string. |
|
578 |
||
579 |
\item[\ttindexbold{Sign.string_of_typ} $sign$ $T$] |
|
580 |
displays $T$ as a string, using the syntax of~$sign$. |
|
581 |
\end{description} |
|
582 |
||
583 |
||
584 |
\subsection{Making and inspecting certified types} |
|
585 |
\begin{ttbox} |
|
586 |
Sign.ctyp_of : Sign.sg -> typ -> Sign.ctyp |
|
587 |
Sign.rep_ctyp : Sign.ctyp -> \{T: typ, sign: Sign.sg\} |
|
588 |
\end{ttbox} |
|
589 |
\begin{description} |
|
590 |
\item[\ttindexbold{Sign.ctyp_of} $sign$ $T$] \index{signatures} |
|
591 |
certifies $T$ with respect to signature~$sign$. |
|
592 |
||
593 |
\item[\ttindexbold{Sign.rep_ctyp} $cT$] |
|
594 |
decomposes $cT$ as a record containing the type itself and its signature. |
|
595 |
\end{description} |
|
596 |
||
597 |
\index{theories|)} |