%
\begin{isabellebody}%
\def\isabellecontext{prelim}%
%
\isadelimtheory
\isanewline
\isanewline
\isanewline
%
\endisadelimtheory
%
\isatagtheory
\isacommand{theory}\isamarkupfalse%
\ prelim\ \isakeyword{imports}\ base\ \isakeyword{begin}%
\endisatagtheory
{\isafoldtheory}%
%
\isadelimtheory
%
\endisadelimtheory
%
\isamarkupchapter{Preliminaries%
}
\isamarkuptrue%
%
\isamarkupsection{Contexts \label{sec:context}%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
A logical context represents the background that is taken for
granted when formulating statements and composing proofs. It acts
as a medium to produce formal content, depending on earlier material
(declarations, results etc.).
In particular, derivations within the primitive Pure logic can be
described as a judgment \isa{{\isasymGamma}\ {\isasymturnstile}\isactrlsub {\isasymTheta}\ {\isasymphi}}, meaning that a
proposition \isa{{\isasymphi}} is derivable from hypotheses \isa{{\isasymGamma}}
within the theory \isa{{\isasymTheta}}. There are logical reasons for
keeping \isa{{\isasymTheta}} and \isa{{\isasymGamma}} separate: theories support type
constructors and schematic polymorphism of constants and axioms,
while the inner calculus of \isa{{\isasymGamma}\ {\isasymturnstile}\ {\isasymphi}} is limited to Simple
Type Theory (with fixed type variables in the assumptions).
\medskip Contexts and derivations are linked by the following key
principles:
\begin{itemize}
\item Transfer: monotonicity of derivations admits results to be
transferred into a 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}}.
\item Export: discharge of hypotheses admits results to be exported
into a smaller context, i.e.\ \isa{{\isasymGamma}{\isacharprime}\ {\isasymturnstile}\isactrlsub {\isasymTheta}\ {\isasymphi}} implies
\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
\isa{{\isasymGamma}} part is affected.
\end{itemize}
\medskip Isabelle/Isar provides two different notions of abstract
containers called \emph{theory context} and \emph{proof context},
respectively. These model the main characteristics of the primitive
\isa{{\isasymTheta}} and \isa{{\isasymGamma}} above, without subscribing to any
particular kind of content yet. Instead, contexts merely impose a
certain policy of managing arbitrary \emph{context data}. The
system provides strongly typed mechanisms to declare new kinds of
data at compile time.
Thus the internal bootstrap process of Isabelle/Pure eventually
reaches a stage where certain data slots provide the logical content
of \isa{{\isasymTheta}} and \isa{{\isasymGamma}} sketched above, but this does not
stop there! Various additional data slots support all kinds of
mechanisms that are not necessarily part of the core logic.
For example, there would be data for canonical introduction and
elimination rules for arbitrary operators (depending on the
object-logic and application), which enables users to perform
standard proof steps implicitly (cf.\ the \isa{rule} method).
Isabelle is able to bring forth more and more concepts successively.
In particular, an object-logic like Isabelle/HOL continues the
Isabelle/Pure setup by adding specific components for automated
reasoning (classical reasoner, tableau prover, structured induction
etc.) and derived specification mechanisms (inductive predicates,
recursive functions etc.). All of this is based on the generic data
management by theory and proof contexts.%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isamarkupsubsection{Theory context \label{sec:context-theory}%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
\glossary{Theory}{FIXME}
Each theory is explicitly named and holds a unique identifier.
There is a separate \emph{theory reference} for pointing backwards
to the enclosing theory context of derived entities. Theories are
related by a (nominal) sub-theory relation, which corresponds to the
canonical dependency graph: each theory is derived from a certain
sub-graph of ancestor theories. The \isa{merge} of two theories
refers to the least upper bound, which actually degenerates into
absorption of one theory into the other, due to the nominal
sub-theory relation this.
The \isa{begin} operation starts a new theory by importing
several parent theories and entering a special \isa{draft} mode,
which is sustained until the final \isa{end} operation. A draft
mode theory acts like a linear type, where updates invalidate
earlier drafts, but theory reference values will be propagated
automatically. Thus derived entities that ``belong'' to a draft
might be transferred spontaneously to a larger context. An
invalidated draft is called ``stale''.
The \isa{checkpoint} operation produces an intermediate stepping
stone that will survive the next update unscathed: both the original
and the changed theory remain valid and are related by the
sub-theory relation. Checkpointing essentially recovers purely
functional theory values, at the expense of some extra internal
bookkeeping.
The \isa{copy} operation produces an auxiliary version that has
the same data content, but is unrelated to the original: updates of
the copy do not affect the original, neither does the sub-theory
relation hold.
\medskip The example in \figref{fig:ex-theory} below shows a theory
graph derived from \isa{Pure}. Theory \isa{Length} imports
\isa{Nat} and \isa{List}. The theory body consists of a
sequence of updates, working mostly on drafts. Intermediate
checkpoints may occur as well, due to the history mechanism provided
by the Isar top-level, cf.\ \secref{sec:isar-toplevel}.
\begin{figure}[htb]
\begin{center}
\begin{tabular}{rcccl}
& & \isa{Pure} \\
& & \isa{{\isasymdown}} \\
& & \isa{FOL} \\
& $\swarrow$ & & $\searrow$ & \\
$Nat$ & & & & \isa{List} \\
& $\searrow$ & & $\swarrow$ \\
& & \isa{Length} \\
& & \multicolumn{3}{l}{~~$\isarkeyword{imports}$} \\
& & \multicolumn{3}{l}{~~$\isarkeyword{begin}$} \\
& & $\vdots$~~ \\
& & \isa{{\isasymbullet}}~~ \\
& & $\vdots$~~ \\
& & \isa{{\isasymbullet}}~~ \\
& & $\vdots$~~ \\
& & \multicolumn{3}{l}{~~$\isarkeyword{end}$} \\
\end{tabular}
\caption{Theory definition depending on ancestors}\label{fig:ex-theory}
\end{center}
\end{figure}%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isadelimmlref
%
\endisadelimmlref
%
\isatagmlref
%
\begin{isamarkuptext}%
\begin{mldecls}
\indexmltype{theory}\verb|type theory| \\
\indexml{Theory.subthy}\verb|Theory.subthy: theory * theory -> bool| \\
\indexml{Theory.merge}\verb|Theory.merge: theory * theory -> theory| \\
\indexml{Theory.checkpoint}\verb|Theory.checkpoint: theory -> theory| \\
\indexml{Theory.copy}\verb|Theory.copy: theory -> theory| \\[1ex]
\indexmltype{theory-ref}\verb|type theory_ref| \\
\indexml{Theory.self-ref}\verb|Theory.self_ref: theory -> theory_ref| \\
\indexml{Theory.deref}\verb|Theory.deref: theory_ref -> theory| \\
\end{mldecls}
\begin{description}
\item \verb|theory| represents theory contexts. This is a
linear type! Most operations destroy the old version, which then
becomes ``stale''.
\item \verb|Theory.subthy|~\isa{{\isacharparenleft}thy\isactrlsub {\isadigit{1}}{\isacharcomma}\ thy\isactrlsub {\isadigit{2}}{\isacharparenright}}
compares theories according to the inherent graph structure of the
construction. This sub-theory relation is a nominal approximation
of inclusion (\isa{{\isasymsubseteq}}) of the corresponding content.
\item \verb|Theory.merge|~\isa{{\isacharparenleft}thy\isactrlsub {\isadigit{1}}{\isacharcomma}\ thy\isactrlsub {\isadigit{2}}{\isacharparenright}}
absorbs one theory into the other. This fails for unrelated
theories!
\item \verb|Theory.checkpoint|~\isa{thy} produces a safe
stepping stone in the linear development of \isa{thy}. The next
update will result in two related, valid theories.
\item \verb|Theory.copy|~\isa{thy} produces a variant of \isa{thy} that holds a copy of the same data. The copy is not related
to the original, which is not touched at all.
\item \verb|theory_ref| represents a sliding reference to a
valid theory --- updates on the original are propagated
automatically.
\item \verb|Theory.self_ref|~\isa{thy} and \verb|Theory.deref|~\isa{thy{\isacharunderscore}ref} convert between \verb|theory| and \verb|theory_ref|. As the referenced theory
evolves monotonically over time, later invocations of \verb|Theory.deref| may refer to larger contexts.
\end{description}%
\end{isamarkuptext}%
\isamarkuptrue%
%
\endisatagmlref
{\isafoldmlref}%
%
\isadelimmlref
%
\endisadelimmlref
%
\isamarkupsubsection{Proof context \label{sec:context-proof}%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
\glossary{Proof context}{The static context of a structured proof,
acts like a local ``theory'' of the current portion of Isar proof
text, generalizes the idea of local hypotheses \isa{{\isasymGamma}} in
judgments \isa{{\isasymGamma}\ {\isasymturnstile}\ {\isasymphi}} of natural deduction calculi. There is a
generic notion of introducing and discharging hypotheses.
Arbritrary auxiliary context data may be adjoined.}
A proof context is a container for pure data with a back-reference
to the theory it belongs to. The \isa{init} operation creates a
proof context derived from a given theory. Modifications to draft
theories are propagated to the proof context as usual, but there is
also an explicit \isa{transfer} operation to force
resynchronization with more substantial updates to the underlying
theory. The actual context data does not require any special
bookkeeping, thanks to the lack of destructive features.
Entities derived in a proof context need to record inherent logical
requirements explicitly, since there is no separate context
identification as for theories. For example, hypotheses used in
primitive derivations (cf.\ \secref{sec:thm}) are recorded
separately within the sequent \isa{{\isasymGamma}\ {\isasymturnstile}\ {\isasymphi}}, just to make double
sure. Results could still leak into an alien proof context do to
programming errors, but Isabelle/Isar includes some extra validity
checks in critical positions, notably at the end of sub-proof.
Proof contexts may be produced in arbitrary ways, although the
common discipline is to follow block structure as a mental model: a
given context is extended consecutively, and results are exported
back into the original context. Note that the Isar proof states
model block-structured reasoning explicitly, using a stack of proof
contexts, cf.\ \secref{isar-proof-state}.%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isadelimmlref
%
\endisadelimmlref
%
\isatagmlref
%
\begin{isamarkuptext}%
\begin{mldecls}
\indexmltype{Proof.context}\verb|type Proof.context| \\
\indexml{ProofContext.init}\verb|ProofContext.init: theory -> Proof.context| \\
\indexml{ProofContext.theory-of}\verb|ProofContext.theory_of: Proof.context -> theory| \\
\indexml{ProofContext.transfer}\verb|ProofContext.transfer: theory -> Proof.context -> Proof.context| \\
\end{mldecls}
\begin{description}
\item \verb|Proof.context| represents proof contexts. Elements
of this type are essentially pure values, with a sliding reference
to the background theory.
\item \verb|ProofContext.init|~\isa{thy} produces a proof context
derived from \isa{thy}, initializing all data.
\item \verb|ProofContext.theory_of|~\isa{ctxt} selects the
background theory from \isa{ctxt}.
\item \verb|ProofContext.transfer|~\isa{thy\ ctxt} promotes the
background theory of \isa{ctxt} to the super theory \isa{thy}.
\end{description}%
\end{isamarkuptext}%
\isamarkuptrue%
%
\endisatagmlref
{\isafoldmlref}%
%
\isadelimmlref
%
\endisadelimmlref
%
\isamarkupsubsection{Generic contexts%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
A generic context is the disjoint sum of either a theory or proof
context. Occasionally, this simplifies uniform treatment of generic
context data, typically extra-logical information. Operations on
generic contexts include the usual injections, partial selections,
and combinators for lifting operations on either component of the
disjoint sum.
Moreover, there are total operations \isa{theory{\isacharunderscore}of} and \isa{proof{\isacharunderscore}of} to convert a generic context into either kind: a theory
can always be selected, while a proof context may have to be
constructed by an ad-hoc \isa{init} operation.%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isadelimmlref
%
\endisadelimmlref
%
\isatagmlref
%
\begin{isamarkuptext}%
\begin{mldecls}
\indexmltype{Context.generic}\verb|type Context.generic| \\
\indexml{Context.theory-of}\verb|Context.theory_of: Context.generic -> theory| \\
\indexml{Context.proof-of}\verb|Context.proof_of: Context.generic -> Proof.context| \\
\end{mldecls}
\begin{description}
\item \verb|Context.generic| is the direct sum of \verb|theory| and \verb|Proof.context|, with datatype constructors
\verb|Context.Theory| and \verb|Context.Proof|.
\item \verb|Context.theory_of|~\isa{context} always produces a
theory from the generic \isa{context}, using \verb|ProofContext.theory_of| as required.
\item \verb|Context.proof_of|~\isa{context} always produces a
proof context from the generic \isa{context}, using \verb|ProofContext.init| as required. Note that this re-initializes the
context data with each invocation.
\end{description}%
\end{isamarkuptext}%
\isamarkuptrue%
%
\endisatagmlref
{\isafoldmlref}%
%
\isadelimmlref
%
\endisadelimmlref
%
\isamarkupsubsection{Context data%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
Both theory and proof contexts manage arbitrary data, which is the
main purpose of contexts in the first place. Data can be declared
incrementally at compile --- Isabelle/Pure and major object-logics
are bootstrapped that way.
\paragraph{Theory data} may refer to destructive entities, which are
maintained in correspondence to the linear evolution of theory
values, or explicit copies.\footnote{Most existing instances of
destructive theory data are merely historical relics (e.g.\ the
destructive theorem storage, and destructive hints for the
Simplifier and Classical rules).} A theory data declaration needs
to implement the following specification:
\medskip
\begin{tabular}{ll}
\isa{name{\isacharcolon}\ string} \\
\isa{T} & the ML type \\
\isa{empty{\isacharcolon}\ T} & initial value \\
\isa{copy{\isacharcolon}\ T\ {\isasymrightarrow}\ T} & refresh impure data \\
\isa{extend{\isacharcolon}\ T\ {\isasymrightarrow}\ T} & re-initialize on import \\
\isa{merge{\isacharcolon}\ T\ {\isasymtimes}\ T\ {\isasymrightarrow}\ T} & join on import \\
\isa{print{\isacharcolon}\ T\ {\isasymrightarrow}\ unit} & diagnostic output \\
\end{tabular}
\medskip
\noindent The \isa{name} acts as a comment for diagnostic
messages; \isa{copy} is just the identity for pure data; \isa{extend} is acts like a unitary version of \isa{merge}, both
should also include the functionality of \isa{copy} for impure
data.
\paragraph{Proof context data} is purely functional. It is declared
by implementing the following specification:
\medskip
\begin{tabular}{ll}
\isa{name{\isacharcolon}\ string} \\
\isa{T} & the ML type \\
\isa{init{\isacharcolon}\ theory\ {\isasymrightarrow}\ T} & produce initial value \\
\isa{print{\isacharcolon}\ T\ {\isasymrightarrow}\ unit} & diagnostic output \\
\end{tabular}
\medskip
\noindent The \isa{init} operation is supposed to produce a pure
value from the given background theory. The rest is analogous to
(pure) theory data.
\paragraph{Generic data} provides a hybrid interface for both kinds.
The declaration is essentially the same as for pure theory data,
without \isa{copy} (it is always the identity). The \isa{init} operation for proof contexts selects the current data value
from the background theory.
\bigskip In any case, a data declaration of type \isa{T} results
in the following interface:
\medskip
\begin{tabular}{ll}
\isa{init{\isacharcolon}\ theory\ {\isasymrightarrow}\ theory} \\
\isa{get{\isacharcolon}\ context\ {\isasymrightarrow}\ T} \\
\isa{put{\isacharcolon}\ T\ {\isasymrightarrow}\ context\ {\isasymrightarrow}\ context} \\
\isa{map{\isacharcolon}\ {\isacharparenleft}T\ {\isasymrightarrow}\ T{\isacharparenright}\ {\isasymrightarrow}\ context\ {\isasymrightarrow}\ context} \\
\isa{print{\isacharcolon}\ context\ {\isasymrightarrow}\ unit}
\end{tabular}
\medskip
\noindent Here \isa{init} needs to be applied to the current
theory context once, in order to register the initial setup. The
other operations provide access for the particular kind of context
(theory, proof, or generic context). Note that this is a safe
interface: there is no other way to access the corresponding data
slot within a context. By keeping these operations private, a
component may maintain abstract values authentically, without other
components interfering.%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isadelimmlref
%
\endisadelimmlref
%
\isatagmlref
%
\begin{isamarkuptext}%
\begin{mldecls}
\indexmlfunctor{TheoryDataFun}\verb|functor TheoryDataFun| \\
\indexmlfunctor{ProofDataFun}\verb|functor ProofDataFun| \\
\indexmlfunctor{GenericDataFun}\verb|functor GenericDataFun| \\
\end{mldecls}
\begin{description}
\item \verb|TheoryDataFun|\isa{{\isacharparenleft}spec{\isacharparenright}} declares data for
type \verb|theory| according to the specification provided as
argument structure. The result structure provides init and access
operations as described above.
\item \verb|ProofDataFun|\isa{{\isacharparenleft}spec{\isacharparenright}} is analogous for
type \verb|Proof.context|.
\item \verb|GenericDataFun|\isa{{\isacharparenleft}spec{\isacharparenright}} is analogous for
type \verb|Context.generic|.
\end{description}%
\end{isamarkuptext}%
\isamarkuptrue%
%
\endisatagmlref
{\isafoldmlref}%
%
\isadelimmlref
%
\endisadelimmlref
%
\isamarkupsection{Named entities%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
Named entities of different kinds (logical constant, type,
type class, theorem, method etc.) live in separate name spaces. It is
usually clear from the occurrence of a name which kind of entity it
refers to. For example, proof method \isa{foo} vs.\ theorem
\isa{foo} vs.\ logical constant \isa{foo} are easily
distinguished by means of the syntactic context. A notable exception
are logical identifiers within a term (\secref{sec:terms}): constants,
fixed variables, and bound variables all share the same identifier
syntax, but are distinguished by their scope.
Each name space is organized as a collection of \emph{qualified
names}, which consist of a sequence of basic name components separated
by dots: \isa{Bar{\isachardot}bar{\isachardot}foo}, \isa{Bar{\isachardot}foo}, and \isa{foo}
are examples for valid qualified names. Name components are
subdivided into \emph{symbols}, which constitute the smallest textual
unit in Isabelle --- raw characters are normally not encountered
directly.%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isamarkupsubsection{Strings of symbols%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
Isabelle strings consist of a sequence of
symbols\glossary{Symbol}{The smallest unit of text in Isabelle,
subsumes plain ASCII characters as well as an infinite collection of
named symbols (for greek, math etc.).}, which are either packed as an
actual \isa{string}, or represented as a list. Each symbol is in
itself a small string of the following form:
\begin{enumerate}
\item either a singleton ASCII character ``\isa{c}'' (with
character code 0--127), for example ``\verb,a,'',
\item or a regular symbol ``\verb,\,\verb,<,\isa{ident}\verb,>,'',
for example ``\verb,\,\verb,<alpha>,'',
\item or a control symbol ``\verb,\,\verb,<^,\isa{ident}\verb,>,'', for example ``\verb,\,\verb,<^bold>,'',
\item or a raw control symbol ``\verb,\,\verb,<^raw:,\isa{{\isasymdots}}\verb,>,'' where ``\isa{{\isasymdots}}'' refers to any
printable ASCII character (excluding ``\verb,.,'' and ``\verb,>,'') or
non-ASCII character, for example ``\verb,\,\verb,<^raw:$\sum_{i = 1}^n$>,'',
\item or a numbered raw control symbol ``\verb,\,\verb,<^raw,\isa{nnn}\verb,>, where \isa{nnn} are digits, for example
``\verb,\,\verb,<^raw42>,''.
\end{enumerate}
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
control symbols available, but a certain collection of standard
symbols is treated specifically. For example,
``\verb,\,\verb,<alpha>,'' is classified as a (non-ASCII) letter,
which means it may occur within regular Isabelle identifier syntax.
Output of symbols depends on the print mode (\secref{sec:print-mode}).
For example, the standard {\LaTeX} setup of the Isabelle document
preparation system would present ``\verb,\,\verb,<alpha>,'' as \isa{{\isasymalpha}}, and ``\verb,\,\verb,<^bold>,\verb,\,\verb,<alpha>,'' as \isa{\isactrlbold {\isasymalpha}}.
\medskip It is important to note that the character set underlying
Isabelle symbols is plain 7-bit ASCII. Since 8-bit characters are
passed through transparently, Isabelle may easily process actual
Unicode/UCS data (using the well-known UTF-8 encoding, for example).
Unicode provides its own collection of mathematical symbols, but there
is presently no link to Isabelle's named ones; both kinds of symbols
coexist independently.%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isadelimmlref
%
\endisadelimmlref
%
\isatagmlref
%
\begin{isamarkuptext}%
\begin{mldecls}
\indexmltype{Symbol.symbol}\verb|type Symbol.symbol| \\
\indexml{Symbol.explode}\verb|Symbol.explode: string -> Symbol.symbol list| \\
\indexml{Symbol.is-letter}\verb|Symbol.is_letter: Symbol.symbol -> bool| \\
\indexml{Symbol.is-digit}\verb|Symbol.is_digit: Symbol.symbol -> bool| \\
\indexml{Symbol.is-quasi}\verb|Symbol.is_quasi: Symbol.symbol -> bool| \\
\indexml{Symbol.is-blank}\verb|Symbol.is_blank: Symbol.symbol -> bool| \\
\indexmltype{Symbol.sym}\verb|type Symbol.sym| \\
\indexml{Symbol.decode}\verb|Symbol.decode: Symbol.symbol -> Symbol.sym| \\
\end{mldecls}
\begin{description}
\item \verb|Symbol.symbol| represents Isabelle symbols; this type
is merely an alias for \verb|string|, but emphasizes the
specific format encountered here.
\item \verb|Symbol.explode|~\isa{s} produces a symbol list from
the packed form usually encountered as user input. This function
replaces \verb|String.explode| for virtually all purposes of
manipulating text in Isabelle! Plain \verb|implode| may be used
for the reverse operation.
\item \verb|Symbol.is_letter|, \verb|Symbol.is_digit|, \verb|Symbol.is_quasi|, \verb|Symbol.is_blank| classify certain symbols
(both ASCII and several named ones) according to fixed syntactic
convections of Isabelle, e.g.\ see \cite{isabelle-isar-ref}.
\item \verb|Symbol.sym| is a concrete datatype that represents
the different kinds of symbols explicitly as \verb|Symbol.Char|,
\verb|Symbol.Sym|, \verb|Symbol.Ctrl|, or \verb|Symbol.Raw|.
\item \verb|Symbol.decode| converts the string representation of a
symbol into the explicit datatype version.
\end{description}%
\end{isamarkuptext}%
\isamarkuptrue%
%
\endisatagmlref
{\isafoldmlref}%
%
\isadelimmlref
%
\endisadelimmlref
%
\isamarkupsubsection{Qualified names and name spaces%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
FIXME
Qualified names are constructed according to implicit naming
principles of the present context.
The last component is called \emph{base name}; the remaining prefix
of qualification may be empty.
Some practical conventions help to organize named entities more
systematically:
\begin{itemize}
\item Names are qualified first by the theory name, second by an
optional ``structure''. For example, a constant \isa{c}
declared as part of a certain structure \isa{b} (say a type
definition) in theory \isa{A} will be named \isa{A{\isachardot}b{\isachardot}c}
internally.
\item
\item
\item
\item
\end{itemize}
Names of different kinds of entities are basically independent, but
some practical naming conventions relate them to each other. For
example, a constant \isa{foo} may be accompanied with theorems
\isa{foo{\isachardot}intro}, \isa{foo{\isachardot}elim}, \isa{foo{\isachardot}simps} etc.
The same may happen for a type \isa{foo}, which is then apt to
cause clashes in the theorem name space! To avoid this, we
occasionally follow an additional convention of suffixes that
determine the original kind of entity that a name has been derived.
For example, constant \isa{foo} is associated with theorem
\isa{foo{\isachardot}intro}, type \isa{foo} with theorem \isa{foo{\isacharunderscore}type{\isachardot}intro}, and type class \isa{foo} with \isa{foo{\isacharunderscore}class{\isachardot}intro}.%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isamarkupsection{Structured output%
}
\isamarkuptrue%
%
\isamarkupsubsection{Pretty printing%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
FIXME%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isamarkupsubsection{Output channels%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
FIXME%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isamarkupsubsection{Print modes%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
FIXME%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isadelimtheory
%
\endisadelimtheory
%
\isatagtheory
\isacommand{end}\isamarkupfalse%
%
\endisatagtheory
{\isafoldtheory}%
%
\isadelimtheory
%
\endisadelimtheory
\isanewline
\end{isabellebody}%
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "root"
%%% End: