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 unique
97 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
102 The \isa{merge} operation produces the least upper bound of two
103 theories, which actually degenerates into absorption of one theory
104 into the other (due to the nominal sub-theory relation).
106 The \isa{begin} operation starts a new theory by importing
107 several parent theories and entering a special \isa{draft} mode,
108 which is sustained until the final \isa{end} operation. A draft
109 theory acts like a linear type, where updates invalidate earlier
110 versions. An invalidated draft is called ``stale''.
112 The \isa{checkpoint} operation produces an intermediate stepping
113 stone that will survive the next update: both the original and the
114 changed theory remain valid and are related by the sub-theory
115 relation. Checkpointing essentially recovers purely functional
116 theory values, at the expense of some extra internal bookkeeping.
118 The \isa{copy} operation produces an auxiliary version that has
119 the same data content, but is unrelated to the original: updates of
120 the copy do not affect the original, neither does the sub-theory
123 \medskip The example in \figref{fig:ex-theory} below shows a theory
124 graph derived from \isa{Pure}, with theory \isa{Length}
125 importing \isa{Nat} and \isa{List}. The body of \isa{Length} consists of a sequence of updates, working mostly on
126 drafts. Intermediate checkpoints may occur as well, due to the
127 history mechanism provided by the Isar top-level, cf.\
128 \secref{sec:isar-toplevel}.
132 \begin{tabular}{rcccl}
134 & & \isa{{\isasymdown}} \\
136 & $\swarrow$ & & $\searrow$ & \\
137 \isa{Nat} & & & & \isa{List} \\
138 & $\searrow$ & & $\swarrow$ \\
140 & & \multicolumn{3}{l}{~~\hyperlink{keyword.imports}{\mbox{\isa{\isakeyword{imports}}}}} \\
141 & & \multicolumn{3}{l}{~~\hyperlink{keyword.begin}{\mbox{\isa{\isakeyword{begin}}}}} \\
143 & & \isa{{\isasymbullet}}~~ \\
145 & & \isa{{\isasymbullet}}~~ \\
147 & & \multicolumn{3}{l}{~~\hyperlink{command.end}{\mbox{\isa{\isacommand{end}}}}} \\
149 \caption{A theory definition depending on ancestors}\label{fig:ex-theory}
153 \medskip There is a separate notion of \emph{theory reference} for
154 maintaining a live link to an evolving theory context: updates on
155 drafts are propagated automatically. Dynamic updating stops after
156 an explicit \isa{end} only.
158 Derived entities may store a theory reference in order to indicate
159 the context they belong to. This implicitly assumes monotonic
160 reasoning, because the referenced context may become larger without
171 \begin{isamarkuptext}%
173 \indexdef{}{ML type}{theory}\verb|type theory| \\
174 \indexdef{}{ML}{Theory.subthy}\verb|Theory.subthy: theory * theory -> bool| \\
175 \indexdef{}{ML}{Theory.merge}\verb|Theory.merge: theory * theory -> theory| \\
176 \indexdef{}{ML}{Theory.checkpoint}\verb|Theory.checkpoint: theory -> theory| \\
177 \indexdef{}{ML}{Theory.copy}\verb|Theory.copy: theory -> theory| \\
180 \indexdef{}{ML type}{theory\_ref}\verb|type theory_ref| \\
181 \indexdef{}{ML}{Theory.deref}\verb|Theory.deref: theory_ref -> theory| \\
182 \indexdef{}{ML}{Theory.check\_thy}\verb|Theory.check_thy: theory -> theory_ref| \\
187 \item \verb|theory| represents theory contexts. This is
188 essentially a linear type! Most operations destroy the original
189 version, which then becomes ``stale''.
191 \item \verb|Theory.subthy|~\isa{{\isacharparenleft}thy\isactrlsub {\isadigit{1}}{\isacharcomma}\ thy\isactrlsub {\isadigit{2}}{\isacharparenright}}
192 compares theories according to the inherent graph structure of the
193 construction. This sub-theory relation is a nominal approximation
194 of inclusion (\isa{{\isasymsubseteq}}) of the corresponding content.
196 \item \verb|Theory.merge|~\isa{{\isacharparenleft}thy\isactrlsub {\isadigit{1}}{\isacharcomma}\ thy\isactrlsub {\isadigit{2}}{\isacharparenright}}
197 absorbs one theory into the other. This fails for unrelated
200 \item \verb|Theory.checkpoint|~\isa{thy} produces a safe
201 stepping stone in the linear development of \isa{thy}. The next
202 update will result in two related, valid theories.
204 \item \verb|Theory.copy|~\isa{thy} produces a variant of \isa{thy} that holds a copy of the same data. The result is not
205 related to the original; the original is unchanged.
207 \item \verb|theory_ref| represents a sliding reference to an
208 always valid theory; updates on the original are propagated
211 \item \verb|Theory.deref|~\isa{thy{\isacharunderscore}ref} turns a \verb|theory_ref| into an \verb|theory| value. As the referenced
212 theory evolves monotonically over time, later invocations of \verb|Theory.deref| may refer to a larger context.
214 \item \verb|Theory.check_thy|~\isa{thy} produces a \verb|theory_ref| from a valid \verb|theory| value.
227 \isamarkupsubsection{Proof context \label{sec:context-proof}%
231 \begin{isamarkuptext}%
232 A proof context is a container for pure data with a back-reference
233 to the theory it belongs to. The \isa{init} operation creates a
234 proof context from a given theory. Modifications to draft theories
235 are propagated to the proof context as usual, but there is also an
236 explicit \isa{transfer} operation to force resynchronization
237 with more substantial updates to the underlying theory. The actual
238 context data does not require any special bookkeeping, thanks to the
239 lack of destructive features.
241 Entities derived in a proof context need to record inherent logical
242 requirements explicitly, since there is no separate context
243 identification as for theories. For example, hypotheses used in
244 primitive derivations (cf.\ \secref{sec:thms}) are recorded
245 separately within the sequent \isa{{\isasymGamma}\ {\isasymturnstile}\ {\isasymphi}}, just to make double
246 sure. Results could still leak into an alien proof context due to
247 programming errors, but Isabelle/Isar includes some extra validity
248 checks in critical positions, notably at the end of a sub-proof.
250 Proof contexts may be manipulated arbitrarily, although the common
251 discipline is to follow block structure as a mental model: a given
252 context is extended consecutively, and results are exported back
253 into the original context. Note that the Isar proof states model
254 block-structured reasoning explicitly, using a stack of proof
255 contexts internally.%
265 \begin{isamarkuptext}%
267 \indexdef{}{ML type}{Proof.context}\verb|type Proof.context| \\
268 \indexdef{}{ML}{ProofContext.init}\verb|ProofContext.init: theory -> Proof.context| \\
269 \indexdef{}{ML}{ProofContext.theory\_of}\verb|ProofContext.theory_of: Proof.context -> theory| \\
270 \indexdef{}{ML}{ProofContext.transfer}\verb|ProofContext.transfer: theory -> Proof.context -> Proof.context| \\
275 \item \verb|Proof.context| represents proof contexts. Elements
276 of this type are essentially pure values, with a sliding reference
277 to the background theory.
279 \item \verb|ProofContext.init|~\isa{thy} produces a proof context
280 derived from \isa{thy}, initializing all data.
282 \item \verb|ProofContext.theory_of|~\isa{ctxt} selects the
283 background theory from \isa{ctxt}, dereferencing its internal
286 \item \verb|ProofContext.transfer|~\isa{thy\ ctxt} promotes the
287 background theory of \isa{ctxt} to the super theory \isa{thy}.
300 \isamarkupsubsection{Generic contexts \label{sec:generic-context}%
304 \begin{isamarkuptext}%
305 A generic context is the disjoint sum of either a theory or proof
306 context. Occasionally, this enables uniform treatment of generic
307 context data, typically extra-logical information. Operations on
308 generic contexts include the usual injections, partial selections,
309 and combinators for lifting operations on either component of the
312 Moreover, there are total operations \isa{theory{\isacharunderscore}of} and \isa{proof{\isacharunderscore}of} to convert a generic context into either kind: a theory
313 can always be selected from the sum, while a proof context might
314 have to be constructed by an ad-hoc \isa{init} operation.%
324 \begin{isamarkuptext}%
326 \indexdef{}{ML type}{Context.generic}\verb|type Context.generic| \\
327 \indexdef{}{ML}{Context.theory\_of}\verb|Context.theory_of: Context.generic -> theory| \\
328 \indexdef{}{ML}{Context.proof\_of}\verb|Context.proof_of: Context.generic -> Proof.context| \\
333 \item \verb|Context.generic| is the direct sum of \verb|theory| and \verb|Proof.context|, with the datatype
334 constructors \verb|Context.Theory| and \verb|Context.Proof|.
336 \item \verb|Context.theory_of|~\isa{context} always produces a
337 theory from the generic \isa{context}, using \verb|ProofContext.theory_of| as required.
339 \item \verb|Context.proof_of|~\isa{context} always produces a
340 proof context from the generic \isa{context}, using \verb|ProofContext.init| as required (note that this re-initializes the
341 context data with each invocation).
354 \isamarkupsubsection{Context data \label{sec:context-data}%
358 \begin{isamarkuptext}%
359 The main purpose of theory and proof contexts is to manage arbitrary
360 data. New data types can be declared incrementally at compile time.
361 There are separate declaration mechanisms for any of the three kinds
362 of contexts: theory, proof, generic.
364 \paragraph{Theory data} may refer to destructive entities, which are
365 maintained in direct correspondence to the linear evolution of
366 theory values, including explicit copies.\footnote{Most existing
367 instances of destructive theory data are merely historical relics
368 (e.g.\ the destructive theorem storage, and destructive hints for
369 the Simplifier and Classical rules).} A theory data declaration
370 needs to implement the following SML signature:
374 \isa{{\isasymtype}\ T} & representing type \\
375 \isa{{\isasymval}\ empty{\isacharcolon}\ T} & empty default value \\
376 \isa{{\isasymval}\ copy{\isacharcolon}\ T\ {\isasymrightarrow}\ T} & refresh impure data \\
377 \isa{{\isasymval}\ extend{\isacharcolon}\ T\ {\isasymrightarrow}\ T} & re-initialize on import \\
378 \isa{{\isasymval}\ merge{\isacharcolon}\ T\ {\isasymtimes}\ T\ {\isasymrightarrow}\ T} & join on import \\
382 \noindent The \isa{empty} value acts as initial default for
383 \emph{any} theory that does not declare actual data content; \isa{copy} maintains persistent integrity for impure data, it is just
384 the identity for pure values; \isa{extend} is acts like a
385 unitary version of \isa{merge}, both operations should also
386 include the functionality of \isa{copy} for impure data.
388 \paragraph{Proof context data} is purely functional. A declaration
389 needs to implement the following SML signature:
393 \isa{{\isasymtype}\ T} & representing type \\
394 \isa{{\isasymval}\ init{\isacharcolon}\ theory\ {\isasymrightarrow}\ T} & produce initial value \\
398 \noindent The \isa{init} operation is supposed to produce a pure
399 value from the given background theory.
401 \paragraph{Generic data} provides a hybrid interface for both theory
402 and proof data. The declaration is essentially the same as for
403 (pure) theory data, without \isa{copy}. The \isa{init}
404 operation for proof contexts merely selects the current data value
405 from the background theory.
407 \bigskip A data declaration of type \isa{T} results in the
412 \isa{init{\isacharcolon}\ theory\ {\isasymrightarrow}\ T} \\
413 \isa{get{\isacharcolon}\ context\ {\isasymrightarrow}\ T} \\
414 \isa{put{\isacharcolon}\ T\ {\isasymrightarrow}\ context\ {\isasymrightarrow}\ context} \\
415 \isa{map{\isacharcolon}\ {\isacharparenleft}T\ {\isasymrightarrow}\ T{\isacharparenright}\ {\isasymrightarrow}\ context\ {\isasymrightarrow}\ context} \\
419 \noindent Here \isa{init} is only applicable to impure theory
420 data to install a fresh copy persistently (destructive update on
421 uninitialized has no permanent effect). The other operations provide
422 access for the particular kind of context (theory, proof, or generic
423 context). Note that this is a safe interface: there is no other way
424 to access the corresponding data slot of a context. By keeping
425 these operations private, a component may maintain abstract values
426 authentically, without other components interfering.%
436 \begin{isamarkuptext}%
438 \indexdef{}{ML functor}{TheoryDataFun}\verb|functor TheoryDataFun| \\
439 \indexdef{}{ML functor}{ProofDataFun}\verb|functor ProofDataFun| \\
440 \indexdef{}{ML functor}{GenericDataFun}\verb|functor GenericDataFun| \\
445 \item \verb|TheoryDataFun|\isa{{\isacharparenleft}spec{\isacharparenright}} declares data for
446 type \verb|theory| according to the specification provided as
447 argument structure. The resulting structure provides data init and
448 access operations as described above.
450 \item \verb|ProofDataFun|\isa{{\isacharparenleft}spec{\isacharparenright}} is analogous to
451 \verb|TheoryDataFun| for type \verb|Proof.context|.
453 \item \verb|GenericDataFun|\isa{{\isacharparenleft}spec{\isacharparenright}} is analogous to
454 \verb|TheoryDataFun| for type \verb|Context.generic|.
467 \isamarkupsection{Names \label{sec:names}%
471 \begin{isamarkuptext}%
472 In principle, a name is just a string, but there are various
473 convention for encoding additional structure. For example, ``\isa{Foo{\isachardot}bar{\isachardot}baz}'' is considered as a qualified name consisting of
474 three basic name components. The individual constituents of a name
475 may have further substructure, e.g.\ the string
476 ``\verb,\,\verb,<alpha>,'' encodes as a single symbol.%
480 \isamarkupsubsection{Strings of symbols%
484 \begin{isamarkuptext}%
485 A \emph{symbol} constitutes the smallest textual unit in Isabelle
486 --- raw characters are normally not encountered at all. Isabelle
487 strings consist of a sequence of symbols, represented as a packed
488 string or a list of strings. Each symbol is in itself a small
489 string, which has either one of the following forms:
493 \item a single ASCII character ``\isa{c}'', for example
496 \item a regular symbol ``\verb,\,\verb,<,\isa{ident}\verb,>,'',
497 for example ``\verb,\,\verb,<alpha>,'',
499 \item a control symbol ``\verb,\,\verb,<^,\isa{ident}\verb,>,'',
500 for example ``\verb,\,\verb,<^bold>,'',
502 \item a raw symbol ``\verb,\,\verb,<^raw:,\isa{text}\verb,>,''
503 where \isa{text} constists of printable characters excluding
504 ``\verb,.,'' and ``\verb,>,'', for example
505 ``\verb,\,\verb,<^raw:$\sum_{i = 1}^n$>,'',
507 \item a numbered raw control symbol ``\verb,\,\verb,<^raw,\isa{n}\verb,>, where \isa{n} consists of digits, for example
508 ``\verb,\,\verb,<^raw42>,''.
512 \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
513 regular symbols and control symbols, but a fixed collection of
514 standard symbols is treated specifically. For example,
515 ``\verb,\,\verb,<alpha>,'' is classified as a letter, which means it
516 may occur within regular Isabelle identifiers.
518 Since the character set underlying Isabelle symbols is 7-bit ASCII
519 and 8-bit characters are passed through transparently, Isabelle may
520 also process Unicode/UCS data in UTF-8 encoding. Unicode provides
521 its own collection of mathematical symbols, but there is no built-in
522 link to the standard collection of Isabelle.
524 \medskip Output of Isabelle symbols depends on the print mode
525 (\secref{print-mode}). For example, the standard {\LaTeX} setup of
526 the Isabelle document preparation system would present
527 ``\verb,\,\verb,<alpha>,'' as \isa{{\isasymalpha}}, and
528 ``\verb,\,\verb,<^bold>,\verb,\,\verb,<alpha>,'' as \isa{\isactrlbold {\isasymalpha}}.%
538 \begin{isamarkuptext}%
540 \indexdef{}{ML type}{Symbol.symbol}\verb|type Symbol.symbol| \\
541 \indexdef{}{ML}{Symbol.explode}\verb|Symbol.explode: string -> Symbol.symbol list| \\
542 \indexdef{}{ML}{Symbol.is\_letter}\verb|Symbol.is_letter: Symbol.symbol -> bool| \\
543 \indexdef{}{ML}{Symbol.is\_digit}\verb|Symbol.is_digit: Symbol.symbol -> bool| \\
544 \indexdef{}{ML}{Symbol.is\_quasi}\verb|Symbol.is_quasi: Symbol.symbol -> bool| \\
545 \indexdef{}{ML}{Symbol.is\_blank}\verb|Symbol.is_blank: Symbol.symbol -> bool| \\
548 \indexdef{}{ML type}{Symbol.sym}\verb|type Symbol.sym| \\
549 \indexdef{}{ML}{Symbol.decode}\verb|Symbol.decode: Symbol.symbol -> Symbol.sym| \\
554 \item \verb|Symbol.symbol| represents individual Isabelle
555 symbols; this is an alias for \verb|string|.
557 \item \verb|Symbol.explode|~\isa{str} produces a symbol list
558 from the packed form. This function supercedes \verb|String.explode| for virtually all purposes of manipulating text in
561 \item \verb|Symbol.is_letter|, \verb|Symbol.is_digit|, \verb|Symbol.is_quasi|, \verb|Symbol.is_blank| classify standard
562 symbols according to fixed syntactic conventions of Isabelle, cf.\
563 \cite{isabelle-isar-ref}.
565 \item \verb|Symbol.sym| is a concrete datatype that represents
566 the different kinds of symbols explicitly, with constructors \verb|Symbol.Char|, \verb|Symbol.Sym|, \verb|Symbol.Ctrl|, \verb|Symbol.Raw|.
568 \item \verb|Symbol.decode| converts the string representation of a
569 symbol into the datatype version.
582 \isamarkupsubsection{Basic names \label{sec:basic-names}%
586 \begin{isamarkuptext}%
587 A \emph{basic name} essentially consists of a single Isabelle
588 identifier. There are conventions to mark separate classes of basic
589 names, by attaching a suffix of underscores: one underscore means
590 \emph{internal name}, two underscores means \emph{Skolem name},
591 three underscores means \emph{internal Skolem name}.
593 For example, the basic name \isa{foo} has the internal version
594 \isa{foo{\isacharunderscore}}, with Skolem versions \isa{foo{\isacharunderscore}{\isacharunderscore}} and \isa{foo{\isacharunderscore}{\isacharunderscore}{\isacharunderscore}}, respectively.
596 These special versions provide copies of the basic name space, apart
597 from anything that normally appears in the user text. For example,
598 system generated variables in Isar proof contexts are usually marked
599 as internal, which prevents mysterious name references like \isa{xaa} to appear in the text.
601 \medskip Manipulating binding scopes often requires on-the-fly
602 renamings. A \emph{name context} contains a collection of already
603 used names. The \isa{declare} operation adds names to the
606 The \isa{invents} operation derives a number of fresh names from
607 a given starting point. For example, the first three names derived
608 from \isa{a} are \isa{a}, \isa{b}, \isa{c}.
610 The \isa{variants} operation produces fresh names by
611 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
612 step picks the next unused variant from this sequence.%
622 \begin{isamarkuptext}%
624 \indexdef{}{ML}{Name.internal}\verb|Name.internal: string -> string| \\
625 \indexdef{}{ML}{Name.skolem}\verb|Name.skolem: string -> string| \\
628 \indexdef{}{ML type}{Name.context}\verb|type Name.context| \\
629 \indexdef{}{ML}{Name.context}\verb|Name.context: Name.context| \\
630 \indexdef{}{ML}{Name.declare}\verb|Name.declare: string -> Name.context -> Name.context| \\
631 \indexdef{}{ML}{Name.invents}\verb|Name.invents: Name.context -> string -> int -> string list| \\
632 \indexdef{}{ML}{Name.variants}\verb|Name.variants: string list -> Name.context -> string list * Name.context| \\
637 \item \verb|Name.internal|~\isa{name} produces an internal name
638 by adding one underscore.
640 \item \verb|Name.skolem|~\isa{name} produces a Skolem name by
641 adding two underscores.
643 \item \verb|Name.context| represents the context of already used
644 names; the initial value is \verb|Name.context|.
646 \item \verb|Name.declare|~\isa{name} enters a used name into the
649 \item \verb|Name.invents|~\isa{context\ name\ n} produces \isa{n} fresh names derived from \isa{name}.
651 \item \verb|Name.variants|~\isa{names\ context} produces fresh
652 variants of \isa{names}; the result is entered into the context.
665 \isamarkupsubsection{Indexed names%
669 \begin{isamarkuptext}%
670 An \emph{indexed name} (or \isa{indexname}) is a pair of a basic
671 name and a natural number. This representation allows efficient
672 renaming by incrementing the second component only. The canonical
673 way to rename two collections of indexnames apart from each other is
674 this: determine the maximum index \isa{maxidx} of the first
675 collection, then increment all indexes of the second collection by
676 \isa{maxidx\ {\isacharplus}\ {\isadigit{1}}}; the maximum index of an empty collection is
677 \isa{{\isacharminus}{\isadigit{1}}}.
679 Occasionally, basic names and indexed names are injected into the
680 same pair type: the (improper) indexname \isa{{\isacharparenleft}x{\isacharcomma}\ {\isacharminus}{\isadigit{1}}{\isacharparenright}} is used
681 to encode basic names.
683 \medskip Isabelle syntax observes the following rules for
684 representing an indexname \isa{{\isacharparenleft}x{\isacharcomma}\ i{\isacharparenright}} as a packed string:
688 \item \isa{{\isacharquery}x} if \isa{x} does not end with a digit and \isa{i\ {\isacharequal}\ {\isadigit{0}}},
690 \item \isa{{\isacharquery}xi} if \isa{x} does not end with a digit,
692 \item \isa{{\isacharquery}x{\isachardot}i} otherwise.
696 Indexnames may acquire large index numbers over time. Results are
697 normalized towards \isa{{\isadigit{0}}} at certain checkpoints, notably at
698 the end of a proof. This works by producing variants of the
699 corresponding basic name components. For example, the collection
700 \isa{{\isacharquery}x{\isadigit{1}}{\isacharcomma}\ {\isacharquery}x{\isadigit{7}}{\isacharcomma}\ {\isacharquery}x{\isadigit{4}}{\isadigit{2}}} becomes \isa{{\isacharquery}x{\isacharcomma}\ {\isacharquery}xa{\isacharcomma}\ {\isacharquery}xb}.%
710 \begin{isamarkuptext}%
712 \indexdef{}{ML type}{indexname}\verb|type indexname| \\
717 \item \verb|indexname| represents indexed names. This is an
718 abbreviation for \verb|string * int|. The second component is
719 usually non-negative, except for situations where \isa{{\isacharparenleft}x{\isacharcomma}\ {\isacharminus}{\isadigit{1}}{\isacharparenright}}
720 is used to embed basic names into this type.
733 \isamarkupsubsection{Qualified names and name spaces%
737 \begin{isamarkuptext}%
738 A \emph{qualified name} consists of a non-empty sequence of basic
739 name components. The packed representation uses a dot as separator,
740 as in ``\isa{A{\isachardot}b{\isachardot}c}''. The last component is called \emph{base}
741 name, the remaining prefix \emph{qualifier} (which may be empty).
742 The idea of qualified names is to encode nested structures by
743 recording the access paths as qualifiers. For example, an item
744 named ``\isa{A{\isachardot}b{\isachardot}c}'' may be understood as a local entity \isa{c}, within a local structure \isa{b}, within a global
745 structure \isa{A}. Typically, name space hierarchies consist of
746 1--2 levels of qualification, but this need not be always so.
748 The empty name is commonly used as an indication of unnamed
749 entities, whenever this makes any sense. The basic operations on
750 qualified names are smart enough to pass through such improper names
753 \medskip A \isa{naming} policy tells how to turn a name
754 specification into a fully qualified internal name (by the \isa{full} operation), and how fully qualified names may be accessed
755 externally. For example, the default naming policy is to prefix an
756 implicit path: \isa{full\ x} produces \isa{path{\isachardot}x}, and the
757 standard accesses for \isa{path{\isachardot}x} include both \isa{x} and
758 \isa{path{\isachardot}x}. Normally, the naming is implicit in the theory or
759 proof context; there are separate versions of the corresponding.
761 \medskip A \isa{name\ space} manages a collection of fully
762 internalized names, together with a mapping between external names
763 and internal names (in both directions). The corresponding \isa{intern} and \isa{extern} operations are mostly used for
764 parsing and printing only! The \isa{declare} operation augments
765 a name space according to the accesses determined by the naming
768 \medskip As a general principle, there is a separate name space for
769 each kind of formal entity, e.g.\ logical constant, type
770 constructor, type class, theorem. It is usually clear from the
771 occurrence in concrete syntax (or from the scope) which kind of
772 entity a name refers to. For example, the very same name \isa{c} may be used uniformly for a constant, type constructor, and
775 There are common schemes to name theorems systematically, according
776 to the name of the main logical entity involved, e.g.\ \isa{c{\isachardot}intro} for a canonical theorem related to constant \isa{c}.
777 This technique of mapping names from one space into another requires
778 some care in order to avoid conflicts. In particular, theorem names
779 derived from a type constructor or type class are better suffixed in
780 addition to the usual qualification, e.g.\ \isa{c{\isacharunderscore}type{\isachardot}intro}
781 and \isa{c{\isacharunderscore}class{\isachardot}intro} for theorems related to type \isa{c}
782 and class \isa{c}, respectively.%
792 \begin{isamarkuptext}%
794 \indexdef{}{ML}{Long\_Name.base\_name}\verb|Long_Name.base_name: string -> string| \\
795 \indexdef{}{ML}{Long\_Name.qualifier}\verb|Long_Name.qualifier: string -> string| \\
796 \indexdef{}{ML}{Long\_Name.append}\verb|Long_Name.append: string -> string -> string| \\
797 \indexdef{}{ML}{Long\_Name.implode}\verb|Long_Name.implode: string list -> string| \\
798 \indexdef{}{ML}{Long\_Name.explode}\verb|Long_Name.explode: string -> string list| \\
801 \indexdef{}{ML type}{NameSpace.naming}\verb|type NameSpace.naming| \\
802 \indexdef{}{ML}{NameSpace.default\_naming}\verb|NameSpace.default_naming: NameSpace.naming| \\
803 \indexdef{}{ML}{NameSpace.add\_path}\verb|NameSpace.add_path: string -> NameSpace.naming -> NameSpace.naming| \\
804 \indexdef{}{ML}{NameSpace.full\_name}\verb|NameSpace.full_name: NameSpace.naming -> binding -> string| \\
807 \indexdef{}{ML type}{NameSpace.T}\verb|type NameSpace.T| \\
808 \indexdef{}{ML}{NameSpace.empty}\verb|NameSpace.empty: NameSpace.T| \\
809 \indexdef{}{ML}{NameSpace.merge}\verb|NameSpace.merge: NameSpace.T * NameSpace.T -> NameSpace.T| \\
810 \indexdef{}{ML}{NameSpace.declare}\verb|NameSpace.declare: NameSpace.naming -> binding -> NameSpace.T ->|\isasep\isanewline%
811 \verb| string * NameSpace.T| \\
812 \indexdef{}{ML}{NameSpace.intern}\verb|NameSpace.intern: NameSpace.T -> string -> string| \\
813 \indexdef{}{ML}{NameSpace.extern}\verb|NameSpace.extern: NameSpace.T -> string -> string| \\
818 \item \verb|Long_Name.base_name|~\isa{name} returns the base name of a
821 \item \verb|Long_Name.qualifier|~\isa{name} returns the qualifier
824 \item \verb|Long_Name.append|~\isa{name\isactrlisub {\isadigit{1}}\ name\isactrlisub {\isadigit{2}}}
825 appends two qualified names.
827 \item \verb|Long_Name.implode|~\isa{names} and \verb|Long_Name.explode|~\isa{name} convert between the packed string
828 representation and the explicit list form of qualified names.
830 \item \verb|NameSpace.naming| represents the abstract concept of
833 \item \verb|NameSpace.default_naming| is the default naming policy.
834 In a theory context, this is usually augmented by a path prefix
835 consisting of the theory name.
837 \item \verb|NameSpace.add_path|~\isa{path\ naming} augments the
838 naming policy by extending its path component.
840 \item \verb|NameSpace.full_name|~\isa{naming\ binding} turns a
841 name binding (usually a basic name) into the fully qualified
842 internal name, according to the given naming policy.
844 \item \verb|NameSpace.T| represents name spaces.
846 \item \verb|NameSpace.empty| and \verb|NameSpace.merge|~\isa{{\isacharparenleft}space\isactrlisub {\isadigit{1}}{\isacharcomma}\ space\isactrlisub {\isadigit{2}}{\isacharparenright}} are the canonical operations for
847 maintaining name spaces according to theory data management
848 (\secref{sec:context-data}).
850 \item \verb|NameSpace.declare|~\isa{naming\ bindings\ space} enters a
851 name binding as fully qualified internal name into the name space,
852 with external accesses determined by the naming policy.
854 \item \verb|NameSpace.intern|~\isa{space\ name} internalizes a
855 (partially qualified) external name.
857 This operation is mostly for parsing! Note that fully qualified
858 names stemming from declarations are produced via \verb|NameSpace.full_name| and \verb|NameSpace.declare|
859 (or their derivatives for \verb|theory| and
860 \verb|Proof.context|).
862 \item \verb|NameSpace.extern|~\isa{space\ name} externalizes a
863 (fully qualified) internal name.
865 This operation is mostly for printing! User code should not rely on
866 the precise result too much.
884 \isacommand{end}\isamarkupfalse%
896 %%% TeX-master: "root"