diff -r 094d70c81243 -r c0424e4de33d doc-src/IsarRef/Thy/syntax.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/doc-src/IsarRef/Thy/syntax.thy Mon Apr 28 14:22:42 2008 +0200 @@ -0,0 +1,741 @@ + +theory "syntax" +imports CPure +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 + \texttt{"x + y"} and identifier \texttt{z} are legal term + specifications within a theory, while \texttt{x + y} is not. + + Printed theory documents usually omit quotes to gain readability + (this is a matter of {\LaTeX} macro setup, say via + \verb,\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 ``\texttt{;}'' (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 ``\verb,#,'' 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 \verb,-k ZF, + (in conjunction with \verb,-l ZF, to specify the default logic + image). + \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; ``\verb|"|'' (double-quote) and ``\verb|\|'' (backslash) + need to be escaped by a backslash; arbitrary character codes may be + specified as ``\verb|\|$ddd$'', with 3 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 ``\verb,*,\verb,},''; this allows convenient + inclusion of quotes without further escapes. The greek letters do + \emph{not} include \verb,\,, which is already used differently in + the meta-logic. + + Common mathematical symbols such as @{text \} are represented in + Isabelle as \verb,\,. 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 \texttt{(*~\dots~*)} and may be + nested, although user-interface tools might prevent this. Note that + \texttt{(*~\dots~*)} indicate 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 \S\ref{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.\ \verb|"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 + \verb,{,\verb,*,~\dots~\verb,*,\verb,},. For convenience, any of + the smaller text units conforming to \railqtok{nameref} are admitted + as well. A marginal \railnonterm{comment} is of the form + \texttt{--} \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. + + \railalias{subseteq}{\isasymsubseteq} + \railterm{subseteq} + + \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 \texttt{x} instead of \texttt{"x"}. Note that + symbolic identifiers (e.g.\ \texttt{++} or @{text "\"} are available + as well, provided these have not been superseded by commands or + other keywords already (e.g.\ \texttt{=} or \texttt{+}). + + \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 ``$\_$'' (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 + \S\ref{sec:types-pure}) admit infixes only, while @{command + "consts"} (see \S\ref{sec:consts}) and @{command "syntax"} (see + \S\ref{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 ``$_$''); the + special symbol \verb,\, (printed as ``\i'') represents an index + argument that specifies an implicit structure reference (see also + \S\ref{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 ``\verb,++,'' for an infix symbol, or + ``\verb,++,\i'' 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 ``\texttt{,}'' (sequential composition), ``\texttt{|}'' + (alternative choices), ``\texttt{?}'' (try), ``\texttt{+}'' (repeat + at least once), ``\texttt{[$n$]}'' (restriction to first @{text n} + sub-goals, default $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 ``\texttt{[$n$]}'' + evaluates a method expression within a sandbox consisting of the + first @{text n} sub-goals (which need to exist). For example, + @{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 \S\ref{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, j - k)"} + + \item literal fact propositions using @{syntax_ref altstring} syntax + $\backquote\phi\backquote$, (see also method @{method_ref fact} in + \S\ref{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 attribute declarations --- such as + ``@{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 + \S\ref{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 \S\ref{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 + \S\ref{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, + \texttt{{\at}{\ttlbrace}thm~sym~[no_vars]{\ttrbrace}} would print + the 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 \texttt{(*~\dots~*)} or verbatim text + \verb|{*|~\dots~\verb|*|\verb|}|. + + \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 \S\ref{sec:syn-att}); the @{attribute_ref + no_vars} rule (see \S\ref{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 ``$_$'' 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 $1$, \dots, $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