author | wenzelm |
Mon, 03 May 1999 18:35:48 +0200 | |
changeset 6568 | b38bc78d9a9d |
parent 5390 | 0c9e6d860485 |
child 6569 | 66c941ea1f01 |
permissions | -rw-r--r-- |
3201 | 1 |
|
104 | 2 |
%% $Id$ |
145 | 3 |
|
104 | 4 |
\chapter{Theories, Terms and Types} \label{theories} |
5 |
\index{theories|(}\index{signatures|bold} |
|
3108 | 6 |
\index{reading!axioms|see{{\tt assume_ax}}} Theories organize the |
7 |
syntax, declarations and axioms of a mathematical development. They |
|
8 |
are built, starting from the {\Pure} or {\CPure} theory, by extending |
|
9 |
and merging existing theories. They have the \ML\ type |
|
10 |
\mltydx{theory}. Theory operations signal errors by raising exception |
|
11 |
\xdx{THEORY}, returning a message and a list of theories. |
|
104 | 12 |
|
13 |
Signatures, which contain information about sorts, types, constants and |
|
332 | 14 |
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
|
15 |
signature carries a unique list of \bfindex{stamps}, which are \ML\ |
324 | 16 |
references to strings. The strings serve as human-readable names; the |
104 | 17 |
references serve as unique identifiers. Each primitive signature has a |
18 |
single stamp. When two signatures are merged, their lists of stamps are |
|
19 |
also merged. Every theory carries a unique signature. |
|
20 |
||
21 |
Terms and types are the underlying representation of logical syntax. Their |
|
275 | 22 |
\ML\ definitions are irrelevant to naive Isabelle users. Programmers who |
23 |
wish to extend Isabelle may need to know such details, say to code a tactic |
|
24 |
that looks for subgoals of a particular form. Terms and types may be |
|
104 | 25 |
`certified' to be well-formed with respect to a given signature. |
26 |
||
324 | 27 |
|
28 |
\section{Defining theories}\label{sec:ref-defining-theories} |
|
104 | 29 |
|
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
30 |
Theories are usually defined using theory definition files (which have a name |
3485
f27a30a18a17
Now there are TWO spaces after each full stop, so that the Emacs sentence
paulson
parents:
3201
diff
changeset
|
31 |
suffix {\tt .thy}). There is also a low level interface provided by certain |
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
32 |
\ML{} functions (see \S\ref{BuildingATheory}). |
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
33 |
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
|
34 |
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
|
35 |
\begin{description} |
6568 | 36 |
\item[{\it theoryDef}] is the full definition. The new theory is called $id$. |
37 |
It is the union of the named {\bf parent |
|
3108 | 38 |
theories}\indexbold{theories!parent}, possibly extended with new |
6568 | 39 |
components. \thydx{Pure} and \thydx{CPure} are the basic theories, which |
40 |
contain only the meta-logic. They differ just in their concrete syntax for |
|
41 |
function applications. |
|
324 | 42 |
|
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
43 |
\item[$classes$] |
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
44 |
is a series of class declarations. Declaring {\tt$id$ < $id@1$ \dots\ |
324 | 45 |
$id@n$} makes $id$ a subclass of the existing classes $id@1\dots |
46 |
id@n$. This rules out cyclic class structures. Isabelle automatically |
|
47 |
computes the transitive closure of subclass hierarchies; it is not |
|
48 |
necessary to declare {\tt c < e} in addition to {\tt c < d} and {\tt d < |
|
49 |
e}. |
|
50 |
||
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
51 |
\item[$default$] |
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
52 |
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
|
53 |
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
|
54 |
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
|
55 |
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
|
56 |
intersection). |
3108 | 57 |
|
58 |
\item[$sort$] is a finite set of classes. A single class $id$ |
|
59 |
abbreviates the sort $\ttlbrace id\ttrbrace$. |
|
324 | 60 |
|
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
61 |
\item[$types$] |
324 | 62 |
is a series of type declarations. Each declares a new type constructor |
63 |
or type synonym. An $n$-place type constructor is specified by |
|
64 |
$(\alpha@1,\dots,\alpha@n)name$, where the type variables serve only to |
|
65 |
indicate the number~$n$. |
|
66 |
||
332 | 67 |
A {\bf type synonym}\indexbold{type synonyms} is an abbreviation |
1387 | 68 |
$(\alpha@1,\dots,\alpha@n)name = \tau$, where $name$ and $\tau$ can |
69 |
be strings. |
|
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
70 |
|
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
71 |
\item[$infix$] |
324 | 72 |
declares a type or constant to be an infix operator of priority $nat$ |
3485
f27a30a18a17
Now there are TWO spaces after each full stop, so that the Emacs sentence
paulson
parents:
3201
diff
changeset
|
73 |
associating to the left ({\tt infixl}) or right ({\tt infixr}). Only |
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
74 |
2-place type constructors can have infix status; an example is {\tt |
3108 | 75 |
('a,'b)~"*"~(infixr~20)}, which may express binary product types. |
324 | 76 |
|
3108 | 77 |
\item[$arities$] is a series of type arity declarations. Each assigns |
78 |
arities to type constructors. The $name$ must be an existing type |
|
79 |
constructor, which is given the additional arity $arity$. |
|
80 |
||
5369 | 81 |
\item[$nonterminals$]\index{*nonterminal symbols} declares purely |
82 |
syntactic types to be used as nonterminal symbols of the context |
|
83 |
free grammar. |
|
84 |
||
3108 | 85 |
\item[$consts$] is a series of constant declarations. Each new |
86 |
constant $name$ is given the specified type. The optional $mixfix$ |
|
87 |
annotations may attach concrete syntax to the constant. |
|
88 |
||
89 |
\item[$syntax$] \index{*syntax section}\index{print mode} is a variant |
|
90 |
of $consts$ which adds just syntax without actually declaring |
|
91 |
logical constants. This gives full control over a theory's context |
|
3485
f27a30a18a17
Now there are TWO spaces after each full stop, so that the Emacs sentence
paulson
parents:
3201
diff
changeset
|
92 |
free grammar. The optional $mode$ specifies the print mode where the |
f27a30a18a17
Now there are TWO spaces after each full stop, so that the Emacs sentence
paulson
parents:
3201
diff
changeset
|
93 |
mixfix productions should be added. If there is no \texttt{output} |
3108 | 94 |
option given, all productions are also added to the input syntax |
95 |
(regardless of the print mode). |
|
324 | 96 |
|
97 |
\item[$mixfix$] \index{mixfix declarations} |
|
98 |
annotations can take three forms: |
|
273 | 99 |
\begin{itemize} |
100 |
\item A mixfix template given as a $string$ of the form |
|
101 |
{\tt"}\dots{\tt\_}\dots{\tt\_}\dots{\tt"} where the $i$-th underscore |
|
324 | 102 |
indicates the position where the $i$-th argument should go. The list |
103 |
of numbers gives the priority of each argument. The final number gives |
|
104 |
the priority of the whole construct. |
|
104 | 105 |
|
324 | 106 |
\item A constant $f$ of type $\tau@1\To(\tau@2\To\tau)$ can be given {\bf |
107 |
infix} status. |
|
104 | 108 |
|
324 | 109 |
\item A constant $f$ of type $(\tau@1\To\tau@2)\To\tau$ can be given {\bf |
110 |
binder} status. The declaration {\tt binder} $\cal Q$ $p$ causes |
|
286 | 111 |
${\cal Q}\,x.F(x)$ to be treated |
112 |
like $f(F)$, where $p$ is the priority. |
|
273 | 113 |
\end{itemize} |
324 | 114 |
|
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
115 |
\item[$trans$] |
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
116 |
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
|
117 |
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
|
118 |
==}). |
324 | 119 |
|
1650 | 120 |
\item[$rules$] |
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
121 |
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
|
122 |
given by the $string$. Rule names must be distinct within any single |
3108 | 123 |
theory. |
324 | 124 |
|
1905 | 125 |
\item[$defs$] is a series of definitions. They are just like $rules$, except |
126 |
that every $string$ must be a definition (see below for details). |
|
1650 | 127 |
|
128 |
\item[$constdefs$] combines the declaration of constants and their |
|
3485
f27a30a18a17
Now there are TWO spaces after each full stop, so that the Emacs sentence
paulson
parents:
3201
diff
changeset
|
129 |
definition. The first $string$ is the type, the second the definition. |
3108 | 130 |
|
131 |
\item[$axclass$] \index{*axclass section} defines an |
|
132 |
\rmindex{axiomatic type class} as the intersection of existing |
|
3485
f27a30a18a17
Now there are TWO spaces after each full stop, so that the Emacs sentence
paulson
parents:
3201
diff
changeset
|
133 |
classes, with additional axioms holding. Class axioms may not |
f27a30a18a17
Now there are TWO spaces after each full stop, so that the Emacs sentence
paulson
parents:
3201
diff
changeset
|
134 |
contain more than one type variable. The class axioms (with implicit |
3108 | 135 |
sort constraints added) are bound to the given names. Furthermore a |
136 |
class introduction rule is generated, which is automatically |
|
137 |
employed by $instance$ to prove instantiations of this class. |
|
138 |
||
139 |
\item[$instance$] \index{*instance section} proves class inclusions or |
|
140 |
type arities at the logical level and then transfers these to the |
|
3485
f27a30a18a17
Now there are TWO spaces after each full stop, so that the Emacs sentence
paulson
parents:
3201
diff
changeset
|
141 |
type signature. The instantiation is proven and checked properly. |
3108 | 142 |
The user has to supply sufficient witness information: theorems |
143 |
($longident$), axioms ($string$), or even arbitrary \ML{} tactic |
|
144 |
code $verbatim$. |
|
1650 | 145 |
|
1846 | 146 |
\item[$oracle$] links the theory to a trusted external reasoner. It is |
147 |
allowed to create theorems, but each theorem carries a proof object |
|
148 |
describing the oracle invocation. See \S\ref{sec:oracles} for details. |
|
4543 | 149 |
|
5369 | 150 |
\item[$local$, $global$] change the current name declaration mode. |
4543 | 151 |
Initially, theories start in $local$ mode, causing all names of |
152 |
types, constants, axioms etc.\ to be automatically qualified by the |
|
153 |
theory name. Changing this to $global$ causes all names to be |
|
154 |
declared as short base names only. |
|
155 |
||
156 |
The $local$ and $global$ declarations act like switches, affecting |
|
157 |
all following theory sections until changed again explicitly. Also |
|
158 |
note that the final state at the end of the theory will persist. In |
|
159 |
particular, this determines how the names of theorems stored later |
|
160 |
on are handled. |
|
5369 | 161 |
|
162 |
\item[$setup$]\index{*setup!theory} applies a list of ML functions to |
|
163 |
the theory. The argument should denote a value of type |
|
164 |
\texttt{(theory -> theory) list}. Typically, ML packages are |
|
165 |
initialized in this way. |
|
1846 | 166 |
|
324 | 167 |
\item[$ml$] \index{*ML section} |
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
168 |
consists of \ML\ code, typically for parse and print translation functions. |
104 | 169 |
\end{description} |
324 | 170 |
% |
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
171 |
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
|
172 |
declarations, translation rules and the {\tt ML} section in more detail. |
145 | 173 |
|
174 |
||
1905 | 175 |
\subsection{Definitions}\indexbold{definitions} |
176 |
||
3485
f27a30a18a17
Now there are TWO spaces after each full stop, so that the Emacs sentence
paulson
parents:
3201
diff
changeset
|
177 |
{\bf Definitions} are intended to express abbreviations. The simplest |
3108 | 178 |
form of a definition is $f \equiv t$, where $f$ is a constant. |
179 |
Isabelle also allows a derived forms where the arguments of~$f$ appear |
|
180 |
on the left, abbreviating a string of $\lambda$-abstractions. |
|
1905 | 181 |
|
182 |
Isabelle makes the following checks on definitions: |
|
183 |
\begin{itemize} |
|
3108 | 184 |
\item Arguments (on the left-hand side) must be distinct variables. |
1905 | 185 |
\item All variables on the right-hand side must also appear on the left-hand |
186 |
side. |
|
3108 | 187 |
\item All type variables on the right-hand side must also appear on |
188 |
the left-hand side; this prohibits definitions such as {\tt |
|
189 |
(zero::nat) == length ([]::'a list)}. |
|
1905 | 190 |
\item The definition must not be recursive. Most object-logics provide |
191 |
definitional principles that can be used to express recursion safely. |
|
192 |
\end{itemize} |
|
193 |
These checks are intended to catch the sort of errors that might be made |
|
194 |
accidentally. Misspellings, for instance, might result in additional |
|
195 |
variables appearing on the right-hand side. More elaborate checks could be |
|
196 |
made, but the cost might be overly strict rules on declaration order, etc. |
|
197 |
||
198 |
||
275 | 199 |
\subsection{*Classes and arities} |
324 | 200 |
\index{classes!context conditions}\index{arities!context conditions} |
145 | 201 |
|
286 | 202 |
In order to guarantee principal types~\cite{nipkow-prehofer}, |
324 | 203 |
arity declarations must obey two conditions: |
145 | 204 |
\begin{itemize} |
3108 | 205 |
\item There must not be any two declarations $ty :: (\vec{r})c$ and |
206 |
$ty :: (\vec{s})c$ with $\vec{r} \neq \vec{s}$. For example, this |
|
207 |
excludes the following: |
|
145 | 208 |
\begin{ttbox} |
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
209 |
arities |
3108 | 210 |
foo :: ({\ttlbrace}logic{\ttrbrace}) logic |
211 |
foo :: ({\ttlbrace}{\ttrbrace})logic |
|
145 | 212 |
\end{ttbox} |
286 | 213 |
|
145 | 214 |
\item If there are two declarations $ty :: (s@1,\dots,s@n)c$ and $ty :: |
215 |
(s@1',\dots,s@n')c'$ such that $c' < c$ then $s@i' \preceq s@i$ must hold |
|
216 |
for $i=1,\dots,n$. The relationship $\preceq$, defined as |
|
217 |
\[ s' \preceq s \iff \forall c\in s. \exists c'\in s'.~ c'\le c, \] |
|
3108 | 218 |
expresses that the set of types represented by $s'$ is a subset of the |
219 |
set of types represented by $s$. Assuming $term \preceq logic$, the |
|
220 |
following is forbidden: |
|
145 | 221 |
\begin{ttbox} |
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
222 |
arities |
3108 | 223 |
foo :: ({\ttlbrace}logic{\ttrbrace})logic |
224 |
foo :: ({\ttlbrace}{\ttrbrace})term |
|
145 | 225 |
\end{ttbox} |
286 | 226 |
|
145 | 227 |
\end{itemize} |
228 |
||
104 | 229 |
|
6568 | 230 |
\section{The theory loader}\label{sec:more-theories} |
231 |
\index{theories!reading}\index{files!reading} |
|
232 |
||
233 |
Isabelle's theory loader manages dependencies of the internal graph of theory |
|
234 |
nodes (the \emph{theory database}) and the external view of the file system. |
|
235 |
See \S\ref{sec:intro-theories} for its most basic commands, such as |
|
236 |
\texttt{use_thy}. There are a few more operations available. |
|
237 |
||
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
238 |
\begin{ttbox} |
6568 | 239 |
use_thy_only : string -> unit |
240 |
update_thy : string -> unit |
|
241 |
touch_thy : string -> unit |
|
286 | 242 |
delete_tmpfiles : bool ref \hfill{\bf initially true} |
243 |
\end{ttbox} |
|
244 |
||
324 | 245 |
\begin{ttdescription} |
6568 | 246 |
\item[\ttindexbold{use_thy_only} $name$;] is similar to \texttt{use_thy}, but |
247 |
processes the actual theory file $name$\texttt{.thy} only, ignoring |
|
248 |
$name$\texttt{.ML}. This might be useful in replaying proof scripts by hand |
|
249 |
from the very beginning, starting with the fresh theory. |
|
250 |
||
251 |
\item[\ttindexbold{update_thy} $name$;] is similar to \texttt{use_thy}, but |
|
252 |
ensures that theory $name$ is fully up-to-date with respect to the file |
|
253 |
system --- apart from $name$ itself its parents may be reloaded as well. |
|
254 |
||
255 |
\item[\ttindexbold{touch_thy} $name$;] marks theory node $name$ of the |
|
256 |
internal graph as outdated. While the theory remains usable, subsequent |
|
257 |
operations such as \texttt{use_thy} may cause a reload. |
|
258 |
||
259 |
\item[reset \ttindexbold{delete_tmpfiles};] processing theory files usually |
|
260 |
involves temporary {\ML} files to be created. By default, these are deleted |
|
261 |
afterwards. Resetting the \texttt{delete_tmpfiles} flag inhibits this, |
|
262 |
leaving the generated code for debugging purposes. The basic location for |
|
263 |
temporary files is determined by the \texttt{ISABELLE_TMP} environment |
|
264 |
variable, which is private to the running Isabelle process (it may be |
|
265 |
retrieved by \ttindex{getenv} from {\ML}). |
|
324 | 266 |
\end{ttdescription} |
138
9ba8bff1addc
added chapter "Defining Theories" and made changes for new Readthy functions
clasohm
parents:
104
diff
changeset
|
267 |
|
6568 | 268 |
\medskip Theory and {\ML} files are located by skimming through the |
269 |
directories listed in Isabelle's internal load path, which merely contains the |
|
270 |
current directory ``\texttt{.}'' by default. The load path may be accessed by |
|
271 |
the following operations. |
|
332 | 272 |
|
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
273 |
\begin{ttbox} |
6568 | 274 |
show_path: unit -> string list |
275 |
add_path: string -> unit |
|
276 |
del_path: string -> unit |
|
277 |
reset_path: unit -> unit |
|
286 | 278 |
\end{ttbox} |
279 |
||
324 | 280 |
\begin{ttdescription} |
6568 | 281 |
\item[\ttindexbold{show_path}();] displays the load path components in |
282 |
canonical string representation, which is always according to Unix rules. |
|
283 |
||
284 |
\item[\ttindexbold{add_path} $dir$;] adds component $dir$ to the beginning of |
|
285 |
the load path. |
|
286 |
||
287 |
\item[\ttindexbold{del_path} $dir$;] removes any occurrences of component |
|
288 |
$dir$ from the load path. |
|
289 |
||
290 |
\item[\ttindexbold{reset_path}();] resets the load path to ``\texttt{.}'' |
|
291 |
(current directory) only. |
|
324 | 292 |
\end{ttdescription} |
286 | 293 |
|
6568 | 294 |
In operations referring indirectly to some file, such as |
295 |
\texttt{use_thy}~$name$, the argument may be prefixed by some directory that |
|
296 |
will be used as temporary load path. Note that, depending on which parts of |
|
297 |
the ancestry of $name$ are already loaded, the dynamic change of paths might |
|
298 |
be hard to predict. Use this feature with care only. |
|
104 | 299 |
|
300 |
||
866
2d3d020eef11
added documentation of bind_thm, qed, qed_goal, get_thm, thms_of
clasohm
parents:
864
diff
changeset
|
301 |
\section{Basic operations on theories}\label{BasicOperationsOnTheories} |
4384 | 302 |
|
303 |
\subsection{*Theory inclusion} |
|
304 |
\begin{ttbox} |
|
305 |
subthy : theory * theory -> bool |
|
306 |
eq_thy : theory * theory -> bool |
|
307 |
transfer : theory -> thm -> thm |
|
308 |
transfer_sg : Sign.sg -> thm -> thm |
|
309 |
\end{ttbox} |
|
310 |
||
311 |
Inclusion and equality of theories is determined by unique |
|
312 |
identification stamps that are created when declaring new components. |
|
313 |
Theorems contain a reference to the theory (actually to its signature) |
|
314 |
they have been derived in. Transferring theorems to super theories |
|
315 |
has no logical significance, but may affect some operations in subtle |
|
316 |
ways (e.g.\ implicit merges of signatures when applying rules, or |
|
317 |
pretty printing of theorems). |
|
318 |
||
319 |
\begin{ttdescription} |
|
320 |
||
321 |
\item[\ttindexbold{subthy} ($thy@1$, $thy@2$)] determines if $thy@1$ |
|
322 |
is included in $thy@2$ wrt.\ identification stamps. |
|
323 |
||
324 |
\item[\ttindexbold{eq_thy} ($thy@1$, $thy@2$)] determines if $thy@1$ |
|
325 |
is exactly the same as $thy@2$. |
|
326 |
||
327 |
\item[\ttindexbold{transfer} $thy$ $thm$] transfers theorem $thm$ to |
|
328 |
theory $thy$, provided the latter includes the theory of $thm$. |
|
329 |
||
330 |
\item[\ttindexbold{transfer_sg} $sign$ $thm$] is similar to |
|
331 |
\texttt{transfer}, but identifies the super theory via its |
|
332 |
signature. |
|
333 |
||
334 |
\end{ttdescription} |
|
335 |
||
336 |
||
3108 | 337 |
\subsection{*Building a theory} |
286 | 338 |
\label{BuildingATheory} |
339 |
\index{theories!constructing|bold} |
|
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
340 |
\begin{ttbox} |
4317 | 341 |
ProtoPure.thy : theory |
3108 | 342 |
Pure.thy : theory |
343 |
CPure.thy : theory |
|
4317 | 344 |
merge_theories : string -> theory * theory -> theory |
286 | 345 |
\end{ttbox} |
3108 | 346 |
\begin{description} |
4317 | 347 |
\item[\ttindexbold{ProtoPure.thy}, \ttindexbold{Pure.thy}, |
348 |
\ttindexbold{CPure.thy}] contain the syntax and signature of the |
|
349 |
meta-logic. There are basically no axioms: meta-level inferences |
|
350 |
are carried out by \ML\ functions. \texttt{Pure} and \texttt{CPure} |
|
351 |
just differ in their concrete syntax of prefix function application: |
|
352 |
$t(u@1, \ldots, u@n)$ in \texttt{Pure} vs.\ $t\,u@1,\ldots\,u@n$ in |
|
353 |
\texttt{CPure}. \texttt{ProtoPure} is their common parent, |
|
354 |
containing no syntax for printing prefix applications at all! |
|
355 |
||
356 |
\item[\ttindexbold{merge_theories} $name$ ($thy@1$, $thy@2$)] merges |
|
357 |
the two theories $thy@1$ and $thy@2$, creating a new named theory |
|
358 |
node. The resulting theory contains all of the syntax, signature |
|
359 |
and axioms of the constituent theories. Merging theories that |
|
360 |
contain different identification stamps of the same name fails with |
|
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
361 |
the following message |
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
362 |
\begin{ttbox} |
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
363 |
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
|
364 |
\end{ttbox} |
4317 | 365 |
This error may especially occur when a theory is redeclared --- say to |
366 |
change an inappropriate definition --- and bindings to old versions |
|
367 |
persist. Isabelle ensures that old and new theories of the same name |
|
368 |
are not involved in a proof. |
|
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
369 |
|
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
370 |
%% FIXME |
478 | 371 |
%\item [\ttindexbold{extend_theory} $thy$ {\tt"}$T${\tt"} $\cdots$] extends |
372 |
% the theory $thy$ with new types, constants, etc. $T$ identifies the theory |
|
373 |
% internally. When a theory is redeclared, say to change an incorrect axiom, |
|
374 |
% bindings to the old axiom may persist. Isabelle ensures that the old and |
|
375 |
% new theories are not involved in the same proof. Attempting to combine |
|
376 |
% different theories having the same name $T$ yields the fatal error |
|
377 |
%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
|
378 |
%\begin{ttbox} |
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
379 |
%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
|
380 |
%\end{ttbox} |
3108 | 381 |
\end{description} |
286 | 382 |
|
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
383 |
%% FIXME |
275 | 384 |
%\item [\ttindexbold{extend_theory} $thy$ {\tt"}$T${\tt"} |
385 |
% ($classes$, $default$, $types$, $arities$, $consts$, $sextopt$) $rules$] |
|
386 |
%\hfill\break %%% include if line is just too short |
|
286 | 387 |
%is the \ML{} equivalent of the following theory definition: |
275 | 388 |
%\begin{ttbox} |
389 |
%\(T\) = \(thy\) + |
|
390 |
%classes \(c\) < \(c@1\),\(\dots\),\(c@m\) |
|
391 |
% \dots |
|
392 |
%default {\(d@1,\dots,d@r\)} |
|
393 |
%types \(tycon@1\),\dots,\(tycon@i\) \(n\) |
|
394 |
% \dots |
|
395 |
%arities \(tycon@1'\),\dots,\(tycon@j'\) :: (\(s@1\),\dots,\(s@n\))\(c\) |
|
396 |
% \dots |
|
397 |
%consts \(b@1\),\dots,\(b@k\) :: \(\tau\) |
|
398 |
% \dots |
|
399 |
%rules \(name\) \(rule\) |
|
400 |
% \dots |
|
401 |
%end |
|
402 |
%\end{ttbox} |
|
403 |
%where |
|
404 |
%\begin{tabular}[t]{l@{~=~}l} |
|
405 |
%$classes$ & \tt[("$c$",["$c@1$",\dots,"$c@m$"]),\dots] \\ |
|
406 |
%$default$ & \tt["$d@1$",\dots,"$d@r$"]\\ |
|
407 |
%$types$ & \tt[([$tycon@1$,\dots,$tycon@i$], $n$),\dots] \\ |
|
408 |
%$arities$ & \tt[([$tycon'@1$,\dots,$tycon'@j$], ([$s@1$,\dots,$s@n$],$c$)),\dots] |
|
409 |
%\\ |
|
410 |
%$consts$ & \tt[([$b@1$,\dots,$b@k$],$\tau$),\dots] \\ |
|
411 |
%$rules$ & \tt[("$name$",$rule$),\dots] |
|
412 |
%\end{tabular} |
|
104 | 413 |
|
414 |
||
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
415 |
\subsection{Inspecting a theory}\label{sec:inspct-thy} |
104 | 416 |
\index{theories!inspecting|bold} |
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
417 |
\begin{ttbox} |
4317 | 418 |
print_syntax : theory -> unit |
419 |
print_theory : theory -> unit |
|
420 |
parents_of : theory -> theory list |
|
421 |
ancestors_of : theory -> theory list |
|
422 |
sign_of : theory -> Sign.sg |
|
423 |
Sign.stamp_names_of : Sign.sg -> string list |
|
104 | 424 |
\end{ttbox} |
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
425 |
These provide means of viewing a theory's components. |
324 | 426 |
\begin{ttdescription} |
3108 | 427 |
\item[\ttindexbold{print_syntax} $thy$] prints the syntax of $thy$ |
428 |
(grammar, macros, translation functions etc., see |
|
429 |
page~\pageref{pg:print_syn} for more details). |
|
430 |
||
431 |
\item[\ttindexbold{print_theory} $thy$] prints the logical parts of |
|
432 |
$thy$, excluding the syntax. |
|
4317 | 433 |
|
434 |
\item[\ttindexbold{parents_of} $thy$] returns the direct ancestors |
|
435 |
of~$thy$. |
|
436 |
||
437 |
\item[\ttindexbold{ancestors_of} $thy$] returns all ancestors of~$thy$ |
|
438 |
(not including $thy$ itself). |
|
439 |
||
440 |
\item[\ttindexbold{sign_of} $thy$] returns the signature associated |
|
441 |
with~$thy$. It is useful with functions like {\tt |
|
442 |
read_instantiate_sg}, which take a signature as an argument. |
|
443 |
||
444 |
\item[\ttindexbold{Sign.stamp_names_of} $sg$]\index{signatures} |
|
445 |
returns the names of the identification \rmindex{stamps} of ax |
|
446 |
signature. These coincide with the names of its full ancestry |
|
447 |
including that of $sg$ itself. |
|
104 | 448 |
|
324 | 449 |
\end{ttdescription} |
104 | 450 |
|
1369 | 451 |
|
104 | 452 |
\section{Terms} |
453 |
\index{terms|bold} |
|
324 | 454 |
Terms belong to the \ML\ type \mltydx{term}, which is a concrete datatype |
3108 | 455 |
with six constructors: |
104 | 456 |
\begin{ttbox} |
457 |
type indexname = string * int; |
|
458 |
infix 9 $; |
|
459 |
datatype term = Const of string * typ |
|
460 |
| Free of string * typ |
|
461 |
| Var of indexname * typ |
|
462 |
| Bound of int |
|
463 |
| Abs of string * typ * term |
|
464 |
| op $ of term * term; |
|
465 |
\end{ttbox} |
|
324 | 466 |
\begin{ttdescription} |
4317 | 467 |
\item[\ttindexbold{Const} ($a$, $T$)] \index{constants|bold} |
286 | 468 |
is the {\bf constant} with name~$a$ and type~$T$. Constants include |
469 |
connectives like $\land$ and $\forall$ as well as constants like~0 |
|
470 |
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
|
471 |
syntax. |
104 | 472 |
|
4317 | 473 |
\item[\ttindexbold{Free} ($a$, $T$)] \index{variables!free|bold} |
324 | 474 |
is the {\bf free variable} with name~$a$ and type~$T$. |
104 | 475 |
|
4317 | 476 |
\item[\ttindexbold{Var} ($v$, $T$)] \index{unknowns|bold} |
324 | 477 |
is the {\bf scheme variable} with indexname~$v$ and type~$T$. An |
478 |
\mltydx{indexname} is a string paired with a non-negative index, or |
|
479 |
subscript; a term's scheme variables can be systematically renamed by |
|
480 |
incrementing their subscripts. Scheme variables are essentially free |
|
481 |
variables, but may be instantiated during unification. |
|
104 | 482 |
|
324 | 483 |
\item[\ttindexbold{Bound} $i$] \index{variables!bound|bold} |
484 |
is the {\bf bound variable} with de Bruijn index~$i$, which counts the |
|
485 |
number of lambdas, starting from zero, between a variable's occurrence |
|
486 |
and its binding. The representation prevents capture of variables. For |
|
487 |
more information see de Bruijn \cite{debruijn72} or |
|
488 |
Paulson~\cite[page~336]{paulson91}. |
|
104 | 489 |
|
4317 | 490 |
\item[\ttindexbold{Abs} ($a$, $T$, $u$)] |
324 | 491 |
\index{lambda abs@$\lambda$-abstractions|bold} |
492 |
is the $\lambda$-{\bf abstraction} with body~$u$, and whose bound |
|
493 |
variable has name~$a$ and type~$T$. The name is used only for parsing |
|
494 |
and printing; it has no logical significance. |
|
104 | 495 |
|
324 | 496 |
\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
|
497 |
is the {\bf application} of~$t$ to~$u$. |
324 | 498 |
\end{ttdescription} |
286 | 499 |
Application is written as an infix operator to aid readability. |
332 | 500 |
Here is an \ML\ pattern to recognize \FOL{} formulae of |
104 | 501 |
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
|
502 |
\begin{ttbox} |
104 | 503 |
Const("Trueprop",_) $ (Const("op -->",_) $ A $ B) |
504 |
\end{ttbox} |
|
505 |
||
506 |
||
4317 | 507 |
\section{*Variable binding} |
286 | 508 |
\begin{ttbox} |
509 |
loose_bnos : term -> int list |
|
510 |
incr_boundvars : int -> term -> term |
|
511 |
abstract_over : term*term -> term |
|
512 |
variant_abs : string * typ * term -> string * term |
|
4374 | 513 |
aconv : term * term -> bool\hfill{\bf infix} |
286 | 514 |
\end{ttbox} |
515 |
These functions are all concerned with the de Bruijn representation of |
|
516 |
bound variables. |
|
324 | 517 |
\begin{ttdescription} |
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
518 |
\item[\ttindexbold{loose_bnos} $t$] |
286 | 519 |
returns the list of all dangling bound variable references. In |
520 |
particular, {\tt Bound~0} is loose unless it is enclosed in an |
|
521 |
abstraction. Similarly {\tt Bound~1} is loose unless it is enclosed in |
|
522 |
at least two abstractions; if enclosed in just one, the list will contain |
|
523 |
the number 0. A well-formed term does not contain any loose variables. |
|
524 |
||
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
525 |
\item[\ttindexbold{incr_boundvars} $j$] |
332 | 526 |
increases a term's dangling bound variables by the offset~$j$. This is |
286 | 527 |
required when moving a subterm into a context where it is enclosed by a |
528 |
different number of abstractions. Bound variables with a matching |
|
529 |
abstraction are unaffected. |
|
530 |
||
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
531 |
\item[\ttindexbold{abstract_over} $(v,t)$] |
286 | 532 |
forms the abstraction of~$t$ over~$v$, which may be any well-formed term. |
533 |
It replaces every occurrence of \(v\) by a {\tt Bound} variable with the |
|
534 |
correct index. |
|
535 |
||
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
536 |
\item[\ttindexbold{variant_abs} $(a,T,u)$] |
286 | 537 |
substitutes into $u$, which should be the body of an abstraction. |
538 |
It replaces each occurrence of the outermost bound variable by a free |
|
539 |
variable. The free variable has type~$T$ and its name is a variant |
|
332 | 540 |
of~$a$ chosen to be distinct from all constants and from all variables |
286 | 541 |
free in~$u$. |
542 |
||
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
543 |
\item[$t$ \ttindexbold{aconv} $u$] |
286 | 544 |
tests whether terms~$t$ and~$u$ are \(\alpha\)-convertible: identical up |
545 |
to renaming of bound variables. |
|
546 |
\begin{itemize} |
|
547 |
\item |
|
548 |
Two constants, {\tt Free}s, or {\tt Var}s are \(\alpha\)-convertible |
|
549 |
if their names and types are equal. |
|
550 |
(Variables having the same name but different types are thus distinct. |
|
551 |
This confusing situation should be avoided!) |
|
552 |
\item |
|
553 |
Two bound variables are \(\alpha\)-convertible |
|
554 |
if they have the same number. |
|
555 |
\item |
|
556 |
Two abstractions are \(\alpha\)-convertible |
|
557 |
if their bodies are, and their bound variables have the same type. |
|
558 |
\item |
|
559 |
Two applications are \(\alpha\)-convertible |
|
560 |
if the corresponding subterms are. |
|
561 |
\end{itemize} |
|
562 |
||
324 | 563 |
\end{ttdescription} |
286 | 564 |
|
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
565 |
\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
|
566 |
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
|
567 |
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
|
568 |
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
|
569 |
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
|
570 |
take certified terms as arguments. |
104 | 571 |
|
324 | 572 |
Certified terms belong to the abstract type \mltydx{cterm}. |
104 | 573 |
Elements of the type can only be created through the certification process. |
574 |
In case of error, Isabelle raises exception~\ttindex{TERM}\@. |
|
575 |
||
576 |
\subsection{Printing terms} |
|
324 | 577 |
\index{terms!printing of} |
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
578 |
\begin{ttbox} |
275 | 579 |
string_of_cterm : cterm -> string |
104 | 580 |
Sign.string_of_term : Sign.sg -> term -> string |
581 |
\end{ttbox} |
|
324 | 582 |
\begin{ttdescription} |
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
583 |
\item[\ttindexbold{string_of_cterm} $ct$] |
104 | 584 |
displays $ct$ as a string. |
585 |
||
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
586 |
\item[\ttindexbold{Sign.string_of_term} $sign$ $t$] |
104 | 587 |
displays $t$ as a string, using the syntax of~$sign$. |
324 | 588 |
\end{ttdescription} |
104 | 589 |
|
590 |
\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
|
591 |
\begin{ttbox} |
4543 | 592 |
cterm_of : Sign.sg -> term -> cterm |
593 |
read_cterm : Sign.sg -> string * typ -> cterm |
|
594 |
cert_axm : Sign.sg -> string * term -> string * term |
|
595 |
read_axm : Sign.sg -> string * string -> string * term |
|
596 |
rep_cterm : cterm -> {\ttlbrace}T:typ, t:term, sign:Sign.sg, maxidx:int\ttrbrace |
|
597 |
Sign.certify_term : Sign.sg -> term -> term * typ * int |
|
104 | 598 |
\end{ttbox} |
324 | 599 |
\begin{ttdescription} |
4543 | 600 |
|
601 |
\item[\ttindexbold{cterm_of} $sign$ $t$] \index{signatures} certifies |
|
602 |
$t$ with respect to signature~$sign$. |
|
603 |
||
604 |
\item[\ttindexbold{read_cterm} $sign$ ($s$, $T$)] reads the string~$s$ |
|
605 |
using the syntax of~$sign$, creating a certified term. The term is |
|
606 |
checked to have type~$T$; this type also tells the parser what kind |
|
607 |
of phrase to parse. |
|
608 |
||
609 |
\item[\ttindexbold{cert_axm} $sign$ ($name$, $t$)] certifies $t$ with |
|
610 |
respect to $sign$ as a meta-proposition and converts all exceptions |
|
611 |
to an error, including the final message |
|
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
612 |
\begin{ttbox} |
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
613 |
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
|
614 |
\end{ttbox} |
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
615 |
|
4543 | 616 |
\item[\ttindexbold{read_axm} $sign$ ($name$, $s$)] similar to {\tt |
617 |
cert_axm}, but first reads the string $s$ using the syntax of |
|
618 |
$sign$. |
|
619 |
||
620 |
\item[\ttindexbold{rep_cterm} $ct$] decomposes $ct$ as a record |
|
621 |
containing its type, the term itself, its signature, and the maximum |
|
622 |
subscript of its unknowns. The type and maximum subscript are |
|
623 |
computed during certification. |
|
624 |
||
625 |
\item[\ttindexbold{Sign.certify_term}] is a more primitive version of |
|
626 |
\texttt{cterm_of}, returning the internal representation instead of |
|
627 |
an abstract \texttt{cterm}. |
|
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
628 |
|
324 | 629 |
\end{ttdescription} |
104 | 630 |
|
631 |
||
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
632 |
\section{Types}\index{types|bold} |
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
633 |
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
|
634 |
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
|
635 |
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
|
636 |
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
|
637 |
represented by a string. |
104 | 638 |
\begin{ttbox} |
639 |
type class = string; |
|
640 |
type sort = class list; |
|
641 |
||
642 |
datatype typ = Type of string * typ list |
|
643 |
| TFree of string * sort |
|
644 |
| TVar of indexname * sort; |
|
645 |
||
646 |
infixr 5 -->; |
|
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
647 |
fun S --> T = Type ("fun", [S, T]); |
104 | 648 |
\end{ttbox} |
324 | 649 |
\begin{ttdescription} |
4317 | 650 |
\item[\ttindexbold{Type} ($a$, $Ts$)] \index{type constructors|bold} |
324 | 651 |
applies the {\bf type constructor} named~$a$ to the type operands~$Ts$. |
652 |
Type constructors include~\tydx{fun}, the binary function space |
|
653 |
constructor, as well as nullary type constructors such as~\tydx{prop}. |
|
654 |
Other type constructors may be introduced. In expressions, but not in |
|
655 |
patterns, \hbox{\tt$S$-->$T$} is a convenient shorthand for function |
|
656 |
types. |
|
104 | 657 |
|
4317 | 658 |
\item[\ttindexbold{TFree} ($a$, $s$)] \index{type variables|bold} |
324 | 659 |
is the {\bf type variable} with name~$a$ and sort~$s$. |
104 | 660 |
|
4317 | 661 |
\item[\ttindexbold{TVar} ($v$, $s$)] \index{type unknowns|bold} |
324 | 662 |
is the {\bf type unknown} with indexname~$v$ and sort~$s$. |
663 |
Type unknowns are essentially free type variables, but may be |
|
664 |
instantiated during unification. |
|
665 |
\end{ttdescription} |
|
104 | 666 |
|
667 |
||
668 |
\section{Certified types} |
|
669 |
\index{types!certified|bold} |
|
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
670 |
Certified types, which are analogous to certified terms, have type |
275 | 671 |
\ttindexbold{ctyp}. |
104 | 672 |
|
673 |
\subsection{Printing types} |
|
324 | 674 |
\index{types!printing of} |
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
675 |
\begin{ttbox} |
275 | 676 |
string_of_ctyp : ctyp -> string |
104 | 677 |
Sign.string_of_typ : Sign.sg -> typ -> string |
678 |
\end{ttbox} |
|
324 | 679 |
\begin{ttdescription} |
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
680 |
\item[\ttindexbold{string_of_ctyp} $cT$] |
104 | 681 |
displays $cT$ as a string. |
682 |
||
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
478
diff
changeset
|
683 |
\item[\ttindexbold{Sign.string_of_typ} $sign$ $T$] |
104 | 684 |
displays $T$ as a string, using the syntax of~$sign$. |
324 | 685 |
\end{ttdescription} |
104 | 686 |
|
687 |
||
688 |
\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
|
689 |
\begin{ttbox} |
4543 | 690 |
ctyp_of : Sign.sg -> typ -> ctyp |
691 |
rep_ctyp : ctyp -> {\ttlbrace}T: typ, sign: Sign.sg\ttrbrace |
|
692 |
Sign.certify_typ : Sign.sg -> typ -> typ |
|
104 | 693 |
\end{ttbox} |
324 | 694 |
\begin{ttdescription} |
4543 | 695 |
|
696 |
\item[\ttindexbold{ctyp_of} $sign$ $T$] \index{signatures} certifies |
|
697 |
$T$ with respect to signature~$sign$. |
|
698 |
||
699 |
\item[\ttindexbold{rep_ctyp} $cT$] decomposes $cT$ as a record |
|
700 |
containing the type itself and its signature. |
|
701 |
||
702 |
\item[\ttindexbold{Sign.certify_typ}] is a more primitive version of |
|
703 |
\texttt{ctyp_of}, returning the internal representation instead of |
|
704 |
an abstract \texttt{ctyp}. |
|
104 | 705 |
|
324 | 706 |
\end{ttdescription} |
104 | 707 |
|
1846 | 708 |
|
4317 | 709 |
\section{Oracles: calling trusted external reasoners} |
1846 | 710 |
\label{sec:oracles} |
711 |
\index{oracles|(} |
|
712 |
||
713 |
Oracles allow Isabelle to take advantage of external reasoners such as |
|
714 |
arithmetic decision procedures, model checkers, fast tautology checkers or |
|
715 |
computer algebra systems. Invoked as an oracle, an external reasoner can |
|
716 |
create arbitrary Isabelle theorems. It is your responsibility to ensure that |
|
717 |
the external reasoner is as trustworthy as your application requires. |
|
718 |
Isabelle's proof objects~(\S\ref{sec:proofObjects}) record how each theorem |
|
719 |
depends upon oracle calls. |
|
720 |
||
721 |
\begin{ttbox} |
|
4317 | 722 |
invoke_oracle : theory -> xstring -> Sign.sg * object -> thm |
4597
a0bdee64194c
Fixed a lot of overfull and underfull lines (hboxes)
paulson
parents:
4543
diff
changeset
|
723 |
Theory.add_oracle : bstring * (Sign.sg * object -> term) -> theory |
a0bdee64194c
Fixed a lot of overfull and underfull lines (hboxes)
paulson
parents:
4543
diff
changeset
|
724 |
-> theory |
1846 | 725 |
\end{ttbox} |
726 |
\begin{ttdescription} |
|
4317 | 727 |
\item[\ttindexbold{invoke_oracle} $thy$ $name$ ($sign$, $data$)] |
728 |
invokes the oracle $name$ of theory $thy$ passing the information |
|
729 |
contained in the exception value $data$ and creating a theorem |
|
730 |
having signature $sign$. Note that type \ttindex{object} is just an |
|
731 |
abbreviation for \texttt{exn}. Errors arise if $thy$ does not have |
|
732 |
an oracle called $name$, if the oracle rejects its arguments or if |
|
733 |
its result is ill-typed. |
|
734 |
||
735 |
\item[\ttindexbold{Theory.add_oracle} $name$ $fun$ $thy$] extends |
|
736 |
$thy$ by oracle $fun$ called $name$. It is seldom called |
|
737 |
explicitly, as there is concrete syntax for oracles in theory files. |
|
1846 | 738 |
\end{ttdescription} |
739 |
||
740 |
A curious feature of {\ML} exceptions is that they are ordinary constructors. |
|
741 |
The {\ML} type {\tt exn} is a datatype that can be extended at any time. (See |
|
742 |
my {\em {ML} for the Working Programmer}~\cite{paulson-ml2}, especially |
|
743 |
page~136.) The oracle mechanism takes advantage of this to allow an oracle to |
|
744 |
take any information whatever. |
|
745 |
||
746 |
There must be some way of invoking the external reasoner from \ML, either |
|
747 |
because it is coded in {\ML} or via an operating system interface. Isabelle |
|
748 |
expects the {\ML} function to take two arguments: a signature and an |
|
4317 | 749 |
exception object. |
1846 | 750 |
\begin{itemize} |
751 |
\item The signature will typically be that of a desendant of the theory |
|
752 |
declaring the oracle. The oracle will use it to distinguish constants from |
|
753 |
variables, etc., and it will be attached to the generated theorems. |
|
754 |
||
755 |
\item The exception is used to pass arbitrary information to the oracle. This |
|
756 |
information must contain a full description of the problem to be solved by |
|
757 |
the external reasoner, including any additional information that might be |
|
758 |
required. The oracle may raise the exception to indicate that it cannot |
|
759 |
solve the specified problem. |
|
760 |
\end{itemize} |
|
761 |
||
4317 | 762 |
A trivial example is provided in theory {\tt FOL/ex/IffOracle}. This |
763 |
oracle generates tautologies of the form $P\bimp\cdots\bimp P$, with |
|
764 |
an even number of $P$s. |
|
1846 | 765 |
|
4317 | 766 |
The \texttt{ML} section of \texttt{IffOracle.thy} begins by declaring |
767 |
a few auxiliary functions (suppressed below) for creating the |
|
768 |
tautologies. Then it declares a new exception constructor for the |
|
769 |
information required by the oracle: here, just an integer. It finally |
|
770 |
defines the oracle function itself. |
|
1846 | 771 |
\begin{ttbox} |
4317 | 772 |
exception IffOracleExn of int;\medskip |
773 |
fun mk_iff_oracle (sign, IffOracleExn n) = |
|
774 |
if n > 0 andalso n mod 2 = 0 |
|
775 |
then Trueprop $ mk_iff n |
|
776 |
else raise IffOracleExn n; |
|
1846 | 777 |
\end{ttbox} |
4317 | 778 |
Observe the function's two arguments, the signature {\tt sign} and the |
779 |
exception given as a pattern. The function checks its argument for |
|
780 |
validity. If $n$ is positive and even then it creates a tautology |
|
781 |
containing $n$ occurrences of~$P$. Otherwise it signals error by |
|
782 |
raising its own exception (just by happy coincidence). Errors may be |
|
783 |
signalled by other means, such as returning the theorem {\tt True}. |
|
784 |
Please ensure that the oracle's result is correctly typed; Isabelle |
|
785 |
will reject ill-typed theorems by raising a cryptic exception at top |
|
786 |
level. |
|
1846 | 787 |
|
4317 | 788 |
The \texttt{oracle} section of {\tt IffOracle.thy} installs above |
789 |
\texttt{ML} function as follows: |
|
1846 | 790 |
\begin{ttbox} |
4317 | 791 |
IffOracle = FOL +\medskip |
792 |
oracle |
|
793 |
iff = mk_iff_oracle\medskip |
|
1846 | 794 |
end |
795 |
\end{ttbox} |
|
796 |
||
4317 | 797 |
Now in \texttt{IffOracle.ML} we first define a wrapper for invoking |
798 |
the oracle: |
|
1846 | 799 |
\begin{ttbox} |
4597
a0bdee64194c
Fixed a lot of overfull and underfull lines (hboxes)
paulson
parents:
4543
diff
changeset
|
800 |
fun iff_oracle n = invoke_oracle IffOracle.thy "iff" |
a0bdee64194c
Fixed a lot of overfull and underfull lines (hboxes)
paulson
parents:
4543
diff
changeset
|
801 |
(sign_of IffOracle.thy, IffOracleExn n); |
4317 | 802 |
\end{ttbox} |
803 |
||
804 |
Here are some example applications of the \texttt{iff} oracle. An |
|
805 |
argument of 10 is allowed, but one of 5 is forbidden: |
|
806 |
\begin{ttbox} |
|
807 |
iff_oracle 10; |
|
1846 | 808 |
{\out "P <-> P <-> P <-> P <-> P <-> P <-> P <-> P <-> P <-> P" : thm} |
4317 | 809 |
iff_oracle 5; |
1846 | 810 |
{\out Exception- IffOracleExn 5 raised} |
811 |
\end{ttbox} |
|
812 |
||
813 |
\index{oracles|)} |
|
104 | 814 |
\index{theories|)} |
5369 | 815 |
|
816 |
||
817 |
%%% Local Variables: |
|
818 |
%%% mode: latex |
|
819 |
%%% TeX-master: "ref" |
|
820 |
%%% End: |