# HG changeset patch
# User wenzelm
# Date 1010332231 -3600
# Node ID 6e17f2ae9e1624b7db87268621abd1d44cb9784a
# Parent  16d4b8c09086e720e53f7142c089c3631e3d2d10
updated;

diff -r 16d4b8c09086 -r 6e17f2ae9e16 doc-src/TutorialI/Documents/document/Documents.tex
--- 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%
diff -r 16d4b8c09086 -r 6e17f2ae9e16 doc-src/TutorialI/Sets/sets.tex
--- a/doc-src/TutorialI/Sets/sets.tex	Sun Jan 06 13:48:18 2002 +0100
+++ b/doc-src/TutorialI/Sets/sets.tex	Sun Jan 06 16:50:31 2002 +0100
@@ -324,7 +324,7 @@
 \rulenamedx{UN_E}
 \end{isabelle}
 %
-The following built-in syntax translation (see {\S}\ref{sec:def-translations})
+The following built-in syntax translation (see {\S}\ref{sec:syntax-translations})
 lets us express the union over a \emph{type}:
 \begin{isabelle}
 \ \ \ \ \