doc-src/IsarRef/Thy/document/Document_Preparation.tex
author wenzelm
Fri Sep 24 16:17:59 2010 +0200 (2010-09-24)
changeset 39689 78b185bf7660
parent 39437 8c23c61c6d5c
child 40255 9ffbc25e1606
permissions -rw-r--r--
clarified @{type} antiquotation: abbreviations and nonterminals count as "syntactic", disallow TFrees;
tuned;
     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}{term\_type}\hypertarget{antiquotation.term-type}{\hyperlink{antiquotation.term-type}{\mbox{\isa{term{\isacharunderscore}type}}}} & : & \isa{antiquotation} \\
   163     \indexdef{}{antiquotation}{typeof}\hypertarget{antiquotation.typeof}{\hyperlink{antiquotation.typeof}{\mbox{\isa{typeof}}}} & : & \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}{typ}\hypertarget{antiquotation.typ}{\hyperlink{antiquotation.typ}{\mbox{\isa{typ}}}} & : & \isa{antiquotation} \\
   167     \indexdef{}{antiquotation}{type}\hypertarget{antiquotation.type}{\hyperlink{antiquotation.type}{\mbox{\isa{type}}}} & : & \isa{antiquotation} \\
   168     \indexdef{}{antiquotation}{class}\hypertarget{antiquotation.class}{\hyperlink{antiquotation.class}{\mbox{\isa{class}}}} & : & \isa{antiquotation} \\
   169     \indexdef{}{antiquotation}{text}\hypertarget{antiquotation.text}{\hyperlink{antiquotation.text}{\mbox{\isa{text}}}} & : & \isa{antiquotation} \\
   170     \indexdef{}{antiquotation}{goals}\hypertarget{antiquotation.goals}{\hyperlink{antiquotation.goals}{\mbox{\isa{goals}}}} & : & \isa{antiquotation} \\
   171     \indexdef{}{antiquotation}{subgoals}\hypertarget{antiquotation.subgoals}{\hyperlink{antiquotation.subgoals}{\mbox{\isa{subgoals}}}} & : & \isa{antiquotation} \\
   172     \indexdef{}{antiquotation}{prf}\hypertarget{antiquotation.prf}{\hyperlink{antiquotation.prf}{\mbox{\isa{prf}}}} & : & \isa{antiquotation} \\
   173     \indexdef{}{antiquotation}{full\_prf}\hypertarget{antiquotation.full-prf}{\hyperlink{antiquotation.full-prf}{\mbox{\isa{full{\isacharunderscore}prf}}}} & : & \isa{antiquotation} \\
   174     \indexdef{}{antiquotation}{ML}\hypertarget{antiquotation.ML}{\hyperlink{antiquotation.ML}{\mbox{\isa{ML}}}} & : & \isa{antiquotation} \\
   175     \indexdef{}{antiquotation}{ML\_type}\hypertarget{antiquotation.ML-type}{\hyperlink{antiquotation.ML-type}{\mbox{\isa{ML{\isacharunderscore}type}}}} & : & \isa{antiquotation} \\
   176     \indexdef{}{antiquotation}{ML\_struct}\hypertarget{antiquotation.ML-struct}{\hyperlink{antiquotation.ML-struct}{\mbox{\isa{ML{\isacharunderscore}struct}}}} & : & \isa{antiquotation} \\
   177   \end{matharray}
   178 
   179   The overall content of an Isabelle/Isar theory may alternate between
   180   formal and informal text.  The main body consists of formal
   181   specification and proof commands, interspersed with markup commands
   182   (\secref{sec:markup}) or document comments (\secref{sec:comments}).
   183   The argument of markup commands quotes informal text to be printed
   184   in the resulting document, but may again refer to formal entities
   185   via \emph{document antiquotations}.
   186 
   187   For example, embedding of ``\isa{{\isacharat}{\isacharbraceleft}term\ {\isacharbrackleft}show{\isacharunderscore}types{\isacharbrackright}\ {\isachardoublequote}f\ x\ {\isacharequal}\ a\ {\isacharplus}\ x{\isachardoublequote}{\isacharbraceright}}''
   188   within a text block makes
   189   \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.
   190 
   191   Antiquotations usually spare the author tedious typing of logical
   192   entities in full detail.  Even more importantly, some degree of
   193   consistency-checking between the main body of formal text and its
   194   informal explanation is achieved, since terms and types appearing in
   195   antiquotations are checked within the current theory or proof
   196   context.
   197 
   198   \begin{rail}
   199     atsign lbrace antiquotation rbrace
   200     ;
   201 
   202     antiquotation:
   203       'theory' options name |
   204       'thm' options styles thmrefs |
   205       'lemma' options prop 'by' method |
   206       'prop' options styles prop |
   207       'term' options styles term |
   208       'term_type' options styles term |
   209       'typeof' options styles term |
   210       'const' options term |
   211       'abbrev' options term |
   212       'typ' options type |
   213       'type' options name |
   214       'class' options name |
   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     styles: '(' (style + ',') ')'
   229     ;
   230     style: (name +)
   231     ;
   232   \end{rail}
   233 
   234   Note that the syntax of antiquotations may \emph{not} include source
   235   comments \verb|(*|~\isa{{\isachardoublequote}{\isasymdots}{\isachardoublequote}}~\verb|*)| nor verbatim
   236   text \verb|{|\verb|*|~\isa{{\isachardoublequote}{\isasymdots}{\isachardoublequote}}~\verb|*|\verb|}|.
   237 
   238   \begin{description}
   239   
   240   \item \isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}theory\ A{\isacharbraceright}{\isachardoublequote}} prints the name \isa{{\isachardoublequote}A{\isachardoublequote}}, which is
   241   guaranteed to refer to a valid ancestor theory in the current
   242   context.
   243 
   244   \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}}.
   245   Full fact expressions are allowed here, including attributes
   246   (\secref{sec:syn-att}).
   247 
   248   \item \isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}prop\ {\isasymphi}{\isacharbraceright}{\isachardoublequote}} prints a well-typed proposition \isa{{\isachardoublequote}{\isasymphi}{\isachardoublequote}}.
   249 
   250   \item \isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}lemma\ {\isasymphi}\ by\ m{\isacharbraceright}{\isachardoublequote}} proves a well-typed proposition
   251   \isa{{\isachardoublequote}{\isasymphi}{\isachardoublequote}} by method \isa{m} and prints the original \isa{{\isachardoublequote}{\isasymphi}{\isachardoublequote}}.
   252 
   253   \item \isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}term\ t{\isacharbraceright}{\isachardoublequote}} prints a well-typed term \isa{{\isachardoublequote}t{\isachardoublequote}}.
   254 
   255   \item \isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}term{\isacharunderscore}type\ t{\isacharbraceright}{\isachardoublequote}} prints a well-typed term \isa{{\isachardoublequote}t{\isachardoublequote}}
   256   annotated with its type.
   257 
   258   \item \isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}typeof\ t{\isacharbraceright}{\isachardoublequote}} prints the type of a well-typed term
   259   \isa{{\isachardoublequote}t{\isachardoublequote}}.
   260 
   261   \item \isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}const\ c{\isacharbraceright}{\isachardoublequote}} prints a logical or syntactic constant
   262   \isa{{\isachardoublequote}c{\isachardoublequote}}.
   263   
   264   \item \isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}abbrev\ c\ x\isactrlsub {\isadigit{1}}\ {\isasymdots}\ x\isactrlsub n{\isacharbraceright}{\isachardoublequote}} prints a constant abbreviation
   265   \isa{{\isachardoublequote}c\ x\isactrlsub {\isadigit{1}}\ {\isasymdots}\ x\isactrlsub n\ {\isasymequiv}\ rhs{\isachardoublequote}} as defined in the current context.
   266 
   267   \item \isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}typ\ {\isasymtau}{\isacharbraceright}{\isachardoublequote}} prints a well-formed type \isa{{\isachardoublequote}{\isasymtau}{\isachardoublequote}}.
   268 
   269   \item \isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}type\ {\isasymkappa}{\isacharbraceright}{\isachardoublequote}} prints a (logical or syntactic) type
   270     constructor \isa{{\isachardoublequote}{\isasymkappa}{\isachardoublequote}}.
   271 
   272   \item \isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}class\ c{\isacharbraceright}{\isachardoublequote}} prints a class \isa{c}.
   273 
   274   \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
   275   to the Isabelle document style, without demanding well-formedness,
   276   e.g.\ small pieces of terms that should not be parsed or
   277   type-checked yet.
   278 
   279   \item \isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}goals{\isacharbraceright}{\isachardoublequote}} prints the current \emph{dynamic} goal
   280   state.  This is mainly for support of tactic-emulation scripts
   281   within Isar.  Presentation of goal states does not conform to the
   282   idea of human-readable proof documents!
   283 
   284   When explaining proofs in detail it is usually better to spell out
   285   the reasoning via proper Isar proof commands, instead of peeking at
   286   the internal machine configuration.
   287   
   288   \item \isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}subgoals{\isacharbraceright}{\isachardoublequote}} is similar to \isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}goals{\isacharbraceright}{\isachardoublequote}}, but
   289   does not print the main goal.
   290   
   291   \item \isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}prf\ a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n{\isacharbraceright}{\isachardoublequote}} prints the (compact) proof terms
   292   corresponding to the theorems \isa{{\isachardoublequote}a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n{\isachardoublequote}}. Note that this
   293   requires proof terms to be switched on for the current logic
   294   session.
   295   
   296   \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
   297   information omitted in the compact proof term, which is denoted by
   298   ``\isa{{\isacharunderscore}}'' placeholders there.
   299   
   300   \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
   301   structure, respectively.  The source is printed verbatim.
   302 
   303   \end{description}%
   304 \end{isamarkuptext}%
   305 \isamarkuptrue%
   306 %
   307 \isamarkupsubsubsection{Styled antiquotations%
   308 }
   309 \isamarkuptrue%
   310 %
   311 \begin{isamarkuptext}%
   312 The antiquotations \isa{thm}, \isa{prop} and \isa{term} admit an extra \emph{style} specification to modify the
   313   printed result.  A style is specified by a name with a possibly
   314   empty number of arguments;  multiple styles can be sequenced with
   315   commas.  The following standard styles are available:
   316 
   317   \begin{description}
   318   
   319   \item \isa{lhs} extracts the first argument of any application
   320   form with at least two arguments --- typically meta-level or
   321   object-level equality, or any other binary relation.
   322   
   323   \item \isa{rhs} is like \isa{lhs}, but extracts the second
   324   argument.
   325   
   326   \item \isa{{\isachardoublequote}concl{\isachardoublequote}} extracts the conclusion \isa{C} from a rule
   327   in Horn-clause normal form \isa{{\isachardoublequote}A\isactrlsub {\isadigit{1}}\ {\isasymLongrightarrow}\ {\isasymdots}\ A\isactrlsub n\ {\isasymLongrightarrow}\ C{\isachardoublequote}}.
   328   
   329   \item \isa{{\isachardoublequote}prem{\isachardoublequote}} \isa{n} extract premise number
   330   \isa{{\isachardoublequote}n{\isachardoublequote}} from from a rule in Horn-clause
   331   normal form \isa{{\isachardoublequote}A\isactrlsub {\isadigit{1}}\ {\isasymLongrightarrow}\ {\isasymdots}\ A\isactrlsub n\ {\isasymLongrightarrow}\ C{\isachardoublequote}}
   332 
   333   \end{description}%
   334 \end{isamarkuptext}%
   335 \isamarkuptrue%
   336 %
   337 \isamarkupsubsubsection{General options%
   338 }
   339 \isamarkuptrue%
   340 %
   341 \begin{isamarkuptext}%
   342 The following options are available to tune the printed output
   343   of antiquotations.  Note that many of these coincide with global ML
   344   flags of the same names.
   345 
   346   \begin{description}
   347 
   348   \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
   349   \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
   350   printing of explicit type and sort constraints.
   351 
   352   \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}}
   353   controls printing of implicit structures.
   354 
   355   \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
   356   names of types and constants etc.\ to be printed in their fully
   357   qualified internal form.
   358 
   359   \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}}
   360   forces names of types and constants etc.\ to be printed unqualified.
   361   Note that internalizing the output again in the current context may
   362   well yield a different result.
   363 
   364   \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}}
   365   determines whether the printed version of qualified names should be
   366   made sufficiently long to avoid overlap with names declared further
   367   back.  Set to \isa{false} for more concise output.
   368 
   369   \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}}
   370   prints terms in \isa{{\isasymeta}}-contracted form.
   371 
   372   \item \indexdef{}{antiquotation option}{display}\hypertarget{antiquotation option.display}{\hyperlink{antiquotation option.display}{\mbox{\isa{display}}}}~\isa{{\isachardoublequote}{\isacharequal}\ bool{\isachardoublequote}} indicates
   373   if the text is to be output as multi-line ``display material'',
   374   rather than a small piece of text without line breaks (which is the
   375   default).
   376 
   377   In this mode the embedded entities are printed in the same style as
   378   the main theory text.
   379 
   380   \item \indexdef{}{antiquotation option}{break}\hypertarget{antiquotation option.break}{\hyperlink{antiquotation option.break}{\mbox{\isa{break}}}}~\isa{{\isachardoublequote}{\isacharequal}\ bool{\isachardoublequote}} controls
   381   line breaks in non-display material.
   382 
   383   \item \indexdef{}{antiquotation option}{quotes}\hypertarget{antiquotation option.quotes}{\hyperlink{antiquotation option.quotes}{\mbox{\isa{quotes}}}}~\isa{{\isachardoublequote}{\isacharequal}\ bool{\isachardoublequote}} indicates
   384   if the output should be enclosed in double quotes.
   385 
   386   \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
   387   standard setup for {\LaTeX} output is already present by default,
   388   including the modes \isa{latex} and \isa{xsymbols}.
   389 
   390   \item \indexdef{}{antiquotation option}{margin}\hypertarget{antiquotation option.margin}{\hyperlink{antiquotation option.margin}{\mbox{\isa{margin}}}}~\isa{{\isachardoublequote}{\isacharequal}\ nat{\isachardoublequote}} and
   391   \indexdef{}{antiquotation option}{indent}\hypertarget{antiquotation option.indent}{\hyperlink{antiquotation option.indent}{\mbox{\isa{indent}}}}~\isa{{\isachardoublequote}{\isacharequal}\ nat{\isachardoublequote}} change the margin
   392   or indentation for pretty printing of display material.
   393 
   394   \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}}
   395   determines the maximum number of goals to be printed (for goal-based
   396   antiquotation).
   397 
   398   \item \indexdef{}{antiquotation option}{source}\hypertarget{antiquotation option.source}{\hyperlink{antiquotation option.source}{\mbox{\isa{source}}}}~\isa{{\isachardoublequote}{\isacharequal}\ bool{\isachardoublequote}} prints the
   399   original source text of the antiquotation arguments, rather than its
   400   internal representation.  Note that formal checking of
   401   \hyperlink{antiquotation.thm}{\mbox{\isa{thm}}}, \hyperlink{antiquotation.term}{\mbox{\isa{term}}}, etc. is still
   402   enabled; use the \hyperlink{antiquotation.text}{\mbox{\isa{text}}} antiquotation for unchecked
   403   output.
   404 
   405   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
   406   to an internalized logical entity back to a source form, according
   407   to the syntax of the current context.  Thus the printed output is
   408   not under direct control of the author, it may even fluctuate a bit
   409   as the underlying theory is changed later on.
   410 
   411   In contrast, \indexdef{}{antiquotation option}{source}\hypertarget{antiquotation option.source}{\hyperlink{antiquotation option.source}{\mbox{\isa{source}}}}~\isa{{\isachardoublequote}{\isacharequal}\ true{\isachardoublequote}}
   412   admits direct printing of the given source text, with the desirable
   413   well-formedness check in the background, but without modification of
   414   the printed text.
   415 
   416   \end{description}
   417 
   418   For boolean flags, ``\isa{{\isachardoublequote}name\ {\isacharequal}\ true{\isachardoublequote}}'' may be abbreviated as
   419   ``\isa{name}''.  All of the above flags are disabled by default,
   420   unless changed from ML, say in the \verb|ROOT.ML| of the
   421   logic session.%
   422 \end{isamarkuptext}%
   423 \isamarkuptrue%
   424 %
   425 \isamarkupsection{Markup via command tags \label{sec:tags}%
   426 }
   427 \isamarkuptrue%
   428 %
   429 \begin{isamarkuptext}%
   430 Each Isabelle/Isar command may be decorated by additional
   431   presentation tags, to indicate some modification in the way it is
   432   printed in the document.
   433 
   434   \indexouternonterm{tags}
   435   \begin{rail}
   436     tags: ( tag * )
   437     ;
   438     tag: '\%' (ident | string)
   439   \end{rail}
   440 
   441   Some tags are pre-declared for certain classes of commands, serving
   442   as default markup if no tags are given in the text:
   443 
   444   \medskip
   445   \begin{tabular}{ll}
   446     \isa{{\isachardoublequote}theory{\isachardoublequote}} & theory begin/end \\
   447     \isa{{\isachardoublequote}proof{\isachardoublequote}} & all proof commands \\
   448     \isa{{\isachardoublequote}ML{\isachardoublequote}} & all commands involving ML code \\
   449   \end{tabular}
   450 
   451   \medskip The Isabelle document preparation system
   452   \cite{isabelle-sys} allows tagged command regions to be presented
   453   specifically, e.g.\ to fold proof texts, or drop parts of the text
   454   completely.
   455 
   456   For example ``\hyperlink{command.by}{\mbox{\isa{\isacommand{by}}}}~\isa{{\isachardoublequote}{\isacharpercent}invisible\ auto{\isachardoublequote}}'' causes
   457   that piece of proof to be treated as \isa{invisible} instead of
   458   \isa{{\isachardoublequote}proof{\isachardoublequote}} (the default), which may be shown or hidden
   459   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
   460   invariably.
   461 
   462   Explicit tag specifications within a proof apply to all subsequent
   463   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
   464   sub-proof to be typeset as \isa{visible} (unless some of its parts
   465   are tagged differently).
   466 
   467   \medskip Command tags merely produce certain markup environments for
   468   type-setting.  The meaning of these is determined by {\LaTeX}
   469   macros, as defined in \hyperlink{file.~~/lib/texinputs/isabelle.sty}{\mbox{\isa{\isatt{{\isachartilde}{\isachartilde}{\isacharslash}lib{\isacharslash}texinputs{\isacharslash}isabelle{\isachardot}sty}}}} or
   470   by the document author.  The Isabelle document preparation tools
   471   also provide some high-level options to specify the meaning of
   472   arbitrary tags to ``keep'', ``drop'', or ``fold'' the corresponding
   473   parts of the text.  Logic sessions may also specify ``document
   474   versions'', where given tags are interpreted in some particular way.
   475   Again see \cite{isabelle-sys} for further details.%
   476 \end{isamarkuptext}%
   477 \isamarkuptrue%
   478 %
   479 \isamarkupsection{Draft presentation%
   480 }
   481 \isamarkuptrue%
   482 %
   483 \begin{isamarkuptext}%
   484 \begin{matharray}{rcl}
   485     \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}} \\
   486     \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}} \\
   487   \end{matharray}
   488 
   489   \begin{rail}
   490     ('display\_drafts' | 'print\_drafts') (name +)
   491     ;
   492   \end{rail}
   493 
   494   \begin{description}
   495 
   496   \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
   497   of raw source files.  Only those symbols that do not require
   498   additional {\LaTeX} packages are displayed properly, everything else
   499   is left verbatim.
   500 
   501   \end{description}%
   502 \end{isamarkuptext}%
   503 \isamarkuptrue%
   504 %
   505 \isadelimtheory
   506 %
   507 \endisadelimtheory
   508 %
   509 \isatagtheory
   510 \isacommand{end}\isamarkupfalse%
   511 %
   512 \endisatagtheory
   513 {\isafoldtheory}%
   514 %
   515 \isadelimtheory
   516 %
   517 \endisadelimtheory
   518 \isanewline
   519 \end{isabellebody}%
   520 %%% Local Variables:
   521 %%% mode: latex
   522 %%% TeX-master: "root"
   523 %%% End: