1 theory Document_Preparation
5 chapter {* Document preparation \label{ch:document-prep} *}
7 text {* Isabelle/Isar provides a simple document preparation system
8 based on regular {PDF-\LaTeX} technology, with full support for
9 hyper-links and bookmarks. Thus the results are well suited for WWW
10 browsing and as printed copies.
12 \medskip Isabelle generates {\LaTeX} output while running a
13 \emph{logic session} (see also \cite{isabelle-sys}). Getting
14 started with a working configuration for common situations is quite
15 easy by using the Isabelle @{verbatim mkdir} and @{verbatim make}
20 to initialize a separate directory for session @{verbatim Foo} (it
21 is safe to experiment, since @{verbatim "isabelle mkdir"} never
22 overwrites existing files). Ensure that @{verbatim "Foo/ROOT.ML"}
23 holds ML commands to load all theories required for this session;
24 furthermore @{verbatim "Foo/document/root.tex"} should include any
25 special {\LaTeX} macro packages required for your document (the
26 default is usually sufficient as a start).
28 The session is controlled by a separate @{verbatim IsaMakefile}
29 (with crude source dependencies by default). This file is located
30 one level up from the @{verbatim Foo} directory location. Now
35 to run the @{verbatim Foo} session, with browser information and
36 document preparation enabled. Unless any errors are reported by
37 Isabelle or {\LaTeX}, the output will appear inside the directory
38 defined by the @{verbatim ISABELLE_BROWSER_INFO} setting (as
39 reported by the batch job in verbose mode).
41 \medskip You may also consider to tune the @{verbatim usedir}
42 options in @{verbatim IsaMakefile}, for example to switch the output
43 format between @{verbatim pdf} and @{verbatim dvi}, or activate the
44 @{verbatim "-D"} option to retain a second copy of the generated
45 {\LaTeX} sources (for manual inspection or separate runs of
48 \medskip See \emph{The Isabelle System Manual} \cite{isabelle-sys}
49 for further details on Isabelle logic sessions and theory
50 presentation. The Isabelle/HOL tutorial \cite{isabelle-hol-book}
51 also covers theory presentation to some extent.
55 section {* Markup commands \label{sec:markup} *}
58 \begin{matharray}{rcl}
59 @{command_def "header"} & : & @{text "toplevel \<rightarrow> toplevel"} \\[0.5ex]
60 @{command_def "chapter"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
61 @{command_def "section"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
62 @{command_def "subsection"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
63 @{command_def "subsubsection"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
64 @{command_def "text"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
65 @{command_def "text_raw"} & : & @{text "local_theory \<rightarrow> local_theory"} \\[0.5ex]
66 @{command_def "sect"} & : & @{text "proof \<rightarrow> proof"} \\
67 @{command_def "subsect"} & : & @{text "proof \<rightarrow> proof"} \\
68 @{command_def "subsubsect"} & : & @{text "proof \<rightarrow> proof"} \\
69 @{command_def "txt"} & : & @{text "proof \<rightarrow> proof"} \\
70 @{command_def "txt_raw"} & : & @{text "proof \<rightarrow> proof"} \\
73 Markup commands provide a structured way to insert text into the
74 document generated from a theory. Each markup command takes a
75 single @{syntax text} argument, which is passed as argument to a
76 corresponding {\LaTeX} macro. The default macros provided by
77 @{"file" "~~/lib/texinputs/isabelle.sty"} can be redefined according
78 to the needs of the underlying document and {\LaTeX} styles.
80 Note that formal comments (\secref{sec:comments}) are similar to
81 markup commands, but have a different status within Isabelle/Isar
85 ('chapter' | 'section' | 'subsection' | 'subsubsection' | 'text') target? text
87 ('header' | 'text\_raw' | 'sect' | 'subsect' | 'subsubsect' | 'txt' | 'txt\_raw') text
93 \item @{command header} provides plain text markup just preceding
94 the formal beginning of a theory. The corresponding {\LaTeX} macro
95 is @{verbatim "\\isamarkupheader"}, which acts like @{command
98 \item @{command chapter}, @{command section}, @{command subsection},
99 and @{command subsubsection} mark chapter and section headings
100 within the main theory body or local theory targets. The
101 corresponding {\LaTeX} macros are @{verbatim "\\isamarkupchapter"},
102 @{verbatim "\\isamarkupsection"}, @{verbatim
103 "\\isamarkupsubsection"} etc.
105 \item @{command sect}, @{command subsect}, and @{command subsubsect}
106 mark section headings within proofs. The corresponding {\LaTeX}
107 macros are @{verbatim "\\isamarkupsect"}, @{verbatim
108 "\\isamarkupsubsect"} etc.
110 \item @{command text} and @{command txt} specify paragraphs of plain
111 text. This corresponds to a {\LaTeX} environment @{verbatim
112 "\\begin{isamarkuptext}"} @{text "\<dots>"} @{verbatim
113 "\\end{isamarkuptext}"} etc.
115 \item @{command text_raw} and @{command txt_raw} insert {\LaTeX}
116 source into the output, without additional markup. Thus the full
117 range of document manipulations becomes available, at the risk of
118 messing up document output.
122 Except for @{command "text_raw"} and @{command "txt_raw"}, the text
123 passed to any of the above markup commands may refer to formal
124 entities via \emph{document antiquotations}, see also
125 \secref{sec:antiq}. These are interpreted in the present theory or
126 proof context, or the named @{text "target"}.
128 \medskip The proof markup commands closely resemble those for theory
129 specifications, but have a different formal status and produce
130 different {\LaTeX} macros. The default definitions coincide for
131 analogous commands such as @{command section} and @{command sect}.
135 section {* Document Antiquotations \label{sec:antiq} *}
138 \begin{matharray}{rcl}
139 @{antiquotation_def "theory"} & : & @{text antiquotation} \\
140 @{antiquotation_def "thm"} & : & @{text antiquotation} \\
141 @{antiquotation_def "lemma"} & : & @{text antiquotation} \\
142 @{antiquotation_def "prop"} & : & @{text antiquotation} \\
143 @{antiquotation_def "term"} & : & @{text antiquotation} \\
144 @{antiquotation_def term_type} & : & @{text antiquotation} \\
145 @{antiquotation_def typeof} & : & @{text antiquotation} \\
146 @{antiquotation_def const} & : & @{text antiquotation} \\
147 @{antiquotation_def abbrev} & : & @{text antiquotation} \\
148 @{antiquotation_def typ} & : & @{text antiquotation} \\
149 @{antiquotation_def "text"} & : & @{text antiquotation} \\
150 @{antiquotation_def goals} & : & @{text antiquotation} \\
151 @{antiquotation_def subgoals} & : & @{text antiquotation} \\
152 @{antiquotation_def prf} & : & @{text antiquotation} \\
153 @{antiquotation_def full_prf} & : & @{text antiquotation} \\
154 @{antiquotation_def ML} & : & @{text antiquotation} \\
155 @{antiquotation_def ML_type} & : & @{text antiquotation} \\
156 @{antiquotation_def ML_struct} & : & @{text antiquotation} \\
159 The overall content of an Isabelle/Isar theory may alternate between
160 formal and informal text. The main body consists of formal
161 specification and proof commands, interspersed with markup commands
162 (\secref{sec:markup}) or document comments (\secref{sec:comments}).
163 The argument of markup commands quotes informal text to be printed
164 in the resulting document, but may again refer to formal entities
165 via \emph{document antiquotations}.
167 For example, embedding of ``@{text [source=false] "@{term [show_types] \"f x = a + x\"}"}''
168 within a text block makes
169 \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.
171 Antiquotations usually spare the author tedious typing of logical
172 entities in full detail. Even more importantly, some degree of
173 consistency-checking between the main body of formal text and its
174 informal explanation is achieved, since terms and types appearing in
175 antiquotations are checked within the current theory or proof
179 atsign lbrace antiquotation rbrace
183 'theory' options name |
184 'thm' options styles thmrefs |
185 'lemma' options prop 'by' method |
186 'prop' options styles prop |
187 'term' options styles term |
188 'term_type' options styles term |
189 'typeof' options styles term |
190 'const' options term |
191 'abbrev' options term |
193 'text' options name |
196 'prf' options thmrefs |
197 'full\_prf' options thmrefs |
199 'ML\_type' options name |
200 'ML\_struct' options name
202 options: '[' (option * ',') ']'
204 option: name | name '=' name
206 styles: '(' (style + ',') ')'
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 "@{term_type t}"} prints a well-typed term @{text "t"}
236 annotated with its type.
238 \item @{text "@{typeof t}"} prints the type of a well-typed term
241 \item @{text "@{const c}"} prints a logical or syntactic constant
244 \item @{text "@{abbrev c x\<^sub>1 \<dots> x\<^sub>n}"} prints a constant abbreviation
245 @{text "c x\<^sub>1 \<dots> x\<^sub>n \<equiv> rhs"} as defined in the current context.
246 \item @{text "@{typ \<tau>}"} prints a well-formed type @{text "\<tau>"}.
248 \item @{text "@{text s}"} prints uninterpreted source text @{text
249 s}. This is particularly useful to print portions of text according
250 to the Isabelle document style, without demanding well-formedness,
251 e.g.\ small pieces of terms that should not be parsed or
254 \item @{text "@{goals}"} prints the current \emph{dynamic} goal
255 state. This is mainly for support of tactic-emulation scripts
256 within Isar. Presentation of goal states does not conform to the
257 idea of human-readable proof documents!
259 When explaining proofs in detail it is usually better to spell out
260 the reasoning via proper Isar proof commands, instead of peeking at
261 the internal machine configuration.
263 \item @{text "@{subgoals}"} is similar to @{text "@{goals}"}, but
264 does not print the main goal.
266 \item @{text "@{prf a\<^sub>1 \<dots> a\<^sub>n}"} prints the (compact) proof terms
267 corresponding to the theorems @{text "a\<^sub>1 \<dots> a\<^sub>n"}. Note that this
268 requires proof terms to be switched on for the current logic
271 \item @{text "@{full_prf a\<^sub>1 \<dots> a\<^sub>n}"} is like @{text "@{prf a\<^sub>1 \<dots>
272 a\<^sub>n}"}, but prints the full proof terms, i.e.\ also displays
273 information omitted in the compact proof term, which is denoted by
274 ``@{text _}'' placeholders there.
276 \item @{text "@{ML s}"}, @{text "@{ML_type s}"}, and @{text
277 "@{ML_struct s}"} check text @{text s} as ML value, type, and
278 structure, respectively. The source is printed verbatim.
284 subsubsection {* Styled antiquotations *}
286 text {* The antiquotations @{text thm}, @{text prop} and @{text
287 term} admit an extra \emph{style} specification to modify the
288 printed result. A style is specified by a name with a possibly
289 empty number of arguments; multiple styles can be sequenced with
290 commas. The following standard styles are available:
294 \item @{text lhs} extracts the first argument of any application
295 form with at least two arguments --- typically meta-level or
296 object-level equality, or any other binary relation.
298 \item @{text rhs} is like @{text lhs}, but extracts the second
301 \item @{text "concl"} extracts the conclusion @{text C} from a rule
302 in Horn-clause normal form @{text "A\<^sub>1 \<Longrightarrow> \<dots> A\<^sub>n \<Longrightarrow> C"}.
304 \item @{text "prem"} @{text n} extract premise number
305 @{text "n"} from from a rule in Horn-clause
306 normal form @{text "A\<^sub>1 \<Longrightarrow> \<dots> A\<^sub>n \<Longrightarrow> C"}
312 subsubsection {* General options *}
314 text {* The following options are available to tune the printed output
315 of antiquotations. Note that many of these coincide with global ML
316 flags of the same names.
320 \item @{antiquotation_option_def show_types}~@{text "= bool"} and
321 @{antiquotation_option_def show_sorts}~@{text "= bool"} control
322 printing of explicit type and sort constraints.
324 \item @{antiquotation_option_def show_structs}~@{text "= bool"}
325 controls printing of implicit structures.
327 \item @{antiquotation_option_def long_names}~@{text "= bool"} forces
328 names of types and constants etc.\ to be printed in their fully
329 qualified internal form.
331 \item @{antiquotation_option_def short_names}~@{text "= bool"}
332 forces names of types and constants etc.\ to be printed unqualified.
333 Note that internalizing the output again in the current context may
334 well yield a different result.
336 \item @{antiquotation_option_def unique_names}~@{text "= bool"}
337 determines whether the printed version of qualified names should be
338 made sufficiently long to avoid overlap with names declared further
339 back. Set to @{text false} for more concise output.
341 \item @{antiquotation_option_def eta_contract}~@{text "= bool"}
342 prints terms in @{text \<eta>}-contracted form.
344 \item @{antiquotation_option_def display}~@{text "= bool"} indicates
345 if the text is to be output as multi-line ``display material'',
346 rather than a small piece of text without line breaks (which is the
349 In this mode the embedded entities are printed in the same style as
350 the main theory text.
352 \item @{antiquotation_option_def break}~@{text "= bool"} controls
353 line breaks in non-display material.
355 \item @{antiquotation_option_def quotes}~@{text "= bool"} indicates
356 if the output should be enclosed in double quotes.
358 \item @{antiquotation_option_def mode}~@{text "= name"} adds @{text
359 name} to the print mode to be used for presentation. Note that the
360 standard setup for {\LaTeX} output is already present by default,
361 including the modes @{text latex} and @{text xsymbols}.
363 \item @{antiquotation_option_def margin}~@{text "= nat"} and
364 @{antiquotation_option_def indent}~@{text "= nat"} change the margin
365 or indentation for pretty printing of display material.
367 \item @{antiquotation_option_def goals_limit}~@{text "= nat"}
368 determines the maximum number of goals to be printed (for goal-based
371 \item @{antiquotation_option_def source}~@{text "= bool"} prints the
372 original source text of the antiquotation arguments, rather than its
373 internal representation. Note that formal checking of
374 @{antiquotation "thm"}, @{antiquotation "term"}, etc. is still
375 enabled; use the @{antiquotation "text"} antiquotation for unchecked
378 Regular @{text "term"} and @{text "typ"} antiquotations with @{text
379 "source = false"} involve a full round-trip from the original source
380 to an internalized logical entity back to a source form, according
381 to the syntax of the current context. Thus the printed output is
382 not under direct control of the author, it may even fluctuate a bit
383 as the underlying theory is changed later on.
385 In contrast, @{antiquotation_option_def source}~@{text "= true"}
386 admits direct printing of the given source text, with the desirable
387 well-formedness check in the background, but without modification of
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>*"} & : & @{text "any \<rightarrow>"} \\
457 @{command_def "print_drafts"}@{text "\<^sup>*"} & : & @{text "any \<rightarrow>"} \\
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