diff -r 14582233d36b -r 3d3e6e07b931 doc-src/IsarRef/Thy/Outer_Syntax.thy --- a/doc-src/IsarRef/Thy/Outer_Syntax.thy Mon Jun 02 22:50:21 2008 +0200 +++ b/doc-src/IsarRef/Thy/Outer_Syntax.thy Mon Jun 02 22:50:23 2008 +0200 @@ -4,7 +4,7 @@ imports Pure begin -chapter {* Syntax primitives *} +chapter {* Outer syntax *} text {* The rather generic framework of Isabelle/Isar syntax emerges from @@ -468,283 +468,4 @@ \secref{sec:proof-context}. *} - -subsection {* Antiquotations \label{sec:antiq} *} - -text {* - \begin{matharray}{rcl} - @{antiquotation_def "theory"} & : & \isarantiq \\ - @{antiquotation_def "thm"} & : & \isarantiq \\ - @{antiquotation_def "prop"} & : & \isarantiq \\ - @{antiquotation_def "term"} & : & \isarantiq \\ - @{antiquotation_def const} & : & \isarantiq \\ - @{antiquotation_def abbrev} & : & \isarantiq \\ - @{antiquotation_def typeof} & : & \isarantiq \\ - @{antiquotation_def typ} & : & \isarantiq \\ - @{antiquotation_def thm_style} & : & \isarantiq \\ - @{antiquotation_def term_style} & : & \isarantiq \\ - @{antiquotation_def "text"} & : & \isarantiq \\ - @{antiquotation_def goals} & : & \isarantiq \\ - @{antiquotation_def subgoals} & : & \isarantiq \\ - @{antiquotation_def prf} & : & \isarantiq \\ - @{antiquotation_def full_prf} & : & \isarantiq \\ - @{antiquotation_def ML} & : & \isarantiq \\ - @{antiquotation_def ML_type} & : & \isarantiq \\ - @{antiquotation_def ML_struct} & : & \isarantiq \\ - \end{matharray} - - The text body of formal comments (see also \secref{sec:comments}) - may contain antiquotations of logical entities, such as theorems, - terms and types, which are to be presented in the final output - produced by the Isabelle document preparation system (see also - \secref{sec:document-prep}). - - Thus embedding of ``@{text "@{term [show_types] \"f x = a + x\"}"}'' - within a text block would cause - \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} to appear in the final {\LaTeX} document. Also note that theorem - antiquotations may involve attributes as well. For example, - @{text "@{thm sym [no_vars]}"} would print the theorem's - statement where all schematic variables have been replaced by fixed - ones, which are easier to read. - - \begin{rail} - atsign lbrace antiquotation rbrace - ; - - antiquotation: - 'theory' options name | - 'thm' options thmrefs | - 'prop' options prop | - 'term' options term | - 'const' options term | - 'abbrev' options term | - 'typeof' options term | - 'typ' options type | - 'thm\_style' options name thmref | - 'term\_style' options name term | - 'text' options name | - 'goals' options | - 'subgoals' options | - 'prf' options thmrefs | - 'full\_prf' options thmrefs | - 'ML' options name | - 'ML\_type' options name | - 'ML\_struct' options name - ; - options: '[' (option * ',') ']' - ; - option: name | name '=' name - ; - \end{rail} - - Note that the syntax of antiquotations may \emph{not} include source - comments @{verbatim "(*"}~@{text "\"}~@{verbatim "*)"} or verbatim - text @{verbatim "{"}@{verbatim "*"}~@{text "\"}~@{verbatim - "*"}@{verbatim "}"}. - - \begin{descr} - - \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"}. Note that attribute specifications - may be included as well (see also \secref{sec:syn-att}); the - @{attribute_ref no_vars} rule (see \secref{sec:misc-meth-att}) would - be particularly useful to suppress printing of schematic variables. - - \item [@{text "@{prop \}"}] prints a well-typed proposition @{text - "\"}. - - \item [@{text "@{term t}"}] prints 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 "@{typeof t}"}] prints the type of a well-typed term - @{text "t"}. - - \item [@{text "@{typ \}"}] prints a well-formed type @{text "\"}. - - \item [@{text "@{thm_style s a}"}] prints theorem @{text a}, - previously applying a style @{text s} to it (see below). - - \item [@{text "@{term_style s t}"}] prints a well-typed term @{text - t} after applying a style @{text s} to it (see below). - - \item [@{text "@{text s}"}] prints uninterpreted source text @{text - s}. This is particularly useful to print portions of text according - to the Isabelle {\LaTeX} output 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 - actual human-readable proof documents. - - Please do not include goal states into document output unless you - really know what you are doing! - - \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 object logic (see the ``Proof terms'' section of the - Isabelle reference manual for information on how to do this). - - \item [@{text "@{full_prf a\<^sub>1 \ a\<^sub>n}"}] is like @{text - "@{prf a\<^sub>1 \ a\<^sub>n}"}, but displays 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_type s}"}, and @{text - "@{ML_struct s}"}] check text @{text s} as ML value, type, and - structure, respectively. The source is displayed verbatim. - - \end{descr} - - \medskip The following standard styles for use with @{text - thm_style} and @{text term_style} are available: - - \begin{descr} - - \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 "prem1"}, \dots, @{text "prem9"}] extract premise - number @{text "1, \, 9"}, respectively, from from a rule in - Horn-clause normal form @{text "A\<^sub>1 \ \ A\<^sub>n \ C"} - - \end{descr} - - \medskip - The following options are available to tune the output. Note that most of - these coincide with ML flags of the same names (see also \cite{isabelle-ref}). - - \begin{descr} - - \item[@{text "show_types = bool"} and @{text "show_sorts = bool"}] - control printing of explicit type and sort constraints. - - \item[@{text "show_structs = bool"}] controls printing of implicit - structures. - - \item[@{text "long_names = bool"}] forces names of types and - constants etc.\ to be printed in their fully qualified internal - form. - - \item[@{text "short_names = 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[@{text "unique_names = 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[@{text "eta_contract = bool"}] prints terms in @{text - \}-contracted form. - - \item[@{text "display = 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). - - \item[@{text "break = bool"}] controls line breaks in non-display - material. - - \item[@{text "quotes = bool"}] indicates if the output should be - enclosed in double quotes. - - \item[@{text "mode = name"}] adds @{text name} to the print mode to - be used for presentation (see also \cite{isabelle-ref}). Note that - the standard setup for {\LaTeX} output is already present by - default, including the modes @{text latex} and @{text xsymbols}. - - \item[@{text "margin = nat"} and @{text "indent = nat"}] change the - margin or indentation for pretty printing of display material. - - \item[@{text "source = bool"}] prints the source text of the - antiquotation arguments, rather than the actual value. Note that - this does not affect well-formedness checks of @{antiquotation - "thm"}, @{antiquotation "term"}, etc. (only the @{antiquotation - "text"} antiquotation admits arbitrary output). - - \item[@{text "goals_limit = nat"}] determines the maximum number of - goals to be printed. - - \item[@{text "locale = name"}] specifies an alternative locale - context used for evaluating and printing the subsequent argument. - - \end{descr} - - 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. - - \medskip Note that antiquotations do not only spare the author from - tedious typing of logical entities, but also achieve some degree of - consistency-checking of informal explanations with formal - developments: well-formedness of terms and types with respect to the - current theory or proof context is ensured here. -*} - - -subsection {* Tagged commands \label{sec:tags} *} - -text {* - Each Isabelle/Isar command may be decorated by presentation tags: - - \indexouternonterm{tags} - \begin{rail} - tags: ( tag * ) - ; - tag: '\%' (ident | string) - \end{rail} - - The tags @{text "theory"}, @{text "proof"}, @{text "ML"} are already - pre-declared for certain classes of commands: - - \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 (see also - \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"}'' would - cause that piece of proof to be treated as @{text invisible} instead - of @{text "proof"} (the default), which may be either show or hidden - depending on the document setup. In contrast, ``@{command - "by"}~@{text "%visible auto"}'' would force 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"}'' would force the - whole sub-proof to be typeset as @{text visible} (unless some of its - parts are tagged differently). -*} - end