doc-src/IsarImplementation/Thy/document/prelim.tex
author wenzelm
Mon Jan 02 20:16:52 2006 +0100 (2006-01-02 ago)
changeset 18537 2681f9e34390
child 18554 bff7a1466fe4
permissions -rw-r--r--
"The Isabelle/Isar Implementation" manual;
wenzelm@18537
     1
%
wenzelm@18537
     2
\begin{isabellebody}%
wenzelm@18537
     3
\def\isabellecontext{prelim}%
wenzelm@18537
     4
%
wenzelm@18537
     5
\isadelimtheory
wenzelm@18537
     6
\isanewline
wenzelm@18537
     7
\isanewline
wenzelm@18537
     8
\isanewline
wenzelm@18537
     9
%
wenzelm@18537
    10
\endisadelimtheory
wenzelm@18537
    11
%
wenzelm@18537
    12
\isatagtheory
wenzelm@18537
    13
\isacommand{theory}\isamarkupfalse%
wenzelm@18537
    14
\ prelim\ \isakeyword{imports}\ base\ \isakeyword{begin}%
wenzelm@18537
    15
\endisatagtheory
wenzelm@18537
    16
{\isafoldtheory}%
wenzelm@18537
    17
%
wenzelm@18537
    18
\isadelimtheory
wenzelm@18537
    19
%
wenzelm@18537
    20
\endisadelimtheory
wenzelm@18537
    21
%
wenzelm@18537
    22
\isamarkupchapter{Preliminaries%
wenzelm@18537
    23
}
wenzelm@18537
    24
\isamarkuptrue%
wenzelm@18537
    25
%
wenzelm@18537
    26
\isamarkupsection{Named entities%
wenzelm@18537
    27
}
wenzelm@18537
    28
\isamarkuptrue%
wenzelm@18537
    29
%
wenzelm@18537
    30
\begin{isamarkuptext}%
wenzelm@18537
    31
Named entities of different kinds (logical constant, type,
wenzelm@18537
    32
type class, theorem, method etc.) live in separate name spaces.  It is
wenzelm@18537
    33
usually clear from the occurrence of a name which kind of entity it
wenzelm@18537
    34
refers to.  For example, proof method \isa{foo} vs.\ theorem
wenzelm@18537
    35
\isa{foo} vs.\ logical constant \isa{foo} are easily
wenzelm@18537
    36
distinguished by means of the syntactic context.  A notable exception
wenzelm@18537
    37
are logical identifiers within a term (\secref{sec:terms}): constants,
wenzelm@18537
    38
fixed variables, and bound variables all share the same identifier
wenzelm@18537
    39
syntax, but are distinguished by their scope.
wenzelm@18537
    40
wenzelm@18537
    41
Each name space is organized as a collection of \emph{qualified
wenzelm@18537
    42
names}, which consist of a sequence of basic name components separated
wenzelm@18537
    43
by dots: \isa{Bar{\isachardot}bar{\isachardot}foo}, \isa{Bar{\isachardot}foo}, and \isa{foo}
wenzelm@18537
    44
are examples for valid qualified names.  Name components are
wenzelm@18537
    45
subdivided into \emph{symbols}, which constitute the smallest textual
wenzelm@18537
    46
unit in Isabelle --- raw characters are normally not encountered
wenzelm@18537
    47
directly.%
wenzelm@18537
    48
\end{isamarkuptext}%
wenzelm@18537
    49
\isamarkuptrue%
wenzelm@18537
    50
%
wenzelm@18537
    51
\isamarkupsubsection{Strings of symbols%
wenzelm@18537
    52
}
wenzelm@18537
    53
\isamarkuptrue%
wenzelm@18537
    54
%
wenzelm@18537
    55
\begin{isamarkuptext}%
wenzelm@18537
    56
Isabelle strings consist of a sequence of
wenzelm@18537
    57
symbols\glossary{Symbol}{The smalles unit of text in Isabelle,
wenzelm@18537
    58
subsumes plain ASCII characters as well as an infinite collection of
wenzelm@18537
    59
named symbols (for greek, math etc.).}, which are either packed as an
wenzelm@18537
    60
actual \isa{string}, or represented as a list.  Each symbol is in
wenzelm@18537
    61
itself a small string of the following form:
wenzelm@18537
    62
wenzelm@18537
    63
\begin{enumerate}
wenzelm@18537
    64
wenzelm@18537
    65
\item either a singleton ASCII character ``\isa{c}'' (with
wenzelm@18537
    66
character code 0--127), for example ``\verb,a,'',
wenzelm@18537
    67
wenzelm@18537
    68
\item or a regular symbol ``\verb,\,\verb,<,\isa{ident}\verb,>,'',
wenzelm@18537
    69
for example ``\verb,\,\verb,<alpha>,'',
wenzelm@18537
    70
wenzelm@18537
    71
\item or a control symbol ``\verb,\,\verb,<^,\isa{ident}\verb,>,'', for example ``\verb,\,\verb,<^bold>,'',
wenzelm@18537
    72
wenzelm@18537
    73
\item or a raw control symbol ``\verb,\,\verb,<^raw:,\isa{{\isasymdots}}\verb,>,'' where ``\isa{{\isasymdots}}'' refers to any printable ASCII
wenzelm@18537
    74
character (excluding ``\verb,>,'') or non-ASCII character, for example
wenzelm@18537
    75
``\verb,\,\verb,<^raw:$\sum_{i = 1}^n$>,'',
wenzelm@18537
    76
wenzelm@18537
    77
\item or a numbered raw control symbol ``\verb,\,\verb,<^raw,\isa{nnn}\verb,>, where \isa{nnn} are digits, for example
wenzelm@18537
    78
``\verb,\,\verb,<^raw42>,''.
wenzelm@18537
    79
wenzelm@18537
    80
\end{enumerate}
wenzelm@18537
    81
wenzelm@18537
    82
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
wenzelm@18537
    83
control symbols available, but a certain collection of standard
wenzelm@18537
    84
symbols is treated specifically.  For example,
wenzelm@18537
    85
``\verb,\,\verb,<alpha>,'' is classified as a (non-ASCII) letter,
wenzelm@18537
    86
which means it may occur within regular Isabelle identifier syntax.
wenzelm@18537
    87
wenzelm@18537
    88
Output of symbols depends on the print mode (\secref{sec:print-mode}).
wenzelm@18537
    89
For example, the standard {\LaTeX} setup of the Isabelle document
wenzelm@18537
    90
preparation system would present ``\verb,\,\verb,<alpha>,'' as \isa{{\isasymalpha}}, and ``\verb,\,\verb,<^bold>,\verb,\,\verb,<alpha>,'' as \isa{\isactrlbold {\isasymalpha}}.
wenzelm@18537
    91
wenzelm@18537
    92
\medskip It is important to note that the character set underlying
wenzelm@18537
    93
Isabelle symbols is plain 7-bit ASCII.  Since 8-bit characters are
wenzelm@18537
    94
passed through transparently, Isabelle may easily process actual
wenzelm@18537
    95
Unicode/UCS data (using the well-known UTF-8 encoding, for example).
wenzelm@18537
    96
Unicode provides its own collection of mathematical symbols, but there
wenzelm@18537
    97
is presently no link to Isabelle's named ones; both kinds of symbols
wenzelm@18537
    98
coexist independently.%
wenzelm@18537
    99
\end{isamarkuptext}%
wenzelm@18537
   100
\isamarkuptrue%
wenzelm@18537
   101
%
wenzelm@18537
   102
\isadelimmlref
wenzelm@18537
   103
%
wenzelm@18537
   104
\endisadelimmlref
wenzelm@18537
   105
%
wenzelm@18537
   106
\isatagmlref
wenzelm@18537
   107
%
wenzelm@18537
   108
\begin{isamarkuptext}%
wenzelm@18537
   109
\begin{mldecls}
wenzelm@18537
   110
  \indexmltype{Symbol.symbol}\verb|type Symbol.symbol| \\
wenzelm@18537
   111
  \indexml{Symbol.explode}\verb|Symbol.explode: string -> Symbol.symbol list| \\
wenzelm@18537
   112
  \indexml{Symbol.is-letter}\verb|Symbol.is_letter: Symbol.symbol -> bool| \\
wenzelm@18537
   113
  \indexml{Symbol.is-digit}\verb|Symbol.is_digit: Symbol.symbol -> bool| \\
wenzelm@18537
   114
  \indexml{Symbol.is-quasi}\verb|Symbol.is_quasi: Symbol.symbol -> bool| \\
wenzelm@18537
   115
  \indexml{Symbol.is-blank}\verb|Symbol.is_blank: Symbol.symbol -> bool| \\
wenzelm@18537
   116
  \indexmltype{Symbol.sym}\verb|type Symbol.sym| \\
wenzelm@18537
   117
  \indexml{Symbol.decode}\verb|Symbol.decode: Symbol.symbol -> Symbol.sym| \\
wenzelm@18537
   118
  \end{mldecls}
wenzelm@18537
   119
wenzelm@18537
   120
  \begin{description}
wenzelm@18537
   121
wenzelm@18537
   122
  \item \verb|Symbol.symbol| represents Isabelle symbols; this type
wenzelm@18537
   123
  is merely an alias for \verb|string|, but emphasizes the
wenzelm@18537
   124
  specific format encountered here.
wenzelm@18537
   125
wenzelm@18537
   126
  \item \verb|Symbol.explode|~\isa{s} produces an actual symbol
wenzelm@18537
   127
  list from the packed form usually encountered as user input.  This
wenzelm@18537
   128
  function replaces \verb|String.explode| for virtually all purposes
wenzelm@18537
   129
  of manipulating text in Isabelle!  Plain \isa{implode} may be
wenzelm@18537
   130
  used for the reverse operation.
wenzelm@18537
   131
wenzelm@18537
   132
  \item \verb|Symbol.is_letter|, \verb|Symbol.is_digit|, \verb|Symbol.is_quasi|, \verb|Symbol.is_blank| classify certain symbols
wenzelm@18537
   133
  (both ASCII and several named ones) according to fixed syntactic
wenzelm@18537
   134
  convections of Isabelle, e.g.\ see \cite{isabelle-isar-ref}.
wenzelm@18537
   135
wenzelm@18537
   136
  \item \verb|Symbol.sym| is a concrete datatype that represents
wenzelm@18537
   137
  the different kinds of symbols explicitly as \verb|Symbol.Char|,
wenzelm@18537
   138
  \verb|Symbol.Sym|, \verb|Symbol.Ctrl|, or \verb|Symbol.Raw|.
wenzelm@18537
   139
wenzelm@18537
   140
  \item \verb|Symbol.decode| converts the string representation of a
wenzelm@18537
   141
  symbol into the explicit datatype version.
wenzelm@18537
   142
wenzelm@18537
   143
  \end{description}%
wenzelm@18537
   144
\end{isamarkuptext}%
wenzelm@18537
   145
\isamarkuptrue%
wenzelm@18537
   146
%
wenzelm@18537
   147
\endisatagmlref
wenzelm@18537
   148
{\isafoldmlref}%
wenzelm@18537
   149
%
wenzelm@18537
   150
\isadelimmlref
wenzelm@18537
   151
%
wenzelm@18537
   152
\endisadelimmlref
wenzelm@18537
   153
%
wenzelm@18537
   154
\isamarkupsubsection{Qualified names and name spaces%
wenzelm@18537
   155
}
wenzelm@18537
   156
\isamarkuptrue%
wenzelm@18537
   157
%
wenzelm@18537
   158
\isadelimFIXME
wenzelm@18537
   159
%
wenzelm@18537
   160
\endisadelimFIXME
wenzelm@18537
   161
%
wenzelm@18537
   162
\isatagFIXME
wenzelm@18537
   163
%
wenzelm@18537
   164
\begin{isamarkuptext}%
wenzelm@18537
   165
Qualified names are constructed according to implicit naming
wenzelm@18537
   166
principles of the present context.
wenzelm@18537
   167
wenzelm@18537
   168
wenzelm@18537
   169
The last component is called \emph{base name}; the remaining prefix of
wenzelm@18537
   170
qualification may be empty.
wenzelm@18537
   171
wenzelm@18537
   172
Some practical conventions help to organize named entities more
wenzelm@18537
   173
systematically:
wenzelm@18537
   174
wenzelm@18537
   175
\begin{itemize}
wenzelm@18537
   176
wenzelm@18537
   177
\item Names are qualified first by the theory name, second by an
wenzelm@18537
   178
optional ``structure''.  For example, a constant \isa{c} declared
wenzelm@18537
   179
as part of a certain structure \isa{b} (say a type definition) in
wenzelm@18537
   180
theory \isa{A} will be named \isa{A{\isachardot}b{\isachardot}c} internally.
wenzelm@18537
   181
wenzelm@18537
   182
\item
wenzelm@18537
   183
wenzelm@18537
   184
\item
wenzelm@18537
   185
wenzelm@18537
   186
\item
wenzelm@18537
   187
wenzelm@18537
   188
\item
wenzelm@18537
   189
wenzelm@18537
   190
\end{itemize}
wenzelm@18537
   191
wenzelm@18537
   192
Names of different kinds of entities are basically independent, but
wenzelm@18537
   193
some practical naming conventions relate them to each other.  For
wenzelm@18537
   194
example, a constant \isa{foo} may be accompanied with theorems
wenzelm@18537
   195
\isa{foo{\isachardot}intro}, \isa{foo{\isachardot}elim}, \isa{foo{\isachardot}simps} etc.  The
wenzelm@18537
   196
same may happen for a type \isa{foo}, which is then apt to cause
wenzelm@18537
   197
clashes in the theorem name space!  To avoid this, we occasionally
wenzelm@18537
   198
follow an additional convention of suffixes that determine the
wenzelm@18537
   199
original kind of entity that a name has been derived.  For example,
wenzelm@18537
   200
constant \isa{foo} is associated with theorem \isa{foo{\isachardot}intro},
wenzelm@18537
   201
type \isa{foo} with theorem \isa{foo{\isacharunderscore}type{\isachardot}intro}, and type
wenzelm@18537
   202
class \isa{foo} with \isa{foo{\isacharunderscore}class{\isachardot}intro}.%
wenzelm@18537
   203
\end{isamarkuptext}%
wenzelm@18537
   204
\isamarkuptrue%
wenzelm@18537
   205
%
wenzelm@18537
   206
\endisatagFIXME
wenzelm@18537
   207
{\isafoldFIXME}%
wenzelm@18537
   208
%
wenzelm@18537
   209
\isadelimFIXME
wenzelm@18537
   210
%
wenzelm@18537
   211
\endisadelimFIXME
wenzelm@18537
   212
%
wenzelm@18537
   213
\isamarkupsection{Structured output%
wenzelm@18537
   214
}
wenzelm@18537
   215
\isamarkuptrue%
wenzelm@18537
   216
%
wenzelm@18537
   217
\isamarkupsubsection{Pretty printing%
wenzelm@18537
   218
}
wenzelm@18537
   219
\isamarkuptrue%
wenzelm@18537
   220
%
wenzelm@18537
   221
\begin{isamarkuptext}%
wenzelm@18537
   222
FIXME%
wenzelm@18537
   223
\end{isamarkuptext}%
wenzelm@18537
   224
\isamarkuptrue%
wenzelm@18537
   225
%
wenzelm@18537
   226
\isamarkupsubsection{Output channels%
wenzelm@18537
   227
}
wenzelm@18537
   228
\isamarkuptrue%
wenzelm@18537
   229
%
wenzelm@18537
   230
\begin{isamarkuptext}%
wenzelm@18537
   231
FIXME%
wenzelm@18537
   232
\end{isamarkuptext}%
wenzelm@18537
   233
\isamarkuptrue%
wenzelm@18537
   234
%
wenzelm@18537
   235
\isamarkupsubsection{Print modes%
wenzelm@18537
   236
}
wenzelm@18537
   237
\isamarkuptrue%
wenzelm@18537
   238
%
wenzelm@18537
   239
\begin{isamarkuptext}%
wenzelm@18537
   240
FIXME%
wenzelm@18537
   241
\end{isamarkuptext}%
wenzelm@18537
   242
\isamarkuptrue%
wenzelm@18537
   243
%
wenzelm@18537
   244
\isamarkupsection{Context \label{sec:context}%
wenzelm@18537
   245
}
wenzelm@18537
   246
\isamarkuptrue%
wenzelm@18537
   247
%
wenzelm@18537
   248
\isadelimFIXME
wenzelm@18537
   249
%
wenzelm@18537
   250
\endisadelimFIXME
wenzelm@18537
   251
%
wenzelm@18537
   252
\isatagFIXME
wenzelm@18537
   253
%
wenzelm@18537
   254
\begin{isamarkuptext}%
wenzelm@18537
   255
What is a context anyway?  A highly advanced
wenzelm@18537
   256
technological and cultural achievement, which took humanity several
wenzelm@18537
   257
thousands of years to be develop, is writing with pen-and-paper.  Here
wenzelm@18537
   258
the paper is the context, or medium.  It accommodates a certain range
wenzelm@18537
   259
of different kinds of pens, but also has some inherent limitations.
wenzelm@18537
   260
For example, carved inscriptions are better done on solid material
wenzelm@18537
   261
like wood or stone.
wenzelm@18537
   262
wenzelm@18537
   263
Isabelle/Isar distinguishes two key notions of context: \emph{theory
wenzelm@18537
   264
  context}\indexbold{theory context} and \emph{proof context}.\indexbold{proof
wenzelm@18537
   265
  context} To motivate this fundamental division consider the very idea of
wenzelm@18537
   266
logical reasoning which is about judgments $\Gamma \Drv{\Theta} \phi$, where
wenzelm@18537
   267
$\Theta$ is the background theory with declarations of operators and axioms
wenzelm@18537
   268
stating their properties, and $\Gamma$ a collection of hypotheses emerging
wenzelm@18537
   269
temporarily during proof.  For example, the rule of implication-introduction
wenzelm@18537
   270
\[
wenzelm@18537
   271
\infer{\Gamma \Drv{\Theta} A \Imp B}{\Gamma, A \Drv{\Theta} B}
wenzelm@18537
   272
\]
wenzelm@18537
   273
can be read as ``to show $A \Imp B$ we may assume $A$ as hypothesis and need
wenzelm@18537
   274
to show $B$''.  It is characteristic that $\Theta$ is unchanged and $\Gamma$
wenzelm@18537
   275
is only modified according to some general patterns of ``assuming'' and
wenzelm@18537
   276
``discharging'' hypotheses.  This admits the following abbreviated notation,
wenzelm@18537
   277
where the fixed $\Theta$ and locally changed $\Gamma$ are left implicit:
wenzelm@18537
   278
\[
wenzelm@18537
   279
\infer{A \Imp B}{\infer*{B}{[A]}}
wenzelm@18537
   280
\]
wenzelm@18537
   281
wenzelm@18537
   282
In some logical traditions (e.g.\ Type Theory) there is a tendency to
wenzelm@18537
   283
unify all kinds of declarations within a single notion of context.
wenzelm@18537
   284
This is theoretically very nice, but also more demanding, because
wenzelm@18537
   285
everything is internalized into the logical calculus itself.
wenzelm@18537
   286
Isabelle/Pure is a very simple logic, but achieves many practically
wenzelm@18537
   287
useful concepts by differentiating various basic elements.
wenzelm@18537
   288
wenzelm@18537
   289
Take polymorphism, for example.  Instead of embarking on the
wenzelm@18537
   290
adventurous enterprise of full higher-order logic with full
wenzelm@18537
   291
type-quantification and polymorphic entities, Isabelle/Pure merely
wenzelm@18537
   292
takes a stripped-down version of Church's Simple Type Theory
wenzelm@18537
   293
\cite{church40}.  Then after the tradition of Gordon's HOL
wenzelm@18537
   294
\cite{mgordon-hol} it is fairly easy to introduce syntactic notions of
wenzelm@18537
   295
type variables and type-constructors, and require every theory
wenzelm@18537
   296
$\Theta$ being closed by type instantiation.  Whenever we wish to
wenzelm@18537
   297
reason with a polymorphic constant or axiom scheme at a particular
wenzelm@18537
   298
type, we may assume that it has been referenced initially at that very
wenzelm@18537
   299
instance (due to the Deduction Theorem).  Thus we achieve the
wenzelm@18537
   300
following \emph{admissible
wenzelm@18537
   301
  rule}\glossary{Admissible rule}{FIXME} of schematic type-instantiation:
wenzelm@18537
   302
wenzelm@18537
   303
\[
wenzelm@18537
   304
\infer{\phi(\tau)}{\infer*{\phi(\alpha)}{[\alpha]}}
wenzelm@18537
   305
\]
wenzelm@18537
   306
wenzelm@18537
   307
Using this approach, the structured Isar proof language offers
wenzelm@18537
   308
schematic polymorphism within nested sub-proofs -- similar to that of
wenzelm@18537
   309
polymorphic let-bindings according to Hindley-Milner.\
wenzelm@18537
   310
\cite{milner78}.  All of this is achieved without disintegrating the
wenzelm@18537
   311
rather simplistic logical core.  On the other hand, the succinct rule
wenzelm@18537
   312
presented above already involves rather delicate interaction of the
wenzelm@18537
   313
theory and proof context (with side-conditions not mentioned here),
wenzelm@18537
   314
and unwinding an admissible rule involves induction over derivations.
wenzelm@18537
   315
All of this diversity needs to be accomodated by the system
wenzelm@18537
   316
architecture and actual implementation.
wenzelm@18537
   317
wenzelm@18537
   318
\medskip Despite these important observations, Isabelle/Isar is not just a
wenzelm@18537
   319
logical calculus, there are further extra-logical aspects to be considered.
wenzelm@18537
   320
Practical experience over the years suggests two context data structures which
wenzelm@18537
   321
are used in rather dissimilar manners, even though there is a considerable
wenzelm@18537
   322
overlap of underlying ideas.
wenzelm@18537
   323
wenzelm@18537
   324
From the system's perspective the mode of use of theory vs.\ proof context is
wenzelm@18537
   325
the key distinction.  The actual content is merely a generic slot for
wenzelm@18537
   326
\emph{theory data} and \emph{proof data}, respectively.  There are generic
wenzelm@18537
   327
interfaces to declare data entries at any time.  Even the core logic of
wenzelm@18537
   328
Isabelle/Pure registers its very own notion of theory context data (types,
wenzelm@18537
   329
constants, axioms etc.) like any other Isabelle tool out there.  Likewise, the
wenzelm@18537
   330
essentials of Isar proof contexts are one proof data slot among many others,
wenzelm@18537
   331
notably those of derived Isar concepts (e.g.\ calculational reasoning rules).
wenzelm@18537
   332
wenzelm@18537
   333
In that respect, a theory is more like a stone tablet to carve long-lasting
wenzelm@18537
   334
inscriptions -- but take care not to break it!  While a proof context is like
wenzelm@18537
   335
a block of paper to scribble and dispose quickly.  More recently Isabelle has
wenzelm@18537
   336
started to cultivate the paper-based craftsmanship a bit further, by
wenzelm@18537
   337
maintaining small collections of paper booklets, better known as locales.
wenzelm@18537
   338
wenzelm@18537
   339
Thus we achive ``thick'' augmented versions of {\boldmath$\Theta$} and
wenzelm@18537
   340
{\boldmath$\Gamma$} to support realistic structured reasoning within a
wenzelm@18537
   341
practically usable system.%
wenzelm@18537
   342
\end{isamarkuptext}%
wenzelm@18537
   343
\isamarkuptrue%
wenzelm@18537
   344
%
wenzelm@18537
   345
\endisatagFIXME
wenzelm@18537
   346
{\isafoldFIXME}%
wenzelm@18537
   347
%
wenzelm@18537
   348
\isadelimFIXME
wenzelm@18537
   349
%
wenzelm@18537
   350
\endisadelimFIXME
wenzelm@18537
   351
%
wenzelm@18537
   352
\isamarkupsubsection{Theory context \label{sec:context-theory}%
wenzelm@18537
   353
}
wenzelm@18537
   354
\isamarkuptrue%
wenzelm@18537
   355
%
wenzelm@18537
   356
\isadelimFIXME
wenzelm@18537
   357
%
wenzelm@18537
   358
\endisadelimFIXME
wenzelm@18537
   359
%
wenzelm@18537
   360
\isatagFIXME
wenzelm@18537
   361
%
wenzelm@18537
   362
\begin{isamarkuptext}%
wenzelm@18537
   363
A theory context consists of management information plus the
wenzelm@18537
   364
actual data, which may be declared by other software modules later on.
wenzelm@18537
   365
The management part is surprisingly complex, we illustrate it by the
wenzelm@18537
   366
following typical situation of incremental theory development.
wenzelm@18537
   367
wenzelm@18537
   368
\begin{tabular}{rcccl}
wenzelm@18537
   369
        &            & $Pure$ \\
wenzelm@18537
   370
        &            & $\downarrow$ \\
wenzelm@18537
   371
        &            & $FOL$ \\
wenzelm@18537
   372
        & $\swarrow$ &              & $\searrow$ & \\
wenzelm@18537
   373
  $Nat$ &            &              &            & $List$ \\
wenzelm@18537
   374
        & $\searrow$ &              & $\swarrow$ \\
wenzelm@18537
   375
        &            & $Length$ \\
wenzelm@18537
   376
        &            & \multicolumn{3}{l}{~~$\isarkeyword{imports}$} \\
wenzelm@18537
   377
        &            & \multicolumn{3}{l}{~~$\isarkeyword{begin}$} \\
wenzelm@18537
   378
        &            & $\vdots$~~ \\
wenzelm@18537
   379
        &            & $\bullet$~~ \\
wenzelm@18537
   380
        &            & $\vdots$~~ \\
wenzelm@18537
   381
        &            & $\bullet$~~ \\
wenzelm@18537
   382
        &            & $\vdots$~~ \\
wenzelm@18537
   383
        &            & \multicolumn{3}{l}{~~$\isarkeyword{end}$} \\
wenzelm@18537
   384
\end{tabular}
wenzelm@18537
   385
wenzelm@18537
   386
\begin{itemize}
wenzelm@18537
   387
\item \emph{name}, \emph{parents} and \emph{ancestors}
wenzelm@18537
   388
\item \emph{identity}
wenzelm@18537
   389
\item \emph{intermediate versions}
wenzelm@18537
   390
\end{itemize}
wenzelm@18537
   391
wenzelm@18537
   392
\begin{description}
wenzelm@18537
   393
\item [draft]
wenzelm@18537
   394
\item [intermediate]
wenzelm@18537
   395
\item [finished]
wenzelm@18537
   396
\end{description}
wenzelm@18537
   397
wenzelm@18537
   398
\emph{theory reference}%
wenzelm@18537
   399
\end{isamarkuptext}%
wenzelm@18537
   400
\isamarkuptrue%
wenzelm@18537
   401
%
wenzelm@18537
   402
\endisatagFIXME
wenzelm@18537
   403
{\isafoldFIXME}%
wenzelm@18537
   404
%
wenzelm@18537
   405
\isadelimFIXME
wenzelm@18537
   406
%
wenzelm@18537
   407
\endisadelimFIXME
wenzelm@18537
   408
%
wenzelm@18537
   409
\isamarkupsubsection{Proof context \label{sec:context-proof}%
wenzelm@18537
   410
}
wenzelm@18537
   411
\isamarkuptrue%
wenzelm@18537
   412
%
wenzelm@18537
   413
\begin{isamarkuptext}%
wenzelm@18537
   414
FIXME
wenzelm@18537
   415
wenzelm@18537
   416
\glossary{Proof context}{The static context of a structured proof,
wenzelm@18537
   417
acts like a local ``theory'' of the current portion of Isar proof
wenzelm@18537
   418
text, generalizes the idea of local hypotheses \isa{{\isasymGamma}} in
wenzelm@18537
   419
judgments \isa{{\isasymGamma}\ {\isasymturnstile}\ {\isasymphi}} of natural deduction calculi.  There is a
wenzelm@18537
   420
generic notion of introducing and discharging hypotheses.  Arbritrary
wenzelm@18537
   421
auxiliary context data may be adjoined.}%
wenzelm@18537
   422
\end{isamarkuptext}%
wenzelm@18537
   423
\isamarkuptrue%
wenzelm@18537
   424
%
wenzelm@18537
   425
\isadelimtheory
wenzelm@18537
   426
%
wenzelm@18537
   427
\endisadelimtheory
wenzelm@18537
   428
%
wenzelm@18537
   429
\isatagtheory
wenzelm@18537
   430
\isacommand{end}\isamarkupfalse%
wenzelm@18537
   431
%
wenzelm@18537
   432
\endisatagtheory
wenzelm@18537
   433
{\isafoldtheory}%
wenzelm@18537
   434
%
wenzelm@18537
   435
\isadelimtheory
wenzelm@18537
   436
%
wenzelm@18537
   437
\endisadelimtheory
wenzelm@18537
   438
\isanewline
wenzelm@18537
   439
\end{isabellebody}%
wenzelm@18537
   440
%%% Local Variables:
wenzelm@18537
   441
%%% mode: latex
wenzelm@18537
   442
%%% TeX-master: "root"
wenzelm@18537
   443
%%% End: