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