3 theory Document_Preparation
7 chapter {* Document preparation \label{ch:document-prep} *}
9 text {* Isabelle/Isar provides a simple document preparation system
10 based on regular {PDF-\LaTeX} technology, with full support for
11 hyper-links and bookmarks. Thus the results are well suited for WWW
12 browsing and as printed copies.
14 \medskip Isabelle generates {\LaTeX} output while running a
15 \emph{logic session} (see also \cite{isabelle-sys}). Getting
16 started with a working configuration for common situations is quite
17 easy by using the Isabelle @{verbatim mkdir} and @{verbatim make}
22 to initialize a separate directory for session @{verbatim Foo} (it
23 is safe to experiment, since @{verbatim "isabelle mkdir"} never
24 overwrites existing files). Ensure that @{verbatim "Foo/ROOT.ML"}
25 holds ML commands to load all theories required for this session;
26 furthermore @{verbatim "Foo/document/root.tex"} should include any
27 special {\LaTeX} macro packages required for your document (the
28 default is usually sufficient as a start).
30 The session is controlled by a separate @{verbatim IsaMakefile}
31 (with crude source dependencies by default). This file is located
32 one level up from the @{verbatim Foo} directory location. Now
37 to run the @{verbatim Foo} session, with browser information and
38 document preparation enabled. Unless any errors are reported by
39 Isabelle or {\LaTeX}, the output will appear inside the directory
40 defined by the @{verbatim ISABELLE_BROWSER_INFO} setting (as
41 reported by the batch job in verbose mode).
43 \medskip You may also consider to tune the @{verbatim usedir}
44 options in @{verbatim IsaMakefile}, for example to switch the output
45 format between @{verbatim pdf} and @{verbatim dvi}, or activate the
46 @{verbatim "-D"} option to retain a second copy of the generated
47 {\LaTeX} sources (for manual inspection or separate runs of
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 to some extent.
57 section {* Markup commands \label{sec:markup} *}
60 \begin{matharray}{rcl}
61 @{command_def "header"} & : & \isarkeep{toplevel} \\[0.5ex]
62 @{command_def "chapter"} & : & \isarkeep{local{\dsh}theory} \\
63 @{command_def "section"} & : & \isarkeep{local{\dsh}theory} \\
64 @{command_def "subsection"} & : & \isarkeep{local{\dsh}theory} \\
65 @{command_def "subsubsection"} & : & \isarkeep{local{\dsh}theory} \\
66 @{command_def "text"} & : & \isarkeep{local{\dsh}theory} \\
67 @{command_def "text_raw"} & : & \isarkeep{local{\dsh}theory} \\[0.5ex]
68 @{command_def "sect"} & : & \isartrans{proof}{proof} \\
69 @{command_def "subsect"} & : & \isartrans{proof}{proof} \\
70 @{command_def "subsubsect"} & : & \isartrans{proof}{proof} \\
71 @{command_def "txt"} & : & \isartrans{proof}{proof} \\
72 @{command_def "txt_raw"} & : & \isartrans{proof}{proof} \\
75 Markup commands provide a structured way to insert text into the
76 document generated from a theory. Each markup command takes a
77 single @{syntax text} argument, which is passed as argument to a
78 corresponding {\LaTeX} macro. The default macros provided by
79 @{"file" "~~/lib/texinputs/isabelle.sty"} can be redefined according
80 to the needs of the underlying document and {\LaTeX} styles.
82 Note that formal comments (\secref{sec:comments}) are similar to
83 markup commands, but have a different status within Isabelle/Isar
87 ('chapter' | 'section' | 'subsection' | 'subsubsection' | 'text') target? text
89 ('header' | 'text\_raw' | 'sect' | 'subsect' | 'subsubsect' | 'txt' | 'txt\_raw') text
95 \item [@{command header}] provides plain text markup just preceding
96 the formal beginning of a theory. The corresponding {\LaTeX} macro
97 is @{verbatim "\\isamarkupheader"}, which acts like @{command
100 \item [@{command chapter}, @{command section}, @{command
101 subsection}, and @{command subsubsection}] mark chapter and section
102 headings within the main theory body or local theory targets. The
103 corresponding {\LaTeX} macros are @{verbatim "\\isamarkupchapter"},
104 @{verbatim "\\isamarkupsection"}, @{verbatim
105 "\\isamarkupsubsection"} etc.
107 \item [@{command sect}, @{command subsect}, and @{command
108 subsubsect}] mark section headings within proofs. The corresponding
109 {\LaTeX} macros are @{verbatim "\\isamarkupsect"}, @{verbatim
110 "\\isamarkupsubsect"} etc.
112 \item [@{command text} and @{command txt}] specify paragraphs of
113 plain text. This corresponds to a {\LaTeX} environment @{verbatim
114 "\\begin{isamarkuptext}"} @{text "\<dots>"} @{verbatim
115 "\\end{isamarkuptext}"} etc.
117 \item [@{command text_raw} and @{command txt_raw}] insert {\LaTeX}
118 source into the output, without additional markup. Thus the full
119 range of document manipulations becomes available, at the risk of
120 messing up document output.
124 Except for @{command "text_raw"} and @{command "txt_raw"}, the text
125 passed to any of the above markup commands may refer to formal
126 entities via \emph{document antiquotations}, see also
127 \secref{sec:antiq}. These are interpreted in the present theory or
128 proof context, or the named @{text "target"}.
130 \medskip The proof markup commands closely resemble those for theory
131 specifications, but have a different formal status and produce
132 different {\LaTeX} macros. The default definitions coincide for
133 analogous commands such as @{command section} and @{command sect}.
137 section {* Document Antiquotations \label{sec:antiq} *}
140 \begin{matharray}{rcl}
141 @{antiquotation_def "theory"} & : & \isarantiq \\
142 @{antiquotation_def "thm"} & : & \isarantiq \\
143 @{antiquotation_def "lemma"} & : & \isarantiq \\
144 @{antiquotation_def "prop"} & : & \isarantiq \\
145 @{antiquotation_def "term"} & : & \isarantiq \\
146 @{antiquotation_def const} & : & \isarantiq \\
147 @{antiquotation_def abbrev} & : & \isarantiq \\
148 @{antiquotation_def typeof} & : & \isarantiq \\
149 @{antiquotation_def typ} & : & \isarantiq \\
150 @{antiquotation_def thm_style} & : & \isarantiq \\
151 @{antiquotation_def term_style} & : & \isarantiq \\
152 @{antiquotation_def "text"} & : & \isarantiq \\
153 @{antiquotation_def goals} & : & \isarantiq \\
154 @{antiquotation_def subgoals} & : & \isarantiq \\
155 @{antiquotation_def prf} & : & \isarantiq \\
156 @{antiquotation_def full_prf} & : & \isarantiq \\
157 @{antiquotation_def ML} & : & \isarantiq \\
158 @{antiquotation_def ML_type} & : & \isarantiq \\
159 @{antiquotation_def ML_struct} & : & \isarantiq \\
162 The overall content of an Isabelle/Isar theory may alternate between
163 formal and informal text. The main body consists of formal
164 specification and proof commands, interspersed with markup commands
165 (\secref{sec:markup}) or document comments (\secref{sec:comments}).
166 The argument of markup commands quotes informal text to be printed
167 in the resulting document, but may again refer to formal entities
168 via \emph{document antiquotations}.
170 For example, embedding of ``@{text [source=false] "@{term [show_types] \"f x = a + x\"}"}''
171 within a text block makes
172 \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} appear in the final {\LaTeX} document.
174 Antiquotations usually spare the author tedious typing of logical
175 entities in full detail. Even more importantly, some degree of
176 consistency-checking between the main body of formal text and its
177 informal explanation is achieved, since terms and types appearing in
178 antiquotations are checked within the current theory or proof
182 atsign lbrace antiquotation rbrace
186 'theory' options name |
187 'thm' options thmrefs |
188 'lemma' options prop 'by' method |
189 'prop' options prop |
190 'term' options term |
191 'const' options term |
192 'abbrev' options term |
193 'typeof' options term |
195 'thm\_style' options name thmref |
196 'term\_style' options name term |
197 'text' options name |
200 'prf' options thmrefs |
201 'full\_prf' options thmrefs |
203 'ML\_type' options name |
204 'ML\_struct' options name
206 options: '[' (option * ',') ']'
208 option: name | name '=' name
212 Note that the syntax of antiquotations may \emph{not} include source
213 comments @{verbatim "(*"}~@{text "\<dots>"}~@{verbatim "*)"} nor verbatim
214 text @{verbatim "{"}@{verbatim "*"}~@{text "\<dots>"}~@{verbatim
219 \item [@{text "@{theory A}"}] prints the name @{text "A"}, which is
220 guaranteed to refer to a valid ancestor theory in the current
223 \item [@{text "@{thm a\<^sub>1 \<dots> a\<^sub>n}"}] prints theorems @{text "a\<^sub>1 \<dots> a\<^sub>n"}.
224 Full fact expressions are allowed here, including attributes
225 (\secref{sec:syn-att}).
227 \item [@{text "@{prop \<phi>}"}] prints a well-typed proposition @{text
230 \item [@{text "@{lemma \<phi> by m}"}] proves a well-typed proposition
231 @{text "\<phi>"} by method @{text m} and prints the original @{text "\<phi>"}.
233 \item [@{text "@{term t}"}] prints a well-typed term @{text "t"}.
235 \item [@{text "@{const c}"}] prints a logical or syntactic constant
238 \item [@{text "@{abbrev c x\<^sub>1 \<dots> x\<^sub>n}"}] prints a constant
239 abbreviation @{text "c x\<^sub>1 \<dots> x\<^sub>n \<equiv> rhs"} as defined in
242 \item [@{text "@{typeof t}"}] prints the type of a well-typed term
245 \item [@{text "@{typ \<tau>}"}] prints a well-formed type @{text "\<tau>"}.
247 \item [@{text "@{thm_style s a}"}] prints theorem @{text a},
248 previously applying a style @{text s} to it (see below).
250 \item [@{text "@{term_style s t}"}] prints a well-typed term @{text
251 t} after applying a style @{text s} to it (see below).
253 \item [@{text "@{text s}"}] prints uninterpreted source text @{text
254 s}. This is particularly useful to print portions of text according
255 to the Isabelle document style, without demanding well-formedness,
256 e.g.\ small pieces of terms that should not be parsed or
259 \item [@{text "@{goals}"}] prints the current \emph{dynamic} goal
260 state. This is mainly for support of tactic-emulation scripts
261 within Isar. Presentation of goal states does not conform to the
262 idea of human-readable proof documents!
264 When explaining proofs in detail it is usually better to spell out
265 the reasoning via proper Isar proof commands, instead of peeking at
266 the internal machine configuration.
268 \item [@{text "@{subgoals}"}] is similar to @{text "@{goals}"}, but
269 does not print the main goal.
271 \item [@{text "@{prf a\<^sub>1 \<dots> a\<^sub>n}"}] prints the (compact) proof terms
272 corresponding to the theorems @{text "a\<^sub>1 \<dots> a\<^sub>n"}. Note that this
273 requires proof terms to be switched on for the current logic
276 \item [@{text "@{full_prf a\<^sub>1 \<dots> a\<^sub>n}"}] is like @{text
277 "@{prf a\<^sub>1 \<dots> a\<^sub>n}"}, but prints the full proof terms, i.e.\ also
278 displays information omitted in the compact proof term, which is
279 denoted by ``@{text _}'' placeholders there.
281 \item [@{text "@{ML s}"}, @{text "@{ML_type s}"}, and @{text
282 "@{ML_struct s}"}] check text @{text s} as ML value, type, and
283 structure, respectively. The source is printed verbatim.
289 subsubsection {* Styled antiquotations *}
291 text {* Some antiquotations like @{text thm_style} and @{text
292 term_style} admit an extra \emph{style} specification to modify the
293 printed result. The following standard styles are available:
297 \item [@{text lhs}] extracts the first argument of any application
298 form with at least two arguments --- typically meta-level or
299 object-level equality, or any other binary relation.
301 \item [@{text rhs}] is like @{text lhs}, but extracts the second
304 \item [@{text "concl"}] extracts the conclusion @{text C} from a rule
305 in Horn-clause normal form @{text "A\<^sub>1 \<Longrightarrow> \<dots> A\<^sub>n \<Longrightarrow> C"}.
307 \item [@{text "prem1"}, \dots, @{text "prem9"}] extract premise
308 number @{text "1, \<dots>, 9"}, respectively, from from a rule in
309 Horn-clause normal form @{text "A\<^sub>1 \<Longrightarrow> \<dots> A\<^sub>n \<Longrightarrow> C"}
315 subsubsection {* General options *}
317 text {* The following options are available to tune the printed output
318 of antiquotations. Note that many of these coincide with global ML
319 flags of the same names.
323 \item[@{text "show_types = bool"} and @{text "show_sorts = bool"}]
324 control printing of explicit type and sort constraints.
326 \item[@{text "show_structs = bool"}] controls printing of implicit
329 \item[@{text "long_names = bool"}] forces names of types and
330 constants etc.\ to be printed in their fully qualified internal
333 \item[@{text "short_names = bool"}] forces names of types and
334 constants etc.\ to be printed unqualified. Note that internalizing
335 the output again in the current context may well yield a different
338 \item[@{text "unique_names = bool"}] determines whether the printed
339 version of qualified names should be made sufficiently long to avoid
340 overlap with names declared further back. Set to @{text false} for
343 \item[@{text "eta_contract = bool"}] prints terms in @{text
344 \<eta>}-contracted form.
346 \item[@{text "display = bool"}] indicates if the text is to be
347 output as multi-line ``display material'', rather than a small piece
348 of text without line breaks (which is the default).
350 In this mode the embedded entities are printed in the same style as
351 the main theory text.
353 \item[@{text "break = bool"}] controls line breaks in non-display
356 \item[@{text "quotes = bool"}] indicates if the output should be
357 enclosed in double quotes.
359 \item[@{text "mode = name"}] adds @{text name} to the print mode to
360 be used for presentation (see also \cite{isabelle-ref}). Note that
361 the standard setup for {\LaTeX} output is already present by
362 default, including the modes @{text latex} and @{text xsymbols}.
364 \item[@{text "margin = nat"} and @{text "indent = nat"}] change the
365 margin or indentation for pretty printing of display material.
367 \item[@{text "goals_limit = nat"}] determines the maximum number of
368 goals to be printed (for goal-based antiquotation).
370 \item[@{text "locale = name"}] specifies an alternative locale
371 context used for evaluating and printing the subsequent argument.
373 \item[@{text "source = bool"}] prints the original source text of
374 the antiquotation arguments, rather than its internal
375 representation. Note that formal checking of @{antiquotation
376 "thm"}, @{antiquotation "term"}, etc. is still enabled; use the
377 @{antiquotation "text"} antiquotation for unchecked output.
379 Regular @{text "term"} and @{text "typ"} antiquotations with @{text
380 "source = false"} involve a full round-trip from the original source
381 to an internalized logical entity back to a source form, according
382 to the syntax of the current context. Thus the printed output is
383 not under direct control of the author, it may even fluctuate a bit
384 as the underlying theory is changed later on.
386 In contrast, @{text "source = true"} admits direct printing of the
387 given source text, with the desirable well-formedness check in the
388 background, but without modification of the printed text.
392 For boolean flags, ``@{text "name = true"}'' may be abbreviated as
393 ``@{text name}''. All of the above flags are disabled by default,
394 unless changed from ML, say in the @{verbatim "ROOT.ML"} of the
399 section {* Markup via command tags \label{sec:tags} *}
401 text {* Each Isabelle/Isar command may be decorated by additional
402 presentation tags, to indicate some modification in the way it is
403 printed in the document.
405 \indexouternonterm{tags}
409 tag: '\%' (ident | string)
412 Some tags are pre-declared for certain classes of commands, serving
413 as default markup if no tags are given in the text:
417 @{text "theory"} & theory begin/end \\
418 @{text "proof"} & all proof commands \\
419 @{text "ML"} & all commands involving ML code \\
422 \medskip The Isabelle document preparation system
423 \cite{isabelle-sys} allows tagged command regions to be presented
424 specifically, e.g.\ to fold proof texts, or drop parts of the text
427 For example ``@{command "by"}~@{text "%invisible auto"}'' causes
428 that piece of proof to be treated as @{text invisible} instead of
429 @{text "proof"} (the default), which may be shown or hidden
430 depending on the document setup. In contrast, ``@{command
431 "by"}~@{text "%visible auto"}'' forces this text to be shown
434 Explicit tag specifications within a proof apply to all subsequent
435 commands of the same level of nesting. For example, ``@{command
436 "proof"}~@{text "%visible \<dots>"}~@{command "qed"}'' forces the whole
437 sub-proof to be typeset as @{text visible} (unless some of its parts
438 are tagged differently).
440 \medskip Command tags merely produce certain markup environments for
441 type-setting. The meaning of these is determined by {\LaTeX}
442 macros, as defined in @{"file" "~~/lib/texinputs/isabelle.sty"} or
443 by the document author. The Isabelle document preparation tools
444 also provide some high-level options to specify the meaning of
445 arbitrary tags to ``keep'', ``drop'', or ``fold'' the corresponding
446 parts of the text. Logic sessions may also specify ``document
447 versions'', where given tags are interpreted in some particular way.
448 Again see \cite{isabelle-sys} for further details.
452 section {* Draft presentation *}
455 \begin{matharray}{rcl}
456 @{command_def "display_drafts"}@{text "\<^sup>*"} & : & \isarkeep{\cdot} \\
457 @{command_def "print_drafts"}@{text "\<^sup>*"} & : & \isarkeep{\cdot} \\
461 ('display\_drafts' | 'print\_drafts') (name +)
467 \item [@{command "display_drafts"}~@{text paths} and @{command
468 "print_drafts"}~@{text paths}] perform simple output of a given list
469 of raw source files. Only those symbols that do not require
470 additional {\LaTeX} packages are displayed properly, everything else