wenzelm@145
|
1 |
|
lcp@104
|
2 |
\chapter{Theories, Terms and Types} \label{theories}
|
wenzelm@30184
|
3 |
\index{theories|(}
|
lcp@104
|
4 |
|
wenzelm@6568
|
5 |
\section{The theory loader}\label{sec:more-theories}
|
wenzelm@6568
|
6 |
\index{theories!reading}\index{files!reading}
|
wenzelm@6568
|
7 |
|
wenzelm@6568
|
8 |
Isabelle's theory loader manages dependencies of the internal graph of theory
|
wenzelm@6568
|
9 |
nodes (the \emph{theory database}) and the external view of the file system.
|
wenzelm@6568
|
10 |
See \S\ref{sec:intro-theories} for its most basic commands, such as
|
wenzelm@6568
|
11 |
\texttt{use_thy}. There are a few more operations available.
|
wenzelm@6568
|
12 |
|
wenzelm@864
|
13 |
\begin{ttbox}
|
wenzelm@6568
|
14 |
use_thy_only : string -> unit
|
wenzelm@7136
|
15 |
update_thy_only : string -> unit
|
wenzelm@6568
|
16 |
touch_thy : string -> unit
|
wenzelm@6658
|
17 |
remove_thy : string -> unit
|
paulson@8136
|
18 |
delete_tmpfiles : bool ref \hfill\textbf{initially true}
|
lcp@286
|
19 |
\end{ttbox}
|
nipkow@275
|
20 |
|
lcp@324
|
21 |
\begin{ttdescription}
|
wenzelm@6569
|
22 |
\item[\ttindexbold{use_thy_only} "$name$";] is similar to \texttt{use_thy},
|
wenzelm@6569
|
23 |
but processes the actual theory file $name$\texttt{.thy} only, ignoring
|
wenzelm@6568
|
24 |
$name$\texttt{.ML}. This might be useful in replaying proof scripts by hand
|
wenzelm@6568
|
25 |
from the very beginning, starting with the fresh theory.
|
wenzelm@6568
|
26 |
|
wenzelm@7136
|
27 |
\item[\ttindexbold{update_thy_only} "$name$";] is similar to
|
wenzelm@7136
|
28 |
\texttt{update_thy}, but processes the actual theory file
|
wenzelm@7136
|
29 |
$name$\texttt{.thy} only, ignoring $name$\texttt{.ML}.
|
wenzelm@7136
|
30 |
|
wenzelm@6569
|
31 |
\item[\ttindexbold{touch_thy} "$name$";] marks theory node $name$ of the
|
wenzelm@6568
|
32 |
internal graph as outdated. While the theory remains usable, subsequent
|
wenzelm@6568
|
33 |
operations such as \texttt{use_thy} may cause a reload.
|
wenzelm@6568
|
34 |
|
wenzelm@6658
|
35 |
\item[\ttindexbold{remove_thy} "$name$";] deletes theory node $name$,
|
wenzelm@6658
|
36 |
including \emph{all} of its descendants. Beware! This is a quick way to
|
wenzelm@6658
|
37 |
dispose a large number of theories at once. Note that {\ML} bindings to
|
wenzelm@6658
|
38 |
theorems etc.\ of removed theories may still persist.
|
wenzelm@6658
|
39 |
|
wenzelm@6568
|
40 |
\end{ttdescription}
|
clasohm@138
|
41 |
|
wenzelm@6568
|
42 |
\medskip Theory and {\ML} files are located by skimming through the
|
wenzelm@6568
|
43 |
directories listed in Isabelle's internal load path, which merely contains the
|
wenzelm@6568
|
44 |
current directory ``\texttt{.}'' by default. The load path may be accessed by
|
wenzelm@6568
|
45 |
the following operations.
|
lcp@286
|
46 |
|
wenzelm@864
|
47 |
\begin{ttbox}
|
wenzelm@6568
|
48 |
show_path: unit -> string list
|
wenzelm@6568
|
49 |
add_path: string -> unit
|
wenzelm@6568
|
50 |
del_path: string -> unit
|
wenzelm@6568
|
51 |
reset_path: unit -> unit
|
wenzelm@7440
|
52 |
with_path: string -> ('a -> 'b) -> 'a -> 'b
|
wenzelm@11052
|
53 |
no_document: ('a -> 'b) -> 'a -> 'b
|
lcp@286
|
54 |
\end{ttbox}
|
clasohm@138
|
55 |
|
lcp@324
|
56 |
\begin{ttdescription}
|
wenzelm@6568
|
57 |
\item[\ttindexbold{show_path}();] displays the load path components in
|
wenzelm@6571
|
58 |
canonical string representation (which is always according to Unix rules).
|
wenzelm@6568
|
59 |
|
wenzelm@6569
|
60 |
\item[\ttindexbold{add_path} "$dir$";] adds component $dir$ to the beginning
|
wenzelm@6569
|
61 |
of the load path.
|
wenzelm@6568
|
62 |
|
wenzelm@6569
|
63 |
\item[\ttindexbold{del_path} "$dir$";] removes any occurrences of component
|
wenzelm@6568
|
64 |
$dir$ from the load path.
|
wenzelm@6568
|
65 |
|
wenzelm@6568
|
66 |
\item[\ttindexbold{reset_path}();] resets the load path to ``\texttt{.}''
|
wenzelm@6568
|
67 |
(current directory) only.
|
wenzelm@7440
|
68 |
|
wenzelm@7440
|
69 |
\item[\ttindexbold{with_path} "$dir$" $f$ $x$;] temporarily adds component
|
wenzelm@11052
|
70 |
$dir$ to the beginning of the load path while executing $(f~x)$.
|
wenzelm@11052
|
71 |
|
wenzelm@11052
|
72 |
\item[\ttindexbold{no_document} $f$ $x$;] temporarily disables {\LaTeX}
|
wenzelm@11052
|
73 |
document generation while executing $(f~x)$.
|
wenzelm@7440
|
74 |
|
lcp@324
|
75 |
\end{ttdescription}
|
clasohm@138
|
76 |
|
wenzelm@7440
|
77 |
Furthermore, in operations referring indirectly to some file (e.g.\
|
wenzelm@7440
|
78 |
\texttt{use_dir}) the argument may be prefixed by a directory that will be
|
wenzelm@7440
|
79 |
temporarily appended to the load path, too.
|
lcp@104
|
80 |
|
lcp@104
|
81 |
|
clasohm@866
|
82 |
\section{Basic operations on theories}\label{BasicOperationsOnTheories}
|
wenzelm@4384
|
83 |
|
wenzelm@4384
|
84 |
\subsection{*Theory inclusion}
|
wenzelm@4384
|
85 |
\begin{ttbox}
|
wenzelm@4384
|
86 |
subthy : theory * theory -> bool
|
wenzelm@4384
|
87 |
eq_thy : theory * theory -> bool
|
wenzelm@4384
|
88 |
transfer : theory -> thm -> thm
|
wenzelm@4384
|
89 |
transfer_sg : Sign.sg -> thm -> thm
|
wenzelm@4384
|
90 |
\end{ttbox}
|
wenzelm@4384
|
91 |
|
wenzelm@4384
|
92 |
Inclusion and equality of theories is determined by unique
|
wenzelm@4384
|
93 |
identification stamps that are created when declaring new components.
|
wenzelm@4384
|
94 |
Theorems contain a reference to the theory (actually to its signature)
|
wenzelm@4384
|
95 |
they have been derived in. Transferring theorems to super theories
|
wenzelm@4384
|
96 |
has no logical significance, but may affect some operations in subtle
|
wenzelm@4384
|
97 |
ways (e.g.\ implicit merges of signatures when applying rules, or
|
wenzelm@4384
|
98 |
pretty printing of theorems).
|
wenzelm@4384
|
99 |
|
wenzelm@4384
|
100 |
\begin{ttdescription}
|
wenzelm@4384
|
101 |
|
wenzelm@4384
|
102 |
\item[\ttindexbold{subthy} ($thy@1$, $thy@2$)] determines if $thy@1$
|
wenzelm@4384
|
103 |
is included in $thy@2$ wrt.\ identification stamps.
|
wenzelm@4384
|
104 |
|
wenzelm@4384
|
105 |
\item[\ttindexbold{eq_thy} ($thy@1$, $thy@2$)] determines if $thy@1$
|
wenzelm@4384
|
106 |
is exactly the same as $thy@2$.
|
wenzelm@4384
|
107 |
|
wenzelm@4384
|
108 |
\item[\ttindexbold{transfer} $thy$ $thm$] transfers theorem $thm$ to
|
wenzelm@4384
|
109 |
theory $thy$, provided the latter includes the theory of $thm$.
|
wenzelm@4384
|
110 |
|
wenzelm@4384
|
111 |
\item[\ttindexbold{transfer_sg} $sign$ $thm$] is similar to
|
wenzelm@4384
|
112 |
\texttt{transfer}, but identifies the super theory via its
|
wenzelm@4384
|
113 |
signature.
|
wenzelm@4384
|
114 |
|
wenzelm@4384
|
115 |
\end{ttdescription}
|
wenzelm@4384
|
116 |
|
wenzelm@4384
|
117 |
|
wenzelm@6571
|
118 |
\subsection{*Primitive theories}
|
wenzelm@864
|
119 |
\begin{ttbox}
|
wenzelm@4317
|
120 |
ProtoPure.thy : theory
|
wenzelm@3108
|
121 |
Pure.thy : theory
|
wenzelm@3108
|
122 |
CPure.thy : theory
|
lcp@286
|
123 |
\end{ttbox}
|
wenzelm@3108
|
124 |
\begin{description}
|
wenzelm@4317
|
125 |
\item[\ttindexbold{ProtoPure.thy}, \ttindexbold{Pure.thy},
|
wenzelm@4317
|
126 |
\ttindexbold{CPure.thy}] contain the syntax and signature of the
|
wenzelm@4317
|
127 |
meta-logic. There are basically no axioms: meta-level inferences
|
wenzelm@4317
|
128 |
are carried out by \ML\ functions. \texttt{Pure} and \texttt{CPure}
|
wenzelm@4317
|
129 |
just differ in their concrete syntax of prefix function application:
|
wenzelm@4317
|
130 |
$t(u@1, \ldots, u@n)$ in \texttt{Pure} vs.\ $t\,u@1,\ldots\,u@n$ in
|
wenzelm@4317
|
131 |
\texttt{CPure}. \texttt{ProtoPure} is their common parent,
|
wenzelm@4317
|
132 |
containing no syntax for printing prefix applications at all!
|
wenzelm@6571
|
133 |
|
wenzelm@864
|
134 |
%% FIXME
|
nipkow@478
|
135 |
%\item [\ttindexbold{extend_theory} $thy$ {\tt"}$T${\tt"} $\cdots$] extends
|
nipkow@478
|
136 |
% the theory $thy$ with new types, constants, etc. $T$ identifies the theory
|
nipkow@478
|
137 |
% internally. When a theory is redeclared, say to change an incorrect axiom,
|
nipkow@478
|
138 |
% bindings to the old axiom may persist. Isabelle ensures that the old and
|
nipkow@478
|
139 |
% new theories are not involved in the same proof. Attempting to combine
|
nipkow@478
|
140 |
% different theories having the same name $T$ yields the fatal error
|
nipkow@478
|
141 |
%extend_theory : theory -> string -> \(\cdots\) -> theory
|
wenzelm@864
|
142 |
%\begin{ttbox}
|
wenzelm@864
|
143 |
%Attempt to merge different versions of theory: \(T\)
|
wenzelm@864
|
144 |
%\end{ttbox}
|
wenzelm@3108
|
145 |
\end{description}
|
lcp@286
|
146 |
|
wenzelm@864
|
147 |
%% FIXME
|
nipkow@275
|
148 |
%\item [\ttindexbold{extend_theory} $thy$ {\tt"}$T${\tt"}
|
nipkow@275
|
149 |
% ($classes$, $default$, $types$, $arities$, $consts$, $sextopt$) $rules$]
|
nipkow@275
|
150 |
%\hfill\break %%% include if line is just too short
|
lcp@286
|
151 |
%is the \ML{} equivalent of the following theory definition:
|
nipkow@275
|
152 |
%\begin{ttbox}
|
nipkow@275
|
153 |
%\(T\) = \(thy\) +
|
nipkow@275
|
154 |
%classes \(c\) < \(c@1\),\(\dots\),\(c@m\)
|
nipkow@275
|
155 |
% \dots
|
nipkow@275
|
156 |
%default {\(d@1,\dots,d@r\)}
|
nipkow@275
|
157 |
%types \(tycon@1\),\dots,\(tycon@i\) \(n\)
|
nipkow@275
|
158 |
% \dots
|
nipkow@275
|
159 |
%arities \(tycon@1'\),\dots,\(tycon@j'\) :: (\(s@1\),\dots,\(s@n\))\(c\)
|
nipkow@275
|
160 |
% \dots
|
nipkow@275
|
161 |
%consts \(b@1\),\dots,\(b@k\) :: \(\tau\)
|
nipkow@275
|
162 |
% \dots
|
nipkow@275
|
163 |
%rules \(name\) \(rule\)
|
nipkow@275
|
164 |
% \dots
|
nipkow@275
|
165 |
%end
|
nipkow@275
|
166 |
%\end{ttbox}
|
nipkow@275
|
167 |
%where
|
nipkow@275
|
168 |
%\begin{tabular}[t]{l@{~=~}l}
|
nipkow@275
|
169 |
%$classes$ & \tt[("$c$",["$c@1$",\dots,"$c@m$"]),\dots] \\
|
nipkow@275
|
170 |
%$default$ & \tt["$d@1$",\dots,"$d@r$"]\\
|
nipkow@275
|
171 |
%$types$ & \tt[([$tycon@1$,\dots,$tycon@i$], $n$),\dots] \\
|
nipkow@275
|
172 |
%$arities$ & \tt[([$tycon'@1$,\dots,$tycon'@j$], ([$s@1$,\dots,$s@n$],$c$)),\dots]
|
nipkow@275
|
173 |
%\\
|
nipkow@275
|
174 |
%$consts$ & \tt[([$b@1$,\dots,$b@k$],$\tau$),\dots] \\
|
nipkow@275
|
175 |
%$rules$ & \tt[("$name$",$rule$),\dots]
|
nipkow@275
|
176 |
%\end{tabular}
|
lcp@104
|
177 |
|
lcp@104
|
178 |
|
wenzelm@864
|
179 |
\subsection{Inspecting a theory}\label{sec:inspct-thy}
|
lcp@104
|
180 |
\index{theories!inspecting|bold}
|
wenzelm@864
|
181 |
\begin{ttbox}
|
wenzelm@4317
|
182 |
print_syntax : theory -> unit
|
wenzelm@4317
|
183 |
print_theory : theory -> unit
|
wenzelm@4317
|
184 |
parents_of : theory -> theory list
|
wenzelm@4317
|
185 |
ancestors_of : theory -> theory list
|
wenzelm@4317
|
186 |
sign_of : theory -> Sign.sg
|
wenzelm@4317
|
187 |
Sign.stamp_names_of : Sign.sg -> string list
|
lcp@104
|
188 |
\end{ttbox}
|
wenzelm@864
|
189 |
These provide means of viewing a theory's components.
|
lcp@324
|
190 |
\begin{ttdescription}
|
wenzelm@3108
|
191 |
\item[\ttindexbold{print_syntax} $thy$] prints the syntax of $thy$
|
wenzelm@3108
|
192 |
(grammar, macros, translation functions etc., see
|
wenzelm@3108
|
193 |
page~\pageref{pg:print_syn} for more details).
|
wenzelm@3108
|
194 |
|
wenzelm@3108
|
195 |
\item[\ttindexbold{print_theory} $thy$] prints the logical parts of
|
wenzelm@3108
|
196 |
$thy$, excluding the syntax.
|
wenzelm@4317
|
197 |
|
wenzelm@4317
|
198 |
\item[\ttindexbold{parents_of} $thy$] returns the direct ancestors
|
wenzelm@4317
|
199 |
of~$thy$.
|
wenzelm@4317
|
200 |
|
wenzelm@4317
|
201 |
\item[\ttindexbold{ancestors_of} $thy$] returns all ancestors of~$thy$
|
wenzelm@4317
|
202 |
(not including $thy$ itself).
|
wenzelm@4317
|
203 |
|
wenzelm@4317
|
204 |
\item[\ttindexbold{sign_of} $thy$] returns the signature associated
|
wenzelm@4317
|
205 |
with~$thy$. It is useful with functions like {\tt
|
wenzelm@4317
|
206 |
read_instantiate_sg}, which take a signature as an argument.
|
wenzelm@4317
|
207 |
|
wenzelm@4317
|
208 |
\item[\ttindexbold{Sign.stamp_names_of} $sg$]\index{signatures}
|
wenzelm@4317
|
209 |
returns the names of the identification \rmindex{stamps} of ax
|
wenzelm@4317
|
210 |
signature. These coincide with the names of its full ancestry
|
wenzelm@4317
|
211 |
including that of $sg$ itself.
|
lcp@104
|
212 |
|
lcp@324
|
213 |
\end{ttdescription}
|
lcp@104
|
214 |
|
clasohm@1369
|
215 |
|
berghofe@11623
|
216 |
\section{Terms}\label{sec:terms}
|
lcp@104
|
217 |
\index{terms|bold}
|
lcp@324
|
218 |
Terms belong to the \ML\ type \mltydx{term}, which is a concrete datatype
|
wenzelm@3108
|
219 |
with six constructors:
|
lcp@104
|
220 |
\begin{ttbox}
|
lcp@104
|
221 |
type indexname = string * int;
|
lcp@104
|
222 |
infix 9 $;
|
lcp@104
|
223 |
datatype term = Const of string * typ
|
lcp@104
|
224 |
| Free of string * typ
|
lcp@104
|
225 |
| Var of indexname * typ
|
lcp@104
|
226 |
| Bound of int
|
lcp@104
|
227 |
| Abs of string * typ * term
|
lcp@104
|
228 |
| op $ of term * term;
|
lcp@104
|
229 |
\end{ttbox}
|
lcp@324
|
230 |
\begin{ttdescription}
|
wenzelm@4317
|
231 |
\item[\ttindexbold{Const} ($a$, $T$)] \index{constants|bold}
|
paulson@8136
|
232 |
is the \textbf{constant} with name~$a$ and type~$T$. Constants include
|
lcp@286
|
233 |
connectives like $\land$ and $\forall$ as well as constants like~0
|
lcp@286
|
234 |
and~$Suc$. Other constants may be required to define a logic's concrete
|
wenzelm@864
|
235 |
syntax.
|
lcp@104
|
236 |
|
wenzelm@4317
|
237 |
\item[\ttindexbold{Free} ($a$, $T$)] \index{variables!free|bold}
|
paulson@8136
|
238 |
is the \textbf{free variable} with name~$a$ and type~$T$.
|
lcp@104
|
239 |
|
wenzelm@4317
|
240 |
\item[\ttindexbold{Var} ($v$, $T$)] \index{unknowns|bold}
|
paulson@8136
|
241 |
is the \textbf{scheme variable} with indexname~$v$ and type~$T$. An
|
lcp@324
|
242 |
\mltydx{indexname} is a string paired with a non-negative index, or
|
lcp@324
|
243 |
subscript; a term's scheme variables can be systematically renamed by
|
lcp@324
|
244 |
incrementing their subscripts. Scheme variables are essentially free
|
lcp@324
|
245 |
variables, but may be instantiated during unification.
|
lcp@104
|
246 |
|
lcp@324
|
247 |
\item[\ttindexbold{Bound} $i$] \index{variables!bound|bold}
|
paulson@8136
|
248 |
is the \textbf{bound variable} with de Bruijn index~$i$, which counts the
|
lcp@324
|
249 |
number of lambdas, starting from zero, between a variable's occurrence
|
lcp@324
|
250 |
and its binding. The representation prevents capture of variables. For
|
lcp@324
|
251 |
more information see de Bruijn \cite{debruijn72} or
|
paulson@6592
|
252 |
Paulson~\cite[page~376]{paulson-ml2}.
|
lcp@104
|
253 |
|
wenzelm@4317
|
254 |
\item[\ttindexbold{Abs} ($a$, $T$, $u$)]
|
lcp@324
|
255 |
\index{lambda abs@$\lambda$-abstractions|bold}
|
paulson@8136
|
256 |
is the $\lambda$-\textbf{abstraction} with body~$u$, and whose bound
|
lcp@324
|
257 |
variable has name~$a$ and type~$T$. The name is used only for parsing
|
lcp@324
|
258 |
and printing; it has no logical significance.
|
lcp@104
|
259 |
|
lcp@324
|
260 |
\item[$t$ \$ $u$] \index{$@{\tt\$}|bold} \index{function applications|bold}
|
paulson@8136
|
261 |
is the \textbf{application} of~$t$ to~$u$.
|
lcp@324
|
262 |
\end{ttdescription}
|
wenzelm@9695
|
263 |
Application is written as an infix operator to aid readability. Here is an
|
wenzelm@9695
|
264 |
\ML\ pattern to recognize FOL formulae of the form~$A\imp B$, binding the
|
wenzelm@9695
|
265 |
subformulae to~$A$ and~$B$:
|
wenzelm@864
|
266 |
\begin{ttbox}
|
lcp@104
|
267 |
Const("Trueprop",_) $ (Const("op -->",_) $ A $ B)
|
lcp@104
|
268 |
\end{ttbox}
|
lcp@104
|
269 |
|
lcp@104
|
270 |
|
wenzelm@4317
|
271 |
\section{*Variable binding}
|
lcp@286
|
272 |
\begin{ttbox}
|
lcp@286
|
273 |
loose_bnos : term -> int list
|
lcp@286
|
274 |
incr_boundvars : int -> term -> term
|
lcp@286
|
275 |
abstract_over : term*term -> term
|
lcp@286
|
276 |
variant_abs : string * typ * term -> string * term
|
paulson@8136
|
277 |
aconv : term * term -> bool\hfill\textbf{infix}
|
lcp@286
|
278 |
\end{ttbox}
|
lcp@286
|
279 |
These functions are all concerned with the de Bruijn representation of
|
lcp@286
|
280 |
bound variables.
|
lcp@324
|
281 |
\begin{ttdescription}
|
wenzelm@864
|
282 |
\item[\ttindexbold{loose_bnos} $t$]
|
lcp@286
|
283 |
returns the list of all dangling bound variable references. In
|
paulson@6669
|
284 |
particular, \texttt{Bound~0} is loose unless it is enclosed in an
|
paulson@6669
|
285 |
abstraction. Similarly \texttt{Bound~1} is loose unless it is enclosed in
|
lcp@286
|
286 |
at least two abstractions; if enclosed in just one, the list will contain
|
lcp@286
|
287 |
the number 0. A well-formed term does not contain any loose variables.
|
lcp@286
|
288 |
|
wenzelm@864
|
289 |
\item[\ttindexbold{incr_boundvars} $j$]
|
lcp@332
|
290 |
increases a term's dangling bound variables by the offset~$j$. This is
|
lcp@286
|
291 |
required when moving a subterm into a context where it is enclosed by a
|
lcp@286
|
292 |
different number of abstractions. Bound variables with a matching
|
lcp@286
|
293 |
abstraction are unaffected.
|
lcp@286
|
294 |
|
wenzelm@864
|
295 |
\item[\ttindexbold{abstract_over} $(v,t)$]
|
lcp@286
|
296 |
forms the abstraction of~$t$ over~$v$, which may be any well-formed term.
|
paulson@6669
|
297 |
It replaces every occurrence of \(v\) by a \texttt{Bound} variable with the
|
lcp@286
|
298 |
correct index.
|
lcp@286
|
299 |
|
wenzelm@864
|
300 |
\item[\ttindexbold{variant_abs} $(a,T,u)$]
|
lcp@286
|
301 |
substitutes into $u$, which should be the body of an abstraction.
|
lcp@286
|
302 |
It replaces each occurrence of the outermost bound variable by a free
|
lcp@286
|
303 |
variable. The free variable has type~$T$ and its name is a variant
|
lcp@332
|
304 |
of~$a$ chosen to be distinct from all constants and from all variables
|
lcp@286
|
305 |
free in~$u$.
|
lcp@286
|
306 |
|
wenzelm@864
|
307 |
\item[$t$ \ttindexbold{aconv} $u$]
|
lcp@286
|
308 |
tests whether terms~$t$ and~$u$ are \(\alpha\)-convertible: identical up
|
lcp@286
|
309 |
to renaming of bound variables.
|
lcp@286
|
310 |
\begin{itemize}
|
lcp@286
|
311 |
\item
|
paulson@6669
|
312 |
Two constants, \texttt{Free}s, or \texttt{Var}s are \(\alpha\)-convertible
|
lcp@286
|
313 |
if their names and types are equal.
|
lcp@286
|
314 |
(Variables having the same name but different types are thus distinct.
|
lcp@286
|
315 |
This confusing situation should be avoided!)
|
lcp@286
|
316 |
\item
|
lcp@286
|
317 |
Two bound variables are \(\alpha\)-convertible
|
lcp@286
|
318 |
if they have the same number.
|
lcp@286
|
319 |
\item
|
lcp@286
|
320 |
Two abstractions are \(\alpha\)-convertible
|
lcp@286
|
321 |
if their bodies are, and their bound variables have the same type.
|
lcp@286
|
322 |
\item
|
lcp@286
|
323 |
Two applications are \(\alpha\)-convertible
|
lcp@286
|
324 |
if the corresponding subterms are.
|
lcp@286
|
325 |
\end{itemize}
|
lcp@286
|
326 |
|
lcp@324
|
327 |
\end{ttdescription}
|
lcp@286
|
328 |
|
wenzelm@864
|
329 |
\section{Certified terms}\index{terms!certified|bold}\index{signatures}
|
paulson@8136
|
330 |
A term $t$ can be \textbf{certified} under a signature to ensure that every type
|
wenzelm@864
|
331 |
in~$t$ is well-formed and every constant in~$t$ is a type instance of a
|
wenzelm@864
|
332 |
constant declared in the signature. The term must be well-typed and its use
|
paulson@6669
|
333 |
of bound variables must be well-formed. Meta-rules such as \texttt{forall_elim}
|
wenzelm@864
|
334 |
take certified terms as arguments.
|
lcp@104
|
335 |
|
lcp@324
|
336 |
Certified terms belong to the abstract type \mltydx{cterm}.
|
lcp@104
|
337 |
Elements of the type can only be created through the certification process.
|
lcp@104
|
338 |
In case of error, Isabelle raises exception~\ttindex{TERM}\@.
|
lcp@104
|
339 |
|
lcp@104
|
340 |
\subsection{Printing terms}
|
lcp@324
|
341 |
\index{terms!printing of}
|
wenzelm@864
|
342 |
\begin{ttbox}
|
nipkow@275
|
343 |
string_of_cterm : cterm -> string
|
lcp@104
|
344 |
Sign.string_of_term : Sign.sg -> term -> string
|
lcp@104
|
345 |
\end{ttbox}
|
lcp@324
|
346 |
\begin{ttdescription}
|
wenzelm@864
|
347 |
\item[\ttindexbold{string_of_cterm} $ct$]
|
lcp@104
|
348 |
displays $ct$ as a string.
|
lcp@104
|
349 |
|
wenzelm@864
|
350 |
\item[\ttindexbold{Sign.string_of_term} $sign$ $t$]
|
lcp@104
|
351 |
displays $t$ as a string, using the syntax of~$sign$.
|
lcp@324
|
352 |
\end{ttdescription}
|
lcp@104
|
353 |
|
lcp@104
|
354 |
\subsection{Making and inspecting certified terms}
|
wenzelm@864
|
355 |
\begin{ttbox}
|
paulson@8136
|
356 |
cterm_of : Sign.sg -> term -> cterm
|
paulson@8136
|
357 |
read_cterm : Sign.sg -> string * typ -> cterm
|
paulson@8136
|
358 |
cert_axm : Sign.sg -> string * term -> string * term
|
paulson@8136
|
359 |
read_axm : Sign.sg -> string * string -> string * term
|
paulson@8136
|
360 |
rep_cterm : cterm -> \{T:typ, t:term, sign:Sign.sg, maxidx:int\}
|
wenzelm@4543
|
361 |
Sign.certify_term : Sign.sg -> term -> term * typ * int
|
lcp@104
|
362 |
\end{ttbox}
|
lcp@324
|
363 |
\begin{ttdescription}
|
wenzelm@4543
|
364 |
|
wenzelm@4543
|
365 |
\item[\ttindexbold{cterm_of} $sign$ $t$] \index{signatures} certifies
|
wenzelm@4543
|
366 |
$t$ with respect to signature~$sign$.
|
wenzelm@4543
|
367 |
|
wenzelm@4543
|
368 |
\item[\ttindexbold{read_cterm} $sign$ ($s$, $T$)] reads the string~$s$
|
wenzelm@4543
|
369 |
using the syntax of~$sign$, creating a certified term. The term is
|
wenzelm@4543
|
370 |
checked to have type~$T$; this type also tells the parser what kind
|
wenzelm@4543
|
371 |
of phrase to parse.
|
wenzelm@4543
|
372 |
|
wenzelm@4543
|
373 |
\item[\ttindexbold{cert_axm} $sign$ ($name$, $t$)] certifies $t$ with
|
wenzelm@4543
|
374 |
respect to $sign$ as a meta-proposition and converts all exceptions
|
wenzelm@4543
|
375 |
to an error, including the final message
|
wenzelm@864
|
376 |
\begin{ttbox}
|
wenzelm@864
|
377 |
The error(s) above occurred in axiom "\(name\)"
|
wenzelm@864
|
378 |
\end{ttbox}
|
wenzelm@864
|
379 |
|
wenzelm@4543
|
380 |
\item[\ttindexbold{read_axm} $sign$ ($name$, $s$)] similar to {\tt
|
wenzelm@4543
|
381 |
cert_axm}, but first reads the string $s$ using the syntax of
|
wenzelm@4543
|
382 |
$sign$.
|
wenzelm@4543
|
383 |
|
wenzelm@4543
|
384 |
\item[\ttindexbold{rep_cterm} $ct$] decomposes $ct$ as a record
|
wenzelm@4543
|
385 |
containing its type, the term itself, its signature, and the maximum
|
wenzelm@4543
|
386 |
subscript of its unknowns. The type and maximum subscript are
|
wenzelm@4543
|
387 |
computed during certification.
|
wenzelm@4543
|
388 |
|
wenzelm@4543
|
389 |
\item[\ttindexbold{Sign.certify_term}] is a more primitive version of
|
wenzelm@4543
|
390 |
\texttt{cterm_of}, returning the internal representation instead of
|
wenzelm@4543
|
391 |
an abstract \texttt{cterm}.
|
wenzelm@864
|
392 |
|
lcp@324
|
393 |
\end{ttdescription}
|
lcp@104
|
394 |
|
lcp@104
|
395 |
|
wenzelm@864
|
396 |
\section{Types}\index{types|bold}
|
wenzelm@864
|
397 |
Types belong to the \ML\ type \mltydx{typ}, which is a concrete datatype with
|
wenzelm@864
|
398 |
three constructor functions. These correspond to type constructors, free
|
wenzelm@864
|
399 |
type variables and schematic type variables. Types are classified by sorts,
|
wenzelm@864
|
400 |
which are lists of classes (representing an intersection). A class is
|
wenzelm@864
|
401 |
represented by a string.
|
lcp@104
|
402 |
\begin{ttbox}
|
lcp@104
|
403 |
type class = string;
|
lcp@104
|
404 |
type sort = class list;
|
lcp@104
|
405 |
|
lcp@104
|
406 |
datatype typ = Type of string * typ list
|
lcp@104
|
407 |
| TFree of string * sort
|
lcp@104
|
408 |
| TVar of indexname * sort;
|
lcp@104
|
409 |
|
lcp@104
|
410 |
infixr 5 -->;
|
wenzelm@864
|
411 |
fun S --> T = Type ("fun", [S, T]);
|
lcp@104
|
412 |
\end{ttbox}
|
lcp@324
|
413 |
\begin{ttdescription}
|
wenzelm@4317
|
414 |
\item[\ttindexbold{Type} ($a$, $Ts$)] \index{type constructors|bold}
|
paulson@8136
|
415 |
applies the \textbf{type constructor} named~$a$ to the type operand list~$Ts$.
|
lcp@324
|
416 |
Type constructors include~\tydx{fun}, the binary function space
|
lcp@324
|
417 |
constructor, as well as nullary type constructors such as~\tydx{prop}.
|
lcp@324
|
418 |
Other type constructors may be introduced. In expressions, but not in
|
lcp@324
|
419 |
patterns, \hbox{\tt$S$-->$T$} is a convenient shorthand for function
|
lcp@324
|
420 |
types.
|
lcp@104
|
421 |
|
wenzelm@4317
|
422 |
\item[\ttindexbold{TFree} ($a$, $s$)] \index{type variables|bold}
|
paulson@8136
|
423 |
is the \textbf{type variable} with name~$a$ and sort~$s$.
|
lcp@104
|
424 |
|
wenzelm@4317
|
425 |
\item[\ttindexbold{TVar} ($v$, $s$)] \index{type unknowns|bold}
|
paulson@8136
|
426 |
is the \textbf{type unknown} with indexname~$v$ and sort~$s$.
|
lcp@324
|
427 |
Type unknowns are essentially free type variables, but may be
|
lcp@324
|
428 |
instantiated during unification.
|
lcp@324
|
429 |
\end{ttdescription}
|
lcp@104
|
430 |
|
lcp@104
|
431 |
|
lcp@104
|
432 |
\section{Certified types}
|
lcp@104
|
433 |
\index{types!certified|bold}
|
wenzelm@864
|
434 |
Certified types, which are analogous to certified terms, have type
|
nipkow@275
|
435 |
\ttindexbold{ctyp}.
|
lcp@104
|
436 |
|
lcp@104
|
437 |
\subsection{Printing types}
|
lcp@324
|
438 |
\index{types!printing of}
|
wenzelm@864
|
439 |
\begin{ttbox}
|
nipkow@275
|
440 |
string_of_ctyp : ctyp -> string
|
lcp@104
|
441 |
Sign.string_of_typ : Sign.sg -> typ -> string
|
lcp@104
|
442 |
\end{ttbox}
|
lcp@324
|
443 |
\begin{ttdescription}
|
wenzelm@864
|
444 |
\item[\ttindexbold{string_of_ctyp} $cT$]
|
lcp@104
|
445 |
displays $cT$ as a string.
|
lcp@104
|
446 |
|
wenzelm@864
|
447 |
\item[\ttindexbold{Sign.string_of_typ} $sign$ $T$]
|
lcp@104
|
448 |
displays $T$ as a string, using the syntax of~$sign$.
|
lcp@324
|
449 |
\end{ttdescription}
|
lcp@104
|
450 |
|
lcp@104
|
451 |
|
lcp@104
|
452 |
\subsection{Making and inspecting certified types}
|
wenzelm@864
|
453 |
\begin{ttbox}
|
wenzelm@4543
|
454 |
ctyp_of : Sign.sg -> typ -> ctyp
|
paulson@8136
|
455 |
rep_ctyp : ctyp -> \{T: typ, sign: Sign.sg\}
|
wenzelm@4543
|
456 |
Sign.certify_typ : Sign.sg -> typ -> typ
|
lcp@104
|
457 |
\end{ttbox}
|
lcp@324
|
458 |
\begin{ttdescription}
|
wenzelm@4543
|
459 |
|
wenzelm@4543
|
460 |
\item[\ttindexbold{ctyp_of} $sign$ $T$] \index{signatures} certifies
|
wenzelm@4543
|
461 |
$T$ with respect to signature~$sign$.
|
wenzelm@4543
|
462 |
|
wenzelm@4543
|
463 |
\item[\ttindexbold{rep_ctyp} $cT$] decomposes $cT$ as a record
|
wenzelm@4543
|
464 |
containing the type itself and its signature.
|
wenzelm@4543
|
465 |
|
wenzelm@4543
|
466 |
\item[\ttindexbold{Sign.certify_typ}] is a more primitive version of
|
wenzelm@4543
|
467 |
\texttt{ctyp_of}, returning the internal representation instead of
|
wenzelm@4543
|
468 |
an abstract \texttt{ctyp}.
|
lcp@104
|
469 |
|
lcp@324
|
470 |
\end{ttdescription}
|
lcp@104
|
471 |
|
paulson@1846
|
472 |
|
lcp@104
|
473 |
\index{theories|)}
|
wenzelm@5369
|
474 |
|
wenzelm@5369
|
475 |
|
wenzelm@5369
|
476 |
%%% Local Variables:
|
wenzelm@5369
|
477 |
%%% mode: latex
|
wenzelm@5369
|
478 |
%%% TeX-master: "ref"
|
wenzelm@5369
|
479 |
%%% End:
|