doc-src/TutorialI/Documents/document/Documents.tex

   of \bfindex{mixfix annotations}.  Associated with any kind of
   constant declaration, mixfixes affect both the grammar productions
   for the parser and output templates for the pretty printer.
 
   In full generality, parser and pretty printer configuration is a
-  subtle affair \cite{isabelle-ref}.  Your syntax specifications need
+  subtle affair~\cite{isabelle-ref}.  Your syntax specifications need
   to interact properly with the existing setup of Isabelle/Pure and
   Isabelle/HOL\@.  To avoid creating ambiguities with existing
   elements, it is particularly important to give new syntactic
   constructs the right precedence.
 
-  \medskip Subsequently we introduce a few simple syntax declaration
+  Below we introduce a few simple syntax declaration
   forms that already cover many common situations fairly well.%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
 \isamarkupsubsection{Infix Annotations%

   arguments may be given infix syntax.  For partial applications with
   fewer than two operands, there is a notation using the prefix~\isa{op}.  For instance, \isa{xor} without arguments is represented as
   \isa{op\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}}; together with ordinary function application, this
   turns \isa{xor\ A} into \isa{op\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ A}.
 
-  \medskip The keyword \isakeyword{infixl} seen above specifies an
+  The keyword \isakeyword{infixl} seen above specifies an
   infix operator that is nested to the \emph{left}: in iterated
   applications the more complex expression appears on the left-hand
   side, and \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} means 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}}.  A \emph{non-oriented} declaration via \isakeyword{infix}
   would render \isa{A\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ B\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ C} illegal, but demand explicit

   \medskip
   \noindent is recognized as the term \isa{{\isasymforall}{\isasymalpha}\isactrlisub {\isadigit{1}}{\isachardot}\ {\isasymalpha}\isactrlisub {\isadigit{1}}\ {\isacharequal}\ {\isasymPi}\isactrlisup {\isasymA}} 
   by Isabelle. Note that \isa{{\isasymPi}\isactrlisup {\isasymA}} is a single
   syntactic entity, not an exponentiation.
 
-  \medskip Replacing our previous definition of \isa{xor} by the
+  Replacing our previous definition of \isa{xor} by the
   following specifies an Isabelle symbol for the new operator:%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
 \isadelimML

 \noindent 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 a named entity \verb,\,\verb,<oplus>, by hand; the
   corresponding symbol will be displayed after further input.
 
-  \medskip More flexible is to provide alternative syntax forms
+  More flexible is to provide alternative syntax forms
   through the \bfindex{print mode} concept~\cite{isabelle-ref}.  By
   convention, the mode of ``$xsymbols$'' is enabled whenever
   Proof~General's X-Symbol mode or {\LaTeX} output is active.  Now
   consider the following hybrid declaration of \isa{xor}:%
 \end{isamarkuptext}%

 \isacommand{constdefs}\isamarkupfalse%
 \isanewline
 \ \ xor\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}bool\ {\isasymRightarrow}\ bool\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequoteopen}{\isacharbrackleft}{\isacharplus}{\isacharbrackright}{\isasymignore}{\isachardoublequoteclose}\ {\isadigit{6}}{\isadigit{0}}{\isacharparenright}\isanewline
 \ \ {\isachardoublequoteopen}A\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}{\isasymignore}\ B\ {\isasymequiv}\ {\isacharparenleft}A\ {\isasymand}\ {\isasymnot}\ B{\isacharparenright}\ {\isasymor}\ {\isacharparenleft}{\isasymnot}\ A\ {\isasymand}\ B{\isacharparenright}{\isachardoublequoteclose}\isanewline
 \isanewline
-\isacommand{syntax}\isamarkupfalse%
-\ {\isacharparenleft}xsymbols{\isacharparenright}\isanewline
-\ \ xor\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}bool\ {\isasymRightarrow}\ bool\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequoteopen}{\isasymoplus}{\isasymignore}{\isachardoublequoteclose}\ {\isadigit{6}}{\isadigit{0}}{\isacharparenright}%
-\begin{isamarkuptext}%
-The \commdx{syntax} command introduced here acts like
-  \isakeyword{consts}, but without declaring a logical constant.  The
-  print mode specification of \isakeyword{syntax}, here \isa{{\isacharparenleft}xsymbols{\isacharparenright}}, is optional.  Also note that its type merely serves
-  for syntactic purposes, and is \emph{not} checked for consistency
-  with the real constant.
-
-  \medskip We may now write \isa{A\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ B} or \isa{A\ {\isasymoplus}\ B} in
-  input, while output uses the nicer syntax of $xsymbols$ whenever
-  that print mode is active.  Such an arrangement is particularly
-  useful for interactive development, where users may type ASCII text
-  and see mathematical symbols displayed during proofs.%
+\isacommand{notation}\isamarkupfalse%
+\ {\isacharparenleft}xsymbols{\isacharparenright}\ xor\ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequoteopen}{\isasymoplus}{\isasymignore}{\isachardoublequoteclose}\ {\isadigit{6}}{\isadigit{0}}{\isacharparenright}%
+\begin{isamarkuptext}%
+The \commdx{notation} command associates a mixfix
+annotation with a logical constant.  The print mode specification of
+\isakeyword{syntax}, here \isa{{\isacharparenleft}xsymbols{\isacharparenright}}, is optional.
+
+We may now write \isa{A\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ B} or \isa{A\ {\isasymoplus}\ B} in input, while
+output uses the nicer syntax of $xsymbols$ whenever that print mode is
+active.  Such an arrangement is particularly useful for interactive
+development, where users may type ASCII text and see mathematical
+symbols displayed during proofs.%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
 \isamarkupsubsection{Prefix Annotations%
 }

   Prefix syntax works the same way for \isakeyword{consts} or
   \isakeyword{constdefs}.%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
-\isamarkupsubsection{Syntax Translations \label{sec:syntax-translations}%
+\isamarkupsubsection{Abbreviations \label{sec:abbreviations}%
 }
 \isamarkuptrue%
 %
 \begin{isamarkuptext}%
 Mixfix syntax annotations merely decorate particular constant
-  application forms with concrete syntax, for instance replacing \
-  \isa{xor\ A\ B} by \isa{A\ {\isasymoplus}\ B}.  Occasionally, the
-  relationship between some piece of notation and its internal form is
-  more complicated.  Here we need \bfindex{syntax translations}.
-
-  Using the \isakeyword{syntax}\index{syntax (command)}, command we
-  introduce uninterpreted notational elements.  Then
-  \commdx{translations} relate input forms to complex logical
-  expressions.  This provides a simple mechanism for syntactic macros;
-  even heavier transformations may be written in ML
-  \cite{isabelle-ref}.
-
-  \medskip A typical use of syntax translations is to introduce
-  relational notation for membership in a set of pair, replacing \
-  \isa{{\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}\ {\isasymin}\ sim} by \isa{x\ {\isasymapprox}\ y}.%
+application forms with concrete syntax, for instance replacing
+\isa{xor\ A\ B} by \isa{A\ {\isasymoplus}\ B}.  Occasionally, the relationship
+between some piece of notation and its internal form is more
+complicated.  Here we need \emph{abbreviations}.
+
+Command \commdx{abbreviation} introduces an uninterpreted notational
+constant as an abbreviation for a complex term. Abbreviations are
+unfolded upon parsing and re-introduced upon printing. This provides a
+simple mechanism for syntactic macros.
+
+A typical use of abbreviations is to introduce relational notation for
+membership in a set of pairs, replacing \isa{{\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}\ {\isasymin}\ sim} by
+\isa{x\ {\isasymapprox}\ y}.%
 \end{isamarkuptext}%
 \isamarkuptrue%
 \isacommand{consts}\isamarkupfalse%
+\ sim\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set{\isachardoublequoteclose}\isanewline
 \isanewline
-\ \ sim\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set{\isachardoublequoteclose}\isanewline
+\isacommand{abbreviation}\isamarkupfalse%
+\ sim{\isadigit{2}}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\ \ \ {\isacharparenleft}\isakeyword{infix}\ {\isachardoublequoteopen}{\isasymapprox}{\isachardoublequoteclose}\ {\isadigit{5}}{\isadigit{0}}{\isacharparenright}\isanewline
+\isakeyword{where}\ {\isachardoublequoteopen}x\ {\isasymapprox}\ y\ \ {\isasymequiv}\ \ {\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}\ {\isasymin}\ sim{\isachardoublequoteclose}%
+\begin{isamarkuptext}%
+\noindent The given meta-equality is used as a rewrite rule
+after parsing (replacing \mbox{\isa{x\ {\isasymapprox}\ y}} by \isa{{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isasymin}\ sim}) and before printing (turning \isa{{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isasymin}\ sim} back into
+\mbox{\isa{x\ {\isasymapprox}\ y}}). The name of the dummy constant \isa{sim{\isadigit{2}}}
+does not matter, as long as it is unique.
+
+Another common application of abbreviations 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{abbreviation}\isamarkupfalse%
+\ not{\isacharunderscore}equal\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequoteopen}{\isachartilde}{\isacharequal}{\isasymignore}{\isachardoublequoteclose}\ {\isadigit{5}}{\isadigit{0}}{\isacharparenright}\isanewline
+\isakeyword{where}\ {\isachardoublequoteopen}x\ {\isachartilde}{\isacharequal}{\isasymignore}\ y\ \ {\isasymequiv}\ \ {\isasymnot}\ {\isacharparenleft}x\ {\isacharequal}\ y{\isacharparenright}{\isachardoublequoteclose}\isanewline
 \isanewline
-\isacommand{syntax}\isamarkupfalse%
-\isanewline
-\ \ {\isachardoublequoteopen}{\isacharunderscore}sim{\isachardoublequoteclose}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\ \ \ \ {\isacharparenleft}\isakeyword{infix}\ {\isachardoublequoteopen}{\isasymapprox}{\isachardoublequoteclose}\ {\isadigit{5}}{\isadigit{0}}{\isacharparenright}\isanewline
-\isacommand{translations}\isamarkupfalse%
-\isanewline
-\ \ {\isachardoublequoteopen}x\ {\isasymapprox}\ y{\isachardoublequoteclose}\ {\isasymrightleftharpoons}\ {\isachardoublequoteopen}{\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}\ {\isasymin}\ sim{\isachardoublequoteclose}%
-\begin{isamarkuptext}%
-\noindent Here the name of the dummy constant \isa{{\isacharunderscore}sim} does
-  not matter, as long as it is not used elsewhere.  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}.
-
-  \medskip Another common 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}\isamarkupfalse%
-\ {\isachardoublequoteopen}{\isacharunderscore}not{\isacharunderscore}equal{\isachardoublequoteclose}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequoteopen}{\isasymnoteq}{\isasymignore}{\isachardoublequoteclose}\ {\isadigit{5}}{\isadigit{0}}{\isacharparenright}\isanewline
-\isacommand{translations}\isamarkupfalse%
-\ {\isachardoublequoteopen}x\ {\isasymnoteq}{\isasymignore}\ y{\isachardoublequoteclose}\ {\isasymrightleftharpoons}\ {\isachardoublequoteopen}{\isasymnot}\ {\isacharparenleft}x\ {\isacharequal}\ y{\isacharparenright}{\isachardoublequoteclose}%
-\begin{isamarkuptext}%
-\noindent Normally one would introduce derived concepts like this
-  within the logic, using \isakeyword{consts} + \isakeyword{defs}
-  instead of \isakeyword{syntax} + \isakeyword{translations}.  The
-  present formulation has the virtue that expressions are immediately
-  replaced by the ``definition'' upon parsing; the effect is reversed
-  upon printing.
-
-  This sort of translation is appropriate when the defined concept is
-  a trivial variation on an existing one.  On the other hand, syntax
-  translations do not scale up well to large hierarchies of concepts.
-  Translations do not replace definitions!%
+\isacommand{notation}\isamarkupfalse%
+\ {\isacharparenleft}xsymbols{\isacharparenright}\ not{\isacharunderscore}equal\ {\isacharparenleft}\isakeyword{infix}\ {\isachardoublequoteopen}{\isasymnoteq}{\isasymignore}{\isachardoublequoteclose}\ {\isadigit{5}}{\isadigit{0}}{\isacharparenright}%
+\begin{isamarkuptext}%
+\noindent The notation \isa{{\isasymnoteq}} is introduced separately to restrict it
+to the \emph{xsymbols} mode.
+
+ Abbreviations are appropriate when the defined concept is a
+simple variation on an existing one.  But because of the automatic
+folding and unfolding of abbreviations, they do not scale up well to
+large hierarchies of concepts. Abbreviations do not replace
+definitions.
+
+Abbreviations are a simplified form of the general concept of
+\emph{syntax translations}; even heavier transformations may be
+written in ML \cite{isabelle-ref}.%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
 \isamarkupsection{Document Preparation \label{sec:document-preparation}%
 }

 
   \medskip
 
   \begin{tabular}{ll}
   \texttt{\at}\verb,{typ,~$\tau$\verb,}, & print type $\tau$ \\
+  \texttt{\at}\verb,{const,~$c$\verb,}, & check existence of $c$ and print it \\
   \texttt{\at}\verb,{term,~$t$\verb,}, & print term $t$ \\
   \texttt{\at}\verb,{prop,~$\phi$\verb,}, & print proposition $\phi$ \\
   \texttt{\at}\verb,{prop [display],~$\phi$\verb,}, & print large proposition $\phi$ (with linebreaks) \\
   \texttt{\at}\verb,{prop [source],~$\phi$\verb,}, & check proposition $\phi$, print its input \\
   \texttt{\at}\verb,{thm,~$a$\verb,}, & print fact $a$ \\