--- a/doc-src/TutorialI/Documents/Documents.thy Sat Jan 05 21:41:38 2002 +0100
+++ b/doc-src/TutorialI/Documents/Documents.thy Sat Jan 05 21:42:01 2002 +0100
@@ -7,11 +7,10 @@
text {*
Concerning Isabelle's ``inner'' language of simply-typed @{text
\<lambda>}-calculus, the core concept of Isabelle's elaborate infrastructure
- for concrete syntax is that of general \emph{mixfix
- annotations}\index{mixfix annotations|bold}. Associated with any
- kind of name and type declaration, mixfixes give rise both to
- grammar productions for the parser and output templates for the
- pretty printer.
+ for concrete syntax is that of general \bfindex{mixfix annotations}.
+ Associated with any kind of name and type declaration, mixfixes give
+ rise both to grammar productions for the parser and output templates
+ for the pretty printer.
In full generality, the whole affair of parser and pretty printer
configuration is rather subtle. Any syntax specifications given by
@@ -26,7 +25,7 @@
*}
-subsection {* Infixes *}
+subsection {* Infix annotations *}
text {*
Syntax annotations may be included wherever constants are declared
@@ -36,11 +35,11 @@
well, although this is less frequently encountered in practice
(@{text "*"} and @{text "+"} types may come to mind).
- Infix declarations\index{infix annotations|bold} provide a useful
- special case of mixfixes, where users need not care about the full
- details of priorities, nesting, spacing, etc. The subsequent
- example of the exclusive-or operation on boolean values illustrates
- typical infix declarations.
+ Infix declarations\index{infix annotations} provide a useful special
+ case of mixfixes, where users need not care about the full details
+ of priorities, nesting, spacing, etc. The subsequent example of the
+ exclusive-or operation on boolean values illustrates typical infix
+ declarations.
*}
constdefs
@@ -116,11 +115,10 @@
proposed over decades, but none has become universally available so
far, not even Unicode\index{Unicode}.
- Isabelle supports a generic notion of
- \emph{symbols}\index{symbols|bold} as the smallest entities of
- source text, without referring to internal encodings. Such
- ``generalized characters'' may be of one of the following three
- kinds:
+ Isabelle supports a generic notion of \bfindex{symbols} as the
+ smallest entities of source text, without referring to internal
+ encodings. Such ``generalized characters'' may be of one of the
+ following three kinds:
\begin{enumerate}
@@ -172,10 +170,10 @@
immediately after continuing further input.
\medskip A slightly more refined scheme is to provide alternative
- syntax via the \emph{print mode}\index{print mode} concept of
- Isabelle (see also \cite{isabelle-ref}). By convention, the mode
- ``$xsymbols$'' is enabled whenever X-Symbol is active. Consider the
- following hybrid declaration of @{text xor}.
+ syntax via the \bfindex{print mode} concept of Isabelle (see also
+ \cite{isabelle-ref}). By convention, the mode ``$xsymbols$'' is
+ enabled whenever X-Symbol is active. Consider the following hybrid
+ declaration of @{text xor}.
*}
(*<*)
@@ -224,13 +222,13 @@
xor :: "bool \<Rightarrow> bool \<Rightarrow> bool" (infixl "\<oplus>\<ignore>" 60)
-subsection {* Prefixes *}
+subsection {* Prefix annotations *}
text {*
- Prefix syntax annotations\index{prefix annotation|bold} are just a
- very degenerate of the general mixfix form \cite{isabelle-ref},
- without any template arguments or priorities --- just some piece of
- literal syntax.
+ Prefix syntax annotations\index{prefix annotation} are just a very
+ degenerate of the general mixfix form \cite{isabelle-ref}, without
+ any template arguments or priorities --- just some piece of literal
+ syntax.
The following example illustrates this idea idea by associating
common symbols with the constructors of a currency datatype.
@@ -246,30 +244,25 @@
Here the degenerate mixfix annotations on the rightmost column
happen to consist of a single Isabelle symbol each:
\verb,\,\verb,<euro>,, \verb,\,\verb,<pounds>,,
- \verb,\,\verb,<yen>,, and \verb,$,.
+ \verb,\,\verb,<yen>,, \verb,$,.
Recall that a constructor like @{text Euro} actually is a function
@{typ "nat \<Rightarrow> currency"}. An expression like @{text "Euro 10"} will
- be printed as @{term "\<euro> 10"}. Merely the head of the application is
- subject to our trivial concrete syntax; this form is sufficient to
- achieve fair conformance to EU~Commission standards of currency
- notation.
+ be printed as @{term "\<euro> 10"}. Only the head of the application is
+ subject to our concrete syntax; this simple form already achieves
+ conformance with notational standards of the European Commission.
\medskip Certainly, the same idea of prefix syntax also works for
\isakeyword{consts}, \isakeyword{constdefs} etc. For example, we
might introduce a (slightly unrealistic) function to calculate an
abstract currency value, by cases on the datatype constructors and
- fixed exchange rates.
+ fixed exchange rates. The funny symbol used here is that of
+ \verb,\<currency>,.
*}
consts
currency :: "currency \<Rightarrow> nat" ("\<currency>")
-text {*
- \noindent The funny symbol encountered here is that of
- \verb,\<currency>,.
-*}
-
subsection {* Syntax translations \label{sec:def-translations} *}
@@ -309,18 +302,239 @@
section {* Document preparation *}
-subsection {* Batch-mode sessions *}
-
-subsection {* {\LaTeX} macros *}
+text {*
+ Isabelle/Isar is centered around a certain notion of \bfindex{formal
+ proof documents}\index{documents|bold}: ultimately the result of the
+ user's theory development efforts is a human-readable record --- as
+ a browsable PDF file or printed on paper. The overall document
+ structure follows traditional mathematical articles, with
+ sectioning, explanations, definitions, theorem statements, and
+ proofs.
-subsubsection {* Structure markup *}
+ The Isar proof language \cite{Wenzel-PhD}, which is not covered in
+ this book, admits to write formal proof texts that are acceptable
+ both to the machine and human readers at the same time. Thus
+ marginal comments and explanations may be kept at a minimum.
+ Nevertheless, Isabelle document output is still useful without
+ actual Isar proof texts; formal specifications usually deserve their
+ own coverage in the text, while unstructured proof scripts may be
+ just ignore by readers (or intentionally suppressed from the text).
-subsubsection {* Symbols and characters *}
+ \medskip The Isabelle document preparation system essentially acts
+ like a formal front-end for {\LaTeX}. After checking definitions
+ and proofs the theory sources are turned into typesetting
+ instructions, so the final document is known to observe quite strong
+ ``soundness'' properties. This enables users to write authentic
+ reports on formal theory developments with little additional effort,
+ the most tedious consistency checks are handled by the system.
+*}
+
+
+subsection {* Isabelle sessions *}
text {*
- FIXME
+ In contrast to the highly interactive mode of the formal parts of
+ Isabelle/Isar theory development, the document preparation stage
+ essentially works in batch-mode. This revolves around the concept
+ of a \bfindex{session}, which essentially consists of a collection
+ of theory source files that contribute to a single output document.
+ Each session is derived from a parent one (usually an object-logic
+ image such as \texttt{HOL}); this results in an overall tree
+ structure of Isabelle sessions.
+
+ The canonical arrangement of source files of a session called
+ \texttt{MySession} is as follows:
+
+ \begin{itemize}
+
+ \item Directory \texttt{MySession} contains the required theory
+ files, say $A@1$\texttt{.thy}, \dots, $A@n$\texttt{.thy}.
+
+ \item File \texttt{MySession/ROOT.ML} holds appropriate ML commands
+ for loading all wanted theories, usually just
+ \texttt{use_thy~"$A@i$"} for any $A@i$ in leaf position of the
+ theory dependency graph.
+
+ \item Directory \texttt{MySession/document} contains everything
+ required for the {\LaTeX} stage, but only \texttt{root.tex} needs to
+ be provided initially. The latter file holds appropriate {\LaTeX}
+ code to commence a document (\verb,\documentclass, etc.), and to
+ include the generated files $A@i$\texttt{.tex} for each theory. The
+ generated file \texttt{session.tex} holds {\LaTeX} commands to
+ include \emph{all} theory output files in topologically sorted
+ order.
+
+ \item In addition an \texttt{IsaMakefile} outside of directory
+ \texttt{MySession} holds appropriate dependencies and invocations of
+ Isabelle tools to control the batch job. The details are covered in
+ \cite{isabelle-sys}; \texttt{isatool usedir} is the most important
+ entry point.
+
+ \end{itemize}
+
+ With everything put in its proper place, \texttt{isatool make}
+ should be sufficient to process the Isabelle session completely,
+ with the generated document appearing in its proper place (within
+ \verb,~/isabelle/browser_info,).
+
+ In practive, users may want to have \texttt{isatool mkdir} generate
+ an initial working setup without further ado. For example, an empty
+ session \texttt{MySession} derived from \texttt{HOL} may be produced
+ as follows:
+
+\begin{verbatim}
+ isatool mkdir HOL MySession
+ isatool make
+\end{verbatim}
+
+ This runs the session with sensible default options, including
+ verbose mode to tell the user where the result will appear. The
+ above dry run should produce should produce a single page of output
+ (with a dummy title, empty table of contents etc.). Any failure at
+ that stage is likely to indicate some technical problems with your
+ {\LaTeX} installation.\footnote{Especially make sure that
+ \texttt{pdflatex} is present.}
+
+ \medskip Users may now start to populate the directory
+ \texttt{MySession}, and the file \texttt{MySession/ROOT.ML}
+ accordingly. \texttt{MySession/document/root.tex} should be also
+ adapted at some point; the generated version is mostly
+ self-explanatory.
+
+ Realistic applications may demand additional files in
+ \texttt{MySession/document} for the {\LaTeX} stage, such as
+ \texttt{root.bib} for the bibliographic database.\footnote{Using
+ that particular name of \texttt{root.bib}, the Isabelle document
+ processor (actually \texttt{isatool document} \cite{isabelle-sys})
+ will be smart enough to invoke \texttt{bibtex} accordingly.}
+
+ \medskip Failure of the document preparation phase in an Isabelle
+ batch session leaves the generated sources in there target location
+ (as pointed out by the accompanied error message). In case of
+ {\LaTeX} errors, users may trace error messages at the file position
+ of the generated text.
+*}
+
+
+subsection {* Structure markup *}
+
+subsubsection {* Sections *}
+
+text {*
+ The large-scale structure of Isabelle documents closely follows
+ {\LaTeX} convention, with chapters, sections, subsubsections etc.
+ The formal Isar language includes separate structure \bfindex{markup
+ commands}, which do not effect the formal content of a theory (or
+ proof), but results in corresponding {\LaTeX} elements issued to the
+ output.
-
+ There are different markup commands for different formal contexts:
+ in header position (just before a \isakeyword{theory} command),
+ within the theory body, or within a proof. Note that the header
+ needs to be treated specially, since ordinary theory and proof
+ commands may only occur \emph{after} the initial \isakeyword{theory}
+ specification.
+
+ \smallskip
+
+ \begin{tabular}{llll}
+ header & theory & proof & default meaning \\\hline
+ & \commdx{chapter} & & \verb,\chapter, \\
+ \commdx{header} & \commdx{section} & \commdx{sect} & \verb,\section, \\
+ & \commdx{subsection} & \commdx{subsect} & \verb,\subsection, \\
+ & \commdx{subsubsection} & \commdx{subsubsect} & \verb,\subsubsection, \\
+ \end{tabular}
+
+ \medskip
+
+ From the Isabelle perspective, each markup command takes a single
+ text argument (delimited by \verb,",\dots\verb,", or
+ \verb,{,\verb,*,~\dots~\verb,*,\verb,},). After stripping
+ surrounding white space, the argument is passed to a {\LaTeX} macro
+ \verb,\isamarkupXXX, for any command \isakeyword{XXX}. The latter
+ are defined in \verb,isabelle.sty, according to the rightmost column
+ above.
+
+ \medskip The following source fragment illustrates structure markup
+ of a theory.
+
+ \begin{ttbox}
+ header {\ttlbrace}* Some properties of Foo Bar elements *{\ttrbrace}
+
+ theory Foo_Bar = Main:
+
+ subsection {\ttlbrace}* Basic definitions *{\ttrbrace}
+
+ consts
+ foo :: \dots
+ bar :: \dots
+ defs \dots
+
+ subsection {\ttlbrace}* Derived rules *{\ttrbrace}
+
+ lemma fooI: \dots
+ lemma fooE: \dots
+
+ subsection {\ttlbrace}* Main theorem *{\ttrbrace}
+
+ theorem main: \dots
+
+ end
+ \end{ttbox}
+
+ \medskip In realistic applications, users may well want to change
+ the meaning of some markup commands, typically via appropriate use
+ of \verb,\renewcommand, in \texttt{root.tex}. The
+ \verb,\isamarkupheader, is a good candidate for some adaption, e.g.\
+ moving it up in the hierarchy to become \verb,\chapter,.
+
+\begin{verbatim}
+ \renewcommand{\isamarkupheader}[1]{\chapter{#1}}
+\end{verbatim}
+
+ Certainly, this requires to change the default
+ \verb,\documentclass{article}, in \texttt{root.tex} to something
+ that supports the notion of chapters in the first place, e.g.\
+ \texttt{report} or \texttt{book}.
+
+ \medskip For each generated theory output the {\LaTeX} macro
+ \verb,\isabellecontext, holds the name of the formal context. This
+ is particularly useful for document headings or footings, e.g.\ like
+ this:
+
+\begin{verbatim}
+ \renewcommand{\isamarkupheader}[1]%
+ {\chapter{#1}\markright{THEORY~\isabellecontext}}
+\end{verbatim}
+
+ \noindent Make sure to include something like
+ \verb,\pagestyle{headings}, in \texttt{root.tex} as well. Moreover,
+ the document should have more than 2 pages.
+*}
+
+
+subsection {* Formal comments and antiquotations *}
+
+text {*
+ Comments of the form \verb,(*,~\dots~\verb,*),
+
+*}
+
+
+subsection {* Symbols and characters *}
+
+text {*
+ FIXME \verb,\isabellestyle,
+*}
+
+
+subsection {* Suppressing output *}
+
+text {*
+ FIXME \verb,no_document,
+
+ FIXME \verb,(,\verb,*,\verb,<,\verb,*,\verb,),
+ \verb,(,\verb,*,\verb,>,\verb,*,\verb,),
*}
(*<*)