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 "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 Apart from formal comments (see \secref{sec:comments}), markup
76 commands provide a structured way to insert text into the document
77 generated from a theory (see \cite{isabelle-sys} for more
78 information on Isabelle's document preparation tools).
81 ('chapter' | 'section' | 'subsection' | 'subsubsection' | 'text') target? text
83 ('header' | 'text\_raw' | 'sect' | 'subsect' | 'subsubsect' | 'txt' | 'txt\_raw') text
89 \item [@{command "header"}~@{text "text"}] provides plain text
90 markup just preceding the formal beginning of a theory. In actual
91 document preparation the corresponding {\LaTeX} macro @{verbatim
92 "\\isamarkupheader"} may be redefined to produce chapter or section
93 headings. See also \secref{sec:markup} for further markup commands.
95 \item [@{command "chapter"}, @{command "section"}, @{command
96 "subsection"}, and @{command "subsubsection"}] mark chapter and
99 \item [@{command "text"} and @{command "txt"}] specify paragraphs of
102 \item [@{command "text_raw"} and @{command "txt_raw"}] insert
103 {\LaTeX} source into the output, without additional markup. Thus
104 the full range of document manipulations becomes available.
108 The @{text "text"} argument of these markup commands (except for
109 @{command "text_raw"}) may contain references to formal entities
110 (``antiquotations'', see also \secref{sec:antiq}). These are
111 interpreted in the present theory context, or the named @{text
114 Any of these markup elements corresponds to a {\LaTeX} command with
115 the name prefixed by @{verbatim "\\isamarkup"}. For the sectioning
116 commands this is a plain macro with a single argument, e.g.\
117 @{verbatim "\\isamarkupchapter{"}@{text "\<dots>"}@{verbatim "}"} for
118 @{command "chapter"}. The @{command "text"} markup results in a
119 {\LaTeX} environment @{verbatim "\\begin{isamarkuptext}"} @{text
120 "\<dots>"} @{verbatim "\\end{isamarkuptext}"}, while @{command "text_raw"}
121 causes the text to be inserted directly into the {\LaTeX} source.
123 \medskip The proof markup commands closely resemble those for theory
124 specifications, but have a different formal status and produce
125 different {\LaTeX} macros. Also note that the @{command_ref
126 "header"} declaration (see \secref{sec:begin-thy}) admits to insert
127 section markup just preceding the actual theory definition.
131 section {* Antiquotations \label{sec:antiq} *}
134 \begin{matharray}{rcl}
135 @{antiquotation_def "theory"} & : & \isarantiq \\
136 @{antiquotation_def "thm"} & : & \isarantiq \\
137 @{antiquotation_def "prop"} & : & \isarantiq \\
138 @{antiquotation_def "term"} & : & \isarantiq \\
139 @{antiquotation_def const} & : & \isarantiq \\
140 @{antiquotation_def abbrev} & : & \isarantiq \\
141 @{antiquotation_def typeof} & : & \isarantiq \\
142 @{antiquotation_def typ} & : & \isarantiq \\
143 @{antiquotation_def thm_style} & : & \isarantiq \\
144 @{antiquotation_def term_style} & : & \isarantiq \\
145 @{antiquotation_def "text"} & : & \isarantiq \\
146 @{antiquotation_def goals} & : & \isarantiq \\
147 @{antiquotation_def subgoals} & : & \isarantiq \\
148 @{antiquotation_def prf} & : & \isarantiq \\
149 @{antiquotation_def full_prf} & : & \isarantiq \\
150 @{antiquotation_def ML} & : & \isarantiq \\
151 @{antiquotation_def ML_type} & : & \isarantiq \\
152 @{antiquotation_def ML_struct} & : & \isarantiq \\
155 The text body of formal comments (see also \secref{sec:comments})
156 may contain antiquotations of logical entities, such as theorems,
157 terms and types, which are to be presented in the final output
158 produced by the Isabelle document preparation system (see also
159 \chref{ch:document-prep}).
161 Thus embedding of ``@{text "@{term [show_types] \"f x = a + x\"}"}''
162 within a text block would cause
163 \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
164 antiquotations may involve attributes as well. For example,
165 @{text "@{thm sym [no_vars]}"} would print the theorem's
166 statement where all schematic variables have been replaced by fixed
167 ones, which are easier to read.
170 atsign lbrace antiquotation rbrace
174 'theory' options name |
175 'thm' options thmrefs |
176 'prop' options prop |
177 'term' options term |
178 'const' options term |
179 'abbrev' options term |
180 'typeof' options term |
182 'thm\_style' options name thmref |
183 'term\_style' options name term |
184 'text' options name |
187 'prf' options thmrefs |
188 'full\_prf' options thmrefs |
190 'ML\_type' options name |
191 'ML\_struct' options name
193 options: '[' (option * ',') ']'
195 option: name | name '=' name
199 Note that the syntax of antiquotations may \emph{not} include source
200 comments @{verbatim "(*"}~@{text "\<dots>"}~@{verbatim "*)"} or verbatim
201 text @{verbatim "{"}@{verbatim "*"}~@{text "\<dots>"}~@{verbatim
206 \item [@{text "@{theory A}"}] prints the name @{text "A"}, which is
207 guaranteed to refer to a valid ancestor theory in the current
210 \item [@{text "@{thm a\<^sub>1 \<dots> a\<^sub>n}"}] prints theorems
211 @{text "a\<^sub>1 \<dots> a\<^sub>n"}. Note that attribute specifications
212 may be included as well (see also \secref{sec:syn-att}); the
213 @{attribute_ref no_vars} rule (see \secref{sec:misc-meth-att}) would
214 be particularly useful to suppress printing of schematic variables.
216 \item [@{text "@{prop \<phi>}"}] prints a well-typed proposition @{text
219 \item [@{text "@{term t}"}] prints a well-typed term @{text "t"}.
221 \item [@{text "@{const c}"}] prints a logical or syntactic constant
224 \item [@{text "@{abbrev c x\<^sub>1 \<dots> x\<^sub>n}"}] prints a constant
225 abbreviation @{text "c x\<^sub>1 \<dots> x\<^sub>n \<equiv> rhs"} as defined in
228 \item [@{text "@{typeof t}"}] prints the type of a well-typed term
231 \item [@{text "@{typ \<tau>}"}] prints a well-formed type @{text "\<tau>"}.
233 \item [@{text "@{thm_style s a}"}] prints theorem @{text a},
234 previously applying a style @{text s} to it (see below).
236 \item [@{text "@{term_style s t}"}] prints a well-typed term @{text
237 t} after applying a style @{text s} to it (see below).
239 \item [@{text "@{text s}"}] prints uninterpreted source text @{text
240 s}. This is particularly useful to print portions of text according
241 to the Isabelle {\LaTeX} output style, without demanding
242 well-formedness (e.g.\ small pieces of terms that should not be
243 parsed or type-checked yet).
245 \item [@{text "@{goals}"}] prints the current \emph{dynamic} goal
246 state. This is mainly for support of tactic-emulation scripts
247 within Isar --- presentation of goal states does not conform to
248 actual human-readable proof documents.
250 Please do not include goal states into document output unless you
251 really know what you are doing!
253 \item [@{text "@{subgoals}"}] is similar to @{text "@{goals}"}, but
254 does not print the main goal.
256 \item [@{text "@{prf a\<^sub>1 \<dots> a\<^sub>n}"}] prints the (compact)
257 proof terms corresponding to the theorems @{text "a\<^sub>1 \<dots>
258 a\<^sub>n"}. Note that this requires proof terms to be switched on
259 for the current object logic (see the ``Proof terms'' section of the
260 Isabelle reference manual for information on how to do this).
262 \item [@{text "@{full_prf a\<^sub>1 \<dots> a\<^sub>n}"}] is like @{text
263 "@{prf a\<^sub>1 \<dots> a\<^sub>n}"}, but displays the full proof terms,
264 i.e.\ also displays information omitted in the compact proof term,
265 which is denoted by ``@{text _}'' placeholders there.
267 \item [@{text "@{ML s}"}, @{text "@{ML_type s}"}, and @{text
268 "@{ML_struct s}"}] check text @{text s} as ML value, type, and
269 structure, respectively. The source is displayed verbatim.
273 \medskip The following standard styles for use with @{text
274 thm_style} and @{text term_style} are available:
278 \item [@{text lhs}] extracts the first argument of any application
279 form with at least two arguments -- typically meta-level or
280 object-level equality, or any other binary relation.
282 \item [@{text rhs}] is like @{text lhs}, but extracts the second
285 \item [@{text "concl"}] extracts the conclusion @{text C} from a rule
286 in Horn-clause normal form @{text "A\<^sub>1 \<Longrightarrow> \<dots> A\<^sub>n \<Longrightarrow> C"}.
288 \item [@{text "prem1"}, \dots, @{text "prem9"}] extract premise
289 number @{text "1, \<dots>, 9"}, respectively, from from a rule in
290 Horn-clause normal form @{text "A\<^sub>1 \<Longrightarrow> \<dots> A\<^sub>n \<Longrightarrow> C"}
295 The following options are available to tune the output. Note that most of
296 these coincide with ML flags of the same names (see also \cite{isabelle-ref}).
300 \item[@{text "show_types = bool"} and @{text "show_sorts = bool"}]
301 control printing of explicit type and sort constraints.
303 \item[@{text "show_structs = bool"}] controls printing of implicit
306 \item[@{text "long_names = bool"}] forces names of types and
307 constants etc.\ to be printed in their fully qualified internal
310 \item[@{text "short_names = bool"}] forces names of types and
311 constants etc.\ to be printed unqualified. Note that internalizing
312 the output again in the current context may well yield a different
315 \item[@{text "unique_names = bool"}] determines whether the printed
316 version of qualified names should be made sufficiently long to avoid
317 overlap with names declared further back. Set to @{text false} for
320 \item[@{text "eta_contract = bool"}] prints terms in @{text
321 \<eta>}-contracted form.
323 \item[@{text "display = bool"}] indicates if the text is to be
324 output as multi-line ``display material'', rather than a small piece
325 of text without line breaks (which is the default).
327 \item[@{text "break = bool"}] controls line breaks in non-display
330 \item[@{text "quotes = bool"}] indicates if the output should be
331 enclosed in double quotes.
333 \item[@{text "mode = name"}] adds @{text name} to the print mode to
334 be used for presentation (see also \cite{isabelle-ref}). Note that
335 the standard setup for {\LaTeX} output is already present by
336 default, including the modes @{text latex} and @{text xsymbols}.
338 \item[@{text "margin = nat"} and @{text "indent = nat"}] change the
339 margin or indentation for pretty printing of display material.
341 \item[@{text "source = bool"}] prints the source text of the
342 antiquotation arguments, rather than the actual value. Note that
343 this does not affect well-formedness checks of @{antiquotation
344 "thm"}, @{antiquotation "term"}, etc. (only the @{antiquotation
345 "text"} antiquotation admits arbitrary output).
347 \item[@{text "goals_limit = nat"}] determines the maximum number of
350 \item[@{text "locale = name"}] specifies an alternative locale
351 context used for evaluating and printing the subsequent argument.
355 For boolean flags, ``@{text "name = true"}'' may be abbreviated as
356 ``@{text name}''. All of the above flags are disabled by default,
357 unless changed from ML.
359 \medskip Note that antiquotations do not only spare the author from
360 tedious typing of logical entities, but also achieve some degree of
361 consistency-checking of informal explanations with formal
362 developments: well-formedness of terms and types with respect to the
363 current theory or proof context is ensured here.
367 section {* Tagged commands \label{sec:tags} *}
370 Each Isabelle/Isar command may be decorated by presentation tags:
372 \indexouternonterm{tags}
376 tag: '\%' (ident | string)
379 The tags @{text "theory"}, @{text "proof"}, @{text "ML"} are already
380 pre-declared for certain classes of commands:
385 @{text "theory"} & theory begin/end \\
386 @{text "proof"} & all proof commands \\
387 @{text "ML"} & all commands involving ML code \\
390 \medskip The Isabelle document preparation system (see also
391 \cite{isabelle-sys}) allows tagged command regions to be presented
392 specifically, e.g.\ to fold proof texts, or drop parts of the text
395 For example ``@{command "by"}~@{text "%invisible auto"}'' would
396 cause that piece of proof to be treated as @{text invisible} instead
397 of @{text "proof"} (the default), which may be either show or hidden
398 depending on the document setup. In contrast, ``@{command
399 "by"}~@{text "%visible auto"}'' would force this text to be shown
402 Explicit tag specifications within a proof apply to all subsequent
403 commands of the same level of nesting. For example, ``@{command
404 "proof"}~@{text "%visible \<dots>"}~@{command "qed"}'' would force the
405 whole sub-proof to be typeset as @{text visible} (unless some of its
406 parts are tagged differently).
410 section {* Draft presentation *}
413 \begin{matharray}{rcl}
414 @{command_def "display_drafts"}@{text "\<^sup>*"} & : & \isarkeep{\cdot} \\
415 @{command_def "print_drafts"}@{text "\<^sup>*"} & : & \isarkeep{\cdot} \\
419 ('display\_drafts' | 'print\_drafts') (name +)
425 \item [@{command "display_drafts"}~@{text paths} and @{command
426 "print_drafts"}~@{text paths}] perform simple output of a given list
427 of raw source files. Only those symbols that do not require
428 additional {\LaTeX} packages are displayed properly, everything else