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