(*<*)

 theory Documents imports Main begin

 (*>*)

 section {* Concrete Syntax \label{sec:concrete-syntax} *}

 text {*

   The core concept of Isabelle's framework for concrete syntax is that

   of \bfindex{mixfix annotations}.  Associated with any kind of

   constant declaration, mixfixes affect both the grammar productions

   for the parser and output templates for the pretty printer.

   In full generality, parser and pretty printer configuration is a

   subtle affair~\cite{isabelle-ref}.  Your syntax specifications need

   to interact properly with the existing setup of Isabelle/Pure and

   Isabelle/HOL\@.  To avoid creating ambiguities with existing

   elements, it is particularly important to give new syntactic

   constructs the right precedence.

   Below we introduce a few simple syntax declaration

   forms that already cover many common situations fairly well.

 *}

 subsection {* Infix Annotations *}

 text {*

   Syntax annotations may be included wherever constants are declared,

   such as \isacommand{definition} and \isacommand{primrec} --- and also

   \isacommand{datatype}, which declares constructor operations.

   Type-constructors may be annotated as well, although this is less

   frequently encountered in practice (the infix type @{text "\<times>"} comes

   to mind).

   Infix declarations\index{infix annotations} provide a useful special

   case of mixfixes.  The following example of the exclusive-or

   operation on boolean values illustrates typical infix declarations.

 *}

 definition xor :: "bool \<Rightarrow> bool \<Rightarrow> bool"    (infixl "[+]" 60)

 where "A [+] B \<equiv> (A \<and> \<not> B) \<or> (\<not> A \<and> B)"

 text {*

   \noindent Now @{text "xor A B"} and @{text "A [+] B"} refer to the

   same expression internally.  Any curried function with at least two

   arguments may be given infix syntax.  For partial applications with

   fewer than two operands, there is a notation using the prefix~@{text

   op}.  For instance, @{text xor} without arguments is represented as

   @{text "op [+]"}; together with ordinary function application, this

   turns @{text "xor A"} into @{text "op [+] A"}.

   The keyword \isakeyword{infixl} seen above specifies an

   infix operator that is nested to the \emph{left}: in iterated

   applications the more complex expression appears on the left-hand

   side, and @{term "A [+] B [+] C"} stands for @{text "(A [+] B) [+]

   C"}.  Similarly, \isakeyword{infixr} means nesting to the

   \emph{right}, reading @{term "A [+] B [+] C"} as @{text "A [+] (B

   [+] C)"}.  A \emph{non-oriented} declaration via \isakeyword{infix}

   would render @{term "A [+] B [+] C"} illegal, but demand explicit

   parentheses to indicate the intended grouping.

   The string @{text [source] "[+]"} in our annotation refers to the

   concrete syntax to represent the operator (a literal token), while

   the number @{text 60} determines the precedence of the construct:

   the syntactic priorities of the arguments and result.  Isabelle/HOL

   already uses up many popular combinations of ASCII symbols for its

   own use, including both @{text "+"} and @{text "++"}.  Longer

   character combinations are more likely to be still available for

   user extensions, such as our~@{text "[+]"}.

   Operator precedences have a range of 0--1000.  Very low or high

   priorities are reserved for the meta-logic.  HOL syntax mainly uses

   the range of 10--100: the equality infix @{text "="} is centered at

   50; logical connectives (like @{text "\<or>"} and @{text "\<and>"}) are

   below 50; algebraic ones (like @{text "+"} and @{text "*"}) are

   above 50.  User syntax should strive to coexist with common HOL

   forms, or use the mostly unused range 100--900.

 *}

 subsection {* Mathematical Symbols \label{sec:syntax-symbols} *}

 text {*

   Concrete syntax based on ASCII characters has inherent limitations.

   Mathematical notation demands a larger repertoire of glyphs.

   Several standards of extended character sets have been proposed over

   decades, but none has become universally available so far.  Isabelle

   has its own notion of \bfindex{symbols} as the smallest entities of

   source text, without referring to internal encodings.  There are

   three kinds of such ``generalized characters'':

   \begin{enumerate}

   \item 7-bit ASCII characters

   \item named symbols: \verb,\,\verb,<,$ident$\verb,>,

   \item named control symbols: \verb,\,\verb,<^,$ident$\verb,>,

   \end{enumerate}

   Here $ident$ is any sequence of letters. 

   This results in an infinite store of symbols, whose

   interpretation is left to further front-end tools.  For example, the

   user-interface of Proof~General + X-Symbol and the Isabelle document

   processor (see \S\ref{sec:document-preparation}) display the

   \verb,\,\verb,<forall>, symbol as~@{text \<forall>}.

   A list of standard Isabelle symbols is given in

   \cite{isabelle-isar-ref}.  You may introduce your own

   interpretation of further symbols by configuring the appropriate

   front-end tool accordingly, e.g.\ by defining certain {\LaTeX}

   macros (see also \S\ref{sec:doc-prep-symbols}).  There are also a

   few predefined control symbols, such as \verb,\,\verb,<^sub>, and

   \verb,\,\verb,<^sup>, for sub- and superscript of the subsequent

   printable symbol, respectively.  For example, \verb,A\<^sup>\<star>, is

   output as @{text "A\<^sup>\<star>"}.

   A number of symbols are considered letters by the Isabelle lexer and

   can be used as part of identifiers. These are the greek letters

   @{text "\<alpha>"} (\verb+\+\verb+<alpha>+), @{text "\<beta>"}

   (\verb+\+\verb+<beta>+), etc. (excluding @{text "\<lambda>"}),

   special letters like @{text "\<A>"} (\verb+\+\verb+<A>+) and @{text

   "\<AA>"} (\verb+\+\verb+<AA>+), and the control symbols

   \verb+\+\verb+<^isub>+ and \verb+\+\verb+<^isup>+ for single letter

   sub and super scripts. This means that the input

   \medskip

   {\small\noindent \verb,\,\verb,<forall>\,\verb,<alpha>\<^isub>1.,~\verb,\,\verb,<alpha>\<^isub>1 = \,\verb,<Pi>\<^isup>\<A>,}

   \medskip

   \noindent is recognized as the term @{term "\<forall>\<alpha>\<^isub>1. \<alpha>\<^isub>1 = \<Pi>\<^isup>\<A>"} 

   by Isabelle. Note that @{text "\<Pi>\<^isup>\<A>"} is a single

   syntactic entity, not an exponentiation.

   Replacing our previous definition of @{text xor} by the

   following specifies an Isabelle symbol for the new operator:

 *}

 (*<*)

 hide const xor

 setup {* Sign.add_path "version1" *}

 (*>*)

 definition xor :: "bool \<Rightarrow> bool \<Rightarrow> bool"    (infixl "\<oplus>" 60)

 where "A \<oplus> B \<equiv> (A \<and> \<not> B) \<or> (\<not> A \<and> B)"

 (*<*)

 local

 (*>*)

 text {*

   \noindent The X-Symbol package within Proof~General provides several

   input methods to enter @{text \<oplus>} in the text.  If all fails one may

   just type a named entity \verb,\,\verb,<oplus>, by hand; the

   corresponding symbol will be displayed after further input.

   More flexible is to provide alternative syntax forms

   through the \bfindex{print mode} concept~\cite{isabelle-ref}.  By

   convention, the mode of ``$xsymbols$'' is enabled whenever

   Proof~General's X-Symbol mode or {\LaTeX} output is active.  Now

   consider the following hybrid declaration of @{text xor}:

 *}

 (*<*)

 hide const xor

 setup {* Sign.add_path "version2" *}

 (*>*)

 definition xor :: "bool \<Rightarrow> bool \<Rightarrow> bool"    (infixl "[+]\<ignore>" 60)

 where "A [+]\<ignore> B \<equiv> (A \<and> \<not> B) \<or> (\<not> A \<and> B)"

 notation (xsymbols) xor (infixl "\<oplus>\<ignore>" 60)

 (*<*)

 local

 (*>*)

 text {*\noindent

 The \commdx{notation} command associates a mixfix

 annotation with a known constant.  The print mode specification,

 here @{text "(xsymbols)"}, is optional.

 We may now write @{text "A [+] B"} or @{text "A \<oplus> B"} in input, while

 output uses the nicer syntax of $xsymbols$ whenever that print mode is

 active.  Such an arrangement is particularly useful for interactive

 development, where users may type ASCII text and see mathematical

 symbols displayed during proofs.  *}

 subsection {* Prefix Annotations *}

 text {*

   Prefix syntax annotations\index{prefix annotation} are another form

   of mixfixes \cite{isabelle-ref}, without any template arguments or

   priorities --- just some literal syntax.  The following example

   associates common symbols with the constructors of a datatype.

 *}

 datatype currency =

     Euro nat    ("\<euro>")

   | Pounds nat  ("\<pounds>")

   | Yen nat     ("\<yen>")

   | Dollar nat  ("$")

 text {*

   \noindent Here the 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,$,.  Recall

   that a constructor like @{text Euro} actually is a function @{typ

   "nat \<Rightarrow> currency"}.  The expression @{text "Euro 10"} will be

   printed as @{term "\<euro> 10"}; only the head of the application is

   subject to our concrete syntax.  This rather simple form already

   achieves conformance with notational standards of the European

   Commission.

   Prefix syntax works the same way for other commands that introduce new constants, e.g. \isakeyword{primrec}.

 *}

 subsection {* Abbreviations \label{sec:abbreviations} *}

 text{* Mixfix syntax annotations merely decorate particular constant

 application forms with concrete syntax, for instance replacing

 @{text "xor A B"} by @{text "A \<oplus> B"}.  Occasionally, the relationship

 between some piece of notation and its internal form is more

 complicated.  Here we need \emph{abbreviations}.

 Command \commdx{abbreviation} introduces an uninterpreted notational

 constant as an abbreviation for a complex term. Abbreviations are

 unfolded upon parsing and re-introduced upon printing. This provides a

 simple mechanism for syntactic macros.

 A typical use of abbreviations is to introduce relational notation for

 membership in a set of pairs, replacing @{text "(x, y) \<in> sim"} by

 @{text "x \<approx> y"}. We assume that a constant @{text sim } of type

 @{typ"('a \<times> 'a) set"} has been introduced at this point. *}

 (*<*)consts sim :: "('a \<times> 'a) set"(*>*)

 abbreviation sim2 :: "'a \<Rightarrow> 'a \<Rightarrow> bool"   (infix "\<approx>" 50)

 where "x \<approx> y  \<equiv>  (x, y) \<in> sim"

 text {* \noindent The given meta-equality is used as a rewrite rule

 after parsing (replacing \mbox{@{prop"x \<approx> y"}} by @{text"(x,y) \<in>

 sim"}) and before printing (turning @{text"(x,y) \<in> sim"} back into

 \mbox{@{prop"x \<approx> y"}}). The name of the dummy constant @{text "sim2"}

 does not matter, as long as it is unique.

 Another common application of abbreviations is to

 provide variant versions of fundamental relational expressions, such

 as @{text \<noteq>} for negated equalities.  The following declaration

 stems from Isabelle/HOL itself:

 *}

 abbreviation not_equal :: "'a \<Rightarrow> 'a \<Rightarrow> bool"    (infixl "~=\<ignore>" 50)

 where "x ~=\<ignore> y  \<equiv>  \<not> (x = y)"

 notation (xsymbols) not_equal (infix "\<noteq>\<ignore>" 50)

 text {* \noindent The notation @{text \<noteq>} is introduced separately to restrict it

 to the \emph{xsymbols} mode.

 Abbreviations are appropriate when the defined concept is a

 simple variation on an existing one.  But because of the automatic

 folding and unfolding of abbreviations, they do not scale up well to

 large hierarchies of concepts. Abbreviations do not replace

 definitions.

 Abbreviations are a simplified form of the general concept of

 \emph{syntax translations}; even heavier transformations may be

 written in ML \cite{isabelle-ref}.

 *}

 section {* Document Preparation \label{sec:document-preparation} *}

 text {*

   Isabelle/Isar is centered around the concept of \bfindex{formal

   proof documents}\index{documents|bold}.  The outcome of a formal

   development effort is meant to be a human-readable record, presented

   as browsable PDF file or printed on paper.  The overall document

   structure follows traditional mathematical articles, with sections,

   intermediate explanations, definitions, theorems and proofs.

   \medskip The Isabelle document preparation system essentially acts

   as a front-end to {\LaTeX}.  After checking specifications and

   proofs formally, the theory sources are turned into typesetting

   instructions in a schematic manner.  This lets you write authentic

   reports on theory developments with little effort: many technical

   consistency checks are handled by the system.

   Here is an example to illustrate the idea of Isabelle document

   preparation.

 *}

 text_raw {* \begin{quotation} *}

 text {*

   The following datatype definition of @{text "'a bintree"} models

   binary trees with nodes being decorated by elements of type @{typ

   'a}.

 *}

 datatype 'a bintree =

      Leaf | Branch 'a  "'a bintree"  "'a bintree"

 text {*

   \noindent The datatype induction rule generated here is of the form

   @{thm [indent = 1, display] bintree.induct [no_vars]}

 *}

 text_raw {* \end{quotation} *}

 text {*

   \noindent The above document output has been produced as follows:

   \begin{ttbox}

   text {\ttlbrace}*

     The following datatype definition of {\at}{\ttlbrace}text "'a bintree"{\ttrbrace}

     models binary trees with nodes being decorated by elements

     of type {\at}{\ttlbrace}typ 'a{\ttrbrace}.

   *{\ttrbrace}

   datatype 'a bintree =

     Leaf | Branch 'a  "'a bintree"  "'a bintree"

   \end{ttbox}

   \begin{ttbox}

   text {\ttlbrace}*

     {\ttback}noindent The datatype induction rule generated here is

     of the form {\at}{\ttlbrace}thm [display] bintree.induct [no_vars]{\ttrbrace}

   *{\ttrbrace}

   \end{ttbox}\vspace{-\medskipamount}

   \noindent Here we have augmented the theory by formal comments

   (using \isakeyword{text} blocks), the informal parts may again refer

   to formal entities by means of ``antiquotations'' (such as

   \texttt{\at}\verb,{text "'a bintree"}, or

   \texttt{\at}\verb,{typ 'a},), see also \S\ref{sec:doc-prep-text}.

 *}

 subsection {* Isabelle Sessions *}

 text {*

   In contrast to the highly interactive mode of Isabelle/Isar theory

   development, the document preparation stage essentially works in

   batch-mode.  An Isabelle \bfindex{session} consists of a collection

   of source files that may contribute to an output document.  Each

   session is derived from a single parent, usually an object-logic

   image like \texttt{HOL}.  This results in an overall tree structure,

   which is reflected by the output location in the file system

   (usually rooted at \verb,~/.isabelle/browser_info,).

   \medskip The easiest way to manage Isabelle sessions is via

   \texttt{isabelle mkdir} (generates an initial session source setup)

   and \texttt{isabelle make} (run sessions controlled by

   \texttt{IsaMakefile}).  For example, a new session

   \texttt{MySession} derived from \texttt{HOL} may be produced as

   follows:

 \begin{verbatim}

   isabelle mkdir HOL MySession

   isabelle make

 \end{verbatim}

   The \texttt{isabelle make} job also informs about the file-system

   location of the ultimate results.  The above dry run should be able

   to produce some \texttt{document.pdf} (with dummy title, empty table

   of contents etc.).  Any failure at this stage usually indicates

   technical problems of the {\LaTeX} installation.

   \medskip The detailed arrangement of the session sources is as

   follows.

   \begin{itemize}

   \item Directory \texttt{MySession} holds the required theory files

   $T@1$\texttt{.thy}, \dots, $T@n$\texttt{.thy}.

   \item File \texttt{MySession/ROOT.ML} holds appropriate ML commands

   for loading all wanted theories, usually just

   ``\texttt{use_thy"$T@i$";}'' for any $T@i$ in leaf position of the

   dependency graph.

   \item Directory \texttt{MySession/document} contains everything

   required for the {\LaTeX} stage; 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 $T@i$\texttt{.tex} for each theory.  Isabelle will generate a

   file \texttt{session.tex} holding {\LaTeX} commands to include all

   generated theory output files in topologically sorted order, so

   \verb,\input{session}, in the body of \texttt{root.tex} does the job

   in most situations.

   \item \texttt{IsaMakefile} holds appropriate dependencies and

   invocations of Isabelle tools to control the batch job.  In fact,

   several sessions may be managed by the same \texttt{IsaMakefile}.

   See the \emph{Isabelle System Manual} \cite{isabelle-sys} 

   for further details, especially on

   \texttt{isabelle usedir} and \texttt{isabelle make}.

   \end{itemize}

   One may now start to populate the directory \texttt{MySession}, and

   the file \texttt{MySession/ROOT.ML} accordingly.  The file

   \texttt{MySession/document/root.tex} should also be adapted at some

   point; the default version is mostly self-explanatory.  Note that

   \verb,\isabellestyle, enables fine-tuning of the general appearance

   of characters and mathematical symbols (see also

   \S\ref{sec:doc-prep-symbols}).

   Especially observe the included {\LaTeX} packages \texttt{isabelle}

   (mandatory), \texttt{isabellesym} (required for mathematical

   symbols), and the final \texttt{pdfsetup} (provides sane defaults

   for \texttt{hyperref}, including URL markup).  All three are

   distributed with Isabelle. Further packages may be required in

   particular applications, say for unusual mathematical symbols.

   \medskip Any additional files for the {\LaTeX} stage go into the

   \texttt{MySession/document} directory as well.  In particular,

   adding a file named \texttt{root.bib} causes an automatic run of

   \texttt{bibtex} to process a bibliographic database; see also

   \texttt{isabelle document} \cite{isabelle-sys}.

   \medskip Any failure of the document preparation phase in an

   Isabelle batch session leaves the generated sources in their target

   location, identified by the accompanying error message.  This lets

   you trace {\LaTeX} problems with the generated files at hand.

 *}

 subsection {* Structure Markup *}

 text {*

   The large-scale structure of Isabelle documents follows existing

   {\LaTeX} conventions, with chapters, sections, subsubsections etc.

   The Isar language includes separate \bfindex{markup commands}, which

   do not affect the formal meaning of a theory (or proof), but result

   in corresponding {\LaTeX} elements.

   There are separate markup commands depending on the textual context:

   in header position (just before \isakeyword{theory}), within the

   theory body, or within a proof.  The header needs to be treated

   specially here, since ordinary theory and proof commands may only

   occur \emph{after} the initial \isakeyword{theory} specification.

   \medskip

   \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,",~@{text \<dots>}~\verb,", or

   \verb,{,\verb,*,~@{text \<dots>}~\verb,*,\verb,},).  After stripping any

   surrounding white space, the argument is passed to a {\LaTeX} macro

   \verb,\isamarkupXYZ, for command \isakeyword{XYZ}.  These macros are

   defined in \verb,isabelle.sty, according to the meaning given in the

   rightmost column above.

   \medskip The following source fragment illustrates structure markup

   of a theory.  Note that {\LaTeX} labels may be included inside of

   section headings as well.

   \begin{ttbox}

   header {\ttlbrace}* Some properties of Foo Bar elements *{\ttrbrace}

   theory Foo_Bar

   imports Main

   begin

   subsection {\ttlbrace}* Basic definitions *{\ttrbrace}

   definition foo :: \dots

   definition bar :: \dots

   subsection {\ttlbrace}* Derived rules *{\ttrbrace}

   lemma fooI: \dots

   lemma fooE: \dots

   subsection {\ttlbrace}* Main theorem {\ttback}label{\ttlbrace}sec:main-theorem{\ttrbrace} *{\ttrbrace}

   theorem main: \dots

   end

   \end{ttbox}\vspace{-\medskipamount}

   You may occasionally want to change the meaning of markup commands,

   say via \verb,\renewcommand, in \texttt{root.tex}.  For example,

   \verb,\isamarkupheader, is a good candidate for some tuning.  We

   could move it up in the hierarchy to become \verb,\chapter,.

 \begin{verbatim}

   \renewcommand{\isamarkupheader}[1]{\chapter{#1}}

 \end{verbatim}

   \noindent Now we must change the document class given in

   \texttt{root.tex} to something that supports chapters.  A suitable

   command is \verb,\documentclass{report},.

   \medskip The {\LaTeX} macro \verb,\isabellecontext, is maintained to

   hold the name of the current theory context.  This is particularly

   useful for document headings:

 \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}; the document

   should have more than two pages to show the effect.

 *}

 subsection {* Formal Comments and Antiquotations \label{sec:doc-prep-text} *}

 text {*

   Isabelle \bfindex{source comments}, which are of the form

   \verb,(,\verb,*,~@{text \<dots>}~\verb,*,\verb,),, essentially act like

   white space and do not really contribute to the content.  They

   mainly serve technical purposes to mark certain oddities in the raw

   input text.  In contrast, \bfindex{formal comments} are portions of

   text that are associated with formal Isabelle/Isar commands

   (\bfindex{marginal comments}), or as standalone paragraphs within a

   theory or proof context (\bfindex{text blocks}).

   \medskip Marginal comments are part of each command's concrete

   syntax \cite{isabelle-ref}; the common form is ``\verb,--,~$text$''

   where $text$ is delimited by \verb,",@{text \<dots>}\verb,", or

   \verb,{,\verb,*,~@{text \<dots>}~\verb,*,\verb,}, as before.  Multiple

   marginal comments may be given at the same time.  Here is a simple

   example:

 *}

 lemma "A --> A"

   -- "a triviality of propositional logic"

   -- "(should not really bother)"

   by (rule impI) -- "implicit assumption step involved here"

 text {*

   \noindent The above output has been produced as follows:

 \begin{verbatim}

   lemma "A --> A"

     -- "a triviality of propositional logic"

     -- "(should not really bother)"

     by (rule impI) -- "implicit assumption step involved here"

 \end{verbatim}

   From the {\LaTeX} viewpoint, ``\verb,--,'' acts like a markup

   command, associated with the macro \verb,\isamarkupcmt, (taking a

   single argument).

   \medskip Text blocks are introduced by the commands \bfindex{text}

   and \bfindex{txt}, for theory and proof contexts, respectively.

   Each takes again a single $text$ argument, which is interpreted as a

   free-form paragraph in {\LaTeX} (surrounded by some additional

   vertical space).  This behavior may be changed by redefining the

   {\LaTeX} environments of \verb,isamarkuptext, or

   \verb,isamarkuptxt,, respectively (via \verb,\renewenvironment,) The

   text style of the body is determined by \verb,\isastyletext, and

   \verb,\isastyletxt,; the default setup uses a smaller font within

   proofs.  This may be changed as follows:

 \begin{verbatim}

   \renewcommand{\isastyletxt}{\isastyletext}

 \end{verbatim}

   \medskip The $text$ part of Isabelle markup commands essentially

   inserts \emph{quoted material} into a formal text, mainly for

   instruction of the reader.  An \bfindex{antiquotation} is again a

   formal object embedded into such an informal portion.  The

   interpretation of antiquotations is limited to some well-formedness

   checks, with the result being pretty printed to the resulting

   document.  Quoted text blocks together with antiquotations provide

   an attractive means of referring to formal entities, with good

   confidence in getting the technical details right (especially syntax

   and types).

   The general syntax of antiquotations is as follows:

   \texttt{{\at}{\ttlbrace}$name$ $arguments${\ttrbrace}}, or

   \texttt{{\at}{\ttlbrace}$name$ [$options$] $arguments${\ttrbrace}}

   for a comma-separated list of options consisting of a $name$ or

   \texttt{$name$=$value$} each.  The syntax of $arguments$ depends on

   the kind of antiquotation, it generally follows the same conventions

   for types, terms, or theorems as in the formal part of a theory.

   \medskip This sentence demonstrates quotations and antiquotations:

   @{term "%x y. x"} is a well-typed term.

   \medskip\noindent The output above was produced as follows:

   \begin{ttbox}

 text {\ttlbrace}*

   This sentence demonstrates quotations and antiquotations:

   {\at}{\ttlbrace}term "%x y. x"{\ttrbrace} is a well-typed term.

 *{\ttrbrace}

   \end{ttbox}\vspace{-\medskipamount}

   The notational change from the ASCII character~\verb,%, to the

   symbol~@{text \<lambda>} reveals that Isabelle printed this term, after

   parsing and type-checking.  Document preparation enables symbolic

   output by default.

   \medskip The next example includes an option to show the type of all

   variables.  The antiquotation

   \texttt{{\at}}\verb,{term [show_types] "%x y. x"}, produces the

   output @{term [show_types] "%x y. x"}.  Type inference has figured

   out the most general typings in the present theory context.  Terms

   may acquire different typings due to constraints imposed by their

   environment; within a proof, for example, variables are given the

   same types as they have in the main goal statement.

   \medskip Several further kinds of antiquotations and options are

   available \cite{isabelle-sys}.  Here are a few commonly used

   combinations:

   \medskip

   \begin{tabular}{ll}

   \texttt{\at}\verb,{typ,~$\tau$\verb,}, & print type $\tau$ \\

   \texttt{\at}\verb,{const,~$c$\verb,}, & check existence of $c$ and print it \\

   \texttt{\at}\verb,{term,~$t$\verb,}, & print term $t$ \\

   \texttt{\at}\verb,{prop,~$\phi$\verb,}, & print proposition $\phi$ \\

   \texttt{\at}\verb,{prop [display],~$\phi$\verb,}, & print large proposition $\phi$ (with linebreaks) \\

   \texttt{\at}\verb,{prop [source],~$\phi$\verb,}, & check proposition $\phi$, print its input \\

   \texttt{\at}\verb,{thm,~$a$\verb,}, & print fact $a$ \\

   \texttt{\at}\verb,{thm,~$a$~\verb,[no_vars]}, & print fact $a$, fixing schematic variables \\

   \texttt{\at}\verb,{thm [source],~$a$\verb,}, & check availability of fact $a$, print its name \\

   \texttt{\at}\verb,{text,~$s$\verb,}, & print uninterpreted text $s$ \\

   \end{tabular}

   \medskip

   Note that \attrdx{no_vars} given above is \emph{not} an

   antiquotation option, but an attribute of the theorem argument given

   here.  This might be useful with a diagnostic command like

   \isakeyword{thm}, too.

   \medskip The \texttt{\at}\verb,{text, $s$\verb,}, antiquotation is

   particularly interesting.  Embedding uninterpreted text within an

   informal body might appear useless at first sight.  Here the key

   virtue is that the string $s$ is processed as Isabelle output,

   interpreting Isabelle symbols appropriately.

   For example, \texttt{\at}\verb,{text "\<forall>\<exists>"}, produces @{text

   "\<forall>\<exists>"}, according to the standard interpretation of these symbol

   (cf.\ \S\ref{sec:doc-prep-symbols}).  Thus we achieve consistent

   mathematical notation in both the formal and informal parts of the

   document very easily, independently of the term language of

   Isabelle.  Manual {\LaTeX} code would leave more control over the

   typesetting, but is also slightly more tedious.

 *}

 subsection {* Interpretation of Symbols \label{sec:doc-prep-symbols} *}

 text {*

   As has been pointed out before (\S\ref{sec:syntax-symbols}),

   Isabelle symbols are the smallest syntactic entities --- a

   straightforward generalization of ASCII characters.  While Isabelle

   does not impose any interpretation of the infinite collection of

   named symbols, {\LaTeX} documents use canonical glyphs for certain

   standard symbols \cite{isabelle-isar-ref}.

   The {\LaTeX} code produced from Isabelle text follows a simple

   scheme.  You can tune the final appearance by redefining certain

   macros, say in \texttt{root.tex} of the document.

   \begin{enumerate}

   \item 7-bit ASCII characters: letters \texttt{A\dots Z} and

   \texttt{a\dots z} are output directly, digits are passed as an

   argument to the \verb,\isadigit, macro, other characters are

   replaced by specifically named macros of the form

   \verb,\isacharXYZ,.

   \item Named symbols: \verb,\,\verb,<XYZ>, is turned into

   \verb,{\isasymXYZ},; note the additional braces.

   \item Named control symbols: \verb,\,\verb,<^XYZ>, is turned into

   \verb,\isactrlXYZ,; subsequent symbols may act as arguments if the

   control macro is defined accordingly.

   \end{enumerate}

   You may occasionally wish to give new {\LaTeX} interpretations of

   named symbols.  This merely requires an appropriate definition of

   \verb,\isasymXYZ,, for \verb,\,\verb,<XYZ>, (see

   \texttt{isabelle.sty} for working examples).  Control symbols are

   slightly more difficult to get right, though.

   \medskip The \verb,\isabellestyle, macro provides a high-level

   interface to tune the general appearance of individual symbols.  For

   example, \verb,\isabellestyle{it}, uses the italics text style to

   mimic the general appearance of the {\LaTeX} math mode; double

   quotes are not printed at all.  The resulting quality of typesetting

   is quite good, so this should be the default style for work that

   gets distributed to a broader audience.

 *}

 subsection {* Suppressing Output \label{sec:doc-prep-suppress} *}

 text {*

   By default, Isabelle's document system generates a {\LaTeX} file for

   each theory that gets loaded while running the session.  The

   generated \texttt{session.tex} will include all of these in order of

   appearance, which in turn gets included by the standard

   \texttt{root.tex}.  Certainly one may change the order or suppress

   unwanted theories by ignoring \texttt{session.tex} and load

   individual files directly in \texttt{root.tex}.  On the other hand,

   such an arrangement requires additional maintenance whenever the

   collection of theories changes.

   Alternatively, one may tune the theory loading process in

   \texttt{ROOT.ML} itself: traversal of the theory dependency graph

   may be fine-tuned by adding \verb,use_thy, invocations, although

   topological sorting still has to be observed.  Moreover, the ML

   operator \verb,no_document, temporarily disables document generation

   while executing a theory loader command.  Its usage is like this:

 \begin{verbatim}

   no_document use_thy "T";

 \end{verbatim}

   \medskip Theory output may be suppressed more selectively, either

   via \bfindex{tagged command regions} or \bfindex{ignored material}.

   Tagged command regions works by annotating commands with named tags,

   which correspond to certain {\LaTeX} markup that tells how to treat

   particular parts of a document when doing the actual type-setting.

   By default, certain Isabelle/Isar commands are implicitly marked up

   using the predefined tags ``\emph{theory}'' (for theory begin and

   end), ``\emph{proof}'' (for proof commands), and ``\emph{ML}'' (for

   commands involving ML code).  Users may add their own tags using the

   \verb,%,\emph{tag} notation right after a command name.  In the

   subsequent example we hide a particularly irrelevant proof:

 *}

 lemma "x = x" by %invisible (simp)

 text {*

   The original source has been ``\verb,lemma "x = x" by %invisible (simp),''.

   Tags observe the structure of proofs; adjacent commands with the

   same tag are joined into a single region.  The Isabelle document

   preparation system allows the user to specify how to interpret a

   tagged region, in order to keep, drop, or fold the corresponding

   parts of the document.  See the \emph{Isabelle System Manual}

   \cite{isabelle-sys} for further details, especially on

   \texttt{isabelle usedir} and \texttt{isabelle document}.

   Ignored material is specified by delimiting the original formal

   source with special source comments

   \verb,(,\verb,*,\verb,<,\verb,*,\verb,), and

   \verb,(,\verb,*,\verb,>,\verb,*,\verb,),.  These parts are stripped

   before the type-setting phase, without affecting the formal checking

   of the theory, of course.  For example, we may hide parts of a proof

   that seem unfit for general public inspection.  The following

   ``fully automatic'' proof is actually a fake:

 *}

 lemma "x \<noteq> (0::int) \<Longrightarrow> 0 < x * x"

   by (auto(*<*)simp add: zero_less_mult_iff(*>*))

 text {*

   \noindent The real source of the proof has been as follows:

 \begin{verbatim}

   by (auto(*<*)simp add: zero_less_mult_iff(*>*))

 \end{verbatim}

 %(*

   \medskip Suppressing portions of printed text demands care.  You

   should not misrepresent the underlying theory development.  It is

   easy to invalidate the visible text by hiding references to

   questionable axioms, for example.

 *}

 (*<*)

 end

 (*>*)