tuned;
authorwenzelm
Wed Aug 30 12:28:32 2006 +0200 (2006-08-30)
changeset 204370eb5e30fd620
parent 20436 0af8655ab0bb
child 20438 9060c73a4578
tuned;
doc-src/IsarImplementation/Thy/logic.thy
doc-src/IsarImplementation/Thy/prelim.thy
     1.1 --- a/doc-src/IsarImplementation/Thy/logic.thy	Wed Aug 30 08:34:45 2006 +0200
     1.2 +++ b/doc-src/IsarImplementation/Thy/logic.thy	Wed Aug 30 12:28:32 2006 +0200
     1.3 @@ -7,6 +7,13 @@
     1.4  
     1.5  section {* Syntax *}
     1.6  
     1.7 +subsection {* Variable names *}
     1.8 +
     1.9 +text {*
    1.10 +  FIXME
    1.11 +*}
    1.12 +
    1.13 +
    1.14  subsection {* Simply-typed lambda calculus *}
    1.15  
    1.16  text {*
     2.1 --- a/doc-src/IsarImplementation/Thy/prelim.thy	Wed Aug 30 08:34:45 2006 +0200
     2.2 +++ b/doc-src/IsarImplementation/Thy/prelim.thy	Wed Aug 30 12:28:32 2006 +0200
     2.3 @@ -5,184 +5,6 @@
     2.4  
     2.5  chapter {* Preliminaries *}
     2.6  
     2.7 -section {* Named entities *}
     2.8 -
     2.9 -text {* Named entities of different kinds (logical constant, type,
    2.10 -type class, theorem, method etc.) live in separate name spaces.  It is
    2.11 -usually clear from the occurrence of a name which kind of entity it
    2.12 -refers to.  For example, proof method @{text "foo"} vs.\ theorem
    2.13 -@{text "foo"} vs.\ logical constant @{text "foo"} are easily
    2.14 -distinguished by means of the syntactic context.  A notable exception
    2.15 -are logical identifiers within a term (\secref{sec:terms}): constants,
    2.16 -fixed variables, and bound variables all share the same identifier
    2.17 -syntax, but are distinguished by their scope.
    2.18 -
    2.19 -Each name space is organized as a collection of \emph{qualified
    2.20 -names}, which consist of a sequence of basic name components separated
    2.21 -by dots: @{text "Bar.bar.foo"}, @{text "Bar.foo"}, and @{text "foo"}
    2.22 -are examples for valid qualified names.  Name components are
    2.23 -subdivided into \emph{symbols}, which constitute the smallest textual
    2.24 -unit in Isabelle --- raw characters are normally not encountered
    2.25 -directly. *}
    2.26 -
    2.27 -
    2.28 -subsection {* Strings of symbols *}
    2.29 -
    2.30 -text {* Isabelle strings consist of a sequence of
    2.31 -symbols\glossary{Symbol}{The smalles unit of text in Isabelle,
    2.32 -subsumes plain ASCII characters as well as an infinite collection of
    2.33 -named symbols (for greek, math etc.).}, which are either packed as an
    2.34 -actual @{text "string"}, or represented as a list.  Each symbol is in
    2.35 -itself a small string of the following form:
    2.36 -
    2.37 -\begin{enumerate}
    2.38 -
    2.39 -\item either a singleton ASCII character ``@{text "c"}'' (with
    2.40 -character code 0--127), for example ``\verb,a,'',
    2.41 -
    2.42 -\item or a regular symbol ``\verb,\,\verb,<,@{text "ident"}\verb,>,'',
    2.43 -for example ``\verb,\,\verb,<alpha>,'',
    2.44 -
    2.45 -\item or a control symbol ``\verb,\,\verb,<^,@{text
    2.46 -"ident"}\verb,>,'', for example ``\verb,\,\verb,<^bold>,'',
    2.47 -
    2.48 -\item or a raw control symbol ``\verb,\,\verb,<^raw:,@{text
    2.49 -"\<dots>"}\verb,>,'' where ``@{text "\<dots>"}'' refers to any
    2.50 -printable ASCII character (excluding ``\verb,.,'' and ``\verb,>,'') or
    2.51 -non-ASCII character, for example ``\verb,\,\verb,<^raw:$\sum_{i = 1}^n$>,'',
    2.52 -
    2.53 -\item or a numbered raw control symbol ``\verb,\,\verb,<^raw,@{text
    2.54 -"nnn"}\verb,>, where @{text "nnn"} are digits, for example
    2.55 -``\verb,\,\verb,<^raw42>,''.
    2.56 -
    2.57 -\end{enumerate}
    2.58 -
    2.59 -The @{text "ident"} syntax for symbol names is @{text "letter (letter
    2.60 -| digit)\<^sup>*"}, where @{text "letter = A..Za..Z"} and @{text
    2.61 -"digit = 0..9"}.  There are infinitely many regular symbols and
    2.62 -control symbols available, but a certain collection of standard
    2.63 -symbols is treated specifically.  For example,
    2.64 -``\verb,\,\verb,<alpha>,'' is classified as a (non-ASCII) letter,
    2.65 -which means it may occur within regular Isabelle identifier syntax.
    2.66 -
    2.67 -Output of symbols depends on the print mode (\secref{sec:print-mode}).
    2.68 -For example, the standard {\LaTeX} setup of the Isabelle document
    2.69 -preparation system would present ``\verb,\,\verb,<alpha>,'' as @{text
    2.70 -"\<alpha>"}, and ``\verb,\,\verb,<^bold>,\verb,\,\verb,<alpha>,'' as @{text
    2.71 -"\<^bold>\<alpha>"}.
    2.72 -
    2.73 -\medskip It is important to note that the character set underlying
    2.74 -Isabelle symbols is plain 7-bit ASCII.  Since 8-bit characters are
    2.75 -passed through transparently, Isabelle may easily process actual
    2.76 -Unicode/UCS data (using the well-known UTF-8 encoding, for example).
    2.77 -Unicode provides its own collection of mathematical symbols, but there
    2.78 -is presently no link to Isabelle's named ones; both kinds of symbols
    2.79 -coexist independently. *}
    2.80 -
    2.81 -text %mlref {*
    2.82 -  \begin{mldecls}
    2.83 -  @{index_ML_type "Symbol.symbol"} \\
    2.84 -  @{index_ML Symbol.explode: "string -> Symbol.symbol list"} \\
    2.85 -  @{index_ML Symbol.is_letter: "Symbol.symbol -> bool"} \\
    2.86 -  @{index_ML Symbol.is_digit: "Symbol.symbol -> bool"} \\
    2.87 -  @{index_ML Symbol.is_quasi: "Symbol.symbol -> bool"} \\
    2.88 -  @{index_ML Symbol.is_blank: "Symbol.symbol -> bool"} \\
    2.89 -  @{index_ML_type "Symbol.sym"} \\
    2.90 -  @{index_ML Symbol.decode: "Symbol.symbol -> Symbol.sym"} \\
    2.91 -  \end{mldecls}
    2.92 -
    2.93 -  \begin{description}
    2.94 -
    2.95 -  \item @{ML_type "Symbol.symbol"} represents Isabelle symbols; this type
    2.96 -  is merely an alias for @{ML_type "string"}, but emphasizes the
    2.97 -  specific format encountered here.
    2.98 -
    2.99 -  \item @{ML "Symbol.explode"}~@{text "s"} produces an actual symbol
   2.100 -  list from the packed form usually encountered as user input.  This
   2.101 -  function replaces @{ML "String.explode"} for virtually all purposes
   2.102 -  of manipulating text in Isabelle!  Plain @{text "implode"} may be
   2.103 -  used for the reverse operation.
   2.104 -
   2.105 -  \item @{ML "Symbol.is_letter"}, @{ML "Symbol.is_digit"}, @{ML
   2.106 -  "Symbol.is_quasi"}, @{ML "Symbol.is_blank"} classify certain symbols
   2.107 -  (both ASCII and several named ones) according to fixed syntactic
   2.108 -  convections of Isabelle, e.g.\ see \cite{isabelle-isar-ref}.
   2.109 -
   2.110 -  \item @{ML_type "Symbol.sym"} is a concrete datatype that represents
   2.111 -  the different kinds of symbols explicitly as @{ML "Symbol.Char"},
   2.112 -  @{ML "Symbol.Sym"}, @{ML "Symbol.Ctrl"}, or @{ML "Symbol.Raw"}.
   2.113 -
   2.114 -  \item @{ML "Symbol.decode"} converts the string representation of a
   2.115 -  symbol into the explicit datatype version.
   2.116 -
   2.117 -  \end{description}
   2.118 -*}
   2.119 -
   2.120 -
   2.121 -subsection {* Simple names *}
   2.122 -
   2.123 -text FIXME
   2.124 -
   2.125 -
   2.126 -subsection {* Qualified names and name spaces *}
   2.127 -
   2.128 -text %FIXME {* Qualified names are constructed according to implicit naming
   2.129 -principles of the present context.
   2.130 -
   2.131 -
   2.132 -The last component is called \emph{base name}; the remaining prefix of
   2.133 -qualification may be empty.
   2.134 -
   2.135 -Some practical conventions help to organize named entities more
   2.136 -systematically:
   2.137 -
   2.138 -\begin{itemize}
   2.139 -
   2.140 -\item Names are qualified first by the theory name, second by an
   2.141 -optional ``structure''.  For example, a constant @{text "c"} declared
   2.142 -as part of a certain structure @{text "b"} (say a type definition) in
   2.143 -theory @{text "A"} will be named @{text "A.b.c"} internally.
   2.144 -
   2.145 -\item
   2.146 -
   2.147 -\item
   2.148 -
   2.149 -\item
   2.150 -
   2.151 -\item
   2.152 -
   2.153 -\end{itemize}
   2.154 -
   2.155 -Names of different kinds of entities are basically independent, but
   2.156 -some practical naming conventions relate them to each other.  For
   2.157 -example, a constant @{text "foo"} may be accompanied with theorems
   2.158 -@{text "foo.intro"}, @{text "foo.elim"}, @{text "foo.simps"} etc.  The
   2.159 -same may happen for a type @{text "foo"}, which is then apt to cause
   2.160 -clashes in the theorem name space!  To avoid this, we occasionally
   2.161 -follow an additional convention of suffixes that determine the
   2.162 -original kind of entity that a name has been derived.  For example,
   2.163 -constant @{text "foo"} is associated with theorem @{text "foo.intro"},
   2.164 -type @{text "foo"} with theorem @{text "foo_type.intro"}, and type
   2.165 -class @{text "foo"} with @{text "foo_class.intro"}.
   2.166 -
   2.167 -*}
   2.168 -
   2.169 -
   2.170 -section {* Structured output *}
   2.171 -
   2.172 -subsection {* Pretty printing *}
   2.173 -
   2.174 -text FIXME
   2.175 -
   2.176 -subsection {* Output channels *}
   2.177 -
   2.178 -text FIXME
   2.179 -
   2.180 -subsection {* Print modes *}
   2.181 -
   2.182 -text FIXME
   2.183 -
   2.184 -
   2.185  section {* Contexts \label{sec:context} *}
   2.186  
   2.187  text {*
   2.188 @@ -362,4 +184,178 @@
   2.189  
   2.190  text %mlref {* FIXME *}
   2.191  
   2.192 +
   2.193 +section {* Named entities *}
   2.194 +
   2.195 +text {* Named entities of different kinds (logical constant, type,
   2.196 +type class, theorem, method etc.) live in separate name spaces.  It is
   2.197 +usually clear from the occurrence of a name which kind of entity it
   2.198 +refers to.  For example, proof method @{text "foo"} vs.\ theorem
   2.199 +@{text "foo"} vs.\ logical constant @{text "foo"} are easily
   2.200 +distinguished by means of the syntactic context.  A notable exception
   2.201 +are logical identifiers within a term (\secref{sec:terms}): constants,
   2.202 +fixed variables, and bound variables all share the same identifier
   2.203 +syntax, but are distinguished by their scope.
   2.204 +
   2.205 +Each name space is organized as a collection of \emph{qualified
   2.206 +names}, which consist of a sequence of basic name components separated
   2.207 +by dots: @{text "Bar.bar.foo"}, @{text "Bar.foo"}, and @{text "foo"}
   2.208 +are examples for valid qualified names.  Name components are
   2.209 +subdivided into \emph{symbols}, which constitute the smallest textual
   2.210 +unit in Isabelle --- raw characters are normally not encountered
   2.211 +directly. *}
   2.212 +
   2.213 +
   2.214 +subsection {* Strings of symbols *}
   2.215 +
   2.216 +text {* Isabelle strings consist of a sequence of
   2.217 +symbols\glossary{Symbol}{The smalles unit of text in Isabelle,
   2.218 +subsumes plain ASCII characters as well as an infinite collection of
   2.219 +named symbols (for greek, math etc.).}, which are either packed as an
   2.220 +actual @{text "string"}, or represented as a list.  Each symbol is in
   2.221 +itself a small string of the following form:
   2.222 +
   2.223 +\begin{enumerate}
   2.224 +
   2.225 +\item either a singleton ASCII character ``@{text "c"}'' (with
   2.226 +character code 0--127), for example ``\verb,a,'',
   2.227 +
   2.228 +\item or a regular symbol ``\verb,\,\verb,<,@{text "ident"}\verb,>,'',
   2.229 +for example ``\verb,\,\verb,<alpha>,'',
   2.230 +
   2.231 +\item or a control symbol ``\verb,\,\verb,<^,@{text
   2.232 +"ident"}\verb,>,'', for example ``\verb,\,\verb,<^bold>,'',
   2.233 +
   2.234 +\item or a raw control symbol ``\verb,\,\verb,<^raw:,@{text
   2.235 +"\<dots>"}\verb,>,'' where ``@{text "\<dots>"}'' refers to any
   2.236 +printable ASCII character (excluding ``\verb,.,'' and ``\verb,>,'') or
   2.237 +non-ASCII character, for example ``\verb,\,\verb,<^raw:$\sum_{i = 1}^n$>,'',
   2.238 +
   2.239 +\item or a numbered raw control symbol ``\verb,\,\verb,<^raw,@{text
   2.240 +"nnn"}\verb,>, where @{text "nnn"} are digits, for example
   2.241 +``\verb,\,\verb,<^raw42>,''.
   2.242 +
   2.243 +\end{enumerate}
   2.244 +
   2.245 +The @{text "ident"} syntax for symbol names is @{text "letter (letter
   2.246 +| digit)\<^sup>*"}, where @{text "letter = A..Za..Z"} and @{text
   2.247 +"digit = 0..9"}.  There are infinitely many regular symbols and
   2.248 +control symbols available, but a certain collection of standard
   2.249 +symbols is treated specifically.  For example,
   2.250 +``\verb,\,\verb,<alpha>,'' is classified as a (non-ASCII) letter,
   2.251 +which means it may occur within regular Isabelle identifier syntax.
   2.252 +
   2.253 +Output of symbols depends on the print mode (\secref{sec:print-mode}).
   2.254 +For example, the standard {\LaTeX} setup of the Isabelle document
   2.255 +preparation system would present ``\verb,\,\verb,<alpha>,'' as @{text
   2.256 +"\<alpha>"}, and ``\verb,\,\verb,<^bold>,\verb,\,\verb,<alpha>,'' as @{text
   2.257 +"\<^bold>\<alpha>"}.
   2.258 +
   2.259 +\medskip It is important to note that the character set underlying
   2.260 +Isabelle symbols is plain 7-bit ASCII.  Since 8-bit characters are
   2.261 +passed through transparently, Isabelle may easily process actual
   2.262 +Unicode/UCS data (using the well-known UTF-8 encoding, for example).
   2.263 +Unicode provides its own collection of mathematical symbols, but there
   2.264 +is presently no link to Isabelle's named ones; both kinds of symbols
   2.265 +coexist independently. *}
   2.266 +
   2.267 +text %mlref {*
   2.268 +  \begin{mldecls}
   2.269 +  @{index_ML_type "Symbol.symbol"} \\
   2.270 +  @{index_ML Symbol.explode: "string -> Symbol.symbol list"} \\
   2.271 +  @{index_ML Symbol.is_letter: "Symbol.symbol -> bool"} \\
   2.272 +  @{index_ML Symbol.is_digit: "Symbol.symbol -> bool"} \\
   2.273 +  @{index_ML Symbol.is_quasi: "Symbol.symbol -> bool"} \\
   2.274 +  @{index_ML Symbol.is_blank: "Symbol.symbol -> bool"} \\
   2.275 +  @{index_ML_type "Symbol.sym"} \\
   2.276 +  @{index_ML Symbol.decode: "Symbol.symbol -> Symbol.sym"} \\
   2.277 +  \end{mldecls}
   2.278 +
   2.279 +  \begin{description}
   2.280 +
   2.281 +  \item @{ML_type "Symbol.symbol"} represents Isabelle symbols; this type
   2.282 +  is merely an alias for @{ML_type "string"}, but emphasizes the
   2.283 +  specific format encountered here.
   2.284 +
   2.285 +  \item @{ML "Symbol.explode"}~@{text "s"} produces an actual symbol
   2.286 +  list from the packed form usually encountered as user input.  This
   2.287 +  function replaces @{ML "String.explode"} for virtually all purposes
   2.288 +  of manipulating text in Isabelle!  Plain @{text "implode"} may be
   2.289 +  used for the reverse operation.
   2.290 +
   2.291 +  \item @{ML "Symbol.is_letter"}, @{ML "Symbol.is_digit"}, @{ML
   2.292 +  "Symbol.is_quasi"}, @{ML "Symbol.is_blank"} classify certain symbols
   2.293 +  (both ASCII and several named ones) according to fixed syntactic
   2.294 +  convections of Isabelle, e.g.\ see \cite{isabelle-isar-ref}.
   2.295 +
   2.296 +  \item @{ML_type "Symbol.sym"} is a concrete datatype that represents
   2.297 +  the different kinds of symbols explicitly as @{ML "Symbol.Char"},
   2.298 +  @{ML "Symbol.Sym"}, @{ML "Symbol.Ctrl"}, or @{ML "Symbol.Raw"}.
   2.299 +
   2.300 +  \item @{ML "Symbol.decode"} converts the string representation of a
   2.301 +  symbol into the explicit datatype version.
   2.302 +
   2.303 +  \end{description}
   2.304 +*}
   2.305 +
   2.306 +
   2.307 +subsection {* Qualified names and name spaces *}
   2.308 +
   2.309 +text %FIXME {* Qualified names are constructed according to implicit naming
   2.310 +principles of the present context.
   2.311 +
   2.312 +
   2.313 +The last component is called \emph{base name}; the remaining prefix of
   2.314 +qualification may be empty.
   2.315 +
   2.316 +Some practical conventions help to organize named entities more
   2.317 +systematically:
   2.318 +
   2.319 +\begin{itemize}
   2.320 +
   2.321 +\item Names are qualified first by the theory name, second by an
   2.322 +optional ``structure''.  For example, a constant @{text "c"} declared
   2.323 +as part of a certain structure @{text "b"} (say a type definition) in
   2.324 +theory @{text "A"} will be named @{text "A.b.c"} internally.
   2.325 +
   2.326 +\item
   2.327 +
   2.328 +\item
   2.329 +
   2.330 +\item
   2.331 +
   2.332 +\item
   2.333 +
   2.334 +\end{itemize}
   2.335 +
   2.336 +Names of different kinds of entities are basically independent, but
   2.337 +some practical naming conventions relate them to each other.  For
   2.338 +example, a constant @{text "foo"} may be accompanied with theorems
   2.339 +@{text "foo.intro"}, @{text "foo.elim"}, @{text "foo.simps"} etc.  The
   2.340 +same may happen for a type @{text "foo"}, which is then apt to cause
   2.341 +clashes in the theorem name space!  To avoid this, we occasionally
   2.342 +follow an additional convention of suffixes that determine the
   2.343 +original kind of entity that a name has been derived.  For example,
   2.344 +constant @{text "foo"} is associated with theorem @{text "foo.intro"},
   2.345 +type @{text "foo"} with theorem @{text "foo_type.intro"}, and type
   2.346 +class @{text "foo"} with @{text "foo_class.intro"}.
   2.347 +
   2.348 +*}
   2.349 +
   2.350 +
   2.351 +section {* Structured output *}
   2.352 +
   2.353 +subsection {* Pretty printing *}
   2.354 +
   2.355 +text FIXME
   2.356 +
   2.357 +subsection {* Output channels *}
   2.358 +
   2.359 +text FIXME
   2.360 +
   2.361 +subsection {* Print modes *}
   2.362 +
   2.363 +text FIXME
   2.364 +
   2.365 +
   2.366  end