1.1 --- a/doc-src/TutorialI/Documents/Documents.thy Sat Jan 05 01:14:46 2002 +0100
1.2 +++ b/doc-src/TutorialI/Documents/Documents.thy Sat Jan 05 01:15:12 2002 +0100
1.3 @@ -81,10 +81,10 @@
1.4 is nested to the \emph{left}: in iterated applications the more
1.5 complex expression appears on the left-hand side: @{term "A [+] B
1.6 [+] C"} stands for @{text "(A [+] B) [+] C"}. Similarly,
1.7 - \isakeyword{infixr} refers to nesting to the \emph{right}, which
1.8 - would turn @{term "A [+] B [+] C"} into @{text "A [+] (B [+] C)"}.
1.9 - In contrast, a \emph{non-oriented} declaration via
1.10 - \isakeyword{infix} would always demand explicit parentheses.
1.11 + \isakeyword{infixr} refers to nesting to the \emph{right}, reading
1.12 + @{term "A [+] B [+] C"} as @{text "A [+] (B [+] C)"}. In contrast,
1.13 + a \emph{non-oriented} declaration via \isakeyword{infix} would
1.14 + always demand explicit parentheses.
1.15
1.16 Many binary operations observe the associative law, so the exact
1.17 grouping does not matter. Nevertheless, formal statements need be
1.18 @@ -101,19 +101,57 @@
1.19 expressions as required. Note that the system would actually print
1.20 the above statement as @{term "A [+] B [+] C = A [+] (B [+] C)"}
1.21 (due to nesting to the left). We have preferred to give the fully
1.22 - parenthesized form in the text for clarity.
1.23 + parenthesized form in the text for clarity. Only in rare situations
1.24 + one may consider to force parentheses by use of non-oriented infix
1.25 + syntax; equality would probably be a typical candidate.
1.26 *}
1.27
1.28 -(*<*)(*FIXME*)
1.29 +
1.30 subsection {* Mathematical symbols \label{sec:thy-present-symbols} *}
1.31
1.32 text {*
1.33 - The limitations of the ASCII character set pose a serious
1.34 - limitations for representing mathematical notation. Even worse
1.35 - many handsome combinations have already been used up by HOL
1.36 - itself. Luckily, Isabelle supports infinitely many \emph{named
1.37 - symbols}. FIXME
1.38 + Concrete syntax based on plain ASCII characters has its inherent
1.39 + limitations. Rich mathematical notation demands a larger repertoire
1.40 + of symbols. Several standards of extended character sets have been
1.41 + proposed over decades, but none has become universally available so
1.42 + far, not even Unicode\index{Unicode}.
1.43
1.44 + Isabelle supports a generic notion of
1.45 + \emph{symbols}\index{symbols|bold} as the smallest entities of
1.46 + source text, without referring to internal encodings. Such
1.47 + ``generalized characters'' may be of one of the following three
1.48 + kinds:
1.49 +
1.50 + \begin{enumerate}
1.51 +
1.52 + \item Traditional 7-bit ASCII characters.
1.53 +
1.54 + \item Named symbols: \verb,\,\verb,<,$ident$\verb,>, (or
1.55 + \verb,\\,\verb,<,$ident$\verb,>,).
1.56 +
1.57 + \item Named control symbols: \verb,\,\verb,<^,$ident$\verb,>, (or
1.58 + \verb,\\,\verb,<^,$ident$\verb,>,).
1.59 +
1.60 + \end{enumerate}
1.61 +
1.62 + Here $ident$ may be any identifier according to the usual Isabelle
1.63 + conventions. This results in an infinite store of symbols, whose
1.64 + interpretation is left to further front-end tools. For example, the
1.65 + \verb,\,\verb,<forall>, symbol of Isabelle is really displayed as
1.66 + $\forall$ --- both by the user-interface of Proof~General + X-Symbol
1.67 + and the Isabelle document processor (see \S\ref{FIXME}).
1.68 +
1.69 + A list of standard Isabelle symbols is given in
1.70 + \cite[appendix~A]{isabelle-sys}. Users may introduce their own
1.71 + interpretation of further symbols by configuring the appropriate
1.72 + front-end tool accordingly, e.g.\ defining appropriate {\LaTeX}
1.73 + macros for document preparation. There are also a few predefined
1.74 + control symbols, such as \verb,\,\verb,<^sub>, and
1.75 + \verb,\,\verb,<^sup>, for sub- and superscript of the subsequent
1.76 + (printable) symbol, respectively.
1.77 +
1.78 + \medskip The following version of our @{text xor} definition uses a
1.79 + standard Isabelle symbol to achieve typographically pleasing output.
1.80 *}
1.81
1.82 (*<*)
1.83 @@ -123,17 +161,79 @@
1.84 constdefs
1.85 xor :: "bool \<Rightarrow> bool \<Rightarrow> bool" (infixl "\<oplus>" 60)
1.86 "A \<oplus> B \<equiv> (A \<and> \<not> B) \<or> (\<not> A \<and> B)"
1.87 -
1.88 (*<*)
1.89 local
1.90 (*>*)
1.91
1.92 +text {*
1.93 + The X-Symbol package within Proof~General provides several input
1.94 + methods to enter @{text \<oplus>} in the text. If all fails one may just
1.95 + type \verb,\,\verb,<oplus>, by hand; the display is adapted
1.96 + immediately after continuing further input.
1.97 +
1.98 + \medskip A slightly more refined scheme is to provide alternative
1.99 + syntax via the \emph{print mode}\index{print mode} concept of
1.100 + Isabelle (see also \cite{isabelle-ref}). By convention, the mode
1.101 + ``$xsymbols$'' is enabled whenever X-Symbol is active. Consider the
1.102 + following hybrid declaration of @{text xor}.
1.103 +*}
1.104 +
1.105 +(*<*)
1.106 +hide const xor
1.107 +ML_setup {* Context.>> (Theory.add_path "2") *}
1.108 +(*>*)
1.109 +constdefs
1.110 + xor :: "bool \<Rightarrow> bool \<Rightarrow> bool" (infixl "[+]\<ignore>" 60)
1.111 + "A [+]\<ignore> B \<equiv> (A \<and> \<not> B) \<or> (\<not> A \<and> B)"
1.112 +
1.113 +syntax (xsymbols)
1.114 + xor :: "bool \<Rightarrow> bool \<Rightarrow> bool" (infixl "\<oplus>\<ignore>" 60)
1.115 +(*<*)
1.116 +local
1.117 +(*>*)
1.118 +
1.119 +text {*
1.120 + Here the \commdx{syntax} command acts like \isakeyword{consts}, but
1.121 + without declaring a logical constant, and with an optional print
1.122 + mode specification. Note that the type declaration given here
1.123 + merely serves for syntactic purposes, and is not checked for
1.124 + consistency with the real constant.
1.125 +
1.126 + \medskip Now we may write either @{text "[+]"} or @{text "\<oplus>"} in
1.127 + input, while output uses the nicer syntax of $xsymbols$, provided
1.128 + that print mode is presently active. This scheme is particularly
1.129 + useful for interactive development, with the user typing plain ASCII
1.130 + text, but gaining improved visual feedback from the system (say in
1.131 + current goal output).
1.132 +
1.133 + \begin{warn}
1.134 + Using alternative syntax declarations easily results in varying
1.135 + versions of input sources. Isabelle provides no systematic way to
1.136 + convert alternative expressions back and forth. Print modes only
1.137 + affect situations where formal entities are pretty printed by the
1.138 + Isabelle process (e.g.\ output of terms and types), but not the
1.139 + original theory text.
1.140 + \end{warn}
1.141 +
1.142 + \medskip The following variant makes the alternative @{text \<oplus>}
1.143 + notation only available for output. Thus we may enforce input
1.144 + sources to refer to plain ASCII only.
1.145 +*}
1.146 +
1.147 +syntax (xsymbols output)
1.148 + xor :: "bool \<Rightarrow> bool \<Rightarrow> bool" (infixl "\<oplus>\<ignore>" 60)
1.149 +
1.150
1.151 subsection {* Prefixes *}
1.152
1.153 text {*
1.154 - Prefix declarations are an even more degenerate form of mixfix
1.155 - annotation, which allow a arbitrary symbolic token to be used for FIXME
1.156 + Prefix syntax annotations\index{prefix annotation|bold} are just a
1.157 + very degenerate of the general mixfix form \cite{isabelle-ref},
1.158 + without any template arguments or priorities --- just some piece of
1.159 + literal syntax.
1.160 +
1.161 + The following example illustrates this idea idea by associating
1.162 + common symbols with the constructors of a currency datatype.
1.163 *}
1.164
1.165 datatype currency =
1.166 @@ -143,16 +243,31 @@
1.167 | Dollar nat ("$")
1.168
1.169 text {*
1.170 - FIXME The predefined Isabelle symbols used above are \verb,\<euro>,,
1.171 - \verb,\<pounds>,, \verb,\<yen>,, and \verb,\<dollar>,.
1.172 + Here the degenerate mixfix annotations on the rightmost column
1.173 + happen to consist of a single Isabelle symbol each:
1.174 + \verb,\,\verb,<euro>,, \verb,\,\verb,<pounds>,,
1.175 + \verb,\,\verb,<yen>,, and \verb,\,$,.
1.176
1.177 - The above syntax annotation makes \verb,\<euro>, stand for the
1.178 - datatype constructor constant @{text Euro}, which happens to be a
1.179 - function @{typ "nat \<Rightarrow> currency"}. Using plain application syntax
1.180 - we may write @{text "Euro 10"} as @{term "\<euro> 10"}. So we already
1.181 - achieve a decent syntactic representation without having to consider
1.182 - arguments and precedences of general mixfix annotations -- prefixes
1.183 - are already sufficient.
1.184 + Recall that a constructor like @{text Euro} actually is a function
1.185 + @{typ "nat \<Rightarrow> currency"}. An expression like @{text "Euro 10"} will
1.186 + be printed as @{term "\<euro> 10"}. Merely the head of the application is
1.187 + subject to our trivial concrete syntax; this form is sufficient to
1.188 + achieve fair conformance to EU~Commission standards of currency
1.189 + notation.
1.190 +
1.191 + \medskip Certainly, the same idea of prefix syntax also works for
1.192 + \isakeyword{consts}, \isakeyword{constdefs} etc. For example, we
1.193 + might introduce a (slightly unrealistic) function to calculate an
1.194 + abstract currency value, by cases on the datatype constructors and
1.195 + fixed exchange rates.
1.196 +*}
1.197 +
1.198 +consts
1.199 + currency :: "currency \<Rightarrow> nat" ("\<currency>")
1.200 +
1.201 +text {*
1.202 + \noindent The funny symbol encountered here is that of
1.203 + \verb,\<currency>,.
1.204 *}
1.205
1.206
1.207 @@ -211,4 +326,3 @@
1.208 (*<*)
1.209 end
1.210 (*>*)
1.211 -(*>*)
2.1 --- a/doc-src/TutorialI/Documents/document/Documents.tex Sat Jan 05 01:14:46 2002 +0100
2.2 +++ b/doc-src/TutorialI/Documents/document/Documents.tex Sat Jan 05 01:15:12 2002 +0100
2.3 @@ -82,10 +82,10 @@
2.4 \medskip The keyword \isakeyword{infixl} specifies an operator that
2.5 is nested to the \emph{left}: in iterated applications the more
2.6 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,
2.7 - \isakeyword{infixr} refers to nesting to the \emph{right}, which
2.8 - 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}}.
2.9 - In contrast, a \emph{non-oriented} declaration via
2.10 - \isakeyword{infix} would always demand explicit parentheses.
2.11 + \isakeyword{infixr} refers to nesting to the \emph{right}, reading
2.12 + \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,
2.13 + a \emph{non-oriented} declaration via \isakeyword{infix} would
2.14 + always demand explicit parentheses.
2.15
2.16 Many binary operations observe the associative law, so the exact
2.17 grouping does not matter. Nevertheless, formal statements need be
2.18 @@ -103,28 +103,234 @@
2.19 expressions as required. Note that the system would actually print
2.20 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}}
2.21 (due to nesting to the left). We have preferred to give the fully
2.22 - parenthesized form in the text for clarity.%
2.23 + parenthesized form in the text for clarity. Only in rare situations
2.24 + one may consider to force parentheses by use of non-oriented infix
2.25 + syntax; equality would probably be a typical candidate.%
2.26 \end{isamarkuptext}%
2.27 \isamarkuptrue%
2.28 +%
2.29 +\isamarkupsubsection{Mathematical symbols \label{sec:thy-present-symbols}%
2.30 +}
2.31 \isamarkuptrue%
2.32 +%
2.33 +\begin{isamarkuptext}%
2.34 +Concrete syntax based on plain ASCII characters has its inherent
2.35 + limitations. Rich mathematical notation demands a larger repertoire
2.36 + of symbols. Several standards of extended character sets have been
2.37 + proposed over decades, but none has become universally available so
2.38 + far, not even Unicode\index{Unicode}.
2.39 +
2.40 + Isabelle supports a generic notion of
2.41 + \emph{symbols}\index{symbols|bold} as the smallest entities of
2.42 + source text, without referring to internal encodings. Such
2.43 + ``generalized characters'' may be of one of the following three
2.44 + kinds:
2.45 +
2.46 + \begin{enumerate}
2.47 +
2.48 + \item Traditional 7-bit ASCII characters.
2.49 +
2.50 + \item Named symbols: \verb,\,\verb,<,$ident$\verb,>, (or
2.51 + \verb,\\,\verb,<,$ident$\verb,>,).
2.52 +
2.53 + \item Named control symbols: \verb,\,\verb,<^,$ident$\verb,>, (or
2.54 + \verb,\\,\verb,<^,$ident$\verb,>,).
2.55 +
2.56 + \end{enumerate}
2.57 +
2.58 + Here $ident$ may be any identifier according to the usual Isabelle
2.59 + conventions. This results in an infinite store of symbols, whose
2.60 + interpretation is left to further front-end tools. For example, the
2.61 + \verb,\,\verb,<forall>, symbol of Isabelle is really displayed as
2.62 + $\forall$ --- both by the user-interface of Proof~General + X-Symbol
2.63 + and the Isabelle document processor (see \S\ref{FIXME}).
2.64 +
2.65 + A list of standard Isabelle symbols is given in
2.66 + \cite[appendix~A]{isabelle-sys}. Users may introduce their own
2.67 + interpretation of further symbols by configuring the appropriate
2.68 + front-end tool accordingly, e.g.\ defining appropriate {\LaTeX}
2.69 + macros for document preparation. There are also a few predefined
2.70 + control symbols, such as \verb,\,\verb,<^sub>, and
2.71 + \verb,\,\verb,<^sup>, for sub- and superscript of the subsequent
2.72 + (printable) symbol, respectively.
2.73 +
2.74 + \medskip The following version of our \isa{xor} definition uses a
2.75 + standard Isabelle symbol to achieve typographically pleasing output.%
2.76 +\end{isamarkuptext}%
2.77 \isamarkuptrue%
2.78 \isamarkupfalse%
2.79 \isamarkupfalse%
2.80 +\isacommand{constdefs}\isanewline
2.81 +\ \ xor\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}bool\ {\isasymRightarrow}\ bool\ {\isasymRightarrow}\ bool{\isachardoublequote}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequote}{\isasymoplus}{\isachardoublequote}\ {\isadigit{6}}{\isadigit{0}}{\isacharparenright}\isanewline
2.82 +\ \ {\isachardoublequote}A\ {\isasymoplus}\ B\ {\isasymequiv}\ {\isacharparenleft}A\ {\isasymand}\ {\isasymnot}\ B{\isacharparenright}\ {\isasymor}\ {\isacharparenleft}{\isasymnot}\ A\ {\isasymand}\ B{\isacharparenright}{\isachardoublequote}\isamarkupfalse%
2.83 \isamarkupfalse%
2.84 -\isamarkupfalse%
2.85 -\isamarkuptrue%
2.86 +%
2.87 +\begin{isamarkuptext}%
2.88 +The X-Symbol package within Proof~General provides several input
2.89 + methods to enter \isa{{\isasymoplus}} in the text. If all fails one may just
2.90 + type \verb,\,\verb,<oplus>, by hand; the display is adapted
2.91 + immediately after continuing further input.
2.92 +
2.93 + \medskip A slightly more refined scheme is to provide alternative
2.94 + syntax via the \emph{print mode}\index{print mode} concept of
2.95 + Isabelle (see also \cite{isabelle-ref}). By convention, the mode
2.96 + ``$xsymbols$'' is enabled whenever X-Symbol is active. Consider the
2.97 + following hybrid declaration of \isa{xor}.%
2.98 +\end{isamarkuptext}%
2.99 \isamarkuptrue%
2.100 \isamarkupfalse%
2.101 +\isamarkupfalse%
2.102 +\isacommand{constdefs}\isanewline
2.103 +\ \ 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
2.104 +\ \ {\isachardoublequote}A\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}{\isasymignore}\ B\ {\isasymequiv}\ {\isacharparenleft}A\ {\isasymand}\ {\isasymnot}\ B{\isacharparenright}\ {\isasymor}\ {\isacharparenleft}{\isasymnot}\ A\ {\isasymand}\ B{\isacharparenright}{\isachardoublequote}\isanewline
2.105 +\isanewline
2.106 +\isamarkupfalse%
2.107 +\isacommand{syntax}\ {\isacharparenleft}xsymbols{\isacharparenright}\isanewline
2.108 +\ \ xor\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}bool\ {\isasymRightarrow}\ bool\ {\isasymRightarrow}\ bool{\isachardoublequote}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequote}{\isasymoplus}{\isasymignore}{\isachardoublequote}\ {\isadigit{6}}{\isadigit{0}}{\isacharparenright}\isamarkupfalse%
2.109 +\isamarkupfalse%
2.110 +%
2.111 +\begin{isamarkuptext}%
2.112 +Here the \commdx{syntax} command acts like \isakeyword{consts}, but
2.113 + without declaring a logical constant, and with an optional print
2.114 + mode specification. Note that the type declaration given here
2.115 + merely serves for syntactic purposes, and is not checked for
2.116 + consistency with the real constant.
2.117 +
2.118 + \medskip Now we may write either \isa{{\isacharbrackleft}{\isacharplus}{\isacharbrackright}} or \isa{{\isasymoplus}} in
2.119 + input, while output uses the nicer syntax of $xsymbols$, provided
2.120 + that print mode is presently active. This scheme is particularly
2.121 + useful for interactive development, with the user typing plain ASCII
2.122 + text, but gaining improved visual feedback from the system (say in
2.123 + current goal output).
2.124 +
2.125 + \begin{warn}
2.126 + Using alternative syntax declarations easily results in varying
2.127 + versions of input sources. Isabelle provides no systematic way to
2.128 + convert alternative expressions back and forth. Print modes only
2.129 + affect situations where formal entities are pretty printed by the
2.130 + Isabelle process (e.g.\ output of terms and types), but not the
2.131 + original theory text.
2.132 + \end{warn}
2.133 +
2.134 + \medskip The following variant makes the alternative \isa{{\isasymoplus}}
2.135 + notation only available for output. Thus we may enforce input
2.136 + sources to refer to plain ASCII only.%
2.137 +\end{isamarkuptext}%
2.138 \isamarkuptrue%
2.139 +\isacommand{syntax}\ {\isacharparenleft}xsymbols\ \isakeyword{output}{\isacharparenright}\isanewline
2.140 +\ \ xor\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}bool\ {\isasymRightarrow}\ bool\ {\isasymRightarrow}\ bool{\isachardoublequote}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequote}{\isasymoplus}{\isasymignore}{\isachardoublequote}\ {\isadigit{6}}{\isadigit{0}}{\isacharparenright}\isamarkupfalse%
2.141 +%
2.142 +\isamarkupsubsection{Prefixes%
2.143 +}
2.144 \isamarkuptrue%
2.145 +%
2.146 +\begin{isamarkuptext}%
2.147 +Prefix syntax annotations\index{prefix annotation|bold} are just a
2.148 + very degenerate of the general mixfix form \cite{isabelle-ref},
2.149 + without any template arguments or priorities --- just some piece of
2.150 + literal syntax.
2.151 +
2.152 + The following example illustrates this idea idea by associating
2.153 + common symbols with the constructors of a currency datatype.%
2.154 +\end{isamarkuptext}%
2.155 \isamarkuptrue%
2.156 -\isamarkupfalse%
2.157 +\isacommand{datatype}\ currency\ {\isacharequal}\isanewline
2.158 +\ \ \ \ Euro\ nat\ \ \ \ {\isacharparenleft}{\isachardoublequote}{\isasymeuro}{\isachardoublequote}{\isacharparenright}\isanewline
2.159 +\ \ {\isacharbar}\ Pounds\ nat\ \ {\isacharparenleft}{\isachardoublequote}{\isasympounds}{\isachardoublequote}{\isacharparenright}\isanewline
2.160 +\ \ {\isacharbar}\ Yen\ nat\ \ \ \ \ {\isacharparenleft}{\isachardoublequote}{\isasymyen}{\isachardoublequote}{\isacharparenright}\isanewline
2.161 +\ \ {\isacharbar}\ Dollar\ nat\ \ {\isacharparenleft}{\isachardoublequote}{\isachardollar}{\isachardoublequote}{\isacharparenright}\isamarkupfalse%
2.162 +%
2.163 +\begin{isamarkuptext}%
2.164 +Here the degenerate mixfix annotations on the rightmost column
2.165 + happen to consist of a single Isabelle symbol each:
2.166 + \verb,\,\verb,<euro>,, \verb,\,\verb,<pounds>,,
2.167 + \verb,\,\verb,<yen>,, and \verb,\,\verb,<dollar>,.
2.168 +
2.169 + Recall that a constructor like \isa{Euro} actually is a function
2.170 + \isa{nat\ {\isasymRightarrow}\ currency}. An expression like \isa{Euro\ {\isadigit{1}}{\isadigit{0}}} will
2.171 + be printed as \isa{{\isasymeuro}\ {\isadigit{1}}{\isadigit{0}}}. Merely the head of the application is
2.172 + subject to our trivial concrete syntax; this form is sufficient to
2.173 + achieve fair conformance to EU~Commission standards of currency
2.174 + notation.
2.175 +
2.176 + \medskip Certainly, the same idea of prefix syntax also works for
2.177 + \isakeyword{consts}, \isakeyword{constdefs} etc. For example, we
2.178 + might introduce a (slightly unrealistic) function to calculate an
2.179 + abstract currency value, by cases on the datatype constructors and
2.180 + fixed exchange rates.%
2.181 +\end{isamarkuptext}%
2.182 \isamarkuptrue%
2.183 +\isacommand{consts}\isanewline
2.184 +\ \ currency\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}currency\ {\isasymRightarrow}\ nat{\isachardoublequote}\ \ \ \ {\isacharparenleft}{\isachardoublequote}{\isasymcurrency}{\isachardoublequote}{\isacharparenright}\isamarkupfalse%
2.185 +%
2.186 +\begin{isamarkuptext}%
2.187 +\noindent The funny symbol encountered here is that of
2.188 + \verb,\<currency>,.%
2.189 +\end{isamarkuptext}%
2.190 \isamarkuptrue%
2.191 +%
2.192 +\isamarkupsubsection{Syntax translations \label{sec:def-translations}%
2.193 +}
2.194 \isamarkuptrue%
2.195 +%
2.196 +\begin{isamarkuptext}%
2.197 +FIXME
2.198 +
2.199 +\index{syntax translations|(}%
2.200 +\index{translations@\isacommand {translations} (command)|(}
2.201 +Isabelle offers an additional definitional facility,
2.202 +\textbf{syntax translations}.
2.203 +They resemble macros: upon parsing, the defined concept is immediately
2.204 +replaced by its definition. This effect is reversed upon printing. For example,
2.205 +the symbol \isa{{\isasymnoteq}} is defined via a syntax translation:%
2.206 +\end{isamarkuptext}%
2.207 \isamarkuptrue%
2.208 +\isacommand{translations}\ {\isachardoublequote}x\ {\isasymnoteq}\ y{\isachardoublequote}\ {\isasymrightleftharpoons}\ {\isachardoublequote}{\isasymnot}{\isacharparenleft}x\ {\isacharequal}\ y{\isacharparenright}{\isachardoublequote}\isamarkupfalse%
2.209 +%
2.210 +\begin{isamarkuptext}%
2.211 +\index{$IsaEqTrans@\isasymrightleftharpoons}
2.212 +\noindent
2.213 +Internally, \isa{{\isasymnoteq}} never appears.
2.214 +
2.215 +In addition to \isa{{\isasymrightleftharpoons}} there are
2.216 +\isa{{\isasymrightharpoonup}}\index{$IsaEqTrans1@\isasymrightharpoonup}
2.217 +and \isa{{\isasymleftharpoondown}}\index{$IsaEqTrans2@\isasymleftharpoondown}
2.218 +for uni-directional translations, which only affect
2.219 +parsing or printing. This tutorial will not cover the details of
2.220 +translations. We have mentioned the concept merely because it
2.221 +crops up occasionally; a number of HOL's built-in constructs are defined
2.222 +via translations. Translations are preferable to definitions when the new
2.223 +concept is a trivial variation on an existing one. For example, we
2.224 +don't need to derive new theorems about \isa{{\isasymnoteq}}, since existing theorems
2.225 +about \isa{{\isacharequal}} still apply.%
2.226 +\index{syntax translations|)}%
2.227 +\index{translations@\isacommand {translations} (command)|)}%
2.228 +\end{isamarkuptext}%
2.229 \isamarkuptrue%
2.230 +%
2.231 +\isamarkupsection{Document preparation%
2.232 +}
2.233 \isamarkuptrue%
2.234 +%
2.235 +\isamarkupsubsection{Batch-mode sessions%
2.236 +}
2.237 +\isamarkuptrue%
2.238 +%
2.239 +\isamarkupsubsection{{\LaTeX} macros%
2.240 +}
2.241 +\isamarkuptrue%
2.242 +%
2.243 +\isamarkupsubsubsection{Structure markup%
2.244 +}
2.245 +\isamarkuptrue%
2.246 +%
2.247 +\isamarkupsubsubsection{Symbols and characters%
2.248 +}
2.249 +\isamarkuptrue%
2.250 +%
2.251 +\begin{isamarkuptext}%
2.252 +FIXME%
2.253 +\end{isamarkuptext}%
2.254 \isamarkuptrue%
2.255 \isamarkupfalse%
2.256 \end{isabellebody}%
3.1 --- a/doc-src/TutorialI/Documents/documents.tex Sat Jan 05 01:14:46 2002 +0100
3.2 +++ b/doc-src/TutorialI/Documents/documents.tex Sat Jan 05 01:15:12 2002 +0100
3.3 @@ -2,19 +2,23 @@
3.4 \chapter{Presenting theories}
3.5 \label{ch:thy-present}
3.6
3.7 -Due to the previous chapters the reader should have become sufficiently
3.8 -acquainted with basic formal theory development in Isabelle/HOL, so that we
3.9 -may now set out on a small interlude concerning the ``marginal'' issue of
3.10 -presenting theories in a typographically pleasing manner. Isabelle provides a
3.11 -rich infrastructure for concrete syntax (for input and output of the logical
3.12 -term language of $\lambda$-calculus), as well as document preparation of
3.13 -collections of theory texts using existing {\LaTeX} infrastructure.
3.14 +Now that the reader has become sufficiently acquainted with basic formal
3.15 +theory development in Isabelle/HOL, the subsequent interlude covers the
3.16 +``marginal'' issue of presenting theories in a typographically pleasing
3.17 +manner. Isabelle provides a rich infrastructure for concrete syntax (input
3.18 +and output of the $\lambda$-calculus term language), as well as document
3.19 +preparation of theory texts using existing PDF-{\LaTeX} technology.
3.20
3.21 -The overall measure of theory beautification depends on the kind of
3.22 -application one has in mind, as well as the intended audience of the final
3.23 -results. In any case, users may already benefit themselves from handsome
3.24 -notation available in interactive development, while requiring only minimal
3.25 -provisions as part of the theory specifications.
3.26 +The measure of theory beautification depends on the kind of application one
3.27 +has in mind, and the intended audience of the final results. In any case,
3.28 +users may already benefit themselves from handsome notation available in
3.29 +interactive development. Only minimal provisions in theory specifications may
3.30 +already change the general appearance of formal entities in a significant way.
3.31 +
3.32 +As has been pointed out by Leibniz\index{Leibniz, Gottfried Wilhelm} more than
3.33 +300 years ago, \emph{notions} are in principle more important than
3.34 +\emph{notations}, but fair textual representation of ideas is very important
3.35 +to reduce the mental effort in actual applications.
3.36
3.37 \input{Documents/document/Documents.tex}
3.38