doc-src/IsarImplementation/Thy/document/prelim.tex
author wenzelm
Thu, 31 Aug 2006 14:53:55 +0200
changeset 20447 5b75f1c4d7d6
parent 20438 9060c73a4578
child 20449 f8a7a8236c68
permissions -rw-r--r--
more on contexts;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
18537
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
     1
%
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
     2
\begin{isabellebody}%
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
     3
\def\isabellecontext{prelim}%
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
     4
%
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
     5
\isadelimtheory
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
     6
\isanewline
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
     7
\isanewline
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
     8
\isanewline
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
     9
%
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    10
\endisadelimtheory
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    11
%
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    12
\isatagtheory
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    13
\isacommand{theory}\isamarkupfalse%
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    14
\ prelim\ \isakeyword{imports}\ base\ \isakeyword{begin}%
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    15
\endisatagtheory
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    16
{\isafoldtheory}%
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    17
%
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    18
\isadelimtheory
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    19
%
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    20
\endisadelimtheory
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    21
%
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    22
\isamarkupchapter{Preliminaries%
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    23
}
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    24
\isamarkuptrue%
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    25
%
20429
116255c9209b more on contexts;
wenzelm
parents: 20215
diff changeset
    26
\isamarkupsection{Contexts \label{sec:context}%
18537
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    27
}
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    28
\isamarkuptrue%
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    29
%
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    30
\begin{isamarkuptext}%
20429
116255c9209b more on contexts;
wenzelm
parents: 20215
diff changeset
    31
A logical context represents the background that is taken for
116255c9209b more on contexts;
wenzelm
parents: 20215
diff changeset
    32
  granted when formulating statements and composing proofs.  It acts
116255c9209b more on contexts;
wenzelm
parents: 20215
diff changeset
    33
  as a medium to produce formal content, depending on earlier material
116255c9209b more on contexts;
wenzelm
parents: 20215
diff changeset
    34
  (declarations, results etc.).
18537
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    35
20429
116255c9209b more on contexts;
wenzelm
parents: 20215
diff changeset
    36
  In particular, derivations within the primitive Pure logic can be
116255c9209b more on contexts;
wenzelm
parents: 20215
diff changeset
    37
  described as a judgment \isa{{\isasymGamma}\ {\isasymturnstile}\isactrlsub {\isasymTheta}\ {\isasymphi}}, meaning that a
116255c9209b more on contexts;
wenzelm
parents: 20215
diff changeset
    38
  proposition \isa{{\isasymphi}} is derivable from hypotheses \isa{{\isasymGamma}}
116255c9209b more on contexts;
wenzelm
parents: 20215
diff changeset
    39
  within the theory \isa{{\isasymTheta}}.  There are logical reasons for
116255c9209b more on contexts;
wenzelm
parents: 20215
diff changeset
    40
  keeping \isa{{\isasymTheta}} and \isa{{\isasymGamma}} separate: theories support type
116255c9209b more on contexts;
wenzelm
parents: 20215
diff changeset
    41
  constructors and schematic polymorphism of constants and axioms,
116255c9209b more on contexts;
wenzelm
parents: 20215
diff changeset
    42
  while the inner calculus of \isa{{\isasymGamma}\ {\isasymturnstile}\ {\isasymphi}} is limited to Simple
116255c9209b more on contexts;
wenzelm
parents: 20215
diff changeset
    43
  Type Theory (with fixed type variables in the assumptions).
18537
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    44
20429
116255c9209b more on contexts;
wenzelm
parents: 20215
diff changeset
    45
  \medskip Contexts and derivations are linked by the following key
116255c9209b more on contexts;
wenzelm
parents: 20215
diff changeset
    46
  principles:
116255c9209b more on contexts;
wenzelm
parents: 20215
diff changeset
    47
116255c9209b more on contexts;
wenzelm
parents: 20215
diff changeset
    48
  \begin{itemize}
116255c9209b more on contexts;
wenzelm
parents: 20215
diff changeset
    49
116255c9209b more on contexts;
wenzelm
parents: 20215
diff changeset
    50
  \item Transfer: monotonicity of derivations admits results to be
116255c9209b more on contexts;
wenzelm
parents: 20215
diff changeset
    51
  transferred into a larger context, i.e.\ \isa{{\isasymGamma}\ {\isasymturnstile}\isactrlsub {\isasymTheta}\ {\isasymphi}}
116255c9209b more on contexts;
wenzelm
parents: 20215
diff changeset
    52
  implies \isa{{\isasymGamma}{\isacharprime}\ {\isasymturnstile}\isactrlsub {\isasymTheta}\isactrlsub {\isacharprime}\ {\isasymphi}} for contexts \isa{{\isasymTheta}{\isacharprime}\ {\isasymsupseteq}\ {\isasymTheta}} and \isa{{\isasymGamma}{\isacharprime}\ {\isasymsupseteq}\ {\isasymGamma}}.
116255c9209b more on contexts;
wenzelm
parents: 20215
diff changeset
    53
116255c9209b more on contexts;
wenzelm
parents: 20215
diff changeset
    54
  \item Export: discharge of hypotheses admits results to be exported
116255c9209b more on contexts;
wenzelm
parents: 20215
diff changeset
    55
  into a smaller context, i.e.\ \isa{{\isasymGamma}{\isacharprime}\ {\isasymturnstile}\isactrlsub {\isasymTheta}\ {\isasymphi}} implies
116255c9209b more on contexts;
wenzelm
parents: 20215
diff changeset
    56
  \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
116255c9209b more on contexts;
wenzelm
parents: 20215
diff changeset
    57
  \isa{{\isasymGamma}} part is affected.
18537
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    58
20429
116255c9209b more on contexts;
wenzelm
parents: 20215
diff changeset
    59
  \end{itemize}
18537
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    60
20429
116255c9209b more on contexts;
wenzelm
parents: 20215
diff changeset
    61
  \medskip Isabelle/Isar provides two different notions of abstract
116255c9209b more on contexts;
wenzelm
parents: 20215
diff changeset
    62
  containers called \emph{theory context} and \emph{proof context},
116255c9209b more on contexts;
wenzelm
parents: 20215
diff changeset
    63
  respectively.  These model the main characteristics of the primitive
116255c9209b more on contexts;
wenzelm
parents: 20215
diff changeset
    64
  \isa{{\isasymTheta}} and \isa{{\isasymGamma}} above, without subscribing to any
116255c9209b more on contexts;
wenzelm
parents: 20215
diff changeset
    65
  particular kind of content yet.  Instead, contexts merely impose a
116255c9209b more on contexts;
wenzelm
parents: 20215
diff changeset
    66
  certain policy of managing arbitrary \emph{context data}.  The
116255c9209b more on contexts;
wenzelm
parents: 20215
diff changeset
    67
  system provides strongly typed mechanisms to declare new kinds of
116255c9209b more on contexts;
wenzelm
parents: 20215
diff changeset
    68
  data at compile time.
18537
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    69
20429
116255c9209b more on contexts;
wenzelm
parents: 20215
diff changeset
    70
  Thus the internal bootstrap process of Isabelle/Pure eventually
116255c9209b more on contexts;
wenzelm
parents: 20215
diff changeset
    71
  reaches a stage where certain data slots provide the logical content
116255c9209b more on contexts;
wenzelm
parents: 20215
diff changeset
    72
  of \isa{{\isasymTheta}} and \isa{{\isasymGamma}} sketched above, but this does not
116255c9209b more on contexts;
wenzelm
parents: 20215
diff changeset
    73
  stop there!  Various additional data slots support all kinds of
116255c9209b more on contexts;
wenzelm
parents: 20215
diff changeset
    74
  mechanisms that are not necessarily part of the core logic.
18537
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    75
20429
116255c9209b more on contexts;
wenzelm
parents: 20215
diff changeset
    76
  For example, there would be data for canonical introduction and
116255c9209b more on contexts;
wenzelm
parents: 20215
diff changeset
    77
  elimination rules for arbitrary operators (depending on the
116255c9209b more on contexts;
wenzelm
parents: 20215
diff changeset
    78
  object-logic and application), which enables users to perform
116255c9209b more on contexts;
wenzelm
parents: 20215
diff changeset
    79
  standard proof steps implicitly (cf.\ the \isa{rule} method).
18537
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    80
20429
116255c9209b more on contexts;
wenzelm
parents: 20215
diff changeset
    81
  Isabelle is able to bring forth more and more concepts successively.
116255c9209b more on contexts;
wenzelm
parents: 20215
diff changeset
    82
  In particular, an object-logic like Isabelle/HOL continues the
116255c9209b more on contexts;
wenzelm
parents: 20215
diff changeset
    83
  Isabelle/Pure setup by adding specific components for automated
116255c9209b more on contexts;
wenzelm
parents: 20215
diff changeset
    84
  reasoning (classical reasoner, tableau prover, structured induction
116255c9209b more on contexts;
wenzelm
parents: 20215
diff changeset
    85
  etc.) and derived specification mechanisms (inductive predicates,
116255c9209b more on contexts;
wenzelm
parents: 20215
diff changeset
    86
  recursive functions etc.).  All of this is based on the generic data
116255c9209b more on contexts;
wenzelm
parents: 20215
diff changeset
    87
  management by theory and proof contexts.%
18537
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    88
\end{isamarkuptext}%
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    89
\isamarkuptrue%
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    90
%
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    91
\isamarkupsubsection{Theory context \label{sec:context-theory}%
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    92
}
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    93
\isamarkuptrue%
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    94
%
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    95
\begin{isamarkuptext}%
20447
5b75f1c4d7d6 more on contexts;
wenzelm
parents: 20438
diff changeset
    96
\glossary{Theory}{FIXME}
5b75f1c4d7d6 more on contexts;
wenzelm
parents: 20438
diff changeset
    97
5b75f1c4d7d6 more on contexts;
wenzelm
parents: 20438
diff changeset
    98
  Each theory is explicitly named and holds a unique identifier.
20429
116255c9209b more on contexts;
wenzelm
parents: 20215
diff changeset
    99
  There is a separate \emph{theory reference} for pointing backwards
116255c9209b more on contexts;
wenzelm
parents: 20215
diff changeset
   100
  to the enclosing theory context of derived entities.  Theories are
116255c9209b more on contexts;
wenzelm
parents: 20215
diff changeset
   101
  related by a (nominal) sub-theory relation, which corresponds to the
116255c9209b more on contexts;
wenzelm
parents: 20215
diff changeset
   102
  canonical dependency graph: each theory is derived from a certain
116255c9209b more on contexts;
wenzelm
parents: 20215
diff changeset
   103
  sub-graph of ancestor theories.  The \isa{merge} of two theories
116255c9209b more on contexts;
wenzelm
parents: 20215
diff changeset
   104
  refers to the least upper bound, which actually degenerates into
116255c9209b more on contexts;
wenzelm
parents: 20215
diff changeset
   105
  absorption of one theory into the other, due to the nominal
116255c9209b more on contexts;
wenzelm
parents: 20215
diff changeset
   106
  sub-theory relation this.
18537
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   107
20429
116255c9209b more on contexts;
wenzelm
parents: 20215
diff changeset
   108
  The \isa{begin} operation starts a new theory by importing
116255c9209b more on contexts;
wenzelm
parents: 20215
diff changeset
   109
  several parent theories and entering a special \isa{draft} mode,
116255c9209b more on contexts;
wenzelm
parents: 20215
diff changeset
   110
  which is sustained until the final \isa{end} operation.  A draft
116255c9209b more on contexts;
wenzelm
parents: 20215
diff changeset
   111
  mode theory acts like a linear type, where updates invalidate
116255c9209b more on contexts;
wenzelm
parents: 20215
diff changeset
   112
  earlier drafts, but theory reference values will be propagated
116255c9209b more on contexts;
wenzelm
parents: 20215
diff changeset
   113
  automatically.  Thus derived entities that ``belong'' to a draft
116255c9209b more on contexts;
wenzelm
parents: 20215
diff changeset
   114
  might be transferred spontaneously to a larger context.  An
20447
5b75f1c4d7d6 more on contexts;
wenzelm
parents: 20438
diff changeset
   115
  invalidated draft is called ``stale''.
20429
116255c9209b more on contexts;
wenzelm
parents: 20215
diff changeset
   116
20447
5b75f1c4d7d6 more on contexts;
wenzelm
parents: 20438
diff changeset
   117
  The \isa{checkpoint} operation produces an intermediate stepping
5b75f1c4d7d6 more on contexts;
wenzelm
parents: 20438
diff changeset
   118
  stone that will survive the next update unscathed: both the original
5b75f1c4d7d6 more on contexts;
wenzelm
parents: 20438
diff changeset
   119
  and the changed theory remain valid and are related by the
5b75f1c4d7d6 more on contexts;
wenzelm
parents: 20438
diff changeset
   120
  sub-theory relation.  Checkpointing essentially recovers purely
5b75f1c4d7d6 more on contexts;
wenzelm
parents: 20438
diff changeset
   121
  functional theory values, at the expense of some extra internal
5b75f1c4d7d6 more on contexts;
wenzelm
parents: 20438
diff changeset
   122
  bookeeping.
5b75f1c4d7d6 more on contexts;
wenzelm
parents: 20438
diff changeset
   123
5b75f1c4d7d6 more on contexts;
wenzelm
parents: 20438
diff changeset
   124
  The \isa{copy} operation produces an auxiliary version that has
5b75f1c4d7d6 more on contexts;
wenzelm
parents: 20438
diff changeset
   125
  the same data content, but is unrelated to the original: updates of
5b75f1c4d7d6 more on contexts;
wenzelm
parents: 20438
diff changeset
   126
  the copy do not affect the original, neither does the sub-theory
5b75f1c4d7d6 more on contexts;
wenzelm
parents: 20438
diff changeset
   127
  relation hold.
20429
116255c9209b more on contexts;
wenzelm
parents: 20215
diff changeset
   128
20447
5b75f1c4d7d6 more on contexts;
wenzelm
parents: 20438
diff changeset
   129
  \medskip The example in \figref{fig:ex-theory} below shows a theory
5b75f1c4d7d6 more on contexts;
wenzelm
parents: 20438
diff changeset
   130
  graph derived from \isa{Pure}. Theory \isa{Length} imports
5b75f1c4d7d6 more on contexts;
wenzelm
parents: 20438
diff changeset
   131
  \isa{Nat} and \isa{List}.  The theory body consists of a
5b75f1c4d7d6 more on contexts;
wenzelm
parents: 20438
diff changeset
   132
  sequence of updates, working mostly on drafts.  Intermediate
5b75f1c4d7d6 more on contexts;
wenzelm
parents: 20438
diff changeset
   133
  checkpoints may occur as well, due to the history mechanism provided
5b75f1c4d7d6 more on contexts;
wenzelm
parents: 20438
diff changeset
   134
  by the Isar toplevel, cf.\ \secref{sec:isar-toplevel}.
5b75f1c4d7d6 more on contexts;
wenzelm
parents: 20438
diff changeset
   135
5b75f1c4d7d6 more on contexts;
wenzelm
parents: 20438
diff changeset
   136
  \begin{figure}[htb]
5b75f1c4d7d6 more on contexts;
wenzelm
parents: 20438
diff changeset
   137
  \begin{center}
20429
116255c9209b more on contexts;
wenzelm
parents: 20215
diff changeset
   138
  \begin{tabular}{rcccl}
20447
5b75f1c4d7d6 more on contexts;
wenzelm
parents: 20438
diff changeset
   139
        &            & \isa{Pure} \\
5b75f1c4d7d6 more on contexts;
wenzelm
parents: 20438
diff changeset
   140
        &            & \isa{{\isasymdown}} \\
5b75f1c4d7d6 more on contexts;
wenzelm
parents: 20438
diff changeset
   141
        &            & \isa{FOL} \\
18537
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   142
        & $\swarrow$ &              & $\searrow$ & \\
20447
5b75f1c4d7d6 more on contexts;
wenzelm
parents: 20438
diff changeset
   143
  $Nat$ &            &              &            & \isa{List} \\
18537
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   144
        & $\searrow$ &              & $\swarrow$ \\
20447
5b75f1c4d7d6 more on contexts;
wenzelm
parents: 20438
diff changeset
   145
        &            & \isa{Length} \\
18537
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   146
        &            & \multicolumn{3}{l}{~~$\isarkeyword{imports}$} \\
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   147
        &            & \multicolumn{3}{l}{~~$\isarkeyword{begin}$} \\
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   148
        &            & $\vdots$~~ \\
20447
5b75f1c4d7d6 more on contexts;
wenzelm
parents: 20438
diff changeset
   149
        &            & \isa{{\isasymbullet}}~~ \\
5b75f1c4d7d6 more on contexts;
wenzelm
parents: 20438
diff changeset
   150
        &            & $\vdots$~~ \\
5b75f1c4d7d6 more on contexts;
wenzelm
parents: 20438
diff changeset
   151
        &            & \isa{{\isasymbullet}}~~ \\
5b75f1c4d7d6 more on contexts;
wenzelm
parents: 20438
diff changeset
   152
        &            & $\vdots$~~ \\
18537
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   153
        &            & \multicolumn{3}{l}{~~$\isarkeyword{end}$} \\
20429
116255c9209b more on contexts;
wenzelm
parents: 20215
diff changeset
   154
  \end{tabular}
20447
5b75f1c4d7d6 more on contexts;
wenzelm
parents: 20438
diff changeset
   155
  \caption{Theory definition depending on ancestors}\label{fig:ex-theory}
5b75f1c4d7d6 more on contexts;
wenzelm
parents: 20438
diff changeset
   156
  \end{center}
5b75f1c4d7d6 more on contexts;
wenzelm
parents: 20438
diff changeset
   157
  \end{figure}%
18537
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   158
\end{isamarkuptext}%
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   159
\isamarkuptrue%
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   160
%
20430
wenzelm
parents: 20429
diff changeset
   161
\isadelimmlref
wenzelm
parents: 20429
diff changeset
   162
%
wenzelm
parents: 20429
diff changeset
   163
\endisadelimmlref
wenzelm
parents: 20429
diff changeset
   164
%
wenzelm
parents: 20429
diff changeset
   165
\isatagmlref
wenzelm
parents: 20429
diff changeset
   166
%
wenzelm
parents: 20429
diff changeset
   167
\begin{isamarkuptext}%
20447
5b75f1c4d7d6 more on contexts;
wenzelm
parents: 20438
diff changeset
   168
\begin{mldecls}
5b75f1c4d7d6 more on contexts;
wenzelm
parents: 20438
diff changeset
   169
  \indexmltype{theory}\verb|type theory| \\
5b75f1c4d7d6 more on contexts;
wenzelm
parents: 20438
diff changeset
   170
  \indexml{Theory.subthy}\verb|Theory.subthy: theory * theory -> bool| \\
5b75f1c4d7d6 more on contexts;
wenzelm
parents: 20438
diff changeset
   171
  \indexml{Theory.merge}\verb|Theory.merge: theory * theory -> theory| \\
5b75f1c4d7d6 more on contexts;
wenzelm
parents: 20438
diff changeset
   172
  \indexml{Theory.checkpoint}\verb|Theory.checkpoint: theory -> theory| \\
5b75f1c4d7d6 more on contexts;
wenzelm
parents: 20438
diff changeset
   173
  \indexml{Theory.copy}\verb|Theory.copy: theory -> theory| \\[1ex]
5b75f1c4d7d6 more on contexts;
wenzelm
parents: 20438
diff changeset
   174
  \indexmltype{theory-ref}\verb|type theory_ref| \\
5b75f1c4d7d6 more on contexts;
wenzelm
parents: 20438
diff changeset
   175
  \indexml{Theory.self-ref}\verb|Theory.self_ref: theory -> theory_ref| \\
5b75f1c4d7d6 more on contexts;
wenzelm
parents: 20438
diff changeset
   176
  \indexml{Theory.deref}\verb|Theory.deref: theory_ref -> theory| \\
5b75f1c4d7d6 more on contexts;
wenzelm
parents: 20438
diff changeset
   177
  \end{mldecls}
5b75f1c4d7d6 more on contexts;
wenzelm
parents: 20438
diff changeset
   178
5b75f1c4d7d6 more on contexts;
wenzelm
parents: 20438
diff changeset
   179
  \begin{description}
5b75f1c4d7d6 more on contexts;
wenzelm
parents: 20438
diff changeset
   180
5b75f1c4d7d6 more on contexts;
wenzelm
parents: 20438
diff changeset
   181
  \item \verb|theory| represents theory contexts.  This is a
5b75f1c4d7d6 more on contexts;
wenzelm
parents: 20438
diff changeset
   182
  linear type!  Most operations destroy the old version, which then
5b75f1c4d7d6 more on contexts;
wenzelm
parents: 20438
diff changeset
   183
  becomes ``stale''.
5b75f1c4d7d6 more on contexts;
wenzelm
parents: 20438
diff changeset
   184
5b75f1c4d7d6 more on contexts;
wenzelm
parents: 20438
diff changeset
   185
  \item \verb|Theory.subthy|~\isa{{\isacharparenleft}thy\isactrlsub {\isadigit{1}}{\isacharcomma}\ thy\isactrlsub {\isadigit{2}}{\isacharparenright}}
5b75f1c4d7d6 more on contexts;
wenzelm
parents: 20438
diff changeset
   186
  compares theories according to the inherent graph structure of the
5b75f1c4d7d6 more on contexts;
wenzelm
parents: 20438
diff changeset
   187
  construction.  This sub-theory relation is a nominal approximation
5b75f1c4d7d6 more on contexts;
wenzelm
parents: 20438
diff changeset
   188
  of inclusion (\isa{{\isasymsubseteq}}) of the corresponding content.
5b75f1c4d7d6 more on contexts;
wenzelm
parents: 20438
diff changeset
   189
5b75f1c4d7d6 more on contexts;
wenzelm
parents: 20438
diff changeset
   190
  \item \verb|Theory.merge|~\isa{{\isacharparenleft}thy\isactrlsub {\isadigit{1}}{\isacharcomma}\ thy\isactrlsub {\isadigit{2}}{\isacharparenright}}
5b75f1c4d7d6 more on contexts;
wenzelm
parents: 20438
diff changeset
   191
  absorbs one theory into the other.  This fails for unrelated
5b75f1c4d7d6 more on contexts;
wenzelm
parents: 20438
diff changeset
   192
  theories!
5b75f1c4d7d6 more on contexts;
wenzelm
parents: 20438
diff changeset
   193
5b75f1c4d7d6 more on contexts;
wenzelm
parents: 20438
diff changeset
   194
  \item \verb|Theory.checkpoint|~\isa{thy} produces a safe
5b75f1c4d7d6 more on contexts;
wenzelm
parents: 20438
diff changeset
   195
  stepping stone in the linear development of \isa{thy}.  The next
5b75f1c4d7d6 more on contexts;
wenzelm
parents: 20438
diff changeset
   196
  update will result in two related, valid theories.
5b75f1c4d7d6 more on contexts;
wenzelm
parents: 20438
diff changeset
   197
5b75f1c4d7d6 more on contexts;
wenzelm
parents: 20438
diff changeset
   198
  \item \verb|Theory.copy|~\isa{thy} produces a variant of \isa{thy} that holds a copy of the same data.  The copy is not related
5b75f1c4d7d6 more on contexts;
wenzelm
parents: 20438
diff changeset
   199
  to the original, which is not touched at all.
5b75f1c4d7d6 more on contexts;
wenzelm
parents: 20438
diff changeset
   200
5b75f1c4d7d6 more on contexts;
wenzelm
parents: 20438
diff changeset
   201
  \item \verb|theory_ref| represents a sliding reference to a
5b75f1c4d7d6 more on contexts;
wenzelm
parents: 20438
diff changeset
   202
  valid theory --- updates on the original are propagated
5b75f1c4d7d6 more on contexts;
wenzelm
parents: 20438
diff changeset
   203
  automatically.
5b75f1c4d7d6 more on contexts;
wenzelm
parents: 20438
diff changeset
   204
5b75f1c4d7d6 more on contexts;
wenzelm
parents: 20438
diff changeset
   205
  \item \verb|Theory.self_ref| and \verb|Theory.deref| convert
5b75f1c4d7d6 more on contexts;
wenzelm
parents: 20438
diff changeset
   206
  between \verb|theory| and \verb|theory_ref|.  As the
5b75f1c4d7d6 more on contexts;
wenzelm
parents: 20438
diff changeset
   207
  referenced theory evolves monotonically over time, later invocations
5b75f1c4d7d6 more on contexts;
wenzelm
parents: 20438
diff changeset
   208
  of \verb|Theory.deref| may refer to larger contexts.
5b75f1c4d7d6 more on contexts;
wenzelm
parents: 20438
diff changeset
   209
5b75f1c4d7d6 more on contexts;
wenzelm
parents: 20438
diff changeset
   210
  \end{description}%
20430
wenzelm
parents: 20429
diff changeset
   211
\end{isamarkuptext}%
wenzelm
parents: 20429
diff changeset
   212
\isamarkuptrue%
wenzelm
parents: 20429
diff changeset
   213
%
wenzelm
parents: 20429
diff changeset
   214
\endisatagmlref
wenzelm
parents: 20429
diff changeset
   215
{\isafoldmlref}%
wenzelm
parents: 20429
diff changeset
   216
%
wenzelm
parents: 20429
diff changeset
   217
\isadelimmlref
wenzelm
parents: 20429
diff changeset
   218
%
wenzelm
parents: 20429
diff changeset
   219
\endisadelimmlref
wenzelm
parents: 20429
diff changeset
   220
%
18537
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   221
\isamarkupsubsection{Proof context \label{sec:context-proof}%
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   222
}
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   223
\isamarkuptrue%
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   224
%
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   225
\begin{isamarkuptext}%
20447
5b75f1c4d7d6 more on contexts;
wenzelm
parents: 20438
diff changeset
   226
\glossary{Proof context}{The static context of a structured proof,
5b75f1c4d7d6 more on contexts;
wenzelm
parents: 20438
diff changeset
   227
  acts like a local ``theory'' of the current portion of Isar proof
5b75f1c4d7d6 more on contexts;
wenzelm
parents: 20438
diff changeset
   228
  text, generalizes the idea of local hypotheses \isa{{\isasymGamma}} in
5b75f1c4d7d6 more on contexts;
wenzelm
parents: 20438
diff changeset
   229
  judgments \isa{{\isasymGamma}\ {\isasymturnstile}\ {\isasymphi}} of natural deduction calculi.  There is a
5b75f1c4d7d6 more on contexts;
wenzelm
parents: 20438
diff changeset
   230
  generic notion of introducing and discharging hypotheses.
5b75f1c4d7d6 more on contexts;
wenzelm
parents: 20438
diff changeset
   231
  Arbritrary auxiliary context data may be adjoined.}
20429
116255c9209b more on contexts;
wenzelm
parents: 20215
diff changeset
   232
20447
5b75f1c4d7d6 more on contexts;
wenzelm
parents: 20438
diff changeset
   233
  A proof context is a container for pure data with a back-reference
5b75f1c4d7d6 more on contexts;
wenzelm
parents: 20438
diff changeset
   234
  to the theory it belongs to.  Modifications to draft theories are
5b75f1c4d7d6 more on contexts;
wenzelm
parents: 20438
diff changeset
   235
  propagated automatically as usual, but there is also an explicit
5b75f1c4d7d6 more on contexts;
wenzelm
parents: 20438
diff changeset
   236
  \isa{transfer} operation to resynchronize with more substantial
5b75f1c4d7d6 more on contexts;
wenzelm
parents: 20438
diff changeset
   237
  updates to the underlying theory.  The actual context data does not
5b75f1c4d7d6 more on contexts;
wenzelm
parents: 20438
diff changeset
   238
  require any special bookkeeping, thanks to the lack of destructive
5b75f1c4d7d6 more on contexts;
wenzelm
parents: 20438
diff changeset
   239
  features.
20429
116255c9209b more on contexts;
wenzelm
parents: 20215
diff changeset
   240
20447
5b75f1c4d7d6 more on contexts;
wenzelm
parents: 20438
diff changeset
   241
  Entities derived in a proof context need to record inherent logical
5b75f1c4d7d6 more on contexts;
wenzelm
parents: 20438
diff changeset
   242
  requirements explicitly, since there is no separate context
5b75f1c4d7d6 more on contexts;
wenzelm
parents: 20438
diff changeset
   243
  identification as for theories.  For example, hypotheses used in
5b75f1c4d7d6 more on contexts;
wenzelm
parents: 20438
diff changeset
   244
  primitive derivations (cf.\ \secref{sec:thm}) are recorded
5b75f1c4d7d6 more on contexts;
wenzelm
parents: 20438
diff changeset
   245
  separately within the sequent \isa{{\isasymGamma}\ {\isasymturnstile}\ {\isasymphi}}, just to make double
5b75f1c4d7d6 more on contexts;
wenzelm
parents: 20438
diff changeset
   246
  sure.  Results could still leak into an alien proof context do to
5b75f1c4d7d6 more on contexts;
wenzelm
parents: 20438
diff changeset
   247
  programming errors, but Isabelle/Isar includes some extra validity
5b75f1c4d7d6 more on contexts;
wenzelm
parents: 20438
diff changeset
   248
  checks in critical positions, notably at the end of sub-proof.
20429
116255c9209b more on contexts;
wenzelm
parents: 20215
diff changeset
   249
20447
5b75f1c4d7d6 more on contexts;
wenzelm
parents: 20438
diff changeset
   250
  Proof contexts may be produced in arbitrary ways, although the
5b75f1c4d7d6 more on contexts;
wenzelm
parents: 20438
diff changeset
   251
  common discipline is to follow block structure as a mental model: a
5b75f1c4d7d6 more on contexts;
wenzelm
parents: 20438
diff changeset
   252
  given context is extended consecutively, and results are exported
5b75f1c4d7d6 more on contexts;
wenzelm
parents: 20438
diff changeset
   253
  back into the original context.  Note that the Isar proof states
5b75f1c4d7d6 more on contexts;
wenzelm
parents: 20438
diff changeset
   254
  model block-structured reasoning explicitly, using a stack of proof
5b75f1c4d7d6 more on contexts;
wenzelm
parents: 20438
diff changeset
   255
  contexts, cf.\ \secref{isar-proof-state}.%
18537
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   256
\end{isamarkuptext}%
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   257
\isamarkuptrue%
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   258
%
20430
wenzelm
parents: 20429
diff changeset
   259
\isadelimmlref
wenzelm
parents: 20429
diff changeset
   260
%
wenzelm
parents: 20429
diff changeset
   261
\endisadelimmlref
wenzelm
parents: 20429
diff changeset
   262
%
wenzelm
parents: 20429
diff changeset
   263
\isatagmlref
wenzelm
parents: 20429
diff changeset
   264
%
wenzelm
parents: 20429
diff changeset
   265
\begin{isamarkuptext}%
wenzelm
parents: 20429
diff changeset
   266
FIXME%
wenzelm
parents: 20429
diff changeset
   267
\end{isamarkuptext}%
wenzelm
parents: 20429
diff changeset
   268
\isamarkuptrue%
wenzelm
parents: 20429
diff changeset
   269
%
wenzelm
parents: 20429
diff changeset
   270
\endisatagmlref
wenzelm
parents: 20429
diff changeset
   271
{\isafoldmlref}%
wenzelm
parents: 20429
diff changeset
   272
%
wenzelm
parents: 20429
diff changeset
   273
\isadelimmlref
wenzelm
parents: 20429
diff changeset
   274
%
wenzelm
parents: 20429
diff changeset
   275
\endisadelimmlref
wenzelm
parents: 20429
diff changeset
   276
%
20429
116255c9209b more on contexts;
wenzelm
parents: 20215
diff changeset
   277
\isamarkupsubsection{Generic contexts%
116255c9209b more on contexts;
wenzelm
parents: 20215
diff changeset
   278
}
116255c9209b more on contexts;
wenzelm
parents: 20215
diff changeset
   279
\isamarkuptrue%
116255c9209b more on contexts;
wenzelm
parents: 20215
diff changeset
   280
%
20430
wenzelm
parents: 20429
diff changeset
   281
\begin{isamarkuptext}%
wenzelm
parents: 20429
diff changeset
   282
FIXME%
wenzelm
parents: 20429
diff changeset
   283
\end{isamarkuptext}%
wenzelm
parents: 20429
diff changeset
   284
\isamarkuptrue%
wenzelm
parents: 20429
diff changeset
   285
%
wenzelm
parents: 20429
diff changeset
   286
\isadelimmlref
wenzelm
parents: 20429
diff changeset
   287
%
wenzelm
parents: 20429
diff changeset
   288
\endisadelimmlref
wenzelm
parents: 20429
diff changeset
   289
%
wenzelm
parents: 20429
diff changeset
   290
\isatagmlref
wenzelm
parents: 20429
diff changeset
   291
%
wenzelm
parents: 20429
diff changeset
   292
\begin{isamarkuptext}%
wenzelm
parents: 20429
diff changeset
   293
FIXME%
wenzelm
parents: 20429
diff changeset
   294
\end{isamarkuptext}%
wenzelm
parents: 20429
diff changeset
   295
\isamarkuptrue%
wenzelm
parents: 20429
diff changeset
   296
%
wenzelm
parents: 20429
diff changeset
   297
\endisatagmlref
wenzelm
parents: 20429
diff changeset
   298
{\isafoldmlref}%
wenzelm
parents: 20429
diff changeset
   299
%
wenzelm
parents: 20429
diff changeset
   300
\isadelimmlref
wenzelm
parents: 20429
diff changeset
   301
%
wenzelm
parents: 20429
diff changeset
   302
\endisadelimmlref
wenzelm
parents: 20429
diff changeset
   303
%
20447
5b75f1c4d7d6 more on contexts;
wenzelm
parents: 20438
diff changeset
   304
\isamarkupsubsection{Context data%
5b75f1c4d7d6 more on contexts;
wenzelm
parents: 20438
diff changeset
   305
}
5b75f1c4d7d6 more on contexts;
wenzelm
parents: 20438
diff changeset
   306
\isamarkuptrue%
5b75f1c4d7d6 more on contexts;
wenzelm
parents: 20438
diff changeset
   307
%
5b75f1c4d7d6 more on contexts;
wenzelm
parents: 20438
diff changeset
   308
\begin{isamarkuptext}%
5b75f1c4d7d6 more on contexts;
wenzelm
parents: 20438
diff changeset
   309
%
5b75f1c4d7d6 more on contexts;
wenzelm
parents: 20438
diff changeset
   310
\end{isamarkuptext}%
5b75f1c4d7d6 more on contexts;
wenzelm
parents: 20438
diff changeset
   311
\isamarkuptrue%
5b75f1c4d7d6 more on contexts;
wenzelm
parents: 20438
diff changeset
   312
%
20438
9060c73a4578 updated;
wenzelm
parents: 20430
diff changeset
   313
\isamarkupsection{Named entities%
9060c73a4578 updated;
wenzelm
parents: 20430
diff changeset
   314
}
9060c73a4578 updated;
wenzelm
parents: 20430
diff changeset
   315
\isamarkuptrue%
9060c73a4578 updated;
wenzelm
parents: 20430
diff changeset
   316
%
9060c73a4578 updated;
wenzelm
parents: 20430
diff changeset
   317
\begin{isamarkuptext}%
9060c73a4578 updated;
wenzelm
parents: 20430
diff changeset
   318
Named entities of different kinds (logical constant, type,
9060c73a4578 updated;
wenzelm
parents: 20430
diff changeset
   319
type class, theorem, method etc.) live in separate name spaces.  It is
9060c73a4578 updated;
wenzelm
parents: 20430
diff changeset
   320
usually clear from the occurrence of a name which kind of entity it
9060c73a4578 updated;
wenzelm
parents: 20430
diff changeset
   321
refers to.  For example, proof method \isa{foo} vs.\ theorem
9060c73a4578 updated;
wenzelm
parents: 20430
diff changeset
   322
\isa{foo} vs.\ logical constant \isa{foo} are easily
9060c73a4578 updated;
wenzelm
parents: 20430
diff changeset
   323
distinguished by means of the syntactic context.  A notable exception
9060c73a4578 updated;
wenzelm
parents: 20430
diff changeset
   324
are logical identifiers within a term (\secref{sec:terms}): constants,
9060c73a4578 updated;
wenzelm
parents: 20430
diff changeset
   325
fixed variables, and bound variables all share the same identifier
9060c73a4578 updated;
wenzelm
parents: 20430
diff changeset
   326
syntax, but are distinguished by their scope.
9060c73a4578 updated;
wenzelm
parents: 20430
diff changeset
   327
9060c73a4578 updated;
wenzelm
parents: 20430
diff changeset
   328
Each name space is organized as a collection of \emph{qualified
9060c73a4578 updated;
wenzelm
parents: 20430
diff changeset
   329
names}, which consist of a sequence of basic name components separated
9060c73a4578 updated;
wenzelm
parents: 20430
diff changeset
   330
by dots: \isa{Bar{\isachardot}bar{\isachardot}foo}, \isa{Bar{\isachardot}foo}, and \isa{foo}
9060c73a4578 updated;
wenzelm
parents: 20430
diff changeset
   331
are examples for valid qualified names.  Name components are
9060c73a4578 updated;
wenzelm
parents: 20430
diff changeset
   332
subdivided into \emph{symbols}, which constitute the smallest textual
9060c73a4578 updated;
wenzelm
parents: 20430
diff changeset
   333
unit in Isabelle --- raw characters are normally not encountered
9060c73a4578 updated;
wenzelm
parents: 20430
diff changeset
   334
directly.%
9060c73a4578 updated;
wenzelm
parents: 20430
diff changeset
   335
\end{isamarkuptext}%
9060c73a4578 updated;
wenzelm
parents: 20430
diff changeset
   336
\isamarkuptrue%
9060c73a4578 updated;
wenzelm
parents: 20430
diff changeset
   337
%
9060c73a4578 updated;
wenzelm
parents: 20430
diff changeset
   338
\isamarkupsubsection{Strings of symbols%
9060c73a4578 updated;
wenzelm
parents: 20430
diff changeset
   339
}
9060c73a4578 updated;
wenzelm
parents: 20430
diff changeset
   340
\isamarkuptrue%
9060c73a4578 updated;
wenzelm
parents: 20430
diff changeset
   341
%
9060c73a4578 updated;
wenzelm
parents: 20430
diff changeset
   342
\begin{isamarkuptext}%
9060c73a4578 updated;
wenzelm
parents: 20430
diff changeset
   343
Isabelle strings consist of a sequence of
9060c73a4578 updated;
wenzelm
parents: 20430
diff changeset
   344
symbols\glossary{Symbol}{The smalles unit of text in Isabelle,
9060c73a4578 updated;
wenzelm
parents: 20430
diff changeset
   345
subsumes plain ASCII characters as well as an infinite collection of
9060c73a4578 updated;
wenzelm
parents: 20430
diff changeset
   346
named symbols (for greek, math etc.).}, which are either packed as an
9060c73a4578 updated;
wenzelm
parents: 20430
diff changeset
   347
actual \isa{string}, or represented as a list.  Each symbol is in
9060c73a4578 updated;
wenzelm
parents: 20430
diff changeset
   348
itself a small string of the following form:
9060c73a4578 updated;
wenzelm
parents: 20430
diff changeset
   349
9060c73a4578 updated;
wenzelm
parents: 20430
diff changeset
   350
\begin{enumerate}
9060c73a4578 updated;
wenzelm
parents: 20430
diff changeset
   351
9060c73a4578 updated;
wenzelm
parents: 20430
diff changeset
   352
\item either a singleton ASCII character ``\isa{c}'' (with
9060c73a4578 updated;
wenzelm
parents: 20430
diff changeset
   353
character code 0--127), for example ``\verb,a,'',
9060c73a4578 updated;
wenzelm
parents: 20430
diff changeset
   354
9060c73a4578 updated;
wenzelm
parents: 20430
diff changeset
   355
\item or a regular symbol ``\verb,\,\verb,<,\isa{ident}\verb,>,'',
9060c73a4578 updated;
wenzelm
parents: 20430
diff changeset
   356
for example ``\verb,\,\verb,<alpha>,'',
9060c73a4578 updated;
wenzelm
parents: 20430
diff changeset
   357
9060c73a4578 updated;
wenzelm
parents: 20430
diff changeset
   358
\item or a control symbol ``\verb,\,\verb,<^,\isa{ident}\verb,>,'', for example ``\verb,\,\verb,<^bold>,'',
9060c73a4578 updated;
wenzelm
parents: 20430
diff changeset
   359
9060c73a4578 updated;
wenzelm
parents: 20430
diff changeset
   360
\item or a raw control symbol ``\verb,\,\verb,<^raw:,\isa{{\isasymdots}}\verb,>,'' where ``\isa{{\isasymdots}}'' refers to any
9060c73a4578 updated;
wenzelm
parents: 20430
diff changeset
   361
printable ASCII character (excluding ``\verb,.,'' and ``\verb,>,'') or
9060c73a4578 updated;
wenzelm
parents: 20430
diff changeset
   362
non-ASCII character, for example ``\verb,\,\verb,<^raw:$\sum_{i = 1}^n$>,'',
9060c73a4578 updated;
wenzelm
parents: 20430
diff changeset
   363
9060c73a4578 updated;
wenzelm
parents: 20430
diff changeset
   364
\item or a numbered raw control symbol ``\verb,\,\verb,<^raw,\isa{nnn}\verb,>, where \isa{nnn} are digits, for example
9060c73a4578 updated;
wenzelm
parents: 20430
diff changeset
   365
``\verb,\,\verb,<^raw42>,''.
9060c73a4578 updated;
wenzelm
parents: 20430
diff changeset
   366
9060c73a4578 updated;
wenzelm
parents: 20430
diff changeset
   367
\end{enumerate}
9060c73a4578 updated;
wenzelm
parents: 20430
diff changeset
   368
9060c73a4578 updated;
wenzelm
parents: 20430
diff changeset
   369
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
9060c73a4578 updated;
wenzelm
parents: 20430
diff changeset
   370
control symbols available, but a certain collection of standard
9060c73a4578 updated;
wenzelm
parents: 20430
diff changeset
   371
symbols is treated specifically.  For example,
9060c73a4578 updated;
wenzelm
parents: 20430
diff changeset
   372
``\verb,\,\verb,<alpha>,'' is classified as a (non-ASCII) letter,
9060c73a4578 updated;
wenzelm
parents: 20430
diff changeset
   373
which means it may occur within regular Isabelle identifier syntax.
9060c73a4578 updated;
wenzelm
parents: 20430
diff changeset
   374
9060c73a4578 updated;
wenzelm
parents: 20430
diff changeset
   375
Output of symbols depends on the print mode (\secref{sec:print-mode}).
9060c73a4578 updated;
wenzelm
parents: 20430
diff changeset
   376
For example, the standard {\LaTeX} setup of the Isabelle document
9060c73a4578 updated;
wenzelm
parents: 20430
diff changeset
   377
preparation system would present ``\verb,\,\verb,<alpha>,'' as \isa{{\isasymalpha}}, and ``\verb,\,\verb,<^bold>,\verb,\,\verb,<alpha>,'' as \isa{\isactrlbold {\isasymalpha}}.
9060c73a4578 updated;
wenzelm
parents: 20430
diff changeset
   378
9060c73a4578 updated;
wenzelm
parents: 20430
diff changeset
   379
\medskip It is important to note that the character set underlying
9060c73a4578 updated;
wenzelm
parents: 20430
diff changeset
   380
Isabelle symbols is plain 7-bit ASCII.  Since 8-bit characters are
9060c73a4578 updated;
wenzelm
parents: 20430
diff changeset
   381
passed through transparently, Isabelle may easily process actual
9060c73a4578 updated;
wenzelm
parents: 20430
diff changeset
   382
Unicode/UCS data (using the well-known UTF-8 encoding, for example).
9060c73a4578 updated;
wenzelm
parents: 20430
diff changeset
   383
Unicode provides its own collection of mathematical symbols, but there
9060c73a4578 updated;
wenzelm
parents: 20430
diff changeset
   384
is presently no link to Isabelle's named ones; both kinds of symbols
9060c73a4578 updated;
wenzelm
parents: 20430
diff changeset
   385
coexist independently.%
9060c73a4578 updated;
wenzelm
parents: 20430
diff changeset
   386
\end{isamarkuptext}%
9060c73a4578 updated;
wenzelm
parents: 20430
diff changeset
   387
\isamarkuptrue%
9060c73a4578 updated;
wenzelm
parents: 20430
diff changeset
   388
%
9060c73a4578 updated;
wenzelm
parents: 20430
diff changeset
   389
\isadelimmlref
9060c73a4578 updated;
wenzelm
parents: 20430
diff changeset
   390
%
9060c73a4578 updated;
wenzelm
parents: 20430
diff changeset
   391
\endisadelimmlref
9060c73a4578 updated;
wenzelm
parents: 20430
diff changeset
   392
%
9060c73a4578 updated;
wenzelm
parents: 20430
diff changeset
   393
\isatagmlref
9060c73a4578 updated;
wenzelm
parents: 20430
diff changeset
   394
%
9060c73a4578 updated;
wenzelm
parents: 20430
diff changeset
   395
\begin{isamarkuptext}%
9060c73a4578 updated;
wenzelm
parents: 20430
diff changeset
   396
\begin{mldecls}
9060c73a4578 updated;
wenzelm
parents: 20430
diff changeset
   397
  \indexmltype{Symbol.symbol}\verb|type Symbol.symbol| \\
9060c73a4578 updated;
wenzelm
parents: 20430
diff changeset
   398
  \indexml{Symbol.explode}\verb|Symbol.explode: string -> Symbol.symbol list| \\
9060c73a4578 updated;
wenzelm
parents: 20430
diff changeset
   399
  \indexml{Symbol.is-letter}\verb|Symbol.is_letter: Symbol.symbol -> bool| \\
9060c73a4578 updated;
wenzelm
parents: 20430
diff changeset
   400
  \indexml{Symbol.is-digit}\verb|Symbol.is_digit: Symbol.symbol -> bool| \\
9060c73a4578 updated;
wenzelm
parents: 20430
diff changeset
   401
  \indexml{Symbol.is-quasi}\verb|Symbol.is_quasi: Symbol.symbol -> bool| \\
9060c73a4578 updated;
wenzelm
parents: 20430
diff changeset
   402
  \indexml{Symbol.is-blank}\verb|Symbol.is_blank: Symbol.symbol -> bool| \\
9060c73a4578 updated;
wenzelm
parents: 20430
diff changeset
   403
  \indexmltype{Symbol.sym}\verb|type Symbol.sym| \\
9060c73a4578 updated;
wenzelm
parents: 20430
diff changeset
   404
  \indexml{Symbol.decode}\verb|Symbol.decode: Symbol.symbol -> Symbol.sym| \\
9060c73a4578 updated;
wenzelm
parents: 20430
diff changeset
   405
  \end{mldecls}
9060c73a4578 updated;
wenzelm
parents: 20430
diff changeset
   406
9060c73a4578 updated;
wenzelm
parents: 20430
diff changeset
   407
  \begin{description}
9060c73a4578 updated;
wenzelm
parents: 20430
diff changeset
   408
9060c73a4578 updated;
wenzelm
parents: 20430
diff changeset
   409
  \item \verb|Symbol.symbol| represents Isabelle symbols; this type
9060c73a4578 updated;
wenzelm
parents: 20430
diff changeset
   410
  is merely an alias for \verb|string|, but emphasizes the
9060c73a4578 updated;
wenzelm
parents: 20430
diff changeset
   411
  specific format encountered here.
9060c73a4578 updated;
wenzelm
parents: 20430
diff changeset
   412
20447
5b75f1c4d7d6 more on contexts;
wenzelm
parents: 20438
diff changeset
   413
  \item \verb|Symbol.explode|~\isa{s} produces a symbol list from
5b75f1c4d7d6 more on contexts;
wenzelm
parents: 20438
diff changeset
   414
  the packed form usually encountered as user input.  This function
5b75f1c4d7d6 more on contexts;
wenzelm
parents: 20438
diff changeset
   415
  replaces \verb|String.explode| for virtually all purposes of
5b75f1c4d7d6 more on contexts;
wenzelm
parents: 20438
diff changeset
   416
  manipulating text in Isabelle!  Plain \verb|implode| may be used
5b75f1c4d7d6 more on contexts;
wenzelm
parents: 20438
diff changeset
   417
  for the reverse operation.
20438
9060c73a4578 updated;
wenzelm
parents: 20430
diff changeset
   418
9060c73a4578 updated;
wenzelm
parents: 20430
diff changeset
   419
  \item \verb|Symbol.is_letter|, \verb|Symbol.is_digit|, \verb|Symbol.is_quasi|, \verb|Symbol.is_blank| classify certain symbols
9060c73a4578 updated;
wenzelm
parents: 20430
diff changeset
   420
  (both ASCII and several named ones) according to fixed syntactic
9060c73a4578 updated;
wenzelm
parents: 20430
diff changeset
   421
  convections of Isabelle, e.g.\ see \cite{isabelle-isar-ref}.
9060c73a4578 updated;
wenzelm
parents: 20430
diff changeset
   422
9060c73a4578 updated;
wenzelm
parents: 20430
diff changeset
   423
  \item \verb|Symbol.sym| is a concrete datatype that represents
9060c73a4578 updated;
wenzelm
parents: 20430
diff changeset
   424
  the different kinds of symbols explicitly as \verb|Symbol.Char|,
9060c73a4578 updated;
wenzelm
parents: 20430
diff changeset
   425
  \verb|Symbol.Sym|, \verb|Symbol.Ctrl|, or \verb|Symbol.Raw|.
9060c73a4578 updated;
wenzelm
parents: 20430
diff changeset
   426
9060c73a4578 updated;
wenzelm
parents: 20430
diff changeset
   427
  \item \verb|Symbol.decode| converts the string representation of a
9060c73a4578 updated;
wenzelm
parents: 20430
diff changeset
   428
  symbol into the explicit datatype version.
9060c73a4578 updated;
wenzelm
parents: 20430
diff changeset
   429
9060c73a4578 updated;
wenzelm
parents: 20430
diff changeset
   430
  \end{description}%
9060c73a4578 updated;
wenzelm
parents: 20430
diff changeset
   431
\end{isamarkuptext}%
9060c73a4578 updated;
wenzelm
parents: 20430
diff changeset
   432
\isamarkuptrue%
9060c73a4578 updated;
wenzelm
parents: 20430
diff changeset
   433
%
9060c73a4578 updated;
wenzelm
parents: 20430
diff changeset
   434
\endisatagmlref
9060c73a4578 updated;
wenzelm
parents: 20430
diff changeset
   435
{\isafoldmlref}%
9060c73a4578 updated;
wenzelm
parents: 20430
diff changeset
   436
%
9060c73a4578 updated;
wenzelm
parents: 20430
diff changeset
   437
\isadelimmlref
9060c73a4578 updated;
wenzelm
parents: 20430
diff changeset
   438
%
9060c73a4578 updated;
wenzelm
parents: 20430
diff changeset
   439
\endisadelimmlref
9060c73a4578 updated;
wenzelm
parents: 20430
diff changeset
   440
%
9060c73a4578 updated;
wenzelm
parents: 20430
diff changeset
   441
\isamarkupsubsection{Qualified names and name spaces%
9060c73a4578 updated;
wenzelm
parents: 20430
diff changeset
   442
}
9060c73a4578 updated;
wenzelm
parents: 20430
diff changeset
   443
\isamarkuptrue%
9060c73a4578 updated;
wenzelm
parents: 20430
diff changeset
   444
%
9060c73a4578 updated;
wenzelm
parents: 20430
diff changeset
   445
\isadelimFIXME
9060c73a4578 updated;
wenzelm
parents: 20430
diff changeset
   446
%
9060c73a4578 updated;
wenzelm
parents: 20430
diff changeset
   447
\endisadelimFIXME
9060c73a4578 updated;
wenzelm
parents: 20430
diff changeset
   448
%
9060c73a4578 updated;
wenzelm
parents: 20430
diff changeset
   449
\isatagFIXME
9060c73a4578 updated;
wenzelm
parents: 20430
diff changeset
   450
%
9060c73a4578 updated;
wenzelm
parents: 20430
diff changeset
   451
\begin{isamarkuptext}%
9060c73a4578 updated;
wenzelm
parents: 20430
diff changeset
   452
Qualified names are constructed according to implicit naming
9060c73a4578 updated;
wenzelm
parents: 20430
diff changeset
   453
principles of the present context.
9060c73a4578 updated;
wenzelm
parents: 20430
diff changeset
   454
9060c73a4578 updated;
wenzelm
parents: 20430
diff changeset
   455
9060c73a4578 updated;
wenzelm
parents: 20430
diff changeset
   456
The last component is called \emph{base name}; the remaining prefix of
9060c73a4578 updated;
wenzelm
parents: 20430
diff changeset
   457
qualification may be empty.
9060c73a4578 updated;
wenzelm
parents: 20430
diff changeset
   458
9060c73a4578 updated;
wenzelm
parents: 20430
diff changeset
   459
Some practical conventions help to organize named entities more
9060c73a4578 updated;
wenzelm
parents: 20430
diff changeset
   460
systematically:
9060c73a4578 updated;
wenzelm
parents: 20430
diff changeset
   461
9060c73a4578 updated;
wenzelm
parents: 20430
diff changeset
   462
\begin{itemize}
9060c73a4578 updated;
wenzelm
parents: 20430
diff changeset
   463
9060c73a4578 updated;
wenzelm
parents: 20430
diff changeset
   464
\item Names are qualified first by the theory name, second by an
9060c73a4578 updated;
wenzelm
parents: 20430
diff changeset
   465
optional ``structure''.  For example, a constant \isa{c} declared
9060c73a4578 updated;
wenzelm
parents: 20430
diff changeset
   466
as part of a certain structure \isa{b} (say a type definition) in
9060c73a4578 updated;
wenzelm
parents: 20430
diff changeset
   467
theory \isa{A} will be named \isa{A{\isachardot}b{\isachardot}c} internally.
9060c73a4578 updated;
wenzelm
parents: 20430
diff changeset
   468
9060c73a4578 updated;
wenzelm
parents: 20430
diff changeset
   469
\item
9060c73a4578 updated;
wenzelm
parents: 20430
diff changeset
   470
9060c73a4578 updated;
wenzelm
parents: 20430
diff changeset
   471
\item
9060c73a4578 updated;
wenzelm
parents: 20430
diff changeset
   472
9060c73a4578 updated;
wenzelm
parents: 20430
diff changeset
   473
\item
9060c73a4578 updated;
wenzelm
parents: 20430
diff changeset
   474
9060c73a4578 updated;
wenzelm
parents: 20430
diff changeset
   475
\item
9060c73a4578 updated;
wenzelm
parents: 20430
diff changeset
   476
9060c73a4578 updated;
wenzelm
parents: 20430
diff changeset
   477
\end{itemize}
9060c73a4578 updated;
wenzelm
parents: 20430
diff changeset
   478
9060c73a4578 updated;
wenzelm
parents: 20430
diff changeset
   479
Names of different kinds of entities are basically independent, but
9060c73a4578 updated;
wenzelm
parents: 20430
diff changeset
   480
some practical naming conventions relate them to each other.  For
9060c73a4578 updated;
wenzelm
parents: 20430
diff changeset
   481
example, a constant \isa{foo} may be accompanied with theorems
9060c73a4578 updated;
wenzelm
parents: 20430
diff changeset
   482
\isa{foo{\isachardot}intro}, \isa{foo{\isachardot}elim}, \isa{foo{\isachardot}simps} etc.  The
9060c73a4578 updated;
wenzelm
parents: 20430
diff changeset
   483
same may happen for a type \isa{foo}, which is then apt to cause
9060c73a4578 updated;
wenzelm
parents: 20430
diff changeset
   484
clashes in the theorem name space!  To avoid this, we occasionally
9060c73a4578 updated;
wenzelm
parents: 20430
diff changeset
   485
follow an additional convention of suffixes that determine the
9060c73a4578 updated;
wenzelm
parents: 20430
diff changeset
   486
original kind of entity that a name has been derived.  For example,
9060c73a4578 updated;
wenzelm
parents: 20430
diff changeset
   487
constant \isa{foo} is associated with theorem \isa{foo{\isachardot}intro},
9060c73a4578 updated;
wenzelm
parents: 20430
diff changeset
   488
type \isa{foo} with theorem \isa{foo{\isacharunderscore}type{\isachardot}intro}, and type
9060c73a4578 updated;
wenzelm
parents: 20430
diff changeset
   489
class \isa{foo} with \isa{foo{\isacharunderscore}class{\isachardot}intro}.%
9060c73a4578 updated;
wenzelm
parents: 20430
diff changeset
   490
\end{isamarkuptext}%
9060c73a4578 updated;
wenzelm
parents: 20430
diff changeset
   491
\isamarkuptrue%
9060c73a4578 updated;
wenzelm
parents: 20430
diff changeset
   492
%
9060c73a4578 updated;
wenzelm
parents: 20430
diff changeset
   493
\endisatagFIXME
9060c73a4578 updated;
wenzelm
parents: 20430
diff changeset
   494
{\isafoldFIXME}%
9060c73a4578 updated;
wenzelm
parents: 20430
diff changeset
   495
%
9060c73a4578 updated;
wenzelm
parents: 20430
diff changeset
   496
\isadelimFIXME
9060c73a4578 updated;
wenzelm
parents: 20430
diff changeset
   497
%
9060c73a4578 updated;
wenzelm
parents: 20430
diff changeset
   498
\endisadelimFIXME
9060c73a4578 updated;
wenzelm
parents: 20430
diff changeset
   499
%
9060c73a4578 updated;
wenzelm
parents: 20430
diff changeset
   500
\isamarkupsection{Structured output%
9060c73a4578 updated;
wenzelm
parents: 20430
diff changeset
   501
}
9060c73a4578 updated;
wenzelm
parents: 20430
diff changeset
   502
\isamarkuptrue%
9060c73a4578 updated;
wenzelm
parents: 20430
diff changeset
   503
%
9060c73a4578 updated;
wenzelm
parents: 20430
diff changeset
   504
\isamarkupsubsection{Pretty printing%
9060c73a4578 updated;
wenzelm
parents: 20430
diff changeset
   505
}
9060c73a4578 updated;
wenzelm
parents: 20430
diff changeset
   506
\isamarkuptrue%
9060c73a4578 updated;
wenzelm
parents: 20430
diff changeset
   507
%
9060c73a4578 updated;
wenzelm
parents: 20430
diff changeset
   508
\begin{isamarkuptext}%
9060c73a4578 updated;
wenzelm
parents: 20430
diff changeset
   509
FIXME%
9060c73a4578 updated;
wenzelm
parents: 20430
diff changeset
   510
\end{isamarkuptext}%
9060c73a4578 updated;
wenzelm
parents: 20430
diff changeset
   511
\isamarkuptrue%
9060c73a4578 updated;
wenzelm
parents: 20430
diff changeset
   512
%
9060c73a4578 updated;
wenzelm
parents: 20430
diff changeset
   513
\isamarkupsubsection{Output channels%
9060c73a4578 updated;
wenzelm
parents: 20430
diff changeset
   514
}
9060c73a4578 updated;
wenzelm
parents: 20430
diff changeset
   515
\isamarkuptrue%
9060c73a4578 updated;
wenzelm
parents: 20430
diff changeset
   516
%
9060c73a4578 updated;
wenzelm
parents: 20430
diff changeset
   517
\begin{isamarkuptext}%
9060c73a4578 updated;
wenzelm
parents: 20430
diff changeset
   518
FIXME%
9060c73a4578 updated;
wenzelm
parents: 20430
diff changeset
   519
\end{isamarkuptext}%
9060c73a4578 updated;
wenzelm
parents: 20430
diff changeset
   520
\isamarkuptrue%
9060c73a4578 updated;
wenzelm
parents: 20430
diff changeset
   521
%
9060c73a4578 updated;
wenzelm
parents: 20430
diff changeset
   522
\isamarkupsubsection{Print modes%
9060c73a4578 updated;
wenzelm
parents: 20430
diff changeset
   523
}
9060c73a4578 updated;
wenzelm
parents: 20430
diff changeset
   524
\isamarkuptrue%
9060c73a4578 updated;
wenzelm
parents: 20430
diff changeset
   525
%
9060c73a4578 updated;
wenzelm
parents: 20430
diff changeset
   526
\begin{isamarkuptext}%
9060c73a4578 updated;
wenzelm
parents: 20430
diff changeset
   527
FIXME%
9060c73a4578 updated;
wenzelm
parents: 20430
diff changeset
   528
\end{isamarkuptext}%
9060c73a4578 updated;
wenzelm
parents: 20430
diff changeset
   529
\isamarkuptrue%
9060c73a4578 updated;
wenzelm
parents: 20430
diff changeset
   530
%
18537
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   531
\isadelimtheory
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   532
%
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   533
\endisadelimtheory
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   534
%
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   535
\isatagtheory
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   536
\isacommand{end}\isamarkupfalse%
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   537
%
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   538
\endisatagtheory
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   539
{\isafoldtheory}%
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   540
%
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   541
\isadelimtheory
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   542
%
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   543
\endisadelimtheory
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   544
\isanewline
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   545
\end{isabellebody}%
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   546
%%% Local Variables:
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   547
%%% mode: latex
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   548
%%% TeX-master: "root"
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   549
%%% End: