--- a/doc-src/TutorialI/Documents/document/Documents.tex Sat Jan 05 01:14:46 2002 +0100
+++ b/doc-src/TutorialI/Documents/document/Documents.tex Sat Jan 05 01:15:12 2002 +0100
@@ -82,10 +82,10 @@
\medskip The keyword \isakeyword{infixl} specifies an operator that
is nested to the \emph{left}: in iterated applications the more
complex expression appears on the left-hand side: \isa{A\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ B\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ C} stands for \isa{{\isacharparenleft}A\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ B{\isacharparenright}\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ C}. Similarly,
- \isakeyword{infixr} refers to nesting to the \emph{right}, which
- would turn \isa{A\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ B\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ C} into \isa{A\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ {\isacharparenleft}B\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ C{\isacharparenright}}.
- In contrast, a \emph{non-oriented} declaration via
- \isakeyword{infix} would always demand explicit parentheses.
+ \isakeyword{infixr} refers to nesting to the \emph{right}, reading
+ \isa{A\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ B\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ C} as \isa{A\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ {\isacharparenleft}B\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ C{\isacharparenright}}. In contrast,
+ a \emph{non-oriented} declaration via \isakeyword{infix} would
+ always demand explicit parentheses.
Many binary operations observe the associative law, so the exact
grouping does not matter. Nevertheless, formal statements need be
@@ -103,28 +103,234 @@
expressions as required. Note that the system would actually print
the above statement as \isa{A\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ B\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ C\ {\isacharequal}\ A\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ {\isacharparenleft}B\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ C{\isacharparenright}}
(due to nesting to the left). We have preferred to give the fully
- parenthesized form in the text for clarity.%
+ parenthesized form in the text for clarity. Only in rare situations
+ one may consider to force parentheses by use of non-oriented infix
+ syntax; equality would probably be a typical candidate.%
\end{isamarkuptext}%
\isamarkuptrue%
+%
+\isamarkupsubsection{Mathematical symbols \label{sec:thy-present-symbols}%
+}
\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+Concrete syntax based on plain ASCII characters has its inherent
+ limitations. Rich mathematical notation demands a larger repertoire
+ of symbols. Several standards of extended character sets have been
+ proposed over decades, but none has become universally available so
+ far, not even Unicode\index{Unicode}.
+
+ Isabelle supports a generic notion of
+ \emph{symbols}\index{symbols|bold} as the smallest entities of
+ source text, without referring to internal encodings. Such
+ ``generalized characters'' may be of one of the following three
+ kinds:
+
+ \begin{enumerate}
+
+ \item Traditional 7-bit ASCII characters.
+
+ \item Named symbols: \verb,\,\verb,<,$ident$\verb,>, (or
+ \verb,\\,\verb,<,$ident$\verb,>,).
+
+ \item Named control symbols: \verb,\,\verb,<^,$ident$\verb,>, (or
+ \verb,\\,\verb,<^,$ident$\verb,>,).
+
+ \end{enumerate}
+
+ Here $ident$ may be any identifier according to the usual Isabelle
+ conventions. This results in an infinite store of symbols, whose
+ interpretation is left to further front-end tools. For example, the
+ \verb,\,\verb,<forall>, symbol of Isabelle is really displayed as
+ $\forall$ --- both by the user-interface of Proof~General + X-Symbol
+ and the Isabelle document processor (see \S\ref{FIXME}).
+
+ A list of standard Isabelle symbols is given in
+ \cite[appendix~A]{isabelle-sys}. Users may introduce their own
+ interpretation of further symbols by configuring the appropriate
+ front-end tool accordingly, e.g.\ defining appropriate {\LaTeX}
+ macros for document preparation. There are also a few predefined
+ control symbols, such as \verb,\,\verb,<^sub>, and
+ \verb,\,\verb,<^sup>, for sub- and superscript of the subsequent
+ (printable) symbol, respectively.
+
+ \medskip The following version of our \isa{xor} definition uses a
+ standard Isabelle symbol to achieve typographically pleasing output.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isamarkupfalse%
+\isamarkupfalse%
+\isacommand{constdefs}\isanewline
+\ \ xor\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}bool\ {\isasymRightarrow}\ bool\ {\isasymRightarrow}\ bool{\isachardoublequote}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequote}{\isasymoplus}{\isachardoublequote}\ {\isadigit{6}}{\isadigit{0}}{\isacharparenright}\isanewline
+\ \ {\isachardoublequote}A\ {\isasymoplus}\ B\ {\isasymequiv}\ {\isacharparenleft}A\ {\isasymand}\ {\isasymnot}\ B{\isacharparenright}\ {\isasymor}\ {\isacharparenleft}{\isasymnot}\ A\ {\isasymand}\ B{\isacharparenright}{\isachardoublequote}\isamarkupfalse%
+\isamarkupfalse%
+%
+\begin{isamarkuptext}%
+The X-Symbol package within Proof~General provides several input
+ methods to enter \isa{{\isasymoplus}} in the text. If all fails one may just
+ type \verb,\,\verb,<oplus>, by hand; the display is adapted
+ immediately after continuing further input.
+
+ \medskip A slightly more refined scheme is to provide alternative
+ syntax via the \emph{print mode}\index{print mode} concept of
+ Isabelle (see also \cite{isabelle-ref}). By convention, the mode
+ ``$xsymbols$'' is enabled whenever X-Symbol is active. Consider the
+ following hybrid declaration of \isa{xor}.%
+\end{isamarkuptext}%
\isamarkuptrue%
\isamarkupfalse%
\isamarkupfalse%
+\isacommand{constdefs}\isanewline
+\ \ xor\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}bool\ {\isasymRightarrow}\ bool\ {\isasymRightarrow}\ bool{\isachardoublequote}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequote}{\isacharbrackleft}{\isacharplus}{\isacharbrackright}{\isasymignore}{\isachardoublequote}\ {\isadigit{6}}{\isadigit{0}}{\isacharparenright}\isanewline
+\ \ {\isachardoublequote}A\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}{\isasymignore}\ B\ {\isasymequiv}\ {\isacharparenleft}A\ {\isasymand}\ {\isasymnot}\ B{\isacharparenright}\ {\isasymor}\ {\isacharparenleft}{\isasymnot}\ A\ {\isasymand}\ B{\isacharparenright}{\isachardoublequote}\isanewline
+\isanewline
\isamarkupfalse%
+\isacommand{syntax}\ {\isacharparenleft}xsymbols{\isacharparenright}\isanewline
+\ \ xor\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}bool\ {\isasymRightarrow}\ bool\ {\isasymRightarrow}\ bool{\isachardoublequote}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequote}{\isasymoplus}{\isasymignore}{\isachardoublequote}\ {\isadigit{6}}{\isadigit{0}}{\isacharparenright}\isamarkupfalse%
\isamarkupfalse%
-\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+Here the \commdx{syntax} command acts like \isakeyword{consts}, but
+ without declaring a logical constant, and with an optional print
+ mode specification. Note that the type declaration given here
+ merely serves for syntactic purposes, and is not checked for
+ consistency with the real constant.
+
+ \medskip Now we may write either \isa{{\isacharbrackleft}{\isacharplus}{\isacharbrackright}} or \isa{{\isasymoplus}} in
+ input, while output uses the nicer syntax of $xsymbols$, provided
+ that print mode is presently active. This scheme is particularly
+ useful for interactive development, with the user typing plain ASCII
+ text, but gaining improved visual feedback from the system (say in
+ current goal output).
+
+ \begin{warn}
+ Using alternative syntax declarations easily results in varying
+ versions of input sources. Isabelle provides no systematic way to
+ convert alternative expressions back and forth. Print modes only
+ affect situations where formal entities are pretty printed by the
+ Isabelle process (e.g.\ output of terms and types), but not the
+ original theory text.
+ \end{warn}
+
+ \medskip The following variant makes the alternative \isa{{\isasymoplus}}
+ notation only available for output. Thus we may enforce input
+ sources to refer to plain ASCII only.%
+\end{isamarkuptext}%
\isamarkuptrue%
-\isamarkupfalse%
+\isacommand{syntax}\ {\isacharparenleft}xsymbols\ \isakeyword{output}{\isacharparenright}\isanewline
+\ \ xor\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}bool\ {\isasymRightarrow}\ bool\ {\isasymRightarrow}\ bool{\isachardoublequote}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequote}{\isasymoplus}{\isasymignore}{\isachardoublequote}\ {\isadigit{6}}{\isadigit{0}}{\isacharparenright}\isamarkupfalse%
+%
+\isamarkupsubsection{Prefixes%
+}
\isamarkuptrue%
-\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+Prefix syntax annotations\index{prefix annotation|bold} are just a
+ very degenerate of the general mixfix form \cite{isabelle-ref},
+ without any template arguments or priorities --- just some piece of
+ literal syntax.
+
+ The following example illustrates this idea idea by associating
+ common symbols with the constructors of a currency datatype.%
+\end{isamarkuptext}%
\isamarkuptrue%
-\isamarkupfalse%
+\isacommand{datatype}\ currency\ {\isacharequal}\isanewline
+\ \ \ \ Euro\ nat\ \ \ \ {\isacharparenleft}{\isachardoublequote}{\isasymeuro}{\isachardoublequote}{\isacharparenright}\isanewline
+\ \ {\isacharbar}\ Pounds\ nat\ \ {\isacharparenleft}{\isachardoublequote}{\isasympounds}{\isachardoublequote}{\isacharparenright}\isanewline
+\ \ {\isacharbar}\ Yen\ nat\ \ \ \ \ {\isacharparenleft}{\isachardoublequote}{\isasymyen}{\isachardoublequote}{\isacharparenright}\isanewline
+\ \ {\isacharbar}\ Dollar\ nat\ \ {\isacharparenleft}{\isachardoublequote}{\isachardollar}{\isachardoublequote}{\isacharparenright}\isamarkupfalse%
+%
+\begin{isamarkuptext}%
+Here the degenerate mixfix annotations on the rightmost column
+ happen to consist of a single Isabelle symbol each:
+ \verb,\,\verb,<euro>,, \verb,\,\verb,<pounds>,,
+ \verb,\,\verb,<yen>,, and \verb,\,\verb,<dollar>,.
+
+ Recall that a constructor like \isa{Euro} actually is a function
+ \isa{nat\ {\isasymRightarrow}\ currency}. An expression like \isa{Euro\ {\isadigit{1}}{\isadigit{0}}} will
+ be printed as \isa{{\isasymeuro}\ {\isadigit{1}}{\isadigit{0}}}. Merely the head of the application is
+ subject to our trivial concrete syntax; this form is sufficient to
+ achieve fair conformance to EU~Commission standards of currency
+ notation.
+
+ \medskip Certainly, the same idea of prefix syntax also works for
+ \isakeyword{consts}, \isakeyword{constdefs} etc. For example, we
+ might introduce a (slightly unrealistic) function to calculate an
+ abstract currency value, by cases on the datatype constructors and
+ fixed exchange rates.%
+\end{isamarkuptext}%
\isamarkuptrue%
+\isacommand{consts}\isanewline
+\ \ currency\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}currency\ {\isasymRightarrow}\ nat{\isachardoublequote}\ \ \ \ {\isacharparenleft}{\isachardoublequote}{\isasymcurrency}{\isachardoublequote}{\isacharparenright}\isamarkupfalse%
+%
+\begin{isamarkuptext}%
+\noindent The funny symbol encountered here is that of
+ \verb,\<currency>,.%
+\end{isamarkuptext}%
\isamarkuptrue%
+%
+\isamarkupsubsection{Syntax translations \label{sec:def-translations}%
+}
\isamarkuptrue%
-\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+FIXME
+
+\index{syntax translations|(}%
+\index{translations@\isacommand {translations} (command)|(}
+Isabelle offers an additional definitional facility,
+\textbf{syntax translations}.
+They resemble macros: upon parsing, the defined concept is immediately
+replaced by its definition. This effect is reversed upon printing. For example,
+the symbol \isa{{\isasymnoteq}} is defined via a syntax translation:%
+\end{isamarkuptext}%
\isamarkuptrue%
+\isacommand{translations}\ {\isachardoublequote}x\ {\isasymnoteq}\ y{\isachardoublequote}\ {\isasymrightleftharpoons}\ {\isachardoublequote}{\isasymnot}{\isacharparenleft}x\ {\isacharequal}\ y{\isacharparenright}{\isachardoublequote}\isamarkupfalse%
+%
+\begin{isamarkuptext}%
+\index{$IsaEqTrans@\isasymrightleftharpoons}
+\noindent
+Internally, \isa{{\isasymnoteq}} never appears.
+
+In addition to \isa{{\isasymrightleftharpoons}} there are
+\isa{{\isasymrightharpoonup}}\index{$IsaEqTrans1@\isasymrightharpoonup}
+and \isa{{\isasymleftharpoondown}}\index{$IsaEqTrans2@\isasymleftharpoondown}
+for uni-directional translations, which only affect
+parsing or printing. This tutorial will not cover the details of
+translations. We have mentioned the concept merely because it
+crops up occasionally; a number of HOL's built-in constructs are defined
+via translations. Translations are preferable to definitions when the new
+concept is a trivial variation on an existing one. For example, we
+don't need to derive new theorems about \isa{{\isasymnoteq}}, since existing theorems
+about \isa{{\isacharequal}} still apply.%
+\index{syntax translations|)}%
+\index{translations@\isacommand {translations} (command)|)}%
+\end{isamarkuptext}%
\isamarkuptrue%
+%
+\isamarkupsection{Document preparation%
+}
+\isamarkuptrue%
+%
+\isamarkupsubsection{Batch-mode sessions%
+}
+\isamarkuptrue%
+%
+\isamarkupsubsection{{\LaTeX} macros%
+}
+\isamarkuptrue%
+%
+\isamarkupsubsubsection{Structure markup%
+}
+\isamarkuptrue%
+%
+\isamarkupsubsubsection{Symbols and characters%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+FIXME%
+\end{isamarkuptext}%
\isamarkuptrue%
\isamarkupfalse%
\end{isabellebody}%