3 \def\isabellecontext{prelim}%
13 \isacommand{theory}\isamarkupfalse%
14 \ prelim\ \isakeyword{imports}\ base\ \isakeyword{begin}%
22 \isamarkupchapter{Preliminaries%
26 \isamarkupsection{Named entities%
30 \begin{isamarkuptext}%
31 Named entities of different kinds (logical constant, type,
32 type class, theorem, method etc.) live in separate name spaces. It is
33 usually clear from the occurrence of a name which kind of entity it
34 refers to. For example, proof method \isa{foo} vs.\ theorem
35 \isa{foo} vs.\ logical constant \isa{foo} are easily
36 distinguished by means of the syntactic context. A notable exception
37 are logical identifiers within a term (\secref{sec:terms}): constants,
38 fixed variables, and bound variables all share the same identifier
39 syntax, but are distinguished by their scope.
41 Each name space is organized as a collection of \emph{qualified
42 names}, which consist of a sequence of basic name components separated
43 by dots: \isa{Bar{\isachardot}bar{\isachardot}foo}, \isa{Bar{\isachardot}foo}, and \isa{foo}
44 are examples for valid qualified names. Name components are
45 subdivided into \emph{symbols}, which constitute the smallest textual
46 unit in Isabelle --- raw characters are normally not encountered
51 \isamarkupsubsection{Strings of symbols%
55 \begin{isamarkuptext}%
56 Isabelle strings consist of a sequence of
57 symbols\glossary{Symbol}{The smalles unit of text in Isabelle,
58 subsumes plain ASCII characters as well as an infinite collection of
59 named symbols (for greek, math etc.).}, which are either packed as an
60 actual \isa{string}, or represented as a list. Each symbol is in
61 itself a small string of the following form:
65 \item either a singleton ASCII character ``\isa{c}'' (with
66 character code 0--127), for example ``\verb,a,'',
68 \item or a regular symbol ``\verb,\,\verb,<,\isa{ident}\verb,>,'',
69 for example ``\verb,\,\verb,<alpha>,'',
71 \item or a control symbol ``\verb,\,\verb,<^,\isa{ident}\verb,>,'', for example ``\verb,\,\verb,<^bold>,'',
73 \item or a raw control symbol ``\verb,\,\verb,<^raw:,\isa{{\isasymdots}}\verb,>,'' where ``\isa{{\isasymdots}}'' refers to any
74 printable ASCII character (excluding ``\verb,.,'' and ``\verb,>,'') or
75 non-ASCII character, for example ``\verb,\,\verb,<^raw:$\sum_{i = 1}^n$>,'',
77 \item or a numbered raw control symbol ``\verb,\,\verb,<^raw,\isa{nnn}\verb,>, where \isa{nnn} are digits, for example
78 ``\verb,\,\verb,<^raw42>,''.
82 The \isa{ident} syntax for symbol names is \isa{letter\ {\isacharparenleft}letter\ {\isacharbar}\ digit{\isacharparenright}\isactrlsup {\isacharasterisk}}, where \isa{letter\ {\isacharequal}\ A{\isachardot}{\isachardot}Za{\isachardot}{\isachardot}Z} and \isa{digit\ {\isacharequal}\ {\isadigit{0}}{\isachardot}{\isachardot}{\isadigit{9}}}. There are infinitely many regular symbols and
83 control symbols available, but a certain collection of standard
84 symbols is treated specifically. For example,
85 ``\verb,\,\verb,<alpha>,'' is classified as a (non-ASCII) letter,
86 which means it may occur within regular Isabelle identifier syntax.
88 Output of symbols depends on the print mode (\secref{sec:print-mode}).
89 For example, the standard {\LaTeX} setup of the Isabelle document
90 preparation system would present ``\verb,\,\verb,<alpha>,'' as \isa{{\isasymalpha}}, and ``\verb,\,\verb,<^bold>,\verb,\,\verb,<alpha>,'' as \isa{\isactrlbold {\isasymalpha}}.
92 \medskip It is important to note that the character set underlying
93 Isabelle symbols is plain 7-bit ASCII. Since 8-bit characters are
94 passed through transparently, Isabelle may easily process actual
95 Unicode/UCS data (using the well-known UTF-8 encoding, for example).
96 Unicode provides its own collection of mathematical symbols, but there
97 is presently no link to Isabelle's named ones; both kinds of symbols
98 coexist independently.%
108 \begin{isamarkuptext}%
110 \indexmltype{Symbol.symbol}\verb|type Symbol.symbol| \\
111 \indexml{Symbol.explode}\verb|Symbol.explode: string -> Symbol.symbol list| \\
112 \indexml{Symbol.is-letter}\verb|Symbol.is_letter: Symbol.symbol -> bool| \\
113 \indexml{Symbol.is-digit}\verb|Symbol.is_digit: Symbol.symbol -> bool| \\
114 \indexml{Symbol.is-quasi}\verb|Symbol.is_quasi: Symbol.symbol -> bool| \\
115 \indexml{Symbol.is-blank}\verb|Symbol.is_blank: Symbol.symbol -> bool| \\
116 \indexmltype{Symbol.sym}\verb|type Symbol.sym| \\
117 \indexml{Symbol.decode}\verb|Symbol.decode: Symbol.symbol -> Symbol.sym| \\
122 \item \verb|Symbol.symbol| represents Isabelle symbols; this type
123 is merely an alias for \verb|string|, but emphasizes the
124 specific format encountered here.
126 \item \verb|Symbol.explode|~\isa{s} produces an actual symbol
127 list from the packed form usually encountered as user input. This
128 function replaces \verb|String.explode| for virtually all purposes
129 of manipulating text in Isabelle! Plain \isa{implode} may be
130 used for the reverse operation.
132 \item \verb|Symbol.is_letter|, \verb|Symbol.is_digit|, \verb|Symbol.is_quasi|, \verb|Symbol.is_blank| classify certain symbols
133 (both ASCII and several named ones) according to fixed syntactic
134 convections of Isabelle, e.g.\ see \cite{isabelle-isar-ref}.
136 \item \verb|Symbol.sym| is a concrete datatype that represents
137 the different kinds of symbols explicitly as \verb|Symbol.Char|,
138 \verb|Symbol.Sym|, \verb|Symbol.Ctrl|, or \verb|Symbol.Raw|.
140 \item \verb|Symbol.decode| converts the string representation of a
141 symbol into the explicit datatype version.
154 \isamarkupsubsection{Simple names%
158 \begin{isamarkuptext}%
163 \isamarkupsubsection{Qualified names and name spaces%
173 \begin{isamarkuptext}%
174 Qualified names are constructed according to implicit naming
175 principles of the present context.
178 The last component is called \emph{base name}; the remaining prefix of
179 qualification may be empty.
181 Some practical conventions help to organize named entities more
186 \item Names are qualified first by the theory name, second by an
187 optional ``structure''. For example, a constant \isa{c} declared
188 as part of a certain structure \isa{b} (say a type definition) in
189 theory \isa{A} will be named \isa{A{\isachardot}b{\isachardot}c} internally.
201 Names of different kinds of entities are basically independent, but
202 some practical naming conventions relate them to each other. For
203 example, a constant \isa{foo} may be accompanied with theorems
204 \isa{foo{\isachardot}intro}, \isa{foo{\isachardot}elim}, \isa{foo{\isachardot}simps} etc. The
205 same may happen for a type \isa{foo}, which is then apt to cause
206 clashes in the theorem name space! To avoid this, we occasionally
207 follow an additional convention of suffixes that determine the
208 original kind of entity that a name has been derived. For example,
209 constant \isa{foo} is associated with theorem \isa{foo{\isachardot}intro},
210 type \isa{foo} with theorem \isa{foo{\isacharunderscore}type{\isachardot}intro}, and type
211 class \isa{foo} with \isa{foo{\isacharunderscore}class{\isachardot}intro}.%
222 \isamarkupsection{Structured output%
226 \isamarkupsubsection{Pretty printing%
230 \begin{isamarkuptext}%
235 \isamarkupsubsection{Output channels%
239 \begin{isamarkuptext}%
244 \isamarkupsubsection{Print modes%
248 \begin{isamarkuptext}%
253 \isamarkupsection{Contexts \label{sec:context}%
257 \begin{isamarkuptext}%
258 A logical context represents the background that is taken for
259 granted when formulating statements and composing proofs. It acts
260 as a medium to produce formal content, depending on earlier material
261 (declarations, results etc.).
263 In particular, derivations within the primitive Pure logic can be
264 described as a judgment \isa{{\isasymGamma}\ {\isasymturnstile}\isactrlsub {\isasymTheta}\ {\isasymphi}}, meaning that a
265 proposition \isa{{\isasymphi}} is derivable from hypotheses \isa{{\isasymGamma}}
266 within the theory \isa{{\isasymTheta}}. There are logical reasons for
267 keeping \isa{{\isasymTheta}} and \isa{{\isasymGamma}} separate: theories support type
268 constructors and schematic polymorphism of constants and axioms,
269 while the inner calculus of \isa{{\isasymGamma}\ {\isasymturnstile}\ {\isasymphi}} is limited to Simple
270 Type Theory (with fixed type variables in the assumptions).
272 \medskip Contexts and derivations are linked by the following key
277 \item Transfer: monotonicity of derivations admits results to be
278 transferred into a larger context, i.e.\ \isa{{\isasymGamma}\ {\isasymturnstile}\isactrlsub {\isasymTheta}\ {\isasymphi}}
279 implies \isa{{\isasymGamma}{\isacharprime}\ {\isasymturnstile}\isactrlsub {\isasymTheta}\isactrlsub {\isacharprime}\ {\isasymphi}} for contexts \isa{{\isasymTheta}{\isacharprime}\ {\isasymsupseteq}\ {\isasymTheta}} and \isa{{\isasymGamma}{\isacharprime}\ {\isasymsupseteq}\ {\isasymGamma}}.
281 \item Export: discharge of hypotheses admits results to be exported
282 into a smaller context, i.e.\ \isa{{\isasymGamma}{\isacharprime}\ {\isasymturnstile}\isactrlsub {\isasymTheta}\ {\isasymphi}} implies
283 \isa{{\isasymGamma}\ {\isasymturnstile}\isactrlsub {\isasymTheta}\ {\isasymDelta}\ {\isasymLongrightarrow}\ {\isasymphi}} where \isa{{\isasymGamma}{\isacharprime}\ {\isasymsupseteq}\ {\isasymGamma}} and \isa{{\isasymDelta}\ {\isacharequal}\ {\isasymGamma}{\isacharprime}\ {\isacharminus}\ {\isasymGamma}}. Note that \isa{{\isasymTheta}} remains unchanged here, only the
284 \isa{{\isasymGamma}} part is affected.
288 \medskip Isabelle/Isar provides two different notions of abstract
289 containers called \emph{theory context} and \emph{proof context},
290 respectively. These model the main characteristics of the primitive
291 \isa{{\isasymTheta}} and \isa{{\isasymGamma}} above, without subscribing to any
292 particular kind of content yet. Instead, contexts merely impose a
293 certain policy of managing arbitrary \emph{context data}. The
294 system provides strongly typed mechanisms to declare new kinds of
295 data at compile time.
297 Thus the internal bootstrap process of Isabelle/Pure eventually
298 reaches a stage where certain data slots provide the logical content
299 of \isa{{\isasymTheta}} and \isa{{\isasymGamma}} sketched above, but this does not
300 stop there! Various additional data slots support all kinds of
301 mechanisms that are not necessarily part of the core logic.
303 For example, there would be data for canonical introduction and
304 elimination rules for arbitrary operators (depending on the
305 object-logic and application), which enables users to perform
306 standard proof steps implicitly (cf.\ the \isa{rule} method).
308 Isabelle is able to bring forth more and more concepts successively.
309 In particular, an object-logic like Isabelle/HOL continues the
310 Isabelle/Pure setup by adding specific components for automated
311 reasoning (classical reasoner, tableau prover, structured induction
312 etc.) and derived specification mechanisms (inductive predicates,
313 recursive functions etc.). All of this is based on the generic data
314 management by theory and proof contexts.%
318 \isamarkupsubsection{Theory context \label{sec:context-theory}%
322 \begin{isamarkuptext}%
323 Each theory is explicitly named and holds a unique identifier.
324 There is a separate \emph{theory reference} for pointing backwards
325 to the enclosing theory context of derived entities. Theories are
326 related by a (nominal) sub-theory relation, which corresponds to the
327 canonical dependency graph: each theory is derived from a certain
328 sub-graph of ancestor theories. The \isa{merge} of two theories
329 refers to the least upper bound, which actually degenerates into
330 absorption of one theory into the other, due to the nominal
331 sub-theory relation this.
333 The \isa{begin} operation starts a new theory by importing
334 several parent theories and entering a special \isa{draft} mode,
335 which is sustained until the final \isa{end} operation. A draft
336 mode theory acts like a linear type, where updates invalidate
337 earlier drafts, but theory reference values will be propagated
338 automatically. Thus derived entities that ``belong'' to a draft
339 might be transferred spontaneously to a larger context. An
340 invalidated draft is called ``stale''. The \isa{copy} operation
341 produces an auxiliary version with the same data content, but is
342 unrelated to the original: updates of the copy do not affect the
343 original, neither does the sub-theory relation hold.
345 The example below shows a theory graph derived from \isa{Pure}.
346 Theory \isa{Length} imports \isa{Nat} and \isa{List}.
347 The linear draft mode is enabled during the ``\isa{{\isasymdots}}'' stage of
351 \begin{tabular}{rcccl}
355 & $\swarrow$ & & $\searrow$ & \\
356 $Nat$ & & & & $List$ \\
357 & $\searrow$ & & $\swarrow$ \\
359 & & \multicolumn{3}{l}{~~$\isarkeyword{imports}$} \\
360 & & \multicolumn{3}{l}{~~$\isarkeyword{begin}$} \\
362 & & \multicolumn{3}{l}{~~$\isarkeyword{end}$} \\
365 \medskip In practice, derived theory operations mostly operate
366 drafts, namely the body of the current portion of theory that the
367 user happens to be composing.
369 \medskip There is also a builtin theory history mechanism that amends for
370 the destructive behaviour of theory drafts. The \isa{checkpoint} operation produces an intermediate stepping stone that
371 survives the next update unscathed: both the original and the
372 changed theory remain valid and are related by the sub-theory
373 relation. This recovering of pure theory values comes at the cost
374 of extra internal bookeeping. The cumulative effect of
375 checkpointing is purged by the \isa{finish} operation.
377 History operations are usually managed by the system, e.g.\ notably
378 in the Isar transaction loop.
385 \isamarkupsubsection{Proof context \label{sec:context-proof}%
389 \begin{isamarkuptext}%
390 A proof context is an arbitrary container that is initialized from a
391 given theory. The result contains a back-reference to the theory it
392 belongs to, together with pure data. No further bookkeeping is
393 required here, thanks to the lack of destructive features.
395 There is no restriction on producing proof contexts, although the
396 usual discipline is to follow block structure as a mental model: a
397 given context is extended consecutively, results are exported back
398 into the original context. In particular, the concept of Isar proof
399 state models block-structured reasoning explicitly, using a stack of
402 Due to the lack of identification and back-referencing, entities
403 derived in a proof context need to record inherent logical
404 requirements explicitly. For example, hypotheses used in a
405 derivation will be recorded separately within the sequent \isa{{\isasymGamma}\ {\isasymturnstile}\ {\isasymphi}}, just to make double sure. Results could leak into an alien
406 proof context do to programming errors, but Isabelle/Isar
407 occasionally includes extra validity checks at the end of a
413 \glossary{Proof context}{The static context of a structured proof,
414 acts like a local ``theory'' of the current portion of Isar proof
415 text, generalizes the idea of local hypotheses \isa{{\isasymGamma}} in
416 judgments \isa{{\isasymGamma}\ {\isasymturnstile}\ {\isasymphi}} of natural deduction calculi. There is a
417 generic notion of introducing and discharging hypotheses. Arbritrary
418 auxiliary context data may be adjoined.}%
422 \isamarkupsubsection{Generic contexts%
431 \isacommand{end}\isamarkupfalse%
443 %%% TeX-master: "root"