1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/doc-src/IsarRef/Thy/syntax.thy Mon Apr 28 14:22:42 2008 +0200
1.3 @@ -0,0 +1,741 @@
1.4 +
1.5 +theory "syntax"
1.6 +imports CPure
1.7 +begin
1.8 +
1.9 +chapter {* Syntax primitives *}
1.10 +
1.11 +text {*
1.12 + The rather generic framework of Isabelle/Isar syntax emerges from
1.13 + three main syntactic categories: \emph{commands} of the top-level
1.14 + Isar engine (covering theory and proof elements), \emph{methods} for
1.15 + general goal refinements (analogous to traditional ``tactics''), and
1.16 + \emph{attributes} for operations on facts (within a certain
1.17 + context). Subsequently we give a reference of basic syntactic
1.18 + entities underlying Isabelle/Isar syntax in a bottom-up manner.
1.19 + Concrete theory and proof language elements will be introduced later
1.20 + on.
1.21 +
1.22 + \medskip In order to get started with writing well-formed
1.23 + Isabelle/Isar documents, the most important aspect to be noted is
1.24 + the difference of \emph{inner} versus \emph{outer} syntax. Inner
1.25 + syntax is that of Isabelle types and terms of the logic, while outer
1.26 + syntax is that of Isabelle/Isar theory sources (specifications and
1.27 + proofs). As a general rule, inner syntax entities may occur only as
1.28 + \emph{atomic entities} within outer syntax. For example, the string
1.29 + \texttt{"x + y"} and identifier \texttt{z} are legal term
1.30 + specifications within a theory, while \texttt{x + y} is not.
1.31 +
1.32 + Printed theory documents usually omit quotes to gain readability
1.33 + (this is a matter of {\LaTeX} macro setup, say via
1.34 + \verb,\isabellestyle,, see also \cite{isabelle-sys}). Experienced
1.35 + users of Isabelle/Isar may easily reconstruct the lost technical
1.36 + information, while mere readers need not care about quotes at all.
1.37 +
1.38 + \medskip Isabelle/Isar input may contain any number of input
1.39 + termination characters ``\texttt{;}'' (semicolon) to separate
1.40 + commands explicitly. This is particularly useful in interactive
1.41 + shell sessions to make clear where the current command is intended
1.42 + to end. Otherwise, the interpreter loop will continue to issue a
1.43 + secondary prompt ``\verb,#,'' until an end-of-command is clearly
1.44 + recognized from the input syntax, e.g.\ encounter of the next
1.45 + command keyword.
1.46 +
1.47 + More advanced interfaces such as Proof~General \cite{proofgeneral}
1.48 + do not require explicit semicolons, the amount of input text is
1.49 + determined automatically by inspecting the present content of the
1.50 + Emacs text buffer. In the printed presentation of Isabelle/Isar
1.51 + documents semicolons are omitted altogether for readability.
1.52 +
1.53 + \begin{warn}
1.54 + Proof~General requires certain syntax classification tables in
1.55 + order to achieve properly synchronized interaction with the
1.56 + Isabelle/Isar process. These tables need to be consistent with
1.57 + the Isabelle version and particular logic image to be used in a
1.58 + running session (common object-logics may well change the outer
1.59 + syntax). The standard setup should work correctly with any of the
1.60 + ``official'' logic images derived from Isabelle/HOL (including
1.61 + HOLCF etc.). Users of alternative logics may need to tell
1.62 + Proof~General explicitly, e.g.\ by giving an option \verb,-k ZF,
1.63 + (in conjunction with \verb,-l ZF, to specify the default logic
1.64 + image).
1.65 + \end{warn}
1.66 +*}
1.67 +
1.68 +
1.69 +section {* Lexical matters \label{sec:lex-syntax} *}
1.70 +
1.71 +text {*
1.72 + The Isabelle/Isar outer syntax provides token classes as presented
1.73 + below; most of these coincide with the inner lexical syntax as
1.74 + presented in \cite{isabelle-ref}.
1.75 +
1.76 + \begin{matharray}{rcl}
1.77 + @{syntax_def ident} & = & letter\,quasiletter^* \\
1.78 + @{syntax_def longident} & = & ident (\verb,.,ident)^+ \\
1.79 + @{syntax_def symident} & = & sym^+ ~|~ \verb,\,\verb,<,ident\verb,>, \\
1.80 + @{syntax_def nat} & = & digit^+ \\
1.81 + @{syntax_def var} & = & ident ~|~ \verb,?,ident ~|~ \verb,?,ident\verb,.,nat \\
1.82 + @{syntax_def typefree} & = & \verb,',ident \\
1.83 + @{syntax_def typevar} & = & typefree ~|~ \verb,?,typefree ~|~ \verb,?,typefree\verb,.,nat \\
1.84 + @{syntax_def string} & = & \verb,", ~\dots~ \verb,", \\
1.85 + @{syntax_def altstring} & = & \backquote ~\dots~ \backquote \\
1.86 + @{syntax_def verbatim} & = & \verb,{*, ~\dots~ \verb,*,\verb,}, \\[1ex]
1.87 +
1.88 + letter & = & latin ~|~ \verb,\,\verb,<,latin\verb,>, ~|~ \verb,\,\verb,<,latin\,latin\verb,>, ~|~ greek ~|~ \\
1.89 + & & \verb,\<^isub>, ~|~ \verb,\<^isup>, \\
1.90 + quasiletter & = & letter ~|~ digit ~|~ \verb,_, ~|~ \verb,', \\
1.91 + latin & = & \verb,a, ~|~ \dots ~|~ \verb,z, ~|~ \verb,A, ~|~ \dots ~|~ \verb,Z, \\
1.92 + digit & = & \verb,0, ~|~ \dots ~|~ \verb,9, \\
1.93 + sym & = & \verb,!, ~|~ \verb,#, ~|~ \verb,$, ~|~ \verb,%, ~|~ \verb,&, ~|~
1.94 + \verb,*, ~|~ \verb,+, ~|~ \verb,-, ~|~ \verb,/, ~|~ \\
1.95 + & & \verb,<, ~|~ \verb,=, ~|~ \verb,>, ~|~ \verb,?, ~|~ \texttt{\at} ~|~
1.96 + \verb,^, ~|~ \verb,_, ~|~ \verb,|, ~|~ \verb,~, \\
1.97 + greek & = & \verb,\<alpha>, ~|~ \verb,\<beta>, ~|~ \verb,\<gamma>, ~|~ \verb,\<delta>, ~| \\
1.98 + & & \verb,\<epsilon>, ~|~ \verb,\<zeta>, ~|~ \verb,\<eta>, ~|~ \verb,\<theta>, ~| \\
1.99 + & & \verb,\<iota>, ~|~ \verb,\<kappa>, ~|~ \verb,\<mu>, ~|~ \verb,\<nu>, ~| \\
1.100 + & & \verb,\<xi>, ~|~ \verb,\<pi>, ~|~ \verb,\<rho>, ~|~ \verb,\<sigma>, ~|~ \verb,\<tau>, ~| \\
1.101 + & & \verb,\<upsilon>, ~|~ \verb,\<phi>, ~|~ \verb,\<chi>, ~|~ \verb,\<psi>, ~| \\
1.102 + & & \verb,\<omega>, ~|~ \verb,\<Gamma>, ~|~ \verb,\<Delta>, ~|~ \verb,\<Theta>, ~| \\
1.103 + & & \verb,\<Lambda>, ~|~ \verb,\<Xi>, ~|~ \verb,\<Pi>, ~|~ \verb,\<Sigma>, ~| \\
1.104 + & & \verb,\<Upsilon>, ~|~ \verb,\<Phi>, ~|~ \verb,\<Psi>, ~|~ \verb,\<Omega>, \\
1.105 + \end{matharray}
1.106 +
1.107 + The syntax of @{syntax string} admits any characters, including
1.108 + newlines; ``\verb|"|'' (double-quote) and ``\verb|\|'' (backslash)
1.109 + need to be escaped by a backslash; arbitrary character codes may be
1.110 + specified as ``\verb|\|$ddd$'', with 3 decimal digits. Alternative
1.111 + strings according to @{syntax altstring} are analogous, using single
1.112 + back-quotes instead. The body of @{syntax verbatim} may consist of
1.113 + any text not containing ``\verb,*,\verb,},''; this allows convenient
1.114 + inclusion of quotes without further escapes. The greek letters do
1.115 + \emph{not} include \verb,\<lambda>,, which is already used differently in
1.116 + the meta-logic.
1.117 +
1.118 + Common mathematical symbols such as @{text \<forall>} are represented in
1.119 + Isabelle as \verb,\<forall>,. There are infinitely many Isabelle symbols
1.120 + like this, although proper presentation is left to front-end tools
1.121 + such as {\LaTeX} or Proof~General with the X-Symbol package. A list
1.122 + of standard Isabelle symbols that work well with these tools is
1.123 + given in \cite[appendix~A]{isabelle-sys}.
1.124 +
1.125 + Source comments take the form \texttt{(*~\dots~*)} and may be
1.126 + nested, although user-interface tools might prevent this. Note that
1.127 + \texttt{(*~\dots~*)} indicate source comments only, which are
1.128 + stripped after lexical analysis of the input. The Isar document
1.129 + syntax also provides formal comments that are considered as part of
1.130 + the text (see \S\ref{sec:comments}).
1.131 +*}
1.132 +
1.133 +
1.134 +section {* Common syntax entities *}
1.135 +
1.136 +text {*
1.137 + We now introduce several basic syntactic entities, such as names,
1.138 + terms, and theorem specifications, which are factored out of the
1.139 + actual Isar language elements to be described later.
1.140 +*}
1.141 +
1.142 +
1.143 +subsection {* Names *}
1.144 +
1.145 +text {*
1.146 + Entity \railqtok{name} usually refers to any name of types,
1.147 + constants, theorems etc.\ that are to be \emph{declared} or
1.148 + \emph{defined} (so qualified identifiers are excluded here). Quoted
1.149 + strings provide an escape for non-identifier names or those ruled
1.150 + out by outer syntax keywords (e.g.\ \verb|"let"|). Already existing
1.151 + objects are usually referenced by \railqtok{nameref}.
1.152 +
1.153 + \indexoutertoken{name}\indexoutertoken{parname}\indexoutertoken{nameref}
1.154 + \indexoutertoken{int}
1.155 + \begin{rail}
1.156 + name: ident | symident | string | nat
1.157 + ;
1.158 + parname: '(' name ')'
1.159 + ;
1.160 + nameref: name | longident
1.161 + ;
1.162 + int: nat | '-' nat
1.163 + ;
1.164 + \end{rail}
1.165 +*}
1.166 +
1.167 +
1.168 +subsection {* Comments \label{sec:comments} *}
1.169 +
1.170 +text {*
1.171 + Large chunks of plain \railqtok{text} are usually given
1.172 + \railtok{verbatim}, i.e.\ enclosed in
1.173 + \verb,{,\verb,*,~\dots~\verb,*,\verb,},. For convenience, any of
1.174 + the smaller text units conforming to \railqtok{nameref} are admitted
1.175 + as well. A marginal \railnonterm{comment} is of the form
1.176 + \texttt{--} \railqtok{text}. Any number of these may occur within
1.177 + Isabelle/Isar commands.
1.178 +
1.179 + \indexoutertoken{text}\indexouternonterm{comment}
1.180 + \begin{rail}
1.181 + text: verbatim | nameref
1.182 + ;
1.183 + comment: '--' text
1.184 + ;
1.185 + \end{rail}
1.186 +*}
1.187 +
1.188 +
1.189 +subsection {* Type classes, sorts and arities *}
1.190 +
1.191 +text {*
1.192 + Classes are specified by plain names. Sorts have a very simple
1.193 + inner syntax, which is either a single class name @{text c} or a
1.194 + list @{text "{c\<^sub>1, \<dots>, c\<^sub>n}"} referring to the
1.195 + intersection of these classes. The syntax of type arities is given
1.196 + directly at the outer level.
1.197 +
1.198 + \railalias{subseteq}{\isasymsubseteq}
1.199 + \railterm{subseteq}
1.200 +
1.201 + \indexouternonterm{sort}\indexouternonterm{arity}
1.202 + \indexouternonterm{classdecl}
1.203 + \begin{rail}
1.204 + classdecl: name (('<' | subseteq) (nameref + ','))?
1.205 + ;
1.206 + sort: nameref
1.207 + ;
1.208 + arity: ('(' (sort + ',') ')')? sort
1.209 + ;
1.210 + \end{rail}
1.211 +*}
1.212 +
1.213 +
1.214 +subsection {* Types and terms \label{sec:types-terms} *}
1.215 +
1.216 +text {*
1.217 + The actual inner Isabelle syntax, that of types and terms of the
1.218 + logic, is far too sophisticated in order to be modelled explicitly
1.219 + at the outer theory level. Basically, any such entity has to be
1.220 + quoted to turn it into a single token (the parsing and type-checking
1.221 + is performed internally later). For convenience, a slightly more
1.222 + liberal convention is adopted: quotes may be omitted for any type or
1.223 + term that is already atomic at the outer level. For example, one
1.224 + may just write \texttt{x} instead of \texttt{"x"}. Note that
1.225 + symbolic identifiers (e.g.\ \texttt{++} or @{text "\<forall>"} are available
1.226 + as well, provided these have not been superseded by commands or
1.227 + other keywords already (e.g.\ \texttt{=} or \texttt{+}).
1.228 +
1.229 + \indexoutertoken{type}\indexoutertoken{term}\indexoutertoken{prop}
1.230 + \begin{rail}
1.231 + type: nameref | typefree | typevar
1.232 + ;
1.233 + term: nameref | var
1.234 + ;
1.235 + prop: term
1.236 + ;
1.237 + \end{rail}
1.238 +
1.239 + Positional instantiations are indicated by giving a sequence of
1.240 + terms, or the placeholder ``$\_$'' (underscore), which means to skip
1.241 + a position.
1.242 +
1.243 + \indexoutertoken{inst}\indexoutertoken{insts}
1.244 + \begin{rail}
1.245 + inst: underscore | term
1.246 + ;
1.247 + insts: (inst *)
1.248 + ;
1.249 + \end{rail}
1.250 +
1.251 + Type declarations and definitions usually refer to
1.252 + \railnonterm{typespec} on the left-hand side. This models basic
1.253 + type constructor application at the outer syntax level. Note that
1.254 + only plain postfix notation is available here, but no infixes.
1.255 +
1.256 + \indexouternonterm{typespec}
1.257 + \begin{rail}
1.258 + typespec: (() | typefree | '(' ( typefree + ',' ) ')') name
1.259 + ;
1.260 + \end{rail}
1.261 +*}
1.262 +
1.263 +
1.264 +subsection {* Mixfix annotations *}
1.265 +
1.266 +text {*
1.267 + Mixfix annotations specify concrete \emph{inner} syntax of Isabelle
1.268 + types and terms. Some commands such as @{command "types"} (see
1.269 + \S\ref{sec:types-pure}) admit infixes only, while @{command
1.270 + "consts"} (see \S\ref{sec:consts}) and @{command "syntax"} (see
1.271 + \S\ref{sec:syn-trans}) support the full range of general mixfixes
1.272 + and binders.
1.273 +
1.274 + \indexouternonterm{infix}\indexouternonterm{mixfix}\indexouternonterm{structmixfix}
1.275 + \begin{rail}
1.276 + infix: '(' ('infix' | 'infixl' | 'infixr') string? nat ')'
1.277 + ;
1.278 + mixfix: infix | '(' string prios? nat? ')' | '(' 'binder' string prios? nat ')'
1.279 + ;
1.280 + structmixfix: mixfix | '(' 'structure' ')'
1.281 + ;
1.282 +
1.283 + prios: '[' (nat + ',') ']'
1.284 + ;
1.285 + \end{rail}
1.286 +
1.287 + Here the \railtok{string} specifications refer to the actual mixfix
1.288 + template (see also \cite{isabelle-ref}), which may include literal
1.289 + text, spacing, blocks, and arguments (denoted by ``$_$''); the
1.290 + special symbol \verb,\<index>, (printed as ``\i'') represents an index
1.291 + argument that specifies an implicit structure reference (see also
1.292 + \S\ref{sec:locale}). Infix and binder declarations provide common
1.293 + abbreviations for particular mixfix declarations. So in practice,
1.294 + mixfix templates mostly degenerate to literal text for concrete
1.295 + syntax, such as ``\verb,++,'' for an infix symbol, or
1.296 + ``\verb,++,\i'' for an infix of an implicit structure.
1.297 +*}
1.298 +
1.299 +
1.300 +subsection {* Proof methods \label{sec:syn-meth} *}
1.301 +
1.302 +text {*
1.303 + Proof methods are either basic ones, or expressions composed of
1.304 + methods via ``\texttt{,}'' (sequential composition), ``\texttt{|}''
1.305 + (alternative choices), ``\texttt{?}'' (try), ``\texttt{+}'' (repeat
1.306 + at least once), ``\texttt{[$n$]}'' (restriction to first @{text n}
1.307 + sub-goals, default $n = 1$). In practice, proof methods are usually
1.308 + just a comma separated list of \railqtok{nameref}~\railnonterm{args}
1.309 + specifications. Note that parentheses may be dropped for single
1.310 + method specifications (with no arguments).
1.311 +
1.312 + \indexouternonterm{method}
1.313 + \begin{rail}
1.314 + method: (nameref | '(' methods ')') (() | '?' | '+' | '[' nat? ']')
1.315 + ;
1.316 + methods: (nameref args | method) + (',' | '|')
1.317 + ;
1.318 + \end{rail}
1.319 +
1.320 + Proper Isar proof methods do \emph{not} admit arbitrary goal
1.321 + addressing, but refer either to the first sub-goal or all sub-goals
1.322 + uniformly. The goal restriction operator ``\texttt{[$n$]}''
1.323 + evaluates a method expression within a sandbox consisting of the
1.324 + first @{text n} sub-goals (which need to exist). For example,
1.325 + @{text "simp_all[3]"} simplifies the first three sub-goals, while
1.326 + @{text "(rule foo, simp_all)[]"} simplifies all new goals that
1.327 + emerge from applying rule @{text "foo"} to the originally first one.
1.328 +
1.329 + Improper methods, notably tactic emulations, offer a separate
1.330 + low-level goal addressing scheme as explicit argument to the
1.331 + individual tactic being involved. Here @{text "[!]"} refers to all
1.332 + goals, and @{text "[n-]"} to all goals starting from @{text "n"},
1.333 +
1.334 + \indexouternonterm{goalspec}
1.335 + \begin{rail}
1.336 + goalspec: '[' (nat '-' nat | nat '-' | nat | '!' ) ']'
1.337 + ;
1.338 + \end{rail}
1.339 +*}
1.340 +
1.341 +
1.342 +subsection {* Attributes and theorems \label{sec:syn-att} *}
1.343 +
1.344 +text {*
1.345 + Attributes (and proof methods, see \S\ref{sec:syn-meth}) have their
1.346 + own ``semi-inner'' syntax, in the sense that input conforming to
1.347 + \railnonterm{args} below is parsed by the attribute a second time.
1.348 + The attribute argument specifications may be any sequence of atomic
1.349 + entities (identifiers, strings etc.), or properly bracketed argument
1.350 + lists. Below \railqtok{atom} refers to any atomic entity, including
1.351 + any \railtok{keyword} conforming to \railtok{symident}.
1.352 +
1.353 + \indexoutertoken{atom}\indexouternonterm{args}\indexouternonterm{attributes}
1.354 + \begin{rail}
1.355 + atom: nameref | typefree | typevar | var | nat | keyword
1.356 + ;
1.357 + arg: atom | '(' args ')' | '[' args ']'
1.358 + ;
1.359 + args: arg *
1.360 + ;
1.361 + attributes: '[' (nameref args * ',') ']'
1.362 + ;
1.363 + \end{rail}
1.364 +
1.365 + Theorem specifications come in several flavors:
1.366 + \railnonterm{axmdecl} and \railnonterm{thmdecl} usually refer to
1.367 + axioms, assumptions or results of goal statements, while
1.368 + \railnonterm{thmdef} collects lists of existing theorems. Existing
1.369 + theorems are given by \railnonterm{thmref} and
1.370 + \railnonterm{thmrefs}, the former requires an actual singleton
1.371 + result.
1.372 +
1.373 + There are three forms of theorem references:
1.374 + \begin{enumerate}
1.375 +
1.376 + \item named facts @{text "a"}
1.377 +
1.378 + \item selections from named facts @{text "a(i, j - k)"}
1.379 +
1.380 + \item literal fact propositions using @{syntax_ref altstring} syntax
1.381 + $\backquote\phi\backquote$, (see also method @{method_ref fact} in
1.382 + \S\ref{sec:pure-meth-att}).
1.383 +
1.384 + \end{enumerate}
1.385 +
1.386 + Any kind of theorem specification may include lists of attributes
1.387 + both on the left and right hand sides; attributes are applied to any
1.388 + immediately preceding fact. If names are omitted, the theorems are
1.389 + not stored within the theorem database of the theory or proof
1.390 + context, but any given attributes are applied nonetheless.
1.391 +
1.392 + An extra pair of brackets around attribute declarations --- such as
1.393 + ``@{text "[[simproc a]]"}'' --- abbreviates a theorem reference
1.394 + involving an internal dummy fact, which will be ignored later on.
1.395 + So only the effect of the attribute on the background context will
1.396 + persist. This form of in-place declarations is particularly useful
1.397 + with commands like @{command "declare"} and @{command "using"}.
1.398 +
1.399 + \indexouternonterm{axmdecl}\indexouternonterm{thmdecl}
1.400 + \indexouternonterm{thmdef}\indexouternonterm{thmref}
1.401 + \indexouternonterm{thmrefs}\indexouternonterm{selection}
1.402 + \begin{rail}
1.403 + axmdecl: name attributes? ':'
1.404 + ;
1.405 + thmdecl: thmbind ':'
1.406 + ;
1.407 + thmdef: thmbind '='
1.408 + ;
1.409 + thmref: (nameref selection? | altstring) attributes? | '[' attributes ']'
1.410 + ;
1.411 + thmrefs: thmref +
1.412 + ;
1.413 +
1.414 + thmbind: name attributes | name | attributes
1.415 + ;
1.416 + selection: '(' ((nat | nat '-' nat?) + ',') ')'
1.417 + ;
1.418 + \end{rail}
1.419 +*}
1.420 +
1.421 +
1.422 +subsection {* Term patterns and declarations \label{sec:term-decls} *}
1.423 +
1.424 +text {*
1.425 + Wherever explicit propositions (or term fragments) occur in a proof
1.426 + text, casual binding of schematic term variables may be given
1.427 + specified via patterns of the form ``@{text "(\<IS> p\<^sub>1 \<dots>
1.428 + p\<^sub>n)"}''. This works both for \railqtok{term} and \railqtok{prop}.
1.429 +
1.430 + \indexouternonterm{termpat}\indexouternonterm{proppat}
1.431 + \begin{rail}
1.432 + termpat: '(' ('is' term +) ')'
1.433 + ;
1.434 + proppat: '(' ('is' prop +) ')'
1.435 + ;
1.436 + \end{rail}
1.437 +
1.438 + \medskip Declarations of local variables @{text "x :: \<tau>"} and
1.439 + logical propositions @{text "a : \<phi>"} represent different views on
1.440 + the same principle of introducing a local scope. In practice, one
1.441 + may usually omit the typing of \railnonterm{vars} (due to
1.442 + type-inference), and the naming of propositions (due to implicit
1.443 + references of current facts). In any case, Isar proof elements
1.444 + usually admit to introduce multiple such items simultaneously.
1.445 +
1.446 + \indexouternonterm{vars}\indexouternonterm{props}
1.447 + \begin{rail}
1.448 + vars: (name+) ('::' type)?
1.449 + ;
1.450 + props: thmdecl? (prop proppat? +)
1.451 + ;
1.452 + \end{rail}
1.453 +
1.454 + The treatment of multiple declarations corresponds to the
1.455 + complementary focus of \railnonterm{vars} versus
1.456 + \railnonterm{props}. In ``@{text "x\<^sub>1 \<dots> x\<^sub>n :: \<tau>"}''
1.457 + the typing refers to all variables, while in @{text "a: \<phi>\<^sub>1 \<dots>
1.458 + \<phi>\<^sub>n"} the naming refers to all propositions collectively.
1.459 + Isar language elements that refer to \railnonterm{vars} or
1.460 + \railnonterm{props} typically admit separate typings or namings via
1.461 + another level of iteration, with explicit @{keyword_ref "and"}
1.462 + separators; e.g.\ see @{command "fix"} and @{command "assume"} in
1.463 + \S\ref{sec:proof-context}.
1.464 +*}
1.465 +
1.466 +
1.467 +subsection {* Antiquotations \label{sec:antiq} *}
1.468 +
1.469 +text {*
1.470 + \begin{matharray}{rcl}
1.471 + @{antiquotation_def "theory"} & : & \isarantiq \\
1.472 + @{antiquotation_def "thm"} & : & \isarantiq \\
1.473 + @{antiquotation_def "prop"} & : & \isarantiq \\
1.474 + @{antiquotation_def "term"} & : & \isarantiq \\
1.475 + @{antiquotation_def const} & : & \isarantiq \\
1.476 + @{antiquotation_def abbrev} & : & \isarantiq \\
1.477 + @{antiquotation_def typeof} & : & \isarantiq \\
1.478 + @{antiquotation_def typ} & : & \isarantiq \\
1.479 + @{antiquotation_def thm_style} & : & \isarantiq \\
1.480 + @{antiquotation_def term_style} & : & \isarantiq \\
1.481 + @{antiquotation_def "text"} & : & \isarantiq \\
1.482 + @{antiquotation_def goals} & : & \isarantiq \\
1.483 + @{antiquotation_def subgoals} & : & \isarantiq \\
1.484 + @{antiquotation_def prf} & : & \isarantiq \\
1.485 + @{antiquotation_def full_prf} & : & \isarantiq \\
1.486 + @{antiquotation_def ML} & : & \isarantiq \\
1.487 + @{antiquotation_def ML_type} & : & \isarantiq \\
1.488 + @{antiquotation_def ML_struct} & : & \isarantiq \\
1.489 + \end{matharray}
1.490 +
1.491 + The text body of formal comments (see also \S\ref{sec:comments}) may
1.492 + contain antiquotations of logical entities, such as theorems, terms
1.493 + and types, which are to be presented in the final output produced by
1.494 + the Isabelle document preparation system (see also
1.495 + \S\ref{sec:document-prep}).
1.496 +
1.497 + Thus embedding of ``@{text "@{term [show_types] \"f x = a + x\"}"}''
1.498 + within a text block would cause
1.499 + \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
1.500 + antiquotations may involve attributes as well. For example,
1.501 + \texttt{{\at}{\ttlbrace}thm~sym~[no_vars]{\ttrbrace}} would print
1.502 + the statement where all schematic variables have been replaced by
1.503 + fixed ones, which are easier to read.
1.504 +
1.505 + \begin{rail}
1.506 + atsign lbrace antiquotation rbrace
1.507 + ;
1.508 +
1.509 + antiquotation:
1.510 + 'theory' options name |
1.511 + 'thm' options thmrefs |
1.512 + 'prop' options prop |
1.513 + 'term' options term |
1.514 + 'const' options term |
1.515 + 'abbrev' options term |
1.516 + 'typeof' options term |
1.517 + 'typ' options type |
1.518 + 'thm\_style' options name thmref |
1.519 + 'term\_style' options name term |
1.520 + 'text' options name |
1.521 + 'goals' options |
1.522 + 'subgoals' options |
1.523 + 'prf' options thmrefs |
1.524 + 'full\_prf' options thmrefs |
1.525 + 'ML' options name |
1.526 + 'ML\_type' options name |
1.527 + 'ML\_struct' options name
1.528 + ;
1.529 + options: '[' (option * ',') ']'
1.530 + ;
1.531 + option: name | name '=' name
1.532 + ;
1.533 + \end{rail}
1.534 +
1.535 + Note that the syntax of antiquotations may \emph{not} include source
1.536 + comments \texttt{(*~\dots~*)} or verbatim text
1.537 + \verb|{*|~\dots~\verb|*|\verb|}|.
1.538 +
1.539 + \begin{descr}
1.540 +
1.541 + \item [@{text "@{theory A}"}] prints the name @{text "A"}, which is
1.542 + guaranteed to refer to a valid ancestor theory in the current
1.543 + context.
1.544 +
1.545 + \item [@{text "@{thm a\<^sub>1 \<dots> a\<^sub>n}"}] prints theorems @{text
1.546 + "a\<^sub>1 \<dots> a\<^sub>n"}. Note that attribute specifications may be
1.547 + included as well (see also \S\ref{sec:syn-att}); the @{attribute_ref
1.548 + no_vars} rule (see \S\ref{sec:misc-meth-att}) would be particularly
1.549 + useful to suppress printing of schematic variables.
1.550 +
1.551 + \item [@{text "@{prop \<phi>}"}] prints a well-typed proposition @{text
1.552 + "\<phi>"}.
1.553 +
1.554 + \item [@{text "@{term t}"}] prints a well-typed term @{text "t"}.
1.555 +
1.556 + \item [@{text "@{const c}"}] prints a logical or syntactic constant
1.557 + @{text "c"}.
1.558 +
1.559 + \item [@{text "@{abbrev c x\<^sub>1 \<dots> x\<^sub>n}"}] prints a constant
1.560 + abbreviation @{text "c x\<^sub>1 \<dots> x\<^sub>n \<equiv> rhs"} as defined in
1.561 + the current context.
1.562 +
1.563 + \item [@{text "@{typeof t}"}] prints the type of a well-typed term
1.564 + @{text "t"}.
1.565 +
1.566 + \item [@{text "@{typ \<tau>}"}] prints a well-formed type @{text "\<tau>"}.
1.567 +
1.568 + \item [@{text "@{thm_style s a}"}] prints theorem @{text a},
1.569 + previously applying a style @{text s} to it (see below).
1.570 +
1.571 + \item [@{text "@{term_style s t}"}] prints a well-typed term @{text
1.572 + t} after applying a style @{text s} to it (see below).
1.573 +
1.574 + \item [@{text "@{text s}"}] prints uninterpreted source text @{text
1.575 + s}. This is particularly useful to print portions of text according
1.576 + to the Isabelle {\LaTeX} output style, without demanding
1.577 + well-formedness (e.g.\ small pieces of terms that should not be
1.578 + parsed or type-checked yet).
1.579 +
1.580 + \item [@{text "@{goals}"}] prints the current \emph{dynamic} goal
1.581 + state. This is mainly for support of tactic-emulation scripts
1.582 + within Isar --- presentation of goal states does not conform to
1.583 + actual human-readable proof documents.
1.584 +
1.585 + Please do not include goal states into document output unless you
1.586 + really know what you are doing!
1.587 +
1.588 + \item [@{text "@{subgoals}"}] is similar to @{text "@{goals}"}, but
1.589 + does not print the main goal.
1.590 +
1.591 + \item [@{text "@{prf a\<^sub>1 \<dots> a\<^sub>n}"}] prints the (compact)
1.592 + proof terms corresponding to the theorems @{text "a\<^sub>1 \<dots>
1.593 + a\<^sub>n"}. Note that this requires proof terms to be switched on
1.594 + for the current object logic (see the ``Proof terms'' section of the
1.595 + Isabelle reference manual for information on how to do this).
1.596 +
1.597 + \item [@{text "@{full_prf a\<^sub>1 \<dots> a\<^sub>n}"}] is like @{text
1.598 + "@{prf a\<^sub>1 \<dots> a\<^sub>n}"}, but displays the full proof terms,
1.599 + i.e.\ also displays information omitted in the compact proof term,
1.600 + which is denoted by ``$_$'' placeholders there.
1.601 +
1.602 + \item [@{text "@{ML s}"}, @{text "@{ML_type s}"}, and @{text
1.603 + "@{ML_struct s}"}] check text @{text s} as ML value, type, and
1.604 + structure, respectively. The source is displayed verbatim.
1.605 +
1.606 + \end{descr}
1.607 +
1.608 + \medskip The following standard styles for use with @{text
1.609 + thm_style} and @{text term_style} are available:
1.610 +
1.611 + \begin{descr}
1.612 +
1.613 + \item [@{text lhs}] extracts the first argument of any application
1.614 + form with at least two arguments -- typically meta-level or
1.615 + object-level equality, or any other binary relation.
1.616 +
1.617 + \item [@{text rhs}] is like @{text lhs}, but extracts the second
1.618 + argument.
1.619 +
1.620 + \item [@{text "concl"}] extracts the conclusion @{text C} from a rule
1.621 + in Horn-clause normal form @{text "A\<^sub>1 \<Longrightarrow> \<dots> A\<^sub>n \<Longrightarrow> C"}.
1.622 +
1.623 + \item [@{text "prem1"}, \dots, @{text "prem9"}] extract premise
1.624 + number $1$, \dots, $9$, respectively, from from a rule in
1.625 + Horn-clause normal form @{text "A\<^sub>1 \<Longrightarrow> \<dots> A\<^sub>n \<Longrightarrow> C"}
1.626 +
1.627 + \end{descr}
1.628 +
1.629 + \medskip
1.630 + The following options are available to tune the output. Note that most of
1.631 + these coincide with ML flags of the same names (see also \cite{isabelle-ref}).
1.632 +
1.633 + \begin{descr}
1.634 +
1.635 + \item[@{text "show_types = bool"} and @{text "show_sorts = bool"}]
1.636 + control printing of explicit type and sort constraints.
1.637 +
1.638 + \item[@{text "show_structs = bool"}] controls printing of implicit
1.639 + structures.
1.640 +
1.641 + \item[@{text "long_names = bool"}] forces names of types and
1.642 + constants etc.\ to be printed in their fully qualified internal
1.643 + form.
1.644 +
1.645 + \item[@{text "short_names = bool"}] forces names of types and
1.646 + constants etc.\ to be printed unqualified. Note that internalizing
1.647 + the output again in the current context may well yield a different
1.648 + result.
1.649 +
1.650 + \item[@{text "unique_names = bool"}] determines whether the printed
1.651 + version of qualified names should be made sufficiently long to avoid
1.652 + overlap with names declared further back. Set to @{text false} for
1.653 + more concise output.
1.654 +
1.655 + \item[@{text "eta_contract = bool"}] prints terms in @{text
1.656 + \<eta>}-contracted form.
1.657 +
1.658 + \item[@{text "display = bool"}] indicates if the text is to be
1.659 + output as multi-line ``display material'', rather than a small piece
1.660 + of text without line breaks (which is the default).
1.661 +
1.662 + \item[@{text "break = bool"}] controls line breaks in non-display
1.663 + material.
1.664 +
1.665 + \item[@{text "quotes = bool"}] indicates if the output should be
1.666 + enclosed in double quotes.
1.667 +
1.668 + \item[@{text "mode = name"}] adds @{text name} to the print mode to
1.669 + be used for presentation (see also \cite{isabelle-ref}). Note that
1.670 + the standard setup for {\LaTeX} output is already present by
1.671 + default, including the modes @{text latex} and @{text xsymbols}.
1.672 +
1.673 + \item[@{text "margin = nat"} and @{text "indent = nat"}] change the
1.674 + margin or indentation for pretty printing of display material.
1.675 +
1.676 + \item[@{text "source = bool"}] prints the source text of the
1.677 + antiquotation arguments, rather than the actual value. Note that
1.678 + this does not affect well-formedness checks of @{antiquotation
1.679 + "thm"}, @{antiquotation "term"}, etc. (only the @{antiquotation
1.680 + "text"} antiquotation admits arbitrary output).
1.681 +
1.682 + \item[@{text "goals_limit = nat"}] determines the maximum number of
1.683 + goals to be printed.
1.684 +
1.685 + \item[@{text "locale = name"}] specifies an alternative locale
1.686 + context used for evaluating and printing the subsequent argument.
1.687 +
1.688 + \end{descr}
1.689 +
1.690 + For boolean flags, ``@{text "name = true"}'' may be abbreviated as
1.691 + ``@{text name}''. All of the above flags are disabled by default,
1.692 + unless changed from ML.
1.693 +
1.694 + \medskip Note that antiquotations do not only spare the author from
1.695 + tedious typing of logical entities, but also achieve some degree of
1.696 + consistency-checking of informal explanations with formal
1.697 + developments: well-formedness of terms and types with respect to the
1.698 + current theory or proof context is ensured here.
1.699 +*}
1.700 +
1.701 +
1.702 +subsection {* Tagged commands \label{sec:tags} *}
1.703 +
1.704 +text {*
1.705 + Each Isabelle/Isar command may be decorated by presentation tags:
1.706 +
1.707 + \indexouternonterm{tags}
1.708 + \begin{rail}
1.709 + tags: ( tag * )
1.710 + ;
1.711 + tag: '\%' (ident | string)
1.712 + \end{rail}
1.713 +
1.714 + The tags @{text "theory"}, @{text "proof"}, @{text "ML"} are already
1.715 + pre-declared for certain classes of commands:
1.716 +
1.717 + \medskip
1.718 +
1.719 + \begin{tabular}{ll}
1.720 + @{text "theory"} & theory begin/end \\
1.721 + @{text "proof"} & all proof commands \\
1.722 + @{text "ML"} & all commands involving ML code \\
1.723 + \end{tabular}
1.724 +
1.725 + \medskip The Isabelle document preparation system (see also
1.726 + \cite{isabelle-sys}) allows tagged command regions to be presented
1.727 + specifically, e.g.\ to fold proof texts, or drop parts of the text
1.728 + completely.
1.729 +
1.730 + For example ``@{command "by"}~@{text "%invisible auto"}'' would
1.731 + cause that piece of proof to be treated as @{text invisible} instead
1.732 + of @{text "proof"} (the default), which may be either show or hidden
1.733 + depending on the document setup. In contrast, ``@{command
1.734 + "by"}~@{text "%visible auto"}'' would force this text to be shown
1.735 + invariably.
1.736 +
1.737 + Explicit tag specifications within a proof apply to all subsequent
1.738 + commands of the same level of nesting. For example, ``@{command
1.739 + "proof"}~@{text "%visible \<dots>"}~@{command "qed"}'' would force the
1.740 + whole sub-proof to be typeset as @{text visible} (unless some of its
1.741 + parts are tagged differently).
1.742 +*}
1.743 +
1.744 +end