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