--- a/doc-src/TutorialI/Documents/document/Documents.tex Thu Nov 08 13:21:15 2007 +0100
+++ b/doc-src/TutorialI/Documents/document/Documents.tex Thu Nov 08 13:23:04 2007 +0100
@@ -26,13 +26,13 @@
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%
@@ -66,7 +66,7 @@
\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
@@ -149,7 +149,7 @@
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%
@@ -176,7 +176,7 @@
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
@@ -201,21 +201,18 @@
\ \ 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}%
+\isacommand{notation}\isamarkupfalse%
+\ {\isacharparenleft}xsymbols{\isacharparenright}\ xor\ {\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.
+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.
- \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.%
+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%
%
@@ -251,69 +248,64 @@
\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}.
+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}.
- 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}.
+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.
- \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}.%
+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%
-\isanewline
-\ \ sim\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set{\isachardoublequoteclose}\isanewline
-\isanewline
-\isacommand{syntax}\isamarkupfalse%
+\ sim\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set{\isachardoublequoteclose}\isanewline
\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}%
+\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 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}.
+\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.
- \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:%
+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{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}%
+\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{notation}\isamarkupfalse%
+\ {\isacharparenleft}xsymbols{\isacharparenright}\ not{\isacharunderscore}equal\ {\isacharparenleft}\isakeyword{infix}\ {\isachardoublequoteopen}{\isasymnoteq}{\isasymignore}{\isachardoublequoteclose}\ {\isadigit{5}}{\isadigit{0}}{\isacharparenright}%
\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.
+\noindent The notation \isa{{\isasymnoteq}} is introduced separately to restrict it
+to the \emph{xsymbols} mode.
- 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!%
+ 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%
%
@@ -713,6 +705,7 @@
\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) \\