author | wenzelm |
Tue, 25 Jul 2006 23:17:41 +0200 | |
changeset 20205 | 7b2958d3d575 |
parent 18554 | bff7a1466fe4 |
child 20214 | 525f934b438b |
permissions | -rw-r--r-- |
18537 | 1 |
|
2 |
(* $Id$ *) |
|
3 |
||
4 |
theory prelim imports base begin |
|
5 |
||
6 |
chapter {* Preliminaries *} |
|
7 |
||
8 |
section {* Named entities *} |
|
9 |
||
10 |
text {* Named entities of different kinds (logical constant, type, |
|
11 |
type class, theorem, method etc.) live in separate name spaces. It is |
|
12 |
usually clear from the occurrence of a name which kind of entity it |
|
13 |
refers to. For example, proof method @{text "foo"} vs.\ theorem |
|
14 |
@{text "foo"} vs.\ logical constant @{text "foo"} are easily |
|
15 |
distinguished by means of the syntactic context. A notable exception |
|
16 |
are logical identifiers within a term (\secref{sec:terms}): constants, |
|
17 |
fixed variables, and bound variables all share the same identifier |
|
18 |
syntax, but are distinguished by their scope. |
|
19 |
||
20 |
Each name space is organized as a collection of \emph{qualified |
|
21 |
names}, which consist of a sequence of basic name components separated |
|
22 |
by dots: @{text "Bar.bar.foo"}, @{text "Bar.foo"}, and @{text "foo"} |
|
23 |
are examples for valid qualified names. Name components are |
|
24 |
subdivided into \emph{symbols}, which constitute the smallest textual |
|
25 |
unit in Isabelle --- raw characters are normally not encountered |
|
26 |
directly. *} |
|
27 |
||
28 |
||
29 |
subsection {* Strings of symbols *} |
|
30 |
||
31 |
text {* Isabelle strings consist of a sequence of |
|
32 |
symbols\glossary{Symbol}{The smalles unit of text in Isabelle, |
|
33 |
subsumes plain ASCII characters as well as an infinite collection of |
|
34 |
named symbols (for greek, math etc.).}, which are either packed as an |
|
35 |
actual @{text "string"}, or represented as a list. Each symbol is in |
|
36 |
itself a small string of the following form: |
|
37 |
||
38 |
\begin{enumerate} |
|
39 |
||
40 |
\item either a singleton ASCII character ``@{text "c"}'' (with |
|
41 |
character code 0--127), for example ``\verb,a,'', |
|
42 |
||
43 |
\item or a regular symbol ``\verb,\,\verb,<,@{text "ident"}\verb,>,'', |
|
44 |
for example ``\verb,\,\verb,<alpha>,'', |
|
45 |
||
46 |
\item or a control symbol ``\verb,\,\verb,<^,@{text |
|
47 |
"ident"}\verb,>,'', for example ``\verb,\,\verb,<^bold>,'', |
|
48 |
||
49 |
\item or a raw control symbol ``\verb,\,\verb,<^raw:,@{text |
|
20205
7b2958d3d575
raw symbols: disallow dot to avoid confusion in NameSpace.unpack;
wenzelm
parents:
18554
diff
changeset
|
50 |
"\<dots>"}\verb,>,'' where ``@{text "\<dots>"}'' refers to any |
7b2958d3d575
raw symbols: disallow dot to avoid confusion in NameSpace.unpack;
wenzelm
parents:
18554
diff
changeset
|
51 |
printable ASCII character (excluding ``\verb,.,'' and ``\verb,>,'') or |
7b2958d3d575
raw symbols: disallow dot to avoid confusion in NameSpace.unpack;
wenzelm
parents:
18554
diff
changeset
|
52 |
non-ASCII character, for example ``\verb,\,\verb,<^raw:$\sum_{i = |
7b2958d3d575
raw symbols: disallow dot to avoid confusion in NameSpace.unpack;
wenzelm
parents:
18554
diff
changeset
|
53 |
1}^n$>,'', |
18537 | 54 |
|
55 |
\item or a numbered raw control symbol ``\verb,\,\verb,<^raw,@{text |
|
56 |
"nnn"}\verb,>, where @{text "nnn"} are digits, for example |
|
57 |
``\verb,\,\verb,<^raw42>,''. |
|
58 |
||
59 |
\end{enumerate} |
|
60 |
||
61 |
The @{text "ident"} syntax for symbol names is @{text "letter (letter |
|
62 |
| digit)\<^sup>*"}, where @{text "letter = A..Za..Z"} and @{text |
|
63 |
"digit = 0..9"}. There are infinitely many regular symbols and |
|
64 |
control symbols available, but a certain collection of standard |
|
65 |
symbols is treated specifically. For example, |
|
66 |
``\verb,\,\verb,<alpha>,'' is classified as a (non-ASCII) letter, |
|
67 |
which means it may occur within regular Isabelle identifier syntax. |
|
68 |
||
69 |
Output of symbols depends on the print mode (\secref{sec:print-mode}). |
|
70 |
For example, the standard {\LaTeX} setup of the Isabelle document |
|
71 |
preparation system would present ``\verb,\,\verb,<alpha>,'' as @{text |
|
72 |
"\<alpha>"}, and ``\verb,\,\verb,<^bold>,\verb,\,\verb,<alpha>,'' as @{text |
|
73 |
"\<^bold>\<alpha>"}. |
|
74 |
||
75 |
\medskip It is important to note that the character set underlying |
|
76 |
Isabelle symbols is plain 7-bit ASCII. Since 8-bit characters are |
|
77 |
passed through transparently, Isabelle may easily process actual |
|
78 |
Unicode/UCS data (using the well-known UTF-8 encoding, for example). |
|
79 |
Unicode provides its own collection of mathematical symbols, but there |
|
80 |
is presently no link to Isabelle's named ones; both kinds of symbols |
|
81 |
coexist independently. *} |
|
82 |
||
83 |
text %mlref {* |
|
84 |
\begin{mldecls} |
|
85 |
@{index_ML_type "Symbol.symbol"} \\ |
|
86 |
@{index_ML Symbol.explode: "string -> Symbol.symbol list"} \\ |
|
87 |
@{index_ML Symbol.is_letter: "Symbol.symbol -> bool"} \\ |
|
88 |
@{index_ML Symbol.is_digit: "Symbol.symbol -> bool"} \\ |
|
89 |
@{index_ML Symbol.is_quasi: "Symbol.symbol -> bool"} \\ |
|
90 |
@{index_ML Symbol.is_blank: "Symbol.symbol -> bool"} \\ |
|
91 |
@{index_ML_type "Symbol.sym"} \\ |
|
92 |
@{index_ML Symbol.decode: "Symbol.symbol -> Symbol.sym"} \\ |
|
93 |
\end{mldecls} |
|
94 |
||
95 |
\begin{description} |
|
96 |
||
97 |
\item @{ML_type "Symbol.symbol"} represents Isabelle symbols; this type |
|
98 |
is merely an alias for @{ML_type "string"}, but emphasizes the |
|
99 |
specific format encountered here. |
|
100 |
||
101 |
\item @{ML "Symbol.explode"}~@{text "s"} produces an actual symbol |
|
102 |
list from the packed form usually encountered as user input. This |
|
103 |
function replaces @{ML "String.explode"} for virtually all purposes |
|
104 |
of manipulating text in Isabelle! Plain @{text "implode"} may be |
|
105 |
used for the reverse operation. |
|
106 |
||
107 |
\item @{ML "Symbol.is_letter"}, @{ML "Symbol.is_digit"}, @{ML |
|
108 |
"Symbol.is_quasi"}, @{ML "Symbol.is_blank"} classify certain symbols |
|
109 |
(both ASCII and several named ones) according to fixed syntactic |
|
110 |
convections of Isabelle, e.g.\ see \cite{isabelle-isar-ref}. |
|
111 |
||
112 |
\item @{ML_type "Symbol.sym"} is a concrete datatype that represents |
|
113 |
the different kinds of symbols explicitly as @{ML "Symbol.Char"}, |
|
114 |
@{ML "Symbol.Sym"}, @{ML "Symbol.Ctrl"}, or @{ML "Symbol.Raw"}. |
|
115 |
||
116 |
\item @{ML "Symbol.decode"} converts the string representation of a |
|
117 |
symbol into the explicit datatype version. |
|
118 |
||
119 |
\end{description} |
|
120 |
*} |
|
121 |
||
122 |
||
123 |
subsection {* Qualified names and name spaces *} |
|
124 |
||
125 |
text %FIXME {* Qualified names are constructed according to implicit naming |
|
126 |
principles of the present context. |
|
127 |
||
128 |
||
129 |
The last component is called \emph{base name}; the remaining prefix of |
|
130 |
qualification may be empty. |
|
131 |
||
132 |
Some practical conventions help to organize named entities more |
|
133 |
systematically: |
|
134 |
||
135 |
\begin{itemize} |
|
136 |
||
137 |
\item Names are qualified first by the theory name, second by an |
|
138 |
optional ``structure''. For example, a constant @{text "c"} declared |
|
139 |
as part of a certain structure @{text "b"} (say a type definition) in |
|
140 |
theory @{text "A"} will be named @{text "A.b.c"} internally. |
|
141 |
||
142 |
\item |
|
143 |
||
144 |
\item |
|
145 |
||
146 |
\item |
|
147 |
||
148 |
\item |
|
149 |
||
150 |
\end{itemize} |
|
151 |
||
152 |
Names of different kinds of entities are basically independent, but |
|
153 |
some practical naming conventions relate them to each other. For |
|
154 |
example, a constant @{text "foo"} may be accompanied with theorems |
|
155 |
@{text "foo.intro"}, @{text "foo.elim"}, @{text "foo.simps"} etc. The |
|
156 |
same may happen for a type @{text "foo"}, which is then apt to cause |
|
157 |
clashes in the theorem name space! To avoid this, we occasionally |
|
158 |
follow an additional convention of suffixes that determine the |
|
159 |
original kind of entity that a name has been derived. For example, |
|
160 |
constant @{text "foo"} is associated with theorem @{text "foo.intro"}, |
|
161 |
type @{text "foo"} with theorem @{text "foo_type.intro"}, and type |
|
162 |
class @{text "foo"} with @{text "foo_class.intro"}. |
|
163 |
||
164 |
*} |
|
165 |
||
166 |
||
167 |
section {* Structured output *} |
|
168 |
||
169 |
subsection {* Pretty printing *} |
|
170 |
||
171 |
text FIXME |
|
172 |
||
173 |
subsection {* Output channels *} |
|
174 |
||
175 |
text FIXME |
|
176 |
||
177 |
subsection {* Print modes *} |
|
178 |
||
179 |
text FIXME |
|
180 |
||
181 |
||
182 |
section {* Context \label{sec:context} *} |
|
183 |
||
184 |
text %FIXME {* What is a context anyway? A highly advanced |
|
185 |
technological and cultural achievement, which took humanity several |
|
186 |
thousands of years to be develop, is writing with pen-and-paper. Here |
|
187 |
the paper is the context, or medium. It accommodates a certain range |
|
188 |
of different kinds of pens, but also has some inherent limitations. |
|
189 |
For example, carved inscriptions are better done on solid material |
|
190 |
like wood or stone. |
|
191 |
||
192 |
Isabelle/Isar distinguishes two key notions of context: \emph{theory |
|
18554 | 193 |
context} and \emph{proof context}. To motivate this fundamental |
194 |
division consider the very idea of logical reasoning which is about |
|
195 |
judgments $\Gamma \Drv{\Theta} \phi$, where $\Theta$ is the background |
|
196 |
theory with declarations of operators and axioms stating their |
|
197 |
properties, and $\Gamma$ a collection of hypotheses emerging |
|
198 |
temporarily during proof. For example, the rule of |
|
199 |
implication-introduction \[ \infer{\Gamma \Drv{\Theta} A \Imp |
|
200 |
B}{\Gamma, A \Drv{\Theta} B} \] can be read as ``to show $A \Imp B$ we |
|
201 |
may assume $A$ as hypothesis and need to show $B$''. It is |
|
202 |
characteristic that $\Theta$ is unchanged and $\Gamma$ is only |
|
203 |
modified according to some general patterns of ``assuming'' and |
|
204 |
``discharging'' hypotheses. This admits the following abbreviated |
|
205 |
notation, where the fixed $\Theta$ and locally changed $\Gamma$ are |
|
206 |
left implicit: \[ \infer{A \Imp B}{\infer*{B}{[A]}} \] |
|
18537 | 207 |
|
208 |
In some logical traditions (e.g.\ Type Theory) there is a tendency to |
|
209 |
unify all kinds of declarations within a single notion of context. |
|
210 |
This is theoretically very nice, but also more demanding, because |
|
211 |
everything is internalized into the logical calculus itself. |
|
212 |
Isabelle/Pure is a very simple logic, but achieves many practically |
|
213 |
useful concepts by differentiating various basic elements. |
|
214 |
||
215 |
Take polymorphism, for example. Instead of embarking on the |
|
216 |
adventurous enterprise of full higher-order logic with full |
|
217 |
type-quantification and polymorphic entities, Isabelle/Pure merely |
|
218 |
takes a stripped-down version of Church's Simple Type Theory |
|
219 |
\cite{church40}. Then after the tradition of Gordon's HOL |
|
220 |
\cite{mgordon-hol} it is fairly easy to introduce syntactic notions of |
|
221 |
type variables and type-constructors, and require every theory |
|
222 |
$\Theta$ being closed by type instantiation. Whenever we wish to |
|
223 |
reason with a polymorphic constant or axiom scheme at a particular |
|
224 |
type, we may assume that it has been referenced initially at that very |
|
225 |
instance (due to the Deduction Theorem). Thus we achieve the |
|
226 |
following \emph{admissible |
|
227 |
rule}\glossary{Admissible rule}{FIXME} of schematic type-instantiation: |
|
228 |
||
229 |
\[ |
|
230 |
\infer{\phi(\tau)}{\infer*{\phi(\alpha)}{[\alpha]}} |
|
231 |
\] |
|
232 |
||
233 |
Using this approach, the structured Isar proof language offers |
|
234 |
schematic polymorphism within nested sub-proofs -- similar to that of |
|
235 |
polymorphic let-bindings according to Hindley-Milner.\ |
|
236 |
\cite{milner78}. All of this is achieved without disintegrating the |
|
237 |
rather simplistic logical core. On the other hand, the succinct rule |
|
238 |
presented above already involves rather delicate interaction of the |
|
239 |
theory and proof context (with side-conditions not mentioned here), |
|
240 |
and unwinding an admissible rule involves induction over derivations. |
|
241 |
All of this diversity needs to be accomodated by the system |
|
242 |
architecture and actual implementation. |
|
243 |
||
244 |
\medskip Despite these important observations, Isabelle/Isar is not just a |
|
245 |
logical calculus, there are further extra-logical aspects to be considered. |
|
246 |
Practical experience over the years suggests two context data structures which |
|
247 |
are used in rather dissimilar manners, even though there is a considerable |
|
248 |
overlap of underlying ideas. |
|
249 |
||
250 |
From the system's perspective the mode of use of theory vs.\ proof context is |
|
251 |
the key distinction. The actual content is merely a generic slot for |
|
252 |
\emph{theory data} and \emph{proof data}, respectively. There are generic |
|
253 |
interfaces to declare data entries at any time. Even the core logic of |
|
254 |
Isabelle/Pure registers its very own notion of theory context data (types, |
|
255 |
constants, axioms etc.) like any other Isabelle tool out there. Likewise, the |
|
256 |
essentials of Isar proof contexts are one proof data slot among many others, |
|
257 |
notably those of derived Isar concepts (e.g.\ calculational reasoning rules). |
|
258 |
||
259 |
In that respect, a theory is more like a stone tablet to carve long-lasting |
|
260 |
inscriptions -- but take care not to break it! While a proof context is like |
|
261 |
a block of paper to scribble and dispose quickly. More recently Isabelle has |
|
262 |
started to cultivate the paper-based craftsmanship a bit further, by |
|
263 |
maintaining small collections of paper booklets, better known as locales. |
|
264 |
||
265 |
Thus we achive ``thick'' augmented versions of {\boldmath$\Theta$} and |
|
266 |
{\boldmath$\Gamma$} to support realistic structured reasoning within a |
|
267 |
practically usable system. |
|
268 |
*} |
|
269 |
||
270 |
||
271 |
subsection {* Theory context \label{sec:context-theory} *} |
|
272 |
||
273 |
text %FIXME {* A theory context consists of management information plus the |
|
274 |
actual data, which may be declared by other software modules later on. |
|
275 |
The management part is surprisingly complex, we illustrate it by the |
|
276 |
following typical situation of incremental theory development. |
|
277 |
||
278 |
\begin{tabular}{rcccl} |
|
279 |
& & $Pure$ \\ |
|
280 |
& & $\downarrow$ \\ |
|
281 |
& & $FOL$ \\ |
|
282 |
& $\swarrow$ & & $\searrow$ & \\ |
|
283 |
$Nat$ & & & & $List$ \\ |
|
284 |
& $\searrow$ & & $\swarrow$ \\ |
|
285 |
& & $Length$ \\ |
|
286 |
& & \multicolumn{3}{l}{~~$\isarkeyword{imports}$} \\ |
|
287 |
& & \multicolumn{3}{l}{~~$\isarkeyword{begin}$} \\ |
|
288 |
& & $\vdots$~~ \\ |
|
289 |
& & $\bullet$~~ \\ |
|
290 |
& & $\vdots$~~ \\ |
|
291 |
& & $\bullet$~~ \\ |
|
292 |
& & $\vdots$~~ \\ |
|
293 |
& & \multicolumn{3}{l}{~~$\isarkeyword{end}$} \\ |
|
294 |
\end{tabular} |
|
295 |
||
296 |
\begin{itemize} |
|
297 |
\item \emph{name}, \emph{parents} and \emph{ancestors} |
|
298 |
\item \emph{identity} |
|
299 |
\item \emph{intermediate versions} |
|
300 |
\end{itemize} |
|
301 |
||
302 |
\begin{description} |
|
303 |
\item [draft] |
|
304 |
\item [intermediate] |
|
305 |
\item [finished] |
|
306 |
\end{description} |
|
307 |
||
308 |
\emph{theory reference} |
|
309 |
*} |
|
310 |
||
311 |
||
312 |
subsection {* Proof context \label{sec:context-proof} *} |
|
313 |
||
314 |
text {* |
|
315 |
FIXME |
|
316 |
||
317 |
\glossary{Proof context}{The static context of a structured proof, |
|
318 |
acts like a local ``theory'' of the current portion of Isar proof |
|
319 |
text, generalizes the idea of local hypotheses @{text "\<Gamma>"} in |
|
320 |
judgments @{text "\<Gamma> \<turnstile> \<phi>"} of natural deduction calculi. There is a |
|
321 |
generic notion of introducing and discharging hypotheses. Arbritrary |
|
322 |
auxiliary context data may be adjoined.} |
|
323 |
||
324 |
*} |
|
325 |
||
326 |
end |