doc-src/TutorialI/Documents/document/Documents.tex

 \isamarkupsection{Concrete Syntax \label{sec:concrete-syntax}%
 }
 \isamarkuptrue%
 %
 \begin{isamarkuptext}%
-Concerning Isabelle's ``inner'' language of simply-typed \isa{{\isasymlambda}}-calculus, the core concept of Isabelle's elaborate
-  infrastructure for concrete syntax is that of general
-  \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, the whole affair of parser and pretty printer
-  configuration is rather subtle, see also \cite{isabelle-ref}.
-  Syntax specifications given by end-users need to interact properly
-  with the existing setup of Isabelle/Pure and Isabelle/HOL.  It is
+The core concept of Isabelle's elaborate infrastructure for concrete
+  syntax is that of general \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
+  rather subtle affair, see \cite{isabelle-ref} for details.  Syntax
+  specifications given by end-users need to interact properly with the
+  existing setup of Isabelle/Pure and Isabelle/HOL.  It is
   particularly important to get the precedence of new syntactic
   constructs right, avoiding ambiguities with existing elements.
 
   \medskip Subsequently we introduce a few simple syntax declaration
-  forms that already cover most common situations fairly well.%
+  forms that already cover many common situations fairly well.%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
 \isamarkupsubsection{Infix Annotations%
 }

 \begin{isamarkuptext}%
 Syntax annotations may be included wherever constants are declared
   directly or indirectly, including \isacommand{consts},
   \isacommand{constdefs}, or \isacommand{datatype} (for the
   constructor operations).  Type-constructors may be annotated as
-  well, although this is less frequently encountered in practice
-  (\isa{{\isacharasterisk}} and \isa{{\isacharplus}} types may come to mind).
+  well, although this is less frequently encountered in practice (the
+  infix type \isa{{\isasymtimes}} comes to mind).
 
   Infix declarations\index{infix annotations} provide a useful special
   case of mixfixes, where users need not care about the full details
   of priorities, nesting, spacing, etc.  The following example of the
   exclusive-or operation on boolean values illustrates typical infix

   applications with less than two operands there is a special notation
   with \isa{op} prefix: \isa{xor} without arguments is represented
   as \isa{op\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}}; together with plain prefix application this
   turns \isa{xor\ A} into \isa{op\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ A}.
 
-  \medskip The string \isa{{\isachardoublequote}{\isacharbrackleft}{\isacharplus}{\isacharbrackright}{\isachardoublequote}} in the above annotation
-  refers to the bit of concrete syntax to represent the operator,
+  \medskip The keyword \isakeyword{infixl} specifies an infix operator
+  that is nested to the \emph{left}: in iterated applications the more
+  complex expression appears on the left-hand side: \isa{A\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ B\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ C} stands for \isa{{\isacharparenleft}A\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ B{\isacharparenright}\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ C}.  Similarly,
+  \isakeyword{infixr} specifies to nesting to the \emph{right},
+  reading \isa{A\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ B\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ C} as \isa{A\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ {\isacharparenleft}B\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ C{\isacharparenright}}.  In
+  contrast, a \emph{non-oriented} declaration via \isakeyword{infix}
+  would render \isa{A\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ B\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ C} illegal, but demand explicit
+  parentheses to indicate the intended grouping.
+
+  The string \isa{{\isachardoublequote}{\isacharbrackleft}{\isacharplus}{\isacharbrackright}{\isachardoublequote}} in the above annotation refers to
+  the concrete syntax to represent the operator (a literal token),
   while the number \isa{{\isadigit{6}}{\isadigit{0}}} determines the precedence of the
   construct (i.e.\ the syntactic priorities of the arguments and
-  result).
-
-  As it happens, Isabelle/HOL already spends many popular combinations
-  of ASCII symbols for its own use, including both \isa{{\isacharplus}} and
-  \isa{{\isacharplus}{\isacharplus}}.  Slightly more awkward combinations like the present
-  \isa{{\isacharbrackleft}{\isacharplus}{\isacharbrackright}} tend to be available for user extensions.  The current
-  arrangement of inner syntax may be inspected via
-  \commdx{print\protect\_syntax}, albeit its output is enormous.
+  result).  As it happens, Isabelle/HOL already uses up many popular
+  combinations of ASCII symbols for its own use, including both \isa{{\isacharplus}} and \isa{{\isacharplus}{\isacharplus}}.  Slightly more awkward combinations like the
+  present \isa{{\isacharbrackleft}{\isacharplus}{\isacharbrackright}} tend to be available for user extensions.
 
   Operator precedence also needs some special considerations.  The
   admissible range is 0--1000.  Very low or high priorities are
   basically reserved for the meta-logic.  Syntax of Isabelle/HOL
   mainly uses the range of 10--100: the equality infix \isa{{\isacharequal}} is
   centered at 50, logical connectives (like \isa{{\isasymor}} and \isa{{\isasymand}}) are below 50, and algebraic ones (like \isa{{\isacharplus}} and \isa{{\isacharasterisk}}) above 50.  User syntax should strive to coexist with common
-  HOL forms, or use the mostly unused range 100--900.
-
-  The keyword \isakeyword{infixl} specifies an infix operator that is
-  nested to the \emph{left}: in iterated applications the more complex
-  expression appears on the left-hand side: \isa{A\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ B\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ C}
-  stands for \isa{{\isacharparenleft}A\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ B{\isacharparenright}\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ C}.  Similarly,
-  \isakeyword{infixr} specifies to nesting to the \emph{right},
-  reading \isa{A\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ B\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ C} as \isa{A\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ {\isacharparenleft}B\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ C{\isacharparenright}}.  In
-  contrast, a \emph{non-oriented} declaration via \isakeyword{infix}
-  would render \isa{A\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ B\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ C} illegal, but demand explicit
-  parentheses to indicate the intended grouping.%
+  HOL forms, or use the mostly unused range 100--900.%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
 \isamarkupsubsection{Mathematical Symbols \label{sec:syntax-symbols}%
 }

   Here $ident$ may be any identifier according to the usual Isabelle
   conventions.  This results in an infinite store of symbols, whose
   interpretation is left to further front-end tools.  For example,
   both 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 really as \isa{{\isasymforall}}.
+  the \verb,\,\verb,<forall>, symbol as \isa{{\isasymforall}}.
 
   A list of standard Isabelle symbols is given in
   \cite[appendix~A]{isabelle-sys}.  Users may introduce their own
   interpretation of further symbols by configuring the appropriate
   front-end tool accordingly, e.g.\ by defining certain {\LaTeX}

 \ \ xor\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}bool\ {\isasymRightarrow}\ bool\ {\isasymRightarrow}\ bool{\isachardoublequote}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequote}{\isasymoplus}{\isasymignore}{\isachardoublequote}\ {\isadigit{6}}{\isadigit{0}}{\isacharparenright}\isamarkupfalse%
 \isamarkupfalse%
 %
 \begin{isamarkuptext}%
 The \commdx{syntax} command introduced here acts like
-  \isakeyword{consts}, but without declaring a logical constant; an
-  optional print mode specification may be given, too.  Note that the
-  type declaration given above merely serves for syntactic purposes,
-  and is not checked for consistency with the real constant.
+  \isakeyword{consts}, but without declaring a logical constant.  The
+  print mode specification (here \isa{{\isacharparenleft}xsymbols{\isacharparenright}}) limits the
+  effect of the syntax annotation concerning output; that alternative
+  production available for input invariably.  Also note that the type
+  declaration in \isakeyword{syntax} merely serves for syntactic
+  purposes, and is \emph{not} checked for consistency with the real
+  constant.
 
   \medskip We may now write \isa{A\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ B} or \isa{A\ {\isasymoplus}\ B} in
   input, while output uses the nicer syntax of $xsymbols$, provided
   that print mode is active.  Such an arrangement is particularly
   useful for interactive development, where users may type plain ASCII
-  text, but gain improved visual feedback from the system.
-
-  \begin{warn}
-  Alternative syntax declarations are apt to result in varying
-  occurrences of concrete syntax in the input sources.  Isabelle
-  provides no systematic way to convert alternative syntax expressions
-  back and forth; print modes only affect situations where formal
-  entities are pretty printed by the Isabelle process (e.g.\ output of
-  terms and types), but not the original theory text.
-  \end{warn}
-
-  \medskip The following variant makes the alternative \isa{{\isasymoplus}}
-  notation only available for output.  Thus we may enforce input
-  sources to refer to plain ASCII only, but effectively disable
-  cut-and-paste from output at the same time.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-\isacommand{syntax}\ {\isacharparenleft}xsymbols\ \isakeyword{output}{\isacharparenright}\isanewline
-\ \ xor\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}bool\ {\isasymRightarrow}\ bool\ {\isasymRightarrow}\ bool{\isachardoublequote}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequote}{\isasymoplus}{\isasymignore}{\isachardoublequote}\ {\isadigit{6}}{\isadigit{0}}{\isacharparenright}\isamarkupfalse%
+  text, but gain improved visual feedback from the system.%
+\end{isamarkuptext}%
+\isamarkuptrue%
 %
 \isamarkupsubsection{Prefix Annotations%
 }
 \isamarkuptrue%
 %
 \begin{isamarkuptext}%
-Prefix syntax annotations\index{prefix annotation} are just another
+Prefix syntax annotations\index{prefix annotation} are another
   degenerate form of mixfixes \cite{isabelle-ref}, without any
   template arguments or priorities --- just some bits of literal
   syntax.  The following example illustrates this idea idea by
   associating common symbols with the constructors of a datatype.%
 \end{isamarkuptext}%

 \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 \isa{Euro} actually is a function \isa{nat\ {\isasymRightarrow}\ currency}.  An expression like \isa{Euro\ {\isadigit{1}}{\isadigit{0}}} will be
   printed as \isa{{\isasymeuro}\ {\isadigit{1}}{\isadigit{0}}}; only the head of the application is
-  subject to our concrete syntax.  This simple form already achieves
-  conformance with notational standards of the European Commission.
+  subject to our concrete syntax.  This rather simple form already
+  achieves conformance with notational standards of the European
+  Commission.
 
   Prefix syntax also works for plain \isakeyword{consts} or
   \isakeyword{constdefs}, of course.%
 \end{isamarkuptext}%
 \isamarkuptrue%

 \isamarkuptrue%
 %
 \begin{isamarkuptext}%
 Mixfix syntax annotations work well in those situations where
   particular constant application forms need to be decorated by
-  concrete syntax; just reconsider \isa{xor\ A\ B} versus \isa{A\ {\isasymoplus}\ B} covered before.  Occasionally the relationship between some
-  piece of notation and its internal form is slightly more involved.
-  Here the concept of \bfindex{syntax translations} enters the scene.
+  concrete syntax; e.g.\ \isa{xor\ A\ B} versus \isa{A\ {\isasymoplus}\ B}
+  covered before.  Occasionally the relationship between some piece of
+  notation and its internal form is slightly more involved.  Here the
+  concept of \bfindex{syntax translations} enters the scene.
 
   Using the raw \isakeyword{syntax}\index{syntax (command)} command we
   may introduce uninterpreted notational elements, while
-  \commdx{translations} relates input forms with more complex logical
+  \commdx{translations} relate input forms with more complex logical
   expressions.  This essentially provides a simple mechanism for
   syntactic macros; even heavier transformations may be written in ML
   \cite{isabelle-ref}.
 
   \medskip A typical example of syntax translations is to decorate
-  relational expressions (i.e.\ set-membership of tuples) with
-  handsome symbolic notation, such as \isa{{\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}\ {\isasymin}\ sim} versus
-  \isa{x\ {\isasymapprox}\ y}.%
+  relational expressions (i.e.\ set-membership of tuples) with nice
+  symbolic notation, such as \isa{{\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}\ {\isasymin}\ sim} versus \isa{x\ {\isasymapprox}\ y}.%
 \end{isamarkuptext}%
 \isamarkuptrue%
 \isacommand{consts}\isanewline
 \ \ sim\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set{\isachardoublequote}\isanewline
 \isanewline

   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.
 
-  The Isar proof language \cite{Wenzel-PhD}, which is not covered in
-  this book, admits to write formal proof texts that are acceptable
-  both to the machine and human readers at the same time.  Thus
-  marginal comments and explanations may be kept at a minimum.  Even
-  without proper coverage of human-readable proofs, Isabelle document
-  preparation is very useful to produce formally derived texts.
-  Unstructured proof scripts given here may be just ignored by
-  readers, or intentionally suppressed from the text by the writer
-  (see also \S\ref{sec:doc-prep-suppress}).
-
   \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 enables users to write
   authentic reports on theory developments with little effort, where

 %
 \begin{isamarkuptext}%
 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 theory source files that may contribute to an output document
+  of source files that may contribute to an output document
   eventually.  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,).
 

 \end{verbatim}
 
   The \texttt{isatool 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 that stage usually indicates
+  of contents etc.).  Any failure at this stage usually indicates
   technical problems of the {\LaTeX} installation.\footnote{Especially
   make sure that \texttt{pdflatex} is present; if all fails one may
   fall back on DVI output by changing \texttt{usedir} options in
   \texttt{IsaMakefile} \cite{isabelle-sys}.}
 
   \medskip The detailed arrangement of the session sources is as
-  follows:
+  follows; advanced
 
   \begin{itemize}
 
   \item Directory \texttt{MySession} holds the required theory files
   $T@1$\texttt{.thy}, \dots, $T@n$\texttt{.thy}.

   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.  The generated
-  \texttt{session.tex} will contain {\LaTeX} commands to include all
-  generated files in topologically sorted order, so
+  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 \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,

   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 handsome
-  defaults for \texttt{hyperref}, including URL markup) --- all three
-  are distributed with Isabelle. Further packages may be required in
+  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, e.g.\ for unusual mathematical symbols.
 
   \medskip Additional files for the {\LaTeX} stage may be put into the
   \texttt{MySession/document} directory, too.  In particular, adding
   \texttt{root.bib} here (with that specific name) causes an automatic

 
 \begin{verbatim}
   \renewcommand{\isamarkupheader}[1]{\chapter{#1}}
 \end{verbatim}
 
-  \noindent Certainly, this requires to change the default
-  \verb,\documentclass{article}, in \texttt{root.tex} to something
-  that supports the notion of chapters in the first place, e.g.\
-  \verb,\documentclass{report},.
+  \noindent That particular modification requires to change the
+  default \verb,\documentclass{article}, in \texttt{root.tex} to
+  something that supports the notion of chapters in the first place,
+  such as \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:
 

   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.  So quoted text blocks together
-  with antiquotations provide very handsome means to reference formal
+  with antiquotations provide very useful means to reference 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}\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 validity of fact $a$, print its name \\
+  \texttt{\at}\verb,{thm [source],~$a$\verb,}, & check availability of fact, print name $a$ \\
   \texttt{\at}\verb,{text,~$s$\verb,}, & print uninterpreted text $s$ \\
   \end{tabular}
 
   \medskip
 

 
   \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 usually be the default
-  style for real production work that gets distributed to a broader
-  audience.%
+  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.%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
 \isamarkupsubsection{Suppressing Output \label{sec:doc-prep-suppress}%
 }
 \isamarkuptrue%
 %
 \begin{isamarkuptext}%
 By default, Isabelle's document system generates a {\LaTeX} source
-  file for each theory that happens to get 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
-  include individual files in \texttt{root.tex} by hand.  On the other
-  hand, such an arrangement requires additional maintenance chores
-  whenever the collection of theories changes.
+  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 include
+  individual files in \texttt{root.tex} by hand.  On the other hand,
+  such an arrangement requires additional maintenance chores 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

   is fairly easy to invalidate the remaining visible text, e.g.\ by
   referencing questionable formal items (strange definitions,
   arbitrary axioms etc.) that have been hidden from sight beforehand.
 
   Authentic reports of formal theories, say as part of a library,
-  usually should refrain from suppressing parts of the text at all.
-  Other users may need the full information for their own derivative
-  work.  If a particular formalization appears inadequate for general
-  public coverage, it is often more appropriate to think of a better
-  way in the first place.
+  should refrain from suppressing parts of the text at all.  Other
+  users may need the full information for their own derivative work.
+  If a particular formalization appears inadequate for general public
+  coverage, it is often more appropriate to think of a better way in
+  the first place.
 
   \medskip Some technical subtleties of the
   \verb,(,\verb,*,\verb,<,\verb,*,\verb,),~\verb,(,\verb,*,\verb,>,\verb,*,\verb,),
   elements need to be kept in mind, too --- the system performs little
   sanity checks here.  Arguments of markup commands and formal