doc-src/TutorialI/Documents/Documents.thy
author wenzelm
Sun Oct 09 15:46:06 2011 +0200 (2011-10-09 ago)
changeset 45106 3498077f2012
parent 38765 5aa8e5e770a8
child 47822 34b44d28fc4b
permissions -rw-r--r--
updated ISABELLE_HOME_USER;
     1 (*<*)
     2 theory Documents imports Main begin
     3 (*>*)
     4 
     5 section {* Concrete Syntax \label{sec:concrete-syntax} *}
     6 
     7 text {*
     8   The core concept of Isabelle's framework for concrete syntax is that
     9   of \bfindex{mixfix annotations}.  Associated with any kind of
    10   constant declaration, mixfixes affect both the grammar productions
    11   for the parser and output templates for the pretty printer.
    12 
    13   In full generality, parser and pretty printer configuration is a
    14   subtle affair~\cite{isabelle-ref}.  Your syntax specifications need
    15   to interact properly with the existing setup of Isabelle/Pure and
    16   Isabelle/HOL\@.  To avoid creating ambiguities with existing
    17   elements, it is particularly important to give new syntactic
    18   constructs the right precedence.
    19 
    20   Below we introduce a few simple syntax declaration
    21   forms that already cover many common situations fairly well.
    22 *}
    23 
    24 
    25 subsection {* Infix Annotations *}
    26 
    27 text {*
    28   Syntax annotations may be included wherever constants are declared,
    29   such as \isacommand{definition} and \isacommand{primrec} --- and also
    30   \isacommand{datatype}, which declares constructor operations.
    31   Type-constructors may be annotated as well, although this is less
    32   frequently encountered in practice (the infix type @{text "\<times>"} comes
    33   to mind).
    34 
    35   Infix declarations\index{infix annotations} provide a useful special
    36   case of mixfixes.  The following example of the exclusive-or
    37   operation on boolean values illustrates typical infix declarations.
    38 *}
    39 
    40 definition xor :: "bool \<Rightarrow> bool \<Rightarrow> bool"    (infixl "[+]" 60)
    41 where "A [+] B \<equiv> (A \<and> \<not> B) \<or> (\<not> A \<and> B)"
    42 
    43 text {*
    44   \noindent Now @{text "xor A B"} and @{text "A [+] B"} refer to the
    45   same expression internally.  Any curried function with at least two
    46   arguments may be given infix syntax.  For partial applications with
    47   fewer than two operands, there is a notation using the prefix~@{text
    48   op}.  For instance, @{text xor} without arguments is represented as
    49   @{text "op [+]"}; together with ordinary function application, this
    50   turns @{text "xor A"} into @{text "op [+] A"}.
    51 
    52   The keyword \isakeyword{infixl} seen above specifies an
    53   infix operator that is nested to the \emph{left}: in iterated
    54   applications the more complex expression appears on the left-hand
    55   side, and @{term "A [+] B [+] C"} stands for @{text "(A [+] B) [+]
    56   C"}.  Similarly, \isakeyword{infixr} means nesting to the
    57   \emph{right}, reading @{term "A [+] B [+] C"} as @{text "A [+] (B
    58   [+] C)"}.  A \emph{non-oriented} declaration via \isakeyword{infix}
    59   would render @{term "A [+] B [+] C"} illegal, but demand explicit
    60   parentheses to indicate the intended grouping.
    61 
    62   The string @{text [source] "[+]"} in our annotation refers to the
    63   concrete syntax to represent the operator (a literal token), while
    64   the number @{text 60} determines the precedence of the construct:
    65   the syntactic priorities of the arguments and result.  Isabelle/HOL
    66   already uses up many popular combinations of ASCII symbols for its
    67   own use, including both @{text "+"} and @{text "++"}.  Longer
    68   character combinations are more likely to be still available for
    69   user extensions, such as our~@{text "[+]"}.
    70 
    71   Operator precedences have a range of 0--1000.  Very low or high
    72   priorities are reserved for the meta-logic.  HOL syntax mainly uses
    73   the range of 10--100: the equality infix @{text "="} is centered at
    74   50; logical connectives (like @{text "\<or>"} and @{text "\<and>"}) are
    75   below 50; algebraic ones (like @{text "+"} and @{text "*"}) are
    76   above 50.  User syntax should strive to coexist with common HOL
    77   forms, or use the mostly unused range 100--900.
    78 *}
    79 
    80 
    81 subsection {* Mathematical Symbols \label{sec:syntax-symbols} *}
    82 
    83 text {*
    84   Concrete syntax based on ASCII characters has inherent limitations.
    85   Mathematical notation demands a larger repertoire of glyphs.
    86   Several standards of extended character sets have been proposed over
    87   decades, but none has become universally available so far.  Isabelle
    88   has its own notion of \bfindex{symbols} as the smallest entities of
    89   source text, without referring to internal encodings.  There are
    90   three kinds of such ``generalized characters'':
    91 
    92   \begin{enumerate}
    93 
    94   \item 7-bit ASCII characters
    95 
    96   \item named symbols: \verb,\,\verb,<,$ident$\verb,>,
    97 
    98   \item named control symbols: \verb,\,\verb,<^,$ident$\verb,>,
    99 
   100   \end{enumerate}
   101 
   102   Here $ident$ is any sequence of letters. 
   103   This results in an infinite store of symbols, whose
   104   interpretation is left to further front-end tools.  For example, the
   105   user-interface of Proof~General + X-Symbol and the Isabelle document
   106   processor (see \S\ref{sec:document-preparation}) display the
   107   \verb,\,\verb,<forall>, symbol as~@{text \<forall>}.
   108 
   109   A list of standard Isabelle symbols is given in
   110   \cite{isabelle-isar-ref}.  You may introduce your own
   111   interpretation of further symbols by configuring the appropriate
   112   front-end tool accordingly, e.g.\ by defining certain {\LaTeX}
   113   macros (see also \S\ref{sec:doc-prep-symbols}).  There are also a
   114   few predefined control symbols, such as \verb,\,\verb,<^sub>, and
   115   \verb,\,\verb,<^sup>, for sub- and superscript of the subsequent
   116   printable symbol, respectively.  For example, \verb,A\<^sup>\<star>, is
   117   output as @{text "A\<^sup>\<star>"}.
   118 
   119   A number of symbols are considered letters by the Isabelle lexer and
   120   can be used as part of identifiers. These are the greek letters
   121   @{text "\<alpha>"} (\verb+\+\verb+<alpha>+), @{text "\<beta>"}
   122   (\verb+\+\verb+<beta>+), etc. (excluding @{text "\<lambda>"}),
   123   special letters like @{text "\<A>"} (\verb+\+\verb+<A>+) and @{text
   124   "\<AA>"} (\verb+\+\verb+<AA>+), and the control symbols
   125   \verb+\+\verb+<^isub>+ and \verb+\+\verb+<^isup>+ for single letter
   126   sub and super scripts. This means that the input
   127 
   128   \medskip
   129   {\small\noindent \verb,\,\verb,<forall>\,\verb,<alpha>\<^isub>1.,~\verb,\,\verb,<alpha>\<^isub>1 = \,\verb,<Pi>\<^isup>\<A>,}
   130 
   131   \medskip
   132   \noindent is recognized as the term @{term "\<forall>\<alpha>\<^isub>1. \<alpha>\<^isub>1 = \<Pi>\<^isup>\<A>"} 
   133   by Isabelle. Note that @{text "\<Pi>\<^isup>\<A>"} is a single
   134   syntactic entity, not an exponentiation.
   135 
   136   Replacing our previous definition of @{text xor} by the
   137   following specifies an Isabelle symbol for the new operator:
   138 *}
   139 
   140 (*<*)
   141 hide_const xor
   142 setup {* Sign.add_path "version1" *}
   143 (*>*)
   144 definition xor :: "bool \<Rightarrow> bool \<Rightarrow> bool"    (infixl "\<oplus>" 60)
   145 where "A \<oplus> B \<equiv> (A \<and> \<not> B) \<or> (\<not> A \<and> B)"
   146 (*<*)
   147 setup {* Sign.local_path *}
   148 (*>*)
   149 
   150 text {*
   151   \noindent The X-Symbol package within Proof~General provides several
   152   input methods to enter @{text \<oplus>} in the text.  If all fails one may
   153   just type a named entity \verb,\,\verb,<oplus>, by hand; the
   154   corresponding symbol will be displayed after further input.
   155 
   156   More flexible is to provide alternative syntax forms
   157   through the \bfindex{print mode} concept~\cite{isabelle-ref}.  By
   158   convention, the mode of ``$xsymbols$'' is enabled whenever
   159   Proof~General's X-Symbol mode or {\LaTeX} output is active.  Now
   160   consider the following hybrid declaration of @{text xor}:
   161 *}
   162 
   163 (*<*)
   164 hide_const xor
   165 setup {* Sign.add_path "version2" *}
   166 (*>*)
   167 definition xor :: "bool \<Rightarrow> bool \<Rightarrow> bool"    (infixl "[+]\<ignore>" 60)
   168 where "A [+]\<ignore> B \<equiv> (A \<and> \<not> B) \<or> (\<not> A \<and> B)"
   169 
   170 notation (xsymbols) xor (infixl "\<oplus>\<ignore>" 60)
   171 (*<*)
   172 setup {* Sign.local_path *}
   173 (*>*)
   174 
   175 text {*\noindent
   176 The \commdx{notation} command associates a mixfix
   177 annotation with a known constant.  The print mode specification,
   178 here @{text "(xsymbols)"}, is optional.
   179 
   180 We may now write @{text "A [+] B"} or @{text "A \<oplus> B"} in input, while
   181 output uses the nicer syntax of $xsymbols$ whenever that print mode is
   182 active.  Such an arrangement is particularly useful for interactive
   183 development, where users may type ASCII text and see mathematical
   184 symbols displayed during proofs.  *}
   185 
   186 
   187 subsection {* Prefix Annotations *}
   188 
   189 text {*
   190   Prefix syntax annotations\index{prefix annotation} are another form
   191   of mixfixes \cite{isabelle-ref}, without any template arguments or
   192   priorities --- just some literal syntax.  The following example
   193   associates common symbols with the constructors of a datatype.
   194 *}
   195 
   196 datatype currency =
   197     Euro nat    ("\<euro>")
   198   | Pounds nat  ("\<pounds>")
   199   | Yen nat     ("\<yen>")
   200   | Dollar nat  ("$")
   201 
   202 text {*
   203   \noindent Here the mixfix annotations on the rightmost column happen
   204   to consist of a single Isabelle symbol each: \verb,\,\verb,<euro>,,
   205   \verb,\,\verb,<pounds>,, \verb,\,\verb,<yen>,, and \verb,$,.  Recall
   206   that a constructor like @{text Euro} actually is a function @{typ
   207   "nat \<Rightarrow> currency"}.  The expression @{text "Euro 10"} will be
   208   printed as @{term "\<euro> 10"}; only the head of the application is
   209   subject to our concrete syntax.  This rather simple form already
   210   achieves conformance with notational standards of the European
   211   Commission.
   212 
   213   Prefix syntax works the same way for other commands that introduce new constants, e.g. \isakeyword{primrec}.
   214 *}
   215 
   216 
   217 subsection {* Abbreviations \label{sec:abbreviations} *}
   218 
   219 text{* Mixfix syntax annotations merely decorate particular constant
   220 application forms with concrete syntax, for instance replacing
   221 @{text "xor A B"} by @{text "A \<oplus> B"}.  Occasionally, the relationship
   222 between some piece of notation and its internal form is more
   223 complicated.  Here we need \emph{abbreviations}.
   224 
   225 Command \commdx{abbreviation} introduces an uninterpreted notational
   226 constant as an abbreviation for a complex term. Abbreviations are
   227 unfolded upon parsing and re-introduced upon printing. This provides a
   228 simple mechanism for syntactic macros.
   229 
   230 A typical use of abbreviations is to introduce relational notation for
   231 membership in a set of pairs, replacing @{text "(x, y) \<in> sim"} by
   232 @{text "x \<approx> y"}. We assume that a constant @{text sim } of type
   233 @{typ"('a \<times> 'a) set"} has been introduced at this point. *}
   234 (*<*)consts sim :: "('a \<times> 'a) set"(*>*)
   235 abbreviation sim2 :: "'a \<Rightarrow> 'a \<Rightarrow> bool"   (infix "\<approx>" 50)
   236 where "x \<approx> y  \<equiv>  (x, y) \<in> sim"
   237 
   238 text {* \noindent The given meta-equality is used as a rewrite rule
   239 after parsing (replacing \mbox{@{prop"x \<approx> y"}} by @{text"(x,y) \<in>
   240 sim"}) and before printing (turning @{text"(x,y) \<in> sim"} back into
   241 \mbox{@{prop"x \<approx> y"}}). The name of the dummy constant @{text "sim2"}
   242 does not matter, as long as it is unique.
   243 
   244 Another common application of abbreviations is to
   245 provide variant versions of fundamental relational expressions, such
   246 as @{text \<noteq>} for negated equalities.  The following declaration
   247 stems from Isabelle/HOL itself:
   248 *}
   249 
   250 abbreviation not_equal :: "'a \<Rightarrow> 'a \<Rightarrow> bool"    (infixl "~=\<ignore>" 50)
   251 where "x ~=\<ignore> y  \<equiv>  \<not> (x = y)"
   252 
   253 notation (xsymbols) not_equal (infix "\<noteq>\<ignore>" 50)
   254 
   255 text {* \noindent The notation @{text \<noteq>} is introduced separately to restrict it
   256 to the \emph{xsymbols} mode.
   257 
   258 Abbreviations are appropriate when the defined concept is a
   259 simple variation on an existing one.  But because of the automatic
   260 folding and unfolding of abbreviations, they do not scale up well to
   261 large hierarchies of concepts. Abbreviations do not replace
   262 definitions.
   263 
   264 Abbreviations are a simplified form of the general concept of
   265 \emph{syntax translations}; even heavier transformations may be
   266 written in ML \cite{isabelle-ref}.
   267 *}
   268 
   269 
   270 section {* Document Preparation \label{sec:document-preparation} *}
   271 
   272 text {*
   273   Isabelle/Isar is centered around the concept of \bfindex{formal
   274   proof documents}\index{documents|bold}.  The outcome of a formal
   275   development effort is meant to be a human-readable record, presented
   276   as browsable PDF file or printed on paper.  The overall document
   277   structure follows traditional mathematical articles, with sections,
   278   intermediate explanations, definitions, theorems and proofs.
   279 
   280   \medskip The Isabelle document preparation system essentially acts
   281   as a front-end to {\LaTeX}.  After checking specifications and
   282   proofs formally, the theory sources are turned into typesetting
   283   instructions in a schematic manner.  This lets you write authentic
   284   reports on theory developments with little effort: many technical
   285   consistency checks are handled by the system.
   286 
   287   Here is an example to illustrate the idea of Isabelle document
   288   preparation.
   289 *}
   290 
   291 text_raw {* \begin{quotation} *}
   292 
   293 text {*
   294   The following datatype definition of @{text "'a bintree"} models
   295   binary trees with nodes being decorated by elements of type @{typ
   296   'a}.
   297 *}
   298 
   299 datatype 'a bintree =
   300      Leaf | Branch 'a  "'a bintree"  "'a bintree"
   301 
   302 text {*
   303   \noindent The datatype induction rule generated here is of the form
   304   @{thm [indent = 1, display] bintree.induct [no_vars]}
   305 *}
   306 
   307 text_raw {* \end{quotation} *}
   308 
   309 text {*
   310   \noindent The above document output has been produced as follows:
   311 
   312   \begin{ttbox}
   313   text {\ttlbrace}*
   314     The following datatype definition of {\at}{\ttlbrace}text "'a bintree"{\ttrbrace}
   315     models binary trees with nodes being decorated by elements
   316     of type {\at}{\ttlbrace}typ 'a{\ttrbrace}.
   317   *{\ttrbrace}
   318 
   319   datatype 'a bintree =
   320     Leaf | Branch 'a  "'a bintree"  "'a bintree"
   321   \end{ttbox}
   322   \begin{ttbox}
   323   text {\ttlbrace}*
   324     {\ttback}noindent The datatype induction rule generated here is
   325     of the form {\at}{\ttlbrace}thm [display] bintree.induct [no_vars]{\ttrbrace}
   326   *{\ttrbrace}
   327   \end{ttbox}\vspace{-\medskipamount}
   328 
   329   \noindent Here we have augmented the theory by formal comments
   330   (using \isakeyword{text} blocks), the informal parts may again refer
   331   to formal entities by means of ``antiquotations'' (such as
   332   \texttt{\at}\verb,{text "'a bintree"}, or
   333   \texttt{\at}\verb,{typ 'a},), see also \S\ref{sec:doc-prep-text}.
   334 *}
   335 
   336 
   337 subsection {* Isabelle Sessions *}
   338 
   339 text {*
   340   In contrast to the highly interactive mode of Isabelle/Isar theory
   341   development, the document preparation stage essentially works in
   342   batch-mode.  An Isabelle \bfindex{session} consists of a collection
   343   of source files that may contribute to an output document.  Each
   344   session is derived from a single parent, usually an object-logic
   345   image like \texttt{HOL}.  This results in an overall tree structure,
   346   which is reflected by the output location in the file system
   347   (usually rooted at \verb,~/.isabelle/IsabelleXXXX/browser_info,).
   348 
   349   \medskip The easiest way to manage Isabelle sessions is via
   350   \texttt{isabelle mkdir} (generates an initial session source setup)
   351   and \texttt{isabelle make} (run sessions controlled by
   352   \texttt{IsaMakefile}).  For example, a new session
   353   \texttt{MySession} derived from \texttt{HOL} may be produced as
   354   follows:
   355 
   356 \begin{verbatim}
   357   isabelle mkdir HOL MySession
   358   isabelle make
   359 \end{verbatim}
   360 
   361   The \texttt{isabelle make} job also informs about the file-system
   362   location of the ultimate results.  The above dry run should be able
   363   to produce some \texttt{document.pdf} (with dummy title, empty table
   364   of contents etc.).  Any failure at this stage usually indicates
   365   technical problems of the {\LaTeX} installation.
   366 
   367   \medskip The detailed arrangement of the session sources is as
   368   follows.
   369 
   370   \begin{itemize}
   371 
   372   \item Directory \texttt{MySession} holds the required theory files
   373   $T@1$\texttt{.thy}, \dots, $T@n$\texttt{.thy}.
   374 
   375   \item File \texttt{MySession/ROOT.ML} holds appropriate ML commands
   376   for loading all wanted theories, usually just
   377   ``\texttt{use_thy"$T@i$";}'' for any $T@i$ in leaf position of the
   378   dependency graph.
   379 
   380   \item Directory \texttt{MySession/document} contains everything
   381   required for the {\LaTeX} stage; only \texttt{root.tex} needs to be
   382   provided initially.
   383 
   384   The latter file holds appropriate {\LaTeX} code to commence a
   385   document (\verb,\documentclass, etc.), and to include the generated
   386   files $T@i$\texttt{.tex} for each theory.  Isabelle will generate a
   387   file \texttt{session.tex} holding {\LaTeX} commands to include all
   388   generated theory output files in topologically sorted order, so
   389   \verb,\input{session}, in the body of \texttt{root.tex} does the job
   390   in most situations.
   391 
   392   \item \texttt{IsaMakefile} holds appropriate dependencies and
   393   invocations of Isabelle tools to control the batch job.  In fact,
   394   several sessions may be managed by the same \texttt{IsaMakefile}.
   395   See the \emph{Isabelle System Manual} \cite{isabelle-sys} 
   396   for further details, especially on
   397   \texttt{isabelle usedir} and \texttt{isabelle make}.
   398 
   399   \end{itemize}
   400 
   401   One may now start to populate the directory \texttt{MySession}, and
   402   the file \texttt{MySession/ROOT.ML} accordingly.  The file
   403   \texttt{MySession/document/root.tex} should also be adapted at some
   404   point; the default version is mostly self-explanatory.  Note that
   405   \verb,\isabellestyle, enables fine-tuning of the general appearance
   406   of characters and mathematical symbols (see also
   407   \S\ref{sec:doc-prep-symbols}).
   408 
   409   Especially observe the included {\LaTeX} packages \texttt{isabelle}
   410   (mandatory), \texttt{isabellesym} (required for mathematical
   411   symbols), and the final \texttt{pdfsetup} (provides sane defaults
   412   for \texttt{hyperref}, including URL markup).  All three are
   413   distributed with Isabelle. Further packages may be required in
   414   particular applications, say for unusual mathematical symbols.
   415 
   416   \medskip Any additional files for the {\LaTeX} stage go into the
   417   \texttt{MySession/document} directory as well.  In particular,
   418   adding a file named \texttt{root.bib} causes an automatic run of
   419   \texttt{bibtex} to process a bibliographic database; see also
   420   \texttt{isabelle document} \cite{isabelle-sys}.
   421 
   422   \medskip Any failure of the document preparation phase in an
   423   Isabelle batch session leaves the generated sources in their target
   424   location, identified by the accompanying error message.  This lets
   425   you trace {\LaTeX} problems with the generated files at hand.
   426 *}
   427 
   428 
   429 subsection {* Structure Markup *}
   430 
   431 text {*
   432   The large-scale structure of Isabelle documents follows existing
   433   {\LaTeX} conventions, with chapters, sections, subsubsections etc.
   434   The Isar language includes separate \bfindex{markup commands}, which
   435   do not affect the formal meaning of a theory (or proof), but result
   436   in corresponding {\LaTeX} elements.
   437 
   438   There are separate markup commands depending on the textual context:
   439   in header position (just before \isakeyword{theory}), within the
   440   theory body, or within a proof.  The header needs to be treated
   441   specially here, since ordinary theory and proof commands may only
   442   occur \emph{after} the initial \isakeyword{theory} specification.
   443 
   444   \medskip
   445 
   446   \begin{tabular}{llll}
   447   header & theory & proof & default meaning \\\hline
   448     & \commdx{chapter} & & \verb,\chapter, \\
   449   \commdx{header} & \commdx{section} & \commdx{sect} & \verb,\section, \\
   450     & \commdx{subsection} & \commdx{subsect} & \verb,\subsection, \\
   451     & \commdx{subsubsection} & \commdx{subsubsect} & \verb,\subsubsection, \\
   452   \end{tabular}
   453 
   454   \medskip
   455 
   456   From the Isabelle perspective, each markup command takes a single
   457   $text$ argument (delimited by \verb,",~@{text \<dots>}~\verb,", or
   458   \verb,{,\verb,*,~@{text \<dots>}~\verb,*,\verb,},).  After stripping any
   459   surrounding white space, the argument is passed to a {\LaTeX} macro
   460   \verb,\isamarkupXYZ, for command \isakeyword{XYZ}.  These macros are
   461   defined in \verb,isabelle.sty, according to the meaning given in the
   462   rightmost column above.
   463 
   464   \medskip The following source fragment illustrates structure markup
   465   of a theory.  Note that {\LaTeX} labels may be included inside of
   466   section headings as well.
   467 
   468   \begin{ttbox}
   469   header {\ttlbrace}* Some properties of Foo Bar elements *{\ttrbrace}
   470 
   471   theory Foo_Bar
   472   imports Main
   473   begin
   474 
   475   subsection {\ttlbrace}* Basic definitions *{\ttrbrace}
   476 
   477   definition foo :: \dots
   478 
   479   definition bar :: \dots
   480 
   481   subsection {\ttlbrace}* Derived rules *{\ttrbrace}
   482 
   483   lemma fooI: \dots
   484   lemma fooE: \dots
   485 
   486   subsection {\ttlbrace}* Main theorem {\ttback}label{\ttlbrace}sec:main-theorem{\ttrbrace} *{\ttrbrace}
   487 
   488   theorem main: \dots
   489 
   490   end
   491   \end{ttbox}\vspace{-\medskipamount}
   492 
   493   You may occasionally want to change the meaning of markup commands,
   494   say via \verb,\renewcommand, in \texttt{root.tex}.  For example,
   495   \verb,\isamarkupheader, is a good candidate for some tuning.  We
   496   could move it up in the hierarchy to become \verb,\chapter,.
   497 
   498 \begin{verbatim}
   499   \renewcommand{\isamarkupheader}[1]{\chapter{#1}}
   500 \end{verbatim}
   501 
   502   \noindent Now we must change the document class given in
   503   \texttt{root.tex} to something that supports chapters.  A suitable
   504   command is \verb,\documentclass{report},.
   505 
   506   \medskip The {\LaTeX} macro \verb,\isabellecontext, is maintained to
   507   hold the name of the current theory context.  This is particularly
   508   useful for document headings:
   509 
   510 \begin{verbatim}
   511   \renewcommand{\isamarkupheader}[1]
   512   {\chapter{#1}\markright{THEORY~\isabellecontext}}
   513 \end{verbatim}
   514 
   515   \noindent Make sure to include something like
   516   \verb,\pagestyle{headings}, in \texttt{root.tex}; the document
   517   should have more than two pages to show the effect.
   518 *}
   519 
   520 
   521 subsection {* Formal Comments and Antiquotations \label{sec:doc-prep-text} *}
   522 
   523 text {*
   524   Isabelle \bfindex{source comments}, which are of the form
   525   \verb,(,\verb,*,~@{text \<dots>}~\verb,*,\verb,),, essentially act like
   526   white space and do not really contribute to the content.  They
   527   mainly serve technical purposes to mark certain oddities in the raw
   528   input text.  In contrast, \bfindex{formal comments} are portions of
   529   text that are associated with formal Isabelle/Isar commands
   530   (\bfindex{marginal comments}), or as standalone paragraphs within a
   531   theory or proof context (\bfindex{text blocks}).
   532 
   533   \medskip Marginal comments are part of each command's concrete
   534   syntax \cite{isabelle-ref}; the common form is ``\verb,--,~$text$''
   535   where $text$ is delimited by \verb,",@{text \<dots>}\verb,", or
   536   \verb,{,\verb,*,~@{text \<dots>}~\verb,*,\verb,}, as before.  Multiple
   537   marginal comments may be given at the same time.  Here is a simple
   538   example:
   539 *}
   540 
   541 lemma "A --> A"
   542   -- "a triviality of propositional logic"
   543   -- "(should not really bother)"
   544   by (rule impI) -- "implicit assumption step involved here"
   545 
   546 text {*
   547   \noindent The above output has been produced as follows:
   548 
   549 \begin{verbatim}
   550   lemma "A --> A"
   551     -- "a triviality of propositional logic"
   552     -- "(should not really bother)"
   553     by (rule impI) -- "implicit assumption step involved here"
   554 \end{verbatim}
   555 
   556   From the {\LaTeX} viewpoint, ``\verb,--,'' acts like a markup
   557   command, associated with the macro \verb,\isamarkupcmt, (taking a
   558   single argument).
   559 
   560   \medskip Text blocks are introduced by the commands \bfindex{text}
   561   and \bfindex{txt}, for theory and proof contexts, respectively.
   562   Each takes again a single $text$ argument, which is interpreted as a
   563   free-form paragraph in {\LaTeX} (surrounded by some additional
   564   vertical space).  This behavior may be changed by redefining the
   565   {\LaTeX} environments of \verb,isamarkuptext, or
   566   \verb,isamarkuptxt,, respectively (via \verb,\renewenvironment,) The
   567   text style of the body is determined by \verb,\isastyletext, and
   568   \verb,\isastyletxt,; the default setup uses a smaller font within
   569   proofs.  This may be changed as follows:
   570 
   571 \begin{verbatim}
   572   \renewcommand{\isastyletxt}{\isastyletext}
   573 \end{verbatim}
   574 
   575   \medskip The $text$ part of Isabelle markup commands essentially
   576   inserts \emph{quoted material} into a formal text, mainly for
   577   instruction of the reader.  An \bfindex{antiquotation} is again a
   578   formal object embedded into such an informal portion.  The
   579   interpretation of antiquotations is limited to some well-formedness
   580   checks, with the result being pretty printed to the resulting
   581   document.  Quoted text blocks together with antiquotations provide
   582   an attractive means of referring to formal entities, with good
   583   confidence in getting the technical details right (especially syntax
   584   and types).
   585 
   586   The general syntax of antiquotations is as follows:
   587   \texttt{{\at}{\ttlbrace}$name$ $arguments${\ttrbrace}}, or
   588   \texttt{{\at}{\ttlbrace}$name$ [$options$] $arguments${\ttrbrace}}
   589   for a comma-separated list of options consisting of a $name$ or
   590   \texttt{$name$=$value$} each.  The syntax of $arguments$ depends on
   591   the kind of antiquotation, it generally follows the same conventions
   592   for types, terms, or theorems as in the formal part of a theory.
   593 
   594   \medskip This sentence demonstrates quotations and antiquotations:
   595   @{term "%x y. x"} is a well-typed term.
   596 
   597   \medskip\noindent The output above was produced as follows:
   598   \begin{ttbox}
   599 text {\ttlbrace}*
   600   This sentence demonstrates quotations and antiquotations:
   601   {\at}{\ttlbrace}term "%x y. x"{\ttrbrace} is a well-typed term.
   602 *{\ttrbrace}
   603   \end{ttbox}\vspace{-\medskipamount}
   604 
   605   The notational change from the ASCII character~\verb,%, to the
   606   symbol~@{text \<lambda>} reveals that Isabelle printed this term, after
   607   parsing and type-checking.  Document preparation enables symbolic
   608   output by default.
   609 
   610   \medskip The next example includes an option to show the type of all
   611   variables.  The antiquotation
   612   \texttt{{\at}}\verb,{term [show_types] "%x y. x"}, produces the
   613   output @{term [show_types] "%x y. x"}.  Type inference has figured
   614   out the most general typings in the present theory context.  Terms
   615   may acquire different typings due to constraints imposed by their
   616   environment; within a proof, for example, variables are given the
   617   same types as they have in the main goal statement.
   618 
   619   \medskip Several further kinds of antiquotations and options are
   620   available \cite{isabelle-isar-ref}.  Here are a few commonly used
   621   combinations:
   622 
   623   \medskip
   624 
   625   \begin{tabular}{ll}
   626   \texttt{\at}\verb,{typ,~$\tau$\verb,}, & print type $\tau$ \\
   627   \texttt{\at}\verb,{const,~$c$\verb,}, & check existence of $c$ and print it \\
   628   \texttt{\at}\verb,{term,~$t$\verb,}, & print term $t$ \\
   629   \texttt{\at}\verb,{prop,~$\phi$\verb,}, & print proposition $\phi$ \\
   630   \texttt{\at}\verb,{prop [display],~$\phi$\verb,}, & print large proposition $\phi$ (with linebreaks) \\
   631   \texttt{\at}\verb,{prop [source],~$\phi$\verb,}, & check proposition $\phi$, print its input \\
   632   \texttt{\at}\verb,{thm,~$a$\verb,}, & print fact $a$ \\
   633   \texttt{\at}\verb,{thm,~$a$~\verb,[no_vars]}, & print fact $a$, fixing schematic variables \\
   634   \texttt{\at}\verb,{thm [source],~$a$\verb,}, & check availability of fact $a$, print its name \\
   635   \texttt{\at}\verb,{text,~$s$\verb,}, & print uninterpreted text $s$ \\
   636   \end{tabular}
   637 
   638   \medskip
   639 
   640   Note that \attrdx{no_vars} given above is \emph{not} an
   641   antiquotation option, but an attribute of the theorem argument given
   642   here.  This might be useful with a diagnostic command like
   643   \isakeyword{thm}, too.
   644 
   645   \medskip The \texttt{\at}\verb,{text, $s$\verb,}, antiquotation is
   646   particularly interesting.  Embedding uninterpreted text within an
   647   informal body might appear useless at first sight.  Here the key
   648   virtue is that the string $s$ is processed as Isabelle output,
   649   interpreting Isabelle symbols appropriately.
   650 
   651   For example, \texttt{\at}\verb,{text "\<forall>\<exists>"}, produces @{text
   652   "\<forall>\<exists>"}, according to the standard interpretation of these symbol
   653   (cf.\ \S\ref{sec:doc-prep-symbols}).  Thus we achieve consistent
   654   mathematical notation in both the formal and informal parts of the
   655   document very easily, independently of the term language of
   656   Isabelle.  Manual {\LaTeX} code would leave more control over the
   657   typesetting, but is also slightly more tedious.
   658 *}
   659 
   660 
   661 subsection {* Interpretation of Symbols \label{sec:doc-prep-symbols} *}
   662 
   663 text {*
   664   As has been pointed out before (\S\ref{sec:syntax-symbols}),
   665   Isabelle symbols are the smallest syntactic entities --- a
   666   straightforward generalization of ASCII characters.  While Isabelle
   667   does not impose any interpretation of the infinite collection of
   668   named symbols, {\LaTeX} documents use canonical glyphs for certain
   669   standard symbols \cite{isabelle-isar-ref}.
   670 
   671   The {\LaTeX} code produced from Isabelle text follows a simple
   672   scheme.  You can tune the final appearance by redefining certain
   673   macros, say in \texttt{root.tex} of the document.
   674 
   675   \begin{enumerate}
   676 
   677   \item 7-bit ASCII characters: letters \texttt{A\dots Z} and
   678   \texttt{a\dots z} are output directly, digits are passed as an
   679   argument to the \verb,\isadigit, macro, other characters are
   680   replaced by specifically named macros of the form
   681   \verb,\isacharXYZ,.
   682 
   683   \item Named symbols: \verb,\,\verb,<XYZ>, is turned into
   684   \verb,{\isasymXYZ},; note the additional braces.
   685 
   686   \item Named control symbols: \verb,\,\verb,<^XYZ>, is turned into
   687   \verb,\isactrlXYZ,; subsequent symbols may act as arguments if the
   688   control macro is defined accordingly.
   689 
   690   \end{enumerate}
   691 
   692   You may occasionally wish to give new {\LaTeX} interpretations of
   693   named symbols.  This merely requires an appropriate definition of
   694   \verb,\isasymXYZ,, for \verb,\,\verb,<XYZ>, (see
   695   \texttt{isabelle.sty} for working examples).  Control symbols are
   696   slightly more difficult to get right, though.
   697 
   698   \medskip The \verb,\isabellestyle, macro provides a high-level
   699   interface to tune the general appearance of individual symbols.  For
   700   example, \verb,\isabellestyle{it}, uses the italics text style to
   701   mimic the general appearance of the {\LaTeX} math mode; double
   702   quotes are not printed at all.  The resulting quality of typesetting
   703   is quite good, so this should be the default style for work that
   704   gets distributed to a broader audience.
   705 *}
   706 
   707 
   708 subsection {* Suppressing Output \label{sec:doc-prep-suppress} *}
   709 
   710 text {*
   711   By default, Isabelle's document system generates a {\LaTeX} file for
   712   each theory that gets loaded while running the session.  The
   713   generated \texttt{session.tex} will include all of these in order of
   714   appearance, which in turn gets included by the standard
   715   \texttt{root.tex}.  Certainly one may change the order or suppress
   716   unwanted theories by ignoring \texttt{session.tex} and load
   717   individual files directly in \texttt{root.tex}.  On the other hand,
   718   such an arrangement requires additional maintenance whenever the
   719   collection of theories changes.
   720 
   721   Alternatively, one may tune the theory loading process in
   722   \texttt{ROOT.ML} itself: traversal of the theory dependency graph
   723   may be fine-tuned by adding \verb,use_thy, invocations, although
   724   topological sorting still has to be observed.  Moreover, the ML
   725   operator \verb,no_document, temporarily disables document generation
   726   while executing a theory loader command.  Its usage is like this:
   727 
   728 \begin{verbatim}
   729   no_document use_thy "T";
   730 \end{verbatim}
   731 
   732   \medskip Theory output may be suppressed more selectively, either
   733   via \bfindex{tagged command regions} or \bfindex{ignored material}.
   734 
   735   Tagged command regions works by annotating commands with named tags,
   736   which correspond to certain {\LaTeX} markup that tells how to treat
   737   particular parts of a document when doing the actual type-setting.
   738   By default, certain Isabelle/Isar commands are implicitly marked up
   739   using the predefined tags ``\emph{theory}'' (for theory begin and
   740   end), ``\emph{proof}'' (for proof commands), and ``\emph{ML}'' (for
   741   commands involving ML code).  Users may add their own tags using the
   742   \verb,%,\emph{tag} notation right after a command name.  In the
   743   subsequent example we hide a particularly irrelevant proof:
   744 *}
   745 
   746 lemma "x = x" by %invisible (simp)
   747 
   748 text {*
   749   The original source has been ``\verb,lemma "x = x" by %invisible (simp),''.
   750   Tags observe the structure of proofs; adjacent commands with the
   751   same tag are joined into a single region.  The Isabelle document
   752   preparation system allows the user to specify how to interpret a
   753   tagged region, in order to keep, drop, or fold the corresponding
   754   parts of the document.  See the \emph{Isabelle System Manual}
   755   \cite{isabelle-sys} for further details, especially on
   756   \texttt{isabelle usedir} and \texttt{isabelle document}.
   757 
   758   Ignored material is specified by delimiting the original formal
   759   source with special source comments
   760   \verb,(,\verb,*,\verb,<,\verb,*,\verb,), and
   761   \verb,(,\verb,*,\verb,>,\verb,*,\verb,),.  These parts are stripped
   762   before the type-setting phase, without affecting the formal checking
   763   of the theory, of course.  For example, we may hide parts of a proof
   764   that seem unfit for general public inspection.  The following
   765   ``fully automatic'' proof is actually a fake:
   766 *}
   767 
   768 lemma "x \<noteq> (0::int) \<Longrightarrow> 0 < x * x"
   769   by (auto(*<*)simp add: zero_less_mult_iff(*>*))
   770 
   771 text {*
   772   \noindent The real source of the proof has been as follows:
   773 
   774 \begin{verbatim}
   775   by (auto(*<*)simp add: zero_less_mult_iff(*>*))
   776 \end{verbatim}
   777 %(*
   778 
   779   \medskip Suppressing portions of printed text demands care.  You
   780   should not misrepresent the underlying theory development.  It is
   781   easy to invalidate the visible text by hiding references to
   782   questionable axioms, for example.
   783 *}
   784 
   785 (*<*)
   786 end
   787 (*>*)