%

\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 required for

  formulating statements and composing proofs.  It acts as a medium to

  produce formal content, depending on earlier material (declarations,

  results etc.).

  For example, derivations within the Isabelle/Pure logic can be

  described as a judgment \isa{{\isasymGamma}\ {\isasymturnstile}\isactrlsub {\isasymTheta}\ {\isasymphi}}, which means 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 can be

  liberal about supporting type constructors and schematic

  polymorphism of constants and axioms, while the inner calculus of

  \isa{{\isasymGamma}\ {\isasymturnstile}\ {\isasymphi}} is strictly 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 \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}}.

  \item Export: discharge of hypotheses admits results to be exported

  into a \emph{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 By modeling the main characteristics of the primitive

  \isa{{\isasymTheta}} and \isa{{\isasymGamma}} above, and abstracting over any

  particular logical content, we arrive at the fundamental notions of

  \emph{theory context} and \emph{proof context} in Isabelle/Isar.

  These implement a certain policy to manage arbitrary \emph{context

  data}.  There is a strongly-typed mechanism to declare new kinds of

  data at compile time.

  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

  \cite{isabelle-isar-ref}).

  \medskip Thus Isabelle/Isar 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 ultimately based on the generic data management by theory

  and proof contexts introduced here.%

\end{isamarkuptext}%

\isamarkuptrue%

%

\isamarkupsubsection{Theory context \label{sec:context-theory}%

}

\isamarkuptrue%

%

\begin{isamarkuptext}%

\glossary{Theory}{FIXME}

  A \emph{theory} is a data container with explicit named and unique

  identifier.  Theories are related by a (nominal) sub-theory

  relation, which corresponds to the dependency graph of the original

  construction; each theory is derived from a certain sub-graph of

  ancestor theories.

  The \isa{merge} operation produces the least upper bound of two

  theories, which actually degenerates into absorption of one theory

  into the other (due to the nominal sub-theory relation).

  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

  theory acts like a linear type, where updates invalidate earlier

  versions.  An invalidated draft is called ``stale''.

  The \isa{checkpoint} operation produces an intermediate stepping

  stone that will survive the next update: 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}, with theory \isa{Length}

  importing \isa{Nat} and \isa{List}.  The body of \isa{Length} 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$ & \\

  \isa{Nat} &    &              &            & \isa{List} \\

        & $\searrow$ &              & $\swarrow$ \\

        &            & \isa{Length} \\

        &            & \multicolumn{3}{l}{~~\mbox{\isa{\isakeyword{imports}}}} \\

        &            & \multicolumn{3}{l}{~~\mbox{\isa{\isakeyword{begin}}}} \\

        &            & $\vdots$~~ \\

        &            & \isa{{\isasymbullet}}~~ \\

        &            & $\vdots$~~ \\

        &            & \isa{{\isasymbullet}}~~ \\

        &            & $\vdots$~~ \\

        &            & \multicolumn{3}{l}{~~\mbox{\isa{\isacommand{end}}}} \\

  \end{tabular}

  \caption{A theory definition depending on ancestors}\label{fig:ex-theory}

  \end{center}

  \end{figure}

  \medskip There is a separate notion of \emph{theory reference} for

  maintaining a live link to an evolving theory context: updates on

  drafts are propagated automatically.  Dynamic updating stops after

  an explicit \isa{end} only.

  Derived entities may store a theory reference in order to indicate

  the context they belong to.  This implicitly assumes monotonic

  reasoning, because the referenced context may become larger without

  further notice.%

\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| \\

  \end{mldecls}

  \begin{mldecls}

  \indexmltype{theory\_ref}\verb|type theory_ref| \\

  \indexml{Theory.deref}\verb|Theory.deref: theory_ref -> theory| \\

  \indexml{Theory.check\_thy}\verb|Theory.check_thy: theory -> theory_ref| \\

  \end{mldecls}

  \begin{description}

  \item \verb|theory| represents theory contexts.  This is

  essentially a linear type!  Most operations destroy the original

  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 result is not

  related to the original; the original is unchanched.

  \item \verb|theory_ref| represents a sliding reference to an

  always valid theory; updates on the original are propagated

  automatically.

  \item \verb|Theory.deref|~\isa{thy{\isacharunderscore}ref} turns a \verb|theory_ref| into an \verb|theory| value.  As the referenced

  theory evolves monotonically over time, later invocations of \verb|Theory.deref| may refer to a larger context.

  \item \verb|Theory.check_thy|~\isa{thy} produces a \verb|theory_ref| from a valid \verb|theory| value.

  \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 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:thms}) 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 a sub-proof.

  Proof contexts may be manipulated arbitrarily, 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 internally, cf.\ \secref{sec: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}, dereferencing its internal

  \verb|theory_ref|.

  \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 \label{sec:generic-context}%

}

\isamarkuptrue%

%

\begin{isamarkuptext}%

A generic context is the disjoint sum of either a theory or proof

  context.  Occasionally, this enables 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 from the sum, while a proof context might

  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 the 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 \label{sec:context-data}%

}

\isamarkuptrue%

%

\begin{isamarkuptext}%

The main purpose of theory and proof contexts is to manage arbitrary

  data.  New data types can be declared incrementally at compile time.

  There are separate declaration mechanisms for any of the three kinds

  of contexts: theory, proof, generic.

  \paragraph{Theory data} may refer to destructive entities, which are

  maintained in direct correspondence to the linear evolution of

  theory values, including 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 SML signature:

  \medskip

  \begin{tabular}{ll}

  \isa{{\isasymtype}\ T} & representing type \\

  \isa{{\isasymval}\ empty{\isacharcolon}\ T} & empty default value \\

  \isa{{\isasymval}\ copy{\isacharcolon}\ T\ {\isasymrightarrow}\ T} & refresh impure data \\

  \isa{{\isasymval}\ extend{\isacharcolon}\ T\ {\isasymrightarrow}\ T} & re-initialize on import \\

  \isa{{\isasymval}\ merge{\isacharcolon}\ T\ {\isasymtimes}\ T\ {\isasymrightarrow}\ T} & join on import \\

  \end{tabular}

  \medskip

  \noindent The \isa{empty} value acts as initial default for

  \emph{any} theory that does not declare actual data content; \isa{copy} maintains persistent integrity for impure data, it is just

  the identity for pure values; \isa{extend} is acts like a

  unitary version of \isa{merge}, both operations should also

  include the functionality of \isa{copy} for impure data.

  \paragraph{Proof context data} is purely functional.  A declaration

  needs to implement the following SML signature:

  \medskip

  \begin{tabular}{ll}

  \isa{{\isasymtype}\ T} & representing type \\

  \isa{{\isasymval}\ init{\isacharcolon}\ theory\ {\isasymrightarrow}\ T} & produce initial value \\

  \end{tabular}

  \medskip

  \noindent The \isa{init} operation is supposed to produce a pure

  value from the given background theory.

  \paragraph{Generic data} provides a hybrid interface for both theory

  and proof data.  The declaration is essentially the same as for

  (pure) theory data, without \isa{copy}.  The \isa{init}

  operation for proof contexts merely selects the current data value

  from the background theory.

  \bigskip 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} \\

  \end{tabular}

  \medskip

  \noindent Here \isa{init} is only applicable to impure theory

  data to install a fresh copy persistently (destructive update on

  uninitialized has no permanent effect).  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 of 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 resulting structure provides data init and

  access operations as described above.

  \item \verb|ProofDataFun|\isa{{\isacharparenleft}spec{\isacharparenright}} is analogous to

  \verb|TheoryDataFun| for type \verb|Proof.context|.

  \item \verb|GenericDataFun|\isa{{\isacharparenleft}spec{\isacharparenright}} is analogous to

  \verb|TheoryDataFun| for type \verb|Context.generic|.

  \end{description}%

\end{isamarkuptext}%

\isamarkuptrue%

%

\endisatagmlref

{\isafoldmlref}%

%

\isadelimmlref

%

\endisadelimmlref

%

\isamarkupsection{Names \label{sec:names}%

}

\isamarkuptrue%

%

\begin{isamarkuptext}%

In principle, a name is just a string, but there are various

  convention for encoding additional structure.  For example, ``\isa{Foo{\isachardot}bar{\isachardot}baz}'' is considered as a qualified name consisting of

  three basic name components.  The individual constituents of a name

  may have further substructure, e.g.\ the string

  ``\verb,\,\verb,<alpha>,'' encodes as a single symbol.%

\end{isamarkuptext}%

\isamarkuptrue%

%

\isamarkupsubsection{Strings of symbols%

}

\isamarkuptrue%

%

\begin{isamarkuptext}%

\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.).}

  A \emph{symbol} constitutes the smallest textual unit in Isabelle

  --- raw characters are normally not encountered at all.  Isabelle

  strings consist of a sequence of symbols, represented as a packed

  string or a list of strings.  Each symbol is in itself a small

  string, which has either one of the following forms:

  \begin{enumerate}

  \item a single ASCII character ``\isa{c}'', for example

  ``\verb,a,'',

  \item a regular symbol ``\verb,\,\verb,<,\isa{ident}\verb,>,'',

  for example ``\verb,\,\verb,<alpha>,'',

  \item a control symbol ``\verb,\,\verb,<^,\isa{ident}\verb,>,'',

  for example ``\verb,\,\verb,<^bold>,'',

  \item a raw symbol ``\verb,\,\verb,<^raw:,\isa{text}\verb,>,''

  where \isa{text} constists of printable characters excluding

  ``\verb,.,'' and ``\verb,>,'', for example

  ``\verb,\,\verb,<^raw:$\sum_{i = 1}^n$>,'',

  \item a numbered raw control symbol ``\verb,\,\verb,<^raw,\isa{n}\verb,>, where \isa{n} consists of digits, for example

  ``\verb,\,\verb,<^raw42>,''.

  \end{enumerate}

  \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

  regular symbols and control symbols, but a fixed collection of

  standard symbols is treated specifically.  For example,

  ``\verb,\,\verb,<alpha>,'' is classified as a letter, which means it

  may occur within regular Isabelle identifiers.

  Since the character set underlying Isabelle symbols is 7-bit ASCII

  and 8-bit characters are passed through transparently, Isabelle may

  also process Unicode/UCS data in UTF-8 encoding.  Unicode provides

  its own collection of mathematical symbols, but there is no built-in

  link to the standard collection of Isabelle.

  \medskip Output of Isabelle symbols depends on the print mode

  (\secref{FIXME}).  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}}.%

\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| \\

  \end{mldecls}

  \begin{mldecls}

  \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 individual Isabelle

  symbols; this is an alias for \verb|string|.

  \item \verb|Symbol.explode|~\isa{str} produces a symbol list

  from the packed form.  This function supercedes \verb|String.explode| for virtually all purposes of manipulating text in

  Isabelle!

  \item \verb|Symbol.is_letter|, \verb|Symbol.is_digit|, \verb|Symbol.is_quasi|, \verb|Symbol.is_blank| classify standard

  symbols according to fixed syntactic conventions of Isabelle, cf.\

  \cite{isabelle-isar-ref}.

  \item \verb|Symbol.sym| is a concrete datatype that represents

  the different kinds of symbols explicitly, with constructors \verb|Symbol.Char|, \verb|Symbol.Sym|, \verb|Symbol.Ctrl|, \verb|Symbol.Raw|.

  \item \verb|Symbol.decode| converts the string representation of a

  symbol into the datatype version.

  \end{description}%

\end{isamarkuptext}%

\isamarkuptrue%

%

\endisatagmlref

{\isafoldmlref}%

%

\isadelimmlref

%

\endisadelimmlref

%

\isamarkupsubsection{Basic names \label{sec:basic-names}%

}

\isamarkuptrue%

%

\begin{isamarkuptext}%

A \emph{basic name} essentially consists of a single Isabelle

  identifier.  There are conventions to mark separate classes of basic

  names, by attaching a suffix of underscores (\isa{{\isacharunderscore}}): one

  underscore means \emph{internal name}, two underscores means

  \emph{Skolem name}, three underscores means \emph{internal Skolem

  name}.

  For example, the basic name \isa{foo} has the internal version

  \isa{foo{\isacharunderscore}}, with Skolem versions \isa{foo{\isacharunderscore}{\isacharunderscore}} and \isa{foo{\isacharunderscore}{\isacharunderscore}{\isacharunderscore}}, respectively.

  These special versions provide copies of the basic name space, apart

  from anything that normally appears in the user text.  For example,

  system generated variables in Isar proof contexts are usually marked

  as internal, which prevents mysterious name references like \isa{xaa} to appear in the text.

  \medskip Manipulating binding scopes often requires on-the-fly

  renamings.  A \emph{name context} contains a collection of already

  used names.  The \isa{declare} operation adds names to the

  context.

  The \isa{invents} operation derives a number of fresh names from

  a given starting point.  For example, the first three names derived

  from \isa{a} are \isa{a}, \isa{b}, \isa{c}.

  The \isa{variants} operation produces fresh names by

  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

  step picks the next unused variant from this sequence.%

\end{isamarkuptext}%

\isamarkuptrue%

%

\isadelimmlref

%

\endisadelimmlref

%

\isatagmlref

%

\begin{isamarkuptext}%

\begin{mldecls}

  \indexml{Name.internal}\verb|Name.internal: string -> string| \\

  \indexml{Name.skolem}\verb|Name.skolem: string -> string| \\

  \end{mldecls}

  \begin{mldecls}

  \indexmltype{Name.context}\verb|type Name.context| \\

  \indexml{Name.context}\verb|Name.context: Name.context| \\

  \indexml{Name.declare}\verb|Name.declare: string -> Name.context -> Name.context| \\

  \indexml{Name.invents}\verb|Name.invents: Name.context -> string -> int -> string list| \\

  \indexml{Name.variants}\verb|Name.variants: string list -> Name.context -> string list * Name.context| \\

  \end{mldecls}

  \begin{description}

  \item \verb|Name.internal|~\isa{name} produces an internal name

  by adding one underscore.

  \item \verb|Name.skolem|~\isa{name} produces a Skolem name by

  adding two underscores.

  \item \verb|Name.context| represents the context of already used

  names; the initial value is \verb|Name.context|.

  \item \verb|Name.declare|~\isa{name} enters a used name into the

  context.

  \item \verb|Name.invents|~\isa{context\ name\ n} produces \isa{n} fresh names derived from \isa{name}.

  \item \verb|Name.variants|~\isa{names\ context} produces fresh

  varians of \isa{names}; the result is entered into the context.

  \end{description}%

\end{isamarkuptext}%

\isamarkuptrue%

%

\endisatagmlref

{\isafoldmlref}%

%

\isadelimmlref

%

\endisadelimmlref

%

\isamarkupsubsection{Indexed names%

}

\isamarkuptrue%

%

\begin{isamarkuptext}%

An \emph{indexed name} (or \isa{indexname}) is a pair of a basic

  name and a natural number.  This representation allows efficient

  renaming by incrementing the second component only.  The canonical

  way to rename two collections of indexnames apart from each other is

  this: determine the maximum index \isa{maxidx} of the first

  collection, then increment all indexes of the second collection by

  \isa{maxidx\ {\isacharplus}\ {\isadigit{1}}}; the maximum index of an empty collection is

  \isa{{\isacharminus}{\isadigit{1}}}.

  Occasionally, basic names and indexed names are injected into the

  same pair type: the (improper) indexname \isa{{\isacharparenleft}x{\isacharcomma}\ {\isacharminus}{\isadigit{1}}{\isacharparenright}} is used

  to encode basic names.

  \medskip Isabelle syntax observes the following rules for

  representing an indexname \isa{{\isacharparenleft}x{\isacharcomma}\ i{\isacharparenright}} as a packed string:

  \begin{itemize}

  \item \isa{{\isacharquery}x} if \isa{x} does not end with a digit and \isa{i\ {\isacharequal}\ {\isadigit{0}}},

  \item \isa{{\isacharquery}xi} if \isa{x} does not end with a digit,

  \item \isa{{\isacharquery}x{\isachardot}i} otherwise.

  \end{itemize}

  Indexnames may acquire large index numbers over time.  Results are

  normalized towards \isa{{\isadigit{0}}} at certain checkpoints, notably at

  the end of a proof.  This works by producing variants of the

  corresponding basic name components.  For example, the collection

  \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}.%

\end{isamarkuptext}%

\isamarkuptrue%

%

\isadelimmlref

%

\endisadelimmlref

%

\isatagmlref

%

\begin{isamarkuptext}%

\begin{mldecls}

  \indexmltype{indexname}\verb|type indexname| \\

  \end{mldecls}

  \begin{description}

  \item \verb|indexname| represents indexed names.  This is an

  abbreviation for \verb|string * int|.  The second component is

  usually non-negative, except for situations where \isa{{\isacharparenleft}x{\isacharcomma}\ {\isacharminus}{\isadigit{1}}{\isacharparenright}}

  is used to embed basic names into this type.

  \end{description}%

\end{isamarkuptext}%

\isamarkuptrue%

%

\endisatagmlref

{\isafoldmlref}%

%

\isadelimmlref

%

\endisadelimmlref

%

\isamarkupsubsection{Qualified names and name spaces%

}

\isamarkuptrue%

%

\begin{isamarkuptext}%

A \emph{qualified name} consists of a non-empty sequence of basic

  name components.  The packed representation uses a dot as separator,

  as in ``\isa{A{\isachardot}b{\isachardot}c}''.  The last component is called \emph{base}

  name, the remaining prefix \emph{qualifier} (which may be empty).

  The idea of qualified names is to encode nested structures by

  recording the access paths as qualifiers.  For example, an item

  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

  structure \isa{A}.  Typically, name space hierarchies consist of

  1--2 levels of qualification, but this need not be always so.

  The empty name is commonly used as an indication of unnamed

  entities, whenever this makes any sense.  The basic operations on

  qualified names are smart enough to pass through such improper names

  unchanged.

  \medskip A \isa{naming} policy tells how to turn a name

  specification into a fully qualified internal name (by the \isa{full} operation), and how fully qualified names may be accessed

  externally.  For example, the default naming policy is to prefix an

  implicit path: \isa{full\ x} produces \isa{path{\isachardot}x}, and the

  standard accesses for \isa{path{\isachardot}x} include both \isa{x} and

  \isa{path{\isachardot}x}.  Normally, the naming is implicit in the theory or

  proof context; there are separate versions of the corresponding.

  \medskip A \isa{name\ space} manages a collection of fully

  internalized names, together with a mapping between external names

  and internal names (in both directions).  The corresponding \isa{intern} and \isa{extern} operations are mostly used for

  parsing and printing only!  The \isa{declare} operation augments

  a name space according to the accesses determined by the naming

  policy.

  \medskip As a general principle, there is a separate name space for

  each kind of formal entity, e.g.\ logical constant, type

  constructor, type class, theorem.  It is usually clear from the

  occurrence in concrete syntax (or from the scope) which kind of

  entity a name refers to.  For example, the very same name \isa{c} may be used uniformly for a constant, type constructor, and

  type class.

  There are common schemes to name theorems systematically, according

  to the name of the main logical entity involved, e.g.\ \isa{c{\isachardot}intro} for a canonical theorem related to constant \isa{c}.

  This technique of mapping names from one space into another requires

  some care in order to avoid conflicts.  In particular, theorem names

  derived from a type constructor or type class are better suffixed in

  addition to the usual qualification, e.g.\ \isa{c{\isacharunderscore}type{\isachardot}intro}

  and \isa{c{\isacharunderscore}class{\isachardot}intro} for theorems related to type \isa{c}

  and class \isa{c}, respectively.%

\end{isamarkuptext}%

\isamarkuptrue%

%

\isadelimmlref

%

\endisadelimmlref

%

\isatagmlref

%

\begin{isamarkuptext}%

\begin{mldecls}

  \indexml{NameSpace.base}\verb|NameSpace.base: string -> string| \\

  \indexml{NameSpace.qualifier}\verb|NameSpace.qualifier: string -> string| \\

  \indexml{NameSpace.append}\verb|NameSpace.append: string -> string -> string| \\

  \indexml{NameSpace.implode}\verb|NameSpace.implode: string list -> string| \\

  \indexml{NameSpace.explode}\verb|NameSpace.explode: string -> string list| \\

  \end{mldecls}

  \begin{mldecls}

  \indexmltype{NameSpace.naming}\verb|type NameSpace.naming| \\

  \indexml{NameSpace.default\_naming}\verb|NameSpace.default_naming: NameSpace.naming| \\

  \indexml{NameSpace.add\_path}\verb|NameSpace.add_path: string -> NameSpace.naming -> NameSpace.naming| \\

  \indexml{NameSpace.full}\verb|NameSpace.full: NameSpace.naming -> string -> string| \\

  \end{mldecls}

  \begin{mldecls}

  \indexmltype{NameSpace.T}\verb|type NameSpace.T| \\

  \indexml{NameSpace.empty}\verb|NameSpace.empty: NameSpace.T| \\

  \indexml{NameSpace.merge}\verb|NameSpace.merge: NameSpace.T * NameSpace.T -> NameSpace.T| \\

  \indexml{NameSpace.declare}\verb|NameSpace.declare: NameSpace.naming -> string -> NameSpace.T -> NameSpace.T| \\

  \indexml{NameSpace.intern}\verb|NameSpace.intern: NameSpace.T -> string -> string| \\

  \indexml{NameSpace.extern}\verb|NameSpace.extern: NameSpace.T -> string -> string| \\

  \end{mldecls}

  \begin{description}

  \item \verb|NameSpace.base|~\isa{name} returns the base name of a

  qualified name.

  \item \verb|NameSpace.qualifier|~\isa{name} returns the qualifier

  of a qualified name.

  \item \verb|NameSpace.append|~\isa{name\isactrlisub {\isadigit{1}}\ name\isactrlisub {\isadigit{2}}}

  appends two qualified names.

  \item \verb|NameSpace.implode|~\isa{name} and \verb|NameSpace.explode|~\isa{names} convert between the packed string

  representation and the explicit list form of qualified names.

  \item \verb|NameSpace.naming| represents the abstract concept of

  a naming policy.

  \item \verb|NameSpace.default_naming| is the default naming policy.

  In a theory context, this is usually augmented by a path prefix

  consisting of the theory name.

  \item \verb|NameSpace.add_path|~\isa{path\ naming} augments the

  naming policy by extending its path component.

  \item \verb|NameSpace.full|\isa{naming\ name} turns a name

  specification (usually a basic name) into the fully qualified

  internal version, according to the given naming policy.

  \item \verb|NameSpace.T| represents name spaces.

  \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

  maintaining name spaces according to theory data management

  (\secref{sec:context-data}).

  \item \verb|NameSpace.declare|~\isa{naming\ name\ space} enters a

  fully qualified name into the name space, with external accesses

  determined by the naming policy.

  \item \verb|NameSpace.intern|~\isa{space\ name} internalizes a

  (partially qualified) external name.

  This operation is mostly for parsing!  Note that fully qualified

  names stemming from declarations are produced via \verb|NameSpace.full| (or its derivatives for \verb|theory| and

  \verb|Proof.context|).

  \item \verb|NameSpace.extern|~\isa{space\ name} externalizes a

  (fully qualified) internal name.

  This operation is mostly for printing!  Note unqualified names are

  produced via \verb|NameSpace.base|.

  \end{description}%

\end{isamarkuptext}%

\isamarkuptrue%

%

\endisatagmlref

{\isafoldmlref}%

%

\isadelimmlref

%

\endisadelimmlref

%

\isadelimtheory

%

\endisadelimtheory

%

\isatagtheory

\isacommand{end}\isamarkupfalse%

%

\endisatagtheory

{\isafoldtheory}%

%

\isadelimtheory

%

\endisadelimtheory

\isanewline

\end{isabellebody}%

%%% Local Variables:

%%% mode: latex

%%% TeX-master: "root"

%%% End: