|
1 (* $Id$ *) |
|
2 |
|
3 theory Document_Preparation |
|
4 imports Main |
|
5 begin |
|
6 |
|
7 chapter {* Document preparation \label{ch:document-prep} *} |
|
8 |
|
9 text {* |
|
10 Isabelle/Isar provides a simple document preparation system based on |
|
11 existing {PDF-\LaTeX} technology, with full support of hyper-links |
|
12 (both local references and URLs) and bookmarks. Thus the results |
|
13 are equally well suited for WWW browsing and as printed copies. |
|
14 |
|
15 \medskip Isabelle generates {\LaTeX} output as part of the run of a |
|
16 \emph{logic session} (see also \cite{isabelle-sys}). Getting |
|
17 started with a working configuration for common situations is quite |
|
18 easy by using the Isabelle @{verbatim mkdir} and @{verbatim make} |
|
19 tools. First invoke |
|
20 \begin{ttbox} |
|
21 isatool mkdir Foo |
|
22 \end{ttbox} |
|
23 to initialize a separate directory for session @{verbatim Foo} --- |
|
24 it is safe to experiment, since @{verbatim "isatool mkdir"} never |
|
25 overwrites existing files. Ensure that @{verbatim "Foo/ROOT.ML"} |
|
26 holds ML commands to load all theories required for this session; |
|
27 furthermore @{verbatim "Foo/document/root.tex"} should include any |
|
28 special {\LaTeX} macro packages required for your document (the |
|
29 default is usually sufficient as a start). |
|
30 |
|
31 The session is controlled by a separate @{verbatim IsaMakefile} |
|
32 (with crude source dependencies by default). This file is located |
|
33 one level up from the @{verbatim Foo} directory location. Now |
|
34 invoke |
|
35 \begin{ttbox} |
|
36 isatool make Foo |
|
37 \end{ttbox} |
|
38 to run the @{verbatim Foo} session, with browser information and |
|
39 document preparation enabled. Unless any errors are reported by |
|
40 Isabelle or {\LaTeX}, the output will appear inside the directory |
|
41 @{verbatim ISABELLE_BROWSER_INFO}, as reported by the batch job in |
|
42 verbose mode. |
|
43 |
|
44 \medskip You may also consider to tune the @{verbatim usedir} |
|
45 options in @{verbatim IsaMakefile}, for example to change the output |
|
46 format from @{verbatim pdf} to @{verbatim dvi}, or activate the |
|
47 @{verbatim "-D"} option to retain a second copy of the generated |
|
48 {\LaTeX} sources. |
|
49 |
|
50 \medskip See \emph{The Isabelle System Manual} \cite{isabelle-sys} |
|
51 for further details on Isabelle logic sessions and theory |
|
52 presentation. The Isabelle/HOL tutorial \cite{isabelle-hol-book} |
|
53 also covers theory presentation issues. |
|
54 *} |
|
55 |
|
56 |
|
57 section {* Markup commands \label{sec:markup} *} |
|
58 |
|
59 text {* |
|
60 \begin{matharray}{rcl} |
|
61 @{command_def "chapter"} & : & \isarkeep{local{\dsh}theory} \\ |
|
62 @{command_def "section"} & : & \isarkeep{local{\dsh}theory} \\ |
|
63 @{command_def "subsection"} & : & \isarkeep{local{\dsh}theory} \\ |
|
64 @{command_def "subsubsection"} & : & \isarkeep{local{\dsh}theory} \\ |
|
65 @{command_def "text"} & : & \isarkeep{local{\dsh}theory} \\ |
|
66 @{command_def "text_raw"} & : & \isarkeep{local{\dsh}theory} \\[0.5ex] |
|
67 @{command_def "sect"} & : & \isartrans{proof}{proof} \\ |
|
68 @{command_def "subsect"} & : & \isartrans{proof}{proof} \\ |
|
69 @{command_def "subsubsect"} & : & \isartrans{proof}{proof} \\ |
|
70 @{command_def "txt"} & : & \isartrans{proof}{proof} \\ |
|
71 @{command_def "txt_raw"} & : & \isartrans{proof}{proof} \\ |
|
72 \end{matharray} |
|
73 |
|
74 Apart from formal comments (see \secref{sec:comments}), markup |
|
75 commands provide a structured way to insert text into the document |
|
76 generated from a theory (see \cite{isabelle-sys} for more |
|
77 information on Isabelle's document preparation tools). |
|
78 |
|
79 \begin{rail} |
|
80 ('chapter' | 'section' | 'subsection' | 'subsubsection' | 'text') target? text |
|
81 ; |
|
82 ('text\_raw' | 'sect' | 'subsect' | 'subsubsect' | 'txt' | 'txt\_raw') text |
|
83 ; |
|
84 \end{rail} |
|
85 |
|
86 \begin{descr} |
|
87 |
|
88 \item [@{command "chapter"}, @{command "section"}, @{command |
|
89 "subsection"}, and @{command "subsubsection"}] mark chapter and |
|
90 section headings. |
|
91 |
|
92 \item [@{command "text"} and @{command "txt"}] specify paragraphs of |
|
93 plain text. |
|
94 |
|
95 \item [@{command "text_raw"} and @{command "txt_raw"}] insert |
|
96 {\LaTeX} source into the output, without additional markup. Thus |
|
97 the full range of document manipulations becomes available. |
|
98 |
|
99 \end{descr} |
|
100 |
|
101 The @{text "text"} argument of these markup commands (except for |
|
102 @{command "text_raw"}) may contain references to formal entities |
|
103 (``antiquotations'', see also \secref{sec:antiq}). These are |
|
104 interpreted in the present theory context, or the named @{text |
|
105 "target"}. |
|
106 |
|
107 Any of these markup elements corresponds to a {\LaTeX} command with |
|
108 the name prefixed by @{verbatim "\\isamarkup"}. For the sectioning |
|
109 commands this is a plain macro with a single argument, e.g.\ |
|
110 @{verbatim "\\isamarkupchapter{"}@{text "\<dots>"}@{verbatim "}"} for |
|
111 @{command "chapter"}. The @{command "text"} markup results in a |
|
112 {\LaTeX} environment @{verbatim "\\begin{isamarkuptext}"} @{text |
|
113 "\<dots>"} @{verbatim "\\end{isamarkuptext}"}, while @{command "text_raw"} |
|
114 causes the text to be inserted directly into the {\LaTeX} source. |
|
115 |
|
116 \medskip The proof markup commands closely resemble those for theory |
|
117 specifications, but have a different formal status and produce |
|
118 different {\LaTeX} macros. Also note that the @{command_ref |
|
119 "header"} declaration (see \secref{sec:begin-thy}) admits to insert |
|
120 section markup just preceding the actual theory definition. |
|
121 *} |
|
122 |
|
123 |
|
124 section {* Antiquotations \label{sec:antiq} *} |
|
125 |
|
126 text {* |
|
127 \begin{matharray}{rcl} |
|
128 @{antiquotation_def "theory"} & : & \isarantiq \\ |
|
129 @{antiquotation_def "thm"} & : & \isarantiq \\ |
|
130 @{antiquotation_def "prop"} & : & \isarantiq \\ |
|
131 @{antiquotation_def "term"} & : & \isarantiq \\ |
|
132 @{antiquotation_def const} & : & \isarantiq \\ |
|
133 @{antiquotation_def abbrev} & : & \isarantiq \\ |
|
134 @{antiquotation_def typeof} & : & \isarantiq \\ |
|
135 @{antiquotation_def typ} & : & \isarantiq \\ |
|
136 @{antiquotation_def thm_style} & : & \isarantiq \\ |
|
137 @{antiquotation_def term_style} & : & \isarantiq \\ |
|
138 @{antiquotation_def "text"} & : & \isarantiq \\ |
|
139 @{antiquotation_def goals} & : & \isarantiq \\ |
|
140 @{antiquotation_def subgoals} & : & \isarantiq \\ |
|
141 @{antiquotation_def prf} & : & \isarantiq \\ |
|
142 @{antiquotation_def full_prf} & : & \isarantiq \\ |
|
143 @{antiquotation_def ML} & : & \isarantiq \\ |
|
144 @{antiquotation_def ML_type} & : & \isarantiq \\ |
|
145 @{antiquotation_def ML_struct} & : & \isarantiq \\ |
|
146 \end{matharray} |
|
147 |
|
148 The text body of formal comments (see also \secref{sec:comments}) |
|
149 may contain antiquotations of logical entities, such as theorems, |
|
150 terms and types, which are to be presented in the final output |
|
151 produced by the Isabelle document preparation system (see also |
|
152 \chref{ch:document-prep}). |
|
153 |
|
154 Thus embedding of ``@{text "@{term [show_types] \"f x = a + x\"}"}'' |
|
155 within a text block would cause |
|
156 \isa{{\isacharparenleft}f{\isasymColon}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isacharparenright}\ {\isacharparenleft}x{\isasymColon}{\isacharprime}a{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}a{\isasymColon}{\isacharprime}a{\isacharparenright}\ {\isacharplus}\ x} to appear in the final {\LaTeX} document. Also note that theorem |
|
157 antiquotations may involve attributes as well. For example, |
|
158 @{text "@{thm sym [no_vars]}"} would print the theorem's |
|
159 statement where all schematic variables have been replaced by fixed |
|
160 ones, which are easier to read. |
|
161 |
|
162 \begin{rail} |
|
163 atsign lbrace antiquotation rbrace |
|
164 ; |
|
165 |
|
166 antiquotation: |
|
167 'theory' options name | |
|
168 'thm' options thmrefs | |
|
169 'prop' options prop | |
|
170 'term' options term | |
|
171 'const' options term | |
|
172 'abbrev' options term | |
|
173 'typeof' options term | |
|
174 'typ' options type | |
|
175 'thm\_style' options name thmref | |
|
176 'term\_style' options name term | |
|
177 'text' options name | |
|
178 'goals' options | |
|
179 'subgoals' options | |
|
180 'prf' options thmrefs | |
|
181 'full\_prf' options thmrefs | |
|
182 'ML' options name | |
|
183 'ML\_type' options name | |
|
184 'ML\_struct' options name |
|
185 ; |
|
186 options: '[' (option * ',') ']' |
|
187 ; |
|
188 option: name | name '=' name |
|
189 ; |
|
190 \end{rail} |
|
191 |
|
192 Note that the syntax of antiquotations may \emph{not} include source |
|
193 comments @{verbatim "(*"}~@{text "\<dots>"}~@{verbatim "*)"} or verbatim |
|
194 text @{verbatim "{"}@{verbatim "*"}~@{text "\<dots>"}~@{verbatim |
|
195 "*"}@{verbatim "}"}. |
|
196 |
|
197 \begin{descr} |
|
198 |
|
199 \item [@{text "@{theory A}"}] prints the name @{text "A"}, which is |
|
200 guaranteed to refer to a valid ancestor theory in the current |
|
201 context. |
|
202 |
|
203 \item [@{text "@{thm a\<^sub>1 \<dots> a\<^sub>n}"}] prints theorems |
|
204 @{text "a\<^sub>1 \<dots> a\<^sub>n"}. Note that attribute specifications |
|
205 may be included as well (see also \secref{sec:syn-att}); the |
|
206 @{attribute_ref no_vars} rule (see \secref{sec:misc-meth-att}) would |
|
207 be particularly useful to suppress printing of schematic variables. |
|
208 |
|
209 \item [@{text "@{prop \<phi>}"}] prints a well-typed proposition @{text |
|
210 "\<phi>"}. |
|
211 |
|
212 \item [@{text "@{term t}"}] prints a well-typed term @{text "t"}. |
|
213 |
|
214 \item [@{text "@{const c}"}] prints a logical or syntactic constant |
|
215 @{text "c"}. |
|
216 |
|
217 \item [@{text "@{abbrev c x\<^sub>1 \<dots> x\<^sub>n}"}] prints a constant |
|
218 abbreviation @{text "c x\<^sub>1 \<dots> x\<^sub>n \<equiv> rhs"} as defined in |
|
219 the current context. |
|
220 |
|
221 \item [@{text "@{typeof t}"}] prints the type of a well-typed term |
|
222 @{text "t"}. |
|
223 |
|
224 \item [@{text "@{typ \<tau>}"}] prints a well-formed type @{text "\<tau>"}. |
|
225 |
|
226 \item [@{text "@{thm_style s a}"}] prints theorem @{text a}, |
|
227 previously applying a style @{text s} to it (see below). |
|
228 |
|
229 \item [@{text "@{term_style s t}"}] prints a well-typed term @{text |
|
230 t} after applying a style @{text s} to it (see below). |
|
231 |
|
232 \item [@{text "@{text s}"}] prints uninterpreted source text @{text |
|
233 s}. This is particularly useful to print portions of text according |
|
234 to the Isabelle {\LaTeX} output style, without demanding |
|
235 well-formedness (e.g.\ small pieces of terms that should not be |
|
236 parsed or type-checked yet). |
|
237 |
|
238 \item [@{text "@{goals}"}] prints the current \emph{dynamic} goal |
|
239 state. This is mainly for support of tactic-emulation scripts |
|
240 within Isar --- presentation of goal states does not conform to |
|
241 actual human-readable proof documents. |
|
242 |
|
243 Please do not include goal states into document output unless you |
|
244 really know what you are doing! |
|
245 |
|
246 \item [@{text "@{subgoals}"}] is similar to @{text "@{goals}"}, but |
|
247 does not print the main goal. |
|
248 |
|
249 \item [@{text "@{prf a\<^sub>1 \<dots> a\<^sub>n}"}] prints the (compact) |
|
250 proof terms corresponding to the theorems @{text "a\<^sub>1 \<dots> |
|
251 a\<^sub>n"}. Note that this requires proof terms to be switched on |
|
252 for the current object logic (see the ``Proof terms'' section of the |
|
253 Isabelle reference manual for information on how to do this). |
|
254 |
|
255 \item [@{text "@{full_prf a\<^sub>1 \<dots> a\<^sub>n}"}] is like @{text |
|
256 "@{prf a\<^sub>1 \<dots> a\<^sub>n}"}, but displays the full proof terms, |
|
257 i.e.\ also displays information omitted in the compact proof term, |
|
258 which is denoted by ``@{text _}'' placeholders there. |
|
259 |
|
260 \item [@{text "@{ML s}"}, @{text "@{ML_type s}"}, and @{text |
|
261 "@{ML_struct s}"}] check text @{text s} as ML value, type, and |
|
262 structure, respectively. The source is displayed verbatim. |
|
263 |
|
264 \end{descr} |
|
265 |
|
266 \medskip The following standard styles for use with @{text |
|
267 thm_style} and @{text term_style} are available: |
|
268 |
|
269 \begin{descr} |
|
270 |
|
271 \item [@{text lhs}] extracts the first argument of any application |
|
272 form with at least two arguments -- typically meta-level or |
|
273 object-level equality, or any other binary relation. |
|
274 |
|
275 \item [@{text rhs}] is like @{text lhs}, but extracts the second |
|
276 argument. |
|
277 |
|
278 \item [@{text "concl"}] extracts the conclusion @{text C} from a rule |
|
279 in Horn-clause normal form @{text "A\<^sub>1 \<Longrightarrow> \<dots> A\<^sub>n \<Longrightarrow> C"}. |
|
280 |
|
281 \item [@{text "prem1"}, \dots, @{text "prem9"}] extract premise |
|
282 number @{text "1, \<dots>, 9"}, respectively, from from a rule in |
|
283 Horn-clause normal form @{text "A\<^sub>1 \<Longrightarrow> \<dots> A\<^sub>n \<Longrightarrow> C"} |
|
284 |
|
285 \end{descr} |
|
286 |
|
287 \medskip |
|
288 The following options are available to tune the output. Note that most of |
|
289 these coincide with ML flags of the same names (see also \cite{isabelle-ref}). |
|
290 |
|
291 \begin{descr} |
|
292 |
|
293 \item[@{text "show_types = bool"} and @{text "show_sorts = bool"}] |
|
294 control printing of explicit type and sort constraints. |
|
295 |
|
296 \item[@{text "show_structs = bool"}] controls printing of implicit |
|
297 structures. |
|
298 |
|
299 \item[@{text "long_names = bool"}] forces names of types and |
|
300 constants etc.\ to be printed in their fully qualified internal |
|
301 form. |
|
302 |
|
303 \item[@{text "short_names = bool"}] forces names of types and |
|
304 constants etc.\ to be printed unqualified. Note that internalizing |
|
305 the output again in the current context may well yield a different |
|
306 result. |
|
307 |
|
308 \item[@{text "unique_names = bool"}] determines whether the printed |
|
309 version of qualified names should be made sufficiently long to avoid |
|
310 overlap with names declared further back. Set to @{text false} for |
|
311 more concise output. |
|
312 |
|
313 \item[@{text "eta_contract = bool"}] prints terms in @{text |
|
314 \<eta>}-contracted form. |
|
315 |
|
316 \item[@{text "display = bool"}] indicates if the text is to be |
|
317 output as multi-line ``display material'', rather than a small piece |
|
318 of text without line breaks (which is the default). |
|
319 |
|
320 \item[@{text "break = bool"}] controls line breaks in non-display |
|
321 material. |
|
322 |
|
323 \item[@{text "quotes = bool"}] indicates if the output should be |
|
324 enclosed in double quotes. |
|
325 |
|
326 \item[@{text "mode = name"}] adds @{text name} to the print mode to |
|
327 be used for presentation (see also \cite{isabelle-ref}). Note that |
|
328 the standard setup for {\LaTeX} output is already present by |
|
329 default, including the modes @{text latex} and @{text xsymbols}. |
|
330 |
|
331 \item[@{text "margin = nat"} and @{text "indent = nat"}] change the |
|
332 margin or indentation for pretty printing of display material. |
|
333 |
|
334 \item[@{text "source = bool"}] prints the source text of the |
|
335 antiquotation arguments, rather than the actual value. Note that |
|
336 this does not affect well-formedness checks of @{antiquotation |
|
337 "thm"}, @{antiquotation "term"}, etc. (only the @{antiquotation |
|
338 "text"} antiquotation admits arbitrary output). |
|
339 |
|
340 \item[@{text "goals_limit = nat"}] determines the maximum number of |
|
341 goals to be printed. |
|
342 |
|
343 \item[@{text "locale = name"}] specifies an alternative locale |
|
344 context used for evaluating and printing the subsequent argument. |
|
345 |
|
346 \end{descr} |
|
347 |
|
348 For boolean flags, ``@{text "name = true"}'' may be abbreviated as |
|
349 ``@{text name}''. All of the above flags are disabled by default, |
|
350 unless changed from ML. |
|
351 |
|
352 \medskip Note that antiquotations do not only spare the author from |
|
353 tedious typing of logical entities, but also achieve some degree of |
|
354 consistency-checking of informal explanations with formal |
|
355 developments: well-formedness of terms and types with respect to the |
|
356 current theory or proof context is ensured here. |
|
357 *} |
|
358 |
|
359 |
|
360 section {* Tagged commands \label{sec:tags} *} |
|
361 |
|
362 text {* |
|
363 Each Isabelle/Isar command may be decorated by presentation tags: |
|
364 |
|
365 \indexouternonterm{tags} |
|
366 \begin{rail} |
|
367 tags: ( tag * ) |
|
368 ; |
|
369 tag: '\%' (ident | string) |
|
370 \end{rail} |
|
371 |
|
372 The tags @{text "theory"}, @{text "proof"}, @{text "ML"} are already |
|
373 pre-declared for certain classes of commands: |
|
374 |
|
375 \medskip |
|
376 |
|
377 \begin{tabular}{ll} |
|
378 @{text "theory"} & theory begin/end \\ |
|
379 @{text "proof"} & all proof commands \\ |
|
380 @{text "ML"} & all commands involving ML code \\ |
|
381 \end{tabular} |
|
382 |
|
383 \medskip The Isabelle document preparation system (see also |
|
384 \cite{isabelle-sys}) allows tagged command regions to be presented |
|
385 specifically, e.g.\ to fold proof texts, or drop parts of the text |
|
386 completely. |
|
387 |
|
388 For example ``@{command "by"}~@{text "%invisible auto"}'' would |
|
389 cause that piece of proof to be treated as @{text invisible} instead |
|
390 of @{text "proof"} (the default), which may be either show or hidden |
|
391 depending on the document setup. In contrast, ``@{command |
|
392 "by"}~@{text "%visible auto"}'' would force this text to be shown |
|
393 invariably. |
|
394 |
|
395 Explicit tag specifications within a proof apply to all subsequent |
|
396 commands of the same level of nesting. For example, ``@{command |
|
397 "proof"}~@{text "%visible \<dots>"}~@{command "qed"}'' would force the |
|
398 whole sub-proof to be typeset as @{text visible} (unless some of its |
|
399 parts are tagged differently). |
|
400 *} |
|
401 |
|
402 |
|
403 section {* Draft presentation *} |
|
404 |
|
405 text {* |
|
406 \begin{matharray}{rcl} |
|
407 @{command_def "display_drafts"}@{text "\<^sup>*"} & : & \isarkeep{\cdot} \\ |
|
408 @{command_def "print_drafts"}@{text "\<^sup>*"} & : & \isarkeep{\cdot} \\ |
|
409 \end{matharray} |
|
410 |
|
411 \begin{rail} |
|
412 ('display\_drafts' | 'print\_drafts') (name +) |
|
413 ; |
|
414 \end{rail} |
|
415 |
|
416 \begin{descr} |
|
417 |
|
418 \item [@{command "display_drafts"}~@{text paths} and @{command |
|
419 "print_drafts"}~@{text paths}] perform simple output of a given list |
|
420 of raw source files. Only those symbols that do not require |
|
421 additional {\LaTeX} packages are displayed properly, everything else |
|
422 is left verbatim. |
|
423 |
|
424 \end{descr} |
|
425 *} |
|
426 |
|
427 end |