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