doc-src/IsarImplementation/Thy/prelim.thy

more on contexts;

(* $Id$ *)

theory prelim imports base begin

chapter {* Preliminaries *}

section {* Named entities *}

text {* Named entities of different kinds (logical constant, type,
type class, theorem, method etc.) live in separate name spaces.  It is
usually clear from the occurrence of a name which kind of entity it
refers to.  For example, proof method @{text "foo"} vs.\ theorem
@{text "foo"} vs.\ logical constant @{text "foo"} are easily
distinguished by means of the syntactic context.  A notable exception
are logical identifiers within a term (\secref{sec:terms}): constants,
fixed variables, and bound variables all share the same identifier
syntax, but are distinguished by their scope.

Each name space is organized as a collection of \emph{qualified
names}, which consist of a sequence of basic name components separated
by dots: @{text "Bar.bar.foo"}, @{text "Bar.foo"}, and @{text "foo"}
are examples for valid qualified names.  Name components are
subdivided into \emph{symbols}, which constitute the smallest textual
unit in Isabelle --- raw characters are normally not encountered
directly. *}


subsection {* Strings of symbols *}

text {* Isabelle strings consist of a sequence of
symbols\glossary{Symbol}{The smalles unit of text in Isabelle,
subsumes plain ASCII characters as well as an infinite collection of
named symbols (for greek, math etc.).}, which are either packed as an
actual @{text "string"}, or represented as a list.  Each symbol is in
itself a small string of the following form:

\begin{enumerate}

\item either a singleton ASCII character ``@{text "c"}'' (with
character code 0--127), for example ``\verb,a,'',

\item or a regular symbol ``\verb,\,\verb,<,@{text "ident"}\verb,>,'',
for example ``\verb,\,\verb,<alpha>,'',

\item or a control symbol ``\verb,\,\verb,<^,@{text
"ident"}\verb,>,'', for example ``\verb,\,\verb,<^bold>,'',

\item or a raw control symbol ``\verb,\,\verb,<^raw:,@{text
"\<dots>"}\verb,>,'' where ``@{text "\<dots>"}'' refers to any
printable ASCII character (excluding ``\verb,.,'' and ``\verb,>,'') or
non-ASCII character, for example ``\verb,\,\verb,<^raw:$\sum_{i = 1}^n$>,'',

\item or a numbered raw control symbol ``\verb,\,\verb,<^raw,@{text
"nnn"}\verb,>, where @{text "nnn"} are digits, for example
``\verb,\,\verb,<^raw42>,''.

\end{enumerate}

The @{text "ident"} syntax for symbol names is @{text "letter (letter
| digit)\<^sup>*"}, where @{text "letter = A..Za..Z"} and @{text
"digit = 0..9"}.  There are infinitely many regular symbols and
control symbols available, but a certain collection of standard
symbols is treated specifically.  For example,
``\verb,\,\verb,<alpha>,'' is classified as a (non-ASCII) letter,
which means it may occur within regular Isabelle identifier syntax.

Output of symbols depends on the print mode (\secref{sec:print-mode}).
For example, the standard {\LaTeX} setup of the Isabelle document
preparation system would present ``\verb,\,\verb,<alpha>,'' as @{text
"\<alpha>"}, and ``\verb,\,\verb,<^bold>,\verb,\,\verb,<alpha>,'' as @{text
"\<^bold>\<alpha>"}.

\medskip It is important to note that the character set underlying
Isabelle symbols is plain 7-bit ASCII.  Since 8-bit characters are
passed through transparently, Isabelle may easily process actual
Unicode/UCS data (using the well-known UTF-8 encoding, for example).
Unicode provides its own collection of mathematical symbols, but there
is presently no link to Isabelle's named ones; both kinds of symbols
coexist independently. *}

text %mlref {*
  \begin{mldecls}
  @{index_ML_type "Symbol.symbol"} \\
  @{index_ML Symbol.explode: "string -> Symbol.symbol list"} \\
  @{index_ML Symbol.is_letter: "Symbol.symbol -> bool"} \\
  @{index_ML Symbol.is_digit: "Symbol.symbol -> bool"} \\
  @{index_ML Symbol.is_quasi: "Symbol.symbol -> bool"} \\
  @{index_ML Symbol.is_blank: "Symbol.symbol -> bool"} \\
  @{index_ML_type "Symbol.sym"} \\
  @{index_ML Symbol.decode: "Symbol.symbol -> Symbol.sym"} \\
  \end{mldecls}

  \begin{description}

  \item @{ML_type "Symbol.symbol"} represents Isabelle symbols; this type
  is merely an alias for @{ML_type "string"}, but emphasizes the
  specific format encountered here.

  \item @{ML "Symbol.explode"}~@{text "s"} produces an actual symbol
  list from the packed form usually encountered as user input.  This
  function replaces @{ML "String.explode"} for virtually all purposes
  of manipulating text in Isabelle!  Plain @{text "implode"} may be
  used for the reverse operation.

  \item @{ML "Symbol.is_letter"}, @{ML "Symbol.is_digit"}, @{ML
  "Symbol.is_quasi"}, @{ML "Symbol.is_blank"} classify certain symbols
  (both ASCII and several named ones) according to fixed syntactic
  convections of Isabelle, e.g.\ see \cite{isabelle-isar-ref}.

  \item @{ML_type "Symbol.sym"} is a concrete datatype that represents
  the different kinds of symbols explicitly as @{ML "Symbol.Char"},
  @{ML "Symbol.Sym"}, @{ML "Symbol.Ctrl"}, or @{ML "Symbol.Raw"}.

  \item @{ML "Symbol.decode"} converts the string representation of a
  symbol into the explicit datatype version.

  \end{description}
*}


subsection {* Simple names *}

text FIXME


subsection {* Qualified names and name spaces *}

text %FIXME {* Qualified names are constructed according to implicit naming
principles of the present context.


The last component is called \emph{base name}; the remaining prefix of
qualification may be empty.

Some practical conventions help to organize named entities more
systematically:

\begin{itemize}

\item Names are qualified first by the theory name, second by an
optional ``structure''.  For example, a constant @{text "c"} declared
as part of a certain structure @{text "b"} (say a type definition) in
theory @{text "A"} will be named @{text "A.b.c"} internally.

\item

\item

\item

\item

\end{itemize}

Names of different kinds of entities are basically independent, but
some practical naming conventions relate them to each other.  For
example, a constant @{text "foo"} may be accompanied with theorems
@{text "foo.intro"}, @{text "foo.elim"}, @{text "foo.simps"} etc.  The
same may happen for a type @{text "foo"}, which is then apt to cause
clashes in the theorem name space!  To avoid this, we occasionally
follow an additional convention of suffixes that determine the
original kind of entity that a name has been derived.  For example,
constant @{text "foo"} is associated with theorem @{text "foo.intro"},
type @{text "foo"} with theorem @{text "foo_type.intro"}, and type
class @{text "foo"} with @{text "foo_class.intro"}.

*}


section {* Structured output *}

subsection {* Pretty printing *}

text FIXME

subsection {* Output channels *}

text FIXME

subsection {* Print modes *}

text FIXME


section {* Contexts \label{sec:context} *}

text {*
  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 @{text "\<Gamma> \<turnstile>\<^sub>\<Theta> \<phi>"}, meaning that a
  proposition @{text "\<phi>"} is derivable from hypotheses @{text "\<Gamma>"}
  within the theory @{text "\<Theta>"}.  There are logical reasons for
  keeping @{text "\<Theta>"} and @{text "\<Gamma>"} separate: theories support type
  constructors and schematic polymorphism of constants and axioms,
  while the inner calculus of @{text "\<Gamma> \<turnstile> \<phi>"} 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.\ @{text "\<Gamma> \<turnstile>\<^sub>\<Theta> \<phi>"}
  implies @{text "\<Gamma>' \<turnstile>\<^sub>\<Theta>\<^sub>' \<phi>"} for contexts @{text "\<Theta>' \<supseteq>
  \<Theta>"} and @{text "\<Gamma>' \<supseteq> \<Gamma>"}.

  \item Export: discharge of hypotheses admits results to be exported
  into a smaller context, i.e.\ @{text "\<Gamma>' \<turnstile>\<^sub>\<Theta> \<phi>"} implies
  @{text "\<Gamma> \<turnstile>\<^sub>\<Theta> \<Delta> \<Longrightarrow> \<phi>"} where @{text "\<Gamma>' \<supseteq> \<Gamma>"} and @{text "\<Delta> =
  \<Gamma>' - \<Gamma>"}.  Note that @{text "\<Theta>"} remains unchanged here, only the
  @{text "\<Gamma>"} 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
  @{text "\<Theta>"} and @{text "\<Gamma>"} 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 @{text "\<Theta>"} and @{text "\<Gamma>"} 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 @{text "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.
*}


subsection {* Theory context \label{sec:context-theory} *}

text {*
  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 @{text "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 @{text "begin"} operation starts a new theory by importing
  several parent theories and entering a special @{text "draft"} mode,
  which is sustained until the final @{text "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 @{text "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 @{text "Pure"}.
  Theory @{text "Length"} imports @{text "Nat"} and @{text "List"}.
  The linear draft mode is enabled during the ``@{text "\<dots>"}'' 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$~~ \\
        &            & \multicolumn{3}{l}{~~$\isarkeyword{end}$} \\
  \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 @{text
  "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 @{text "finish"} operation.

  History operations are usually managed by the system, e.g.\ notably
  in the Isar transaction loop.

  \medskip
  FIXME theory data
*}


subsection {* Proof context \label{sec:context-proof} *}

text {*
  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 @{text "\<Gamma>
  \<turnstile> \<phi>"}, 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 @{text "\<Gamma>"} in
judgments @{text "\<Gamma> \<turnstile> \<phi>"} of natural deduction calculi.  There is a
generic notion of introducing and discharging hypotheses.  Arbritrary
auxiliary context data may be adjoined.}

*}


subsection {* Generic contexts *}

end