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--
     1 (*<*)
     2 theory Documents imports Main begin
     3 (*>*)
     5 section {* Concrete Syntax \label{sec:concrete-syntax} *}
     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.
    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.
    20   Below we introduce a few simple syntax declaration
    21   forms that already cover many common situations fairly well.
    22 *}
    25 subsection {* Infix Annotations *}
    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).
    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 *}
    40 definition xor :: "bool \<Rightarrow> bool \<Rightarrow> bool"    (infixl "[+]" 60)
    41 where "A [+] B \<equiv> (A \<and> \<not> B) \<or> (\<not> A \<and> B)"
    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"}.
    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.
    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 "[+]"}.
    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 *}
    81 subsection {* Mathematical Symbols \label{sec:syntax-symbols} *}
    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'':
    92   \begin{enumerate}
    94   \item 7-bit ASCII characters
    96   \item named symbols: \verb,\,\verb,<,$ident$\verb,>,
    98   \item named control symbols: \verb,\,\verb,<^,$ident$\verb,>,
   100   \end{enumerate}
   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>}.
   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>"}.
   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
   128   \medskip
   129   {\small\noindent \verb,\,\verb,<forall>\,\verb,<alpha>\<^isub>1.,~\verb,\,\verb,<alpha>\<^isub>1 = \,\verb,<Pi>\<^isup>\<A>,}
   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.
   136   Replacing our previous definition of @{text xor} by the
   137   following specifies an Isabelle symbol for the new operator:
   138 *}
   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 (*>*)
   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.
   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 *}
   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)"
   170 notation (xsymbols) xor (infixl "\<oplus>\<ignore>" 60)
   171 (*<*)
   172 setup {* Sign.local_path *}
   173 (*>*)
   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.
   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.  *}
   187 subsection {* Prefix Annotations *}
   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 *}
   196 datatype currency =
   197     Euro nat    ("\<euro>")
   198   | Pounds nat  ("\<pounds>")
   199   | Yen nat     ("\<yen>")
   200   | Dollar nat  ("$")
   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.
   213   Prefix syntax works the same way for other commands that introduce new constants, e.g. \isakeyword{primrec}.
   214 *}
   217 subsection {* Abbreviations \label{sec:abbreviations} *}
   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}.
   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.
   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"
   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.
   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 *}
   250 abbreviation not_equal :: "'a \<Rightarrow> 'a \<Rightarrow> bool"    (infixl "~=\<ignore>" 50)
   251 where "x ~=\<ignore> y  \<equiv>  \<not> (x = y)"
   253 notation (xsymbols) not_equal (infix "\<noteq>\<ignore>" 50)
   255 text {* \noindent The notation @{text \<noteq>} is introduced separately to restrict it
   256 to the \emph{xsymbols} mode.
   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.
   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 *}
   270 section {* Document Preparation \label{sec:document-preparation} *}
   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.
   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.
   287   Here is an example to illustrate the idea of Isabelle document
   288   preparation.
   289 *}
   291 text_raw {* \begin{quotation} *}
   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 *}
   299 datatype 'a bintree =
   300      Leaf | Branch 'a  "'a bintree"  "'a bintree"
   302 text {*
   303   \noindent The datatype induction rule generated here is of the form
   304   @{thm [indent = 1, display] bintree.induct [no_vars]}
   305 *}
   307 text_raw {* \end{quotation} *}
   309 text {*
   310   \noindent The above document output has been produced as follows:
   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}
   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}
   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 *}
   337 subsection {* Isabelle Sessions *}
   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,).
   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:
   356 \begin{verbatim}
   357   isabelle mkdir HOL MySession
   358   isabelle make
   359 \end{verbatim}
   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.
   367   \medskip The detailed arrangement of the session sources is as
   368   follows.
   370   \begin{itemize}
   372   \item Directory \texttt{MySession} holds the required theory files
   373   $T@1$\texttt{.thy}, \dots, $T@n$\texttt{.thy}.
   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.
   380   \item Directory \texttt{MySession/document} contains everything
   381   required for the {\LaTeX} stage; only \texttt{root.tex} needs to be
   382   provided initially.
   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.
   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}.
   399   \end{itemize}
   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}).
   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.
   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}.
   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 *}
   429 subsection {* Structure Markup *}
   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.
   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.
   444   \medskip
   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}
   454   \medskip
   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.
   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.
   468   \begin{ttbox}
   469   header {\ttlbrace}* Some properties of Foo Bar elements *{\ttrbrace}
   471   theory Foo_Bar
   472   imports Main
   473   begin
   475   subsection {\ttlbrace}* Basic definitions *{\ttrbrace}
   477   definition foo :: \dots
   479   definition bar :: \dots
   481   subsection {\ttlbrace}* Derived rules *{\ttrbrace}
   483   lemma fooI: \dots
   484   lemma fooE: \dots
   486   subsection {\ttlbrace}* Main theorem {\ttback}label{\ttlbrace}sec:main-theorem{\ttrbrace} *{\ttrbrace}
   488   theorem main: \dots
   490   end
   491   \end{ttbox}\vspace{-\medskipamount}
   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,.
   498 \begin{verbatim}
   499   \renewcommand{\isamarkupheader}[1]{\chapter{#1}}
   500 \end{verbatim}
   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},.
   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:
   510 \begin{verbatim}
   511   \renewcommand{\isamarkupheader}[1]
   512   {\chapter{#1}\markright{THEORY~\isabellecontext}}
   513 \end{verbatim}
   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 *}
   521 subsection {* Formal Comments and Antiquotations \label{sec:doc-prep-text} *}
   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}).
   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 *}
   541 lemma "A --> A"
   542   -- "a triviality of propositional logic"
   543   -- "(should not really bother)"
   544   by (rule impI) -- "implicit assumption step involved here"
   546 text {*
   547   \noindent The above output has been produced as follows:
   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}
   556   From the {\LaTeX} viewpoint, ``\verb,--,'' acts like a markup
   557   command, associated with the macro \verb,\isamarkupcmt, (taking a
   558   single argument).
   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:
   571 \begin{verbatim}
   572   \renewcommand{\isastyletxt}{\isastyletext}
   573 \end{verbatim}
   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).
   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.
   594   \medskip This sentence demonstrates quotations and antiquotations:
   595   @{term "%x y. x"} is a well-typed term.
   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}
   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.
   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.
   619   \medskip Several further kinds of antiquotations and options are
   620   available \cite{isabelle-isar-ref}.  Here are a few commonly used
   621   combinations:
   623   \medskip
   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}
   638   \medskip
   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.
   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.
   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 *}
   661 subsection {* Interpretation of Symbols \label{sec:doc-prep-symbols} *}
   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}.
   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.
   675   \begin{enumerate}
   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,.
   683   \item Named symbols: \verb,\,\verb,<XYZ>, is turned into
   684   \verb,{\isasymXYZ},; note the additional braces.
   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.
   690   \end{enumerate}
   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.
   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 *}
   708 subsection {* Suppressing Output \label{sec:doc-prep-suppress} *}
   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.
   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:
   728 \begin{verbatim}
   729   no_document use_thy "T";
   730 \end{verbatim}
   732   \medskip Theory output may be suppressed more selectively, either
   733   via \bfindex{tagged command regions} or \bfindex{ignored material}.
   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 *}
   746 lemma "x = x" by %invisible (simp)
   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}.
   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 *}
   768 lemma "x \<noteq> (0::int) \<Longrightarrow> 0 < x * x"
   769   by (auto(*<*)simp add: zero_less_mult_iff(*>*))
   771 text {*
   772   \noindent The real source of the proof has been as follows:
   774 \begin{verbatim}
   775   by (auto(*<*)simp add: zero_less_mult_iff(*>*))
   776 \end{verbatim}
   777 %(*
   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 *}
   785 (*<*)
   786 end
   787 (*>*)