changeset 12666 | 9842befead7a |
parent 12658 | 3939e7dea202 |
child 12671 | bb6db6c0d4df |
12665:61e53dbac238 | 12666:9842befead7a |
---|---|
13 \bfindex{mixfix annotations}. Associated with any kind of constant |
13 \bfindex{mixfix annotations}. Associated with any kind of constant |
14 declaration, mixfixes affect both the grammar productions for the |
14 declaration, mixfixes affect both the grammar productions for the |
15 parser and output templates for the pretty printer. |
15 parser and output templates for the pretty printer. |
16 |
16 |
17 In full generality, the whole affair of parser and pretty printer |
17 In full generality, the whole affair of parser and pretty printer |
18 configuration is rather subtle, see \cite{isabelle-ref} for further |
18 configuration is rather subtle, see also \cite{isabelle-ref}. Any |
19 details. Any syntax specifications given by end-users need to |
19 syntax specifications given by end-users need to interact properly |
20 interact properly with the existing setup of Isabelle/Pure and |
20 with the existing setup of Isabelle/Pure and Isabelle/HOL. It is |
21 Isabelle/HOL. It is particularly important to get the precedence of |
21 particularly important to get the precedence of new syntactic |
22 new syntactic constructs right, avoiding ambiguities with existing |
22 constructs right, avoiding ambiguities with existing elements. |
23 elements. |
|
24 |
23 |
25 \medskip Subsequently we introduce a few simple declaration forms |
24 \medskip Subsequently we introduce a few simple declaration forms |
26 that already cover the most common situations fairly well.% |
25 that already cover the most common situations fairly well.% |
27 \end{isamarkuptext}% |
26 \end{isamarkuptext}% |
28 \isamarkuptrue% |
27 \isamarkuptrue% |
39 well, although this is less frequently encountered in practice |
38 well, although this is less frequently encountered in practice |
40 (\isa{{\isacharasterisk}} and \isa{{\isacharplus}} types may come to mind). |
39 (\isa{{\isacharasterisk}} and \isa{{\isacharplus}} types may come to mind). |
41 |
40 |
42 Infix declarations\index{infix annotations} provide a useful special |
41 Infix declarations\index{infix annotations} provide a useful special |
43 case of mixfixes, where users need not care about the full details |
42 case of mixfixes, where users need not care about the full details |
44 of priorities, nesting, spacing, etc. The subsequent example of the |
43 of priorities, nesting, spacing, etc. The following example of the |
45 exclusive-or operation on boolean values illustrates typical infix |
44 exclusive-or operation on boolean values illustrates typical infix |
46 declarations arising in practice.% |
45 declarations arising in practice.% |
47 \end{isamarkuptext}% |
46 \end{isamarkuptext}% |
48 \isamarkuptrue% |
47 \isamarkuptrue% |
49 \isacommand{constdefs}\isanewline |
48 \isacommand{constdefs}\isanewline |
77 basically reserved for the meta-logic. Syntax of Isabelle/HOL |
76 basically reserved for the meta-logic. Syntax of Isabelle/HOL |
78 mainly uses the range of 10--100: the equality infix \isa{{\isacharequal}} is |
77 mainly uses the range of 10--100: the equality infix \isa{{\isacharequal}} is |
79 centered at 50, logical connectives (like \isa{{\isasymor}} and \isa{{\isasymand}}) are below 50, and algebraic ones (like \isa{{\isacharplus}} and \isa{{\isacharasterisk}}) above 50. User syntax should strive to coexist with common |
78 centered at 50, logical connectives (like \isa{{\isasymor}} and \isa{{\isasymand}}) are below 50, and algebraic ones (like \isa{{\isacharplus}} and \isa{{\isacharasterisk}}) above 50. User syntax should strive to coexist with common |
80 HOL forms, or use the mostly unused range 100--900. |
79 HOL forms, or use the mostly unused range 100--900. |
81 |
80 |
82 \medskip The keyword \isakeyword{infixl} specifies an operator that |
81 The keyword \isakeyword{infixl} specifies an operator that is nested |
83 is nested to the \emph{left}: in iterated applications the more |
82 to the \emph{left}: in iterated applications the more complex |
84 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, |
83 expression appears on the left-hand side: \isa{A\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ B\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ C} |
84 stands for \isa{{\isacharparenleft}A\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ B{\isacharparenright}\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ C}. Similarly, |
|
85 \isakeyword{infixr} specifies to nesting to the \emph{right}, |
85 \isakeyword{infixr} specifies to nesting to the \emph{right}, |
86 reading \isa{A\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ B\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ C} as \isa{A\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ {\isacharparenleft}B\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ C{\isacharparenright}}. In |
86 reading \isa{A\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ B\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ C} as \isa{A\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ {\isacharparenleft}B\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ C{\isacharparenright}}. In |
87 contrast, a \emph{non-oriented} declaration via \isakeyword{infix} |
87 contrast, a \emph{non-oriented} declaration via \isakeyword{infix} |
88 would have rendered \isa{A\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ B\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ C} illegal, but demand |
88 would have rendered \isa{A\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ B\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ C} illegal, but demand |
89 explicit parentheses about the intended grouping.% |
89 explicit parentheses about the intended grouping.% |
97 \begin{isamarkuptext}% |
97 \begin{isamarkuptext}% |
98 Concrete syntax based on plain ASCII characters has its inherent |
98 Concrete syntax based on plain ASCII characters has its inherent |
99 limitations. Rich mathematical notation demands a larger repertoire |
99 limitations. Rich mathematical notation demands a larger repertoire |
100 of symbols. Several standards of extended character sets have been |
100 of symbols. Several standards of extended character sets have been |
101 proposed over decades, but none has become universally available so |
101 proposed over decades, but none has become universally available so |
102 far, not even Unicode\index{Unicode}. Isabelle supports a generic |
102 far. Isabelle supports a generic notion of \bfindex{symbols} as the |
103 notion of \bfindex{symbols} as the smallest entities of source text, |
103 smallest entities of source text, without referring to internal |
104 without referring to internal encodings. |
104 encodings. There are three kinds of such ``generalized |
105 |
105 characters'': |
106 There are three kinds of such ``generalized characters'' available: |
|
107 |
106 |
108 \begin{enumerate} |
107 \begin{enumerate} |
109 |
108 |
110 \item 7-bit ASCII characters |
109 \item 7-bit ASCII characters |
111 |
110 |
118 Here $ident$ may be any identifier according to the usual Isabelle |
117 Here $ident$ may be any identifier according to the usual Isabelle |
119 conventions. This results in an infinite store of symbols, whose |
118 conventions. This results in an infinite store of symbols, whose |
120 interpretation is left to further front-end tools. For example, |
119 interpretation is left to further front-end tools. For example, |
121 both by the user-interface of Proof~General + X-Symbol and the |
120 both by the user-interface of Proof~General + X-Symbol and the |
122 Isabelle document processor (see \S\ref{sec:document-preparation}) |
121 Isabelle document processor (see \S\ref{sec:document-preparation}) |
123 display the \verb,\,\verb,<forall>, symbol really as ``$\forall$''. |
122 display the \verb,\,\verb,<forall>, symbol really as \isa{{\isasymforall}}. |
124 |
123 |
125 A list of standard Isabelle symbols is given in |
124 A list of standard Isabelle symbols is given in |
126 \cite[appendix~A]{isabelle-sys}. Users may introduce their own |
125 \cite[appendix~A]{isabelle-sys}. Users may introduce their own |
127 interpretation of further symbols by configuring the appropriate |
126 interpretation of further symbols by configuring the appropriate |
128 front-end tool accordingly, e.g.\ by defining certain {\LaTeX} |
127 front-end tool accordingly, e.g.\ by defining certain {\LaTeX} |
129 macros (see also \S\ref{sec:doc-prep-symbols}). There are also a |
128 macros (see also \S\ref{sec:doc-prep-symbols}). There are also a |
130 few predefined control symbols, such as \verb,\,\verb,<^sub>, and |
129 few predefined control symbols, such as \verb,\,\verb,<^sub>, and |
131 \verb,\,\verb,<^sup>, for sub- and superscript of the subsequent |
130 \verb,\,\verb,<^sup>, for sub- and superscript of the subsequent |
132 (printable) symbol, respectively. For example, \verb,A\<^sup>\<star>, is |
131 (printable) symbol, respectively. For example, \verb,A\<^sup>\<star>, is |
133 shown as ``\isa{A\isactrlsup {\isasymstar}}''. |
132 shown as \isa{A\isactrlsup {\isasymstar}}. |
134 |
133 |
135 \medskip The following version of our \isa{xor} definition uses a |
134 \medskip The following version of our \isa{xor} definition uses a |
136 standard Isabelle symbol to achieve typographically pleasing output.% |
135 standard Isabelle symbol to achieve typographically pleasing output.% |
137 \end{isamarkuptext}% |
136 \end{isamarkuptext}% |
138 \isamarkuptrue% |
137 \isamarkuptrue% |
224 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 |
223 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 |
225 printed as \isa{{\isasymeuro}\ {\isadigit{1}}{\isadigit{0}}}; only the head of the application is |
224 printed as \isa{{\isasymeuro}\ {\isadigit{1}}{\isadigit{0}}}; only the head of the application is |
226 subject to our concrete syntax. This simple form already achieves |
225 subject to our concrete syntax. This simple form already achieves |
227 conformance with notational standards of the European Commission. |
226 conformance with notational standards of the European Commission. |
228 |
227 |
229 \medskip Certainly, the same idea of prefix syntax also works for |
228 Prefix syntax also works for plain \isakeyword{consts} or |
230 \isakeyword{consts}, \isakeyword{constdefs} etc. The slightly |
229 \isakeyword{constdefs}, of course.% |
231 unusual syntax declaration below decorates the existing \isa{currency} type with the international currency symbol \isa{{\isasymcurrency}} |
|
232 (\verb,\,\verb,<currency>,).% |
|
233 \end{isamarkuptext}% |
|
234 \isamarkuptrue% |
|
235 \isacommand{syntax}\isanewline |
|
236 \ \ currency\ {\isacharcolon}{\isacharcolon}\ type\ \ \ \ {\isacharparenleft}{\isachardoublequote}{\isasymcurrency}{\isachardoublequote}{\isacharparenright}\isamarkupfalse% |
|
237 % |
|
238 \begin{isamarkuptext}% |
|
239 \noindent Here \isa{type} refers to the builtin syntactic category |
|
240 of Isabelle types. We may now write down funny things like \isa{{\isasymeuro}\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ {\isasymcurrency}}, for example.% |
|
241 \end{isamarkuptext}% |
230 \end{isamarkuptext}% |
242 \isamarkuptrue% |
231 \isamarkuptrue% |
243 % |
232 % |
244 \isamarkupsubsection{Syntax Translations \label{sec:syntax-translations}% |
233 \isamarkupsubsection{Syntax Translations \label{sec:syntax-translations}% |
245 } |
234 } |
255 Using the raw \isakeyword{syntax}\index{syntax (command)} command we |
244 Using the raw \isakeyword{syntax}\index{syntax (command)} command we |
256 may introduce uninterpreted notational elements, while |
245 may introduce uninterpreted notational elements, while |
257 \commdx{translations} relates the input forms with more complex |
246 \commdx{translations} relates the input forms with more complex |
258 logical expressions. This essentially provides a simple mechanism |
247 logical expressions. This essentially provides a simple mechanism |
259 for for syntactic macros; even heavier transformations may be |
248 for for syntactic macros; even heavier transformations may be |
260 programmed in ML \cite{isabelle-ref}. |
249 written in ML \cite{isabelle-ref}. |
261 |
250 |
262 \medskip A typical example of syntax translations is to decorate |
251 \medskip A typical example of syntax translations is to decorate |
263 relational expressions (set membership of tuples) with nice symbolic |
252 relational expressions with nice symbolic notation, such as \isa{{\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}\ {\isasymin}\ sim} versus \isa{x\ {\isasymapprox}\ y}.% |
264 notation, such as \isa{{\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}\ {\isasymin}\ sim} versus \isa{x\ {\isasymapprox}\ y}.% |
|
265 \end{isamarkuptext}% |
253 \end{isamarkuptext}% |
266 \isamarkuptrue% |
254 \isamarkuptrue% |
267 \isacommand{consts}\isanewline |
255 \isacommand{consts}\isanewline |
268 \ \ sim\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set{\isachardoublequote}\isanewline |
256 \ \ sim\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set{\isachardoublequote}\isanewline |
269 \isanewline |
257 \isanewline |
295 \begin{isamarkuptext}% |
283 \begin{isamarkuptext}% |
296 \noindent Normally one would introduce derived concepts like this |
284 \noindent Normally one would introduce derived concepts like this |
297 within the logic, using \isakeyword{consts} + \isakeyword{defs} |
285 within the logic, using \isakeyword{consts} + \isakeyword{defs} |
298 instead of \isakeyword{syntax} + \isakeyword{translations}. The |
286 instead of \isakeyword{syntax} + \isakeyword{translations}. The |
299 present formulation has the virtue that expressions are immediately |
287 present formulation has the virtue that expressions are immediately |
300 replaced by its ``definition'' upon parsing; the effect is reversed |
288 replaced by the ``definition'' upon parsing; the effect is reversed |
301 upon printing. Internally, \isa{{\isasymnoteq}} never appears. |
289 upon printing. |
302 |
290 |
303 Simulating definitions via translations is adequate for very basic |
291 Simulating definitions via translations is adequate for very basic |
304 logical concepts, where a new representation is a trivial variation |
292 principles, where a new representation is a trivial variation on an |
305 on an existing one. On the other hand, syntax translations do not |
293 existing one. On the other hand, syntax translations do not scale |
306 scale up well to large hierarchies of concepts built on each other.% |
294 up well to large hierarchies of concepts built on each other.% |
307 \end{isamarkuptext}% |
295 \end{isamarkuptext}% |
308 \isamarkuptrue% |
296 \isamarkuptrue% |
309 % |
297 % |
310 \isamarkupsection{Document Preparation \label{sec:document-preparation}% |
298 \isamarkupsection{Document Preparation \label{sec:document-preparation}% |
311 } |
299 } |
312 \isamarkuptrue% |
300 \isamarkuptrue% |
313 % |
301 % |
314 \begin{isamarkuptext}% |
302 \begin{isamarkuptext}% |
315 Isabelle/Isar is centered around the concept of \bfindex{formal |
303 Isabelle/Isar is centered around the concept of \bfindex{formal |
316 proof documents}\index{documents|bold}. Ultimately the result of |
304 proof documents}\index{documents|bold}. The ultimate result of a |
317 the user's theory development efforts is meant to be a |
305 formal development effort is meant to be a human-readable record, |
318 human-readable record, presented as a browsable PDF file or printed |
306 presented as browsable PDF file or printed on paper. The overall |
319 on paper. The overall document structure follows traditional |
307 document structure follows traditional mathematical articles, with |
320 mathematical articles, with sectioning, intermediate explanations, |
308 sections, intermediate explanations, definitions, theorems and |
321 definitions, theorem statements and proofs. |
309 proofs. |
322 |
310 |
323 The Isar proof language \cite{Wenzel-PhD}, which is not covered in |
311 The Isar proof language \cite{Wenzel-PhD}, which is not covered in |
324 this book, admits to write formal proof texts that are acceptable |
312 this book, admits to write formal proof texts that are acceptable |
325 both to the machine and human readers at the same time. Thus |
313 both to the machine and human readers at the same time. Thus |
326 marginal comments and explanations may be kept at a minimum. Even |
314 marginal comments and explanations may be kept at a minimum. Even |
327 without proper coverage of human-readable proofs, Isabelle document |
315 without proper coverage of human-readable proofs, Isabelle document |
328 is very useful to produce formally derived texts (elaborating on the |
316 is very useful to produce formally derived texts. Unstructured |
329 specifications etc.). Unstructured proof scripts given here may be |
317 proof scripts given here may be just ignored by readers, or |
330 just ignored by readers, or intentionally suppressed from the text |
318 intentionally suppressed from the text by the writer (see also |
331 by the writer (see also \S\ref{sec:doc-prep-suppress}). |
319 \S\ref{sec:doc-prep-suppress}). |
332 |
320 |
333 \medskip The Isabelle document preparation system essentially acts |
321 \medskip The Isabelle document preparation system essentially acts |
334 like a formal front-end to {\LaTeX}. After checking specifications |
322 like a formal front-end to {\LaTeX}. After checking specifications |
335 and proofs, the theory sources are turned into typesetting |
323 and proofs, the theory sources are turned into typesetting |
336 instructions in a well-defined manner. This enables users to write |
324 instructions in a well-defined manner. This enables users to write |
337 authentic reports on formal theory developments with little |
325 authentic reports on formal developments with little effort, most |
338 additional effort, the most tedious consistency checks are handled |
326 tedious consistency checks are handled by the system.% |
339 by the system.% |
|
340 \end{isamarkuptext}% |
327 \end{isamarkuptext}% |
341 \isamarkuptrue% |
328 \isamarkuptrue% |
342 % |
329 % |
343 \isamarkupsubsection{Isabelle Sessions% |
330 \isamarkupsubsection{Isabelle Sessions% |
344 } |
331 } |
359 \texttt{MySession}: |
346 \texttt{MySession}: |
360 |
347 |
361 \begin{itemize} |
348 \begin{itemize} |
362 |
349 |
363 \item Directory \texttt{MySession} contains the required theory |
350 \item Directory \texttt{MySession} contains the required theory |
364 files ($A@1$\texttt{.thy}, \dots, $A@n$\texttt{.thy}). |
351 files $T@1$\texttt{.thy}, \dots, $T@n$\texttt{.thy}. |
365 |
352 |
366 \item File \texttt{MySession/ROOT.ML} holds appropriate ML commands |
353 \item File \texttt{MySession/ROOT.ML} holds appropriate ML commands |
367 for loading all wanted theories, usually just |
354 for loading all wanted theories, usually just |
368 ``\texttt{use_thy~"$A@i$";}'' for any $A@i$ in leaf position of the |
355 ``\texttt{use_thy"$T@i$";}'' for any $T@i$ in leaf position of the |
369 theory dependency graph. |
356 theory dependency graph. |
370 |
357 |
371 \item Directory \texttt{MySession/document} contains everything |
358 \item Directory \texttt{MySession/document} contains everything |
372 required for the {\LaTeX} stage; only \texttt{root.tex} needs to be |
359 required for the {\LaTeX} stage; only \texttt{root.tex} needs to be |
373 provided initially. |
360 provided initially. |
374 |
361 |
375 The latter file holds appropriate {\LaTeX} code to commence a |
362 The latter file holds appropriate {\LaTeX} code to commence a |
376 document (\verb,\documentclass, etc.), and to include the generated |
363 document (\verb,\documentclass, etc.), and to include the generated |
377 files $A@i$\texttt{.tex} for each theory. The generated |
364 files $T@i$\texttt{.tex} for each theory. The generated |
378 \texttt{session.tex} will hold {\LaTeX} commands to include all |
365 \texttt{session.tex} will hold {\LaTeX} commands to include all |
379 theory output files in topologically sorted order, so |
366 theory output files in topologically sorted order, so |
380 \verb,\input{session}, in \texttt{root.tex} will do it in most |
367 \verb,\input{session}, in \texttt{root.tex} will do it in most |
381 situations. |
368 situations. |
382 |
369 |
383 \item In addition, \texttt{IsaMakefile} outside of the directory |
370 \item \texttt{IsaMakefile} outside of the directory |
384 \texttt{MySession} holds appropriate dependencies and invocations of |
371 \texttt{MySession} holds appropriate dependencies and invocations of |
385 Isabelle tools to control the batch job. In fact, several sessions |
372 Isabelle tools to control the batch job. In fact, several sessions |
386 may be controlled by the same \texttt{IsaMakefile}. See also |
373 may be controlled by the same \texttt{IsaMakefile}. See also |
387 \cite{isabelle-sys} for further details, especially on |
374 \cite{isabelle-sys} for further details, especially on |
388 \texttt{isatool usedir} and \texttt{isatool make}. |
375 \texttt{isatool usedir} and \texttt{isatool make}. |
391 |
378 |
392 With everything put in its proper place, \texttt{isatool make} |
379 With everything put in its proper place, \texttt{isatool make} |
393 should be sufficient to process the Isabelle session completely, |
380 should be sufficient to process the Isabelle session completely, |
394 with the generated document appearing in its proper place. |
381 with the generated document appearing in its proper place. |
395 |
382 |
396 \medskip In practice, users may want to have \texttt{isatool mkdir} |
383 \medskip In reality, users may want to have \texttt{isatool mkdir} |
397 generate an initial working setup without further ado. For example, |
384 generate an initial working setup without further ado. For example, |
398 an empty session \texttt{MySession} derived from \texttt{HOL} may be |
385 an empty session \texttt{MySession} derived from \texttt{HOL} may be |
399 produced as follows: |
386 produced as follows: |
400 |
387 |
401 \begin{verbatim} |
388 \begin{verbatim} |
451 \begin{isamarkuptext}% |
438 \begin{isamarkuptext}% |
452 The large-scale structure of Isabelle documents follows existing |
439 The large-scale structure of Isabelle documents follows existing |
453 {\LaTeX} conventions, with chapters, sections, subsubsections etc. |
440 {\LaTeX} conventions, with chapters, sections, subsubsections etc. |
454 The Isar language includes separate \bfindex{markup commands}, which |
441 The Isar language includes separate \bfindex{markup commands}, which |
455 do not effect the formal content of a theory (or proof), but result |
442 do not effect the formal content of a theory (or proof), but result |
456 in corresponding {\LaTeX} elements issued to the output. |
443 in corresponding {\LaTeX} elements. |
457 |
444 |
458 There are separate markup commands for different formal contexts: in |
445 There are separate markup commands depending on the textual context: |
459 header position (just before a \isakeyword{theory} command), within |
446 in header position (just before \isakeyword{theory}), within the |
460 the theory body, or within a proof. Note that the header needs to |
447 theory body, or within a proof. The header needs to be treated |
461 be treated specially, since ordinary theory and proof commands may |
448 specially here, since ordinary theory and proof commands may only |
462 only occur \emph{after} the initial \isakeyword{theory} |
449 occur \emph{after} the initial \isakeyword{theory} specification. |
463 specification. |
450 |
464 |
451 \medskip |
465 \smallskip |
|
466 |
452 |
467 \begin{tabular}{llll} |
453 \begin{tabular}{llll} |
468 header & theory & proof & default meaning \\\hline |
454 header & theory & proof & default meaning \\\hline |
469 & \commdx{chapter} & & \verb,\chapter, \\ |
455 & \commdx{chapter} & & \verb,\chapter, \\ |
470 \commdx{header} & \commdx{section} & \commdx{sect} & \verb,\section, \\ |
456 \commdx{header} & \commdx{section} & \commdx{sect} & \verb,\section, \\ |
510 |
496 |
511 end |
497 end |
512 \end{ttbox} |
498 \end{ttbox} |
513 |
499 |
514 Users may occasionally want to change the meaning of markup |
500 Users may occasionally want to change the meaning of markup |
515 commands, say via \verb,\renewcommand, in \texttt{root.tex}. The |
501 commands, say via \verb,\renewcommand, in \texttt{root.tex}; |
516 \verb,\isamarkupheader, is a good candidate for some adaption, e.g.\ |
502 \verb,\isamarkupheader, is a good candidate for some adaption, e.g.\ |
517 moving it up in the hierarchy to become \verb,\chapter,. |
503 moving it up in the hierarchy to become \verb,\chapter,. |
518 |
504 |
519 \begin{verbatim} |
505 \begin{verbatim} |
520 \renewcommand{\isamarkupheader}[1]{\chapter{#1}} |
506 \renewcommand{\isamarkupheader}[1]{\chapter{#1}} |
543 \isamarkupsubsection{Formal Comments and Antiquotations% |
529 \isamarkupsubsection{Formal Comments and Antiquotations% |
544 } |
530 } |
545 \isamarkuptrue% |
531 \isamarkuptrue% |
546 % |
532 % |
547 \begin{isamarkuptext}% |
533 \begin{isamarkuptext}% |
548 FIXME check |
534 Isabelle source comments, which are of the form |
549 |
535 \verb,(,\verb,*,~\dots~\verb,*,\verb,),, essentially act like white |
550 Source comments of the form \verb,(,\verb,*,~\dots~\verb,*,\verb,), |
536 space and do not really contribute to the content. They mainly |
551 essentially act like white space and do not contribute to the formal |
537 serve technical purposes to mark certain oddities in the raw input |
552 text at all. They mainly serve technical purposes to mark certain |
538 text. In contrast, \bfindex{formal comments} are portions of text |
553 oddities or problems with the raw sources. |
539 that are associated with formal Isabelle/Isar commands |
554 |
540 (\bfindex{marginal comments}), or as stanalone paragraphs within a |
555 In contrast, \bfindex{formal comments} are portions of text that are |
541 theory or proof context (\bfindex{text blocks}). |
556 associated with formal Isabelle/Isar commands (\bfindex{marginal |
|
557 comments}), or even as stanalone paragraphs positioned explicitly |
|
558 within a theory or proof context (\bfindex{text blocks}). |
|
559 |
542 |
560 \medskip Marginal comments are part of each command's concrete |
543 \medskip Marginal comments are part of each command's concrete |
561 syntax \cite{isabelle-ref}; the common form \verb,--,~text, where |
544 syntax \cite{isabelle-ref}; the common form is ``\verb,--,~text'' |
562 $text$, delimited by \verb,",\dots\verb,", or |
545 where $text$ is delimited by \verb,",\dots\verb,", or |
563 \verb,{,\verb,*,~\dots~\verb,*,\verb,}, as usual. Multiple marginal |
546 \verb,{,\verb,*,~\dots~\verb,*,\verb,}, as usual. Multiple marginal |
564 comments may be given at the same time. Here is a simple example: |
547 comments may be given at the same time. Here is a simple example:% |
548 \end{isamarkuptext}% |
|
549 \isamarkuptrue% |
|
550 \isacommand{lemma}\ {\isachardoublequote}A\ {\isacharminus}{\isacharminus}{\isachargreater}\ A{\isachardoublequote}\isanewline |
|
551 \ \ % |
|
552 \isamarkupcmt{a triviality of propositional logic% |
|
553 } |
|
554 \isanewline |
|
555 \ \ % |
|
556 \isamarkupcmt{(should not really bother)% |
|
557 } |
|
558 \isanewline |
|
559 \ \ \isamarkupfalse% |
|
560 \isacommand{by}\ {\isacharparenleft}rule\ impI{\isacharparenright}\ % |
|
561 \isamarkupcmt{implicit assumption step involved here% |
|
562 } |
|
563 \isamarkupfalse% |
|
564 % |
|
565 \begin{isamarkuptext}% |
|
566 \noindent The above output has been produced as follows: |
|
565 |
567 |
566 \begin{verbatim} |
568 \begin{verbatim} |
567 lemma "A --> A" |
569 lemma "A --> A" |
568 -- "a triviality of propositional logic" |
570 -- "a triviality of propositional logic" |
569 -- "(should not really bother)" |
571 -- "(should not really bother)" |
570 by (rule impI) -- "implicit assumption step involved here" |
572 by (rule impI) -- "implicit assumption step involved here" |
571 \end{verbatim} |
573 \end{verbatim} |
572 |
574 |
573 From the {\LaTeX} view, \verb,--, acts like a markup command, the |
575 From the {\LaTeX} view, ``\verb,--,'' acts like a markup command, |
574 corresponding macro is \verb,\isamarkupcmt, (of a single argument). |
576 the corresponding macro is \verb,\isamarkupcmt, (with a single |
575 |
577 argument). |
576 \medskip The commands \bfindex{text} and \bfindex{txt} both |
578 |
577 introduce a text block (for theory and proof contexts, |
579 \medskip Text blocks are introduced by the commands \bfindex{text} |
578 respectively), taking a single $text$ argument. The {\LaTeX} output |
580 and \bfindex{txt}, for theory and proof contexts, respectively. |
579 appears as a free-form text, surrounded with separate paragraphs and |
581 Each takes again a single $text$ argument, which is interpreted as a |
580 additional vertical spacing. This behavior is determined by the |
582 free-form paragraph in {\LaTeX} (surrounded by some additional |
581 {\LaTeX} environment definitions \verb,isamarkuptext, and |
583 vertical space). The exact behavior may be changed by redefining |
582 \verb,isamarkuptxt,, respectively. This may be changed via |
584 the {\LaTeX} environments of \verb,isamarkuptext, or |
583 \verb,\renewenvironment,, but it is often sufficient to redefine |
585 \verb,isamarkuptxt,, respectively. The text style of the body is |
584 \verb,\isastyletext, or \verb,\isastyletxt, only, which determine |
586 determined by the \verb,\isastyletext, and \verb,\isastyletxt, |
585 the body text style. |
587 macros; the default uses a smaller font within proofs. |
586 |
588 |
587 \medskip The $text$ part of each of the various markup commands |
589 \medskip The $text$ part of each of the various markup commands |
588 considered so far essentially inserts \emph{quoted} material within |
590 considered so far essentially inserts quoted material within a |
589 a formal text, essentially for instruction of the reader only |
591 formal text, mainly for instruction of the reader (arbitrary |
590 (arbitrary {\LaTeX} macros may be included). |
592 {\LaTeX} macros may be also included). An \bfindex{antiquotation} |
591 |
593 is again a formal object that has been embedded into such an |
592 An \bfindex{antiquotation} is again a formal object that has been |
594 informal portion. The interpretation of antiquotations is limited |
593 embedded into such an informal portion of text. Typically, the |
595 to some well-formedness checks, with the result being pretty printed |
594 interpretation of an antiquotation is limited to well-formedness |
596 to the resulting document. So quoted text blocks together with |
595 checks, with the result being pretty printed into the resulting |
597 antiquotations provide very handsome means to reference formal |
596 document output. So quoted text blocks together with antiquotations |
598 entities with good confidence in technical details (especially |
597 provide very handsome means to reference formal entities within |
599 syntax and types). |
598 informal expositions, with a high level of confidence in the |
600 |
599 technical details (especially syntax and types). |
601 The general syntax of antiquotations is as follows: |
600 |
|
601 The general format of antiquotations is as follows: |
|
602 \texttt{{\at}{\ttlbrace}$name$ $arguments${\ttrbrace}}, or |
602 \texttt{{\at}{\ttlbrace}$name$ $arguments${\ttrbrace}}, or |
603 \texttt{{\at}{\ttlbrace}$name$ [$options$] $arguments${\ttrbrace}} |
603 \texttt{{\at}{\ttlbrace}$name$ [$options$] $arguments${\ttrbrace}} |
604 for a comma-separated list of $name$ or assignments |
604 for a comma-separated list of options consisting of a $name$ or |
605 \texttt{$name$=$value$} of $options$ (see \cite{isabelle-isar-ref} |
605 \texttt{$name$=$value$} pair \cite{isabelle-isar-ref}. The syntax |
606 for details). The syntax of $arguments$ depends on the |
606 of $arguments$ depends on the kind of antiquotation, it generally |
607 antiquotation name, it generally follows the same conventions for |
607 follows the same conventions for types, terms, or theorems as in the |
608 types, terms, or theorems as in the formal part of a theory. |
608 formal part of a theory. |
609 |
609 |
610 \medskip Here is an example use of the quotation-antiquotation |
610 \medskip Here is an example of the quotation-antiquotation |
611 technique: \isa{{\isasymlambda}x\ y{\isachardot}\ x} is a well-typed term. |
611 technique: \isa{{\isasymlambda}x\ y{\isachardot}\ x} is a well-typed term. |
612 |
612 |
613 \medskip This output has been produced as follows: |
613 \medskip\noindent The above output has been produced as follows: |
614 \begin{ttbox} |
614 \begin{ttbox} |
615 text {\ttlbrace}* |
615 text {\ttlbrace}* |
616 Here is an example use of the quotation-antiquotation technique: |
616 Here is an example of the quotation-antiquotation technique: |
617 {\at}{\ttlbrace}term "%x y. x"{\ttrbrace} is a well-typed term. |
617 {\at}{\ttlbrace}term "%x y. x"{\ttrbrace} is a well-typed term. |
618 *{\ttrbrace} |
618 *{\ttrbrace} |
619 \end{ttbox} |
619 \end{ttbox} |
620 |
620 |
621 From the notational change of the ASCII character \verb,%, to the |
621 From the notational change of the ASCII character \verb,%, to the |
622 symbol \isa{{\isasymlambda}} we see that the term really got printed by the |
622 symbol \isa{{\isasymlambda}} we see that the term really got printed by the |
623 system --- recall that the document preparation system enables |
623 system (after parsing and type-checking), document preparation |
624 symbolic output by default. |
624 enables symbolic output by default. |
625 |
625 |
626 \medskip In the following example we include an option to enable the |
626 \medskip The next example includes an option to modify the |
627 \verb,show_types, flag of Isabelle: the antiquotation |
627 \verb,show_types, flag of Isabelle: |
628 \texttt{{\at}}\verb,{term [show_types] "%x y. x"}, produces \isa{{\isasymlambda}{\isacharparenleft}x{\isasymColon}{\isacharprime}a{\isacharparenright}\ y{\isasymColon}{\isacharprime}b{\isachardot}\ x}. Here type-inference has figured out the |
628 \texttt{{\at}}\verb,{term [show_types] "%x y. x"}, produces \isa{{\isasymlambda}{\isacharparenleft}x{\isasymColon}{\isacharprime}a{\isacharparenright}\ y{\isasymColon}{\isacharprime}b{\isachardot}\ x}. Here type-inference has figured out the |
629 most general typings in the present (theory) context. Within a |
629 most general typings in the present (theory) context. Note that |
630 proof, one may get different results according to typings that have |
630 term fragments may acquire a different typings due to constraints |
631 already been figured out in the text so far, say some fixed |
631 imposed by previous text (within a proof), say by the main goal |
632 variables in the main statement given before hand. |
632 statement given before hand. |
633 |
633 |
634 \medskip Several further kinds of antiquotations (and options) are |
634 \medskip Several further kinds of antiquotations (and options) are |
635 available \cite{isabelle-sys}. The most commonly used combinations |
635 available \cite{isabelle-sys}. Here are a few commonly used |
636 are as follows: |
636 combinations are as follows: |
637 |
637 |
638 \medskip |
638 \medskip |
639 |
639 |
640 \begin{tabular}{ll} |
640 \begin{tabular}{ll} |
641 \texttt{\at}\verb,{typ,~$\tau$\verb,}, & print type $\tau$ \\ |
641 \texttt{\at}\verb,{typ,~$\tau$\verb,}, & print type $\tau$ \\ |
642 \texttt{\at}\verb,{term,~$t$\verb,}, & print term $t$ \\ |
642 \texttt{\at}\verb,{term,~$t$\verb,}, & print term $t$ \\ |
643 \texttt{\at}\verb,{prop,~$\phi$\verb,}, & print proposition $\phi$ \\ |
643 \texttt{\at}\verb,{prop,~$\phi$\verb,}, & print proposition $\phi$ \\ |
644 \texttt{\at}\verb,{prop [display],~$\phi$\verb,}, & print large proposition $\phi$ (with linebreaks) \\ |
|
644 \texttt{\at}\verb,{prop [source],~$\phi$\verb,}, & check proposition $\phi$, print its input \\ |
645 \texttt{\at}\verb,{prop [source],~$\phi$\verb,}, & check proposition $\phi$, print its input \\ |
645 \texttt{\at}\verb,{thm,~$a$\verb,}, & print fact $a$ \\ |
646 \texttt{\at}\verb,{thm,~$a$\verb,}, & print fact $a$ \\ |
646 \texttt{\at}\verb,{thm,~$a$~\verb,[no_vars]}, & print fact $a$, fixing schematic variables \\ |
647 \texttt{\at}\verb,{thm,~$a$~\verb,[no_vars]}, & print fact $a$, fixing schematic variables \\ |
647 \texttt{\at}\verb,{thm [source],~$a$\verb,}, & check availability of fact $a$, print its name \\ |
648 \texttt{\at}\verb,{thm [source],~$a$\verb,}, & check validity of fact $a$, print its name \\ |
648 \texttt{\at}\verb,{text,~$s$\verb,}, & print uninterpreted text $s$ \\ |
649 \texttt{\at}\verb,{text,~$s$\verb,}, & print uninterpreted text $s$ \\ |
649 \end{tabular} |
650 \end{tabular} |
650 |
651 |
651 \medskip |
652 \medskip |
652 |
653 |
653 Note that \verb,no_vars, given above is \emph{not} an option, but |
654 Note that \attrdx{no_vars} given above is \emph{not} an |
654 merely an attribute of the theorem argument given here. |
655 antiquotation option, but an attribute of the theorem argument given |
655 |
656 here. This might be useful with a diagnostic command like |
656 The \texttt{\at}\verb,{text, $s$\verb,}, antiquotation is |
657 \isakeyword{thm}, too. |
658 |
|
659 \medskip The \texttt{\at}\verb,{text, $s$\verb,}, antiquotation is |
|
657 particularly interesting. Embedding uninterpreted text within an |
660 particularly interesting. Embedding uninterpreted text within an |
658 informal text body might appear useless at first sight. Here the |
661 informal body might appear useless at first sight. Here the key |
659 key virtue is that the string $s$ is processed as proper Isabelle |
662 virtue is that the string $s$ is processed as Isabelle output, |
660 output, interpreting Isabelle symbols (\S\ref{sec:syntax-symbols}) |
663 interpreting Isabelle symbols appropriately. |
661 appropriately. |
664 |
662 |
665 For example, \texttt{\at}\verb,{text "\<forall>\<exists>"}, produces \isa{{\isasymforall}{\isasymexists}}, according to the standard interpretation of these symbol |
663 For example, \texttt{\at}\verb,{text "\<forall>\<exists>"}, produces \isa{{\isasymforall}{\isasymexists}}, |
666 (cf.\ \S\ref{sec:doc-prep-symbols}). Thus we achieve consistent |
664 according to the standard interpretation of these symbol (cf.\ |
|
665 \S\ref{sec:doc-prep-symbols}). Thus we achieve consistent |
|
666 mathematical notation in both the formal and informal parts of the |
667 mathematical notation in both the formal and informal parts of the |
667 document very easily. Manual {\LaTeX} code leaves more control over |
668 document very easily. Manual {\LaTeX} code would leave more control |
668 the type-setting, but is slightly more tedious. Also note that |
669 over the type-setting, but is also slightly more tedious.% |
669 Isabelle symbols may be also displayed within the editor buffer of |
|
670 Proof~General.% |
|
671 \end{isamarkuptext}% |
670 \end{isamarkuptext}% |
672 \isamarkuptrue% |
671 \isamarkuptrue% |
673 % |
672 % |
674 \isamarkupsubsection{Interpretation of symbols \label{sec:doc-prep-symbols}% |
673 \isamarkupsubsection{Interpretation of symbols \label{sec:doc-prep-symbols}% |
675 } |
674 } |
676 \isamarkuptrue% |
675 \isamarkuptrue% |
677 % |
676 % |
678 \begin{isamarkuptext}% |
677 \begin{isamarkuptext}% |
679 FIXME tune |
678 As has been pointed out before (\S\ref{sec:syntax-symbols}), |
680 |
679 Isabelle symbols are the the smallest syntactic entities, a |
681 According to \S\ref{sec:syntax-symbols}, the smalles syntactic |
680 straight-forward generalization of ASCII characters. While Isabelle |
682 entities of Isabelle text are symbols, a straight-forward |
681 does not impose any interpretation of the infinite collection of |
683 generalization of ASCII characters. Concerning document |
682 symbols, the {\LaTeX} document output produces the canonical output |
684 preperation, symbols are translated uniformly to {\LaTeX} code as |
683 for certain standard symbols \cite[appendix~A]{isabelle-sys}. |
685 follows. |
684 |
685 The {\LaTeX} code produced from Isabelle text follows a relatively |
|
686 simple scheme (see below). Users may wish to tune the final |
|
687 appearance by redefining certain macros, say in \texttt{root.tex} of |
|
688 the document. |
|
686 |
689 |
687 \begin{enumerate} \item 7-bit ASCII characters: letters |
690 \begin{enumerate} \item 7-bit ASCII characters: letters |
688 \texttt{A\dots Z} and \texttt{a\dots z} are output verbatim, digits |
691 \texttt{A\dots Z} and \texttt{a\dots z} are output verbatim, digits |
689 are passed as an argument to the \verb,\isadigit, macro, other |
692 are passed as an argument to the \verb,\isadigit, macro, other |
690 characters are replaced by specific macros \verb,\isacharXYZ, (see |
693 characters are replaced by specifically named macros of the form |
691 also \texttt{isabelle.sty}). |
694 \verb,\isacharXYZ,. |
692 |
695 |
693 \item Named symbols: \verb,\,\verb,<,$XYZ$\verb,>, become |
696 \item Named symbols: \verb,\,\verb,<,$XYZ$\verb,>, become |
694 \verb,\{\isasym,$XYZ$\verb,}, each (note the additional braces). |
697 \verb,{\isasym,$XYZ$\verb,}, each (note the additional braces). See |
695 See \cite[appendix~A]{isabelle-sys} and \texttt{isabellesym.sty} for |
698 \cite[appendix~A]{isabelle-sys} and \texttt{isabellesym.sty} for the |
696 the collection of predefined standard symbols. |
699 collection of predefined standard symbols. |
697 |
700 |
698 \item Named control symbols: \verb,\,\verb,<^,$XYZ$\verb,>, become |
701 \item Named control symbols: \verb,\,\verb,<^,$XYZ$\verb,>, become |
699 \verb,\isactrl,$XYZ$; subsequent symbols may act as arguments, if |
702 \verb,\isactrl,$XYZ$; subsequent symbols may act as arguments, if |
700 the corresponding macro is defined accordingly. |
703 the corresponding macro is defined accordingly. |
701 \end{enumerate}% |
704 \end{enumerate} |
705 |
|
706 Users may occasionally wish to invent new named symbols; this merely |
|
707 requires an appropriate definition of \verb,\,\verb,<,$XYZ$\verb,>, |
|
708 as far as {\LaTeX} output is concerned. Control symbols are |
|
709 slightly more difficult to get right, though. |
|
710 |
|
711 \medskip The \verb,\isabellestyle, macro provides a high-level |
|
712 interface to tune the general appearance of individual symbols. For |
|
713 example, \verb,\isabellestyle{it}, uses italics fonts to mimic the |
|
714 general appearance of the {\LaTeX} math mode; double quotes are not |
|
715 printed at all. The resulting quality of type-setting is quite |
|
716 good, so this should probably be the default style for real |
|
717 production work that gets distributed to a broader audience.% |
|
702 \end{isamarkuptext}% |
718 \end{isamarkuptext}% |
703 \isamarkuptrue% |
719 \isamarkuptrue% |
704 % |
720 % |
705 \isamarkupsubsection{Suppressing Output \label{sec:doc-prep-suppress}% |
721 \isamarkupsubsection{Suppressing Output \label{sec:doc-prep-suppress}% |
706 } |
722 } |
724 the ML operator \verb,no_document, temporarily disables document |
740 the ML operator \verb,no_document, temporarily disables document |
725 generation while executing a theory loader command; its usage is |
741 generation while executing a theory loader command; its usage is |
726 like this: |
742 like this: |
727 |
743 |
728 \begin{verbatim} |
744 \begin{verbatim} |
729 no_document use_thy "A"; |
745 no_document use_thy "T"; |
730 \end{verbatim} |
746 \end{verbatim} |
731 |
747 |
732 \medskip Theory output may be also suppressed in smaller portions as |
748 \medskip Theory output may be also suppressed in smaller portions as |
733 well. For example, research papers or slides usually do not include |
749 well. For example, research papers or slides usually do not include |
734 the formal content in full. In order to delimit \bfindex{ignored |
750 the formal content in full. In order to delimit \bfindex{ignored |
743 |
759 |
744 \medskip |
760 \medskip |
745 |
761 |
746 \begin{tabular}{l} |
762 \begin{tabular}{l} |
747 \verb,(,\verb,*,\verb,<,\verb,*,\verb,), \\ |
763 \verb,(,\verb,*,\verb,<,\verb,*,\verb,), \\ |
748 \texttt{theory A = Main:} \\ |
764 \texttt{theory T = Main:} \\ |
749 \verb,(,\verb,*,\verb,>,\verb,*,\verb,), \\ |
765 \verb,(,\verb,*,\verb,>,\verb,*,\verb,), \\ |
750 ~~$\vdots$ \\ |
766 ~~$\vdots$ \\ |
751 \verb,(,\verb,*,\verb,<,\verb,*,\verb,), \\ |
767 \verb,(,\verb,*,\verb,<,\verb,*,\verb,), \\ |
752 \texttt{end} \\ |
768 \texttt{end} \\ |
753 \verb,(,\verb,*,\verb,>,\verb,*,\verb,), \\ |
769 \verb,(,\verb,*,\verb,>,\verb,*,\verb,), \\ |
779 easy to invalidate the remaining visible text, e.g.\ by referencing |
795 easy to invalidate the remaining visible text, e.g.\ by referencing |
780 questionable formal items (strange definitions, arbitrary axioms |
796 questionable formal items (strange definitions, arbitrary axioms |
781 etc.) that have been hidden from sight beforehand. |
797 etc.) that have been hidden from sight beforehand. |
782 |
798 |
783 Some minor technical subtleties of the |
799 Some minor technical subtleties of the |
784 \verb,(,\verb,*,\verb,<,\verb,*,\verb,),-\verb,(,\verb,*,\verb,>,\verb,*,\verb,), |
800 \verb,(,\verb,*,\verb,<,\verb,*,\verb,),~\verb,(,\verb,*,\verb,>,\verb,*,\verb,), |
785 elements need to be kept in mind as well, since the system performs |
801 elements need to be kept in mind as well, since the system performs |
786 little sanity checks here. Arguments of markup commands and formal |
802 little sanity checks here. Arguments of markup commands and formal |
787 comments must not be hidden, otherwise presentation fails. Open and |
803 comments must not be hidden, otherwise presentation fails. Open and |
788 close parentheses need to be inserted carefully; it is fairly easy |
804 close parentheses need to be inserted carefully; it is fairly easy |
789 to hide the wrong parts, especially after rearranging the sources. |
805 to hide the wrong parts, especially after rearranging the sources. |