3 theory Document_Preparation
7 chapter {* Document preparation \label{ch:document-prep} *}
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.
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}
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).
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
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
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
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.
57 section {* Markup commands \label{sec:markup} *}
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} \\
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).
80 ('chapter' | 'section' | 'subsection' | 'subsubsection' | 'text') target? text
82 ('text\_raw' | 'sect' | 'subsect' | 'subsubsect' | 'txt' | 'txt\_raw') text
88 \item [@{command "chapter"}, @{command "section"}, @{command
89 "subsection"}, and @{command "subsubsection"}] mark chapter and
92 \item [@{command "text"} and @{command "txt"}] specify paragraphs of
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.
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
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.
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.
124 section {* Antiquotations \label{sec:antiq} *}
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 \\
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}).
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.
163 atsign lbrace antiquotation rbrace
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 |
175 'thm\_style' options name thmref |
176 'term\_style' options name term |
177 'text' options name |
180 'prf' options thmrefs |
181 'full\_prf' options thmrefs |
183 'ML\_type' options name |
184 'ML\_struct' options name
186 options: '[' (option * ',') ']'
188 option: name | name '=' name
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
199 \item [@{text "@{theory A}"}] prints the name @{text "A"}, which is
200 guaranteed to refer to a valid ancestor theory in the current
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.
209 \item [@{text "@{prop \<phi>}"}] prints a well-typed proposition @{text
212 \item [@{text "@{term t}"}] prints a well-typed term @{text "t"}.
214 \item [@{text "@{const c}"}] prints a logical or syntactic constant
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
221 \item [@{text "@{typeof t}"}] prints the type of a well-typed term
224 \item [@{text "@{typ \<tau>}"}] prints a well-formed type @{text "\<tau>"}.
226 \item [@{text "@{thm_style s a}"}] prints theorem @{text a},
227 previously applying a style @{text s} to it (see below).
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).
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).
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.
243 Please do not include goal states into document output unless you
244 really know what you are doing!
246 \item [@{text "@{subgoals}"}] is similar to @{text "@{goals}"}, but
247 does not print the main goal.
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).
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.
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.
266 \medskip The following standard styles for use with @{text
267 thm_style} and @{text term_style} are available:
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.
275 \item [@{text rhs}] is like @{text lhs}, but extracts the second
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"}.
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"}
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}).
293 \item[@{text "show_types = bool"} and @{text "show_sorts = bool"}]
294 control printing of explicit type and sort constraints.
296 \item[@{text "show_structs = bool"}] controls printing of implicit
299 \item[@{text "long_names = bool"}] forces names of types and
300 constants etc.\ to be printed in their fully qualified internal
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
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
313 \item[@{text "eta_contract = bool"}] prints terms in @{text
314 \<eta>}-contracted form.
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).
320 \item[@{text "break = bool"}] controls line breaks in non-display
323 \item[@{text "quotes = bool"}] indicates if the output should be
324 enclosed in double quotes.
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}.
331 \item[@{text "margin = nat"} and @{text "indent = nat"}] change the
332 margin or indentation for pretty printing of display material.
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).
340 \item[@{text "goals_limit = nat"}] determines the maximum number of
343 \item[@{text "locale = name"}] specifies an alternative locale
344 context used for evaluating and printing the subsequent argument.
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.
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.
360 section {* Tagged commands \label{sec:tags} *}
363 Each Isabelle/Isar command may be decorated by presentation tags:
365 \indexouternonterm{tags}
369 tag: '\%' (ident | string)
372 The tags @{text "theory"}, @{text "proof"}, @{text "ML"} are already
373 pre-declared for certain classes of commands:
378 @{text "theory"} & theory begin/end \\
379 @{text "proof"} & all proof commands \\
380 @{text "ML"} & all commands involving ML code \\
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
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
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).
403 section {* Draft presentation *}
406 \begin{matharray}{rcl}
407 @{command_def "display_drafts"}@{text "\<^sup>*"} & : & \isarkeep{\cdot} \\
408 @{command_def "print_drafts"}@{text "\<^sup>*"} & : & \isarkeep{\cdot} \\
412 ('display\_drafts' | 'print\_drafts') (name +)
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