%

\begin{isabellebody}%

\def\isabellecontext{Prelim}%

%

\isadelimtheory

%

\endisadelimtheory

%

\isatagtheory

\isacommand{theory}\isamarkupfalse%

\ Prelim\isanewline

\isakeyword{imports}\ Base\isanewline

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

A \emph{theory} is a data container with explicit name 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.  To this end, the system maintains a set of

  symbolic ``identification stamps'' within each theory.

  In order to avoid the full-scale overhead of explicit sub-theory

  identification of arbitrary intermediate stages, a theory is

  switched into \isa{draft} mode under certain circumstances.  A

  draft theory acts like a linear type, where updates invalidate

  earlier versions.  An invalidated draft is called \emph{stale}.

  The \isa{checkpoint} operation produces a safe stepping stone

  that will survive the next update without becoming stale: both the

  old and the new 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.

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

  theories, which actually degenerates into absorption of one theory

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

  The \isa{begin} operation starts a new theory by importing

  several parent theories and entering a special mode of nameless

  incremental updates, until the final \isa{end} operation is

  performed.

  \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 internally, while transaction boundaries of Isar top-level

  commands (\secref{sec:isar-toplevel}) are guaranteed to be safe

  checkpoints.

  \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}{~~\hyperlink{keyword.imports}{\mbox{\isa{\isakeyword{imports}}}}} \\

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

        &            & $\vdots$~~ \\

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

        &            & $\vdots$~~ \\

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

        &            & $\vdots$~~ \\

        &            & \multicolumn{3}{l}{~~\hyperlink{command.end}{\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}

  \indexdef{}{ML type}{theory}\verb|type theory| \\

  \indexdef{}{ML}{Theory.subthy}\verb|Theory.subthy: theory * theory -> bool| \\

  \indexdef{}{ML}{Theory.checkpoint}\verb|Theory.checkpoint: theory -> theory| \\

  \indexdef{}{ML}{Theory.copy}\verb|Theory.copy: theory -> theory| \\

  \indexdef{}{ML}{Theory.merge}\verb|Theory.merge: theory * theory -> theory| \\

  \indexdef{}{ML}{Theory.begin\_theory}\verb|Theory.begin_theory: string -> theory list -> theory| \\

  \end{mldecls}

  \begin{mldecls}

  \indexdef{}{ML type}{theory\_ref}\verb|type theory_ref| \\

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

  \indexdef{}{ML}{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, with explicit runtime checking!  Most

  internal theory 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 intrinsic graph structure of the construction.

  This sub-theory relation is a nominal approximation of inclusion

  (\isa{{\isasymsubseteq}}) of the corresponding content (according to the

  semantics of the ML modules that implement the data).

  \item \verb|Theory.checkpoint|~\isa{thy} produces a safe

  stepping stone in the linear development of \isa{thy}.  This

  changes the old theory, but the next update will result in two

  related, valid theories.

  \item \verb|Theory.copy|~\isa{thy} produces a variant of \isa{thy} with the same data.  The copy is not related to the original,

  but the original is unchanged.

  \item \verb|Theory.merge|~\isa{{\isacharparenleft}thy\isactrlsub {\isadigit{1}}{\isacharcomma}\ thy\isactrlsub {\isadigit{2}}{\isacharparenright}} absorbs one theory

  into the other, without changing \isa{thy\isactrlsub {\isadigit{1}}} or \isa{thy\isactrlsub {\isadigit{2}}}.

  This version of ad-hoc theory merge fails for unrelated theories!

  \item \verb|Theory.begin_theory|~\isa{name\ parents} constructs

  a new theory based on the given parents.  This {\ML} function is

  normally not invoked directly.

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

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.

  Entities derived in a proof context need to record logical

  requirements explicitly, since there is no separate context

  identification or symbolic inclusion 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 due 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 an Isar proof state models

  block-structured reasoning explicitly, using a stack of proof

  contexts internally.  For various technical reasons, the background

  theory of an Isar proof state must not be changed while the proof is

  still under construction!%

\end{isamarkuptext}%

\isamarkuptrue%

%

\isadelimmlref

%

\endisadelimmlref

%

\isatagmlref

%

\begin{isamarkuptext}%

\begin{mldecls}

  \indexdef{}{ML type}{Proof.context}\verb|type Proof.context| \\

  \indexdef{}{ML}{ProofContext.init}\verb|ProofContext.init: theory -> Proof.context| \\

  \indexdef{}{ML}{ProofContext.theory\_of}\verb|ProofContext.theory_of: Proof.context -> theory| \\

  \indexdef{}{ML}{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, which

  incurs a small runtime overhead.%

\end{isamarkuptext}%

\isamarkuptrue%

%

\isadelimmlref

%

\endisadelimmlref

%

\isatagmlref

%

\begin{isamarkuptext}%

\begin{mldecls}

  \indexdef{}{ML type}{Context.generic}\verb|type Context.generic| \\

  \indexdef{}{ML}{Context.theory\_of}\verb|Context.theory_of: Context.generic -> theory| \\

  \indexdef{}{ML}{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 (pure) 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} declarations need 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}\ 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{extend} is acts like a unitary version of \isa{merge}.

  Implementing \isa{merge} can be tricky.  The general idea is

  that \isa{merge\ {\isacharparenleft}data\isactrlsub {\isadigit{1}}{\isacharcomma}\ data\isactrlsub {\isadigit{2}}{\isacharparenright}} inserts those parts of \isa{data\isactrlsub {\isadigit{2}}} into \isa{data\isactrlsub {\isadigit{1}}} that are not yet present, while

  keeping the general order of things.  The \verb|Library.merge|

  function on plain lists may serve as canonical template.

  Particularly note that shared parts of the data must not be

  duplicated by naive concatenation, or a theory graph that is like a

  chain of diamonds would cause an exponential blowup!

  \paragraph{Proof context data} declarations need 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 and should be somehow

  ``immediate''.  Whenever a proof context is initialized, which

  happens frequently, the the system invokes the \isa{init}

  operation of \emph{all} theory data slots ever declared.

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

  and proof data.  The \isa{init} operation for proof contexts is

  predefined to select the current data value from the background

  theory.

  \bigskip Any of these data declaration over type \isa{T} result

  in an ML structure with the following signature:

  \medskip

  \begin{tabular}{ll}

  \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 These other operations provide exclusive access for the

  particular kind of context (theory, proof, or generic context).

  This interface fully observes the ML discipline for types and

  scopes: there is no other way to access the corresponding data slot

  of a context.  By keeping these operations private, an Isabelle/ML

  module may maintain abstract values authentically.%

\end{isamarkuptext}%

\isamarkuptrue%

%

\isadelimmlref

%

\endisadelimmlref

%

\isatagmlref

%

\begin{isamarkuptext}%

\begin{mldecls}

  \indexdef{}{ML functor}{Theory\_Data}\verb|functor Theory_Data| \\

  \indexdef{}{ML functor}{Proof\_Data}\verb|functor Proof_Data| \\

  \indexdef{}{ML functor}{Generic\_Data}\verb|functor Generic_Data| \\

  \end{mldecls}

  \begin{description}

  \item \verb|Theory_Data|\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|Proof_Data|\isa{{\isacharparenleft}spec{\isacharparenright}} is analogous to

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

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

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

  \end{description}%

\end{isamarkuptext}%

\isamarkuptrue%

%

\endisatagmlref

{\isafoldmlref}%

%

\isadelimmlref

%

\endisadelimmlref

%

\isadelimmlex

%

\endisadelimmlex

%

\isatagmlex

%

\begin{isamarkuptext}%

The following artificial example demonstrates theory

  data: we maintain a set of terms that are supposed to be wellformed

  wrt.\ the enclosing theory.  The public interface is as follows:%

\end{isamarkuptext}%

\isamarkuptrue%

%

\endisatagmlex

{\isafoldmlex}%

%

\isadelimmlex

%

\endisadelimmlex

%

\isadelimML

%

\endisadelimML

%

\isatagML

\isacommand{ML}\isamarkupfalse%

\ {\isacharverbatimopen}\isanewline

\ \ signature\ WELLFORMED{\isacharunderscore}TERMS\ {\isacharequal}\isanewline

\ \ sig\isanewline

\ \ \ \ val\ get{\isacharcolon}\ theory\ {\isacharminus}{\isachargreater}\ term\ list\isanewline

\ \ \ \ val\ add{\isacharcolon}\ term\ {\isacharminus}{\isachargreater}\ theory\ {\isacharminus}{\isachargreater}\ theory\isanewline

\ \ end{\isacharsemicolon}\isanewline

{\isacharverbatimclose}%

\endisatagML

{\isafoldML}%

%

\isadelimML

%

\endisadelimML

%

\begin{isamarkuptext}%

\noindent The implementation uses private theory data

  internally, and only exposes an operation that involves explicit

  argument checking wrt.\ the given theory.%

\end{isamarkuptext}%

\isamarkuptrue%

%

\isadelimML

%

\endisadelimML

%

\isatagML

\isacommand{ML}\isamarkupfalse%

\ {\isacharverbatimopen}\isanewline

\ \ structure\ Wellformed{\isacharunderscore}Terms{\isacharcolon}\ WELLFORMED{\isacharunderscore}TERMS\ {\isacharequal}\isanewline

\ \ struct\isanewline

\isanewline

\ \ structure\ Terms\ {\isacharequal}\ Theory{\isacharunderscore}Data\isanewline

\ \ {\isacharparenleft}\isanewline

\ \ \ \ type\ T\ {\isacharequal}\ term\ OrdList{\isachardot}T{\isacharsemicolon}\isanewline

\ \ \ \ val\ empty\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isacharsemicolon}\isanewline

\ \ \ \ val\ extend\ {\isacharequal}\ I{\isacharsemicolon}\isanewline

\ \ \ \ fun\ merge\ {\isacharparenleft}ts{\isadigit{1}}{\isacharcomma}\ ts{\isadigit{2}}{\isacharparenright}\ {\isacharequal}\isanewline

\ \ \ \ \ \ OrdList{\isachardot}union\ Term{\isacharunderscore}Ord{\isachardot}fast{\isacharunderscore}term{\isacharunderscore}ord\ ts{\isadigit{1}}\ ts{\isadigit{2}}{\isacharsemicolon}\isanewline

\ \ {\isacharparenright}\isanewline

\isanewline

\ \ val\ get\ {\isacharequal}\ Terms{\isachardot}get{\isacharsemicolon}\isanewline

\isanewline

\ \ fun\ add\ raw{\isacharunderscore}t\ thy\ {\isacharequal}\isanewline

\ \ \ \ let\ val\ t\ {\isacharequal}\ Sign{\isachardot}cert{\isacharunderscore}term\ thy\ raw{\isacharunderscore}t\isanewline

\ \ \ \ in\ Terms{\isachardot}map\ {\isacharparenleft}OrdList{\isachardot}insert\ Term{\isacharunderscore}Ord{\isachardot}fast{\isacharunderscore}term{\isacharunderscore}ord\ t{\isacharparenright}\ thy\ end{\isacharsemicolon}\isanewline

\isanewline

\ \ end{\isacharsemicolon}\isanewline

{\isacharverbatimclose}%

\endisatagML

{\isafoldML}%

%

\isadelimML

%

\endisadelimML

%

\begin{isamarkuptext}%

We use \verb|term OrdList.T| for reasonably efficient

  representation of a set of terms: all operations are linear in the

  number of stored elements.  Here we assume that our users do not

  care about the declaration order, since that data structure forces

  its own arrangement of elements.

  Observe how the \verb|merge| operation joins the data slots of

  the two constituents: \verb|OrdList.union| prevents duplication of

  common data from different branches, thus avoiding the danger of

  exponential blowup.  (Plain list append etc.\ must never be used for

  theory data merges.)

  \medskip Our intended invariant is achieved as follows:

  \begin{enumerate}

  \item \verb|Wellformed_Terms.add| only admits terms that have passed

  the \verb|Sign.cert_term| check of the given theory at that point.

  \item Wellformedness in the sense of \verb|Sign.cert_term| is

  monotonic wrt.\ the sub-theory relation.  So our data can move

  upwards in the hierarchy (via extension or merges), and maintain

  wellformedness without further checks.

  \end{enumerate}

  Note that all basic operations of the inference kernel (which

  includes \verb|Sign.cert_term|) observe this monotonicity principle,

  but other user-space tools don't.  For example, fully-featured

  type-inference via \verb|Syntax.check_term| (cf.\

  \secref{sec:term-check}) is not necessarily monotonic wrt.\ the

  background theory, since constraints of term constants can be

  strengthened by later declarations, for example.

  In most cases, user-space context data does not have to take such

  invariants too seriously.  The situation is different in the

  implementation of the inference kernel itself, which uses the very

  same data mechanisms for types, constants, axioms etc.%

\end{isamarkuptext}%

\isamarkuptrue%

%

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

}

\isamarkuptrue%

%

\begin{isamarkuptext}%

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

  conventions for representing additional structure.  For example,

  ``\isa{Foo{\isachardot}bar{\isachardot}baz}'' is considered as a long name consisting of

  qualifier \isa{Foo{\isachardot}bar} and base name \isa{baz}.  The

  individual constituents of a name may have further substructure,

  e.g.\ the string ``\verb,\,\verb,<alpha>,'' encodes as a single

  symbol.

  \medskip Subsequently, we shall introduce specific categories of

  names.  Roughly speaking these correspond to logical entities as

  follows:

  \begin{itemize}

  \item Basic names (\secref{sec:basic-name}): free and bound

  variables.

  \item Indexed names (\secref{sec:indexname}): schematic variables.

  \item Long names (\secref{sec:long-name}): constants of any kind

  (type constructors, term constants, other concepts defined in user

  space).  Such entities are typically managed via name spaces

  (\secref{sec:name-space}).

  \end{itemize}%

\end{isamarkuptext}%

\isamarkuptrue%

%

\isamarkupsubsection{Strings of symbols%

}

\isamarkuptrue%

%

\begin{isamarkuptext}%

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

  Isabelle --- raw ML characters are normally not encountered at all!

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

  packed string or an exploded 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}'' or raw byte in the

  range of 128\dots 255, 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} consists 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 can

  also process Unicode/UCS data in UTF-8 encoding.\footnote{When

  counting precise source positions internally, bytes in the range of

  128\dots 191 are ignored.  In UTF-8 encoding, this interval covers

  the additional trailer bytes, so Isabelle happens to count Unicode

  characters here, not bytes in memory.  In ISO-Latin encoding, the

  ignored range merely includes some extra punctuation characters that

  even have replacements within the standard collection of Isabelle

  symbols; the accented letters range is counted properly.} Unicode

  provides its own collection of mathematical symbols, but within the

  core Isabelle/ML world there is no link to the standard collection

  of Isabelle regular symbols.

  \medskip Output of Isabelle symbols depends on the print mode

  (\secref{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}}.  On-screen rendering usually works by mapping a finite

  subset of Isabelle symbols to suitable Unicode characters.%

\end{isamarkuptext}%

\isamarkuptrue%

%

\isadelimmlref

%

\endisadelimmlref

%

\isatagmlref

%

\begin{isamarkuptext}%

\begin{mldecls}

  \indexdef{}{ML type}{Symbol.symbol}\verb|type Symbol.symbol = string| \\

  \indexdef{}{ML}{Symbol.explode}\verb|Symbol.explode: string -> Symbol.symbol list| \\

  \indexdef{}{ML}{Symbol.is\_letter}\verb|Symbol.is_letter: Symbol.symbol -> bool| \\

  \indexdef{}{ML}{Symbol.is\_digit}\verb|Symbol.is_digit: Symbol.symbol -> bool| \\

  \indexdef{}{ML}{Symbol.is\_quasi}\verb|Symbol.is_quasi: Symbol.symbol -> bool| \\

  \indexdef{}{ML}{Symbol.is\_blank}\verb|Symbol.is_blank: Symbol.symbol -> bool| \\

  \end{mldecls}

  \begin{mldecls}

  \indexdef{}{ML type}{Symbol.sym}\verb|type Symbol.sym| \\

  \indexdef{}{ML}{Symbol.decode}\verb|Symbol.decode: Symbol.symbol -> Symbol.sym| \\

  \end{mldecls}

  \begin{description}

  \item \verb|Symbol.symbol| represents individual Isabelle

  symbols.

  \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!\footnote{The runtime overhead for exploded strings is

  mainly that of the list structure: individual symbols that happen to

  be a singleton string --- which is the most common case --- do not

  require extra memory in Poly/ML.}

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

  \paragraph{Historical note.} In the original SML90 standard the

  primitive ML type \verb|char| did not exists, and the basic \verb|explode: string -> string list| operation would produce a list of

  singleton strings as in Isabelle/ML today.  When SML97 came out,

  Isabelle did not adopt its slightly anachronistic 8-bit characters,

  but the idea of exploding a string into a list of small strings was

  extended to ``symbols'' as explained above.  Thus Isabelle sources

  can refer to an infinite store of user-defined symbols, without

  having to worry about the multitude of Unicode encodings.%

\end{isamarkuptext}%

\isamarkuptrue%

%

\endisatagmlref

{\isafoldmlref}%

%

\isadelimmlref

%

\endisadelimmlref

%

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

}

\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: 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 names like \isa{xaa} to

  appear in human-readable 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}

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

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

  \end{mldecls}

  \begin{mldecls}

  \indexdef{}{ML type}{Name.context}\verb|type Name.context| \\

  \indexdef{}{ML}{Name.context}\verb|Name.context: Name.context| \\

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

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

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

  \end{mldecls}

  \begin{mldecls}

  \indexdef{}{ML}{Variable.names\_of}\verb|Variable.names_of: Proof.context -> 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

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

  \item \verb|Variable.names_of|~\isa{ctxt} retrieves the context

  of declared type and term variable names.  Projecting a proof

  context down to a primitive name context is occasionally useful when

  invoking lower-level operations.  Regular management of ``fresh

  variables'' is done by suitable operations of structure \verb|Variable|, which is also able to provide an official status of

  ``locally fixed variable'' within the logical environment (cf.\

  \secref{sec:variables}).

  \end{description}%

\end{isamarkuptext}%

\isamarkuptrue%

%

\endisatagmlref

{\isafoldmlref}%

%

\isadelimmlref

%

\endisadelimmlref

%

\isamarkupsubsection{Indexed names \label{sec:indexname}%

}

\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 are injected into the same pair type of

  indexed names: then \isa{{\isacharparenleft}x{\isacharcomma}\ {\isacharminus}{\isadigit{1}}{\isacharparenright}} is used to encode the basic

  name \isa{x}.

  \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 after several maxidx

  shifts have been applied.  Results are usually 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}

  \indexdef{}{ML type}{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 inject basic names into this type.  Other negative

  indexes should not be used.

  \end{description}%

\end{isamarkuptext}%

\isamarkuptrue%

%

\endisatagmlref

{\isafoldmlref}%

%

\isadelimmlref

%

\endisadelimmlref

%

\isamarkupsubsection{Long names \label{sec:long-name}%

}

\isamarkuptrue%

%

\begin{isamarkuptext}%

A \emph{long name} consists of a sequence of non-empty 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 is called \emph{qualifier} (which may be

  empty).  The qualifier can be understood as the access path to the

  named entity while passing through some nested block-structure,

  although our free-form long names do not really enforce any strict

  discipline.

  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}.  In practice, long names

  usually represent 1--3 levels of qualification.  User ML code should

  not make any assumptions about the particular structure of long

  names!

  The empty name is commonly used as an indication of unnamed

  entities, or entities that are not entered into the corresponding

  name space, whenever this makes any sense.  The basic operations on

  long names map empty names again to empty names.%

\end{isamarkuptext}%

\isamarkuptrue%

%

\isadelimmlref

%

\endisadelimmlref

%

\isatagmlref

%

\begin{isamarkuptext}%

\begin{mldecls}

  \indexdef{}{ML}{Long\_Name.base\_name}\verb|Long_Name.base_name: string -> string| \\

  \indexdef{}{ML}{Long\_Name.qualifier}\verb|Long_Name.qualifier: string -> string| \\

  \indexdef{}{ML}{Long\_Name.append}\verb|Long_Name.append: string -> string -> string| \\

  \indexdef{}{ML}{Long\_Name.implode}\verb|Long_Name.implode: string list -> string| \\

  \indexdef{}{ML}{Long\_Name.explode}\verb|Long_Name.explode: string -> string list| \\

  \end{mldecls}

  \begin{description}

  \item \verb|Long_Name.base_name|~\isa{name} returns the base name

  of a long name.

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

  of a long name.

  \item \verb|Long_Name.append|~\isa{name\isactrlisub {\isadigit{1}}\ name\isactrlisub {\isadigit{2}}} appends two long

  names.

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

  representation and the explicit list form of long names.

  \end{description}%

\end{isamarkuptext}%

\isamarkuptrue%

%

\endisatagmlref

{\isafoldmlref}%

%

\isadelimmlref

%

\endisadelimmlref

%