1.1 --- a/doc-src/TutorialI/Documents/document/Documents.tex Sat Jan 05 21:41:11 2002 +0100
1.2 +++ b/doc-src/TutorialI/Documents/document/Documents.tex Sat Jan 05 21:41:38 2002 +0100
1.3 @@ -9,11 +9,10 @@
1.4 %
1.5 \begin{isamarkuptext}%
1.6 Concerning Isabelle's ``inner'' language of simply-typed \isa{{\isasymlambda}}-calculus, the core concept of Isabelle's elaborate infrastructure
1.7 - for concrete syntax is that of general \emph{mixfix
1.8 - annotations}\index{mixfix annotations|bold}. Associated with any
1.9 - kind of name and type declaration, mixfixes give rise both to
1.10 - grammar productions for the parser and output templates for the
1.11 - pretty printer.
1.12 + for concrete syntax is that of general \bfindex{mixfix annotations}.
1.13 + Associated with any kind of name and type declaration, mixfixes give
1.14 + rise both to grammar productions for the parser and output templates
1.15 + for the pretty printer.
1.16
1.17 In full generality, the whole affair of parser and pretty printer
1.18 configuration is rather subtle. Any syntax specifications given by
1.19 @@ -28,7 +27,7 @@
1.20 \end{isamarkuptext}%
1.21 \isamarkuptrue%
1.22 %
1.23 -\isamarkupsubsection{Infixes%
1.24 +\isamarkupsubsection{Infix annotations%
1.25 }
1.26 \isamarkuptrue%
1.27 %
1.28 @@ -40,11 +39,11 @@
1.29 well, although this is less frequently encountered in practice
1.30 (\isa{{\isacharasterisk}} and \isa{{\isacharplus}} types may come to mind).
1.31
1.32 - Infix declarations\index{infix annotations|bold} provide a useful
1.33 - special case of mixfixes, where users need not care about the full
1.34 - details of priorities, nesting, spacing, etc. The subsequent
1.35 - example of the exclusive-or operation on boolean values illustrates
1.36 - typical infix declarations.%
1.37 + Infix declarations\index{infix annotations} provide a useful special
1.38 + case of mixfixes, where users need not care about the full details
1.39 + of priorities, nesting, spacing, etc. The subsequent example of the
1.40 + exclusive-or operation on boolean values illustrates typical infix
1.41 + declarations.%
1.42 \end{isamarkuptext}%
1.43 \isamarkuptrue%
1.44 \isacommand{constdefs}\isanewline
1.45 @@ -120,11 +119,10 @@
1.46 proposed over decades, but none has become universally available so
1.47 far, not even Unicode\index{Unicode}.
1.48
1.49 - Isabelle supports a generic notion of
1.50 - \emph{symbols}\index{symbols|bold} as the smallest entities of
1.51 - source text, without referring to internal encodings. Such
1.52 - ``generalized characters'' may be of one of the following three
1.53 - kinds:
1.54 + Isabelle supports a generic notion of \bfindex{symbols} as the
1.55 + smallest entities of source text, without referring to internal
1.56 + encodings. Such ``generalized characters'' may be of one of the
1.57 + following three kinds:
1.58
1.59 \begin{enumerate}
1.60
1.61 @@ -172,10 +170,10 @@
1.62 immediately after continuing further input.
1.63
1.64 \medskip A slightly more refined scheme is to provide alternative
1.65 - syntax via the \emph{print mode}\index{print mode} concept of
1.66 - Isabelle (see also \cite{isabelle-ref}). By convention, the mode
1.67 - ``$xsymbols$'' is enabled whenever X-Symbol is active. Consider the
1.68 - following hybrid declaration of \isa{xor}.%
1.69 + syntax via the \bfindex{print mode} concept of Isabelle (see also
1.70 + \cite{isabelle-ref}). By convention, the mode ``$xsymbols$'' is
1.71 + enabled whenever X-Symbol is active. Consider the following hybrid
1.72 + declaration of \isa{xor}.%
1.73 \end{isamarkuptext}%
1.74 \isamarkuptrue%
1.75 \isamarkupfalse%
1.76 @@ -220,15 +218,15 @@
1.77 \isacommand{syntax}\ {\isacharparenleft}xsymbols\ \isakeyword{output}{\isacharparenright}\isanewline
1.78 \ \ xor\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}bool\ {\isasymRightarrow}\ bool\ {\isasymRightarrow}\ bool{\isachardoublequote}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequote}{\isasymoplus}{\isasymignore}{\isachardoublequote}\ {\isadigit{6}}{\isadigit{0}}{\isacharparenright}\isamarkupfalse%
1.79 %
1.80 -\isamarkupsubsection{Prefixes%
1.81 +\isamarkupsubsection{Prefix annotations%
1.82 }
1.83 \isamarkuptrue%
1.84 %
1.85 \begin{isamarkuptext}%
1.86 -Prefix syntax annotations\index{prefix annotation|bold} are just a
1.87 - very degenerate of the general mixfix form \cite{isabelle-ref},
1.88 - without any template arguments or priorities --- just some piece of
1.89 - literal syntax.
1.90 +Prefix syntax annotations\index{prefix annotation} are just a very
1.91 + degenerate of the general mixfix form \cite{isabelle-ref}, without
1.92 + any template arguments or priorities --- just some piece of literal
1.93 + syntax.
1.94
1.95 The following example illustrates this idea idea by associating
1.96 common symbols with the constructors of a currency datatype.%
1.97 @@ -244,31 +242,25 @@
1.98 Here the degenerate mixfix annotations on the rightmost column
1.99 happen to consist of a single Isabelle symbol each:
1.100 \verb,\,\verb,<euro>,, \verb,\,\verb,<pounds>,,
1.101 - \verb,\,\verb,<yen>,, and \verb,$,.
1.102 + \verb,\,\verb,<yen>,, \verb,$,.
1.103
1.104 Recall that a constructor like \isa{Euro} actually is a function
1.105 \isa{nat\ {\isasymRightarrow}\ currency}. An expression like \isa{Euro\ {\isadigit{1}}{\isadigit{0}}} will
1.106 - be printed as \isa{{\isasymeuro}\ {\isadigit{1}}{\isadigit{0}}}. Merely the head of the application is
1.107 - subject to our trivial concrete syntax; this form is sufficient to
1.108 - achieve fair conformance to EU~Commission standards of currency
1.109 - notation.
1.110 + be printed as \isa{{\isasymeuro}\ {\isadigit{1}}{\isadigit{0}}}. Only the head of the application is
1.111 + subject to our concrete syntax; this simple form already achieves
1.112 + conformance with notational standards of the European Commission.
1.113
1.114 \medskip Certainly, the same idea of prefix syntax also works for
1.115 \isakeyword{consts}, \isakeyword{constdefs} etc. For example, we
1.116 might introduce a (slightly unrealistic) function to calculate an
1.117 abstract currency value, by cases on the datatype constructors and
1.118 - fixed exchange rates.%
1.119 + fixed exchange rates. The funny symbol used here is that of
1.120 + \verb,\<currency>,.%
1.121 \end{isamarkuptext}%
1.122 \isamarkuptrue%
1.123 \isacommand{consts}\isanewline
1.124 \ \ currency\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}currency\ {\isasymRightarrow}\ nat{\isachardoublequote}\ \ \ \ {\isacharparenleft}{\isachardoublequote}{\isasymcurrency}{\isachardoublequote}{\isacharparenright}\isamarkupfalse%
1.125 %
1.126 -\begin{isamarkuptext}%
1.127 -\noindent The funny symbol encountered here is that of
1.128 - \verb,\<currency>,.%
1.129 -\end{isamarkuptext}%
1.130 -\isamarkuptrue%
1.131 -%
1.132 \isamarkupsubsection{Syntax translations \label{sec:def-translations}%
1.133 }
1.134 \isamarkuptrue%
1.135 @@ -312,24 +304,250 @@
1.136 }
1.137 \isamarkuptrue%
1.138 %
1.139 -\isamarkupsubsection{Batch-mode sessions%
1.140 -}
1.141 +\begin{isamarkuptext}%
1.142 +Isabelle/Isar is centered around a certain notion of \bfindex{formal
1.143 + proof documents}\index{documents|bold}: ultimately the result of the
1.144 + user's theory development efforts is a human-readable record --- as
1.145 + a browsable PDF file or printed on paper. The overall document
1.146 + structure follows traditional mathematical articles, with
1.147 + sectioning, explanations, definitions, theorem statements, and
1.148 + proofs.
1.149 +
1.150 + The Isar proof language \cite{Wenzel-PhD}, which is not covered in
1.151 + this book, admits to write formal proof texts that are acceptable
1.152 + both to the machine and human readers at the same time. Thus
1.153 + marginal comments and explanations may be kept at a minimum.
1.154 + Nevertheless, Isabelle document output is still useful without
1.155 + actual Isar proof texts; formal specifications usually deserve their
1.156 + own coverage in the text, while unstructured proof scripts may be
1.157 + just ignore by readers (or intentionally suppressed from the text).
1.158 +
1.159 + \medskip The Isabelle document preparation system essentially acts
1.160 + like a formal front-end for {\LaTeX}. After checking definitions
1.161 + and proofs the theory sources are turned into typesetting
1.162 + instructions, so the final document is known to observe quite strong
1.163 + ``soundness'' properties. This enables users to write authentic
1.164 + reports on formal theory developments with little additional effort,
1.165 + the most tedious consistency checks are handled by the system.%
1.166 +\end{isamarkuptext}%
1.167 \isamarkuptrue%
1.168 %
1.169 -\isamarkupsubsection{{\LaTeX} macros%
1.170 -}
1.171 -\isamarkuptrue%
1.172 -%
1.173 -\isamarkupsubsubsection{Structure markup%
1.174 -}
1.175 -\isamarkuptrue%
1.176 -%
1.177 -\isamarkupsubsubsection{Symbols and characters%
1.178 +\isamarkupsubsection{Isabelle sessions%
1.179 }
1.180 \isamarkuptrue%
1.181 %
1.182 \begin{isamarkuptext}%
1.183 -FIXME%
1.184 +In contrast to the highly interactive mode of the formal parts of
1.185 + Isabelle/Isar theory development, the document preparation stage
1.186 + essentially works in batch-mode. This revolves around the concept
1.187 + of a \bfindex{session}, which essentially consists of a collection
1.188 + of theory source files that contribute to a single output document.
1.189 + Each session is derived from a parent one (usually an object-logic
1.190 + image such as \texttt{HOL}); this results in an overall tree
1.191 + structure of Isabelle sessions.
1.192 +
1.193 + The canonical arrangement of source files of a session called
1.194 + \texttt{MySession} is as follows:
1.195 +
1.196 + \begin{itemize}
1.197 +
1.198 + \item Directory \texttt{MySession} contains the required theory
1.199 + files, say $A@1$\texttt{.thy}, \dots, $A@n$\texttt{.thy}.
1.200 +
1.201 + \item File \texttt{MySession/ROOT.ML} holds appropriate ML commands
1.202 + for loading all wanted theories, usually just
1.203 + \texttt{use_thy~"$A@i$"} for any $A@i$ in leaf position of the
1.204 + theory dependency graph.
1.205 +
1.206 + \item Directory \texttt{MySession/document} contains everything
1.207 + required for the {\LaTeX} stage, but only \texttt{root.tex} needs to
1.208 + be provided initially. The latter file holds appropriate {\LaTeX}
1.209 + code to commence a document (\verb,\documentclass, etc.), and to
1.210 + include the generated files $A@i$\texttt{.tex} for each theory. The
1.211 + generated file \texttt{session.tex} holds {\LaTeX} commands to
1.212 + include \emph{all} theory output files in topologically sorted
1.213 + order.
1.214 +
1.215 + \item In addition an \texttt{IsaMakefile} outside of directory
1.216 + \texttt{MySession} holds appropriate dependencies and invocations of
1.217 + Isabelle tools to control the batch job. The details are covered in
1.218 + \cite{isabelle-sys}; \texttt{isatool usedir} is the most important
1.219 + entry point.
1.220 +
1.221 + \end{itemize}
1.222 +
1.223 + With everything put in its proper place, \texttt{isatool make}
1.224 + should be sufficient to process the Isabelle session completely,
1.225 + with the generated document appearing in its proper place (within
1.226 + \verb,~/isabelle/browser_info,).
1.227 +
1.228 + In practive, users may want to have \texttt{isatool mkdir} generate
1.229 + an initial working setup without further ado. For example, an empty
1.230 + session \texttt{MySession} derived from \texttt{HOL} may be produced
1.231 + as follows:
1.232 +
1.233 +\begin{verbatim}
1.234 + isatool mkdir HOL MySession
1.235 + isatool make
1.236 +\end{verbatim}
1.237 +
1.238 + This runs the session with sensible default options, including
1.239 + verbose mode to tell the user where the result will appear. The
1.240 + above dry run should produce should produce a single page of output
1.241 + (with a dummy title, empty table of contents etc.). Any failure at
1.242 + that stage is likely to indicate some technical problems with your
1.243 + {\LaTeX} installation.\footnote{Especially make sure that
1.244 + \texttt{pdflatex} is present.}
1.245 +
1.246 + \medskip Users may now start to populate the directory
1.247 + \texttt{MySession}, and the file \texttt{MySession/ROOT.ML}
1.248 + accordingly. \texttt{MySession/document/root.tex} should be also
1.249 + adapted at some point; the generated version is mostly
1.250 + self-explanatory.
1.251 +
1.252 + Realistic applications may demand additional files in
1.253 + \texttt{MySession/document} for the {\LaTeX} stage, such as
1.254 + \texttt{root.bib} for the bibliographic database.\footnote{Using
1.255 + that particular name of \texttt{root.bib}, the Isabelle document
1.256 + processor (actually \texttt{isatool document} \cite{isabelle-sys})
1.257 + will be smart enough to invoke \texttt{bibtex} accordingly.}
1.258 +
1.259 + \medskip Failure of the document preparation phase in an Isabelle
1.260 + batch session leaves the generated sources in there target location
1.261 + (as pointed out by the accompanied error message). In case of
1.262 + {\LaTeX} errors, users may trace error messages at the file position
1.263 + of the generated text.%
1.264 +\end{isamarkuptext}%
1.265 +\isamarkuptrue%
1.266 +%
1.267 +\isamarkupsubsection{Structure markup%
1.268 +}
1.269 +\isamarkuptrue%
1.270 +%
1.271 +\isamarkupsubsubsection{Sections%
1.272 +}
1.273 +\isamarkuptrue%
1.274 +%
1.275 +\begin{isamarkuptext}%
1.276 +The large-scale structure of Isabelle documents closely follows
1.277 + {\LaTeX} convention, with chapters, sections, subsubsections etc.
1.278 + The formal Isar language includes separate structure \bfindex{markup
1.279 + commands}, which do not effect the formal content of a theory (or
1.280 + proof), but results in corresponding {\LaTeX} elements issued to the
1.281 + output.
1.282 +
1.283 + There are different markup commands for different formal contexts:
1.284 + in header position (just before a \isakeyword{theory} command),
1.285 + within the theory body, or within a proof. Note that the header
1.286 + needs to be treated specially, since ordinary theory and proof
1.287 + commands may only occur \emph{after} the initial \isakeyword{theory}
1.288 + specification.
1.289 +
1.290 + \smallskip
1.291 +
1.292 + \begin{tabular}{llll}
1.293 + header & theory & proof & default meaning \\\hline
1.294 + & \commdx{chapter} & & \verb,\chapter, \\
1.295 + \commdx{header} & \commdx{section} & \commdx{sect} & \verb,\section, \\
1.296 + & \commdx{subsection} & \commdx{subsect} & \verb,\subsection, \\
1.297 + & \commdx{subsubsection} & \commdx{subsubsect} & \verb,\subsubsection, \\
1.298 + \end{tabular}
1.299 +
1.300 + \medskip
1.301 +
1.302 + From the Isabelle perspective, each markup command takes a single
1.303 + text argument (delimited by \verb,",\dots\verb,", or
1.304 + \verb,{,\verb,*,~\dots~\verb,*,\verb,},). After stripping
1.305 + surrounding white space, the argument is passed to a {\LaTeX} macro
1.306 + \verb,\isamarkupXXX, for any command \isakeyword{XXX}. The latter
1.307 + are defined in \verb,isabelle.sty, according to the rightmost column
1.308 + above.
1.309 +
1.310 + \medskip The following source fragment illustrates structure markup
1.311 + of a theory.
1.312 +
1.313 + \begin{ttbox}
1.314 + header {\ttlbrace}* Some properties of Foo Bar elements *{\ttrbrace}
1.315 +
1.316 + theory Foo_Bar = Main:
1.317 +
1.318 + subsection {\ttlbrace}* Basic definitions *{\ttrbrace}
1.319 +
1.320 + consts
1.321 + foo :: \dots
1.322 + bar :: \dots
1.323 + defs \dots
1.324 +
1.325 + subsection {\ttlbrace}* Derived rules *{\ttrbrace}
1.326 +
1.327 + lemma fooI: \dots
1.328 + lemma fooE: \dots
1.329 +
1.330 + subsection {\ttlbrace}* Main theorem *{\ttrbrace}
1.331 +
1.332 + theorem main: \dots
1.333 +
1.334 + end
1.335 + \end{ttbox}
1.336 +
1.337 + \medskip In realistic applications, users may well want to change
1.338 + the meaning of some markup commands, typically via appropriate use
1.339 + of \verb,\renewcommand, in \texttt{root.tex}. The
1.340 + \verb,\isamarkupheader, is a good candidate for some adaption, e.g.\
1.341 + moving it up in the hierarchy to become \verb,\chapter,.
1.342 +
1.343 +\begin{verbatim}
1.344 + \renewcommand{\isamarkupheader}[1]{\chapter{#1}}
1.345 +\end{verbatim}
1.346 +
1.347 + Certainly, this requires to change the default
1.348 + \verb,\documentclass{article}, in \texttt{root.tex} to something
1.349 + that supports the notion of chapters in the first place, e.g.\
1.350 + \texttt{report} or \texttt{book}.
1.351 +
1.352 + \medskip For each generated theory output the {\LaTeX} macro
1.353 + \verb,\isabellecontext, holds the name of the formal context. This
1.354 + is particularly useful for document headings or footings, e.g.\ like
1.355 + this:
1.356 +
1.357 +\begin{verbatim}
1.358 + \renewcommand{\isamarkupheader}[1]%
1.359 + {\chapter{#1}\markright{THEORY~\isabellecontext}}
1.360 +\end{verbatim}
1.361 +
1.362 + \noindent Make sure to include something like
1.363 + \verb,\pagestyle{headings}, in \texttt{root.tex} as well. Moreover,
1.364 + the document should have more than 2 pages.%
1.365 +\end{isamarkuptext}%
1.366 +\isamarkuptrue%
1.367 +%
1.368 +\isamarkupsubsection{Formal comments and antiquotations%
1.369 +}
1.370 +\isamarkuptrue%
1.371 +%
1.372 +\begin{isamarkuptext}%
1.373 +Comments of the form \verb,(*,~\dots~\verb,*),%
1.374 +\end{isamarkuptext}%
1.375 +\isamarkuptrue%
1.376 +%
1.377 +\isamarkupsubsection{Symbols and characters%
1.378 +}
1.379 +\isamarkuptrue%
1.380 +%
1.381 +\begin{isamarkuptext}%
1.382 +FIXME \verb,\isabellestyle,%
1.383 +\end{isamarkuptext}%
1.384 +\isamarkuptrue%
1.385 +%
1.386 +\isamarkupsubsection{Suppressing output%
1.387 +}
1.388 +\isamarkuptrue%
1.389 +%
1.390 +\begin{isamarkuptext}%
1.391 +FIXME \verb,no_document,
1.392 +
1.393 + FIXME \verb,(,\verb,*,\verb,<,\verb,*,\verb,),
1.394 + \verb,(,\verb,*,\verb,>,\verb,*,\verb,),%
1.395 \end{isamarkuptext}%
1.396 \isamarkuptrue%
1.397 \isamarkupfalse%