101 \begin{isamarkuptext}% |
101 \begin{isamarkuptext}% |
102 Such rules may be used in simplification to regroup nested |
102 Such rules may be used in simplification to regroup nested |
103 expressions as required. Note that the system would actually print |
103 expressions as required. Note that the system would actually print |
104 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}} |
104 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}} |
105 (due to nesting to the left). We have preferred to give the fully |
105 (due to nesting to the left). We have preferred to give the fully |
106 parenthesized form in the text for clarity.% |
106 parenthesized form in the text for clarity. Only in rare situations |
107 \end{isamarkuptext}% |
107 one may consider to force parentheses by use of non-oriented infix |
108 \isamarkuptrue% |
108 syntax; equality would probably be a typical candidate.% |
109 \isamarkuptrue% |
109 \end{isamarkuptext}% |
110 \isamarkuptrue% |
110 \isamarkuptrue% |
111 \isamarkupfalse% |
111 % |
112 \isamarkupfalse% |
112 \isamarkupsubsection{Mathematical symbols \label{sec:thy-present-symbols}% |
113 \isamarkupfalse% |
113 } |
114 \isamarkupfalse% |
114 \isamarkuptrue% |
115 \isamarkuptrue% |
115 % |
116 \isamarkuptrue% |
116 \begin{isamarkuptext}% |
117 \isamarkupfalse% |
117 Concrete syntax based on plain ASCII characters has its inherent |
118 \isamarkuptrue% |
118 limitations. Rich mathematical notation demands a larger repertoire |
119 \isamarkuptrue% |
119 of symbols. Several standards of extended character sets have been |
120 \isamarkuptrue% |
120 proposed over decades, but none has become universally available so |
121 \isamarkupfalse% |
121 far, not even Unicode\index{Unicode}. |
122 \isamarkuptrue% |
122 |
123 \isamarkuptrue% |
123 Isabelle supports a generic notion of |
124 \isamarkuptrue% |
124 \emph{symbols}\index{symbols|bold} as the smallest entities of |
125 \isamarkuptrue% |
125 source text, without referring to internal encodings. Such |
126 \isamarkuptrue% |
126 ``generalized characters'' may be of one of the following three |
127 \isamarkuptrue% |
127 kinds: |
|
128 |
|
129 \begin{enumerate} |
|
130 |
|
131 \item Traditional 7-bit ASCII characters. |
|
132 |
|
133 \item Named symbols: \verb,\,\verb,<,$ident$\verb,>, (or |
|
134 \verb,\\,\verb,<,$ident$\verb,>,). |
|
135 |
|
136 \item Named control symbols: \verb,\,\verb,<^,$ident$\verb,>, (or |
|
137 \verb,\\,\verb,<^,$ident$\verb,>,). |
|
138 |
|
139 \end{enumerate} |
|
140 |
|
141 Here $ident$ may be any identifier according to the usual Isabelle |
|
142 conventions. This results in an infinite store of symbols, whose |
|
143 interpretation is left to further front-end tools. For example, the |
|
144 \verb,\,\verb,<forall>, symbol of Isabelle is really displayed as |
|
145 $\forall$ --- both by the user-interface of Proof~General + X-Symbol |
|
146 and the Isabelle document processor (see \S\ref{FIXME}). |
|
147 |
|
148 A list of standard Isabelle symbols is given in |
|
149 \cite[appendix~A]{isabelle-sys}. Users may introduce their own |
|
150 interpretation of further symbols by configuring the appropriate |
|
151 front-end tool accordingly, e.g.\ defining appropriate {\LaTeX} |
|
152 macros for document preparation. There are also a few predefined |
|
153 control symbols, such as \verb,\,\verb,<^sub>, and |
|
154 \verb,\,\verb,<^sup>, for sub- and superscript of the subsequent |
|
155 (printable) symbol, respectively. |
|
156 |
|
157 \medskip The following version of our \isa{xor} definition uses a |
|
158 standard Isabelle symbol to achieve typographically pleasing output.% |
|
159 \end{isamarkuptext}% |
|
160 \isamarkuptrue% |
|
161 \isamarkupfalse% |
|
162 \isamarkupfalse% |
|
163 \isacommand{constdefs}\isanewline |
|
164 \ \ xor\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}bool\ {\isasymRightarrow}\ bool\ {\isasymRightarrow}\ bool{\isachardoublequote}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequote}{\isasymoplus}{\isachardoublequote}\ {\isadigit{6}}{\isadigit{0}}{\isacharparenright}\isanewline |
|
165 \ \ {\isachardoublequote}A\ {\isasymoplus}\ B\ {\isasymequiv}\ {\isacharparenleft}A\ {\isasymand}\ {\isasymnot}\ B{\isacharparenright}\ {\isasymor}\ {\isacharparenleft}{\isasymnot}\ A\ {\isasymand}\ B{\isacharparenright}{\isachardoublequote}\isamarkupfalse% |
|
166 \isamarkupfalse% |
|
167 % |
|
168 \begin{isamarkuptext}% |
|
169 The X-Symbol package within Proof~General provides several input |
|
170 methods to enter \isa{{\isasymoplus}} in the text. If all fails one may just |
|
171 type \verb,\,\verb,<oplus>, by hand; the display is adapted |
|
172 immediately after continuing further input. |
|
173 |
|
174 \medskip A slightly more refined scheme is to provide alternative |
|
175 syntax via the \emph{print mode}\index{print mode} concept of |
|
176 Isabelle (see also \cite{isabelle-ref}). By convention, the mode |
|
177 ``$xsymbols$'' is enabled whenever X-Symbol is active. Consider the |
|
178 following hybrid declaration of \isa{xor}.% |
|
179 \end{isamarkuptext}% |
|
180 \isamarkuptrue% |
|
181 \isamarkupfalse% |
|
182 \isamarkupfalse% |
|
183 \isacommand{constdefs}\isanewline |
|
184 \ \ 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 |
|
185 \ \ {\isachardoublequote}A\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}{\isasymignore}\ B\ {\isasymequiv}\ {\isacharparenleft}A\ {\isasymand}\ {\isasymnot}\ B{\isacharparenright}\ {\isasymor}\ {\isacharparenleft}{\isasymnot}\ A\ {\isasymand}\ B{\isacharparenright}{\isachardoublequote}\isanewline |
|
186 \isanewline |
|
187 \isamarkupfalse% |
|
188 \isacommand{syntax}\ {\isacharparenleft}xsymbols{\isacharparenright}\isanewline |
|
189 \ \ xor\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}bool\ {\isasymRightarrow}\ bool\ {\isasymRightarrow}\ bool{\isachardoublequote}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequote}{\isasymoplus}{\isasymignore}{\isachardoublequote}\ {\isadigit{6}}{\isadigit{0}}{\isacharparenright}\isamarkupfalse% |
|
190 \isamarkupfalse% |
|
191 % |
|
192 \begin{isamarkuptext}% |
|
193 Here the \commdx{syntax} command acts like \isakeyword{consts}, but |
|
194 without declaring a logical constant, and with an optional print |
|
195 mode specification. Note that the type declaration given here |
|
196 merely serves for syntactic purposes, and is not checked for |
|
197 consistency with the real constant. |
|
198 |
|
199 \medskip Now we may write either \isa{{\isacharbrackleft}{\isacharplus}{\isacharbrackright}} or \isa{{\isasymoplus}} in |
|
200 input, while output uses the nicer syntax of $xsymbols$, provided |
|
201 that print mode is presently active. This scheme is particularly |
|
202 useful for interactive development, with the user typing plain ASCII |
|
203 text, but gaining improved visual feedback from the system (say in |
|
204 current goal output). |
|
205 |
|
206 \begin{warn} |
|
207 Using alternative syntax declarations easily results in varying |
|
208 versions of input sources. Isabelle provides no systematic way to |
|
209 convert alternative expressions back and forth. Print modes only |
|
210 affect situations where formal entities are pretty printed by the |
|
211 Isabelle process (e.g.\ output of terms and types), but not the |
|
212 original theory text. |
|
213 \end{warn} |
|
214 |
|
215 \medskip The following variant makes the alternative \isa{{\isasymoplus}} |
|
216 notation only available for output. Thus we may enforce input |
|
217 sources to refer to plain ASCII only.% |
|
218 \end{isamarkuptext}% |
|
219 \isamarkuptrue% |
|
220 \isacommand{syntax}\ {\isacharparenleft}xsymbols\ \isakeyword{output}{\isacharparenright}\isanewline |
|
221 \ \ xor\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}bool\ {\isasymRightarrow}\ bool\ {\isasymRightarrow}\ bool{\isachardoublequote}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequote}{\isasymoplus}{\isasymignore}{\isachardoublequote}\ {\isadigit{6}}{\isadigit{0}}{\isacharparenright}\isamarkupfalse% |
|
222 % |
|
223 \isamarkupsubsection{Prefixes% |
|
224 } |
|
225 \isamarkuptrue% |
|
226 % |
|
227 \begin{isamarkuptext}% |
|
228 Prefix syntax annotations\index{prefix annotation|bold} are just a |
|
229 very degenerate of the general mixfix form \cite{isabelle-ref}, |
|
230 without any template arguments or priorities --- just some piece of |
|
231 literal syntax. |
|
232 |
|
233 The following example illustrates this idea idea by associating |
|
234 common symbols with the constructors of a currency datatype.% |
|
235 \end{isamarkuptext}% |
|
236 \isamarkuptrue% |
|
237 \isacommand{datatype}\ currency\ {\isacharequal}\isanewline |
|
238 \ \ \ \ Euro\ nat\ \ \ \ {\isacharparenleft}{\isachardoublequote}{\isasymeuro}{\isachardoublequote}{\isacharparenright}\isanewline |
|
239 \ \ {\isacharbar}\ Pounds\ nat\ \ {\isacharparenleft}{\isachardoublequote}{\isasympounds}{\isachardoublequote}{\isacharparenright}\isanewline |
|
240 \ \ {\isacharbar}\ Yen\ nat\ \ \ \ \ {\isacharparenleft}{\isachardoublequote}{\isasymyen}{\isachardoublequote}{\isacharparenright}\isanewline |
|
241 \ \ {\isacharbar}\ Dollar\ nat\ \ {\isacharparenleft}{\isachardoublequote}{\isachardollar}{\isachardoublequote}{\isacharparenright}\isamarkupfalse% |
|
242 % |
|
243 \begin{isamarkuptext}% |
|
244 Here the degenerate mixfix annotations on the rightmost column |
|
245 happen to consist of a single Isabelle symbol each: |
|
246 \verb,\,\verb,<euro>,, \verb,\,\verb,<pounds>,, |
|
247 \verb,\,\verb,<yen>,, and \verb,\,\verb,<dollar>,. |
|
248 |
|
249 Recall that a constructor like \isa{Euro} actually is a function |
|
250 \isa{nat\ {\isasymRightarrow}\ currency}. An expression like \isa{Euro\ {\isadigit{1}}{\isadigit{0}}} will |
|
251 be printed as \isa{{\isasymeuro}\ {\isadigit{1}}{\isadigit{0}}}. Merely the head of the application is |
|
252 subject to our trivial concrete syntax; this form is sufficient to |
|
253 achieve fair conformance to EU~Commission standards of currency |
|
254 notation. |
|
255 |
|
256 \medskip Certainly, the same idea of prefix syntax also works for |
|
257 \isakeyword{consts}, \isakeyword{constdefs} etc. For example, we |
|
258 might introduce a (slightly unrealistic) function to calculate an |
|
259 abstract currency value, by cases on the datatype constructors and |
|
260 fixed exchange rates.% |
|
261 \end{isamarkuptext}% |
|
262 \isamarkuptrue% |
|
263 \isacommand{consts}\isanewline |
|
264 \ \ currency\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}currency\ {\isasymRightarrow}\ nat{\isachardoublequote}\ \ \ \ {\isacharparenleft}{\isachardoublequote}{\isasymcurrency}{\isachardoublequote}{\isacharparenright}\isamarkupfalse% |
|
265 % |
|
266 \begin{isamarkuptext}% |
|
267 \noindent The funny symbol encountered here is that of |
|
268 \verb,\<currency>,.% |
|
269 \end{isamarkuptext}% |
|
270 \isamarkuptrue% |
|
271 % |
|
272 \isamarkupsubsection{Syntax translations \label{sec:def-translations}% |
|
273 } |
|
274 \isamarkuptrue% |
|
275 % |
|
276 \begin{isamarkuptext}% |
|
277 FIXME |
|
278 |
|
279 \index{syntax translations|(}% |
|
280 \index{translations@\isacommand {translations} (command)|(} |
|
281 Isabelle offers an additional definitional facility, |
|
282 \textbf{syntax translations}. |
|
283 They resemble macros: upon parsing, the defined concept is immediately |
|
284 replaced by its definition. This effect is reversed upon printing. For example, |
|
285 the symbol \isa{{\isasymnoteq}} is defined via a syntax translation:% |
|
286 \end{isamarkuptext}% |
|
287 \isamarkuptrue% |
|
288 \isacommand{translations}\ {\isachardoublequote}x\ {\isasymnoteq}\ y{\isachardoublequote}\ {\isasymrightleftharpoons}\ {\isachardoublequote}{\isasymnot}{\isacharparenleft}x\ {\isacharequal}\ y{\isacharparenright}{\isachardoublequote}\isamarkupfalse% |
|
289 % |
|
290 \begin{isamarkuptext}% |
|
291 \index{$IsaEqTrans@\isasymrightleftharpoons} |
|
292 \noindent |
|
293 Internally, \isa{{\isasymnoteq}} never appears. |
|
294 |
|
295 In addition to \isa{{\isasymrightleftharpoons}} there are |
|
296 \isa{{\isasymrightharpoonup}}\index{$IsaEqTrans1@\isasymrightharpoonup} |
|
297 and \isa{{\isasymleftharpoondown}}\index{$IsaEqTrans2@\isasymleftharpoondown} |
|
298 for uni-directional translations, which only affect |
|
299 parsing or printing. This tutorial will not cover the details of |
|
300 translations. We have mentioned the concept merely because it |
|
301 crops up occasionally; a number of HOL's built-in constructs are defined |
|
302 via translations. Translations are preferable to definitions when the new |
|
303 concept is a trivial variation on an existing one. For example, we |
|
304 don't need to derive new theorems about \isa{{\isasymnoteq}}, since existing theorems |
|
305 about \isa{{\isacharequal}} still apply.% |
|
306 \index{syntax translations|)}% |
|
307 \index{translations@\isacommand {translations} (command)|)}% |
|
308 \end{isamarkuptext}% |
|
309 \isamarkuptrue% |
|
310 % |
|
311 \isamarkupsection{Document preparation% |
|
312 } |
|
313 \isamarkuptrue% |
|
314 % |
|
315 \isamarkupsubsection{Batch-mode sessions% |
|
316 } |
|
317 \isamarkuptrue% |
|
318 % |
|
319 \isamarkupsubsection{{\LaTeX} macros% |
|
320 } |
|
321 \isamarkuptrue% |
|
322 % |
|
323 \isamarkupsubsubsection{Structure markup% |
|
324 } |
|
325 \isamarkuptrue% |
|
326 % |
|
327 \isamarkupsubsubsection{Symbols and characters% |
|
328 } |
|
329 \isamarkuptrue% |
|
330 % |
|
331 \begin{isamarkuptext}% |
|
332 FIXME% |
|
333 \end{isamarkuptext}% |
128 \isamarkuptrue% |
334 \isamarkuptrue% |
129 \isamarkupfalse% |
335 \isamarkupfalse% |
130 \end{isabellebody}% |
336 \end{isabellebody}% |
131 %%% Local Variables: |
337 %%% Local Variables: |
132 %%% mode: latex |
338 %%% mode: latex |