doc-src/IsarRef/Thy/document/Document_Preparation.tex
author wenzelm
Mon Mar 09 21:25:33 2009 +0100 (2009-03-09)
changeset 30397 b6212ae21656
parent 30172 afdf7808cfd0
child 32893 dbef0e6438ec
permissions -rw-r--r--
markup antiquotation options;
more correct references to external manuals;
     1 %
     2 \begin{isabellebody}%
     3 \def\isabellecontext{Document{\isacharunderscore}Preparation}%
     4 %
     5 \isadelimtheory
     6 %
     7 \endisadelimtheory
     8 %
     9 \isatagtheory
    10 \isacommand{theory}\isamarkupfalse%
    11 \ Document{\isacharunderscore}Preparation\isanewline
    12 \isakeyword{imports}\ Main\isanewline
    13 \isakeyword{begin}%
    14 \endisatagtheory
    15 {\isafoldtheory}%
    16 %
    17 \isadelimtheory
    18 %
    19 \endisadelimtheory
    20 %
    21 \isamarkupchapter{Document preparation \label{ch:document-prep}%
    22 }
    23 \isamarkuptrue%
    24 %
    25 \begin{isamarkuptext}%
    26 Isabelle/Isar provides a simple document preparation system
    27   based on regular {PDF-\LaTeX} technology, with full support for
    28   hyper-links and bookmarks.  Thus the results are well suited for WWW
    29   browsing and as printed copies.
    30 
    31   \medskip Isabelle generates {\LaTeX} output while running a
    32   \emph{logic session} (see also \cite{isabelle-sys}).  Getting
    33   started with a working configuration for common situations is quite
    34   easy by using the Isabelle \verb|mkdir| and \verb|make|
    35   tools.  First invoke
    36 \begin{ttbox}
    37   isabelle mkdir Foo
    38 \end{ttbox}
    39   to initialize a separate directory for session \verb|Foo| (it
    40   is safe to experiment, since \verb|isabelle mkdir| never
    41   overwrites existing files).  Ensure that \verb|Foo/ROOT.ML|
    42   holds ML commands to load all theories required for this session;
    43   furthermore \verb|Foo/document/root.tex| should include any
    44   special {\LaTeX} macro packages required for your document (the
    45   default is usually sufficient as a start).
    46 
    47   The session is controlled by a separate \verb|IsaMakefile|
    48   (with crude source dependencies by default).  This file is located
    49   one level up from the \verb|Foo| directory location.  Now
    50   invoke
    51 \begin{ttbox}
    52   isabelle make Foo
    53 \end{ttbox}
    54   to run the \verb|Foo| session, with browser information and
    55   document preparation enabled.  Unless any errors are reported by
    56   Isabelle or {\LaTeX}, the output will appear inside the directory
    57   defined by the \verb|ISABELLE_BROWSER_INFO| setting (as
    58   reported by the batch job in verbose mode).
    59 
    60   \medskip You may also consider to tune the \verb|usedir|
    61   options in \verb|IsaMakefile|, for example to switch the output
    62   format between \verb|pdf| and \verb|dvi|, or activate the
    63   \verb|-D| option to retain a second copy of the generated
    64   {\LaTeX} sources (for manual inspection or separate runs of
    65   \hyperlink{executable.latex}{\mbox{\isa{\isatt{latex}}}}).
    66 
    67   \medskip See \emph{The Isabelle System Manual} \cite{isabelle-sys}
    68   for further details on Isabelle logic sessions and theory
    69   presentation.  The Isabelle/HOL tutorial \cite{isabelle-hol-book}
    70   also covers theory presentation to some extent.%
    71 \end{isamarkuptext}%
    72 \isamarkuptrue%
    73 %
    74 \isamarkupsection{Markup commands \label{sec:markup}%
    75 }
    76 \isamarkuptrue%
    77 %
    78 \begin{isamarkuptext}%
    79 \begin{matharray}{rcl}
    80     \indexdef{}{command}{header}\hypertarget{command.header}{\hyperlink{command.header}{\mbox{\isa{\isacommand{header}}}}} & : & \isa{{\isachardoublequote}toplevel\ {\isasymrightarrow}\ toplevel{\isachardoublequote}} \\[0.5ex]
    81     \indexdef{}{command}{chapter}\hypertarget{command.chapter}{\hyperlink{command.chapter}{\mbox{\isa{\isacommand{chapter}}}}} & : & \isa{{\isachardoublequote}local{\isacharunderscore}theory\ {\isasymrightarrow}\ local{\isacharunderscore}theory{\isachardoublequote}} \\
    82     \indexdef{}{command}{section}\hypertarget{command.section}{\hyperlink{command.section}{\mbox{\isa{\isacommand{section}}}}} & : & \isa{{\isachardoublequote}local{\isacharunderscore}theory\ {\isasymrightarrow}\ local{\isacharunderscore}theory{\isachardoublequote}} \\
    83     \indexdef{}{command}{subsection}\hypertarget{command.subsection}{\hyperlink{command.subsection}{\mbox{\isa{\isacommand{subsection}}}}} & : & \isa{{\isachardoublequote}local{\isacharunderscore}theory\ {\isasymrightarrow}\ local{\isacharunderscore}theory{\isachardoublequote}} \\
    84     \indexdef{}{command}{subsubsection}\hypertarget{command.subsubsection}{\hyperlink{command.subsubsection}{\mbox{\isa{\isacommand{subsubsection}}}}} & : & \isa{{\isachardoublequote}local{\isacharunderscore}theory\ {\isasymrightarrow}\ local{\isacharunderscore}theory{\isachardoublequote}} \\
    85     \indexdef{}{command}{text}\hypertarget{command.text}{\hyperlink{command.text}{\mbox{\isa{\isacommand{text}}}}} & : & \isa{{\isachardoublequote}local{\isacharunderscore}theory\ {\isasymrightarrow}\ local{\isacharunderscore}theory{\isachardoublequote}} \\
    86     \indexdef{}{command}{text\_raw}\hypertarget{command.text-raw}{\hyperlink{command.text-raw}{\mbox{\isa{\isacommand{text{\isacharunderscore}raw}}}}} & : & \isa{{\isachardoublequote}local{\isacharunderscore}theory\ {\isasymrightarrow}\ local{\isacharunderscore}theory{\isachardoublequote}} \\[0.5ex]
    87     \indexdef{}{command}{sect}\hypertarget{command.sect}{\hyperlink{command.sect}{\mbox{\isa{\isacommand{sect}}}}} & : & \isa{{\isachardoublequote}proof\ {\isasymrightarrow}\ proof{\isachardoublequote}} \\
    88     \indexdef{}{command}{subsect}\hypertarget{command.subsect}{\hyperlink{command.subsect}{\mbox{\isa{\isacommand{subsect}}}}} & : & \isa{{\isachardoublequote}proof\ {\isasymrightarrow}\ proof{\isachardoublequote}} \\
    89     \indexdef{}{command}{subsubsect}\hypertarget{command.subsubsect}{\hyperlink{command.subsubsect}{\mbox{\isa{\isacommand{subsubsect}}}}} & : & \isa{{\isachardoublequote}proof\ {\isasymrightarrow}\ proof{\isachardoublequote}} \\
    90     \indexdef{}{command}{txt}\hypertarget{command.txt}{\hyperlink{command.txt}{\mbox{\isa{\isacommand{txt}}}}} & : & \isa{{\isachardoublequote}proof\ {\isasymrightarrow}\ proof{\isachardoublequote}} \\
    91     \indexdef{}{command}{txt\_raw}\hypertarget{command.txt-raw}{\hyperlink{command.txt-raw}{\mbox{\isa{\isacommand{txt{\isacharunderscore}raw}}}}} & : & \isa{{\isachardoublequote}proof\ {\isasymrightarrow}\ proof{\isachardoublequote}} \\
    92   \end{matharray}
    93 
    94   Markup commands provide a structured way to insert text into the
    95   document generated from a theory.  Each markup command takes a
    96   single \hyperlink{syntax.text}{\mbox{\isa{text}}} argument, which is passed as argument to a
    97   corresponding {\LaTeX} macro.  The default macros provided by
    98   \hyperlink{file.~~/lib/texinputs/isabelle.sty}{\mbox{\isa{\isatt{{\isachartilde}{\isachartilde}{\isacharslash}lib{\isacharslash}texinputs{\isacharslash}isabelle{\isachardot}sty}}}} can be redefined according
    99   to the needs of the underlying document and {\LaTeX} styles.
   100 
   101   Note that formal comments (\secref{sec:comments}) are similar to
   102   markup commands, but have a different status within Isabelle/Isar
   103   syntax.
   104 
   105   \begin{rail}
   106     ('chapter' | 'section' | 'subsection' | 'subsubsection' | 'text') target? text
   107     ;
   108     ('header' | 'text\_raw' | 'sect' | 'subsect' | 'subsubsect' | 'txt' | 'txt\_raw') text
   109     ;
   110   \end{rail}
   111 
   112   \begin{description}
   113 
   114   \item \hyperlink{command.header}{\mbox{\isa{\isacommand{header}}}} provides plain text markup just preceding
   115   the formal beginning of a theory.  The corresponding {\LaTeX} macro
   116   is \verb|\isamarkupheader|, which acts like \hyperlink{command.section}{\mbox{\isa{\isacommand{section}}}} by default.
   117   
   118   \item \hyperlink{command.chapter}{\mbox{\isa{\isacommand{chapter}}}}, \hyperlink{command.section}{\mbox{\isa{\isacommand{section}}}}, \hyperlink{command.subsection}{\mbox{\isa{\isacommand{subsection}}}},
   119   and \hyperlink{command.subsubsection}{\mbox{\isa{\isacommand{subsubsection}}}} mark chapter and section headings
   120   within the main theory body or local theory targets.  The
   121   corresponding {\LaTeX} macros are \verb|\isamarkupchapter|,
   122   \verb|\isamarkupsection|, \verb|\isamarkupsubsection| etc.
   123 
   124   \item \hyperlink{command.sect}{\mbox{\isa{\isacommand{sect}}}}, \hyperlink{command.subsect}{\mbox{\isa{\isacommand{subsect}}}}, and \hyperlink{command.subsubsect}{\mbox{\isa{\isacommand{subsubsect}}}}
   125   mark section headings within proofs.  The corresponding {\LaTeX}
   126   macros are \verb|\isamarkupsect|, \verb|\isamarkupsubsect| etc.
   127 
   128   \item \hyperlink{command.text}{\mbox{\isa{\isacommand{text}}}} and \hyperlink{command.txt}{\mbox{\isa{\isacommand{txt}}}} specify paragraphs of plain
   129   text.  This corresponds to a {\LaTeX} environment \verb|\begin{isamarkuptext}| \isa{{\isachardoublequote}{\isasymdots}{\isachardoublequote}} \verb|\end{isamarkuptext}| etc.
   130 
   131   \item \hyperlink{command.text-raw}{\mbox{\isa{\isacommand{text{\isacharunderscore}raw}}}} and \hyperlink{command.txt-raw}{\mbox{\isa{\isacommand{txt{\isacharunderscore}raw}}}} insert {\LaTeX}
   132   source into the output, without additional markup.  Thus the full
   133   range of document manipulations becomes available, at the risk of
   134   messing up document output.
   135 
   136   \end{description}
   137 
   138   Except for \hyperlink{command.text-raw}{\mbox{\isa{\isacommand{text{\isacharunderscore}raw}}}} and \hyperlink{command.txt-raw}{\mbox{\isa{\isacommand{txt{\isacharunderscore}raw}}}}, the text
   139   passed to any of the above markup commands may refer to formal
   140   entities via \emph{document antiquotations}, see also
   141   \secref{sec:antiq}.  These are interpreted in the present theory or
   142   proof context, or the named \isa{{\isachardoublequote}target{\isachardoublequote}}.
   143 
   144   \medskip The proof markup commands closely resemble those for theory
   145   specifications, but have a different formal status and produce
   146   different {\LaTeX} macros.  The default definitions coincide for
   147   analogous commands such as \hyperlink{command.section}{\mbox{\isa{\isacommand{section}}}} and \hyperlink{command.sect}{\mbox{\isa{\isacommand{sect}}}}.%
   148 \end{isamarkuptext}%
   149 \isamarkuptrue%
   150 %
   151 \isamarkupsection{Document Antiquotations \label{sec:antiq}%
   152 }
   153 \isamarkuptrue%
   154 %
   155 \begin{isamarkuptext}%
   156 \begin{matharray}{rcl}
   157     \indexdef{}{antiquotation}{theory}\hypertarget{antiquotation.theory}{\hyperlink{antiquotation.theory}{\mbox{\isa{theory}}}} & : & \isa{antiquotation} \\
   158     \indexdef{}{antiquotation}{thm}\hypertarget{antiquotation.thm}{\hyperlink{antiquotation.thm}{\mbox{\isa{thm}}}} & : & \isa{antiquotation} \\
   159     \indexdef{}{antiquotation}{lemma}\hypertarget{antiquotation.lemma}{\hyperlink{antiquotation.lemma}{\mbox{\isa{lemma}}}} & : & \isa{antiquotation} \\
   160     \indexdef{}{antiquotation}{prop}\hypertarget{antiquotation.prop}{\hyperlink{antiquotation.prop}{\mbox{\isa{prop}}}} & : & \isa{antiquotation} \\
   161     \indexdef{}{antiquotation}{term}\hypertarget{antiquotation.term}{\hyperlink{antiquotation.term}{\mbox{\isa{term}}}} & : & \isa{antiquotation} \\
   162     \indexdef{}{antiquotation}{const}\hypertarget{antiquotation.const}{\hyperlink{antiquotation.const}{\mbox{\isa{const}}}} & : & \isa{antiquotation} \\
   163     \indexdef{}{antiquotation}{abbrev}\hypertarget{antiquotation.abbrev}{\hyperlink{antiquotation.abbrev}{\mbox{\isa{abbrev}}}} & : & \isa{antiquotation} \\
   164     \indexdef{}{antiquotation}{typeof}\hypertarget{antiquotation.typeof}{\hyperlink{antiquotation.typeof}{\mbox{\isa{typeof}}}} & : & \isa{antiquotation} \\
   165     \indexdef{}{antiquotation}{typ}\hypertarget{antiquotation.typ}{\hyperlink{antiquotation.typ}{\mbox{\isa{typ}}}} & : & \isa{antiquotation} \\
   166     \indexdef{}{antiquotation}{thm\_style}\hypertarget{antiquotation.thm-style}{\hyperlink{antiquotation.thm-style}{\mbox{\isa{thm{\isacharunderscore}style}}}} & : & \isa{antiquotation} \\
   167     \indexdef{}{antiquotation}{term\_style}\hypertarget{antiquotation.term-style}{\hyperlink{antiquotation.term-style}{\mbox{\isa{term{\isacharunderscore}style}}}} & : & \isa{antiquotation} \\
   168     \indexdef{}{antiquotation}{text}\hypertarget{antiquotation.text}{\hyperlink{antiquotation.text}{\mbox{\isa{text}}}} & : & \isa{antiquotation} \\
   169     \indexdef{}{antiquotation}{goals}\hypertarget{antiquotation.goals}{\hyperlink{antiquotation.goals}{\mbox{\isa{goals}}}} & : & \isa{antiquotation} \\
   170     \indexdef{}{antiquotation}{subgoals}\hypertarget{antiquotation.subgoals}{\hyperlink{antiquotation.subgoals}{\mbox{\isa{subgoals}}}} & : & \isa{antiquotation} \\
   171     \indexdef{}{antiquotation}{prf}\hypertarget{antiquotation.prf}{\hyperlink{antiquotation.prf}{\mbox{\isa{prf}}}} & : & \isa{antiquotation} \\
   172     \indexdef{}{antiquotation}{full\_prf}\hypertarget{antiquotation.full-prf}{\hyperlink{antiquotation.full-prf}{\mbox{\isa{full{\isacharunderscore}prf}}}} & : & \isa{antiquotation} \\
   173     \indexdef{}{antiquotation}{ML}\hypertarget{antiquotation.ML}{\hyperlink{antiquotation.ML}{\mbox{\isa{ML}}}} & : & \isa{antiquotation} \\
   174     \indexdef{}{antiquotation}{ML\_type}\hypertarget{antiquotation.ML-type}{\hyperlink{antiquotation.ML-type}{\mbox{\isa{ML{\isacharunderscore}type}}}} & : & \isa{antiquotation} \\
   175     \indexdef{}{antiquotation}{ML\_struct}\hypertarget{antiquotation.ML-struct}{\hyperlink{antiquotation.ML-struct}{\mbox{\isa{ML{\isacharunderscore}struct}}}} & : & \isa{antiquotation} \\
   176   \end{matharray}
   177 
   178   The overall content of an Isabelle/Isar theory may alternate between
   179   formal and informal text.  The main body consists of formal
   180   specification and proof commands, interspersed with markup commands
   181   (\secref{sec:markup}) or document comments (\secref{sec:comments}).
   182   The argument of markup commands quotes informal text to be printed
   183   in the resulting document, but may again refer to formal entities
   184   via \emph{document antiquotations}.
   185 
   186   For example, embedding of ``\isa{{\isacharat}{\isacharbraceleft}term\ {\isacharbrackleft}show{\isacharunderscore}types{\isacharbrackright}\ {\isachardoublequote}f\ x\ {\isacharequal}\ a\ {\isacharplus}\ x{\isachardoublequote}{\isacharbraceright}}''
   187   within a text block makes
   188   \isa{{\isacharparenleft}f{\isasymColon}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isacharparenright}\ {\isacharparenleft}x{\isasymColon}{\isacharprime}a{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}a{\isasymColon}{\isacharprime}a{\isacharparenright}\ {\isacharplus}\ x} appear in the final {\LaTeX} document.
   189 
   190   Antiquotations usually spare the author tedious typing of logical
   191   entities in full detail.  Even more importantly, some degree of
   192   consistency-checking between the main body of formal text and its
   193   informal explanation is achieved, since terms and types appearing in
   194   antiquotations are checked within the current theory or proof
   195   context.
   196 
   197   \begin{rail}
   198     atsign lbrace antiquotation rbrace
   199     ;
   200 
   201     antiquotation:
   202       'theory' options name |
   203       'thm' options thmrefs |
   204       'lemma' options prop 'by' method |
   205       'prop' options prop |
   206       'term' options term |
   207       'const' options term |
   208       'abbrev' options term |
   209       'typeof' options term |
   210       'typ' options type |
   211       'thm\_style' options name thmref |
   212       'term\_style' options name term |
   213       'text' options name |
   214       'goals' options |
   215       'subgoals' options |
   216       'prf' options thmrefs |
   217       'full\_prf' options thmrefs |
   218       'ML' options name |
   219       'ML\_type' options name |
   220       'ML\_struct' options name
   221     ;
   222     options: '[' (option * ',') ']'
   223     ;
   224     option: name | name '=' name
   225     ;
   226   \end{rail}
   227 
   228   Note that the syntax of antiquotations may \emph{not} include source
   229   comments \verb|(*|~\isa{{\isachardoublequote}{\isasymdots}{\isachardoublequote}}~\verb|*)| nor verbatim
   230   text \verb|{|\verb|*|~\isa{{\isachardoublequote}{\isasymdots}{\isachardoublequote}}~\verb|*|\verb|}|.
   231 
   232   \begin{description}
   233   
   234   \item \isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}theory\ A{\isacharbraceright}{\isachardoublequote}} prints the name \isa{{\isachardoublequote}A{\isachardoublequote}}, which is
   235   guaranteed to refer to a valid ancestor theory in the current
   236   context.
   237 
   238   \item \isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}thm\ a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n{\isacharbraceright}{\isachardoublequote}} prints theorems \isa{{\isachardoublequote}a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n{\isachardoublequote}}.
   239   Full fact expressions are allowed here, including attributes
   240   (\secref{sec:syn-att}).
   241 
   242   \item \isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}prop\ {\isasymphi}{\isacharbraceright}{\isachardoublequote}} prints a well-typed proposition \isa{{\isachardoublequote}{\isasymphi}{\isachardoublequote}}.
   243 
   244   \item \isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}lemma\ {\isasymphi}\ by\ m{\isacharbraceright}{\isachardoublequote}} proves a well-typed proposition
   245   \isa{{\isachardoublequote}{\isasymphi}{\isachardoublequote}} by method \isa{m} and prints the original \isa{{\isachardoublequote}{\isasymphi}{\isachardoublequote}}.
   246 
   247   \item \isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}term\ t{\isacharbraceright}{\isachardoublequote}} prints a well-typed term \isa{{\isachardoublequote}t{\isachardoublequote}}.
   248 
   249   \item \isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}const\ c{\isacharbraceright}{\isachardoublequote}} prints a logical or syntactic constant
   250   \isa{{\isachardoublequote}c{\isachardoublequote}}.
   251   
   252   \item \isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}abbrev\ c\ x\isactrlsub {\isadigit{1}}\ {\isasymdots}\ x\isactrlsub n{\isacharbraceright}{\isachardoublequote}} prints a constant abbreviation
   253   \isa{{\isachardoublequote}c\ x\isactrlsub {\isadigit{1}}\ {\isasymdots}\ x\isactrlsub n\ {\isasymequiv}\ rhs{\isachardoublequote}} as defined in the current context.
   254 
   255   \item \isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}typeof\ t{\isacharbraceright}{\isachardoublequote}} prints the type of a well-typed term
   256   \isa{{\isachardoublequote}t{\isachardoublequote}}.
   257 
   258   \item \isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}typ\ {\isasymtau}{\isacharbraceright}{\isachardoublequote}} prints a well-formed type \isa{{\isachardoublequote}{\isasymtau}{\isachardoublequote}}.
   259   
   260   \item \isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}thm{\isacharunderscore}style\ s\ a{\isacharbraceright}{\isachardoublequote}} prints theorem \isa{a},
   261   previously applying a style \isa{s} to it (see below).
   262   
   263   \item \isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}term{\isacharunderscore}style\ s\ t{\isacharbraceright}{\isachardoublequote}} prints a well-typed term \isa{t}
   264   after applying a style \isa{s} to it (see below).
   265 
   266   \item \isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}text\ s{\isacharbraceright}{\isachardoublequote}} prints uninterpreted source text \isa{s}.  This is particularly useful to print portions of text according
   267   to the Isabelle document style, without demanding well-formedness,
   268   e.g.\ small pieces of terms that should not be parsed or
   269   type-checked yet.
   270 
   271   \item \isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}goals{\isacharbraceright}{\isachardoublequote}} prints the current \emph{dynamic} goal
   272   state.  This is mainly for support of tactic-emulation scripts
   273   within Isar.  Presentation of goal states does not conform to the
   274   idea of human-readable proof documents!
   275 
   276   When explaining proofs in detail it is usually better to spell out
   277   the reasoning via proper Isar proof commands, instead of peeking at
   278   the internal machine configuration.
   279   
   280   \item \isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}subgoals{\isacharbraceright}{\isachardoublequote}} is similar to \isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}goals{\isacharbraceright}{\isachardoublequote}}, but
   281   does not print the main goal.
   282   
   283   \item \isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}prf\ a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n{\isacharbraceright}{\isachardoublequote}} prints the (compact) proof terms
   284   corresponding to the theorems \isa{{\isachardoublequote}a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n{\isachardoublequote}}. Note that this
   285   requires proof terms to be switched on for the current logic
   286   session.
   287   
   288   \item \isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}full{\isacharunderscore}prf\ a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n{\isacharbraceright}{\isachardoublequote}} is like \isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}prf\ a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n{\isacharbraceright}{\isachardoublequote}}, but prints the full proof terms, i.e.\ also displays
   289   information omitted in the compact proof term, which is denoted by
   290   ``\isa{{\isacharunderscore}}'' placeholders there.
   291   
   292   \item \isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}ML\ s{\isacharbraceright}{\isachardoublequote}}, \isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}ML{\isacharunderscore}type\ s{\isacharbraceright}{\isachardoublequote}}, and \isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}ML{\isacharunderscore}struct\ s{\isacharbraceright}{\isachardoublequote}} check text \isa{s} as ML value, type, and
   293   structure, respectively.  The source is printed verbatim.
   294 
   295   \end{description}%
   296 \end{isamarkuptext}%
   297 \isamarkuptrue%
   298 %
   299 \isamarkupsubsubsection{Styled antiquotations%
   300 }
   301 \isamarkuptrue%
   302 %
   303 \begin{isamarkuptext}%
   304 Some antiquotations like \isa{thm{\isacharunderscore}style} and \isa{term{\isacharunderscore}style} admit an extra \emph{style} specification to modify the
   305   printed result.  The following standard styles are available:
   306 
   307   \begin{description}
   308   
   309   \item \isa{lhs} extracts the first argument of any application
   310   form with at least two arguments --- typically meta-level or
   311   object-level equality, or any other binary relation.
   312   
   313   \item \isa{rhs} is like \isa{lhs}, but extracts the second
   314   argument.
   315   
   316   \item \isa{{\isachardoublequote}concl{\isachardoublequote}} extracts the conclusion \isa{C} from a rule
   317   in Horn-clause normal form \isa{{\isachardoublequote}A\isactrlsub {\isadigit{1}}\ {\isasymLongrightarrow}\ {\isasymdots}\ A\isactrlsub n\ {\isasymLongrightarrow}\ C{\isachardoublequote}}.
   318   
   319   \item \isa{{\isachardoublequote}prem{\isadigit{1}}{\isachardoublequote}}, \dots, \isa{{\isachardoublequote}prem{\isadigit{9}}{\isachardoublequote}} extract premise number
   320   \isa{{\isachardoublequote}{\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isadigit{9}}{\isachardoublequote}}, respectively, from from a rule in Horn-clause
   321   normal form \isa{{\isachardoublequote}A\isactrlsub {\isadigit{1}}\ {\isasymLongrightarrow}\ {\isasymdots}\ A\isactrlsub n\ {\isasymLongrightarrow}\ C{\isachardoublequote}}
   322 
   323   \end{description}%
   324 \end{isamarkuptext}%
   325 \isamarkuptrue%
   326 %
   327 \isamarkupsubsubsection{General options%
   328 }
   329 \isamarkuptrue%
   330 %
   331 \begin{isamarkuptext}%
   332 The following options are available to tune the printed output
   333   of antiquotations.  Note that many of these coincide with global ML
   334   flags of the same names.
   335 
   336   \begin{description}
   337 
   338   \item \indexdef{}{antiquotation option}{show\_types}\hypertarget{antiquotation option.show-types}{\hyperlink{antiquotation option.show-types}{\mbox{\isa{show{\isacharunderscore}types}}}}~\isa{{\isachardoublequote}{\isacharequal}\ bool{\isachardoublequote}} and
   339   \indexdef{}{antiquotation option}{show\_sorts}\hypertarget{antiquotation option.show-sorts}{\hyperlink{antiquotation option.show-sorts}{\mbox{\isa{show{\isacharunderscore}sorts}}}}~\isa{{\isachardoublequote}{\isacharequal}\ bool{\isachardoublequote}} control
   340   printing of explicit type and sort constraints.
   341 
   342   \item \indexdef{}{antiquotation option}{show\_structs}\hypertarget{antiquotation option.show-structs}{\hyperlink{antiquotation option.show-structs}{\mbox{\isa{show{\isacharunderscore}structs}}}}~\isa{{\isachardoublequote}{\isacharequal}\ bool{\isachardoublequote}}
   343   controls printing of implicit structures.
   344 
   345   \item \indexdef{}{antiquotation option}{long\_names}\hypertarget{antiquotation option.long-names}{\hyperlink{antiquotation option.long-names}{\mbox{\isa{long{\isacharunderscore}names}}}}~\isa{{\isachardoublequote}{\isacharequal}\ bool{\isachardoublequote}} forces
   346   names of types and constants etc.\ to be printed in their fully
   347   qualified internal form.
   348 
   349   \item \indexdef{}{antiquotation option}{short\_names}\hypertarget{antiquotation option.short-names}{\hyperlink{antiquotation option.short-names}{\mbox{\isa{short{\isacharunderscore}names}}}}~\isa{{\isachardoublequote}{\isacharequal}\ bool{\isachardoublequote}}
   350   forces names of types and constants etc.\ to be printed unqualified.
   351   Note that internalizing the output again in the current context may
   352   well yield a different result.
   353 
   354   \item \indexdef{}{antiquotation option}{unique\_names}\hypertarget{antiquotation option.unique-names}{\hyperlink{antiquotation option.unique-names}{\mbox{\isa{unique{\isacharunderscore}names}}}}~\isa{{\isachardoublequote}{\isacharequal}\ bool{\isachardoublequote}}
   355   determines whether the printed version of qualified names should be
   356   made sufficiently long to avoid overlap with names declared further
   357   back.  Set to \isa{false} for more concise output.
   358 
   359   \item \indexdef{}{antiquotation option}{eta\_contract}\hypertarget{antiquotation option.eta-contract}{\hyperlink{antiquotation option.eta-contract}{\mbox{\isa{eta{\isacharunderscore}contract}}}}~\isa{{\isachardoublequote}{\isacharequal}\ bool{\isachardoublequote}}
   360   prints terms in \isa{{\isasymeta}}-contracted form.
   361 
   362   \item \indexdef{}{antiquotation option}{display}\hypertarget{antiquotation option.display}{\hyperlink{antiquotation option.display}{\mbox{\isa{display}}}}~\isa{{\isachardoublequote}{\isacharequal}\ bool{\isachardoublequote}} indicates
   363   if the text is to be output as multi-line ``display material'',
   364   rather than a small piece of text without line breaks (which is the
   365   default).
   366 
   367   In this mode the embedded entities are printed in the same style as
   368   the main theory text.
   369 
   370   \item \indexdef{}{antiquotation option}{break}\hypertarget{antiquotation option.break}{\hyperlink{antiquotation option.break}{\mbox{\isa{break}}}}~\isa{{\isachardoublequote}{\isacharequal}\ bool{\isachardoublequote}} controls
   371   line breaks in non-display material.
   372 
   373   \item \indexdef{}{antiquotation option}{quotes}\hypertarget{antiquotation option.quotes}{\hyperlink{antiquotation option.quotes}{\mbox{\isa{quotes}}}}~\isa{{\isachardoublequote}{\isacharequal}\ bool{\isachardoublequote}} indicates
   374   if the output should be enclosed in double quotes.
   375 
   376   \item \indexdef{}{antiquotation option}{mode}\hypertarget{antiquotation option.mode}{\hyperlink{antiquotation option.mode}{\mbox{\isa{mode}}}}~\isa{{\isachardoublequote}{\isacharequal}\ name{\isachardoublequote}} adds \isa{name} to the print mode to be used for presentation.  Note that the
   377   standard setup for {\LaTeX} output is already present by default,
   378   including the modes \isa{latex} and \isa{xsymbols}.
   379 
   380   \item \indexdef{}{antiquotation option}{margin}\hypertarget{antiquotation option.margin}{\hyperlink{antiquotation option.margin}{\mbox{\isa{margin}}}}~\isa{{\isachardoublequote}{\isacharequal}\ nat{\isachardoublequote}} and
   381   \indexdef{}{antiquotation option}{indent}\hypertarget{antiquotation option.indent}{\hyperlink{antiquotation option.indent}{\mbox{\isa{indent}}}}~\isa{{\isachardoublequote}{\isacharequal}\ nat{\isachardoublequote}} change the margin
   382   or indentation for pretty printing of display material.
   383 
   384   \item \indexdef{}{antiquotation option}{goals\_limit}\hypertarget{antiquotation option.goals-limit}{\hyperlink{antiquotation option.goals-limit}{\mbox{\isa{goals{\isacharunderscore}limit}}}}~\isa{{\isachardoublequote}{\isacharequal}\ nat{\isachardoublequote}}
   385   determines the maximum number of goals to be printed (for goal-based
   386   antiquotation).
   387 
   388   \item \indexdef{}{antiquotation option}{source}\hypertarget{antiquotation option.source}{\hyperlink{antiquotation option.source}{\mbox{\isa{source}}}}~\isa{{\isachardoublequote}{\isacharequal}\ bool{\isachardoublequote}} prints the
   389   original source text of the antiquotation arguments, rather than its
   390   internal representation.  Note that formal checking of
   391   \hyperlink{antiquotation.thm}{\mbox{\isa{thm}}}, \hyperlink{antiquotation.term}{\mbox{\isa{term}}}, etc. is still
   392   enabled; use the \hyperlink{antiquotation.text}{\mbox{\isa{text}}} antiquotation for unchecked
   393   output.
   394 
   395   Regular \isa{{\isachardoublequote}term{\isachardoublequote}} and \isa{{\isachardoublequote}typ{\isachardoublequote}} antiquotations with \isa{{\isachardoublequote}source\ {\isacharequal}\ false{\isachardoublequote}} involve a full round-trip from the original source
   396   to an internalized logical entity back to a source form, according
   397   to the syntax of the current context.  Thus the printed output is
   398   not under direct control of the author, it may even fluctuate a bit
   399   as the underlying theory is changed later on.
   400 
   401   In contrast, \indexdef{}{antiquotation option}{source}\hypertarget{antiquotation option.source}{\hyperlink{antiquotation option.source}{\mbox{\isa{source}}}}~\isa{{\isachardoublequote}{\isacharequal}\ true{\isachardoublequote}}
   402   admits direct printing of the given source text, with the desirable
   403   well-formedness check in the background, but without modification of
   404   the printed text.
   405 
   406   \end{description}
   407 
   408   For boolean flags, ``\isa{{\isachardoublequote}name\ {\isacharequal}\ true{\isachardoublequote}}'' may be abbreviated as
   409   ``\isa{name}''.  All of the above flags are disabled by default,
   410   unless changed from ML, say in the \verb|ROOT.ML| of the
   411   logic session.%
   412 \end{isamarkuptext}%
   413 \isamarkuptrue%
   414 %
   415 \isamarkupsection{Markup via command tags \label{sec:tags}%
   416 }
   417 \isamarkuptrue%
   418 %
   419 \begin{isamarkuptext}%
   420 Each Isabelle/Isar command may be decorated by additional
   421   presentation tags, to indicate some modification in the way it is
   422   printed in the document.
   423 
   424   \indexouternonterm{tags}
   425   \begin{rail}
   426     tags: ( tag * )
   427     ;
   428     tag: '\%' (ident | string)
   429   \end{rail}
   430 
   431   Some tags are pre-declared for certain classes of commands, serving
   432   as default markup if no tags are given in the text:
   433 
   434   \medskip
   435   \begin{tabular}{ll}
   436     \isa{{\isachardoublequote}theory{\isachardoublequote}} & theory begin/end \\
   437     \isa{{\isachardoublequote}proof{\isachardoublequote}} & all proof commands \\
   438     \isa{{\isachardoublequote}ML{\isachardoublequote}} & all commands involving ML code \\
   439   \end{tabular}
   440 
   441   \medskip The Isabelle document preparation system
   442   \cite{isabelle-sys} allows tagged command regions to be presented
   443   specifically, e.g.\ to fold proof texts, or drop parts of the text
   444   completely.
   445 
   446   For example ``\hyperlink{command.by}{\mbox{\isa{\isacommand{by}}}}~\isa{{\isachardoublequote}{\isacharpercent}invisible\ auto{\isachardoublequote}}'' causes
   447   that piece of proof to be treated as \isa{invisible} instead of
   448   \isa{{\isachardoublequote}proof{\isachardoublequote}} (the default), which may be shown or hidden
   449   depending on the document setup.  In contrast, ``\hyperlink{command.by}{\mbox{\isa{\isacommand{by}}}}~\isa{{\isachardoublequote}{\isacharpercent}visible\ auto{\isachardoublequote}}'' forces this text to be shown
   450   invariably.
   451 
   452   Explicit tag specifications within a proof apply to all subsequent
   453   commands of the same level of nesting.  For example, ``\hyperlink{command.proof}{\mbox{\isa{\isacommand{proof}}}}~\isa{{\isachardoublequote}{\isacharpercent}visible\ {\isasymdots}{\isachardoublequote}}~\hyperlink{command.qed}{\mbox{\isa{\isacommand{qed}}}}'' forces the whole
   454   sub-proof to be typeset as \isa{visible} (unless some of its parts
   455   are tagged differently).
   456 
   457   \medskip Command tags merely produce certain markup environments for
   458   type-setting.  The meaning of these is determined by {\LaTeX}
   459   macros, as defined in \hyperlink{file.~~/lib/texinputs/isabelle.sty}{\mbox{\isa{\isatt{{\isachartilde}{\isachartilde}{\isacharslash}lib{\isacharslash}texinputs{\isacharslash}isabelle{\isachardot}sty}}}} or
   460   by the document author.  The Isabelle document preparation tools
   461   also provide some high-level options to specify the meaning of
   462   arbitrary tags to ``keep'', ``drop'', or ``fold'' the corresponding
   463   parts of the text.  Logic sessions may also specify ``document
   464   versions'', where given tags are interpreted in some particular way.
   465   Again see \cite{isabelle-sys} for further details.%
   466 \end{isamarkuptext}%
   467 \isamarkuptrue%
   468 %
   469 \isamarkupsection{Draft presentation%
   470 }
   471 \isamarkuptrue%
   472 %
   473 \begin{isamarkuptext}%
   474 \begin{matharray}{rcl}
   475     \indexdef{}{command}{display\_drafts}\hypertarget{command.display-drafts}{\hyperlink{command.display-drafts}{\mbox{\isa{\isacommand{display{\isacharunderscore}drafts}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}any\ {\isasymrightarrow}{\isachardoublequote}} \\
   476     \indexdef{}{command}{print\_drafts}\hypertarget{command.print-drafts}{\hyperlink{command.print-drafts}{\mbox{\isa{\isacommand{print{\isacharunderscore}drafts}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}any\ {\isasymrightarrow}{\isachardoublequote}} \\
   477   \end{matharray}
   478 
   479   \begin{rail}
   480     ('display\_drafts' | 'print\_drafts') (name +)
   481     ;
   482   \end{rail}
   483 
   484   \begin{description}
   485 
   486   \item \hyperlink{command.display-drafts}{\mbox{\isa{\isacommand{display{\isacharunderscore}drafts}}}}~\isa{paths} and \hyperlink{command.print-drafts}{\mbox{\isa{\isacommand{print{\isacharunderscore}drafts}}}}~\isa{paths} perform simple output of a given list
   487   of raw source files.  Only those symbols that do not require
   488   additional {\LaTeX} packages are displayed properly, everything else
   489   is left verbatim.
   490 
   491   \end{description}%
   492 \end{isamarkuptext}%
   493 \isamarkuptrue%
   494 %
   495 \isadelimtheory
   496 %
   497 \endisadelimtheory
   498 %
   499 \isatagtheory
   500 \isacommand{end}\isamarkupfalse%
   501 %
   502 \endisatagtheory
   503 {\isafoldtheory}%
   504 %
   505 \isadelimtheory
   506 %
   507 \endisadelimtheory
   508 \isanewline
   509 \end{isabellebody}%
   510 %%% Local Variables:
   511 %%% mode: latex
   512 %%% TeX-master: "root"
   513 %%% End: