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