wenzelm@11648: % wenzelm@11648: \begin{isabellebody}% wenzelm@11648: \def\isabellecontext{Documents}% wenzelm@11866: \isamarkupfalse% wenzelm@12627: % wenzelm@12647: \isamarkupsection{Concrete Syntax \label{sec:concrete-syntax}% wenzelm@12627: } wenzelm@12627: \isamarkuptrue% wenzelm@12627: % wenzelm@12627: \begin{isamarkuptext}% wenzelm@12767: The core concept of Isabelle's framework for concrete syntax is that wenzelm@12767: of \bfindex{mixfix annotations}. Associated with any kind of wenzelm@12767: constant declaration, mixfixes affect both the grammar productions wenzelm@12767: for the parser and output templates for the pretty printer. wenzelm@12627: wenzelm@12743: In full generality, parser and pretty printer configuration is a wenzelm@12767: subtle affair \cite{isabelle-ref}. Your syntax specifications need wenzelm@12767: to interact properly with the existing setup of Isabelle/Pure and wenzelm@12767: Isabelle/HOL\@. To avoid creating ambiguities with existing wenzelm@12767: elements, it is particularly important to give new syntactic paulson@12764: constructs the right precedence. wenzelm@12627: wenzelm@12671: \medskip Subsequently we introduce a few simple syntax declaration wenzelm@12743: forms that already cover many common situations fairly well.% wenzelm@12627: \end{isamarkuptext}% wenzelm@12627: \isamarkuptrue% wenzelm@12627: % wenzelm@12647: \isamarkupsubsection{Infix Annotations% wenzelm@12627: } wenzelm@12627: \isamarkuptrue% wenzelm@12627: % wenzelm@12627: \begin{isamarkuptext}% paulson@12764: Syntax annotations may be included wherever constants are declared, wenzelm@12767: such as \isacommand{consts} and \isacommand{constdefs} --- and also wenzelm@12767: \isacommand{datatype}, which declares constructor operations. wenzelm@12767: Type-constructors may be annotated as well, although this is less wenzelm@12767: frequently encountered in practice (the infix type \isa{{\isasymtimes}} comes wenzelm@12767: to mind). wenzelm@12627: wenzelm@12644: Infix declarations\index{infix annotations} provide a useful special wenzelm@12767: case of mixfixes. The following example of the exclusive-or wenzelm@12767: operation on boolean values illustrates typical infix declarations.% wenzelm@12627: \end{isamarkuptext}% wenzelm@12627: \isamarkuptrue% wenzelm@12627: \isacommand{constdefs}\isanewline wenzelm@12627: \ \ xor\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}bool\ {\isasymRightarrow}\ bool\ {\isasymRightarrow}\ bool{\isachardoublequote}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequote}{\isacharbrackleft}{\isacharplus}{\isacharbrackright}{\isachardoublequote}\ {\isadigit{6}}{\isadigit{0}}{\isacharparenright}\isanewline wenzelm@12627: \ \ {\isachardoublequote}A\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ B\ {\isasymequiv}\ {\isacharparenleft}A\ {\isasymand}\ {\isasymnot}\ B{\isacharparenright}\ {\isasymor}\ {\isacharparenleft}{\isasymnot}\ A\ {\isasymand}\ B{\isacharparenright}{\isachardoublequote}\isamarkupfalse% wenzelm@12627: % wenzelm@12627: \begin{isamarkuptext}% wenzelm@12652: \noindent Now \isa{xor\ A\ B} and \isa{A\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ B} refer to the wenzelm@12652: same expression internally. Any curried function with at least two wenzelm@12767: arguments may be given infix syntax. For partial applications with wenzelm@12767: fewer than two operands, there is a notation using the prefix~\isa{op}. For instance, \isa{xor} without arguments is represented as wenzelm@12767: \isa{op\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}}; together with ordinary function application, this wenzelm@12652: turns \isa{xor\ A} into \isa{op\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ A}. wenzelm@12627: wenzelm@12747: \medskip The keyword \isakeyword{infixl} seen above specifies an wenzelm@12747: infix operator that is nested to the \emph{left}: in iterated wenzelm@12747: applications the more complex expression appears on the left-hand wenzelm@12767: side, and \isa{A\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ B\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ C} stands for \isa{{\isacharparenleft}A\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ B{\isacharparenright}\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ C}. Similarly, \isakeyword{infixr} means nesting to the wenzelm@12767: \emph{right}, reading \isa{A\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ B\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ C} as \isa{A\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ {\isacharparenleft}B\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ C{\isacharparenright}}. A \emph{non-oriented} declaration via \isakeyword{infix} wenzelm@12767: would render \isa{A\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ B\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ C} illegal, but demand explicit wenzelm@12767: parentheses to indicate the intended grouping. wenzelm@12743: wenzelm@12747: The string \isa{{\isachardoublequote}{\isacharbrackleft}{\isacharplus}{\isacharbrackright}{\isachardoublequote}} in our annotation refers to the wenzelm@12747: concrete syntax to represent the operator (a literal token), while paulson@12764: the number \isa{{\isadigit{6}}{\isadigit{0}}} determines the precedence of the construct: wenzelm@12767: the syntactic priorities of the arguments and result. Isabelle/HOL wenzelm@12767: already uses up many popular combinations of ASCII symbols for its wenzelm@12767: own use, including both \isa{{\isacharplus}} and \isa{{\isacharplus}{\isacharplus}}. Longer wenzelm@12767: character combinations are more likely to be still available for wenzelm@12767: user extensions, such as our~\isa{{\isacharbrackleft}{\isacharplus}{\isacharbrackright}}. wenzelm@12627: wenzelm@12767: Operator precedences have a range of 0--1000. Very low or high wenzelm@12767: priorities are reserved for the meta-logic. HOL syntax mainly uses wenzelm@12767: the range of 10--100: the equality infix \isa{{\isacharequal}} is centered at wenzelm@12767: 50; logical connectives (like \isa{{\isasymor}} and \isa{{\isasymand}}) are wenzelm@12767: below 50; algebraic ones (like \isa{{\isacharplus}} and \isa{{\isacharasterisk}}) are wenzelm@12767: above 50. User syntax should strive to coexist with common HOL wenzelm@12767: forms, or use the mostly unused range 100--900.% wenzelm@12627: \end{isamarkuptext}% wenzelm@12627: \isamarkuptrue% wenzelm@12635: % wenzelm@12658: \isamarkupsubsection{Mathematical Symbols \label{sec:syntax-symbols}% wenzelm@12635: } wenzelm@12627: \isamarkuptrue% wenzelm@12635: % wenzelm@12635: \begin{isamarkuptext}% wenzelm@12767: Concrete syntax based on ASCII characters has inherent limitations. wenzelm@12767: Mathematical notation demands a larger repertoire of glyphs. wenzelm@12767: Several standards of extended character sets have been proposed over wenzelm@12767: decades, but none has become universally available so far. Isabelle wenzelm@12767: has its own notion of \bfindex{symbols} as the smallest entities of wenzelm@12767: source text, without referring to internal encodings. There are wenzelm@12767: three kinds of such ``generalized characters'': wenzelm@12635: wenzelm@12635: \begin{enumerate} wenzelm@12635: wenzelm@12652: \item 7-bit ASCII characters wenzelm@12635: wenzelm@12652: \item named symbols: \verb,\,\verb,<,$ident$\verb,>, wenzelm@12635: wenzelm@12652: \item named control symbols: \verb,\,\verb,<^,$ident$\verb,>, wenzelm@12635: wenzelm@12635: \end{enumerate} wenzelm@12635: wenzelm@12635: Here $ident$ may be any identifier according to the usual Isabelle wenzelm@12635: conventions. This results in an infinite store of symbols, whose wenzelm@12767: interpretation is left to further front-end tools. For example, the wenzelm@12767: user-interface of Proof~General + X-Symbol and the Isabelle document wenzelm@12767: processor (see \S\ref{sec:document-preparation}) display the wenzelm@12767: \verb,\,\verb,, symbol as~\isa{{\isasymforall}}. wenzelm@12635: wenzelm@12635: A list of standard Isabelle symbols is given in wenzelm@12767: \cite[appendix~A]{isabelle-sys}. You may introduce your own wenzelm@12635: interpretation of further symbols by configuring the appropriate wenzelm@12652: front-end tool accordingly, e.g.\ by defining certain {\LaTeX} wenzelm@12652: macros (see also \S\ref{sec:doc-prep-symbols}). There are also a wenzelm@12652: few predefined control symbols, such as \verb,\,\verb,<^sub>, and wenzelm@12635: \verb,\,\verb,<^sup>, for sub- and superscript of the subsequent paulson@12764: printable symbol, respectively. For example, \verb,A\<^sup>\, is wenzelm@12671: output as \isa{A\isactrlsup {\isasymstar}}. wenzelm@12635: wenzelm@12767: \medskip Replacing our definition of \isa{xor} by the following nipkow@13439: specifies an Isabelle symbol for the new operator:% wenzelm@12635: \end{isamarkuptext}% wenzelm@12627: \isamarkuptrue% wenzelm@12627: \isamarkupfalse% wenzelm@12627: \isamarkupfalse% wenzelm@12635: \isacommand{constdefs}\isanewline wenzelm@12635: \ \ xor\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}bool\ {\isasymRightarrow}\ bool\ {\isasymRightarrow}\ bool{\isachardoublequote}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequote}{\isasymoplus}{\isachardoublequote}\ {\isadigit{6}}{\isadigit{0}}{\isacharparenright}\isanewline nipkow@13791: \ \ {\isachardoublequote}A\ {\isasymoplus}\ B\ {\isasymequiv}\ {\isacharparenleft}A\ {\isasymand}\ {\isasymnot}\ B{\isacharparenright}\ {\isasymor}\ {\isacharparenleft}{\isasymnot}\ A\ {\isasymand}\ B{\isacharparenright}{\isachardoublequote}\isamarkupfalse% wenzelm@12627: \isamarkupfalse% wenzelm@12635: % wenzelm@12635: \begin{isamarkuptext}% wenzelm@12652: \noindent The X-Symbol package within Proof~General provides several wenzelm@12652: input methods to enter \isa{{\isasymoplus}} in the text. If all fails one may wenzelm@12767: just type a named entity \verb,\,\verb,, by hand; the wenzelm@12767: corresponding symbol will be displayed after further input. wenzelm@12635: wenzelm@12767: \medskip More flexible is to provide alternative syntax forms wenzelm@12767: through the \bfindex{print mode} concept~\cite{isabelle-ref}. By wenzelm@12767: convention, the mode of ``$xsymbols$'' is enabled whenever wenzelm@12767: Proof~General's X-Symbol mode or {\LaTeX} output is active. Now wenzelm@12767: consider the following hybrid declaration of \isa{xor}:% wenzelm@12635: \end{isamarkuptext}% wenzelm@12627: \isamarkuptrue% wenzelm@12627: \isamarkupfalse% wenzelm@12635: \isamarkupfalse% wenzelm@12635: \isacommand{constdefs}\isanewline wenzelm@12635: \ \ xor\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}bool\ {\isasymRightarrow}\ bool\ {\isasymRightarrow}\ bool{\isachardoublequote}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequote}{\isacharbrackleft}{\isacharplus}{\isacharbrackright}{\isasymignore}{\isachardoublequote}\ {\isadigit{6}}{\isadigit{0}}{\isacharparenright}\isanewline wenzelm@12635: \ \ {\isachardoublequote}A\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}{\isasymignore}\ B\ {\isasymequiv}\ {\isacharparenleft}A\ {\isasymand}\ {\isasymnot}\ B{\isacharparenright}\ {\isasymor}\ {\isacharparenleft}{\isasymnot}\ A\ {\isasymand}\ B{\isacharparenright}{\isachardoublequote}\isanewline wenzelm@12635: \isanewline wenzelm@12635: \isamarkupfalse% wenzelm@12635: \isacommand{syntax}\ {\isacharparenleft}xsymbols{\isacharparenright}\isanewline nipkow@13791: \ \ xor\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}bool\ {\isasymRightarrow}\ bool\ {\isasymRightarrow}\ bool{\isachardoublequote}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequote}{\isasymoplus}{\isasymignore}{\isachardoublequote}\ {\isadigit{6}}{\isadigit{0}}{\isacharparenright}\isamarkupfalse% wenzelm@12635: \isamarkupfalse% wenzelm@12635: % wenzelm@12635: \begin{isamarkuptext}% wenzelm@12652: The \commdx{syntax} command introduced here acts like wenzelm@12743: \isakeyword{consts}, but without declaring a logical constant. The wenzelm@12747: print mode specification of \isakeyword{syntax}, here \isa{{\isacharparenleft}xsymbols{\isacharparenright}}, is optional. Also note that its type merely serves wenzelm@12747: for syntactic purposes, and is \emph{not} checked for consistency wenzelm@12747: with the real constant. wenzelm@12635: wenzelm@12672: \medskip We may now write \isa{A\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ B} or \isa{A\ {\isasymoplus}\ B} in wenzelm@12767: input, while output uses the nicer syntax of $xsymbols$ whenever wenzelm@12672: that print mode is active. Such an arrangement is particularly wenzelm@12767: useful for interactive development, where users may type ASCII text wenzelm@12767: and see mathematical symbols displayed during proofs.% wenzelm@12635: \end{isamarkuptext}% wenzelm@12627: \isamarkuptrue% wenzelm@12635: % wenzelm@12647: \isamarkupsubsection{Prefix Annotations% wenzelm@12635: } wenzelm@12627: \isamarkuptrue% wenzelm@12635: % wenzelm@12635: \begin{isamarkuptext}% wenzelm@12767: Prefix syntax annotations\index{prefix annotation} are another form wenzelm@12767: of mixfixes \cite{isabelle-ref}, without any template arguments or wenzelm@12767: priorities --- just some literal syntax. The following example wenzelm@12767: associates common symbols with the constructors of a datatype.% wenzelm@12635: \end{isamarkuptext}% wenzelm@12627: \isamarkuptrue% wenzelm@12635: \isacommand{datatype}\ currency\ {\isacharequal}\isanewline wenzelm@12635: \ \ \ \ Euro\ nat\ \ \ \ {\isacharparenleft}{\isachardoublequote}{\isasymeuro}{\isachardoublequote}{\isacharparenright}\isanewline wenzelm@12635: \ \ {\isacharbar}\ Pounds\ nat\ \ {\isacharparenleft}{\isachardoublequote}{\isasympounds}{\isachardoublequote}{\isacharparenright}\isanewline wenzelm@12635: \ \ {\isacharbar}\ Yen\ nat\ \ \ \ \ {\isacharparenleft}{\isachardoublequote}{\isasymyen}{\isachardoublequote}{\isacharparenright}\isanewline wenzelm@12635: \ \ {\isacharbar}\ Dollar\ nat\ \ {\isacharparenleft}{\isachardoublequote}{\isachardollar}{\isachardoublequote}{\isacharparenright}\isamarkupfalse% wenzelm@12635: % wenzelm@12635: \begin{isamarkuptext}% wenzelm@12652: \noindent Here the mixfix annotations on the rightmost column happen wenzelm@12652: to consist of a single Isabelle symbol each: \verb,\,\verb,,, wenzelm@12652: \verb,\,\verb,,, \verb,\,\verb,,, and \verb,$,. Recall wenzelm@12747: that a constructor like \isa{Euro} actually is a function \isa{nat\ {\isasymRightarrow}\ currency}. The expression \isa{Euro\ {\isadigit{1}}{\isadigit{0}}} will be wenzelm@12652: printed as \isa{{\isasymeuro}\ {\isadigit{1}}{\isadigit{0}}}; only the head of the application is wenzelm@12743: subject to our concrete syntax. This rather simple form already wenzelm@12743: achieves conformance with notational standards of the European wenzelm@12743: Commission. wenzelm@12635: wenzelm@12767: Prefix syntax works the same way for \isakeyword{consts} or paulson@12764: \isakeyword{constdefs}.% wenzelm@12649: \end{isamarkuptext}% wenzelm@12649: \isamarkuptrue% wenzelm@12649: % wenzelm@12649: \isamarkupsubsection{Syntax Translations \label{sec:syntax-translations}% wenzelm@12635: } wenzelm@12627: \isamarkuptrue% wenzelm@12635: % wenzelm@12635: \begin{isamarkuptext}% wenzelm@12767: Mixfix syntax annotations merely decorate particular constant wenzelm@12767: application forms with concrete syntax, for instance replacing \ wenzelm@12767: \isa{xor\ A\ B} by \isa{A\ {\isasymoplus}\ B}. Occasionally, the wenzelm@12767: relationship between some piece of notation and its internal form is wenzelm@12767: more complicated. Here we need \bfindex{syntax translations}. wenzelm@12635: paulson@12764: Using the \isakeyword{syntax}\index{syntax (command)}, command we paulson@12764: introduce uninterpreted notational elements. Then paulson@12764: \commdx{translations} relate input forms to complex logical wenzelm@12767: expressions. This provides a simple mechanism for syntactic macros; wenzelm@12767: even heavier transformations may be written in ML wenzelm@12671: \cite{isabelle-ref}. wenzelm@12649: paulson@12764: \medskip A typical use of syntax translations is to introduce wenzelm@12767: relational notation for membership in a set of pair, replacing \ wenzelm@12767: \isa{{\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}\ {\isasymin}\ sim} by \isa{x\ {\isasymapprox}\ y}.% wenzelm@12635: \end{isamarkuptext}% wenzelm@12627: \isamarkuptrue% wenzelm@12649: \isacommand{consts}\isanewline wenzelm@12649: \ \ sim\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set{\isachardoublequote}\isanewline wenzelm@12649: \isanewline wenzelm@12649: \isamarkupfalse% wenzelm@12649: \isacommand{syntax}\isanewline wenzelm@12649: \ \ {\isachardoublequote}{\isacharunderscore}sim{\isachardoublequote}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ bool{\isachardoublequote}\ \ \ \ {\isacharparenleft}\isakeyword{infix}\ {\isachardoublequote}{\isasymapprox}{\isachardoublequote}\ {\isadigit{5}}{\isadigit{0}}{\isacharparenright}\isanewline wenzelm@12649: \isamarkupfalse% wenzelm@12649: \isacommand{translations}\isanewline wenzelm@12649: \ \ {\isachardoublequote}x\ {\isasymapprox}\ y{\isachardoublequote}\ {\isasymrightleftharpoons}\ {\isachardoublequote}{\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}\ {\isasymin}\ sim{\isachardoublequote}\isamarkupfalse% wenzelm@12635: % wenzelm@12635: \begin{isamarkuptext}% wenzelm@12649: \noindent Here the name of the dummy constant \isa{{\isacharunderscore}sim} does wenzelm@12767: not matter, as long as it is not used elsewhere. Prefixing an wenzelm@12767: underscore is a common convention. The \isakeyword{translations} wenzelm@12649: declaration already uses concrete syntax on the left-hand side; wenzelm@12649: internally we relate a raw application \isa{{\isacharunderscore}sim\ x\ y} with wenzelm@12649: \isa{{\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}\ {\isasymin}\ sim}. wenzelm@12635: wenzelm@12652: \medskip Another common application of syntax translations is to wenzelm@12649: provide variant versions of fundamental relational expressions, such wenzelm@12649: as \isa{{\isasymnoteq}} for negated equalities. The following declaration wenzelm@12649: stems from Isabelle/HOL itself:% wenzelm@12649: \end{isamarkuptext}% wenzelm@12649: \isamarkuptrue% wenzelm@12649: \isacommand{syntax}\ {\isachardoublequote}{\isacharunderscore}not{\isacharunderscore}equal{\isachardoublequote}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ bool{\isachardoublequote}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequote}{\isasymnoteq}{\isasymignore}{\isachardoublequote}\ {\isadigit{5}}{\isadigit{0}}{\isacharparenright}\isanewline wenzelm@12649: \isamarkupfalse% wenzelm@12649: \isacommand{translations}\ {\isachardoublequote}x\ {\isasymnoteq}{\isasymignore}\ y{\isachardoublequote}\ {\isasymrightleftharpoons}\ {\isachardoublequote}{\isasymnot}\ {\isacharparenleft}x\ {\isacharequal}\ y{\isacharparenright}{\isachardoublequote}\isamarkupfalse% wenzelm@12649: % wenzelm@12649: \begin{isamarkuptext}% wenzelm@12649: \noindent Normally one would introduce derived concepts like this wenzelm@12652: within the logic, using \isakeyword{consts} + \isakeyword{defs} wenzelm@12652: instead of \isakeyword{syntax} + \isakeyword{translations}. The wenzelm@12649: present formulation has the virtue that expressions are immediately wenzelm@12666: replaced by the ``definition'' upon parsing; the effect is reversed wenzelm@12666: upon printing. wenzelm@12649: wenzelm@12767: This sort of translation is appropriate when the defined concept is wenzelm@12767: a trivial variation on an existing one. On the other hand, syntax wenzelm@12767: translations do not scale up well to large hierarchies of concepts. wenzelm@12767: Translations do not replace definitions!% wenzelm@12635: \end{isamarkuptext}% wenzelm@12627: \isamarkuptrue% wenzelm@12635: % wenzelm@12652: \isamarkupsection{Document Preparation \label{sec:document-preparation}% wenzelm@12635: } wenzelm@12627: \isamarkuptrue% wenzelm@12635: % wenzelm@12644: \begin{isamarkuptext}% wenzelm@12652: Isabelle/Isar is centered around the concept of \bfindex{formal wenzelm@12767: proof documents}\index{documents|bold}. The outcome of a formal wenzelm@12767: development effort is meant to be a human-readable record, presented wenzelm@12767: as browsable PDF file or printed on paper. The overall document wenzelm@12767: structure follows traditional mathematical articles, with sections, wenzelm@12767: intermediate explanations, definitions, theorems and proofs. wenzelm@12644: wenzelm@12644: \medskip The Isabelle document preparation system essentially acts wenzelm@12671: as a front-end to {\LaTeX}. After checking specifications and wenzelm@12671: proofs formally, the theory sources are turned into typesetting wenzelm@12767: instructions in a schematic manner. This lets you write authentic wenzelm@12767: reports on theory developments with little effort: many technical wenzelm@12767: consistency checks are handled by the system. wenzelm@12745: wenzelm@12745: Here is an example to illustrate the idea of Isabelle document wenzelm@12747: preparation.% wenzelm@12747: \end{isamarkuptext}% wenzelm@12747: \isamarkuptrue% wenzelm@12747: % wenzelm@12747: \begin{quotation} wenzelm@12747: % wenzelm@12747: \begin{isamarkuptext}% wenzelm@12747: The following datatype definition of \isa{{\isacharprime}a\ bintree} models wenzelm@12747: binary trees with nodes being decorated by elements of type \isa{{\isacharprime}a}.% wenzelm@12745: \end{isamarkuptext}% wenzelm@12745: \isamarkuptrue% wenzelm@12745: \isacommand{datatype}\ {\isacharprime}a\ bintree\ {\isacharequal}\isanewline wenzelm@12747: \ \ \ \ \ Leaf\ {\isacharbar}\ Branch\ {\isacharprime}a\ \ {\isachardoublequote}{\isacharprime}a\ bintree{\isachardoublequote}\ \ {\isachardoublequote}{\isacharprime}a\ bintree{\isachardoublequote}\isamarkupfalse% wenzelm@12745: % wenzelm@12745: \begin{isamarkuptext}% wenzelm@12745: \noindent The datatype induction rule generated here is of the form wenzelm@12745: \begin{isabelle}% wenzelm@12749: \ {\isasymlbrakk}P\ Leaf{\isacharsemicolon}\isanewline paulson@14379: \isaindent{\ \ }{\isasymAnd}a\ bintree{\isadigit{1}}\ bintree{\isadigit{2}}{\isachardot}\isanewline paulson@14379: \isaindent{\ \ \ \ \ }{\isasymlbrakk}P\ bintree{\isadigit{1}}{\isacharsemicolon}\ P\ bintree{\isadigit{2}}{\isasymrbrakk}\ {\isasymLongrightarrow}\ P\ {\isacharparenleft}Branch\ a\ bintree{\isadigit{1}}\ bintree{\isadigit{2}}{\isacharparenright}{\isasymrbrakk}\isanewline wenzelm@12749: \isaindent{\ }{\isasymLongrightarrow}\ P\ bintree% wenzelm@12747: \end{isabelle}% wenzelm@12747: \end{isamarkuptext}% wenzelm@12747: \isamarkuptrue% wenzelm@12747: % wenzelm@12747: \end{quotation} wenzelm@12747: % wenzelm@12747: \begin{isamarkuptext}% wenzelm@12767: \noindent The above document output has been produced as follows: wenzelm@12745: wenzelm@12745: \begin{ttbox} wenzelm@12745: text {\ttlbrace}* wenzelm@12745: The following datatype definition of {\at}{\ttlbrace}text "'a bintree"{\ttrbrace} wenzelm@12745: models binary trees with nodes being decorated by elements wenzelm@12745: of type {\at}{\ttlbrace}typ 'a{\ttrbrace}. wenzelm@12745: *{\ttrbrace} wenzelm@12745: wenzelm@12745: datatype 'a bintree = wenzelm@12745: Leaf | Branch 'a "'a bintree" "'a bintree" wenzelm@12767: \end{ttbox} wenzelm@12767: \begin{ttbox} wenzelm@12745: text {\ttlbrace}* wenzelm@12745: {\ttback}noindent The datatype induction rule generated here is wenzelm@12745: of the form {\at}{\ttlbrace}thm [display] bintree.induct [no_vars]{\ttrbrace} wenzelm@12745: *{\ttrbrace} wenzelm@12767: \end{ttbox}\vspace{-\medskipamount} wenzelm@12745: wenzelm@12747: \noindent Here we have augmented the theory by formal comments wenzelm@12767: (using \isakeyword{text} blocks), the informal parts may again refer wenzelm@12767: to formal entities by means of ``antiquotations'' (such as wenzelm@12745: \texttt{\at}\verb,{text "'a bintree"}, or wenzelm@12747: \texttt{\at}\verb,{typ 'a},), see also \S\ref{sec:doc-prep-text}.% wenzelm@12644: \end{isamarkuptext}% wenzelm@12635: \isamarkuptrue% wenzelm@12635: % wenzelm@12647: \isamarkupsubsection{Isabelle Sessions% wenzelm@12635: } wenzelm@12635: \isamarkuptrue% wenzelm@12635: % wenzelm@12635: \begin{isamarkuptext}% wenzelm@12652: In contrast to the highly interactive mode of Isabelle/Isar theory wenzelm@12652: development, the document preparation stage essentially works in wenzelm@12671: batch-mode. An Isabelle \bfindex{session} consists of a collection wenzelm@12767: of source files that may contribute to an output document. Each wenzelm@12767: session is derived from a single parent, usually an object-logic wenzelm@12767: image like \texttt{HOL}. This results in an overall tree structure, wenzelm@12767: which is reflected by the output location in the file system wenzelm@12767: (usually rooted at \verb,~/isabelle/browser_info,). wenzelm@12644: wenzelm@12684: \medskip The easiest way to manage Isabelle sessions is via wenzelm@12686: \texttt{isatool mkdir} (generates an initial session source setup) wenzelm@12686: and \texttt{isatool make} (run sessions controlled by wenzelm@12684: \texttt{IsaMakefile}). For example, a new session wenzelm@12684: \texttt{MySession} derived from \texttt{HOL} may be produced as wenzelm@12684: follows: wenzelm@12684: wenzelm@12684: \begin{verbatim} wenzelm@12684: isatool mkdir HOL MySession wenzelm@12684: isatool make wenzelm@12684: \end{verbatim} wenzelm@12684: wenzelm@12686: The \texttt{isatool make} job also informs about the file-system wenzelm@12686: location of the ultimate results. The above dry run should be able wenzelm@12686: to produce some \texttt{document.pdf} (with dummy title, empty table wenzelm@12743: of contents etc.). Any failure at this stage usually indicates wenzelm@12686: technical problems of the {\LaTeX} installation.\footnote{Especially wenzelm@12767: make sure that \texttt{pdflatex} is present; if in doubt one may wenzelm@12686: fall back on DVI output by changing \texttt{usedir} options in wenzelm@12686: \texttt{IsaMakefile} \cite{isabelle-sys}.} wenzelm@12684: wenzelm@12684: \medskip The detailed arrangement of the session sources is as wenzelm@12747: follows. wenzelm@12644: wenzelm@12644: \begin{itemize} wenzelm@12644: wenzelm@12671: \item Directory \texttt{MySession} holds the required theory files wenzelm@12671: $T@1$\texttt{.thy}, \dots, $T@n$\texttt{.thy}. wenzelm@12644: wenzelm@12644: \item File \texttt{MySession/ROOT.ML} holds appropriate ML commands wenzelm@12644: for loading all wanted theories, usually just wenzelm@12666: ``\texttt{use_thy"$T@i$";}'' for any $T@i$ in leaf position of the wenzelm@12671: dependency graph. wenzelm@12644: wenzelm@12644: \item Directory \texttt{MySession/document} contains everything wenzelm@12652: required for the {\LaTeX} stage; only \texttt{root.tex} needs to be wenzelm@12652: provided initially. wenzelm@12644: wenzelm@12652: The latter file holds appropriate {\LaTeX} code to commence a wenzelm@12652: document (\verb,\documentclass, etc.), and to include the generated wenzelm@12743: files $T@i$\texttt{.tex} for each theory. Isabelle will generate a wenzelm@12743: file \texttt{session.tex} holding {\LaTeX} commands to include all wenzelm@12747: generated theory output files in topologically sorted order, so wenzelm@12747: \verb,\input{session}, in the body of \texttt{root.tex} does the job wenzelm@12747: in most situations. wenzelm@12652: wenzelm@12682: \item \texttt{IsaMakefile} holds appropriate dependencies and wenzelm@12682: invocations of Isabelle tools to control the batch job. In fact, wenzelm@12747: several sessions may be managed by the same \texttt{IsaMakefile}. paulson@12764: See the \emph{Isabelle System Manual} \cite{isabelle-sys} paulson@12764: for further details, especially on wenzelm@12652: \texttt{isatool usedir} and \texttt{isatool make}. wenzelm@12644: wenzelm@12644: \end{itemize} wenzelm@12644: wenzelm@12686: One may now start to populate the directory \texttt{MySession}, and wenzelm@12767: the file \texttt{MySession/ROOT.ML} accordingly. The file wenzelm@12767: \texttt{MySession/document/root.tex} should also be adapted at some wenzelm@12686: point; the default version is mostly self-explanatory. Note that wenzelm@12686: \verb,\isabellestyle, enables fine-tuning of the general appearance wenzelm@12686: of characters and mathematical symbols (see also wenzelm@12686: \S\ref{sec:doc-prep-symbols}). wenzelm@12644: wenzelm@12686: Especially observe the included {\LaTeX} packages \texttt{isabelle} wenzelm@12686: (mandatory), \texttt{isabellesym} (required for mathematical wenzelm@12743: symbols), and the final \texttt{pdfsetup} (provides sane defaults paulson@12764: for \texttt{hyperref}, including URL markup). All three are wenzelm@12743: distributed with Isabelle. Further packages may be required in paulson@12764: particular applications, say for unusual mathematical symbols. wenzelm@12644: wenzelm@12747: \medskip Any additional files for the {\LaTeX} stage go into the wenzelm@12747: \texttt{MySession/document} directory as well. In particular, wenzelm@12767: adding a file named \texttt{root.bib} causes an automatic run of wenzelm@12767: \texttt{bibtex} to process a bibliographic database; see also wenzelm@12767: \texttt{isatool document} \cite{isabelle-sys}. wenzelm@12652: wenzelm@12652: \medskip Any failure of the document preparation phase in an wenzelm@12671: Isabelle batch session leaves the generated sources in their target wenzelm@12767: location, identified by the accompanying error message. This lets wenzelm@12767: you trace {\LaTeX} problems with the generated files at hand.% wenzelm@12644: \end{isamarkuptext}% wenzelm@12644: \isamarkuptrue% wenzelm@12644: % wenzelm@12647: \isamarkupsubsection{Structure Markup% wenzelm@12644: } wenzelm@12644: \isamarkuptrue% wenzelm@12644: % wenzelm@12644: \begin{isamarkuptext}% wenzelm@12652: The large-scale structure of Isabelle documents follows existing wenzelm@12652: {\LaTeX} conventions, with chapters, sections, subsubsections etc. wenzelm@12652: The Isar language includes separate \bfindex{markup commands}, which wenzelm@12682: do not affect the formal meaning of a theory (or proof), but result wenzelm@12666: in corresponding {\LaTeX} elements. wenzelm@12644: wenzelm@12666: There are separate markup commands depending on the textual context: wenzelm@12666: in header position (just before \isakeyword{theory}), within the wenzelm@12666: theory body, or within a proof. The header needs to be treated wenzelm@12666: specially here, since ordinary theory and proof commands may only wenzelm@12666: occur \emph{after} the initial \isakeyword{theory} specification. wenzelm@12644: wenzelm@12666: \medskip wenzelm@12644: wenzelm@12644: \begin{tabular}{llll} wenzelm@12644: header & theory & proof & default meaning \\\hline wenzelm@12644: & \commdx{chapter} & & \verb,\chapter, \\ wenzelm@12644: \commdx{header} & \commdx{section} & \commdx{sect} & \verb,\section, \\ wenzelm@12644: & \commdx{subsection} & \commdx{subsect} & \verb,\subsection, \\ wenzelm@12644: & \commdx{subsubsection} & \commdx{subsubsect} & \verb,\subsubsection, \\ wenzelm@12644: \end{tabular} wenzelm@12644: wenzelm@12644: \medskip wenzelm@12644: wenzelm@12644: From the Isabelle perspective, each markup command takes a single wenzelm@12747: $text$ argument (delimited by \verb,",~\isa{{\isasymdots}}~\verb,", or wenzelm@12747: \verb,{,\verb,*,~\isa{{\isasymdots}}~\verb,*,\verb,},). After stripping any wenzelm@12644: surrounding white space, the argument is passed to a {\LaTeX} macro wenzelm@12767: \verb,\isamarkupXYZ, for command \isakeyword{XYZ}. These macros are wenzelm@12767: defined in \verb,isabelle.sty, according to the meaning given in the wenzelm@12767: rightmost column above. wenzelm@12644: wenzelm@12644: \medskip The following source fragment illustrates structure markup wenzelm@12652: of a theory. Note that {\LaTeX} labels may be included inside of wenzelm@12652: section headings as well. wenzelm@12644: wenzelm@12644: \begin{ttbox} wenzelm@12644: header {\ttlbrace}* Some properties of Foo Bar elements *{\ttrbrace} wenzelm@12644: wenzelm@12644: theory Foo_Bar = Main: wenzelm@12644: wenzelm@12644: subsection {\ttlbrace}* Basic definitions *{\ttrbrace} wenzelm@12644: wenzelm@12644: consts wenzelm@12644: foo :: \dots wenzelm@12644: bar :: \dots wenzelm@12647: wenzelm@12644: defs \dots wenzelm@12647: wenzelm@12644: subsection {\ttlbrace}* Derived rules *{\ttrbrace} wenzelm@12644: wenzelm@12644: lemma fooI: \dots wenzelm@12644: lemma fooE: \dots wenzelm@12644: wenzelm@12647: subsection {\ttlbrace}* Main theorem {\ttback}label{\ttlbrace}sec:main-theorem{\ttrbrace} *{\ttrbrace} wenzelm@12644: wenzelm@12644: theorem main: \dots wenzelm@12644: wenzelm@12644: end wenzelm@12767: \end{ttbox}\vspace{-\medskipamount} wenzelm@12644: wenzelm@12767: You may occasionally want to change the meaning of markup commands, wenzelm@12767: say via \verb,\renewcommand, in \texttt{root.tex}. For example, wenzelm@12767: \verb,\isamarkupheader, is a good candidate for some tuning. We wenzelm@12767: could move it up in the hierarchy to become \verb,\chapter,. wenzelm@12644: wenzelm@12644: \begin{verbatim} wenzelm@12644: \renewcommand{\isamarkupheader}[1]{\chapter{#1}} wenzelm@12644: \end{verbatim} wenzelm@12644: wenzelm@12767: \noindent Now we must change the document class given in wenzelm@12767: \texttt{root.tex} to something that supports chapters. A suitable wenzelm@12767: command is \verb,\documentclass{report},. wenzelm@12644: wenzelm@12647: \medskip The {\LaTeX} macro \verb,\isabellecontext, is maintained to wenzelm@12647: hold the name of the current theory context. This is particularly wenzelm@12652: useful for document headings: wenzelm@12644: wenzelm@12644: \begin{verbatim} wenzelm@12652: \renewcommand{\isamarkupheader}[1] wenzelm@12644: {\chapter{#1}\markright{THEORY~\isabellecontext}} wenzelm@12644: \end{verbatim} wenzelm@12644: wenzelm@12644: \noindent Make sure to include something like wenzelm@12647: \verb,\pagestyle{headings}, in \texttt{root.tex}; the document paulson@12764: should have more than two pages to show the effect.% wenzelm@12644: \end{isamarkuptext}% wenzelm@12644: \isamarkuptrue% wenzelm@12644: % wenzelm@12745: \isamarkupsubsection{Formal Comments and Antiquotations \label{sec:doc-prep-text}% wenzelm@12644: } wenzelm@12644: \isamarkuptrue% wenzelm@12644: % wenzelm@12644: \begin{isamarkuptext}% wenzelm@12745: Isabelle \bfindex{source comments}, which are of the form wenzelm@12747: \verb,(,\verb,*,~\isa{{\isasymdots}}~\verb,*,\verb,),, essentially act like wenzelm@12747: white space and do not really contribute to the content. They wenzelm@12747: mainly serve technical purposes to mark certain oddities in the raw wenzelm@12747: input text. In contrast, \bfindex{formal comments} are portions of wenzelm@12747: text that are associated with formal Isabelle/Isar commands wenzelm@12682: (\bfindex{marginal comments}), or as standalone paragraphs within a wenzelm@12666: theory or proof context (\bfindex{text blocks}). wenzelm@12658: wenzelm@12658: \medskip Marginal comments are part of each command's concrete wenzelm@12671: syntax \cite{isabelle-ref}; the common form is ``\verb,--,~$text$'' wenzelm@12747: where $text$ is delimited by \verb,",\isa{{\isasymdots}}\verb,", or wenzelm@12747: \verb,{,\verb,*,~\isa{{\isasymdots}}~\verb,*,\verb,}, as before. Multiple wenzelm@12671: marginal comments may be given at the same time. Here is a simple wenzelm@12671: example:% wenzelm@12666: \end{isamarkuptext}% wenzelm@12666: \isamarkuptrue% wenzelm@12666: \isacommand{lemma}\ {\isachardoublequote}A\ {\isacharminus}{\isacharminus}{\isachargreater}\ A{\isachardoublequote}\isanewline wenzelm@12666: \ \ % wenzelm@12666: \isamarkupcmt{a triviality of propositional logic% wenzelm@12666: } wenzelm@12666: \isanewline wenzelm@12666: \ \ % wenzelm@12666: \isamarkupcmt{(should not really bother)% wenzelm@12666: } wenzelm@12666: \isanewline wenzelm@12666: \ \ \isamarkupfalse% wenzelm@12666: \isacommand{by}\ {\isacharparenleft}rule\ impI{\isacharparenright}\ % wenzelm@12666: \isamarkupcmt{implicit assumption step involved here% wenzelm@12666: } wenzelm@12666: \isamarkupfalse% wenzelm@12666: % wenzelm@12666: \begin{isamarkuptext}% wenzelm@12666: \noindent The above output has been produced as follows: wenzelm@12658: wenzelm@12658: \begin{verbatim} wenzelm@12658: lemma "A --> A" wenzelm@12658: -- "a triviality of propositional logic" wenzelm@12658: -- "(should not really bother)" wenzelm@12658: by (rule impI) -- "implicit assumption step involved here" wenzelm@12658: \end{verbatim} wenzelm@12658: wenzelm@12671: From the {\LaTeX} viewpoint, ``\verb,--,'' acts like a markup wenzelm@12671: command, associated with the macro \verb,\isamarkupcmt, (taking a wenzelm@12671: single argument). wenzelm@12658: wenzelm@12666: \medskip Text blocks are introduced by the commands \bfindex{text} wenzelm@12666: and \bfindex{txt}, for theory and proof contexts, respectively. wenzelm@12666: Each takes again a single $text$ argument, which is interpreted as a wenzelm@12666: free-form paragraph in {\LaTeX} (surrounded by some additional wenzelm@12671: vertical space). This behavior may be changed by redefining the wenzelm@12671: {\LaTeX} environments of \verb,isamarkuptext, or wenzelm@12671: \verb,isamarkuptxt,, respectively (via \verb,\renewenvironment,) The wenzelm@12671: text style of the body is determined by \verb,\isastyletext, and wenzelm@12671: \verb,\isastyletxt,; the default setup uses a smaller font within wenzelm@12747: proofs. This may be changed as follows: wenzelm@12747: wenzelm@12747: \begin{verbatim} wenzelm@12747: \renewcommand{\isastyletxt}{\isastyletext} wenzelm@12747: \end{verbatim} wenzelm@12658: wenzelm@12767: \medskip The $text$ part of Isabelle markup commands essentially wenzelm@12767: inserts \emph{quoted material} into a formal text, mainly for wenzelm@12767: instruction of the reader. An \bfindex{antiquotation} is again a wenzelm@12767: formal object embedded into such an informal portion. The wenzelm@12767: interpretation of antiquotations is limited to some well-formedness wenzelm@12767: checks, with the result being pretty printed to the resulting wenzelm@12767: document. Quoted text blocks together with antiquotations provide wenzelm@12767: an attractive means of referring to formal entities, with good wenzelm@12767: confidence in getting the technical details right (especially syntax wenzelm@12767: and types). wenzelm@12658: wenzelm@12666: The general syntax of antiquotations is as follows: wenzelm@12658: \texttt{{\at}{\ttlbrace}$name$ $arguments${\ttrbrace}}, or wenzelm@12658: \texttt{{\at}{\ttlbrace}$name$ [$options$] $arguments${\ttrbrace}} wenzelm@12666: for a comma-separated list of options consisting of a $name$ or wenzelm@12767: \texttt{$name$=$value$} each. The syntax of $arguments$ depends on wenzelm@12767: the kind of antiquotation, it generally follows the same conventions wenzelm@12767: for types, terms, or theorems as in the formal part of a theory. wenzelm@12658: wenzelm@12767: \medskip This sentence demonstrates quotations and antiquotations: wenzelm@12767: \isa{{\isasymlambda}x\ y{\isachardot}\ x} is a well-typed term. wenzelm@12658: paulson@12764: \medskip\noindent The output above was produced as follows: wenzelm@12658: \begin{ttbox} wenzelm@12658: text {\ttlbrace}* paulson@12764: This sentence demonstrates quotations and antiquotations: wenzelm@12658: {\at}{\ttlbrace}term "%x y. x"{\ttrbrace} is a well-typed term. wenzelm@12658: *{\ttrbrace} wenzelm@12767: \end{ttbox}\vspace{-\medskipamount} wenzelm@12658: paulson@12764: The notational change from the ASCII character~\verb,%, to the wenzelm@12767: symbol~\isa{{\isasymlambda}} reveals that Isabelle printed this term, after wenzelm@12767: parsing and type-checking. Document preparation enables symbolic wenzelm@12767: output by default. wenzelm@12658: paulson@12764: \medskip The next example includes an option to modify Isabelle's paulson@12764: \verb,show_types, flag. The antiquotation wenzelm@12767: \texttt{{\at}}\verb,{term [show_types] "%x y. x"}, produces the wenzelm@12767: output \isa{{\isasymlambda}{\isacharparenleft}x{\isasymColon}{\isacharprime}a{\isacharparenright}\ y{\isasymColon}{\isacharprime}b{\isachardot}\ x}. Type inference has figured wenzelm@12767: out the most general typings in the present theory context. Terms wenzelm@12767: may acquire different typings due to constraints imposed by their wenzelm@12767: environment; within a proof, for example, variables are given the wenzelm@12767: same types as they have in the main goal statement. wenzelm@12658: paulson@12764: \medskip Several further kinds of antiquotations and options are wenzelm@12666: available \cite{isabelle-sys}. Here are a few commonly used wenzelm@12671: combinations: wenzelm@12658: wenzelm@12658: \medskip wenzelm@12658: wenzelm@12658: \begin{tabular}{ll} wenzelm@12658: \texttt{\at}\verb,{typ,~$\tau$\verb,}, & print type $\tau$ \\ wenzelm@12658: \texttt{\at}\verb,{term,~$t$\verb,}, & print term $t$ \\ wenzelm@12658: \texttt{\at}\verb,{prop,~$\phi$\verb,}, & print proposition $\phi$ \\ wenzelm@12666: \texttt{\at}\verb,{prop [display],~$\phi$\verb,}, & print large proposition $\phi$ (with linebreaks) \\ wenzelm@12658: \texttt{\at}\verb,{prop [source],~$\phi$\verb,}, & check proposition $\phi$, print its input \\ wenzelm@12658: \texttt{\at}\verb,{thm,~$a$\verb,}, & print fact $a$ \\ wenzelm@12658: \texttt{\at}\verb,{thm,~$a$~\verb,[no_vars]}, & print fact $a$, fixing schematic variables \\ wenzelm@12747: \texttt{\at}\verb,{thm [source],~$a$\verb,}, & check availability of fact $a$, print its name \\ wenzelm@12658: \texttt{\at}\verb,{text,~$s$\verb,}, & print uninterpreted text $s$ \\ wenzelm@12658: \end{tabular} wenzelm@12658: wenzelm@12658: \medskip wenzelm@12658: wenzelm@12666: Note that \attrdx{no_vars} given above is \emph{not} an wenzelm@12666: antiquotation option, but an attribute of the theorem argument given wenzelm@12666: here. This might be useful with a diagnostic command like wenzelm@12666: \isakeyword{thm}, too. wenzelm@12658: wenzelm@12666: \medskip The \texttt{\at}\verb,{text, $s$\verb,}, antiquotation is wenzelm@12658: particularly interesting. Embedding uninterpreted text within an wenzelm@12666: informal body might appear useless at first sight. Here the key wenzelm@12666: virtue is that the string $s$ is processed as Isabelle output, wenzelm@12666: interpreting Isabelle symbols appropriately. wenzelm@12658: wenzelm@12666: For example, \texttt{\at}\verb,{text "\\"}, produces \isa{{\isasymforall}{\isasymexists}}, according to the standard interpretation of these symbol wenzelm@12666: (cf.\ \S\ref{sec:doc-prep-symbols}). Thus we achieve consistent wenzelm@12658: mathematical notation in both the formal and informal parts of the wenzelm@12767: document very easily, independently of the term language of wenzelm@12767: Isabelle. Manual {\LaTeX} code would leave more control over the wenzelm@12767: typesetting, but is also slightly more tedious.% wenzelm@12644: \end{isamarkuptext}% wenzelm@12644: \isamarkuptrue% wenzelm@12644: % wenzelm@12674: \isamarkupsubsection{Interpretation of Symbols \label{sec:doc-prep-symbols}% wenzelm@12644: } wenzelm@12644: \isamarkuptrue% wenzelm@12644: % wenzelm@12644: \begin{isamarkuptext}% wenzelm@12666: As has been pointed out before (\S\ref{sec:syntax-symbols}), wenzelm@12671: Isabelle symbols are the smallest syntactic entities --- a wenzelm@12682: straightforward generalization of ASCII characters. While Isabelle wenzelm@12666: does not impose any interpretation of the infinite collection of paulson@12764: named symbols, {\LaTeX} documents use canonical glyphs for certain wenzelm@12671: standard symbols \cite[appendix~A]{isabelle-sys}. wenzelm@12658: wenzelm@12767: The {\LaTeX} code produced from Isabelle text follows a simple wenzelm@12767: scheme. You can tune the final appearance by redefining certain wenzelm@12767: macros, say in \texttt{root.tex} of the document. wenzelm@12658: wenzelm@12671: \begin{enumerate} wenzelm@12671: wenzelm@12671: \item 7-bit ASCII characters: letters \texttt{A\dots Z} and wenzelm@12747: \texttt{a\dots z} are output directly, digits are passed as an wenzelm@12671: argument to the \verb,\isadigit, macro, other characters are wenzelm@12671: replaced by specifically named macros of the form wenzelm@12666: \verb,\isacharXYZ,. wenzelm@12658: wenzelm@12767: \item Named symbols: \verb,\,\verb,, is turned into wenzelm@12767: \verb,{\isasymXYZ},; note the additional braces. wenzelm@12658: wenzelm@12767: \item Named control symbols: \verb,\,\verb,<^XYZ>, is turned into wenzelm@12767: \verb,\isactrlXYZ,; subsequent symbols may act as arguments if the wenzelm@12767: control macro is defined accordingly. wenzelm@12671: wenzelm@12666: \end{enumerate} wenzelm@12666: paulson@12764: You may occasionally wish to give new {\LaTeX} interpretations of paulson@12764: named symbols. This merely requires an appropriate definition of wenzelm@12767: \verb,\isasymXYZ,, for \verb,\,\verb,, (see wenzelm@12747: \texttt{isabelle.sty} for working examples). Control symbols are wenzelm@12747: slightly more difficult to get right, though. wenzelm@12666: wenzelm@12666: \medskip The \verb,\isabellestyle, macro provides a high-level wenzelm@12666: interface to tune the general appearance of individual symbols. For wenzelm@12671: example, \verb,\isabellestyle{it}, uses the italics text style to wenzelm@12671: mimic the general appearance of the {\LaTeX} math mode; double wenzelm@12743: quotes are not printed at all. The resulting quality of typesetting wenzelm@12743: is quite good, so this should be the default style for work that wenzelm@12743: gets distributed to a broader audience.% wenzelm@12644: \end{isamarkuptext}% wenzelm@12644: \isamarkuptrue% wenzelm@12644: % wenzelm@12652: \isamarkupsubsection{Suppressing Output \label{sec:doc-prep-suppress}% wenzelm@12644: } wenzelm@12644: \isamarkuptrue% wenzelm@12644: % wenzelm@12644: \begin{isamarkuptext}% wenzelm@12749: By default, Isabelle's document system generates a {\LaTeX} file for wenzelm@12749: each theory that gets loaded while running the session. The wenzelm@12749: generated \texttt{session.tex} will include all of these in order of wenzelm@12749: appearance, which in turn gets included by the standard wenzelm@12743: \texttt{root.tex}. Certainly one may change the order or suppress wenzelm@12747: unwanted theories by ignoring \texttt{session.tex} and load wenzelm@12747: individual files directly in \texttt{root.tex}. On the other hand, wenzelm@12747: such an arrangement requires additional maintenance whenever the wenzelm@12747: collection of theories changes. wenzelm@12644: wenzelm@12647: Alternatively, one may tune the theory loading process in wenzelm@12652: \texttt{ROOT.ML} itself: traversal of the theory dependency graph wenzelm@12671: may be fine-tuned by adding \verb,use_thy, invocations, although wenzelm@12671: topological sorting still has to be observed. Moreover, the ML wenzelm@12671: operator \verb,no_document, temporarily disables document generation wenzelm@12767: while executing a theory loader command. Its usage is like this: wenzelm@12647: wenzelm@12647: \begin{verbatim} wenzelm@12666: no_document use_thy "T"; wenzelm@12647: \end{verbatim} wenzelm@12647: wenzelm@12767: \medskip Theory output may be suppressed more selectively. Research wenzelm@12767: articles and slides usually do not include the formal content in wenzelm@12767: full. Delimiting \bfindex{ignored material} by the special source wenzelm@12767: comments \verb,(,\verb,*,\verb,<,\verb,*,\verb,), and wenzelm@12767: \verb,(,\verb,*,\verb,>,\verb,*,\verb,), tells the document wenzelm@12767: preparation system to suppress these parts; the formal checking of wenzelm@12771: the theory is unchanged, of course. wenzelm@12647: wenzelm@12767: In this example, we hide a theory's \isakeyword{theory} and wenzelm@12767: \isakeyword{end} brackets: wenzelm@12647: wenzelm@12647: \medskip wenzelm@12647: wenzelm@12647: \begin{tabular}{l} wenzelm@12647: \verb,(,\verb,*,\verb,<,\verb,*,\verb,), \\ wenzelm@12666: \texttt{theory T = Main:} \\ wenzelm@12647: \verb,(,\verb,*,\verb,>,\verb,*,\verb,), \\ wenzelm@12647: ~~$\vdots$ \\ wenzelm@12647: \verb,(,\verb,*,\verb,<,\verb,*,\verb,), \\ wenzelm@12647: \texttt{end} \\ wenzelm@12647: \verb,(,\verb,*,\verb,>,\verb,*,\verb,), \\ wenzelm@12647: \end{tabular} wenzelm@12647: wenzelm@12647: \medskip wenzelm@12647: paulson@12764: Text may be suppressed in a fine-grained manner. We may even hide wenzelm@12747: vital parts of a proof, pretending that things have been simpler wenzelm@12767: than they really were. For example, this ``fully automatic'' proof wenzelm@12767: is actually a fake:% wenzelm@12649: \end{isamarkuptext}% wenzelm@12649: \isamarkuptrue% wenzelm@12649: \isacommand{lemma}\ {\isachardoublequote}x\ {\isasymnoteq}\ {\isacharparenleft}{\isadigit{0}}{\isacharcolon}{\isacharcolon}int{\isacharparenright}\ {\isasymLongrightarrow}\ {\isadigit{0}}\ {\isacharless}\ x\ {\isacharasterisk}\ x{\isachardoublequote}\isanewline wenzelm@12649: \ \ \isamarkupfalse% wenzelm@12649: \isacommand{by}\ {\isacharparenleft}auto{\isacharparenright}\isamarkupfalse% wenzelm@12649: % wenzelm@12649: \begin{isamarkuptext}% wenzelm@12649: \noindent Here the real source of the proof has been as follows: wenzelm@12649: wenzelm@12649: \begin{verbatim} paulson@14353: by (auto(*<*)simp add: zero_less_mult_iff(*>*)) wenzelm@12658: \end{verbatim} wenzelm@12658: %(* wenzelm@12649: wenzelm@12767: \medskip Suppressing portions of printed text demands care. You wenzelm@12767: should not misrepresent the underlying theory development. It is wenzelm@12767: easy to invalidate the visible text by hiding references to wenzelm@12767: questionable axioms. wenzelm@12652: wenzelm@12747: Authentic reports of Isabelle/Isar theories, say as part of a wenzelm@12767: library, should suppress nothing. Other users may need the full wenzelm@12767: information for their own derivative work. If a particular wenzelm@12767: formalization appears inadequate for general public coverage, it is wenzelm@12767: often more appropriate to think of a better way in the first place. wenzelm@12671: wenzelm@12671: \medskip Some technical subtleties of the wenzelm@12666: \verb,(,\verb,*,\verb,<,\verb,*,\verb,),~\verb,(,\verb,*,\verb,>,\verb,*,\verb,), paulson@12764: elements need to be kept in mind, too --- the system performs few wenzelm@12671: sanity checks here. Arguments of markup commands and formal wenzelm@12649: comments must not be hidden, otherwise presentation fails. Open and wenzelm@12751: close parentheses need to be inserted carefully; it is easy to hide wenzelm@12751: the wrong parts, especially after rearranging the theory text.% wenzelm@12635: \end{isamarkuptext}% wenzelm@12627: \isamarkuptrue% wenzelm@11866: \isamarkupfalse% wenzelm@11648: \end{isabellebody}% wenzelm@11648: %%% Local Variables: wenzelm@11648: %%% mode: latex wenzelm@11648: %%% TeX-master: "root" wenzelm@11648: %%% End: