doc-src/IsarImplementation/Thy/document/prelim.tex

 {\isafoldmlref}%
 %
 \isadelimmlref
 %
 \endisadelimmlref
+%
+\isamarkupsubsection{Simple names%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+FIXME%
+\end{isamarkuptext}%
+\isamarkuptrue%
 %
 \isamarkupsubsection{Qualified names and name spaces%
 }
 \isamarkuptrue%
 %

 \begin{isamarkuptext}%
 FIXME%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
-\isamarkupsection{Context \label{sec:context}%
-}
-\isamarkuptrue%
-%
-\isadelimFIXME
-%
-\endisadelimFIXME
-%
-\isatagFIXME
-%
-\begin{isamarkuptext}%
-What is a context anyway?  A highly advanced
-technological and cultural achievement, which took humanity several
-thousands of years to be develop, is writing with pen-and-paper.  Here
-the paper is the context, or medium.  It accommodates a certain range
-of different kinds of pens, but also has some inherent limitations.
-For example, carved inscriptions are better done on solid material
-like wood or stone.
-
-Isabelle/Isar distinguishes two key notions of context: \emph{theory
-context} and \emph{proof context}.  To motivate this fundamental
-division consider the very idea of logical reasoning which is about
-judgments $\Gamma \Drv{\Theta} \phi$, where $\Theta$ is the background
-theory with declarations of operators and axioms stating their
-properties, and $\Gamma$ a collection of hypotheses emerging
-temporarily during proof.  For example, the rule of
-implication-introduction \[ \infer{\Gamma \Drv{\Theta} A \Imp
-B}{\Gamma, A \Drv{\Theta} B} \] can be read as ``to show $A \Imp B$ we
-may assume $A$ as hypothesis and need to show $B$''.  It is
-characteristic that $\Theta$ is unchanged and $\Gamma$ is only
-modified according to some general patterns of ``assuming'' and
-``discharging'' hypotheses.  This admits the following abbreviated
-notation, where the fixed $\Theta$ and locally changed $\Gamma$ are
-left implicit: \[ \infer{A \Imp B}{\infer*{B}{[A]}} \]
-
-In some logical traditions (e.g.\ Type Theory) there is a tendency to
-unify all kinds of declarations within a single notion of context.
-This is theoretically very nice, but also more demanding, because
-everything is internalized into the logical calculus itself.
-Isabelle/Pure is a very simple logic, but achieves many practically
-useful concepts by differentiating various basic elements.
-
-Take polymorphism, for example.  Instead of embarking on the
-adventurous enterprise of full higher-order logic with full
-type-quantification and polymorphic entities, Isabelle/Pure merely
-takes a stripped-down version of Church's Simple Type Theory
-\cite{church40}.  Then after the tradition of Gordon's HOL
-\cite{mgordon-hol} it is fairly easy to introduce syntactic notions of
-type variables and type-constructors, and require every theory
-$\Theta$ being closed by type instantiation.  Whenever we wish to
-reason with a polymorphic constant or axiom scheme at a particular
-type, we may assume that it has been referenced initially at that very
-instance (due to the Deduction Theorem).  Thus we achieve the
-following \emph{admissible
-  rule}\glossary{Admissible rule}{FIXME} of schematic type-instantiation:
-
-\[
-\infer{\phi(\tau)}{\infer*{\phi(\alpha)}{[\alpha]}}
-\]
-
-Using this approach, the structured Isar proof language offers
-schematic polymorphism within nested sub-proofs -- similar to that of
-polymorphic let-bindings according to Hindley-Milner.\
-\cite{milner78}.  All of this is achieved without disintegrating the
-rather simplistic logical core.  On the other hand, the succinct rule
-presented above already involves rather delicate interaction of the
-theory and proof context (with side-conditions not mentioned here),
-and unwinding an admissible rule involves induction over derivations.
-All of this diversity needs to be accomodated by the system
-architecture and actual implementation.
-
-\medskip Despite these important observations, Isabelle/Isar is not just a
-logical calculus, there are further extra-logical aspects to be considered.
-Practical experience over the years suggests two context data structures which
-are used in rather dissimilar manners, even though there is a considerable
-overlap of underlying ideas.
-
-From the system's perspective the mode of use of theory vs.\ proof context is
-the key distinction.  The actual content is merely a generic slot for
-\emph{theory data} and \emph{proof data}, respectively.  There are generic
-interfaces to declare data entries at any time.  Even the core logic of
-Isabelle/Pure registers its very own notion of theory context data (types,
-constants, axioms etc.) like any other Isabelle tool out there.  Likewise, the
-essentials of Isar proof contexts are one proof data slot among many others,
-notably those of derived Isar concepts (e.g.\ calculational reasoning rules).
-
-In that respect, a theory is more like a stone tablet to carve long-lasting
-inscriptions -- but take care not to break it!  While a proof context is like
-a block of paper to scribble and dispose quickly.  More recently Isabelle has
-started to cultivate the paper-based craftsmanship a bit further, by
-maintaining small collections of paper booklets, better known as locales.
-
-Thus we achive ``thick'' augmented versions of {\boldmath$\Theta$} and
-{\boldmath$\Gamma$} to support realistic structured reasoning within a
-practically usable system.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\endisatagFIXME
-{\isafoldFIXME}%
-%
-\isadelimFIXME
-%
-\endisadelimFIXME
+\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%
 %
-\isadelimFIXME
-%
-\endisadelimFIXME
-%
-\isatagFIXME
-%
-\begin{isamarkuptext}%
-A theory context consists of management information plus the
-actual data, which may be declared by other software modules later on.
-The management part is surprisingly complex, we illustrate it by the
-following typical situation of incremental theory development.
-
-\begin{tabular}{rcccl}
+\begin{isamarkuptext}%
+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{copy} operation
+  produces an auxiliary version with 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 example below shows a theory graph derived from \isa{Pure}.
+  Theory \isa{Length} imports \isa{Nat} and \isa{List}.
+  The linear draft mode is enabled during the ``\isa{{\isasymdots}}'' stage of
+  the theory body.
+
+  \bigskip
+  \begin{tabular}{rcccl}
         &            & $Pure$ \\
         &            & $\downarrow$ \\
         &            & $FOL$ \\
         & $\swarrow$ &              & $\searrow$ & \\
   $Nat$ &            &              &            & $List$ \\
         & $\searrow$ &              & $\swarrow$ \\
         &            & $Length$ \\
         &            & \multicolumn{3}{l}{~~$\isarkeyword{imports}$} \\
         &            & \multicolumn{3}{l}{~~$\isarkeyword{begin}$} \\
         &            & $\vdots$~~ \\
-        &            & $\bullet$~~ \\
-        &            & $\vdots$~~ \\
-        &            & $\bullet$~~ \\
-        &            & $\vdots$~~ \\
         &            & \multicolumn{3}{l}{~~$\isarkeyword{end}$} \\
-\end{tabular}
-
-\begin{itemize}
-\item \emph{name}, \emph{parents} and \emph{ancestors}
-\item \emph{identity}
-\item \emph{intermediate versions}
-\end{itemize}
-
-\begin{description}
-\item [draft]
-\item [intermediate]
-\item [finished]
-\end{description}
-
-\emph{theory reference}%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\endisatagFIXME
-{\isafoldFIXME}%
-%
-\isadelimFIXME
-%
-\endisadelimFIXME
+  \end{tabular}
+
+  \medskip In practice, derived theory operations mostly operate
+  drafts, namely the body of the current portion of theory that the
+  user happens to be composing.
+
+ \medskip There is also a builtin theory history mechanism that amends for
+  the destructive behaviour of theory drafts.  The \isa{checkpoint} operation produces an intermediate stepping stone that
+  survives the next update unscathed: both the original and the
+  changed theory remain valid and are related by the sub-theory
+  relation.  This recovering of pure theory values comes at the cost
+  of extra internal bookeeping.  The cumulative effect of
+  checkpointing is purged by the \isa{finish} operation.
+
+  History operations are usually managed by the system, e.g.\ notably
+  in the Isar transaction loop.
+
+  \medskip
+  FIXME theory data%
+\end{isamarkuptext}%
+\isamarkuptrue%
 %
 \isamarkupsubsection{Proof context \label{sec:context-proof}%
 }
 \isamarkuptrue%
 %
 \begin{isamarkuptext}%
-FIXME
+A proof context is an arbitrary container that is initialized from a
+  given theory.  The result contains a back-reference to the theory it
+  belongs to, together with pure data.  No further bookkeeping is
+  required here, thanks to the lack of destructive features.
+
+  There is no restriction on producing proof contexts, although the
+  usual discipline is to follow block structure as a mental model: a
+  given context is extended consecutively, results are exported back
+  into the original context.  In particular, the concept of Isar proof
+  state models block-structured reasoning explicitly, using a stack of
+  proof contexts.
+
+  Due to the lack of identification and back-referencing, entities
+  derived in a proof context need to record inherent logical
+  requirements explicitly.  For example, hypotheses used in a
+  derivation will be recorded separately within the sequent \isa{{\isasymGamma}\ {\isasymturnstile}\ {\isasymphi}}, just to make double sure.  Results could leak into an alien
+  proof context do to programming errors, but Isabelle/Isar
+  occasionally includes extra validity checks at the end of a
+  sub-proof.
+
+  \medskip
+  FIXME proof data
 
 \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.}%
 \end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsection{Generic contexts%
+}
 \isamarkuptrue%
 %
 \isadelimtheory
 %
 \endisadelimtheory