diff -r 220fb39be543 -r 33d95687514e doc-src/IsarRef/Thy/Outer_Syntax.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/doc-src/IsarRef/Thy/Outer_Syntax.thy Mon Jun 02 21:19:46 2008 +0200 @@ -0,0 +1,750 @@ +(* $Id$ *) + +theory Outer_Syntax +imports Pure +begin + +chapter {* Syntax primitives *} + +text {* + The rather generic framework of Isabelle/Isar syntax emerges from + three main syntactic categories: \emph{commands} of the top-level + Isar engine (covering theory and proof elements), \emph{methods} for + general goal refinements (analogous to traditional ``tactics''), and + \emph{attributes} for operations on facts (within a certain + context). Subsequently we give a reference of basic syntactic + entities underlying Isabelle/Isar syntax in a bottom-up manner. + Concrete theory and proof language elements will be introduced later + on. + + \medskip In order to get started with writing well-formed + Isabelle/Isar documents, the most important aspect to be noted is + the difference of \emph{inner} versus \emph{outer} syntax. Inner + syntax is that of Isabelle types and terms of the logic, while outer + syntax is that of Isabelle/Isar theory sources (specifications and + proofs). As a general rule, inner syntax entities may occur only as + \emph{atomic entities} within outer syntax. For example, the string + @{verbatim "\"x + y\""} and identifier @{verbatim z} are legal term + specifications within a theory, while @{verbatim "x + y"} without + quotes is not. + + Printed theory documents usually omit quotes to gain readability + (this is a matter of {\LaTeX} macro setup, say via @{verbatim + "\\isabellestyle"}, see also \cite{isabelle-sys}). Experienced + users of Isabelle/Isar may easily reconstruct the lost technical + information, while mere readers need not care about quotes at all. + + \medskip Isabelle/Isar input may contain any number of input + termination characters ``@{verbatim ";"}'' (semicolon) to separate + commands explicitly. This is particularly useful in interactive + shell sessions to make clear where the current command is intended + to end. Otherwise, the interpreter loop will continue to issue a + secondary prompt ``@{verbatim "#"}'' until an end-of-command is + clearly recognized from the input syntax, e.g.\ encounter of the + next command keyword. + + More advanced interfaces such as Proof~General \cite{proofgeneral} + do not require explicit semicolons, the amount of input text is + determined automatically by inspecting the present content of the + Emacs text buffer. In the printed presentation of Isabelle/Isar + documents semicolons are omitted altogether for readability. + + \begin{warn} + Proof~General requires certain syntax classification tables in + order to achieve properly synchronized interaction with the + Isabelle/Isar process. These tables need to be consistent with + the Isabelle version and particular logic image to be used in a + running session (common object-logics may well change the outer + syntax). The standard setup should work correctly with any of the + ``official'' logic images derived from Isabelle/HOL (including + HOLCF etc.). Users of alternative logics may need to tell + Proof~General explicitly, e.g.\ by giving an option @{verbatim "-k ZF"} + (in conjunction with @{verbatim "-l ZF"}, to specify the default + logic image). Note that option @{verbatim "-L"} does both + of this at the same time. + \end{warn} +*} + + +section {* Lexical matters \label{sec:lex-syntax} *} + +text {* + The Isabelle/Isar outer syntax provides token classes as presented + below; most of these coincide with the inner lexical syntax as + presented in \cite{isabelle-ref}. + + \begin{matharray}{rcl} + @{syntax_def ident} & = & letter\,quasiletter^* \\ + @{syntax_def longident} & = & ident (\verb,.,ident)^+ \\ + @{syntax_def symident} & = & sym^+ ~|~ \verb,\,\verb,<,ident\verb,>, \\ + @{syntax_def nat} & = & digit^+ \\ + @{syntax_def var} & = & ident ~|~ \verb,?,ident ~|~ \verb,?,ident\verb,.,nat \\ + @{syntax_def typefree} & = & \verb,',ident \\ + @{syntax_def typevar} & = & typefree ~|~ \verb,?,typefree ~|~ \verb,?,typefree\verb,.,nat \\ + @{syntax_def string} & = & \verb,", ~\dots~ \verb,", \\ + @{syntax_def altstring} & = & \backquote ~\dots~ \backquote \\ + @{syntax_def verbatim} & = & \verb,{*, ~\dots~ \verb,*,\verb,}, \\[1ex] + + letter & = & latin ~|~ \verb,\,\verb,<,latin\verb,>, ~|~ \verb,\,\verb,<,latin\,latin\verb,>, ~|~ greek ~|~ \\ + & & \verb,\<^isub>, ~|~ \verb,\<^isup>, \\ + quasiletter & = & letter ~|~ digit ~|~ \verb,_, ~|~ \verb,', \\ + latin & = & \verb,a, ~|~ \dots ~|~ \verb,z, ~|~ \verb,A, ~|~ \dots ~|~ \verb,Z, \\ + digit & = & \verb,0, ~|~ \dots ~|~ \verb,9, \\ + sym & = & \verb,!, ~|~ \verb,#, ~|~ \verb,$, ~|~ \verb,%, ~|~ \verb,&, ~|~ + \verb,*, ~|~ \verb,+, ~|~ \verb,-, ~|~ \verb,/, ~|~ \\ + & & \verb,<, ~|~ \verb,=, ~|~ \verb,>, ~|~ \verb,?, ~|~ \texttt{\at} ~|~ + \verb,^, ~|~ \verb,_, ~|~ \verb,|, ~|~ \verb,~, \\ + greek & = & \verb,\, ~|~ \verb,\, ~|~ \verb,\, ~|~ \verb,\, ~| \\ + & & \verb,\, ~|~ \verb,\, ~|~ \verb,\, ~|~ \verb,\, ~| \\ + & & \verb,\, ~|~ \verb,\, ~|~ \verb,\, ~|~ \verb,\, ~| \\ + & & \verb,\, ~|~ \verb,\, ~|~ \verb,\, ~|~ \verb,\, ~|~ \verb,\, ~| \\ + & & \verb,\, ~|~ \verb,\, ~|~ \verb,\, ~|~ \verb,\, ~| \\ + & & \verb,\, ~|~ \verb,\, ~|~ \verb,\, ~|~ \verb,\, ~| \\ + & & \verb,\, ~|~ \verb,\, ~|~ \verb,\, ~|~ \verb,\, ~| \\ + & & \verb,\, ~|~ \verb,\, ~|~ \verb,\, ~|~ \verb,\, \\ + \end{matharray} + + The syntax of @{syntax string} admits any characters, including + newlines; ``@{verbatim "\""}'' (double-quote) and ``@{verbatim + "\\"}'' (backslash) need to be escaped by a backslash; arbitrary + character codes may be specified as ``@{verbatim "\\"}@{text ddd}'', + with three decimal digits. Alternative strings according to + @{syntax altstring} are analogous, using single back-quotes instead. + The body of @{syntax verbatim} may consist of any text not + containing ``@{verbatim "*"}@{verbatim "}"}''; this allows + convenient inclusion of quotes without further escapes. The greek + letters do \emph{not} include @{verbatim "\"}, which is already used + differently in the meta-logic. + + Common mathematical symbols such as @{text \} are represented in + Isabelle as @{verbatim \}. There are infinitely many Isabelle + symbols like this, although proper presentation is left to front-end + tools such as {\LaTeX} or Proof~General with the X-Symbol package. + A list of standard Isabelle symbols that work well with these tools + is given in \cite[appendix~A]{isabelle-sys}. + + Source comments take the form @{verbatim "(*"}~@{text + "\"}~@{verbatim "*)"} and may be nested, although user-interface + tools might prevent this. Note that this form indicates source + comments only, which are stripped after lexical analysis of the + input. The Isar document syntax also provides formal comments that + are considered as part of the text (see \secref{sec:comments}). +*} + + +section {* Common syntax entities *} + +text {* + We now introduce several basic syntactic entities, such as names, + terms, and theorem specifications, which are factored out of the + actual Isar language elements to be described later. +*} + + +subsection {* Names *} + +text {* + Entity \railqtok{name} usually refers to any name of types, + constants, theorems etc.\ that are to be \emph{declared} or + \emph{defined} (so qualified identifiers are excluded here). Quoted + strings provide an escape for non-identifier names or those ruled + out by outer syntax keywords (e.g.\ quoted @{verbatim "\"let\""}). + Already existing objects are usually referenced by + \railqtok{nameref}. + + \indexoutertoken{name}\indexoutertoken{parname}\indexoutertoken{nameref} + \indexoutertoken{int} + \begin{rail} + name: ident | symident | string | nat + ; + parname: '(' name ')' + ; + nameref: name | longident + ; + int: nat | '-' nat + ; + \end{rail} +*} + + +subsection {* Comments \label{sec:comments} *} + +text {* + Large chunks of plain \railqtok{text} are usually given + \railtok{verbatim}, i.e.\ enclosed in @{verbatim "{"}@{verbatim + "*"}~@{text "\"}~@{verbatim "*"}@{verbatim "}"}. For convenience, + any of the smaller text units conforming to \railqtok{nameref} are + admitted as well. A marginal \railnonterm{comment} is of the form + @{verbatim "--"} \railqtok{text}. Any number of these may occur + within Isabelle/Isar commands. + + \indexoutertoken{text}\indexouternonterm{comment} + \begin{rail} + text: verbatim | nameref + ; + comment: '--' text + ; + \end{rail} +*} + + +subsection {* Type classes, sorts and arities *} + +text {* + Classes are specified by plain names. Sorts have a very simple + inner syntax, which is either a single class name @{text c} or a + list @{text "{c\<^sub>1, \, c\<^sub>n}"} referring to the + intersection of these classes. The syntax of type arities is given + directly at the outer level. + + \indexouternonterm{sort}\indexouternonterm{arity} + \indexouternonterm{classdecl} + \begin{rail} + classdecl: name (('<' | subseteq) (nameref + ','))? + ; + sort: nameref + ; + arity: ('(' (sort + ',') ')')? sort + ; + \end{rail} +*} + + +subsection {* Types and terms \label{sec:types-terms} *} + +text {* + The actual inner Isabelle syntax, that of types and terms of the + logic, is far too sophisticated in order to be modelled explicitly + at the outer theory level. Basically, any such entity has to be + quoted to turn it into a single token (the parsing and type-checking + is performed internally later). For convenience, a slightly more + liberal convention is adopted: quotes may be omitted for any type or + term that is already atomic at the outer level. For example, one + may just write @{verbatim x} instead of quoted @{verbatim "\"x\""}. + Note that symbolic identifiers (e.g.\ @{verbatim "++"} or @{text + "\"} are available as well, provided these have not been superseded + by commands or other keywords already (such as @{verbatim "="} or + @{verbatim "+"}). + + \indexoutertoken{type}\indexoutertoken{term}\indexoutertoken{prop} + \begin{rail} + type: nameref | typefree | typevar + ; + term: nameref | var + ; + prop: term + ; + \end{rail} + + Positional instantiations are indicated by giving a sequence of + terms, or the placeholder ``@{text _}'' (underscore), which means to + skip a position. + + \indexoutertoken{inst}\indexoutertoken{insts} + \begin{rail} + inst: underscore | term + ; + insts: (inst *) + ; + \end{rail} + + Type declarations and definitions usually refer to + \railnonterm{typespec} on the left-hand side. This models basic + type constructor application at the outer syntax level. Note that + only plain postfix notation is available here, but no infixes. + + \indexouternonterm{typespec} + \begin{rail} + typespec: (() | typefree | '(' ( typefree + ',' ) ')') name + ; + \end{rail} +*} + + +subsection {* Mixfix annotations *} + +text {* + Mixfix annotations specify concrete \emph{inner} syntax of Isabelle + types and terms. Some commands such as @{command "types"} (see + \secref{sec:types-pure}) admit infixes only, while @{command + "consts"} (see \secref{sec:consts}) and @{command "syntax"} (see + \secref{sec:syn-trans}) support the full range of general mixfixes + and binders. + + \indexouternonterm{infix}\indexouternonterm{mixfix}\indexouternonterm{structmixfix} + \begin{rail} + infix: '(' ('infix' | 'infixl' | 'infixr') string? nat ')' + ; + mixfix: infix | '(' string prios? nat? ')' | '(' 'binder' string prios? nat ')' + ; + structmixfix: mixfix | '(' 'structure' ')' + ; + + prios: '[' (nat + ',') ']' + ; + \end{rail} + + Here the \railtok{string} specifications refer to the actual mixfix + template (see also \cite{isabelle-ref}), which may include literal + text, spacing, blocks, and arguments (denoted by ``@{text _}''); the + special symbol ``@{verbatim "\"}'' (printed as ``@{text "\"}'') + represents an index argument that specifies an implicit structure + reference (see also \secref{sec:locale}). Infix and binder + declarations provide common abbreviations for particular mixfix + declarations. So in practice, mixfix templates mostly degenerate to + literal text for concrete syntax, such as ``@{verbatim "++"}'' for + an infix symbol, or ``@{verbatim "++"}@{text "\"}'' for an infix of + an implicit structure. +*} + + +subsection {* Proof methods \label{sec:syn-meth} *} + +text {* + Proof methods are either basic ones, or expressions composed of + methods via ``@{verbatim ","}'' (sequential composition), + ``@{verbatim "|"}'' (alternative choices), ``@{verbatim "?"}'' + (try), ``@{verbatim "+"}'' (repeat at least once), ``@{verbatim + "["}@{text n}@{verbatim "]"}'' (restriction to first @{text n} + sub-goals, with default @{text "n = 1"}). In practice, proof + methods are usually just a comma separated list of + \railqtok{nameref}~\railnonterm{args} specifications. Note that + parentheses may be dropped for single method specifications (with no + arguments). + + \indexouternonterm{method} + \begin{rail} + method: (nameref | '(' methods ')') (() | '?' | '+' | '[' nat? ']') + ; + methods: (nameref args | method) + (',' | '|') + ; + \end{rail} + + Proper Isar proof methods do \emph{not} admit arbitrary goal + addressing, but refer either to the first sub-goal or all sub-goals + uniformly. The goal restriction operator ``@{text "[n]"}'' + evaluates a method expression within a sandbox consisting of the + first @{text n} sub-goals (which need to exist). For example, the + method ``@{text "simp_all[3]"}'' simplifies the first three + sub-goals, while ``@{text "(rule foo, simp_all)[]"}'' simplifies all + new goals that emerge from applying rule @{text "foo"} to the + originally first one. + + Improper methods, notably tactic emulations, offer a separate + low-level goal addressing scheme as explicit argument to the + individual tactic being involved. Here ``@{text "[!]"}'' refers to + all goals, and ``@{text "[n-]"}'' to all goals starting from @{text + "n"}. + + \indexouternonterm{goalspec} + \begin{rail} + goalspec: '[' (nat '-' nat | nat '-' | nat | '!' ) ']' + ; + \end{rail} +*} + + +subsection {* Attributes and theorems \label{sec:syn-att} *} + +text {* + Attributes (and proof methods, see \secref{sec:syn-meth}) have their + own ``semi-inner'' syntax, in the sense that input conforming to + \railnonterm{args} below is parsed by the attribute a second time. + The attribute argument specifications may be any sequence of atomic + entities (identifiers, strings etc.), or properly bracketed argument + lists. Below \railqtok{atom} refers to any atomic entity, including + any \railtok{keyword} conforming to \railtok{symident}. + + \indexoutertoken{atom}\indexouternonterm{args}\indexouternonterm{attributes} + \begin{rail} + atom: nameref | typefree | typevar | var | nat | keyword + ; + arg: atom | '(' args ')' | '[' args ']' + ; + args: arg * + ; + attributes: '[' (nameref args * ',') ']' + ; + \end{rail} + + Theorem specifications come in several flavors: + \railnonterm{axmdecl} and \railnonterm{thmdecl} usually refer to + axioms, assumptions or results of goal statements, while + \railnonterm{thmdef} collects lists of existing theorems. Existing + theorems are given by \railnonterm{thmref} and + \railnonterm{thmrefs}, the former requires an actual singleton + result. + + There are three forms of theorem references: + \begin{enumerate} + + \item named facts @{text "a"}, + + \item selections from named facts @{text "a(i)"} or @{text "a(j - k)"}, + + \item literal fact propositions using @{syntax_ref altstring} syntax + @{verbatim "`"}@{text "\"}@{verbatim "`"} (see also method + @{method_ref fact} in \secref{sec:pure-meth-att}). + + \end{enumerate} + + Any kind of theorem specification may include lists of attributes + both on the left and right hand sides; attributes are applied to any + immediately preceding fact. If names are omitted, the theorems are + not stored within the theorem database of the theory or proof + context, but any given attributes are applied nonetheless. + + An extra pair of brackets around attributes (like ``@{text + "[[simproc a]]"}'') abbreviates a theorem reference involving an + internal dummy fact, which will be ignored later on. So only the + effect of the attribute on the background context will persist. + This form of in-place declarations is particularly useful with + commands like @{command "declare"} and @{command "using"}. + + \indexouternonterm{axmdecl}\indexouternonterm{thmdecl} + \indexouternonterm{thmdef}\indexouternonterm{thmref} + \indexouternonterm{thmrefs}\indexouternonterm{selection} + \begin{rail} + axmdecl: name attributes? ':' + ; + thmdecl: thmbind ':' + ; + thmdef: thmbind '=' + ; + thmref: (nameref selection? | altstring) attributes? | '[' attributes ']' + ; + thmrefs: thmref + + ; + + thmbind: name attributes | name | attributes + ; + selection: '(' ((nat | nat '-' nat?) + ',') ')' + ; + \end{rail} +*} + + +subsection {* Term patterns and declarations \label{sec:term-decls} *} + +text {* + Wherever explicit propositions (or term fragments) occur in a proof + text, casual binding of schematic term variables may be given + specified via patterns of the form ``@{text "(\ p\<^sub>1 \ + p\<^sub>n)"}''. This works both for \railqtok{term} and \railqtok{prop}. + + \indexouternonterm{termpat}\indexouternonterm{proppat} + \begin{rail} + termpat: '(' ('is' term +) ')' + ; + proppat: '(' ('is' prop +) ')' + ; + \end{rail} + + \medskip Declarations of local variables @{text "x :: \"} and + logical propositions @{text "a : \"} represent different views on + the same principle of introducing a local scope. In practice, one + may usually omit the typing of \railnonterm{vars} (due to + type-inference), and the naming of propositions (due to implicit + references of current facts). In any case, Isar proof elements + usually admit to introduce multiple such items simultaneously. + + \indexouternonterm{vars}\indexouternonterm{props} + \begin{rail} + vars: (name+) ('::' type)? + ; + props: thmdecl? (prop proppat? +) + ; + \end{rail} + + The treatment of multiple declarations corresponds to the + complementary focus of \railnonterm{vars} versus + \railnonterm{props}. In ``@{text "x\<^sub>1 \ x\<^sub>n :: \"}'' + the typing refers to all variables, while in @{text "a: \\<^sub>1 \ + \\<^sub>n"} the naming refers to all propositions collectively. + Isar language elements that refer to \railnonterm{vars} or + \railnonterm{props} typically admit separate typings or namings via + another level of iteration, with explicit @{keyword_ref "and"} + separators; e.g.\ see @{command "fix"} and @{command "assume"} in + \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