--- a/doc-src/TutorialI/Documents/document/Documents.tex Sun Jan 06 13:48:18 2002 +0100
+++ b/doc-src/TutorialI/Documents/document/Documents.tex Sun Jan 06 16:50:31 2002 +0100
@@ -108,7 +108,7 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
-\isamarkupsubsection{Mathematical Symbols \label{sec:thy-present-symbols}%
+\isamarkupsubsection{Mathematical Symbols%
}
\isamarkuptrue%
%
@@ -141,7 +141,7 @@
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}).
+ and the Isabelle document processor (see \S\ref{sec:document-prep}).
A list of standard Isabelle symbols is given in
\cite[appendix~A]{isabelle-sys}. Users may introduce their own
@@ -239,68 +239,101 @@
\ \ {\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:
+\noindent 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>,, \verb,$,.
+ \verb,\,\verb,<yen>,, and \verb,$,.
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}}}. Only the head of the application is
- subject to our concrete syntax; this simple form already achieves
+ be printed as \isa{{\isasymeuro}\ {\isadigit{1}}{\isadigit{0}}}; only the head of the application is
+ subject to our concrete syntax. This simple form already achieves
conformance with notational standards of the European Commission.
\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. The funny symbol used here is that of
- \verb,\<currency>,.%
+ \isakeyword{consts}, \isakeyword{constdefs} etc. The slightly
+ unusual syntax declaration below decorates the existing \isa{currency} type with the international currency symbol \isa{{\isasymcurrency}}
+ (\verb,\,\verb,<currency>,).%
\end{isamarkuptext}%
\isamarkuptrue%
-\isacommand{consts}\isanewline
-\ \ currency\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}currency\ {\isasymRightarrow}\ nat{\isachardoublequote}\ \ \ \ {\isacharparenleft}{\isachardoublequote}{\isasymcurrency}{\isachardoublequote}{\isacharparenright}\isamarkupfalse%
+\isacommand{syntax}\isanewline
+\ \ currency\ {\isacharcolon}{\isacharcolon}\ type\ \ \ \ {\isacharparenleft}{\isachardoublequote}{\isasymcurrency}{\isachardoublequote}{\isacharparenright}\isamarkupfalse%
%
-\isamarkupsubsection{Syntax Translations \label{sec:def-translations}%
+\begin{isamarkuptext}%
+\noindent Here \isa{type} refers to the builtin syntactic category
+ of Isabelle types. We could now write down funny things like \isa{{\isasymeuro}\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ {\isasymcurrency}}, for example.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsection{Syntax Translations \label{sec:syntax-translations}%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
-FIXME
+Mixfix syntax annotations work well for those situations, where a
+ constant application forms needs to be decorated by concrete syntax.
+ Just reconsider \isa{xor\ A\ B} versus \isa{A\ {\isasymoplus}\ B} covered
+ before. Occasionally, the relationship between some piece of
+ notation and its internal form is slightly more involved.
-\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:%
+ Here the concept of \bfindex{syntax translations} enters the scene.
+ Using the raw \isakeyword{syntax}\index{syntax (command)} command we
+ introduce uninterpreted notational elements, while
+ \commdx{translations} relates the input forms with certain logical
+ expressions. This essentially provides a simple mechanism for for
+ syntactic macros; even heavier transformations may be programmed in
+ ML \cite{isabelle-ref}.
+
+ \medskip A typical example of syntax translations is to decorate an
+ relational expression (i.e.\ set membership of tuples) with nice
+ symbolic notation, such as \isa{{\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}\ {\isasymin}\ sim} versus \isa{x\ {\isasymapprox}\ y}.%
\end{isamarkuptext}%
\isamarkuptrue%
-\isacommand{translations}\ {\isachardoublequote}x\ {\isasymnoteq}\ y{\isachardoublequote}\ {\isasymrightleftharpoons}\ {\isachardoublequote}{\isasymnot}{\isacharparenleft}x\ {\isacharequal}\ y{\isacharparenright}{\isachardoublequote}\isamarkupfalse%
+\isacommand{consts}\isanewline
+\ \ sim\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set{\isachardoublequote}\isanewline
+\isanewline
+\isamarkupfalse%
+\isacommand{syntax}\isanewline
+\ \ {\isachardoublequote}{\isacharunderscore}sim{\isachardoublequote}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ bool{\isachardoublequote}\ \ \ \ {\isacharparenleft}\isakeyword{infix}\ {\isachardoublequote}{\isasymapprox}{\isachardoublequote}\ {\isadigit{5}}{\isadigit{0}}{\isacharparenright}\isanewline
+\isamarkupfalse%
+\isacommand{translations}\isanewline
+\ \ {\isachardoublequote}x\ {\isasymapprox}\ y{\isachardoublequote}\ {\isasymrightleftharpoons}\ {\isachardoublequote}{\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}\ {\isasymin}\ sim{\isachardoublequote}\isamarkupfalse%
%
\begin{isamarkuptext}%
-\index{$IsaEqTrans@\isasymrightleftharpoons}
-\noindent
-Internally, \isa{{\isasymnoteq}} never appears.
+\noindent Here the name of the dummy constant \isa{{\isacharunderscore}sim} does
+ not really matter, as long as it is not used otherwise. Prefixing
+ an underscore is a common convention. The \isakeyword{translations}
+ declaration already uses concrete syntax on the left-hand side;
+ internally we relate a raw application \isa{{\isacharunderscore}sim\ x\ y} with
+ \isa{{\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}\ {\isasymin}\ sim}.
-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)|)}%
+ \medskip Another useful application of syntax translations is to
+ provide variant versions of fundamental relational expressions, such
+ as \isa{{\isasymnoteq}} for negated equalities. The following declaration
+ stems from Isabelle/HOL itself:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{syntax}\ {\isachardoublequote}{\isacharunderscore}not{\isacharunderscore}equal{\isachardoublequote}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ bool{\isachardoublequote}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequote}{\isasymnoteq}{\isasymignore}{\isachardoublequote}\ {\isadigit{5}}{\isadigit{0}}{\isacharparenright}\isanewline
+\isamarkupfalse%
+\isacommand{translations}\ {\isachardoublequote}x\ {\isasymnoteq}{\isasymignore}\ y{\isachardoublequote}\ {\isasymrightleftharpoons}\ {\isachardoublequote}{\isasymnot}\ {\isacharparenleft}x\ {\isacharequal}\ y{\isacharparenright}{\isachardoublequote}\isamarkupfalse%
+%
+\begin{isamarkuptext}%
+\noindent Normally one would introduce derived concepts like this
+ within the logic, using \isakeyword{consts} and \isakeyword{defs}
+ instead of \isakeyword{syntax} and \isakeyword{translations}. The
+ present formulation has the virtue that expressions are immediately
+ replaced by its ``definition'' upon parsing; the effect is reversed
+ upon printing. Internally, \isa{{\isasymnoteq}} never appears.
+
+ Simulating definitions via translations is adequate for very basic
+ variations of fundamental logical concepts, when the new
+ representation is a trivial variation on an existing one. On the
+ other hand, syntax translations do not scale up well to large
+ hierarchies of concepts built on each other.%
\end{isamarkuptext}%
\isamarkuptrue%
%
-\isamarkupsection{Document Preparation%
+\isamarkupsection{Document Preparation \label{sec:document-prep}%
}
\isamarkuptrue%
%
@@ -432,9 +465,7 @@
\isamarkuptrue%
%
\begin{isamarkuptext}%
-FIXME \verb,\label, within sections;
-
- The large-scale structure of Isabelle documents closely follows
+The large-scale structure of Isabelle documents closely follows
{\LaTeX} convention, with chapters, sections, subsubsections etc.
The formal Isar language includes separate structure \bfindex{markup
commands}, which do not effect the formal content of a theory (or
@@ -532,7 +563,9 @@
\isamarkuptrue%
%
\begin{isamarkuptext}%
-Comments of the form \verb,(,\verb,*,~\dots~\verb,*,\verb,),%
+Comments of the form \verb,(,\verb,*,~\dots~\verb,*,\verb,),
+
+ FIXME%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -600,8 +633,45 @@
\medskip
- Ignoring portions of printed text like this demands some special
- care. FIXME%
+ Text may be suppressed at a very fine grain; thus we may even drop
+ vital parts of the formal text, preventing that things have been
+ simpler than in reality. For example, the following ``fully
+ automatic'' proof is actually a fake:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{lemma}\ {\isachardoublequote}x\ {\isasymnoteq}\ {\isacharparenleft}{\isadigit{0}}{\isacharcolon}{\isacharcolon}int{\isacharparenright}\ {\isasymLongrightarrow}\ {\isadigit{0}}\ {\isacharless}\ x\ {\isacharasterisk}\ x{\isachardoublequote}\isanewline
+\ \ \isamarkupfalse%
+\isacommand{by}\ {\isacharparenleft}auto{\isacharparenright}\isamarkupfalse%
+%
+\begin{isamarkuptext}%
+\noindent Here the real source of the proof has been as follows:
+
+\begin{verbatim}
+ by (auto(*<*)simp add: int_less_le(*>*))
+\end{verbatim} %(*
+
+ \medskip Ignoring portions of printed text generally demands some
+ care by the user. First of all, the writer is responsible not to
+ obfuscate the underlying formal development in an unduly manner. It
+ is fairly easy to scramble the remaining visible text by referring
+ to questionable formal items (strange definitions, arbitrary axioms
+ etc.) that have been hidden from sight.
+
+ Some minor technical subtleties of the
+ \verb,(,\verb,*,\verb,<,\verb,*,\verb,),~\verb,(,\verb,*,\verb,>,\verb,*,\verb,),
+ elements need to be observed as well, as the system performs little
+ sanity checks here. Arguments of markup commands and formal
+ comments must not be hidden, otherwise presentation fails. Open and
+ close parentheses need to be inserted carefully; it is fairly easy
+ to hide just the wrong parts, especially after rearranging the
+ sources.
+
+ \medskip Authentic reports of formal theories, say as part of a
+ library, should usually refrain from suppressing parts of the text
+ at all. Other users may need the full information for their own
+ derivative work. If a particular formalization works out as too
+ ugly for general public coverage, it is often better to think of a
+ better way in the first place.%
\end{isamarkuptext}%
\isamarkuptrue%
\isamarkupfalse%