diff -r c04001b3a753 -r 12afbf6eb7f9 doc-src/IsarRef/Document_Preparation.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/doc-src/IsarRef/Document_Preparation.thy Tue Aug 28 12:45:49 2012 +0200 @@ -0,0 +1,611 @@ +theory Document_Preparation +imports Base Main +begin + +chapter {* Document preparation \label{ch:document-prep} *} + +text {* Isabelle/Isar provides a simple document preparation system + based on regular {PDF-\LaTeX} technology, with full support for + hyper-links and bookmarks. Thus the results are well suited for WWW + browsing and as printed copies. + + \medskip Isabelle generates {\LaTeX} output while running a + \emph{logic session} (see also \cite{isabelle-sys}). Getting + started with a working configuration for common situations is quite + easy by using the Isabelle @{verbatim mkdir} and @{verbatim make} + tools. First invoke +\begin{ttbox} + isabelle mkdir Foo +\end{ttbox} + to initialize a separate directory for session @{verbatim Foo} (it + is safe to experiment, since @{verbatim "isabelle mkdir"} never + overwrites existing files). Ensure that @{verbatim "Foo/ROOT.ML"} + holds ML commands to load all theories required for this session; + furthermore @{verbatim "Foo/document/root.tex"} should include any + special {\LaTeX} macro packages required for your document (the + default is usually sufficient as a start). + + The session is controlled by a separate @{verbatim IsaMakefile} + (with crude source dependencies by default). This file is located + one level up from the @{verbatim Foo} directory location. Now + invoke +\begin{ttbox} + isabelle make Foo +\end{ttbox} + to run the @{verbatim Foo} session, with browser information and + document preparation enabled. Unless any errors are reported by + Isabelle or {\LaTeX}, the output will appear inside the directory + defined by the @{verbatim ISABELLE_BROWSER_INFO} setting (as + reported by the batch job in verbose mode). + + \medskip You may also consider to tune the @{verbatim usedir} + options in @{verbatim IsaMakefile}, for example to switch the output + format between @{verbatim pdf} and @{verbatim dvi}, or activate the + @{verbatim "-D"} option to retain a second copy of the generated + {\LaTeX} sources (for manual inspection or separate runs of + @{executable latex}). + + \medskip See \emph{The Isabelle System Manual} \cite{isabelle-sys} + for further details on Isabelle logic sessions and theory + presentation. The Isabelle/HOL tutorial \cite{isabelle-hol-book} + also covers theory presentation to some extent. +*} + + +section {* Markup commands \label{sec:markup} *} + +text {* + \begin{matharray}{rcl} + @{command_def "header"} & : & @{text "toplevel \ toplevel"} \\[0.5ex] + @{command_def "chapter"} & : & @{text "local_theory \ local_theory"} \\ + @{command_def "section"} & : & @{text "local_theory \ local_theory"} \\ + @{command_def "subsection"} & : & @{text "local_theory \ local_theory"} \\ + @{command_def "subsubsection"} & : & @{text "local_theory \ local_theory"} \\ + @{command_def "text"} & : & @{text "local_theory \ local_theory"} \\ + @{command_def "text_raw"} & : & @{text "local_theory \ local_theory"} \\[0.5ex] + @{command_def "sect"} & : & @{text "proof \ proof"} \\ + @{command_def "subsect"} & : & @{text "proof \ proof"} \\ + @{command_def "subsubsect"} & : & @{text "proof \ proof"} \\ + @{command_def "txt"} & : & @{text "proof \ proof"} \\ + @{command_def "txt_raw"} & : & @{text "proof \ proof"} \\ + \end{matharray} + + Markup commands provide a structured way to insert text into the + document generated from a theory. Each markup command takes a + single @{syntax text} argument, which is passed as argument to a + corresponding {\LaTeX} macro. The default macros provided by + @{file "~~/lib/texinputs/isabelle.sty"} can be redefined according + to the needs of the underlying document and {\LaTeX} styles. + + Note that formal comments (\secref{sec:comments}) are similar to + markup commands, but have a different status within Isabelle/Isar + syntax. + + @{rail " + (@@{command chapter} | @@{command section} | @@{command subsection} | + @@{command subsubsection} | @@{command text}) @{syntax target}? @{syntax text} + ; + (@@{command header} | @@{command text_raw} | @@{command sect} | @@{command subsect} | + @@{command subsubsect} | @@{command txt} | @@{command txt_raw}) @{syntax text} + "} + + \begin{description} + + \item @{command header} provides plain text markup just preceding + the formal beginning of a theory. The corresponding {\LaTeX} macro + is @{verbatim "\\isamarkupheader"}, which acts like @{command + section} by default. + + \item @{command chapter}, @{command section}, @{command subsection}, + and @{command subsubsection} mark chapter and section headings + within the main theory body or local theory targets. The + corresponding {\LaTeX} macros are @{verbatim "\\isamarkupchapter"}, + @{verbatim "\\isamarkupsection"}, @{verbatim + "\\isamarkupsubsection"} etc. + + \item @{command sect}, @{command subsect}, and @{command subsubsect} + mark section headings within proofs. The corresponding {\LaTeX} + macros are @{verbatim "\\isamarkupsect"}, @{verbatim + "\\isamarkupsubsect"} etc. + + \item @{command text} and @{command txt} specify paragraphs of plain + text. This corresponds to a {\LaTeX} environment @{verbatim + "\\begin{isamarkuptext}"} @{text "\"} @{verbatim + "\\end{isamarkuptext}"} etc. + + \item @{command text_raw} and @{command txt_raw} insert {\LaTeX} + source into the output, without additional markup. Thus the full + range of document manipulations becomes available, at the risk of + messing up document output. + + \end{description} + + Except for @{command "text_raw"} and @{command "txt_raw"}, the text + passed to any of the above markup commands may refer to formal + entities via \emph{document antiquotations}, see also + \secref{sec:antiq}. These are interpreted in the present theory or + proof context, or the named @{text "target"}. + + \medskip The proof markup commands closely resemble those for theory + specifications, but have a different formal status and produce + different {\LaTeX} macros. The default definitions coincide for + analogous commands such as @{command section} and @{command sect}. +*} + + +section {* Document Antiquotations \label{sec:antiq} *} + +text {* + \begin{matharray}{rcl} + @{antiquotation_def "theory"} & : & @{text antiquotation} \\ + @{antiquotation_def "thm"} & : & @{text antiquotation} \\ + @{antiquotation_def "lemma"} & : & @{text antiquotation} \\ + @{antiquotation_def "prop"} & : & @{text antiquotation} \\ + @{antiquotation_def "term"} & : & @{text antiquotation} \\ + @{antiquotation_def term_type} & : & @{text antiquotation} \\ + @{antiquotation_def typeof} & : & @{text antiquotation} \\ + @{antiquotation_def const} & : & @{text antiquotation} \\ + @{antiquotation_def abbrev} & : & @{text antiquotation} \\ + @{antiquotation_def typ} & : & @{text antiquotation} \\ + @{antiquotation_def type} & : & @{text antiquotation} \\ + @{antiquotation_def class} & : & @{text antiquotation} \\ + @{antiquotation_def "text"} & : & @{text antiquotation} \\ + @{antiquotation_def goals} & : & @{text antiquotation} \\ + @{antiquotation_def subgoals} & : & @{text antiquotation} \\ + @{antiquotation_def prf} & : & @{text antiquotation} \\ + @{antiquotation_def full_prf} & : & @{text antiquotation} \\ + @{antiquotation_def ML} & : & @{text antiquotation} \\ + @{antiquotation_def ML_op} & : & @{text antiquotation} \\ + @{antiquotation_def ML_type} & : & @{text antiquotation} \\ + @{antiquotation_def ML_struct} & : & @{text antiquotation} \\ + @{antiquotation_def "file"} & : & @{text antiquotation} \\ + \end{matharray} + + The overall content of an Isabelle/Isar theory may alternate between + formal and informal text. The main body consists of formal + specification and proof commands, interspersed with markup commands + (\secref{sec:markup}) or document comments (\secref{sec:comments}). + The argument of markup commands quotes informal text to be printed + in the resulting document, but may again refer to formal entities + via \emph{document antiquotations}. + + For example, embedding of ``@{text [source=false] "@{term [show_types] \"f x = a + x\"}"}'' + within a text block makes + \isa{{\isacharparenleft}f{\isasymColon}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isacharparenright}\ {\isacharparenleft}x{\isasymColon}{\isacharprime}a{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}a{\isasymColon}{\isacharprime}a{\isacharparenright}\ {\isacharplus}\ x} appear in the final {\LaTeX} document. + + Antiquotations usually spare the author tedious typing of logical + entities in full detail. Even more importantly, some degree of + consistency-checking between the main body of formal text and its + informal explanation is achieved, since terms and types appearing in + antiquotations are checked within the current theory or proof + context. + + %% FIXME less monolithic presentation, move to individual sections!? + @{rail " + '@{' antiquotation '}' + ; + @{syntax_def antiquotation}: + @@{antiquotation theory} options @{syntax name} | + @@{antiquotation thm} options styles @{syntax thmrefs} | + @@{antiquotation lemma} options @{syntax prop} @'by' @{syntax method} @{syntax method}? | + @@{antiquotation prop} options styles @{syntax prop} | + @@{antiquotation term} options styles @{syntax term} | + @@{antiquotation (HOL) value} options styles @{syntax term} | + @@{antiquotation term_type} options styles @{syntax term} | + @@{antiquotation typeof} options styles @{syntax term} | + @@{antiquotation const} options @{syntax term} | + @@{antiquotation abbrev} options @{syntax term} | + @@{antiquotation typ} options @{syntax type} | + @@{antiquotation type} options @{syntax name} | + @@{antiquotation class} options @{syntax name} | + @@{antiquotation text} options @{syntax name} + ; + @{syntax antiquotation}: + @@{antiquotation goals} options | + @@{antiquotation subgoals} options | + @@{antiquotation prf} options @{syntax thmrefs} | + @@{antiquotation full_prf} options @{syntax thmrefs} | + @@{antiquotation ML} options @{syntax name} | + @@{antiquotation ML_op} options @{syntax name} | + @@{antiquotation ML_type} options @{syntax name} | + @@{antiquotation ML_struct} options @{syntax name} | + @@{antiquotation \"file\"} options @{syntax name} + ; + options: '[' (option * ',') ']' + ; + option: @{syntax name} | @{syntax name} '=' @{syntax name} + ; + styles: '(' (style + ',') ')' + ; + style: (@{syntax name} +) + "} + + Note that the syntax of antiquotations may \emph{not} include source + comments @{verbatim "(*"}~@{text "\"}~@{verbatim "*)"} nor verbatim + text @{verbatim "{"}@{verbatim "*"}~@{text "\"}~@{verbatim + "*"}@{verbatim "}"}. + + \begin{description} + + \item @{text "@{theory A}"} prints the name @{text "A"}, which is + guaranteed to refer to a valid ancestor theory in the current + context. + + \item @{text "@{thm a\<^sub>1 \ a\<^sub>n}"} prints theorems @{text "a\<^sub>1 \ a\<^sub>n"}. + Full fact expressions are allowed here, including attributes + (\secref{sec:syn-att}). + + \item @{text "@{prop \}"} prints a well-typed proposition @{text + "\"}. + + \item @{text "@{lemma \ by m}"} proves a well-typed proposition + @{text "\"} by method @{text m} and prints the original @{text "\"}. + + \item @{text "@{term t}"} prints a well-typed term @{text "t"}. + + \item @{text "@{value t}"} evaluates a term @{text "t"} and prints + its result, see also @{command_ref (HOL) value}. + + \item @{text "@{term_type t}"} prints a well-typed term @{text "t"} + annotated with its type. + + \item @{text "@{typeof t}"} prints the type of a well-typed term + @{text "t"}. + + \item @{text "@{const c}"} prints a logical or syntactic constant + @{text "c"}. + + \item @{text "@{abbrev c x\<^sub>1 \ x\<^sub>n}"} prints a constant abbreviation + @{text "c x\<^sub>1 \ x\<^sub>n \ rhs"} as defined in the current context. + + \item @{text "@{typ \}"} prints a well-formed type @{text "\"}. + + \item @{text "@{type \}"} prints a (logical or syntactic) type + constructor @{text "\"}. + + \item @{text "@{class c}"} prints a class @{text c}. + + \item @{text "@{text s}"} prints uninterpreted source text @{text + s}. This is particularly useful to print portions of text according + to the Isabelle document style, without demanding well-formedness, + e.g.\ small pieces of terms that should not be parsed or + type-checked yet. + + \item @{text "@{goals}"} prints the current \emph{dynamic} goal + state. This is mainly for support of tactic-emulation scripts + within Isar. Presentation of goal states does not conform to the + idea of human-readable proof documents! + + When explaining proofs in detail it is usually better to spell out + the reasoning via proper Isar proof commands, instead of peeking at + the internal machine configuration. + + \item @{text "@{subgoals}"} is similar to @{text "@{goals}"}, but + does not print the main goal. + + \item @{text "@{prf a\<^sub>1 \ a\<^sub>n}"} prints the (compact) proof terms + corresponding to the theorems @{text "a\<^sub>1 \ a\<^sub>n"}. Note that this + requires proof terms to be switched on for the current logic + session. + + \item @{text "@{full_prf a\<^sub>1 \ a\<^sub>n}"} is like @{text "@{prf a\<^sub>1 \ + a\<^sub>n}"}, but prints the full proof terms, i.e.\ also displays + information omitted in the compact proof term, which is denoted by + ``@{text _}'' placeholders there. + + \item @{text "@{ML s}"}, @{text "@{ML_op s}"}, @{text "@{ML_type + s}"}, and @{text "@{ML_struct s}"} check text @{text s} as ML value, + infix operator, type, and structure, respectively. The source is + printed verbatim. + + \item @{text "@{file path}"} checks that @{text "path"} refers to a + file (or directory) and prints it verbatim. + + \end{description} +*} + + +subsection {* Styled antiquotations *} + +text {* The antiquotations @{text thm}, @{text prop} and @{text + term} admit an extra \emph{style} specification to modify the + printed result. A style is specified by a name with a possibly + empty number of arguments; multiple styles can be sequenced with + commas. The following standard styles are available: + + \begin{description} + + \item @{text lhs} extracts the first argument of any application + form with at least two arguments --- typically meta-level or + object-level equality, or any other binary relation. + + \item @{text rhs} is like @{text lhs}, but extracts the second + argument. + + \item @{text "concl"} extracts the conclusion @{text C} from a rule + in Horn-clause normal form @{text "A\<^sub>1 \ \ A\<^sub>n \ C"}. + + \item @{text "prem"} @{text n} extract premise number + @{text "n"} from from a rule in Horn-clause + normal form @{text "A\<^sub>1 \ \ A\<^sub>n \ C"} + + \end{description} +*} + + +subsection {* General options *} + +text {* The following options are available to tune the printed output + of antiquotations. Note that many of these coincide with global ML + flags of the same names. + + \begin{description} + + \item @{antiquotation_option_def show_types}~@{text "= bool"} and + @{antiquotation_option_def show_sorts}~@{text "= bool"} control + printing of explicit type and sort constraints. + + \item @{antiquotation_option_def show_structs}~@{text "= bool"} + controls printing of implicit structures. + + \item @{antiquotation_option_def show_abbrevs}~@{text "= bool"} + controls folding of abbreviations. + + \item @{antiquotation_option_def names_long}~@{text "= bool"} forces + names of types and constants etc.\ to be printed in their fully + qualified internal form. + + \item @{antiquotation_option_def names_short}~@{text "= bool"} + forces names of types and constants etc.\ to be printed unqualified. + Note that internalizing the output again in the current context may + well yield a different result. + + \item @{antiquotation_option_def names_unique}~@{text "= bool"} + determines whether the printed version of qualified names should be + made sufficiently long to avoid overlap with names declared further + back. Set to @{text false} for more concise output. + + \item @{antiquotation_option_def eta_contract}~@{text "= bool"} + prints terms in @{text \}-contracted form. + + \item @{antiquotation_option_def display}~@{text "= bool"} indicates + if the text is to be output as multi-line ``display material'', + rather than a small piece of text without line breaks (which is the + default). + + In this mode the embedded entities are printed in the same style as + the main theory text. + + \item @{antiquotation_option_def break}~@{text "= bool"} controls + line breaks in non-display material. + + \item @{antiquotation_option_def quotes}~@{text "= bool"} indicates + if the output should be enclosed in double quotes. + + \item @{antiquotation_option_def mode}~@{text "= name"} adds @{text + name} to the print mode to be used for presentation. Note that the + standard setup for {\LaTeX} output is already present by default, + including the modes @{text latex} and @{text xsymbols}. + + \item @{antiquotation_option_def margin}~@{text "= nat"} and + @{antiquotation_option_def indent}~@{text "= nat"} change the margin + or indentation for pretty printing of display material. + + \item @{antiquotation_option_def goals_limit}~@{text "= nat"} + determines the maximum number of goals to be printed (for goal-based + antiquotation). + + \item @{antiquotation_option_def source}~@{text "= bool"} prints the + original source text of the antiquotation arguments, rather than its + internal representation. Note that formal checking of + @{antiquotation "thm"}, @{antiquotation "term"}, etc. is still + enabled; use the @{antiquotation "text"} antiquotation for unchecked + output. + + Regular @{text "term"} and @{text "typ"} antiquotations with @{text + "source = false"} involve a full round-trip from the original source + to an internalized logical entity back to a source form, according + to the syntax of the current context. Thus the printed output is + not under direct control of the author, it may even fluctuate a bit + as the underlying theory is changed later on. + + In contrast, @{antiquotation_option source}~@{text "= true"} + admits direct printing of the given source text, with the desirable + well-formedness check in the background, but without modification of + the printed text. + + \end{description} + + For boolean flags, ``@{text "name = true"}'' may be abbreviated as + ``@{text name}''. All of the above flags are disabled by default, + unless changed from ML, say in the @{verbatim "ROOT.ML"} of the + logic session. +*} + + +section {* Markup via command tags \label{sec:tags} *} + +text {* Each Isabelle/Isar command may be decorated by additional + presentation tags, to indicate some modification in the way it is + printed in the document. + + @{rail " + @{syntax_def tags}: ( tag * ) + ; + tag: '%' (@{syntax ident} | @{syntax string}) + "} + + Some tags are pre-declared for certain classes of commands, serving + as default markup if no tags are given in the text: + + \medskip + \begin{tabular}{ll} + @{text "theory"} & theory begin/end \\ + @{text "proof"} & all proof commands \\ + @{text "ML"} & all commands involving ML code \\ + \end{tabular} + + \medskip The Isabelle document preparation system + \cite{isabelle-sys} allows tagged command regions to be presented + specifically, e.g.\ to fold proof texts, or drop parts of the text + completely. + + For example ``@{command "by"}~@{text "%invisible auto"}'' causes + that piece of proof to be treated as @{text invisible} instead of + @{text "proof"} (the default), which may be shown or hidden + depending on the document setup. In contrast, ``@{command + "by"}~@{text "%visible auto"}'' forces this text to be shown + invariably. + + Explicit tag specifications within a proof apply to all subsequent + commands of the same level of nesting. For example, ``@{command + "proof"}~@{text "%visible \"}~@{command "qed"}'' forces the whole + sub-proof to be typeset as @{text visible} (unless some of its parts + are tagged differently). + + \medskip Command tags merely produce certain markup environments for + type-setting. The meaning of these is determined by {\LaTeX} + macros, as defined in @{file "~~/lib/texinputs/isabelle.sty"} or + by the document author. The Isabelle document preparation tools + also provide some high-level options to specify the meaning of + arbitrary tags to ``keep'', ``drop'', or ``fold'' the corresponding + parts of the text. Logic sessions may also specify ``document + versions'', where given tags are interpreted in some particular way. + Again see \cite{isabelle-sys} for further details. +*} + + +section {* Railroad diagrams *} + +text {* + \begin{matharray}{rcl} + @{antiquotation_def "rail"} & : & @{text antiquotation} \\ + \end{matharray} + + @{rail "'rail' string"} + + The @{antiquotation rail} antiquotation allows to include syntax + diagrams into Isabelle documents. {\LaTeX} requires the style file + @{"file" "~~/lib/texinputs/pdfsetup.sty"}, which can be used via + @{verbatim "\\usepackage{pdfsetup}"} in @{verbatim "root.tex"}, for + example. + + The rail specification language is quoted here as Isabelle @{syntax + string}; it has its own grammar given below. + + @{rail " + rule? + ';' + ; + rule: ((identifier | @{syntax antiquotation}) ':')? body + ; + body: concatenation + '|' + ; + concatenation: ((atom '?'?) +) (('*' | '+') atom?)? + ; + atom: '(' body? ')' | identifier | + '@'? (string | @{syntax antiquotation}) | + '\\\\\\\\' + "} + + The lexical syntax of @{text "identifier"} coincides with that of + @{syntax ident} in regular Isabelle syntax, but @{text string} uses + single quotes instead of double quotes of the standard @{syntax + string} category, to avoid extra escapes. + + Each @{text rule} defines a formal language (with optional name), + using a notation that is similar to EBNF or regular expressions with + recursion. The meaning and visual appearance of these rail language + elements is illustrated by the following representative examples. + + \begin{itemize} + + \item Empty @{verbatim "()"} + + @{rail "()"} + + \item Nonterminal @{verbatim "A"} + + @{rail "A"} + + \item Nonterminal via Isabelle antiquotation + @{verbatim "@{syntax method}"} + + @{rail "@{syntax method}"} + + \item Terminal @{verbatim "'xyz'"} + + @{rail "'xyz'"} + + \item Terminal in keyword style @{verbatim "@'xyz'"} + + @{rail "@'xyz'"} + + \item Terminal via Isabelle antiquotation + @{verbatim "@@{method rule}"} + + @{rail "@@{method rule}"} + + \item Concatenation @{verbatim "A B C"} + + @{rail "A B C"} + + \item Linebreak @{verbatim "\\\\"} inside + concatenation\footnote{Strictly speaking, this is only a single + backslash, but the enclosing @{syntax string} syntax requires a + second one for escaping.} @{verbatim "A B C \\\\ D E F"} + + @{rail "A B C \\ D E F"} + + \item Variants @{verbatim "A | B | C"} + + @{rail "A | B | C"} + + \item Option @{verbatim "A ?"} + + @{rail "A ?"} + + \item Repetition @{verbatim "A *"} + + @{rail "A *"} + + \item Repetition with separator @{verbatim "A * sep"} + + @{rail "A * sep"} + + \item Strict repetition @{verbatim "A +"} + + @{rail "A +"} + + \item Strict repetition with separator @{verbatim "A + sep"} + + @{rail "A + sep"} + + \end{itemize} +*} + + +section {* Draft presentation *} + +text {* + \begin{matharray}{rcl} + @{command_def "display_drafts"}@{text "\<^sup>*"} & : & @{text "any \"} \\ + @{command_def "print_drafts"}@{text "\<^sup>*"} & : & @{text "any \"} \\ + \end{matharray} + + @{rail " + (@@{command display_drafts} | @@{command print_drafts}) (@{syntax name} +) + + "} + + \begin{description} + + \item @{command "display_drafts"}~@{text paths} and @{command + "print_drafts"}~@{text paths} perform simple output of a given list + of raw source files. Only those symbols that do not require + additional {\LaTeX} packages are displayed properly, everything else + is left verbatim. + + \end{description} +*} + +end