1.1 --- a/doc-src/IsarRef/IsaMakefile Mon Apr 28 13:41:04 2008 +0200
1.2 +++ b/doc-src/IsarRef/IsaMakefile Mon Apr 28 14:22:42 2008 +0200
1.3 @@ -21,7 +21,8 @@
1.4
1.5 Thy: $(LOG)/Pure-Thy.gz
1.6
1.7 -$(LOG)/Pure-Thy.gz: Thy/ROOT.ML ../antiquote_setup.ML Thy/intro.thy
1.8 +$(LOG)/Pure-Thy.gz: Thy/ROOT.ML ../antiquote_setup.ML Thy/intro.thy \
1.9 + Thy/syntax.thy
1.10 @$(USEDIR) Pure Thy
1.11
1.12
2.1 --- a/doc-src/IsarRef/Makefile Mon Apr 28 13:41:04 2008 +0200
2.2 +++ b/doc-src/IsarRef/Makefile Mon Apr 28 14:22:42 2008 +0200
2.3 @@ -13,7 +13,7 @@
2.4
2.5 NAME = isar-ref
2.6
2.7 -FILES = isar-ref.tex Thy/document/intro.tex basics.tex syntax.tex pure.tex \
2.8 +FILES = isar-ref.tex Thy/document/intro.tex basics.tex Thy/document/syntax.tex pure.tex \
2.9 generic.tex logics.tex refcard.tex conversion.tex \
2.10 ../isar.sty ../rail.sty ../railsetup.sty ../proof.sty \
2.11 ../iman.sty ../extra.sty ../ttbox.sty ../manual.bib
3.1 --- a/doc-src/IsarRef/Thy/ROOT.ML Mon Apr 28 13:41:04 2008 +0200
3.2 +++ b/doc-src/IsarRef/Thy/ROOT.ML Mon Apr 28 14:22:42 2008 +0200
3.3 @@ -3,3 +3,4 @@
3.4
3.5 use "../../antiquote_setup.ML";
3.6 use_thy "intro";
3.7 +use_thy "syntax";
4.1 --- a/doc-src/IsarRef/Thy/document/session.tex Mon Apr 28 13:41:04 2008 +0200
4.2 +++ b/doc-src/IsarRef/Thy/document/session.tex Mon Apr 28 14:22:42 2008 +0200
4.3 @@ -1,5 +1,7 @@
4.4 \input{intro.tex}
4.5
4.6 +\input{syntax.tex}
4.7 +
4.8 %%% Local Variables:
4.9 %%% mode: latex
4.10 %%% TeX-master: "root"
5.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
5.2 +++ b/doc-src/IsarRef/Thy/document/syntax.tex Mon Apr 28 14:22:42 2008 +0200
5.3 @@ -0,0 +1,785 @@
5.4 +%
5.5 +\begin{isabellebody}%
5.6 +\def\isabellecontext{syntax}%
5.7 +%
5.8 +\isadelimtheory
5.9 +\isanewline
5.10 +%
5.11 +\endisadelimtheory
5.12 +%
5.13 +\isatagtheory
5.14 +\isacommand{theory}\isamarkupfalse%
5.15 +\ {\isachardoublequoteopen}syntax{\isachardoublequoteclose}\isanewline
5.16 +\isakeyword{imports}\ CPure\isanewline
5.17 +\isakeyword{begin}%
5.18 +\endisatagtheory
5.19 +{\isafoldtheory}%
5.20 +%
5.21 +\isadelimtheory
5.22 +%
5.23 +\endisadelimtheory
5.24 +%
5.25 +\isamarkupchapter{Syntax primitives%
5.26 +}
5.27 +\isamarkuptrue%
5.28 +%
5.29 +\begin{isamarkuptext}%
5.30 +The rather generic framework of Isabelle/Isar syntax emerges from
5.31 + three main syntactic categories: \emph{commands} of the top-level
5.32 + Isar engine (covering theory and proof elements), \emph{methods} for
5.33 + general goal refinements (analogous to traditional ``tactics''), and
5.34 + \emph{attributes} for operations on facts (within a certain
5.35 + context). Subsequently we give a reference of basic syntactic
5.36 + entities underlying Isabelle/Isar syntax in a bottom-up manner.
5.37 + Concrete theory and proof language elements will be introduced later
5.38 + on.
5.39 +
5.40 + \medskip In order to get started with writing well-formed
5.41 + Isabelle/Isar documents, the most important aspect to be noted is
5.42 + the difference of \emph{inner} versus \emph{outer} syntax. Inner
5.43 + syntax is that of Isabelle types and terms of the logic, while outer
5.44 + syntax is that of Isabelle/Isar theory sources (specifications and
5.45 + proofs). As a general rule, inner syntax entities may occur only as
5.46 + \emph{atomic entities} within outer syntax. For example, the string
5.47 + \texttt{"x + y"} and identifier \texttt{z} are legal term
5.48 + specifications within a theory, while \texttt{x + y} is not.
5.49 +
5.50 + Printed theory documents usually omit quotes to gain readability
5.51 + (this is a matter of {\LaTeX} macro setup, say via
5.52 + \verb,\isabellestyle,, see also \cite{isabelle-sys}). Experienced
5.53 + users of Isabelle/Isar may easily reconstruct the lost technical
5.54 + information, while mere readers need not care about quotes at all.
5.55 +
5.56 + \medskip Isabelle/Isar input may contain any number of input
5.57 + termination characters ``\texttt{;}'' (semicolon) to separate
5.58 + commands explicitly. This is particularly useful in interactive
5.59 + shell sessions to make clear where the current command is intended
5.60 + to end. Otherwise, the interpreter loop will continue to issue a
5.61 + secondary prompt ``\verb,#,'' until an end-of-command is clearly
5.62 + recognized from the input syntax, e.g.\ encounter of the next
5.63 + command keyword.
5.64 +
5.65 + More advanced interfaces such as Proof~General \cite{proofgeneral}
5.66 + do not require explicit semicolons, the amount of input text is
5.67 + determined automatically by inspecting the present content of the
5.68 + Emacs text buffer. In the printed presentation of Isabelle/Isar
5.69 + documents semicolons are omitted altogether for readability.
5.70 +
5.71 + \begin{warn}
5.72 + Proof~General requires certain syntax classification tables in
5.73 + order to achieve properly synchronized interaction with the
5.74 + Isabelle/Isar process. These tables need to be consistent with
5.75 + the Isabelle version and particular logic image to be used in a
5.76 + running session (common object-logics may well change the outer
5.77 + syntax). The standard setup should work correctly with any of the
5.78 + ``official'' logic images derived from Isabelle/HOL (including
5.79 + HOLCF etc.). Users of alternative logics may need to tell
5.80 + Proof~General explicitly, e.g.\ by giving an option \verb,-k ZF,
5.81 + (in conjunction with \verb,-l ZF, to specify the default logic
5.82 + image).
5.83 + \end{warn}%
5.84 +\end{isamarkuptext}%
5.85 +\isamarkuptrue%
5.86 +%
5.87 +\isamarkupsection{Lexical matters \label{sec:lex-syntax}%
5.88 +}
5.89 +\isamarkuptrue%
5.90 +%
5.91 +\begin{isamarkuptext}%
5.92 +The Isabelle/Isar outer syntax provides token classes as presented
5.93 + below; most of these coincide with the inner lexical syntax as
5.94 + presented in \cite{isabelle-ref}.
5.95 +
5.96 + \begin{matharray}{rcl}
5.97 + \indexdef{}{syntax}{ident}\isa{ident} & = & letter\,quasiletter^* \\
5.98 + \indexdef{}{syntax}{longident}\isa{longident} & = & ident (\verb,.,ident)^+ \\
5.99 + \indexdef{}{syntax}{symident}\isa{symident} & = & sym^+ ~|~ \verb,\,\verb,<,ident\verb,>, \\
5.100 + \indexdef{}{syntax}{nat}\isa{nat} & = & digit^+ \\
5.101 + \indexdef{}{syntax}{var}\isa{var} & = & ident ~|~ \verb,?,ident ~|~ \verb,?,ident\verb,.,nat \\
5.102 + \indexdef{}{syntax}{typefree}\isa{typefree} & = & \verb,',ident \\
5.103 + \indexdef{}{syntax}{typevar}\isa{typevar} & = & typefree ~|~ \verb,?,typefree ~|~ \verb,?,typefree\verb,.,nat \\
5.104 + \indexdef{}{syntax}{string}\isa{string} & = & \verb,", ~\dots~ \verb,", \\
5.105 + \indexdef{}{syntax}{altstring}\isa{altstring} & = & \backquote ~\dots~ \backquote \\
5.106 + \indexdef{}{syntax}{verbatim}\isa{verbatim} & = & \verb,{*, ~\dots~ \verb,*,\verb,}, \\[1ex]
5.107 +
5.108 + letter & = & latin ~|~ \verb,\,\verb,<,latin\verb,>, ~|~ \verb,\,\verb,<,latin\,latin\verb,>, ~|~ greek ~|~ \\
5.109 + & & \verb,\<^isub>, ~|~ \verb,\<^isup>, \\
5.110 + quasiletter & = & letter ~|~ digit ~|~ \verb,_, ~|~ \verb,', \\
5.111 + latin & = & \verb,a, ~|~ \dots ~|~ \verb,z, ~|~ \verb,A, ~|~ \dots ~|~ \verb,Z, \\
5.112 + digit & = & \verb,0, ~|~ \dots ~|~ \verb,9, \\
5.113 + sym & = & \verb,!, ~|~ \verb,#, ~|~ \verb,$, ~|~ \verb,%, ~|~ \verb,&, ~|~
5.114 + \verb,*, ~|~ \verb,+, ~|~ \verb,-, ~|~ \verb,/, ~|~ \\
5.115 + & & \verb,<, ~|~ \verb,=, ~|~ \verb,>, ~|~ \verb,?, ~|~ \texttt{\at} ~|~
5.116 + \verb,^, ~|~ \verb,_, ~|~ \verb,|, ~|~ \verb,~, \\
5.117 + greek & = & \verb,\<alpha>, ~|~ \verb,\<beta>, ~|~ \verb,\<gamma>, ~|~ \verb,\<delta>, ~| \\
5.118 + & & \verb,\<epsilon>, ~|~ \verb,\<zeta>, ~|~ \verb,\<eta>, ~|~ \verb,\<theta>, ~| \\
5.119 + & & \verb,\<iota>, ~|~ \verb,\<kappa>, ~|~ \verb,\<mu>, ~|~ \verb,\<nu>, ~| \\
5.120 + & & \verb,\<xi>, ~|~ \verb,\<pi>, ~|~ \verb,\<rho>, ~|~ \verb,\<sigma>, ~|~ \verb,\<tau>, ~| \\
5.121 + & & \verb,\<upsilon>, ~|~ \verb,\<phi>, ~|~ \verb,\<chi>, ~|~ \verb,\<psi>, ~| \\
5.122 + & & \verb,\<omega>, ~|~ \verb,\<Gamma>, ~|~ \verb,\<Delta>, ~|~ \verb,\<Theta>, ~| \\
5.123 + & & \verb,\<Lambda>, ~|~ \verb,\<Xi>, ~|~ \verb,\<Pi>, ~|~ \verb,\<Sigma>, ~| \\
5.124 + & & \verb,\<Upsilon>, ~|~ \verb,\<Phi>, ~|~ \verb,\<Psi>, ~|~ \verb,\<Omega>, \\
5.125 + \end{matharray}
5.126 +
5.127 + The syntax of \isa{string} admits any characters, including
5.128 + newlines; ``\verb|"|'' (double-quote) and ``\verb|\|'' (backslash)
5.129 + need to be escaped by a backslash; arbitrary character codes may be
5.130 + specified as ``\verb|\|$ddd$'', with 3 decimal digits. Alternative
5.131 + strings according to \isa{altstring} are analogous, using single
5.132 + back-quotes instead. The body of \isa{verbatim} may consist of
5.133 + any text not containing ``\verb,*,\verb,},''; this allows convenient
5.134 + inclusion of quotes without further escapes. The greek letters do
5.135 + \emph{not} include \verb,\<lambda>,, which is already used differently in
5.136 + the meta-logic.
5.137 +
5.138 + Common mathematical symbols such as \isa{{\isasymforall}} are represented in
5.139 + Isabelle as \verb,\<forall>,. There are infinitely many Isabelle symbols
5.140 + like this, although proper presentation is left to front-end tools
5.141 + such as {\LaTeX} or Proof~General with the X-Symbol package. A list
5.142 + of standard Isabelle symbols that work well with these tools is
5.143 + given in \cite[appendix~A]{isabelle-sys}.
5.144 +
5.145 + Source comments take the form \texttt{(*~\dots~*)} and may be
5.146 + nested, although user-interface tools might prevent this. Note that
5.147 + \texttt{(*~\dots~*)} indicate source comments only, which are
5.148 + stripped after lexical analysis of the input. The Isar document
5.149 + syntax also provides formal comments that are considered as part of
5.150 + the text (see \S\ref{sec:comments}).%
5.151 +\end{isamarkuptext}%
5.152 +\isamarkuptrue%
5.153 +%
5.154 +\isamarkupsection{Common syntax entities%
5.155 +}
5.156 +\isamarkuptrue%
5.157 +%
5.158 +\begin{isamarkuptext}%
5.159 +We now introduce several basic syntactic entities, such as names,
5.160 + terms, and theorem specifications, which are factored out of the
5.161 + actual Isar language elements to be described later.%
5.162 +\end{isamarkuptext}%
5.163 +\isamarkuptrue%
5.164 +%
5.165 +\isamarkupsubsection{Names%
5.166 +}
5.167 +\isamarkuptrue%
5.168 +%
5.169 +\begin{isamarkuptext}%
5.170 +Entity \railqtok{name} usually refers to any name of types,
5.171 + constants, theorems etc.\ that are to be \emph{declared} or
5.172 + \emph{defined} (so qualified identifiers are excluded here). Quoted
5.173 + strings provide an escape for non-identifier names or those ruled
5.174 + out by outer syntax keywords (e.g.\ \verb|"let"|). Already existing
5.175 + objects are usually referenced by \railqtok{nameref}.
5.176 +
5.177 + \indexoutertoken{name}\indexoutertoken{parname}\indexoutertoken{nameref}
5.178 + \indexoutertoken{int}
5.179 + \begin{rail}
5.180 + name: ident | symident | string | nat
5.181 + ;
5.182 + parname: '(' name ')'
5.183 + ;
5.184 + nameref: name | longident
5.185 + ;
5.186 + int: nat | '-' nat
5.187 + ;
5.188 + \end{rail}%
5.189 +\end{isamarkuptext}%
5.190 +\isamarkuptrue%
5.191 +%
5.192 +\isamarkupsubsection{Comments \label{sec:comments}%
5.193 +}
5.194 +\isamarkuptrue%
5.195 +%
5.196 +\begin{isamarkuptext}%
5.197 +Large chunks of plain \railqtok{text} are usually given
5.198 + \railtok{verbatim}, i.e.\ enclosed in
5.199 + \verb,{,\verb,*,~\dots~\verb,*,\verb,},. For convenience, any of
5.200 + the smaller text units conforming to \railqtok{nameref} are admitted
5.201 + as well. A marginal \railnonterm{comment} is of the form
5.202 + \texttt{--} \railqtok{text}. Any number of these may occur within
5.203 + Isabelle/Isar commands.
5.204 +
5.205 + \indexoutertoken{text}\indexouternonterm{comment}
5.206 + \begin{rail}
5.207 + text: verbatim | nameref
5.208 + ;
5.209 + comment: '--' text
5.210 + ;
5.211 + \end{rail}%
5.212 +\end{isamarkuptext}%
5.213 +\isamarkuptrue%
5.214 +%
5.215 +\isamarkupsubsection{Type classes, sorts and arities%
5.216 +}
5.217 +\isamarkuptrue%
5.218 +%
5.219 +\begin{isamarkuptext}%
5.220 +Classes are specified by plain names. Sorts have a very simple
5.221 + inner syntax, which is either a single class name \isa{c} or a
5.222 + list \isa{{\isacharbraceleft}c\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ c\isactrlsub n{\isacharbraceright}} referring to the
5.223 + intersection of these classes. The syntax of type arities is given
5.224 + directly at the outer level.
5.225 +
5.226 + \railalias{subseteq}{\isasymsubseteq}
5.227 + \railterm{subseteq}
5.228 +
5.229 + \indexouternonterm{sort}\indexouternonterm{arity}
5.230 + \indexouternonterm{classdecl}
5.231 + \begin{rail}
5.232 + classdecl: name (('<' | subseteq) (nameref + ','))?
5.233 + ;
5.234 + sort: nameref
5.235 + ;
5.236 + arity: ('(' (sort + ',') ')')? sort
5.237 + ;
5.238 + \end{rail}%
5.239 +\end{isamarkuptext}%
5.240 +\isamarkuptrue%
5.241 +%
5.242 +\isamarkupsubsection{Types and terms \label{sec:types-terms}%
5.243 +}
5.244 +\isamarkuptrue%
5.245 +%
5.246 +\begin{isamarkuptext}%
5.247 +The actual inner Isabelle syntax, that of types and terms of the
5.248 + logic, is far too sophisticated in order to be modelled explicitly
5.249 + at the outer theory level. Basically, any such entity has to be
5.250 + quoted to turn it into a single token (the parsing and type-checking
5.251 + is performed internally later). For convenience, a slightly more
5.252 + liberal convention is adopted: quotes may be omitted for any type or
5.253 + term that is already atomic at the outer level. For example, one
5.254 + may just write \texttt{x} instead of \texttt{"x"}. Note that
5.255 + symbolic identifiers (e.g.\ \texttt{++} or \isa{{\isasymforall}} are available
5.256 + as well, provided these have not been superseded by commands or
5.257 + other keywords already (e.g.\ \texttt{=} or \texttt{+}).
5.258 +
5.259 + \indexoutertoken{type}\indexoutertoken{term}\indexoutertoken{prop}
5.260 + \begin{rail}
5.261 + type: nameref | typefree | typevar
5.262 + ;
5.263 + term: nameref | var
5.264 + ;
5.265 + prop: term
5.266 + ;
5.267 + \end{rail}
5.268 +
5.269 + Positional instantiations are indicated by giving a sequence of
5.270 + terms, or the placeholder ``$\_$'' (underscore), which means to skip
5.271 + a position.
5.272 +
5.273 + \indexoutertoken{inst}\indexoutertoken{insts}
5.274 + \begin{rail}
5.275 + inst: underscore | term
5.276 + ;
5.277 + insts: (inst *)
5.278 + ;
5.279 + \end{rail}
5.280 +
5.281 + Type declarations and definitions usually refer to
5.282 + \railnonterm{typespec} on the left-hand side. This models basic
5.283 + type constructor application at the outer syntax level. Note that
5.284 + only plain postfix notation is available here, but no infixes.
5.285 +
5.286 + \indexouternonterm{typespec}
5.287 + \begin{rail}
5.288 + typespec: (() | typefree | '(' ( typefree + ',' ) ')') name
5.289 + ;
5.290 + \end{rail}%
5.291 +\end{isamarkuptext}%
5.292 +\isamarkuptrue%
5.293 +%
5.294 +\isamarkupsubsection{Mixfix annotations%
5.295 +}
5.296 +\isamarkuptrue%
5.297 +%
5.298 +\begin{isamarkuptext}%
5.299 +Mixfix annotations specify concrete \emph{inner} syntax of Isabelle
5.300 + types and terms. Some commands such as \isa{types} (see
5.301 + \S\ref{sec:types-pure}) admit infixes only, while \isa{consts} (see \S\ref{sec:consts}) and \isa{syntax} (see
5.302 + \S\ref{sec:syn-trans}) support the full range of general mixfixes
5.303 + and binders.
5.304 +
5.305 + \indexouternonterm{infix}\indexouternonterm{mixfix}\indexouternonterm{structmixfix}
5.306 + \begin{rail}
5.307 + infix: '(' ('infix' | 'infixl' | 'infixr') string? nat ')'
5.308 + ;
5.309 + mixfix: infix | '(' string prios? nat? ')' | '(' 'binder' string prios? nat ')'
5.310 + ;
5.311 + structmixfix: mixfix | '(' 'structure' ')'
5.312 + ;
5.313 +
5.314 + prios: '[' (nat + ',') ']'
5.315 + ;
5.316 + \end{rail}
5.317 +
5.318 + Here the \railtok{string} specifications refer to the actual mixfix
5.319 + template (see also \cite{isabelle-ref}), which may include literal
5.320 + text, spacing, blocks, and arguments (denoted by ``$_$''); the
5.321 + special symbol \verb,\<index>, (printed as ``\i'') represents an index
5.322 + argument that specifies an implicit structure reference (see also
5.323 + \S\ref{sec:locale}). Infix and binder declarations provide common
5.324 + abbreviations for particular mixfix declarations. So in practice,
5.325 + mixfix templates mostly degenerate to literal text for concrete
5.326 + syntax, such as ``\verb,++,'' for an infix symbol, or
5.327 + ``\verb,++,\i'' for an infix of an implicit structure.%
5.328 +\end{isamarkuptext}%
5.329 +\isamarkuptrue%
5.330 +%
5.331 +\isamarkupsubsection{Proof methods \label{sec:syn-meth}%
5.332 +}
5.333 +\isamarkuptrue%
5.334 +%
5.335 +\begin{isamarkuptext}%
5.336 +Proof methods are either basic ones, or expressions composed of
5.337 + methods via ``\texttt{,}'' (sequential composition), ``\texttt{|}''
5.338 + (alternative choices), ``\texttt{?}'' (try), ``\texttt{+}'' (repeat
5.339 + at least once), ``\texttt{[$n$]}'' (restriction to first \isa{n}
5.340 + sub-goals, default $n = 1$). In practice, proof methods are usually
5.341 + just a comma separated list of \railqtok{nameref}~\railnonterm{args}
5.342 + specifications. Note that parentheses may be dropped for single
5.343 + method specifications (with no arguments).
5.344 +
5.345 + \indexouternonterm{method}
5.346 + \begin{rail}
5.347 + method: (nameref | '(' methods ')') (() | '?' | '+' | '[' nat? ']')
5.348 + ;
5.349 + methods: (nameref args | method) + (',' | '|')
5.350 + ;
5.351 + \end{rail}
5.352 +
5.353 + Proper Isar proof methods do \emph{not} admit arbitrary goal
5.354 + addressing, but refer either to the first sub-goal or all sub-goals
5.355 + uniformly. The goal restriction operator ``\texttt{[$n$]}''
5.356 + evaluates a method expression within a sandbox consisting of the
5.357 + first \isa{n} sub-goals (which need to exist). For example,
5.358 + \isa{simp{\isacharunderscore}all{\isacharbrackleft}{\isadigit{3}}{\isacharbrackright}} simplifies the first three sub-goals, while
5.359 + \isa{{\isacharparenleft}rule\ foo{\isacharcomma}\ simp{\isacharunderscore}all{\isacharparenright}{\isacharbrackleft}{\isacharbrackright}} simplifies all new goals that
5.360 + emerge from applying rule \isa{foo} to the originally first one.
5.361 +
5.362 + Improper methods, notably tactic emulations, offer a separate
5.363 + low-level goal addressing scheme as explicit argument to the
5.364 + individual tactic being involved. Here \isa{{\isacharbrackleft}{\isacharbang}{\isacharbrackright}} refers to all
5.365 + goals, and \isa{{\isacharbrackleft}n{\isacharminus}{\isacharbrackright}} to all goals starting from \isa{n},
5.366 +
5.367 + \indexouternonterm{goalspec}
5.368 + \begin{rail}
5.369 + goalspec: '[' (nat '-' nat | nat '-' | nat | '!' ) ']'
5.370 + ;
5.371 + \end{rail}%
5.372 +\end{isamarkuptext}%
5.373 +\isamarkuptrue%
5.374 +%
5.375 +\isamarkupsubsection{Attributes and theorems \label{sec:syn-att}%
5.376 +}
5.377 +\isamarkuptrue%
5.378 +%
5.379 +\begin{isamarkuptext}%
5.380 +Attributes (and proof methods, see \S\ref{sec:syn-meth}) have their
5.381 + own ``semi-inner'' syntax, in the sense that input conforming to
5.382 + \railnonterm{args} below is parsed by the attribute a second time.
5.383 + The attribute argument specifications may be any sequence of atomic
5.384 + entities (identifiers, strings etc.), or properly bracketed argument
5.385 + lists. Below \railqtok{atom} refers to any atomic entity, including
5.386 + any \railtok{keyword} conforming to \railtok{symident}.
5.387 +
5.388 + \indexoutertoken{atom}\indexouternonterm{args}\indexouternonterm{attributes}
5.389 + \begin{rail}
5.390 + atom: nameref | typefree | typevar | var | nat | keyword
5.391 + ;
5.392 + arg: atom | '(' args ')' | '[' args ']'
5.393 + ;
5.394 + args: arg *
5.395 + ;
5.396 + attributes: '[' (nameref args * ',') ']'
5.397 + ;
5.398 + \end{rail}
5.399 +
5.400 + Theorem specifications come in several flavors:
5.401 + \railnonterm{axmdecl} and \railnonterm{thmdecl} usually refer to
5.402 + axioms, assumptions or results of goal statements, while
5.403 + \railnonterm{thmdef} collects lists of existing theorems. Existing
5.404 + theorems are given by \railnonterm{thmref} and
5.405 + \railnonterm{thmrefs}, the former requires an actual singleton
5.406 + result.
5.407 +
5.408 + There are three forms of theorem references:
5.409 + \begin{enumerate}
5.410 +
5.411 + \item named facts \isa{a}
5.412 +
5.413 + \item selections from named facts \isa{a{\isacharparenleft}i{\isacharcomma}\ j\ {\isacharminus}\ k{\isacharparenright}}
5.414 +
5.415 + \item literal fact propositions using \indexref{}{syntax}{altstring}\isa{altstring} syntax
5.416 + $\backquote\phi\backquote$, (see also method \indexref{}{method}{fact}\isa{fact} in
5.417 + \S\ref{sec:pure-meth-att}).
5.418 +
5.419 + \end{enumerate}
5.420 +
5.421 + Any kind of theorem specification may include lists of attributes
5.422 + both on the left and right hand sides; attributes are applied to any
5.423 + immediately preceding fact. If names are omitted, the theorems are
5.424 + not stored within the theorem database of the theory or proof
5.425 + context, but any given attributes are applied nonetheless.
5.426 +
5.427 + An extra pair of brackets around attribute declarations --- such as
5.428 + ``\isa{{\isacharbrackleft}{\isacharbrackleft}simproc\ a{\isacharbrackright}{\isacharbrackright}}'' --- abbreviates a theorem reference
5.429 + involving an internal dummy fact, which will be ignored later on.
5.430 + So only the effect of the attribute on the background context will
5.431 + persist. This form of in-place declarations is particularly useful
5.432 + with commands like \isa{declare} and \isa{using}.
5.433 +
5.434 + \indexouternonterm{axmdecl}\indexouternonterm{thmdecl}
5.435 + \indexouternonterm{thmdef}\indexouternonterm{thmref}
5.436 + \indexouternonterm{thmrefs}\indexouternonterm{selection}
5.437 + \begin{rail}
5.438 + axmdecl: name attributes? ':'
5.439 + ;
5.440 + thmdecl: thmbind ':'
5.441 + ;
5.442 + thmdef: thmbind '='
5.443 + ;
5.444 + thmref: (nameref selection? | altstring) attributes? | '[' attributes ']'
5.445 + ;
5.446 + thmrefs: thmref +
5.447 + ;
5.448 +
5.449 + thmbind: name attributes | name | attributes
5.450 + ;
5.451 + selection: '(' ((nat | nat '-' nat?) + ',') ')'
5.452 + ;
5.453 + \end{rail}%
5.454 +\end{isamarkuptext}%
5.455 +\isamarkuptrue%
5.456 +%
5.457 +\isamarkupsubsection{Term patterns and declarations \label{sec:term-decls}%
5.458 +}
5.459 +\isamarkuptrue%
5.460 +%
5.461 +\begin{isamarkuptext}%
5.462 +Wherever explicit propositions (or term fragments) occur in a proof
5.463 + text, casual binding of schematic term variables may be given
5.464 + specified via patterns of the form ``\isa{{\isacharparenleft}{\isasymIS}\ p\isactrlsub {\isadigit{1}}\ {\isasymdots}\ p\isactrlsub n{\isacharparenright}}''. This works both for \railqtok{term} and \railqtok{prop}.
5.465 +
5.466 + \indexouternonterm{termpat}\indexouternonterm{proppat}
5.467 + \begin{rail}
5.468 + termpat: '(' ('is' term +) ')'
5.469 + ;
5.470 + proppat: '(' ('is' prop +) ')'
5.471 + ;
5.472 + \end{rail}
5.473 +
5.474 + \medskip Declarations of local variables \isa{x\ {\isacharcolon}{\isacharcolon}\ {\isasymtau}} and
5.475 + logical propositions \isa{a\ {\isacharcolon}\ {\isasymphi}} represent different views on
5.476 + the same principle of introducing a local scope. In practice, one
5.477 + may usually omit the typing of \railnonterm{vars} (due to
5.478 + type-inference), and the naming of propositions (due to implicit
5.479 + references of current facts). In any case, Isar proof elements
5.480 + usually admit to introduce multiple such items simultaneously.
5.481 +
5.482 + \indexouternonterm{vars}\indexouternonterm{props}
5.483 + \begin{rail}
5.484 + vars: (name+) ('::' type)?
5.485 + ;
5.486 + props: thmdecl? (prop proppat? +)
5.487 + ;
5.488 + \end{rail}
5.489 +
5.490 + The treatment of multiple declarations corresponds to the
5.491 + complementary focus of \railnonterm{vars} versus
5.492 + \railnonterm{props}. In ``\isa{x\isactrlsub {\isadigit{1}}\ {\isasymdots}\ x\isactrlsub n\ {\isacharcolon}{\isacharcolon}\ {\isasymtau}}''
5.493 + the typing refers to all variables, while in \isa{a{\isacharcolon}\ {\isasymphi}\isactrlsub {\isadigit{1}}\ {\isasymdots}\ {\isasymphi}\isactrlsub n} the naming refers to all propositions collectively.
5.494 + Isar language elements that refer to \railnonterm{vars} or
5.495 + \railnonterm{props} typically admit separate typings or namings via
5.496 + another level of iteration, with explicit \indexref{}{keyword}{and}\isa{and}
5.497 + separators; e.g.\ see \isa{fix} and \isa{assume} in
5.498 + \S\ref{sec:proof-context}.%
5.499 +\end{isamarkuptext}%
5.500 +\isamarkuptrue%
5.501 +%
5.502 +\isamarkupsubsection{Antiquotations \label{sec:antiq}%
5.503 +}
5.504 +\isamarkuptrue%
5.505 +%
5.506 +\begin{isamarkuptext}%
5.507 +\begin{matharray}{rcl}
5.508 + \indexdef{}{antiquotation}{theory}\isa{theory} & : & \isarantiq \\
5.509 + \indexdef{}{antiquotation}{thm}\isa{thm} & : & \isarantiq \\
5.510 + \indexdef{}{antiquotation}{prop}\isa{prop} & : & \isarantiq \\
5.511 + \indexdef{}{antiquotation}{term}\isa{term} & : & \isarantiq \\
5.512 + \indexdef{}{antiquotation}{const}\isa{const} & : & \isarantiq \\
5.513 + \indexdef{}{antiquotation}{abbrev}\isa{abbrev} & : & \isarantiq \\
5.514 + \indexdef{}{antiquotation}{typeof}\isa{typeof} & : & \isarantiq \\
5.515 + \indexdef{}{antiquotation}{typ}\isa{typ} & : & \isarantiq \\
5.516 + \indexdef{}{antiquotation}{thm-style}\isa{thm{\isacharunderscore}style} & : & \isarantiq \\
5.517 + \indexdef{}{antiquotation}{term-style}\isa{term{\isacharunderscore}style} & : & \isarantiq \\
5.518 + \indexdef{}{antiquotation}{text}\isa{text} & : & \isarantiq \\
5.519 + \indexdef{}{antiquotation}{goals}\isa{goals} & : & \isarantiq \\
5.520 + \indexdef{}{antiquotation}{subgoals}\isa{subgoals} & : & \isarantiq \\
5.521 + \indexdef{}{antiquotation}{prf}\isa{prf} & : & \isarantiq \\
5.522 + \indexdef{}{antiquotation}{full-prf}\isa{full{\isacharunderscore}prf} & : & \isarantiq \\
5.523 + \indexdef{}{antiquotation}{ML}\isa{ML} & : & \isarantiq \\
5.524 + \indexdef{}{antiquotation}{ML-type}\isa{ML{\isacharunderscore}type} & : & \isarantiq \\
5.525 + \indexdef{}{antiquotation}{ML-struct}\isa{ML{\isacharunderscore}struct} & : & \isarantiq \\
5.526 + \end{matharray}
5.527 +
5.528 + The text body of formal comments (see also \S\ref{sec:comments}) may
5.529 + contain antiquotations of logical entities, such as theorems, terms
5.530 + and types, which are to be presented in the final output produced by
5.531 + the Isabelle document preparation system (see also
5.532 + \S\ref{sec:document-prep}).
5.533 +
5.534 + Thus embedding of ``\isa{{\isacharat}{\isacharbraceleft}term\ {\isacharbrackleft}show{\isacharunderscore}types{\isacharbrackright}\ {\isachardoublequote}f\ x\ {\isacharequal}\ a\ {\isacharplus}\ x{\isachardoublequote}{\isacharbraceright}}''
5.535 + within a text block would cause
5.536 + \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
5.537 + antiquotations may involve attributes as well. For example,
5.538 + \texttt{{\at}{\ttlbrace}thm~sym~[no_vars]{\ttrbrace}} would print
5.539 + the statement where all schematic variables have been replaced by
5.540 + fixed ones, which are easier to read.
5.541 +
5.542 + \begin{rail}
5.543 + atsign lbrace antiquotation rbrace
5.544 + ;
5.545 +
5.546 + antiquotation:
5.547 + 'theory' options name |
5.548 + 'thm' options thmrefs |
5.549 + 'prop' options prop |
5.550 + 'term' options term |
5.551 + 'const' options term |
5.552 + 'abbrev' options term |
5.553 + 'typeof' options term |
5.554 + 'typ' options type |
5.555 + 'thm\_style' options name thmref |
5.556 + 'term\_style' options name term |
5.557 + 'text' options name |
5.558 + 'goals' options |
5.559 + 'subgoals' options |
5.560 + 'prf' options thmrefs |
5.561 + 'full\_prf' options thmrefs |
5.562 + 'ML' options name |
5.563 + 'ML\_type' options name |
5.564 + 'ML\_struct' options name
5.565 + ;
5.566 + options: '[' (option * ',') ']'
5.567 + ;
5.568 + option: name | name '=' name
5.569 + ;
5.570 + \end{rail}
5.571 +
5.572 + Note that the syntax of antiquotations may \emph{not} include source
5.573 + comments \texttt{(*~\dots~*)} or verbatim text
5.574 + \verb|{*|~\dots~\verb|*|\verb|}|.
5.575 +
5.576 + \begin{descr}
5.577 +
5.578 + \item [\isa{{\isacharat}{\isacharbraceleft}theory\ A{\isacharbraceright}}] prints the name \isa{A}, which is
5.579 + guaranteed to refer to a valid ancestor theory in the current
5.580 + context.
5.581 +
5.582 + \item [\isa{{\isacharat}{\isacharbraceleft}thm\ a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n{\isacharbraceright}}] prints theorems \isa{a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n}. Note that attribute specifications may be
5.583 + included as well (see also \S\ref{sec:syn-att}); the \indexref{}{attribute}{no-vars}\isa{no{\isacharunderscore}vars} rule (see \S\ref{sec:misc-meth-att}) would be particularly
5.584 + useful to suppress printing of schematic variables.
5.585 +
5.586 + \item [\isa{{\isacharat}{\isacharbraceleft}prop\ {\isasymphi}{\isacharbraceright}}] prints a well-typed proposition \isa{{\isasymphi}}.
5.587 +
5.588 + \item [\isa{{\isacharat}{\isacharbraceleft}term\ t{\isacharbraceright}}] prints a well-typed term \isa{t}.
5.589 +
5.590 + \item [\isa{{\isacharat}{\isacharbraceleft}const\ c{\isacharbraceright}}] prints a logical or syntactic constant
5.591 + \isa{c}.
5.592 +
5.593 + \item [\isa{{\isacharat}{\isacharbraceleft}abbrev\ c\ x\isactrlsub {\isadigit{1}}\ {\isasymdots}\ x\isactrlsub n{\isacharbraceright}}] prints a constant
5.594 + abbreviation \isa{c\ x\isactrlsub {\isadigit{1}}\ {\isasymdots}\ x\isactrlsub n\ {\isasymequiv}\ rhs} as defined in
5.595 + the current context.
5.596 +
5.597 + \item [\isa{{\isacharat}{\isacharbraceleft}typeof\ t{\isacharbraceright}}] prints the type of a well-typed term
5.598 + \isa{t}.
5.599 +
5.600 + \item [\isa{{\isacharat}{\isacharbraceleft}typ\ {\isasymtau}{\isacharbraceright}}] prints a well-formed type \isa{{\isasymtau}}.
5.601 +
5.602 + \item [\isa{{\isacharat}{\isacharbraceleft}thm{\isacharunderscore}style\ s\ a{\isacharbraceright}}] prints theorem \isa{a},
5.603 + previously applying a style \isa{s} to it (see below).
5.604 +
5.605 + \item [\isa{{\isacharat}{\isacharbraceleft}term{\isacharunderscore}style\ s\ t{\isacharbraceright}}] prints a well-typed term \isa{t} after applying a style \isa{s} to it (see below).
5.606 +
5.607 + \item [\isa{{\isacharat}{\isacharbraceleft}text\ s{\isacharbraceright}}] prints uninterpreted source text \isa{s}. This is particularly useful to print portions of text according
5.608 + to the Isabelle {\LaTeX} output style, without demanding
5.609 + well-formedness (e.g.\ small pieces of terms that should not be
5.610 + parsed or type-checked yet).
5.611 +
5.612 + \item [\isa{{\isacharat}{\isacharbraceleft}goals{\isacharbraceright}}] prints the current \emph{dynamic} goal
5.613 + state. This is mainly for support of tactic-emulation scripts
5.614 + within Isar --- presentation of goal states does not conform to
5.615 + actual human-readable proof documents.
5.616 +
5.617 + Please do not include goal states into document output unless you
5.618 + really know what you are doing!
5.619 +
5.620 + \item [\isa{{\isacharat}{\isacharbraceleft}subgoals{\isacharbraceright}}] is similar to \isa{{\isacharat}{\isacharbraceleft}goals{\isacharbraceright}}, but
5.621 + does not print the main goal.
5.622 +
5.623 + \item [\isa{{\isacharat}{\isacharbraceleft}prf\ a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n{\isacharbraceright}}] prints the (compact)
5.624 + proof terms corresponding to the theorems \isa{a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n}. Note that this requires proof terms to be switched on
5.625 + for the current object logic (see the ``Proof terms'' section of the
5.626 + Isabelle reference manual for information on how to do this).
5.627 +
5.628 + \item [\isa{{\isacharat}{\isacharbraceleft}full{\isacharunderscore}prf\ a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n{\isacharbraceright}}] is like \isa{{\isacharat}{\isacharbraceleft}prf\ a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n{\isacharbraceright}}, but displays the full proof terms,
5.629 + i.e.\ also displays information omitted in the compact proof term,
5.630 + which is denoted by ``$_$'' placeholders there.
5.631 +
5.632 + \item [\isa{{\isacharat}{\isacharbraceleft}ML\ s{\isacharbraceright}}, \isa{{\isacharat}{\isacharbraceleft}ML{\isacharunderscore}type\ s{\isacharbraceright}}, and \isa{{\isacharat}{\isacharbraceleft}ML{\isacharunderscore}struct\ s{\isacharbraceright}}] check text \isa{s} as ML value, type, and
5.633 + structure, respectively. The source is displayed verbatim.
5.634 +
5.635 + \end{descr}
5.636 +
5.637 + \medskip The following standard styles for use with \isa{thm{\isacharunderscore}style} and \isa{term{\isacharunderscore}style} are available:
5.638 +
5.639 + \begin{descr}
5.640 +
5.641 + \item [\isa{lhs}] extracts the first argument of any application
5.642 + form with at least two arguments -- typically meta-level or
5.643 + object-level equality, or any other binary relation.
5.644 +
5.645 + \item [\isa{rhs}] is like \isa{lhs}, but extracts the second
5.646 + argument.
5.647 +
5.648 + \item [\isa{concl}] extracts the conclusion \isa{C} from a rule
5.649 + in Horn-clause normal form \isa{A\isactrlsub {\isadigit{1}}\ {\isasymLongrightarrow}\ {\isasymdots}\ A\isactrlsub n\ {\isasymLongrightarrow}\ C}.
5.650 +
5.651 + \item [\isa{prem{\isadigit{1}}}, \dots, \isa{prem{\isadigit{9}}}] extract premise
5.652 + number $1$, \dots, $9$, respectively, from from a rule in
5.653 + Horn-clause normal form \isa{A\isactrlsub {\isadigit{1}}\ {\isasymLongrightarrow}\ {\isasymdots}\ A\isactrlsub n\ {\isasymLongrightarrow}\ C}
5.654 +
5.655 + \end{descr}
5.656 +
5.657 + \medskip
5.658 + The following options are available to tune the output. Note that most of
5.659 + these coincide with ML flags of the same names (see also \cite{isabelle-ref}).
5.660 +
5.661 + \begin{descr}
5.662 +
5.663 + \item[\isa{show{\isacharunderscore}types\ {\isacharequal}\ bool} and \isa{show{\isacharunderscore}sorts\ {\isacharequal}\ bool}]
5.664 + control printing of explicit type and sort constraints.
5.665 +
5.666 + \item[\isa{show{\isacharunderscore}structs\ {\isacharequal}\ bool}] controls printing of implicit
5.667 + structures.
5.668 +
5.669 + \item[\isa{long{\isacharunderscore}names\ {\isacharequal}\ bool}] forces names of types and
5.670 + constants etc.\ to be printed in their fully qualified internal
5.671 + form.
5.672 +
5.673 + \item[\isa{short{\isacharunderscore}names\ {\isacharequal}\ bool}] forces names of types and
5.674 + constants etc.\ to be printed unqualified. Note that internalizing
5.675 + the output again in the current context may well yield a different
5.676 + result.
5.677 +
5.678 + \item[\isa{unique{\isacharunderscore}names\ {\isacharequal}\ bool}] determines whether the printed
5.679 + version of qualified names should be made sufficiently long to avoid
5.680 + overlap with names declared further back. Set to \isa{false} for
5.681 + more concise output.
5.682 +
5.683 + \item[\isa{eta{\isacharunderscore}contract\ {\isacharequal}\ bool}] prints terms in \isa{{\isasymeta}}-contracted form.
5.684 +
5.685 + \item[\isa{display\ {\isacharequal}\ bool}] indicates if the text is to be
5.686 + output as multi-line ``display material'', rather than a small piece
5.687 + of text without line breaks (which is the default).
5.688 +
5.689 + \item[\isa{break\ {\isacharequal}\ bool}] controls line breaks in non-display
5.690 + material.
5.691 +
5.692 + \item[\isa{quotes\ {\isacharequal}\ bool}] indicates if the output should be
5.693 + enclosed in double quotes.
5.694 +
5.695 + \item[\isa{mode\ {\isacharequal}\ name}] adds \isa{name} to the print mode to
5.696 + be used for presentation (see also \cite{isabelle-ref}). Note that
5.697 + the standard setup for {\LaTeX} output is already present by
5.698 + default, including the modes \isa{latex} and \isa{xsymbols}.
5.699 +
5.700 + \item[\isa{margin\ {\isacharequal}\ nat} and \isa{indent\ {\isacharequal}\ nat}] change the
5.701 + margin or indentation for pretty printing of display material.
5.702 +
5.703 + \item[\isa{source\ {\isacharequal}\ bool}] prints the source text of the
5.704 + antiquotation arguments, rather than the actual value. Note that
5.705 + this does not affect well-formedness checks of \isa{thm}, \isa{term}, etc. (only the \isa{text} antiquotation admits arbitrary output).
5.706 +
5.707 + \item[\isa{goals{\isacharunderscore}limit\ {\isacharequal}\ nat}] determines the maximum number of
5.708 + goals to be printed.
5.709 +
5.710 + \item[\isa{locale\ {\isacharequal}\ name}] specifies an alternative locale
5.711 + context used for evaluating and printing the subsequent argument.
5.712 +
5.713 + \end{descr}
5.714 +
5.715 + For boolean flags, ``\isa{name\ {\isacharequal}\ true}'' may be abbreviated as
5.716 + ``\isa{name}''. All of the above flags are disabled by default,
5.717 + unless changed from ML.
5.718 +
5.719 + \medskip Note that antiquotations do not only spare the author from
5.720 + tedious typing of logical entities, but also achieve some degree of
5.721 + consistency-checking of informal explanations with formal
5.722 + developments: well-formedness of terms and types with respect to the
5.723 + current theory or proof context is ensured here.%
5.724 +\end{isamarkuptext}%
5.725 +\isamarkuptrue%
5.726 +%
5.727 +\isamarkupsubsection{Tagged commands \label{sec:tags}%
5.728 +}
5.729 +\isamarkuptrue%
5.730 +%
5.731 +\begin{isamarkuptext}%
5.732 +Each Isabelle/Isar command may be decorated by presentation tags:
5.733 +
5.734 + \indexouternonterm{tags}
5.735 + \begin{rail}
5.736 + tags: ( tag * )
5.737 + ;
5.738 + tag: '\%' (ident | string)
5.739 + \end{rail}
5.740 +
5.741 + The tags \isa{theory}, \isa{proof}, \isa{ML} are already
5.742 + pre-declared for certain classes of commands:
5.743 +
5.744 + \medskip
5.745 +
5.746 + \begin{tabular}{ll}
5.747 + \isa{theory} & theory begin/end \\
5.748 + \isa{proof} & all proof commands \\
5.749 + \isa{ML} & all commands involving ML code \\
5.750 + \end{tabular}
5.751 +
5.752 + \medskip The Isabelle document preparation system (see also
5.753 + \cite{isabelle-sys}) allows tagged command regions to be presented
5.754 + specifically, e.g.\ to fold proof texts, or drop parts of the text
5.755 + completely.
5.756 +
5.757 + For example ``\isa{by}~\isa{{\isacharpercent}invisible\ auto}'' would
5.758 + cause that piece of proof to be treated as \isa{invisible} instead
5.759 + of \isa{proof} (the default), which may be either show or hidden
5.760 + depending on the document setup. In contrast, ``\isa{by}~\isa{{\isacharpercent}visible\ auto}'' would force this text to be shown
5.761 + invariably.
5.762 +
5.763 + Explicit tag specifications within a proof apply to all subsequent
5.764 + commands of the same level of nesting. For example, ``\isa{proof}~\isa{{\isacharpercent}visible\ {\isasymdots}}~\isa{qed}'' would force the
5.765 + whole sub-proof to be typeset as \isa{visible} (unless some of its
5.766 + parts are tagged differently).%
5.767 +\end{isamarkuptext}%
5.768 +\isamarkuptrue%
5.769 +%
5.770 +\isadelimtheory
5.771 +%
5.772 +\endisadelimtheory
5.773 +%
5.774 +\isatagtheory
5.775 +\isacommand{end}\isamarkupfalse%
5.776 +%
5.777 +\endisatagtheory
5.778 +{\isafoldtheory}%
5.779 +%
5.780 +\isadelimtheory
5.781 +%
5.782 +\endisadelimtheory
5.783 +\isanewline
5.784 +\end{isabellebody}%
5.785 +%%% Local Variables:
5.786 +%%% mode: latex
5.787 +%%% TeX-master: "root"
5.788 +%%% End:
6.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
6.2 +++ b/doc-src/IsarRef/Thy/syntax.thy Mon Apr 28 14:22:42 2008 +0200
6.3 @@ -0,0 +1,741 @@
6.4 +
6.5 +theory "syntax"
6.6 +imports CPure
6.7 +begin
6.8 +
6.9 +chapter {* Syntax primitives *}
6.10 +
6.11 +text {*
6.12 + The rather generic framework of Isabelle/Isar syntax emerges from
6.13 + three main syntactic categories: \emph{commands} of the top-level
6.14 + Isar engine (covering theory and proof elements), \emph{methods} for
6.15 + general goal refinements (analogous to traditional ``tactics''), and
6.16 + \emph{attributes} for operations on facts (within a certain
6.17 + context). Subsequently we give a reference of basic syntactic
6.18 + entities underlying Isabelle/Isar syntax in a bottom-up manner.
6.19 + Concrete theory and proof language elements will be introduced later
6.20 + on.
6.21 +
6.22 + \medskip In order to get started with writing well-formed
6.23 + Isabelle/Isar documents, the most important aspect to be noted is
6.24 + the difference of \emph{inner} versus \emph{outer} syntax. Inner
6.25 + syntax is that of Isabelle types and terms of the logic, while outer
6.26 + syntax is that of Isabelle/Isar theory sources (specifications and
6.27 + proofs). As a general rule, inner syntax entities may occur only as
6.28 + \emph{atomic entities} within outer syntax. For example, the string
6.29 + \texttt{"x + y"} and identifier \texttt{z} are legal term
6.30 + specifications within a theory, while \texttt{x + y} is not.
6.31 +
6.32 + Printed theory documents usually omit quotes to gain readability
6.33 + (this is a matter of {\LaTeX} macro setup, say via
6.34 + \verb,\isabellestyle,, see also \cite{isabelle-sys}). Experienced
6.35 + users of Isabelle/Isar may easily reconstruct the lost technical
6.36 + information, while mere readers need not care about quotes at all.
6.37 +
6.38 + \medskip Isabelle/Isar input may contain any number of input
6.39 + termination characters ``\texttt{;}'' (semicolon) to separate
6.40 + commands explicitly. This is particularly useful in interactive
6.41 + shell sessions to make clear where the current command is intended
6.42 + to end. Otherwise, the interpreter loop will continue to issue a
6.43 + secondary prompt ``\verb,#,'' until an end-of-command is clearly
6.44 + recognized from the input syntax, e.g.\ encounter of the next
6.45 + command keyword.
6.46 +
6.47 + More advanced interfaces such as Proof~General \cite{proofgeneral}
6.48 + do not require explicit semicolons, the amount of input text is
6.49 + determined automatically by inspecting the present content of the
6.50 + Emacs text buffer. In the printed presentation of Isabelle/Isar
6.51 + documents semicolons are omitted altogether for readability.
6.52 +
6.53 + \begin{warn}
6.54 + Proof~General requires certain syntax classification tables in
6.55 + order to achieve properly synchronized interaction with the
6.56 + Isabelle/Isar process. These tables need to be consistent with
6.57 + the Isabelle version and particular logic image to be used in a
6.58 + running session (common object-logics may well change the outer
6.59 + syntax). The standard setup should work correctly with any of the
6.60 + ``official'' logic images derived from Isabelle/HOL (including
6.61 + HOLCF etc.). Users of alternative logics may need to tell
6.62 + Proof~General explicitly, e.g.\ by giving an option \verb,-k ZF,
6.63 + (in conjunction with \verb,-l ZF, to specify the default logic
6.64 + image).
6.65 + \end{warn}
6.66 +*}
6.67 +
6.68 +
6.69 +section {* Lexical matters \label{sec:lex-syntax} *}
6.70 +
6.71 +text {*
6.72 + The Isabelle/Isar outer syntax provides token classes as presented
6.73 + below; most of these coincide with the inner lexical syntax as
6.74 + presented in \cite{isabelle-ref}.
6.75 +
6.76 + \begin{matharray}{rcl}
6.77 + @{syntax_def ident} & = & letter\,quasiletter^* \\
6.78 + @{syntax_def longident} & = & ident (\verb,.,ident)^+ \\
6.79 + @{syntax_def symident} & = & sym^+ ~|~ \verb,\,\verb,<,ident\verb,>, \\
6.80 + @{syntax_def nat} & = & digit^+ \\
6.81 + @{syntax_def var} & = & ident ~|~ \verb,?,ident ~|~ \verb,?,ident\verb,.,nat \\
6.82 + @{syntax_def typefree} & = & \verb,',ident \\
6.83 + @{syntax_def typevar} & = & typefree ~|~ \verb,?,typefree ~|~ \verb,?,typefree\verb,.,nat \\
6.84 + @{syntax_def string} & = & \verb,", ~\dots~ \verb,", \\
6.85 + @{syntax_def altstring} & = & \backquote ~\dots~ \backquote \\
6.86 + @{syntax_def verbatim} & = & \verb,{*, ~\dots~ \verb,*,\verb,}, \\[1ex]
6.87 +
6.88 + letter & = & latin ~|~ \verb,\,\verb,<,latin\verb,>, ~|~ \verb,\,\verb,<,latin\,latin\verb,>, ~|~ greek ~|~ \\
6.89 + & & \verb,\<^isub>, ~|~ \verb,\<^isup>, \\
6.90 + quasiletter & = & letter ~|~ digit ~|~ \verb,_, ~|~ \verb,', \\
6.91 + latin & = & \verb,a, ~|~ \dots ~|~ \verb,z, ~|~ \verb,A, ~|~ \dots ~|~ \verb,Z, \\
6.92 + digit & = & \verb,0, ~|~ \dots ~|~ \verb,9, \\
6.93 + sym & = & \verb,!, ~|~ \verb,#, ~|~ \verb,$, ~|~ \verb,%, ~|~ \verb,&, ~|~
6.94 + \verb,*, ~|~ \verb,+, ~|~ \verb,-, ~|~ \verb,/, ~|~ \\
6.95 + & & \verb,<, ~|~ \verb,=, ~|~ \verb,>, ~|~ \verb,?, ~|~ \texttt{\at} ~|~
6.96 + \verb,^, ~|~ \verb,_, ~|~ \verb,|, ~|~ \verb,~, \\
6.97 + greek & = & \verb,\<alpha>, ~|~ \verb,\<beta>, ~|~ \verb,\<gamma>, ~|~ \verb,\<delta>, ~| \\
6.98 + & & \verb,\<epsilon>, ~|~ \verb,\<zeta>, ~|~ \verb,\<eta>, ~|~ \verb,\<theta>, ~| \\
6.99 + & & \verb,\<iota>, ~|~ \verb,\<kappa>, ~|~ \verb,\<mu>, ~|~ \verb,\<nu>, ~| \\
6.100 + & & \verb,\<xi>, ~|~ \verb,\<pi>, ~|~ \verb,\<rho>, ~|~ \verb,\<sigma>, ~|~ \verb,\<tau>, ~| \\
6.101 + & & \verb,\<upsilon>, ~|~ \verb,\<phi>, ~|~ \verb,\<chi>, ~|~ \verb,\<psi>, ~| \\
6.102 + & & \verb,\<omega>, ~|~ \verb,\<Gamma>, ~|~ \verb,\<Delta>, ~|~ \verb,\<Theta>, ~| \\
6.103 + & & \verb,\<Lambda>, ~|~ \verb,\<Xi>, ~|~ \verb,\<Pi>, ~|~ \verb,\<Sigma>, ~| \\
6.104 + & & \verb,\<Upsilon>, ~|~ \verb,\<Phi>, ~|~ \verb,\<Psi>, ~|~ \verb,\<Omega>, \\
6.105 + \end{matharray}
6.106 +
6.107 + The syntax of @{syntax string} admits any characters, including
6.108 + newlines; ``\verb|"|'' (double-quote) and ``\verb|\|'' (backslash)
6.109 + need to be escaped by a backslash; arbitrary character codes may be
6.110 + specified as ``\verb|\|$ddd$'', with 3 decimal digits. Alternative
6.111 + strings according to @{syntax altstring} are analogous, using single
6.112 + back-quotes instead. The body of @{syntax verbatim} may consist of
6.113 + any text not containing ``\verb,*,\verb,},''; this allows convenient
6.114 + inclusion of quotes without further escapes. The greek letters do
6.115 + \emph{not} include \verb,\<lambda>,, which is already used differently in
6.116 + the meta-logic.
6.117 +
6.118 + Common mathematical symbols such as @{text \<forall>} are represented in
6.119 + Isabelle as \verb,\<forall>,. There are infinitely many Isabelle symbols
6.120 + like this, although proper presentation is left to front-end tools
6.121 + such as {\LaTeX} or Proof~General with the X-Symbol package. A list
6.122 + of standard Isabelle symbols that work well with these tools is
6.123 + given in \cite[appendix~A]{isabelle-sys}.
6.124 +
6.125 + Source comments take the form \texttt{(*~\dots~*)} and may be
6.126 + nested, although user-interface tools might prevent this. Note that
6.127 + \texttt{(*~\dots~*)} indicate source comments only, which are
6.128 + stripped after lexical analysis of the input. The Isar document
6.129 + syntax also provides formal comments that are considered as part of
6.130 + the text (see \S\ref{sec:comments}).
6.131 +*}
6.132 +
6.133 +
6.134 +section {* Common syntax entities *}
6.135 +
6.136 +text {*
6.137 + We now introduce several basic syntactic entities, such as names,
6.138 + terms, and theorem specifications, which are factored out of the
6.139 + actual Isar language elements to be described later.
6.140 +*}
6.141 +
6.142 +
6.143 +subsection {* Names *}
6.144 +
6.145 +text {*
6.146 + Entity \railqtok{name} usually refers to any name of types,
6.147 + constants, theorems etc.\ that are to be \emph{declared} or
6.148 + \emph{defined} (so qualified identifiers are excluded here). Quoted
6.149 + strings provide an escape for non-identifier names or those ruled
6.150 + out by outer syntax keywords (e.g.\ \verb|"let"|). Already existing
6.151 + objects are usually referenced by \railqtok{nameref}.
6.152 +
6.153 + \indexoutertoken{name}\indexoutertoken{parname}\indexoutertoken{nameref}
6.154 + \indexoutertoken{int}
6.155 + \begin{rail}
6.156 + name: ident | symident | string | nat
6.157 + ;
6.158 + parname: '(' name ')'
6.159 + ;
6.160 + nameref: name | longident
6.161 + ;
6.162 + int: nat | '-' nat
6.163 + ;
6.164 + \end{rail}
6.165 +*}
6.166 +
6.167 +
6.168 +subsection {* Comments \label{sec:comments} *}
6.169 +
6.170 +text {*
6.171 + Large chunks of plain \railqtok{text} are usually given
6.172 + \railtok{verbatim}, i.e.\ enclosed in
6.173 + \verb,{,\verb,*,~\dots~\verb,*,\verb,},. For convenience, any of
6.174 + the smaller text units conforming to \railqtok{nameref} are admitted
6.175 + as well. A marginal \railnonterm{comment} is of the form
6.176 + \texttt{--} \railqtok{text}. Any number of these may occur within
6.177 + Isabelle/Isar commands.
6.178 +
6.179 + \indexoutertoken{text}\indexouternonterm{comment}
6.180 + \begin{rail}
6.181 + text: verbatim | nameref
6.182 + ;
6.183 + comment: '--' text
6.184 + ;
6.185 + \end{rail}
6.186 +*}
6.187 +
6.188 +
6.189 +subsection {* Type classes, sorts and arities *}
6.190 +
6.191 +text {*
6.192 + Classes are specified by plain names. Sorts have a very simple
6.193 + inner syntax, which is either a single class name @{text c} or a
6.194 + list @{text "{c\<^sub>1, \<dots>, c\<^sub>n}"} referring to the
6.195 + intersection of these classes. The syntax of type arities is given
6.196 + directly at the outer level.
6.197 +
6.198 + \railalias{subseteq}{\isasymsubseteq}
6.199 + \railterm{subseteq}
6.200 +
6.201 + \indexouternonterm{sort}\indexouternonterm{arity}
6.202 + \indexouternonterm{classdecl}
6.203 + \begin{rail}
6.204 + classdecl: name (('<' | subseteq) (nameref + ','))?
6.205 + ;
6.206 + sort: nameref
6.207 + ;
6.208 + arity: ('(' (sort + ',') ')')? sort
6.209 + ;
6.210 + \end{rail}
6.211 +*}
6.212 +
6.213 +
6.214 +subsection {* Types and terms \label{sec:types-terms} *}
6.215 +
6.216 +text {*
6.217 + The actual inner Isabelle syntax, that of types and terms of the
6.218 + logic, is far too sophisticated in order to be modelled explicitly
6.219 + at the outer theory level. Basically, any such entity has to be
6.220 + quoted to turn it into a single token (the parsing and type-checking
6.221 + is performed internally later). For convenience, a slightly more
6.222 + liberal convention is adopted: quotes may be omitted for any type or
6.223 + term that is already atomic at the outer level. For example, one
6.224 + may just write \texttt{x} instead of \texttt{"x"}. Note that
6.225 + symbolic identifiers (e.g.\ \texttt{++} or @{text "\<forall>"} are available
6.226 + as well, provided these have not been superseded by commands or
6.227 + other keywords already (e.g.\ \texttt{=} or \texttt{+}).
6.228 +
6.229 + \indexoutertoken{type}\indexoutertoken{term}\indexoutertoken{prop}
6.230 + \begin{rail}
6.231 + type: nameref | typefree | typevar
6.232 + ;
6.233 + term: nameref | var
6.234 + ;
6.235 + prop: term
6.236 + ;
6.237 + \end{rail}
6.238 +
6.239 + Positional instantiations are indicated by giving a sequence of
6.240 + terms, or the placeholder ``$\_$'' (underscore), which means to skip
6.241 + a position.
6.242 +
6.243 + \indexoutertoken{inst}\indexoutertoken{insts}
6.244 + \begin{rail}
6.245 + inst: underscore | term
6.246 + ;
6.247 + insts: (inst *)
6.248 + ;
6.249 + \end{rail}
6.250 +
6.251 + Type declarations and definitions usually refer to
6.252 + \railnonterm{typespec} on the left-hand side. This models basic
6.253 + type constructor application at the outer syntax level. Note that
6.254 + only plain postfix notation is available here, but no infixes.
6.255 +
6.256 + \indexouternonterm{typespec}
6.257 + \begin{rail}
6.258 + typespec: (() | typefree | '(' ( typefree + ',' ) ')') name
6.259 + ;
6.260 + \end{rail}
6.261 +*}
6.262 +
6.263 +
6.264 +subsection {* Mixfix annotations *}
6.265 +
6.266 +text {*
6.267 + Mixfix annotations specify concrete \emph{inner} syntax of Isabelle
6.268 + types and terms. Some commands such as @{command "types"} (see
6.269 + \S\ref{sec:types-pure}) admit infixes only, while @{command
6.270 + "consts"} (see \S\ref{sec:consts}) and @{command "syntax"} (see
6.271 + \S\ref{sec:syn-trans}) support the full range of general mixfixes
6.272 + and binders.
6.273 +
6.274 + \indexouternonterm{infix}\indexouternonterm{mixfix}\indexouternonterm{structmixfix}
6.275 + \begin{rail}
6.276 + infix: '(' ('infix' | 'infixl' | 'infixr') string? nat ')'
6.277 + ;
6.278 + mixfix: infix | '(' string prios? nat? ')' | '(' 'binder' string prios? nat ')'
6.279 + ;
6.280 + structmixfix: mixfix | '(' 'structure' ')'
6.281 + ;
6.282 +
6.283 + prios: '[' (nat + ',') ']'
6.284 + ;
6.285 + \end{rail}
6.286 +
6.287 + Here the \railtok{string} specifications refer to the actual mixfix
6.288 + template (see also \cite{isabelle-ref}), which may include literal
6.289 + text, spacing, blocks, and arguments (denoted by ``$_$''); the
6.290 + special symbol \verb,\<index>, (printed as ``\i'') represents an index
6.291 + argument that specifies an implicit structure reference (see also
6.292 + \S\ref{sec:locale}). Infix and binder declarations provide common
6.293 + abbreviations for particular mixfix declarations. So in practice,
6.294 + mixfix templates mostly degenerate to literal text for concrete
6.295 + syntax, such as ``\verb,++,'' for an infix symbol, or
6.296 + ``\verb,++,\i'' for an infix of an implicit structure.
6.297 +*}
6.298 +
6.299 +
6.300 +subsection {* Proof methods \label{sec:syn-meth} *}
6.301 +
6.302 +text {*
6.303 + Proof methods are either basic ones, or expressions composed of
6.304 + methods via ``\texttt{,}'' (sequential composition), ``\texttt{|}''
6.305 + (alternative choices), ``\texttt{?}'' (try), ``\texttt{+}'' (repeat
6.306 + at least once), ``\texttt{[$n$]}'' (restriction to first @{text n}
6.307 + sub-goals, default $n = 1$). In practice, proof methods are usually
6.308 + just a comma separated list of \railqtok{nameref}~\railnonterm{args}
6.309 + specifications. Note that parentheses may be dropped for single
6.310 + method specifications (with no arguments).
6.311 +
6.312 + \indexouternonterm{method}
6.313 + \begin{rail}
6.314 + method: (nameref | '(' methods ')') (() | '?' | '+' | '[' nat? ']')
6.315 + ;
6.316 + methods: (nameref args | method) + (',' | '|')
6.317 + ;
6.318 + \end{rail}
6.319 +
6.320 + Proper Isar proof methods do \emph{not} admit arbitrary goal
6.321 + addressing, but refer either to the first sub-goal or all sub-goals
6.322 + uniformly. The goal restriction operator ``\texttt{[$n$]}''
6.323 + evaluates a method expression within a sandbox consisting of the
6.324 + first @{text n} sub-goals (which need to exist). For example,
6.325 + @{text "simp_all[3]"} simplifies the first three sub-goals, while
6.326 + @{text "(rule foo, simp_all)[]"} simplifies all new goals that
6.327 + emerge from applying rule @{text "foo"} to the originally first one.
6.328 +
6.329 + Improper methods, notably tactic emulations, offer a separate
6.330 + low-level goal addressing scheme as explicit argument to the
6.331 + individual tactic being involved. Here @{text "[!]"} refers to all
6.332 + goals, and @{text "[n-]"} to all goals starting from @{text "n"},
6.333 +
6.334 + \indexouternonterm{goalspec}
6.335 + \begin{rail}
6.336 + goalspec: '[' (nat '-' nat | nat '-' | nat | '!' ) ']'
6.337 + ;
6.338 + \end{rail}
6.339 +*}
6.340 +
6.341 +
6.342 +subsection {* Attributes and theorems \label{sec:syn-att} *}
6.343 +
6.344 +text {*
6.345 + Attributes (and proof methods, see \S\ref{sec:syn-meth}) have their
6.346 + own ``semi-inner'' syntax, in the sense that input conforming to
6.347 + \railnonterm{args} below is parsed by the attribute a second time.
6.348 + The attribute argument specifications may be any sequence of atomic
6.349 + entities (identifiers, strings etc.), or properly bracketed argument
6.350 + lists. Below \railqtok{atom} refers to any atomic entity, including
6.351 + any \railtok{keyword} conforming to \railtok{symident}.
6.352 +
6.353 + \indexoutertoken{atom}\indexouternonterm{args}\indexouternonterm{attributes}
6.354 + \begin{rail}
6.355 + atom: nameref | typefree | typevar | var | nat | keyword
6.356 + ;
6.357 + arg: atom | '(' args ')' | '[' args ']'
6.358 + ;
6.359 + args: arg *
6.360 + ;
6.361 + attributes: '[' (nameref args * ',') ']'
6.362 + ;
6.363 + \end{rail}
6.364 +
6.365 + Theorem specifications come in several flavors:
6.366 + \railnonterm{axmdecl} and \railnonterm{thmdecl} usually refer to
6.367 + axioms, assumptions or results of goal statements, while
6.368 + \railnonterm{thmdef} collects lists of existing theorems. Existing
6.369 + theorems are given by \railnonterm{thmref} and
6.370 + \railnonterm{thmrefs}, the former requires an actual singleton
6.371 + result.
6.372 +
6.373 + There are three forms of theorem references:
6.374 + \begin{enumerate}
6.375 +
6.376 + \item named facts @{text "a"}
6.377 +
6.378 + \item selections from named facts @{text "a(i, j - k)"}
6.379 +
6.380 + \item literal fact propositions using @{syntax_ref altstring} syntax
6.381 + $\backquote\phi\backquote$, (see also method @{method_ref fact} in
6.382 + \S\ref{sec:pure-meth-att}).
6.383 +
6.384 + \end{enumerate}
6.385 +
6.386 + Any kind of theorem specification may include lists of attributes
6.387 + both on the left and right hand sides; attributes are applied to any
6.388 + immediately preceding fact. If names are omitted, the theorems are
6.389 + not stored within the theorem database of the theory or proof
6.390 + context, but any given attributes are applied nonetheless.
6.391 +
6.392 + An extra pair of brackets around attribute declarations --- such as
6.393 + ``@{text "[[simproc a]]"}'' --- abbreviates a theorem reference
6.394 + involving an internal dummy fact, which will be ignored later on.
6.395 + So only the effect of the attribute on the background context will
6.396 + persist. This form of in-place declarations is particularly useful
6.397 + with commands like @{command "declare"} and @{command "using"}.
6.398 +
6.399 + \indexouternonterm{axmdecl}\indexouternonterm{thmdecl}
6.400 + \indexouternonterm{thmdef}\indexouternonterm{thmref}
6.401 + \indexouternonterm{thmrefs}\indexouternonterm{selection}
6.402 + \begin{rail}
6.403 + axmdecl: name attributes? ':'
6.404 + ;
6.405 + thmdecl: thmbind ':'
6.406 + ;
6.407 + thmdef: thmbind '='
6.408 + ;
6.409 + thmref: (nameref selection? | altstring) attributes? | '[' attributes ']'
6.410 + ;
6.411 + thmrefs: thmref +
6.412 + ;
6.413 +
6.414 + thmbind: name attributes | name | attributes
6.415 + ;
6.416 + selection: '(' ((nat | nat '-' nat?) + ',') ')'
6.417 + ;
6.418 + \end{rail}
6.419 +*}
6.420 +
6.421 +
6.422 +subsection {* Term patterns and declarations \label{sec:term-decls} *}
6.423 +
6.424 +text {*
6.425 + Wherever explicit propositions (or term fragments) occur in a proof
6.426 + text, casual binding of schematic term variables may be given
6.427 + specified via patterns of the form ``@{text "(\<IS> p\<^sub>1 \<dots>
6.428 + p\<^sub>n)"}''. This works both for \railqtok{term} and \railqtok{prop}.
6.429 +
6.430 + \indexouternonterm{termpat}\indexouternonterm{proppat}
6.431 + \begin{rail}
6.432 + termpat: '(' ('is' term +) ')'
6.433 + ;
6.434 + proppat: '(' ('is' prop +) ')'
6.435 + ;
6.436 + \end{rail}
6.437 +
6.438 + \medskip Declarations of local variables @{text "x :: \<tau>"} and
6.439 + logical propositions @{text "a : \<phi>"} represent different views on
6.440 + the same principle of introducing a local scope. In practice, one
6.441 + may usually omit the typing of \railnonterm{vars} (due to
6.442 + type-inference), and the naming of propositions (due to implicit
6.443 + references of current facts). In any case, Isar proof elements
6.444 + usually admit to introduce multiple such items simultaneously.
6.445 +
6.446 + \indexouternonterm{vars}\indexouternonterm{props}
6.447 + \begin{rail}
6.448 + vars: (name+) ('::' type)?
6.449 + ;
6.450 + props: thmdecl? (prop proppat? +)
6.451 + ;
6.452 + \end{rail}
6.453 +
6.454 + The treatment of multiple declarations corresponds to the
6.455 + complementary focus of \railnonterm{vars} versus
6.456 + \railnonterm{props}. In ``@{text "x\<^sub>1 \<dots> x\<^sub>n :: \<tau>"}''
6.457 + the typing refers to all variables, while in @{text "a: \<phi>\<^sub>1 \<dots>
6.458 + \<phi>\<^sub>n"} the naming refers to all propositions collectively.
6.459 + Isar language elements that refer to \railnonterm{vars} or
6.460 + \railnonterm{props} typically admit separate typings or namings via
6.461 + another level of iteration, with explicit @{keyword_ref "and"}
6.462 + separators; e.g.\ see @{command "fix"} and @{command "assume"} in
6.463 + \S\ref{sec:proof-context}.
6.464 +*}
6.465 +
6.466 +
6.467 +subsection {* Antiquotations \label{sec:antiq} *}
6.468 +
6.469 +text {*
6.470 + \begin{matharray}{rcl}
6.471 + @{antiquotation_def "theory"} & : & \isarantiq \\
6.472 + @{antiquotation_def "thm"} & : & \isarantiq \\
6.473 + @{antiquotation_def "prop"} & : & \isarantiq \\
6.474 + @{antiquotation_def "term"} & : & \isarantiq \\
6.475 + @{antiquotation_def const} & : & \isarantiq \\
6.476 + @{antiquotation_def abbrev} & : & \isarantiq \\
6.477 + @{antiquotation_def typeof} & : & \isarantiq \\
6.478 + @{antiquotation_def typ} & : & \isarantiq \\
6.479 + @{antiquotation_def thm_style} & : & \isarantiq \\
6.480 + @{antiquotation_def term_style} & : & \isarantiq \\
6.481 + @{antiquotation_def "text"} & : & \isarantiq \\
6.482 + @{antiquotation_def goals} & : & \isarantiq \\
6.483 + @{antiquotation_def subgoals} & : & \isarantiq \\
6.484 + @{antiquotation_def prf} & : & \isarantiq \\
6.485 + @{antiquotation_def full_prf} & : & \isarantiq \\
6.486 + @{antiquotation_def ML} & : & \isarantiq \\
6.487 + @{antiquotation_def ML_type} & : & \isarantiq \\
6.488 + @{antiquotation_def ML_struct} & : & \isarantiq \\
6.489 + \end{matharray}
6.490 +
6.491 + The text body of formal comments (see also \S\ref{sec:comments}) may
6.492 + contain antiquotations of logical entities, such as theorems, terms
6.493 + and types, which are to be presented in the final output produced by
6.494 + the Isabelle document preparation system (see also
6.495 + \S\ref{sec:document-prep}).
6.496 +
6.497 + Thus embedding of ``@{text "@{term [show_types] \"f x = a + x\"}"}''
6.498 + within a text block would cause
6.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
6.500 + antiquotations may involve attributes as well. For example,
6.501 + \texttt{{\at}{\ttlbrace}thm~sym~[no_vars]{\ttrbrace}} would print
6.502 + the statement where all schematic variables have been replaced by
6.503 + fixed ones, which are easier to read.
6.504 +
6.505 + \begin{rail}
6.506 + atsign lbrace antiquotation rbrace
6.507 + ;
6.508 +
6.509 + antiquotation:
6.510 + 'theory' options name |
6.511 + 'thm' options thmrefs |
6.512 + 'prop' options prop |
6.513 + 'term' options term |
6.514 + 'const' options term |
6.515 + 'abbrev' options term |
6.516 + 'typeof' options term |
6.517 + 'typ' options type |
6.518 + 'thm\_style' options name thmref |
6.519 + 'term\_style' options name term |
6.520 + 'text' options name |
6.521 + 'goals' options |
6.522 + 'subgoals' options |
6.523 + 'prf' options thmrefs |
6.524 + 'full\_prf' options thmrefs |
6.525 + 'ML' options name |
6.526 + 'ML\_type' options name |
6.527 + 'ML\_struct' options name
6.528 + ;
6.529 + options: '[' (option * ',') ']'
6.530 + ;
6.531 + option: name | name '=' name
6.532 + ;
6.533 + \end{rail}
6.534 +
6.535 + Note that the syntax of antiquotations may \emph{not} include source
6.536 + comments \texttt{(*~\dots~*)} or verbatim text
6.537 + \verb|{*|~\dots~\verb|*|\verb|}|.
6.538 +
6.539 + \begin{descr}
6.540 +
6.541 + \item [@{text "@{theory A}"}] prints the name @{text "A"}, which is
6.542 + guaranteed to refer to a valid ancestor theory in the current
6.543 + context.
6.544 +
6.545 + \item [@{text "@{thm a\<^sub>1 \<dots> a\<^sub>n}"}] prints theorems @{text
6.546 + "a\<^sub>1 \<dots> a\<^sub>n"}. Note that attribute specifications may be
6.547 + included as well (see also \S\ref{sec:syn-att}); the @{attribute_ref
6.548 + no_vars} rule (see \S\ref{sec:misc-meth-att}) would be particularly
6.549 + useful to suppress printing of schematic variables.
6.550 +
6.551 + \item [@{text "@{prop \<phi>}"}] prints a well-typed proposition @{text
6.552 + "\<phi>"}.
6.553 +
6.554 + \item [@{text "@{term t}"}] prints a well-typed term @{text "t"}.
6.555 +
6.556 + \item [@{text "@{const c}"}] prints a logical or syntactic constant
6.557 + @{text "c"}.
6.558 +
6.559 + \item [@{text "@{abbrev c x\<^sub>1 \<dots> x\<^sub>n}"}] prints a constant
6.560 + abbreviation @{text "c x\<^sub>1 \<dots> x\<^sub>n \<equiv> rhs"} as defined in
6.561 + the current context.
6.562 +
6.563 + \item [@{text "@{typeof t}"}] prints the type of a well-typed term
6.564 + @{text "t"}.
6.565 +
6.566 + \item [@{text "@{typ \<tau>}"}] prints a well-formed type @{text "\<tau>"}.
6.567 +
6.568 + \item [@{text "@{thm_style s a}"}] prints theorem @{text a},
6.569 + previously applying a style @{text s} to it (see below).
6.570 +
6.571 + \item [@{text "@{term_style s t}"}] prints a well-typed term @{text
6.572 + t} after applying a style @{text s} to it (see below).
6.573 +
6.574 + \item [@{text "@{text s}"}] prints uninterpreted source text @{text
6.575 + s}. This is particularly useful to print portions of text according
6.576 + to the Isabelle {\LaTeX} output style, without demanding
6.577 + well-formedness (e.g.\ small pieces of terms that should not be
6.578 + parsed or type-checked yet).
6.579 +
6.580 + \item [@{text "@{goals}"}] prints the current \emph{dynamic} goal
6.581 + state. This is mainly for support of tactic-emulation scripts
6.582 + within Isar --- presentation of goal states does not conform to
6.583 + actual human-readable proof documents.
6.584 +
6.585 + Please do not include goal states into document output unless you
6.586 + really know what you are doing!
6.587 +
6.588 + \item [@{text "@{subgoals}"}] is similar to @{text "@{goals}"}, but
6.589 + does not print the main goal.
6.590 +
6.591 + \item [@{text "@{prf a\<^sub>1 \<dots> a\<^sub>n}"}] prints the (compact)
6.592 + proof terms corresponding to the theorems @{text "a\<^sub>1 \<dots>
6.593 + a\<^sub>n"}. Note that this requires proof terms to be switched on
6.594 + for the current object logic (see the ``Proof terms'' section of the
6.595 + Isabelle reference manual for information on how to do this).
6.596 +
6.597 + \item [@{text "@{full_prf a\<^sub>1 \<dots> a\<^sub>n}"}] is like @{text
6.598 + "@{prf a\<^sub>1 \<dots> a\<^sub>n}"}, but displays the full proof terms,
6.599 + i.e.\ also displays information omitted in the compact proof term,
6.600 + which is denoted by ``$_$'' placeholders there.
6.601 +
6.602 + \item [@{text "@{ML s}"}, @{text "@{ML_type s}"}, and @{text
6.603 + "@{ML_struct s}"}] check text @{text s} as ML value, type, and
6.604 + structure, respectively. The source is displayed verbatim.
6.605 +
6.606 + \end{descr}
6.607 +
6.608 + \medskip The following standard styles for use with @{text
6.609 + thm_style} and @{text term_style} are available:
6.610 +
6.611 + \begin{descr}
6.612 +
6.613 + \item [@{text lhs}] extracts the first argument of any application
6.614 + form with at least two arguments -- typically meta-level or
6.615 + object-level equality, or any other binary relation.
6.616 +
6.617 + \item [@{text rhs}] is like @{text lhs}, but extracts the second
6.618 + argument.
6.619 +
6.620 + \item [@{text "concl"}] extracts the conclusion @{text C} from a rule
6.621 + in Horn-clause normal form @{text "A\<^sub>1 \<Longrightarrow> \<dots> A\<^sub>n \<Longrightarrow> C"}.
6.622 +
6.623 + \item [@{text "prem1"}, \dots, @{text "prem9"}] extract premise
6.624 + number $1$, \dots, $9$, respectively, from from a rule in
6.625 + Horn-clause normal form @{text "A\<^sub>1 \<Longrightarrow> \<dots> A\<^sub>n \<Longrightarrow> C"}
6.626 +
6.627 + \end{descr}
6.628 +
6.629 + \medskip
6.630 + The following options are available to tune the output. Note that most of
6.631 + these coincide with ML flags of the same names (see also \cite{isabelle-ref}).
6.632 +
6.633 + \begin{descr}
6.634 +
6.635 + \item[@{text "show_types = bool"} and @{text "show_sorts = bool"}]
6.636 + control printing of explicit type and sort constraints.
6.637 +
6.638 + \item[@{text "show_structs = bool"}] controls printing of implicit
6.639 + structures.
6.640 +
6.641 + \item[@{text "long_names = bool"}] forces names of types and
6.642 + constants etc.\ to be printed in their fully qualified internal
6.643 + form.
6.644 +
6.645 + \item[@{text "short_names = bool"}] forces names of types and
6.646 + constants etc.\ to be printed unqualified. Note that internalizing
6.647 + the output again in the current context may well yield a different
6.648 + result.
6.649 +
6.650 + \item[@{text "unique_names = bool"}] determines whether the printed
6.651 + version of qualified names should be made sufficiently long to avoid
6.652 + overlap with names declared further back. Set to @{text false} for
6.653 + more concise output.
6.654 +
6.655 + \item[@{text "eta_contract = bool"}] prints terms in @{text
6.656 + \<eta>}-contracted form.
6.657 +
6.658 + \item[@{text "display = bool"}] indicates if the text is to be
6.659 + output as multi-line ``display material'', rather than a small piece
6.660 + of text without line breaks (which is the default).
6.661 +
6.662 + \item[@{text "break = bool"}] controls line breaks in non-display
6.663 + material.
6.664 +
6.665 + \item[@{text "quotes = bool"}] indicates if the output should be
6.666 + enclosed in double quotes.
6.667 +
6.668 + \item[@{text "mode = name"}] adds @{text name} to the print mode to
6.669 + be used for presentation (see also \cite{isabelle-ref}). Note that
6.670 + the standard setup for {\LaTeX} output is already present by
6.671 + default, including the modes @{text latex} and @{text xsymbols}.
6.672 +
6.673 + \item[@{text "margin = nat"} and @{text "indent = nat"}] change the
6.674 + margin or indentation for pretty printing of display material.
6.675 +
6.676 + \item[@{text "source = bool"}] prints the source text of the
6.677 + antiquotation arguments, rather than the actual value. Note that
6.678 + this does not affect well-formedness checks of @{antiquotation
6.679 + "thm"}, @{antiquotation "term"}, etc. (only the @{antiquotation
6.680 + "text"} antiquotation admits arbitrary output).
6.681 +
6.682 + \item[@{text "goals_limit = nat"}] determines the maximum number of
6.683 + goals to be printed.
6.684 +
6.685 + \item[@{text "locale = name"}] specifies an alternative locale
6.686 + context used for evaluating and printing the subsequent argument.
6.687 +
6.688 + \end{descr}
6.689 +
6.690 + For boolean flags, ``@{text "name = true"}'' may be abbreviated as
6.691 + ``@{text name}''. All of the above flags are disabled by default,
6.692 + unless changed from ML.
6.693 +
6.694 + \medskip Note that antiquotations do not only spare the author from
6.695 + tedious typing of logical entities, but also achieve some degree of
6.696 + consistency-checking of informal explanations with formal
6.697 + developments: well-formedness of terms and types with respect to the
6.698 + current theory or proof context is ensured here.
6.699 +*}
6.700 +
6.701 +
6.702 +subsection {* Tagged commands \label{sec:tags} *}
6.703 +
6.704 +text {*
6.705 + Each Isabelle/Isar command may be decorated by presentation tags:
6.706 +
6.707 + \indexouternonterm{tags}
6.708 + \begin{rail}
6.709 + tags: ( tag * )
6.710 + ;
6.711 + tag: '\%' (ident | string)
6.712 + \end{rail}
6.713 +
6.714 + The tags @{text "theory"}, @{text "proof"}, @{text "ML"} are already
6.715 + pre-declared for certain classes of commands:
6.716 +
6.717 + \medskip
6.718 +
6.719 + \begin{tabular}{ll}
6.720 + @{text "theory"} & theory begin/end \\
6.721 + @{text "proof"} & all proof commands \\
6.722 + @{text "ML"} & all commands involving ML code \\
6.723 + \end{tabular}
6.724 +
6.725 + \medskip The Isabelle document preparation system (see also
6.726 + \cite{isabelle-sys}) allows tagged command regions to be presented
6.727 + specifically, e.g.\ to fold proof texts, or drop parts of the text
6.728 + completely.
6.729 +
6.730 + For example ``@{command "by"}~@{text "%invisible auto"}'' would
6.731 + cause that piece of proof to be treated as @{text invisible} instead
6.732 + of @{text "proof"} (the default), which may be either show or hidden
6.733 + depending on the document setup. In contrast, ``@{command
6.734 + "by"}~@{text "%visible auto"}'' would force this text to be shown
6.735 + invariably.
6.736 +
6.737 + Explicit tag specifications within a proof apply to all subsequent
6.738 + commands of the same level of nesting. For example, ``@{command
6.739 + "proof"}~@{text "%visible \<dots>"}~@{command "qed"}'' would force the
6.740 + whole sub-proof to be typeset as @{text visible} (unless some of its
6.741 + parts are tagged differently).
6.742 +*}
6.743 +
6.744 +end
7.1 --- a/doc-src/IsarRef/isar-ref.tex Mon Apr 28 13:41:04 2008 +0200
7.2 +++ b/doc-src/IsarRef/isar-ref.tex Mon Apr 28 14:22:42 2008 +0200
7.3 @@ -70,7 +70,7 @@
7.4
7.5 \input{Thy/document/intro.tex}
7.6 \input{basics.tex}
7.7 -\input{syntax.tex}
7.8 +\input{Thy/document/syntax.tex}
7.9 \input{pure.tex}
7.10 \input{generic.tex}
7.11 \input{logics.tex}
8.1 --- a/doc-src/IsarRef/syntax.tex Mon Apr 28 13:41:04 2008 +0200
8.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
8.3 @@ -1,686 +0,0 @@
8.4 -
8.5 -\chapter{Syntax primitives}
8.6 -
8.7 -The rather generic framework of Isabelle/Isar syntax emerges from three main
8.8 -syntactic categories: \emph{commands} of the top-level Isar engine (covering
8.9 -theory and proof elements), \emph{methods} for general goal refinements
8.10 -(analogous to traditional ``tactics''), and \emph{attributes} for operations
8.11 -on facts (within a certain context). Here we give a reference of basic
8.12 -syntactic entities underlying Isabelle/Isar syntax in a bottom-up manner.
8.13 -Concrete theory and proof language elements will be introduced later on.
8.14 -
8.15 -\medskip
8.16 -
8.17 -In order to get started with writing well-formed Isabelle/Isar documents, the
8.18 -most important aspect to be noted is the difference of \emph{inner} versus
8.19 -\emph{outer} syntax. Inner syntax is that of Isabelle types and terms of the
8.20 -logic, while outer syntax is that of Isabelle/Isar theory sources (including
8.21 -proofs). As a general rule, inner syntax entities may occur only as
8.22 -\emph{atomic entities} within outer syntax. For example, the string
8.23 -\texttt{"x + y"} and identifier \texttt{z} are legal term specifications
8.24 -within a theory, while \texttt{x + y} is not.
8.25 -
8.26 -\begin{warn}
8.27 - Old-style Isabelle theories used to fake parts of the inner syntax of types,
8.28 - with rather complicated rules when quotes may be omitted. Despite the minor
8.29 - drawback of requiring quotes more often, the syntax of Isabelle/Isar is
8.30 - somewhat simpler and more robust in that respect.
8.31 -\end{warn}
8.32 -
8.33 -Printed theory documents usually omit quotes to gain readability (this is a
8.34 -matter of {\LaTeX} macro setup, say via \verb,\isabellestyle,, see also
8.35 -\cite{isabelle-sys}). Experienced users of Isabelle/Isar may easily
8.36 -reconstruct the lost technical information, while mere readers need not care
8.37 -about quotes at all.
8.38 -
8.39 -\medskip
8.40 -
8.41 -Isabelle/Isar input may contain any number of input termination characters
8.42 -``\texttt{;}'' (semicolon) to separate commands explicitly. This is
8.43 -particularly useful in interactive shell sessions to make clear where the
8.44 -current command is intended to end. Otherwise, the interpreter loop will
8.45 -continue to issue a secondary prompt ``\verb,#,'' until an end-of-command is
8.46 -clearly recognized from the input syntax, e.g.\ encounter of the next command
8.47 -keyword.
8.48 -
8.49 -Advanced interfaces such as Proof~General \cite{proofgeneral} do not require
8.50 -explicit semicolons, the amount of input text is determined automatically by
8.51 -inspecting the present content of the Emacs text buffer. In the printed
8.52 -presentation of Isabelle/Isar documents semicolons are omitted altogether for
8.53 -readability.
8.54 -
8.55 -\begin{warn}
8.56 - Proof~General requires certain syntax classification tables in order to
8.57 - achieve properly synchronized interaction with the Isabelle/Isar process.
8.58 - These tables need to be consistent with the Isabelle version and particular
8.59 - logic image to be used in a running session (common object-logics may well
8.60 - change the outer syntax). The standard setup should work correctly with any
8.61 - of the ``official'' logic images derived from Isabelle/HOL (including HOLCF
8.62 - etc.). Users of alternative logics may need to tell Proof~General
8.63 - explicitly, e.g.\ by giving an option \verb,-k ZF, (in conjunction with
8.64 - \verb,-l ZF, to specify the default logic image).
8.65 -\end{warn}
8.66 -
8.67 -\section{Lexical matters}\label{sec:lex-syntax}
8.68 -
8.69 -The Isabelle/Isar outer syntax provides token classes as presented below; most
8.70 -of these coincide with the inner lexical syntax as presented in
8.71 -\cite{isabelle-ref}.
8.72 -
8.73 -\indexoutertoken{ident}\indexoutertoken{longident}\indexoutertoken{symident}
8.74 -\indexoutertoken{nat}\indexoutertoken{var}\indexoutertoken{typefree}
8.75 -\indexoutertoken{typevar}\indexoutertoken{string}\indexoutertoken{altstring}
8.76 -\indexoutertoken{verbatim}
8.77 -\begin{matharray}{rcl}
8.78 - ident & = & letter\,quasiletter^* \\
8.79 - longident & = & ident (\verb,.,ident)^+ \\
8.80 - symident & = & sym^+ ~|~ \verb,\<,ident\verb,>, \\
8.81 - nat & = & digit^+ \\
8.82 - var & = & ident ~|~ \verb,?,ident ~|~ \verb,?,ident\verb,.,nat \\
8.83 - typefree & = & \verb,',ident \\
8.84 - typevar & = & typefree ~|~ \verb,?,typefree ~|~ \verb,?,typefree\verb,.,nat \\
8.85 - string & = & \verb,", ~\dots~ \verb,", \\
8.86 - altstring & = & \backquote ~\dots~ \backquote \\
8.87 - verbatim & = & \verb,{*, ~\dots~ \verb,*}, \\[1ex]
8.88 -
8.89 - letter & = & latin ~|~ \verb,\<,latin\verb,>, ~|~ \verb,\<,latin\,latin\verb,>, ~|~ greek ~|~ \\
8.90 - & & \verb,\<^isub>, ~|~ \verb,\<^isup>, \\
8.91 - quasiletter & = & letter ~|~ digit ~|~ \verb,_, ~|~ \verb,', \\
8.92 - latin & = & \verb,a, ~|~ \dots ~|~ \verb,z, ~|~ \verb,A, ~|~ \dots ~|~ \verb,Z, \\
8.93 - digit & = & \verb,0, ~|~ \dots ~|~ \verb,9, \\
8.94 - sym & = & \verb,!, ~|~ \verb,#, ~|~ \verb,$, ~|~ \verb,%, ~|~ \verb,&, ~|~ %$
8.95 - \verb,*, ~|~ \verb,+, ~|~ \verb,-, ~|~ \verb,/, ~|~ \\
8.96 - & & \verb,<, ~|~ \verb,=, ~|~ \verb,>, ~|~ \verb,?, ~|~ \texttt{\at} ~|~
8.97 - \verb,^, ~|~ \verb,_, ~|~ \verb,|, ~|~ \verb,~, \\
8.98 -greek & = & \verb,\<alpha>, ~|~ \verb,\<beta>, ~|~ \verb,\<gamma>, ~|~ \verb,\<delta>, ~| \\
8.99 - & & \verb,\<epsilon>, ~|~ \verb,\<zeta>, ~|~ \verb,\<eta>, ~|~ \verb,\<theta>, ~| \\
8.100 - & & \verb,\<iota>, ~|~ \verb,\<kappa>, ~|~ \verb,\<mu>, ~|~ \verb,\<nu>, ~| \\
8.101 - & & \verb,\<xi>, ~|~ \verb,\<pi>, ~|~ \verb,\<rho>, ~|~ \verb,\<sigma>, ~|~ \verb,\<tau>, ~| \\
8.102 - & & \verb,\<upsilon>, ~|~ \verb,\<phi>, ~|~ \verb,\<chi>, ~|~ \verb,\<psi>, ~| \\
8.103 - & & \verb,\<omega>, ~|~ \verb,\<Gamma>, ~|~ \verb,\<Delta>, ~|~ \verb,\<Theta>, ~| \\
8.104 - & & \verb,\<Lambda>, ~|~ \verb,\<Xi>, ~|~ \verb,\<Pi>, ~|~ \verb,\<Sigma>, ~| \\
8.105 - & & \verb,\<Upsilon>, ~|~ \verb,\<Phi>, ~|~ \verb,\<Psi>, ~|~ \verb,\<Omega>, \\
8.106 -\end{matharray}
8.107 -
8.108 -The syntax of $string$ admits any characters, including newlines;
8.109 -``\verb|"|'' (double-quote) and ``\verb|\|'' (backslash) need to be
8.110 -escaped by a backslash; arbitrary character codes may be specified as
8.111 -``\verb|\|$ddd$'', with 3 decimal digits as in SML. Alternative
8.112 -strings according to $altstring$ are analogous, using single
8.113 -back-quotes instead. The body of $verbatim$ may consist of any text
8.114 -not containing ``\verb|*}|''; this allows convenient inclusion of
8.115 -quotes without further escapes. The greek letters do \emph{not}
8.116 -include \verb,\<lambda>,, which is already used differently in the
8.117 -meta-logic.
8.118 -
8.119 -Common mathematical symbols such as $\forall$ are represented in Isabelle as
8.120 -\verb,\<forall>,. There are infinitely many legal symbols like this, although
8.121 -proper presentation is left to front-end tools such as {\LaTeX} or
8.122 -Proof~General with the X-Symbol package. A list of standard Isabelle symbols
8.123 -that work well with these tools is given in \cite[appendix~A]{isabelle-sys}.
8.124 -
8.125 -Comments take the form \texttt{(*~\dots~*)} and may be nested, although
8.126 -user-interface tools may prevent this. Note that \texttt{(*~\dots~*)}
8.127 -indicate source comments only, which are stripped after lexical analysis of
8.128 -the input. The Isar document syntax also provides formal comments that are
8.129 -considered as part of the text (see \S\ref{sec:comments}).
8.130 -
8.131 -\begin{warn}
8.132 - Proof~General does not handle nested comments properly; it is also unable to
8.133 - keep \verb,(*,\,/\,\verb,{*, and \verb,*),\,/\,\verb,*}, apart, despite
8.134 - their rather different meaning. These are inherent problems of Emacs
8.135 - legacy. Users should not be overly aggressive about nesting or alternating
8.136 - these delimiters.
8.137 -\end{warn}
8.138 -
8.139 -
8.140 -\section{Common syntax entities}
8.141 -
8.142 -Subsequently, we introduce several basic syntactic entities, such as names,
8.143 -terms, and theorem specifications, which have been factored out of the actual
8.144 -Isar language elements to be described later.
8.145 -
8.146 -Note that some of the basic syntactic entities introduced below (e.g.\
8.147 -\railqtok{name}) act much like tokens rather than plain nonterminals (e.g.\
8.148 -\railnonterm{sort}), especially for the sake of error messages. E.g.\ syntax
8.149 -elements like $\CONSTS$ referring to \railqtok{name} or \railqtok{type} would
8.150 -really report a missing name or type rather than any of the constituent
8.151 -primitive tokens such as \railtok{ident} or \railtok{string}.
8.152 -
8.153 -
8.154 -\subsection{Names}
8.155 -
8.156 -Entity \railqtok{name} usually refers to any name of types, constants,
8.157 -theorems etc.\ that are to be \emph{declared} or \emph{defined} (so qualified
8.158 -identifiers are excluded here). Quoted strings provide an escape for
8.159 -non-identifier names or those ruled out by outer syntax keywords (e.g.\
8.160 -\verb|"let"|). Already existing objects are usually referenced by
8.161 -\railqtok{nameref}.
8.162 -
8.163 -\indexoutertoken{name}\indexoutertoken{parname}\indexoutertoken{nameref}
8.164 -\indexoutertoken{int}
8.165 -\begin{rail}
8.166 - name: ident | symident | string | nat
8.167 - ;
8.168 - parname: '(' name ')'
8.169 - ;
8.170 - nameref: name | longident
8.171 - ;
8.172 - int: nat | '-' nat
8.173 - ;
8.174 -\end{rail}
8.175 -
8.176 -
8.177 -\subsection{Comments}\label{sec:comments}
8.178 -
8.179 -Large chunks of plain \railqtok{text} are usually given \railtok{verbatim},
8.180 -i.e.\ enclosed in \verb|{*|~\dots~\verb|*}|. For convenience, any of the
8.181 -smaller text units conforming to \railqtok{nameref} are admitted as well. A
8.182 -marginal \railnonterm{comment} is of the form \texttt{--} \railqtok{text}.
8.183 -Any number of these may occur within Isabelle/Isar commands.
8.184 -
8.185 -\indexoutertoken{text}\indexouternonterm{comment}
8.186 -\begin{rail}
8.187 - text: verbatim | nameref
8.188 - ;
8.189 - comment: '--' text
8.190 - ;
8.191 -\end{rail}
8.192 -
8.193 -
8.194 -\subsection{Type classes, sorts and arities}
8.195 -
8.196 -Classes are specified by plain names. Sorts have a very simple inner syntax,
8.197 -which is either a single class name $c$ or a list $\{c@1, \dots, c@n\}$
8.198 -referring to the intersection of these classes. The syntax of type arities is
8.199 -given directly at the outer level.
8.200 -
8.201 -\railalias{subseteq}{\isasymsubseteq}
8.202 -\railterm{subseteq}
8.203 -
8.204 -\indexouternonterm{sort}\indexouternonterm{arity}
8.205 -\indexouternonterm{classdecl}
8.206 -\begin{rail}
8.207 - classdecl: name (('<' | subseteq) (nameref + ','))?
8.208 - ;
8.209 - sort: nameref
8.210 - ;
8.211 - arity: ('(' (sort + ',') ')')? sort
8.212 - ;
8.213 -\end{rail}
8.214 -
8.215 -
8.216 -\subsection{Types and terms}\label{sec:types-terms}
8.217 -
8.218 -The actual inner Isabelle syntax, that of types and terms of the logic, is far
8.219 -too sophisticated in order to be modelled explicitly at the outer theory
8.220 -level. Basically, any such entity has to be quoted to turn it into a single
8.221 -token (the parsing and type-checking is performed internally later). For
8.222 -convenience, a slightly more liberal convention is adopted: quotes may be
8.223 -omitted for any type or term that is already atomic at the outer level. For
8.224 -example, one may just write \texttt{x} instead of \texttt{"x"}. Note that
8.225 -symbolic identifiers (e.g.\ \texttt{++} or $\forall$) are available as well,
8.226 -provided these have not been superseded by commands or other keywords already
8.227 -(e.g.\ \texttt{=} or \texttt{+}).
8.228 -
8.229 -\indexoutertoken{type}\indexoutertoken{term}\indexoutertoken{prop}
8.230 -\begin{rail}
8.231 - type: nameref | typefree | typevar
8.232 - ;
8.233 - term: nameref | var
8.234 - ;
8.235 - prop: term
8.236 - ;
8.237 -\end{rail}
8.238 -
8.239 -Positional instantiations are indicated by giving a sequence of terms, or the
8.240 -placeholder ``$\_$'' (underscore), which means to skip a position.
8.241 -
8.242 -\indexoutertoken{inst}\indexoutertoken{insts}
8.243 -\begin{rail}
8.244 - inst: underscore | term
8.245 - ;
8.246 - insts: (inst *)
8.247 - ;
8.248 -\end{rail}
8.249 -
8.250 -Type declarations and definitions usually refer to \railnonterm{typespec} on
8.251 -the left-hand side. This models basic type constructor application at the
8.252 -outer syntax level. Note that only plain postfix notation is available here,
8.253 -but no infixes.
8.254 -
8.255 -\indexouternonterm{typespec}
8.256 -\begin{rail}
8.257 - typespec: (() | typefree | '(' ( typefree + ',' ) ')') name
8.258 - ;
8.259 -\end{rail}
8.260 -
8.261 -
8.262 -\subsection{Mixfix annotations}
8.263 -
8.264 -Mixfix annotations specify concrete \emph{inner} syntax of Isabelle types and
8.265 -terms. Some commands such as $\TYPES$ (see \S\ref{sec:types-pure}) admit
8.266 -infixes only, while $\CONSTS$ (see \S\ref{sec:consts}) and
8.267 -$\isarkeyword{syntax}$ (see \S\ref{sec:syn-trans}) support the full range of
8.268 -general mixfixes and binders.
8.269 -
8.270 -\indexouternonterm{infix}\indexouternonterm{mixfix}\indexouternonterm{structmixfix}
8.271 -\begin{rail}
8.272 - infix: '(' ('infix' | 'infixl' | 'infixr') string? nat ')'
8.273 - ;
8.274 - mixfix: infix | '(' string prios? nat? ')' | '(' 'binder' string prios? nat ')'
8.275 - ;
8.276 - structmixfix: mixfix | '(' 'structure' ')'
8.277 - ;
8.278 -
8.279 - prios: '[' (nat + ',') ']'
8.280 - ;
8.281 -\end{rail}
8.282 -
8.283 -Here the \railtok{string} specifications refer to the actual mixfix template
8.284 -(see also \cite{isabelle-ref}), which may include literal text, spacing,
8.285 -blocks, and arguments (denoted by ``$_$''); the special symbol \verb,\<index>,
8.286 -(printed as ``\i'') represents an index argument that specifies an implicit
8.287 -structure reference (see also \S\ref{sec:locale}). Infix and binder
8.288 -declarations provide common abbreviations for particular mixfix declarations.
8.289 -So in practice, mixfix templates mostly degenerate to literal text for
8.290 -concrete syntax, such as ``\verb,++,'' for an infix symbol, or ``\verb,++,\i''
8.291 -for an infix of an implicit structure.
8.292 -
8.293 -
8.294 -
8.295 -\subsection{Proof methods}\label{sec:syn-meth}
8.296 -
8.297 -Proof methods are either basic ones, or expressions composed of
8.298 -methods via ``\texttt{,}'' (sequential composition), ``\texttt{|}''
8.299 -(alternative choices), ``\texttt{?}'' (try), ``\texttt{+}'' (repeat at
8.300 -least once), ``\texttt{[$n$]}'' (restriction to first $n$ sub-goals,
8.301 -default $n = 1$). In practice, proof methods are usually just a comma
8.302 -separated list of \railqtok{nameref}~\railnonterm{args}
8.303 -specifications. Note that parentheses may be dropped for single
8.304 -method specifications (with no arguments).
8.305 -
8.306 -\indexouternonterm{method}
8.307 -\begin{rail}
8.308 - method: (nameref | '(' methods ')') (() | '?' | '+' | '[' nat? ']')
8.309 - ;
8.310 - methods: (nameref args | method) + (',' | '|')
8.311 - ;
8.312 -\end{rail}
8.313 -
8.314 -Proper Isar proof methods do \emph{not} admit arbitrary goal
8.315 -addressing, but refer either to the first sub-goal or all sub-goals
8.316 -uniformly. The goal restriction operator ``\texttt{[$n$]}'' evaluates
8.317 -a method expression within a sandbox consisting of the first $n$
8.318 -sub-goals (which need to exist). For example,
8.319 -$simp_all\mbox{\tt[}3\mbox{\tt]}$ simplifies the first three
8.320 -sub-goals, while $(rule~foo, simp_all)\mbox{\tt[]}$ simplifies all new
8.321 -goals that emerge from applying rule $foo$ to the originally first
8.322 -one.
8.323 -
8.324 -Improper methods, notably tactic emulations, offer a separate
8.325 -low-level goal addressing scheme as explicit argument to the
8.326 -individual tactic being involved. Here $[!]$ refers to all goals, and
8.327 -$[n-]$ to all goals starting from $n$,
8.328 -
8.329 -\indexouternonterm{goalspec}
8.330 -\begin{rail}
8.331 - goalspec: '[' (nat '-' nat | nat '-' | nat | '!' ) ']'
8.332 - ;
8.333 -\end{rail}
8.334 -
8.335 -
8.336 -\subsection{Attributes and theorems}\label{sec:syn-att}
8.337 -
8.338 -Attributes (and proof methods, see \S\ref{sec:syn-meth}) have their own
8.339 -``semi-inner'' syntax, in the sense that input conforming to
8.340 -\railnonterm{args} below is parsed by the attribute a second time. The
8.341 -attribute argument specifications may be any sequence of atomic entities
8.342 -(identifiers, strings etc.), or properly bracketed argument lists. Below
8.343 -\railqtok{atom} refers to any atomic entity, including any \railtok{keyword}
8.344 -conforming to \railtok{symident}.
8.345 -
8.346 -\indexoutertoken{atom}\indexouternonterm{args}\indexouternonterm{attributes}
8.347 -\begin{rail}
8.348 - atom: nameref | typefree | typevar | var | nat | keyword
8.349 - ;
8.350 - arg: atom | '(' args ')' | '[' args ']'
8.351 - ;
8.352 - args: arg *
8.353 - ;
8.354 - attributes: '[' (nameref args * ',') ']'
8.355 - ;
8.356 -\end{rail}
8.357 -
8.358 -Theorem specifications come in several flavors: \railnonterm{axmdecl}
8.359 -and \railnonterm{thmdecl} usually refer to axioms, assumptions or
8.360 -results of goal statements, while \railnonterm{thmdef} collects lists
8.361 -of existing theorems. Existing theorems are given by
8.362 -\railnonterm{thmref} and \railnonterm{thmrefs}, the former requires an
8.363 -actual singleton result. There are three forms of theorem references:
8.364 -(1) named facts $a$, (2) selections from named facts $a(i, j - k)$, or
8.365 -(3) literal fact propositions using $altstring$ syntax
8.366 -$\backquote\phi\backquote$, (see also method $fact$ in
8.367 -\S\ref{sec:pure-meth-att}).
8.368 -
8.369 -Any kind of theorem specification may include lists of attributes both
8.370 -on the left and right hand sides; attributes are applied to any
8.371 -immediately preceding fact. If names are omitted, the theorems are
8.372 -not stored within the theorem database of the theory or proof context,
8.373 -but any given attributes are applied nonetheless.
8.374 -
8.375 -An extra pair of brackets around attribute declarations --- such as
8.376 -``$[[simproc~a]]$'' --- abbreviates a theorem reference involving an
8.377 -internal dummy fact, which will be ignored later on. So only the
8.378 -effect of the attribute on the background context will persist. This
8.379 -form of in-place declarations is particularly useful with commands
8.380 -like $\DECLARE$ and $\USINGNAME$.
8.381 -
8.382 -\indexouternonterm{axmdecl}\indexouternonterm{thmdecl}
8.383 -\indexouternonterm{thmdef}\indexouternonterm{thmref}
8.384 -\indexouternonterm{thmrefs}\indexouternonterm{selection}
8.385 -\begin{rail}
8.386 - axmdecl: name attributes? ':'
8.387 - ;
8.388 - thmdecl: thmbind ':'
8.389 - ;
8.390 - thmdef: thmbind '='
8.391 - ;
8.392 - thmref: (nameref selection? | altstring) attributes? | '[' attributes ']'
8.393 - ;
8.394 - thmrefs: thmref +
8.395 - ;
8.396 -
8.397 - thmbind: name attributes | name | attributes
8.398 - ;
8.399 - selection: '(' ((nat | nat '-' nat?) + ',') ')'
8.400 - ;
8.401 -\end{rail}
8.402 -
8.403 -
8.404 -\subsection{Term patterns and declarations}\label{sec:term-decls}
8.405 -
8.406 -Wherever explicit propositions (or term fragments) occur in a proof text,
8.407 -casual binding of schematic term variables may be given specified via patterns
8.408 -of the form ``$\ISS{p@1\;\dots}{p@n}$''. There are separate versions
8.409 -available for \railqtok{term}s and \railqtok{prop}s. The latter provides a
8.410 -$\CONCLNAME$ part with patterns referring the (atomic) conclusion of a rule.
8.411 -
8.412 -\indexouternonterm{termpat}\indexouternonterm{proppat}
8.413 -\begin{rail}
8.414 - termpat: '(' ('is' term +) ')'
8.415 - ;
8.416 - proppat: '(' ('is' prop +) ')'
8.417 - ;
8.418 -\end{rail}
8.419 -
8.420 -Declarations of local variables $x :: \tau$ and logical propositions $a :
8.421 -\phi$ represent different views on the same principle of introducing a local
8.422 -scope. In practice, one may usually omit the typing of $vars$ (due to
8.423 -type-inference), and the naming of propositions (due to implicit references of
8.424 -current facts). In any case, Isar proof elements usually admit to introduce
8.425 -multiple such items simultaneously.
8.426 -
8.427 -\indexouternonterm{vars}\indexouternonterm{props}
8.428 -\begin{rail}
8.429 - vars: (name+) ('::' type)?
8.430 - ;
8.431 - props: thmdecl? (prop proppat? +)
8.432 - ;
8.433 -\end{rail}
8.434 -
8.435 -The treatment of multiple declarations corresponds to the complementary focus
8.436 -of $vars$ versus $props$: in ``$x@1~\dots~x@n :: \tau$'' the typing refers to
8.437 -all variables, while in $a\colon \phi@1~\dots~\phi@n$ the naming refers to all
8.438 -propositions collectively. Isar language elements that refer to $vars$ or
8.439 -$props$ typically admit separate typings or namings via another level of
8.440 -iteration, with explicit $\AND$ separators; e.g.\ see $\FIXNAME$ and
8.441 -$\ASSUMENAME$ in \S\ref{sec:proof-context}.
8.442 -
8.443 -
8.444 -\subsection{Antiquotations}\label{sec:antiq}
8.445 -
8.446 -\begin{matharray}{rcl}
8.447 - theory & : & \isarantiq \\
8.448 - thm & : & \isarantiq \\
8.449 - prop & : & \isarantiq \\
8.450 - term & : & \isarantiq \\
8.451 - const & : & \isarantiq \\
8.452 - abbrev & : & \isarantiq \\
8.453 - typeof & : & \isarantiq \\
8.454 - typ & : & \isarantiq \\
8.455 - thm_style & : & \isarantiq \\
8.456 - term_style & : & \isarantiq \\
8.457 - text & : & \isarantiq \\
8.458 - goals & : & \isarantiq \\
8.459 - subgoals & : & \isarantiq \\
8.460 - prf & : & \isarantiq \\
8.461 - full_prf & : & \isarantiq \\
8.462 - ML & : & \isarantiq \\
8.463 - ML_type & : & \isarantiq \\
8.464 - ML_struct & : & \isarantiq \\
8.465 -\end{matharray}
8.466 -
8.467 -The text body of formal comments (see also \S\ref{sec:comments}) may contain
8.468 -antiquotations of logical entities, such as theorems, terms and types, which
8.469 -are to be presented in the final output produced by the Isabelle document
8.470 -preparation system (see also \S\ref{sec:document-prep}).
8.471 -
8.472 -Thus embedding of
8.473 -``\texttt{{\at}{\ttlbrace}term~[show_types]~"f(x)~=~a~+~x"{\ttrbrace}}''
8.474 -within a text block would cause
8.475 -\isa{(f{\isasymColon}'a~{\isasymRightarrow}~'a)~(x{\isasymColon}'a)~=~(a{\isasymColon}'a)~+~x}
8.476 -to appear in the final {\LaTeX} document. Also note that theorem
8.477 -antiquotations may involve attributes as well. For example,
8.478 -\texttt{{\at}{\ttlbrace}thm~sym~[no_vars]{\ttrbrace}} would print the
8.479 -statement where all schematic variables have been replaced by fixed ones,
8.480 -which are easier to read.
8.481 -
8.482 -\indexisarant{theory}\indexisarant{thm}\indexisarant{prop}\indexisarant{term}\indexisarant{const}
8.483 -\indexisarant{abbrev}\indexisarant{typeof}\indexisarant{typ}\indexisarant{thm-style}
8.484 -\indexisarant{term-style}\indexisarant{text}\indexisarant{goals}
8.485 -\indexisarant{subgoals}\indexisarant{prf}\indexisarant{full-prf}\indexisarant{ML}
8.486 -\indexisarant{ML-type}\indexisarant{ML-struct}
8.487 -
8.488 -\begin{rail}
8.489 - atsign lbrace antiquotation rbrace
8.490 - ;
8.491 -
8.492 - antiquotation:
8.493 - 'theory' options name |
8.494 - 'thm' options thmrefs |
8.495 - 'prop' options prop |
8.496 - 'term' options term |
8.497 - 'const' options term |
8.498 - 'abbrev' options term |
8.499 - 'typeof' options term |
8.500 - 'typ' options type |
8.501 - 'thm\_style' options name thmref |
8.502 - 'term\_style' options name term |
8.503 - 'text' options name |
8.504 - 'goals' options |
8.505 - 'subgoals' options |
8.506 - 'prf' options thmrefs |
8.507 - 'full\_prf' options thmrefs |
8.508 - 'ML' options name |
8.509 - 'ML\_type' options name |
8.510 - 'ML\_struct' options name
8.511 - ;
8.512 - options: '[' (option * ',') ']'
8.513 - ;
8.514 - option: name | name '=' name
8.515 - ;
8.516 -\end{rail}
8.517 -
8.518 -Note that the syntax of antiquotations may \emph{not} include source comments
8.519 -\texttt{(*~\dots~*)} or verbatim text \verb|{*|~\dots~\verb|*}|.
8.520 -
8.521 -\begin{descr}
8.522 -
8.523 -\item [$\at\{theory~A\}$] prints the name $A$, which is guaranteed to
8.524 - refer to a valid ancestor theory in the current context.
8.525 -
8.526 -\item [$\at\{thm~\vec a\}$] prints theorems $\vec a$. Note that attribute
8.527 - specifications may be included as well (see also \S\ref{sec:syn-att}); the
8.528 - $no_vars$ operation (see \S\ref{sec:misc-meth-att}) would be particularly
8.529 - useful to suppress printing of schematic variables.
8.530 -
8.531 -\item [$\at\{prop~\phi\}$] prints a well-typed proposition $\phi$.
8.532 -
8.533 -\item [$\at\{term~t\}$] prints a well-typed term $t$.
8.534 -
8.535 -\item [$\at\{const~c\}$] prints a logical or syntactic constant $c$.
8.536 -
8.537 -\item [$\at\{abbrev~c\,\vec x\}$] prints a constant abbreviation
8.538 - $c\,\vec x \equiv rhs$ as defined in the current context.
8.539 -
8.540 -\item [$\at\{typeof~t\}$] prints the type of a well-typed term $t$.
8.541 -
8.542 -\item [$\at\{typ~\tau\}$] prints a well-formed type $\tau$.
8.543 -
8.544 -\item [$\at\{thm_style~s~a\}$] prints theorem $a$, previously applying a style
8.545 - $s$ to it (see below).
8.546 -
8.547 -\item [$\at\{term_style~s~t\}$] prints a well-typed term $t$ after applying a
8.548 - style $s$ to it (see below).
8.549 -
8.550 -\item [$\at\{text~s\}$] prints uninterpreted source text $s$. This is
8.551 - particularly useful to print portions of text according to the Isabelle
8.552 - {\LaTeX} output style, without demanding well-formedness (e.g.\ small pieces
8.553 - of terms that should not be parsed or type-checked yet).
8.554 -
8.555 -\item [$\at\{goals\}$] prints the current \emph{dynamic} goal state. This is
8.556 - mainly for support of tactic-emulation scripts within Isar --- presentation
8.557 - of goal states does not conform to actual human-readable proof documents.
8.558 - Please do not include goal states into document output unless you really
8.559 - know what you are doing!
8.560 -
8.561 -\item [$\at\{subgoals\}$] is similar to $goals$, but does not print the main
8.562 - goal.
8.563 -
8.564 -\item [$\at\{prf~\vec a\}$] prints the (compact) proof terms corresponding to
8.565 - the theorems $\vec a$. Note that this requires proof terms to be switched on
8.566 - for the current object logic (see the ``Proof terms'' section of the
8.567 - Isabelle reference manual for information on how to do this).
8.568 -
8.569 -\item [$\at\{full_prf~\vec a\}$] is like $\at\{prf~\vec a\}$, but displays the
8.570 - full proof terms, i.e.\ also displays information omitted in the compact
8.571 - proof term, which is denoted by ``$_$'' placeholders there.
8.572 -
8.573 -\item [$\at\{ML~s\}$, $\at\{ML_type~s\}$, and $\at\{ML_struct~s\}$] check text
8.574 - $s$ as ML value, type, and structure, respectively. If successful, the
8.575 - source is displayed verbatim.
8.576 -
8.577 -\end{descr}
8.578 -
8.579 -\medskip
8.580 -
8.581 -The following standard styles for use with $thm_style$ and $term_style$ are
8.582 -available:
8.583 -
8.584 -\begin{descr}
8.585 -
8.586 -\item [$lhs$] extracts the first argument of any application form with at
8.587 - least two arguments -- typically meta-level or object-level equality, or any
8.588 - other binary relation.
8.589 -
8.590 -\item [$rhs$] is like $lhs$, but extracts the second argument.
8.591 -
8.592 -\item [$concl$] extracts the conclusion $C$ from a nested meta-level
8.593 - implication $A@1 \Imp \cdots A@n \Imp C$.
8.594 -
8.595 -\item [$prem1$, \dots, $prem9$] extract premise number $1$, \dots, $9$,
8.596 - respectively, from a nested meta-level implication $A@1 \Imp \cdots A@n \Imp
8.597 - C$.
8.598 -
8.599 -\end{descr}
8.600 -
8.601 -\medskip
8.602 -
8.603 -The following options are available to tune the output. Note that most of
8.604 -these coincide with ML flags of the same names (see also \cite{isabelle-ref}).
8.605 -\begin{descr}
8.606 -\item[$show_types = bool$ and $show_sorts = bool$] control printing of
8.607 - explicit type and sort constraints.
8.608 -\item[$show_structs = bool$] controls printing of implicit structures.
8.609 -\item[$long_names = bool$] forces names of types and constants etc.\ to be
8.610 - printed in their fully qualified internal form.
8.611 -\item[$short_names = bool$] forces names of types and constants etc.\ to be
8.612 - printed unqualified. Note that internalizing the output again in the
8.613 - current context may well yield a different result.
8.614 -\item[$unique_names = bool$] determines whether the printed version of
8.615 - qualified names should be made sufficiently long to avoid overlap with names
8.616 - declared further back. Set to $false$ for more concise output.
8.617 -\item[$eta_contract = bool$] prints terms in $\eta$-contracted form.
8.618 -\item[$display = bool$] indicates if the text is to be output as multi-line
8.619 - ``display material'', rather than a small piece of text without line breaks
8.620 - (which is the default).
8.621 -\item[$break = bool$] controls line breaks in non-display material.
8.622 -\item[$quotes = bool$] indicates if the output should be enclosed in double
8.623 - quotes.
8.624 -\item[$mode = name$] adds $name$ to the print mode to be used for presentation
8.625 - (see also \cite{isabelle-ref}). Note that the standard setup for {\LaTeX}
8.626 - output is already present by default, including the modes ``$latex$'',
8.627 - ``$xsymbols$'', ``$symbols$''.
8.628 -\item[$margin = nat$ and $indent = nat$] change the margin or indentation for
8.629 - pretty printing of display material.
8.630 -\item[$source = bool$] prints the source text of the antiquotation arguments,
8.631 - rather than the actual value. Note that this does not affect
8.632 - well-formedness checks of $thm$, $term$, etc. (only the $text$ antiquotation
8.633 - admits arbitrary output).
8.634 -\item[$goals_limit = nat$] determines the maximum number of goals to be
8.635 - printed.
8.636 -\item[$locale = name$] specifies an alternative context used for evaluating
8.637 - and printing the subsequent argument.
8.638 -\end{descr}
8.639 -
8.640 -For boolean flags, ``$name = true$'' may be abbreviated as ``$name$''. All of
8.641 -the above flags are disabled by default, unless changed from ML.
8.642 -
8.643 -\medskip Note that antiquotations do not only spare the author from tedious
8.644 -typing of logical entities, but also achieve some degree of
8.645 -consistency-checking of informal explanations with formal developments:
8.646 -well-formedness of terms and types with respect to the current theory or proof
8.647 -context is ensured here.
8.648 -
8.649 -
8.650 -\subsection{Tagged commands}\label{sec:tags}
8.651 -
8.652 -Each Isabelle/Isar command may be decorated by presentation tags:
8.653 -
8.654 -\indexouternonterm{tags}
8.655 -\begin{rail}
8.656 - tags: ( tag * )
8.657 - ;
8.658 - tag: '\%' (ident | string)
8.659 -\end{rail}
8.660 -
8.661 -The tags $theory$, $proof$, $ML$ are already pre-declared for certain classes
8.662 -of commands:
8.663 -
8.664 -\medskip
8.665 -
8.666 -\begin{tabular}{ll}
8.667 - $theory$ & theory begin and end \\
8.668 - $proof$ & all proof commands \\
8.669 - $ML$ & all commands involving ML code \\
8.670 -\end{tabular}
8.671 -
8.672 -\medskip The Isabelle document preparation system (see also
8.673 -\cite{isabelle-sys}) allows tagged command regions to be presented
8.674 -specifically, e.g.\ to fold proof texts, or drop parts of the text completely.
8.675 -
8.676 -For example ``$\BYNAME~\%invisible~(auto)$'' would cause that piece of proof
8.677 -to be treated as $invisible$ instead of $proof$ (the default), which may be
8.678 -either show or hidden depending on the document setup. In contrast,
8.679 -``$\BYNAME~\%visible~(auto)$'' would force this text to be shown invariably.
8.680 -
8.681 -Explicit tag specifications within a proof apply to all subsequent commands of
8.682 -the same level of nesting. For example,
8.683 -``$\PROOFNAME~\%visible~\dots\QEDNAME$'' would force the whole sub-proof to be
8.684 -typeset as $visible$ (unless some of its parts are tagged differently).
8.685 -
8.686 -%%% Local Variables:
8.687 -%%% mode: latex
8.688 -%%% TeX-master: "isar-ref"
8.689 -%%% End: