# HG changeset patch # User wenzelm # Date 1011015562 -3600 # Node ID 46e3ef8dd9eace1c5f82a4b0b7baad14c3b88f19 # Parent 83cd2140977d3964affe3e3d89ced31d661482aa tuned; diff -r 83cd2140977d -r 46e3ef8dd9ea doc-src/TutorialI/Documents/Documents.thy --- a/doc-src/TutorialI/Documents/Documents.thy Mon Jan 14 00:16:43 2002 +0100 +++ b/doc-src/TutorialI/Documents/Documents.thy Mon Jan 14 14:39:22 2002 +0100 @@ -5,22 +5,21 @@ section {* Concrete Syntax \label{sec:concrete-syntax} *} text {* - Concerning Isabelle's ``inner'' language of simply-typed @{text - \}-calculus, the core concept of Isabelle's elaborate - infrastructure for concrete syntax is that of general - \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. + The core concept of Isabelle's elaborate infrastructure for concrete + syntax is that of general \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, the whole affair of parser and pretty printer - configuration is rather subtle, see also \cite{isabelle-ref}. - Syntax specifications given by end-users need to interact properly - with the existing setup of Isabelle/Pure and Isabelle/HOL. It is + In full generality, parser and pretty printer configuration is a + rather subtle affair, see \cite{isabelle-ref} for details. Syntax + specifications given by end-users need to interact properly with the + existing setup of Isabelle/Pure and Isabelle/HOL. It is particularly important to get the precedence of new syntactic constructs right, avoiding ambiguities with existing elements. \medskip Subsequently we introduce a few simple syntax declaration - forms that already cover most common situations fairly well. + forms that already cover many common situations fairly well. *} @@ -31,8 +30,8 @@ directly or indirectly, including \isacommand{consts}, \isacommand{constdefs}, or \isacommand{datatype} (for the constructor operations). Type-constructors may be annotated as - well, although this is less frequently encountered in practice - (@{text "*"} and @{text "+"} types may come to mind). + well, although this is less frequently encountered in practice (the + infix type @{text "\"} comes to mind). Infix declarations\index{infix annotations} provide a useful special case of mixfixes, where users need not care about the full details @@ -54,18 +53,24 @@ as @{text "op [+]"}; together with plain prefix application this turns @{text "xor A"} into @{text "op [+] A"}. - \medskip The string @{text [source] "[+]"} in the above annotation - refers to the bit of concrete syntax to represent the operator, + \medskip The keyword \isakeyword{infixl} specifies an infix operator + that is nested to the \emph{left}: in iterated applications the more + complex expression appears on the left-hand side: @{term "A [+] B + [+] C"} stands for @{text "(A [+] B) [+] C"}. Similarly, + \isakeyword{infixr} specifies to nesting to the \emph{right}, + reading @{term "A [+] B [+] C"} as @{text "A [+] (B [+] C)"}. In + contrast, a \emph{non-oriented} declaration via \isakeyword{infix} + would render @{term "A [+] B [+] C"} illegal, but demand explicit + parentheses to indicate the intended grouping. + + The string @{text [source] "[+]"} in the above annotation refers to + the concrete syntax to represent the operator (a literal token), while the number @{text 60} determines the precedence of the construct (i.e.\ the syntactic priorities of the arguments and - result). - - As it happens, Isabelle/HOL already spends many popular combinations - of ASCII symbols for its own use, including both @{text "+"} and - @{text "++"}. Slightly more awkward combinations like the present - @{text "[+]"} tend to be available for user extensions. The current - arrangement of inner syntax may be inspected via - \commdx{print\protect\_syntax}, albeit its output is enormous. + result). As it happens, Isabelle/HOL already uses up many popular + combinations of ASCII symbols for its own use, including both @{text + "+"} and @{text "++"}. Slightly more awkward combinations like the + present @{text "[+]"} tend to be available for user extensions. Operator precedence also needs some special considerations. The admissible range is 0--1000. Very low or high priorities are @@ -76,15 +81,6 @@ "*"}) above 50. User syntax should strive to coexist with common HOL forms, or use the mostly unused range 100--900. - The keyword \isakeyword{infixl} specifies an infix operator that is - nested to the \emph{left}: in iterated applications the more complex - expression appears on the left-hand side: @{term "A [+] B [+] C"} - stands for @{text "(A [+] B) [+] C"}. Similarly, - \isakeyword{infixr} specifies to nesting to the \emph{right}, - reading @{term "A [+] B [+] C"} as @{text "A [+] (B [+] C)"}. In - contrast, a \emph{non-oriented} declaration via \isakeyword{infix} - would render @{term "A [+] B [+] C"} illegal, but demand explicit - parentheses to indicate the intended grouping. *} @@ -115,7 +111,7 @@ interpretation is left to further front-end tools. For example, both the user-interface of Proof~General + X-Symbol and the Isabelle document processor (see \S\ref{sec:document-preparation}) display - the \verb,\,\verb,, symbol really as @{text \}. + the \verb,\,\verb,, symbol as @{text \}. A list of standard Isabelle symbols is given in \cite[appendix~A]{isabelle-sys}. Users may introduce their own @@ -173,40 +169,26 @@ text {* The \commdx{syntax} command introduced here acts like - \isakeyword{consts}, but without declaring a logical constant; an - optional print mode specification may be given, too. Note that the - type declaration given above merely serves for syntactic purposes, - and is not checked for consistency with the real constant. + \isakeyword{consts}, but without declaring a logical constant. The + print mode specification (here @{text "(xsymbols)"}) limits the + effect of the syntax annotation concerning output; that alternative + production available for input invariably. Also note that the type + declaration in \isakeyword{syntax} merely serves for syntactic + purposes, and is \emph{not} checked for consistency with the real + constant. \medskip We may now write @{text "A [+] B"} or @{text "A \ B"} in input, while output uses the nicer syntax of $xsymbols$, provided that print mode is active. Such an arrangement is particularly useful for interactive development, where users may type plain ASCII text, but gain improved visual feedback from the system. - - \begin{warn} - Alternative syntax declarations are apt to result in varying - occurrences of concrete syntax in the input sources. Isabelle - provides no systematic way to convert alternative syntax expressions - back and forth; print modes only affect situations where formal - entities are pretty printed by the Isabelle process (e.g.\ output of - terms and types), but not the original theory text. - \end{warn} - - \medskip The following variant makes the alternative @{text \} - notation only available for output. Thus we may enforce input - sources to refer to plain ASCII only, but effectively disable - cut-and-paste from output at the same time. *} -syntax (xsymbols output) - xor :: "bool \ bool \ bool" (infixl "\\" 60) - subsection {* Prefix Annotations *} text {* - Prefix syntax annotations\index{prefix annotation} are just another + Prefix syntax annotations\index{prefix annotation} are another degenerate form of mixfixes \cite{isabelle-ref}, without any template arguments or priorities --- just some bits of literal syntax. The following example illustrates this idea idea by @@ -226,8 +208,9 @@ that a constructor like @{text Euro} actually is a function @{typ "nat \ currency"}. An expression like @{text "Euro 10"} will be printed as @{term "\ 10"}; only the head of the application is - subject to our concrete syntax. This simple form already achieves - conformance with notational standards of the European Commission. + subject to our concrete syntax. This rather simple form already + achieves conformance with notational standards of the European + Commission. Prefix syntax also works for plain \isakeyword{consts} or \isakeyword{constdefs}, of course. @@ -239,22 +222,22 @@ text{* Mixfix syntax annotations work well in those situations where particular constant application forms need to be decorated by - concrete syntax; just reconsider @{text "xor A B"} versus @{text "A - \ B"} covered before. Occasionally the relationship between some - piece of notation and its internal form is slightly more involved. - Here the concept of \bfindex{syntax translations} enters the scene. + concrete syntax; e.g.\ @{text "xor A B"} versus @{text "A \ B"} + covered before. Occasionally the relationship between some piece of + notation and its internal form is slightly more involved. Here the + concept of \bfindex{syntax translations} enters the scene. Using the raw \isakeyword{syntax}\index{syntax (command)} command we may introduce uninterpreted notational elements, while - \commdx{translations} relates input forms with more complex logical + \commdx{translations} relate input forms with more complex logical expressions. This essentially provides a simple mechanism for syntactic macros; even heavier transformations may be written in ML \cite{isabelle-ref}. \medskip A typical example of syntax translations is to decorate - relational expressions (i.e.\ set-membership of tuples) with - handsome symbolic notation, such as @{text "(x, y) \ sim"} versus - @{text "x \ y"}. + relational expressions (i.e.\ set-membership of tuples) with nice + symbolic notation, such as @{text "(x, y) \ sim"} versus @{text "x + \ y"}. *} consts @@ -308,16 +291,6 @@ sections, intermediate explanations, definitions, theorems and proofs. - The Isar proof language \cite{Wenzel-PhD}, which is not covered in - this book, admits to write formal proof texts that are acceptable - both to the machine and human readers at the same time. Thus - marginal comments and explanations may be kept at a minimum. Even - without proper coverage of human-readable proofs, Isabelle document - preparation is very useful to produce formally derived texts. - Unstructured proof scripts given here may be just ignored by - readers, or intentionally suppressed from the text by the writer - (see also \S\ref{sec:doc-prep-suppress}). - \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 @@ -333,7 +306,7 @@ 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 theory source files that may contribute to an output document + of source files that may contribute to an output document eventually. 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 @@ -354,14 +327,14 @@ The \texttt{isatool 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 that stage usually indicates + of contents etc.). Any failure at this stage usually indicates technical problems of the {\LaTeX} installation.\footnote{Especially make sure that \texttt{pdflatex} is present; if all fails one may fall back on DVI output by changing \texttt{usedir} options in \texttt{IsaMakefile} \cite{isabelle-sys}.} \medskip The detailed arrangement of the session sources is as - follows: + follows; advanced \begin{itemize} @@ -379,9 +352,9 @@ 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. The generated - \texttt{session.tex} will contain {\LaTeX} commands to include all - generated files in topologically sorted order, so + 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 \texttt{root.tex} does the job in most situations. @@ -403,9 +376,9 @@ Especially observe the included {\LaTeX} packages \texttt{isabelle} (mandatory), \texttt{isabellesym} (required for mathematical - symbols), and the final \texttt{pdfsetup} (provides handsome - defaults for \texttt{hyperref}, including URL markup) --- all three - are distributed with Isabelle. Further packages may be required in + 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, e.g.\ for unusual mathematical symbols. \medskip Additional files for the {\LaTeX} stage may be put into the @@ -495,10 +468,10 @@ \renewcommand{\isamarkupheader}[1]{\chapter{#1}} \end{verbatim} - \noindent Certainly, this requires to change the default - \verb,\documentclass{article}, in \texttt{root.tex} to something - that supports the notion of chapters in the first place, e.g.\ - \verb,\documentclass{report},. + \noindent That particular modification requires to change the + default \verb,\documentclass{article}, in \texttt{root.tex} to + something that supports the notion of chapters in the first place, + such as \verb,\documentclass{report},. \medskip The {\LaTeX} macro \verb,\isabellecontext, is maintained to hold the name of the current theory context. This is particularly @@ -572,7 +545,7 @@ an informal portion. The interpretation of antiquotations is limited to some well-formedness checks, with the result being pretty printed to the resulting document. So quoted text blocks together - with antiquotations provide very handsome means to reference formal + with antiquotations provide very useful means to reference formal entities with good confidence in getting the technical details right (especially syntax and types). @@ -623,7 +596,7 @@ \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 validity of fact $a$, print its name \\ + \texttt{\at}\verb,{thm [source],~$a$\verb,}, & check availability of fact, print name $a$ \\ \texttt{\at}\verb,{text,~$s$\verb,}, & print uninterpreted text $s$ \\ \end{tabular} @@ -690,10 +663,9 @@ 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 usually be the default - style for real production work that gets distributed to a broader - audience. + 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. *} @@ -701,14 +673,14 @@ text {* By default, Isabelle's document system generates a {\LaTeX} source - file for each theory that happens to get 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 - include individual files in \texttt{root.tex} by hand. On the other - hand, such an arrangement requires additional maintenance chores - whenever the collection of theories changes. + 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 include + individual files in \texttt{root.tex} by hand. On the other hand, + such an arrangement requires additional maintenance chores 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 @@ -772,11 +744,11 @@ arbitrary axioms etc.) that have been hidden from sight beforehand. Authentic reports of formal theories, say as part of a library, - usually should refrain from suppressing parts of the text at all. - Other users may need the full information for their own derivative - work. If a particular formalization appears inadequate for general - public coverage, it is often more appropriate to think of a better - way in the first place. + should refrain from suppressing parts of the text at all. Other + users may need the full information for their own derivative work. + If a particular formalization appears inadequate for general public + coverage, it is often more appropriate to think of a better way in + the first place. \medskip Some technical subtleties of the \verb,(,\verb,*,\verb,<,\verb,*,\verb,),~\verb,(,\verb,*,\verb,>,\verb,*,\verb,), diff -r 83cd2140977d -r 46e3ef8dd9ea doc-src/TutorialI/Documents/document/Documents.tex --- a/doc-src/TutorialI/Documents/document/Documents.tex Mon Jan 14 00:16:43 2002 +0100 +++ b/doc-src/TutorialI/Documents/document/Documents.tex Mon Jan 14 14:39:22 2002 +0100 @@ -8,21 +8,21 @@ \isamarkuptrue% % \begin{isamarkuptext}% -Concerning Isabelle's ``inner'' language of simply-typed \isa{{\isasymlambda}}-calculus, the core concept of Isabelle's elaborate - infrastructure for concrete syntax is that of general - \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. +The core concept of Isabelle's elaborate infrastructure for concrete + syntax is that of general \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, the whole affair of parser and pretty printer - configuration is rather subtle, see also \cite{isabelle-ref}. - Syntax specifications given by end-users need to interact properly - with the existing setup of Isabelle/Pure and Isabelle/HOL. It is + In full generality, parser and pretty printer configuration is a + rather subtle affair, see \cite{isabelle-ref} for details. Syntax + specifications given by end-users need to interact properly with the + existing setup of Isabelle/Pure and Isabelle/HOL. It is particularly important to get the precedence of new syntactic constructs right, avoiding ambiguities with existing elements. \medskip Subsequently we introduce a few simple syntax declaration - forms that already cover most common situations fairly well.% + forms that already cover many common situations fairly well.% \end{isamarkuptext}% \isamarkuptrue% % @@ -35,8 +35,8 @@ directly or indirectly, including \isacommand{consts}, \isacommand{constdefs}, or \isacommand{datatype} (for the constructor operations). Type-constructors may be annotated as - well, although this is less frequently encountered in practice - (\isa{{\isacharasterisk}} and \isa{{\isacharplus}} types may come to mind). + well, although this is less frequently encountered in practice (the + infix type \isa{{\isasymtimes}} comes to mind). Infix declarations\index{infix annotations} provide a useful special case of mixfixes, where users need not care about the full details @@ -58,35 +58,29 @@ as \isa{op\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}}; together with plain prefix application this turns \isa{xor\ A} into \isa{op\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ A}. - \medskip The string \isa{{\isachardoublequote}{\isacharbrackleft}{\isacharplus}{\isacharbrackright}{\isachardoublequote}} in the above annotation - refers to the bit of concrete syntax to represent the operator, + \medskip The keyword \isakeyword{infixl} specifies an infix operator + that is nested to the \emph{left}: in iterated applications the more + complex expression appears on the left-hand side: \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} specifies to nesting to the \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}}. In + contrast, a \emph{non-oriented} declaration via \isakeyword{infix} + would render \isa{A\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ B\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ C} illegal, but demand explicit + parentheses to indicate the intended grouping. + + The string \isa{{\isachardoublequote}{\isacharbrackleft}{\isacharplus}{\isacharbrackright}{\isachardoublequote}} in the above 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 (i.e.\ the syntactic priorities of the arguments and - result). - - As it happens, Isabelle/HOL already spends many popular combinations - of ASCII symbols for its own use, including both \isa{{\isacharplus}} and - \isa{{\isacharplus}{\isacharplus}}. Slightly more awkward combinations like the present - \isa{{\isacharbrackleft}{\isacharplus}{\isacharbrackright}} tend to be available for user extensions. The current - arrangement of inner syntax may be inspected via - \commdx{print\protect\_syntax}, albeit its output is enormous. + result). As it happens, Isabelle/HOL already uses up many popular + combinations of ASCII symbols for its own use, including both \isa{{\isacharplus}} and \isa{{\isacharplus}{\isacharplus}}. Slightly more awkward combinations like the + present \isa{{\isacharbrackleft}{\isacharplus}{\isacharbrackright}} tend to be available for user extensions. Operator precedence also needs some special considerations. The admissible range is 0--1000. Very low or high priorities are basically reserved for the meta-logic. Syntax of Isabelle/HOL mainly uses the range of 10--100: the equality infix \isa{{\isacharequal}} is centered at 50, logical connectives (like \isa{{\isasymor}} and \isa{{\isasymand}}) are below 50, and algebraic ones (like \isa{{\isacharplus}} and \isa{{\isacharasterisk}}) above 50. User syntax should strive to coexist with common - HOL forms, or use the mostly unused range 100--900. - - The keyword \isakeyword{infixl} specifies an infix operator that is - nested to the \emph{left}: in iterated applications the more complex - expression appears on the left-hand side: \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} specifies to nesting to the \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}}. In - contrast, a \emph{non-oriented} declaration via \isakeyword{infix} - would render \isa{A\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ B\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ C} illegal, but demand explicit - parentheses to indicate the intended grouping.% + HOL forms, or use the mostly unused range 100--900.% \end{isamarkuptext}% \isamarkuptrue% % @@ -119,7 +113,7 @@ interpretation is left to further front-end tools. For example, both the user-interface of Proof~General + X-Symbol and the Isabelle document processor (see \S\ref{sec:document-preparation}) display - the \verb,\,\verb,, symbol really as \isa{{\isasymforall}}. + the \verb,\,\verb,, symbol as \isa{{\isasymforall}}. A list of standard Isabelle symbols is given in \cite[appendix~A]{isabelle-sys}. Users may introduce their own @@ -169,41 +163,28 @@ % \begin{isamarkuptext}% The \commdx{syntax} command introduced here acts like - \isakeyword{consts}, but without declaring a logical constant; an - optional print mode specification may be given, too. Note that the - type declaration given above merely serves for syntactic purposes, - and is not checked for consistency with the real constant. + \isakeyword{consts}, but without declaring a logical constant. The + print mode specification (here \isa{{\isacharparenleft}xsymbols{\isacharparenright}}) limits the + effect of the syntax annotation concerning output; that alternative + production available for input invariably. Also note that the type + declaration in \isakeyword{syntax} merely serves for syntactic + purposes, and is \emph{not} checked for consistency with the real + constant. \medskip We may now write \isa{A\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ B} or \isa{A\ {\isasymoplus}\ B} in input, while output uses the nicer syntax of $xsymbols$, provided that print mode is active. Such an arrangement is particularly useful for interactive development, where users may type plain ASCII - text, but gain improved visual feedback from the system. - - \begin{warn} - Alternative syntax declarations are apt to result in varying - occurrences of concrete syntax in the input sources. Isabelle - provides no systematic way to convert alternative syntax expressions - back and forth; print modes only affect situations where formal - entities are pretty printed by the Isabelle process (e.g.\ output of - terms and types), but not the original theory text. - \end{warn} - - \medskip The following variant makes the alternative \isa{{\isasymoplus}} - notation only available for output. Thus we may enforce input - sources to refer to plain ASCII only, but effectively disable - cut-and-paste from output at the same time.% + text, but gain improved visual feedback from the system.% \end{isamarkuptext}% \isamarkuptrue% -\isacommand{syntax}\ {\isacharparenleft}xsymbols\ \isakeyword{output}{\isacharparenright}\isanewline -\ \ xor\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}bool\ {\isasymRightarrow}\ bool\ {\isasymRightarrow}\ bool{\isachardoublequote}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequote}{\isasymoplus}{\isasymignore}{\isachardoublequote}\ {\isadigit{6}}{\isadigit{0}}{\isacharparenright}\isamarkupfalse% % \isamarkupsubsection{Prefix Annotations% } \isamarkuptrue% % \begin{isamarkuptext}% -Prefix syntax annotations\index{prefix annotation} are just another +Prefix syntax annotations\index{prefix annotation} are another degenerate form of mixfixes \cite{isabelle-ref}, without any template arguments or priorities --- just some bits of literal syntax. The following example illustrates this idea idea by @@ -222,8 +203,9 @@ \verb,\,\verb,,, \verb,\,\verb,,, and \verb,$,. Recall that a constructor like \isa{Euro} actually is a function \isa{nat\ {\isasymRightarrow}\ currency}. An expression like \isa{Euro\ {\isadigit{1}}{\isadigit{0}}} will be printed as \isa{{\isasymeuro}\ {\isadigit{1}}{\isadigit{0}}}; only the head of the application is - subject to our concrete syntax. This simple form already achieves - conformance with notational standards of the European Commission. + subject to our concrete syntax. This rather simple form already + achieves conformance with notational standards of the European + Commission. Prefix syntax also works for plain \isakeyword{consts} or \isakeyword{constdefs}, of course.% @@ -237,21 +219,21 @@ \begin{isamarkuptext}% Mixfix syntax annotations work well in those situations where particular constant application forms need to be decorated by - concrete syntax; just reconsider \isa{xor\ A\ B} versus \isa{A\ {\isasymoplus}\ B} covered before. Occasionally the relationship between some - piece of notation and its internal form is slightly more involved. - Here the concept of \bfindex{syntax translations} enters the scene. + concrete syntax; e.g.\ \isa{xor\ A\ B} versus \isa{A\ {\isasymoplus}\ B} + covered before. Occasionally the relationship between some piece of + notation and its internal form is slightly more involved. Here the + concept of \bfindex{syntax translations} enters the scene. Using the raw \isakeyword{syntax}\index{syntax (command)} command we may introduce uninterpreted notational elements, while - \commdx{translations} relates input forms with more complex logical + \commdx{translations} relate input forms with more complex logical expressions. This essentially provides a simple mechanism for syntactic macros; even heavier transformations may be written in ML \cite{isabelle-ref}. \medskip A typical example of syntax translations is to decorate - relational expressions (i.e.\ set-membership of tuples) with - handsome symbolic notation, such as \isa{{\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}\ {\isasymin}\ sim} versus - \isa{x\ {\isasymapprox}\ y}.% + relational expressions (i.e.\ set-membership of tuples) with nice + symbolic notation, such as \isa{{\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}\ {\isasymin}\ sim} versus \isa{x\ {\isasymapprox}\ y}.% \end{isamarkuptext}% \isamarkuptrue% \isacommand{consts}\isanewline @@ -310,16 +292,6 @@ sections, intermediate explanations, definitions, theorems and proofs. - The Isar proof language \cite{Wenzel-PhD}, which is not covered in - this book, admits to write formal proof texts that are acceptable - both to the machine and human readers at the same time. Thus - marginal comments and explanations may be kept at a minimum. Even - without proper coverage of human-readable proofs, Isabelle document - preparation is very useful to produce formally derived texts. - Unstructured proof scripts given here may be just ignored by - readers, or intentionally suppressed from the text by the writer - (see also \S\ref{sec:doc-prep-suppress}). - \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 @@ -337,7 +309,7 @@ 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 theory source files that may contribute to an output document + of source files that may contribute to an output document eventually. 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 @@ -358,14 +330,14 @@ The \texttt{isatool 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 that stage usually indicates + of contents etc.). Any failure at this stage usually indicates technical problems of the {\LaTeX} installation.\footnote{Especially make sure that \texttt{pdflatex} is present; if all fails one may fall back on DVI output by changing \texttt{usedir} options in \texttt{IsaMakefile} \cite{isabelle-sys}.} \medskip The detailed arrangement of the session sources is as - follows: + follows; advanced \begin{itemize} @@ -383,9 +355,9 @@ 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. The generated - \texttt{session.tex} will contain {\LaTeX} commands to include all - generated files in topologically sorted order, so + 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 \texttt{root.tex} does the job in most situations. @@ -407,9 +379,9 @@ Especially observe the included {\LaTeX} packages \texttt{isabelle} (mandatory), \texttt{isabellesym} (required for mathematical - symbols), and the final \texttt{pdfsetup} (provides handsome - defaults for \texttt{hyperref}, including URL markup) --- all three - are distributed with Isabelle. Further packages may be required in + 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, e.g.\ for unusual mathematical symbols. \medskip Additional files for the {\LaTeX} stage may be put into the @@ -501,10 +473,10 @@ \renewcommand{\isamarkupheader}[1]{\chapter{#1}} \end{verbatim} - \noindent Certainly, this requires to change the default - \verb,\documentclass{article}, in \texttt{root.tex} to something - that supports the notion of chapters in the first place, e.g.\ - \verb,\documentclass{report},. + \noindent That particular modification requires to change the + default \verb,\documentclass{article}, in \texttt{root.tex} to + something that supports the notion of chapters in the first place, + such as \verb,\documentclass{report},. \medskip The {\LaTeX} macro \verb,\isabellecontext, is maintained to hold the name of the current theory context. This is particularly @@ -590,7 +562,7 @@ an informal portion. The interpretation of antiquotations is limited to some well-formedness checks, with the result being pretty printed to the resulting document. So quoted text blocks together - with antiquotations provide very handsome means to reference formal + with antiquotations provide very useful means to reference formal entities with good confidence in getting the technical details right (especially syntax and types). @@ -640,7 +612,7 @@ \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 validity of fact $a$, print its name \\ + \texttt{\at}\verb,{thm [source],~$a$\verb,}, & check availability of fact, print name $a$ \\ \texttt{\at}\verb,{text,~$s$\verb,}, & print uninterpreted text $s$ \\ \end{tabular} @@ -708,10 +680,9 @@ 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 usually be the default - style for real production work that gets distributed to a broader - audience.% + 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% % @@ -721,14 +692,14 @@ % \begin{isamarkuptext}% By default, Isabelle's document system generates a {\LaTeX} source - file for each theory that happens to get 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 - include individual files in \texttt{root.tex} by hand. On the other - hand, such an arrangement requires additional maintenance chores - whenever the collection of theories changes. + 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 include + individual files in \texttt{root.tex} by hand. On the other hand, + such an arrangement requires additional maintenance chores 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 @@ -793,11 +764,11 @@ arbitrary axioms etc.) that have been hidden from sight beforehand. Authentic reports of formal theories, say as part of a library, - usually should refrain from suppressing parts of the text at all. - Other users may need the full information for their own derivative - work. If a particular formalization appears inadequate for general - public coverage, it is often more appropriate to think of a better - way in the first place. + should refrain from suppressing parts of the text at all. Other + users may need the full information for their own derivative work. + If a particular formalization appears inadequate for general public + coverage, it is often more appropriate to think of a better way in + the first place. \medskip Some technical subtleties of the \verb,(,\verb,*,\verb,<,\verb,*,\verb,),~\verb,(,\verb,*,\verb,>,\verb,*,\verb,), diff -r 83cd2140977d -r 46e3ef8dd9ea doc-src/TutorialI/Documents/documents.tex --- a/doc-src/TutorialI/Documents/documents.tex Mon Jan 14 00:16:43 2002 +0100 +++ b/doc-src/TutorialI/Documents/documents.tex Mon Jan 14 14:39:22 2002 +0100 @@ -2,18 +2,19 @@ \chapter{Presenting Theories} \label{ch:thy-present} -Due to the previous chapters the reader should have become sufficiently -acquainted with elementary theory development in Isabelle/HOL. The following -interlude covers the seemingly ``marginal'' issue of presenting theories in a -typographically pleasing manner. Isabelle provides a rich infrastructure for -concrete syntax of the underlying $\lambda$-calculus language, as well as -document preparation of theory texts based on existing PDF-{\LaTeX} -technology. +By now the reader should have become sufficiently acquainted with elementary +theory development in Isabelle/HOL. The following interlude covers the +seemingly ``marginal'' issue of presenting theories in a typographically +pleasing manner. Isabelle provides a rich infrastructure for concrete syntax +of the underlying $\lambda$-calculus language (see +\S\ref{sec:concrete-syntax}), as well as document preparation of theory texts +based on existing PDF-{\LaTeX} technology (see +\S\ref{sec:document-preparation}). -As has been pointed out by Leibniz\index{Leibniz, Gottfried Wilhelm} more than -300 years ago, \emph{notions} are in principle more important than -\emph{notations}, but fair textual representation of ideas is vital to reduce -the mental effort in actual applications. +As pointed out by Leibniz\index{Leibniz, Gottfried Wilhelm} more than 300 +years ago, \emph{notions} are in principle more important than +\emph{notations}, but suggestive textual representation of ideas is vital to +reduce the mental effort to comprehend and apply them. \input{Documents/document/Documents.tex}