3 (*>*) |
3 (*>*) |
4 |
4 |
5 section {* Concrete Syntax \label{sec:concrete-syntax} *} |
5 section {* Concrete Syntax \label{sec:concrete-syntax} *} |
6 |
6 |
7 text {* |
7 text {* |
8 The core concept of Isabelle's elaborate infrastructure for concrete |
8 The core concept of Isabelle's framework for concrete |
9 syntax is that of general \bfindex{mixfix annotations}. Associated |
9 syntax is that of \bfindex{mixfix annotations}. Associated |
10 with any kind of constant declaration, mixfixes affect both the |
10 with any kind of constant declaration, mixfixes affect both the |
11 grammar productions for the parser and output templates for the |
11 grammar productions for the parser and output templates for the |
12 pretty printer. |
12 pretty printer. |
13 |
13 |
14 In full generality, parser and pretty printer configuration is a |
14 In full generality, parser and pretty printer configuration is a |
15 rather subtle affair, see \cite{isabelle-ref} for details. Syntax |
15 subtle affair \cite{isabelle-ref}. Your syntax |
16 specifications given by end-users need to interact properly with the |
16 specifications need to interact properly with the |
17 existing setup of Isabelle/Pure and Isabelle/HOL. It is |
17 existing setup of Isabelle/Pure and Isabelle/HOL\@. |
18 particularly important to get the precedence of new syntactic |
18 To avoid creating ambiguities with existing elements, it is |
19 constructs right, avoiding ambiguities with existing elements. |
19 particularly important to give new syntactic |
|
20 constructs the right precedence. |
20 |
21 |
21 \medskip Subsequently we introduce a few simple syntax declaration |
22 \medskip Subsequently we introduce a few simple syntax declaration |
22 forms that already cover many common situations fairly well. |
23 forms that already cover many common situations fairly well. |
23 *} |
24 *} |
24 |
25 |
25 |
26 |
26 subsection {* Infix Annotations *} |
27 subsection {* Infix Annotations *} |
27 |
28 |
28 text {* |
29 text {* |
29 Syntax annotations may be included wherever constants are declared |
30 Syntax annotations may be included wherever constants are declared, |
30 directly or indirectly, including \isacommand{consts}, |
31 such as \isacommand{consts} and |
31 \isacommand{constdefs}, or \isacommand{datatype} (for the |
32 \isacommand{constdefs} --- and also \isacommand{datatype}, which |
32 constructor operations). Type-constructors may be annotated as |
33 declares constructor operations. Type-constructors may be annotated as |
33 well, although this is less frequently encountered in practice (the |
34 well, although this is less frequently encountered in practice (the |
34 infix type @{text "\<times>"} comes to mind). |
35 infix type @{text "\<times>"} comes to mind). |
35 |
36 |
36 Infix declarations\index{infix annotations} provide a useful special |
37 Infix declarations\index{infix annotations} provide a useful special |
37 case of mixfixes, where users need not care about the full details |
38 case of mixfixes. The following example of the |
38 of priorities, nesting, spacing, etc. The following example of the |
|
39 exclusive-or operation on boolean values illustrates typical infix |
39 exclusive-or operation on boolean values illustrates typical infix |
40 declarations arising in practice. |
40 declarations. |
41 *} |
41 *} |
42 |
42 |
43 constdefs |
43 constdefs |
44 xor :: "bool \<Rightarrow> bool \<Rightarrow> bool" (infixl "[+]" 60) |
44 xor :: "bool \<Rightarrow> bool \<Rightarrow> bool" (infixl "[+]" 60) |
45 "A [+] B \<equiv> (A \<and> \<not> B) \<or> (\<not> A \<and> B)" |
45 "A [+] B \<equiv> (A \<and> \<not> B) \<or> (\<not> A \<and> B)" |
46 |
46 |
47 text {* |
47 text {* |
48 \noindent Now @{text "xor A B"} and @{text "A [+] B"} refer to the |
48 \noindent Now @{text "xor A B"} and @{text "A [+] B"} refer to the |
49 same expression internally. Any curried function with at least two |
49 same expression internally. Any curried function with at least two |
50 arguments may be associated with infix syntax. For partial |
50 arguments may be given infix syntax. For partial |
51 applications with less than two operands there is a special notation |
51 applications with fewer than two operands, there is a notation |
52 with \isa{op} prefix: @{text xor} without arguments is represented |
52 using the prefix~\isa{op}. For instance, @{text xor} without arguments is represented |
53 as @{text "op [+]"}; together with plain prefix application this |
53 as @{text "op [+]"}; together with ordinary function application, this |
54 turns @{text "xor A"} into @{text "op [+] A"}. |
54 turns @{text "xor A"} into @{text "op [+] A"}. |
55 |
55 |
56 \medskip The keyword \isakeyword{infixl} seen above specifies an |
56 \medskip The keyword \isakeyword{infixl} seen above specifies an |
57 infix operator that is nested to the \emph{left}: in iterated |
57 infix operator that is nested to the \emph{left}: in iterated |
58 applications the more complex expression appears on the left-hand |
58 applications the more complex expression appears on the left-hand |
59 side, @{term "A [+] B [+] C"} stands for @{text "(A [+] B) [+] C"}. |
59 side, and @{term "A [+] B [+] C"} stands for @{text "(A [+] B) [+] C"}. |
60 Similarly, \isakeyword{infixr} specifies nesting to the |
60 Similarly, \isakeyword{infixr} specifies nesting to the |
61 \emph{right}, reading @{term "A [+] B [+] C"} as @{text "A [+] (B |
61 \emph{right}, reading @{term "A [+] B [+] C"} as @{text "A [+] (B |
62 [+] C)"}. In contrast, a \emph{non-oriented} declaration via |
62 [+] C)"}. In contrast, a \emph{non-oriented} declaration via |
63 \isakeyword{infix} would render @{term "A [+] B [+] C"} illegal, but |
63 \isakeyword{infix} would render @{term "A [+] B [+] C"} illegal, but |
64 demand explicit parentheses to indicate the intended grouping. |
64 demand explicit parentheses to indicate the intended grouping. |
65 |
65 |
66 The string @{text [source] "[+]"} in our annotation refers to the |
66 The string @{text [source] "[+]"} in our annotation refers to the |
67 concrete syntax to represent the operator (a literal token), while |
67 concrete syntax to represent the operator (a literal token), while |
68 the number @{text 60} determines the precedence of the construct |
68 the number @{text 60} determines the precedence of the construct: |
69 (i.e.\ the syntactic priorities of the arguments and result). As it |
69 the syntactic priorities of the arguments and result. |
70 happens, Isabelle/HOL already uses up many popular combinations of |
70 Isabelle/HOL already uses up many popular combinations of |
71 ASCII symbols for its own use, including both @{text "+"} and @{text |
71 ASCII symbols for its own use, including both @{text "+"} and @{text |
72 "++"}. As a rule of thumb, more awkward character combinations are |
72 "++"}. Longer character combinations are |
73 more likely to be still available for user extensions, just as our |
73 more likely to be still available for user extensions, such as our~@{text "[+]"}. |
74 present @{text "[+]"}. |
74 |
75 |
75 Operator precedences have a range of 0--1000. Very low or high priorities are |
76 Operator precedence also needs some special considerations. The |
76 reserved for the meta-logic. HOL syntax |
77 admissible range is 0--1000. Very low or high priorities are |
|
78 basically reserved for the meta-logic. Syntax of Isabelle/HOL |
|
79 mainly uses the range of 10--100: the equality infix @{text "="} is |
77 mainly uses the range of 10--100: the equality infix @{text "="} is |
80 centered at 50, logical connectives (like @{text "\<or>"} and @{text |
78 centered at 50; logical connectives (like @{text "\<or>"} and @{text |
81 "\<and>"}) are below 50, and algebraic ones (like @{text "+"} and @{text |
79 "\<and>"}) are below 50; algebraic ones (like @{text "+"} and @{text |
82 "*"}) above 50. User syntax should strive to coexist with common |
80 "*"}) are above 50. User syntax should strive to coexist with common |
83 HOL forms, or use the mostly unused range 100--900. |
81 HOL forms, or use the mostly unused range 100--900. |
84 |
82 |
85 *} |
83 *} |
86 |
84 |
87 |
85 |
88 subsection {* Mathematical Symbols \label{sec:syntax-symbols} *} |
86 subsection {* Mathematical Symbols \label{sec:syntax-symbols} *} |
89 |
87 |
90 text {* |
88 text {* |
91 Concrete syntax based on plain ASCII characters has its inherent |
89 Concrete syntax based on ASCII characters has inherent |
92 limitations. Rich mathematical notation demands a larger repertoire |
90 limitations. Mathematical notation demands a larger repertoire |
93 of glyphs. Several standards of extended character sets have been |
91 of glyphs. Several standards of extended character sets have been |
94 proposed over decades, but none has become universally available so |
92 proposed over decades, but none has become universally available so |
95 far. Isabelle supports a generic notion of \bfindex{symbols} as the |
93 far. Isabelle supports a generic notion of \bfindex{symbols} as the |
96 smallest entities of source text, without referring to internal |
94 smallest entities of source text, without referring to internal |
97 encodings. There are three kinds of such ``generalized |
95 encodings. There are three kinds of such ``generalized |
110 Here $ident$ may be any identifier according to the usual Isabelle |
108 Here $ident$ may be any identifier according to the usual Isabelle |
111 conventions. This results in an infinite store of symbols, whose |
109 conventions. This results in an infinite store of symbols, whose |
112 interpretation is left to further front-end tools. For example, |
110 interpretation is left to further front-end tools. For example, |
113 both the user-interface of Proof~General + X-Symbol and the Isabelle |
111 both the user-interface of Proof~General + X-Symbol and the Isabelle |
114 document processor (see \S\ref{sec:document-preparation}) display |
112 document processor (see \S\ref{sec:document-preparation}) display |
115 the \verb,\,\verb,<forall>, symbol as @{text \<forall>}. |
113 the \verb,\,\verb,<forall>, symbol as~@{text \<forall>}. |
116 |
114 |
117 A list of standard Isabelle symbols is given in |
115 A list of standard Isabelle symbols is given in |
118 \cite[appendix~A]{isabelle-sys}. Users may introduce their own |
116 \cite[appendix~A]{isabelle-sys}. You may introduce their own |
119 interpretation of further symbols by configuring the appropriate |
117 interpretation of further symbols by configuring the appropriate |
120 front-end tool accordingly, e.g.\ by defining certain {\LaTeX} |
118 front-end tool accordingly, e.g.\ by defining certain {\LaTeX} |
121 macros (see also \S\ref{sec:doc-prep-symbols}). There are also a |
119 macros (see also \S\ref{sec:doc-prep-symbols}). There are also a |
122 few predefined control symbols, such as \verb,\,\verb,<^sub>, and |
120 few predefined control symbols, such as \verb,\,\verb,<^sub>, and |
123 \verb,\,\verb,<^sup>, for sub- and superscript of the subsequent |
121 \verb,\,\verb,<^sup>, for sub- and superscript of the subsequent |
124 (printable) symbol, respectively. For example, \verb,A\<^sup>\<star>, is |
122 printable symbol, respectively. For example, \verb,A\<^sup>\<star>, is |
125 output as @{text "A\<^sup>\<star>"}. |
123 output as @{text "A\<^sup>\<star>"}. |
126 |
124 |
127 \medskip The following version of our @{text xor} definition uses a |
125 \medskip Replacing our definition of @{text xor} by the following |
128 standard Isabelle symbol to achieve typographically more pleasing |
126 specifies a Isabelle symbol for the new operator: |
129 output than before. |
|
130 *} |
127 *} |
131 |
128 |
132 (*<*) |
129 (*<*) |
133 hide const xor |
130 hide const xor |
134 ML_setup {* Context.>> (Theory.add_path "version1") *} |
131 ML_setup {* Context.>> (Theory.add_path "version1") *} |
209 printed as @{term "\<euro> 10"}; only the head of the application is |
206 printed as @{term "\<euro> 10"}; only the head of the application is |
210 subject to our concrete syntax. This rather simple form already |
207 subject to our concrete syntax. This rather simple form already |
211 achieves conformance with notational standards of the European |
208 achieves conformance with notational standards of the European |
212 Commission. |
209 Commission. |
213 |
210 |
214 Prefix syntax also works for plain \isakeyword{consts} or |
211 Prefix syntax also works for \isakeyword{consts} or |
215 \isakeyword{constdefs}, of course. |
212 \isakeyword{constdefs}. |
216 *} |
213 *} |
217 |
214 |
218 |
215 |
219 subsection {* Syntax Translations \label{sec:syntax-translations} *} |
216 subsection {* Syntax Translations \label{sec:syntax-translations} *} |
220 |
217 |
221 text{* |
218 text{* |
222 Mixfix syntax annotations work well in those situations where |
219 Mixfix syntax annotations merely decorate |
223 particular constant application forms need to be decorated by |
220 particular constant application forms with |
224 concrete syntax; e.g.\ @{text "xor A B"} versus @{text "A \<oplus> B"} |
221 concrete syntax, for instance replacing \ @{text "xor A B"} by @{text "A \<oplus> B"}. Occasionally, the relationship between some piece of |
225 covered before. Occasionally the relationship between some piece of |
222 notation and its internal form is more complicated. Here we need |
226 notation and its internal form is slightly more involved. Here the |
223 \bfindex{syntax translations}. |
227 concept of \bfindex{syntax translations} enters the scene. |
224 |
228 |
225 Using the \isakeyword{syntax}\index{syntax (command)}, command we |
229 Using the raw \isakeyword{syntax}\index{syntax (command)} command we |
226 introduce uninterpreted notational elements. Then |
230 may introduce uninterpreted notational elements, while |
227 \commdx{translations} relate input forms to complex logical |
231 \commdx{translations} relate input forms with more complex logical |
228 expressions. This provides a simple mechanism for |
232 expressions. This essentially provides a simple mechanism for |
|
233 syntactic macros; even heavier transformations may be written in ML |
229 syntactic macros; even heavier transformations may be written in ML |
234 \cite{isabelle-ref}. |
230 \cite{isabelle-ref}. |
235 |
231 |
236 \medskip A typical example of syntax translations is to decorate |
232 \medskip A typical use of syntax translations is to introduce |
237 relational expressions (set-membership of tuples) with symbolic |
233 relational notation for membership in a set of pair, |
238 notation, e.g.\ @{text "(x, y) \<in> sim"} versus @{text "x \<approx> y"}. |
234 replacing \ @{text "(x, y) \<in> sim"} by @{text "x \<approx> y"}. |
239 *} |
235 *} |
240 |
236 |
241 consts |
237 consts |
242 sim :: "('a \<times> 'a) set" |
238 sim :: "('a \<times> 'a) set" |
243 |
239 |
269 instead of \isakeyword{syntax} + \isakeyword{translations}. The |
265 instead of \isakeyword{syntax} + \isakeyword{translations}. The |
270 present formulation has the virtue that expressions are immediately |
266 present formulation has the virtue that expressions are immediately |
271 replaced by the ``definition'' upon parsing; the effect is reversed |
267 replaced by the ``definition'' upon parsing; the effect is reversed |
272 upon printing. |
268 upon printing. |
273 |
269 |
274 Simulating definitions via translations is adequate for very basic |
270 This sort of translation is appropriate when the |
275 principles, where a new representation is a trivial variation on an |
271 defined concept is a trivial variation on an |
276 existing one. On the other hand, syntax translations do not scale |
272 existing one. On the other hand, syntax translations do not scale |
277 up well to large hierarchies of concepts built on each other. |
273 up well to large hierarchies of concepts. Translations |
|
274 do not replace definitions! |
278 *} |
275 *} |
279 |
276 |
280 |
277 |
281 section {* Document Preparation \label{sec:document-preparation} *} |
278 section {* Document Preparation \label{sec:document-preparation} *} |
282 |
279 |
283 text {* |
280 text {* |
284 Isabelle/Isar is centered around the concept of \bfindex{formal |
281 Isabelle/Isar is centered around the concept of \bfindex{formal |
285 proof documents}\index{documents|bold}. The ultimate result of a |
282 proof documents}\index{documents|bold}. The outcome of a |
286 formal development effort is meant to be a human-readable record, |
283 formal development effort is meant to be a human-readable record, |
287 presented as browsable PDF file or printed on paper. The overall |
284 presented as browsable PDF file or printed on paper. The overall |
288 document structure follows traditional mathematical articles, with |
285 document structure follows traditional mathematical articles, with |
289 sections, intermediate explanations, definitions, theorems and |
286 sections, intermediate explanations, definitions, theorems and |
290 proofs. |
287 proofs. |
291 |
288 |
292 \medskip The Isabelle document preparation system essentially acts |
289 \medskip The Isabelle document preparation system essentially acts |
293 as a front-end to {\LaTeX}. After checking specifications and |
290 as a front-end to {\LaTeX}. After checking specifications and |
294 proofs formally, the theory sources are turned into typesetting |
291 proofs formally, the theory sources are turned into typesetting |
295 instructions in a schematic manner. This enables users to write |
292 instructions in a schematic manner. This lets you write |
296 authentic reports on theory developments with little effort --- many |
293 authentic reports on theory developments with little effort: many |
297 technical consistency checks are handled by the system. |
294 technical consistency checks are handled by the system. |
298 |
295 |
299 Here is an example to illustrate the idea of Isabelle document |
296 Here is an example to illustrate the idea of Isabelle document |
300 preparation. |
297 preparation. |
301 *} |
298 *} |
405 in most situations. |
402 in most situations. |
406 |
403 |
407 \item \texttt{IsaMakefile} holds appropriate dependencies and |
404 \item \texttt{IsaMakefile} holds appropriate dependencies and |
408 invocations of Isabelle tools to control the batch job. In fact, |
405 invocations of Isabelle tools to control the batch job. In fact, |
409 several sessions may be managed by the same \texttt{IsaMakefile}. |
406 several sessions may be managed by the same \texttt{IsaMakefile}. |
410 See also \cite{isabelle-sys} for further details, especially on |
407 See the \emph{Isabelle System Manual} \cite{isabelle-sys} |
|
408 for further details, especially on |
411 \texttt{isatool usedir} and \texttt{isatool make}. |
409 \texttt{isatool usedir} and \texttt{isatool make}. |
412 |
410 |
413 \end{itemize} |
411 \end{itemize} |
414 |
412 |
415 One may now start to populate the directory \texttt{MySession}, and |
413 One may now start to populate the directory \texttt{MySession}, and |
416 the file \texttt{MySession/ROOT.ML} accordingly. |
414 the file \texttt{MySession/ROOT.ML} accordingly. |
417 \texttt{MySession/document/root.tex} should also be adapted at some |
415 The file \texttt{MySession/document/root.tex} should also be adapted at some |
418 point; the default version is mostly self-explanatory. Note that |
416 point; the default version is mostly self-explanatory. Note that |
419 \verb,\isabellestyle, enables fine-tuning of the general appearance |
417 \verb,\isabellestyle, enables fine-tuning of the general appearance |
420 of characters and mathematical symbols (see also |
418 of characters and mathematical symbols (see also |
421 \S\ref{sec:doc-prep-symbols}). |
419 \S\ref{sec:doc-prep-symbols}). |
422 |
420 |
423 Especially observe the included {\LaTeX} packages \texttt{isabelle} |
421 Especially observe the included {\LaTeX} packages \texttt{isabelle} |
424 (mandatory), \texttt{isabellesym} (required for mathematical |
422 (mandatory), \texttt{isabellesym} (required for mathematical |
425 symbols), and the final \texttt{pdfsetup} (provides sane defaults |
423 symbols), and the final \texttt{pdfsetup} (provides sane defaults |
426 for \texttt{hyperref}, including URL markup) --- all three are |
424 for \texttt{hyperref}, including URL markup). All three are |
427 distributed with Isabelle. Further packages may be required in |
425 distributed with Isabelle. Further packages may be required in |
428 particular applications, e.g.\ for unusual mathematical symbols. |
426 particular applications, say for unusual mathematical symbols. |
429 |
427 |
430 \medskip Any additional files for the {\LaTeX} stage go into the |
428 \medskip Any additional files for the {\LaTeX} stage go into the |
431 \texttt{MySession/document} directory as well. In particular, |
429 \texttt{MySession/document} directory as well. In particular, |
432 adding \texttt{root.bib} (with that specific name) causes an |
430 adding a file named \texttt{root.bib} causes an |
433 automatic run of \texttt{bibtex} to process a bibliographic |
431 automatic run of \texttt{bibtex} to process a bibliographic |
434 database; see also \texttt{isatool document} in \cite{isabelle-sys}. |
432 database; see also \texttt{isatool document} \cite{isabelle-sys}. |
435 |
433 |
436 \medskip Any failure of the document preparation phase in an |
434 \medskip Any failure of the document preparation phase in an |
437 Isabelle batch session leaves the generated sources in their target |
435 Isabelle batch session leaves the generated sources in their target |
438 location (as pointed out by the accompanied error message). This |
436 location, identified by the accompanying error message. This |
439 enables users to trace {\LaTeX} problems with the generated files at |
437 lets you trace {\LaTeX} problems with the generated files at |
440 hand. |
438 hand. |
441 *} |
439 *} |
442 |
440 |
443 |
441 |
444 subsection {* Structure Markup *} |
442 subsection {* Structure Markup *} |
503 theorem main: \dots |
501 theorem main: \dots |
504 |
502 |
505 end |
503 end |
506 \end{ttbox} |
504 \end{ttbox} |
507 |
505 |
508 Users may occasionally want to change the meaning of markup |
506 You may occasionally want to change the meaning of markup |
509 commands, say via \verb,\renewcommand, in \texttt{root.tex}; |
507 commands, say via \verb,\renewcommand, in \texttt{root.tex}. For example, |
510 \verb,\isamarkupheader, is a good candidate for some tuning, e.g.\ |
508 \verb,\isamarkupheader, is a good candidate for some tuning. |
511 moving it up in the hierarchy to become \verb,\chapter,. |
509 We could |
|
510 move it up in the hierarchy to become \verb,\chapter,. |
512 |
511 |
513 \begin{verbatim} |
512 \begin{verbatim} |
514 \renewcommand{\isamarkupheader}[1]{\chapter{#1}} |
513 \renewcommand{\isamarkupheader}[1]{\chapter{#1}} |
515 \end{verbatim} |
514 \end{verbatim} |
516 |
515 |
517 \noindent That particular modification requires change to the |
516 \noindent Now we must change the |
518 document class given in \texttt{root.tex} to something that supports |
517 document class given in \texttt{root.tex} to something that supports |
519 the notion of chapters in the first place, such as |
518 chapters. A suitable command is |
520 \verb,\documentclass{report},. |
519 \verb,\documentclass{report},. |
521 |
520 |
522 \medskip The {\LaTeX} macro \verb,\isabellecontext, is maintained to |
521 \medskip The {\LaTeX} macro \verb,\isabellecontext, is maintained to |
523 hold the name of the current theory context. This is particularly |
522 hold the name of the current theory context. This is particularly |
524 useful for document headings: |
523 useful for document headings: |
605 for a comma-separated list of options consisting of a $name$ or |
604 for a comma-separated list of options consisting of a $name$ or |
606 \texttt{$name$=$value$}. The syntax of $arguments$ depends on the |
605 \texttt{$name$=$value$}. The syntax of $arguments$ depends on the |
607 kind of antiquotation, it generally follows the same conventions for |
606 kind of antiquotation, it generally follows the same conventions for |
608 types, terms, or theorems as in the formal part of a theory. |
607 types, terms, or theorems as in the formal part of a theory. |
609 |
608 |
610 \medskip Here is an example of the quotation-antiquotation |
609 \medskip This sentence demonstrates quotations and antiquotations: |
611 technique: @{term "%x y. x"} is a well-typed term. |
610 @{term "%x y. x"} is a well-typed term. |
612 |
611 |
613 \medskip\noindent The above output has been produced as follows: |
612 \medskip\noindent The output above was produced as follows: |
614 \begin{ttbox} |
613 \begin{ttbox} |
615 text {\ttlbrace}* |
614 text {\ttlbrace}* |
616 Here is an example of the quotation-antiquotation technique: |
615 This sentence demonstrates quotations and antiquotations: |
617 {\at}{\ttlbrace}term "%x y. x"{\ttrbrace} is a well-typed term. |
616 {\at}{\ttlbrace}term "%x y. x"{\ttrbrace} is a well-typed term. |
618 *{\ttrbrace} |
617 *{\ttrbrace} |
619 \end{ttbox} |
618 \end{ttbox} |
620 |
619 |
621 From the notational change of the ASCII character \verb,%, to the |
620 The notational change from the ASCII character~\verb,%, to the |
622 symbol @{text \<lambda>} we see that the term really got printed by the |
621 symbol~@{text \<lambda>} reveals that Isabelle printed this term, |
623 system (after parsing and type-checking) --- document preparation |
622 after parsing and type-checking. Document preparation |
624 enables symbolic output by default. |
623 enables symbolic output by default. |
625 |
624 |
626 \medskip The next example includes an option to modify the |
625 \medskip The next example includes an option to modify Isabelle's |
627 \verb,show_types, flag of Isabelle: |
626 \verb,show_types, flag. The antiquotation |
628 \texttt{{\at}}\verb,{term [show_types] "%x y. x"}, produces @{term |
627 \texttt{{\at}}\verb,{term [show_types] "%x y. x"}, produces |
629 [show_types] "%x y. x"}. Type-inference has figured out the most |
628 the output @{term [show_types] "%x y. x"}. |
630 general typings in the present (theory) context. Note that term |
629 Type inference has figured out the most |
631 fragments may acquire different typings due to constraints imposed |
630 general typings in the present theory context. Terms |
632 by previous text (say within a proof), e.g.\ due to the main goal |
631 may acquire different typings due to constraints imposed |
633 statement given beforehand. |
632 by their environment; within a proof, for example, variables are given |
634 |
633 the same types as they have in the main goal statement. |
635 \medskip Several further kinds of antiquotations (and options) are |
634 |
|
635 \medskip Several further kinds of antiquotations and options are |
636 available \cite{isabelle-sys}. Here are a few commonly used |
636 available \cite{isabelle-sys}. Here are a few commonly used |
637 combinations: |
637 combinations: |
638 |
638 |
639 \medskip |
639 \medskip |
640 |
640 |
741 |
741 |
742 \begin{verbatim} |
742 \begin{verbatim} |
743 no_document use_thy "T"; |
743 no_document use_thy "T"; |
744 \end{verbatim} |
744 \end{verbatim} |
745 |
745 |
746 \medskip Theory output may also be suppressed in smaller portions. |
746 \medskip Theory output may be suppressed more selectively. |
747 For example, research articles, or slides usually do not include the |
747 Research articles and slides usually do not include the |
748 formal content in full. In order to delimit \bfindex{ignored |
748 formal content in full. In order to delimit \bfindex{ignored |
749 material} special source comments |
749 material}, special source comments |
750 \verb,(,\verb,*,\verb,<,\verb,*,\verb,), and |
750 \verb,(,\verb,*,\verb,<,\verb,*,\verb,), and |
751 \verb,(,\verb,*,\verb,>,\verb,*,\verb,), may be included in the |
751 \verb,(,\verb,*,\verb,>,\verb,*,\verb,), may be included in the |
752 text. Only the document preparation system is affected, the formal |
752 text. Only document preparation is affected; the formal |
753 checking of the theory is performed unchanged. |
753 checking of the theory is unchanged. |
754 |
754 |
755 In the subsequent example we suppress the slightly formalistic |
755 In this example, we suppress a theory's uninteresting |
756 \isakeyword{theory} + \isakeyword{end} surroundings a theory. |
756 \isakeyword{theory} and \isakeyword{end} brackets: |
757 |
757 |
758 \medskip |
758 \medskip |
759 |
759 |
760 \begin{tabular}{l} |
760 \begin{tabular}{l} |
761 \verb,(,\verb,*,\verb,<,\verb,*,\verb,), \\ |
761 \verb,(,\verb,*,\verb,<,\verb,*,\verb,), \\ |
784 \begin{verbatim} |
784 \begin{verbatim} |
785 by (auto(*<*)simp add: int_less_le(*>*)) |
785 by (auto(*<*)simp add: int_less_le(*>*)) |
786 \end{verbatim} |
786 \end{verbatim} |
787 %(* |
787 %(* |
788 |
788 |
789 \medskip Ignoring portions of printed text does demand some care by |
789 \medskip Suppressing portions of printed text demands care. |
790 the writer. First of all, the user is responsible not to obfuscate |
790 You should not misrepresent |
791 the underlying theory development in an unduly manner. It is fairly |
791 the underlying theory development. It is |
792 easy to invalidate the visible text, e.g.\ by referencing |
792 easy to invalidate the visible text by hiding |
793 questionable formal items (strange definitions, arbitrary axioms |
793 references to questionable axioms. |
794 etc.) that have been hidden from sight beforehand. |
|
795 |
794 |
796 Authentic reports of Isabelle/Isar theories, say as part of a |
795 Authentic reports of Isabelle/Isar theories, say as part of a |
797 library, should refrain from suppressing parts of the text at all. |
796 library, should suppress nothing. |
798 Other users may need the full information for their own derivative |
797 Other users may need the full information for their own derivative |
799 work. If a particular formalization appears inadequate for general |
798 work. If a particular formalization appears inadequate for general |
800 public coverage, it is often more appropriate to think of a better |
799 public coverage, it is often more appropriate to think of a better |
801 way in the first place. |
800 way in the first place. |
802 |
801 |
803 \medskip Some technical subtleties of the |
802 \medskip Some technical subtleties of the |
804 \verb,(,\verb,*,\verb,<,\verb,*,\verb,),~\verb,(,\verb,*,\verb,>,\verb,*,\verb,), |
803 \verb,(,\verb,*,\verb,<,\verb,*,\verb,),~\verb,(,\verb,*,\verb,>,\verb,*,\verb,), |
805 elements need to be kept in mind, too --- the system performs little |
804 elements need to be kept in mind, too --- the system performs few |
806 sanity checks here. Arguments of markup commands and formal |
805 sanity checks here. Arguments of markup commands and formal |
807 comments must not be hidden, otherwise presentation fails. Open and |
806 comments must not be hidden, otherwise presentation fails. Open and |
808 close parentheses need to be inserted carefully; it is easy to hide |
807 close parentheses need to be inserted carefully; it is easy to hide |
809 the wrong parts, especially after rearranging the theory text. |
808 the wrong parts, especially after rearranging the theory text. |
810 *} |
809 *} |