author | clasohm |
Thu, 19 Jan 1995 16:05:21 +0100 | |
changeset 866 | 2d3d020eef11 |
parent 864 | d63b111b917a |
child 1369 | b82815e61b30 |
permissions | -rw-r--r-- |
104 | 1 |
%% $Id$ |
145 | 2 |
|
104 | 3 |
\chapter{Theories, Terms and Types} \label{theories} |
4 |
\index{theories|(}\index{signatures|bold} |
|
478 | 5 |
\index{reading!axioms|see{{\tt assume_ax}}} |
104 | 6 |
Theories organize the syntax, declarations and axioms of a mathematical |
7 |
development. They are built, starting from the Pure theory, by extending |
|
324 | 8 |
and merging existing theories. They have the \ML\ type \mltydx{theory}. |
9 |
Theory operations signal errors by raising exception \xdx{THEORY}, |
|
104 | 10 |
returning a message and a list of theories. |
11 |
||
12 |
Signatures, which contain information about sorts, types, constants and |
|
332 | 13 |
syntax, have the \ML\ type~\mltydx{Sign.sg}. For identification, each |
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
14 |
signature carries a unique list of \bfindex{stamps}, which are \ML\ |
324 | 15 |
references to strings. The strings serve as human-readable names; the |
104 | 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 |
|
275 | 21 |
\ML\ definitions are irrelevant to naive Isabelle users. Programmers who |
22 |
wish to extend Isabelle may need to know such details, say to code a tactic |
|
23 |
that looks for subgoals of a particular form. Terms and types may be |
|
104 | 24 |
`certified' to be well-formed with respect to a given signature. |
25 |
||
324 | 26 |
|
27 |
\section{Defining theories}\label{sec:ref-defining-theories} |
|
104 | 28 |
|
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
29 |
Theories are usually defined using theory definition files (which have a name |
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
30 |
suffix {\tt .thy}). There is also a low level interface provided by certain |
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
31 |
\ML{} functions (see \S\ref{BuildingATheory}). |
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
32 |
Appendix~\ref{app:TheorySyntax} presents the concrete syntax for theory |
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
33 |
definitions; here is an explanation of the constituent parts: |
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
34 |
\begin{description} |
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
35 |
\item[{\it theoryDef}] |
324 | 36 |
is the full definition. The new theory is called $id$. It is the union |
37 |
of the named {\bf parent theories}\indexbold{theories!parent}, possibly |
|
38 |
extended with new classes, etc. The basic theory, which contains only |
|
39 |
the meta-logic, is called \thydx{Pure}. |
|
138
9ba8bff1addc
added chapter "Defining Theories" and made changes for new Readthy functions
clasohm
parents:
104
diff
changeset
|
40 |
|
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
41 |
Normally each {\it name\/} is an identifier, the name of the parent theory. |
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
42 |
Quoted strings can be used to document additional file dependencies; see |
275 | 43 |
\S\ref{LoadingTheories} for details. |
324 | 44 |
|
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
45 |
\item[$classes$] |
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
46 |
is a series of class declarations. Declaring {\tt$id$ < $id@1$ \dots\ |
324 | 47 |
$id@n$} makes $id$ a subclass of the existing classes $id@1\dots |
48 |
id@n$. This rules out cyclic class structures. Isabelle automatically |
|
49 |
computes the transitive closure of subclass hierarchies; it is not |
|
50 |
necessary to declare {\tt c < e} in addition to {\tt c < d} and {\tt d < |
|
51 |
e}. |
|
52 |
||
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
53 |
\item[$default$] |
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
54 |
introduces $sort$ as the new default sort for type variables. This applies |
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
55 |
to unconstrained type variables in an input string but not to type |
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
56 |
variables created internally. If omitted, the default sort is the listwise |
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
57 |
union of the default sorts of the parent theories (i.e.\ their logical |
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
58 |
intersection). |
324 | 59 |
|
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
60 |
\item[$sort$] |
324 | 61 |
is a finite set of classes. A single class $id$ abbreviates the singleton |
62 |
set {\tt\{}$id${\tt\}}. |
|
63 |
||
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
64 |
\item[$types$] |
324 | 65 |
is a series of type declarations. Each declares a new type constructor |
66 |
or type synonym. An $n$-place type constructor is specified by |
|
67 |
$(\alpha@1,\dots,\alpha@n)name$, where the type variables serve only to |
|
68 |
indicate the number~$n$. |
|
69 |
||
332 | 70 |
A {\bf type synonym}\indexbold{type synonyms} is an abbreviation |
324 | 71 |
$(\alpha@1,\dots,\alpha@n)name = \mbox{\tt"}\tau\mbox{\tt"}$, where |
72 |
$name$ can be a string and $\tau$ must be enclosed in quotation marks. |
|
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
73 |
|
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
74 |
\item[$infix$] |
324 | 75 |
declares a type or constant to be an infix operator of priority $nat$ |
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
76 |
associating to the left ({\tt infixl}) or right ({\tt infixr}). Only |
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
77 |
2-place type constructors can have infix status; an example is {\tt |
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
78 |
('a,'b)~"*"~(infixr~20)}, which expresses binary product types. |
324 | 79 |
|
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
80 |
\item[$arities$] |
324 | 81 |
is a series of arity declarations. Each assigns arities to type |
82 |
constructors. The $name$ must be an existing type constructor, which is |
|
273 | 83 |
given the additional arity $arity$. |
324 | 84 |
|
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
85 |
\item[$constDecl$] |
324 | 86 |
is a series of constant declarations. Each new constant $name$ is given |
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
87 |
the type specified by the $string$. The optional $mixfix$ annotations may |
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
88 |
attach concrete syntax to the constant. A variant of {\tt consts} is the |
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
89 |
{\tt syntax} section\index{*syntax section}, which adds just syntax without |
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
90 |
declaring logical constants. |
324 | 91 |
|
92 |
\item[$mixfix$] \index{mixfix declarations} |
|
93 |
annotations can take three forms: |
|
273 | 94 |
\begin{itemize} |
95 |
\item A mixfix template given as a $string$ of the form |
|
96 |
{\tt"}\dots{\tt\_}\dots{\tt\_}\dots{\tt"} where the $i$-th underscore |
|
324 | 97 |
indicates the position where the $i$-th argument should go. The list |
98 |
of numbers gives the priority of each argument. The final number gives |
|
99 |
the priority of the whole construct. |
|
104 | 100 |
|
324 | 101 |
\item A constant $f$ of type $\tau@1\To(\tau@2\To\tau)$ can be given {\bf |
102 |
infix} status. |
|
104 | 103 |
|
324 | 104 |
\item A constant $f$ of type $(\tau@1\To\tau@2)\To\tau$ can be given {\bf |
105 |
binder} status. The declaration {\tt binder} $\cal Q$ $p$ causes |
|
286 | 106 |
${\cal Q}\,x.F(x)$ to be treated |
107 |
like $f(F)$, where $p$ is the priority. |
|
273 | 108 |
\end{itemize} |
324 | 109 |
|
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
110 |
\item[$trans$] |
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
111 |
specifies syntactic translation rules (macros). There are three forms: |
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
112 |
parse rules ({\tt =>}), print rules ({\tt <=}), and parse/print rules ({\tt |
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
113 |
==}). |
324 | 114 |
|
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
115 |
\item[$rule$] |
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
116 |
is a series of rule declarations. Each has a name $id$ and the formula is |
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
117 |
given by the $string$. Rule names must be distinct within any single |
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
118 |
theory file. |
324 | 119 |
|
120 |
\item[$ml$] \index{*ML section} |
|
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
121 |
consists of \ML\ code, typically for parse and print translation functions. |
104 | 122 |
\end{description} |
324 | 123 |
% |
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
124 |
Chapters~\ref{Defining-Logics} and \ref{chap:syntax} explain mixfix |
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
125 |
declarations, translation rules and the {\tt ML} section in more detail. |
145 | 126 |
|
127 |
||
275 | 128 |
\subsection{*Classes and arities} |
324 | 129 |
\index{classes!context conditions}\index{arities!context conditions} |
145 | 130 |
|
286 | 131 |
In order to guarantee principal types~\cite{nipkow-prehofer}, |
324 | 132 |
arity declarations must obey two conditions: |
145 | 133 |
\begin{itemize} |
286 | 134 |
\item There must be no two declarations $ty :: (\vec{r})c$ and $ty :: |
135 |
(\vec{s})c$ with $\vec{r} \neq \vec{s}$. For example, the following is |
|
136 |
forbidden: |
|
145 | 137 |
\begin{ttbox} |
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
138 |
types |
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
139 |
'a ty |
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
140 |
arities |
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
141 |
ty :: ({\ttlbrace}logic{\ttrbrace}) logic |
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
142 |
ty :: ({\ttlbrace}{\ttrbrace})logic |
145 | 143 |
\end{ttbox} |
286 | 144 |
|
145 | 145 |
\item If there are two declarations $ty :: (s@1,\dots,s@n)c$ and $ty :: |
146 |
(s@1',\dots,s@n')c'$ such that $c' < c$ then $s@i' \preceq s@i$ must hold |
|
147 |
for $i=1,\dots,n$. The relationship $\preceq$, defined as |
|
148 |
\[ s' \preceq s \iff \forall c\in s. \exists c'\in s'.~ c'\le c, \] |
|
149 |
expresses that the set of types represented by $s'$ is a subset of the set of |
|
286 | 150 |
types represented by $s$. For example, the following is forbidden: |
145 | 151 |
\begin{ttbox} |
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
152 |
classes |
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
153 |
term < logic |
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
154 |
types |
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
155 |
'a ty |
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
156 |
arities |
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
157 |
ty :: ({\ttlbrace}logic{\ttrbrace})logic |
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
158 |
ty :: ({\ttlbrace}{\ttrbrace})term |
145 | 159 |
\end{ttbox} |
286 | 160 |
|
145 | 161 |
\end{itemize} |
162 |
||
104 | 163 |
|
324 | 164 |
\section{Loading a new theory}\label{LoadingTheories} |
165 |
\index{theories!loading}\index{files!reading} |
|
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
166 |
\begin{ttbox} |
286 | 167 |
use_thy : string -> unit |
168 |
time_use_thy : string -> unit |
|
169 |
loadpath : string list ref \hfill{\bf initially {\tt["."]}} |
|
170 |
delete_tmpfiles : bool ref \hfill{\bf initially true} |
|
171 |
\end{ttbox} |
|
172 |
||
324 | 173 |
\begin{ttdescription} |
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
174 |
\item[\ttindexbold{use_thy} $thyname$] |
286 | 175 |
reads the theory $thyname$ and creates an \ML{} structure as described below. |
275 | 176 |
|
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
177 |
\item[\ttindexbold{time_use_thy} $thyname$] |
286 | 178 |
calls {\tt use_thy} $thyname$ and reports the time taken. |
138
9ba8bff1addc
added chapter "Defining Theories" and made changes for new Readthy functions
clasohm
parents:
104
diff
changeset
|
179 |
|
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
180 |
\item[\ttindexbold{loadpath}] |
286 | 181 |
contains a list of directories to search when locating the files that |
182 |
define a theory. This list is only used if the theory name in {\tt |
|
183 |
use_thy} does not specify the path explicitly. |
|
184 |
||
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
185 |
\item[\ttindexbold{delete_tmpfiles} := false;] |
286 | 186 |
suppresses the deletion of temporary files. |
324 | 187 |
\end{ttdescription} |
286 | 188 |
% |
104 | 189 |
Each theory definition must reside in a separate file. Let the file {\it |
332 | 190 |
T}{\tt.thy} contain the definition of a theory called~$T$, whose parent |
191 |
theories are $TB@1$ \dots $TB@n$. Calling \ttindexbold{use_thy}~{\tt"{\it |
|
192 |
T\/}"} reads the file {\it T}{\tt.thy}, writes a temporary \ML{} |
|
193 |
file {\tt.{\it T}.thy.ML}, and reads the latter file. Recursive {\tt |
|
286 | 194 |
use_thy} calls load those parent theories that have not been loaded |
332 | 195 |
previously; the recursive calls may continue to any depth. One {\tt use_thy} |
196 |
call can read an entire logic provided all theories are linked appropriately. |
|
138
9ba8bff1addc
added chapter "Defining Theories" and made changes for new Readthy functions
clasohm
parents:
104
diff
changeset
|
197 |
|
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
198 |
The result is an \ML\ structure~$T$ containing at least a component {\tt thy} |
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
199 |
for the new theory and components for each of the rules. The structure also |
332 | 200 |
contains the definitions of the {\tt ML} section, if present. The file |
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
201 |
{\tt.{\it T}.thy.ML} is then deleted if {\tt delete_tmpfiles} is set to {\tt |
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
202 |
true} and no errors occurred. |
138
9ba8bff1addc
added chapter "Defining Theories" and made changes for new Readthy functions
clasohm
parents:
104
diff
changeset
|
203 |
|
332 | 204 |
Finally the file {\it T}{\tt.ML} is read, if it exists. This file normally |
205 |
begins with the declaration {\tt open~$T$} and contains proofs involving |
|
206 |
the new theory. |
|
207 |
||
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
208 |
Some applications construct theories directly by calling \ML\ functions. In |
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
209 |
this situation there is no {\tt.thy} file, only an {\tt.ML} file. The |
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
210 |
{\tt.ML} file must declare an \ML\ structure having the theory's name and a |
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
211 |
component {\tt thy} containing the new theory object. |
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
212 |
Section~\ref{sec:pseudo-theories} below describes a way of linking such |
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
213 |
theories to their parents. |
324 | 214 |
|
215 |
\begin{warn} |
|
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
216 |
Temporary files are written to the current directory, so this must be |
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
217 |
writable. Isabelle inherits the current directory from the operating |
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
218 |
system; you can change it within Isabelle by typing {\tt |
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
219 |
cd"$dir$"}\index{*cd}. |
273 | 220 |
\end{warn} |
138
9ba8bff1addc
added chapter "Defining Theories" and made changes for new Readthy functions
clasohm
parents:
104
diff
changeset
|
221 |
|
9ba8bff1addc
added chapter "Defining Theories" and made changes for new Readthy functions
clasohm
parents:
104
diff
changeset
|
222 |
|
324 | 223 |
\section{Reloading modified theories}\label{sec:reloading-theories} |
224 |
\indexbold{theories!reloading} |
|
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
225 |
\begin{ttbox} |
286 | 226 |
update : unit -> unit |
227 |
unlink_thy : string -> unit |
|
228 |
\end{ttbox} |
|
332 | 229 |
Changing a theory on disk often makes it necessary to reload all theories |
230 |
descended from it. However, {\tt use_thy} reads only one theory, even if |
|
231 |
some of the parent theories are out of date. In this case you should call |
|
232 |
{\tt update()}. |
|
233 |
||
286 | 234 |
Isabelle keeps track of all loaded theories and their files. If |
235 |
\ttindex{use_thy} finds that the theory to be loaded has been read before, |
|
236 |
it determines whether to reload the theory as follows. First it looks for |
|
237 |
the theory's files in their previous location. If it finds them, it |
|
238 |
compares their modification times to the internal data and stops if they |
|
239 |
are equal. If the files have been moved, {\tt use_thy} searches for them |
|
240 |
as it would for a new theory. After {\tt use_thy} reloads a theory, it |
|
241 |
marks the children as out-of-date. |
|
242 |
||
324 | 243 |
\begin{ttdescription} |
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
244 |
\item[\ttindexbold{update}()] |
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
245 |
reloads all modified theories and their descendants in the correct order. |
138
9ba8bff1addc
added chapter "Defining Theories" and made changes for new Readthy functions
clasohm
parents:
104
diff
changeset
|
246 |
|
286 | 247 |
\item[\ttindexbold{unlink_thy} $thyname$]\indexbold{theories!removing} |
248 |
informs Isabelle that theory $thyname$ no longer exists. If you delete the |
|
249 |
theory files for $thyname$ then you must execute {\tt unlink_thy}; |
|
250 |
otherwise {\tt update} will complain about a missing file. |
|
324 | 251 |
\end{ttdescription} |
286 | 252 |
|
253 |
||
332 | 254 |
\goodbreak |
324 | 255 |
\subsection{Important note for Poly/ML users}\index{Poly/{\ML} compiler} |
286 | 256 |
The theory mechanism depends upon reference variables. At the end of a |
257 |
Poly/\ML{} session, the contents of references are lost unless they are |
|
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
258 |
declared in the current database. In particular, assignments to references |
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
259 |
of the {\tt Pure} database are lost, including all information about loaded |
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
260 |
theories. To avoid losing this information simply call |
286 | 261 |
\begin{ttbox} |
478 | 262 |
init_thy_reader(); |
286 | 263 |
\end{ttbox} |
478 | 264 |
when building the new database. |
286 | 265 |
|
266 |
||
332 | 267 |
\subsection{*Pseudo theories}\label{sec:pseudo-theories} |
268 |
\indexbold{theories!pseudo}% |
|
275 | 269 |
Any automatic reloading facility requires complete knowledge of all |
286 | 270 |
dependencies. Sometimes theories depend on objects created in \ML{} files |
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
271 |
with no associated theory definition file. These objects may be theories but |
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
272 |
they could also be theorems, proof procedures, etc. |
332 | 273 |
|
274 |
Unless such dependencies are documented, {\tt update} fails to reload these |
|
275 |
\ML{} files and the system is left in a state where some objects, such as |
|
276 |
theorems, still refer to old versions of theories. This may lead to the |
|
277 |
error |
|
275 | 278 |
\begin{ttbox} |
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
279 |
Attempt to merge different versions of theories: \dots |
275 | 280 |
\end{ttbox} |
324 | 281 |
Therefore there is a way to link theories and {\bf orphaned} \ML{} files --- |
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
282 |
those not associated with a theory definition. |
138
9ba8bff1addc
added chapter "Defining Theories" and made changes for new Readthy functions
clasohm
parents:
104
diff
changeset
|
283 |
|
324 | 284 |
Let us assume we have an orphaned \ML{} file named {\tt orphan.ML} and a |
332 | 285 |
theory~$B$ that depends on {\tt orphan.ML} --- for example, {\tt B.ML} uses |
286 |
theorems proved in {\tt orphan.ML}. Then {\tt B.thy} should |
|
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
287 |
mention this dependency as follows: |
138
9ba8bff1addc
added chapter "Defining Theories" and made changes for new Readthy functions
clasohm
parents:
104
diff
changeset
|
288 |
\begin{ttbox} |
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
289 |
B = \(\ldots\) + "orphan" + \(\ldots\) |
138
9ba8bff1addc
added chapter "Defining Theories" and made changes for new Readthy functions
clasohm
parents:
104
diff
changeset
|
290 |
\end{ttbox} |
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
291 |
Quoted strings stand for \ML{} files rather than theories, and merely |
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
292 |
document additional dependencies. Thus {\tt orphan} is not used in building |
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
293 |
the base of theory~$B$, but {\tt orphan.ML} is loaded automatically |
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
294 |
whenever~$B$ is (re)built. |
275 | 295 |
|
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
296 |
The orphaned file may have its own dependencies. If {\tt orphan.ML} depends |
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
297 |
on theories or files $A@1$, \ldots, $A@n$, record this by creating a {\bf |
324 | 298 |
pseudo theory} in the file {\tt orphan.thy}: |
275 | 299 |
\begin{ttbox} |
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
300 |
orphan = \(A@1\) + \(\ldots\) + \(A@n\) |
275 | 301 |
\end{ttbox} |
286 | 302 |
The resulting theory is a dummy, but it ensures that {\tt update} reloads |
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
303 |
{\tt orphan} whenever it reloads one of the $A@i$. |
138
9ba8bff1addc
added chapter "Defining Theories" and made changes for new Readthy functions
clasohm
parents:
104
diff
changeset
|
304 |
|
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
305 |
For an extensive example of how this technique can be used to link lots of |
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
306 |
theory files and load them by just a few {\tt use_thy} calls, consult the |
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
307 |
sources of \ZF{} set theory. |
138
9ba8bff1addc
added chapter "Defining Theories" and made changes for new Readthy functions
clasohm
parents:
104
diff
changeset
|
308 |
|
104 | 309 |
|
310 |
||
866
2d3d020eef11
added documentation of bind_thm, qed, qed_goal, get_thm, thms_of
clasohm
parents:
864
diff
changeset
|
311 |
\section{Basic operations on theories}\label{BasicOperationsOnTheories} |
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
312 |
\subsection{Extracting an axiom or theorem from a theory} |
324 | 313 |
\index{theories!axioms of}\index{axioms!extracting} |
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
314 |
\index{theories!theorems of}\index{theorems!extracting} |
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
315 |
\begin{ttbox} |
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
316 |
get_axiom : theory -> string -> thm |
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
317 |
get_thm : theory -> string -> thm |
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
318 |
assume_ax : theory -> string -> thm |
104 | 319 |
\end{ttbox} |
324 | 320 |
\begin{ttdescription} |
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
321 |
\item[\ttindexbold{get_axiom} $thy$ $name$] |
866
2d3d020eef11
added documentation of bind_thm, qed, qed_goal, get_thm, thms_of
clasohm
parents:
864
diff
changeset
|
322 |
returns an axiom with the given $name$ from $thy$, raising exception |
2d3d020eef11
added documentation of bind_thm, qed, qed_goal, get_thm, thms_of
clasohm
parents:
864
diff
changeset
|
323 |
\xdx{THEORY} if none exists. Merging theories can cause several axioms |
2d3d020eef11
added documentation of bind_thm, qed, qed_goal, get_thm, thms_of
clasohm
parents:
864
diff
changeset
|
324 |
to have the same name; {\tt get_axiom} returns an arbitrary one. |
104 | 325 |
|
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
326 |
\item[\ttindexbold{get_thm} $thy$ $name$] |
866
2d3d020eef11
added documentation of bind_thm, qed, qed_goal, get_thm, thms_of
clasohm
parents:
864
diff
changeset
|
327 |
is analogous to {\tt get_axiom}, but looks for a stored theorem. Like |
2d3d020eef11
added documentation of bind_thm, qed, qed_goal, get_thm, thms_of
clasohm
parents:
864
diff
changeset
|
328 |
{\tt get_axiom} it searches all parents of a theory if the theorem |
2d3d020eef11
added documentation of bind_thm, qed, qed_goal, get_thm, thms_of
clasohm
parents:
864
diff
changeset
|
329 |
is not associated with $thy$. |
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
330 |
|
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
331 |
\item[\ttindexbold{assume_ax} $thy$ $formula$] |
286 | 332 |
reads the {\it formula} using the syntax of $thy$, following the same |
333 |
conventions as axioms in a theory definition. You can thus pretend that |
|
334 |
{\it formula} is an axiom and use the resulting theorem like an axiom. |
|
335 |
Actually {\tt assume_ax} returns an assumption; \ttindex{result} |
|
336 |
complains about additional assumptions, but \ttindex{uresult} does not. |
|
104 | 337 |
|
338 |
For example, if {\it formula} is |
|
332 | 339 |
\hbox{\tt a=b ==> b=a} then the resulting theorem has the form |
340 |
\hbox{\verb'?a=?b ==> ?b=?a [!!a b. a=b ==> b=a]'} |
|
324 | 341 |
\end{ttdescription} |
104 | 342 |
|
286 | 343 |
\subsection{Building a theory} |
344 |
\label{BuildingATheory} |
|
345 |
\index{theories!constructing|bold} |
|
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
346 |
\begin{ttbox} |
332 | 347 |
pure_thy : theory |
348 |
merge_theories : theory * theory -> theory |
|
286 | 349 |
\end{ttbox} |
324 | 350 |
\begin{ttdescription} |
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
351 |
\item[\ttindexbold{pure_thy}] contains just the syntax and signature |
286 | 352 |
of the meta-logic. There are no axioms: meta-level inferences are carried |
353 |
out by \ML\ functions. |
|
354 |
\item[\ttindexbold{merge_theories} ($thy@1$, $thy@2$)] merges the two |
|
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
355 |
theories $thy@1$ and $thy@2$. The resulting theory contains all of the |
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
356 |
syntax, signature and axioms of the constituent theories. Merging theories |
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
357 |
that contain different identification stamps of the same name fails with |
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
358 |
the following message |
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
359 |
\begin{ttbox} |
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
360 |
Attempt to merge different versions of theories: "\(T@1\)", \(\ldots\), "\(T@n\)" |
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
361 |
\end{ttbox} |
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
362 |
This error may especially occur when a theory is redeclared --- say to |
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
363 |
change an incorrect axiom --- and bindings to old versions persist. |
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
364 |
Isabelle ensures that old and new theories of the same name are not |
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
365 |
involved in a proof. |
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
366 |
|
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
367 |
%% FIXME |
478 | 368 |
%\item [\ttindexbold{extend_theory} $thy$ {\tt"}$T${\tt"} $\cdots$] extends |
369 |
% the theory $thy$ with new types, constants, etc. $T$ identifies the theory |
|
370 |
% internally. When a theory is redeclared, say to change an incorrect axiom, |
|
371 |
% bindings to the old axiom may persist. Isabelle ensures that the old and |
|
372 |
% new theories are not involved in the same proof. Attempting to combine |
|
373 |
% different theories having the same name $T$ yields the fatal error |
|
374 |
%extend_theory : theory -> string -> \(\cdots\) -> theory |
|
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
375 |
%\begin{ttbox} |
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
376 |
%Attempt to merge different versions of theory: \(T\) |
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
377 |
%\end{ttbox} |
324 | 378 |
\end{ttdescription} |
286 | 379 |
|
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
380 |
%% FIXME |
275 | 381 |
%\item [\ttindexbold{extend_theory} $thy$ {\tt"}$T${\tt"} |
382 |
% ($classes$, $default$, $types$, $arities$, $consts$, $sextopt$) $rules$] |
|
383 |
%\hfill\break %%% include if line is just too short |
|
286 | 384 |
%is the \ML{} equivalent of the following theory definition: |
275 | 385 |
%\begin{ttbox} |
386 |
%\(T\) = \(thy\) + |
|
387 |
%classes \(c\) < \(c@1\),\(\dots\),\(c@m\) |
|
388 |
% \dots |
|
389 |
%default {\(d@1,\dots,d@r\)} |
|
390 |
%types \(tycon@1\),\dots,\(tycon@i\) \(n\) |
|
391 |
% \dots |
|
392 |
%arities \(tycon@1'\),\dots,\(tycon@j'\) :: (\(s@1\),\dots,\(s@n\))\(c\) |
|
393 |
% \dots |
|
394 |
%consts \(b@1\),\dots,\(b@k\) :: \(\tau\) |
|
395 |
% \dots |
|
396 |
%rules \(name\) \(rule\) |
|
397 |
% \dots |
|
398 |
%end |
|
399 |
%\end{ttbox} |
|
400 |
%where |
|
401 |
%\begin{tabular}[t]{l@{~=~}l} |
|
402 |
%$classes$ & \tt[("$c$",["$c@1$",\dots,"$c@m$"]),\dots] \\ |
|
403 |
%$default$ & \tt["$d@1$",\dots,"$d@r$"]\\ |
|
404 |
%$types$ & \tt[([$tycon@1$,\dots,$tycon@i$], $n$),\dots] \\ |
|
405 |
%$arities$ & \tt[([$tycon'@1$,\dots,$tycon'@j$], ([$s@1$,\dots,$s@n$],$c$)),\dots] |
|
406 |
%\\ |
|
407 |
%$consts$ & \tt[([$b@1$,\dots,$b@k$],$\tau$),\dots] \\ |
|
408 |
%$rules$ & \tt[("$name$",$rule$),\dots] |
|
409 |
%\end{tabular} |
|
104 | 410 |
|
411 |
||
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
412 |
\subsection{Inspecting a theory}\label{sec:inspct-thy} |
104 | 413 |
\index{theories!inspecting|bold} |
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
414 |
\begin{ttbox} |
104 | 415 |
print_theory : theory -> unit |
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
416 |
axioms_of : theory -> (string * thm) list |
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
417 |
thms_of : theory -> (string * thm) list |
104 | 418 |
parents_of : theory -> theory list |
419 |
sign_of : theory -> Sign.sg |
|
420 |
stamps_of_thy : theory -> string ref list |
|
421 |
\end{ttbox} |
|
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
422 |
These provide means of viewing a theory's components. |
324 | 423 |
\begin{ttdescription} |
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
424 |
\item[\ttindexbold{print_theory} $thy$] |
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
425 |
prints the contents of $thy$ excluding the syntax related parts (which are |
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
426 |
shown by {\tt print_syntax}). The output is quite verbose. |
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
427 |
|
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
428 |
\item[\ttindexbold{axioms_of} $thy$] |
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
429 |
returns the additional axioms of the most recent extend node of~$thy$. |
104 | 430 |
|
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
431 |
\item[\ttindexbold{thms_of} $thy$] |
866
2d3d020eef11
added documentation of bind_thm, qed, qed_goal, get_thm, thms_of
clasohm
parents:
864
diff
changeset
|
432 |
returns all theorems that are associated with $thy$. |
104 | 433 |
|
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
434 |
\item[\ttindexbold{parents_of} $thy$] |
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
435 |
returns the direct ancestors of~$thy$. |
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
436 |
|
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
437 |
\item[\ttindexbold{sign_of} $thy$] |
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
438 |
returns the signature associated with~$thy$. It is useful with functions |
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
439 |
like {\tt read_instantiate_sg}, which take a signature as an argument. |
104 | 440 |
|
441 |
\item[\ttindexbold{stamps_of_thy} $thy$]\index{signatures} |
|
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
442 |
returns the identification \rmindex{stamps} of the signature associated |
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
443 |
with~$thy$. |
324 | 444 |
\end{ttdescription} |
104 | 445 |
|
446 |
||
447 |
\section{Terms} |
|
448 |
\index{terms|bold} |
|
324 | 449 |
Terms belong to the \ML\ type \mltydx{term}, which is a concrete datatype |
104 | 450 |
with six constructors: there are six kinds of term. |
451 |
\begin{ttbox} |
|
452 |
type indexname = string * int; |
|
453 |
infix 9 $; |
|
454 |
datatype term = Const of string * typ |
|
455 |
| Free of string * typ |
|
456 |
| Var of indexname * typ |
|
457 |
| Bound of int |
|
458 |
| Abs of string * typ * term |
|
459 |
| op $ of term * term; |
|
460 |
\end{ttbox} |
|
324 | 461 |
\begin{ttdescription} |
462 |
\item[\ttindexbold{Const}($a$, $T$)] \index{constants|bold} |
|
286 | 463 |
is the {\bf constant} with name~$a$ and type~$T$. Constants include |
464 |
connectives like $\land$ and $\forall$ as well as constants like~0 |
|
465 |
and~$Suc$. Other constants may be required to define a logic's concrete |
|
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
466 |
syntax. |
104 | 467 |
|
324 | 468 |
\item[\ttindexbold{Free}($a$, $T$)] \index{variables!free|bold} |
469 |
is the {\bf free variable} with name~$a$ and type~$T$. |
|
104 | 470 |
|
324 | 471 |
\item[\ttindexbold{Var}($v$, $T$)] \index{unknowns|bold} |
472 |
is the {\bf scheme variable} with indexname~$v$ and type~$T$. An |
|
473 |
\mltydx{indexname} is a string paired with a non-negative index, or |
|
474 |
subscript; a term's scheme variables can be systematically renamed by |
|
475 |
incrementing their subscripts. Scheme variables are essentially free |
|
476 |
variables, but may be instantiated during unification. |
|
104 | 477 |
|
324 | 478 |
\item[\ttindexbold{Bound} $i$] \index{variables!bound|bold} |
479 |
is the {\bf bound variable} with de Bruijn index~$i$, which counts the |
|
480 |
number of lambdas, starting from zero, between a variable's occurrence |
|
481 |
and its binding. The representation prevents capture of variables. For |
|
482 |
more information see de Bruijn \cite{debruijn72} or |
|
483 |
Paulson~\cite[page~336]{paulson91}. |
|
104 | 484 |
|
324 | 485 |
\item[\ttindexbold{Abs}($a$, $T$, $u$)] |
486 |
\index{lambda abs@$\lambda$-abstractions|bold} |
|
487 |
is the $\lambda$-{\bf abstraction} with body~$u$, and whose bound |
|
488 |
variable has name~$a$ and type~$T$. The name is used only for parsing |
|
489 |
and printing; it has no logical significance. |
|
104 | 490 |
|
324 | 491 |
\item[$t$ \$ $u$] \index{$@{\tt\$}|bold} \index{function applications|bold} |
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
492 |
is the {\bf application} of~$t$ to~$u$. |
324 | 493 |
\end{ttdescription} |
286 | 494 |
Application is written as an infix operator to aid readability. |
332 | 495 |
Here is an \ML\ pattern to recognize \FOL{} formulae of |
104 | 496 |
the form~$A\imp B$, binding the subformulae to~$A$ and~$B$: |
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
497 |
\begin{ttbox} |
104 | 498 |
Const("Trueprop",_) $ (Const("op -->",_) $ A $ B) |
499 |
\end{ttbox} |
|
500 |
||
501 |
||
324 | 502 |
\section{Variable binding} |
286 | 503 |
\begin{ttbox} |
504 |
loose_bnos : term -> int list |
|
505 |
incr_boundvars : int -> term -> term |
|
506 |
abstract_over : term*term -> term |
|
507 |
variant_abs : string * typ * term -> string * term |
|
508 |
aconv : term*term -> bool\hfill{\bf infix} |
|
509 |
\end{ttbox} |
|
510 |
These functions are all concerned with the de Bruijn representation of |
|
511 |
bound variables. |
|
324 | 512 |
\begin{ttdescription} |
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
513 |
\item[\ttindexbold{loose_bnos} $t$] |
286 | 514 |
returns the list of all dangling bound variable references. In |
515 |
particular, {\tt Bound~0} is loose unless it is enclosed in an |
|
516 |
abstraction. Similarly {\tt Bound~1} is loose unless it is enclosed in |
|
517 |
at least two abstractions; if enclosed in just one, the list will contain |
|
518 |
the number 0. A well-formed term does not contain any loose variables. |
|
519 |
||
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
520 |
\item[\ttindexbold{incr_boundvars} $j$] |
332 | 521 |
increases a term's dangling bound variables by the offset~$j$. This is |
286 | 522 |
required when moving a subterm into a context where it is enclosed by a |
523 |
different number of abstractions. Bound variables with a matching |
|
524 |
abstraction are unaffected. |
|
525 |
||
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
526 |
\item[\ttindexbold{abstract_over} $(v,t)$] |
286 | 527 |
forms the abstraction of~$t$ over~$v$, which may be any well-formed term. |
528 |
It replaces every occurrence of \(v\) by a {\tt Bound} variable with the |
|
529 |
correct index. |
|
530 |
||
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
531 |
\item[\ttindexbold{variant_abs} $(a,T,u)$] |
286 | 532 |
substitutes into $u$, which should be the body of an abstraction. |
533 |
It replaces each occurrence of the outermost bound variable by a free |
|
534 |
variable. The free variable has type~$T$ and its name is a variant |
|
332 | 535 |
of~$a$ chosen to be distinct from all constants and from all variables |
286 | 536 |
free in~$u$. |
537 |
||
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
538 |
\item[$t$ \ttindexbold{aconv} $u$] |
286 | 539 |
tests whether terms~$t$ and~$u$ are \(\alpha\)-convertible: identical up |
540 |
to renaming of bound variables. |
|
541 |
\begin{itemize} |
|
542 |
\item |
|
543 |
Two constants, {\tt Free}s, or {\tt Var}s are \(\alpha\)-convertible |
|
544 |
if their names and types are equal. |
|
545 |
(Variables having the same name but different types are thus distinct. |
|
546 |
This confusing situation should be avoided!) |
|
547 |
\item |
|
548 |
Two bound variables are \(\alpha\)-convertible |
|
549 |
if they have the same number. |
|
550 |
\item |
|
551 |
Two abstractions are \(\alpha\)-convertible |
|
552 |
if their bodies are, and their bound variables have the same type. |
|
553 |
\item |
|
554 |
Two applications are \(\alpha\)-convertible |
|
555 |
if the corresponding subterms are. |
|
556 |
\end{itemize} |
|
557 |
||
324 | 558 |
\end{ttdescription} |
286 | 559 |
|
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
560 |
\section{Certified terms}\index{terms!certified|bold}\index{signatures} |
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
561 |
A term $t$ can be {\bf certified} under a signature to ensure that every type |
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
562 |
in~$t$ is well-formed and every constant in~$t$ is a type instance of a |
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
563 |
constant declared in the signature. The term must be well-typed and its use |
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
564 |
of bound variables must be well-formed. Meta-rules such as {\tt forall_elim} |
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
565 |
take certified terms as arguments. |
104 | 566 |
|
324 | 567 |
Certified terms belong to the abstract type \mltydx{cterm}. |
104 | 568 |
Elements of the type can only be created through the certification process. |
569 |
In case of error, Isabelle raises exception~\ttindex{TERM}\@. |
|
570 |
||
571 |
\subsection{Printing terms} |
|
324 | 572 |
\index{terms!printing of} |
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
573 |
\begin{ttbox} |
275 | 574 |
string_of_cterm : cterm -> string |
104 | 575 |
Sign.string_of_term : Sign.sg -> term -> string |
576 |
\end{ttbox} |
|
324 | 577 |
\begin{ttdescription} |
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
578 |
\item[\ttindexbold{string_of_cterm} $ct$] |
104 | 579 |
displays $ct$ as a string. |
580 |
||
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
581 |
\item[\ttindexbold{Sign.string_of_term} $sign$ $t$] |
104 | 582 |
displays $t$ as a string, using the syntax of~$sign$. |
324 | 583 |
\end{ttdescription} |
104 | 584 |
|
585 |
\subsection{Making and inspecting certified terms} |
|
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
586 |
\begin{ttbox} |
275 | 587 |
cterm_of : Sign.sg -> term -> cterm |
588 |
read_cterm : Sign.sg -> string * typ -> cterm |
|
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
589 |
cert_axm : Sign.sg -> string * term -> string * term |
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
590 |
read_axm : Sign.sg -> string * string -> string * term |
275 | 591 |
rep_cterm : cterm -> \{T:typ, t:term, sign:Sign.sg, maxidx:int\} |
104 | 592 |
\end{ttbox} |
324 | 593 |
\begin{ttdescription} |
275 | 594 |
\item[\ttindexbold{cterm_of} $sign$ $t$] \index{signatures} |
104 | 595 |
certifies $t$ with respect to signature~$sign$. |
596 |
||
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
597 |
\item[\ttindexbold{read_cterm} $sign$ ($s$, $T$)] |
104 | 598 |
reads the string~$s$ using the syntax of~$sign$, creating a certified term. |
599 |
The term is checked to have type~$T$; this type also tells the parser what |
|
600 |
kind of phrase to parse. |
|
601 |
||
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
602 |
\item[\ttindexbold{cert_axm} $sign$ ($name$, $t$)] |
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
603 |
certifies $t$ with respect to $sign$ as a meta-proposition and converts all |
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
604 |
exceptions to an error, including the final message |
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
605 |
\begin{ttbox} |
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
606 |
The error(s) above occurred in axiom "\(name\)" |
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
607 |
\end{ttbox} |
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
608 |
|
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
609 |
\item[\ttindexbold{read_axm} $sign$ ($name$, $s$)] |
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
610 |
similar to {\tt cert_axm}, but first reads the string $s$ using the syntax of |
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
611 |
$sign$. |
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
612 |
|
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
613 |
\item[\ttindexbold{rep_cterm} $ct$] |
104 | 614 |
decomposes $ct$ as a record containing its type, the term itself, its |
615 |
signature, and the maximum subscript of its unknowns. The type and maximum |
|
616 |
subscript are computed during certification. |
|
324 | 617 |
\end{ttdescription} |
104 | 618 |
|
619 |
||
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
620 |
\section{Types}\index{types|bold} |
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
621 |
Types belong to the \ML\ type \mltydx{typ}, which is a concrete datatype with |
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
622 |
three constructor functions. These correspond to type constructors, free |
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
623 |
type variables and schematic type variables. Types are classified by sorts, |
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
624 |
which are lists of classes (representing an intersection). A class is |
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
625 |
represented by a string. |
104 | 626 |
\begin{ttbox} |
627 |
type class = string; |
|
628 |
type sort = class list; |
|
629 |
||
630 |
datatype typ = Type of string * typ list |
|
631 |
| TFree of string * sort |
|
632 |
| TVar of indexname * sort; |
|
633 |
||
634 |
infixr 5 -->; |
|
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
635 |
fun S --> T = Type ("fun", [S, T]); |
104 | 636 |
\end{ttbox} |
324 | 637 |
\begin{ttdescription} |
638 |
\item[\ttindexbold{Type}($a$, $Ts$)] \index{type constructors|bold} |
|
639 |
applies the {\bf type constructor} named~$a$ to the type operands~$Ts$. |
|
640 |
Type constructors include~\tydx{fun}, the binary function space |
|
641 |
constructor, as well as nullary type constructors such as~\tydx{prop}. |
|
642 |
Other type constructors may be introduced. In expressions, but not in |
|
643 |
patterns, \hbox{\tt$S$-->$T$} is a convenient shorthand for function |
|
644 |
types. |
|
104 | 645 |
|
324 | 646 |
\item[\ttindexbold{TFree}($a$, $s$)] \index{type variables|bold} |
647 |
is the {\bf type variable} with name~$a$ and sort~$s$. |
|
104 | 648 |
|
324 | 649 |
\item[\ttindexbold{TVar}($v$, $s$)] \index{type unknowns|bold} |
650 |
is the {\bf type unknown} with indexname~$v$ and sort~$s$. |
|
651 |
Type unknowns are essentially free type variables, but may be |
|
652 |
instantiated during unification. |
|
653 |
\end{ttdescription} |
|
104 | 654 |
|
655 |
||
656 |
\section{Certified types} |
|
657 |
\index{types!certified|bold} |
|
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
658 |
Certified types, which are analogous to certified terms, have type |
275 | 659 |
\ttindexbold{ctyp}. |
104 | 660 |
|
661 |
\subsection{Printing types} |
|
324 | 662 |
\index{types!printing of} |
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
663 |
\begin{ttbox} |
275 | 664 |
string_of_ctyp : ctyp -> string |
104 | 665 |
Sign.string_of_typ : Sign.sg -> typ -> string |
666 |
\end{ttbox} |
|
324 | 667 |
\begin{ttdescription} |
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
668 |
\item[\ttindexbold{string_of_ctyp} $cT$] |
104 | 669 |
displays $cT$ as a string. |
670 |
||
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
671 |
\item[\ttindexbold{Sign.string_of_typ} $sign$ $T$] |
104 | 672 |
displays $T$ as a string, using the syntax of~$sign$. |
324 | 673 |
\end{ttdescription} |
104 | 674 |
|
675 |
||
676 |
\subsection{Making and inspecting certified types} |
|
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
677 |
\begin{ttbox} |
275 | 678 |
ctyp_of : Sign.sg -> typ -> ctyp |
679 |
rep_ctyp : ctyp -> \{T: typ, sign: Sign.sg\} |
|
104 | 680 |
\end{ttbox} |
324 | 681 |
\begin{ttdescription} |
275 | 682 |
\item[\ttindexbold{ctyp_of} $sign$ $T$] \index{signatures} |
104 | 683 |
certifies $T$ with respect to signature~$sign$. |
684 |
||
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
685 |
\item[\ttindexbold{rep_ctyp} $cT$] |
104 | 686 |
decomposes $cT$ as a record containing the type itself and its signature. |
324 | 687 |
\end{ttdescription} |
104 | 688 |
|
689 |
\index{theories|)} |