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,),