|
1 % |
|
2 \begin{isabellebody}% |
|
3 \def\isabellecontext{Documents}% |
|
4 % |
|
5 \isadelimtheory |
|
6 % |
|
7 \endisadelimtheory |
|
8 % |
|
9 \isatagtheory |
|
10 % |
|
11 \endisatagtheory |
|
12 {\isafoldtheory}% |
|
13 % |
|
14 \isadelimtheory |
|
15 % |
|
16 \endisadelimtheory |
|
17 % |
|
18 \isamarkupsection{Concrete Syntax \label{sec:concrete-syntax}% |
|
19 } |
|
20 \isamarkuptrue% |
|
21 % |
|
22 \begin{isamarkuptext}% |
|
23 The core concept of Isabelle's framework for concrete syntax is that |
|
24 of \bfindex{mixfix annotations}. Associated with any kind of |
|
25 constant declaration, mixfixes affect both the grammar productions |
|
26 for the parser and output templates for the pretty printer. |
|
27 |
|
28 In full generality, parser and pretty printer configuration is a |
|
29 subtle affair~\cite{isabelle-ref}. Your syntax specifications need |
|
30 to interact properly with the existing setup of Isabelle/Pure and |
|
31 Isabelle/HOL\@. To avoid creating ambiguities with existing |
|
32 elements, it is particularly important to give new syntactic |
|
33 constructs the right precedence. |
|
34 |
|
35 Below we introduce a few simple syntax declaration |
|
36 forms that already cover many common situations fairly well.% |
|
37 \end{isamarkuptext}% |
|
38 \isamarkuptrue% |
|
39 % |
|
40 \isamarkupsubsection{Infix Annotations% |
|
41 } |
|
42 \isamarkuptrue% |
|
43 % |
|
44 \begin{isamarkuptext}% |
|
45 Syntax annotations may be included wherever constants are declared, |
|
46 such as \isacommand{definition} and \isacommand{primrec} --- and also |
|
47 \isacommand{datatype}, which declares constructor operations. |
|
48 Type-constructors may be annotated as well, although this is less |
|
49 frequently encountered in practice (the infix type \isa{{\isaliteral{5C3C74696D65733E}{\isasymtimes}}} comes |
|
50 to mind). |
|
51 |
|
52 Infix declarations\index{infix annotations} provide a useful special |
|
53 case of mixfixes. The following example of the exclusive-or |
|
54 operation on boolean values illustrates typical infix declarations.% |
|
55 \end{isamarkuptext}% |
|
56 \isamarkuptrue% |
|
57 \isacommand{definition}\isamarkupfalse% |
|
58 \ xor\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}bool\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool{\isaliteral{22}{\isachardoublequoteclose}}\ \ \ \ {\isaliteral{28}{\isacharparenleft}}\isakeyword{infixl}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{2B}{\isacharplus}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequoteclose}}\ {\isadigit{6}}{\isadigit{0}}{\isaliteral{29}{\isacharparenright}}\isanewline |
|
59 \isakeyword{where}\ {\isaliteral{22}{\isachardoublequoteopen}}A\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{2B}{\isacharplus}}{\isaliteral{5D}{\isacharbrackright}}\ B\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ {\isaliteral{28}{\isacharparenleft}}A\ {\isaliteral{5C3C616E643E}{\isasymand}}\ {\isaliteral{5C3C6E6F743E}{\isasymnot}}\ B{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C6F723E}{\isasymor}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6E6F743E}{\isasymnot}}\ A\ {\isaliteral{5C3C616E643E}{\isasymand}}\ B{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}% |
|
60 \begin{isamarkuptext}% |
|
61 \noindent Now \isa{xor\ A\ B} and \isa{A\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{2B}{\isacharplus}}{\isaliteral{5D}{\isacharbrackright}}\ B} refer to the |
|
62 same expression internally. Any curried function with at least two |
|
63 arguments may be given infix syntax. For partial applications with |
|
64 fewer than two operands, there is a notation using the prefix~\isa{op}. For instance, \isa{xor} without arguments is represented as |
|
65 \isa{op\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{2B}{\isacharplus}}{\isaliteral{5D}{\isacharbrackright}}}; together with ordinary function application, this |
|
66 turns \isa{xor\ A} into \isa{op\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{2B}{\isacharplus}}{\isaliteral{5D}{\isacharbrackright}}\ A}. |
|
67 |
|
68 The keyword \isakeyword{infixl} seen above specifies an |
|
69 infix operator that is nested to the \emph{left}: in iterated |
|
70 applications the more complex expression appears on the left-hand |
|
71 side, and \isa{A\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{2B}{\isacharplus}}{\isaliteral{5D}{\isacharbrackright}}\ B\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{2B}{\isacharplus}}{\isaliteral{5D}{\isacharbrackright}}\ C} stands for \isa{{\isaliteral{28}{\isacharparenleft}}A\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{2B}{\isacharplus}}{\isaliteral{5D}{\isacharbrackright}}\ B{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{2B}{\isacharplus}}{\isaliteral{5D}{\isacharbrackright}}\ C}. Similarly, \isakeyword{infixr} means nesting to the |
|
72 \emph{right}, reading \isa{A\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{2B}{\isacharplus}}{\isaliteral{5D}{\isacharbrackright}}\ B\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{2B}{\isacharplus}}{\isaliteral{5D}{\isacharbrackright}}\ C} as \isa{A\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{2B}{\isacharplus}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{28}{\isacharparenleft}}B\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{2B}{\isacharplus}}{\isaliteral{5D}{\isacharbrackright}}\ C{\isaliteral{29}{\isacharparenright}}}. A \emph{non-oriented} declaration via \isakeyword{infix} |
|
73 would render \isa{A\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{2B}{\isacharplus}}{\isaliteral{5D}{\isacharbrackright}}\ B\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{2B}{\isacharplus}}{\isaliteral{5D}{\isacharbrackright}}\ C} illegal, but demand explicit |
|
74 parentheses to indicate the intended grouping. |
|
75 |
|
76 The string \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{2B}{\isacharplus}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequote}}} in our annotation refers to the |
|
77 concrete syntax to represent the operator (a literal token), while |
|
78 the number \isa{{\isadigit{6}}{\isadigit{0}}} determines the precedence of the construct: |
|
79 the syntactic priorities of the arguments and result. Isabelle/HOL |
|
80 already uses up many popular combinations of ASCII symbols for its |
|
81 own use, including both \isa{{\isaliteral{2B}{\isacharplus}}} and \isa{{\isaliteral{2B}{\isacharplus}}{\isaliteral{2B}{\isacharplus}}}. Longer |
|
82 character combinations are more likely to be still available for |
|
83 user extensions, such as our~\isa{{\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{2B}{\isacharplus}}{\isaliteral{5D}{\isacharbrackright}}}. |
|
84 |
|
85 Operator precedences have a range of 0--1000. Very low or high |
|
86 priorities are reserved for the meta-logic. HOL syntax mainly uses |
|
87 the range of 10--100: the equality infix \isa{{\isaliteral{3D}{\isacharequal}}} is centered at |
|
88 50; logical connectives (like \isa{{\isaliteral{5C3C6F723E}{\isasymor}}} and \isa{{\isaliteral{5C3C616E643E}{\isasymand}}}) are |
|
89 below 50; algebraic ones (like \isa{{\isaliteral{2B}{\isacharplus}}} and \isa{{\isaliteral{2A}{\isacharasterisk}}}) are |
|
90 above 50. User syntax should strive to coexist with common HOL |
|
91 forms, or use the mostly unused range 100--900.% |
|
92 \end{isamarkuptext}% |
|
93 \isamarkuptrue% |
|
94 % |
|
95 \isamarkupsubsection{Mathematical Symbols \label{sec:syntax-symbols}% |
|
96 } |
|
97 \isamarkuptrue% |
|
98 % |
|
99 \begin{isamarkuptext}% |
|
100 Concrete syntax based on ASCII characters has inherent limitations. |
|
101 Mathematical notation demands a larger repertoire of glyphs. |
|
102 Several standards of extended character sets have been proposed over |
|
103 decades, but none has become universally available so far. Isabelle |
|
104 has its own notion of \bfindex{symbols} as the smallest entities of |
|
105 source text, without referring to internal encodings. There are |
|
106 three kinds of such ``generalized characters'': |
|
107 |
|
108 \begin{enumerate} |
|
109 |
|
110 \item 7-bit ASCII characters |
|
111 |
|
112 \item named symbols: \verb,\,\verb,<,$ident$\verb,>, |
|
113 |
|
114 \item named control symbols: \verb,\,\verb,<^,$ident$\verb,>, |
|
115 |
|
116 \end{enumerate} |
|
117 |
|
118 Here $ident$ is any sequence of letters. |
|
119 This results in an infinite store of symbols, whose |
|
120 interpretation is left to further front-end tools. For example, the |
|
121 user-interface of Proof~General + X-Symbol and the Isabelle document |
|
122 processor (see \S\ref{sec:document-preparation}) display the |
|
123 \verb,\,\verb,<forall>, symbol as~\isa{{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}}. |
|
124 |
|
125 A list of standard Isabelle symbols is given in |
|
126 \cite{isabelle-isar-ref}. You may introduce your own |
|
127 interpretation of further symbols by configuring the appropriate |
|
128 front-end tool accordingly, e.g.\ by defining certain {\LaTeX} |
|
129 macros (see also \S\ref{sec:doc-prep-symbols}). There are also a |
|
130 few predefined control symbols, such as \verb,\,\verb,<^sub>, and |
|
131 \verb,\,\verb,<^sup>, for sub- and superscript of the subsequent |
|
132 printable symbol, respectively. For example, \verb,A\<^sup>\<star>, is |
|
133 output as \isa{A\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{5C3C737461723E}{\isasymstar}}}. |
|
134 |
|
135 A number of symbols are considered letters by the Isabelle lexer and |
|
136 can be used as part of identifiers. These are the greek letters |
|
137 \isa{{\isaliteral{5C3C616C7068613E}{\isasymalpha}}} (\verb+\+\verb+<alpha>+), \isa{{\isaliteral{5C3C626574613E}{\isasymbeta}}} |
|
138 (\verb+\+\verb+<beta>+), etc. (excluding \isa{{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}}), |
|
139 special letters like \isa{{\isaliteral{5C3C413E}{\isasymA}}} (\verb+\+\verb+<A>+) and \isa{{\isaliteral{5C3C41413E}{\isasymAA}}} (\verb+\+\verb+<AA>+), and the control symbols |
|
140 \verb+\+\verb+<^isub>+ and \verb+\+\verb+<^isup>+ for single letter |
|
141 sub and super scripts. This means that the input |
|
142 |
|
143 \medskip |
|
144 {\small\noindent \verb,\,\verb,<forall>\,\verb,<alpha>\<^isub>1.,~\verb,\,\verb,<alpha>\<^isub>1 = \,\verb,<Pi>\<^isup>\<A>,} |
|
145 |
|
146 \medskip |
|
147 \noindent is recognized as the term \isa{{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5C3C50693E}{\isasymPi}}\isaliteral{5C3C5E697375703E}{}\isactrlisup {\isaliteral{5C3C413E}{\isasymA}}} |
|
148 by Isabelle. Note that \isa{{\isaliteral{5C3C50693E}{\isasymPi}}\isaliteral{5C3C5E697375703E}{}\isactrlisup {\isaliteral{5C3C413E}{\isasymA}}} is a single |
|
149 syntactic entity, not an exponentiation. |
|
150 |
|
151 Replacing our previous definition of \isa{xor} by the |
|
152 following specifies an Isabelle symbol for the new operator:% |
|
153 \end{isamarkuptext}% |
|
154 \isamarkuptrue% |
|
155 % |
|
156 \isadelimML |
|
157 % |
|
158 \endisadelimML |
|
159 % |
|
160 \isatagML |
|
161 % |
|
162 \endisatagML |
|
163 {\isafoldML}% |
|
164 % |
|
165 \isadelimML |
|
166 % |
|
167 \endisadelimML |
|
168 \isacommand{definition}\isamarkupfalse% |
|
169 \ xor\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}bool\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool{\isaliteral{22}{\isachardoublequoteclose}}\ \ \ \ {\isaliteral{28}{\isacharparenleft}}\isakeyword{infixl}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6F706C75733E}{\isasymoplus}}{\isaliteral{22}{\isachardoublequoteclose}}\ {\isadigit{6}}{\isadigit{0}}{\isaliteral{29}{\isacharparenright}}\isanewline |
|
170 \isakeyword{where}\ {\isaliteral{22}{\isachardoublequoteopen}}A\ {\isaliteral{5C3C6F706C75733E}{\isasymoplus}}\ B\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ {\isaliteral{28}{\isacharparenleft}}A\ {\isaliteral{5C3C616E643E}{\isasymand}}\ {\isaliteral{5C3C6E6F743E}{\isasymnot}}\ B{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C6F723E}{\isasymor}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6E6F743E}{\isasymnot}}\ A\ {\isaliteral{5C3C616E643E}{\isasymand}}\ B{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}% |
|
171 \isadelimML |
|
172 % |
|
173 \endisadelimML |
|
174 % |
|
175 \isatagML |
|
176 % |
|
177 \endisatagML |
|
178 {\isafoldML}% |
|
179 % |
|
180 \isadelimML |
|
181 % |
|
182 \endisadelimML |
|
183 % |
|
184 \begin{isamarkuptext}% |
|
185 \noindent Proof~General provides several input methods to enter |
|
186 \isa{{\isaliteral{5C3C6F706C75733E}{\isasymoplus}}} in the text. If all fails one may just type a named |
|
187 entity \verb,\,\verb,<oplus>, by hand; the corresponding symbol will |
|
188 be displayed after further input. |
|
189 |
|
190 More flexible is to provide alternative syntax forms |
|
191 through the \bfindex{print mode} concept~\cite{isabelle-ref}. By |
|
192 convention, the mode of ``$xsymbols$'' is enabled whenever |
|
193 Proof~General's X-Symbol mode or {\LaTeX} output is active. Now |
|
194 consider the following hybrid declaration of \isa{xor}:% |
|
195 \end{isamarkuptext}% |
|
196 \isamarkuptrue% |
|
197 % |
|
198 \isadelimML |
|
199 % |
|
200 \endisadelimML |
|
201 % |
|
202 \isatagML |
|
203 % |
|
204 \endisatagML |
|
205 {\isafoldML}% |
|
206 % |
|
207 \isadelimML |
|
208 % |
|
209 \endisadelimML |
|
210 \isacommand{definition}\isamarkupfalse% |
|
211 \ xor\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}bool\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool{\isaliteral{22}{\isachardoublequoteclose}}\ \ \ \ {\isaliteral{28}{\isacharparenleft}}\isakeyword{infixl}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{2B}{\isacharplus}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{5C3C69676E6F72653E}{\isasymignore}}{\isaliteral{22}{\isachardoublequoteclose}}\ {\isadigit{6}}{\isadigit{0}}{\isaliteral{29}{\isacharparenright}}\isanewline |
|
212 \isakeyword{where}\ {\isaliteral{22}{\isachardoublequoteopen}}A\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{2B}{\isacharplus}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{5C3C69676E6F72653E}{\isasymignore}}\ B\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ {\isaliteral{28}{\isacharparenleft}}A\ {\isaliteral{5C3C616E643E}{\isasymand}}\ {\isaliteral{5C3C6E6F743E}{\isasymnot}}\ B{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C6F723E}{\isasymor}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6E6F743E}{\isasymnot}}\ A\ {\isaliteral{5C3C616E643E}{\isasymand}}\ B{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
|
213 \isanewline |
|
214 \isacommand{notation}\isamarkupfalse% |
|
215 \ {\isaliteral{28}{\isacharparenleft}}xsymbols{\isaliteral{29}{\isacharparenright}}\ xor\ {\isaliteral{28}{\isacharparenleft}}\isakeyword{infixl}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6F706C75733E}{\isasymoplus}}{\isaliteral{5C3C69676E6F72653E}{\isasymignore}}{\isaliteral{22}{\isachardoublequoteclose}}\ {\isadigit{6}}{\isadigit{0}}{\isaliteral{29}{\isacharparenright}}% |
|
216 \isadelimML |
|
217 % |
|
218 \endisadelimML |
|
219 % |
|
220 \isatagML |
|
221 % |
|
222 \endisatagML |
|
223 {\isafoldML}% |
|
224 % |
|
225 \isadelimML |
|
226 % |
|
227 \endisadelimML |
|
228 % |
|
229 \begin{isamarkuptext}% |
|
230 \noindent |
|
231 The \commdx{notation} command associates a mixfix |
|
232 annotation with a known constant. The print mode specification, |
|
233 here \isa{{\isaliteral{28}{\isacharparenleft}}xsymbols{\isaliteral{29}{\isacharparenright}}}, is optional. |
|
234 |
|
235 We may now write \isa{A\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{2B}{\isacharplus}}{\isaliteral{5D}{\isacharbrackright}}\ B} or \isa{A\ {\isaliteral{5C3C6F706C75733E}{\isasymoplus}}\ B} in input, while |
|
236 output uses the nicer syntax of $xsymbols$ whenever that print mode is |
|
237 active. Such an arrangement is particularly useful for interactive |
|
238 development, where users may type ASCII text and see mathematical |
|
239 symbols displayed during proofs.% |
|
240 \end{isamarkuptext}% |
|
241 \isamarkuptrue% |
|
242 % |
|
243 \isamarkupsubsection{Prefix Annotations% |
|
244 } |
|
245 \isamarkuptrue% |
|
246 % |
|
247 \begin{isamarkuptext}% |
|
248 Prefix syntax annotations\index{prefix annotation} are another form |
|
249 of mixfixes \cite{isabelle-ref}, without any template arguments or |
|
250 priorities --- just some literal syntax. The following example |
|
251 associates common symbols with the constructors of a datatype.% |
|
252 \end{isamarkuptext}% |
|
253 \isamarkuptrue% |
|
254 \isacommand{datatype}\isamarkupfalse% |
|
255 \ currency\ {\isaliteral{3D}{\isacharequal}}\isanewline |
|
256 \ \ \ \ Euro\ nat\ \ \ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6575726F3E}{\isasymeuro}}{\isaliteral{22}{\isachardoublequoteclose}}{\isaliteral{29}{\isacharparenright}}\isanewline |
|
257 \ \ {\isaliteral{7C}{\isacharbar}}\ Pounds\ nat\ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C706F756E64733E}{\isasympounds}}{\isaliteral{22}{\isachardoublequoteclose}}{\isaliteral{29}{\isacharparenright}}\isanewline |
|
258 \ \ {\isaliteral{7C}{\isacharbar}}\ Yen\ nat\ \ \ \ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C79656E3E}{\isasymyen}}{\isaliteral{22}{\isachardoublequoteclose}}{\isaliteral{29}{\isacharparenright}}\isanewline |
|
259 \ \ {\isaliteral{7C}{\isacharbar}}\ Dollar\ nat\ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{24}{\isachardollar}}{\isaliteral{22}{\isachardoublequoteclose}}{\isaliteral{29}{\isacharparenright}}% |
|
260 \begin{isamarkuptext}% |
|
261 \noindent Here the mixfix annotations on the rightmost column happen |
|
262 to consist of a single Isabelle symbol each: \verb,\,\verb,<euro>,, |
|
263 \verb,\,\verb,<pounds>,, \verb,\,\verb,<yen>,, and \verb,$,. Recall |
|
264 that a constructor like \isa{Euro} actually is a function \isa{nat\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ currency}. The expression \isa{Euro\ {\isadigit{1}}{\isadigit{0}}} will be |
|
265 printed as \isa{{\isaliteral{5C3C6575726F3E}{\isasymeuro}}\ {\isadigit{1}}{\isadigit{0}}}; only the head of the application is |
|
266 subject to our concrete syntax. This rather simple form already |
|
267 achieves conformance with notational standards of the European |
|
268 Commission. |
|
269 |
|
270 Prefix syntax works the same way for other commands that introduce new constants, e.g. \isakeyword{primrec}.% |
|
271 \end{isamarkuptext}% |
|
272 \isamarkuptrue% |
|
273 % |
|
274 \isamarkupsubsection{Abbreviations \label{sec:abbreviations}% |
|
275 } |
|
276 \isamarkuptrue% |
|
277 % |
|
278 \begin{isamarkuptext}% |
|
279 Mixfix syntax annotations merely decorate particular constant |
|
280 application forms with concrete syntax, for instance replacing |
|
281 \isa{xor\ A\ B} by \isa{A\ {\isaliteral{5C3C6F706C75733E}{\isasymoplus}}\ B}. Occasionally, the relationship |
|
282 between some piece of notation and its internal form is more |
|
283 complicated. Here we need \emph{abbreviations}. |
|
284 |
|
285 Command \commdx{abbreviation} introduces an uninterpreted notational |
|
286 constant as an abbreviation for a complex term. Abbreviations are |
|
287 unfolded upon parsing and re-introduced upon printing. This provides a |
|
288 simple mechanism for syntactic macros. |
|
289 |
|
290 A typical use of abbreviations is to introduce relational notation for |
|
291 membership in a set of pairs, replacing \isa{{\isaliteral{28}{\isacharparenleft}}x{\isaliteral{2C}{\isacharcomma}}\ y{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ sim} by |
|
292 \isa{x\ {\isaliteral{5C3C617070726F783E}{\isasymapprox}}\ y}. We assume that a constant \isa{sim} of type |
|
293 \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ {\isaliteral{27}{\isacharprime}}a{\isaliteral{29}{\isacharparenright}}\ set} has been introduced at this point.% |
|
294 \end{isamarkuptext}% |
|
295 \isamarkuptrue% |
|
296 \isacommand{abbreviation}\isamarkupfalse% |
|
297 \ sim{\isadigit{2}}\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool{\isaliteral{22}{\isachardoublequoteclose}}\ \ \ {\isaliteral{28}{\isacharparenleft}}\isakeyword{infix}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C617070726F783E}{\isasymapprox}}{\isaliteral{22}{\isachardoublequoteclose}}\ {\isadigit{5}}{\isadigit{0}}{\isaliteral{29}{\isacharparenright}}\isanewline |
|
298 \isakeyword{where}\ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{5C3C617070726F783E}{\isasymapprox}}\ y\ \ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ \ {\isaliteral{28}{\isacharparenleft}}x{\isaliteral{2C}{\isacharcomma}}\ y{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ sim{\isaliteral{22}{\isachardoublequoteclose}}% |
|
299 \begin{isamarkuptext}% |
|
300 \noindent The given meta-equality is used as a rewrite rule |
|
301 after parsing (replacing \mbox{\isa{x\ {\isaliteral{5C3C617070726F783E}{\isasymapprox}}\ y}} by \isa{{\isaliteral{28}{\isacharparenleft}}x{\isaliteral{2C}{\isacharcomma}}y{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ sim}) and before printing (turning \isa{{\isaliteral{28}{\isacharparenleft}}x{\isaliteral{2C}{\isacharcomma}}y{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ sim} back into |
|
302 \mbox{\isa{x\ {\isaliteral{5C3C617070726F783E}{\isasymapprox}}\ y}}). The name of the dummy constant \isa{sim{\isadigit{2}}} |
|
303 does not matter, as long as it is unique. |
|
304 |
|
305 Another common application of abbreviations is to |
|
306 provide variant versions of fundamental relational expressions, such |
|
307 as \isa{{\isaliteral{5C3C6E6F7465713E}{\isasymnoteq}}} for negated equalities. The following declaration |
|
308 stems from Isabelle/HOL itself:% |
|
309 \end{isamarkuptext}% |
|
310 \isamarkuptrue% |
|
311 \isacommand{abbreviation}\isamarkupfalse% |
|
312 \ not{\isaliteral{5F}{\isacharunderscore}}equal\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool{\isaliteral{22}{\isachardoublequoteclose}}\ \ \ \ {\isaliteral{28}{\isacharparenleft}}\isakeyword{infixl}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{7E}{\isachartilde}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{5C3C69676E6F72653E}{\isasymignore}}{\isaliteral{22}{\isachardoublequoteclose}}\ {\isadigit{5}}{\isadigit{0}}{\isaliteral{29}{\isacharparenright}}\isanewline |
|
313 \isakeyword{where}\ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{7E}{\isachartilde}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{5C3C69676E6F72653E}{\isasymignore}}\ y\ \ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ \ {\isaliteral{5C3C6E6F743E}{\isasymnot}}\ {\isaliteral{28}{\isacharparenleft}}x\ {\isaliteral{3D}{\isacharequal}}\ y{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
|
314 \isanewline |
|
315 \isacommand{notation}\isamarkupfalse% |
|
316 \ {\isaliteral{28}{\isacharparenleft}}xsymbols{\isaliteral{29}{\isacharparenright}}\ not{\isaliteral{5F}{\isacharunderscore}}equal\ {\isaliteral{28}{\isacharparenleft}}\isakeyword{infix}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6E6F7465713E}{\isasymnoteq}}{\isaliteral{5C3C69676E6F72653E}{\isasymignore}}{\isaliteral{22}{\isachardoublequoteclose}}\ {\isadigit{5}}{\isadigit{0}}{\isaliteral{29}{\isacharparenright}}% |
|
317 \begin{isamarkuptext}% |
|
318 \noindent The notation \isa{{\isaliteral{5C3C6E6F7465713E}{\isasymnoteq}}} is introduced separately to restrict it |
|
319 to the \emph{xsymbols} mode. |
|
320 |
|
321 Abbreviations are appropriate when the defined concept is a |
|
322 simple variation on an existing one. But because of the automatic |
|
323 folding and unfolding of abbreviations, they do not scale up well to |
|
324 large hierarchies of concepts. Abbreviations do not replace |
|
325 definitions. |
|
326 |
|
327 Abbreviations are a simplified form of the general concept of |
|
328 \emph{syntax translations}; even heavier transformations may be |
|
329 written in ML \cite{isabelle-ref}.% |
|
330 \end{isamarkuptext}% |
|
331 \isamarkuptrue% |
|
332 % |
|
333 \isamarkupsection{Document Preparation \label{sec:document-preparation}% |
|
334 } |
|
335 \isamarkuptrue% |
|
336 % |
|
337 \begin{isamarkuptext}% |
|
338 Isabelle/Isar is centered around the concept of \bfindex{formal |
|
339 proof documents}\index{documents|bold}. The outcome of a formal |
|
340 development effort is meant to be a human-readable record, presented |
|
341 as browsable PDF file or printed on paper. The overall document |
|
342 structure follows traditional mathematical articles, with sections, |
|
343 intermediate explanations, definitions, theorems and proofs. |
|
344 |
|
345 \medskip The Isabelle document preparation system essentially acts |
|
346 as a front-end to {\LaTeX}. After checking specifications and |
|
347 proofs formally, the theory sources are turned into typesetting |
|
348 instructions in a schematic manner. This lets you write authentic |
|
349 reports on theory developments with little effort: many technical |
|
350 consistency checks are handled by the system. |
|
351 |
|
352 Here is an example to illustrate the idea of Isabelle document |
|
353 preparation.% |
|
354 \end{isamarkuptext}% |
|
355 \isamarkuptrue% |
|
356 % |
|
357 \begin{quotation} |
|
358 % |
|
359 \begin{isamarkuptext}% |
|
360 The following datatype definition of \isa{{\isaliteral{27}{\isacharprime}}a\ bintree} models |
|
361 binary trees with nodes being decorated by elements of type \isa{{\isaliteral{27}{\isacharprime}}a}.% |
|
362 \end{isamarkuptext}% |
|
363 \isamarkuptrue% |
|
364 \isacommand{datatype}\isamarkupfalse% |
|
365 \ {\isaliteral{27}{\isacharprime}}a\ bintree\ {\isaliteral{3D}{\isacharequal}}\isanewline |
|
366 \ \ \ \ \ Leaf\ {\isaliteral{7C}{\isacharbar}}\ Branch\ {\isaliteral{27}{\isacharprime}}a\ \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}a\ bintree{\isaliteral{22}{\isachardoublequoteclose}}\ \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}a\ bintree{\isaliteral{22}{\isachardoublequoteclose}}% |
|
367 \begin{isamarkuptext}% |
|
368 \noindent The datatype induction rule generated here is of the form |
|
369 \begin{isabelle}% |
|
370 \ {\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}P\ Leaf{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
|
371 \isaindent{\ \ }{\isaliteral{5C3C416E643E}{\isasymAnd}}a\ bintree{\isadigit{1}}\ bintree{\isadigit{2}}{\isaliteral{2E}{\isachardot}}\isanewline |
|
372 \isaindent{\ \ \ \ \ }{\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}P\ bintree{\isadigit{1}}{\isaliteral{3B}{\isacharsemicolon}}\ P\ bintree{\isadigit{2}}{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ P\ {\isaliteral{28}{\isacharparenleft}}Branch\ a\ bintree{\isadigit{1}}\ bintree{\isadigit{2}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\isanewline |
|
373 \isaindent{\ }{\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ P\ bintree% |
|
374 \end{isabelle}% |
|
375 \end{isamarkuptext}% |
|
376 \isamarkuptrue% |
|
377 % |
|
378 \end{quotation} |
|
379 % |
|
380 \begin{isamarkuptext}% |
|
381 \noindent The above document output has been produced as follows: |
|
382 |
|
383 \begin{ttbox} |
|
384 text {\ttlbrace}* |
|
385 The following datatype definition of {\at}{\ttlbrace}text "'a bintree"{\ttrbrace} |
|
386 models binary trees with nodes being decorated by elements |
|
387 of type {\at}{\ttlbrace}typ 'a{\ttrbrace}. |
|
388 *{\ttrbrace} |
|
389 |
|
390 datatype 'a bintree = |
|
391 Leaf | Branch 'a "'a bintree" "'a bintree" |
|
392 \end{ttbox} |
|
393 \begin{ttbox} |
|
394 text {\ttlbrace}* |
|
395 {\ttback}noindent The datatype induction rule generated here is |
|
396 of the form {\at}{\ttlbrace}thm [display] bintree.induct [no_vars]{\ttrbrace} |
|
397 *{\ttrbrace} |
|
398 \end{ttbox}\vspace{-\medskipamount} |
|
399 |
|
400 \noindent Here we have augmented the theory by formal comments |
|
401 (using \isakeyword{text} blocks), the informal parts may again refer |
|
402 to formal entities by means of ``antiquotations'' (such as |
|
403 \texttt{\at}\verb,{text "'a bintree"}, or |
|
404 \texttt{\at}\verb,{typ 'a},), see also \S\ref{sec:doc-prep-text}.% |
|
405 \end{isamarkuptext}% |
|
406 \isamarkuptrue% |
|
407 % |
|
408 \isamarkupsubsection{Isabelle Sessions% |
|
409 } |
|
410 \isamarkuptrue% |
|
411 % |
|
412 \begin{isamarkuptext}% |
|
413 In contrast to the highly interactive mode of Isabelle/Isar theory |
|
414 development, the document preparation stage essentially works in |
|
415 batch-mode. An Isabelle \bfindex{session} consists of a collection |
|
416 of source files that may contribute to an output document. Each |
|
417 session is derived from a single parent, usually an object-logic |
|
418 image like \texttt{HOL}. This results in an overall tree structure, |
|
419 which is reflected by the output location in the file system |
|
420 (usually rooted at \verb,~/.isabelle/IsabelleXXXX/browser_info,). |
|
421 |
|
422 \medskip The easiest way to manage Isabelle sessions is via |
|
423 \texttt{isabelle mkdir} (generates an initial session source setup) |
|
424 and \texttt{isabelle make} (run sessions controlled by |
|
425 \texttt{IsaMakefile}). For example, a new session |
|
426 \texttt{MySession} derived from \texttt{HOL} may be produced as |
|
427 follows: |
|
428 |
|
429 \begin{verbatim} |
|
430 isabelle mkdir HOL MySession |
|
431 isabelle make |
|
432 \end{verbatim} |
|
433 |
|
434 The \texttt{isabelle make} job also informs about the file-system |
|
435 location of the ultimate results. The above dry run should be able |
|
436 to produce some \texttt{document.pdf} (with dummy title, empty table |
|
437 of contents etc.). Any failure at this stage usually indicates |
|
438 technical problems of the {\LaTeX} installation. |
|
439 |
|
440 \medskip The detailed arrangement of the session sources is as |
|
441 follows. |
|
442 |
|
443 \begin{itemize} |
|
444 |
|
445 \item Directory \texttt{MySession} holds the required theory files |
|
446 $T@1$\texttt{.thy}, \dots, $T@n$\texttt{.thy}. |
|
447 |
|
448 \item File \texttt{MySession/ROOT.ML} holds appropriate ML commands |
|
449 for loading all wanted theories, usually just |
|
450 ``\texttt{use_thy"$T@i$";}'' for any $T@i$ in leaf position of the |
|
451 dependency graph. |
|
452 |
|
453 \item Directory \texttt{MySession/document} contains everything |
|
454 required for the {\LaTeX} stage; only \texttt{root.tex} needs to be |
|
455 provided initially. |
|
456 |
|
457 The latter file holds appropriate {\LaTeX} code to commence a |
|
458 document (\verb,\documentclass, etc.), and to include the generated |
|
459 files $T@i$\texttt{.tex} for each theory. Isabelle will generate a |
|
460 file \texttt{session.tex} holding {\LaTeX} commands to include all |
|
461 generated theory output files in topologically sorted order, so |
|
462 \verb,\input{session}, in the body of \texttt{root.tex} does the job |
|
463 in most situations. |
|
464 |
|
465 \item \texttt{IsaMakefile} holds appropriate dependencies and |
|
466 invocations of Isabelle tools to control the batch job. In fact, |
|
467 several sessions may be managed by the same \texttt{IsaMakefile}. |
|
468 See the \emph{Isabelle System Manual} \cite{isabelle-sys} |
|
469 for further details, especially on |
|
470 \texttt{isabelle usedir} and \texttt{isabelle make}. |
|
471 |
|
472 \end{itemize} |
|
473 |
|
474 One may now start to populate the directory \texttt{MySession}, and |
|
475 the file \texttt{MySession/ROOT.ML} accordingly. The file |
|
476 \texttt{MySession/document/root.tex} should also be adapted at some |
|
477 point; the default version is mostly self-explanatory. Note that |
|
478 \verb,\isabellestyle, enables fine-tuning of the general appearance |
|
479 of characters and mathematical symbols (see also |
|
480 \S\ref{sec:doc-prep-symbols}). |
|
481 |
|
482 Especially observe the included {\LaTeX} packages \texttt{isabelle} |
|
483 (mandatory), \texttt{isabellesym} (required for mathematical |
|
484 symbols), and the final \texttt{pdfsetup} (provides sane defaults |
|
485 for \texttt{hyperref}, including URL markup). All three are |
|
486 distributed with Isabelle. Further packages may be required in |
|
487 particular applications, say for unusual mathematical symbols. |
|
488 |
|
489 \medskip Any additional files for the {\LaTeX} stage go into the |
|
490 \texttt{MySession/document} directory as well. In particular, |
|
491 adding a file named \texttt{root.bib} causes an automatic run of |
|
492 \texttt{bibtex} to process a bibliographic database; see also |
|
493 \texttt{isabelle document} \cite{isabelle-sys}. |
|
494 |
|
495 \medskip Any failure of the document preparation phase in an |
|
496 Isabelle batch session leaves the generated sources in their target |
|
497 location, identified by the accompanying error message. This lets |
|
498 you trace {\LaTeX} problems with the generated files at hand.% |
|
499 \end{isamarkuptext}% |
|
500 \isamarkuptrue% |
|
501 % |
|
502 \isamarkupsubsection{Structure Markup% |
|
503 } |
|
504 \isamarkuptrue% |
|
505 % |
|
506 \begin{isamarkuptext}% |
|
507 The large-scale structure of Isabelle documents follows existing |
|
508 {\LaTeX} conventions, with chapters, sections, subsubsections etc. |
|
509 The Isar language includes separate \bfindex{markup commands}, which |
|
510 do not affect the formal meaning of a theory (or proof), but result |
|
511 in corresponding {\LaTeX} elements. |
|
512 |
|
513 There are separate markup commands depending on the textual context: |
|
514 in header position (just before \isakeyword{theory}), within the |
|
515 theory body, or within a proof. The header needs to be treated |
|
516 specially here, since ordinary theory and proof commands may only |
|
517 occur \emph{after} the initial \isakeyword{theory} specification. |
|
518 |
|
519 \medskip |
|
520 |
|
521 \begin{tabular}{llll} |
|
522 header & theory & proof & default meaning \\\hline |
|
523 & \commdx{chapter} & & \verb,\chapter, \\ |
|
524 \commdx{header} & \commdx{section} & \commdx{sect} & \verb,\section, \\ |
|
525 & \commdx{subsection} & \commdx{subsect} & \verb,\subsection, \\ |
|
526 & \commdx{subsubsection} & \commdx{subsubsect} & \verb,\subsubsection, \\ |
|
527 \end{tabular} |
|
528 |
|
529 \medskip |
|
530 |
|
531 From the Isabelle perspective, each markup command takes a single |
|
532 $text$ argument (delimited by \verb,",~\isa{{\isaliteral{5C3C646F74733E}{\isasymdots}}}~\verb,", or |
|
533 \verb,{,\verb,*,~\isa{{\isaliteral{5C3C646F74733E}{\isasymdots}}}~\verb,*,\verb,},). After stripping any |
|
534 surrounding white space, the argument is passed to a {\LaTeX} macro |
|
535 \verb,\isamarkupXYZ, for command \isakeyword{XYZ}. These macros are |
|
536 defined in \verb,isabelle.sty, according to the meaning given in the |
|
537 rightmost column above. |
|
538 |
|
539 \medskip The following source fragment illustrates structure markup |
|
540 of a theory. Note that {\LaTeX} labels may be included inside of |
|
541 section headings as well. |
|
542 |
|
543 \begin{ttbox} |
|
544 header {\ttlbrace}* Some properties of Foo Bar elements *{\ttrbrace} |
|
545 |
|
546 theory Foo_Bar |
|
547 imports Main |
|
548 begin |
|
549 |
|
550 subsection {\ttlbrace}* Basic definitions *{\ttrbrace} |
|
551 |
|
552 definition foo :: \dots |
|
553 |
|
554 definition bar :: \dots |
|
555 |
|
556 subsection {\ttlbrace}* Derived rules *{\ttrbrace} |
|
557 |
|
558 lemma fooI: \dots |
|
559 lemma fooE: \dots |
|
560 |
|
561 subsection {\ttlbrace}* Main theorem {\ttback}label{\ttlbrace}sec:main-theorem{\ttrbrace} *{\ttrbrace} |
|
562 |
|
563 theorem main: \dots |
|
564 |
|
565 end |
|
566 \end{ttbox}\vspace{-\medskipamount} |
|
567 |
|
568 You may occasionally want to change the meaning of markup commands, |
|
569 say via \verb,\renewcommand, in \texttt{root.tex}. For example, |
|
570 \verb,\isamarkupheader, is a good candidate for some tuning. We |
|
571 could move it up in the hierarchy to become \verb,\chapter,. |
|
572 |
|
573 \begin{verbatim} |
|
574 \renewcommand{\isamarkupheader}[1]{\chapter{#1}} |
|
575 \end{verbatim} |
|
576 |
|
577 \noindent Now we must change the document class given in |
|
578 \texttt{root.tex} to something that supports chapters. A suitable |
|
579 command is \verb,\documentclass{report},. |
|
580 |
|
581 \medskip The {\LaTeX} macro \verb,\isabellecontext, is maintained to |
|
582 hold the name of the current theory context. This is particularly |
|
583 useful for document headings: |
|
584 |
|
585 \begin{verbatim} |
|
586 \renewcommand{\isamarkupheader}[1] |
|
587 {\chapter{#1}\markright{THEORY~\isabellecontext}} |
|
588 \end{verbatim} |
|
589 |
|
590 \noindent Make sure to include something like |
|
591 \verb,\pagestyle{headings}, in \texttt{root.tex}; the document |
|
592 should have more than two pages to show the effect.% |
|
593 \end{isamarkuptext}% |
|
594 \isamarkuptrue% |
|
595 % |
|
596 \isamarkupsubsection{Formal Comments and Antiquotations \label{sec:doc-prep-text}% |
|
597 } |
|
598 \isamarkuptrue% |
|
599 % |
|
600 \begin{isamarkuptext}% |
|
601 Isabelle \bfindex{source comments}, which are of the form |
|
602 \verb,(,\verb,*,~\isa{{\isaliteral{5C3C646F74733E}{\isasymdots}}}~\verb,*,\verb,),, essentially act like |
|
603 white space and do not really contribute to the content. They |
|
604 mainly serve technical purposes to mark certain oddities in the raw |
|
605 input text. In contrast, \bfindex{formal comments} are portions of |
|
606 text that are associated with formal Isabelle/Isar commands |
|
607 (\bfindex{marginal comments}), or as standalone paragraphs within a |
|
608 theory or proof context (\bfindex{text blocks}). |
|
609 |
|
610 \medskip Marginal comments are part of each command's concrete |
|
611 syntax \cite{isabelle-ref}; the common form is ``\verb,--,~$text$'' |
|
612 where $text$ is delimited by \verb,",\isa{{\isaliteral{5C3C646F74733E}{\isasymdots}}}\verb,", or |
|
613 \verb,{,\verb,*,~\isa{{\isaliteral{5C3C646F74733E}{\isasymdots}}}~\verb,*,\verb,}, as before. Multiple |
|
614 marginal comments may be given at the same time. Here is a simple |
|
615 example:% |
|
616 \end{isamarkuptext}% |
|
617 \isamarkuptrue% |
|
618 \isacommand{lemma}\isamarkupfalse% |
|
619 \ {\isaliteral{22}{\isachardoublequoteopen}}A\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ A{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
|
620 \ \ % |
|
621 \isamarkupcmt{a triviality of propositional logic% |
|
622 } |
|
623 \isanewline |
|
624 \ \ % |
|
625 \isamarkupcmt{(should not really bother)% |
|
626 } |
|
627 \isanewline |
|
628 % |
|
629 \isadelimproof |
|
630 \ \ % |
|
631 \endisadelimproof |
|
632 % |
|
633 \isatagproof |
|
634 \isacommand{by}\isamarkupfalse% |
|
635 \ {\isaliteral{28}{\isacharparenleft}}rule\ impI{\isaliteral{29}{\isacharparenright}}\ % |
|
636 \isamarkupcmt{implicit assumption step involved here% |
|
637 } |
|
638 % |
|
639 \endisatagproof |
|
640 {\isafoldproof}% |
|
641 % |
|
642 \isadelimproof |
|
643 % |
|
644 \endisadelimproof |
|
645 % |
|
646 \begin{isamarkuptext}% |
|
647 \noindent The above output has been produced as follows: |
|
648 |
|
649 \begin{verbatim} |
|
650 lemma "A --> A" |
|
651 -- "a triviality of propositional logic" |
|
652 -- "(should not really bother)" |
|
653 by (rule impI) -- "implicit assumption step involved here" |
|
654 \end{verbatim} |
|
655 |
|
656 From the {\LaTeX} viewpoint, ``\verb,--,'' acts like a markup |
|
657 command, associated with the macro \verb,\isamarkupcmt, (taking a |
|
658 single argument). |
|
659 |
|
660 \medskip Text blocks are introduced by the commands \bfindex{text} |
|
661 and \bfindex{txt}, for theory and proof contexts, respectively. |
|
662 Each takes again a single $text$ argument, which is interpreted as a |
|
663 free-form paragraph in {\LaTeX} (surrounded by some additional |
|
664 vertical space). This behavior may be changed by redefining the |
|
665 {\LaTeX} environments of \verb,isamarkuptext, or |
|
666 \verb,isamarkuptxt,, respectively (via \verb,\renewenvironment,) The |
|
667 text style of the body is determined by \verb,\isastyletext, and |
|
668 \verb,\isastyletxt,; the default setup uses a smaller font within |
|
669 proofs. This may be changed as follows: |
|
670 |
|
671 \begin{verbatim} |
|
672 \renewcommand{\isastyletxt}{\isastyletext} |
|
673 \end{verbatim} |
|
674 |
|
675 \medskip The $text$ part of Isabelle markup commands essentially |
|
676 inserts \emph{quoted material} into a formal text, mainly for |
|
677 instruction of the reader. An \bfindex{antiquotation} is again a |
|
678 formal object embedded into such an informal portion. The |
|
679 interpretation of antiquotations is limited to some well-formedness |
|
680 checks, with the result being pretty printed to the resulting |
|
681 document. Quoted text blocks together with antiquotations provide |
|
682 an attractive means of referring to formal entities, with good |
|
683 confidence in getting the technical details right (especially syntax |
|
684 and types). |
|
685 |
|
686 The general syntax of antiquotations is as follows: |
|
687 \texttt{{\at}{\ttlbrace}$name$ $arguments${\ttrbrace}}, or |
|
688 \texttt{{\at}{\ttlbrace}$name$ [$options$] $arguments${\ttrbrace}} |
|
689 for a comma-separated list of options consisting of a $name$ or |
|
690 \texttt{$name$=$value$} each. The syntax of $arguments$ depends on |
|
691 the kind of antiquotation, it generally follows the same conventions |
|
692 for types, terms, or theorems as in the formal part of a theory. |
|
693 |
|
694 \medskip This sentence demonstrates quotations and antiquotations: |
|
695 \isa{{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}x\ y{\isaliteral{2E}{\isachardot}}\ x} is a well-typed term. |
|
696 |
|
697 \medskip\noindent The output above was produced as follows: |
|
698 \begin{ttbox} |
|
699 text {\ttlbrace}* |
|
700 This sentence demonstrates quotations and antiquotations: |
|
701 {\at}{\ttlbrace}term "%x y. x"{\ttrbrace} is a well-typed term. |
|
702 *{\ttrbrace} |
|
703 \end{ttbox}\vspace{-\medskipamount} |
|
704 |
|
705 The notational change from the ASCII character~\verb,%, to the |
|
706 symbol~\isa{{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}} reveals that Isabelle printed this term, after |
|
707 parsing and type-checking. Document preparation enables symbolic |
|
708 output by default. |
|
709 |
|
710 \medskip The next example includes an option to show the type of all |
|
711 variables. The antiquotation |
|
712 \texttt{{\at}}\verb,{term [show_types] "%x y. x"}, produces the |
|
713 output \isa{{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}{\isaliteral{28}{\isacharparenleft}}x{\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}{\isaliteral{27}{\isacharprime}}a{\isaliteral{29}{\isacharparenright}}\ y{\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}{\isaliteral{27}{\isacharprime}}b{\isaliteral{2E}{\isachardot}}\ x}. Type inference has figured |
|
714 out the most general typings in the present theory context. Terms |
|
715 may acquire different typings due to constraints imposed by their |
|
716 environment; within a proof, for example, variables are given the |
|
717 same types as they have in the main goal statement. |
|
718 |
|
719 \medskip Several further kinds of antiquotations and options are |
|
720 available \cite{isabelle-isar-ref}. Here are a few commonly used |
|
721 combinations: |
|
722 |
|
723 \medskip |
|
724 |
|
725 \begin{tabular}{ll} |
|
726 \texttt{\at}\verb,{typ,~$\tau$\verb,}, & print type $\tau$ \\ |
|
727 \texttt{\at}\verb,{const,~$c$\verb,}, & check existence of $c$ and print it \\ |
|
728 \texttt{\at}\verb,{term,~$t$\verb,}, & print term $t$ \\ |
|
729 \texttt{\at}\verb,{prop,~$\phi$\verb,}, & print proposition $\phi$ \\ |
|
730 \texttt{\at}\verb,{prop [display],~$\phi$\verb,}, & print large proposition $\phi$ (with linebreaks) \\ |
|
731 \texttt{\at}\verb,{prop [source],~$\phi$\verb,}, & check proposition $\phi$, print its input \\ |
|
732 \texttt{\at}\verb,{thm,~$a$\verb,}, & print fact $a$ \\ |
|
733 \texttt{\at}\verb,{thm,~$a$~\verb,[no_vars]}, & print fact $a$, fixing schematic variables \\ |
|
734 \texttt{\at}\verb,{thm [source],~$a$\verb,}, & check availability of fact $a$, print its name \\ |
|
735 \texttt{\at}\verb,{text,~$s$\verb,}, & print uninterpreted text $s$ \\ |
|
736 \end{tabular} |
|
737 |
|
738 \medskip |
|
739 |
|
740 Note that \attrdx{no_vars} given above is \emph{not} an |
|
741 antiquotation option, but an attribute of the theorem argument given |
|
742 here. This might be useful with a diagnostic command like |
|
743 \isakeyword{thm}, too. |
|
744 |
|
745 \medskip The \texttt{\at}\verb,{text, $s$\verb,}, antiquotation is |
|
746 particularly interesting. Embedding uninterpreted text within an |
|
747 informal body might appear useless at first sight. Here the key |
|
748 virtue is that the string $s$ is processed as Isabelle output, |
|
749 interpreting Isabelle symbols appropriately. |
|
750 |
|
751 For example, \texttt{\at}\verb,{text "\<forall>\<exists>"}, produces \isa{{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}{\isaliteral{5C3C6578697374733E}{\isasymexists}}}, according to the standard interpretation of these symbol |
|
752 (cf.\ \S\ref{sec:doc-prep-symbols}). Thus we achieve consistent |
|
753 mathematical notation in both the formal and informal parts of the |
|
754 document very easily, independently of the term language of |
|
755 Isabelle. Manual {\LaTeX} code would leave more control over the |
|
756 typesetting, but is also slightly more tedious.% |
|
757 \end{isamarkuptext}% |
|
758 \isamarkuptrue% |
|
759 % |
|
760 \isamarkupsubsection{Interpretation of Symbols \label{sec:doc-prep-symbols}% |
|
761 } |
|
762 \isamarkuptrue% |
|
763 % |
|
764 \begin{isamarkuptext}% |
|
765 As has been pointed out before (\S\ref{sec:syntax-symbols}), |
|
766 Isabelle symbols are the smallest syntactic entities --- a |
|
767 straightforward generalization of ASCII characters. While Isabelle |
|
768 does not impose any interpretation of the infinite collection of |
|
769 named symbols, {\LaTeX} documents use canonical glyphs for certain |
|
770 standard symbols \cite{isabelle-isar-ref}. |
|
771 |
|
772 The {\LaTeX} code produced from Isabelle text follows a simple |
|
773 scheme. You can tune the final appearance by redefining certain |
|
774 macros, say in \texttt{root.tex} of the document. |
|
775 |
|
776 \begin{enumerate} |
|
777 |
|
778 \item 7-bit ASCII characters: letters \texttt{A\dots Z} and |
|
779 \texttt{a\dots z} are output directly, digits are passed as an |
|
780 argument to the \verb,\isadigit, macro, other characters are |
|
781 replaced by specifically named macros of the form |
|
782 \verb,\isacharXYZ,. |
|
783 |
|
784 \item Named symbols: \verb,\,\verb,<XYZ>, is turned into |
|
785 \verb,{\isasymXYZ},; note the additional braces. |
|
786 |
|
787 \item Named control symbols: \verb,\,\verb,<^XYZ>, is turned into |
|
788 \verb,\isactrlXYZ,; subsequent symbols may act as arguments if the |
|
789 control macro is defined accordingly. |
|
790 |
|
791 \end{enumerate} |
|
792 |
|
793 You may occasionally wish to give new {\LaTeX} interpretations of |
|
794 named symbols. This merely requires an appropriate definition of |
|
795 \verb,\isasymXYZ,, for \verb,\,\verb,<XYZ>, (see |
|
796 \texttt{isabelle.sty} for working examples). Control symbols are |
|
797 slightly more difficult to get right, though. |
|
798 |
|
799 \medskip The \verb,\isabellestyle, macro provides a high-level |
|
800 interface to tune the general appearance of individual symbols. For |
|
801 example, \verb,\isabellestyle{it}, uses the italics text style to |
|
802 mimic the general appearance of the {\LaTeX} math mode; double |
|
803 quotes are not printed at all. The resulting quality of typesetting |
|
804 is quite good, so this should be the default style for work that |
|
805 gets distributed to a broader audience.% |
|
806 \end{isamarkuptext}% |
|
807 \isamarkuptrue% |
|
808 % |
|
809 \isamarkupsubsection{Suppressing Output \label{sec:doc-prep-suppress}% |
|
810 } |
|
811 \isamarkuptrue% |
|
812 % |
|
813 \begin{isamarkuptext}% |
|
814 By default, Isabelle's document system generates a {\LaTeX} file for |
|
815 each theory that gets loaded while running the session. The |
|
816 generated \texttt{session.tex} will include all of these in order of |
|
817 appearance, which in turn gets included by the standard |
|
818 \texttt{root.tex}. Certainly one may change the order or suppress |
|
819 unwanted theories by ignoring \texttt{session.tex} and load |
|
820 individual files directly in \texttt{root.tex}. On the other hand, |
|
821 such an arrangement requires additional maintenance whenever the |
|
822 collection of theories changes. |
|
823 |
|
824 Alternatively, one may tune the theory loading process in |
|
825 \texttt{ROOT.ML} itself: traversal of the theory dependency graph |
|
826 may be fine-tuned by adding \verb,use_thy, invocations, although |
|
827 topological sorting still has to be observed. Moreover, the ML |
|
828 operator \verb,no_document, temporarily disables document generation |
|
829 while executing a theory loader command. Its usage is like this: |
|
830 |
|
831 \begin{verbatim} |
|
832 no_document use_thy "T"; |
|
833 \end{verbatim} |
|
834 |
|
835 \medskip Theory output may be suppressed more selectively, either |
|
836 via \bfindex{tagged command regions} or \bfindex{ignored material}. |
|
837 |
|
838 Tagged command regions works by annotating commands with named tags, |
|
839 which correspond to certain {\LaTeX} markup that tells how to treat |
|
840 particular parts of a document when doing the actual type-setting. |
|
841 By default, certain Isabelle/Isar commands are implicitly marked up |
|
842 using the predefined tags ``\emph{theory}'' (for theory begin and |
|
843 end), ``\emph{proof}'' (for proof commands), and ``\emph{ML}'' (for |
|
844 commands involving ML code). Users may add their own tags using the |
|
845 \verb,%,\emph{tag} notation right after a command name. In the |
|
846 subsequent example we hide a particularly irrelevant proof:% |
|
847 \end{isamarkuptext}% |
|
848 \isamarkuptrue% |
|
849 \isacommand{lemma}\isamarkupfalse% |
|
850 \ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{3D}{\isacharequal}}\ x{\isaliteral{22}{\isachardoublequoteclose}}% |
|
851 \isadeliminvisible |
|
852 \ % |
|
853 \endisadeliminvisible |
|
854 % |
|
855 \isataginvisible |
|
856 \isacommand{by}\isamarkupfalse% |
|
857 \ {\isaliteral{28}{\isacharparenleft}}simp{\isaliteral{29}{\isacharparenright}}% |
|
858 \endisataginvisible |
|
859 {\isafoldinvisible}% |
|
860 % |
|
861 \isadeliminvisible |
|
862 % |
|
863 \endisadeliminvisible |
|
864 % |
|
865 \begin{isamarkuptext}% |
|
866 The original source has been ``\verb,lemma "x = x" by %invisible (simp),''. |
|
867 Tags observe the structure of proofs; adjacent commands with the |
|
868 same tag are joined into a single region. The Isabelle document |
|
869 preparation system allows the user to specify how to interpret a |
|
870 tagged region, in order to keep, drop, or fold the corresponding |
|
871 parts of the document. See the \emph{Isabelle System Manual} |
|
872 \cite{isabelle-sys} for further details, especially on |
|
873 \texttt{isabelle usedir} and \texttt{isabelle document}. |
|
874 |
|
875 Ignored material is specified by delimiting the original formal |
|
876 source with special source comments |
|
877 \verb,(,\verb,*,\verb,<,\verb,*,\verb,), and |
|
878 \verb,(,\verb,*,\verb,>,\verb,*,\verb,),. These parts are stripped |
|
879 before the type-setting phase, without affecting the formal checking |
|
880 of the theory, of course. For example, we may hide parts of a proof |
|
881 that seem unfit for general public inspection. The following |
|
882 ``fully automatic'' proof is actually a fake:% |
|
883 \end{isamarkuptext}% |
|
884 \isamarkuptrue% |
|
885 \isacommand{lemma}\isamarkupfalse% |
|
886 \ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{5C3C6E6F7465713E}{\isasymnoteq}}\ {\isaliteral{28}{\isacharparenleft}}{\isadigit{0}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}int{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isadigit{0}}\ {\isaliteral{3C}{\isacharless}}\ x\ {\isaliteral{2A}{\isacharasterisk}}\ x{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
|
887 % |
|
888 \isadelimproof |
|
889 \ \ % |
|
890 \endisadelimproof |
|
891 % |
|
892 \isatagproof |
|
893 \isacommand{by}\isamarkupfalse% |
|
894 \ {\isaliteral{28}{\isacharparenleft}}auto{\isaliteral{29}{\isacharparenright}}% |
|
895 \endisatagproof |
|
896 {\isafoldproof}% |
|
897 % |
|
898 \isadelimproof |
|
899 % |
|
900 \endisadelimproof |
|
901 % |
|
902 \begin{isamarkuptext}% |
|
903 \noindent The real source of the proof has been as follows: |
|
904 |
|
905 \begin{verbatim} |
|
906 by (auto(*<*)simp add: zero_less_mult_iff(*>*)) |
|
907 \end{verbatim} |
|
908 %(* |
|
909 |
|
910 \medskip Suppressing portions of printed text demands care. You |
|
911 should not misrepresent the underlying theory development. It is |
|
912 easy to invalidate the visible text by hiding references to |
|
913 questionable axioms, for example.% |
|
914 \end{isamarkuptext}% |
|
915 \isamarkuptrue% |
|
916 % |
|
917 \isadelimtheory |
|
918 % |
|
919 \endisadelimtheory |
|
920 % |
|
921 \isatagtheory |
|
922 % |
|
923 \endisatagtheory |
|
924 {\isafoldtheory}% |
|
925 % |
|
926 \isadelimtheory |
|
927 % |
|
928 \endisadelimtheory |
|
929 \end{isabellebody}% |
|
930 %%% Local Variables: |
|
931 %%% mode: latex |
|
932 %%% TeX-master: "root" |
|
933 %%% End: |