1.1 --- a/doc-src/IsarRef/pure.tex Thu Oct 21 15:57:26 1999 +0200
1.2 +++ b/doc-src/IsarRef/pure.tex Thu Oct 21 17:42:21 1999 +0200
1.3 @@ -1,12 +1,12 @@
1.4
1.5 -\chapter{Basic Isar Elements}\label{ch:pure-syntax}
1.6 +\chapter{Basic Isar Language Elements}\label{ch:pure-syntax}
1.7
1.8 Subsequently, we introduce the main part of the basic Isar theory and proof
1.9 commands as provided by Isabelle/Pure. Chapter~\ref{ch:gen-tools} describes
1.10 -further Isar elements as provided by generic tools and packages (such as the
1.11 -Simplifier) that are either part of Pure Isabelle, or pre-loaded by most
1.12 -object logics. See chapter~\ref{ch:hol-tools} for actual object-logic
1.13 -specific elements (for Isabelle/HOL).
1.14 +further Isar elements provided by generic tools and packages (such as the
1.15 +Simplifier) that are either part of Pure Isabelle or pre-loaded by most object
1.16 +logics. Chapter~\ref{ch:hol-tools} refers to actual object-logic specific
1.17 +elements of Isabelle/HOL.
1.18
1.19 \medskip
1.20
1.21 @@ -24,8 +24,9 @@
1.22
1.23 \subsection{Defining theories}\label{sec:begin-thy}
1.24
1.25 -\indexisarcmd{theory}\indexisarcmd{end}\indexisarcmd{context}
1.26 +\indexisarcmd{header}\indexisarcmd{theory}\indexisarcmd{end}\indexisarcmd{context}
1.27 \begin{matharray}{rcl}
1.28 + \isarcmd{header} & : & \isarkeep{toplevel} \\
1.29 \isarcmd{theory} & : & \isartrans{\cdot}{theory} \\
1.30 \isarcmd{context}^* & : & \isartrans{\cdot}{theory} \\
1.31 \isarcmd{end} & : & \isartrans{theory}{\cdot} \\
1.32 @@ -37,13 +38,18 @@
1.33 proof as well. In contrast, ``old-style'' Isabelle theories support batch
1.34 processing only, with the proof scripts collected in separate ML files.
1.35
1.36 -The first command of any theory has to be $\THEORY$, starting a new theory
1.37 -based on the merge of existing ones. The theory context may be also changed
1.38 -by $\CONTEXT$ without creating a new theory. In both cases, $\END$ concludes
1.39 -the theory development; it has to be the very last command of any proper
1.40 -theory file.
1.41 +The first actual command of any theory has to be $\THEORY$, starting a new
1.42 +theory based on the merge of existing ones. Just preceding $\THEORY$, there
1.43 +may be an optional $\isarkeyword{header}$ declaration, which is relevant to
1.44 +document preparation only; it acts very much like a special pre-theory markup
1.45 +command (cf.\ \S\ref{sec:markup-thy} and \S\ref{sec:markup-thy}). The theory
1.46 +context may be also changed by $\CONTEXT$ without creating a new theory. In
1.47 +both cases, $\END$ concludes the theory development; it has to be the very
1.48 +last command in a theory file.
1.49
1.50 \begin{rail}
1.51 + 'header' text
1.52 + ;
1.53 'theory' name '=' (name + '+') filespecs? ':'
1.54 ;
1.55 'context' name
1.56 @@ -55,6 +61,12 @@
1.57 \end{rail}
1.58
1.59 \begin{descr}
1.60 +\item [$\isarkeyword{header}~text$] provides plain text markup just preceding
1.61 + the formal begin of a theory. In actual document preparation the
1.62 + corresponding {\LaTeX} macro \verb,\isamarkupheader, may be redefined to
1.63 + produce chapter or section headings. See also \S\ref{sec:markup-thy} and
1.64 + \S\ref{sec:markup-prf} for further markup commands.
1.65 +
1.66 \item [$\THEORY~A = B@1 + \cdots + B@n$] commences a new theory $A$ based on
1.67 existing ones $B@1 + \cdots + B@n$. Isabelle's theory loader system ensures
1.68 that any of the base theories are properly loaded (and fully up-to-date when
1.69 @@ -65,64 +77,70 @@
1.70 associated with any theory should \emph{not} be included in
1.71 $\isarkeyword{files}$.
1.72
1.73 -\item [$\CONTEXT~B$] enters an existing theory context $B$, basically in
1.74 - read-only mode, so only a limited set of commands may be performed. Just as
1.75 - for $\THEORY$, the theory loader ensures that $B$ is loaded and up-to-date.
1.76 +\item [$\CONTEXT~B$] enters an existing theory context, basically in read-only
1.77 + mode, so only a limited set of commands may be performed. Just as for
1.78 + $\THEORY$, the theory loader ensures that $B$ is loaded and up-to-date.
1.79
1.80 \item [$\END$] concludes the current theory definition or context switch.
1.81 - Note that this command cannot be undone, instead the theory definition
1.82 - itself has to be retracted.
1.83 + Note that this command cannot be undone, instead the whole theory definition
1.84 + has to be retracted.
1.85 \end{descr}
1.86
1.87
1.88 -\subsection{Formal comments}\label{sec:formal-cmt-thy}
1.89 +\subsection{Theory markup commands}\label{sec:markup-thy}
1.90
1.91 -\indexisarcmd{title}\indexisarcmd{chapter}\indexisarcmd{section}\indexisarcmd{subsection}
1.92 -\indexisarcmd{subsubsection}\indexisarcmd{text}
1.93 +\indexisarcmd{chapter}\indexisarcmd{section}\indexisarcmd{subsection}
1.94 +\indexisarcmd{subsubsection}\indexisarcmd{text}\indexisarcmd{text-raw}
1.95 \begin{matharray}{rcl}
1.96 - \isarcmd{title} & : & \isartrans{theory}{theory} \\
1.97 \isarcmd{chapter} & : & \isartrans{theory}{theory} \\
1.98 \isarcmd{section} & : & \isartrans{theory}{theory} \\
1.99 \isarcmd{subsection} & : & \isartrans{theory}{theory} \\
1.100 \isarcmd{subsubsection} & : & \isartrans{theory}{theory} \\
1.101 \isarcmd{text} & : & \isartrans{theory}{theory} \\
1.102 + \isarcmd{text_raw} & : & \isartrans{theory}{theory} \\
1.103 \end{matharray}
1.104
1.105 -There are several commands to include \emph{formal comments} in theory
1.106 -specification (a few more are available for proofs, see
1.107 -\S\ref{sec:formal-cmt-prf}). In contrast to source-level comments
1.108 -\verb|(*|\dots\verb|*)|, which are stripped at the lexical level, any text
1.109 -given as formal comment is meant to be part of the actual document.
1.110 -Consequently, it would be included in the final printed version.
1.111 +Apart from formal comments (see \S\ref{sec:comments}), markup commands provide
1.112 +another way to insert text into the document generated from a theory (see
1.113 +\cite{isabelle-sys} for more information on Isabelle's document preparation
1.114 +tools).
1.115
1.116 -Apart from plain prose, formal comments may also refer to logical entities of
1.117 -the theory context (types, terms, theorems etc.). Proper processing of the
1.118 -text would then include some further consistency checks with the items
1.119 -declared in the current theory, e.g.\ type-checking of included
1.120 -terms.\footnote{The current version of Isabelle/Isar does not process formal
1.121 - comments in any such way. This will be available as part of the automatic
1.122 - theory and proof document preparation system (using (PDF){\LaTeX}) that is
1.123 - planned for the near future.}
1.124 +\railalias{textraw}{text\_raw}
1.125 +\railterm{textraw}
1.126
1.127 \begin{rail}
1.128 - 'title' text text? text?
1.129 - ;
1.130 - ('chapter' | 'section' | 'subsection' | 'subsubsection' | 'text') text
1.131 + ('chapter' | 'section' | 'subsection' | 'subsubsection' | 'text' | textraw) text
1.132 ;
1.133 \end{rail}
1.134
1.135 \begin{descr}
1.136 -\item [$\isarkeyword{title}~title~author~date$] specifies the document title
1.137 - just as in typical {\LaTeX} documents.
1.138 \item [$\isarkeyword{chapter}$, $\isarkeyword{section}$,
1.139 $\isarkeyword{subsection}$, and $\isarkeyword{subsubsection}$] mark chapter
1.140 and section headings.
1.141 -\item [$\TEXT$] specifies an actual body of prose text, including references
1.142 - to formal entities.\footnote{The latter feature is not yet exploited.
1.143 - Nevertheless, any text of the form \texttt{\at\ttlbrace\dots\ttrbrace}
1.144 - should be considered as reserved for future use.}
1.145 +\item [$\TEXT$] specifies paragraphs of plain text, including references to
1.146 + formal entities.\footnote{The latter feature is not yet supported.
1.147 + Nevertheless, any source text of the form
1.148 + ``\texttt{\at\ttlbrace$\dots$\ttrbrace}'' should be considered as reserved
1.149 + for future use.}
1.150 +\item [$\isarkeyword{text_raw}$] inserts {\LaTeX} source into the output,
1.151 + without additional markup. Thus the full range of document manipulations
1.152 + becomes available. A typical application would be to emit
1.153 + \verb,\begin{comment}, and \verb,\end{comment}, commands to exclude certain
1.154 + parts from the final document.\footnote{This requires the \texttt{comment}
1.155 + {\LaTeX} package to be included}
1.156 \end{descr}
1.157
1.158 +Any markup command (except $\isarkeyword{text_raw}$) corresponds to a {\LaTeX}
1.159 +macro with the name derived from \verb,\isamarkup, (e.g.\
1.160 +\verb,\isamarkupchapter, for $\isarkeyword{chapter}$). The \railqtoken{text}
1.161 +argument is passed to that macro unchanged, i.e.\ any {\LaTeX} commands may be
1.162 +included here.
1.163 +
1.164 +\medskip Further markup commands are available for proofs (see
1.165 +\S\ref{sec:markup-prf}). Also note that the $\isarkeyword{header}$
1.166 +declaration (see \S\ref{sec:begin-thy}) admits to insert document markup
1.167 +elements just preceding the actual theory definition.
1.168 +
1.169
1.170 \subsection{Type classes and sorts}\label{sec:classes}
1.171
1.172 @@ -147,10 +165,10 @@
1.173 of existing classes $\vec c$. Cyclic class structures are ruled out.
1.174 \item [$\isarkeyword{classrel}~c@1<c@2$] states a subclass relation between
1.175 existing classes $c@1$ and $c@2$. This is done axiomatically! The
1.176 - $\isarkeyword{instance}$ command (see \S\ref{sec:axclass}) provides a way
1.177 + $\isarkeyword{instance}$ command (see \S\ref{sec:axclass}) provides a way to
1.178 introduce proven class relations.
1.179 \item [$\isarkeyword{defaultsort}~s$] makes sort $s$ the new default sort for
1.180 - any type variables input without sort constraints. Usually, the default
1.181 + any type variables given without sort constraints. Usually, the default
1.182 sort would be only changed when defining new logics.
1.183 \end{descr}
1.184
1.185 @@ -180,19 +198,19 @@
1.186 \item [$\TYPES~(\vec\alpha)t = \tau$] introduces \emph{type synonym}
1.187 $(\vec\alpha)t$ for existing type $\tau$. Unlike actual type definitions,
1.188 as are available in Isabelle/HOL for example, type synonyms are just purely
1.189 - syntactic abbreviations, without any logical significance. Internally, type
1.190 + syntactic abbreviations without any logical significance. Internally, type
1.191 synonyms are fully expanded, as may be observed when printing terms or
1.192 theorems.
1.193 \item [$\isarkeyword{typedecl}~(\vec\alpha)t$] declares a new type constructor
1.194 - $t$, intended as an actual logical type. Note that some logics such as
1.195 - Isabelle/HOL provide their own version of $\isarkeyword{typedecl}$.
1.196 + $t$, intended as an actual logical type. Note that object-logics such as
1.197 + Isabelle/HOL override $\isarkeyword{typedecl}$ by their own version.
1.198 \item [$\isarkeyword{nonterminals}~\vec c$] declares $0$-ary type constructors
1.199 $\vec c$ to act as purely syntactic types, i.e.\ nonterminal symbols of
1.200 Isabelle's inner syntax of terms or types.
1.201 \item [$\isarkeyword{arities}~t::(\vec s)s$] augments Isabelle's order-sorted
1.202 signature of types by new type constructor arities. This is done
1.203 axiomatically! The $\isarkeyword{instance}$ command (see
1.204 - \S\ref{sec:axclass}) provides a way introduce proven type arities.
1.205 + \S\ref{sec:axclass}) provides a way to introduce proven type arities.
1.206 \end{descr}
1.207
1.208
1.209 @@ -220,7 +238,7 @@
1.210 \begin{descr}
1.211 \item [$\CONSTS~c::\sigma$] declares constant $c$ to have any instance of type
1.212 scheme $\sigma$. The optional mixfix annotations may attach concrete syntax
1.213 - constants.
1.214 + to the constants declared.
1.215 \item [$\DEFS~name: eqn$] introduces $eqn$ as a definitional axiom for some
1.216 existing constant. See \cite[\S6]{isabelle-ref} for more details on the
1.217 form of equations admitted as constant definitions.
1.218 @@ -256,9 +274,9 @@
1.219 \texttt{output} flag given, all productions are added both to the input and
1.220 output grammar.
1.221 \item [$\isarkeyword{translations}~rules$] specifies syntactic translation
1.222 - rules (also known as \emph{macros}): parse/print rules (\texttt{==}), parse
1.223 - rules (\texttt{=>}), or print rules (\texttt{<=}). Translation patterns may
1.224 - be prefixed by the syntactic category to be used for parsing; the default is
1.225 + rules (i.e.\ \emph{macros}): parse/print rules (\texttt{==}), parse rules
1.226 + (\texttt{=>}), or print rules (\texttt{<=}). Translation patterns may be
1.227 + prefixed by the syntactic category to be used for parsing; the default is
1.228 \texttt{logic}.
1.229 \end{descr}
1.230
1.231 @@ -281,8 +299,8 @@
1.232
1.233 \begin{descr}
1.234 \item [$\isarkeyword{axioms}~a: \phi$] introduces arbitrary statements as
1.235 - logical axioms. In fact, axioms are ``axiomatic theorems'', and may be
1.236 - referred later just as any other theorem.
1.237 + axioms of the meta-logic. In fact, axioms are ``axiomatic theorems'', and
1.238 + may be referred later just as any other theorem.
1.239
1.240 Axioms are usually only introduced when declaring new logical systems.
1.241 Everyday work is typically done the hard way, with proper definitions and
1.242 @@ -303,35 +321,37 @@
1.243 \isarcmd{local} & : & \isartrans{theory}{theory} \\
1.244 \end{matharray}
1.245
1.246 -Isabelle organizes any kind of names (of types, constants, theorems etc.) by
1.247 -hierarchically structured name spaces. Normally the user never has to control
1.248 -the behavior of name space entry by hand, yet the following commands provide
1.249 -some way to do so.
1.250 +Isabelle organizes any kind of name declarations (of types, constants,
1.251 +theorems etc.) by hierarchically structured name spaces. Normally the user
1.252 +never has to control the behavior of name space entry by hand, yet the
1.253 +following commands provide some way to do so.
1.254
1.255 \begin{descr}
1.256 \item [$\isarkeyword{global}$ and $\isarkeyword{local}$] change the current
1.257 name declaration mode. Initially, theories start in $\isarkeyword{local}$
1.258 mode, causing all names to be automatically qualified by the theory name.
1.259 - Changing this to $\isarkeyword{global}$ causes all names to be declared as
1.260 - base names only, until $\isarkeyword{local}$ is declared again.
1.261 + Changing this to $\isarkeyword{global}$ causes all names to be declared
1.262 + without the theory prefix, until $\isarkeyword{local}$ is declared again.
1.263 \end{descr}
1.264
1.265
1.266 \subsection{Incorporating ML code}\label{sec:ML}
1.267
1.268 -\indexisarcmd{use}\indexisarcmd{ML}\indexisarcmd{setup}
1.269 +\indexisarcmd{use}\indexisarcmd{ML}\indexisarcmd{ML-setup}\indexisarcmd{setup}
1.270 \begin{matharray}{rcl}
1.271 \isarcmd{use} & : & \isartrans{\cdot}{\cdot} \\
1.272 \isarcmd{ML} & : & \isartrans{\cdot}{\cdot} \\
1.273 + \isarcmd{ML_setup} & : & \isartrans{theory}{theory} \\
1.274 \isarcmd{setup} & : & \isartrans{theory}{theory} \\
1.275 \end{matharray}
1.276
1.277 +\railalias{MLsetup}{ML\_setup}
1.278 +\railterm{MLsetup}
1.279 +
1.280 \begin{rail}
1.281 'use' name
1.282 ;
1.283 - 'ML' text
1.284 - ;
1.285 - 'setup' text
1.286 + ('ML' | MLsetup | 'setup') text
1.287 ;
1.288 \end{rail}
1.289
1.290 @@ -342,13 +362,18 @@
1.291 $\isarkeyword{files}$ dependency declaration given in the theory header (see
1.292 also \S\ref{sec:begin-thy}).
1.293
1.294 -\item [$\isarkeyword{ML}~text$] reads and executes ML commands from $text$.
1.295 - The theory context is passed in the same way as for $\isarkeyword{use}$.
1.296 -
1.297 +\item [$\isarkeyword{ML}~text$] executes ML commands from $text$. The theory
1.298 + context is passed in the same way as for $\isarkeyword{use}$.
1.299 +
1.300 +\item [$\isarkeyword{ML_setup}~text$] executes ML commands from $text$. The
1.301 + theory context is passed down to the ML session, and fetched back
1.302 + afterwards. Thus $text$ may actually change the theory as a side effect.
1.303 +
1.304 \item [$\isarkeyword{setup}~text$] changes the current theory context by
1.305 - applying setup functions $text$, which has to be an ML expression of type
1.306 - $(theory \to theory)~list$. The $\isarkeyword{setup}$ command is the usual
1.307 - way to initialize object-logic specific tools and packages written in ML.
1.308 + applying setup functions from $text$, which has to refer to an ML expression
1.309 + of type $(theory \to theory)~list$. The $\isarkeyword{setup}$ command is
1.310 + the canonical way to initialize object-logic specific tools and packages
1.311 + written in ML.
1.312 \end{descr}
1.313
1.314
1.315 @@ -406,30 +431,36 @@
1.316 \begin{descr}
1.317 \item [$proof(prove)$] means that a new goal has just been stated that is now
1.318 to be \emph{proven}; the next command may refine it by some proof method
1.319 - ($\approx$ tactic), and enter a sub-proof to establish the final result.
1.320 + (read: tactic), and enter a sub-proof to establish the actual result.
1.321 \item [$proof(state)$] is like an internal theory mode: the context may be
1.322 augmented by \emph{stating} additional assumptions, intermediate result etc.
1.323 -\item [$proof(chain)$] is an intermediate mode between $proof(state)$ and
1.324 +\item [$proof(chain)$] is intermediate between $proof(state)$ and
1.325 $proof(prove)$: existing facts (i.e.\ the contents of $this$) have been just
1.326 - picked up in order to use them when refining the goal claimed next.
1.327 + picked up in order to be used when refining the goal claimed next.
1.328 \end{descr}
1.329
1.330
1.331 -\subsection{Formal comments}\label{sec:formal-cmt-prf}
1.332 +\subsection{Proof markup commands}\label{sec:markup-prf}
1.333
1.334 -\indexisarcmd{sect}\indexisarcmd{subsect}\indexisarcmd{subsect}\indexisarcmd{txt}
1.335 +\indexisarcmd{sect}\indexisarcmd{subsect}\indexisarcmd{subsect}
1.336 +\indexisarcmd{txt}\indexisarcmd{txt-raw}
1.337 \begin{matharray}{rcl}
1.338 \isarcmd{sect} & : & \isartrans{proof(state)}{proof(state)} \\
1.339 \isarcmd{subsect} & : & \isartrans{proof(state)}{proof(state)} \\
1.340 \isarcmd{subsubsect} & : & \isartrans{proof(state)}{proof(state)} \\
1.341 \isarcmd{txt} & : & \isartrans{proof(state)}{proof(state)} \\
1.342 + \isarcmd{txt_raw} & : & \isartrans{proof(state)}{proof(state)} \\
1.343 \end{matharray}
1.344
1.345 -These formal comments in proof mode closely correspond to the ones of theory
1.346 -mode (see \S\ref{sec:formal-cmt-thy}).
1.347 +These markup commands for proof mode closely correspond to the ones of theory
1.348 +mode (see \S\ref{sec:markup-thy}). Note that $\isarkeyword{txt_raw}$ is
1.349 +special in the same way as $\isarkeyword{text_raw}$.
1.350 +
1.351 +\railalias{txtraw}{txt\_raw}
1.352 +\railterm{txtraw}
1.353
1.354 \begin{rail}
1.355 - ('sect' | 'subsect' | 'subsubsect' | 'txt') text
1.356 + ('sect' | 'subsect' | 'subsubsect' | 'txt' | txtraw) text
1.357 ;
1.358 \end{rail}
1.359
1.360 @@ -449,24 +480,25 @@
1.361 quantification as provided by the Isabelle/Pure logical framework.
1.362 Introducing some \emph{arbitrary, but fixed} variable via $\FIX x$ results in
1.363 a local object that may be used in the subsequent proof as any other variable
1.364 -or constant. Furthermore, any result $\phi[x]$ exported from the current
1.365 -context will be universally closed wrt.\ $x$ at the outermost level (this is
1.366 -expressed using Isabelle's meta-variables).
1.367 +or constant. Furthermore, any result $\edrv \phi[x]$ exported from the
1.368 +current context will be universally closed wrt.\ $x$ at the outermost level:
1.369 +$\edrv \All x \phi$; this is expressed using Isabelle's meta-variables.
1.370
1.371 Similarly, introducing some assumption $\chi$ has two effects. On the one
1.372 hand, a local theorem is created that may be used as a fact in subsequent
1.373 -proof steps. On the other hand, any result $\phi$ exported from the context
1.374 -becomes conditional wrt.\ the assumption. Thus, solving an enclosing goal
1.375 -using such a result would basically introduce a new subgoal stemming from the
1.376 -assumption. How this situation is handled depends on the actual version of
1.377 -assumption command used: while $\ASSUMENAME$ solves the subgoal by unifying
1.378 -with some premise of the goal, $\PRESUMENAME$ leaves the subgoal unchanged to
1.379 -be proved later by the user.
1.380 +proof steps. On the other hand, any result $\chi \drv \phi$ exported from the
1.381 +context becomes conditional wrt.\ the assumption: $\edrv \chi \Imp \phi$.
1.382 +Thus, solving an enclosing goal using such a result would basically introduce
1.383 +a new subgoal stemming from the assumption. How this situation is handled
1.384 +depends on the actual version of assumption command used: while $\ASSUMENAME$
1.385 +insists on solving the subgoal by unification with some premise of the goal,
1.386 +$\PRESUMENAME$ leaves the subgoal unchanged in order to be proved later by the
1.387 +user.
1.388
1.389 Local definitions, introduced by $\DEF{}{x \equiv t}$, are achieved by
1.390 combining $\FIX x$ with another kind of assumption that causes any
1.391 -hypothetical equation $x = t$ to be eliminated by reflexivity. Thus,
1.392 -exporting some result $\phi[x]$ simply yields $\phi[t]$.
1.393 +hypothetical equation $x \equiv t$ to be eliminated by reflexivity. Thus,
1.394 +exporting some result $x \equiv t \drv \phi[x]$ yields $\edrv \phi[t]$.
1.395
1.396 \begin{rail}
1.397 'fix' (vars + 'and') comment?
1.398 @@ -488,13 +520,13 @@
1.399 \item [$\FIX{x}$] introduces a local \emph{arbitrary, but fixed} variable $x$.
1.400 \item [$\ASSUME{a}{\Phi}$ and $\PRESUME{a}{\Phi}$] introduce local theorems
1.401 $\Phi$ by assumption. Subsequent results applied to an enclosing goal
1.402 - (e.g.\ via $\SHOWNAME$) are handled as follows: $\ASSUMENAME$ expects to be
1.403 + (e.g.\ by $\SHOWNAME$) are handled as follows: $\ASSUMENAME$ expects to be
1.404 able to unify with existing premises in the goal, while $\PRESUMENAME$
1.405 leaves $\Phi$ as new subgoals.
1.406
1.407 Several lists of assumptions may be given (separated by
1.408 - $\isarkeyword{and}$); the resulting list of facts consists of all of these
1.409 - concatenated.
1.410 + $\isarkeyword{and}$); the resulting list of current facts consists of all of
1.411 + these concatenated.
1.412 \item [$\DEF{a}{x \equiv t}$] introduces a local (non-polymorphic) definition.
1.413 In results exported from the context, $x$ is replaced by $t$. Basically,
1.414 $\DEF{}{x \equiv t}$ abbreviates $\FIX{x}~\PRESUME{}{x \equiv t}$, with the
1.415 @@ -503,8 +535,8 @@
1.416 The default name for the definitional equation is $x_def$.
1.417 \end{descr}
1.418
1.419 -The special theorem name $prems$\indexisarthm{prems} refers to all current
1.420 -assumptions.
1.421 +The special name $prems$\indexisarthm{prems} refers to all assumptions of the
1.422 +current context as a list of theorems.
1.423
1.424
1.425 \subsection{Facts and forward chaining}
1.426 @@ -536,10 +568,12 @@
1.427 as $a$. Note that attributes may be involved as well, both on the left and
1.428 right hand sides.
1.429 \item [$\THEN$] indicates forward chaining by the current facts in order to
1.430 - establish the goal claimed next. The initial proof method invoked to refine
1.431 - that will be offered these facts to do ``anything appropriate'' (see also
1.432 - \S\ref{sec:proof-steps}). For example, method $rule$ (see
1.433 - \S\ref{sec:pure-meth}) would do an elimination rather than an introduction.
1.434 + establish the goal to be claimed next. The initial proof method invoked to
1.435 + refine that will be offered the facts to do ``anything appropriate'' (cf.\
1.436 + also \S\ref{sec:proof-steps}). For example, method $rule$ (see
1.437 + \S\ref{sec:pure-meth}) would typically do an elimination rather than an
1.438 + introduction. Automatic methods usually insert the facts into the goal
1.439 + state before operation.
1.440 \item [$\FROM{\vec b}$] abbreviates $\NOTE{}{\vec b}~\THEN$; thus $\THEN$ is
1.441 equivalent to $\FROM{this}$.
1.442 \item [$\WITH{\vec b}$] abbreviates $\FROM{\vec b~facts}$; thus the forward
1.443 @@ -547,11 +581,11 @@
1.444 \end{descr}
1.445
1.446 Basic proof methods (such as $rule$, see \S\ref{sec:pure-meth}) expect
1.447 -multiple facts to be given in proper order, corresponding to a prefix of the
1.448 -premises of the rule involved. Note that positions may be easily skipped
1.449 +multiple facts to be given in their proper order, corresponding to a prefix of
1.450 +the premises of the rule involved. Note that positions may be easily skipped
1.451 using a form like $\FROM{\text{\texttt{_}}~a~b}$, for example. This involves
1.452 -the rule $\PROP\psi \Imp \PROP\psi$, which is bound in Isabelle/Pure as
1.453 -``\texttt{_}'' (underscore).\indexisarthm{_@\texttt{_}}
1.454 +the trivial rule $\PROP\psi \Imp \PROP\psi$, which is bound in Isabelle/Pure
1.455 +as ``\texttt{_}'' (underscore).\indexisarthm{_@\texttt{_}}
1.456
1.457
1.458 \subsection{Goal statements}
1.459 @@ -568,9 +602,9 @@
1.460 \end{matharray}
1.461
1.462 Proof mode is entered from theory mode by initial goal commands $\THEOREMNAME$
1.463 -and $\LEMMANAME$. New local goals may be claimed within proof mode: four
1.464 -variants are available, indicating whether the result is meant to solve some
1.465 -pending goal and whether forward chaining is employed.
1.466 +and $\LEMMANAME$. New local goals may be claimed within proof mode as well.
1.467 +Four variants are available, indicating whether the result is meant to solve
1.468 +some pending goal and whether forward chaining is employed.
1.469
1.470 \begin{rail}
1.471 ('theorem' | 'lemma') goal
1.472 @@ -584,19 +618,19 @@
1.473
1.474 \begin{descr}
1.475 \item [$\THEOREM{a}{\phi}$] enters proof mode with $\phi$ as main goal,
1.476 - eventually resulting in some theorem $\turn \phi$, and put back into the
1.477 - theory.
1.478 + eventually resulting in some theorem $\turn \phi$ put back into the theory.
1.479 \item [$\LEMMANAME$] is similar to $\THEOREMNAME$, but tags the result as
1.480 ``lemma''.
1.481 \item [$\HAVE{a}{\phi}$] claims a local goal, eventually resulting in a
1.482 theorem with the current assumption context as hypotheses.
1.483 \item [$\SHOW{a}{\phi}$] is similar to $\HAVE{a}{\phi}$, but solves some
1.484 - pending goal with the result \emph{exported} into the corresponding context.
1.485 -\item [$\HENCE{a}{\phi}$] abbreviates $\THEN~\HAVE{a}{\phi}$, i.e.\ claims a
1.486 - local goal to be proven by forward chaining the current facts. Note that
1.487 - $\HENCENAME$ is equivalent to $\FROM{this}~\HAVENAME$.
1.488 -\item [$\THUS{a}{\phi}$] abbreviates $\THEN~\SHOW{a}{\phi}$. Note that
1.489 - $\THUSNAME$ is equivalent to $\FROM{this}~\SHOWNAME$.
1.490 + pending goal with the result \emph{exported} into the corresponding context
1.491 + (cf.\ \S\ref{sec:proof-context}).
1.492 +\item [$\HENCENAME$] abbreviates $\THEN~\HAVENAME$, i.e.\ claims a local goal
1.493 + to be proven by forward chaining the current facts. Note that $\HENCENAME$
1.494 + is also equivalent to $\FROM{this}~\HAVENAME$.
1.495 +\item [$\THUSNAME$] abbreviates $\THEN~\SHOWNAME$. Note that $\THUSNAME$ is
1.496 + also equivalent to $\FROM{this}~\SHOWNAME$.
1.497 \end{descr}
1.498
1.499
1.500 @@ -618,7 +652,7 @@
1.501 \begin{enumerate}
1.502 \item An \emph{initial} refinement step $\PROOF{m@1}$ reduces a newly stated
1.503 goal to a number of sub-goals that are to be solved later. Facts are passed
1.504 - to $m@1$ for forward chaining if so indicated by $proof(chain)$ mode.
1.505 + to $m@1$ for forward chaining, if so indicated by $proof(chain)$ mode.
1.506
1.507 \item A \emph{terminal} conclusion step $\QED{m@2}$ solves any remaining goals
1.508 completely. No facts are passed to $m@2$.
1.509 @@ -630,20 +664,20 @@
1.510 \medskip
1.511
1.512 Also note that initial proof methods should either solve the goal completely,
1.513 -or constitute some well-understood deterministic reduction to new sub-goals.
1.514 -Arbitrary automatic proof tools that are prone leave a large number of badly
1.515 -structured sub-goals are no help in continuing the proof document in any
1.516 -intelligible way. A much better technique would be to $\SHOWNAME$ some
1.517 -non-trivial reduction as an explicit rule, which is solved completely by some
1.518 -automated method, and then applied to some pending goal.
1.519 +or constitute some well-understood reduction to new sub-goals. Arbitrary
1.520 +automatic proof tools that are prone leave a large number of badly structured
1.521 +sub-goals are no help in continuing the proof document in any intelligible
1.522 +way. A much better technique would be to $\SHOWNAME$ some non-trivial
1.523 +reduction as an explicit rule, which is solved completely by some automated
1.524 +method, and then applied to some pending goal.
1.525
1.526 \medskip
1.527
1.528 Unless given explicitly by the user, the default initial method is
1.529 ``$default$'', which is usually set up to apply a single standard elimination
1.530 or introduction rule according to the topmost symbol involved. There is no
1.531 -default terminal method; in any case the final step is to solve all remaining
1.532 -goals by assumption.
1.533 +separate default terminal method; in any case the final step is to solve all
1.534 +remaining goals by assumption, though.
1.535
1.536 \begin{rail}
1.537 'proof' interest? meth? comment?
1.538 @@ -663,27 +697,31 @@
1.539 \item [$\PROOF{m@1}$] refines the goal by proof method $m@1$; facts for
1.540 forward chaining are passed if so indicated by $proof(chain)$ mode.
1.541 \item [$\QED{m@2}$] refines any remaining goals by proof method $m@2$ and
1.542 - concludes the sub-proof. If the goal had been $\SHOWNAME$ (or $\THUSNAME$),
1.543 - some pending sub-goal is solved as well by the rule resulting from the
1.544 - result exported to the enclosing goal context. Thus $\QEDNAME$ may fail for
1.545 - two reasons: either $m@2$ fails to solve all remaining goals completely, or
1.546 - the resulting rule does not resolve with any enclosing goal. Debugging such
1.547 - a situation might involve temporarily changing $\SHOWNAME$ into $\HAVENAME$,
1.548 - or softening the local context by replacing $\ASSUMENAME$ by $\PRESUMENAME$.
1.549 -\item [$\BYY{m@1}{m@2}$] is a \emph{terminal proof}; it abbreviates
1.550 - $\PROOF{m@1}~\QED{m@2}$, with automatic backtracking across both methods.
1.551 - Debugging an unsuccessful $\BYY{m@1}{m@2}$ commands might be done by simply
1.552 - expanding the abbreviation by hand; note that $\PROOF{m@1}$ is usually
1.553 + concludes the sub-proof by assumption. If the goal had been $\SHOWNAME$ (or
1.554 + $\THUSNAME$), some pending sub-goal is solved as well by the rule resulting
1.555 + from the result \emph{exported} into the enclosing goal context. Thus
1.556 + $\QEDNAME$ may fail for two reasons: either $m@2$ fails, or the resulting
1.557 + rule does not fit to any pending goal\footnote{This includes any additional
1.558 + ``strong'' assumptions as introduced by $\ASSUMENAME$.} of the enclosing
1.559 + context. Debugging such a situation might involve temporarily changing
1.560 + $\SHOWNAME$ into $\HAVENAME$, or weakening the local context by replacing
1.561 + some occurrences of $\ASSUMENAME$ by $\PRESUMENAME$.
1.562 +\item [$\BYY{m@1}{m@2}$] is a \emph{terminal proof}\index{proof!terminal}; it
1.563 + abbreviates $\PROOF{m@1}~\QED{m@2}$, with automatic backtracking across both
1.564 + methods. Debugging an unsuccessful $\BYY{m@1}{m@2}$ commands might be done
1.565 + by expanding its definition; in many cases $\PROOF{m@1}$ is already
1.566 sufficient to see what is going wrong.
1.567 -\item [``$\DDOT$''] is a \emph{default proof}; it abbreviates $\BY{default}$.
1.568 -\item [``$\DOT$''] is a \emph{trivial proof}; it abbreviates
1.569 - $\BY{assumption}$.
1.570 -\item [$\isarkeyword{sorry}$] is a \emph{fake proof}; provided that
1.571 - \texttt{quick_and_dirty} is enabled, $\isarkeyword{sorry}$ pretends to solve
1.572 - the goal without further ado. Of course, the result is a fake theorem only,
1.573 - involving some oracle in its internal derivation object (this is indicated
1.574 - as $[!]$ in the printed result). The main application of
1.575 - $\isarkeyword{sorry}$ is to support top-down proof development.
1.576 +\item [``$\DDOT$''] is a \emph{default proof}\index{proof!default}; it
1.577 + abbreviates $\BY{default}$.
1.578 +\item [``$\DOT$''] is a \emph{trivial proof}\index{proof!trivial}; it
1.579 + abbreviates $\BY{assumption}$.
1.580 +\item [$\isarkeyword{sorry}$] is a \emph{fake proof}\index{proof!fake};
1.581 + provided that \texttt{quick_and_dirty} is enabled, $\isarkeyword{sorry}$
1.582 + pretends to solve the goal without further ado. Of course, the result is a
1.583 + fake theorem only, involving some oracle in its internal derivation object
1.584 + (this is indicated as ``$[!]$'' in the printed result). The main
1.585 + application of $\isarkeyword{sorry}$ is to support experimentation and
1.586 + top-down proof development.
1.587 \end{descr}
1.588
1.589
1.590 @@ -691,7 +729,7 @@
1.591
1.592 The following commands emulate unstructured tactic scripts to some extent.
1.593 While these are anathema for writing proper Isar proof documents, they might
1.594 -come in handy for exploring and debugging.
1.595 +come in handy for interactive exploration and debugging.
1.596
1.597 \indexisarcmd{apply}\indexisarcmd{then-apply}\indexisarcmd{back}
1.598 \begin{matharray}{rcl}
1.599 @@ -713,8 +751,8 @@
1.600 \end{rail}
1.601
1.602 \begin{descr}
1.603 -\item [$\isarkeyword{apply}~(m)$] applies proof method $m$ in the
1.604 - plain-old-tactic sense. Facts for forward chaining are reset.
1.605 +\item [$\isarkeyword{apply}~(m)$] applies proof method $m$ in the plain old
1.606 + tactic sense. Facts for forward chaining are reset.
1.607 \item [$\isarkeyword{then_apply}~(m)$] is similar to $\isarkeyword{apply}$,
1.608 but keeps the goal's facts.
1.609 \item [$\isarkeyword{back}$] does back-tracking over the result sequence of
1.610 @@ -734,8 +772,8 @@
1.611
1.612 Abbreviations may be either bound by explicit $\LET{p \equiv t}$ statements,
1.613 or by annotating assumptions or goal statements ($\ASSUMENAME$, $\SHOWNAME$
1.614 -etc.) with a list of patterns $\IS{p@1 \dots p@n}$. In both cases,
1.615 -higher-order matching is applied to bind extra-logical text variables, which
1.616 +etc.) with a list of patterns $\ISS{p@1 \dots}{p@n}$. In both cases,
1.617 +higher-order matching is invoked to bind extra-logical term variables, which
1.618 may be either named schematic variables of the form $\Var{x}$, or nameless
1.619 dummies ``\texttt{_}'' (underscore).\indexisarvar{_@\texttt{_}} Note that in
1.620 the $\LETNAME$ form the patterns occur on the left-hand side, while the
1.621 @@ -775,7 +813,7 @@
1.622 $\Var{this_concl}$\indexisarvar{this-concl}, and
1.623 $\Var{this}$\indexisarvar{this}, similar to $\Var{thesis}$ above. In case
1.624 $\Var{this}$ refers to an object-logic statement that is an application
1.625 -$f(x)$, then $x$ is bound to the special text variable
1.626 +$f(t)$, then $t$ is bound to the special text variable
1.627 ``$\dots$''\indexisarvar{\dots} (three dots). The canonical application of
1.628 this feature are calculational proofs (see \S\ref{sec:calculation}).
1.629
1.630 @@ -793,24 +831,25 @@
1.631 mostly handled rather casually, with little explicit user-intervention. Any
1.632 local goal statement automatically opens \emph{two} blocks, which are closed
1.633 again when concluding the sub-proof (by $\QEDNAME$ etc.). Sections of
1.634 -different context within a sub-proof are typically switched via
1.635 -$\isarkeyword{next}$, which is just a single block-close followed by
1.636 -block-open again. Thus the effect of $\isarkeyword{next}$ is to reset the
1.637 -proof context to that of the head of the sub-proof. Note that there is no
1.638 -goal focus involved here!
1.639 +different context within a sub-proof may be switched via $\isarkeyword{next}$,
1.640 +which is just a single block-close followed by block-open again. Thus the
1.641 +effect of $\isarkeyword{next}$ is a local reset the proof
1.642 +context.\footnote{There is no goal focus involved here!}
1.643
1.644 For slightly more advanced applications, there are explicit block parentheses
1.645 -as well. These typically achieve a strong forward style of reasoning.
1.646 +as well. These typically achieve a stronger forward style of reasoning.
1.647
1.648 \begin{descr}
1.649 \item [$\isarkeyword{next}$] switches to a fresh block within a sub-proof,
1.650 - resetting the context to the initial one.
1.651 + resetting the local context to the initial one.
1.652 \item [$\isarkeyword{\{\{}$ and $\isarkeyword{\}\}}$] explicitly open and
1.653 - close blocks. Any current facts pass through $\isarkeyword{\{\{}$
1.654 - unchanged, while $\isarkeyword{\}\}}$ causes them to be \emph{exported} into
1.655 - the enclosing context. Thus fixed variables are generalized, assumptions
1.656 - discharged, and local definitions eliminated. There is no difference of
1.657 - $\ASSUMENAME$ and $\PRESUMENAME$ here.
1.658 + close blocks. Any current facts pass through ``$\isarkeyword{\{\{}$''
1.659 + unchanged, while ``$\isarkeyword{\}\}}$'' causes any result to be
1.660 + \emph{exported} into the enclosing context. Thus fixed variables are
1.661 + generalized, assumptions discharged, and local definitions unfolded (cf.\
1.662 + \S\ref{sec:proof-context}). There is no difference of $\ASSUMENAME$ and
1.663 + $\PRESUMENAME$ in this mode of forward reasoning --- in contrast to plain
1.664 + backward reasoning with the result exported at $\SHOWNAME$ time.
1.665 \end{descr}
1.666
1.667
1.668 @@ -842,14 +881,18 @@
1.669 \end{rail}
1.670
1.671 \begin{descr}
1.672 -\item [$\isarkeyword{typ}~\tau$, $\isarkeyword{term}~t$,
1.673 - $\isarkeyword{prop}~\phi$] read and print types / terms / propositions
1.674 +\item [$\isarkeyword{typ}~\tau$] reads and prints types of the meta-logic
1.675 according to the current theory or proof context.
1.676 +\item [$\isarkeyword{term}~t$, $\isarkeyword{prop}~\phi$] read, type-checks
1.677 + and print terms or propositions according to the current theory or proof
1.678 + context; the inferred type of $t$ is output as well. Note that these
1.679 + commands are also useful in inspecting the current environment of term
1.680 + abbreviations.
1.681 \item [$\isarkeyword{thm}~thms$] retrieves lists of theorems from the current
1.682 theory or proof context. Note that any attributes included in the theorem
1.683 specifications are applied to a temporary context derived from the current
1.684 theory or proof; the result is discarded, i.e.\ attributes involved in
1.685 - $thms$ only have a temporary effect.
1.686 + $thms$ do not have any permanent effect.
1.687 \end{descr}
1.688
1.689
1.690 @@ -872,15 +915,16 @@
1.691 \item [$\isarkeyword{pwd}~$] prints the current working directory.
1.692 \item [$\isarkeyword{use_thy}$, $\isarkeyword{use_thy_only}$,
1.693 $\isarkeyword{update_thy}$, and $\isarkeyword{update_thy_only}$] load some
1.694 - theory given as $name$ argument. These commands are exactly the same as the
1.695 - corresponding ML functions (see also \cite[\S1,\S6]{isabelle-ref}). Note
1.696 - that both the ML and Isar versions may load new- and old-style theories
1.697 - alike.
1.698 + theory given as $name$ argument. These commands are basically the same as
1.699 + the corresponding ML functions\footnote{For historic reasons, the original
1.700 + ML versions also change the theory context to that of the theory loaded.}
1.701 + (see also \cite[\S1,\S6]{isabelle-ref}). Note that both the ML and Isar
1.702 + versions may load new- and old-style theories alike.
1.703 \end{descr}
1.704
1.705 -Note that these system commands are scarcely used when working with
1.706 -Proof~General, since loading of theories is done fully automatic.
1.707 -
1.708 +Note that these system commands are scarcely used when working with the
1.709 +Proof~General interface, since loading of theories is done fully
1.710 +transparently.
1.711
1.712 %%% Local Variables:
1.713 %%% mode: latex