1.1 --- a/doc-src/IsarRef/IsaMakefile Mon Jun 02 21:13:48 2008 +0200
1.2 +++ b/doc-src/IsarRef/IsaMakefile Mon Jun 02 21:19:46 2008 +0200
1.3 @@ -22,7 +22,7 @@
1.4 HOL-IsarRef: $(LOG)/HOL-IsarRef.gz
1.5
1.6 $(LOG)/HOL-IsarRef.gz: Thy/ROOT.ML ../antiquote_setup.ML \
1.7 - Thy/Introduction.thy Thy/syntax.thy Thy/Spec.thy Thy/Proof.thy \
1.8 + Thy/Introduction.thy Thy/Outer_Syntax.thy Thy/Spec.thy Thy/Proof.thy \
1.9 Thy/pure.thy Thy/Generic.thy Thy/HOL_Specific.thy \
1.10 Thy/Quick_Reference.thy Thy/ML_Tactic.thy
1.11 @$(USEDIR) -s IsarRef HOL Thy
2.1 --- a/doc-src/IsarRef/Makefile Mon Jun 02 21:13:48 2008 +0200
2.2 +++ b/doc-src/IsarRef/Makefile Mon Jun 02 21:19:46 2008 +0200
2.3 @@ -18,7 +18,7 @@
2.4 Thy/document/ML_Tactic.tex Thy/document/Proof.tex \
2.5 Thy/document/Quick_Reference.tex Thy/document/Spec.tex \
2.6 Thy/document/ZF_Specific.tex Thy/document/Introduction.tex \
2.7 - Thy/document/pure.tex Thy/document/syntax.tex ../isar.sty \
2.8 + Thy/document/pure.tex Thy/document/Outer_Syntax.tex ../isar.sty \
2.9 ../rail.sty ../railsetup.sty ../proof.sty ../iman.sty ../extra.sty \
2.10 ../ttbox.sty ../isabelle.sty ../isabellesym.sty ../pdfsetup.sty \
2.11 ../manual.bib
3.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
3.2 +++ b/doc-src/IsarRef/Thy/Outer_Syntax.thy Mon Jun 02 21:19:46 2008 +0200
3.3 @@ -0,0 +1,750 @@
3.4 +(* $Id$ *)
3.5 +
3.6 +theory Outer_Syntax
3.7 +imports Pure
3.8 +begin
3.9 +
3.10 +chapter {* Syntax primitives *}
3.11 +
3.12 +text {*
3.13 + The rather generic framework of Isabelle/Isar syntax emerges from
3.14 + three main syntactic categories: \emph{commands} of the top-level
3.15 + Isar engine (covering theory and proof elements), \emph{methods} for
3.16 + general goal refinements (analogous to traditional ``tactics''), and
3.17 + \emph{attributes} for operations on facts (within a certain
3.18 + context). Subsequently we give a reference of basic syntactic
3.19 + entities underlying Isabelle/Isar syntax in a bottom-up manner.
3.20 + Concrete theory and proof language elements will be introduced later
3.21 + on.
3.22 +
3.23 + \medskip In order to get started with writing well-formed
3.24 + Isabelle/Isar documents, the most important aspect to be noted is
3.25 + the difference of \emph{inner} versus \emph{outer} syntax. Inner
3.26 + syntax is that of Isabelle types and terms of the logic, while outer
3.27 + syntax is that of Isabelle/Isar theory sources (specifications and
3.28 + proofs). As a general rule, inner syntax entities may occur only as
3.29 + \emph{atomic entities} within outer syntax. For example, the string
3.30 + @{verbatim "\"x + y\""} and identifier @{verbatim z} are legal term
3.31 + specifications within a theory, while @{verbatim "x + y"} without
3.32 + quotes is not.
3.33 +
3.34 + Printed theory documents usually omit quotes to gain readability
3.35 + (this is a matter of {\LaTeX} macro setup, say via @{verbatim
3.36 + "\\isabellestyle"}, see also \cite{isabelle-sys}). Experienced
3.37 + users of Isabelle/Isar may easily reconstruct the lost technical
3.38 + information, while mere readers need not care about quotes at all.
3.39 +
3.40 + \medskip Isabelle/Isar input may contain any number of input
3.41 + termination characters ``@{verbatim ";"}'' (semicolon) to separate
3.42 + commands explicitly. This is particularly useful in interactive
3.43 + shell sessions to make clear where the current command is intended
3.44 + to end. Otherwise, the interpreter loop will continue to issue a
3.45 + secondary prompt ``@{verbatim "#"}'' until an end-of-command is
3.46 + clearly recognized from the input syntax, e.g.\ encounter of the
3.47 + next command keyword.
3.48 +
3.49 + More advanced interfaces such as Proof~General \cite{proofgeneral}
3.50 + do not require explicit semicolons, the amount of input text is
3.51 + determined automatically by inspecting the present content of the
3.52 + Emacs text buffer. In the printed presentation of Isabelle/Isar
3.53 + documents semicolons are omitted altogether for readability.
3.54 +
3.55 + \begin{warn}
3.56 + Proof~General requires certain syntax classification tables in
3.57 + order to achieve properly synchronized interaction with the
3.58 + Isabelle/Isar process. These tables need to be consistent with
3.59 + the Isabelle version and particular logic image to be used in a
3.60 + running session (common object-logics may well change the outer
3.61 + syntax). The standard setup should work correctly with any of the
3.62 + ``official'' logic images derived from Isabelle/HOL (including
3.63 + HOLCF etc.). Users of alternative logics may need to tell
3.64 + Proof~General explicitly, e.g.\ by giving an option @{verbatim "-k ZF"}
3.65 + (in conjunction with @{verbatim "-l ZF"}, to specify the default
3.66 + logic image). Note that option @{verbatim "-L"} does both
3.67 + of this at the same time.
3.68 + \end{warn}
3.69 +*}
3.70 +
3.71 +
3.72 +section {* Lexical matters \label{sec:lex-syntax} *}
3.73 +
3.74 +text {*
3.75 + The Isabelle/Isar outer syntax provides token classes as presented
3.76 + below; most of these coincide with the inner lexical syntax as
3.77 + presented in \cite{isabelle-ref}.
3.78 +
3.79 + \begin{matharray}{rcl}
3.80 + @{syntax_def ident} & = & letter\,quasiletter^* \\
3.81 + @{syntax_def longident} & = & ident (\verb,.,ident)^+ \\
3.82 + @{syntax_def symident} & = & sym^+ ~|~ \verb,\,\verb,<,ident\verb,>, \\
3.83 + @{syntax_def nat} & = & digit^+ \\
3.84 + @{syntax_def var} & = & ident ~|~ \verb,?,ident ~|~ \verb,?,ident\verb,.,nat \\
3.85 + @{syntax_def typefree} & = & \verb,',ident \\
3.86 + @{syntax_def typevar} & = & typefree ~|~ \verb,?,typefree ~|~ \verb,?,typefree\verb,.,nat \\
3.87 + @{syntax_def string} & = & \verb,", ~\dots~ \verb,", \\
3.88 + @{syntax_def altstring} & = & \backquote ~\dots~ \backquote \\
3.89 + @{syntax_def verbatim} & = & \verb,{*, ~\dots~ \verb,*,\verb,}, \\[1ex]
3.90 +
3.91 + letter & = & latin ~|~ \verb,\,\verb,<,latin\verb,>, ~|~ \verb,\,\verb,<,latin\,latin\verb,>, ~|~ greek ~|~ \\
3.92 + & & \verb,\<^isub>, ~|~ \verb,\<^isup>, \\
3.93 + quasiletter & = & letter ~|~ digit ~|~ \verb,_, ~|~ \verb,', \\
3.94 + latin & = & \verb,a, ~|~ \dots ~|~ \verb,z, ~|~ \verb,A, ~|~ \dots ~|~ \verb,Z, \\
3.95 + digit & = & \verb,0, ~|~ \dots ~|~ \verb,9, \\
3.96 + sym & = & \verb,!, ~|~ \verb,#, ~|~ \verb,$, ~|~ \verb,%, ~|~ \verb,&, ~|~
3.97 + \verb,*, ~|~ \verb,+, ~|~ \verb,-, ~|~ \verb,/, ~|~ \\
3.98 + & & \verb,<, ~|~ \verb,=, ~|~ \verb,>, ~|~ \verb,?, ~|~ \texttt{\at} ~|~
3.99 + \verb,^, ~|~ \verb,_, ~|~ \verb,|, ~|~ \verb,~, \\
3.100 + greek & = & \verb,\<alpha>, ~|~ \verb,\<beta>, ~|~ \verb,\<gamma>, ~|~ \verb,\<delta>, ~| \\
3.101 + & & \verb,\<epsilon>, ~|~ \verb,\<zeta>, ~|~ \verb,\<eta>, ~|~ \verb,\<theta>, ~| \\
3.102 + & & \verb,\<iota>, ~|~ \verb,\<kappa>, ~|~ \verb,\<mu>, ~|~ \verb,\<nu>, ~| \\
3.103 + & & \verb,\<xi>, ~|~ \verb,\<pi>, ~|~ \verb,\<rho>, ~|~ \verb,\<sigma>, ~|~ \verb,\<tau>, ~| \\
3.104 + & & \verb,\<upsilon>, ~|~ \verb,\<phi>, ~|~ \verb,\<chi>, ~|~ \verb,\<psi>, ~| \\
3.105 + & & \verb,\<omega>, ~|~ \verb,\<Gamma>, ~|~ \verb,\<Delta>, ~|~ \verb,\<Theta>, ~| \\
3.106 + & & \verb,\<Lambda>, ~|~ \verb,\<Xi>, ~|~ \verb,\<Pi>, ~|~ \verb,\<Sigma>, ~| \\
3.107 + & & \verb,\<Upsilon>, ~|~ \verb,\<Phi>, ~|~ \verb,\<Psi>, ~|~ \verb,\<Omega>, \\
3.108 + \end{matharray}
3.109 +
3.110 + The syntax of @{syntax string} admits any characters, including
3.111 + newlines; ``@{verbatim "\""}'' (double-quote) and ``@{verbatim
3.112 + "\\"}'' (backslash) need to be escaped by a backslash; arbitrary
3.113 + character codes may be specified as ``@{verbatim "\\"}@{text ddd}'',
3.114 + with three decimal digits. Alternative strings according to
3.115 + @{syntax altstring} are analogous, using single back-quotes instead.
3.116 + The body of @{syntax verbatim} may consist of any text not
3.117 + containing ``@{verbatim "*"}@{verbatim "}"}''; this allows
3.118 + convenient inclusion of quotes without further escapes. The greek
3.119 + letters do \emph{not} include @{verbatim "\<lambda>"}, which is already used
3.120 + differently in the meta-logic.
3.121 +
3.122 + Common mathematical symbols such as @{text \<forall>} are represented in
3.123 + Isabelle as @{verbatim \<forall>}. There are infinitely many Isabelle
3.124 + symbols like this, although proper presentation is left to front-end
3.125 + tools such as {\LaTeX} or Proof~General with the X-Symbol package.
3.126 + A list of standard Isabelle symbols that work well with these tools
3.127 + is given in \cite[appendix~A]{isabelle-sys}.
3.128 +
3.129 + Source comments take the form @{verbatim "(*"}~@{text
3.130 + "\<dots>"}~@{verbatim "*)"} and may be nested, although user-interface
3.131 + tools might prevent this. Note that this form indicates source
3.132 + comments only, which are stripped after lexical analysis of the
3.133 + input. The Isar document syntax also provides formal comments that
3.134 + are considered as part of the text (see \secref{sec:comments}).
3.135 +*}
3.136 +
3.137 +
3.138 +section {* Common syntax entities *}
3.139 +
3.140 +text {*
3.141 + We now introduce several basic syntactic entities, such as names,
3.142 + terms, and theorem specifications, which are factored out of the
3.143 + actual Isar language elements to be described later.
3.144 +*}
3.145 +
3.146 +
3.147 +subsection {* Names *}
3.148 +
3.149 +text {*
3.150 + Entity \railqtok{name} usually refers to any name of types,
3.151 + constants, theorems etc.\ that are to be \emph{declared} or
3.152 + \emph{defined} (so qualified identifiers are excluded here). Quoted
3.153 + strings provide an escape for non-identifier names or those ruled
3.154 + out by outer syntax keywords (e.g.\ quoted @{verbatim "\"let\""}).
3.155 + Already existing objects are usually referenced by
3.156 + \railqtok{nameref}.
3.157 +
3.158 + \indexoutertoken{name}\indexoutertoken{parname}\indexoutertoken{nameref}
3.159 + \indexoutertoken{int}
3.160 + \begin{rail}
3.161 + name: ident | symident | string | nat
3.162 + ;
3.163 + parname: '(' name ')'
3.164 + ;
3.165 + nameref: name | longident
3.166 + ;
3.167 + int: nat | '-' nat
3.168 + ;
3.169 + \end{rail}
3.170 +*}
3.171 +
3.172 +
3.173 +subsection {* Comments \label{sec:comments} *}
3.174 +
3.175 +text {*
3.176 + Large chunks of plain \railqtok{text} are usually given
3.177 + \railtok{verbatim}, i.e.\ enclosed in @{verbatim "{"}@{verbatim
3.178 + "*"}~@{text "\<dots>"}~@{verbatim "*"}@{verbatim "}"}. For convenience,
3.179 + any of the smaller text units conforming to \railqtok{nameref} are
3.180 + admitted as well. A marginal \railnonterm{comment} is of the form
3.181 + @{verbatim "--"} \railqtok{text}. Any number of these may occur
3.182 + within Isabelle/Isar commands.
3.183 +
3.184 + \indexoutertoken{text}\indexouternonterm{comment}
3.185 + \begin{rail}
3.186 + text: verbatim | nameref
3.187 + ;
3.188 + comment: '--' text
3.189 + ;
3.190 + \end{rail}
3.191 +*}
3.192 +
3.193 +
3.194 +subsection {* Type classes, sorts and arities *}
3.195 +
3.196 +text {*
3.197 + Classes are specified by plain names. Sorts have a very simple
3.198 + inner syntax, which is either a single class name @{text c} or a
3.199 + list @{text "{c\<^sub>1, \<dots>, c\<^sub>n}"} referring to the
3.200 + intersection of these classes. The syntax of type arities is given
3.201 + directly at the outer level.
3.202 +
3.203 + \indexouternonterm{sort}\indexouternonterm{arity}
3.204 + \indexouternonterm{classdecl}
3.205 + \begin{rail}
3.206 + classdecl: name (('<' | subseteq) (nameref + ','))?
3.207 + ;
3.208 + sort: nameref
3.209 + ;
3.210 + arity: ('(' (sort + ',') ')')? sort
3.211 + ;
3.212 + \end{rail}
3.213 +*}
3.214 +
3.215 +
3.216 +subsection {* Types and terms \label{sec:types-terms} *}
3.217 +
3.218 +text {*
3.219 + The actual inner Isabelle syntax, that of types and terms of the
3.220 + logic, is far too sophisticated in order to be modelled explicitly
3.221 + at the outer theory level. Basically, any such entity has to be
3.222 + quoted to turn it into a single token (the parsing and type-checking
3.223 + is performed internally later). For convenience, a slightly more
3.224 + liberal convention is adopted: quotes may be omitted for any type or
3.225 + term that is already atomic at the outer level. For example, one
3.226 + may just write @{verbatim x} instead of quoted @{verbatim "\"x\""}.
3.227 + Note that symbolic identifiers (e.g.\ @{verbatim "++"} or @{text
3.228 + "\<forall>"} are available as well, provided these have not been superseded
3.229 + by commands or other keywords already (such as @{verbatim "="} or
3.230 + @{verbatim "+"}).
3.231 +
3.232 + \indexoutertoken{type}\indexoutertoken{term}\indexoutertoken{prop}
3.233 + \begin{rail}
3.234 + type: nameref | typefree | typevar
3.235 + ;
3.236 + term: nameref | var
3.237 + ;
3.238 + prop: term
3.239 + ;
3.240 + \end{rail}
3.241 +
3.242 + Positional instantiations are indicated by giving a sequence of
3.243 + terms, or the placeholder ``@{text _}'' (underscore), which means to
3.244 + skip a position.
3.245 +
3.246 + \indexoutertoken{inst}\indexoutertoken{insts}
3.247 + \begin{rail}
3.248 + inst: underscore | term
3.249 + ;
3.250 + insts: (inst *)
3.251 + ;
3.252 + \end{rail}
3.253 +
3.254 + Type declarations and definitions usually refer to
3.255 + \railnonterm{typespec} on the left-hand side. This models basic
3.256 + type constructor application at the outer syntax level. Note that
3.257 + only plain postfix notation is available here, but no infixes.
3.258 +
3.259 + \indexouternonterm{typespec}
3.260 + \begin{rail}
3.261 + typespec: (() | typefree | '(' ( typefree + ',' ) ')') name
3.262 + ;
3.263 + \end{rail}
3.264 +*}
3.265 +
3.266 +
3.267 +subsection {* Mixfix annotations *}
3.268 +
3.269 +text {*
3.270 + Mixfix annotations specify concrete \emph{inner} syntax of Isabelle
3.271 + types and terms. Some commands such as @{command "types"} (see
3.272 + \secref{sec:types-pure}) admit infixes only, while @{command
3.273 + "consts"} (see \secref{sec:consts}) and @{command "syntax"} (see
3.274 + \secref{sec:syn-trans}) support the full range of general mixfixes
3.275 + and binders.
3.276 +
3.277 + \indexouternonterm{infix}\indexouternonterm{mixfix}\indexouternonterm{structmixfix}
3.278 + \begin{rail}
3.279 + infix: '(' ('infix' | 'infixl' | 'infixr') string? nat ')'
3.280 + ;
3.281 + mixfix: infix | '(' string prios? nat? ')' | '(' 'binder' string prios? nat ')'
3.282 + ;
3.283 + structmixfix: mixfix | '(' 'structure' ')'
3.284 + ;
3.285 +
3.286 + prios: '[' (nat + ',') ']'
3.287 + ;
3.288 + \end{rail}
3.289 +
3.290 + Here the \railtok{string} specifications refer to the actual mixfix
3.291 + template (see also \cite{isabelle-ref}), which may include literal
3.292 + text, spacing, blocks, and arguments (denoted by ``@{text _}''); the
3.293 + special symbol ``@{verbatim "\<index>"}'' (printed as ``@{text "\<index>"}'')
3.294 + represents an index argument that specifies an implicit structure
3.295 + reference (see also \secref{sec:locale}). Infix and binder
3.296 + declarations provide common abbreviations for particular mixfix
3.297 + declarations. So in practice, mixfix templates mostly degenerate to
3.298 + literal text for concrete syntax, such as ``@{verbatim "++"}'' for
3.299 + an infix symbol, or ``@{verbatim "++"}@{text "\<index>"}'' for an infix of
3.300 + an implicit structure.
3.301 +*}
3.302 +
3.303 +
3.304 +subsection {* Proof methods \label{sec:syn-meth} *}
3.305 +
3.306 +text {*
3.307 + Proof methods are either basic ones, or expressions composed of
3.308 + methods via ``@{verbatim ","}'' (sequential composition),
3.309 + ``@{verbatim "|"}'' (alternative choices), ``@{verbatim "?"}''
3.310 + (try), ``@{verbatim "+"}'' (repeat at least once), ``@{verbatim
3.311 + "["}@{text n}@{verbatim "]"}'' (restriction to first @{text n}
3.312 + sub-goals, with default @{text "n = 1"}). In practice, proof
3.313 + methods are usually just a comma separated list of
3.314 + \railqtok{nameref}~\railnonterm{args} specifications. Note that
3.315 + parentheses may be dropped for single method specifications (with no
3.316 + arguments).
3.317 +
3.318 + \indexouternonterm{method}
3.319 + \begin{rail}
3.320 + method: (nameref | '(' methods ')') (() | '?' | '+' | '[' nat? ']')
3.321 + ;
3.322 + methods: (nameref args | method) + (',' | '|')
3.323 + ;
3.324 + \end{rail}
3.325 +
3.326 + Proper Isar proof methods do \emph{not} admit arbitrary goal
3.327 + addressing, but refer either to the first sub-goal or all sub-goals
3.328 + uniformly. The goal restriction operator ``@{text "[n]"}''
3.329 + evaluates a method expression within a sandbox consisting of the
3.330 + first @{text n} sub-goals (which need to exist). For example, the
3.331 + method ``@{text "simp_all[3]"}'' simplifies the first three
3.332 + sub-goals, while ``@{text "(rule foo, simp_all)[]"}'' simplifies all
3.333 + new goals that emerge from applying rule @{text "foo"} to the
3.334 + originally first one.
3.335 +
3.336 + Improper methods, notably tactic emulations, offer a separate
3.337 + low-level goal addressing scheme as explicit argument to the
3.338 + individual tactic being involved. Here ``@{text "[!]"}'' refers to
3.339 + all goals, and ``@{text "[n-]"}'' to all goals starting from @{text
3.340 + "n"}.
3.341 +
3.342 + \indexouternonterm{goalspec}
3.343 + \begin{rail}
3.344 + goalspec: '[' (nat '-' nat | nat '-' | nat | '!' ) ']'
3.345 + ;
3.346 + \end{rail}
3.347 +*}
3.348 +
3.349 +
3.350 +subsection {* Attributes and theorems \label{sec:syn-att} *}
3.351 +
3.352 +text {*
3.353 + Attributes (and proof methods, see \secref{sec:syn-meth}) have their
3.354 + own ``semi-inner'' syntax, in the sense that input conforming to
3.355 + \railnonterm{args} below is parsed by the attribute a second time.
3.356 + The attribute argument specifications may be any sequence of atomic
3.357 + entities (identifiers, strings etc.), or properly bracketed argument
3.358 + lists. Below \railqtok{atom} refers to any atomic entity, including
3.359 + any \railtok{keyword} conforming to \railtok{symident}.
3.360 +
3.361 + \indexoutertoken{atom}\indexouternonterm{args}\indexouternonterm{attributes}
3.362 + \begin{rail}
3.363 + atom: nameref | typefree | typevar | var | nat | keyword
3.364 + ;
3.365 + arg: atom | '(' args ')' | '[' args ']'
3.366 + ;
3.367 + args: arg *
3.368 + ;
3.369 + attributes: '[' (nameref args * ',') ']'
3.370 + ;
3.371 + \end{rail}
3.372 +
3.373 + Theorem specifications come in several flavors:
3.374 + \railnonterm{axmdecl} and \railnonterm{thmdecl} usually refer to
3.375 + axioms, assumptions or results of goal statements, while
3.376 + \railnonterm{thmdef} collects lists of existing theorems. Existing
3.377 + theorems are given by \railnonterm{thmref} and
3.378 + \railnonterm{thmrefs}, the former requires an actual singleton
3.379 + result.
3.380 +
3.381 + There are three forms of theorem references:
3.382 + \begin{enumerate}
3.383 +
3.384 + \item named facts @{text "a"},
3.385 +
3.386 + \item selections from named facts @{text "a(i)"} or @{text "a(j - k)"},
3.387 +
3.388 + \item literal fact propositions using @{syntax_ref altstring} syntax
3.389 + @{verbatim "`"}@{text "\<phi>"}@{verbatim "`"} (see also method
3.390 + @{method_ref fact} in \secref{sec:pure-meth-att}).
3.391 +
3.392 + \end{enumerate}
3.393 +
3.394 + Any kind of theorem specification may include lists of attributes
3.395 + both on the left and right hand sides; attributes are applied to any
3.396 + immediately preceding fact. If names are omitted, the theorems are
3.397 + not stored within the theorem database of the theory or proof
3.398 + context, but any given attributes are applied nonetheless.
3.399 +
3.400 + An extra pair of brackets around attributes (like ``@{text
3.401 + "[[simproc a]]"}'') abbreviates a theorem reference involving an
3.402 + internal dummy fact, which will be ignored later on. So only the
3.403 + effect of the attribute on the background context will persist.
3.404 + This form of in-place declarations is particularly useful with
3.405 + commands like @{command "declare"} and @{command "using"}.
3.406 +
3.407 + \indexouternonterm{axmdecl}\indexouternonterm{thmdecl}
3.408 + \indexouternonterm{thmdef}\indexouternonterm{thmref}
3.409 + \indexouternonterm{thmrefs}\indexouternonterm{selection}
3.410 + \begin{rail}
3.411 + axmdecl: name attributes? ':'
3.412 + ;
3.413 + thmdecl: thmbind ':'
3.414 + ;
3.415 + thmdef: thmbind '='
3.416 + ;
3.417 + thmref: (nameref selection? | altstring) attributes? | '[' attributes ']'
3.418 + ;
3.419 + thmrefs: thmref +
3.420 + ;
3.421 +
3.422 + thmbind: name attributes | name | attributes
3.423 + ;
3.424 + selection: '(' ((nat | nat '-' nat?) + ',') ')'
3.425 + ;
3.426 + \end{rail}
3.427 +*}
3.428 +
3.429 +
3.430 +subsection {* Term patterns and declarations \label{sec:term-decls} *}
3.431 +
3.432 +text {*
3.433 + Wherever explicit propositions (or term fragments) occur in a proof
3.434 + text, casual binding of schematic term variables may be given
3.435 + specified via patterns of the form ``@{text "(\<IS> p\<^sub>1 \<dots>
3.436 + p\<^sub>n)"}''. This works both for \railqtok{term} and \railqtok{prop}.
3.437 +
3.438 + \indexouternonterm{termpat}\indexouternonterm{proppat}
3.439 + \begin{rail}
3.440 + termpat: '(' ('is' term +) ')'
3.441 + ;
3.442 + proppat: '(' ('is' prop +) ')'
3.443 + ;
3.444 + \end{rail}
3.445 +
3.446 + \medskip Declarations of local variables @{text "x :: \<tau>"} and
3.447 + logical propositions @{text "a : \<phi>"} represent different views on
3.448 + the same principle of introducing a local scope. In practice, one
3.449 + may usually omit the typing of \railnonterm{vars} (due to
3.450 + type-inference), and the naming of propositions (due to implicit
3.451 + references of current facts). In any case, Isar proof elements
3.452 + usually admit to introduce multiple such items simultaneously.
3.453 +
3.454 + \indexouternonterm{vars}\indexouternonterm{props}
3.455 + \begin{rail}
3.456 + vars: (name+) ('::' type)?
3.457 + ;
3.458 + props: thmdecl? (prop proppat? +)
3.459 + ;
3.460 + \end{rail}
3.461 +
3.462 + The treatment of multiple declarations corresponds to the
3.463 + complementary focus of \railnonterm{vars} versus
3.464 + \railnonterm{props}. In ``@{text "x\<^sub>1 \<dots> x\<^sub>n :: \<tau>"}''
3.465 + the typing refers to all variables, while in @{text "a: \<phi>\<^sub>1 \<dots>
3.466 + \<phi>\<^sub>n"} the naming refers to all propositions collectively.
3.467 + Isar language elements that refer to \railnonterm{vars} or
3.468 + \railnonterm{props} typically admit separate typings or namings via
3.469 + another level of iteration, with explicit @{keyword_ref "and"}
3.470 + separators; e.g.\ see @{command "fix"} and @{command "assume"} in
3.471 + \secref{sec:proof-context}.
3.472 +*}
3.473 +
3.474 +
3.475 +subsection {* Antiquotations \label{sec:antiq} *}
3.476 +
3.477 +text {*
3.478 + \begin{matharray}{rcl}
3.479 + @{antiquotation_def "theory"} & : & \isarantiq \\
3.480 + @{antiquotation_def "thm"} & : & \isarantiq \\
3.481 + @{antiquotation_def "prop"} & : & \isarantiq \\
3.482 + @{antiquotation_def "term"} & : & \isarantiq \\
3.483 + @{antiquotation_def const} & : & \isarantiq \\
3.484 + @{antiquotation_def abbrev} & : & \isarantiq \\
3.485 + @{antiquotation_def typeof} & : & \isarantiq \\
3.486 + @{antiquotation_def typ} & : & \isarantiq \\
3.487 + @{antiquotation_def thm_style} & : & \isarantiq \\
3.488 + @{antiquotation_def term_style} & : & \isarantiq \\
3.489 + @{antiquotation_def "text"} & : & \isarantiq \\
3.490 + @{antiquotation_def goals} & : & \isarantiq \\
3.491 + @{antiquotation_def subgoals} & : & \isarantiq \\
3.492 + @{antiquotation_def prf} & : & \isarantiq \\
3.493 + @{antiquotation_def full_prf} & : & \isarantiq \\
3.494 + @{antiquotation_def ML} & : & \isarantiq \\
3.495 + @{antiquotation_def ML_type} & : & \isarantiq \\
3.496 + @{antiquotation_def ML_struct} & : & \isarantiq \\
3.497 + \end{matharray}
3.498 +
3.499 + The text body of formal comments (see also \secref{sec:comments})
3.500 + may contain antiquotations of logical entities, such as theorems,
3.501 + terms and types, which are to be presented in the final output
3.502 + produced by the Isabelle document preparation system (see also
3.503 + \secref{sec:document-prep}).
3.504 +
3.505 + Thus embedding of ``@{text "@{term [show_types] \"f x = a + x\"}"}''
3.506 + within a text block would cause
3.507 + \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
3.508 + antiquotations may involve attributes as well. For example,
3.509 + @{text "@{thm sym [no_vars]}"} would print the theorem's
3.510 + statement where all schematic variables have been replaced by fixed
3.511 + ones, which are easier to read.
3.512 +
3.513 + \begin{rail}
3.514 + atsign lbrace antiquotation rbrace
3.515 + ;
3.516 +
3.517 + antiquotation:
3.518 + 'theory' options name |
3.519 + 'thm' options thmrefs |
3.520 + 'prop' options prop |
3.521 + 'term' options term |
3.522 + 'const' options term |
3.523 + 'abbrev' options term |
3.524 + 'typeof' options term |
3.525 + 'typ' options type |
3.526 + 'thm\_style' options name thmref |
3.527 + 'term\_style' options name term |
3.528 + 'text' options name |
3.529 + 'goals' options |
3.530 + 'subgoals' options |
3.531 + 'prf' options thmrefs |
3.532 + 'full\_prf' options thmrefs |
3.533 + 'ML' options name |
3.534 + 'ML\_type' options name |
3.535 + 'ML\_struct' options name
3.536 + ;
3.537 + options: '[' (option * ',') ']'
3.538 + ;
3.539 + option: name | name '=' name
3.540 + ;
3.541 + \end{rail}
3.542 +
3.543 + Note that the syntax of antiquotations may \emph{not} include source
3.544 + comments @{verbatim "(*"}~@{text "\<dots>"}~@{verbatim "*)"} or verbatim
3.545 + text @{verbatim "{"}@{verbatim "*"}~@{text "\<dots>"}~@{verbatim
3.546 + "*"}@{verbatim "}"}.
3.547 +
3.548 + \begin{descr}
3.549 +
3.550 + \item [@{text "@{theory A}"}] prints the name @{text "A"}, which is
3.551 + guaranteed to refer to a valid ancestor theory in the current
3.552 + context.
3.553 +
3.554 + \item [@{text "@{thm a\<^sub>1 \<dots> a\<^sub>n}"}] prints theorems
3.555 + @{text "a\<^sub>1 \<dots> a\<^sub>n"}. Note that attribute specifications
3.556 + may be included as well (see also \secref{sec:syn-att}); the
3.557 + @{attribute_ref no_vars} rule (see \secref{sec:misc-meth-att}) would
3.558 + be particularly useful to suppress printing of schematic variables.
3.559 +
3.560 + \item [@{text "@{prop \<phi>}"}] prints a well-typed proposition @{text
3.561 + "\<phi>"}.
3.562 +
3.563 + \item [@{text "@{term t}"}] prints a well-typed term @{text "t"}.
3.564 +
3.565 + \item [@{text "@{const c}"}] prints a logical or syntactic constant
3.566 + @{text "c"}.
3.567 +
3.568 + \item [@{text "@{abbrev c x\<^sub>1 \<dots> x\<^sub>n}"}] prints a constant
3.569 + abbreviation @{text "c x\<^sub>1 \<dots> x\<^sub>n \<equiv> rhs"} as defined in
3.570 + the current context.
3.571 +
3.572 + \item [@{text "@{typeof t}"}] prints the type of a well-typed term
3.573 + @{text "t"}.
3.574 +
3.575 + \item [@{text "@{typ \<tau>}"}] prints a well-formed type @{text "\<tau>"}.
3.576 +
3.577 + \item [@{text "@{thm_style s a}"}] prints theorem @{text a},
3.578 + previously applying a style @{text s} to it (see below).
3.579 +
3.580 + \item [@{text "@{term_style s t}"}] prints a well-typed term @{text
3.581 + t} after applying a style @{text s} to it (see below).
3.582 +
3.583 + \item [@{text "@{text s}"}] prints uninterpreted source text @{text
3.584 + s}. This is particularly useful to print portions of text according
3.585 + to the Isabelle {\LaTeX} output style, without demanding
3.586 + well-formedness (e.g.\ small pieces of terms that should not be
3.587 + parsed or type-checked yet).
3.588 +
3.589 + \item [@{text "@{goals}"}] prints the current \emph{dynamic} goal
3.590 + state. This is mainly for support of tactic-emulation scripts
3.591 + within Isar --- presentation of goal states does not conform to
3.592 + actual human-readable proof documents.
3.593 +
3.594 + Please do not include goal states into document output unless you
3.595 + really know what you are doing!
3.596 +
3.597 + \item [@{text "@{subgoals}"}] is similar to @{text "@{goals}"}, but
3.598 + does not print the main goal.
3.599 +
3.600 + \item [@{text "@{prf a\<^sub>1 \<dots> a\<^sub>n}"}] prints the (compact)
3.601 + proof terms corresponding to the theorems @{text "a\<^sub>1 \<dots>
3.602 + a\<^sub>n"}. Note that this requires proof terms to be switched on
3.603 + for the current object logic (see the ``Proof terms'' section of the
3.604 + Isabelle reference manual for information on how to do this).
3.605 +
3.606 + \item [@{text "@{full_prf a\<^sub>1 \<dots> a\<^sub>n}"}] is like @{text
3.607 + "@{prf a\<^sub>1 \<dots> a\<^sub>n}"}, but displays the full proof terms,
3.608 + i.e.\ also displays information omitted in the compact proof term,
3.609 + which is denoted by ``@{text _}'' placeholders there.
3.610 +
3.611 + \item [@{text "@{ML s}"}, @{text "@{ML_type s}"}, and @{text
3.612 + "@{ML_struct s}"}] check text @{text s} as ML value, type, and
3.613 + structure, respectively. The source is displayed verbatim.
3.614 +
3.615 + \end{descr}
3.616 +
3.617 + \medskip The following standard styles for use with @{text
3.618 + thm_style} and @{text term_style} are available:
3.619 +
3.620 + \begin{descr}
3.621 +
3.622 + \item [@{text lhs}] extracts the first argument of any application
3.623 + form with at least two arguments -- typically meta-level or
3.624 + object-level equality, or any other binary relation.
3.625 +
3.626 + \item [@{text rhs}] is like @{text lhs}, but extracts the second
3.627 + argument.
3.628 +
3.629 + \item [@{text "concl"}] extracts the conclusion @{text C} from a rule
3.630 + in Horn-clause normal form @{text "A\<^sub>1 \<Longrightarrow> \<dots> A\<^sub>n \<Longrightarrow> C"}.
3.631 +
3.632 + \item [@{text "prem1"}, \dots, @{text "prem9"}] extract premise
3.633 + number @{text "1, \<dots>, 9"}, respectively, from from a rule in
3.634 + Horn-clause normal form @{text "A\<^sub>1 \<Longrightarrow> \<dots> A\<^sub>n \<Longrightarrow> C"}
3.635 +
3.636 + \end{descr}
3.637 +
3.638 + \medskip
3.639 + The following options are available to tune the output. Note that most of
3.640 + these coincide with ML flags of the same names (see also \cite{isabelle-ref}).
3.641 +
3.642 + \begin{descr}
3.643 +
3.644 + \item[@{text "show_types = bool"} and @{text "show_sorts = bool"}]
3.645 + control printing of explicit type and sort constraints.
3.646 +
3.647 + \item[@{text "show_structs = bool"}] controls printing of implicit
3.648 + structures.
3.649 +
3.650 + \item[@{text "long_names = bool"}] forces names of types and
3.651 + constants etc.\ to be printed in their fully qualified internal
3.652 + form.
3.653 +
3.654 + \item[@{text "short_names = bool"}] forces names of types and
3.655 + constants etc.\ to be printed unqualified. Note that internalizing
3.656 + the output again in the current context may well yield a different
3.657 + result.
3.658 +
3.659 + \item[@{text "unique_names = bool"}] determines whether the printed
3.660 + version of qualified names should be made sufficiently long to avoid
3.661 + overlap with names declared further back. Set to @{text false} for
3.662 + more concise output.
3.663 +
3.664 + \item[@{text "eta_contract = bool"}] prints terms in @{text
3.665 + \<eta>}-contracted form.
3.666 +
3.667 + \item[@{text "display = bool"}] indicates if the text is to be
3.668 + output as multi-line ``display material'', rather than a small piece
3.669 + of text without line breaks (which is the default).
3.670 +
3.671 + \item[@{text "break = bool"}] controls line breaks in non-display
3.672 + material.
3.673 +
3.674 + \item[@{text "quotes = bool"}] indicates if the output should be
3.675 + enclosed in double quotes.
3.676 +
3.677 + \item[@{text "mode = name"}] adds @{text name} to the print mode to
3.678 + be used for presentation (see also \cite{isabelle-ref}). Note that
3.679 + the standard setup for {\LaTeX} output is already present by
3.680 + default, including the modes @{text latex} and @{text xsymbols}.
3.681 +
3.682 + \item[@{text "margin = nat"} and @{text "indent = nat"}] change the
3.683 + margin or indentation for pretty printing of display material.
3.684 +
3.685 + \item[@{text "source = bool"}] prints the source text of the
3.686 + antiquotation arguments, rather than the actual value. Note that
3.687 + this does not affect well-formedness checks of @{antiquotation
3.688 + "thm"}, @{antiquotation "term"}, etc. (only the @{antiquotation
3.689 + "text"} antiquotation admits arbitrary output).
3.690 +
3.691 + \item[@{text "goals_limit = nat"}] determines the maximum number of
3.692 + goals to be printed.
3.693 +
3.694 + \item[@{text "locale = name"}] specifies an alternative locale
3.695 + context used for evaluating and printing the subsequent argument.
3.696 +
3.697 + \end{descr}
3.698 +
3.699 + For boolean flags, ``@{text "name = true"}'' may be abbreviated as
3.700 + ``@{text name}''. All of the above flags are disabled by default,
3.701 + unless changed from ML.
3.702 +
3.703 + \medskip Note that antiquotations do not only spare the author from
3.704 + tedious typing of logical entities, but also achieve some degree of
3.705 + consistency-checking of informal explanations with formal
3.706 + developments: well-formedness of terms and types with respect to the
3.707 + current theory or proof context is ensured here.
3.708 +*}
3.709 +
3.710 +
3.711 +subsection {* Tagged commands \label{sec:tags} *}
3.712 +
3.713 +text {*
3.714 + Each Isabelle/Isar command may be decorated by presentation tags:
3.715 +
3.716 + \indexouternonterm{tags}
3.717 + \begin{rail}
3.718 + tags: ( tag * )
3.719 + ;
3.720 + tag: '\%' (ident | string)
3.721 + \end{rail}
3.722 +
3.723 + The tags @{text "theory"}, @{text "proof"}, @{text "ML"} are already
3.724 + pre-declared for certain classes of commands:
3.725 +
3.726 + \medskip
3.727 +
3.728 + \begin{tabular}{ll}
3.729 + @{text "theory"} & theory begin/end \\
3.730 + @{text "proof"} & all proof commands \\
3.731 + @{text "ML"} & all commands involving ML code \\
3.732 + \end{tabular}
3.733 +
3.734 + \medskip The Isabelle document preparation system (see also
3.735 + \cite{isabelle-sys}) allows tagged command regions to be presented
3.736 + specifically, e.g.\ to fold proof texts, or drop parts of the text
3.737 + completely.
3.738 +
3.739 + For example ``@{command "by"}~@{text "%invisible auto"}'' would
3.740 + cause that piece of proof to be treated as @{text invisible} instead
3.741 + of @{text "proof"} (the default), which may be either show or hidden
3.742 + depending on the document setup. In contrast, ``@{command
3.743 + "by"}~@{text "%visible auto"}'' would force this text to be shown
3.744 + invariably.
3.745 +
3.746 + Explicit tag specifications within a proof apply to all subsequent
3.747 + commands of the same level of nesting. For example, ``@{command
3.748 + "proof"}~@{text "%visible \<dots>"}~@{command "qed"}'' would force the
3.749 + whole sub-proof to be typeset as @{text visible} (unless some of its
3.750 + parts are tagged differently).
3.751 +*}
3.752 +
3.753 +end
4.1 --- a/doc-src/IsarRef/Thy/ROOT.ML Mon Jun 02 21:13:48 2008 +0200
4.2 +++ b/doc-src/IsarRef/Thy/ROOT.ML Mon Jun 02 21:19:46 2008 +0200
4.3 @@ -5,7 +5,7 @@
4.4 use "../../antiquote_setup.ML";
4.5
4.6 use_thy "Introduction";
4.7 -use_thy "syntax";
4.8 +use_thy "Outer_Syntax";
4.9 use_thy "Spec";
4.10 use_thy "Proof";
4.11 use_thy "pure";
5.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
5.2 +++ b/doc-src/IsarRef/Thy/document/Outer_Syntax.tex Mon Jun 02 21:19:46 2008 +0200
5.3 @@ -0,0 +1,787 @@
5.4 +%
5.5 +\begin{isabellebody}%
5.6 +\def\isabellecontext{Outer{\isacharunderscore}Syntax}%
5.7 +%
5.8 +\isadelimtheory
5.9 +\isanewline
5.10 +\isanewline
5.11 +%
5.12 +\endisadelimtheory
5.13 +%
5.14 +\isatagtheory
5.15 +\isacommand{theory}\isamarkupfalse%
5.16 +\ Outer{\isacharunderscore}Syntax\isanewline
5.17 +\isakeyword{imports}\ Pure\isanewline
5.18 +\isakeyword{begin}%
5.19 +\endisatagtheory
5.20 +{\isafoldtheory}%
5.21 +%
5.22 +\isadelimtheory
5.23 +%
5.24 +\endisadelimtheory
5.25 +%
5.26 +\isamarkupchapter{Syntax primitives%
5.27 +}
5.28 +\isamarkuptrue%
5.29 +%
5.30 +\begin{isamarkuptext}%
5.31 +The rather generic framework of Isabelle/Isar syntax emerges from
5.32 + three main syntactic categories: \emph{commands} of the top-level
5.33 + Isar engine (covering theory and proof elements), \emph{methods} for
5.34 + general goal refinements (analogous to traditional ``tactics''), and
5.35 + \emph{attributes} for operations on facts (within a certain
5.36 + context). Subsequently we give a reference of basic syntactic
5.37 + entities underlying Isabelle/Isar syntax in a bottom-up manner.
5.38 + Concrete theory and proof language elements will be introduced later
5.39 + on.
5.40 +
5.41 + \medskip In order to get started with writing well-formed
5.42 + Isabelle/Isar documents, the most important aspect to be noted is
5.43 + the difference of \emph{inner} versus \emph{outer} syntax. Inner
5.44 + syntax is that of Isabelle types and terms of the logic, while outer
5.45 + syntax is that of Isabelle/Isar theory sources (specifications and
5.46 + proofs). As a general rule, inner syntax entities may occur only as
5.47 + \emph{atomic entities} within outer syntax. For example, the string
5.48 + \verb|"x + y"| and identifier \verb|z| are legal term
5.49 + specifications within a theory, while \verb|x + y| without
5.50 + quotes is not.
5.51 +
5.52 + Printed theory documents usually omit quotes to gain readability
5.53 + (this is a matter of {\LaTeX} macro setup, say via \verb|\isabellestyle|, see also \cite{isabelle-sys}). Experienced
5.54 + users of Isabelle/Isar may easily reconstruct the lost technical
5.55 + information, while mere readers need not care about quotes at all.
5.56 +
5.57 + \medskip Isabelle/Isar input may contain any number of input
5.58 + termination characters ``\verb|;|'' (semicolon) to separate
5.59 + commands explicitly. This is particularly useful in interactive
5.60 + shell sessions to make clear where the current command is intended
5.61 + to end. Otherwise, the interpreter loop will continue to issue a
5.62 + secondary prompt ``\verb|#|'' until an end-of-command is
5.63 + clearly recognized from the input syntax, e.g.\ encounter of the
5.64 + next command keyword.
5.65 +
5.66 + More advanced interfaces such as Proof~General \cite{proofgeneral}
5.67 + do not require explicit semicolons, the amount of input text is
5.68 + determined automatically by inspecting the present content of the
5.69 + Emacs text buffer. In the printed presentation of Isabelle/Isar
5.70 + documents semicolons are omitted altogether for readability.
5.71 +
5.72 + \begin{warn}
5.73 + Proof~General requires certain syntax classification tables in
5.74 + order to achieve properly synchronized interaction with the
5.75 + Isabelle/Isar process. These tables need to be consistent with
5.76 + the Isabelle version and particular logic image to be used in a
5.77 + running session (common object-logics may well change the outer
5.78 + syntax). The standard setup should work correctly with any of the
5.79 + ``official'' logic images derived from Isabelle/HOL (including
5.80 + HOLCF etc.). Users of alternative logics may need to tell
5.81 + Proof~General explicitly, e.g.\ by giving an option \verb|-k ZF|
5.82 + (in conjunction with \verb|-l ZF|, to specify the default
5.83 + logic image). Note that option \verb|-L| does both
5.84 + of this at the same time.
5.85 + \end{warn}%
5.86 +\end{isamarkuptext}%
5.87 +\isamarkuptrue%
5.88 +%
5.89 +\isamarkupsection{Lexical matters \label{sec:lex-syntax}%
5.90 +}
5.91 +\isamarkuptrue%
5.92 +%
5.93 +\begin{isamarkuptext}%
5.94 +The Isabelle/Isar outer syntax provides token classes as presented
5.95 + below; most of these coincide with the inner lexical syntax as
5.96 + presented in \cite{isabelle-ref}.
5.97 +
5.98 + \begin{matharray}{rcl}
5.99 + \indexdef{}{syntax}{ident}\hypertarget{syntax.ident}{\hyperlink{syntax.ident}{\mbox{\isa{ident}}}} & = & letter\,quasiletter^* \\
5.100 + \indexdef{}{syntax}{longident}\hypertarget{syntax.longident}{\hyperlink{syntax.longident}{\mbox{\isa{longident}}}} & = & ident (\verb,.,ident)^+ \\
5.101 + \indexdef{}{syntax}{symident}\hypertarget{syntax.symident}{\hyperlink{syntax.symident}{\mbox{\isa{symident}}}} & = & sym^+ ~|~ \verb,\,\verb,<,ident\verb,>, \\
5.102 + \indexdef{}{syntax}{nat}\hypertarget{syntax.nat}{\hyperlink{syntax.nat}{\mbox{\isa{nat}}}} & = & digit^+ \\
5.103 + \indexdef{}{syntax}{var}\hypertarget{syntax.var}{\hyperlink{syntax.var}{\mbox{\isa{var}}}} & = & ident ~|~ \verb,?,ident ~|~ \verb,?,ident\verb,.,nat \\
5.104 + \indexdef{}{syntax}{typefree}\hypertarget{syntax.typefree}{\hyperlink{syntax.typefree}{\mbox{\isa{typefree}}}} & = & \verb,',ident \\
5.105 + \indexdef{}{syntax}{typevar}\hypertarget{syntax.typevar}{\hyperlink{syntax.typevar}{\mbox{\isa{typevar}}}} & = & typefree ~|~ \verb,?,typefree ~|~ \verb,?,typefree\verb,.,nat \\
5.106 + \indexdef{}{syntax}{string}\hypertarget{syntax.string}{\hyperlink{syntax.string}{\mbox{\isa{string}}}} & = & \verb,", ~\dots~ \verb,", \\
5.107 + \indexdef{}{syntax}{altstring}\hypertarget{syntax.altstring}{\hyperlink{syntax.altstring}{\mbox{\isa{altstring}}}} & = & \backquote ~\dots~ \backquote \\
5.108 + \indexdef{}{syntax}{verbatim}\hypertarget{syntax.verbatim}{\hyperlink{syntax.verbatim}{\mbox{\isa{verbatim}}}} & = & \verb,{*, ~\dots~ \verb,*,\verb,}, \\[1ex]
5.109 +
5.110 + letter & = & latin ~|~ \verb,\,\verb,<,latin\verb,>, ~|~ \verb,\,\verb,<,latin\,latin\verb,>, ~|~ greek ~|~ \\
5.111 + & & \verb,\<^isub>, ~|~ \verb,\<^isup>, \\
5.112 + quasiletter & = & letter ~|~ digit ~|~ \verb,_, ~|~ \verb,', \\
5.113 + latin & = & \verb,a, ~|~ \dots ~|~ \verb,z, ~|~ \verb,A, ~|~ \dots ~|~ \verb,Z, \\
5.114 + digit & = & \verb,0, ~|~ \dots ~|~ \verb,9, \\
5.115 + sym & = & \verb,!, ~|~ \verb,#, ~|~ \verb,$, ~|~ \verb,%, ~|~ \verb,&, ~|~
5.116 + \verb,*, ~|~ \verb,+, ~|~ \verb,-, ~|~ \verb,/, ~|~ \\
5.117 + & & \verb,<, ~|~ \verb,=, ~|~ \verb,>, ~|~ \verb,?, ~|~ \texttt{\at} ~|~
5.118 + \verb,^, ~|~ \verb,_, ~|~ \verb,|, ~|~ \verb,~, \\
5.119 + greek & = & \verb,\<alpha>, ~|~ \verb,\<beta>, ~|~ \verb,\<gamma>, ~|~ \verb,\<delta>, ~| \\
5.120 + & & \verb,\<epsilon>, ~|~ \verb,\<zeta>, ~|~ \verb,\<eta>, ~|~ \verb,\<theta>, ~| \\
5.121 + & & \verb,\<iota>, ~|~ \verb,\<kappa>, ~|~ \verb,\<mu>, ~|~ \verb,\<nu>, ~| \\
5.122 + & & \verb,\<xi>, ~|~ \verb,\<pi>, ~|~ \verb,\<rho>, ~|~ \verb,\<sigma>, ~|~ \verb,\<tau>, ~| \\
5.123 + & & \verb,\<upsilon>, ~|~ \verb,\<phi>, ~|~ \verb,\<chi>, ~|~ \verb,\<psi>, ~| \\
5.124 + & & \verb,\<omega>, ~|~ \verb,\<Gamma>, ~|~ \verb,\<Delta>, ~|~ \verb,\<Theta>, ~| \\
5.125 + & & \verb,\<Lambda>, ~|~ \verb,\<Xi>, ~|~ \verb,\<Pi>, ~|~ \verb,\<Sigma>, ~| \\
5.126 + & & \verb,\<Upsilon>, ~|~ \verb,\<Phi>, ~|~ \verb,\<Psi>, ~|~ \verb,\<Omega>, \\
5.127 + \end{matharray}
5.128 +
5.129 + The syntax of \hyperlink{syntax.string}{\mbox{\isa{string}}} admits any characters, including
5.130 + newlines; ``\verb|"|'' (double-quote) and ``\verb|\|'' (backslash) need to be escaped by a backslash; arbitrary
5.131 + character codes may be specified as ``\verb|\|\isa{ddd}'',
5.132 + with three decimal digits. Alternative strings according to
5.133 + \hyperlink{syntax.altstring}{\mbox{\isa{altstring}}} are analogous, using single back-quotes instead.
5.134 + The body of \hyperlink{syntax.verbatim}{\mbox{\isa{verbatim}}} may consist of any text not
5.135 + containing ``\verb|*|\verb|}|''; this allows
5.136 + convenient inclusion of quotes without further escapes. The greek
5.137 + letters do \emph{not} include \verb|\<lambda>|, which is already used
5.138 + differently in the meta-logic.
5.139 +
5.140 + Common mathematical symbols such as \isa{{\isasymforall}} are represented in
5.141 + Isabelle as \verb|\<forall>|. There are infinitely many Isabelle
5.142 + symbols like this, although proper presentation is left to front-end
5.143 + tools such as {\LaTeX} or Proof~General with the X-Symbol package.
5.144 + A list of standard Isabelle symbols that work well with these tools
5.145 + is given in \cite[appendix~A]{isabelle-sys}.
5.146 +
5.147 + Source comments take the form \verb|(*|~\isa{{\isachardoublequote}{\isasymdots}{\isachardoublequote}}~\verb|*)| and may be nested, although user-interface
5.148 + tools might prevent this. Note that this form indicates source
5.149 + comments only, which are stripped after lexical analysis of the
5.150 + input. The Isar document syntax also provides formal comments that
5.151 + are considered as part of the text (see \secref{sec:comments}).%
5.152 +\end{isamarkuptext}%
5.153 +\isamarkuptrue%
5.154 +%
5.155 +\isamarkupsection{Common syntax entities%
5.156 +}
5.157 +\isamarkuptrue%
5.158 +%
5.159 +\begin{isamarkuptext}%
5.160 +We now introduce several basic syntactic entities, such as names,
5.161 + terms, and theorem specifications, which are factored out of the
5.162 + actual Isar language elements to be described later.%
5.163 +\end{isamarkuptext}%
5.164 +\isamarkuptrue%
5.165 +%
5.166 +\isamarkupsubsection{Names%
5.167 +}
5.168 +\isamarkuptrue%
5.169 +%
5.170 +\begin{isamarkuptext}%
5.171 +Entity \railqtok{name} usually refers to any name of types,
5.172 + constants, theorems etc.\ that are to be \emph{declared} or
5.173 + \emph{defined} (so qualified identifiers are excluded here). Quoted
5.174 + strings provide an escape for non-identifier names or those ruled
5.175 + out by outer syntax keywords (e.g.\ quoted \verb|"let"|).
5.176 + Already existing objects are usually referenced by
5.177 + \railqtok{nameref}.
5.178 +
5.179 + \indexoutertoken{name}\indexoutertoken{parname}\indexoutertoken{nameref}
5.180 + \indexoutertoken{int}
5.181 + \begin{rail}
5.182 + name: ident | symident | string | nat
5.183 + ;
5.184 + parname: '(' name ')'
5.185 + ;
5.186 + nameref: name | longident
5.187 + ;
5.188 + int: nat | '-' nat
5.189 + ;
5.190 + \end{rail}%
5.191 +\end{isamarkuptext}%
5.192 +\isamarkuptrue%
5.193 +%
5.194 +\isamarkupsubsection{Comments \label{sec:comments}%
5.195 +}
5.196 +\isamarkuptrue%
5.197 +%
5.198 +\begin{isamarkuptext}%
5.199 +Large chunks of plain \railqtok{text} are usually given
5.200 + \railtok{verbatim}, i.e.\ enclosed in \verb|{|\verb|*|~\isa{{\isachardoublequote}{\isasymdots}{\isachardoublequote}}~\verb|*|\verb|}|. For convenience,
5.201 + any of the smaller text units conforming to \railqtok{nameref} are
5.202 + admitted as well. A marginal \railnonterm{comment} is of the form
5.203 + \verb|--| \railqtok{text}. Any number of these may occur
5.204 + within Isabelle/Isar commands.
5.205 +
5.206 + \indexoutertoken{text}\indexouternonterm{comment}
5.207 + \begin{rail}
5.208 + text: verbatim | nameref
5.209 + ;
5.210 + comment: '--' text
5.211 + ;
5.212 + \end{rail}%
5.213 +\end{isamarkuptext}%
5.214 +\isamarkuptrue%
5.215 +%
5.216 +\isamarkupsubsection{Type classes, sorts and arities%
5.217 +}
5.218 +\isamarkuptrue%
5.219 +%
5.220 +\begin{isamarkuptext}%
5.221 +Classes are specified by plain names. Sorts have a very simple
5.222 + inner syntax, which is either a single class name \isa{c} or a
5.223 + list \isa{{\isachardoublequote}{\isacharbraceleft}c\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ c\isactrlsub n{\isacharbraceright}{\isachardoublequote}} referring to the
5.224 + intersection of these classes. The syntax of type arities is given
5.225 + directly at the outer level.
5.226 +
5.227 + \indexouternonterm{sort}\indexouternonterm{arity}
5.228 + \indexouternonterm{classdecl}
5.229 + \begin{rail}
5.230 + classdecl: name (('<' | subseteq) (nameref + ','))?
5.231 + ;
5.232 + sort: nameref
5.233 + ;
5.234 + arity: ('(' (sort + ',') ')')? sort
5.235 + ;
5.236 + \end{rail}%
5.237 +\end{isamarkuptext}%
5.238 +\isamarkuptrue%
5.239 +%
5.240 +\isamarkupsubsection{Types and terms \label{sec:types-terms}%
5.241 +}
5.242 +\isamarkuptrue%
5.243 +%
5.244 +\begin{isamarkuptext}%
5.245 +The actual inner Isabelle syntax, that of types and terms of the
5.246 + logic, is far too sophisticated in order to be modelled explicitly
5.247 + at the outer theory level. Basically, any such entity has to be
5.248 + quoted to turn it into a single token (the parsing and type-checking
5.249 + is performed internally later). For convenience, a slightly more
5.250 + liberal convention is adopted: quotes may be omitted for any type or
5.251 + term that is already atomic at the outer level. For example, one
5.252 + may just write \verb|x| instead of quoted \verb|"x"|.
5.253 + Note that symbolic identifiers (e.g.\ \verb|++| or \isa{{\isachardoublequote}{\isasymforall}{\isachardoublequote}} are available as well, provided these have not been superseded
5.254 + by commands or other keywords already (such as \verb|=| or
5.255 + \verb|+|).
5.256 +
5.257 + \indexoutertoken{type}\indexoutertoken{term}\indexoutertoken{prop}
5.258 + \begin{rail}
5.259 + type: nameref | typefree | typevar
5.260 + ;
5.261 + term: nameref | var
5.262 + ;
5.263 + prop: term
5.264 + ;
5.265 + \end{rail}
5.266 +
5.267 + Positional instantiations are indicated by giving a sequence of
5.268 + terms, or the placeholder ``\isa{{\isacharunderscore}}'' (underscore), which means to
5.269 + skip a position.
5.270 +
5.271 + \indexoutertoken{inst}\indexoutertoken{insts}
5.272 + \begin{rail}
5.273 + inst: underscore | term
5.274 + ;
5.275 + insts: (inst *)
5.276 + ;
5.277 + \end{rail}
5.278 +
5.279 + Type declarations and definitions usually refer to
5.280 + \railnonterm{typespec} on the left-hand side. This models basic
5.281 + type constructor application at the outer syntax level. Note that
5.282 + only plain postfix notation is available here, but no infixes.
5.283 +
5.284 + \indexouternonterm{typespec}
5.285 + \begin{rail}
5.286 + typespec: (() | typefree | '(' ( typefree + ',' ) ')') name
5.287 + ;
5.288 + \end{rail}%
5.289 +\end{isamarkuptext}%
5.290 +\isamarkuptrue%
5.291 +%
5.292 +\isamarkupsubsection{Mixfix annotations%
5.293 +}
5.294 +\isamarkuptrue%
5.295 +%
5.296 +\begin{isamarkuptext}%
5.297 +Mixfix annotations specify concrete \emph{inner} syntax of Isabelle
5.298 + types and terms. Some commands such as \hyperlink{command.types}{\mbox{\isa{\isacommand{types}}}} (see
5.299 + \secref{sec:types-pure}) admit infixes only, while \hyperlink{command.consts}{\mbox{\isa{\isacommand{consts}}}} (see \secref{sec:consts}) and \hyperlink{command.syntax}{\mbox{\isa{\isacommand{syntax}}}} (see
5.300 + \secref{sec:syn-trans}) support the full range of general mixfixes
5.301 + and binders.
5.302 +
5.303 + \indexouternonterm{infix}\indexouternonterm{mixfix}\indexouternonterm{structmixfix}
5.304 + \begin{rail}
5.305 + infix: '(' ('infix' | 'infixl' | 'infixr') string? nat ')'
5.306 + ;
5.307 + mixfix: infix | '(' string prios? nat? ')' | '(' 'binder' string prios? nat ')'
5.308 + ;
5.309 + structmixfix: mixfix | '(' 'structure' ')'
5.310 + ;
5.311 +
5.312 + prios: '[' (nat + ',') ']'
5.313 + ;
5.314 + \end{rail}
5.315 +
5.316 + Here the \railtok{string} specifications refer to the actual mixfix
5.317 + template (see also \cite{isabelle-ref}), which may include literal
5.318 + text, spacing, blocks, and arguments (denoted by ``\isa{{\isacharunderscore}}''); the
5.319 + special symbol ``\verb|\<index>|'' (printed as ``\isa{{\isachardoublequote}{\isasymindex}{\isachardoublequote}}'')
5.320 + represents an index argument that specifies an implicit structure
5.321 + reference (see also \secref{sec:locale}). Infix and binder
5.322 + declarations provide common abbreviations for particular mixfix
5.323 + declarations. So in practice, mixfix templates mostly degenerate to
5.324 + literal text for concrete syntax, such as ``\verb|++|'' for
5.325 + an infix symbol, or ``\verb|++|\isa{{\isachardoublequote}{\isasymindex}{\isachardoublequote}}'' for an infix of
5.326 + an implicit structure.%
5.327 +\end{isamarkuptext}%
5.328 +\isamarkuptrue%
5.329 +%
5.330 +\isamarkupsubsection{Proof methods \label{sec:syn-meth}%
5.331 +}
5.332 +\isamarkuptrue%
5.333 +%
5.334 +\begin{isamarkuptext}%
5.335 +Proof methods are either basic ones, or expressions composed of
5.336 + methods via ``\verb|,|'' (sequential composition),
5.337 + ``\verb||\verb,|,\verb||'' (alternative choices), ``\verb|?|''
5.338 + (try), ``\verb|+|'' (repeat at least once), ``\verb|[|\isa{n}\verb|]|'' (restriction to first \isa{n}
5.339 + sub-goals, with default \isa{{\isachardoublequote}n\ {\isacharequal}\ {\isadigit{1}}{\isachardoublequote}}). In practice, proof
5.340 + methods are usually just a comma separated list of
5.341 + \railqtok{nameref}~\railnonterm{args} specifications. Note that
5.342 + parentheses may be dropped for single method specifications (with no
5.343 + 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 ``\isa{{\isachardoublequote}{\isacharbrackleft}n{\isacharbrackright}{\isachardoublequote}}''
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, the
5.358 + method ``\isa{{\isachardoublequote}simp{\isacharunderscore}all{\isacharbrackleft}{\isadigit{3}}{\isacharbrackright}{\isachardoublequote}}'' simplifies the first three
5.359 + sub-goals, while ``\isa{{\isachardoublequote}{\isacharparenleft}rule\ foo{\isacharcomma}\ simp{\isacharunderscore}all{\isacharparenright}{\isacharbrackleft}{\isacharbrackright}{\isachardoublequote}}'' simplifies all
5.360 + new goals that emerge from applying rule \isa{{\isachardoublequote}foo{\isachardoublequote}} to the
5.361 + originally first one.
5.362 +
5.363 + Improper methods, notably tactic emulations, offer a separate
5.364 + low-level goal addressing scheme as explicit argument to the
5.365 + individual tactic being involved. Here ``\isa{{\isachardoublequote}{\isacharbrackleft}{\isacharbang}{\isacharbrackright}{\isachardoublequote}}'' refers to
5.366 + all goals, and ``\isa{{\isachardoublequote}{\isacharbrackleft}n{\isacharminus}{\isacharbrackright}{\isachardoublequote}}'' to all goals starting from \isa{{\isachardoublequote}n{\isachardoublequote}}.
5.367 +
5.368 + \indexouternonterm{goalspec}
5.369 + \begin{rail}
5.370 + goalspec: '[' (nat '-' nat | nat '-' | nat | '!' ) ']'
5.371 + ;
5.372 + \end{rail}%
5.373 +\end{isamarkuptext}%
5.374 +\isamarkuptrue%
5.375 +%
5.376 +\isamarkupsubsection{Attributes and theorems \label{sec:syn-att}%
5.377 +}
5.378 +\isamarkuptrue%
5.379 +%
5.380 +\begin{isamarkuptext}%
5.381 +Attributes (and proof methods, see \secref{sec:syn-meth}) have their
5.382 + own ``semi-inner'' syntax, in the sense that input conforming to
5.383 + \railnonterm{args} below is parsed by the attribute a second time.
5.384 + The attribute argument specifications may be any sequence of atomic
5.385 + entities (identifiers, strings etc.), or properly bracketed argument
5.386 + lists. Below \railqtok{atom} refers to any atomic entity, including
5.387 + any \railtok{keyword} conforming to \railtok{symident}.
5.388 +
5.389 + \indexoutertoken{atom}\indexouternonterm{args}\indexouternonterm{attributes}
5.390 + \begin{rail}
5.391 + atom: nameref | typefree | typevar | var | nat | keyword
5.392 + ;
5.393 + arg: atom | '(' args ')' | '[' args ']'
5.394 + ;
5.395 + args: arg *
5.396 + ;
5.397 + attributes: '[' (nameref args * ',') ']'
5.398 + ;
5.399 + \end{rail}
5.400 +
5.401 + Theorem specifications come in several flavors:
5.402 + \railnonterm{axmdecl} and \railnonterm{thmdecl} usually refer to
5.403 + axioms, assumptions or results of goal statements, while
5.404 + \railnonterm{thmdef} collects lists of existing theorems. Existing
5.405 + theorems are given by \railnonterm{thmref} and
5.406 + \railnonterm{thmrefs}, the former requires an actual singleton
5.407 + result.
5.408 +
5.409 + There are three forms of theorem references:
5.410 + \begin{enumerate}
5.411 +
5.412 + \item named facts \isa{{\isachardoublequote}a{\isachardoublequote}},
5.413 +
5.414 + \item selections from named facts \isa{{\isachardoublequote}a{\isacharparenleft}i{\isacharparenright}{\isachardoublequote}} or \isa{{\isachardoublequote}a{\isacharparenleft}j\ {\isacharminus}\ k{\isacharparenright}{\isachardoublequote}},
5.415 +
5.416 + \item literal fact propositions using \indexref{}{syntax}{altstring}\hyperlink{syntax.altstring}{\mbox{\isa{altstring}}} syntax
5.417 + \verb|`|\isa{{\isachardoublequote}{\isasymphi}{\isachardoublequote}}\verb|`| (see also method
5.418 + \indexref{}{method}{fact}\hyperlink{method.fact}{\mbox{\isa{fact}}} in \secref{sec:pure-meth-att}).
5.419 +
5.420 + \end{enumerate}
5.421 +
5.422 + Any kind of theorem specification may include lists of attributes
5.423 + both on the left and right hand sides; attributes are applied to any
5.424 + immediately preceding fact. If names are omitted, the theorems are
5.425 + not stored within the theorem database of the theory or proof
5.426 + context, but any given attributes are applied nonetheless.
5.427 +
5.428 + An extra pair of brackets around attributes (like ``\isa{{\isachardoublequote}{\isacharbrackleft}{\isacharbrackleft}simproc\ a{\isacharbrackright}{\isacharbrackright}{\isachardoublequote}}'') abbreviates a theorem reference involving an
5.429 + internal dummy fact, which will be ignored later on. So only the
5.430 + effect of the attribute on the background context will persist.
5.431 + This form of in-place declarations is particularly useful with
5.432 + commands like \hyperlink{command.declare}{\mbox{\isa{\isacommand{declare}}}} and \hyperlink{command.using}{\mbox{\isa{\isacommand{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{{\isachardoublequote}{\isacharparenleft}{\isasymIS}\ p\isactrlsub {\isadigit{1}}\ {\isasymdots}\ p\isactrlsub n{\isacharparenright}{\isachardoublequote}}''. 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{{\isachardoublequote}x\ {\isacharcolon}{\isacharcolon}\ {\isasymtau}{\isachardoublequote}} and
5.475 + logical propositions \isa{{\isachardoublequote}a\ {\isacharcolon}\ {\isasymphi}{\isachardoublequote}} 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{{\isachardoublequote}x\isactrlsub {\isadigit{1}}\ {\isasymdots}\ x\isactrlsub n\ {\isacharcolon}{\isacharcolon}\ {\isasymtau}{\isachardoublequote}}''
5.493 + the typing refers to all variables, while in \isa{{\isachardoublequote}a{\isacharcolon}\ {\isasymphi}\isactrlsub {\isadigit{1}}\ {\isasymdots}\ {\isasymphi}\isactrlsub n{\isachardoublequote}} 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}\hyperlink{keyword.and}{\mbox{\isa{\isakeyword{and}}}}
5.497 + separators; e.g.\ see \hyperlink{command.fix}{\mbox{\isa{\isacommand{fix}}}} and \hyperlink{command.assume}{\mbox{\isa{\isacommand{assume}}}} in
5.498 + \secref{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}\hypertarget{antiquotation.theory}{\hyperlink{antiquotation.theory}{\mbox{\isa{theory}}}} & : & \isarantiq \\
5.509 + \indexdef{}{antiquotation}{thm}\hypertarget{antiquotation.thm}{\hyperlink{antiquotation.thm}{\mbox{\isa{thm}}}} & : & \isarantiq \\
5.510 + \indexdef{}{antiquotation}{prop}\hypertarget{antiquotation.prop}{\hyperlink{antiquotation.prop}{\mbox{\isa{prop}}}} & : & \isarantiq \\
5.511 + \indexdef{}{antiquotation}{term}\hypertarget{antiquotation.term}{\hyperlink{antiquotation.term}{\mbox{\isa{term}}}} & : & \isarantiq \\
5.512 + \indexdef{}{antiquotation}{const}\hypertarget{antiquotation.const}{\hyperlink{antiquotation.const}{\mbox{\isa{const}}}} & : & \isarantiq \\
5.513 + \indexdef{}{antiquotation}{abbrev}\hypertarget{antiquotation.abbrev}{\hyperlink{antiquotation.abbrev}{\mbox{\isa{abbrev}}}} & : & \isarantiq \\
5.514 + \indexdef{}{antiquotation}{typeof}\hypertarget{antiquotation.typeof}{\hyperlink{antiquotation.typeof}{\mbox{\isa{typeof}}}} & : & \isarantiq \\
5.515 + \indexdef{}{antiquotation}{typ}\hypertarget{antiquotation.typ}{\hyperlink{antiquotation.typ}{\mbox{\isa{typ}}}} & : & \isarantiq \\
5.516 + \indexdef{}{antiquotation}{thm\_style}\hypertarget{antiquotation.thm-style}{\hyperlink{antiquotation.thm-style}{\mbox{\isa{thm{\isacharunderscore}style}}}} & : & \isarantiq \\
5.517 + \indexdef{}{antiquotation}{term\_style}\hypertarget{antiquotation.term-style}{\hyperlink{antiquotation.term-style}{\mbox{\isa{term{\isacharunderscore}style}}}} & : & \isarantiq \\
5.518 + \indexdef{}{antiquotation}{text}\hypertarget{antiquotation.text}{\hyperlink{antiquotation.text}{\mbox{\isa{text}}}} & : & \isarantiq \\
5.519 + \indexdef{}{antiquotation}{goals}\hypertarget{antiquotation.goals}{\hyperlink{antiquotation.goals}{\mbox{\isa{goals}}}} & : & \isarantiq \\
5.520 + \indexdef{}{antiquotation}{subgoals}\hypertarget{antiquotation.subgoals}{\hyperlink{antiquotation.subgoals}{\mbox{\isa{subgoals}}}} & : & \isarantiq \\
5.521 + \indexdef{}{antiquotation}{prf}\hypertarget{antiquotation.prf}{\hyperlink{antiquotation.prf}{\mbox{\isa{prf}}}} & : & \isarantiq \\
5.522 + \indexdef{}{antiquotation}{full\_prf}\hypertarget{antiquotation.full-prf}{\hyperlink{antiquotation.full-prf}{\mbox{\isa{full{\isacharunderscore}prf}}}} & : & \isarantiq \\
5.523 + \indexdef{}{antiquotation}{ML}\hypertarget{antiquotation.ML}{\hyperlink{antiquotation.ML}{\mbox{\isa{ML}}}} & : & \isarantiq \\
5.524 + \indexdef{}{antiquotation}{ML\_type}\hypertarget{antiquotation.ML-type}{\hyperlink{antiquotation.ML-type}{\mbox{\isa{ML{\isacharunderscore}type}}}} & : & \isarantiq \\
5.525 + \indexdef{}{antiquotation}{ML\_struct}\hypertarget{antiquotation.ML-struct}{\hyperlink{antiquotation.ML-struct}{\mbox{\isa{ML{\isacharunderscore}struct}}}} & : & \isarantiq \\
5.526 + \end{matharray}
5.527 +
5.528 + The text body of formal comments (see also \secref{sec:comments})
5.529 + may contain antiquotations of logical entities, such as theorems,
5.530 + terms and types, which are to be presented in the final output
5.531 + produced by the Isabelle document preparation system (see also
5.532 + \secref{sec:document-prep}).
5.533 +
5.534 + Thus embedding of ``\isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}term\ {\isacharbrackleft}show{\isacharunderscore}types{\isacharbrackright}\ {\isachardoublequote}f\ x\ {\isacharequal}\ a\ {\isacharplus}\ x{\isachardoublequote}{\isacharbraceright}{\isachardoublequote}}''
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 + \isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}thm\ sym\ {\isacharbrackleft}no{\isacharunderscore}vars{\isacharbrackright}{\isacharbraceright}{\isachardoublequote}} would print the theorem's
5.539 + statement where all schematic variables have been replaced by fixed
5.540 + 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 \verb|(*|~\isa{{\isachardoublequote}{\isasymdots}{\isachardoublequote}}~\verb|*)| or verbatim
5.574 + text \verb|{|\verb|*|~\isa{{\isachardoublequote}{\isasymdots}{\isachardoublequote}}~\verb|*|\verb|}|.
5.575 +
5.576 + \begin{descr}
5.577 +
5.578 + \item [\isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}theory\ A{\isacharbraceright}{\isachardoublequote}}] prints the name \isa{{\isachardoublequote}A{\isachardoublequote}}, which is
5.579 + guaranteed to refer to a valid ancestor theory in the current
5.580 + context.
5.581 +
5.582 + \item [\isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}thm\ a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n{\isacharbraceright}{\isachardoublequote}}] prints theorems
5.583 + \isa{{\isachardoublequote}a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n{\isachardoublequote}}. Note that attribute specifications
5.584 + may be included as well (see also \secref{sec:syn-att}); the
5.585 + \indexref{}{attribute}{no\_vars}\hyperlink{attribute.no-vars}{\mbox{\isa{no{\isacharunderscore}vars}}} rule (see \secref{sec:misc-meth-att}) would
5.586 + be particularly useful to suppress printing of schematic variables.
5.587 +
5.588 + \item [\isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}prop\ {\isasymphi}{\isacharbraceright}{\isachardoublequote}}] prints a well-typed proposition \isa{{\isachardoublequote}{\isasymphi}{\isachardoublequote}}.
5.589 +
5.590 + \item [\isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}term\ t{\isacharbraceright}{\isachardoublequote}}] prints a well-typed term \isa{{\isachardoublequote}t{\isachardoublequote}}.
5.591 +
5.592 + \item [\isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}const\ c{\isacharbraceright}{\isachardoublequote}}] prints a logical or syntactic constant
5.593 + \isa{{\isachardoublequote}c{\isachardoublequote}}.
5.594 +
5.595 + \item [\isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}abbrev\ c\ x\isactrlsub {\isadigit{1}}\ {\isasymdots}\ x\isactrlsub n{\isacharbraceright}{\isachardoublequote}}] prints a constant
5.596 + abbreviation \isa{{\isachardoublequote}c\ x\isactrlsub {\isadigit{1}}\ {\isasymdots}\ x\isactrlsub n\ {\isasymequiv}\ rhs{\isachardoublequote}} as defined in
5.597 + the current context.
5.598 +
5.599 + \item [\isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}typeof\ t{\isacharbraceright}{\isachardoublequote}}] prints the type of a well-typed term
5.600 + \isa{{\isachardoublequote}t{\isachardoublequote}}.
5.601 +
5.602 + \item [\isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}typ\ {\isasymtau}{\isacharbraceright}{\isachardoublequote}}] prints a well-formed type \isa{{\isachardoublequote}{\isasymtau}{\isachardoublequote}}.
5.603 +
5.604 + \item [\isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}thm{\isacharunderscore}style\ s\ a{\isacharbraceright}{\isachardoublequote}}] prints theorem \isa{a},
5.605 + previously applying a style \isa{s} to it (see below).
5.606 +
5.607 + \item [\isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}term{\isacharunderscore}style\ s\ t{\isacharbraceright}{\isachardoublequote}}] prints a well-typed term \isa{t} after applying a style \isa{s} to it (see below).
5.608 +
5.609 + \item [\isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}text\ s{\isacharbraceright}{\isachardoublequote}}] prints uninterpreted source text \isa{s}. This is particularly useful to print portions of text according
5.610 + to the Isabelle {\LaTeX} output style, without demanding
5.611 + well-formedness (e.g.\ small pieces of terms that should not be
5.612 + parsed or type-checked yet).
5.613 +
5.614 + \item [\isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}goals{\isacharbraceright}{\isachardoublequote}}] prints the current \emph{dynamic} goal
5.615 + state. This is mainly for support of tactic-emulation scripts
5.616 + within Isar --- presentation of goal states does not conform to
5.617 + actual human-readable proof documents.
5.618 +
5.619 + Please do not include goal states into document output unless you
5.620 + really know what you are doing!
5.621 +
5.622 + \item [\isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}subgoals{\isacharbraceright}{\isachardoublequote}}] is similar to \isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}goals{\isacharbraceright}{\isachardoublequote}}, but
5.623 + does not print the main goal.
5.624 +
5.625 + \item [\isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}prf\ a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n{\isacharbraceright}{\isachardoublequote}}] prints the (compact)
5.626 + proof terms corresponding to the theorems \isa{{\isachardoublequote}a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n{\isachardoublequote}}. Note that this requires proof terms to be switched on
5.627 + for the current object logic (see the ``Proof terms'' section of the
5.628 + Isabelle reference manual for information on how to do this).
5.629 +
5.630 + \item [\isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}full{\isacharunderscore}prf\ a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n{\isacharbraceright}{\isachardoublequote}}] is like \isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}prf\ a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n{\isacharbraceright}{\isachardoublequote}}, but displays the full proof terms,
5.631 + i.e.\ also displays information omitted in the compact proof term,
5.632 + which is denoted by ``\isa{{\isacharunderscore}}'' placeholders there.
5.633 +
5.634 + \item [\isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}ML\ s{\isacharbraceright}{\isachardoublequote}}, \isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}ML{\isacharunderscore}type\ s{\isacharbraceright}{\isachardoublequote}}, and \isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}ML{\isacharunderscore}struct\ s{\isacharbraceright}{\isachardoublequote}}] check text \isa{s} as ML value, type, and
5.635 + structure, respectively. The source is displayed verbatim.
5.636 +
5.637 + \end{descr}
5.638 +
5.639 + \medskip The following standard styles for use with \isa{thm{\isacharunderscore}style} and \isa{term{\isacharunderscore}style} are available:
5.640 +
5.641 + \begin{descr}
5.642 +
5.643 + \item [\isa{lhs}] extracts the first argument of any application
5.644 + form with at least two arguments -- typically meta-level or
5.645 + object-level equality, or any other binary relation.
5.646 +
5.647 + \item [\isa{rhs}] is like \isa{lhs}, but extracts the second
5.648 + argument.
5.649 +
5.650 + \item [\isa{{\isachardoublequote}concl{\isachardoublequote}}] extracts the conclusion \isa{C} from a rule
5.651 + in Horn-clause normal form \isa{{\isachardoublequote}A\isactrlsub {\isadigit{1}}\ {\isasymLongrightarrow}\ {\isasymdots}\ A\isactrlsub n\ {\isasymLongrightarrow}\ C{\isachardoublequote}}.
5.652 +
5.653 + \item [\isa{{\isachardoublequote}prem{\isadigit{1}}{\isachardoublequote}}, \dots, \isa{{\isachardoublequote}prem{\isadigit{9}}{\isachardoublequote}}] extract premise
5.654 + number \isa{{\isachardoublequote}{\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isadigit{9}}{\isachardoublequote}}, respectively, from from a rule in
5.655 + Horn-clause normal form \isa{{\isachardoublequote}A\isactrlsub {\isadigit{1}}\ {\isasymLongrightarrow}\ {\isasymdots}\ A\isactrlsub n\ {\isasymLongrightarrow}\ C{\isachardoublequote}}
5.656 +
5.657 + \end{descr}
5.658 +
5.659 + \medskip
5.660 + The following options are available to tune the output. Note that most of
5.661 + these coincide with ML flags of the same names (see also \cite{isabelle-ref}).
5.662 +
5.663 + \begin{descr}
5.664 +
5.665 + \item[\isa{{\isachardoublequote}show{\isacharunderscore}types\ {\isacharequal}\ bool{\isachardoublequote}} and \isa{{\isachardoublequote}show{\isacharunderscore}sorts\ {\isacharequal}\ bool{\isachardoublequote}}]
5.666 + control printing of explicit type and sort constraints.
5.667 +
5.668 + \item[\isa{{\isachardoublequote}show{\isacharunderscore}structs\ {\isacharequal}\ bool{\isachardoublequote}}] controls printing of implicit
5.669 + structures.
5.670 +
5.671 + \item[\isa{{\isachardoublequote}long{\isacharunderscore}names\ {\isacharequal}\ bool{\isachardoublequote}}] forces names of types and
5.672 + constants etc.\ to be printed in their fully qualified internal
5.673 + form.
5.674 +
5.675 + \item[\isa{{\isachardoublequote}short{\isacharunderscore}names\ {\isacharequal}\ bool{\isachardoublequote}}] forces names of types and
5.676 + constants etc.\ to be printed unqualified. Note that internalizing
5.677 + the output again in the current context may well yield a different
5.678 + result.
5.679 +
5.680 + \item[\isa{{\isachardoublequote}unique{\isacharunderscore}names\ {\isacharequal}\ bool{\isachardoublequote}}] determines whether the printed
5.681 + version of qualified names should be made sufficiently long to avoid
5.682 + overlap with names declared further back. Set to \isa{false} for
5.683 + more concise output.
5.684 +
5.685 + \item[\isa{{\isachardoublequote}eta{\isacharunderscore}contract\ {\isacharequal}\ bool{\isachardoublequote}}] prints terms in \isa{{\isasymeta}}-contracted form.
5.686 +
5.687 + \item[\isa{{\isachardoublequote}display\ {\isacharequal}\ bool{\isachardoublequote}}] indicates if the text is to be
5.688 + output as multi-line ``display material'', rather than a small piece
5.689 + of text without line breaks (which is the default).
5.690 +
5.691 + \item[\isa{{\isachardoublequote}break\ {\isacharequal}\ bool{\isachardoublequote}}] controls line breaks in non-display
5.692 + material.
5.693 +
5.694 + \item[\isa{{\isachardoublequote}quotes\ {\isacharequal}\ bool{\isachardoublequote}}] indicates if the output should be
5.695 + enclosed in double quotes.
5.696 +
5.697 + \item[\isa{{\isachardoublequote}mode\ {\isacharequal}\ name{\isachardoublequote}}] adds \isa{name} to the print mode to
5.698 + be used for presentation (see also \cite{isabelle-ref}). Note that
5.699 + the standard setup for {\LaTeX} output is already present by
5.700 + default, including the modes \isa{latex} and \isa{xsymbols}.
5.701 +
5.702 + \item[\isa{{\isachardoublequote}margin\ {\isacharequal}\ nat{\isachardoublequote}} and \isa{{\isachardoublequote}indent\ {\isacharequal}\ nat{\isachardoublequote}}] change the
5.703 + margin or indentation for pretty printing of display material.
5.704 +
5.705 + \item[\isa{{\isachardoublequote}source\ {\isacharequal}\ bool{\isachardoublequote}}] prints the source text of the
5.706 + antiquotation arguments, rather than the actual value. Note that
5.707 + this does not affect well-formedness checks of \hyperlink{antiquotation.thm}{\mbox{\isa{thm}}}, \hyperlink{antiquotation.term}{\mbox{\isa{term}}}, etc. (only the \hyperlink{antiquotation.text}{\mbox{\isa{text}}} antiquotation admits arbitrary output).
5.708 +
5.709 + \item[\isa{{\isachardoublequote}goals{\isacharunderscore}limit\ {\isacharequal}\ nat{\isachardoublequote}}] determines the maximum number of
5.710 + goals to be printed.
5.711 +
5.712 + \item[\isa{{\isachardoublequote}locale\ {\isacharequal}\ name{\isachardoublequote}}] specifies an alternative locale
5.713 + context used for evaluating and printing the subsequent argument.
5.714 +
5.715 + \end{descr}
5.716 +
5.717 + For boolean flags, ``\isa{{\isachardoublequote}name\ {\isacharequal}\ true{\isachardoublequote}}'' may be abbreviated as
5.718 + ``\isa{name}''. All of the above flags are disabled by default,
5.719 + unless changed from ML.
5.720 +
5.721 + \medskip Note that antiquotations do not only spare the author from
5.722 + tedious typing of logical entities, but also achieve some degree of
5.723 + consistency-checking of informal explanations with formal
5.724 + developments: well-formedness of terms and types with respect to the
5.725 + current theory or proof context is ensured here.%
5.726 +\end{isamarkuptext}%
5.727 +\isamarkuptrue%
5.728 +%
5.729 +\isamarkupsubsection{Tagged commands \label{sec:tags}%
5.730 +}
5.731 +\isamarkuptrue%
5.732 +%
5.733 +\begin{isamarkuptext}%
5.734 +Each Isabelle/Isar command may be decorated by presentation tags:
5.735 +
5.736 + \indexouternonterm{tags}
5.737 + \begin{rail}
5.738 + tags: ( tag * )
5.739 + ;
5.740 + tag: '\%' (ident | string)
5.741 + \end{rail}
5.742 +
5.743 + The tags \isa{{\isachardoublequote}theory{\isachardoublequote}}, \isa{{\isachardoublequote}proof{\isachardoublequote}}, \isa{{\isachardoublequote}ML{\isachardoublequote}} are already
5.744 + pre-declared for certain classes of commands:
5.745 +
5.746 + \medskip
5.747 +
5.748 + \begin{tabular}{ll}
5.749 + \isa{{\isachardoublequote}theory{\isachardoublequote}} & theory begin/end \\
5.750 + \isa{{\isachardoublequote}proof{\isachardoublequote}} & all proof commands \\
5.751 + \isa{{\isachardoublequote}ML{\isachardoublequote}} & all commands involving ML code \\
5.752 + \end{tabular}
5.753 +
5.754 + \medskip The Isabelle document preparation system (see also
5.755 + \cite{isabelle-sys}) allows tagged command regions to be presented
5.756 + specifically, e.g.\ to fold proof texts, or drop parts of the text
5.757 + completely.
5.758 +
5.759 + For example ``\hyperlink{command.by}{\mbox{\isa{\isacommand{by}}}}~\isa{{\isachardoublequote}{\isacharpercent}invisible\ auto{\isachardoublequote}}'' would
5.760 + cause that piece of proof to be treated as \isa{invisible} instead
5.761 + of \isa{{\isachardoublequote}proof{\isachardoublequote}} (the default), which may be either show or hidden
5.762 + depending on the document setup. In contrast, ``\hyperlink{command.by}{\mbox{\isa{\isacommand{by}}}}~\isa{{\isachardoublequote}{\isacharpercent}visible\ auto{\isachardoublequote}}'' would force this text to be shown
5.763 + invariably.
5.764 +
5.765 + Explicit tag specifications within a proof apply to all subsequent
5.766 + commands of the same level of nesting. For example, ``\hyperlink{command.proof}{\mbox{\isa{\isacommand{proof}}}}~\isa{{\isachardoublequote}{\isacharpercent}visible\ {\isasymdots}{\isachardoublequote}}~\hyperlink{command.qed}{\mbox{\isa{\isacommand{qed}}}}'' would force the
5.767 + whole sub-proof to be typeset as \isa{visible} (unless some of its
5.768 + parts are tagged differently).%
5.769 +\end{isamarkuptext}%
5.770 +\isamarkuptrue%
5.771 +%
5.772 +\isadelimtheory
5.773 +%
5.774 +\endisadelimtheory
5.775 +%
5.776 +\isatagtheory
5.777 +\isacommand{end}\isamarkupfalse%
5.778 +%
5.779 +\endisatagtheory
5.780 +{\isafoldtheory}%
5.781 +%
5.782 +\isadelimtheory
5.783 +%
5.784 +\endisadelimtheory
5.785 +\isanewline
5.786 +\end{isabellebody}%
5.787 +%%% Local Variables:
5.788 +%%% mode: latex
5.789 +%%% TeX-master: "root"
5.790 +%%% End:
6.1 --- a/doc-src/IsarRef/Thy/syntax.thy Mon Jun 02 21:13:48 2008 +0200
6.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
6.3 @@ -1,750 +0,0 @@
6.4 -(* $Id$ *)
6.5 -
6.6 -theory "syntax"
6.7 -imports Pure
6.8 -begin
6.9 -
6.10 -chapter {* Syntax primitives *}
6.11 -
6.12 -text {*
6.13 - The rather generic framework of Isabelle/Isar syntax emerges from
6.14 - three main syntactic categories: \emph{commands} of the top-level
6.15 - Isar engine (covering theory and proof elements), \emph{methods} for
6.16 - general goal refinements (analogous to traditional ``tactics''), and
6.17 - \emph{attributes} for operations on facts (within a certain
6.18 - context). Subsequently we give a reference of basic syntactic
6.19 - entities underlying Isabelle/Isar syntax in a bottom-up manner.
6.20 - Concrete theory and proof language elements will be introduced later
6.21 - on.
6.22 -
6.23 - \medskip In order to get started with writing well-formed
6.24 - Isabelle/Isar documents, the most important aspect to be noted is
6.25 - the difference of \emph{inner} versus \emph{outer} syntax. Inner
6.26 - syntax is that of Isabelle types and terms of the logic, while outer
6.27 - syntax is that of Isabelle/Isar theory sources (specifications and
6.28 - proofs). As a general rule, inner syntax entities may occur only as
6.29 - \emph{atomic entities} within outer syntax. For example, the string
6.30 - @{verbatim "\"x + y\""} and identifier @{verbatim z} are legal term
6.31 - specifications within a theory, while @{verbatim "x + y"} without
6.32 - quotes is not.
6.33 -
6.34 - Printed theory documents usually omit quotes to gain readability
6.35 - (this is a matter of {\LaTeX} macro setup, say via @{verbatim
6.36 - "\\isabellestyle"}, see also \cite{isabelle-sys}). Experienced
6.37 - users of Isabelle/Isar may easily reconstruct the lost technical
6.38 - information, while mere readers need not care about quotes at all.
6.39 -
6.40 - \medskip Isabelle/Isar input may contain any number of input
6.41 - termination characters ``@{verbatim ";"}'' (semicolon) to separate
6.42 - commands explicitly. This is particularly useful in interactive
6.43 - shell sessions to make clear where the current command is intended
6.44 - to end. Otherwise, the interpreter loop will continue to issue a
6.45 - secondary prompt ``@{verbatim "#"}'' until an end-of-command is
6.46 - clearly recognized from the input syntax, e.g.\ encounter of the
6.47 - next command keyword.
6.48 -
6.49 - More advanced interfaces such as Proof~General \cite{proofgeneral}
6.50 - do not require explicit semicolons, the amount of input text is
6.51 - determined automatically by inspecting the present content of the
6.52 - Emacs text buffer. In the printed presentation of Isabelle/Isar
6.53 - documents semicolons are omitted altogether for readability.
6.54 -
6.55 - \begin{warn}
6.56 - Proof~General requires certain syntax classification tables in
6.57 - order to achieve properly synchronized interaction with the
6.58 - Isabelle/Isar process. These tables need to be consistent with
6.59 - the Isabelle version and particular logic image to be used in a
6.60 - running session (common object-logics may well change the outer
6.61 - syntax). The standard setup should work correctly with any of the
6.62 - ``official'' logic images derived from Isabelle/HOL (including
6.63 - HOLCF etc.). Users of alternative logics may need to tell
6.64 - Proof~General explicitly, e.g.\ by giving an option @{verbatim "-k ZF"}
6.65 - (in conjunction with @{verbatim "-l ZF"}, to specify the default
6.66 - logic image). Note that option @{verbatim "-L"} does both
6.67 - of this at the same time.
6.68 - \end{warn}
6.69 -*}
6.70 -
6.71 -
6.72 -section {* Lexical matters \label{sec:lex-syntax} *}
6.73 -
6.74 -text {*
6.75 - The Isabelle/Isar outer syntax provides token classes as presented
6.76 - below; most of these coincide with the inner lexical syntax as
6.77 - presented in \cite{isabelle-ref}.
6.78 -
6.79 - \begin{matharray}{rcl}
6.80 - @{syntax_def ident} & = & letter\,quasiletter^* \\
6.81 - @{syntax_def longident} & = & ident (\verb,.,ident)^+ \\
6.82 - @{syntax_def symident} & = & sym^+ ~|~ \verb,\,\verb,<,ident\verb,>, \\
6.83 - @{syntax_def nat} & = & digit^+ \\
6.84 - @{syntax_def var} & = & ident ~|~ \verb,?,ident ~|~ \verb,?,ident\verb,.,nat \\
6.85 - @{syntax_def typefree} & = & \verb,',ident \\
6.86 - @{syntax_def typevar} & = & typefree ~|~ \verb,?,typefree ~|~ \verb,?,typefree\verb,.,nat \\
6.87 - @{syntax_def string} & = & \verb,", ~\dots~ \verb,", \\
6.88 - @{syntax_def altstring} & = & \backquote ~\dots~ \backquote \\
6.89 - @{syntax_def verbatim} & = & \verb,{*, ~\dots~ \verb,*,\verb,}, \\[1ex]
6.90 -
6.91 - letter & = & latin ~|~ \verb,\,\verb,<,latin\verb,>, ~|~ \verb,\,\verb,<,latin\,latin\verb,>, ~|~ greek ~|~ \\
6.92 - & & \verb,\<^isub>, ~|~ \verb,\<^isup>, \\
6.93 - quasiletter & = & letter ~|~ digit ~|~ \verb,_, ~|~ \verb,', \\
6.94 - latin & = & \verb,a, ~|~ \dots ~|~ \verb,z, ~|~ \verb,A, ~|~ \dots ~|~ \verb,Z, \\
6.95 - digit & = & \verb,0, ~|~ \dots ~|~ \verb,9, \\
6.96 - sym & = & \verb,!, ~|~ \verb,#, ~|~ \verb,$, ~|~ \verb,%, ~|~ \verb,&, ~|~
6.97 - \verb,*, ~|~ \verb,+, ~|~ \verb,-, ~|~ \verb,/, ~|~ \\
6.98 - & & \verb,<, ~|~ \verb,=, ~|~ \verb,>, ~|~ \verb,?, ~|~ \texttt{\at} ~|~
6.99 - \verb,^, ~|~ \verb,_, ~|~ \verb,|, ~|~ \verb,~, \\
6.100 - greek & = & \verb,\<alpha>, ~|~ \verb,\<beta>, ~|~ \verb,\<gamma>, ~|~ \verb,\<delta>, ~| \\
6.101 - & & \verb,\<epsilon>, ~|~ \verb,\<zeta>, ~|~ \verb,\<eta>, ~|~ \verb,\<theta>, ~| \\
6.102 - & & \verb,\<iota>, ~|~ \verb,\<kappa>, ~|~ \verb,\<mu>, ~|~ \verb,\<nu>, ~| \\
6.103 - & & \verb,\<xi>, ~|~ \verb,\<pi>, ~|~ \verb,\<rho>, ~|~ \verb,\<sigma>, ~|~ \verb,\<tau>, ~| \\
6.104 - & & \verb,\<upsilon>, ~|~ \verb,\<phi>, ~|~ \verb,\<chi>, ~|~ \verb,\<psi>, ~| \\
6.105 - & & \verb,\<omega>, ~|~ \verb,\<Gamma>, ~|~ \verb,\<Delta>, ~|~ \verb,\<Theta>, ~| \\
6.106 - & & \verb,\<Lambda>, ~|~ \verb,\<Xi>, ~|~ \verb,\<Pi>, ~|~ \verb,\<Sigma>, ~| \\
6.107 - & & \verb,\<Upsilon>, ~|~ \verb,\<Phi>, ~|~ \verb,\<Psi>, ~|~ \verb,\<Omega>, \\
6.108 - \end{matharray}
6.109 -
6.110 - The syntax of @{syntax string} admits any characters, including
6.111 - newlines; ``@{verbatim "\""}'' (double-quote) and ``@{verbatim
6.112 - "\\"}'' (backslash) need to be escaped by a backslash; arbitrary
6.113 - character codes may be specified as ``@{verbatim "\\"}@{text ddd}'',
6.114 - with three decimal digits. Alternative strings according to
6.115 - @{syntax altstring} are analogous, using single back-quotes instead.
6.116 - The body of @{syntax verbatim} may consist of any text not
6.117 - containing ``@{verbatim "*"}@{verbatim "}"}''; this allows
6.118 - convenient inclusion of quotes without further escapes. The greek
6.119 - letters do \emph{not} include @{verbatim "\<lambda>"}, which is already used
6.120 - differently in the meta-logic.
6.121 -
6.122 - Common mathematical symbols such as @{text \<forall>} are represented in
6.123 - Isabelle as @{verbatim \<forall>}. There are infinitely many Isabelle
6.124 - symbols like this, although proper presentation is left to front-end
6.125 - tools such as {\LaTeX} or Proof~General with the X-Symbol package.
6.126 - A list of standard Isabelle symbols that work well with these tools
6.127 - is given in \cite[appendix~A]{isabelle-sys}.
6.128 -
6.129 - Source comments take the form @{verbatim "(*"}~@{text
6.130 - "\<dots>"}~@{verbatim "*)"} and may be nested, although user-interface
6.131 - tools might prevent this. Note that this form indicates source
6.132 - comments only, which are stripped after lexical analysis of the
6.133 - input. The Isar document syntax also provides formal comments that
6.134 - are considered as part of the text (see \secref{sec:comments}).
6.135 -*}
6.136 -
6.137 -
6.138 -section {* Common syntax entities *}
6.139 -
6.140 -text {*
6.141 - We now introduce several basic syntactic entities, such as names,
6.142 - terms, and theorem specifications, which are factored out of the
6.143 - actual Isar language elements to be described later.
6.144 -*}
6.145 -
6.146 -
6.147 -subsection {* Names *}
6.148 -
6.149 -text {*
6.150 - Entity \railqtok{name} usually refers to any name of types,
6.151 - constants, theorems etc.\ that are to be \emph{declared} or
6.152 - \emph{defined} (so qualified identifiers are excluded here). Quoted
6.153 - strings provide an escape for non-identifier names or those ruled
6.154 - out by outer syntax keywords (e.g.\ quoted @{verbatim "\"let\""}).
6.155 - Already existing objects are usually referenced by
6.156 - \railqtok{nameref}.
6.157 -
6.158 - \indexoutertoken{name}\indexoutertoken{parname}\indexoutertoken{nameref}
6.159 - \indexoutertoken{int}
6.160 - \begin{rail}
6.161 - name: ident | symident | string | nat
6.162 - ;
6.163 - parname: '(' name ')'
6.164 - ;
6.165 - nameref: name | longident
6.166 - ;
6.167 - int: nat | '-' nat
6.168 - ;
6.169 - \end{rail}
6.170 -*}
6.171 -
6.172 -
6.173 -subsection {* Comments \label{sec:comments} *}
6.174 -
6.175 -text {*
6.176 - Large chunks of plain \railqtok{text} are usually given
6.177 - \railtok{verbatim}, i.e.\ enclosed in @{verbatim "{"}@{verbatim
6.178 - "*"}~@{text "\<dots>"}~@{verbatim "*"}@{verbatim "}"}. For convenience,
6.179 - any of the smaller text units conforming to \railqtok{nameref} are
6.180 - admitted as well. A marginal \railnonterm{comment} is of the form
6.181 - @{verbatim "--"} \railqtok{text}. Any number of these may occur
6.182 - within Isabelle/Isar commands.
6.183 -
6.184 - \indexoutertoken{text}\indexouternonterm{comment}
6.185 - \begin{rail}
6.186 - text: verbatim | nameref
6.187 - ;
6.188 - comment: '--' text
6.189 - ;
6.190 - \end{rail}
6.191 -*}
6.192 -
6.193 -
6.194 -subsection {* Type classes, sorts and arities *}
6.195 -
6.196 -text {*
6.197 - Classes are specified by plain names. Sorts have a very simple
6.198 - inner syntax, which is either a single class name @{text c} or a
6.199 - list @{text "{c\<^sub>1, \<dots>, c\<^sub>n}"} referring to the
6.200 - intersection of these classes. The syntax of type arities is given
6.201 - directly at the outer level.
6.202 -
6.203 - \indexouternonterm{sort}\indexouternonterm{arity}
6.204 - \indexouternonterm{classdecl}
6.205 - \begin{rail}
6.206 - classdecl: name (('<' | subseteq) (nameref + ','))?
6.207 - ;
6.208 - sort: nameref
6.209 - ;
6.210 - arity: ('(' (sort + ',') ')')? sort
6.211 - ;
6.212 - \end{rail}
6.213 -*}
6.214 -
6.215 -
6.216 -subsection {* Types and terms \label{sec:types-terms} *}
6.217 -
6.218 -text {*
6.219 - The actual inner Isabelle syntax, that of types and terms of the
6.220 - logic, is far too sophisticated in order to be modelled explicitly
6.221 - at the outer theory level. Basically, any such entity has to be
6.222 - quoted to turn it into a single token (the parsing and type-checking
6.223 - is performed internally later). For convenience, a slightly more
6.224 - liberal convention is adopted: quotes may be omitted for any type or
6.225 - term that is already atomic at the outer level. For example, one
6.226 - may just write @{verbatim x} instead of quoted @{verbatim "\"x\""}.
6.227 - Note that symbolic identifiers (e.g.\ @{verbatim "++"} or @{text
6.228 - "\<forall>"} are available as well, provided these have not been superseded
6.229 - by commands or other keywords already (such as @{verbatim "="} or
6.230 - @{verbatim "+"}).
6.231 -
6.232 - \indexoutertoken{type}\indexoutertoken{term}\indexoutertoken{prop}
6.233 - \begin{rail}
6.234 - type: nameref | typefree | typevar
6.235 - ;
6.236 - term: nameref | var
6.237 - ;
6.238 - prop: term
6.239 - ;
6.240 - \end{rail}
6.241 -
6.242 - Positional instantiations are indicated by giving a sequence of
6.243 - terms, or the placeholder ``@{text _}'' (underscore), which means to
6.244 - skip a position.
6.245 -
6.246 - \indexoutertoken{inst}\indexoutertoken{insts}
6.247 - \begin{rail}
6.248 - inst: underscore | term
6.249 - ;
6.250 - insts: (inst *)
6.251 - ;
6.252 - \end{rail}
6.253 -
6.254 - Type declarations and definitions usually refer to
6.255 - \railnonterm{typespec} on the left-hand side. This models basic
6.256 - type constructor application at the outer syntax level. Note that
6.257 - only plain postfix notation is available here, but no infixes.
6.258 -
6.259 - \indexouternonterm{typespec}
6.260 - \begin{rail}
6.261 - typespec: (() | typefree | '(' ( typefree + ',' ) ')') name
6.262 - ;
6.263 - \end{rail}
6.264 -*}
6.265 -
6.266 -
6.267 -subsection {* Mixfix annotations *}
6.268 -
6.269 -text {*
6.270 - Mixfix annotations specify concrete \emph{inner} syntax of Isabelle
6.271 - types and terms. Some commands such as @{command "types"} (see
6.272 - \secref{sec:types-pure}) admit infixes only, while @{command
6.273 - "consts"} (see \secref{sec:consts}) and @{command "syntax"} (see
6.274 - \secref{sec:syn-trans}) support the full range of general mixfixes
6.275 - and binders.
6.276 -
6.277 - \indexouternonterm{infix}\indexouternonterm{mixfix}\indexouternonterm{structmixfix}
6.278 - \begin{rail}
6.279 - infix: '(' ('infix' | 'infixl' | 'infixr') string? nat ')'
6.280 - ;
6.281 - mixfix: infix | '(' string prios? nat? ')' | '(' 'binder' string prios? nat ')'
6.282 - ;
6.283 - structmixfix: mixfix | '(' 'structure' ')'
6.284 - ;
6.285 -
6.286 - prios: '[' (nat + ',') ']'
6.287 - ;
6.288 - \end{rail}
6.289 -
6.290 - Here the \railtok{string} specifications refer to the actual mixfix
6.291 - template (see also \cite{isabelle-ref}), which may include literal
6.292 - text, spacing, blocks, and arguments (denoted by ``@{text _}''); the
6.293 - special symbol ``@{verbatim "\<index>"}'' (printed as ``@{text "\<index>"}'')
6.294 - represents an index argument that specifies an implicit structure
6.295 - reference (see also \secref{sec:locale}). Infix and binder
6.296 - declarations provide common abbreviations for particular mixfix
6.297 - declarations. So in practice, mixfix templates mostly degenerate to
6.298 - literal text for concrete syntax, such as ``@{verbatim "++"}'' for
6.299 - an infix symbol, or ``@{verbatim "++"}@{text "\<index>"}'' for an infix of
6.300 - an implicit structure.
6.301 -*}
6.302 -
6.303 -
6.304 -subsection {* Proof methods \label{sec:syn-meth} *}
6.305 -
6.306 -text {*
6.307 - Proof methods are either basic ones, or expressions composed of
6.308 - methods via ``@{verbatim ","}'' (sequential composition),
6.309 - ``@{verbatim "|"}'' (alternative choices), ``@{verbatim "?"}''
6.310 - (try), ``@{verbatim "+"}'' (repeat at least once), ``@{verbatim
6.311 - "["}@{text n}@{verbatim "]"}'' (restriction to first @{text n}
6.312 - sub-goals, with default @{text "n = 1"}). In practice, proof
6.313 - methods are usually just a comma separated list of
6.314 - \railqtok{nameref}~\railnonterm{args} specifications. Note that
6.315 - parentheses may be dropped for single method specifications (with no
6.316 - arguments).
6.317 -
6.318 - \indexouternonterm{method}
6.319 - \begin{rail}
6.320 - method: (nameref | '(' methods ')') (() | '?' | '+' | '[' nat? ']')
6.321 - ;
6.322 - methods: (nameref args | method) + (',' | '|')
6.323 - ;
6.324 - \end{rail}
6.325 -
6.326 - Proper Isar proof methods do \emph{not} admit arbitrary goal
6.327 - addressing, but refer either to the first sub-goal or all sub-goals
6.328 - uniformly. The goal restriction operator ``@{text "[n]"}''
6.329 - evaluates a method expression within a sandbox consisting of the
6.330 - first @{text n} sub-goals (which need to exist). For example, the
6.331 - method ``@{text "simp_all[3]"}'' simplifies the first three
6.332 - sub-goals, while ``@{text "(rule foo, simp_all)[]"}'' simplifies all
6.333 - new goals that emerge from applying rule @{text "foo"} to the
6.334 - originally first one.
6.335 -
6.336 - Improper methods, notably tactic emulations, offer a separate
6.337 - low-level goal addressing scheme as explicit argument to the
6.338 - individual tactic being involved. Here ``@{text "[!]"}'' refers to
6.339 - all goals, and ``@{text "[n-]"}'' to all goals starting from @{text
6.340 - "n"}.
6.341 -
6.342 - \indexouternonterm{goalspec}
6.343 - \begin{rail}
6.344 - goalspec: '[' (nat '-' nat | nat '-' | nat | '!' ) ']'
6.345 - ;
6.346 - \end{rail}
6.347 -*}
6.348 -
6.349 -
6.350 -subsection {* Attributes and theorems \label{sec:syn-att} *}
6.351 -
6.352 -text {*
6.353 - Attributes (and proof methods, see \secref{sec:syn-meth}) have their
6.354 - own ``semi-inner'' syntax, in the sense that input conforming to
6.355 - \railnonterm{args} below is parsed by the attribute a second time.
6.356 - The attribute argument specifications may be any sequence of atomic
6.357 - entities (identifiers, strings etc.), or properly bracketed argument
6.358 - lists. Below \railqtok{atom} refers to any atomic entity, including
6.359 - any \railtok{keyword} conforming to \railtok{symident}.
6.360 -
6.361 - \indexoutertoken{atom}\indexouternonterm{args}\indexouternonterm{attributes}
6.362 - \begin{rail}
6.363 - atom: nameref | typefree | typevar | var | nat | keyword
6.364 - ;
6.365 - arg: atom | '(' args ')' | '[' args ']'
6.366 - ;
6.367 - args: arg *
6.368 - ;
6.369 - attributes: '[' (nameref args * ',') ']'
6.370 - ;
6.371 - \end{rail}
6.372 -
6.373 - Theorem specifications come in several flavors:
6.374 - \railnonterm{axmdecl} and \railnonterm{thmdecl} usually refer to
6.375 - axioms, assumptions or results of goal statements, while
6.376 - \railnonterm{thmdef} collects lists of existing theorems. Existing
6.377 - theorems are given by \railnonterm{thmref} and
6.378 - \railnonterm{thmrefs}, the former requires an actual singleton
6.379 - result.
6.380 -
6.381 - There are three forms of theorem references:
6.382 - \begin{enumerate}
6.383 -
6.384 - \item named facts @{text "a"},
6.385 -
6.386 - \item selections from named facts @{text "a(i)"} or @{text "a(j - k)"},
6.387 -
6.388 - \item literal fact propositions using @{syntax_ref altstring} syntax
6.389 - @{verbatim "`"}@{text "\<phi>"}@{verbatim "`"} (see also method
6.390 - @{method_ref fact} in \secref{sec:pure-meth-att}).
6.391 -
6.392 - \end{enumerate}
6.393 -
6.394 - Any kind of theorem specification may include lists of attributes
6.395 - both on the left and right hand sides; attributes are applied to any
6.396 - immediately preceding fact. If names are omitted, the theorems are
6.397 - not stored within the theorem database of the theory or proof
6.398 - context, but any given attributes are applied nonetheless.
6.399 -
6.400 - An extra pair of brackets around attributes (like ``@{text
6.401 - "[[simproc a]]"}'') abbreviates a theorem reference involving an
6.402 - internal dummy fact, which will be ignored later on. So only the
6.403 - effect of the attribute on the background context will persist.
6.404 - This form of in-place declarations is particularly useful with
6.405 - commands like @{command "declare"} and @{command "using"}.
6.406 -
6.407 - \indexouternonterm{axmdecl}\indexouternonterm{thmdecl}
6.408 - \indexouternonterm{thmdef}\indexouternonterm{thmref}
6.409 - \indexouternonterm{thmrefs}\indexouternonterm{selection}
6.410 - \begin{rail}
6.411 - axmdecl: name attributes? ':'
6.412 - ;
6.413 - thmdecl: thmbind ':'
6.414 - ;
6.415 - thmdef: thmbind '='
6.416 - ;
6.417 - thmref: (nameref selection? | altstring) attributes? | '[' attributes ']'
6.418 - ;
6.419 - thmrefs: thmref +
6.420 - ;
6.421 -
6.422 - thmbind: name attributes | name | attributes
6.423 - ;
6.424 - selection: '(' ((nat | nat '-' nat?) + ',') ')'
6.425 - ;
6.426 - \end{rail}
6.427 -*}
6.428 -
6.429 -
6.430 -subsection {* Term patterns and declarations \label{sec:term-decls} *}
6.431 -
6.432 -text {*
6.433 - Wherever explicit propositions (or term fragments) occur in a proof
6.434 - text, casual binding of schematic term variables may be given
6.435 - specified via patterns of the form ``@{text "(\<IS> p\<^sub>1 \<dots>
6.436 - p\<^sub>n)"}''. This works both for \railqtok{term} and \railqtok{prop}.
6.437 -
6.438 - \indexouternonterm{termpat}\indexouternonterm{proppat}
6.439 - \begin{rail}
6.440 - termpat: '(' ('is' term +) ')'
6.441 - ;
6.442 - proppat: '(' ('is' prop +) ')'
6.443 - ;
6.444 - \end{rail}
6.445 -
6.446 - \medskip Declarations of local variables @{text "x :: \<tau>"} and
6.447 - logical propositions @{text "a : \<phi>"} represent different views on
6.448 - the same principle of introducing a local scope. In practice, one
6.449 - may usually omit the typing of \railnonterm{vars} (due to
6.450 - type-inference), and the naming of propositions (due to implicit
6.451 - references of current facts). In any case, Isar proof elements
6.452 - usually admit to introduce multiple such items simultaneously.
6.453 -
6.454 - \indexouternonterm{vars}\indexouternonterm{props}
6.455 - \begin{rail}
6.456 - vars: (name+) ('::' type)?
6.457 - ;
6.458 - props: thmdecl? (prop proppat? +)
6.459 - ;
6.460 - \end{rail}
6.461 -
6.462 - The treatment of multiple declarations corresponds to the
6.463 - complementary focus of \railnonterm{vars} versus
6.464 - \railnonterm{props}. In ``@{text "x\<^sub>1 \<dots> x\<^sub>n :: \<tau>"}''
6.465 - the typing refers to all variables, while in @{text "a: \<phi>\<^sub>1 \<dots>
6.466 - \<phi>\<^sub>n"} the naming refers to all propositions collectively.
6.467 - Isar language elements that refer to \railnonterm{vars} or
6.468 - \railnonterm{props} typically admit separate typings or namings via
6.469 - another level of iteration, with explicit @{keyword_ref "and"}
6.470 - separators; e.g.\ see @{command "fix"} and @{command "assume"} in
6.471 - \secref{sec:proof-context}.
6.472 -*}
6.473 -
6.474 -
6.475 -subsection {* Antiquotations \label{sec:antiq} *}
6.476 -
6.477 -text {*
6.478 - \begin{matharray}{rcl}
6.479 - @{antiquotation_def "theory"} & : & \isarantiq \\
6.480 - @{antiquotation_def "thm"} & : & \isarantiq \\
6.481 - @{antiquotation_def "prop"} & : & \isarantiq \\
6.482 - @{antiquotation_def "term"} & : & \isarantiq \\
6.483 - @{antiquotation_def const} & : & \isarantiq \\
6.484 - @{antiquotation_def abbrev} & : & \isarantiq \\
6.485 - @{antiquotation_def typeof} & : & \isarantiq \\
6.486 - @{antiquotation_def typ} & : & \isarantiq \\
6.487 - @{antiquotation_def thm_style} & : & \isarantiq \\
6.488 - @{antiquotation_def term_style} & : & \isarantiq \\
6.489 - @{antiquotation_def "text"} & : & \isarantiq \\
6.490 - @{antiquotation_def goals} & : & \isarantiq \\
6.491 - @{antiquotation_def subgoals} & : & \isarantiq \\
6.492 - @{antiquotation_def prf} & : & \isarantiq \\
6.493 - @{antiquotation_def full_prf} & : & \isarantiq \\
6.494 - @{antiquotation_def ML} & : & \isarantiq \\
6.495 - @{antiquotation_def ML_type} & : & \isarantiq \\
6.496 - @{antiquotation_def ML_struct} & : & \isarantiq \\
6.497 - \end{matharray}
6.498 -
6.499 - The text body of formal comments (see also \secref{sec:comments})
6.500 - may contain antiquotations of logical entities, such as theorems,
6.501 - terms and types, which are to be presented in the final output
6.502 - produced by the Isabelle document preparation system (see also
6.503 - \secref{sec:document-prep}).
6.504 -
6.505 - Thus embedding of ``@{text "@{term [show_types] \"f x = a + x\"}"}''
6.506 - within a text block would cause
6.507 - \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.508 - antiquotations may involve attributes as well. For example,
6.509 - @{text "@{thm sym [no_vars]}"} would print the theorem's
6.510 - statement where all schematic variables have been replaced by fixed
6.511 - ones, which are easier to read.
6.512 -
6.513 - \begin{rail}
6.514 - atsign lbrace antiquotation rbrace
6.515 - ;
6.516 -
6.517 - antiquotation:
6.518 - 'theory' options name |
6.519 - 'thm' options thmrefs |
6.520 - 'prop' options prop |
6.521 - 'term' options term |
6.522 - 'const' options term |
6.523 - 'abbrev' options term |
6.524 - 'typeof' options term |
6.525 - 'typ' options type |
6.526 - 'thm\_style' options name thmref |
6.527 - 'term\_style' options name term |
6.528 - 'text' options name |
6.529 - 'goals' options |
6.530 - 'subgoals' options |
6.531 - 'prf' options thmrefs |
6.532 - 'full\_prf' options thmrefs |
6.533 - 'ML' options name |
6.534 - 'ML\_type' options name |
6.535 - 'ML\_struct' options name
6.536 - ;
6.537 - options: '[' (option * ',') ']'
6.538 - ;
6.539 - option: name | name '=' name
6.540 - ;
6.541 - \end{rail}
6.542 -
6.543 - Note that the syntax of antiquotations may \emph{not} include source
6.544 - comments @{verbatim "(*"}~@{text "\<dots>"}~@{verbatim "*)"} or verbatim
6.545 - text @{verbatim "{"}@{verbatim "*"}~@{text "\<dots>"}~@{verbatim
6.546 - "*"}@{verbatim "}"}.
6.547 -
6.548 - \begin{descr}
6.549 -
6.550 - \item [@{text "@{theory A}"}] prints the name @{text "A"}, which is
6.551 - guaranteed to refer to a valid ancestor theory in the current
6.552 - context.
6.553 -
6.554 - \item [@{text "@{thm a\<^sub>1 \<dots> a\<^sub>n}"}] prints theorems
6.555 - @{text "a\<^sub>1 \<dots> a\<^sub>n"}. Note that attribute specifications
6.556 - may be included as well (see also \secref{sec:syn-att}); the
6.557 - @{attribute_ref no_vars} rule (see \secref{sec:misc-meth-att}) would
6.558 - be particularly useful to suppress printing of schematic variables.
6.559 -
6.560 - \item [@{text "@{prop \<phi>}"}] prints a well-typed proposition @{text
6.561 - "\<phi>"}.
6.562 -
6.563 - \item [@{text "@{term t}"}] prints a well-typed term @{text "t"}.
6.564 -
6.565 - \item [@{text "@{const c}"}] prints a logical or syntactic constant
6.566 - @{text "c"}.
6.567 -
6.568 - \item [@{text "@{abbrev c x\<^sub>1 \<dots> x\<^sub>n}"}] prints a constant
6.569 - abbreviation @{text "c x\<^sub>1 \<dots> x\<^sub>n \<equiv> rhs"} as defined in
6.570 - the current context.
6.571 -
6.572 - \item [@{text "@{typeof t}"}] prints the type of a well-typed term
6.573 - @{text "t"}.
6.574 -
6.575 - \item [@{text "@{typ \<tau>}"}] prints a well-formed type @{text "\<tau>"}.
6.576 -
6.577 - \item [@{text "@{thm_style s a}"}] prints theorem @{text a},
6.578 - previously applying a style @{text s} to it (see below).
6.579 -
6.580 - \item [@{text "@{term_style s t}"}] prints a well-typed term @{text
6.581 - t} after applying a style @{text s} to it (see below).
6.582 -
6.583 - \item [@{text "@{text s}"}] prints uninterpreted source text @{text
6.584 - s}. This is particularly useful to print portions of text according
6.585 - to the Isabelle {\LaTeX} output style, without demanding
6.586 - well-formedness (e.g.\ small pieces of terms that should not be
6.587 - parsed or type-checked yet).
6.588 -
6.589 - \item [@{text "@{goals}"}] prints the current \emph{dynamic} goal
6.590 - state. This is mainly for support of tactic-emulation scripts
6.591 - within Isar --- presentation of goal states does not conform to
6.592 - actual human-readable proof documents.
6.593 -
6.594 - Please do not include goal states into document output unless you
6.595 - really know what you are doing!
6.596 -
6.597 - \item [@{text "@{subgoals}"}] is similar to @{text "@{goals}"}, but
6.598 - does not print the main goal.
6.599 -
6.600 - \item [@{text "@{prf a\<^sub>1 \<dots> a\<^sub>n}"}] prints the (compact)
6.601 - proof terms corresponding to the theorems @{text "a\<^sub>1 \<dots>
6.602 - a\<^sub>n"}. Note that this requires proof terms to be switched on
6.603 - for the current object logic (see the ``Proof terms'' section of the
6.604 - Isabelle reference manual for information on how to do this).
6.605 -
6.606 - \item [@{text "@{full_prf a\<^sub>1 \<dots> a\<^sub>n}"}] is like @{text
6.607 - "@{prf a\<^sub>1 \<dots> a\<^sub>n}"}, but displays the full proof terms,
6.608 - i.e.\ also displays information omitted in the compact proof term,
6.609 - which is denoted by ``@{text _}'' placeholders there.
6.610 -
6.611 - \item [@{text "@{ML s}"}, @{text "@{ML_type s}"}, and @{text
6.612 - "@{ML_struct s}"}] check text @{text s} as ML value, type, and
6.613 - structure, respectively. The source is displayed verbatim.
6.614 -
6.615 - \end{descr}
6.616 -
6.617 - \medskip The following standard styles for use with @{text
6.618 - thm_style} and @{text term_style} are available:
6.619 -
6.620 - \begin{descr}
6.621 -
6.622 - \item [@{text lhs}] extracts the first argument of any application
6.623 - form with at least two arguments -- typically meta-level or
6.624 - object-level equality, or any other binary relation.
6.625 -
6.626 - \item [@{text rhs}] is like @{text lhs}, but extracts the second
6.627 - argument.
6.628 -
6.629 - \item [@{text "concl"}] extracts the conclusion @{text C} from a rule
6.630 - in Horn-clause normal form @{text "A\<^sub>1 \<Longrightarrow> \<dots> A\<^sub>n \<Longrightarrow> C"}.
6.631 -
6.632 - \item [@{text "prem1"}, \dots, @{text "prem9"}] extract premise
6.633 - number @{text "1, \<dots>, 9"}, respectively, from from a rule in
6.634 - Horn-clause normal form @{text "A\<^sub>1 \<Longrightarrow> \<dots> A\<^sub>n \<Longrightarrow> C"}
6.635 -
6.636 - \end{descr}
6.637 -
6.638 - \medskip
6.639 - The following options are available to tune the output. Note that most of
6.640 - these coincide with ML flags of the same names (see also \cite{isabelle-ref}).
6.641 -
6.642 - \begin{descr}
6.643 -
6.644 - \item[@{text "show_types = bool"} and @{text "show_sorts = bool"}]
6.645 - control printing of explicit type and sort constraints.
6.646 -
6.647 - \item[@{text "show_structs = bool"}] controls printing of implicit
6.648 - structures.
6.649 -
6.650 - \item[@{text "long_names = bool"}] forces names of types and
6.651 - constants etc.\ to be printed in their fully qualified internal
6.652 - form.
6.653 -
6.654 - \item[@{text "short_names = bool"}] forces names of types and
6.655 - constants etc.\ to be printed unqualified. Note that internalizing
6.656 - the output again in the current context may well yield a different
6.657 - result.
6.658 -
6.659 - \item[@{text "unique_names = bool"}] determines whether the printed
6.660 - version of qualified names should be made sufficiently long to avoid
6.661 - overlap with names declared further back. Set to @{text false} for
6.662 - more concise output.
6.663 -
6.664 - \item[@{text "eta_contract = bool"}] prints terms in @{text
6.665 - \<eta>}-contracted form.
6.666 -
6.667 - \item[@{text "display = bool"}] indicates if the text is to be
6.668 - output as multi-line ``display material'', rather than a small piece
6.669 - of text without line breaks (which is the default).
6.670 -
6.671 - \item[@{text "break = bool"}] controls line breaks in non-display
6.672 - material.
6.673 -
6.674 - \item[@{text "quotes = bool"}] indicates if the output should be
6.675 - enclosed in double quotes.
6.676 -
6.677 - \item[@{text "mode = name"}] adds @{text name} to the print mode to
6.678 - be used for presentation (see also \cite{isabelle-ref}). Note that
6.679 - the standard setup for {\LaTeX} output is already present by
6.680 - default, including the modes @{text latex} and @{text xsymbols}.
6.681 -
6.682 - \item[@{text "margin = nat"} and @{text "indent = nat"}] change the
6.683 - margin or indentation for pretty printing of display material.
6.684 -
6.685 - \item[@{text "source = bool"}] prints the source text of the
6.686 - antiquotation arguments, rather than the actual value. Note that
6.687 - this does not affect well-formedness checks of @{antiquotation
6.688 - "thm"}, @{antiquotation "term"}, etc. (only the @{antiquotation
6.689 - "text"} antiquotation admits arbitrary output).
6.690 -
6.691 - \item[@{text "goals_limit = nat"}] determines the maximum number of
6.692 - goals to be printed.
6.693 -
6.694 - \item[@{text "locale = name"}] specifies an alternative locale
6.695 - context used for evaluating and printing the subsequent argument.
6.696 -
6.697 - \end{descr}
6.698 -
6.699 - For boolean flags, ``@{text "name = true"}'' may be abbreviated as
6.700 - ``@{text name}''. All of the above flags are disabled by default,
6.701 - unless changed from ML.
6.702 -
6.703 - \medskip Note that antiquotations do not only spare the author from
6.704 - tedious typing of logical entities, but also achieve some degree of
6.705 - consistency-checking of informal explanations with formal
6.706 - developments: well-formedness of terms and types with respect to the
6.707 - current theory or proof context is ensured here.
6.708 -*}
6.709 -
6.710 -
6.711 -subsection {* Tagged commands \label{sec:tags} *}
6.712 -
6.713 -text {*
6.714 - Each Isabelle/Isar command may be decorated by presentation tags:
6.715 -
6.716 - \indexouternonterm{tags}
6.717 - \begin{rail}
6.718 - tags: ( tag * )
6.719 - ;
6.720 - tag: '\%' (ident | string)
6.721 - \end{rail}
6.722 -
6.723 - The tags @{text "theory"}, @{text "proof"}, @{text "ML"} are already
6.724 - pre-declared for certain classes of commands:
6.725 -
6.726 - \medskip
6.727 -
6.728 - \begin{tabular}{ll}
6.729 - @{text "theory"} & theory begin/end \\
6.730 - @{text "proof"} & all proof commands \\
6.731 - @{text "ML"} & all commands involving ML code \\
6.732 - \end{tabular}
6.733 -
6.734 - \medskip The Isabelle document preparation system (see also
6.735 - \cite{isabelle-sys}) allows tagged command regions to be presented
6.736 - specifically, e.g.\ to fold proof texts, or drop parts of the text
6.737 - completely.
6.738 -
6.739 - For example ``@{command "by"}~@{text "%invisible auto"}'' would
6.740 - cause that piece of proof to be treated as @{text invisible} instead
6.741 - of @{text "proof"} (the default), which may be either show or hidden
6.742 - depending on the document setup. In contrast, ``@{command
6.743 - "by"}~@{text "%visible auto"}'' would force this text to be shown
6.744 - invariably.
6.745 -
6.746 - Explicit tag specifications within a proof apply to all subsequent
6.747 - commands of the same level of nesting. For example, ``@{command
6.748 - "proof"}~@{text "%visible \<dots>"}~@{command "qed"}'' would force the
6.749 - whole sub-proof to be typeset as @{text visible} (unless some of its
6.750 - parts are tagged differently).
6.751 -*}
6.752 -
6.753 -end
7.1 --- a/doc-src/IsarRef/isar-ref.tex Mon Jun 02 21:13:48 2008 +0200
7.2 +++ b/doc-src/IsarRef/isar-ref.tex Mon Jun 02 21:19:46 2008 +0200
7.3 @@ -75,7 +75,7 @@
7.4
7.5 \input{Thy/document/Introduction.tex}
7.6 \input{basics.tex}
7.7 -\input{Thy/document/syntax.tex}
7.8 +\input{Thy/document/Outer_Syntax.tex}
7.9 \input{Thy/document/Spec.tex}
7.10 \input{Thy/document/Proof.tex}
7.11 \input{Thy/document/pure.tex}