3 \def\isabellecontext{Prelim}%
10 \isacommand{theory}\isamarkupfalse%
12 \isakeyword{imports}\ Base\isanewline
21 \isamarkupchapter{Preliminaries%
25 \isamarkupsection{Contexts \label{sec:context}%
29 \begin{isamarkuptext}%
30 A logical context represents the background that is required for
31 formulating statements and composing proofs. It acts as a medium to
32 produce formal content, depending on earlier material (declarations,
35 For example, derivations within the Isabelle/Pure logic can be
36 described as a judgment \isa{{\isasymGamma}\ {\isasymturnstile}\isactrlsub {\isasymTheta}\ {\isasymphi}}, which means that a
37 proposition \isa{{\isasymphi}} is derivable from hypotheses \isa{{\isasymGamma}}
38 within the theory \isa{{\isasymTheta}}. There are logical reasons for
39 keeping \isa{{\isasymTheta}} and \isa{{\isasymGamma}} separate: theories can be
40 liberal about supporting type constructors and schematic
41 polymorphism of constants and axioms, while the inner calculus of
42 \isa{{\isasymGamma}\ {\isasymturnstile}\ {\isasymphi}} is strictly limited to Simple Type Theory (with
43 fixed type variables in the assumptions).
45 \medskip Contexts and derivations are linked by the following key
50 \item Transfer: monotonicity of derivations admits results to be
51 transferred into a \emph{larger} context, i.e.\ \isa{{\isasymGamma}\ {\isasymturnstile}\isactrlsub {\isasymTheta}\ {\isasymphi}} implies \isa{{\isasymGamma}{\isacharprime}\ {\isasymturnstile}\isactrlsub {\isasymTheta}\isactrlsub {\isacharprime}\ {\isasymphi}} for contexts \isa{{\isasymTheta}{\isacharprime}\ {\isasymsupseteq}\ {\isasymTheta}} and \isa{{\isasymGamma}{\isacharprime}\ {\isasymsupseteq}\ {\isasymGamma}}.
53 \item Export: discharge of hypotheses admits results to be exported
54 into a \emph{smaller} context, i.e.\ \isa{{\isasymGamma}{\isacharprime}\ {\isasymturnstile}\isactrlsub {\isasymTheta}\ {\isasymphi}}
55 implies \isa{{\isasymGamma}\ {\isasymturnstile}\isactrlsub {\isasymTheta}\ {\isasymDelta}\ {\isasymLongrightarrow}\ {\isasymphi}} where \isa{{\isasymGamma}{\isacharprime}\ {\isasymsupseteq}\ {\isasymGamma}} and
56 \isa{{\isasymDelta}\ {\isacharequal}\ {\isasymGamma}{\isacharprime}\ {\isacharminus}\ {\isasymGamma}}. Note that \isa{{\isasymTheta}} remains unchanged here,
57 only the \isa{{\isasymGamma}} part is affected.
61 \medskip By modeling the main characteristics of the primitive
62 \isa{{\isasymTheta}} and \isa{{\isasymGamma}} above, and abstracting over any
63 particular logical content, we arrive at the fundamental notions of
64 \emph{theory context} and \emph{proof context} in Isabelle/Isar.
65 These implement a certain policy to manage arbitrary \emph{context
66 data}. There is a strongly-typed mechanism to declare new kinds of
69 The internal bootstrap process of Isabelle/Pure eventually reaches a
70 stage where certain data slots provide the logical content of \isa{{\isasymTheta}} and \isa{{\isasymGamma}} sketched above, but this does not stop there!
71 Various additional data slots support all kinds of mechanisms that
72 are not necessarily part of the core logic.
74 For example, there would be data for canonical introduction and
75 elimination rules for arbitrary operators (depending on the
76 object-logic and application), which enables users to perform
77 standard proof steps implicitly (cf.\ the \isa{rule} method
78 \cite{isabelle-isar-ref}).
80 \medskip Thus Isabelle/Isar is able to bring forth more and more
81 concepts successively. In particular, an object-logic like
82 Isabelle/HOL continues the Isabelle/Pure setup by adding specific
83 components for automated reasoning (classical reasoner, tableau
84 prover, structured induction etc.) and derived specification
85 mechanisms (inductive predicates, recursive functions etc.). All of
86 this is ultimately based on the generic data management by theory
87 and proof contexts introduced here.%
91 \isamarkupsubsection{Theory context \label{sec:context-theory}%
95 \begin{isamarkuptext}%
96 A \emph{theory} is a data container with explicit name and
97 unique identifier. Theories are related by a (nominal) sub-theory
98 relation, which corresponds to the dependency graph of the original
99 construction; each theory is derived from a certain sub-graph of
100 ancestor theories. To this end, the system maintains a set of
101 symbolic ``identification stamps'' within each theory.
103 In order to avoid the full-scale overhead of explicit sub-theory
104 identification of arbitrary intermediate stages, a theory is
105 switched into \isa{draft} mode under certain circumstances. A
106 draft theory acts like a linear type, where updates invalidate
107 earlier versions. An invalidated draft is called \emph{stale}.
109 The \isa{checkpoint} operation produces a safe stepping stone
110 that will survive the next update without becoming stale: both the
111 old and the new theory remain valid and are related by the
112 sub-theory relation. Checkpointing essentially recovers purely
113 functional theory values, at the expense of some extra internal
116 The \isa{copy} operation produces an auxiliary version that has
117 the same data content, but is unrelated to the original: updates of
118 the copy do not affect the original, neither does the sub-theory
121 The \isa{merge} operation produces the least upper bound of two
122 theories, which actually degenerates into absorption of one theory
123 into the other (according to the nominal sub-theory relation).
125 The \isa{begin} operation starts a new theory by importing
126 several parent theories and entering a special mode of nameless
127 incremental updates, until the final \isa{end} operation is
130 \medskip The example in \figref{fig:ex-theory} below shows a theory
131 graph derived from \isa{Pure}, with theory \isa{Length}
132 importing \isa{Nat} and \isa{List}. The body of \isa{Length} consists of a sequence of updates, working mostly on
133 drafts internally, while transaction boundaries of Isar top-level
134 commands (\secref{sec:isar-toplevel}) are guaranteed to be safe
139 \begin{tabular}{rcccl}
141 & & \isa{{\isasymdown}} \\
143 & $\swarrow$ & & $\searrow$ & \\
144 \isa{Nat} & & & & \isa{List} \\
145 & $\searrow$ & & $\swarrow$ \\
147 & & \multicolumn{3}{l}{~~\hyperlink{keyword.imports}{\mbox{\isa{\isakeyword{imports}}}}} \\
148 & & \multicolumn{3}{l}{~~\hyperlink{keyword.begin}{\mbox{\isa{\isakeyword{begin}}}}} \\
150 & & \isa{{\isasymbullet}}~~ \\
152 & & \isa{{\isasymbullet}}~~ \\
154 & & \multicolumn{3}{l}{~~\hyperlink{command.end}{\mbox{\isa{\isacommand{end}}}}} \\
156 \caption{A theory definition depending on ancestors}\label{fig:ex-theory}
160 \medskip There is a separate notion of \emph{theory reference} for
161 maintaining a live link to an evolving theory context: updates on
162 drafts are propagated automatically. Dynamic updating stops after
163 an explicit \isa{end} only.
165 Derived entities may store a theory reference in order to indicate
166 the context they belong to. This implicitly assumes monotonic
167 reasoning, because the referenced context may become larger without
178 \begin{isamarkuptext}%
180 \indexdef{}{ML type}{theory}\verb|type theory| \\
181 \indexdef{}{ML}{Theory.subthy}\verb|Theory.subthy: theory * theory -> bool| \\
182 \indexdef{}{ML}{Theory.checkpoint}\verb|Theory.checkpoint: theory -> theory| \\
183 \indexdef{}{ML}{Theory.copy}\verb|Theory.copy: theory -> theory| \\
184 \indexdef{}{ML}{Theory.merge}\verb|Theory.merge: theory * theory -> theory| \\
185 \indexdef{}{ML}{Theory.begin\_theory}\verb|Theory.begin_theory: string -> theory list -> theory| \\
188 \indexdef{}{ML type}{theory\_ref}\verb|type theory_ref| \\
189 \indexdef{}{ML}{Theory.deref}\verb|Theory.deref: theory_ref -> theory| \\
190 \indexdef{}{ML}{Theory.check\_thy}\verb|Theory.check_thy: theory -> theory_ref| \\
195 \item \verb|theory| represents theory contexts. This is
196 essentially a linear type, with explicit runtime checking! Most
197 internal theory operations destroy the original version, which then
200 \item \verb|Theory.subthy|~\isa{{\isacharparenleft}thy\isactrlsub {\isadigit{1}}{\isacharcomma}\ thy\isactrlsub {\isadigit{2}}{\isacharparenright}} compares theories
201 according to the intrinsic graph structure of the construction.
202 This sub-theory relation is a nominal approximation of inclusion
203 (\isa{{\isasymsubseteq}}) of the corresponding content (according to the
204 semantics of the ML modules that implement the data).
206 \item \verb|Theory.checkpoint|~\isa{thy} produces a safe
207 stepping stone in the linear development of \isa{thy}. This
208 changes the old theory, but the next update will result in two
209 related, valid theories.
211 \item \verb|Theory.copy|~\isa{thy} produces a variant of \isa{thy} with the same data. The copy is not related to the original,
212 but the original is unchanged.
214 \item \verb|Theory.merge|~\isa{{\isacharparenleft}thy\isactrlsub {\isadigit{1}}{\isacharcomma}\ thy\isactrlsub {\isadigit{2}}{\isacharparenright}} absorbs one theory
215 into the other, without changing \isa{thy\isactrlsub {\isadigit{1}}} or \isa{thy\isactrlsub {\isadigit{2}}}.
216 This version of ad-hoc theory merge fails for unrelated theories!
218 \item \verb|Theory.begin_theory|~\isa{name\ parents} constructs
219 a new theory based on the given parents. This {\ML} function is
220 normally not invoked directly.
222 \item \verb|theory_ref| represents a sliding reference to an
223 always valid theory; updates on the original are propagated
226 \item \verb|Theory.deref|~\isa{thy{\isacharunderscore}ref} turns a \verb|theory_ref| into an \verb|theory| value. As the referenced
227 theory evolves monotonically over time, later invocations of \verb|Theory.deref| may refer to a larger context.
229 \item \verb|Theory.check_thy|~\isa{thy} produces a \verb|theory_ref| from a valid \verb|theory| value.
242 \isamarkupsubsection{Proof context \label{sec:context-proof}%
246 \begin{isamarkuptext}%
247 A proof context is a container for pure data with a
248 back-reference to the theory it belongs to. The \isa{init}
249 operation creates a proof context from a given theory.
250 Modifications to draft theories are propagated to the proof context
251 as usual, but there is also an explicit \isa{transfer} operation
252 to force resynchronization with more substantial updates to the
255 Entities derived in a proof context need to record logical
256 requirements explicitly, since there is no separate context
257 identification or symbolic inclusion as for theories. For example,
258 hypotheses used in primitive derivations (cf.\ \secref{sec:thms})
259 are recorded separately within the sequent \isa{{\isasymGamma}\ {\isasymturnstile}\ {\isasymphi}}, just to
260 make double sure. Results could still leak into an alien proof
261 context due to programming errors, but Isabelle/Isar includes some
262 extra validity checks in critical positions, notably at the end of a
265 Proof contexts may be manipulated arbitrarily, although the common
266 discipline is to follow block structure as a mental model: a given
267 context is extended consecutively, and results are exported back
268 into the original context. Note that an Isar proof state models
269 block-structured reasoning explicitly, using a stack of proof
270 contexts internally. For various technical reasons, the background
271 theory of an Isar proof state must not be changed while the proof is
272 still under construction!%
282 \begin{isamarkuptext}%
284 \indexdef{}{ML type}{Proof.context}\verb|type Proof.context| \\
285 \indexdef{}{ML}{ProofContext.init}\verb|ProofContext.init: theory -> Proof.context| \\
286 \indexdef{}{ML}{ProofContext.theory\_of}\verb|ProofContext.theory_of: Proof.context -> theory| \\
287 \indexdef{}{ML}{ProofContext.transfer}\verb|ProofContext.transfer: theory -> Proof.context -> Proof.context| \\
292 \item \verb|Proof.context| represents proof contexts. Elements
293 of this type are essentially pure values, with a sliding reference
294 to the background theory.
296 \item \verb|ProofContext.init|~\isa{thy} produces a proof context
297 derived from \isa{thy}, initializing all data.
299 \item \verb|ProofContext.theory_of|~\isa{ctxt} selects the
300 background theory from \isa{ctxt}, dereferencing its internal
303 \item \verb|ProofContext.transfer|~\isa{thy\ ctxt} promotes the
304 background theory of \isa{ctxt} to the super theory \isa{thy}.
317 \isamarkupsubsection{Generic contexts \label{sec:generic-context}%
321 \begin{isamarkuptext}%
322 A generic context is the disjoint sum of either a theory or proof
323 context. Occasionally, this enables uniform treatment of generic
324 context data, typically extra-logical information. Operations on
325 generic contexts include the usual injections, partial selections,
326 and combinators for lifting operations on either component of the
329 Moreover, there are total operations \isa{theory{\isacharunderscore}of} and \isa{proof{\isacharunderscore}of} to convert a generic context into either kind: a theory
330 can always be selected from the sum, while a proof context might
331 have to be constructed by an ad-hoc \isa{init} operation, which
332 incurs a small runtime overhead.%
342 \begin{isamarkuptext}%
344 \indexdef{}{ML type}{Context.generic}\verb|type Context.generic| \\
345 \indexdef{}{ML}{Context.theory\_of}\verb|Context.theory_of: Context.generic -> theory| \\
346 \indexdef{}{ML}{Context.proof\_of}\verb|Context.proof_of: Context.generic -> Proof.context| \\
351 \item \verb|Context.generic| is the direct sum of \verb|theory| and \verb|Proof.context|, with the datatype
352 constructors \verb|Context.Theory| and \verb|Context.Proof|.
354 \item \verb|Context.theory_of|~\isa{context} always produces a
355 theory from the generic \isa{context}, using \verb|ProofContext.theory_of| as required.
357 \item \verb|Context.proof_of|~\isa{context} always produces a
358 proof context from the generic \isa{context}, using \verb|ProofContext.init| as required (note that this re-initializes the
359 context data with each invocation).
372 \isamarkupsubsection{Context data \label{sec:context-data}%
376 \begin{isamarkuptext}%
377 The main purpose of theory and proof contexts is to manage
378 arbitrary (pure) data. New data types can be declared incrementally
379 at compile time. There are separate declaration mechanisms for any
380 of the three kinds of contexts: theory, proof, generic.
382 \paragraph{Theory data} declarations need to implement the following
387 \isa{{\isasymtype}\ T} & representing type \\
388 \isa{{\isasymval}\ empty{\isacharcolon}\ T} & empty default value \\
389 \isa{{\isasymval}\ extend{\isacharcolon}\ T\ {\isasymrightarrow}\ T} & re-initialize on import \\
390 \isa{{\isasymval}\ merge{\isacharcolon}\ T\ {\isasymtimes}\ T\ {\isasymrightarrow}\ T} & join on import \\
394 \noindent The \isa{empty} value acts as initial default for
395 \emph{any} theory that does not declare actual data content; \isa{extend} is acts like a unitary version of \isa{merge}.
397 Implementing \isa{merge} can be tricky. The general idea is
398 that \isa{merge\ {\isacharparenleft}data\isactrlsub {\isadigit{1}}{\isacharcomma}\ data\isactrlsub {\isadigit{2}}{\isacharparenright}} inserts those parts of \isa{data\isactrlsub {\isadigit{2}}} into \isa{data\isactrlsub {\isadigit{1}}} that are not yet present, while
399 keeping the general order of things. The \verb|Library.merge|
400 function on plain lists may serve as canonical template.
402 Particularly note that shared parts of the data must not be
403 duplicated by naive concatenation, or a theory graph that is like a
404 chain of diamonds would cause an exponential blowup!
406 \paragraph{Proof context data} declarations need to implement the
407 following SML signature:
411 \isa{{\isasymtype}\ T} & representing type \\
412 \isa{{\isasymval}\ init{\isacharcolon}\ theory\ {\isasymrightarrow}\ T} & produce initial value \\
416 \noindent The \isa{init} operation is supposed to produce a pure
417 value from the given background theory and should be somehow
418 ``immediate''. Whenever a proof context is initialized, which
419 happens frequently, the the system invokes the \isa{init}
420 operation of \emph{all} theory data slots ever declared.
422 \paragraph{Generic data} provides a hybrid interface for both theory
423 and proof data. The \isa{init} operation for proof contexts is
424 predefined to select the current data value from the background
427 \bigskip Any of these data declaration over type \isa{T} result
428 in an ML structure with the following signature:
432 \isa{get{\isacharcolon}\ context\ {\isasymrightarrow}\ T} \\
433 \isa{put{\isacharcolon}\ T\ {\isasymrightarrow}\ context\ {\isasymrightarrow}\ context} \\
434 \isa{map{\isacharcolon}\ {\isacharparenleft}T\ {\isasymrightarrow}\ T{\isacharparenright}\ {\isasymrightarrow}\ context\ {\isasymrightarrow}\ context} \\
438 \noindent These other operations provide exclusive access for the
439 particular kind of context (theory, proof, or generic context).
440 This interface fully observes the ML discipline for types and
441 scopes: there is no other way to access the corresponding data slot
442 of a context. By keeping these operations private, an Isabelle/ML
443 module may maintain abstract values authentically.%
453 \begin{isamarkuptext}%
455 \indexdef{}{ML functor}{Theory\_Data}\verb|functor Theory_Data| \\
456 \indexdef{}{ML functor}{Proof\_Data}\verb|functor Proof_Data| \\
457 \indexdef{}{ML functor}{Generic\_Data}\verb|functor Generic_Data| \\
462 \item \verb|Theory_Data|\isa{{\isacharparenleft}spec{\isacharparenright}} declares data for
463 type \verb|theory| according to the specification provided as
464 argument structure. The resulting structure provides data init and
465 access operations as described above.
467 \item \verb|Proof_Data|\isa{{\isacharparenleft}spec{\isacharparenright}} is analogous to
468 \verb|Theory_Data| for type \verb|Proof.context|.
470 \item \verb|Generic_Data|\isa{{\isacharparenleft}spec{\isacharparenright}} is analogous to
471 \verb|Theory_Data| for type \verb|Context.generic|.
490 \begin{isamarkuptext}%
491 The following artificial example demonstrates theory
492 data: we maintain a set of terms that are supposed to be wellformed
493 wrt.\ the enclosing theory. The public interface is as follows:%
509 \isacommand{ML}\isamarkupfalse%
510 \ {\isacharverbatimopen}\isanewline
511 \ \ signature\ WELLFORMED{\isacharunderscore}TERMS\ {\isacharequal}\isanewline
513 \ \ \ \ val\ get{\isacharcolon}\ theory\ {\isacharminus}{\isachargreater}\ term\ list\isanewline
514 \ \ \ \ val\ add{\isacharcolon}\ term\ {\isacharminus}{\isachargreater}\ theory\ {\isacharminus}{\isachargreater}\ theory\isanewline
515 \ \ end{\isacharsemicolon}\isanewline
516 {\isacharverbatimclose}%
524 \begin{isamarkuptext}%
525 \noindent The implementation uses private theory data
526 internally, and only exposes an operation that involves explicit
527 argument checking wrt.\ the given theory.%
536 \isacommand{ML}\isamarkupfalse%
537 \ {\isacharverbatimopen}\isanewline
538 \ \ structure\ Wellformed{\isacharunderscore}Terms{\isacharcolon}\ WELLFORMED{\isacharunderscore}TERMS\ {\isacharequal}\isanewline
539 \ \ struct\isanewline
541 \ \ structure\ Terms\ {\isacharequal}\ Theory{\isacharunderscore}Data\isanewline
542 \ \ {\isacharparenleft}\isanewline
543 \ \ \ \ type\ T\ {\isacharequal}\ term\ OrdList{\isachardot}T{\isacharsemicolon}\isanewline
544 \ \ \ \ val\ empty\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isacharsemicolon}\isanewline
545 \ \ \ \ val\ extend\ {\isacharequal}\ I{\isacharsemicolon}\isanewline
546 \ \ \ \ fun\ merge\ {\isacharparenleft}ts{\isadigit{1}}{\isacharcomma}\ ts{\isadigit{2}}{\isacharparenright}\ {\isacharequal}\isanewline
547 \ \ \ \ \ \ OrdList{\isachardot}union\ Term{\isacharunderscore}Ord{\isachardot}fast{\isacharunderscore}term{\isacharunderscore}ord\ ts{\isadigit{1}}\ ts{\isadigit{2}}{\isacharsemicolon}\isanewline
548 \ \ {\isacharparenright}\isanewline
550 \ \ val\ get\ {\isacharequal}\ Terms{\isachardot}get{\isacharsemicolon}\isanewline
552 \ \ fun\ add\ raw{\isacharunderscore}t\ thy\ {\isacharequal}\isanewline
553 \ \ \ \ let\ val\ t\ {\isacharequal}\ Sign{\isachardot}cert{\isacharunderscore}term\ thy\ raw{\isacharunderscore}t\isanewline
554 \ \ \ \ in\ Terms{\isachardot}map\ {\isacharparenleft}OrdList{\isachardot}insert\ Term{\isacharunderscore}Ord{\isachardot}fast{\isacharunderscore}term{\isacharunderscore}ord\ t{\isacharparenright}\ thy\ end{\isacharsemicolon}\isanewline
556 \ \ end{\isacharsemicolon}\isanewline
557 {\isacharverbatimclose}%
565 \begin{isamarkuptext}%
566 We use \verb|term OrdList.T| for reasonably efficient
567 representation of a set of terms: all operations are linear in the
568 number of stored elements. Here we assume that our users do not
569 care about the declaration order, since that data structure forces
570 its own arrangement of elements.
572 Observe how the \verb|merge| operation joins the data slots of
573 the two constituents: \verb|OrdList.union| prevents duplication of
574 common data from different branches, thus avoiding the danger of
575 exponential blowup. (Plain list append etc.\ must never be used for
578 \medskip Our intended invariant is achieved as follows:
581 \item \verb|Wellformed_Terms.add| only admits terms that have passed
582 the \verb|Sign.cert_term| check of the given theory at that point.
584 \item Wellformedness in the sense of \verb|Sign.cert_term| is
585 monotonic wrt.\ the sub-theory relation. So our data can move
586 upwards in the hierarchy (via extension or merges), and maintain
587 wellformedness without further checks.
591 Note that all basic operations of the inference kernel (which
592 includes \verb|Sign.cert_term|) observe this monotonicity principle,
593 but other user-space tools don't. For example, fully-featured
594 type-inference via \verb|Syntax.check_term| (cf.\
595 \secref{sec:term-check}) is not necessarily monotonic wrt.\ the
596 background theory, since constraints of term constants can be
597 strengthened by later declarations, for example.
599 In most cases, user-space context data does not have to take such
600 invariants too seriously. The situation is different in the
601 implementation of the inference kernel itself, which uses the very
602 same data mechanisms for types, constants, axioms etc.%
606 \isamarkupsection{Names \label{sec:names}%
610 \begin{isamarkuptext}%
611 In principle, a name is just a string, but there are various
612 conventions for representing additional structure. For example,
613 ``\isa{Foo{\isachardot}bar{\isachardot}baz}'' is considered as a long name consisting of
614 qualifier \isa{Foo{\isachardot}bar} and base name \isa{baz}. The
615 individual constituents of a name may have further substructure,
616 e.g.\ the string ``\verb,\,\verb,<alpha>,'' encodes as a single
619 \medskip Subsequently, we shall introduce specific categories of
620 names. Roughly speaking these correspond to logical entities as
624 \item Basic names (\secref{sec:basic-name}): free and bound
627 \item Indexed names (\secref{sec:indexname}): schematic variables.
629 \item Long names (\secref{sec:long-name}): constants of any kind
630 (type constructors, term constants, other concepts defined in user
631 space). Such entities are typically managed via name spaces
632 (\secref{sec:name-space}).
638 \isamarkupsubsection{Strings of symbols%
642 \begin{isamarkuptext}%
643 A \emph{symbol} constitutes the smallest textual unit in
644 Isabelle --- raw ML characters are normally not encountered at all!
645 Isabelle strings consist of a sequence of symbols, represented as a
646 packed string or an exploded list of strings. Each symbol is in
647 itself a small string, which has either one of the following forms:
651 \item a single ASCII character ``\isa{c}'' or raw byte in the
652 range of 128\dots 255, for example ``\verb,a,'',
654 \item a regular symbol ``\verb,\,\verb,<,\isa{ident}\verb,>,'',
655 for example ``\verb,\,\verb,<alpha>,'',
657 \item a control symbol ``\verb,\,\verb,<^,\isa{ident}\verb,>,'',
658 for example ``\verb,\,\verb,<^bold>,'',
660 \item a raw symbol ``\verb,\,\verb,<^raw:,\isa{text}\verb,>,''
661 where \isa{text} consists of printable characters excluding
662 ``\verb,.,'' and ``\verb,>,'', for example
663 ``\verb,\,\verb,<^raw:$\sum_{i = 1}^n$>,'',
665 \item a numbered raw control symbol ``\verb,\,\verb,<^raw,\isa{n}\verb,>, where \isa{n} consists of digits, for example
666 ``\verb,\,\verb,<^raw42>,''.
670 \noindent 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
671 regular symbols and control symbols, but a fixed collection of
672 standard symbols is treated specifically. For example,
673 ``\verb,\,\verb,<alpha>,'' is classified as a letter, which means it
674 may occur within regular Isabelle identifiers.
676 Since the character set underlying Isabelle symbols is 7-bit ASCII
677 and 8-bit characters are passed through transparently, Isabelle can
678 also process Unicode/UCS data in UTF-8 encoding.\footnote{When
679 counting precise source positions internally, bytes in the range of
680 128\dots 191 are ignored. In UTF-8 encoding, this interval covers
681 the additional trailer bytes, so Isabelle happens to count Unicode
682 characters here, not bytes in memory. In ISO-Latin encoding, the
683 ignored range merely includes some extra punctuation characters that
684 even have replacements within the standard collection of Isabelle
685 symbols; the accented letters range is counted properly.} Unicode
686 provides its own collection of mathematical symbols, but within the
687 core Isabelle/ML world there is no link to the standard collection
688 of Isabelle regular symbols.
690 \medskip Output of Isabelle symbols depends on the print mode
691 (\secref{print-mode}). For example, the standard {\LaTeX} setup of
692 the Isabelle document preparation system would present
693 ``\verb,\,\verb,<alpha>,'' as \isa{{\isasymalpha}}, and
694 ``\verb,\,\verb,<^bold>,\verb,\,\verb,<alpha>,'' as \isa{\isactrlbold {\isasymalpha}}. On-screen rendering usually works by mapping a finite
695 subset of Isabelle symbols to suitable Unicode characters.%
705 \begin{isamarkuptext}%
707 \indexdef{}{ML type}{Symbol.symbol}\verb|type Symbol.symbol = string| \\
708 \indexdef{}{ML}{Symbol.explode}\verb|Symbol.explode: string -> Symbol.symbol list| \\
709 \indexdef{}{ML}{Symbol.is\_letter}\verb|Symbol.is_letter: Symbol.symbol -> bool| \\
710 \indexdef{}{ML}{Symbol.is\_digit}\verb|Symbol.is_digit: Symbol.symbol -> bool| \\
711 \indexdef{}{ML}{Symbol.is\_quasi}\verb|Symbol.is_quasi: Symbol.symbol -> bool| \\
712 \indexdef{}{ML}{Symbol.is\_blank}\verb|Symbol.is_blank: Symbol.symbol -> bool| \\
715 \indexdef{}{ML type}{Symbol.sym}\verb|type Symbol.sym| \\
716 \indexdef{}{ML}{Symbol.decode}\verb|Symbol.decode: Symbol.symbol -> Symbol.sym| \\
721 \item \verb|Symbol.symbol| represents individual Isabelle
724 \item \verb|Symbol.explode|~\isa{str} produces a symbol list
725 from the packed form. This function supercedes \verb|String.explode| for virtually all purposes of manipulating text in
726 Isabelle!\footnote{The runtime overhead for exploded strings is
727 mainly that of the list structure: individual symbols that happen to
728 be a singleton string --- which is the most common case --- do not
729 require extra memory in Poly/ML.}
731 \item \verb|Symbol.is_letter|, \verb|Symbol.is_digit|, \verb|Symbol.is_quasi|, \verb|Symbol.is_blank| classify standard
732 symbols according to fixed syntactic conventions of Isabelle, cf.\
733 \cite{isabelle-isar-ref}.
735 \item \verb|Symbol.sym| is a concrete datatype that represents
736 the different kinds of symbols explicitly, with constructors \verb|Symbol.Char|, \verb|Symbol.Sym|, \verb|Symbol.Ctrl|, \verb|Symbol.Raw|.
738 \item \verb|Symbol.decode| converts the string representation of a
739 symbol into the datatype version.
743 \paragraph{Historical note.} In the original SML90 standard the
744 primitive ML type \verb|char| did not exists, and the basic \verb|explode: string -> string list| operation would produce a list of
745 singleton strings as in Isabelle/ML today. When SML97 came out,
746 Isabelle did not adopt its slightly anachronistic 8-bit characters,
747 but the idea of exploding a string into a list of small strings was
748 extended to ``symbols'' as explained above. Thus Isabelle sources
749 can refer to an infinite store of user-defined symbols, without
750 having to worry about the multitude of Unicode encodings.%
761 \isamarkupsubsection{Basic names \label{sec:basic-name}%
765 \begin{isamarkuptext}%
766 A \emph{basic name} essentially consists of a single Isabelle
767 identifier. There are conventions to mark separate classes of basic
768 names, by attaching a suffix of underscores: one underscore means
769 \emph{internal name}, two underscores means \emph{Skolem name},
770 three underscores means \emph{internal Skolem name}.
772 For example, the basic name \isa{foo} has the internal version
773 \isa{foo{\isacharunderscore}}, with Skolem versions \isa{foo{\isacharunderscore}{\isacharunderscore}} and \isa{foo{\isacharunderscore}{\isacharunderscore}{\isacharunderscore}}, respectively.
775 These special versions provide copies of the basic name space, apart
776 from anything that normally appears in the user text. For example,
777 system generated variables in Isar proof contexts are usually marked
778 as internal, which prevents mysterious names like \isa{xaa} to
779 appear in human-readable text.
781 \medskip Manipulating binding scopes often requires on-the-fly
782 renamings. A \emph{name context} contains a collection of already
783 used names. The \isa{declare} operation adds names to the
786 The \isa{invents} operation derives a number of fresh names from
787 a given starting point. For example, the first three names derived
788 from \isa{a} are \isa{a}, \isa{b}, \isa{c}.
790 The \isa{variants} operation produces fresh names by
791 incrementing tentative names as base-26 numbers (with digits \isa{a{\isachardot}{\isachardot}z}) until all clashes are resolved. For example, name \isa{foo} results in variants \isa{fooa}, \isa{foob}, \isa{fooc}, \dots, \isa{fooaa}, \isa{fooab} etc.; each renaming
792 step picks the next unused variant from this sequence.%
802 \begin{isamarkuptext}%
804 \indexdef{}{ML}{Name.internal}\verb|Name.internal: string -> string| \\
805 \indexdef{}{ML}{Name.skolem}\verb|Name.skolem: string -> string| \\
808 \indexdef{}{ML type}{Name.context}\verb|type Name.context| \\
809 \indexdef{}{ML}{Name.context}\verb|Name.context: Name.context| \\
810 \indexdef{}{ML}{Name.declare}\verb|Name.declare: string -> Name.context -> Name.context| \\
811 \indexdef{}{ML}{Name.invents}\verb|Name.invents: Name.context -> string -> int -> string list| \\
812 \indexdef{}{ML}{Name.variants}\verb|Name.variants: string list -> Name.context -> string list * Name.context| \\
815 \indexdef{}{ML}{Variable.names\_of}\verb|Variable.names_of: Proof.context -> Name.context| \\
820 \item \verb|Name.internal|~\isa{name} produces an internal name
821 by adding one underscore.
823 \item \verb|Name.skolem|~\isa{name} produces a Skolem name by
824 adding two underscores.
826 \item \verb|Name.context| represents the context of already used
827 names; the initial value is \verb|Name.context|.
829 \item \verb|Name.declare|~\isa{name} enters a used name into the
832 \item \verb|Name.invents|~\isa{context\ name\ n} produces \isa{n} fresh names derived from \isa{name}.
834 \item \verb|Name.variants|~\isa{names\ context} produces fresh
835 variants of \isa{names}; the result is entered into the context.
837 \item \verb|Variable.names_of|~\isa{ctxt} retrieves the context
838 of declared type and term variable names. Projecting a proof
839 context down to a primitive name context is occasionally useful when
840 invoking lower-level operations. Regular management of ``fresh
841 variables'' is done by suitable operations of structure \verb|Variable|, which is also able to provide an official status of
842 ``locally fixed variable'' within the logical environment (cf.\
843 \secref{sec:variables}).
856 \isamarkupsubsection{Indexed names \label{sec:indexname}%
860 \begin{isamarkuptext}%
861 An \emph{indexed name} (or \isa{indexname}) is a pair of a basic
862 name and a natural number. This representation allows efficient
863 renaming by incrementing the second component only. The canonical
864 way to rename two collections of indexnames apart from each other is
865 this: determine the maximum index \isa{maxidx} of the first
866 collection, then increment all indexes of the second collection by
867 \isa{maxidx\ {\isacharplus}\ {\isadigit{1}}}; the maximum index of an empty collection is
868 \isa{{\isacharminus}{\isadigit{1}}}.
870 Occasionally, basic names are injected into the same pair type of
871 indexed names: then \isa{{\isacharparenleft}x{\isacharcomma}\ {\isacharminus}{\isadigit{1}}{\isacharparenright}} is used to encode the basic
874 \medskip Isabelle syntax observes the following rules for
875 representing an indexname \isa{{\isacharparenleft}x{\isacharcomma}\ i{\isacharparenright}} as a packed string:
879 \item \isa{{\isacharquery}x} if \isa{x} does not end with a digit and \isa{i\ {\isacharequal}\ {\isadigit{0}}},
881 \item \isa{{\isacharquery}xi} if \isa{x} does not end with a digit,
883 \item \isa{{\isacharquery}x{\isachardot}i} otherwise.
887 Indexnames may acquire large index numbers after several maxidx
888 shifts have been applied. Results are usually normalized towards
889 \isa{{\isadigit{0}}} at certain checkpoints, notably at the end of a proof.
890 This works by producing variants of the corresponding basic name
891 components. For example, the collection \isa{{\isacharquery}x{\isadigit{1}}{\isacharcomma}\ {\isacharquery}x{\isadigit{7}}{\isacharcomma}\ {\isacharquery}x{\isadigit{4}}{\isadigit{2}}}
892 becomes \isa{{\isacharquery}x{\isacharcomma}\ {\isacharquery}xa{\isacharcomma}\ {\isacharquery}xb}.%
902 \begin{isamarkuptext}%
904 \indexdef{}{ML type}{indexname}\verb|type indexname| \\
909 \item \verb|indexname| represents indexed names. This is an
910 abbreviation for \verb|string * int|. The second component is
911 usually non-negative, except for situations where \isa{{\isacharparenleft}x{\isacharcomma}\ {\isacharminus}{\isadigit{1}}{\isacharparenright}}
912 is used to inject basic names into this type. Other negative
913 indexes should not be used.
926 \isamarkupsubsection{Long names \label{sec:long-name}%
930 \begin{isamarkuptext}%
931 A \emph{long name} consists of a sequence of non-empty name
932 components. The packed representation uses a dot as separator, as
933 in ``\isa{A{\isachardot}b{\isachardot}c}''. The last component is called \emph{base
934 name}, the remaining prefix is called \emph{qualifier} (which may be
935 empty). The qualifier can be understood as the access path to the
936 named entity while passing through some nested block-structure,
937 although our free-form long names do not really enforce any strict
940 For example, an item named ``\isa{A{\isachardot}b{\isachardot}c}'' may be understood as
941 a local entity \isa{c}, within a local structure \isa{b},
942 within a global structure \isa{A}. In practice, long names
943 usually represent 1--3 levels of qualification. User ML code should
944 not make any assumptions about the particular structure of long
947 The empty name is commonly used as an indication of unnamed
948 entities, or entities that are not entered into the corresponding
949 name space, whenever this makes any sense. The basic operations on
950 long names map empty names again to empty names.%
960 \begin{isamarkuptext}%
962 \indexdef{}{ML}{Long\_Name.base\_name}\verb|Long_Name.base_name: string -> string| \\
963 \indexdef{}{ML}{Long\_Name.qualifier}\verb|Long_Name.qualifier: string -> string| \\
964 \indexdef{}{ML}{Long\_Name.append}\verb|Long_Name.append: string -> string -> string| \\
965 \indexdef{}{ML}{Long\_Name.implode}\verb|Long_Name.implode: string list -> string| \\
966 \indexdef{}{ML}{Long\_Name.explode}\verb|Long_Name.explode: string -> string list| \\
971 \item \verb|Long_Name.base_name|~\isa{name} returns the base name
974 \item \verb|Long_Name.qualifier|~\isa{name} returns the qualifier
977 \item \verb|Long_Name.append|~\isa{name\isactrlisub {\isadigit{1}}\ name\isactrlisub {\isadigit{2}}} appends two long
980 \item \verb|Long_Name.implode|~\isa{names} and \verb|Long_Name.explode|~\isa{name} convert between the packed string
981 representation and the explicit list form of long names.
994 \isamarkupsubsection{Name spaces \label{sec:name-space}%
998 \begin{isamarkuptext}%
999 A \isa{name\ space} manages a collection of long names,
1000 together with a mapping between partially qualified external names
1001 and fully qualified internal names (in both directions). Note that
1002 the corresponding \isa{intern} and \isa{extern} operations
1003 are mostly used for parsing and printing only! The \isa{declare} operation augments a name space according to the accesses
1004 determined by a given binding, and a naming policy from the context.
1006 \medskip A \isa{binding} specifies details about the prospective
1007 long name of a newly introduced formal entity. It consists of a
1008 base name, prefixes for qualification (separate ones for system
1009 infrastructure and user-space mechanisms), a slot for the original
1010 source position, and some additional flags.
1012 \medskip A \isa{naming} provides some additional details for
1013 producing a long name from a binding. Normally, the naming is
1014 implicit in the theory or proof context. The \isa{full}
1015 operation (and its variants for different context types) produces a
1016 fully qualified internal name to be entered into a name space. The
1017 main equation of this ``chemical reaction'' when binding new
1018 entities in a context is as follows:
1022 \isa{binding\ {\isacharplus}\ naming\ {\isasymlongrightarrow}\ long\ name\ {\isacharplus}\ name\ space\ accesses}
1026 \medskip As a general principle, there is a separate name space for
1027 each kind of formal entity, e.g.\ fact, logical constant, type
1028 constructor, type class. It is usually clear from the occurrence in
1029 concrete syntax (or from the scope) which kind of entity a name
1030 refers to. For example, the very same name \isa{c} may be used
1031 uniformly for a constant, type constructor, and type class.
1033 There are common schemes to name derived entities systematically
1034 according to the name of the main logical entity involved, e.g.\
1035 fact \isa{c{\isachardot}intro} for a canonical introduction rule related to
1036 constant \isa{c}. This technique of mapping names from one
1037 space into another requires some care in order to avoid conflicts.
1038 In particular, theorem names derived from a type constructor or type
1039 class are better suffixed in addition to the usual qualification,
1040 e.g.\ \isa{c{\isacharunderscore}type{\isachardot}intro} and \isa{c{\isacharunderscore}class{\isachardot}intro} for
1041 theorems related to type \isa{c} and class \isa{c},
1043 \end{isamarkuptext}%
1052 \begin{isamarkuptext}%
1054 \indexdef{}{ML type}{binding}\verb|type binding| \\
1055 \indexdef{}{ML}{Binding.empty}\verb|Binding.empty: binding| \\
1056 \indexdef{}{ML}{Binding.name}\verb|Binding.name: string -> binding| \\
1057 \indexdef{}{ML}{Binding.qualify}\verb|Binding.qualify: bool -> string -> binding -> binding| \\
1058 \indexdef{}{ML}{Binding.prefix}\verb|Binding.prefix: bool -> string -> binding -> binding| \\
1059 \indexdef{}{ML}{Binding.conceal}\verb|Binding.conceal: binding -> binding| \\
1060 \indexdef{}{ML}{Binding.str\_of}\verb|Binding.str_of: binding -> string| \\
1063 \indexdef{}{ML type}{Name\_Space.naming}\verb|type Name_Space.naming| \\
1064 \indexdef{}{ML}{Name\_Space.default\_naming}\verb|Name_Space.default_naming: Name_Space.naming| \\
1065 \indexdef{}{ML}{Name\_Space.add\_path}\verb|Name_Space.add_path: string -> Name_Space.naming -> Name_Space.naming| \\
1066 \indexdef{}{ML}{Name\_Space.full\_name}\verb|Name_Space.full_name: Name_Space.naming -> binding -> string| \\
1069 \indexdef{}{ML type}{Name\_Space.T}\verb|type Name_Space.T| \\
1070 \indexdef{}{ML}{Name\_Space.empty}\verb|Name_Space.empty: string -> Name_Space.T| \\
1071 \indexdef{}{ML}{Name\_Space.merge}\verb|Name_Space.merge: Name_Space.T * Name_Space.T -> Name_Space.T| \\
1072 \indexdef{}{ML}{Name\_Space.declare}\verb|Name_Space.declare: bool -> Name_Space.naming -> binding -> Name_Space.T ->|\isasep\isanewline%
1073 \verb| string * Name_Space.T| \\
1074 \indexdef{}{ML}{Name\_Space.intern}\verb|Name_Space.intern: Name_Space.T -> string -> string| \\
1075 \indexdef{}{ML}{Name\_Space.extern}\verb|Name_Space.extern: Name_Space.T -> string -> string| \\
1076 \indexdef{}{ML}{Name\_Space.is\_concealed}\verb|Name_Space.is_concealed: Name_Space.T -> string -> bool|
1081 \item \verb|binding| represents the abstract concept of name
1084 \item \verb|Binding.empty| is the empty binding.
1086 \item \verb|Binding.name|~\isa{name} produces a binding with base
1089 \item \verb|Binding.qualify|~\isa{mandatory\ name\ binding}
1090 prefixes qualifier \isa{name} to \isa{binding}. The \isa{mandatory} flag tells if this name component always needs to be
1091 given in name space accesses --- this is mostly \isa{false} in
1092 practice. Note that this part of qualification is typically used in
1093 derived specification mechanisms.
1095 \item \verb|Binding.prefix| is similar to \verb|Binding.qualify|, but
1096 affects the system prefix. This part of extra qualification is
1097 typically used in the infrastructure for modular specifications,
1098 notably ``local theory targets'' (see also \chref{ch:local-theory}).
1100 \item \verb|Binding.conceal|~\isa{binding} indicates that the
1101 binding shall refer to an entity that serves foundational purposes
1102 only. This flag helps to mark implementation details of
1103 specification mechanism etc. Other tools should not depend on the
1104 particulars of concealed entities (cf.\ \verb|Name_Space.is_concealed|).
1106 \item \verb|Binding.str_of|~\isa{binding} produces a string
1107 representation for human-readable output, together with some formal
1108 markup that might get used in GUI front-ends, for example.
1110 \item \verb|Name_Space.naming| represents the abstract concept of
1113 \item \verb|Name_Space.default_naming| is the default naming policy.
1114 In a theory context, this is usually augmented by a path prefix
1115 consisting of the theory name.
1117 \item \verb|Name_Space.add_path|~\isa{path\ naming} augments the
1118 naming policy by extending its path component.
1120 \item \verb|Name_Space.full_name|~\isa{naming\ binding} turns a
1121 name binding (usually a basic name) into the fully qualified
1122 internal name, according to the given naming policy.
1124 \item \verb|Name_Space.T| represents name spaces.
1126 \item \verb|Name_Space.empty|~\isa{kind} and \verb|Name_Space.merge|~\isa{{\isacharparenleft}space\isactrlisub {\isadigit{1}}{\isacharcomma}\ space\isactrlisub {\isadigit{2}}{\isacharparenright}} are the canonical operations for
1127 maintaining name spaces according to theory data management
1128 (\secref{sec:context-data}); \isa{kind} is a formal comment
1129 to characterize the purpose of a name space.
1131 \item \verb|Name_Space.declare|~\isa{strict\ naming\ bindings\ space} enters a name binding as fully qualified internal name into
1132 the name space, with external accesses determined by the naming
1135 \item \verb|Name_Space.intern|~\isa{space\ name} internalizes a
1136 (partially qualified) external name.
1138 This operation is mostly for parsing! Note that fully qualified
1139 names stemming from declarations are produced via \verb|Name_Space.full_name| and \verb|Name_Space.declare|
1140 (or their derivatives for \verb|theory| and
1141 \verb|Proof.context|).
1143 \item \verb|Name_Space.extern|~\isa{space\ name} externalizes a
1144 (fully qualified) internal name.
1146 This operation is mostly for printing! User code should not rely on
1147 the precise result too much.
1149 \item \verb|Name_Space.is_concealed|~\isa{space\ name} indicates
1150 whether \isa{name} refers to a strictly private entity that
1151 other tools are supposed to ignore!
1154 \end{isamarkuptext}%
1169 \isacommand{end}\isamarkupfalse%
1179 %%% Local Variables:
1181 %%% TeX-master: "root"